Multi-Claim Proofs

[aszepieniec]

I finished a first draft for documentation on the validity rules for transactions here. It highlights one important issue and anticipates a solution.

The issue is this: with the current Triton VM, we cannot generate a single-proof for a transaction without recursion, even if all parts not related to recursion are an order of magnitude less complex. In particular, we need to prove, for every lock script and type script, that those scripts halt gracefully.

The anticipated solution is this: generate a single-proof for multiple claims. If memory serves, Ferdinand had articulated the idea a while ago. The integrity of the AET implies the truth of not one but several claims.

[aszepieniec]

Brainstorming out loud here. To support this feature we need:

• an opcode to delimit the end of one program and the beginning of the next
• to extend halt with an optional immediate argument containing the instruction address of the next program, if any
• to compute not one but multiple program hashes
• to conditionally reset all state-bearing registers and populate the bottom of the stack with the next program hash
• to tailor all cross-table arguments to the $i$th program execution so as to disallow cross-program communication