`RoostReleaseSync`

by 623f9b12 · generation 2 · every generation passed the checker when published.

Two-store release sync: a single-threaded configuration store applies changes and a git-shaped history store versions them as commits. Interface changes (apply, commit+move ref, record head) and pushes (import objects, CAS+apply in the config store, move ref) may crash between steps; three idempotent reconcile rules run on restart. Checks quiescent agreement of both stores, no lost push between racing pushers, no dropped items under rollback, and refs never dangling.

Raw .tla Raw .cfg

RoostReleaseSync.tla

MODULE RoostReleaseSync

Two-store release sync: a configuration store and a git-shaped history store, kept consistent across crashes and racing writers.

A tenant's configuration ("the manifest": a set of items, each active or archived) is applied in one single-threaded store (the config store) and versioned as commits in a second store (the repo). Changes arrive two ways:

Interface change (three steps under a mutex held by the config store) Change1 apply the mutation to the live configuration (one transaction; the mutex is taken) Change2 write a commit whose tree is the new configuration and move the repo's main ref to it Change3 record that commit as `head` in the config store; release

Push (a client pushes a commit it built on a base it cloned) Push0 the repo imports the commit's objects (content-addressed: harmless if the push is later rejected) Push2 the config store takes the mutex and does the real compare-and-set: head must equal the pusher's base; validates the tree (a known item may be archived, never dropped) and applies it; records head := new Push3 still under the mutex, main := new; release

A crash may hit between any two steps. On restart, before serving anything, Reconcile runs three idempotent rules: (a) if main's tree equals the live configuration, adopt main as head; else (b) if head's tree differs from the live configuration, commit the configuration on top of main and point both at it; else (c) if main differs from head, move main to head.

Rollback is "revert to": a change whose new configuration is an older commit's tree with every item known since then archived, never dropped.

EXTENDS Naturals, FiniteSets

CONSTANTS
Items,	configuration items (objects, tools, pages, ...)
Pushers,	clients that each push once
MaxCommits,	commit ids 1..MaxCommits; 0 = the empty initial commit
MaxChanges,	bound on interface changes (incl. rollbacks) per run
NoObs	model value: no tool-call observation

States ≜ {"absent", "active", "archived"}

Manifests ≜ [Items → States]

Empty ≜ [i ∈ Items ↦ "absent"]

CommitIds ≜ 0..MaxCommits

Kinds ≜ {"create", "archive", "unarchive"}

Muts ≜ Kinds × Items

VARIABLES
applied,	the live configuration (the truth)
head,	commit the config store believes it is at
main,	the repo's main ref
objects,	commit ids present in the repo (1..MaxCommits)
tree,	CommitIds -> Manifests (tree of each commit; Empty when unallocated)
nextCommit,	next free commit id
lock,	"free" \| "change" \| a pusher
phase,	interface change in flight: "idle" \| "applied" \| "committed"
pending,	commit written by Change2, awaiting Change3
changes,	interface changes started so far
booted,	FALSE from a crash until Reconcile has run
pst,	Pushers -> "idle" \| "imported" \| "applied" \| "done" \| "rejected" \| "crashed"
pbase,	Pushers -> base commit the push was built on
pnew,	Pushers -> the pushed commit
padopted,	Pushers -> TRUE once the config store applied this push
known,	Items -> TRUE once the item has ever been active
obs	observation: the configuration a tool call saw, cleared by other steps

vars ≜ ⟨applied, head, main, objects, tree, nextCommit, lock, phase, pending, changes,

booted, pst, pbase, pnew, padopted, known, obs⟩

PushStates ≜ {"idle", "imported", "applied", "done", "rejected", "crashed"}

TypeOK ≜

∧ applied ∈ Manifests

∧ head ∈ CommitIds

∧ main ∈ CommitIds

∧ objects ⊆ 1..MaxCommits

∧ tree ∈ [CommitIds → Manifests]

