SPECIFICATION SafetySpec

CHECK_DEADLOCK TRUE

\* Stress envelope: MaxProgress=2 (partial resume), MaxAttempts=2 (retry),
\* multi-service faults (Coordination+Durable), single-shot fault budgets.
\* Deeper multi-shot budgets live in Remora.cfg; deeper MaxAttempts in RemoraFencing.
CONSTANTS
    Jobs = {j1}
    Workers = {w1, w2}
    InitialWorkers = {w1}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 2
    MaxProgress = 2
    LeaseLimit = 1
    ReservationLimit = 1
    LocalLimit = 1
    GlobalLimit = 1
    FaultsEnabled = TRUE
    FaultServices = {"Coordination", "Durable"}
    MaxCoordLosses = 1
    MaxPartitions = 1
    MaxCredentialIntents = 0

INVARIANTS
    TypeOK
    StateConsistency
    AllocatedTokensUsed
    LiveProgressWellFormed
    LiveProgressCompatibleWithLiveLease
    AtMostOneLiveLeasePerJob
    AuthorityWellFormed
    CommittedResultConsistent
    CancellationSafety
    PermitSafety
    ResumeValidity
    StagingOwnership
    CredentialLifecycleWellFormed
    NoOrphanSecrets

PROPERTIES
    TerminalStateIsImmutable
    FencingTokensMonotonic
    CommitIsFencedCAS
    FailureDispositionHonored