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

#1823)

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

* Use Z.modulo to redefine SS' as suggested by Andres and simplify proofs

* Save some loc

* More comments

* Use sigma types for the Joye ladder

* Use more sigma types and clean up

* Joye ladder: refactor SS, TT

* Simplify HordP

* Use match-goal-with to make proof more readable

* Avoid the +1-1 when defining/using SS/TT as suggested by Andres

* Refactor the ladder

---------

Co-authored-by: Alix Trieu <[email protected]>
Co-authored-by: Andres Erbsen <[email protected]>

Makefile

@@ -88,15 +88,19 @@ EXCLUDED_VOFILES := $(filter $(EXCLUDE_PATTERN),$(VOFILES))
 # add files to this list to prevent them from being built as final
 # targets by the "lite" target
 LITE_UNMADE_VOFILES := src/Curves/Weierstrass/AffineProofs.vo \
-	src/Curves/Weierstrass/Jacobian.vo \
+	src/Curves/Weierstrass/Jacobian/Jacobian.vo \
+	src/Curves/Weierstrass/Jacobian/CoZ.vo \
+	src/Curves/Weierstrass/Jacobian/ScalarMult.vo \
 	src/Curves/Weierstrass/Projective.vo \
 	src/Rewriter/RulesGood.vo \
 	src/Rewriter/All.vo \
 	$(PERFTESTING_VO) \
 	$(EXCLUDED_VO)
 NOBIGMEM_UNMADE_VOFILES := \
 	src/Curves/Weierstrass/AffineProofs.vo \
-	src/Curves/Weierstrass/Jacobian.vo \
+	src/Curves/Weierstrass/Jacobian/Jacobian.vo \
+	src/Curves/Weierstrass/Jacobian/CoZ.vo \
+	src/Curves/Weierstrass/Jacobian/ScalarMult.vo \
 	src/Curves/Weierstrass/Projective.vo \
 	$(PERFTESTING_VO) \
 	$(EXCLUDED_VO)