arXiv CSopen access

The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware Ray Iskander1, Khaled Kirah2,* 1

2

Verdict Security, [email protected] Faculty of Engineering, Ain Shams University, Cairo, Egypt

Abstract This is Paper 7 of a series of formally-verified analyses of masked NTT hardware for postquantum cryptography. Paper 1 [1] established structural dependency analysis of the QANARY platform, and Paper 2 [2] quantified security margins under partial NTT masking. Arbitrary-depth k-stage masked NTT pipelines with fresh inter-stage masking and per-stage PF-PINI(≤2) gadgets satisfy a per-observation cardinality bound of 2 ⋅ q2k−2 on the preimage of any output value, machine-checked in Lean 4 with zero sorry. Under the standard (informal) semantic translation that divides this cardinality by the total mask-tuple space size q2k−1 , the per-observation conditional probability bound is 2/q, independent of pipeline depth k. The QANARY program has previously established machine-checked cardinality bounds on the per-observation leakage of masked NTT hardware: PF-PINI(2) for Barrett reduction (Paper 5 [3]), 2-stage composition with fresh inter-stage masking (Paper 6 [4]), an underlying universality theorem (Paper 3 [5]), and PF-PINI(1) for butterfly wires (Paper 4 [6]). This paper closes the program with four contributions. First, a k-stage composition theorem generalizing Paper 6’s two-stage result to arbitrary k ≥ 1 gives the last-stagedetermined bound Gk−1 .maxMult ⋅ q2k−2 : only the last stage’s PF-PINI parameter survives, with intermediate parameters erased by fresh inter-stage masking. Second, Montgomery reduction satisfies PF-PINI(2) with tight max-multiplicity 2. Third, we assemble these into the end-to-end bound 2 ⋅ q2k−2 for any depth-k PF-PINI(≤2) pipeline under fresh inter-stage masking. Fourth, a Lean-verified hypothesis-violation conditional anchors the prior empirical and structural Adams Bridge analyses ([1, 2, 7, 8]).

Keywords: arithmetic masking, PF-PINI, k-stage composition, Montgomery reduction, formal verification, Lean 4, post-quantum cryptography, NTT hardware, side-channel analysis, probing security

1. Introduction The Number Theoretic Transform (NTT) is the computational backbone of the new NIST post-quantum standards ML-DSA (FIPS 204 [9]) and ML-KEM (FIPS 203 [10]). Hardware implementations of NTT-based cryptography must resist side-channel attacks, particularly differential power analysis (DPA), through arithmetic masking: splitting sensitive values into random shares that are processed independently in ℤq for the cryptosystem’s prime q. *Correspondence Author: [email protected] Ray Iskander: [email protected]

For Boolean masking over GF(2n ), the composition problem is solved. Ishai, Sahai, and Wagner [11] established the foundational probing security model. Barthe et al. [12] formalized Non-Interference (NI) and Strong Non-Interference (SNI), proving sequential composability of SNI gadgets. Cassiers and Standaert [13] introduced Probe Isolating NonInterference (PINI), achieving trivially composable gadgets, any PINI circuit built from PINI gadgets is automatically PINI. For arithmetic masking over ℤq for prime q, the picture is more recent. 1.1. The 1-Bit Barrier from Prior QANARY Papers The QANARY program has, in a sequence of papers, developed PF-PINI (Prime-Field Probe Isolating Non-Interference) as a quantitative single-wire leakage parameter for arithmeticmasked gadgets. Paper 5 proved that Barrett reduction, one of the two standard modular reductions used in NTT-PQC hardware, satisfies PF-PINI(2): the cardinality of the preimage of any output value under a uniform mask is at most 2. Semantically (informal, not mechanically formalized), this corresponds to a per-observation conditional probability bound Pr[output = v ∣ x] ≤ 2/q , at most 1 bit of conditional min-entropy loss per observation. Paper 6 proved the 2-stage composition theorem with fresh inter-stage masking: when a fresh random mask is inserted between two PF-PINI gadgets, the composed pipeline’s output cardinality is bounded by the last stage’s parameter alone, with the first stage’s parameter completely erased. What was missing, and what this paper provides, is the generalization to arbitrary pipeline depth, the analogous PF-PINI characterization of Montgomery reduction (the second standard modular reduction), and a single end-to-end cardinality bound that assembles the program’s results for use in downstream hardware certification. 1.2. Why Montgomery Matters NTT-PQC hardware uses two standard modular reductions: Barrett reduction (used in many ML-KEM implementations) and Montgomery reduction (used in many ML-DSA implementations and in some ML-KEM ones). Until this paper, the QANARY program’s quantitative-leakage results were Barrett-only, an incomplete picture for the field of NTTPQC accelerators. A Phase 0 reconnaissance (montgomery_recon.py in the artifact repository) verified by exhaustive sweep at ML-KEM parameters and stratified sampling at ML-DSA parameters that Montgomery reduction exhibits the same two-branch, max-multiplicity-2 structure as Barrett, with the wraparound shift constant 2s replaced by 2w−s (where w is the hardware register width). This reconnaissance gated the formal Lean development: the empirical structural match indicated that Paper 5’s Barrett proof transplants character-forcharacter to Montgomery with the substitution 2s ↦ 2w−s . 1.3. Contributions This paper makes four contributions, three core theorems and one anchoring lemma, all formalized in Lean 4 with zero sorry and zero non-standard axioms. 1. The k-stage composition theorem (Section 3) (pfpini_pipeline_composition_k_stages): for any k ≥ 1 and any sequence of PF-PINI gadgets G0 , … , Gk−1 , the cardinality of the preimage of the pipeline output under all mask tuples is bounded by Gk−1 .maxMult ⋅ q2k−2 . The bound depends only on the last stage; intermediate stages’ parameters are erased by fresh inter-stage masking.

2

2. Montgomery is PF-PINI(2) (Section 4) (montgomery_max_multiplicity_two and tightness companion montgomery_count_eq_two): Montgomery reduction satisfies the same two-branch max-multiplicity-2 structure as Barrett, with tightness verified at ML-KEM and MLDSA parameters. 3. The end-to-end multiplicity bound (Section 5) (qanary_kstage_output_multiplicity_bound): assembling Paper 4’s butterfly PFPINI(1) [6], Paper 5’s Barrett PF-PINI(2), this paper §4’s Montgomery PF-PINI(2), and §3’s k-stage composition theorem, we prove that any k-stage pipeline of PFPINI(≤2) gadgets with fresh inter-stage masking has output preimage bounded by 2 ⋅ q2k−2 , regardless of pipeline depth k. We also include a framing lemma: 4. Formal anchoring of the Adams Bridge discussion (Section 5.3 + Section 7) qanary_unmasked_stage_violates_hypothesis): a short Lean-verified conditional (≤5line proof: intro; have; omega) stating that a pipeline containing any stage with effective maxMult ≥ 3 , for example, an unmasked stage, does not satisfy the hypothesis of Theorem 5.1. The substantive content of this lemma is structural rather than deep: it lifts the prose-only Adams Bridge discussion of Papers 1–2 [1, 2], the empirical findings of Karabulut & Azarderakhsh [7], and the architectural review of Saarinen [8] into a Lean-verified conditional, strictly weaker than any insecurity claim about Adams Bridge. We list it explicitly as an anchoring lemma rather than a coequal theorem to acknowledge its triviality of proof and its strategic role in keeping the formal claim strictly weaker than any “Adams Bridge is insecure” assertion. The headline framing for the contribution against PINI is the following: PINI provides a perfect simulability guarantee for n -share encoded gadgets in higher-order probing models, when it applies, t-PINI says no leakage at all. PFPINI is the complementary tool for first-order arithmetic-masked gadgets like standard Barrett or Montgomery reduction, which inherently leak under a single arithmetic mask: it answers “how large is the cardinality of the output preimage under the mask?” with a number, which under first-order DPA semantically bounds the output probability by 2/q (informal interpretation, not mechanically formalized). Paper 7 proves the cardinality bound stays at 2 ⋅ q2k−2 across k stages of Barrett, Montgomery, and butterfly gadgets composed under fresh masking. Connection to certification standards. Per-observation cardinality and probability bounds are aligned with the trajectory of post-quantum hardware certification standards: NIST FIPS 140-3 [14] governs cryptographic module security validation, NIST IR 8547 [15] (initial public draft of the PQC transition timeline, November 2024) sets deployment expectations, and ISO/IEC 17825:2024 [16] informs side-channel testing protocols (TVLA-based). A precise quantitative per-observation bound of the kind this paper proves provides the cardinality-level evidence on which DPA-resistance arguments at the architecture level rest, complementing, rather than replacing, the gate-level evidence that tools like SILVER and maskVerif provide.

3

1.4. Paper Organization Section 2 reviews preliminaries: arithmetic masking, the PF-PINI definition, the pipeline model, and the prior PF-PINI results from the QANARY program. Section 3 proves the 𝑘stage composition theorem. Section 4 proves Montgomery PF-PINI(2) and tightness. Section 5 assembles the end-to-end multiplicity bound and its specializations, and proves the hypothesis-violation theorem. Section 6 places PF-PINI in the related-work landscape: probing security lineage, automated verification tools, proof-assistant formalizations, and prior empirical Adams Bridge analyses. Section 7 discusses Adams Bridge as a theoremapplicability case, with the convergence table of theoretical and empirical findings. Section 8 covers limitations and future work, including the cardinality-vs-probability semantic gap, the first-order scope, and the lack of a formal PF-PINI ↔ PINI translation. Section 9 concludes.

2. Preliminaries 2.1. Arithmetic Masking and the Probing Model Let q be an odd prime. (Throughout the paper, the cryptographic application context is an odd prime q, the standard moduli of NIST PQC, e.g., q = 3329 for ML-KEM and q = 8,380,417 for ML-DSA. The Lean theorems are stated more generally for any q with the type-class hypothesis NeZero q; primality is not required for any proof.) A value x ∈ ℤq is arithmetically masked by a uniformly random mask m ∈ ℤq as x̃ = x − m (mod q) . A masked gadget G over ℤq is a function G: ℤq × ℤq → ℤq taking a secret x and a mask m to an output G(x, m). We work in the first-order probing model: the adversary observes the value carried on a single internal wire, computed as G(x, m) for known x and uniform random m. The leakage of the gadget is captured by how strongly the marginal distribution of G(x, m) over m depends on the secret x. A first-order probing adversary that observes G(x, m) at a single wire learns at most H∞ (output) − H∞ (output ∣ x) bits of information per observation, so bounding the conditional max-probability Prm [G(x, m) = v ∣ x] from above immediately bounds the per-observation leakage. Higher-order probing, where the adversary correlates observations from multiple wires, is outside the scope of PF-PINI as defined here; see §8.2 for a discussion of this scope choice. 2.2. The PF-PINI Definition Following Paper 5 and Paper 6, we use the Prime-Field Probe Isolating Non-Interference (PFPINI) parameter as a quantitative single-wire bound. Definition 2.1 (PF-PINI Gadget). An PF-PINI gadget over ℤq is a triple (compute,maxMult,bound) where: • compute: ℤq × ℤq → ℤq is the gadget’s deterministic computation, • maxMult ∈ ℕ is the PF-PINI parameter, • bound is the proof obligation ∀ x, v ∈ ℤq , |{m ∈ ℤq :compute(x, m) = v}| ≤ maxMult. In the Lean 4 formalization, this is the PFPINIGadget structure (defined in QanaryPaper5/Basic.lean): structure PFPINIGadget (q : ℕ) [NeZero q] where compute : ZMod q → ZMod q → ZMod q maxMult : ℕ bound : ∀ x v, (univ.filter (fun m => compute x m = v)).card ≤ maxMult

