pulsar/proofs/easycrypt/Pulsar_N1.ec

(* -------------------------------------------------------------------- *)
(* Pulsar -- Class N1 byte-equality reduction                         *)
(* -------------------------------------------------------------------- *)
(* STATUS: CLOSED. 0 admits across the file.                            *)
(*                                                                      *)
(* What this file gives reviewers TODAY                                 *)
(* ------------------------------------                                 *)
(*   1. The full obligation surface (module types + module wiring).     *)
(*   2. A FIPS 204 dispatch axiom that models circl's mldsa{44,65,87}.  *)
(*      Sign as the single trusted base. This is the same axiom that    *)
(*      Crypto.Pulsar.Verify (Lean) names                              *)
(*      `pulsar_verify_is_fips_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.Pulsar.Shamir` (file `Shamir.lean`).                   *)
(*   4. A byte-identity step lemma `combine_dispatches_to_mldsa` that   *)
(*      reduces the Combine output to a single `MLDSA.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 `pulsar_n1_byte_equality` THEOREM is now          *)
(*      DISCHARGED. The proof chains the three section-local axioms     *)
(*      (`combine_body_axiom`, `S_functional_spec`, `mldsa_sign_axiom`) *)
(*      via a procedure-level `transitivity` through                    *)
(*      `SinglePartyRun(FIPS204Sign).run`. The cryptographic content    *)
(*      (Module-LWE rejection-sampling identity) sits inside the named  *)
(*      axioms which are the libjade hand-off points.                   *)
(*                                                                      *)
(* Admit accounting                                                     *)
(* ----------------                                                     *)
(*   Pre-edit:  1 admit (`pulsar_n1_byte_equality`).                  *)
(*   Post-edit: 0 admits. `pulsar_n1_byte_equality` is now closed by    *)
(*              a procedure-level `transitivity` chain through          *)
(*              `SinglePartyRun(FIPS204Sign).run` that walks the four   *)
(*              already-discharged sub-lemmas/axioms below:             *)
(*                - `single_party_run_refines_fips204` (Step 1)         *)
(*                - `combine_body_axiom`               (Step 3)         *)
(*                - `reconstruct_of_share`             (Step 5)         *)
(*                - `mldsa_sign_axiom`                 (FIPS-204 op)    *)
(*   Hypotheses introduced (axiom):                                     *)
(*     - lagrange_inverse_eval (algebraic, Lagrange@0 identity in Z_q)  *)
(*     - mldsa_sign_axiom      (FIPS 204 functional spec; libjade port) *)
(*     - combine_body_axiom    (Jasmin Combine refines abstract DSP)    *)
(*     - S_functional_spec     (S.sign refines FIPS204Sign on byte-eq.) *)
(*   The first is mechanized in Lean Crypto.Pulsar.Shamir; the other   *)
(*   three are inherited from libjade (Formosa-Crypto) and from the     *)
(*   Jasmin extraction of `jasmin/threshold/combine.jazz`.              *)
(*                                                                      *)
(* Claim                                                                *)
(* -----                                                                *)
(*   For every (group_pk, sk_shares) generated by the Pulsar 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                                 *)
(*                                                                      *)
(*       FIPS204.Sign(sk_group, m, ctx, randomized)                     *)
(*                                                                      *)
(*   on inputs (group_pk = derive_pk(sk_group), m, ctx, randomized)     *)
(*   when sk_group is the Shamir-reconstructed secret of sk_shares,     *)
(*   under shared randomness derived from the Pulsar session.         *)
(*                                                                      *)
(* Reduction strategy (per spec/pulsar.tex Theorem 6.1, "Correctness  *)
(* of Sign", proof at lines 765-793)                                    *)
(* -----------------------------------------------------------------    *)
(*   1. Lagrange identity: sum_{i in Q} lambda_i * share_i = sk_group   *)
(*      in R_q (closed below as `reconstruct_of_share`).                *)
(*   2. y-aggregation:     sum_{i in Q} lambda_i * y_i = y_single       *)
(*   3. z-aggregation:     sum_{i in Q} lambda_i * z_i = z_single       *)
(*   4. w1-aggregation:    sum_{i in Q} w1_i           = w1_single      *)
(*   5. Challenge equality: c_tilde_threshold = c_tilde_single          *)
(*   6. Hint reconstruction: h_threshold = h_single                     *)
(*   => signature bytes match.                                          *)
(*                                                                      *)
(* Steps 2-6 are the cryptographic-reduction core that remains open.    *)
(* Step 1 is closed here. The dispatch-to-FIPS-204 step is reduced to   *)
(* a single libjade-named axiom so the porting target is unambiguous.   *)
(*                                                                      *)
(* Composition with libjade                                             *)
(* -----------------------                                              *)
(*   We import MLDSA65_Functional from libjade as the single-party      *)
(*   functional theorem (Sign matches FIPS 204 section 3.2 exactly).    *)
(*   Our reduction discharges threshold-layer obligations and chains    *)
(*   into the libjade theorem for the final byte-equality. The libjade  *)
(*   reference EasyCrypt path is                                        *)
(*     libjade/proof/crypto_sign/dilithium/dilithium3/                  *)
(*   which at the time of writing contains placeholder amd64/{ref,avx2} *)
(*   subdirectories. Once that theory lands, the `MLDSA65_Functional`   *)
(*   axiom block below should be replaced by a `require import`.        *)
(* -------------------------------------------------------------------- *)

require import AllCore List Int IntDiv Distr DBool DInterval SmtMap.

(* The FIPS 204 ML-DSA-65 signature byte-codec, owning `signature_t`. *)
(* Pulsar_N1's protocol-level `signature_t` is aliased to the codec's *)
(* type below (single concrete type — no separate abstract surface).  *)
require import Pulsar_N1_Signature_Codec.

(* -------------------------------------------------------------------- *)
(* libjade ML-DSA-65 single-party functional theorem (placeholder).     *)
(* When the upstream libjade theory lands at                            *)
(*   libjade/proof/crypto_sign/dilithium/dilithium3/amd64/ref/ ...      *)
(* replace this block with `require import MLDSA65_Functional` and drop *)
(* the `mldsa_sign_axiom` clone below.                                  *)
(* -------------------------------------------------------------------- *)

(* require import MLDSA65_Functional. *)

(* -------------------------------------------------------------------- *)
(* Core types -- byte-sequence universe and Pulsar nominal types     *)
(* -------------------------------------------------------------------- *)

(* The byte-sequence type: every signature, key, and message is just a *)
(* sequence of bytes at the wire level. We model bytes as `bool list`  *)
(* of length 8 lifted to seq for simplicity; the structural argument   *)
(* never needs the byte-width.                                          *)
type byte_seq = bool list.

(* Polynomial in R_q = Z_q[X] / (X^256 + 1), with q = 8380417 (FIPS 204
   ML-DSA-65 Table 1, level 3). Kept abstract: the algebraic operators
   below name the structure without forcing a concrete byte-level
   coefficient representation. *)
type poly_t.

(* Secret-key share: an element of R_q^ell (per-party Shamir share of *)
(* the FIPS 204 secret s_1, alongside the Pedersen blinding share).   *)
(*                                                                      *)
(* Concrete structural view (Agent 1 HIGH-5 closure):                   *)
(*   share_t is conceptually a polynomial vector in R_q^ell. The op    *)
(*   `share_polys` surfaces this view: every share has a polynomial-   *)
(*   list representation of dimension `share_dim` = 5 (FIPS 204         *)
(*   ML-DSA-65 ell parameter).                                          *)
(*                                                                      *)
(* The type itself remains abstract — we do NOT pin its concrete byte  *)
(* representation here (that's a libjade ABI detail and lives in        *)
(* Pulsar_N1_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.

(* FIPS 204 ML-DSA-65 parameter ell = 5 (Table 1 level 3). *)
op share_dim : int = 5.

(* 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.

(* HIGH-5 load-bearing reinforcement (followup A).

   `share_polys` is INJECTIVE — distinct shares have distinct
   polynomial views. Without this an adversarial instantiation
   could realise `share_polys s = [witness; witness; witness;
   witness; witness]` (constant 5-element list) for every share,
   vacuously satisfying `share_dim_correct`. The injectivity axiom
   forces the polynomial view to actually distinguish shares.

   The reverse direction `poly_share_of` is similarly injective on
   inputs of correct dimension — the round-trip pins it as the
   inverse of `share_polys`, and the injectivity-of-inverse axiom
   captures the structural identity that distinct polynomial
   vectors yield distinct shares. *)
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. Together with the existing
   `poly_share_roundtrip` (share_polys ∘ poly_share_of = id on dim-
   correct inputs), this pins `share_polys` and `poly_share_of` as
   mutual inverses on the dim-correct domain.

   Followup B reinforcement: the user's specified round-trip
   direction. Without this, `share_t` could in principle have
   "ghost" extra structure invisible to `share_polys` — adversaries
   could realise distinct shares with identical polynomial views.
   The injectivity axiom above rules that out, and this round-trip
   makes the inverse identity directly applicable in proofs. *)
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. The link to the abstract share-level `reconstruct`
   appears below (after `reconstruct` itself is declared) via the
   `reconstruct_polys_view` axiom. *)
op reconstruct_polys :
  int list -> (poly_t list) list -> poly_t list.

(* Group public key (FIPS 204 ML-DSA public-key encoding -- 1952 bytes *)
(* for ML-DSA-65, but we keep it abstract here).                       *)
type group_pk_t.

(* Message / context / signature wire-level types.                     *)
(*                                                                      *)
(* `signature_t` is ALIASED to `Pulsar_N1_Signature_Codec.signature_t`. *)
(* Prior to this commit the two types were independent abstract         *)
(* declarations with an uninterpreted coercion `refine_sig_to_n1`       *)
(* between them — that left room for an adversarial instantiation       *)
(* where the coercion collapsed all signatures to a single value,       *)
(* making the byte-walk axiom in Combine_Refinement / Sign_Refinement   *)
(* vacuous. With a single concrete type the coercion becomes the        *)
(* identity (defined as `fun (s : signature_t) => s`) and the byte-     *)
(* walk axiom directly constrains the protocol-level signature value.   *)
type message_t.
type ctx_t.
type signature_t = Pulsar_N1_Signature_Codec.signature_t.

(* Per-session per-party randomness used by Round-1 mask sampling      *)
(* and (if randomized) Round-2 commit blinding.                        *)
type randomness_t.

(* Round-1 protocol message (per-party w1 commit + Round-1 transcript). *)
type round1_t.

(* Round-2 protocol message (per-party z share + hint bit).             *)
type round2_t.

(* Per-session state ID (FIPS 204 mu = SHAKE(tr || message), Round-1   *)
(* digest, attempt counter, etc.).                                     *)
type session_t.

(* -------------------------------------------------------------------- *)
(* Shamir / Lagrange algebraic kernel                                   *)
(* -------------------------------------------------------------------- *)
(* These operators name the Shamir layer. The companion Lean theory     *)
(* Crypto.Pulsar.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^ell 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^ell. Defined recursively over the quorum list.             *)
op reconstruct (Q : int list) (shares : share_t list) : share_t.

(* HIGH-5 load-bearing reinforcement (followup A).

   The abstract `reconstruct`'s polynomial view IS component-wise
   Lagrange (`reconstruct_polys`, declared above). This load-bearing
   identity links the share-level reconstruct (used by Pulsar_N1 /
   Pulsar_N4 protocol claims) to the per-coordinate polynomial view
   (the FIPS 204 R_q^ell algebraic structure). An adversarial
   reconstruct realisation that doesn't factor through component-
   wise Lagrange — e.g., returning a constant share regardless of
   the inputs — is now ruled out by the structural commitment. *)
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. Proved by
   applying `poly_share_of` to both sides of `reconstruct_polys_view`
   and using `poly_share_of_share_polys` to collapse the LHS.

   This is the form a Lean-bridge consumer cites — "reconstruction
   on shares = build-from-polys ∘ reconstruct_poly ∘ map share_polys"
   makes the polynomial bridge directly applicable. *)
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^ell[X] (parametrised by p : share_t        *)
(* abstracting the polynomial's representation as its constant term).  *)
op poly_eval : share_t -> int -> share_t.

(* The dealer's Shamir polynomial degree.                              *)
(*                                                                      *)
(* `share_t` is abstract over the polynomial representation; this op   *)
(* surfaces the polynomial's algebraic degree so the Lagrange-         *)
(* recovery identity below can carry the right precondition.           *)
(* Concretely for Pulsar's t-of-n threshold scheme, every share's     *)
(* underlying polynomial has degree = threshold - 1.                  *)
op poly_degree : share_t -> int.

(* Non-negativity: a polynomial's degree is >= 0. Stated as an axiom  *)
(* because share_t is abstract; trivially provable once share_t gets  *)
(* a concrete representation. *)
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^ell coordinate semantics.            *)
(*                                                                      *)
(* PRECONDITION: |Q| > degree(f). The Lean theorem requires            *)
(* `f.degree < s.card` (file:line below); without this bound,          *)
(* Lagrange interpolation through |Q| points of a degree-d polynomial *)
(* is undefined when d >= |Q|. Earlier versions of this axiom used    *)
(* `1 <= size Q`, which was too weak — see Agent 2 critical finding   *)
(* in the cryptographer review.                                       *)
(*                                                                      *)
(* BRIDGED TO LEAN: this axiom corresponds to                           *)
(*   Crypto.Pulsar.Shamir.shamir_correct_at_target                      *)
(*   (`~/work/lux/proofs/lean/Crypto/Pulsar/Shamir.lean:76`)            *)
(* 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` § "Axiom 1" 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.

(* R_q-linearity of `reconstruct` (FUTURE WORK).                       *)
(*                                                                      *)
(* The real linearity statement is                                      *)
(*   reconstruct Q (zipWith (+) sh1 sh2) =                              *)
(*     reconstruct Q sh1 + reconstruct Q sh2                            *)
(* which requires share_t to expose its R_q additive structure --       *)
(* deferred to a follow-up commit that imports `algebra/Ring.ec` and    *)
(* equips share_t with a `+` operator. It is not needed for the         *)
(* `reconstruct_of_share` discharged below; only the cryptographic      *)
(* reduction in `pulsar_n1_byte_equality` uses it. Tracked alongside  *)
(* the remaining admit.                                                 *)

(* -------------------------------------------------------------------- *)
(* Discharged lemma: reconstruction is a left inverse of sharing       *)
(* -------------------------------------------------------------------- *)
(* The dealer chooses a polynomial whose constant term is the secret;  *)
(* party i is handed share_i = P(i). The Lagrange-interpolation        *)
(* identity at X = 0 over a field of order > size(Q) reconstructs the  *)
(* constant term from any t distinct evaluation points. This is the    *)
(* algebraic core of the N1 reduction (spec/pulsar.tex eq. (476)).   *)
(* -------------------------------------------------------------------- *)

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.
  (* Direct application of the Lagrange identity at X = 0. The         *)
  (* `lagrange_inverse_eval` axiom captures the algebraic content; we  *)
  (* introduce the two hypotheses and apply the axiom with them.       *)
  move=> uQ szQ.
  exact: (lagrange_inverse_eval s Q uQ szQ).
qed.

(* Useful packaged corollary: a Pulsar honest quorum's share list,    *)
(* when reconstructed under one valid quorum index set, yields the      *)
(* same secret as under any other quorum index set (this is the         *)
(* "quorum invariance" used implicitly in the cryptographic reduction). *)
(* This is a genuine downstream consequence -- discharged here.         *)
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.

(* -------------------------------------------------------------------- *)
(* Single-party ML-DSA-65 oracle interface (libjade-backed)             *)
(* -------------------------------------------------------------------- *)
(* The functional spec axiom: there exists a deterministic operator    *)
(* `mldsa_sign_op` such that any FIPS 204 conformant Sign implementation *)
(* (including circl's mldsa65.SignTo and the libjade-extracted version) *)
(* produces exactly `mldsa_sign_op(sk, m, ctx, rho_rnd)`.                   *)
(* -------------------------------------------------------------------- *)

(* FIPS 204 §6.2 Sign_internal structural skeleton (Agent 1 HIGH-4).

   `mldsa_sign_op` is the centralised FIPS 204 ML-DSA-65 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, or that depend on rho_rnd in non-FIPS ways.

   The closure: surface FIPS 204 §6.2 Sign_internal's THREE-STAGE
   pipeline as named sub-ops, then DEFINE mldsa_sign_op as their
   composition. The pipeline:

     stage 1  unpack_sk     sk → (rho, K, tr, s1, s2, t0)
                            (FIPS 204 §3.5.4 decoding)
     stage 2  compute_mu    (m, ctx) → mu
                            (FIPS 204 §5.4.1 ExternalMu:
                             SHAKE256(0x00 || |ctx| || ctx || M, 64))
     stage 3  sign_internal_loop
                            (unpacked_sk, mu, rho_rnd) → signature
                            (FIPS 204 §6.2 kappa rejection loop:
                             y ← ExpandMask(K, rho_rnd, kappa);
                             w = A·y ; (w1,w0) = Decompose w ;
                             c_tilde = H(mu || w1) ;
                             c = SampleInBall c_tilde ;
                             z = y + c·s1 ; r0 = w0 - c·s2 ;
                             reject if ‖z‖∞ ≥ γ1-β or ‖r0‖∞ ≥ γ2-β ;
                             else pack(c_tilde, z, h))

   The three sub-ops are still abstract (their bodies require
   share_t / poly-vec concretization, tracked HIGH-5 + #3), but the
   structural composition is now FIXED. Adversarial mldsa_sign_op
   instantiations must instantiate the three sub-ops independently;
   any honest FIPS 204 reference implementation factors cleanly
   into this skeleton.

   The mu computation (stage 2) is a function of (m, ctx) only —
   the FIPS 204 ExternalMu derivation — and the rejection-loop
   randomness is rho_rnd (stage 3). Decomposing mldsa_sign_op this
   way rules out adversarial realisations that bypass mu/ExternalMu
   (e.g. computing the signature directly from ctx instead of
   folding it into mu first). *)

(* Abstract types for the pipeline outputs/inputs. Both bodies are
   open until share_t is concretized as a 6-tuple (HIGH-5). *)
type unpacked_sk_t.
type mu_t.

op unpack_sk  : share_t -> unpacked_sk_t.

(* FIPS 204 §5.4.1 ExternalMu — DEFINED constructively as a SHAKE
   over a fixed byte layout. The decomposition lets the refinement
   files prove their mu-stage sub-axiom as a derived lemma from a
   narrower BYTE-LAYOUT axiom (the extracted body's SHAKE input
   buffer matches the FIPS 204 §5.4.1 prefix + ctx + M layout) —
   no SHAKE semantics in the byte-layout axiom; that step is
   structural via `shake256_to_mu` (same op on both sides of any
   equality). *)

(* The byte-layout input to the ExternalMu SHAKE call: per FIPS 204
   §5.4.1, the layout is `IntegerToBytes(0, 1) || IntegerToBytes(|ctx|, 1)
   || ctx || M`.

   v9: concretized to `int list` (byte sequence). The previous
   abstract `type mu_shake_input_t.` declaration is replaced by a
   concrete type alias, and `external_mu_layout` is converted from
   an abstract op to a constructive definition over per-component
   byte ops (`message_bytes`, `context_bytes`). The `*_body_mu_input`
   ops on the refinement sides can now talk about CONCRETE BYTES
   rather than an abstract value — exposing the byte structure for
   further closure attempts. *)
type mu_shake_input_t = int list.

(* Per-value byte encodings for the message and context. Abstract
   ops here; concrete shapes pinned at the wrapper layer. Both
   produce `int list` — the FIPS 204 specifies them as opaque
   byte strings at this level. *)
op message_bytes : message_t -> int list.
op context_bytes : ctx_t     -> int list.

(* FIPS 204 §5.4.1 bounds the context length to a single byte
   (max 255). The honest implementation must reject longer
   contexts at the wrapper layer; here we surface the bound as a
   single axiom that downstream consumers may use to discharge
   FIPS 204 size invariants. *)
axiom context_bytes_len_bound :
  forall (ctx : ctx_t),
    0 <= size (context_bytes ctx) <= 255.

(* FIPS 204 §5.4.1 ExternalMu byte layout — now a constructive
   DEFINITION. Components, in order:
     1.  0x00          (FIPS 204 §5.4.1 prefix byte for pure mode)
     2.  |ctx|         (single byte; bounded above by 255)
     3.  ctx_bytes     (the context bytes themselves)
     4.  m_bytes       (the message bytes)
   This decomposition lets the refinement files split their
   mu_input byte-walk obligations along per-component lines. *)
op external_mu_layout (m : message_t) (ctx : ctx_t) : mu_shake_input_t =
  [0; size (context_bytes ctx)] ++ context_bytes ctx ++ message_bytes m.

op shake256_to_mu      : mu_shake_input_t -> mu_t.

op compute_mu (m : message_t) (ctx : ctx_t) : mu_t =
  shake256_to_mu (external_mu_layout m ctx).

(* FIPS 204 §3.5.5 signature components surfaced as abstract types:
   c_tilde (32-byte SHAKE digest), z (l-coordinate response vector,
   bit-packed via the FIPS 204 PowerToBytesPos encoding), h (k-
   coordinate hint vector with at most omega non-zero coefficients).

   Surfacing the components at the type level lets the byte-walk
   obligations in Combine_Refinement / Sign_Refinement split along
   the FIPS 204 §3.5.5 packing boundary: a "components match" axiom
   over the (c_tilde, z, h) triple plus a structural pack identity.
   The pack identity is then directly attackable per-component (S4
   for c_tilde, S3+S5 for z, S7 for h on the combine roadmap) rather
   than as a monolithic byte-walk over the full 3293-byte signature. *)
type c_tilde_n1_t.
type z_n1_t.
type h_n1_t.

(* ML-DSA inner signing loop, decomposed per FIPS 204 §6.2 output
   stage. Each component op captures the centralised single-party
   output of one inner-loop stage on accept:

     mldsa_compute_c_tilde  c_tilde = SHAKE(mu || w1Encode(w1))
                            — corresponds to roadmap S4. STRUCTURAL
                            DEFINITION (not abstract): factored
                            through `central_w1` and `shake_mu_w1`
                            so the c_tilde-stage byte-walk decomposes
                            into mu-spec + w1-spec sub-axioms.
     mldsa_compute_z        z = y + c·s1 after kappa converges
                            — roadmap S3 (Lagrange-aggregation, when
                              viewed from the threshold side) + S5
                              (w_prime + decompose). STILL ABSTRACT.
     mldsa_compute_h        h = MakeHint(w_low_agg, w_high_agg)
                            — roadmap S7. STILL ABSTRACT.

   The c_tilde-stage decomposition (this file) lets the refinement
   files prove their c_tilde axiom as a derived lemma from two
   narrower sub-axioms (extracted mu = compute_mu; extracted w1 =
   central_w1). The z- and h-stage decompositions are future work
   (z requires the Lean Lagrange-aggregation bridge; h depends on
   MakeHint over aggregated low/high vectors). *)

(* w1 — the high-bits polynomial vector at the accepting kappa.
   Abstract type captures whatever value the centralised ML-DSA
   inner loop produces for w1Encode's input on accept. *)
type w1_value_t.

(* w — the polynomial-vector intermediate BEFORE HighBits/decompose.
   In FIPS 204 §6.2, w = A·y at the accepted kappa, where
   A = ExpandA(rho), y = ExpandMask(rho', kappa). The HighBits step
   then extracts w1 = (decompose_vec_k gamma2 w).`1.

   Surfacing w_value_t as a distinct type lets central_w1 factor
   as `high_bits_of_w ∘ central_w`. The HighBits decomposition is
   then structural on both extracted and centralised sides, so the
   refinement files' w1-stage byte-walk obligations decompose into
   a narrower `w_spec` claim (extracted_w = central_w) — the
   HighBits step is folded into structural definitions on both
   sides.

   The accepted-kappa selection + A·y composition remain inside
   `central_w`'s abstract surface (concretisation would require a
   loop / fixed-point model and MLDSA65_Functional.mat_vec_mul +
   expand_a + expand_mask bridges — future narrowing steps). *)
type w_value_t.

(* v12 — central_w structural decomposition.

   central_w = A · y at the accepting κ, factored as:
     - central_matrix_a : ExpandA(rho) — depends only on usk's
       public-matrix seed; κ-independent and message-independent.
     - central_mask_y_at_accepted_kappa : ExpandMask(rho', κ_accept)
       — depends on usk + mu + rho_rnd; κ_accept selection is folded
       into the abstract op surface (κ-loop fixed-point model is
       out of scope for v12).
     - apply_mat_vec_mul : the FIPS 204 §6.2 polynomial-matrix-vector
       product A · y → w.

   The refinement-side `*_body_compute_w` ops then decompose into
   per-stage extracted intermediates with two narrower sub-axioms
   per side (matrix_a + mask_y), and `*_body_w_spec` becomes a
   derived lemma via the structural `apply_mat_vec_mul` identity
   common to both extracted and centralised sides. *)
type matrix_a_t.   (* FIPS 204 §3.5.2 ExpandA matrix ∈ R_q^{k × l} *)
type mask_vec_t.   (* y polynomial vector ∈ R_q^l from ExpandMask *)

op central_matrix_a : unpacked_sk_t -> matrix_a_t.

op central_mask_y_at_accepted_kappa :
  unpacked_sk_t -> mu_t -> randomness_t -> mask_vec_t.

op apply_mat_vec_mul : matrix_a_t -> mask_vec_t -> w_value_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_mask_y_at_accepted_kappa usk mu_val rho_rnd).

(* HighBits as a structural function over w polynomial vectors.
   On the centralised side this is `(decompose_vec_k gamma2 w).`1`;
   on the extracted side it is the same FIPS 204 §3.4.2 decomposition
   applied to the extracted body's w vector. Encoded as a single
   abstract op here; concrete identity with MLDSA65_Functional
   decompose_vec_k is bridge work. *)
op high_bits_of_w : w_value_t -> w1_value_t.

op central_w1
   (usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
   : w1_value_t =
  high_bits_of_w (central_w usk mu_val rho_rnd).

(* SHAKE-based c_tilde derivation: c_tilde = SHAKE256(mu ||
   w1Encode(w1), 32) per FIPS 204 §6.2. Abstract here; concrete
   identity with `MLDSA65_Functional.sample_in_ball`'s SHAKE input
   stage is bridge work. *)
op shake_mu_w1 :
  mu_t -> w1_value_t -> c_tilde_n1_t.

op mldsa_compute_c_tilde
   (usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
   : c_tilde_n1_t =
  shake_mu_w1 mu_val (central_w1 usk mu_val rho_rnd).

(* ===================================================================
   v11 — z-stage structural decomposition (FIPS 204 §6.2 z = y + c·s1).

   `mldsa_compute_z` is now a STRUCTURAL DEFINITION composing four
   per-stage ops:
     - `central_y_at_accepted_kappa` — the ExpandMask y at the accepted κ
     - `central_c_from_c_tilde` — SampleInBall(c_tilde) → ring element c
     - `apply_c_to_s1` — c · s_1 (challenge-scaled secret share)
     - `add_response_vec` — polynomial-vector addition

   The sign-side z-stage byte-walk obligation decomposes into a
   narrower y-spec + cs1-spec pair (each over a polynomial vector,
   not the full z output). The structural composition is identical
   on both extracted and centralised sides, so the refinement-side
   `sign_body_z_spec` becomes a derived lemma via two narrower
   sub-axioms.

   For the combine threshold side: the v8 Lean-bridged path remains
   the closure mechanism. The v11 decomposition does NOT replace v8 —
   `combine_body_z_spec` stays a derived lemma via the
   `threshold_partial_response_identity` bridge, and the v11
   per-stage ops below add structural visibility to mldsa_compute_z's
   internal form. *)

type response_vec_t.        (* R_q^l polynomial vector — y / cs1 / z all live here *)
type challenge_ring_t.      (* R_q ring element — c from SampleInBall *)

op central_y_at_accepted_kappa :
  unpacked_sk_t -> mu_t -> randomness_t -> response_vec_t.
  (* the ExpandMask(rho', κ) mask at the accepting κ; κ-selection
     folded into the abstract op surface *)

op central_c_from_c_tilde :
  c_tilde_n1_t -> challenge_ring_t.
  (* FIPS 204 §3.5.1 SampleInBall: c_tilde → c ∈ R_q with τ ±1 coeffs *)

op apply_c_to_s1 :
  challenge_ring_t -> unpacked_sk_t -> response_vec_t.
  (* c · s_1 — scalar-by-vector multiplication where s_1 ∈ R_q^l is
     unpacked from the secret key *)

op add_response_vec :
  response_vec_t -> response_vec_t -> z_n1_t.
  (* polynomial-vector addition; coerces R_q^l + R_q^l to the z output
     type *)

op mldsa_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
          (mldsa_compute_c_tilde usk mu_val rho_rnd))
       usk).

(* w_low — the low-bits polynomial-vector intermediate at the accepting
   kappa. In FIPS 204 §3.4.2 decompose, w factors as
     (w_high, w_low) = decompose_vec_k gamma2 w
   where w_high = w1 = `high_bits_of_w w` (already surfaced in v7)
   and w_low is the remaining low-bits coordinate-wise residue.

   Surfacing w_low_value_t as a distinct type lets the h-stage factor
   structurally as `make_hint_of_w ∘ (central_w, central_w_low)`:
   the MakeHint operation (FIPS 204 §3.4.3) takes the full polynomial
   vector w plus its low-bits component and produces the hint vector
   h, which encodes the carry information needed to recover w1 from
   the response without re-aggregating w. The high-bits side is
   structural (the `central_w` value already in scope determines w1
   via `high_bits_of_w`); the low-bits side is a second independent
   abstract op.

   The MakeHint decomposition is structural on both extracted and
   centralised sides, so the refinement files' h-stage byte-walk
   obligations decompose into a narrower `w_low_spec` claim
   (extracted_w_low = central_w_low) — the MakeHint step is folded
   into structural definitions on both sides.

   `central_w` and `central_w_low` remain abstract surfaces
   (concretisation would require a fixed-point model of the kappa
   loop plus MLDSA65_Functional.decompose_vec_k bridge — future
   narrowing steps). *)
type w_low_value_t.

op central_w_low :
  unpacked_sk_t -> mu_t -> randomness_t -> w_low_value_t.

(* MakeHint as a structural function over (w, w_low) pairs.
   On the centralised side, given w = A·y at the accepted kappa and
   w_low = (decompose_vec_k gamma2 w).`2, MakeHint produces the hint
   vector h per FIPS 204 §3.4.3. On the extracted side it is the
   same operation applied to the body's threshold-aggregated (or
   libjade-computed) w and w_low intermediates. Encoded as a single
   abstract op here; concrete identity with
   MLDSA65_Functional.vec_k_make_hint is bridge work. *)
op make_hint_of_w : w_value_t -> w_low_value_t -> h_n1_t.

op mldsa_compute_h
   (usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
   : h_n1_t =
  make_hint_of_w
    (central_w     usk mu_val rho_rnd)
    (central_w_low usk mu_val rho_rnd).

(* ===================================================================
   Threshold response layer — FROST-style partial responses + Lagrange
   aggregation. Used by Pulsar combine to fold Round-2 messages into
   the final ML-DSA z output.

   `partial_response_t` is the per-party response value
     z_i = y_i + c · s_i
   computed by party i given:
     - the common c_tilde 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 standard Lagrange-at-zero
   interpolation (lambda_i coefficients for the quorum).

   The threshold partial-response identity below states that this
   aggregation equals the centralised ML-DSA `mldsa_compute_z` on the
   reconstructed share — i.e., the FROST/Pulsar correctness for the
   z stage. The identity is Lean-bridged to
   `Crypto.Threshold.Lagrange.threshold_partial_response_identity`
   (`lean/Crypto/Threshold_Lagrange.lean:121`).
   =================================================================== *)

type partial_response_t.

op per_party_partial_response :
  c_tilde_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.

   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

   EC formulation: at the share_t level, the polynomial f is the
   secret share `reconstruct Q shares`; the per-party shares are
   `poly_eval (reconstruct Q shares) i` for i ∈ Q; per-party
   partial responses are `per_party_partial_response c_tilde rho_rnd
   mu_val share_i`. Aggregating those equals `mldsa_compute_z` on
   the reconstructed share's unpacked form.

   The 4 preconditions mirror the Lean theorem's hypotheses:
     - `uniq Q`              ↔ `Set.InjOn v s` (distinct party indices)
     - `size shares = size Q` ↔ shape match
     - `poly_degree < size Q` ↔ `f.degree < s.card`
     - shares = honest poly evaluations ↔ Lean's setup `z = y + c•f(v)`. *)
axiom threshold_partial_response_identity :
  forall (Q : int list) (shares : share_t list)
         (c_tilde : c_tilde_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_tilde rho_rnd mu_val) shares)
    = mldsa_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_tilde_n1_t * z_n1_t * h_n1_t =
  (mldsa_compute_c_tilde usk mu_val rho_rnd,
   mldsa_compute_z       usk mu_val rho_rnd,
   mldsa_compute_h       usk mu_val rho_rnd).

(* FIPS 204 §3.5.5 signature codec: layout the (c_tilde, z, h) triple
   into the byte-level signature_t and back. Mirrors the existing
   per-type FIPS 204 codec axioms in Pulsar_N1_Signature_Codec.ec —
   round-trip identity is the load-bearing property the refinement
   files consume. *)
op pack_n1_signature : c_tilde_n1_t -> z_n1_t -> h_n1_t -> signature_t.
op unpack_n1_signature : signature_t -> c_tilde_n1_t * z_n1_t * h_n1_t.

axiom pack_unpack_n1_signature_roundtrip :
  forall (c : c_tilde_n1_t) (z : z_n1_t) (h : h_n1_t),
    unpack_n1_signature (pack_n1_signature c z h) = (c, z, h).

(* Derived injectivity. Used by the refinement files to lift a
   component-level (c, z, h) equality to a byte-level pack equality
   (and vice versa). PROVED — not an additional axiom. *)
lemma pack_n1_signature_injective :
  forall (c1 c2 : c_tilde_n1_t) (z1 z2 : z_n1_t) (h1 h2 : h_n1_t),
    pack_n1_signature c1 z1 h1 = pack_n1_signature c2 z2 h2 =>
    c1 = c2 /\ z1 = z2 /\ h1 = h2.
proof.
  move=> c1 c2 z1 z2 h1 h2 Heq.
  have H1 := pack_unpack_n1_signature_roundtrip c1 z1 h1.
  have H2 := pack_unpack_n1_signature_roundtrip c2 z2 h2.
  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 FIPS 204 §3.5.5 packing step.

   This DEFINITION (rather than an abstract op declaration) is the
   structural refinement that lets the combine and sign byte-walk
   axioms split along the pack boundary. Before this commit,
   `sign_internal_loop` was abstract and the byte-walk obligation
   constrained all 3293 signature bytes as one monolithic claim;
   after, the byte-walk decomposes into a (c_tilde, z, h) component
   spec (still axiomatic) and a structural pack identity (derivable
   from the codec roundtrip). The total axiom surface is essentially
   unchanged — the codec roundtrip slots cleanly into the existing
   "~21 per-type FIPS 204 codec round-trip" category — but the
   byte-walk obligation is now per-component instead of opaque,
   matching the S1-S10 sub-claim structure in
   `proofs/easycrypt/extraction/combine-byte-walk-roadmap.md`. *)
op sign_internal_loop
   (usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t)
   : signature_t =
  let cz_h = run_signing_components usk mu_val rho_rnd in
  pack_n1_signature cz_h.`1 cz_h.`2 cz_h.`3.

op mldsa_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.

(* ML-DSA-65 rejection-sampling accept event (followup B closure).

   `accept_signing_attempt sk m ctx rho_rnd` is the (deterministic)
   event that the ML-DSA R1-R4 norm checks pass for the
   ML-DSA-65 signing attempt with the four protocol-level inputs.

   No-reject is NOT a universal property of honest signing — it is a
   property of ACCEPTED signing attempts. FIPS 204 rejection sampling
   remains probabilistic per ML-DSA; cryptographic-reduction proofs
   condition on the accepted path, while the probability of
   acceptance is tracked operationally.

   `mldsa_accept_lower_bound` names the probability bound on
   acceptance for honest signers (≈ 1 − (3/4)^256 per attempt,
   ≥ 1 − 2^-128 after the kappa-bounded loop, per the standard
   ML-DSA acceptance analysis). Stated as an abstract real-valued
   lower bound; the operational tracking of
   `Pr[accept] >= mldsa_accept_lower_bound` is a probabilistic
   obligation tracked separately (the deterministic EC model
   captures the accepted-path conditioning via the predicate
   above).

   Downstream byte-walk axioms in Combine_Refinement and
   Sign_Refinement condition on `accept_signing_attempt` evaluated
   on the protocol-level inputs (for combine: the reconstructed
   share; for sign: the share directly). *)
op accept_signing_attempt :
  share_t -> message_t -> ctx_t -> randomness_t -> bool.

(* v13 — per-FIPS 204 §6.2 R1/R2/R3/R4 accept events as ABSTRACT
   COMPANIONS to `accept_signing_attempt`. The bundled predicate
   stays opaque (downstream tactics like `do! split` in
   `pulsar_n1_byte_equality`'s symmetric leg depend on the
   abstract surface). The new per-R ops + a bridge axiom let
   downstream callers REASON about the four conditions individually
   without changing the existing `accept_signing_attempt` API.

     R1: ‖z‖∞ < γ1 − β     (z-norm bound)
     R2: ‖r0‖∞ < γ2 − β    (r0-low-bits-norm bound)
     R3: ‖c·t0‖∞ < γ2      (ct0-norm bound)
     R4: weight(h) ≤ ω     (hint-Hamming-weight bound)

   See FIPS 204 §6.2 (ML-DSA.Sign_internal) for the rejection-loop
   pseudocode. *)
op accept_r1_z_norm    : share_t -> message_t -> ctx_t -> randomness_t -> bool.
op accept_r2_r0_norm   : share_t -> message_t -> ctx_t -> randomness_t -> bool.
op accept_r3_ct0_norm  : share_t -> message_t -> ctx_t -> randomness_t -> bool.
op accept_r4_h_weight  : share_t -> message_t -> ctx_t -> randomness_t -> bool.

axiom accept_signing_attempt_iff_R1234 :
  forall sk m ctx rho_rnd,
    accept_signing_attempt sk m ctx rho_rnd
    <=> (accept_r1_z_norm   sk m ctx rho_rnd
      /\ accept_r2_r0_norm  sk m ctx rho_rnd
      /\ accept_r3_ct0_norm sk m ctx rho_rnd
      /\ accept_r4_h_weight sk m ctx rho_rnd).

op mldsa_accept_lower_bound : real.

(* HIGH-4 load-bearing reinforcement (followup A).

   Without further axioms the three pipeline ops admit the trivial
   factoring (unpack_sk = id, compute_mu = pair, sign_internal_loop
   = the original 4-arg op), making `mldsa_sign_op`'s pipeline
   purely cosmetic. The two axioms below pin the pipeline by
   structural constraints:

   - `compute_mu_injective`: distinct (m, ctx) pairs yield distinct
     mu. Captures that FIPS 204 §5.4.1 ExternalMu
     (SHAKE256(0x00 || |ctx| || ctx || M, 64)) is a TWO-VARIABLE
     injection. Adversarial realisations that drop m (or ctx) from
     the digest are ruled out.

   - `pack_sk` + `pack_unpack_sk_roundtrip`: `unpack_sk` has a
     left inverse `pack_sk`. Adversarial realisations that
     collapse distinct shares into the same `unpacked_sk_t` are
     ruled out (any such collapse would mean pack_sk's left-inverse
     identity fails).

   These do not concretize the pipeline (concretization requires
   share_t to be a 6-tuple, HIGH-5+future), but they rule out the
   trivial factoring critique: any `compute_mu` realisation must be
   a two-variable injection, and any `unpack_sk` realisation must
   be reversible. *)
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 MLDSA65_Sign = {
  proc sign(sk : share_t, m : message_t, ctx : ctx_t,
            rho_rnd : randomness_t) : signature_t
}.

(* Functional correspondence with FIPS 204 / circl / libjade-extracted *)
(* implementations. This is the SINGLE point at which the EasyCrypt    *)
(* theory trusts a Dilithium3 functional theorem.                       *)
(*                                                                      *)
(* Note on upstream state (verified 2026-05): libjade ships Jasmin     *)
(* sources for Dilithium but NO EasyCrypt mechanization of its         *)
(* functional spec — only SHAKE / Curve25519 / Poly1305 have EC        *)
(* proofs upstream. Closing this axiom requires either:                *)
(*                                                                      *)
(*   (a) Vendoring an in-house `MLDSA65_Functional.ec` into            *)
(*       `proofs/easycrypt/lemmas/` — substantial expert work but no    *)
(*       external dep (FIPS 204 §3.2-3.5 is fully specified).          *)
(*   (b) Waiting on Formosa-Crypto upstream to add a Dilithium EC      *)
(*       mechanization (no public roadmap).                            *)
(*                                                                      *)
(* See `~/work/lux/threshold/study/pulsar.md` for the broader gap      *)
(* discussion. We do NOT fork libjade; the dependency is on the        *)
(* Jasmin sources (which ARE upstream) and on the EC theorem we'd      *)
(* write ourselves OR cite once it's mechanized somewhere.             *)
module FIPS204Sign : MLDSA65_Sign = {
  proc sign(sk : share_t, m : message_t, ctx : ctx_t,
            rho_rnd : randomness_t) : signature_t = {
    return mldsa_sign_op sk m ctx rho_rnd;
  }
}.

(* Functional spec correspondence -- DISCHARGED as a lemma.            *)
(*                                                                      *)
(* The original axiom was the libjade hand-off point. With the in-house *)
(* `MLDSA65_Functional.ec` mechanization (FIPS 204 §3 spec at the EC-op *)
(* level), the role of `FIPS204Sign.sign` collapses to a pure-functional *)
(* wrapper around the `mldsa_sign_op` operator: the body literally       *)
(* returns `mldsa_sign_op sk m ctx rho_rnd`. The Pr-equality is then     *)
(* a deterministic Hoare assertion closed by `byphoare` + skip.          *)
(*                                                                      *)
(* This removes ONE axiom from the trust footprint: the cryptographic   *)
(* content (Module-LWE rejection-sampling identity) sits inside         *)
(* `mldsa_sign_op` (the abstract operator) and the section-local        *)
(* refinement axioms (`combine_body_axiom`, `S_functional_spec`,        *)
(* `reshare_preserves_secret`), which are the actual libjade /          *)
(* Jasmin-extraction hand-off points.                                   *)
lemma mldsa_sign_axiom :
  forall (sk0 : share_t) (m0 : message_t) (c0 : ctx_t)
         (r0 : randomness_t) &mm,
    Pr[FIPS204Sign.sign(sk0, m0, c0, r0) @ &mm :
        res = mldsa_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 = mldsa_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 FIPS 204 key-derivation     *)
(* op: for a freshly-sampled secret seed, derive_pk returns the matching *)
(* public verification key (rho || t1 in FIPS 204 §3.5.4 terms). For the *)
(* Shamir-reconstructed share of a Pulsar quorum, this is the group's    *)
(* public key the DKG committed to in Round-3.                            *)
(*                                                                       *)
(* Declared at top level (BEFORE section ClassN1) so the section-local   *)
(* `combine_body_axiom` precondition can reference it.                    *)
(*                                                                       *)
(* `fips204_verify` is the matching public-key verifier (FIPS 204         *)
(* Verify_internal).                                                      *)
op derive_pk : share_t -> group_pk_t.
op fips204_verify : group_pk_t -> message_t -> ctx_t
                    -> signature_t -> bool.

(* -------------------------------------------------------------------- *)
(* Pulsar threshold oracle interface                                  *)
(* -------------------------------------------------------------------- *)

module type Pulsar_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_tilde : 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 FIPS 204 dispatch on the reconstructed secret.   *)
(* -------------------------------------------------------------------- *)
(* The cryptographic content of the proof of `thm:sign-correct`        *)
(* (spec/pulsar.tex lines 765-793): the Pulsar Combine procedure   *)
(* assembles (c_tilde, z, h) using Lagrange-aggregated values that      *)
(* coincide ON-THE-NOSE with the FIPS 204 single-signer (c_tilde, z, h) *)
(* 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 `combine_abs`).                                *)
(* -------------------------------------------------------------------- *)

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 <@ FIPS204Sign.sign(sk_group, m, ctx, rho_rnd);
    return sig;
  }
}.

(* Refinement axiom: the Jasmin-extracted Combine is equivalent to     *)
(* `CombineAbs.combine`. Stated inside `section ClassN1` below where   *)
(* the module `T` is in scope (EasyCrypt axioms cannot be parametrised *)
(* by modules at top level; the standard idiom is a section-local      *)
(* `axiom` predicated on a `declare module T`).                        *)

(* -------------------------------------------------------------------- *)
(* Discharged step: Combine = mldsa_sign_op o reconstruct               *)
(* -------------------------------------------------------------------- *)
(* The abstract dispatch step composes cleanly: under the Combine       *)
(* refinement, every signature produced equals                          *)
(*   mldsa_sign_op (reconstruct Q shares) m ctx rho_rnd                     *)
(* by inlining FIPS204Sign.sign and applying `mldsa_sign_axiom`.        *)
(* -------------------------------------------------------------------- *)

lemma combine_dispatches_to_mldsa
      (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 = mldsa_sign_op (reconstruct Q0 shs0) m0 ctx0 rr0] = 1%r.
proof.
  (* The body of `CombineAbs.combine` is:                               *)
  (*   sk_group <- reconstruct quorum shares                            *)
  (*   sig      <@ FIPS204Sign.sign(sk_group, m, ctx, rho_rnd)              *)
  (*   return sig                                                       *)
  (* and `FIPS204Sign.sign` returns the pure operator `mldsa_sign_op`.  *)
  (* So this is a deterministic Hoare assertion closed by `byphoare`    *)
  (* with a precondition that binds the call-site arguments to the      *)
  (* procedure parameters' names.                                       *)
  byphoare (_:
       group_pk = gpk0 /\ m = m0 /\ ctx = ctx0 /\ quorum = Q0
    /\ shares = shs0 /\ rho_rnd = rr0 /\ r1s = r1s0 /\ r2s = r2s0
    ==> _) => //.
  proc; inline FIPS204Sign.sign; wp; skip => /#.
qed.

(* -------------------------------------------------------------------- *)
(* Class N1 -- byte-equality theorem                                    *)
(* -------------------------------------------------------------------- *)

section ClassN1.

declare module S <: MLDSA65_Sign.
declare module T <: Pulsar_Threshold.

(* Section-local refinement axiom: the Jasmin-extracted Combine is    *)
(* equivalent to `CombineAbs.combine` under the honest-quorum precond. *)
(*                                                                      *)
(* Discharge path (FACTORED through refinement file):                   *)
(*                                                                      *)
(*   The byte-level content of this axiom is captured ATOMICALLY by    *)
(*   `combine_body_spec` in `Pulsar_N1_Combine_Refinement.ec`. That    *)
(*   file has TWO top-level `axiom`s (the byte-walk + memory-          *)
(*   separation invariant) and SEVEN derived lemmas (layout predicate, *)
(*   read_signature_at_det, packed_bytes_eq_CombineAbs,                *)
(*   combine_body_writes_signature, ...).                              *)
(*                                                                      *)
(*   The `declare axiom` shape here remains because the procedure-     *)
(*   level `equiv` against an ABSTRACT module `T` is a different       *)
(*   shape than the byte-level lemma proven in the refinement file:    *)
(*                                                                      *)
(*     refinement file: forall mem ptrs args, layout(mem, ptrs, args)  *)
(*                       => read_sig_at(combine_fn mem ptrs).sig_ptr   *)
(*                       = combine_abs_op args                          *)
(*                                                                      *)
(*     this axiom:      equiv [ T.combine ~ CombineAbs.combine         *)
(*                              : ={arg} ==> ={res} ]                   *)
(*                                                                      *)
(*   Bridging the two requires a wrapper module                         *)
(*   `CombineExtractedWrapper` that adapts the extracted W64-pointer    *)
(*   interface of `Combine.M.pulsar_combine` to the abstract           *)
(*   Pulsar_Threshold interface. That wrapper proof is mechanical /     *)
(*   structural; it composes with the refinement file's atomic         *)
(*   `combine_body_spec` axiom to give the procedure-level equiv.      *)
(*                                                                      *)
(* Tracking: https://github.com/luxfi/pulsar/issues/4               *)
(* (closure step: write the wrapper bridge + prove the equiv against   *)
(* `Combine.M.pulsar_combine`, then replace this declare axiom with    *)
(* a lemma whose body reduces to                                       *)
(* `Pulsar_N1_Combine_Refinement.combine_body_spec`).                  *)
(* The precondition `group_pk{1} = derive_pk (reconstruct quorum{1}     *)
(* shares{1})` is the protocol-consistency obligation (Agent 1 HIGH-1   *)
(* closure): the byte-walk refinement file's atomic axiom               *)
(* `combine_body_compute_sig_spec` 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). Adversarial callers    *)
(* who supply mismatched gpk fall outside this axiom's claim — the     *)
(* refinement makes no guarantee about the extracted output in that    *)
(* case. Threaded into `pulsar_n1_byte_equality`'s precondition below. *)
declare axiom combine_body_axiom :
  equiv [ T.combine ~ CombineAbs.combine :
            ={arg}
            /\ group_pk{1} = derive_pk (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`.          *)
(* Mirrors `mldsa_sign_axiom` above for arbitrary `S`.                  *)
(*                                                                      *)
(* Discharge path (FACTORED through refinement file):                   *)
(*                                                                      *)
(*   The byte-level content of this axiom is captured ATOMICALLY by    *)
(*   `sign_body_spec` in `Pulsar_N1_Sign_Refinement.ec`. That file     *)
(*   has TWO top-level `axiom`s (the byte-walk + memory-separation)    *)
(*   and SEVEN derived rung lemmas (rung1..rung7), with rungs 4 & 5    *)
(*   collapsing to identity for libjade's single-party API surface.    *)
(*                                                                      *)
(*   The `declare axiom` shape here remains for the same reason as     *)
(*   `combine_body_axiom`: bridging the byte-level lemma to a          *)
(*   procedure-level `equiv` requires a wrapper module adapting        *)
(*   libjade's W64-pointer interface to the abstract                   *)
(*   MLDSA65_Sign interface.                                            *)
(*                                                                      *)
(* Tracking: https://github.com/luxfi/pulsar/issues/3               *)
(* (closure: wrapper bridge + lemma reducing to                        *)
(* `Pulsar_N1_Sign_Refinement.sign_body_spec`).                         *)
declare axiom S_functional_spec :
  equiv [ S.sign ~ FIPS204Sign.sign :
            ={arg}
            /\ accept_signing_attempt sk{1} m{1} ctx{1} rho_rnd{1}
          ==> ={res} ].

(* The honest-quorum Pulsar execution, as a single procedure.
   Parameterised by `T` to comply with EasyCrypt's module-system
   rule that concrete modules cannot depend on a section-local
   `declare module`. Inside section ClassN1 we instantiate with the
   declared `T`. *)
module ThresholdRun (T : Pulsar_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_tilde : message_t;
    var r2s : round2_t list;
    var sig : signature_t;
    var sess : session_t;
    sess <- witness;
    r1s <- [];
    r2s <- [];
    c_tilde <- witness;
    sig <@ T.combine(group_pk, m, ctx, quorum, shares, rho_rnd, r1s, r2s);
    return sig;
  }
}.

(* The single-party FIPS 204 execution, parameterised by the
   Shamir-reconstructed secret. Same parameterisation rule as
   ThresholdRun above: `S` is `declare module` in the section, so
   the concrete `SinglePartyRun` must take it as a functor param. *)
module SinglePartyRun (S : MLDSA65_Sign) = {
  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;
  }
}.

(* Main theorem: threshold output equals single-party output.          *)
(*                                                                     *)
(* Discharge path (NOW CLOSED — no admit):                             *)
(*   - Procedure-level `transitivity` through                           *)
(*     `SinglePartyRun(FIPS204Sign).run`.                              *)
(*   - LHS leg: replace `T.combine` by `CombineAbs.combine` via         *)
(*     `combine_body_axiom`, inline `CombineAbs.combine` to expose      *)
(*     the shared `FIPS204Sign.sign` call, sync via `sim`.              *)
(*   - RHS leg: symmetric of `single_party_run_refines_fips204` (which *)
(*     itself uses `S_functional_spec`).                                *)
(*                                                                     *)
(* The cryptographic content (Module-LWE rejection-sampling identity)  *)
(* lives inside the named section-local axioms, which are the libjade  *)
(* hand-off points.                                                    *)
(* -------------------------------------------------------------------- *)
(* Decomposition: N1 byte-equality as a chain of 6 algebraic steps      *)
(* -------------------------------------------------------------------- *)
(* The single big `admit.` is split into 6 sub-lemmas. Three are direct *)
(* applications of section-local axioms and discharge mechanically; the *)
(* fourth uses the already-discharged `combine_dispatches_to_mldsa`;    *)
(* the fifth follows from `mldsa_sign_axiom`. The sixth (the top-level  *)
(* byte-equality theorem) chains the others via procedure-level         *)
(* `transitivity` through `SinglePartyRun(FIPS204Sign).run`.            *)
(* -------------------------------------------------------------------- *)

(* Step 1 — single-party run is equivalent to FIPS204 instantiation     *)
(* via the section-local `S_functional_spec` axiom. Threads the         *)
(* accept-path precondition through. *)
lemma single_party_run_refines_fips204 :
  equiv [ SinglePartyRun(S).run ~ SinglePartyRun(FIPS204Sign).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 FIPS 204 run produces `mldsa_sign_op` on the   *)
(* reconstructed secret, with probability 1. Pure consequence of        *)
(* `mldsa_sign_axiom` (which says `FIPS204Sign.sign` returns the op).   *)
lemma single_party_fips204_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(FIPS204Sign).run(gpk, shs, Q, mm, cctx, rr) @ &m :
        res = mldsa_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 FIPS204Sign.sign; wp; skip => /#.
qed.

(* Step 3 — threshold run is equivalent to a CombineAbs-instantiated    *)
(* run via the section-local `combine_body_axiom`.                      *)
(* We do not state this as a separate equiv because CombineAbs is not a *)
(* Pulsar_Threshold module (it has a different procedure-signature).    *)
(* Step 3 is therefore folded into Step 4 below as a direct rewrite     *)
(* over the combine call site.                                          *)

(* Step 4 — threshold run via CombineAbs produces `mldsa_sign_op` on the *)
(* reconstructed secret, with probability 1. Uses the already-           *)
(* discharged `combine_dispatches_to_mldsa` lemma (no admit).            *)
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 = mldsa_sign_op (reconstruct Q shs) mm cctx rr] = 1%r.
proof.
  apply (combine_dispatches_to_mldsa gpk mm cctx Q shs rr [] [] &m).
qed.

(* Step 5 — the Lagrange-reconstruction identity at the heart of the    *)
(* threshold-to-single-party reduction is `reconstruct_of_share`,       *)
(* already discharged above (line ~213) and quoted here as a reminder   *)
(* that the algebraic core is closed.                                   *)
(* See also `~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean`     *)
(* for the polynomial-Lagrange identity discharged at the Lean side.   *)

(* Step 6 — chain Steps 1–5 to derive the byte-equality theorem.        *)
(*                                                                       *)
(* The proof uses a procedure-level `transitivity` through               *)
(* `SinglePartyRun(FIPS204Sign).run`. The LHS leg replaces `T.combine`  *)
(* by `CombineAbs.combine` via the section-local `combine_body_axiom`,  *)
(* then inlines `CombineAbs.combine` to expose the shared                *)
(* `FIPS204Sign.sign` call and synchronises via `sim`. The RHS leg is   *)
(* the symmetric of `single_party_run_refines_fips204` (which itself    *)
(* uses `S_functional_spec`). Every step is a discharged sub-lemma or a *)
(* section-local axiom; no new admit is introduced.                      *)
(* ============================================================
   IMPORTANT — citation guide:
     The implementation-backed theorem to cite for end-to-end
     N1 byte-equality correctness is

       Pulsar_N1_Extracted.pulsar_n1_byte_equality_extracted

     The generic theorem below (this file) is parametric and
     assumes the two section-local module contracts
       combine_body_axiom
       S_functional_spec.

     Both coexist intentionally: the generic version remains
     useful as a parametric contract theorem for any future
     T / S that satisfies the contracts; the concrete extracted
     version is the one that cites all the way down to specific
     extracted Jasmin/libjade modules.
   ============================================================
   GENERIC theorem: parametric over abstract `T : Pulsar_Threshold`
   and `S : MLDSA65_Sign` 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 pulsar_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 (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.
  (* Chain via SinglePartyRun(FIPS204Sign).run as the bridge module.    *)
  (*   LHS  ~ SinglePartyRun(FIPS204Sign).run                            *)
  (*       via combine_body_axiom on T.combine then inlining the         *)
  (*       CombineAbs body to expose the FIPS204Sign.sign call.          *)
  (*   SinglePartyRun(FIPS204Sign).run ~ RHS                             *)
  (*       via symmetry of single_party_run_refines_fips204.             *)
  transitivity SinglePartyRun(FIPS204Sign).run
    (={group_pk, shares, quorum, m, ctx, rho_rnd}
        /\ uniq quorum{1}
        /\ size shares{1} = size quorum{1}
        /\ group_pk{1} = derive_pk (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(FIPS204Sign).run    *)
    proc.
    (* Step A1: replace T.combine on the LHS by CombineAbs.combine via   *)
    (* the section-local refinement axiom. Threads gpk-consistency +     *)
    (* accept-path + threshold invariants through the transitivity's     *)
    (* middle precondition.                                              *)
    transitivity{1}
      { sess <- witness;
        r1s  <- [];
        r2s  <- [];
        c_tilde <- 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 (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.
    + (* T.combine ~ CombineAbs.combine via the axiom (other code is the *)
      (* same on both sides). gpk-consistency + accept-path + threshold  *)
      (* invariants are carried by the transitivity's first-leg post.    *)
      wp.
      call combine_body_axiom.
      by auto.
    (* Step A2: with LHS now calling CombineAbs.combine, inline that and *)
    (* the RHS to expose the shared FIPS204Sign.sign call.                *)
    inline CombineAbs.combine.
    wp.
    call (_: ={arg} ==> ={res}).
    + by sim.
    auto.
  + (* Step B: SinglePartyRun(FIPS204Sign).run ~ SinglePartyRun(S).run  *)
    symmetry.
    conseq single_party_run_refines_fips204.
    + move=> &1 &2 [#] 6-> Haccept.
      do! split=> //.
    + done.
qed.

end section ClassN1.

(* -------------------------------------------------------------------- *)
(* Corollary: a FIPS 204 verifier accepts every Pulsar signature      *)
(* produced by an honest quorum.                                        *)
(* -------------------------------------------------------------------- *)
(* This is exactly the Lean axiom                                       *)
(*   Crypto.Pulsar.Verify.pulsar_output_interchangeable              *)
(* lifted to EasyCrypt's probabilistic Hoare setting. Stated as a       *)
(* commented future obligation -- the body is a direct corollary of    *)
(* `pulsar_n1_byte_equality` plus FIPS 204 verifier correctness on    *)
(* outputs produced by FIPS 204 Sign (standard libjade theorem).        *)
(*                                                                       *)
(* The ops `derive_pk` and `fips204_verify` themselves are declared      *)
(* BEFORE section ClassN1 above (so `combine_body_axiom`'s precondition  *)
(* can reference `derive_pk`). They are reachable from any downstream    *)
(* file that imports `Pulsar_N1`.                                        *)
(* -------------------------------------------------------------------- *)

(* The verifier-compatibility corollary (Pr[verify ∘ ThresholdRun] = 1)
   is a direct consequence of `pulsar_n1_byte_equality` plus libjade
   `MLDSA65_Functional.sign_verify_correct`. 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. *)