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-07-27 02:50:34 +00:00 · 2026-05-19 08:38:08 -07:00
parent e9e4529a09
commit 1d483f7389
2 changed files with 412 additions and 0 deletions
@@ -0,0 +1,269 @@
+# Lean <-> EasyCrypt Shamir / Lagrange bridge for Corona
+
+## Why this document exists
+
+Corona's machine-checked proof stack uses **two complementary
+provers**, mirroring Pulsar's posture:
+
+* **EasyCrypt** drives the procedure-level refinement / equiv proofs
+  for the threshold layer (`proofs/easycrypt/Corona_N1.ec`,
+  `Corona_N4.ec`, the two `*_Refinement.ec` files, the two
+  `*_Layout.ec` files, the `Corona_N1_{Combine,Sign}_Wrapper.ec`
+  files, and `Corona_N1_Extracted.ec`).
+  EasyCrypt is the right tool for procedural Hoare/equiv goals with
+  side-channel-aware semantics -- but its first-order theory of
+  finite fields and polynomial interpolation is comparatively thin.
+* **Lean 4 + Mathlib** carries the algebraic content: Shamir
+  reconstruction, Lagrange interpolation linearity, finite-field
+  polynomial uniqueness. Mathlib has the field theory we'd otherwise
+  have to re-axiomatize in EC.
+
+The bridge between them is currently **conceptual** -- the EC side
+states the algebraic identities it needs as **named axioms** that
+correspond 1:1 to **proved Lean theorems** in
+`~/work/lux/proofs/lean/Crypto/Corona/`. This document pins that 1:1
+correspondence so a reviewer can verify the math content is discharged
+elsewhere and not silently hand-waved.
+
+The honest framing: **the EasyCrypt axioms named below are not
+unproved obligations in the strict sense -- they are imports from the
+Lean proof artifact**. The audit gap is operational (no mechanical
+proof-object exchange across the two provers, no shared serialization
+format) rather than mathematical.
+
+## Repository pin-points
+
+* EasyCrypt side: `~/work/lux/corona/proofs/easycrypt/`.
+* Lean side: `~/work/lux/proofs/lean/Crypto/Corona/`.
+
+## Axiom-to-theorem mapping
+
+### Axiom 1: `Corona_N1.lagrange_inverse_eval`
+
+**EasyCrypt statement** (`proofs/easycrypt/Corona_N1.ec`):
+
+```ec
+op poly_degree : share_t -> int.
+axiom poly_degree_nonneg (s : share_t) : 0 <= poly_degree s.
+
+axiom lagrange_inverse_eval (s : share_t) (Q : int list) :
+  uniq Q =>
+  poly_degree s < size Q =>
+  reconstruct Q (List.map (poly_eval s) Q) = s.
+```
+
+The `poly_degree s < size Q` precondition matches the Lean theorem's
+`f.degree < s.card`. Earlier weaker `1 <= size Q` formulations permit
+unsound instantiations on short quorums reconstructing a non-constant
+polynomial.
+
+**Lean proof** (`lean/Crypto/Corona/Shamir.lean:shamir_correct_at_target`):
+
+```lean
+theorem shamir_correct_at_target
+    {F : Type*} [Field F] [DecidableEq F]
+    (f : Polynomial F) {ι : Type*} [DecidableEq ι]
+    (s : Finset ι) (v : ι → F)
+    (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card) :
+    f = Lagrange.interpolate s v (fun i => f.eval (v i)) :=
+  Crypto.Threshold.Lagrange.threshold_reconstructs_secret f s v hvs degree_f_lt
+```
+
+**Correspondence**:
+
+| Symbol | EC | Lean |
+|---|---|---|
+| Shamir polynomial | `s : share_t` (abstracted as its constant term) | `f : Polynomial F` |
+| Quorum / evaluation set | `Q : int list` (with `uniq Q`) | `s : Finset ι` + `v : ι → F` injective on `s` |
+| Per-party share | `poly_eval s i` | `f.eval (v i)` |
+| Reconstruction | `reconstruct Q shares` | `(Lagrange.interpolate s v shares).eval 0` |
+| Identity at quorum | `reconstruct Q (map (poly_eval s) Q) = s` | `f = Lagrange.interpolate s v (fun i => f.eval (v i))` then evaluate at 0 |
+
+The Lean theorem is **stronger** (polynomial-level equality, not just
+constant-term recovery). Specializing to evaluation at 0 yields the
+EC-side identity via
+`Crypto.Threshold.Lagrange.secret_recovery_at_zero`
+(file `lean/Crypto/Threshold_Lagrange.lean:62`).
+
+### Axiom 2: `Corona_N4.reconstruct_linear`
+
+**EasyCrypt statement** (`proofs/easycrypt/Corona_N4.ec`):
+
+```ec
+axiom reconstruct_linear :
+  forall (q : int list) (a b : share_t list),
+    size a = size q => size b = size q =>
+    reconstruct q (zip_add a b) =
+      add_share (reconstruct q a) (reconstruct q b).
+```
+
+**Lean proof** (`lean/Crypto/Threshold_Lagrange.lean:combine_distributes_over_sum`):
+
+```lean
+theorem combine_distributes_over_sum
+    {ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F) (a b : ι → F) :
+    Lagrange.interpolate s v (a + b) =
+      Lagrange.interpolate s v a + Lagrange.interpolate s v b :=
+  (Lagrange.interpolate s v).map_add a b
+```
+
+**Correspondence**:
+
+| Symbol | EC | Lean |
+|---|---|---|
+| Quorum | `q : int list` | `s : Finset ι` |
+| Per-party value | `a : share_t list`, `b : share_t list` | `a, b : ι → F` |
+| Pointwise sum | `zip_add a b` | `a + b` (pointwise) |
+| Combination | `reconstruct q (...)` | `(Lagrange.interpolate s v (...)).eval 0` |
+| Linearity | `reconstruct (a + b) = reconstruct a + reconstruct b` | `interpolate (a + b) = interpolate a + interpolate b` |
+
+The Lean theorem follows from `LinearMap.map_add` applied to
+`Lagrange.interpolate s v`, which Mathlib expresses as an F-linear
+map. Evaluating at 0 preserves the equation.
+
+### Axiom 3: `Corona_N4.shamir_correct`
+
+**EasyCrypt statement** (`proofs/easycrypt/Corona_N4.ec`):
+
+```ec
+axiom shamir_correct :
+  forall (q : int list) (s : share_t),
+    uniq q => 1 <= size q =>
+    reconstruct q (fresh_sharing q s) = s.
+```
+
+**Lean proof** (same as Axiom 1: `shamir_correct_at_target`).
+
+Plus the auxiliary `secret_recovery_at_zero`
+(`lean/Crypto/Threshold_Lagrange.lean:62`).
+
+**Correspondence**: `fresh_sharing q s` is the Corona adapter that
+constructs the per-party shares of `s` along quorum `q` (= mapping
+`q -> poly_eval s` on each `q[i]`, modulo the internal randomness of
+the polynomial above degree 0). After Lagrange-recovery via
+`reconstruct`, the constant term `s` returns.
+
+### Axiom 4: `Corona_N4.add_share_zeroR`
+
+**EasyCrypt statement** (`proofs/easycrypt/Corona_N4.ec`):
+
+```ec
+axiom add_share_zeroR : forall (s : share_t), add_share s zero_share = s.
+```
+
+This is an algebraic identity on the `share_t` ring (right-identity of
+addition). Mathlib provides this for any `AddCommMonoid`-instance
+type, but the EC side keeps `share_t` abstract and so axiomatizes the
+property directly. On the Lean side this is implicit in the `Ring` /
+`Polynomial`-coefficient instances and never needs an explicit
+theorem -- it's provided by Mathlib for any AddCommMonoid (and proved
+in `lean/Crypto/Corona/Shamir.lean:add_share_zeroR` as a one-line
+`exact add_zero f` for the surfacing convenience).
+
+### Axiom 5: `Corona_N1.threshold_partial_response_identity`
+
+**EasyCrypt statement** (`proofs/easycrypt/Corona_N1.ec`):
+
+```ec
+axiom threshold_partial_response_identity :
+  forall (Q : int list) (shares : share_t list)
+         (c : c_n1_t) (rho_rnd : randomness_t) (mu_val : mu_t),
+    uniq Q =>
+    size shares = size Q =>
+    poly_degree (reconstruct Q shares) < size Q =>
+    shares = List.map (poly_eval (reconstruct Q shares)) Q =>
+    lagrange_aggregate_responses Q
+      (List.map (per_party_partial_response c rho_rnd mu_val) shares)
+    = rlwe_compute_z
+        (unpack_sk (reconstruct Q shares))
+        mu_val rho_rnd.
+```
+
+**Lean counterpart**
+(`~/work/lux/proofs/lean/Crypto/Threshold_Lagrange.lean:121`,
+theorem `threshold_partial_response_identity`):
+
+```lean
+theorem threshold_partial_response_identity
+    (f : F[X]) {ι : Type*} [DecidableEq ι] (s : Finset ι) (v : ι → F)
+    (hvs : Set.InjOn v s) (degree_f_lt : f.degree < s.card)
+    (y : ι → F) (c : F)
+    (z : ι → F) (hz : z = y + c • fun i => f.eval (v i)) :
+    (Lagrange.interpolate s v z).eval 0 =
+      (Lagrange.interpolate s v y).eval 0 + c * f.eval 0
+```
+
+**Type correspondence**
+
+| Lean | EasyCrypt | Meaning |
+|---|---|---|
+| `F[X]` | (abstracted into `share_t`) | secret-sharing polynomial |
+| `s : Finset ι` | `Q : int list` (with `uniq Q`) | quorum |
+| `v : ι → F` (with `Set.InjOn v s`) | implicit in `uniq Q` | party indexing |
+| `degree_f_lt : f.degree < s.card` | `poly_degree (reconstruct Q shares) < size Q` | sharing-polynomial degree bound |
+| `z = y + c • fun i => f.eval (v i)` (per party) | `per_party_partial_response c rho_rnd mu_val (poly_eval (reconstruct Q shares) i)` | per-party response |
+| `Lagrange.interpolate s v z .eval 0` | `lagrange_aggregate_responses Q [per_party_PR_i]` | quorum aggregation at 0 |
+| `+ c * f.eval 0` | folded into the abstract `rlwe_compute_z` on the reconstructed share | centralised z |
+
+**Used by**
+`Corona_N1_Combine_Refinement.combine_body_spec` (the byte-walk
+obligation; this bridge factors the z-stage portion of the byte-walk
+into a Lean-discharged identity + a narrower extraction-side
+sub-axiom).
+
+**Honest framing**
+
+The EC axiom integrates THREE facts:
+1. The Lean theorem's algebraic identity (interpolate-z = interpolate-y + c·f(0));
+2. The implicit y-aggregation: `rlwe_compute_z`'s y_central equals the
+   Lagrange-aggregation of the per-party y_i values used in
+   `per_party_partial_response`;
+3. The structural decomposition `rlwe_compute_z = y_central + c · s_central`.
+
+(2) and (3) are folded into the EC axiom's RHS via the abstract
+`rlwe_compute_z` op. Future narrowing would expose y_aggregation as a
+separate identity and split this bridge into smaller pieces.
+
+## What this bridge does NOT do
+
+It does **not** provide a mechanical proof-object exchange. The EC
+axioms are still trusted in the EC dependency cone -- the bridge is a
+code-review-level mapping, not a formal-method-level one.
+
+The honest closure path is:
+
+1. **Either** mechanize the four axioms inside EasyCrypt itself (would
+   require importing or rebuilding a finite-field polynomial-
+   interpolation library in EC; multi-week project),
+2. **Or** prove the same statements in a tool whose proof object EC
+   can consume (no current standard format),
+3. **Or** keep the conceptual bridge and pin the Lean commit in the EC
+   file headers (which we do, see "Citation comments" below).
+
+Option (3) is what we do today. It is honest -- the EC axiom
+statements correspond 1:1 to Lean theorems we have proved -- but it
+is not strict closure inside the EC dependency cone.
+
+## Citation comments
+
+Each of the five EC axioms above has an inline comment immediately
+preceding it that names the Lean theorem and file. Updating the EC
+axiom statement without updating the Lean side (or vice versa) trips
+the per-push test via `scripts/check-lean-bridge.sh`.
+
+## Honest summary
+
+The trust footprint of the extracted Corona N1 byte-equality theorem:
+
+* **Implementation-refinement axioms** (EC, byte-walks): 4 stage-level
+  obligations in the Refinement scaffolds + 3 atomic byte-walk +
+  layout-frame + memory-separation axioms per refinement file.
+* **Algebraic-content axioms bridged to Lean**: 5 (Axioms 1-5 above).
+  Each has a corresponding Lean theorem cited inline.
+* **Module-contract axioms in the extracted N1 corollary**: 0 (after
+  wrapper instantiation, both `combine_body_axiom` and
+  `S_functional_spec` are discharged by the Wrapper lemmas
+  `wrapper_combine_refines_abs` and `wrapper_sign_refines_central`).
+
+The full per-axiom inventory lives in
+`proofs/easycrypt/Corona_N1_Extracted.ec` and `AXIOM-INVENTORY.md`.
@@ -0,0 +1,143 @@
+#!/usr/bin/env bash
+# Lean <-> EasyCrypt Shamir bridge guard for Corona.
+#
+# Each EC axiom named in proofs/lean-easycrypt-bridge.md must:
+#   1. Still exist in the EC source as an `axiom` (not `lemma`).
+#   2. Carry an inline citation comment naming the Lean theorem.
+#   3. The Lean theorem named in the citation must EXIST in the
+#      named Lean file (hardened guard).
+#
+# Plus:
+#   4. The bridge doc must exist.
+#   5. Every EC file path mentioned in the bridge doc text must
+#      exist on disk (catches stale refs to decomplected files).
+#
+# Mirrors ~/work/lux/pulsar/scripts/check-lean-bridge.sh but for the
+# Corona axiom set.
+
+set -euo pipefail
+
+REPO_ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+cd "$REPO_ROOT"
+
+# Lean repo autodetect.
+LEAN_ROOT=""
+for candidate in \
+    "$HOME/work/lux/proofs/lean" \
+    "$HOME/work/lux/proofs" \
+    "$REPO_ROOT/../proofs/lean" \
+    "$REPO_ROOT/../../proofs/lean" \
+; do
+    if [[ -d "$candidate/Crypto" ]]; then
+        LEAN_ROOT="$candidate"
+        break
+    fi
+done
+have_lean=0
+if [[ -n "$LEAN_ROOT" ]]; then
+    have_lean=1
+fi
+
+FAIL=0
+
+# (axiom-name, ec-file, lean-citation-substring, lean-theorem-name, lean-file-rel-to-Crypto)
+declare -a BRIDGE=(
+    "lagrange_inverse_eval|proofs/easycrypt/Corona_N1.ec|shamir_correct_at_target|shamir_correct_at_target|Corona/Shamir.lean"
+    "add_share_zeroR|proofs/easycrypt/Corona_N4.ec|AddCommMonoid||"
+    "reconstruct_linear|proofs/easycrypt/Corona_N4.ec|combine_distributes_over_sum|combine_distributes_over_sum|Threshold_Lagrange.lean"
+    "shamir_correct|proofs/easycrypt/Corona_N4.ec|shamir_correct_at_target|shamir_correct_at_target|Corona/Shamir.lean"
+    "threshold_partial_response_identity|proofs/easycrypt/Corona_N1.ec|threshold_partial_response_identity|threshold_partial_response_identity|Threshold_Lagrange.lean"
+)
+
+echo "==> Lean <-> EC Shamir bridge guard (Corona)"
+if [[ $have_lean -eq 1 ]]; then
+    echo "    [info] Lean repo: $LEAN_ROOT"
+else
+    echo "    [info] no Lean repo on disk; skipping Lean-side existence checks"
+fi
+
+for entry in "${BRIDGE[@]}"; do
+    IFS='|' read -r axiom file lean_ref lean_thm lean_rel <<< "$entry"
+
+    # 1. EC file present.
+    if [[ ! -f "$file" ]]; then
+        echo "    [FAIL] $axiom: $file not found"
+        FAIL=1
+        continue
+    fi
+
+    # 2. EC axiom still exists.
+    line=$(grep -nE "^axiom[[:space:]]+${axiom}[[:space:]]*" "$file" | head -1 | cut -d: -f1)
+    if [[ -z "$line" ]]; then
+        echo "    [FAIL] $axiom: declaration not found in $file"
+        FAIL=1
+        continue
+    fi
+
+    # 3. Citation comment in the 30 lines preceding the axiom.
+    start=$((line > 30 ? line - 30 : 1))
+    if ! sed -n "${start},${line}p" "$file" | grep -q "$lean_ref"; then
+        echo "    [FAIL] $axiom @ $file:$line -- bridge comment missing reference to '$lean_ref'"
+        FAIL=1
+        continue
+    fi
+
+    # 4. Lean theorem existence (when a Lean repo is on disk).
+    if [[ $have_lean -eq 1 && -n "$lean_thm" && -n "$lean_rel" ]]; then
+        lean_file="$LEAN_ROOT/Crypto/$lean_rel"
+        if [[ ! -f "$lean_file" ]]; then
+            echo "    [FAIL] $axiom: cited Lean file $lean_file not found"
+            FAIL=1
+            continue
+        fi
+        if ! grep -qE "^(theorem|lemma)[[:space:]]+${lean_thm}[[:space:]]*\\b" "$lean_file"; then
+            echo "    [FAIL] $axiom: cited Lean theorem $lean_thm not found in $lean_file"
+            FAIL=1
+            continue
+        fi
+    fi
+
+    echo "    [ok]   $axiom @ $file:$line -> $lean_ref"
+done
+
+# Bridge doc presence.
+BRIDGE_DOC="proofs/lean-easycrypt-bridge.md"
+if [[ ! -f "$BRIDGE_DOC" ]]; then
+    echo "    [FAIL] $BRIDGE_DOC is missing"
+    FAIL=1
+else
+    missing_refs=()
+    while IFS= read -r ref; do
+        clean=$(echo "$ref" | tr -d '`')
+        if [[ ! -f "$clean" ]]; then
+            missing_refs+=("$clean")
+        fi
+    done < <(grep -oE 'proofs/easycrypt/[A-Za-z0-9_/]+\.(ec|md)' "$BRIDGE_DOC" | sort -u)
+
+    if [[ $have_lean -eq 1 ]]; then
+        while IFS= read -r ref; do
+            clean=$(echo "$ref" | tr -d '`')
+            rel="${clean#*lean/Crypto/}"
+            full="$LEAN_ROOT/Crypto/$rel"
+            if [[ ! -f "$full" ]]; then
+                missing_refs+=("$clean")
+            fi
+        done < <(grep -oE 'lean/Crypto/[A-Za-z0-9_/]+\.lean' "$BRIDGE_DOC" | sort -u)
+    fi
+
+    if [[ ${#missing_refs[@]} -gt 0 ]]; then
+        echo "    [FAIL] bridge doc references files that don't exist on disk:"
+        printf "             %s\n" "${missing_refs[@]}"
+        FAIL=1
+    else
+        echo "    [ok]   $BRIDGE_DOC present + every file path in it exists"
+    fi
+fi
+
+if [[ $FAIL -ne 0 ]]; then
+    echo
+    echo "    Lean <-> EC bridge guard FAILED"
+    exit 2
+fi
+echo "    [ok]   all ${#BRIDGE[@]} axiom citations present + Lean-side names verified"
+exit 0