Merge pull request privacy-scaling-explorations#146 from input-output…

…-hk/dev-feature/53-gen-eccc

Implement Ecc Chip for Pluto ... and Vesta and Eris

# Project Context

This issue corresponds to the Milestone 3 updated SOW task "New: Extend EccChip to support Pluto". There is no corresponding GitHub issue, since this is the Pluto/Eris analog of supporting Pallas, which was the starting state. However, the work for this issue overlaps significantly with SOW task "zcash#578: Extend EccChip to support ~~Vesta~~ Eris" ([zcash#578](zcash#578)), since it seems easiest to just generalize to all curves at the same time. So, while we only need to ensure Pluto support for Milestone 3, the strategy we're using also gives Eris and Vesta support "for free".

This builds on top of privacy-scaling-explorations#145 directly, depends directly on privacy-scaling-explorations#143 and privacy-scaling-explorations#144 as well, and is the culmination of generalization work that started at a lower level with privacy-scaling-explorations#101, privacy-scaling-explorations#107, and privacy-scaling-explorations#114. 

The corresponding Galois internal issue is [Galois#53](https://gitlab-ext.galois.com/iog-midnight/halo2/-/issues/53).

# Issue Description

Generalize the Ecc Chip to arbitrary curves, allowing any assumptions that apply to all of Pallas, Vesta, Pluto, and Eris. This work is broken up into several subtasks, concerned with updating the major components of the Ecc Chip ([vbsm](privacy-scaling-explorations#143), [fbsm](privacy-scaling-explorations#145), and [point witnessing](privacy-scaling-explorations#144)), along with the final work here of updating the full Ecc Chip to use all of the updated components, have tests for all curves, and provide instantiations for all curves.

Behind the scenes there are various traits associated with the vbsm and fbsm generalizations, but the final Ecc Chip interface exposes `EccCurve` and `EccField` as the traits required for curves and fields used with Ecc Chip (and of course these traits are implemented for Pallas, Vesta, Pluto, Eris, and their fields).

book/src/design/gadgets/ecc.md

@@ -2,25 +2,22 @@
 
 ## `EccChip`
 
-`halo2_gadgets` provides a chip that implements `EccInstructions` using 10 advice columns.
-The chip is currently restricted to the Pallas curve, but will be extended to support the
-[Vesta curve](https://github.com/zcash/halo2/issues/578) in the near future.
+The `halo2_gadgets` package provides a chip that implements `ecc::EccInstructions` using 10 advice columns.
+The chip supports the [Pallas, Vesta](https://github.com/zcash/pasta), [Pluto, and Eris](https://github.com/daira/pluto-eris) curves.
 
 ### Chip assumptions
 
+Let $C$ be one of Pallas, Vesta, Pluto, or Eris, and let $\mathbb{F}_b$ and $\mathbb{F}_s$ be $C$'s base and scalar fields, respectively. The points of $C$ are the solutions over $\mathbb{F}_b$ of the Short Weierstrass equation $y^s = x^3 + \mathfrak{a}x + \mathfrak{b}$, where $\mathfrak{a} = 0$ for all four curves, $\mathfrak{b} = 5$ for Pallas and Vesta, and $\mathfrak{b} = 57$ for Pluto and Eris.
+
 A non-exhaustive list of assumptions made by `EccChip`:
-- $0$ is not an $x$-coordinate of a valid point on the curve.
-  - Holds for Pallas because $b$ is not square in $\mathbb{F}_q$.
-- $0$ is not a $y$-coordinate of a valid point on the curve.
-  - Holds for Pallas because $-b$ is not a cube in $\mathbb{F}_q$.
-  - The sage script checks this condition for all four curves (Pallas, Vesta,
-    Pluto, Eris)
-- The base and scalar fields of the Ecc Chip curves have 2-adicity at least 3,
-  i.e. $2^3 \mid p - 1$ and $2^3 \mid q - 1$.
-  - Holds for Pallas, Vesta, Pluto, and Eris, which all have 2-adicity of 32.
-- The curve equation is $y^2 = x^3 + b$, i.e. it's an instance of the Short
-  Weierstrass form $y^2 = x^3 + ax + b$, with $a = 0$.
-  - The [point doubling gadget](ecc/doubling.html#point-doubling.md) is specialized to this $a = 0$ case.
+- Zero is not the $x$-coordinate of a point on the curve. Equivalently, $\mathfrak{b}$ is not a square in $\mathbb{F}_b$.
+- Zero is not the $y$-coordinate of a point on the curve. Equivalently, $-\mathfrak{b}$ is not a cube in $\mathbb{F}_b$. Together this assumption and the last assumption allow us to represent the identity ("point at infinity") as $(0, 0),$ and s.t. only knowing one coordinate suffices.
+- The base field $\mathbb{F}_b$ and scalar field $\mathbb{F}_s$ have 2-adicity at least 3, i.e. $2^3 \mid b - 1$ and $2^3 \mid s - 1$. In fact, Pallas, Vesta, Pluto, and Eris all have 2-adicity of 32, which is relevant to efficient FFTs.
+- The curve equation is $y^2 = x^3 + \mathfrak{b}$, i.e. it's an instance of the Short Weierstrass form $y^2 = x^3 + \mathfrak{a}x + \mathfrak{b}$, with $\mathfrak{a} = 0$. The [point doubling gadget](ecc/doubling.html#point-doubling.md) is specialized to this $\mathfrak{a} = 0$ case.
+
+The sage script `halo2_gadgets/scripts/full_width_variable_base_scalar_mul.sage`
+checks the first three conditions above, and various other more technical
+conditions related to [variable-base scalar multiplication](ecc/var-base-scalar-mul.html), for Pallas, Vesta, Pluto, and Eris. The fourth condition is asserted in the code.
 
 ### Layout
 

halo2_gadgets/CHANGELOG.md

@@ -17,6 +17,7 @@ and this project adheres to Rust's notion of
   - `copy_short_check`: replaced by `pow2_range_check`
 - Added APIs in `halo2_gadgets::utilities::lookup_range_check::LookupRangeCheckConfig`:
   - `pow2_range_check`: a range check for a power-of-two range.
+- Remove `BaseFitsInScalarInstructions` trait. It's no longer needed, as its methods have been moved into the more general `EccInstructions` trait.
 
 ## [0.2.0] - 2022-06-23
 ### Added

halo2_gadgets/scripts/full_width_variable_base_scalar_mul.sage

@@ -49,6 +49,7 @@ def field_checks(p, q, a):
     Additional conditions that apply to other parts of Ecc Chip, but not nec
     scalar mul in particular:
     - There is no point with x or y coord equal to 0.
+    - The base field has 2-adicity at least 32.
     """
     assert q > p
 
@@ -82,6 +83,9 @@ def field_checks(p, q, a):
     assert Fp(a).nth_root(2, all=True) == [], "x can't be 0"
     assert Fp(-a).nth_root(3, all=True) == [], "y can't be 0"
 
+    # Check that the base field has 2-adicity at least 32.
+    assert (2^32).divides(p-1), "p must have 2-adicity at least 32"
+
     print("p:", bin(p))
     print("q:", bin(q))