∧ nextCommit ∈ 1..(MaxCommits + 1)

∧ lock ∈ {"free", "change"} ∪ Pushers

∧ phase ∈ {"idle", "applied", "committed"}

∧ pending ∈ CommitIds

∧ changes ∈ 0..MaxChanges

∧ booted ∈ BOOLEAN

∧ pst ∈ [Pushers → PushStates]

∧ pbase ∈ [Pushers → CommitIds]

∧ pnew ∈ [Pushers → CommitIds]

∧ padopted ∈ [Pushers → BOOLEAN]

∧ known ∈ [Items → BOOLEAN]

∧ obs ∈ Manifests ∪ {NoObs}

Init ≜

∧ applied = Empty

∧ head = 0

∧ main = 0

∧ objects = {}

∧ tree = [c ∈ CommitIds ↦ Empty]

∧ nextCommit = 1

∧ lock = "free"

∧ phase = "idle"

∧ pending = 0

∧ changes = 0

∧ booted = TRUE

∧ pst = [p ∈ Pushers ↦ "idle"]

∧ pbase = [p ∈ Pushers ↦ 0]

∧ pnew = [p ∈ Pushers ↦ 0]

∧ padopted = [p ∈ Pushers ↦ FALSE]

∧ known = [i ∈ Items ↦ FALSE]

∧ obs = NoObs

---------------------------------------------------------------- helpers

Enabled(M, m) ≜

CASE m[1] = "create" → M[m[2]] = "absent"

□ m[1] = "archive" → M[m[2]] = "active"

□ m[1] = "unarchive" → M[m[2]] = "archived"

Mutate(M, m) ≜

[M EXCEPT ![m[2]] = IF m[1] = "archive" THEN "archived" ELSE "active"]

Rollback semantics: an item active in the target is active; an item the live configuration knows but the target does not have active is archived; nothing is dropped.

RevertTo(M, T) ≜

[i ∈ Items ↦ IF T[i] = "active" THEN "active"

ELSE IF M[i] ≠ "absent" THEN "archived" ELSE "absent"]

The validator: a pushed tree may not drop an item the configuration has.

Valid(T) ≜ ∀ i ∈ Items : applied[i] ≠ "absent" ⇒ T[i] ≠ "absent"

Known(M) ≜ [i ∈ Items ↦ known[i] ∨ M[i] ≠ "absent"]

Quiet ≜ booted ∧ lock = "free"

-------------------------------------------------------- interface change

Change1(m) ≜

∧ Quiet ∧ phase = "idle" ∧ changes < MaxChanges

∧ Enabled(applied, m)

∧ applied^′ = Mutate(applied, m)

∧ known^′ = Known(applied^′)

∧ lock^′ = "change" ∧ phase^′ = "applied" ∧ changes^′ = changes + 1

∧ obs^′ = NoObs

∧ UNCHANGED ⟨head, main, objects, tree, nextCommit, pending, booted, pst, pbase, pnew, padopted⟩

Rollback1(c) ≜

∧ Quiet ∧ phase = "idle" ∧ changes < MaxChanges

∧ c ∈ objects ∪ {0}

∧ RevertTo(applied, tree[c]) ≠ applied

∧ applied^′ = RevertTo(applied, tree[c])

∧ known^′ = Known(applied^′)

∧ lock^′ = "change" ∧ phase^′ = "applied" ∧ changes^′ = changes + 1

∧ obs^′ = NoObs

∧ UNCHANGED ⟨head, main, objects, tree, nextCommit, pending, booted, pst, pbase, pnew, padopted⟩

Change2 ≜

∧ booted ∧ phase = "applied" ∧ nextCommit ≤ MaxCommits

∧ LET c ≜ nextCommit IN

∧ tree^′ = [tree EXCEPT ![c] = applied]

∧ objects^′ = objects ∪ {c}

∧ main^′ = c

