新鲜掩码使NTT流水线可组合：PQC硬件中算术掩码的机器验证证明

用于ML-KEM（FIPS 203）和ML-DSA（FIPS 204）的后量子密码（PQC）加速器依赖于在$\mathbb{Z}_q$上的流水线化数论变换（NTT）阶段。我们先前的工作建立了大规模的结构依赖分析[1]，并量化了部分NTT掩码的安全裕度[2]。对于存在r的情况，逐阶段算术掩码是否能保证流水线级的安全性，此前没有机器验证的答案：组合框架（ISW、t-SNI、PINI、DOM）仅针对$\mathrm{GF}(2)$上的布尔掩码形式化；没有证明助手工件处理$\mathbb{Z}_q$上的NTT蝶形运算。我们在Lean 4和Mathlib中展示了三个机器验证的结果，全部零sorry。首先，我们弥补了先前工作的一个明确局限性：在新鲜随机性下，值独立性意味着恒定的边际分布（通过代数互信息零代理）。其次，蝶形运算的每上下文均匀性：对于任何在$\mathbb{Z}/q\mathbb{Z}$（$q > 0$）上带有新鲜输出掩码的Cooley-Tukey蝶形运算，每个输出线恰好有一个掩码值产生每个输出，这是一个与秘密无关的均匀边际，对所有模数、旋转因子和输入普遍成立。第三，在ISW一阶探测模型下，具有新鲜每阶段掩码的k阶段NTT流水线在每个阶段都满足每上下文均匀性。我们记录了一个命名的警告：蝶形运算输出的逐点值独立性是错误的。Adams Bridge加速器（CHIPS Alliance Caliptra）不满足新鲜掩码假设，其掩码仅在INTT第0轮激活，这从架构上解释了其结构不安全性。工件：九个定理，1738次构建任务，零个sorry。非线性组件（Barrett）的组合将在后续手稿中讨论，证明Barrett满足PF-PINI(2)（一位障碍）[3]以及PF-PINI组件在新鲜掩码更新下的k阶段组合[4]。