saymrwulf/betrusted-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/betrusted-ed25519-verified.git synced 2026-09-04 20:24:08 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
betrusted-ed25519-verified/verification/Proofs/ScalarFromBytesSpec.lean
mrwulf 77262e0ea0 Hash-to-scalar PROVEN: from_bytes_wide_spec - Scalar::from_hash's reduction is exact mod l 
The apex brick of the scalar layer: for any 64 bytes (the opaque SHA-512
digest), [from_bytes_wide bytes] = (LE 512-bit value) mod l, with
canonical 52-bit-bounded output. Composition: bytes_unpack_spec (8x8
loops) -> split_words_lo/hi_spec (exact div/mod per limb, disjoint ORs
as additions) -> wide_split_telescope (isolated omega) -> montgomery_mul
by R and RR (R cancels as a unit, RR restores it) -> the canonical add.

The two kernel-capacity walls found and crossed en route (control repo
FAILURES.md updated):
- a montgomery_mul inside any walk motive replays its 400-line body at
  every kernel step (fix: named prefix functions in the pinned source);
- straight-line IndexMut closure chains make kernel defeq exponential in
  depth (fix: struct-literal construction - the split halves now build
  Scalar52([...]) directly). Full certificate: 77 s kernel-inclusive.

Regenerated gen (sources factor from_bytes_wide -> from_bytes_wide_parts
-> split_words_lo/hi; documented pure refactors, cargo-checked).
check-scalar.sh: 13 proof files, 13 kernel audits, all exactly
[propext, Classical.choice, Quot.sound]. Button pressed fresh: green.
2026-07-04 11:00:52 +02:00

458 lines
26 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

