bug-reports: strange failure invoking FStar GTot fn in Pulse

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
+}
+```

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
+
+
 *)