Fix issue 583.

Author: gebner

lib/pulse/lib/Pulse.Lib.Array.fst

@@ -18,6 +18,7 @@ module Pulse.Lib.Array
 #lang-pulse
 open Pulse.Lib.Core
 open Pulse.Lib.Reference
+open Pulse.Lib.WithPure
 open Pulse.Lib.Array.Basic
 open Pulse.Class.PtsTo
 open FStar.Ghost

lib/pulse/lib/Pulse.Lib.Pervasives.fst

@@ -21,6 +21,7 @@ include Pulse.Lib.Core
 include Pulse.Lib.Inv
 include Pulse.Lib.Send
 include Pulse.Lib.Forall
+include Pulse.Lib.WithPure
 include Pulse.Lib.Array
 include Pulse.Lib.Reference
 include Pulse.Lib.Reference.Array

src/checker/Pulse.Checker.While.fst

@@ -63,7 +63,9 @@ let rec subst_loop_requires_marker (t: term) (v: term -> term) : Dv term =
     | _ -> default ()
   )
   | R.Tv_Abs b body ->
-    R.pack_ln (R.Tv_Abs b (subst_loop_requires_marker body v))
+    let b = R.inspect_binder b in
+    let b = { b with sort = subst_loop_requires_marker b.sort v } in
+    R.pack_ln (R.Tv_Abs (R.pack_binder b) (subst_loop_requires_marker body v))
   | _ -> t
 
 let subst_loop_requires_marker_with_true t = subst_loop_requires_marker t fun _ -> tm_l_true

src/checker/Pulse.JoinComp.fst

@@ -43,15 +43,8 @@ let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop)
       tm_exists_sl u b (close_term post y)
     )
   in
-  (* generate exists (_:squash pr). post 
-     Useful if the well-formedness of post depends on pr in scope *)
-  let guard_with_squash pr (post:slprop) : T.Tac slprop =
-    let n, u, pr = pr in
-    let b = {binder_ty=mk_squash u pr; binder_ppname=n; binder_attrs=Sealed.seal []} in
-    tm_exists_sl u_zero b post
-  in
   let maybe_elim_rewrites_to pr (post:term) : T.Tac term =
-    let _, _, property = pr in
+    let n, _, property = pr in
     let open R in
     let hd, args = T.collect_app_ln property in
     match T.inspect_ln hd, args with
@@ -62,15 +55,15 @@ let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop)
         | Tv_Var n1 ->
           let n1 = inspect_namedv n1 in
           if n1.uniq = x_ret then
-            tm_star post (tm_pure (RT.eq2 u typ lhs rhs))
+            tm_with_pure (RT.eq2 u typ lhs rhs) n post
           else
             Pulse.Syntax.Naming.subst_term post [RT.NT n1.uniq rhs]
         | _ -> 
           let eq = RT.eq2 u typ lhs rhs in
-          tm_star post (tm_pure eq)
+          tm_with_pure eq n post
       )
-      else tm_star post (tm_pure property) //guard_with_squash pr post?
-    | _ -> tm_star post (tm_pure property) //guard_with_squash pr post?
+      else tm_with_pure property n post
+    | _ -> tm_with_pure property n post
   in
   let close_post = close_post x_ret dom_g g1 in
   match bs1 with
@@ -257,7 +250,15 @@ and combine_args g b (args1 args2:list R.argv) : T.Tac (list R.argv) =
     (combine_terms true g b (a1, a2), v1)::combine_args g b args1 args2
   | _ -> []
 
-let join_slprop g b (ex1 ex2:list (universe & binder)) (p1 p2:slprop)
+let guard_with_pure then_ b (pred: term) n (acc: slprop) : slprop =
+  match inspect_term acc with
+  | Tm_IsUnreachable -> acc
+  | _ ->
+    tm_with_pure
+      (mk_imp (RT.eq2 u0 tm_bool b (if then_ then tm_true else tm_false)) pred)
+      n acc
+
+let rec join_slprop g b (ex1 ex2:list (universe & binder)) (p1 p2:slprop)
 : T.Tac slprop
 = match inspect_term p1, inspect_term p2 with
   | Tm_IsUnreachable, _ -> p2
@@ -270,6 +271,11 @@ let join_slprop g b (ex1 ex2:list (universe & binder)) (p1 p2:slprop)
     //Not doing anything interesting to share binders
     RT.mk_if b p1 p2
 
+  | Tm_WithPure pred1 n1 p1, _ ->
+    guard_with_pure true b pred1 n1 <| join_slprop g b ex1 ex1 p1 p2
+  | _, Tm_WithPure pred2 n2 p2 ->
+    guard_with_pure false b pred2 n2 <| join_slprop g b ex1 ex1 p1 p2
+
   | _ ->
     let open Pulse.Show in
     let p1s, p2s = slprop_as_list p1, slprop_as_list p2 in

test/bug-reports/Bug583.fst

@@ -0,0 +1,13 @@
+module Bug583
+open Pulse
+#lang-pulse
+
+fn problem () {
+  let mut i = 0sz;
+  let mut j = 1sz;
+  while ((!j `SizeT.sub` !i) <> 0sz)
+    invariant live i
+    invariant live j
+    invariant pure (!i `SizeT.lte` !j)
+  {}
+}

test/bug-reports/Bug583b.fst

@@ -0,0 +1,35 @@
+module Bug583b
+open Pulse
+#lang-pulse
+open Pulse.Lib.BoundedIntegers
+module SZ = FStar.SizeT
+module R  = Pulse.Lib.Reference
+
+fn binary_search_style_FAILS
+  (lo_init hi_init: SZ.t)
+  requires pure (SZ.v lo_init < SZ.v hi_init /\ SZ.v hi_init <= 100)
+  returns _: unit
+  ensures pure True
+{
+  let mut lo: SZ.t = lo_init;
+  let mut hi: SZ.t = hi_init;
+
+  while (
+    let vlo = !lo;
+    let vhi = !hi;
+    (vhi - vlo) > 1sz
+  )
+  invariant exists* vlo vhi.
+    R.pts_to lo vlo **
+    R.pts_to hi vhi **
+    pure (
+      SZ.v vlo <= SZ.v vhi /\
+      SZ.v vhi <= 100
+    )
+  {
+    let vlo = !lo;
+    let vhi = !hi;
+    let mid = vlo + ((vhi - vlo) / 2sz);
+    lo := mid
+  }
+}