From 1766544daf032fc3e3f9aad643fadf435523f6e6 Mon Sep 17 00:00:00 2001 From: saymrwulf Date: Fri, 3 Jul 2026 17:26:50 +0200 Subject: [PATCH] scalar layer: Scalar52::sub FULLY proven mod l (sub_val_spec) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit sub_val_spec closes the top-level two-clause value spec: denote(Scalar52.sub a b) = denote(a) - denote(b) in ZMod l for limb-bounded inputs with canonical subtrahend (scVal b < l). Axiom-clean [propext, Classical.choice, Quot.sound]; no sorry. The assembly documented-as-remaining last session is now done. Key resolutions: - Applied the WP "spec_bind" rule manually instead of "step", and reduced the resulting "let (difference,borrow) := (dw,w)" Prod-let with an explicit "show" — this was the destructuring friction that blocked the earlier attempt (step's arity heuristics mis-typed the pair result). - Inlined the subtle "Choice::from" identity (no step-spec, like csel_step). - PERFORMANCE: kept "scLimbs" as opaque atoms in the gamma5=1 derivation instead of "unfold ... at *" — the unfold exploded omega with 2^52..2^260 coefficients and blew past 600s; atomic form proves in ~1 min (METHOD 4, same kernel-cost discipline as the field layer). - The 2^260 borrow-wrap and the +l conditional-add cancel in ZMod l: beta5=0 direct; beta5=1 forces top carry gamma5=1 from scVal b < l, closed by linear_combination over the two telescopes (sub_telescope, add_telescope). check-scalar.sh: sub_val_spec in the manifest + Phase-3 audit (4/4 clean); proof-phase caps raised to 600s/8192MB for the assembly; full button green. exponentiation.threshold raised to 300 for the 2^260 literal. Co-Authored-By: Claude Fable 5 --- README.md | 2 +- verification/Proofs/ScalarSubSpec.lean | 132 ++++++++++++++++++++----- verification/check-scalar.sh | 6 +- 3 files changed, 110 insertions(+), 30 deletions(-) diff --git a/README.md b/README.md index d322f12..5ec97a1 100644 --- a/README.md +++ b/README.md @@ -27,7 +27,7 @@ in this repository. |-------|-------------|--------|-----------------------| | Field 𝔽_p | `fieldImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` | | Group law (Edwards) | `edwardsImplementation` | ✅ proven | `[propext, Classical.choice, Quot.sound]` | -| Scalar mod ℓ | `scalarImplementation` (planned; `L_val`, `sub_loop_spec`, `cond_add_l_*_spec` proven) | 🔨 foundation+sub | denotation + L=ℓ + sub borrow/carry chains proven; sub value-assembly & mul in progress | +| Scalar mod ℓ | `scalarImplementation` (planned; `sub_val_spec` ✅, `L_val`, loop specs proven) | 🔨 sub done · add/mul next | denotation + L=ℓ + FULL sub (⟦sub a b⟧=⟦a⟧−⟦b⟧ in ZMod ℓ) proven; add & Montgomery mul next | | Signature (EdDSA) | `verifyEquation` (planned) | ⏳ planned | — | Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started. diff --git a/verification/Proofs/ScalarSubSpec.lean b/verification/Proofs/ScalarSubSpec.lean index 9666de2..9702dd2 100644 --- a/verification/Proofs/ScalarSubSpec.lean +++ b/verification/Proofs/ScalarSubSpec.lean @@ -51,6 +51,7 @@ open curve25519_dalek set_option maxHeartbeats 4000000 set_option linter.unusedSimpArgs false +set_option exponentiation.threshold 300 namespace ScalarProofs @@ -705,32 +706,111 @@ theorem add_telescope + (c0 + 2^52*c1 + 2^104*c2 + 2^156*c3 + 2^208*c4) := by omega -/-! ### Top-level `sub_val_spec` — remaining assembly (no `sorry` shipped) +/-! ### Top-level subtraction value spec -/ -Every mechanically hard piece is proven above and kernel-checked: - • `sub_loop_spec` — the full 5-limb borrow chain (wrapping_sub, mask, - borrow-out bit): the loop unroll that blocked the - earlier attempt; - • `cond_add_l_zero_spec`, `cond_add_l_one_spec` — both conditional-add-ℓ - cases, full carry chains (the condition-1 case drives - the write-back through a stepped `csel_step` so the - `index_mut` matches `sub_loop`'s working pattern); - • `sub_telescope`, `add_telescope` — the 2⁵²ⁱ-weighted value telescopes - up to 2²⁶⁰, discharged by `omega` (no kernel-capacity - blowup — coefficients stay ≤ 2²⁶⁰); - • `sub_step_arith`, `csel_step`, the bit↔arith lemmas. - -`sub_val_spec` assembles them: unfold `sub`, run `sub_loop`, read -`borrow >>> 63` into a `Choice`, run `conditional_add_l`, split on the -underflow bit β5. The value identity in `ZMod ℓ`, - ⟦sub a b⟧ = ⟦a⟧ − ⟦b⟧ (canonical inputs, scVal b < ℓ), -is complete on paper: β5 = 0 gives ⟦d⟧ + ⟦b⟧ = ⟦a⟧ directly; β5 = 1 gives -the borrow-wrap 2²⁶⁰ and the +ℓ, which cancel in `ZMod ℓ` once the top -carry γ5 = 1 (forced by scVal b < ℓ). The remaining step is purely the -Aeneas binding-arity for destructuring `sub_loop_spec`'s pair-valued, -multi-existential postcondition inside the outer `do`-block — a mechanical, -not a mathematical or trust gap. Tracked in the control-repo MANIFEST -scalar `open_frontier`; this file ships only kernel-checked content -(Invariants H1/H4). -/ +/-- **Scalar subtraction is correct mod ℓ.** For limb-bounded inputs with + canonical subtrahend (scVal b < ℓ), the transpiled `Scalar52::sub` + denotes ⟦a⟧ − ⟦b⟧ in `ZMod ℓ`. Assembly of `sub_loop_spec` (borrow + chain) and `cond_add_l_{zero,one}_spec` (conditional +ℓ) through the + two telescopes; the bind is applied manually via `spec_bind` to keep + full control of the postcondition destructuring. -/ +theorem sub_val_spec (a b : Sc) + (a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 : U64) + (ha : (↑a : List U64) = [a0, a1, a2, a3, a4]) + (hb : (↑b : List U64) = [b0, b1, b2, b3, b4]) + (hab : a0.val < 2^52 ∧ a1.val < 2^52 ∧ a2.val < 2^52 ∧ a3.val < 2^52 ∧ a4.val < 2^52) + (hbb : b0.val < 2^52 ∧ b1.val < 2^52 ∧ b2.val < 2^52 ∧ b3.val < 2^52 ∧ b4.val < 2^52) + (hcb : scVal b < Ell) : + backend.serial.u64.scalar.Scalar52.sub a b + ⦃ r => scDenote r = scDenote a - scDenote b ⦄ := by + obtain ⟨hA0, hA1, hA2, hA3, hA4⟩ := hab + obtain ⟨hB0, hB1, hB2, hB3, hB4⟩ := hbb + unfold backend.serial.u64.scalar.Scalar52.sub + step as ⟨sh, hsh⟩ + step as ⟨mask, hmask⟩ + have hmaskv : mask.val = 2^52 - 1 := by + simp [hmask, hsh, U64.size_def, U64.numBits] + -- bind the borrow loop manually + apply spec_bind (sub_loop_spec a b mask a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 ha hb hmaskv + ⟨hA0, hA1, hA2, hA3, hA4, hB0, hB1, hB2, hB3, hB4⟩) + rintro ⟨dw, w⟩ ⟨d0, d1, d2, d3, d4, β1, β2, β3, β4, β5, hdl, + hβ1, hβ2, hβ3, hβ4, hβ5, hd0, hd1, hd2, hd3, hd4, + he0, he1, he2, he3, he4, hbor⟩ + simp only at hdl hbor + show (do + let i1 ← w >>> 63#i32 + let i2 ← lift (UScalar.cast UScalarTy.U8 i1) + let c ← subtle.Choice.Insts.CoreConvertFromU8.from i2 + let (_, difference1) ← dw.conditional_add_l c + ok difference1) ⦃ r => scDenote r = scDenote a - scDenote b ⦄ + -- borrow >>> 63, cast, Choice + step as ⟨i1, hi1⟩ + have hi1v : i1.val = β5 := by rw [hi1]; exact hbor + step as ⟨i2, hi2⟩ + -- Choice.from is the identity model; inline c := i2 + simp only [subtle.Choice.Insts.CoreConvertFromU8.from, bind_tc_ok] + set cc := i2 with hccdef + have hccv : cc.val = β5 := by + have hb5 : β5 < 2^8 := by omega + rw [hi2, UScalar.cast_val_eq, hi1v] + simp only [UScalarTy.U8, UScalarTy.numBits] + omega + have hdb : d0.val < 2^52 ∧ d1.val < 2^52 ∧ d2.val < 2^52 ∧ d3.val < 2^52 ∧ d4.val < 2^52 := + ⟨hd0, hd1, hd2, hd3, hd4⟩ + have hTsub : scLimbs d0 d1 d2 d3 d4 + scLimbs b0 b1 b2 b3 b4 + = scLimbs a0 a1 a2 a3 a4 + 2^260 * β5 := by + unfold scLimbs + exact sub_telescope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ he0 he1 he2 he3 he4 + have hsva : scVal a = scLimbs a0 a1 a2 a3 a4 := scVal_eq a a0 a1 a2 a3 a4 ha + have hsvb : scVal b = scLimbs b0 b1 b2 b3 b4 := scVal_eq b b0 b1 b2 b3 b4 hb + rcases (Nat.le_one_iff_eq_zero_or_eq_one.mp hβ5) with hβz | hβo + · -- β5 = 0: no underflow, cond-add is identity on values + have hc0 : cc.val = 0 := by rw [hccv, hβz] + apply spec_bind (cond_add_l_zero_spec dw cc d0 d1 d2 d3 d4 hdl hc0 hdb) + rintro ⟨cw1, cw2⟩ ⟨r0, r1, r2, r3, r4, hrl, hr0, hr1, hr2, hr3, hr4⟩ + simp only at hrl + show scDenote cw2 = scDenote a - scDenote b + have hcwval : scVal cw2 = scLimbs d0 d1 d2 d3 d4 := by + rw [scVal_eq cw2 r0 r1 r2 r3 r4 hrl]; unfold scLimbs; rw [hr0, hr1, hr2, hr3, hr4] + have key : scVal cw2 + scVal b = scVal a := by + rw [hcwval, hsva, hsvb]; rw [hβz] at hTsub; simpa using hTsub + have hc := congrArg (Nat.cast (R := ZMod Ell)) key + push_cast at hc + simp only [scDenote]; rw [eq_sub_iff_add_eq]; exact hc + · -- β5 = 1: underflow; +ℓ, and the 2^260 wrap cancels in ZMod ℓ + have hc1 : cc.val = 1 := by rw [hccv, hβo] + apply spec_bind (cond_add_l_one_spec dw cc d0 d1 d2 d3 d4 hdl hc1 hdb) + rintro ⟨cw1, cw2⟩ ⟨r0, r1, r2, r3, r4, γ1, γ2, γ3, γ4, γ5, hrl, + hgb1, hgb2, hgb3, hgb4, hgb5, hrb0, hrb1, hrb2, hrb3, hrb4, + hf0, hf1, hf2, hf3, hf4⟩ + simp only at hrl + show scDenote cw2 = scDenote a - scDenote b + have hLsum : (671914833335277 + 2^52*3916664325105025 + 2^104*1367801 + + 2^156*0 + 2^208*17592186044416 : ℕ) = Ell := by unfold Ell; norm_num + have hTadd : scLimbs r0 r1 r2 r3 r4 + 2^260 * γ5 = scLimbs d0 d1 d2 d3 d4 + Ell := by + have h := add_telescope r0.val r1.val r2.val r3.val r4.val + d0.val d1.val d2.val d3.val d4.val + 671914833335277 3916664325105025 1367801 0 17592186044416 + γ1 γ2 γ3 γ4 γ5 hf0 hf1 hf2 hf3 hf4 + unfold scLimbs; rw [← hLsum]; linear_combination h + have hblt : scLimbs b0 b1 b2 b3 b4 < Ell := by rw [← hsvb]; exact hcb + -- γ5 = 1, derived with scLimbs kept as opaque atoms (no 2^52i unfold → + -- omega stays cheap: 4 atoms + one 2^260 literal + Ell as an atom) + have hrlt : scLimbs r0 r1 r2 r3 r4 < 2^260 := by unfold scLimbs; omega + have hd_eq : scLimbs d0 d1 d2 d3 d4 + scLimbs b0 b1 b2 b3 b4 + = scLimbs a0 a1 a2 a3 a4 + 2^260 := by rw [hβo] at hTsub; simpa using hTsub + have hγ5 : γ5 = 1 := by + -- atoms: R,D,B,A := scLimbs …, Ell; facts below force γ5 = 1 + have hRnn : 0 ≤ scLimbs a0 a1 a2 a3 a4 := Nat.zero_le _ + omega + have hc := congrArg (Nat.cast (R := ZMod Ell)) hTadd + have hc2 := congrArg (Nat.cast (R := ZMod Ell)) hTsub + have hEz : (Ell : ZMod Ell) = 0 := ZMod.natCast_self Ell + simp only [scDenote, scVal_eq cw2 r0 r1 r2 r3 r4 hrl, hsva, hsvb, hβo, hγ5] + rw [hγ5] at hc + rw [hβo] at hc2 + push_cast at hc hc2 ⊢ + rw [hEz] at hc + linear_combination hc + hc2 end ScalarProofs diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh index 32c9028..ddb56c2 100755 --- a/verification/check-scalar.sh +++ b/verification/check-scalar.sh @@ -19,7 +19,7 @@ lake env bash -c " cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" for m in ${GEN[*]}; do echo \" · gen \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"\$m.lean\" || exit 1; done cd '$HERE' - for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=300 LEAN_MEM_MB=6144 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done + for m in ${PROOFS[*]}; do echo \" · proof \$m\"; LEAN_TIMEOUT=600 LEAN_MEM_MB=8192 '$HERE/lean-guard' \"Proofs/\$m.lean\" || exit 1; done " || { echo FAIL; exit 1; } echo "=== Phase 3: axiom audit (kernel-level) ===" cd "$AENEAS_LEAN" @@ -30,12 +30,12 @@ lake env bash -c " AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean') { echo 'import Proofs.ScalarDenote'; echo 'import Proofs.ScalarSubSpec'; echo '#print axioms ScalarProofs.L_val' echo '#print axioms ScalarProofs.sub_loop_spec' - echo '#print axioms ScalarProofs.cond_add_l_one_spec'; } > \"\$AUD\" + echo '#print axioms ScalarProofs.cond_add_l_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; } > \"\$AUD\" OUT=\$(LEAN_TIMEOUT=120 LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) echo \"\$OUT\" rm -f \"\$AUD\" \"\${AUD%.lean}.olean\" N=\$(echo \"\$OUT\" | grep -cF \"depends on axioms: [propext, Classical.choice, Quot.sound]\" || true) - [ \"\$N\" -eq 3 ] || { echo \"AXIOM AUDIT FAILED: \$N/3 clean\"; exit 1; } + [ \"\$N\" -eq 4 ] || { echo \"AXIOM AUDIT FAILED: \$N/4 clean\"; exit 1; } " || { echo FAIL; exit 1; } echo " L_val axiom-clean"