Found during the #807 review (silent-failure-hunter pass on PR #811).
An integer literal outside the i64 range (e.g. 18446744073709551616 = 2^64) is accepted by vera check, and the verifier models it at its unbounded mathematical value, but codegen then hard-rejects it with an internal-looking WAT error rather than a clean Vera diagnostic:
i64.const 18446744073709551616
^ invalid i64 number: constant out of range
Repro:
public fn f(@Unit -> @Int)
requires(true) ensures(@Int.result == 0) effects(pure)
{ 18446744073709551616 }
Severity: low / not a soundness hole. Codegen rejects the literal, so no wrong value is ever executed — it is a hard compile failure, not a silent wrong answer. The verifier reasoning over the unbounded literal value is therefore never exploitable at runtime.
Pre-existing (not introduced by #811): the same gap exists on main for a plain { 18446744073709551616 } body, with or without any int_to_float/conversion involved — the checker has no i64 integer-literal range validation.
Fix: add an integer-literal range check in the checker (@Int within [i64.MIN, i64.MAX], @Nat within [0, u64.MAX]) emitting a clean E1xx diagnostic at check time, so the error names the problem and points at the literal instead of surfacing a raw WAT i64.const failure at codegen.
Related: the #392 smt.py soundness audit (the verifier↔runtime integer-domain consistency theme); #798 (i64/u64 arithmetic overflow trapping).
Found during the #807 review (silent-failure-hunter pass on PR #811).
An integer literal outside the i64 range (e.g.
18446744073709551616= 2^64) is accepted byvera check, and the verifier models it at its unbounded mathematical value, but codegen then hard-rejects it with an internal-looking WAT error rather than a clean Vera diagnostic:Repro:
Severity: low / not a soundness hole. Codegen rejects the literal, so no wrong value is ever executed — it is a hard compile failure, not a silent wrong answer. The verifier reasoning over the unbounded literal value is therefore never exploitable at runtime.
Pre-existing (not introduced by #811): the same gap exists on
mainfor a plain{ 18446744073709551616 }body, with or without anyint_to_float/conversion involved — the checker has no i64 integer-literal range validation.Fix: add an integer-literal range check in the checker (
@Intwithin [i64.MIN, i64.MAX],@Natwithin [0, u64.MAX]) emitting a clean E1xx diagnostic at check time, so the error names the problem and points at the literal instead of surfacing a raw WATi64.constfailure at codegen.Related: the #392
smt.pysoundness audit (the verifier↔runtime integer-domain consistency theme); #798 (i64/u64 arithmetic overflow trapping).