Correctness of the Inner-Outer Ajtai Commitment

Perfect correctness for lawful gadget decompositions: if the message and inner gadget decompositions invert their gadget matrices, an honest commitment always verifies.

References

• Nguyen, N. K., and Seiler, G., Greyhound: Fast Polynomial Commitments from Lattices
• Nguyen, N. K., O'Rourke, G., and Zhang, J., Hachi: Efficient Lattice-Based Multilinear Polynomial Commitments over Extension Fields

theorem ArkLib.Lattices.Ajtai.InnerOuter.generateDecomps_derivedMessage {R : Type} [Field R] [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} (base : R) (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits) (hMessageDecomp : IsLawfulGadgetDecomposition Φ base decomp.message) (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) (i : Fin blocks) : derivedMessage Φ base (generateDecomps Φ decomp pp m) i = m i

Honest message decompositions recover the message: G · sᵢ = mᵢ (derivedMessage = m).

theorem ArkLib.Lattices.Ajtai.InnerOuter.generateDecomps_message_checks {R : Type} [Field R] [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} [DecidableEq (PolyVec Φ.Rq messageRows)] (base : R) (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits) (hMessageDecomp : IsLawfulGadgetDecomposition Φ base decomp.message) (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) : ((List.finRange blocks).all fun (i : Fin blocks) => Simple.verify Φ (gadgetMatrix Φ base messageRows messageDigits) ((generateDecomps Φ decomp pp m).message i) (m i) ()) = true

Honest message decompositions pass the message gadget checks.

theorem ArkLib.Lattices.Ajtai.InnerOuter.generateDecomps_inner_eq {R : Type} [Field R] [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} (base : R) (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits) (hInnerDecomp : IsLawfulGadgetDecomposition Φ base decomp.inner) (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) (i : Fin blocks) : Simple.commit Φ (gadgetMatrix Φ base innerRows innerDigits) ((generateDecomps Φ decomp pp m).innerDecomp i) = Simple.commit Φ pp.innerMatrix ((generateDecomps Φ decomp pp m).message i)

Honest inner decompositions satisfy the inner gadget relation G · t̂ᵢ = A sᵢ.

theorem ArkLib.Lattices.Ajtai.InnerOuter.generateDecomps_inner_checks {R : Type} [Field R] [BEq R] [LawfulBEq R] (Φ : CyclotomicModulus R) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} [DecidableEq (PolyVec Φ.Rq innerRows)] (base : R) (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits) (hInnerDecomp : IsLawfulGadgetDecomposition Φ base decomp.inner) (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) : ((List.finRange blocks).all fun (i : Fin blocks) => Simple.verify Φ (gadgetMatrix Φ base innerRows innerDigits) ((generateDecomps Φ decomp pp m).innerDecomp i) (Simple.commit Φ pp.innerMatrix ((generateDecomps Φ decomp pp m).message i)) ()) = true

Honest inner decompositions pass the inner gadget checks.

Concrete instantiation over ZMod q

The genuine base-b (binary) gadget decomposition zmodDigitDecomposition instantiates the inner-outer commitment over R = ZMod q, giving perfect correctness whenever 1 < b, every residue fits in the chosen digit count (q ≤ b ^ digits), and 1 ≤ deg φ.

theorem ArkLib.Lattices.Ajtai.InnerOuter.perfectlyCorrect_of_lawful {q : ℕ} [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)] (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} [SampleableType (Simple.PublicParams Φ innerRows (messageRows * messageDigits))] [SampleableType (Simple.PublicParams Φ outerRows (blocks * (innerRows * innerDigits)))] (base : ZMod q) (βSq γ κ : ℕ) (decomp : Decomposition Φ messageRows messageDigits innerRows innerDigits) (hMessageDecomp : IsLawfulGadgetDecomposition Φ base decomp.message) (hInnerDecomp : IsLawfulGadgetDecomposition Φ base decomp.inner) (hκpos : 0 < CyclotomicModulus.Rq.l1Norm Φ 1) (hκle : CyclotomicModulus.Rq.l1Norm Φ 1 ≤ κ) (hβ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) (i : Fin blocks), Φ.vecL2NormSq ((generateDecomps Φ decomp pp m).message i) ≤ βSq) (hγ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks), Φ.vecLInftyNorm (generateDecomps Φ decomp pp m).innerDecomp.flattenBlocks ≤ γ) : (commitmentScheme Φ base βSq γ κ decomp).PerfectlyCorrect

Perfect correctness of the inner-outer Ajtai commitment for lawful decompositions.

The honest opening uses the trivial challenge cᵢ = 1, under which verify_weak reduces to the ordinary honest check. Correctness therefore needs, beyond gadget lawfulness:

