Hashing/PastaSSWU.lean pins mapXY against hashtocurve.sage fixtures and ties the θ constants to pasta_curves' THETA limbs; fixtures against the zcash-test-vectors group-hash vectors are the next step on the hashing branch. Together those give transitive coverage CompElliptic ↔ zcash-test-vectors ↔ pasta_curves, since the two references are tested against each other.
A direct comparison against the Rust pasta_curves implementation (its map_to_curve_simple_swu path and hash-to-curve internals, e.g. via a small Rust harness printing intermediate values for the same inputs) would close the triangle without relying on the intermediate.
🤖 Claude Fable 5
Hashing/PastaSSWU.leanpinsmapXYagainsthashtocurve.sagefixtures and ties the θ constants topasta_curves'THETAlimbs; fixtures against the zcash-test-vectors group-hash vectors are the next step on the hashing branch. Together those give transitive coverage CompElliptic ↔ zcash-test-vectors ↔ pasta_curves, since the two references are tested against each other.A direct comparison against the Rust
pasta_curvesimplementation (itsmap_to_curve_simple_swupath and hash-to-curve internals, e.g. via a small Rust harness printing intermediate values for the same inputs) would close the triangle without relying on the intermediate.🤖 Claude Fable 5