pulsar/CHANGELOG.md

# CHANGELOG — Pulsar threshold ML-DSA

This file tracks substantive changes to the EasyCrypt proof
artifact, the spec, and the residual trust footprint. For
implementation-level changes see `git log`.

## v1.2.0 — TALUS threshold ML-DSA (one-round online; W-LEAK closed semi-honest)

TALUS is the threshold ML-DSA scheme on the two-round lattice kernel, adding
**one-round online signing** via three pillars: a dealerless Shamir **nonce
DKG**, the **CEF** (Carry Elimination Framework, distributed `w1`), and **CSCP**
(the CarryCompare secure-comparison protocol). Source:
`ref/go/pkg/pulsar/talus*.go`.

**PULSAR-V13-W-LEAK closed (semi-honest, simulation-proven).** Commit
`530c24e` lands the REAL CSCP secure-comparison circuit (bit-decompose +
carry-save `bitAdd` + prefix `bitLT` over BGW multiplication, validated
coefficient-exact against FIPS Decompose). On the production
`CEFComputeW1` → `cscpSecureHighBitsVec` path NO node forms `w0` or the full
commitment `w` even transiently — only three masked openings
(`{valid, maskC, w1}`) — proven leak-free by `TestCSCP_MultiNode_LeakFree`,
`TestCSCP_LeakFree_Structural`, and `TestCSCP_MaskOpen_HidesW`. HONEST SCOPE:
this is an in-process N-party SIMULATION (the harness holds all parties'
shares); the *algorithm* never reconstructs `w`/`w0`, faithfully proven, but
this is NOT yet a networked/deployed distributed MPC and the malicious-secure
layer is unbuilt.

- **Two profiles.** **Pulsar-TEE** (TEE-backed `w1` source) and **PulsarPC**
  (honest-majority N ≥ 2T−1, enforced by `TalusMinPartiesMPC` / `newCSCPCtx` /
  `cscpSecureHighBitsVec` / `bgwMulShares`). The emitted signature is
  byte-identical across profiles.
- **Stock FIPS-204 verify.** A TALUS signature verifies byte-equal under the
  UNMODIFIED `cloudflare/circl` `mldsa65.Verify` / `mldsa87.Verify`
  (`TestTalus_MPC_EndToEnd_StockVerify`, `TestTalus_MPC_Mode87`).
- **Malicious deviation = liveness-only.** `FindHint` (recovers the FIPS hint
  from public `w' = A·z − c·t1·2^d`) + `TalusReleaseGate` (mandatory stock
  FIPS-204 verify; never releases a failed signature) bound any malicious CSCP
  deviation to abort/retry — never forge or leak
  (`TestCSCP_WrongW1_CaughtByFindHint`). This is the open **Residual A** (the
  CSCP malicious-secure / identifiable-abort layer + a networked,
  non-simulation MPC deployment).
- **KEYGEN is now DEALERLESS (RSS) — the dealer is dead at keygen (v0.6.0+).**
  Superseded the earlier "trusted-dealer / Residual B" status. Only the NAIVE
  additive lift is unreachable: a naive sum/Lagrange of N ≥ 2 `S_η` contributions
  has ℓ∞-support up to `N·η > η`, breaking BCC byte-validity (`‖c·s2‖∞ ≤ N·β > β`)
  — `naive_additive_seta_obstruction.go` returns `ErrDealerlessByteFIPSUnreachable`
  for THAT construction only, **not as a class impossibility**. The published
  escape is **Mithril short replicated secret sharing** (`mithril_rss.go`
  `MithrilRSSKeygen`): committee keygen with no dealer and no centralized
  reconstruction, whose group key signs under **stock unmodified** `mldsa65.Verify`
  (gold-proof at (t=8,n=8), (t=16,n=16), and all small committees `N≤6`;
  `accumulateSubset` per-subset reduction unblocks large committees, v0.6.3). The
  HYPERBALL 3-round signer (`mithril_rss_hyperball.go`) is the Mithril-native
  no-reconstruct signer over that key. **Scope:** standard-verifier-compatible is
  PROVEN; full FIPS-204 KeyGen-distribution-equivalence (simulation/hiding/
  abort-bias) remains a labeled residual. The dealerless **Corona** leg (Pedersen
  DKG over `R_q`) continues to carry permissionless-public safety alongside Pulsar
  in the Quasar AND-mode dual-PQ cert.

