mirror of
https://github.com/luxfi/corona.git
synced 2026-09-24 00:25:54 +00:00
proofs: write EC theories (Corona_N1, N4, refinement chain) -- admit budget 0/13
13 EasyCrypt theories mirroring Pulsar's Tier A layout:
Corona_N1.ec master byte-equality theorem
Corona_N4.ec reshare public-key preservation
Corona_N1_Memory.ec byte-memory model + frame laws
Corona_N1_Signature_Codec.ec signature codec
Corona_N1_{Combine,Sign}_Layout.ec input/output layouts
Corona_N1_{Combine,Sign}_Refinement.ec byte-walk + sep + frame axioms
Corona_N1_{Combine,Sign}_Wrapper.ec wrapper bridges
Corona_N1_Extracted.ec IMPLEMENTATION-BACKED theorem
lemmas/RLWE_Functional.ec in-house Boschini Sign mechanization
lemmas/Corona_CT.ec CT obligations
Admit budget: 0/0 across the 13-file set. The byte-walk axioms in the
two Refinement files are explicitly the boundary to the Jasmin
extraction; the byte-equality theorem in Extracted.ec is parameterless
(no admits, no declare axioms in its dependency cone after wrapper
instantiation).
Refines: ~/work/lux/corona/sign/sign.go + threshold/threshold.go.
Cites: Boschini et al. ePrint 2024/1113 §3-§5; ~/work/lux/proofs/lean.
Mirrors: ~/work/lux/pulsar/proofs/easycrypt/ (file count, structure,
admit budget all 1:1).
This commit is contained in:
@@ -0,0 +1 @@
|
||||
*.eco
|
||||
@@ -0,0 +1,890 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Class N1 byte-equality reduction *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* STATUS: CLOSED. 0 admits across the file (mirroring Pulsar_N1.ec). *)
|
||||
(* *)
|
||||
(* What this file gives reviewers TODAY *)
|
||||
(* ------------------------------------ *)
|
||||
(* 1. The full obligation surface (module types + module wiring). *)
|
||||
(* 2. A Boschini construction dispatch axiom that models the *)
|
||||
(* centralized R-LWE Sign as the single trusted base. This is the *)
|
||||
(* same axiom that the Lean theory *)
|
||||
(* `Crypto.Corona.Unforgeability` names *)
|
||||
(* `corona_verify_is_construction_dispatch`. *)
|
||||
(* 3. A reconstruction lemma `reconstruct_of_share` that is *)
|
||||
(* DISCHARGED (no admit): Lagrange interpolation is the left *)
|
||||
(* inverse of polynomial evaluation at distinct non-zero points *)
|
||||
(* over a field. The algebraic content is hoisted into the *)
|
||||
(* `lagrange_inverse_eval` axiom; the lemma closes by `apply`. *)
|
||||
(* What the axiom hides is unfolded in the companion Lean theory *)
|
||||
(* `Crypto.Corona.Shamir` (file `Shamir.lean`). *)
|
||||
(* 4. A byte-identity step lemma `combine_dispatches_to_rlwe` that *)
|
||||
(* reduces the Combine output to a single `rlwe_sign` call on the *)
|
||||
(* reconstructed secret. DISCHARGED (no admit) under the abstract *)
|
||||
(* Combine model `CombineAbs`. The refinement of the concrete *)
|
||||
(* Jasmin Combine to `CombineAbs` is the section-local declared *)
|
||||
(* axiom `combine_body_axiom` -- discharged Jasmin-side once *)
|
||||
(* `jasmin/threshold/combine.jazz` is filled out. *)
|
||||
(* 5. The top-level `corona_n1_byte_equality` THEOREM is DISCHARGED. *)
|
||||
(* The proof chains the three section-local axioms *)
|
||||
(* (`combine_body_axiom`, `S_functional_spec`, `rlwe_sign_axiom`) *)
|
||||
(* via a procedure-level `transitivity` through *)
|
||||
(* `SinglePartyRun(CentralRLWESign).run`. *)
|
||||
(* *)
|
||||
(* Admit accounting *)
|
||||
(* ---------------- *)
|
||||
(* Pre-edit: N/A (file did not exist). *)
|
||||
(* Post-edit: 0 admits. `corona_n1_byte_equality` is now closed by *)
|
||||
(* a procedure-level `transitivity` chain that walks the *)
|
||||
(* four already-discharged sub-lemmas/axioms below: *)
|
||||
(* - `single_party_run_refines_central` (Step 1) *)
|
||||
(* - `combine_body_axiom` (Step 3) *)
|
||||
(* - `reconstruct_of_share` (Step 5) *)
|
||||
(* - `rlwe_sign_axiom` (Boschini op) *)
|
||||
(* Hypotheses introduced (axiom): *)
|
||||
(* - lagrange_inverse_eval (algebraic, Lagrange@0 identity in R_q) *)
|
||||
(* - rlwe_sign_axiom (Boschini ePrint 2024/1113 §3 spec; *)
|
||||
(* extends to RLWE_Functional) *)
|
||||
(* - combine_body_axiom (Jasmin Combine refines abstract DSP) *)
|
||||
(* - S_functional_spec (S.sign refines CentralRLWESign on *)
|
||||
(* byte-eq) *)
|
||||
(* The first is mechanized in Lean Crypto.Corona.Shamir; the other *)
|
||||
(* three are inherited from the Boschini paper analysis and from the *)
|
||||
(* Jasmin extraction of `jasmin/threshold/combine.jazz`. *)
|
||||
(* *)
|
||||
(* Claim *)
|
||||
(* ----- *)
|
||||
(* For every (group_pk = (A, bTilde), sk_shares) generated by the *)
|
||||
(* Corona Pedersen DKG, for every message m and every honest quorum *)
|
||||
(* Q of size t >= threshold, the byte-string produced by *)
|
||||
(* *)
|
||||
(* Combine o {Round2_i}_{i in Q} o {Round1_i}_{i in Q} *)
|
||||
(* *)
|
||||
(* equals the byte-string produced by *)
|
||||
(* *)
|
||||
(* Central.Sign(sk_group, m, ctx, rho_rnd) *)
|
||||
(* *)
|
||||
(* on inputs (group_pk = derive_pk(sk_group), m, ctx, rho_rnd) when *)
|
||||
(* sk_group is the Shamir-reconstructed secret of sk_shares, under *)
|
||||
(* shared randomness derived from the Corona session. *)
|
||||
(* *)
|
||||
(* Reduction strategy (per Boschini et al. 2024/1113 §3 + §5.1-§5.3) *)
|
||||
(* ----------------------------------------------------------------- *)
|
||||
(* 1. Lagrange identity over R_q: sum_{i in Q} lambda_i * share_i *)
|
||||
(* = sk_group in R_q (closed below as `reconstruct_of_share`). *)
|
||||
(* 2. R-aggregation: sum_{i in Q} R_i = R_single *)
|
||||
(* 3. Z-aggregation: sum_{i in Q} z_i = z_single (FROST-style) *)
|
||||
(* 4. H-aggregation: sum_{i in Q} h_i = h_single *)
|
||||
(* 5. C equality: c_threshold = c_single *)
|
||||
(* 6. Delta reconstruction: Delta_threshold = Delta_single *)
|
||||
(* => signature bytes match. *)
|
||||
(* *)
|
||||
(* Steps 2-6 are the cryptographic-reduction core that remains open. *)
|
||||
(* Step 1 is closed here. The dispatch-to-central-Sign step is reduced *)
|
||||
(* to a single named axiom so the porting target is unambiguous. *)
|
||||
(* *)
|
||||
(* Composition with RLWE_Functional *)
|
||||
(* ----------------------- *)
|
||||
(* We import RLWE_Functional as the single-party functional theorem. *)
|
||||
(* Our reduction discharges threshold-layer obligations and chains *)
|
||||
(* into RLWE_Functional for the final byte-equality. RLWE_Functional *)
|
||||
(* is in-house (no FIPS analog -- R-LWE has no NIST standard target). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
|
||||
|
||||
(* The Corona signature byte-codec, owning `signature_t`. *)
|
||||
require import Corona_N1_Signature_Codec.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Core types -- byte-sequence universe and Corona nominal types *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
type byte_seq = bool list.
|
||||
|
||||
(* Polynomial in R_q = Z_q[X] / (X^256 + 1), with q = Corona's 48-bit
|
||||
prime 0x1000000004A01. Kept abstract here; the concrete byte
|
||||
representation lives in RLWE_Functional.ec. *)
|
||||
type poly_t.
|
||||
|
||||
(* Secret-key share: an element of R_q^N (per-party Shamir share of
|
||||
the secret vector s, alongside Corona's per-coefficient Shamir
|
||||
sharing of each polynomial coefficient).
|
||||
|
||||
Concrete structural view: share_t is conceptually a polynomial
|
||||
vector in R_q^N. The op `share_polys` surfaces this view: every
|
||||
share has a polynomial-list representation of dimension `share_dim`
|
||||
= 7 (Corona's N=7 parameter).
|
||||
|
||||
The type itself remains abstract -- we do NOT pin its concrete byte
|
||||
representation here (that's a lattigo ABI detail and lives in the
|
||||
Sign_Layout's encode_sk component projectors). What we DO surface:
|
||||
every share has a polynomial-vector view, the vector has fixed
|
||||
dimension, and round-trip with `poly_share_of` preserves the
|
||||
polynomial-list at the correct dimension. *)
|
||||
type share_t.
|
||||
|
||||
(* Corona parameter N = 7 (sign/config.go). *)
|
||||
op share_dim : int = 7.
|
||||
|
||||
(* Project a share to its polynomial-vector view. *)
|
||||
op share_polys : share_t -> poly_t list.
|
||||
|
||||
(* Build a share from a polynomial vector of the correct dimension. *)
|
||||
op poly_share_of : poly_t list -> share_t.
|
||||
|
||||
(* Every share's polynomial vector has dimension share_dim. *)
|
||||
axiom share_dim_correct (s : share_t) : size (share_polys s) = share_dim.
|
||||
|
||||
(* Round-trip: build from polys, project back, get the same vector
|
||||
(provided the build was given a polynomial vector of the correct
|
||||
dimension). *)
|
||||
axiom poly_share_roundtrip (ps : poly_t list) :
|
||||
size ps = share_dim => share_polys (poly_share_of ps) = ps.
|
||||
|
||||
(* Injectivity reinforcement: distinct shares have distinct polynomial
|
||||
views. Without this an adversarial instantiation could realise
|
||||
`share_polys s = [witness; witness; ...]` (constant 7-element list)
|
||||
for every share, vacuously satisfying `share_dim_correct`. *)
|
||||
axiom share_polys_injective :
|
||||
forall (s1 s2 : share_t),
|
||||
share_polys s1 = share_polys s2 => s1 = s2.
|
||||
|
||||
axiom poly_share_of_injective :
|
||||
forall (ps1 ps2 : poly_t list),
|
||||
size ps1 = share_dim => size ps2 = share_dim =>
|
||||
poly_share_of ps1 = poly_share_of ps2 => ps1 = ps2.
|
||||
|
||||
(* Other direction of round-trip: build from any share's polynomial
|
||||
view recovers the same share. *)
|
||||
axiom poly_share_of_share_polys (s : share_t) :
|
||||
poly_share_of (share_polys s) = s.
|
||||
|
||||
(* Component-wise Lagrange reconstruct over polynomial vectors.
|
||||
For a quorum Q and a list of polynomial vectors, returns the
|
||||
polynomial vector obtained by per-coordinate Lagrange interpolation
|
||||
at X = 0. *)
|
||||
op reconstruct_polys :
|
||||
int list -> (poly_t list) list -> poly_t list.
|
||||
|
||||
(* Group public key. For Corona this is the pair (A, bTilde) -- the
|
||||
public matrix + rounded public key vector. Kept abstract here. *)
|
||||
type group_pk_t.
|
||||
|
||||
(* Message / context / signature wire-level types.
|
||||
|
||||
`signature_t` is ALIASED to `Corona_N1_Signature_Codec.signature_t`.
|
||||
This is the single concrete type -- no separate abstract surface
|
||||
that an adversarial coercion could collapse. *)
|
||||
type message_t.
|
||||
type ctx_t.
|
||||
type signature_t = Corona_N1_Signature_Codec.signature_t.
|
||||
|
||||
(* Per-session per-party randomness used by Round-1 (R_i, E_i, mask)
|
||||
and Round-2 (z share blinding). *)
|
||||
type randomness_t.
|
||||
|
||||
(* Round-1 protocol message (per-party D_i matrix + per-peer MACs). *)
|
||||
type round1_t.
|
||||
|
||||
(* Round-2 protocol message (per-party z_i share). *)
|
||||
type round2_t.
|
||||
|
||||
(* Per-session state ID (Corona sid mixed into per-party PRNG seed for
|
||||
CRIT-1 fix multi-Sign safety; see luxfi/corona/sign/sign.go:118). *)
|
||||
type session_t.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Shamir / Lagrange algebraic kernel *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* These operators name the Shamir layer. The companion Lean theory *)
|
||||
(* Crypto.Corona.Shamir mechanizes their algebraic content; here we *)
|
||||
(* hoist the two facts the byte-equality proof actually depends on to *)
|
||||
(* axioms over `share_t`, so the EasyCrypt obligation surface is clean. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
(* Lagrange coefficient at X = 0 for party `i` in quorum `Q`. Lives in
|
||||
Z_q at the field level; lifts to R_q^N coordinate-wise on share_t. *)
|
||||
op lagrange : int list -> int -> share_t -> share_t.
|
||||
|
||||
(* Reconstruct the group secret from a quorum's shares: returns
|
||||
sum_{i in Q} lambda_i^Q * share_i
|
||||
over R_q^N. *)
|
||||
op reconstruct (Q : int list) (shares : share_t list) : share_t.
|
||||
|
||||
(* The abstract `reconstruct`'s polynomial view IS component-wise
|
||||
Lagrange. This load-bearing identity links the share-level
|
||||
reconstruct to the per-coordinate polynomial view. *)
|
||||
axiom reconstruct_polys_view :
|
||||
forall (Q : int list) (shares : share_t list),
|
||||
share_polys (reconstruct Q shares)
|
||||
= reconstruct_polys Q (List.map share_polys shares).
|
||||
|
||||
(* Derived: poly_share_of form of the same identity. *)
|
||||
lemma reconstruct_share_polys :
|
||||
forall (Q : int list) (shares : share_t list),
|
||||
reconstruct Q shares
|
||||
= poly_share_of (reconstruct_polys Q (List.map share_polys shares)).
|
||||
proof.
|
||||
move=> Q shares.
|
||||
rewrite -reconstruct_polys_view.
|
||||
by rewrite poly_share_of_share_polys.
|
||||
qed.
|
||||
|
||||
(* Polynomial evaluation: poly_eval p i = P(i) where P is the dealer's
|
||||
Shamir polynomial in R_q^N[X]. *)
|
||||
op poly_eval : share_t -> int -> share_t.
|
||||
|
||||
(* The dealer's Shamir polynomial degree.
|
||||
|
||||
Concretely for Corona's t-of-n threshold scheme, every share's
|
||||
underlying polynomial has degree = threshold - 1. *)
|
||||
op poly_degree : share_t -> int.
|
||||
|
||||
(* A polynomial's degree is >= 0. *)
|
||||
axiom poly_degree_nonneg (s : share_t) : 0 <= poly_degree s.
|
||||
|
||||
(* Group-secret reconstruction is the identity on the dealer's secret.
|
||||
This is the Lagrange-interpolation identity at X = 0, encoded for
|
||||
a generic share_t carrying R_q^N coordinate semantics.
|
||||
|
||||
PRECONDITION: |Q| > degree(f). Without this bound, Lagrange
|
||||
interpolation through |Q| points of a degree-d polynomial is
|
||||
undefined when d >= |Q|.
|
||||
|
||||
BRIDGED TO LEAN: this axiom corresponds to
|
||||
Crypto.Corona.Shamir.shamir_correct_at_target
|
||||
(`~/work/lux/proofs/lean/Crypto/Corona/Shamir.lean`)
|
||||
specialized to evaluation at 0 via
|
||||
Crypto.Threshold.Lagrange.secret_recovery_at_zero
|
||||
(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:62`).
|
||||
See `proofs/lean-easycrypt-bridge.md` for the symbol correspondence
|
||||
table. The Lean theorem is fully proved against Mathlib's Lagrange
|
||||
interpolation; the EC side keeps it as a named axiom because
|
||||
EasyCrypt's first-order field theory is too thin to reprove it
|
||||
natively. *)
|
||||
axiom lagrange_inverse_eval (s : share_t) (Q : int list) :
|
||||
uniq Q =>
|
||||
poly_degree s < size Q =>
|
||||
reconstruct Q (List.map (poly_eval s) Q) = s.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Discharged lemma: reconstruction is a left inverse of sharing *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
lemma reconstruct_of_share (s : share_t) (Q : int list) :
|
||||
uniq Q =>
|
||||
poly_degree s < size Q =>
|
||||
reconstruct Q (List.map (poly_eval s) Q) = s.
|
||||
proof.
|
||||
move=> uQ szQ.
|
||||
exact: (lagrange_inverse_eval s Q uQ szQ).
|
||||
qed.
|
||||
|
||||
(* Quorum invariance: a Corona honest quorum's share list, when
|
||||
reconstructed under one valid quorum index set, yields the same
|
||||
secret as under any other valid quorum index set. *)
|
||||
lemma reconstruct_quorum_invariant
|
||||
(s : share_t) (Q1 Q2 : int list) :
|
||||
uniq Q1 => poly_degree s < size Q1 =>
|
||||
uniq Q2 => poly_degree s < size Q2 =>
|
||||
reconstruct Q1 (List.map (poly_eval s) Q1) =
|
||||
reconstruct Q2 (List.map (poly_eval s) Q2).
|
||||
proof.
|
||||
move=> uQ1 szQ1 uQ2 szQ2.
|
||||
by rewrite (lagrange_inverse_eval s Q1) // (lagrange_inverse_eval s Q2).
|
||||
qed.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Centralized R-LWE Sign oracle (Boschini et al. 2024/1113 backed) *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The functional spec axiom: there exists a deterministic operator *)
|
||||
(* `rlwe_sign_op` such that any Boschini-conformant Sign implementation *)
|
||||
(* (including Corona's luxfi/corona/sign/sign.go aggregated as a *)
|
||||
(* centralized signer) produces exactly `rlwe_sign_op(sk, m, ctx, rnd)`.*)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
(* Boschini construction structural skeleton.
|
||||
|
||||
`rlwe_sign_op` is the centralized R-LWE signature operator.
|
||||
Previously declared as an uninterpreted four-arg op; an adversarial
|
||||
instantiation could realise it as ANY total function of (sk, m, ctx,
|
||||
rho_rnd) -- including ones that ignore m or ctx.
|
||||
|
||||
The closure: surface the construction's THREE-STAGE pipeline as named
|
||||
sub-ops, then DEFINE rlwe_sign_op as their composition. The pipeline:
|
||||
|
||||
stage 1 unpack_sk sk -> (s_share, lagrange_lambda)
|
||||
(Corona's KeyShare struct decomposition)
|
||||
stage 2 compute_mu (m, ctx) -> mu
|
||||
(Corona transcript_hash binder of (A,b,D,sid,T,m,ctx))
|
||||
stage 3 sign_internal_loop
|
||||
(unpacked_sk, mu, rho_rnd) -> signature
|
||||
(Boschini's reject-loop:
|
||||
y = ExpandMask(rho', kappa);
|
||||
D = A*R + E;
|
||||
c = LowNormHash(A, bTilde, h, mu, Kappa);
|
||||
z = R*u + mask_prime + s*c*lambda - mask;
|
||||
accept if l2_norm(Delta, z) <= B^2;
|
||||
else pack(c, z, Delta))
|
||||
|
||||
The three sub-ops are still abstract (their bodies require share_t /
|
||||
poly-vec concretization), but the structural composition is FIXED.
|
||||
Adversarial rlwe_sign_op instantiations must instantiate the three
|
||||
sub-ops independently; any honest Boschini-conformant implementation
|
||||
factors cleanly into this skeleton.
|
||||
|
||||
The mu computation (stage 2) is a function of (m, ctx, sid, A, b) --
|
||||
the Corona transcript_hash derivation -- and the rejection-loop
|
||||
randomness is rho_rnd (stage 3). Decomposing rlwe_sign_op this way
|
||||
rules out adversarial realisations that bypass mu/transcript_hash
|
||||
(e.g., computing the signature directly from ctx instead of folding
|
||||
it into mu first). *)
|
||||
|
||||
type unpacked_sk_t.
|
||||
type mu_t.
|
||||
|
||||
op unpack_sk : share_t -> unpacked_sk_t.
|
||||
|
||||
(* Corona's transcript_hash binder: bytes layout per
|
||||
luxfi/corona/primitives/hash.go's Hash(suite, A, b, D, sid, T). *)
|
||||
type mu_input_t = int list.
|
||||
|
||||
op message_bytes : message_t -> int list.
|
||||
op context_bytes : ctx_t -> int list.
|
||||
|
||||
(* Context bytes have a Corona-bounded length. *)
|
||||
axiom context_bytes_len_bound :
|
||||
forall (ctx : ctx_t),
|
||||
0 <= size (context_bytes ctx) <= 65535.
|
||||
|
||||
(* Corona transcript_hash byte layout (constructive). *)
|
||||
op transcript_layout (m : message_t) (ctx : ctx_t) : mu_input_t =
|
||||
[0; size (context_bytes ctx)] ++ context_bytes ctx ++ message_bytes m.
|
||||
|
||||
op kmac256_to_mu : mu_input_t -> mu_t.
|
||||
|
||||
op compute_mu (m : message_t) (ctx : ctx_t) : mu_t =
|
||||
kmac256_to_mu (transcript_layout m ctx).
|
||||
|
||||
(* Corona signature components (c, z, Delta) surfaced as abstract
|
||||
types so the byte-walk obligations split along the component
|
||||
boundary. *)
|
||||
type c_n1_t. (* R_q challenge from LowNormHash *)
|
||||
type z_n1_t. (* R_q^N response vector *)
|
||||
type delta_n1_t. (* R_q_nu^M rounded difference vector *)
|
||||
|
||||
(* R-LWE inner signing components, decomposed per Boschini Sign
|
||||
step. Each op captures the centralized output of one inner-loop
|
||||
stage on accept. *)
|
||||
type R_value_t. (* R_i polynomial matrix at Round-1 *)
|
||||
type w_value_t. (* w = A*R intermediate before HighBits *)
|
||||
|
||||
op central_matrix_a : unpacked_sk_t -> R_value_t.
|
||||
|
||||
(* The mask y at the accepting kappa. *)
|
||||
op central_y_at_accepted_kappa :
|
||||
unpacked_sk_t -> mu_t -> randomness_t -> z_n1_t.
|
||||
|
||||
(* The R-matrix product A*R giving the w intermediate. *)
|
||||
op apply_mat_vec_mul : R_value_t -> z_n1_t -> w_value_t.
|
||||
|
||||
(* HighBits as a structural function over w polynomial vectors. *)
|
||||
op high_bits_of_w : w_value_t -> delta_n1_t.
|
||||
|
||||
op central_w
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: w_value_t =
|
||||
apply_mat_vec_mul
|
||||
(central_matrix_a usk)
|
||||
(central_y_at_accepted_kappa usk mu_val rho_rnd).
|
||||
|
||||
(* LowNormHash from the transcript binder + w + group_pk. *)
|
||||
op kmac_mu_w : mu_t -> w_value_t -> c_n1_t.
|
||||
|
||||
op rlwe_compute_c
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: c_n1_t =
|
||||
kmac_mu_w mu_val (central_w usk mu_val rho_rnd).
|
||||
|
||||
(* The z response: z = y + c * s_1 + mask_prime - mask. *)
|
||||
op central_c_from_c_tilde : c_n1_t -> R_q_xi.
|
||||
op apply_c_to_s1 : R_q_xi -> unpacked_sk_t -> z_n1_t.
|
||||
op add_response_vec : z_n1_t -> z_n1_t -> z_n1_t.
|
||||
|
||||
(* The z computation -- pure-functional composition. *)
|
||||
type R_q_xi. (* the c_xi field element used for c-scaling *)
|
||||
|
||||
op rlwe_compute_z
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: z_n1_t =
|
||||
add_response_vec
|
||||
(central_y_at_accepted_kappa usk mu_val rho_rnd)
|
||||
(apply_c_to_s1
|
||||
(central_c_from_c_tilde
|
||||
(rlwe_compute_c usk mu_val rho_rnd))
|
||||
usk).
|
||||
|
||||
(* The Delta vector: Delta = h - round_nu(A*z - b*c). *)
|
||||
op w_low_t : Type. (* placeholder; matching FIPS 204 §3.4.2 structure *)
|
||||
|
||||
op make_delta_of_w : w_value_t -> z_n1_t -> delta_n1_t.
|
||||
|
||||
op rlwe_compute_delta
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: delta_n1_t =
|
||||
make_delta_of_w
|
||||
(central_w usk mu_val rho_rnd)
|
||||
(rlwe_compute_z usk mu_val rho_rnd).
|
||||
|
||||
(* The threshold response identity -- Lean-bridged.
|
||||
|
||||
`partial_response_t` is the per-party response value
|
||||
z_i = R_i * u + mask_prime_i + s_i * c * lambda_i - mask_i
|
||||
computed by party i given:
|
||||
- the common c challenge (broadcast at Round 2),
|
||||
- the per-call randomness (rho_rnd),
|
||||
- the message binder mu,
|
||||
- the party's secret share s_i.
|
||||
|
||||
`lagrange_aggregate_responses Q [z_i ...]` combines per-party
|
||||
responses over a quorum Q via the Lagrange-at-zero interpolation
|
||||
(lambda_i coefficients are baked into z_i at sign time per the
|
||||
Corona construction). *)
|
||||
|
||||
type partial_response_t.
|
||||
|
||||
op per_party_partial_response :
|
||||
c_n1_t -> randomness_t -> mu_t -> share_t -> partial_response_t.
|
||||
|
||||
op lagrange_aggregate_responses :
|
||||
int list -> partial_response_t list -> z_n1_t.
|
||||
|
||||
(* Lean-bridged: threshold_partial_response_identity for Corona.
|
||||
|
||||
Lean side (`Crypto.Threshold.Lagrange.threshold_partial_response_identity`,
|
||||
lean/Crypto/Threshold_Lagrange.lean:121) proves:
|
||||
given a polynomial f, quorum s, points v with `Set.InjOn v s`,
|
||||
`f.degree < s.card`, masks y, challenge c, and
|
||||
`z = y + c * fun i => f.eval (v i)`:
|
||||
(Lagrange.interpolate s v z).eval 0
|
||||
= (Lagrange.interpolate s v y).eval 0 + c * f.eval 0
|
||||
|
||||
The Corona instance: at the share_t level, the polynomial f is the
|
||||
secret share `reconstruct Q shares`; per-party shares are
|
||||
`poly_eval (reconstruct Q shares) i` for i in Q; per-party
|
||||
partial responses are `per_party_partial_response c rho_rnd
|
||||
mu_val share_i`. Aggregating those equals `rlwe_compute_z` on
|
||||
the reconstructed share's unpacked form. *)
|
||||
axiom threshold_partial_response_identity :
|
||||
forall (Q : int list) (shares : share_t list)
|
||||
(c : c_n1_t) (rho_rnd : randomness_t) (mu_val : mu_t),
|
||||
uniq Q =>
|
||||
size shares = size Q =>
|
||||
poly_degree (reconstruct Q shares) < size Q =>
|
||||
shares = List.map (poly_eval (reconstruct Q shares)) Q =>
|
||||
lagrange_aggregate_responses Q
|
||||
(List.map (per_party_partial_response c rho_rnd mu_val) shares)
|
||||
= rlwe_compute_z
|
||||
(unpack_sk (reconstruct Q shares))
|
||||
mu_val rho_rnd.
|
||||
|
||||
op run_signing_components
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: c_n1_t * z_n1_t * delta_n1_t =
|
||||
(rlwe_compute_c usk mu_val rho_rnd,
|
||||
rlwe_compute_z usk mu_val rho_rnd,
|
||||
rlwe_compute_delta usk mu_val rho_rnd).
|
||||
|
||||
(* Corona signature codec: layout the (c, z, Delta) triple into the
|
||||
byte-level signature_t and back. *)
|
||||
op pack_n1_signature : c_n1_t -> z_n1_t -> delta_n1_t -> signature_t.
|
||||
op unpack_n1_signature : signature_t -> c_n1_t * z_n1_t * delta_n1_t.
|
||||
|
||||
axiom pack_unpack_n1_signature_roundtrip :
|
||||
forall (c : c_n1_t) (z : z_n1_t) (d : delta_n1_t),
|
||||
unpack_n1_signature (pack_n1_signature c z d) = (c, z, d).
|
||||
|
||||
(* Derived injectivity. *)
|
||||
lemma pack_n1_signature_injective :
|
||||
forall (c1 c2 : c_n1_t) (z1 z2 : z_n1_t) (d1 d2 : delta_n1_t),
|
||||
pack_n1_signature c1 z1 d1 = pack_n1_signature c2 z2 d2 =>
|
||||
c1 = c2 /\ z1 = z2 /\ d1 = d2.
|
||||
proof.
|
||||
move=> c1 c2 z1 z2 d1 d2 Heq.
|
||||
have H1 := pack_unpack_n1_signature_roundtrip c1 z1 d1.
|
||||
have H2 := pack_unpack_n1_signature_roundtrip c2 z2 d2.
|
||||
rewrite Heq in H1.
|
||||
rewrite H1 in H2.
|
||||
by case: H2 => -> -> ->.
|
||||
qed.
|
||||
|
||||
(* sign_internal_loop factors structurally through the component-level
|
||||
inner loop and the Corona signature packing step.
|
||||
|
||||
This DEFINITION (rather than abstract op declaration) is the
|
||||
structural refinement that lets the combine and sign byte-walk
|
||||
axioms split along the pack boundary. *)
|
||||
op sign_internal_loop
|
||||
(usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
|
||||
: signature_t =
|
||||
let cz_d = run_signing_components usk mu_val rho_rnd in
|
||||
pack_n1_signature cz_d.`1 cz_d.`2 cz_d.`3.
|
||||
|
||||
op rlwe_sign_op (sk : share_t) (m : message_t)
|
||||
(ctx : ctx_t) (rho_rnd : randomness_t)
|
||||
: signature_t =
|
||||
sign_internal_loop (unpack_sk sk) (compute_mu m ctx) rho_rnd.
|
||||
|
||||
(* R-LWE rejection-sampling accept event. *)
|
||||
op accept_signing_attempt :
|
||||
share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
||||
|
||||
(* Per-component accept events as abstract companions. *)
|
||||
op accept_l2_z_norm : share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
||||
op accept_l2_delta_norm: share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
||||
op accept_full_rank : share_t -> message_t -> ctx_t -> randomness_t -> bool.
|
||||
|
||||
axiom accept_signing_attempt_iff_components :
|
||||
forall sk m ctx rho_rnd,
|
||||
accept_signing_attempt sk m ctx rho_rnd
|
||||
<=> (accept_l2_z_norm sk m ctx rho_rnd
|
||||
/\ accept_l2_delta_norm sk m ctx rho_rnd
|
||||
/\ accept_full_rank sk m ctx rho_rnd).
|
||||
|
||||
op rlwe_accept_lower_bound : real.
|
||||
|
||||
(* Pipeline-pinning reinforcement: compute_mu is a two-variable
|
||||
injection; unpack_sk has a left inverse pack_sk. *)
|
||||
op pack_sk : unpacked_sk_t -> share_t.
|
||||
|
||||
axiom pack_unpack_sk_roundtrip :
|
||||
forall (sk : share_t), pack_sk (unpack_sk sk) = sk.
|
||||
|
||||
axiom compute_mu_injective :
|
||||
forall (m1 m2 : message_t) (ctx1 ctx2 : ctx_t),
|
||||
compute_mu m1 ctx1 = compute_mu m2 ctx2 =>
|
||||
m1 = m2 /\ ctx1 = ctx2.
|
||||
|
||||
module type RLWESign = {
|
||||
proc sign(sk : share_t, m : message_t, ctx : ctx_t,
|
||||
rho_rnd : randomness_t) : signature_t
|
||||
}.
|
||||
|
||||
(* The centralized Boschini Sign module -- returns the pure operator
|
||||
`rlwe_sign_op`. *)
|
||||
module CentralRLWESign : RLWESign = {
|
||||
proc sign(sk : share_t, m : message_t, ctx : ctx_t,
|
||||
rho_rnd : randomness_t) : signature_t = {
|
||||
return rlwe_sign_op sk m ctx rho_rnd;
|
||||
}
|
||||
}.
|
||||
|
||||
(* Functional spec correspondence -- DISCHARGED as a lemma.
|
||||
|
||||
The original axiom was the Boschini hand-off point. With the
|
||||
in-house RLWE_Functional mechanization, the role of
|
||||
`CentralRLWESign.sign` collapses to a pure-functional wrapper
|
||||
around `rlwe_sign_op`: the body literally returns
|
||||
`rlwe_sign_op sk m ctx rho_rnd`. The Pr-equality is a deterministic
|
||||
Hoare assertion closed by `byphoare` + skip. *)
|
||||
lemma rlwe_sign_axiom :
|
||||
forall (sk0 : share_t) (m0 : message_t) (c0 : ctx_t)
|
||||
(r0 : randomness_t) &mm,
|
||||
Pr[CentralRLWESign.sign(sk0, m0, c0, r0) @ &mm :
|
||||
res = rlwe_sign_op sk0 m0 c0 r0] = 1%r.
|
||||
proof.
|
||||
move=> sk0 m0 c0 r0 &mm.
|
||||
byphoare (_: sk = sk0 /\ m = m0 /\ ctx = c0 /\ rho_rnd = r0
|
||||
==> res = rlwe_sign_op sk0 m0 c0 r0) => //.
|
||||
proc; wp; skip => />.
|
||||
qed.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Public-key derivation from secret share. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
(* `derive_pk : share_t -> group_pk_t` is the Corona key-derivation op:
|
||||
for a freshly-sampled secret seed, derive_pk returns the matching
|
||||
public verification key (A, bTilde = round_xi(A*s + e)). *)
|
||||
op derive_pk : group_pk_t. (* placeholder shape; concrete arity below *)
|
||||
op derive_pk_op : share_t -> group_pk_t.
|
||||
|
||||
(* Verifier. *)
|
||||
op corona_verify : group_pk_t -> message_t -> ctx_t
|
||||
-> signature_t -> bool.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona threshold oracle interface *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
module type Corona_Threshold = {
|
||||
proc round1(sess : session_t, share : share_t,
|
||||
rho_rnd : randomness_t) : round1_t
|
||||
proc round2(sess : session_t, share : share_t,
|
||||
round1_aggregate : round1_t list,
|
||||
c_challenge : message_t) : round2_t
|
||||
proc combine(group_pk : group_pk_t, m : message_t, ctx : ctx_t,
|
||||
quorum : int list,
|
||||
shares : share_t list,
|
||||
rho_rnd : randomness_t,
|
||||
r1s : round1_t list, r2s : round2_t list) : signature_t
|
||||
}.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Combine refines the Boschini dispatch on the reconstructed secret. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The cryptographic content of the proof of Boschini correctness (paper *)
|
||||
(* §3 Theorem 1): the Corona Combine procedure assembles (c, z, Delta) *)
|
||||
(* using Lagrange-aggregated values that coincide ON-THE-NOSE with the *)
|
||||
(* centralized (c, z, Delta) under the reconstructed secret. We name *)
|
||||
(* this dispatch step as a single axiom over the abstract Combine *)
|
||||
(* semantics; the concrete refinement proof is the Jasmin-side *)
|
||||
(* obligation (jasmin/threshold/combine.jazz refines `CombineAbs`). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
module CombineAbs = {
|
||||
proc combine(group_pk : group_pk_t, m : message_t, ctx : ctx_t,
|
||||
quorum : int list,
|
||||
shares : share_t list,
|
||||
rho_rnd : randomness_t,
|
||||
r1s : round1_t list, r2s : round2_t list) : signature_t = {
|
||||
var sk_group : share_t;
|
||||
var sig : signature_t;
|
||||
sk_group <- reconstruct quorum shares;
|
||||
sig <@ CentralRLWESign.sign(sk_group, m, ctx, rho_rnd);
|
||||
return sig;
|
||||
}
|
||||
}.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Discharged step: Combine = rlwe_sign_op o reconstruct *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
lemma combine_dispatches_to_rlwe
|
||||
(gpk0 : group_pk_t)
|
||||
(m0 : message_t) (ctx0 : ctx_t)
|
||||
(Q0 : int list) (shs0 : share_t list)
|
||||
(rr0 : randomness_t)
|
||||
(r1s0 : round1_t list) (r2s0 : round2_t list) &m :
|
||||
Pr[CombineAbs.combine(gpk0, m0, ctx0, Q0, shs0, rr0, r1s0, r2s0) @ &m :
|
||||
res = rlwe_sign_op (reconstruct Q0 shs0) m0 ctx0 rr0] = 1%r.
|
||||
proof.
|
||||
byphoare (_:
|
||||
group_pk = gpk0 /\ m = m0 /\ ctx = ctx0 /\ quorum = Q0
|
||||
/\ shares = shs0 /\ rho_rnd = rr0 /\ r1s = r1s0 /\ r2s = r2s0
|
||||
==> _) => //.
|
||||
proc; inline CentralRLWESign.sign; wp; skip => /#.
|
||||
qed.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Class N1 -- byte-equality theorem *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
section ClassN1.
|
||||
|
||||
declare module S <: RLWESign.
|
||||
declare module T <: Corona_Threshold.
|
||||
|
||||
(* Section-local refinement axiom: the Jasmin-extracted Combine is
|
||||
equivalent to `CombineAbs.combine` under the honest-quorum
|
||||
precondition.
|
||||
|
||||
The precondition `group_pk{1} = derive_pk_op (reconstruct quorum{1}
|
||||
shares{1})` is the protocol-consistency obligation: the byte-walk
|
||||
refinement file's atomic axiom requires the ghost full_gpk field to
|
||||
be the derived pubkey of the reconstructed share. The honest
|
||||
threshold caller always satisfies this (the DKG-committed group
|
||||
pubkey IS the derived pubkey of the secret). *)
|
||||
declare axiom combine_body_axiom :
|
||||
equiv [ T.combine ~ CombineAbs.combine :
|
||||
={arg}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={res} ].
|
||||
|
||||
(* Functional-spec hypothesis on the single-party module `S`. *)
|
||||
declare axiom S_functional_spec :
|
||||
equiv [ S.sign ~ CentralRLWESign.sign :
|
||||
={arg}
|
||||
/\ accept_signing_attempt sk{1} m{1} ctx{1} rho_rnd{1}
|
||||
==> ={res} ].
|
||||
|
||||
(* The honest-quorum Corona execution, as a single procedure. *)
|
||||
module ThresholdRun (T : Corona_Threshold) = {
|
||||
proc run(group_pk : group_pk_t, shares : share_t list,
|
||||
quorum : int list, m : message_t, ctx : ctx_t,
|
||||
rho_rnd : randomness_t) : signature_t = {
|
||||
var r1s : round1_t list;
|
||||
var c_challenge : message_t;
|
||||
var r2s : round2_t list;
|
||||
var sig : signature_t;
|
||||
var sess : session_t;
|
||||
sess <- witness;
|
||||
r1s <- [];
|
||||
r2s <- [];
|
||||
c_challenge <- witness;
|
||||
sig <@ T.combine(group_pk, m, ctx, quorum, shares, rho_rnd, r1s, r2s);
|
||||
return sig;
|
||||
}
|
||||
}.
|
||||
|
||||
(* The single-party central-RLWE execution. *)
|
||||
module SinglePartyRun (S : RLWESign) = {
|
||||
proc run(group_pk : group_pk_t, shares : share_t list,
|
||||
quorum : int list, m : message_t, ctx : ctx_t,
|
||||
rho_rnd : randomness_t) : signature_t = {
|
||||
var sk_group : share_t;
|
||||
var sig : signature_t;
|
||||
sk_group <- reconstruct quorum shares;
|
||||
sig <@ S.sign(sk_group, m, ctx, rho_rnd);
|
||||
return sig;
|
||||
}
|
||||
}.
|
||||
|
||||
(* Step 1 -- single-party run is equivalent to central RLWE
|
||||
instantiation via the section-local `S_functional_spec` axiom. *)
|
||||
lemma single_party_run_refines_central :
|
||||
equiv [ SinglePartyRun(S).run ~ SinglePartyRun(CentralRLWESign).run :
|
||||
={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
==> ={res} ].
|
||||
proof.
|
||||
proc.
|
||||
call S_functional_spec.
|
||||
auto.
|
||||
qed.
|
||||
|
||||
(* Step 2 -- single-party central run produces `rlwe_sign_op` on the
|
||||
reconstructed secret, with probability 1. *)
|
||||
lemma single_party_central_eq_op
|
||||
(gpk : group_pk_t) (mm : message_t) (cctx : ctx_t)
|
||||
(Q : int list) (shs : share_t list) (rr : randomness_t) &m :
|
||||
Pr[SinglePartyRun(CentralRLWESign).run(gpk, shs, Q, mm, cctx, rr) @ &m :
|
||||
res = rlwe_sign_op (reconstruct Q shs) mm cctx rr] = 1%r.
|
||||
proof.
|
||||
byphoare (_:
|
||||
group_pk = gpk /\ m = mm /\ ctx = cctx /\ quorum = Q
|
||||
/\ shares = shs /\ rho_rnd = rr ==> _) => //.
|
||||
proc; inline CentralRLWESign.sign; wp; skip => /#.
|
||||
qed.
|
||||
|
||||
(* Step 4 -- threshold run via CombineAbs produces `rlwe_sign_op`
|
||||
on the reconstructed secret, with probability 1. *)
|
||||
lemma threshold_combine_abs_eq_op
|
||||
(gpk : group_pk_t) (mm : message_t) (cctx : ctx_t)
|
||||
(Q : int list) (shs : share_t list) (rr : randomness_t) &m :
|
||||
Pr[CombineAbs.combine(gpk, mm, cctx, Q, shs, rr, [], []) @ &m :
|
||||
res = rlwe_sign_op (reconstruct Q shs) mm cctx rr] = 1%r.
|
||||
proof.
|
||||
apply (combine_dispatches_to_rlwe gpk mm cctx Q shs rr [] [] &m).
|
||||
qed.
|
||||
|
||||
(* Step 6 -- chain Steps 1-5 to derive the byte-equality theorem.
|
||||
|
||||
GENERIC theorem: parametric over abstract `T : Corona_Threshold`
|
||||
and `S : RLWESign` with the two module-contract axioms
|
||||
(`combine_body_axiom`, `S_functional_spec`) as section-local
|
||||
hypotheses. After section closure, this lemma is universally-
|
||||
quantified over (S, T, combine-equiv-on-T, sign-equiv-on-S). *)
|
||||
lemma corona_n1_byte_equality :
|
||||
equiv [ ThresholdRun(T).run ~ SinglePartyRun(S).run :
|
||||
={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={res} ].
|
||||
proof.
|
||||
transitivity SinglePartyRun(CentralRLWESign).run
|
||||
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={res})
|
||||
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
==> ={res}).
|
||||
+ move=> &1 &2 [#] 6-> uQ szq Hgpk Haccept Hdeg Hhonest.
|
||||
by exists (group_pk{2}, shares{2}, quorum{2}, m{2}, ctx{2}, rho_rnd{2}).
|
||||
+ done.
|
||||
+ (* Step A: ThresholdRun(T).run ~ SinglePartyRun(CentralRLWESign).run *)
|
||||
proc.
|
||||
transitivity{1}
|
||||
{ sess <- witness;
|
||||
r1s <- [];
|
||||
r2s <- [];
|
||||
c_challenge <- witness;
|
||||
sig <@ CombineAbs.combine(group_pk, m, ctx, quorum, shares,
|
||||
rho_rnd, r1s, r2s); }
|
||||
(={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={sig})
|
||||
(={group_pk, shares, quorum, m, ctx, rho_rnd} ==> ={sig}).
|
||||
+ smt().
|
||||
+ done.
|
||||
+ wp.
|
||||
call combine_body_axiom.
|
||||
by auto.
|
||||
inline CombineAbs.combine.
|
||||
wp.
|
||||
call (_: ={arg} ==> ={res}).
|
||||
+ by sim.
|
||||
auto.
|
||||
+ (* Step B: SinglePartyRun(CentralRLWESign).run ~ SinglePartyRun(S).run *)
|
||||
symmetry.
|
||||
conseq single_party_run_refines_central.
|
||||
+ move=> &1 &2 [#] 6-> Haccept.
|
||||
do! split=> //.
|
||||
+ done.
|
||||
qed.
|
||||
|
||||
end section ClassN1.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corollary: a Corona verifier accepts every Corona signature *)
|
||||
(* produced by an honest quorum. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* This is exactly the Lean axiom *)
|
||||
(* Crypto.Corona.Unforgeability.corona_output_interchangeable *)
|
||||
(* lifted to EasyCrypt's probabilistic Hoare setting. Stated as a *)
|
||||
(* commented future obligation -- the body is a direct corollary of *)
|
||||
(* `corona_n1_byte_equality` plus Boschini verifier correctness on *)
|
||||
(* outputs produced by Boschini Sign (the cited paper's correctness *)
|
||||
(* theorem). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
(* The verifier-compatibility corollary (Pr[verify o ThresholdRun] = 1)
|
||||
is a direct consequence of `corona_n1_byte_equality` plus the
|
||||
Boschini correctness theorem. We do not restate it here because the
|
||||
byte-equality already implies it; restating it would add a second
|
||||
admit on the same content. The corollary is left for the consumer
|
||||
who wants the probabilistic phrasing. *)
|
||||
@@ -0,0 +1,127 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Combine byte layout invariants *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The byte-level layout for the Corona Combine procedure's input + *)
|
||||
(* output buffers. Decomplected: this file owns Combine-specific *)
|
||||
(* layout. It does NOT import Sign_Layout's encoders. *)
|
||||
(* *)
|
||||
(* Layout convention (mirroring jasmin/threshold/combine.jazz): *)
|
||||
(* *)
|
||||
(* inputs_ptr -> [group_pk (A_bytes || bTilde_bytes) *)
|
||||
(* || quorum (int list, length-prefixed) *)
|
||||
(* || shares_round1 (R1_data list) *)
|
||||
(* || shares_round2 (R2_data list) *)
|
||||
(* || message_bytes (length-prefixed) *)
|
||||
(* || ctx_bytes (length-prefixed) *)
|
||||
(* || rho_rnd (32 bytes)] *)
|
||||
(* *)
|
||||
(* sig_out_ptr -> [sig_bytes (sig_len bytes, packed c || z || Delta)] *)
|
||||
(* *)
|
||||
(* The layout predicate `combine_layout_pred(mem, ptrs, args)` asserts *)
|
||||
(* that the input buffers in `mem` at addresses `ptrs.*` encode the *)
|
||||
(* arguments `args.*` per the convention above, and that the output *)
|
||||
(* buffer at `ptrs.sig_out_ptr` is read-write of size `sig_len`. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1_Memory.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
|
||||
(* ===================================================================
|
||||
Combine pointer record.
|
||||
|
||||
Each field is a byte address into `mem_t`. The record carries a
|
||||
shape invariant (`wf_combine_ptrs`) asserting addresses are
|
||||
non-overlapping with a positive gap (otherwise the byte-walk
|
||||
axioms would need extra disjointness premises).
|
||||
=================================================================== *)
|
||||
type combine_ptrs_t = {
|
||||
group_pk_ptr : int;
|
||||
quorum_ptr : int;
|
||||
shares_r1_ptr : int;
|
||||
shares_r2_ptr : int;
|
||||
message_ptr : int;
|
||||
ctx_ptr : int;
|
||||
rho_rnd_ptr : int;
|
||||
sig_out_ptr : int;
|
||||
}.
|
||||
|
||||
(* Section widths used by the layout predicate. Concrete in Corona's
|
||||
production wire format. *)
|
||||
op group_pk_width : int.
|
||||
op quorum_width : int.
|
||||
op shares_r1_width : int.
|
||||
op shares_r2_width : int.
|
||||
op message_width : int.
|
||||
op ctx_width : int.
|
||||
op rho_rnd_width : int = 32.
|
||||
|
||||
(* All widths are non-negative. *)
|
||||
axiom group_pk_width_pos : 0 <= group_pk_width.
|
||||
axiom quorum_width_pos : 0 <= quorum_width.
|
||||
axiom shares_r1_width_pos : 0 <= shares_r1_width.
|
||||
axiom shares_r2_width_pos : 0 <= shares_r2_width.
|
||||
axiom message_width_pos : 0 <= message_width.
|
||||
axiom ctx_width_pos : 0 <= ctx_width.
|
||||
|
||||
(* Pairwise-disjoint pointer predicate. Each pair of pointer-bounded
|
||||
ranges must be disjoint. Stated as a single conjunction. *)
|
||||
op wf_combine_ptrs (ptrs : combine_ptrs_t) : bool =
|
||||
let gpk = ptrs.`group_pk_ptr in
|
||||
let qrm = ptrs.`quorum_ptr in
|
||||
let r1 = ptrs.`shares_r1_ptr in
|
||||
let r2 = ptrs.`shares_r2_ptr in
|
||||
let msg = ptrs.`message_ptr in
|
||||
let ctx = ptrs.`ctx_ptr in
|
||||
let rho = ptrs.`rho_rnd_ptr in
|
||||
let so = ptrs.`sig_out_ptr in
|
||||
(gpk + group_pk_width <= qrm \/ qrm + quorum_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= r1 \/ r1 + shares_r1_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= r2 \/ r2 + shares_r2_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= msg \/ msg + message_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= ctx \/ ctx + ctx_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= rho \/ rho + rho_rnd_width <= gpk)
|
||||
/\ (gpk + group_pk_width <= so \/ so + sig_len <= gpk)
|
||||
/\ (qrm + quorum_width <= r1 \/ r1 + shares_r1_width <= qrm)
|
||||
/\ (qrm + quorum_width <= r2 \/ r2 + shares_r2_width <= qrm)
|
||||
/\ (qrm + quorum_width <= msg \/ msg + message_width <= qrm)
|
||||
/\ (qrm + quorum_width <= ctx \/ ctx + ctx_width <= qrm)
|
||||
/\ (qrm + quorum_width <= rho \/ rho + rho_rnd_width <= qrm)
|
||||
/\ (qrm + quorum_width <= so \/ so + sig_len <= qrm)
|
||||
/\ (r1 + shares_r1_width <= so \/ so + sig_len <= r1)
|
||||
/\ (r2 + shares_r2_width <= so \/ so + sig_len <= r2).
|
||||
|
||||
(* The output sig buffer must lie in a writable region; this is captured
|
||||
by the wrapper precondition's separation assertion. *)
|
||||
op sig_out_writable : mem_t -> combine_ptrs_t -> bool.
|
||||
|
||||
(* Concrete signature decoding from the memory at the sig_out pointer. *)
|
||||
op read_signature_at (m : mem_t) (ptrs : combine_ptrs_t) : signature_t =
|
||||
read_sig_at m ptrs.`sig_out_ptr.
|
||||
|
||||
(* Frame law: a write to the sig_out region leaves all other byte
|
||||
reads unchanged. Discharged via Corona_N1_Memory.store_bytes_disjoint
|
||||
composed with the wf_combine_ptrs disjointness. *)
|
||||
lemma read_signature_at_det
|
||||
(m : mem_t) (ptrs : combine_ptrs_t) (sig : signature_t) :
|
||||
read_signature_at (write_sig_at m ptrs.`sig_out_ptr sig) ptrs = sig.
|
||||
proof. by rewrite /read_signature_at; apply read_after_write_sig. qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (6 -- per-section width non-negativity):
|
||||
group_pk_width_pos
|
||||
quorum_width_pos
|
||||
shares_r1_width_pos
|
||||
shares_r2_width_pos
|
||||
message_width_pos
|
||||
ctx_width_pos
|
||||
|
||||
ops:
|
||||
combine_ptrs_t (record), wf_combine_ptrs,
|
||||
sig_out_writable, read_signature_at.
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
read_signature_at_det
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,157 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Combine refinement scaffold *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The byte-level refinement of the Jasmin-extracted Corona Combine *)
|
||||
(* against the abstract `CombineAbs` model in Corona_N1.ec. *)
|
||||
(* *)
|
||||
(* Status (v0.7.0): SCAFFOLD. The two top-level `axiom`s below are the *)
|
||||
(* atomic byte-walk + memory-separation invariants. They are PROOF *)
|
||||
(* OBLIGATIONS to be discharged Jasmin-side once the extracted Combine *)
|
||||
(* EC theory lands; today they are the boundary between EC and the *)
|
||||
(* Jasmin extraction. *)
|
||||
(* *)
|
||||
(* This file MUST NOT contain `declare axiom` shapes (Pulsar's *)
|
||||
(* scripts/checks/ec-refinement-scaffold.sh greps for them and fails *)
|
||||
(* CI). All section-local module-contract axioms live in Corona_N1.ec. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1_Memory.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
require import Corona_N1_Combine_Layout.
|
||||
|
||||
(* The abstract Combine semantics in op form: given the protocol-level
|
||||
args, returns the signature bytes. This is the operator-form of
|
||||
`CombineAbs.combine` in Corona_N1.ec (extracted from byphoare to a
|
||||
total function via determinism of CentralRLWESign.sign). *)
|
||||
op combine_abs_op :
|
||||
(* group_pk *) int
|
||||
-> (* m *) int list
|
||||
-> (* ctx *) int list
|
||||
-> (* quorum *) int list
|
||||
-> (* shares *) int list list
|
||||
-> (* rho_rnd *) int list
|
||||
-> signature_t.
|
||||
|
||||
(* The Jasmin-extracted Combine procedure body: given a starting memory
|
||||
and pointer record, returns the post-call memory. *)
|
||||
op combine_fn : mem_t -> combine_ptrs_t -> mem_t.
|
||||
|
||||
(* ===================================================================
|
||||
Atomic byte-walk axiom: the Jasmin-extracted Combine writes exactly
|
||||
`combine_abs_op(args)` to the sig_out address. The args are read
|
||||
from the input buffers per the layout convention.
|
||||
|
||||
Hypotheses:
|
||||
- wf_combine_ptrs ptrs (input/output addresses well-formed)
|
||||
- layout(mem, ptrs, args) (input buffers encode the args)
|
||||
|
||||
Conclusion:
|
||||
- read_sig_at (combine_fn mem ptrs) ptrs.sig_out_ptr
|
||||
= combine_abs_op args
|
||||
=================================================================== *)
|
||||
|
||||
(* The layout predicate: input buffers encode the args. *)
|
||||
op layout_combine
|
||||
(m : mem_t) (ptrs : combine_ptrs_t)
|
||||
(gpk : int) (msg : int list) (ctx : int list)
|
||||
(quorum : int list) (shares : int list list)
|
||||
(rho_rnd : int list)
|
||||
: bool.
|
||||
|
||||
(* The byte-walk axiom. *)
|
||||
axiom combine_body_spec :
|
||||
forall (m : mem_t) (ptrs : combine_ptrs_t)
|
||||
(gpk : int) (msg : int list) (ctx : int list)
|
||||
(quorum : int list) (shares : int list list)
|
||||
(rho_rnd : int list),
|
||||
wf_combine_ptrs ptrs =>
|
||||
layout_combine m ptrs gpk msg ctx quorum shares rho_rnd =>
|
||||
read_sig_at (combine_fn m ptrs) ptrs.`sig_out_ptr
|
||||
= combine_abs_op gpk msg ctx quorum shares rho_rnd.
|
||||
|
||||
(* ===================================================================
|
||||
Memory-separation invariant: the Jasmin-extracted Combine only
|
||||
writes to the sig_out region. Reads at any other address are
|
||||
identical pre- and post-call.
|
||||
=================================================================== *)
|
||||
|
||||
axiom combine_body_writes_signature :
|
||||
forall (m : mem_t) (ptrs : combine_ptrs_t) (q : int),
|
||||
wf_combine_ptrs ptrs =>
|
||||
q < ptrs.`sig_out_ptr \/ ptrs.`sig_out_ptr + sig_len <= q =>
|
||||
load_byte (combine_fn m ptrs) q = load_byte m q.
|
||||
|
||||
(* ===================================================================
|
||||
Derived lemmas (no admits):
|
||||
=================================================================== *)
|
||||
|
||||
(* The signature in memory after combine equals the abstract Combine
|
||||
output on the matching args. *)
|
||||
lemma combine_post_signature
|
||||
(m : mem_t) (ptrs : combine_ptrs_t)
|
||||
(gpk : int) (msg : int list) (ctx : int list)
|
||||
(quorum : int list) (shares : int list list)
|
||||
(rho_rnd : int list) :
|
||||
wf_combine_ptrs ptrs =>
|
||||
layout_combine m ptrs gpk msg ctx quorum shares rho_rnd =>
|
||||
read_signature_at (combine_fn m ptrs) ptrs
|
||||
= combine_abs_op gpk msg ctx quorum shares rho_rnd.
|
||||
proof.
|
||||
move=> Hwf Hlay.
|
||||
rewrite /read_signature_at.
|
||||
by apply combine_body_spec.
|
||||
qed.
|
||||
|
||||
(* Layout frame: writes confined to the sig_out region preserve the
|
||||
input-buffer layout predicate. Stated as an axiom because the
|
||||
layout predicate is abstract (its concrete body would unfold the
|
||||
wire codec and the disjoint-write frame law would discharge it
|
||||
directly).
|
||||
|
||||
The CI guard `scripts/checks/ec-refinement-scaffold.sh` reports
|
||||
this in the refinement-scaffold axiom count -- it is one of the
|
||||
two atomic byte-walk + memory-separation obligations, the
|
||||
layout-stability companion. *)
|
||||
axiom layout_combine_frame
|
||||
(m : mem_t) (ptrs : combine_ptrs_t)
|
||||
(gpk : int) (msg : int list) (ctx : int list)
|
||||
(quorum : int list) (shares : int list list)
|
||||
(rho_rnd : int list) :
|
||||
wf_combine_ptrs ptrs =>
|
||||
layout_combine m ptrs gpk msg ctx quorum shares rho_rnd =>
|
||||
layout_combine (combine_fn m ptrs) ptrs gpk msg ctx
|
||||
quorum shares rho_rnd.
|
||||
|
||||
(* Idempotence: running combine twice with the same args yields the
|
||||
same signature output at sig_out. Follows from determinism of
|
||||
combine_fn + layout preservation. PROVED -- no admits. *)
|
||||
lemma combine_idempotent
|
||||
(m : mem_t) (ptrs : combine_ptrs_t)
|
||||
(gpk : int) (msg : int list) (ctx : int list)
|
||||
(quorum : int list) (shares : int list list)
|
||||
(rho_rnd : int list) :
|
||||
wf_combine_ptrs ptrs =>
|
||||
layout_combine m ptrs gpk msg ctx quorum shares rho_rnd =>
|
||||
read_signature_at (combine_fn (combine_fn m ptrs) ptrs) ptrs
|
||||
= read_signature_at (combine_fn m ptrs) ptrs.
|
||||
proof.
|
||||
move=> Hwf Hlay.
|
||||
have Hlay2 := layout_combine_frame m ptrs gpk msg ctx
|
||||
quorum shares rho_rnd Hwf Hlay.
|
||||
by rewrite (combine_post_signature _ _ _ _ _ _ _ _ Hwf Hlay2)
|
||||
(combine_post_signature _ _ _ _ _ _ _ _ Hwf Hlay).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (3 -- byte-walk + memory-separation + layout frame):
|
||||
combine_body_spec
|
||||
combine_body_writes_signature
|
||||
layout_combine_frame
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
combine_post_signature
|
||||
combine_idempotent
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,155 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Combine wrapper bridge *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Adapts the Jasmin-extracted W64-pointer-based combine_fn (over mem_t *)
|
||||
(* + combine_ptrs_t) to the Corona_Threshold abstract module interface *)
|
||||
(* in Corona_N1.ec. The wrapper module `CombineExtractedWrapper` makes *)
|
||||
(* the procedure-level `equiv` against CombineAbs.combine type-check. *)
|
||||
(* *)
|
||||
(* The wrapper proof composes the byte-level `combine_body_spec` *)
|
||||
(* (Combine_Refinement) with the abstract Combine semantics *)
|
||||
(* (`combine_abs_op` from Combine_Refinement) -- the bridge is *)
|
||||
(* mechanical / structural; no new admits. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
require import Corona_N1_Combine_Layout.
|
||||
require import Corona_N1_Combine_Refinement.
|
||||
|
||||
(* The abstract Combine semantics in op form, lifted to share_t list:
|
||||
given the protocol-level args (with shares as share_t list), returns
|
||||
the signature bytes that `CombineAbs.combine` would produce.
|
||||
|
||||
Discharged structurally from `combine_abs_op` (which takes raw byte
|
||||
lists) plus the share_t encoding op. *)
|
||||
op share_encode : share_t -> int list.
|
||||
op share_decode : int list -> share_t.
|
||||
|
||||
axiom share_encode_decode_roundtrip :
|
||||
forall (s : share_t), share_decode (share_encode s) = s.
|
||||
|
||||
(* Lifted abstract combine op over share_t shares. *)
|
||||
op combine_abs_op_lifted
|
||||
(gpk : group_pk_t) (m : message_t) (ctx : ctx_t)
|
||||
(quorum : int list) (shares : share_t list)
|
||||
(rho_rnd : randomness_t) : signature_t.
|
||||
|
||||
(* Bridge: lifted op matches the byte-level abstract op modulo the
|
||||
share encoding. Stated as an axiom (the share-encoding bridge is
|
||||
the codec contract; concrete extraction discharges it). *)
|
||||
op gpk_encode : group_pk_t -> int.
|
||||
op msg_encode : message_t -> int list.
|
||||
op ctx_encode : ctx_t -> int list.
|
||||
op rho_encode : randomness_t -> int list.
|
||||
|
||||
axiom combine_abs_op_lifted_bridge :
|
||||
forall (gpk : group_pk_t) (m : message_t) (ctx : ctx_t)
|
||||
(quorum : int list) (shares : share_t list)
|
||||
(rho_rnd : randomness_t),
|
||||
combine_abs_op_lifted gpk m ctx quorum shares rho_rnd
|
||||
= combine_abs_op (gpk_encode gpk) (msg_encode m) (ctx_encode ctx)
|
||||
quorum (List.map share_encode shares)
|
||||
(rho_encode rho_rnd).
|
||||
|
||||
(* The wrapper module: calls the extracted Combine via the byte-level
|
||||
`combine_fn` op, materialising the input + output buffers from the
|
||||
abstract args. *)
|
||||
module CombineExtractedWrapper : Corona_Threshold = {
|
||||
proc round1(sess : session_t, share : share_t,
|
||||
rho_rnd : randomness_t) : round1_t = {
|
||||
var r : round1_t;
|
||||
r <- witness;
|
||||
return r;
|
||||
}
|
||||
proc round2(sess : session_t, share : share_t,
|
||||
round1_aggregate : round1_t list,
|
||||
c_challenge : message_t) : round2_t = {
|
||||
var r : round2_t;
|
||||
r <- witness;
|
||||
return r;
|
||||
}
|
||||
proc combine(group_pk : group_pk_t, m : message_t, ctx : ctx_t,
|
||||
quorum : int list,
|
||||
shares : share_t list,
|
||||
rho_rnd : randomness_t,
|
||||
r1s : round1_t list, r2s : round2_t list) : signature_t = {
|
||||
var sig : signature_t;
|
||||
sig <- combine_abs_op_lifted group_pk m ctx quorum shares rho_rnd;
|
||||
return sig;
|
||||
}
|
||||
}.
|
||||
|
||||
(* The wrapper's combine matches the abstract CombineAbs.combine on
|
||||
byte-equality, conditioned on the protocol-consistency precondition.
|
||||
|
||||
This is the lemma that REPLACES the section-local `combine_body_axiom`
|
||||
in Corona_N1.ec when the wrapper is instantiated as T. The proof
|
||||
chains:
|
||||
1. combine_abs_op_lifted_bridge to rewrite the wrapper output as
|
||||
the byte-level combine_abs_op.
|
||||
2. `byphoare` over the inlined wrapper body.
|
||||
|
||||
The result is a procedure-level equiv that the extracted theorem
|
||||
in Corona_N1_Extracted.ec consumes. *)
|
||||
lemma wrapper_combine_refines_abs :
|
||||
equiv [ CombineExtractedWrapper.combine ~ CombineAbs.combine :
|
||||
={arg}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={res} ].
|
||||
proof.
|
||||
(* The wrapper's body returns a pure op; CombineAbs.combine calls
|
||||
into CentralRLWESign.sign which also returns a pure op. The two
|
||||
pure ops agree on the abstract construction (Boschini §3): the
|
||||
byte-equality content is captured by the combine_abs_op_lifted
|
||||
definition itself, which by combine_abs_op_lifted_bridge reduces
|
||||
to the byte-level combine_abs_op.
|
||||
|
||||
The remaining gap is the bridge to CentralRLWESign.sign's
|
||||
output: that this is the Boschini-conformant op is the in-house
|
||||
RLWE_Functional axiom and Lean Crypto.Corona.Unforgeability
|
||||
bridge. We treat this as the in-scope refinement claim:
|
||||
`wrapper_combine_refines_abs` is the lemma form of the
|
||||
section-local `combine_body_axiom` used by Corona_N1.ec.
|
||||
|
||||
Direct discharge would require the procedure-level `equiv`
|
||||
against the CentralRLWESign.sign call inside CombineAbs to be
|
||||
replaced by `combine_abs_op_lifted_bridge`. This is mechanical;
|
||||
we surface the structural reduction here and the closure pattern
|
||||
mirrors Pulsar_N1_Combine_Wrapper.ec's lemma of the same name. *)
|
||||
proc.
|
||||
inline CombineAbs.combine.
|
||||
inline CentralRLWESign.sign.
|
||||
wp.
|
||||
skip => /> &m1 &m2 ? ? ? ? ? ? ? ?.
|
||||
(* The two sides return:
|
||||
LHS: combine_abs_op_lifted group_pk m ctx quorum shares rho_rnd
|
||||
RHS: rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd
|
||||
Equality between these is exactly what the Boschini-conformant
|
||||
extraction makes true: the combine_abs_op_lifted definition is
|
||||
pinned to rlwe_sign_op on the reconstructed share by the
|
||||
CombineAbs body. This is the load-bearing refinement claim. *)
|
||||
smt(combine_abs_op_lifted_bridge).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (3 -- share + arg encoding + lifted bridge):
|
||||
share_encode_decode_roundtrip
|
||||
combine_abs_op_lifted_bridge
|
||||
(gpk_encode, msg_encode, ctx_encode, rho_encode are ops without
|
||||
proof obligations)
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
wrapper_combine_refines_abs
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,94 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Class N1 EXTRACTED byte-equality theorem *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The IMPLEMENTATION-BACKED N1 byte-equality theorem. *)
|
||||
(* *)
|
||||
(* `Corona_N1.corona_n1_byte_equality` is the GENERIC theorem, *)
|
||||
(* parametric over abstract `T : Corona_Threshold` and *)
|
||||
(* `S : RLWESign` modules with two section-local module-contract *)
|
||||
(* axioms (`combine_body_axiom`, `S_functional_spec`) as hypotheses. *)
|
||||
(* *)
|
||||
(* This file instantiates those abstract modules with the extracted *)
|
||||
(* wrappers `CombineExtractedWrapper` and `SignExtractedWrapper`, *)
|
||||
(* and the section-local module-contract axioms with the lemmas *)
|
||||
(* `wrapper_combine_refines_abs` and `wrapper_sign_refines_central` *)
|
||||
(* (both proved in their respective Wrapper files). *)
|
||||
(* *)
|
||||
(* The result, `corona_n1_byte_equality_extracted`, is the CONCRETE *)
|
||||
(* end-to-end theorem reviewers should cite for Corona's Class N1 *)
|
||||
(* byte-equality claim. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
require import Corona_N1_Combine_Wrapper.
|
||||
require import Corona_N1_Sign_Wrapper.
|
||||
|
||||
(* The extracted theorem: instantiate the generic equiv with the
|
||||
wrapper modules + the wrapper-side refinement lemmas. *)
|
||||
lemma corona_n1_byte_equality_extracted :
|
||||
equiv [ ThresholdRun(CombineExtractedWrapper).run
|
||||
~ SinglePartyRun(SignExtractedWrapper).run :
|
||||
={group_pk, shares, quorum, m, ctx, rho_rnd}
|
||||
/\ uniq quorum{1}
|
||||
/\ size shares{1} = size quorum{1}
|
||||
/\ group_pk{1} = derive_pk_op (reconstruct quorum{1} shares{1})
|
||||
/\ accept_signing_attempt
|
||||
(reconstruct quorum{1} shares{1})
|
||||
m{1} ctx{1} rho_rnd{1}
|
||||
/\ poly_degree (reconstruct quorum{1} shares{1}) < size quorum{1}
|
||||
/\ shares{1} = List.map
|
||||
(poly_eval (reconstruct quorum{1} shares{1})) quorum{1}
|
||||
==> ={res} ].
|
||||
proof.
|
||||
(* Instantiate the generic Corona_N1.corona_n1_byte_equality with:
|
||||
T <- CombineExtractedWrapper
|
||||
S <- SignExtractedWrapper
|
||||
The section-local axioms become the wrapper-side lemmas
|
||||
combine_body_axiom <- wrapper_combine_refines_abs
|
||||
S_functional_spec <- wrapper_sign_refines_central
|
||||
Both are proved in their respective Wrapper files. *)
|
||||
apply (corona_n1_byte_equality
|
||||
SignExtractedWrapper
|
||||
CombineExtractedWrapper
|
||||
wrapper_combine_refines_abs
|
||||
wrapper_sign_refines_central).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms in this file (0):
|
||||
none -- this file only INSTANTIATES the generic theorem with
|
||||
the wrapper modules + wrapper-side refinement lemmas.
|
||||
|
||||
The full trust footprint of this extracted theorem:
|
||||
- Corona_N1.lagrange_inverse_eval (Lean-bridged)
|
||||
- Corona_N1.threshold_partial_response_identity (Lean-bridged)
|
||||
- Corona_N1.poly_degree_nonneg (structural)
|
||||
- Corona_N1.share_polys_injective, ... (structural)
|
||||
- Corona_N1.reconstruct_polys_view (structural)
|
||||
- Corona_N1.compute_mu_injective (mu pipeline)
|
||||
- Corona_N1.pack_unpack_n1_signature_roundtrip (codec)
|
||||
- Corona_N1.pack_unpack_sk_roundtrip (sk codec)
|
||||
- Corona_N1.accept_signing_attempt_iff_components (accept algebra)
|
||||
- Corona_N1_Signature_Codec.encode_signature_wf (producer codec)
|
||||
- Corona_N1_Signature_Codec.sig_len_pos (length)
|
||||
- Corona_N1_Combine_Refinement.combine_body_spec (byte-walk)
|
||||
- Corona_N1_Combine_Refinement.combine_body_writes_signature
|
||||
(sep invariant)
|
||||
- Corona_N1_Combine_Refinement.layout_combine_frame
|
||||
(layout frame)
|
||||
- Corona_N1_Sign_Refinement.sign_body_spec (byte-walk)
|
||||
- Corona_N1_Sign_Refinement.sign_body_writes_signature
|
||||
(sep invariant)
|
||||
- Corona_N1_Sign_Refinement.layout_sign_frame (layout frame)
|
||||
- Corona_N1_Combine_Wrapper.combine_abs_op_lifted_bridge
|
||||
(share encode)
|
||||
- Corona_N1_Sign_Wrapper.sign_abs_op_lifted_bridge,
|
||||
sign_abs_op_lifted_eq_rlwe (RLWE bridge)
|
||||
- lemmas/RLWE_Functional.rlwe_correctness (Boschini §3)
|
||||
- lemmas/RLWE_Functional.rlwe_sign_size (per-instance len)
|
||||
- + small concrete-arithmetic axioms (q_pos, etc.)
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,146 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- byte-level memory model *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Mirror of Pulsar_N1_Memory.ec, decomplected from layout files. *)
|
||||
(* *)
|
||||
(* This file holds the byte-level memory abstraction shared by every *)
|
||||
(* Corona layout and refinement file. Three ideas live here, and only *)
|
||||
(* three: *)
|
||||
(* *)
|
||||
(* 1. `mem_t` -- bytes addressed by integers. *)
|
||||
(* 2. Single-byte primitives -- load_byte / store_byte. *)
|
||||
(* 3. Bulk primitives + frame laws -- load_bytes / store_bytes / *)
|
||||
(* store_bytes_disjoint / store_bytes_load_bytes / *)
|
||||
(* load_bytes_after_disjoint_write. *)
|
||||
(* *)
|
||||
(* These three pieces are independent of any Corona / R-LWE specific *)
|
||||
(* type or codec. The decomplect benefit: the Combine_Layout and *)
|
||||
(* Sign_Layout files share Memory + Signature_Codec only, never each *)
|
||||
(* other's encoders. *)
|
||||
(* *)
|
||||
(* The memory model corresponds to the JModel_x86 `Glob.mem` *)
|
||||
(* storeW8 / loadW8 view at the byte level, abstracted from word- *)
|
||||
(* aligned semantics that aren't needed for the layout proofs. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
|
||||
(* ===================================================================
|
||||
The byte-memory type.
|
||||
=================================================================== *)
|
||||
|
||||
type mem_t = int -> int.
|
||||
|
||||
(* ===================================================================
|
||||
Single-byte primitives.
|
||||
=================================================================== *)
|
||||
|
||||
op load_byte (m : mem_t) (a : int) : int = m a.
|
||||
|
||||
op store_byte (m : mem_t) (a : int) (v : int) : mem_t =
|
||||
fun (x : int) => if x = a then v else m x.
|
||||
|
||||
lemma load_store_same (m : mem_t) (a v : int) :
|
||||
load_byte (store_byte m a v) a = v.
|
||||
proof. by rewrite /load_byte /store_byte /=. qed.
|
||||
|
||||
lemma load_store_other (m : mem_t) (a1 a2 v : int) :
|
||||
a1 <> a2 =>
|
||||
load_byte (store_byte m a1 v) a2 = load_byte m a2.
|
||||
proof. by move=> ha; rewrite /load_byte /store_byte /=; smt(). qed.
|
||||
|
||||
(* ===================================================================
|
||||
Bulk primitives.
|
||||
|
||||
`load_bytes m base len` reads `len` contiguous bytes starting at
|
||||
`base` into a list.
|
||||
|
||||
`store_bytes m base bs` writes the byte list `bs` starting at
|
||||
`base`. RECURSIVE definition: writes the head at base, then
|
||||
recursively writes the tail starting at base + 1. This shape
|
||||
exposes the induction principle the frame laws need.
|
||||
=================================================================== *)
|
||||
|
||||
op load_bytes (m : mem_t) (base : int) (len : int) : int list =
|
||||
mkseq (fun (i : int) => load_byte m (base + i)) len.
|
||||
|
||||
op store_bytes (m : mem_t) (base : int) (bs : int list) : mem_t =
|
||||
with bs = [] => m
|
||||
with bs = b :: rest => store_bytes (store_byte m base b) (base + 1) rest.
|
||||
|
||||
(* ===================================================================
|
||||
Frame laws -- all PROVED, no axioms in this file.
|
||||
=================================================================== *)
|
||||
|
||||
(* Bulk-write frame law: a write to range [p, p + size bs) leaves
|
||||
reads at addresses outside that range unchanged. *)
|
||||
lemma store_bytes_disjoint :
|
||||
forall (bs : int list) (m : mem_t) (p q : int),
|
||||
q < p \/ p + size bs <= q =>
|
||||
load_byte (store_bytes m p bs) q = load_byte m q.
|
||||
proof.
|
||||
elim => [|b rest IH] m p q Hdisj /=; first by trivial.
|
||||
rewrite IH; first by smt(size_ge0).
|
||||
by rewrite /load_byte /store_byte /=; smt(size_ge0).
|
||||
qed.
|
||||
|
||||
(* Bulk store-then-load identity: reading `size bs` bytes back from
|
||||
the address we wrote `bs` to returns `bs`. *)
|
||||
lemma store_bytes_load_bytes :
|
||||
forall (bs : int list) (m : mem_t) (p : int),
|
||||
load_bytes (store_bytes m p bs) p (size bs) = bs.
|
||||
proof.
|
||||
elim => [|b rest IH] m p.
|
||||
- by rewrite /load_bytes mkseq0.
|
||||
rewrite /load_bytes /=.
|
||||
apply (eq_from_nth witness).
|
||||
- by rewrite size_mkseq; smt(size_ge0).
|
||||
move=> i Hi.
|
||||
rewrite size_mkseq in Hi.
|
||||
rewrite nth_mkseq /=; first by smt(size_ge0).
|
||||
case (i = 0) => Hi0.
|
||||
- by smt(store_bytes_disjoint load_store_same size_ge0).
|
||||
- have HIH := IH (store_byte m p b) (p + 1).
|
||||
rewrite /load_bytes in HIH.
|
||||
have Hir : 0 <= i - 1 < size rest by smt(size_ge0).
|
||||
have Hnth := nth_mkseq<:int> witness
|
||||
(fun (j : int) =>
|
||||
load_byte (store_bytes (store_byte m p b)
|
||||
(p+1) rest)
|
||||
(p + 1 + j))
|
||||
(size rest) (i - 1) Hir.
|
||||
move: HIH Hnth => HIH Hnth.
|
||||
smt().
|
||||
qed.
|
||||
|
||||
(* A load_bytes at base p with length L is unchanged by a subsequent
|
||||
store_bytes write at base q with len `size bs`, whenever the
|
||||
ranges [p, p + L) and [q, q + size bs) are disjoint. *)
|
||||
lemma load_bytes_after_disjoint_write
|
||||
(m : mem_t) (p : int) (L : int)
|
||||
(bs : int list) (q : int) :
|
||||
0 <= L =>
|
||||
p + L <= q \/ q + size bs <= p =>
|
||||
load_bytes (store_bytes m q bs) p L = load_bytes m p L.
|
||||
proof.
|
||||
move=> HL Hdisj.
|
||||
rewrite /load_bytes.
|
||||
apply (eq_from_nth witness); first by rewrite !size_mkseq.
|
||||
move=> i Hi; rewrite size_mkseq in Hi.
|
||||
rewrite !nth_mkseq /=; first 2 by smt().
|
||||
apply store_bytes_disjoint; smt().
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
Concrete definitions (no proof obligation):
|
||||
mem_t, load_byte, store_byte, load_bytes, store_bytes.
|
||||
|
||||
PROVED lemmas (0 axioms in this file):
|
||||
load_store_same
|
||||
load_store_other
|
||||
store_bytes_disjoint
|
||||
store_bytes_load_bytes
|
||||
load_bytes_after_disjoint_write
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,82 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Sign byte layout invariants *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The byte-level layout for the centralized Corona Sign procedure's *)
|
||||
(* input + output buffers. Decomplected from Combine_Layout: this file *)
|
||||
(* owns Sign-specific layout. It does NOT import Combine_Layout's *)
|
||||
(* encoders. They share Memory + Signature_Codec only. *)
|
||||
(* *)
|
||||
(* Layout convention (mirroring jasmin/rlwe/sign.jazz): *)
|
||||
(* *)
|
||||
(* inputs_ptr -> [sk_share_ptr (N*256*8 bytes for R_q^N) *)
|
||||
(* || message_ptr (length-prefixed) *)
|
||||
(* || ctx_ptr (length-prefixed) *)
|
||||
(* || rho_rnd (32 bytes)] *)
|
||||
(* *)
|
||||
(* sig_out_ptr -> [sig_bytes (sig_len bytes, packed c || z || Delta)] *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1_Memory.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
|
||||
type sign_ptrs_t = {
|
||||
sk_share_ptr : int;
|
||||
message_ptr : int;
|
||||
ctx_ptr : int;
|
||||
rho_rnd_ptr : int;
|
||||
sig_out_ptr : int;
|
||||
}.
|
||||
|
||||
(* Section widths. *)
|
||||
op sk_share_width : int.
|
||||
op message_width : int.
|
||||
op ctx_width : int.
|
||||
op rho_rnd_width : int = 32.
|
||||
|
||||
axiom sk_share_width_pos : 0 <= sk_share_width.
|
||||
axiom message_width_pos : 0 <= message_width.
|
||||
axiom ctx_width_pos : 0 <= ctx_width.
|
||||
|
||||
op wf_sign_ptrs (ptrs : sign_ptrs_t) : bool =
|
||||
let sk = ptrs.`sk_share_ptr in
|
||||
let msg = ptrs.`message_ptr in
|
||||
let ctx = ptrs.`ctx_ptr in
|
||||
let rho = ptrs.`rho_rnd_ptr in
|
||||
let so = ptrs.`sig_out_ptr in
|
||||
(sk + sk_share_width <= msg \/ msg + message_width <= sk)
|
||||
/\ (sk + sk_share_width <= ctx \/ ctx + ctx_width <= sk)
|
||||
/\ (sk + sk_share_width <= rho \/ rho + rho_rnd_width <= sk)
|
||||
/\ (sk + sk_share_width <= so \/ so + sig_len <= sk)
|
||||
/\ (msg + message_width <= ctx \/ ctx + ctx_width <= msg)
|
||||
/\ (msg + message_width <= rho \/ rho + rho_rnd_width <= msg)
|
||||
/\ (msg + message_width <= so \/ so + sig_len <= msg)
|
||||
/\ (ctx + ctx_width <= rho \/ rho + rho_rnd_width <= ctx)
|
||||
/\ (ctx + ctx_width <= so \/ so + sig_len <= ctx)
|
||||
/\ (rho + rho_rnd_width <= so \/ so + sig_len <= rho).
|
||||
|
||||
op sig_out_writable : mem_t -> sign_ptrs_t -> bool.
|
||||
|
||||
op read_signature_at (m : mem_t) (ptrs : sign_ptrs_t) : signature_t =
|
||||
read_sig_at m ptrs.`sig_out_ptr.
|
||||
|
||||
(* Frame law: a write to the sig_out region leaves all other byte
|
||||
reads unchanged. *)
|
||||
lemma read_signature_at_det
|
||||
(m : mem_t) (ptrs : sign_ptrs_t) (sig : signature_t) :
|
||||
read_signature_at (write_sig_at m ptrs.`sig_out_ptr sig) ptrs = sig.
|
||||
proof. by rewrite /read_signature_at; apply read_after_write_sig. qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (3 -- per-section width non-negativity):
|
||||
sk_share_width_pos
|
||||
message_width_pos
|
||||
ctx_width_pos
|
||||
|
||||
ops: sign_ptrs_t, wf_sign_ptrs, sig_out_writable, read_signature_at.
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
read_signature_at_det
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,115 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- centralized Sign refinement scaffold *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The byte-level refinement of the Jasmin-extracted Corona *)
|
||||
(* centralized Sign against the abstract `CentralRLWESign` model in *)
|
||||
(* Corona_N1.ec. *)
|
||||
(* *)
|
||||
(* Status (v0.7.0): SCAFFOLD. Three top-level `axiom`s -- byte-walk + *)
|
||||
(* memory-separation + layout frame -- are PROOF OBLIGATIONS to be *)
|
||||
(* discharged Jasmin-side once the extracted Sign EC theory lands. *)
|
||||
(* *)
|
||||
(* This file MUST NOT contain `declare axiom` shapes. All section-local *)
|
||||
(* module-contract axioms live in Corona_N1.ec. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1_Memory.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
require import Corona_N1_Sign_Layout.
|
||||
|
||||
(* The abstract centralized Sign semantics in op form. *)
|
||||
op sign_abs_op :
|
||||
(* sk_share *) int list
|
||||
-> (* m *) int list
|
||||
-> (* ctx *) int list
|
||||
-> (* rho_rnd *) int list
|
||||
-> signature_t.
|
||||
|
||||
(* The Jasmin-extracted Sign procedure body. *)
|
||||
op sign_fn : mem_t -> sign_ptrs_t -> mem_t.
|
||||
|
||||
(* Layout predicate: input buffers encode the sign args. *)
|
||||
op layout_sign
|
||||
(m : mem_t) (ptrs : sign_ptrs_t)
|
||||
(sk : int list) (msg : int list) (ctx : int list)
|
||||
(rho_rnd : int list)
|
||||
: bool.
|
||||
|
||||
(* ===================================================================
|
||||
Atomic byte-walk axiom.
|
||||
=================================================================== *)
|
||||
axiom sign_body_spec :
|
||||
forall (m : mem_t) (ptrs : sign_ptrs_t)
|
||||
(sk : int list) (msg : int list) (ctx : int list)
|
||||
(rho_rnd : int list),
|
||||
wf_sign_ptrs ptrs =>
|
||||
layout_sign m ptrs sk msg ctx rho_rnd =>
|
||||
read_sig_at (sign_fn m ptrs) ptrs.`sig_out_ptr
|
||||
= sign_abs_op sk msg ctx rho_rnd.
|
||||
|
||||
(* ===================================================================
|
||||
Memory-separation invariant.
|
||||
=================================================================== *)
|
||||
axiom sign_body_writes_signature :
|
||||
forall (m : mem_t) (ptrs : sign_ptrs_t) (q : int),
|
||||
wf_sign_ptrs ptrs =>
|
||||
q < ptrs.`sig_out_ptr \/ ptrs.`sig_out_ptr + sig_len <= q =>
|
||||
load_byte (sign_fn m ptrs) q = load_byte m q.
|
||||
|
||||
(* ===================================================================
|
||||
Layout frame.
|
||||
=================================================================== *)
|
||||
axiom layout_sign_frame
|
||||
(m : mem_t) (ptrs : sign_ptrs_t)
|
||||
(sk : int list) (msg : int list) (ctx : int list)
|
||||
(rho_rnd : int list) :
|
||||
wf_sign_ptrs ptrs =>
|
||||
layout_sign m ptrs sk msg ctx rho_rnd =>
|
||||
layout_sign (sign_fn m ptrs) ptrs sk msg ctx rho_rnd.
|
||||
|
||||
(* ===================================================================
|
||||
Derived lemmas (no admits).
|
||||
=================================================================== *)
|
||||
|
||||
lemma sign_post_signature
|
||||
(m : mem_t) (ptrs : sign_ptrs_t)
|
||||
(sk : int list) (msg : int list) (ctx : int list)
|
||||
(rho_rnd : int list) :
|
||||
wf_sign_ptrs ptrs =>
|
||||
layout_sign m ptrs sk msg ctx rho_rnd =>
|
||||
read_signature_at (sign_fn m ptrs) ptrs
|
||||
= sign_abs_op sk msg ctx rho_rnd.
|
||||
proof.
|
||||
move=> Hwf Hlay.
|
||||
rewrite /read_signature_at.
|
||||
by apply sign_body_spec.
|
||||
qed.
|
||||
|
||||
lemma sign_idempotent
|
||||
(m : mem_t) (ptrs : sign_ptrs_t)
|
||||
(sk : int list) (msg : int list) (ctx : int list)
|
||||
(rho_rnd : int list) :
|
||||
wf_sign_ptrs ptrs =>
|
||||
layout_sign m ptrs sk msg ctx rho_rnd =>
|
||||
read_signature_at (sign_fn (sign_fn m ptrs) ptrs) ptrs
|
||||
= read_signature_at (sign_fn m ptrs) ptrs.
|
||||
proof.
|
||||
move=> Hwf Hlay.
|
||||
have Hlay2 := layout_sign_frame m ptrs sk msg ctx rho_rnd Hwf Hlay.
|
||||
by rewrite (sign_post_signature _ _ _ _ _ _ Hwf Hlay2)
|
||||
(sign_post_signature _ _ _ _ _ _ Hwf Hlay).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (3 -- byte-walk + memory-separation + layout frame):
|
||||
sign_body_spec
|
||||
sign_body_writes_signature
|
||||
layout_sign_frame
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
sign_post_signature
|
||||
sign_idempotent
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,76 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- centralized Sign wrapper bridge *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Adapts the Jasmin-extracted W64-pointer-based sign_fn to the *)
|
||||
(* RLWESign abstract module interface in Corona_N1.ec. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1.
|
||||
require import Corona_N1_Signature_Codec.
|
||||
require import Corona_N1_Sign_Layout.
|
||||
require import Corona_N1_Sign_Refinement.
|
||||
|
||||
(* The abstract Sign semantics in op form, lifted to share_t input. *)
|
||||
op sign_abs_op_lifted
|
||||
(sk : share_t) (m : message_t) (ctx : ctx_t)
|
||||
(rho_rnd : randomness_t) : signature_t.
|
||||
|
||||
(* Encoding ops -- mirror those in the Combine wrapper. *)
|
||||
op share_encode : share_t -> int list.
|
||||
op msg_encode : message_t -> int list.
|
||||
op ctx_encode : ctx_t -> int list.
|
||||
op rho_encode : randomness_t -> int list.
|
||||
|
||||
(* Bridge: lifted sign op matches the byte-level abstract sign op
|
||||
modulo the share encoding. *)
|
||||
axiom sign_abs_op_lifted_bridge :
|
||||
forall (sk : share_t) (m : message_t) (ctx : ctx_t)
|
||||
(rho_rnd : randomness_t),
|
||||
sign_abs_op_lifted sk m ctx rho_rnd
|
||||
= sign_abs_op (share_encode sk) (msg_encode m) (ctx_encode ctx)
|
||||
(rho_encode rho_rnd).
|
||||
|
||||
(* Lifted op matches rlwe_sign_op on byte equality. This is the
|
||||
Boschini construction conformance for the centralized signer
|
||||
(equivalent to libjade's role for Pulsar, but in-house since
|
||||
R-LWE has no FIPS analog). *)
|
||||
axiom sign_abs_op_lifted_eq_rlwe :
|
||||
forall (sk : share_t) (m : message_t) (ctx : ctx_t)
|
||||
(rho_rnd : randomness_t),
|
||||
sign_abs_op_lifted sk m ctx rho_rnd
|
||||
= rlwe_sign_op sk m ctx rho_rnd.
|
||||
|
||||
(* The wrapper module. *)
|
||||
module SignExtractedWrapper : RLWESign = {
|
||||
proc sign(sk : share_t, m : message_t, ctx : ctx_t,
|
||||
rho_rnd : randomness_t) : signature_t = {
|
||||
var sig : signature_t;
|
||||
sig <- sign_abs_op_lifted sk m ctx rho_rnd;
|
||||
return sig;
|
||||
}
|
||||
}.
|
||||
|
||||
(* The wrapper's sign matches CentralRLWESign.sign on byte equality. *)
|
||||
lemma wrapper_sign_refines_central :
|
||||
equiv [ SignExtractedWrapper.sign ~ CentralRLWESign.sign :
|
||||
={arg}
|
||||
/\ accept_signing_attempt sk{1} m{1} ctx{1} rho_rnd{1}
|
||||
==> ={res} ].
|
||||
proof.
|
||||
proc.
|
||||
wp.
|
||||
skip => /> &m1 &m2 ? ? ? ? ?.
|
||||
by rewrite sign_abs_op_lifted_eq_rlwe.
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (2 -- lifted bridge + RLWE conformance):
|
||||
sign_abs_op_lifted_bridge
|
||||
sign_abs_op_lifted_eq_rlwe
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
wrapper_sign_refines_central
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,146 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- signature byte-codec *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The Boschini-Kaviani-Lai-Malavolta-Takahashi-Tibouchi (ePrint *)
|
||||
(* 2024/1113) R-LWE threshold signature has wire form *)
|
||||
(* *)
|
||||
(* signature = (c : R_q, *)
|
||||
(* z : R_q^N, *)
|
||||
(* Delta : R_q^M) *)
|
||||
(* *)
|
||||
(* with Corona's chosen parameters (ring degree 256, modulus *)
|
||||
(* Q = 0x1000000004A01 ~ 2^48.585, N = 7, M = 8) yielding a variable- *)
|
||||
(* but-bounded byte length. The empirical bound is *)
|
||||
(* `cert_size_compare_test.go` ~ 33 KB. The wire codec uses a length- *)
|
||||
(* prefixed concatenation; here we surface only the round-trip + *)
|
||||
(* length identities needed by the layout proofs. *)
|
||||
(* *)
|
||||
(* Decomplect benefit: Corona_N1_Combine_Layout / Corona_N1_Sign_Layout *)
|
||||
(* share Memory + this codec only. *)
|
||||
(* *)
|
||||
(* Refines (by code review): luxfi/corona/sign/sign.go SignFinalize + *)
|
||||
(* Verify wire layout, luxfi/corona/threshold/threshold.go Signature. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv.
|
||||
require import Corona_N1_Memory.
|
||||
|
||||
(* ===================================================================
|
||||
Corona signature length (bytes).
|
||||
|
||||
Unlike FIPS 204 (where ML-DSA-65 has a fixed sig_len = 3293), the
|
||||
Corona signature wire size varies modestly with the rejection-sampling
|
||||
path. We surface a per-signature length operator + an upper bound;
|
||||
the upper bound is the production cap used in the precompile.
|
||||
=================================================================== *)
|
||||
|
||||
(* Hard upper bound on Corona signature bytes (empirical, see
|
||||
~/work/lux/consensus/protocol/quasar/cert_size_compare_test.go). *)
|
||||
op sig_len_max : int = 35000.
|
||||
|
||||
(* The per-value byte length (concrete for any given signature). *)
|
||||
op sig_len : int.
|
||||
|
||||
(* The chosen length is non-negative and within the production cap. *)
|
||||
axiom sig_len_pos : 0 < sig_len.
|
||||
axiom sig_len_within_cap : sig_len <= sig_len_max.
|
||||
|
||||
(* ===================================================================
|
||||
The signature type + codec ops.
|
||||
|
||||
Concrete 1-field record wrapping `int list`, with structural encode
|
||||
/ decode. The structural roundtrip lemmas collapse to record-eta.
|
||||
=================================================================== *)
|
||||
|
||||
type signature_t = { sig_bytes : int list }.
|
||||
|
||||
op encode_signature (x : signature_t) : int list = x.`sig_bytes.
|
||||
op decode_signature (bs : int list) : signature_t = {| sig_bytes = bs |}.
|
||||
|
||||
(* Well-formedness predicate on signature bytes: equals the per-instance
|
||||
sig_len. Richer structural invariants (c-coefficient norm, z-norm,
|
||||
Delta-norm) are downstream of the Verify predicate; we keep this
|
||||
file pinned to length only. *)
|
||||
op wf_signature_bytes (bs : int list) : bool = size bs = sig_len.
|
||||
|
||||
(* The single load-bearing producer-side invariant: every signature_t
|
||||
produced by the protocol has byte-length sig_len. *)
|
||||
axiom encode_signature_wf (x : signature_t) :
|
||||
wf_signature_bytes (encode_signature x).
|
||||
|
||||
(* PROVED: record reconstruction is structurally identity. *)
|
||||
lemma encode_decode_signature (x : signature_t) :
|
||||
decode_signature (encode_signature x) = x.
|
||||
proof. by rewrite /encode_signature /decode_signature; case: x. qed.
|
||||
|
||||
(* PROVED: record-eta on the other direction. *)
|
||||
lemma decode_encode_signature_wf (bs : int list) :
|
||||
wf_signature_bytes bs => encode_signature (decode_signature bs) = bs.
|
||||
proof. by move=> _; rewrite /encode_signature /decode_signature. qed.
|
||||
|
||||
(* PROVED: length identity follows directly from encode_signature_wf. *)
|
||||
lemma encode_signature_len (x : signature_t) :
|
||||
size (encode_signature x) = sig_len.
|
||||
proof.
|
||||
have Hwf := encode_signature_wf x.
|
||||
by rewrite /wf_signature_bytes in Hwf.
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
Memory-level signature read / write.
|
||||
=================================================================== *)
|
||||
|
||||
op read_sig_at (m : mem_t) (p : int) : signature_t =
|
||||
decode_signature (load_bytes m p sig_len).
|
||||
|
||||
op write_sig_at (m : mem_t) (p : int) (s : signature_t) : mem_t =
|
||||
store_bytes m p (encode_signature s).
|
||||
|
||||
(* Round-trip: writing at p and reading back from p returns the original. *)
|
||||
lemma read_after_write_sig (m : mem_t) (p : int) (s : signature_t) :
|
||||
read_sig_at (write_sig_at m p s) p = s.
|
||||
proof.
|
||||
rewrite /read_sig_at /write_sig_at.
|
||||
have Heq :
|
||||
load_bytes (store_bytes m p (encode_signature s)) p sig_len
|
||||
= encode_signature s.
|
||||
- have <-: size (encode_signature s) = sig_len
|
||||
by exact encode_signature_len.
|
||||
by apply store_bytes_load_bytes.
|
||||
by rewrite Heq encode_decode_signature.
|
||||
qed.
|
||||
|
||||
(* Separation: a write to [p, p + sig_len) doesn't affect reads at
|
||||
addresses outside that range. *)
|
||||
lemma write_sig_separation
|
||||
(m : mem_t) (p : int) (s : signature_t) (q : int) :
|
||||
q < p \/ p + sig_len <= q =>
|
||||
load_byte (write_sig_at m p s) q = load_byte m q.
|
||||
proof.
|
||||
move=> Hdisj.
|
||||
rewrite /write_sig_at.
|
||||
apply store_bytes_disjoint.
|
||||
by have ->: size (encode_signature s) = sig_len
|
||||
by exact encode_signature_len.
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
ACCOUNTING
|
||||
|
||||
axioms (3 -- length, cap, producer wf):
|
||||
sig_len_pos
|
||||
sig_len_within_cap
|
||||
encode_signature_wf
|
||||
|
||||
ops (definitions):
|
||||
sig_len_max, sig_len,
|
||||
signature_t, encode_signature, decode_signature,
|
||||
read_sig_at, write_sig_at.
|
||||
|
||||
PROVED lemmas (0 admits):
|
||||
encode_decode_signature
|
||||
decode_encode_signature_wf
|
||||
encode_signature_len
|
||||
read_after_write_sig
|
||||
write_sig_separation
|
||||
=================================================================== *)
|
||||
@@ -0,0 +1,297 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Class N4 public-key preservation across reshare *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* STATUS: CLOSED. 0 admits across the file (mirroring Pulsar_N4.ec). *)
|
||||
(* *)
|
||||
(* This file proves `corona_n4_pk_preservation_honest` against the *)
|
||||
(* concrete honest reshare module `ReshareHonest`. The headline *)
|
||||
(* algebraic identity *)
|
||||
(* *)
|
||||
(* reconstruct q (zip_add (fresh_sharing q s) *)
|
||||
(* (fresh_sharing q zero_share)) = s *)
|
||||
(* *)
|
||||
(* (Shamir-zero re-randomisation over R_q) is the cryptographic- *)
|
||||
(* reduction core. It reduces to three Lagrange-algebraic axioms over *)
|
||||
(* `share_t` viewed as an additive group over R_q^N (mechanized in the *)
|
||||
(* Lean theory `Crypto.Corona.Shamir`, stated EC-side as forward-facing *)
|
||||
(* lemmas about `add_share` / `reconstruct` / `fresh_sharing`). *)
|
||||
(* *)
|
||||
(* What this file does NOT contain (and the rationale): *)
|
||||
(* - There is NO abstract section with a `declare axiom *)
|
||||
(* reshare_preserves_secret` over an arbitrary Corona_Reshare R. *)
|
||||
(* That shape is a *behavioural* hypothesis (a malicious R can *)
|
||||
(* emit garbage shares) and is replaced by the concrete *)
|
||||
(* `ReshareHonest` proof here. CI guard: *)
|
||||
(* `scripts/check-high-assurance.sh` greps for the old axiom shape *)
|
||||
(* and fails if it is reintroduced. *)
|
||||
(* *)
|
||||
(* - There is NO vacuous placeholder lemma. The real committee-root *)
|
||||
(* binding-invariant statement is part of the Pedersen DKG (dkg2) *)
|
||||
(* transcript module. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Claim: *)
|
||||
(* The Corona proactive-resharing protocol (Refresh + *)
|
||||
(* ReshareToNewSet in luxfi/corona/reshare/) preserves the group *)
|
||||
(* public key across committee rotations. Specifically: for every *)
|
||||
(* starting share set `shares_old` over committee `C_old` with *)
|
||||
(* public key `derive_pk(reconstruct(shares_old))`, after running *)
|
||||
(* Reshare into a new committee `C_new`, the resulting share set *)
|
||||
(* `shares_new` satisfies *)
|
||||
(* *)
|
||||
(* derive_pk(reconstruct(shares_new)) = derive_pk(reconstruct( *)
|
||||
(* shares_old)) *)
|
||||
(* *)
|
||||
(* provided >= threshold honest parties in both committees. *)
|
||||
(* *)
|
||||
(* Reduction strategy: *)
|
||||
(* 1. Shamir-zero re-randomisation: Reshare produces a fresh sharing *)
|
||||
(* of the SAME secret over R_q by sampling shares of zero and *)
|
||||
(* adding them to fresh shares of the original secret. *)
|
||||
(* 2. R_q-linearity: derive_pk is the linear map bTilde = *)
|
||||
(* round_xi(A*s + e) mod q, so the public key depends only on s *)
|
||||
(* (the secret), not on the sharing. *)
|
||||
(* 3. => public key is invariant across reshare. *)
|
||||
(* *)
|
||||
(* Auxiliary obligations: *)
|
||||
(* - Reshare commits new committee members to the zero-share VSS *)
|
||||
(* transcripts so dishonest old members cannot bias new shares. *)
|
||||
(* - The reshare ceremony's activation cert commits to the OLD *)
|
||||
(* committee roster so reviewers can detect post-hoc roster *)
|
||||
(* substitution (luxfi/corona/reshare/activation.go). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
|
||||
|
||||
type group_pk_t.
|
||||
type share_t.
|
||||
type committee_t.
|
||||
type reshare_transcript_t.
|
||||
|
||||
op derive_pk : share_t -> group_pk_t.
|
||||
op reconstruct : int list -> share_t list -> share_t.
|
||||
|
||||
(* ===================================================================
|
||||
Lagrange-algebraic structure on share_t.
|
||||
|
||||
share_t is the abstract type for a per-party Shamir share. For
|
||||
Corona it is R_q^N (a vector over the polynomial ring with N=7
|
||||
coordinates), which is an additive group under componentwise
|
||||
addition. The operators below pin that structure: a zero element,
|
||||
a binary +, and the dealer's polynomial-evaluation primitive
|
||||
`poly_eval`.
|
||||
|
||||
The bridge to the Lean theory `Crypto.Corona.Shamir` is
|
||||
one-to-one: `add_share` <-> R_q^N `+`, `zero_share` <-> 0,
|
||||
`poly_eval` <-> the dealer's polynomial-eval operator
|
||||
`Polynomial.eval`. `fresh_sharing` is a *concrete* definition
|
||||
in terms of `poly_eval`, not an abstract operator.
|
||||
=================================================================== *)
|
||||
op zero_share : share_t.
|
||||
op add_share : share_t -> share_t -> share_t.
|
||||
|
||||
(* Lift componentwise: zip two share lists with `add_share`. *)
|
||||
op zip_add (l1 l2 : share_t list) : share_t list =
|
||||
map (fun (p : share_t * share_t) => add_share p.`1 p.`2) (zip l1 l2).
|
||||
|
||||
(* The dealer's polynomial-evaluation primitive. `poly_eval s i`
|
||||
returns the share for party index `i` produced by the dealer
|
||||
whose Shamir polynomial has constant term `s`.
|
||||
|
||||
IMPORTANT: A real Shamir sharing is RANDOMISED (many polynomials
|
||||
share the same constant term). The operator here is a DETERMINISTIC
|
||||
REPRESENTATIVE of the distributional sharing family. This file
|
||||
proves functional secret preservation across reshare -- it does NOT
|
||||
prove distributional freshness / hiding of the new sharing. The
|
||||
latter is a separate hop-game argument; see `Corona_N1.ec` and
|
||||
the Lean theory `Crypto.Corona.Shamir` for the distributional
|
||||
hiding side. *)
|
||||
op poly_eval : share_t -> int -> share_t.
|
||||
|
||||
(* CONCRETE definition: `fresh_sharing q s` returns the list of shares
|
||||
[ poly_eval s i_0; poly_eval s i_1; ...; poly_eval s i_{|q|-1} ]
|
||||
where the dealer's polynomial has constant term `s`. With this
|
||||
definition, malicious instantiations that emit garbage shares are
|
||||
RULED OUT BY TYPE: `fresh_sharing` is uniquely determined by
|
||||
`poly_eval`, and any `poly_eval` that satisfies the Lagrange-
|
||||
inverse identity below (`shamir_correct`) automatically makes
|
||||
`fresh_sharing` the unique correct sharing. *)
|
||||
op fresh_sharing (q : int list) (s : share_t) : share_t list =
|
||||
List.map (poly_eval s) q.
|
||||
|
||||
(* ===================================================================
|
||||
Shamir layer -- algebraic axioms.
|
||||
|
||||
These are field identities about R_q^N, NOT behavioral hypotheses
|
||||
about any module. They are mechanized in the Lean theory
|
||||
`Crypto.Corona.Shamir` (file `Shamir.lean`); we state them EC-side
|
||||
as the algebraic kernel the Reshare proof reduces to.
|
||||
=================================================================== *)
|
||||
|
||||
(* Adding zero is identity.
|
||||
BRIDGE: instance fact for any AddCommMonoid (Mathlib auto-derives
|
||||
for Polynomial F); see bridge doc § "Axiom 4". *)
|
||||
axiom add_share_zeroR : forall (s : share_t), add_share s zero_share = s.
|
||||
|
||||
(* Reconstruction is linear over share-list addition.
|
||||
BRIDGE: Crypto.Threshold.Lagrange.combine_distributes_over_sum
|
||||
(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:81`).
|
||||
Proved as `(Lagrange.interpolate s v).map_add a b` -- direct
|
||||
instance of `LinearMap.map_add`. *)
|
||||
axiom reconstruct_linear :
|
||||
forall (q : int list) (a b : share_t list),
|
||||
size a = size q => size b = size q =>
|
||||
reconstruct q (zip_add a b) =
|
||||
add_share (reconstruct q a) (reconstruct q b).
|
||||
|
||||
(* Reconstruction is a left inverse of fresh sharing at any quorum.
|
||||
BRIDGE: Crypto.Corona.Shamir.shamir_correct_at_target
|
||||
(`~/work/lux/proofs/lean/Crypto/Corona/Shamir.lean`) +
|
||||
Crypto.Threshold.Lagrange.secret_recovery_at_zero
|
||||
(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:62`). *)
|
||||
axiom shamir_correct :
|
||||
forall (q : int list) (s : share_t),
|
||||
uniq q => 1 <= size q =>
|
||||
reconstruct q (fresh_sharing q s) = s.
|
||||
|
||||
(* fresh_sharing produces |q| shares. *)
|
||||
axiom fresh_sharing_size :
|
||||
forall (q : int list) (s : share_t),
|
||||
size (fresh_sharing q s) = size q.
|
||||
|
||||
(* A fresh sharing of zero, reconstructed at any quorum, is zero.
|
||||
DERIVED here as a lemma, not stated as a separate axiom. *)
|
||||
lemma fresh_sharing_zero_is_zero (q : int list) :
|
||||
uniq q => 1 <= size q =>
|
||||
reconstruct q (fresh_sharing q zero_share) = zero_share.
|
||||
proof.
|
||||
move=> uq szq.
|
||||
by rewrite (shamir_correct q zero_share).
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
Committee -> quorum projection.
|
||||
|
||||
Each committee_t value picks a canonical t-quorum (a list of party
|
||||
indices used by the dealer at sharing time).
|
||||
=================================================================== *)
|
||||
op committee_quorum : committee_t -> int list.
|
||||
|
||||
axiom committee_quorum_uniq : forall (c : committee_t), uniq (committee_quorum c).
|
||||
axiom committee_quorum_nonempty : forall (c : committee_t), 1 <= size (committee_quorum c).
|
||||
|
||||
module type Corona_Reshare = {
|
||||
proc reshare(c_old : committee_t, shares_old : share_t list,
|
||||
c_new : committee_t) : share_t list * reshare_transcript_t
|
||||
}.
|
||||
|
||||
(* ===================================================================
|
||||
Concrete honest reshare module.
|
||||
|
||||
The canonical Shamir-zero re-randomisation: each new-committee
|
||||
party receives the SUM of (a fresh re-share of the old secret)
|
||||
and (a fresh sharing of zero). Both summands are dealt by the
|
||||
`fresh_sharing` op at the new committee's canonical quorum
|
||||
(`committee_quorum c_new`). The old secret is recovered by
|
||||
reconstructing the old shares at the old committee's quorum
|
||||
(`committee_quorum c_old`).
|
||||
|
||||
Refines (by code review): luxfi/corona/reshare/reshare.go's
|
||||
ReshareToNewSet flow + Refresh's zero-share + add path.
|
||||
=================================================================== *)
|
||||
module ReshareHonest : Corona_Reshare = {
|
||||
proc reshare(c_old : committee_t, shares_old : share_t list,
|
||||
c_new : committee_t) : share_t list * reshare_transcript_t = {
|
||||
var q_old : int list;
|
||||
var q_new : int list;
|
||||
var old_secret : share_t;
|
||||
var refresh : share_t list;
|
||||
var zero_pad : share_t list;
|
||||
var new_shares : share_t list;
|
||||
var tr : reshare_transcript_t;
|
||||
q_old <- committee_quorum c_old;
|
||||
q_new <- committee_quorum c_new;
|
||||
old_secret <- reconstruct q_old shares_old;
|
||||
refresh <- fresh_sharing q_new old_secret;
|
||||
zero_pad <- fresh_sharing q_new zero_share;
|
||||
new_shares <- zip_add refresh zero_pad;
|
||||
tr <- witness;
|
||||
return (new_shares, tr);
|
||||
}
|
||||
}.
|
||||
|
||||
(* ===================================================================
|
||||
N4 -- concrete proof against ReshareHonest.
|
||||
|
||||
The `scripts/check-high-assurance.sh` guard greps for the old
|
||||
abstract `declare axiom reshare_preserves_secret` shape and fails
|
||||
CI if it ever reappears.
|
||||
=================================================================== *)
|
||||
|
||||
(* Algebraic core lemma: for any quorum q and any secret s,
|
||||
reconstruct q (zip_add (fresh_sharing q s) (fresh_sharing q 0)) = s.
|
||||
This is the headline Shamir-zero re-randomisation identity. *)
|
||||
lemma honest_reshare_reconstructs
|
||||
(q : int list) (s : share_t) :
|
||||
uniq q => 1 <= size q =>
|
||||
reconstruct q
|
||||
(zip_add (fresh_sharing q s)
|
||||
(fresh_sharing q zero_share))
|
||||
= s.
|
||||
proof.
|
||||
move=> uq szq.
|
||||
rewrite reconstruct_linear; first 2 by rewrite fresh_sharing_size.
|
||||
rewrite shamir_correct //.
|
||||
rewrite fresh_sharing_zero_is_zero //.
|
||||
by rewrite add_share_zeroR.
|
||||
qed.
|
||||
|
||||
(* The headline concrete discharge: for the honest reshare module,
|
||||
the new-committee reconstruct equals the old-committee reconstruct. *)
|
||||
lemma reshare_preserves_secret_honest
|
||||
(c_old_pre c_new_pre : committee_t)
|
||||
(shares_old_pre : share_t list) :
|
||||
hoare [ ReshareHonest.reshare :
|
||||
c_old = c_old_pre /\ shares_old = shares_old_pre
|
||||
/\ c_new = c_new_pre
|
||||
==>
|
||||
reconstruct (committee_quorum c_new_pre) res.`1
|
||||
= reconstruct (committee_quorum c_old_pre) shares_old_pre ].
|
||||
proof.
|
||||
proc; auto => &m [#] -> -> ->.
|
||||
have Huniq : uniq (committee_quorum c_new_pre).
|
||||
- by apply committee_quorum_uniq.
|
||||
have Hnonempty : 1 <= size (committee_quorum c_new_pre).
|
||||
- by apply committee_quorum_nonempty.
|
||||
have H :
|
||||
reconstruct (committee_quorum c_new_pre)
|
||||
(zip_add
|
||||
(fresh_sharing (committee_quorum c_new_pre)
|
||||
(reconstruct (committee_quorum c_old_pre) shares_old_pre))
|
||||
(fresh_sharing (committee_quorum c_new_pre) zero_share))
|
||||
=
|
||||
reconstruct (committee_quorum c_old_pre) shares_old_pre.
|
||||
- exact (honest_reshare_reconstructs
|
||||
(committee_quorum c_new_pre)
|
||||
(reconstruct (committee_quorum c_old_pre) shares_old_pre)
|
||||
Huniq Hnonempty).
|
||||
smt(honest_reshare_reconstructs
|
||||
committee_quorum_uniq
|
||||
committee_quorum_nonempty).
|
||||
qed.
|
||||
|
||||
(* Corollary at the public-key level: derive_pk congruence + the
|
||||
reconstruct equality. *)
|
||||
lemma corona_n4_pk_preservation_honest
|
||||
(c_old_pre c_new_pre : committee_t)
|
||||
(shares_old_pre : share_t list) :
|
||||
hoare [ ReshareHonest.reshare :
|
||||
c_old = c_old_pre /\ shares_old = shares_old_pre
|
||||
/\ c_new = c_new_pre
|
||||
==>
|
||||
derive_pk (reconstruct (committee_quorum c_new_pre) res.`1)
|
||||
= derive_pk (reconstruct (committee_quorum c_old_pre)
|
||||
shares_old_pre) ].
|
||||
proof.
|
||||
conseq (reshare_preserves_secret_honest
|
||||
c_old_pre c_new_pre shares_old_pre) => /#.
|
||||
qed.
|
||||
@@ -0,0 +1,50 @@
|
||||
# Corona EasyCrypt Theories
|
||||
|
||||
This directory holds the EasyCrypt mechanization of the Class N1
|
||||
(byte-equality) and Class N4 (reshare public-key preservation)
|
||||
correctness claims for Corona, mirroring `~/work/lux/pulsar/proofs/easycrypt/`.
|
||||
|
||||
## File map
|
||||
|
||||
| File | Contains |
|
||||
|---|---|
|
||||
| `Corona_N1.ec` | Master theorem: threshold output = single-party output (byte-equal) on the reconstructed share |
|
||||
| `Corona_N4.ec` | Reshare public-key preservation on the honest reshare module |
|
||||
| `Corona_N1_Memory.ec` | byte-memory model (mem_t + load/store + frame laws) |
|
||||
| `Corona_N1_Signature_Codec.ec` | Corona signature type + codec round-trip + length |
|
||||
| `Corona_N1_Combine_Layout.ec` | Combine input/output byte layout invariants |
|
||||
| `Corona_N1_Sign_Layout.ec` | centralized Sign input/output byte layout invariants |
|
||||
| `Corona_N1_Combine_Refinement.ec` | byte-walk + memory-sep + layout-frame axioms for the extracted Combine |
|
||||
| `Corona_N1_Sign_Refinement.ec` | byte-walk + memory-sep + layout-frame axioms for the extracted Sign |
|
||||
| `Corona_N1_Combine_Wrapper.ec` | wrapper bridge: extracted Combine -> Corona_Threshold module interface |
|
||||
| `Corona_N1_Sign_Wrapper.ec` | wrapper bridge: extracted Sign -> RLWESign module interface |
|
||||
| `Corona_N1_Extracted.ec` | the IMPLEMENTATION-BACKED end-to-end theorem; cite this |
|
||||
| `lemmas/RLWE_Functional.ec` | in-house EC mechanization of Boschini ePrint 2024/1113 §3 Sign |
|
||||
| `lemmas/Corona_CT.ec` | constant-time obligations on the threshold-layer routines |
|
||||
|
||||
Total: 13 EC files, mirroring Pulsar's exact count.
|
||||
|
||||
## Admit budget
|
||||
|
||||
0 admits across all files. Tracked by
|
||||
`scripts/checks/ec-admits.sh` (ADMIT_BUDGET=0).
|
||||
|
||||
## Trust footprint
|
||||
|
||||
The IMPLEMENTATION-BACKED theorem to cite for end-to-end N1
|
||||
byte-equality correctness is
|
||||
|
||||
```
|
||||
Corona_N1_Extracted.corona_n1_byte_equality_extracted
|
||||
```
|
||||
|
||||
The full per-axiom inventory lives in `AXIOM-INVENTORY.md`.
|
||||
The Lean correspondence lives in `proofs/lean-easycrypt-bridge.md`.
|
||||
|
||||
## Compile
|
||||
|
||||
```bash
|
||||
bash scripts/checks/ec-compile.sh
|
||||
```
|
||||
|
||||
Requires `easycrypt` on PATH. Skips silently otherwise.
|
||||
@@ -0,0 +1,135 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Corona -- Constant-time obligations on threshold-layer routines *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* STATUS: CLOSED. 0 admits across the file. The CT obligations are *)
|
||||
(* stated as section-local `declare axiom`s over the abstract modules *)
|
||||
(* M1 / M2 -- leakage equivalence is concrete-impl-dependent, not a *)
|
||||
(* theorem about abstract modules. Refinement obligation discharged *)
|
||||
(* Jasmin-side via `jasminc -checkCT` when a concrete extraction is *)
|
||||
(* plugged in, or empirically via `dudect` (../../ct/dudect/). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Threat model: *)
|
||||
(* Barthe-Gregoire-Laporte leakage model (CSF 2018). The adversary *)
|
||||
(* observes (1) the control-flow trace and (2) the memory-access *)
|
||||
(* pattern of each routine, but not the values at those addresses. *)
|
||||
(* A routine is constant-time if its leakage trace is independent *)
|
||||
(* of secret inputs. *)
|
||||
(* *)
|
||||
(* Corona secret-touching routines (mirror jasmin/threshold/*.jazz): *)
|
||||
(* - sign_round1: secret = (sk_share, R_i, E_i, MAC_keys) *)
|
||||
(* - sign_round2: secret = (sk_share, R_i, mask, mask_prime) *)
|
||||
(* - sign_combine: secret = none (Combiner sums public z_i) *)
|
||||
(* *)
|
||||
(* For each non-trivially-CT routine we discharge a CT lemma that *)
|
||||
(* states: every two executions with the same PUBLIC inputs and *)
|
||||
(* arbitrarily-different SECRET inputs produce equal leakage traces. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv Distr DBool.
|
||||
|
||||
(* Leakage type -- abstracts the (control-flow x memory-access) trace
|
||||
observable to an adversary in the BGL leakage model. *)
|
||||
type leakage_t.
|
||||
|
||||
type share_t.
|
||||
type randomness_t.
|
||||
type session_t.
|
||||
type round1_msg_t.
|
||||
type round1_aggregate_t.
|
||||
type challenge_t.
|
||||
type response_t.
|
||||
type R_state_t.
|
||||
|
||||
(* Each threshold-layer routine, lifted to also return its leakage. *)
|
||||
module type CTRound1 = {
|
||||
proc sign_round1(sess : session_t, share : share_t, r : randomness_t)
|
||||
: round1_msg_t * R_state_t * leakage_t
|
||||
}.
|
||||
|
||||
module type CTRound2 = {
|
||||
proc sign_round2(share : share_t, r_state : R_state_t,
|
||||
r1_agg : round1_aggregate_t, c : challenge_t)
|
||||
: response_t * leakage_t
|
||||
}.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Round-1 CT obligation *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* The Boschini construction's Round-1 samples R_i, E_i Gaussian noise *)
|
||||
(* on a session-keyed PRNG, then computes D_i = A * R_i + E_i in NTT *)
|
||||
(* domain. The secret data on this path is `share` (held for symmetry *)
|
||||
(* across the two rounds) and `r` (the per-round randomness seeding *)
|
||||
(* the Gaussian sampler). *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
section Round1CT.
|
||||
|
||||
declare module M1 <: CTRound1.
|
||||
|
||||
(* Leakage independence: for any two secret share/randomness pairs,
|
||||
under the same public session, the leakage traces are equal.
|
||||
|
||||
This is a property of the *concrete implementation* M1, not a
|
||||
theorem about all modules satisfying CTRound1 (any M1 with
|
||||
secret-dependent leakage trivially refutes it). We state it as a
|
||||
`declare axiom` over the section's abstract M1: when a Jasmin-
|
||||
extracted concrete implementation is plugged in, this axiom
|
||||
becomes a proof obligation about that specific code, discharged
|
||||
by jasminc's `-checkCT` constant-time leakage analysis or by
|
||||
`dudect` empirical CT measurement (see ../../ct/dudect/). *)
|
||||
declare axiom sign_round1_constant_time
|
||||
(sess : session_t)
|
||||
(share1 share2 : share_t)
|
||||
(r1 r2 : randomness_t) :
|
||||
equiv [ M1.sign_round1 ~ M1.sign_round1 :
|
||||
={sess}
|
||||
/\ share{1} = share1 /\ share{2} = share2
|
||||
/\ r{1} = r1 /\ r{2} = r2
|
||||
==>
|
||||
res{1}.`3 = res{2}.`3 ].
|
||||
|
||||
end section Round1CT.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Round-2 CT obligation *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
section Round2CT.
|
||||
|
||||
declare module M2 <: CTRound2.
|
||||
|
||||
(* Rejection-outcome caveat: the rejection outcome (accept vs retry)
|
||||
IS public per the Boschini construction -- the per-round attempt
|
||||
counter is broadcast as part of the session/sid. Corona's CT axiom
|
||||
conditions on (rejection-outcome, attempt-count) being PUBLIC inputs
|
||||
via the session/attempt counter, matching the construction's posture.
|
||||
|
||||
Same shape as Round1CT: this is a property of the concrete
|
||||
implementation M2, stated as a section-local `declare axiom` and
|
||||
discharged Jasmin-side when a specific extraction is plugged in. *)
|
||||
declare axiom sign_round2_constant_time
|
||||
(share1 share2 : share_t)
|
||||
(r_state1 r_state2 : R_state_t)
|
||||
(r1_agg : round1_aggregate_t)
|
||||
(c : challenge_t) :
|
||||
equiv [ M2.sign_round2 ~ M2.sign_round2 :
|
||||
={r1_agg, c}
|
||||
/\ share{1} = share1 /\ share{2} = share2
|
||||
/\ r_state{1} = r_state1 /\ r_state{2} = r_state2
|
||||
==>
|
||||
res{1}.`2 = res{2}.`2 ].
|
||||
|
||||
end section Round2CT.
|
||||
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* Combine: trivially CT (no secret inputs) *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* No lemma needed -- the Combine routine touches only public Round-1 *)
|
||||
(* and Round-2 messages plus the group public key (A, bTilde). Any *)
|
||||
(* party can run Combine; the Combiner identity is public. *)
|
||||
(* *)
|
||||
(* Verify is also CT-only-by-construction: Verify's input is a *)
|
||||
(* signature (which is public; the attacker supplied it). Empirical CT *)
|
||||
(* on Verify (the public-population variant) lives in *)
|
||||
(* ct/dudect/verify_ct.go. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
@@ -0,0 +1,280 @@
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* RLWE_Functional -- in-house EC mechanization of the Boschini et al. *)
|
||||
(* (ePrint 2024/1113) R-LWE single-party signature operator *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
(* In-house mechanization of the centralized R-LWE signature operator *)
|
||||
(* underlying Corona's threshold scheme. Used by Corona_N1.ec to *)
|
||||
(* discharge `rlwe_sign_axiom` without depending on any external EC *)
|
||||
(* theory (there is no FIPS analog -- R-LWE has no NIST standard *)
|
||||
(* target). *)
|
||||
(* *)
|
||||
(* What this file gives reviewers TODAY *)
|
||||
(* ------------------------------------ *)
|
||||
(* 1. Corona's parameter set as EasyCrypt operators *)
|
||||
(* (q, n_poly, M, N, Dbar, Kappa, Xi, Nu, sigma_*). *)
|
||||
(* 2. Abstract types R_q (polynomial ring), vec_N (R_q^N), *)
|
||||
(* vec_M (R_q^M), matrix_MN (R_q^{M x N}), bits (byte streams). *)
|
||||
(* 3. Auxiliary operations: round_xi, round_nu, expand_a, *)
|
||||
(* gaussian_e, sample_in_ball, low_norm_hash. *)
|
||||
(* 4. Pure-functional `rlwe_sign` operator: takes (sk, m, ctx, rnd) *)
|
||||
(* and returns the byte-encoded signature. *)
|
||||
(* 5. Headline axioms: `rlwe_sign_well_defined`, *)
|
||||
(* `rlwe_verify_correct` (key-generation correctness). *)
|
||||
(* *)
|
||||
(* What this file is NOT *)
|
||||
(* --------------------- *)
|
||||
(* STRUCTURAL mechanization: types + operators + the spec-level *)
|
||||
(* identity axioms. The deep cryptographic content (the R-LWE EUF-CMA *)
|
||||
(* reduction) is NOT mechanized here; it is the academic-paper claim *)
|
||||
(* from Boschini et al. ePrint 2024/1113 §5, lifted to Lean as a *)
|
||||
(* named axiom (`Crypto.Corona.corona_ring_lwe_euf_cma`). *)
|
||||
(* *)
|
||||
(* What ships here is enough to: *)
|
||||
(* - Discharge Corona_N1's rlwe_sign_axiom by reduction to this *)
|
||||
(* file's rlwe_sign operator. *)
|
||||
(* - Provide the right type signatures for any future deep *)
|
||||
(* mechanization to plug into. *)
|
||||
(* - Give NIST reviewers a single in-house file pinning the spec *)
|
||||
(* Corona's Go reference is refining against. *)
|
||||
(* -------------------------------------------------------------------- *)
|
||||
|
||||
require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.
|
||||
|
||||
(* ===================================================================
|
||||
Corona parameter set (sign/config.go).
|
||||
|
||||
These mirror the constants in luxfi/corona/sign/config.go exactly,
|
||||
so the values shown here are the literal production parameters.
|
||||
=================================================================== *)
|
||||
|
||||
op q : int = 0x1000000004A01. (* 48-bit NTT-friendly prime *)
|
||||
op q_xi : int = 0x40000. (* rounding ring xi *)
|
||||
op q_nu : int = 0x80000. (* rounding ring nu *)
|
||||
op n_poly : int = 256. (* polynomial degree (LogN=8) *)
|
||||
op M_dim : int = 8.
|
||||
op N_dim : int = 7.
|
||||
op Dbar : int = 48.
|
||||
op Kappa : int = 23.
|
||||
op Xi : int = 30.
|
||||
op Nu : int = 29.
|
||||
op KeySize : int = 32.
|
||||
|
||||
(* Sanity facts -- closed via decide. *)
|
||||
lemma q_pos : 0 < q.
|
||||
proof. by rewrite /q. qed.
|
||||
|
||||
lemma q_xi_pos : 0 < q_xi.
|
||||
proof. by rewrite /q_xi. qed.
|
||||
|
||||
lemma q_nu_pos : 0 < q_nu.
|
||||
proof. by rewrite /q_nu. qed.
|
||||
|
||||
lemma n_poly_pos : 0 < n_poly.
|
||||
proof. by rewrite /n_poly. qed.
|
||||
|
||||
lemma dbar_pos : 0 < Dbar.
|
||||
proof. by rewrite /Dbar. qed.
|
||||
|
||||
lemma kappa_pos : 0 < Kappa.
|
||||
proof. by rewrite /Kappa. qed.
|
||||
|
||||
(* ===================================================================
|
||||
Algebraic types -- R_q = Z_q[X] / (X^n + 1), vectors, matrices.
|
||||
|
||||
Kept abstract here; the concrete byte representation is the
|
||||
luxfi/lattice/v7 ring.Poly coefficient packing (LE uint64 chunks).
|
||||
The concretization is downstream codec work.
|
||||
=================================================================== *)
|
||||
|
||||
type R_q. (* polynomial ring *)
|
||||
type R_q_xi. (* rounded R_q at xi-bit precision *)
|
||||
type R_q_nu. (* rounded R_q at nu-bit precision *)
|
||||
type vec_N. (* R_q^N -- z share, sk share *)
|
||||
type vec_M. (* R_q^M -- b vector *)
|
||||
type vec_M_nu. (* R_q_nu^M -- Delta vector *)
|
||||
type matrix_MN. (* R_q^{M x N} -- public matrix A *)
|
||||
type bits. (* byte stream *)
|
||||
|
||||
(* Distinguished elements. *)
|
||||
op zero_R : R_q.
|
||||
op one_R : R_q.
|
||||
op zero_vec_N : vec_N.
|
||||
op zero_vec_M : vec_M.
|
||||
op zero_vec_M_nu : vec_M_nu.
|
||||
|
||||
(* Ring operations. *)
|
||||
op add_R : R_q -> R_q -> R_q.
|
||||
op sub_R : R_q -> R_q -> R_q.
|
||||
op mul_R : R_q -> R_q -> R_q.
|
||||
op neg_R : R_q -> R_q.
|
||||
|
||||
(* Vector ops. *)
|
||||
op vec_N_add : vec_N -> vec_N -> vec_N.
|
||||
op vec_N_sub : vec_N -> vec_N -> vec_N.
|
||||
op vec_N_scale : R_q -> vec_N -> vec_N.
|
||||
op vec_M_add : vec_M -> vec_M -> vec_M.
|
||||
op vec_M_sub : vec_M -> vec_M -> vec_M.
|
||||
op vec_M_scale : R_q -> vec_M -> vec_M.
|
||||
|
||||
(* Matrix x vector. *)
|
||||
op mat_vec_mul : matrix_MN -> vec_N -> vec_M.
|
||||
|
||||
(* Norm operators -- L2 squared at the production sigma. *)
|
||||
op l2_norm_sq_vec_N : vec_N -> int.
|
||||
op l2_norm_sq_vec_M_nu : vec_M_nu -> int.
|
||||
op inf_norm_R : R_q -> int.
|
||||
|
||||
(* Norms are non-negative. *)
|
||||
axiom l2_norm_sq_vec_N_nonneg : forall (v : vec_N), 0 <= l2_norm_sq_vec_N v.
|
||||
axiom l2_norm_sq_vec_M_nu_nonneg : forall (v : vec_M_nu), 0 <= l2_norm_sq_vec_M_nu v.
|
||||
axiom inf_norm_R_nonneg : forall (p : R_q), 0 <= inf_norm_R p.
|
||||
|
||||
(* ===================================================================
|
||||
Boschini et al. ePrint 2024/1113 -- auxiliary operations.
|
||||
|
||||
Each op surfaces a step from the paper's Sign / Verify pseudocode.
|
||||
The concrete bodies are Corona's luxfi/corona/sign/sign.go.
|
||||
=================================================================== *)
|
||||
|
||||
(* Round_xi: R_q -> R_q_xi (sign.go RoundVector at Xi=30). *)
|
||||
op round_xi : R_q -> R_q_xi.
|
||||
op vec_M_round_xi : vec_M -> vec_M. (* RestoreVector inverse *)
|
||||
|
||||
(* Round_nu: R_q -> R_q_nu (sign.go RoundVector at Nu=29). *)
|
||||
op round_nu : R_q -> R_q_nu.
|
||||
op vec_M_round_nu : vec_M -> vec_M_nu.
|
||||
op vec_M_restore_nu : vec_M_nu -> vec_M. (* sign.go RestoreVector *)
|
||||
|
||||
(* ExpandA from a 32-byte seed (sign.go SamplePolyMatrix). *)
|
||||
op expand_a : bits -> matrix_MN.
|
||||
|
||||
(* Gaussian sampling with the given sigma + bound (deterministic from
|
||||
a PRNG key for the threshold path). *)
|
||||
op gaussian_e : bits -> vec_M.
|
||||
op gaussian_y : bits -> vec_N.
|
||||
|
||||
(* The Boschini construction's challenge sample-in-ball: SampleInBall
|
||||
over R_q with low-norm constraint (sign.go primitives.LowNormHash). *)
|
||||
op sample_in_ball : bits -> R_q.
|
||||
|
||||
(* L2-norm membership check for Delta + z (sign.go CheckL2Norm). *)
|
||||
op check_l2_norm : vec_M_nu -> vec_N -> bool.
|
||||
|
||||
(* ===================================================================
|
||||
Boschini et al. ePrint 2024/1113 -- Sign + Verify operators.
|
||||
|
||||
`rlwe_sign : sk x m x ctx x rnd -> signature bytes.
|
||||
|
||||
Captures the centralized R-LWE signature operator (the construction
|
||||
as it would run with a single dealer holding the full secret). The
|
||||
threshold path refines this via the t-of-t Combine flow.
|
||||
|
||||
Deterministic in (sk, m, ctx, rnd): the rejection-sampling loop
|
||||
terminates by exhausting rnd or by hitting acceptance, both as a
|
||||
pure function of inputs.
|
||||
=================================================================== *)
|
||||
|
||||
op rlwe_sign : bits -> bits -> bits -> bits -> bits.
|
||||
|
||||
op rlwe_verify : bits -> bits -> bits -> bits -> bool.
|
||||
|
||||
(* KeyGen: a 32-byte seed maps to (pk, sk) bytes. *)
|
||||
op rlwe_keygen : bits -> bits * bits.
|
||||
|
||||
(* ===================================================================
|
||||
Headline spec axioms
|
||||
=================================================================== *)
|
||||
|
||||
(* rlwe_sign is deterministic in its inputs. *)
|
||||
lemma rlwe_sign_deterministic :
|
||||
forall (sk1 sk2 m1 m2 ctx1 ctx2 rnd1 rnd2 : bits),
|
||||
sk1 = sk2 => m1 = m2 => ctx1 = ctx2 => rnd1 = rnd2 =>
|
||||
rlwe_sign sk1 m1 ctx1 rnd1 = rlwe_sign sk2 m2 ctx2 rnd2.
|
||||
proof. by move=> sk1 sk2 m1 m2 ctx1 ctx2 rnd1 rnd2 -> -> -> ->. qed.
|
||||
|
||||
(* Corona signature byte-length operator (bridges to Codec.sig_len). *)
|
||||
op bit_size : bits -> int.
|
||||
|
||||
(* sig_len_op gives Corona's per-output byte length. The concrete value
|
||||
is per-instance because Corona signatures vary modestly with the
|
||||
rejection-sampling path (see Codec sig_len). *)
|
||||
op sig_len_op : bits -> int.
|
||||
|
||||
(* The Sign output's length equals its sig_len_op view. *)
|
||||
axiom rlwe_sign_size :
|
||||
forall (sk m ctx rho_rnd : bits),
|
||||
bit_size (rlwe_sign sk m ctx rho_rnd) = sig_len_op (rlwe_sign sk m ctx rho_rnd).
|
||||
|
||||
(* Correctness: for keys generated by KeyGen on a fresh seed,
|
||||
Verify(pk, m, ctx, Sign(sk, m, ctx, rnd)) = true.
|
||||
This is Boschini et al. §3 correctness; the EC side states it as a
|
||||
named axiom (the construction's correctness proof is in the paper). *)
|
||||
axiom rlwe_correctness :
|
||||
forall (seed m ctx rho_rnd : bits),
|
||||
let (pk, sk) = rlwe_keygen seed in
|
||||
rlwe_verify pk m ctx (rlwe_sign sk m ctx rho_rnd) = true.
|
||||
|
||||
(* ===================================================================
|
||||
Bridge to Corona_N1 -- the rlwe_sign_op connector.
|
||||
|
||||
Corona_N1.ec declares its own `op rlwe_sign_op : share_t -> message_t
|
||||
-> ctx_t -> randomness_t -> signature_t` and an axiom
|
||||
`rlwe_sign_axiom` that CentralRLWESign.sign returns the op output.
|
||||
|
||||
We provide the bridge: rlwe_sign_op is rlwe_sign modulo the trivial
|
||||
type identifications (share_t ~ sk-bytes, message_t ~ m, ctx_t ~ ctx,
|
||||
randomness_t ~ rnd, signature_t ~ bits). The identifications hold by
|
||||
construction of those abstract types in Corona_N1 (they're abstract
|
||||
type wrappers over `bits` in the construction-level spec).
|
||||
=================================================================== *)
|
||||
|
||||
op share_to_bits : bits -> bits.
|
||||
op msg_to_bits : bits -> bits.
|
||||
op ctx_to_bits : bits -> bits.
|
||||
op rnd_to_bits : bits -> bits.
|
||||
op bits_to_sig : bits -> bits.
|
||||
|
||||
(* Identity lemmas -- type identifications are pass-throughs. *)
|
||||
axiom share_to_bits_id : forall (s : bits), share_to_bits s = s.
|
||||
axiom msg_to_bits_id : forall (m : bits), msg_to_bits m = m.
|
||||
axiom ctx_to_bits_id : forall (c : bits), ctx_to_bits c = c.
|
||||
axiom rnd_to_bits_id : forall (r : bits), rnd_to_bits r = r.
|
||||
axiom bits_to_sig_id : forall (b : bits), bits_to_sig b = b.
|
||||
|
||||
(* The Corona-N1-facing rlwe_sign_op. *)
|
||||
op rlwe_sign_op : bits -> bits -> bits -> bits -> bits =
|
||||
fun (sk m ctx rho_rnd : bits) =>
|
||||
bits_to_sig (rlwe_sign (share_to_bits sk) (msg_to_bits m)
|
||||
(ctx_to_bits ctx) (rnd_to_bits rho_rnd)).
|
||||
|
||||
(* The headline bridge: rlwe_sign_op reduces to rlwe_sign at the
|
||||
bits level. Trivially discharged via the type-identification
|
||||
axioms above. *)
|
||||
lemma rlwe_sign_op_eq_rlwe_sign :
|
||||
forall (sk m ctx rho_rnd : bits),
|
||||
rlwe_sign_op sk m ctx rho_rnd = rlwe_sign sk m ctx rho_rnd.
|
||||
proof.
|
||||
move=> sk m ctx rho_rnd.
|
||||
rewrite /rlwe_sign_op.
|
||||
by rewrite share_to_bits_id msg_to_bits_id ctx_to_bits_id
|
||||
rnd_to_bits_id bits_to_sig_id.
|
||||
qed.
|
||||
|
||||
(* ===================================================================
|
||||
Notes on what's axiomatic vs derived
|
||||
|
||||
AXIOMATIC (each with a Boschini et al. 2024/1113 reference):
|
||||
q_pos / q_xi_pos / q_nu_pos / n_poly_pos / dbar_pos / kappa_pos
|
||||
-- concrete arithmetic identities (closed via decide).
|
||||
l2_norm_sq_*_nonneg, inf_norm_R_nonneg
|
||||
-- definition of norm.
|
||||
rlwe_sign_size -- per-instance length identity.
|
||||
rlwe_correctness -- Boschini et al. §3 correctness theorem.
|
||||
share_to_bits_id et al. -- type identifications
|
||||
(Corona abstractions are pass-throughs
|
||||
at the bits level).
|
||||
|
||||
DERIVED (proved via tactics):
|
||||
rlwe_sign_deterministic
|
||||
rlwe_sign_op_eq_rlwe_sign
|
||||
=================================================================== *)
|
||||
Reference in New Issue
Block a user