Builtin operators#197
Conversation
There was a problem hiding this comment.
left some comments, I need to have another pass on the division which seems to be the most tricky part of the logic :o
also I remember that there was a nice way to check if a < b in the field without having to check a 256 bits decomposition but only a 128 bit decomposition. We should check how other implementations do it :o
| // otherwise, the carry bit of sum_bits is 1. | ||
|
|
||
| /* | ||
| psuedo code: |
| (ConstOrCell::Cell(lhs_), ConstOrCell::Const(rhs_)) => { | ||
| let pow2 = B::Field::from(2u32).pow(rhs_.into_repr()); | ||
| let res = compiler.backend.mul_const(lhs_, &pow2, span); | ||
| Var::new_var(res, span) |
There was a problem hiding this comment.
The weird thing to me is that at this point there is no way to tell if there is an overflow, the modulus length also impacts that. Maybe that's fine though... But I'm not sure what people would expect. Is this operator implemented in any other DSL? How do they handle overflows?
There was a problem hiding this comment.
yeah, overflow is probably something to take care of here.
One of the compilers restricts the value type to be integer and the shift amount to be u8. I guess the reason it restrict to be integer is for range checking the resulted value.
| // convert to bigint | ||
| let pow2 = B::Field::from(2u32).pow(rhs.into_repr()); | ||
| let res = *lhs * pow2; | ||
| Var::new_constant(res, span) |
There was a problem hiding this comment.
We should return an error on overflow perhaps
| // 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.
Note that we also wanted to remove this add_constant fn :p
| 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.
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.
yeah, this constraint seems not well done. let me research a bit on how others constrain this.
| // lhs + (1 << LEN) - rhs | ||
| // proof: | ||
| // lhs + (1 << LEN) will add a carry bit, valued 1, to the bit array representing lhs, | ||
| // resulted in a bit array of length LEN + 1, named as sum_bits. |
There was a problem hiding this comment.
Trying to understand this but intuitively this is not going to work when we are too close to the modulus
|
|
||
| env.cached_values.insert(cache_key, res); | ||
| Ok(res) | ||
| } |
There was a problem hiding this comment.
why not a single Value::Div(VarOrCst, VarOrCst)?
|
what's the status here? Do we have these as native functions now or do we still want this PR merged? |
|
let's hold this one, until we figured out #214 |
|
Closing this, as these operators are implemented for hint functions by another PR #253 |
To support operators and apply default constraints: <, /, %, <<