mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-03 19:53:45 +00:00
mrwulf
07b0f46018
Full replication of dalek's phase 2 in one increment - the five files ported with only the v4 deltas (to_bytes -> as_bytes on both serializers, byte-identical bodies verified; compress inlines the affine conversion; recompute has ONE sha512_hash3 oracle bind instead of five, so the inversion is a single bind_ok_inv before the proven tail). Every proof compiled FIRST TRY after the mechanical renames. - Proofs/ToBytesMath + ToBytesSpec: field as_bytes canonicity. - Proofs/ScalarPackSpec: scalar pack + canonical hash-to-scalar entry. - Proofs/CompressSpec: ed_compress_spec - compress emits the canonical encoding of the denoted affine point. - Proofs/PointLiftSpec: dsm dispatch transfer, byte-comparison bridge, recompute inversion, and THE HALF-LIFT verify_accepts_iff_point: accept IFF the signature's R bytes are the canonical encoding of the recomputed [k](-A) + [s]B (valid, on-curve, certified model). check.sh: five new certificates (exact standard three) and Phase 3b now enforces the hash3 + wire-format boundary on BOTH apex and half-lift. 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 | ||