Borrow flow-sensitive polish (v0.31.11.x)

This chapter covers the three v0.25.x carryovers landed during the v0.31.11.x sub-cycle (May 2026):

1. Flow-sensitive borrow release across if / else arms.
2. Implicit two-phase borrows at call sites.
3. IR-gen path-arg lowering for $$m / $$i parameters passed across free-function call boundaries.

The chapter is example-driven; each pattern below mirrors a regression fixture under tests/bugs/.

1. Per-arm release on if / else

Prior to v0.31.11.x, a borrow taken inside one arm of an if / else extended to the end of the enclosing scope, even when both arms provably released. That over-conservative shape is now narrowed at the join point.

func:main = int32() {
    int32[2]:arr = [10, 20];
    if (cond) {
        $$m int32:slot = arr[0];
        slot = 99;
    } else {
        $$m int32:slot = arr[1];
        slot = 99;
    };
    // both arms released; arr is free again here.
    $$m int32:reuse = arr[0];
    exit reuse;
};

Internally this is pruneArmReleasedLoans in src/frontend/sema/borrow_checker.cpp: loans whose scope provably ends in both arms are released at the join; loans live in either arm remain live afterwards. There is no silent narrowing — if an arm cannot be proven to release (early pass / exit), the loan is conservatively kept live.

K test 165 pins the merge rule.

2. Implicit two-phase borrows

Sequenced read-then-write at the same call site is now handled automatically; you no longer need to manually split:

// before — manual split was required
int32:n = v.len();
v.push(n);

// after — direct form accepted
v.push(v.len());

The two-phase rewrite is a call-site AST rewrite: the read-borrow of the argument expression is sequenced strictly before the write-borrow of the receiver. Already-split code is preserved verbatim (the rewrite is a no-op when the user has split).

ARIA-058 (TWO_PHASE_READ_OUTLIVES_CALL) is reserved but not yet emitted. The current implementation does not produce a case where the read-borrow outlives the call; existing ARIA-023 covers any latent sequential overlap. The diagnostic site is comment-tagged in borrow_checker.cpp for future activation.

K test 166 locks the legal nested form (raw add(raw add(a, b), c)).

3. Path-arg lowering for $$m / $$i across calls

Borrow parameters now flow correctly across free-function call boundaries when the caller pre-binds the path into a named borrow local:

func:bump = int32($$m int32:p) {
    p = p + 5i32;
    pass p;
};

func:main = int32() {
    int32[3]:arr = [10, 20, 30];

    // literal index
    $$m int32:slot = arr[1];
    raw bump(slot);
    exit arr[1];          // -> 25
};

Dynamic indices follow the same shape:

int32:i = 1;
$$m int32:slot = arr[i];
raw bump(slot);
exit arr[1];              // -> 25

Immutable borrows ($$i) work identically for the read direction:

func:peek = int32($$i int32:p) { pass p; };

int32:i = 1;
$$i int32:slot = arr[i];
int32:out = raw peek(slot);
exit out;                 // -> 20

Disjoint borrows at fixed positions

Two $$m borrows into the same array are accepted at disjoint literal positions:

$$m int32:lo = arr[0];
$$m int32:hi = arr[2];
raw add5(lo);
raw add5(hi);
exit 0;

Two $$m borrows at dynamic positions are conservatively rejected by ARIA-023 — the checker treats dynamic indices as wildcards (arr[*]) until a disjointness proof grows in the rules/Z3 layer. Pre-binding can still buy you sequential write access at the same dynamic slot by pass-and-rebind shapes.

Same dynamic index — rejected

int32:i = 1;
$$m int32:a = arr[i];
$$m int32:b = arr[i];   // ARIA-023 — overlapping mutable loans

Inline path-arg syntax — reserved

The current Nitpick parser does not accept inline path arguments at call sites:

// NOT accepted today — parse error.
raw bump($$m arr[i].field);

Pre-binding into a named borrow is mandatory. The future inline form is reserved under ARIA-059 (PATH_ARG_AMBIGUOUS) in borrow_checker.cpp (comment-tag near pruneArmReleasedLoans). Same-slot dynamic aliasing is already covered by ARIA-023 (see the same-dynamic-index case above), so no new emission is required for the current surface.

K modelling note

The K runtime models value flow only across free-function call boundaries — it does not model $$m writeback through a call. K test 167 therefore locks the value-flow form (arr[i] → v → add5(v) → r) using $$i for the array read; the $$m cross-call writeback path is regression-locked by the C++ fixtures (bug541 – bug545) instead. This mirrors the v0.31.10.x precedent for the <func-summaries> cell (XMOD-DEC-009).

Diagnostic summary

Fixtures

Validation status (v0.31.11.4)

• Compiler CTest (this cycle's labels): green (bug_tests_v031111, bug_tests_v031112, bug_tests_v031113).
• K core: 167/167 (was 164/164 entering the sub-cycle).
• K proofs: 11/11.
• Known-flaky test_pin_gc_pressure_v02861 unrelated to this cycle.