• the trivial challenge is an admissible challenge: 0 < ‖1‖₁ and ‖1‖₁ ≤ κ;
• each honest message decomposition is ℓ₂²-short: ‖sᵢ‖₂² ≤ βSq;
• the flattened honest inner decomposition is ℓ∞-short: ‖t̂‖∞ ≤ γ.

The gadget relations (derivedMessage = m, inner A sᵢ = G t̂ᵢ, outer commit) hold structurally from lawfulness; the bounds are exactly the weak-verifier side conditions for the honest case.

theorem ArkLib.Lattices.Ajtai.InnerOuter.perfectlyCorrect_of_digits {q : ℕ} [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)] (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} [SampleableType (Simple.PublicParams Φ innerRows (messageRows * messageDigits))] [SampleableType (Simple.PublicParams Φ outerRows (blocks * (innerRows * innerDigits)))] (base : ZMod q) (βSq γ κ : ℕ) (hdeg : 1 ≤ Φ.φ.natDegree) (hmsg : 0 < messageDigits) (hinner : 0 < innerDigits) (ddMsg : DigitDecomposition base messageDigits) (ddInner : DigitDecomposition base innerDigits) (hκpos : 0 < CyclotomicModulus.Rq.l1Norm Φ 1) (hκle : CyclotomicModulus.Rq.l1Norm Φ 1 ≤ κ) (hβ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks) (i : Fin blocks), Φ.vecL2NormSq ((generateDecomps Φ (Decomposition.ofDigits Φ ddMsg ddInner) pp m).message i) ≤ βSq) (hγ : ∀ (pp : PublicParams Φ innerRows messageRows messageDigits outerRows blocks innerDigits) (m : Message Φ messageRows blocks), Φ.vecLInftyNorm (generateDecomps Φ (Decomposition.ofDigits Φ ddMsg ddInner) pp m).innerDecomp.flattenBlocks ≤ γ) : (commitmentScheme Φ base βSq γ κ (Decomposition.ofDigits Φ ddMsg ddInner)).PerfectlyCorrect

Perfect correctness for genuine base-b (Hachi gadget G⁻¹) decompositions, modulo the weak-verifier shortness side conditions. Instantiates perfectlyCorrect_of_lawful with gadgetDecompose (lawful by gadgetDecompose_lawful), discharging gadget lawfulness; the trivial-challenge admissibility (hκpos, hκle) and the honest shortness bounds (hβ, hγ) remain explicit. For the concrete binary decomposition they are discharged unconditionally by perfectlyCorrect below (via Rq.l1Norm_one and the GadgetNorms bounds).

theorem ArkLib.Lattices.Ajtai.InnerOuter.perfectlyCorrect {q : ℕ} [NeZero q] [Fact (Nat.Prime q)] [BEq (ZMod q)] [LawfulBEq (ZMod q)] (Φ : CyclotomicModulus (ZMod q)) [IsCyclotomic Φ] {innerRows messageRows messageDigits outerRows blocks innerDigits : ℕ} [SampleableType (Simple.PublicParams Φ innerRows (messageRows * messageDigits))] [SampleableType (Simple.PublicParams Φ outerRows (blocks * (innerRows * innerDigits)))] (b κ : ℕ) (hb : 1 < b) (hκ : 1 ≤ κ) (hbq : b - 1 ≤ q / 2) (hdeg : 1 ≤ Φ.φ.natDegree) (hmsg : 0 < messageDigits) (hinner : 0 < innerDigits) (hqm : q ≤ b ^ messageDigits) (hqi : q ≤ b ^ innerDigits) : (commitmentScheme Φ (↑b) (messageRows * messageDigits * (Φ.φ.natDegree * (b - 1) ^ 2)) (b - 1) κ (Decomposition.ofDigits Φ (zmodDigitDecomposition b messageDigits hb hqm) (zmodDigitDecomposition b innerDigits hb hqi))).PerfectlyCorrect

Unconditional perfect correctness with the concrete binary decomposition. Both message and inner decompositions are the genuine base-b digit decomposition of ZMod q (zmodDigitDecomposition, the Hachi gadget inverse G⁻¹). All weak-verifier side conditions are discharged automatically: the trivial challenge cᵢ = 1 is short (Rq.l1Norm_one), and the digit decompositions are short (GadgetNorms), with βSq := (mr·md)·(deg φ)·(b-1)² and γ := b - 1. The hypotheses are exactly those for reconstruction (1 < b, q ≤ bᵈⁱᵍⁱᵗˢ, 1 ≤ deg φ, positive digit counts), plus 1 ≤ κ and the no-wraparound condition b - 1 ≤ q/2 for the centered digit norm.