Support degree ranges #1667

Schaeff · 2024-08-08T12:12:25Z

We currently hardcode the range of degrees that variable degree machines are preprocessed for. Expose that in machines instead.

This changes pil namespaces to accept a min and max degree:

namespace main(123..456);
namespace main(5); // allowed for backward compatibility, translates to `5..5`

It adds two new builtins:

std::prover::min_degree
std::prover::max_degree

And sets the behavior of the std::prover::degree builtin to only succeed if min_degree and max_degree are equal.

Pulled out of #1676, where it helps making the tests run faster. I think this could possibly be removed by #1667 again.

Schaeff · 2024-08-12T18:44:33Z

One choice we have to make is how to access the degree in the backends: currently we receive it from the pil, but with this change the pil has degree ranges. Two options:

when we modify the pil in the composite backend, replace the degree range with the single degree for that proof so we can access it like before
get the degree from somewhere else, such as the fixed columns or the verification key

The latter seems cleaner so that a single pil can support different degrees without having to be modified, but also seems like a bigger change now.

Edit: this is actually fine: the composite backend overwrites the degree ranges with the specific degree each backend operates over.

ast/src/asm_analysis/mod.rs

backend/src/composite/mod.rs

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: ```bash 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!

Pulled out of #1676, where it helps making the tests run faster. I think this could possibly be removed by #1667 again.

Small one extracted from #1667

executor/src/witgen/machines/block_machine.rs

executor/src/witgen/machines/sorted_witness_machine.rs

executor/src/witgen/machines/write_once_memory.rs

georgwiese

Cool! LGTM, just a few small comments.

georgwiese · 2024-08-21T17:22:27Z

test_data/asm/connect_no_witgen.asm

@@ -17,7 +17,7 @@ machine Empty with degree: 16 {
    let f: col = |i| i / 2;
    w = f;

-    std::check::assert(std::prover::degree() == 2**4, || "Degree is not 2**4");
+    std::check::assert(std::prover::min_degree() == 2**4, || "Degree is not 2**4");


Why this change? I don't think this would be sound for any larger degree?

Here I agree!

georgwiese · 2024-08-21T17:26:10Z

std/machines/shift.asm

@@ -16,7 +16,7 @@ machine ByteShift with

    let bit_counts = [256, 32, 4, 2];
    let min_degree = std::array::product(bit_counts);
-    std::check::assert(std::prover::degree() >= std::array::product(bit_counts), || "The shift machine needs at least 65536 rows to work.");
+    std::check::assert(std::prover::min_degree() >= std::array::product(bit_counts), || "The shift machine needs at least 65536 rows to work.");


While that is correct, I think it's actually a feature if this fails because the degree is set to a range! Wouldn't make any sense.

In the composite case, I agree with you: why would you make this trace larger than the minimum? Then we can even remove & 0xffffffff in P_C!
But in the monolithic case, we need to be able to fit an instance of this machine inside a trace of arbitrary size, which is where using min_degree and & 0xffffffff makes sense.

Right! Forgot about the monolithic case.

georgwiese · 2024-08-21T17:26:24Z

std/machines/binary.asm

@@ -15,7 +15,7 @@ machine ByteBinary with

    let bit_counts = [256, 256, 3];
    let min_degree = std::array::product(bit_counts);
-    std::check::assert(std::prover::degree() >= std::array::product(bit_counts), || "The binary machine needs at least 196608 rows to work.");
+    std::check::assert(std::prover::min_degree() >= std::array::product(bit_counts), || "The binary machine needs at least 196608 rows to work.");


Same comment as in the shift machine.

same, with inputs being defined with cross_product which internally cycles through the values

georgwiese · 2024-08-21T17:37:04Z

riscv/src/continuations.rs

@@ -113,6 +105,20 @@ where
                } else {
                    pipeline
                };
+
+                // get the length of the columns in the machine we want to extend with external witness values


Suggested change

// get the length of the columns in the machine we want to extend with external witness values

// get the length of the main machine

georgwiese · 2024-08-21T17:52:24Z

riscv/src/continuations.rs

+    {
+        n.value.clone().try_into().unwrap()
+    } else {
+        unimplemented!("Continuations rely on `Main` defining a max_degree in asm")


Would that be the problem that it's not set at all? I think it's more that it needs to be a number as opposed to a complex expression (like 2**20, which would actually make sense?).

I'm wondering if we can re-use the code from above and just request the PIL? Anyway, I think if we leave it like this, the error message could be more like it was before #1683, see this diff.

If it's not set at all, it defaults to 1 << MAX_DEGREE which is too large for the memory machine not to run out of rows. If we run this check at the pil level, then to do it properly we'd need to get the main degree, get the memory degree, and check that it's 4x. Is this what you're suggesting?

What we should to go towards is removing these defaults and move all this logic to asm, where the degree ranges would get explicitly set on the different traces so we don't need to check anything here.

georgwiese · 2024-08-21T17:59:17Z

riscv/src/code_gen.rs

+        1 << (powdr_linker::MIN_DEGREE_LOG - 2),
+        1 << (*powdr_linker::MAX_DEGREE_LOG - 2),


Suggested change

1 << (powdr_linker::MIN_DEGREE_LOG - 2),

1 << (*powdr_linker::MAX_DEGREE_LOG - 2),

1 << powdr_linker::MIN_DEGREE_LOG,

// We expect some machines (e.g. register memory) to use up to 4x the number

// of rows as main. By setting the max degree of main to be smaller by a factor

// of 4, we ensure that we don't run out of rows in those machines.

1 << (*powdr_linker::MAX_DEGREE_LOG - 2),

I don't really see a reason to set a lower min degree! That will just add commitments to tiny fixed columns to the verification key. In practice, for any computation of significant size, we'd use the max size anyway, except for the last chunk. I think we could even set it to a larger value, like 10.

There is a bad reason: if we set min and max to the same value, the linker assumes that we are in the monolithic case and sets all degrees to that same value. It's the case mentioned here which we cannot support. What we could do here is reduce the range log to (MAX_RANGE - 3)..(MAX_RANGE - 2)

Oh, but I didn't suggest setting it to the same value. Not quite sure about the tradeoffs, but I think it could be a useful feature that we can prove the last chunk (or only chunk in case of a small computation) faster because it is smaller. But going below 1 << MIN_DEGREE_LOG (=32 in practice) seems unnecessary, proving 32 rows should take no time.

Oh I misread your suggestion! Yes I agree.

georgwiese · 2024-08-21T18:30:45Z

pil-analyzer/src/condenser.rs

+        if degree.min == degree.max {
+            Ok(Value::Integer(degree.min.into()).into())
+        } else {
+            Err(EvalError::DataNotAvailable)


Is that the right error?

You can argue that it is, as the degree will eventually be known (in constant evaluation), it's just not known yet at this stage where it's still a range. We could also make it always unavailable at this stage, then that means we cannot access degree outside of constant definitions.

linker/src/lib.rs

georgwiese · 2024-08-21T18:35:45Z

linker/src/lib.rs

@@ -407,7 +446,7 @@ namespace main_sub(16);
    pc' = (1 - first_step') * pc_update;
    pol commit _output_0_free_value;
    1 $ [0, pc, instr__jump_to_operation, instr__reset, instr__loop, instr_return, _output_0_const, _output_0_read_free, read__output_0_pc, read__output_0__input_0] in main_sub__rom.latch $ [main_sub__rom.operation_id, main_sub__rom.p_line, main_sub__rom.p_instr__jump_to_operation, main_sub__rom.p_instr__reset, main_sub__rom.p_instr__loop, main_sub__rom.p_instr_return, main_sub__rom.p__output_0_const, main_sub__rom.p__output_0_read_free, main_sub__rom.p_read__output_0_pc, main_sub__rom.p_read__output_0__input_0];
-namespace main_sub__rom(8);
+namespace main_sub__rom(16);


Why did this change?

Main having a single degree triggers the monolithic mode. To be fixed properly with explicit proof objects soon.

georgwiese · 2024-08-21T19:04:31Z

asm-to-pil/src/vm_to_constrained.rs

-            .degree
-            .clone()
-            .unwrap_or_else(|| Expression::from(self.code_lines.len().next_power_of_two() as u32));
+        // this can lead to false negatives as we apply expression equality here, so `4` and `2 + 2` would be considered different.


Where do we check for expression equality?

Oh, this looks like a leftover comment of something that got moved somewhere else

Actually no, we check expression equality in is_static

georgwiese · 2024-08-26T15:33:21Z

riscv/src/continuations.rs

+
+    let length: usize = match max_degree_expr {
+        Some(Expression::Number(_, n)) => n.value.clone().try_into().unwrap(),
+        // if the max degree is not defined, it defaults to


Is this complete?

leonardoalt · 2024-09-02T08:07:43Z

conflicts

georgwiese

Let's gooo 🚀

Schaeff added 2 commits August 8, 2024 12:40

wip

148bff5

use min and max instead of enum

ba3ba4c

georgwiese mentioned this pull request Aug 12, 2024

Make MAX_DEGREE_LOG configurable #1677

Merged

github-merge-queue bot pushed a commit that referenced this pull request Aug 12, 2024

Make MAX_DEGREE_LOG configurable (#1677)

d87a33c

Pulled out of #1676, where it helps making the tests run faster. I think this could possibly be removed by #1667 again.

Schaeff added 2 commits August 12, 2024 16:30

wip

64644c3

pull main

7053b20

Schaeff added 7 commits August 13, 2024 12:10

Merge branch 'main' of github.com:powdr-labs/powdr into degree-range

3098ec7

make tests pass

1b2f372

clippy, fmt

526283b

clippy

33a5dcf

clean

39a74e9

Merge branch 'main' of github.com:powdr-labs/powdr into degree-range

cff82b4

pull main

e6d064f

Schaeff commented Aug 14, 2024

View reviewed changes

ast/src/asm_analysis/mod.rs Show resolved Hide resolved

Schaeff commented Aug 14, 2024

View reviewed changes

backend/src/composite/mod.rs Outdated Show resolved Hide resolved

georgwiese mentioned this pull request Aug 14, 2024

RISC-V machine: Use dynamic VADCOP #1683

Merged

Schaeff added 2 commits August 15, 2024 12:39

fix more tests, add min_degree and max_degree builtins

46f6668

pull main

e76cce8

Schaeff mentioned this pull request Aug 15, 2024

Use degree type where applicable #1690

Merged

Schaeff added 4 commits August 15, 2024 15:20

fix test

8b36746

pull main

94db106

fix typo

64df34a

specify range on test pil

db41e3f

topanisto pushed a commit that referenced this pull request Aug 15, 2024

Make MAX_DEGREE_LOG configurable (#1677)

380658a

Pulled out of #1676, where it helps making the tests run faster. I think this could possibly be removed by #1667 again.

github-merge-queue bot pushed a commit that referenced this pull request Aug 15, 2024

Use degree type where applicable (#1690)

b1431e5

Small one extracted from #1667

Schaeff added 2 commits August 16, 2024 12:21

fix continuations

5b6c4ae

pull main

ce67050

Schaeff commented Aug 16, 2024

View reviewed changes

executor/src/witgen/machines/block_machine.rs Show resolved Hide resolved

Schaeff commented Aug 16, 2024

View reviewed changes

executor/src/witgen/machines/sorted_witness_machine.rs Show resolved Hide resolved

Schaeff commented Aug 16, 2024

View reviewed changes

executor/src/witgen/machines/write_once_memory.rs Show resolved Hide resolved

Schaeff added 7 commits August 16, 2024 13:31

clean

2a9952e

fmt

f6fdf08

add book page

ceef184

set degree range on riscv main

156bd45

fix comment

ebac2a6

typo

a666a35

get correct length for continuations

76a94c7

Schaeff force-pushed the degree-range branch from be0ed75 to 76a94c7 Compare August 18, 2024 13:36

Merge branch 'main' of github.com:powdr-labs/powdr into degree-range

99af3c4

Schaeff marked this pull request as ready for review August 18, 2024 20:23

georgwiese reviewed Aug 21, 2024

View reviewed changes

address review comments

f4bb74b

georgwiese reviewed Aug 26, 2024

View reviewed changes

Schaeff added 4 commits August 26, 2024 21:33

address review comments

152767b

pull main

6d9a33e

add comment

d017416

fix path separator

cc5a9a9

pull main

de7bc37

georgwiese approved these changes Sep 3, 2024

View reviewed changes

Schaeff added this pull request to the merge queue Sep 3, 2024

georgwiese mentioned this pull request Sep 3, 2024

Introduce machine parts. #1743

Merged

Merged via the queue into main with commit 7f259b4 Sep 3, 2024
14 checks passed

Schaeff deleted the degree-range branch September 3, 2024 13:08

chriseth mentioned this pull request Sep 3, 2024

Replace degree, min_degree and max_degree builtins by a single builtin #1748

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Support degree ranges #1667

Support degree ranges #1667

Schaeff commented Aug 8, 2024 •

edited

Loading

Schaeff commented Aug 12, 2024 •

edited

Loading

georgwiese left a comment

georgwiese Aug 21, 2024

Schaeff Aug 22, 2024

georgwiese Aug 21, 2024

Schaeff Aug 22, 2024

georgwiese Aug 26, 2024

georgwiese Aug 21, 2024

Schaeff Aug 22, 2024 •

edited

Loading

georgwiese Aug 21, 2024

georgwiese Aug 21, 2024

Schaeff Aug 22, 2024

georgwiese Aug 21, 2024

Schaeff Aug 21, 2024 •

edited

Loading

georgwiese Aug 26, 2024

Schaeff Aug 26, 2024

georgwiese Aug 21, 2024

Schaeff Aug 22, 2024

georgwiese Aug 21, 2024

Schaeff Aug 21, 2024

georgwiese Aug 21, 2024

Schaeff Aug 21, 2024

Schaeff Aug 26, 2024

georgwiese Aug 26, 2024

Schaeff Aug 26, 2024

Schaeff Aug 26, 2024

leonardoalt commented Sep 2, 2024

georgwiese left a comment

	// get the length of the columns in the machine we want to extend with external witness values
	// get the length of the main machine

		1 << (powdr_linker::MIN_DEGREE_LOG - 2),
		1 << (*powdr_linker::MAX_DEGREE_LOG - 2),

-<< (powdr_linker::MIN_DEGREE_LOG - 2),
-<< (*powdr_linker::MAX_DEGREE_LOG - 2),
+<< powdr_linker::MIN_DEGREE_LOG,
+        // We expect some machines (e.g. register memory) to use up to 4x the number
+        // of rows as main. By setting the max degree of main to be smaller by a factor
+        // of 4, we ensure that we don't run out of rows in those machines.
+<< (*powdr_linker::MAX_DEGREE_LOG - 2),

Support degree ranges #1667

Support degree ranges #1667

Conversation

Schaeff commented Aug 8, 2024 • edited Loading

Schaeff commented Aug 12, 2024 • edited Loading

georgwiese left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Schaeff Aug 22, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Schaeff Aug 21, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

leonardoalt commented Sep 2, 2024

georgwiese left a comment

Choose a reason for hiding this comment

Schaeff commented Aug 8, 2024 •

edited

Loading

Schaeff commented Aug 12, 2024 •

edited

Loading

Schaeff Aug 22, 2024 •

edited

Loading

Schaeff Aug 21, 2024 •

edited

Loading