Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: safe ecc_sum and tests #244

Merged
merged 6 commits into from
Apr 9, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions halo2-base/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,9 @@ env_logger = "0.10.0"
proptest = "1.1.0"
# native poseidon for testing
pse-poseidon = { git = "https://github.com/axiom-crypto/pse-poseidon.git" }
clap = "=4.4" # fix clap version to prevent requiring rustc 1.74
clap_builder = "=4.4"
clap_lex = "=0.6.0"

# memory allocation
[target.'cfg(not(target_env = "msvc"))'.dependencies]
Expand Down
3 changes: 3 additions & 0 deletions halo2-ecc/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,9 @@ criterion-macro = "0.4"
halo2-base = { path = "../halo2-base", default-features = false, features = ["test-utils"] }
test-log = "0.2.12"
env_logger = "0.10.0"
clap = "=4.4" # fix clap version to prevent requiring rustc 1.74
clap_builder = "=4.4"
clap_lex = "=0.6.0"

[features]
default = ["jemallocator", "halo2-axiom", "display"]
Expand Down
57 changes: 56 additions & 1 deletion halo2-ecc/src/bn254/tests/ec_add.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ fn g2_add_test<F: BigPrimeField>(
let points =
_points.iter().map(|pt| g2_chip.assign_point_unchecked(ctx, *pt)).collect::<Vec<_>>();

let acc = g2_chip.sum::<G2Affine>(ctx, points);
let acc = g2_chip.sum_unsafe::<G2Affine>(ctx, points);

let answer = _points.iter().fold(G2Affine::identity(), |a, b| (a + b).to_affine());
let x = fp2_chip.get_assigned_value(&acc.x.into());
Expand All @@ -48,6 +48,27 @@ fn g2_add_test<F: BigPrimeField>(
assert_eq!(answer.y, y);
}

fn g1_sum_safe_test<F: BigPrimeField>(
ctx: &mut Context<F>,
range: &RangeChip<F>,
params: CircuitParams,
_points: Vec<G1Affine>,
) {
let fp_chip = FpChip::<F>::new(range, params.limb_bits, params.num_limbs);
let g1_chip = EccChip::new(&fp_chip);

let points =
_points.iter().map(|pt| g1_chip.assign_point_unchecked(ctx, *pt)).collect::<Vec<_>>();

let acc = g1_chip.sum::<G1Affine>(ctx, points);

let answer = _points.iter().fold(G1Affine::identity(), |a, b| (a + b).to_affine());
let x = fp_chip.get_assigned_value(&acc.x.into());
let y = fp_chip.get_assigned_value(&acc.y.into());
assert_eq!(answer.x, x);
assert_eq!(answer.y, y);
}

#[test]
fn test_ec_add() {
let path = "configs/bn254/ec_add_circuit.config";
Expand All @@ -65,6 +86,40 @@ fn test_ec_add() {
.run(|ctx, range| g2_add_test(ctx, range, params, points));
}

#[test]
fn test_ec_sum_safe() {
let path = "configs/bn254/ec_add_circuit.config";
let params: CircuitParams = serde_json::from_reader(
File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")),
)
.unwrap();

let k = params.degree;
let points = (0..params.batch_size).map(|_| G1Affine::random(OsRng)).collect_vec();

base_test()
.k(k)
.lookup_bits(params.lookup_bits)
.run(|ctx, range| g1_sum_safe_test(ctx, range, params, points));
}

#[test]
fn test_ec_zero_sum_safe() {
let path = "configs/bn254/ec_add_circuit.config";
let params: CircuitParams = serde_json::from_reader(
File::open(path).unwrap_or_else(|e| panic!("{path} does not exist: {e:?}")),
)
.unwrap();

let k = params.degree;
let points = (0..params.batch_size).map(|_| G1Affine::identity()).collect_vec();

base_test()
.k(k)
.lookup_bits(params.lookup_bits)
.run(|ctx, range| g1_sum_safe_test(ctx, range, params, points));
}

#[test]
fn bench_ec_add() -> Result<(), Box<dyn std::error::Error>> {
let config_path = "configs/bn254/bench_ec_add.config";
Expand Down
2 changes: 1 addition & 1 deletion halo2-ecc/src/ecc/ecdsa.rs
Original file line number Diff line number Diff line change
Expand Up @@ -71,7 +71,7 @@ where

// compute (x1, y1) = u1 * G + u2 * pubkey and check (r mod n) == x1 as integers
// because it is possible for u1 * G == u2 * pubkey, we must use `EccChip::sum`
let sum = chip.sum::<GA>(ctx, [u1_mul, u2_mul]);
let sum = chip.sum_unsafe::<GA>(ctx, [u1_mul, u2_mul]);
// WARNING: For optimization reasons, does not reduce x1 mod n, which is
// invalid unless p is very close to n in size.
// enforce x1 < n
Expand Down
56 changes: 54 additions & 2 deletions halo2-ecc/src/ecc/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -936,8 +936,18 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC> {
EcPoint::new(P.x, self.field_chip.negate(ctx, P.y))
}

pub fn negate_strict(
&self,
ctx: &mut Context<F>,
P: impl Into<StrictEcPoint<F, FC>>,
) -> StrictEcPoint<F, FC> {
let P = P.into();
StrictEcPoint::new(P.x, self.field_chip.negate(ctx, P.y))
}

/// Assumes that P.x != Q.x
/// If `is_strict == true`, then actually constrains that `P.x != Q.x`
/// Neither are points at infinity (otherwise, undefined behavior)
pub fn add_unequal(
&self,
ctx: &mut Context<F>,
Expand Down Expand Up @@ -980,6 +990,19 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC> {
self.field_chip.range().gate().and(ctx, x_is_equal, y_is_equal)
}

/// Checks if a point is the point at infinity (represented by (0, 0))
/// Assumes points at infinity are always serialized as (0, 0) as bigints
pub fn is_infinity(
&self,
ctx: &mut Context<F>,
P: EcPoint<F, FC::FieldPoint>,
) -> AssignedValue<F> {
// TODO: optimize
let x_is_zero = self.field_chip.is_soft_zero(ctx, P.x);
let y_is_zero = self.field_chip.is_soft_zero(ctx, P.y);
self.field_chip.range().gate().and(ctx, x_is_zero, y_is_zero)
}

pub fn assert_equal(
&self,
ctx: &mut Context<F>,
Expand All @@ -990,8 +1013,8 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC> {
self.field_chip.assert_equal(ctx, P.y, Q.y);
}

/// None of elements in `points` can be point at infinity.
pub fn sum<C>(
/// None of elements in `points` can be point at infinity. Sum cannot be point at infinity either.
pub fn sum_unsafe<C>(
&self,
ctx: &mut Context<F>,
points: impl IntoIterator<Item = EcPoint<F, FC::FieldPoint>>,
Expand All @@ -1014,6 +1037,35 @@ impl<'chip, F: BigPrimeField, FC: FieldChip<F>> EccChip<'chip, F, FC>
where
FC: Selectable<F, FC::FieldPoint>,
{
/// Expensive version of `sum_unsafe`, but works generally meaning that
/// * sum can be the point at infinity
/// * addends can be points at infinity
pub fn sum<C>(
&self,
ctx: &mut Context<F>,
points: impl IntoIterator<Item = EcPoint<F, FC::FieldPoint>>,
) -> EcPoint<F, FC::FieldPoint>
where
C: CurveAffineExt<Base = FC::FieldType>,
{
let rand_point = self.load_random_point::<C>(ctx);
let rand_point2 = self.load_random_point::<C>(ctx);
let neg_rand_point = self.negate(ctx, rand_point.clone());
let mut acc = ComparableEcPoint::from(neg_rand_point.clone());
for point in points {
let point_is_inf = self.is_infinity(ctx, point.clone());
let addend = self.select(ctx, rand_point2.clone(), point.clone(), point_is_inf);
jonathanpwang marked this conversation as resolved.
Show resolved Hide resolved
let _acc = self.add_unequal(ctx, acc.clone(), addend.clone(), true);
let _acc = self.select(ctx, acc.clone().into(), _acc, point_is_inf);
acc = _acc.into();
}
let acc_is_neg_rand = self.is_equal(ctx, acc.clone().into(), neg_rand_point);
let addend = self.select(ctx, rand_point2.clone(), acc.clone().into(), acc_is_neg_rand);
let sum = self.add_unequal(ctx, addend, rand_point, true);
let inf = self.load_private_unchecked(ctx, (FC::FieldType::ZERO, FC::FieldType::ZERO));
self.select(ctx, inf, sum, acc_is_neg_rand)
}

pub fn select(
&self,
ctx: &mut Context<F>,
Expand Down
Loading