Skip to content

Commit

Permalink
feat: enable to_radix for any field element (#1343)
Browse files Browse the repository at this point in the history
* Enable to_radix for any field element

* add integration test

* use proper bound during modulo (and small optimisation)

* update integration test
  • Loading branch information
guipublic authored May 15, 2023
1 parent 7df3bb1 commit c3bdec2
Show file tree
Hide file tree
Showing 3 changed files with 100 additions and 15 deletions.
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
x = "2040124"
_y = "0x2000000000000000000000000000000000000000000000000000000000000000"
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
use dep::std;

fn main(x : Field) {
fn main(x : Field, _y: Field) {
// The result of this byte array will be big-endian
let y: Field = 2040124;
let be_byte_array = y.to_be_bytes(31);
Expand All @@ -11,4 +11,17 @@ fn main(x : Field) {
assert(le_byte_array[0] == be_byte_array[30]);
assert(le_byte_array[1] == be_byte_array[29]);
assert(le_byte_array[2] == be_byte_array[28]);

let z = 0 - 1;
let p_bytes = std::field::modulus_le_bytes();
let z_bytes = z.to_le_bytes(32);
assert(p_bytes[10] == z_bytes[10]);
assert(p_bytes[0] == z_bytes[0] as u8 + 1 as u8);

let p_bits = std::field::modulus_le_bits();
let z_bits = z.to_le_bits(std::field::modulus_num_bits() as u32);
assert(z_bits[0] == 0);
assert(p_bits[100] == z_bits[100]);

_y.to_le_bits(std::field::modulus_num_bits() as u32);
}
99 changes: 85 additions & 14 deletions crates/noirc_evaluator/src/ssa/acir_gen/constraints.rs
Original file line number Diff line number Diff line change
Expand Up @@ -405,25 +405,43 @@ pub(crate) fn to_radix_base(
evaluator: &mut Evaluator,
) -> Vec<Witness> {
// ensure there is no overflow
let mut max = BigUint::from(radix);
max = max.pow(limb_size) - BigUint::one();
assert!(max < FieldElement::modulus());
let rad = BigUint::from(radix);
let max = rad.pow(limb_size) - BigUint::one();

let (mut result, bytes) = to_radix_little(radix, limb_size, evaluator);
if max < FieldElement::modulus() {
let (mut result, bytes) = to_radix_little(radix, limb_size, evaluator);

evaluator.push_opcode(AcirOpcode::Directive(Directive::ToLeRadix {
a: lhs.clone(),
b: result.clone(),
radix,
}));
evaluator.push_opcode(AcirOpcode::Directive(Directive::ToLeRadix {
a: lhs.clone(),
b: result.clone(),
radix,
}));

if endianness == Endian::Big {
result.reverse();
}
if endianness == Endian::Big {
result.reverse();
}

evaluator.push_opcode(AcirOpcode::Arithmetic(subtract(lhs, FieldElement::one(), &bytes)));
evaluator.push_opcode(AcirOpcode::Arithmetic(subtract(lhs, FieldElement::one(), &bytes)));
result
} else {
let min = rad.pow(limb_size - 1) - BigUint::one();
assert!(min < FieldElement::modulus());

let max_bits = max.bits() as u32;
let a = evaluate_constant_modulo(lhs, radix, max_bits, evaluator)
.to_witness()
.expect("Constant expressions should already be simplified");
let y = subtract(lhs, FieldElement::one(), &Expression::from(a));
let radix_f = FieldElement::from(radix as i128);
let y = Expression::default().add_mul(FieldElement::one() / radix_f, &y);
let mut b = to_radix_base(&y, radix, limb_size - 1, endianness, evaluator);
match endianness {
Endian::Little => b.insert(0, a),
Endian::Big => b.push(a),
}

result
b
}
}

//Decomposition into b-base: \sum ai b^i, where 0<=ai<b
Expand Down Expand Up @@ -527,6 +545,59 @@ pub(crate) fn evaluate_truncate(
Expression::from(b_witness)
}

//Returns b such that lhs (a number whose value requires max_bits) mod rhs is b
pub(crate) fn evaluate_constant_modulo(
lhs: &Expression,
rhs: u32,
max_bits: u32,
evaluator: &mut Evaluator,
) -> Expression {
let modulus = FieldElement::from(rhs as i128);
let modulus_exp = Expression::from_field(modulus);
assert_ne!(rhs, 0);
let modulus_bits = bit_size_u128((rhs - 1) as u128);
assert!(max_bits >= rhs, "max_bits = {max_bits}, rhs = {rhs}");
//0. Check for constant expression. This can happen through arithmetic simplifications
if let Some(a_c) = lhs.to_const() {
let mut a_big = BigUint::from_bytes_be(&a_c.to_be_bytes());
a_big %= BigUint::from_bytes_be(&modulus.to_be_bytes());
return Expression::from(FieldElement::from_be_bytes_reduce(&a_big.to_bytes_be()));
}

//1. Generate witnesses b,c
let b_witness = evaluator.add_witness_to_cs();
let c_witness = evaluator.add_witness_to_cs();
evaluator.push_opcode(AcirOpcode::Directive(Directive::Quotient {
a: lhs.clone(),
b: modulus_exp.clone(),
q: c_witness,
r: b_witness,
predicate: None,
}));
bound_constraint_with_offset(
&Expression::from(b_witness),
&modulus_exp,
&Expression::one(),
modulus_bits,
evaluator,
);
//if rhs is a power of 2, then we avoid this range check as it is redundant with the previous one.
if rhs & (rhs - 1) != 0 {
try_range_constraint(b_witness, modulus_bits, evaluator);
}
let c_bound = FieldElement::modulus() / BigUint::from(rhs) - BigUint::one();
try_range_constraint(c_witness, c_bound.bits() as u32, evaluator);

//2. Add the constraint lhs = b+q*rhs
let b_arith = b_witness.into();
let c_arith = c_witness.into();
let res = add(&b_arith, modulus, &c_arith);
let my_constraint = add(&res, -FieldElement::one(), lhs);
evaluator.push_opcode(AcirOpcode::Arithmetic(my_constraint));

Expression::from(b_witness)
}

pub(crate) fn evaluate_udiv(
lhs: &Expression,
rhs: &Expression,
Expand Down

0 comments on commit c3bdec2

Please sign in to comment.