mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
c093098b64
bridge (Proofs/PointLiftSpec.lean, kernel-audited) - vartime_dsm_basepoint_spec: the PUBLIC dsm entry the verifier calls (EdwardsPoint::vartime_double_scalar_mul_basepoint) satisfies the dsm certificate - under the serial pin the backend dispatch is the real constant Serial, so the wrapper reduces definitionally to the certified serial path. No new axioms; in CERTS. - rangeEq_iff_bytesVal: the verifier's byte-wise comparison IS value equality of the encodings - little-endian digits are unique (32-fold byte peel, one omega over the flat bound set; U8 equality recovered via UScalar.eq_of_val_eq). With ed_compress_spec and from_bytes_mod_order_wide_spec already landed, the half-lift now needs only the recompute bind-chain inversion (the sha calls are oracles - inverted from the hrec hypothesis the apex carries) and the assembly theorem. Full button green fresh. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
174 lines
11 KiB
Text
174 lines
11 KiB
Text
/- ──────────────────────────────────────────────────────────────────────────────
|
||
Proofs/PointLiftSpec.lean — phase 2, the half-lift toward the point-level
|
||
verification equation.
|
||
|
||
This file assembles the connective tissue between the byte-level apex
|
||
(SigApexSpec: accept ⇔ byte equality) and the denoted-point world:
|
||
|
||
1. `vartime_dsm_basepoint_spec` — the public dsm entry is its serial
|
||
implementation (the backend dispatch is REAL code under the serial
|
||
pin: get_selected_backend = ok .Serial), so the dsm certificate
|
||
transfers to the function the verifier actually calls.
|
||
2. `bytesVal_inj` / `rangeEq_iff_bytesVal` — the byte-wise comparison the
|
||
verifier performs is exactly value equality of the two encodings
|
||
(little-endian digits are unique: peel one byte at a time).
|
||
|
||
The recompute-chain inversion and the half-lift theorem itself build on
|
||
these in the sequel (the sha calls are oracles — axioms cannot be walked,
|
||
so the chain is INVERTED from the `hrec` hypothesis the apex already
|
||
carries, exactly as the apex itself is hypothesis-parametric).
|
||
────────────────────────────────────────────────────────────────────────────── -/
|
||
import Proofs.CompressSpec
|
||
import Proofs.ScalarPackSpec
|
||
import Proofs.DsmMulSpec
|
||
import Proofs.SigApexSpec
|
||
open Aeneas Aeneas.Std Result
|
||
open curve25519_dalek
|
||
|
||
set_option maxHeartbeats 4000000
|
||
set_option linter.unusedSimpArgs false
|
||
set_option maxRecDepth 8000
|
||
|
||
namespace CurveFieldProofs
|
||
|
||
open Aeneas.Std.WP
|
||
|
||
/-- **The public dsm entry satisfies the dsm certificate**: the backend
|
||
dispatch is the real constant Serial (no axiom), so
|
||
`vartime_double_scalar_mul_basepoint` IS the certified serial path. -/
|
||
theorem vartime_dsm_basepoint_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) :
|
||
edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint 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
|
||
unfold edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint
|
||
backend.vartime_double_base_mul backend.get_selected_backend
|
||
simp only [bind_tc_ok]
|
||
exact vartime_double_base_mul_spec a b 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
|
||
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
|
||
hab hbb Va Vb hVa hVb hValt hVblt hAv hAc
|
||
|
||
/-- One digit-peeling step: equal little-endian values with byte-sized heads
|
||
force equal heads and equal tails. -/
|
||
theorem byte_peel {b c X Y : ℕ} (hb : b < 2^8) (hc : c < 2^8)
|
||
(h : b + 2^8 * X = c + 2^8 * Y) : b = c ∧ X = Y := by
|
||
omega
|
||
|
||
/-- **Little-endian digits are unique**: equal `bytesVal` forces equal byte
|
||
arrays, hence the verifier's byte-wise comparison IS value equality. -/
|
||
theorem rangeEq_iff_bytesVal (e r : Std.Array Std.U8 32#usize) :
|
||
rangeEq e r 0 ↔ bytesVal e = bytesVal r := by
|
||
obtain ⟨e0, e1, e2, e3, e4, e5, e6, e7, e8, e9, e10, e11, e12, e13, e14, e15,
|
||
e16, e17, e18, e19, e20, e21, e22, e23, e24, e25, e26, e27, e28, e29, e30, e31,
|
||
hel⟩ := Bytes32.exists_bytes e
|
||
obtain ⟨r0, r1, r2, r3, r4, r5, r6, r7, r8, r9, r10, r11, r12, r13, r14, r15,
|
||
r16, r17, r18, r19, r20, r21, r22, r23, r24, r25, r26, r27, r28, r29, r30, r31,
|
||
hrl⟩ := Bytes32.exists_bytes r
|
||
constructor
|
||
· -- pointwise equality ⇒ equal sums
|
||
intro h
|
||
have hpt : ∀ j, j < 32 → e.val[j]! = r.val[j]! := fun j hj => h j (Nat.zero_le _) hj
|
||
have h0 : e0 = r0 := by simpa [hel, hrl] using hpt 0 (by norm_num)
|
||
have h1 : e1 = r1 := by simpa [hel, hrl] using hpt 1 (by norm_num)
|
||
have h2 : e2 = r2 := by simpa [hel, hrl] using hpt 2 (by norm_num)
|
||
have h3 : e3 = r3 := by simpa [hel, hrl] using hpt 3 (by norm_num)
|
||
have h4 : e4 = r4 := by simpa [hel, hrl] using hpt 4 (by norm_num)
|
||
have h5 : e5 = r5 := by simpa [hel, hrl] using hpt 5 (by norm_num)
|
||
have h6 : e6 = r6 := by simpa [hel, hrl] using hpt 6 (by norm_num)
|
||
have h7 : e7 = r7 := by simpa [hel, hrl] using hpt 7 (by norm_num)
|
||
have h8 : e8 = r8 := by simpa [hel, hrl] using hpt 8 (by norm_num)
|
||
have h9 : e9 = r9 := by simpa [hel, hrl] using hpt 9 (by norm_num)
|
||
have h10 : e10 = r10 := by simpa [hel, hrl] using hpt 10 (by norm_num)
|
||
have h11 : e11 = r11 := by simpa [hel, hrl] using hpt 11 (by norm_num)
|
||
have h12 : e12 = r12 := by simpa [hel, hrl] using hpt 12 (by norm_num)
|
||
have h13 : e13 = r13 := by simpa [hel, hrl] using hpt 13 (by norm_num)
|
||
have h14 : e14 = r14 := by simpa [hel, hrl] using hpt 14 (by norm_num)
|
||
have h15 : e15 = r15 := by simpa [hel, hrl] using hpt 15 (by norm_num)
|
||
have h16 : e16 = r16 := by simpa [hel, hrl] using hpt 16 (by norm_num)
|
||
have h17 : e17 = r17 := by simpa [hel, hrl] using hpt 17 (by norm_num)
|
||
have h18 : e18 = r18 := by simpa [hel, hrl] using hpt 18 (by norm_num)
|
||
have h19 : e19 = r19 := by simpa [hel, hrl] using hpt 19 (by norm_num)
|
||
have h20 : e20 = r20 := by simpa [hel, hrl] using hpt 20 (by norm_num)
|
||
have h21 : e21 = r21 := by simpa [hel, hrl] using hpt 21 (by norm_num)
|
||
have h22 : e22 = r22 := by simpa [hel, hrl] using hpt 22 (by norm_num)
|
||
have h23 : e23 = r23 := by simpa [hel, hrl] using hpt 23 (by norm_num)
|
||
have h24 : e24 = r24 := by simpa [hel, hrl] using hpt 24 (by norm_num)
|
||
have h25 : e25 = r25 := by simpa [hel, hrl] using hpt 25 (by norm_num)
|
||
have h26 : e26 = r26 := by simpa [hel, hrl] using hpt 26 (by norm_num)
|
||
have h27 : e27 = r27 := by simpa [hel, hrl] using hpt 27 (by norm_num)
|
||
have h28 : e28 = r28 := by simpa [hel, hrl] using hpt 28 (by norm_num)
|
||
have h29 : e29 = r29 := by simpa [hel, hrl] using hpt 29 (by norm_num)
|
||
have h30 : e30 = r30 := by simpa [hel, hrl] using hpt 30 (by norm_num)
|
||
have h31 : e31 = r31 := by simpa [hel, hrl] using hpt 31 (by norm_num)
|
||
simp only [bytesVal, hel, hrl, h0, h1, h2, h3, h4, h5, h6, h7, h8, h9, h10, h11, h12, h13, h14, h15, h16, h17, h18, h19, h20, h21, h22, h23, h24, h25, h26, h27, h28, h29, h30, h31]
|
||
· -- equal sums ⇒ pointwise equality: peel 32 bytes
|
||
intro h
|
||
simp only [bytesVal, hel, hrl] at h
|
||
intro j hj0 hj32
|
||
simp only [hel, hrl]
|
||
-- normalize both sums into head + 2^8·tail form, peel, recurse
|
||
have hb : ∀ x : Std.U8, x.val < 2^8 := fun x => by scalar_tac
|
||
have hpeel : e0.val = r0.val ∧ e1.val = r1.val ∧ e2.val = r2.val ∧
|
||
e3.val = r3.val ∧ e4.val = r4.val ∧ e5.val = r5.val ∧
|
||
e6.val = r6.val ∧ e7.val = r7.val ∧ e8.val = r8.val ∧
|
||
e9.val = r9.val ∧ e10.val = r10.val ∧ e11.val = r11.val ∧
|
||
e12.val = r12.val ∧ e13.val = r13.val ∧ e14.val = r14.val ∧
|
||
e15.val = r15.val ∧ e16.val = r16.val ∧ e17.val = r17.val ∧
|
||
e18.val = r18.val ∧ e19.val = r19.val ∧ e20.val = r20.val ∧
|
||
e21.val = r21.val ∧ e22.val = r22.val ∧ e23.val = r23.val ∧
|
||
e24.val = r24.val ∧ e25.val = r25.val ∧ e26.val = r26.val ∧
|
||
e27.val = r27.val ∧ e28.val = r28.val ∧ e29.val = r29.val ∧
|
||
e30.val = r30.val ∧ e31.val = r31.val := by
|
||
have hbe0 := hb e0; have hbr0 := hb r0
|
||
have hbe1 := hb e1; have hbr1 := hb r1
|
||
have hbe2 := hb e2; have hbr2 := hb r2
|
||
have hbe3 := hb e3; have hbr3 := hb r3
|
||
have hbe4 := hb e4; have hbr4 := hb r4
|
||
have hbe5 := hb e5; have hbr5 := hb r5
|
||
have hbe6 := hb e6; have hbr6 := hb r6
|
||
have hbe7 := hb e7; have hbr7 := hb r7
|
||
have hbe8 := hb e8; have hbr8 := hb r8
|
||
have hbe9 := hb e9; have hbr9 := hb r9
|
||
have hbe10 := hb e10; have hbr10 := hb r10
|
||
have hbe11 := hb e11; have hbr11 := hb r11
|
||
have hbe12 := hb e12; have hbr12 := hb r12
|
||
have hbe13 := hb e13; have hbr13 := hb r13
|
||
have hbe14 := hb e14; have hbr14 := hb r14
|
||
have hbe15 := hb e15; have hbr15 := hb r15
|
||
have hbe16 := hb e16; have hbr16 := hb r16
|
||
have hbe17 := hb e17; have hbr17 := hb r17
|
||
have hbe18 := hb e18; have hbr18 := hb r18
|
||
have hbe19 := hb e19; have hbr19 := hb r19
|
||
have hbe20 := hb e20; have hbr20 := hb r20
|
||
have hbe21 := hb e21; have hbr21 := hb r21
|
||
have hbe22 := hb e22; have hbr22 := hb r22
|
||
have hbe23 := hb e23; have hbr23 := hb r23
|
||
have hbe24 := hb e24; have hbr24 := hb r24
|
||
have hbe25 := hb e25; have hbr25 := hb r25
|
||
have hbe26 := hb e26; have hbr26 := hb r26
|
||
have hbe27 := hb e27; have hbr27 := hb r27
|
||
have hbe28 := hb e28; have hbr28 := hb r28
|
||
have hbe29 := hb e29; have hbr29 := hb r29
|
||
have hbe30 := hb e30; have hbr30 := hb r30
|
||
have hbe31 := hb e31; have hbr31 := hb r31
|
||
omega
|
||
obtain ⟨q0, q1, q2, q3, q4, q5, q6, q7, q8, q9, q10, q11, q12, q13, q14,
|
||
q15, q16, q17, q18, q19, q20, q21, q22, q23, q24, q25, q26, q27, q28,
|
||
q29, q30, q31⟩ := hpeel
|
||
-- j is one of 0..31: close each case with the matching byte equality
|
||
interval_cases j <;> simp_all <;> exact UScalar.eq_of_val_eq (by assumption)
|
||
|
||
end CurveFieldProofs
|