The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike 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.

翻译：即将发布的IEEE-P3109低精度浮点运算标准将成为未来机器学习硬件与软件的基础。与IEEE-754不同，P3109引入了一个由位宽、精度、符号性和定义域共同决定的参数化框架。这种灵活性导致了巨大的格式组合空间——其中某些格式精度低至仅有一位比特——同时带来了随机舍入与饱和运算等全新特性。这些差异造成了本文旨在解决的特殊验证空白。本文提出FLoPS（Lean中对P3109标准的形式化建模），即在Lean中构建P3109的全面形式化模型。我们的工作提供了严格且经机器检验的规范，便于对标准进行深度分析。我们通过验证基础性质并分析P3109语境下的关键算法来展示该模型的实用性。具体而言，我们揭示了FastTwoSum算法在任意舍入模式下利用饱和运算计算精确"溢出误差"的新特性，而ExtractScalar算法先前建立的属性在精度仅一位比特的格式中失效。本工作为P3109的推理提供了经过验证的基础，并支持未来数值软件的形式化验证。我们的Lean开发代码已开源并公开发布。