SRAI #463

zemse · 2024-10-25T13:00:46Z

This PR adds SRAI to shift_imm, also changes logic for SLLI and SRLI.

Closes #365

ceno_zkvm/src/chip_handler/general.rs

ceno_zkvm/src/instructions/riscv.rs

ceno_zkvm/src/instructions/riscv/srai.rs

naure · 2024-10-26T09:42:44Z

Regarding the constraints, here is a more efficient way, without division or limb decomposition.

First calculate the sign-extension, that is bits flowing in from the left.

let imm = cb.create_witin(…);    // UInt not necessary.
let ones = imm - 1;       // 2**shift - 1, or 00…111 in binary.
let inflow = msb * ones;  // Extend with 0s or 1s.

Calculate the bits flowing out to the right

// outflow < imm
AssertLTConfig::construct_circuit(…, outflow, imm, …)

Then require:

rd * imm + outflow == inflow * 2**32 + rs1

Other checks:

rs1 < 2**32 from register read.
rd < 2**32 from UInt::new.
shift < 32 from imm_or_funct7

naure · 2024-10-26T09:53:32Z

This technique can also be refactored with SRLI by setting constant inflow = 0.

hero78119 · 2024-10-26T14:20:11Z

Regarding the constraints, here is a more efficient way, without division or limb decomposition.

First calculate the sign-extension, that is bits flowing in from the left.
let imm = cb.create_witin(…);    // UInt not necessary.
let ones = imm - 1;       // 2**shift - 1, or 00…111 in binary.
let inflow = msb * ones;  // Extend with 0s or 1s.
Calculate the bits flowing out to the right
// outflow < imm
AssertLTConfig::construct_circuit(…, outflow, imm, …)
Then require:
rd * imm + outflow == inflow * 2**32 + rs1
Other checks:

rs1 < 2**32 from register read.

rd < 2**32 from UInt::new.

shift < 32 from imm_or_funct7

What an insightful observation bro!!
It taught me something new and totally changed how I see the question 😇😇

zemse · 2024-10-26T14:22:16Z

Thanks! I have updated the implementation

let imm = cb.create_witin(…); // UInt not necessary.

shift < 32 from imm_or_funct7

I had to keep imm as UInt so that it gets range checked to be under 32 bits.

naure · 2024-10-26T15:18:12Z

imm as UInt so that it gets range checked to be under 32 bits.

Unnecessary, it is a fixed value. Following the code, it will go through a cb.fetch function, where it matches the fixed column imm in the program table, which is in turn populated by imm_or_funct7, which finally computes 1 << rs1 with rs1 < 32.

naure · 2024-10-26T15:46:15Z

One more argument for soundness, both sides of the equation are 63 bits numbers (<2**63), fitting in Goldilocks.

rd * imm + outflow == inflow * 2**32 + rs1
32 + 31.      31.         31 + 32.     32.                (Bit widths)

matthiasgoergens · 2024-10-27T12:39:31Z

imm as UInt so that it gets range checked to be under 32 bits.

Unnecessary, it is a fixed value. Following the code, it will go through a cb.fetch function, where it matches the fixed column imm in the program table, which is in turn populated by imm_or_funct7, which finally computes 1 << rs1 with rs1 < 32.

Yes!

And part of that is arguably unnecessary, too.

matthiasgoergens · 2024-10-27T12:44:32Z

ceno_zkvm/src/chip_handler/general.rs

