Kleene Algebra Modulo Theories

TL;DR

This paper introduces Kleene algebra modulo theories (KMT), a framework that automatically derives sound and complete semantics for domain-specific Kleene algebras with tests, facilitating easier extension and implementation.

Contribution

It provides a formal, automatable method to create and reason about domain-specific KATs using pushback, enabling efficient equivalence checking and new theoretical results.

Findings

Automated derivation of semantics for KATs from primitives and state notions

Proved soundness and completeness of the derived KATs with respect to tracing semantics

Implemented a practical OCaml framework for defining and composing KATs

Abstract

Kleene algebras with tests (KATs) offer sound, complete, and decidable equational reasoning about regularly structured programs. Interest in KATs has increased greatly since NetKAT demonstrated how well extensions of KATs with domain-specific primitives and extra axioms apply to computer networks. Unfortunately, extending a KAT to a new domain by adding custom primitives, proving its equational theory sound and complete, and coming up with an efficient implementation is still an expert's task. Abstruse metatheory is holding back KAT's potential. We offer a fast path to a "minimum viable model" of a KAT, formally or in code through our framework, Kleene algebra modulo theories (KMT). Given primitives and a notion of state, we can automatically derive a corresponding KAT's semantics, prove its equational theory sound and complete with respect to a tracing semantics (programs are denoted as traces of states), and derive a normalization-based decision procedure for equivalence checking. Our framework is based on pushback, a generalization of weakest preconditions that specifies how predicates and actions interact. We offer several case studies, showing tracing variants of theories from the literature (bitvectors, NetKAT) along with novel compositional theories (products, temporal logic, and sets). We derive new results over unbounded state, reasoning about monotonically increasing, unbounded natural numbers. Our OCaml implementation closely matches the theory: users define and compose KATs with the module system.