mirror of
https://github.com/powdr-labs/powdr.git
synced 2026-04-20 03:03:25 -04:00
c26ca455cb
Another step towards VadCoP (#1495) With this PR, the `CompositeBackend` splits the given PIL into multiple machines and creates a proof for each machine. The rough algorithm is as follows: 1. The PIL is split into namespaces 2. Any lookups or permutations that reference multiple namespaces are removed. 3. Any other constraints that reference multiple namespaces lead to the two namespaces being merged. This is an example: ``` $ RUST_LOG=debug cargo run pil test_data/asm/block_to_block.asm -o output -f --prove-with halo2-composite --field bn254 ... Skipping connecting identity: main.instr_add { main.x, main.y, main.z } in 1 { main_arith.x, main_arith.y, main_arith.z }; == Proving machine: main PIL: namespace main(8); col fixed x(i) { i / 4 }; col fixed y(i) { i / 4 + 1 }; col witness z; col witness res; col fixed latch = [0, 0, 0, 1]*; main.res' = (1 - main.latch) * (main.res + main.z); (1 - main.instr_add) * (main.x + main.y - main.z) = 0; col fixed instr_add = [0, 1]*; Starting proof generation... Generating PK for snark... Generating proof... Time taken: 149.459458ms Proof generation done. == Proving machine: main_arith PIL: namespace main_arith(8); col witness x; col witness y; col witness z; main_arith.z = main_arith.x + main_arith.y; Starting proof generation... Generating PK for snark... Generating proof... Time taken: 150.752125ms Proof generation done. Writing output/block_to_block_proof.bin. ``` Seems seems to work across the entire codebase and allows us to create Halo2 proofs by machine! For STARK backends, we typically expect that IDs (e.g. Polynomial IDs, constraint IDs, ...) are re-assigned, which is not yet happening in this implementation. As mentioned in the comment, the easiest way to fix that would be to fix #1488 and re-parse the PIL file.