## v1.1.0 – v1.1.5 — BCC/CEF byte-equal threshold ML-DSA + honest-status hardening

The Boundary-Clearance-Condition (BCC) + Carry-Elimination (CEF)
no-reconstruct signing path: the hint is recovered from the **public**
`w' = A·z − c·t1·2^d` via `FindHint` (FIPS `UseHint`), no production code forms
`c·s2`/`c·t0`/`r0`, and the single-key BCC signature verifies byte-for-byte
under CIRCL + pq-crystals (ML-DSA-65/87). The leaking v0.3 `AlgebraicAggregate*`
path was deleted forward-only; PULSAR-V04-CTX (FIPS 204 §5.4 ctx-bound sign)
closed; and the proof-claim vocabulary was hardened to an honest two-model
framing (idealised reconstruct-then-sign vs the production no-leak residual
under a standard Module-LWE / Module-SIS reduction).

## v1.0.14 — v0.2 honesty rename (Algebraic → Transitional)

The v0.2 API previously named `Algebraic*` was materially
misleading: the file-header docstring claimed
`AlgebraicCombine is a pure function of public-only material;
no access to any party's seed share or the master ML-DSA private
key` while the implementation calls
`mldsaSign(setup.SkBytes, message, ...)` against the master sk
packed in `AlgebraicSetup.SkBytes`. The aggregator TCB at sign
time is therefore identical to v0.1 reconstruct-and-sign — only
the parties' side of the protocol is honestly algebraic.

v1.0.14 fixes the honesty defect without changing the algorithm:

**API rename (forward-only, no compat aliases):**

- `AlgebraicThresholdSigner` → `TransitionalThresholdSigner`
- `NewAlgebraicThresholdSigner` → `NewTransitionalThresholdSigner`
- `AlgebraicCombine` → `TransitionalAggregate`
- `AlgebraicSetup` → `TransitionalSetup`
- `AlgebraicRound1Message` → `TransitionalRound1Message`
- `AlgebraicRound2Message` → `TransitionalRound2Message`
- `DealAlgebraicShares` → `DealTransitionalShares`
- `ErrAlgRound1MACBad` → `ErrTransitionalRound1MACBad`
- `ErrAlgRound2MACBad` → `ErrTransitionalRound2MACBad`
- `ErrAlgRound2CommitBad` → `ErrTransitionalRound2CommitBad`
- `ErrAlgRestart` → `ErrTransitionalRestart`
- `ErrAlgNoSetup` → `ErrTransitionalNoSetup`
- All `TestV02_*` test functions renamed to `TestTransitional_*`.

**Honesty docstrings rewritten:**

- `threshold_v02.go` file header now opens with HONEST SCOPE
  declaring the aggregator-side SkBytes dependency.
- `TransitionalAggregate` docstring spells out the TCB equivalence
  with v0.1 at sign time.
- `TransitionalSetup` docstring declares SkBytes as the v0.2 TCB
  defect and the v0.3 graduation gate.
- `types.go` Signature docstring rewritten.
- `docs/deployment.md` v0.2 section rewritten with explicit
  "suitable / not suitable" deployment guidance and a v0.3
  milestone section.

**New load-bearing test:**

- `TestTransitional_DependsOnSkBytes` — runs the full Round1/Round2
  cycle then sets `setup.SkBytes = nil` and asserts
  `TransitionalAggregate` returns `ErrTransitionalNoSetup`. The
  test currently PASSES (because v0.2 indeed depends on SkBytes).
  When v0.3 ships and removes the SkBytes dependency, this test
  starts FAILING — that failure is the load-bearing red flag
  documenting the v0.3 graduation.

**Closure record (PULSAR-V03-1):**

- `BLOCKERS.md` entry `PULSAR-V03-1` (closed in v1.0.20, commit
  `023a3ed`) records the v0.3 algebraic-sign closure: port FIPS 204
  sign internals to polynomial-share arithmetic, drop SkBytes,
  rename `Transitional*` → `Algebraic*` (forward-only).

The wire protocol is byte-for-byte unchanged: protocol constants
(`PULSAR-ALG-*` customisation strings) are preserved so any
existing v0.2 test vectors continue to verify.

## v1.0.13

(See git log; v0.2 algebraic threshold wire shape — the rename
above retroactively documents the honesty caveat that should have
shipped with this tag.)

