zeekay df342b8bce proofs: Lean <-> EC bridge map + check-lean-bridge.sh CI guard
5-axiom Lean-to-EasyCrypt correspondence for Corona, mirroring Pulsar's
structure:

  lagrange_inverse_eval (Corona_N1.ec)
    -> Crypto.Corona.Shamir.shamir_correct_at_target

  threshold_partial_response_identity (Corona_N1.ec)
    -> Crypto.Threshold.Lagrange.threshold_partial_response_identity

  add_share_zeroR (Corona_N4.ec)
    -> Mathlib AddCommMonoid instance

  reconstruct_linear (Corona_N4.ec)
    -> Crypto.Threshold.Lagrange.combine_distributes_over_sum

  shamir_correct (Corona_N4.ec)
    -> Crypto.Corona.Shamir.shamir_correct_at_target

CI guard `scripts/check-lean-bridge.sh` verifies for every EC axiom
that (1) the axiom still exists as `axiom` (not silently demoted to
`lemma`), (2) it carries an inline citation comment naming the Lean
theorem, (3) the Lean theorem still exists at the named path. It also
checks that every EC file mentioned in the bridge doc exists on disk.

Auto-detects the Lean repo at ~/work/lux/proofs/lean or sibling
locations. Skips Lean-side existence checks if no Lean repo is on disk.

Mirrors ~/work/lux/pulsar/scripts/check-lean-bridge.sh exactly.
2026-05-19 08:38:08 -07:00
2026-05-12 09:21:34 -07:00

Corona

Lux is not merely adding post-quantum signatures to a chain; it defines a hybrid finality architecture for DAG-native consensus, with protocol-agnostic threshold lifecycle, post-quantum threshold sealing, and cross-chain propagation of Horizon finality.

See LP-105 §Claims and evidence for the canonical claims/evidence table and the ten architectural commitments — single source of truth.

Corona is the Lux Ring-LWE post-quantum threshold signature library for Quasar consensus. The 2-round threshold construction line traces back to the Boschini–Kaviani–Lai–Malavolta–Takahashi–Tibouchi R-LWE paper (ePrint 2024/1113). Corona adds the production lifecycle that line lacked: Pedersen DKG over R_q with proper hiding, proactive resharing for epoch validator rotation, identifiable abort, and the integration surface Quasar consumes.

The Module-LWE sibling library lives at luxfi/pulsar. Pulsar's threshold signature output is byte-equal to FIPS 204 single-party ML-DSA (NIST MPTC Class N1). The two libraries are independent — there is no import line between them — and Quasar consumes them as parallel kernels selected per-chain via FinalitySchemeID.

Why "Corona"

A corona is the luminous ring of light surrounding a star — visible only when the brighter central body (the Pulsar / Quasar) is partially occluded. Brand-paired with Pulsar (Module-LWE) and Quasar (the consensus that consumes both): the same family of threshold-finality light, observed at a different layer.

Production lifecycle additions

The original Boschini et al construction (ePrint 2024/1113) is a research artefact — trusted-dealer DKG, no proactive resharing, no integration surface. Corona is the production track that fills those gaps:

Layer Original R-LWE construction Corona
2-round threshold sign ✅ same byte-equal protocol ✅ inherited
Trusted-dealer Gen ✅ for fixed federation ✅ retained for bridge MPC
Proactive resharing for epoch validator rotation ❌ not specified 🚧 corona/reshare/ (this fork)
Pedersen DKG over R_q with proper hiding ❌ not specified 🚧 corona/dkg2/ (this fork)
Per-validator triple-sign integration with Quasar ❌ N/A 🚧 corona/consensus/ integration

Composition with Pulsar as optional layered PQ defense

Corona is independently usable: a chain can pick Ring-LWE Corona as its sole PQ threshold layer, no cross-dependency on Pulsar. Lux primary- network QuasarCert combines both lattice families as a Double Lattice layered defence so a break in one family does not break finality:

QuasarCert {
    BLS         — optional classical fast-path (BLS-12-381 aggregate)
    Corona      — Ring-LWE   threshold ML-DSA (this repo)
    Pulsar      — Module-LWE threshold ML-DSA (luxfi/pulsar)
    MLDSARollup — per-validator ML-DSA-65 rolled up via STARK/FRI (P3Q)
}

Each layer is checkable independently with no shared code; selecting the layer happens at chain-construction time via the FinalitySchemeID axis on the chain's ChainSecurityProfile. The pure-PQ profile drops BLS entirely and runs on Corona + Pulsar.

Layout

  • sign/ — 2-round threshold signing (byte-equal with upstream)
  • primitives/ — Shamir, hashes, MACs, PRFs (byte-equal with upstream)
  • utils/ — NTT, Montgomery, ring helpers (byte-equal with upstream)
  • networking/ — TCP peer-to-peer (byte-equal with upstream)
  • dkg/ — original Lux DKG (Feldman VSS without noise; broken for public broadcast — see RED-DKG-REVIEW). Retained for reference.
  • dkg2/ — proper Pedersen DKG over R_q (Pulsar addition; this fork)
  • reshare/ — proactive secret resharing for epoch rotation (Pulsar addition; this fork)
  • cmd/ — KAT oracle generators

Status

WIP. The 2-round Sign+Verify path is byte-equal-validated against the original R-LWE construction (ePrint 2024/1113) via 16 SHA-256 KATs. The production-lifecycle additions (resharing + Pedersen DKG) are under design and implementation.

S
Description
A 2-round lattice-based threshold signature from standard assumptions for public networks
Readme
16 MiB
Languages
Go 75.2%
eC 13.6%
TeX 5.8%
Shell 3.7%
Makefile 0.8%
Other 0.8%