Skip to content

Commit

Permalink
finished addition
Browse files Browse the repository at this point in the history
  • Loading branch information
zhenfeizhang committed Nov 28, 2024
1 parent b374ecc commit 8594c7a
Show file tree
Hide file tree
Showing 12 changed files with 463 additions and 86 deletions.
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

3 changes: 3 additions & 0 deletions circuit-std-rs/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,6 @@ pub use traits::StdCircuit;

pub mod logup;
pub use logup::{LogUpCircuit, LogUpParams};

pub mod range_proof;
pub use range_proof::*;
31 changes: 31 additions & 0 deletions circuit-std-rs/src/range_proof.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
//! use log up for range proofs
use expander_compiler::{
declare_circuit,
frontend::{Config, Define, Variable, API},
};

use crate::LogUpParams;

#[derive(Clone, Copy, Debug)]
pub struct RangeProofParams {
pub number_of_bits: usize,
}

declare_circuit!(_RangeCircuit {
// This circuit range checks len(values) number of value
values: [Variable]
});

pub type RangeProofCircuit = _RangeCircuit<Variable>;

impl<C: Config> Define<C> for RangeProofCircuit {
fn define(&self, builder: &mut API<C>) {
let log_up_param = LogUpParams {
key_len: 1 << 8,
value_len: 1 << 8,
n_table_rows: 1 << 8,
n_queries: self.values.len(),
};
}
}
4 changes: 2 additions & 2 deletions expander_compiler/src/frontend/builder.rs
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@ pub struct Builder<C: Config> {

#[derive(Clone, Copy, Debug, Default)]
pub struct Variable {
id: usize,
pub id: usize,
}

pub enum VariableOrValue<F: Field> {
Expand Down Expand Up @@ -484,7 +484,7 @@ impl<C: Config> RootBuilder<C> {
}
}

fn last_builder(&mut self) -> &mut Builder<C> {
pub fn last_builder(&mut self) -> &mut Builder<C> {
&mut self.current_builders.last_mut().unwrap().1
}

Expand Down
1 change: 1 addition & 0 deletions expander_compiler/src/frontend/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ pub use crate::circuit::config::*;
pub use crate::field::{Field, BN254, GF2, M31};
pub use crate::utils::error::Error;
pub use api::BasicAPI;
pub use builder::ToVariableOrValue;
pub use builder::Variable;
pub use circuit::Define;
pub use witness::WitnessSolver;
Expand Down
2 changes: 2 additions & 0 deletions rsa_circuit/src/tests.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
mod native;
mod u120_add;
mod u120_mul;
mod u2048_add;
mod u2048_comp;
2 changes: 1 addition & 1 deletion rsa_circuit/src/tests/u120_add.rs
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@ impl Define<BN254Config> for AddCircuit<Variable> {
// };

let (result, carry_out) =
u120::add_u120::<BN254Config>(&self.x, &self.y, &self.carry_in, &two_to_120, builder);
u120::add_u120(&self.x, &self.y, &self.carry_in, &two_to_120, builder);

builder.assert_is_equal(result, self.result);
builder.assert_is_equal(carry_out, self.carry_out);
Expand Down
4 changes: 1 addition & 3 deletions rsa_circuit/src/tests/u120_mul.rs
Original file line number Diff line number Diff line change
Expand Up @@ -23,12 +23,10 @@ impl Define<BN254Config> for MulCircuit<Variable> {
let two_to_120 = builder.constant(BN_TWO_TO_120);

let (result, carry_out) =
u120::mul_u120::<BN254Config>(&self.x, &self.y, &self.carry_in, &two_to_120, builder);

u120::mul_u120(&self.x, &self.y, &self.carry_in, &two_to_120, builder);

builder.assert_is_equal(result, self.result);
builder.assert_is_equal(carry_out, self.carry_out);

}
}

Expand Down
164 changes: 164 additions & 0 deletions rsa_circuit/src/tests/u2048_add.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,164 @@
use expander_compiler::frontend::*;
use expander_compiler::{
declare_circuit,
frontend::{BN254Config, Define, Variable, API},
};
use halo2curves::bn256::Fr;

use crate::constants::{BN_TWO_TO_120, N_LIMBS};
use crate::u2048::U2048Variable;

declare_circuit!(AddModCircuit {
x: [Variable; N_LIMBS],
y: [Variable; N_LIMBS],
result: [Variable; N_LIMBS],
carry: Variable,
modulus: [Variable; N_LIMBS],
});

impl Define<BN254Config> for AddModCircuit<Variable> {
fn define(&self, builder: &mut API<BN254Config>) {
let x = U2048Variable::from_raw(self.x);
let y = U2048Variable::from_raw(self.y);
let result = U2048Variable::from_raw(self.result);
let modulus = U2048Variable::from_raw(self.modulus);
let two_to_120 = builder.constant(BN_TWO_TO_120);

U2048Variable::assert_add(&x, &y, &result, &self.carry, &modulus, &two_to_120, builder);
}
}

impl AddModCircuit<Fr> {
fn create_circuit(
x: [[u64; 2]; N_LIMBS],
y: [[u64; 2]; N_LIMBS],
result: [[u64; 2]; N_LIMBS],
carry: u64,
modulus: [[u64; 2]; N_LIMBS],
) -> AddModCircuit<Fr> {
let mut x_limbs = [Fr::zero(); N_LIMBS];
let mut y_limbs = [Fr::zero(); N_LIMBS];
let mut result_limbs = [Fr::zero(); N_LIMBS];
let mut modulus_limbs = [Fr::zero(); N_LIMBS];

for i in 0..N_LIMBS {
x_limbs[i] = Fr::from_raw([x[i][0], x[i][1], 0, 0]);
y_limbs[i] = Fr::from_raw([y[i][0], y[i][1], 0, 0]);
result_limbs[i] = Fr::from_raw([result[i][0], result[i][1], 0, 0]);
modulus_limbs[i] = Fr::from_raw([modulus[i][0], modulus[i][1], 0, 0]);
}

Self {
x: x_limbs,
y: y_limbs,
result: result_limbs,
carry: Fr::from(carry),
modulus: modulus_limbs,
}
}
}

#[test]
fn test_mod_add() {
let compile_result = compile(&AddModCircuit::default()).unwrap();

{
// Test case: Simple addition without mod reduction
let x = [[5, 0]; N_LIMBS];
let y = [[3, 0]; N_LIMBS];
let result = [[8, 0]; N_LIMBS];
let modulus = [[10, 0]; N_LIMBS];

let assignment = AddModCircuit::<Fr>::create_circuit(x, y, result, 0, modulus);
let witness = compile_result
.witness_solver
.solve_witness(&assignment)
.unwrap();

let output = compile_result.layered_circuit.run(&witness);
assert_eq!(output, vec![true]);
}

{
// Test case: Addition with carry between limbs (like u64::MAX + u64::MAX)
let mut x = [[0, 0]; N_LIMBS];
let mut y = [[0, 0]; N_LIMBS];
let mut result = [[0, 0]; N_LIMBS];
let mut modulus = [[0, 0]; N_LIMBS];

x[0] = [u64::MAX, 0];
y[0] = [u64::MAX, 0];
result[0] = [u64::MAX - 1, 1];
modulus[1] = [0, 1]; // Large modulus to avoid reduction

let assignment = AddModCircuit::<Fr>::create_circuit(x, y, result, 0, modulus);
let witness = compile_result
.witness_solver
.solve_witness(&assignment)
.unwrap();

let output = compile_result.layered_circuit.run(&witness);
assert_eq!(output, vec![true]);
}

{
// Test case: Addition with modular reduction
let mut x = [[0, 0]; N_LIMBS];
let mut y = [[0, 0]; N_LIMBS];
let mut result = [[0, 0]; N_LIMBS];
let mut modulus = [[0, 0]; N_LIMBS];

x[0] = [7, 0];
y[0] = [5, 0];
result[0] = [2, 0];
modulus[0] = [10, 0];

let assignment = AddModCircuit::<Fr>::create_circuit(x, y, result, 1, modulus);
let witness = compile_result
.witness_solver
.solve_witness(&assignment)
.unwrap();

let output = compile_result.layered_circuit.run(&witness);
assert_eq!(output, vec![true]);
}

{
// Test case: Invalid carry value
let x = [[5, 0]; N_LIMBS];
let y = [[3, 0]; N_LIMBS];
let result = [[8, 0]; N_LIMBS];
let modulus = [[10, 0]; N_LIMBS];

let assignment = AddModCircuit::<Fr>::create_circuit(x, y, result, 2, modulus); // carry > 1
let witness = compile_result
.witness_solver
.solve_witness(&assignment)
.unwrap();

let output = compile_result.layered_circuit.run(&witness);
assert_eq!(output, vec![false]);
}

{
// Negative test: result >= modulus
let mut x = [[0, 0]; N_LIMBS];
let mut y = [[0, 0]; N_LIMBS];
let mut result = [[0, 0]; N_LIMBS];
let mut modulus = [[0, 0]; N_LIMBS];

x[0] = [7, 0];
y[0] = [5, 0];
result[0] = [12, 0]; // result > modulus
modulus[0] = [10, 0];

let assignment = AddModCircuit::<Fr>::create_circuit(x, y, result, 0, modulus);
let witness = compile_result
.witness_solver
.solve_witness(&assignment)
.unwrap();

let output = compile_result.layered_circuit.run(&witness);
assert_eq!(output, vec![false]);
}
}
Loading

0 comments on commit 8594c7a

Please sign in to comment.