New STProver architecture

[rpanic]

We want to build a STProver that has few properties:

1. Be Tree-agnostic, as long as the tree implementation has a checkMembership() and computeRoot() functionality
2. Be able to process multiple batches of connected ST batches
   This means that we want to encode the applying of a set of ST-batches, while being able to mark any batch on whether it should progress the state root or not. The output of this Prover will be a to stateRoot
3. Batches and their contents have to be assertable easily.
4. (not sure if that is needed - might be for merging) There should be a single assertable hash with a list of all applied STs, that can be asserted either in the blockProof/settlement/etc

Since we can make the assumptions that we have some fixed order in which we process ST-batches, we can safely encode the batches themself in a hashlist.

The new ST Prover can be imagined as two paths running independently and only at the end merging together and proving their equality.

The first path is the emitting part, where there is a set of circuits that run in a fixed order, which emit state transitions incrementally. In our case this would be Runtimes via the State abstraction and the Protocol + Block Producing circuits via their hooks.
Each part of the execution emits a independent set of STs (called a Batch) $B_n = { ST_1, ST_2, ..., ST_m }$ and a boolean indicator on whether those STs should be applied or thrown away.
Setting the indicator to $true$ means that all ST preconditions will be checked and all ST updates will be applied. The indicator being $false$ means only the preconditions will be checked and updates applied, but the end result being thrown away in favor of the state before that particular batch.

The set of all Batches will continously aggregated into a hash list based commitment as { stsHash, applied } where stsHash is itself a hash list commitment of all STs in that batch.

The second path is the state modification part of the circuits, in our case the STProver. It will take a set of Batches and a beginning state $S_0$ and apply the batches one by one to arrive at a end state $S_n$ along with a commitment to all executed batches $c(B_0, ..., B_n)$.

The algorithm by which it does this is fairly straight forward.
Define the state of the algorithm as a struct of: { currentBatch: { stsHash: Field, stagedRoot: Field }, batchListHash: Field, finalizedRoot: Field }

First, the set of batches { sts: ST[], applied: Bool }[] will be flattened trivially into { st: ST, type: "continue" | "closeAndApply" | "closeAndThrowAway" }[]

Then, for each of those entries:

1. Apply the current ST onto the staged root and append the ST to the stsHash
2. If type == "closeAndApply":
   1. Add the currentBatch to the batchListHash
   2. set finalizedRoot to stagedRoot
   3. Reset currentBatch
3. If type == "closeAndThrowAway":
   1. Add the currentBatch to the batchListHash
   2. Reset current batch

Notice that for closeAndThrowAway, we don't update the finalizedRoot, but instead throw away the result. This ensures that all preconditions of the STs are still checked, but no updated are applied.

Merging the two pipeline paths:
We have two paths in our proving pipeline: One that emits the STs, and one that takes STs and applies them to the tree.
Those are now very much independent, but we have to make sure that both path worked with the same STs.

It makes sense to choose a very long interval in which the two paths run independently, because it improves the proving efficiency. When choosing to merge, two things have to be enforced:

1. Assert that the batchListHash of both paths match
2. The new output is set to the ST-path's finalizedRoot output

When this happens at any point in the proof chain, we assert the validity, completeness and correctness of the STs and the equality of both paths.

Example:

In our example, we start at stateroot $S_1$, protocol hooks that progress from $S_1 \to S_2$ , and a failed runtime method $S_2 \to S_3$. Finally, we have some imaginary afterTx hooks that progress from $S_2 \to S_4$.

A the emitted batch list looks like this:

$$\begin{aligned} \{ batch: ST_a, applied: true \}\\\ \{ batch: ST_b, applied: false \}\\\ \{ batch: ST_c, applied: true \} \end{aligned}$$

The corresponding steps in the ST Prover would look like

