zcash/ironwood carries Zcash/Circuits/Specs/CompEllipticExtras.lean (from zcash/ironwood#89), written in CompElliptic's own namespaces as explicit upstreaming candidates. Assessment:
Move as-is to CompElliptic/CurveForms/ShortWeierstrass.lean:
SWPoint.add_x / SWPoint.add_y — rfl projection lemmas about add; pure API completeness.y_eq_or_y_eq_neg_of_onCurve — two on-curve points sharing an x-coordinate have equal or opposite y. Generic for the y² = f(x) form; worth stating that way, since the property is not short-Weierstrass-specific.SWPoint.onCurve_of_ne_zero — a nonzero representable point is on the curve.SWPoint.eq_or_eq_neg_of_x_eq — nonzero points sharing an x-coordinate are equal or negated. The load-bearing one: it is the concrete form of the extractor ±-property (Extractor.toIVK_pm) that ironwood's key-binding instantiation at Pallas will need, so upstreaming serves both the circuits side and the key-binding instantiation.
Add for symmetry, from ironwood's Zcash/Circuits/Specs/Pallas.lean:
neg_five_not_isCube (no x with x³ = −5 over the Pallas base field) and no_onCurve_y_zero (no Pallas point with y = 0). CompElliptic already proves the Vesta-side twins, so symmetry argues for hosting the Pallas side in CompElliptic/Curves/Pasta.lean too. Relatedly, "no Pallas point has x = 0" (5 a non-square) is exactly the identity-point obligation recorded on Extractor.toIVK_pm's docstring in ironwood — hosting these facts upstream gives the key-binding instantiation and the circuits one shared source.
Not to move: the Fp/Fq abbreviations (PallasBaseField/PallasScalarField). These are Zcash-specific usage; consumers can keep them as local aliases.
🤖 Filed with Claude Code (Claude Fable 5).
zcash/ironwood carries
Zcash/Circuits/Specs/CompEllipticExtras.lean(from zcash/ironwood#89), written in CompElliptic's own namespaces as explicit upstreaming candidates. Assessment:Move as-is to
CompElliptic/CurveForms/ShortWeierstrass.lean:SWPoint.add_x/SWPoint.add_y—rflprojection lemmas aboutadd; pure API completeness.y_eq_or_y_eq_neg_of_onCurve— two on-curve points sharing an x-coordinate have equal or opposite y. Generic for they² = f(x)form; worth stating that way, since the property is not short-Weierstrass-specific.SWPoint.onCurve_of_ne_zero— a nonzero representable point is on the curve.SWPoint.eq_or_eq_neg_of_x_eq— nonzero points sharing an x-coordinate are equal or negated. The load-bearing one: it is the concrete form of the extractor ±-property (Extractor.toIVK_pm) that ironwood's key-binding instantiation at Pallas will need, so upstreaming serves both the circuits side and the key-binding instantiation.Add for symmetry, from ironwood's
Zcash/Circuits/Specs/Pallas.lean:neg_five_not_isCube(no x with x³ = −5 over the Pallas base field) andno_onCurve_y_zero(no Pallas point with y = 0). CompElliptic already proves the Vesta-side twins, so symmetry argues for hosting the Pallas side inCompElliptic/Curves/Pasta.leantoo. Relatedly, "no Pallas point has x = 0" (5 a non-square) is exactly the identity-point obligation recorded onExtractor.toIVK_pm's docstring in ironwood — hosting these facts upstream gives the key-binding instantiation and the circuits one shared source.Not to move: the
Fp/Fqabbreviations (PallasBaseField/PallasScalarField). These are Zcash-specific usage; consumers can keep them as local aliases.🤖 Filed with Claude Code (Claude Fable 5).