dalek-ed25519-verified/verification/Proofs/TelProbe.lean

import Proofs.ScalarDenote
open Aeneas Aeneas.Std

set_option maxHeartbeats 8000000
set_option exponentiation.threshold 600

namespace ScalarProofs

/-- The 512-bit lo/hi split telescope. -/
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

end ScalarProofs
-												Signature layer: the 64-byte unpack certificates (8x8 loops proven)

Toward Scalar::from_hash: bytes_unpack_spec proves the from_bytes_wide
word-unpack loops pack 64 little-endian bytes into 8 words exactly.

- Proofs/ScalarBytesSpec.lean (3308 lines): bytes_word_loop_spec_0..7,
  each split head/tail at j=4 (the 8-fold monolith grows exponentially
  in elaboration - METHOD 4). Disjoint-bit ORs become additions via
  core's Nat.two_pow_add_eq_or_of_lt with explicit calc bridges (the
  default simp set literalizes 2^8 -> 256 and breaks pow-form rewrites;
  simp only everywhere).
- Proofs/ScalarUnpackSpec.lean: bytes_unpack_spec composes the eight
  inner lemmas through the outer loop (iterator start needs a term-level
  equality rewrite per peel).

The from_bytes_wide main walk itself is proven at elaboration level
(fail-probe verified end to end) but its single-decl kernel certificate
replays >30min; it ships next as a phase-split (plan in the control
repo's method notes). check-scalar.sh: 12 proof files, 12 kernel audits,
all exactly [propext, Classical.choice, Quot.sound]. Button green.

											
										
										
											2026-07-04 01:00:42 +00:00
+								import Proofs.ScalarDenote
 								open Aeneas Aeneas.Std
 								set_option maxHeartbeats 8000000
 								set_option exponentiation.threshold 600
 								namespace ScalarProofs
 								/-- The 512-bit lo/hi split telescope. -/
 								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
 								end ScalarProofs