From 02480e1f7661fbb5bf19355ee0b8498e226d519e Mon Sep 17 00:00:00 2001 From: Nikhil Swamy Date: Mon, 13 Jan 2025 22:28:50 -0800 Subject: [PATCH] restore many examples, mainly in layered efffects, needing explicit universe instantiations for mootonocitity proofs --- examples/algorithms/BinarySearch.fst | 10 +++-- .../BinaryTreesEnumeration.fsti | 3 +- .../data_structures/LowStar.Lens.Buffer.fsti | 4 +- .../data_structures/LowStar.Lens.Tuple2.fst | 2 +- examples/data_structures/LowStar.Lens.fsti | 2 +- examples/data_structures/RBTreeIntrinsic.fst | 1 + .../doublylinkedlist/DoublyLinkedList.fst | 6 +-- examples/dsls/DSL.fst.config.json | 3 +- .../dsls/bool_refinement/BoolRefinement.fst | 15 +++++-- examples/layeredeffects/DM4F.fst | 8 ++-- examples/layeredeffects/DM4F_layered.fst | 4 +- examples/layeredeffects/DM4F_layered5.fst | 2 +- examples/layeredeffects/GT.fst | 14 +++--- examples/layeredeffects/GTWP.fst | 43 +++++++++++++------ .../layeredeffects/GenericPartialDM4A.fst | 2 +- examples/layeredeffects/HoareSTPolyBind.fst | 7 +-- examples/layeredeffects/ID1.fst | 11 ++--- examples/layeredeffects/ID2.fst | 9 ++-- examples/layeredeffects/ID3.fst | 11 ++--- examples/layeredeffects/ID4.fst | 29 +++++++++---- examples/layeredeffects/ID5.fst | 21 ++++----- examples/layeredeffects/IteSoundness.fst | 14 +++--- examples/layeredeffects/MSeqExn.fst | 4 +- examples/layeredeffects/ND.fst | 9 ++-- examples/layeredeffects/Sec2.HIFC.fst | 2 +- examples/layeredeffects/Z3EncodingIssue.fst | 6 +-- examples/misc/WorkingWithSquashedProofs.fst | 14 +++--- examples/native_tactics/Clear.fst | 2 +- examples/native_tactics/Makefile | 2 +- .../oplss2021/OPLSS2021.DijkstraMonads.fst | 6 +-- examples/paradoxes/PrecedesRank.fst | 4 +- examples/tactics/Postprocess.fst | 14 +++--- 32 files changed, 169 insertions(+), 115 deletions(-) diff --git a/examples/algorithms/BinarySearch.fst b/examples/algorithms/BinarySearch.fst index 81beb3569d5..4b973c2e88c 100644 --- a/examples/algorithms/BinarySearch.fst +++ b/examples/algorithms/BinarySearch.fst @@ -106,13 +106,15 @@ let hint1 y a = () val hint2 : t:(seq int) -> a:int -> mid:int -> Lemma (requires - (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\ + (forall i1 i2. + {:pattern index t i1; index t i2} + (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\ (0 <= mid) /\ (mid < length t) /\ (index t mid < a)) (ensures (forall p. (((0 <= p) /\ (p < length t) /\ (index t p = a) /\ (p <= mid)) ==> False))) -let hint2 t a mid = hint1 (index t mid) a +let hint2 t a mid = () val hint3 : y:int -> a:int -> Lemma (requires True) @@ -122,7 +124,9 @@ let hint3 y a = () val hint4 : t:(seq int) -> a:int -> mid:int -> Lemma (requires - (forall i1 i2. (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\ + (forall i1 i2. + {:pattern index t i1; index t i2} + (0 <= i1) ==> (i1 <= i2) ==> (i2 < length t) ==> (index t i1 <= index t i2)) /\ (0 <= mid) /\ (mid < length t) /\ (a < index t mid)) diff --git a/examples/data_structures/BinaryTreesEnumeration.fsti b/examples/data_structures/BinaryTreesEnumeration.fsti index 5ab5b5d372d..08a15c9f41f 100644 --- a/examples/data_structures/BinaryTreesEnumeration.fsti +++ b/examples/data_structures/BinaryTreesEnumeration.fsti @@ -235,6 +235,7 @@ let memP_concatMap_intro #a #b (x: a) (y: b) (f:a -> list b) (l: list a) : can I get rid of them without cluttering the rest of the proof with many copies of the same function? Can I infer them by unifying with the current “goal”? *) +module T = FStar.Tactics let product_complete (#a #b: Type) (l1: list a) (l2: list b) x1 x2 : Lemma (List.memP x1 l1 ==> List.memP x2 l2 ==> @@ -244,7 +245,7 @@ let product_complete (#a #b: Type) (l1: list a) (l2: list b) x1 x2 : let f1 = fun x1 -> List.Tot.map (f2 x1) l2 in let l = f1 x1 in let ls = List.Tot.map f1 l1 in - assert (product l1 l2 == List.Tot.concatMap f1 l1); + assert (product l1 l2 == List.Tot.concatMap f1 l1) by (T.trefl()); memP_map_intro (f2 x1) x2 l2 <: Lemma (List.memP x2 l2 ==> List.memP x l); diff --git a/examples/data_structures/LowStar.Lens.Buffer.fsti b/examples/data_structures/LowStar.Lens.Buffer.fsti index 3381b6e96a7..01d54a298f7 100644 --- a/examples/data_structures/LowStar.Lens.Buffer.fsti +++ b/examples/data_structures/LowStar.Lens.Buffer.fsti @@ -189,11 +189,11 @@ val mk (#a:_) (#p:_) (#q:_) (b:B.mbuffer a p q) (f:flavor b) (snap:HS.mem{B.live : Tot (l:buffer_lens b f{(lens_of l).snapshot == snap}) /// `elim_inv`: Revealing the abstract invariant of buffer lenses -val elim_inv (#a:_) (#p:_) (#q:_) +val elim_inv (#a:Type) (#p:_) (#q:_) (#b:B.mbuffer a p q) (#f:flavor b) (bl:buffer_lens b f) - : Lemma (reveal_inv(); + : Lemma (reveal_inv u#0 u#0 (); (forall (h:HS.mem).{:pattern (lens_of bl).invariant (lens_of bl).x h} let l = lens_of bl in (exists h'.{:pattern mk b f h'} B.live h' b /\ bl == mk b f h') /\ diff --git a/examples/data_structures/LowStar.Lens.Tuple2.fst b/examples/data_structures/LowStar.Lens.Tuple2.fst index 79f1784044f..64eafecad1e 100644 --- a/examples/data_structures/LowStar.Lens.Tuple2.fst +++ b/examples/data_structures/LowStar.Lens.Tuple2.fst @@ -295,7 +295,7 @@ let elim_tup2_inv (bl1:LB.buffer_lens b1 f1) (bl2:LB.buffer_lens b2 f2{composable (LB.lens_of bl1) (LB.lens_of bl2)}) : Lemma (let t = mk_tup2 bl1 bl2 in - reveal_inv(); + reveal_inv u#0 u#0 (); (forall h. {:pattern inv (lens_of t) h} inv (lens_of t) h ==> (LB.lens_of bl1).invariant b1 h /\ diff --git a/examples/data_structures/LowStar.Lens.fsti b/examples/data_structures/LowStar.Lens.fsti index c9d4450b4f6..168ffb3353b 100644 --- a/examples/data_structures/LowStar.Lens.fsti +++ b/examples/data_structures/LowStar.Lens.fsti @@ -226,7 +226,7 @@ effect LensST (a:Type) /// `reveal_inv`: Revealing the abstract invariant val reveal_inv (_:unit) - : Lemma ((forall #a #b (l:hs_lens a b) h. {:pattern inv l h} + : Lemma ((forall (#a:Type u#a) (#b:Type u#b) (l:hs_lens a b) h. {:pattern inv l h} inv l h <==> (l.invariant l.x h /\ B.modifies (as_loc l.footprint) l.snapshot h /\ diff --git a/examples/data_structures/RBTreeIntrinsic.fst b/examples/data_structures/RBTreeIntrinsic.fst index fc986315da7..08affb2b0fb 100644 --- a/examples/data_structures/RBTreeIntrinsic.fst +++ b/examples/data_structures/RBTreeIntrinsic.fst @@ -383,6 +383,7 @@ val balanceLB_preserves_sort : #h:nat -> #c:color -> a:almostNode h -> x:int -> (requires almostNode_sorted a /\ sorted b /\ chain (almostNode_max a) x (min b)) (ensures hiddenTree_sorted (balanceLB a x b)) let balanceLB_preserves_sort #h #c left z d = () +#restart-solver val balanceRB_preserves_sort : #h:nat -> #c:color -> a:rbnode h c -> x:int -> b:almostNode h -> Lemma diff --git a/examples/doublylinkedlist/DoublyLinkedList.fst b/examples/doublylinkedlist/DoublyLinkedList.fst index b34fd763aeb..f76050ce96c 100644 --- a/examples/doublylinkedlist/DoublyLinkedList.fst +++ b/examples/doublylinkedlist/DoublyLinkedList.fst @@ -1221,7 +1221,7 @@ let lemma_dll_links_contained (#t:Type) (h0:heap) (d:dll t) (i:nat) : lemma_unsnoc_is_last nl #set-options "--z3rlimit 10 --initial_ifuel 2" - +#restart-solver let lemma_dll_links_disjoint (#t:Type) (h0:heap) (d:dll t) (i:nat) : Lemma (requires ( @@ -1964,8 +1964,8 @@ let dll_append (#t:Type) (d1 d2:dll t) : #reset-options -#set-options "--z3rlimit 40 --max_fuel 2 --max_ifuel 1" - +#set-options "--z3rlimit 80 --max_fuel 2 --max_ifuel 1 --query_stats --split_queries no --z3smtopt '(set-option :smt.qi.eager_threshold 5)'" +#restart-solver let dll_split_using (#t:Type) (d:dll t) (e:pointer (node t)) : StackInline (dll t * dll t) (requires (fun h0 -> diff --git a/examples/dsls/DSL.fst.config.json b/examples/dsls/DSL.fst.config.json index d1360f24590..fba973ae45c 100644 --- a/examples/dsls/DSL.fst.config.json +++ b/examples/dsls/DSL.fst.config.json @@ -1,7 +1,8 @@ { "fstar_exe": "fstar.exe", "options": [ - "--z3version", "4.13.3" + "--z3version", "4.13.3", + "--ext", "context_pruning" ], "include_dirs": [ "bool_refinement", diff --git a/examples/dsls/bool_refinement/BoolRefinement.fst b/examples/dsls/bool_refinement/BoolRefinement.fst index 6e36e91d41b..d2bd39d2d64 100644 --- a/examples/dsls/bool_refinement/BoolRefinement.fst +++ b/examples/dsls/bool_refinement/BoolRefinement.fst @@ -4,8 +4,7 @@ module R = FStar.Reflection.V2 module L = FStar.List.Tot open FStar.List.Tot -#set-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'" - +#set-options "--z3smtopt '(set-option :smt.qi.eager_threshold 20)' --z3smtopt '(set-option :smt.arith.nl false)'" let var = nat let index = nat @@ -126,6 +125,7 @@ let rec close_exp' (e:src_exp) (v:var) (n:nat) let open_exp e v = open_exp' e v 0 let close_exp e v = close_exp' e v 0 +#restart-solver let rec open_close' (e:src_exp) (x:var) (n:nat { ln' e (n - 1) }) : Lemma (open_exp' (close_exp' e x n) x n == e) @@ -607,6 +607,7 @@ let rec extend_env_l_lookup_bvar (g:R.env) (sg:src_env) (x:var) //key lemma about src types: Their elaborations are closed #push-options "--z3rlimit_factor 4 --fuel 8 --ifuel 2" +#restart-solver let rec src_refinements_are_closed_core (n:nat) (e:src_exp {ln' e (n - 1) && closed e}) @@ -1146,7 +1147,8 @@ let rec src_typing_freevars #f (sg:src_env) (e:src_exp) (t:s_ty) (d:src_typing f src_typing_freevars _ _ _ dbody #pop-options -#push-options "--z3rlimit_factor 4" +#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2" +#restart-solver let rec src_typing_renaming (#f:RT.fstar_top_env) (sg sg':src_env) (x:var { None? (lookup sg x) && None? (lookup sg' x) }) @@ -1259,6 +1261,7 @@ let rec src_typing_renaming (#f:RT.fstar_top_env) in let dt = src_ty_ok_renaming _ _ _ _ _ _ dt in T_If _ _ _ _ _ _ _ _ db dt1 dt2 st1 st2 dt +#pop-options let sub_typing_weakening #f (sg sg':src_env) (x:var { None? (lookup sg x) && None? (lookup sg' x) }) @@ -1323,6 +1326,8 @@ let sub_typing_weakening #f (sg sg':src_env) | _ -> admit ()) +#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2" +#restart-solver let rec src_typing_weakening #f (sg sg':src_env) (x:var { None? (lookup sg x) && None? (lookup sg' x) }) (b:binding) @@ -1518,6 +1523,8 @@ let freevars_refinement (e:R.term) (bv0:_) = () #pop-options +#push-options "--z3rlimit_factor 8 --query_stats --split_queries no --fuel 2 --ifuel 2" +#restart-solver let rec soundness (#f:RT.fstar_top_env) (#sg:src_env { src_env_ok sg } ) (#se:src_exp { ln se }) @@ -1673,7 +1680,9 @@ and src_ty_ok_soundness (#f:RT.fstar_top_env) in freevars_refinement (elab_exp e) bv0; RT.T_Refine (extend_env_l f sg) x RT.bool_ty refinement' _ _ _ _ bool_typing dr +#pop-options +#restart-solver let soundness_lemma (f:RT.fstar_top_env) (sg:src_env { src_env_ok sg }) (se:src_exp { ln se }) diff --git a/examples/layeredeffects/DM4F.fst b/examples/layeredeffects/DM4F.fst index 341c70f7774..8ec634ce5cd 100644 --- a/examples/layeredeffects/DM4F.fst +++ b/examples/layeredeffects/DM4F.fst @@ -78,13 +78,13 @@ effect { } unfold -let lift_wp (#a:Type) (#st:Type0) (w:pure_wp a) : wp st a = - elim_pure_wp_monotonicity_forall (); +let lift_wp (#a:Type u#a) (#st:Type0) (w:pure_wp a) : wp st a = + elim_pure_wp_monotonicity_forall u#a (); fun s0 p -> w (fun x -> p (x, s0)) -let lift_pure_st a wp st (f : unit -> PURE a wp) +let lift_pure_st (a:Type u#a) wp st (f : unit -> PURE a wp) : repr a st (lift_wp wp) - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); fun s0 -> (f (), s0) sub_effect PURE ~> ST = lift_pure_st diff --git a/examples/layeredeffects/DM4F_layered.fst b/examples/layeredeffects/DM4F_layered.fst index ea78ab3ab01..eed560f13a0 100644 --- a/examples/layeredeffects/DM4F_layered.fst +++ b/examples/layeredeffects/DM4F_layered.fst @@ -128,12 +128,12 @@ let lift_pure_st_wp #a #st (w : pure_wp a) : wp st a = r let lift_id_st_wp #a #st (w : pure_wp a) : wp st a = - elim_pure_wp_monotonicity_forall (); + elim_pure_wp_monotonicity w; fun s0 p -> w (fun x -> p x s0) let lift_id_st a wp st (f : ID2.repr a wp) : repr a st (lift_id_st_wp wp) - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity wp; fun s0 -> (f (), s0) sub_effect ID ~> ST = lift_id_st diff --git a/examples/layeredeffects/DM4F_layered5.fst b/examples/layeredeffects/DM4F_layered5.fst index bf9b918c2ef..494fd78a9be 100644 --- a/examples/layeredeffects/DM4F_layered5.fst +++ b/examples/layeredeffects/DM4F_layered5.fst @@ -106,7 +106,7 @@ effect { } let lift_id_st_wp #a #st (w : ID5.wp a) : wp st a = - elim_pure_wp_monotonicity_forall (); + elim_pure_wp_monotonicity w; fun s0 p -> w (fun x -> p x s0) let lift_id_st a wp st (f : ID5.repr a wp) diff --git a/examples/layeredeffects/GT.fst b/examples/layeredeffects/GT.fst index 1af27cd4efc..529a492b3bb 100644 --- a/examples/layeredeffects/GT.fst +++ b/examples/layeredeffects/GT.fst @@ -20,22 +20,22 @@ let m (a:Type u#aa) (i:idx) : Type u#aa = let t_return #a (x:a) : m a T = (fun () -> x) let g_return #a (x:a) : m a G = (fun () -> x) let d_return #a (x:a) : m a D = raise_val (fun () -> x) - +#push-options "--print_universes --log_queries --query_stats" +#restart-solver let return (a:Type) (x:a) (i:idx) : m a i = - match i with + match i returns m a i with | T -> t_return x | G -> g_return x | D -> d_return x - let t_bind #a #b (c : m a T) (f : a -> m b T) : m b T = fun () -> f (c ()) () let g_bind #a #b (c : m a G) (f : a -> m b G) : m b G = fun () -> f (c ()) () let d_bind #a #b (c : m a D) (f : a -> m b D) : m b D = raise_val (fun () -> downgrade_val (f (downgrade_val c ())) ()) let bind (a b : Type) (i:idx) (c : m a i) (f : a -> m b i) : m b i = - match i with + match i returns m b i with | T -> t_bind #a #b c f - | D -> coerce (d_bind #a #b c f) // GM: wow... still needs a coerce, how can that be? + | D -> d_bind #a #b (coerce c) f // GM: wow... still needs a coerce, how can that be? | G -> g_bind #a #b c f // Already somewhat usable @@ -77,10 +77,10 @@ let lift_pure_gtd (a:Type) (wp : pure_wp a) (i : idx) // case analyze [i]. // GM: ok not anymore FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; - match i with + match i returns m a i with | T -> f | G -> f - | D -> coerce (raise_val (fun () -> f () <: Dv a)) + | D -> raise_val (fun () -> f () <: Dv a) sub_effect PURE ~> GTD = lift_pure_gtd diff --git a/examples/layeredeffects/GTWP.fst b/examples/layeredeffects/GTWP.fst index e897f538ccb..d16c02383a5 100644 --- a/examples/layeredeffects/GTWP.fst +++ b/examples/layeredeffects/GTWP.fst @@ -17,8 +17,9 @@ let coerce #a #b (x:a{a == b}) : b = x let wp (a:Type) = pure_wp a unfold -let bind_wp #a #b (wc : wp a) (wf : a -> wp b) : wp b = - elim_pure_wp_monotonicity_forall (); +let bind_wp (#a:Type u#a) (#b:Type u#b) (wc : wp a) (wf : a -> wp b) : wp b = + elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wc (fun x -> wf x p)) let m (a:Type u#aa) (i:idx) (w : wp a) : Type u#aa = @@ -41,15 +42,24 @@ let return (a:Type) (x:a) (i:idx) : m a i (return_wp x) = | D -> coerce (d_return x) // these two rely on monotonicity since the computed WP is not exactly bind_wp -let t_bind #a #b #wc #wf (c : m a T wc) (f : (x:a -> m b T (wf x))) : m b T (bind_wp wc wf) = elim_pure_wp_monotonicity_forall (); fun () -> f (c ()) () -let g_bind #a #b #wc #wf (c : m a G wc) (f : (x:a -> m b G (wf x))) : m b G (bind_wp wc wf) = elim_pure_wp_monotonicity_forall (); fun () -> f (c ()) () +let t_bind (#a:Type u#a) (#b:Type u#b) #wc #wf (c : m a T wc) (f : (x:a -> m b T (wf x))) +: m b T (bind_wp wc wf) += elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); + fun () -> f (c ()) () +let g_bind (#a:Type u#a) (#b:Type u#b) #wc #wf (c : m a G wc) (f : (x:a -> m b G (wf x))) +: m b G (bind_wp wc wf) += elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); + fun () -> f (c ()) () let d_bind #a #b #wc #wf (c : m a D wc) (f : (x:a -> m b D (wf x))) : m b D (bind_wp wc wf) = raise_val (fun () -> let y = downgrade_val c () in // cannot inline this downgrade_val (f y) ()) -let bind (a b : Type) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a -> m b i (wf x))) : m b i (bind_wp wc wf) = - elim_pure_wp_monotonicity_forall (); +let bind (a:Type u#a) (b : Type u#b) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a -> m b i (wf x))) : m b i (bind_wp wc wf) = + elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); match i with | T -> t_bind #_ #_ #wc #wf c f | G -> g_bind #_ #_ #wc #wf c f @@ -64,10 +74,17 @@ let subcomp (a:Type u#aa) (i:idx) (requires (forall p. wp2 p ==> wp1 p)) (ensures (fun _ -> True)) = match i with - | T -> f - | G -> f + | T -> + let f : m a T wp1 = coerce #(m a i wp1) #(m a T wp1) f in + let f : m a T wp2 = f in + coerce #(m a T wp2) #(m a i wp2) f + | G -> + let f : m a G wp1 = coerce #(m a i wp1) #(m a G wp1) f in + let f : m a G wp2 = f in + coerce #(m a G wp2) #(m a i wp2) f | D -> (* This case needs some handholding. *) + let f : m a D wp1 = coerce #(m a i wp1) #(m a D wp1) f in let f : raise_t (unit -> DIV a wp1) = f in let f : unit -> DIV a wp1 = downgrade_val f in let f : unit -> DIV a wp2 = f in @@ -75,8 +92,8 @@ let subcomp (a:Type u#aa) (i:idx) coerce (raise_val f) unfold -let ite_wp #a (w1 w2 : wp a) (b:bool) : wp a = - elim_pure_wp_monotonicity_forall (); +let ite_wp (#a:Type u#a) (w1 w2 : wp a) (b:bool) : wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun p -> if b then w1 p else w2 p) let if_then_else (a:Type) (i:idx) (w1 w2 : wp a) @@ -99,18 +116,18 @@ effect { } } -let lift_pure_gtd (a:Type) (w : wp a) (i : idx) +let lift_pure_gtd (a:Type u#a) (w : wp a) (i : idx) (f : unit -> PURE a w) : Pure (m a i w) (requires True) (ensures (fun _ -> True)) - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); match i with | T -> f | G -> f | D -> let f' () : DIV a w = f () in let f'' : m a D w = raise_val f' in - f'' + coerce f'' // GM: Surprised that this works actually... I expected that I would need to // case analyze [i]. diff --git a/examples/layeredeffects/GenericPartialDM4A.fst b/examples/layeredeffects/GenericPartialDM4A.fst index 0ebfdcb480a..337ced6201e 100644 --- a/examples/layeredeffects/GenericPartialDM4A.fst +++ b/examples/layeredeffects/GenericPartialDM4A.fst @@ -138,7 +138,7 @@ effect { let lift_pure_dm4a (a:Type) (wp : pure_wp a) (f:unit -> PURE a wp) : Tot (repr a (wp (fun _ -> True)) (fun _ -> w_return (f ()))) = fun _ -> - FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); + FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; let x = f () in interp_ret x; m_return x diff --git a/examples/layeredeffects/HoareSTPolyBind.fst b/examples/layeredeffects/HoareSTPolyBind.fst index d2f73511d6f..e7cac429517 100644 --- a/examples/layeredeffects/HoareSTPolyBind.fst +++ b/examples/layeredeffects/HoareSTPolyBind.fst @@ -155,12 +155,13 @@ let bind_pure_hoarest (a:Type) (b:Type) (wp:pure_wp a) (req:a -> pre_t) (ens:a - polymonadic_bind (PURE, HoareST) |> HoareST = bind_pure_hoarest -let bind_hoarest_pure (a:Type) (b:Type) (req:pre_t) (ens:post_t a) (wp:a -> pure_wp b) +let bind_hoarest_pure (a:Type u#a) (b:Type u#b) (req:pre_t) (ens:post_t a) (wp:a -> pure_wp b) (f:repr a req ens) (g:(x:a -> unit -> PURE b (wp x))) : repr b (fun h -> req h /\ (forall x h1. ens h x h1 ==> (wp x) (fun _ -> True))) (fun h0 r h1 -> exists x. ens h0 x h1 /\ (~ ((wp x) (fun y -> y =!= r)))) -= FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); += FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#a (); + FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#b (); fun _ -> let x = f () in (g x) () @@ -179,7 +180,7 @@ let subcomp_pure_hoarest (a:Type) (wp:pure_wp a) (req:pre_t) (ens:post_t a) (forall h. req h ==> wp (fun _ -> True)) /\ (forall h0 r h1. (~ (wp (fun x -> x =!= r \/ h0 =!= h1))) ==> ens h0 r h1)) (ensures fun _ -> True) -= FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); += FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; fun _ -> f () polymonadic_subcomp PURE <: HoareST = subcomp_pure_hoarest diff --git a/examples/layeredeffects/ID1.fst b/examples/layeredeffects/ID1.fst index 6f2bca03f59..f26476f4e2f 100644 --- a/examples/layeredeffects/ID1.fst +++ b/examples/layeredeffects/ID1.fst @@ -22,11 +22,12 @@ let return (a : Type) (x : a) : repr a (return_wp x) = fun p _ -> x unfold -let bind_wp #a #b +let bind_wp (#a:Type u#a) (#b:Type u#b) (wp_v : wp a) (wp_f : (x:a -> wp b)) : wp b - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp_v (fun x -> wp_f x p)) let bind (a b : Type) (wp_v : wp a) (wp_f: a -> wp b) @@ -52,8 +53,8 @@ let subcomp (a:Type u#uu) (w1 w2:wp a) //= fun p pf -> f (hide (fun x -> reveal p x)) () unfold -let ite_wp #a (wp1 wp2 : wp a) (b : bool) : wp a = - elim_pure_wp_monotonicity_forall (); +let ite_wp (#a:Type u#a) (wp1 wp2 : wp a) (b : bool) : wp a = + elim_pure_wp_monotonicity_forall u#a (); (as_pure_wp (fun (p:a -> Type) -> (b ==> wp1 p) /\ ((~b) ==> wp2 p))) let if_then_else (a : Type) (wp1 wp2 : wp a) (f : repr a wp1) (g : repr a wp2) (p : bool) : Type = @@ -99,7 +100,7 @@ open FStar.Tactics.V2 let elim_pure #a #wp ($f : unit -> PURE a wp) p : Pure a (requires (wp p)) (ensures (fun r -> p r)) - = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); + = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; f () let lift_pure_nd (a:Type) (wp:wp a) (f:unit -> PURE a wp) : diff --git a/examples/layeredeffects/ID2.fst b/examples/layeredeffects/ID2.fst index e4b2ba01e67..e99228da51c 100644 --- a/examples/layeredeffects/ID2.fst +++ b/examples/layeredeffects/ID2.fst @@ -11,7 +11,7 @@ let repr (a : Type u#aa) (wp : pure_wp a) : Type u#aa = let return (a : Type) (x : a) : repr a (pure_return a x) = fun () -> x -let bind (a b : Type) +let bind (a : Type u#a) (b : Type u#b) (wp_v : pure_wp a) (wp_f: a -> pure_wp b) (v : repr a wp_v) (f : (x:a -> repr b (wp_f x))) @@ -19,7 +19,8 @@ let bind (a b : Type) // Fun fact: using () instead of _ below makes us // lose the refinement and then this proof fails. // Keep that in mind all ye who enter here. - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); fun _ -> f (v ()) () let subcomp (a:Type) @@ -31,8 +32,8 @@ let subcomp (a:Type) = f unfold -let if_then_else_wp (#a:Type) (wp1 wp2:pure_wp a) (p:bool) : pure_wp a = - elim_pure_wp_monotonicity_forall (); +let if_then_else_wp (#a:Type u#a) (wp1 wp2:pure_wp a) (p:bool) : pure_wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun post -> (p ==> wp1 post) /\ ((~p) ==> wp2 post)) let if_then_else (a : Type) diff --git a/examples/layeredeffects/ID3.fst b/examples/layeredeffects/ID3.fst index cc15db0a508..edb00e2c3e9 100644 --- a/examples/layeredeffects/ID3.fst +++ b/examples/layeredeffects/ID3.fst @@ -20,8 +20,9 @@ let return (a : Type) (x : a) : repr a (as_pure_wp (fun p -> p x)) = x unfold -let bind_wp #a #b (wp_v:w a) (wp_f:a -> w b) : w b = - elim_pure_wp_monotonicity_forall (); +let bind_wp (#a:Type u#a) (#b:Type u#b) (wp_v:w a) (wp_f:a -> w b) : w b = + elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp_v (fun x -> wp_f x p)) let bind (a b : Type) (wp_v : w a) (wp_f: a -> w b) @@ -38,8 +39,8 @@ let subcomp (a:Type) (wp1 wp2: w a) = f unfold -let if_then_else_wp #a (wp1 wp2:w a) (p:bool) = - elim_pure_wp_monotonicity_forall (); +let if_then_else_wp (#a:Type u#a) (wp1 wp2:w a) (p:bool) = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun post -> (p ==> wp1 post) /\ ((~p) ==> wp2 post)) let if_then_else (a : Type) (wp1 wp2 : w a) (f : repr a wp1) (g : repr a wp2) (p : bool) : Type = @@ -61,7 +62,7 @@ effect { let lift_pure_nd (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) : Pure (repr a wp) (requires (wp (fun _ -> True))) (ensures (fun _ -> True)) - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity wp; f () sub_effect PURE ~> ID = lift_pure_nd diff --git a/examples/layeredeffects/ID4.fst b/examples/layeredeffects/ID4.fst index dbfae376bfe..4eb28cf996a 100644 --- a/examples/layeredeffects/ID4.fst +++ b/examples/layeredeffects/ID4.fst @@ -30,11 +30,12 @@ let return (a : Type) (x : a) : repr a (return_wp x) = (_, (fun p _ -> x)) unfold -let bind_wp #a #b +let bind_wp (#a:Type u#a) (#b:Type u#b) (wp_v : wp0 a) (wp_f : (x:a -> wp0 b)) : wp0 b - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp_v (fun x -> wp_f x p)) let bind (a b : Type) (wp_v : wp0 a) (wp_f: a -> wp0 b) @@ -63,8 +64,8 @@ let subcomp (a:Type) (w1 w2: wp0 a) = let (m, r) = f in (m, r) -let ite_wp #a (wp1 wp2 : wp0 a) (b : bool) : wp0 a = - elim_pure_wp_monotonicity_forall (); +let ite_wp (#a:Type u#a) (wp1 wp2 : wp0 a) (b : bool) : wp0 a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp ((fun (p:a -> Type) -> (b ==> wp1 p) /\ ((~b) ==> wp2 p))) let if_then_else (a : Type) (wp1 wp2 : wp0 a) (f : repr a wp1) (g : repr a wp2) (p : bool) : Type = @@ -93,12 +94,22 @@ effect { with {repr; return; bind; subcomp; if_then_else} } -let lift_pure_nd (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) : repr a wp +let run_pure (#a:Type u#a) + (#p:a -> Type0) + (#wp:pure_wp a) + (f: unit -> PURE a wp) + (_: squash (wp p)) +: x:a{p x} += FStar.Monotonic.Pure.elim_pure #a #wp f p + +let lift_pure_nd (a:Type u#a) (wp:pure_wp a) (f:unit -> PURE a wp) : repr a wp = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; - (_, (fun (p:erased (a -> Type0)) _ -> // need the type annot - let r = f () in - assert (reveal p r); - r)) + let ff (p: erased (a -> Type0)) + (pf_wp: squash (wp p)) + : v:a{reveal p v} + = run_pure #a #(reveal p) #wp f () + in + (), ff sub_effect PURE ~> ID = lift_pure_nd diff --git a/examples/layeredeffects/ID5.fst b/examples/layeredeffects/ID5.fst index 0dfd1eebe47..ea335716398 100644 --- a/examples/layeredeffects/ID5.fst +++ b/examples/layeredeffects/ID5.fst @@ -26,11 +26,12 @@ let return (a : Type) (x : a) : repr a (return_wp x) = fun p _ -> x unfold -let bind_wp #a #b +let bind_wp (#a:Type u#a) (#b:Type u#b) (wp_v : wp a) (wp_f : (x:a -> wp b)) : wp b - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp_v (fun x -> wp_f x p)) let bind (a b : Type) (wp_v : wp a) (wp_f: a -> wp b) @@ -58,8 +59,8 @@ let subcomp (a:Type u#uu) (w1 w2:wp a) //= fun p pf -> f (hide (fun x -> reveal p x)) () unfold -let ite_wp #a (wp1 wp2 : wp a) (b : bool) : wp a = - elim_pure_wp_monotonicity_forall (); +let ite_wp (#a:Type u#a) (wp1 wp2 : wp a) (b : bool) : wp a = + elim_pure_wp_monotonicity_forall u#a (); (as_pure_wp (fun (p:a -> Type) -> (b ==> wp1 p) /\ ((~b) ==> wp2 p))) let if_then_else (a : Type) (wp1 wp2 : wp a) (f : repr a wp1) (g : repr a wp2) (p : bool) : Type = @@ -70,16 +71,16 @@ let default_if_then_else (a:Type) (wp:wp a) (f:repr a wp) (g:repr a wp) (p:bool) = repr a wp unfold -let strengthen_wp (#a:Type) (w:wp a) (p:Type0) : wp a = - elim_pure_wp_monotonicity_forall (); +let strengthen_wp (#a:Type u#a) (w:wp a) (p:Type0) : wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun post -> p /\ w post) let strengthen #a #w (p:Type0) (f : squash p -> repr a w) : repr a (strengthen_wp w p) = fun post _ -> f () post () unfold -let weaken_wp (#a:Type) (w:wp a) (p:Type0) : wp a = - elim_pure_wp_monotonicity_forall (); +let weaken_wp (#a:Type u#a) (w:wp a) (p:Type0) : wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun post -> p ==> w post) let weaken #a #w (p:Type0) (f : repr a w) : Pure (repr a (weaken_wp w p)) @@ -88,8 +89,8 @@ let weaken #a #w (p:Type0) (f : repr a w) : Pure (repr a (weaken_wp w p)) = fun post _ -> f post () unfold -let cut_wp (#a:Type) (w:wp a) (p:Type0) : wp a = - elim_pure_wp_monotonicity_forall (); +let cut_wp (#a:Type u#a) (w:wp a) (p:Type0) : wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun post -> p /\ (p ==> w post)) let cut #a #w (p:Type0) (f : repr a w) : repr a (cut_wp w p) = diff --git a/examples/layeredeffects/IteSoundness.fst b/examples/layeredeffects/IteSoundness.fst index 443743b2d29..c2420be3efd 100644 --- a/examples/layeredeffects/IteSoundness.fst +++ b/examples/layeredeffects/IteSoundness.fst @@ -45,14 +45,16 @@ let return_wp (#a:Type) (x:a) : pure_wp a = as_pure_wp (fun p -> p x) let return (a:Type) (x:a) : repr a (return_wp x) = fun () -> x unfold -let bind_wp (#a #b:Type) (wp1:pure_wp a) (wp2:a -> pure_wp b) : pure_wp b = - elim_pure_wp_monotonicity_forall (); +let bind_wp (#a:Type u#a) (#b:Type u#b) (wp1:pure_wp a) (wp2:a -> pure_wp b) : pure_wp b = + elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp1 (fun x -> wp2 x p)) -let bind (a b:Type) (wp1:pure_wp a) (wp2:a -> pure_wp b) +let bind (a:Type u#a) (b:Type u#b) (wp1:pure_wp a) (wp2:a -> pure_wp b) (f:repr a wp1) (g:(x:a -> repr b (wp2 x))) : repr b (bind_wp wp1 wp2) - = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); + = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#a (); + FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall u#b (); fun () -> let x = f () in g x () @@ -64,8 +66,8 @@ let subcomp (a:Type) (wp1 wp2:pure_wp a) (f:repr a wp1) = f unfold -let ite_wp (#a:Type) (wp_then wp_else:pure_wp a) (b:bool) : pure_wp a = - elim_pure_wp_monotonicity_forall (); +let ite_wp (#a:Type u#a) (wp_then wp_else:pure_wp a) (b:bool) : pure_wp a = + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun p -> (b ==> wp_then p) /\ ((~ b) ==> wp_else p)) let if_then_else (a:Type) (wp_then wp_else:pure_wp a) (f:repr a wp_then) (g:repr a wp_else) diff --git a/examples/layeredeffects/MSeqExn.fst b/examples/layeredeffects/MSeqExn.fst index f464e536fc8..04c94eb2786 100644 --- a/examples/layeredeffects/MSeqExn.fst +++ b/examples/layeredeffects/MSeqExn.fst @@ -124,9 +124,9 @@ let lift_pure_wp (#a:Type) (wp:pure_wp a) : wp_t a = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; fun p s0 -> wp (fun x -> p (Success x) s0) -let lift_pure_mseqexn (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) +let lift_pure_mseqexn (a:Type u#a) (wp:pure_wp a) (f:unit -> PURE a wp) : repr a (lift_pure_wp wp) -= elim_pure_wp_monotonicity_forall (); fun s0 -> Success (f ()), s0 += elim_pure_wp_monotonicity_forall u#a (); fun s0 -> Success (f ()), s0 sub_effect PURE ~> MSeqEXN = lift_pure_mseqexn diff --git a/examples/layeredeffects/ND.fst b/examples/layeredeffects/ND.fst index 6634df87062..79934194919 100644 --- a/examples/layeredeffects/ND.fst +++ b/examples/layeredeffects/ND.fst @@ -38,10 +38,11 @@ unfold let w_return x = as_pure_wp (fun p -> p x) unfold -val w_bind (#a #b : Type) : w a -> (a -> w b) -> w b +val w_bind (#a:Type u#a) (#b : Type u#b) : w a -> (a -> w b) -> w b unfold let w_bind wp1 k = - elim_pure_wp_monotonicity_forall (); + elim_pure_wp_monotonicity_forall u#a (); + elim_pure_wp_monotonicity_forall u#b (); as_pure_wp (fun p -> wp1 (fun x -> k x p)) val interp (#a : Type) : m a -> w a @@ -119,8 +120,8 @@ let ibind (a : Type) (b : Type) (wp_v : w a) (wp_f: a -> w b) (v : irepr a wp_v) let isubcomp (a:Type) (wp1 wp2: w a) (f : irepr a wp1) : Pure (irepr a wp2) (requires w_ord wp2 wp1) (ensures fun _ -> True) = f -let wp_if_then_else (#a:Type) (wp1 wp2:w a) (b:bool) : w a= - elim_pure_wp_monotonicity_forall (); +let wp_if_then_else (#a:Type u#a) (wp1 wp2:w a) (b:bool) : w a= + elim_pure_wp_monotonicity_forall u#a (); as_pure_wp (fun p -> (b ==> wp1 p) /\ ((~b) ==> wp2 p)) let i_if_then_else (a : Type) (wp1 wp2 : w a) (f : irepr a wp1) (g : irepr a wp2) (b : bool) : Type = diff --git a/examples/layeredeffects/Sec2.HIFC.fst b/examples/layeredeffects/Sec2.HIFC.fst index 3853cdeacaa..351a7cf2371 100644 --- a/examples/layeredeffects/Sec2.HIFC.fst +++ b/examples/layeredeffects/Sec2.HIFC.fst @@ -725,7 +725,7 @@ let lift_PURE_HIFC (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp) : Pure (hifc a bot bot [] (fun _ -> True) (fun s0 _ s1 -> s0 == s1)) (requires wp (fun _ -> True)) (ensures fun _ -> True) - = FStar.Monotonic.Pure.elim_pure_wp_monotonicity_forall (); + = FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp; return a (f ()) sub_effect PURE ~> HIFC = lift_PURE_HIFC diff --git a/examples/layeredeffects/Z3EncodingIssue.fst b/examples/layeredeffects/Z3EncodingIssue.fst index cccd9886479..7428f4a39ba 100644 --- a/examples/layeredeffects/Z3EncodingIssue.fst +++ b/examples/layeredeffects/Z3EncodingIssue.fst @@ -15,7 +15,6 @@ *) module Z3EncodingIssue -#set-options "--ext 'context_pruning='" // working around a quirk with unfoldings in FStar.Integers.uint_8, which gets pruned away but apparently is needed /// This module illustrates a z3 encoding issue when a layered effect is written in a particular style @@ -32,8 +31,6 @@ module Z3EncodingIssue /// /// (But all is not lost, there exists an alternative style which comes with all the goodies /// of the layered effects in this setting, see MSeqExn.fst for the alternative style) - - module Seq = FStar.Seq open FStar.Integers @@ -92,7 +89,8 @@ let subcomp (a:Type) (wp_f:wp_t a) (wp_g:wp_t a) (f:repr a wp_f) : Pure (repr a wp_g) - (requires forall p s. wp_g p s ==> wp_f p s) + (requires + (forall p s. wp_g p s ==> wp_f p s)) (ensures fun _ -> True) = f diff --git a/examples/misc/WorkingWithSquashedProofs.fst b/examples/misc/WorkingWithSquashedProofs.fst index aeaaa2faf60..e16d00351a1 100644 --- a/examples/misc/WorkingWithSquashedProofs.fst +++ b/examples/misc/WorkingWithSquashedProofs.fst @@ -31,18 +31,18 @@ val bar (a:Type) (x:a) : Type //And let's say I have a way of proving some Lemma based on a proof of this `pred` assume -val foo_pf_implies_bar (a:Type) (x:a) (pf:foo a x) - : Lemma (bar a x) +val foo_pf_implies_bar (a:Type u#a) (x:a) (pf:foo u#a u#b a x) + : Lemma (bar u#a u#0 a x) //Now, if I have `foo` in a refinement, I can still prove `bar, like so //One can use FStar.Squash.bind_squash for that, but it takes a couple of steps //expect_failure is an attribute that tells F* that this next definition will fail -[@expect_failure] //but this doesn't quite work because `bind_squash` expects a GTot function but we are giving it a Lemma, which isn't identical -let foo_implies_bar (a:Type) (x:a{foo a x}) +[@expect_failure] ///but this doesn't quite work because `bind_squash` expects a GTot function but we are giving it a Lemma, which isn't identical +let foo_implies_bar (a:Type u#a) (x:a{foo u#a u#b a x}) : Lemma (bar a x) - = let s : squash (foo a x) = () in + = let s : squash (foo u#a u#b a x) = () in FStar.Squash.bind_squash #(foo a x) #(bar a x) s (foo_pf_implies_bar a x) //So, to make it work, we need to turn a lemma into a GTot function returning a squash @@ -51,9 +51,9 @@ let lemma_as_squash #a #b ($lem: (a -> Lemma b)) (x:a) = lem x //Now, I can use FStar.Squash.bind_squash to complete the proof -let foo_implies_bar (a:Type) (x:a{foo a x}) +let foo_implies_bar (a:Type) (x:a{foo u#a u#b a x}) : Lemma (bar a x) - = FStar.Squash.bind_squash () (lemma_as_squash (foo_pf_implies_bar a x)) + = FStar.Squash.bind_squash () (lemma_as_squash (foo_pf_implies_bar u#a u#b a x)) // Another example, this time with disjunctions diff --git a/examples/native_tactics/Clear.fst b/examples/native_tactics/Clear.fst index 7d5773bf2c6..257bb97bb56 100644 --- a/examples/native_tactics/Clear.fst +++ b/examples/native_tactics/Clear.fst @@ -19,7 +19,7 @@ open FStar.Tactics.V2 assume val phi : Type assume val psi : Type -assume val xi : Type +assume val xi : Type u#0 assume val p : squash xi diff --git a/examples/native_tactics/Makefile b/examples/native_tactics/Makefile index e445de851ba..0aa9628182b 100644 --- a/examples/native_tactics/Makefile +++ b/examples/native_tactics/Makefile @@ -5,7 +5,7 @@ # 'include test.mk'. FSTAR_HOME=../.. -OTHERFLAGS += --z3version 4.13.3 +OTHERFLAGS += --z3version 4.13.3 --ext context_pruning FSTAR_EXE ?= $(FSTAR_HOME)/out/bin/fstar.exe FSTAR=$(FSTAR_EXE) $(OTHERFLAGS) diff --git a/examples/oplss2021/OPLSS2021.DijkstraMonads.fst b/examples/oplss2021/OPLSS2021.DijkstraMonads.fst index 97a1df03579..324918490b6 100644 --- a/examples/oplss2021/OPLSS2021.DijkstraMonads.fst +++ b/examples/oplss2021/OPLSS2021.DijkstraMonads.fst @@ -165,13 +165,13 @@ layered_effect { let pure a wp = unit -> PURE a wp unfold -let lift_wp (#a:Type) (#st:Type0) (w:pure_wp a) : wp st a = - elim_pure_wp_monotonicity_forall (); +let lift_wp (#a:Type u#a) (#st:Type0) (w:pure_wp a) : wp st a = + elim_pure_wp_monotonicity_forall u#a (); fun s0 p -> w (fun x -> p (x, s0)) let lift_pure_st a st wp (f : pure a wp) : repr a st (lift_wp wp) - = elim_pure_wp_monotonicity_forall (); + = elim_pure_wp_monotonicity wp; fun s0 -> (f (), s0) sub_effect PURE ~> ST = lift_pure_st diff --git a/examples/paradoxes/PrecedesRank.fst b/examples/paradoxes/PrecedesRank.fst index ccf687bf3dc..743a9ade4a5 100644 --- a/examples/paradoxes/PrecedesRank.fst +++ b/examples/paradoxes/PrecedesRank.fst @@ -64,6 +64,6 @@ let diag (r:ras) : Lemma (r.rank pid > r.rank pid) = () (* We obviously get false from that. *) -let falso () : Lemma (~(exists (r:ras). True)) = - let aux (r:ras) : Lemma (True ==> False) = diag r in +let falso () : Lemma (~(exists (r:ras u#0). True)) = + let aux (r:ras u#0) : Lemma (True ==> False) = diag r in Classical.forall_to_exists aux diff --git a/examples/tactics/Postprocess.fst b/examples/tactics/Postprocess.fst index ff0f320a4c4..b94d96436d5 100644 --- a/examples/tactics/Postprocess.fst +++ b/examples/tactics/Postprocess.fst @@ -69,14 +69,18 @@ let q_as_lem (#a:Type) (#b:a -> Type) (p:squash (forall x. b x)) (x:a) : Lemma (b x) = () -let congruence_fun #a (#b:a -> Type) (f g:(x:a -> b x)) (x:squash (forall x. f x == g x)) : +let congruence_fun (#a:Type u#a) (#b:a -> Type u#b) (f g:(x:a -> b x)) (x:squash (forall x. f x == g x)) : Lemma (ensures (fun (x:a) -> f x) == (fun (x:a) -> g x)) = assert ((fun (x:a) -> f x) == (fun (x:a) -> g x)) by (l_to_r [quote (q_as_lem x)]; - trefl()) - -let apply_feq_lem #a #b ($f $g : a -> b) : Lemma (requires (forall x. f x == g x)) - (ensures ((fun x -> f x) == (fun x -> g x))) = congruence_fun f g () + trefl()) + +let apply_feq_lem (#a:Type u#a) (#b:Type u#b) ($f $g : a -> b) + : Lemma + (requires (forall x. f x == g x)) + (ensures ((fun x -> f x) == (fun x -> g x))) += assert ((fun x -> f x) == (fun x -> g x)) + by (mapply (`congruence_fun)) let fext () = apply_lemma (`apply_feq_lem); dismiss (); ignore (forall_intros ())