saymrwulf/betrusted-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/betrusted-ed25519-verified.git synced 2026-09-03 20:13:47 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

PHASE-2 HALF-LIFT on the betrusted fork: verify_accepts_iff_point, button-enforced

Browse source 
Verbatim port of the risc0 fork's phase-2 files (identical v4 shape:
as_bytes serializers, inlined affine conversion, single sha512_hash3
oracle bind) - every proof compiled unchanged. verify_accepts_iff_point:
accept IFF the signature's R bytes are the canonical encoding of the
recomputed [k](-A) + [s]B over the certified model. Five new standard
certificates; Phase 3b enforces the hash3 + wire-format boundary on both
apex and half-lift. Full button green fresh.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-05 16:57:57 +02:00
parent 0ac1ad066a
commit 81f6590670
6 changed files with 2185 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

201
verification/Proofs/CompressSpec.lean Normal file
View file

@ -0,0 +1,201 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/CompressSpec.lean — phase 2, brick 1: `EdwardsPoint::compress` emits
the canonical wire encoding of the denoted affine point.
THE THEOREM (`ed_compress_spec`): for a valid extended point Pt,
compress Pt = ok s with
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) · 2²⁵⁵
— the 32 bytes are the canonical little-endian encoding of the affine
y-coordinate with the parity ("sign") bit of the affine x-coordinate in
bit 255. Combined with `verify_accepts_iff` (SigApexSpec), this pins the
byte comparison of the apex to an equation on DENOTED POINTS — the
half-lift toward the point-level verification equation.
CHAIN (all real extracted code, all previously certified):
to_affine = invert Z, mul X, mul Y (invert_spec, mul_spec')
compress = to_bytes y (to_bytes_spec — canonicity)
is_negative x (to_bytes again, bit 0)
s[31] ^= sign << 7 (XOR on a clear bit = +2²⁵⁵)
The parity of the CANONICAL encoding is the standard "sign" convention:
is_negative reads bit 0 of to_bytes, i.e. (feVal x mod p) mod 2 =
(edX Pt).val mod 2.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.ToBytesSpec
import Proofs.InvertSpec
import Proofs.EdMain
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
/-- Premise-free restatement of `to_bytes_spec` (destructures internally). -/
theorem to_bytes_spec' (a : Fe) :
fe_to_bytes a ⦃ s => bytesVal s = feVal a % P ⦄ := by
obtain ⟨l0, l1, l2, l3, l4, hl⟩ := Fe.exists_limbs a
exact to_bytes_spec a l0 l1 l2 l3 l4 hl
/-- Destructuring device for 32-byte arrays (the `Fe.exists_limbs` idiom). -/
theorem Bytes32.exists_bytes (s : 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,
(↑s : 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] := by
have h : (↑s : List Std.U8).length = 32 := by
have := s.property
simp_all
match hl : (↑s : List Std.U8) with
| [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15,
c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31] =>
exact ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15,
c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, rfl⟩
| [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_ => simp [hl] at h
/-- **`is_negative` is the parity of the canonical residue** — bit 0 of the
canonical encoding (`Choice` is the transparent-u8 model). -/
theorem is_negative_spec (a : Fe) :
field.FieldElement51.is_negative a ⦃ c => c.val = (feVal a % P) % 2 ⦄ := by
unfold field.FieldElement51.is_negative
step with (to_bytes_spec' a) as ⟨s, hs⟩
obtain ⟨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,
hsl⟩ := Bytes32.exists_bytes s
step as ⟨i, hi⟩
simp [hsl] at hi
step as ⟨i1, hi1⟩
-- into Choice = the identity From instance
simp only [core.convert.IntoFrom.into, subtle.Choice.Insts.CoreConvertFromU8,
subtle.Choice.Insts.CoreConvertFromU8.from]
try simp only [spec_ok]
-- value: b0 &&& 1 = b0 % 2 = bytesVal s % 2 = (feVal a % P) % 2
have hi1v : i1.val = b0.val % 2 := by
rw [hi1, hi, UScalar.val_and]
have := Nat.and_two_pow_sub_one_eq_mod b0.val 1
norm_num at this
simpa using this
have hb0 : b0.val % 2 = bytesVal s % 2 := by
simp only [bytesVal, hsl]
omega
rw [hi1v, hb0, hs]
/-- **`compress` on a valid extended point emits the canonical encoding**:
the affine y-residue with the x-parity bit at position 255. -/
theorem ed_compress_spec (Pt : EdPoint) (hv : ExtValid Pt) :
edwards.EdwardsPoint.compress Pt ⦃ s =>
bytesVal s = (edY Pt).val + ((edX Pt).val % 2) * 2^255 ⦄ := by
obtain ⟨hbX, hbY, hbZ, hZne, hcoh⟩ := hv
unfold edwards.EdwardsPoint.compress
-- recip ← invert Z
step with (invert_spec Pt.Z (Bnd.mono hbZ (by norm_num))) as ⟨recip, hbr, hrv⟩
-- x ← X · recip, y ← Y · recip
step with (mul_spec' Pt.X recip (Bnd.mono hbX (by norm_num)) (Bnd.mono hbr (by norm_num)))
as ⟨x, hbx, hxv⟩
step with (mul_spec' Pt.Y recip (Bnd.mono hbY (by norm_num)) (Bnd.mono hbr (by norm_num)))
as ⟨y, hby, hyv⟩
-- (v4: the affine conversion is inlined in compress)
step with (to_bytes_spec' y) as ⟨s, hs⟩
obtain ⟨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,
hsl⟩ := Bytes32.exists_bytes s
step with (is_negative_spec x) as ⟨c, hc⟩
-- unwrap_u8 is the transparent-u8 identity: reduce it away
simp only [subtle.Choice.unwrap_u8, bind_tc_ok]
have hsignv : c.val = (feVal x % P) % 2 := hc
-- sign << 7
step as ⟨hi7, hhi7⟩
have hsle : c.val ≤ 1 := by rw [hsignv]; omega
have hhi7v : hi7.val = c.val * 2^7 := by
rw [hhi7]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show c.val * 2^7 < U8.size by scalar_tac)]
-- s[31]
step as ⟨t31, ht31⟩
simp [hsl] at ht31
-- xor
step as ⟨t31x, ht31x⟩
-- update
step as ⟨s1, hs1⟩
have hsl1 : (↑s1 : 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, t31x] := by
simp only [hs1, Array.set_val_eq, hsl]
rfl
try simp only [spec_ok]
-- ── value assembly ───────────────────────────────────────────────────────
-- the canonical y-residue is < p < 2²⁵⁵, so its top byte is < 2⁷
have hsval : bytesVal s = feVal y % P := hs
have hslt : bytesVal s < 2^255 := by
rw [hsval]
have : feVal y % P < P := Nat.mod_lt _ (by unfold P; norm_num)
unfold P at this ⊢
omega
have hb31top : b31.val < 2^7 := by
have hexp : bytesVal s = 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, hsl]
omega
-- the xor adds sign·2⁷ to a clear bit
have ht31xv : t31x.val = b31.val + c.val * 2^7 := by
have hsb : c.val = 0 ∨ c.val = 1 := by
rw [hsignv]; omega
rw [ht31x, UScalar.val_xor, ht31, hhi7v]
rcases hsb with h | h
· simp [h]
· rw [h]
norm_num
exact xor_top_bit b31.val hb31top
-- reassemble: only byte 31 changed, and it grew by sign·2⁷ at weight 2²⁴⁸
have hexp : bytesVal s = 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, hsl]
have hexp1 : bytesVal s1 = 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 + t31x.val * 2^248 := by
simp only [bytesVal, hsl1]
have hstep : bytesVal s1 = bytesVal s + c.val * 2^255 := by
rw [hexp, hexp1, ht31xv]
ring
-- denotation bridges: the residues are the .val of the denoted coordinates
haveI : NeZero P := ⟨by unfold P; norm_num⟩
have hyval : feVal y % P = (edY Pt).val := by
have h1 : ⟪y⟫ = edY Pt := by
rw [hyv, hrv]
unfold edY
rw [div_eq_mul_inv]
rw [← h1]
simp [denote, ZMod.val_natCast]
have hxval : (feVal x % P) % 2 = (edX Pt).val % 2 := by
have h1 : ⟪x⟫ = edX Pt := by
rw [hxv, hrv]
unfold edX
rw [div_eq_mul_inv]
rw [← h1]
simp [denote, ZMod.val_natCast]
rw [hstep, hs, hsignv, hyval, hxval]
end CurveFieldProofs

321
verification/Proofs/PointLiftSpec.lean Normal file
View file

@ -0,0 +1,321 @@
/- ──────────────────────────────────────────────────────────────────────────────
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)
/-- List-level 32-destructure (helper for the 64-byte device). -/
theorem List.exists_len32 (l : List Std.U8) (h : l.length = 32) :
∃ (d0 d1 d2 d3 d4 d5 d6 d7 d8 d9 d10 d11 d12 d13 d14 d15 d16 d17 d18 d19 d20 d21 d22 d23 d24 d25 d26 d27 d28 d29 d30 d31 : Std.U8), l = [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31] := by
match hl : l with
| [d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31] => exact ⟨d0, d1, d2, d3, d4, d5, d6, d7, d8, d9, d10, d11, d12, d13, d14, d15, d16, d17, d18, d19, d20, d21, d22, d23, d24, d25, d26, d27, d28, d29, d30, d31, rfl⟩
| [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| _::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_::_ => simp [hl] at h
/-- Destructuring device for 64-byte arrays (hash outputs): 32-cons prefix,
then the list-level device on the tail. -/
theorem Bytes64.exists_bytes (s : Std.Array Std.U8 64#usize) :
∃ (c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 c25 c26 c27 c28 c29 c30 c31 c32 c33 c34 c35 c36 c37 c38 c39 c40 c41 c42 c43 c44 c45 c46 c47 c48 c49 c50 c51 c52 c53 c54 c55 c56 c57 c58 c59 c60 c61 c62 c63 : Std.U8),
(↑s : List Std.U8) = [c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63] := by
have h : (↑s : List Std.U8).length = 64 := by
have := s.property
simp_all
match hl : (↑s : List Std.U8) with
| c0 :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: c9 :: c10 :: c11 :: c12 :: c13 :: c14 :: c15 :: c16 :: c17 :: c18 :: c19 :: c20 :: c21 :: c22 :: c23 :: c24 :: c25 :: c26 :: c27 :: c28 :: c29 :: c30 :: c31 :: rest =>
have h2 : rest.length = 32 := by
rw [hl] at h
simp at h
omega
obtain ⟨c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, hr⟩ := List.exists_len32 rest h2
exact ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, by rw [hr]⟩
| [] | [_] | [_,_] | [_,_,_] | [_,_,_,_] | [_,_,_,_,_] | [_,_,_,_,_,_] | [_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
| [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] | [_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_,_] => simp [hl] at h
/-- Generic ok-inversion of one monadic bind: a successful chain names the
intermediate and its defining equation. -/
theorem bind_ok_inv {α β : Type} {e : Result α} {f : α → Result β} {b : β}
(h : (do let x ← e; f x) = ok b) : ∃ a, e = ok a ∧ f a = ok b := by
cases he : e with
| ok v =>
refine ⟨v, rfl, ?_⟩
rw [he] at h
simpa using h
| fail err =>
rw [he] at h
simp [Bind.bind, Aeneas.Std.bind] at h
| div =>
rw [he] at h
simp [Bind.bind, Aeneas.Std.bind] at h
open ed25519_dalek in
/-- **Inversion of the recompute chain**: a successful recompute names its
intermediates — the hash output, the reduced scalar k, the negated key
point, and the dsm result — each with its defining equation. (The SHA
calls are oracles: axioms cannot be walked, so the chain is inverted
from the hypothesis, mirroring the apex's hypothesis-parametric form.) -/
theorem recompute_inv (key : verifying.VerifyingKey)
(sig : signature.InternalSignature) (msg : Slice Std.U8)
(er : curve25519_dalek.edwards.CompressedEdwardsY)
(hrec : verifying.recompute_r_sha512 key sig msg = ok er) :
∃ (hash : Std.Array Std.U8 64#usize) (k : scalar.Scalar)
(mA ep : EdPoint),
scalar.Scalar.from_bytes_mod_order_wide hash = ok k ∧
edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg key.point = ok mA ∧
edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint k mA sig.s = ok ep ∧
edwards.EdwardsPoint.compress ep = ok er := by
unfold verifying.recompute_r_sha512 at hrec
simp only [curve25519_dalek.edwards.CompressedEdwardsY.as_bytes, lift,
bind_tc_ok] at hrec
obtain ⟨hash, _, hrec⟩ := bind_ok_inv hrec
obtain ⟨k, hk, hrec⟩ := bind_ok_inv hrec
obtain ⟨mA, hmA, hrec⟩ := bind_ok_inv hrec
obtain ⟨ep, hep, hrec⟩ := bind_ok_inv hrec
exact ⟨hash, k, mA, ep, hk, hmA, hep, hrec⟩
open ed25519_dalek in
/-- **THE HALF-LIFT: the verifier accepts iff the signature's R bytes are
the canonical encoding of the recomputed point.** For a parsing
signature (`hparse`), a valid on-curve public-key point, a canonical
signature scalar, and a successful recompute (`hrec` — the SHA calls
are oracles, hence hypothesis-parametric like the apex itself), there
is a point R' — [k](−A) + [s]B over the certified model — with
accept ⇔ bytesVal R_bytes = (edY R').val + ((edX R').val % 2)·2²⁵⁵.
The byte-for-byte comparison of the apex IS point-encoding equality. -/
theorem verify_accepts_iff_point
(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) :
∃ (R' : EdPoint), ExtValid R' ∧ OnCurveExt R' ∧
(verifying.verify_sha512 key msg sig = ok (core.result.Result.Ok ())
↔ bytesVal r1 = (edY R').val + ((edX R').val % 2) * 2^255) := by
obtain ⟨hash, k, mA, ep, hk, hmA, hep, hcomp⟩ := recompute_inv key val msg er hrec
-- k is canonical (< ℓ < 2²⁵³)
obtain ⟨c0, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, hhl⟩ := Bytes64.exists_bytes hash
obtain ⟨k', hk', hkpost⟩ := spec_imp_exists
(ScalarProofs.from_bytes_mod_order_wide_spec hash c0 c1 c2 c3 c4 c5 c6 c7 c8 c9 c10 c11 c12 c13 c14 c15 c16 c17 c18 c19 c20 c21 c22 c23 c24 c25 c26 c27 c28 c29 c30 c31 c32 c33 c34 c35 c36 c37 c38 c39 c40 c41 c42 c43 c44 c45 c46 c47 c48 c49 c50 c51 c52 c53 c54 c55 c56 c57 c58 c59 c60 c61 c62 c63 hhl _ rfl)
rw [hk] at hk'
have hkk : k = k' := by simpa using hk'
subst hkk
obtain ⟨hklt, -⟩ := hkpost
obtain ⟨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, hkbl⟩ := Bytes32.exists_bytes k.bytes
have hkval : bytesVal k.bytes = 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 := by
simp only [bytesVal, hkbl]
have hValt : (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) < 2^253 := by
have hEll : ScalarProofs.Ell < 2^253 := by unfold ScalarProofs.Ell; norm_num
omega
-- mA = −A, valid and on-curve
unfold edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg at hmA
obtain ⟨mA', hmA', hmApost⟩ := spec_imp_exists (edwards_neg_law key.point hkv hkc)
rw [hmA'] at hmA
have hmm : mA = mA' := by simpa using hmA.symm
subst hmm
obtain ⟨hmAv, hmAc, -⟩ := hmApost
-- ep = [k](−A) + [s]B, valid and on-curve
obtain ⟨ep', hep', heppost⟩ := spec_imp_exists
(vartime_dsm_basepoint_spec k val.s mA
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 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
hkbl hsb _ Vs rfl hVs hValt hVslt hmAv hmAc)
rw [hep'] at hep
have hee' : ep = ep' := by simpa using hep.symm
subst hee'
obtain ⟨hepv, hepc, -⟩ := heppost
-- er is the canonical encoding of ep
obtain ⟨er2, hcomp', hcpost⟩ := spec_imp_exists (ed_compress_spec ep hepv)
rw [hcomp'] at hcomp
have her : er = er2 := by simpa using hcomp.symm
subst her
-- e IS er (as_bytes is the identity)
have hee : er = e := by
have : curve25519_dalek.edwards.CompressedEdwardsY.as_bytes er = ok er := by
simp [curve25519_dalek.edwards.CompressedEdwardsY.as_bytes]
rw [this] at he
simpa using he
refine ⟨ep, hepv, hepc, ?_⟩
rw [verify_accepts_iff key msg sig val er e r1 hparse hrec he hr1,
rangeEq_iff_bytesVal, ← hee, hcpost]
exact eq_comm
end CurveFieldProofs

599
verification/Proofs/ScalarPackSpec.lean Normal file
View file

@ -0,0 +1,599 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/ScalarPackSpec.lean — phase 2, half-lift prerequisite: the scalar
PACK step (`Scalar52::to_bytes` / `Scalar52::pack`) and the composed
`Scalar::from_bytes_mod_order_wide` — the hash-to-scalar entry the
verifier's recompute path calls.
`Scalar52::to_bytes` is pure bit-packing (radix 2⁵² → little-endian bytes,
NO reduction — its callers guarantee canonical limbs): 30 shift-extracts
plus 2 limb-boundary bytes (6, 19 — the only offsets where 52j is not
byte-aligned). `scalar_pack` (the ℕ identity) mirrors ToBytesMath's
bytes_pack at the 52-bit offsets; the boundary ORs become additions via
the same disjointness idiom.
THE COMPOSED SPEC (`from_bytes_mod_order_wide_spec`): for a 64-byte input
with value T, the returned Scalar's 32 bytes have value V with
V < ℓ and (V : ZMod ℓ) = T
— i.e. the verifier's k = SHA-512 output reduced mod ℓ, in EXACTLY the
byte-value form the dsm certificate (`vartime_double_base_mul_spec`)
takes as its scalar premises (V < ℓ < 2²⁵³).
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.ToBytesSpec
import Proofs.ScalarFromBytesSpec
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 8000000
set_option linter.unusedSimpArgs false
set_option maxRecDepth 8000
namespace ScalarProofs
open Aeneas.Std.WP
open CurveFieldProofs (bytesVal nat_shr byte_split_0 xor_top_bit)
/-- Offset-4 byte split for 52-bit limbs (the pack's odd-offset limbs 1, 3):
low 4 bits close the boundary byte, six whole bytes follow. -/
theorem byte_split_52_4 (f : ℕ) :
f % 2^4 + (f / 2^4 % 2^8) * 2^4 + (f / 2^12 % 2^8) * 2^12
+ (f / 2^20 % 2^8) * 2^20 + (f / 2^28 % 2^8) * 2^28
+ (f / 2^36 % 2^8) * 2^36 + (f / 2^44) * 2^44 = f := by
have e1 : f / 2^4 / 2^8 = f / 2^12 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^12 / 2^8 = f / 2^20 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^20 / 2^8 = f / 2^28 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^28 / 2^8 = f / 2^36 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^36 / 2^8 = f / 2^44 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^4)
have d1 := Nat.div_add_mod (f / 2^4) (2^8)
have d2 := Nat.div_add_mod (f / 2^12) (2^8)
have d3 := Nat.div_add_mod (f / 2^20) (2^8)
have d4 := Nat.div_add_mod (f / 2^28) (2^8)
have d5 := Nat.div_add_mod (f / 2^36) (2^8)
omega
/-- THE 52-BIT PACKING IDENTITY: the 32 bytes `Scalar52::to_bytes` emits
assemble to the limb value (boundary bytes 6 and 19 in additive form). -/
theorem scalar_pack (l0 l1 l2 l3 l4 : ℕ)
(h0 : l0 < 2^52) (h1 : l1 < 2^52) (h2 : l2 < 2^52)
(h3 : l3 < 2^52) (h4 : l4 < 2^48) :
(l0 % 2^8)
+ (l0 / 2^8 % 2^8) * 2^8
+ (l0 / 2^16 % 2^8) * 2^16
+ (l0 / 2^24 % 2^8) * 2^24
+ (l0 / 2^32 % 2^8) * 2^32
+ (l0 / 2^40 % 2^8) * 2^40
+ (l0 / 2^48 + (l1 % 2^4) * 2^4) * 2^48
+ (l1 / 2^4 % 2^8) * 2^56
+ (l1 / 2^12 % 2^8) * 2^64
+ (l1 / 2^20 % 2^8) * 2^72
+ (l1 / 2^28 % 2^8) * 2^80
+ (l1 / 2^36 % 2^8) * 2^88
+ (l1 / 2^44 % 2^8) * 2^96
+ (l2 % 2^8) * 2^104
+ (l2 / 2^8 % 2^8) * 2^112
+ (l2 / 2^16 % 2^8) * 2^120
+ (l2 / 2^24 % 2^8) * 2^128
+ (l2 / 2^32 % 2^8) * 2^136
+ (l2 / 2^40 % 2^8) * 2^144
+ (l2 / 2^48 + (l3 % 2^4) * 2^4) * 2^152
+ (l3 / 2^4 % 2^8) * 2^160
+ (l3 / 2^12 % 2^8) * 2^168
+ (l3 / 2^20 % 2^8) * 2^176
+ (l3 / 2^28 % 2^8) * 2^184
+ (l3 / 2^36 % 2^8) * 2^192
+ (l3 / 2^44 % 2^8) * 2^200
+ (l4 % 2^8) * 2^208
+ (l4 / 2^8 % 2^8) * 2^216
+ (l4 / 2^16 % 2^8) * 2^224
+ (l4 / 2^24 % 2^8) * 2^232
+ (l4 / 2^32 % 2^8) * 2^240
+ (l4 / 2^40) * 2^248
= l0 + l1 * 2^52 + l2 * 2^104 + l3 * 2^156 + l4 * 2^208 := by
have s0 := byte_split_0 l0
have s1 := byte_split_52_4 l1
have s2 := byte_split_0 l2
have s3 := byte_split_52_4 l3
-- limb 4 has only 6 bytes: split_0's seventh chunk vanishes (l4 < 2^48)
have s4 := byte_split_0 l4
have h4z : l4 / 2^48 = 0 := Nat.div_eq_of_lt h4
-- l1/2^44, l3/2^44, l4/2^40 all fit a byte: the mods are the identity
have h1m : l1 / 2^44 % 2^8 = l1 / 2^44 :=
Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l1 < 2^44 * 2^8 by omega))
have h3m : l3 / 2^44 % 2^8 = l3 / 2^44 :=
Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l3 < 2^44 * 2^8 by omega))
have h4m : l4 / 2^40 % 2^8 = l4 / 2^40 :=
Nat.mod_eq_of_lt (Nat.div_lt_of_lt_mul (show l4 < 2^40 * 2^8 by omega))
rw [h1m, h3m]
rw [h4m, h4z] at s4
zify at s0 s1 s2 s3 s4 ⊢
linear_combination s0 + 2^52 * s1 + 2^104 * s2 + 2^156 * s3 + 2^208 * s4
/-- **`Scalar52::to_bytes` is the canonical serializer of canonical limbs**:
for limbs below 2⁵² with value below 2²⁵³ (every reduced scalar), the 32
output bytes denote exactly the limb value. -/
theorem scalar52_to_bytes_spec (a : Sc) (l0 l1 l2 l3 l4 : U64)
(hl : (↑a : List U64) = [l0, l1, l2, l3, l4])
(hb0 : l0.val < 2^52) (hb1 : l1.val < 2^52) (hb2 : l2.val < 2^52)
(hb3 : l3.val < 2^52) (hb4 : l4.val < 2^48) :
backend.serial.u64.scalar.Scalar52.as_bytes a
⦃ s => bytesVal s = scVal a ⦄ := by
unfold backend.serial.u64.scalar.Scalar52.as_bytes
-- limb 0 read
step as ⟨v0, hv0⟩
simp [hl] at hv0
-- byte 0 (limb 0 >> 0)
step as ⟨x0, hx0⟩
rw [hv0] at hx0
step as ⟨b0, hb0⟩
have hb0v : b0.val = l0.val % 2^8 := by
rw [hb0, UScalar.cast_val_eq, hx0, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s1, hs1⟩
have hsl0 : (↑s1 : List Std.U8) = [b0, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs1, Array.set_val_eq, Array.repeat_val]
rfl
clear hx0 hb0 hs1
-- byte 1 (limb 0 >> 8)
step as ⟨x1, hx1⟩
rw [hv0] at hx1
step as ⟨b1, hb1⟩
have hb1v : b1.val = l0.val / 2^8 % 2^8 := by
rw [hb1, UScalar.cast_val_eq, hx1, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s2, hs2⟩
have hsl1 : (↑s2 : List Std.U8) = [b0, b1, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs2, Array.set_val_eq, hsl0]
rfl
clear hx1 hb1 hs2 hsl0
-- byte 2 (limb 0 >> 16)
step as ⟨x2, hx2⟩
rw [hv0] at hx2
step as ⟨b2, hb2⟩
have hb2v : b2.val = l0.val / 2^16 % 2^8 := by
rw [hb2, UScalar.cast_val_eq, hx2, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s3, hs3⟩
have hsl2 : (↑s3 : List Std.U8) = [b0, b1, b2, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs3, Array.set_val_eq, hsl1]
rfl
clear hx2 hb2 hs3 hsl1
-- byte 3 (limb 0 >> 24)
step as ⟨x3, hx3⟩
rw [hv0] at hx3
step as ⟨b3, hb3⟩
have hb3v : b3.val = l0.val / 2^24 % 2^8 := by
rw [hb3, UScalar.cast_val_eq, hx3, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s4, hs4⟩
have hsl3 : (↑s4 : List Std.U8) = [b0, b1, b2, b3, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs4, Array.set_val_eq, hsl2]
rfl
clear hx3 hb3 hs4 hsl2
-- byte 4 (limb 0 >> 32)
step as ⟨x4, hx4⟩
rw [hv0] at hx4
step as ⟨b4, hb4⟩
have hb4v : b4.val = l0.val / 2^32 % 2^8 := by
rw [hb4, UScalar.cast_val_eq, hx4, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s5, hs5⟩
have hsl4 : (↑s5 : List Std.U8) = [b0, b1, b2, b3, b4, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs5, Array.set_val_eq, hsl3]
rfl
clear hx4 hb4 hs5 hsl3
-- byte 5 (limb 0 >> 40)
step as ⟨x5, hx5⟩
rw [hv0] at hx5
step as ⟨b5, hb5⟩
have hb5v : b5.val = l0.val / 2^40 % 2^8 := by
rw [hb5, UScalar.cast_val_eq, hx5, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s6, hs6⟩
have hsl5 : (↑s6 : List Std.U8) = [b0, b1, b2, b3, b4, b5, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs6, Array.set_val_eq, hsl4]
rfl
clear hx5 hb5 hs6 hsl4
-- byte 6 (boundary: limb 0 >> 48 | limb 1 << 4)
step as ⟨x6, hx6⟩
rw [hv0] at hx6
step as ⟨v1, hv1⟩
simp [hl] at hv1
step as ⟨y6, hy6⟩
rw [hv1] at hy6
have hy6v : y6.val = l1.val * 2^4 := by
rw [hy6]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show l1.val * 2^4 < U64.size by scalar_tac)]
step as ⟨z6, hz6⟩
step as ⟨b6, hb6⟩
have hb6v : b6.val = l0.val / 2^48 + (l1.val % 2^4) * 2^4 := by
rw [hb6, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz6, UScalar.val_or, hx6, nat_shr, hy6v]
have hxlt : l0.val / 2^48 < 2^4 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := l0.val / 2^48) (i := 4) hxlt (l1.val)
have hadd : l0.val / 2^48 ||| l1.val * 2^4 = l0.val / 2^48 + l1.val * 2^4 := by
calc l0.val / 2^48 ||| l1.val * 2^4
= l0.val / 2^48 ||| 2^4 * l1.val := by rw [Nat.mul_comm]
_ = 2^4 * l1.val ||| l0.val / 2^48 := Nat.lor_comm _ _
_ = 2^4 * l1.val + l0.val / 2^48 := hor.symm
_ = l0.val / 2^48 + l1.val * 2^4 := by ring
rw [hadd]
omega
step as ⟨s7, hs7⟩
have hsl6 : (↑s7 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs7, Array.set_val_eq, hsl5]
rfl
clear hx6 hy6 hy6v hz6 hb6 hs7 hsl5
-- byte 7 (limb 1 >> 4)
step as ⟨x7, hx7⟩
rw [hv1] at hx7
step as ⟨b7, hb7⟩
have hb7v : b7.val = l1.val / 2^4 % 2^8 := by
rw [hb7, UScalar.cast_val_eq, hx7, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s8, hs8⟩
have hsl7 : (↑s8 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs8, Array.set_val_eq, hsl6]
rfl
clear hx7 hb7 hs8 hsl6
-- byte 8 (limb 1 >> 12)
step as ⟨x8, hx8⟩
rw [hv1] at hx8
step as ⟨b8, hb8⟩
have hb8v : b8.val = l1.val / 2^12 % 2^8 := by
rw [hb8, UScalar.cast_val_eq, hx8, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s9, hs9⟩
have hsl8 : (↑s9 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs9, Array.set_val_eq, hsl7]
rfl
clear hx8 hb8 hs9 hsl7
-- byte 9 (limb 1 >> 20)
step as ⟨x9, hx9⟩
rw [hv1] at hx9
step as ⟨b9, hb9⟩
have hb9v : b9.val = l1.val / 2^20 % 2^8 := by
rw [hb9, UScalar.cast_val_eq, hx9, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s10, hs10⟩
have hsl9 : (↑s10 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs10, Array.set_val_eq, hsl8]
rfl
clear hx9 hb9 hs10 hsl8
-- byte 10 (limb 1 >> 28)
step as ⟨x10, hx10⟩
rw [hv1] at hx10
step as ⟨b10, hb10⟩
have hb10v : b10.val = l1.val / 2^28 % 2^8 := by
rw [hb10, UScalar.cast_val_eq, hx10, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s11, hs11⟩
have hsl10 : (↑s11 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs11, Array.set_val_eq, hsl9]
rfl
clear hx10 hb10 hs11 hsl9
-- byte 11 (limb 1 >> 36)
step as ⟨x11, hx11⟩
rw [hv1] at hx11
step as ⟨b11, hb11⟩
have hb11v : b11.val = l1.val / 2^36 % 2^8 := by
rw [hb11, UScalar.cast_val_eq, hx11, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s12, hs12⟩
have hsl11 : (↑s12 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs12, Array.set_val_eq, hsl10]
rfl
clear hx11 hb11 hs12 hsl10
-- byte 12 (limb 1 >> 44)
step as ⟨x12, hx12⟩
rw [hv1] at hx12
step as ⟨b12, hb12⟩
have hb12v : b12.val = l1.val / 2^44 % 2^8 := by
rw [hb12, UScalar.cast_val_eq, hx12, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s13, hs13⟩
have hsl12 : (↑s13 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs13, Array.set_val_eq, hsl11]
rfl
clear hx12 hb12 hs13 hsl11
-- limb 2 read
step as ⟨v2, hv2⟩
simp [hl] at hv2
-- byte 13 (limb 2 >> 0)
step as ⟨x13, hx13⟩
rw [hv2] at hx13
step as ⟨b13, hb13⟩
have hb13v : b13.val = l2.val % 2^8 := by
rw [hb13, UScalar.cast_val_eq, hx13, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s14, hs14⟩
have hsl13 : (↑s14 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs14, Array.set_val_eq, hsl12]
rfl
clear hx13 hb13 hs14 hsl12
-- byte 14 (limb 2 >> 8)
step as ⟨x14, hx14⟩
rw [hv2] at hx14
step as ⟨b14, hb14⟩
have hb14v : b14.val = l2.val / 2^8 % 2^8 := by
rw [hb14, UScalar.cast_val_eq, hx14, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s15, hs15⟩
have hsl14 : (↑s15 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs15, Array.set_val_eq, hsl13]
rfl
clear hx14 hb14 hs15 hsl13
-- byte 15 (limb 2 >> 16)
step as ⟨x15, hx15⟩
rw [hv2] at hx15
step as ⟨b15, hb15⟩
have hb15v : b15.val = l2.val / 2^16 % 2^8 := by
rw [hb15, UScalar.cast_val_eq, hx15, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s16, hs16⟩
have hsl15 : (↑s16 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs16, Array.set_val_eq, hsl14]
rfl
clear hx15 hb15 hs16 hsl14
-- byte 16 (limb 2 >> 24)
step as ⟨x16, hx16⟩
rw [hv2] at hx16
step as ⟨b16, hb16⟩
have hb16v : b16.val = l2.val / 2^24 % 2^8 := by
rw [hb16, UScalar.cast_val_eq, hx16, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s17, hs17⟩
have hsl16 : (↑s17 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs17, Array.set_val_eq, hsl15]
rfl
clear hx16 hb16 hs17 hsl15
-- byte 17 (limb 2 >> 32)
step as ⟨x17, hx17⟩
rw [hv2] at hx17
step as ⟨b17, hb17⟩
have hb17v : b17.val = l2.val / 2^32 % 2^8 := by
rw [hb17, UScalar.cast_val_eq, hx17, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s18, hs18⟩
have hsl17 : (↑s18 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs18, Array.set_val_eq, hsl16]
rfl
clear hx17 hb17 hs18 hsl16
-- byte 18 (limb 2 >> 40)
step as ⟨x18, hx18⟩
rw [hv2] at hx18
step as ⟨b18, hb18⟩
have hb18v : b18.val = l2.val / 2^40 % 2^8 := by
rw [hb18, UScalar.cast_val_eq, hx18, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s19, hs19⟩
have hsl18 : (↑s19 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs19, Array.set_val_eq, hsl17]
rfl
clear hx18 hb18 hs19 hsl17
-- byte 19 (boundary: limb 2 >> 48 | limb 3 << 4)
step as ⟨x19, hx19⟩
rw [hv2] at hx19
step as ⟨v3, hv3⟩
simp [hl] at hv3
step as ⟨y19, hy19⟩
rw [hv3] at hy19
have hy19v : y19.val = l3.val * 2^4 := by
rw [hy19]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show l3.val * 2^4 < U64.size by scalar_tac)]
step as ⟨z19, hz19⟩
step as ⟨b19, hb19⟩
have hb19v : b19.val = l2.val / 2^48 + (l3.val % 2^4) * 2^4 := by
rw [hb19, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz19, UScalar.val_or, hx19, nat_shr, hy19v]
have hxlt : l2.val / 2^48 < 2^4 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := l2.val / 2^48) (i := 4) hxlt (l3.val)
have hadd : l2.val / 2^48 ||| l3.val * 2^4 = l2.val / 2^48 + l3.val * 2^4 := by
calc l2.val / 2^48 ||| l3.val * 2^4
= l2.val / 2^48 ||| 2^4 * l3.val := by rw [Nat.mul_comm]
_ = 2^4 * l3.val ||| l2.val / 2^48 := Nat.lor_comm _ _
_ = 2^4 * l3.val + l2.val / 2^48 := hor.symm
_ = l2.val / 2^48 + l3.val * 2^4 := by ring
rw [hadd]
omega
step as ⟨s20, hs20⟩
have hsl19 : (↑s20 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs20, Array.set_val_eq, hsl18]
rfl
clear hx19 hy19 hy19v hz19 hb19 hs20 hsl18
-- byte 20 (limb 3 >> 4)
step as ⟨x20, hx20⟩
rw [hv3] at hx20
step as ⟨b20, hb20⟩
have hb20v : b20.val = l3.val / 2^4 % 2^8 := by
rw [hb20, UScalar.cast_val_eq, hx20, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s21, hs21⟩
have hsl20 : (↑s21 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs21, Array.set_val_eq, hsl19]
rfl
clear hx20 hb20 hs21 hsl19
-- byte 21 (limb 3 >> 12)
step as ⟨x21, hx21⟩
rw [hv3] at hx21
step as ⟨b21, hb21⟩
have hb21v : b21.val = l3.val / 2^12 % 2^8 := by
rw [hb21, UScalar.cast_val_eq, hx21, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s22, hs22⟩
have hsl21 : (↑s22 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs22, Array.set_val_eq, hsl20]
rfl
clear hx21 hb21 hs22 hsl20
-- byte 22 (limb 3 >> 20)
step as ⟨x22, hx22⟩
rw [hv3] at hx22
step as ⟨b22, hb22⟩
have hb22v : b22.val = l3.val / 2^20 % 2^8 := by
rw [hb22, UScalar.cast_val_eq, hx22, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s23, hs23⟩
have hsl22 : (↑s23 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs23, Array.set_val_eq, hsl21]
rfl
clear hx22 hb22 hs23 hsl21
-- byte 23 (limb 3 >> 28)
step as ⟨x23, hx23⟩
rw [hv3] at hx23
step as ⟨b23, hb23⟩
have hb23v : b23.val = l3.val / 2^28 % 2^8 := by
rw [hb23, UScalar.cast_val_eq, hx23, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s24, hs24⟩
have hsl23 : (↑s24 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs24, Array.set_val_eq, hsl22]
rfl
clear hx23 hb23 hs24 hsl22
-- byte 24 (limb 3 >> 36)
step as ⟨x24, hx24⟩
rw [hv3] at hx24
step as ⟨b24, hb24⟩
have hb24v : b24.val = l3.val / 2^36 % 2^8 := by
rw [hb24, UScalar.cast_val_eq, hx24, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s25, hs25⟩
have hsl24 : (↑s25 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs25, Array.set_val_eq, hsl23]
rfl
clear hx24 hb24 hs25 hsl23
-- byte 25 (limb 3 >> 44)
step as ⟨x25, hx25⟩
rw [hv3] at hx25
step as ⟨b25, hb25⟩
have hb25v : b25.val = l3.val / 2^44 % 2^8 := by
rw [hb25, UScalar.cast_val_eq, hx25, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s26, hs26⟩
have hsl25 : (↑s26 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs26, Array.set_val_eq, hsl24]
rfl
clear hx25 hb25 hs26 hsl24
-- limb 4 read
step as ⟨v4, hv4⟩
simp [hl] at hv4
-- byte 26 (limb 4 >> 0)
step as ⟨x26, hx26⟩
rw [hv4] at hx26
step as ⟨b26, hb26⟩
have hb26v : b26.val = l4.val % 2^8 := by
rw [hb26, UScalar.cast_val_eq, hx26, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s27, hs27⟩
have hsl26 : (↑s27 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs27, Array.set_val_eq, hsl25]
rfl
clear hx26 hb26 hs27 hsl25
-- byte 27 (limb 4 >> 8)
step as ⟨x27, hx27⟩
rw [hv4] at hx27
step as ⟨b27, hb27⟩
have hb27v : b27.val = l4.val / 2^8 % 2^8 := by
rw [hb27, UScalar.cast_val_eq, hx27, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s28, hs28⟩
have hsl27 : (↑s28 : 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, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs28, Array.set_val_eq, hsl26]
rfl
clear hx27 hb27 hs28 hsl26
-- byte 28 (limb 4 >> 16)
step as ⟨x28, hx28⟩
rw [hv4] at hx28
step as ⟨b28, hb28⟩
have hb28v : b28.val = l4.val / 2^16 % 2^8 := by
rw [hb28, UScalar.cast_val_eq, hx28, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s29, hs29⟩
have hsl28 : (↑s29 : 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, 0#u8, 0#u8, 0#u8] := by
simp only [hs29, Array.set_val_eq, hsl27]
rfl
clear hx28 hb28 hs29 hsl27
-- byte 29 (limb 4 >> 24)
step as ⟨x29, hx29⟩
rw [hv4] at hx29
step as ⟨b29, hb29⟩
have hb29v : b29.val = l4.val / 2^24 % 2^8 := by
rw [hb29, UScalar.cast_val_eq, hx29, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s30, hs30⟩
have hsl29 : (↑s30 : 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, 0#u8, 0#u8] := by
simp only [hs30, Array.set_val_eq, hsl28]
rfl
clear hx29 hb29 hs30 hsl28
-- byte 30 (limb 4 >> 32)
step as ⟨x30, hx30⟩
rw [hv4] at hx30
step as ⟨b30, hb30⟩
have hb30v : b30.val = l4.val / 2^32 % 2^8 := by
rw [hb30, UScalar.cast_val_eq, hx30, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s31, hs31⟩
have hsl30 : (↑s31 : 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, 0#u8] := by
simp only [hs31, Array.set_val_eq, hsl29]
rfl
clear hx30 hb30 hs31 hsl29
-- byte 31 (limb 4 >> 40)
step as ⟨x31, hx31⟩
rw [hv4] at hx31
step as ⟨b31, hb31⟩
have hb31v : b31.val = l4.val / 2^40 := by
rw [hb31, UScalar.cast_val_eq, hx31, nat_shr]
norm_num [UScalarTy.numBits]
omega
step as ⟨s32, hs32⟩
have hsl31 : (↑s32 : 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] := by
simp only [hs32, Array.set_val_eq, hsl30]
rfl
clear hx31 hb31 hs32 hsl30
try simp only [spec_ok]
-- assembly via the 52-bit packing identity
have hsum : bytesVal s32 = l0.val + l1.val * 2^52 + l2.val * 2^104
+ l3.val * 2^156 + l4.val * 2^208 := by
simp only [bytesVal, hsl31]
rw [hb0v, hb1v, hb2v, hb3v, hb4v, hb5v, hb6v, hb7v, hb8v, hb9v, hb10v,
hb11v, hb12v, hb13v, hb14v, hb15v, hb16v, hb17v, hb18v, hb19v, hb20v,
hb21v, hb22v, hb23v, hb24v, hb25v, hb26v, hb27v, hb28v, hb29v, hb30v,
hb31v]
exact scalar_pack l0.val l1.val l2.val l3.val l4.val hb0 hb1 hb2 hb3 hb4
rw [hsum, scVal_eq a l0 l1 l2 l3 l4 hl]
unfold scLimbs
ring
/-- **The hash-to-scalar entry is total and canonical**: for a 64-byte input
of value T, `from_bytes_mod_order_wide` returns a Scalar whose 32 bytes
denote V with V < ℓ and V ≡ T (mod ℓ) — exactly the scalar premises the
dsm certificate consumes. -/
theorem from_bytes_mod_order_wide_spec (input : Std.Array Std.U8 64#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 b32 b33 b34 b35 b36 b37 b38 b39 b40 b41 b42 b43 b44 b45 b46 b47 b48 b49 b50 b51 b52 b53 b54 b55 b56 b57 b58 b59 b60 b61 b62 b63 : Std.U8)
(hb : (↑input : 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, b32, b33, b34, b35, b36, b37, b38, b39, b40, b41, b42, b43, b44, b45, b46, b47, b48, b49, b50, b51, b52, b53, b54, b55, b56, b57, b58, b59, b60, b61, b62, b63])
(T : ℕ) (hT : T = 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 + b32.val * 2^256 + b33.val * 2^264 + b34.val * 2^272 + b35.val * 2^280 + b36.val * 2^288 + b37.val * 2^296 + b38.val * 2^304 + b39.val * 2^312 + b40.val * 2^320 + b41.val * 2^328 + b42.val * 2^336 + b43.val * 2^344 + b44.val * 2^352 + b45.val * 2^360 + b46.val * 2^368 + b47.val * 2^376 + b48.val * 2^384 + b49.val * 2^392 + b50.val * 2^400 + b51.val * 2^408 + b52.val * 2^416 + b53.val * 2^424 + b54.val * 2^432 + b55.val * 2^440 + b56.val * 2^448 + b57.val * 2^456 + b58.val * 2^464 + b59.val * 2^472 + b60.val * 2^480 + b61.val * 2^488 + b62.val * 2^496 + b63.val * 2^504) :
scalar.Scalar.from_bytes_mod_order_wide input
⦃ k => bytesVal k.bytes < Ell ∧ (bytesVal k.bytes : ZMod Ell) = (T : ZMod Ell) ⦄ := by
unfold scalar.Scalar.from_bytes_mod_order_wide scalar.Scalar52.pack
step with (from_bytes_wide_spec input 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 b32 b33 b34 b35 b36 b37 b38 b39 b40 b41 b42 b43 b44 b45 b46 b47 b48 b49 b50 b51 b52 b53 b54 b55 b56 b57 b58 b59 b60 b61 b62 b63 hb T hT)
as ⟨r, hex, hlt, hden⟩
obtain ⟨s0, s1, s2, s3, s4, hrl, hs0, hs1, hs2, hs3, hs4⟩ := hex
-- top-limb tightening: scVal r < ℓ < 2²⁵³ forces s4 < 2⁴⁵ < 2⁴⁸
have hs4' : s4.val < 2^48 := by
have hv := scVal_eq r s0 s1 s2 s3 s4 hrl
have : scVal r < 2^253 := by
have : Ell < 2^253 := by unfold Ell; norm_num
omega
unfold scLimbs at hv
omega
step with (scalar52_to_bytes_spec r s0 s1 s2 s3 s4 hrl hs0 hs1 hs2 hs3 hs4')
as ⟨bytes, hbv⟩
try simp only [spec_ok]
constructor
· simpa [hbv] using hlt
· rw [hbv]
exact hden
end ScalarProofs

281
verification/Proofs/ToBytesMath.lean Normal file
View file

@ -0,0 +1,281 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/ToBytesMath.lean — the pure ℕ mathematics of `FieldElement51::to_bytes`
(phase 2 of the signature apex: compress semantics, brick "to_bytes canonicity").
`to_bytes` canonicalizes a weakly-reduced field element (limbs < 2⁵¹+19·2¹³,
hence value h < 2p) to r = h mod p and serializes r little-endian:
1. THE q-TRICK: q := carry of h + 19 out of bit 255 = (h+19)/2²⁵⁵, computed
limb-wise as a 5-rung carry telescope; q ∈ {0,1}, and q = 1 ↔ h ≥ p
(h ≥ p ↔ h + 19 ≥ 2²⁵⁵). (q_telescope, q_facts)
2. r = (h + 19q) mod 2²⁵⁵ = h mod p — adding 19q and discarding bit 255
subtracts exactly pq. (q_mod_p)
3. The carry chain computing (h + 19q) mod 2²⁵⁵ limb-wise. (carry_pack)
4. The 32-byte little-endian packing: each limb splits into byte chunks
(byte_split_*); their weighted sum reassembles the value. (bytes_pack)
Everything here is context-free ℕ arithmetic (METHOD 4: heavy identities in
isolation, applied once). The symbolic execution of the transpiled code
lives in Proofs/ToBytesSpec.lean, which consumes exactly these lemmas.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.Denote
import Mathlib.Tactic.LinearCombination
open Aeneas Aeneas.Std Result
set_option maxHeartbeats 4000000
namespace CurveFieldProofs
/-- `>>>` on ℕ is division (generic-exponent companion of ReduceSpec's
`nat_shift_div`, which is specialized to 51). -/
theorem nat_shr (n k : ℕ) : n >>> k = n / 2^k :=
Nat.shiftRight_eq_div_pow n k
/-- One rung of a carry telescope: absorbing a floor-quotient into the next
limb and re-dividing is one division at the combined weight. -/
theorem div_rung (a b j k : ℕ) : (a + b / 2^j) / 2^k = (a * 2^j + b) / 2^(j+k) := by
have h1 : (a * 2^j + b) / 2^j = a + b / 2^j := by
rw [Nat.add_comm (a * 2^j) b, Nat.add_mul_div_right _ _ (Nat.two_pow_pos j)]
omega
rw [← h1, Nat.div_div_eq_div_mul, ← pow_add]
/-- THE q-TELESCOPE: the limb-wise 5-rung carry computation equals one
division of the assembled value by 2²⁵⁵. `x` is the (already offset)
limb-0 summand — in `to_bytes`, x = m0 + 19 for the q pass and
x = m0 + 19q for the final carry pass. -/
theorem q_telescope (x m1 m2 m3 m4 : ℕ) :
(m4 + (m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) / 2^51) / 2^51
= (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) / 2^255 := by
have h1 : (m1 + x / 2^51) / 2^51 = (m1 * 2^51 + x) / 2^102 := by
have h := div_rung m1 x 51 51; norm_num at h; exact h
have h2 : (m2 + (m1 * 2^51 + x) / 2^102) / 2^51
= (m2 * 2^102 + (m1 * 2^51 + x)) / 2^153 := by
have h := div_rung m2 (m1 * 2^51 + x) 102 51; norm_num at h; exact h
have h3 : (m3 + (m2 * 2^102 + (m1 * 2^51 + x)) / 2^153) / 2^51
= (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) / 2^204 := by
have h := div_rung m3 (m2 * 2^102 + (m1 * 2^51 + x)) 153 51; norm_num at h; exact h
have h4 : (m4 + (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) / 2^204) / 2^51
= (m4 * 2^204 + (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x)))) / 2^255 := by
have h := div_rung m4 (m3 * 2^153 + (m2 * 2^102 + (m1 * 2^51 + x))) 204 51
norm_num at h; exact h
rw [h1, h2, h3, h4]
congr 1
ring
/-- The q facts: for h < 2p (p = 2²⁵⁵ − 19), the carry q = (h+19)/2²⁵⁵ is a
bit, and it fires exactly when h is not yet canonical. -/
theorem q_facts (h : ℕ) (hh : h < 2 * P) :
(h + 19) / 2^255 ≤ 1 ∧ ((h + 19) / 2^255 = 1 ↔ P ≤ h) := by
unfold P at *
constructor
· omega
· omega
/-- Adding 19q and discarding bit 255 computes h mod p exactly. -/
theorem q_mod_p (h : ℕ) (hh : h < 2 * P) :
(h + 19 * ((h + 19) / 2^255)) % 2^255 = h % P := by
have h1 : (h + 19) / 2^255 ≤ 1 := (q_facts h hh).1
rcases Nat.le_one_iff_eq_zero_or_eq_one.mp h1 with hq | hq <;>
· rw [hq]
unfold P at *
omega
/-- THE CARRY-PACK ACCOUNTING: the masked limbs of the final carry pass
assemble to the value mod 2²⁵⁵. Stated over the *quotient/remainder
forms* the symbolic execution produces:
t₀ = x, t_{i+1} = m_{i+1} + t_i / 2⁵¹, f_i = t_i mod 2⁵¹. -/
theorem carry_pack (x m1 m2 m3 m4 : ℕ) :
(x % 2^51)
+ ((m1 + x / 2^51) % 2^51) * 2^51
+ ((m2 + (m1 + x / 2^51) / 2^51) % 2^51) * 2^102
+ ((m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) % 2^51) * 2^153
+ ((m4 + (m3 + (m2 + (m1 + x / 2^51) / 2^51) / 2^51) / 2^51) % 2^51) * 2^204
= (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) % 2^255 := by
-- name the telescope stages
set t0 := x with ht0
set t1 := m1 + t0 / 2^51 with ht1
set t2 := m2 + t1 / 2^51 with ht2
set t3 := m3 + t2 / 2^51 with ht3
set t4 := m4 + t3 / 2^51 with ht4
-- the top carry-out equals the global quotient (the same telescope as q)
have htop : t4 / 2^51
= (x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) / 2^255 := by
simpa [ht1, ht2, ht3, ht4] using q_telescope x m1 m2 m3 m4
-- flat div/mod facts for each stage
have d0 := Nat.div_add_mod t0 (2^51)
have d1 := Nat.div_add_mod t1 (2^51)
have d2 := Nat.div_add_mod t2 (2^51)
have d3 := Nat.div_add_mod t3 (2^51)
have d4 := Nat.div_add_mod t4 (2^51)
have dT := Nat.div_add_mod
(x + m1 * 2^51 + m2 * 2^102 + m3 * 2^153 + m4 * 2^204) (2^255)
-- linear assembly: Σ fᵢ·2⁵¹ⁱ + 2²⁵⁵·(t4/2⁵¹) = T, then subtract via dT
omega
/-! ### Byte-chunk splits: one per limb, offsets follow 51·j mod 8. -/
/-- Limb 0 (bit offset 0): bytes 0–5 whole, low 3 bits of byte 6. -/
theorem byte_split_0 (f : ℕ) :
f % 2^8 + (f / 2^8 % 2^8) * 2^8 + (f / 2^16 % 2^8) * 2^16
+ (f / 2^24 % 2^8) * 2^24 + (f / 2^32 % 2^8) * 2^32
+ (f / 2^40 % 2^8) * 2^40 + (f / 2^48) * 2^48 = f := by
have e1 : f / 2^8 / 2^8 = f / 2^16 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^16 / 2^8 = f / 2^24 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^24 / 2^8 = f / 2^32 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^32 / 2^8 = f / 2^40 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^40 / 2^8 = f / 2^48 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^8)
have d1 := Nat.div_add_mod (f / 2^8) (2^8)
have d2 := Nat.div_add_mod (f / 2^16) (2^8)
have d3 := Nat.div_add_mod (f / 2^24) (2^8)
have d4 := Nat.div_add_mod (f / 2^32) (2^8)
have d5 := Nat.div_add_mod (f / 2^40) (2^8)
omega
/-- Limb 1 (bit offset 3): low 5 bits close byte 6, bytes 7–11 whole,
low 6 bits of byte 12 take the top (f < 2⁵¹ ⇒ f/2⁴⁵ < 2⁶). -/
theorem byte_split_1 (f : ℕ) :
f % 2^5 + (f / 2^5 % 2^8) * 2^5 + (f / 2^13 % 2^8) * 2^13
+ (f / 2^21 % 2^8) * 2^21 + (f / 2^29 % 2^8) * 2^29
+ (f / 2^37 % 2^8) * 2^37 + (f / 2^45) * 2^45 = f := by
have e1 : f / 2^5 / 2^8 = f / 2^13 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^13 / 2^8 = f / 2^21 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^21 / 2^8 = f / 2^29 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^29 / 2^8 = f / 2^37 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^37 / 2^8 = f / 2^45 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^5)
have d1 := Nat.div_add_mod (f / 2^5) (2^8)
have d2 := Nat.div_add_mod (f / 2^13) (2^8)
have d3 := Nat.div_add_mod (f / 2^21) (2^8)
have d4 := Nat.div_add_mod (f / 2^29) (2^8)
have d5 := Nat.div_add_mod (f / 2^37) (2^8)
omega
/-- Limb 2 (bit offset 6): low 2 bits close byte 12, bytes 13–18 whole,
the single top bit lands in byte 19 (f/2⁵⁰ < 2). -/
theorem byte_split_2 (f : ℕ) :
f % 2^2 + (f / 2^2 % 2^8) * 2^2 + (f / 2^10 % 2^8) * 2^10
+ (f / 2^18 % 2^8) * 2^18 + (f / 2^26 % 2^8) * 2^26
+ (f / 2^34 % 2^8) * 2^34 + (f / 2^42 % 2^8) * 2^42
+ (f / 2^50) * 2^50 = f := by
have e1 : f / 2^2 / 2^8 = f / 2^10 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^10 / 2^8 = f / 2^18 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^18 / 2^8 = f / 2^26 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^26 / 2^8 = f / 2^34 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^34 / 2^8 = f / 2^42 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e6 : f / 2^42 / 2^8 = f / 2^50 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^2)
have d1 := Nat.div_add_mod (f / 2^2) (2^8)
have d2 := Nat.div_add_mod (f / 2^10) (2^8)
have d3 := Nat.div_add_mod (f / 2^18) (2^8)
have d4 := Nat.div_add_mod (f / 2^26) (2^8)
have d5 := Nat.div_add_mod (f / 2^34) (2^8)
have d6 := Nat.div_add_mod (f / 2^42) (2^8)
omega
/-- Limb 3 (bit offset 1): low 7 bits close byte 19, bytes 20–24 whole,
low 4 bits of byte 25 take the top (f/2⁴⁷ < 2⁴). -/
theorem byte_split_3 (f : ℕ) :
f % 2^7 + (f / 2^7 % 2^8) * 2^7 + (f / 2^15 % 2^8) * 2^15
+ (f / 2^23 % 2^8) * 2^23 + (f / 2^31 % 2^8) * 2^31
+ (f / 2^39 % 2^8) * 2^39 + (f / 2^47) * 2^47 = f := by
have e1 : f / 2^7 / 2^8 = f / 2^15 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^15 / 2^8 = f / 2^23 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^23 / 2^8 = f / 2^31 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^31 / 2^8 = f / 2^39 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^39 / 2^8 = f / 2^47 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^7)
have d1 := Nat.div_add_mod (f / 2^7) (2^8)
have d2 := Nat.div_add_mod (f / 2^15) (2^8)
have d3 := Nat.div_add_mod (f / 2^23) (2^8)
have d4 := Nat.div_add_mod (f / 2^31) (2^8)
have d5 := Nat.div_add_mod (f / 2^39) (2^8)
omega
/-- Limb 4 (bit offset 4): high 4 bits of byte 25 take the low 4 bits,
bytes 26–31 whole (f/2⁴⁴ < 2⁷ — the canonical top byte < 2⁷). -/
theorem byte_split_4 (f : ℕ) :
f % 2^4 + (f / 2^4 % 2^8) * 2^4 + (f / 2^12 % 2^8) * 2^12
+ (f / 2^20 % 2^8) * 2^20 + (f / 2^28 % 2^8) * 2^28
+ (f / 2^36 % 2^8) * 2^36 + (f / 2^44) * 2^44 = f := by
have e1 : f / 2^4 / 2^8 = f / 2^12 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e2 : f / 2^12 / 2^8 = f / 2^20 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e3 : f / 2^20 / 2^8 = f / 2^28 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e4 : f / 2^28 / 2^8 = f / 2^36 := by rw [Nat.div_div_eq_div_mul]; norm_num
have e5 : f / 2^36 / 2^8 = f / 2^44 := by rw [Nat.div_div_eq_div_mul]; norm_num
have d0 := Nat.div_add_mod f (2^4)
have d1 := Nat.div_add_mod (f / 2^4) (2^8)
have d2 := Nat.div_add_mod (f / 2^12) (2^8)
have d3 := Nat.div_add_mod (f / 2^20) (2^8)
have d4 := Nat.div_add_mod (f / 2^28) (2^8)
have d5 := Nat.div_add_mod (f / 2^36) (2^8)
omega
/-- THE PACKING IDENTITY: the 32 little-endian bytes that `to_bytes` emits —
27 plain shift-extracts plus 4 boundary bytes (each an OR of the high
bits of one limb with the low bits of the next, already normalized to
its additive form by the walk) — assemble to the limb value. -/
theorem bytes_pack (f0 f1 f2 f3 f4 : ℕ)
(h0 : f0 < 2^51) (h1 : f1 < 2^51) (h2 : f2 < 2^51)
(h3 : f3 < 2^51) (h4 : f4 < 2^51) :
(f0 % 2^8)
+ (f0 / 2^8 % 2^8) * 2^8
+ (f0 / 2^16 % 2^8) * 2^16
+ (f0 / 2^24 % 2^8) * 2^24
+ (f0 / 2^32 % 2^8) * 2^32
+ (f0 / 2^40 % 2^8) * 2^40
+ (f0 / 2^48 + (f1 % 2^5) * 2^3) * 2^48
+ (f1 / 2^5 % 2^8) * 2^56
+ (f1 / 2^13 % 2^8) * 2^64
+ (f1 / 2^21 % 2^8) * 2^72
+ (f1 / 2^29 % 2^8) * 2^80
+ (f1 / 2^37 % 2^8) * 2^88
+ (f1 / 2^45 + (f2 % 2^2) * 2^6) * 2^96
+ (f2 / 2^2 % 2^8) * 2^104
+ (f2 / 2^10 % 2^8) * 2^112
+ (f2 / 2^18 % 2^8) * 2^120
+ (f2 / 2^26 % 2^8) * 2^128
+ (f2 / 2^34 % 2^8) * 2^136
+ (f2 / 2^42 % 2^8) * 2^144
+ (f2 / 2^50 + (f3 % 2^7) * 2^1) * 2^152
+ (f3 / 2^7 % 2^8) * 2^160
+ (f3 / 2^15 % 2^8) * 2^168
+ (f3 / 2^23 % 2^8) * 2^176
+ (f3 / 2^31 % 2^8) * 2^184
+ (f3 / 2^39 % 2^8) * 2^192
+ (f3 / 2^47 + (f4 % 2^4) * 2^4) * 2^200
+ (f4 / 2^4 % 2^8) * 2^208
+ (f4 / 2^12 % 2^8) * 2^216
+ (f4 / 2^20 % 2^8) * 2^224
+ (f4 / 2^28 % 2^8) * 2^232
+ (f4 / 2^36 % 2^8) * 2^240
+ (f4 / 2^44) * 2^248
= f0 + f1 * 2^51 + f2 * 2^102 + f3 * 2^153 + f4 * 2^204 := by
have s0 := byte_split_0 f0
have s1 := byte_split_1 f1
have s2 := byte_split_2 f2
have s3 := byte_split_3 f3
have s4 := byte_split_4 f4
-- Each limb's split, scaled by its radix weight, accounts for exactly the
-- terms above that mention it (boundary bytes contribute to two limbs).
-- Cast to ℤ and take the weighted linear combination of the five splits.
zify at s0 s1 s2 s3 s4 ⊢
linear_combination s0 + 2^51 * s1 + 2^102 * s2 + 2^153 * s3 + 2^204 * s4
/-- Setting a clear top bit by XOR is addition (compress's sign-bit write). -/
theorem xor_top_bit (a : ℕ) (h : a < 2^7) : a ^^^ 2^7 = a + 2^7 := by
have hdiv : (a ^^^ 2^7) / 2^7 = 1 := by
rw [Nat.xor_div_two_pow]
rw [Nat.div_eq_of_lt h]
norm_num
have hand := Nat.and_two_pow_sub_one_eq_mod (a ^^^ 2^7) 7
have hdistrib := Nat.and_xor_distrib_right (a := a) (b := 2^7) (c := 2^7 - 1)
have ha : a &&& (2^7 - 1) = a := by
rw [Nat.and_two_pow_sub_one_eq_mod, Nat.mod_eq_of_lt h]
have h2 : 2^7 &&& (2^7 - 1) = 0 := by decide
have hmod : (a ^^^ 2^7) % 2^7 = a := by
rw [← hand, hdistrib, ha, h2, Nat.xor_zero]
have hdm := Nat.div_add_mod (a ^^^ 2^7) (2^7)
omega
end CurveFieldProofs

767
verification/Proofs/ToBytesSpec.lean Normal file
View file

@ -0,0 +1,767 @@
/- ──────────────────────────────────────────────────────────────────────────────
Proofs/ToBytesSpec.lean — total-correctness spec of `FieldElement51::to_bytes`
(phase 2 of the signature apex: the "to_bytes canonicity" brick).
THE THEOREM (`to_bytes_spec`): for any field element a,
to_bytes a = ok s with bytesVal s = feVal a mod p
— the emitted 32 bytes are the CANONICAL little-endian encoding of the
represented residue. Canonicity (bytesVal s < p, top bit clear) and
injectivity ("equal residues ⇒ equal bytes, equal bytes ⇒ equal residues")
are corollaries (`to_bytes_lt`, at the end), because bytesVal s is pinned
to the residue itself.
STRUCTURE: one straight-line symbolic execution (~150 machine ops — the
longest walk in the repo, but loop-free), consuming the pure ℕ lemmas of
Proofs/ToBytesMath.lean at exactly four joints:
q_telescope — the 5-rung carry chain that computes q = (h+19)/2²⁵⁵;
q_facts — q ∈ {0,1} (also feeds the no-overflow side conditions);
carry_pack + q_mod_p — the final carry pass assembles (h+19q) mod 2²⁵⁵
= h mod p;
bytes_pack — the 32 shift/mask extractions reassemble the value.
The four boundary bytes (6, 12, 19, 25) OR the high bits of one limb with
the low bits of the next; disjointness turns each OR into +
(Nat.two_pow_add_eq_or_of_lt, the ScalarBytesSpec idiom).
Rust: `FieldElement51::to_bytes`, curve25519-dalek/src/backend/serial/u64/
field.rs:368-450 (incl. its trailing debug-assert that the top bit is
clear — discharged, not assumed). Gen: gen/CurveField/Funs.lean
`backend.serial.u64.field.FieldElement51.as_bytes`.
────────────────────────────────────────────────────────────────────────────── -/
import Proofs.ReduceSpec
import Proofs.ToBytesMath
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
abbrev fe_to_bytes := backend.serial.u64.field.FieldElement51.as_bytes
/-- Little-endian value of a 32-byte array (match-style, like `feVal`). -/
def bytesVal (s : Std.Array Std.U8 32#usize) : ℕ :=
match (↑s : List Std.U8) with
| [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] =>
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
| _ => 0
/-- **`to_bytes` is the canonical encoder**: it always succeeds and its
output bytes denote exactly the represented residue mod p. -/
theorem to_bytes_spec (a : Fe) (l0 l1 l2 l3 l4 : U64)
(hl : (↑a : List U64) = [l0, l1, l2, l3, l4]) :
fe_to_bytes a ⦃ s => bytesVal s = feVal a % P ⦄ := by
unfold fe_to_bytes backend.serial.u64.field.FieldElement51.as_bytes
-- weak reduction: limbs < 2⁵¹ + 19·2¹³, value preserved mod p (exactly)
step with (reduce_spec a l0 l1 l2 l3 l4 hl) as ⟨fe, hbnd, hval⟩
obtain ⟨m0, m1, m2, m3, m4, hm⟩ := Fe.exists_limbs fe
rw [Bnd_eq fe m0 m1 m2 m3 m4 _ hm] at hbnd
obtain ⟨hbm0, hbm1, hbm2, hbm3, hbm4⟩ := hbnd
rw [feVal_eq fe m0 m1 m2 m3 m4 hm] at hval
-- h := the weakly-reduced value; h < 2p
have hh2p : limbsVal m0 m1 m2 m3 m4 < 2 * P := by
unfold limbsVal P
omega
-- ── the q pass: q = (h+19)/2²⁵⁵ ─────────────────────────────────────────
step as ⟨i, hi⟩
simp [hm] at hi
step as ⟨i1, hi1⟩
rw [hi] at hi1
step as ⟨q, hq⟩
step as ⟨i2, hi2⟩
simp [hm] at hi2
step as ⟨i3, hi3⟩
rw [hi2] at hi3
step as ⟨q1, hq1⟩
step as ⟨i4, hi4⟩
simp [hm] at hi4
step as ⟨i5, hi5⟩
rw [hi4] at hi5
step as ⟨q2, hq2⟩
step as ⟨i6, hi6⟩
simp [hm] at hi6
step as ⟨i7, hi7⟩
rw [hi6] at hi7
step as ⟨q3, hq3⟩
step as ⟨i8, hi8⟩
simp [hm] at hi8
step as ⟨i9, hi9⟩
rw [hi8] at hi9
step as ⟨q4, hq4⟩
-- q4 = (h + 19) / 2²⁵⁵, and q4 ≤ 1
have hq4v : q4.val = (limbsVal m0 m1 m2 m3 m4 + 19) / 2^255 := by
rw [hq4, nat_shr, hi9, hq3, nat_shr, hi7, hq2, nat_shr, hi5, hq1, nat_shr,
hi3, hq, nat_shr, hi1]
have := q_telescope (m0.val + 19) m1.val m2.val m3.val m4.val
unfold limbsVal
omega
have hq4le : q4.val ≤ 1 := by
rw [hq4v]; exact (q_facts _ hh2p).1
-- fold 19q into limb 0
step as ⟨i10, hi10⟩
step as ⟨i11, hi11⟩
rw [hi] at hi11
step as ⟨limbs, hlimbs⟩
have hll : (↑limbs : List U64) = [i11, m1, m2, m3, m4] := by
simp only [hlimbs, Array.set_val_eq, hm]
rfl
have hi11v : i11.val = m0.val + 19 * q4.val := by
rw [hi11, hi10]
-- the local mask constant 2⁵¹ − 1
step as ⟨i12, hi12⟩
step as ⟨mask, hmask⟩
have hmaskv : mask.val = 2251799813685247 := by
rw [hmask, hi12]
simp [Nat.shiftLeft_eq]
scalar_tac
have hmask_mod : ∀ n : ℕ, n &&& mask.val = n % 2^51 := by
intro n
rw [hmaskv, nat_and_mask]
norm_num
-- ── the carry pass: normalize to radix 2⁵¹, dropping the 2²⁵⁵ carry ────
-- round 0→1
step as ⟨i13, hi13⟩
simp [hll] at hi13
step as ⟨i14, hi14⟩
rw [hi13] at hi14
step as ⟨i15, hi15⟩
simp [hll] at hi15
step as ⟨i16, hi16⟩
rw [hi15] at hi16
step as ⟨limbs1, hlimbs1⟩
have hll1 : (↑limbs1 : List U64) = [i11, i16, m2, m3, m4] := by
simp only [hlimbs1, Array.set_val_eq, hll]; rfl
step as ⟨i17, hi17⟩
simp [hll1] at hi17
step as ⟨i18, hi18⟩
rw [hi17] at hi18
step as ⟨limbs2, hlimbs2⟩
have hll2 : (↑limbs2 : List U64) = [i18, i16, m2, m3, m4] := by
simp only [hlimbs2, Array.set_val_eq, hll1]; rfl
-- round 1→2
step as ⟨i19, hi19⟩
simp [hll2] at hi19
step as ⟨i20, hi20⟩
rw [hi19] at hi20
step as ⟨i21, hi21⟩
simp [hll2] at hi21
step as ⟨i22, hi22⟩
rw [hi21] at hi22
step as ⟨limbs3, hlimbs3⟩
have hll3 : (↑limbs3 : List U64) = [i18, i16, i22, m3, m4] := by
simp only [hlimbs3, Array.set_val_eq, hll2]; rfl
step as ⟨i23, hi23⟩
simp [hll3] at hi23
step as ⟨i24, hi24⟩
rw [hi23] at hi24
step as ⟨limbs4, hlimbs4⟩
have hll4 : (↑limbs4 : List U64) = [i18, i24, i22, m3, m4] := by
simp only [hlimbs4, Array.set_val_eq, hll3]; rfl
-- round 2→3
step as ⟨i25, hi25⟩
simp [hll4] at hi25
step as ⟨i26, hi26⟩
rw [hi25] at hi26
step as ⟨i27, hi27⟩
simp [hll4] at hi27
step as ⟨i28, hi28⟩
rw [hi27] at hi28
step as ⟨limbs5, hlimbs5⟩
have hll5 : (↑limbs5 : List U64) = [i18, i24, i22, i28, m4] := by
simp only [hlimbs5, Array.set_val_eq, hll4]; rfl
step as ⟨i29, hi29⟩
simp [hll5] at hi29
step as ⟨i30, hi30⟩
rw [hi29] at hi30
step as ⟨limbs6, hlimbs6⟩
have hll6 : (↑limbs6 : List U64) = [i18, i24, i30, i28, m4] := by
simp only [hlimbs6, Array.set_val_eq, hll5]; rfl
-- round 3→4
step as ⟨i31, hi31⟩
simp [hll6] at hi31
step as ⟨i32, hi32⟩
rw [hi31] at hi32
step as ⟨i33, hi33⟩
simp [hll6] at hi33
step as ⟨i34, hi34⟩
rw [hi33] at hi34
step as ⟨limbs7, hlimbs7⟩
have hll7 : (↑limbs7 : List U64) = [i18, i24, i30, i28, i34] := by
simp only [hlimbs7, Array.set_val_eq, hll6]; rfl
step as ⟨i35, hi35⟩
simp [hll7] at hi35
step as ⟨i36, hi36⟩
rw [hi35] at hi36
step as ⟨limbs8, hlimbs8⟩
have hll8 : (↑limbs8 : List U64) = [i18, i24, i30, i36, i34] := by
simp only [hlimbs8, Array.set_val_eq, hll7]; rfl
-- top slot: final mask
step as ⟨i37, hi37⟩
simp [hll8] at hi37
step as ⟨i38, hi38⟩
rw [hi37] at hi38
step as ⟨limbs9, hlimbs9⟩
have hll9 : (↑limbs9 : List U64) = [i18, i24, i30, i36, i38] := by
simp only [hlimbs9, Array.set_val_eq, hll8]; rfl
-- ── final-limb values in the exact nested q/r forms carry_pack expects ──
have hf0v : i18.val = i11.val % 2^51 := by
rw [hi18, UScalar.val_and, hmask_mod]
have hi14v : i14.val = i11.val / 2^51 := by
rw [hi14, nat_shr]
have hi16v : i16.val = m1.val + i11.val / 2^51 := by
rw [hi16, hi14v]
have hf1v : i24.val = (m1.val + i11.val / 2^51) % 2^51 := by
rw [hi24, UScalar.val_and, hmask_mod, hi16v]
have hi20v : i20.val = (m1.val + i11.val / 2^51) / 2^51 := by
rw [hi20, nat_shr, hi16v]
have hi22v : i22.val = m2.val + (m1.val + i11.val / 2^51) / 2^51 := by
rw [hi22, hi20v]
have hf2v : i30.val = (m2.val + (m1.val + i11.val / 2^51) / 2^51) % 2^51 := by
rw [hi30, UScalar.val_and, hmask_mod, hi22v]
have hi26v : i26.val = (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51 := by
rw [hi26, nat_shr, hi22v]
have hi28v : i28.val = m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51 := by
rw [hi28, hi26v]
have hf3v : i36.val = (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) % 2^51 := by
rw [hi36, UScalar.val_and, hmask_mod, hi28v]
have hi32v : i32.val = (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51 := by
rw [hi32, nat_shr, hi28v]
have hi34v : i34.val = m4.val + (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51 := by
rw [hi34, hi32v]
have hf4v : i38.val = (m4.val + (m3.val + (m2.val + (m1.val + i11.val / 2^51) / 2^51) / 2^51) / 2^51) % 2^51 := by
rw [hi38, UScalar.val_and, hmask_mod, hi34v]
have hf0lt : i18.val < 2^51 := by rw [hf0v]; exact Nat.mod_lt _ (by norm_num)
have hf1lt : i24.val < 2^51 := by rw [hf1v]; exact Nat.mod_lt _ (by norm_num)
have hf2lt : i30.val < 2^51 := by rw [hf2v]; exact Nat.mod_lt _ (by norm_num)
have hf3lt : i36.val < 2^51 := by rw [hf3v]; exact Nat.mod_lt _ (by norm_num)
have hf4lt : i38.val < 2^51 := by rw [hf4v]; exact Nat.mod_lt _ (by norm_num)
clear hi14 hi16 hi20 hi22 hi26 hi28 hi32 hi34 hi18 hi24 hi30 hi36 hi38
clear hi14v hi16v hi20v hi22v hi26v hi28v hi32v hi34v
clear hlimbs hlimbs1 hlimbs2 hlimbs3 hlimbs4 hlimbs5 hlimbs6 hlimbs7 hlimbs8 hlimbs9
clear hll hll1 hll2 hll3 hll4 hll5 hll6 hll7 hll8
-- ── the 32 byte extractions ──────────────────────────────────────────────
-- byte 0 (limb 0 read + low byte)
step as ⟨v0, hv0⟩
simp [hll9] at hv0
step as ⟨b0, hb0⟩
rw [hv0] at hb0
have hb0v : b0.val = i18.val % 2^8 := by
rw [hb0, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
step as ⟨s1, hs1⟩
have hsl0 : (↑s1 : List Std.U8) = [b0, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs1, Array.set_val_eq, Array.repeat_val]
rfl
clear hb0 hs1
-- byte 1 (limb 0 >> 8)
step as ⟨x1, hx1⟩
rw [hv0] at hx1
step as ⟨b1, hb1⟩
have hb1v : b1.val = i18.val / 2^8 % 2^8 := by
rw [hb1, UScalar.cast_val_eq, hx1, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s2, hs2⟩
have hsl1 : (↑s2 : List Std.U8) = [b0, b1, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs2, Array.set_val_eq, hsl0]
rfl
clear hx1 hb1 hs2 hsl0
-- byte 2 (limb 0 >> 16)
step as ⟨x2, hx2⟩
rw [hv0] at hx2
step as ⟨b2, hb2⟩
have hb2v : b2.val = i18.val / 2^16 % 2^8 := by
rw [hb2, UScalar.cast_val_eq, hx2, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s3, hs3⟩
have hsl2 : (↑s3 : List Std.U8) = [b0, b1, b2, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs3, Array.set_val_eq, hsl1]
rfl
clear hx2 hb2 hs3 hsl1
-- byte 3 (limb 0 >> 24)
step as ⟨x3, hx3⟩
rw [hv0] at hx3
step as ⟨b3, hb3⟩
have hb3v : b3.val = i18.val / 2^24 % 2^8 := by
rw [hb3, UScalar.cast_val_eq, hx3, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s4, hs4⟩
have hsl3 : (↑s4 : List Std.U8) = [b0, b1, b2, b3, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs4, Array.set_val_eq, hsl2]
rfl
clear hx3 hb3 hs4 hsl2
-- byte 4 (limb 0 >> 32)
step as ⟨x4, hx4⟩
rw [hv0] at hx4
step as ⟨b4, hb4⟩
have hb4v : b4.val = i18.val / 2^32 % 2^8 := by
rw [hb4, UScalar.cast_val_eq, hx4, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s5, hs5⟩
have hsl4 : (↑s5 : List Std.U8) = [b0, b1, b2, b3, b4, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs5, Array.set_val_eq, hsl3]
rfl
clear hx4 hb4 hs5 hsl3
-- byte 5 (limb 0 >> 40)
step as ⟨x5, hx5⟩
rw [hv0] at hx5
step as ⟨b5, hb5⟩
have hb5v : b5.val = i18.val / 2^40 % 2^8 := by
rw [hb5, UScalar.cast_val_eq, hx5, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s6, hs6⟩
have hsl5 : (↑s6 : List Std.U8) = [b0, b1, b2, b3, b4, b5, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs6, Array.set_val_eq, hsl4]
rfl
clear hx5 hb5 hs6 hsl4
-- byte 6 (boundary: limb 0 >> 48 | limb 1 << 3)
step as ⟨x6, hx6⟩
rw [hv0] at hx6
step as ⟨v1, hv1⟩
simp [hll9] at hv1
step as ⟨y6, hy6⟩
rw [hv1] at hy6
have hy6v : y6.val = i24.val * 2^3 := by
rw [hy6]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show i24.val * 2^3 < U64.size by scalar_tac)]
step as ⟨z6, hz6⟩
step as ⟨b6, hb6⟩
have hb6v : b6.val = i18.val / 2^48 + (i24.val % 2^5) * 2^3 := by
rw [hb6, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz6, UScalar.val_or, hx6, nat_shr, hy6v]
have hxlt : i18.val / 2^48 < 2^3 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i18.val / 2^48) (i := 3) hxlt (i24.val)
have hadd : i18.val / 2^48 ||| i24.val * 2^3 = i18.val / 2^48 + i24.val * 2^3 := by
calc i18.val / 2^48 ||| i24.val * 2^3
= i18.val / 2^48 ||| 2^3 * i24.val := by rw [Nat.mul_comm]
_ = 2^3 * i24.val ||| i18.val / 2^48 := Nat.lor_comm _ _
_ = 2^3 * i24.val + i18.val / 2^48 := hor.symm
_ = i18.val / 2^48 + i24.val * 2^3 := by ring
rw [hadd]
omega
step as ⟨s7, hs7⟩
have hsl6 : (↑s7 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs7, Array.set_val_eq, hsl5]
rfl
clear hx6 hy6 hy6v hz6 hb6 hs7 hsl5
-- byte 7 (limb 1 >> 5)
step as ⟨x7, hx7⟩
rw [hv1] at hx7
step as ⟨b7, hb7⟩
have hb7v : b7.val = i24.val / 2^5 % 2^8 := by
rw [hb7, UScalar.cast_val_eq, hx7, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s8, hs8⟩
have hsl7 : (↑s8 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs8, Array.set_val_eq, hsl6]
rfl
clear hx7 hb7 hs8 hsl6
-- byte 8 (limb 1 >> 13)
step as ⟨x8, hx8⟩
rw [hv1] at hx8
step as ⟨b8, hb8⟩
have hb8v : b8.val = i24.val / 2^13 % 2^8 := by
rw [hb8, UScalar.cast_val_eq, hx8, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s9, hs9⟩
have hsl8 : (↑s9 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs9, Array.set_val_eq, hsl7]
rfl
clear hx8 hb8 hs9 hsl7
-- byte 9 (limb 1 >> 21)
step as ⟨x9, hx9⟩
rw [hv1] at hx9
step as ⟨b9, hb9⟩
have hb9v : b9.val = i24.val / 2^21 % 2^8 := by
rw [hb9, UScalar.cast_val_eq, hx9, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s10, hs10⟩
have hsl9 : (↑s10 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs10, Array.set_val_eq, hsl8]
rfl
clear hx9 hb9 hs10 hsl8
-- byte 10 (limb 1 >> 29)
step as ⟨x10, hx10⟩
rw [hv1] at hx10
step as ⟨b10, hb10⟩
have hb10v : b10.val = i24.val / 2^29 % 2^8 := by
rw [hb10, UScalar.cast_val_eq, hx10, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s11, hs11⟩
have hsl10 : (↑s11 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs11, Array.set_val_eq, hsl9]
rfl
clear hx10 hb10 hs11 hsl9
-- byte 11 (limb 1 >> 37)
step as ⟨x11, hx11⟩
rw [hv1] at hx11
step as ⟨b11, hb11⟩
have hb11v : b11.val = i24.val / 2^37 % 2^8 := by
rw [hb11, UScalar.cast_val_eq, hx11, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s12, hs12⟩
have hsl11 : (↑s12 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs12, Array.set_val_eq, hsl10]
rfl
clear hx11 hb11 hs12 hsl10
-- byte 12 (boundary: limb 1 >> 45 | limb 2 << 6)
step as ⟨x12, hx12⟩
rw [hv1] at hx12
step as ⟨v2, hv2⟩
simp [hll9] at hv2
step as ⟨y12, hy12⟩
rw [hv2] at hy12
have hy12v : y12.val = i30.val * 2^6 := by
rw [hy12]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show i30.val * 2^6 < U64.size by scalar_tac)]
step as ⟨z12, hz12⟩
step as ⟨b12, hb12⟩
have hb12v : b12.val = i24.val / 2^45 + (i30.val % 2^2) * 2^6 := by
rw [hb12, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz12, UScalar.val_or, hx12, nat_shr, hy12v]
have hxlt : i24.val / 2^45 < 2^6 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i24.val / 2^45) (i := 6) hxlt (i30.val)
have hadd : i24.val / 2^45 ||| i30.val * 2^6 = i24.val / 2^45 + i30.val * 2^6 := by
calc i24.val / 2^45 ||| i30.val * 2^6
= i24.val / 2^45 ||| 2^6 * i30.val := by rw [Nat.mul_comm]
_ = 2^6 * i30.val ||| i24.val / 2^45 := Nat.lor_comm _ _
_ = 2^6 * i30.val + i24.val / 2^45 := hor.symm
_ = i24.val / 2^45 + i30.val * 2^6 := by ring
rw [hadd]
omega
step as ⟨s13, hs13⟩
have hsl12 : (↑s13 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs13, Array.set_val_eq, hsl11]
rfl
clear hx12 hy12 hy12v hz12 hb12 hs13 hsl11
-- byte 13 (limb 2 >> 2)
step as ⟨x13, hx13⟩
rw [hv2] at hx13
step as ⟨b13, hb13⟩
have hb13v : b13.val = i30.val / 2^2 % 2^8 := by
rw [hb13, UScalar.cast_val_eq, hx13, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s14, hs14⟩
have hsl13 : (↑s14 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs14, Array.set_val_eq, hsl12]
rfl
clear hx13 hb13 hs14 hsl12
-- byte 14 (limb 2 >> 10)
step as ⟨x14, hx14⟩
rw [hv2] at hx14
step as ⟨b14, hb14⟩
have hb14v : b14.val = i30.val / 2^10 % 2^8 := by
rw [hb14, UScalar.cast_val_eq, hx14, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s15, hs15⟩
have hsl14 : (↑s15 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs15, Array.set_val_eq, hsl13]
rfl
clear hx14 hb14 hs15 hsl13
-- byte 15 (limb 2 >> 18)
step as ⟨x15, hx15⟩
rw [hv2] at hx15
step as ⟨b15, hb15⟩
have hb15v : b15.val = i30.val / 2^18 % 2^8 := by
rw [hb15, UScalar.cast_val_eq, hx15, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s16, hs16⟩
have hsl15 : (↑s16 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs16, Array.set_val_eq, hsl14]
rfl
clear hx15 hb15 hs16 hsl14
-- byte 16 (limb 2 >> 26)
step as ⟨x16, hx16⟩
rw [hv2] at hx16
step as ⟨b16, hb16⟩
have hb16v : b16.val = i30.val / 2^26 % 2^8 := by
rw [hb16, UScalar.cast_val_eq, hx16, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s17, hs17⟩
have hsl16 : (↑s17 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs17, Array.set_val_eq, hsl15]
rfl
clear hx16 hb16 hs17 hsl15
-- byte 17 (limb 2 >> 34)
step as ⟨x17, hx17⟩
rw [hv2] at hx17
step as ⟨b17, hb17⟩
have hb17v : b17.val = i30.val / 2^34 % 2^8 := by
rw [hb17, UScalar.cast_val_eq, hx17, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s18, hs18⟩
have hsl17 : (↑s18 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs18, Array.set_val_eq, hsl16]
rfl
clear hx17 hb17 hs18 hsl16
-- byte 18 (limb 2 >> 42)
step as ⟨x18, hx18⟩
rw [hv2] at hx18
step as ⟨b18, hb18⟩
have hb18v : b18.val = i30.val / 2^42 % 2^8 := by
rw [hb18, UScalar.cast_val_eq, hx18, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s19, hs19⟩
have hsl18 : (↑s19 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs19, Array.set_val_eq, hsl17]
rfl
clear hx18 hb18 hs19 hsl17
-- byte 19 (boundary: limb 2 >> 50 | limb 3 << 1)
step as ⟨x19, hx19⟩
rw [hv2] at hx19
step as ⟨v3, hv3⟩
simp [hll9] at hv3
step as ⟨y19, hy19⟩
rw [hv3] at hy19
have hy19v : y19.val = i36.val * 2^1 := by
rw [hy19]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show i36.val * 2^1 < U64.size by scalar_tac)]
step as ⟨z19, hz19⟩
step as ⟨b19, hb19⟩
have hb19v : b19.val = i30.val / 2^50 + (i36.val % 2^7) * 2^1 := by
rw [hb19, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz19, UScalar.val_or, hx19, nat_shr, hy19v]
have hxlt : i30.val / 2^50 < 2^1 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i30.val / 2^50) (i := 1) hxlt (i36.val)
have hadd : i30.val / 2^50 ||| i36.val * 2^1 = i30.val / 2^50 + i36.val * 2^1 := by
calc i30.val / 2^50 ||| i36.val * 2^1
= i30.val / 2^50 ||| 2^1 * i36.val := by rw [Nat.mul_comm]
_ = 2^1 * i36.val ||| i30.val / 2^50 := Nat.lor_comm _ _
_ = 2^1 * i36.val + i30.val / 2^50 := hor.symm
_ = i30.val / 2^50 + i36.val * 2^1 := by ring
rw [hadd]
omega
step as ⟨s20, hs20⟩
have hsl19 : (↑s20 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs20, Array.set_val_eq, hsl18]
rfl
clear hx19 hy19 hy19v hz19 hb19 hs20 hsl18
-- byte 20 (limb 3 >> 7)
step as ⟨x20, hx20⟩
rw [hv3] at hx20
step as ⟨b20, hb20⟩
have hb20v : b20.val = i36.val / 2^7 % 2^8 := by
rw [hb20, UScalar.cast_val_eq, hx20, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s21, hs21⟩
have hsl20 : (↑s21 : List Std.U8) = [b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, b16, b17, b18, b19, b20, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs21, Array.set_val_eq, hsl19]
rfl
clear hx20 hb20 hs21 hsl19
-- byte 21 (limb 3 >> 15)
step as ⟨x21, hx21⟩
rw [hv3] at hx21
step as ⟨b21, hb21⟩
have hb21v : b21.val = i36.val / 2^15 % 2^8 := by
rw [hb21, UScalar.cast_val_eq, hx21, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s22, hs22⟩
have hsl21 : (↑s22 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs22, Array.set_val_eq, hsl20]
rfl
clear hx21 hb21 hs22 hsl20
-- byte 22 (limb 3 >> 23)
step as ⟨x22, hx22⟩
rw [hv3] at hx22
step as ⟨b22, hb22⟩
have hb22v : b22.val = i36.val / 2^23 % 2^8 := by
rw [hb22, UScalar.cast_val_eq, hx22, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s23, hs23⟩
have hsl22 : (↑s23 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs23, Array.set_val_eq, hsl21]
rfl
clear hx22 hb22 hs23 hsl21
-- byte 23 (limb 3 >> 31)
step as ⟨x23, hx23⟩
rw [hv3] at hx23
step as ⟨b23, hb23⟩
have hb23v : b23.val = i36.val / 2^31 % 2^8 := by
rw [hb23, UScalar.cast_val_eq, hx23, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s24, hs24⟩
have hsl23 : (↑s24 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs24, Array.set_val_eq, hsl22]
rfl
clear hx23 hb23 hs24 hsl22
-- byte 24 (limb 3 >> 39)
step as ⟨x24, hx24⟩
rw [hv3] at hx24
step as ⟨b24, hb24⟩
have hb24v : b24.val = i36.val / 2^39 % 2^8 := by
rw [hb24, UScalar.cast_val_eq, hx24, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s25, hs25⟩
have hsl24 : (↑s25 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs25, Array.set_val_eq, hsl23]
rfl
clear hx24 hb24 hs25 hsl23
-- byte 25 (boundary: limb 3 >> 47 | limb 4 << 4)
step as ⟨x25, hx25⟩
rw [hv3] at hx25
step as ⟨v4, hv4⟩
simp [hll9] at hv4
step as ⟨y25, hy25⟩
rw [hv4] at hy25
have hy25v : y25.val = i38.val * 2^4 := by
rw [hy25]
simp only [Nat.shiftLeft_eq]
rw [Nat.mod_eq_of_lt (show i38.val * 2^4 < U64.size by scalar_tac)]
step as ⟨z25, hz25⟩
step as ⟨b25, hb25⟩
have hb25v : b25.val = i36.val / 2^47 + (i38.val % 2^4) * 2^4 := by
rw [hb25, UScalar.cast_val_eq]
norm_num [UScalarTy.numBits]
rw [hz25, UScalar.val_or, hx25, nat_shr, hy25v]
have hxlt : i36.val / 2^47 < 2^4 := by omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i36.val / 2^47) (i := 4) hxlt (i38.val)
have hadd : i36.val / 2^47 ||| i38.val * 2^4 = i36.val / 2^47 + i38.val * 2^4 := by
calc i36.val / 2^47 ||| i38.val * 2^4
= i36.val / 2^47 ||| 2^4 * i38.val := by rw [Nat.mul_comm]
_ = 2^4 * i38.val ||| i36.val / 2^47 := Nat.lor_comm _ _
_ = 2^4 * i38.val + i36.val / 2^47 := hor.symm
_ = i36.val / 2^47 + i38.val * 2^4 := by ring
rw [hadd]
omega
step as ⟨s26, hs26⟩
have hsl25 : (↑s26 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs26, Array.set_val_eq, hsl24]
rfl
clear hx25 hy25 hy25v hz25 hb25 hs26 hsl24
-- byte 26 (limb 4 >> 4)
step as ⟨x26, hx26⟩
rw [hv4] at hx26
step as ⟨b26, hb26⟩
have hb26v : b26.val = i38.val / 2^4 % 2^8 := by
rw [hb26, UScalar.cast_val_eq, hx26, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s27, hs27⟩
have hsl26 : (↑s27 : 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, 0#u8, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs27, Array.set_val_eq, hsl25]
rfl
clear hx26 hb26 hs27 hsl25
-- byte 27 (limb 4 >> 12)
step as ⟨x27, hx27⟩
rw [hv4] at hx27
step as ⟨b27, hb27⟩
have hb27v : b27.val = i38.val / 2^12 % 2^8 := by
rw [hb27, UScalar.cast_val_eq, hx27, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s28, hs28⟩
have hsl27 : (↑s28 : 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, 0#u8, 0#u8, 0#u8, 0#u8] := by
simp only [hs28, Array.set_val_eq, hsl26]
rfl
clear hx27 hb27 hs28 hsl26
-- byte 28 (limb 4 >> 20)
step as ⟨x28, hx28⟩
rw [hv4] at hx28
step as ⟨b28, hb28⟩
have hb28v : b28.val = i38.val / 2^20 % 2^8 := by
rw [hb28, UScalar.cast_val_eq, hx28, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s29, hs29⟩
have hsl28 : (↑s29 : 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, 0#u8, 0#u8, 0#u8] := by
simp only [hs29, Array.set_val_eq, hsl27]
rfl
clear hx28 hb28 hs29 hsl27
-- byte 29 (limb 4 >> 28)
step as ⟨x29, hx29⟩
rw [hv4] at hx29
step as ⟨b29, hb29⟩
have hb29v : b29.val = i38.val / 2^28 % 2^8 := by
rw [hb29, UScalar.cast_val_eq, hx29, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s30, hs30⟩
have hsl29 : (↑s30 : 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, 0#u8, 0#u8] := by
simp only [hs30, Array.set_val_eq, hsl28]
rfl
clear hx29 hb29 hs30 hsl28
-- byte 30 (limb 4 >> 36)
step as ⟨x30, hx30⟩
rw [hv4] at hx30
step as ⟨b30, hb30⟩
have hb30v : b30.val = i38.val / 2^36 % 2^8 := by
rw [hb30, UScalar.cast_val_eq, hx30, nat_shr]
norm_num [UScalarTy.numBits]
step as ⟨s31, hs31⟩
have hsl30 : (↑s31 : 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, 0#u8] := by
simp only [hs31, Array.set_val_eq, hsl29]
rfl
clear hx30 hb30 hs31 hsl29
-- byte 31 (limb 4 >> 44)
step as ⟨x31, hx31⟩
rw [hv4] at hx31
step as ⟨b31, hb31⟩
have hb31v : b31.val = i38.val / 2^44 := by
rw [hb31, UScalar.cast_val_eq, hx31, nat_shr]
norm_num [UScalarTy.numBits]
omega
step as ⟨s32, hs32⟩
have hsl31 : (↑s32 : 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] := by
simp only [hs32, Array.set_val_eq, hsl30]
rfl
clear hx31 hb31 hs32 hsl30
-- ── the trailing debug-assert: the top bit of byte 31 is clear ───────────
step as ⟨t115, ht115⟩
simp [hsl31] at ht115
step as ⟨t116, ht116⟩
rw [ht115] at ht116
have hb31lt : b31.val < 2^7 := by
rw [hb31v]; omega
have ht116z : t116 = 0#u8 := by
have hval : t116.val = 0 := by
rw [ht116, UScalar.val_and]
have h128 : (128#u8).val = 2^7 := by norm_num
rw [h128, Nat.and_two_pow]
have htb : b31.val.testBit 7 = false := Nat.testBit_lt_two_pow hb31lt
rw [htb]
simp
scalar_tac
rw [ht116z]
step
try simp only [spec_ok]
-- ── assembly: bytes → limbs → mod-2²⁵⁵ → mod-p ──────────────────────────
have hsum : bytesVal s32 =
i18.val + i24.val * 2^51 + i30.val * 2^102 + i36.val * 2^153 + i38.val * 2^204 := by
simp only [bytesVal, hsl31]
rw [hb0v, hb1v, hb2v, hb3v, hb4v, hb5v, hb6v, hb7v, hb8v, hb9v, hb10v,
hb11v, hb12v, hb13v, hb14v, hb15v, hb16v, hb17v, hb18v, hb19v, hb20v,
hb21v, hb22v, hb23v, hb24v, hb25v, hb26v, hb27v, hb28v, hb29v, hb30v,
hb31v]
exact bytes_pack i18.val i24.val i30.val i36.val i38.val
hf0lt hf1lt hf2lt hf3lt hf4lt
have hmod255 : i18.val + i24.val * 2^51 + i30.val * 2^102 + i36.val * 2^153 + i38.val * 2^204
= (i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204) % 2^255 := by
rw [hf0v, hf1v, hf2v, hf3v, hf4v]
exact carry_pack i11.val m1.val m2.val m3.val m4.val
have hmodp : (i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204) % 2^255
= limbsVal m0 m1 m2 m3 m4 % P := by
have hre : i11.val + m1.val * 2^51 + m2.val * 2^102 + m3.val * 2^153 + m4.val * 2^204
= limbsVal m0 m1 m2 m3 m4 + 19 * ((limbsVal m0 m1 m2 m3 m4 + 19) / 2^255) := by
rw [hi11v, hq4v]
unfold limbsVal
ring
rw [hre]
exact q_mod_p _ hh2p
have hfe_a : feVal a % P = limbsVal m0 m1 m2 m3 m4 % P := by
rw [← hval]
rw [Nat.add_mul_mod_self_left]
rw [hsum, hmod255, hmodp, hfe_a]
end CurveFieldProofs

18
verification/check.sh
View file

@ -63,7 +63,12 @@ PROOFS=(
DsmNafLoopSpec DsmNafLoopSpec
DsmNafSpec DsmNafSpec
DsmMulSpec DsmMulSpec
ToBytesMath
ToBytesSpec
ScalarPackSpec
CompressSpec
SigApexSpec SigApexSpec
PointLiftSpec
) )
# Fully-qualified certificate names; each must be axiom-clean. # Fully-qualified certificate names; each must be axiom-clean.
CERTS=( CERTS=(
@ -83,6 +88,10 @@ CERTS=(
CurveFieldProofs.run_basepoint CurveFieldProofs.run_basepoint
CurveFieldProofs.vartime_double_base_mul_spec CurveFieldProofs.vartime_double_base_mul_spec
CurveFieldProofs.verify_loop_full CurveFieldProofs.verify_loop_full
CurveFieldProofs.to_bytes_spec
CurveFieldProofs.ed_compress_spec
ScalarProofs.from_bytes_mod_order_wide_spec
CurveFieldProofs.vartime_dsm_basepoint_spec
) )
# Imports needed so every certificate in CERTS is in scope for the audit. # Imports needed so every certificate in CERTS is in scope for the audit.
AUDIT_IMPORTS=( AUDIT_IMPORTS=(
@ -94,6 +103,10 @@ AUDIT_IMPORTS=(
Proofs.DsmNafSpec Proofs.DsmNafSpec
Proofs.DsmMulSpec Proofs.DsmMulSpec
Proofs.SigApexSpec Proofs.SigApexSpec
Proofs.ToBytesSpec
Proofs.CompressSpec
Proofs.ScalarPackSpec
Proofs.PointLiftSpec
) )
# ── Phase 0: resource + integrity guards ──────────────────────────────────── # ── Phase 0: resource + integrity guards ────────────────────────────────────
@ -185,12 +198,13 @@ lake env bash -c "
cd '$HERE' cd '$HERE'
ALLOWED='[propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]' ALLOWED='[propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]'
AUD=\$(mktemp '$HERE/.apex-XXXX.lean') AUD=\$(mktemp '$HERE/.apex-XXXX.lean')
{ echo 'import Proofs.SigApexSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; } > \"\$AUD\" { echo 'import Proofs.SigApexSpec'; echo 'import Proofs.PointLiftSpec'; echo '#print axioms CurveFieldProofs.verify_accepts_iff'; echo '#print axioms CurveFieldProofs.verify_accepts_iff_point'; } > \"\$AUD\"
OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1) OUT=\$(LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=4096 '$HERE/lean-guard' \"\$AUD\" 2>&1)
echo \"\$OUT\" echo \"\$OUT\"
rm -f \"\$AUD\" rm -f \"\$AUD\"
FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ') FLAT=\$(echo \"\$OUT\" | tr '\\n' ' ' | tr -s ' ')
if echo \"\$FLAT\" | grep -qF \"depends on axioms: \$ALLOWED\"; then if echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff' depends on axioms: \$ALLOWED\" \
&& echo \"\$FLAT\" | grep -qF \"'CurveFieldProofs.verify_accepts_iff_point' depends on axioms: \$ALLOWED\"; then
echo ' apex axiom cone = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)' echo ' apex axiom cone = exactly the SHA-512 + wire-format boundary (no curve/scalar/backend axioms)'
else else
echo 'APEX AUDIT FAILED: verify_accepts_iff cone is not the documented boundary'; exit 1 echo 'APEX AUDIT FAILED: verify_accepts_iff cone is not the documented boundary'; exit 1