4

Semantic interpretation (informal, not Lean-formalized). For any fixed secret x and any output value v , the conditional probability over a uniform mask m satisfies Prm [compute(x, m) = v ∣ x] ≤ maxMult/q. Equivalently, the conditional min-entropy is at least H∞ (output ∣ x) ≥ log 2 q − log 2 maxMult . For PF-PINI( maxMult = 2 ), the standard parameter for both Barrett (Paper 5) and Montgomery (this paper, Section 4), this gives Pr ≤ 2/q and H∞ ≥ log 2 q − 1 bits per observation. The probability and min-entropy claims are informal interpretations of the cardinality bound under the first-order uniform-mask model; the cardinality bound itself is what the Lean artifact establishes. 2.3. Pipeline Model A k-stage masked pipeline is a sequence of PF-PINI gadgets G0 , G1 , … , Gk−1 chained with a fresh inter-stage mask between each adjacent pair. The pipeline takes a secret x, k per-stage masks m0 , … , mk−1 , and k − 1 inter-stage fresh masks f0 , … , fk−2 , and computes: 𝑎0 = 𝐺0 (𝑥, 𝑚0 ) 𝑎0′ = 𝑎0 − 𝑓0 𝑎1 = 𝐺1 (𝑎0′ , 𝑚1 ) 𝑎1′ = 𝑎1 − 𝑓1 ⋮ ′ 𝑎𝑘−1 = 𝐺𝑘−1 (𝑎𝑘−2 , 𝑚𝑘−1 ). The pipeline’s output is 𝑎𝑘−1 . Total mask space size: |ℤ𝑞 |𝑘 ⋅ |ℤ𝑞 |𝑘−1 = 𝑞 2𝑘−1 . In Lean, the pipeline is defined recursively over 𝑘 as kPipelineOutput (QanaryPaper7/KStageComposition.lean): noncomputable def kPipelineOutput : (k : ℕ) → (Fin k → PFPINIGadget q) → ZMod q → (Fin k → ZMod q) → (Fin (k - 1) → ZMod q) → ZMod q | 0, _, x, _, _ => x | 1, stages, x, state_masks, _ => (stages 0).compute x (state_masks 0) | n + 2, stages, x, state_masks, fresh_masks => (stages (Fin.last (n + 1))).compute (kPipelineOutput (n + 1) ... - fresh_masks ⟨n, _⟩) (state_masks (Fin.last (n + 1))) We verify two specialization lemmas (sorry-free) so the recursive definition matches the expected concrete forms: • •

Lemma 2.2 (kPipelineOutput_one). At k = 1, the pipeline reduces to a single gadget application: kPipelineOutput(1, [G0 ], x, [m0 ], ∅) = G0 (x, m0 ). Lemma 2.3 (kPipelineOutput_two). At k = 2 , the pipeline matches Paper 6’s composedWithFresh exactly: kPipelineOutput(2, [G0 , G1 ], x, [m0 , m1 ], [f0 ]) = composedWithFresh(G0 , G1 , x, m0 , f0 , m1 ).

These lemmas establish that k-stage composition (Paper 7 Section 3) is a strict generalization of Paper 6’s 2-stage theorem with no behavioral mismatch at the overlap.

5

2.4. Known PF-PINI Results from the QANARY Program Paper 7 builds on three machine-checked PF-PINI results from earlier papers in the QANARY program: •

•

•

