runtimeverification / avm-semantics

BSD 3-Clause "New" or "Revised" License
15 stars 4 forks source link

Claim generation test #223

Closed nwatson22 closed 1 year ago

nwatson22 commented 1 year ago

In this PR, I aimed to experiment with automatic claim generation. All the relevant files are in example. example/kavm-mini.md is an example kavm-like VM which can run basic TEAL-like programs. example/generate_proofs.py houses the code for generating the claims automatically and setting up an example claim, which is similar to the manually written claim in example/kavm-mini-spec.md.