mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
a62b8aa14d
button-enforced (phase-2 goal reached on dalek)
CurveFieldProofs.verify_accepts_iff_point_eq: under the half-lift's
hypotheses, for ANY valid on-curve point Q whose canonical encoding is
the signature's R bytes,
verifier accepts <=> Q = [k]*(-A) + [s]*B (as denoted points)
- the literal point-level EdDSA verification equation, no decompress
needed: the canonical encoding is INJECTIVE on curve points.
Proofs/PointEqSpec.lean:
- one_add_d_y_sq_ne_zero: 1 + d*y^2 never vanishes - d nonsquare
(edD_not_square, the completeness ingredient doing its second job)
vs -1 a square (p = 1 mod 4).
- x_sq_of_onCurve + enc_inj_coord: the curve equation determines x^2
from y; +/-x have different parities mod an odd prime unless x = 0,
so y-residue + parity bit determine the point.
- enc_point_inj (standard three axioms): equal canonical encodings of
valid on-curve points force equal denoted points.
- verify_accepts_iff_point_eq: half-lift + injectivity. Axiom cone
EXACTLY the apex boundary; Phase 3b now enforces all THREE tiers
(byte apex, half-lift, point equation).
Remaining phase-2 garnish: the constructive decompress specs (sqrt
chain), giving "the accepted bytes decompress to the recomputed point".
Full button green fresh.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveSig.llbc | ||
| extract.sh | ||
| lean-guard | ||