interp: fix inverted can_end guard in eliminate_shared_loans

[karthikbhargavan]

Bug

eliminate_shared_loans (src/interp/InterpReduceCollapse.ml) removes shared loans that have no matching shared borrow. Its guard was inverted w.r.t. its own comment ("Only update the non-frozen abstractions"):

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

can_end = false is the frozen case (input abstractions are created with region_can_end _ = false), so the pass mutated exactly the frozen abstractions and skipped the endable join abstractions it was written to clean up. The sibling end_endable_shared_loans_at_abs (InterpAbs.ml) implements the same can_end polarity correctly.

Mechanism

eliminate_shared_loans runs at the end of every reduce_ctx and in collapse_ctx, i.e. on every loop fixed-point round and every join — contexts where frozen-abstraction immutability is load-bearing (join_prefixes' hard sanity_check, compute_fixed_abs_ids). When a matchless shared loan sits inside the frozen input abstraction at loop entry (e.g. after let s = *x; x = y;), the first loop join mutates the frozen abstraction. It then fails the strict-equality recognition in compute_fixed_abs_ids, drops out of fixed_aids, is marker-split and re-kinded endable, and match_ctx_with_target later tries to merge the input abstraction — whose continuation has no output — so merge_abs_conts hits [%craise] "Unreachable" (InterpAbs.ml:1688 on dev). Result: a spurious failure, in both translation and -borrow-check modes, on rustc-valid code.

Fixes #24

Fix

Invert the guard to match its comment (if abs.can_end then ... else abs) and strengthen the comment to state why frozen abstractions must not be touched.

Validation

All with charon at the pinned commit (v0.1.223); repro files from the issue.

• Before (unpatched dev build): f6_matchless_loan.rs and f6_variant_loop_ignores_x.rs fail with [Error] Unreachable (interp/InterpAbs.ml, line 1688) in -backend lean and are rejected by -borrow-check; both controls (control_no_loop.rs, control_loan_kept_alive.rs) pass.
• After (this patch): both repros translate successfully and the generated Lean is correct — the loop uses y's value (def f (x y : Std.U32) ... := f_loop y x 0#u32); both controls still pass; -borrow-check accepts all four.
• Regression battery: full extract-tests suite (with -checks) passes; every regenerated backend output is byte-identical to the committed files (git status clean apart from this fix). Additionally, the patched binary was run with -backend lean on all 101 regenerated tests/llbc/*.llbc fixtures: 95 pass, and the 6 failures (borrow_check_negative, loops_borrow_check_negative, higher_ranked_implied_bounds_{borrow,regions,types}, raw_pointers) fail identically under an unpatched dev build — pre-existing expected failures, not caused by this patch.
• dune build and dune build @fmt pass.

🤖 Generated with Claude Code

[abentkamp]

Right, this is clearly an accidental error in the code. However, I don't think the lengthy comment is necessary. Instead, adding one or two of the examples you found as tests might be useful.