mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
c85704c0c4
`Proofs/SigApexSpec.lean`:
- `verify_loop_full` — the extracted 32-byte comparison loop returns exactly
the byte-equality of the two arrays (induction; axiom cone = exactly
[propext, Classical.choice, Quot.sound]).
- `verify_accepts_iff` — THE APEX: for a signature that parses, the
extracted RustCrypto verifier accepts IFF the recomputed compressed point
compress( [s]·B − [k]·A )
equals the signature's R byte-for-byte. The recomputation is grounded in
the PROVEN curve model (every curve and scalar call is a certified
definition); k is whatever scalar the SHA-512 oracle produces — the
honest EdDSA acceptance criterion with the hash opaque.
Boundary hygiene forced by the audit itself:
- The public vartime_double_scalar_mul_basepoint dispatch pulled the AVX2
vector-backend axiom into the apex cone. Fixed at the build level:
extract.sh pins RUSTFLAGS --cfg curve25519_dalek_backend="serial", so the
SIMD arm compiles out; BackendKind has only Serial and
get_selected_backend becomes a real definition (ok Serial).
- subtle.Choice.unwrap_u8 upgraded from axiom to the documented model
definition (Choice := U8; unwrap_u8 = self.0) — it sits on the verify
path via compress → is_negative.
- CurveSig modules added to GEN_MODULES (stale-olean incoherence otherwise).
check.sh grows Phase 3b: the apex certificate's axiom cone must equal
EXACTLY
[propext, Classical.choice, Quot.sound,
ed25519.Signature, sha2.Sha512,
sha512_new, sha512_update, sha512_finalize_bytes,
ed25519.Signature.to_bytes, signature.error.Error, Error.new]
— the SHA-512 hash oracle plus the opaque wire-format types. NO curve
axioms, NO scalar axioms, NO backend axioms, enforced on every button press.
Full check.sh green: 16 standard certificates + the apex audit.
Phase 2 (the point-level equation [s]B − [k]A = decompress R, needing
to_bytes canonicity and decompress) remains deferred and documented.
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 | ||