From 85ffa5a8e2c9877b85ed0343f6044cd49837247c Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Wed, 1 Oct 2025 14:48:54 -0700 Subject: [PATCH] fixing Steel to work with F* smt universes --- Makefile | 2 +- Steel.fst.config.json | 5 ++- lib/steel/Steel.Effect.Common.fst | 4 +- lib/steel/Steel.Heap.fst | 27 +++++++------ lib/steel/Steel.Memory.fst | 47 ++++++++++++---------- lib/steel/Steel.Reference.fst | 32 +++++++-------- lib/steel/Steel.ST.HigherArray.fsti | 9 +++-- lib/steel/Steel.ST.Util.fst | 2 +- lib/steel/Steel.Semantics.Instantiate.fst | 22 +++++----- lib/steel/Steel.Semantics.Instantiate.fsti | 10 ++--- share/steel/examples/steel/Duplex.PCM.fst | 6 +-- share/steel/examples/steel/ParDiv.fst | 12 +++--- share/steel/examples/steel/Queue.fst | 4 +- 13 files changed, 96 insertions(+), 86 deletions(-) diff --git a/Makefile b/Makefile index 902c50bcf..49912ba7e 100644 --- a/Makefile +++ b/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 diff --git a/Steel.fst.config.json b/Steel.fst.config.json index f729f8ab8..c5d8c21f8 100644 --- a/Steel.fst.config.json +++ b/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", diff --git a/lib/steel/Steel.Effect.Common.fst b/lib/steel/Steel.Effect.Common.fst index 0551545de..551aab844 100644 --- a/lib/steel/Steel.Effect.Common.fst +++ b/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 diff --git a/lib/steel/Steel.Heap.fst b/lib/steel/Steel.Heap.fst index 51f1b244e..9edbf84ae 100644 --- a/lib/steel/Steel.Heap.fst +++ b/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 diff --git a/lib/steel/Steel.Memory.fst b/lib/steel/Steel.Memory.fst index 26f0bbb6f..01a138e16 100644 --- a/lib/steel/Steel.Memory.fst +++ b/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)) diff --git a/lib/steel/Steel.Reference.fst b/lib/steel/Steel.Reference.fst index ebe35b0cf..117566a87 100644 --- a/lib/steel/Steel.Reference.fst +++ b/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 diff --git a/lib/steel/Steel.ST.HigherArray.fsti b/lib/steel/Steel.ST.HigherArray.fsti index c2b386177..6433da1ab 100644 --- a/lib/steel/Steel.ST.HigherArray.fsti +++ 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 diff --git a/lib/steel/Steel.ST.Util.fst b/lib/steel/Steel.ST.Util.fst index 7bc2d4c62..cb54ab69d 100644 --- a/lib/steel/Steel.ST.Util.fst +++ b/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) diff --git a/lib/steel/Steel.Semantics.Instantiate.fst b/lib/steel/Steel.Semantics.Instantiate.fst index ba078d2e5..c747477b7 100644 --- a/lib/steel/Steel.Semantics.Instantiate.fst +++ b/lib/steel/Steel.Semantics.Instantiate.fst @@ -19,8 +19,8 @@ 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 @@ -28,17 +28,17 @@ let is_unit () #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) diff --git a/lib/steel/Steel.Semantics.Instantiate.fsti b/lib/steel/Steel.Semantics.Instantiate.fsti index dd2201225..f25498d82 100644 --- a/lib/steel/Steel.Semantics.Instantiate.fsti +++ b/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)) \ No newline at end of file diff --git a/share/steel/examples/steel/Duplex.PCM.fst b/share/steel/examples/steel/Duplex.PCM.fst index 15d3af9fd..dfa95ca29 100644 --- a/share/steel/examples/steel/Duplex.PCM.fst +++ b/share/steel/examples/steel/Duplex.PCM.fst @@ -641,7 +641,7 @@ let upd_gen_action #p r x y f = rewrite_slprop (pts_to r (reveal (hide y))) (pts_to r y) (fun _ -> ()) -#push-options "--z3rlimit_factor 8 --ifuel 2 --fuel 1 --split_queries no" +#push-options "--z3rlimit_factor 8 --ifuel 2 --fuel 1 --split_queries no --retry 3" #restart-solver let write_a_f_aux @@ -715,7 +715,7 @@ let write_a_f_aux res #pop-options -#push-options "--z3rlimit_factor 8 --ifuel 2 --fuel 1 --split_queries no" +#push-options "--z3rlimit_factor 8 --ifuel 2 --fuel 1 --split_queries no --retry 3" #restart-solver let write_b_f_aux (#p:dprot) @@ -745,7 +745,7 @@ let write_b_f_aux assert (composable post (A_W (step next x) (extend tr x))); assert (compose (A_W (step next x) (extend tr x)) post == res) ) else if is_recv (step next x) then ( - assert (composable post (A_R next tr)); + assert_spinoff (composable post (A_R next tr)); assert (compose (A_R next tr) post == res) ) else ( assert (is_fin (step next x)); diff --git a/share/steel/examples/steel/ParDiv.fst b/share/steel/examples/steel/ParDiv.fst index ddc1032a2..89f59850a 100644 --- a/share/steel/examples/steel/ParDiv.fst +++ b/share/steel/examples/steel/ParDiv.fst @@ -72,7 +72,7 @@ let post #s a (c:comm_monoid s) = a -> c.r * Also see: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/views.pdf *) noeq -type action #s (c:comm_monoid s) (a:Type) = { +type action (#s:Type u#s) (c:comm_monoid u#s u#s s) (a:Type) = { pre: c.r; post: a -> c.r; sem: (frame:c.r -> @@ -209,7 +209,7 @@ let rec run #s #c (i:nat) #pre #a #post (f:m s c a pre post) (state:s) * - Note, we'll probably have to add a thunk to make it work with * the current implementation but that's a detail *) -let eff #s (#c:comm_monoid s) a (pre:c.r) (post: a -> c.r) = +let eff (#s:Type u#1) (#c:comm_monoid s) a (pre:c.r) (post: a -> c.r) = m s c a pre post /// eff is a monad: we give a return and bind for it, though we don't @@ -259,7 +259,7 @@ let par #s (#c:comm_monoid s) assume val heap : Type u#1 /// Assume some monoid of heap assertions -assume val hm : comm_monoid heap +assume val hm : comm_monoid u#1 u#1 heap /// For this demo, we'll also assume that this assertions are affine /// i.e., it's ok to forget some properties of the heap @@ -296,9 +296,9 @@ assume val upd_ok (x:ref 'a) (v:'a) (h:heap) (frame:hm.r) hm.interp (pts_to x v `hm.star` frame) h')) /// Here's a sample action for dereference -let (!) (x:ref 'a) - : eff 'a (ptr_live x) (pts_to x) - = let act : action hm 'a = +let (!) (#a:Type) (x:ref a) + : eff a (ptr_live x) (pts_to x) + = let act : action hm a = { pre = ptr_live x; post = pts_to x; diff --git a/share/steel/examples/steel/Queue.fst b/share/steel/examples/steel/Queue.fst index bdb11ba74..4d0de982a 100644 --- a/share/steel/examples/steel/Queue.fst +++ b/share/steel/examples/steel/Queue.fst @@ -42,8 +42,8 @@ let emp_equiv_pure (requires p) (ensures (emp `equiv` pure p)) = reveal_emp (); - Classical.forall_intro intro_emp; - Classical.forall_intro (pure_interp p) + Classical.forall_intro (intro_emp u#1); + Classical.forall_intro (pure_interp u#1 p) let rec next_last (#a: Type)