Formal verification of masking in post-quantum cryptographic (PQC) hardware relies on SMT solvers over finite domains. Our prior work established structural dependency analysis at scale [1] and quantified the security margin of partial NTT masking [2]. QANARY, our structural dependency analysis framework, verified 1.17 million cells across 30 modules of the Adams Bridge ML-DSA/ML-KEM accelerator [3, 4], but its core soundness result (Theorem 3.9.1) was machine-checked only at $q = 5$ via $2^{25}$ Boolean wire functions. This left portability to ML-KEM ($q = 3{,}329$, FIPS 203 [5]) and ML-DSA ($q = 8{,}380{,}417$, FIPS 204 [6]) as an open gap. NIST IR 8547 [7] (March 2025) motivates closing such gaps. We present the first machine-checked universal proof of the $r$-free sub-theorem of Theorem 3.9.1: for every $q > 0$, every wire function, and every pair of secrets, value-independence implies identical marginal distributions. The proof, in Lean 4 [8] with Mathlib [9], requires five lines versus $2^{25}$ finite evaluations. It is sorry-free, reducing the trusted base from {Z3 [10], CVC5 [11], Python} to the Lean 4 kernel. We provide nine theorems (T1--T6, T1', T3') covering reparametrization, bijectivity, overflow bounds, RNG bias, and a universal non-tightness counterexample for all $q \geq 2$. The results establish commutative ring axioms of $\mathbb{Z}/q\mathbb{Z}$ as the natural abstraction layer for arithmetic masking verification.

翻译：后量子密码硬件中掩码的形式化验证依赖于有限域上的SMT求解器。我们先前的工作建立了大规模结构依赖分析[1]，并量化了部分NTT掩码的安全边界[2]。我们的结构依赖分析框架QANARY验证了Adams Bridge ML-DSA/ML-KEM加速器[3,4]中30个模块的117万个单元，但其核心完备性结果（定理3.9.1）仅在q=5时通过2^25个布尔线函数进行机器检验。这导致其对ML-KEM（q=3329，FIPS 203[5]）和ML-DSA（q=8380417，FIPS 204[6]）的可移植性仍属未解难题。NIST IR 8547[7]（2025年3月）推动了此类问题的解决。我们提出了定理3.9.1中r-free子定理的首次机器检验通用证明：对所有q>0、所有线函数及所有秘密对，值独立性蕴含相同边际分布。该证明基于Lean 4[8]与Mathlib[9]，仅需五行代码而非2^25次有限评估。证明无缺项，将可信基从{Z3[10]、CVC5[11]、Python}缩减至Lean 4内核。我们提供九个定理（T1-T6、T1'、T3'），涵盖重参数化、双射性、溢出界、RNG偏差，以及对所有q≥2的非紧致通用反例。研究结果确立了Z/qZ的交换环公理作为算术掩码验证的自然抽象层。