Post-quantum cryptographic accelerators require side-channel resistance evidence for FIPS 140-3 certification. However, exact masking-verification tools scale only to gadgets of a few thousand cells. We present a four-stage verification hierarchy, D0/D1 structural dependency analysis, fresh-mask refinement, Boolean Single-Authentication Distance Checking (SADC), and arithmetic SADC, that extends sound first-order masking verification to production arithmetic modules. Applied to the 1.17-million-cell Adams Bridge ML-DSA/ML-KEM accelerator, structural analysis completes in seconds across all 30 masked submodules. A multi-cycle extension (MC-D1) reclassifies 12 modules from structurally clean to structurally flagged. On the 5,543-cell ML-KEM Barrett reduction module, the pipeline machine-verifies 198 of 363 structurally flagged wires (54.5%) as first-order secure, reports 165 as candidate insecure for designer triage (a sound upper bound), and leaves 0 indeterminate. Every verdict is cross validated by Z3 and CVC5 with 0 disagreements across 363 wires. The result narrows manual review from hundreds of structural flags to 165 actionable candidates with mathematical certificates, enabling pre-silicon side-channel evidence generation on production ML-KEM hardware.

翻译：后量子密码加速器需满足FIPS 140-3认证的侧信道抗性证据，但精确的掩码验证工具仅适用于数千门规模的小型组件。我们提出四阶段验证层次结构：D0/D1结构依赖性分析、新鲜掩码细化、布尔单认证距离检测（SADC）与算术SADC，将可靠的一阶掩码验证扩展至生产级算术模块。当应用于包含117万个单元的Adams Bridge ML-DSA/ML-KEM加速器时，结构分析可在数秒内完成全部30个有掩码子模块的处理。多周期扩展（MC-D1）将12个模块从结构清洁状态重新归类为结构标记状态。针对5,543个门规模的ML-KEM Barrett约减模块，该流水线可机器验证363根结构标记导线中的198根（54.5%）为一阶安全，将165根标记为候选不安全状态供设计人员排查（可靠的严格上界），且无任何未定结果。所有验证结论均通过Z3与CVC5交叉验证，363根导线判定零分歧。该成果将人工审核范围从数百个结构标记压缩至165个带数学证明的可操作候选对象，使生产级ML-KEM硬件能够生成硅前侧信道证据。