Skip to content

Commit

Permalink
Merge 1cbc5e1 into fd1f619
Browse files Browse the repository at this point in the history
  • Loading branch information
sirasistant authored Jan 15, 2024
2 parents fd1f619 + 1cbc5e1 commit 292031f
Show file tree
Hide file tree
Showing 5 changed files with 201 additions and 54 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -8,10 +8,6 @@ use crate::{
note_interface::NoteInterface,
},
oracle::get_nullifier_membership_witness::get_low_nullifier_membership_witness,
utils::{
full_field_less_than,
full_field_greater_than,
},
};

pub fn prove_nullifier_non_inclusion(
Expand All @@ -36,13 +32,13 @@ pub fn prove_nullifier_non_inclusion(

// 3.b) Prove that the low nullifier is smaller than the nullifier
assert(
full_field_less_than(witness.leaf_preimage.nullifier, nullifier), "Proving nullifier non-inclusion failed: low_nullifier.value < nullifier.value check failed"
dep::protocol_types::utils::field::lt(witness.leaf_preimage.nullifier, nullifier), "Proving nullifier non-inclusion failed: low_nullifier.value < nullifier.value check failed"
);

// 3.c) Prove that the low nullifier is pointing "over" the nullifier to prove that the nullifier is not
// included in the nullifier tree (or to 0 if the to-be-inserted nullifier is the largest of all)
assert(
full_field_greater_than(witness.leaf_preimage.next_nullifier, nullifier)
dep::protocol_types::utils::field::gt(witness.leaf_preimage.next_nullifier, nullifier)
| (witness.leaf_preimage.next_index == 0), "Proving nullifier non-inclusion failed: low_nullifier.next_value > nullifier.value check failed"
);
// --> Now we have traversed the trees all the way up to archive root and verified that the nullifier
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,6 @@ use crate::{
get_public_data_witness,
PublicDataWitness,
},
utils::{
full_field_less_than,
},
};

pub fn prove_public_value_inclusion(
Expand All @@ -39,8 +36,8 @@ pub fn prove_public_value_inclusion(
assert_eq(preimage.value, value, "Public value does not match value in witness");
} else {
assert_eq(value, 0, "Got non-zero public value for non-existing slot");
assert(full_field_less_than(preimage.slot, public_value_leaf_slot), "Invalid witness range");
assert(full_field_less_than(public_value_leaf_slot, preimage.next_slot), "Invalid witness range");
dep::protocol_types::utils::field::assert_lt(preimage.slot, public_value_leaf_slot);
dep::protocol_types::utils::field::assert_lt(public_value_leaf_slot, preimage.next_slot);
}

// 5) Prove that the leaf we validated is in the public data tree
Expand Down
9 changes: 0 additions & 9 deletions yarn-project/aztec-nr/aztec/src/utils.nr
Original file line number Diff line number Diff line change
Expand Up @@ -8,15 +8,6 @@ pub fn arr_copy_slice<T, N, M>(src: [T; N], mut dst: [T; M], offset: Field) -> [
// TODO(#3470): Copied over from https://github.com/AztecProtocol/aztec-packages/blob/a07c4bd47313be6aa604a63f37857eb0136b41ba/yarn-project/noir-protocol-circuits/src/crates/rollup-lib/src/base/base_rollup_inputs.nr#L599
// move to a shared place?

// TODO to radix returns u8, so we cannot use bigger radixes. It'd be ideal to use a radix of the maximum range-constrained integer noir supports
pub fn full_field_less_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(lhs, rhs)
}

pub fn full_field_greater_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(rhs, lhs)
}

struct Reader<N> {
data: [Field; N],
offset: Field,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -177,8 +177,8 @@ impl BaseRollupInputs {
|nullifier: Field| {nullifier == 0}, // Nullifier is zero
|leaf: NullifierLeafPreimage| {leaf.hash()}, // Hash leaf
|low_leaf: NullifierLeafPreimage, nullifier: Field| { // Is valid low leaf
let is_less_than_nullifier = full_field_less_than(low_leaf.nullifier, nullifier);
let is_next_greater_than = full_field_less_than(nullifier, low_leaf.next_nullifier);
let is_less_than_nullifier = dep::types::utils::field::lt(low_leaf.nullifier, nullifier);
let is_next_greater_than = dep::types::utils::field::lt(nullifier, low_leaf.next_nullifier);

(!low_leaf.is_empty()) & is_less_than_nullifier & (
is_next_greater_than |
Expand Down Expand Up @@ -398,8 +398,8 @@ fn insert_public_data_update_requests(
let is_update = low_preimage.slot == write.slot;
let is_low_empty = low_preimage.is_empty();

let is_less_than_slot = full_field_less_than(low_preimage.slot, write.slot);
let is_next_greater_than = full_field_less_than(write.slot, low_preimage.next_slot);
let is_less_than_slot = dep::types::utils::field::lt(low_preimage.slot, write.slot);
let is_next_greater_than = dep::types::utils::field::lt(write.slot, low_preimage.next_slot);
let is_in_range = is_less_than_slot & (
is_next_greater_than |
((low_preimage.next_index == 0) & (low_preimage.next_slot == 0)));
Expand Down Expand Up @@ -456,8 +456,8 @@ fn validate_public_data_reads(
let is_low_empty = low_preimage.is_empty();
let is_exact = low_preimage.slot == read.leaf_slot;

let is_less_than_slot = full_field_less_than(low_preimage.slot, read.leaf_slot);
let is_next_greater_than = full_field_less_than(read.leaf_slot, low_preimage.next_slot);
let is_less_than_slot = dep::types::utils::field::lt(low_preimage.slot, read.leaf_slot);
let is_next_greater_than = dep::types::utils::field::lt(read.leaf_slot, low_preimage.next_slot);
let is_in_range = is_less_than_slot
& (is_next_greater_than | ((low_preimage.next_index == 0) & (low_preimage.next_slot == 0)));

Expand Down Expand Up @@ -519,41 +519,13 @@ fn consistent_call_data_hash_full_fields() {
);
}

// TODO to radix returns u8, so we cannot use bigger radixes. It'd be ideal to use a radix of the maximum range-constrained integer noir supports
pub fn full_field_less_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(lhs, rhs)
}

pub fn full_field_greater_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(rhs, lhs)
}

#[test]
fn test_u256_less_than() {
assert(full_field_less_than(1, 1000));
assert(!full_field_less_than(1000, 1000));
assert(!full_field_less_than(1000, 1));
assert(full_field_less_than(0, 0 - 1));
assert(!full_field_less_than(0 - 1, 0));
}

#[test]
fn test_u256_greater_than() {
assert(full_field_greater_than(1000, 1));
assert(!full_field_greater_than(1000, 1000));
assert(!full_field_greater_than(1, 1000));
assert(!full_field_greater_than(0, 0 - 1));
assert(full_field_greater_than(0 - 1, 0));
}

mod tests {
use crate::{
base::{
base_rollup_inputs::{
CALL_DATA_HASH_FULL_FIELDS,
CALL_DATA_HASH_LOG_FIELDS,
BaseRollupInputs,
full_field_less_than,
},
state_diff_hints::StateDiffHints,
},
Expand Down Expand Up @@ -603,6 +575,15 @@ mod tests {
};
use dep::std::option::Option;

// TODO to radix returns u8, so we cannot use bigger radixes. It'd be ideal to use a radix of the maximum range-constrained integer noir supports
fn full_field_less_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(lhs, rhs)
}

fn full_field_greater_than(lhs: Field, rhs: Field) -> bool {
dep::std::eddsa::lt_bytes32(rhs, lhs)
}

struct NullifierInsertion {
existing_index: u64,
value: Field,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,185 @@ pub fn field_from_bytes<N>(bytes: [u8; N], big_endian: bool) -> Field {

as_field
}

global PLO: Field = 53438638232309528389504892708671455233;
global PHI: Field = 64323764613183177041862057485226039389;
global TWO_POW_128: Field = 0x100000000000000000000000000000000;

#[test]
fn check_plo_phi() {
assert_eq(PLO + PHI * TWO_POW_128, 0);
let p_bytes = dep::std::field::modulus_le_bytes();
let mut p_low: Field = 0;
let mut p_high: Field = 0;

let mut offset = 1;
for i in 0..16 {
p_low += (p_bytes[i] as Field) * offset;
p_high += (p_bytes[i + 16] as Field) * offset;
offset *= 256;
}
assert_eq(p_low, PLO);
assert_eq(p_high, PHI);
}

unconstrained fn decompose_unsafe(x: Field) -> (Field, Field) {
let x_bytes = x.to_le_bytes(32);

let mut low: Field = 0;
let mut high: Field = 0;

let mut offset = 1;
for i in 0..16 {
low += (x_bytes[i] as Field) * offset;
high += (x_bytes[i + 16] as Field) * offset;
offset *= 256;
}

(low, high)
}

#[test]
fn test_decompose_unsafe() {
assert_eq(decompose_unsafe(TWO_POW_128), (0, 1));
assert_eq(decompose_unsafe(TWO_POW_128 + 0x1234567890), (0x1234567890, 1));
assert_eq(decompose_unsafe(0x1234567890), (0x1234567890, 0));
}

pub fn decompose(x: Field) -> (Field, Field) {
let (xlo, xhi) = decompose_unsafe(x);
let borrow = lt_unsafe(PLO, xlo, 16);

xlo.assert_max_bit_size(128);
xhi.assert_max_bit_size(128);

assert_eq(x, xlo + TWO_POW_128 * xhi);
let rlo = PLO - xlo + (borrow as Field) * TWO_POW_128;
let rhi = PHI - xhi - (borrow as Field);

rlo.assert_max_bit_size(128);
rhi.assert_max_bit_size(128);

(xlo, xhi)
}

#[test]
fn test_decompose() {
assert_eq(decompose(TWO_POW_128), (0, 1));
assert_eq(decompose(TWO_POW_128 + 0x1234567890), (0x1234567890, 1));
assert_eq(decompose(0x1234567890), (0x1234567890, 0));
}

unconstrained fn lt_unsafe(x: Field, y: Field, num_bytes: u32) -> bool {
let x_bytes = x.__to_le_radix(256, num_bytes);
let y_bytes = y.__to_le_radix(256, num_bytes);
let mut x_is_lt = false;
let mut done = false;
for i in 0..num_bytes {
if (!done) {
let x_byte = x_bytes[num_bytes - 1 - i];
let y_byte = y_bytes[num_bytes - 1 - i];
let bytes_match = x_byte == y_byte;
if !bytes_match {
x_is_lt = x_byte < y_byte;
done = true;
}
}
}
x_is_lt
}

#[test]
fn test_lt_unsafe() {
assert(lt_unsafe(0, 1, 16));
assert(lt_unsafe(0, 0x100, 16));
assert(lt_unsafe(0x100, TWO_POW_128 - 1, 16));
assert(!lt_unsafe(0, TWO_POW_128, 16));
}

unconstrained fn lte_unsafe(x: Field, y: Field, num_bytes: u32) -> bool {
lt_unsafe(x, y, num_bytes) | (x == y)
}

#[test]
fn test_lte_unsafe() {
assert(lte_unsafe(0, 1, 16));
assert(lte_unsafe(0, 0x100, 16));
assert(lte_unsafe(0x100, TWO_POW_128 - 1, 16));
assert(!lte_unsafe(0, TWO_POW_128, 16));

assert(lte_unsafe(0, 0, 16));
assert(lte_unsafe(0x100, 0x100, 16));
assert(lte_unsafe(TWO_POW_128 - 1, TWO_POW_128 - 1, 16));
assert(lte_unsafe(TWO_POW_128, TWO_POW_128, 16));
}

pub fn assert_gt(a: Field, b: Field) {
let (alo, ahi) = decompose(a);
let (blo, bhi) = decompose(b);

let borrow = lte_unsafe(alo, blo, 16);

let rlo = alo - blo - 1 + (borrow as Field) * TWO_POW_128;
let rhi = ahi - bhi - (borrow as Field);

rlo.assert_max_bit_size(128);
rhi.assert_max_bit_size(128);
}

pub fn assert_lt(a: Field, b: Field) {
assert_gt(b, a);
}

#[test]
fn test_assert_gt() {
assert_gt(1, 0);
assert_gt(0x100, 0);
assert_gt((0 - 1), (0 - 2));
assert_gt(TWO_POW_128, 0);
assert_gt(0 - 1, 0);
}

#[test(should_fail)]
fn test_assert_gt_should_fail_eq() {
assert_gt(0, 0);
}

#[test(should_fail)]
fn test_assert_gt_should_fail_low_lt() {
assert_gt(0, 0x100);
}

#[test(should_fail)]
fn test_assert_gt_should_fail_high_lt() {
assert_gt(TWO_POW_128, TWO_POW_128 + 0x100);
}

pub fn gt(a: Field, b: Field) -> bool {
if a == b {
false
} else if lt_unsafe(a, b, 32) {
assert_gt(b, a);
false
} else {
assert_gt(a, b);
true
}
}

pub fn lt(a: Field, b: Field) -> bool {
gt(b, a)
}

#[test]
fn test_gt() {
assert(gt(1, 0));
assert(gt(0x100, 0));
assert(gt((0 - 1), (0 - 2)));
assert(gt(TWO_POW_128, 0));
assert(!gt(0, 0));
assert(!gt(0, 0x100));
assert(gt(0 - 1, 0 - 2));
assert(!gt(0 - 2, 0 - 1));
}

0 comments on commit 292031f

Please sign in to comment.