From fddd9b1b03bcba1fc2d15eb5337280845e7f0c51 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 3 Oct 2024 09:34:53 -0700 Subject: [PATCH 1/5] Replace must_erase_during_extraction with erasable. --- src/typechecker/FStarC.TypeChecker.Env.fst | 11 +-- src/typechecker/FStarC.TypeChecker.Env.fsti | 4 + .../FStarC.TypeChecker.Normalize.fst | 2 + src/typechecker/FStarC.TypeChecker.Quals.fst | 78 +++++++++---------- src/typechecker/FStarC.TypeChecker.Quals.fsti | 1 - src/typechecker/FStarC.TypeChecker.Util.fst | 37 +-------- .../MustEraseForExtraction.fst | 3 +- .../MustEraseForExtraction.fsti | 4 +- ulib/FStar.Attributes.fsti | 14 +--- ulib/FStar.GSet.fsti | 5 +- ulib/FStar.GhostSet.fsti | 2 +- ulib/FStar.Monotonic.HyperHeap.fsti | 5 +- ulib/FStar.TSet.fst | 3 - ulib/FStar.TSet.fsti | 5 +- 14 files changed, 58 insertions(+), 116 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index 5d666167725..edc7dcc93e3 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -945,13 +945,8 @@ let cache_in_fv_tab (tab:SMap.t 'a) (fv:fv) (f:unit -> (bool & 'a)) : 'a = let fv_has_erasable_attr env fv = let f () = let ex, erasable = fv_exists_and_has_attr env fv.fv_name.v Const.erasable_attr in - ex,erasable - //unfortunately, treating the Const.must_erase_for_extraction_attr - //in the same way here as erasable_attr leads to regressions in fragile proofs, - //notably in FStar.ModifiesGen, since this expands the class of computation types - //that can be promoted from ghost to tot. That in turn results in slightly different - //smt encodings, leading to breakages. So, sadly, I'm not including must_erase_for_extraction - //here. In any case, must_erase_for_extraction is transitionary and should be removed + let ex, must_erase_for_extraction = fv_exists_and_has_attr env fv.fv_name.v Const.must_erase_for_extraction_attr in + ex, erasable || must_erase_for_extraction in cache_in_fv_tab env.erasable_types_tab fv f @@ -1047,10 +1042,12 @@ let rec non_informative env t = || fv_eq_lid fv Const.erased_lid || fv_has_erasable_attr env fv | Tm_app {hd=head} -> non_informative env head + | Tm_abs {body} -> non_informative env body | Tm_uinst (t, _) -> non_informative env t | Tm_arrow {comp=c} -> (is_pure_or_ghost_comp c && non_informative env (comp_result c)) || is_erasable_effect env (comp_effect_name c) + | Tm_meta {tm} -> non_informative env tm | _ -> false let num_effect_indices env name r = diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti index 4e628b59330..74cb984e048 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -347,7 +347,11 @@ val fv_with_lid_has_attr : env -> fv_lid:lid -> attr_lid:lid -> bool val fv_has_attr : env -> fv -> attr_lid:lid -> bool val fv_has_strict_args : env -> fv -> option (list int) val fv_has_erasable_attr : env -> fv -> bool + +(* `non_informative env t` is true if the type family `t: (... -> Type) is noninformative, + i.e., any `x: t ...` can be erased to `()`. *) val non_informative : env -> typ -> bool + val try_lookup_effect_lid : env -> lident -> option term val lookup_effect_lid : env -> lident -> term val lookup_effect_abbrev : env -> universes -> lident -> option (binders & comp) diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index c82e3531151..95e9ac3950a 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -2774,6 +2774,8 @@ let non_info_norm env t = let steps = [UnfoldUntil delta_constant; AllowUnboundUniverses; EraseUniverses; + Primops; + Beta; Iota; HNF; (* We could use Weak too were it not that we need * to descend in the codomain of arrows. *) diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fst b/src/typechecker/FStarC.TypeChecker.Quals.fst index 402d8396dfe..e84fb41b613 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fst +++ b/src/typechecker/FStarC.TypeChecker.Quals.fst @@ -199,6 +199,26 @@ let check_sigelt_quals_pre (env:FStarC.TypeChecker.Env.env) se = then err [] | _ -> () +// A faster under-approximation of non_info_norm. +// We call this function on every let-binding that has an interface val +// (while non_info_norm is only called on types), +// so it needs to be fast and shouldn't unfold too much. +// The regular non_info_norm doesn't set Weak, +// which makes the normalizer reduce lets. +let non_info_norm_weak env t = + let steps = [UnfoldUntil delta_constant; + AllowUnboundUniverses; + EraseUniverses; + Primops; + Beta; Iota; + HNF; + Weak; + Unascribe; //remove ascriptions + ForExtraction //and refinement types + ] + in + non_informative env (N.normalize steps env t) + let check_erasable env quals (r:Range.range) se = let lids = U.lids_of_sigelt se in let val_exists = @@ -221,6 +241,22 @@ let check_erasable env quals (r:Range.range) se = text "Mismatch of attributes between declaration and definition."; text "Definition is marked `erasable` but the declaration is not."; ]; + if not se_has_erasable_attr && not (Options.ide ()) then begin + match se.sigel with + | Sig_let {lbs=(false, [lb])} -> + let lbname = BU.right lb.lbname in + let has_iface_val = match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with + | Some iface_decls -> iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v)) + | None -> false in + let _, body, _ = U.abs_formals lb.lbdef in + if has_iface_val && non_info_norm_weak env body then log_issue lbname Error_MustEraseMissing [ + text (BU.format1 "Values of type `%s` will be erased during extraction, \ + but its interface hides this fact." (show lbname)); + text (BU.format1 "Add the `erasable` \ + attribute to the `val %s` declaration for this symbol in the interface" (show lbname)); + ] + | _ -> () + end; if se_has_erasable_attr then begin match se.sigel with @@ -259,47 +295,6 @@ let check_erasable env quals (r:Range.range) se = ] end -(* - * Given `val t : Type` in an interface - * and `let t = e` in the corresponding implementation - * The val declaration should contains the `must_erase_for_extraction` attribute - * if and only if `e` is a type that's non-informative (e..g., unit, t -> unit, etc.) - *) -let check_must_erase_attribute env se = - if Options.ide() then () else - match se.sigel with - | Sig_let {lbs; lids=l} -> - begin match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with - | None -> - () - - | Some iface_decls -> - snd lbs |> List.iter (fun lb -> - let lbname = BU.right lb.lbname in - let has_iface_val = - iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v)) - in - if has_iface_val - then - let must_erase = TcUtil.must_erase_for_extraction env lb.lbdef in - let has_attr = Env.fv_has_attr env lbname C.must_erase_for_extraction_attr in - if must_erase && not has_attr - then log_issue lbname Error_MustEraseMissing [ - text (BU.format1 "Values of type `%s` will be erased during extraction, \ - but its interface hides this fact." (show lbname)); - text (BU.format1 "Add the `must_erase_for_extraction` \ - attribute to the `val %s` declaration for this symbol in the interface" (show lbname)); - ] - else if has_attr && not must_erase - then log_issue lbname Error_MustEraseMissing [ - text (BU.format1 "Values of type `%s` cannot be erased during extraction, \ - but the `must_erase_for_extraction` attribute claims that it can." - (show lbname)); - text "Please remove the attribute."; - ]) - end - | _ -> () - let check_typeclass_instance_attribute env (rng:Range.range) se = let is_tc_instance = se.sigattrs |> BU.for_some @@ -354,6 +349,5 @@ let check_sigelt_quals_post env se = let quals = se.sigquals in let r = se.sigrng in check_erasable env quals r se; - check_must_erase_attribute env se; check_typeclass_instance_attribute env r se; () diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fsti b/src/typechecker/FStarC.TypeChecker.Quals.fsti index 4bd5660dade..9331ec254cf 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fsti +++ b/src/typechecker/FStarC.TypeChecker.Quals.fsti @@ -28,7 +28,6 @@ after the function is typechecked. Currently, the only things that must be checked after the function is typechecked are: - The erasable attribute, since the defn must be elaborated. See #3253. -- The must_erase attribute - The instance attribute for typeclasses *) diff --git a/src/typechecker/FStarC.TypeChecker.Util.fst b/src/typechecker/FStarC.TypeChecker.Util.fst index ff705aff598..af9c8e66d12 100644 --- a/src/typechecker/FStarC.TypeChecker.Util.fst +++ b/src/typechecker/FStarC.TypeChecker.Util.fst @@ -3251,40 +3251,9 @@ let maybe_add_implicit_binders (env:env) (bs:binders) : binders = let must_erase_for_extraction (g:env) (t:typ) = - let rec descend env t = //t is expected to b in WHNF - match (SS.compress t).n with - | Tm_arrow _ -> - let bs, c = U.arrow_formals_comp t in - let env = FStarC.TypeChecker.Env.push_binders env bs in - (Env.is_erasable_effect env (U.comp_effect_name c)) //includes GHOST - || (U.is_pure_or_ghost_comp c && aux env (U.comp_result c)) - | Tm_refine {b={sort=t}} -> - aux env t - | Tm_app {hd=head} - | Tm_uinst (head, _) -> - descend env head - | Tm_fvar fv -> - //special treatment for must_erase_for_extraction here - //See Env.type_is_erasable for more explanations - Env.fv_has_attr env fv C.must_erase_for_extraction_attr - | _ -> false - and aux env t = - let t = N.normalize [Env.Primops; - Env.Weak; - Env.HNF; - Env.UnfoldUntil delta_constant; - Env.Beta; - Env.AllowUnboundUniverses; - Env.Zeta; - Env.Iota; - Env.Unascribe] env t in -// debug g (fun () -> BU.print1 "aux %s\n" (show t)); - let res = Env.non_informative env t || descend env t in - if !dbg_Extraction - then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t); - res - in - aux g t + let res = N.non_info_norm g t in + if !dbg_Extraction then BU.print2 "must_erase=%s: %s\n" (if res then "true" else "false") (show t); + res let effect_extraction_mode env l = l |> Env.norm_eff_name env diff --git a/tests/micro-benchmarks/MustEraseForExtraction.fst b/tests/micro-benchmarks/MustEraseForExtraction.fst index c7d7c873c3e..554cd54bcd7 100644 --- a/tests/micro-benchmarks/MustEraseForExtraction.fst +++ b/tests/micro-benchmarks/MustEraseForExtraction.fst @@ -17,7 +17,8 @@ module MustEraseForExtraction [@@(expect_failure [318])] let t1 = unit +[@@erasable] let t2 = unit -[@@(expect_failure [318])] +[@@(expect_failure [162])] let t3 = bool diff --git a/tests/micro-benchmarks/MustEraseForExtraction.fsti b/tests/micro-benchmarks/MustEraseForExtraction.fsti index bfd3f977621..e87b4614a03 100644 --- a/tests/micro-benchmarks/MustEraseForExtraction.fsti +++ b/tests/micro-benchmarks/MustEraseForExtraction.fsti @@ -17,8 +17,8 @@ module MustEraseForExtraction val t1 : Type0 -[@@must_erase_for_extraction] +[@@erasable] val t2 : Type0 -[@@must_erase_for_extraction] +[@@erasable] val t3 : Type0 diff --git a/ulib/FStar.Attributes.fsti b/ulib/FStar.Attributes.fsti index b36c911124b..6b3db8ec794 100644 --- a/ulib/FStar.Attributes.fsti +++ b/ulib/FStar.Attributes.fsti @@ -119,19 +119,7 @@ val tcnorm : unit construction to track position information in generated VCs *) val dm4f_bind_range : unit -(** We erase all ghost functions and unit-returning pure functions to - [()] at extraction. This creates a small issue with abstract - types. Consider a module that defines an abstract type [t] whose - (internal) definition is [unit] and also defines [f: int -> t]. [f] - would be erased to be just [()] inside the module, while the - client calls to [f] would not, since [t] is abstract. To get - around this, when extracting interfaces, if we encounter an - abstract type, we tag it with this attribute, so that - extraction can treat it specially. - - Note, since the use of cross-module inlining (the [--cmi] option), - this attribute is no longer necessary. We retain it for legacy, - but will remove it in the future. *) +[@@deprecated "use [@@erasable] instead"] val must_erase_for_extraction : unit (** When attached a top-level definition, the typechecker will succeed diff --git a/ulib/FStar.GSet.fsti b/ulib/FStar.GSet.fsti index 408496dc2c8..d6b5c10f943 100644 --- a/ulib/FStar.GSet.fsti +++ b/ulib/FStar.GSet.fsti @@ -18,10 +18,7 @@ module FStar.GSet (** Computational sets (on Types): membership is a boolean function *) #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" -(* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in - *) -[@@must_erase_for_extraction] +[@@erasable] val set (a: Type u#a) : Type u#a val equal (#a:Type) (s1:set a) (s2:set a) : Type0 diff --git a/ulib/FStar.GhostSet.fsti b/ulib/FStar.GhostSet.fsti index 239423a4e6c..dd52e6b1214 100644 --- a/ulib/FStar.GhostSet.fsti +++ b/ulib/FStar.GhostSet.fsti @@ -18,7 +18,7 @@ module FStar.GhostSet (** Ghost computational sets: membership is a ghost boolean function *) #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" -[@@must_erase_for_extraction; erasable] +[@@erasable] val set (a: Type u#a) : Type u#a let decide_eq a = x:a -> y:a -> GTot (b:bool { b <==> (x==y) }) diff --git a/ulib/FStar.Monotonic.HyperHeap.fsti b/ulib/FStar.Monotonic.HyperHeap.fsti index 927f269cbaa..f470ef331ba 100644 --- a/ulib/FStar.Monotonic.HyperHeap.fsti +++ b/ulib/FStar.Monotonic.HyperHeap.fsti @@ -27,10 +27,7 @@ open FStar.Ghost * Clients should not open/know about HyperHeap, they should work only with HyperStack *) -(* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in - *) -[@@must_erase_for_extraction] +[@@erasable] val rid :eqtype val reveal (r:rid) :GTot (list (int & int)) diff --git a/ulib/FStar.TSet.fst b/ulib/FStar.TSet.fst index 8c4f3c15ea9..14a23730d6d 100644 --- a/ulib/FStar.TSet.fst +++ b/ulib/FStar.TSet.fst @@ -20,9 +20,6 @@ module FStar.TSet #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" module F = FStar.FunctionalExtensionality -(* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in - *) [@@erasable] let set a = F.restricted_t a (fun _ -> prop) diff --git a/ulib/FStar.TSet.fsti b/ulib/FStar.TSet.fsti index 47f99d567c9..7771132c2f5 100644 --- a/ulib/FStar.TSet.fsti +++ b/ulib/FStar.TSet.fsti @@ -19,10 +19,7 @@ module FStar.TSet #set-options "--initial_fuel 0 --max_fuel 0 --initial_ifuel 0 --max_ifuel 0" -(* - * AR: mark it must_erase_for_extraction temporarily until CMI comes in - *) -[@@must_erase_for_extraction; erasable] +[@@erasable] val set (a:Type u#a) : Type u#(max 1 a) val equal (#a:Type) (s1:set a) (s2:set a) : prop From 35a435e8a095d9982f8e9c7dde15bcf95b4b736a Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 9 Jan 2025 19:05:45 -0800 Subject: [PATCH 2/5] Suppress erasable warning for props. --- src/typechecker/FStarC.TypeChecker.Env.fst | 7 +++++++ src/typechecker/FStarC.TypeChecker.Env.fsti | 5 +++++ .../FStarC.TypeChecker.Normalize.fst | 15 +++++++++++++ .../FStarC.TypeChecker.Normalize.fsti | 1 + src/typechecker/FStarC.TypeChecker.Quals.fst | 21 ++++++++++++------- 5 files changed, 42 insertions(+), 7 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Env.fst b/src/typechecker/FStarC.TypeChecker.Env.fst index edc7dcc93e3..c9daa2a809f 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fst +++ b/src/typechecker/FStarC.TypeChecker.Env.fst @@ -1050,6 +1050,13 @@ let rec non_informative env t = | Tm_meta {tm} -> non_informative env tm | _ -> false +let rec non_informative_sort t = + match (U.unrefine t).n with + | Tm_fvar fv when fv_eq_lid fv Const.prop_lid -> true + | Tm_arrow {comp=c} -> non_informative_sort (comp_result c) + | Tm_meta {tm} -> non_informative_sort tm + | _ -> false + let num_effect_indices env name r = let sig_t = name |> lookup_effect_lid env |> SS.compress in match sig_t.n with diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti index 74cb984e048..f4175e2072d 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -352,6 +352,11 @@ val fv_has_erasable_attr : env -> fv -> bool i.e., any `x: t ...` can be erased to `()`. *) val non_informative : env -> typ -> bool +(* `non_informative_sort t` is `true` if the type family `t: ... -> Type` only ranges over noninformative types, + i.e., any `x: s ...` such that `s ... : t ...` can be erased. + (practically, this means that `t` is of the form `... -> prop`) *) +val non_informative_sort : typ -> bool + val try_lookup_effect_lid : env -> lident -> option term val lookup_effect_lid : env -> lident -> term val lookup_effect_abbrev : env -> universes -> lident -> option (binders & comp) diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index 95e9ac3950a..14090cadf33 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -2785,6 +2785,21 @@ let non_info_norm env t = in non_informative env (normalize steps env t) +let non_info_sort_norm env t = + let steps = [UnfoldUntil (Env.delta_depth_of_fv env (S.fvconst PC.prop_lid)); // do not unfold prop + AllowUnboundUniverses; + EraseUniverses; + Primops; + Beta; Iota; + HNF; + (* We could use Weak too were it not that we need + * to descend in the codomain of arrows. *) + Unascribe; //remove ascriptions + ForExtraction //and refinement types + ] + in + non_informative_sort (normalize steps env t) + (* * Ghost T to Pure T promotion * diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fsti b/src/typechecker/FStarC.TypeChecker.Normalize.fsti index 207b25966ba..31231590b60 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fsti +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fsti @@ -35,6 +35,7 @@ val unfold_whnf': steps -> Env.env -> term -> term val unfold_whnf: Env.env -> term -> term val reduce_uvar_solutions:Env.env -> term -> term val non_info_norm: Env.env -> term -> bool +val non_info_sort_norm: Env.env -> term -> bool (* * The maybe versions of ghost_to_pure only promote diff --git a/src/typechecker/FStarC.TypeChecker.Quals.fst b/src/typechecker/FStarC.TypeChecker.Quals.fst index e84fb41b613..a7def04741d 100644 --- a/src/typechecker/FStarC.TypeChecker.Quals.fst +++ b/src/typechecker/FStarC.TypeChecker.Quals.fst @@ -248,13 +248,20 @@ let check_erasable env quals (r:Range.range) se = let has_iface_val = match DsEnv.iface_decls (Env.dsenv env) (Env.current_module env) with | Some iface_decls -> iface_decls |> BU.for_some (Parser.AST.decl_is_val (ident_of_lid lbname.fv_name.v)) | None -> false in - let _, body, _ = U.abs_formals lb.lbdef in - if has_iface_val && non_info_norm_weak env body then log_issue lbname Error_MustEraseMissing [ - text (BU.format1 "Values of type `%s` will be erased during extraction, \ - but its interface hides this fact." (show lbname)); - text (BU.format1 "Add the `erasable` \ - attribute to the `val %s` declaration for this symbol in the interface" (show lbname)); - ] + let val_decl = Env.try_lookup_val_decl env lbname.fv_name.v in + if has_iface_val && Some? val_decl then + let _, body, _ = U.abs_formals lb.lbdef in + let Some ((us, t), _) = val_decl in + let known_to_be_erasable = + let env = Env.push_univ_vars env us in + N.non_info_sort_norm env t in + if not known_to_be_erasable && non_info_norm_weak env body then + log_issue lbname Error_MustEraseMissing [ + text (BU.format1 "Values of type `%s` will be erased during extraction, \ + but its interface hides this fact." (show lbname)); + text (BU.format1 "Add the `erasable` \ + attribute to the `val %s` declaration for this symbol in the interface" (show lbname)); + ] | _ -> () end; if se_has_erasable_attr From a1349cb4b96e30fe9e28cc8c84670d737b0f3116 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 13 Jan 2025 10:36:47 -0800 Subject: [PATCH 3/5] Fix test. --- tests/tactics/Postprocess.fst.output.expected | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/tactics/Postprocess.fst.output.expected b/tests/tactics/Postprocess.fst.output.expected index 94c1f77bf15..37e5d29a3f9 100644 --- a/tests/tactics/Postprocess.fst.output.expected +++ b/tests/tactics/Postprocess.fst.output.expected @@ -482,11 +482,11 @@ in [@ ] visible let apply_feq_lem : ($f:(uu___:a@1:(Tm_unknown) -> Tot b@1:(Tm_unknown)) -> $g:(uu___:a@2:(Tm_unknown) -> Tot b@2:(Tm_unknown)) -> Lemma (unit)) = (fun $f $g -> (congruence_fun f@1:(Tm_unknown) g@0:(Tm_unknown) ())) [@ ] -visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1096 : unit = (apply_lemma `(apply_feq_lem)[]) +visible let fext : (uu___:unit -> Tac (unit)) = (fun uu___ -> let uu___#1098 : unit = (apply_lemma `(apply_feq_lem)[]) in -let uu___#1097 : unit = (dismiss ()) +let uu___#1099 : unit = (dismiss ()) in -let uu___#1098 : (list binding) = (forall_intros ()) +let uu___#1100 : (list binding) = (forall_intros ()) in (ignore uu___@0:(Tm_unknown))) [@ ] From 54a64c4d751ba6a29155604bfb4ac613de5e507f Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 25 Jun 2025 10:14:22 -0700 Subject: [PATCH 4/5] Remove some erasable warnings. --- ulib/FStar.Fin.fsti | 6 +++--- ulib/FStar.GSet.fsti | 4 ++-- ulib/FStar.GhostSet.fsti | 4 ++-- ulib/FStar.Pervasives.fsti | 4 ++-- ulib/FStar.Seq.Properties.fsti | 2 +- ulib/FStar.Set.fsti | 2 +- ulib/FStar.WellFounded.fst | 1 + ulib/experimental/FStar.Sequence.Base.fsti | 6 +++--- 8 files changed, 15 insertions(+), 14 deletions(-) diff --git a/ulib/FStar.Fin.fsti b/ulib/FStar.Fin.fsti index f00030d4f63..4db9b0ff413 100644 --- a/ulib/FStar.Fin.fsti +++ b/ulib/FStar.Fin.fsti @@ -90,9 +90,9 @@ type binary_relation (a: Type) = a -> a -> bool Use reveal_opaque when you really need it. Or use refl/trans/symm lemmas below to keep the context clean. *) -val is_reflexive (#a:Type) (r: binary_relation a) : Type0 -val is_symmetric (#a:Type) (r: binary_relation a) : Type0 -val is_transitive (#a:Type) (r: binary_relation a) : Type0 +val is_reflexive (#a:Type) (r: binary_relation a) : prop +val is_symmetric (#a:Type) (r: binary_relation a) : prop +val is_transitive (#a:Type) (r: binary_relation a) : prop val is_reflexive_intro (#a:Type) (r: binary_relation a) : Lemma (requires forall (x:a). r x x) (ensures is_reflexive r) diff --git a/ulib/FStar.GSet.fsti b/ulib/FStar.GSet.fsti index d6b5c10f943..18223d0baaa 100644 --- a/ulib/FStar.GSet.fsti +++ b/ulib/FStar.GSet.fsti @@ -21,7 +21,7 @@ module FStar.GSet [@@erasable] val set (a: Type u#a) : Type u#a -val equal (#a:Type) (s1:set a) (s2:set a) : Type0 +val equal (#a:Type) (s1:set a) (s2:set a) : prop (* destructors *) @@ -41,7 +41,7 @@ let disjoint (#a:Type) (s1: set a) (s2: set a) = equal (intersect s1 s2) empty (* ops *) -type subset (#a:Type) (s1:set a) (s2:set a) :Type0 = forall x. mem x s1 ==> mem x s2 +type subset (#a:Type) (s1:set a) (s2:set a) :prop = forall x. mem x s1 ==> mem x s2 (* Properties *) val mem_empty: #a:Type -> x:a -> Lemma diff --git a/ulib/FStar.GhostSet.fsti b/ulib/FStar.GhostSet.fsti index dd52e6b1214..b5c677157a3 100644 --- a/ulib/FStar.GhostSet.fsti +++ b/ulib/FStar.GhostSet.fsti @@ -23,7 +23,7 @@ val set (a: Type u#a) : Type u#a let decide_eq a = x:a -> y:a -> GTot (b:bool { b <==> (x==y) }) -val equal (#a:Type) (s1:set a) (s2:set a) : Type0 +val equal (#a:Type) (s1:set a) (s2:set a) : prop (* destructors *) @@ -43,7 +43,7 @@ let disjoint (#a:Type) (s1: set a) (s2: set a) = equal (intersect s1 s2) empty (* ops *) -type subset (#a:Type) (s1:set a) (s2:set a) :Type0 = forall x. mem x s1 ==> mem x s2 +type subset (#a:Type) (s1:set a) (s2:set a) :prop = forall x. mem x s1 ==> mem x s2 (* Properties *) val mem_empty: #a:Type -> x:a -> Lemma diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index b940c7d0079..83e45a14af6 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -141,7 +141,7 @@ let trivial_pure_post (a: Type) : pure_post a = fun _ -> True Use [intro_ambient t] for that. See, e.g., LowStar.Monotonic.Buffer.fst and its usage there for loc_none *) [@@ remove_unused_type_parameters [0; 1;]] -val ambient (#a: Type) (x: a) : Type0 +val ambient (#a: Type) (x: a) : prop (** cf. [ambient], above *) val intro_ambient (#a: Type) (x: a) : Tot (squash (ambient x)) @@ -566,7 +566,7 @@ new_effect { setting. If used unwisely, this can lead to very poor SMT solver performance. *) [@@ remove_unused_type_parameters [0]] -val inversion (a: Type) : Type0 +val inversion (a: Type) : prop (** To introduce [inversion t] in the SMT solver's context, call [allow_inversion t]. *) diff --git a/ulib/FStar.Seq.Properties.fsti b/ulib/FStar.Seq.Properties.fsti index 0f5bb3513e6..cbfe4bcdf05 100644 --- a/ulib/FStar.Seq.Properties.fsti +++ b/ulib/FStar.Seq.Properties.fsti @@ -462,7 +462,7 @@ val lemma_index_is_nth: #a:Type -> s:seq a -> i:nat{i < length s} -> Lemma // for when the sequence payload is not an eqtype //////////////////////////////////////////////////////////////////////////////// [@@ remove_unused_type_parameters [0; 1; 2]] -val contains (#a:Type) (s:seq a) (x:a) : Tot Type0 +val contains (#a:Type) (s:seq a) (x:a) : Tot prop val contains_intro (#a:Type) (s:seq a) (k:nat) (x:a) : Lemma (k < Seq.length s /\ Seq.index s k == x diff --git a/ulib/FStar.Set.fsti b/ulib/FStar.Set.fsti index c9f3a78e02c..d545e7f4e47 100644 --- a/ulib/FStar.Set.fsti +++ b/ulib/FStar.Set.fsti @@ -23,7 +23,7 @@ val set (a:eqtype) : Type0 val equal (#a:eqtype) (s1:set a) (s2:set a) - : Type0 + : prop (* destructors *) diff --git a/ulib/FStar.WellFounded.fst b/ulib/FStar.WellFounded.fst index eab78d99e16..04f9989ba8d 100644 --- a/ulib/FStar.WellFounded.fst +++ b/ulib/FStar.WellFounded.fst @@ -40,6 +40,7 @@ type acc (#a:Type u#a) (r:binrel u#a u#r a) (x:a) : Type u#(max a r) = (* * A binrel r is well-founded if every element is accessible *) +[@@ erasable] let well_founded (#a:Type u#a) (r:binrel u#a u#r a) = x:a -> acc r x (* diff --git a/ulib/experimental/FStar.Sequence.Base.fsti b/ulib/experimental/FStar.Sequence.Base.fsti index 0c4246ccbb1..3f48f410363 100644 --- a/ulib/experimental/FStar.Sequence.Base.fsti +++ b/ulib/experimental/FStar.Sequence.Base.fsti @@ -100,7 +100,7 @@ val update: #ty: Type -> s: seq ty -> i: nat{i < length s} -> ty -> seq ty /// /// function Seq#Contains(Seq T, T): bool; -val contains: #ty: Type -> seq ty -> ty -> Type0 +val contains: #ty: Type -> seq ty -> ty -> prop /// We represent the Dafny function `Seq#Take` with `take`: /// @@ -120,7 +120,7 @@ val drop: #ty: Type -> s: seq ty -> howMany: nat{howMany <= length s} -> seq ty /// /// We also provide the infix symbol `$==` for it. -val equal: #ty: Type -> seq ty -> seq ty -> Type0 +val equal: #ty: Type -> seq ty -> seq ty -> prop let ($==) = equal /// Instead of representing the Dafny function `Seq#SameUntil`, which @@ -131,7 +131,7 @@ let ($==) = equal /// /// We also provide the infix notation `$<=` for it. -val is_prefix: #ty: Type -> seq ty -> seq ty -> Type0 +val is_prefix: #ty: Type -> seq ty -> seq ty -> prop let ($<=) = is_prefix /// We represent the Dafny function `Seq#Rank` with `rank`. From 9f26644e3417bad1ac0158f982199e2544c4da01 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Thu, 3 Jul 2025 14:43:32 -0700 Subject: [PATCH 5/5] Fix test. --- examples/Cfg.fst.config.json | 1 + examples/crypto/OPLSS.AE.fst | 2 ++ 2 files changed, 3 insertions(+) diff --git a/examples/Cfg.fst.config.json b/examples/Cfg.fst.config.json index c35b2567495..d9b2f6248bf 100644 --- a/examples/Cfg.fst.config.json +++ b/examples/Cfg.fst.config.json @@ -5,5 +5,6 @@ "--z3version", "4.13.3" ], "include_dirs": [ + "crypto" ] } diff --git a/examples/crypto/OPLSS.AE.fst b/examples/crypto/OPLSS.AE.fst index 9af29ff6b94..a109b46a5f4 100644 --- a/examples/crypto/OPLSS.AE.fst +++ b/examples/crypto/OPLSS.AE.fst @@ -238,6 +238,7 @@ let keygen () = Key ka ke +#push-options "--z3rlimit 10" /// encrypt: /// We return a cipher, preserve the invariant, /// and extend the log by exactly one entry @@ -245,6 +246,7 @@ let encrypt k plain = let c = CPA.encrypt k.enc plain in let t = MAC.mac k.mac c in (c, t) +#pop-options /// decrypt: /// In the ideal case, we prove it functionally correct and secure