∧ pending^′ = c

∧ nextCommit^′ = c + 1

∧ phase^′ = "committed"

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, head, lock, changes, booted, pst, pbase, pnew, padopted, known⟩

Change3 ≜

∧ booted ∧ phase = "committed"

∧ head^′ = pending

∧ pending^′ = 0 ∧ phase^′ = "idle" ∧ lock^′ = "free"

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, main, objects, tree, nextCommit, changes, booted, pst, pbase, pnew, padopted, known⟩

-------------------------------------------------------------------- push

The pusher clones main, edits, and pushes: objects land first. It may push a valid mutation or an invalid tree that drops an item.

PushTrees(B) ≜

{Mutate(tree[B], m) : m ∈ {m ∈ Muts : Enabled(tree[B], m)}}

∪ {[tree[B] EXCEPT ![i] = "absent"] : i ∈ {i ∈ Items : tree[B][i] ≠ "absent"}}

Push0(p) ≜

∧ booted ∧ pst[p] = "idle" ∧ nextCommit ≤ MaxCommits

∧ ∃ T ∈ PushTrees(main) :

LET c ≜ nextCommit IN

∧ tree^′ = [tree EXCEPT ![c] = T]

∧ objects^′ = objects ∪ {c}

∧ pbase^′ = [pbase EXCEPT ![p] = main]

∧ pnew^′ = [pnew EXCEPT ![p] = c]

∧ nextCommit^′ = c + 1

∧ pst^′ = [pst EXCEPT ![p] = "imported"]

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, head, main, lock, phase, pending, changes, booted, padopted, known⟩

The compare-and-set lives here, in the single-threaded config store.

Push2(p) ≜

∧ Quiet ∧ pst[p] = "imported"

∧ IF head = pbase[p] ∧ Valid(tree[pnew[p]])

THEN ∧ applied^′ = tree[pnew[p]]

∧ known^′ = Known(applied^′)

∧ head^′ = pnew[p]

∧ lock^′ = p

∧ pst^′ = [pst EXCEPT ![p] = "applied"]

∧ padopted^′ = [padopted EXCEPT ![p] = TRUE]

ELSE ∧ pst^′ = [pst EXCEPT ![p] = "rejected"]

∧ UNCHANGED ⟨applied, known, head, lock, padopted⟩

∧ obs^′ = NoObs

∧ UNCHANGED ⟨main, objects, tree, nextCommit, phase, pending, changes, booted, pbase, pnew⟩

Push3(p) ≜

∧ booted ∧ pst[p] = "applied" ∧ lock = p

∧ main^′ = pnew[p]

∧ pst^′ = [pst EXCEPT ![p] = "done"]

∧ lock^′ = "free"

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, head, objects, tree, nextCommit, phase, pending, changes, booted, pbase, pnew, padopted, known⟩

---------------------------------------------------------- crash/recover

Crash ≜

∧ booted

∧ booted^′ = FALSE

∧ lock^′ = "free" ∧ phase^′ = "idle" ∧ pending^′ = 0

∧ pst^′ = [p ∈ Pushers ↦ IF pst[p] ∈ {"imported", "applied"} THEN "crashed" ELSE pst[p]]

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, head, main, objects, tree, nextCommit, changes, pbase, pnew, padopted, known⟩

Reconcile ≜

∧ ¬booted

∧ IF main ≠ 0 ∧ tree[main] = applied

THEN ∧ head^′ = main

∧ UNCHANGED ⟨main, objects, tree, nextCommit⟩

ELSE IF tree[head] ≠ applied

THEN ∧ nextCommit ≤ MaxCommits

∧ LET c ≜ nextCommit IN

∧ tree^′ = [tree EXCEPT ![c] = applied]

∧ objects^′ = objects ∪ {c}

∧ main^′ = c

∧ head^′ = c

∧ nextCommit^′ = c + 1

ELSE ∧ main^′ = head

