Make Solm integer semantics width-aware and overflow-explicit

[sbillig]

Summary

Fix integer casts, wrapping negation, binary arithmetic, and expression typing in Solm, and migrate the affected specifications and proofs.

Values remain represented by Lean’s unbounded Int, but integer operations now carry the width, signedness, and overflow policy needed to interpret them correctly. This avoids relying on storage writes or ABI encoding to repair an incorrect intermediate value.

Semantic fixes

1. Integer casts normalize to the target type

Integer-to-integer casts previously returned their input unchanged, so narrowing followed by widening could preserve bits that should have been discarded.

The shared normalizeInt function now:

• Reduces the value modulo 2^N.
• Returns that residue for unsigned types.
• Interprets it as two’s complement for signed types.

castValue?, integer storage-word interpretation, and legacy ABI cleaning share this implementation. For example, narrowing 511 to uint8 produces 255, even when subsequently widened.

Modern ABI decoding still rejects noncanonical words. ABI encoding and explicit range assertions remain validation operations, not truncating conversions.

2. Unary negation preserves the declared width

Unbounded negation produced an out-of-range positive result when negating a signed minimum.

UnaryOp.neg now carries an IntType; evaluation negates the mathematical value and normalizes the result at that type. Wrapping int8 negation therefore maps -128 back to -128.

The corresponding Cat proofs retain their permitted signed-minimum boundary rather than excluding it with a stronger hypothesis.

This operator models legacy/unchecked wrapping negation only. Modern checked-overflow negation is not implemented. Surface negation requires an explicitly typed operand, such as -int256(x).

3. Arithmetic has explicit checked and wrapping semantics

Arithmetic operators carry both IntType and IntArithMode. A shared evalIntArithResult either checks the mathematical result against the declared signed/unsigned range or normalizes it for wrapping arithmetic.

This applies to addition, subtraction, multiplication, division, and exponentiation. Overflow is handled at the operation itself, including narrow intermediate expressions—not deferred until assignment or encoding.

Surface binary arithmetic is checked by default. The elaborator supports lexical unchecked { ... } blocks and the specification-only unchecked(expr) form. It records the selected mode on generated operators; the mode does not propagate into called functions.

Ordinary % never selects wrapping behavior. The final implementation has no divisor-spelling heuristic. Explicit as T range assertions remain checked.

4. Signed division and remainder use truncation toward zero

Runtime division and remainder use Int.tdiv and Int.tmod, replacing Lean’s Euclidean division/remainder behavior.

For example, signed -5 / 2 evaluates to -2, and -5 % 2 evaluates to -1.

The signed-minimum divided by -1 case passes through the shared overflow handler: checked division reverts, while wrapping division returns the signed minimum. Division and remainder by zero revert regardless of overflow mode.

5. Bitwise operations and shifts respect width and signedness

Integer bitwise operations first interpret operands as unsigned bit patterns of the declared width, perform the operation, and reinterpret the result at the declared signedness. Integer complement follows the same width-bounded approach.

Left shifts truncate to the declared width. Right shifts normalize the operand first and preserve its sign for signed types: int8(-3) >> 1 produces -2. Oversized shifts produce zero, or -1 for a negative signed right shift. Negative shift amounts are rejected.

Fixed-bytes complement, bitwise operations, and shifts have separate AST constructors, preserving their behavior without conflating them with typed integers.

6. Literal expressions retain exact values during elaboration

Literal-only expressions are evaluated with exact rational precision before conversion into runtime integer expressions.

This permits intermediate values outside the destination width and preserves fractional intermediates:

• (255 + 1) - 1 folds to 255.
• (5 / 2) * 2 folds to 5.

Literal values also participate in type selection. A representable literal can use the other operand’s type; otherwise, its smallest representable integer type participates in promotion or rejection. For example, a uint32 operand plus 4294967296 selects uint40.

Genuinely typed narrow subexpressions retain their widths. Typed type(T).min/max expressions and conditional expressions are not incorrectly treated as arbitrary-precision literals. Opaque Lean escapes are not assumed to be Solidity constant expressions.

7. Shift and exponentiation typing follows the left operand

The result type of shifts and exponentiation comes from the left/base operand, not a common type formed with the right operand.

Thus a wide shift count does not widen a uint8 value, and a wide exponent does not remove uint8 multiplication overflow.

Literal bases with typed right operands use the appropriate full-word signed or unsigned type. The right operand is checked independently as unsigned and elaborated without imposing the left operand’s width on its subtree.

8. Typed bindings require valid values

Previously, local declarations and parameter binding could ignore their declared ABI types.

The recursive valueMatchesABIType checks integer ranges, fixed-byte widths, array lengths and elements, and tuple shapes. Parameter binding uses this check; successful typed local-declaration proofs now require corresponding validation evidence.

These checks do not silently truncate values. Invalid local bindings are excluded from valid execution derivations; this change does not introduce an EVM revert rule for malformed specifications.

Specification and proof migration

The migration adds reusable normalization, typed-arithmetic, and binding lemmas, and repairs consumers at their actual source invariants:

• Dai: model permit nonce increments as wrapped UInt256 values throughout evaluation and storage.
• Vat: use signed multiplication/division, truncating-division facts, signed range obligations, and explicit wrapping for word-valued updates.
• Clipper: retain the distinction between legacy wrapping arithmetic and SafeMath checks; supply typed-binding evidence and remove redundant wrapping-helper bounds.
• Uniswap V2: migrate the completed upstream consumers, deriving narrow reserve bounds from existing packed-storage invariants. Public correctness statements remain unchanged.
• Scaffolds: update affected literal expressions and operator annotations. The limited V3 unsigned observeSingle interpolation repair makes uint160 accumulator arithmetic, uint256 intermediate arithmetic, and narrowing explicit.

Limitations

Unary negation remains wrapping-only (no checked/unchecked behavior difference). The uniswap v3 scaffold still has known full-precision and source-width/signedness issues deferred to separate work.