Joye double-add ladder for short Weierstrass curves in co-Z arithmetic#1823

Merged

andres-erbsen merged 11 commits intomit-plv:masterfrom atrieu:JoyeCoZ

Apr 2, 2024

+1,689-3

Commits on Apr 1, 2024

Joye double-add ladder for short Weierstrass curves in co-Z arithmetic

atrieu
authored and
andres-erbsen
committed
Use Z.modulo to redefine SS' as suggested by Andres and simplify proofs

atrieu
authored and
andres-erbsen
committed
Save some loc

atrieu
authored and
andres-erbsen
committed
More comments

atrieu
authored and
andres-erbsen
committed
Use sigma types for the Joye ladder

atrieu
authored and
andres-erbsen
committed
Use more sigma types and clean up

atrieu
authored and
andres-erbsen
committed
Joye ladder: refactor SS, TT
andres-erbsen
committed
Simplify HordP

atrieu
authored and
andres-erbsen
committed
Use match-goal-with to make proof more readable

atrieu
authored and
andres-erbsen
committed
Avoid the +1-1 when defining/using SS/TT as suggested by Andres

atrieu
authored and
andres-erbsen
committed
Refactor the ladder

atrieu
authored and
andres-erbsen
committed