+            || "require_equal",
+            |cb| {
+                cb.cs
+                    .require_zero(name_fn, a.to_monomial_form() - b.to_monomial_form())


What does this change have to do with SRAI?

This is not related to SRAI. This is for MockProver accurate error description. The way MockProver infers assert equal is by destructuring LHS,RHS = Sum(LHS, RHS). After the monomial PR, Mock Prover is not able to infer require equal correctly because to_monomial_form is performed on Sum(LHS, RHS) the result doesn't correctly destructure to what it should be.

This change can be in other PR.

matthiasgoergens · 2024-10-27T12:45:04Z

ceno_zkvm/src/expression.rs

@@ -757,7 +757,9 @@ pub mod fmt {
    ) -> String {
        match expression {
            Expression::WitIn(wit_in) => {
-                wtns.push(*wit_in);
+                if !wtns.contains(wit_in) {


What does this change have to do with SRAI?

Seems like an unrelated improvement?

This is not related to SRAI. If Wtns(x) appears multiple times in the expression, then it is duplicated.

This change can be in other PR.

I'm happy to review that extracted PR fast.

Putting unrelated changes in their own PR is best; but as a second best alternative you can also expand the PR description for this PR to include the additional unrelated changes.

zemse · 2024-10-27T18:36:32Z

Changing imm to WitIn requires impl of UInt x WitIn (currently we just support muliply of UInt and UInt) since that is needed in SLLI. Do you think it can be followed up in other PR?

matthiasgoergens · 2024-10-27T23:50:58Z

Changing imm to WitIn requires impl of UInt x WitIn (currently we just support muliply of UInt and UInt) since that is needed in SLLI. Do you think it can be followed up in other PR?

Why don't you get that other PR into master first, if that's useful, and built this PR on that one?

naure · 2024-10-28T06:50:09Z

UInt x WitIn

That's uint.value() * witin.expr()

~~But yes that can be done in a follow up PR.~~

Already done.

hero78119

A quick review went through.
👍 Per offline discussion, make SLLI follow in/out flow and the final config sharing with same imm as witin is nice

ceno_zkvm/src/instructions/riscv/shift_imm.rs

naure

Nice implementation of the arithmetic approach and nice refactoring of all three instructions!

hero78119

LGTM!

Copy-and-paste coding, again. See 47f5572 / #463

matthiasgoergens · 2024-10-28T10:29:28Z

ceno_zkvm/src/instructions/riscv/shift_imm.rs

+        let outflow = match I::INST_KIND {
+            InsnKind::SLLI => (rs1_read.as_u64() * imm as u64) >> UInt::<E>::TOTAL_BITS,
+            InsnKind::SRAI | InsnKind::SRLI => {
+                if I::INST_KIND == InsnKind::SRAI {


Why do you mix pattern matching with if?

matthiasgoergens · 2024-10-28T10:32:08Z

ceno_zkvm/src/instructions/riscv/shift_imm.rs

+            InsnKind::SRAI | InsnKind::SRLI => {
+                if I::INST_KIND == InsnKind::SRAI {
+                    let max_signed_limb_expr = (1 << (UInt::<E>::LIMB_BITS - 1)) - 1;
+                    config.is_lt_config.as_ref().unwrap().assign_instance(


@hero78119 We are freely mixing .unwrap()s into our code. We pay the mental tax for the extra complexity of the Result wrapper but don't actually use it.

(The unwrap might even be justified here. It's honestly hard to tell.)

Copy-and-paste coding, again. See 47f5572 / #463 This PR only patches up the unnecessary clone, it doesn't fix the code-duplication-with-small-variations that's the actual problem with our pervasive copy-and-paste culture.

To close #143 and catch up milestone - [x] unify existing SLL/SRL to in/out flow, following #463, which save bunch of witins allocation. - [x] on top of in/out flow, implementing SRA opcode - [x] documentation on in/out flow

zemse requested a review from hero78119 October 25, 2024 13:35

naure reviewed Oct 25, 2024

View reviewed changes

zemse added 7 commits October 26, 2024 00:11

first pass - works for positive

f8d6225

working

bf8e157

clippy

a93b505

update comment

c5b2b20

undo temp change

618a13c

move srai to shift_imm

41b4c32

rm require_bool

764ea38

zemse force-pushed the srai branch from c386253 to 764ea38 Compare October 25, 2024 19:08

zemse added 2 commits October 26, 2024 00:43

change annotation

8a831d7

nit picks

4ad95ae

naure mentioned this pull request Oct 26, 2024

Revisit the set of tables #408

Open

use new approach on srai

867ce46

combine with srli

7e9911f

zemse added 2 commits October 26, 2024 19:54

rm unnessary util

ee4737c

avoid msb config in srli

de1c98f

matthiasgoergens reviewed Oct 27, 2024

View reviewed changes

change SLLI logic

2ecb01a

naure approved these changes Oct 28, 2024

View reviewed changes

hero78119 reviewed Oct 28, 2024

View reviewed changes

naure requested changes Oct 28, 2024

View reviewed changes

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

zemse added 6 commits October 28, 2024 13:00

outflow < imm

e881bb5

use IsLtConfig instead of MsbConfig

4fdbee1

refactor constant

5214ebe

refactor out common things

fe39ba4

rm msb extensions

d1bdc66

revert mock prover improvements

fab50fa

zemse requested review from naure, hero78119 and matthiasgoergens October 28, 2024 08:28

hero78119 mentioned this pull request Oct 28, 2024

Unify signed bit extraction via gadget #482

Closed

naure approved these changes Oct 28, 2024

View reviewed changes

use constants

2f8fa7d

hero78119 approved these changes Oct 28, 2024

View reviewed changes

hero78119 enabled auto-merge (squash) October 28, 2024 10:03

hero78119 merged commit 47f5572 into scroll-tech:master Oct 28, 2024
6 checks passed

matthiasgoergens added a commit that referenced this pull request Oct 28, 2024

Remove unnecessary clones

8b53f73

Copy-and-paste coding, again. See 47f5572 / #463

matthiasgoergens mentioned this pull request Oct 28, 2024

Remove unnecessary clones #484

Merged

matthiasgoergens reviewed Oct 28, 2024

View reviewed changes

hero78119 mentioned this pull request Oct 30, 2024

SRA opcode impl and shift logic circuit optimisation #505

Merged

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

SRAI #463

SRAI #463

zemse commented Oct 25, 2024 •

edited

Loading

naure commented Oct 26, 2024 •

edited

Loading

naure commented Oct 26, 2024

hero78119 commented Oct 26, 2024

zemse commented Oct 26, 2024

naure commented Oct 26, 2024

naure commented Oct 26, 2024

matthiasgoergens commented Oct 27, 2024

matthiasgoergens Oct 27, 2024

zemse Oct 27, 2024

matthiasgoergens Oct 27, 2024

zemse Oct 27, 2024

matthiasgoergens Oct 27, 2024

matthiasgoergens Oct 27, 2024

zemse commented Oct 27, 2024

matthiasgoergens commented Oct 27, 2024 •

edited

Loading

naure commented Oct 28, 2024 •

edited

Loading

hero78119 left a comment

naure left a comment

hero78119 left a comment

matthiasgoergens Oct 28, 2024

matthiasgoergens Oct 28, 2024 •

edited

Loading

SRAI #463

SRAI #463

Conversation

zemse commented Oct 25, 2024 • edited Loading

naure commented Oct 26, 2024 • edited Loading

naure commented Oct 26, 2024

hero78119 commented Oct 26, 2024

zemse commented Oct 26, 2024

naure commented Oct 26, 2024

naure commented Oct 26, 2024

matthiasgoergens commented Oct 27, 2024

matthiasgoergens Oct 27, 2024

Choose a reason for hiding this comment

zemse Oct 27, 2024

Choose a reason for hiding this comment

matthiasgoergens Oct 27, 2024

Choose a reason for hiding this comment

zemse Oct 27, 2024

Choose a reason for hiding this comment

matthiasgoergens Oct 27, 2024

Choose a reason for hiding this comment

matthiasgoergens Oct 27, 2024

Choose a reason for hiding this comment

zemse commented Oct 27, 2024

matthiasgoergens commented Oct 27, 2024 • edited Loading

naure commented Oct 28, 2024 • edited Loading

hero78119 left a comment

Choose a reason for hiding this comment

naure left a comment

Choose a reason for hiding this comment

hero78119 left a comment

Choose a reason for hiding this comment

matthiasgoergens Oct 28, 2024

Choose a reason for hiding this comment

matthiasgoergens Oct 28, 2024 • edited Loading

Choose a reason for hiding this comment

zemse commented Oct 25, 2024 •

edited

Loading

naure commented Oct 26, 2024 •

edited

Loading

matthiasgoergens commented Oct 27, 2024 •

edited

Loading

naure commented Oct 28, 2024 •

edited

Loading

matthiasgoergens Oct 28, 2024 •

edited

Loading