remora/docs/protocol/RemoraCombined.cfg

SPECIFICATION SafetySpec

CHECK_DEADLOCK TRUE

\* Combined contention: both local and deployment-wide limits constrain work.
\* Shrunk from 3 jobs to 2 so TLC finishes in minutes; Local=1 and Global=2
\* still force both limiters to bind under two live workers.
CONSTANTS
    Jobs = {j1, j2}
    Workers = {w1, w2}
    InitialWorkers = {w1, w2}
    NoJob = NoJob
    NoWorker = NoWorker
    MaxAttempts = 1
    MaxProgress = 1
    LeaseLimit = 1
    ReservationLimit = 1
    LocalLimit = 1
    GlobalLimit = 2
    FaultsEnabled = FALSE
    FaultServices = {}
    MaxCoordLosses = 0
    MaxPartitions = 0
    MaxCredentialIntents = 0

INVARIANTS
    TypeOK
    StateConsistency
    AllocatedTokensUsed
    LiveProgressWellFormed
    LiveProgressCompatibleWithLiveLease
    AtMostOneLiveLeasePerJob
    AuthorityWellFormed
    CommittedResultConsistent
    CancellationSafety
    PermitSafety
    ResumeValidity
    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
			`\* Combined contention: both local and deployment-wide limits constrain work.`
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			`\* Shrunk from 3 jobs to 2 so TLC finishes in minutes; Local=1 and Global=2`
			`\* still force both limiters to bind under two live workers.`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`CONSTANTS`
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			`Jobs = {j1, j2}`
Add initial draft of Remora model 2026-07-10 11:39:49 +09:00			`Workers = {w1, w2}`
			`InitialWorkers = {w1, w2}`
			`NoJob = NoJob`
			`NoWorker = NoWorker`
			`MaxAttempts = 1`
			`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 = 2`
			`FaultsEnabled = FALSE`
			`FaultServices = {}`
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 = 0`
			`MaxPartitions = 0`
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`
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`