This is Paper 6 of a series of formally-verified analyses of masked NTT hardware for post-quantum cryptography; Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Boolean masking composition is well-understood through NI, SNI, and PINI. Arithmetic masking over $\mathbb{Z}_q$ for prime $q$, the foundation of NTT-based post-quantum cryptography, has lacked an analogous theory. We prove, to our knowledge, the first machine-checked composition theorems for arithmetic masking over prime fields. Our key insight is the renewal argument: when a fresh random mask is applied between two pipeline stages, the intermediate wire becomes perfectly uniform regardless of Stage 1's security parameter. For two PF-PINI gadgets with parameters $k_1$ and $k_2$, the composed two-stage pipeline with fresh masking satisfies PF-PINI($k_2$), Stage 1's multiplicity is completely erased from the composed output. Without fresh masking, intermediate wires have multiplicity up to $k_1$, creating a necessary condition for differential power analysis. We formalize both theorems in Lean 4 with 18 machine-checked proofs and zero sorry stubs. We formally bridge the algebraic and hardware-faithful arithmetic models of Barrett reduction, and instantiate the theorems to formally diagnose Microsoft's Adams Bridge PQC accelerator: its absence of fresh inter-stage masking leaves Barrett output wires non-uniform under the first-order probing model, the same architectural flaw that two independent empirical analyses [3, 4] and our own prior structural analysis [1] identified. Computational evidence further suggests the 1-Bit Barrier is universal across Barrett and Montgomery reductions.

翻译：本文是后量子密码学中掩码NTT硬件系列形式化验证分析的第六篇论文；论文1[1]建立了QANARY平台的结构依赖性分析，论文2[2]量化了部分NTT掩码下的安全裕度。布尔掩码组合通过NI、SNI和PINI已得到充分理解。对于定义在质数$q$上的$\mathbb{Z}_q$算术掩码（即基于NTT的后量子密码学的基础），一直缺乏类似的理论。据我们所知，我们证明了首个针对质数域上算术掩码的机器验证组合定理。我们的核心洞察在于更新论证：当两个流水级之间施加一个新鲜随机掩码时，无论第1级的安全参数如何，中间导线都变得完全均匀。对于参数分别为$k_1$和$k_2$的两个PF-PINI部件，带新鲜掩码的两级流水线组合满足PF-PINI($k_2$)，第1级的重数在组合输出中被完全消除。无新鲜掩码时，中间导线的重数可达$k_1$，这构成差分功耗分析的必要条件。我们在Lean 4中完成了两个定理的形式化证明，包含18个机器验证的证明，零个sorry占位符。我们还形式化地建立了Barrett约减的代数模型与硬件保真算术模型之间的桥梁，并将这些定理实例化，以形式化诊断微软Adams Bridge PQC加速器：其缺乏级间新鲜掩码，导致Barrett输出导线在一阶探针模型下非均匀——这正是两个独立实证分析[3, 4]及我们前期结构分析[1]所发现的同一架构缺陷。计算证据进一步表明，1比特壁垒在Barrett约减和Montgomery约减中具有普适性。