[prover] fun_post_of: chained mutations of capturing closures in loop-invoking HOFs

[wrwg]

Tracking anchor for the TODO(#...)s in closure_checker.rs / spec_instrumentation.rs and the staged fun_post_of design.

The major use case of &mut-capturing closures — let s = 0; v.for_each_ref(|e| s += *e) — cannot verify under the carried-mutation model: the HOF applies f N times, but the opaque call-site model havocs the capture once and ensures_of<f> describes exactly one application (a quantified forall i: ensures_of<f>(v[i]) over-constrains the single post value into vacuity, hence the guard rejecting it). The previous (reverted) closure model never verified this shape either — its tests were pragma verify = false admission checks deferring to a "fold-of-ensures encoding" that was never built.

Design: the function value is the advancing state object. One application is a deterministic transition f' = step(f, x); step already exists in the encoding as the trailing fun slot of the $result_of Skolem for carrying fun types. A new two-state behavioral predicate fun_post_of<f>(args) surfaces it, and a recursive spec fun chains it:

spec fun apply_all<T>(f: |&T| has copy + drop, v: vector<T>, end: u64): |&T| has copy + drop {
    if (end == 0) f else fun_post_of<apply_all(f, v, end - 1)>(v[end - 1])
}
spec for_each_ref {
    pragma opaque;
    requires forall i in 0..len(v): !aborts_of<apply_all(f, v, i)>(v[i]);
    aborts_if false;
    ensures f == apply_all(old(f), v, len(v));
}

Callers unfold the chain via the closure-variant axioms (concrete lengths unroll; symbolic lengths need a user lemma — parity with spec_fold). The callee proves the chain with a loop invariant f == apply_all(old(f), v, i), which certifies the application discipline: the successor is an uninterpreted transition on an indexed $param'fn$p'(n) variant family ($result_of(..)->fun_slot == $param($param_next(..)), $param_next uninterpreted — never n+1), so zero-apply, double-apply, and out-of-order bodies face falsifiable VCs.

Staging (stage 1 — guards and admission — is landed with the TODOs pointing here):

• Stage 2, spec language: BehaviorKind::FunPostOf (parser → model → Boogie projection of the $result_of trailing fun slot; identity for non-carrying values); fun params become two-state in specs opt-in per (function, param) — bare f in post conditions keeps today's entry-value meaning unless the spec mentions old(f) or fun_post_of on that param (unconditional flip would break existing spec_fold-style specs, and a per-type trigger would be non-modular); BP subject position stays an implicit old(); admit old(f) (today rejected by the is_pure gate); lift the spec-fun fun-result-type gate (TODO(LAMBDA) in boogie spec_translator.rs) needed for apply_all.
• Stage 3, advancing param variants: indexed $param(n) for opted-in params with entry pinning to $param(0); family axiom; apply param-branch advancement fun_out := $result_of(..)->fun_slot; Invoke rebinding and loop havoc gated on one shared "advancing" predicate — loop havoc is emitted usage-based (over-approximate) at bytecode level and refined at translation (no-op for non-advancing temps, variant-preserving repack for advancing ones); the closure-variant ensures_of axiom body equates f_post to a syntactic ctor application so caller-side chains keep e-matching past the first application; the param-variant axiom constrains f_post for def/call coherence.
• Stage 4: end-to-end accumulator tests, documentation.

Soundness constraints established by adversarial review, to be enforced in stages 2–3: the chain feature is gated on fun types with an empty evaluator memory union (a memory-free fold cannot describe steps under a changing heap); surviving copies of carrying values are model-level errors (linearity — a copy would fork carried state; the copy ability bound is admitted so loop-invoking HOF signatures accept these closures); the call-site vacuity guard must count all post-value constraints per carrying subject (multiple, quantified, or fun_post_of-equated), not just syntactic ensures_of occurrences.

---

Filed by Claude (AI agent) on behalf of @wrwg.

[wrwg]

[Claude Agent] Status update — the design has landed on branch wrwg/chain-lemmas (stacked on wrwg/fun-post-of → wrwg/inline-beh), beyond the staged plan above:

• Stages 1–4 as described: fun_post_of, opt-in two-state fun params, indexed $param(n) families with uninterpreted successor indices, usage-based loop havoc. The motivating accumulator (let s = 0; v.for_each_ref(|e| s += *e)) verifies end-to-end for concrete/bounded lengths.
• Compositional layer (not in the original plan): partial_of<f>(g) / captures_of<f>(g) (closed-world recognizer/selector over the session's variants; witness is any function value), surface write_of<g, j>, universal (unpinned) fun params for lemmas and for variant-observed params, guarded closure-variant axioms, and verify-mode currying of |e| step(&mut s, e) to a partial application of step. With these, a fully generic chain lemma (for_each_chain, generic in the step function) proves the unbounded symbolic-length accumulator: ensures result == spec_sum(v, len(v)) with aborts_if false, no length bound.
• Follow-ups split out: [prover] Recursive lemma application lacks a well-foundedness check #20275 (well-foundedness of recursive lemma application), [prover] Generalize the chain-lemma layer: generic lemma instance checks, multi-captures, apply triggers #20278 (generic lemma instance checks, multi-captures, apply triggers), [prover] Behavioral predicates in spec fun bodies do not contribute to memory usage #20279 (BP memory usage in spec fun bodies). [prover] Fun-value disequalities are provable from constructor distinctness #20274 remains relevant (closed-world negative facts).

Key tests: closures/inline/inline_opaque_hof_{for_each_sum,symbolic_sum,generic_chain}.move, closures/{write_of_surface,partial_of_params{,_fail}}.move. Dev docs: doc/dev/fun_values_note.md.