mirror of
https://github.com/saymrwulf/betrusted-ed25519-verified.git
synced 2026-09-04 20:24:08 +00:00
mrwulf
cb628b9119
Third pyramid capped. Identical shape to the risc0 fork (both are sha2-0.10 stacks): the hash oracle is the single monomorphic sha512_hash3(R, A, m) call, extraction runs --no-default-features. - gen/CurveSig: extracted verify glue, definitionally welded to the proven CurveField model (every curve and scalar call resolves to a certified definition; only the hash and wire formats are opaque). - Proofs/SigApexSpec.lean (unchanged from dalek): verify_loop_full with the standard three-axiom cone, and verify_accepts_iff — the verifier accepts IFF compress([s]B - [k]A) = R byte-for-byte. - check.sh Phase 3b enforces the apex cone to be EXACTLY [propext, Classical.choice, Quot.sound, ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new]. - extract.sh gains the reproducible CurveSig stanza (same recipe verified byte-exact on the risc0 fork this session). Full check.sh green: all standard certificates + the apex audit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
||
|---|---|---|
| .. | ||
| gen | ||
| Proofs | ||
| check-scalar.sh | ||
| check.sh | ||
| CurveField.llbc | ||
| CurveScalar.llbc | ||
| CurveSig.llbc | ||
| extract-scalar.sh | ||
| extract.sh | ||
| lean-guard | ||