mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-04-20 03:03:25 -04:00
34fdbd1ccd
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!
69 lines
1.7 KiB
Rust
69 lines
1.7 KiB
Rust
use std::machines::binary::ByteBinary;
|
|
use std::machines::binary::Binary;
|
|
|
|
machine Main with degree: 262144 {
|
|
reg pc[@pc];
|
|
reg X0[<=];
|
|
reg X1[<=];
|
|
reg X2[<=];
|
|
reg A;
|
|
|
|
ByteBinary byte_binary;
|
|
Binary binary(byte_binary);
|
|
|
|
instr and X0, X1 -> X2 link ~> X2 = binary.and(X0, X1);
|
|
instr or X0, X1 -> X2 link ~> X2 = binary.or(X0, X1);
|
|
instr xor X0, X1 -> X2 link ~> X2 = binary.xor(X0, X1);
|
|
|
|
instr assert_eq X0, X1 {
|
|
X0 = X1
|
|
}
|
|
|
|
function main {
|
|
|
|
// AND
|
|
A <== and(0, 0);
|
|
assert_eq A, 0;
|
|
A <== and(0xffffffff, 0xffffffff);
|
|
assert_eq A, 0xffffffff;
|
|
A <== and(0xffffffff, 0xabcdef01);
|
|
assert_eq A, 0xabcdef01;
|
|
A <== and(0xabcdef01, 0xffffffff);
|
|
assert_eq A, 0xabcdef01;
|
|
A <== and(0, 0xabcdef01);
|
|
assert_eq A, 0;
|
|
A <== and(0xabcdef01, 0);
|
|
assert_eq A, 0;
|
|
|
|
// OR
|
|
A <== or(0, 0);
|
|
assert_eq A, 0;
|
|
A <== or(0xffffffff, 0xffffffff);
|
|
assert_eq A, 0xffffffff;
|
|
A <== or(0xffffffff, 0xabcdef01);
|
|
assert_eq A, 0xffffffff;
|
|
A <== or(0xabcdef01, 0xffffffff);
|
|
assert_eq A, 0xffffffff;
|
|
A <== or(0, 0xabcdef01);
|
|
assert_eq A, 0xabcdef01;
|
|
A <== or(0xabcdef01, 0);
|
|
assert_eq A, 0xabcdef01;
|
|
|
|
// XOR
|
|
A <== xor(0, 0);
|
|
assert_eq A, 0;
|
|
A <== xor(0xffffffff, 0xffffffff);
|
|
assert_eq A, 0;
|
|
A <== xor(0xffffffff, 0xabcdef01);
|
|
assert_eq A, 0x543210fe;
|
|
A <== xor(0xabcdef01, 0xffffffff);
|
|
assert_eq A, 0x543210fe;
|
|
A <== xor(0, 0xabcdef01);
|
|
assert_eq A, 0xabcdef01;
|
|
A <== xor(0xabcdef01, 0);
|
|
assert_eq A, 0xabcdef01;
|
|
|
|
return;
|
|
}
|
|
}
|