rigorously test Triton VM's initial constraints

[jan-ferdinand]

Initial constraints inherently only apply to the first row of the execution trace. For the Processor Table, some initial constraints are “deactivated” depending on the instruction in that first row since they would not make sense. For both completeness and soundness of Triton VM, it is crucial that all initial constraints check precisely the properties that need checking.

• [ ] For each instruction where it is legal[^1] to do so:
  • [ ] write a short Triton assembly (TASM) program that starts with that instruction
  • [ ] write a test that evaluates all initial constraints on an execution trace generated from the TASM program
  • [ ] prove & verify correct execution of the TASM program
• [ ] For all other instructions, i.e., instructions a program cannot start with:
  • [ ] write a short TASM program that starts with that instruction
  • [ ] write a test that expects a failure
  • [ ] ensure that the error message communicates the reason of failure clearly to the programmer

The instructions that a TASM program cannot start with are:

• pop, because the resulting stack would be too shallow
• return, because there is no-where to return to
• recurse, because no call has been executed yet and hence there is nothing to recurse on
• assert, because the initially all-zero stack implies that the top element is not 1 and because the resulting stack would be too shallow
• add, because the resulting stack would be too shallow
• absorb, because the Sponge needs to be initialized using absorb_init before further absorptions
• squeeze, because the Sponge needs to be initialized using absorb_init before any squeezing
• mul, because the resulting stack would be too shallow
• invert, because the top of the stack is initially zero and thus doesn't have an inverse
• eq, because the resulting stack would be too shallow
• lt, because the resulting stack would be too shallow
• and, because the resulting stack would be too shallow
• xor, because the resulting stack would be too shallow
• log_2_floor, because the top of the stack is initially zero and thus the logarithm is undefined
• pow, because the resulting stack would be too shallow
• div, because the initially all-zero stack implies division by zero
• xinvert, because the top of the stack is initially zero and thus doesn't have an inverse
• xbmul, because the resulting stack would be too shallow
• write_io, because the resulting stack would be too shallow

[^1]: I specifically say legal, not sensical, because some instructions probably don't make sense as the first instruction. For example, swap 1 is a worse nop since the stack is initialized to all zeros. However, Triton VM should not fail in such cases.