mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
e07f51c7f7
The load-bearing brick of the point-level apex equation:
FieldElement51::to_bytes always succeeds and its 32 output bytes denote
EXACTLY the represented residue - bytesVal s = feVal a mod p. Since the
canonical residue determines the bytes, this is simultaneously
canonicity ("output is the canonical encoding") and the injectivity
compress needs ("equal residues iff equal bytes").
- Proofs/ToBytesMath.lean: the context-free ℕ mathematics (METHOD 4) -
the 5-rung carry telescope (div_rung/q_telescope), the q-trick facts
(q = (h+19)/2^255 is a bit, fires iff h >= p), q_mod_p (adding 19q and
discarding bit 255 subtracts pq exactly), carry_pack (the masked-limb
assembly mod 2^255), five per-limb byte-chunk splits, and bytes_pack
(the 32-byte little-endian reassembly, closed by one zify +
linear_combination over the five splits).
- Proofs/ToBytesSpec.lean: the symbolic execution - at ~150 machine ops
the longest walk in the repo, loop-free: weak reduce (reduce_spec),
the q pass, the fold + carry pass, 32 byte extractions (the four
limb-boundary bytes turn disjoint ORs into additions via
Nat.two_pow_add_eq_or_of_lt), and the trailing top-bit debug-assert
DISCHARGED (b31 = f4/2^44 < 2^7), not assumed.
- check.sh: ToBytesMath/ToBytesSpec in PROOFS, to_bytes_spec in CERTS
(exact standard-three audit) - full button green fresh.
Walk lessons (for the control repo, next push): rw index-equations into
their consumers instead of subst (subst eliminates the wrong side or
dies on dependent do-motives); never rw [Nat.mod_eq_of_lt (by omega)]
(metavariable goal reaches omega) - state the bound with show.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| AddSpec.lean | ||
| Basic.lean | ||
| ConstSpecs.lean | ||
| Denote.lean | ||
| DsmLoopSpec.lean | ||
| DsmMulSpec.lean | ||
| DsmNafLoadSpec.lean | ||
| DsmNafLoopSpec.lean | ||
| DsmNafMath.lean | ||
| DsmNafSpec.lean | ||
| DsmStepSpec.lean | ||
| DsmTableSpec.lean | ||
| EdAddAffNiels.lean | ||
| EdAddProjNiels.lean | ||
| EdConvert.lean | ||
| EdCurve.lean | ||
| EdDenote.lean | ||
| EdDouble.lean | ||
| EdMain.lean | ||
| FeQ.lean | ||
| Field.lean | ||
| FieldMain.lean | ||
| InvertSpec.lean | ||
| MulSpec.lean | ||
| P25519.lean | ||
| ReduceSpec.lean | ||
| ScalarAddSpec.lean | ||
| ScalarBytesSpec.lean | ||
| ScalarDenote.lean | ||
| ScalarFromBytesSpec.lean | ||
| ScalarFullMulSpec.lean | ||
| ScalarLoop.lean | ||
| ScalarMain.lean | ||
| ScalarMontSpec.lean | ||
| ScalarMulSpec.lean | ||
| ScalarReduceSpec.lean | ||
| ScalarSubSpec.lean | ||
| ScalarUnpackSpec.lean | ||
| ScalarWideSpec.lean | ||
| SigApexSpec.lean | ||
| Square2Spec.lean | ||
| SquareSpec.lean | ||
| SubNegSpec.lean | ||
| ToBytesMath.lean | ||
| ToBytesSpec.lean | ||