Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

bgillesp · 2024-11-18T15:05:24Z

This PR extends the existing DIVU opcode implementation to expose the remainder as an output, and to handle the (more complicated) signed case. See the comments in div.rs for details, but in summary:

The basic design of signed and unsigned DIV and REM opcode circuits is to represent the division algorithm relation dividend = quotient * divisor + remainder using native field elements, and constraining so that either 0 <= remainder < divisor or divisor == 0 holds.
Some nontrivial steps are needed in the signed case to handle the additional complexity of different signs for the divisor and remainder values, as well as to handle signed division overflow where -2^31 / -1 = 2^31 is out of the representable range for i32 values.
In either case, either the quotient or the remainder value is exposed as the output register rd.
In theory with the current implementation, consecutive calls to DIV and REM or DIVU and REMU could be batched into a single circuit since both of the outputs are represented; however, this is not yet implemented.

Currently the circuit implementation and documentation are finished and ready for review. Unit tests still need to be finished, but it would be great to get some eyes on the circuit design now.

kunxian-xia · 2024-12-10T02:17:49Z

@bgillesp when will this pr be ready for review?

bgillesp · 2024-12-10T16:25:37Z

Unit tests still need to be added for the new opcode circuits, but everything else is in shape for an initial review -- will change the PR out of Draft now.

Implementing a TODO from #596

ceno_zkvm/src/gadgets/is_lt.rs

To help make #596 easier to read and reason about.

To make the diff for #596 easier to read.

matthiasgoergens

A few comments and suggestions so far.

ceno_zkvm/src/gadgets/signed.rs

ceno_zkvm/src/gadgets/signed_ext.rs

ceno_zkvm/src/instructions/riscv/div.rs

To make the diff for #596 easier to read.

matthiasgoergens · 2024-12-11T03:02:43Z

@bgillesp I made a version of this PR that has an easier to read diff and left some comments there. They apply here as well. See #734

hero78119 · 2024-12-11T03:06:42Z

Attach DIVU circuit statistics 🔥

First row master branch, second row this PR

+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| opcode_name   | num_instances | lookups | reads | witnesses | writes | 0_expr_deg | 0_expr_sumcheck_deg |
+---------------+---------------+---------+-------+-----------+--------+------------+---------------------+
| DIVU          | 0             | 21      | 4     | 37        | 4      | [1: 7]     | [2: 8]              | 
| DIVU          | 0             | 13      | 4     | 29        | 4      | [1: 5]     | [2: 5]              |

hero78119

Epic job! thanks for the implementation and clear documentation.
Just do a quick overview and will proceed arithmetics constrain review 2nd round

ceno_zkvm/src/gadgets/signed_ext.rs

ceno_zkvm/src/gadgets/signed.rs

ceno_zkvm/src/instructions/riscv/div.rs

…opcodes The current implementation tries to be generic over different UInt widths, but the circuit design soundness relies on specifically using 32-bit registers in the Goldilocks field, so it doesn't make sense to sacrifice readability for unused generality here.

…lity

…tion

… versions

…ded value The current assumption of the circuit design is that n_bits has to be 8 or 16, so this change will better flag violations of this assumption if we end up changing the base limb size to 32 bits.

bgillesp · 2024-12-11T18:13:38Z

Thank you for the generous feedback everyone! 🙏 I think I've addressed your comments as much as I can currently -- will keep an eye on this space to help move things forward as the review progresses.

To help make #596 easier to read and reason about. Also introduce a few more conversion helpers.

KimiWu123 · 2024-12-12T02:39:52Z

ceno_zkvm/src/instructions/riscv/div.rs

+                let neg_div_expr = {
+                    let a_neg = dividend_signed.is_negative.expr();
+                    let b_neg = divisor_signed.is_negative.expr();
+                    &a_neg * (1 - &b_neg) + (1 - &a_neg) * &b_neg


Really minor one, I like the original style more because It's clear and slightly efficient. It reduces the number of recursion here. But it depends on you :)

// a_neg * (1 - b_neg) + (1 - a_neg) * b_neg (a_neg.clone() + b_neg.clone()) - (Expression::<E>::from(2) * a_neg * b_neg)

Yeah, I think the fact that it was simplified to monomial form was why I went with the original version, but then the current revision is closer to the underlying logic of the expression, which gives an easily readable meaning for binary inputs. I don't think I have a strong opinion about it -- any thoughts @matthiasgoergens since the change was your suggestion?

There are two parts to my suggestion. One is to remove the manual clones, and the other is to use a simpler algebraic expression.

They are independent of each other.

I don't really have much of an opinion on whether (a + b - 2 * a * b) or a * (1 - b) + (1 - a) * b is easier to read. I went with the latter, because someone had made a comment // a_neg * (1 - b_neg) + (1 - a_neg) * b_neg to that end; so I assume someone thought that form is easier to read.

Here's my suggestion, if you want to use the original expression:

// a_neg xor b_neg &a_neg + &b_neg - 2 * a_neg * b_neg

@KimiWu123 Btw, when you say 'efficient', do you mean that the distribution function will be called slightly less often; or do you mean that the final resulting expression will be different?

Sure, this seems also like a good way to write it, with the simple comment -- updated to this version in the latest commit.

KimiWu123 · 2024-12-12T02:40:52Z

ceno_zkvm/src/instructions/riscv/div.rs


        Ok(())
    }
 }

