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引入了一个由位宽、精度、符号性及定义域共同定义的参数化框架。这种灵活性产生了巨大的格式组合空间——部分格式精度低至1比特——同时还引入了随机舍入与饱和算术等新颖特性。这些差异造成了独特的验证空白，而本文旨在填补这一空白。本文提出了FLoPS（Lean中P3109标准的形式化建模），即P3109在Lean中的全面形式化模型。我们的工作提供了一份严格且经机器校验的规范，便于对该标准进行深入分析。我们通过验证基础性质并剖析P3109语境下的关键算法，展示了该模型的实用性。具体而言，我们发现FastTwoSum算法展现出一种新颖特性：在饱和算术下，可使用任意舍入模式计算精确的"溢出误差"；而此前已确立的ExtractScalar算法性质，在精度为1比特的格式中出现失效。本工作为P3109的推理提供了经过验证的基础，并支持对未来数值软件的形式化验证。我们的Lean开发成果已开源，可供公开获取。