模块分析：flocq

1. 角色定位

flocq/ 是用于浮点运算形式化验证的库，CompCert 使用其证明与定义来支撑浮点语义与优化正确性。

2. 结构概览

• Core/: 浮点基本定义与表示（格式、指数、舍入等）
• IEEE754/: IEEE 754 细节与属性
• Prop/: 各类误差/舍入性质证明
• Calc/: 运算与算法层（加法、乘法、除法、开方等）
• Version.v: 版本信息

3. 与 CompCert 的关系

• 为 Floats、Values 与 C 语义提供数学/证明基础
• 较少直接与驱动或后端相互调用，但作为证明依赖非常关键