mirror of
https://github.com/luxfi/proofs.git
synced 2026-10-30 15:21:05 +00:00
zooqueen
ebf46cbba8
Corona is Lux's fork of Ringtail (ePrint 2024/1113) = two-round Module-LWE
(M=8, N=7 over R_q=Z_q[X]/(X^256+1), q=0x1000000004A01 48-bit, sigma=6.108) —
NOT Ring-LWE rank-1. Corona.lean: hardness Module-LWE; axiom corona_ring_lwe_euf_cma
-> corona_module_lwe_euf_cma; EUF-CMA reduces to Module-LWE; params corrected
(was q=2^32/sigma=13744). Corona/{OutputInterchange,Unforgeability,dkg2}, Quasar,
Magnetar, HQC, BLS, Threshold_Lagrange label fixes. 'Ring-LWE = Module-LWE rank 1'
kept only as general math remark. lake build: success.
119 lines
4.9 KiB
Lean4
119 lines
4.9 KiB
Lean4
/-
|
||
Corona Output-Interchangeability (Class N1) -- Lean formalization.
|
||
|
||
Mirrors `~/work/lux/proofs/lean/Crypto/Pulsar/OutputInterchange.lean`;
|
||
Corona is a Module-LWE threshold scheme (the Ringtail-derived
|
||
parameter regime), distinct from Pulsar only in parameters/lifecycle.
|
||
|
||
Claim: every signature byte string produced by Corona's threshold
|
||
Combine procedure on inputs `(group_pk = (A, bTilde), m, ctx, quorum,
|
||
shares)` (satisfying the protocol invariants) verifies under the
|
||
Corona reference verifier `Verify(group_pk, m, σ)`.
|
||
|
||
EasyCrypt counterpart:
|
||
`~/work/lux/corona/proofs/easycrypt/Corona_N1_Extracted.ec`
|
||
`corona_n1_byte_equality_extracted` (equiv form).
|
||
-/
|
||
|
||
import Crypto.Corona.Shamir
|
||
import Crypto.Threshold_Lagrange
|
||
import Mathlib.Tactic
|
||
|
||
namespace Crypto.Corona.OutputInterchange
|
||
|
||
/-- Abstract types for the protocol layer. The three artifact types
|
||
that appear as outputs of the opaque protocol operations are modeled
|
||
as distinct single-field byte wrappers so they are `Inhabited` (every
|
||
real public key / share / signature is a concrete byte string), while
|
||
the protocol *operations* below remain fully opaque — that is where
|
||
the cryptographic abstraction lives. -/
|
||
structure GroupPk where ofBytes :: (bytes : ByteArray) deriving Inhabited
|
||
structure Share where ofBytes :: (bytes : ByteArray) deriving Inhabited
|
||
structure Signature where ofBytes :: (bytes : ByteArray) deriving Inhabited
|
||
opaque Message : Type
|
||
opaque Ctx : Type
|
||
opaque Randomness : Type
|
||
opaque Quorum : Type
|
||
|
||
/-- The Corona Verify predicate. -/
|
||
opaque verify : GroupPk → Message → Ctx → Signature → Bool
|
||
|
||
/-- The Corona threshold Combine output: byte string of the final
|
||
signature. -/
|
||
opaque threshold_combine :
|
||
GroupPk → Message → Ctx → Quorum → List Share → Randomness → Signature
|
||
|
||
/-- The centralized Boschini Sign output on the reconstructed share. -/
|
||
opaque central_sign :
|
||
Share → Message → Ctx → Randomness → Signature
|
||
|
||
/-- Lagrange reconstruction of the shares. -/
|
||
opaque reconstruct : Quorum → List Share → Share
|
||
|
||
/-- The public-key derivation map: secret -> public. -/
|
||
opaque derive_pk : Share → GroupPk
|
||
|
||
/-- The honest-quorum / accept-path predicate. -/
|
||
opaque accept_path : Share → Message → Ctx → Randomness → Prop
|
||
|
||
/-- Class N1 byte-equality: threshold Combine = central Sign on the
|
||
reconstructed share, byte-for-byte. This is the Lean statement of
|
||
the EC `corona_n1_byte_equality_extracted` theorem.
|
||
|
||
Stated as a named axiom because it is bridged to the EC proof; the
|
||
Lean side does NOT re-prove the byte-walk content (that's the
|
||
Jasmin extraction + MLWE_Functional structural identity). -/
|
||
axiom corona_n1_byte_equality
|
||
(gpk : GroupPk) (m : Message) (ctx : Ctx) (q : Quorum)
|
||
(shares : List Share) (rho : Randomness)
|
||
(sk_group : Share)
|
||
(h_recon : reconstruct q shares = sk_group)
|
||
(h_gpk : gpk = derive_pk sk_group)
|
||
(h_accept : accept_path sk_group m ctx rho) :
|
||
threshold_combine gpk m ctx q shares rho
|
||
= central_sign sk_group m ctx rho
|
||
|
||
/-- Verifier correctness on outputs of the centralized Sign.
|
||
This is Boschini ePrint 2024/1113 §3 Theorem 1, restated in Lean
|
||
as a named axiom (the proof is in the cited paper). -/
|
||
axiom corona_central_verify_correct
|
||
(sk : Share) (m : Message) (ctx : Ctx) (rho : Randomness)
|
||
(h_accept : accept_path sk m ctx rho) :
|
||
verify (derive_pk sk) m ctx (central_sign sk m ctx rho) = true
|
||
|
||
/-- Class N1 output interchangeability (the verifier-compatibility
|
||
corollary): every honest-quorum Corona signature verifies under
|
||
the same group public key.
|
||
|
||
Discharged: chains the byte-equality (`corona_n1_byte_equality`)
|
||
with the verifier correctness (`corona_central_verify_correct`). -/
|
||
theorem corona_output_interchangeable
|
||
(gpk : GroupPk) (m : Message) (ctx : Ctx) (q : Quorum)
|
||
(shares : List Share) (rho : Randomness)
|
||
(sk_group : Share)
|
||
(h_recon : reconstruct q shares = sk_group)
|
||
(h_gpk : gpk = derive_pk sk_group)
|
||
(h_accept : accept_path sk_group m ctx rho) :
|
||
verify gpk m ctx (threshold_combine gpk m ctx q shares rho) = true := by
|
||
rw [corona_n1_byte_equality gpk m ctx q shares rho sk_group
|
||
h_recon h_gpk h_accept]
|
||
rw [h_gpk]
|
||
exact corona_central_verify_correct sk_group m ctx rho h_accept
|
||
|
||
/-- Convenience theorem: byte-equality up to the group-pk-derivation
|
||
consistency. This is the cleanest statement reviewers should cite
|
||
when reading the EC bridge. -/
|
||
theorem corona_verify_is_construction_dispatch
|
||
(gpk : GroupPk) (m : Message) (ctx : Ctx) (q : Quorum)
|
||
(shares : List Share) (rho : Randomness)
|
||
(sk_group : Share)
|
||
(h_recon : reconstruct q shares = sk_group)
|
||
(h_gpk : gpk = derive_pk sk_group)
|
||
(h_accept : accept_path sk_group m ctx rho) :
|
||
threshold_combine gpk m ctx q shares rho
|
||
= central_sign sk_group m ctx rho :=
|
||
corona_n1_byte_equality gpk m ctx q shares rho sk_group
|
||
h_recon h_gpk h_accept
|
||
|
||
end Crypto.Corona.OutputInterchange
|