From f0b839148ecd6e0a006a6adddc83175e0f92045b Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 15 Jan 2025 10:49:14 -0800 Subject: [PATCH] Revert ulib changes. --- ulib/FStar.BigOps.fsti | 4 ++-- ulib/FStar.Fin.fst | 9 +++++---- ulib/FStar.HyperStack.ST.fsti | 4 ++-- ulib/FStar.IndefiniteDescription.fst | 2 +- ulib/FStar.Modifies.fst | 2 +- ulib/FStar.Modifies.fsti | 2 +- ulib/FStar.ModifiesGen.fst | 2 -- ulib/FStar.Monotonic.Seq.fst | 4 ++-- ulib/FStar.ReflexiveTransitiveClosure.fst | 2 +- ulib/FStar.SquashProperties.fst | 2 +- ulib/FStar.Tactics.BreakVC.fst | 2 +- ulib/FStar.Tactics.Effect.fsti | 4 ++-- ulib/LowStar.Literal.fsti | 2 +- ulib/LowStar.Monotonic.Buffer.fst | 2 +- ulib/LowStar.Monotonic.Buffer.fsti | 2 +- ulib/LowStar.PrefixFreezableBuffer.fsti | 4 ++-- ulib/Prims.fst | 4 ++-- ulib/legacy/FStar.Array.fsti | 2 +- ulib/legacy/FStar.Pointer.Base.fst | 4 ++-- 19 files changed, 29 insertions(+), 30 deletions(-) diff --git a/ulib/FStar.BigOps.fsti b/ulib/FStar.BigOps.fsti index d54da25749c..8abf004e7f7 100644 --- a/ulib/FStar.BigOps.fsti +++ b/ulib/FStar.BigOps.fsti @@ -174,7 +174,7 @@ let big_or #a (f: (a -> Type)) (l: list a) : prop = (** Mapping pairs of elements of [l] using [f] and combining them with [op]. *) [@@ __reduce__] -let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> GTot b)) (l: list a) (z: b) : GTot b = +let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> b)) (l: list a) (z: b) : GTot b = match l with | [] -> z | hd :: tl -> (map_op' op (f hd) tl z) `op` (pairwise_op' op f tl z) @@ -195,7 +195,7 @@ let anti_reflexive (#a: Type) (f: (a -> a -> Type)) = forall x. ~(f x x) {[ pairwise_and f [a; b; c] = f a b /\ f a c /\ f b c ]} *) [@@ __reduce__] -let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p /\ q) (fun x y -> f x y) l True +let pairwise_and' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_and f l True (** Equations for [pairwise_and] showing it to be a fold with [big_and] *) val pairwise_and'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_and' f [] == True) diff --git a/ulib/FStar.Fin.fst b/ulib/FStar.Fin.fst index 33640898625..306c781e04a 100644 --- a/ulib/FStar.Fin.fst +++ b/ulib/FStar.Fin.fst @@ -141,9 +141,9 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a) let index_of_first_pigeon = find_eq eq holes first_pigeon in //we carefully carve first_pigeon from (holes) let holes_except_first_pigeon = S.append (S.slice holes 0 (index_of_first_pigeon)) (S.slice holes (index_of_first_pigeon+1) (S.length holes)) in - introduce forall (x: items_of eq holes { not (eq x first_pigeon) }). contains_eq eq holes_except_first_pigeon x with - // all but first pigeon remain in reduced - (let index_of_x_in_holes = find_eq eq holes x in + let all_but_first_pigeon_remain_in_reduced (x: items_of eq holes { not (eq x first_pigeon) }) + : Lemma (contains_eq eq holes_except_first_pigeon x) + = let index_of_x_in_holes = find_eq eq holes x in reveal_opaque (`%contains_eq) (contains_eq eq); if index_of_x_in_holes < index_of_first_pigeon then assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon index_of_x_in_holes) @@ -152,7 +152,8 @@ let rec pigeonhole_eq (#a:Type) (eq: equivalence_relation a) Classical.move_requires (trans_lemma eq x (S.index holes index_of_x_in_holes)) first_pigeon; // append/slice smtpat hint assert (S.index holes index_of_x_in_holes == S.index holes_except_first_pigeon (index_of_x_in_holes-1)) - end); + end + in Classical.forall_intro all_but_first_pigeon_remain_in_reduced; let i1, i2 = pigeonhole_eq (eq) (holes_except_first_pigeon) (S.init #(items_of eq holes_except_first_pigeon) (S.length pigeons - 1) diff --git a/ulib/FStar.HyperStack.ST.fsti b/ulib/FStar.HyperStack.ST.fsti index 893f7186e0a..719a42de873 100644 --- a/ulib/FStar.HyperStack.ST.fsti +++ b/ulib/FStar.HyperStack.ST.fsti @@ -409,7 +409,7 @@ val rfree (#a:Type) (#rel:preorder a) (r:mreference a rel{HS.is_mm r /\ HS.is_he :ST unit (requires (fun m0 -> r `is_live_for_rw_in` m0)) (ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0)) -unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop = +unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) = m0 `contains` r /\ m1 == HyperStack.upd m0 r v (** @@ -420,7 +420,7 @@ val op_Colon_Equals (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) :STL unit (requires (fun m -> r `is_live_for_rw_in` m /\ rel (HS.sel m r) v)) (ensures (assign_post r v)) -unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop = +unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) = m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r (** diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst index 3bf86a914c3..0bad5da531f 100644 --- a/ulib/FStar.IndefiniteDescription.fst +++ b/ulib/FStar.IndefiniteDescription.fst @@ -64,4 +64,4 @@ let stronger_markovs_principle (p: (nat -> GTot bool)) boolean predicate *) let stronger_markovs_principle_prop (p: (nat -> GTot prop)) : Ghost nat (requires (~(forall (n: nat). ~(p n)))) (ensures (fun n -> p n)) = - indefinite_description_ghost _ (fun x -> p x) \ No newline at end of file + indefinite_description_ghost _ p \ No newline at end of file diff --git a/ulib/FStar.Modifies.fst b/ulib/FStar.Modifies.fst index f3a08375b0b..106a2910789 100644 --- a/ulib/FStar.Modifies.fst +++ b/ulib/FStar.Modifies.fst @@ -237,7 +237,7 @@ let loc_includes_region_union_l = MG.loc_includes_region_union_l let loc_includes_addresses_addresses = MG.loc_includes_addresses_addresses #_ cls -let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2 +let loc_disjoint = MG.loc_disjoint let loc_disjoint_sym = MG.loc_disjoint_sym diff --git a/ulib/FStar.Modifies.fsti b/ulib/FStar.Modifies.fsti index bb45dbc91a4..f4fab8c0f4c 100644 --- a/ulib/FStar.Modifies.fsti +++ b/ulib/FStar.Modifies.fsti @@ -238,7 +238,7 @@ val loc_includes_addresses_addresses val loc_disjoint (s1 s2: loc) -: Type0 +: GTot Type0 val loc_disjoint_sym (s1 s2: loc) diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst index dbbf9505fc4..412343c3c23 100644 --- a/ulib/FStar.ModifiesGen.fst +++ b/ulib/FStar.ModifiesGen.fst @@ -1184,7 +1184,6 @@ let loc_includes_loc_regions_restrict_to_regions (loc_includes (loc_regions false rs) (restrict_to_regions l rs)) = Classical.forall_intro (loc_aux_includes_refl #al #c) -#push-options "--z3rlimit_factor 2" let modifies_only_live_regions #al #c rs l h h' = let s = l in let c_rs = Set.complement rs in @@ -1206,7 +1205,6 @@ let modifies_only_live_regions #al #c rs l h h' = modifies_only_live_regions_weak rs s_c_rs h h'; loc_includes_restrict_to_regions s c_rs; modifies_loc_includes s h h' s_c_rs -#pop-options let no_upd_fresh_region #al #c r l h0 h1 = modifies_only_live_regions (HS.mod_set (Set.singleton r)) l h0 h1 diff --git a/ulib/FStar.Monotonic.Seq.fst b/ulib/FStar.Monotonic.Seq.fst index ef924718e9e..da801ea4714 100644 --- a/ulib/FStar.Monotonic.Seq.fst +++ b/ulib/FStar.Monotonic.Seq.fst @@ -277,7 +277,7 @@ let map_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows) (f let map_has_at_index (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows) (f:a -> Tot b) - (n:nat) (v:b) : HST.mem_predicate = fun h -> + (n:nat) (v:b) (h:mem) = let s = HS.sel h r in n < Seq.length s /\ Seq.index (map f s) n == v @@ -347,7 +347,7 @@ let collect_prefix_stable (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows let collect_has_at_index (#a:Type) (#b:Type) (#i:rid) (r:m_rref i (seq a) grows) (f:a -> Tot (seq b)) - (n:nat) (v:b) : HST.mem_predicate = fun (h:mem) -> + (n:nat) (v:b) (h:mem) = let s = HS.sel h r in n < Seq.length (collect f s) /\ Seq.index (collect f s) n == v diff --git a/ulib/FStar.ReflexiveTransitiveClosure.fst b/ulib/FStar.ReflexiveTransitiveClosure.fst index 4bab5a2868f..7727552199c 100644 --- a/ulib/FStar.ReflexiveTransitiveClosure.fst +++ b/ulib/FStar.ReflexiveTransitiveClosure.fst @@ -182,4 +182,4 @@ let induct (x:a) (y:a) (xy:squash (closure r x y)) : squash (p x y) = let xy = FStar.Squash.join_squash #(_closure r x y) xy in - FStar.Squash.bind_squash xy (fun xy -> induct_ r p f_refl f_step f_closure x y xy) + FStar.Squash.bind_squash xy (induct_ r p f_refl f_step f_closure x y) diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst index c081a4de7a2..fb9a54a5daf 100644 --- a/ulib/FStar.SquashProperties.fst +++ b/ulib/FStar.SquashProperties.fst @@ -108,7 +108,7 @@ let l1 (a:Type) (b:Type) = let f0 (x:pow a) (y:b) : GTot bool = false in let g0 (x:pow b) (y:a) : GTot bool = false in map_squash nr (fun (f:(retract (pow a) (pow b) -> GTot False)) -> - MkC (fun x y -> f0 x y) (fun x y -> g0 x y) (fun r x -> false_elim (f r)))) + MkC f0 g0 (fun r x -> false_elim (f r)))) (* The paradoxical set *) type u = p:Type -> Tot (squash (pow p)) diff --git a/ulib/FStar.Tactics.BreakVC.fst b/ulib/FStar.Tactics.BreakVC.fst index a4e4af39ca6..6222055173c 100644 --- a/ulib/FStar.Tactics.BreakVC.fst +++ b/ulib/FStar.Tactics.BreakVC.fst @@ -22,7 +22,7 @@ let aux (ps:proofstate) (p : __result unit -> Type0) spinoff (squash (p (Success () ps))); <==> { spinoff_equiv (squash (p (Success () ps))) } squash (p (Success () ps)); - ==>> { squash_p_impl_p _ } + ==>> { squash_p_impl_p fun _ -> p (Success () ps) } p (Success () ps); ==> { () } tac_return_wp () ps p; diff --git a/ulib/FStar.Tactics.Effect.fsti b/ulib/FStar.Tactics.Effect.fsti index d104d531ef3..3105eb38085 100644 --- a/ulib/FStar.Tactics.Effect.fsti +++ b/ulib/FStar.Tactics.Effect.fsti @@ -25,11 +25,11 @@ open FStar.Stubs.Tactics.Result * will break. (`synth_by_tactic` is fine) *) type tac_wp_t0 (a:Type) = - proofstate -> (__result a -> Type0) -> Type0 + proofstate -> (__result a -> GTot Type0) -> GTot Type0 unfold let tac_wp_monotonic (#a:Type) (wp:tac_wp_t0 a) = - forall (ps:proofstate) (p q:__result a -> Type0). + forall (ps:proofstate) (p q:__result a -> GTot Type0). (forall x. p x ==> q x) ==> (wp ps p ==> wp ps q) type tac_wp_t (a:Type) = wp:tac_wp_t0 a{tac_wp_monotonic wp} diff --git a/ulib/LowStar.Literal.fsti b/ulib/LowStar.Literal.fsti index abbaaf286b3..183e49ef519 100644 --- a/ulib/LowStar.Literal.fsti +++ b/ulib/LowStar.Literal.fsti @@ -90,7 +90,7 @@ unfold let buffer_of_literal_post (s: ascii_string) (h0: HS.mem) (b: IB.ibuffer val buffer_of_literal: (s: ascii_string) -> ST.Stack (IB.ibuffer UInt8.t) (requires (fun _ -> String.length s < pow2 32)) - (ensures fun h0 b h1 -> buffer_of_literal_post s h0 b h1) + (ensures buffer_of_literal_post s) /// .. note:: /// diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst index 19cc759d3ba..684ff260f0d 100644 --- a/ulib/LowStar.Monotonic.Buffer.fst +++ b/ulib/LowStar.Monotonic.Buffer.fst @@ -1047,7 +1047,7 @@ let loc_includes_union_l_regions [SMTPat (loc_includes (loc_union s1 s2) (loc_regions prf r))] = loc_includes_union_l s1 s2 (loc_regions prf r) -let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2 +let loc_disjoint = MG.loc_disjoint let loc_disjoint_sym = MG.loc_disjoint_sym diff --git a/ulib/LowStar.Monotonic.Buffer.fsti b/ulib/LowStar.Monotonic.Buffer.fsti index a1e1bd1c235..94e6961fe21 100644 --- a/ulib/LowStar.Monotonic.Buffer.fsti +++ b/ulib/LowStar.Monotonic.Buffer.fsti @@ -853,7 +853,7 @@ val loc_includes_union_l_regions val loc_disjoint (s1 s2: loc) -: Type0 +: GTot Type0 val loc_disjoint_sym (s1 s2: loc) diff --git a/ulib/LowStar.PrefixFreezableBuffer.fsti b/ulib/LowStar.PrefixFreezableBuffer.fsti index ab6e3eafb99..46ec82badc1 100644 --- a/ulib/LowStar.PrefixFreezableBuffer.fsti +++ b/ulib/LowStar.PrefixFreezableBuffer.fsti @@ -139,13 +139,13 @@ unfold let alloc_post_mem_common val gcmalloc (r:HS.rid) (len:u32) : ST (b:lbuffer len{frameOf b == r /\ recallable b}) (requires fun _ -> malloc_pre r len) - (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1) + (ensures alloc_post_mem_common) val malloc (r:HS.rid) (len:u32) : ST (b:lbuffer len{frameOf b == r /\ freeable b}) (requires fun _ -> malloc_pre r len) - (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1) + (ensures alloc_post_mem_common) unfold let alloca_pre (len:U32.t) = //precondition for stack allocated prefix freezable buffers UInt.size (U32.v len + 4) 32 /\ alloca_pre len diff --git a/ulib/Prims.fst b/ulib/Prims.fst index 178db26204d..9535c2c2712 100644 --- a/ulib/Prims.fst +++ b/ulib/Prims.fst @@ -312,7 +312,7 @@ let pure_pre = Type0 [pre] is also valid. This provides a way for postcondition formula to be typed in a context where they can assume the validity of the precondition. This is discussed extensively in Issue #57 *) -let pure_post' (a pre: Type) = _: a{pre} -> pure_pre +let pure_post' (a pre: Type) = _: a{pre} -> GTot Type0 let pure_post (a: Type) = pure_post' a True (** A pure weakest precondition transforms postconditions on [a]-typed @@ -322,7 +322,7 @@ let pure_post (a: Type) = pure_post' a True property over the postconditions To enforce it, we first define a vanilla wp type, and then refine it with the monotonicity condition *) -let pure_wp' (a: Type) = pure_post a -> pure_pre +let pure_wp' (a: Type) = pure_post a -> GTot pure_pre (** The monotonicity predicate is marked opaque_to_smt, meaning that its definition is hidden from the SMT solver, diff --git a/ulib/legacy/FStar.Array.fsti b/ulib/legacy/FStar.Array.fsti index 34d3a9345b2..c91ef0cc33d 100644 --- a/ulib/legacy/FStar.Array.fsti +++ b/ulib/legacy/FStar.Array.fsti @@ -52,7 +52,7 @@ val op_At_Bar (#a:Type0) (s1:array a) (s2:array a) modifies Set.empty h0 h1)) unfold let create_post (#a:Type0) (s:seq a) -: heap -> st_post' (array a) True +: heap -> array a -> heap -> Type0 = fun h0 x h1 -> x `unused_in` h0 /\ contains h1 x /\ diff --git a/ulib/legacy/FStar.Pointer.Base.fst b/ulib/legacy/FStar.Pointer.Base.fst index 144c25fd4dd..adb2e570a31 100644 --- a/ulib/legacy/FStar.Pointer.Base.fst +++ b/ulib/legacy/FStar.Pointer.Base.fst @@ -3812,12 +3812,12 @@ let modifies_buffer_elim' #t1 b p h h' = assert (n > 0); let pre (i: UInt32.t) - : Tot Type0 + : GTot Type0 = UInt32.v i < n in let post (i: UInt32.t) - : Tot Type0 + : GTot Type0 = pre i /\ ( let q = gpointer_of_buffer_cell b i in equal_values h q h' q