Formalizing TEAL

TEAL is a stack-based programming language for the Algorand blockchain. It has 256 registers (called scratch space). Here's an example of a TEAL program with looping:

#pragma version 4
// loop 1 - 10
// init loop var
int 0 
loop:
int 1
+
dup
// implement loop code
// ...
// check upper bound
int 10
<=
bnz loop
// once the loop exits, the last counter value will be left on stack

TEAL plays two major roles which are slightly different:

• Smart signatures: some money is locked up by a "locking script" implemented in TEAL posted on a public bulletin board (the Algorand blockchain). If you can post on the bulletin board a "unlocking script" such that when you run the unlocking script followed by the locking script the stack ends up with a true element at the top, then you can claim the money. In this role TEAL is basically just a very smart predicate.
• Smart contracts: Stateful "autonomous" TEAL programs that have their own "bank accounts" and can do things like send money.

Big or small step semantics?

I chose to model steps as the execution of an entire operation (e.g. Add). It would be possible to get more granular, e.g. when the Add opcode is encountered the State goes to an "Adding" state and there are individual steps for popping the first element off the stack, the second, computing the addition, and then pushing the result. This would have some advantages, for example you could talk about malformed programs and exactly how they fail more easily, but would be significantly more cumbersome.

I didn't get to modeling TEAL transaction approval. It is interesting to note that this will require adding some "Transaction State" to the program state. See the following example:

// Begin inner transaction
itxn_begin

// Set transaction type to payment
int pay
itxn_field TypeEnum

// Set recipient address
txn ApplicationArgs 0  // Get recipient from app call args
itxn_field Receiver

// Set amount to send
int 1000000  // 1 ALGO (in microAlgos)
itxn_field Amount

// Set fee (0 means use minimum)
int 0
itxn_field Fee

// Submit the inner transaction
itxn_submit

Opcodes

TEAL has hundreds of opcodes and I didn't model them all. Here's what I got to:

• Basic arithmetic (PushInt, Add, Not, Eq, Dup)
• Branching (BranchNZ)
• Loads and Stores (for working with scratch space)

Stack elements

TEAL has two basic kinds of stack elements:

• Unsigned 64-bit integers
• Arbitrary-length strings of bytes

I augmented this with an "artifical" type of SHA256 hashes of some preimage. This is to avoid having to implement and prove things about the actual sha256 function, which would be insanely complex and slow. This is still somewhat useful because you can still e.g. know that two SHA256 hashes of the same preimages will be equal, but you can't really prove things about SHA256 hashes of different preimages (in general) because you don't know if there will be a collision or not (though you can axiomatize things if you want to use the fact that e.g. sha256([1]) != sha256([2])). And obviously this does not allow you to manipulate hashes, which is technically possible in TEAL (though I suspect almost never done). Another strategy to deal with hashing could have been to require any proof about a TEAL program to go through for an arbitrary choice of hash function. For certain proofs you could introduce an axiom which says that hash collision don't happen.

Cost

Operations in TEAL are associated with a cost, which curiously depends only on the opcode, even when the inputs are sometimes of arbitrarily length (e.g. b* which does multiplication for bigints costs 20). Most opcodes cost 1, with the exceptions being stuff like bigints and hashing.

There are limitations on the total cost allowed when executing a TEAL program (it depends on whether the program is for a signature or contract). If a TEAL program uses more cost than allowed, the VM halts execution and rolls back any changes it made to the state. However, since TEAL has loops, it can be unclear exactly how many opcodes a TEAL program might execute in the worst case. This motivates modeling the cost of opcodes -- it is necessary if you want to be certain of liveness of a sufficiently complex smart contract.

Proofs of Concept

The primary proof in this project was showing that TEAL (the limited version of this project) is deterministic, meaning that the current state (which in my model includes the program) uniquely defines the next state. This proof was pretty cumbersome, and while writing it I actually found some bugs in my spec. Likely the proof can be made much nicer by writing some custom tactics -- the main difficulty was having to unpack Prop structures in order to guide grind.

I also wrote a proof of correctness and cost for a simple program which runs add twice. My original goal was to prove the correctness and cost for a subset sum witness checking program, but I ran out of time. I don't actually think this should be too hard once some custom tactics are written. The main difficulty is writing down all of the intermediate states for trans, but it shouldn't be hard to write a tactic which automaticaly fills in most of the details for these intermediate states.

I also wrote a proof of correctness and cost for a simple progrma which compares two SHA256 hashes of the same preimage, to illustrate the point that this type of TEAL program can be checked in my model even without an implementation of SHA256.

I ended up significantly refactoring the project and I didn't have time to redo some of my old proofs. In an older version of the project I had a nice theorem which said that if s =>* s' then there is k and a map Fin (k+2) -> State of intermediate states. I think this would be quite nice to use alongside with some custom tactics for proving things about TEAL programs. You can see old.teal for some very messy code showing the idea.

Prior Work

Some prior work on verifying smart contracts:

• Clear: A framework for proving things about Solidity smart contracts. Solidity is a high-level language which compiles down to Yul (a slightly lower level language) which compiles down to EVM bytecode (most analogous to TEAL). Clear has custom Lean tactics.
• Some work has been done to verify smart contracts with a tool called KFramework https://github.com/runtimeverification/verified-smart-contracts?tab=readme-ov-file
• Certora prover: for Solidity. Has a nice custom language for writing specs https://docs.certora.com/en/latest/
• There is some work on verifying TEAL with KFramework by a company called Runtime Verification. https://runtimeverification.com/blog/runtime-verification-and-algorand-announce-a-new-engagement-to-build-formal-tools-for-algorands-smart-contract-ecosystem

Future work

Here are some things I would love to get to:

• Transactions. This would allow you to prove things like "this contract only transfers money to people if the following conditions are met" i.e. thou cannot steal.
• Global, local, and box storage. This would allow you to prove that two TEAL programs can run concurrently without locks.
• Function calls
• Implementing tactics for making it easy to prove things about concrete TEAL programs. It should be trivial to prove something like that the (PushInt a; PushInt b; PushInt c; Add; Add) program computes (a+b+c). Dealing with ReflTransGen makes this hard, but I'm sure there's a way to do it.
• Proving some things about moderately complex TEAL programs. For example, something like a TEAL program which checks that the input is a witness for some subset sum problem.
• Basic security proofs? E.g. implement a subset sum witness checker program and prove that any unlocking script that works implies that the unlocking script ended up with a valid subset sum answer on its stack (as compared against a Lean spec).
• Reductions: prove that either some TEAL program is secure or you can use the unlocking script to compute a hash collision.