Blinding

Proved: A·s' + e' + (A·s₁ + s₂) = A·(s₁ + s') + (s₂ + e') over any commutative ring -- the sender's published value is the honest ML-DSA public key of the widened secret, which is why the recipient can sign -- and the Power2Round rounding-error bound for the announced key, generic and at the concrete ML-DSA parameters (docs/TECHNICAL_SPEC.md §4).

Assumed: nothing. Pure algebra over VCVio's LatticeCrypto layer.

`blinded_key_correctness`

Blinding is key-preserving: the sender's published value A *ᵥ s' + e' added to the recipient's meta key A *ᵥ s₁ + s₂ is the honest public key of the widened secret (s₁ + s', s₂ + e'), over any commutative ring.

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem blinded_key_correctness {R : Type*} [CommRing R] {k l : ℕ}
    (A : Matrix (Fin k) (Fin l) R) (s₁ s' : Fin l → R) (s₂ e' : Fin k → R) :
    A *ᵥ s' + e' + (A *ᵥ s₁ + s₂) = A *ᵥ (s₁ + s') + (s₂ + e') := by

proof

  rw [Matrix.mulVec_add]
  abel

Blinding.lean:26-31 ↗

`stealth_pk_eq_blinded_keypair`

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem stealth_pk_eq_blinded_keypair {R : Type*} [CommRing R] {k l : ℕ}
    (A : Matrix (Fin k) (Fin l) R) (s₁ s' : Fin l → R) (s₂ e' t : Fin k → R)
    (ht : t = A *ᵥ s₁ + s₂) :
    A *ᵥ s' + e' + t = A *ᵥ (s₁ + s') + (s₂ + e') := by

proof

  subst ht
  exact blinded_key_correctness A s₁ s' s₂ e'

Blinding.lean:35-41 ↗

1. The blinded-key correctness identity

`stealth_pk_rounding_error`

The rounding error dropped by Power2Round on an announced stealth key is at most 2 ^ (d - 1), for any parameters satisfying the Power2RoundOps laws.

axioms: propext · sorry-free ✓

theorem stealth_pk_rounding_error {Coeff : Type*} [CommRing Coeff]
    {ring : NegacyclicRing Coeff} [AddCommGroup ring.Poly] {d : ℕ}
    (ops : Power2RoundOps ring d) (cnorm : ring.Poly → ℕ)
    (laws : Power2RoundOps.Laws ops cnorm) (t' : ring.Poly) :
    cnorm (t' - ops.shift2 (ops.power2Round t')) ≤ 2 ^ (d - 1) :=
  laws.power2Round_bound t'

Blinding.lean:49-55 ↗

`stealth_pk_rounding_error_concrete`

Concrete instantiation at the ML-DSA parameters (d = 13): the rounding error of every announced stealth public key is at most 2^12. Uses the proven (sorry-free) MLDSA.Concrete.concretePower2RoundLaws.

axioms: propext, Classical.choice, Quot.sound · sorry-free ✓

theorem stealth_pk_rounding_error_concrete (t' : Rq) :
    cInfNorm (t' - concretePower2RoundOps.shift2
        (concretePower2RoundOps.power2Round t')) ≤ 2 ^ 12 :=
  concretePower2RoundLaws.power2Round_bound t'

Blinding.lean:60-64 ↗