Add a General-Purpose Cryptol Model of Basic Abstract State Machines (ASMs)

[kiniry]

Title

Add a General-Purpose Cryptol Model of Basic Abstract State Machines (ASMs)

Description

Summary

This issue tracks the design and implementation of a reusable Cryptol specification of Basic Abstract State Machines (ASMs) as defined in Section 2.2 of Börger and Stärk's Abstract State Machines. This model serves as a foundational building block for executable semantics, compilation, and formal verification of structured state-transition systems.

---

Motivation and Scope

This Cryptol model is intended to:

1. Serve as an executable reference model for Basic ASMs, capable of simulation and trace generation using the Cryptol interpreter.
2. Act as a specification source for verified compilation from Cryptol to high-assurance target languages, especially Rust and Verilog.
3. Provide a formal denotational baseline for verifying the behavioral correctness of manually implemented or automatically generated state machines in other languages, using SAW and its backends (LLVM IR, MIR, JVM, Yosys IR, etc.).

---

Technical Goals

• Represent ASM states as structured Cryptol records encapsulating functions or finite maps.
• Define and compose ASM rules:
  • Simple assignment
  • Conditional execution
  • Parallel update semantics
• Encode step and simulation semantics for iterative execution of ASMs.
• Provide human-readable trace output in an easily parsable format during simulation.
• Build an exemplar model based on Section 2.3 "Correct Lift Control" from Börger and Stärk’s book to validate the framework.

---

Conditions of Satisfaction

• The Cryptol code must typecheck, simulate correctly, and produce readable trace output.
• It must be possible to assert and prove well-formedness properties using :prove, such as:
  • Disjointness of parallel updates
  • Domain consistency across state transitions
• Include a rich test suite:
  • Unit tests for individual rule semantics
  • Property-based tests for step invariants and termination conditions
• Demonstrate:
  • Compilation of the ASM model to Rust and Verilog
  • Verification of behaviorally equivalent implementations in LLVM IR, MIR, JVM bytecode, or Yosys IR using SAW

---

Intended Usage

This ASM model will be leveraged in multiple domains of high-assurance engineering, including:

• As a formal specification and simulation engine for systems such as E2E-VIV, SEASHIP, HARDENS, and other secure or safety-critical components.
• As a verification reference for comparing high-level ASM designs against lower-level implementations using SAW-backed tooling.