saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

scalar layer: mul_internal proven — Montgomery frontier phase A down

Browse source 
Proofs/ScalarMulSpec.lean (axiom-clean, no sorry):
- m_spec: the widening 52x52->104-bit product helper — total, exact
- mul_internal_spec: all NINE schoolbook column sums proven exact
  (z_k = sum_{i+j=k} a_i*b_j) and bounded (each product < 2^104, each
  column < 2^107) through the 60-step straight-line extraction

This is the half of Scalar52::mul that the kernel-capacity frontier does
NOT touch. Phase B — montgomery_reduce (74 steps, part1/part2, the
Montgomery invariant result = input * R^{-1} mod l with R = 2^260, and
the double-round composition through RR) — remains the open frontier,
now precisely one function wide.

check-scalar.sh: ScalarMulSpec in manifest + audit (6/6 clean), green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
saymrwulf 2026-07-03 18:56:04 +02:00
parent 7dff4157a2
commit 3cd7a17ab2
2 changed files with 279 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

275
verification/Proofs/ScalarMulSpec.lean Normal file
View file

@ -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

8
verification/check-scalar.sh
View file

@ -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)
echo "=== stub/axiom audit ==="
grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/Scalar*.lean 2>/dev/null && { echo "axiom under Proofs/"; exit 1; }
@ -28,14 +28,14 @@ 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.ScalarDenote'; echo 'import Proofs.ScalarSubSpec'; echo 'import Proofs.ScalarAddSpec'; echo 'import Proofs.ScalarMulSpec'; echo '#print axioms ScalarProofs.L_val'
echo '#print axioms ScalarProofs.sub_loop_spec'
echo '#print axioms ScalarProofs.cond_add_l_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; } > \"\$AUD\"
echo '#print axioms ScalarProofs.cond_add_l_one_spec'; echo '#print axioms ScalarProofs.sub_val_spec'; echo '#print axioms ScalarProofs.add_val_spec'; echo '#print axioms ScalarProofs.mul_internal_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 5 ] || { echo \"AXIOM AUDIT FAILED: \$N/5 clean\"; exit 1; }
[ \"\$N\" -eq 6 ] || { echo \"AXIOM AUDIT FAILED: \$N/6 clean\"; exit 1; }
" || { echo FAIL; exit 1; }
echo " L_val axiom-clean"