remora/docs/protocol/RemoraFencing.cfg

SPECIFICATION SafetySpec

CHECK_DEADLOCK TRUE

\* Repeated fencing with delayed outcomes, lease loss, and replacement.
\* MaxAttempts=3 stresses token replacement; fault budgets kept at 1 for TLC size.
CONSTANTS
    Jobs = {j1}
    Workers = {w1, w2}
    InitialWorkers = {w1}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 3
    MaxProgress = 1
    LeaseLimit = 1
    ReservationLimit = 1
    LocalLimit = 1
    GlobalLimit = 1
    FaultsEnabled = TRUE
    FaultServices = {"Coordination"}
    MaxCoordLosses = 1
    MaxPartitions = 1
    MaxCredentialIntents = 0

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

PROPERTIES
    TerminalStateIsImmutable
    FencingTokensMonotonic
    CommitIsFencedCAS
    FailureDispositionHonored
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`SPECIFICATION SafetySpec`

Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`CHECK_DEADLOCK TRUE`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`\* Repeated fencing with delayed outcomes, lease loss, and replacement.`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`\* MaxAttempts=3 stresses token replacement; fault budgets kept at 1 for TLC size.`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`CONSTANTS`
			`Jobs = {j1}`
			`Workers = {w1, w2}`
			`InitialWorkers = {w1}`
			`NoJob = NoJob`
			`NoWorker = NoWorker`
			`MaxAttempts = 3`
			`MaxProgress = 1`
			`LeaseLimit = 1`
Specify fenced activation and source credential contracts Define bounded reservation recovery, exact activation replay fencing, immutable source identities, and deployment-owned secret and target policy boundaries. Align the OpenAPI contract and add a split-store activation safety refinement. 2026-07-14 18:12:28 +09:00			`ReservationLimit = 1`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`LocalLimit = 1`
			`GlobalLimit = 1`
			`FaultsEnabled = TRUE`
			`FaultServices = {"Coordination"}`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`MaxCoordLosses = 1`
			`MaxPartitions = 1`
Model durable ownership for credential secrets 2026-07-16 23:01:17 +09:00			`MaxCredentialIntents = 0`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`INVARIANTS`
			`TypeOK`
			`StateConsistency`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`AllocatedTokensUsed`
Weaken live progress to a coordination-only hint (IF-6). Drop LiveProgressAligned in favor of well-formedness and lease-compatible progress, stop durable CAS from clearing Redis progress, and add ambient ClearStaleLiveProgress so TLC matches Postgres + Dragonfly separation. 2026-07-10 14:16:29 +09:00			`LiveProgressWellFormed`
			`LiveProgressCompatibleWithLiveLease`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`AtMostOneLiveLeasePerJob`
			`AuthorityWellFormed`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`CommittedResultConsistent`
			`CancellationSafety`
			`PermitSafety`
			`ResumeValidity`
Model checkpoint staging ownership transfer 2026-07-17 15:01:15 +09:00			`CheckpointStagingOwnership`
Strengthen JobProtocol model after independent review. Replace tautological invariants with non-trivial ones, allow multi-shot coordination loss and re-partition, fix reap/progress lifecycle, enable deadlock checking via Done, and add stress and multi-shot TLC configs. 2026-07-10 12:43:32 +09:00			`StagingOwnership`
Model durable ownership for credential secrets 2026-07-16 23:01:17 +09:00			`CredentialLifecycleWellFormed`
			`NoOrphanSecrets`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00
			`PROPERTIES`
			`TerminalStateIsImmutable`
			`FencingTokensMonotonic`
			`CommitIsFencedCAS`
Model durable failure disposition 2026-07-13 16:41:51 +09:00			`FailureDispositionHonored`