+// TODO Tests


I guess you forgot this TODO. I didn't see any testing added.

Not forgotten! I mentioned that this is still TODO in the PR description -- another member of our team is working on it, but paused yesterday due to the rapid changes from the review. Should be finished relatively soon, but probably an initial review of the circuit design would still be valuable at this point before we validate with unit tests.

Implementing a TODO from #596

To make the diff for scroll-tech#596 easier to read.

To help make scroll-tech#596 easier to read and reason about. Also introduce a few more conversion helpers.

Implementing a TODO from scroll-tech#596

bgillesp · 2024-12-13T18:45:24Z

Note that while commit e719763 is showing failed tests, the cargo make tests command runs successfully on my local build, so I'm guessing it might be something stalled on the CI end.

matthiasgoergens · 2024-12-15T00:12:13Z

Note that while commit e719763 is showing failed tests, the cargo make tests command runs successfully on my local build, so I'm guessing it might be something stalled on the CI end.

I clicked the button to kick off a re-run of the tests. (Is that button available for you?)

matthiasgoergens

Thanks for your patience with the review process. Looking good now.

Please remove the now obsolete TODO about the LT -> Lt rename before merging.

matthiasgoergens · 2024-12-15T01:42:27Z

ceno_zkvm/src/gadgets/is_lt.rs

@@ -18,6 +18,7 @@ use crate::{

 use super::SignedExtendConfig;

+// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions


Suggested change

// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions

matthiasgoergens · 2024-12-15T01:45:41Z

ceno_zkvm/src/instructions/riscv/div.rs

+                    is_dividend_max_negative.expr() * is_divisor_minus_one.expr(),
+                )?;
+
+                // For signed division overflow, dividend = -2^31 and divisor


I suspect we actually might be able to get away without any special handling of signed division overflow (and just get the right answer out of the general constraints).

But that's something for me to think about later, nothing that should hold up this PR.

My suspicion is because we have more range available in Goldilocks, and (i32::MIN as Goldilocks) / (-1) == 1<<31 as Goldilocks, which is the answer we want at the end.

Bryan Gillespie added 2 commits November 15, 2024 11:34

Move Signed gadget from MULH opcode to gadgets submodule

4fb46a4

Extend DIVU gadget implementation to support REMU/DIV/REM opcodes

2812c12

This was linked to issues Nov 19, 2024

remu #590

Open

div #588

Open

rem #589

Open

mcalancea self-assigned this Dec 6, 2024

Bryan Gillespie added 6 commits December 6, 2024 13:36

Format updates

6919ece

Merge branch 'master' into bg/div-rem-remu-opcodes

754a75d

A few DIV opcode circuit fixes, documentation, and vm integration

b9be2fc

Rename divu.rs to div.rs and add check for Goldilocks field

22bc22a

Small reformatting and doc improvements

4c11b43

Merge branch 'master' into bg/div-rem-remu-opcodes

277fd77

kunxian-xia requested a review from naure December 10, 2024 02:17

bgillesp changed the title ~~[WIP] Feat/Opcode Circuits for DIV, REM, and REMU opcodes~~ Feat/Opcode Circuits for DIV, REM, and REMU opcodes Dec 10, 2024

bgillesp marked this pull request as ready for review December 10, 2024 16:25

Bryan Gillespie added 2 commits December 10, 2024 09:38

Formatting fix

36c2af4

Fix a couple of missed changes in rv32im.rs needed for new opcodes

3e7931b

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Rename AssertLTConfig to AssertLtConfig

9878cc8

Implementing a TODO from #596

matthiasgoergens mentioned this pull request Dec 11, 2024

Rename AssertLTConfig to AssertLtConfig #731

Merged

matthiasgoergens reviewed Dec 11, 2024

View reviewed changes

ceno_zkvm/src/gadgets/is_lt.rs Show resolved Hide resolved

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Introduce Value::as_i32

ed6797b

To help make #596 easier to read and reason about.

matthiasgoergens mentioned this pull request Dec 11, 2024

Introduce Value::as_i32 #732

Merged

matthiasgoergens added a commit that referenced this pull request Dec 11, 2024

Rename mod divu to mod div

0af1111

To make the diff for #596 easier to read.

matthiasgoergens mentioned this pull request Dec 11, 2024

Rename mod divu to mod div #733

Merged

matthiasgoergens reviewed Dec 11, 2024

View reviewed changes

kunxian-xia pushed a commit that referenced this pull request Dec 11, 2024

