From b8985903184fae37197c3a6fb278f2056b76e105 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 5 Dec 2024 16:00:08 -0800 Subject: [PATCH 1/6] Introduce UnfoldOnce normalizer step (scaffolding only) --- src/parser/FStarC.Parser.Const.fst | 1 + src/syntax/FStarC.Syntax.Embeddings.fst | 7 +++++++ src/typechecker/FStarC.TypeChecker.Cfg.fst | 6 ++++++ src/typechecker/FStarC.TypeChecker.Cfg.fsti | 1 + src/typechecker/FStarC.TypeChecker.Env.fsti | 1 + ulib/FStar.Pervasives.fst | 4 ++++ ulib/FStar.Pervasives.fsti | 7 +++++++ 7 files changed, 27 insertions(+) diff --git a/src/parser/FStarC.Parser.Const.fst b/src/parser/FStarC.Parser.Const.fst index 14bee4d37ca..d698f4819b7 100644 --- a/src/parser/FStarC.Parser.Const.fst +++ b/src/parser/FStarC.Parser.Const.fst @@ -323,6 +323,7 @@ let steps_delta = psconst "delta" let steps_reify = psconst "reify_" let steps_norm_debug = psconst "norm_debug" let steps_unfoldonly = psconst "delta_only" +let steps_unfoldonce = psconst "delta_once" let steps_unfoldfully = psconst "delta_fully" let steps_unfoldattr = psconst "delta_attr" let steps_unfoldqual = psconst "delta_qualifier" diff --git a/src/syntax/FStarC.Syntax.Embeddings.fst b/src/syntax/FStarC.Syntax.Embeddings.fst index 008305ef41f..f8c6e13d094 100644 --- a/src/syntax/FStarC.Syntax.Embeddings.fst +++ b/src/syntax/FStarC.Syntax.Embeddings.fst @@ -798,6 +798,7 @@ let steps_Iota = tconst PC.steps_iota let steps_Reify = tconst PC.steps_reify let steps_NormDebug = tconst PC.steps_norm_debug let steps_UnfoldOnly = tconst PC.steps_unfoldonly +let steps_UnfoldOnce = tconst PC.steps_unfoldonce let steps_UnfoldFully = tconst PC.steps_unfoldonly let steps_UnfoldAttr = tconst PC.steps_unfoldattr let steps_UnfoldQual = tconst PC.steps_unfoldqual @@ -848,6 +849,9 @@ let e_norm_step : embedding Pervasives.norm_step = | UnfoldOnly l -> S.mk_Tm_app steps_UnfoldOnly [S.as_arg (embed l rng None norm)] rng + | UnfoldOnce l -> + S.mk_Tm_app steps_UnfoldOnce [S.as_arg (embed l rng None norm)] + rng | UnfoldFully l -> S.mk_Tm_app steps_UnfoldFully [S.as_arg (embed l rng None norm)] rng @@ -902,6 +906,9 @@ let e_norm_step : embedding Pervasives.norm_step = | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonly -> BU.bind_opt (try_unembed l norm) (fun ss -> Some <| UnfoldOnly ss) + | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldonce -> + BU.bind_opt (try_unembed l norm) (fun ss -> + Some <| UnfoldOnce ss) | Tm_fvar fv, [(l, _)] when S.fv_eq_lid fv PC.steps_unfoldfully -> BU.bind_opt (try_unembed l norm) (fun ss -> Some <| UnfoldFully ss) diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fst b/src/typechecker/FStarC.TypeChecker.Cfg.fst index 7b3d35965e2..16d03eb98e4 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fst +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fst @@ -46,6 +46,7 @@ let steps_to_string f = do_not_unfold_pure_lets = %s;\n\ unfold_until = %s;\n\ unfold_only = %s;\n\ + unfold_once = %s;\n\ unfold_fully = %s;\n\ unfold_attr = %s;\n\ unfold_qual = %s;\n\ @@ -78,6 +79,7 @@ let steps_to_string f = f.do_not_unfold_pure_lets |> show; f.unfold_until |> show; f.unfold_only |> show; + f.unfold_once |> show; f.unfold_fully |> show; f.unfold_attr |> show; f.unfold_qual |> show; @@ -149,6 +151,7 @@ let default_steps : fsteps = { do_not_unfold_pure_lets = false; unfold_until = None; unfold_only = None; + unfold_once = None; unfold_fully = None; unfold_attr = None; unfold_qual = None; @@ -191,6 +194,7 @@ let fstep_add_one s fs = | DoNotUnfoldPureLets -> { fs with do_not_unfold_pure_lets = true } | UnfoldUntil d -> { fs with unfold_until = Some d } | UnfoldOnly lids -> { fs with unfold_only = Some lids } + | UnfoldOnce lids -> { fs with unfold_once = Some lids } | UnfoldFully lids -> { fs with unfold_fully = Some lids } | UnfoldAttr lids -> { fs with unfold_attr = Some lids } | UnfoldQual strs -> @@ -459,6 +463,8 @@ let translate_norm_step = function | Pervasives.NormDebug -> [NormDebug] | Pervasives.UnfoldOnly names -> [UnfoldUntil delta_constant; UnfoldOnly (List.map I.lid_of_str names)] + | Pervasives.UnfoldOnce names -> + [UnfoldUntil delta_constant; UnfoldOnce (List.map I.lid_of_str names)] | Pervasives.UnfoldFully names -> [UnfoldUntil delta_constant; UnfoldFully (List.map I.lid_of_str names)] | Pervasives.UnfoldAttr names -> diff --git a/src/typechecker/FStarC.TypeChecker.Cfg.fsti b/src/typechecker/FStarC.TypeChecker.Cfg.fsti index 2a8915dcf65..dfe2ed86774 100644 --- a/src/typechecker/FStarC.TypeChecker.Cfg.fsti +++ b/src/typechecker/FStarC.TypeChecker.Cfg.fsti @@ -56,6 +56,7 @@ type fsteps = { do_not_unfold_pure_lets : bool; unfold_until : option S.delta_depth; unfold_only : option (list I.lid); + unfold_once : option (list I.lid); unfold_fully : option (list I.lid); unfold_attr : option (list I.lid); unfold_qual : option (list string); diff --git a/src/typechecker/FStarC.TypeChecker.Env.fsti b/src/typechecker/FStarC.TypeChecker.Env.fsti index fdc48da5081..bd7920b35bc 100644 --- a/src/typechecker/FStarC.TypeChecker.Env.fsti +++ b/src/typechecker/FStarC.TypeChecker.Env.fsti @@ -44,6 +44,7 @@ type step = | DoNotUnfoldPureLets | UnfoldUntil of delta_depth | UnfoldOnly of list FStarC.Ident.lid + | UnfoldOnce of list FStarC.Ident.lid | UnfoldFully of list FStarC.Ident.lid | UnfoldAttr of list FStarC.Ident.lid | UnfoldQual of list string diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst index 42987e0cdc6..0ffdc79d0b3 100644 --- a/ulib/FStar.Pervasives.fst +++ b/ulib/FStar.Pervasives.fst @@ -57,6 +57,7 @@ type norm_step = | Reify // Reify effectful definitions into their representations | NormDebug // Turn on debugging for this call | UnfoldOnly : list string -> norm_step // Unlike Delta, unfold definitions for only the given + | UnfoldOnce : list string -> norm_step // names, each string is a fully qualified name // like `A.M.f` // idem @@ -103,6 +104,9 @@ let reify_ = Reify irreducible let delta_only s = UnfoldOnly s +irreducible +let delta_once s = UnfoldOnce s + irreducible let delta_fully s = UnfoldFully s diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 31dd09c6942..623a07c1fa6 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -217,6 +217,13 @@ val reify_ : norm_step list. Each string is a fully qualified name like [A.M.f] *) val delta_only (s: list string) : Tot norm_step +(** Like [delta_only], unfold only the definitions in this list, +but do so only once. This is useful for a controlled unfolding +of recursive definitions. NOTE: if there are many occurrences +of a variable in this list, it is unspecified which one will +be unfolded (currently it depends on normalization order). *) +val delta_once (s: list string) : Tot norm_step + (** Unfold definitions for only the names in the given list, but unfold each definition encountered after unfolding as well. From 50be0f2ca6572de7fac56747a42aef67821a06d5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 5 Dec 2024 17:13:47 -0800 Subject: [PATCH 2/6] Normalizer: Implement UnfoldOnce --- ...FStarC.TypeChecker.Normalize.Unfolding.fst | 30 ++++++++++++------- ...StarC.TypeChecker.Normalize.Unfolding.fsti | 1 + .../FStarC.TypeChecker.Normalize.fst | 10 +++++++ 3 files changed, 30 insertions(+), 11 deletions(-) diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fst b/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fst index 842f7a34dc8..3c36512f6c7 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fst @@ -34,15 +34,16 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = | None -> [] | Some quals -> quals in - (* unfold or not, fully or not, reified or not *) - let yes = true , false , false in - let no = false , false , false in - let fully = true , true , false in - let reif = true , false , true in + (* unfold or not, fully or not, reified or not, only once or not *) + let yes = true , false , false, false in + let no = false , false , false, false in + let fully = true , true , false, false in + let reif = true , false , true, false in + let once = true , false , false, true in let yesno b = if b then yes else no in let fullyno b = if b then fully else no in - let comb_or l = List.fold_right (fun (a,b,c) (x,y,z) -> (a||x, b||y, c||z)) l (false, false, false) in + let comb_or l = List.fold_right (fun (a,b,c,d) (x,y,z,w) -> (a||x, b||y, c||z, d||w)) l (false, false, false, false) in let default_unfolding () = log_unfolding cfg (fun () -> BU.print3 "should_unfold: Reached a %s with delta_depth = %s\n >> Our delta_level is %s\n" @@ -57,12 +58,13 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = in let selective_unfold = Some? cfg.steps.unfold_only || + Some? cfg.steps.unfold_once || Some? cfg.steps.unfold_fully || Some? cfg.steps.unfold_attr || Some? cfg.steps.unfold_qual || Some? cfg.steps.unfold_namespace in - let res : bool & bool & bool = + let res : bool & bool & bool & bool = match qninfo, selective_unfold with // We unfold dm4f actions if and only if we are reifying | _ when Env.qninfo_is_action qninfo -> @@ -83,6 +85,11 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = log_unfolding cfg (fun () -> BU.print_string " >> HasMaskedEffect, not unfolding\n"); no + // Unfoldonce. NB: this is before the zeta case, so we unfold even if zeta is off + | _, true when Some? cfg.steps.unfold_once && BU.for_some (fv_eq_lid fv) (Some?.v cfg.steps.unfold_once) -> + log_unfolding cfg (fun () -> BU.print_string " >> UnfoldOnce\n"); + once + // Recursive lets may only be unfolded when Zeta is on | Some (Inr ({sigquals=qs; sigel=Sig_let {lbs=(is_rec, _)}}, _), _), _ when is_rec && not cfg.steps.zeta && not cfg.steps.zeta_full -> @@ -160,10 +167,11 @@ let should_unfold cfg should_reify fv qninfo : should_unfold_res = ); let r = match res with - | false, _, _ -> Should_unfold_no - | true, false, false -> Should_unfold_yes - | true, true, false -> Should_unfold_fully - | true, false, true -> Should_unfold_reify + | false, _, _, _ -> Should_unfold_no + | true, false, false, false -> Should_unfold_yes + | true, false, false, true -> Should_unfold_once + | true, true, false, false -> Should_unfold_fully + | true, false, true, false -> Should_unfold_reify | _ -> failwith <| BU.format1 "Unexpected unfolding result: %s" (show res) in diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fsti b/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fsti index fc981c6c573..afc391bbed1 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fsti +++ b/src/typechecker/FStarC.TypeChecker.Normalize.Unfolding.fsti @@ -13,6 +13,7 @@ val plugin_unfold_warn_ctr : ref int type should_unfold_res = | Should_unfold_no | Should_unfold_yes + | Should_unfold_once | Should_unfold_fully | Should_unfold_reify diff --git a/src/typechecker/FStarC.TypeChecker.Normalize.fst b/src/typechecker/FStarC.TypeChecker.Normalize.fst index dd13893880b..678dc03a734 100644 --- a/src/typechecker/FStarC.TypeChecker.Normalize.fst +++ b/src/typechecker/FStarC.TypeChecker.Normalize.fst @@ -631,9 +631,19 @@ let decide_unfolding cfg stack fv qninfo (* : option (option cfg * stack) *) = | Should_unfold_no -> // No unfolding None + | Should_unfold_yes -> // Usual unfolding, no change to cfg or stack Some (None, stack) + + | Should_unfold_once -> + let Some once = cfg.steps.unfold_once in + let cfg' = { cfg with steps = { + cfg.steps with unfold_once = + Some <| List.filter (fun lid -> not (S.fv_eq_lid fv lid)) once } } in + // Unfold only once. Keep the stack, but remove the lid from the step. + Some (Some cfg', stack) + | Should_unfold_fully -> // Unfolding fully, use new cfg with more steps and keep old one in stack let cfg' = From 0080943b7f6a0b5a17464ee40ffaf9d76f5d699c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 5 Dec 2024 17:14:15 -0800 Subject: [PATCH 3/6] Pervasives: use delta_once for reveal_opaque --- ulib/FStar.Pervasives.fsti | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 623a07c1fa6..d9f46f6f97f 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -335,9 +335,8 @@ val normalize_spec (a: Type0) : Lemma (normalize a == a) val norm_spec (s: list norm_step) (#a: Type) (x: a) : Lemma (norm s #a x == x) (** Use the following to expose an ["opaque_to_smt"] definition to the - solver as: [reveal_opaque (`%defn) defn]. NB: zeta is needed in - the case where the definition is recursive. *) -let reveal_opaque (s: string) = norm_spec [delta_only [s]; zeta] + solver as: [reveal_opaque (`%defn) defn]. *) +let reveal_opaque (s: string) = norm_spec [delta_once [s]] (** Wrappers over pure wp combinators that return a pure_wp type (with monotonicity refinement) *) From 9bf48cee0685c4d141ed446b1888b9d40e3e7590 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Thu, 5 Dec 2024 17:15:55 -0800 Subject: [PATCH 4/6] Add a test --- tests/micro-benchmarks/UnfoldOnce.fst | 29 +++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/micro-benchmarks/UnfoldOnce.fst diff --git a/tests/micro-benchmarks/UnfoldOnce.fst b/tests/micro-benchmarks/UnfoldOnce.fst new file mode 100644 index 00000000000..0671172b6f6 --- /dev/null +++ b/tests/micro-benchmarks/UnfoldOnce.fst @@ -0,0 +1,29 @@ +module UnfoldOnce + +open FStar.Tactics.V2 + +#push-options "--admit_smt_queries true" +let rec f () : Tot int = 1 + f () +#pop-options + +let _ = + assert True by begin + let t = (`(f ())) in + let t' = norm_term [delta_once [`%f]] t in + let expected = (`(1 + f () <: Tot Prims.int)) in + (* print ("t' = " ^term_to_string t'); *) + (* print ("expected = " ^term_to_string expected); *) + guard (term_eq t' expected); + () + end + +let _ = + assert True by begin + let t = (`(f () + f ())) in + let t' = norm_term [delta_once [`%f]] t in + let expected = (`((1 + f () <: Tot Prims.int) + f ())) in + (* print ("t' = " ^term_to_string t'); *) + (* print ("expected = " ^term_to_string expected); *) + guard (term_eq t' expected); + () + end From 0a6098fc6098b01a8980a8b307906f2136520d55 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 6 Dec 2024 10:59:40 -0800 Subject: [PATCH 5/6] Update expected output (line numbers) --- tests/error-messages/NegativeTests.Neg.fst.json_output.expected | 2 +- tests/error-messages/NegativeTests.Neg.fst.output.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected index 544da7d4c3a..cee9400b4f5 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.json_output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.json_output.expected @@ -20,7 +20,7 @@ {"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.Native.option 'a {Some? _}\ngot type FStar.Pervasives.Native.option 'a","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.Native.fst","start_pos":{"line":33,"col":4},"end_pos":{"line":33,"col":8}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":46,"col":30},"end_pos":{"line":46,"col":31}}},"number":19,"ctx":["While typechecking the top-level declaration `let bad_projector`","While typechecking the top-level declaration `[@@expect_failure] let bad_projector`"]} >>] >> Got issues: [ -{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":520,"col":4},"end_pos":{"line":520,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} +{"msg":["Subtyping check failed","Expected type _: FStar.Pervasives.result Prims.int {V? _}\ngot type FStar.Pervasives.result Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"FStar.Pervasives.fsti","start_pos":{"line":526,"col":4},"end_pos":{"line":526,"col":5}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":50,"col":45},"end_pos":{"line":50,"col":47}}},"number":19,"ctx":["While typechecking the top-level declaration `val NegativeTests.Neg.test`","While typechecking the top-level declaration `[@@expect_failure] val NegativeTests.Neg.test`"]} >>] >> Got issues: [ {"msg":["Subtyping check failed","Expected type Prims.nat\ngot type Prims.int","The SMT solver could not prove the query. Use --query_stats for more details."],"level":"Error","range":{"def":{"file_name":"Prims.fst","start_pos":{"line":680,"col":18},"end_pos":{"line":680,"col":24}},"use":{"file_name":"NegativeTests.Neg.fst","start_pos":{"line":55,"col":25},"end_pos":{"line":55,"col":26}}},"number":19,"ctx":["While checking for top-level effects","While typechecking the top-level declaration `let h1`","While typechecking the top-level declaration `[@@expect_failure] let h1`"]} diff --git a/tests/error-messages/NegativeTests.Neg.fst.output.expected b/tests/error-messages/NegativeTests.Neg.fst.output.expected index 9e9360e0883..498f2dbc414 100644 --- a/tests/error-messages/NegativeTests.Neg.fst.output.expected +++ b/tests/error-messages/NegativeTests.Neg.fst.output.expected @@ -63,7 +63,7 @@ got type FStar.Pervasives.result Prims.int - The SMT solver could not prove the query. Use --query_stats for more details. - - See also FStar.Pervasives.fsti(520,4-520,5) + - See also FStar.Pervasives.fsti(526,4-526,5) >>] >> Got issues: [ From 5fcd56d959cdc1052c711b0b4569f5cfa5a714e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 12 Jan 2025 15:38:11 -0800 Subject: [PATCH 6/6] rlimits --- examples/data_structures/BinomialQueue.fst | 2 +- examples/doublylinkedlist/DoublyLinkedList.fst | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/data_structures/BinomialQueue.fst b/examples/data_structures/BinomialQueue.fst index b717ca58936..5a388a7dd51 100644 --- a/examples/data_structures/BinomialQueue.fst +++ b/examples/data_structures/BinomialQueue.fst @@ -360,7 +360,7 @@ let rec carry_repr (d:pos) (q:forest) (t:tree) (lq lt:ms) (ms_append (keys_of_tree hd) (keys_of_tree t)) #pop-options -#push-options "--z3rlimit 50 --fuel 1 --ifuel 1" +#push-options "--z3rlimit 75 --fuel 1 --ifuel 1" let rec join_repr (d:pos) (p q:forest) (c:tree) (lp lq lc:ms) : Lemma diff --git a/examples/doublylinkedlist/DoublyLinkedList.fst b/examples/doublylinkedlist/DoublyLinkedList.fst index b34fd763aeb..d529f88e79f 100644 --- a/examples/doublylinkedlist/DoublyLinkedList.fst +++ b/examples/doublylinkedlist/DoublyLinkedList.fst @@ -1964,7 +1964,7 @@ let dll_append (#t:Type) (d1 d2:dll t) : #reset-options -#set-options "--z3rlimit 40 --max_fuel 2 --max_ifuel 1" +#set-options "--z3rlimit 60 --max_fuel 2 --max_ifuel 1" let dll_split_using (#t:Type) (d:dll t) (e:pointer (node t)) : StackInline (dll t * dll t)