/- Proofs/ScalarFromBytesSpec.lean — hash-to-scalar, the apex brick of the
scalar layer: ⟦from_bytes_wide bytes⟧ = (LE 512-bit value) mod ℓ, the
mathematical content of Scalar::from_hash after the (opaque) SHA-512.
The pinned source factors from_bytes_wide → from_bytes_wide_parts →
split_words_lo/hi (documented pure refactors) so every verification
walk stays at the proven-cheap ~25-step scale and no walk motive ever
carries a Montgomery call — the kernel-replay capacity lesson. -/
import Proofs.ScalarUnpackSpec
import Proofs.ScalarAddSpec
open Aeneas Aeneas.Std Result
open curve25519_dalek
set_option maxHeartbeats 8000000
set_option linter.unusedSimpArgs false
set_option exponentiation.threshold 600
namespace ScalarProofs
open Aeneas.Std.WP
/-- The 512-bit lo/hi split telescope (8 atomic words, isolated omega). -/
theorem wide_split_telescope (v0 v1 v2 v3 v4 v5 v6 v7 : ℕ)
(h0 : v0 < 2^64) (h1 : v1 < 2^64) (h2 : v2 < 2^64) (h3 : v3 < 2^64)
(h4 : v4 < 2^64) (h5 : v5 < 2^64) (h6 : v6 < 2^64) (h7 : v7 < 2^64) :
(v0 % 2^52
+ 2^52 * ((v0 / 2^52 + 2^12 * (v1 % 2^52)) % 2^52)
+ 2^104 * ((v1 / 2^40 + 2^24 * (v2 % 2^40)) % 2^52)
+ 2^156 * ((v2 / 2^28 + 2^36 * (v3 % 2^28)) % 2^52)
+ 2^208 * ((v3 / 2^16 + 2^48 * (v4 % 2^16)) % 2^52))
+ 2^260 *
((v4 / 2^4 % 2^52)
+ 2^52 * ((v4 / 2^56 + 2^8 * (v5 % 2^56)) % 2^52)
+ 2^104 * ((v5 / 2^44 + 2^20 * (v6 % 2^44)) % 2^52)
+ 2^156 * ((v6 / 2^32 + 2^32 * (v7 % 2^32)) % 2^52)
+ 2^208 * (v7 / 2^20 % 2^52))
= v0 + 2^64 * v1 + 2^128 * v2 + 2^192 * v3 + 2^256 * v4
+ 2^320 * v5 + 2^384 * v6 + 2^448 * v7 := by
omega
/-- The lo-half 52-bit split: exact div/mod value per limb. -/
theorem split_words_lo_spec (words : Std.Array Std.U64 8#usize)
(v0 v1 v2 v3 v4 v5 v6 v7 : U64)
(hwsl : (↑words : List U64) = [v0, v1, v2, v3, v4, v5, v6, v7]) :
backend.serial.u64.scalar.Scalar52.split_words_lo words
⦃ s => ∃ i2 i7 i12 i17 i22 : U64,
(↑s : List U64) = [i2, i7, i12, i17, i22] ∧
i2.val = v0.val % 2^52 ∧
i7.val = (v0.val / 2^52 + 2^12 * (v1.val % 2^52)) % 2^52 ∧
i12.val = (v1.val / 2^40 + 2^24 * (v2.val % 2^40)) % 2^52 ∧
i17.val = (v2.val / 2^28 + 2^36 * (v3.val % 2^28)) % 2^52 ∧
i22.val = (v3.val / 2^16 + 2^48 * (v4.val % 2^16)) % 2^52 ⦄ := by
have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
unfold backend.serial.u64.scalar.Scalar52.split_words_lo
have hvb0 : v0.val < 2^64 := by scalar_tac
have hvb1 : v1.val < 2^64 := by scalar_tac
have hvb2 : v2.val < 2^64 := by scalar_tac
have hvb3 : v3.val < 2^64 := by scalar_tac
have hvb4 : v4.val < 2^64 := by scalar_tac
have hvb5 : v5.val < 2^64 := by scalar_tac
have hvb6 : v6.val < 2^64 := by scalar_tac
have hvb7 : v7.val < 2^64 := by scalar_tac
step as ⟨sh, hsh⟩
step as ⟨mask, hmask⟩
have hmaskv : mask.val = 2^52 - 1 := by
simp [hmask, hsh, U64.size_def, U64.numBits]
step as ⟨i1, hi1⟩
simp [hwsl] at hi1
have hi1v : i1.val = v0.val := by rw [hi1]
step as ⟨i2, hi2⟩
have hi2v : i2.val = (v0.val) % 2^52 := by
rw [hi2, UScalar.val_and, hmaskv, hi1v, nat_and_mask52]
step as ⟨i3, hi3⟩
have hi3v : i3.val = v0.val / 2^52 := by
rw [hi3, hi1v, Nat.shiftRight_eq_div_pow]
step as ⟨i4, hi4⟩
simp [hwsl] at hi4
have hi4v : i4.val = v1.val := by rw [hi4]
step as ⟨i5, hi5⟩
have hi5v : i5.val = 2^12 * (v1.val % 2^52) := by
rw [hi5]
simp [hi4v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i6, hi6⟩
have hi6add : i3.val ||| i5.val = i3.val + i5.val := by
have hlt : i3.val < 2^12 := by rw [hi3v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i3.val) (i := 12) hlt (v1.val % 2^52)
calc i3.val ||| i5.val
= i3.val ||| 2^12 * (v1.val % 2^52) := by rw [hi5v]
_ = 2^12 * (v1.val % 2^52) ||| i3.val := Nat.lor_comm _ _
_ = 2^12 * (v1.val % 2^52) + i3.val := hor.symm
_ = i3.val + i5.val := by rw [hi5v]; ring
have hi6v : i6.val = v0.val / 2^52 + 2^12 * (v1.val % 2^52) := by
rw [hi6, UScalar.val_or, hi6add, hi3v, hi5v]
step as ⟨i7, hi7⟩
have hi7v : i7.val = (v0.val / 2^52 + 2^12 * (v1.val % 2^52)) % 2^52 := by
rw [hi7, UScalar.val_and, hmaskv, hi6v, nat_and_mask52]
step as ⟨i8, hi8⟩
have hi8v : i8.val = v1.val / 2^40 := by
rw [hi8, hi4v, Nat.shiftRight_eq_div_pow]
step as ⟨i9, hi9⟩
simp [hwsl] at hi9
have hi9v : i9.val = v2.val := by rw [hi9]
step as ⟨i10, hi10⟩
have hi10v : i10.val = 2^24 * (v2.val % 2^40) := by
rw [hi10]
simp [hi9v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i11, hi11⟩
have hi11add : i8.val ||| i10.val = i8.val + i10.val := by
have hlt : i8.val < 2^24 := by rw [hi8v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i8.val) (i := 24) hlt (v2.val % 2^40)
calc i8.val ||| i10.val
= i8.val ||| 2^24 * (v2.val % 2^40) := by rw [hi10v]
_ = 2^24 * (v2.val % 2^40) ||| i8.val := Nat.lor_comm _ _
_ = 2^24 * (v2.val % 2^40) + i8.val := hor.symm
_ = i8.val + i10.val := by rw [hi10v]; ring
have hi11v : i11.val = v1.val / 2^40 + 2^24 * (v2.val % 2^40) := by
rw [hi11, UScalar.val_or, hi11add, hi8v, hi10v]
step as ⟨i12, hi12⟩
have hi12v : i12.val = (v1.val / 2^40 + 2^24 * (v2.val % 2^40)) % 2^52 := by
rw [hi12, UScalar.val_and, hmaskv, hi11v, nat_and_mask52]
step as ⟨i13, hi13⟩
have hi13v : i13.val = v2.val / 2^28 := by
rw [hi13, hi9v, Nat.shiftRight_eq_div_pow]
step as ⟨i14, hi14⟩
simp [hwsl] at hi14
have hi14v : i14.val = v3.val := by rw [hi14]
step as ⟨i15, hi15⟩
have hi15v : i15.val = 2^36 * (v3.val % 2^28) := by
rw [hi15]
simp [hi14v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i16, hi16⟩
have hi16add : i13.val ||| i15.val = i13.val + i15.val := by
have hlt : i13.val < 2^36 := by rw [hi13v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i13.val) (i := 36) hlt (v3.val % 2^28)
calc i13.val ||| i15.val
= i13.val ||| 2^36 * (v3.val % 2^28) := by rw [hi15v]
_ = 2^36 * (v3.val % 2^28) ||| i13.val := Nat.lor_comm _ _
_ = 2^36 * (v3.val % 2^28) + i13.val := hor.symm
_ = i13.val + i15.val := by rw [hi15v]; ring
have hi16v : i16.val = v2.val / 2^28 + 2^36 * (v3.val % 2^28) := by
rw [hi16, UScalar.val_or, hi16add, hi13v, hi15v]
step as ⟨i17, hi17⟩
have hi17v : i17.val = (v2.val / 2^28 + 2^36 * (v3.val % 2^28)) % 2^52 := by
rw [hi17, UScalar.val_and, hmaskv, hi16v, nat_and_mask52]
step as ⟨i18, hi18⟩
have hi18v : i18.val = v3.val / 2^16 := by
rw [hi18, hi14v, Nat.shiftRight_eq_div_pow]
step as ⟨i19, hi19⟩
simp [hwsl] at hi19
have hi19v : i19.val = v4.val := by rw [hi19]
step as ⟨i20, hi20⟩
have hi20v : i20.val = 2^48 * (v4.val % 2^16) := by
rw [hi20]
simp [hi19v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i21, hi21⟩
have hi21add : i18.val ||| i20.val = i18.val + i20.val := by
have hlt : i18.val < 2^48 := by rw [hi18v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i18.val) (i := 48) hlt (v4.val % 2^16)
calc i18.val ||| i20.val
= i18.val ||| 2^48 * (v4.val % 2^16) := by rw [hi20v]
_ = 2^48 * (v4.val % 2^16) ||| i18.val := Nat.lor_comm _ _
_ = 2^48 * (v4.val % 2^16) + i18.val := hor.symm
_ = i18.val + i20.val := by rw [hi20v]; ring
have hi21v : i21.val = v3.val / 2^16 + 2^48 * (v4.val % 2^16) := by
rw [hi21, UScalar.val_or, hi21add, hi18v, hi20v]
step as ⟨i22, hi22⟩
have hi22v : i22.val = (v3.val / 2^16 + 2^48 * (v4.val % 2^16)) % 2^52 := by
rw [hi22, UScalar.val_and, hmaskv, hi21v, nat_and_mask52]
have hlist : (↑(Array.make 5#usize [ i2, i7, i12, i17, i22 ]) : List U64) = [i2, i7, i12, i17, i22] := by rfl
try simp only [spec_ok]
exact ⟨i2, i7, i12, i17, i22, hlist, hi2v, hi7v, hi12v, hi17v, hi22v⟩
/-- The hi-half 52-bit split: exact div/mod value per limb. -/
theorem split_words_hi_spec (words : Std.Array Std.U64 8#usize)
(v0 v1 v2 v3 v4 v5 v6 v7 : U64)
(hwsl : (↑words : List U64) = [v0, v1, v2, v3, v4, v5, v6, v7]) :
backend.serial.u64.scalar.Scalar52.split_words_hi words
⦃ s => ∃ i3 i8 i13 i18 i20 : U64,
(↑s : List U64) = [i3, i8, i13, i18, i20] ∧
i3.val = v4.val / 2^4 % 2^52 ∧
i8.val = (v4.val / 2^56 + 2^8 * (v5.val % 2^56)) % 2^52 ∧
i13.val = (v5.val / 2^44 + 2^20 * (v6.val % 2^44)) % 2^52 ∧
i18.val = (v6.val / 2^32 + 2^32 * (v7.val % 2^32)) % 2^52 ∧
i20.val = v7.val / 2^20 % 2^52 ⦄ := by
have hsz64 : (U64.size : ℕ) = 2^64 := by scalar_tac
unfold backend.serial.u64.scalar.Scalar52.split_words_hi
have hvb0 : v0.val < 2^64 := by scalar_tac
have hvb1 : v1.val < 2^64 := by scalar_tac
have hvb2 : v2.val < 2^64 := by scalar_tac
have hvb3 : v3.val < 2^64 := by scalar_tac
have hvb4 : v4.val < 2^64 := by scalar_tac
have hvb5 : v5.val < 2^64 := by scalar_tac
have hvb6 : v6.val < 2^64 := by scalar_tac
have hvb7 : v7.val < 2^64 := by scalar_tac
step as ⟨sh, hsh⟩
step as ⟨mask, hmask⟩
have hmaskv : mask.val = 2^52 - 1 := by
simp [hmask, hsh, U64.size_def, U64.numBits]
step as ⟨i1, hi1⟩
simp [hwsl] at hi1
have hi1v : i1.val = v4.val := by rw [hi1]
step as ⟨i2, hi2⟩
have hi2v : i2.val = v4.val / 2^4 := by
rw [hi2, hi1v, Nat.shiftRight_eq_div_pow]
step as ⟨i3, hi3⟩
have hi3v : i3.val = (v4.val / 2^4) % 2^52 := by
rw [hi3, UScalar.val_and, hmaskv, hi2v, nat_and_mask52]
step as ⟨i4, hi4⟩
have hi4v : i4.val = v4.val / 2^56 := by
rw [hi4, hi1v, Nat.shiftRight_eq_div_pow]
step as ⟨i5, hi5⟩
simp [hwsl] at hi5
have hi5v : i5.val = v5.val := by rw [hi5]
step as ⟨i6, hi6⟩
have hi6v : i6.val = 2^8 * (v5.val % 2^56) := by
rw [hi6]
simp [hi5v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i7, hi7⟩
have hi7add : i4.val ||| i6.val = i4.val + i6.val := by
have hlt : i4.val < 2^8 := by rw [hi4v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i4.val) (i := 8) hlt (v5.val % 2^56)
calc i4.val ||| i6.val
= i4.val ||| 2^8 * (v5.val % 2^56) := by rw [hi6v]
_ = 2^8 * (v5.val % 2^56) ||| i4.val := Nat.lor_comm _ _
_ = 2^8 * (v5.val % 2^56) + i4.val := hor.symm
_ = i4.val + i6.val := by rw [hi6v]; ring
have hi7v : i7.val = v4.val / 2^56 + 2^8 * (v5.val % 2^56) := by
rw [hi7, UScalar.val_or, hi7add, hi4v, hi6v]
step as ⟨i8, hi8⟩
have hi8v : i8.val = (v4.val / 2^56 + 2^8 * (v5.val % 2^56)) % 2^52 := by
rw [hi8, UScalar.val_and, hmaskv, hi7v, nat_and_mask52]
step as ⟨i9, hi9⟩
have hi9v : i9.val = v5.val / 2^44 := by
rw [hi9, hi5v, Nat.shiftRight_eq_div_pow]
step as ⟨i10, hi10⟩
simp [hwsl] at hi10
have hi10v : i10.val = v6.val := by rw [hi10]
step as ⟨i11, hi11⟩
have hi11v : i11.val = 2^20 * (v6.val % 2^44) := by
rw [hi11]
simp [hi10v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i12, hi12⟩
have hi12add : i9.val ||| i11.val = i9.val + i11.val := by
have hlt : i9.val < 2^20 := by rw [hi9v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i9.val) (i := 20) hlt (v6.val % 2^44)
calc i9.val ||| i11.val
= i9.val ||| 2^20 * (v6.val % 2^44) := by rw [hi11v]
_ = 2^20 * (v6.val % 2^44) ||| i9.val := Nat.lor_comm _ _
_ = 2^20 * (v6.val % 2^44) + i9.val := hor.symm
_ = i9.val + i11.val := by rw [hi11v]; ring
have hi12v : i12.val = v5.val / 2^44 + 2^20 * (v6.val % 2^44) := by
rw [hi12, UScalar.val_or, hi12add, hi9v, hi11v]
step as ⟨i13, hi13⟩
have hi13v : i13.val = (v5.val / 2^44 + 2^20 * (v6.val % 2^44)) % 2^52 := by
rw [hi13, UScalar.val_and, hmaskv, hi12v, nat_and_mask52]
step as ⟨i14, hi14⟩
have hi14v : i14.val = v6.val / 2^32 := by
rw [hi14, hi10v, Nat.shiftRight_eq_div_pow]
step as ⟨i15, hi15⟩
simp [hwsl] at hi15
have hi15v : i15.val = v7.val := by rw [hi15]
step as ⟨i16, hi16⟩
have hi16v : i16.val = 2^32 * (v7.val % 2^32) := by
rw [hi16]
simp [hi15v, Nat.shiftLeft_eq, hsz64]
omega
step as ⟨i17, hi17⟩
have hi17add : i14.val ||| i16.val = i14.val + i16.val := by
have hlt : i14.val < 2^32 := by rw [hi14v]; omega
have hor := Nat.two_pow_add_eq_or_of_lt (b := i14.val) (i := 32) hlt (v7.val % 2^32)
calc i14.val ||| i16.val
= i14.val ||| 2^32 * (v7.val % 2^32) := by rw [hi16v]
_ = 2^32 * (v7.val % 2^32) ||| i14.val := Nat.lor_comm _ _
_ = 2^32 * (v7.val % 2^32) + i14.val := hor.symm
_ = i14.val + i16.val := by rw [hi16v]; ring
have hi17v : i17.val = v6.val / 2^32 + 2^32 * (v7.val % 2^32) := by
rw [hi17, UScalar.val_or, hi17add, hi14v, hi16v]
step as ⟨i18, hi18⟩
have hi18v : i18.val = (v6.val / 2^32 + 2^32 * (v7.val % 2^32)) % 2^52 := by
rw [hi18, UScalar.val_and, hmaskv, hi17v, nat_and_mask52]
step as ⟨i19, hi19⟩
have hi19v : i19.val = v7.val / 2^20 := by
rw [hi19, hi15v, Nat.shiftRight_eq_div_pow]
step as ⟨i20, hi20⟩
have hi20v : i20.val = (v7.val / 2^20) % 2^52 := by
rw [hi20, UScalar.val_and, hmaskv, hi19v, nat_and_mask52]
have hlist : (↑(Array.make 5#usize [ i3, i8, i13, i18, i20 ]) : List U64) = [i3, i8, i13, i18, i20] := by rfl
try simp only [spec_ok]
exact ⟨i3, i8, i13, i18, i20, hlist, hi3v, hi8v, hi13v, hi18v, hi20v⟩
/-- The prefix: bytes → words (bytes_unpack_spec) → the lo/hi pair. -/
theorem fbw_parts_spec (bytes : 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 : (↑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, 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]) :
backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts bytes
⦃ p => ∃ v0 v1 v2 v3 v4 v5 v6 v7 i2 i7 i12 i17 i22 h0 h1 h2 h3 h4 : U64,
(↑p.1 : List U64) = [i2, i7, i12, i17, i22] ∧
(↑p.2 : List U64) = [h0, h1, h2, h3, h4] ∧
v0.val = 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 ∧
v1.val = b8.val + b9.val * 2^8 + b10.val * 2^16 + b11.val * 2^24 + b12.val * 2^32 + b13.val * 2^40 + b14.val * 2^48 + b15.val * 2^56 ∧
v2.val = b16.val + b17.val * 2^8 + b18.val * 2^16 + b19.val * 2^24 + b20.val * 2^32 + b21.val * 2^40 + b22.val * 2^48 + b23.val * 2^56 ∧
v3.val = b24.val + b25.val * 2^8 + b26.val * 2^16 + b27.val * 2^24 + b28.val * 2^32 + b29.val * 2^40 + b30.val * 2^48 + b31.val * 2^56 ∧
v4.val = b32.val + b33.val * 2^8 + b34.val * 2^16 + b35.val * 2^24 + b36.val * 2^32 + b37.val * 2^40 + b38.val * 2^48 + b39.val * 2^56 ∧
v5.val = b40.val + b41.val * 2^8 + b42.val * 2^16 + b43.val * 2^24 + b44.val * 2^32 + b45.val * 2^40 + b46.val * 2^48 + b47.val * 2^56 ∧
v6.val = b48.val + b49.val * 2^8 + b50.val * 2^16 + b51.val * 2^24 + b52.val * 2^32 + b53.val * 2^40 + b54.val * 2^48 + b55.val * 2^56 ∧
v7.val = b56.val + b57.val * 2^8 + b58.val * 2^16 + b59.val * 2^24 + b60.val * 2^32 + b61.val * 2^40 + b62.val * 2^48 + b63.val * 2^56 ∧
i2.val = v0.val % 2^52 ∧
i7.val = (v0.val / 2^52 + 2^12 * (v1.val % 2^52)) % 2^52 ∧
i12.val = (v1.val / 2^40 + 2^24 * (v2.val % 2^40)) % 2^52 ∧
i17.val = (v2.val / 2^28 + 2^36 * (v3.val % 2^28)) % 2^52 ∧
i22.val = (v3.val / 2^16 + 2^48 * (v4.val % 2^16)) % 2^52 ∧
h0.val = v4.val / 2^4 % 2^52 ∧
h1.val = (v4.val / 2^56 + 2^8 * (v5.val % 2^56)) % 2^52 ∧
h2.val = (v5.val / 2^44 + 2^20 * (v6.val % 2^44)) % 2^52 ∧
h3.val = (v6.val / 2^32 + 2^32 * (v7.val % 2^32)) % 2^52 ∧
h4.val = v7.val / 2^20 % 2^52 ⦄ := by
unfold backend.serial.u64.scalar.Scalar52.from_bytes_wide_parts
have hrep : (↑(Array.repeat 8#usize 0#u64) : List U64)
= [0#u64, 0#u64, 0#u64, 0#u64, 0#u64, 0#u64, 0#u64, 0#u64] := by rfl
step with (bytes_unpack_spec bytes (Array.repeat 8#usize 0#u64)
b0 b1 b2 b3 b4 b5 b6 b7 b8 b9 b10 b11 b12 b13 b14 b15 b16 b17 b18 b19 b20 b21 b22 b23 b24 b25 b26 b27 b28 b29 b30 b31 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
0#u64 0#u64 0#u64 0#u64 0#u64 0#u64 0#u64 0#u64 hb hrep
⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩) as
⟨v0, v1, v2, v3, v4, v5, v6, v7, ws, hwsl, hv0, hv1, hv2, hv3, hv4, hv5, hv6, hv7⟩
step with (split_words_lo_spec ws v0 v1 v2 v3 v4 v5 v6 v7 hwsl) as
⟨i2, i7, i12, i17, i22, slo, hlol, hi2v, hi7v, hi12v, hi17v, hi22v⟩
step with (split_words_hi_spec ws v0 v1 v2 v3 v4 v5 v6 v7 hwsl) as
⟨i3, i8, i13, i18, i20, shi, hhil, hi3v, hi8v, hi13v, hi18v, hi20v⟩
try simp only [spec_ok]
exact ⟨v0, v1, v2, v3, v4, v5, v6, v7, i2, i7, i12, i17, i22, i3, i8, i13, i18, i20,
hlol, hhil, hv0, hv1, hv2, hv3, hv4, hv5, hv6, hv7,
hi2v, hi7v, hi12v, hi17v, hi22v, hi3v, hi8v, hi13v, hi18v, hi20v⟩
/-- **Hash-to-scalar is exact reduction mod ℓ.** -/
theorem from_bytes_wide_spec (bytes : 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 : (↑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, 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) :
backend.serial.u64.scalar.Scalar52.from_bytes_wide bytes
⦃ r => (∃ s0 s1 s2 s3 s4 : U64, (↑r : List U64) = [s0, s1, s2, s3, s4] ∧
s0.val < 2^52 ∧ s1.val < 2^52 ∧ s2.val < 2^52 ∧ s3.val < 2^52 ∧
s4.val < 2^52) ∧
scVal r < Ell ∧
scDenote r = (T : ZMod Ell) ⦄ := by
unfold backend.serial.u64.scalar.Scalar52.from_bytes_wide
apply spec_bind (fbw_parts_spec bytes 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)
rintro ⟨lo, hi⟩ ⟨v0, v1, v2, v3, v4, v5, v6, v7, i2, i7, i12, i17, i22, i3, i8, i13, i18, i20,
hlol, hhil, hv0, hv1, hv2, hv3, hv4, hv5, hv6, hv7,
hi2v, hi7v, hi12v, hi17v, hi22v, hi3v, hi8v, hi13v, hi18v, hi20v⟩
simp only at hlol hhil
have hvb0 : v0.val < 2^64 := by scalar_tac
have hvb1 : v1.val < 2^64 := by scalar_tac
have hvb2 : v2.val < 2^64 := by scalar_tac
have hvb3 : v3.val < 2^64 := by scalar_tac
have hvb4 : v4.val < 2^64 := by scalar_tac
have hvb5 : v5.val < 2^64 := by scalar_tac
have hvb6 : v6.val < 2^64 := by scalar_tac
have hvb7 : v7.val < 2^64 := by scalar_tac
have hbndi2 : i2.val < 2^52 := by
rw [hi2v]; exact Nat.mod_lt _ (by norm_num)
have hbndi7 : i7.val < 2^52 := by
rw [hi7v]; exact Nat.mod_lt _ (by norm_num)
have hbndi12 : i12.val < 2^52 := by
rw [hi12v]; exact Nat.mod_lt _ (by norm_num)
have hbndi17 : i17.val < 2^52 := by
rw [hi17v]; exact Nat.mod_lt _ (by norm_num)
have hbndi22 : i22.val < 2^52 := by
rw [hi22v]; exact Nat.mod_lt _ (by norm_num)
have hbndi3 : i3.val < 2^52 := by
rw [hi3v]; exact Nat.mod_lt _ (by norm_num)
have hbndi8 : i8.val < 2^52 := by
rw [hi8v]; exact Nat.mod_lt _ (by norm_num)
have hbndi13 : i13.val < 2^52 := by
rw [hi13v]; exact Nat.mod_lt _ (by norm_num)
have hbndi18 : i18.val < 2^52 := by
rw [hi18v]; exact Nat.mod_lt _ (by norm_num)
have hbndi20 : i20.val < 2^52 := by
rw [hi20v]; exact Nat.mod_lt _ (by norm_num)
have hlov : scVal lo = scLimbs i2 i7 i12 i17 i22 := scVal_eq _ _ _ _ _ _ hlol
have hhiv : scVal hi = scLimbs i3 i8 i13 i18 i20 := scVal_eq _ _ _ _ _ _ hhil
have hlolt : scVal lo < 2^260 := by
rw [hlov]; unfold scLimbs
exact nonce_sum_bound hbndi2 hbndi7 hbndi12 hbndi17 hbndi22
have hhilt : scVal hi < 2^260 := by
rw [hhiv]; unfold scLimbs
exact nonce_sum_bound hbndi3 hbndi8 hbndi13 hbndi18 hbndi20
have hcablo : scVal lo * scVal backend.serial.u64.constants.R < 2^260 * Ell :=
Nat.mul_lt_mul'' hlolt R_lt
have hcabhi : scVal hi * scVal backend.serial.u64.constants.RR < 2^260 * Ell :=
Nat.mul_lt_mul'' hhilt RR_lt
have hRl0 : (4302102966953709#u64).val = 4302102966953709 := by rfl
have hRl1 : (1049714374468698#u64).val = 1049714374468698 := by rfl
have hRl2 : (4503599278581019#u64).val = 4503599278581019 := by rfl
have hRl3 : (4503599627370495#u64).val = 4503599627370495 := by rfl
have hRl4 : (17592186044415#u64).val = 17592186044415 := by rfl
have hRRl0 : (2764609938444603#u64).val = 2764609938444603 := by rfl
have hRRl1 : (3768881411696287#u64).val = 3768881411696287 := by rfl
have hRRl2 : (1616719297148420#u64).val = 1616719297148420 := by rfl
have hRRl3 : (1087343033131391#u64).val = 1087343033131391 := by rfl
have hRRl4 : (10175238647962#u64).val = 10175238647962 := by rfl
step with (montgomery_mul_spec lo backend.serial.u64.constants.R
i2 i7 i12 i17 i22
(4302102966953709#u64) (1049714374468698#u64) (4503599278581019#u64)
(4503599627370495#u64) (17592186044415#u64)
hlol R_limbs
⟨hbndi2, hbndi7, hbndi12, hbndi17, hbndi22⟩
⟨by rw [hRl0]; norm_num, by rw [hRl1]; norm_num, by rw [hRl2]; norm_num,
by rw [hRl3]; norm_num, by rw [hRl4]; norm_num⟩
hcablo) as ⟨lo1, hlo1ex, hlo1c, hlo1d⟩
obtain ⟨p0, p1, p2, p3, p4, hlo1l, hp0, hp1, hp2, hp3, hp4⟩ := hlo1ex
step with (montgomery_mul_spec hi backend.serial.u64.constants.RR
i3 i8 i13 i18 i20
(2764609938444603#u64) (3768881411696287#u64) (1616719297148420#u64)
(1087343033131391#u64) (10175238647962#u64)
hhil RR_limbs
⟨hbndi3, hbndi8, hbndi13, hbndi18, hbndi20⟩
⟨by rw [hRRl0]; norm_num, by rw [hRRl1]; norm_num, by rw [hRRl2]; norm_num,
by rw [hRRl3]; norm_num, by rw [hRRl4]; norm_num⟩
hcabhi) as ⟨hi1, hhi1ex, hhi1c, hhi1d⟩
obtain ⟨q0, q1, q2, q3, q4, hhi1l, hq0, hq1, hq2, hq3, hq4⟩ := hhi1ex
apply spec_mono (add_val_spec hi1 lo1 q0 q1 q2 q3 q4 p0 p1 p2 p3 p4 hhi1l hlo1l
⟨hq0, hq1, hq2, hq3, hq4⟩ ⟨hp0, hp1, hp2, hp3, hp4⟩ hhi1c hlo1c)
intro r hr
refine ⟨hr.1, hr.2.1, ?_⟩
rw [hr.2.2]
have hRd : scDenote backend.serial.u64.constants.R = 2^260 := by
simp only [scDenote, R_scVal]; exact R_denote
have hRRd : scDenote backend.serial.u64.constants.RR = 2^520 := by
simp only [scDenote, RR_scVal]; exact RR_denote
have hlo1v : scDenote lo1 = scDenote lo :=
R_isUnit.mul_right_cancel (by rw [hlo1d, hRd])
have hhi1v : scDenote hi1 = scDenote hi * 2^260 :=
R_isUnit.mul_right_cancel (by rw [hhi1d, hRRd]; ring)
have hLOv : scVal lo = v0.val % 2^52 + 2^52 * ((v0.val / 2^52 + 2^12 * (v1.val % 2^52)) % 2^52) + 2^104 * ((v1.val / 2^40 + 2^24 * (v2.val % 2^40)) % 2^52) + 2^156 * ((v2.val / 2^28 + 2^36 * (v3.val % 2^28)) % 2^52) + 2^208 * ((v3.val / 2^16 + 2^48 * (v4.val % 2^16)) % 2^52) := by
rw [hlov]; unfold scLimbs
rw [hi2v, hi7v, hi12v, hi17v, hi22v]
have hHIv : scVal hi = v4.val / 2^4 % 2^52 + 2^52 * ((v4.val / 2^56 + 2^8 * (v5.val % 2^56)) % 2^52) + 2^104 * ((v5.val / 2^44 + 2^20 * (v6.val % 2^44)) % 2^52) + 2^156 * ((v6.val / 2^32 + 2^32 * (v7.val % 2^32)) % 2^52) + 2^208 * (v7.val / 2^20 % 2^52) := by
rw [hhiv]; unfold scLimbs
rw [hi3v, hi8v, hi13v, hi18v, hi20v]
have htel := wide_split_telescope v0.val v1.val v2.val v3.val v4.val v5.val
v6.val v7.val hvb0 hvb1 hvb2 hvb3 hvb4 hvb5 hvb6 hvb7
have hVB : v0.val + 2^64 * v1.val + 2^128 * v2.val + 2^192 * v3.val + 2^256 * v4.val + 2^320 * v5.val + 2^384 * v6.val + 2^448 * v7.val
= 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 := by
rw [hv0, hv1, hv2, hv3, hv4, hv5, hv6, hv7]; ring
have hT2 : T = 2^260 * scVal hi + scVal lo := by
rw [hT, ← hVB, hHIv, hLOv, ← htel]
exact Nat.add_comm _ _
rw [hhi1v, hlo1v, hT2]
simp only [scDenote]
push_cast
ring
end ScalarProofs
Reference in a new issue View git blame Copy permalink