[bug] t27o: int_ok(64, unsigned) overflows in bit(64), so usize / u64 / u128 parameters get no body-derived oracle samples #10864

What is wrong

int_ok(w, sg, m, neg) (specs/tools/t27o/rust_convert.t27) decides whether an integer type of w bits holds the sample m. For an unsigned type it asks m < bit(w), and bit(n) is 2^n computed by n doublings of a usize. For the 64-bit unsigned types (u64, usize, and u128, which int_type_width clamps to 64) that is bit(64) = 2^64, one doubling past what a usize holds.

• under t27b (and t27c test-report) the call traps: integer overflow (* on u64) at bit;
• in the compiled converter (tri t27o, release: wrapping) bit(64) is 0, so m < 0 is false for every sample.

Either way, a usize / u64 / u128 parameter gets none of the body-derived samples of #9102.

Repro (t27o of the branch of #10817)

pub fn f(x: u32) -> bool { x == 5 }
pub fn g(x: usize) -> bool { x == 5 }

tri t27o --oracle samples f with 0 1 2 7 10 100 4294967295 4 5 6, and g with 0 1 2 7 10 100 18446744073709551615 only: the 4, 5, 6 the body names are missing, so x == 5 is never reached from the oracle's side for the most common integer type of Rust.

The signed 64-bit types are fine (bit(63)), as are all narrower types.

Expected

g is sampled with 4, 5 and 6 too. Every sample num_value returns is below 2^62, so for w >= 63 an unsigned type holds all of them: int_ok can answer true for w >= 63 without computing bit(w).

Found by

Writing the direct tests of int_ok (lane C1 of #10522, issue #10825). A test cannot pin this one: the call traps under t27b and t27c, so int_ok is tested for widths 8, 16 and 32 and for the signed 64-bit type, and this issue holds the 64-bit unsigned case.

User Scenarios

• Given a Rust function with a usize parameter compared to a small constant (e.g., x == 5), When tri t27o --oracle generates samples, Then the oracle includes the body-derived samples 4, 5, 6 alongside the boundary samples.
• Given a Rust function with a u64 parameter compared to a small constant, When tri t27o --oracle generates samples, Then the oracle includes the body-derived samples 4, 5, 6 alongside the boundary samples.
• Given the int_ok predicate for width 64 and unsigned, When evaluating a sample m < 2^62, Then it returns true without computing bit(64).

Requirements

• FR-001: int_ok in specs/tools/t27o/rust_convert.t27 MUST return true for unsigned widths w >= 63 without evaluating bit(w).
• FR-002: int_ok MUST continue to compute bit(w) for unsigned widths w < 63 and for all signed widths.
• FR-003: The oracle for usize/u64/u128 parameters MUST include body-derived samples (e.g., 4, 5, 6 from x == 5) in addition to boundary samples.

Success Criteria

• tri t27o --oracle on a function fn g(x: usize) -> bool { x == 5 } produces samples including 4, 5, 6 (exit 0).
• tri t27o --oracle on a function fn h(x: u64) -> bool { x == 5 } produces samples including 4, 5, 6 (exit 0).
• tri t27c test specs/tools/t27o/rust_convert.t27 runs without integer overflow traps (exit 0).
• The direct tests of int_ok for width 64 unsigned pass (5 tests).

Boundary

• specs/tools/t27o/rust_convert.t27