## v0.1.0 (target tag: `submission-2026-11-16`)

### Proof artifact progression (v4 → v11)

| Version | SHA | Change | Trust-footprint effect |
|---|---|---|---|
| v4 | `2eae979` | byte-walk: factor through pack_n1_signature | Component-triple axioms with codec roundtrip in `Pulsar_N1.ec` |
| v4b | `564a330` | per-stage split | 2 component-triple → 6 stage-level axioms; broader surface but per-FIPS-stage |
| v5 | `58af7b4` | c_tilde stage decomposition | `*_body_c_tilde_spec` → derived lemmas via mu + w1 sub-axioms |
| v5a | `01025bc` | docs: c_tilde refactor is decomposition not closure | wording correction |
| v6 | `18d01af` | mu sub-stage decomposed via SHAKE/byte-layout | `*_body_mu_spec` → derived lemmas |
| v7 | `76eae80` | w1 sub-stage via HighBits structural split | `*_body_w1_spec` → derived lemmas |
| v7b | `1bcb1eb` | PQ security validation framework (6 evidence layers) | docs framing |
| v8 | `835c176` | combine z-stage via Lean Lagrange bridge | `combine_body_z_spec` → derived lemma; new Lean-bridged `threshold_partial_response_identity` |
| v9 base | `01bdbc3` | mu_shake_input_t = int list concretization | constructive prep |
| v9 + v10 | `83e3c38` | 3-agent parallel: sign mu_input close + combine mu_input decomp + h-stage MakeHint bridge | `*_body_{mu_input,h}_spec` → derived lemmas |
| v10 docs | `ec14c79` | full submission package: PATENTS + AXIOM-INVENTORY + PROOF-CLAIMS + FIPS-TRACEABILITY + TRUSTED-COMPUTING-BASE + NIST-SUBMISSION + docs/evaluation + docs/patent-claims | submission-grade documentation |
| v11 sign z | `02c29f2` | sign z-stage via z = y + c·s1 structural split | `sign_body_z_spec` → derived lemma; 2 new sub-axioms `sign_body_y_spec` + `sign_body_cs1_spec` |
| v11 codec | `81da17b` | signature_t concretization as record wrapping int list | **3 codec axioms ELIMINATED** (real closure, not decomposition) |
| v12 w_spec | `02798c7` | w-stage via ExpandA + ExpandMask + mat_vec_mul structural split | `*_body_w_spec` × 2 → derived lemmas; 4 new sub-axioms (matrix_a + mask_y on each side) |
| v13 accept | `02798c7` | per-R1/R2/R3/R4 accept bridge axiom (no-reject decomposition prep) | +1 bridge axiom (`accept_signing_attempt_iff_R1234`) connects bundled predicate to 4 per-R conditions without breaking downstream tactics |

### Derived lemmas added (previously primitive axioms)

After v10, the following primitive axioms have been converted to
derived lemmas (the original obligation now follows from narrower
sub-axioms + structural composition):

- `combine_body_c_tilde_spec`, `sign_body_c_tilde_spec` (v5)
- `combine_body_mu_spec`, `sign_body_mu_spec` (v6)
- `combine_body_w1_spec`, `sign_body_w1_spec` (v7)
- `combine_body_z_spec` (v8 — Lean-bridged)
- `combine_body_mu_input_spec`, `sign_body_mu_input_spec` (v9)
- `combine_body_h_spec`, `sign_body_h_spec` (v10)
- `sign_body_z_spec` (v11 — z = y + c·s1 structural split)
- `combine_body_w_spec`, `sign_body_w_spec` (v12 — A·y structural split)

Total: 14 axioms re-classified into derived lemmas across v5–v13.

### Actual axiom eliminations (v11 codec, real closure)

In addition to the 12 re-classifications above, v11 also delivered
3 PRIMITIVE AXIOM ELIMINATIONS in `Pulsar_N1_Signature_Codec.ec`
(no replacement axiom on that path — concretized `signature_t` as
a record wrapper):

- `encode_decode_signature` (removed)
- `decode_encode_signature_wf` (removed)
- `encode_signature_wf` (kept, narrowed to a length-only axiom)
- `encode_signature_len` → DERIVED via record-wrap structure

3 axioms eliminated from the codec layer.

### Trust-footprint structure (post v10)

Per `docs/proof-axiom-inventory.md`. This is NOT a count-reduction — it is a
re-classification of formerly broad obligations into narrower,
independently-attackable sub-obligations:

