K-Michelson: A Michelson Semantics

Introduction

K-Michelson is:

• a formal, executable, and human-readable semantics of the Michelson blockchain programming language using the K framework;

• a unit test framework for Michelson programs that allows testing program behavior at a finer granularity than contract invocation;

• a formal verification framework for Michelson programs using a slight extension of Michelson as an assertion language.

Goals

• Serve as a human-readable and executable reference document specifying how Michelson programs should operate.

• Provide tools for testing and verifying Michelson programs operate as designed.

Non-Goals

• Provide a complete formal model of the Tezos blockchain. In particular, we do not model things like: networking and peer-to-peer communication, block baking or validation, transaction pools, protocol amendment, etc.

• Replace existing Tezos CLI tools. Developers should still use tezos-client for interfacing with Tezos nodes, tezos-node for running your own nodes, etc.

Getting Started

See INSTALL.md for installation instructions.

See USER_GUIDE.md for usage instructions.

Project Structure

The project has a very simple layout. Source files live at the project root.

• syntax.md specifies the syntax of Michelson and other input data

• common.md specifies common infrastructure used in the type checker and the core semantics

• types.md contains a rudimentary type-checker for Michelson

• michelson.md specifies:

  • the configuration (state representation) of Michelson programs (module MICHELSON-CONFIG)
  • the core semantic rules of Michelson as well as semantic extensions to support unit testing (module MICHELSON)

• compat.md is a compatability layer between K-Michelson and the Tezos Reference client used for cross-validation testing

Other directories include:

• /ext - Git submodules for our direct dependencies
• /hooks - C++ definitions which implement some low-level operations
• /lib - scripts used by the test harness
• /media - source code for presentations about K-Michelson
• /tests - source code for all tests

See the tests README for more information on test formats and organization.