One complicated part is the actual proof verification. I had considered
looking into what it would take to build a verifying for a modern proof
system if we used pairings as a primitive, but it turns out even that is
pretty involved even in a higher level language (at least for PLONK [3])
and would be error-prone when trying to adapt the code for new circuits
with differently-shaped public inputs. The size of the code on-chain
alone would probably make it prohibitively expensive, so it would be a
lot more efficient just to assume we can introduce a specific opcode for
doing a proof verification implemented natively. The way I assumed it
would work is taking the serialized proof, a verification key, and the
public input as separate stack items. The public input is the
concatenation of the state and deposit commitments we took from the
input, the batch post-state commitment (provided as part of the
witness), data from transaction outputs corresponding to
internally-initiated withdrawals from the rollup, and the rollup batch
data itself (also passed as part of the witness).
I'd be interested in knowing what sort of Simplicity Jets would facilitate rollups. I suppose some pairing-friendly curve operations would do. It might not make the first cut of Simplicity, but we will see.
Simplicity's design doesn't have anything like a 520 byte stack limit. There is just going to be an overall maximum allowed Simplicity evaluation state size of some value that I have yet to decide. I would imagine it to be something like 1MB.