saymrwulf/risc0-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/risc0-ed25519-verified.git synced 2026-09-03 19:53:45 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

NAF encoder proven end-to-end + the phase-1 double-scalar-mul apex

Browse source 
The complete non_adjacent_form(5) verification (four stages):
- `Proofs/DsmNafLoadSpec.lean` (generated) — the LE byte-to-word load.
- `Proofs/DsmNafMath.lean` — the digit loop's arithmetic core: window-read
  lemmas (single/cross-word), the exact ZZ invariant steps (Nat.mod_mul
  telescope), the carry-kill argument from V < 2^253, and the exit theorem.
- `Proofs/DsmNafLoopSpec.lean` — the w=5 digit loop by induction on the
  remaining-bits measure: per-step 64-bit window read (4-way word split),
  digit write via hcast/wrapping_sub (exact value window - 32*carry',
  oddness, |d| < 16), invariant carried through even/odd steps.
- `Proofs/DsmNafSpec.lean` — the public spec: both entry masserts
  DISCHARGED; the digits satisfy the NAF conditions and
      sum naf[k]*2^k = V   EXACTLY (integers, no modular slack)
  for any scalar whose LE byte value V is below 2^253.

And the campaign's brick 4, `Proofs/DsmMulSpec.lean`:
- `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is the standard
  base point: valid extended coordinates (X*Y = Z*T) and the curve equation,
  kernel-checked via denominator-free 121666-scaled witnesses. Includes the
  generic witness lemmas fp_mul_eq_of_witness / onCurve_of_witness.
- `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC of
  vartime_double_base::mul: for canonical scalars and a valid on-curve A,
  the result is valid, on-curve, and denotes
      dsmFold (naf a) (naf b) (edPt A) edBasePt edId 256
  with both digit arrays proven exact NAF encodings. Phase 2 (group
  semantics [a]A + [b]B) requires Edwards associativity — deferred and
  documented; nothing assumes it.

