Home

Awesome

KAVM — Algorand Virtual Machine and TEAL Semantics in K

🛠️Work in progress🛠️

KAVM leverages the K Framework to empower Algorand smart contracts' developers with property-based testing and formal verification.

Getting Started

Installing KAVM

For now, KAVM can only be installed from source. We intend to provide a Docker image and standalone packages for popular operating systems at a later stage. To install KAVM from source, please refer to Working on KAVM.

Entry points

The semantics can be used either via the kavm command-line interface or programmaticaly with the kavm Python package.

kavm runner script

The kavm Python tool provides a command-line interface for the semantics:

See kavm --help for more information.

Note: make sure to activate the Python virtual environment build by KAVM with . .build/venv/bin/activate for the kavm script to be available.

kavm Python library

kavm provides Python bindings to KAVM

Testing harness

Concrete Execution Tests

The tests are located in tests/.

Run make test-avm-semantics -j8 to execute the test suite. Adjust the -jX option as needed to run X tests in parallel.

Each test has two components:

Currently, a test is considered passing if the kavm runner script returns 0. The final state network state is not examined.

The negative test scenarios are expected to fail and have the .fail.avm-simulation file extension.

Symbolic Proofs

NOTE: the specs have not yet been fully ported to the current semantics and are failing. They are not checked on CI and are not called by make test.

The specifications are located in tests/specs/.

Run make test-avm-prove to verify the specifications.

The verification.md module must be compiled with the Haskell backend and included in every spec file. The Makefile target test-avm-prove ensures that the verification module is compiled properly before checking the specs.

Repository Structure

K files

Algorand network state and AVM files

The AVM semantics source files are located in lib/include/kframework/avm/:

TEAL Interpreter

Transaction Execution Approval Language (TEAL) is the language that governs approval of Algorand transactions and serves as the execution layer for Algorand Smart Contracts.

The K modules describing syntax and semantics of TEAL are located in lib/include/kframework/avm/teal/:

Not all TEAL opcodes are supported by the semantics as of yet. See the relevant wiki page for the table of supported opcodes and their execution costs. The semantics does not yet support contract-to-contract calls.

Python packages

kavm[./kavm] is a Python package that enables interoperability between KAVM and algod — the Algorand node daemon. kavm also provides a drop-in replacement for py-algorand-sdk, making it possible to run existing deployment and testing scripts on top of KAVM.

kavm uses two auxiliary scripts located in lib/include/kframework/avm/scripts/:

Working on KAVM

Build system

When developing, make sure to activate the Python virtual environment build by KAVM with . .build/venv/bin/activate for the kavm script to be available. The Makefile activates the environment itself when necessary.

Managing PATH with direnv

We use direnv to manage the environment variables such as PATH, see .envrc.

After installing direnv, run direnv allow to activate the settings for the project's directory.

Feel free to ignore direnv if you prefer your global installation of K.

Rule Coverage

This project contains facilities to generate coverage metrics for K rewrite rules that were executed by kavm run. This is helpful in ensuring that the test suite contains input programs that exercise all rewrite rules in the semantics.

To generate the coverage report for the AVM simulation scenarious squite (tests/scenarios/), run the following command:

  make clean-coverage && make test-kavm-avm-simulation && make coverage

This command generates a .build/coverage.xml file. This file contains information about the K rewrite rules that have been exercised for all tests in the (tests/scenarios/) directory.