mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-03 20:13:48 +00:00
mrwulf
fe021b9486
THE THEOREM (CurveFieldProofs.verify_accepts_iff_point): for a parsing
signature, a valid on-curve public-key point, a canonical signature
scalar, and a successful recompute, there is a point R' - the certified
[k](-A) + [s]B, ExtValid and on-curve - with
verifier accepts <=> bytesVal R_bytes
= (edY R').val + ((edX R').val % 2) * 2^255
The apex's byte-for-byte comparison IS point-encoding equality: the
signature's R bytes are accepted exactly when they are THE canonical
encoding of the recomputed point. Axiom cone: EXACTLY the apex boundary
(SHA-512 oracle + wire-format opaques; zero curve/scalar/backend axioms),
now enforced for BOTH apex and half-lift by check.sh Phase 3b.
New machinery in Proofs/PointLiftSpec.lean:
- bind_ok_inv: generic ok-inversion of one monadic bind - the clean way
to invert oracle-bearing chains (axioms cannot be walked).
- recompute_inv: names the recompute chain's intermediates (hash, k,
-A, R') with their defining equations, via eight flat bind_ok_inv
steps after the pass-through reductions.
- Bytes64.exists_bytes + List.exists_len32: the 64-byte destructure -
Lean's match refuses list patterns beyond ~32 elements, so the device
is a 32-cons prefix + a list-level 32-destructure on the tail.
- The assembly: recompute_inv + from_bytes_mod_order_wide_spec (k
canonical) + edwards_neg_law (-A) + vartime_dsm_basepoint_spec (R',
valid, on-curve) + ed_compress_spec (er = canonical encoding) +
rangeEq_iff_bytesVal (byte comparison = value equality), threaded
through the ok-injectivity of the inverted equations.
Full button green fresh, incl. the extended Phase 3b.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveSig.llbc | ||
| extract.sh | ||
| lean-guard | ||