add_incomplete::tests: Constrain output of `P + Q` test.

Also minor docfixes and refactors.

Co-authored-by: Jack Grigg <jack@electriccoin.co>
This commit is contained in:
therealyingtong 2021-06-14 00:19:21 +08:00
parent 7341996d2c
commit 8a8df98a50
4 changed files with 32 additions and 16 deletions

View File

@ -470,7 +470,7 @@ mod tests {
// Test complete addition
{
super::chip::add::tests::test_add(
chip,
chip.clone(),
layouter.namespace(|| "complete addition"),
&zero,
p_val,
@ -484,9 +484,12 @@ mod tests {
// Test incomplete addition
{
super::chip::add_incomplete::tests::test_add_incomplete(
chip,
layouter.namespace(|| "incomplete addition"),
&zero,
p_val,
&p,
q_val,
&q,
&p_neg,
)?;
@ -498,7 +501,7 @@ mod tests {
#[test]
fn ecc() {
let k = 5;
let k = 6;
let circuit = MyCircuit {};
let prover = MockProver::run(k, &circuit, vec![]).unwrap();
assert_eq!(prover.verify(), Ok(()))

View File

@ -409,13 +409,13 @@ pub mod tests {
// Check complete addition P + (-P)
{
let result = p.add(layouter.namespace(|| "P + (-P)"), p_neg)?;
result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
result.constrain_equal(layouter.namespace(|| "P + (-P) = 𝒪"), zero)?;
}
// Check complete addition 𝒪 + 𝒪
{
let result = zero.add(layouter.namespace(|| "𝒪 + 𝒪"), zero)?;
result.constrain_equal(layouter.namespace(|| "P + (-P) = 0"), zero)?;
result.constrain_equal(layouter.namespace(|| "𝒪 + 𝒪 = 𝒪"), zero)?;
}
// Check P + Q

View File

@ -53,7 +53,7 @@ impl Config {
(x_r.clone() + x_q.clone() + x_p.clone())
* (x_p.clone() - x_q.clone())
* (x_p.clone() - x_q.clone())
- (y_p.clone() - y_q.clone()) * (y_p.clone() - y_q.clone())
- (y_p.clone() - y_q.clone()).square()
};
// (y_r + y_q)(x_p x_q) (y_p y_q)(x_q x_r) = 0
@ -143,22 +143,35 @@ impl Config {
#[cfg(test)]
pub mod tests {
use halo2::{arithmetic::CurveAffine, circuit::Layouter, plonk::Error};
use group::Curve;
use halo2::{circuit::Layouter, plonk::Error};
use pasta_curves::pallas;
use crate::circuit::gadget::ecc::{EccInstructions, Point};
#[allow(clippy::too_many_arguments)]
pub fn test_add_incomplete<
C: CurveAffine,
EccChip: EccInstructions<C> + Clone + Eq + std::fmt::Debug,
EccChip: EccInstructions<pallas::Affine> + Clone + Eq + std::fmt::Debug,
>(
mut layouter: impl Layouter<C::Base>,
zero: &Point<C, EccChip>,
p: &Point<C, EccChip>,
q: &Point<C, EccChip>,
p_neg: &Point<C, EccChip>,
chip: EccChip,
mut layouter: impl Layouter<pallas::Base>,
zero: &Point<pallas::Affine, EccChip>,
p_val: pallas::Affine,
p: &Point<pallas::Affine, EccChip>,
q_val: pallas::Affine,
q: &Point<pallas::Affine, EccChip>,
p_neg: &Point<pallas::Affine, EccChip>,
) -> Result<(), Error> {
// P + Q
p.add_incomplete(layouter.namespace(|| "P + Q"), q)?;
{
let result = p.add_incomplete(layouter.namespace(|| "P + Q"), q)?;
let witnessed_result = Point::new(
chip,
layouter.namespace(|| "witnessed P + Q"),
Some((p_val + q_val).to_affine()),
)?;
result.constrain_equal(layouter.namespace(|| "constrain P + Q"), &witnessed_result)?;
}
// P + P should return an error
p.add_incomplete(layouter.namespace(|| "P + P"), p)

View File

@ -40,8 +40,8 @@ impl Config {
let y = meta.query_advice(self.y, Rotation::cur());
// y^2 = x^3 + b
let curve_eqn = y.clone() * y.clone()
- (x.clone() * x.clone() * x.clone())
let curve_eqn = y.clone().square()
- (x.clone().square() * x.clone())
- Expression::Constant(pallas::Affine::b());
vec![