CompositeBackend: Share randomness

[georgwiese]

Whenever separate machines access the same challenge (as they do to implement a bus, see #1497), we need the randomness to be the same across proofs.

One way to implement this would be to:

• Do phase-1 proof generation for each machine, get the challenges
• Sum them up across proofs
• Pass them to the phase-2 witness generation
• Finish the proof

Verifier

This is the current implementation of Backend::verify in CompositeBackend:

powdr/backend/src/composite/mod.rs

Lines 169 to 175 in e1169a7

	fn verify(&self, proof: &[u8], instances: &[Vec<F>]) -> Result<(), Error> {
	let proof: CompositeProof = bincode::deserialize(proof).unwrap();
	for (machine_data, machine_proof) in self.machine_data.values().zip_eq(proof.proofs) {
	machine_data.backend.verify(&machine_proof, instances)?;
	}
	Ok(())
	}

One problem with this is that this interface does not give us explicit access to the challenges, as computed by the backend, so the verifier can't easily re-compute the shared challenge.

One way to work around would be:

• Expose the per-machine challenges as public
  • I guess currently this would involve adding a stage-2 witness column, adding a constraint that it is always equal to the challenge, and expose the first cell as public.
• Also expose the shared challenge as public (which is used in the bus constraints)
• Then, the CompositeBackend verifier can check that:
  • All machines used the same shared randomness
  • The value used it equal to the sum of all per-machine challenges

[georgwiese]

Let me try to spec this out a bit more.

Current Backend interface

Currently, our Backend::prove function has the following signature:

powdr/backend/src/lib.rs

Lines 159 to 164 in e1169a7

	fn prove(
	&self,
	witness: &[(String, Vec<F>)],
	prev_proof: Option<Proof>,
	witgen_callback: WitgenCallback<F>,
	) -> Result<Proof, Error>;

It creates the first-phase proof and then calls witgen_callback.next_stage_witness, with the following signature:

powdr/executor/src/witgen/mod.rs

Lines 76 to 81 in e1169a7

	pub fn next_stage_witness(
	&self,
	current_witness: &[(String, Vec<T>)],
	challenges: BTreeMap<u64, T>,
	stage: u8,
	) -> Vec<(String, Vec<T>)> {

The reason we have this callback-based workflow (as opposed to explicitly exposing running the proof for different phases) is because of the Halo2 API (currently the only backend that supports challenges): It makes us implement a Circuit trait and just calls Circuit::synthesize several times. Inside this function, we might have the challenges available or not, and invoke the callback when they are, to get the additional phase-2 witness columns.

Current CompositeBackend implementation

To create a proof, the CompositeBackend just loops over all machines sequentially and invokes the underlying backend to create a proof for each machine independently:

powdr/backend/src/composite/mod.rs

Lines 150 to 165 in e1169a7

	let proof = CompositeProof {
	proofs: self
	.machine_data
	.iter()
	.map(|(machine, MachineData { pil, backend })| {
	let witgen_callback = witgen_callback.clone().with_pil(pil.clone());
	log::info!("== Proving machine: {} (size {})", machine, pil.degree());
	log::debug!("PIL:\n{}", pil);
	let witness = machine_witness_columns(witness, pil, machine);
	backend.prove(&witness, None, witgen_callback)
	})
	.collect::<Result<_, _>>()?,
	};

Of course, right now, any challenges will be different between machines.

Possible implementation of shared randomness

With this implementation, sharing randomness between machines seems tricky, but I think it might be possible. It could look like this:

• Before proving the first machine, we modify witgen_callback to first initiate proving of the next machine, again with a modified witgen_callback
• We somehow collect all challenges and compute the shared challenges by summing them up
• Only then do we actually invoke the "original" witgen_callback

I'm not sure if this is possible in Rust, perhaps with some asynchronous primitives (like async / await).

[lvella]

I just did the threads to suspend the execution of the prover in the middle. I won't work on the rest of the problem now, so I'll unassign myself.

[georgwiese]

I'll close this as the proving part is done. The verification part is left to do and tracked in #1608.