pure/loops: skip output reordering when the ok-tuple is not a permutation of the loop outputs

[karthikbhargavan]

Summary

Translating a function that returns a borrowed value from inside a loop — e.g.

pub fn ret_in_loop(x: &mut u32) -> u32 {
    loop { if *x > 0 { return *x; } *x += 1; }
}

crashed Aeneas with an uncaught internal error (CFailure) that escaped the per-function error recovery and aborted translation of the entire crate.

Root cause: when the forward result coincides with a given-back value, SymbolicToPure produces let v = loop ... in ok (v, v) — the ok-tuple repeats the same fvar. compute_outputs_indices_if_followed_by_ok (src/pure/PureMicroPassesLoops.ml) assumed the ok-tuple args are a permutation of the loop-output pattern; with a duplicated fvar the computed index list has the wrong length and the break-rewriter's sanity check fires (PureMicroPassesLoops.ml:1818-1819). Had the lengths happened to match, duplicated indices would instead have silently duplicated break outputs, so the guard is a correctness fix as well as a crash fix.

Fix: in compute_outputs_indices_if_followed_by_ok, return None unless (a) the ok-tuple args and the loop-output pattern have equal length and (b) the computed index list is duplicate-free (a true permutation). None merely skips the reordering optimization for that loop.

Fixes #22

Validation

All with the pinned charon (v0.1.223, charon-pin = cb50ff16); the repro llbc were regenerated with it.

• Repro before: unpatched dev build on f4_return_in_loop.rs → [Error] Internal error, backtrace through PureMicroPassesLoops.ml, exit 2, no output.
• Repro after: patched build → exit 0, F4.lean generated; the loop function is as expected, with the single loop result used for both outputs:

  def ret_in_loop (x : Std.U32) : Result (Std.U32 × Std.U32) := do
    let x1 ← ret_in_loop_loop x
    ok (x1, x1)

• Control: control_ok.rs (distinct returned value) still translates, exit 0.
• Battery: regenerated all 101 test-suite llbc fixtures from tests/src and ran both the patched and an unpatched dev binary with -backend lean on every fixture: zero exit-code differences; the only 6 non-zero fixtures (borrow_check_negative, loops_borrow_check_negative, raw_pointers, higher_ranked_implied_bounds_{borrow,regions,types}) fail identically on unpatched dev (expected-failure tests). The full extract-tests run (all backends, -checks) passed and left every committed generated output byte-identical (git status clean apart from the source change).
• dune build and dune build @fmt both pass.

🤖 Generated with Claude Code