FLoPS: Semantics, Operations, and Properties of P3109 Floating-Point Representations in Lean

TL;DR

FLoPS, Formalization in Lean of the P3109 Standard, which is a comprehensive formal model of P3109 in Lean that serves as a rigorous, machine-checked specification that facilitates deep analysis of the standard and enables formal verification of future numerical software.

Abstract

The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike the fixed types of IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats -- some with as little as one bit of precision -- alongside novel features such as stochastic rounding and saturation arithmetic. These deviations create a unique verification gap that this paper intends to address. This paper presents FLoPS, Formalization in Lean of the P3109 Standard, which is a comprehensive formal model of P3109 in Lean. Our work serves as a rigorous, machine-checked specification that facilitates deep analysis of the standard. We demonstrate the model's utility by verifying foundational properties and analyzing key algorithms within the P3109 context. Specifically, we reveal that FastTwoSum exhibits a novel property of computing exact "overflow error" under saturation using any rounding mode, whereas previously established properties of the ExtractScalar algorithm fail for formats with one bit of precision. This work provides a verified foundation for reasoning about P3109 and enables formal verification of future numerical software. Our Lean development is open source and publicly available.

Figures (7)

• Figure 1: The binary encoding of finite floating-point numbers. For a finite $x$, $t$ represents the $P-1$ trailing bits of $x$'s significand $m$. $B$ and $W$ each represent the exponent bias and bitwidth.
• Figure 2: The "Triangle of Correctness" illustrating the formal isomorphism between the bit-level representation, the algebraic model, and the semantic value set.
• Figure 3: The definition of emax for all $K$, $P$, $s$, and $d$.
• Figure 4: The definition of $n_{fmax}$, the encoding of the maximum finite value in a given format.
• Figure 5: (a) The bit-to-ADT decoding function. (b) The helper function for finite value encodings.

Theorems & Definitions (15)

• Lemma 1: $\Phi$ is injective
• Lemma 2: $\Phi$ is surjective
• Lemma 3: Reduction
• Theorem 4: Round-Trip Identity
• Lemma 5: Projection equals to rounding if already in range
• Lemma 6: Projection is "faithful"
• Definition 7: FastTwoSum
• Lemma 8: Exact Intermediate Step
• Lemma 9: Representable Error
• Theorem 10: Exact Error Computation