diff --git a/README.md b/README.md index 9dc34c1..5b675c3 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 β„“ | `add_val_spec` βœ… `sub_val_spec` βœ… (aggregate planned) | πŸ”¨ add+sub done Β· mul next | ⟦add⟧/⟦sub⟧ = +/βˆ’ in ZMod β„“ proven against this fork's v4 two-loop masked-L sub; Montgomery mul next | +| Scalar mod β„“ | `scalarImplementation` (add βœ… sub βœ… mul βœ…) | βœ… proven | `[propext, Classical.choice, Quot.sound]` | | Signature (EdDSA) | `verifyEquation` (planned) | ⏳ planned | β€” | Status legend: βœ… proven & axiom-audited Β· ⏳ in progress Β· ❌ not started. diff --git a/verification/Proofs/ScalarAddSpec.lean b/verification/Proofs/ScalarAddSpec.lean index d28b519..f0abb2a 100644 --- a/verification/Proofs/ScalarAddSpec.lean +++ b/verification/Proofs/ScalarAddSpec.lean @@ -226,7 +226,9 @@ theorem add_val_spec (a b : Sc) (hbb : b0.val < 2^52 ∧ b1.val < 2^52 ∧ b2.val < 2^52 ∧ b3.val < 2^52 ∧ b4.val < 2^52) (hca : scVal a < Ell) (hcb : scVal b < Ell) : backend.serial.u64.scalar.Scalar52.add a b - ⦃ r => scDenote r = scDenote a + scDenote b ⦄ := by + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ s4.val < 2^52) ∧ + 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.add @@ -241,7 +243,9 @@ theorem add_val_spec (a b : Sc) hf0, hf1, hf2, hf3, hf4⟩ try simp only at hrl show backend.serial.u64.scalar.Scalar52.sub sum backend.serial.u64.constants.L - ⦃ r => scDenote r = scDenote a + scDenote b ⦄ + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ s4.val < 2^52) ∧ + scDenote r = scDenote a + scDenote b ⦄ -- telescope: scLimbs sum + 2^260Β·Ξ³5 = scVal a + scVal b; canonicity kills Ξ³5 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 @@ -269,7 +273,8 @@ theorem add_val_spec (a b : Sc) (by refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> norm_num) (by rw [L_val])) intro r hr - rw [hr] + refine ⟨hr.1, ?_⟩ + rw [hr.2] have hL0 : scDenote backend.serial.u64.constants.L = 0 := by simp only [scDenote, L_val]; exact ZMod.natCast_self Ell have hsd : scDenote sum = scDenote a + scDenote b := by diff --git a/verification/Proofs/ScalarFullMulSpec.lean b/verification/Proofs/ScalarFullMulSpec.lean new file mode 100644 index 0000000..8e89577 --- /dev/null +++ b/verification/Proofs/ScalarFullMulSpec.lean @@ -0,0 +1,249 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ScalarFullMulSpec.lean β€” Scalar52 multiplication, phase C: `mul`. + + `mul a b` composes the proven pieces (scalar.rs:302-305): + mul_internal a b β€” nine exact schoolbook columns (phase A) + montgomery_reduce β€” ⟦ab'⟧·R = aΒ·b with R = 2^260 (phase B) + mul_internal ab' RR β€” columns against RR ≑ RΒ² (mod β„“) + montgomery_reduce β€” ⟦r⟧·R = ⟦ab'⟧·RΒ² ⟹ ⟦r⟧ = ⟦ab'⟧·R + so ⟦r⟧·R = ⟦ab'⟧·RΒ·R = (⟦a⟧·⟦b⟧)Β·R, and R = 2^260 is a unit in ZMod β„“ + (β„“ is odd), giving ⟦mul a b⟧ = ⟦a⟧ Β· ⟦b⟧. + + The first reduction carries the honest Montgomery hypothesis + scVal a Β· scVal b < 2^260Β·β„“ (canonical inputs satisfy it: β„“Β² < 2^260Β·β„“); + the second needs nothing extra because scVal RR < β„“. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ScalarReduceSpec +open Aeneas Aeneas.Std Result +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option exponentiation.threshold 600 + +namespace ScalarProofs + +open Aeneas.Std.WP + +/-! ### The RR constant: RR ≑ RΒ² = 2^520 (mod β„“) -/ + +/-- The transpiled `constants::RR` as a limb list. -/ +theorem RR_limbs : + (↑backend.serial.u64.constants.RR : List U64) = + [2764609938444603#u64, 3768881411696287#u64, 1616719297148420#u64, + 1087343033131391#u64, 10175238647962#u64] := by + unfold backend.serial.u64.constants.RR + rfl + +/-- The value of the transpiled RR constant. -/ +theorem RR_scVal : scVal backend.serial.u64.constants.RR + = 4185850391763183796333492317919282507600454137915443218209456916606550724923 := by + rw [scVal_eq _ _ _ _ _ _ RR_limbs] + unfold scLimbs + norm_num + +/-- RR is canonical (below β„“). -/ +theorem RR_lt : scVal backend.serial.u64.constants.RR < Ell := by + rw [RR_scVal]; unfold Ell; norm_num + +/-- **RR denotes RΒ² = 2^520 in ZMod β„“** β€” the exact division witness + 2^520 = RR + KΒ·β„“ is kernel-checked literal arithmetic. -/ +theorem RR_denote : + ((4185850391763183796333492317919282507600454137915443218209456916606550724923 : β„•) + : ZMod Ell) = 2^520 := by + have h : (2:β„•)^520 + = 4185850391763183796333492317919282507600454137915443218209456916606550724923 + + 474284397516047136454946754595585670565175736652605875744292671501348828217547577 + * Ell := by + unfold Ell; norm_num + have hc := congrArg (Nat.cast (R := ZMod Ell)) h + push_cast at hc + -- push_cast evaluates 2^520 to its literal and kills the ↑Ell factor: + -- hc : (2^520-literal : ZMod Ell) = RR + KΒ·0 + have h2 : ((2:ZMod Ell))^520 + = (3432398830065304857490950399540696608634717650071652704697231729592771591698828026061279820330727277488648155695740429018560993999858321906287014145557528576 : ZMod Ell) := by norm_num + rw [h2] + push_cast + rw [hc, ZMod.natCast_self Ell] + ring + +/-- 2^260 is a unit in ZMod β„“ (β„“ is odd). -/ +theorem R_isUnit : IsUnit ((2 : ZMod Ell)^260) := by + have hcop : Nat.Coprime 2 Ell := by + unfold Ell + norm_num + exact ⟨3618502788666131106986593281521497120428558179689953803000975469142727125494, + by norm_num⟩ + have h2 : IsUnit ((2 : β„•) : ZMod Ell) := (ZMod.isUnit_iff_coprime 2 Ell).mpr hcop + have h2' : IsUnit (2 : ZMod Ell) := by simpa using h2 + exact h2'.pow 260 + +/-- 52-bit product bound (both factors 52-bit). -/ +theorem col_bound {x y : β„•} (hx : x < 2^52) (hy : y < 2^52) : x * y < 2^104 := by + have h := Nat.mul_lt_mul'' hx hy + omega + +/-! ### The full multiplication -/ + +/-- **Scalar multiplication is correct mod β„“.** For limb-bounded inputs + under the Montgomery hypothesis scVal a Β· scVal b < 2^260Β·β„“ (canonical + inputs always satisfy it), the transpiled `Scalar52::mul` denotes + ⟦a⟧·⟦b⟧ in ZMod β„“, with a 52-bit-bounded limb representation. -/ +theorem mul_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) + (hcab : scVal a * scVal b < 2^260 * Ell) : + backend.serial.u64.scalar.Scalar52.mul a b + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + 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.mul + -- ── columns of aΒ·b ── + apply spec_bind (mul_internal_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 ha hb + ⟨hA0, hA1, hA2, hA3, hA4, hB0, hB1, hB2, hB3, hB4⟩) + rintro zz ⟨z0, z1, z2, z3, z4, z5, z6, z7, z8, hzl, + hz0e, hz1e, hz2e, hz3e, hz4e, hz5e, hz6e, hz7e, hz8e⟩ + show (do + let ab ← backend.serial.u64.scalar.Scalar52.montgomery_reduce zz + let a2 ← backend.serial.u64.scalar.Scalar52.mul_internal ab + backend.serial.u64.constants.RR + backend.serial.u64.scalar.Scalar52.montgomery_reduce a2) + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + scDenote r = scDenote a * scDenote b ⦄ + -- column bounds and the column value identity + have hzb0 : z0.val < 2^107 := by + have := col_bound hA0 hB0; omega + have hzb1 : z1.val < 2^107 := by + have := col_bound hA0 hB1; have := col_bound hA1 hB0; omega + have hzb2 : z2.val < 2^107 := by + have := col_bound hA0 hB2; have := col_bound hA1 hB1 + have := col_bound hA2 hB0; omega + have hzb3 : z3.val < 2^107 := by + have := col_bound hA0 hB3; have := col_bound hA1 hB2 + have := col_bound hA2 hB1; have := col_bound hA3 hB0; omega + have hzb4 : z4.val < 2^107 := by + have := col_bound hA0 hB4; have := col_bound hA1 hB3 + have := col_bound hA2 hB2; have := col_bound hA3 hB1 + have := col_bound hA4 hB0; omega + have hzb5 : z5.val < 2^107 := by + have := col_bound hA1 hB4; have := col_bound hA2 hB3 + have := col_bound hA3 hB2; have := col_bound hA4 hB1; omega + have hzb6 : z6.val < 2^107 := by + have := col_bound hA2 hB4; have := col_bound hA3 hB3 + have := col_bound hA4 hB2; omega + have hzb7 : z7.val < 2^107 := by + have := col_bound hA3 hB4; have := col_bound hA4 hB3; omega + have hzb8 : z8.val < 2^107 := by + have := col_bound hA4 hB4; omega + have hZval : z0.val + 2^52 * z1.val + 2^104 * z2.val + 2^156 * z3.val + + 2^208 * z4.val + 2^260 * z5.val + 2^312 * z6.val + 2^364 * z7.val + + 2^416 * z8.val = scVal a * scVal b := by + rw [hz0e, hz1e, hz2e, hz3e, hz4e, hz5e, hz6e, hz7e, hz8e, + scVal_eq a a0 a1 a2 a3 a4 ha, scVal_eq b b0 b1 b2 b3 b4 hb] + unfold scLimbs + ring + have hZlt : z0.val + 2^52 * z1.val + 2^104 * z2.val + 2^156 * z3.val + + 2^208 * z4.val + 2^260 * z5.val + 2^312 * z6.val + 2^364 * z7.val + + 2^416 * z8.val < 2^260 * Ell := by rw [hZval]; exact hcab + -- ── first reduction: ⟦ab'⟧·R = aΒ·b ── + apply spec_bind (montgomery_reduce_spec zz z0 z1 z2 z3 z4 z5 z6 z7 z8 hzl + ⟨hzb0, hzb1, hzb2, hzb3, hzb4, hzb5, hzb6, hzb7, hzb8⟩ hZlt) + rintro ab ⟨⟨ab0, ab1, ab2, ab3, ab4, habl, hab0, hab1, hab2, hab3, hab4⟩, habd⟩ + show (do + let a2 ← backend.serial.u64.scalar.Scalar52.mul_internal ab + backend.serial.u64.constants.RR + backend.serial.u64.scalar.Scalar52.montgomery_reduce a2) + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + scDenote r = scDenote a * scDenote b ⦄ + -- RR limb values + have hR0 : (2764609938444603#u64).val = 2764609938444603 := by rfl + have hR1 : (3768881411696287#u64).val = 3768881411696287 := by rfl + have hR2 : (1616719297148420#u64).val = 1616719297148420 := by rfl + have hR3 : (1087343033131391#u64).val = 1087343033131391 := by rfl + have hR4 : (10175238647962#u64).val = 10175238647962 := by rfl + -- ── columns of ab'Β·RR ── + apply spec_bind (mul_internal_spec ab backend.serial.u64.constants.RR + ab0 ab1 ab2 ab3 ab4 + (2764609938444603#u64) (3768881411696287#u64) (1616719297148420#u64) + (1087343033131391#u64) (10175238647962#u64) + habl RR_limbs + ⟨hab0, hab1, hab2, hab3, hab4, + by rw [hR0]; norm_num, by rw [hR1]; norm_num, by rw [hR2]; norm_num, + by rw [hR3]; norm_num, by rw [hR4]; norm_num⟩) + rintro ww ⟨w0, w1, w2, w3, w4, w5, w6, w7, w8, hwl, + hw0e, hw1e, hw2e, hw3e, hw4e, hw5e, hw6e, hw7e, hw8e⟩ + show backend.serial.u64.scalar.Scalar52.montgomery_reduce ww + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + scDenote r = scDenote a * scDenote b ⦄ + simp only [hR0, hR1, hR2, hR3, hR4] at hw0e hw1e hw2e hw3e hw4e hw5e hw6e hw7e hw8e + -- column bounds (RR limbs are literals below 2^52: linear, omega-cheap) + have hwb0 : w0.val < 2^107 := by omega + have hwb1 : w1.val < 2^107 := by omega + have hwb2 : w2.val < 2^107 := by omega + have hwb3 : w3.val < 2^107 := by omega + have hwb4 : w4.val < 2^107 := by omega + have hwb5 : w5.val < 2^107 := by omega + have hwb6 : w6.val < 2^107 := by omega + have hwb7 : w7.val < 2^107 := by omega + have hwb8 : w8.val < 2^107 := by omega + have hsvab : scVal ab = scLimbs ab0 ab1 ab2 ab3 ab4 := + scVal_eq ab ab0 ab1 ab2 ab3 ab4 habl + have hWval : w0.val + 2^52 * w1.val + 2^104 * w2.val + 2^156 * w3.val + + 2^208 * w4.val + 2^260 * w5.val + 2^312 * w6.val + 2^364 * w7.val + + 2^416 * w8.val + = scVal ab + * 4185850391763183796333492317919282507600454137915443218209456916606550724923 := by + rw [hw0e, hw1e, hw2e, hw3e, hw4e, hw5e, hw6e, hw7e, hw8e, hsvab] + unfold scLimbs + ring + have hablt : scVal ab < 2^260 := by + rw [hsvab]; unfold scLimbs; omega + have hWlt : w0.val + 2^52 * w1.val + 2^104 * w2.val + 2^156 * w3.val + + 2^208 * w4.val + 2^260 * w5.val + 2^312 * w6.val + 2^364 * w7.val + + 2^416 * w8.val < 2^260 * Ell := by + rw [hWval] + have hRRE : + (4185850391763183796333492317919282507600454137915443218209456916606550724923 : β„•) + < Ell := by unfold Ell; norm_num + exact Nat.mul_lt_mul'' hablt hRRE + -- ── second reduction and the R-cancellation ── + apply spec_mono (montgomery_reduce_spec ww w0 w1 w2 w3 w4 w5 w6 w7 w8 hwl + ⟨hwb0, hwb1, hwb2, hwb3, hwb4, hwb5, hwb6, hwb7, hwb8⟩ hWlt) + intro r hr + refine ⟨hr.1, ?_⟩ + have hcW := congrArg (Nat.cast (R := ZMod Ell)) hWval + push_cast at hcW + have hcZ := congrArg (Nat.cast (R := ZMod Ell)) hZval + push_cast at hcZ + have hr2 := hr.2 + push_cast at hr2 + have habd2 := habd + push_cast at habd2 + refine R_isUnit.mul_right_cancel ?_ + calc scDenote r * 2^260 = ((scVal ab : β„•) : ZMod Ell) + * ((4185850391763183796333492317919282507600454137915443218209456916606550724923 : β„•) + : ZMod Ell) := by + rw [hr2]; push_cast; linear_combination hcW + _ = ((scVal ab : β„•) : ZMod Ell) * 2^520 := by rw [RR_denote] + _ = (((scVal ab : β„•) : ZMod Ell) * 2^260) * 2^260 := by ring + _ = (((scVal a : β„•) : ZMod Ell) * ((scVal b : β„•) : ZMod Ell)) * 2^260 := by + have hd : ((scVal ab : β„•) : ZMod Ell) * 2^260 + = ((scVal a : β„•) : ZMod Ell) * ((scVal b : β„•) : ZMod Ell) := by + simp only [scDenote] at habd2 + rw [habd2]; linear_combination hcZ + rw [hd] + _ = (scDenote a * scDenote b) * 2^260 := by simp only [scDenote] + +end ScalarProofs diff --git a/verification/Proofs/ScalarMain.lean b/verification/Proofs/ScalarMain.lean new file mode 100644 index 0000000..df29878 --- /dev/null +++ b/verification/Proofs/ScalarMain.lean @@ -0,0 +1,91 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ScalarMain.lean β€” the scalar-layer aggregate certificate. + + Clean-interface corollaries of the assembly proofs, stated through + `ScBnd` (52-bit limb representation) and `scDenote` (⟦·⟧ : Scalar52 β†’ + ZMod β„“), plus the single bundled certificate `scalarImplementation`: + + Β· add: canonical inputs β†’ ⟦add a b⟧ = ⟦a⟧ + ⟦b⟧, ScBnd out + Β· sub: canonical subtrahend β†’ ⟦sub a b⟧ = ⟦a⟧ βˆ’ ⟦b⟧, ScBnd out + Β· mul: Montgomery input bound β†’ ⟦mul a b⟧ = ⟦a⟧ Β· ⟦b⟧, ScBnd out + (canonical inputs satisfy it: β„“Β·β„“ < 2^260Β·β„“) + + Audit: `#print axioms ScalarProofs.scalarImplementation` must report + exactly [propext, Classical.choice, Quot.sound]. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ScalarFullMulSpec +import Proofs.ScalarAddSpec +open Aeneas Aeneas.Std Result +open curve25519_dalek + +set_option linter.unusedSimpArgs false +set_option exponentiation.threshold 600 + +namespace ScalarProofs + +open Aeneas.Std.WP + +/-- Addition, clean interface. -/ +theorem scalar_add_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b) + (hca : scVal a < Ell) (hcb : scVal b < Ell) : + backend.serial.u64.scalar.Scalar52.add a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a + scDenote b ⦄ := by + obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha + obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb + apply spec_mono (add_val_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl + ⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hca hcb) + intro r hr + exact ⟨hr.1, hr.2⟩ + +/-- Subtraction, clean interface. -/ +theorem scalar_sub_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b) + (hcb : scVal b ≀ Ell) : + backend.serial.u64.scalar.Scalar52.sub a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a - scDenote b ⦄ := by + obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha + obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb + apply spec_mono (sub_val_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl + ⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hcb) + intro r hr + exact ⟨hr.1, hr.2⟩ + +/-- Multiplication, clean interface. The Montgomery hypothesis + scVal a Β· scVal b < 2^260Β·β„“ holds in particular for canonical inputs. -/ +theorem scalar_mul_correct (a b : Sc) (ha : ScBnd a) (hb : ScBnd b) + (hm : scVal a * scVal b < 2^260 * Ell) : + backend.serial.u64.scalar.Scalar52.mul a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a * scDenote b ⦄ := by + obtain ⟨a0, a1, a2, a3, a4, hal, hA0, hA1, hA2, hA3, hA4⟩ := ha + obtain ⟨b0, b1, b2, b3, b4, hbl, hB0, hB1, hB2, hB3, hB4⟩ := hb + apply spec_mono (mul_spec a b a0 a1 a2 a3 a4 b0 b1 b2 b3 b4 hal hbl + ⟨hA0, hA1, hA2, hA3, hA4⟩ ⟨hB0, hB1, hB2, hB3, hB4⟩ hm) + intro r hr + exact ⟨hr.1, hr.2⟩ + +/-- Canonical inputs always satisfy the Montgomery multiplication bound. -/ +theorem canonical_mul_bound {a b : Sc} (hca : scVal a < Ell) (hcb : scVal b < Ell) : + scVal a * scVal b < 2^260 * Ell := by + have h1 : scVal a * scVal b < Ell * Ell := Nat.mul_lt_mul'' hca hcb + have h2 : Ell * Ell ≀ 2^260 * Ell := + Nat.mul_le_mul_right Ell (by unfold Ell; norm_num) + exact lt_of_lt_of_le h1 h2 + +/-- **The scalar-layer certificate**: the transpiled `Scalar52` add, sub + and mul all denote the ring operations of ZMod β„“ on canonical inputs, + with 52-bit-bounded limb output. One theorem, one axiom audit. -/ +theorem scalarImplementation : + (βˆ€ a b : Sc, ScBnd a β†’ ScBnd b β†’ scVal a < Ell β†’ scVal b < Ell β†’ + backend.serial.u64.scalar.Scalar52.add a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a + scDenote b ⦄) ∧ + (βˆ€ a b : Sc, ScBnd a β†’ ScBnd b β†’ scVal b ≀ Ell β†’ + backend.serial.u64.scalar.Scalar52.sub a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a - scDenote b ⦄) ∧ + (βˆ€ a b : Sc, ScBnd a β†’ ScBnd b β†’ scVal a < Ell β†’ scVal b < Ell β†’ + backend.serial.u64.scalar.Scalar52.mul a b + ⦃ r => ScBnd r ∧ scDenote r = scDenote a * scDenote b ⦄) := + ⟨fun a b ha hb hca hcb => scalar_add_correct a b ha hb hca hcb, + fun a b ha hb hcb => scalar_sub_correct a b ha hb hcb, + fun a b ha hb hca hcb => + scalar_mul_correct a b ha hb (canonical_mul_bound hca hcb)⟩ + +end ScalarProofs diff --git a/verification/Proofs/ScalarMontSpec.lean b/verification/Proofs/ScalarMontSpec.lean new file mode 100644 index 0000000..b2d997e --- /dev/null +++ b/verification/Proofs/ScalarMontSpec.lean @@ -0,0 +1,387 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ScalarMontSpec.lean β€” Scalar52 Montgomery reduction (phase B) and + the full multiplication `Scalar52::mul` (phase C). + + `montgomery_reduce z` folds a 9-limb double-width value Z = Ξ£ z_kΒ·2^52k + down by R = 2^260: five `part1` rounds pick nonce digits n_k with + (sum + n_kΒ·Lβ‚€) ≑ 0 (mod 2^52) β€” exact division, nothing is shifted out β€” + and four `part2` rounds split exactly. Telescoping the nine round + equations gives scLimbs r Β· 2^260 = Z + NΒ·β„“ with N = Ξ£ n_kΒ·2^52k, + so in ZMod β„“: ⟦r⟧ Β· 2^260 = Z. The final canonicalization is the + already-proven `sub r L` (⟦L⟧ = 0). + + The arithmetic heart is the constant identity + LFACTOR Β· Lβ‚€ ≑ βˆ’1 (mod 2^52), + 1439961107955227 Β· 671914833335277 + 1 = 214835089243030 Β· 2^52, + kernel-checked by norm_num (`mont_key`). + + `mul a b` then composes: montgomery_reduce (mul_internal a b) gives + ⟦ab⟧·R⁻¹; a second round against RR ≑ RΒ² (mod β„“) multiplies R back in: + ⟦mul a b⟧ = ⟦a⟧·⟦b⟧. The first reduction needs the honest Montgomery + hypothesis scVal a Β· scVal b < 2^260Β·β„“ (callers with canonical + scalars satisfy it: β„“Β² < 2^260Β·β„“); the second is unconditional because + scVal RR < β„“. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ScalarSubSpec +import Proofs.ScalarMulSpec +open Aeneas Aeneas.Std Result +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false +set_option exponentiation.threshold 600 + +namespace ScalarProofs + +open Aeneas.Std.WP + +/-! ### The Montgomery constant identity -/ + +/-- The transpiled `constants::LFACTOR` value. -/ +theorem LFACTOR_val : backend.serial.u64.constants.LFACTOR.val = 1439961107955227 := by + unfold backend.serial.u64.constants.LFACTOR; rfl + +/-- **The defining property of LFACTOR**: LFACTORΒ·Lβ‚€ ≑ βˆ’1 (mod 2^52), + stated as an exact β„• identity. Kernel-checked literal arithmetic. -/ +theorem mont_key : (1:β„•) + 1439961107955227 * 671914833335277 = 214835089243030 * 2^52 := by + norm_num + +/-- **Montgomery cancellation**: with the nonce p = (sΒ·LFACTOR) mod 2^52, + the sum s + pΒ·Lβ‚€ has zero low 52 bits β€” `part1`'s shift is an exact + division. -/ +theorem mont_cancel (s p : β„•) (hp : p = (s * 1439961107955227) % 2^52) : + (s + p * 671914833335277) % 2^52 = 0 := by + have hmod : p ≑ s * 1439961107955227 [MOD 2^52] := hp β–Έ (Nat.mod_modEq _ _) + have h1 : s + p * 671914833335277 + ≑ s + s * 1439961107955227 * 671914833335277 [MOD 2^52] := + Nat.ModEq.add_left s (hmod.mul_right _) + have h2 : s + s * 1439961107955227 * 671914833335277 + = s * 214835089243030 * 2^52 := by + calc s + s * 1439961107955227 * 671914833335277 + = s * (1 + 1439961107955227 * 671914833335277) := by ring + _ = s * (214835089243030 * 2^52) := by rw [mont_key] + _ = s * 214835089243030 * 2^52 := by ring + calc (s + p * 671914833335277) % 2^52 + = (s + s * 1439961107955227 * 671914833335277) % 2^52 := h1 + _ = 0 := by rw [h2]; exact Nat.mul_mod_left _ _ + +/-! ### The two round helpers -/ + +/-- **`part2` splits exactly**: carryΒ·2^52 + w = sum, w < 2^52 + (scalar.rs:273-276 β€” mask and shift, nothing lost). -/ +theorem part2_spec (sum : U128) : + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 sum + ⦃ cw => cw.2.val < 2^52 ∧ cw.1.val * 2^52 + cw.2.val = sum.val ⦄ := by + unfold backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 + step with UScalar.cast.step_spec as ⟨i, hi⟩ + have hiv : i.val = sum.val % 2^64 := by + simp [hi, UScalar.cast_val_eq, U64.size, U128.size] + step as ⟨i1, hi1⟩ + step as ⟨i2, hi2⟩ + have hi2v : i2.val = 2^52 - 1 := by + simp [hi2, hi1, U64.size_def, U64.numBits] + step as ⟨w, hw⟩ + have hwv : w.val = sum.val % 2^52 := by + rw [hw, UScalar.val_and, hi2v, nat_and_mask52, hiv, + Nat.mod_mod_of_dvd sum.val (by norm_num : (2:β„•)^52 ∣ 2^64)] + step as ⟨i3, hi3⟩ + have hi3v : i3.val = sum.val / 2^52 := by + rw [hi3, Nat.shiftRight_eq_div_pow] + try simp only [spec_ok] + constructor + Β· rw [hwv]; exact Nat.mod_lt _ (by norm_num) + Β· rw [hi3v, hwv]; omega + +/-- **`part1` divides exactly** (scalar.rs:268-271): the nonce digit + p = (sumΒ·LFACTOR) & mask52 makes sum + pΒ·Lβ‚€ divisible by 2^52 + (`mont_cancel`), so the shifted carry satisfies the *equation* + carryΒ·2^52 = sum + pΒ·Lβ‚€ β€” no information is discarded. The sum bound + keeps the internal u128 addition from overflowing. -/ +theorem part1_spec (sum : U128) (hs : sum.val < 2^124) : + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 sum + ⦃ cw => cw.2.val < 2^52 ∧ + cw.1.val * 2^52 = sum.val + cw.2.val * 671914833335277 ⦄ := by + unfold backend.serial.u64.scalar.Scalar52.montgomery_reduce.part1 + backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index + step with UScalar.cast.step_spec as ⟨i, hi⟩ + have hiv : i.val = sum.val % 2^64 := by + simp [hi, UScalar.cast_val_eq, U64.size, U128.size] + step as ⟨i1, hi1⟩ + have hsz : UScalar.size UScalarTy.U64 = 2^64 := by scalar_tac + have hi1v : i1.val = sum.val * 1439961107955227 % 2^64 := by + rw [hi1] + simp only [core.num.U64.wrapping_mul, UScalar.wrapping_mul_val_eq] + rw [hiv, LFACTOR_val, hsz] + exact Nat.mod_mul_mod .. + step as ⟨i2, hi2⟩ + step as ⟨i3, hi3⟩ + have hi3v : i3.val = 2^52 - 1 := by + simp [hi3, hi2, U64.size_def, U64.numBits] + step as ⟨p, hp⟩ + have hpv : p.val = (sum.val * 1439961107955227) % 2^52 := by + rw [hp, UScalar.val_and, hi3v, nat_and_mask52, hi1v, + Nat.mod_mod_of_dvd _ (by norm_num : (2:β„•)^52 ∣ 2^64)] + have hpb : p.val < 2^52 := by rw [hpv]; exact Nat.mod_lt _ (by norm_num) + step as ⟨i4, hi4⟩ + try simp [L_limbs] at hi4 + have hi4v : i4.val = 671914833335277 := by rw [hi4]; rfl + step with m_spec as ⟨i5, hi5⟩ + have hi5v : i5.val = p.val * 671914833335277 := by rw [hi5, hi4v] + have hi5b : i5.val < 2^102 := by + rw [hi5v] + calc p.val * 671914833335277 < 2^52 * 671914833335277 := + Nat.mul_lt_mul_of_lt_of_le hpb (le_refl _) (by norm_num) + _ < 2^102 := by norm_num + step as ⟨i6, hi6⟩ + have hi6v : i6.val = sum.val + p.val * 671914833335277 := by + rw [hi6, hi5v] + step as ⟨i7, hi7⟩ + have hdvd : (sum.val + p.val * 671914833335277) % 2^52 = 0 := + mont_cancel sum.val p.val hpv + have hi7v : i7.val * 2^52 = sum.val + p.val * 671914833335277 := by + rw [hi7, Nat.shiftRight_eq_div_pow, hi6v] + omega + try simp only [spec_ok] + exact ⟨hpb, hi7v⟩ + +/-! ### The two value telescopes -/ + +/-- **Head telescope**: the five exact-division rounds E0–E4, weighted + 1, 2^52, …, 2^208 and summed, eliminate the carries c0–c3 and give + the full Montgomery identity with the round-5..8 input state Xβ€² on + the left: Xβ€²Β·2^260 = Z + NΒ·β„“. One `linear_combination` certificate + (verified numerically over random traces before formalization). -/ +theorem mont_head_telescope + (z0 z1 z2 z3 z4 z5 z6 z7 z8 n0 n1 n2 n3 n4 c0 c1 c2 c3 c4 : β„•) + (e0 : c0 * 2^52 = z0 + n0 * 671914833335277) + (e1 : c1 * 2^52 = c0 + z1 + n0 * 3916664325105025 + n1 * 671914833335277) + (e2 : c2 * 2^52 = c1 + z2 + n0 * 1367801 + n1 * 3916664325105025 + n2 * 671914833335277) + (e3 : c3 * 2^52 = c2 + z3 + n1 * 1367801 + n2 * 3916664325105025 + n3 * 671914833335277) + (e4 : c4 * 2^52 = c3 + z4 + n0 * 17592186044416 + n2 * 1367801 + n3 * 3916664325105025 + n4 * 671914833335277) : + ((c4 + z5 + n1 * 17592186044416 + n3 * 1367801 + n4 * 3916664325105025) + 2^52 * (z6 + n2 * 17592186044416 + n4 * 1367801) + 2^104 * (z7 + n3 * 17592186044416) + 2^156 * (z8 + n4 * 17592186044416)) * 2^260 + = (z0 + 2^52 * z1 + 2^104 * z2 + 2^156 * z3 + 2^208 * z4 + 2^260 * z5 + 2^312 * z6 + 2^364 * z7 + 2^416 * z8) + + (n0 + 2^52 * n1 + 2^104 * n2 + 2^156 * n3 + 2^208 * n4) * Ell := by + unfold Ell + linear_combination (e0 : (c0 * 2^52 : β„•) = _) + 2^52 * e1 + 2^104 * e2 + + 2^156 * e3 + 2^208 * e4 + +/-- **Tail telescope**: the four exact-split rounds E5–E8, weighted + 1, 2^52, 2^104, 2^156, cancel c5–c7 and reassemble the input state: + the result limbs plus top carry equal Xβ€² exactly. -/ +theorem mont_tail_telescope + (z5 z6 z7 z8 n1 n2 n3 n4 c4 c5 c6 c7 c8 r0 r1 r2 r3 : β„•) + (e5 : c5 * 2^52 + r0 = c4 + z5 + n1 * 17592186044416 + n3 * 1367801 + n4 * 3916664325105025) + (e6 : c6 * 2^52 + r1 = c5 + z6 + n2 * 17592186044416 + n4 * 1367801) + (e7 : c7 * 2^52 + r2 = c6 + z7 + n3 * 17592186044416) + (e8 : c8 * 2^52 + r3 = c7 + z8 + n4 * 17592186044416) : + r0 + 2^52 * r1 + 2^104 * r2 + 2^156 * r3 + 2^208 * c8 + = (c4 + z5 + n1 * 17592186044416 + n3 * 1367801 + n4 * 3916664325105025) + 2^52 * (z6 + n2 * 17592186044416 + n4 * 1367801) + 2^104 * (z7 + n3 * 17592186044416) + 2^156 * (z8 + n4 * 17592186044416) := by + linear_combination (e5 : (c5 * 2^52 + r0 : β„•) = _) + 2^52 * e6 + + 2^104 * e7 + 2^156 * e8 + +/-- The standard Montgomery output bound: Z < RΒ·β„“ and N < R force the + pre-canonical result below 2β„“. Atomic in `Ell` throughout. -/ +theorem mont_bound (X N Z : β„•) (hT : X * 2^260 = Z + N * Ell) + (hZ : Z < 2^260 * Ell) (hN : N < 2^260) : X < 2 * Ell := by + have h1 : N * Ell ≀ (2^260 - 1) * Ell := + Nat.mul_le_mul_right Ell (by omega) + have h3 : 2^260 * X < 2^260 * (2 * Ell) := by + calc 2^260 * X = X * 2^260 := Nat.mul_comm _ _ + _ = Z + N * Ell := hT + _ ≀ Z + (2^260 - 1) * Ell := Nat.add_le_add_left h1 Z + _ < 2^260 * Ell + (2^260 - 1) * Ell := Nat.add_lt_add_right hZ _ + _ ≀ 2^260 * (2 * Ell) := by + have he : (2:β„•)^260 * Ell + (2^260 - 1) * Ell + = (2^260 + (2^260 - 1)) * Ell := by ring + rw [he] + have h2 : (2:β„•)^260 + (2^260 - 1) ≀ 2^261 := by norm_num + calc ((2:β„•)^260 + (2^260 - 1)) * Ell ≀ 2^261 * Ell := + Nat.mul_le_mul_right Ell h2 + _ = 2^260 * (2 * Ell) := by ring + exact Nat.lt_of_mul_lt_mul_left h3 + +/-! ### The walk, split at the round-4/round-5 boundary (METHOD 4: the + 74-step monolith exceeds the elaboration budget; each half is a + `mul_internal`-sized walk) -/ + +/-- **Tail of the reduction** (rounds 5–8 + canonicalization): from the + mid-state (carry4, n1..n4) and limbs 5..8, the four `part2` rounds + produce limbs summing (with the top carry) to exactly the mid-state + value Xβ€²; the trailing `sub _ L` subtracts ⟦L⟧ = 0. The hypothesis + Xβ€² < 2β„“ (provided by `mont_head_telescope` + `mont_bound` at the + call site) keeps the top carry below 2^52 for the sub. -/ +theorem mont_tail_spec (limbs : Std.Array Std.U128 9#usize) + (z0 z1 z2 z3 z4 z5 z6 z7 z8 : Std.U128) (carry4 : Std.U128) + (n1 n2 n3 n4 i3 i8 i21 : U64) + (hl : (↑limbs : List Std.U128) = [z0, z1, z2, z3, z4, z5, z6, z7, z8]) + (hvi3 : i3.val = 3916664325105025) (hvi8 : i8.val = 1367801) (hvi21 : i21.val = 17592186044416) + (hcb4 : carry4.val < 2^62) + (hnb : n1.val < 2^52 ∧ n2.val < 2^52 ∧ n3.val < 2^52 ∧ n4.val < 2^52) + (hzb : z5.val < 2^107 ∧ z6.val < 2^107 ∧ z7.val < 2^107 ∧ z8.val < 2^107) + (hX : (carry4.val + z5.val + n1.val * 17592186044416 + n3.val * 1367801 + n4.val * 3916664325105025) + 2^52 * (z6.val + n2.val * 17592186044416 + n4.val * 1367801) + 2^104 * (z7.val + n3.val * 17592186044416) + 2^156 * (z8.val + n4.val * 17592186044416) < 2 * Ell) : + (do + let i28 ← Array.index_usize limbs 5#usize + let i29 ← carry4 + i28 + let i30 ← backend.serial.u64.scalar.m n1 i21 + let i31 ← i29 + i30 + let i32 ← backend.serial.u64.scalar.m n3 i8 + let i33 ← i31 + i32 + let i34 ← backend.serial.u64.scalar.m n4 i3 + let i35 ← i33 + i34 + let (carry5, r0) ← + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i35 + let i36 ← Array.index_usize limbs 6#usize + let i37 ← carry5 + i36 + let i38 ← backend.serial.u64.scalar.m n2 i21 + let i39 ← i37 + i38 + let i40 ← backend.serial.u64.scalar.m n4 i8 + let i41 ← i39 + i40 + let (carry6, r1) ← + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i41 + let i42 ← Array.index_usize limbs 7#usize + let i43 ← carry6 + i42 + let i44 ← backend.serial.u64.scalar.m n3 i21 + let i45 ← i43 + i44 + let (carry7, r2) ← + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i45 + let i46 ← Array.index_usize limbs 8#usize + let i47 ← carry7 + i46 + let i48 ← backend.serial.u64.scalar.m n4 i21 + let i49 ← i47 + i48 + let (carry8, r3) ← + backend.serial.u64.scalar.Scalar52.montgomery_reduce.part2 i49 + let r4 ← lift (UScalar.cast .U64 carry8) + backend.serial.u64.scalar.Scalar52.sub + (Array.make 5#usize [ r0, r1, r2, r3, r4 ]) + backend.serial.u64.constants.L) + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + scDenote r = (((carry4.val + z5.val + n1.val * 17592186044416 + n3.val * 1367801 + n4.val * 3916664325105025) + 2^52 * (z6.val + n2.val * 17592186044416 + n4.val * 1367801) + 2^104 * (z7.val + n3.val * 17592186044416) + 2^156 * (z8.val + n4.val * 17592186044416) : β„•) : ZMod Ell) ⦄ := by + obtain ⟨hn1b, hn2b, hn3b, hn4b⟩ := hnb + obtain ⟨hz5, hz6, hz7, hz8⟩ := hzb + step as ⟨i28, hi28⟩ + simp [hl] at hi28 + have hvi28 : i28.val = z5.val := by rw [hi28] + have hsi29 : carry4.val + i28.val < 2^128 := by omega + step as ⟨i29, hi29⟩ + have hvi29 : i29.val = carry4.val + i28.val := by rw [hi29] + have hbi29 : i29.val < 2^110 := by omega + step with m_spec as ⟨i30, hi30⟩ + have hvi30 : i30.val = n1.val * 17592186044416 := by rw [hi30, hvi21] + have hbi30 : i30.val < 2^104 := by rw [hvi30]; omega + have hsi31 : i29.val + i30.val < 2^128 := by omega + step as ⟨i31, hi31⟩ + have hvi31 : i31.val = i29.val + i30.val := by rw [hi31] + have hbi31 : i31.val < 2^112 := by omega + step with m_spec as ⟨i32, hi32⟩ + have hvi32 : i32.val = n3.val * 1367801 := by rw [hi32, hvi8] + have hbi32 : i32.val < 2^104 := by rw [hvi32]; omega + have hsi33 : i31.val + i32.val < 2^128 := by omega + step as ⟨i33, hi33⟩ + have hvi33 : i33.val = i31.val + i32.val := by rw [hi33] + have hbi33 : i33.val < 2^113 := by omega + step with m_spec as ⟨i34, hi34⟩ + have hvi34 : i34.val = n4.val * 3916664325105025 := by rw [hi34, hvi3] + have hbi34 : i34.val < 2^104 := by rw [hvi34]; omega + have hsi35 : i33.val + i34.val < 2^128 := by omega + step as ⟨i35, hi35⟩ + have hvi35 : i35.val = i33.val + i34.val := by rw [hi35] + have hbi35 : i35.val < 2^114 := by omega + step with (part2_spec i35) as ⟨carry5, r0, hr0b, hE5⟩ + rw [hvi35, hvi33, hvi31, hvi29, hvi28, hvi30, hvi32, hvi34] at hE5 + have hcb5 : carry5.val < 2^62 := by omega + step as ⟨i36, hi36⟩ + simp [hl] at hi36 + have hvi36 : i36.val = z6.val := by rw [hi36] + have hsi37 : carry5.val + i36.val < 2^128 := by omega + step as ⟨i37, hi37⟩ + have hvi37 : i37.val = carry5.val + i36.val := by rw [hi37] + have hbi37 : i37.val < 2^110 := by omega + step with m_spec as ⟨i38, hi38⟩ + have hvi38 : i38.val = n2.val * 17592186044416 := by rw [hi38, hvi21] + have hbi38 : i38.val < 2^104 := by rw [hvi38]; omega + have hsi39 : i37.val + i38.val < 2^128 := by omega + step as ⟨i39, hi39⟩ + have hvi39 : i39.val = i37.val + i38.val := by rw [hi39] + have hbi39 : i39.val < 2^112 := by omega + step with m_spec as ⟨i40, hi40⟩ + have hvi40 : i40.val = n4.val * 1367801 := by rw [hi40, hvi8] + have hbi40 : i40.val < 2^104 := by rw [hvi40]; omega + have hsi41 : i39.val + i40.val < 2^128 := by omega + step as ⟨i41, hi41⟩ + have hvi41 : i41.val = i39.val + i40.val := by rw [hi41] + have hbi41 : i41.val < 2^113 := by omega + step with (part2_spec i41) as ⟨carry6, r1, hr1b, hE6⟩ + rw [hvi41, hvi39, hvi37, hvi36, hvi38, hvi40] at hE6 + have hcb6 : carry6.val < 2^62 := by omega + step as ⟨i42, hi42⟩ + simp [hl] at hi42 + have hvi42 : i42.val = z7.val := by rw [hi42] + have hsi43 : carry6.val + i42.val < 2^128 := by omega + step as ⟨i43, hi43⟩ + have hvi43 : i43.val = carry6.val + i42.val := by rw [hi43] + have hbi43 : i43.val < 2^110 := by omega + step with m_spec as ⟨i44, hi44⟩ + have hvi44 : i44.val = n3.val * 17592186044416 := by rw [hi44, hvi21] + have hbi44 : i44.val < 2^104 := by rw [hvi44]; omega + have hsi45 : i43.val + i44.val < 2^128 := by omega + step as ⟨i45, hi45⟩ + have hvi45 : i45.val = i43.val + i44.val := by rw [hi45] + have hbi45 : i45.val < 2^112 := by omega + step with (part2_spec i45) as ⟨carry7, r2, hr2b, hE7⟩ + rw [hvi45, hvi43, hvi42, hvi44] at hE7 + have hcb7 : carry7.val < 2^62 := by omega + step as ⟨i46, hi46⟩ + simp [hl] at hi46 + have hvi46 : i46.val = z8.val := by rw [hi46] + have hsi47 : carry7.val + i46.val < 2^128 := by omega + step as ⟨i47, hi47⟩ + have hvi47 : i47.val = carry7.val + i46.val := by rw [hi47] + have hbi47 : i47.val < 2^110 := by omega + step with m_spec as ⟨i48, hi48⟩ + have hvi48 : i48.val = n4.val * 17592186044416 := by rw [hi48, hvi21] + have hbi48 : i48.val < 2^104 := by rw [hvi48]; omega + have hsi49 : i47.val + i48.val < 2^128 := by omega + step as ⟨i49, hi49⟩ + have hvi49 : i49.val = i47.val + i48.val := by rw [hi49] + have hbi49 : i49.val < 2^112 := by omega + step with (part2_spec i49) as ⟨carry8, r3, hr3b, hE8⟩ + rw [hvi49, hvi47, hvi46, hvi48] at hE8 + + -- reassemble the mid-state value and bound the top carry + have hTt := mont_tail_telescope z5.val z6.val z7.val z8.val + n1.val n2.val n3.val n4.val carry4.val carry5.val carry6.val carry7.val + carry8.val r0.val r1.val r2.val r3.val hE5 hE6 hE7 hE8 + have hEll254 : 2 * Ell < 2^254 := by unfold Ell; norm_num + have hc8b : carry8.val < 2^46 := by omega + step with UScalar.cast.step_spec as ⟨r4, hr4⟩ + have hr4v : r4.val = carry8.val := by + rw [hr4, UScalar.cast_val_eq] + simp only [UScalarTy.U64, UScalarTy.numBits] + omega + have hr4b : r4.val < 2^52 := by omega + + -- canonicalize: sub _ L with ⟦L⟧ = 0 + have hmk : ((↑(Array.make 5#usize [r0, r1, r2, r3, r4])) : List U64) + = [r0, r1, r2, r3, r4] := by simp [Array.make] + apply spec_mono (sub_val_spec _ backend.serial.u64.constants.L + r0 r1 r2 r3 r4 _ _ _ _ _ hmk L_limbs + ⟨hr0b, hr1b, hr2b, hr3b, hr4b⟩ + (by refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> norm_num) + (by rw [L_val])) + intro r hr + refine ⟨hr.1, ?_⟩ + rw [hr.2] + have hEz : (Ell : ZMod Ell) = 0 := ZMod.natCast_self Ell + have hL0 : scDenote backend.serial.u64.constants.L = 0 := by + simp only [scDenote, L_val]; exact hEz + rw [hL0, sub_zero] + have hpre : scVal (Array.make 5#usize [r0, r1, r2, r3, r4]) + = scLimbs r0 r1 r2 r3 r4 := scVal_eq _ _ _ _ _ _ hmk + simp only [scDenote, hpre] + unfold scLimbs + rw [hr4v] + exact congrArg (Nat.cast (R := ZMod Ell)) hTt + +end ScalarProofs diff --git a/verification/Proofs/ScalarMulSpec.lean b/verification/Proofs/ScalarMulSpec.lean new file mode 100644 index 0000000..1b73c69 --- /dev/null +++ b/verification/Proofs/ScalarMulSpec.lean @@ -0,0 +1,275 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ScalarMulSpec.lean β€” Scalar52 multiplication, phase A: mul_internal + + `mul_internal a b` computes the nine schoolbook column sums + z_k = Ξ£_(i+j=k) a_iΒ·b_j into u128 words (scalar.rs:222-236) β€” no carries, + no reduction; those happen in montgomery_reduce (phase B, open frontier). + This file proves the columns exact and bounded: each product < 2^104 + (52+52 bits), each column < 5Β·2^104 < 2^107. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ScalarDenote +open Aeneas Aeneas.Std Result +open curve25519_dalek + +set_option maxHeartbeats 8000000 +set_option linter.unusedSimpArgs false + +namespace ScalarProofs + +open Aeneas.Std.WP + +/-- The widening 52Γ—52β†’104-bit product helper `m` (scalar.rs:56-58): + total, value exact (u64β†’u128 casts cannot truncate; the product of two + 64-bit values cannot overflow u128). -/ +theorem m_spec (x y : U64) : + backend.serial.u64.scalar.m x y ⦃ r => r.val = x.val * y.val ⦄ := by + unfold backend.serial.u64.scalar.m + step with UScalar.cast.step_spec as ⟨cx, hcx⟩ + step with UScalar.cast.step_spec as ⟨cy, hcy⟩ + have hcxv : cx.val = x.val := by + simp [hcx, UScalar.cast_val_eq, U64.size, U128.size] + have hcyv : cy.val = y.val := by + simp [hcy, UScalar.cast_val_eq, U64.size, U128.size] + have hfits : cx.val * cy.val ≀ U128.max := by + rw [hcxv, hcyv] + have hx := x.hBounds + have hy := y.hBounds + have h2 : x.val * y.val < 2^64 * 2^64 := by + apply Nat.mul_lt_mul'' <;> scalar_tac + scalar_tac + step as ⟨r, hr⟩ + try simp only [spec_ok] + rw [hr, hcxv, hcyv] + +/-- `mul_internal`: the nine exact schoolbook columns, each bounded. + For 52-bit-bounded inputs no operation can overflow. -/ +theorem mul_internal_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]) + (hbnd : a0.val < 2^52 ∧ a1.val < 2^52 ∧ a2.val < 2^52 ∧ a3.val < 2^52 ∧ a4.val < 2^52 ∧ + b0.val < 2^52 ∧ b1.val < 2^52 ∧ b2.val < 2^52 ∧ b3.val < 2^52 ∧ b4.val < 2^52) : + backend.serial.u64.scalar.Scalar52.mul_internal a b + ⦃ (zz : Std.Array Std.U128 9#usize) => βˆƒ z0 z1 z2 z3 z4 z5 z6 z7 z8 : Std.U128, + (↑zz : List Std.U128) = [z0, z1, z2, z3, z4, z5, z6, z7, z8] ∧ + z0.val = (a0.val * b0.val) ∧ + z1.val = ((a0.val * b1.val) + (a1.val * b0.val)) ∧ + z2.val = (((a0.val * b2.val) + (a1.val * b1.val)) + (a2.val * b0.val)) ∧ + z3.val = ((((a0.val * b3.val) + (a1.val * b2.val)) + (a2.val * b1.val)) + (a3.val * b0.val)) ∧ + z4.val = (((((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val)) + (a3.val * b1.val)) + (a4.val * b0.val)) ∧ + z5.val = ((((a1.val * b4.val) + (a2.val * b3.val)) + (a3.val * b2.val)) + (a4.val * b1.val)) ∧ + z6.val = (((a2.val * b4.val) + (a3.val * b3.val)) + (a4.val * b2.val)) ∧ + z7.val = ((a3.val * b4.val) + (a4.val * b3.val)) ∧ + z8.val = (a4.val * b4.val) ⦄ := by + obtain ⟨hA0, hA1, hA2, hA3, hA4, hB0, hB1, hB2, hB3, hB4⟩ := hbnd + unfold backend.serial.u64.scalar.Scalar52.mul_internal + backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index + step as ⟨i, hi⟩ + simp [ha] at hi + have hvi : i.val = a0.val := by rw [hi] + step as ⟨i1, hi1⟩ + simp [hb] at hi1 + have hvi1 : i1.val = b0.val := by rw [hi1] + step with m_spec as ⟨i2, hi2⟩ + have hvi2 : i2.val = a0.val * b0.val := by rw [hi2, hvi, hvi1] + have hbi2 : a0.val * b0.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA0 hB0; omega + step as ⟨z1, hz1⟩ + step as ⟨i3, hi3⟩ + simp [hb] at hi3 + have hvi3 : i3.val = b1.val := by rw [hi3] + step with m_spec as ⟨i4, hi4⟩ + have hvi4 : i4.val = a0.val * b1.val := by rw [hi4, hvi, hvi3] + have hbi4 : a0.val * b1.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA0 hB1; omega + step as ⟨i5, hi5⟩ + simp [ha] at hi5 + have hvi5 : i5.val = a1.val := by rw [hi5] + step with m_spec as ⟨i6, hi6⟩ + have hvi6 : i6.val = a1.val * b0.val := by rw [hi6, hvi5, hvi1] + have hbi6 : a1.val * b0.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA1 hB0; omega + have hsi7 : i4.val + i6.val < 2^128 := by rw [hvi4, hvi6]; omega + step as ⟨i7, hi7⟩ + have hvi7 : i7.val = (a0.val * b1.val) + (a1.val * b0.val) := by rw [hi7, hvi4, hvi6] + have hbi7 : (a0.val * b1.val) + (a1.val * b0.val) < 2^107 := by omega + step as ⟨z2, hz2⟩ + step as ⟨i8, hi8⟩ + simp [hb] at hi8 + have hvi8 : i8.val = b2.val := by rw [hi8] + step with m_spec as ⟨i9, hi9⟩ + have hvi9 : i9.val = a0.val * b2.val := by rw [hi9, hvi, hvi8] + have hbi9 : a0.val * b2.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA0 hB2; omega + step with m_spec as ⟨i10, hi10⟩ + have hvi10 : i10.val = a1.val * b1.val := by rw [hi10, hvi5, hvi3] + have hbi10 : a1.val * b1.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA1 hB1; omega + have hsi11 : i9.val + i10.val < 2^128 := by rw [hvi9, hvi10]; omega + step as ⟨i11, hi11⟩ + have hvi11 : i11.val = (a0.val * b2.val) + (a1.val * b1.val) := by rw [hi11, hvi9, hvi10] + have hbi11 : (a0.val * b2.val) + (a1.val * b1.val) < 2^107 := by omega + step as ⟨i12, hi12⟩ + simp [ha] at hi12 + have hvi12 : i12.val = a2.val := by rw [hi12] + step with m_spec as ⟨i13, hi13⟩ + have hvi13 : i13.val = a2.val * b0.val := by rw [hi13, hvi12, hvi1] + have hbi13 : a2.val * b0.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA2 hB0; omega + have hsi14 : i11.val + i13.val < 2^128 := by rw [hvi11, hvi13]; omega + step as ⟨i14, hi14⟩ + have hvi14 : i14.val = ((a0.val * b2.val) + (a1.val * b1.val)) + (a2.val * b0.val) := by rw [hi14, hvi11, hvi13] + have hbi14 : ((a0.val * b2.val) + (a1.val * b1.val)) + (a2.val * b0.val) < 2^107 := by omega + step as ⟨z3, hz3⟩ + step as ⟨i15, hi15⟩ + simp [hb] at hi15 + have hvi15 : i15.val = b3.val := by rw [hi15] + step with m_spec as ⟨i16, hi16⟩ + have hvi16 : i16.val = a0.val * b3.val := by rw [hi16, hvi, hvi15] + have hbi16 : a0.val * b3.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA0 hB3; omega + step with m_spec as ⟨i17, hi17⟩ + have hvi17 : i17.val = a1.val * b2.val := by rw [hi17, hvi5, hvi8] + have hbi17 : a1.val * b2.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA1 hB2; omega + have hsi18 : i16.val + i17.val < 2^128 := by rw [hvi16, hvi17]; omega + step as ⟨i18, hi18⟩ + have hvi18 : i18.val = (a0.val * b3.val) + (a1.val * b2.val) := by rw [hi18, hvi16, hvi17] + have hbi18 : (a0.val * b3.val) + (a1.val * b2.val) < 2^107 := by omega + step with m_spec as ⟨i19, hi19⟩ + have hvi19 : i19.val = a2.val * b1.val := by rw [hi19, hvi12, hvi3] + have hbi19 : a2.val * b1.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA2 hB1; omega + have hsi20 : i18.val + i19.val < 2^128 := by rw [hvi18, hvi19]; omega + step as ⟨i20, hi20⟩ + have hvi20 : i20.val = ((a0.val * b3.val) + (a1.val * b2.val)) + (a2.val * b1.val) := by rw [hi20, hvi18, hvi19] + have hbi20 : ((a0.val * b3.val) + (a1.val * b2.val)) + (a2.val * b1.val) < 2^107 := by omega + step as ⟨i21, hi21⟩ + simp [ha] at hi21 + have hvi21 : i21.val = a3.val := by rw [hi21] + step with m_spec as ⟨i22, hi22⟩ + have hvi22 : i22.val = a3.val * b0.val := by rw [hi22, hvi21, hvi1] + have hbi22 : a3.val * b0.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA3 hB0; omega + have hsi23 : i20.val + i22.val < 2^128 := by rw [hvi20, hvi22]; omega + step as ⟨i23, hi23⟩ + have hvi23 : i23.val = (((a0.val * b3.val) + (a1.val * b2.val)) + (a2.val * b1.val)) + (a3.val * b0.val) := by rw [hi23, hvi20, hvi22] + have hbi23 : (((a0.val * b3.val) + (a1.val * b2.val)) + (a2.val * b1.val)) + (a3.val * b0.val) < 2^107 := by omega + step as ⟨z4, hz4⟩ + step as ⟨i24, hi24⟩ + simp [hb] at hi24 + have hvi24 : i24.val = b4.val := by rw [hi24] + step with m_spec as ⟨i25, hi25⟩ + have hvi25 : i25.val = a0.val * b4.val := by rw [hi25, hvi, hvi24] + have hbi25 : a0.val * b4.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA0 hB4; omega + step with m_spec as ⟨i26, hi26⟩ + have hvi26 : i26.val = a1.val * b3.val := by rw [hi26, hvi5, hvi15] + have hbi26 : a1.val * b3.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA1 hB3; omega + have hsi27 : i25.val + i26.val < 2^128 := by rw [hvi25, hvi26]; omega + step as ⟨i27, hi27⟩ + have hvi27 : i27.val = (a0.val * b4.val) + (a1.val * b3.val) := by rw [hi27, hvi25, hvi26] + have hbi27 : (a0.val * b4.val) + (a1.val * b3.val) < 2^107 := by omega + step with m_spec as ⟨i28, hi28⟩ + have hvi28 : i28.val = a2.val * b2.val := by rw [hi28, hvi12, hvi8] + have hbi28 : a2.val * b2.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA2 hB2; omega + have hsi29 : i27.val + i28.val < 2^128 := by rw [hvi27, hvi28]; omega + step as ⟨i29, hi29⟩ + have hvi29 : i29.val = ((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val) := by rw [hi29, hvi27, hvi28] + have hbi29 : ((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val) < 2^107 := by omega + step with m_spec as ⟨i30, hi30⟩ + have hvi30 : i30.val = a3.val * b1.val := by rw [hi30, hvi21, hvi3] + have hbi30 : a3.val * b1.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA3 hB1; omega + have hsi31 : i29.val + i30.val < 2^128 := by rw [hvi29, hvi30]; omega + step as ⟨i31, hi31⟩ + have hvi31 : i31.val = (((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val)) + (a3.val * b1.val) := by rw [hi31, hvi29, hvi30] + have hbi31 : (((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val)) + (a3.val * b1.val) < 2^107 := by omega + step as ⟨i32, hi32⟩ + simp [ha] at hi32 + have hvi32 : i32.val = a4.val := by rw [hi32] + step with m_spec as ⟨i33, hi33⟩ + have hvi33 : i33.val = a4.val * b0.val := by rw [hi33, hvi32, hvi1] + have hbi33 : a4.val * b0.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA4 hB0; omega + have hsi34 : i31.val + i33.val < 2^128 := by rw [hvi31, hvi33]; omega + step as ⟨i34, hi34⟩ + have hvi34 : i34.val = ((((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val)) + (a3.val * b1.val)) + (a4.val * b0.val) := by rw [hi34, hvi31, hvi33] + have hbi34 : ((((a0.val * b4.val) + (a1.val * b3.val)) + (a2.val * b2.val)) + (a3.val * b1.val)) + (a4.val * b0.val) < 2^107 := by omega + step as ⟨z5, hz5⟩ + step with m_spec as ⟨i35, hi35⟩ + have hvi35 : i35.val = a1.val * b4.val := by rw [hi35, hvi5, hvi24] + have hbi35 : a1.val * b4.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA1 hB4; omega + step with m_spec as ⟨i36, hi36⟩ + have hvi36 : i36.val = a2.val * b3.val := by rw [hi36, hvi12, hvi15] + have hbi36 : a2.val * b3.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA2 hB3; omega + have hsi37 : i35.val + i36.val < 2^128 := by rw [hvi35, hvi36]; omega + step as ⟨i37, hi37⟩ + have hvi37 : i37.val = (a1.val * b4.val) + (a2.val * b3.val) := by rw [hi37, hvi35, hvi36] + have hbi37 : (a1.val * b4.val) + (a2.val * b3.val) < 2^107 := by omega + step with m_spec as ⟨i38, hi38⟩ + have hvi38 : i38.val = a3.val * b2.val := by rw [hi38, hvi21, hvi8] + have hbi38 : a3.val * b2.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA3 hB2; omega + have hsi39 : i37.val + i38.val < 2^128 := by rw [hvi37, hvi38]; omega + step as ⟨i39, hi39⟩ + have hvi39 : i39.val = ((a1.val * b4.val) + (a2.val * b3.val)) + (a3.val * b2.val) := by rw [hi39, hvi37, hvi38] + have hbi39 : ((a1.val * b4.val) + (a2.val * b3.val)) + (a3.val * b2.val) < 2^107 := by omega + step with m_spec as ⟨i40, hi40⟩ + have hvi40 : i40.val = a4.val * b1.val := by rw [hi40, hvi32, hvi3] + have hbi40 : a4.val * b1.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA4 hB1; omega + have hsi41 : i39.val + i40.val < 2^128 := by rw [hvi39, hvi40]; omega + step as ⟨i41, hi41⟩ + have hvi41 : i41.val = (((a1.val * b4.val) + (a2.val * b3.val)) + (a3.val * b2.val)) + (a4.val * b1.val) := by rw [hi41, hvi39, hvi40] + have hbi41 : (((a1.val * b4.val) + (a2.val * b3.val)) + (a3.val * b2.val)) + (a4.val * b1.val) < 2^107 := by omega + step as ⟨z6, hz6⟩ + step with m_spec as ⟨i42, hi42⟩ + have hvi42 : i42.val = a2.val * b4.val := by rw [hi42, hvi12, hvi24] + have hbi42 : a2.val * b4.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA2 hB4; omega + step with m_spec as ⟨i43, hi43⟩ + have hvi43 : i43.val = a3.val * b3.val := by rw [hi43, hvi21, hvi15] + have hbi43 : a3.val * b3.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA3 hB3; omega + have hsi44 : i42.val + i43.val < 2^128 := by rw [hvi42, hvi43]; omega + step as ⟨i44, hi44⟩ + have hvi44 : i44.val = (a2.val * b4.val) + (a3.val * b3.val) := by rw [hi44, hvi42, hvi43] + have hbi44 : (a2.val * b4.val) + (a3.val * b3.val) < 2^107 := by omega + step with m_spec as ⟨i45, hi45⟩ + have hvi45 : i45.val = a4.val * b2.val := by rw [hi45, hvi32, hvi8] + have hbi45 : a4.val * b2.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA4 hB2; omega + have hsi46 : i44.val + i45.val < 2^128 := by rw [hvi44, hvi45]; omega + step as ⟨i46, hi46⟩ + have hvi46 : i46.val = ((a2.val * b4.val) + (a3.val * b3.val)) + (a4.val * b2.val) := by rw [hi46, hvi44, hvi45] + have hbi46 : ((a2.val * b4.val) + (a3.val * b3.val)) + (a4.val * b2.val) < 2^107 := by omega + step as ⟨z7, hz7⟩ + step with m_spec as ⟨i47, hi47⟩ + have hvi47 : i47.val = a3.val * b4.val := by rw [hi47, hvi21, hvi24] + have hbi47 : a3.val * b4.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA3 hB4; omega + step with m_spec as ⟨i48, hi48⟩ + have hvi48 : i48.val = a4.val * b3.val := by rw [hi48, hvi32, hvi15] + have hbi48 : a4.val * b3.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA4 hB3; omega + have hsi49 : i47.val + i48.val < 2^128 := by rw [hvi47, hvi48]; omega + step as ⟨i49, hi49⟩ + have hvi49 : i49.val = (a3.val * b4.val) + (a4.val * b3.val) := by rw [hi49, hvi47, hvi48] + have hbi49 : (a3.val * b4.val) + (a4.val * b3.val) < 2^107 := by omega + step as ⟨z8, hz8⟩ + step with m_spec as ⟨i50, hi50⟩ + have hvi50 : i50.val = a4.val * b4.val := by rw [hi50, hvi32, hvi24] + have hbi50 : a4.val * b4.val < 2^104 := by + have h := Nat.mul_lt_mul'' hA4 hB4; omega + step as ⟨zfin, hzfin⟩ + try simp only [spec_ok] + refine ⟨i2, i7, i14, i23, i34, i41, i46, i49, i50, ?_, + hvi2, hvi7, hvi14, hvi23, hvi34, hvi41, hvi46, hvi49, hvi50⟩ + simp [hzfin, hz1, hz2, hz3, hz4, hz5, hz6, hz7, hz8, Array.set_val_eq] + +end ScalarProofs diff --git a/verification/Proofs/ScalarReduceSpec.lean b/verification/Proofs/ScalarReduceSpec.lean new file mode 100644 index 0000000..1a46eed --- /dev/null +++ b/verification/Proofs/ScalarReduceSpec.lean @@ -0,0 +1,204 @@ +/- ────────────────────────────────────────────────────────────────────────────── + Proofs/ScalarReduceSpec.lean β€” Scalar52 Montgomery reduction, the main walk. + + Rounds 0–4 of `montgomery_reduce` (the five exact-division `part1` rounds), + composed with `mont_tail_spec` (rounds 5–8 + the `sub _ L` + canonicalization) from ScalarMontSpec. Split across two files because the + 74-step monolith exceeds a single declaration's elaboration budget + (METHOD 4); each half is a `mul_internal`-sized walk. + ────────────────────────────────────────────────────────────────────────────── -/ +import Proofs.ScalarMontSpec +open Aeneas Aeneas.Std Result +open curve25519_dalek + +set_option maxHeartbeats 16000000 +set_option linter.unusedSimpArgs false +set_option exponentiation.threshold 600 + +namespace ScalarProofs + +open Aeneas.Std.WP + +/-- The nonce value N = Ξ£ n_kΒ·2^52k of five 52-bit digits stays below R. + Standalone so its `omega` sees exactly five hypotheses β€” inside the + walk, the same goal drags ~110 hypotheses (five round equations with + 2^102-scale coefficients included) into one Presburger instance and + never returns (measured: the single spiralling line of the file). -/ +theorem nonce_sum_bound {n0 n1 n2 n3 n4 : β„•} (h0 : n0 < 2^52) (h1 : n1 < 2^52) + (h2 : n2 < 2^52) (h3 : n3 < 2^52) (h4 : n4 < 2^52) : + n0 + 2^52 * n1 + 2^104 * n2 + 2^156 * n3 + 2^208 * n4 < 2^260 := by + omega + +/-- **Montgomery reduction is exact division by R = 2^260 mod β„“.** For a + 9-limb double-width input Z = Ξ£ z_kΒ·2^52k with column-bounded limbs + (z_k < 2^107, what `mul_internal` produces) and the standard + Montgomery hypothesis Z < 2^260Β·β„“, the transpiled `montgomery_reduce` + returns a 52-bit-bounded scalar r with ⟦r⟧·2^260 = Z in ZMod β„“. + Rounds 0–4 walk `part1_spec` here; rounds 5–8 and the `sub _ L` + canonicalization are `mont_tail_spec`; the value accounting is + `mont_head_telescope` + `mont_bound`. -/ +theorem montgomery_reduce_spec (limbs : Std.Array Std.U128 9#usize) + (z0 z1 z2 z3 z4 z5 z6 z7 z8 : Std.U128) + (hl : (↑limbs : List Std.U128) = [z0, z1, z2, z3, z4, z5, z6, z7, z8]) + (hzb : z0.val < 2^107 ∧ z1.val < 2^107 ∧ z2.val < 2^107 ∧ z3.val < 2^107 ∧ + z4.val < 2^107 ∧ z5.val < 2^107 ∧ z6.val < 2^107 ∧ z7.val < 2^107 ∧ + z8.val < 2^107) + (hZ : z0.val + 2^52 * z1.val + 2^104 * z2.val + 2^156 * z3.val + 2^208 * z4.val + 2^260 * z5.val + 2^312 * z6.val + 2^364 * z7.val + 2^416 * z8.val < 2^260 * Ell) : + backend.serial.u64.scalar.Scalar52.montgomery_reduce limbs + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ + s4.val < 2^52) ∧ + scDenote r * 2^260 = ((z0.val + 2^52 * z1.val + 2^104 * z2.val + 2^156 * z3.val + 2^208 * z4.val + 2^260 * z5.val + 2^312 * z6.val + 2^364 * z7.val + 2^416 * z8.val : β„•) : ZMod Ell) ⦄ := by + obtain ⟨hz0, hz1, hz2, hz3, hz4, hz5, hz6, hz7, hz8⟩ := hzb + -- Hide the Montgomery bound behind an existential for the duration of + -- the walk: a bare 2^416-coefficient inequality in the local context + -- sends every step's side-condition automation into the huge literals + -- (measured: the walk never finishes). It re-enters only for mont_bound. + replace hZ : βˆƒ B : β„•, + (z0.val + 2^52 * z1.val + 2^104 * z2.val + 2^156 * z3.val + + 2^208 * z4.val + 2^260 * z5.val + 2^312 * z6.val + 2^364 * z7.val + + 2^416 * z8.val < B) ∧ B = 2^260 * Ell := ⟨_, hZ, rfl⟩ + unfold backend.serial.u64.scalar.Scalar52.montgomery_reduce + backend.serial.u64.scalar.Scalar52.Insts.CoreOpsIndexIndexUsizeU64.index + step as ⟨i, hi⟩ + simp [hl] at hi + have hvi : i.val = z0.val := by rw [hi] + have hbi : i.val < 2^124 := by clear hZ; omega + step with (part1_spec i hbi) as ⟨carry, n0, hn0b, hE0⟩ + rw [hvi] at hE0 + have hcb0 : carry.val < 2^60 := by clear hZ; omega + step as ⟨i1, hi1⟩ + simp [hl] at hi1 + have hvi1 : i1.val = z1.val := by rw [hi1] + have hsi2 : carry.val + i1.val < 2^128 := by clear hZ; omega + step as ⟨i2, hi2⟩ + have hvi2 : i2.val = carry.val + i1.val := by rw [hi2] + have hbi2 : i2.val < 2^110 := by clear hZ; omega + step as ⟨i3, hi3⟩ + try simp [L_limbs] at hi3 + have hvi3 : i3.val = 3916664325105025 := by rw [hi3]; rfl + step with m_spec as ⟨i4, hi4⟩ + have hvi4 : i4.val = n0.val * 3916664325105025 := by rw [hi4, hvi3] + have hbi4 : i4.val < 2^104 := by clear hZ; rw [hvi4]; omega + have hsi5 : i2.val + i4.val < 2^128 := by clear hZ; omega + step as ⟨i5, hi5⟩ + have hvi5 : i5.val = i2.val + i4.val := by rw [hi5] + have hbi5 : i5.val < 2^112 := by clear hZ; omega + have hbp1 : i5.val < 2^124 := by clear hZ; omega + step with (part1_spec i5 hbp1) as ⟨carry1, n1, hn1b, hE1⟩ + rw [hvi5, hvi2, hvi1, hvi4] at hE1 + have hcb1 : carry1.val < 2^60 := by clear hZ; omega + step as ⟨i6, hi6⟩ + simp [hl] at hi6 + have hvi6 : i6.val = z2.val := by rw [hi6] + have hsi7 : carry1.val + i6.val < 2^128 := by clear hZ; omega + step as ⟨i7, hi7⟩ + have hvi7 : i7.val = carry1.val + i6.val := by rw [hi7] + have hbi7 : i7.val < 2^110 := by clear hZ; omega + step as ⟨i8, hi8⟩ + try simp [L_limbs] at hi8 + have hvi8 : i8.val = 1367801 := by rw [hi8]; rfl + step with m_spec as ⟨i9, hi9⟩ + have hvi9 : i9.val = n0.val * 1367801 := by rw [hi9, hvi8] + have hbi9 : i9.val < 2^104 := by clear hZ; rw [hvi9]; omega + have hsi10 : i7.val + i9.val < 2^128 := by clear hZ; omega + step as ⟨i10, hi10⟩ + have hvi10 : i10.val = i7.val + i9.val := by rw [hi10] + have hbi10 : i10.val < 2^112 := by clear hZ; omega + step with m_spec as ⟨i11, hi11⟩ + have hvi11 : i11.val = n1.val * 3916664325105025 := by rw [hi11, hvi3] + have hbi11 : i11.val < 2^104 := by clear hZ; rw [hvi11]; omega + have hsi12 : i10.val + i11.val < 2^128 := by clear hZ; omega + step as ⟨i12, hi12⟩ + have hvi12 : i12.val = i10.val + i11.val := by rw [hi12] + have hbi12 : i12.val < 2^113 := by clear hZ; omega + have hbp2 : i12.val < 2^124 := by clear hZ; omega + step with (part1_spec i12 hbp2) as ⟨carry2, n2, hn2b, hE2⟩ + rw [hvi12, hvi10, hvi7, hvi6, hvi9, hvi11] at hE2 + have hcb2 : carry2.val < 2^62 := by clear hZ; omega + step as ⟨i13, hi13⟩ + simp [hl] at hi13 + have hvi13 : i13.val = z3.val := by rw [hi13] + have hsi14 : carry2.val + i13.val < 2^128 := by clear hZ; omega + step as ⟨i14, hi14⟩ + have hvi14 : i14.val = carry2.val + i13.val := by rw [hi14] + have hbi14 : i14.val < 2^110 := by clear hZ; omega + step with m_spec as ⟨i15, hi15⟩ + have hvi15 : i15.val = n1.val * 1367801 := by rw [hi15, hvi8] + have hbi15 : i15.val < 2^104 := by clear hZ; rw [hvi15]; omega + have hsi16 : i14.val + i15.val < 2^128 := by clear hZ; omega + step as ⟨i16, hi16⟩ + have hvi16 : i16.val = i14.val + i15.val := by rw [hi16] + have hbi16 : i16.val < 2^112 := by clear hZ; omega + step with m_spec as ⟨i17, hi17⟩ + have hvi17 : i17.val = n2.val * 3916664325105025 := by rw [hi17, hvi3] + have hbi17 : i17.val < 2^104 := by clear hZ; rw [hvi17]; omega + have hsi18 : i16.val + i17.val < 2^128 := by clear hZ; omega + step as ⟨i18, hi18⟩ + have hvi18 : i18.val = i16.val + i17.val := by rw [hi18] + have hbi18 : i18.val < 2^113 := by clear hZ; omega + have hbp3 : i18.val < 2^124 := by clear hZ; omega + step with (part1_spec i18 hbp3) as ⟨carry3, n3, hn3b, hE3⟩ + rw [hvi18, hvi16, hvi14, hvi13, hvi15, hvi17] at hE3 + have hcb3 : carry3.val < 2^62 := by clear hZ; omega + step as ⟨i19, hi19⟩ + simp [hl] at hi19 + have hvi19 : i19.val = z4.val := by rw [hi19] + have hsi20 : carry3.val + i19.val < 2^128 := by clear hZ; omega + step as ⟨i20, hi20⟩ + have hvi20 : i20.val = carry3.val + i19.val := by rw [hi20] + have hbi20 : i20.val < 2^110 := by clear hZ; omega + step as ⟨i21, hi21⟩ + try simp [L_limbs] at hi21 + have hvi21 : i21.val = 17592186044416 := by rw [hi21]; rfl + step with m_spec as ⟨i22, hi22⟩ + have hvi22 : i22.val = n0.val * 17592186044416 := by rw [hi22, hvi21] + have hbi22 : i22.val < 2^104 := by clear hZ; rw [hvi22]; omega + have hsi23 : i20.val + i22.val < 2^128 := by clear hZ; omega + step as ⟨i23, hi23⟩ + have hvi23 : i23.val = i20.val + i22.val := by rw [hi23] + have hbi23 : i23.val < 2^112 := by clear hZ; omega + step with m_spec as ⟨i24, hi24⟩ + have hvi24 : i24.val = n2.val * 1367801 := by rw [hi24, hvi8] + have hbi24 : i24.val < 2^104 := by clear hZ; rw [hvi24]; omega + have hsi25 : i23.val + i24.val < 2^128 := by clear hZ; omega + step as ⟨i25, hi25⟩ + have hvi25 : i25.val = i23.val + i24.val := by rw [hi25] + have hbi25 : i25.val < 2^113 := by clear hZ; omega + step with m_spec as ⟨i26, hi26⟩ + have hvi26 : i26.val = n3.val * 3916664325105025 := by rw [hi26, hvi3] + have hbi26 : i26.val < 2^104 := by clear hZ; rw [hvi26]; omega + have hsi27 : i25.val + i26.val < 2^128 := by clear hZ; omega + step as ⟨i27, hi27⟩ + have hvi27 : i27.val = i25.val + i26.val := by rw [hi27] + have hbi27 : i27.val < 2^114 := by clear hZ; omega + have hbp4 : i27.val < 2^124 := by clear hZ; omega + step with (part1_spec i27 hbp4) as ⟨carry4, n4, hn4b, hE4⟩ + rw [hvi27, hvi25, hvi23, hvi20, hvi19, hvi22, hvi24, hvi26] at hE4 + have hcb4 : carry4.val < 2^62 := by clear hZ; omega + + -- the head telescope gives Xβ€²Β·2^260 = Z + NΒ·β„“; mont_bound gives Xβ€² < 2β„“ + have hHT := mont_head_telescope z0.val z1.val z2.val z3.val z4.val z5.val + z6.val z7.val z8.val n0.val n1.val n2.val n3.val n4.val + carry.val carry1.val carry2.val carry3.val carry4.val + hE0 hE1 hE2 hE3 hE4 + have hNb := nonce_sum_bound hn0b hn1b hn2b hn3b hn4b + obtain ⟨B, hZlt, hBeq⟩ := hZ + subst hBeq + have hXb := mont_bound _ _ _ hHT hZlt hNb + + -- rounds 5–8 + canonicalization + apply spec_mono (mont_tail_spec limbs z0 z1 z2 z3 z4 z5 z6 z7 z8 carry4 + n1 n2 n3 n4 i3 i8 i21 hl hvi3 hvi8 hvi21 hcb4 + ⟨hn1b, hn2b, hn3b, hn4b⟩ ⟨hz5, hz6, hz7, hz8⟩ hXb) + intro r hr + refine ⟨hr.1, ?_⟩ + rw [hr.2] + have hEz : (Ell : ZMod Ell) = 0 := ZMod.natCast_self Ell + have hc := congrArg (Nat.cast (R := ZMod Ell)) hHT + push_cast at hc + rw [hEz] at hc + push_cast + linear_combination hc + +end ScalarProofs diff --git a/verification/Proofs/ScalarSubSpec.lean b/verification/Proofs/ScalarSubSpec.lean index a1cec8a..a0d3a4e 100644 --- a/verification/Proofs/ScalarSubSpec.lean +++ b/verification/Proofs/ScalarSubSpec.lean @@ -742,7 +742,9 @@ theorem sub_val_spec (a b : Sc) (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 + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ s4.val < 2^52) ∧ + 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 @@ -763,7 +765,9 @@ theorem sub_val_spec (a b : Sc) let underflow_mask ← lift (core.num.U64.wrapping_sub i2 1#u64) backend.serial.u64.scalar.Scalar52.sub_loop1 { start := 0#usize, Β«endΒ» := 5#usize } dw mask underflow_mask 0#u64) - ⦃ r => scDenote r = scDenote a - scDenote b ⦄ + ⦃ r => (βˆƒ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧ + s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧ s4.val < 2^52) ∧ + scDenote r = scDenote a - scDenote b ⦄ -- underflow mask: um = ((borrow>>>63) ^^^ 1) βˆ’ 1 (all-ones iff borrow) step as ⟨i1, hi1⟩ have hi1v : i1.val = Ξ²5 := by rw [hi1]; exact hbor @@ -789,6 +793,8 @@ theorem sub_val_spec (a b : Sc) rw [humv, hi2v, hΞ²z]; norm_num apply spec_mono (sub_loop1_zero_spec dw mask um d0 d1 d2 d3 d4 hdl hmaskv humz hdb) rintro d ⟨r0, r1, r2, r3, r4, hrl, hr0, hr1, hr2, hr3, hr4⟩ + refine ⟨⟨r0, r1, r2, r3, r4, hrl, + by omega, by omega, by omega, by omega, by omega⟩, ?_⟩ have hdval : scVal d = scLimbs d0 d1 d2 d3 d4 := by rw [scVal_eq d r0 r1 r2 r3 r4 hrl]; unfold scLimbs; rw [hr0, hr1, hr2, hr3, hr4] have key : scVal d + scVal b = scVal a := by @@ -803,6 +809,7 @@ theorem sub_val_spec (a b : Sc) rintro d ⟨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⟩ + refine ⟨⟨r0, r1, r2, r3, r4, hrl, hrb0, hrb1, hrb2, hrb3, hrb4⟩, ?_⟩ 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 diff --git a/verification/check-scalar.sh b/verification/check-scalar.sh index e875038..c98e596 100755 --- a/verification/check-scalar.sh +++ b/verification/check-scalar.sh @@ -7,7 +7,7 @@ source ~/aeneas-toolchain/env.sh HERE="$(cd "$(dirname "$0")" && pwd)" AENEAS_LEAN="$AENEAS_HOME/backends/lean" GEN=(CurveScalar/TypesExternal CurveScalar/Types CurveScalar/FunsExternal CurveScalar/Funs) -PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec) +PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain) echo "=== stub/axiom audit ===" grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; } @@ -28,16 +28,17 @@ lake env bash -c " export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\" cd '$HERE' AUD=\$(mktemp '$HERE/.audit-scalar-XXXX.lean') - { echo 'import Proofs.ScalarDenote'; echo 'import Proofs.ScalarSubSpec'; echo 'import Proofs.ScalarAddSpec'; echo '#print axioms ScalarProofs.L_val' + { echo 'import Proofs.ScalarMain'; echo '#print axioms ScalarProofs.L_val' echo '#print axioms ScalarProofs.sub_loop_spec' - echo '#print axioms ScalarProofs.sub_loop1_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; } > \"\$AUD\" + echo '#print axioms ScalarProofs.sub_loop1_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_spec' + echo '#print axioms ScalarProofs.part1_spec'; echo '#print axioms ScalarProofs.montgomery_reduce_spec'; echo '#print axioms ScalarProofs.mul_spec'; echo '#print axioms ScalarProofs.scalarImplementation'; } > \"\$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 5 ] || { echo \"AXIOM AUDIT FAILED: \$N/5 clean\"; exit 1; } + [ \"\$N\" -eq 10 ] || { echo \"AXIOM AUDIT FAILED: \$N/10 clean\"; exit 1; } " || { echo FAIL; exit 1; } echo " L_val axiom-clean" echo "" -echo "SCALAR FOUNDATION: gen compiles; denotation + group-order constant (L = β„“) proven." +echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round through RR) proven mod β„“; aggregate certificate scalarImplementation kernel-audited."