From 73a7c5cd18c3a16d9ad37f05b406c3613e4ae5a6 Mon Sep 17 00:00:00 2001 From: mfrisella Date: Wed, 26 Jul 2023 16:28:34 -0700 Subject: [PATCH] bug-reports: strange failure invoking FStar GTot fn in Pulse --- .../examples/pulse/bug-reports/FStarGhost.fst | 47 +++++++++++++++++++ .../pulse/by-example/PulseByExample.fst | 29 ++++++++++-- 2 files changed, 73 insertions(+), 3 deletions(-) create mode 100644 share/steel/examples/pulse/bug-reports/FStarGhost.fst diff --git a/share/steel/examples/pulse/bug-reports/FStarGhost.fst b/share/steel/examples/pulse/bug-reports/FStarGhost.fst new file mode 100644 index 000000000..02e82fe30 --- /dev/null +++ b/share/steel/examples/pulse/bug-reports/FStarGhost.fst @@ -0,0 +1,47 @@ +module FStarGhost + +open Pulse.Main +open Pulse.Steel.Wrapper +open Steel.ST.Util +module G = FStar.Ghost +module R = Steel.ST.Reference +module GR = Steel.ST.GhostReference + +let fstar_gtot_incr (n:G.erased nat) : GTot nat + = n + 1 + +(* this checks *) +```pulse +ghost +fn invoke_fstar_gtot (r:GR.ref nat) (#n:G.erased nat) + requires GR.pts_to r full_perm n + ensures GR.pts_to r full_perm (n+1) +{ + gwrite r (fstar_gtot_incr n) +} +``` + +(* invocation of GTot fcn: expected a total term, got a ghost term *) +[@@expect_failure] +```pulse +ghost +fn bind_fstar_gtot (r:GR.ref nat) (#n:G.erased nat) + requires GR.pts_to r full_perm n + ensures GR.pts_to r full_perm (n+1) +{ + let nn = fstar_gtot_incr n; + gwrite r nn +} +``` + +(* same issue as above *) +[@@expect_failure] +```pulse +ghost +fn return_fstar_gtot (#n:G.erased nat) + requires emp + ensures emp +{ + fstar_gtot_incr n +} +``` diff --git a/share/steel/examples/pulse/by-example/PulseByExample.fst b/share/steel/examples/pulse/by-example/PulseByExample.fst index c72aada8d..a32488522 100644 --- a/share/steel/examples/pulse/by-example/PulseByExample.fst +++ b/share/steel/examples/pulse/by-example/PulseByExample.fst @@ -104,7 +104,12 @@ fn invoke (r:ref nat) - +(* +to cover +- ref alloc/free +- local references +- earlier, explicitly introduce erased/exists/forall in spec +*) ```pulse @@ -172,6 +177,24 @@ fn write_array (#t:Type0) ``` (* -- loop invariants -- magic wand! + + +- loop invariants (while), other control flow (if, match) +- then, a program that brings everything up to this point together + - maybe fibo with primitive types then introduce bounded integers + +- arrays + +- some more mature example (e.g. sorting alg) + +- some simple record data structure along with a library of functions on this DS + (e.g. library of functions on 2D points) + +- build up to explaining the pulse implementation of lpht? -- emphasis on connecting + pure implementation to imperative code +- pulse linked list? -- more traditional sep logic example + +- concurrency, e.g. par incr of a ctr + + *) \ No newline at end of file