掩码 Barrett 归约的机器校验势集基数界：后量子密码硬件中的 1 比特侧信道泄漏屏障

Barrett 归约是所有实用的基于 NTT 的后量子密码实现中的非线性核心。现有的组合框架（ISW、t-SNI、PINI、DOM）处理 GF(2) 上的布尔掩码；但没有一个能在素数域上的一阶算术掩码和一阶探测模型下对 Barrett 的泄漏提供机器校验的刻画。基于我们先前的系列工作——QANARY [15]、部分 NTT 掩码余量 [14]、代数基础 [16] 以及蝶形组合 [18]——我们填补了这一空白。我们证明了一个三分律：对于任意 $q > 0$ 和移位 $s$，Barrett 内部线映射 $f_x(m) = ((x + 2^s - m) \bmod 2^s) \bmod q$ 的原像基数属于 $\{0, 1, 2\}$，绝不会更多。我们将其称为 1 比特屏障：最大重数为 2 意味着每条内部线至多损失 1 比特最小熵，这在所有模数上普遍成立。计为零的情况（即不可达的输出值）表明实际泄漏通常严格小于 1 比特，使得该界是保守的。我们引入 PF-PINI（Prime-Field PINI）：Barrett 满足 PF-PINI(2)；Cooley-Tukey 蝶形满足 PF-PINI(1)。我们观察到（尚未证明），引入新鲜的级间掩码后，组合流水线的最大重数为 $\max(k_1, k_2)$，因此 1 比特屏障得以传播。该三分律、PF-PINI 实例化以及基数结果均在 Lean 4 中使用 Mathlib 进行了机器校验：12 个已证结果，零个 sorry，对所有 $q > 0$ 普遍成立（最小熵界由标准定义推出）。Adams Bridge 缺乏新鲜的级间掩码，违反了 PF-PINI 组合，这解释了为何论文 1 [15] 和论文 2 [14] 发现了漏洞。NIST IR 8547 建议使用形式化方法进行 PQC 实现验证。1 比特屏障为 ML-KEM (FIPS 203) 和 ML-DSA (FIPS 204) 中的掩码 Barrett 归约提供了首个普遍的机器校验基数界，并给出了相应的 1 比特泄漏解释。