Invariants
Proved: centered-norm sub-additivity, hence the blinded secret is 2·eta-short
and the signer bound doubles (beta' = tau·(2·eta) = 2·beta); the ownership
relation TOGETHER WITH the coefficient bound IS possession of an ML-DSA signing
key, and the blinded secret is such a key; the stealth public key roundtrips,
and so do both meta-address wire formats as CONCRETE byte strings at their
spec lengths — 0x01 at 5,633 B and the commitment form 0x02 at 1,217 B
(docs/DECISIONS.md D-024, Lean items 1-3).
Assumed: the two inner packers (pack23 of full-precision t, the ML-KEM
encapsulation key) are parameters with roundtrip hypotheses — VCVio has no
fixed-length byte encoder with a proven law (docs/encodings.md).
cInfNorm_add_le
Centered infinity norm is sub-additive: ‖f + g‖ ≤ ‖f‖ + ‖g‖.
The centered representative is ZMod.valMinAbs, which is sub-additive in
absolute value (natAbs_valMinAbs_add_le), lifted coefficient-wise.
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem cInfNorm_add_le (f g : Rq) :
cInfNorm (f + g) ≤ cInfNorm f + cInfNorm g := byproof
apply cInfNorm_le_of_coeff_le
intro i
rw [Rq.get_add, centeredRepr_eq_valMinAbs]
calc ((f.get i + g.get i).valMinAbs).natAbs
≤ ((f.get i).valMinAbs + (g.get i).valMinAbs).natAbs :=
ZMod.natAbs_valMinAbs_add_le _ _
_ ≤ ((f.get i).valMinAbs).natAbs + ((g.get i).valMinAbs).natAbs :=
Int.natAbs_add_le _ _
_ ≤ cInfNorm f + cInfNorm g := by
rw [← centeredRepr_eq_valMinAbs, ← centeredRepr_eq_valMinAbs]
exact Nat.add_le_add (coeff_le_cInfNorm f i) (coeff_le_cInfNorm g i)blinded_norm_bound
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blinded_norm_bound {f g : Rq} {eta : ℕ}
(hf : cInfNorm f ≤ eta) (hg : cInfNorm g ≤ eta) :
cInfNorm (f + g) ≤ 2 * eta :=
(cInfNorm_add_le f g).trans (by omega)beta_blinded_eq_two_beta
axioms: propext · sorry-free ✓
theorem beta_blinded_eq_two_beta (params : Params) :
params.tau * (2 * params.eta) = 2 * params.beta := byproof
unfold MLDSA.Params.beta; ring1. Widened-bound signing invariant
IsOwnershipWitness
The MLWE ownership relation the ZK circuit proves: A *ᵥ s + e = t.
This is the linear half only; shortness is IsShortPair.
def IsOwnershipWitness {R : Type*} [CommRing R] {k l : ℕ}
(A : Matrix (Fin k) (Fin l) R) (t : Fin k → R)
(s : Fin l → R) (e : Fin k → R) : Prop :=
A *ᵥ s + e = tIsShortPair
def IsShortPair {k l : ℕ} (eta : ℕ) (s : Fin l → Rq) (e : Fin k → Rq) : Prop :=
(∀ i, cInfNorm (s i) ≤ eta) ∧ (∀ i, cInfNorm (e i) ≤ eta)IsSigningKey
def IsSigningKey {k l : ℕ}
(A : Matrix (Fin k) (Fin l) Rq) (t : Fin k → Rq)
(s : Fin l → Rq) (e : Fin k → Rq) (eta : ℕ) : Prop :=
IsOwnershipWitness A t s e ∧ IsShortPair eta s eownership_iff_signing
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem ownership_iff_signing {k l : ℕ}
(A : Matrix (Fin k) (Fin l) Rq) (t : Fin k → Rq)
(s : Fin l → Rq) (e : Fin k → Rq) (eta : ℕ) :
(IsOwnershipWitness A t s e ∧
(∀ i, cInfNorm (s i) ≤ eta) ∧ (∀ i, cInfNorm (e i) ≤ eta)) ↔
IsSigningKey A t s e eta :=
Iff.rflblinded_is_ownership_witness
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blinded_is_ownership_witness {R : Type*} [CommRing R] {k l : ℕ}
(A : Matrix (Fin k) (Fin l) R) (s₁ s' : Fin l → R) (s₂ e' : Fin k → R) :
IsOwnershipWitness A (A *ᵥ s' + e' + (A *ᵥ s₁ + s₂)) (s₁ + s') (s₂ + e') :=
(blinded_key_correctness A s₁ s' s₂ e').symmblinded_is_signing_key
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem blinded_is_signing_key {k l : ℕ}
(A : Matrix (Fin k) (Fin l) Rq) (s₁ s' : Fin l → Rq) (s₂ e' : Fin k → Rq)
{eta : ℕ}
(hs₁ : ∀ i, cInfNorm (s₁ i) ≤ eta) (hs' : ∀ i, cInfNorm (s' i) ≤ eta)
(hs₂ : ∀ i, cInfNorm (s₂ i) ≤ eta) (he' : ∀ i, cInfNorm (e' i) ≤ eta) :
IsSigningKey A (A *ᵥ s' + e' + (A *ᵥ s₁ + s₂)) (s₁ + s') (s₂ + e')
(2 * eta) :=
⟨blinded_is_ownership_witness A s₁ s' s₂ e',
fun i => blinded_norm_bound (hs₁ i) (hs' i),
fun i => blinded_norm_bound (hs₂ i) (he' i)⟩2. Ownership relation <-> signing-key possession
stealth_pk_roundtrips
The stealth public key roundtrips: decoding the encoded (rho, t1) returns
it unchanged — a direct consequence of VCVio's public-key encoding law.
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem stealth_pk_roundtrips {p : Params} {prims : Primitives p}
(enc : Encoding p prims) (laws : enc.Laws)
(rho : Bytes 32) (t1 : Vector prims.Power2High p.k) :
enc.pkDecode (enc.pkEncode rho t1) = (rho, t1) :=
laws.pkDecode_pkEncode rho t1splitBytes
Split a byte string of length m + n at offset m.
def splitBytes {m n : ℕ} (v : Bytes (m + n)) : Bytes m × Bytes n :=
((v.extract 0 m).cast (by omega), (v.extract m (m + n)).cast (by omega))splitBytes_append
theorem splitBytes_append {m n : ℕ} (a : Bytes m) (b : Bytes n) :
splitBytes (a ++ b) = (a, b) := byproof
have h₁ : ((a ++ b).extract 0 m).cast (by omega) = a := by
refine Vector.ext fun i hi => ?_
simp only [Vector.getElem_cast, Vector.getElem_extract, Nat.zero_add,
Vector.getElem_append]
rw [dif_pos hi]
have h₂ : ((a ++ b).extract m (m + n)).cast (by omega) = b := by
refine Vector.ext fun i hi => ?_
simp only [Vector.getElem_cast, Vector.getElem_extract, Vector.getElem_append,
Nat.add_sub_cancel_left]
rw [dif_neg (by omega)]
rw [splitBytes, h₁, h₂]qBits
Bit width of a full-precision ML-DSA coefficient: q = 8380417 < 2^23
(the spec's Q_BITS; a standard public key would instead carry t1).
def qBits : ℕ := 23packedTBytes
def packedTBytes (p : Params) : ℕ := p.k * ringDegree * qBits / 8packedTBytes_mldsa65
theorem packedTBytes_mldsa65 : packedTBytes mldsa65 = 4416 := rflmetaAddressEncode
def metaAddressEncode {T Ek : Type*} {nt nek : ℕ}
(packT : T → Bytes nt) (packEk : Ek → Bytes nek)
(version : UInt8) (rho : Bytes 32) (t : T) (ek : Ek) :
Bytes (1 + (32 + (nt + nek))) :=
#v[version] ++ (rho ++ (packT t ++ packEk ek))metaAddressDecode
def metaAddressDecode {T Ek : Type*} {nt nek : ℕ}
(unpackT : Bytes nt → T) (unpackEk : Bytes nek → Ek)
(m : Bytes (1 + (32 + (nt + nek)))) : UInt8 × Bytes 32 × T × Ek :=
let s := splitBytes m
let r := splitBytes s.2
let b := splitBytes r.2
(s.1[0], r.1, unpackT b.1, unpackEk b.2)meta_address_roundtrips
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem meta_address_roundtrips {T Ek : Type*} {nt nek : ℕ}
(packT : T → Bytes nt) (unpackT : Bytes nt → T)
(hT : ∀ t, unpackT (packT t) = t)
(packEk : Ek → Bytes nek) (unpackEk : Bytes nek → Ek)
(hEk : ∀ ek, unpackEk (packEk ek) = ek)
(version : UInt8) (rho : Bytes 32) (t : T) (ek : Ek) :
metaAddressDecode unpackT unpackEk
(metaAddressEncode packT packEk version rho t ek) = (version, rho, t, ek) := byproof
simp only [metaAddressEncode, metaAddressDecode, splitBytes_append, hT, hEk]
rflmetaAddress_size_mldsa65_mlkem768
axioms: propext · sorry-free ✓
theorem metaAddress_size_mldsa65_mlkem768 :
1 + (32 + (packedTBytes mldsa65 + MLKEM.Params.publicKeyBytes MLKEM.mlkem768)) = 5633 :=
rflmeta_address_roundtrips_5633
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem meta_address_roundtrips_5633 {T Ek : Type*}
(packT : T → Bytes 4416) (unpackT : Bytes 4416 → T)
(hT : ∀ t, unpackT (packT t) = t)
(packEk : Ek → Bytes 1184) (unpackEk : Bytes 1184 → Ek)
(hEk : ∀ ek, unpackEk (packEk ek) = ek)
(version : UInt8) (rho : Bytes 32) (t : T) (ek : Ek) :
metaAddressDecode unpackT unpackEk
(metaAddressEncode packT packEk version rho t ek : Bytes 5633)
= (version, rho, t, ek) :=
meta_address_roundtrips packT unpackT hT packEk unpackEk hEk version rho t ekmetaAddressCommitEncode
The commitment meta-address, version(1) ‖ spend_key(32) ‖ ek: the full-precision
t of format 0x01 is replaced by a 32-byte commitment to the spending key.
def metaAddressCommitEncode {Ek : Type*} {nek : ℕ} (packEk : Ek → Bytes nek)
(version : UInt8) (commitment : Bytes 32) (ek : Ek) : Bytes (1 + (32 + nek)) :=
#v[version] ++ (commitment ++ packEk ek)metaAddressCommitDecode
def metaAddressCommitDecode {Ek : Type*} {nek : ℕ} (unpackEk : Bytes nek → Ek)
(m : Bytes (1 + (32 + nek))) : UInt8 × Bytes 32 × Ek :=
let s := splitBytes m
let r := splitBytes s.2
(s.1[0], r.1, unpackEk r.2)meta_address_commit_roundtrips
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem meta_address_commit_roundtrips {Ek : Type*} {nek : ℕ}
(packEk : Ek → Bytes nek) (unpackEk : Bytes nek → Ek)
(hEk : ∀ ek, unpackEk (packEk ek) = ek)
(version : UInt8) (commitment : Bytes 32) (ek : Ek) :
metaAddressCommitDecode unpackEk (metaAddressCommitEncode packEk version commitment ek)
= (version, commitment, ek) := byproof
simp only [metaAddressCommitEncode, metaAddressCommitDecode, splitBytes_append, hEk]
rflmetaAddressCommit_size_mlkem768
axioms: none · sorry-free ✓
theorem metaAddressCommit_size_mlkem768 :
1 + (32 + MLKEM.Params.publicKeyBytes MLKEM.mlkem768) = 1217 := rflmeta_address_commit_roundtrips_1217
axioms: propext, Classical.choice, Quot.sound · sorry-free ✓
theorem meta_address_commit_roundtrips_1217 {Ek : Type*}
(packEk : Ek → Bytes 1184) (unpackEk : Bytes 1184 → Ek)
(hEk : ∀ ek, unpackEk (packEk ek) = ek)
(version : UInt8) (commitment : Bytes 32) (ek : Ek) :
metaAddressCommitDecode unpackEk
(metaAddressCommitEncode packEk version commitment ek : Bytes 1217)
= (version, commitment, ek) :=
meta_address_commit_roundtrips packEk unpackEk hEk version commitment ek