Rename mod divu to mod div (#733)

a879b84

To make the diff for #596 easier to read.

hero78119 reviewed Dec 11, 2024

View reviewed changes

ceno_zkvm/src/gadgets/signed_ext.rs Show resolved Hide resolved

ceno_zkvm/src/gadgets/signed.rs Outdated Show resolved Hide resolved

ceno_zkvm/src/instructions/riscv/div.rs Outdated Show resolved Hide resolved

Bryan Gillespie added 15 commits December 11, 2024 07:39

Fix bug in signed remainder construction

7821de4

Small comment fixes

23e6421

Update UInt assignment in DIV opcodes to use assign_value function

eb0a117

Change unnecessary generic constant with hard-coded value for readabi…

4425c13

…lity

Merge branch 'master' into bg/div-rem-remu-opcodes

0158e01

Change Signed circuit to use bit shift directly on expression

54bf10c

Small updates based on PR comments

92bce79

Fix assignment to remainder_nonnegative in DIV/REM opcodes circuit

8317a28

Simplify syntax for a few Expression definitions

0c3f5ed

Remove a few unnecessary type annotations

41e3e19

Use built-in arithmetic calls for unsigned quotient/remainder computa…

137964a

…tion

Simplify variables in signed DIV/REM assignment by shadowing unsigned…

0f71c30

… versions

Use parameter for limb size in SignedExtendConfig rather than hard-co…

124d623

…ded value The current assumption of the circuit design is that n_bits has to be 8 or 16, so this change will better flag violations of this assumption if we end up changing the base limb size to 32 bits.

Revise Signed val construction to use relevant UInt utility function

833dbca

matthiasgoergens added a commit that referenced this pull request Dec 12, 2024

Introduce Value::as_i32 (#732)

2cd6a6d

To help make #596 easier to read and reason about. Also introduce a few more conversion helpers.

KimiWu123 reviewed Dec 12, 2024

View reviewed changes

Merge branch 'master' into bg/div-rem-remu-opcodes

5947d99

matthiasgoergens added a commit that referenced this pull request Dec 12, 2024

Rename AssertLTConfig to AssertLtConfig (#731)

35b352e

Implementing a TODO from #596

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Rename mod divu to mod div (scroll-tech#733)

cf15c14

To make the diff for scroll-tech#596 easier to read.

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Introduce Value::as_i32 (scroll-tech#732)

e28e557

To help make scroll-tech#596 easier to read and reason about. Also introduce a few more conversion helpers.

10to4 pushed a commit to 10to4/ceno that referenced this pull request Dec 12, 2024

Rename AssertLTConfig to AssertLtConfig (scroll-tech#731)

5077eb1

Implementing a TODO from scroll-tech#596

Bryan Gillespie added 2 commits December 13, 2024 10:31

Merge branch 'master' into bg/div-rem-remu-opcodes

19647e0

Change way that expression for neg_div_expr is written

e719763

matthiasgoergens approved these changes Dec 15, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

bgillesp commented Nov 18, 2024 •

edited

Loading

kunxian-xia commented Dec 10, 2024

bgillesp commented Dec 10, 2024

matthiasgoergens left a comment

matthiasgoergens commented Dec 11, 2024

hero78119 commented Dec 11, 2024 •

edited

Loading

hero78119 left a comment

bgillesp commented Dec 11, 2024

KimiWu123 Dec 12, 2024

bgillesp Dec 12, 2024

matthiasgoergens Dec 12, 2024 •

edited

Loading

bgillesp Dec 13, 2024

KimiWu123 Dec 12, 2024

bgillesp Dec 12, 2024

bgillesp commented Dec 13, 2024

matthiasgoergens commented Dec 15, 2024

matthiasgoergens left a comment

matthiasgoergens Dec 15, 2024

matthiasgoergens Dec 15, 2024

		@@ -18,6 +18,7 @@ use crate::{

		use super::SignedExtendConfig;

		// TODO rename to AssertLtConfig (LT -> Lt) to fit naming conventions

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Are you sure you want to change the base?

Feat/Opcode Circuits for DIV, REM, and REMU opcodes #596

Conversation

bgillesp commented Nov 18, 2024 • edited Loading

kunxian-xia commented Dec 10, 2024

bgillesp commented Dec 10, 2024

matthiasgoergens left a comment

Choose a reason for hiding this comment

matthiasgoergens commented Dec 11, 2024

hero78119 commented Dec 11, 2024 • edited Loading

hero78119 left a comment

Choose a reason for hiding this comment

bgillesp commented Dec 11, 2024

KimiWu123 Dec 12, 2024

Choose a reason for hiding this comment

bgillesp Dec 12, 2024

Choose a reason for hiding this comment

matthiasgoergens Dec 12, 2024 • edited Loading

Choose a reason for hiding this comment

bgillesp Dec 13, 2024

Choose a reason for hiding this comment

KimiWu123 Dec 12, 2024

Choose a reason for hiding this comment

bgillesp Dec 12, 2024

Choose a reason for hiding this comment

bgillesp commented Dec 13, 2024

matthiasgoergens commented Dec 15, 2024

matthiasgoergens left a comment

Choose a reason for hiding this comment

matthiasgoergens Dec 15, 2024

Choose a reason for hiding this comment

matthiasgoergens Dec 15, 2024

Choose a reason for hiding this comment

bgillesp commented Nov 18, 2024 •

edited

Loading

hero78119 commented Dec 11, 2024 •

edited

Loading

matthiasgoergens Dec 12, 2024 •

edited

Loading