pulsar/proofs/easycrypt/Pulsar_N4.ec

(* -------------------------------------------------------------------- *)
(* Pulsar — Class N4 public-key preservation across reshare           *)
(* -------------------------------------------------------------------- *)
(* STATUS: CLOSED. 0 admits across the file.                            *)
(*                                                                      *)
(* This file proves `pulsar_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) is the cryptographic-reduction core.  *)
(* It reduces to three Lagrange-algebraic axioms over `share_t` viewed  *)
(* as an additive group (mechanized in the Lean theory                  *)
(* `Crypto.Pulsar.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 Pulsar_Reshare R.    *)
(*     That shape is a *behavioural* hypothesis (a malicious R can      *)
(*     emit garbage shares) and was removed in favour of 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                            *)
(*     (`pulsar_n4_transcript_binds_committee` with postcondition       *)
(*     `true`). That stub was removed; the real committee-root          *)
(*     binding-invariant statement is part of the Pedersen DKG          *)
(*     transcript module and lives in study/pulsar.md.                  *)
(* -------------------------------------------------------------------- *)
(* Claim:                                                                *)
(*   The Pulsar proactive-resharing protocol (Reshare in              *)
(*   spec/pulsar.tex §4.5) 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 t = 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 accumulator commits to the OLD committee   *)
(*     roster (committeeRootFromShares) so reviewers can detect          *)
(*     post-hoc roster substitution.                                     *)
(* -------------------------------------------------------------------- *)

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
   ML-DSA-65 it is R_q^ell (a vector over the polynomial ring), which
   is an additive group under componentwise addition. The three
   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.Pulsar.Shamir` is
   one-to-one: `add_share` ↔ R_q^ell `+`, `zero_share` ↔ 0,
   `poly_eval` ↔ the dealer's polynomial-eval operator
   `Polynomial.eval`. `fresh_sharing` is now a *concrete* definition
   in terms of `poly_eval`, not an abstract operator (see below).
   =================================================================== *)
op zero_share : share_t.
op add_share  : share_t -> share_t -> share_t.

(* Lift componentwise: zip two share lists with `add_share`. Lists
   must be the same length and indexed by the same quorum positions. *)
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`. The same operator
   name + signature exists in `Pulsar_N1.ec`; both files use it
   identically.

   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 `Pulsar_N1.ec` and
   the Lean theory `Crypto.Pulsar.Shamir` for the distributional
   hiding side. The deterministic-representative choice is sound
   because for any concrete dealer randomness `r` we can plug `r`
   into the right-hand side of the sharing identities below and the
   same proof goes through — `poly_eval` is just the unhided
   "pure function" view of the dealer. *)
op poly_eval : share_t -> int -> share_t.

(* CONCRETE definition (no longer an abstract op): `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` (encoded in the
   `share_t` representative). 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.

   Closes the abstraction-gap critique in Agent 2's HIGH finding
   ("`fresh_sharing` could be a malicious adversary"). *)
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^ell, NOT behavioral hypotheses
   about any module. They are mechanized in the Lean theory
   `Crypto.Pulsar.Shamir` (file `Shamir.lean`); we state them EC-side
   as the algebraic kernel the Reshare proof reduces to.
   =================================================================== *)

(* BRIDGED TO LEAN: the three axioms below correspond 1:1 to proved
   Lean theorems in `~/work/lux/proofs/lean/Crypto/`. Inline citations
   given per-axiom; the full symbol-correspondence table lives in
   `proofs/lean-easycrypt-bridge.md` (§ "Axioms 2-4"). The EC side
   states them as axioms because EasyCrypt's first-order theory of
   finite-field polynomial interpolation is comparatively thin; the
   honest closure path (see bridge doc § "Future work") is to either
   mechanize them in EC or wire a Lean-proof-object consumer. *)

(* 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
   (Lagrange-at-zero identity).
   BRIDGE: Crypto.Pulsar.Shamir.shamir_correct_at_target
   (`~/work/lux/proofs/lean/Crypto/Pulsar/Shamir.lean:76`) +
   Crypto.Threshold.Lagrange.secret_recovery_at_zero
   (`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:62`).
   Same theorem as Axiom 1 in the bridge doc, applied to a
   `fresh_sharing` build. *)
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 (so zip_add against an
   old-quorum-length share list is well-typed). *)
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.
   This is an instance of `shamir_correct` at s = zero_share — 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). The protocol's
   "honest quorum" is this projection; concrete extensions to OTHER
   quorum-subsets follow from Shamir's quorum invariance (a separate
   algebraic identity not needed for the headline reshare property).
   =================================================================== *)
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 Pulsar_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`).
   =================================================================== *)
module ReshareHonest : Pulsar_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.

   We do NOT keep the old abstract section with its
   `declare axiom reshare_preserves_secret`: that shape is a
   *behavioural* assumption over an arbitrary R (a malicious R can
   emit garbage shares), and concrete cryptographic correctness must
   be discharged against a concrete honest module instead. The
   section + axiom version was removed in favour of the four-axiom
   Shamir-algebraic kernel above plus the `ReshareHonest` module.

   The `scripts/check-high-assurance.sh` guard greps for the old
   axiom 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.
   The quorums are the canonical committee quora — derived from the
   committee values, not free parameters. *)
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.
  (* The intermediate H makes the lemma instantiation transparent:
     it states the exact equality the body of `ReshareHonest.reshare`
     induces, discharged from `honest_reshare_reconstructs`
     specialised at q = committee_quorum c_new_pre and
     s = reconstruct (committee_quorum c_old_pre) shares_old_pre.
     The algebraic content is fully in this H; the closing smt only
     bridges the syntactic gap between auto's symbolic-execution
     normalisation and the lemma statement. *)
  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 pulsar_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.