cubical-sm is a Cubical Agda library for state-machine presentations, execution laws, homomorphisms, simulations, and nested abstraction chains.

The public namespace is SM.*. The broad sanity surface is SM.Everything.

Core Concepts

The library gives Formal Foundry a proof-assistant vocabulary for process models:

• Machine, the concrete state-machine presentation;
• runState, which folds a list of inputs into a final state;
• runOutputs, which records emitted output traces;
• Reachable, the inductive reachability relation generated by steps;
• StepInvariant and InvariantFrom, for invariant reasoning;
• Hom, a structure-preserving state map;
• Simulation, a relation preserving one-step output and future relatedness;
• BehavioralEquiv, a pair of homomorphisms in opposite directions.

The property modules include append laws for executions, invariant lifting over runs, reachability after runs, homomorphic preservation of runs and reachability, input-trace extraction from reachability proofs, simulation soundness, and preservation by product and serial composition.

Nested Machines

SM.Nested builds abstraction chains from homomorphic collapses. That is directly relevant to State Machine Studio: the UI stores hierarchical machines with concrete layers collapsing into abstract layers, and the Agda library supplies the language for reasoning about those chains.

The nested modules include JSON and text import/export tooling. The JSON generated by SM.Nested.JSONExport can be turned back into a readable Agda module, which is the right bridge between browser-edited machine data and proof-assistant review.

How It Fits

cubical-sm is the process-model foundation for State Machine Studio and for later temporal-logic work. It turns state-machine diagrams into checked objects with execution laws, reachability, homomorphisms, simulations, and abstraction maps.

Many Formal Foundry products begin with process language: a rulebook has cases, a workflow has states, a system has transitions, and a domain model has abstract and concrete levels. Ordinary diagrams are useful, but they are usually informal.

cubical-sm makes that process language checkable. It can say that a machine runs, that a state is reachable, that an invariant holds after a run, or that one machine preserves another machine’s behavior through a structure-preserving map.

The nested layer is especially product-facing. State Machine Studio works with hierarchical machines, concrete layers, abstract layers, and collapse maps between them. SM.Nested gives those ideas a checked vocabulary and an interchange route through structural JSON and text formats.

The public message is practical: state-machine models are not only drawings. In this stack, they can become checked objects with execution laws, reachability, simulations, homomorphisms, and abstraction maps.