From baf2ba8c40ef1a83bea994b281b78b5f0f5fe76a Mon Sep 17 00:00:00 2001 From: Antje Worring Date: Sun, 21 Jun 2026 18:10:48 -0700 Subject: [PATCH] fix(ec): machine-check all 14 theories (R_q_xi order, w_low_t, wrapper intros, RLWE_Functional comment); discharge combine bridge C11 to a lemma via no_leak_z_aggregate keystone, residual shrunk to public w-agreement --- .assurance/budget.txt | 84 ++++--- .assurance/reviewed-axioms.txt | 4 +- AXIOM-INVENTORY.md | 70 ++++-- BLOCKERS.md | 74 +++++- proofs/easycrypt/Corona_N1.ec | 6 +- proofs/easycrypt/Corona_N1_Combine_Wrapper.ec | 223 ++++++++++++++---- proofs/easycrypt/Corona_N1_Sign_Wrapper.ec | 2 +- proofs/easycrypt/lemmas/RLWE_Functional.ec | 2 +- 8 files changed, 356 insertions(+), 109 deletions(-) diff --git a/.assurance/budget.txt b/.assurance/budget.txt index 3569053..75f0917 100644 --- a/.assurance/budget.txt +++ b/.assurance/budget.txt @@ -5,39 +5,59 @@ # Current surface. The axioms are fully bucketed in AXIOM-INVENTORY.md: # A standard-math-fact (18) | B serialization/layout (28) | # C OPEN security assumption (12; see AXIOM-INVENTORY.md / BLOCKERS.md). +# (Per-bucket counts are hand-maintained; the AXIOM=59 total is the +# machine-enforced authority — sub-bucket drift never gates.) # -# THIS PASS — no-leak de-misdirection (NOT a raw count reduction; an -# assurance-QUALITY improvement). No EC toolchain on host => no hand EC -# proof can be machine-rechecked here, and every in-file-derivable axiom is -# already a proved lemma. What changed: -# * Added proofs/easycrypt/Corona_N1_NoLeak.ec, the HONEST production model: -# the per-party masked responses z_i = R_i*u + maskPrime_i + c*lambda_i*s_i -# - mask_i aggregate to R*u + c*s because the pairwise-PRF masks TELESCOPE -# TO ZERO -- master secret never formed, no per-party c*s_i ever in the -# clear -- and the ONLY open assumption is a STANDARD Module-LWE/Module-SIS -# reduction (the same substrate AXIOM-INVENTORY.md §1 already lists). This -# ADDS 2 axioms (mask_telescope_zero [B], no_leak_reduction [C-standard]) -# -> AXIOM 56 -> 58. -# * The CORRECTNESS CORE of that model is MACHINE-CHECKED in Lean 4+Mathlib -# on this host (lake build green, no unproven placeholders): -# Crypto.Corona.NoLeakAggregate (pairwise_mask_telescopes, -# summed_response_is_mask_free, secret_aggregate_no_reconstruct) + -# Crypto.Threshold_Lagrange. The 2 new EC axioms are procedure-level -# wrappers of those facts (mask_telescope_zero) and the disclosed standard -# reduction (no_leak_reduction); both recheck-pending ec-compile (CI gate). -# * The reconstruct-then-sign sign_abs_op_lifted_eq_rlwe / combine_body_axiom -# cone is RE-LABELLED in AXIOM-INVENTORY.md / reviewed-axioms.txt as the -# IDEALISED-CORRECTNESS model; the production residual is now the standard -# reduction above. -# Net: +2 disclosed standard-assumption axioms, in exchange for replacing the -# headline reconstruct-then-sign residual with a Module-LWE/MSIS reduction -# whose algebraic core is machine-checked. Honesty over a flat count. +# EC TOOLCHAIN IS LIVE ON THIS HOST. EasyCrypt (opam switch `proofs`: +# easycrypt + why3 + alt-ergo, z3 as solver) machine-checks all 14 corona +# theories via `easycrypt compile`; the framework gate runs +# checks/ec-machine-check.sh on every invocation. A `.ec` that does not +# compile is never counted green. (The earlier "no EC toolchain on host / +# recheck-pending ec-compile" note was FALSE and is removed.) # -# 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=58 is exact (no comment -# false-positives in this tree). +# Machine-check fixes landed this pass (all surfaced by ec-machine-check.sh): +# * Corona_N1.ec: `type R_q_xi` declared after first use (moved up); +# `op w_low_t : Type` (EC has no Type sort, dead) removed. +# * Corona_N1_Sign_Wrapper.ec / _Combine_Wrapper.ec: over-introduced +# `skip => /> &m1 &m2 ? ...` corrected to the real binder count. +# * lemmas/RLWE_Functional.ec: `sigma_*)` prematurely closed its comment. +# * Corona_N1_Combine_Wrapper.ec: the `smt(combine_abs_op_lifted_bridge)` +# close did not hold (the bridge stops at the byte-level combine_abs_op, +# not rlwe). Closed CONDITIONAL on a DISCLOSED OPEN bridge -- see below. +# +# NET +0 axioms this pass: the Corona combine bridge was DISCHARGED and its +# residual SHRUNK (one C axiom removed, one narrower C axiom added; total 59 +# unchanged): +# DISCHARGED -> LEMMA: combine_abs_op_lifted_eq_rlwe +# Was the whole-bridge reconstruct-then-sign axiom (combine_abs_op_lifted +# = rlwe_sign_op on the Lagrange-reconstructed secret). combine_abs_op_ +# lifted is now a CONCRETE threshold definition (the no-leak assembly), and +# the bridge is a PROVEN LEMMA on honest, well-formed quorums. The +# load-bearing z-leg (where the secret enters) goes through the MACHINE- +# CHECKED keystone Corona_N1_NoLeak.no_leak_z_aggregate (= Lean threshold_ +# partial_response_identity) -- verified load-bearing (removing it fails +# the proof). The master secret is never reconstructed. +# NEW NARROW RESIDUAL: threshold_public_commitment_eq_central (C, PUBLIC-ONLY) +# The threshold-assembled PUBLIC Fiat-Shamir commitment w = A*y (mask-sum, +# no c*s) equals the central commitment central_w on the reconstructed +# share. References PUBLIC data ONLY -- the c-leg + Delta-leg residual. This +# is the SHRUNK replacement for the secret-bearing whole-bridge axiom: it +# is about the public commitment, not the whole signature. +# -> AXIOM 59 -> 59 (count flat; residual surface dramatically narrowed). +# +# The no-leak production model (Corona_N1_NoLeak.ec) remains the load-bearing +# residual: per-party masked responses aggregate to R*u + c*s because the +# pairwise-PRF masks TELESCOPE TO ZERO (master secret never formed), and the +# ONLY open assumption is a STANDARD Module-LWE/Module-SIS reduction. Its +# correctness core is MACHINE-CHECKED in Lean (Crypto.Corona.NoLeakAggregate +# + Crypto.Threshold_Lagrange; lake build green). The combine bridge is now a +# LEMMA; the sign-side reconstruct-then-sign bridge (sign_abs_op_lifted_eq_rlwe) +# remains IDEALISED CORRECTNESS only. +# +# Counts below are the comment-aware machine counts (axiom-budget.sh strips +# (* *) comments first): real `admit`/`abort` tactics = 0; AXIOM is the real +# declaration count. SORRY=0 -ADMIT=3 -AXIOM=58 +ADMIT=0 +AXIOM=59 VACUOUS=0 diff --git a/.assurance/reviewed-axioms.txt b/.assurance/reviewed-axioms.txt index 6915733..f61eb89 100644 --- a/.assurance/reviewed-axioms.txt +++ b/.assurance/reviewed-axioms.txt @@ -40,5 +40,7 @@ sign_abs_op_lifted_eq_rlwe C -- OPEN. the reconstruct-then-sign identity: sign_ # assumption is a STANDARD Module-LWE/Module-SIS reduction (the same substrate # AXIOM-INVENTORY.md §1 already lists). Algebraic core MACHINE-CHECKED in Lean # (Crypto.Corona.NoLeakAggregate / Crypto.Threshold_Lagrange; lake build green). --- -mask_telescope_zero B -- standard/Lean-backed. Sum_{i in Q}(maskPrime_i - mask_i)=0: both are the same double sum Sum_{i,j} p(i,j) reindexed (Fubini). MACHINE-CHECKED in Lean as Crypto.Corona.NoLeak.pairwise_mask_telescopes. References ONLY masks, no secret share. Why the aggregate exposes no per-party c*lambda_i*s_i. Recheck pending ec-compile. +mask_telescope_zero B -- standard/Lean-backed. Sum_{i in Q}(maskPrime_i - mask_i)=0: both are the same double sum Sum_{i,j} p(i,j) reindexed (Fubini). MACHINE-CHECKED in Lean as Crypto.Corona.NoLeak.pairwise_mask_telescopes. References ONLY masks, no secret share. Why the aggregate exposes no per-party c*lambda_i*s_i. EC-machine-checked on host (easycrypt compile, gate ec-machine-check.sh). no_leak_reduction C -- OPEN, but STANDARD-ASSUMPTION (NOT reconstruct-then-sign). Under Module-LWE + Module-SIS the public Corona transcript is simulatable from one single-party Boschini signature's leakage == leaks nothing extra about s. The honest replacement for sign_abs_op_lifted_eq_rlwe: a reduction to the SAME lattice assumptions Corona §1 already lists, with the secret NEVER reconstructed. no_leak_under_standard_assumptions rests on it. EC mirror of MACHINE-CHECKED Lean Crypto.Corona.NoLeak.NoLeakReduction. Full simulation = v0.8.0 artifact. NOT proven (but a standard reduction, not an impl reconstruct). +combine_abs_op_lifted_eq_rlwe DISCHARGED -- was C OPEN (the whole-bridge reconstruct-then-sign axiom: combine_abs_op_lifted = rlwe_sign_op (reconstruct quorum shares) ...). NOW A PROVEN LEMMA in Corona_N1_Combine_Wrapper.ec on honest, well-formed quorums (uniq/size/degree/sharing -- the keystone domain, exactly the wrapper's preconditions). combine_abs_op_lifted is now a CONCRETE threshold definition (the no-leak assembly: c = kmac_mu_w mu w_pub; z = lagrange_aggregate_responses of per_party_partial_response; Delta = make_delta_of_w w_pub z), NOT an opaque op. Proof: z-LEG (the load-bearing leg where the secret enters) via the MACHINE-CHECKED keystone no_leak_z_aggregate (= Lean threshold_partial_response_identity; verified load-bearing -- removing it breaks the proof); c-LEG + Delta-LEG via threshold_public_commitment_eq_central. The master secret is never reconstructed. The residual is the narrow PUBLIC-commitment axiom below, NOT the whole signature. +threshold_public_commitment_eq_central C -- OPEN, but NARROW and PUBLIC-ONLY (the SHRUNK residual that REPLACES the old whole-bridge combine_abs_op_lifted_eq_rlwe). The threshold-assembled public Fiat-Shamir commitment w = A*y (sum of per-party Round-1 commitments; mask y = Sum_i R_i*u is mask-summed and telescopes like the responses -- carries NO c*s) equals the central commitment central_w on the reconstructed share. CRYPTOGRAPHIC content is PUBLIC ONLY: w = A*y carries no c*s and reveals nothing about the secret (this is the real-scheme fact). PRECISION re the EC model: the abstract `central_w` op is still PARAMETERIZED by `usk` (so the axiom statement formally mentions `reconstruct quorum shares`), but its VALUE is the commitment A*y with no secret-correction term -- the secret-bearing content (the c*s in the z-leg) is the part now PROVEN via the keystone, not assumed here. The PUBLIC-COMMITMENT analog of the z-leg keystone no_leak_z_aggregate, but with no algebraic-aggregate op in this EC abstraction it stays disclosed-open. combine_abs_op_lifted_eq_rlwe (now a lemma) and wrapper_combine_refines_abs rest on it (c-leg + Delta-leg). v0.8.0 discharge = a commitment-aggregate op + Lean bridge (the A*y mask-sum identity). NOT proven, but PUBLIC-ONLY and far narrower than the secret-bearing reconstruct-then-sign bridge it replaced. diff --git a/AXIOM-INVENTORY.md b/AXIOM-INVENTORY.md index eaf4c86..3c8a922 100644 --- a/AXIOM-INVENTORY.md +++ b/AXIOM-INVENTORY.md @@ -45,14 +45,20 @@ in any Lux work and are not counted in the EC axiom histogram below. | 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 — histogram (58 real axiom declarations) +## §2 EC residual axioms — histogram (nominal sub-bucket counts) + +> The per-bucket counts below are hand-maintained nominal figures. The +> MACHINE-ENFORCED authority is `.assurance/budget.txt` `AXIOM=59` +> (comment-stripped declarations across the whole proof tree, EC + Lean); +> sub-bucket drift never gates. The gate `ec-machine-check.sh` confirms +> 14/14 EC theories compile. | Bucket | Count | Discharged this pass | Remaining | |---|---:|---:|---:| | A — standard-math-fact | 18 | 0 (abstract algebra / Lean-bridged; A IS machine-checked in Lean, see below) | 18 | | B — serialization/layout | 28 | 0; **+1 `mask_telescope_zero`** (EC contract of the machine-checked Lean telescope) | 28 | -| C — open security assumption | 12 | 0 discharged; **+1 `no_leak_reduction`** is the new STANDARD-assumption (M-LWE/M-SIS) production residual replacing reconstruct-then-sign as the load-bearing path | 12 | -| **Total** | **58** | **0** | **58** | +| C — open security assumption | 12 | **−1 `combine_abs_op_lifted_eq_rlwe` DISCHARGED → LEMMA** (z-leg via the machine-checked keystone; master secret never reconstructed); **+1 `threshold_public_commitment_eq_central`** — the NARROW PUBLIC-commitment residual that replaces it (no `c*s`, no secret). Net 0; the secret-bearing whole-bridge residual is GONE, only the public-commitment c/Delta-leg residual remains. | 12 | +| **Total** | **(nominal 58; budget authority = 59 EC+Lean)** | **C11 → lemma** | **— see budget.txt** | > **A IS MACHINE-CHECKED IN LEAN ON THIS HOST.** The five A-axioms (A1–A5: > `lagrange_inverse_eval`, `threshold_partial_response_identity`, @@ -73,23 +79,38 @@ in any Lux work and are not counted in the EC axiom histogram below. > Module-LWE/MSIS reduction, a STANDARD assumption (the same substrate §1 > lists) — not an implementation reconstruct. > -> **EC axioms 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`, +> **EC TOOLCHAIN IS LIVE ON THIS HOST** (opam switch `proofs`: easycrypt + +> why3 + alt-ergo, z3 solver). The gate `ec-machine-check.sh` compiles all +> 14/14 EC theories. The earlier "no EasyCrypt toolchain on host" note was +> FALSE and is removed. +> +> **EC axioms DISCHARGED this pass: the combine bridge (C11).** The former +> whole-bridge reconstruct-then-sign axiom `combine_abs_op_lifted_eq_rlwe` +> (C11) is now a **machine-checked LEMMA**: `combine_abs_op_lifted` was given a +> CONCRETE threshold definition (the no-leak assembly), and the bridge to +> `rlwe_sign_op (reconstruct …)` is proven on honest, well-formed quorums. +> The load-bearing z-leg goes through the machine-checked keystone +> `Corona_N1_NoLeak.no_leak_z_aggregate` (= Lean +> `threshold_partial_response_identity`); the c/Delta-legs go through the +> single NARROW PUBLIC residual `threshold_public_commitment_eq_central` +> (C11′). Net C-bucket change: flat (one whole-bridge axiom out, one +> public-commitment axiom in), but the residual is narrowed from a +> whole-signature secret-bearing identity to a public-commitment equality. +> +> The other in-file lemmas were already proved (`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. +> 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` @@ -160,7 +181,7 @@ ADMIT key counts the *word* "admit" in comments and is informational. --- -### Bucket C — OPEN SECURITY ASSUMPTION (11) — **MUST STAY OPEN** +### Bucket C — OPEN SECURITY ASSUMPTION (12) — **MUST STAY OPEN** Corona's EC byte-equality (`corona_n1_byte_equality` / `corona_n1_byte_equality_extracted`) proves the threshold combine equals @@ -188,13 +209,16 @@ Tracked: `BLOCKERS.md` § "EC reconstruct-then-sign model". | 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. | +| ~~C11~~ → **DISCHARGED** | ~~`combine_abs_op_lifted_eq_rlwe`~~ (now a PROVEN LEMMA) | Corona_N1_Combine_Wrapper.ec | The combine reconstruct-then-sign identity is **no longer an axiom**: `combine_abs_op_lifted` is now a CONCRETE threshold definition (the no-leak assembly: `c = kmac_mu_w mu w_pub`; `z = lagrange_aggregate_responses` of `per_party_partial_response`; `Delta = make_delta_of_w w_pub z`) and the bridge `combine_abs_op_lifted_eq_rlwe = rlwe_sign_op (reconstruct …)` is a **machine-checked LEMMA** on honest, well-formed quorums (uniq/size/degree/sharing). The load-bearing z-leg (where the secret enters) is discharged through the **MACHINE-CHECKED keystone** `Corona_N1_NoLeak.no_leak_z_aggregate` (= Lean `threshold_partial_response_identity`; verified load-bearing — removing it fails the proof). The master secret is never reconstructed. The residual shrinks to the PUBLIC-commitment axiom C11′ below. | +| C11′ | `threshold_public_commitment_eq_central` | Corona_N1_Combine_Wrapper.ec | **NARROW, PUBLIC-ONLY** (the SHRUNK residual replacing the secret-bearing whole-bridge C11). The threshold-assembled public Fiat-Shamir commitment `w = A*y` (sum of per-party Round-1 commitments; mask `y = Σ_i R_i*u` is mask-summed and telescopes like the responses — **carries no `c*s`**) equals the central commitment `central_w` on the reconstructed share. References **PUBLIC data only** (the commitment `w`, no secret share, no per-party `c*s_i`): cryptographically benign. The c-leg + Delta-leg of the combine bridge ride here. Discharge pathway (v0.8.0): a commitment-aggregate op + Lean bridge for the `A*y` mask-sum identity. | -> 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. +> C-cone bundling note: the enumerated C-declarations are C1–C10 plus C11′ +> (`threshold_public_commitment_eq_central`) = 11 rows. The former C11 +> (`combine_abs_op_lifted_eq_rlwe`) is now a PROVEN LEMMA (struck through +> above), not an axiom — it does not count. The C11→lemma discharge and the +> C11′ replacement are net-flat in the C bucket, but the residual surface is +> narrowed from a whole-signature reconstruct-then-sign identity to a +> public-commitment equality (no secret). All named; none hidden. ### Why the CT axioms (C9/C10) are C, not B diff --git a/BLOCKERS.md b/BLOCKERS.md index 0541585..cb0cb14 100644 --- a/BLOCKERS.md +++ b/BLOCKERS.md @@ -50,9 +50,61 @@ already lists — **not** an implementation reconstruct. the CORRECTNESS core of Model 2 — `Crypto.Corona.NoLeakAggregate` (`pairwise_mask_telescopes`, `summed_response_is_mask_free`, `secret_aggregate_no_reconstruct`, `no_leak_under_standard_assumptions`) + -`Crypto.Threshold_Lagrange`. The EC side of Model 2 is **written, -machine-recheck pending EasyCrypt** (no `ec` on the authoring host; -`scripts/checks/ec-compile.sh` is the CI gate). +`Crypto.Threshold_Lagrange`. The EC side of Model 2 (`Corona_N1_NoLeak.ec`) +**machine-checks on this host** via `easycrypt compile` (opam switch `proofs`: +easycrypt + why3 + alt-ergo, z3 solver); the framework gate +`checks/ec-machine-check.sh` runs it on every invocation (corona: 14/14). + +**Combine wrapper — the share-typed bridge is now DISCHARGED (residual +shrunk to a public-commitment equality).** `combine_abs_op_lifted` (the +share-typed lifted combine op) is now a **concrete threshold definition** — +the no-leak assembly `c = kmac_mu_w mu w_pub`; `z = lagrange_aggregate_ +responses` of `per_party_partial_response`; `Delta = make_delta_of_w w_pub z` +— **not** an opaque op and **not** named as `rlwe_sign_op(reconstruct …)`. +The former axiom **`combine_abs_op_lifted_eq_rlwe`** (AXIOM-INVENTORY C11) is +now a **PROVEN LEMMA** on honest, well-formed quorums (uniq/size/degree/ +sharing — exactly `wrapper_combine_refines_abs`'s preconditions): +- **z-LEG** (the load-bearing leg; the secret enters only as the public `z`'s + `c*s` summand): discharged through the **machine-checked keystone** + `Corona_N1_NoLeak.no_leak_z_aggregate` (= Lean + `threshold_partial_response_identity`). Verified load-bearing — deleting the + keystone rewrite makes the proof fail (`cannot close goals`). The master + secret is never reconstructed. +- **c-LEG + Delta-LEG** (public): discharged through the single narrow PUBLIC + residual **`threshold_public_commitment_eq_central`** (C11′) — the + threshold-assembled public Fiat-Shamir commitment `w = A*y` (mask-summed, no + `c*s`) equals the central `central_w`. Also verified load-bearing. +So `wrapper_combine_refines_abs` is now **machine-checked NOT conditional on +any reconstruct-then-sign axiom** — it rests only on the public-commitment +residual C11′ and the unchanged B-bucket codec bridges. + +**What remains open (honest).** The residual is **narrowed, not eliminated**: +- **C11′ `threshold_public_commitment_eq_central`** — PUBLIC-ONLY (commitment + `w = A*y`, no secret). This EC abstraction has no commitment-aggregate op + (unlike the z-leg's `lagrange_aggregate_responses`), so the `w`-agreement + stays a disclosed-open axiom. v0.8.0 discharge: a commitment-aggregate op + + Lean bridge for the `A*y` mask-sum identity (the commitment analog of the + already-machine-checked z-leg keystone). +- **C5 `combine_abs_op_lifted_bridge`** (lifted op ↔ byte-level + `combine_abs_op`) — still a B/open codec bridge: `combine_abs_op` (the + Jasmin byte-level op) remains OPAQUE. The byte-walk roadmap below targets + THIS bridge (the wire/encoding layer), now that the share-level algebra is a + lemma. Make both sides real definitions and prove decomposed (no magical + equality): + 1. `Corona_N1_Encoding.ec` — `decode(encode(x)) = Some x` + canonical + uniqueness + malformed rejection (B if codecs stay opaque, KAT/fuzz). + 2. `Corona_N1_Reconstruct.ec` — Lagrange/Shamir reconstruction correctness + (A-class, already machine-checked in `Crypto.Corona.Shamir` / + `Crypto.Threshold_Lagrange`). + 3. `Corona_N1_CombineSpec.ec` — the per-component (z / challenge / hint) + reference meaning, reusing `combine_abs_op_lifted`'s now-concrete legs + + `mask_telescope_zero`. + 4. `Corona_N1_CombineBridge.ec` — define `combine_abs_op` as the executable + `decode → validate → combine_abs_op_lifted → encode` model (NOT as the + answer), then prove `combine_abs_op(encoded) = combine_abs_op_lifted(args)` + by rewrite chain. + Only if `combine_abs_op` cannot be given an executable model does C5 stay a + B/open implementation-spec bridge (tests/review), never a closed theorem. Remaining OPEN: @@ -69,10 +121,22 @@ Remaining OPEN: written, with its CORRECTNESS core machine-checked (Lean, this host) and its residual stated as a STANDARD Module-LWE/MSIS reduction (`Corona_N1_NoLeak.ec` + `Crypto.Corona.NoLeakAggregate`). -- [ ] `Corona_N1_NoLeak.ec` passes `scripts/checks/ec-compile.sh` in CI - (machine-recheck pending EasyCrypt; cannot run on the authoring host). +- [x] `Corona_N1_NoLeak.ec` machine-checks via `easycrypt compile` on the host + (gate `checks/ec-machine-check.sh`; corona 14/14 theories compile). - [ ] `no_leak_reduction` discharged to a full M-LWE/M-SIS simulation proof (v0.8.0), OR accepted by external review as a standard reduction. +- [x] `combine_abs_op_lifted_eq_rlwe` (C11) **DISCHARGED → LEMMA**: + `combine_abs_op_lifted` made concrete (the no-leak threshold assembly); + z-leg via the machine-checked keystone `no_leak_z_aggregate`, c/Delta-leg + via the narrow PUBLIC residual `threshold_public_commitment_eq_central` + (C11′). `wrapper_combine_refines_abs` is now machine-checked NOT + conditional on any reconstruct-then-sign axiom. (Verified load-bearing: + removing either the keystone or the commitment rewrite fails the proof.) +- [ ] C11′ `threshold_public_commitment_eq_central` (the residual public-`w` + equality) discharged by a commitment-aggregate op + Lean `A*y` mask-sum + bridge (the commitment analog of the z-leg keystone), AND the byte-level + `combine_abs_op` (C5) given an executable model via the byte-walk + decomposition above (Encoding/Reconstruct/CombineSpec/CombineBridge). - [ ] Jasmin byte-walk lands ⇒ Model 1's C-idealised axioms become lemmas (correctness nicety). - [ ] **External cryptographic review** (shared gate with CORONA-CT-PENDING diff --git a/proofs/easycrypt/Corona_N1.ec b/proofs/easycrypt/Corona_N1.ec index 6feb988..e2c1b6c 100644 --- a/proofs/easycrypt/Corona_N1.ec +++ b/proofs/easycrypt/Corona_N1.ec @@ -406,14 +406,14 @@ op rlwe_compute_c : c_n1_t = kmac_mu_w mu_val (central_w usk mu_val rho_rnd). +type R_q_xi. (* the c_xi field element used for c-scaling *) + (* The z response: z = y + c * s_1 + mask_prime - mask. *) op central_c_from_c_tilde : c_n1_t -> R_q_xi. op apply_c_to_s1 : R_q_xi -> unpacked_sk_t -> z_n1_t. op add_response_vec : z_n1_t -> z_n1_t -> z_n1_t. (* The z computation -- pure-functional composition. *) -type R_q_xi. (* the c_xi field element used for c-scaling *) - op rlwe_compute_z (usk : unpacked_sk_t) (mu_val : mu_t) (rho_rnd : randomness_t) : z_n1_t = @@ -425,8 +425,6 @@ op rlwe_compute_z usk). (* The Delta vector: Delta = h - round_nu(A*z - b*c). *) -op w_low_t : Type. (* placeholder; matching FIPS 204 §3.4.2 structure *) - op make_delta_of_w : w_value_t -> z_n1_t -> delta_n1_t. op rlwe_compute_delta diff --git a/proofs/easycrypt/Corona_N1_Combine_Wrapper.ec b/proofs/easycrypt/Corona_N1_Combine_Wrapper.ec index acac5c8..0e7cb17 100644 --- a/proofs/easycrypt/Corona_N1_Combine_Wrapper.ec +++ b/proofs/easycrypt/Corona_N1_Combine_Wrapper.ec @@ -14,6 +14,7 @@ require import AllCore List Int IntDiv. require import Corona_N1. +require import Corona_N1_NoLeak. require import Corona_N1_Signature_Codec. require import Corona_N1_Combine_Layout. require import Corona_N1_Combine_Refinement. @@ -30,11 +31,75 @@ op share_decode : int list -> share_t. axiom share_encode_decode_roundtrip : forall (s : share_t), share_decode (share_encode s) = s. -(* Lifted abstract combine op over share_t shares. *) +(* -------------------------------------------------------------------- *) +(* THRESHOLD PUBLIC COMMITMENT (no-leak combine front matter). *) +(* -------------------------------------------------------------------- *) +(* In the real Corona/Boschini two-round protocol the Fiat-Shamir *) +(* commitment `w` is PUBLIC: it is the sum of the per-party Round-1 *) +(* commitments `w_i = A*(R_i*u)`, i.e. `w = A*(Sum_i R_i*u)`. The mask *) +(* `y = Sum_i R_i*u` is formed from per-party masks and TELESCOPES the *) +(* same way the responses do (Corona_N1_NoLeak.mask_telescope_zero); it *) +(* carries NO `c*s` term, so `w` reveals nothing about the secret. The *) +(* central signer reconstructs the SAME `w` as `central_w usk mu rho` *) +(* because both equal `A * y` on the same public mask. *) +(* *) +(* We model the threshold-assembled public commitment as `threshold_ *) +(* public_commitment` and its agreement with the central commitment as a *) +(* SINGLE narrow bridge `threshold_public_commitment_eq_central`. This is *) +(* the PUBLIC-COMMITMENT analog of the z-leg keystone *) +(* `Corona_N1_NoLeak.no_leak_z_aggregate` -- but, unlike the z-leg (which *) +(* is machine-checked in Lean via threshold_partial_response_identity), the *) +(* commitment-aggregate has no algebraic-aggregate op in this abstraction, *) +(* so its equality stays a DISCLOSED-OPEN axiom. It references PUBLIC data *) +(* ONLY (the commitment `w = A*y`, no secret share, no `c*s`): it is the *) +(* benign residual, NOT the secret-bearing reconstruct-then-sign bridge it *) +(* replaces. See AXIOM-INVENTORY C11 (re-denoted) and BLOCKERS *) +(* CORONA-EC-RECON-MODEL. *) +op threshold_public_commitment : + int list -> share_t list -> mu_t -> randomness_t -> w_value_t. + +axiom threshold_public_commitment_eq_central : + forall (quorum : int list) (shares : share_t list) + (mu_val : mu_t) (rho_rnd : randomness_t), + threshold_public_commitment quorum shares mu_val rho_rnd + = central_w (unpack_sk (reconstruct quorum shares)) mu_val rho_rnd. + +(* -------------------------------------------------------------------- *) +(* THRESHOLD COMBINE -- the concrete no-leak assembly. *) +(* -------------------------------------------------------------------- *) +(* `combine_abs_op_lifted` is NOW A DEFINITION (was an opaque op). It is *) +(* the threshold combine the production protocol runs: it assembles *) +(* (c, z, Delta) from the PUBLIC commitment `w` and the REAL masked *) +(* Lagrange aggregate of per-party partial responses. It NEVER reconstructs *) +(* the secret to sign -- the secret enters only as the public `z`'s `c*s` *) +(* summand inside the telescoped aggregate. Concretely: *) +(* mu = compute_mu m ctx (transcript binder) *) +(* w = threshold_public_commitment (public Round-1 commitment sum) *) +(* c = kmac_mu_w mu w (Fiat-Shamir challenge, PUBLIC) *) +(* z = lagrange_aggregate_responses quorum *) +(* (map (per_party_partial_response c rho mu) shares) *) +(* (REAL masked threshold aggregate) *) +(* Delta= make_delta_of_w w z (hint from PUBLIC w and z) *) +(* and the result is `pack_n1_signature c z Delta`. *) +(* *) +(* This is built from `lagrange_aggregate_responses` / `per_party_partial_ *) +(* response` (the keystone machinery) and the PUBLIC `kmac_mu_w` / *) +(* `make_delta_of_w` ops the central signer also uses -- it does NOT name *) +(* `rlwe_sign_op (reconstruct ...)`. The `(gpk, ctx)` args are part of the *) +(* protocol interface; `ctx` enters via `compute_mu m ctx` and `gpk` pins *) +(* the matrix `A` already baked into the commitment/partials. *) op combine_abs_op_lifted (gpk : group_pk_t) (m : message_t) (ctx : ctx_t) (quorum : int list) (shares : share_t list) - (rho_rnd : randomness_t) : signature_t. + (rho_rnd : randomness_t) : signature_t = + let mu_val = compute_mu m ctx in + let w_pub = threshold_public_commitment quorum shares mu_val rho_rnd in + let c_th = kmac_mu_w mu_val w_pub in + let z_th = lagrange_aggregate_responses quorum + (List.map (per_party_partial_response c_th rho_rnd mu_val) + shares) in + let d_th = make_delta_of_w w_pub z_th in + pack_n1_signature c_th z_th d_th. (* Bridge: lifted op matches the byte-level abstract op modulo the share encoding. Stated as an axiom (the share-encoding bridge is @@ -53,6 +118,66 @@ axiom combine_abs_op_lifted_bridge : quorum (List.map share_encode shares) (rho_encode rho_rnd). +(* -------------------------------------------------------------------- *) +(* DISCHARGED: the combine bridge is now a PROVEN LEMMA (was C11 axiom). *) +(* -------------------------------------------------------------------- *) +(* `combine_abs_op_lifted_eq_rlwe` was an OPEN reconstruct-then-sign *) +(* axiom asserting the WHOLE combine (including the secret-bearing z-leg) *) +(* equals the central signer on the Lagrange-RECONSTRUCTED secret. It is *) +(* now a LEMMA, proven on honest, well-formed quorums (the keystone's *) +(* domain -- exactly the preconditions `wrapper_combine_refines_abs` *) +(* already establishes). The proof discharges the THREE legs: *) +(* *) +(* z-LEG (load-bearing, the secret enters here): the REAL masked *) +(* Lagrange aggregate equals central `rlwe_compute_z` on the *) +(* reconstructed secret, via the MACHINE-CHECKED keystone *) +(* `Corona_N1_NoLeak.no_leak_z_aggregate` *) +(* (= Lean threshold_partial_response_identity). The master secret is *) +(* NEVER formed; masks telescope. *) +(* c-LEG (public): the threshold Fiat-Shamir challenge *) +(* `kmac_mu_w mu w_pub` equals central `rlwe_compute_c`, by the single *) +(* narrow PUBLIC-commitment bridge `threshold_public_commitment_eq_ *) +(* central` (rewrites `w_pub` to `central_w`). *) +(* Delta-LEG (public): `make_delta_of_w w_pub z_th` equals central *) +(* `rlwe_compute_delta`, by the same commitment bridge + the z-leg. *) +(* *) +(* ASSEMBLY: the packed (c,z,Delta) triple equals *) +(* `run_signing_components` of the central signer, i.e. *) +(* `sign_internal_loop usk mu rho = rlwe_sign_op (reconstruct ...)`. *) +(* *) +(* The ONLY residual axiom is `threshold_public_commitment_eq_central`, *) +(* a statement about PUBLIC data (the commitment `w = A*y`), MUCH narrower *) +(* than the original whole-bridge axiom and carrying NO secret content. *) +lemma combine_abs_op_lifted_eq_rlwe + (gpk : group_pk_t) (m : message_t) (ctx : ctx_t) + (quorum : int list) (shares : share_t list) + (rho_rnd : randomness_t) : + uniq quorum => + size shares = size quorum => + poly_degree (reconstruct quorum shares) < size quorum => + shares = List.map (poly_eval (reconstruct quorum shares)) quorum => + combine_abs_op_lifted gpk m ctx quorum shares rho_rnd + = rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd. +proof. + move=> Huniq Hsize Hdeg Hshare. + rewrite /combine_abs_op_lifted /=. + (* z-LEG: the real masked aggregate = central rlwe_compute_z. The + keystone holds for ANY challenge fed to the partials, in particular + the threshold Fiat-Shamir c = kmac_mu_w mu w_pub. *) + rewrite (no_leak_z_aggregate quorum shares + (kmac_mu_w (compute_mu m ctx) + (threshold_public_commitment quorum shares + (compute_mu m ctx) rho_rnd)) + rho_rnd (compute_mu m ctx) Huniq Hsize Hdeg Hshare). + (* c-LEG + Delta-LEG: rewrite the public commitment w_pub to central_w. *) + rewrite threshold_public_commitment_eq_central. + (* RHS: unfold the central signer down to its (c, z, Delta) components. *) + rewrite /rlwe_sign_op /sign_internal_loop /run_signing_components /=. + rewrite /rlwe_compute_c /rlwe_compute_delta. + (* Both sides are now pack_n1_signature of identical components. *) + done. +qed. + (* The wrapper module: calls the extracted Combine via the byte-level `combine_fn` op, materialising the input + output buffers from the abstract args. *) @@ -82,14 +207,20 @@ module CombineExtractedWrapper : Corona_Threshold = { }. (* The wrapper's combine matches the abstract CombineAbs.combine on - byte-equality, conditioned on the protocol-consistency precondition. + byte-equality, conditioned on the honest-quorum precondition. - This is the lemma that REPLACES the section-local `combine_body_axiom` - in Corona_N1.ec when the wrapper is instantiated as T. The proof - chains: - 1. combine_abs_op_lifted_bridge to rewrite the wrapper output as - the byte-level combine_abs_op. - 2. `byphoare` over the inlined wrapper body. + This lemma is now UNCONDITIONAL on any reconstruct-then-sign axiom: + the combine bridge `combine_abs_op_lifted_eq_rlwe` is a PROVEN LEMMA + (above), so `wrapper_combine_refines_abs` rests only on the narrow + PUBLIC-commitment residual `threshold_public_commitment_eq_central` + (and the unchanged B-bucket codec bridges). It is machine-CHECKED by + EasyCrypt. The proof: + 1. inlines both procedure bodies (`CombineAbs.combine` calls + `CentralRLWESign.sign`), reducing each side to a pure op; + 2. discharges the resulting op-equality by the proven bridge + `combine_abs_op_lifted_eq_rlwe`, supplying the honest-quorum + preconditions (uniq / size / degree / sharing) carried by the + equiv's precondition. The result is a procedure-level equiv that the extracted theorem in Corona_N1_Extracted.ec consumes. *) @@ -107,49 +238,57 @@ lemma wrapper_combine_refines_abs : (poly_eval (reconstruct quorum{1} shares{1})) quorum{1} ==> ={res} ]. proof. - (* The wrapper's body returns a pure op; CombineAbs.combine calls - into CentralRLWESign.sign which also returns a pure op. The two - pure ops agree on the abstract construction (Boschini §3): the - byte-equality content is captured by the combine_abs_op_lifted - definition itself, which by combine_abs_op_lifted_bridge reduces - to the byte-level combine_abs_op. - - The remaining gap is the bridge to CentralRLWESign.sign's - output: that this is the Boschini-conformant op is the in-house - RLWE_Functional axiom and Lean Crypto.Corona.Unforgeability - bridge. We treat this as the in-scope refinement claim: - `wrapper_combine_refines_abs` is the lemma form of the - section-local `combine_body_axiom` used by Corona_N1.ec. - - Direct discharge would require the procedure-level `equiv` - against the CentralRLWESign.sign call inside CombineAbs to be - replaced by `combine_abs_op_lifted_bridge`. This is mechanical; - we surface the structural reduction here and the closure pattern - mirrors Pulsar_N1_Combine_Wrapper.ec's lemma of the same name. *) + (* Both sides reduce to a pure op: + LHS CombineExtractedWrapper.combine returns + combine_abs_op_lifted group_pk m ctx quorum shares rho_rnd + RHS CombineAbs.combine reconstructs sk_group and calls + CentralRLWESign.sign, returning + rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd. + The two ops are equal by the PROVEN bridge + `combine_abs_op_lifted_eq_rlwe`: the threshold combine's masked + Lagrange z-aggregate equals central rlwe_compute_z via the Lean- + backed keystone (no_leak_z_aggregate), and the public challenge / + hint agree via the single narrow public-commitment residual. The + honest-quorum preconditions (uniq / size / degree / sharing) are + carried in the equiv precondition and threaded to the bridge. *) proc. inline CombineAbs.combine. inline CentralRLWESign.sign. wp. - skip => /> &m1 &m2 ? ? ? ? ? ? ? ?. - (* The two sides return: - LHS: combine_abs_op_lifted group_pk m ctx quorum shares rho_rnd - RHS: rlwe_sign_op (reconstruct quorum shares) m ctx rho_rnd - Equality between these is exactly what the Boschini-conformant - extraction makes true: the combine_abs_op_lifted definition is - pinned to rlwe_sign_op on the reconstructed share by the - CombineAbs body. This is the load-bearing refinement claim. *) - smt(combine_abs_op_lifted_bridge). + skip => /> &m1 &m2 ? ? ? ?. + by rewrite combine_abs_op_lifted_eq_rlwe. qed. (* =================================================================== ACCOUNTING - axioms (3 -- share + arg encoding + lifted bridge): + axioms (2 encoding/codec bridges, accepted with KAT+fuzz -- bucket B): share_encode_decode_roundtrip - combine_abs_op_lifted_bridge - (gpk_encode, msg_encode, ctx_encode, rho_encode are ops without - proof obligations) + combine_abs_op_lifted_bridge (lifted -> byte-level combine_abs_op; + now CONSTRAINS the still-opaque + combine_abs_op against the concrete + threshold definition -- B codec) - PROVED lemmas (0 admits): + axiom (1 NARROW public-commitment residual -- bucket C, DISCLOSED): + threshold_public_commitment_eq_central + The threshold-assembled PUBLIC commitment w = A*y (sum of per-party + Round-1 commitments, mask-summed, NO c*s) equals the central + commitment central_w on the reconstructed share. References PUBLIC + data ONLY. This is the SHRUNK residual that REPLACES the old + whole-bridge reconstruct-then-sign axiom combine_abs_op_lifted_eq_rlwe. + + DISCHARGED (was C11 axiom, now a PROVEN LEMMA -- net axiom count unchanged, + residual surface dramatically narrowed from whole-signature to public w): + combine_abs_op_lifted_eq_rlwe + z-leg via the MACHINE-CHECKED keystone Corona_N1_NoLeak.no_leak_z_ + aggregate (= Lean threshold_partial_response_identity): the load- + bearing secret-bearing leg is PROVEN, not assumed. c-leg + Delta-leg + via threshold_public_commitment_eq_central. The master secret is + never formed. + + lemmas machine-CHECKED by EasyCrypt (no longer conditional on any + reconstruct-then-sign axiom; rest only on the narrow public-commitment + residual + B codec bridges): + combine_abs_op_lifted_eq_rlwe wrapper_combine_refines_abs =================================================================== *) diff --git a/proofs/easycrypt/Corona_N1_Sign_Wrapper.ec b/proofs/easycrypt/Corona_N1_Sign_Wrapper.ec index 2c9c87f..de52491 100644 --- a/proofs/easycrypt/Corona_N1_Sign_Wrapper.ec +++ b/proofs/easycrypt/Corona_N1_Sign_Wrapper.ec @@ -60,7 +60,7 @@ lemma wrapper_sign_refines_central : proof. proc. wp. - skip => /> &m1 &m2 ? ? ? ? ?. + skip => /> &m1 &m2. by rewrite sign_abs_op_lifted_eq_rlwe. qed. diff --git a/proofs/easycrypt/lemmas/RLWE_Functional.ec b/proofs/easycrypt/lemmas/RLWE_Functional.ec index 77a7949..88f963c 100644 --- a/proofs/easycrypt/lemmas/RLWE_Functional.ec +++ b/proofs/easycrypt/lemmas/RLWE_Functional.ec @@ -11,7 +11,7 @@ (* What this file gives reviewers TODAY *) (* ------------------------------------ *) (* 1. Corona's parameter set as EasyCrypt operators *) -(* (q, n_poly, M, N, Dbar, Kappa, Xi, Nu, sigma_*). *) +(* (q, n_poly, M, N, Dbar, Kappa, Xi, Nu, sigma_star). *) (* 2. Abstract types R_q (polynomial ring), vec_N (R_q^N), *) (* vec_M (R_q^M), matrix_MN (R_q^{M x N}), bits (byte streams). *) (* 3. Auxiliary operations: round_xi, round_nu, expand_a, *)