RISC-V machine: Use dynamic VADCOP #1683

georgwiese · 2024-08-13T15:37:02Z

Builds on #1687
Fixed #1572

With this PR, we are using dynamic VADCOP in the RISC-V zk-VM.

There were a few smaller fixes needed to make this work. In summary, the changes are as follows:

We set the degree the main machine to None, and all fixed lookup machines to the appropriate size. As a consequence, the CPU, all block machines & memory have a dynamic size.
As a consequence, I had to adjust some tests (set the size of all machines, so they can still be run with monolithic provers) and was able to remove the Memory_<size> machines 🎉
With the main machine being of flexible size, the prover can chose for how long to run it. We run it for 1 << (MAX_DEGREE_LOG - 2) steps and compute the bootloader inputs accordingly. With this choice, we can guarantee that the register memory (which can be up to 4x larger than the main machine) does not run out of rows.

Note that while we do access MAX_DEGREE_LOG in a bunch of places now, this will go away once #1667 is merged, which will allow us to configure the degree range in ASM and for each machine individually.

Example:

export MAX_LOG_DEGREE=18
cargo run -r --bin powdr-rs compile riscv/tests/riscv_data/many_chunks -o output --continuations
cargo run -r --bin powdr-rs execute output/many_chunks.asm -o output --continuations -w
cargo run -r --features plonky3,halo2 prove output/many_chunks.asm -d output/chunk_0 --field gl --backend plonky3-composite

This leads to the following output:

== Proving machine: main (size 65536), stage 0
==> Proof stage computed in 1.918317417s
== Proving machine: main__rom (size 8192), stage 0
==> Proof stage computed in 45.847375ms
== Proving machine: main_binary (size 1024), stage 0
==> Proof stage computed in 27.718416ms
== Proving machine: main_bit2 (size 4), stage 0
==> Proof stage computed in 15.280667ms
== Proving machine: main_bit6 (size 64), stage 0
==> Proof stage computed in 17.449875ms
== Proving machine: main_bit7 (size 128), stage 0
==> Proof stage computed in 20.717834ms
== Proving machine: main_bootloader_inputs (size 262144), stage 0
==> Proof stage computed in 524.013375ms
== Proving machine: main_byte (size 256), stage 0
==> Proof stage computed in 17.280167ms
== Proving machine: main_byte2 (size 65536), stage 0
==> Proof stage computed in 164.709625ms
== Proving machine: main_byte_binary (size 262144), stage 0
==> Proof stage computed in 504.743917ms
== Proving machine: main_byte_compare (size 65536), stage 0
==> Proof stage computed in 169.881542ms
== Proving machine: main_byte_shift (size 65536), stage 0
==> Proof stage computed in 146.235916ms
== Proving machine: main_memory (size 32768), stage 0
==> Proof stage computed in 326.522167ms
== Proving machine: main_poseidon_gl (size 16384), stage 0
==> Proof stage computed in 1.324662625s
== Proving machine: main_regs (size 262144), stage 0
==> Proof stage computed in 2.009408667s
== Proving machine: main_shift (size 32), stage 0
==> Proof stage computed in 13.71825ms
== Proving machine: main_split_gl (size 16384), stage 0
==> Proof stage computed in 108.019334ms
Proof generation took 7.364567s
Proof size: 8432928 bytes
Writing output/chunk_0/many_chunks_proof.bin.

Note that main_bootloader_inputs is still equal to the maximum size, we should fix that in a following PR!

When making fixed lookup machines smaller in the RISC-V VM (#1683), I came across the issue that range-constraint lookups (e.g. `[two_bits] in [TWO_BITS]` where `TWO_BITS = [0, 1, 2, 3]`) where not recognized as such if the fixed column was *just* the right size (in the above example, `TWO_BITS = [0, 1, 2, 3, 0]` would have worked).

georgwiese · 2024-08-14T20:07:07Z

executor/src/witgen/mod.rs

-                            if let Some(external_values) = &external_values {
-                                if external_values.len() != poly.degree.unwrap() as usize {
-                                    log::debug!(
-                                        "External witness values for column {} were only partially provided \
-                                        (length is {} but the degree is {})",
-                                        name,
-                                        external_values.len(),
-                                        poly.degree.unwrap()
-                                    );
-                                }
-                            }


We can't really check this easily anymore with dynamic sizes, and it was only a debug log anyway.

georgwiese · 2024-08-14T20:09:25Z

.github/workflows/pr-tests.yml

@@ -11,7 +11,7 @@ on:
 env:
  CARGO_TERM_COLOR: always
  POWDR_GENERATE_PROOFS: "true"
-  MAX_DEGREE_LOG: "10"
+  MAX_DEGREE_LOG: "20"


Had to increase, because otherwise the RISC-V tests would run only for 256 rows... Now, it is $2^{18}$, as before this PR. It doesn't seem like it has a big impact on test time (we don't have too many dynamic VADCOP tests and the RISC-V tests are slow anyway).

we should also add log 22 tests at some point

After #1667, we can configure the range for each test and machine individually, should be much better than this global setting.

leonardoalt · 2024-08-15T08:56:04Z

executor/src/witgen/vm_processor.rs

