Proof generation from ABI methods prototype

runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License

15 stars 4 forks source link

Proof generation from ABI methods prototype #227

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

This PR demonstrates using pyk features to automatically generate a simple claim about a PyTeal-generated contract (defined in proofs/create_pyteal_contract.py).

I have also added a number of new lemmas for dealing with lengthBytes symbolically, so please review that those are correct.