The foundation: ArithSpec

This is the founding document of the programme, and the earliest of the five deposits. It specifies integer arithmetic completely enough that any two machines produce the same result bit for bit — with round-to-nearest-even controlled by three guard bits, and explicit saturation.

Its algebraic properties have been explored by bounded exhaustive enumeration: five formal models (one in the paper, four in a note not yet published), two of which are deliberate counter-examples showing where the structure ceases to be associative. The dedicated page sets all of this out in detail.

Scope of the result