-
Notifications
You must be signed in to change notification settings - Fork 59
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
Builtin operators #197
base: main
Are you sure you want to change the base?
Builtin operators #197
Changes from 1 commit
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,13 +1,16 @@ | ||
use crate::{ | ||
backends::Backend, | ||
circuit_writer::CircuitWriter, | ||
circuit_writer::{CircuitWriter, VarInfo}, | ||
constants::Span, | ||
parser::types::{GenericParameters, TyKind}, | ||
stdlib::bits::to_bits, | ||
var::{ConstOrCell, Value, Var}, | ||
}; | ||
|
||
use super::boolean; | ||
|
||
use ark_ff::{One, Zero}; | ||
use ark_ff::{Field, One, PrimeField, Zero}; | ||
use kimchi::o1_utils::FieldHelpers; | ||
|
||
use std::ops::Neg; | ||
|
||
|
@@ -99,6 +102,143 @@ pub fn mul<B: Backend>( | |
} | ||
} | ||
|
||
fn constrain_div_mod<B: Backend>( | ||
compiler: &mut CircuitWriter<B>, | ||
lhs: &ConstOrCell<B::Field, B::Var>, | ||
rhs: &ConstOrCell<B::Field, B::Var>, | ||
span: Span, | ||
) -> (B::Var, B::Var) { | ||
// to constrain lhs − q * rhs − rem = 0 | ||
// where rhs is the modulus | ||
// so 0 <= rem < rhs | ||
|
||
let one = B::Field::one(); | ||
|
||
// todo: to avoid duplicating a lot of code due the different combinations of the input types | ||
// until we refactor the backend to handle ConstOrCell or some kind of wrapper that encapsulate the different variable types | ||
// convert cst to var for easier handling | ||
let lhs = match lhs { | ||
ConstOrCell::Const(lhs) => compiler.backend.add_constant( | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Note that we also wanted to remove this add_constant fn :p |
||
Some("wrap a constant as var"), | ||
*lhs, | ||
span, | ||
), | ||
ConstOrCell::Cell(lhs) => lhs.clone(), | ||
}; | ||
|
||
let rhs = match rhs { | ||
ConstOrCell::Const(rhs) => compiler.backend.add_constant( | ||
Some("wrap a constant as var"), | ||
*rhs, | ||
span, | ||
), | ||
ConstOrCell::Cell(rhs) => rhs.clone(), | ||
}; | ||
|
||
// witness var for quotient | ||
let q = Value::VarDivVar(lhs.clone(), rhs.clone()); | ||
let q_var = compiler.backend.new_internal_var(q, span); | ||
|
||
// witness var for remainder | ||
let rem = Value::VarModVar(lhs.clone(), rhs.clone()); | ||
let rem_var = compiler.backend.new_internal_var(rem, span); | ||
|
||
// rem < rhs | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. If lhs < rhs then we will have rem = lhs. So either we forbid lhs < rhs or we add an edge case to make it work as well. Both might lead to extra constraints tho... There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. yeah, this constraint seems not well done. let me research a bit on how others constrain this. |
||
let lt_rem = &less_than(compiler, None, &ConstOrCell::Cell(rem_var.clone()), &ConstOrCell::Cell(rhs.clone()), span)[0]; | ||
let lt_rem = lt_rem.cvar().expect("expected a cell var"); | ||
compiler.backend.assert_eq_const(lt_rem, one, span); | ||
|
||
// foundamental constraint: lhs - q * rhs - rem = 0 | ||
let q_mul_rhs = compiler.backend.mul(&q_var, &rhs, span); | ||
let lhs_sub_q_mul_rhs = compiler.backend.sub(&lhs, &q_mul_rhs, span); | ||
|
||
// cell representing the foundamental constraint | ||
let fc_var = compiler.backend.sub(&lhs_sub_q_mul_rhs, &rem_var, span); | ||
compiler.backend.assert_eq_const(&fc_var, B::Field::zero(), span); | ||
|
||
(rem_var, q_var) | ||
} | ||
|
||
/// Divide operation | ||
pub fn div<B: Backend>( | ||
compiler: &mut CircuitWriter<B>, | ||
lhs: &ConstOrCell<B::Field, B::Var>, | ||
rhs: &ConstOrCell<B::Field, B::Var>, | ||
span: Span, | ||
) -> Var<B::Field, B::Var> { | ||
// to constrain lhs − q * rhs − rem = 0 | ||
// rhs can't be zero | ||
match rhs { | ||
ConstOrCell::Const(rhs) => { | ||
if rhs.is_zero() { | ||
panic!("division by zero"); | ||
} | ||
} | ||
_ => { | ||
let is_zero = is_zero_cell(compiler, rhs, span); | ||
let is_zero = is_zero[0].cvar().unwrap(); | ||
compiler.backend.assert_eq_const(is_zero, B::Field::zero(), span); | ||
} | ||
}; | ||
|
||
match (lhs, rhs) { | ||
// if rhs is a constant, we can just divide lhs by rhs | ||
(ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { | ||
// to bigint | ||
let lhs = lhs.to_biguint(); | ||
let rhs = rhs.to_biguint(); | ||
let res = lhs / rhs; | ||
|
||
Var::new_constant(B::Field::from(res), span) | ||
} | ||
_ => { | ||
let (_, q) = constrain_div_mod(compiler, lhs, rhs, span); | ||
Var::new_var(q, span) | ||
}, | ||
} | ||
} | ||
|
||
/// Modulus operation | ||
pub fn modulus<B: Backend>( | ||
compiler: &mut CircuitWriter<B>, | ||
lhs: &ConstOrCell<B::Field, B::Var>, | ||
rhs: &ConstOrCell<B::Field, B::Var>, | ||
span: Span, | ||
) -> Var<B::Field, B::Var> { | ||
// to constrain lhs − q * rhs − rem = 0 | ||
|
||
let zero = B::Field::zero(); | ||
|
||
// rhs can't be zero | ||
match &rhs { | ||
ConstOrCell::Const(rhs) => { | ||
if rhs.is_zero() { | ||
panic!("modulus by zero"); | ||
} | ||
} | ||
_ => { | ||
let is_zero = is_zero_cell(compiler, rhs, span); | ||
let is_zero = is_zero[0].cvar().unwrap(); | ||
compiler.backend.assert_eq_const(is_zero, zero, span); | ||
} | ||
}; | ||
|
||
match (lhs, rhs) { | ||
// if rhs is a constant, we can just divide lhs by rhs | ||
(ConstOrCell::Const(lhs), ConstOrCell::Const(rhs)) => { | ||
let lhs = lhs.to_biguint(); | ||
let rhs = rhs.to_biguint(); | ||
let res = lhs % rhs; | ||
|
||
Var::new_constant(res.into(), span) | ||
} | ||
_ => { | ||
let (rem, _) = constrain_div_mod(compiler, lhs, rhs, span); | ||
Var::new_var(rem, span) | ||
} | ||
} | ||
} | ||
|
||
/// This takes variables that can be anything, and returns a boolean | ||
// TODO: so perhaps it's not really relevant in this file? | ||
pub fn equal<B: Backend>( | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
why not a single
Value::Div(VarOrCst, VarOrCst)
?