I was basing it on these benchmarks for Miden vs Plonk
I mean, if you have some kind of “instruction” which is dynamically decoded by the circuit, where the inputs and outputs are copied into or out of a “register”, this seems like it would always have overhead over placing two Halo2 chips with relative references. This effect would be magnified a lot if the register has to be copied between circuits, for example if a circuit only executes a single instruction. Maybe this is not really a significant factor, but it would always exist.
If the VM works in this recursive-verifying cycle, where it executes one or more instructions on one side of the cycle and incrementally/recursively verifies/accumulates on the other side of the cycle, then “instruction decoding” (or generally deciding what to execute next) has to happen somewhere - but if the execution circuit is “specialized” - by which I mean that it is not generic, that the circuit is hardcoded to do a particular operation - then when the recursive verifier checks that the execution circuit is the correct one, that means there doesn’t have to be any instruction decoding in the execution circuit. Instead, the VM compiles (out of circuit) one or more instructions into the specialized/hardcoded execution circuit, and provides the correct verifying key for that circuit.
In order to get true IVC/recursive verification, since we have proofs on both sides of the cycle, we have to accumulate both sides of the cycle as well. Otherwise, if we only accumulate on one side, then we still need to verify the entire history of proofs from the other side of the cycle. Imagine that we only accumulate execution circuit proofs with the verifier circuit, then at each stage we only have one execution circuit accumulator, but in order to trust that the execution circuit accumulator was created properly, we need to check the verifier circuit proof since the beginning of execution, which doesn’t bring us the asymptotic efficiency we wanted. So the execution circuit also has to accumulate the verifier proofs so that we only have to check the two accumulators to be assured of the entire history.