From f4c485566e4a078654e7711f9b189867d2bab3ce Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 21 Nov 2025 15:21:47 -0800 Subject: [PATCH 1/2] Use default prover for impure specs too. --- src/checker/Pulse.Checker.ImpureSpec.fst | 59 ++---------------------- src/checker/Pulse.Checker.Prover.fst | 25 +++++----- 2 files changed, 16 insertions(+), 68 deletions(-) diff --git a/src/checker/Pulse.Checker.ImpureSpec.fst b/src/checker/Pulse.Checker.ImpureSpec.fst index e14fca0e4..9cc6769c3 100644 --- a/src/checker/Pulse.Checker.ImpureSpec.fst +++ b/src/checker/Pulse.Checker.ImpureSpec.fst @@ -60,63 +60,10 @@ let rec get_rewrites_to_from_post (g: env) xres (post: slprop) : T.Tac (option R | _ -> None) | _ -> None -let prove_this (g: env) (goal: slprop) (ctxt: list slprop) : T.Tac (option (list slprop)) = - match inspect_term goal with - | Tm_Pure p -> - // TODO: pure (x == ?u) - Some [] - | Tm_ExistsSL u b body -> - let uv = RU.new_implicit_var "witness for exists*" (RU.range_of_term goal) (elab_env g) b.binder_ty false in - Some (slprop_as_list (open_term' body uv 0)) - | Tm_WithPure p _ body -> - Some (tm_pure p :: slprop_as_list (open_term' body unit_const 0)) - | Tm_Star a b -> - Some [a; b] - | _ -> - let rec try_match (ctxt: list slprop) : Dv bool = - match ctxt with - | [] -> false - | c::ctxt -> - if RU.teq_nosmt_force_phase1 (elab_env g) goal c then - true - else - try_match ctxt - in - if try_match ctxt then - Some [] - else - None - -let rec prove_step (g: env) (goals: list slprop) (ctxt: list slprop) : T.Tac (option (list slprop)) = - match goals with - | [] -> None - | goal::goals -> - match prove_this g goal ctxt with - | Some new_goals -> Some (new_goals @ goals) - | None -> - match prove_step g goals ctxt with - | Some stepped -> Some (goal :: stepped) - | None -> None - -let rec prove_loop (g: env) (goals: list slprop) (ctxt: list slprop) : T.Tac (list slprop) = - match prove_step g goals ctxt with - | Some new_goals -> prove_loop g new_goals ctxt - | None -> goals - let prove (g: env) (goal: slprop) (ctxt: slprop) (r: range) : T.Tac unit = - let (| goal, _ |) = normalize_slprop g goal true in - let goal = slprop_as_list goal in - let (| ctxt, _ |) = normalize_slprop g ctxt true in - let ctxt = slprop_as_list ctxt in - match prove_loop g goal ctxt with - | [] -> () - | unsolved_goals -> - T.fail_doc_at [ - text "Cannot prove remaining precondition:"; - separate hardline (T.map pp unsolved_goals); - text "from context:"; - separate hardline (T.map pp ctxt); - ] (Some r) + let allow_amb = true in + let (| g', ctxt', _ |) = Pulse.Checker.Prover.prove r g ctxt goal allow_amb in + () let symb_eval_stateful_app (g: env) (ctxt: slprop) (t: term) : T.Tac R.term = let t, ty, _ = tc_term_phase1 g t in diff --git a/src/checker/Pulse.Checker.Prover.fst b/src/checker/Pulse.Checker.Prover.fst index fb39a9c66..0693a8d85 100644 --- a/src/checker/Pulse.Checker.Prover.fst +++ b/src/checker/Pulse.Checker.Prover.fst @@ -535,7 +535,7 @@ let check_slprop_equiv_ext r (g:env) (p q:slprop) match res with | None -> fail_doc_with_subissues g (Some r) issues [ - text "rewrite: could not prove equality of"; + text "Could not prove equality of:"; pp p; pp q; ] @@ -1097,11 +1097,12 @@ let prove rng (g: env) (ctxt goals: slprop) allow_amb : ] else [])) (Some rng) else - let before, after = k g' in - let h: slprop_equiv g' (elab_slprops (solved' @ ctxt')) (elab_slprops (ctxt' @ solved' @ goals')) = RU.magic () in - let k = cont_elab_trans before (cont_elab_frame after ctxt') h [] in - let h: slprop_equiv g' (elab_slprops (ctxt' @ [Unknown goals])) (tm_star goals (elab_slprops ctxt')) = RU.magic () in - (| g', RU.deep_compress_safe (elab_slprops ctxt'), k_elab_equiv k (VE_Refl _ _) h |) + (| g', RU.deep_compress_safe (elab_slprops ctxt'), fun post_hint post_hint_typ -> + let before, after = k g' in + let h: slprop_equiv g' (elab_slprops (solved' @ ctxt')) (elab_slprops (ctxt' @ solved' @ goals')) = RU.magic () in + let k = cont_elab_trans before (cont_elab_frame after ctxt') h [] in + let h: slprop_equiv g' (elab_slprops (ctxt' @ [Unknown goals])) (tm_star goals (elab_slprops ctxt')) = RU.magic () in + k_elab_equiv k (VE_Refl _ _) h post_hint post_hint_typ |) #restart-solver #push-options "--z3rlimit_factor 2" @@ -1195,10 +1196,10 @@ let elim_exists_and_pure (#g:env) (#ctxt:slprop) let ctxt' = Pulse.Checker.Prover.Substs.ss_term ctxt ss in let (| g', ctxt'', goals'', solved, k |) = try_elim_core g [Unknown ctxt'] in let h: tot_typing g' (elab_slprops ctxt'') tm_slprop = RU.magic () in // TODO thread through prover - let h1: slprop_equiv g (elab_slprops ([] @ [Unknown ctxt'])) ctxt = (RU.magic() <: slprop_equiv g ctxt' ctxt) in - let h2: slprop_equiv g' (elab_slprops (ctxt'' @ solved @ goals'')) (elab_slprops ([] @ solved @ ctxt'')) = RU.magic () in - let h3: slprop_equiv g' (elab_slprops (ctxt'' @ [])) (elab_slprops ctxt'') = RU.magic () in - let before, after = k g' in - (| g', elab_slprops ctxt'', h, + (| g', elab_slprops ctxt'', h, fun post_hint post_hint_typ -> + let h1: slprop_equiv g (elab_slprops ([] @ [Unknown ctxt'])) ctxt = (RU.magic() <: slprop_equiv g ctxt' ctxt) in + let h2: slprop_equiv g' (elab_slprops (ctxt'' @ solved @ goals'')) (elab_slprops ([] @ solved @ ctxt'')) = RU.magic () in + let h3: slprop_equiv g' (elab_slprops (ctxt'' @ [])) (elab_slprops ctxt'') = RU.magic () in + let before, after = k g' in k_elab_trans (k_elab_equiv (before []) h1 (VE_Refl _ _)) - (k_elab_equiv (after ctxt'') h2 h3) |) \ No newline at end of file + (k_elab_equiv (after ctxt'') h2 h3) post_hint post_hint_typ |) \ No newline at end of file From c00952bbb7becfdfd3ba83694116456d228446e8 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 24 Nov 2025 16:33:32 -0800 Subject: [PATCH 2/2] Fix tests. --- test/LoopInvariants.fst.output.expected | 12 ++++++------ test/bug-reports/Bug174.fst.output.expected | 13 +++++++++---- ...xistsErasedAndPureEqualities.fst.output.expected | 6 +++--- 3 files changed, 18 insertions(+), 13 deletions(-) diff --git a/test/LoopInvariants.fst.output.expected b/test/LoopInvariants.fst.output.expected index b6461471d..acf691794 100644 --- a/test/LoopInvariants.fst.output.expected +++ b/test/LoopInvariants.fst.output.expected @@ -2,23 +2,23 @@ - Expected failure: - When using multiple invariants, they must all be in the "new" style without a binder. -* Info at LoopInvariants.fst(77,4-77,8): +* Info at LoopInvariants.fst(76,20-77,8): - Expected failure: - - rewrite: could not prove equality of + - Could not prove equality of: - Pulse.Lib.Reference.pts_to s 3 - Pulse.Lib.Reference.pts_to s 2 - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also LoopInvariants.fst(77,4-77,10) + - See also LoopInvariants.fst(76,20-77,10) -* Info at LoopInvariants.fst(88,4-88,8): +* Info at LoopInvariants.fst(86,2-88,8): - Expected failure: - - rewrite: could not prove equality of + - Could not prove equality of: - Pulse.Lib.Reference.pts_to s 3 - Pulse.Lib.Reference.pts_to s 2 - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. - - See also LoopInvariants.fst(88,4-88,10) + - See also LoopInvariants.fst(86,2-88,10) diff --git a/test/bug-reports/Bug174.fst.output.expected b/test/bug-reports/Bug174.fst.output.expected index bebb2b81a..e1e7f4475 100644 --- a/test/bug-reports/Bug174.fst.output.expected +++ b/test/bug-reports/Bug174.fst.output.expected @@ -1,9 +1,14 @@ -* Info at Bug174.fst(15,1-16,42): +* Info at Bug174.fst(16,30-16,42): - Expected failure: - - rewrite: could not prove equality of - - Pulse.Lib.Reference.pts_to r v - - Pulse.Lib.Reference.pts_to r v + - Ill-typed term: !r + - Expected a term of type + Pulse.Lib.Core.stt FStar.SizeT.t + (r |-> Pulse.Class.PtsTo.Frac 1.0R v) + (fun x -> + r |-> Pulse.Class.PtsTo.Frac 1.0R v ** + Pulse.Lib.Core.rewrites_to x v) - Assertion failed - The SMT solver could not prove the query. Use --query_stats for more details. + - See also Bug174.fst(15,1-16,40) diff --git a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected index 8c3148a80..c31575d99 100644 --- a/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected +++ b/test/bug-reports/ExistsErasedAndPureEqualities.fst.output.expected @@ -9,9 +9,9 @@ v#269 : FStar.Ghost.erased Prims.int, x#263 : Pulse.Lib.Reference.ref Prims.int -* Info at ExistsErasedAndPureEqualities.fst(70,4-71,21): +* Info at ExistsErasedAndPureEqualities.fst(70,32-72,5): - Expected failure: - - Failed to prove pure property: v == (*?u102*)_ + - Ill-typed term: pure (v == (*?u102*)_) + - Expected a term of type slprop - Cannot check relation with uvars. - - See also ExistsErasedAndPureEqualities.fst(70,23-71,15)