Fix the semantics of the signed remainder: MIN % -1 overflows

[karthikbhargavan]

Summary

The scalar remainder models (Lean IScalar.rem, F*/Coq scalar_rem, and the
interpreter's concrete evaluation of Rem) treated iN::MIN % -1 as a success
returning 0, whereas the operation panics in Rust. The division models
already fail on iN::MIN / -1 (explicitly in Lean, via the range check in
F*/Coq and the interpreter), so remainder was inconsistent with division. The
remainder result 0 is representable, which is why the range checks that
catch the division overflow never trigger for the remainder. This PR makes the
signed remainder fail on x = MIN && y = -1, strengthens the associated spec
theorems (rem and checked_rem), and adds regression tests. Unsigned
remainder and the division-by-zero behavior are unchanged.

Rust semantics

• i32::MIN % -1 panics ("attempt to calculate the remainder with overflow")
  in both debug and release builds; remainder overflow, like division
  overflow, is not demoted to wrapping in release mode (RFC 560 / behavior
  of Rem on integers). rustc even rejects the constant form statically:

  $ cat main.rs
  fn main() {
      let x = std::hint::black_box(i32::MIN);
      let y = std::hint::black_box(-1);
      println!("{}", x % y);
  }
  $ rustc -O main.rs && ./main
  thread 'main' panicked at main.rs:4:20:
  attempt to calculate the remainder with overflow
  

  (With literal constants, rustc fails at compile time: error: this arithmetic operation will overflow: attempt to compute the remainder of `i32::MIN % -1_i32`, which would overflow.)

• The i32::checked_rem documentation: "Checked integer remainder. Computes
  self % rhs, returning None if rhs == 0 or the division results in
  overflow." So i32::MIN.checked_rem(-1) == None, while the Lean
  checked_rem spec theorems proved none ↔ y = 0.

• MIR encodes this: Rem with panic-on-overflow semantics fails when
  x = MIN && y = -1, exactly like Div.

Changes

• backends/lean/Aeneas/Std/Scalar/Ops/Rem.lean: IScalar.rem now fails with
  integerOverflow when x.val = IScalar.min ty && y.val = -1 (mirroring
  IScalar.div); IScalar.rem_bv_spec, IScalar.rem_spec and the per-type
  rem_bv_spec/rem_spec theorems take the corresponding hNoOverflow
  hypothesis (as the div specs already do); regression #assert vectors:
  MIN % -1 fails for i8..i128, MIN % 1 = 0, plain signed/unsigned cases
  and by-zero cases unchanged.
• backends/lean/Aeneas/Std/Scalar/CheckedOps/Rem.lean: the signed
  checked_rem specs now state
  none ↔ y = 0 ∨ (x = MIN ∧ y = -1) (same formulation as checked_div).
• backends/fstar/Primitives.fst: scalar_rem fails on x = scalar_min ty && y = -1; assert_norm checks for MIN % -1 and MIN % 1.
• backends/coq/Primitives.v: same check in scalar_rem. This also adds the
  previously missing division-by-zero check: in Coq Z.rem x 0 = x, so
  scalar_rem x 0 returned Ok x instead of failing.
• src/interp/InterpExpressions.ml: the concrete evaluation of Rem errors
  (panic) on MIN % -1; Div already errored via the mk_scalar range
  check.

Not touched:

• backends/hol4/primitivesScript.sml has the same gap (int_rem guarded
  only by y = 0); left as is since I could not run HOL4 locally to fix the
  dependent proofs.
• The F* int_rem also disagrees with Rust on the sign of the result for
  negative dividends when the division is inexact (e.g. int_rem (-7) 3
  evaluates to -2, Rust gives -1; the existing assert_norm checks only
  exercise |x| < |y|). That is a separate pre-existing issue, out of scope
  here.

Test evidence

• Lean: full lake build of the Aeneas library succeeds (1454 jobs),
  including the new #assert regression vectors (which are checked at
  elaboration time) and the reworked proofs.
• F*: fstar.exe Primitives.fst verifies the module, including the new
  assert_norm checks.
• OCaml: dune build of src (against the pinned Charon) succeeds.
• Coq: not verified locally (no Coq toolchain available); the change mirrors
  the guard style of scalar_div in the same file.

🤖 Generated with Claude Code

[abentkamp]

Looks good!

Only one small issue: I think we should try to separate Lean tests from the library, so that they don't slow down the regular build.

[abentkamp]

These tests should probably converted to Rust and go into tests/src

[abentkamp]

Oh, but the pull request should go into dev, not main!