Module governed_commit 

Bounded governed-commit assembly used by the semantic bridge.

Structs

GovernedCommit

One bounded integrated request. The component fields are the actual executable carriers; the remaining fields expose the external effect, persistence, failure, and recovery boundary absent from the individual rows.

Enums

AbstractPhase

Frozen abstract phases for the direct source-level refinement proof. These are the same five observations used by GovernedCommitAbstract.tla.

CommitPhase

Concrete phase of the bounded governed-commit assembly.