We've discussed a possible annotated opcode output with @pirapira and the idea is to have a simple text format:

• each opcode is on a single line and no whitespaces are allowed around opcodes
• empty lines are allowed
• comments are denoted by a line starting with ;;
• the format starts with ;; annotated_evm_output
• assertions for verification are stored as ;; assert:
• multiple assertion lines between opcodes are joined with logical conjunction

Format within assertions:

• conjunction is represented as /\
• disjunction is represented as \/
• parentheses are allowed to group statements
• (syntax of statements to be described by @pirapira after an experiment Assertions between opcodes pirapira/evmverif#5)

;; annotated_evm_output
PUSH1 0x60
PUSH1 0x40
PUSH1 0x60
PUSH1 0x40

;; we know the stack height here
;; assert: length stack > 3

;; we know the top element must be one of these
;; assert: (stack 0 = caller) \/ (stack 0 = balance)
MUL