Also: removed a vestigial pre-re-extraction axiom stub
(backend.serial.scalar_mul.vartime_double_base.mul) from FunsExternal —
a root-level leftover that shadowed the real namespaced definition during
name resolution in proof files. Never referenced by any certificate (the
#print-axioms audit guards against that); deleted for hygiene.

CERTS += naf_load_spec, naf_exit, naf_digit_loop_spec,
non_adjacent_form_spec, run_basepoint, vartime_double_base_mul_spec —
each audited to exactly [propext, Classical.choice, Quot.sound].
Full check.sh green.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-04 16:52:08 +02:00
parent eb167a12fe
commit af3ec18fc0
7 changed files with 2427 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

200
verification/Proofs/DsmMulSpec.lean Normal file
View file

@ -0,0 +1,200 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/DsmMulSpec.lean — double-scalar-mul campaign, brick 4:
the basepoint constant and the public `vartime_double_base::mul` spec.
· `run_basepoint` — the transpiled ED25519_BASEPOINT_POINT is a VALID
extended point ON THE CURVE denoting the standard base point
B = (x_B, y_B), x_B = 15112…202, y_B = 46316…960
— kernel-checked literal arithmetic: the extended coherence X·Y = Z·T
and the (121666-scaled, denominator-free) curve equation
121666·y² + 121665·x²y² ≡ 121666 + 121666·x² (mod p).
A corrupted basepoint constant would be caught here.
· `vartime_double_base_mul_spec` — THE PHASE-1 COMPUTATIONAL SPEC:
for canonical scalars (byte values < 2^253) and a valid on-curve A,
`mul a A b` returns a valid on-curve R with
edPt R = dsmFold (digits of a) (digits of b) (edPt A) edBasePt edId 256
where both digit arrays are proven NAF encodings of the scalars' exact
byte values (existentially exposed with their NafDigits + nafSum facts).
Composes non_adjacent_form_spec ×2, dsm_top_index_spec, naf_table_spec
×2 (A and the basepoint), dsm_loop_spec, proj_as_extended_spec.
Phase 2 (reading dsmFold as [a]A + [b]B in the group) requires Edwards
associativity — deliberately deferred and documented; nothing here
assumes it.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.DsmNafSpec
open Aeneas Aeneas.Std Result ControlFlow
open curve25519_dalek
set_option maxHeartbeats 8000000
set_option linter.unusedSimpArgs false
set_option maxRecDepth 8000
set_option exponentiation.threshold 600
namespace CurveFieldProofs
open Aeneas.Std.WP
/-- Generic mod-p witness → Fp product identity (abstract, no literal
crunching during cast distribution). -/
theorem fp_mul_eq_of_witness (a b c : ℕ) (hmod : (a * b) % P = c % P) :
(a : Fp) * (b : Fp) = (c : Fp) := by
have h1 : ((a * b : ℕ) : Fp) = ((c : ℕ) : Fp) := by
rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod]
push_cast at h1
exact h1
/-- Generic 121666-scaled curve-equation witness → OnCurve (abstract x, y). -/
theorem onCurve_of_witness (x y : ℕ)
(hmod : (121666 * (y * y) + 121665 * (x * x) * (y * y)) % P
= (121666 + 121666 * (x * x)) % P) :
OnCurve (x : Fp) (y : Fp) := by
have h1 : ((121666 * (y * y) + 121665 * (x * x) * (y * y) : ℕ) : Fp)
= ((121666 + 121666 * (x * x) : ℕ) : Fp) := by
rw [← ZMod.natCast_mod, hmod, ZMod.natCast_mod]
push_cast at h1
have h6 : (121666 : Fp) ≠ 0 := by
have h : ((121666 : ℕ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
simpa using h
have hd := edD_char
unfold OnCurve
apply mul_left_cancel₀ h6
linear_combination h1 - (x : Fp)^2 * (y : Fp)^2 * hd
/-- The standard Ed25519 base point, as ZMod literals. -/
noncomputable def edBasePt : Fp × Fp :=
((15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp),
(46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp))
/-- **The transpiled basepoint constant is the standard base point** —
valid, on-curve, kernel-audited literal arithmetic. -/
theorem run_basepoint :
∃ B : EdPoint,
backend.serial.u64.constants.ED25519_BASEPOINT_POINT = ok B ∧
ExtValid B ∧ OnCurveExt B ∧ edPt B = edBasePt := by
-- the four coordinate denotations
have hXv : ⟪(Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64,
2070867633025821#u64, 562264141797630#u64, 587772402128613#u64] :
backend.serial.u64.field.FieldElement51)⟫ =
(15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) := by
simp [denote, feVal, limbsVal, Array.make]
have hYv : ⟪(Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64,
450359962737049#u64, 900719925474099#u64, 1801439850948198#u64] :
backend.serial.u64.field.FieldElement51)⟫ =
(46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by
simp [denote, feVal, limbsVal, Array.make]
have hZv : ⟪(Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64] :
backend.serial.u64.field.FieldElement51)⟫ = (1 : Fp) := by
simp [denote, feVal, limbsVal, Array.make]
have hTv : ⟪(Array.make 5#usize [1841354044333475#u64, 16398895984059#u64,
755974180946558#u64, 900171276175154#u64, 1821297809914039#u64] :
backend.serial.u64.field.FieldElement51)⟫ =
(46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by
simp [denote, feVal, limbsVal, Array.make]
-- coherence of the affine literals: x·y = t (z = 1)
have hco : (15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp) *
(46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) =
(46827403850823179245072216630277197565144205554125654976674165829533817101731 : Fp) := by
apply fp_mul_eq_of_witness
norm_num [P]
-- the curve equation for the affine literals (121666-scaled witness)
have hcv : OnCurve
(15112221349535400772501151409588531511454012693041857206046113283949847762202 : Fp)
(46316835694926478169428394003475163141307993866256225615783033603165251855960 : Fp) := by
have h := onCurve_of_witness
15112221349535400772501151409588531511454012693041857206046113283949847762202
46316835694926478169428394003475163141307993866256225615783033603165251855960
(by norm_num [P])
push_cast at h
exact h
refine ⟨⟨Array.make 5#usize [1738742601995546#u64, 1146398526822698#u64,
2070867633025821#u64, 562264141797630#u64, 587772402128613#u64],
Array.make 5#usize [1801439850948184#u64, 1351079888211148#u64,
450359962737049#u64, 900719925474099#u64, 1801439850948198#u64],
Array.make 5#usize [1#u64, 0#u64, 0#u64, 0#u64, 0#u64],
Array.make 5#usize [1841354044333475#u64, 16398895984059#u64,
755974180946558#u64, 900171276175154#u64, 1821297809914039#u64]⟩,
?_, ⟨?_, ?_, ?_, ?_, ?_, ?_⟩, ?_, ?_⟩
· unfold backend.serial.u64.constants.ED25519_BASEPOINT_POINT
backend.serial.u64.field.FieldElement51.from_limbs
rfl
· simp [Bnd, Array.make]
· simp [Bnd, Array.make]
· simp [Bnd, Array.make]
· simp [Bnd, Array.make]
· show ⟪_⟫ ≠ 0
rw [hZv]; exact one_ne_zero
· show ⟪_⟫ * ⟪_⟫ = ⟪_⟫ * ⟪_⟫
rw [hXv, hYv, hZv, hTv, one_mul]
exact hco
· show OnCurve (edX _) (edY _)
unfold edX edY
simp only
rw [hXv, hYv, hZv, div_one, div_one]
exact hcv
· show (edX _, edY _) = edBasePt
unfold edX edY edBasePt
simp only
rw [hXv, hYv, hZv, div_one, div_one]
/-- **vartime_double_base::mul — the phase-1 computational specification.**
For canonical scalars a, b (LE byte values Va, Vb < 2^253) and a valid
on-curve A: the result is a valid on-curve point denoting the abstract
double-and-add fold of the two proven NAF encodings over A and the
standard base point. -/
theorem vartime_double_base_mul_spec
(a b : scalar.Scalar) (A : EdPoint)
(a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31 : Std.U8)
(b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8)
(hab : (↑a.bytes : List Std.U8) = [a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, a16, a17, a18, a19, a20, a21, a22, a23, a24, a25, a26, a27, a28, a29, a30, a31])
(hbb : (↑b.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31])
(Va Vb : ℕ)
(hVa : Va = a0.val + a1.val * 2^8 + a2.val * 2^16 + a3.val * 2^24 + a4.val * 2^32 + a5.val * 2^40 + a6.val * 2^48 + a7.val * 2^56 + a8.val * 2^64 + a9.val * 2^72 + a10.val * 2^80 + a11.val * 2^88 + a12.val * 2^96 + a13.val * 2^104 + a14.val * 2^112 + a15.val * 2^120 + a16.val * 2^128 + a17.val * 2^136 + a18.val * 2^144 + a19.val * 2^152 + a20.val * 2^160 + a21.val * 2^168 + a22.val * 2^176 + a23.val * 2^184 + a24.val * 2^192 + a25.val * 2^200 + a26.val * 2^208 + a27.val * 2^216 + a28.val * 2^224 + a29.val * 2^232 + a30.val * 2^240 + a31.val * 2^248)
(hVb : Vb = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248)
(hValt : Va < 2^253) (hVblt : Vb < 2^253)
(hAv : ExtValid A) (hAc : OnCurveExt A) :
backend.serial.scalar_mul.vartime_double_base.mul a A b ⦃ R =>
ExtValid R ∧ OnCurveExt R ∧
∃ (na nb : Std.Array Std.I8 256#usize),
NafDigits na ∧ NafDigits nb ∧
nafSum na 256 = (Va : ℤ) ∧ nafSum nb 256 = (Vb : ℤ) ∧
edPt R = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 ⦄ := by
obtain ⟨B, hBok, hBv, hBc, hBpt⟩ := run_basepoint
unfold backend.serial.scalar_mul.vartime_double_base.mul
-- the two NAF encodings
step with (non_adjacent_form_spec a
a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14 a15 a16 a17 a18 a19 a20 a21 a22 a23 a24 a25 a26 a27 a28 a29 a30 a31
hab Va hVa hValt) as ⟨na, hnaD, hnaS⟩
step with (non_adjacent_form_spec b
b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31
hbb Vb hVb hVblt) as ⟨nb, hnbD, hnbS⟩
-- the top index (constant 255)
step with (dsm_top_index_spec na nb) as ⟨i, hi⟩
-- table over A
step with (naf_table_spec A hAv hAc) as
⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, ta, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩
-- the basepoint constant
rw [hBok]
simp only [bind_tc_ok]
-- table over B
step with (naf_table_spec B hBv hBc) as
⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, tb, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩
-- the 256-step Straus loop
step with (dsm_loop_spec i (by rw [hi]; scalar_tac : i.val = 255) na nb ta tb A B
⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, hlA, hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩
⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, hlB, hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩
hnaD hnbD) as ⟨r, hrv, hrc, hrfold⟩
-- the final projective → extended conversion
apply spec_mono (proj_as_extended_spec r hrv)
rintro R ⟨hRv, -, -, -, -, hRx, hRy⟩
refine ⟨hRv, ?_, na, nb, hnaD, hnbD, hnaS, hnbS, ?_⟩
· show OnCurve (edX R) (edY R)
rw [hRx, hRy]
exact hrc
· calc edPt R = (edX R, edY R) := rfl
_ = (projX r, projY r) := by rw [hRx, hRy]
_ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) (edPt B) edId 256 := hrfold
_ = dsmFold (nafDigit na) (nafDigit nb) (edPt A) edBasePt edId 256 := by
rw [hBpt]
end CurveFieldProofs

1473
verification/Proofs/DsmNafLoadSpec.lean Normal file
View file

File diff suppressed because it is too large Load diff

418
verification/Proofs/DsmNafLoopSpec.lean Normal file
View file

@ -0,0 +1,418 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/DsmNafLoopSpec.lean — NAF campaign, stage 3: the w=5 digit loop,
by induction on the remaining-bits measure (no unrolling).
State (naf, pos, carry); exact ℤ invariant (DsmNafMath):
carry ≤ 1 ∧ (carry = 1 → pos ≤ 254) ∧ digits ≥ pos all zero ∧
digit conditions ∧ nafSum naf 256 + carry·2^pos = V mod 2^pos.
One symbolic body-walk per induction step:
· `naf_bitbuf_spec` — the (single|cross)-word 64-bit read at bit pos,
4-way split on the word index, closed by naf_window_single/cross.
· `naf_update_spec` — the odd-digit write: hcast / wrapping_sub digit,
new carry ∈ {0,1}, exact digit value window − 32·carry′, oddness and
|d| < 16 (the strict lower bound needs the window's oddness).
· even step: pos+1 via naf_even_step / naf_carry_even;
odd step: pos+5 via nafSum_set / naf_odd_step / naf_carry_odd.
Exit (pos ≥ 256): naf_exit — the carry is provably dead and
nafSum naf 256 = V exactly (V < 2^253: canonical scalars, which is
what the mul call sites provide).
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.DsmNafMath
open Aeneas Aeneas.Std Result ControlFlow
open curve25519_dalek
set_option maxHeartbeats 8000000
set_option linter.unusedSimpArgs false
set_option maxRecDepth 8000
namespace CurveFieldProofs
open Aeneas.Std.WP
/-! ### Digit-array set plumbing -/
/-- Entries away from the written index are unchanged. -/
theorem nafDigit_set_ne (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ)
(d : Std.I8) (hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d)
(k : ℕ) (hk : k < 256) (hne : k ≠ pos) :
nafDigit naf' k = nafDigit naf k := by
have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
unfold nafDigit
rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) k
(by rw [List.length_set]; omega),
List.getElem_set_ne (by omega),
← getElem!_pos (↑naf : List Std.I8) k (by omega)]
/-- The written entry holds the new digit. -/
theorem nafDigit_set_eq (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ)
(d : Std.I8) (hpos : pos < 256)
(hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) :
nafDigit naf' pos = d.val := by
have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
unfold nafDigit
rw [hset, getElem!_pos ((↑naf : List Std.I8).set pos d) pos
(by rw [List.length_set]; omega),
List.getElem_set_self]
/-! ### The 64-bit window read and the digit write -/
/-- The 64-bit buffer read of the digit loop at bit position pos: its masked
value is the 5-bit window of V at pos. Four word cases (the fifth word is
the zero pad), each closed by naf_window_single (bit_idx < 59) or
naf_window_cross. -/
theorem naf_bitbuf_spec
(x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ)
(hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64])
(hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))))
(u bidx : Usize) (pos : ℕ) (hposv : pos < 256)
(hu : u.val = pos / 64) (hbidx : bidx.val = pos % 64) :
(if bidx < 59#usize
then do
let i1 ← Array.index_usize x_u64 u
i1 >>> bidx
else
do
let i1 ← Array.index_usize x_u64 u
let i2 ← i1 >>> bidx
let i3 ← 1#usize + u
let i4 ← Array.index_usize x_u64 i3
let i5 ← 64#usize - bidx
let i6 ← i4 <<< i5
ok (i2 ||| i6))
⦃ buf => buf.val % 32 = (V / 2^pos) % 32 ⦄ := by
have hb0 : v0.val < 2^64 := by scalar_tac
have hb1 : v1.val < 2^64 := by scalar_tac
have hb2 : v2.val < 2^64 := by scalar_tac
have hb3 : v3.val < 2^64 := by scalar_tac
have hulen : u.val < 4 := by clear * - hu hposv; omega
have hsz : (U64.size : ℕ) = 2^64 := by scalar_tac
split
· -- single-word read
rename_i hblt
have hbv : pos % 64 < 59 := by
have h := hbidx ▸ (show bidx.val < 59 by clear * - hblt; scalar_tac)
omega
step as ⟨w, hw⟩
step as ⟨buf, hbuf⟩
rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega)
with hc | hc | hc | hc
· have huv : u.val = 0 := by omega
simp only [hx, huv] at hw
simp at hw
rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by
rw [hVdef]; try ring
have h := naf_window_single V (0) v0.val (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) 0 (pos % 64)
hd (by norm_num) (by omega)
rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 1 := by omega
simp only [hx, huv] at hw
simp at hw
rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
rw [hVdef]; try ring
have h := naf_window_single V (v0.val) v1.val (v2.val + 2^64 * (v3.val + 2^64 * 0)) 64 (pos % 64)
hd (by omega) (by omega)
rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 2 := by omega
simp only [hx, huv] at hw
simp at hw
rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * 0)) := by
rw [hVdef]; try ring
have h := naf_window_single V (v0.val + 2^64 * v1.val) v2.val (v3.val + 2^64 * 0) 128 (pos % 64)
hd (by omega) (by omega)
rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 3 := by omega
simp only [hx, huv] at hw
simp at hw
rw [hbuf, hw, hbidx, Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * (0)) := by
rw [hVdef]; try ring
have h := naf_window_single V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val (0) 192 (pos % 64)
hd (by omega) (by omega)
rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· -- cross-word read
rename_i hbge
have hbv : 59 ≤ pos % 64 := by
have h : ¬ (bidx.val < 59) := by clear * - hbge; scalar_tac
omega
step as ⟨w, hw⟩
step as ⟨i2, hi2⟩
step as ⟨i3, hi3⟩
step as ⟨w', hw'⟩
step as ⟨i5, hi5⟩
step as ⟨i6, hi6⟩
try simp only [spec_ok]
rcases (show pos / 64 = 0 ∨ pos / 64 = 1 ∨ pos / 64 = 2 ∨ pos / 64 = 3 by omega)
with hc | hc | hc | hc
· have huv : u.val = 0 := by omega
have hi3v : i3.val = 1 := by clear * - hi3 huv; omega
simp only [hx, huv] at hw
simp at hw
simp only [hx, hi3v] at hw'
simp at hw'
rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
Nat.shiftRight_eq_div_pow]
have hd : V = 0 + 2^0 * (v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0)))) := by
rw [hVdef]; try simp; try ring
have h := naf_window_cross V (0) v0.val (v1.val) (v2.val + 2^64 * (v3.val + 2^64 * 0)) 0 (pos % 64)
hd (by norm_num) (by omega) (by omega)
rw [show (0 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 1 := by omega
have hi3v : i3.val = 2 := by clear * - hi3 huv; omega
simp only [hx, huv] at hw
simp at hw
simp only [hx, hi3v] at hw'
simp at hw'
rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
rw [hVdef]; try simp; try ring
have h := naf_window_cross V (v0.val) v1.val (v2.val) (v3.val + 2^64 * 0) 64 (pos % 64)
hd (by omega) (by omega) (by omega)
rw [show (64 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 2 := by omega
have hi3v : i3.val = 3 := by clear * - hi3 huv; omega
simp only [hx, huv] at hw
simp at hw
simp only [hx, hi3v] at hw'
simp at hw'
rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * v1.val + 2^128 * (v2.val + 2^64 * (v3.val + 2^64 * (0))) := by
rw [hVdef]; try simp; try ring
have h := naf_window_cross V (v0.val + 2^64 * v1.val) v2.val (v3.val) (0) 128 (pos % 64)
hd (by omega) (by omega) (by omega)
rw [show (128 : ℕ) + pos % 64 = pos from by omega] at h
exact h
· have huv : u.val = 3 := by omega
have hi3v : i3.val = 4 := by clear * - hi3 huv; omega
simp only [hx, huv] at hw
simp at hw
simp only [hx, hi3v] at hw'
simp at hw'
rw [UScalar.val_or, hi2, hi6, hi5, hbidx, hw, hw', hsz,
Nat.shiftRight_eq_div_pow]
have hd : V = v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * (v3.val + 2^64 * ((0#u64).val + 2^64 * (0))) := by
rw [hVdef]; try simp; try ring
have h := naf_window_cross V (v0.val + 2^64 * v1.val + 2^128 * v2.val) v3.val ((0#u64).val) (0) 192 (pos % 64)
hd (by omega) (by omega) (by omega)
rw [show (192 : ℕ) + pos % 64 = pos from by omega] at h
exact h
/-- The odd-digit write: hcast (or hcast + wrapping_sub) produces the digit
window − 32·carry′ with carry′ the ≥16 indicator; the digit is odd with
|d| < 16, and the entry is written at pos. -/
theorem naf_update_spec (naf : Std.Array Std.I8 256#usize) (pos : Usize) (window : Std.U64)
(hpos : pos.val < 256) (hwle : window.val ≤ 32) (hwodd : window.val % 2 = 1) :
(if window < 16#u64
then do
let i4 ← lift (UScalar.hcast .I8 window)
let a ← Array.update naf pos i4
ok (a, 0#u64)
else
do
let i4 ← lift (UScalar.hcast .I8 window)
let i5 ← lift (UScalar.hcast .I8 32#u64)
let i6 ← lift (core.num.I8.wrapping_sub i4 i5)
let a ← Array.update naf pos i6
ok (a, 1#u64))
⦃ p => ∃ d : Std.I8, (↑p.1 : List Std.I8) = (↑naf : List Std.I8).set pos.val d ∧
p.2.val ≤ 1 ∧
(d.val : ℤ) = (window.val : ℤ) - 32 * (p.2.val : ℤ) ∧
d.val % 2 = 1 ∧ -16 < d.val ∧ d.val < 16 ∧
((window.val < 16 ∧ p.2.val = 0) ∨ (16 ≤ window.val ∧ p.2.val = 1)) ⦄ := by
split
· rename_i hlt
have hltv : window.val < 16 := by clear * - hlt; scalar_tac
step with (UScalar.hcast_inBounds_spec .I8 window
(by clear * - hltv; scalar_tac)) as ⟨d, hd⟩
step as ⟨a, ha⟩
try simp only [spec_ok]
refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hd], ?_, ?_, ?_,
Or.inl ⟨hltv, by simp⟩⟩
· rw [hd]; clear * - hwodd; omega
· rw [hd]; push_cast; omega
· rw [hd]; clear * - hltv; omega
· rename_i hge
have hgev : 16 ≤ window.val := by clear * - hge; scalar_tac
step with (UScalar.hcast_inBounds_spec .I8 window
(by clear * - hwle; scalar_tac)) as ⟨d0, hd0⟩
step with (UScalar.hcast_inBounds_spec .I8 32#u64
(by scalar_tac)) as ⟨t32, ht32⟩
step as ⟨d, hd⟩
step as ⟨a, ha⟩
try simp only [spec_ok]
have hdv : (d.val : ℤ) = (window.val : ℤ) - 32 := by
rw [hd]
simp only [core.num.I8.wrapping_sub_val_eq, hd0, ht32]
have hb := Aeneas.Arith.Int.bmod_pow2_eq_of_inBounds' 8 ((window.val : ℤ) - 32)
(by norm_num) (by clear * - ; push_cast; omega)
(by clear * - hwle; push_cast; omega)
push_cast at hb ⊢
convert hb using 2 <;> norm_num
refine ⟨d, by rw [ha, Array.set_val_eq], by simp, by simp [hdv], ?_, ?_, ?_,
Or.inr ⟨hgev, by simp⟩⟩
· rw [hdv]; clear * - hwodd hgev; omega
· rw [hdv]; clear * - hgev hwodd; push_cast; omega
· rw [hdv]; clear * - hwle; omega
/-! ### The digit loop -/
/-- **The w=5 NAF digit loop**, by induction on the remaining-bits measure.
From any state satisfying the invariant, the loop returns a digit array
with the NAF digit conditions and exact value V. -/
theorem naf_digit_loop_spec
(x_u64 : Std.Array Std.U64 5#usize) (v0 v1 v2 v3 : Std.U64) (V : ℕ)
(hx : (↑x_u64 : List Std.U64) = [v0, v1, v2, v3, 0#u64])
(hVdef : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))))
(hV : V < 2^253) (m : ℕ) :
∀ (naf : Std.Array Std.I8 256#usize) (pos : Usize) (carry : Std.U64),
256 - pos.val ≤ m →
carry.val ≤ 1 →
(carry.val = 1 → pos.val ≤ 254) →
(∀ k, pos.val ≤ k → k < 256 → nafDigit naf k = 0) →
(∀ k, k < 256 → (nafDigit naf k = 0 ∨ nafDigit naf k % 2 = 1) ∧
-16 < nafDigit naf k ∧ nafDigit naf k < 16) →
nafSum naf 256 + carry.val * 2^pos.val = ((V % 2^pos.val : ℕ) : ℤ) →
scalar.Scalar.non_adjacent_form_loop1 5#usize naf x_u64 32#u64 31#u64 pos carry
⦃ res => NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by
induction m with
| zero =>
intro naf pos carry hm hc hcp hzero hdig hinv
unfold scalar.Scalar.non_adjacent_form_loop1
apply loop_step
simp only [scalar.Scalar.non_adjacent_form_loop1.body]
have hguard : ¬ (pos < 256#usize) := by clear * - hm; scalar_tac
rw [if_neg hguard]
try simp only [spec_ok]
exact ⟨hdig, naf_exit V pos.val carry.val _ hV (by clear * - hm; omega) hc hcp hinv⟩
| succ m ih =>
intro naf pos carry hm hc hcp hzero hdig hinv
unfold scalar.Scalar.non_adjacent_form_loop1
apply loop_step
simp only [scalar.Scalar.non_adjacent_form_loop1.body]
by_cases hguard : pos < 256#usize
swap
· -- exit branch (measure slack)
rw [if_neg hguard]
try simp only [spec_ok]
have hge : 256 ≤ pos.val := by clear * - hguard; scalar_tac
exact ⟨hdig, naf_exit V pos.val carry.val _ hV hge hc hcp hinv⟩
· rw [if_pos hguard]
have hposv : pos.val < 256 := by clear * - hguard; scalar_tac
-- u64_idx ← pos / 64 ; bit_idx ← pos % 64 ; i ← 64 − 5
step as ⟨u, hu⟩
step as ⟨bidx, hbidx⟩
step as ⟨i59, hi59⟩
have hi59v : i59 = 59#usize := by clear * - hi59; scalar_tac
rw [hi59v]
-- bit_buf: the 5-bit window of V at pos
step with (naf_bitbuf_spec x_u64 v0 v1 v2 v3 V hx hVdef u bidx pos.val
hposv hu hbidx) as ⟨buf, hbuf⟩
-- i1 ← buf &&& 31 : the masked window
step as ⟨msk, hmsk⟩
have hmskv : msk.val = (V / 2^pos.val) % 32 := by
rw [hmsk, UScalar.val_and]
rw [show (31#u64).val = 2^5 - 1 by scalar_tac,
Nat.and_two_pow_sub_one_eq_mod]
rw [show (2:ℕ)^5 = 32 from by norm_num]
exact hbuf
-- window ← carry + msk
step as ⟨win, hwin⟩
have hwinv : win.val = carry.val + (V / 2^pos.val) % 32 := by
rw [hwin, hmskv]
have hwle : win.val ≤ 32 := by clear * - hwinv hc; omega
-- i2 ← win &&& 1 : the parity bit
step as ⟨par, hpar⟩
have hparv : par.val = win.val % 2 := by
rw [hpar, UScalar.val_and]
rw [show (1#u64).val = 2^1 - 1 by scalar_tac,
Nat.and_two_pow_sub_one_eq_mod]
try norm_num
split
· -- EVEN window: digit 0, pos+1, carry unchanged
rename_i hz
have heven : (carry.val + (V / 2^pos.val) % 32) % 2 = 0 := by
have h : par.val = 0 := by rw [hz]; simp
rw [← hwinv, ← hparv]
exact h
step as ⟨pos1, hpos1⟩
have hpos1v : pos1.val = pos.val + 1 := by clear * - hpos1; omega
try simp only [spec_ok]
apply ih naf pos1 carry (by clear * - hm hpos1v; omega) hc
(fun h1 => by have := naf_carry_even V pos.val carry.val hV hc heven h1
clear * - this hpos1v; omega)
(fun k hk1 hk2 => hzero k (by clear * - hk1 hpos1v; omega) hk2)
hdig
(by rw [hpos1v]
exact naf_even_step V pos.val carry.val _ hc hinv heven)
· -- ODD window: write digit, pos+5, carry from the ≥16 test
rename_i hnz
have hwodd : win.val % 2 = 1 := by
have h : par.val ≠ 0 := by
clear * - hnz
intro h
exact hnz (by scalar_tac)
clear * - h hparv
omega
-- i3 ← 32 / 2 (= 16)
step as ⟨h16, hh16⟩
have hh16v : h16 = 16#u64 := by clear * - hh16; scalar_tac
rw [hh16v]
-- the digit write (both branches of the < 16 test)
step with (naf_update_spec naf pos win hposv hwle hwodd) as
⟨d, naf1, carry1, hset, hc1, hdval, hdodd, hdlo, hdhi, hcase⟩
-- pos1 ← pos + 5
step as ⟨pos1, hpos1⟩
have hpos1v : pos1.val = pos.val + 5 := by clear * - hpos1; scalar_tac
try simp only [spec_ok]
-- the digit facts at the written index and away from it
have holdz : nafDigit naf pos.val = 0 :=
hzero pos.val (le_refl _) hposv
have hsum1 : nafSum naf1 256 = nafSum naf 256 + d.val * 2^pos.val :=
nafSum_set naf naf1 pos.val d hposv holdz hset
have hdig1 : ∀ k, k < 256 → nafDigit naf1 k =
if k = pos.val then d.val else nafDigit naf k := by
intro k hk
by_cases h : k = pos.val
· subst h
rw [nafDigit_set_eq naf naf1 pos.val d hk hset, if_pos rfl]
· rw [nafDigit_set_ne naf naf1 pos.val d hset k hk h, if_neg h]
-- the window as a ℕ fact for the step lemmas
have hwcase : (carry.val + (V / 2^pos.val) % 32 < 16 ∧ carry1.val = 0) ∨
(16 ≤ carry.val + (V / 2^pos.val) % 32 ∧ carry1.val = 1) := by
rw [← hwinv]
exact hcase
apply ih naf1 pos1 carry1 (by clear * - hm hpos1v; omega) hc1
(fun h1 => by
have := naf_carry_odd V pos.val carry.val carry1.val hV hc hwcase h1
clear * - this hpos1v; omega)
(fun k hk1 hk2 => by
rw [hdig1 k hk2, if_neg (by clear * - hk1 hpos1v hposv; omega)]
exact hzero k (by clear * - hk1 hpos1v; omega) hk2)
(fun k hk => by
rw [hdig1 k hk]
by_cases h : k = pos.val
· rw [if_pos h]
exact ⟨Or.inr hdodd, hdlo, hdhi⟩
· rw [if_neg h]
exact hdig k hk)
(by rw [hpos1v, hsum1]
have hd' : (d.val : ℤ) = (carry.val : ℤ) +
((V / 2^pos.val) % 32 : ℕ) - 32 * carry1.val := by
rw [hdval, hwinv]
push_cast
ring
exact naf_odd_step V pos.val carry.val carry1.val _ d.val hinv hd')
end CurveFieldProofs

239
verification/Proofs/DsmNafMath.lean Normal file
View file

@ -0,0 +1,239 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/DsmNafMath.lean — NAF campaign, stage 2: the pure arithmetic core
of the w=5 NAF digit loop (no extraction dependence beyond `nafDigit`).
The digit loop's state is (naf, pos, carry) with the exact ℤ invariant
nafSum naf 256 + carry·2^pos = V mod 2^pos
(digits at k ≥ pos all zero, carry ≤ 1, and carry = 1 → pos ≤ 254 given
V < 2^253 — the component that kills the carry at exit).
Step theorems the monadic walk plugs in:
· `nafSum_set` — writing a fresh digit adds d·2^pos to the sum.
· `div_pow_shift` / `mod32_absorb` / `naf_window_single` / `naf_window_cross`
— the 64-bit buffer read at bit position p+b sees (V >> (p+b)) mod 32
(single word when b + 5 ≤ 64; cross-word via disjoint-OR otherwise).
· `naf_even_step` — even window ⇒ pos+1, carry preserved (the parity
of V >> pos matches carry, so both sides absorb carry·2^(pos+1)).
· `naf_odd_step` — odd window ⇒ digit (window − 32·carry'), pos+5:
the digit plus the new carry reconstruct the 5 consumed bits
(Nat.mod_mul telescoping).
· `naf_carry_even` / `naf_carry_odd` — carry = 1 → pos ≤ 254 propagation
from V < 2^253.
· `naf_exit` — pos ≥ 256 kills the carry: nafSum = V exactly.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.DsmLoopSpec
open Aeneas Aeneas.Std
open curve25519_dalek
set_option maxHeartbeats 4000000
set_option linter.unusedSimpArgs false
set_option maxRecDepth 8000
namespace CurveFieldProofs
/-! ### The signed digit sum -/
/-- Σ_{k<m} naf[k]·2^k over ℤ — the value a digit array denotes. -/
def nafSum (naf : Std.Array Std.I8 256#usize) (m : ℕ) : ℤ :=
∑ k ∈ Finset.range m, nafDigit naf k * 2^k
/-- Setting entry `pos` (previously 0) adds d·2^pos to the full sum. -/
theorem nafSum_set (naf naf' : Std.Array Std.I8 256#usize) (pos : ℕ) (d : Std.I8)
(hpos : pos < 256) (hold : nafDigit naf pos = 0)
(hset : (↑naf' : List Std.I8) = (↑naf : List Std.I8).set pos d) :
nafSum naf' 256 = nafSum naf 256 + d.val * 2^pos := by
have hlen : (↑naf : List Std.I8).length = 256 := by scalar_tac
have hlen' : ((↑naf : List Std.I8).set pos d).length = 256 := by
rw [List.length_set]; exact hlen
have hdig : ∀ k, k < 256 → nafDigit naf' k =
if k = pos then d.val else nafDigit naf k := by
intro k hk
unfold nafDigit
rw [hset]
by_cases h : k = pos
· subst h
rw [getElem!_pos ((↑naf : List Std.I8).set k d) k (by omega),
List.getElem_set_self]
simp
· rw [getElem!_pos ((↑naf : List Std.I8).set pos d) k (by omega),
List.getElem_set_ne (by omega),
← getElem!_pos (↑naf : List Std.I8) k (by omega)]
rw [if_neg h]
unfold nafSum
have hmem : pos ∈ Finset.range 256 := Finset.mem_range.mpr hpos
rw [← Finset.sum_erase_add _ _ hmem, ← Finset.sum_erase_add _ _ hmem]
have hcongr : ∑ k ∈ (Finset.range 256).erase pos, nafDigit naf' k * 2^k
= ∑ k ∈ (Finset.range 256).erase pos, nafDigit naf k * 2^k := by
apply Finset.sum_congr rfl
intro k hk
rw [hdig k (Finset.mem_range.mp (Finset.mem_of_mem_erase hk)),
if_neg (Finset.ne_of_mem_erase hk)]
rw [hcongr, hdig pos hpos, if_pos rfl, hold]
ring
/-! ### Window-read arithmetic -/
/-- Dividing the three-part value lo + 2^p·(w + 2^64·rest) by 2^(p+b)
(b ≤ 64, lo < 2^p) yields w >> b plus the rest shifted down. -/
theorem div_pow_shift (lo w rest p b : ℕ) (hlo : lo < 2^p) (hb : b ≤ 64) :
(lo + 2^p * (w + 2^64 * rest)) / 2^(p+b) = w / 2^b + 2^(64-b) * rest := by
have hp : (0:ℕ) < 2^p := Nat.two_pow_pos p
have hbp : (0:ℕ) < 2^b := Nat.two_pow_pos b
rw [pow_add, ← Nat.div_div_eq_div_mul]
have h1 : (lo + 2^p * (w + 2^64 * rest)) / 2^p = w + 2^64 * rest := by
rw [Nat.add_mul_div_left _ _ hp, Nat.div_eq_of_lt hlo, Nat.zero_add]
rw [h1]
have h2 : (2:ℕ)^64 = 2^b * 2^(64-b) := by
rw [← pow_add]; congr 1; omega
rw [h2, Nat.mul_assoc, Nat.add_mul_div_left _ _ hbp]
/-- Multiples of 2^m (m ≥ 5) vanish mod 32. -/
theorem mod32_absorb (x y m : ℕ) (hm : 5 ≤ m) :
(x + 2^m * y) % 32 = x % 32 := by
have h : (2:ℕ)^m = 32 * 2^(m-5) := by
rw [show (32:ℕ) = 2^5 by norm_num, ← pow_add]; congr 1; omega
rw [h, Nat.mul_assoc, Nat.add_mul_mod_self_left]
/-- Single-word window read: when the 5-bit window at bit b fits inside
word w (b + 5 ≤ 64), (w >> b) mod 32 is the value's window at p+b. -/
theorem naf_window_single (V lo w rest p b : ℕ)
(hV : V = lo + 2^p * (w + 2^64 * rest)) (hlo : lo < 2^p) (hb : b + 5 ≤ 64) :
(w / 2^b) % 32 = (V / 2^(p+b)) % 32 := by
rw [hV, div_pow_shift lo w rest p b hlo (by omega)]
exact (mod32_absorb _ _ _ (by omega)).symm
/-- Cross-word window read: when the window at bit b straddles into the next
word w' (b ≥ 60), the extracted read (w >> b) ||| ((w' << (64−b)) mod 2^64)
still sees the value's window at p+b, mod 32. -/
theorem naf_window_cross (V lo w w' rest p b : ℕ)
(hV : V = lo + 2^p * (w + 2^64 * (w' + 2^64 * rest)))
(hlo : lo < 2^p) (hw : w < 2^64) (hb : b < 64) :
((w / 2^b) ||| (w' <<< (64 - b)) % 2^64) % 32 = (V / 2^(p+b)) % 32 := by
have hp64 : (2:ℕ)^(64-b) * 2^b = 2^64 := by
rw [← pow_add]; congr 1; omega
have hp128 : (2:ℕ)^(64-b) * 2^64 = 2^(128-b) := by
rw [← pow_add]; congr 1; omega
-- the truncated shift: (w' << (64−b)) mod 2^64 = 2^(64−b)·(w' mod 2^b)
have hsh : (w' <<< (64 - b)) % 2^64 = 2^(64-b) * (w' % 2^b) := by
rw [Nat.shiftLeft_eq, Nat.mul_comm w' _, ← hp64, Nat.mul_mod_mul_left]
-- the OR is disjoint: w >> b < 2^(64−b)
have hdl : w / 2^b < 2^(64-b) := by
rw [Nat.div_lt_iff_lt_mul (Nat.two_pow_pos b)]
calc w < 2^64 := hw
_ = 2^(64-b) * 2^b := hp64.symm
have hor := Nat.two_pow_add_eq_or_of_lt (b := w / 2^b) (i := 64-b) hdl (w' % 2^b)
rw [hsh, Nat.lor_comm, ← hor]
-- the value side
rw [hV, div_pow_shift lo w _ p b hlo (by omega)]
-- both sides are (w/2^b + 2^(64−b)·(w' mod 2^b)) mod 32 after absorbing
-- the 2^64-multiples: w' = w' mod 2^b + 2^b·(w'/2^b)
have hw' : w' = w' % 2^b + 2^b * (w' / 2^b) := (Nat.mod_add_div _ _).symm
have e1 : w / 2^b + 2^(64-b) * (w' + 2^64 * rest)
= (2^(64-b) * (w' % 2^b) + w / 2^b)
+ 2^64 * (w' / 2^b + 2^(64-b) * rest) := by
conv_lhs => rw [hw']
rw [Nat.mul_add, Nat.mul_add, Nat.mul_add, ← Nat.mul_assoc, hp64,
← Nat.mul_assoc, hp128]
have hp128' : (2:ℕ)^(128-b) = 2^64 * 2^(64-b) := by
rw [← pow_add]; congr 1; omega
rw [hp128']
ring
rw [e1]
have := mod32_absorb (2^(64-b) * (w' % 2^b) + w / 2^b)
(w' / 2^b + 2^(64-b) * rest) 64 (by omega)
rw [this]
/-! ### Invariant step theorems -/
/-- Even window: digit 0, position advances by 1, carry preserved.
The parity of V >> pos equals the carry, so the invariant extends. -/
theorem naf_even_step (V pos : ℕ) (carry : ℕ) (S : ℤ)
(hc : carry ≤ 1)
(hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ))
(heven : (carry + (V / 2^pos) % 32) % 2 = 0) :
S + carry * 2^(pos+1) = ((V % 2^(pos+1) : ℕ) : ℤ) := by
have hmm : V % 2^(pos+1) = V % 2^pos + 2^pos * ((V / 2^pos) % 2) := by
rw [pow_succ, Nat.mod_mul]
have hpar : (V / 2^pos) % 2 = carry := by omega
rw [hmm, hpar]
push_cast at hinv ⊢
linear_combination hinv
/-- Odd window: digit window − 32·carry', position advances by 5.
The digit plus the promoted carry reconstruct the 5 consumed bits. -/
theorem naf_odd_step (V pos : ℕ) (carry carry' : ℕ) (S d : ℤ)
(hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ))
(hd : d = (carry : ℤ) + ((V / 2^pos) % 32 : ℕ) - 32 * carry') :
(S + d * 2^pos) + carry' * 2^(pos+5) = ((V % 2^(pos+5) : ℕ) : ℤ) := by
have hmm : V % 2^(pos+5) = V % 2^pos + 2^pos * ((V / 2^pos) % 32) := by
have h : (2:ℕ)^(pos+5) = 2^pos * 32 := by rw [pow_add]; norm_num
rw [h, Nat.mod_mul]
rw [hmm, hd]
push_cast at hinv ⊢
linear_combination hinv
/-- Carry propagation, even step: with V < 2^253, an even step that keeps
carry = 1 must be reading a set bit, so pos ≤ 252 and pos+1 ≤ 254. -/
theorem naf_carry_even (V pos : ℕ) (carry : ℕ) (hV : V < 2^253)
(hc : carry ≤ 1)
(heven : (carry + (V / 2^pos) % 32) % 2 = 0) :
carry = 1 → pos + 1 ≤ 254 := by
intro h1
subst h1
have h3 : 1 ≤ (V / 2^pos) % 32 := by
generalize (V / 2^pos) % 32 = r at heven ⊢
omega
have hge : 1 ≤ V / 2^pos := le_trans h3 (Nat.mod_le _ _)
have hle : 2^pos ≤ V := by
have h5 := (Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge
simpa using h5
have hpb : pos ≤ 252 := by
by_contra h
have h253 : (2:ℕ)^253 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
exact absurd (lt_of_le_of_lt (le_trans h253 hle) hV) (lt_irrefl _)
omega
/-- Carry propagation, odd step: producing carry' = 1 needs window ≥ 16, so
V >> pos ≥ 15, forcing pos ≤ 249 (V < 2^253) and pos+5 ≤ 254. -/
theorem naf_carry_odd (V pos : ℕ) (carry carry' : ℕ) (hV : V < 2^253)
(hc : carry ≤ 1)
(hcw : (carry + (V / 2^pos) % 32 < 16 ∧ carry' = 0) ∨
(16 ≤ carry + (V / 2^pos) % 32 ∧ carry' = 1)) :
carry' = 1 → pos + 5 ≤ 254 := by
intro h1
rcases hcw with ⟨-, h0⟩ | ⟨hge, -⟩
· omega
· have h15 : 15 ≤ (V / 2^pos) % 32 := by
generalize (V / 2^pos) % 32 = r at hge ⊢
omega
have hge15 : 15 ≤ V / 2^pos := le_trans h15 (Nat.mod_le _ _)
have hmul : 15 * 2^pos ≤ V :=
(Nat.le_div_iff_mul_le (Nat.two_pow_pos pos)).mp hge15
have hpb : pos ≤ 249 := by
by_contra h
have h250 : (2:ℕ)^250 ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
have hbig : (2:ℕ)^253 < 15 * 2^250 := by norm_num
have hmono : 15 * 2^250 ≤ 15 * 2^pos := Nat.mul_le_mul_left 15 h250
exact absurd (lt_of_le_of_lt (le_trans hmono hmul) hV) (not_lt.mpr hbig.le)
omega
/-- Exit: at pos ≥ 256 the carry must be dead (carry = 1 forces pos ≤ 254),
and V mod 2^pos = V, so the digit sum equals V exactly. -/
theorem naf_exit (V pos : ℕ) (carry : ℕ) (S : ℤ) (hV : V < 2^253)
(hpos : 256 ≤ pos) (hc : carry ≤ 1) (hcp : carry = 1 → pos ≤ 254)
(hinv : S + carry * 2^pos = ((V % 2^pos : ℕ) : ℤ)) : S = V := by
have hc0 : carry = 0 := by
by_contra h
have h1 : carry = 1 := by omega
have := hcp h1
omega
subst hc0
have hmod : V % 2^pos = V := by
apply Nat.mod_eq_of_lt
calc V < 2^253 := hV
_ ≤ 2^pos := Nat.pow_le_pow_right (by norm_num) (by omega)
rw [hmod] at hinv
push_cast at hinv
linarith
end CurveFieldProofs

84
verification/Proofs/DsmNafSpec.lean Normal file
View file

@ -0,0 +1,84 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/DsmNafSpec.lean — NAF campaign, stage 4: the public spec of
`Scalar::non_adjacent_form(5)`.
Composes the proven stages: both entry masserts DISCHARGED (w = 5 is in
[2,8]), the LE byte→word load (DsmNafLoadSpec), width = 1<<<5 = 32 and
window_mask = 31 computed, and the digit loop (DsmNafLoopSpec) seeded
with the all-zeros state whose invariant is trivial.
POST: the 256 digits satisfy the NAF conditions (odd-or-zero, |d| < 16 —
exactly `NafDigits`, what dsm_loop_spec consumes) and their signed sum
reconstructs the scalar's little-endian byte value EXACTLY:
nafSum res 256 = V (as integers, no modular slack).
Requires V < 2^253 — canonical scalars, which the mul call sites provide.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.DsmNafLoadSpec
import Proofs.DsmNafLoopSpec
open Aeneas Aeneas.Std Result ControlFlow
open curve25519_dalek
set_option maxHeartbeats 8000000
set_option linter.unusedSimpArgs false
set_option maxRecDepth 8000
namespace CurveFieldProofs
open Aeneas.Std.WP
/-- **Scalar::non_adjacent_form(5)**: for a scalar whose 32-byte LE value V
is below 2^253, the result is a 256-entry NAF digit array — every digit
odd or zero with |d| < 16, and Σ naf[k]·2^k = V exactly. Both entry
masserts are discharged. -/
theorem non_adjacent_form_spec (self : scalar.Scalar)
(b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 : Std.U8)
(hb : (↑self.bytes : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, b21, b22, b23, b24, b25, b26, b27, b28, b29, b30, b31])
(V : ℕ)
(hVbytes : V = b0.val + b1.val * 2^8 + b2.val * 2^16 + b3.val * 2^24 + b4.val * 2^32 + b5.val * 2^40 + b6.val * 2^48 + b7.val * 2^56 + b8.val * 2^64 + b9.val * 2^72 + b10.val * 2^80 + b11.val * 2^88 + b12.val * 2^96 + b13.val * 2^104 + b14.val * 2^112 + b15.val * 2^120 + b16.val * 2^128 + b17.val * 2^136 + b18.val * 2^144 + b19.val * 2^152 + b20.val * 2^160 + b21.val * 2^168 + b22.val * 2^176 + b23.val * 2^184 + b24.val * 2^192 + b25.val * 2^200 + b26.val * 2^208 + b27.val * 2^216 + b28.val * 2^224 + b29.val * 2^232 + b30.val * 2^240 + b31.val * 2^248)
(hV : V < 2^253) :
scalar.Scalar.non_adjacent_form self 5#usize ⦃ res =>
NafDigits res ∧ nafSum res 256 = (V : ℤ) ⦄ := by
unfold scalar.Scalar.non_adjacent_form
step with (massert_spec (5#usize ≥ 2#usize) (by scalar_tac)) as ⟨h2⟩
step with (massert_spec (5#usize ≤ 8#usize) (by scalar_tac)) as ⟨h8⟩
-- the LE load fills x_u64[0..3]; word 4 stays 0
step with (naf_load_spec self (Array.repeat 5#usize 0#u64)
b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31
hb (by simp [List.replicate])) as ⟨v0, v1, v2, v3, ws, hws, hv0, hv1, hv2, hv3⟩
-- width ← 1 <<< 5 (= 32), window_mask ← width − 1 (= 31)
step as ⟨wd, hwd⟩
have hwdv : wd = 32#u64 := by clear * - hwd; scalar_tac
rw [hwdv]
step as ⟨mk, hmk⟩
have hmkv : mk = 31#u64 := by clear * - hmk; scalar_tac
rw [hmkv]
-- the initial all-zeros digit state
have hz : ∀ k, k < 256 → nafDigit (Array.repeat 256#usize 0#i8) k = 0 := by
intro k hk
unfold nafDigit
rw [getElem!_pos (↑(Array.repeat 256#usize 0#i8) : List Std.I8) k
(by simp; omega)]
simp only [Array.repeat_val, List.getElem_replicate]
simp
have hsum0 : nafSum (Array.repeat 256#usize 0#i8) 256 = 0 := by
unfold nafSum
apply Finset.sum_eq_zero
intro k hk
rw [hz k (Finset.mem_range.mp hk)]
ring
-- the word-form value
have hVw : V = v0.val + 2^64 * (v1.val + 2^64 * (v2.val + 2^64 * (v3.val + 2^64 * 0))) := by
rw [hVbytes, hv0, hv1, hv2, hv3]
ring
-- the digit loop from the trivial invariant
apply naf_digit_loop_spec ws v0 v1 v2 v3 V hws hVw hV 256
(Array.repeat 256#usize 0#i8) 0#usize 0#u64
(by scalar_tac)
(by scalar_tac)
(by intro h; simp at h)
(fun k _ hk => hz k hk)
(fun k hk => ⟨Or.inl (hz k hk), by rw [hz k hk]; norm_num,
by rw [hz k hk]; norm_num⟩)
(by simp [hsum0])
end CurveFieldProofs

13
verification/check.sh
View file

@ -54,6 +54,11 @@ PROOFS=(
DsmTableSpec
DsmStepSpec
DsmLoopSpec
DsmNafLoadSpec
DsmNafMath
DsmNafLoopSpec
DsmNafSpec
DsmMulSpec
)
# Fully-qualified certificate names; each must be axiom-clean.
CERTS=(
@ -66,6 +71,12 @@ CERTS=(
CurveFieldProofs.dsm_step_p_law
CurveFieldProofs.dsm_step_b_law
CurveFieldProofs.dsm_loop_spec
CurveFieldProofs.naf_load_spec
CurveFieldProofs.naf_exit
CurveFieldProofs.naf_digit_loop_spec
CurveFieldProofs.non_adjacent_form_spec
CurveFieldProofs.run_basepoint
CurveFieldProofs.vartime_double_base_mul_spec
)
# Imports needed so every certificate in CERTS is in scope for the audit.
AUDIT_IMPORTS=(
@ -74,6 +85,8 @@ AUDIT_IMPORTS=(
Proofs.DsmTableSpec
Proofs.DsmStepSpec
Proofs.DsmLoopSpec
Proofs.DsmNafSpec
Proofs.DsmMulSpec
)
# ── Phase 0: resource + integrity guards ────────────────────────────────────

8
verification/gen/CurveField/FunsExternal.lean
View file

@ -330,14 +330,6 @@ axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::backend::serial::scalar_mul::vartime_double_base::mul]:
Source: 'curve25519-dalek/src/backend/serial/scalar_mul/vartime_double_base.rs', lines 23:0-72:1
Visibility: public -/
axiom backend.serial.scalar_mul.vartime_double_base.mul
:
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1
Visibility: public -/