Identity / Butterfly (Paper 4 / Paper 5, identityPFPINI): the masked butterfly wire compute(𝑥, 𝑚) = 𝑥 − 𝑚 satisfies PF-PINI(1). Each output value is hit by exactly one mask, the gadget is bijective in 𝑚. (Mathematical result: Paper 4; PF-PINI Lean packaging as identityPFPINI: Paper 5’s QanaryPaper5/Basic.lean.) Barrett Reduction (Paper 5, barrettPFPINI s): the hardware-faithful Barrett internal map 𝑥−𝑚 if 𝑚.val ≤ 𝑥.val barrettInternalMap(𝑠, 𝑥, 𝑚) = { 𝑠 𝑥 − 𝑚 + 2 if 𝑚.val > 𝑥.val satisfies PF-PINI(2) for any modulus 𝑞 with NeZero 𝑞 and any shift parameter 𝑠 (the cryptographic application targets odd primes; the Lean theorem holds more generally). Here 𝑚.val, 𝑥.val ∈ ℕ are the canonical Nat representatives of 𝑚, 𝑥 ∈ ℤ𝑞 , and 2𝑠 denotes the image of 2𝑠 in ℤ𝑞 . The proof goes through the two-branch lemma: the map’s output equals one of two algebraic values, so its preimage is a subset of a twoelement set. 2-Stage Composition with Fresh Masking (Paper 6, pfpini_composition_with_fresh_mask): for any PF-PINI gadgets 𝐺1 and 𝐺2 , the composed two-stage pipeline with fresh inter-stage masking satisfies the cardinality bound |{(𝑚1 , 𝑓, 𝑚2 ) ∈ ℤ3𝑞 : 𝐺2 (𝐺1 (𝑥, 𝑚1 ) − 𝑓, 𝑚2 ) = 𝑣}| ≤ 𝐺2 .maxMult ⋅ 𝑞 2 . Critically, the bound depends only on 𝐺2 (the last stage); 𝐺1 ’s parameter is erased by the fresh inter-stage mask.

The renewal lemma fresh_mask_renewal (Paper 6) gives the structural reason: for any 𝐺1 and any target intermediate value 𝑤 , exactly 𝑞 pairs (𝑚1 , 𝑓) satisfy 𝐺1 (𝑥, 𝑚1 ) − 𝑓 = 𝑤 , the intermediate wire is perfectly uniform after the fresh mask. Paper 7’s k-stage theorem (§3) generalizes the 2-stage bound and the last-stage-only structure to arbitrary 𝑘 ≥ 1.

3. The k-Stage Composition Theorem This section presents Paper 7’s first contribution: a tight cardinality bound on the output of an arbitrary k-stage PF-PINI pipeline with fresh inter-stage masking. 3.1. Statement Theorem 3.1 (k-Stage Composition; pfpini_pipeline_composition_k_stages). Let k ≥ 1 and let G0 , G1 , … , Gk−1 be PF-PINI gadgets over ℤq (Lean theorem stated for any q with NeZero q; cryptographic application targets odd primes). For any secret x ∈ ℤq and any target output v ∈ ℤq , the cardinality of the set of mask tuples that produce v is bounded by: |{(m, f) ∈ ℤkq × ℤk−1 : kPipelineOutput(k, [G0 , … , Gk−1 ], x, m, f) = v}| q ≤ Gk−1 .maxMult ⋅ q2k−2 .

6

The bound depends only on the last stage’s parameter Gk−1 .maxMult (we call this the “laststage-determined” property; cf. Section 3.4). Intermediate gadgets’ parameters are completely erased by the fresh inter-stage masks. In Lean (QanaryPaper7/KStageComposition.lean): theorem pfpini_pipeline_composition_k_stages (k : ℕ) (hk : 1 ≤ k) (stages : Fin k → PFPINIGadget q) (x v : ZMod q) : (univ.filter (fun masks : (Fin k → ZMod q) × (Fin (k - 1) → ZMod q) => kPipelineOutput k stages x masks.1 masks.2 = v)).card ≤ (stages ⟨k - 1, by omega⟩).maxMult * (Fintype.card (ZMod q)) ^ (2 * k 2) The total mask space has size qk ⋅ qk−1 = q2k−1 ; the cardinality bound Gk−1 .maxMult ⋅ q2k−2 corresponds, under uniform masks (informal, not Lean-formalized), to the per-observation conditional probability bound Pr[output = v ∣ x] ≤ Gk−1 .maxMult/q , independent of the pipeline depth k. 3.2. Proof Sketch The proof proceeds by strong induction on 𝑘, with two cases. Base case (𝑘 = 1). The pipeline reduces to a single gadget application 𝐺0 (𝑥, 𝑚0 ) with no fresh masks (pfpini_pipeline_k1). The mask space (ℤ𝑞 )1 × (ℤ𝑞 )0 is in bijection with ℤ𝑞 via 𝑚 ↦ ((𝜆_, 𝑚),Fin.elim0) . Under this bijection, the filter set is {𝑚 ∈ ℤ𝑞 : 𝐺0 (𝑥, 𝑚) = 𝑣} , whose cardinality is bounded by 𝐺0 .maxMult via (stages 0).bound x v. The exponent 2𝑘 − 2 = 0 at 𝑘 = 1 gives 𝑞 0 = 1, so the target bound matches. Inductive case (𝑘 = 𝑛 + 2). We reassociate the state-mask space using Fin.snoc, peeling off the last state mask 𝑚𝑘−1 as the inner variable. Specifically, (ℤ𝑞 )𝑛+2 × (ℤ𝑞 )𝑛+1 is in bijection with ((ℤ𝑞 )𝑛+1 × (ℤ𝑞 )𝑛+1 ) × ℤ𝑞 via splitting state masks into (Fin.init 𝑚, 𝑚 (Fin.last)). Under this reassociation, the unfolding lemma kPipelineOutput_nPlus2_snoc shows: kPipelineOutput(𝑘,stages, 𝑥,Fin.snoc 𝑚′ 𝑚𝑘−1 , 𝑓) = 𝐺𝑘−1 .compute( prev′ (𝑚′ , 𝑓), 𝑚𝑘−1 ), where prev′ (𝑚′ , 𝑓) depends only on 𝑚′ and 𝑓, not on 𝑚𝑘−1 . For each fixed (𝑚′ , 𝑓), the fiber count over 𝑚𝑘−1 satisfying the predicate is bounded by 𝐺𝑘−1 .maxMult via (stages last).bound. Applying the standard combinatorial fiber-decomposition lemma card_filter_prod_le_mul: |{(𝑚′ , 𝑓, 𝑚𝑘−1 ):predicate}| ≤ |(ℤ𝑞 )𝑛+1 × (ℤ𝑞 )𝑛+1 | ⋅ 𝐺𝑘−1 .maxMult = 𝑞 2(𝑛+1) ⋅ 𝐺𝑘−1 .maxMult, which matches the target exponent 2𝑘 − 2 = 2(𝑛 + 1). ▫ The proof’s structure mirrors Paper 6’s 2-stage pfpini_composition_with_fresh_mask: peel the last stage’s mask off as the inner type, apply the per-stage PF-PINI bound on the fiber, and apply the fiber-decomposition lemma on the outer. The novelty in 𝑘-stage is the Fin.snoc reassociation that handles the variable-arity recursion uniformly. The proof is fully constructive in Lean 4 with zero sorry and zero non-standard axioms; the entire QanaryPaper7/KStageComposition.lean file (329 lines) builds in a fraction of the 1753-job total lake build.

7

3.3. Maximum-Over-Stages Corollary The headline bound is tight, it depends only on the last stage. For situations where it is more convenient to bound the cardinality by the maximum over all stages’ parameters (rather than the specific last-stage parameter), the symmetric corollary is immediate. Corollary 3.2 (Max-Over-Stages Bound; pfpini_pipeline_composition_k_stages_max_bound). Under the hypotheses of Theorem 3.1: |{(m, f):kPipelineOutput(… ) = v}| ≤ (

sup i∈{0,…,k−1}

Gi .maxMult) ⋅ q2k−2 .

Proof. From Theorem 3.1, |{… }| ≤ Gk−1 .maxMult ⋅ q2k−2 . Since Gk−1 .maxMult ≤ supi Gi .maxMult, the result follows by monotonicity of multiplication on the right. ▫ This corollary mirrors Paper 6’s pfpini_composition_max_bound and is a convenience wrapper, the tight last-stage-only bound is the headline result. 3.4. Discussion Last-stage-only is striking. A naive expectation might be that the leakage of a k-stage pipeline grows with k : more stages means more wires, more probing surface, and a multiplicative degradation of the bound. Theorem 3.1 says the opposite holds when fresh masking separates each pair of adjacent stages: the bound depends only on the last stage’s maxMult, not on the depth k or any intermediate stages’ parameters. Depth-independent semantic bound. For the special case where every stage satisfies Gi .maxMult ≤ 2, the case for both Barrett (Paper 5) and Montgomery (Paper 7, §4), Theorem 3.1 gives a cardinality bound of 2 ⋅ q2k−2 . Dividing by the total mask-space size q2k−1 , the per-observation conditional probability is bounded by 2/q (informal semantic interpretation; not Lean-formalized), regardless of pipeline depth k. Why this matters for hardware design. A designer building an NTT pipeline typically composes k = 4 or k = 8 Barrett (or Montgomery) reductions in series. Theorem 3.1’s cardinality bound, under uniform random masks, translates (informally, not Lean-formalized) into a per-observation conditional probability bound of 2/q on the final pipeline output whenever every stage is PF-PINI( ≤ 2 ) and fresh inter-stage masking is present. The composition theorem gives the designer a precise sufficient condition: PF-PINI(≤ 2) per stage, plus fresh inter-stage masks. The 2/q probability reading is depth-independent; the cardinality bound itself scales as q2k−2 because the mask-tuple space scales as q2k−1 .

4. Montgomery Reduction is PF-PINI(2) This section presents Paper 7’s second contribution: the formal proof that Montgomery reduction joins Barrett in the PF-PINI(2) class. Combined with Paper 5’s Barrett result, this establishes the 1-Bit Barrier across both standard modular reductions used in NTT-PQC hardware. 4.1. Hardware-Faithful Montgomery Map Montgomery reduction is parameterized by an odd prime q, a Montgomery radix R = 2s coprime to q, and the precomputed constant q′ = −q−1 mod R. For an input T in the range 0 ≤ T < q ⋅ R, the standard algorithm computes

8

Montgomery(T) = (T + ((T mod R) ⋅ q′ mod R) ⋅ q) / R = T ⋅ R−1 mod q. In a hardware implementation that operates in the Montgomery domain, the masked input is T = (x ⋅ R − m ⋅ R) mod 2w , where w ≥ ⌈log 2 (q ⋅ R)⌉ is the hardware register width and the subtraction wraps modulo 2w . (The Lean theorem montgomery_max_multiplicity_two is stated for any s, w ∈ ℕ; the cryptographic application context further requires the hardwarewidth inequality w ≥ ⌈log 2 (q ⋅ R)⌉ . In the degenerate Nat-saturated case w < s , the wraparound shift constant 2w−s collapses to 1 and the bound ≤ 2 holds trivially; this is consistent with but not the operative regime for the formal statement. This mirrors §2.1’s hedge for the modulus parameter q.) Reducing this masked Montgomery value yields one of two algebraic outcomes, depending on whether the wraparound triggered: • •

No wraparound (m.val ≤ x.val): the masked T stays in the range 0 ≤ T < q ⋅ R and Montgomery reduction returns x − m mod q. Wraparound (m.val > x.val): the masked T is 2w + (x − m) ⋅ R, and Montgomery reduction returns x − m + c mod q, where c = 2w−s mod q is the collision offset.

This is exactly the two-branch structure that Paper 5 identified for Barrett, with the wraparound shift constant 2s replaced by 2w−s . We capture this hardware-faithful (QanaryPaper7/MontgomeryPFPINI.lean):

behavior

in

the

Lean

definition

def montgomeryInternalMap (s w : ℕ) (x m : ZMod q) : ZMod q := if m.val ≤ x.val then x - m else x - m + ↑(2 ^ (w - s)) The shift constant 2w−s , distinct from Barrett’s 2s , is what makes Montgomery’s collision pattern numerically different from Barrett’s, even though their structural form is identical. 4.2. The Two-Branch Lemma The map’s structure immediately yields the two-branch characterization. Lemma 4.1 (Two-Branch; montgomeryInternalMap_eq_or). For any 𝑠, 𝑤 ∈ ℕ and 𝑥, 𝑚 ∈ ℤ𝑞 : montgomeryInternalMap(𝑠, 𝑤, 𝑥, 𝑚) = (𝑥 − 𝑚) ∨ montgomeryInternalMap(𝑠, 𝑤, 𝑥, 𝑚) = (𝑥 − 𝑚) + 2𝑤−𝑠 , where 2w−s denotes the image of 2w−s in ℤq . Proof. Direct case split on the conditional in the definition. ▫ From the two-branch lemma, the preimage characterization follows immediately. Lemma 4.2 (Preimage Subset; montgomeryInternalMap_preimage_subset). For any 𝑠, 𝑤 ∈ ℕ and 𝑥, 𝑣 ∈ ℤ𝑞 : {𝑚 ∈ ℤ𝑞 :montgomeryInternalMap(𝑠, 𝑤, 𝑥, 𝑚) = 𝑣} ⊆ {𝑥 − 𝑣, 𝑥 − 𝑣 + 2𝑤−𝑠 }. Proof. By Lemma 4.1, every m in the preimage satisfies one of the two algebraic equations. Solving each for m gives the two candidates. ▫ 4.3. The 1-Bit Barrier for Montgomery The preimage subset has cardinality at most 2, so the cardinality of the preimage is bounded by 2.

9

Theorem 4.3 (Montgomery Max-Multiplicity ≤ 2, The 1-Bit Barrier for Montgomery; montgomery_max_multiplicity_two). For any s, w ∈ ℕ, any q with NeZero q, and any x, v ∈ ℤq (the cryptographic application targets odd primes; the Lean theorem holds more generally): |{m ∈ ℤq :montgomeryInternalMap(s, w, x, m) = v}| ≤ 2. Proof. By Lemma 4.2, the preimage is a subset of a two-element set. The cardinality bound follows from monotonicity of Finset.card, with the two-element bound from card_insert_le. ▫ In Lean: theorem montgomery_max_multiplicity_two (s w : ℕ) (x v : ZMod q) : (univ.filter (fun m : ZMod q => montgomeryInternalMap s w x m = v)).card ≤ 2 := by calc (univ.filter (fun m => montgomeryInternalMap s w x m = v)).card ≤ ({x - v, x - v + ↑(2 ^ (w - s))} : Finset (ZMod q)).card := card_le_card (montgomeryInternalMap_preimage_subset s w x v) _ ≤ 2 := by have h := card_insert_le (x - v) ({x - v + ↑(2 ^ (w - s))} : Finset (ZMod q)) rw [card_singleton] at h; exact h We package the result as an PF-PINI gadget instance. Definition 4.4 (montgomeryPFPINI). For each s, w ∈ ℕ, the Montgomery reduction is an PFPINI gadget over ℤq with maxMult = 2: def montgomeryPFPINI (s w : ℕ) : PFPINIGadget q where compute := montgomeryInternalMap s w maxMult := 2 bound := montgomery_max_multiplicity_two s w This is the direct analogue of Paper 5’s barrettPFPINI s, with the two reductions occupying parallel positions in the PF-PINI(2) class. 4.4. Tightness Theorem 4.3 gives an upper bound of 2 on the preimage cardinality. To show the bound is tight (i.e., that some (x, v) pair achieves cardinality exactly 2, not just ≤ 2), we exhibit the two preimages and prove they are distinct. Lemma 4.5 (Direct-Branch Hit; montgomeryInternalMap_candidate_A). For any 𝑠, 𝑤 ∈ ℕ and 𝑥, 𝑣 ∈ ℤ𝑞 with (𝑥 − 𝑣).val ≤ 𝑥.val: montgomeryInternalMap(𝑠, 𝑤, 𝑥, 𝑥 − 𝑣) = 𝑣. Lemma 4.6 (Wraparound-Branch Hit; montgomeryInternalMap_candidate_B). For any 𝑠, 𝑤 ∈ ℕ and 𝑥, 𝑣 ∈ ℤ𝑞 with ¬ ((𝑥 − 𝑣 + 2𝑤−𝑠 ).val ≤ 𝑥.val): montgomeryInternalMap(𝑠, 𝑤, 𝑥, 𝑥 − 𝑣 + 2𝑤−𝑠 ) = 𝑣. 10

Theorem 4.7 (Tightness; montgomery_count_eq_two). Let s, w ∈ ℕ and let x, v ∈ ℤq satisfy: • • •

(x − v).val ≤ x.val (direct branch hits), ¬ ((x − v + 2w−s ).val ≤ x.val) (wraparound branch hits), 2w−s ≠ 0 in ℤq (branch offset nonzero, i.e., q ∤ 2w−s , which holds for any odd prime q > 1).

Then the preimage of v has cardinality exactly 2: |{m ∈ ℤq :montgomeryInternalMap(s, w, x, m) = v}| = 2. Proof. The two candidates x − v and x − v + 2w−s are distinct (since the offset is nonzero) and both lie in the preimage (Lemmas 4.5–4.6). The pair {x − v, x − v + 2w−s } is therefore a 2-element subset of the preimage, giving the lower bound |preimage| ≥ 2. Combined with the upper bound from Theorem 4.3, |preimage| = 2. ▫ Theorem 4.7 mirrors Paper 5’s barrett_count_eq_two character-for-character, with the substitution 2s ↦ 2w−s . The tightness result was added during the external Grok+Gemini audit pass (2026-04-20, Grok co-creative recommendation P2): symmetrizing Paper 7’s Montgomery result with Paper 5’s Barrett tightness establishes that the PF-PINI(2) parameter is not merely an upper bound but the exact max-multiplicity for standard parameter regimes. 4.5. Concrete Instances We instantiate montgomeryPFPINI s w at the parameters used by the two NIST PQC standards. ML-KEM (FIPS 203): 𝑞 = 3329 , 𝑠 = 16 , 𝑤 = 28 . The collision offset is 𝑐 = 212 mod 3329 = 767. Phase 0 reconnaissance verified the PF-PINI(2) bound by exhaustive sweep over all 𝑞 2 = 11,082,241 secret-mask pairs in ℤ23329 : maximum observed multiplicity is exactly 2, matching the Lean theorem. ML-DSA (FIPS 204): 𝑞 = 8,380,417 , 𝑠 = 23 , 𝑤 = 56 . The collision offset is 𝑐 = 233 mod 8,380,417 = 7167 . Phase 0 reconnaissance verified the bound on a stratified sample of 110 secrets across four strata (50 random + 20 near 0 + 20 near 𝑞/2 + 20 near 𝑞 − 1), with a full 𝑞-sweep over 𝑚 for each secret (≈ 9.2 × 108 (𝑥, 𝑚) pairs total; full sweep is > 7 × 1013 pairs, infeasible); analytical agreement with the Lean theorem (which is universal over 𝑞, 𝑠, 𝑤) provides the formal guarantee. Both ML-KEM and ML-DSA Montgomery reductions therefore satisfy PF-PINI(2), with maxMult exactly 2 (Theorem 4.7). The full Phase 0 reconnaissance is recorded in montgomery_recon_report.md and montgomery_recon_results.json in the artifact repository. Why Montgomery joining Barrett in PF-PINI(2) matters. Until this paper, the QANARY program’s quantitative-leakage results were Barrett-only. Montgomery reduction is the second standard modular reduction used in NTT hardware (and the dominant one in some implementations), so the previous Barrett-only coverage was incomplete for the field of NTT-PQC accelerators. With Theorem 4.3 in place, the framework’s coverage extends to both standard modular reductions used in NIST PQC hardware (Barrett and Montgomery); other reductions (e.g., Solinas, Plantard) remain future work, see Section 8.6.

11

5. The End-to-End Multiplicity Bound This section presents Paper 7’s third contribution: an end-to-end cardinality bound that assembles the QANARY program’s per-gadget PF-PINI results (Papers 4–5, plus Paper 7 §4) and the k-stage composition theorem (§3) into a single citable statement for an arbitrary masked NTT pipeline. The capstone is pure assembly, its proof is four lines in Lean. Its value is providing a single inequality that summarizes the program’s combined cardinality guarantees, so downstream hardware certification can cite one bound rather than several, and so the consistency of the dependent stack is verified at compile time. 5.1. The Capstone Theorem Theorem 5.1 (QANARY End-to-End Output Multiplicity Bound; qanary_kstage_output_multiplicity_bound). Let k ≥ 1 and let G0 , G1 , … , Gk−1 be PF-PINI gadgets over ℤq satisfying Gi .maxMult ≤ 2 for every i (Lean theorem stated for any q with NeZero q; cryptographic application targets odd primes). For any secret x ∈ ℤq and any output v ∈ ℤq : |{(m, f) ∈ ℤkq × ℤk−1 : kPipelineOutput(k, [G0 , … , Gk−1 ], x, m, f) = v}| ≤ 2 ⋅ q2k−2 . q Proof. By Theorem 3.1, the cardinality is bounded by Gk−1 .maxMult ⋅ q2k−2 . Since Gk−1 .maxMult ≤ 2 by hypothesis, the bound follows from monotonicity of multiplication on the right. ▫ In Lean (QanaryPaper7/ConfirmationTheorem.lean): theorem qanary_kstage_output_multiplicity_bound (k : ℕ) (hk : 1 ≤ k) (stages : Fin k → PFPINIGadget q) (h_bounded : ∀ i, (stages i).maxMult ≤ 2) (x v : ZMod q) : (univ.filter (fun masks : (Fin k → ZMod q) × (Fin (k - 1) → ZMod q) => kPipelineOutput k stages x masks.1 masks.2 = v)).card ≤ 2 * (Fintype.card (ZMod q)) ^ (2 * k - 2) := by calc (univ.filter _).card ≤ (stages ⟨k - 1, by omega⟩).maxMult * (Fintype.card (ZMod q)) ^ (2 * k - 2) := pfpini_pipeline_composition_k_stages k hk stages x v _ ≤ 2 * (Fintype.card (ZMod q)) ^ (2 * k - 2) := by apply Nat.mul_le_mul_right exact h_bounded _ Applicability of the hypothesis. The hypothesis ∀𝑖, 𝐺𝑖 .maxMult ≤ 2 is satisfied by any pipeline whose per-stage gadgets are drawn from the PF-PINI(≤2) class documented across the QANARY program: • • •

identityPFPINI (PF-PINI(1)): butterfly wires (Paper 4 / Paper 5). barrettPFPINI s (PF-PINI(2)): Barrett reduction (Paper 5). montgomeryPFPINI s w (PF-PINI(2)): Montgomery reduction (this paper, §4).

Any combination of these, Barrett-Barrett, Barrett-Montgomery, Montgomery-butterflyBarrett, etc., satisfies the hypothesis and falls under the capstone bound. 12

When the hypothesis does not hold. A pipeline containing any stage with maxMult > 2, for example, an unmasked stage, whose effective maxMult = 𝑞 in the single-mask model, does not satisfy the hypothesis, and the capstone’s 2 ⋅ 𝑞 2𝑘−2 cardinality bound is not applicable. See Section 5.3 for the formal statement of this hypothesis-violation condition, and §7 for a discussion of the Adams Bridge case where Papers 1–2 identify specific RTL stages outside the hypothesis. 5.2. Specializations The capstone admits two natural specializations. Theorem 5.2 (Butterfly-Only Pipeline; qanary_butterfly_only_multiplicity_bound). If every stage satisfies 𝐺𝑖 .maxMult ≤ 1, for example, every stage is a butterfly with fresh refresh (Paper 4), then: |{(𝑚, 𝑓):kPipelineOutput(… ) = 𝑣}| ≤ 1 ⋅ 𝑞 2𝑘−2 . Semantic interpretation (informal, not Lean-formalized): Pr[output = v ∣ x] ≤ 1/q, perfect output uniformity per observation, regardless of pipeline depth. Unsurprising in retrospect, but the formal statement records that PF-PINI’s quantitative parameter propagates faithfully: when all stages satisfy the PF-PINI(1) bound, the composed pipeline’s output preimage achieves the corresponding PF-PINI(1)-level cardinality bound. Theorem 5.3 (Modular-Reduction Pipeline; qanary_modular_reduction_pipeline_multiplicity_bound). If every stage is a modular reduction, Barrett or Montgomery, then Gi .maxMult ≤ 2 for all i, and the capstone bound 2 ⋅ q2k−2 applies. This is a readability alias for the capstone theorem; the Lean signature admits any PF-PINI gadget with maxMult ≤ 2, but the name emphasizes the intended use case (modular-reduction pipelines as in Adams Bridge), not a Lean-level restriction. 5.3. Hypothesis Violation The capstone’s hypothesis ∀𝑖, 𝐺𝑖 .maxMult ≤ 2 is required: a single stage with maxMult > 2, for example, an unmasked stage, invalidates the bound. We formalize this as a Lean theorem. Theorem 5.4 (Stage-of-Excess-Multiplicity Violates Hypothesis; qanary_unmasked_stage_violates_hypothesis).¹ Let G0 , … , Gk−1 be PF-PINI gadgets over ℤq , and suppose some stage Gi has Gi .maxMult ≥ 3. Then the hypothesis ∀j, Gj .maxMult ≤ 2 of Theorem 5.1 fails. ¹ The Lean theorem name encodes the motivating instance, an unmasked stage has effective maxMult = q ≥ 3 in the single-mask model, but the formal statement is fully general over any stage with maxMult ≥ 3. Proof. Direct contradiction: instantiating the universal hypothesis at j = i gives Gi .maxMult ≤ 2, contradicting Gi .maxMult ≥ 3. ▫ In Lean: theorem qanary_unmasked_stage_violates_hypothesis {k : ℕ} (stages : Fin k → PFPINIGadget q) (i : Fin k) (h_unmasked : (stages i).maxMult ≥ 3) : ¬ (∀ j, (stages j).maxMult ≤ 2) := by 13

intro h_all have := h_all i omega The theorem is structurally trivial, its content is the formal statement that an unmasked stage violates the capstone’s hypothesis, not a claim about the security or insecurity of any specific implementation. Its strategic value is anchoring the Adams Bridge discussion (Section 7) in a Lean-verified conditional: the empirical findings of Papers 1–2 (specific unmasked INTT stages) translate to “the capstone hypothesis fails at those stages,” a strictly weaker claim than “Adams Bridge is broken.” This theorem was added during the external Grok+Gemini audit pass (2026-04-20, Gemini co-creative recommendation P1) for exactly this anchoring purpose: it moves the Adams Bridge analysis from prose-only to a Lean-verified formal conditional. 5.4. Semantic Interpretation The capstone (Theorem 5.1) bounds the cardinality of the preimage of v over the mask-tuple space. Under the first-order probing model with uniform random masks, this cardinality bound corresponds (informally) to a per-observation conditional probability bound and a conditional min-entropy bound. Probability bound (informal, not Lean-formalized). The total mask-tuple space has size qk ⋅ qk−1 = q2k−1 . Dividing the cardinality bound 2 ⋅ q2k−2 by the total mask-space size gives: 2 ⋅ q2k−2 2 Pr [output = v ∣ x] ≤ = , 2k−1 masks q q regardless of pipeline depth k. Min-entropy bound (informal, not Lean-formalized). Equivalently, the conditional minentropy of the output given the secret satisfies: 2 H∞ (output ∣ x) ≥ −log 2 ( ) = log 2 q − 1 bits per observation. q For the two NIST PQC standards: • ML-KEM ( q = 3329 ): H∞ ≥ log 2 (3329) − 1 ≈ 11.70 − 1 = 10.70 bits per observation. • ML-DSA ( q = 8,380,417 ): H∞ ≥ log 2 (8,380,417) − 1 ≈ 21.999 bits per observation. These are the 1-Bit Barrier bounds of Paper 5, lifted from a single Barrett (or Montgomery, per Section 4) gadget to an arbitrary-depth pipeline of such gadgets composed under fresh masking. The cardinality bound is what the Lean artifact establishes; the probability and minentropy interpretations are semantic consequences of the cardinality theorem under the firstorder uniform-mask model and are not themselves stated or proved in Lean. See Section 8.1 for further discussion of this scope choice and Section 8.6 for future-work plans to mechanize the probability bound.

6. Related Work 6.1. Probing Security Lineage

The probing security model originates with Ishai, Sahai, and Wagner [11], who established that a circuit operating on n-share encoded values can be made secure against any t-probing adversary for t < n/2. Their construction provided a foundational target: composability of

14

the secure abstraction without an exponential blow-up in proof size. Barthe et al. [12] formalized two qualitative composability notions in this lineage: Non-Interference (NI) and Strong Non-Interference (SNI). An SNI gadget can be composed sequentially with another SNI gadget without the composition’s security order degrading; this is a qualitative preservation result. Cassiers and Standaert [13] introduced Probe Isolating Non-Interference (PINI) in IEEE Transactions on Information Forensics and Security, Volume 15 (2020), pages 2542–2555 (DOI 10.1109/TIFS.2020.2971153; preprint IACR ePrint 2018/438). PINI achieves a stronger composability property: any circuit constructed entirely from PINI gadgets is automatically PINI, with no per-composition proof obligation. The PINI composition theorems are the canonical reference for this qualitative composability result. These three notions, NI, SNI, PINI, are qualitative properties: a gadget either satisfies the property or does not. They were developed primarily for Boolean masking over GF(2n ) and address the question “can a t-probing adversary distinguish the masked circuit from the ideal one?” They do not provide a quantitative per-observation leakage measure. 6.2. PINI versus PF-PINI PF-PINI is fundamentally different from PINI in three respects: object of definition, quantity bounded, and target threat model. Object of definition. PINI is a property of n-share encoded gadgets: inputs and outputs are n-share tuples (x0 , … , xn−1 ) with x = x0 + ⋯ + xn−1 (mod q). The t-PINI property asserts that any set of t ≤ n − 1 probes is simulatable from at most t shares per input. PF-PINI is a property of single-secret single-mask gadgets: the input is an unmasked x ∈ ℤq and the mask m ∈ ℤq is a separate randomized quantity; the gadget computes a single-wire value G(x, m). Quantity bounded. PINI certifies probing-simulability: when the property holds at parameter t , the gadget achieves perfect zero-leakage simulation against any t -probing adversary on its n-share encoded form. PF-PINI bounds cardinality of the output preimage under the mask: the answer is a number (maxMult), with semantic interpretation (informal, not Lean-formalized) Pr[output = v ∣ x] ≤ maxMult/q under uniform masks. PF-PINI is therefore the appropriate tool for gadgets that inherently leak under a single arithmetic mask (e.g., standard Barrett or Montgomery reduction, where a perfect-simulability certificate at t = 1 does not exist on the underlying single-mask map); PINI remains the appropriate tool for higher-order n-share encoded gadgets that admit perfect simulability. Target threat model. PINI is designed for higher-order probing adversaries on n-share encoded circuits. PF-PINI is designed for first-order DPA on first-order masked hardware, the dominant deployed threat model in NIST PQC accelerators ([1, 2, 7, 8]). The quantitative gap. For the dominant deployed threat model, first-order DPA on firstorder masked NTT hardware, PINI’s qualitative simulability certificate does not directly yield a per-observation cardinality (or probability) bound; PF-PINI’s cardinality bound does. For higher-order n-share encoded gadgets, PF-PINI as defined here does not directly yield a t-probing simulability certificate; PINI does. On formal comparison. PF-PINI and PINI operate on different objects (single-mask (x, m) maps vs. n -share encoded gadgets) and measure different quantities (a per-observation preimage cardinality bound vs. a probing-simulation certificate). We do not claim a formal non-implication between the two notions; translating certificates of one into bounds of the other requires additional theorems beyond those we establish here. Different natural translation choices (e.g., treating PF-PINI’s mask m as PINI’s share x1 with x0 : = x − m; or treating PF-PINI’s (x, m) pair as an unshared plaintext input to a 2-share encoded PINI gadget) yield different induced objects, each requiring a separate translation theorem. Paper 15

7’s contribution is the quantitative preimage cardinality bound for first-order masked NTT hardware; a formal comparison between PF-PINI and PINI is left to future work. The two frameworks are best understood as complementary tools for complementary questions. 6.3. Automated Verification Tools maskVerif. Barthe, Belaïd, Dupressoir, Fouque, Grégoire, and Strub introduced maskVerif in Verified Proofs of Higher-Order Masking [17], with subsequent elaboration in later Bartheet-al. works (e.g., the ESORICS 2019 extension to physical defaults). maskVerif performs automated, gate-level verification of NI / t-SNI / PINI properties on circuits decomposed into individual boolean or arithmetic gates. Output is a SAT/SMT-certified proof that the property holds (or a counterexample). SILVER. Statistical Independence and Leakage Verification (SILVER) was introduced [18]. It is a BDD-based (Binary Decision Diagram) verifier that checks statistical independence properties at the gate level. It is distinct from EasyCrypt-style proof-assistant formalizations (see Section 6.4): SILVER is a tool, not a proof framework. Granularity comparison: gate-level vs gadget-level. Table 1 summarises the differences in object of verification, proof artifact, composition handling, reusability across moduli, output type, and typical case studies between the gate-level tools (maskVerif/SILVER) and the gadget-level PF-PINI framework. maskVerif / SILVER Axis (gate-level) PF-PINI (gadget-level) Object of verification Individual wires and gates Semantic gadget as a unit (Barrett, Montgomery, butterfly) Proof artifact SAT / BDD certificate per Lean theorem per gadget circuit instance type (Papers 5/6/7), universal over 𝑞 Composition Built into tool via External composition NI/SNI/PINI preservation theorem (Paper 6 for 𝑘 = 2, Paper 7 for 𝑘) Per-instance verification: the Proved once, applies to all 𝑞 Reusability across 𝑞 tools verify a specific circuit with NeZero 𝑞 (primality at a chosen (𝑞, 𝑠) not required for proof; cryptographic application targets odd primes) Output Yes/no certificate Quantitative maxMult , propagates to maxMultlast ⋅ 𝑞 2𝑘−2 Typical case study AES S-box, Keccak 𝜒, GIFT Barrett at 𝑞 = 3329 and 𝑞 = S-box, PRESENT 8,380,417 ; Montgomery at any odd prime Table 1. Granularity comparison between gate-level masking verifiers (maskVerif and SILVER) and gadget-level PF-PINI verification. The two approaches operate on different objects, produce different proof artifacts, and answer complementary questions; they are complementary rather than competing tools.

16

Feature, not limitation. PQC hardware IP blocks (Barrett, Montgomery, NTT butterfly) are designed and verified by their authors as functional units that are instantiated dozens of times across an NTT pipeline (e.g., Adams Bridge’s INTT instantiates Barrett at several pipeline stages per ML-KEM path). Gate-level re-verification at each instantiation duplicates proof work; gadget-level abstraction matches the natural modular boundaries of hardware design. PF-PINI’s gadget-level approach proves barrettPFPINI once at the Lean level (Paper 5, 12 theorems zero sorry) and applies the composition theorem to arbitrary pipelines (Paper 7 §3); changing q requires no re-verification (Paper 3’s universality theorem value_independence_implies_constant_marginal makes the gadget instance work for any odd prime). On scope. Published case studies appear to focus maskVerif and SILVER on symmetric primitives (S-boxes at 4-bit or 8-bit width; Keccak χ at 5-bit width) rather than modular reduction at NTT-PQC scale (q = 3329 requires 12-bit state; q = 8,380,417 requires 23-bit state). We are not aware of a published maskVerif or SILVER case study on Barrett or Montgomery at these widths; we note this as a scope difference, not a criticism of the tools. Complementarity. maskVerif / SILVER and PF-PINI are complementary, not competing. maskVerif / SILVER are the right tools for verifying novel cryptographic primitives at the gate level. PF-PINI is the right tool for composing verified modular reductions into arbitrarydepth pipelines with a quantitative per-observation bound. 6.4. Proof-Assistant Formalizations of Masking Machine-checked proofs of masking security have been developed primarily in EasyCrypt, providing high-assurance guarantees for Boolean masking constructions over GF(2𝑛 ). These formalizations cover NI, SNI, and specific masking schemes, but they operate exclusively over GF(2𝑛 ) rather than ℤ𝑞 for prime 𝑞. To our knowledge, no EasyCrypt formalization (or other proof-assistant formalization beyond the QANARY program) addresses arithmetic masking composition over ℤ𝑞 . The QANARY program (Papers 3–7) fills this gap in Lean 4: Paper 3 establishes a universality theorem applicable across moduli, Paper 4 covers butterfly composition, Paper 5 covers Barrett PF-PINI(2), Paper 6 covers 2-stage composition with fresh masking and the renewal lemma, and this paper covers 𝑘-stage composition, Montgomery PF-PINI(2), and the end-toend multiplicity bound. All Lean theorems carry zero sorry and zero non-standard axioms. 6.5. Arithmetic Masking Foundations Coron [19] developed Higher Order Masking of Look-Up Tables (EUROCRYPT 2014), a high-order masking countermeasure for block-cipher S-boxes based on randomized table recomputation, proved secure in the Ishai–Sahai–Wagner probing model. This and related works address the construction of masked gadgets, including conversions between Boolean and arithmetic representations when needed (classical references are Goubin [20], CHES 2001, for B→A conversion, and Coron–Tchulkine [21], CHES 2003, for A→B conversion), but do not provide composition theorems for arithmetic masking pipelines over ℤq for prime q. The QANARY program, and Paper 7 specifically, addresses the composition gap: given PF-PINI gadgets constructed by any means, how does the per-observation cardinality bound propagate through arbitrary-depth pipelines?

6.6. PQC Hardware and Empirical Side-Channel Attacks Adams Bridge is the open-source post-quantum accelerator developed under the Caliptra silicon root-of-trust program (CHIPS Alliance / Microsoft / industry consortium); its design is described by Bisheh-Niasar et al. [22]. The accelerator has shipped in two versions with materially different scope: the initial release (October 2024 [23]) integrated into Caliptra 2.0 supports ML-DSA-87 (FIPS 204 [9]) only; Adams Bridge 2.0 (integrated into Caliptra 2.1, 17

October 2025 [24]) adds ML-KEM 1024 (FIPS 203 [10]) alongside ML-DSA-87. Both schemes use first-order arithmetic masking in the Domain-Oriented Masking (DOM) [25] family. The empirical analyses [7, 8] target v1.0 (ML-DSA-only); the structural analyses [1, 2] inform both schemes as supported in v2.0. Karabulut, M. and Azarderakhsh [7] (Florida Atlantic University; distinct from Emre Karabulut in [22]) (IACR ePrint 2025/009; IEEE HOST 2025) reported the first published empirical CPA result on an industry-grade postquantum accelerator, targeting the initial Adams Bridge release (Caliptra 2.0) ML-DSA pipeline. Their published result demonstrates empirical behaviors consistent with pipeline configurations whose post-NTT modular-reduction stage falls outside the hypothesis of Theorem 5.1. This empirical observation is consistent with the wire-level multiplicity-2 phenomenon at the gadget level, and is the empirical evidence that motivated Paper 5’s formal PF-PINI(2) characterization of Barrett and, in this paper (§4), of Montgomery. Saarinen [8] (Hardwear.io USA 2025, invited talk, May 2025) reported, by RTL review and pre-silicon analysis of the initial Adams Bridge release (Caliptra 2.0), that the partial masking configuration applied on the ML-DSA signing path does not satisfy the sufficient conditions of Theorem 5.1 (specifically, that the key is not arithmetically share-split as required by the hypothesis ∀𝑖, 𝐺𝑖 .maxMult ≤ 2). Iskander and Kirah [1, 2] (arXiv:2604.15249, Paper 1 of the QANARY program; arXiv:2604.03813, Paper 2) identified, through structural dependency analysis and partial-NTT security-margin analysis, specific RTL stages in Adams Bridge whose configurations, recast here in the PF-PINI vocabulary of this paper, exhibit effective maxMult > 2 in the single-mask model, and identified the absence of fresh inter-stage masking between adjacent INTT stages as the specific architectural feature that prevents a depth-independent bound. Paper 6’s renewal lemma and 2-stage composition theorem are the formal counterpart of this finding. This paper provides the formal compositional explanation for why these findings are consistent: the Adams Bridge INTT pipeline configurations identified by [1, 2] do not satisfy the hypothesis ∀i, Gi .maxMult ≤ 2 of the capstone Theorem 5.1. Section 7 elaborates. 6.7. The Gap This Paper Fills Paper 4 [6] proves k-stage uniformity for butterfly-only pipelines (ntt_pipeline_composition, quantified over all q > 0 and k ≥ 0); Paper 6 [4] proves 2-stage PF-PINI composition for any gadget class. No prior work proves k-stage PF-PINI composition for arbitrary gadget classes, Theorem 3.1 is the first such bound, generalizing Paper 6’s result and complementing Paper 4’s butterfly-only k-stage uniformity. No prior work provides PF-PINI characterizations for both Barrett and Montgomery in a single program. Paper 5 covered Barrett and this one covers Montgomery and packages the unified result. No prior work assembles per-gadget PF-PINI results and pipeline composition into a single end-to-end machine-checked cardinality bound for masked NTT hardware, Theorem 5.1 of this paper is, to our knowledge, the first such bound.

7. Discussion: Adams Bridge as a Theorem-Applicability Case This section discusses the Adams Bridge PQC accelerator as a concrete application domain for the capstone theorem (Theorem 5.1) and the hypothesis-violation theorem (Theorem 5.4). The scope of this discussion is prose-level theorem applicability, not a formal claim about Adams Bridge. Adams Bridge does not appear in any Lean theorem statement in this paper; the only Lean theorem touching Adams Bridge concerns is Theorem 5.4, whose statement is “any pipeline with a stage of maxMult ≥ 3 violates the capstone hypothesis”, a pipelineagnostic conditional, not an Adams-Bridge-specific assertion. 18

7.1. Background Adams Bridge is the Caliptra-family open-source PQC accelerator [22]. The initial release (Caliptra 2.0, October 2024 [23]) supports ML-DSA-87 [9] only; Adams Bridge 2.0 (integrated into Caliptra 2.1, October 2025 [24]) supports both ML-DSA-87 and ML-KEM 1024 [10], with first-order DOM-family [25] arithmetic masking across a multi-stage Inverse NTT (INTT) pipeline. Different pipeline paths use Barrett reduction at 𝑞 = 3329 (ML-KEM) and Montgomery reduction at 𝑞 = 8,380,417 (ML-DSA), the two reductions this paper places jointly in PF-PINI(2). Three independent analyses of Adams Bridge have been reported across 2025 and 2026: •

•

•

Karabulut, M. and Azarderakhsh [7] (Florida Atlantic University; distinct from Emre Karabulut in [22]) reported a published empirical CPA result on the initial Adams Bridge release (Caliptra 2.0) ML-DSA pipeline within the trace budget reported in their paper, demonstrating empirical behaviors consistent with pipeline configurations whose post-NTT modular-reduction stage falls outside the hypothesis of Theorem 5.1. Saarinen [8] reported, by RTL review and pre-silicon analysis of the initial Adams Bridge release (Caliptra 2.0), that the partial masking configuration applied on the ML-DSA signing path does not satisfy the sufficient conditions of Theorem 5.1 (in particular, that the key is not arithmetically share-split as required by the hypothesis). Iskander and Kirah [1, 2] (Papers 1 and 2 of the QANARY program) identified specific RTL stages whose configurations, recast here in the PF-PINI vocabulary of this paper, exhibit effective maxMult > 2 in the single-mask model, including the absence of fresh inter-stage masking between adjacent INTT stages, and quantified the resulting depth-dependent security margins under partial NTT masking.

These empirical and structural findings motivated the formal program of Papers 3–7. This paper provides the formal compositional explanation for why these findings are consistent: in the language of Theorem 5.1, the absence of fresh inter-stage masking, combined with stages identified by [1, 2] as effectively unmasked, places those configurations outside the capstone’s hypothesis ∀i, Gi .maxMult ≤ 2. 7.2. What the Capstone Says About Adams Bridge Theorem 5.1 establishes a cardinality bound of 2 ⋅ q2k−2 for any k -stage masked NTT pipeline whose every stage satisfies PF-PINI(≤2) and that has fresh inter-stage masking. The bound applies to any combination of Barrett (Paper 5), Montgomery (this paper, §4), and butterfly-with-fresh-refresh (Paper 4) stages. Theorem 5.4 establishes the converse-direction conditional: if any stage has maxMult ≥ 3, for example, an unmasked stage, whose effective maxMult = q in the single-mask model, then the hypothesis of Theorem 5.1 fails at that stage, and the 2 ⋅ q2k−2 cardinality bound is not applicable to that pipeline. For Adams Bridge specifically, Papers [1, 2] identify particular RTL stages in the INTT pipeline whose configuration is consistent with the hypothesis-violation condition of Theorem 5.4. The formal statement that follows from this is precisely: “Adams Bridge’s INTT pipeline, in the configurations identified by [1, 2], does not satisfy the sufficient conditions of Theorem 5.1.” This is strictly weaker than “Adams Bridge is insecure”: an independent alternative framework outside the PF-PINI scope (for example, a fully gate-level analysis of the specific implementation under a stronger probing model) could in principle establish a separate security guarantee for those configurations through different reasoning. This paper does not 19

attempt such an alternative analysis and does not assert any security or insecurity claim for Adams Bridge beyond the formal conditional statement above. 7.3. Theoretical ↔ Empirical Convergence Table 2 summarises how the formal results of this paper relate to the prior empirical and structural findings on Adams Bridge.

Source Karabulut, M. & Azarderakhsh, ePrint 2025/009 [7] (FAU; distinct from Emre Karabulut in [22])

Saarinen, Hardwear.io 2025 [8]

Method Empirical CPA on the initial Adams Bridge release (Caliptra 2.0) MLDSA pipeline

Finding Empirical behaviors consistent with pipeline configurations whose post-NTT modular-reduction stage falls outside Theorem 5.1’s hypothesis

RTL review + preUSA silicon analysis on the initial Adams Bridge release (Caliptra 2.0)

Reports that the partial masking configuration applied on the MLDSA signing path does not satisfy the sufficient conditions of Theorem 5.1 Specific RTL stages consistent with effective maxMult > 2 across multiple modules Depth-dependent security margin quantification under partial masking

Iskander & Kirah, Structural arXiv:2604.15249 dependency analysis (Paper 1) [1]

Iskander & Kirah, Partial-NTT security arXiv:2604.03813 margin analysis; (Paper 2) [2] identifies absence of fresh inter-stage masking This paper (Paper Lean 4 formal 7), Theorem 5.4 verification (qanary_unmasked_s tage_violates_hypot hesis) This paper (Paper Lean 4 formal 7), Theorem 5.1 verification (qanary_kstage_outp ut_multiplicity_boun d)

If ∃𝑖, 𝐺𝑖 .maxMult ≥ 3, then the capstone hypothesis fails at stage 𝑖

∀𝑘, ∀ PF-PINI(≤2) stages with fresh inter-stage masking: cardinality bound 2 ⋅ 𝑞 2𝑘−2

20

Relationship to Theorem 5.1’s hypothesis Consistent with the wire-level multiplicity-2 phenomenon at the gadget level; motivates Paper 5’s barrettPFPINI and this paper’s montgomeryPFPINI Identifies an architectural pattern that places configurations outside the capstone’s hypothesis Maps which specific RTL stages fall outside the hypothesis Quantifies what the capstone forfeits when one or more stages violate the hypothesis Formal conditional anchoring of the empirical findings, strictly weaker than any “Adams Bridge is insecure” assertion Provides the formal target a remediated configuration must satisfy

Table 2. Convergence between Paper 7’s formal capstone results and the prior empirical and structural findings on Adams Bridge. Each row maps a published source (or this paper) to its method, finding, and how it relates to the hypothesis of Theorem 5.1. The convergence across three independent methodologies (empirical CPA, architectural review, structural dependency analysis) and the formal anchoring via Theorem 5.4 establishes the chain from empirical attack to architectural cause to formal hypothesis-violation condition. 7.4. Prescriptive Remediation Theorem 5.1’s hypothesis ∀i, Gi .maxMult ≤ 2 is constructive: any specific pipeline configuration that satisfies it falls under the cardinality bound, and any configuration that violates it (per Theorem 5.4) can be brought back within the hypothesis by replacing the violating stages. The remediation is direct: 1. Identify stages with effective maxMult > 2, for Adams Bridge’s case, the unmasked INTT stages identified by [1, 2]. 2. Replace each such stage with an PF-PINI(≤2) gadget. The QANARY program provides three such gadgets: o identityPFPINI (PF-PINI(1)), butterfly with fresh refresh (mathematical result: Paper 4; PF-PINI Lean packaging: Paper 5), o barrettPFPINI s (PF-PINI(2)), Barrett reduction (Paper 5), o montgomeryPFPINI s w (PF-PINI(2)), Montgomery reduction (this paper, §4). 3. Insert k − 1 fresh inter-stage masks between every adjacent pair of stages (Paper 6’s renewal-lemma requirement). We acknowledge that supplying k − 1 fresh ℤq masks per pipeline evaluation imposes a non-trivial random-number generation throughput requirement on the surrounding silicon: this PRNG cost is the architectural price paid to obtain a depth-independent leakage bound, and budgeting for it is a hardwaredesign decision orthogonal to the formal theorem. After remediation, the configuration satisfies the hypothesis of Theorem 5.1, and the cardinality bound 2 ⋅ q2k−2 applies to the pipeline output, regardless of pipeline depth. This prescriptive output is the qualitative difference between Theorem 5.1 / 5.4 and a yes/no security certificate that omits actionable diagnostic information: the framework tells the designer not merely whether their configuration is in or out of scope, but precisely what to change to bring it back in scope. 7.5. Framing Discipline We restate the framing discipline that governs this section, since the Adams Bridge discussion is the most sensitive part of this paper. The formal statement is: “Adams Bridge’s INTT pipeline, in the configurations identified by [1, 2], does not satisfy the sufficient conditions of Theorem 5.1.” The formal statement is not: “Adams Bridge is broken,” “Adams Bridge is insecure,” or “Adams Bridge is vulnerable.” The distinction matters for three reasons. First, an alternative independent framework outside the PF-PINI scope could in principle establish a separate security guarantee for the same configurations through different reasoning that we do not attempt here. Second, Theorem 5.1 provides a sufficient condition for the cardinality bound 2 ⋅ q2k−2 ; failure to satisfy a sufficient condition does not establish that the conclusion is false (only that this theorem’s proof of the conclusion does not apply). 21

Third, “Adams Bridge is broken” would be a claim about the implementation as a whole; the formal hypothesis-violation statement is local to specific stages identified in the cited papers, and the remediation in §7.4 is a local intervention. We adopt this discipline throughout the paper.

8. Discussion, Limitations, and Future Work 8.1. Cardinality vs Probability: The Semantic Gap The Lean artifact accompanying this paper proves cardinality bounds on the preimage of pipeline outputs over the mask-tuple space. The probability and min-entropy interpretations of the cardinality bound (cf. §5.4) are informal semantic consequences under the first-order uniform-mask model; they are not themselves stated or proved in Lean. The translation from cardinality to probability is straightforward: under uniform random masks, Pr[output = v ∣ x] = |preimage(v)|/|total mask space| , and our cardinality bound gives the numerator while the structure of the mask space gives the denominator. However, mechanizing this translation requires (a) introducing a probability monad or measuretheoretic framework into the Lean development, (b) defining the uniform distribution over the mask-tuple space, and (c) proving the relationship between cardinality bounds and probability bounds. We adopt the cardinality-only formalization for two reasons: first, it keeps the proof obligations sharp and verifiable without dependency on a probability framework; second, a cardinality bound is what mechanically certifies the architectural property, the probability interpretation is the engineering consequence that hardware designers care about, and it is unambiguous from the cardinality. The semantic gap is a known limitation, and mechanizing the probability/min-entropy bounds in Lean is left as future work. 8.2. First-Order Probing Model and Physical Defaults PF-PINI is defined for a first-order probing adversary: the adversary observes the value carried on a single internal wire. Our maxMult parameter quantifies the leakage of one wire under one observation per secret. Higher-order probing, where the adversary correlates observations from t ≥ 2 wires simultaneously, is outside the scope of PF-PINI as defined here. A separate scope boundary concerns physical defaults. Our formalization works at the algebraic ℤq level and abstracts away time and signal transitions. In physical hardware, glitches and transition leakage on fresh-mask insertion paths can cause leakage that the classical probing model does not see; this is the regime addressed by the robust probing model of Faust et al. [26] (TCHES 2018) and by tools such as maskVerif’s physical-defaults extension and SILVER’s gate-level model. Because PF-PINI operates over ℤq algebra rather than over a netlist with timing, glitch- and transition-induced leakage from physical defaults is outside our formal scope. Designers using PF-PINI as the architecture-level bound should compose it with a gate-level analysis (e.g., maskVerif/SILVER) for the physical-defaults regime. This scope choice mirrors Paper 6’s §8 scope statement and reflects the dominant deployed threat model in NIST PQC accelerators: most published side-channel attacks against PQC hardware ([7, 8]) are first-order DPA attacks at the algebraic level, and the PF-PINI(2) bound directly addresses the attack class that has been empirically demonstrated. Two natural extensions are left as future work. (i) Generalize PF-PINI from |{m: G(x, m) = v}| to a bound on |{(m1 , … , mn ): (Gw1 (x, m∗ ), … , Gwt (x, m∗ )) = (v1 , … , vt )}| for t probed 22

wires (higher-order extension). (ii) Integrate with the robust probing model so that the cardinality bound carries through to glitch-extended adversaries (physical-defaults extension). 8.3. Single-Mask Single-Secret Model PF-PINI is a property of single-secret single-mask gadgets: the input is an unmasked x ∈ ℤq and the mask m ∈ ℤq is a separate randomized quantity. This contrasts with PINI’s n-share encoded gadget model, in which inputs and outputs are n-share tuples. Comparing PF-PINI’s bounds with PINI’s certificates therefore requires a translation theorem between the two computational models. Different natural translations (e.g., treating PFPINI’s mask m as PINI’s share x1 with x0 : = x − m; or treating PF-PINI’s (x, m) pair as an unshared plaintext input to a PINI gadget) yield different induced objects, each requiring a separate translation theorem (cf. PFPINI_vs_PINI_differentiation.md §5 for full discussion). Paper 7 does not provide such a translation. We do not claim a formal non-implication between PF-PINI and PINI; we argue only that they are complementary tools for complementary questions (§6.2). 8.4. No Formal PF-PINI ↔ PINI Translation Following from §8.3, a fully formal equivalence or non-equivalence proof between PF-PINI and PINI, across natural framework-translation choices, is out of scope for this paper and left to future work. The argument we provide in §6.2 is informal but rigorous: PF-PINI and PINI operate on different objects and measure different quantities, so neither’s definitional machinery directly yields the other’s bound without an additional translation theorem. A future work artifact establishing such a translation theorem (in either direction) would tighten the relationship between the two frameworks and clarify when one can be used as evidence for the other. 8.5. Pipeline Model Scope The pipeline model kPipelineOutput defined in §2.3 captures linear pipelines: a sequence of PF-PINI gadgets 𝐺0 , 𝐺1 , … , 𝐺𝑘−1 chained with fresh inter-stage masks. Architectures with branching (where one stage’s output feeds multiple downstream stages), feedback (where a downstream stage’s output is fed back to an upstream stage), or non-trivial control flow are not modeled by kPipelineOutput and are not directly covered by Theorem 3.1 or Theorem 5.1. For the dominant case of NTT-based PQC hardware, the linear-pipeline model captures the inner-loop structure: an NTT or INTT proceeds through a sequence of butterfly + reduction stages, each consuming the previous stage’s output. Outer-loop control flow (e.g., the radix-2 vs radix-4 schedule) does not affect the linear-pipeline structure of the inner loop. Extending the framework to branching and feedback architectures, for example, to capture pipelines with shared intermediate buffers or with output-to-input feedback for streaming computation, is left as future work. 8.6. Future Work Summary We summarize the open problems identified above: 1. Mechanize the probability bound. Introduce a probability monad / measuretheoretic framework into Lean and mechanize the cardinality-to-probability translation, so the per-observation probability bound Pr ≤ 2/𝑞 is itself a Lean theorem rather than an informal semantic consequence.

23

2. Higher-order generalization. Extend PF-PINI from single-wire single-observation to 𝑡 -wire 𝑡 -observation bounds, enabling direct comparison with 𝑡 -PINI / 𝑡 -SNI for multi-probe adversaries. 3. PF-PINI ↔ PINI translation. Provide a formal translation theorem (in one or both directions) between PF-PINI’s single-mask cardinality bound and PINI’s 𝑛 -share simulability certificate. 4. Branching and feedback pipelines. Extend kPipelineOutput and Theorem 3.1 to architectures with non-linear pipeline topology. 5. Beyond Barrett and Montgomery. Apply the PF-PINI(2) characterization technique to other modular reductions (e.g., Solinas reduction, special-prime reductions used in CRYSTALS-Dilithium variants), the Phase 0 reconnaissance pattern of montgomery_recon.py provides a template. 6. Formal masking-tool integration. Combine PF-PINI’s gadget-level proofs with maskVerif’s or SILVER’s gate-level verification, so a hybrid proof can certify both the gadget abstraction (Lean) and its gate-level realization (maskVerif / SILVER) in a single artifact.

Conclusion This paper has presented four contributions, three core theorems and one anchoring lemma, to the formal compositional analysis of arithmetic masking for masked NTT post-quantum hardware. First, Theorem 3.1 (pfpini_pipeline_composition_k_stages) generalizes Paper 6’s 2-stage composition theorem to arbitrary 𝑘 ≥ 1 stages, with the tight last-stage-only cardinality bound 𝐺𝑘−1 .maxMult ⋅ 𝑞 2𝑘−2 . The bound depends only on the last stage; intermediate stages’ parameters are erased by fresh inter-stage masking. Second, Theorem 4.3 (montgomery_max_multiplicity_two) and its tightness companion Theorem 4.7 (montgomery_count_eq_two) prove that Montgomery reduction satisfies PFPINI(2), with max-multiplicity exactly 2 for standard parameters. Combined with Paper 5’s Barrett result, this establishes the 1-Bit Barrier across both standard modular reductions used in NTT-PQC hardware. Third, Theorem 5.1 (qanary_kstage_output_multiplicity_bound) assembles the per-gadget PF-PINI results (Papers 4, 5, plus this paper §4) and the 𝑘-stage composition theorem into a single end-to-end cardinality bound: any 𝑘-stage pipeline of PF-PINI(≤2) gadgets with fresh inter-stage masking has output preimage bounded by 2 ⋅ 𝑞 2𝑘−2 , regardless of 𝑘. Fourth, Theorem 5.4 (qanary_unmasked_stage_violates_hypothesis) formally anchors the Adams Bridge discussion in §7: the empirical findings of Papers 1, 2, and the prior work of Karabulut & Azarderakhsh and Saarinen translate into the formal conditional that specific RTL stages identified by structural analysis fall outside the hypothesis of Theorem 5.1. This formal conditional is strictly weaker than any “Adams Bridge is broken” assertion and is paired with a prescriptive remediation (§7.4) that brings configurations back within the hypothesis. All Lean 4 theorems carry zero sorry and zero non-standard axioms. The artifact comprises 20 declarations across three theorem modules (QanaryPaper7/KStageComposition.lean, QanaryPaper7/MontgomeryPFPINI.lean, QanaryPaper7/ConfirmationTheorem.lean) plus QanaryPaper7/Basic.lean (shared imports and sibling-dependency sanity checks; no exported declarations), and builds cleanly with lake build in 1753 jobs.

24

The 1-Bit Barrier is universal across the two standard modular reductions in NTT-PQC hardware (Barrett, Montgomery) and propagates faithfully through 𝑘-stage pipelines under fresh inter-stage masking. The QANARY program now provides, in machine-checked form, the quantitative compositional foundation that designers of post-quantum cryptographic accelerators need: a depth-independent cardinality bound on per-observation output preimages whose informal semantic interpretation under the first-order uniform-mask probing model is a 2/𝑞 per-observation conditional probability bound. The cardinality bound itself is the Lean-formalized result; the per-observation probability bound is the engineering consequence on which DPA-resistance arguments rest.

Code and Data Availability The Lean 4 artifact accompanying this paper is publicly available under the MIT license: •

• • •

Repository: https://github.com/rayiskander2406/qanary-k-stage-composition-arXivXXXX.XXXXX (arXiv ID will be substituted post-submission per series convention; repository becomes public concurrent with arXiv mint and once Papers 5 + 6, sibling Lake dependencies, are also public). Toolchain: Lean 4 v4.30.0-rc1 (managed via elan). Pinned dependency: Mathlib at commit 322515540d7fd29ef8992b82c89044f86f02ac10. License: MIT (artifact); CC-BY-4.0 (manuscript).

Reproduction

# Sibling repos required for local-path dependencies declared in lakefile.lean. # Place all five repositories under a common parent directory. mkdir qanary-artifacts && cd qanary-artifacts git clone https://github.com/rayiskander2406/qanary-universal-maskingproofs-arXiv-2604.18717 qanary-universal git clone https://github.com/rayiskander2406/qanary-masked-nttpipeline-security-arXiv-2604.20793 qanary-paper4 git clone https://github.com/rayiskander2406/qanary-one-bit-barrierarXiv-2604.24670 qanary-paper5 git clone https://github.com/rayiskander2406/qanary-pf-pinicomposition-arXiv-2604.25878 qanary-paper6 # Paper 7 itself: clone the public artifact once the arXiv mint completes. # The github.com URL on the next line substitutes the actual arXiv ID # for the placeholder per series convention (see §"Code and Data # Availability" repository note above); the URL as written is NOT a # runnable URL. git clone https://github.com/rayiskander2406/qanary-k-stagecomposition-arXiv-XXXX.XXXXX qanary-paper7 # placeholder, substitute real arXiv ID at mint time cd qanary-paper7 lake build # ~5–30 min on first run depending on hardware (cached Mathlib runs are at the lower end; clean fetches at the higher end) python3 reproduce.py --check 25

Expected output: 20 proved declarations across the three theorem modules (KStageComposition.lean, MontgomeryPFPINI.lean, ConfirmationTheorem.lean); Basic.lean carries shared imports and sanity checks but no exported declarations; zero sorry, zero admit, zero added axiom, zero native_decide calls, zero errors. The reproduce.py --check script enforces toolchain pin, Mathlib pin, sibling artifacts, build success, zero-stub scan, theorem index match, license, citation metadata, and archive bundle. The full lake build reports 1753 jobs.

Artifact contents Table 3 maps each top-level path in the artifact to its purpose. Path QanaryPaper7/Basic.lean

Purpose Shared imports + utilities (Mathlib, QanaryPaper5.Basic, QanaryPaper6.PositiveComposition).

QanaryPaper7/KStageComposition.lean

𝑘 -stage pipeline definition (kPipelineOutput, specialization lemmas kPipelineOutput_one, kPipelineOutput_two), the headline theorem pfpini_pipeline_composition_k_stages and its max-bound corollary pfpini_pipeline_composition_k_stages_max _bound. Montgomery reduction map (montgomeryInternalMap), two-branch lemma (montgomeryInternalMap_eq_or), preimage-subset lemma, the montgomery_max_multiplicity_two PFPINI(2) bound, the montgomeryPFPINI gadget instance, and tightness via montgomery_count_eq_two. End-to-end capstone (qanary_kstage_output_multiplicity_bound) , butterfly-only specialization (qanary_butterfly_only_multiplicity_bound) , modular-reduction-pipeline specialization (qanary_modular_reduction_pipeline_multi plicity_bound), and the hypothesis-violation conditional qanary_unmasked_stage_violates_hypothesi s. Library root + scaffold harness. QanaryPaper7.lean is the operative root that imports the four QanaryPaper7/*.lean modules (referenced by lean_lib QanaryPaper7 in lakefile.lean); Main.lean is a Phase-0 build-elaboration heartbeat retained for sibling-dependency-resolution

QanaryPaper7/MontgomeryPFPINI.lean

QanaryPaper7/ConfirmationTheorem.lean

QanaryPaper7.lean, Main.lean

26

Path

lakefile.lean, lake-manifest.json

lean-toolchain LICENSE, CITATION.cff, .zenodo.json reproduce.py README.md

Purpose sanity checks and is not part of the exported proof surface. Build configuration with pinned Mathlib and four sibling-repo dependencies (Papers 3, 4, 5, 6). Pins leanprover/lean4:v4.30.0-rc1. MIT license, machine-readable citation metadata, Zenodo deposit metadata. Single-command verification entry point (-check mode skips re-build). Top-level documentation and theorem index.

Table 3. Artifact path inventory. The three theorem modules (KStageComposition.lean, MontgomeryPFPINI.lean, ConfirmationTheorem.lean) contain the 20 declarations listed above; Basic.lean carries shared imports and sibling-dependency sanity checks. Total lake build job count: 1753. Paper 7 imports the Lean kernels of Papers 3 (qanaryUniversal), 4 (qanaryPaper4), 5 (qanaryPaper5), and 6 (qanaryPaper6) as local-path Lake dependencies; sibling clones of all four are therefore required for lake build to succeed (see the Reproduction block above).

Archival DOI A long-term-preservation Zenodo deposit will be minted prior to arXiv submission, following the pattern established for Paper 1 (10.5281/zenodo.19625392), Paper 2 (10.5281/zenodo.19508454), Paper 3 (10.5281/zenodo.19689480), and Paper 4 (10.5281/zenodo.19705450). The concept DOI (always resolving to the latest archived version) and the v1.0.0 version DOI (fixed to a specific git commit) will be substituted into this section in the next manuscript revision following deposit.

Independent reproducibility The artifact has no external data dependencies, no random seeds, and no networked services beyond the initial lake package fetches. Verification is purely a function of the Lean 4 kernel and the pinned Mathlib commit; identical inputs yield identical outputs across machines. The trusted computing base is the Lean 4 kernel; this paper’s artifact contains no native_decide invocations.

References 1. Iskander, Kirah, Structural Dependency Analysis for Masked NTT Hardware: Scalable Pre-Silicon Verification of Post-Quantum Cryptographic Accelerators, arXiv:2604.15249 (Paper 1 of QANARY program). https://arxiv.org/abs/2604.15249. (Verification chain: arXiv listing v2 2026-04-20; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-16, v2 replaced 2026-04-20. Zenodo concept DOI: 10.5281/zenodo.19625392.) 27

2. Iskander, Kirah, Partial Number Theoretic Transform Masking in Post-Quantum Cryptography (PQC) Hardware: A Security Margin Analysis, arXiv:2604.03813 (Paper 2 of QANARY program). https://arxiv.org/abs/2604.03813. (Verification chain: arXiv listing v2 2026-04-17; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-04, v2 replaced 2026-04-17. Zenodo concept DOI: 10.5281/zenodo.19508454.) 3. Iskander, Kirah, Machine-Checked Cardinality Bounds for Masked Barrett Reduction: A 1-Bit Side-Channel Leakage Barrier in Post-Quantum Cryptographic Hardware, arXiv:2604.24670 (Paper 5 of QANARY program). https://arxiv.org/abs/2604.24670. (Verification chain: arXiv listing 2026-04-27; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-27, v2 replaced 2026-04-28. Zenodo concept DOI: 10.5281/zenodo.19842166.) 4. Iskander, Kirah, Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking, arXiv:2604.25878 (Paper 6 of QANARY program). https://arxiv.org/abs/2604.25878. (Verification chain: arXiv listing v1 2026-04-28; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-28 (publicly listed 2026-04-29). Zenodo concept DOI: 10.5281/zenodo.19905303.) 5. Iskander, Kirah, From Finite Enumeration to Universal Proof: Ring-Theoretic Foundations for PQC Hardware Masking Verification, arXiv:2604.18717 (Paper 3 of QANARY program). https://arxiv.org/abs/2604.18717. (Verification chain: arXiv listing 2026-04-22; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-20, v2 replaced 2026-04-22. Zenodo concept DOI: 10.5281/zenodo.19689480.) 6. Iskander, Kirah, Fresh Masking Makes NTT Pipelines Composable: MachineChecked Proofs for Arithmetic Masking in PQC Hardware, arXiv:2604.20793 (Paper 4 of QANARY program). https://arxiv.org/abs/2604.20793. (Verification chain: arXiv listing v2 2026-04-25; primary subject cs.CR; authors Iskander, Kirah; v1 submitted 2026-04-22 (publicly listed 2026-04-23), v2 replaced 2026-04-25. Zenodo concept DOI: 10.5281/zenodo.19705450.) 7. Karabulut, M., Azarderakhsh, R., Efficient CPA Attack on Hardware Implementation of ML-DSA in Post-Quantum Root of Trust, IACR ePrint 2025/009; IEEE International Symposium on Hardware Oriented Security and Trust (HOST) 2025. 8. Saarinen, Why “Adams Bridge” Leaks: Attacking a PQC Root-of-Trust, Hardwear.io USA 2025 (invited talk). Slides: https://hardwear.io/usa-2025/presentation/attackinga-pqc-root-of-trust.pdf. 9. National Institute of Standards and Technology, Module-Lattice-Based Digital Signature Standard, Federal Information Processing Standards Publication 204, August 13, 2024. DOI: 10.6028/NIST.FIPS.204. 10. National Institute of Standards and Technology, Module-Lattice-Based KeyEncapsulation Mechanism Standard, Federal Information Processing Standards Publication 203, August 13, 2024. DOI: 10.6028/NIST.FIPS.203. 11. Ishai, Sahai, Wagner, Private Circuits: Securing Hardware against Probing Attacks, CRYPTO 2003, LNCS 2729, pp. 463–481. Springer. DOI: 10.1007/978-3-54045146-4_27. 12. Barthe, G., Belaïd, S., Dupressoir, F., Fouque, P.-A., Grégoire, B., Strub, P.-Y., Zucchini, R. Strong Non-Interference and Type-Directed Higher-Order Masking. Proc. 28

2016 ACM SIGSAC Conference on Computer and Communications Security (CCS ’16), Vienna, October 2016, ACM. DOI: 10.1145/2976749.2978427. ePrint 2015/506. 13. Cassiers, G., Standaert, F.-X., Trivially and Efficiently Composing Masked Gadgets with Probe Isolating Non-Interference, IEEE Transactions on Information Forensics and Security, Vol. 15 (2020), pp. 2542–2555. DOI: 10.1109/TIFS.2020.2971153. Preprint: IACR ePrint 2018/438. 14. National Institute of Standards and Technology, Security Requirements for Cryptographic Modules, Federal Information Processing Standards Publication 140-3, approved March 22, 2019; effective September 22, 2019. DOI: 10.6028/NIST.FIPS.140-3. URL: https://csrc.nist.gov/pubs/fips/140-3/final. 15. National Institute of Standards and Technology, Transition to Post-Quantum Cryptography Standards, NIST Internal Report 8547 (Initial Public Draft), November 2024. DOI: 10.6028/NIST.IR.8547.ipd. 16. International Organization for Standardization / International Electrotechnical Commission, Information technology – Security techniques – Testing methods for the mitigation of non-invasive attack classes against cryptographic modules, ISO/IEC 17825:2024. 17. Barthe, Belaïd, Dupressoir, Fouque, Grégoire, Strub, Verified Proofs of Higher-Order Masking, EUROCRYPT 2015, LNCS 9056, pp. 457–485. Springer. DOI: 10.1007/978-3-662-46800-5_18. Preprint: IACR ePrint 2015/060. 18. Knichel, Sasdrich, Moradi, SILVER – Statistical Independence and Leakage Verification, ASIACRYPT 2020 (ePrint 2020/634). 19. Coron, J.-S. Higher Order Masking of Look-Up Tables. EUROCRYPT 2014, LNCS 8441, pp. 441–458. DOI: 10.1007/978-3-642-55220-5_25. ePrint 2013/700. 20. Goubin, L. A Sound Method for Switching between Boolean and Arithmetic Masking. CHES 2001, LNCS 2162, pp. 3–15. Springer. DOI: 10.1007/3-540-44709-1_2. 21. Coron, J.-S., Tchulkine, A. A New Algorithm for Switching from Arithmetic to Boolean Masking. CHES 2003, LNCS 2779, pp. 89–97. Springer. DOI: 10.1007/9783-540-45238-6_8. 22. Bisheh-Niasar, M., Karabulut, E., Upadhyayula, K., Norris, M., Pillilli, B. Adams Bridge Accelerator: Bridging the Post-Quantum Transition. IACR ePrint 2026/256. (Design paper for the Caliptra-family Adams Bridge accelerator; distinct in both authorship and substance from [8]. Identity-disambiguation note: this entry’s second author is Emre Karabulut (Caliptra / Microsoft team, Adams Bridge designer); ref [7]’s first author is Merve Karabulut (Florida Atlantic University, attack paper co-author with Reza Azarderakhsh). These are two different researchers who share a last name. This paper does not assert, imply, or rely on any relationship between them.) 23. Pillilli, B., et al. Adams Bridge: An Accelerator for Post-Quantum Resilient Cryptography, Microsoft Azure Confidential Computing Blog, October 15, 2024. Announcement of the open-sourced Adams Bridge accelerator (ML-DSA / Dilithium only) as a discrete crypto accelerator and as integrated into Caliptra 2.0. URL: https://techcommunity.microsoft.com/blog/azureconfidentialcomputingblog/adamsbridge-an-accelerator-for-post-quantum-resilient-cryptography/4269585. 29

24. CHIPS Alliance, Caliptra 2.1 RTL Release, October 2025 (announced at OCP Global Summit). Integrates Adams Bridge 2.0 with both ML-DSA-87 and ML-KEM 1024 and side-channel countermeasures. URL: https://www.chipsalliance.org/news/caliptra2-1/; release notes at https://github.com/chipsalliance/caliptra-rtl/blob/main/Release_Notes.md. 25. Groß, H., Mangard, S., Korak, T. Domain-Oriented Masking: Compact Masked Hardware Implementations with Arbitrary Protection Order. Proceedings of the 2016 ACM Workshop on Theory of Implementation Security (TIS ’16), pp. 3–13, October 2016. DOI: 10.1145/2996366.2996426. Preprint: IACR ePrint 2016/486. 26. Faust, S., Grosso, V., Merino Del Pozo, S., Paglialonga, C., Standaert, F.-X. Composable Masking Schemes in the Presence of Physical Defaults & the Robust Probing Model. IACR Transactions on Cryptographic Hardware and Embedded Systems (TCHES), 2018(3), pp. 89–120. DOI: 10.13154/tches.v2018.i3.89-120. Preprint: IACR ePrint 2017/711.

30