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: Recursive verification #1246

Closed
wants to merge 11 commits into from
Closed
654 changes: 381 additions & 273 deletions Cargo.lock

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
@@ -25,7 +25,7 @@ rust-version = "1.66"

[workspace.dependencies]
# acvm = "0.9.0"
acvm = { version = "0.9.0", features = ["bn254"], path = "/Users/maximvezenov/Documents/dev/noir-lang/acvm/acvm" }
acvm = { features = ["bn254"], git = "https://github.com/noir-lang/acvm.git", branch = "mv/verify_proof" }
arena = { path = "crates/arena" }
fm = { path = "crates/fm" }
iter-extended = { path = "crates/iter-extended" }
7 changes: 3 additions & 4 deletions crates/nargo/src/ops/execute.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
use acvm::PartialWitnessGenerator;
use acvm::{acir::circuit::Circuit, pwg::block::Blocks};
use acvm::{PartialWitnessGenerator, PartialWitnessGeneratorStatus};
use noirc_abi::WitnessMap;

use crate::NargoError;
@@ -10,9 +10,8 @@ pub fn execute_circuit(
mut initial_witness: WitnessMap,
) -> Result<WitnessMap, NargoError> {
let mut blocks = Blocks::default();
let (unresolved_opcodes, oracles) =
backend.solve(&mut initial_witness, &mut blocks, circuit.opcodes)?;
if !unresolved_opcodes.is_empty() || !oracles.is_empty() {
let solver_status = backend.solve(&mut initial_witness, &mut blocks, circuit.opcodes)?;
if matches!(solver_status, PartialWitnessGeneratorStatus::RequiresOracleData { .. }) {
todo!("Add oracle support to nargo execute")
}

3 changes: 1 addition & 2 deletions crates/nargo_cli/Cargo.toml
Original file line number Diff line number Diff line change
@@ -37,8 +37,7 @@ termcolor = "1.1.2"
color-eyre = "0.6.2"

# Backends
# acvm-backend-barretenberg = { git = "https://github.com/noir-lang/aztec_backend", rev = "ba1d0d61b94de91b15044d97608907c21bfb5299", default-features=false }
acvm-backend-barretenberg = { path = "/Users/maximvezenov/Documents/dev/noir-lang/aztec_backend", default-features=false }
acvm-backend-barretenberg = { git = "https://github.com/noir-lang/aztec_backend", branch = "mv/recursion", default-features=false }

[dev-dependencies]
tempdir = "0.3.7"
4 changes: 2 additions & 2 deletions crates/nargo_cli/tests/test_data/merkle_insert/src/main.nr
Original file line number Diff line number Diff line change
@@ -12,8 +12,8 @@ fn main(
let old_leaf_exists = std::merkle::check_membership(old_root, old_leaf, index, old_hash_path);
constrain old_leaf_exists == 1;
constrain old_root == std::merkle::compute_root_from_leaf(old_leaf, index, old_hash_path);
let new_leaf_exists = std::merkle::check_membership(new_root, leaf, index, old_hash_path);
constrain new_leaf_exists == 1;
let calculated_root = std::merkle::compute_merkle_root(leaf, index, old_hash_path);
constrain new_root == calculated_root;

let h = std::hash::mimc_bn254(mimc_input);
// Regression test for PR #891
2 changes: 1 addition & 1 deletion crates/noirc_evaluator/src/lib.rs
Original file line number Diff line number Diff line change
@@ -174,7 +174,7 @@ impl Evaluator {
let inter_var_witness = self.add_witness_to_cs();

// Link that witness to the arithmetic gate
let constraint = &arithmetic_gate - &inter_var_witness;
let constraint = &arithmetic_gate - inter_var_witness;
self.opcodes.push(AcirOpcode::Arithmetic(constraint));
inter_var_witness
}
20 changes: 10 additions & 10 deletions crates/noirc_evaluator/src/ssa/acir_gen/constraints.rs
Original file line number Diff line number Diff line change
@@ -31,7 +31,7 @@ pub(crate) fn mul_with_witness(
let a_arith;
let a_arith = if !a.mul_terms.is_empty() && !b.is_const() {
let a_witness = evaluator.create_intermediate_variable(a.clone());
a_arith = Expression::from(&a_witness);
a_arith = Expression::from(a_witness);
&a_arith
} else {
a
@@ -42,7 +42,7 @@ pub(crate) fn mul_with_witness(
a_arith
} else {
let b_witness = evaluator.create_intermediate_variable(b.clone());
b_arith = Expression::from(&b_witness);
b_arith = Expression::from(b_witness);
&b_arith
}
} else {
@@ -54,9 +54,9 @@ pub(crate) fn mul_with_witness(
//a*b
pub(crate) fn mul(a: &Expression, b: &Expression) -> Expression {
if a.is_const() {
return b * &a.q_c;
return b * a.q_c;
} else if b.is_const() {
return a * &b.q_c;
return a * b.q_c;
} else if !(a.is_linear() && b.is_linear()) {
unreachable!("Can only multiply linear terms");
}
@@ -125,9 +125,9 @@ pub(crate) fn subtract(a: &Expression, k: FieldElement, b: &Expression) -> Expre
// TODO in either case, we can put this in ACIR, if its useful
pub(crate) fn add(a: &Expression, k: FieldElement, b: &Expression) -> Expression {
if a.is_const() {
return (b * &k) + &a.q_c;
return (b * k) + a.q_c;
} else if b.is_const() {
return a.clone() + &(k * b.q_c);
return a.clone() + (k * b.q_c);
}

let mut output = Expression::from_field(a.q_c + k * b.q_c);
@@ -497,7 +497,7 @@ pub(crate) fn evaluate_truncate(
if let Some(a_c) = lhs.to_const() {
let mut a_big = BigUint::from_bytes_be(&a_c.to_be_bytes());
a_big %= exp_big;
return Expression::from(&FieldElement::from_be_bytes_reduce(&a_big.to_bytes_be()));
return Expression::from(FieldElement::from_be_bytes_reduce(&a_big.to_bytes_be()));
}
let exp = FieldElement::from_be_bytes_reduce(&exp_big.to_bytes_be());

@@ -524,7 +524,7 @@ pub(crate) fn evaluate_truncate(
let my_constraint = add(&res, -FieldElement::one(), lhs);
evaluator.push_opcode(AcirOpcode::Arithmetic(my_constraint));

Expression::from(&b_witness)
Expression::from(b_witness)
}

pub(crate) fn evaluate_udiv(
@@ -552,8 +552,8 @@ pub(crate) fn evaluate_udiv(
//range check q<=a
try_range_constraint(q_witness, bit_size, evaluator);
// a-b*q-r = 0
let mut d = mul_with_witness(evaluator, rhs, &Expression::from(&q_witness));
d = add(&d, FieldElement::one(), &Expression::from(&r_witness));
let mut d = mul_with_witness(evaluator, rhs, &Expression::from(q_witness));
d = add(&d, FieldElement::one(), &Expression::from(r_witness));
d = mul_with_witness(evaluator, &d, predicate);
let div_euclidean = subtract(&pa, FieldElement::one(), &d);

2 changes: 1 addition & 1 deletion crates/noirc_evaluator/src/ssa/acir_gen/internal_var.rs
Original file line number Diff line number Diff line change
@@ -98,7 +98,7 @@ impl InternalVar {
/// Expression, this method is infallible.
pub(crate) fn from_witness(witness: Witness) -> InternalVar {
InternalVar {
expression: Expression::from(&witness),
expression: Expression::from(witness),
cached_witness: Some(witness),
id: None,
}
4 changes: 2 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/binary.rs
Original file line number Diff line number Diff line change
@@ -146,12 +146,12 @@ pub(crate) fn evaluate(
if r_value.is_zero() {
panic!("Panic - division by zero");
} else {
(l_c.expression() * &r_value.inverse()).into()
(l_c.expression() * r_value.inverse()).into()
}
} else {
//TODO avoid creating witnesses here.
let x_witness = acir_gen.var_cache.get_or_compute_witness(r_c, evaluator).expect("unexpected constant expression");
let inverse = Expression::from(&constraints::evaluate_inverse(
let inverse = Expression::from(constraints::evaluate_inverse(
x_witness, &predicate, evaluator,
));
InternalVar::from(constraints::mul_with_witness(
4 changes: 2 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/bitwise.rs
Original file line number Diff line number Diff line change
@@ -155,9 +155,9 @@ pub(super) fn evaluate_bitwise(
constraints::subtract(
&Expression::from_field(max),
FieldElement::one(),
&Expression::from(&result),
&Expression::from(result),
)
} else {
Expression::from(&result)
Expression::from(result)
}
}
4 changes: 2 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/cmp.rs
Original file line number Diff line number Diff line change
@@ -69,7 +69,7 @@ pub(super) fn evaluate_neq(
.get_or_compute_witness(x, evaluator)
.expect("unexpected constant expression");

return Expression::from(&constraints::evaluate_zero_equality(x_witness, evaluator));
return Expression::from(constraints::evaluate_zero_equality(x_witness, evaluator));
}

// Arriving here means that `lhs` and `rhs` are not Arrays
@@ -95,7 +95,7 @@ pub(super) fn evaluate_neq(
.var_cache
.get_or_compute_witness(x, evaluator)
.expect("unexpected constant expression");
Expression::from(&constraints::evaluate_zero_equality(x_witness, evaluator))
Expression::from(constraints::evaluate_zero_equality(x_witness, evaluator))
}
}

Original file line number Diff line number Diff line change
@@ -107,7 +107,7 @@ pub(crate) fn evaluate(
}
outputs =
prepare_outputs(&mut acir_gen.memory, instruction_id, array.len, ctx, evaluator);
let out_expr: Vec<Expression> = outputs.iter().map(|w| w.into()).collect();
let out_expr: Vec<Expression> = outputs.iter().map(|w| (*w).into()).collect();
for i in 0..(out_expr.len() - 1) {
bound_constraint_with_offset(
&out_expr[i],
2 changes: 1 addition & 1 deletion crates/noirc_evaluator/src/ssa/acir_gen/operations/not.rs
Original file line number Diff line number Diff line change
@@ -19,7 +19,7 @@ pub(crate) fn evaluate(
let l_c = var_cache.get_or_compute_internal_var_unwrap(*value, evaluator, ctx);
Some(
constraints::subtract(
&Expression::from(&FieldElement::from(a)),
&Expression::from(FieldElement::from(a)),
FieldElement::one(),
l_c.expression(),
)
5 changes: 3 additions & 2 deletions crates/noirc_evaluator/src/ssa/acir_gen/operations/sort.rs
Original file line number Diff line number Diff line change
@@ -119,6 +119,7 @@ mod test {
acir::{circuit::opcodes::BlackBoxFuncCall, native_types::Witness},
pwg::block::Blocks,
FieldElement, OpcodeResolution, OpcodeResolutionError, PartialWitnessGenerator,
PartialWitnessGeneratorStatus,
};

use crate::{
@@ -180,10 +181,10 @@ mod test {
// compute the network output by solving the constraints
let backend = MockBackend {};
let mut blocks = Blocks::default();
let (unresolved_opcodes, oracles) = backend
let solver_status = backend
.solve(&mut solved_witness, &mut blocks, eval.opcodes.clone())
.expect("Could not solve permutation constraints");
assert!(unresolved_opcodes.is_empty() && oracles.is_empty(), "Incomplete solution");
assert_eq!(solver_status, PartialWitnessGeneratorStatus::Solved, "Incomplete solution");
let mut b_val = Vec::new();
for i in 0..output.len() {
b_val.push(solved_witness[&b_wit[i]]);
18 changes: 10 additions & 8 deletions crates/noirc_evaluator/src/ssa/builtin.rs
Original file line number Diff line number Diff line change
@@ -78,10 +78,10 @@ impl Opcode {
| BlackBoxFunc::FixedBaseScalarMul
| BlackBoxFunc::VerifyProof => BigUint::zero(),
// Verify returns zero or one
BlackBoxFunc::SchnorrVerify
| BlackBoxFunc::EcdsaSecp256k1
| BlackBoxFunc::MerkleMembership => BigUint::one(),
BlackBoxFunc::HashToField128Security => ObjectType::native_field().max_size(),
BlackBoxFunc::SchnorrVerify | BlackBoxFunc::EcdsaSecp256k1 => BigUint::one(),
BlackBoxFunc::ComputeMerkleRoot | BlackBoxFunc::HashToField128Security => {
ObjectType::native_field().max_size()
}
BlackBoxFunc::AES => {
todo!("ICE: AES is unimplemented")
}
@@ -112,11 +112,13 @@ impl Opcode {
BlackBoxFunc::SHA256 | BlackBoxFunc::Blake2s => {
(32, ObjectType::unsigned_integer(8))
}
BlackBoxFunc::HashToField128Security => (1, ObjectType::native_field()),
BlackBoxFunc::ComputeMerkleRoot | BlackBoxFunc::HashToField128Security => {
(1, ObjectType::native_field())
}
// See issue #775 on changing this to return a boolean
BlackBoxFunc::MerkleMembership
| BlackBoxFunc::SchnorrVerify
| BlackBoxFunc::EcdsaSecp256k1 => (1, ObjectType::native_field()),
BlackBoxFunc::SchnorrVerify | BlackBoxFunc::EcdsaSecp256k1 => {
(1, ObjectType::native_field())
}
BlackBoxFunc::Pedersen => (2, ObjectType::native_field()),
BlackBoxFunc::FixedBaseScalarMul => (2, ObjectType::native_field()),
BlackBoxFunc::VerifyProof => (16, ObjectType::native_field()),
6 changes: 3 additions & 3 deletions flake.lock

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

13 changes: 6 additions & 7 deletions noir_stdlib/src/merkle.nr
Original file line number Diff line number Diff line change
@@ -5,16 +5,15 @@
// and the hashpath proves this
// Currently we assume that it is a binary tree, so depth k implies a width of 2^k
// XXX: In the future we can add an arity parameter
#[foreign(merkle_membership)]
fn check_membership(_root : Field, _leaf : Field, _index : Field, _hash_path: [Field]) -> Field {}


#[alternative(merkle_membership)]
fn check_membership_in_noir(root : Field, leaf : Field, index : Field, hash_path: [Field]) -> Field {
(compute_root_from_leaf(leaf, index, hash_path) == root) as Field
fn check_membership(_root : Field, _leaf : Field, _index : Field, _hash_path: [Field]) -> Field {
(compute_merkle_root(_leaf, _index, _hash_path) == _root) as Field
}

#[foreign(compute_merkle_root)]
fn compute_merkle_root(_leaf : Field, _index : Field, _hash_path: [Field]) -> Field {}

// Returns the root of the tree from the provided leaf and its hashpath, using pedersen hash
#[alternative(compute_merkle_root)]
fn compute_root_from_leaf(leaf : Field, index : Field, hash_path: [Field]) -> Field {
let n = hash_path.len();
let index_bits = index.to_le_bits(n as u32);