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.

翻译：即将发布的IEEE-P3109低精度浮点运算标准可能成为未来机器学习硬件与软件的基石。与IEEE-754的固定类型不同，P3109引入了一个由位宽、精度、符号性和定义域参数化的框架。这种灵活性产生了庞大的格式组合空间——部分格式的精度甚至低至1比特——同时引入了随机舍入和饱和运算等新特性。这些差异构成了一个独特的验证缺口，本文旨在解决这一问题。本文提出FLoPS（P3109标准的Lean形式化），即P3109在Lean中的完整形式化模型。我们的工作提供了一个经过机器检验的严格规范，有助于对该标准进行深入分析。我们通过验证基本性质及分析P3109框架下的关键算法，展示了该模型的实用性。具体而言，我们揭示了FastTwoSum算法在饱和模式下使用任意舍入方式时，均能精确计算“溢出误差”的新特性；而先前已建立的ExtractScalar算法性质在精度为1比特的格式中不再成立。本工作为P3109的推理提供了经过验证的基础，并能支持未来数值软件的形式化验证。我们的Lean开发代码已开源并公开可用。