mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
Double-scalar-mul proof campaign, bricks 1-3: table, digit step, loop
Three new proof files over the CurveField extraction, composing the proven group-law layer (no new axioms, no associativity assumed — computational layering over the abstract `edAdd`): - `Proofs/DsmTableSpec.lean` — `NafLookupTable5::from(&A)`: the 8 entries are valid `ProjectiveNielsPoint` caches of valid on-curve points denoting the odd multiples A, 3A, ..., 15A as the `edOdd` double-and-add recursion. 7 explicit loop peels over edwards_as_projective_niels_spec / add_projniels_law / compl_as_extended_law, seeded by edwards_double_law. `select`: both masserts (x odd, x < 16) DISCHARGED — panic-freedom is proven, not assumed; post enumerates all 8 digit cases. - `Proofs/DsmStepSpec.lean` — `proj_double_law` (the projective doubling denotes `edAdd P P`; same Z^2-scaled linear_combination discipline as the extended-coordinate law), `compl_as_projective_law` ((X:Z),(Y:T) to (XT:YZ:ZT) preserves the point), `naf_select_entry` (digit-indexed lookup returns THE entry: NafEntryOf r A ((x-1)/2)), and `dsm_step_p_law` / `dsm_step_b_law`: the three-way NAF digit step denotes `edDigit` — add the d-th odd multiple, add its negation, or pass through. - `Proofs/DsmLoopSpec.lean` — the 256-iteration Straus loop by GENUINE induction on the counter (one symbolic body walk, no unrolling): `dsm_loop_spec` — from the identity, the loop returns a valid on-curve point denoting `dsmFold ... edId 256`, the abstract double-and-add fold of both digit arrays over the table points. Digit and table hypotheses are exactly what the NAF spec and naf_table_spec provide (layering). check.sh wired: PROOFS + AUDIT_IMPORTS + 7 new CERTS (naf_table_spec, naf_select_spec, proj_double_law, compl_as_projective_law, dsm_step_p_law, dsm_step_b_law, dsm_loop_spec), each `#print axioms`-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:
parent
09ed72ad54
commit
df39ab92f1
4 changed files with 1029 additions and 0 deletions
216
verification/Proofs/DsmLoopSpec.lean
Normal file
216
verification/Proofs/DsmLoopSpec.lean
Normal file
|
|
@ -0,0 +1,216 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/DsmLoopSpec.lean — double-scalar-mul campaign, brick 3:
|
||||
the 256-iteration Straus/NAF loop, by genuine induction (no unrolling).
|
||||
|
||||
dsm_loop seeds r = identity, j = top+1 and runs
|
||||
while j > 0 { idx = j-1; t = r.double();
|
||||
t = dsm_step_p(t, table_a, a_naf[idx]);
|
||||
t = dsm_step_b(t, table_b, b_naf[idx]);
|
||||
r = t.as_projective(); j = idx; }
|
||||
|
||||
ABSTRACTION: `dsmFold aD bD pA pB P j` — process digits j−1 … 0 onto the
|
||||
accumulator P over the abstract Edwards addition: each iteration doubles
|
||||
and applies the two digits through `edDigit` (DsmStepSpec). The loop
|
||||
invariant is
|
||||
ProjValid r ∧ OnCurve (projPt r) ∧ result = dsmFold … (projPt r) j
|
||||
proven by induction on j.val, one symbolic body-walk per induction step:
|
||||
proj_double_law → dsm_step_p_law → dsm_step_b_law → compl_as_projective_law.
|
||||
|
||||
Digit hypotheses (odd-or-zero, |d| < 16, for all 256 positions of both
|
||||
arrays) are exactly what the NAF spec will provide (layering). Table
|
||||
hypotheses are naf_table_spec's post for both tables.
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.DsmStepSpec
|
||||
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
|
||||
|
||||
/-! ### The abstract double-and-add fold -/
|
||||
|
||||
/-- The k-th NAF digit of an extracted digit array, as an integer. -/
|
||||
def nafDigit (a : Std.Array Std.I8 256#usize) (k : ℕ) : ℤ := (a.val[k]!).val
|
||||
|
||||
/-- `dsmFold aD bD pA pB P j`: apply digits j−1, j−2, …, 0 to accumulator P —
|
||||
per digit: double, add aD's digit-multiple of pA, add bD's digit-multiple
|
||||
of pB (all through `edDigit`, over the abstract `edAdd`). -/
|
||||
noncomputable def dsmFold (aD bD : ℕ → ℤ) (pA pB : Fp × Fp) :
|
||||
(Fp × Fp) → ℕ → Fp × Fp
|
||||
| P, 0 => P
|
||||
| P, j + 1 => dsmFold aD bD pA pB
|
||||
(edDigit pB (bD j) (edDigit pA (aD j) (edAdd P P))) j
|
||||
|
||||
@[simp] theorem dsmFold_zero (aD bD : ℕ → ℤ) (pA pB P : Fp × Fp) :
|
||||
dsmFold aD bD pA pB P 0 = P := rfl
|
||||
|
||||
theorem dsmFold_succ (aD bD : ℕ → ℤ) (pA pB P : Fp × Fp) (j : ℕ) :
|
||||
dsmFold aD bD pA pB P (j + 1) = dsmFold aD bD pA pB
|
||||
(edDigit pB (bD j) (edDigit pA (aD j) (edAdd P P))) j := rfl
|
||||
|
||||
/- The neutral point is on the curve: `onCurve_id` (EdCurve.lean). -/
|
||||
|
||||
/-- Digit-array contract: every position is a NAF digit — odd or zero,
|
||||
magnitude below 16. (The NAF spec provides this; layering.) -/
|
||||
def NafDigits (a : Std.Array Std.I8 256#usize) : Prop :=
|
||||
∀ k : ℕ, k < 256 →
|
||||
(nafDigit a k = 0 ∨ nafDigit a k % 2 = 1) ∧
|
||||
-16 < nafDigit a k ∧ nafDigit a k < 16
|
||||
|
||||
/-- Table contract: the 8 entries are proven caches of the odd multiples
|
||||
of A (naf_table_spec's post, bundled). -/
|
||||
def NafTableOf
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(A : EdPoint) : Prop :=
|
||||
∃ e0 e1 e2 e3 e4 e5 e6 e7,
|
||||
tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
|
||||
NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
|
||||
NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
|
||||
NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7
|
||||
|
||||
/-! ### The loop induction -/
|
||||
|
||||
/-- **The Straus loop body, by induction on the counter.** From any valid
|
||||
on-curve accumulator r at counter j ≤ 256, the loop returns a valid
|
||||
on-curve point denoting `dsmFold` of the remaining digits applied to
|
||||
(projX r, projY r). One symbolic walk per induction step. -/
|
||||
theorem dsm_loop_loop_spec
|
||||
(a_naf b_naf : Std.Array Std.I8 256#usize)
|
||||
(ta tb : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(A B : EdPoint)
|
||||
(hta : NafTableOf ta A) (htb : NafTableOf tb B)
|
||||
(hda : NafDigits a_naf) (hdb : NafDigits b_naf)
|
||||
(n : ℕ) :
|
||||
∀ (j : Usize) (r : ProjPoint), j.val = n → n ≤ 256 →
|
||||
ProjValid r → OnCurve (projX r) (projY r) →
|
||||
backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
|
||||
a_naf b_naf ta tb r j ⦃ res =>
|
||||
ProjValid res ∧ OnCurve (projX res) (projY res) ∧
|
||||
(projX res, projY res) = dsmFold (nafDigit a_naf) (nafDigit b_naf)
|
||||
(edPt A) (edPt B) (projX r, projY r) n ⦄ := by
|
||||
obtain ⟨eA0, eA1, eA2, eA3, eA4, eA5, eA6, eA7, hlA,
|
||||
hA0, hA1, hA2, hA3, hA4, hA5, hA6, hA7⟩ := hta
|
||||
obtain ⟨eB0, eB1, eB2, eB3, eB4, eB5, eB6, eB7, hlB,
|
||||
hB0, hB1, hB2, hB3, hB4, hB5, hB6, hB7⟩ := htb
|
||||
induction n with
|
||||
| zero =>
|
||||
intro j r hj hle hv hc
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
|
||||
apply loop_step
|
||||
simp only [backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop.body]
|
||||
have hj0 : ¬ (j > 0#usize) := by clear * - hj; scalar_tac
|
||||
rw [if_neg hj0]
|
||||
try simp only [spec_ok]
|
||||
exact ⟨hv, hc, rfl⟩
|
||||
| succ n ih =>
|
||||
intro j r hj hle hv hc
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop
|
||||
apply loop_step
|
||||
simp only [backend.serial.scalar_mul.vartime_double_base.dsm_loop_loop.body]
|
||||
have hjpos : j > 0#usize := by clear * - hj; scalar_tac
|
||||
rw [if_pos hjpos]
|
||||
-- idx ← j − 1
|
||||
step as ⟨idx, hidx⟩
|
||||
have hidxv : idx.val = n := by clear * - hidx hj; scalar_tac
|
||||
-- t0 ← r.double() (the projective doubling law)
|
||||
step with (proj_double_law r hv hc) as
|
||||
⟨t0, t0bX, t0bY, t0bZ, t0bT, t0z, t0t, t0x, t0y⟩
|
||||
have hct0 : OnCurve (complX t0) (complY t0) := by
|
||||
rw [t0x, t0y]
|
||||
exact edAdd_closure hc hc
|
||||
-- da ← a_naf[idx]
|
||||
step as ⟨da, hdav⟩
|
||||
have hban : n < (↑a_naf : List Std.I8).length := by
|
||||
clear * - hle; scalar_tac
|
||||
have hdaq : da.val = nafDigit a_naf n := by
|
||||
rw [hdav]
|
||||
simp only [nafDigit, hidxv, getElem!_pos (↑a_naf : List Std.I8) n hban]
|
||||
obtain ⟨hdA1, hdA2, hdA3⟩ := hda n (by omega)
|
||||
-- t1 ← dsm_step_p t0 ta da
|
||||
step with (dsm_step_p_law t0 ta da A eA0 eA1 eA2 eA3 eA4 eA5 eA6 eA7 hlA
|
||||
hA0 hA1 hA2 hA3 hA4 hA5 hA6 hA7 t0bX t0bY t0bZ t0bT t0z t0t hct0
|
||||
(by clear * - hdA1 hdaq; omega)
|
||||
(by clear * - hdA2 hdaq; omega) (by clear * - hdA3 hdaq; omega)) as
|
||||
⟨t1, t1bX, t1bY, t1bZ, t1bT, t1z, t1t, hct1, ht1⟩
|
||||
-- db ← b_naf[idx]
|
||||
step as ⟨db, hdbv⟩
|
||||
have hbbn : n < (↑b_naf : List Std.I8).length := by
|
||||
clear * - hle; scalar_tac
|
||||
have hdbq : db.val = nafDigit b_naf n := by
|
||||
rw [hdbv]
|
||||
simp only [nafDigit, hidxv, getElem!_pos (↑b_naf : List Std.I8) n hbbn]
|
||||
obtain ⟨hdB1, hdB2, hdB3⟩ := hdb n (by omega)
|
||||
-- t2 ← dsm_step_b t1 tb db
|
||||
step with (dsm_step_b_law t1 tb db B eB0 eB1 eB2 eB3 eB4 eB5 eB6 eB7 hlB
|
||||
hB0 hB1 hB2 hB3 hB4 hB5 hB6 hB7 t1bX t1bY t1bZ t1bT t1z t1t hct1
|
||||
(by clear * - hdB1 hdbq; omega) (by clear * - hdB2 hdbq; omega)
|
||||
(by clear * - hdB3 hdbq; omega)) as
|
||||
⟨t2, t2bX, t2bY, t2bZ, t2bT, t2z, t2t, hct2, ht2⟩
|
||||
-- r1 ← t2.as_projective()
|
||||
step with (compl_as_projective_law t2 t2bX t2bY t2bZ t2bT t2z t2t) as
|
||||
⟨r1, hr1v, hr1x, hr1y⟩
|
||||
have hcr1 : OnCurve (projX r1) (projY r1) := by
|
||||
rw [hr1x, hr1y]; exact hct2
|
||||
-- the digit chain: (projPt r1) = edDigit_B (edDigit_A (edAdd P P))
|
||||
have hchain : (projX r1, projY r1)
|
||||
= edDigit (edPt B) (nafDigit b_naf n)
|
||||
(edDigit (edPt A) (nafDigit a_naf n)
|
||||
(edAdd (projX r, projY r) (projX r, projY r))) := by
|
||||
have e1 : (complX t0, complY t0)
|
||||
= edAdd (projX r, projY r) (projX r, projY r) := by
|
||||
rw [Prod.ext_iff]; exact ⟨t0x, t0y⟩
|
||||
have e2 : (projX r1, projY r1) = (complX t2, complY t2) := by
|
||||
rw [Prod.ext_iff]; exact ⟨hr1x, hr1y⟩
|
||||
rw [e2, ht2, hdbq, ht1, hdaq, e1]
|
||||
try simp only [spec_ok]
|
||||
-- close with the induction hypothesis at counter idx (= n)
|
||||
apply spec_mono (ih idx r1 hidxv (by omega) hr1v hcr1)
|
||||
intro res ⟨hv', hc', heq⟩
|
||||
refine ⟨hv', hc', ?_⟩
|
||||
rw [heq, hchain, dsmFold_succ]
|
||||
|
||||
/-! ### The top-index constant and the public loop wrapper -/
|
||||
|
||||
/-- `dsm_top_index` is the constant 255 (leading zero digits are identity
|
||||
doublings — the source patch starts every walk at bit 255). -/
|
||||
theorem dsm_top_index_spec (a b : Std.Array Std.I8 256#usize) :
|
||||
backend.serial.scalar_mul.vartime_double_base.dsm_top_index a b
|
||||
⦃ r => r = 255#usize ⦄ := by
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_top_index
|
||||
simp [spec_ok]
|
||||
|
||||
/-- **The full Straus loop**: from the identity, process all 256 digit
|
||||
positions — the result denotes `dsmFold … edId 256`. -/
|
||||
theorem dsm_loop_spec (i : Usize) (hi : i.val = 255)
|
||||
(a_naf b_naf : Std.Array Std.I8 256#usize)
|
||||
(ta tb : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(A B : EdPoint)
|
||||
(hta : NafTableOf ta A) (htb : NafTableOf tb B)
|
||||
(hda : NafDigits a_naf) (hdb : NafDigits b_naf) :
|
||||
backend.serial.scalar_mul.vartime_double_base.dsm_loop
|
||||
i a_naf b_naf ta tb ⦃ res =>
|
||||
ProjValid res ∧ OnCurve (projX res) (projY res) ∧
|
||||
(projX res, projY res) = dsmFold (nafDigit a_naf) (nafDigit b_naf)
|
||||
(edPt A) (edPt B) edId 256 ⦄ := by
|
||||
obtain ⟨P0, hP0ok, hP0v, hP0x, hP0y⟩ := run_projective_identity
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_loop
|
||||
rw [hP0ok]
|
||||
simp only [bind_tc_ok]
|
||||
have hcP0 : OnCurve (projX P0) (projY P0) := by
|
||||
rw [hP0x, hP0y]; exact onCurve_id
|
||||
-- j ← i + 1 (= 256)
|
||||
step as ⟨j, hj⟩
|
||||
have hjv : j.val = 256 := by clear * - hj hi; scalar_tac
|
||||
apply spec_mono (dsm_loop_loop_spec a_naf b_naf ta tb A B hta htb hda hdb
|
||||
256 j P0 hjv (by omega) hP0v hcP0)
|
||||
intro res ⟨hv, hc, heq⟩
|
||||
refine ⟨hv, hc, ?_⟩
|
||||
rw [heq, hP0x, hP0y]
|
||||
rfl
|
||||
|
||||
end CurveFieldProofs
|
||||
315
verification/Proofs/DsmStepSpec.lean
Normal file
315
verification/Proofs/DsmStepSpec.lean
Normal file
|
|
@ -0,0 +1,315 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/DsmStepSpec.lean — double-scalar-mul campaign, brick 2:
|
||||
the per-digit step of the Straus/NAF loop.
|
||||
|
||||
vartime_double_base's loop body is
|
||||
t = r.double(); t = dsm_step_p(t, table_a, a_naf[i]);
|
||||
t = dsm_step_b(t, table_b, b_naf[i]); r = t.as_projective();
|
||||
This file proves the three non-loop ingredients as LAWS over the abstract
|
||||
Edwards addition (computational layering, no associativity):
|
||||
|
||||
· `proj_double_law` — ProjectivePoint::double denotes edAdd P P
|
||||
(lift of the coordinate-level proj_double_spec,
|
||||
same Z²-scaled linear_combination discipline as
|
||||
edwards_double_law's Z⁴ one).
|
||||
· `compl_as_projective_law` — CompletedPoint::as_projective preserves the
|
||||
denoted affine point ((X:Z),(Y:T)) ↦ (XT:YZ:ZT).
|
||||
· `naf_select_entry` — select on a table with proven entries returns
|
||||
THE entry for the digit: NafEntryOf r A ((x−1)/2).
|
||||
· `dsm_step_p_law`/`dsm_step_b_law` — the three-way digit step denotes
|
||||
`edDigit`: add the (+d)-th odd multiple, add the
|
||||
negation of the (−d)-th, or pass through.
|
||||
|
||||
The digit hypotheses (odd-or-zero, |d| < 16) are exactly what the NAF
|
||||
digit spec will provide; they are taken as hypotheses here (layering).
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.DsmTableSpec
|
||||
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
|
||||
|
||||
/-! ### Projective coordinate plumbing -/
|
||||
|
||||
/-- ⟪X⟫ = x·⟪Z⟫ for a projective point with ⟪Z⟫ ≠ 0 (x := projX). -/
|
||||
theorem proj_X_eq (p : ProjPoint) (hZ0 : ⟪p.Z⟫ ≠ 0) : ⟪p.X⟫ = projX p * ⟪p.Z⟫ := by
|
||||
unfold projX
|
||||
field_simp
|
||||
|
||||
/-- ⟪Y⟫ = y·⟪Z⟫ for a projective point with ⟪Z⟫ ≠ 0 (y := projY). -/
|
||||
theorem proj_Y_eq (p : ProjPoint) (hZ0 : ⟪p.Z⟫ ≠ 0) : ⟪p.Y⟫ = projY p * ⟪p.Z⟫ := by
|
||||
unfold projY
|
||||
field_simp
|
||||
|
||||
/-- **ProjectivePoint::double denotes the Edwards doubling law.**
|
||||
|
||||
MATH: for a valid projective point P on the curve, `double` returns a
|
||||
completed point t with 2⁵⁴-bounded limbs, unit denominators, and
|
||||
(complX t, complY t) = edAdd (projX P, projY P) (projX P, projY P).
|
||||
Same derivation as `edwards_double_law` with Z² in place of Z⁴:
|
||||
the curve equation turns Y²−X² into Z²·(1+D) and 2Z²−(Y²−X²) into
|
||||
Z²·(1−D), both nonzero by completeness at the diagonal. -/
|
||||
theorem proj_double_law (p : ProjPoint) (hp : ProjValid p)
|
||||
(hcp : OnCurve (projX p) (projY p)) :
|
||||
backend.serial.curve_models.ProjectivePoint.double p ⦃ t =>
|
||||
Bnd t.X (2^54) ∧ Bnd t.Y (2^54) ∧ Bnd t.Z (2^54) ∧ Bnd t.T (2^54) ∧
|
||||
⟪t.Z⟫ ≠ 0 ∧ ⟪t.T⟫ ≠ 0 ∧
|
||||
complX t = (edAdd (projX p, projY p) (projX p, projY p)).1 ∧
|
||||
complY t = (edAdd (projX p, projY p) (projX p, projY p)).2 ⦄ := by
|
||||
apply spec_mono (proj_double_spec p hp)
|
||||
rintro t ⟨hbX, hbY, hbZ, hbT, hvX, hvY, hvZ, hvT⟩
|
||||
obtain ⟨-, -, -, hZ0⟩ := hp
|
||||
obtain ⟨hp1, hm1⟩ := completeness hcp hcp
|
||||
have hX := proj_X_eq p hZ0
|
||||
have hY := proj_Y_eq p hZ0
|
||||
have hZ2 : ⟪p.Z⟫^2 ≠ 0 := pow_ne_zero 2 hZ0
|
||||
-- the curve equation in doubling-friendly form
|
||||
have hcur : projY p ^ 2 - projX p ^ 2
|
||||
= 1 + edD * projX p * projX p * projY p * projY p := by
|
||||
have h := hcp
|
||||
unfold OnCurve at h
|
||||
linear_combination h
|
||||
-- the four coordinates, Z²-scaled
|
||||
have eX : ⟪t.X⟫ = ⟪p.Z⟫^2 * (projX p * projY p + projX p * projY p) := by
|
||||
rw [hvX, hX, hY]; ring
|
||||
have eY : ⟪t.Y⟫ = ⟪p.Z⟫^2 * (projY p * projY p + projX p * projX p) := by
|
||||
rw [hvY, hX, hY]; ring
|
||||
have eZ : ⟪t.Z⟫ = ⟪p.Z⟫^2 *
|
||||
(1 + edD * projX p * projX p * projY p * projY p) := by
|
||||
rw [hvZ, hX, hY]
|
||||
linear_combination ⟪p.Z⟫^2 * hcur
|
||||
have eT : ⟪t.T⟫ = ⟪p.Z⟫^2 *
|
||||
(1 - edD * projX p * projX p * projY p * projY p) := by
|
||||
rw [hvT, hX, hY]
|
||||
linear_combination (-(⟪p.Z⟫^2)) * hcur
|
||||
have hZne : ⟪t.Z⟫ ≠ 0 := by rw [eZ]; exact mul_ne_zero hZ2 hp1
|
||||
have hTne : ⟪t.T⟫ ≠ 0 := by rw [eT]; exact mul_ne_zero hZ2 hm1
|
||||
refine ⟨hbX.mono (by norm_num), hbY.mono (by norm_num),
|
||||
hbZ.mono (by norm_num), hbT.mono (by norm_num), hZne, hTne, ?_, ?_⟩
|
||||
· show ⟪t.X⟫ / ⟪t.Z⟫ = (projX p * projY p + projX p * projY p) /
|
||||
(1 + edD * projX p * projX p * projY p * projY p)
|
||||
rw [fp_div_eq_div_iff hZne hp1, eX, eZ]
|
||||
ring
|
||||
· show ⟪t.Y⟫ / ⟪t.T⟫ = (projY p * projY p + projX p * projX p) /
|
||||
(1 - edD * projX p * projX p * projY p * projY p)
|
||||
rw [fp_div_eq_div_iff hTne hm1, eY, eT]
|
||||
ring
|
||||
|
||||
/-- **CompletedPoint::as_projective preserves the denoted point.**
|
||||
|
||||
MATH: ((X:Z),(Y:T)) ↦ (XT : YZ : ZT) — with ⟪Z⟫,⟪T⟫ ≠ 0 the new
|
||||
denominator ZT is a unit and XT/ZT = X/Z, YZ/ZT = Y/T. -/
|
||||
theorem compl_as_projective_law (p : ComplPoint)
|
||||
(hbX : Bnd p.X (2^54)) (hbY : Bnd p.Y (2^54))
|
||||
(hbZ : Bnd p.Z (2^54)) (hbT : Bnd p.T (2^54))
|
||||
(hZ0 : ⟪p.Z⟫ ≠ 0) (hT0 : ⟪p.T⟫ ≠ 0) :
|
||||
backend.serial.curve_models.CompletedPoint.as_projective p ⦃ r =>
|
||||
ProjValid r ∧ projX r = complX p ∧ projY r = complY p ⦄ := by
|
||||
unfold backend.serial.curve_models.CompletedPoint.as_projective
|
||||
step with (mul_spec' _ _ hbX hbT) as ⟨fe, feb, fev⟩
|
||||
step with (mul_spec' _ _ hbY hbZ) as ⟨fe1, fe1b, fe1v⟩
|
||||
step with (mul_spec' _ _ hbZ hbT) as ⟨fe2, fe2b, fe2v⟩
|
||||
try simp only [spec_ok]
|
||||
refine ⟨⟨feb.mono (by norm_num), fe1b.mono (by norm_num),
|
||||
fe2b.mono (by norm_num), ?_⟩, ?_, ?_⟩
|
||||
· show ⟪fe2⟫ ≠ 0
|
||||
rw [fe2v]; exact mul_ne_zero hZ0 hT0
|
||||
· show ⟪fe⟫ / ⟪fe2⟫ = ⟪p.X⟫ / ⟪p.Z⟫
|
||||
rw [fev, fe2v, mul_div_mul_right _ _ hT0]
|
||||
· show ⟪fe1⟫ / ⟪fe2⟫ = ⟪p.Y⟫ / ⟪p.T⟫
|
||||
rw [fe1v, fe2v, mul_comm ⟪p.Z⟫ ⟪p.T⟫, mul_div_mul_right _ _ hZ0]
|
||||
|
||||
/-! ### Digit-indexed table lookup -/
|
||||
|
||||
/-- select on a table with proven entries returns THE entry for the digit:
|
||||
for odd x < 16, the result is a valid cache of the ((x−1)/2)-th odd
|
||||
multiple of A. -/
|
||||
theorem naf_select_entry
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(x : Usize) (A : EdPoint)
|
||||
(e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
|
||||
(h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
|
||||
(h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
|
||||
(h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
|
||||
(hodd : x.val % 2 = 1) (hlt : x.val < 16) :
|
||||
window.NafLookupTable5.select
|
||||
backend.serial.curve_models.ProjectiveNielsPoint.Insts.CoreMarkerCopy tbl x
|
||||
⦃ r => NafEntryOf r A ((x.val - 1) / 2) ⦄ := by
|
||||
apply spec_mono (naf_select_spec tbl x e0 e1 e2 e3 e4 e5 e6 e7 hl hodd hlt)
|
||||
rintro r ⟨i1, i3, i5, i7, i9, i11, i13, i15⟩
|
||||
have hx : x.val = 1 ∨ x.val = 3 ∨ x.val = 5 ∨ x.val = 7 ∨ x.val = 9 ∨
|
||||
x.val = 11 ∨ x.val = 13 ∨ x.val = 15 := by omega
|
||||
rcases hx with hx | hx | hx | hx | hx | hx | hx | hx
|
||||
· rw [i1 hx, hx]; exact h0
|
||||
· rw [i3 hx, hx]; exact h1
|
||||
· rw [i5 hx, hx]; exact h2
|
||||
· rw [i7 hx, hx]; exact h3
|
||||
· rw [i9 hx, hx]; exact h4
|
||||
· rw [i11 hx, hx]; exact h5
|
||||
· rw [i13 hx, hx]; exact h6
|
||||
· rw [i15 hx, hx]; exact h7
|
||||
|
||||
/-! ### The abstract digit step -/
|
||||
|
||||
/-- One NAF digit's action on the accumulator: add the d-th odd multiple of
|
||||
the base (d > 0), add its negation (d < 0), or pass through (d = 0) —
|
||||
over the abstract `edAdd`, no associativity. -/
|
||||
noncomputable def edDigit (aPt : Fp × Fp) (d : ℤ) (P : Fp × Fp) : Fp × Fp :=
|
||||
if 0 < d then edAdd P (edOdd ((d.toNat - 1) / 2) aPt)
|
||||
else if d < 0 then edAdd P (edNeg (edOdd (((-d).toNat - 1) / 2) aPt))
|
||||
else P
|
||||
|
||||
/-- **The digit step denotes `edDigit`.**
|
||||
|
||||
Given a bounded, unit-denominator completed accumulator t denoting an
|
||||
on-curve point, a table whose entries are proven caches of odd multiples
|
||||
of A, and a NAF digit (odd or zero, |d| < 16): `dsm_step_p` returns a
|
||||
completed point with the same validity shape denoting
|
||||
`edDigit (edPt A) d.val (complX t, complY t)`. The `select` masserts
|
||||
(panic freedom) are discharged, not assumed. -/
|
||||
theorem dsm_step_p_law (t : ComplPoint)
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(d : Std.I8) (A : EdPoint)
|
||||
(e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
|
||||
(h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
|
||||
(h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
|
||||
(h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
|
||||
(hbX : Bnd t.X (2^54)) (hbY : Bnd t.Y (2^54))
|
||||
(hbZ : Bnd t.Z (2^54)) (hbT : Bnd t.T (2^54))
|
||||
(hZ0 : ⟪t.Z⟫ ≠ 0) (hT0 : ⟪t.T⟫ ≠ 0)
|
||||
(hct : OnCurve (complX t) (complY t))
|
||||
(hd : d.val = 0 ∨ d.val % 2 = 1) (hdlo : -16 < d.val) (hdhi : d.val < 16) :
|
||||
backend.serial.scalar_mul.vartime_double_base.dsm_step_p t tbl d ⦃ r =>
|
||||
Bnd r.X (2^54) ∧ Bnd r.Y (2^54) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^54) ∧
|
||||
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
|
||||
OnCurve (complX r) (complY r) ∧
|
||||
(complX r, complY r) = edDigit (edPt A) d.val (complX t, complY t) ⦄ := by
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_step_p
|
||||
split
|
||||
· -- d > 0: add the d-th odd multiple
|
||||
rename_i hdpos
|
||||
have hdposv : (0:ℤ) < d.val := by clear * - hdpos; scalar_tac
|
||||
-- ep ← t.as_extended
|
||||
step with (compl_as_extended_law t hbX hbY hbZ hbT hZ0 hT0) as ⟨ep, hepv, hepx, hepy⟩
|
||||
have hepc : OnCurveExt ep := by
|
||||
show OnCurve (edX ep) (edY ep)
|
||||
rw [hepx, hepy]; exact hct
|
||||
have hept : edPt ep = (complX t, complY t) := by
|
||||
calc edPt ep = (edX ep, edY ep) := rfl
|
||||
_ = (complX t, complY t) := by rw [hepx, hepy]
|
||||
-- i ← d as usize (in-bounds: 0 < d < 16)
|
||||
step with (IScalar.hcast_inBounds_spec .Usize d
|
||||
(by clear * - hdposv hdhi; scalar_tac)) as ⟨i, hi⟩
|
||||
have hiv : i.val = d.val.toNat := by clear * - hi hdposv; omega
|
||||
have hiodd : i.val % 2 = 1 := by clear * - hiv hd hdposv; omega
|
||||
have hilt : i.val < 16 := by clear * - hiv hdhi hdposv; omega
|
||||
-- pnp ← select tbl i (the ((i−1)/2)-th odd multiple's cache)
|
||||
step with (naf_select_entry tbl i A e0 e1 e2 e3 e4 e5 e6 e7 hl
|
||||
h0 h1 h2 h3 h4 h5 h6 h7 hiodd hilt) as ⟨pnp, hpnp⟩
|
||||
obtain ⟨hpv, Q, hpn, hQv, hQc, hQpt⟩ := hpnp
|
||||
-- r ← ep + pnp (the mixed-add kernel law)
|
||||
apply spec_mono (add_projniels_law ep pnp hpn hepv hQv hepc hQc hpv)
|
||||
rintro r ⟨rbX, rbY, rbZ, rbT, rz, rt, rx, ry⟩
|
||||
have hcr : OnCurve (complX r) (complY r) := by
|
||||
rw [rx, ry]
|
||||
exact edAdd_closure (show OnCurve (edX ep) (edY ep) from hepc)
|
||||
(show OnCurve (edX Q) (edY Q) from hQc)
|
||||
refine ⟨rbX.mono (by norm_num), rbY.mono (by norm_num), rbZ,
|
||||
rbT.mono (by norm_num), rz, rt, hcr, ?_⟩
|
||||
have hk : (i.val - 1) / 2 = (d.val.toNat - 1) / 2 := by
|
||||
clear * - hiv; omega
|
||||
simp only [edDigit, if_pos hdposv]
|
||||
calc (complX r, complY r)
|
||||
= ((edAdd (edPt ep) (edPt Q)).1, (edAdd (edPt ep) (edPt Q)).2) := by
|
||||
rw [rx, ry]
|
||||
_ = edAdd (edPt ep) (edPt Q) := rfl
|
||||
_ = edAdd (complX t, complY t) (edOdd ((d.val.toNat - 1) / 2) (edPt A)) := by
|
||||
rw [hept, hQpt, hk]
|
||||
· -- d < 0 or d = 0
|
||||
split
|
||||
· -- d < 0: add the negation of the (−d)-th odd multiple
|
||||
rename_i hdneg
|
||||
have hdnegv : d.val < 0 := by clear * - hdneg; scalar_tac
|
||||
-- ep ← t.as_extended
|
||||
step with (compl_as_extended_law t hbX hbY hbZ hbT hZ0 hT0) as ⟨ep, hepv, hepx, hepy⟩
|
||||
have hepc : OnCurveExt ep := by
|
||||
show OnCurve (edX ep) (edY ep)
|
||||
rw [hepx, hepy]; exact hct
|
||||
have hept : edPt ep = (complX t, complY t) := by
|
||||
calc edPt ep = (edX ep, edY ep) := rfl
|
||||
_ = (complX t, complY t) := by rw [hepx, hepy]
|
||||
-- i ← −d; i1 ← i as usize
|
||||
step as ⟨i, hi⟩
|
||||
have hiv : i.val = -d.val := by clear * - hi hdnegv hdlo; scalar_tac
|
||||
step with (IScalar.hcast_inBounds_spec .Usize i
|
||||
(by clear * - hiv hdnegv hdlo; scalar_tac)) as ⟨i1, hi1⟩
|
||||
have hi1v : i1.val = (-d.val).toNat := by clear * - hi1 hiv hdnegv; omega
|
||||
have hiodd : i1.val % 2 = 1 := by clear * - hi1v hd hdnegv; omega
|
||||
have hilt : i1.val < 16 := by clear * - hi1v hdlo hdnegv; omega
|
||||
-- pnp ← select tbl i1
|
||||
step with (naf_select_entry tbl i1 A e0 e1 e2 e3 e4 e5 e6 e7 hl
|
||||
h0 h1 h2 h3 h4 h5 h6 h7 hiodd hilt) as ⟨pnp, hpnp⟩
|
||||
obtain ⟨hpv, Q, hpn, hQv, hQc, hQpt⟩ := hpnp
|
||||
-- r ← ep − pnp (the mixed-sub kernel law)
|
||||
apply spec_mono (sub_projniels_law ep pnp hpn hepv hQv hepc hQc hpv)
|
||||
rintro r ⟨rbX, rbY, rbZ, rbT, rz, rt, rx, ry⟩
|
||||
have hcr : OnCurve (complX r) (complY r) := by
|
||||
rw [rx, ry]
|
||||
exact edAdd_closure (show OnCurve (edX ep) (edY ep) from hepc)
|
||||
(onCurve_neg (show OnCurve (edX Q) (edY Q) from hQc))
|
||||
refine ⟨rbX.mono (by norm_num), rbY.mono (by norm_num),
|
||||
rbZ.mono (by norm_num), rbT, rz, rt, hcr, ?_⟩
|
||||
have hk : (i1.val - 1) / 2 = ((-d.val).toNat - 1) / 2 := by
|
||||
clear * - hi1v; omega
|
||||
have hnpos : ¬ ((0:ℤ) < d.val) := by clear * - hdnegv; omega
|
||||
simp only [edDigit, if_neg hnpos, if_pos hdnegv]
|
||||
calc (complX r, complY r)
|
||||
= ((edAdd (edPt ep) (edNeg (edPt Q))).1,
|
||||
(edAdd (edPt ep) (edNeg (edPt Q))).2) := by
|
||||
rw [rx, ry]
|
||||
_ = edAdd (edPt ep) (edNeg (edPt Q)) := rfl
|
||||
_ = edAdd (complX t, complY t)
|
||||
(edNeg (edOdd (((-d.val).toNat - 1) / 2) (edPt A))) := by
|
||||
rw [hept, hQpt, hk]
|
||||
· -- d = 0: pass through
|
||||
rename_i hnpos hnneg
|
||||
have h0v : d.val = 0 := by clear * - hnpos hnneg; scalar_tac
|
||||
try simp only [spec_ok]
|
||||
have hzero : ¬ ((0:ℤ) < d.val) ∧ ¬ (d.val < 0) := by
|
||||
clear * - h0v; omega
|
||||
refine ⟨hbX, hbY, hbZ, hbT, hZ0, hT0, hct, ?_⟩
|
||||
simp only [edDigit, if_neg hzero.1, if_neg hzero.2]
|
||||
|
||||
/-- `dsm_step_b` delegates to `dsm_step_p` (both tables are runtime
|
||||
`NafLookupTable5<ProjectiveNielsPoint>` in this extraction). -/
|
||||
theorem dsm_step_b_law (t : ComplPoint)
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(d : Std.I8) (A : EdPoint)
|
||||
(e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
|
||||
(h0 : NafEntryOf e0 A 0) (h1 : NafEntryOf e1 A 1) (h2 : NafEntryOf e2 A 2)
|
||||
(h3 : NafEntryOf e3 A 3) (h4 : NafEntryOf e4 A 4) (h5 : NafEntryOf e5 A 5)
|
||||
(h6 : NafEntryOf e6 A 6) (h7 : NafEntryOf e7 A 7)
|
||||
(hbX : Bnd t.X (2^54)) (hbY : Bnd t.Y (2^54))
|
||||
(hbZ : Bnd t.Z (2^54)) (hbT : Bnd t.T (2^54))
|
||||
(hZ0 : ⟪t.Z⟫ ≠ 0) (hT0 : ⟪t.T⟫ ≠ 0)
|
||||
(hct : OnCurve (complX t) (complY t))
|
||||
(hd : d.val = 0 ∨ d.val % 2 = 1) (hdlo : -16 < d.val) (hdhi : d.val < 16) :
|
||||
backend.serial.scalar_mul.vartime_double_base.dsm_step_b t tbl d ⦃ r =>
|
||||
Bnd r.X (2^54) ∧ Bnd r.Y (2^54) ∧ Bnd r.Z (2^54) ∧ Bnd r.T (2^54) ∧
|
||||
⟪r.Z⟫ ≠ 0 ∧ ⟪r.T⟫ ≠ 0 ∧
|
||||
OnCurve (complX r) (complY r) ∧
|
||||
(complX r, complY r) = edDigit (edPt A) d.val (complX t, complY t) ⦄ := by
|
||||
unfold backend.serial.scalar_mul.vartime_double_base.dsm_step_b
|
||||
exact dsm_step_p_law t tbl d A e0 e1 e2 e3 e4 e5 e6 e7 hl
|
||||
h0 h1 h2 h3 h4 h5 h6 h7 hbX hbY hbZ hbT hZ0 hT0 hct hd hdlo hdhi
|
||||
|
||||
end CurveFieldProofs
|
||||
485
verification/Proofs/DsmTableSpec.lean
Normal file
485
verification/Proofs/DsmTableSpec.lean
Normal file
|
|
@ -0,0 +1,485 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/DsmTableSpec.lean — double-scalar-mul campaign, brick 1:
|
||||
the NAF lookup-table construction `NafLookupTable5::from(&A)`.
|
||||
|
||||
window.rs builds the odd-multiples table [A, 3A, 5A, 7A, 9A, 11A, 13A, 15A]
|
||||
(as ProjectiveNielsPoint caches):
|
||||
Ai[0] = A.as_projective_niels(); A2 = A.double();
|
||||
for i in 0..7 { Ai[i+1] = (A2 + Ai[i]).as_extended().as_projective_niels() }
|
||||
|
||||
SPEC (relational, computational layering — no associativity assumed):
|
||||
entry k is a VALID niels cache of a valid on-curve point Q_k with
|
||||
edPt Q_k = edOdd k (edPt A)
|
||||
where `edOdd` is the abstract double-and-add recursion
|
||||
edOdd 0 p = p, edOdd (k+1) p = edAdd (edAdd p p) (edOdd k p)
|
||||
— i.e. exactly the (2k+1)-fold sum the code computes, expressed over the
|
||||
proven abstract Edwards addition `edAdd` (EdCurve). Composes the proven
|
||||
group-layer laws: edwards_as_projective_niels_spec, edwards_double_law,
|
||||
add_projniels_law, compl_as_extended_law (EdMain / EdConvert).
|
||||
|
||||
Loop-peel machinery (loop_step / range_next_*_spec) is the field layer's
|
||||
(AddSpec.lean, same namespace) — this file imports only the CurveField
|
||||
extraction tree.
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.EdMain
|
||||
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
|
||||
|
||||
/- Loop-peel machinery (loop_step / range_next_*_spec) comes from the
|
||||
field layer's AddSpec.lean — already in this namespace via Proofs.EdMain. -/
|
||||
|
||||
/-! ### The abstract odd-multiple recursion -/
|
||||
|
||||
/-- `edOdd k p` is the double-and-add recursion the table loop computes:
|
||||
p, then 2p+p, 2p+(3p), … — abstractly, the (2k+1)-th odd multiple,
|
||||
expressed over `edAdd` WITHOUT assuming associativity (computational
|
||||
layering; the group-semantics reading is phase 2 of the campaign). -/
|
||||
noncomputable def edOdd : ℕ → Fp × Fp → Fp × Fp
|
||||
| 0, p => p
|
||||
| k + 1, p => edAdd (edAdd p p) (edOdd k p)
|
||||
|
||||
@[simp] theorem edOdd_zero (p : Fp × Fp) : edOdd 0 p = p := rfl
|
||||
|
||||
theorem edOdd_succ (k : ℕ) (p : Fp × Fp) :
|
||||
edOdd (k + 1) p = edAdd (edAdd p p) (edOdd k p) := rfl
|
||||
|
||||
/-- Entry contract of the NAF table: a valid niels cache of a valid,
|
||||
on-curve point denoting the k-th odd multiple of A. -/
|
||||
def NafEntryOf (e : backend.serial.curve_models.ProjectiveNielsPoint) (A : EdPoint) (k : ℕ) : Prop :=
|
||||
ProjNielsValid e ∧ ∃ Q : EdPoint, IsNielsOf e Q ∧ ExtValid Q ∧
|
||||
OnCurveExt Q ∧ edPt Q = edOdd k (edPt A)
|
||||
|
||||
/-- The entry list of a `NafLookupTable5` (the type is a transparent
|
||||
synonym for `Array ProjectiveNielsPoint 8`). -/
|
||||
def tblEntries
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint) : List backend.serial.curve_models.ProjectiveNielsPoint :=
|
||||
Subtype.val (tbl : Std.Array backend.serial.curve_models.ProjectiveNielsPoint 8#usize)
|
||||
|
||||
/-! ### The table-construction loop: 7 concrete peels -/
|
||||
|
||||
/-- The `from` loop: starting from `[cache(A)]*8`, after 7 iterations entry k
|
||||
holds a valid cache of the k-th odd multiple, for every k ≤ 7. -/
|
||||
theorem naf_table_loop_spec (A A2 : EdPoint)
|
||||
(Ai : Std.Array backend.serial.curve_models.ProjectiveNielsPoint 8#usize) (n0 : backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(hl0 : (↑Ai : List backend.serial.curve_models.ProjectiveNielsPoint) = [n0, n0, n0, n0, n0, n0, n0, n0])
|
||||
(hn0v : ProjNielsValid n0) (hn0n : IsNielsOf n0 A)
|
||||
(hAv : ExtValid A) (hAc : OnCurveExt A)
|
||||
(hA2v : ExtValid A2) (hA2c : OnCurveExt A2)
|
||||
(hA2pt : edPt A2 = edAdd (edPt A) (edPt A)) :
|
||||
window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop
|
||||
{ start := 0#usize, «end» := 7#usize } Ai A2
|
||||
⦃ arr => ∃ e0 e1 e2 e3 e4 e5 e6 e7,
|
||||
(↑arr : List backend.serial.curve_models.ProjectiveNielsPoint) = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
|
||||
NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
|
||||
NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
|
||||
NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7 ⦄ := by
|
||||
have hq0pt : edPt A = edOdd 0 (edPt A) := rfl
|
||||
unfold window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop
|
||||
-- ── iteration 0: read entry 0 (cache of q0), write entry 1 = cache of 2A + q0
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with range_next_lt_spec as ⟨o0, iter0, ho0, hs0, he0⟩
|
||||
simp only [ho0]
|
||||
have hsv0 : iter0.start.val = 1 := by clear * - hs0; omega
|
||||
have hev0 : iter0.«end».val = 7 := by clear * - he0; scalar_tac
|
||||
-- entry 0 out of the array
|
||||
step as ⟨e0x, he0x⟩
|
||||
simp [hl0] at he0x
|
||||
rw [he0x]
|
||||
-- cp ← A2 + n0 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n0 hn0n hA2v hAv hA2c hAc hn0v) as
|
||||
⟨cp0, cb0X, cb0Y, cb0Z, cb0T, cz0, ct0, cx0, cy0⟩
|
||||
-- q1 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp0 (cb0X.mono (by norm_num))
|
||||
(cb0Y.mono (by norm_num)) cb0Z (cb0T.mono (by norm_num)) cz0 ct0) as
|
||||
⟨q1, hq1v, hq1x, hq1y⟩
|
||||
have hq1c : OnCurveExt q1 := by
|
||||
show OnCurve (edX q1) (edY q1)
|
||||
rw [hq1x, cx0, hq1y, cy0]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX A) (edY A) from hAc)
|
||||
have hq1pt : edPt q1 = edOdd 1 (edPt A) := by
|
||||
have h : edPt q1 = edAdd (edPt A2) (edPt A) := by
|
||||
calc edPt q1 = (edX q1, edY q1) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt A)).1, (edAdd (edPt A2) (edPt A)).2) := by
|
||||
rw [hq1x, cx0, hq1y, cy0]
|
||||
_ = edAdd (edPt A2) (edPt A) := rfl
|
||||
rw [h, hA2pt, hq0pt]
|
||||
rfl
|
||||
-- n1 ← q1.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q1 hq1v) as ⟨n1, hn1v, hn1n⟩
|
||||
-- write it at index 1
|
||||
step as ⟨j0, hj0⟩
|
||||
have hj0v : j0 = 1#usize := by clear * - hj0; scalar_tac
|
||||
rw [hj0v]
|
||||
step as ⟨Ai1, hA1⟩
|
||||
have hl1 : (↑Ai1 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n0, n0, n0, n0, n0, n0] := by
|
||||
simp only [hA1, Array.set_val_eq, hl0]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 1: read entry 1 (cache of q1), write entry 2 = cache of 2A + q1
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter0 (by clear * - hsv0 hev0; scalar_tac)) as ⟨o1, iter1, ho1, hs1, he1⟩
|
||||
simp only [ho1]
|
||||
have hsv1 : iter1.start.val = 2 := by clear * - hs1 hsv0; omega
|
||||
have hev1 : iter1.«end».val = 7 := by clear * - he1 hev0; scalar_tac
|
||||
have hidx1 : iter0.start = 1#usize := by clear * - hsv0; scalar_tac
|
||||
rw [hidx1]
|
||||
-- entry 1 out of the array
|
||||
step as ⟨e1x, he1x⟩
|
||||
simp [hl1] at he1x
|
||||
rw [he1x]
|
||||
-- cp ← A2 + n1 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n1 hn1n hA2v hq1v hA2c hq1c hn1v) as
|
||||
⟨cp1, cb1X, cb1Y, cb1Z, cb1T, cz1, ct1, cx1, cy1⟩
|
||||
-- q2 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp1 (cb1X.mono (by norm_num))
|
||||
(cb1Y.mono (by norm_num)) cb1Z (cb1T.mono (by norm_num)) cz1 ct1) as
|
||||
⟨q2, hq2v, hq2x, hq2y⟩
|
||||
have hq2c : OnCurveExt q2 := by
|
||||
show OnCurve (edX q2) (edY q2)
|
||||
rw [hq2x, cx1, hq2y, cy1]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q1) (edY q1) from hq1c)
|
||||
have hq2pt : edPt q2 = edOdd 2 (edPt A) := by
|
||||
have h : edPt q2 = edAdd (edPt A2) (edPt q1) := by
|
||||
calc edPt q2 = (edX q2, edY q2) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q1)).1, (edAdd (edPt A2) (edPt q1)).2) := by
|
||||
rw [hq2x, cx1, hq2y, cy1]
|
||||
_ = edAdd (edPt A2) (edPt q1) := rfl
|
||||
rw [h, hA2pt, hq1pt]
|
||||
rfl
|
||||
-- n2 ← q2.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q2 hq2v) as ⟨n2, hn2v, hn2n⟩
|
||||
-- write it at index 2
|
||||
step as ⟨j1, hj1⟩
|
||||
have hj1v : j1 = 2#usize := by clear * - hj1; scalar_tac
|
||||
rw [hj1v]
|
||||
step as ⟨Ai2, hA2⟩
|
||||
have hl2 : (↑Ai2 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n0, n0, n0, n0, n0] := by
|
||||
simp only [hA2, Array.set_val_eq, hl1]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 2: read entry 2 (cache of q2), write entry 3 = cache of 2A + q2
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter1 (by clear * - hsv1 hev1; scalar_tac)) as ⟨o2, iter2, ho2, hs2, he2⟩
|
||||
simp only [ho2]
|
||||
have hsv2 : iter2.start.val = 3 := by clear * - hs2 hsv1; omega
|
||||
have hev2 : iter2.«end».val = 7 := by clear * - he2 hev1; scalar_tac
|
||||
have hidx2 : iter1.start = 2#usize := by clear * - hsv1; scalar_tac
|
||||
rw [hidx2]
|
||||
-- entry 2 out of the array
|
||||
step as ⟨e2x, he2x⟩
|
||||
simp [hl2] at he2x
|
||||
rw [he2x]
|
||||
-- cp ← A2 + n2 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n2 hn2n hA2v hq2v hA2c hq2c hn2v) as
|
||||
⟨cp2, cb2X, cb2Y, cb2Z, cb2T, cz2, ct2, cx2, cy2⟩
|
||||
-- q3 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp2 (cb2X.mono (by norm_num))
|
||||
(cb2Y.mono (by norm_num)) cb2Z (cb2T.mono (by norm_num)) cz2 ct2) as
|
||||
⟨q3, hq3v, hq3x, hq3y⟩
|
||||
have hq3c : OnCurveExt q3 := by
|
||||
show OnCurve (edX q3) (edY q3)
|
||||
rw [hq3x, cx2, hq3y, cy2]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q2) (edY q2) from hq2c)
|
||||
have hq3pt : edPt q3 = edOdd 3 (edPt A) := by
|
||||
have h : edPt q3 = edAdd (edPt A2) (edPt q2) := by
|
||||
calc edPt q3 = (edX q3, edY q3) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q2)).1, (edAdd (edPt A2) (edPt q2)).2) := by
|
||||
rw [hq3x, cx2, hq3y, cy2]
|
||||
_ = edAdd (edPt A2) (edPt q2) := rfl
|
||||
rw [h, hA2pt, hq2pt]
|
||||
rfl
|
||||
-- n3 ← q3.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q3 hq3v) as ⟨n3, hn3v, hn3n⟩
|
||||
-- write it at index 3
|
||||
step as ⟨j2, hj2⟩
|
||||
have hj2v : j2 = 3#usize := by clear * - hj2; scalar_tac
|
||||
rw [hj2v]
|
||||
step as ⟨Ai3, hA3⟩
|
||||
have hl3 : (↑Ai3 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n3, n0, n0, n0, n0] := by
|
||||
simp only [hA3, Array.set_val_eq, hl2]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 3: read entry 3 (cache of q3), write entry 4 = cache of 2A + q3
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter2 (by clear * - hsv2 hev2; scalar_tac)) as ⟨o3, iter3, ho3, hs3, he3⟩
|
||||
simp only [ho3]
|
||||
have hsv3 : iter3.start.val = 4 := by clear * - hs3 hsv2; omega
|
||||
have hev3 : iter3.«end».val = 7 := by clear * - he3 hev2; scalar_tac
|
||||
have hidx3 : iter2.start = 3#usize := by clear * - hsv2; scalar_tac
|
||||
rw [hidx3]
|
||||
-- entry 3 out of the array
|
||||
step as ⟨e3x, he3x⟩
|
||||
simp [hl3] at he3x
|
||||
rw [he3x]
|
||||
-- cp ← A2 + n3 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n3 hn3n hA2v hq3v hA2c hq3c hn3v) as
|
||||
⟨cp3, cb3X, cb3Y, cb3Z, cb3T, cz3, ct3, cx3, cy3⟩
|
||||
-- q4 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp3 (cb3X.mono (by norm_num))
|
||||
(cb3Y.mono (by norm_num)) cb3Z (cb3T.mono (by norm_num)) cz3 ct3) as
|
||||
⟨q4, hq4v, hq4x, hq4y⟩
|
||||
have hq4c : OnCurveExt q4 := by
|
||||
show OnCurve (edX q4) (edY q4)
|
||||
rw [hq4x, cx3, hq4y, cy3]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q3) (edY q3) from hq3c)
|
||||
have hq4pt : edPt q4 = edOdd 4 (edPt A) := by
|
||||
have h : edPt q4 = edAdd (edPt A2) (edPt q3) := by
|
||||
calc edPt q4 = (edX q4, edY q4) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q3)).1, (edAdd (edPt A2) (edPt q3)).2) := by
|
||||
rw [hq4x, cx3, hq4y, cy3]
|
||||
_ = edAdd (edPt A2) (edPt q3) := rfl
|
||||
rw [h, hA2pt, hq3pt]
|
||||
rfl
|
||||
-- n4 ← q4.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q4 hq4v) as ⟨n4, hn4v, hn4n⟩
|
||||
-- write it at index 4
|
||||
step as ⟨j3, hj3⟩
|
||||
have hj3v : j3 = 4#usize := by clear * - hj3; scalar_tac
|
||||
rw [hj3v]
|
||||
step as ⟨Ai4, hA4⟩
|
||||
have hl4 : (↑Ai4 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n3, n4, n0, n0, n0] := by
|
||||
simp only [hA4, Array.set_val_eq, hl3]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 4: read entry 4 (cache of q4), write entry 5 = cache of 2A + q4
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter3 (by clear * - hsv3 hev3; scalar_tac)) as ⟨o4, iter4, ho4, hs4, he4⟩
|
||||
simp only [ho4]
|
||||
have hsv4 : iter4.start.val = 5 := by clear * - hs4 hsv3; omega
|
||||
have hev4 : iter4.«end».val = 7 := by clear * - he4 hev3; scalar_tac
|
||||
have hidx4 : iter3.start = 4#usize := by clear * - hsv3; scalar_tac
|
||||
rw [hidx4]
|
||||
-- entry 4 out of the array
|
||||
step as ⟨e4x, he4x⟩
|
||||
simp [hl4] at he4x
|
||||
rw [he4x]
|
||||
-- cp ← A2 + n4 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n4 hn4n hA2v hq4v hA2c hq4c hn4v) as
|
||||
⟨cp4, cb4X, cb4Y, cb4Z, cb4T, cz4, ct4, cx4, cy4⟩
|
||||
-- q5 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp4 (cb4X.mono (by norm_num))
|
||||
(cb4Y.mono (by norm_num)) cb4Z (cb4T.mono (by norm_num)) cz4 ct4) as
|
||||
⟨q5, hq5v, hq5x, hq5y⟩
|
||||
have hq5c : OnCurveExt q5 := by
|
||||
show OnCurve (edX q5) (edY q5)
|
||||
rw [hq5x, cx4, hq5y, cy4]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q4) (edY q4) from hq4c)
|
||||
have hq5pt : edPt q5 = edOdd 5 (edPt A) := by
|
||||
have h : edPt q5 = edAdd (edPt A2) (edPt q4) := by
|
||||
calc edPt q5 = (edX q5, edY q5) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q4)).1, (edAdd (edPt A2) (edPt q4)).2) := by
|
||||
rw [hq5x, cx4, hq5y, cy4]
|
||||
_ = edAdd (edPt A2) (edPt q4) := rfl
|
||||
rw [h, hA2pt, hq4pt]
|
||||
rfl
|
||||
-- n5 ← q5.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q5 hq5v) as ⟨n5, hn5v, hn5n⟩
|
||||
-- write it at index 5
|
||||
step as ⟨j4, hj4⟩
|
||||
have hj4v : j4 = 5#usize := by clear * - hj4; scalar_tac
|
||||
rw [hj4v]
|
||||
step as ⟨Ai5, hA5⟩
|
||||
have hl5 : (↑Ai5 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n3, n4, n5, n0, n0] := by
|
||||
simp only [hA5, Array.set_val_eq, hl4]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 5: read entry 5 (cache of q5), write entry 6 = cache of 2A + q5
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter4 (by clear * - hsv4 hev4; scalar_tac)) as ⟨o5, iter5, ho5, hs5, he5⟩
|
||||
simp only [ho5]
|
||||
have hsv5 : iter5.start.val = 6 := by clear * - hs5 hsv4; omega
|
||||
have hev5 : iter5.«end».val = 7 := by clear * - he5 hev4; scalar_tac
|
||||
have hidx5 : iter4.start = 5#usize := by clear * - hsv4; scalar_tac
|
||||
rw [hidx5]
|
||||
-- entry 5 out of the array
|
||||
step as ⟨e5x, he5x⟩
|
||||
simp [hl5] at he5x
|
||||
rw [he5x]
|
||||
-- cp ← A2 + n5 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n5 hn5n hA2v hq5v hA2c hq5c hn5v) as
|
||||
⟨cp5, cb5X, cb5Y, cb5Z, cb5T, cz5, ct5, cx5, cy5⟩
|
||||
-- q6 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp5 (cb5X.mono (by norm_num))
|
||||
(cb5Y.mono (by norm_num)) cb5Z (cb5T.mono (by norm_num)) cz5 ct5) as
|
||||
⟨q6, hq6v, hq6x, hq6y⟩
|
||||
have hq6c : OnCurveExt q6 := by
|
||||
show OnCurve (edX q6) (edY q6)
|
||||
rw [hq6x, cx5, hq6y, cy5]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q5) (edY q5) from hq5c)
|
||||
have hq6pt : edPt q6 = edOdd 6 (edPt A) := by
|
||||
have h : edPt q6 = edAdd (edPt A2) (edPt q5) := by
|
||||
calc edPt q6 = (edX q6, edY q6) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q5)).1, (edAdd (edPt A2) (edPt q5)).2) := by
|
||||
rw [hq6x, cx5, hq6y, cy5]
|
||||
_ = edAdd (edPt A2) (edPt q5) := rfl
|
||||
rw [h, hA2pt, hq5pt]
|
||||
rfl
|
||||
-- n6 ← q6.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q6 hq6v) as ⟨n6, hn6v, hn6n⟩
|
||||
-- write it at index 6
|
||||
step as ⟨j5, hj5⟩
|
||||
have hj5v : j5 = 6#usize := by clear * - hj5; scalar_tac
|
||||
rw [hj5v]
|
||||
step as ⟨Ai6, hA6⟩
|
||||
have hl6 : (↑Ai6 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n3, n4, n5, n6, n0] := by
|
||||
simp only [hA6, Array.set_val_eq, hl5]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 6: read entry 6 (cache of q6), write entry 7 = cache of 2A + q6
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_lt_spec iter5 (by clear * - hsv5 hev5; scalar_tac)) as ⟨o6, iter6, ho6, hs6, he6⟩
|
||||
simp only [ho6]
|
||||
have hsv6 : iter6.start.val = 7 := by clear * - hs6 hsv5; omega
|
||||
have hev6 : iter6.«end».val = 7 := by clear * - he6 hev5; scalar_tac
|
||||
have hidx6 : iter5.start = 6#usize := by clear * - hsv5; scalar_tac
|
||||
rw [hidx6]
|
||||
-- entry 6 out of the array
|
||||
step as ⟨e6x, he6x⟩
|
||||
simp [hl6] at he6x
|
||||
rw [he6x]
|
||||
-- cp ← A2 + n6 (the mixed-add kernel law)
|
||||
step with (add_projniels_law A2 n6 hn6n hA2v hq6v hA2c hq6c hn6v) as
|
||||
⟨cp6, cb6X, cb6Y, cb6Z, cb6T, cz6, ct6, cx6, cy6⟩
|
||||
-- q7 ← cp.as_extended (valid extended point denoting the sum)
|
||||
step with (compl_as_extended_law cp6 (cb6X.mono (by norm_num))
|
||||
(cb6Y.mono (by norm_num)) cb6Z (cb6T.mono (by norm_num)) cz6 ct6) as
|
||||
⟨q7, hq7v, hq7x, hq7y⟩
|
||||
have hq7c : OnCurveExt q7 := by
|
||||
show OnCurve (edX q7) (edY q7)
|
||||
rw [hq7x, cx6, hq7y, cy6]
|
||||
exact edAdd_closure (show OnCurve (edX A2) (edY A2) from hA2c)
|
||||
(show OnCurve (edX q6) (edY q6) from hq6c)
|
||||
have hq7pt : edPt q7 = edOdd 7 (edPt A) := by
|
||||
have h : edPt q7 = edAdd (edPt A2) (edPt q6) := by
|
||||
calc edPt q7 = (edX q7, edY q7) := rfl
|
||||
_ = ((edAdd (edPt A2) (edPt q6)).1, (edAdd (edPt A2) (edPt q6)).2) := by
|
||||
rw [hq7x, cx6, hq7y, cy6]
|
||||
_ = edAdd (edPt A2) (edPt q6) := rfl
|
||||
rw [h, hA2pt, hq6pt]
|
||||
rfl
|
||||
-- n7 ← q7.as_projective_niels (the new table entry)
|
||||
step with (edwards_as_projective_niels_spec q7 hq7v) as ⟨n7, hn7v, hn7n⟩
|
||||
-- write it at index 7
|
||||
step as ⟨j6, hj6⟩
|
||||
have hj6v : j6 = 7#usize := by clear * - hj6; scalar_tac
|
||||
rw [hj6v]
|
||||
step as ⟨Ai7, hA7⟩
|
||||
have hl7 : (↑Ai7 : List backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
= [n0, n1, n2, n3, n4, n5, n6, n7] := by
|
||||
simp only [hA7, Array.set_val_eq, hl6]
|
||||
rfl
|
||||
try simp only [spec_ok]
|
||||
-- ── iteration 7: range exhausted (start = end = 7) — done
|
||||
apply loop_step
|
||||
simp only [window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from_loop.body]
|
||||
step with (range_next_ge_spec iter6 (by clear * - hsv6 hev6; scalar_tac)) as ⟨o7, iter7, ho7, hr7⟩
|
||||
simp only [ho7]
|
||||
try simp only [spec_ok]
|
||||
refine ⟨n0, n1, n2, n3, n4, n5, n6, n7, hl7, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
|
||||
· exact ⟨hn0v, A, hn0n, hAv, hAc, hq0pt⟩
|
||||
· exact ⟨hn1v, q1, hn1n, hq1v, hq1c, hq1pt⟩
|
||||
· exact ⟨hn2v, q2, hn2n, hq2v, hq2c, hq2pt⟩
|
||||
· exact ⟨hn3v, q3, hn3n, hq3v, hq3c, hq3pt⟩
|
||||
· exact ⟨hn4v, q4, hn4n, hq4v, hq4c, hq4pt⟩
|
||||
· exact ⟨hn5v, q5, hn5n, hq5v, hq5c, hq5pt⟩
|
||||
· exact ⟨hn6v, q6, hn6n, hq6v, hq6c, hq6pt⟩
|
||||
· exact ⟨hn7v, q7, hn7n, hq7v, hq7c, hq7pt⟩
|
||||
|
||||
/-! ### The public table-construction spec -/
|
||||
|
||||
/-- **NafLookupTable5::from(&A)**: for a valid on-curve A, the table's 8
|
||||
entries are valid niels caches of valid on-curve points denoting
|
||||
A, 3A, 5A, …, 15A — the odd multiples as `edOdd` values over the
|
||||
proven abstract Edwards addition. -/
|
||||
theorem naf_table_spec (A : EdPoint) (hA : ExtValid A) (hcA : OnCurveExt A) :
|
||||
window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from A
|
||||
⦃ tbl => ∃ e0 e1 e2 e3 e4 e5 e6 e7,
|
||||
tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7] ∧
|
||||
NafEntryOf e0 A 0 ∧ NafEntryOf e1 A 1 ∧ NafEntryOf e2 A 2 ∧
|
||||
NafEntryOf e3 A 3 ∧ NafEntryOf e4 A 4 ∧ NafEntryOf e5 A 5 ∧
|
||||
NafEntryOf e6 A 6 ∧ NafEntryOf e7 A 7 ⦄ := by
|
||||
unfold window.NafLookupTable5ProjectiveNielsPoint.Insts.CoreConvertFromSharedAEdwardsPoint.from
|
||||
step with (edwards_as_projective_niels_spec A hA) as ⟨pnp, hpv, hpn⟩
|
||||
step with (edwards_double_law A hA hcA) as ⟨A2, hA2v, hA2c, hA2pt⟩
|
||||
step with (naf_table_loop_spec A A2 (Array.repeat 8#usize pnp) pnp
|
||||
(by simp [List.replicate]) hpv hpn hA hcA hA2v hA2c hA2pt) as
|
||||
⟨e0, e1, e2, e3, e4, e5, e6, e7, tblA, hl, h0, h1, h2, h3, h4, h5, h6, h7⟩
|
||||
try simp only [spec_ok]
|
||||
exact ⟨e0, e1, e2, e3, e4, e5, e6, e7, hl, h0, h1, h2, h3, h4, h5, h6, h7⟩
|
||||
|
||||
|
||||
/-! ### The table lookup -/
|
||||
|
||||
/-- **NafLookupTable5::select(x)** for odd x < 16: returns entry x/2 —
|
||||
enumerated per digit so downstream digit case-splits use it directly.
|
||||
The two `massert`s (x odd, x < 16) are DISCHARGED, certifying the
|
||||
absence of the lookup panic paths. -/
|
||||
theorem naf_select_spec
|
||||
(tbl : window.NafLookupTable5 backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(x : Usize)
|
||||
(e0 e1 e2 e3 e4 e5 e6 e7 : backend.serial.curve_models.ProjectiveNielsPoint)
|
||||
(hl : tblEntries tbl = [e0, e1, e2, e3, e4, e5, e6, e7])
|
||||
(hodd : x.val % 2 = 1) (hlt : x.val < 16) :
|
||||
window.NafLookupTable5.select
|
||||
backend.serial.curve_models.ProjectiveNielsPoint.Insts.CoreMarkerCopy tbl x
|
||||
⦃ r => (x.val = 1 → r = e0) ∧ (x.val = 3 → r = e1) ∧ (x.val = 5 → r = e2) ∧
|
||||
(x.val = 7 → r = e3) ∧ (x.val = 9 → r = e4) ∧ (x.val = 11 → r = e5) ∧
|
||||
(x.val = 13 → r = e6) ∧ (x.val = 15 → r = e7) ⦄ := by
|
||||
unfold window.NafLookupTable5.select
|
||||
step as ⟨lv, hlv⟩
|
||||
have hlv1 : lv = 1#usize := by
|
||||
clear * - hlv hodd
|
||||
have h1 : x.val &&& 1 = 1 := by rw [Nat.and_one_is_mod, hodd]
|
||||
scalar_tac
|
||||
step with (massert_spec _ hlv1) as ⟨hu1⟩
|
||||
step with (massert_spec (x < 16#usize) (by clear * - hlt; scalar_tac)) as ⟨hu2⟩
|
||||
step as ⟨i, hi⟩
|
||||
step as ⟨r, hr⟩
|
||||
simp only [tblEntries] at hl
|
||||
simp [hl] at hr
|
||||
refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ <;> intro hx
|
||||
· have hik : i.val = 0 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 1 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 2 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 3 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 4 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 5 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 6 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
· have hik : i.val = 7 := by clear * - hi hx; omega
|
||||
rw [hr]; simp [hik]
|
||||
|
||||
end CurveFieldProofs
|
||||
|
|
@ -51,16 +51,29 @@ PROOFS=(
|
|||
EdAddAffNiels
|
||||
EdConvert
|
||||
EdMain
|
||||
DsmTableSpec
|
||||
DsmStepSpec
|
||||
DsmLoopSpec
|
||||
)
|
||||
# Fully-qualified certificate names; each must be axiom-clean.
|
||||
CERTS=(
|
||||
CurveFieldProofs.fieldImplementation
|
||||
CurveFieldProofs.edwardsImplementation
|
||||
CurveFieldProofs.naf_table_spec
|
||||
CurveFieldProofs.naf_select_spec
|
||||
CurveFieldProofs.proj_double_law
|
||||
CurveFieldProofs.compl_as_projective_law
|
||||
CurveFieldProofs.dsm_step_p_law
|
||||
CurveFieldProofs.dsm_step_b_law
|
||||
CurveFieldProofs.dsm_loop_spec
|
||||
)
|
||||
# Imports needed so every certificate in CERTS is in scope for the audit.
|
||||
AUDIT_IMPORTS=(
|
||||
Proofs.FieldMain
|
||||
Proofs.EdMain
|
||||
Proofs.DsmTableSpec
|
||||
Proofs.DsmStepSpec
|
||||
Proofs.DsmLoopSpec
|
||||
)
|
||||
|
||||
# ── Phase 0: resource + integrity guards ────────────────────────────────────
|
||||
|
|
|
|||
Loading…
Reference in a new issue