saymrwulf/dalek-ed25519-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/dalek-ed25519-verified.git synced 2026-09-04 20:24:12 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

chore: remove stray telescope probe file (never wired into the button)

Browse source
This commit is contained in:
mrwulf 2026-07-04 04:33:50 +02:00
parent 3037c2e013
commit c3f4ad3692
1 changed files with 0 additions and 28 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
verification/Proofs/TelProbe.lean
View file

@ -1,28 +0,0 @@
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