mirror of
https://github.com/saymrwulf/dalek-ed25519-verified.git
synced 2026-09-04 20:24:12 +00:00
mrwulf
4140ff3249
Gen merge: extract.sh now co-extracts the Scalar52 backend and the public scalar::from_bytes_mod_order[_wide] conversions into the SAME CurveField model, so the whole library — field, curve_models, edwards, scalar — shares one type universe (Scalar is a single structure, not two). The scalar proof chain repoints by one import line (ScalarDenote: CurveScalar.Funs -> CurveField.Funs); check-scalar.sh's gen list follows. Both buttons — the scalar certificates and the field/group/dsm certificates — pass fresh over the merged gen, so the merge is proven-safe, not merely hoped-safe. Verify glue (gen/CurveSig): the extracted ed25519-dalek verify_sha512 path, integrated against the proven model: - TypesExternal.lean imports CurveField.Types, so CompressedEdwardsY / EdwardsPoint / Scalar in the glue ARE the proven model's types. Only the genuinely foreign types stay opaque: sha2.Sha512, ed25519.Signature, signature.error.Error. - FunsExternal.lean imports CurveField.Funs, so every curve/scalar call (compress, vartime_double_scalar_mul_basepoint, as_bytes, neg, from_bytes_mod_order[_wide]) resolves to a proven definition — no axioms. The `?`-operator plumbing (Try::branch, FromResidual::from_residual) and compressed_from_bytes get real definitions. Only the SHA-512 hasher (sha512_new/update/finalize_bytes) and two opaque wire accessors (Signature.to_bytes, Error.new) remain axiomatized — the deliberate, documented hash-oracle boundary. Audited: `verify_sha512`'s entire axiom cone is [propext, Classical.choice, Quot.sound, sha2.Sha512, sha512_new, sha512_update, sha512_finalize_bytes, ed25519.Signature.to_bytes, signature.error.Error.new] — zero curve axioms, zero scalar axioms. The verify path is definitionally grounded in the certified model; the only trust boundary is SHA-512. 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 | ||
| Square2Spec.lean | ||
| SquareSpec.lean | ||
| SubNegSpec.lean | ||