@@ -66,17 +66,17 @@ pub struct VmProcessor<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> {
 }

 impl<'a, 'b, 'c, T: FieldElement, Q: QueryCallback<T>> VmProcessor<'a, 'b, 'c, T, Q> {
+    #[allow(clippy::too_many_arguments)]


leonardoalt

Awesome!

Pulled out of #1683 Because our memory machine requires a `Byte2` machine to range-check some values, we need to provide that machine in any test that uses memory. But that machine needs a size of $2^{16}$, which is a lot for just some simple tests. Previously, the `Byte2` machine did not have a size set (this will change in #1683), so it would just get the size of the main machine. This works because in our simple tests, the values are small enough in practice. But really, this breaks an assumption of the `Byte2` machine. With this PR, this is explicit, with all the affected test (that we want to keep small) using `std::machines::test_util::FakeByte2` instead of `std::machines::range::Byte2`. Note that this is exploiting the fact that we're not type checking the machine passed to memory. But the alternative would be to copy the memory machine and use that in the test.

The base branch was changed.

leonardoalt · 2024-08-15T09:26:31Z

has conflicts now

georgwiese · 2024-08-15T09:48:05Z

has conflicts now

I rebased onto main (works much better than merge when a branch you were building on was merged...)

georgwiese mentioned this pull request Aug 14, 2024

Witgen: Recognize range constraints in more cases #1685

Merged

georgwiese force-pushed the riscv-dynamic-vadcop branch from 639b21a to 49ee814 Compare August 14, 2024 13:28

georgwiese changed the base branch from main to fix-range-constraint-detection August 14, 2024 13:29

georgwiese force-pushed the fix-range-constraint-detection branch from 080adf2 to e17c57b Compare August 14, 2024 13:36

georgwiese force-pushed the riscv-dynamic-vadcop branch from 49ee814 to 486facf Compare August 14, 2024 13:38

Base automatically changed from fix-range-constraint-detection to main August 14, 2024 14:26

georgwiese force-pushed the riscv-dynamic-vadcop branch 2 times, most recently from 197047e to a022fa3 Compare August 14, 2024 14:37

georgwiese changed the base branch from main to fake-byte2 August 14, 2024 14:37

georgwiese mentioned this pull request Aug 14, 2024

Introduce FakeByte2 of a fixed degree #1687

Merged

georgwiese commented Aug 14, 2024

View reviewed changes

georgwiese changed the title ~~[WIP] RISC-V machine: Use dynamic VADCOP~~ RISC-V machine: Use dynamic VADCOP Aug 14, 2024

georgwiese marked this pull request as ready for review August 14, 2024 20:11

leonardoalt reviewed Aug 15, 2024

View reviewed changes

leonardoalt previously approved these changes Aug 15, 2024

View reviewed changes

Base automatically changed from fake-byte2 to main August 15, 2024 09:08

georgwiese added 9 commits August 15, 2024 11:45

RISC-V machine: Use dynamic VADCOP

f9e8fdb

Make fixed lookup machines only as big as needed

4bb7430

Fix binary_test

53eee11

Make continuations work

7783a56

Clippy

2a0a531

Increment MAX_DEGREE_LOG

2bebc5a

Increment MAX_DEGREE_LOG

77dfff7

Bug fix

856fa8f

Increment MAX_DEGREE_LOG

bea6652

Polish

f50c62e

georgwiese force-pushed the riscv-dynamic-vadcop branch from 6fc9231 to f50c62e Compare August 15, 2024 09:45

georgwiese enabled auto-merge August 15, 2024 10:12

leonardoalt approved these changes Aug 15, 2024

View reviewed changes

georgwiese added this pull request to the merge queue Aug 15, 2024

Merged via the queue into main with commit 34fdbd1 Aug 15, 2024
14 checks passed

georgwiese deleted the riscv-dynamic-vadcop branch August 15, 2024 12:00

georgwiese mentioned this pull request Aug 21, 2024

Support degree ranges #1667

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

RISC-V machine: Use dynamic VADCOP #1683

RISC-V machine: Use dynamic VADCOP #1683

georgwiese commented Aug 13, 2024 •

edited

Loading

georgwiese Aug 14, 2024

georgwiese Aug 14, 2024

leonardoalt Aug 15, 2024

georgwiese Aug 15, 2024

leonardoalt Aug 15, 2024

leonardoalt left a comment

leonardoalt commented Aug 15, 2024

georgwiese commented Aug 15, 2024

RISC-V machine: Use dynamic VADCOP #1683

RISC-V machine: Use dynamic VADCOP #1683

Conversation

georgwiese commented Aug 13, 2024 • edited Loading

Example:

georgwiese Aug 14, 2024

Choose a reason for hiding this comment

georgwiese Aug 14, 2024

Choose a reason for hiding this comment

leonardoalt Aug 15, 2024

Choose a reason for hiding this comment

georgwiese Aug 15, 2024

Choose a reason for hiding this comment

leonardoalt Aug 15, 2024

Choose a reason for hiding this comment

leonardoalt left a comment

Choose a reason for hiding this comment

leonardoalt commented Aug 15, 2024

georgwiese commented Aug 15, 2024

georgwiese commented Aug 13, 2024 •

edited

Loading