∧ UNCHANGED ⟨head, objects, tree, nextCommit⟩

∧ booted^′ = TRUE

∧ obs^′ = NoObs

∧ UNCHANGED ⟨applied, lock, phase, pending, changes, pst, pbase, pnew, padopted, known⟩

------------------------------------------------------------- observation

ToolCall ≜

∧ booted

∧ obs^′ = applied

∧ UNCHANGED ⟨applied, head, main, objects, tree, nextCommit, lock, phase, pending, changes,

booted, pst, pbase, pnew, padopted, known⟩

Next ≜

∨ ∃ m ∈ Muts : Change1(m)

∨ ∃ c ∈ CommitIds : Rollback1(c)

∨ Change2 ∨ Change3

∨ ∃ p ∈ Pushers : Push0(p) ∨ Push2(p) ∨ Push3(p)

∨ Crash ∨ Reconcile ∨ ToolCall

Spec ≜ Init ∧ □[Next]_vars

Invariants

Whenever the store has booted and no change is in flight, the repo's main names exactly the applied configuration and the pointer agrees.

AppliedMatchesMainAfterReconcile ≜

Quiet ⇒ (main = head ∧ tree[head] = applied)

A tool call sees the whole applied configuration, and when nothing is in flight that configuration is a committed release.

CallSeesOneRelease ≜

obs ≠ NoObs ⇒ (obs = applied ∧ (lock ≠ "free" ∨ ∃ c ∈ objects ∪ {0} : tree[c] = obs))

An item that was ever active is still present (active or archived).

NothingDropped ≜

∀ i ∈ Items : known[i] ⇒ applied[i] ≠ "absent"

RefNeverDangles ≜

∧ main ∈ objects ∪ {0}

∧ head ∈ objects ∪ {0}

Two pushes built on the same base cannot both be applied: one must be told it is stale.

NoLostPush ≜

∀ p, q ∈ Pushers : p ≠ q ⇒ ¬(padopted[p] ∧ padopted[q] ∧ pbase[p] = pbase[q])

RoostReleaseSync.cfg

CONSTANTS

Items = {a, b}

Pushers = {p1, p2}

MaxCommits = 5

MaxChanges = 2

NoObs = NoObs

SPECIFICATION Spec

INVARIANT TypeOK

INVARIANT AppliedMatchesMainAfterReconcile

INVARIANT CallSeesOneRelease

INVARIANT NothingDropped

INVARIANT RefNeverDangles

INVARIANT NoLostPush

CHECK_DEADLOCK FALSE

