From 6cf684224d480ef2bb35ac355c45c7cb7cb4623f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 15:05:09 -0800 Subject: [PATCH 01/15] Normalize under refinements for expected type propagation. --- src/typechecker/FStarC.TypeChecker.TcTerm.fst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.TcTerm.fst b/src/typechecker/FStarC.TypeChecker.TcTerm.fst index 28e7720dec6..2c443f53e47 100644 --- a/src/typechecker/FStarC.TypeChecker.TcTerm.fst +++ b/src/typechecker/FStarC.TypeChecker.TcTerm.fst @@ -2051,7 +2051,7 @@ and tc_abs_expected_function_typ env (bs:binders) (t0:option (typ & bool)) (body (* CK: add this case since the type may be f:(a -> M b wp){φ}, in which case I drop the refinement *) (* NS: 07/21 dropping the refinement is not sound; we need to check that f validates phi. See Bug #284 *) | Tm_refine {b} -> - let _, bs, bs', copt, env_body, body, g_env = as_function_typ norm b.sort in + let _, bs, bs', copt, env_body, body, g_env = as_function_typ false b.sort in //we pass type `t` out to check afterwards the full refinement type is respected Some t, bs, bs', copt, env_body, body, g_env @@ -2284,8 +2284,8 @@ and tc_abs env (top:term) (bs:binders) (body:term) : term & lcomp & guard_t = tc_abs_expected_function_typ env bs topt body in if Debug.extreme () then - BU.print3 "After expected_function_typ, tfun_opt: %s, c_opt: %s, and expected type in envbody: %s\n" - (show tfun_opt) (show c_opt) (show (Env.expected_typ envbody)); + BU.print4 "After expected_function_typ, tfun_opt: %s, bs: %s, c_opt: %s, and expected type in envbody: %s\n" + (show tfun_opt) (show bs) (show c_opt) (show (Env.expected_typ envbody)); if !dbg_NYC then BU.print2 "!!!!!!!!!!!!!!!Guard for function with binders %s is %s\n" From 7364a6eef962bda99c3b8ee3fc9322f45289db1f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 16:28:39 -0800 Subject: [PATCH 02/15] Disable cross-effect subtyping. --- src/typechecker/FStarC.TypeChecker.Rel.fst | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index d6c2ae1ab47..f4ebf67aa1c 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -4026,6 +4026,16 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = solve_one_universe_eq orig u1 u2 wl | Tm_arrow {bs=bs1; comp=c1}, Tm_arrow {bs=bs2; comp=c2} -> + let eff1, eff2 = + let env = p_env wl orig in + c1 |> U.comp_effect_name |> Env.norm_eff_name env, + c2 |> U.comp_effect_name |> Env.norm_eff_name env in + + if not (Ident.lid_equals eff1 eff2) then + giveup wl (Thunk.mk fun _ -> "computation type mismatch in arrow: " ^ string_of_lid eff1 ^ " vs " ^ string_of_lid eff2) orig + + else + let mk_c c = function | [] -> c | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in From 857784a9037005255717ffc9a388f6fc6de85547 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 16:29:11 -0800 Subject: [PATCH 03/15] Start fixing ulib. --- ulib/FStar.All.fsti | 2 +- ulib/FStar.Classical.fst | 14 +++--- ulib/FStar.Classical.fsti | 4 +- ulib/FStar.IndefiniteDescription.fst | 2 +- ulib/FStar.Pervasives.fsti | 59 +++++++++++++------------- ulib/FStar.ST.fst | 2 +- ulib/FStar.Squash.fst | 6 +-- ulib/FStar.Squash.fsti | 4 +- ulib/FStar.Tactics.Effect.fsti | 6 +-- ulib/FStar.Tactics.V1.Logic.Lemmas.fst | 6 +-- ulib/Prims.fst | 8 ++-- 11 files changed, 57 insertions(+), 56 deletions(-) diff --git a/ulib/FStar.All.fsti b/ulib/FStar.All.fsti index 750653d6651..37f7f4ee176 100644 --- a/ulib/FStar.All.fsti +++ b/ulib/FStar.All.fsti @@ -28,7 +28,7 @@ unfold let lift_state_all (a : Type) (wp : st_wp a) (p : all_post a) = wp (fun a sub_effect STATE ~> ALL { lift_wp = lift_state_all } unfold -let lift_exn_all (a : Type) (wp : ex_wp a) (p : all_post a) (h : heap) = wp (fun ra -> p ra h) +let lift_exn_all (a : Type) (wp : ex_wp a) : all_wp_h heap a = fun (p : all_post a) (h : heap) -> wp (fun ra -> p ra h) sub_effect EXN ~> ALL { lift_wp = lift_exn_all } effect All (a:Type) (pre:all_pre) (post:(h:heap -> Tot (all_post' a (pre h)))) = diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst index dc7197a0995..0befaf76327 100644 --- a/ulib/FStar.Classical.fst +++ b/ulib/FStar.Classical.fst @@ -40,11 +40,11 @@ let get_equality #t a b = get_squashed #(equals a b) (a == b) let impl_to_arrow #a #b impl sx = bind_squash #(a -> GTot b) impl (fun f -> bind_squash sx (fun x -> return_squash (f x))) -let arrow_to_impl #a #b f = squash_double_arrow (return_squash (fun x -> f (return_squash x))) +let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squash b)) (fun x -> f (return_squash x))) let impl_intro_gtot #p #q f = return_squash f -let impl_intro_tot #p #q f = return_squash #(p -> GTot q) f +let impl_intro_tot #p #q f = return_squash #(p -> GTot q) fun x -> f x let impl_intro #p #q f = give_witness #(p ==> q) (squash_double_arrow (return_squash (lemma_to_squash_gtot f))) @@ -92,13 +92,13 @@ let gtot_to_lemma #a #p f x = give_proof #(p x) (return_squash (f x)) let forall_intro_squash_gtot #a #p f = bind_squash #(x: a -> GTot (p x)) #(forall (x: a). p x) - (squash_double_arrow #a #p (return_squash f)) + (squash_double_arrow #a #(fun x -> p x) (return_squash f)) (fun f -> lemma_forall_intro_gtot #a #p f) let forall_intro_squash_gtot_join #a #p f = join_squash (bind_squash #(x: a -> GTot (p x)) #(forall (x: a). p x) - (squash_double_arrow #a #p (return_squash f)) + (squash_double_arrow #a #(fun x -> p x) (return_squash f)) (fun f -> lemma_forall_intro_gtot #a #p f)) let forall_intro #a #p f = give_witness (forall_intro_squash_gtot (lemma_to_squash_gtot #a #p f)) @@ -115,10 +115,10 @@ let forall_intro_2 #a #b #p f = let forall_intro_2_with_pat #a #b #c #p pat f = forall_intro_2 #a #b #p f let forall_intro_3 #a #b #c #p f = - let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 (f x) in + let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 #_ #_ #(fun y z -> p x y z) (f x) in forall_intro g -let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #p f +let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #(fun x y z -> p x y z) f let forall_intro_4 #a #b #c #d #p f = let g: x: a -> Lemma (forall (y: b x) (z: c x y) (w: d x y z). p x y z w) = @@ -165,7 +165,7 @@ let exists_intro_not_all_not (#a:Type) (#p:a -> Type) (get_proof (forall x. ~ (p x))) (fun (g: (forall x. ~ (p x))) -> bind_squash #(x:a -> GTot (~(p x))) #Prims.empty g - (fun (h:(x:a -> GTot (~(p x)))) -> f h)) + (fun (h:(x:a -> GTot (~(p x)))) -> f fun x -> h x)) in () #pop-options diff --git a/ulib/FStar.Classical.fsti b/ulib/FStar.Classical.fsti index e58b28d8b03..f0947bad3e8 100644 --- a/ulib/FStar.Classical.fsti +++ b/ulib/FStar.Classical.fsti @@ -321,7 +321,7 @@ val forall_intro_4 TODO: Seems overly specific; could be removed? *) val forall_impl_intro (#a: Type) - (#p #q: (a -> GTot Type)) + (#p #q: (a -> Type)) ($_: (x: a -> squash (p x) -> Lemma (q x))) : Lemma (forall x. p x ==> q x) @@ -331,7 +331,7 @@ val forall_impl_intro *) val ghost_lemma (#a: Type) - (#p: (a -> GTot Type0)) + (#p: (a -> Type0)) (#q: (a -> unit -> GTot Type0)) ($_: (x: a -> Lemma (requires p x) (ensures (q x ())))) : Lemma (forall (x: a). p x ==> q x ()) diff --git a/ulib/FStar.IndefiniteDescription.fst b/ulib/FStar.IndefiniteDescription.fst index 0bad5da531f..3bf86a914c3 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 _ p \ No newline at end of file + indefinite_description_ghost _ (fun x -> p x) \ No newline at end of file diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index d9f46f6f97f..bd624178796 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -342,7 +342,7 @@ let reveal_opaque (s: string) = norm_spec [delta_once [s]] (with monotonicity refinement) *) unfold -let pure_return (a:Type) (x:a) : pure_wp a = +let pure_return (a:Type) (x:a) : GTot (pure_wp a) = reveal_opaque (`%pure_wp_monotonic) pure_wp_monotonic; pure_return0 a x @@ -455,7 +455,7 @@ let st_wp_h (heap a: Type) = st_post_h heap a -> Tot (st_pre_h heap) (** Returning a value does not transform the state *) unfold -let st_return (heap a: Type) (x: a) (p: st_post_h heap a) = p x +let st_return (heap a: Type) (x: a) : GTot (st_wp_h heap a) = fun (p: st_post_h heap a) -> p x (** Sequential composition of stateful WPs *) unfold @@ -463,24 +463,27 @@ let st_bind_wp (heap: Type) (a b: Type) (wp1: st_wp_h heap a) - (wp2: (a -> GTot (st_wp_h heap b))) + (wp2: a -> st_wp_h heap b) + : st_wp_h heap b = fun (p: st_post_h heap b) (h0: heap) - = wp1 (fun a h1 -> wp2 a p h1) h0 + -> wp1 (fun a h1 -> wp2 a p h1) h0 (** Branching for stateful WPs *) unfold let st_if_then_else (heap a p: Type) (wp_then wp_else: st_wp_h heap a) + : st_wp_h heap a = + fun (post: st_post_h heap a) (h0: heap) - = wp_then post h0 /\ (~p ==> wp_else post h0) + -> wp_then post h0 /\ (~p ==> wp_else post h0) (** As with [PURE] the [wp] combinator names the postcondition as [k] to avoid duplicating it. *) unfold -let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) (post: st_post_h heap a) (h0: heap) = +let st_ite_wp (heap a: Type) (wp: st_wp_h heap a) : st_wp_h heap a = fun (post: st_post_h heap a) (h0: heap) -> forall (k: st_post_h heap a). (forall (x: a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0 @@ -491,12 +494,12 @@ let st_stronger (heap a: Type) (wp1 wp2: st_wp_h heap a) = (** Closing the scope of a binder within a stateful WP *) unfold -let st_close_wp (heap a b: Type) (wp: (b -> GTot (st_wp_h heap a))) (p: st_post_h heap a) (h: heap) = +let st_close_wp (heap a b: Type) (wp: b -> st_wp_h heap a) : st_wp_h heap a = fun (p: st_post_h heap a) (h: heap) -> (forall (b: b). wp b p h) (** Applying a stateful WP to a trivial postcondition *) unfold -let st_trivial (heap a: Type) (wp: st_wp_h heap a) = (forall h0. wp (fun r h1 -> True) h0) +let st_trivial (heap a: Type) (wp: st_wp_h heap a) : GTot prop = (forall h0. wp (fun r h1 -> True) h0) (** Introducing a new effect template [STATE_h] *) new_effect { @@ -546,8 +549,7 @@ let ex_return (a: Type) (x: a) (p: ex_post a) : GTot Type0 = p (V x) (** Sequential composition of exception-raising code requires case analysing the result of the first computation before "running" the second one *) unfold -let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_post b) - : GTot Type0 = +let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> (ex_wp b))) : ex_wp b = fun p -> forall (k: ex_post b). (forall (rb: result b). {:pattern (guard_free (k rb))} p rb ==> k rb) ==> (wp1 (function @@ -558,12 +560,12 @@ let ex_bind_wp (a b: Type) (wp1: ex_wp a) (wp2: (a -> GTot (ex_wp b))) (p: ex_po (** As for other effects, branching in [ex_wp] appears in two forms. First, a simple case analysis on [p] *) unfold -let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) (post: ex_post a) = +let ex_if_then_else (a p: Type) (wp_then wp_else: ex_wp a) : ex_wp a = fun (post: ex_post a) -> wp_then post /\ (~p ==> wp_else post) (** Naming continuations for use with branching *) unfold -let ex_ite_wp (a: Type) (wp: ex_wp a) (post: ex_post a) = +let ex_ite_wp (a: Type) (wp: ex_wp a) : ex_wp a = fun (post: ex_post a) -> forall (k: ex_post a). (forall (rb: result a). {:pattern (guard_free (k rb))} post rb ==> k rb) ==> wp k @@ -573,11 +575,11 @@ let ex_stronger (a: Type) (wp1 wp2: ex_wp a) = (forall (p: ex_post a). wp1 p ==> (** Closing the scope of a binder for exceptional WPs *) unfold -let ex_close_wp (a b: Type) (wp: (b -> GTot (ex_wp a))) (p: ex_post a) = (forall (b: b). wp b p) +let ex_close_wp (a b: Type) (wp: b -> ex_wp a) : ex_wp a = fun (p: ex_post a) -> (forall (b: b). wp b p) (** Applying a computation with a trivial postcondition *) unfold -let ex_trivial (a: Type) (wp: ex_wp a) = wp (fun r -> True) +let ex_trivial (a: Type) (wp: ex_wp a) : GTot ex_pre = wp (fun r -> True) (** Introduce a new effect for [EXN] *) new_effect { @@ -601,7 +603,7 @@ effect Exn (a: Type) (pre: ex_pre) (post: ex_post' a pre) = NOTE: BE WARNED, CODE IN THE [EXN] EFFECT IS ONLY CHECKED FOR PARTIAL CORRECTNESS *) unfold -let lift_div_exn (a: Type) (wp: pure_wp a) (p: ex_post a) = wp (fun a -> p (V a)) +let lift_div_exn (a: Type) (wp: pure_wp a) : ex_wp a = fun (p: ex_post a) -> wp (fun a -> p (V a)) sub_effect DIV ~> EXN { lift_wp = lift_div_exn } (** A variant of [Exn] with trivial pre- and postconditions *) @@ -637,7 +639,7 @@ let all_wp_h (h a: Type) = all_post_h h a -> Tot (all_pre_h h) (** Returning a value [x] normally promotes it to the [V x] result without touching the [heap] *) unfold -let all_return (heap a: Type) (x: a) (p: all_post_h heap a) = p (V x) +let all_return (heap a: Type) (x: a) : GTot (all_wp_h heap a) = fun (p: all_post_h heap a) -> p (V x) (** Sequential composition for [ALL_h] is like [EXN]: case analysis of the exceptional result before "running" the continuation *) @@ -646,10 +648,9 @@ let all_bind_wp (heap: Type) (a b: Type) (wp1: all_wp_h heap a) - (wp2: (a -> GTot (all_wp_h heap b))) - (p: all_post_h heap b) - (h0: heap) - : GTot Type0 = + (wp2: a -> all_wp_h heap b) + : all_wp_h heap b = + fun (p: all_post_h heap b) (h0: heap) -> wp1 (fun ra h1 -> (match ra with | V v -> wp2 v p h1 @@ -662,13 +663,13 @@ unfold let all_if_then_else (heap a p: Type) (wp_then wp_else: all_wp_h heap a) - (post: all_post_h heap a) - (h0: heap) - = wp_then post h0 /\ (~p ==> wp_else post h0) + : all_wp_h heap a + = fun (post: all_post_h heap a) (h0: heap) + -> wp_then post h0 /\ (~p ==> wp_else post h0) (** Naming postcondition for better sharing in [ALL_h] *) unfold -let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) (post: all_post_h heap a) (h0: heap) = +let all_ite_wp (heap a: Type) (wp: all_wp_h heap a) : all_wp_h heap a = fun (post: all_post_h heap a) (h0: heap) -> forall (k: all_post_h heap a). (forall (x: result a) (h: heap). {:pattern (guard_free (k x h))} post x h ==> k x h) ==> wp k h0 @@ -681,14 +682,14 @@ let all_stronger (heap a: Type) (wp1 wp2: all_wp_h heap a) = unfold let all_close_wp (heap a b: Type) - (wp: (b -> GTot (all_wp_h heap a))) - (p: all_post_h heap a) - (h: heap) - = (forall (b: b). wp b p h) + (wp: b -> all_wp_h heap a) + : all_wp_h heap a + = fun (p: all_post_h heap a) (h: heap) + -> (forall (b: b). wp b p h) (** Applying an [ALL_h] wp to a trivial postcondition *) unfold -let all_trivial (heap a: Type) (wp: all_wp_h heap a) = (forall (h0: heap). wp (fun r h1 -> True) h0) +let all_trivial (heap a: Type) (wp: all_wp_h heap a) : GTot prop = (forall (h0: heap). wp (fun r h1 -> True) h0) (** Introducing the [ALL_h] effect template *) new_effect { diff --git a/ulib/FStar.ST.fst b/ulib/FStar.ST.fst index 4f44fd94ba8..7cf25bcd895 100644 --- a/ulib/FStar.ST.fst +++ b/ulib/FStar.ST.fst @@ -30,7 +30,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' heap a pre let gst_post (a:Type) = st_post_h heap a let gst_wp (a:Type) = st_wp_h heap a -unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:heap) = wp (fun a -> p a h) +unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h heap a = fun (p:gst_post a) (h:heap) -> wp (fun a -> p a h) sub_effect DIV ~> GST = lift_div_gst let heap_rel (h1:heap) (h2:heap) = diff --git a/ulib/FStar.Squash.fst b/ulib/FStar.Squash.fst index c29493a6f9e..2b2d5bc9181 100644 --- a/ulib/FStar.Squash.fst +++ b/ulib/FStar.Squash.fst @@ -35,15 +35,15 @@ let give_proof (#p:Type) _ = () let proof_irrelevance (p:Type) x y = () let squash_double_arrow #a #p f = - bind_squash f push_squash + bind_squash f fun g -> push_squash fun x -> g x -let push_sum (#a:Type) (#b:(a -> Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) = +let push_sum (#a:Type) (#b:(a -> GTot Type)) ($p : dtuple2 a (fun (x:a) -> squash (b x))) = match p with | Mkdtuple2 x y -> bind_squash #(b x) #(dtuple2 a b) y (fun y' -> return_squash (Mkdtuple2 x y')) -let squash_double_sum (#a:Type) (#b:(a -> Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) = +let squash_double_sum (#a:Type) (#b:(a -> GTot Type)) (p : squash (dtuple2 a (fun (x:a) -> squash (b x)))) = bind_squash p (fun p' -> push_sum p') // Need eta... let map_squash (#a:Type) (#b:Type) s f = diff --git a/ulib/FStar.Squash.fsti b/ulib/FStar.Squash.fsti index c0563201d88..15c7d84f966 100644 --- a/ulib/FStar.Squash.fsti +++ b/ulib/FStar.Squash.fsti @@ -76,13 +76,13 @@ val squash_double_arrow (#a: Type) (#p: (a -> Type)) ($f: (squash (x: a -> GTot : GTot (squash (x: a -> GTot (p x))) (** The analog of [push_squash] for sums (existential quantification *) -val push_sum (#a: Type) (#b: (a -> Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x)))) +val push_sum (#a: Type) (#b: (a -> GTot Type)) ($p: (dtuple2 a (fun (x: a) -> squash (b x)))) : Tot (squash (dtuple2 a b)) (** The analog of [squash_double_arrow] for sums (existential quantification) *) val squash_double_sum (#a: Type) - (#b: (a -> Type)) + (#b: (a -> GTot Type)) ($p: (squash (dtuple2 a (fun (x: a) -> squash (b x))))) : Tot (squash (dtuple2 a b)) diff --git a/ulib/FStar.Tactics.Effect.fsti b/ulib/FStar.Tactics.Effect.fsti index d104d531ef3..579516ce3bf 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} @@ -58,7 +58,7 @@ let tac_bind_wp (#a #b:Type) (wp_f:tac_wp_t a) (wp_g:a -> tac_wp_t b) : tac_wp_t unfold let tac_wp_compact (a:Type) (wp:tac_wp_t a) : tac_wp_t a = fun ps post -> - forall (k:__result a -> Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k + forall (k:__result a -> GTot Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k /// tac_bind_interleave_begin is an ugly hack to get interface interleaving diff --git a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst index 6c659076957..71e51968676 100644 --- a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst +++ b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst @@ -16,18 +16,18 @@ module FStar.Tactics.V1.Logic.Lemmas let fa_intro_lem (#a:Type) (#p:a -> Type) (f:(x:a -> squash (p x))) : Lemma (forall (x:a). p x) = - FStar.Classical.lemma_forall_intro_gtot + FStar.Classical.lemma_forall_intro_gtot #_ #(fun x -> p x) ((fun x -> FStar.IndefiniteDescription.elim_squash (f x)) <: (x:a -> GTot (p x))) let split_lem #a #b sa sb = () let imp_intro_lem #a #b f = - FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x f)) + FStar.Classical.give_witness (FStar.Classical.arrow_to_impl (fun (x:squash a) -> FStar.Squash.bind_squash x (fun y -> f y))) let __lemma_to_squash #req #ens (_ : squash req) (h : (unit -> Lemma (requires req) (ensures ens))) : squash ens = h () -let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq f) +let vbind #p #q sq f = FStar.Classical.give_witness_from_squash (FStar.Squash.bind_squash sq (fun y -> f y)) let or_ind #p #q #phi o l r = () diff --git a/ulib/Prims.fst b/ulib/Prims.fst index f25def5bf9c..9535c2c2712 100644 --- a/ulib/Prims.fst +++ b/ulib/Prims.fst @@ -351,7 +351,7 @@ type guard_free : Type0 -> Type0 Clients should not use it directly, instead use FStar.Pervasives.pure_return *) unfold -let pure_return0 (a: Type) (x: a) : pure_wp a = +let pure_return0 (a: Type) : a -> GTot (pure_wp a) = fun x -> fun (p: pure_post a) -> forall (return_val: a). return_val == x ==> p return_val @@ -363,7 +363,7 @@ unfold let pure_bind_wp0 (a b: Type) (wp1: pure_wp a) - (wp2: (a -> GTot (pure_wp b))) + (wp2: (a -> pure_wp b)) : pure_wp b = fun (p: pure_post b) -> wp1 (fun (bind_result_1: a) -> wp2 bind_result_1 p) @@ -410,11 +410,11 @@ let pure_stronger (a: Type) (wp1 wp2: pure_wp a) = forall (p: pure_post a). wp1 Clients should not use it directly, instead use FStar.Pervasives.pure_close_wp *) unfold -let pure_close_wp0 (a b: Type) (wp: (b -> GTot (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p +let pure_close_wp0 (a b: Type) (wp: (b -> (pure_wp a))) : pure_wp a = fun (p: pure_post a) -> forall (b: b). wp b p (** Trivial WP for PURE: Prove the WP with the trivial postcondition *) unfold -let pure_trivial (a: Type) (wp: pure_wp a) = wp (fun (trivial_result: a) -> True) +let pure_trivial (a: Type) : pure_wp a -> GTot Type = fun wp -> wp (fun (trivial_result: a) -> True) (** Introduces the PURE effect. The definition of the PURE effect is fixed. From d3d0b64e030f6e31db3328d1f4f363ca80a7fbfd Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 16:49:05 -0800 Subject: [PATCH 04/15] Fix tactic effect. --- ulib/FStar.Tactics.Effect.fsti | 6 +++--- ulib/FStar.Tactics.V1.Derived.fst | 2 +- ulib/FStar.Tactics.V2.Derived.fst | 2 +- ulib/Prims.fst | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/ulib/FStar.Tactics.Effect.fsti b/ulib/FStar.Tactics.Effect.fsti index 579516ce3bf..d104d531ef3 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 -> GTot Type0) -> GTot Type0 + proofstate -> (__result a -> Type0) -> Type0 unfold let tac_wp_monotonic (#a:Type) (wp:tac_wp_t0 a) = - forall (ps:proofstate) (p q:__result a -> GTot Type0). + forall (ps:proofstate) (p q:__result a -> 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} @@ -58,7 +58,7 @@ let tac_bind_wp (#a #b:Type) (wp_f:tac_wp_t a) (wp_g:a -> tac_wp_t b) : tac_wp_t unfold let tac_wp_compact (a:Type) (wp:tac_wp_t a) : tac_wp_t a = fun ps post -> - forall (k:__result a -> GTot Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k + forall (k:__result a -> Type0). (forall (r:__result a).{:pattern (guard_free (k r))} post r ==> k r) ==> wp ps k /// tac_bind_interleave_begin is an ugly hack to get interface interleaving diff --git a/ulib/FStar.Tactics.V1.Derived.fst b/ulib/FStar.Tactics.V1.Derived.fst index a4478fa47b2..3e918b038b1 100644 --- a/ulib/FStar.Tactics.V1.Derived.fst +++ b/ulib/FStar.Tactics.V1.Derived.fst @@ -428,7 +428,7 @@ val (<|>) : (unit -> Tac 'a) -> let (<|>) t1 t2 = fun () -> or_else t1 t2 let first (ts : list (unit -> Tac 'a)) : Tac 'a = - L.fold_right (<|>) ts (fun () -> fail "no tactics to try") () + L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") () let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) = match catch t with diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst index 06f6a002612..f8d87432266 100644 --- a/ulib/FStar.Tactics.V2.Derived.fst +++ b/ulib/FStar.Tactics.V2.Derived.fst @@ -482,7 +482,7 @@ val (<|>) : (unit -> Tac 'a) -> let (<|>) t1 t2 = fun () -> or_else t1 t2 let first (ts : list (unit -> Tac 'a)) : Tac 'a = - L.fold_right (<|>) ts (fun () -> fail "no tactics to try") () + L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") () let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) = match catch t with diff --git a/ulib/Prims.fst b/ulib/Prims.fst index 9535c2c2712..178db26204d 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} -> GTot Type0 +let pure_post' (a pre: Type) = _: a{pre} -> pure_pre 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 -> GTot pure_pre +let pure_wp' (a: Type) = pure_post a -> pure_pre (** The monotonicity predicate is marked opaque_to_smt, meaning that its definition is hidden from the SMT solver, From 61d83010ae8374018c9ff6c479b43362c23a74d0 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 17:32:28 -0800 Subject: [PATCH 05/15] Fix more ulib. --- ulib/FStar.BigOps.fst | 2 +- ulib/FStar.BigOps.fsti | 10 +++++----- ulib/FStar.Cardinality.Cantor.fst | 6 +++--- ulib/FStar.Cardinality.Cantor.fsti | 4 ++-- ulib/FStar.Cardinality.Universes.fst | 9 ++++----- ulib/FStar.Cardinality.Universes.fsti | 4 ++-- ulib/FStar.Fin.fst | 9 ++++----- ulib/FStar.Functions.fsti | 11 +++++++++++ ulib/FStar.HyperStack.ST.fsti | 14 +++++++------- ulib/FStar.ReflexiveTransitiveClosure.fst | 4 ++-- ulib/FStar.SquashProperties.fst | 17 +++++------------ ulib/experimental/FStar.OrdSet.fst | 2 +- ulib/legacy/FStar.Array.fsti | 2 +- ulib/legacy/FStar.Relational.Comp.fst | 2 +- 14 files changed, 49 insertions(+), 47 deletions(-) diff --git a/ulib/FStar.BigOps.fst b/ulib/FStar.BigOps.fst index 552c224774c..d1cb673b6ab 100644 --- a/ulib/FStar.BigOps.fst +++ b/ulib/FStar.BigOps.fst @@ -108,7 +108,7 @@ let pairwise_or'_nil (#a:Type) (f:a -> a -> Type0) = assert (pairwise_or' f [] == False) by (T.compute()) let pairwise_or'_cons (#a:Type) (f:a -> a -> Type) (hd:a) (tl:list a) - = assert (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl)) + = assert_norm (pairwise_or' f (hd::tl) == (big_or' (f hd) tl \/ pairwise_or' f tl)) let pairwise_or'_prop (#a:Type) (f:a -> a -> Type) (l:list a) = match l with diff --git a/ulib/FStar.BigOps.fsti b/ulib/FStar.BigOps.fsti index b3a307a7fac..d54da25749c 100644 --- a/ulib/FStar.BigOps.fsti +++ b/ulib/FStar.BigOps.fsti @@ -85,7 +85,7 @@ val map_op'_cons (** [big_and' f l] = [/\_{x in l} f x] *) [@@ __reduce__] -let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_and f l True +let big_and' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p /\ q) (fun x -> f x) l True (** Equations for [big_and'] showing it to be trivial over the empty list *) val big_and'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_and' f [] == True) @@ -125,7 +125,7 @@ let big_and #a (f: (a -> Type)) (l: list a) : prop = (** [big_or f l] = [\/_{x in l} f x] *) [@@ __reduce__] -let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' l_or f l False +let big_or' #a (f: (a -> Type)) (l: list a) : Type = map_op' (fun p q -> p \/ q) (fun x -> f x) l False (** Equations for [big_or] showing it to be [False] on the empty list *) val big_or'_nil (#a: Type) (f: (a -> Type)) : Lemma (big_or' f [] == False) @@ -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 -> b)) (l: list a) (z: b) : GTot b = +let rec pairwise_op' #a #b (op: (b -> b -> GTot b)) (f: (a -> a -> GTot 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' l_and f l True +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 (** 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) @@ -235,7 +235,7 @@ let pairwise_and #a (f: (a -> a -> Type)) (l: list a) : prop = (** [pairwise_or f l] disjoins [f] on all pairs excluding the diagonal i.e., [pairwise_or f [a; b; c] = f a b \/ f a c \/ f b c] *) [@@ __reduce__] -let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' l_or f l False +let pairwise_or' #a (f: (a -> a -> Type)) (l: list a) : Type = pairwise_op' (fun p q -> p \/ q) (fun x y -> f x y) l False (** Equations for [pairwise_or'] showing it to be a fold with [big_or'] *) val pairwise_or'_nil (#a: Type) (f: (a -> a -> Type0)) : Lemma (pairwise_or' f [] == False) diff --git a/ulib/FStar.Cardinality.Cantor.fst b/ulib/FStar.Cardinality.Cantor.fst index 349cd6ee246..107034f2df3 100644 --- a/ulib/FStar.Cardinality.Cantor.fst +++ b/ulib/FStar.Cardinality.Cantor.fst @@ -2,7 +2,7 @@ module FStar.Cardinality.Cantor open FStar.Functions -let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) = +let no_surj_powerset (a : Type) (f : a -> GTot (powerset a)) : Lemma (~(is_surj f)) = let aux () : Lemma (requires is_surj f) (ensures False) = (* Cantor's proof: given a supposed surjective f, we define a set s that cannot be in the image of f. Namely, @@ -16,9 +16,9 @@ let no_surj_powerset (a : Type) (f : a -> powerset a) : Lemma (~(is_surj f)) = in Classical.move_requires aux () -let no_inj_powerset (a : Type) (f : powerset a -> a) : Lemma (~(is_inj f)) = +let no_inj_powerset (a : Type) (f : powerset a -> GTot a) : Lemma (~(is_inj f)) = let aux () : Lemma (requires is_inj f) (ensures False) = - let g : a -> GTot (powerset a) = inverse_of_inj f (fun _ -> false) in + let g : a -> GTot (powerset a) = inverse_of_inj (fun x -> f x) (fun _ -> false) in no_surj_powerset a g in Classical.move_requires aux () diff --git a/ulib/FStar.Cardinality.Cantor.fsti b/ulib/FStar.Cardinality.Cantor.fsti index af749e8bedc..cd51ee8f57d 100644 --- a/ulib/FStar.Cardinality.Cantor.fsti +++ b/ulib/FStar.Cardinality.Cantor.fsti @@ -6,8 +6,8 @@ set. *) open FStar.Functions -val no_surj_powerset (a : Type) (f : a -> powerset a) +val no_surj_powerset (a : Type) (f : a -> GTot (powerset a)) : Lemma (~(is_surj f)) -val no_inj_powerset (a : Type) (f : powerset a -> a) +val no_inj_powerset (a : Type) (f : powerset a -> GTot a) : Lemma (~(is_inj f)) diff --git a/ulib/FStar.Cardinality.Universes.fst b/ulib/FStar.Cardinality.Universes.fst index 5eb0e8bafa1..a6a2e6fa57c 100644 --- a/ulib/FStar.Cardinality.Universes.fst +++ b/ulib/FStar.Cardinality.Universes.fst @@ -19,7 +19,7 @@ let aux_inj_type_powerset (f1 f2 : powerset (Type u#a)) assert (xx1 === xx2); assert (f1 == f2) -let inj_type_powerset () : Lemma (is_inj type_powerset) = +let inj_type_powerset () : Lemma (is_inj_tot type_powerset) = Classical.forall_intro_2 (fun f1 -> Classical.move_requires (aux_inj_type_powerset f1)) (* let u' > u be universes. (u' = max(a+1, b), u=a below) @@ -29,14 +29,13 @@ let inj_type_powerset () : Lemma (is_inj type_powerset) = 3- Therefore, there cannot be an injection from Type(u') into Type(u), otherwise we would compose it with the first injection and obtain the second impossible injection. *) -let no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a) : Lemma (~(is_inj f)) = +let no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a)) : Lemma (~(is_inj f)) = let aux () : Lemma (requires is_inj f) (ensures False) = - let comp : powerset (Type u#a) -> Type u#a = fun x -> f (type_powerset x) in + let comp : powerset (Type u#a) -> GTot (Type u#a) = fun x -> f (to_gtot type_powerset x) in inj_type_powerset (); - inj_comp type_powerset f; no_inj_powerset _ comp in Classical.move_requires aux () -let no_inj_universes_suc (f : Type u#(a+1) -> Type u#a) : Lemma (~(is_inj f)) = +let no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a)) : Lemma (~(is_inj f)) = no_inj_universes f diff --git a/ulib/FStar.Cardinality.Universes.fsti b/ulib/FStar.Cardinality.Universes.fsti index 4a4baaa14a0..bd0a54ab8e9 100644 --- a/ulib/FStar.Cardinality.Universes.fsti +++ b/ulib/FStar.Cardinality.Universes.fsti @@ -6,9 +6,9 @@ open FStar.Cardinality.Cantor (* Prove that there can be no injection from a universe into a strictly smaller universe. We use `max (a+1) b` to represent an arbitrary universe strictly larger than `a` as we cannot write sums of universe levels. *) -val no_inj_universes (f : Type u#(max (a+1) b) -> Type u#a) +val no_inj_universes (f : Type u#(max (a+1) b) -> GTot (Type u#a)) : Lemma (~(is_inj f)) (* A simpler version for the +1 case. *) -val no_inj_universes_suc (f : Type u#(a+1) -> Type u#a) +val no_inj_universes_suc (f : Type u#(a+1) -> GTot (Type u#a)) : Lemma (~(is_inj f)) diff --git a/ulib/FStar.Fin.fst b/ulib/FStar.Fin.fst index 306c781e04a..33640898625 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 - 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 + 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 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,8 +152,7 @@ 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 - in Classical.forall_intro all_but_first_pigeon_remain_in_reduced; + end); 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.Functions.fsti b/ulib/FStar.Functions.fsti index 9982dc4ddf5..747bad9987d 100644 --- a/ulib/FStar.Functions.fsti +++ b/ulib/FStar.Functions.fsti @@ -6,12 +6,23 @@ about functions and sets. *) let is_inj (#a #b : _) (f : a -> GTot b) : prop = forall (x1 x2 : a). f x1 == f x2 ==> x1 == x2 +let to_gtot #a #b (f: a -> b) : (a -> GTot b) = fun x -> f x + +let is_inj_tot #a #b (f: a -> b) : prop = + is_inj (to_gtot f) + let is_surj (#a #b : _) (f : a -> GTot b) : prop = forall (y:b). exists (x:a). f x == y +let is_surj_tot #a #b (f: a -> b) : prop = + is_surj (to_gtot f) + let is_bij (#a #b : _) (f : a -> GTot b) : prop = is_inj f /\ is_surj f +let is_bij_tot #a #b (f: a -> b) : prop = + is_bij (to_gtot f) + let in_image (#a #b : _) (f : a -> GTot b) (y : b) : prop = exists (x:a). f x == y diff --git a/ulib/FStar.HyperStack.ST.fsti b/ulib/FStar.HyperStack.ST.fsti index 695db7263ce..41abbe1ac8c 100644 --- a/ulib/FStar.HyperStack.ST.fsti +++ b/ulib/FStar.HyperStack.ST.fsti @@ -47,7 +47,7 @@ let gst_post' (a:Type) (pre:Type) = st_post_h' mem a pre let gst_post (a:Type) = st_post_h mem a let gst_wp (a:Type) = st_wp_h mem a -unfold let lift_div_gst (a:Type) (wp:pure_wp a) (p:gst_post a) (h:mem) = wp (fun a -> p a h) +unfold let lift_div_gst (a:Type) (wp:pure_wp a) : st_wp_h mem a = fun p h -> wp (fun a -> p a h) sub_effect DIV ~> GST = lift_div_gst (* @@ -337,14 +337,14 @@ let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem) *) val salloc (#a:Type) (#rel:preorder a) (init:a) :StackInline (mstackref a rel) (requires (fun m -> is_stack_region (get_tip m))) - (ensures salloc_post init) + (ensures fun m0 r m1 -> salloc_post init m0 r m1) // JP, AR: these are not supported in C, and `salloc` already benefits from // automatic memory management. [@@ (deprecated "Use salloc instead") ] val salloc_mm (#a:Type) (#rel:preorder a) (init:a) :StackInline (mmmstackref a rel) (requires (fun m -> is_stack_region (get_tip m))) - (ensures salloc_post init) + (ensures fun m0 r m1 -> salloc_post init m0 r m1) [@@ (deprecated "Use salloc instead") ] val sfree (#a:Type) (#rel:preorder a) (r:mmmstackref a rel) @@ -387,11 +387,11 @@ let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem) val ralloc (#a:Type) (#rel:preorder a) (i:rid) (init:a) :ST (mref a rel) (requires (fun m -> is_eternal_region i)) - (ensures (ralloc_post i init)) + (ensures fun m0 r m1 -> ralloc_post i init m0 r m1) val ralloc_mm (#a:Type) (#rel:preorder a) (i:rid) (init:a) :ST (mmmref a rel) (requires (fun m -> is_eternal_region i)) - (ensures (ralloc_post i init)) + (ensures fun m0 r m1 -> ralloc_post i init m0 r m1) (* * AR: 12/26: For a ref to be readable/writable/free-able, @@ -417,7 +417,7 @@ unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m *) 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)) + (ensures fun m0 _ m1 -> assign_post r v m0 () m1) 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 @@ -428,7 +428,7 @@ unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) *) val op_Bang (#a:Type) (#rel:preorder a) (r:mreference a rel) :Stack a (requires (fun m -> r `is_live_for_rw_in` m)) - (ensures (deref_post r)) + (ensures fun m0 x m1 -> deref_post r m0 x m1) let modifies_none (h0:mem) (h1:mem) = modifies Set.empty h0 h1 diff --git a/ulib/FStar.ReflexiveTransitiveClosure.fst b/ulib/FStar.ReflexiveTransitiveClosure.fst index c6e2a6097ad..4bab5a2868f 100644 --- a/ulib/FStar.ReflexiveTransitiveClosure.fst +++ b/ulib/FStar.ReflexiveTransitiveClosure.fst @@ -157,7 +157,7 @@ let squash_implies_to_arrow (p:Type u#p) (q:Type) let squash_double_arrow (#a:Type u#a) (#p:Type0) (f:(squash (a -> Tot (squash p)))) : Tot (squash (a -> GTot p)) = - FStar.Squash.squash_double_arrow f + FStar.Squash.squash_double_arrow (Squash.map_squash f (fun f x -> f x) <: squash (a -> GTot (squash p))) let stable_on_closure #a r p hr = assert (forall x y. p x ==> closure r x y ==> p y) by @@ -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 (induct_ r p f_refl f_step f_closure x y) + FStar.Squash.bind_squash xy (fun xy -> induct_ r p f_refl f_step f_closure x y xy) diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst index d8b9e6664f6..fb9a54a5daf 100644 --- a/ulib/FStar.SquashProperties.fst +++ b/ulib/FStar.SquashProperties.fst @@ -57,18 +57,11 @@ let bool_of_or #p #q t = | Prims.Right _ -> false val excluded_middle : p:Type -> GTot (squash (b:bool{b <==> p})) -let excluded_middle (p:Type) = map_squash (join_squash (get_proof (p \/ (~p)))) bool_of_or +let excluded_middle (p:Type) = + map_squash (join_squash (get_proof (p \/ (~p)))) (fun x -> (bool_of_or x <: b:bool { b <==> p })) -val excluded_middle_squash : p:Type0 -> GTot (p \/ ~p) -let excluded_middle_squash p = - bind_squash (excluded_middle p) (fun x -> - if x then - map_squash (get_proof p) (Prims.Left #p) - else - return_squash (Prims.Right #_ #(~p) (return_squash (fun (h:p) -> - give_proof (return_squash h); - false_elim #False ())))) +let excluded_middle_squash (p: Type0) : GTot (p \/ ~p) = join_squash () (* we thought we might prove proof irrelevance by Berardi ... but didn't manage *) @@ -112,8 +105,8 @@ let l1 (a:Type) (b:Type) = | Prims.Left (MkR f0 g0 e) -> return_squash (MkC f0 g0 (fun _ -> e)) | Prims.Right nr -> - let f0 (x:pow a) (y:b) = false in - let g0 (x:pow b) (y:a) = false in + 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 f0 g0 (fun r x -> false_elim (f r)))) diff --git a/ulib/experimental/FStar.OrdSet.fst b/ulib/experimental/FStar.OrdSet.fst index 5a3bd3069ac..cffed4555ec 100644 --- a/ulib/experimental/FStar.OrdSet.fst +++ b/ulib/experimental/FStar.OrdSet.fst @@ -99,7 +99,7 @@ let rec insert' #_ #f x s = else if f x hd then x::hd::tl else hd::(insert' #_ #f x tl) -let rec distinct' #a f l : Tot (ordset a f) = +let rec distinct' #a (f: cmp a) (l: list a) : Tot (ordset a f) = match l with | [] -> [] | x::t -> insert' x (distinct' f t) diff --git a/ulib/legacy/FStar.Array.fsti b/ulib/legacy/FStar.Array.fsti index c91ef0cc33d..34d3a9345b2 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 -> array a -> heap -> Type0 +: heap -> st_post' (array a) True = fun h0 x h1 -> x `unused_in` h0 /\ contains h1 x /\ diff --git a/ulib/legacy/FStar.Relational.Comp.fst b/ulib/legacy/FStar.Relational.Comp.fst index 4e0a530a34a..2792c7ca126 100644 --- a/ulib/legacy/FStar.Relational.Comp.fst +++ b/ulib/legacy/FStar.Relational.Comp.fst @@ -42,7 +42,7 @@ let comp a b wp0 wp1 p h2 = (R?.l h2) //TODO: this should be conditional on the monotonicity of the wps -assume Monotone_comp: forall a b wp1 wp2 p1 p2. (forall x h. p1 x h ==> p2 x h) +assume Monotone_comp: forall a b wp1 wp2 (p1 p2: st_post_h heap2 (rel a b)). (forall x h. p1 x h ==> p2 x h) ==> (forall h. comp a b wp1 wp2 p1 h ==> comp a b wp1 wp2 p2 h) From 7a9ab00b00572721f6cb6d8da826a701c925f144 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 21:03:13 -0800 Subject: [PATCH 06/15] Finish ulib. --- ulib/FStar.HyperStack.All.fst | 2 +- ulib/FStar.Modifies.fst | 4 +-- ulib/FStar.Modifies.fsti | 2 +- ulib/FStar.ModifiesGen.fst | 34 +++++++++++++----------- ulib/FStar.Monotonic.DependentMap.fsti | 15 +++++------ ulib/FStar.Monotonic.Map.fst | 12 ++++----- ulib/FStar.Monotonic.Seq.fst | 6 ++--- ulib/LowStar.Endianness.fst | 16 +++++------ ulib/LowStar.Literal.fsti | 2 +- ulib/LowStar.Monotonic.Buffer.fst | 16 +++++------ ulib/LowStar.Monotonic.Buffer.fsti | 2 +- ulib/LowStar.PrefixFreezableBuffer.fsti | 4 +-- ulib/LowStar.RVector.fst | 2 +- ulib/LowStar.Vector.fst | 18 ++++++------- ulib/legacy/FStar.Buffer.Quantifiers.fst | 10 +++---- ulib/legacy/FStar.Pointer.Base.fst | 12 ++++----- 16 files changed, 79 insertions(+), 78 deletions(-) diff --git a/ulib/FStar.HyperStack.All.fst b/ulib/FStar.HyperStack.All.fst index c6dbcd68380..6d947680a03 100644 --- a/ulib/FStar.HyperStack.All.fst +++ b/ulib/FStar.HyperStack.All.fst @@ -25,7 +25,7 @@ new_effect ALL = ALL_h HyperStack.mem unfold let lift_state_all (a:Type) (wp:st_wp a) (p:all_post a) = wp (fun a -> p (V a)) sub_effect STATE ~> ALL = lift_state_all -unfold let lift_exn_all (a:Type) (wp:ex_wp a) (p:all_post a) (h:HyperStack.mem) = wp (fun ra -> p ra h) +unfold let lift_exn_all (a:Type) (wp:ex_wp a) : all_wp_h HyperStack.mem a = fun p h -> wp (fun ra -> p ra h) sub_effect EXN ~> ALL = lift_exn_all effect All (a:Type) (pre:all_pre) (post: (h0:HyperStack.mem -> Tot (all_post' a (pre h0)))) = diff --git a/ulib/FStar.Modifies.fst b/ulib/FStar.Modifies.fst index 106a2910789..7656c45b117 100644 --- a/ulib/FStar.Modifies.fst +++ b/ulib/FStar.Modifies.fst @@ -95,7 +95,7 @@ let loc_aux_includes_trans' (s3: loc_aux) : Lemma ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3) -= Classical.move_requires (loc_aux_includes_trans s1 s2) s3 += Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3 let loc_aux_disjoint_buffer (l: loc_aux) @@ -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 = MG.loc_disjoint +let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2 let loc_disjoint_sym = MG.loc_disjoint_sym diff --git a/ulib/FStar.Modifies.fsti b/ulib/FStar.Modifies.fsti index f4fab8c0f4c..bb45dbc91a4 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) -: GTot Type0 +: Type0 val loc_disjoint_sym (s1 s2: loc) diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst index 412343c3c23..f98c1fc5b8f 100644 --- a/ulib/FStar.ModifiesGen.fst +++ b/ulib/FStar.ModifiesGen.fst @@ -352,7 +352,7 @@ let loc_aux_includes_buffer_includes : Lemma (requires (loc_aux_includes_buffer s b1 /\ b1 `aloc_includes` b2)) (ensures (loc_aux_includes_buffer s b2)) -= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3)) += Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3)) let loc_aux_includes_loc_aux_includes_buffer (#al: aloc_t) (#c: cls al) @@ -361,7 +361,7 @@ let loc_aux_includes_loc_aux_includes_buffer : Lemma (requires (loc_aux_includes s1 s2 /\ loc_aux_includes_buffer s2 b)) (ensures (loc_aux_includes_buffer s1 b)) -= Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires (loc_aux_includes_buffer_includes #al #c s b1) b2) += Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires #_ #_ #(fun b2 -> loc_aux_includes_buffer s b2) (loc_aux_includes_buffer_includes #al #c s b1) b2) let loc_aux_includes_trans (#al: aloc_t) (#c: cls al) @@ -369,7 +369,7 @@ let loc_aux_includes_trans : Lemma (requires (loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3)) (ensures (loc_aux_includes s1 s3)) -= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3)) += Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3)) let addrs_of_loc_weak_loc_union (#al: aloc_t) (#c: cls al) @@ -590,7 +590,7 @@ let loc_aux_disjoint_loc_aux_includes (ensures (loc_aux_disjoint l1 l3)) = // FIXME: WHY WHY WHY do I need this assert? assert (forall (b1 b3: aloc c) . (GSet.mem b1 l1 /\ GSet.mem b3 l3) ==> (exists (b2: aloc c) . GSet.mem b2 l2 /\ aloc_disjoint b1 b2 /\ aloc_includes b2 b3)); - Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires (aloc_disjoint_includes #al #c b1 b2) b3) + Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires #_ #_ #(fun b3 -> aloc_disjoint b1 b3) (aloc_disjoint_includes #al #c b1 b2) b3) let loc_disjoint_includes #al #c p1 p2 p1' p2' = regions_of_loc_monotonic p1 p1'; @@ -1028,7 +1028,7 @@ let modifies_refl #al #c s h = let modifies_loc_includes #al #c s1 h h' s2 = assert (modifies_preserves_mreferences s1 h h'); Classical.forall_intro_2 (loc_aux_disjoint_sym #al #c); - Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3); + Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires #_ #_ #(fun l3 -> loc_aux_disjoint l1 l3) (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3); assert (modifies_preserves_alocs s1 h h') let modifies_preserves_liveness #al #c s1 s2 h h' #t #pre r = () @@ -1078,7 +1078,7 @@ let modifies_trans' : Lemma (requires (modifies s h1 h2 /\ modifies s h2 h3)) (ensures (modifies s h1 h3)) -= Classical.forall_intro_3 (fun r a b -> Classical.move_requires (c.aloc_preserved_trans #r #a b h1 h2) h3) += Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h3 -> c.aloc_preserved b h1 h3) (c.aloc_preserved_trans #r #a b h1 h2) h3) let modifies_trans #al #c s12 h1 h2 s23 h3 = let u = loc_union s12 s23 in @@ -1112,7 +1112,7 @@ let modifies_only_live_regions_weak )) (ensures (modifies l h h')) = assert (modifies_preserves_mreferences l h h'); // FIXME: WHY WHY WHY? - Classical.forall_intro_3 (fun r a b -> Classical.move_requires (addr_unused_in_aloc_preserved #al #c #r #a b h) h') + Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h2 -> c.aloc_preserved b h h2) (addr_unused_in_aloc_preserved #al #c #r #a b h) h') #pop-options (* Restrict a set of locations along a set of regions *) @@ -1184,6 +1184,7 @@ 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 @@ -1205,6 +1206,7 @@ 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 @@ -1543,7 +1545,7 @@ let modifies_only_not_unused_in #al #c l h h' = #push-options "--z3rlimit 20" let mreference_live_loc_not_unused_in #al c #t #pre h b = - Classical.move_requires (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b); + Classical.move_requires #_ #(fun ra -> does_not_contain_addr h ra) (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b); assert (~ (h `does_not_contain_addr` (HS.frameOf b, HS.as_addr b))); loc_addresses_not_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h; loc_includes_trans (loc_not_unused_in c h) (loc_freed_mreference b) (loc_mreference b); @@ -1552,7 +1554,7 @@ let mreference_live_loc_not_unused_in #al c #t #pre h b = #push-options "--z3cliopt 'smt.qi.eager_threshold=100'" let mreference_unused_in_loc_unused_in #al c #t #pre h b = - Classical.move_requires (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b); + Classical.move_requires #_ #_ #(fun ra -> does_not_contain_addr h ra) (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b); loc_addresses_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h; loc_includes_addresses_addresses c false true (HS.frameOf b) (Set.singleton (HS.as_addr b)) (Set.singleton (HS.as_addr b)); loc_includes_trans (loc_unused_in c h) (loc_freed_mreference b) (loc_mreference b); @@ -1872,7 +1874,7 @@ let union_loc_of_loc_includes_elim (x: aloc (c b)) : Lemma ((GSet.mem x auxs /\ (~ (GSet.mem x.addr (addrs_of_loc_weak smaller x.region)))) ==> g' r a x) - = Classical.move_requires (f r a) x + = Classical.move_requires #_ #_ #(fun x-> g' r a x) (f r a) x in Classical.forall_intro_3 f'; assert (forall (r: HS.rid) (a: nat) (x: aloc (c b)) . @@ -1894,8 +1896,8 @@ let union_loc_of_loc_includes_elim #pop-options let union_loc_of_loc_includes #al c b s1 s2 = - Classical.move_requires (union_loc_of_loc_includes_elim c b s1) s2; - Classical.move_requires (union_loc_of_loc_includes_intro c b s1) s2 + Classical.move_requires #_ #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_elim c b s1) s2; + Classical.move_requires #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_intro c b s1) s2 #push-options "--fuel 0 --ifuel 0" let union_loc_of_loc_disjoint_intro @@ -1977,8 +1979,8 @@ let union_loc_of_loc_disjoint_elim #pop-options let union_loc_of_loc_disjoint #al c b s1 s2 = - Classical.move_requires (union_loc_of_loc_disjoint_elim c b s1) s2; - Classical.move_requires (union_loc_of_loc_disjoint_intro c b s1) s2 + Classical.move_requires #_ #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_elim c b s1) s2; + Classical.move_requires #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_intro c b s1) s2 #push-options "--z3rlimit 32" let modifies_union_loc_of_loc_elim @@ -2065,8 +2067,8 @@ let modifies_union_loc_of_loc_intro #pop-options let modifies_union_loc_of_loc #al c b l h1 h2 = - Classical.move_requires (modifies_union_loc_of_loc_elim c b l h1) h2; - Classical.move_requires (modifies_union_loc_of_loc_intro c b l h1) h2 + Classical.move_requires #_ #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) #(fun h2 -> modifies l h1 h2) (modifies_union_loc_of_loc_elim c b l h1) h2; + Classical.move_requires #_ #(fun h2 -> modifies l h1 h2) #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) (modifies_union_loc_of_loc_intro c b l h1) h2 let loc_of_union_loc #al #c b l = let (Loc regions region_liveness_tags non_live_addrs live_addrs aux) = l in diff --git a/ulib/FStar.Monotonic.DependentMap.fsti b/ulib/FStar.Monotonic.DependentMap.fsti index 37d1b9a82af..76092efe6d8 100644 --- a/ulib/FStar.Monotonic.DependentMap.fsti +++ b/ulib/FStar.Monotonic.DependentMap.fsti @@ -96,9 +96,8 @@ let defined (#r:HST.erid) (t:t r a b inv) (x:a) - (h:HS.mem) - : GTot Type - = Some? (sel (HS.sel h t) x) + : HST.mem_predicate = fun (h:HS.mem) -> + Some? (sel (HS.sel h t) x) /// `fresh t x h`: The map is not defined at point `x` let fresh @@ -109,8 +108,8 @@ let fresh (t:t r a b inv) (x:a) (h:HS.mem) - : GTot Type0 - = ~ (defined t x h) + : HST.mem_predicate = fun (h:HS.mem) -> + ~ (defined t x h) /// `value_of t x h`: Get the value of `x` in the map `t` in state `h` let value_of @@ -133,9 +132,9 @@ let contains (t:t r a b inv) (x:a) (y:b x) - (h:HS.mem) - : GTot Type0 - = defined t x h /\ + : HST.mem_predicate + = fun (h:HS.mem) -> + defined t x h /\ value_of t x h == y /// `contains_stable`: The `contains` predicate is stable with respect to `grows` diff --git a/ulib/FStar.Monotonic.Map.fst b/ulib/FStar.Monotonic.Map.fst index 7fb705038dd..a71489665f1 100644 --- a/ulib/FStar.Monotonic.Map.fst +++ b/ulib/FStar.Monotonic.Map.fst @@ -63,13 +63,13 @@ let alloc (#r:rid) #a #b #inv ralloc_post r (empty_map a b) h0 x h1)) = ralloc r (empty_map a b) -let defined #r #a #b #inv (m:t r a b inv) (x:a) (h:HS.mem) - : GTot Type0 - = Some? (sel (HS.sel h m) x) +let defined #r #a #b #inv (m:t r a b inv) (x:a) + : HST.mem_predicate = fun (h:HS.mem) -> + Some? (sel (HS.sel h m) x) -let contains #r #a #b #inv (m:t r a b inv) (x:a) (y:b x) (h:HS.mem) - : GTot Type0 - = Some? (sel (HS.sel h m) x) /\ Some?.v (sel (HS.sel h m) x) == y +let contains #r #a #b #inv (m:t r a b inv) (x:a) (y:b x) + : HST.mem_predicate = fun (h:HS.mem) -> + Some? (sel (HS.sel h m) x) /\ Some?.v (sel (HS.sel h m) x) == y let value #r #a #b #inv (m:t r a b inv) (x:a) (h:HS.mem{defined m x h}) : GTot (r:b x{contains m x r h}) diff --git a/ulib/FStar.Monotonic.Seq.fst b/ulib/FStar.Monotonic.Seq.fst index 32040d0000b..ef924718e9e 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) (h:mem) = + (n:nat) (v:b) : HST.mem_predicate = fun h -> 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) (h:mem) = + (n:nat) (v:b) : HST.mem_predicate = fun (h:mem) -> let s = HS.sel h r in n < Seq.length (collect f s) /\ Seq.index (collect f s) n == v @@ -368,7 +368,7 @@ type log_t (i:rid) (a:Type) = m_rref i (seq a) grows let increases (x:int) (y:int) = b2t (x <= y) let at_most_log_len (#l:rid) (#a:Type) (x:nat) (log:log_t l a) - : mem -> GTot Type0 + : HST.mem_predicate = fun h -> x <= Seq.length (HS.sel h log) //Note: we may want int seqn, instead of nat seqn diff --git a/ulib/LowStar.Endianness.fst b/ulib/LowStar.Endianness.fst index 9b0af2d6caa..9743f3351bd 100644 --- a/ulib/LowStar.Endianness.fst +++ b/ulib/LowStar.Endianness.fst @@ -113,7 +113,7 @@ assume val store16_le_i (z:u16) : Stack unit (requires (store_pre b (U32.v i) 2 (fun s -> le_to_n s == U16.v z))) - (ensures (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z)) h0 r h1) assume val load16_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -131,7 +131,7 @@ assume val store16_be_i (z:u16) : Stack unit (requires (store_pre b (U32.v i) 2 (fun s -> be_to_n s == U16.v z))) - (ensures (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z)) h0 r h1) assume val load16_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -149,7 +149,7 @@ assume val store32_le_i (z:u32) : Stack unit (requires (store_pre b (U32.v i) 4 (fun s -> le_to_n s == U32.v z))) - (ensures (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z)) h0 r h1 ) assume val load32_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -167,7 +167,7 @@ assume val store32_be_i (z:u32) : Stack unit (requires (store_pre b (U32.v i) 4 (fun s -> be_to_n s == U32.v z))) - (ensures (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z)) h0 r h1 ) assume val load32_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -185,7 +185,7 @@ assume val store64_le_i (z:u64) : Stack unit (requires (store_pre b (U32.v i) 8 (fun s -> le_to_n s == U64.v z))) - (ensures (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z)) h0 r h1 ) assume val load64_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -203,7 +203,7 @@ assume val store64_be_i (z:u64) : Stack unit (requires (store_pre b (U32.v i) 8 (fun s -> be_to_n s == U64.v z))) - (ensures (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z)) h0 r h1 ) assume val load64_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -221,7 +221,7 @@ assume val store128_le_i (z:u128) : Stack unit (requires (store_pre b (U32.v i) 16 (fun s -> le_to_n s == U128.v z))) - (ensures (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z)) h0 r h1 ) assume val load128_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -239,7 +239,7 @@ assume val store128_be_i (z:u128) : Stack unit (requires (store_pre b (U32.v i) 16 (fun s -> be_to_n s == U128.v z))) - (ensures (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z))) + (ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z)) h0 r h1 ) assume val load128_be_i diff --git a/ulib/LowStar.Literal.fsti b/ulib/LowStar.Literal.fsti index 183e49ef519..abbaaf286b3 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 buffer_of_literal_post s) + (ensures fun h0 b h1 -> buffer_of_literal_post s h0 b h1) /// .. note:: /// diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst index 684ff260f0d..deddd649707 100644 --- a/ulib/LowStar.Monotonic.Buffer.fst +++ b/ulib/LowStar.Monotonic.Buffer.fst @@ -383,7 +383,7 @@ let ubuffer_preserved_intro ) ==> Seq.equal (Seq.slice (as_seq h b') (boff - U32.v idx) (boff - U32.v idx + blen)) (Seq.slice (as_seq h' b') (boff - U32.v idx) (boff - U32.v idx + blen)) ))))) - = Classical.move_requires (f0 t' rrel rel) b'; + = Classical.move_requires #_ #_ #(fun b' -> live h' b') (f0 t' rrel rel) b'; Classical.move_requires (f t' rrel rel) b' in Classical.forall_intro_4 g' @@ -899,10 +899,10 @@ let loc_includes_union_r' (loc_includes s (loc_union s1 s2) <==> (loc_includes s s1 /\ loc_includes s s2)) [SMTPat (loc_includes s (loc_union s1 s2))] = Classical.move_requires (loc_includes_union_r s s1) s2; - Classical.move_requires (loc_includes_union_l s1 s2) s1; - Classical.move_requires (loc_includes_union_l s1 s2) s2; - Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s1; - Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s2 + Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s1; + Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s2; + Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s1; + Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s2 let loc_includes_none = MG.loc_includes_none @@ -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 = MG.loc_disjoint +let loc_disjoint s1 s2 = MG.loc_disjoint s1 s2 let loc_disjoint_sym = MG.loc_disjoint_sym @@ -1456,13 +1456,13 @@ let fresh_frame_loc_not_unused_in_disjoint let live_loc_not_unused_in #_ #_ #_ b h = unused_in_equiv b h; - Classical.move_requires (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b); + Classical.move_requires #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b); MG.loc_addresses_not_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h; () let unused_in_loc_unused_in #_ #_ #_ b h = unused_in_equiv b h; - Classical.move_requires (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b); + Classical.move_requires #_ #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b); MG.loc_addresses_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h; () diff --git a/ulib/LowStar.Monotonic.Buffer.fsti b/ulib/LowStar.Monotonic.Buffer.fsti index 94e6961fe21..a1e1bd1c235 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) -: GTot Type0 +: Type0 val loc_disjoint_sym (s1 s2: loc) diff --git a/ulib/LowStar.PrefixFreezableBuffer.fsti b/ulib/LowStar.PrefixFreezableBuffer.fsti index 46ec82badc1..ab6e3eafb99 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 alloc_post_mem_common) + (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1) val malloc (r:HS.rid) (len:u32) : ST (b:lbuffer len{frameOf b == r /\ freeable b}) (requires fun _ -> malloc_pre r len) - (ensures alloc_post_mem_common) + (ensures fun h0 b h1 -> alloc_post_mem_common h0 b h1) 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/LowStar.RVector.fst b/ulib/LowStar.RVector.fst index 93e11cac701..6b38d83a170 100644 --- a/ulib/LowStar.RVector.fst +++ b/ulib/LowStar.RVector.fst @@ -74,7 +74,7 @@ val rs_elems_inv: i:nat -> j:nat{i <= j && j <= S.length rs} -> GTot Type0 let rs_elems_inv #a #rst rg h rs i j = - V.forall_seq rs i j (rg_inv rg h) + V.forall_seq rs i j (fun x -> rg_inv rg h x) val rv_elems_inv: #a:Type0 -> #rst:Type -> #rg:regional rst a -> diff --git a/ulib/LowStar.Vector.fst b/ulib/LowStar.Vector.fst index 802c6c4e92a..24e13950f81 100644 --- a/ulib/LowStar.Vector.fst +++ b/ulib/LowStar.Vector.fst @@ -514,7 +514,7 @@ let shrink #a vec new_size = val fold_left_seq: #a:Type -> #b:Type0 -> seq:S.seq a -> - f:(b -> a -> GTot b) -> ib:b -> + f:(b -> a -> Tot b) -> ib:b -> GTot b (decreases (S.length seq)) let rec fold_left_seq #a #b seq f ib = if S.length seq = 0 then ib @@ -549,7 +549,7 @@ let fold_left #a #b vec f ib = val forall_seq: #a:Type -> seq:S.seq a -> i:nat -> j:nat{i <= j && j <= S.length seq} -> - p:(a -> GTot Type0) -> GTot Type0 + p:(a -> Type0) -> GTot Type0 let forall_seq #a seq i j p = forall (idx:nat{i <= idx && idx < j}). p (S.index seq idx) @@ -557,7 +557,7 @@ let forall_seq #a seq i j p = val forall_buffer: #a:Type -> h:HS.mem -> buf:B.buffer a -> i:nat -> j:nat{i <= j && j <= B.length buf} -> - p:(a -> GTot Type0) -> GTot Type0 + p:(a -> Type0) -> GTot Type0 let forall_buffer #a h buf i j p = forall_seq (B.as_seq h buf) i j p @@ -577,7 +577,7 @@ let forall_all #a h vec p = val forall2_seq: #a:Type -> seq:S.seq a -> i:nat -> j:nat{i <= j && j <= S.length seq} -> - p:(a -> a -> GTot Type0) -> GTot Type0 + p:(a -> a -> Tot Type0) -> GTot Type0 let forall2_seq #a seq i j p = forall (k:nat{i <= k && k < j}) (l:nat{i <= l && l < j && k <> l}). p (S.index seq k) (S.index seq l) @@ -585,20 +585,20 @@ let forall2_seq #a seq i j p = val forall2_buffer: #a:Type -> h:HS.mem -> buf:B.buffer a -> i:nat -> j:nat{i <= j && j <= B.length buf} -> - p:(a -> a -> GTot Type0) -> GTot Type0 + p:(a -> a -> Tot Type0) -> GTot Type0 let forall2_buffer #a h buf i j p = forall2_seq (B.as_seq h buf) i j p val forall2: #a:Type -> h:HS.mem -> vec:vector a -> i:uint32_t -> j:uint32_t{i <= j && j <= size_of vec} -> - p:(a -> a -> GTot Type0) -> GTot Type0 + p:(a -> a -> Tot Type0) -> GTot Type0 let forall2 #a h vec i j p = forall2_seq (as_seq h vec) (U32.v i) (U32.v j) p val forall2_all: #a:Type -> h:HS.mem -> vec:vector a -> - p:(a -> a -> GTot Type0) -> GTot Type0 + p:(a -> a -> Tot Type0) -> GTot Type0 let forall2_all #a h vec p = forall2 h vec 0ul (size_of vec) p @@ -646,7 +646,7 @@ val forall_seq_ok: #a:Type -> seq:S.seq a -> i:nat -> j:nat{i <= j && j <= S.length seq} -> k:nat{i <= k && k < j} -> - p:(a -> GTot Type0) -> + p:(a -> Tot Type0) -> Lemma (requires (forall_seq seq i j p)) (ensures (p (S.index seq k))) let forall_seq_ok #a seq i j k p = () @@ -655,7 +655,7 @@ val forall2_seq_ok: #a:Type -> seq:S.seq a -> i:nat -> j:nat{i <= j && j <= S.length seq} -> k:nat{i <= k && k < j} -> l:nat{i <= l && l < j && k <> l} -> - p:(a -> a -> GTot Type0) -> + p:(a -> a -> Tot Type0) -> Lemma (requires (forall2_seq seq i j p)) (ensures (p (S.index seq k) (S.index seq l))) let forall2_seq_ok #a seq i j k l p = () diff --git a/ulib/legacy/FStar.Buffer.Quantifiers.fst b/ulib/legacy/FStar.Buffer.Quantifiers.fst index 783b9af7ffc..6a9287189a5 100644 --- a/ulib/legacy/FStar.Buffer.Quantifiers.fst +++ b/ulib/legacy/FStar.Buffer.Quantifiers.fst @@ -35,7 +35,7 @@ let lemma_sub_quantifiers #a h b b' i len = let lemma_post (j:nat) = j < length b' ==> get h b' j == get h b (j + v i) in let qj : j:nat -> Lemma (lemma_post j) = fun j -> assert (j < v len ==> Seq.index (as_seq h b') j == Seq.index (as_seq h b) (j + v i)) in - Classical.forall_intro #_ #lemma_post qj + Classical.forall_intro #_ #(fun x -> lemma_post x) qj val lemma_offset_quantifiers: #a:Type -> h:mem -> b:buffer a -> b':buffer a -> i:FStar.UInt32.t{v i <= length b} -> Lemma (requires (live h b /\ live h b' /\ Seq.slice (as_seq h b) (v i) (length b) == as_seq h b')) @@ -56,7 +56,7 @@ let lemma_create_quantifiers #a h b init len = let lemma_post (i:nat) = i < length b ==> get h b i == init in let qi : i:nat -> Lemma (lemma_post i) = fun i -> assert (i < length b ==> get h b i == Seq.index (as_seq h b) i) in - Classical.forall_intro #_ #lemma_post qi + Classical.forall_intro #_ #(fun x -> lemma_post x) qi val lemma_index_quantifiers: #a:Type -> h:mem -> b:buffer a -> n:FStar.UInt32.t -> Lemma (requires (live h b /\ v n < length b)) @@ -101,8 +101,8 @@ let lemma_blit_quantifiers #a h0 h1 b bi b' bi' len = ==> Seq.index (Seq.slice (as_seq h1 b') (v bi'+v len) (length b')) (j - (v bi'+v len)) == Seq.index (Seq.slice (as_seq h0 b') (v bi'+v len) (length b')) (j - (v bi'+v len))) in - Classical.forall_intro #_ #lemma_post_1 qj_1; - Classical.forall_intro #_ #lemma_post_2 qj_2 + Classical.forall_intro #_ #(fun x -> lemma_post_1 x) qj_1; + Classical.forall_intro #_ #(fun x -> lemma_post_2 x) qj_2 (* Equality predicate between buffers with quantifiers *) @@ -116,4 +116,4 @@ let eq_lemma #a h b h' b' = let lemma_post (j:nat) = j < length b ==> get h b j == get h' b' j in let qj : j:nat -> Lemma (lemma_post j) = fun j -> assert(j < length b ==> Seq.index (as_seq h b) j == Seq.index (as_seq h' b') j) in - Classical.forall_intro #_ #lemma_post qj + Classical.forall_intro #_ #(fun x -> lemma_post x) qj diff --git a/ulib/legacy/FStar.Pointer.Base.fst b/ulib/legacy/FStar.Pointer.Base.fst index adb2e570a31..7075aa564ae 100644 --- a/ulib/legacy/FStar.Pointer.Base.fst +++ b/ulib/legacy/FStar.Pointer.Base.fst @@ -3214,8 +3214,8 @@ let disjoint_sym' (requires True) (ensures (disjoint p1 p2 <==> disjoint p2 p1)) [SMTPat (disjoint p1 p2)] -= FStar.Classical.move_requires (disjoint_sym #value1 #value2 p1) p2; - FStar.Classical.move_requires (disjoint_sym #value2 #value1 p2) p1 += FStar.Classical.move_requires #_ #(fun p2 -> disjoint p1 p2) (disjoint_sym #value1 #value2 p1) p2; + FStar.Classical.move_requires #_ #(fun p1 -> disjoint p2 p1) (disjoint_sym #value2 #value1 p2) p1 let disjoint_sym'' (value1: typ) @@ -3407,7 +3407,7 @@ let loc_aux_includes_trans' (s3: loc_aux) : Lemma ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3) -= Classical.move_requires (loc_aux_includes_trans s1 s2) s3 += Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3 (* Disjointness of two memory locations *) @@ -3605,7 +3605,7 @@ let disjoint_not_self (p: pointer t) : Lemma (disjoint p p ==> False) -= Classical.move_requires (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p) += Classical.move_requires #_ #(fun p2 -> path_disjoint (Pointer?.p p) p2) (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p) let loc_aux_in_addr (l: loc_aux) @@ -3812,12 +3812,12 @@ let modifies_buffer_elim' #t1 b p h h' = assert (n > 0); let pre (i: UInt32.t) - : GTot Type0 + : Tot Type0 = UInt32.v i < n in let post (i: UInt32.t) - : GTot Type0 + : Tot Type0 = pre i /\ ( let q = gpointer_of_buffer_cell b i in equal_values h q h' q From 168762a60d78583451ac99566c8732e5fedfef3a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 21:17:14 -0800 Subject: [PATCH 07/15] Allow cross-effect subtyping in MLish --- src/typechecker/FStarC.TypeChecker.Rel.fst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index f4ebf67aa1c..d7b728e71b6 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -4031,7 +4031,7 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = c1 |> U.comp_effect_name |> Env.norm_eff_name env, c2 |> U.comp_effect_name |> Env.norm_eff_name env in - if not (Ident.lid_equals eff1 eff2) then + if not (Options.ml_ish () || Ident.lid_equals eff1 eff2) then giveup wl (Thunk.mk fun _ -> "computation type mismatch in arrow: " ^ string_of_lid eff1 ^ " vs " ^ string_of_lid eff2) orig else From b1e5a5ff171e52011cb8790ba2228192ab0ed040 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 7 Jan 2025 21:42:13 -0800 Subject: [PATCH 08/15] Compare effect names after partial application. --- src/typechecker/FStarC.TypeChecker.Rel.fst | 20 +++++++++----------- ulib/FStar.Pervasives.fsti | 2 +- ulib/FStar.SquashProperties.fst | 2 +- 3 files changed, 11 insertions(+), 13 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index d7b728e71b6..9602cb7c680 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -4026,6 +4026,13 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = solve_one_universe_eq orig u1 u2 wl | Tm_arrow {bs=bs1; comp=c1}, Tm_arrow {bs=bs2; comp=c2} -> + let mk_c c = function + | [] -> c + | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in + + let (bs1, c1), (bs2, c2) = + match_num_binders (bs1, mk_c c1) (bs2, mk_c c2) in + let eff1, eff2 = let env = p_env wl orig in c1 |> U.comp_effect_name |> Env.norm_eff_name env, @@ -4033,18 +4040,9 @@ and solve_t' (problem:tprob) (wl:worklist) : solution = if not (Options.ml_ish () || Ident.lid_equals eff1 eff2) then giveup wl (Thunk.mk fun _ -> "computation type mismatch in arrow: " ^ string_of_lid eff1 ^ " vs " ^ string_of_lid eff2) orig - else - - let mk_c c = function - | [] -> c - | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in - - let (bs1, c1), (bs2, c2) = - match_num_binders (bs1, mk_c c1) (bs2, mk_c c2) in - - solve_binders bs1 bs2 orig wl - (fun wl scope subst -> + solve_binders bs1 bs2 orig wl + (fun wl scope subst -> let c1 = Subst.subst_comp subst c1 in let c2 = Subst.subst_comp subst c2 in //open both comps let rel = if (Options.use_eq_at_higher_order()) then EQ else problem.relation in diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index bd624178796..d49c5ed642d 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -544,7 +544,7 @@ let ex_wp (a: Type) = ex_post a -> GTot ex_pre (** Returning a value [x] normally promotes it to the [V x] result *) unfold -let ex_return (a: Type) (x: a) (p: ex_post a) : GTot Type0 = p (V x) +let ex_return (a: Type) (x: a) : GTot (ex_wp a) = fun p -> p (V x) (** Sequential composition of exception-raising code requires case analysing the result of the first computation before "running" the second one *) diff --git a/ulib/FStar.SquashProperties.fst b/ulib/FStar.SquashProperties.fst index fb9a54a5daf..c081a4de7a2 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 f0 g0 (fun r x -> false_elim (f r)))) + MkC (fun x y -> f0 x y) (fun x y -> g0 x y) (fun r x -> false_elim (f r)))) (* The paradoxical set *) type u = p:Type -> Tot (squash (pow p)) From 514ffdf63bf372f034069d213f5c8ce934dd6bbe Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 8 Jan 2025 12:59:38 -0800 Subject: [PATCH 09/15] When solving `?u x = rhs x`, check for compatible effects. --- src/typechecker/FStarC.TypeChecker.Rel.fst | 19 ++++++++++++++++++- ulib/FStar.Monotonic.DependentMap.fsti | 10 +++++----- 2 files changed, 23 insertions(+), 6 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index 9602cb7c680..ae7b446488e 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -2959,9 +2959,26 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) bs, S.mk_Tm_app rhs_hd rhs_args rhs.pos in + // We need to check that `?u` and `rhs` have compatible effects + let compatible_effs () = + let env = { env with admit=true; expected_typ=None } in + let get_eff ty = + match (SS.compress ty).n with + | Tm_arrow {bs=bs'; comp=c'} when List.length bs' = List.length bs -> + Some (c' |> U.comp_effect_name |> Env.norm_eff_name env) + | Tm_arrow {bs=bs'; comp=c'} when List.length bs' > List.length bs -> + Some PC.effect_Tot_lid + | _ -> None in + let t_rhs, _ = env.typeof_well_typed_tot_or_gtot_term env rhs false in + let eff_rhs = get_eff t_rhs in + let eff_u = get_eff (U.ctx_uvar_typ ctx_u) in + match eff_u, eff_rhs with + | Some eff_u, Some eff_rhs -> lid_equals eff_u eff_rhs + | _ -> false + in let sol = match bs with - | [] -> rhs + | [] when compatible_effs () -> rhs | _ -> u_abs (U.ctx_uvar_typ ctx_u) (sn_binders env bs) rhs in [TERM(ctx_u, sol)] diff --git a/ulib/FStar.Monotonic.DependentMap.fsti b/ulib/FStar.Monotonic.DependentMap.fsti index 76092efe6d8..9428dd111f9 100644 --- a/ulib/FStar.Monotonic.DependentMap.fsti +++ b/ulib/FStar.Monotonic.DependentMap.fsti @@ -29,7 +29,7 @@ let partial_dependent_map (a:eqtype) (b:a -> Type) = DM.t a (opt b) /// An empty partial, dependent map maps all keys to None -let empty_partial_dependent_map (#a:_) (#b:_) +let empty_partial_dependent_map (#a:eqtype) (#b:_) : partial_dependent_map a b = DM.create #a #(opt b) (fun x -> None) //////////////////////////////////////////////////////////////////////////////// @@ -45,16 +45,16 @@ val map : Type u#b /// `repr m`: A ghost function that reveals the internal `map` as a `DM.t` -val repr (#a:_) (#b:_) +val repr (#a:eqtype) (#b:_) (r:map a b) : GTot (partial_dependent_map a b) /// An `empty : map a b` is equivalent to the `empty_partial_dependent_map` -val empty (#a:_) (#b:_) +val empty (#a:eqtype) (#b:_) : r:map a b{repr r == empty_partial_dependent_map} /// Selecting a key from a map `sel r x` is equivalent to selecting it from its `repr` -val sel (#a:_) (#b:_) +val sel (#a:eqtype) (#b:_) (r:map a b) (x:a) : Pure (option (b x)) @@ -62,7 +62,7 @@ val sel (#a:_) (#b:_) (ensures (fun o -> DM.sel (repr r) x == o)) /// Updating a map using `upd r x v` is equivalent to updating its repr -val upd (#a:_) (#b:_) +val upd (#a:eqtype) (#b:_) (r:map a b) (x:a) (v:b x) From 08f6d105ccdfe1ab8c25c560a6df73df8ffae163 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 11:31:23 -0800 Subject: [PATCH 10/15] Revert unnecessary ulib changes. --- ulib/FStar.HyperStack.ST.fsti | 19 ++++++++++--------- ulib/LowStar.Endianness.fst | 16 ++++++++-------- 2 files changed, 18 insertions(+), 17 deletions(-) diff --git a/ulib/FStar.HyperStack.ST.fsti b/ulib/FStar.HyperStack.ST.fsti index 41abbe1ac8c..893f7186e0a 100644 --- a/ulib/FStar.HyperStack.ST.fsti +++ b/ulib/FStar.HyperStack.ST.fsti @@ -324,6 +324,7 @@ val pop_frame (_:unit) #push-options "--z3rlimit 40" let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem) (s:mreference a rel{is_stack_region (frameOf s)}) (m1:mem) + : GTot prop = is_stack_region (get_tip m0) /\ Map.domain (get_hmap m0) == Map.domain (get_hmap m1) /\ get_tip m0 == get_tip m1 /\ @@ -337,14 +338,14 @@ let salloc_post (#a:Type) (#rel:preorder a) (init:a) (m0:mem) *) val salloc (#a:Type) (#rel:preorder a) (init:a) :StackInline (mstackref a rel) (requires (fun m -> is_stack_region (get_tip m))) - (ensures fun m0 r m1 -> salloc_post init m0 r m1) + (ensures salloc_post init) // JP, AR: these are not supported in C, and `salloc` already benefits from // automatic memory management. [@@ (deprecated "Use salloc instead") ] val salloc_mm (#a:Type) (#rel:preorder a) (init:a) :StackInline (mmmstackref a rel) (requires (fun m -> is_stack_region (get_tip m))) - (ensures fun m0 r m1 -> salloc_post init m0 r m1) + (ensures salloc_post init) [@@ (deprecated "Use salloc instead") ] val sfree (#a:Type) (#rel:preorder a) (r:mmmstackref a rel) @@ -378,7 +379,7 @@ val new_colored_region (r0:rid) (c:int) (r1, m1) == HS.new_eternal_region m0 r0 (Some c))) let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem) - (x:mreference a rel) (m1:mem) = + (x:mreference a rel) (m1:mem) : GTot prop = let region_i = get_hmap m0 `Map.sel` i in as_ref x `Heap.unused_in` region_i /\ i `is_in` get_hmap m0 /\ @@ -387,11 +388,11 @@ let ralloc_post (#a:Type) (#rel:preorder a) (i:rid) (init:a) (m0:mem) val ralloc (#a:Type) (#rel:preorder a) (i:rid) (init:a) :ST (mref a rel) (requires (fun m -> is_eternal_region i)) - (ensures fun m0 r m1 -> ralloc_post i init m0 r m1) + (ensures (ralloc_post i init)) val ralloc_mm (#a:Type) (#rel:preorder a) (i:rid) (init:a) :ST (mmmref a rel) (requires (fun m -> is_eternal_region i)) - (ensures fun m0 r m1 -> ralloc_post i init m0 r m1) + (ensures (ralloc_post i init)) (* * AR: 12/26: For a ref to be readable/writable/free-able, @@ -408,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) = +unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m0:mem) (_:unit) (m1:mem) : GTot prop = m0 `contains` r /\ m1 == HyperStack.upd m0 r v (** @@ -417,9 +418,9 @@ unfold let assign_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (v:a) (m *) 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 fun m0 _ m1 -> assign_post r v m0 () m1) + (ensures (assign_post r v)) -unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) = +unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) (x:a) (m1:mem) : GTot prop = m1 == m0 /\ m0 `contains` r /\ x == HyperStack.sel m0 r (** @@ -428,7 +429,7 @@ unfold let deref_post (#a:Type) (#rel:preorder a) (r:mreference a rel) (m0:mem) *) val op_Bang (#a:Type) (#rel:preorder a) (r:mreference a rel) :Stack a (requires (fun m -> r `is_live_for_rw_in` m)) - (ensures fun m0 x m1 -> deref_post r m0 x m1) + (ensures (deref_post r)) let modifies_none (h0:mem) (h1:mem) = modifies Set.empty h0 h1 diff --git a/ulib/LowStar.Endianness.fst b/ulib/LowStar.Endianness.fst index 9743f3351bd..9b0af2d6caa 100644 --- a/ulib/LowStar.Endianness.fst +++ b/ulib/LowStar.Endianness.fst @@ -113,7 +113,7 @@ assume val store16_le_i (z:u16) : Stack unit (requires (store_pre b (U32.v i) 2 (fun s -> le_to_n s == U16.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z)) h0 r h1) + (ensures (store_post b (U32.v i) 2 (fun s -> le_to_n s == U16.v z))) assume val load16_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -131,7 +131,7 @@ assume val store16_be_i (z:u16) : Stack unit (requires (store_pre b (U32.v i) 2 (fun s -> be_to_n s == U16.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z)) h0 r h1) + (ensures (store_post b (U32.v i) 2 (fun s -> be_to_n s == U16.v z))) assume val load16_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -149,7 +149,7 @@ assume val store32_le_i (z:u32) : Stack unit (requires (store_pre b (U32.v i) 4 (fun s -> le_to_n s == U32.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 4 (fun s -> le_to_n s == U32.v z))) assume val load32_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -167,7 +167,7 @@ assume val store32_be_i (z:u32) : Stack unit (requires (store_pre b (U32.v i) 4 (fun s -> be_to_n s == U32.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 4 (fun s -> be_to_n s == U32.v z))) assume val load32_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -185,7 +185,7 @@ assume val store64_le_i (z:u64) : Stack unit (requires (store_pre b (U32.v i) 8 (fun s -> le_to_n s == U64.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 8 (fun s -> le_to_n s == U64.v z))) assume val load64_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -203,7 +203,7 @@ assume val store64_be_i (z:u64) : Stack unit (requires (store_pre b (U32.v i) 8 (fun s -> be_to_n s == U64.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 8 (fun s -> be_to_n s == U64.v z))) assume val load64_be_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -221,7 +221,7 @@ assume val store128_le_i (z:u128) : Stack unit (requires (store_pre b (U32.v i) 16 (fun s -> le_to_n s == U128.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 16 (fun s -> le_to_n s == U128.v z))) assume val load128_le_i (#rrel #rel:MB.srel u8) (b:MB.mbuffer u8 rrel rel) @@ -239,7 +239,7 @@ assume val store128_be_i (z:u128) : Stack unit (requires (store_pre b (U32.v i) 16 (fun s -> be_to_n s == U128.v z))) - (ensures fun h0 r h1 -> (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z)) h0 r h1 ) + (ensures (store_post b (U32.v i) 16 (fun s -> be_to_n s == U128.v z))) assume val load128_be_i From 60deb2cc0dcb62249adf31a21cabadaa7c81ec6e Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 16:50:18 -0800 Subject: [PATCH 11/15] Eta-expand unification solutions. --- src/typechecker/FStarC.TypeChecker.Rel.fst | 64 ++++++++++++++++------ 1 file changed, 47 insertions(+), 17 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index ae7b446488e..77938a5862a 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -2150,6 +2150,44 @@ let has_typeclass_constraint (u:ctx_uvar) (wl:worklist) : bool = wl.typeclass_variables |> for_any (fun v -> UF.equiv v.ctx_uvar_head u.ctx_uvar_head) +let maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term = + let norm = N.normalize [Env.Primops; Env.HNF; Env.Beta; Env.Eager_unfolding; Env.Unascribe; Env.Unrefine] env in + let t_e = norm t_e in + let t_expected = norm t_expected in + if !dbg_Rel then BU.print2 "t_e=%s t_exp=%s\n" (show t_e) (show t_expected); + let rec aux e t_e t_expected = + match (SS.compress t_e).n, (SS.compress t_expected).n with + | Tm_arrow {bs=bs_e; comp=c_e}, Tm_arrow {bs=bs_exp; comp=c_exp} -> + let mk_c c = function + | [] -> c + | bs -> mk_Total(mk (Tm_arrow {bs; comp=c}) c.pos) in + let (bs_e, c_e), (bs_exp, c_exp) = + match_num_binders (bs_e, mk_c c_e) (bs_exp, mk_c c_exp) in + let bs_e, c_e = SS.open_comp bs_e c_e in + let bs_exp, c_exp = SS.open_comp bs_exp c_exp in + let bs_exp, as_exp = U.args_of_binders bs_exp in + let e' = U.mk_app e as_exp in + let return e' = Some (U.abs bs_exp e' (Some (U.residual_comp_of_comp c_exp))) in + begin match aux e' (U.comp_result c_e) (U.comp_result c_exp) with + | Some e' -> return e' + | None -> + let eff_e, eff_exp = + c_e |> U.comp_effect_name |> Env.norm_eff_name env, + c_exp |> U.comp_effect_name |> Env.norm_eff_name env in + if lid_equals eff_e eff_exp then + None + else + return e' + end + | _, _ -> None + in + aux e t_e t_expected + +let eta_expand_fun env (e t_e t_expected: term) : term = + match maybe_eta_expand_fun env e t_e t_expected with + | None -> e + | Some e -> e + (* This function returns true for those lazykinds that are "complete" in the sense that unfolding them does not lose any information. For instance, embedded universes @@ -2915,7 +2953,6 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) *) let mk_solution env (lhs:flex_t) (bs:binders) (rhs:term) = let bs_orig = bs in - let rhs_orig = rhs in let (Flex (_, ctx_u, args)) = lhs in let bs, rhs = let bv_not_free_in_arg x arg = @@ -2959,26 +2996,19 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) bs, S.mk_Tm_app rhs_hd rhs_args rhs.pos in - // We need to check that `?u` and `rhs` have compatible effects - let compatible_effs () = + let rhs = let env = { env with admit=true; expected_typ=None } in - let get_eff ty = - match (SS.compress ty).n with - | Tm_arrow {bs=bs'; comp=c'} when List.length bs' = List.length bs -> - Some (c' |> U.comp_effect_name |> Env.norm_eff_name env) - | Tm_arrow {bs=bs'; comp=c'} when List.length bs' > List.length bs -> - Some PC.effect_Tot_lid - | _ -> None in + let t_u, _ = + let Flex (lhs, _, _) = lhs in + let lhs_hd, _ = U.head_and_args lhs in + env.typeof_well_typed_tot_or_gtot_term env (U.mk_app lhs_hd (U.args_of_non_null_binders bs)) false in let t_rhs, _ = env.typeof_well_typed_tot_or_gtot_term env rhs false in - let eff_rhs = get_eff t_rhs in - let eff_u = get_eff (U.ctx_uvar_typ ctx_u) in - match eff_u, eff_rhs with - | Some eff_u, Some eff_rhs -> lid_equals eff_u eff_rhs - | _ -> false - in + if !dbg_Rel then BU.print2 "t_rhs=%s t_u=%s\n" (show t_rhs) (show t_u); + eta_expand_fun env rhs t_rhs t_u in + if !dbg_Rel then BU.print1 "rhs_eta=%s\n" (show rhs); let sol = match bs with - | [] when compatible_effs () -> rhs + | [] -> rhs | _ -> u_abs (U.ctx_uvar_typ ctx_u) (sn_binders env bs) rhs in [TERM(ctx_u, sol)] From abd7d4e324b0d49ef8f39427cb7a1a762b6ec640 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 16:57:36 -0800 Subject: [PATCH 12/15] Revert unnecessary changes to ulib. --- ulib/FStar.Classical.fst | 4 ++-- ulib/FStar.Classical.fsti | 4 ++-- ulib/FStar.Modifies.fst | 2 +- ulib/FStar.ModifiesGen.fst | 32 +++++++++++++------------- ulib/FStar.Tactics.V1.Logic.Lemmas.fst | 2 +- ulib/LowStar.Monotonic.Buffer.fst | 14 +++++------ ulib/legacy/FStar.Pointer.Base.fst | 8 +++---- 7 files changed, 33 insertions(+), 33 deletions(-) diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst index 0befaf76327..026702d4a1d 100644 --- a/ulib/FStar.Classical.fst +++ b/ulib/FStar.Classical.fst @@ -115,10 +115,10 @@ let forall_intro_2 #a #b #p f = let forall_intro_2_with_pat #a #b #c #p pat f = forall_intro_2 #a #b #p f let forall_intro_3 #a #b #c #p f = - let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 #_ #_ #(fun y z -> p x y z) (f x) in + let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 (f x) in forall_intro g -let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #(fun x y z -> p x y z) f +let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c f let forall_intro_4 #a #b #c #d #p f = let g: x: a -> Lemma (forall (y: b x) (z: c x y) (w: d x y z). p x y z w) = diff --git a/ulib/FStar.Classical.fsti b/ulib/FStar.Classical.fsti index f0947bad3e8..e58b28d8b03 100644 --- a/ulib/FStar.Classical.fsti +++ b/ulib/FStar.Classical.fsti @@ -321,7 +321,7 @@ val forall_intro_4 TODO: Seems overly specific; could be removed? *) val forall_impl_intro (#a: Type) - (#p #q: (a -> Type)) + (#p #q: (a -> GTot Type)) ($_: (x: a -> squash (p x) -> Lemma (q x))) : Lemma (forall x. p x ==> q x) @@ -331,7 +331,7 @@ val forall_impl_intro *) val ghost_lemma (#a: Type) - (#p: (a -> Type0)) + (#p: (a -> GTot Type0)) (#q: (a -> unit -> GTot Type0)) ($_: (x: a -> Lemma (requires p x) (ensures (q x ())))) : Lemma (forall (x: a). p x ==> q x ()) diff --git a/ulib/FStar.Modifies.fst b/ulib/FStar.Modifies.fst index 7656c45b117..f3a08375b0b 100644 --- a/ulib/FStar.Modifies.fst +++ b/ulib/FStar.Modifies.fst @@ -95,7 +95,7 @@ let loc_aux_includes_trans' (s3: loc_aux) : Lemma ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3) -= Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3 += Classical.move_requires (loc_aux_includes_trans s1 s2) s3 let loc_aux_disjoint_buffer (l: loc_aux) diff --git a/ulib/FStar.ModifiesGen.fst b/ulib/FStar.ModifiesGen.fst index f98c1fc5b8f..dbbf9505fc4 100644 --- a/ulib/FStar.ModifiesGen.fst +++ b/ulib/FStar.ModifiesGen.fst @@ -352,7 +352,7 @@ let loc_aux_includes_buffer_includes : Lemma (requires (loc_aux_includes_buffer s b1 /\ b1 `aloc_includes` b2)) (ensures (loc_aux_includes_buffer s b2)) -= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3)) += Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3)) let loc_aux_includes_loc_aux_includes_buffer (#al: aloc_t) (#c: cls al) @@ -361,7 +361,7 @@ let loc_aux_includes_loc_aux_includes_buffer : Lemma (requires (loc_aux_includes s1 s2 /\ loc_aux_includes_buffer s2 b)) (ensures (loc_aux_includes_buffer s1 b)) -= Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires #_ #_ #(fun b2 -> loc_aux_includes_buffer s b2) (loc_aux_includes_buffer_includes #al #c s b1) b2) += Classical.forall_intro_3 (fun s b1 b2 -> Classical.move_requires (loc_aux_includes_buffer_includes #al #c s b1) b2) let loc_aux_includes_trans (#al: aloc_t) (#c: cls al) @@ -369,7 +369,7 @@ let loc_aux_includes_trans : Lemma (requires (loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3)) (ensures (loc_aux_includes s1 s3)) -= Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires #_ #_ #(fun x3 -> c.aloc_includes b1 x3) (c.aloc_includes_trans #r #a b1 b2) b3)) += Classical.forall_intro_3 (fun r a b1 -> Classical.forall_intro_2 (fun b2 b3 -> Classical.move_requires (c.aloc_includes_trans #r #a b1 b2) b3)) let addrs_of_loc_weak_loc_union (#al: aloc_t) (#c: cls al) @@ -590,7 +590,7 @@ let loc_aux_disjoint_loc_aux_includes (ensures (loc_aux_disjoint l1 l3)) = // FIXME: WHY WHY WHY do I need this assert? assert (forall (b1 b3: aloc c) . (GSet.mem b1 l1 /\ GSet.mem b3 l3) ==> (exists (b2: aloc c) . GSet.mem b2 l2 /\ aloc_disjoint b1 b2 /\ aloc_includes b2 b3)); - Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires #_ #_ #(fun b3 -> aloc_disjoint b1 b3) (aloc_disjoint_includes #al #c b1 b2) b3) + Classical.forall_intro_3 (fun b1 b2 b3 -> Classical.move_requires (aloc_disjoint_includes #al #c b1 b2) b3) let loc_disjoint_includes #al #c p1 p2 p1' p2' = regions_of_loc_monotonic p1 p1'; @@ -1028,7 +1028,7 @@ let modifies_refl #al #c s h = let modifies_loc_includes #al #c s1 h h' s2 = assert (modifies_preserves_mreferences s1 h h'); Classical.forall_intro_2 (loc_aux_disjoint_sym #al #c); - Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires #_ #_ #(fun l3 -> loc_aux_disjoint l1 l3) (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3); + Classical.forall_intro_3 (fun l1 l2 l3 -> Classical.move_requires (loc_aux_disjoint_loc_aux_includes #al #c l1 l2) l3); assert (modifies_preserves_alocs s1 h h') let modifies_preserves_liveness #al #c s1 s2 h h' #t #pre r = () @@ -1078,7 +1078,7 @@ let modifies_trans' : Lemma (requires (modifies s h1 h2 /\ modifies s h2 h3)) (ensures (modifies s h1 h3)) -= Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h3 -> c.aloc_preserved b h1 h3) (c.aloc_preserved_trans #r #a b h1 h2) h3) += Classical.forall_intro_3 (fun r a b -> Classical.move_requires (c.aloc_preserved_trans #r #a b h1 h2) h3) let modifies_trans #al #c s12 h1 h2 s23 h3 = let u = loc_union s12 s23 in @@ -1112,7 +1112,7 @@ let modifies_only_live_regions_weak )) (ensures (modifies l h h')) = assert (modifies_preserves_mreferences l h h'); // FIXME: WHY WHY WHY? - Classical.forall_intro_3 (fun r a b -> Classical.move_requires #_ #_ #(fun h2 -> c.aloc_preserved b h h2) (addr_unused_in_aloc_preserved #al #c #r #a b h) h') + Classical.forall_intro_3 (fun r a b -> Classical.move_requires (addr_unused_in_aloc_preserved #al #c #r #a b h) h') #pop-options (* Restrict a set of locations along a set of regions *) @@ -1545,7 +1545,7 @@ let modifies_only_not_unused_in #al #c l h h' = #push-options "--z3rlimit 20" let mreference_live_loc_not_unused_in #al c #t #pre h b = - Classical.move_requires #_ #(fun ra -> does_not_contain_addr h ra) (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b); + Classical.move_requires (does_not_contain_addr_addr_unused_in h) (HS.frameOf b, HS.as_addr b); assert (~ (h `does_not_contain_addr` (HS.frameOf b, HS.as_addr b))); loc_addresses_not_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h; loc_includes_trans (loc_not_unused_in c h) (loc_freed_mreference b) (loc_mreference b); @@ -1554,7 +1554,7 @@ let mreference_live_loc_not_unused_in #al c #t #pre h b = #push-options "--z3cliopt 'smt.qi.eager_threshold=100'" let mreference_unused_in_loc_unused_in #al c #t #pre h b = - Classical.move_requires #_ #_ #(fun ra -> does_not_contain_addr h ra) (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b); + Classical.move_requires (addr_unused_in_does_not_contain_addr h) (HS.frameOf b, HS.as_addr b); loc_addresses_unused_in c (HS.frameOf b) (Set.singleton (HS.as_addr b)) h; loc_includes_addresses_addresses c false true (HS.frameOf b) (Set.singleton (HS.as_addr b)) (Set.singleton (HS.as_addr b)); loc_includes_trans (loc_unused_in c h) (loc_freed_mreference b) (loc_mreference b); @@ -1874,7 +1874,7 @@ let union_loc_of_loc_includes_elim (x: aloc (c b)) : Lemma ((GSet.mem x auxs /\ (~ (GSet.mem x.addr (addrs_of_loc_weak smaller x.region)))) ==> g' r a x) - = Classical.move_requires #_ #_ #(fun x-> g' r a x) (f r a) x + = Classical.move_requires (f r a) x in Classical.forall_intro_3 f'; assert (forall (r: HS.rid) (a: nat) (x: aloc (c b)) . @@ -1896,8 +1896,8 @@ let union_loc_of_loc_includes_elim #pop-options let union_loc_of_loc_includes #al c b s1 s2 = - Classical.move_requires #_ #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_elim c b s1) s2; - Classical.move_requires #_ #(fun s2 -> loc_includes s1 s2) (union_loc_of_loc_includes_intro c b s1) s2 + Classical.move_requires (union_loc_of_loc_includes_elim c b s1) s2; + Classical.move_requires (union_loc_of_loc_includes_intro c b s1) s2 #push-options "--fuel 0 --ifuel 0" let union_loc_of_loc_disjoint_intro @@ -1979,8 +1979,8 @@ let union_loc_of_loc_disjoint_elim #pop-options let union_loc_of_loc_disjoint #al c b s1 s2 = - Classical.move_requires #_ #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_elim c b s1) s2; - Classical.move_requires #_ #(fun s2 -> loc_disjoint s1 s2) (union_loc_of_loc_disjoint_intro c b s1) s2 + Classical.move_requires (union_loc_of_loc_disjoint_elim c b s1) s2; + Classical.move_requires (union_loc_of_loc_disjoint_intro c b s1) s2 #push-options "--z3rlimit 32" let modifies_union_loc_of_loc_elim @@ -2067,8 +2067,8 @@ let modifies_union_loc_of_loc_intro #pop-options let modifies_union_loc_of_loc #al c b l h1 h2 = - Classical.move_requires #_ #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) #(fun h2 -> modifies l h1 h2) (modifies_union_loc_of_loc_elim c b l h1) h2; - Classical.move_requires #_ #(fun h2 -> modifies l h1 h2) #(fun h2 -> modifies (union_loc_of_loc c b l) h1 h2) (modifies_union_loc_of_loc_intro c b l h1) h2 + Classical.move_requires (modifies_union_loc_of_loc_elim c b l h1) h2; + Classical.move_requires (modifies_union_loc_of_loc_intro c b l h1) h2 let loc_of_union_loc #al #c b l = let (Loc regions region_liveness_tags non_live_addrs live_addrs aux) = l in diff --git a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst index 71e51968676..b11df5a6dc5 100644 --- a/ulib/FStar.Tactics.V1.Logic.Lemmas.fst +++ b/ulib/FStar.Tactics.V1.Logic.Lemmas.fst @@ -16,7 +16,7 @@ module FStar.Tactics.V1.Logic.Lemmas let fa_intro_lem (#a:Type) (#p:a -> Type) (f:(x:a -> squash (p x))) : Lemma (forall (x:a). p x) = - FStar.Classical.lemma_forall_intro_gtot #_ #(fun x -> p x) + FStar.Classical.lemma_forall_intro_gtot ((fun x -> FStar.IndefiniteDescription.elim_squash (f x)) <: (x:a -> GTot (p x))) let split_lem #a #b sa sb = () diff --git a/ulib/LowStar.Monotonic.Buffer.fst b/ulib/LowStar.Monotonic.Buffer.fst index deddd649707..19cc759d3ba 100644 --- a/ulib/LowStar.Monotonic.Buffer.fst +++ b/ulib/LowStar.Monotonic.Buffer.fst @@ -383,7 +383,7 @@ let ubuffer_preserved_intro ) ==> Seq.equal (Seq.slice (as_seq h b') (boff - U32.v idx) (boff - U32.v idx + blen)) (Seq.slice (as_seq h' b') (boff - U32.v idx) (boff - U32.v idx + blen)) ))))) - = Classical.move_requires #_ #_ #(fun b' -> live h' b') (f0 t' rrel rel) b'; + = Classical.move_requires (f0 t' rrel rel) b'; Classical.move_requires (f t' rrel rel) b' in Classical.forall_intro_4 g' @@ -899,10 +899,10 @@ let loc_includes_union_r' (loc_includes s (loc_union s1 s2) <==> (loc_includes s s1 /\ loc_includes s s2)) [SMTPat (loc_includes s (loc_union s1 s2))] = Classical.move_requires (loc_includes_union_r s s1) s2; - Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s1; - Classical.move_requires #_ #_ #(fun s -> loc_includes (loc_union s1 s2) s) (loc_includes_union_l s1 s2) s2; - Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s1; - Classical.move_requires #_ #_ #(fun s3 -> loc_includes s s3) (loc_includes_trans s (loc_union s1 s2)) s2 + Classical.move_requires (loc_includes_union_l s1 s2) s1; + Classical.move_requires (loc_includes_union_l s1 s2) s2; + Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s1; + Classical.move_requires (loc_includes_trans s (loc_union s1 s2)) s2 let loc_includes_none = MG.loc_includes_none @@ -1456,13 +1456,13 @@ let fresh_frame_loc_not_unused_in_disjoint let live_loc_not_unused_in #_ #_ #_ b h = unused_in_equiv b h; - Classical.move_requires #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b); + Classical.move_requires (MG.does_not_contain_addr_addr_unused_in h) (frameOf b, as_addr b); MG.loc_addresses_not_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h; () let unused_in_loc_unused_in #_ #_ #_ b h = unused_in_equiv b h; - Classical.move_requires #_ #_ #(fun ra -> MG.does_not_contain_addr h ra) (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b); + Classical.move_requires (MG.addr_unused_in_does_not_contain_addr h) (frameOf b, as_addr b); MG.loc_addresses_unused_in cls (frameOf b) (Set.singleton (as_addr b)) h; () diff --git a/ulib/legacy/FStar.Pointer.Base.fst b/ulib/legacy/FStar.Pointer.Base.fst index 7075aa564ae..144c25fd4dd 100644 --- a/ulib/legacy/FStar.Pointer.Base.fst +++ b/ulib/legacy/FStar.Pointer.Base.fst @@ -3214,8 +3214,8 @@ let disjoint_sym' (requires True) (ensures (disjoint p1 p2 <==> disjoint p2 p1)) [SMTPat (disjoint p1 p2)] -= FStar.Classical.move_requires #_ #(fun p2 -> disjoint p1 p2) (disjoint_sym #value1 #value2 p1) p2; - FStar.Classical.move_requires #_ #(fun p1 -> disjoint p2 p1) (disjoint_sym #value2 #value1 p2) p1 += FStar.Classical.move_requires (disjoint_sym #value1 #value2 p1) p2; + FStar.Classical.move_requires (disjoint_sym #value2 #value1 p2) p1 let disjoint_sym'' (value1: typ) @@ -3407,7 +3407,7 @@ let loc_aux_includes_trans' (s3: loc_aux) : Lemma ((loc_aux_includes s1 s2 /\ loc_aux_includes s2 s3) ==> loc_aux_includes s1 s3) -= Classical.move_requires #_ #_ #(fun s3 -> loc_aux_includes s1 s3) (loc_aux_includes_trans s1 s2) s3 += Classical.move_requires (loc_aux_includes_trans s1 s2) s3 (* Disjointness of two memory locations *) @@ -3605,7 +3605,7 @@ let disjoint_not_self (p: pointer t) : Lemma (disjoint p p ==> False) -= Classical.move_requires #_ #(fun p2 -> path_disjoint (Pointer?.p p) p2) (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p) += Classical.move_requires (path_disjoint_not_path_equal (Pointer?.p p)) (Pointer?.p p) let loc_aux_in_addr (l: loc_aux) From 3617cf608f45f45118027f367afaf0bac13ecd2f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 17:22:49 -0800 Subject: [PATCH 13/15] Add eta-expansion as a coercion. --- src/typechecker/FStarC.TypeChecker.Rel.fsti | 3 +++ src/typechecker/FStarC.TypeChecker.Util.fst | 9 +++++++++ 2 files changed, 12 insertions(+) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fsti b/src/typechecker/FStarC.TypeChecker.Rel.fsti index 8f58dfac52c..db6f310e272 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fsti +++ b/src/typechecker/FStarC.TypeChecker.Rel.fsti @@ -52,6 +52,9 @@ val head_matches_delta (env:env) (logical:bool) (smt_ok:bool) (t1 t2:typ) : (mat val may_relate_with_logical_guard (env:env) (is_equality:bool) (head:typ) : bool val guard_to_string : env -> guard_t -> string val simplify_guard : env -> guard_t -> guard_t + +val maybe_eta_expand_fun (env: env) (e t_e t_expected: term) : option term + val solve_deferred_constraints: env -> guard_t -> guard_t val solve_non_tactic_deferred_constraints: maybe_defer_flex_flex:bool -> env -> guard_t -> guard_t diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index d2eca1faae6..e112b403955 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -2572,6 +2572,15 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_ BU.print1 "(%s) No user coercion found\n" (Range.string_of_range e.pos) in + + match maybe_eta_expand_fun env e lc.res_typ exp_t with + | Some e' -> + if !dbg_Coercions then + BU.print3 "(%s) Eta-expansion coercion from %s to %s" (Range.string_of_range e.pos) (show e) (show e'); + // FIXME: do we need to type-check this again? + e', { lc with res_typ = exp_t }, Env.trivial_guard + + | None -> (* TODO: hide/reveal also user coercions? it's trickier for sure *) From 45bdbae8c76e7fbfc3fd13a979abe8645cd8a22d Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 17:24:56 -0800 Subject: [PATCH 14/15] Revert unnecessary changes to ulib. --- ulib/FStar.Classical.fst | 10 +++++----- ulib/FStar.Tactics.V1.Derived.fst | 2 +- ulib/FStar.Tactics.V2.Derived.fst | 2 +- ulib/LowStar.RVector.fst | 2 +- ulib/legacy/FStar.Buffer.Quantifiers.fst | 10 +++++----- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/ulib/FStar.Classical.fst b/ulib/FStar.Classical.fst index 026702d4a1d..b9de4cd1fdc 100644 --- a/ulib/FStar.Classical.fst +++ b/ulib/FStar.Classical.fst @@ -44,7 +44,7 @@ let arrow_to_impl #a #b f = squash_double_arrow (return_squash #(a -> GTot (squa let impl_intro_gtot #p #q f = return_squash f -let impl_intro_tot #p #q f = return_squash #(p -> GTot q) fun x -> f x +let impl_intro_tot #p #q f = return_squash #(p -> GTot q) f let impl_intro #p #q f = give_witness #(p ==> q) (squash_double_arrow (return_squash (lemma_to_squash_gtot f))) @@ -92,13 +92,13 @@ let gtot_to_lemma #a #p f x = give_proof #(p x) (return_squash (f x)) let forall_intro_squash_gtot #a #p f = bind_squash #(x: a -> GTot (p x)) #(forall (x: a). p x) - (squash_double_arrow #a #(fun x -> p x) (return_squash f)) + (squash_double_arrow #a #p (return_squash f)) (fun f -> lemma_forall_intro_gtot #a #p f) let forall_intro_squash_gtot_join #a #p f = join_squash (bind_squash #(x: a -> GTot (p x)) #(forall (x: a). p x) - (squash_double_arrow #a #(fun x -> p x) (return_squash f)) + (squash_double_arrow #a #p (return_squash f)) (fun f -> lemma_forall_intro_gtot #a #p f)) let forall_intro #a #p f = give_witness (forall_intro_squash_gtot (lemma_to_squash_gtot #a #p f)) @@ -118,7 +118,7 @@ let forall_intro_3 #a #b #c #p f = let g: x: a -> Lemma (forall (y: b x) (z: c x y). p x y z) = fun x -> forall_intro_2 (f x) in forall_intro g -let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c f +let forall_intro_3_with_pat #a #b #c #d #p pat f = forall_intro_3 #a #b #c #p f let forall_intro_4 #a #b #c #d #p f = let g: x: a -> Lemma (forall (y: b x) (z: c x y) (w: d x y z). p x y z w) = @@ -165,7 +165,7 @@ let exists_intro_not_all_not (#a:Type) (#p:a -> Type) (get_proof (forall x. ~ (p x))) (fun (g: (forall x. ~ (p x))) -> bind_squash #(x:a -> GTot (~(p x))) #Prims.empty g - (fun (h:(x:a -> GTot (~(p x)))) -> f fun x -> h x)) + (fun (h:(x:a -> GTot (~(p x)))) -> f h)) in () #pop-options diff --git a/ulib/FStar.Tactics.V1.Derived.fst b/ulib/FStar.Tactics.V1.Derived.fst index 3e918b038b1..a4478fa47b2 100644 --- a/ulib/FStar.Tactics.V1.Derived.fst +++ b/ulib/FStar.Tactics.V1.Derived.fst @@ -428,7 +428,7 @@ val (<|>) : (unit -> Tac 'a) -> let (<|>) t1 t2 = fun () -> or_else t1 t2 let first (ts : list (unit -> Tac 'a)) : Tac 'a = - L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") () + L.fold_right (<|>) ts (fun () -> fail "no tactics to try") () let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) = match catch t with diff --git a/ulib/FStar.Tactics.V2.Derived.fst b/ulib/FStar.Tactics.V2.Derived.fst index f8d87432266..06f6a002612 100644 --- a/ulib/FStar.Tactics.V2.Derived.fst +++ b/ulib/FStar.Tactics.V2.Derived.fst @@ -482,7 +482,7 @@ val (<|>) : (unit -> Tac 'a) -> let (<|>) t1 t2 = fun () -> or_else t1 t2 let first (ts : list (unit -> Tac 'a)) : Tac 'a = - L.fold_right (fun t1 t2 () -> or_else t1 t2) ts (fun () -> fail "no tactics to try") () + L.fold_right (<|>) ts (fun () -> fail "no tactics to try") () let rec repeat (#a:Type) (t : unit -> Tac a) : Tac (list a) = match catch t with diff --git a/ulib/LowStar.RVector.fst b/ulib/LowStar.RVector.fst index 6b38d83a170..93e11cac701 100644 --- a/ulib/LowStar.RVector.fst +++ b/ulib/LowStar.RVector.fst @@ -74,7 +74,7 @@ val rs_elems_inv: i:nat -> j:nat{i <= j && j <= S.length rs} -> GTot Type0 let rs_elems_inv #a #rst rg h rs i j = - V.forall_seq rs i j (fun x -> rg_inv rg h x) + V.forall_seq rs i j (rg_inv rg h) val rv_elems_inv: #a:Type0 -> #rst:Type -> #rg:regional rst a -> diff --git a/ulib/legacy/FStar.Buffer.Quantifiers.fst b/ulib/legacy/FStar.Buffer.Quantifiers.fst index 6a9287189a5..783b9af7ffc 100644 --- a/ulib/legacy/FStar.Buffer.Quantifiers.fst +++ b/ulib/legacy/FStar.Buffer.Quantifiers.fst @@ -35,7 +35,7 @@ let lemma_sub_quantifiers #a h b b' i len = let lemma_post (j:nat) = j < length b' ==> get h b' j == get h b (j + v i) in let qj : j:nat -> Lemma (lemma_post j) = fun j -> assert (j < v len ==> Seq.index (as_seq h b') j == Seq.index (as_seq h b) (j + v i)) in - Classical.forall_intro #_ #(fun x -> lemma_post x) qj + Classical.forall_intro #_ #lemma_post qj val lemma_offset_quantifiers: #a:Type -> h:mem -> b:buffer a -> b':buffer a -> i:FStar.UInt32.t{v i <= length b} -> Lemma (requires (live h b /\ live h b' /\ Seq.slice (as_seq h b) (v i) (length b) == as_seq h b')) @@ -56,7 +56,7 @@ let lemma_create_quantifiers #a h b init len = let lemma_post (i:nat) = i < length b ==> get h b i == init in let qi : i:nat -> Lemma (lemma_post i) = fun i -> assert (i < length b ==> get h b i == Seq.index (as_seq h b) i) in - Classical.forall_intro #_ #(fun x -> lemma_post x) qi + Classical.forall_intro #_ #lemma_post qi val lemma_index_quantifiers: #a:Type -> h:mem -> b:buffer a -> n:FStar.UInt32.t -> Lemma (requires (live h b /\ v n < length b)) @@ -101,8 +101,8 @@ let lemma_blit_quantifiers #a h0 h1 b bi b' bi' len = ==> Seq.index (Seq.slice (as_seq h1 b') (v bi'+v len) (length b')) (j - (v bi'+v len)) == Seq.index (Seq.slice (as_seq h0 b') (v bi'+v len) (length b')) (j - (v bi'+v len))) in - Classical.forall_intro #_ #(fun x -> lemma_post_1 x) qj_1; - Classical.forall_intro #_ #(fun x -> lemma_post_2 x) qj_2 + Classical.forall_intro #_ #lemma_post_1 qj_1; + Classical.forall_intro #_ #lemma_post_2 qj_2 (* Equality predicate between buffers with quantifiers *) @@ -116,4 +116,4 @@ let eq_lemma #a h b h' b' = let lemma_post (j:nat) = j < length b ==> get h b j == get h' b' j in let qj : j:nat -> Lemma (lemma_post j) = fun j -> assert(j < length b ==> Seq.index (as_seq h b) j == Seq.index (as_seq h' b') j) in - Classical.forall_intro #_ #(fun x -> lemma_post x) qj + Classical.forall_intro #_ #lemma_post qj From 863147a555a42e359d3976c930bd55748c09871e Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 10 Jan 2025 14:50:49 -0800 Subject: [PATCH 15/15] Disable eta-expansion in MLish --- src/typechecker/FStarC.TypeChecker.Rel.fst | 2 ++ src/typechecker/FStarC.TypeChecker.Util.fst | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst index 77938a5862a..c707b2522e0 100644 --- a/src/typechecker/FStarC.TypeChecker.Rel.fst +++ b/src/typechecker/FStarC.TypeChecker.Rel.fst @@ -2997,6 +2997,8 @@ and solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:flex_t) (rhs:term) S.mk_Tm_app rhs_hd rhs_args rhs.pos in let rhs = + // eta-expand functions for effect promotion, unless we're in --MLish + if Options.ml_ish () then rhs else let env = { env with admit=true; expected_typ=None } in let t_u, _ = let Flex (lhs, _, _) = lhs in diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index e112b403955..33b1bd9ab5b 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -2573,7 +2573,8 @@ let maybe_coerce_lc env (e:term) (lc:lcomp) (exp_t:term) : term & lcomp & guard_ (Range.string_of_range e.pos) in - match maybe_eta_expand_fun env e lc.res_typ exp_t with + // eta-expand functions for effect promotion, unless we're in --MLish + match if Options.ml_ish () then None else maybe_eta_expand_fun env e lc.res_typ exp_t with | Some e' -> if !dbg_Coercions then BU.print3 "(%s) Eta-expansion coercion from %s to %s" (Range.string_of_range e.pos) (show e) (show e');