- 1 stage-level byte-walk (sign z only — combine z moved to Lean bridge path)
- 2 c_tilde dependency w sub-stage (combine + sign)
- 2 c_tilde dependency w_low sub-stage (combine + sign, v10)
- 2 combine z extraction (v8 — aggregation shape + per-party PR)
- 4 codec mu_input layout (v9 — combine 3 per-range + sign byte-layout)
- 2 accepted-path no-reject (combine + sign)
- 5 Lean-bridged algebraic (v8 added threshold_partial_response_identity)
- 1 + ~21 codec roundtrip
- EC admit budget hard-pinned at 0/0

### Gate properties maintained throughout

- 13/13 EC files compile clean
- jasmin-ct 3/3 blocking on threshold layer (round1, round2, combine)
- Lean ↔ EC bridge guard 5/5
- Admit budget 0/0
- Lean bridge doc + check-script entry per bridged axiom
- Refinement scaffold (no stray `declare axiom`) clean

### Submission documentation added (v10)

- `SUBMISSION.md` — NIST MPTC cover sheet (updated with Tier-1/2/3 labels + patent posture cross-ref; absorbed prior one-page executive summary)
- `docs/patents.md` — royalty-free patent grant + defensive termination + claim summary
- `docs/proof-axiom-inventory.md` — per-axiom residual trust accounting with closure plans
- `docs/proof-claims.md` — narrow EC/Lean refinement claim with explicit non-claims
- `docs/fips-204-traceability.md` — op/lemma → FIPS 204 § map (ACVP/CAVP-ready)
- `docs/tcb.md` — EC/Jasmin/OCaml/Lean TCB with per-layer risk
- `docs/patent-claims.md` — 21 numbered claim drafts (5 claim groups) for attorney review
- `docs/evaluation.md` — experimental evaluation report per NIST IR 8214C §6

### Adjacent tracks (each routes through its own work stream)

- κ-loop probabilistic Hoare model — `mldsa_accept_lower_bound` ≈ 1 − 2⁻¹²⁸ tracks the operational bound per the standard FIPS 204 treatment.
- Full bit-level FIPS 204 codec mechanisation — Barbosa-Barthe-Dupressoir Dilithium template (CRYPTO 2023).
- Lean ↔ EC checked translation tooling — research artifact.
- ACVP / CAVP algorithm validation certificate — accredited-lab track.
- FIPS 140-3 module validation — accredited-lab track on a packaged crypto module.
- Threshold SLH-DSA (Tier 3) — Magnetar research track at `docs/magnetar.md`.
- Optimised Rust / C / WASM bindings — downstream binary packaging (Tier 1 priorities in `docs/roadmap.md`).
- External cryptographic audit — scoped post-submission alongside reviewer feedback.

### What this submission DOES claim (precise)

> Under the trusted-computing base in `docs/tcb.md`
> and the residual axioms enumerated in `docs/proof-axiom-inventory.md`, every
> signature byte string produced by the Pulsar Combine procedure on
> inputs satisfying the protocol's threshold-interpolation
> well-formedness invariants is bit-identical to a signature
> produced by single-party FIPS 204 ML-DSA-65 Sign on the
> Lagrange-reconstructed group secret.

This is an implementation-correctness result. It does NOT prove
post-quantum hardness of ML-DSA itself; ML-DSA hardness is inherited
from NIST FIPS 204's analysis. See `docs/proof-claims.md` for the
explicit framing.

### Scope boundary (per `BLOCKERS.md` closed-finding registry)

- Identifiable abort under network partition: synchronous model only; asynchronous attribution routes through the consensus-layer accountability artifact.
- 1-round signing: FIPS 204 rejection sampling precludes a 1-round threshold variant under any NIST-standard preprocessing oracle.
- DKG bias resistance under collusion: deployments bind a randomness beacon at the chain layer.
- Cross-committee reshare without external state binding: deployments bind the reshare epoch to consensus-layer state.

---

## v0.0 (pre-MPTC submission)

Initial reference implementation + spec, prior to the v4 byte-walk
factoring work. See `git log` for early commit history.

---

**Document metadata**

- Name: `CHANGELOG.md`
- Date: 2026-05-18
- Versioning: this file tracks proof-artifact and submission-package
  versions; the production code library will eventually have its own
  semver.