Issue #1175: Prover: least = 0 - b in bounding_mixed_fits overflows when b is i64::MIN (wraps in release, panics in dev)

Open and answer this issue on GitHub.

ready · opened 2026-11-02 · updated 2026-11-02 · 0 comments

Found by R4 while fixing the red CI. With recursion_limit = 512 (a3d5af8e) the dev profile builds again. Three sysroot tests then panic with “attempt to subtract with overflow”:

• the_tools_lower_the_same_on_one_thread_as_on_every_core
• stds_nikaia_half_lowers_the_same_at_both_switches
• the_committed_rust_is_what_this_compiler_lowers

Where: lowered/bounds_walk.rs:614. It comes from least = 0 - b in bounding_mixed_fits (crates/nikaia-std/src/tools/bounds_walk.nika:977) when b is i64::MIN.

Why it matters: release builds, which CI runs, wrap instead of panicking. So CI stays green while the prover computes with a wrong, wrapped bound, which can make it prove something false.

To build

1. In bounds_walk.nika, handle b == i64::MIN explicitly: saturate, or treat the bound as unbounded.
2. Add a test in tests/compiler/ that reaches this bound.
3. Re-check that the checker should have refused the unguarded 0 - b. If it should have, also file that as a checker defect.

Back to Open Issues