[KAVM] Lightweight Python test driver

[geo2a]

We need a concise way to describe complex test vectors for KAVM.

In the other project, PyTeal_eval, @vasil-sd is in the process of solving very similar challenge, and we would like to join forces and share the same surface test description API.

Short-term goal

Emit strings that would contain K terms that will be passed as values to the $PGM configuration variable to kavm.

Network state

For example, the following PyTeal_eval-like pseudocode:

acc = Account(address="1")                       # new account
app = Application(app_id=1, creator_address="1") # new app
asa = Asset(asset_id="42", creator_address="1") # new asset

would produce the following K term (excluding comments):

addAccount <address> b\"1\" </address>";
addApp     <appID> 1 </appID> <address> b\"1\" </address> 0";      // the address is the creator's address
addAsset   <assetID> 42 </assetID> <address> b\"1\" </address> 0"; // the address is the creator's address

The relevant K rules are now located in the (avm-initialization.md)[https://github.com/runtimeverification/algorand-sc-semantics/blob/kteal-prime/modules/avm/avm-initialization.md] file of algorand-sc-semantics/kteal-prime, pending migration to this repo.

Note that here we are being unnecessarily verbose on the PyTeal_eval part: many of the constructor arguments may be omitted and provided with generated values. The K terms, however, will need to be precise and include all the information that was generated by PyTeal_eval.

Transaction group

Similarly to the network state, the tool will emit K terms for specifying transactions:

txn[0] = Transaction(type="appl", sender="1", app_id=1, on_completion=0, accounts=[1])

addAppCallTx <txID>            0        </txID>
             <sender>          b\"1\"   </sender>
             <applicationID>   1        </applicationID>
             <onCompletion>    0        </onCompletion>
             <accounts>        b\"1\"   </accounts>;

The KAVM semantics will handle bundling of the transactions into a group internally.

Same remark regarding the verbosity in PyTeal_eval constructors applies: many of the constructor arguments may be omitted and provided with generated values. The K terms, however, will need to be precise and include all the information that was generated by PyTeal_eval.

Long-term goal

The PyTeal_eval will eventually support integrate py-algorand-sdk to work with real blockchain data, while retaining the same lightweight format for test scenarios. If made compatible, KAVM will benefit from this too, with the ad-hoc passing of K terms upgraded to a more robust communication protocol.

[geo2a]

Note that the long-term goal aligns with the "Algorand Network Interactor" idea that we had on TODO for a while in the TEAL Tools board

[geo2a]

I'm closing this as outdated. We not have a prototype integration with py-algorand-sdk that solves implements this.