From a08b6f047896a62d6b777eea66504f261b4d5605 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 5 Sep 2025 17:47:15 -0700 Subject: [PATCH 1/2] Adapt to tactic monad change. --- src/checker/Pulse.Checker.Base.fst | 4 +-- src/checker/Pulse.Checker.Pure.fst | 6 ++--- src/checker/Pulse.Checker.WithLocal.fst | 2 +- src/checker/Pulse.JoinComp.fst | 2 +- src/checker/Pulse.JoinComp.fsti | 8 +----- src/checker/Pulse.Typing.Combinators.fst | 22 +++++++-------- src/checker/Pulse.Typing.Combinators.fsti | 8 +++--- src/checker/Pulse.Typing.Env.fst | 1 - src/checker/Pulse.Typing.Env.fsti | 8 +++--- src/ml/PulseSyntaxExtension_SyntaxWrapper.ml | 4 +-- src/ml/Pulse_RuntimeUtils.ml | 28 +++++++------------- 11 files changed, 36 insertions(+), 57 deletions(-) diff --git a/src/checker/Pulse.Checker.Base.fst b/src/checker/Pulse.Checker.Base.fst index 8e60da8c8..d6968dc6a 100644 --- a/src/checker/Pulse.Checker.Base.fst +++ b/src/checker/Pulse.Checker.Base.fst @@ -1179,8 +1179,8 @@ let infer_post #g #ctxt (r:checker_result_t g ctxt NoHint) let bs0 = bindings g in let dom_g = dom g in let fvs_t = freevars t in - let fail_fv_typ #a (x:string) - : T.Tac a = + let fail_fv_typ (x:string) + : T.Tac unit = fail_doc g (Some (T.range_of_term t)) [Pulse.PP.text "Could not infer a type for this block; the return type `"; Pulse.PP.text (T.term_to_string t); diff --git a/src/checker/Pulse.Checker.Pure.fst b/src/checker/Pulse.Checker.Pure.fst index 959761a0f..f6755bd87 100644 --- a/src/checker/Pulse.Checker.Pure.fst +++ b/src/checker/Pulse.Checker.Pure.fst @@ -166,8 +166,8 @@ does not make sense, as that indicates a well-typed term with no particular expected type, which is fine. *) let ill_typed_term (t:term) (expected_typ got_typ : option term) : TacH (list document) - (requires fun _ -> None? expected_typ ==> None? got_typ) - (ensures fun _ _ -> True) + (requires None? expected_typ ==> None? got_typ) + (ensures fun _ -> True) = let open Pulse.PP in match expected_typ, got_typ with @@ -192,7 +192,7 @@ let instantiate_term_implicits let rng = RU.range_of_term t0 in let f = RU.env_set_range f (Pulse.Typing.Env.get_range g (Some rng)) in let topt, issues = catch_all (fun _ -> rtb_instantiate_implicits g f t0 expected inst_extra) in - let fail #a issues : Tac a = + let fail issues : Tac _ = fail_doc_with_subissues g (Some rng) issues [] in match topt with diff --git a/src/checker/Pulse.Checker.WithLocal.fst b/src/checker/Pulse.Checker.WithLocal.fst index 92a56e8d8..6c74c8e89 100644 --- a/src/checker/Pulse.Checker.WithLocal.fst +++ b/src/checker/Pulse.Checker.WithLocal.fst @@ -46,7 +46,7 @@ let with_local_pre_typing (#g:env) (#pre:term) (pre_typing:tot_typing g pre tm_s tm_slprop = admit() -#push-options "--z3rlimit_factor 8 --fuel 0 --ifuel 1 --split_queries no" +#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 1 --split_queries no" let head_range (t:st_term {Tm_WithLocal? t.term}) : range = let Tm_WithLocal { initializer } = t.term in (RU.range_of_term initializer) diff --git a/src/checker/Pulse.JoinComp.fst b/src/checker/Pulse.JoinComp.fst index 3f8ab45d1..a71084f67 100644 --- a/src/checker/Pulse.JoinComp.fst +++ b/src/checker/Pulse.JoinComp.fst @@ -285,7 +285,7 @@ let rec join_comps (c_else:comp_st) (e_else_typing:st_typing g_else e_else c_else) (post:post_hint_t) - : TacS (c:comp_st & + : T.TacH (c:comp_st & st_typing g_then e_then c & st_typing g_else e_else c) (requires diff --git a/src/checker/Pulse.JoinComp.fsti b/src/checker/Pulse.JoinComp.fsti index 5474bcd8a..b9ade13aa 100644 --- a/src/checker/Pulse.JoinComp.fsti +++ b/src/checker/Pulse.JoinComp.fsti @@ -19,12 +19,6 @@ module Pulse.JoinComp open Pulse.Syntax open Pulse.Typing module T = FStar.Tactics.V2 -effect TacS (a:Type) (pre : Type0) (post : (_:a{pre}) -> Type0) = - Tactics.TacH a (requires (fun _ -> pre)) - (ensures (fun _ r -> pre /\ ( - match r with - | Tactics.Result.Success r _ -> post r - | _ -> True))) // does not guarantee anything on failure val join_post #g #hyp #b (p1:post_hint_for_env (g_with_eq g hyp b tm_true)) @@ -41,7 +35,7 @@ val join_comps (c_else:comp_st) (e_else_typing:st_typing g_else e_else c_else) (post:post_hint_t) -: TacS (c:comp_st & +: T.TacH (c:comp_st & st_typing g_then e_then c & st_typing g_else e_else c) (requires diff --git a/src/checker/Pulse.Typing.Combinators.fst b/src/checker/Pulse.Typing.Combinators.fst index eb71643af..7a432c7b6 100644 --- a/src/checker/Pulse.Typing.Combinators.fst +++ b/src/checker/Pulse.Typing.Combinators.fst @@ -169,7 +169,6 @@ let rec slprop_equiv_typing (#g:_) (#t0 #t1:term) (v:slprop_equiv g t0 t1) let t0_typing = d1 t1_typing in construct_forall_typing #g #u #b #t0 x b_typing t0_typing) -#push-options "--z3rlimit_factor 8 --ifuel 1 --fuel 2" let bind_t (case_c1 case_c2:comp_st -> bool) = (g:env) -> (pre:term) -> @@ -190,15 +189,14 @@ let bind_t (case_c1 case_c2:comp_st -> bool) = c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\ comp_post_matches_hint c post_hint } & st_typing g t c) - (requires fun _ -> - let _, x = px in + (requires + (let _, x = px in comp_pre c1 == pre /\ None? (lookup g x) /\ (~(x `Set.mem` freevars_st e2)) /\ open_term (comp_post c1) x == comp_pre c2 /\ - (~ (x `Set.mem` freevars (comp_post c2)))) - (ensures fun _ _ -> True) -#pop-options + (~ (x `Set.mem` freevars (comp_post c2))))) + (ensures fun _ -> True) let mk_bind_st_st : bind_t C_ST? C_ST? @@ -359,18 +357,18 @@ let rec mk_bind (g:env) st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\ comp_post_matches_hint c post_hint } & st_typing g t c) - (requires fun _ -> - let _, x = px in + (requires + (let _, x = px in comp_pre c1 == pre /\ None? (lookup g x) /\ (~(x `Set.mem` freevars_st e2)) /\ open_term (comp_post c1) x == comp_pre c2 /\ - (~ (x `Set.mem` freevars (comp_post c2)))) - (ensures fun _ _ -> True) = + (~ (x `Set.mem` freevars (comp_post c2))))) + (ensures fun _ -> True) = let _, x = px in let b = nvar_as_binder px (comp_res c1) in - let fail_bias (#a:Type) tag - : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r) + let fail_bias tag + : T.TacH _ (requires True) (ensures fun _ -> False) = let open Pulse.PP in fail_doc g (Some e1.range) [text "Cannot compose computations in this " ^/^ text tag ^/^ text " block:"; diff --git a/src/checker/Pulse.Typing.Combinators.fsti b/src/checker/Pulse.Typing.Combinators.fsti index ccc36f26f..e2fac7af2 100644 --- a/src/checker/Pulse.Typing.Combinators.fsti +++ b/src/checker/Pulse.Typing.Combinators.fsti @@ -58,14 +58,14 @@ val mk_bind (g:env) c:comp_st { st_comp_of_comp c == st_comp_with_pre (st_comp_of_comp c2) pre /\ comp_post_matches_hint c post_hint } & st_typing g t c) - (requires fun _ -> - let _, x = px in + (requires + (let _, x = px in comp_pre c1 == pre /\ None? (lookup g x) /\ (~(x `Set.mem` freevars_st e2)) /\ open_term (comp_post c1) x == comp_pre c2 /\ - (~ (x `Set.mem` freevars (comp_post c2)))) - (ensures fun _ _ -> True) + (~ (x `Set.mem` freevars (comp_post c2))))) + (ensures fun _ -> True) val bind_res_and_post_typing (g:env) (s2:comp_st) (x:var { fresh_wrt x g (freevars (comp_post s2)) }) diff --git a/src/checker/Pulse.Typing.Env.fst b/src/checker/Pulse.Typing.Env.fst index 1be8a15bc..31d498b7a 100644 --- a/src/checker/Pulse.Typing.Env.fst +++ b/src/checker/Pulse.Typing.Env.fst @@ -459,7 +459,6 @@ let info (g:env) (r:option range) (msg:string) = let fail_doc_with_subissues #a (g:env) (ro : option range) (sub : list Issue.issue) (msg : list document) - : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r) = (* If for whatever reason `sub` is empty, F* will handle it well and a generic error message will be displayed *) diff --git a/src/checker/Pulse.Typing.Env.fsti b/src/checker/Pulse.Typing.Env.fsti index c105cf128..c8468b4a1 100644 --- a/src/checker/Pulse.Typing.Env.fsti +++ b/src/checker/Pulse.Typing.Env.fsti @@ -225,10 +225,10 @@ val get_range (g:env) (r:option range) : T.Tac range val fail_doc_env (#a:Type) (with_env:bool) (g:env) (r:option range) (msg:list Pprint.document) - : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r) + : T.TacH a (requires True) (ensures fun _ -> False) let fail_doc (#a:Type) (g:env) (r:option range) (msg:list Pprint.document) - : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r) + : T.TacH a (requires True) (ensures fun _ -> False) = fail_doc_env false g r msg val warn_doc (g:env) (r:option range) (msg:list Pprint.document) @@ -241,7 +241,7 @@ val info_doc_env (g:env) (r:option range) (msg:list Pprint.document) : T.Tac unit val fail (#a:Type) (g:env) (r:option range) (msg:string) - : T.TAC a (fun _ post -> forall ex ps. post FStar.Tactics.Result.(Failed ex ps)) + : T.TacH a (requires True) (ensures fun _ -> False) val warn (g:env) (r:option range) (msg:string) : T.Tac unit @@ -252,7 +252,7 @@ val info (g:env) (r:option range) (msg:string) val fail_doc_with_subissues #a (g:env) (ro : option range) (sub : list Issue.issue) (msg : list Pprint.document) - : T.TacH a (requires fun _ -> True) (ensures fun _ r -> FStar.Tactics.Result.Failed? r) + : T.TacH a (requires True) (ensures fun _ -> False) val info_doc_with_subissues (g:env) (r:option range) (sub : list Issue.issue) diff --git a/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml b/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml index 7a18c7e2e..a828121d3 100644 --- a/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml +++ b/src/ml/PulseSyntaxExtension_SyntaxWrapper.ml @@ -238,9 +238,7 @@ let tac_to_string (env:Env.env) f = [] [] in - match f ps with - | FStarC_Tactics_Result.Success (x, _) -> x - | FStarC_Tactics_Result.Failed (exn, _) -> failwith (print_exn exn) + f (ref ps) let binder_to_string (env:Env.env) (b:binder) : string diff --git a/src/ml/Pulse_RuntimeUtils.ml b/src/ml/Pulse_RuntimeUtils.ml index 20605cade..6269b13a9 100644 --- a/src/ml/Pulse_RuntimeUtils.ml +++ b/src/ml/Pulse_RuntimeUtils.ml @@ -3,8 +3,7 @@ type context = ((string * FStarC_Range.range option) list) (* FStar_Sealed.seale let extend_context (s:string) (r:FStarC_Range.range option) (c:context) = (s,r)::c module TR = FStarC_Tactics_Result -type ('a,'wp) tac_repr = FStarC_Tactics_Types.proofstate -> 'a TR.__result -type 'a utac = ('a, unit) tac_repr +type 'a utac = 'a FStarC_Tactics_Monad.tac let ctxt_elt_as_string (s, r) = match r with @@ -13,10 +12,7 @@ let ctxt_elt_as_string (s, r) = "@" ^ FStarC_Range.string_of_range r ^ ": " ^ s let rec print_context (c:context) : string utac = fun ps -> - TR.Success ( - String.concat "\n>" (List.map ctxt_elt_as_string c), - ps - ) + String.concat "\n>" (List.map ctxt_elt_as_string c) let rec with_context (c:context) (f: unit -> 'a utac) : 'a utac = fun ps -> match c with @@ -206,14 +202,6 @@ let whnf_lax (g:TcEnv.env) (t:S.term) : S.term = let hnf_lax (g:TcEnv.env) (t:S.term) : S.term = FStarC_TypeChecker_Normalize.normalize [TcEnv.Unascribe; TcEnv.Primops; TcEnv.HNF; TcEnv.UnfoldUntil S.delta_constant; TcEnv.Beta] g t -let norm_well_typed_term_aux - (g:TcEnv.env) - (t:S.term) - (steps:FStarC_NormSteps.norm_step list) - = let steps = FStarC_TypeChecker_Cfg.translate_norm_steps steps in - let t' = FStarC_TypeChecker_Normalize.normalize (TcEnv.Unascribe::steps) g t in - FStar_Pervasives.Mkdtuple3 (t', (), ()) - let norm_well_typed_term (g:TcEnv.env) (t:S.term) @@ -221,16 +209,18 @@ let norm_well_typed_term (k:_) (typing:_) (steps:FStarC_NormSteps.norm_step list) - (ps:_) - = let t' = norm_well_typed_term_aux g t steps in - FStarC_Tactics_Result.Success (t', ps) + : ((S.term, unit, unit) Fstar_pluginlib.FStar_Pervasives.dtuple3) utac + = fun ps -> + let steps = FStarC_TypeChecker_Cfg.translate_norm_steps steps in + let t' = FStarC_TypeChecker_Normalize.normalize (TcEnv.Unascribe::steps) g t in + Fstar_pluginlib.FStar_Pervasives.Mkdtuple3 (t', (), ()) let add_attribute (s:S.sigelt) (x:S.attribute) = { s with sigattrs = x::s.sigattrs } let add_noextract_qual (s:S.sigelt) = { s with sigquals = S.NoExtract::s.sigquals } -let get_attributes (s:S.sigelt) (ps:_) = - FStarC_Tactics_Result.Success (s.sigattrs, ps) +let get_attributes (s:S.sigelt) : _ utac = fun ps -> + s.sigattrs let must_erase_for_extraction (g:FStarC_Reflection_Types.env) (ty:FStarC_Syntax_Syntax.term) = FStarC_TypeChecker_Util.must_erase_for_extraction g ty From bd9724c59f573991a1309e790f5a09a8cc6d2b29 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 23 Sep 2025 16:21:27 -0700 Subject: [PATCH 2/2] Fix tests. --- test/bug-reports/Bug.SpinLock.fst.output.expected | 1 + test/bug-reports/Bug107.fst.output.expected | 2 ++ test/bug-reports/Bug267.fst.output.expected | 1 + test/bug-reports/Bug274.fst.output.expected | 3 +++ test/bug-reports/Bug29.fst.output.expected | 1 + .../ExistsErasedAndPureEqualities.fst.output.expected | 3 +++ test/bug-reports/IntroGhost.fst.output.expected | 2 ++ test/bug-reports/PartialApp.fst.output.expected | 2 ++ test/nolib/Test.Matcher.fst.output.expected | 1 + test/nolib/Test.RewriteBy.fst.output.expected | 2 +- 10 files changed, 17 insertions(+), 1 deletion(-) diff --git a/test/bug-reports/Bug.SpinLock.fst.output.expected b/test/bug-reports/Bug.SpinLock.fst.output.expected index d8ec9c15c..031929361 100644 --- a/test/bug-reports/Bug.SpinLock.fst.output.expected +++ b/test/bug-reports/Bug.SpinLock.fst.output.expected @@ -1,5 +1,6 @@ * Info at Bug.SpinLock.fst(45,2-45,4): - Expected failure: + - Tactic failed - Cannot prove: Pulse.Lib.Reference.pts_to __ ?__ - In the context: diff --git a/test/bug-reports/Bug107.fst.output.expected b/test/bug-reports/Bug107.fst.output.expected index 7d1a8a816..9e2936ac6 100644 --- a/test/bug-reports/Bug107.fst.output.expected +++ b/test/bug-reports/Bug107.fst.output.expected @@ -1,8 +1,10 @@ * Info at Bug107.fst(45,9-45,16): - Expected failure: + - Tactic failed - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo 1 _ * Info at Bug107.fst(56,9-56,16): - Expected failure: + - Tactic failed - Could not resolve implicit uu___#87 of type Prims.int in term Bug107.foo _ 2 diff --git a/test/bug-reports/Bug267.fst.output.expected b/test/bug-reports/Bug267.fst.output.expected index fad0fe5aa..b9d0544ca 100644 --- a/test/bug-reports/Bug267.fst.output.expected +++ b/test/bug-reports/Bug267.fst.output.expected @@ -1,5 +1,6 @@ * Info at Bug267.fst(14,4-14,6): - Expected failure: + - Tactic failed - Expected a total term, but this term has Ghost effect * Info at Bug267.fst(62,4-62,5): diff --git a/test/bug-reports/Bug274.fst.output.expected b/test/bug-reports/Bug274.fst.output.expected index dc475d73c..bebbc3aa9 100644 --- a/test/bug-reports/Bug274.fst.output.expected +++ b/test/bug-reports/Bug274.fst.output.expected @@ -1,5 +1,6 @@ * Info at Bug274.fst(29,4-29,15): - Expected failure: + - Tactic failed - Cannot prove any of: Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _ - In the context: @@ -36,6 +37,7 @@ * Info at Bug274.fst(41,4-41,15): - Expected failure: + - Tactic failed - Cannot prove any of: Pulse.Lib.Trade.trade _ _ ** Pulse.Lib.Trade.trade _ _ - In the context: @@ -72,6 +74,7 @@ * Info at Bug274.fst(73,4-73,12): - Expected failure: + - Tactic failed - Cannot prove any of: _ ** Pulse.Lib.Trade.trade _ _ - In the context: diff --git a/test/bug-reports/Bug29.fst.output.expected b/test/bug-reports/Bug29.fst.output.expected index ee2059e7b..e7f1e68db 100644 --- a/test/bug-reports/Bug29.fst.output.expected +++ b/test/bug-reports/Bug29.fst.output.expected @@ -1,5 +1,6 @@ * Info at Bug29.fst(57,4-57,45): - Expected failure: + - Tactic failed - Cannot prove: Pulse.Lib.Reference.pts_to r v - In the context: diff --git a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected index 6278c78f0..f46c01e1b 100644 --- a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected +++ b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected @@ -1,10 +1,12 @@ * Info at ExistsErasedAndPureEqualities.fst(32,4-33,21): - Expected failure: + - Tactic failed - Could not resolve all free variables in the proposition: v == v_ - See also ExistsErasedAndPureEqualities.fst(32,4-34,12) * Info at ExistsErasedAndPureEqualities.fst(50,4-51,21): - Expected failure: + - Tactic failed - Could not resolve all free variables in the proposition: v == v_ - See also ExistsErasedAndPureEqualities.fst(50,4-52,12) @@ -21,6 +23,7 @@ * Info at ExistsErasedAndPureEqualities.fst(79,4-80,21): - Expected failure: + - Tactic failed - Could not resolve all free variables in the proposition: v == v_ - See also ExistsErasedAndPureEqualities.fst(79,4-81,12) diff --git a/test/bug-reports/IntroGhost.fst.output.expected b/test/bug-reports/IntroGhost.fst.output.expected index d4fc7fe6e..a816f5bb3 100644 --- a/test/bug-reports/IntroGhost.fst.output.expected +++ b/test/bug-reports/IntroGhost.fst.output.expected @@ -1,5 +1,6 @@ * Info at IntroGhost.fst(44,18-44,20): - Expected failure: + - Tactic failed - Cannot prove: Pulse.Lib.Reference.pts_to r __ - In the context: @@ -7,6 +8,7 @@ * Info at IntroGhost.fst(71,2-71,4): - Expected failure: + - Tactic failed - Cannot prove: Pulse.Lib.Reference.pts_to r 0 - In the context: diff --git a/test/bug-reports/PartialApp.fst.output.expected b/test/bug-reports/PartialApp.fst.output.expected index 98e297a36..6c38c44a2 100644 --- a/test/bug-reports/PartialApp.fst.output.expected +++ b/test/bug-reports/PartialApp.fst.output.expected @@ -1,10 +1,12 @@ * Info at PartialApp.fst(26,2-26,3): - Expected failure: + - Tactic failed - This statement returns a value of type: Prims.int - Did you forget to assign it or ignore it? * Info at PartialApp.fst(60,2-60,9): - Expected failure: + - Tactic failed - This function is partially applied. Remaining type: y: t -> Pulse.Lib.Core.stt Prims.unit diff --git a/test/nolib/Test.Matcher.fst.output.expected b/test/nolib/Test.Matcher.fst.output.expected index ff291bf1a..7432a6ce6 100644 --- a/test/nolib/Test.Matcher.fst.output.expected +++ b/test/nolib/Test.Matcher.fst.output.expected @@ -1,5 +1,6 @@ * Info at Test.Matcher.fst(69,2-69,4): - Expected failure: + - Tactic failed - Cannot prove: Test.Matcher.fpts_to #Prims.int r diff --git a/test/nolib/Test.RewriteBy.fst.output.expected b/test/nolib/Test.RewriteBy.fst.output.expected index 423e3f8ee..2eab8bcb0 100644 --- a/test/nolib/Test.RewriteBy.fst.output.expected +++ b/test/nolib/Test.RewriteBy.fst.output.expected @@ -12,5 +12,5 @@ - Reduction stopped at: reify (let _ = FStar.Stubs.Tactics.V2.Builtins.dump "a" in Test.RewriteBy.tac ()) - "(((proofstate)))" + "(((ref proofstate)))"