Modernizing K: Enhancing Functionality and Ease of Use

With K v6 we are modernizing the K Framework. We focused on emphasizing usability and customization in the design to make it easier than ever to generate a set of tools for your programming language environment! This includes easy installation, IDE support, a Python API, RPC interface, Language Bindings, a Haskell backend and an LLVM backend, symbolic debugger capabilities, and faster symbolic execution.

About K

K began as an academic project but has been adapted to commercial uses and has found particular success in the blockchain ecosystem by providing formal verification for projects on Ethereum, Algorand, Cardano, Embedded Systems, and more. Since the industry requires fast-paced development, K provides a way for developers to build faster, better, stronger, and safer tools.

With K, programming language tool builders can create debugging and analysis tools. Companies that need to market their tools can get there more quickly by using K, rather than embarking on their own journey. 

If you would like to learn more about K, check out our 0 to K tutorial.

Here are some of our other commercial engagements that you may be interested in:

• Serokell Collaboration: Runtime Verification Inc. has collaborated with the well-known Haskell consultancy Serokell to enhance the performance of the Haskell backend. You can read about it here.
• Formal Verification of Ethereum 2.0 Deposit Contract: Our team has conducted a formal verification of the Beacon Chain smart contract with K. You can read about it here. 
• Formal Model of the Beacon Chain: We have also developed a formal model of the Beacon Chain using K. You can read about it here.

What is new?

Modern K has undergone significant development and improvement, providing users with a more powerful, flexible, and efficient tool that is easier to use than ever before. To see these improvements in action or learn how to set up a Modern K definition, check out our newly released IMP semantics. This semantics uses the best Modern K practices, including: 

• Managing building the project with the kbuild system
• Managing invoking semantics with pyk
• Using the new RPC-based prover

Easy Installation

We have developed a one-line installation tool called kup, which is based on Nix. It provides a simple package manager for K-based projects, allowing a user to install and maintain everything with a simple command. We have made changes to the CLI options to improve the usability of the tools. The image below shows the CLI interface:

Performance

For the last couple of years, we have continuously worked on improving performance for:

Python API

We created a Python library (pyk) of useful commands to allow external tools to interface with the K tools. We chose Python because it is ubiquitous and very extensible. It’s great for scripting and experimenting. The pyk library introduces a new tool, kbuild, that lets kompilation targets be declared in a TOML configuration file. Based on the configuration, the tool manages dependencies to other K projects and takes care of calling the kompile tool with the right arguments on source file changes.

IDE Support

We have also added support for the K language in VSCode and other IDEs that support the Language Server Protocol through KIDE/klsp. The animation below demonstrates the following features: code completion, go-to definition and find references, syntax error highlighting, and selection range.

RPC Interface to the Prover

We identified a set of symbolic execution primitives and exposed them over RPC to allow users to write their own strategies on top of our symbolic execution engine. We recommend using pyk to interact with the prover this way since it already has all the required functionality built-in. The interface for interacting with the symbolic execution engine exists here. 

Language Bindings

We have added bindings from K to other languages to allow you to embed your language’s concrete execution features into an application more easily. Currently, we support binding to Python (via integration with pyk), and to any language with a C FFI. So far, we’ve used the C bindings successfully for applications written in C, Haskell, and Rust. These bindings can be used to integrate your K language semantics directly into other larger tools, such as web/RPC servers, or hook it up to external databases for storing data. This enables building powerful tools rapidly and directly from the K semantics. You can use the reference implementation of your language directly as a real implementation while you are prototyping with language features.

Haskell Backend: A new Symbolic Execution Backend

The new Haskell backend for K replaces the old Java implementation with over 150k lines of open-source Haskell code. It implements an all-path reachability algorithm for automated verification of programming languages and includes a language for writing formal specifications about users’ programs as K reachability claims. These claims get symbolically executed and proven by the backend. Users can provide proof hints inside the K specification, such as lemmas or loop invariants. The new Haskell backend also supports one-path reachability. 

K’s semantics was formalized into matching logic, and the new Haskell backend was designed based on matching mu-logic.

Technical Overview of Haskell Backend

Programs are represented as matching logic patterns and simplified according to the laws of matching logic. They are executed using the small-step semantics defined by the user, which accumulates path conditions on the symbolic variables. Infeasible path conditions are discovered by both the internal matching logic simplification engine and by translating and sending the condition to the SMT solver. The SMT solver we use is Z3. If you would like to know more about the theoretical background of the Haskell backend, you can review the docs on GitHub.

Design Decisions

The design decisions for the Haskell backend were made based on historical reasons, as the codebase was started in 2017. The effect stack is based on monad transformers and MTL, which is a simple, well-tested design. The matching logic pattern AST type representation is based on Cofree abstraction and integrates well with recursion schemes, allowing us to use synthetic attributes for information storage and optimization of certain procedures. For the traversal of the aforementioned AST types, we used recursion schemes to abstract away explicit recursive procedures, facilitate the removal of boilerplate, and increase code readability. 

We represented branching computations using the LogicT monad transformer, which introduced excellent semantics for implementing symbolic execution, unification procedures, and simplification of disjunction-based representation of terms. To avoid space leaks, we used Strict Haskell via the Strict language extension. This extension forces developers to explicitly mark lazy computations as such and to consider whether laziness is actually useful in that particular context.

LLVM Backend

The LLVM backend enables the K Framework to provide concrete execution capabilities. The backend’s implementation can be found here. Using the LLVM backend, a language semantics written in K can be compiled into an interpreter that can parse and execute programs written in that language. The interpreter generated by the backend is written in LLVM (hence the name) for performance and portability reasons. 

At a high level, the backend-generated interpreter exhaustively rewrites the input program according to the language semantics rules. To do this, the interpreter selects a rule that matches the current state of the program, applies the rewrite described in the selected rule, and repeats the process until no rules match. 

The backend consists of three main components: a pattern matching algorithm implemented in Scala, a code generator implemented in C++, and a runtime implemented in C/C++ and LLVM IR. The pattern matching component generates efficient decision trees that are used to select an applicable semantic rule matching a given program state. The backend uses a state-of-the-art pattern matching algorithm along with extensions to cover use cases unique to the K concrete execution problem. Click here for more on pattern matching.

The code generator component translates the decision tree and the rewrite suggested by each semantic rule into LLVM IR. The runtime component executes the high-level loop pattern matching the program state against semantic rules and rewriting it according to these rules. It also includes complementary subsystems such as a memory allocator and a garbage collector. Additional details and diagrams about the high-level structure of the LLVM backend can be found here. 

The LLVM backend offers some additional quality-of-life features, such as dedicated debug mode, as well as the ability to export various APIs (such as concrete term simplification) as libraries.

If you would like to learn more about K backends, check out the lessons in the K tutorial on backends.

What has this enabled?

KAVM is a tool that allows for formal verification of smart contracts on the Algorand blockchain by providing a mathematical foundation for the specification and implementation of smart contracts on Algorand and allowing developers to reason about the behavior of their contracts in a rigorous manner.

KEVM foundry property testing. It builds on the popular Foundry toolchain and adds support for property verification using the formal semantics of EVM written in K.

Connect with us!

Try out K or get in contact with the dev team by joining the chat at Riot, Discord, or Telegram.

If you are interested in viewing the changelog, it can be found on GitHub.