LLBC: translate wrapping arithmetic as wrapping, and cover what the Charon bump will touch

[feliperodri]

First of the PRs toward moving our Charon pin to current (#4834). The plan is in that issue's thread; this one lands on the old pin, on purpose.

Why tests first. Between our pin and Charon's latest tag, the AST changed how arithmetic overflow, integer types and literals, and switches are represented. The port will compile long before it's correct, and today only the 10 tests in tests/llbc would notice a change in meaning — none of which do arithmetic. So this adds nine tests pinning the current, hand-reviewed LLBC for exactly those constructs. When the bump lands, every changed expected file has to be explained as formatting or intended.

The bug it found. Writing the arithmetic tests turned up a real one: MIR's plain Add/Sub/Mul wrap on overflow, but we translated them to Charon's CheckedAdd/CheckedSub/CheckedMul, which return a (result, overflowed) pair. So intrinsics::wrapping_add produced type-incorrect LLBC:

@0 := copy (a@1) checked.+ copy (b@2)    // @0: u8

Now it's wrapping.+. Checked arithmetic (a + b with overflow checks) still goes through CheckedBinaryOp, which Charon folds with the overflow assert into a panicking + — unchanged, and covered by arith_checked. I confirmed arith_wrapping is the only test that fails without the fix.

Worth a look: I reviewed each expected file by hand rather than trusting the output, and two shapes look odd but are correct — ! prints as ~ for both u8 and bool (Charon uses one symbol for Not), and in switch_int the 0 arm falls through to code after the switch, which is how control-flow reconstruction places it. The expected files leave out main, since its @FunN ids are allocation order and will churn with the bump.

Also: seven existing tests were checking nothing. expected mode ignores the exit status and only looks for the expected lines, so an empty expected file always passes — even if Kani panics. enum, generic, option, projection, struct, traitimpl and tuple all had one, and they cover exactly what the bump re-represents (ADTs, tuples, generics, trait impls). The second commit pins their current, hand-reviewed output. Separately, it might be worth making expected mode reject an empty file outright; I haven't done that here.

Not covered yet, because the backend doesn't translate them today: arrays, slices, str, Box, casts, const generics, supertraits, associated consts. Those are coverage the bump has to add rather than preserve.

tests/llbc 19/19, kani-llbc-regression.sh, fmt, clippy.

[Copilot]

Copilot review overview

🟢 Approval recommended

The arithmetic correction is narrowly scoped and covered by comprehensive LLBC regression expectations.

Review effort: Balanced
Findings: None

What changed in this PR

Fixes LLBC arithmetic translation and establishes regression baselines before upgrading Charon.

Changes:

• Translates plain MIR addition, subtraction, and multiplication as wrapping operations while preserving checked operations.
• Adds nine LLBC regression fixtures for arithmetic, literals, unary operations, and switches.
• Populates seven previously empty LLBC expectations.

File	Description
kani-compiler/​src/​codegen_aeneas_llbc/​mir_to_ullbc/​mod.rs	Separates checked and wrapping arithmetic translation.
tests/​llbc/​arith_checked/​test.rs	Exercises checked arithmetic.
tests/​llbc/​arith_checked/​expected	Pins checked arithmetic LLBC.
tests/​llbc/​arith_unchecked/​test.rs	Exercises unchecked arithmetic.
tests/​llbc/​arith_unchecked/​expected	Pins unchecked arithmetic LLBC.
tests/​llbc/​arith_wrapping/​test.rs	Exercises wrapping arithmetic.
tests/​llbc/​arith_wrapping/​expected	Verifies wrapping operators.
tests/​llbc/​bool_char/​test.rs	Exercises Boolean and character literals.
tests/​llbc/​bool_char/​expected	Pins literal translation.
tests/​llbc/​div_rem/​test.rs	Exercises division and remainder.
tests/​llbc/​div_rem/​expected	Pins division and remainder LLBC.
tests/​llbc/​enum/​expected	Adds the enum baseline.
tests/​llbc/​generic/​expected	Adds the generic baseline.
tests/​llbc/​int_literals/​test.rs	Exercises all integer widths.
tests/​llbc/​int_literals/​expected	Pins integer literal translation.
tests/​llbc/​option/​expected	Adds the generic Option baseline.
tests/​llbc/​projection/​expected	Adds nested projection coverage.
tests/​llbc/​shifts/​test.rs	Exercises signed and unsigned shifts.
tests/​llbc/​shifts/​expected	Pins shift translation.
tests/​llbc/​struct/​expected	Adds the struct baseline.
tests/​llbc/​switch_int/​test.rs	Exercises integer switch reconstruction.
tests/​llbc/​switch_int/​expected	Pins multi-arm switch LLBC.
tests/​llbc/​traitimpl/​expected	Adds trait implementation coverage.
tests/​llbc/​tuple/​expected	Adds the tuple baseline.
tests/​llbc/​unops/​test.rs	Exercises negation and not operations.
tests/​llbc/​unops/​expected	Pins unary-operation LLBC.

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.