Issue #553: A narrowing as is written only where it is shown to fit: NK1241, with checked_<T>() / truncating_<T>() (ADR-285 D12)

Open and answer this issue on GitHub.

language, compiler, ready · opened 2026-10-08 · updated 2026-10-10 · 0 comments

How it came up

While deciding f32 (#552), the owner set the rule for f64 as f32:

• the prover fails it early where it can;
• where nothing proves it safe, the program must handle it;
• there are named methods for Rust’s behaviour.

Asked whether integers keep their run-time abort, the owner answered that the same principle naturally holds for integers.

Decided (2026-10-08, 0.0.703)

ADR-285 D12, D13, Part I 2.2, Part III A.2 and C.3. A conversion that can lose a value is written as only where it is shown to fit. That covers a wider integer to a narrower one, signed to unsigned or back, and an f64 to an integer or to an f32.

• A constant that does not fit is NK1116 (as today, D29).
• A value the prover shows within the destination’s range converts, and the emitted conversion carries no check.
• Any other narrowing as is NK1241. The program writes one of two things:
  • checked_<T>(), a T? that is null where the value does not fit;
  • truncating_<T>(), or rounding_f32(), which is the backend’s conversion.
• checked_* now also converts out of an f64; NaN fits no integer.
• A conversion is no longer in A.2’s list of run-time stops. Arithmetic overflow (D5) is unchanged.

Today (develop, 0.0.702)

A narrowing as is emitted as try_from (or a std helper out of an f64) and aborts at run time where it does not fit. The corpus has 83 as to an integer type: 60 as i64, 12 as u64, 8 as u32 and 3 as i32. How many of them narrow, and how many the prover shows to fit, is what step 1 finds out.

To build (the order the owner set, 2026-10-08)

1. Build the check as a warning. A narrowing as that the prover does not show to fit is NK1241 at warning severity. Its help names checked_<T>() and truncating_<T>(), and rounding_f32() for f32. A proved one emits a plain conversion. Unproved ones keep today’s run-time check while the warning stands.

   Tests:

   • let small = big as i32 with big: i64 a parameter warns NK1241;
   • after assert(big >= 0 && big < 1000) the same line does not warn;
   • 5000000000 as i32 is NK1116;
   • k as u64 after if k >= 0 does not warn;
   • f as i32 with f: f64 warns.
2. Go through every warning the corpus and nikaia lower-std give. Each site is one of three cases:
   • The prover is too weak, and the site is safe. Rewrite the line with the name it means (checked_i32() ?? …, or an assert that proves it). Open an issue to strengthen the prover where that is possible, naming the site and the fact it missed.
   • The code had a defect. The value can really be out of range. Fix it: handle the null from checked_<T>(), or say truncating_<T>() where the low digits are meant. The output may change here, because that is the point of the fix. Say which outputs changed, and why, in the commit.
   • The low digits were meant. Write truncating_<T>().
3. checked_* out of an f64. Add std.contracts entries (by hand, D36) and their lowering. Tests: 1e20.checked_i32() is null; (0.0 / 0.0).checked_i64() is null; 3.7.checked_i32() is 3.
4. Turn the warning into the refusal once step 2 has no site left, and remove the run-time conversion check of D12’s old form. Test: the first test of step 1 is now an error.

f32’s half (checked_f32, rounding_f32, as f32) is #552. Build its as f32 step on this check.

Back to Open Issues