Inverted can_end guard in eliminate_shared_loans mutates frozen abstractions; valid programs rejected #24

Found during an adversarial audit of the join/collapse machinery (2026-07-25). Applies to upstream code: src/interp/InterpReduceCollapse.ml is byte-identical to upstream commit 004e11fe40dee0d8ff1d8d509f0a8985ba2249ad. Empirically reproduced (valid code rejected) and the one-line fix validated.

Description

eliminate_shared_loans (src/interp/InterpReduceCollapse.ml:23-54) removes shared loans that have no matching shared borrow. The guard selecting which abstractions to update is inverted w.r.t. its own comment (:44-46):

let update_abs (abs : abs) : abs =
  (* Only update the non-frozen abstractions *)
  if not abs.can_end then update_loans#visit_abs () abs else abs
in

can_end = false is the frozen case (SynthInput abstractions are created with region_can_end _ = false, src/interp/Interp.ml:284). So the code mutates exactly the frozen abstractions and skips the endable ones it was written for. It runs at the end of every reduce_ctx (InterpReduceCollapse.ml:840), i.e. on every loop fixed-point round (InterpLoopsFixedPoint.ml:207) and join (InterpJoin.ml:1025,1070,1151,1377), where frozen-abstraction immutability is load-bearing (join_prefixes hard sanity_check abs0 = abs1; compute_fixed_abs_ids).

Repro (valid code rejected)

pub fn f<'a>(mut x: &'a u32, y: &'a u32) -> u32 {
    let mut s = *x;
    x = y;                 // the loan created for the first `*x` read is now
    let mut i = 0u32;      // matchless, inside the frozen input abstraction
    loop {
        s = s.wrapping_add(*x);
        i = i.wrapping_add(1);
        if i > 10 { return s; }
    }
}

charon rustc --preset=aeneas --dest-file f6.llbc -- --crate-type=rlib f6_matchless_loan.rs   # charon v0.1.196
aeneas -backend lean f6.llbc -dest out -abort-on-error    # also fails with -borrow-check

• Observed: [Error] Unreachable, Compiler source: interp/InterpAbs.ml, line 1671 (abs_cont_bind_outputs, via merge_abs_conts <- collapse_ctx <- match_ctx_with_target when entering the loop). -borrow-check rejects the function the same way: a spurious borrow-check failure on rustc-valid code.
• Expected: successful translation / borrow-check.

Controls isolating the precondition (both translate fine): same reassignment without a loop; same loop with the original borrow kept alive (loan not matchless). The loop body does not even need to use x.

Mechanism (from -log InterpLoopsFixedPoint,InterpJoin traces): at loop entry the frozen InputAbs contains a matchless shared loan. During the first loop join, the inverted guard mutates it, so it fails to be preserved as a fixed abstraction — it is marker-split, re-kinded endable, and drops out of fixed_aids; match_ctx_with_target later tries to merge the input abstraction, whose continuation has no output, and merge_abs_conts hits the Unreachable.

Fix (validated)

if abs.can_end then update_loans#visit_abs () abs else abs

With only this change, both repro variants translate to correct Lean (the loop correctly uses y's value: def f x y = f_loop y x 0), while the controls and a battery of loop/join tests are unaffected. Cross-check the intended polarity with end_endable_shared_loans_at_abs (InterpAbs.ml:2131), which implements the same idea correctly.