Use --ext __unrefine everywhere

Pulse.fst.config.json

@@ -4,8 +4,8 @@
     "--query_cache",
     "--load_cmxs",
     "pulse",
-    "--ext",
-    "context_pruning"
+    "--ext", "__unrefine",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "lib/pulse",

lib/pulse/Pulse.fst.config.json

@@ -3,6 +3,7 @@
 	"options": [
 		"--query_cache",
 		"--load_cmxs", "pulse",
+		"--ext", "__unrefine",
 		"--ext", "context_pruning"
 	],
 	"include_dirs": [

lib/pulse/c/Pulse.C.Types.Scalar.fsti

@@ -134,7 +134,7 @@ let read_prf
     p' == p
   ))
 = 
-  let prf v0' p' : Lemma
+  let prf v0' (p':perm) : Lemma
     (requires (mk_fraction (scalar t) (mk_scalar v0') p' == mk_fraction (scalar t) (mk_scalar v0) p))
     (ensures (v0' == Ghost.reveal v0 /\ p' == Ghost.reveal p))
   = mk_scalar_inj (Ghost.reveal v0) v0' p p'

lib/pulse/core/Pulse.fst.config.json

@@ -2,8 +2,8 @@
 	"fstar_exe": "fstar.exe",
 	"options": [
 		"--query_cache",
-		"--ext",
-		"context_pruning"
+		"--ext", "__unrefine",
+		"--ext", "context_pruning"
 	],
 	"include_dirs": [
 	]

lib/pulse/core/PulseCore.HeapExtension.fst

@@ -1897,7 +1897,7 @@ let distinct_invariants_have_distinct_names
 let invariant_name_identifies_invariant
       (#h:heap_sig u#a)
       (e:inames (extend h))
-      (p q:ext_slprop h)
+      (p q:(extend h).slprop)
       (i:iiref h)
       (j:iiref h{ i == j } )
 : ghost_action_except (extend h)

lib/pulse/core/PulseCore.MemoryAlt.fst

@@ -617,7 +617,7 @@ let distinct_invariants_have_distinct_names_alt
       (q:slprop u#m { p =!= q })
       (i j:iref)
 : pst_ghost_action_except u#0 u#m 
-    (squash (~(eq2 #(E.iiref sig_1) (reveal_iref i) (reveal_iref j))))
+    (squash (reveal_iref i =!= reveal_iref j))
     e 
     (inv i p `star` inv j q)
     (fun _ -> inv i p `star` inv j q)
@@ -640,7 +640,7 @@ let distinct_invariants_have_distinct_names
       (q:slprop u#m { p =!= q })
       (i j:iref)
 : pst_ghost_action_except u#0 u#m 
-    (squash (~(eq2 #iref i j)))
+    (squash (i =!= j))
     e 
     (inv i p `star` inv j q)
     (fun _ -> inv i p `star` inv j q)

lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst

@@ -172,7 +172,8 @@ let repr_t_sz kt vt sz = r:repr_t kt vt { r.sz == sz}
 let lemma_clean_upd_lookup_walk #kt #vt #sz
       (spec1 spec2 : spec_t kt vt) 
       (repr1 repr2 : repr_t_sz kt vt sz)
-      idx k v (k':_{k =!= k'})
+      (idx : nat{idx < repr1.sz})
+       k v (k':_{k =!= k'})
   : Lemma (requires
       repr_related repr1 repr2 
       /\ (forall i. i < repr1.sz /\ i <> idx ==> repr1 @@ i == repr2 @@ i)
@@ -206,7 +207,8 @@ let lemma_clean_upd_lookup_walk #kt #vt #sz
 let lemma_used_upd_lookup_walk #kt #vt #sz
       (spec1 spec2 : spec_t kt vt)
       (repr1 repr2 : repr_t_sz kt vt sz)
-      idx k (k':_{k =!= k'})
+      (idx : nat{idx < repr1.sz})
+      k (k':_{k =!= k'})
       (v v' : vt)
   : Lemma (requires
          repr_related repr1 repr2
@@ -244,7 +246,8 @@ let lemma_used_upd_lookup_walk #kt #vt #sz
 let lemma_del_lookup_walk #kt #vt #sz 
       (spec1 spec2 : spec_t kt vt)
       (repr1 repr2 : repr_t_sz kt vt sz)
-      upos k v (k':_{k =!= k'})
+      (upos : nat{upos < repr1.sz})
+      k v (k':_{k =!= k'})
   : Lemma (requires
       repr_related repr1 repr2 /\
       (forall i. i < sz /\ i <> upos ==> repr1 @@ i == repr2 @@ i) /\
@@ -278,7 +281,8 @@ let lemma_del_lookup_walk #kt #vt #sz
 let lemma_zombie_upd_lookup_walk #kt #vt #sz
       (spec spec' : spec_t kt vt)
       (repr repr' : repr_t_sz kt vt sz)
-      idx k v (k':_{k =!= k'})
+      (idx : nat{idx < repr.sz})
+      k v (k':_{k =!= k'})
   : Lemma (requires
       repr_related repr repr'
       /\ (forall i. i < sz /\ i <> idx ==> repr @@ i == repr' @@ i)

lib/pulse/lib/Pulse.Lib.HigherArray.fst

@@ -538,7 +538,7 @@ fn pts_to_range_prop'
   (#s: Seq.seq elt)
 requires pts_to_range a i j #p s
 ensures pts_to_range a i j #p s ** pure (
-      (i <= j /\ j <= length a /\ Seq.length s == j - i)
+      (i <= j /\ j <= length a /\ eq2 #nat (Seq.length s) (j - i))
     )
 {
   unfold pts_to_range a i j #p s;
@@ -550,7 +550,6 @@ ensures pts_to_range a i j #p s ** pure (
 
 let pts_to_range_prop = pts_to_range_prop'
 
-
 ghost
 fn pts_to_range_intro'
   (#elt: Type)

share/pulse/Makefile.include-base

@@ -19,7 +19,7 @@ else
 USE_HINTS:=
 endif
 
-FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning
+FSTAR_OPTIONS += $(USE_HINTS) --ext context_pruning --ext __unrefine
 
 # A place to put all build artifacts
 ifneq (,$(OUTPUT_DIRECTORY))

share/pulse/examples/Pulse.fst.config.json

@@ -8,8 +8,8 @@
     "_output/cache",
     "--warn_error", 
     "-249",
-    "--ext",
-    "context_pruning"
+    "--ext", "__unrefine",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
     "../../../lib/pulse",

src/checker/Pulse.Checker.Prover.Match.Matchers.fst

@@ -289,7 +289,7 @@ let head_is_uvar (uvs:env) (t:term) : T.Tac bool =
   let hd, _ = T.collect_app t in
   match T.inspect hd with
   | T.Tv_Var v ->
-    List.existsb (fun (x, _) -> x = v.uniq) (bindings uvs)
+    List.existsb (fun (x, _) -> (x <: var) = v.uniq) (bindings uvs)
   | _ -> false
 
 (**************** The actual matchers *)

src/checker/Pulse.Typing.Env.fst

@@ -158,7 +158,7 @@ let rec remove_binding_aux (g:env)
     let m = Map.restrict (Set.complement (Set.singleton x)) (Map.upd g.m x tm_unknown) in
     // we need uniqueness invariant in the representation
     assume (forall (b:var & typ). List.Tot.memP b prefix <==> (List.Tot.memP b g.bs /\
-                                                               fst b =!= x));
+                                                               fst b =!= (x <: var)));
     let g' = {g with bs = prefix; names=prefix_names; m} in
     assert (equal g (push_env (push_binding (mk_env (fstar_env g)) x ppname_default t) g'));
     x, t, g'

src/checker/PulseChecker.fst.config.json

@@ -2,8 +2,8 @@
   "fstar_exe": "fstar.exe",
   "options": [
     "--query_cache",
-    "--ext",
-    "context_pruning"
+    "--ext", "__unrefine",
+    "--ext", "context_pruning"
   ],
   "include_dirs": [
   ]