mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
eb2c77be09
(verify_accepts_iff_decompress, button-enforced)
THE THEOREM: under the apex hypotheses, the signature's R bytes
DECOMPRESS to a valid on-curve point Pt, and
verifier accepts <=> Pt = [k]*(-A) + [s]*B (as points)
- accept iff decompress(R) equals the recomputed point. Every link of
the chain (byte comparison <-> canonical-encoding equality <-> point
equality <-> decompressed-point equality) is machine-checked over the
extracted code. Axiom cone EXACTLY the SHA-512 + wire-format boundary;
Phase 3b now enforces FOUR certificate tiers (byte apex, half-lift,
point equation, full lift).
Proofs/DecompressMain.lean:
- edwards_d_denote: the extracted EDWARDS_D constant denotes THE curve
d (edwards_d_spec + edD_char cancelled by 121666 nonzero).
- decompress_of_canonical (standard three axioms): canonical encodings
of valid on-curve points decompress to them - from_bytes recovers the
y-residue exactly (sign bit discarded), Q's own x witnesses the
square so sqrt_ratio_i returns the even root, the sign bit (Q's
x-parity, from byte 31) selects +/-root, and the parity-injectivity
argument pins the selection to edX Q; the assembled {X,Y,1,X*Y} is
ExtValid and on-curve.
- verify_accepts_iff_decompress: the capstone composition.
Full button green fresh. Remaining: replicate x3, coherence pass 4.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
321 lines
17 KiB
Text
321 lines
17 KiB
Text
/- ──────────────────────────────────────────────────────────────────────────────
|
||
Proofs/DecompressMain.lean — phase 2, decompress step 3: THE CONSTRUCTIVE
|
||
DECOMPRESSION THEOREM.
|
||
|
||
`decompress_of_canonical`: for a valid on-curve point Q whose canonical
|
||
encoding is the bytes rb, the extracted `CompressedEdwardsY::decompress`
|
||
succeeds with `some P` — a valid on-curve point denoting exactly Q.
|
||
|
||
The chain: from_bytes recovers the y-residue (the sign bit at 2²⁵⁵ is
|
||
discarded — from_bytes_spec is exact below it); u = y²−1 and
|
||
v = d·y²+1 are built by certified ops with ⟪EDWARDS_D⟫ = d
|
||
(edwards_d_spec + edD_char, cancelled by 121666 ≠ 0); Q's own
|
||
x-coordinate witnesses that u/v is a square (x_sq_of_onCurve), so
|
||
sqrt_ratio_i succeeds with the even-parity root; the sign bit — Q's
|
||
x-parity, extracted from byte 31 — selects between ±root, and the
|
||
parity-injectivity argument (enc_inj_coord, on-curve invariance of x²)
|
||
pins the selected root to edX Q. The result point {X, Y, 1, X·Y} is
|
||
ExtValid, on-curve, and denotes Q.
|
||
────────────────────────────────────────────────────────────────────────────── -/
|
||
import Proofs.FromBytesSpec
|
||
open Aeneas Aeneas.Std Result
|
||
open curve25519_dalek
|
||
|
||
set_option maxHeartbeats 8000000
|
||
set_option linter.unusedSimpArgs false
|
||
set_option maxRecDepth 8000
|
||
|
||
namespace CurveFieldProofs
|
||
|
||
open Aeneas.Std.WP
|
||
|
||
/-- ⟪EDWARDS_D⟫ is THE curve constant d. -/
|
||
theorem edwards_d_denote :
|
||
backend.serial.u64.constants.EDWARDS_D ⦃ D => Bnd D (2^52) ∧ ⟪D⟫ = edD ⦄ := by
|
||
apply spec_mono edwards_d_spec
|
||
intro D ⟨hb, hd⟩
|
||
refine ⟨hb, ?_⟩
|
||
have h121666 : (121666 : Fp) ≠ 0 := by
|
||
have h : ((121666 : ℕ) : Fp) ≠ 0 := natCast_ne_zero_of_mod (by decide)
|
||
exact_mod_cast h
|
||
have hchar := edD_char
|
||
have : (121666 : Fp) * (⟪D⟫ - edD) = 0 := by linear_combination hd - hchar
|
||
rcases mul_eq_zero.mp this with h | h
|
||
· exact absurd h h121666
|
||
· linear_combination h
|
||
|
||
open ed25519_dalek in
|
||
/-- **THE CONSTRUCTIVE DECOMPRESSION THEOREM**: canonical encodings of
|
||
valid on-curve points decompress to them. -/
|
||
theorem decompress_of_canonical (Q : EdPoint) (hQv : ExtValid Q) (hQc : OnCurveExt Q)
|
||
(rb : Std.Array Std.U8 32#usize)
|
||
(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)
|
||
(hbl : (↑rb : 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])
|
||
(henc : bytesVal rb = (edY Q).val + ((edX Q).val % 2) * 2^255) :
|
||
edwards.CompressedEdwardsY.decompress rb ⦃ o =>
|
||
∃ Pt : EdPoint, o = some Pt ∧ ExtValid Pt ∧ OnCurveExt Pt ∧ edPt Pt = edPt Q ⦄ := by
|
||
haveI : NeZero P := ⟨by unfold P; norm_num⟩
|
||
unfold edwards.CompressedEdwardsY.decompress curve25519_dalek.edwards.decompress.step_1
|
||
-- as_bytes is the identity; parse y
|
||
simp only [edwards.CompressedEdwardsY.as_bytes, bind_tc_ok]
|
||
step with (from_bytes_spec rb 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 hbl)
|
||
as ⟨Y, hbY, hYv⟩
|
||
-- the parsed field element denotes edY Q
|
||
have hyresid : (edY Q).val < 2^255 :=
|
||
lt_of_lt_of_le (ZMod.val_lt _) (by unfold P; norm_num)
|
||
have hparle : (edX Q).val % 2 ≤ 1 := Nat.le_of_lt_succ (Nat.mod_lt _ (by norm_num))
|
||
have hYval : feVal Y = (edY Q).val := by
|
||
rw [hYv, henc]
|
||
have : ((edY Q).val + (edX Q).val % 2 * 2^255) % 2^255 = (edY Q).val := by
|
||
rcases Nat.mod_two_eq_zero_or_one (edX Q).val with h | h <;> rw [h] <;> omega
|
||
exact this
|
||
have hYden : ⟪Y⟫ = edY Q := by
|
||
apply ZMod.val_injective
|
||
show (⟪Y⟫).val = (edY Q).val
|
||
unfold denote
|
||
rw [ZMod.val_natCast, hYval, Nat.mod_eq_of_lt (ZMod.val_lt _)]
|
||
-- Z = 1
|
||
step with one_spec as ⟨Z, hbZ, hZv⟩
|
||
-- YY = y², u = y² − 1
|
||
step with (square_spec' Y (Bnd.mono hbY (by norm_num))) as ⟨YY, hbYY, hYY⟩
|
||
obtain ⟨yy0, yy1, yy2, yy3, yy4, hyyl⟩ := Fe.exists_limbs YY
|
||
obtain ⟨z0, z1, z2, z3, z4, hzl⟩ := Fe.exists_limbs Z
|
||
step with (sub_spec YY Z yy0 yy1 yy2 yy3 yy4 z0 z1 z2 z3 z4 hyyl hzl
|
||
(Bnd.mono hbYY (by norm_num)) (Bnd.mono hbZ (by norm_num))) as ⟨u, hbu, huv⟩
|
||
-- D, then v = d·y² + 1
|
||
step with edwards_d_denote as ⟨D, hbD, hDv⟩
|
||
step with (mul_spec' YY D (Bnd.mono hbYY (by norm_num)) (Bnd.mono hbD (by norm_num)))
|
||
as ⟨vd, hbvd, hvd⟩
|
||
step with (add_spec'' vd Z (Bnd.mono hbvd (by norm_num)) (Bnd.mono hbZ (by norm_num)))
|
||
as ⟨v, hbv, hvv⟩
|
||
-- interpreted u, v
|
||
have huval : ⟪u⟫ = (edY Q)^2 - 1 := by
|
||
rw [huv, hYY, hYden, hZv]
|
||
ring
|
||
have hvval : ⟪v⟫ = 1 + edD * (edY Q)^2 := by
|
||
rw [hvv, hvd, hYY, hYden, hDv, hZv]
|
||
ring
|
||
-- Q's x witnesses the square; v never vanishes
|
||
have hvne : ⟪v⟫ ≠ 0 := by rw [hvval]; exact one_add_d_y_sq_ne_zero _
|
||
have hwit : (edX Q) ^ 2 * ⟪v⟫ = ⟪u⟫ := by
|
||
rw [hvval, huval]
|
||
exact x_sq_of_onCurve hQc
|
||
-- the square root succeeds with the even-parity root
|
||
step with (sqrt_ratio_i_sq_spec u v (Bnd.mono hbu (by norm_num))
|
||
(Bnd.mono hbv (by norm_num)) hvne (edX Q) hwit) as ⟨sc, sr, hc1, hbr, hrsq, hrpar⟩
|
||
-- the validity Choice converts to true
|
||
simp only [core.convert.IntoFrom.into, Bool.Insts.CoreConvertFromChoice.from,
|
||
bind_tc_ok]
|
||
rw [show (sc.val != 0) = true from by simp [hc1]]
|
||
rw [if_pos rfl]
|
||
-- ── step_2: the sign select ──────────────────────────────────────────────
|
||
unfold curve25519_dalek.edwards.decompress.step_2
|
||
simp only [edwards.CompressedEdwardsY.as_bytes, bind_tc_ok]
|
||
step as ⟨t31, ht31⟩
|
||
simp [hbl] at ht31
|
||
step as ⟨sgn, hsgn⟩
|
||
simp only [subtle.Choice.Insts.CoreConvertFromU8.from, bind_tc_ok]
|
||
-- the sign bit is Q's x-parity
|
||
have hb31v : b31.val = (edY Q).val / 2^248 + ((edX Q).val % 2) * 2^7 := by
|
||
have hexp : bytesVal rb = 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 := by
|
||
simp only [bytesVal, hbl]
|
||
rw [henc] at hexp
|
||
have hB0 : b0.val < 256 := by scalar_tac
|
||
have hB1 : b1.val < 256 := by scalar_tac
|
||
have hB2 : b2.val < 256 := by scalar_tac
|
||
have hB3 : b3.val < 256 := by scalar_tac
|
||
have hB4 : b4.val < 256 := by scalar_tac
|
||
have hB5 : b5.val < 256 := by scalar_tac
|
||
have hB6 : b6.val < 256 := by scalar_tac
|
||
have hB7 : b7.val < 256 := by scalar_tac
|
||
have hB8 : b8.val < 256 := by scalar_tac
|
||
have hB9 : b9.val < 256 := by scalar_tac
|
||
have hB10 : b10.val < 256 := by scalar_tac
|
||
have hB11 : b11.val < 256 := by scalar_tac
|
||
have hB12 : b12.val < 256 := by scalar_tac
|
||
have hB13 : b13.val < 256 := by scalar_tac
|
||
have hB14 : b14.val < 256 := by scalar_tac
|
||
have hB15 : b15.val < 256 := by scalar_tac
|
||
have hB16 : b16.val < 256 := by scalar_tac
|
||
have hB17 : b17.val < 256 := by scalar_tac
|
||
have hB18 : b18.val < 256 := by scalar_tac
|
||
have hB19 : b19.val < 256 := by scalar_tac
|
||
have hB20 : b20.val < 256 := by scalar_tac
|
||
have hB21 : b21.val < 256 := by scalar_tac
|
||
have hB22 : b22.val < 256 := by scalar_tac
|
||
have hB23 : b23.val < 256 := by scalar_tac
|
||
have hB24 : b24.val < 256 := by scalar_tac
|
||
have hB25 : b25.val < 256 := by scalar_tac
|
||
have hB26 : b26.val < 256 := by scalar_tac
|
||
have hB27 : b27.val < 256 := by scalar_tac
|
||
have hB28 : b28.val < 256 := by scalar_tac
|
||
have hB29 : b29.val < 256 := by scalar_tac
|
||
have hB30 : b30.val < 256 := by scalar_tac
|
||
have hB31 : b31.val < 256 := by scalar_tac
|
||
omega
|
||
have hsgnv : sgn.val = (edX Q).val % 2 := by
|
||
rw [hsgn, ht31, nat_shr, hb31v]
|
||
have : (edY Q).val / 2^248 < 2^7 := by
|
||
have := hyresid
|
||
omega
|
||
omega
|
||
-- −root, then select
|
||
obtain ⟨r0, r1, r2, r3, r4, hrl⟩ := Fe.exists_limbs sr
|
||
unfold Shared0FieldElement51.Insts.CoreOpsArithNegFieldElement51.neg
|
||
step with (neg_spec sr r0 r1 r2 r3 r4 hrl (Bnd.mono hbr (by norm_num)))
|
||
as ⟨Xn, hbXn, hXnv⟩
|
||
obtain ⟨n0, n1, n2, n3, n4, hnl⟩ := Fe.exists_limbs Xn
|
||
step with (fe_cond_assign_spec sr Xn sgn r0 r1 r2 r3 r4 n0 n1 n2 n3 n4 hrl hnl)
|
||
as ⟨X1, hX1l⟩
|
||
-- Bnd X1 first (needed by the T-multiply)
|
||
have hbX1 : Bnd X1 (2^52) := by
|
||
have hb1 : Bnd sr (2^52) := hbr
|
||
have hb2 : Bnd Xn (2^52) := hbXn
|
||
split at hX1l
|
||
· rw [Bnd_eq X1 r0 r1 r2 r3 r4 _ (by rw [hX1l])]
|
||
rw [Bnd_eq sr r0 r1 r2 r3 r4 _ hrl] at hb1
|
||
exact hb1
|
||
· rw [Bnd_eq X1 n0 n1 n2 n3 n4 _ (by rw [hX1l])]
|
||
rw [Bnd_eq Xn n0 n1 n2 n3 n4 _ hnl] at hb2
|
||
exact hb2
|
||
-- T = X1·Y
|
||
step with (mul_spec' X1 Y (Bnd.mono hbX1 (by norm_num)) (Bnd.mono hbY (by norm_num)))
|
||
as ⟨T, hbT, hTv⟩
|
||
try simp only [spec_ok]
|
||
-- ── the selected root IS edX Q ───────────────────────────────────────────
|
||
-- the root is on-curve (only x² appears in the equation)
|
||
have hrsq' : ⟪sr⟫ ^ 2 = (edX Q) ^ 2 := by
|
||
have h := hrsq
|
||
rw [hwit.symm] at h
|
||
have hcancel : (⟪sr⟫ ^ 2 - (edX Q) ^ 2) * ⟪v⟫ = 0 := by linear_combination h
|
||
rcases mul_eq_zero.mp hcancel with h' | h'
|
||
· linear_combination h'
|
||
· exact absurd h' hvne
|
||
have hronc : OnCurve ⟪sr⟫ (edY Q) := by
|
||
show -(⟪sr⟫^2) + (edY Q)^2 = 1 + edD * ⟪sr⟫^2 * (edY Q)^2
|
||
rw [hrsq']
|
||
exact hQc
|
||
have hX1den : ⟪X1⟫ = ⟪sr⟫ ∨ ⟪X1⟫ = -⟪sr⟫ := by
|
||
split at hX1l
|
||
· left
|
||
unfold denote
|
||
rw [feVal_eq X1 r0 r1 r2 r3 r4 (by rw [hX1l]),
|
||
feVal_eq sr r0 r1 r2 r3 r4 hrl]
|
||
· right
|
||
have : ⟪X1⟫ = ⟪Xn⟫ := by
|
||
unfold denote
|
||
rw [feVal_eq X1 n0 n1 n2 n3 n4 (by rw [hX1l]),
|
||
feVal_eq Xn n0 n1 n2 n3 n4 hnl]
|
||
rw [this, hXnv]
|
||
have hX1x : ⟪X1⟫ = edX Q := by
|
||
rcases Nat.mod_two_eq_zero_or_one (edX Q).val with hx | hx
|
||
· -- x has even parity: no flip (sgn = 0), root already matches by parity
|
||
have hs0 : sgn.val = 0 := by rw [hsgnv, hx]
|
||
have hkeep : ⟪X1⟫ = ⟪sr⟫ := by
|
||
split at hX1l
|
||
· unfold denote
|
||
rw [feVal_eq X1 r0 r1 r2 r3 r4 (by rw [hX1l]),
|
||
feVal_eq sr r0 r1 r2 r3 r4 hrl]
|
||
· exact absurd hs0 (by assumption)
|
||
rw [hkeep]
|
||
exact enc_inj_coord hronc hQc (by rw [hrpar, hx])
|
||
· -- x odd: the flip fires; −root has odd parity (root even, nonzero)
|
||
have hs1 : sgn.val ≠ 0 := by rw [hsgnv, hx]; norm_num
|
||
have hflip : ⟪X1⟫ = -⟪sr⟫ := by
|
||
split at hX1l
|
||
· exact absurd (by assumption) hs1
|
||
· have : ⟪X1⟫ = ⟪Xn⟫ := by
|
||
unfold denote
|
||
rw [feVal_eq X1 n0 n1 n2 n3 n4 (by rw [hX1l]),
|
||
feVal_eq Xn n0 n1 n2 n3 n4 hnl]
|
||
rw [this, hXnv]
|
||
have hrnz : ⟪sr⟫ ≠ 0 := by
|
||
intro hz
|
||
rw [hz] at hrsq'
|
||
have hxz : edX Q = 0 := by
|
||
have := hrsq'.symm
|
||
have h2 : (edX Q)^2 = 0 := by linear_combination -hrsq'
|
||
exact pow_eq_zero_iff (n := 2) (by norm_num) |>.mp h2
|
||
rw [hxz] at hx
|
||
simp at hx
|
||
have hnegonc : OnCurve (-⟪sr⟫) (edY Q) := by
|
||
show -((-⟪sr⟫)^2) + (edY Q)^2 = 1 + edD * (-⟪sr⟫)^2 * (edY Q)^2
|
||
have : (-⟪sr⟫)^2 = ⟪sr⟫^2 := by ring
|
||
rw [this, hrsq']
|
||
exact hQc
|
||
have hnegpar : (-⟪sr⟫).val % 2 = 1 := by
|
||
rw [ZMod.neg_val, if_neg hrnz]
|
||
have hlt := ZMod.val_lt ⟪sr⟫
|
||
have hpodd : P % 2 = 1 := by unfold P; norm_num
|
||
have hpos : 0 < (⟪sr⟫).val := by
|
||
rcases Nat.eq_zero_or_pos (⟪sr⟫).val with h | h
|
||
· exact absurd ((ZMod.val_eq_zero _).mp h) hrnz
|
||
· exact h
|
||
omega
|
||
rw [hflip]
|
||
exact enc_inj_coord hnegonc hQc (by rw [hnegpar, hx])
|
||
-- ── assemble the point ───────────────────────────────────────────────────
|
||
refine ⟨_, rfl, ?_, ?_, ?_⟩
|
||
· -- ExtValid
|
||
refine ⟨?_, Bnd.mono hbY (by norm_num), Bnd.mono hbZ (by norm_num), ?_, ?_, ?_⟩
|
||
· exact hbX1
|
||
· exact Bnd.mono hbT (by norm_num)
|
||
· rw [hZv]; norm_num
|
||
· -- coherence X·Y = Z·T
|
||
show ⟪X1⟫ * ⟪Y⟫ = ⟪Z⟫ * ⟪T⟫
|
||
rw [hTv, hZv]
|
||
ring
|
||
· -- on-curve
|
||
show OnCurve (⟪X1⟫ / ⟪Z⟫) (⟪Y⟫ / ⟪Z⟫)
|
||
rw [hZv, div_one, div_one, hX1x, hYden]
|
||
exact hQc
|
||
· -- denotes Q
|
||
show (⟪X1⟫ / ⟪Z⟫, ⟪Y⟫ / ⟪Z⟫) = edPt Q
|
||
rw [hZv, div_one, div_one, hX1x, hYden]
|
||
rfl
|
||
|
||
open ed25519_dalek in
|
||
/-- **THE FULL POINT-LEVEL LIFT.** Under the point-equation premises, the
|
||
signature's R bytes DECOMPRESS to a valid on-curve point Pt, and the
|
||
verifier accepts **iff** Pt equals the recomputed [k]·(−A) + [s]·B:
|
||
|
||
accept ⇔ decompress(R) = [k]·(−A) + [s]·B (as points).
|
||
|
||
This is the constructive capstone of phase 2: byte comparison ↔
|
||
canonical-encoding equality ↔ point equality ↔ decompressed-point
|
||
equality, every link machine-checked over the extracted code. -/
|
||
theorem verify_accepts_iff_decompress
|
||
(key : verifying.VerifyingKey) (msg : Slice Std.U8) (sig : ed25519.Signature)
|
||
(val : signature.InternalSignature)
|
||
(er : curve25519_dalek.edwards.CompressedEdwardsY)
|
||
(e r1 : Std.Array Std.U8 32#usize)
|
||
(hparse : signature.InternalSignature.Insts.CoreConvertTryFromShared0SignatureError.try_from sig
|
||
= ok (core.result.Result.Ok val))
|
||
(hrec : verifying.recompute_r_sha512 key val msg = ok er)
|
||
(he : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes er = ok e)
|
||
(hr1 : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes val.R = ok r1)
|
||
(hkv : ExtValid key.point) (hkc : OnCurveExt key.point)
|
||
(t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 t23 t24 t25 t26 t27 t28 t29 t30 t31 : Std.U8)
|
||
(hsb : (↑val.s.bytes : List Std.U8) = [t0, t1, t2, t3, t4, t5, t6, t7, t8, t9, t10, t11, t12, t13, t14, t15, t16, t17, t18, t19, t20, t21, t22, t23, t24, t25, t26, t27, t28, t29, t30, t31])
|
||
(Vs : ℕ) (hVs : Vs = t0.val + t1.val * 2^8 + t2.val * 2^16 + t3.val * 2^24 + t4.val * 2^32 + t5.val * 2^40 + t6.val * 2^48 + t7.val * 2^56 + t8.val * 2^64 + t9.val * 2^72 + t10.val * 2^80 + t11.val * 2^88 + t12.val * 2^96 + t13.val * 2^104 + t14.val * 2^112 + t15.val * 2^120 + t16.val * 2^128 + t17.val * 2^136 + t18.val * 2^144 + t19.val * 2^152 + t20.val * 2^160 + t21.val * 2^168 + t22.val * 2^176 + t23.val * 2^184 + t24.val * 2^192 + t25.val * 2^200 + t26.val * 2^208 + t27.val * 2^216 + t28.val * 2^224 + t29.val * 2^232 + t30.val * 2^240 + t31.val * 2^248)
|
||
(hVslt : Vs < 2^253)
|
||
(Q : EdPoint) (hQv : ExtValid Q) (hQc : OnCurveExt Q)
|
||
(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)
|
||
(hbl : (↑r1 : 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])
|
||
(henc : bytesVal r1 = (edY Q).val + ((edX Q).val % 2) * 2^255) :
|
||
∃ (R' Pt : EdPoint), ExtValid R' ∧ OnCurveExt R' ∧
|
||
curve25519_dalek.edwards.CompressedEdwardsY.decompress r1 = ok (some Pt) ∧
|
||
ExtValid Pt ∧ OnCurveExt Pt ∧
|
||
(verifying.verify_sha512 key msg sig = ok (core.result.Result.Ok ())
|
||
↔ edPt Pt = edPt R') := by
|
||
obtain ⟨R', hRv, hRc, hiff⟩ := verify_accepts_iff_point_eq key msg sig val er e r1
|
||
hparse hrec he hr1 hkv hkc
|
||
t0 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 t16 t17 t18 t19 t20 t21 t22 t23 t24 t25 t26 t27 t28 t29 t30 t31 hsb Vs hVs hVslt Q hQv hQc henc
|
||
obtain ⟨o, ho, Pt, hosome, hPv, hPc, hPQ⟩ := spec_imp_exists
|
||
(decompress_of_canonical Q hQv hQc r1 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 hbl henc)
|
||
refine ⟨R', Pt, hRv, hRc, ?_, hPv, hPc, ?_⟩
|
||
· rw [ho, hosome]
|
||
· rw [hiff, hPQ]
|
||
|
||
end CurveFieldProofs
|