Implement SRL and SLL #304
Conversation
|
@KimiWu123 in this PR, Soham find a underconstrain situation, where we should constrain remainder < quotient.
Thus, I introduced cc @zemse for review |
|
### Desc. ~~This PR is trying to integrate `DivConfig` introduced in #304 into `divu` opcode. However,`DivConfig` fails when `divisor` is zero.~~ ### Findings ~~`assert_less_than` should be `None` in this case since both of `lhs: remainder` and `rhs: divisor` are witnesses and range-checked.~~ https://github.com/scroll-tech/ceno/blob/77a250c9e7988e6d126154c34396912721394dfe/ceno_zkvm/src/gadgets/div.rs#L44-L50 ---- ### Update ~~In the first place, this PR is trying to fix a failure when `divisor` is zero. During fixing this issue, realized we don't really need `DivConfig` since there are not much duplicated code between `SRL` and `DIVU`. Therefore, we don't really need to "fix" this issue since it works well on `SRL`. But I need to add "remainder < divisor" constraints in `DIVU`.~~ I was trying to use `DivConfig` in this PR, but it made more complicated code. So, the current version is only to add `remainder < divisor` constraints in `divu`. ### Changes - Fixing under constraints in `less_than` - Adding "remainder < divisor" constraint in `divu` - Adding some tests for `SRL` and `SLL` --------- Co-authored-by: Ming <[email protected]>
Closes #282 and #123