Hash-to-curve mappings, and groundwork for their analysis

[daira]

The deployed "Simplified SWU" hash-to-curve mappings used by Zcash's $\mathsf{GroupHash}$ for Pallas and Vesta, mirrored from protocol spec §5.4.9.8 — and the groundwork for their analysis.

The distribution of such a mapping is controlled by its character sums, and this PR isolates which part of that analysis is elementary and which part rests on top of deeper number theory. ("Mapping" is RFC 9380's term for these functions; design/naming-survey.md records why it is preferred over the papers' "encoding".)

Hashing/CharacterSum.lean — the elementary core

A mapping is odd when negating the input negates the output (f (-u) = -f u). For any odd mapping into a finite abelian group of odd order, this module proves: f 0 = 0 (IsOdd.map_zero); the value multiplicity is negation-symmetric (IsOdd.mult_neg); and for every nontrivial character, ∑ u, ψ (f u) = ∑ Q, (mult f Q − 1) · ψ Q (charSum_eq). The only nontrivial input is orthogonality (AddChar.sum_eq_zero_of_ne_one). The point of the identity: the sign convention drops out of the character sum entirely, leaving the sign-free covering-multiplicity deviation as the one object needing a bound.

Hashing/WellDistributed.lean — the deep input, quarantined

WeilBounded f C states the Weil bound in squared exact-arithmetic form (‖∑ u, ψ (f u)‖² ≤ C²·#F, avoiding Real.sqrt), and WeilBounded.deviation transports it through charSum_eq to the multiplicity deviation. The module docstring records why this bound cannot be reduced to the target curve's order — it is Hasse–Weil for the mapping's genus-8 covering curve, needed uniformly over roughly #G character twists, and the prime-order-witness-plus-fibre-bound method of CurveOrder is special to near-prime-order elliptic curves. Weil 1948 and Farashahi–Fouque–Shparlinski–Tibouchi–Voloch (eprint 2010/539) are cited for the forms intended to discharge it. FFSTV's Theorem 6 covers fields ≡ 3 (mod 4). The redo of its genus computation for the deployed generalized variant (the Pasta fields are ≡ 1 (mod 4)) does not seem to be covered in the literature.

Hashing/TwoTermUniformity.lean — the payoff of the WeilBounded hypothesis

pairCount f Q counts the input pairs with f u₀ + f u₁ = Q — the two-term output distribution. The chain mirrors the pipeline of a Discrete Fourier Transform:

• Orthogonality over the dual group (sum_addChar_apply, by Pontryagin duality — evaluation at a point is itself a character of the character group);
• The Fourier expansion (card_mul_pairCount — a self-convolution squares the spectrum);
• Parseval (card_mul_sum_sq_pairCount — the exact second moment, consuming no Weil bound);
• From WeilBounded: the summed squared deviation from uniform is at most #G·(#G − 1)·(C²·#F)² (sum_sq_dev_le). By Cauchy–Schwarz the squared L¹ probability deviation is then at most (#G − 1)·C⁴/#F² (sq_sum_abs_prob_dev_le) — statistical distance about C²/√q ≈ 2^{-116} at the deployed sizes, with C ≈ 52 the constant expected from FFSTV.

Hashing/SignedLift.lean — the sign convention, structurally

signedLift is the shape of RFC 9380's "if sgn0 u ≠ sgn0 y, set y = -y" step: select between the two points over an even abscissa by matching the root's sign to the input's. signedLift_neg proves the lift odd at every nonzero input, requiring the root chooser to be even only up to sign, which is what the deployed algorithm satisfies (its nonsquare branch carries a bare factor of u). The zero exception is explicit rather than assumed away: the deployed mapping is not odd at u = 0 (oddness there would force 2-torsion on an odd-order curve), zeroRepaired/isOdd_zeroRepaired give the literally-odd variant, and charSum_sub_zeroRepaired prices the repair exactly: the character sums differ by ψ (f 0) − 1, at most 2 in norm (norm_charSum_sub_zeroRepaired). That shift is the analysis's O(1) term, as an identity.

Hashing/SimplifiedSWU.lean — the deployed mapping, from the spec

sqrtRatio comes with its three lemmas: the Bool component is exactly squareness of the ratio; each branch returns a genuine root of its target; and the fallback default is a dead case, because a nonsquare times a nonsquare is a square (isSquare_mul_of_not_isSquare, via the quadratic character).

SSWUParams bundles the curve (with A·B ≠ 0), the nonsquare Z, the Tonelli–Shanks data, the nonsquare lam, the precomputed θ with θ²·lam = Z, the sign function, and RFC 9380's four criteria on Z; the on-curve proof consumes criteria 1 and 4.

SSWUParams.mapXY is the spec's thirteen steps verbatim, with the spec's own intermediate names. onCurve_mapXY proves every output is an affine curve point: the sign-matching step squares away; the square branch is the definition of U; and the nonsquare branch closes by θ²·lam = Z together with the SSWU identity Zuu³·U = g(x2num/xdiv)·xdiv³. Criterion 4 makes the exceptional ta = 0 case unreachable in that branch.

Isogenies/ThreeIsogeny.lean — Vélu's formulae, symbolically

The deployed mapping reaches Pallas and Vesta through auxiliary curves, each 3-isogenous to its target, because simplified SWU needs A ≠ 0 and the Pasta curves have A = 0. This module formalizes the method behind the specified isogeny maps, rather than checking their coefficients as two curve-sized literal identities. ThreeIsogeny takes a kernel abscissa and a normalizing scalar, and derives the rational maps and the codomain from Vélu's formulae — the method by which Sage's rational_maps() produced the maps that the specification adopted. The on-curve proof is a single polynomial identity modulo the degree-3 division polynomial, discharged by linear_combination with a cofactor computed in Sage (the script is recorded next to the proof). Rational points never meet the kernel fibre, because the kernel ordinate is irrational; and the map commutes with negation, which the analysis will consume as oddness. Cited: Vélu (1971), and Galbraith's "Mathematics of Public Key Cryptography", Theorem 25.1.6.

Curves/IsoPasta.lean — the derived and specified isogenies

Each deployed isogeny is stated twice —as derived using Vélu's formulae, and as the explicit mapping given in the protocol specification— and the statements proved equal. Pallas.iso and Vesta.iso are the Vélu derivations: the kernel abscissa x₀ = -b₁/2 and the scalar s, recovered from the specified coefficients, with every obligation a numeral check — and both kernel ordinates satisfy y₀² = 5, so kernel irrationality is exactly five_not_isSquare. Pallas.iso_map and Vesta.iso_map quote the protocol specification's hex constants verbatim, as CP_1, ..., CP_13 and CV_1, ..., CV_13 —checked against the decimal constants of hashtocurve.sage— and iso_map_eq proves each equal to its derivation (one decide per coefficient, assembled by linear_combination). onCurve_iso_map is the payoff: points of the iso-curves land on their targets.

Curves/PastaOrder.lean — the iso-curve orders

iso-Pallas and iso-Vesta have the same orders as their targets, pinned by the same witness route: a prime-order witness point (at x = 1 and x = 4), its native_decide torsion certificate, and the elementary fibre bound. The one new ingredient is iso-Vesta's 2-torsion exclusion: its curve cubic has a linear term, so Vesta's cube-residue argument does not apply — and none is needed, because a y = 0 point of iso-Vesta would map to a y = 0 point of Vesta under the isogeny (ThreeIsogeny.no_y_zero_of_codomain), and Vesta has none. The census gains the two certificates and the two orders under +native, and the isogeny layer's headline theorems under the standard tier.

Isogenies/ThreeIsogeny.lean, continued — bijectivity on rational points, by counting

Injectivity consumes no homomorphism property: an abscissa collision would make the second abscissa a rational root of a quadratic whose discriminant is the squared difference of the abscissas of the two kernel translates — 16·y₀²·y₁² up to a square factor — so a collision exhibits the nonsquare y₀² as a square, contradicting kernel_irrational (abscissa_inj, with Sage-computed cofactors recorded next to the proof). Equal images over one abscissa force equal ordinates, because the alternative makes the image rational 2-torsion (map_injective; the codomain-side exclusion for Pallas is the new Pallas.no_onCurve_y_zero, mirroring Vesta's). ThreeIsogeny.map packages the affine map as a function on curve points, and counting upgrades injectivity to bijectivity when the two groups have equal order (map_bijective); Pallas.iso_map_bijective and Vesta.iso_map_bijective instantiate this with the iso-curve orders.

Isogenies/VeluCertificates.lean — the homomorphism identities, as certificates

The homomorphism property of the isogeny reduces to two polynomial identities: the abscissa of the image of a sum agrees with the abscissa the codomain group law computes from the images, once for the chord case (distinct abscissas) and once for the tangent case (doubling). This module proves both, each as a single linear_combination certificate, generic over any commutative ring. The statements are phrased in kernel-centred coordinates —the translation putting the kernel abscissa at the origin, under which Vélu's numerators are short and the division-polynomial relation collapses to the two-term p² = 12·x₀·g₀— and, for the chord, in symmetric variables for the two summands. Together these shrink the chord certificate roughly sevenfold, which is the difference between an infeasible elaboration and one that finishes in under a minute. The module doc explains the coordinates and defines the working vocabulary (certificate, cofactor, atom, mass). The cofactors are computed by scripts/gen_velu_certificates.sage, which re-verifies the emitted identity by exact polynomial expansion before writing the Lean text, and Lean's ring normalization re-checks the same identity on every build — so no Gröbner-basis output is trusted. CI also re-runs the generator and fails if the regenerated file differs from the committed one, with Sage pinned to the version whose bundled Singular produced the committed cofactors (lift output can differ between versions even when both are valid). ThreeIsogeny.map_zero (the identity maps to the identity) lands alongside, with references for the standard fact that an isogeny is automatically a group homomorphism (Galbraith §25.1; Silverman, Theorem III.4.8). The generated section also carries the support lemmas the wrapper proofs consume: the ψ₃ instances, the atom semantics, and the final corrections, in the same coordinates, each verified the same way.

Isogenies/Homomorphism.lean — the homomorphism property, proved

ThreeIsogeny.map is a group homomorphism on rational points (map_add). That an isogeny is automatically a group homomorphism is standard (Galbraith §25.1; Silverman, Theorem III.4.8), but Mathlib has no isogeny theory to supply it, and this development does not rely on the general theorem: the property is proved directly for the maps in use. The proof is layered. chord_x_compat and tangent_x_compat consume the certificates through the generated support lemmas —with the Vieta eliminations' saturation factors and the 2-power clearings cancelled in the wrappers— and say that the image of a sum's third point has exactly the abscissa the codomain group law computes from the two image points. The point level assembles the branches of add (map_add_x), upgrades abscissa agreement to agreement up to sign (map_add_pm; on-curve points sharing an abscissa are equal or negatives), and resolves the sign by group algebra: the ambiguous cases force 2-torsion on the codomain, which the existing no-y = 0 hypothesis excludes. Pallas.iso_map_add and Vesta.iso_map_add instantiate it with every hypothesis discharged by the 2-torsion exclusions, so the homomorphism facts sit in the census's standard tier, consuming no native_decide.

Fields/Sqrt.lean — a valid rootOfUnity is a nonsquare

TonelliShanks.rootOfUnity_not_isSquare: the root of unity of a valid instance has full 2-power order, so its Euler power factors as (rootOfUnity^(2^(twoAdicity-1)))^oddPart = (-1)^oddPart = -1, whereas Euler's criterion gives 1 for a nonzero square. This discharges the nonsquare obligation of any deployment that reuses rootOfUnity as an auxiliary nonsquare —as the deployed parameters below do— with no per-field computation.

Hashing/PastaSSWU.lean — the deployed parameters

Pallas.sswu and Vesta.sswu instantiate SSWUParams with the deployed parameters: Z = -13, parity sgn0, and the square-root split over lam := rootOfUnity, matching pasta_curves' ROOT_OF_UNITY so that intermediate values can be compared directly. The θ values are quoted from pasta_curves' THETA constants (revision-pinned in the module doc); θ_spec pins each to ±THETA, and decide-checked examples equate the hex literals to the reference's little-endian from_raw limbs, verbatim. The criterion-4 obligations are discharged by computed square-root witnesses, with the divisions cleared by field_simp before decide (modular inversion under kernel evaluation is infeasible, while the division-free identities elaborate in a few hundred heartbeats).

Hashing/PastaSSWU.lean — pinned test fixtures

Sixteen native_decide fixtures pin the instances against the references. Per field, mapXY is pinned at hashtocurve.sage's self-test inputs (u = 0 exercises the exceptional ta = 0 branch) and at the two hash_to_field outputs of its hash-to-curve test vector, which take opposite IsSquare branches. The composed construction (mapHashOutputsToCurve) is pinned against the zcash-test-vectors group-hash vector for Pallas; against hashtocurve.sage's Vesta vector, whose shape is what a zcash-test-vectors Vesta vector is expected to take (zcash/zcash-test-vectors#132); and against the Halo 2 fixed-generator derivation for Vesta, at indices 0 and 2^11 - 1 plus W and U. One further example checks the Vesta vector's Jacobian-to-affine conversion, with the script's printed output quoted verbatim, so the pinned point can be compared directly against it. Filed alongside: zcash/pasta#6 and zcash/zips#1349 for small reference bugs surfaced by this work, and #24 to track a direct comparison against the Rust pasta_curves implementation.

Hashing/SignedLift.lean and Hashing/SimplifiedSWU.lean, continued — the mapping is odd

signedLift now takes a candidate point map F → SWPoint E and re-derives each output's sign from the input's, so validity rides inside SWPoint and oddness needs a single hypothesis: signedLift_neg consumes m (-u) = ±(m u). On the SSWU side, mapXY is split into mapXYUpToSign —the spec's steps up to the candidate ordinate, written once— and the sign-matching step, so their composition is step-for-step the spec's list. candidateMap packages the candidate as a curve point (valid_pre), map_eq_signedLift factors the mapping through signedLift, and map_neg gives oddness away from 0; the zero exception is exactly the one zeroRepaired prices.

Hashing/PastaSSWU.lean, continued — the composed map_to_curve

mapToCurve —simplified SWU, then the isogeny— is the deployed map_to_curve for each curve. mapToCurve_neg composes SSWUParams.map_neg with ThreeIsogeny.map_neg, and isOdd_zeroRepaired_mapToCurve is the literally-odd form the character-sum analysis consumes. charSum_mapToCurve_sub_zeroRepaired and its norm form instantiate the repair pricing at the deployed mapping, so conclusions about the repaired variant carry back at an exact O(1) cost. The census records the isOdd and transport theorems under +native, witnessed by the Tonelli–Shanks instances — their only native leaves.

mapHashOutputsToCurve is the deployed construction after hash_to_field: add on the iso-curve, apply the isogeny once, as the spec and hashtocurve.sage do. The name is deliberately not hash_to_curve — RFC 9380's includes hash_to_field, and the RFC intentionally leaves this composition unnamed, since it is cryptographically hazardous unless composed with hash_to_field. RFC 9380 §6.6.3 licenses the one-evaluation order by exactly the homomorphism this PR proves; mapHashOutputsToCurve_eq consumes map_add/iso_map_add to agree with the per-point order that zcash-test-vectors and pasta_curves use, and the composed fixtures pin mapHashOutputsToCurve itself.

Hashing/SimplifiedSWU.lean and Fields/Residue.lean, continued — all four RFC criteria certified

SSWUParams initially recorded only the two Z criteria the on-curve proof consumes, so it admitted instances that RFC 9380 does not (over GF(7), y² = x³ + x + 3 with Z = -1). The record now carries all four: crit2 (Z ≠ -1) and crit3 (g(X) - Z has no roots, which for a cubic is the RFC's irreducibility condition). crit3 is discharged by a new lemma, cubic_no_root_of_resolvent_noncube: Cardano's method run backwards as a certificate — a square root s of the resolvent discriminant together with a non-cube resolvent root w rules out all roots of x³ + A·x + q at once, entirely within F. The per-curve s and w were computed in Sagemath; the arithmetic side conditions are checked by decide, and the non-cube certificates by one fast modular exponentiation each (not_exists_pow_eq_of_pow_ne_one). Criteria 2 and 3 turn out to be patent-avoidance constraints rather than mathematical requirements — they entered in draft 5 of the RFC to keep the mapping outside US patents 8,718,276 and 8,712,038 (Icart et al., expiring June 2030) — and the SimplifiedSWU module documentation now records that provenance, which is why no proof consumes them.

Deferred

• Indifferentiability from a random oracle with respect to an abstract hash_to_field(·, 2) (Brier et al.'s Theorem 1 with its explicit simulator), consuming TwoTermUniformity as the regularity half, is tracked as Justify indifferentiability of mapHashOutputsToCurve from an RO wrt the hash_to_field outputs #25.

🤖 Claude Fable 5

[daira]

Self-reACK

[TalDerei]

sparse pass, ACK! can follow-up with a deeper analysis

[TalDerei]

Deeper pass at 05c61008.

I did not find a core implementation-correctness bug in the deployed SSWU/isogeny path, or a Lean/kernel soundness hole. The formulas and constants match the protocol and pinned pasta_curves implementation; I also independently checked the new native order witnesses, roots-of-unity/θ identities, concrete RFC criteria, supplied SSWU fixtures, and sampled isogeny identities.

I did find these scope/specification gaps:

1. SSWUParams is an algebraic-correctness record, not yet a complete RFC 9380 SSWU-parameter certificate. It encodes that Z is nonsquare and criterion 4, but not Z ≠ -1 or irreducibility of g(X) - Z (criteria 2 and 3). This is a real distinction: the current record admits non-RFC instances (for example over F₇, y² = x³ + x + 3, Z = -1). The concrete Pasta instances do satisfy all four criteria, so this is not a deployed-output bug. I suggest either adding those obligations or stating explicitly that SSWUParams certifies on-curve correctness only.

2. The ≈ 2^-116 deployed uniformity figure remains conditional. Every endpoint in TwoTermUniformity consumes WeilBounded f C; there is no concrete WeilBounded theorem for the deployed mapping, the module says the generalized Pasta redo is unwritten, and the zero-repaired-to-deployed transport is not composed. That is a clean external assumption boundary, but the numerical claim should be labelled conditional.

3. WellDistributed.lean currently says well-distributedness makes the construction statistically close to uniform “and hence indifferentiable.” Statistical regularity is only one half of the argument; the efficient preimage simulator and hash_to_field composition are still deferred in Justify indifferentiability of mapHashOutputsToCurve from an RO wrt the hash_to_field outputs #25. I’d say “a regularity ingredient toward indifferentiability” here.

The upstream y/y′ typo is already tracked in zcash/zips#1349, and this PR implements the intended y′ behavior correctly.

So my scope verdict is: sound as deployed mapping plus conditional groundwork, but not yet an end-to-end proof of deployed random-oracle security.

with the help of claude

[TalDerei]

still can't believe it implemented this so well...

[daira]

there is no concrete WeilBounded theorem for the deployed mapping

Fable claimed that proving WeilBounded would be weeks of work, and I believe it. Not only do I not know most of the required mathematics; Mathlib doesn't have a bunch of needed infrastructure. It was kind-of a miracle that we were able to prove the homomorphism without that infrastructure: the size of the equation system should have been infeasible to prove using a linear_combination certificate. It was for the first few tries, until we found the kernel-centred coordinate trick.

As the comments in WellDistributed.lean explain, WeilBounded is actually necessary: well-distributedness needs the uniform bound over every nontrivial character. That's deep number theory and algebraic geometry. It's the "Riemann hypothesis for (a subset of) algebraic varieties", a special case of the Generalized Riemann Hypothesis which is one of the hardest believed-to-be-true-but-unsolved problems in mathematics. The algebraic variety case is solved and there's a lot of material explaining pencil-and-paper proofs, so I may attempt to tilt at this windmill when I have time, just to learn new math! But I'm not going to block this PR on it :-)

For the assurance we need to justify that the hash-to-curve is well-distributed, we only need to know that we've correctly stated the Weil bound. That is something for which we can just check the relevant literature (and I will).

[TalDerei]

kernel-centred coordinate trick.

can we document this somewhere? these kinds of techniques are useful to have in the backpocket and externalize.

[daira]

Thanks — all three points led to changes.

Point 1 is addressed in b718fac and its follow-ups: SSWUParams now carries crit2 (Z ≠ -1) and crit3 (g(X) - Z has no roots, which for a cubic is the RFC's irreducibility), so your F₇ instance is no longer constructible. crit3 is discharged by a Cardano-resolvent certificate (Fields.cubic_no_root_of_resolvent_noncube). A square root s of the resolvent discriminant plus a non-cube resolvent root w, computed in Sagemath and checked by decide, rule out all roots at once.

Digging into why the RFC has criteria 2 and 3 at all turned up something worth recording: they are patent-avoidance constraints, not mathematical requirements. They entered in draft 5 (cfrg/draft-irtf-cfrg-hash-to-curve#172) to keep the mapping outside US patents 8,718,276 and 8,712,038 (Icart et al., expiring June 2030). The original simplified SWU of Brier et al., and Wahby–Boneh's own ξ for BLS12-381, are literally the Z = -1 case the criteria forbid. The SimplifiedSWU module doc now records this, which is also why no proof consumes those two criteria.

Point 2: you were right that the zero-repaired-to-deployed transport was not composed — that lemma existed only generically. The deployed and repaired character sums differ by exactly ψ (f 0) - 1, at most 2 in norm; that is now instantiated at the deployed mapToCurve for each curve, with the norm forms in the census. The ≈ 2^{-116} figures now state their reliance on the WeilBounded hypothesis. The "routine but unwritten redo" sentence now clarifies that the ≡ 1 (mod 4) case needed by the Pasta curves "does not seem to be covered in the literature". Separately, WeilBounded is an external input to the formalization; see the earlier comment.

Point 3: agreed, and reworded — statistical regularity is now described as an ingredient of indifferentiability, with the efficient preimage simulator tracked in #25. One boundary note: the hash_to_field composition is intentionally out of scope rather than deferred — we treat hash_to_field as a random oracle, so the formalization depends only on its type, not on what it concretely is.

Posted with the assistance of Claude Fable 5

[daira]

Self-ACK 5c7beec

[daira]

can we document this somewhere? these kinds of techniques are useful to have in the backpocket and externalize.

It's documented in VeluCertificates.lean.