Proofs

35 of 41 core ops proven for every input, 0 for every input but a stated window, 6 fuzzed. 0 counterexamples found and pinned. 5,933 s of solver time.

A test checks the inputs it was given. These checks cover every input: Halmos runs each op of the inline libraries with symbolic arguments, all 2²⁵⁶ or 2⁵¹² of them at once, and the solver shows that no input makes the op return a different word, or revert with a different error, from a reference specification written separately from the library code. The specifications are plain Solidity on exact integers, short enough to read: Ref127.sol, Ref19.sol. FP19's reference rounds to 237 bits from comparisons on the exact value, not from the library's normalisation.

Where the proofs found something, it is on this page: two FP127 ops leave their documented semantics on a narrow family of inputs, each pinned by a test that fails once it is fixed. The square roots are fuzzed against exact integer roots, not proved. Method, trust base and limits: docs/proofs.md.

FP127

FP19

Lemmas

The specifications reach exact integers through a few primitives built from the EVM's own opcodes; each is proved over unbounded integers with Z3 (4.12.6), and the op proofs keep multiplication and division uninterpreted, so they hold whatever the solver might assume about a 256-bit product.

• L1 proved: umul: (MULMOD(a,b,2^256-1) - MUL(a,b) - borrow, MUL(a,b)) = a b
• L2 proved: smul, signs (+, +): signed high word by the corrections
• L3 proved: MUL of two exponent fields is zero iff one is
• L4 proved: DIV(2^256 - u, u) + 1 = floor(2^256 / u)
• L5 proved: (x XOR SAR(255, x)) - SAR(255, x) = |x|
• L6 proved: ma mb in [2^472, 2^474) for significands
• L7 proved: floor(ma 2^255 / mb) >= 2^254
• K18 proved: q18: floor(m 2^60 / 5^18) by two word divisions, every intermediate a word
• K127 proved: divq(a, b) = floor(a 2^128 / b): S1-S6, B1-B3
• K19 proved: divh(a, b) = floor(a 2^255 / b): S1-S6, B1-B3
• R1 proved: isqrtw(z) = floor(sqrt z) for 2^128 <= z < 2^256
• R2 proved: FP127 sqrt(x) = floor(sqrt(x 2^128)) for 0 < x < 2^255

Status: proven, every input against the spec, its primitives proved; proven outside one window, every input but the stated family, where a pinned test shows the op leaving its documented result; fuzzed, no symbolic proof, the op is fuzzed against the exact spec; counterexample, fuzzed, with a pinned input where it leaves the spec. Solver time is Halmos's own on one machine, two solver threads per check; it varies run to run. Tools: Halmos 0.3.3 with CLZ added and commuted products (bitwuzla 0.8.1), forge 1.7.1, solc 0.8.38. Every check: make proofs PROOFS_FULL=1. Dataset: proofs.json.