$$\begin{aligned} \{ finalizedStateRoot: S_1, stagedRoot: S_2, batch: ST_a \}\\\ \{ finalizedStateRoot: S_2, stagedRoot: S_3, batch: ST_b \}\\\ \{ finalizedStateRoot: S_2, stagedRoot: S_4, batch: ST_c \}\\\ \rightarrow output: S_4 (S_1 \rightarrow S_2 \rightarrow S_4) \end{aligned}$$

As we can see, the third batch, is based off $S_2$, so all STs that were emitted in the runtime, have been proven to be correct, but the stateroot has been thrown away.

[rpanic]

Intermediary state roots

In our application, we want to occasionally work with the actual state root after some step.
For example, after each block, we want to use the state root of the last block in a provable way in order to enable things like state proofs, which have to be asserted against a up-to-date state root.
A simple solution would be to roll up the STProof at the same interval as we want to use the state roots, but this limits the versatility of the architecture in an unwanted way. In out example, that would mean that we have to do that every block, which might not be the most economical thing to do.
So, we can use the following protocol to independently witness state roots and check their correctness at the end, when we rollup the ST Proof. We subsequently refer to this witnessed state root as "intermediary state root".

Protocol

The intuition on how we accomplish this is by adding the fact that we've witnesses a certain value to a accumulator. The STProver does the same thing and we can again, during the merging process, assert the accumuluators' equality.

Define set $A$ as the list of all state roots witnessed by the application and set $S$ as the set of all accumulated state roots by the prover.
The simple protocol to assert that $A = S$ is the following:

The prover (BlockProver) accumulates all of $A$ into a hashlist by setting the accumulator $acc$ to some public value.
acc += { appliedBatchListState, root }
where the appliedBatchListState is the current hash of the batch list and root is the value of the witnessed root.

The verifier (STProver) does the same using its internal intermediary state. As an implementation caveat, the STProver has a flag witnessRoot for any ST t it proves which indicates whether the state root after applying t should be added to the witness accumulator or not.
Furthermore, the following invariant has to hold: t.witnessRoot implies t.type.isClosing

Both parties leak the resulting witnessedRootsHash as a public output. So then, the final proof, that consumes all previous block proofs (merged together) along with the ST proof, can assert that the witnessedRootsHash matches in both proofs, therefore making sure that all of the initial witnessed roots are indeed correct intermediary state roots and also that the time of their occurance is consistent.

Deduplication

The above protocol has a problem however.
We know that if a batch of STs is empty, the hashlist ignores that batch and doesn't append it to it's commitment.
Now, if there are multiple points in the BlockProver where a certain state root r is witnessed, and those points have been witnessed on the same batch list's tip tip, the tuple { appliedBatchListState: tip, root: r } will be added to the witnessed root list twice.

However, as we specified above, the STProver appends to the witnessed root list at maximum once for every ST. This means that the STProver has no way of reconstructing the correct witnessedRootsHash with the above tuple being included twice.

To mitigate this, when the BlockProver appends to the witnessed root list, it deduplicates potential duplicates.

The algorithm to do that is fairly simple. In essence, the BlockProver can provide a preimage to the append function of the hashlist, where we can provable detect duplicates and then skip the append operation and treat it as a no-op.

The only thing we have to do given the preimage and the current data to be appended is check if
hash(preimage, witnessedRootData) === currentHashListCommitment. If this evaluates to true, we skip the appending, as this statement proves that the current tip ends with the exact same data we want to append.

Edge case

There exists a edge-case when the batch list is empty and we want to witness a root. If we would append our witnessing to the accumulator, the STProver could not verify that, since there is no ST that we could piggy-back on.
So in addition to the deduplication described above, we skip the append if witnessedRoot == finalizedRoot. The finalized root is updated every time we merge a STProof into the BlockProver. So therefore, when that root is the same as the one we witnesses, we can safely assume it to be correct iff the appliedBatchList is empty.

In practice, we transform this statement and implement it as
pendingBatch.isEmpty implies (finalizedRoot == witnessedRoot) at every point where we witness a state root.