Generate K claims from scratch

[geo2a]

This PR provides a way for generating K claims about PyTeal contracts without writing K directly. Perhaps some K will need to be written using pyk combinators, but that should be possible to avoid too, eventually.

The workflow looks like this:

1. initialize all actors (contract creator, etc.) and the contract for simulation. This step is done completely with py-algroand-sdk
2. execute the transactions to "deploy" the contract, i.e. bring the system to a desired "live" state for verification. This only involves concrete execution and can be done with both KAVM and algod, using the same code
3. Create symbolic variables for all entities that need to be symbolic: balances, state variables etc. Specify any relevant preconditions.
4. Edit the objects obtained at step 2 by intriducing the variables created at step 3.
5. Initialize a KAVMProof object with the edited py-algorand-sdk objects that now contain symbolic variables
6. The initialized KAVMProof object will generate a mapping from the initial state variables (defined in step 3) to the existential variables in the eventual final state. Use this mapping to formulate the postconditions: what would you like the final state of the variables to look like?
7. Run proof.

See ./kavm/src/tests/algod_integration/contracts/kcoin_vault/test_specs.py for a complete and relatively well-documented example.

[geo2a]

@nwatson22 I've merged master, please approve the PR so we can merge it. Thanks!