From 254958184131f6a2eea3a0e7cfcb137f7c164b7a Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Fri, 26 Jun 2026 23:09:44 +0300 Subject: [PATCH 1/9] Sketch Pulse stateful bool short-circuiting --- pulse/src/checker/Pulse.Checker.Base.fst | 262 ++++++++++++++++------ pulse/src/checker/Pulse.Checker.Base.fsti | 6 + pulse/src/checker/Pulse.Checker.Bind.fst | 21 +- pulse/src/checker/Pulse.Checker.fst | 6 +- pulse/src/checker/Pulse.JoinComp.fst | 134 ++++++++--- pulse/test/ShortCircuitStatefulBool.fst | 101 +++++++++ 6 files changed, 420 insertions(+), 110 deletions(-) create mode 100644 pulse/test/ShortCircuitStatefulBool.fst diff --git a/pulse/src/checker/Pulse.Checker.Base.fst b/pulse/src/checker/Pulse.Checker.Base.fst index 16423bbba8b..0a641a9fe25 100644 --- a/pulse/src/checker/Pulse.Checker.Base.fst +++ b/pulse/src/checker/Pulse.Checker.Base.fst @@ -595,26 +595,77 @@ let bind_st_term (g:env) (s:st_term) let g = Pulse.Typing.Env.push_binding g x b.binder_ppname b.binder_ty in g, b, x, RT.var_as_term x +type short_circuit_op = + | ShortCircuitAnd + | ShortCircuitOr + +let prims_op_ampamp_lid : R.name = ["Prims"; "op_AmpAmp"] +let prims_op_barbar_lid : R.name = ["Prims"; "op_BarBar"] + +(* F* parses/desugars Pulse `&&` and `||` as ordinary Prims applications. + The generic hoister traverses all application arguments and would therefore + bind both boolean operands before the operator is checked. Recognize these + two applications first and reify their control-flow shape in Pulse syntax, so + the right operand is hoisted only in the branch where the sequential boolean + semantics actually evaluates it. *) +let as_short_circuit_op (head:term) : T.Tac (option short_circuit_op) = + match R.inspect_ln head with + | R.Tv_FVar fv + | R.Tv_UInst fv _ -> + let lid = R.inspect_fv fv in + if lid = prims_op_ampamp_lid then Some ShortCircuitAnd + else if lid = prims_op_barbar_lid then Some ShortCircuitOr + else None + | _ -> None + +let mk_bool_return_st (rng:Range.range) (v:term) : st_term = + mk_term (Tm_Return {expected_type=tm_bool; insert_eq=false; term=v}) rng + (* Hoist a single F*-level Tv_Match branch body by delegating to maybe_hoist. Returns the body as an st_term and whether any hoisting was done. *) -let hoist_branch_body (g:env) (body:term) (rng:Range.range) +let rec hoist_branch_body (g:env) (body:term) (rng:Range.range) (maybe_hoist_fn: env -> T.argv -> T.Tac (env & list (binder & var & st_term) & T.argv)) : T.Tac (st_term & bool) = let body_rng = RU.range_of_term body in - let (_g', binders, (body', _q)) = maybe_hoist_fn g (body, R.Q_Explicit) in - match binders with - | [] -> - (mk_term (Tm_Return {expected_type=tm_unknown;insert_eq=false;term=body}) body_rng, false) - | _ -> - let ret = mk_term (Tm_Return {expected_type=tm_unknown;insert_eq=false;term=body'}) body_rng in - let final_st = List.Tot.fold_right - (fun (b, v, arg) (acc:st_term) -> - let acc' = Pulse.Syntax.Naming.close_st_term acc v in - mk_term (Tm_Bind { binder = b; head = arg; body = acc' }) rng) - binders - ret + match hoist_whole_short_circuit_body g body rng maybe_hoist_fn with + | Some st -> (st, true) + | None -> + let (_g', binders, (body', _q)) = maybe_hoist_fn g (body, R.Q_Explicit) in + match binders with + | [] -> + (mk_term (Tm_Return {expected_type=tm_unknown;insert_eq=false;term=body}) body_rng, false) + | _ -> + let ret = mk_term (Tm_Return {expected_type=tm_unknown;insert_eq=false;term=body'}) body_rng in + let final_st = List.Tot.fold_right + (fun (b, v, arg) (acc:st_term) -> + let acc' = Pulse.Syntax.Naming.close_st_term acc v in + mk_term (Tm_Bind { binder = b; head = arg; body = acc' }) rng) + binders + ret + in + (final_st, true) + +and hoist_whole_short_circuit_body + (g:env) + (body:term) + (rng:Range.range) + (maybe_hoist_fn: env -> T.argv -> T.Tac (env & list (binder & var & st_term) & T.argv)) +: T.Tac (option st_term) += let head, args = T.collect_app_ln body in + match as_short_circuit_op head, args with + | Some op, [(lhs, R.Q_Explicit); (rhs, R.Q_Explicit)] -> + let lhs_st, lhs_changed = hoist_branch_body g lhs rng maybe_hoist_fn in + let rhs_st, rhs_changed = hoist_branch_body g rhs rng maybe_hoist_fn in + if not (lhs_changed || rhs_changed) then None else + let true_st = mk_bool_return_st rng tm_true in + let false_st = mk_bool_return_st rng tm_false in + let then_, else_ = + match op with + | ShortCircuitAnd -> rhs_st, false_st + | ShortCircuitOr -> true_st, rhs_st in - (final_st, true) + Some (mk_term (Tm_If { b = lhs_st; then_; else_; post = None }) rng) + | _ -> None (* Process all branches of an F*-level Tv_Match, hoisting stateful apps in each branch body. Returns processed branches and whether any changed. *) @@ -654,6 +705,28 @@ let convert_fstar_match (g:env) (t:term) ) else None | _ -> None +let convert_short_circuit_app + (g:env) + (head:term) + (args:list T.argv) + (rng:Range.range) + (maybe_hoist_fn: env -> T.argv -> T.Tac (env & list (binder & var & st_term) & T.argv)) +: T.Tac (option st_term) += match as_short_circuit_op head, args with + | Some op, [(lhs, R.Q_Explicit); (rhs, R.Q_Explicit)] -> + let lhs_st, lhs_changed = hoist_branch_body g lhs rng maybe_hoist_fn in + let rhs_st, rhs_changed = hoist_branch_body g rhs rng maybe_hoist_fn in + if not (lhs_changed || rhs_changed) then None else + let true_st = mk_bool_return_st rng tm_true in + let false_st = mk_bool_return_st rng tm_false in + let then_, else_ = + match op with + | ShortCircuitAnd -> rhs_st, false_st + | ShortCircuitOr -> true_st, rhs_st + in + Some (mk_term (Tm_If { b = lhs_st; then_; else_; post = None }) rng) + | _ -> None + let rec maybe_hoist (g:env) (arg:T.argv) : T.Tac (env & list (binder & var & st_term) & T.argv) = let t, q = arg in @@ -667,26 +740,32 @@ let rec maybe_hoist (g:env) (arg:T.argv) let g, b, x, var_t = bind_st_term g st_cond in g, [b, x, st_cond], (var_t, q) | None -> g, [], arg) - | _ -> - match is_stateful_application g t with - | None -> ( - let g, binders, args = maybe_hoist_args g args in - match binders with - | [] -> g, [], arg // no elab - | _ -> - let t = RU.mk_app_flat head args (T.range_of_term t) in - g, binders, (t, q) - ) - | Some _ -> ( - let g, binders, args = maybe_hoist_args g args in - if Cons? args - then ( - let st_app = as_stateful_application t head args in - let g, b, x, t = bind_st_term g st_app in - let arg = t, q in - g, binders@[b, x, st_app], arg - ) - else T.fail "Impossible: is_stateful_application returned true but no args to hoist" + | _ -> ( + match convert_short_circuit_app g head args (T.range_of_term t) maybe_hoist with + | Some st_sc -> + let g, b, x, t = bind_st_term g st_sc in + g, [b, x, st_sc], (t, q) + | None -> + match is_stateful_application g t with + | None -> ( + let g, binders, args = maybe_hoist_args g args in + match binders with + | [] -> g, [], arg // no elab + | _ -> + let t = RU.mk_app_flat head args (T.range_of_term t) in + g, binders, (t, q) + ) + | Some _ -> ( + let g, binders, args = maybe_hoist_args g args in + if Cons? args + then ( + let st_app = as_stateful_application t head args in + let g, b, x, t = bind_st_term g st_app in + let arg = t, q in + g, binders@[b, x, st_app], arg + ) + else T.fail "Impossible: is_stateful_application returned true but no args to hoist" + ) ) and maybe_hoist_args (g:env) (args:list T.argv) @@ -699,6 +778,17 @@ and maybe_hoist_args (g:env) (args:list T.argv) args (g, [], []) +let hoist_short_circuit_return (g:env) (t:term) +: T.Tac (option st_term) += let head, args = T.collect_app_ln t in + convert_short_circuit_app g head args (T.range_of_term t) maybe_hoist + +let hoist_control_flow_return (g:env) (t:term) +: T.Tac (option st_term) += match hoist_short_circuit_return g t with + | Some st -> Some st + | None -> convert_fstar_match g t maybe_hoist + #push-options "--ifuel 1" let maybe_hoist_top (hoist_top_level:bool) @@ -729,44 +819,74 @@ let hoist_stateful_apps = match decompose_app g tt with | None -> None | Some (head, args, rebuild) -> - let _, binders, args = maybe_hoist_args g args in - match args with - | [] -> - // No args after decomposition. Check if the term is an F*-level - // Tv_Match with stateful branches (the "hard case" from #443). - (match tt with - | Inl t -> - (match convert_fstar_match g t maybe_hoist with - | Some st_cond -> - let rng = RU.range_of_term t in - let _, b, v, var_t = bind_st_term g st_cond in - let bind_term = context (Inl var_t) in - let body = Pulse.Syntax.Naming.close_st_term bind_term v in - Some (mk_term (Tm_Bind { binder = b; head = st_cond; body }) rng) - | None -> None) - | _ -> None) - | _ -> - let tt' = rebuild args in - let _, binders', tt' = maybe_hoist_top (hoist_top_level && Inl? tt) g tt' in - let binders = binders @ binders' in - match binders with - | [] -> ( - match tt, tt' with - | Inl _, Inr _ -> ( - Some (context tt') //we at least elaborated a pure term to an inpure term - ) - | _ -> None //No elaboration - ) + match tt with + | Inl t -> ( + let bind_context_to_st (rng:Range.range) (st_cond:st_term) : T.Tac (option st_term) = + let _, b, v, var_t = bind_st_term g st_cond in + let bind_term = context (Inl var_t) in + let body = Pulse.Syntax.Naming.close_st_term bind_term v in + Some (mk_term (Tm_Bind { binder = b; head = st_cond; body }) rng) + in + match convert_short_circuit_app g head args (RU.range_of_term t) maybe_hoist with + | Some st_sc -> bind_context_to_st (RU.range_of_term t) st_sc + | None -> + let _, binders, args = maybe_hoist_args g args in + match args with + | [] -> + // No args after decomposition. Check if the term is an F*-level + // Tv_Match with stateful branches (the "hard case" from #443). + (match convert_fstar_match g t maybe_hoist with + | Some st_cond -> bind_context_to_st (RU.range_of_term t) st_cond + | None -> None) + | _ -> + let tt' = rebuild args in + let _, binders', tt' = maybe_hoist_top (hoist_top_level && Inl? tt) g tt' in + let binders = binders @ binders' in + match binders with + | [] -> ( + match tt, tt' with + | Inl _, Inr _ -> ( + Some (context tt') //we at least elaborated a pure term to an inpure term + ) + | _ -> None //No elaboration + ) + | _ -> + let bind_term = context tt' in + let res = List.Tot.fold_right + (fun (b, v, arg) body -> + let body = Pulse.Syntax.Naming.close_st_term body v in + mk_term (Tm_Bind { binder = b; head = arg; body = body }) bind_term.range) + binders + bind_term + in + Some res + ) + | Inr _ -> + let _, binders, args = maybe_hoist_args g args in + match args with + | [] -> None | _ -> - let bind_term = context tt' in - let res = List.Tot.fold_right - (fun (b, v, arg) body -> - let body = Pulse.Syntax.Naming.close_st_term body v in - mk_term (Tm_Bind { binder = b; head = arg; body = body }) bind_term.range) - binders - bind_term - in - Some res + let tt' = rebuild args in + let _, binders', tt' = maybe_hoist_top (hoist_top_level && Inl? tt) g tt' in + let binders = binders @ binders' in + match binders with + | [] -> ( + match tt, tt' with + | Inl _, Inr _ -> ( + Some (context tt') //we at least elaborated a pure term to an inpure term + ) + | _ -> None //No elaboration + ) + | _ -> + let bind_term = context tt' in + let res = List.Tot.fold_right + (fun (b, v, arg) body -> + let body = Pulse.Syntax.Naming.close_st_term body v in + mk_term (Tm_Bind { binder = b; head = arg; body = body }) bind_term.range) + binders + bind_term + in + Some res let hoist_st_lambda (g:env) diff --git a/pulse/src/checker/Pulse.Checker.Base.fsti b/pulse/src/checker/Pulse.Checker.Base.fsti index 3ef3737e229..e4eae2be03c 100644 --- a/pulse/src/checker/Pulse.Checker.Base.fsti +++ b/pulse/src/checker/Pulse.Checker.Base.fsti @@ -199,6 +199,12 @@ val checker_result_t_equiv_ctxt (g:env) (ctxt ctxt' : slprop) val is_stateful_application (g:env) (e:term) : T.Tac (option st_term) +val hoist_short_circuit_return (g:env) (t:term) +: T.Tac (option st_term) + +val hoist_control_flow_return (g:env) (t:term) +: T.Tac (option st_term) + val hoist (g:env) (tt:either term st_term) diff --git a/pulse/src/checker/Pulse.Checker.Bind.fst b/pulse/src/checker/Pulse.Checker.Bind.fst index addd037dbe2..604d35a4e4e 100644 --- a/pulse/src/checker/Pulse.Checker.Bind.fst +++ b/pulse/src/checker/Pulse.Checker.Bind.fst @@ -26,6 +26,7 @@ open Pulse.Show open Pulse.Checker.Util module T = FStar.Tactics.V2 +module R = FStar.Reflection.V2 module P = Pulse.Syntax.Printer module Abs = Pulse.Checker.Abs @@ -200,6 +201,14 @@ let check_tot_bind = let g = Pulse.Typing.Env.push_context g "check_tot_bind" t.range in let Tm_TotBind { binder=b; head=e1; body=e2 } = t.term in + let body_returns_bound_var (body:st_term) : bool = + match body.term with + | Tm_Return { term } -> + (match R.inspect_ln term with + | R.Tv_BVar bv -> (R.inspect_bv bv).index = 0 + | _ -> false) + | _ -> false + in let rebuild (head:either term st_term) : T.Tac (t:st_term { Tm_Bind? t.term }) = match head with | Inl e1' -> @@ -209,6 +218,16 @@ let check_tot_bind | Inr e1' -> { t with term = Tm_Bind { binder=b; head=e1'; body=e2 } } in + match if body_returns_bound_var e2 + then Pulse.Checker.Base.hoist_control_flow_return g e1 + else None with + | Some t' -> + Pulse.Checker.Util.debug g "pulse.hoist" (fun _ -> + Printf.sprintf "Eta-reduced and elaborated control-flow let\n%s\nto\n%s\n" + (show t) + (show t')); + check g pre post_hint res_ppname t' + | None -> match Pulse.Checker.Base.hoist g (Inl e1) false rebuild with | None -> //no stateful apps; just return the head and check it let t = rebuild (Inl e1) in @@ -221,4 +240,4 @@ let check_tot_bind (show t) (show t')); check g pre post_hint res_ppname t' -#pop-options \ No newline at end of file +#pop-options diff --git a/pulse/src/checker/Pulse.Checker.fst b/pulse/src/checker/Pulse.Checker.fst index d03268d650a..e2c94f5ca97 100644 --- a/pulse/src/checker/Pulse.Checker.fst +++ b/pulse/src/checker/Pulse.Checker.fst @@ -196,7 +196,9 @@ let maybe_elaborate_stateful_head (g:env) (t:st_term) let b' = { b with term = Tm_Return { expected_type; insert_eq; term = bt' } } in {t with term=Tm_If { b=b'; then_=e1; else_=e2; post }} in - Pulse.Checker.Base.hoist g (Inl bt) true rebuild + (match Pulse.Checker.Base.hoist g (Inl bt) true rebuild with + | Some t -> Some t + | None -> None) | _ -> // Stateful condition: transform into let _cond = b; if (return _cond) { e1 } else { e2 } let binder = mk_binder_ppname Pulse.Typing.tm_bool (mk_ppname_no_range "_if_cond") in @@ -262,6 +264,8 @@ let maybe_elaborate_stateful_head (g:env) (t:st_term) {t with term=Tm_Goto { lbl; arg }} in Pulse.Checker.Base.hoist g (Inl arg) true rebuild + | Tm_Return { term = bt } -> + Pulse.Checker.Base.hoist_control_flow_return g bt | _ -> None #pop-options diff --git a/pulse/src/checker/Pulse.JoinComp.fst b/pulse/src/checker/Pulse.JoinComp.fst index 699b56a40a3..10d501b576b 100644 --- a/pulse/src/checker/Pulse.JoinComp.fst +++ b/pulse/src/checker/Pulse.JoinComp.fst @@ -33,7 +33,7 @@ module RT = FStar.Reflection.Typing module R = FStar.Reflection.V2 module RU = Pulse.RuntimeUtils -let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) +let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) : T.Tac slprop = let maybe_close (n, y,ty) (post:slprop) = if not (y `Set.mem` freevars post) then post @@ -43,51 +43,111 @@ let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) tm_exists_sl u b (close_term post y) ) in - let maybe_elim_rewrites_to pr (post:term) : T.Tac term = + let subst_term_with (t:term) (substs:list RT.subst_elt) : T.Tac term = + match substs with + | [] -> t + | _ -> Pulse.Syntax.Naming.subst_term t substs + in + let pure_fact_subst (lhs rhs:term) (allow_symmetric:bool) + : T.Tac (option RT.subst_elt) + = + let open R in + let subst_var_if_not_return (x:term) (replacement:term) : T.Tac (option RT.subst_elt) = + match T.inspect_ln x with + | Tv_Var n1 -> + let n1 = inspect_namedv n1 in + if n1.uniq = x_ret then None + else Some (RT.NT n1.uniq replacement) + | _ -> None + in + match subst_var_if_not_return lhs rhs with + | Some s -> Some s + | None -> + if allow_symmetric + then subst_var_if_not_return rhs lhs + else None + in + let keep_pure_eq n (u:universe) (typ lhs rhs:term) (post:term) : T.Tac term = + tm_with_pure (RT.eq2 u typ lhs rhs) n post + in + let apply_pure_fact pr (substs:list RT.subst_elt) (post:term) + : T.Tac (list RT.subst_elt & term) + = let n, property = pr in let open R in - let hd, args = T.collect_app_ln property in - match T.inspect_ln hd, args with + let property = subst_term_with property substs in + let hd_tm, args = T.collect_app_ln property in + match T.inspect_ln hd_tm, args with | Tv_UInst hd [u], [(typ, Q_Implicit); (lhs, Q_Explicit); (rhs, Q_Explicit)] -> if T.inspect_fv hd = rewrites_to_p_lid then ( - match T.inspect_ln lhs with - | Tv_Var n1 -> - let n1 = inspect_namedv n1 in - if n1.uniq = x_ret then - tm_with_pure (RT.eq2 u typ lhs rhs) n post - else - Pulse.Syntax.Naming.subst_term post [RT.NT n1.uniq rhs] - | _ -> - let eq = RT.eq2 u typ lhs rhs in - tm_with_pure eq n post + match pure_fact_subst lhs rhs false with + | Some s -> + s :: substs, Pulse.Syntax.Naming.subst_term post [s] + | None -> + substs, keep_pure_eq n u typ lhs rhs post ) - else tm_with_pure property n post - | _ -> tm_with_pure property n post + else if FStar.Reflection.TermEq.term_eq hd_tm (`(Prims.eq2 u#0)) + then ( + match pure_fact_subst lhs rhs true with + | Some s -> + s :: substs, Pulse.Syntax.Naming.subst_term post [s] + | None -> + substs, keep_pure_eq n u typ lhs rhs post + ) + else substs, tm_with_pure property n post + | _ -> substs, tm_with_pure property n post in - let close_post = close_post x_ret dom_g g1 in - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret - then close_post tl post - else if y `Set.mem` dom_g - then close_term post x_ret - else ( - let open R in - match T.inspect_ln ty with - | Tv_App hd (p, Q_Explicit) -> ( - match T.inspect_ln hd with - | Tv_FVar fv -> - if inspect_fv fv = R.squash_qn - then close_post tl (maybe_elim_rewrites_to (n, p) post) - else close_post tl (maybe_close (n,y,ty) post) - | _ -> close_post tl (maybe_close (n,y,ty) post) + let rec apply_pure_facts bs1 (substs:list RT.subst_elt) (post:term) + : T.Tac term + = + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret || y `Set.mem` dom_g + then apply_pure_facts tl substs post + else ( + match T.inspect_ln ty with + | R.Tv_App hd (p, R.Q_Explicit) -> ( + match T.inspect_ln hd with + | R.Tv_FVar fv -> + if R.inspect_fv fv = R.squash_qn + then + let substs, post = apply_pure_fact (n, p) substs post in + apply_pure_facts tl substs post + else apply_pure_facts tl substs post + | _ -> apply_pure_facts tl substs post + ) + | _ -> apply_pure_facts tl substs post ) - | _ -> close_post tl (maybe_close (n,y,ty) post) ) - ) - | _::tl -> close_post tl post + | _::tl -> apply_pure_facts tl substs post + in + let rec close_vars bs1 (post:term) : T.Tac term = + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret + then close_vars tl post + else if y `Set.mem` dom_g + then close_term post x_ret + else ( + match T.inspect_ln ty with + | R.Tv_App hd (p, R.Q_Explicit) -> ( + match T.inspect_ln hd with + | R.Tv_FVar fv -> + if R.inspect_fv fv = R.squash_qn + then close_vars tl post + else close_vars tl (maybe_close (n,y,ty) post) + | _ -> close_vars tl (maybe_close (n,y,ty) post) + ) + | _ -> close_vars tl (maybe_close (n,y,ty) post) + ) + ) + | _::tl -> close_vars tl post + in + let post = apply_pure_facts bs1 [] post in + close_vars bs1 post let rec bindings_var_dom : env_bindings -> Set.set var = function | [] -> Set.empty diff --git a/pulse/test/ShortCircuitStatefulBool.fst b/pulse/test/ShortCircuitStatefulBool.fst new file mode 100644 index 00000000000..ffb7ecc9643 --- /dev/null +++ b/pulse/test/ShortCircuitStatefulBool.fst @@ -0,0 +1,101 @@ +module ShortCircuitStatefulBool + +#lang-pulse +open Pulse + +(* Helpers whose state update makes eager evaluation of a skipped operand visible. *) +fn tick_true (n: ref int) + requires n |-> 'v + returns b: bool + ensures n |-> ('v + 1) ** pure (b) +{ + n := !n + 1; + true +} + +fn stateful_and_skips_rhs (flag: ref bool) (n: ref int) + requires flag |-> false ** n |-> 0 + returns b: bool + ensures flag |-> false ** n |-> 0 ** pure (b == false) +{ + (!flag) && tick_true n +} + +fn stateful_and_runs_rhs (flag: ref bool) (n: ref int) + requires flag |-> true ** n |-> 0 + returns b: bool + ensures flag |-> true ** n |-> 1 ** pure (b) +{ + (!flag) && tick_true n +} + +fn stateful_or_skips_rhs (flag: ref bool) (n: ref int) + requires flag |-> true ** n |-> 0 + returns b: bool + ensures flag |-> true ** n |-> 0 ** pure (b) +{ + (!flag) || tick_true n +} + +fn stateful_or_runs_rhs (flag: ref bool) (n: ref int) + requires flag |-> false ** n |-> 0 + returns b: bool + ensures flag |-> false ** n |-> 1 ** pure (b) +{ + (!flag) || tick_true n +} + +fn nested_stateful_and_or (a: ref bool) (b: ref bool) (n: ref int) + requires a |-> false ** b |-> false ** n |-> 0 + returns r: bool + ensures a |-> false ** b |-> false ** n |-> 0 ** pure (r == false) +{ + (!a) && ((!b) || tick_true n) +} + +fn nested_stateful_or_and (a: ref bool) (b: ref bool) (n: ref int) + requires a |-> true ** b |-> true ** n |-> 0 + returns r: bool + ensures a |-> true ** b |-> true ** n |-> 0 ** pure (r) +{ + (!a) || ((!b) && tick_true n) +} + +(* Equivalent expression-position conditionals. The condition is not a bare + variable after hoisting the read; branch joining must still infer a usable + postcondition and simplify it under the branch hypothesis. *) +fn explicit_if_expr_then (i: ref int) (n: ref int) + requires i |-> 1 ** n |-> 0 + returns b: bool + ensures i |-> 1 ** n |-> 1 ** pure (b) +{ + let b = (if (!i = 1) then tick_true n else false); + b +} + +fn explicit_if_expr_else (i: ref int) (n: ref int) + requires i |-> 1 ** n |-> 0 + returns b: bool + ensures i |-> 1 ** n |-> 0 ** pure (b == false) +{ + let b = (if (!i = 0) then tick_true n else false); + b +} + +fn while_guard_and_short_circuits (i: ref int) (n: ref int) + requires i |-> 1 ** n |-> 0 + ensures i |-> 1 ** n |-> 0 +{ + while ((!i = 0) && tick_true n) + invariant i |-> 1 ** n |-> 0 + { () } +} + +fn pure_operands_no_regression (x: bool) (y: bool) + returns r: bool + ensures pure (r == ((x && y) || (x || y))) +{ + let a = x && y; + let b = x || y; + a || b +} From a645413057f42aa28daf3c2d8457bb3eab1c99d0 Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Fri, 26 Jun 2026 23:55:50 +0300 Subject: [PATCH 2/9] Drop broad Pulse postcondition substitution sketch --- pulse/src/checker/Pulse.JoinComp.fst | 134 ++++++++------------------- 1 file changed, 37 insertions(+), 97 deletions(-) diff --git a/pulse/src/checker/Pulse.JoinComp.fst b/pulse/src/checker/Pulse.JoinComp.fst index 10d501b576b..5968012892b 100644 --- a/pulse/src/checker/Pulse.JoinComp.fst +++ b/pulse/src/checker/Pulse.JoinComp.fst @@ -33,7 +33,7 @@ module RT = FStar.Reflection.Typing module R = FStar.Reflection.V2 module RU = Pulse.RuntimeUtils -let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) +let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) : T.Tac slprop = let maybe_close (n, y,ty) (post:slprop) = if not (y `Set.mem` freevars post) then post @@ -43,111 +43,51 @@ let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) tm_exists_sl u b (close_term post y) ) in - let subst_term_with (t:term) (substs:list RT.subst_elt) : T.Tac term = - match substs with - | [] -> t - | _ -> Pulse.Syntax.Naming.subst_term t substs - in - let pure_fact_subst (lhs rhs:term) (allow_symmetric:bool) - : T.Tac (option RT.subst_elt) - = - let open R in - let subst_var_if_not_return (x:term) (replacement:term) : T.Tac (option RT.subst_elt) = - match T.inspect_ln x with - | Tv_Var n1 -> - let n1 = inspect_namedv n1 in - if n1.uniq = x_ret then None - else Some (RT.NT n1.uniq replacement) - | _ -> None - in - match subst_var_if_not_return lhs rhs with - | Some s -> Some s - | None -> - if allow_symmetric - then subst_var_if_not_return rhs lhs - else None - in - let keep_pure_eq n (u:universe) (typ lhs rhs:term) (post:term) : T.Tac term = - tm_with_pure (RT.eq2 u typ lhs rhs) n post - in - let apply_pure_fact pr (substs:list RT.subst_elt) (post:term) - : T.Tac (list RT.subst_elt & term) - = + let maybe_elim_rewrites_to pr (post:term) : T.Tac term = let n, property = pr in let open R in - let property = subst_term_with property substs in - let hd_tm, args = T.collect_app_ln property in - match T.inspect_ln hd_tm, args with + let hd, args = T.collect_app_ln property in + match T.inspect_ln hd, args with | Tv_UInst hd [u], [(typ, Q_Implicit); (lhs, Q_Explicit); (rhs, Q_Explicit)] -> if T.inspect_fv hd = rewrites_to_p_lid then ( - match pure_fact_subst lhs rhs false with - | Some s -> - s :: substs, Pulse.Syntax.Naming.subst_term post [s] - | None -> - substs, keep_pure_eq n u typ lhs rhs post - ) - else if FStar.Reflection.TermEq.term_eq hd_tm (`(Prims.eq2 u#0)) - then ( - match pure_fact_subst lhs rhs true with - | Some s -> - s :: substs, Pulse.Syntax.Naming.subst_term post [s] - | None -> - substs, keep_pure_eq n u typ lhs rhs post - ) - else substs, tm_with_pure property n post - | _ -> substs, tm_with_pure property n post - in - let rec apply_pure_facts bs1 (substs:list RT.subst_elt) (post:term) - : T.Tac term - = - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret || y `Set.mem` dom_g - then apply_pure_facts tl substs post - else ( - match T.inspect_ln ty with - | R.Tv_App hd (p, R.Q_Explicit) -> ( - match T.inspect_ln hd with - | R.Tv_FVar fv -> - if R.inspect_fv fv = R.squash_qn - then - let substs, post = apply_pure_fact (n, p) substs post in - apply_pure_facts tl substs post - else apply_pure_facts tl substs post - | _ -> apply_pure_facts tl substs post - ) - | _ -> apply_pure_facts tl substs post + match T.inspect_ln lhs with + | Tv_Var n1 -> + let n1 = inspect_namedv n1 in + if n1.uniq = x_ret then + tm_with_pure (RT.eq2 u typ lhs rhs) n post + else + Pulse.Syntax.Naming.subst_term post [RT.NT n1.uniq rhs] + | _ -> + let eq = RT.eq2 u typ lhs rhs in + tm_with_pure eq n post ) - ) - | _::tl -> apply_pure_facts tl substs post + else tm_with_pure property n post + | _ -> tm_with_pure property n post in - let rec close_vars bs1 (post:term) : T.Tac term = - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret - then close_vars tl post - else if y `Set.mem` dom_g - then close_term post x_ret - else ( - match T.inspect_ln ty with - | R.Tv_App hd (p, R.Q_Explicit) -> ( - match T.inspect_ln hd with - | R.Tv_FVar fv -> - if R.inspect_fv fv = R.squash_qn - then close_vars tl post - else close_vars tl (maybe_close (n,y,ty) post) - | _ -> close_vars tl (maybe_close (n,y,ty) post) - ) - | _ -> close_vars tl (maybe_close (n,y,ty) post) + let close_post = close_post x_ret dom_g g1 in + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret + then close_post tl post + else if y `Set.mem` dom_g + then close_term post x_ret + else ( + let open R in + match T.inspect_ln ty with + | Tv_App hd (p, Q_Explicit) -> ( + match T.inspect_ln hd with + | Tv_FVar fv -> + if inspect_fv fv = R.squash_qn + then close_post tl (maybe_elim_rewrites_to (n, p) post) + else close_post tl (maybe_close (n,y,ty) post) + | _ -> close_post tl (maybe_close (n,y,ty) post) ) + | _ -> close_post tl (maybe_close (n,y,ty) post) ) - | _::tl -> close_vars tl post - in - let post = apply_pure_facts bs1 [] post in - close_vars bs1 post + ) + | _::tl -> close_post tl post let rec bindings_var_dom : env_bindings -> Set.set var = function | [] -> Set.empty From 0d0694cf79450cca58496114c82d37951fc39b44 Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 00:56:48 +0300 Subject: [PATCH 3/9] Account for Pulse while guard limitation --- .../pulse/examples/PulseExample.ContiguousSubSequence.fst | 6 +++--- pulse/test/ShortCircuitStatefulBool.fst | 3 +++ 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst index 88fa7f35e03..e698eeca391 100644 --- a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst +++ b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst @@ -38,8 +38,8 @@ ensures let mut i0 : SZ.t = 0sz; let mut i1 : SZ.t = j; while ( - (!i0 <> len0 && - !i1 <> len1) + let v1 = !i1; + (!i0 <> len0 && v1 <> len1) ) invariant exists* v0 v1. @@ -108,4 +108,4 @@ ensures } }; false -} \ No newline at end of file +} diff --git a/pulse/test/ShortCircuitStatefulBool.fst b/pulse/test/ShortCircuitStatefulBool.fst index ffb7ecc9643..4d290fa0407 100644 --- a/pulse/test/ShortCircuitStatefulBool.fst +++ b/pulse/test/ShortCircuitStatefulBool.fst @@ -82,6 +82,9 @@ fn explicit_if_expr_else (i: ref int) (n: ref int) b } +(* The while checker still cannot infer the postcondition for a guard whose + boolean result is tied to a stateful short-circuit branch. *) +[@@expect_failure] fn while_guard_and_short_circuits (i: ref int) (n: ref int) requires i |-> 1 ** n |-> 0 ensures i |-> 1 ** n |-> 0 From 74a3e3eebaf8688369e6fdf565a612d5c6da7dcf Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 09:12:20 +0300 Subject: [PATCH 4/9] Avoid repeated impure reads in Pulse example post --- .../pulse/examples/PulseExample.ContiguousSubSequence.fst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst index e698eeca391..10ac83467a6 100644 --- a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst +++ b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst @@ -54,7 +54,9 @@ ensures starts_with_at (SZ.v j) (take s0 (SZ.v v0)) s1 ) ensures - (!i1 < len1 /\ !i0 < len0 /\ Seq.index s1 (SZ.v !i1) =!= Seq.index s0 (SZ.v !i0)) + (let v1 = !i1; + let v0 = !i0; + v1 < len1 /\ v0 < len0 /\ Seq.index s1 (SZ.v v1) =!= Seq.index s0 (SZ.v v0)) { let v0 = !i0; let v1 = !i1; From 01943303f2b0feb5303a1da9113607092777d20a Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 10:11:08 +0300 Subject: [PATCH 5/9] Fix Pulse example post let syntax --- .../pulse/examples/PulseExample.ContiguousSubSequence.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst index 10ac83467a6..2e27cec74ac 100644 --- a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst +++ b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst @@ -54,8 +54,8 @@ ensures starts_with_at (SZ.v j) (take s0 (SZ.v v0)) s1 ) ensures - (let v1 = !i1; - let v0 = !i0; + (let v1 = !i1 in + let v0 = !i0 in v1 < len1 /\ v0 < len0 /\ Seq.index s1 (SZ.v v1) =!= Seq.index s0 (SZ.v v0)) { let v0 = !i0; From 3312addc6cbbaa5079fb901d264eacaa763bdc70 Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 11:12:03 +0300 Subject: [PATCH 6/9] Use direct Pulse reads in example postcondition --- .../pulse/examples/PulseExample.ContiguousSubSequence.fst | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst index 2e27cec74ac..e698eeca391 100644 --- a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst +++ b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst @@ -54,9 +54,7 @@ ensures starts_with_at (SZ.v j) (take s0 (SZ.v v0)) s1 ) ensures - (let v1 = !i1 in - let v0 = !i0 in - v1 < len1 /\ v0 < len0 /\ Seq.index s1 (SZ.v v1) =!= Seq.index s0 (SZ.v v0)) + (!i1 < len1 /\ !i0 < len0 /\ Seq.index s1 (SZ.v !i1) =!= Seq.index s0 (SZ.v !i0)) { let v0 = !i0; let v1 = !i1; From edc1806a6fb93c20012b23d3458a637590cbf2ff Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 12:35:22 +0300 Subject: [PATCH 7/9] Narrow Pulse short-circuit hoisting --- .../PulseExample.ContiguousSubSequence.fst | 4 +- pulse/src/checker/Pulse.Checker.Base.fst | 4 +- pulse/src/checker/Pulse.Checker.fst | 6 +- pulse/src/checker/Pulse.JoinComp.fst | 134 +++++++++++++----- pulse/test/ShortCircuitStatefulBool.fst | 18 ++- 5 files changed, 115 insertions(+), 51 deletions(-) diff --git a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst index e698eeca391..2630bf2eb31 100644 --- a/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst +++ b/pulse/share/pulse/examples/PulseExample.ContiguousSubSequence.fst @@ -38,8 +38,8 @@ ensures let mut i0 : SZ.t = 0sz; let mut i1 : SZ.t = j; while ( - let v1 = !i1; - (!i0 <> len0 && v1 <> len1) + (!i0 <> len0 && + !i1 <> len1) ) invariant exists* v0 v1. diff --git a/pulse/src/checker/Pulse.Checker.Base.fst b/pulse/src/checker/Pulse.Checker.Base.fst index 0a641a9fe25..8db9a083647 100644 --- a/pulse/src/checker/Pulse.Checker.Base.fst +++ b/pulse/src/checker/Pulse.Checker.Base.fst @@ -827,7 +827,9 @@ let hoist_stateful_apps let body = Pulse.Syntax.Naming.close_st_term bind_term v in Some (mk_term (Tm_Bind { binder = b; head = st_cond; body }) rng) in - match convert_short_circuit_app g head args (RU.range_of_term t) maybe_hoist with + match if hoist_top_level + then convert_short_circuit_app g head args (RU.range_of_term t) maybe_hoist + else None with | Some st_sc -> bind_context_to_st (RU.range_of_term t) st_sc | None -> let _, binders, args = maybe_hoist_args g args in diff --git a/pulse/src/checker/Pulse.Checker.fst b/pulse/src/checker/Pulse.Checker.fst index e2c94f5ca97..d03268d650a 100644 --- a/pulse/src/checker/Pulse.Checker.fst +++ b/pulse/src/checker/Pulse.Checker.fst @@ -196,9 +196,7 @@ let maybe_elaborate_stateful_head (g:env) (t:st_term) let b' = { b with term = Tm_Return { expected_type; insert_eq; term = bt' } } in {t with term=Tm_If { b=b'; then_=e1; else_=e2; post }} in - (match Pulse.Checker.Base.hoist g (Inl bt) true rebuild with - | Some t -> Some t - | None -> None) + Pulse.Checker.Base.hoist g (Inl bt) true rebuild | _ -> // Stateful condition: transform into let _cond = b; if (return _cond) { e1 } else { e2 } let binder = mk_binder_ppname Pulse.Typing.tm_bool (mk_ppname_no_range "_if_cond") in @@ -264,8 +262,6 @@ let maybe_elaborate_stateful_head (g:env) (t:st_term) {t with term=Tm_Goto { lbl; arg }} in Pulse.Checker.Base.hoist g (Inl arg) true rebuild - | Tm_Return { term = bt } -> - Pulse.Checker.Base.hoist_control_flow_return g bt | _ -> None #pop-options diff --git a/pulse/src/checker/Pulse.JoinComp.fst b/pulse/src/checker/Pulse.JoinComp.fst index 5968012892b..10d501b576b 100644 --- a/pulse/src/checker/Pulse.JoinComp.fst +++ b/pulse/src/checker/Pulse.JoinComp.fst @@ -33,7 +33,7 @@ module RT = FStar.Reflection.Typing module R = FStar.Reflection.V2 module RU = Pulse.RuntimeUtils -let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) +let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) : T.Tac slprop = let maybe_close (n, y,ty) (post:slprop) = if not (y `Set.mem` freevars post) then post @@ -43,51 +43,111 @@ let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) tm_exists_sl u b (close_term post y) ) in - let maybe_elim_rewrites_to pr (post:term) : T.Tac term = + let subst_term_with (t:term) (substs:list RT.subst_elt) : T.Tac term = + match substs with + | [] -> t + | _ -> Pulse.Syntax.Naming.subst_term t substs + in + let pure_fact_subst (lhs rhs:term) (allow_symmetric:bool) + : T.Tac (option RT.subst_elt) + = + let open R in + let subst_var_if_not_return (x:term) (replacement:term) : T.Tac (option RT.subst_elt) = + match T.inspect_ln x with + | Tv_Var n1 -> + let n1 = inspect_namedv n1 in + if n1.uniq = x_ret then None + else Some (RT.NT n1.uniq replacement) + | _ -> None + in + match subst_var_if_not_return lhs rhs with + | Some s -> Some s + | None -> + if allow_symmetric + then subst_var_if_not_return rhs lhs + else None + in + let keep_pure_eq n (u:universe) (typ lhs rhs:term) (post:term) : T.Tac term = + tm_with_pure (RT.eq2 u typ lhs rhs) n post + in + let apply_pure_fact pr (substs:list RT.subst_elt) (post:term) + : T.Tac (list RT.subst_elt & term) + = let n, property = pr in let open R in - let hd, args = T.collect_app_ln property in - match T.inspect_ln hd, args with + let property = subst_term_with property substs in + let hd_tm, args = T.collect_app_ln property in + match T.inspect_ln hd_tm, args with | Tv_UInst hd [u], [(typ, Q_Implicit); (lhs, Q_Explicit); (rhs, Q_Explicit)] -> if T.inspect_fv hd = rewrites_to_p_lid then ( - match T.inspect_ln lhs with - | Tv_Var n1 -> - let n1 = inspect_namedv n1 in - if n1.uniq = x_ret then - tm_with_pure (RT.eq2 u typ lhs rhs) n post - else - Pulse.Syntax.Naming.subst_term post [RT.NT n1.uniq rhs] - | _ -> - let eq = RT.eq2 u typ lhs rhs in - tm_with_pure eq n post + match pure_fact_subst lhs rhs false with + | Some s -> + s :: substs, Pulse.Syntax.Naming.subst_term post [s] + | None -> + substs, keep_pure_eq n u typ lhs rhs post ) - else tm_with_pure property n post - | _ -> tm_with_pure property n post + else if FStar.Reflection.TermEq.term_eq hd_tm (`(Prims.eq2 u#0)) + then ( + match pure_fact_subst lhs rhs true with + | Some s -> + s :: substs, Pulse.Syntax.Naming.subst_term post [s] + | None -> + substs, keep_pure_eq n u typ lhs rhs post + ) + else substs, tm_with_pure property n post + | _ -> substs, tm_with_pure property n post in - let close_post = close_post x_ret dom_g g1 in - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret - then close_post tl post - else if y `Set.mem` dom_g - then close_term post x_ret - else ( - let open R in - match T.inspect_ln ty with - | Tv_App hd (p, Q_Explicit) -> ( - match T.inspect_ln hd with - | Tv_FVar fv -> - if inspect_fv fv = R.squash_qn - then close_post tl (maybe_elim_rewrites_to (n, p) post) - else close_post tl (maybe_close (n,y,ty) post) - | _ -> close_post tl (maybe_close (n,y,ty) post) + let rec apply_pure_facts bs1 (substs:list RT.subst_elt) (post:term) + : T.Tac term + = + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret || y `Set.mem` dom_g + then apply_pure_facts tl substs post + else ( + match T.inspect_ln ty with + | R.Tv_App hd (p, R.Q_Explicit) -> ( + match T.inspect_ln hd with + | R.Tv_FVar fv -> + if R.inspect_fv fv = R.squash_qn + then + let substs, post = apply_pure_fact (n, p) substs post in + apply_pure_facts tl substs post + else apply_pure_facts tl substs post + | _ -> apply_pure_facts tl substs post + ) + | _ -> apply_pure_facts tl substs post ) - | _ -> close_post tl (maybe_close (n,y,ty) post) ) - ) - | _::tl -> close_post tl post + | _::tl -> apply_pure_facts tl substs post + in + let rec close_vars bs1 (post:term) : T.Tac term = + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret + then close_vars tl post + else if y `Set.mem` dom_g + then close_term post x_ret + else ( + match T.inspect_ln ty with + | R.Tv_App hd (p, R.Q_Explicit) -> ( + match T.inspect_ln hd with + | R.Tv_FVar fv -> + if R.inspect_fv fv = R.squash_qn + then close_vars tl post + else close_vars tl (maybe_close (n,y,ty) post) + | _ -> close_vars tl (maybe_close (n,y,ty) post) + ) + | _ -> close_vars tl (maybe_close (n,y,ty) post) + ) + ) + | _::tl -> close_vars tl post + in + let post = apply_pure_facts bs1 [] post in + close_vars bs1 post let rec bindings_var_dom : env_bindings -> Set.set var = function | [] -> Set.empty diff --git a/pulse/test/ShortCircuitStatefulBool.fst b/pulse/test/ShortCircuitStatefulBool.fst index 4d290fa0407..381c697cc2f 100644 --- a/pulse/test/ShortCircuitStatefulBool.fst +++ b/pulse/test/ShortCircuitStatefulBool.fst @@ -18,7 +18,8 @@ fn stateful_and_skips_rhs (flag: ref bool) (n: ref int) returns b: bool ensures flag |-> false ** n |-> 0 ** pure (b == false) { - (!flag) && tick_true n + let b = (!flag) && tick_true n; + b } fn stateful_and_runs_rhs (flag: ref bool) (n: ref int) @@ -26,7 +27,8 @@ fn stateful_and_runs_rhs (flag: ref bool) (n: ref int) returns b: bool ensures flag |-> true ** n |-> 1 ** pure (b) { - (!flag) && tick_true n + let b = (!flag) && tick_true n; + b } fn stateful_or_skips_rhs (flag: ref bool) (n: ref int) @@ -34,7 +36,8 @@ fn stateful_or_skips_rhs (flag: ref bool) (n: ref int) returns b: bool ensures flag |-> true ** n |-> 0 ** pure (b) { - (!flag) || tick_true n + let b = (!flag) || tick_true n; + b } fn stateful_or_runs_rhs (flag: ref bool) (n: ref int) @@ -42,7 +45,8 @@ fn stateful_or_runs_rhs (flag: ref bool) (n: ref int) returns b: bool ensures flag |-> false ** n |-> 1 ** pure (b) { - (!flag) || tick_true n + let b = (!flag) || tick_true n; + b } fn nested_stateful_and_or (a: ref bool) (b: ref bool) (n: ref int) @@ -50,7 +54,8 @@ fn nested_stateful_and_or (a: ref bool) (b: ref bool) (n: ref int) returns r: bool ensures a |-> false ** b |-> false ** n |-> 0 ** pure (r == false) { - (!a) && ((!b) || tick_true n) + let r = (!a) && ((!b) || tick_true n); + r } fn nested_stateful_or_and (a: ref bool) (b: ref bool) (n: ref int) @@ -58,7 +63,8 @@ fn nested_stateful_or_and (a: ref bool) (b: ref bool) (n: ref int) returns r: bool ensures a |-> true ** b |-> true ** n |-> 0 ** pure (r) { - (!a) || ((!b) && tick_true n) + let r = (!a) || ((!b) && tick_true n); + r } (* Equivalent expression-position conditionals. The condition is not a bare From b8603029b876cf6ae2f945c7b425d756d9be6ee3 Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 13:34:01 +0300 Subject: [PATCH 8/9] Keep Pulse pure facts after substitution --- pulse/src/checker/Pulse.JoinComp.fst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pulse/src/checker/Pulse.JoinComp.fst b/pulse/src/checker/Pulse.JoinComp.fst index 10d501b576b..a035031d0e8 100644 --- a/pulse/src/checker/Pulse.JoinComp.fst +++ b/pulse/src/checker/Pulse.JoinComp.fst @@ -83,7 +83,7 @@ let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) then ( match pure_fact_subst lhs rhs false with | Some s -> - s :: substs, Pulse.Syntax.Naming.subst_term post [s] + s :: substs, keep_pure_eq n u typ lhs rhs (Pulse.Syntax.Naming.subst_term post [s]) | None -> substs, keep_pure_eq n u typ lhs rhs post ) @@ -91,7 +91,7 @@ let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) then ( match pure_fact_subst lhs rhs true with | Some s -> - s :: substs, Pulse.Syntax.Naming.subst_term post [s] + s :: substs, keep_pure_eq n u typ lhs rhs (Pulse.Syntax.Naming.subst_term post [s]) | None -> substs, keep_pure_eq n u typ lhs rhs post ) From 919cb1418d564bc17c582d14f31aaa663d6cb727 Mon Sep 17 00:00:00 2001 From: seiko1337 Date: Sat, 27 Jun 2026 13:52:50 +0300 Subject: [PATCH 9/9] Narrow Pulse join pure substitutions --- pulse/src/checker/Pulse.JoinComp.fst | 128 +++++++++------------------ 1 file changed, 42 insertions(+), 86 deletions(-) diff --git a/pulse/src/checker/Pulse.JoinComp.fst b/pulse/src/checker/Pulse.JoinComp.fst index a035031d0e8..f1fbecf2bc2 100644 --- a/pulse/src/checker/Pulse.JoinComp.fst +++ b/pulse/src/checker/Pulse.JoinComp.fst @@ -33,7 +33,7 @@ module RT = FStar.Reflection.Typing module R = FStar.Reflection.V2 module RU = Pulse.RuntimeUtils -let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) +let rec close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) : T.Tac slprop = let maybe_close (n, y,ty) (post:slprop) = if not (y `Set.mem` freevars post) then post @@ -43,111 +43,67 @@ let close_post x_ret dom_g g1 (bs1:env_bindings) (post:slprop) tm_exists_sl u b (close_term post y) ) in - let subst_term_with (t:term) (substs:list RT.subst_elt) : T.Tac term = - match substs with - | [] -> t - | _ -> Pulse.Syntax.Naming.subst_term t substs - in - let pure_fact_subst (lhs rhs:term) (allow_symmetric:bool) - : T.Tac (option RT.subst_elt) - = + let subst_var_if_not_return (x:term) (replacement:term) : T.Tac (option RT.subst_elt) = let open R in - let subst_var_if_not_return (x:term) (replacement:term) : T.Tac (option RT.subst_elt) = - match T.inspect_ln x with - | Tv_Var n1 -> - let n1 = inspect_namedv n1 in - if n1.uniq = x_ret then None - else Some (RT.NT n1.uniq replacement) - | _ -> None - in - match subst_var_if_not_return lhs rhs with - | Some s -> Some s - | None -> - if allow_symmetric - then subst_var_if_not_return rhs lhs - else None - in - let keep_pure_eq n (u:universe) (typ lhs rhs:term) (post:term) : T.Tac term = - tm_with_pure (RT.eq2 u typ lhs rhs) n post + match T.inspect_ln x with + | Tv_Var n1 -> + let n1 = inspect_namedv n1 in + if n1.uniq = x_ret then None + else Some (RT.NT n1.uniq replacement) + | _ -> None in - let apply_pure_fact pr (substs:list RT.subst_elt) (post:term) - : T.Tac (list RT.subst_elt & term) - = + let maybe_elim_pure_fact pr (post:term) : T.Tac term = let n, property = pr in let open R in - let property = subst_term_with property substs in let hd_tm, args = T.collect_app_ln property in match T.inspect_ln hd_tm, args with | Tv_UInst hd [u], [(typ, Q_Implicit); (lhs, Q_Explicit); (rhs, Q_Explicit)] -> if T.inspect_fv hd = rewrites_to_p_lid then ( - match pure_fact_subst lhs rhs false with + match subst_var_if_not_return lhs rhs with | Some s -> - s :: substs, keep_pure_eq n u typ lhs rhs (Pulse.Syntax.Naming.subst_term post [s]) + Pulse.Syntax.Naming.subst_term post [s] | None -> - substs, keep_pure_eq n u typ lhs rhs post + tm_with_pure (RT.eq2 u typ lhs rhs) n post ) else if FStar.Reflection.TermEq.term_eq hd_tm (`(Prims.eq2 u#0)) then ( - match pure_fact_subst lhs rhs true with + match subst_var_if_not_return lhs rhs with | Some s -> - s :: substs, keep_pure_eq n u typ lhs rhs (Pulse.Syntax.Naming.subst_term post [s]) + tm_with_pure property n (Pulse.Syntax.Naming.subst_term post [s]) | None -> - substs, keep_pure_eq n u typ lhs rhs post - ) - else substs, tm_with_pure property n post - | _ -> substs, tm_with_pure property n post - in - let rec apply_pure_facts bs1 (substs:list RT.subst_elt) (post:term) - : T.Tac term - = - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret || y `Set.mem` dom_g - then apply_pure_facts tl substs post - else ( - match T.inspect_ln ty with - | R.Tv_App hd (p, R.Q_Explicit) -> ( - match T.inspect_ln hd with - | R.Tv_FVar fv -> - if R.inspect_fv fv = R.squash_qn - then - let substs, post = apply_pure_fact (n, p) substs post in - apply_pure_facts tl substs post - else apply_pure_facts tl substs post - | _ -> apply_pure_facts tl substs post - ) - | _ -> apply_pure_facts tl substs post + (match subst_var_if_not_return rhs lhs with + | Some s -> + tm_with_pure property n (Pulse.Syntax.Naming.subst_term post [s]) + | None -> + tm_with_pure property n post) ) - ) - | _::tl -> apply_pure_facts tl substs post + else tm_with_pure property n post + | _ -> tm_with_pure property n post in - let rec close_vars bs1 (post:term) : T.Tac term = - match bs1 with - | [] -> post - | BindingVar {n;x=y;ty}::tl -> ( - if y = x_ret - then close_vars tl post - else if y `Set.mem` dom_g - then close_term post x_ret - else ( - match T.inspect_ln ty with - | R.Tv_App hd (p, R.Q_Explicit) -> ( - match T.inspect_ln hd with - | R.Tv_FVar fv -> - if R.inspect_fv fv = R.squash_qn - then close_vars tl post - else close_vars tl (maybe_close (n,y,ty) post) - | _ -> close_vars tl (maybe_close (n,y,ty) post) - ) - | _ -> close_vars tl (maybe_close (n,y,ty) post) + let close_post = close_post x_ret dom_g g1 in + match bs1 with + | [] -> post + | BindingVar {n;x=y;ty}::tl -> ( + if y = x_ret + then close_post tl post + else if y `Set.mem` dom_g + then close_term post x_ret + else ( + let open R in + match T.inspect_ln ty with + | Tv_App hd (p, Q_Explicit) -> ( + match T.inspect_ln hd with + | Tv_FVar fv -> + if inspect_fv fv = R.squash_qn + then close_post tl (maybe_elim_pure_fact (n, p) post) + else close_post tl (maybe_close (n,y,ty) post) + | _ -> close_post tl (maybe_close (n,y,ty) post) ) + | _ -> close_post tl (maybe_close (n,y,ty) post) ) - | _::tl -> close_vars tl post - in - let post = apply_pure_facts bs1 [] post in - close_vars bs1 post + ) + | _::tl -> close_post tl post let rec bindings_var_dom : env_bindings -> Set.set var = function | [] -> Set.empty