----------------------------- MODULE RoostReleaseSync ----------------------------- (***************************************************************************) (* Two-store release sync: a configuration store and a git-shaped history *) (* store, kept consistent across crashes and racing writers. *) (* *) (* A tenant's configuration ("the manifest": a set of items, each active *) (* or archived) is applied in one single-threaded store (the config store) *) (* and versioned as commits in a second store (the repo). Changes arrive *) (* two ways: *) (* *) (* Interface change (three steps under a mutex held by the config store) *) (* Change1 apply the mutation to the live configuration (one *) (* transaction; the mutex is taken) *) (* Change2 write a commit whose tree is the new configuration and *) (* move the repo's main ref to it *) (* Change3 record that commit as `head` in the config store; release *) (* *) (* Push (a client pushes a commit it built on a base it cloned) *) (* Push0 the repo imports the commit's objects (content-addressed: *) (* harmless if the push is later rejected) *) (* Push2 the config store takes the mutex and does the real *) (* compare-and-set: head must equal the pusher's base; *) (* validates the tree (a known item may be archived, never *) (* dropped) and applies it; records head := new *) (* Push3 still under the mutex, main := new; release *) (* *) (* A crash may hit between any two steps. On restart, before serving *) (* anything, Reconcile runs three idempotent rules: (a) if main's tree *) (* equals the live configuration, adopt main as head; else (b) if head's *) (* tree differs from the live configuration, commit the configuration on *) (* top of main and point both at it; else (c) if main differs from head, *) (* move main to head. *) (* *) (* Rollback is "revert to": a change whose new configuration is an older *) (* commit's tree with every item known since then archived, never dropped. *) (***************************************************************************) EXTENDS Naturals, FiniteSets CONSTANTS Items, \* configuration items (objects, tools, pages, ...) Pushers, \* clients that each push once MaxCommits, \* commit ids 1..MaxCommits; 0 = the empty initial commit MaxChanges, \* bound on interface changes (incl. rollbacks) per run NoObs \* model value: no tool-call observation States == {"absent", "active", "archived"} Manifests == [Items -> States] Empty == [i \in Items |-> "absent"] CommitIds == 0..MaxCommits Kinds == {"create", "archive", "unarchive"} Muts == Kinds \X Items VARIABLES applied, \* the live configuration (the truth) head, \* commit the config store believes it is at main, \* the repo's main ref objects, \* commit ids present in the repo (1..MaxCommits) tree, \* CommitIds -> Manifests (tree of each commit; Empty when unallocated) nextCommit, \* next free commit id lock, \* "free" | "change" | a pusher phase, \* interface change in flight: "idle" | "applied" | "committed" pending, \* commit written by Change2, awaiting Change3 changes, \* interface changes started so far booted, \* FALSE from a crash until Reconcile has run pst, \* Pushers -> "idle" | "imported" | "applied" | "done" | "rejected" | "crashed" pbase, \* Pushers -> base commit the push was built on pnew, \* Pushers -> the pushed commit padopted, \* Pushers -> TRUE once the config store applied this push known, \* Items -> TRUE once the item has ever been active obs \* observation: the configuration a tool call saw, cleared by other steps vars == <<applied, head, main, objects, tree, nextCommit, lock, phase, pending, changes, booted, pst, pbase, pnew, padopted, known, obs>> PushStates == {"idle", "imported", "applied", "done", "rejected", "crashed"} TypeOK == /\ applied \in Manifests /\ head \in CommitIds /\ main \in CommitIds /\ objects \subseteq 1..MaxCommits /\ tree \in [CommitIds -> Manifests] /\ nextCommit \in 1..(MaxCommits + 1) /\ lock \in {"free", "change"} \cup Pushers /\ phase \in {"idle", "applied", "committed"} /\ pending \in CommitIds /\ changes \in 0..MaxChanges /\ booted \in BOOLEAN /\ pst \in [Pushers -> PushStates] /\ pbase \in [Pushers -> CommitIds] /\ pnew \in [Pushers -> CommitIds] /\ padopted \in [Pushers -> BOOLEAN] /\ known \in [Items -> BOOLEAN] /\ obs \in Manifests \cup {NoObs} Init == /\ applied = Empty /\ head = 0 /\ main = 0 /\ objects = {} /\ tree = [c \in CommitIds |-> Empty] /\ nextCommit = 1 /\ lock = "free" /\ phase = "idle" /\ pending = 0 /\ changes = 0 /\ booted = TRUE /\ pst = [p \in Pushers |-> "idle"] /\ pbase = [p \in Pushers |-> 0] /\ pnew = [p \in Pushers |-> 0] /\ padopted = [p \in Pushers |-> FALSE] /\ known = [i \in Items |-> FALSE] /\ obs = NoObs (* ---------------------------------------------------------------- helpers *) Enabled(M, m) == CASE m[1] = "create" -> M[m[2]] = "absent" [] m[1] = "archive" -> M[m[2]] = "active" [] m[1] = "unarchive" -> M[m[2]] = "archived" Mutate(M, m) == [M EXCEPT ![m[2]] = IF m[1] = "archive" THEN "archived" ELSE "active"] (* Rollback semantics: an item active in the target is active; an item the live configuration knows but the target does not have active is archived; nothing is dropped. *) RevertTo(M, T) == [i \in Items |-> IF T[i] = "active" THEN "active" ELSE IF M[i] # "absent" THEN "archived" ELSE "absent"] (* The validator: a pushed tree may not drop an item the configuration has. *) Valid(T) == \A i \in Items : applied[i] # "absent" => T[i] # "absent" Known(M) == [i \in Items |-> known[i] \/ M[i] # "absent"] Quiet == booted /\ lock = "free" (* -------------------------------------------------------- interface change *) Change1(m) == /\ Quiet /\ phase = "idle" /\ changes < MaxChanges /\ Enabled(applied, m) /\ applied' = Mutate(applied, m) /\ known' = Known(applied') /\ lock' = "change" /\ phase' = "applied" /\ changes' = changes + 1 /\ obs' = NoObs /\ UNCHANGED <<head, main, objects, tree, nextCommit, pending, booted, pst, pbase, pnew, padopted>> Rollback1(c) == /\ Quiet /\ phase = "idle" /\ changes < MaxChanges /\ c \in objects \cup {0} /\ RevertTo(applied, tree[c]) # applied /\ applied' = RevertTo(applied, tree[c]) /\ known' = Known(applied') /\ lock' = "change" /\ phase' = "applied" /\ changes' = changes + 1 /\ obs' = NoObs /\ UNCHANGED <<head, main, objects, tree, nextCommit, pending, booted, pst, pbase, pnew, padopted>> Change2 == /\ booted /\ phase = "applied" /\ nextCommit <= MaxCommits /\ LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = applied] /\ objects' = objects \cup {c} /\ main' = c /\ pending' = c /\ nextCommit' = c + 1 /\ phase' = "committed" /\ obs' = NoObs /\ UNCHANGED <<applied, head, lock, changes, booted, pst, pbase, pnew, padopted, known>> Change3 == /\ booted /\ phase = "committed" /\ head' = pending /\ pending' = 0 /\ phase' = "idle" /\ lock' = "free" /\ obs' = NoObs /\ UNCHANGED <<applied, main, objects, tree, nextCommit, changes, booted, pst, pbase, pnew, padopted, known>> (* -------------------------------------------------------------------- push *) (* The pusher clones main, edits, and pushes: objects land first. It may push a valid mutation or an invalid tree that drops an item. *) PushTrees(B) == {Mutate(tree[B], m) : m \in {m \in Muts : Enabled(tree[B], m)}} \cup {[tree[B] EXCEPT ![i] = "absent"] : i \in {i \in Items : tree[B][i] # "absent"}} Push0(p) == /\ booted /\ pst[p] = "idle" /\ nextCommit <= MaxCommits /\ \E T \in PushTrees(main) : LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = T] /\ objects' = objects \cup {c} /\ pbase' = [pbase EXCEPT ![p] = main] /\ pnew' = [pnew EXCEPT ![p] = c] /\ nextCommit' = c + 1 /\ pst' = [pst EXCEPT ![p] = "imported"] /\ obs' = NoObs /\ UNCHANGED <<applied, head, main, lock, phase, pending, changes, booted, padopted, known>> (* The compare-and-set lives here, in the single-threaded config store. *) Push2(p) == /\ Quiet /\ pst[p] = "imported" /\ IF head = pbase[p] /\ Valid(tree[pnew[p]]) THEN /\ applied' = tree[pnew[p]] /\ known' = Known(applied') /\ head' = pnew[p] /\ lock' = p /\ pst' = [pst EXCEPT ![p] = "applied"] /\ padopted' = [padopted EXCEPT ![p] = TRUE] ELSE /\ pst' = [pst EXCEPT ![p] = "rejected"] /\ UNCHANGED <<applied, known, head, lock, padopted>> /\ obs' = NoObs /\ UNCHANGED <<main, objects, tree, nextCommit, phase, pending, changes, booted, pbase, pnew>> Push3(p) == /\ booted /\ pst[p] = "applied" /\ lock = p /\ main' = pnew[p] /\ pst' = [pst EXCEPT ![p] = "done"] /\ lock' = "free" /\ obs' = NoObs /\ UNCHANGED <<applied, head, objects, tree, nextCommit, phase, pending, changes, booted, pbase, pnew, padopted, known>> (* ---------------------------------------------------------- crash/recover *) Crash == /\ booted /\ booted' = FALSE /\ lock' = "free" /\ phase' = "idle" /\ pending' = 0 /\ pst' = [p \in Pushers |-> IF pst[p] \in {"imported", "applied"} THEN "crashed" ELSE pst[p]] /\ obs' = NoObs /\ UNCHANGED <<applied, head, main, objects, tree, nextCommit, changes, pbase, pnew, padopted, known>> Reconcile == /\ ~booted /\ IF main # 0 /\ tree[main] = applied THEN /\ head' = main /\ UNCHANGED <<main, objects, tree, nextCommit>> ELSE IF tree[head] # applied THEN /\ nextCommit <= MaxCommits /\ LET c == nextCommit IN /\ tree' = [tree EXCEPT ![c] = applied] /\ objects' = objects \cup {c} /\ main' = c /\ head' = c /\ nextCommit' = c + 1 ELSE /\ main' = head /\ UNCHANGED <<head, objects, tree, nextCommit>> /\ booted' = TRUE /\ obs' = NoObs /\ UNCHANGED <<applied, lock, phase, pending, changes, pst, pbase, pnew, padopted, known>> (* ------------------------------------------------------------- observation *) ToolCall == /\ booted /\ obs' = applied /\ UNCHANGED <<applied, head, main, objects, tree, nextCommit, lock, phase, pending, changes, booted, pst, pbase, pnew, padopted, known>> Next == \/ \E m \in Muts : Change1(m) \/ \E c \in CommitIds : Rollback1(c) \/ Change2 \/ Change3 \/ \E p \in Pushers : Push0(p) \/ Push2(p) \/ Push3(p) \/ Crash \/ Reconcile \/ ToolCall Spec == Init /\ [][Next]_vars (***************************************************************************) (* Invariants *) (***************************************************************************) (* Whenever the store has booted and no change is in flight, the repo's main names exactly the applied configuration and the pointer agrees. *) AppliedMatchesMainAfterReconcile == Quiet => (main = head /\ tree[head] = applied) (* A tool call sees the whole applied configuration, and when nothing is in flight that configuration is a committed release. *) CallSeesOneRelease == obs # NoObs => (obs = applied /\ (lock # "free" \/ \E c \in objects \cup {0} : tree[c] = obs)) (* An item that was ever active is still present (active or archived). *) NothingDropped == \A i \in Items : known[i] => applied[i] # "absent" RefNeverDangles == /\ main \in objects \cup {0} /\ head \in objects \cup {0} (* Two pushes built on the same base cannot both be applied: one must be told it is stale. *) NoLostPush == \A p, q \in Pushers : p # q => ~(padopted[p] /\ padopted[q] /\ pbase[p] = pbase[q]) =============================================================================

Generations

gen	changes	distinct states	depth	published	raw
2 (latest)	Wider bounds: two interface changes and five commit ids; same model.	56969	16	2026-09-11 05:47:01 UTC	.tla .cfg
1	Initial model: mutex-held push path with the compare-and-set in the configuration store; crash between every step; reconcile with adopt / commit-on-top / move-ref rules.	8253	13	2026-09-11 05:43:55 UTC	.tla .cfg

Defend this spec

Ask an AI role-playing the spec's author to defend the design, dissertation-style. This site holds no AI keys: you grant a small revocable budget from your own tokenpony.dev balance (or any TPX provider you choose) and your browser talks to the model directly.

Loading…