Emulate shared challenges in `CompositeBackend`

[georgwiese]

With #1603 demonstrating how shared challenges can be computed when computing proofs in the CompositeBackend, we still have to do the same in the verification algorithm. However, the Backend::verify function does not currently give us access to the challenges (unlike prove, where we could manipulate the witgen_callback to access them).

Here, I want to sketch how we can anyway emulate shared challenges using any backend.

Background

Let's say two machines request a shared challenge alpha of a particular ID, like so:

let alpha = challenge(0 /* stage */, 1 /* id */);

Then, this challenge should depend on all phase stage-0 witness columns of both machines. But in the composite proof, the proving backend is invoked independently for each machine, so it is not aware of the other machine's columns.

A way to emulate challenges anyway is this:

• In each machine, sample local challenges alpha_local1 and alpha_local2, depending only on the local stage-0 witness columns.
• To get the shared challenge, sum up all local challenges.

#1603 does this in the proving stage: It intercepts the otherwise independent machine proofs and modifies the challenges to be equal to the sum of local challenges.

A verifier with shared challenges

CompositeBackend::verify just calls Backend::verify for each machine proof, so it would not have direct access to the local challenges.

However, we do the following:

1. Expose the local challenge as a public output
2. Instead of the local challenge, use a prover-provided (and unconstrained) claimed shared challenge in the constraints
3. Expose the claimed shared challenge as public
4. In CompositeBackend::verify, verify all machine proofs and also check that the shared challenges have been computed correctly

Implementation

Our abstractions are currently not ideal to implement this. In particular, only cells in the trace can be exposed as publics. So, let me spell out the above list a bit more, using the abstractions we have available today:

1. Expose the local challenge as a public output
   1. Add a witness column alpha_local_col
   2. Add a constraint alpha_local_col = alpha_local
   3. Expose alpha_local_col[0] as public
2. Instead of the local challenge, use a prover-provided (and unconstrained) claimed shared challenge in the constraints
   1. Add a witness column alpha
   2. Add a constraint alpha = alpha'
   3. Because alpha is a column that is equal to the same value everywhere, this can be used like a scalar. All constraints that need to use the shared challenge should reference it.
3. Expose the claimed shared challenge as public
   1. Expose alpha[0] as public
4. In CompositeBackend::verify, verify all machine proofs and also check that the shared challenges have been computed correctly
   1. Checking the machine proof automatically verifies that alpha_local_col has the correct value (because there is a constraint for it), and that alpha was equal to whatever value is in the publics.
   2. The verifier runs additional checks on the publics to verify that the shared challenges have been computed correctly.

Note: This needs a slight modification in #1603, which currently overwrites the challenges, so witgen wouldn't have access to the local challenge anymore.

Discussion

This suggested implementation adds significant overhead. For example, for Plonky3, we're currently adding 3 witness columns for each public (this could be changed to just one fixed column though, see #1607). So, this transformation would currently add 8 witness columns per challenge (2 witness and 2 fixed after #1607). For a bus, for example, we would need 2 extension field challenges, so we'd have 4 challenges. A more integrated solution could achieve shared challenges without any extra cost.

I still think it's worth doing though, because the cost still seems manageable and we'd have a backend-agnostic implementation.

[georgwiese]

Note that if publics were just scalars that can be used in constraints (as they natively are in Plonky3) instead of cells in the trace (as they natively are in Halo2, and is also what we currently implement), this would be a lot cheaper. We would just:

1. Add a public alpha_local_public
2. Add a constraint alpha_local_public = alpha_local
3. Add a public alpha and use it in the constraints that expect a shared challenge

No need to add any columns.

[Schaeff]

Another reason to move away from publics as cells to publics as scalars.

[georgwiese]

A good test for this is the block_to_block_with_bus_composite test introduced in #1628. It is marked as should_panic until this issue is resolved.