CompositeBackend: Create proofs for each machine (working with Halo2)

[georgwiese]

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.

[georgwiese]

Removed for now, until the re-parsing is happening.

[leonardoalt]

Awesome! Some small comments that don't necessarily need to be fixed. Can this PR be merged already or do we need to wait?

[leonardoalt]

Is this always correct? I don't have a counterexample, but wondering if there are cases that would break this

[georgwiese]

I think so! The code is inspired by our implementation of Display:

powdr/ast/src/analyzed/display.rs

Lines 29 to 37 in 91d41df

	let name = namespace.pop().unwrap();
	if namespace != current_namespace {
	current_namespace = namespace;
	writeln!(
	f,
	"namespace {}({degree});",
	current_namespace.relative_to(&Default::default())
	)?;
	};

[leonardoalt]

Is this PR going to wait for that, or should it be merged before?

[georgwiese]

Should be merged before!

[georgwiese]

Yeah, I think it can be merged!