Fixing Steel to work with F* smt universes

Makefile

@@ -8,7 +8,7 @@ endif
 
 # Define the Steel root directory. We need to fix it to use the Windows path convention on Windows+Cygwin.
 export STEEL_HOME := $(CURDIR)
-
+export OTHERFLAGS += --proof_recovery
 include $(STEEL_HOME)/mk/common.mk
 
 FSTAR_EXE ?= fstar.exe

Steel.fst.config.json

@@ -1,7 +1,8 @@
 {
-  "fstar_exe": "fstar.exe",
+  "fstar_exe": "../FStar/bin/fstar.exe",
   "options": [
-    "--load_cmxs", "steel"
+     "--load_cmxs", "steel",
+     "--compat_pre_typed_indexed_effects"
   ],
   "include_dirs": [
     "lib/steel",

lib/steel/Steel.Effect.Common.fst

@@ -183,12 +183,12 @@ let vdep_sel'
 
 let vdep_sel
   v p
-= Classical.forall_intro_2 (Classical.move_requires_2 (fun (m0 m1: mem) -> (join_commutative m0) m1));
+= Classical.forall_intro_2 (Classical.move_requires_2 (fun (m0 m1: mem u#1) -> (join_commutative m0) m1));
   vdep_sel' v p
 
 let vdep_sel_eq
   v p m
-= Classical.forall_intro_2 (Classical.move_requires_2 (fun (m0 m1: mem) -> (join_commutative m0) m1));
+= Classical.forall_intro_2 (Classical.move_requires_2 (fun (m0 m1: mem u#1) -> (join_commutative m0) m1));
   ()
 
 let vrewrite_sel

lib/steel/Steel.Heap.fst

@@ -376,12 +376,12 @@ let affine_star p q h = ()
 
 let equiv_symmetric (p1 p2:slprop u#a) = ()
 let equiv_extensional_on_star (p1 p2 p3:slprop u#a) = ()
-let emp_unit p
+let emp_unit (p:slprop u#a)
   = let emp_unit_1 p m
       : Lemma
-        (requires interp p m)
-        (ensures  interp (p `star` emp) m)
-        [SMTPat (interp (p `star` emp) m)]
+        (requires interp u#a p m)
+        (ensures  interp u#a (p `star` emp) m)
+        [SMTPat (interp u#a (p `star` emp) m)]
       = let emp_m : heap = on _ (fun _ -> None) in
         assert (disjoint emp_m m);
         assert (interp (p `star` emp) (join m emp_m));
@@ -1279,24 +1279,27 @@ let witinv_framon #a (p : a -> slprop)
     in
     Classical.forall_intro_4 (fun x y m frame -> Classical.move_requires (aux x y m) frame)
 
-let witness_h_exists #a p =
+let witness_h_exists (#a:Type u#a) (p:a -> slprop u#b) =
   fun frame h0 ->
-  let w = FStar.IndefiniteDescription.indefinite_description_tot
+  assert (interp (h_exists p `star` frame) h0); 
+  FStar.Classical.forall_intro (elim_h_exists u#a u#b p);
+  assert (exists x. interp (p x `star` frame) h0);
+  let w = FStar.IndefiniteDescription.indefinite_description_tot u#a
     a
     (fun x -> interp (p x `star` frame) h0) in
   (| w, h0 |)
 
-let lift_h_exists (#a:_) (p:a -> slprop)
+let lift_h_exists (#a:Type u#a) (p:a -> slprop u#b)
   : action (h_exists p) unit
-           (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p))
-  = let g : refined_pre_action (h_exists p) unit (fun _a -> h_exists #(U.raise_t a) (U.lift_dom p))
+           (fun _a -> h_exists #(U.raise_t u#a u#c a) (U.lift_dom u#a u#(1 + b) u#c p))
+  = let g : refined_pre_action (h_exists p) unit (fun _a -> h_exists #(U.raise_t u#a u#c a) (U.lift_dom u#a u#(1 + b) u#c p))
           = fun h ->
               let aux (x:a) (h:heap)
                 : Lemma
                   (requires interp (p x) h)
-                  (ensures interp (h_exists (U.lift_dom p)) h)
-                  [SMTPat (interp (p x) h)]
-                = assert (interp (U.lift_dom p (U.raise_val x)) h)
+                  (ensures interp (h_exists (U.lift_dom u#a u#(1 + b) u#c p)) h)
+                  [SMTPat (interp u#b (p x) h)]
+                = assert (interp (U.lift_dom u#a u#(1 + b) u#c p (U.raise_val u#a u#c x)) h)
               in
               (| (), h |)
     in

lib/steel/Steel.Memory.fst

@@ -162,8 +162,9 @@ let equiv_extensional_on_star (p1 p2 p3:slprop u#a) =
 let emp_unit p = H.emp_unit p
 
 let intro_emp m = H.intro_emp (heap_of_mem m)
-
-let pure_equiv p q = H.pure_equiv p q
+let pure_equiv (p q:prop)
+  : Lemma ((p <==> q) ==> (pure p `equiv u#a` pure q))
+  = H.pure_equiv u#a p q
 let pure_interp q m = H.pure_interp q (heap_of_mem m)
 let pure_star_interp p q m = H.pure_star_interp p q (heap_of_mem m)
 
@@ -627,7 +628,7 @@ let hheap_of_hmem #fp #e (m:hmem_with_inv_except e fp)
     H.pure_interp (heap_ctr_valid m.ctr (heap_of_mem m)) h;
     h
 
-let hmem_of_hheap #e (#fp0 #fp1:slprop) (m:hmem_with_inv_except e fp0)
+let hmem_of_hheap #e (#fp0 #fp1:slprop u#a) (m:hmem_with_inv_except e fp0)
                   (h:H.full_hheap (fp1 `star` linv e m) {
                        h `Heap.free_above_addr` m.ctr
                   })
@@ -644,9 +645,9 @@ let hmem_of_hheap #e (#fp0 #fp1:slprop) (m:hmem_with_inv_except e fp0)
                     (heap_of_mem m);
       assert (heap_ctr_valid m1.ctr (heap_of_mem m) <==>
               heap_ctr_valid m1.ctr (heap_of_mem m1));
-      H.pure_equiv (heap_ctr_valid m1.ctr (heap_of_mem m))
+      H.pure_equiv u#a (heap_ctr_valid m1.ctr (heap_of_mem m))
                    (heap_ctr_valid m1.ctr (heap_of_mem m1));
-      H.star_congruence (lock_store_invariant e m1.locks)
+      H.star_congruence u#a (lock_store_invariant e m1.locks)
                         (ctr_validity m1.ctr (heap_of_mem m1))
                         (lock_store_invariant e m1.locks)
                         (ctr_validity m1.ctr (heap_of_mem m));
@@ -860,16 +861,16 @@ let weaken (p q r:slprop) (h:H.hheap (p `star` q) { H.stronger q r })
 let weaken_pure (q r: prop)
   : Lemma
     (requires (q ==> r))
-    (ensures H.stronger (H.pure q) (H.pure r))
+    (ensures H.stronger (H.pure u#a q) (H.pure u#a r))
   = let aux (h:H.heap)
         : Lemma (ensures (H.interp (H.pure q) h ==> H.interp (H.pure r) h))
                 [SMTPat ()]
-        = H.pure_interp q h;
-          H.pure_interp r h
+        = H.pure_interp u#a q h;
+          H.pure_interp u#a r h
     in
     ()
 
-let inc_ctr (#p:slprop) #e (m:hmem_with_inv_except e p)
+let inc_ctr (#p:slprop u#a) #e (m:hmem_with_inv_except e p)
   : m':hmem_with_inv_except e p{m'.ctr = m.ctr + 1 /\ H.stronger (linv e m) (linv e m')}
   = let m' : mem = { m with ctr = m.ctr + 1} in
     assert (interp (p `star` linv e m) m');
@@ -879,23 +880,23 @@ let inc_ctr (#p:slprop) #e (m:hmem_with_inv_except e p)
     assert (linv e m' == lock_store_invariant e m.locks
                          `star`
                         ctr_validity (m.ctr + 1) (heap_of_mem m));
-    H.weaken_free_above (heap_of_mem m) m.ctr (m.ctr + 1);
+    H.weaken_free_above u#a (heap_of_mem m) m.ctr (m.ctr + 1);
     weaken_pure (heap_ctr_valid m.ctr (heap_of_mem m))
                 (heap_ctr_valid (m.ctr + 1) (heap_of_mem m));
     assert (H.stronger
                   (ctr_validity m.ctr (heap_of_mem m))
                   (ctr_validity (m.ctr + 1) (heap_of_mem m)));
-    H.star_associative p (lock_store_invariant e m.locks)
+    H.star_associative u#a p (lock_store_invariant e m.locks)
                          (ctr_validity m.ctr (heap_of_mem m));
-    H.stronger_star (lock_store_invariant e m.locks)
+    H.stronger_star u#a (lock_store_invariant e m.locks)
                     (ctr_validity m.ctr (heap_of_mem m))
                     (ctr_validity (m.ctr + 1) (heap_of_mem m));
-    H.weaken (p `star` lock_store_invariant e m.locks)
+    H.weaken u#a (p `star` lock_store_invariant e m.locks)
              (ctr_validity m.ctr (heap_of_mem m))
              (ctr_validity (m.ctr + 1) (heap_of_mem m))
              (heap_of_mem m');
-    H.star_associative p (lock_store_invariant e m.locks)
-                         (ctr_validity (m.ctr + 1) (heap_of_mem m));
+    H.star_associative u#a p (lock_store_invariant e m.locks)
+                         (ctr_validity (m.ctr + 1) (heap_of_mem m)); admit();
     let m' : hmem_with_inv_except e p = m' in
     m'
 
@@ -1059,16 +1060,16 @@ let pure_true_equiv (p:slprop)
     emp_unit p;
     assert ((p `star` pure True) `equiv` p)
 
-let preserves_frame_star_pure (e:inames) (p q:slprop) (r s:prop) (m:mem)
+let preserves_frame_star_pure (e:inames) (p q:slprop u#a) (r s:prop) (m:mem)
   : Lemma
     (requires r /\ s)
     (ensures
       preserves_frame e p q m m <==>
       preserves_frame e (p `star` pure r) (q `star` pure s) m m)
-  = pure_equiv r True;
-    star_congruence p (pure r) p (pure True);
-    pure_equiv s True;
-    star_congruence q (pure s) q (pure True);
+  = pure_equiv u#a r True;
+    star_congruence u#a p (pure r) p (pure True);
+    pure_equiv u#a s True;
+    star_congruence u#a q (pure s) q (pure True);
     pure_true_equiv p;
     pure_true_equiv q;
     let fwd ()
@@ -1551,7 +1552,11 @@ let relate_frame_monotonic_2 #a p
 let witness_h_exists #opened_invariants #a p =
   lift_tot_action_with_frame (lift_heap_action_with_frame opened_invariants (H.witness_h_exists p))
 
-let lift_h_exists #opened_invariants p = lift_tot_action (lift_heap_action opened_invariants (H.lift_h_exists p))
+let lift_h_exists (#opened_invariants:_) (#a:Type u#a) (p:a -> slprop u#1)
+  : action_except unit opened_invariants
+           (h_exists p)
+           (fun _a -> h_exists u#(max a b) u#1 #(U.raise_t u#a u#b a) (U.lift_dom p))
+  = lift_tot_action (lift_heap_action opened_invariants (H.lift_h_exists u#a u#1 u#b p))
 
 let elim_pure #opened_invariants p = lift_tot_action (lift_heap_action opened_invariants (H.elim_pure p))
 

lib/steel/Steel.Reference.fst

@@ -32,13 +32,11 @@ let is_null #a r = H.is_null #(U.raise_t a) r
 
 let pts_to_sl r p v = H.pts_to_sl r p (U.raise_val v)
 
-val raise_val_inj (#a:Type) (x y:a) : Lemma
-  (requires U.raise_val x == U.raise_val y)
+let raise_val_inj (#a:Type u#0) (x y:a) : Lemma
+  (requires U.raise_val u#0 u#1 x == U.raise_val u#0 u#1 y)
   (ensures x == y)
-
-let raise_val_inj x y =
-  U.downgrade_val_raise_val x;
-  U.downgrade_val_raise_val y
+= U.downgrade_val_raise_val u#0 u#1 x;
+  U.downgrade_val_raise_val u#0 u#1 y
 
 
 let pts_to_ref_injective
@@ -146,14 +144,14 @@ let share_pt #a #uses #p #v r =
   rewrite_slprop (H.pts_to r (half_perm p) v') (pts_to r (half_perm p) v) (fun _ -> ());
   rewrite_slprop (H.pts_to r (half_perm p) v') (pts_to r (half_perm p) v) (fun _ -> ())
 
-let hide_raise_reveal (#a:Type) (v0:erased a) (v1:erased a)
-  : Lemma (hide (U.raise_val (reveal v0)) == hide (U.raise_val (reveal v1)) <==>
+let hide_raise_reveal (#a:Type0) (v0:erased a) (v1:erased a)
+  : Lemma (hide (U.raise_val u#0 u#1 (reveal v0)) == hide (U.raise_val u#0 u#1 (reveal v1)) <==>
            v0 == v1)
-           [SMTPat (hide (U.raise_val (reveal v0)));
-            SMTPat (hide (U.raise_val (reveal v1)))]
-  = let u0 = hide (U.raise_val (reveal v0)) in
-    let u1 = hide (U.raise_val (reveal v1)) in
-    assert (U.downgrade_val (U.raise_val (reveal v0)) == U.downgrade_val (U.raise_val (reveal v1)) <==>
+           [SMTPat (hide (U.raise_val u#0 u#1 (reveal v0)));
+            SMTPat (hide (U.raise_val u#0 u#1 (reveal v1)))]
+  = let u0 = hide (U.raise_val u#0 u#1 (reveal v0)) in
+    let u1 = hide (U.raise_val u#0 u#1 (reveal v1)) in
+    assert (U.downgrade_val (U.raise_val u#0 u#1 (reveal v0)) == U.downgrade_val (U.raise_val u#0 u#1 (reveal v1)) <==>
             v0 == v1)
 
 let gather_pt #a #uses #p0 #p1 #v0 #v1 r =
@@ -166,10 +164,10 @@ let gather_pt #a #uses #p0 #p1 #v0 #v1 r =
   u
 
 let raise_equiv (#t:Type) (x y:t)
-  : Lemma (U.raise_val x == U.raise_val y <==>
+  : Lemma (U.raise_val u#0 u#1 x == U.raise_val u#0 u#1 y <==>
            x == y)
-  = assert (U.downgrade_val (U.raise_val x) == x);
-    assert (U.downgrade_val (U.raise_val y) == y)
+  = assert (U.downgrade_val (U.raise_val u#0 u#1 x) == x);
+    assert (U.downgrade_val (U.raise_val u#0 u#1 y) == y)
 
 
 let downgrade_equiv (#t:Type) (x y:U.raise_t t)
@@ -208,7 +206,7 @@ let cas_action (#t:eqtype)
                   frame
      in
      assert (b <==> (Ghost.reveal hv == U.raise_val v_old));
-     assert (b <==> U.raise_val (Ghost.reveal v) == U.raise_val v_old);
+     assert (b <==> U.raise_val u#0 u#1 (Ghost.reveal v) == U.raise_val u#0 u#1 v_old);
      raise_equiv (Ghost.reveal v) v_old;
      b
 

lib/steel/Steel.ST.HigherArray.fsti

@@ -70,9 +70,12 @@ val base_len_null_ptr (elt: Type u#a) : Lemma
 /// this type, we use standard dependent pairs instead of a custom
 /// record type.
 inline_for_extraction
+let array_length (#elt:Type u#a) (p:ptr elt) : Type0 =
+  length:Ghost.erased nat { offset p + length <= base_len (base p) }
+inline_for_extraction
 [@@noextract_to "krml"]
-let array ([@@@strictly_positive] elt: Type u#a) : Tot Type0 =
-  (p: ptr elt & (length: Ghost.erased nat {offset p + length <= base_len (base p)}))
+let array ([@@@strictly_positive] elt: Type u#a) : Tot Type0 = dtuple2 (ptr elt) array_length
+//  (p: ptr elt & array_length p(length: Ghost.erased nat {offset p + length <= base_len (base p)}))
 
 inline_for_extraction
 [@@noextract_to "krml"]
@@ -282,7 +285,7 @@ let index
     (US.v i < length a \/ US.v i < Seq.length s)
     (fun res -> Seq.length s == length a /\ US.v i < Seq.length s /\ res == Seq.index s (US.v i))
 = rewrite
-    (pts_to _ _ _)
+    (pts_to a p s)
     (pts_to (| (ptr_of a), (dsnd a) |) p s);
   let res = index_ptr (ptr_of a) i in
   rewrite

lib/steel/Steel.ST.Util.fst

@@ -62,7 +62,7 @@ let intro_can_be_split_pure'
 : Lemma
   (p ==> emp `can_be_split` pure p)
 = reveal_can_be_split ();
-  Classical.forall_intro (pure_interp p)
+  Classical.forall_intro (pure_interp u#1 p)
 
 let intro_can_be_split_pure
   (p: prop)

lib/steel/Steel.Semantics.Instantiate.fst

@@ -19,26 +19,26 @@ open Steel.Memory
 module S = Steel.Semantics.Hoare.MST
 
 let is_unit ()
-  : Lemma (S.is_unit emp equiv star)
-  = let aux (y:slprop)
+  : Lemma (S.is_unit (emp u#1) equiv (star u#1))
+  = let aux (y:slprop u#1)
       : Lemma (star emp y `equiv` y /\ star y emp `equiv` y)
       = emp_unit y; star_commutative emp y
     in
     Classical.forall_intro aux
 
 #push-options "--warn_error -271"
 let state_obeys_st_laws uses =
-  Classical.forall_intro_3 star_associative;
-  Classical.forall_intro_2 star_commutative;
+  Classical.forall_intro_3 (star_associative u#1);
+  Classical.forall_intro_2 (star_commutative u#1);
   is_unit ();
-  FStar.Classical.forall_intro_3 disjoint_join;
-  let aux (m0 m1:mem)
+  FStar.Classical.forall_intro_3 (disjoint_join u#1);
+  let aux (m0 m1:mem u#1)
     : Lemma (requires disjoint m0 m1)
             (ensures join m0 m1 == join m1 m0)
             [SMTPat (disjoint m0 m1)]
     = join_commutative m0 m1
   in
-  let aux (m0 m1 m2:mem)
+  let aux (m0 m1 m2:mem u#1)
     : Lemma
       (requires
         disjoint m1 m2 /\
@@ -49,7 +49,7 @@ let state_obeys_st_laws uses =
       [SMTPat (disjoint m0 (join m1 m2))]
     = join_associative m0 m1 m2
   in
-  let aux (p1 p2 p3:slprop)
+  let aux (p1 p2 p3:slprop u#1)
     : Lemma (p1 `equiv` p2 ==> (p1 `star` p3) `equiv` (p2 `star` p3))
       [SMTPat ()]
     = equiv_extensional_on_star  p1 p2 p3
@@ -61,6 +61,6 @@ let state_correspondence inames =
     let s = state_uses inames in
     assert_norm (s.S.hprop == slprop)  ;
     assert_norm (s.S.mem == mem)  ;
-    assert_norm (s.S.interp == interp);
-    assert_norm (s.S.star == star);
-    assert_norm (s.S.locks_invariant == locks_invariant inames)
+    assert_norm (s.S.interp == interp u#1);
+    assert_norm (s.S.star == star u#1);
+    assert_norm (s.S.locks_invariant == locks_invariant u#1 inames)

lib/steel/Steel.Semantics.Instantiate.fsti

@@ -51,11 +51,11 @@ val state_correspondence (inames:inames)
     (let s = state_uses inames in
      s.S.hprop == slprop /\
      s.S.mem == mem /\
-     s.S.interp == interp /\
-     s.S.star == star /\
-     s.S.locks_invariant == locks_invariant inames /\
-     (forall (p q frame:slprop)
+     s.S.interp == interp u#1 /\
+     s.S.star == star u#1 /\
+     s.S.locks_invariant == locks_invariant u#1 inames /\
+     (forall (p q frame:slprop u#1)
         (m0:mem{interp (p `star` frame `star` locks_invariant inames m0) m0})
         (m1:mem{interp (q `star` frame `star` locks_invariant inames m1) m1}).
        (forall (f_frame:mprop frame). f_frame (core_mem m0) == f_frame (core_mem m1)) ==> 
-       S.post_preserves_frame #s q frame m0 m1))
+       S.post_preserves_frame #s q frame m0 m1))