mirror of
https://github.com/luxfi/corona.git
synced 2026-07-27 02:50:34 +00:00
proofs: honest bucketed axiom inventory + reconstruct-then-sign disclosure
Reclassify (not reduce) the EasyCrypt axiom surface and correct the prior
inventory's understatement. NO axioms discharged this pass (honest): no
easycrypt toolchain on host, and every in-file-derivable axiom is already a
proved lemma; residual A/B axioms are over abstract ops/constants
(op group_pk_width : int., op sig_len : int.) and the C axioms are open.
- AXIOM-INVENTORY.md: replace the §2 table that mislabelled the wrapper
bridges and section-local module contracts as "Discharged in the
Wrapper". They are now correctly bucket C / OPEN: combine_body_spec hides
the Boschini combine steps 2-6, and combine_abs_op_lifted_bridge /
sign_abs_op_lifted_eq_rlwe pin the lifted op to rlwe_sign_op on the
Lagrange-RECONSTRUCTED master secret (reconstruct-then-sign). Complete
bucketed census of all 56 axioms -- A (18, 5 Lean-bridged), B (27), C
(11) -- one row per axiom with name, file:line, justification. CT
contracts (sign_round{1,2}_constant_time) classified C/fail-closed.
- PROOF-CLAIMS.md: add assurance vocabulary + two load-bearing disclosures
-- (1) the EC byte-equality MODELS reconstruct-then-sign; (2) Corona has
NO independent interop verifier (R-LWE has no NIST target), so its
byte-equality is asserted + same-construction Go<->C++ KAT, never
"proven/verified". Corrects the §4 claim that Pulsar is machine-checked
"at every step" (it too rests on the same reconstruct-then-sign cone).
- BLOCKERS.md (new): CORONA-EC-RECON-MODEL, CORONA-CT-PENDING,
CORONA-NO-INDEP-VERIFIER -- all OPEN, all cross-referenced to the shared
external-review gate.
- .assurance/reviewed-axioms.txt: list every load-bearing / security-cone
axiom (A: 5 Lean-bridged; C: combine_body_axiom, S_functional_spec,
combine_body_spec, combine_abs_op_lifted_bridge, sign_abs_op_lifted_eq_rlwe)
with bucket + justification.
- .assurance/budget.txt: correct prose (0 real admit. tactics; AXIOM=56 exact).
Framework gate (circular-proof + axiom-budget + the other three) PASS with
full disclosure. go test ./... green (no Go touched).
This commit is contained in:
Antje Worring
+20
-4
@@ -1,9 +1,25 @@
|
||||
# Unproven-assertion budget (max counts). Enforced by
|
||||
# ~/work/lux/proofs/framework/checks/axiom-budget.sh. FAILS on any drift above.
|
||||
# Goal: decrease, never raise. Current surface (2026-06). The EasyCrypt
|
||||
# byte-equality proof still models a secret-reconstructing abstraction with the
|
||||
# steps 2-6 reduction open (see AUDIT-2026-06); those open steps are the bulk of
|
||||
# the 56 axioms and are tracked for discharge in PROOF-CLAIMS.
|
||||
# Goal: decrease, never raise.
|
||||
#
|
||||
# Current surface (reclassified, not reduced, this pass). The 56 axioms are
|
||||
# fully bucketed in AXIOM-INVENTORY.md:
|
||||
# A standard-math-fact (18) | B serialization/layout (27) |
|
||||
# C OPEN security assumption (11, reconstruct-then-sign; see BLOCKERS.md).
|
||||
# The EC byte-equality proof MODELS reconstruct-then-sign: CombineAbs
|
||||
# reconstructs the master secret and signs with it (steps 2-6 of the Boschini
|
||||
# combine are open inside combine_body_spec / the wrapper bridges). Those open
|
||||
# steps are the bulk of the C axioms; the production no-leak path is interop-
|
||||
# tested (Go<->C++ KAT), NOT EC-proven.
|
||||
# 0 NEW discharges this pass: no EasyCrypt toolchain on host, and every
|
||||
# in-file-derivable axiom is already a proved lemma; residual A/B axioms are
|
||||
# over abstract ops/constants (op group_pk_width : int., op sig_len : int.)
|
||||
# not dischargeable without a verify-gated concretization.
|
||||
#
|
||||
# Real `admit.` tactics = 0 (scripts/checks/ec-admits.sh, matching ^admit.$,
|
||||
# is authoritative). ADMIT=3 below is the budget regex counting the WORD
|
||||
# "admit" in comments; informational only. AXIOM=56 is exact (no comment
|
||||
# false-positives in this tree).
|
||||
SORRY=0
|
||||
ADMIT=3
|
||||
AXIOM=56
|
||||
|
||||
@@ -1,7 +1,28 @@
|
||||
# Axioms that a LOAD-BEARING lemma rests on, reviewed and justified.
|
||||
# Format: AXIOM_NAME <justification>
|
||||
# An entry MUST be a cited standard fact or a layout/encoding identity, NEVER a
|
||||
# restatement of a security conclusion.
|
||||
# Enforced by ~/work/lux/proofs/framework/checks/circular-proof.sh.
|
||||
# Format: AXIOM_NAME <bucket> -- <justification>
|
||||
#
|
||||
# An entry MUST be a cited standard fact, a layout/encoding identity, or a
|
||||
# DISCLOSED-AND-OPEN security assumption -- NEVER a silently-closed security
|
||||
# conclusion. The framework (circular-proof.sh) HARD-requires only axioms a
|
||||
# load-bearing-named lemma discharges via apply/exact in <=12 lines (today:
|
||||
# lagrange_inverse_eval). We list MORE than the mechanical minimum so the
|
||||
# whole trust cone of corona_n1_byte_equality is written down. This is full
|
||||
# disclosure, NOT a blanket allow: only load-bearing / security-cone axioms
|
||||
# appear; pure layout/length B-axioms and structural-only A-axioms are
|
||||
# inventoried in AXIOM-INVENTORY.md. Buckets: A standard-math-fact |
|
||||
# B serialization/layout | C OPEN security assumption (reconstruct-then-sign;
|
||||
# see BLOCKERS.md).
|
||||
|
||||
lagrange_inverse_eval Standard Lagrange interpolation: constant-term recovery from t distinct evaluations over a field of order > committee size. Field-theory primitive EasyCrypt lacks built-in; candidate for discharge against Mathlib `lagrange`. NOT a security conclusion -- the algebraic core the Raccoon-family threshold reduction uses.
|
||||
# --- A: load-bearing standard-math-fact (mechanically flagged) ---
|
||||
lagrange_inverse_eval A -- Lagrange-at-0 secret recovery from t distinct evaluations over a field of order > committee size. EasyCrypt lacks this over abstract share_t; Lean-bridged to Crypto.Corona.Shamir.shamir_correct_at_target. The algebraic core the Raccoon/Boschini-family threshold reduction USES, NOT the security claim. Used by reconstruct_of_share via `exact:`.
|
||||
threshold_partial_response_identity A -- Lagrange-aggregation of partial responses = rlwe_compute_z on the reconstructed share. Lean-bridged. Load-bearing in the combine refinement cone.
|
||||
reconstruct_linear A -- reconstruction linear over share-list addition. Lean-bridged. Load-bearing for the N4 reshare-preservation lemmas.
|
||||
shamir_correct A -- reconstruction left-inverse of fresh sharing (Lagrange-at-zero). Lean-bridged. Load-bearing for honest_reshare_reconstructs / reshare_preserves_secret_honest (N4).
|
||||
add_share_zeroR A -- additive identity on share_t (AddCommMonoid). Lean-bridged. Load-bearing for the N4 zero-sharing argument.
|
||||
|
||||
# --- C: OPEN security assumptions in the byte-equality cone (reconstruct-then-sign; steps 2-6 open). DISCLOSED, NOT closed. See BLOCKERS.md. ---
|
||||
combine_body_axiom C -- OPEN. declare axiom: T.combine ~ CombineAbs.combine on honest-quorum inputs == the extracted threshold combine equals the centralised RLWE sign of the LAGRANGE-RECONSTRUCTED secret. corona_n1_byte_equality rests on it. Closure = the Jasmin byte-walk (v0.8.0). NOT proven.
|
||||
S_functional_spec C -- OPEN. declare axiom: S.sign ~ CentralRLWESign.sign on accepted inputs == the single-party module is a faithful Boschini signer. corona_n1_byte_equality rests on it. NOT proven.
|
||||
combine_body_spec C -- OPEN. the Jasmin-extracted combine writes exactly combine_abs_op(args); the Boschini combine steps 2-6 (open/aggregate/reject) are INSIDE this atomic byte-walk axiom, unproved. wrapper_combine_refines_abs / corona_n1_byte_equality_extracted rest on it. NOT proven.
|
||||
combine_abs_op_lifted_bridge C -- OPEN. share-typed lifted combine op = byte-level combine_abs_op modulo encoding; the security content of wrapper_combine_refines_abs rides here. NOT proven.
|
||||
sign_abs_op_lifted_eq_rlwe C -- OPEN. the reconstruct-then-sign identity: sign_abs_op_lifted sk = rlwe_sign_op sk == the lifted op IS the centralised Boschini signer. wrapper_sign_refines_central rests on it. NOT proven.
|
||||
|
||||
+205
-110
@@ -1,133 +1,228 @@
|
||||
# AXIOM-INVENTORY -- Corona
|
||||
# AXIOM-INVENTORY — Corona (bucketed, honest, complete)
|
||||
|
||||
> Honest enumeration of every cryptographic assumption + residual
|
||||
> axiom Corona depends on. This document is load-bearing for the
|
||||
> Tier A submission gate: per the project rubric, AXIOM-INVENTORY
|
||||
> MUST be reviewable by an external cryptographer and MUST close
|
||||
> every residual axiom with either a closure plan or an explicit
|
||||
> non-closure rationale.
|
||||
> Honest enumeration of every cryptographic assumption + residual EC
|
||||
> axiom Corona depends on, classified into exactly one bucket with a
|
||||
> per-axiom justification. This document is the disclosure artifact for
|
||||
> the Tier-A submission gate and the merge gate "remaining axioms not
|
||||
> discharged OR reclassified": every residual axiom is RECLASSIFIED
|
||||
> (bucketed + justified), and the genuinely-open security assumptions are
|
||||
> flagged **C / OPEN** and tracked in `BLOCKERS.md`.
|
||||
>
|
||||
> Status at **v0.7.0**: EC theory artifacts have landed. 13 EC files
|
||||
> mirror the Pulsar Tier A layout. The admit budget is **0/0**
|
||||
> across the EC file set (statically tracked by
|
||||
> `scripts/checks/ec-admits.sh`). Section §2 enumerates the residual
|
||||
> axioms (top-level `axiom` declarations and `declare axiom`s inside
|
||||
> sections), each cited with its closure pathway.
|
||||
> Status correction (this pass): the prior revision of §2 labelled the
|
||||
> wrapper-bridge axioms (`combine_abs_op_lifted_bridge`,
|
||||
> `sign_abs_op_lifted_eq_rlwe`) and the section-local `combine_body_axiom`
|
||||
> / `S_functional_spec` as "Discharged in the Wrapper". That was
|
||||
> **understated**. The wrapper *lemmas* (`wrapper_combine_refines_abs`,
|
||||
> `wrapper_sign_refines_central`) are real EasyCrypt, but they REST ON
|
||||
> those bridge axioms, and the bridge axioms carry the security content
|
||||
> (they assume the aggregated combine equals `rlwe_sign_op` of the
|
||||
> **Lagrange-reconstructed master secret**). They are now correctly
|
||||
> classified **C / OPEN**.
|
||||
|
||||
## §1 Construction-level axioms (cryptographic assumptions)
|
||||
## Buckets
|
||||
|
||||
These are the underlying hardness + soundness assumptions of the
|
||||
R-LWE threshold construction. They are NOT closed in any Lux work --
|
||||
they are the substrate of the security argument and are inherited
|
||||
from the academic literature.
|
||||
- **A — STANDARD-MATH-FACT.** Cited field/algebra/coding identity EC lacks
|
||||
built-in over the abstract types in play. Legitimate; cite the source.
|
||||
- **B — SERIALIZATION/LAYOUT-IDENTITY.** encode/decode round-trips,
|
||||
byte-length facts, layout refinement over abstract ops/constants.
|
||||
Dischargeable only after concretizing the op/constant.
|
||||
- **C — OPEN SECURITY ASSUMPTION.** Security-relevant content the reduction
|
||||
has NOT closed — the steps-2–6 combine body + the reconstruct-then-sign
|
||||
`CombineAbs` abstraction. **MUST stay open and disclosed.** Tracked in
|
||||
`BLOCKERS.md`.
|
||||
|
||||
| Axiom | Reference | Rationale for non-closure |
|
||||
## §1 Construction-level assumptions (cryptographic substrate — NOT Lux-closable)
|
||||
|
||||
These are the underlying hardness + soundness assumptions of the R-LWE
|
||||
threshold construction, inherited from the literature. They are not closed
|
||||
in any Lux work and are not counted in the EC axiom histogram below.
|
||||
|
||||
| Assumption | Reference | Rationale for non-closure |
|
||||
|---|---|---|
|
||||
| **Module-LWE / Ring-LWE hardness** | Lyubashevsky-Peikert-Regev (TOC 2013) for R-LWE; Langlois-Stehle (Designs, Codes 2015) for module variants | Standard PQ lattice hardness assumption; same substrate as ML-DSA / ML-KEM. Not a Corona-specific assumption. |
|
||||
| **Short Integer Solution (SIS) hardness over `R_q`** | Ajtai (1996); Micciancio-Regev (SIAM 2007) for ring variant | Unforgeability of Corona's underlying signature reduces to R-SIS at the parameters in `sign/config.go`. Not closing. |
|
||||
| **Boschini-Kaviani-Lai-Malavolta-Takahashi-Tibouchi construction soundness** | IACR ePrint 2024/1113; IEEE S&P 2025 | The 2-round threshold-signing protocol's UC-soundness is proved in the cited paper. Lux's production fork inherits this proof; the Lux modifications (Pedersen-VSS DKG, keyera lifecycle, proactive reshare) are conservative additions analyzed below. |
|
||||
| **Pedersen-VSS soundness** | Pedersen (CRYPTO 1991) | Lux's DKG (`dkg2/`) uses Pedersen-VSS to replace the upstream broken Feldman commit. Soundness reduces to discrete-log hardness in the underlying group; assumed. |
|
||||
| **cSHAKE256 / KMAC256 collision + preimage resistance** | NIST SP 800-185 | Used in `hash/sp800_185.go` for domain-separated hashing across DKG, signing, reshare. Hash function security is standard assumption. |
|
||||
| Module-LWE / Ring-LWE hardness | Lyubashevsky-Peikert-Regev (TOC 2013); Langlois-Stehlé (DCC 2015) | Standard PQ lattice hardness; same substrate as ML-DSA / ML-KEM. |
|
||||
| R-SIS hardness over `R_q` | Ajtai (1996); Micciancio-Regev (SIAM 2007) | Unforgeability reduces to R-SIS at `sign/config.go` parameters. |
|
||||
| Boschini-Kaviani-Lai-Malavolta-Takahashi-Tibouchi soundness | IACR ePrint 2024/1113; IEEE S&P 2025 | The 2-round threshold protocol's UC-soundness is in the cited paper; Lux's fork inherits it. Note: this is the Ringtail/Corona-family paper, NOT a Pulsar citation. |
|
||||
| Pedersen-VSS soundness | Pedersen (CRYPTO 1991) | Corona's DKG (`dkg2/`) reduces to discrete-log hardness. |
|
||||
| cSHAKE256 / KMAC256 collision + preimage resistance | NIST SP 800-185 | Domain-separated hashing across DKG/signing/reshare. |
|
||||
|
||||
## §2 EC residual axioms (v0.7.0 inventory)
|
||||
## §2 EC residual axioms — histogram (56 real axiom declarations)
|
||||
|
||||
The 13 EC files compile against the `axiom` and `declare axiom`
|
||||
declarations enumerated below. Each is one of: (a) an algebraic
|
||||
identity discharged in Lean (5 Lean-bridged axioms), (b) a structural
|
||||
type/codec property closed at the wrapper layer, or (c) a Boschini
|
||||
ePrint 2024/1113 construction-level identity cited at its inline
|
||||
comment.
|
||||
| Bucket | Count | Discharged this pass | Remaining |
|
||||
|---|---:|---:|---:|
|
||||
| A — standard-math-fact | 18 | 0 (abstract algebra / Lean-bridged) | 18 |
|
||||
| B — serialization/layout | 27 | 0 (abstract ops/constants) | 27 |
|
||||
| C — open security assumption | 11 | 0 (must stay open) | 11 |
|
||||
| **Total** | **56** | **0** | **56** |
|
||||
|
||||
| Axiom | File | Status | Closure pathway |
|
||||
> **Discharged this pass: 0 new.** Reason (honest): no EasyCrypt toolchain
|
||||
> on this host (no `easycrypt`/`alt-ergo`/`why3`), and everything
|
||||
> dischargeable from in-file material is already a proved lemma
|
||||
> (`encode_decode_signature`, `decode_encode_signature_wf`,
|
||||
> `encode_signature_len`, `read_after_write_sig`, `write_sig_separation`,
|
||||
> `pack_n1_signature_injective`, `reconstruct_of_share`,
|
||||
> `reconstruct_quorum_invariant`, `fresh_sharing_zero_is_zero`,
|
||||
> `combine_post_signature`, `combine_idempotent`, `sign_post_signature`,
|
||||
> `sign_idempotent`, `wrapper_combine_refines_abs`,
|
||||
> `wrapper_sign_refines_central`, `corona_n1_byte_equality_extracted`). The
|
||||
> residual A-axioms are over abstract algebra (`inf_norm_R : R_q -> int`),
|
||||
> and the residual B-axioms are over abstract ops/constants
|
||||
> (`op group_pk_width : int.`, `op sig_len : int.`, `share_encode`/`decode`
|
||||
> abstract). Discharging them requires concretizing those — a verify-gated
|
||||
> wire-format decision that cannot be done blind and machine-rechecked
|
||||
> here. Faking such a discharge is the cheat the gate forbids. The honest
|
||||
> reclassification + disclosure below is the gate-satisfying outcome.
|
||||
|
||||
EC admit budget remains **0 / 0** (real `admit.` tactics; statically
|
||||
guarded by `scripts/checks/ec-admits.sh`). The `.assurance/budget.txt`
|
||||
ADMIT key counts the *word* "admit" in comments and is informational.
|
||||
|
||||
---
|
||||
|
||||
### Bucket A — STANDARD-MATH-FACT (18)
|
||||
|
||||
| # | Axiom | File:line | Justification | Discharge path |
|
||||
|---|---|---|---|---|
|
||||
| A1 | `lagrange_inverse_eval` | Corona_N1.ec:266 | Lagrange-at-0 secret recovery from t distinct evals. **Load-bearing** (`reconstruct_of_share` uses `exact:`). | Lean-bridged `Crypto.Corona.Shamir.shamir_correct_at_target`. Acknowledged in reviewed-axioms.txt. |
|
||||
| A2 | `threshold_partial_response_identity` | Corona_N1.ec:478 | Lagrange-aggregation of partial responses = `rlwe_compute_z` on reconstructed share. | Lean-bridged `Crypto.Threshold.Lagrange.threshold_partial_response_identity`. |
|
||||
| A3 | `reconstruct_linear` | Corona_N4.ec:140 | Reconstruction linear over share-list addition. | Lean-bridged `Crypto.Threshold.Lagrange.combine_distributes_over_sum`. |
|
||||
| A4 | `shamir_correct` | Corona_N4.ec:151 | Reconstruction left-inverse of fresh sharing. | Lean-bridged `Crypto.Corona.Shamir.shamir_correct_at_target`. |
|
||||
| A5 | `add_share_zeroR` | Corona_N4.ec:133 | Additive identity on `share_t`. | Lean-bridged Mathlib `AddCommMonoid`. |
|
||||
| A6 | `l2_norm_sq_vec_N_nonneg` | RLWE_Functional.ec:128 | L2² norm ≥ 0 (abstract `l2_norm_sq_vec_N`). | Discharge after norm concretization. |
|
||||
| A7 | `l2_norm_sq_vec_M_nu_nonneg` | RLWE_Functional.ec:129 | As A6 over `vec_M_nu`. | As A6. |
|
||||
| A8 | `inf_norm_R_nonneg` | RLWE_Functional.ec:130 | inf-norm ≥ 0 over `R_q`. | As A6. |
|
||||
| A9 | `rlwe_correctness` | RLWE_Functional.ec:212 | Boschini ePrint 2024/1113 §3 correctness theorem (cited). | Inherited from the paper; not Lux-closable. |
|
||||
| A10 | `share_to_bits_id` | RLWE_Functional.ec:238 | Type-identification pass-through. | Discharge after type identification is definitional. |
|
||||
| A11 | `msg_to_bits_id` | RLWE_Functional.ec:239 | As A10. | As A10. |
|
||||
| A12 | `ctx_to_bits_id` | RLWE_Functional.ec:240 | As A10. | As A10. |
|
||||
| A13 | `rnd_to_bits_id` | RLWE_Functional.ec:241 | As A10. | As A10. |
|
||||
| A14 | `bits_to_sig_id` | RLWE_Functional.ec:242 | As A10. | As A10. |
|
||||
| A15 | `poly_degree_nonneg` | Corona_N1.ec:245 | `0 <= poly_degree s` (abstract `poly_degree`). | Discharge after `share_t` concretization. |
|
||||
| A16 | `accept_signing_attempt_iff_components` | Corona_N1.ec:547 | accept ⇔ (l2-z ∧ l2-Δ ∧ full-rank): algebra of the R-LWE accept predicate. | Discharge with the concrete accept predicate. |
|
||||
| A17 | `compute_mu_injective` | Corona_N1.ec:563 | distinct (m,ctx) ⇒ distinct mu (transcript binder injectivity). | Discharge with concrete transcript_hash. |
|
||||
| A18 | `context_bytes_len_bound` | Corona_N1.ec:356 | `0 <= |context_bytes ctx| <= 65535`. | Discharge after `context_bytes` concretization. |
|
||||
|
||||
---
|
||||
|
||||
### Bucket B — SERIALIZATION / LAYOUT-IDENTITY (27)
|
||||
|
||||
| # | Axiom | File:line | Justification |
|
||||
|---|---|---|---|
|
||||
| `lagrange_inverse_eval` | `Corona_N1.ec` | Lean-bridged | `Crypto.Corona.Shamir.shamir_correct_at_target` (Lean) |
|
||||
| `threshold_partial_response_identity` | `Corona_N1.ec` | Lean-bridged | `Crypto.Threshold.Lagrange.threshold_partial_response_identity` (Lean) |
|
||||
| `reconstruct_linear` | `Corona_N4.ec` | Lean-bridged | `Crypto.Threshold.Lagrange.combine_distributes_over_sum` (Lean) |
|
||||
| `shamir_correct` | `Corona_N4.ec` | Lean-bridged | `Crypto.Corona.Shamir.shamir_correct_at_target` (Lean) |
|
||||
| `add_share_zeroR` | `Corona_N4.ec` | Lean-bridged | Mathlib `AddCommMonoid` instance |
|
||||
| `share_dim_correct`, `poly_share_roundtrip` et al. | `Corona_N1.ec` | Structural | Type-level invariant; concretization closes |
|
||||
| `reconstruct_polys_view`, `share_polys_injective`, `poly_share_of_injective`, `poly_share_of_share_polys` | `Corona_N1.ec` | Structural | Pinning the abstract share_t to its polynomial-vector view |
|
||||
| `poly_degree_nonneg`, `context_bytes_len_bound` | `Corona_N1.ec` | Definitional | Trivially provable once share_t is concretized |
|
||||
| `accept_signing_attempt_iff_components` | `Corona_N1.ec` | Construction | Boschini §3 accept-event decomposition |
|
||||
| `compute_mu_injective`, `pack_unpack_sk_roundtrip` | `Corona_N1.ec` | Construction | Corona transcript_hash binder; sk-codec |
|
||||
| `pack_unpack_n1_signature_roundtrip` | `Corona_N1.ec` | Construction | Corona signature codec round-trip |
|
||||
| `committee_quorum_uniq`, `committee_quorum_nonempty`, `fresh_sharing_size` | `Corona_N4.ec` | Definitional | Committee-quorum well-formedness |
|
||||
| `sig_len_pos`, `sig_len_within_cap`, `encode_signature_wf` | `Corona_N1_Signature_Codec.ec` | Codec | Producer-side byte-length invariant |
|
||||
| `q_pos`, `q_xi_pos`, `q_nu_pos`, `n_poly_pos`, `dbar_pos`, `kappa_pos` | `lemmas/RLWE_Functional.ec` | Concrete arithmetic | Closed via `decide` |
|
||||
| `l2_norm_sq_*_nonneg`, `inf_norm_R_nonneg` | `lemmas/RLWE_Functional.ec` | Definitional | Definition of norm |
|
||||
| `rlwe_sign_size`, `rlwe_correctness` | `lemmas/RLWE_Functional.ec` | Construction | Boschini ePrint 2024/1113 §3 correctness theorem |
|
||||
| `share_to_bits_id`, `msg_to_bits_id`, `ctx_to_bits_id`, `rnd_to_bits_id`, `bits_to_sig_id` | `lemmas/RLWE_Functional.ec` | Type identification | Pass-through codec |
|
||||
| `*_width_pos` (per-section widths) | `Corona_N1_Combine_Layout.ec`, `Corona_N1_Sign_Layout.ec` | Definitional | Non-negative widths |
|
||||
| `combine_body_spec`, `combine_body_writes_signature`, `layout_combine_frame` | `Corona_N1_Combine_Refinement.ec` | Byte-walk + frame | Jasmin-side via `combine.jazz` extraction |
|
||||
| `sign_body_spec`, `sign_body_writes_signature`, `layout_sign_frame` | `Corona_N1_Sign_Refinement.ec` | Byte-walk + frame | Jasmin-side via `rlwe/sign.jazz` extraction |
|
||||
| `share_encode_decode_roundtrip`, `combine_abs_op_lifted_bridge` | `Corona_N1_Combine_Wrapper.ec` | Codec bridge | Wire encoding |
|
||||
| `sign_abs_op_lifted_bridge`, `sign_abs_op_lifted_eq_rlwe` | `Corona_N1_Sign_Wrapper.ec` | RLWE conformance | Bridge to `rlwe_sign_op` |
|
||||
| `combine_body_axiom` (section-local `declare axiom`) | `Corona_N1.ec` § ClassN1 | Module contract | Discharged in `Corona_N1_Combine_Wrapper.wrapper_combine_refines_abs` |
|
||||
| `S_functional_spec` (section-local `declare axiom`) | `Corona_N1.ec` § ClassN1 | Module contract | Discharged in `Corona_N1_Sign_Wrapper.wrapper_sign_refines_central` |
|
||||
| `round1_commit_constant_time`, `round2_response_constant_time` (section-local) | `lemmas/Corona_CT.ec` | CT contract | Discharged Jasmin-side via `jasminc -checkCT` |
|
||||
| B1 | `group_pk_width_pos` | Corona_N1_Combine_Layout.ec:60 | `0 <= group_pk_width` (abstract `op group_pk_width : int`). |
|
||||
| B2 | `quorum_width_pos` | …:61 | `0 <= quorum_width`. |
|
||||
| B3 | `shares_r1_width_pos` | …:62 | `0 <= shares_r1_width`. |
|
||||
| B4 | `shares_r2_width_pos` | …:63 | `0 <= shares_r2_width`. |
|
||||
| B5 | `message_width_pos` (combine) | …:64 | `0 <= message_width`. |
|
||||
| B6 | `ctx_width_pos` (combine) | …:65 | `0 <= ctx_width`. |
|
||||
| B7 | `sk_share_width_pos` | Corona_N1_Sign_Layout.ec:37 | `0 <= sk_share_width`. |
|
||||
| B8 | `message_width_pos` (sign) | Corona_N1_Sign_Layout.ec:38 | `0 <= message_width` (sign-layout copy; distinct file/namespace). |
|
||||
| B9 | `ctx_width_pos` (sign) | Corona_N1_Sign_Layout.ec:39 | `0 <= ctx_width` (sign-layout copy). |
|
||||
| B10 | `sig_len_pos` | Corona_N1_Signature_Codec.ec:45 | `0 < sig_len` (abstract `op sig_len : int`). |
|
||||
| B11 | `sig_len_within_cap` | …:46 | `sig_len <= sig_len_max (=35000)`. |
|
||||
| B12 | `encode_signature_wf` | …:68 | Producer-side: `wf_signature_bytes (encode_signature x)`. |
|
||||
| B13 | `combine_body_writes_signature` | Corona_N1_Combine_Refinement.ec:79 | memory-separation: combine writes only the sig_out range. |
|
||||
| B14 | `layout_combine_frame` | …:116 | layout-stability: writes confined to sig_out preserve the input-buffer layout predicate. |
|
||||
| B15 | `layout_sign_frame` | Corona_N1_Sign_Refinement.ec:63 | sign-side layout-stability companion. |
|
||||
| B16 | `sign_body_writes_signature` | Corona_N1_Sign_Refinement.ec:54 | sign-side memory-separation. |
|
||||
| B17 | `share_encode_decode_roundtrip` | Corona_N1_Combine_Wrapper.ec:30 | `share_decode (share_encode s) = s` (abstract codec). |
|
||||
| B18 | `share_dim_correct` | Corona_N1.ec:137 | `|share_polys s| = share_dim`. |
|
||||
| B19 | `poly_share_roundtrip` | …:142 | poly-share codec round-trip. |
|
||||
| B20 | `share_polys_injective` | …:149 | `share_polys` injective. |
|
||||
| B21 | `poly_share_of_injective` | …:153 | `poly_share_of` injective. |
|
||||
| B22 | `poly_share_of_share_polys` | …:160 | round-trip pinning share↔poly-vector view. |
|
||||
| B23 | `reconstruct_polys_view` | …:218 | `reconstruct` agrees with its polynomial-vector view. |
|
||||
| B24 | `pack_unpack_n1_signature_roundtrip` | …:503 | unpack∘pack = id on (c,z,Δ). Pack-injectivity is DERIVED. |
|
||||
| B25 | `pack_unpack_sk_roundtrip` | …:560 | `pack_sk (unpack_sk sk) = sk`. |
|
||||
| B26 | `fresh_sharing_size` | Corona_N4.ec:157 | `|fresh_sharing q s| = |q|`. |
|
||||
| B27 | `committee_quorum_uniq` / `committee_quorum_nonempty` | Corona_N4.ec:179–180 | canonical quorum duplicate-free + non-empty (one row; two declarations). |
|
||||
|
||||
**Admit budget: 0/0** across all 13 EC files
|
||||
(`scripts/checks/ec-admits.sh` is the static guard).
|
||||
> Counting note: B27 bundles the two committee facts. Per *declaration*,
|
||||
> bucket B = 28; the histogram counts B27 as one logical row. Both readings
|
||||
> disclosed; no hidden axiom.
|
||||
|
||||
## §3 Implementation-level axioms (TCB)
|
||||
---
|
||||
|
||||
These are residual gaps between the verified construction and the
|
||||
shipped Go implementation. Each has a closure plan.
|
||||
### Bucket C — OPEN SECURITY ASSUMPTION (11) — **MUST STAY OPEN**
|
||||
|
||||
Corona's EC byte-equality (`corona_n1_byte_equality` /
|
||||
`corona_n1_byte_equality_extracted`) proves the threshold combine equals
|
||||
`CombineAbs.combine`, whose body (`wrapper_combine_refines_abs`, lines
|
||||
96–142 of Corona_N1_Combine_Wrapper.ec) reduces — via the bridge axioms
|
||||
below — to `rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd`: the
|
||||
**centralised R-LWE signer applied to the Lagrange-reconstructed master
|
||||
secret**. This is the **reconstruct-then-sign / CombineAbs reconstruct-then-
|
||||
sign abstraction**. The "steps 2–6" of the Boschini combine (the
|
||||
`CombineAbs.combine` open/aggregate/reject steps) are **opened**, not
|
||||
proved leak-free. The no-leak property of the production signer is
|
||||
**interop-tested (Go↔C++ KAT byte-equality; and the production R-LWE path's
|
||||
correctness is by code review against the paper), NOT EC-proven**.
|
||||
Tracked: `BLOCKERS.md` § "EC reconstruct-then-sign model".
|
||||
|
||||
| # | Axiom | File:line | What is assumed (open) |
|
||||
|---|---|---|---|
|
||||
| C1 | `combine_body_axiom` (declare axiom) | Corona_N1.ec:697 | `T.combine ~ CombineAbs.combine` on honest-quorum inputs — the extracted threshold combine equals the centralised RLWE sign of the reconstructed secret. The module-contract form of the whole combine refinement; closure pathway is the Jasmin byte-walk (production target v0.8.0). |
|
||||
| C2 | `S_functional_spec` (declare axiom) | Corona_N1.ec:712 | `S.sign ~ CentralRLWESign.sign` on accepted inputs — the single-party module is a faithful Boschini signer. |
|
||||
| C3 | `combine_body_spec` | Corona_N1_Combine_Refinement.ec:63 | the Jasmin-extracted combine writes exactly `combine_abs_op(args)` to sig_out. Atomic byte-walk; **steps 2–6 are inside this axiom, unproved.** |
|
||||
| C4 | `sign_body_spec` | Corona_N1_Sign_Refinement.ec:42 | the Jasmin-extracted central sign writes exactly `sign_abs_op(args)` to sig_out. Atomic byte-walk. |
|
||||
| C5 | `combine_abs_op_lifted_bridge` | Corona_N1_Combine_Wrapper.ec:47 | the share-typed lifted combine op = the byte-level `combine_abs_op` modulo encoding. The bridge from the abstract module interface to the byte-walk; the security content rides here. |
|
||||
| C6 | `sign_abs_op_lifted_bridge` | Corona_N1_Sign_Wrapper.ec:27 | the share-typed lifted sign op = the byte-level `sign_abs_op` modulo encoding. |
|
||||
| C7 | `sign_abs_op_lifted_eq_rlwe` | Corona_N1_Sign_Wrapper.ec:38 | **the reconstruct-then-sign identity in its starkest form**: `sign_abs_op_lifted sk … = rlwe_sign_op sk …` — the lifted op IS the centralised Boschini signer (the analog of libjade's role for Pulsar, but in-house since R-LWE has no FIPS target). This is the open Boschini-conformance claim. |
|
||||
| C8 | `rlwe_sign_size` | RLWE_Functional.ec:204 | per-instance signature byte length under Boschini's rejection-sampling. Carries the construction's wire-size contract; classified C because it is a construction-level claim from the paper, not a pure layout identity. |
|
||||
| C9 | `sign_round1_constant_time` (declare axiom) | lemmas/Corona_CT.ec:80 | Round-1 commit is constant-time. A CT *contract*, discharged Jasmin-side via `jasminc -checkCT` (roadmap), NOT by EC; a timing property, so a name/EC claim cannot certify it (see `proof-by-rename.sh` rationale). |
|
||||
| C10 | `sign_round2_constant_time` (declare axiom) | lemmas/Corona_CT.ec:110 | Round-2 response is constant-time. As C9. |
|
||||
|
||||
> C-cone bundling note: the histogram lists 11; the table enumerates 10
|
||||
> rows. The 11th C-declaration is `combine_body_axiom`'s and
|
||||
> `S_functional_spec`'s pair counted with the two CT contracts and the two
|
||||
> refinement byte-walks and the three wrapper bridges and `rlwe_sign_size`
|
||||
> = 11 declarations total (C1–C10 with C9/C10 being the two CT axioms). All
|
||||
> named; none hidden.
|
||||
|
||||
### Why the CT axioms (C9/C10) are C, not B
|
||||
|
||||
`sign_round{1,2}_constant_time` are `declare axiom` CT *contracts*. A
|
||||
constant-time property is a runtime/timing property that an EC axiom (or a
|
||||
name grep) cannot certify — it needs a dudect/ctgrind/jasmin-CT harness
|
||||
(`proof-by-rename.sh` exists to catch exactly the "name grep certifies
|
||||
timing" anti-pattern). Corona's dudect harness is wired (smoke-budget) and
|
||||
the submission-grade 10⁹-sample run is roadmap v0.8.0. So these axioms are
|
||||
**fail-closed-pending-review**, disclosed here as open.
|
||||
|
||||
## §3 Implementation-level axioms (TCB — residual Go ↔ construction gaps)
|
||||
|
||||
| Axiom | Location | Closure plan |
|
||||
|---|---|---|
|
||||
| `cloudflare/circl` lattice primitives correctness | indirect via `luxfi/lattice/v7` | Trust the library; upstream is community-audited. Not closing in Lux. |
|
||||
| `luxfi/lattice/v7` ring arithmetic correctness | `threshold/`, `sign/` | Cross-runtime byte-equality with C++ port at `luxcpp/crypto/corona/`; KAT manifest pins it. CI-enforced via `scripts/regen-kats.sh --verify`. |
|
||||
| Implementation matches Boschini construction at the protocol level | `dkg2/`, `threshold/`, `sign/`, `reshare/` | **v0.7.0**: EC scaffold lands (13 files, admit 0/0). Closure pathway from byte-walk axioms in `Corona_N1_{Combine,Sign}_Refinement.ec` requires the Jasmin extraction to fill out (production target at v0.8.0). |
|
||||
| Constant-time execution of the threshold layer | `threshold/`, `sign/` | **v0.7.0**: dudect harness lands at `ct/dudect/` (Verify + Combine). Smoke-budget runs are wired; the submission-grade 10^9-sample run on pinned hardware is the v0.8.0 audit target. |
|
||||
| Identifiable abort attribution under partition | `reshare/complaint.go`, `dkg2/complaint.go` | Lux profile adds typed complaint records; soundness reduces to identity-key signature unforgeability. Documented in `SPEC.md` and tested in `complaint_test.go`. EC formal proof remains roadmap v0.8.0. |
|
||||
| Cross-era key preservation via Reanchor | `reshare/activation.go`, `keyera/` | Lux profile adds activation cert circuit-breaker. Soundness inherited from R-LWE + KMAC collision resistance. `Corona_N4.ec` proves the public-key preservation property on the honest reshare module. |
|
||||
| `cloudflare/circl` / `luxfi/lattice/v7` primitive correctness | indirect | Trust upstream (community-audited); cross-runtime KAT byte-equality vs C++ port pins ring arithmetic (`scripts/regen-kats.sh --verify`). |
|
||||
| Implementation matches Boschini construction (protocol level) | `dkg2/`, `threshold/`, `sign/`, `reshare/` | EC scaffold lands (13 files, admit 0/0); the byte-walk axioms C3/C4 require the Jasmin extraction to fill out (v0.8.0). |
|
||||
| Constant-time execution of the threshold layer | `threshold/`, `sign/` | dudect harness at `ct/dudect/`; 10⁹-sample pinned-hardware run is v0.8.0. See C9/C10. |
|
||||
| Identifiable abort under partition | `reshare/complaint.go`, `dkg2/complaint.go` | typed complaint records; soundness reduces to identity-key signature unforgeability; EC proof roadmap v0.8.0. |
|
||||
| Cross-era key preservation (Reanchor) | `reshare/activation.go`, `keyera/` | activation-cert circuit-breaker; `Corona_N4.ec` proves public-key preservation on the honest reshare module. |
|
||||
|
||||
## §4 Comparison to Pulsar's AXIOM-INVENTORY
|
||||
## §4 Honest framing
|
||||
|
||||
Pulsar's `~/work/lux/pulsar/AXIOM-INVENTORY.md` enumerates the residual
|
||||
EC axioms after the v4-v13 decomposition cascade. Corona v0.7.0
|
||||
achieves the same structural shape:
|
||||
Corona's EC theories refine the Go implementation against an in-house
|
||||
mechanization of the Boschini construction. The byte-equality theorem is
|
||||
honest *as an idealised statement* — but it models **reconstruct-then-
|
||||
sign**: the EC `CombineAbs` reconstructs the master secret and signs with
|
||||
it. That is intentionally NOT how the production threshold path runs; the
|
||||
production path's leak-freedom is established by code review + cross-runtime
|
||||
KAT, not by this EC proof. Five algebraic axioms (A1–A5) are Lean-bridged.
|
||||
The byte-walk obligations (C3/C4), the wrapper bridges (C5–C7), and the CT
|
||||
contracts (C9/C10) are the open surface, tracked in `BLOCKERS.md` and gated
|
||||
on the v0.8.0 Jasmin-extraction + dudect + external-audit roadmap.
|
||||
|
||||
- 13 EC files (Pulsar parity)
|
||||
- Admit budget 0/0 (Pulsar parity)
|
||||
- 5 Lean-bridged algebraic axioms (Pulsar parity: `lagrange_inverse_eval`,
|
||||
`threshold_partial_response_identity`, `add_share_zeroR`,
|
||||
`reconstruct_linear`, `shamir_correct`)
|
||||
- Byte-walk + memory-separation + layout-frame axioms in the two
|
||||
Refinement files (Pulsar parity)
|
||||
- Wrapper-side discharge of section-local module-contract axioms
|
||||
(Pulsar parity)
|
||||
## §5 Comparison to Pulsar's AXIOM-INVENTORY
|
||||
|
||||
Corona is structurally easier than Pulsar in one respect: there is
|
||||
no FIPS 204 byte-equal claim, so no `accept_signing_attempt`
|
||||
kappa-rejection-sampling-loop reasoning. The Corona N1 analog is
|
||||
"implementation matches Boschini construction" which is a narrower
|
||||
refinement than Pulsar's FIPS 204 byte-equality.
|
||||
|
||||
## §5 Honest framing
|
||||
|
||||
This document is the **inventory** of axioms Corona's EC proofs
|
||||
depend on at v0.7.0. The EC files compile against these named axioms
|
||||
+ the Lean-bridged ones; the **admit budget is 0/0** across the 13-file
|
||||
set. Five algebraic axioms are bridged to Lean theorems with explicit
|
||||
inline citations (CI-enforced via `scripts/check-lean-bridge.sh`).
|
||||
|
||||
What remains operational:
|
||||
- Jasmin extraction filling out the byte-walk refinement (production
|
||||
target v0.8.0).
|
||||
- dudect submission-grade 10^9-sample runs on pinned hardware
|
||||
(production target v0.8.0).
|
||||
- External cryptographic audit engagement (production target v0.8.0).
|
||||
Pulsar (`~/work/lux/pulsar/AXIOM-INVENTORY.md`) has the same A/B/C structure
|
||||
over 78 axioms, with a far more decomposed refinement cone (per-stage
|
||||
byte-walk axioms reduced to derived lemmas across v4–v12). Corona's
|
||||
refinement is coarser: the whole combine is ONE `combine_body_spec` byte-
|
||||
walk (C3) plus the wrapper bridges, where Pulsar splits it into ~10 narrow
|
||||
per-stage sub-axioms. Both share the identical open core: the EC byte-
|
||||
equality models reconstruct-then-sign, and the production no-leak path is
|
||||
interop-tested, not EC-proven.
|
||||
|
||||
## §6 Cross-references
|
||||
|
||||
- `SUBMISSION.md` -- submission cover sheet
|
||||
- `PROOF-CLAIMS.md` -- narrow claim + explicit non-claims
|
||||
- `TRUSTED-COMPUTING-BASE.md` -- TCB inventory
|
||||
- `FIPS-TRACEABILITY.md` -- Boschini paper -> code traceability
|
||||
- `DEPLOYMENT-RUNBOOK.md` -- operator trust-model disclosure
|
||||
- `CRYPTOGRAPHER-SIGN-OFF.md` -- independent review verdict
|
||||
- `proofs/lean-easycrypt-bridge.md` -- Lean-bridged axiom correspondence
|
||||
- `proofs/easycrypt/Corona_N1_Extracted.ec` -- implementation-backed N1 theorem
|
||||
- `CHANGELOG.md` -- v0.7.0 roadmap closure
|
||||
`SUBMISSION.md`, `PROOF-CLAIMS.md`, `BLOCKERS.md`, `TRUSTED-COMPUTING-BASE.md`,
|
||||
`FIPS-TRACEABILITY.md`, `proofs/lean-easycrypt-bridge.md`,
|
||||
`proofs/easycrypt/Corona_N1_Extracted.ec`.
|
||||
|
||||
+93
@@ -0,0 +1,93 @@
|
||||
# Finding registry — luxfi/corona
|
||||
|
||||
**Status: OPEN items present (see `## Open`).** Corona's single-party /
|
||||
N4 reshare / code-review-against-Boschini claims are at the disclosed
|
||||
v0.7.0/v0.8.0-roadmap tier; the EasyCrypt byte-equality proof rests on an
|
||||
OPEN reconstruct-then-sign axiom cone, the constant-time evidence is a
|
||||
static audit (dudect-submission-grade pending), and there is no independent
|
||||
interop verifier for the R-LWE construction. None of these is hidden — they
|
||||
are the honest proof-tier of a published-construction implementation. See
|
||||
`PROOF-CLAIMS.md` §0 and `AXIOM-INVENTORY.md` §C.
|
||||
|
||||
This file is the finding registry. New findings open under `## Open`; on
|
||||
fix they move to `## Closed` with commit + tag.
|
||||
|
||||
## Open
|
||||
|
||||
### CORONA-EC-RECON-MODEL (HIGH — proof-scope disclosure)
|
||||
|
||||
**Status: OPEN. Disclosed, not closed.** The EasyCrypt Class N1
|
||||
byte-equality theorem (`corona_n1_byte_equality` /
|
||||
`corona_n1_byte_equality_extracted`) is machine-checked structurally
|
||||
(0 admits) but proved **relative to** the bucket-C asserted axioms in
|
||||
`AXIOM-INVENTORY.md` §C:
|
||||
|
||||
- `combine_body_spec` (the atomic Jasmin byte-walk) — the **Boschini
|
||||
combine steps 2–6 (open/aggregate/reject) are INSIDE this axiom,
|
||||
unproved.**
|
||||
- `combine_abs_op_lifted_bridge` + `sign_abs_op_lifted_eq_rlwe` — the
|
||||
wrapper bridges that pin the lifted combine/sign op to
|
||||
`rlwe_sign_op (reconstruct quorum shares) …`, i.e. the centralised
|
||||
R-LWE signer applied to the **Lagrange-reconstructed master secret**.
|
||||
- `combine_body_axiom` / `S_functional_spec` — the section-local module
|
||||
contracts of the same identity.
|
||||
|
||||
So the EC model **reconstructs the master key and signs with it**
|
||||
(reconstruct-then-sign). This is an idealised *correctness* statement; it
|
||||
is NOT a proof that the production threshold path is leak-free, and it is
|
||||
NOT how the production path is intended to run.
|
||||
|
||||
**Resolution criteria:**
|
||||
- [ ] Jasmin combine/sign byte-walk lands (production target v0.8.0) ⇒
|
||||
`combine_body_spec` / `sign_body_spec` and the layout-frame axioms
|
||||
become lemmas against the Jasmin operational semantics.
|
||||
- [ ] Wrapper bridges (`combine_abs_op_lifted_bridge`,
|
||||
`sign_abs_op_lifted_eq_rlwe`, `combine_abs_op_lifted_bridge`)
|
||||
discharge to lemmas, OR are replaced by a faithful (non-reconstruct)
|
||||
model of the Boschini steps 2–6.
|
||||
- [ ] `combine_body_axiom` / `S_functional_spec` discharge to lemmas via
|
||||
the wrapper instantiation against the extracted modules.
|
||||
- [ ] **External cryptographic review** (shared gate with
|
||||
CORONA-CT-PENDING and CORONA-NO-INDEP-VERIFIER below) signs off that
|
||||
the reconstruct-then-sign EC model is an acceptable correctness
|
||||
idealisation given the separate code-review + KAT evidence.
|
||||
|
||||
### CORONA-CT-PENDING (MEDIUM — constant-time evidence)
|
||||
|
||||
**Status: OPEN.** Constant-time evidence for the threshold + DKG paths is a
|
||||
per-path **static audit** (`CONSTANT-TIME-REVIEW.md`, zero must-fix
|
||||
findings) plus the upstream lattigo CT claims. The EC `declare axiom`s
|
||||
`sign_round1_constant_time` / `sign_round2_constant_time`
|
||||
(`lemmas/Corona_CT.ec`, bucket C9/C10) are CT **contracts**, NOT
|
||||
certificates — a timing property cannot be certified by an EC axiom or a
|
||||
name grep (`proof-by-rename.sh` exists to catch that anti-pattern). The
|
||||
dudect harness (`ct/dudect/`) is wired at smoke-budget.
|
||||
|
||||
**Resolution criteria:**
|
||||
- [ ] `jasminc -checkCT` discharges the CT contracts on the extracted
|
||||
threshold layer (production target v0.8.0).
|
||||
- [ ] dudect submission-grade 10⁹-sample run on pinned hardware.
|
||||
- [ ] External review of the CT posture (shared external-review gate).
|
||||
|
||||
### CORONA-NO-INDEP-VERIFIER (MEDIUM — interop disclosure)
|
||||
|
||||
**Status: OPEN by design (no NIST target for R-LWE).** Corona's signature
|
||||
byte-equality is cross-validated only **Go↔C++ of the SAME construction**
|
||||
(`luxcpp/crypto/corona` via `scripts/regen-kats.sh --verify`), NOT against
|
||||
an independent verifier. Unlike Pulsar (CIRCL + pq-crystals FIPS 204), the
|
||||
Boschini R-LWE construction has no second independent implementation to
|
||||
diff against. Therefore Corona's combine byte-equality is **asserted +
|
||||
same-construction-KAT-tested**, never "proven/verified" in the
|
||||
≥2-independent-implementations sense. `PROOF-CLAIMS.md` is worded to never
|
||||
claim otherwise.
|
||||
|
||||
**Resolution criteria:**
|
||||
- [ ] An independent R-LWE verifier (third-party or a from-the-paper
|
||||
re-implementation) is stood up and the KAT manifest diffs against it, OR
|
||||
- [ ] External review accepts the same-construction KAT + code-review
|
||||
posture as sufficient for the disclosed tier (shared external-review
|
||||
gate).
|
||||
|
||||
## Closed
|
||||
|
||||
(none yet)
|
||||
+56
-7
@@ -1,12 +1,46 @@
|
||||
# PROOF-CLAIMS — Corona (HONEST framing)
|
||||
# PROOF-CLAIMS — Corona (assurance-vocabulary, HONEST)
|
||||
|
||||
> **What this submission proves, and — critically — what it does NOT.**
|
||||
> Companion to `TRUSTED-COMPUTING-BASE.md` (TCB) and `SUBMISSION.md`
|
||||
> (cover sheet).
|
||||
> Every claim carries one assurance-vocabulary tag that MATCHES the
|
||||
> artifact's actual state. Companion to `AXIOM-INVENTORY.md` (bucketed
|
||||
> axiom census), `BLOCKERS.md` (open findings),
|
||||
> `TRUSTED-COMPUTING-BASE.md` (TCB), `SUBMISSION.md` (cover sheet).
|
||||
>
|
||||
> Read this before reading the Corona code. The framing matters as
|
||||
> much as the implementation.
|
||||
|
||||
## §0 Assurance vocabulary (canonical) + the two load-bearing disclosures
|
||||
|
||||
| Tag | Meaning |
|
||||
|---|---|
|
||||
| **machine-checked** | A proof assistant verifies it; the named file has ZERO `sorry`/`admit`/`:= True`. (No EasyCrypt toolchain on host; `scripts/checks/ec-compile.sh` is the CI gate, skipped when easycrypt is absent.) |
|
||||
| **sound-by-reduction** | Pen-and-paper reduction to a stated assumption; not mechanized. |
|
||||
| **interop-tested** | Validated against ≥2 INDEPENDENT implementations. |
|
||||
| **asserted-axiom** | Taken as an axiom in EC; bucketed in AXIOM-INVENTORY.md (A/B). |
|
||||
| **fail-closed-pending-review** | Implemented but gated to REFUSE until external review. |
|
||||
| **open-research** | Multi-month roadmap; not done. |
|
||||
|
||||
**Disclosure 1 — the EC byte-equality MODELS reconstruct-then-sign.**
|
||||
`corona_n1_byte_equality` / `corona_n1_byte_equality_extracted` prove the
|
||||
threshold combine equals `CombineAbs.combine`, whose body
|
||||
(`wrapper_combine_refines_abs`) reduces — via the bridge axioms
|
||||
`combine_abs_op_lifted_bridge` and `sign_abs_op_lifted_eq_rlwe` — to
|
||||
`rlwe_sign_op (reconstruct quorum shares) …`: the centralised R-LWE signer
|
||||
applied to the **Lagrange-reconstructed master secret**. The Boschini
|
||||
combine **steps 2–6** (open/aggregate/reject) are **opened inside
|
||||
`combine_body_spec`, not proved**. So the EC theorem is **machine-checked
|
||||
(0 admits) modulo a C-cone of asserted axioms that reconstruct-then-sign** —
|
||||
it is NOT a proof that the production threshold path is leak-free.
|
||||
|
||||
**Disclosure 2 — the no-leak property is NOT independently interop-tested.**
|
||||
Corona's KAT cross-validation is **Go↔C++ of the SAME construction**
|
||||
(`luxcpp/crypto/corona`), not against an independent verifier. There is no
|
||||
CIRCL/pq-crystals analog for R-LWE (no NIST target). So Corona's combine
|
||||
output byte-equality is **asserted + same-construction-KAT-tested**, NOT
|
||||
interop-tested in the ≥2-independent-implementations sense (unlike Pulsar's
|
||||
CIRCL + pq-crystals). We therefore do NOT claim Corona byte-equality is
|
||||
"proven/verified" anywhere in this document.
|
||||
|
||||
## §1 The narrow claim Corona makes at this submission
|
||||
|
||||
The strongest precise statement supported by Corona v0.4.1:
|
||||
@@ -51,7 +85,16 @@ submission. See §3 below for the explicit non-claims list.
|
||||
|
||||
This section is the load-bearing honesty disclosure. Read it.
|
||||
|
||||
### §3.1 v0.7.0: EC + Lean + Jasmin scaffolding LANDED (was: NOT proved)
|
||||
### §3.1 v0.7.0: EC + Lean + Jasmin scaffolding LANDED — but the EC byte-equality is reconstruct-then-sign (asserted-axiom cone)
|
||||
|
||||
**Assurance: machine-checked structure (0 admits) MODULO the C-cone of
|
||||
asserted axioms (reconstruct-then-sign).** The 13 EC theories are
|
||||
structurally complete, but `corona_n1_byte_equality` rests on the open
|
||||
bucket-C axioms in `AXIOM-INVENTORY.md` §C (the `combine_body_spec`
|
||||
byte-walk with Boschini steps 2–6 inside it, and the
|
||||
`combine_abs_op_lifted_bridge` / `sign_abs_op_lifted_eq_rlwe` wrapper
|
||||
bridges that pin the lifted op to `rlwe_sign_op` on the **reconstructed**
|
||||
secret). See §0 Disclosure 1.
|
||||
|
||||
**v0.7.0 update**: Corona now ships:
|
||||
- **13 EasyCrypt theories** compiling clean with admit budget **0/0**
|
||||
@@ -179,9 +222,15 @@ DESIGN.md invariants ("what is preserved across resharing")
|
||||
```
|
||||
|
||||
Each "implements" / "conforms" relation is by **inspection and
|
||||
test**, NOT machine-checked. Compare to Pulsar's refinement chain
|
||||
(machine-checked at every step via EasyCrypt 13/13 + Lean bridges
|
||||
5/5 + Jasmin-CT 3/3).
|
||||
test**, NOT machine-checked. Compare to Pulsar's refinement chain, which
|
||||
is machine-checked (0-admit) at the EC level **but only modulo the same
|
||||
reconstruct-then-sign asserted-axiom cone** — Pulsar's EC byte-equality is
|
||||
also relative to `combine_body_axiom` / `S_functional_spec` (its
|
||||
`AXIOM-INVENTORY.md` §C). The honest difference is degree of
|
||||
*decomposition* (Pulsar splits the byte-walk into ~10 narrow per-stage
|
||||
sub-axioms; Corona keeps one `combine_body_spec`) and *interop*: Pulsar's
|
||||
final signature is interop-tested vs CIRCL + pq-crystals, Corona's is
|
||||
same-construction Go↔C++ KAT only (§0 Disclosure 2).
|
||||
|
||||
## §5 What an auditor verifying this submission should do
|
||||
|
||||
|
||||
Reference in New Issue
Block a user