DistRefs

---- MODULE DistRefs ---- (***************************************************************************) (* Dist-ref publish/serve protocol for a git-backed site. *) (* *) (* Two server refs matter for serving: "main" (source history) and "dist" *) (* (the served artifact snapshot). Serving is ONE atomic read with *) (* fallback: serve dist when it exists, else main. Push policy (enforced *) (* server-side): main and dist are owner-only; a visitor may only push *) (* their own fork ref. Fork refs are never read by serving, so they are *) (* abstracted away here (their policy is checked in ForkRefs.tla). *) (* *) (* Owner publish of draft d is TWO pushes that are NOT atomic together: *) (* 1. push dist <- d (full self-contained tree, sources+builds) *) (* 2. push main <- src(d) (filtered source-only commit) *) (* Either push can fail or be delayed; a newer publish can overlap the *) (* window between them. Trees are abstract draft ids 1..2; main holds a *) (* source id (0 = initial seed); dist holds a draft id or is absent. *) (***************************************************************************) EXTENDS Naturals, TLC (* TRUE: the server's receive-pack policy rejects non-owner pushes to *) (* dist. FALSE: the guard is disabled, admitting the visitor attack. *) CONSTANT GuardDist Seed == 0 \* initial source commit on main NoDraft == 0 \* dist absent Drafts == 1..2 \* two sequential drafts bound the model VARIABLES dist, \* draft id currently on the dist ref, or NoDraft distAuthor, \* who pushed it: "none" | "owner" | "visitor" main, \* source id on main: Seed or a published draft's source phase \* per-draft publish progress vars == <<dist, distAuthor, main, phase>> Phases == {"idle", "distDone", "done", "distFail", "mainFail"} (* The serving rule: one atomic read, dist preferred, main as fallback. *) (* main's author is always "owner": main is owner-only under the same *) (* receive-pack policy (modeled and checked in ForkRefs.tla). *) Served == IF dist # NoDraft THEN [ref |-> "dist", id |-> dist, author |-> distAuthor] ELSE [ref |-> "main", id |-> main, author |-> "owner"] TypeOK == /\ dist \in {NoDraft} \cup Drafts /\ distAuthor \in {"none", "owner", "visitor"} /\ (dist = NoDraft) <=> (distAuthor = "none") /\ main \in {Seed} \cup Drafts /\ phase \in [Drafts -> Phases] Init == /\ dist = NoDraft /\ distAuthor = "none" /\ main = Seed /\ phase = [d \in Drafts |-> "idle"] (* Drafts publish in order; draft d may start once every earlier draft's *) (* dist push has resolved (ok or fail) -- so publish d can overlap an *) (* earlier publish whose main push is still pending or failed. *) CanStart(d) == /\ phase[d] = "idle" /\ \A e \in Drafts : e < d => phase[e] # "idle" (* Owner push 1 of 2: the full draft tree lands on dist. *) PushDistOK(d) == /\ CanStart(d) /\ dist' = d /\ distAuthor' = "owner" /\ phase' = [phase EXCEPT ![d] = "distDone"] /\ UNCHANGED main (* The dist push fails; the publish aborts before touching main. *) PushDistFail(d) == /\ CanStart(d) /\ phase' = [phase EXCEPT ![d] = "distFail"] /\ UNCHANGED <<dist, distAuthor, main>> (* Owner push 2 of 2: the filtered source commit lands on main. Possibly *) (* delayed past a newer publish's dist push (force-push, no CAS on this *) (* edge in the client). *) PushMainOK(d) == /\ phase[d] = "distDone" /\ main' = d /\ phase' = [phase EXCEPT ![d] = "done"] /\ UNCHANGED <<dist, distAuthor>> (* The main push fails permanently: dist serves d, src(d) never lands. *) PushMainFail(d) == /\ phase[d] = "distDone" /\ phase' = [phase EXCEPT ![d] = "mainFail"] /\ UNCHANGED <<dist, distAuthor, main>> (* A visitor attempts to push dist. With GuardDist the server's policy *) (* rejects it with no state change (a stutter step, not modeled); with *) (* the guard off the push lands and the visitor controls the served tree. *) VisitorPushDist == /\ ~GuardDist /\ \E d \in Drafts : /\ dist' = d /\ distAuthor' = "visitor" /\ UNCHANGED <<main, phase>> Next == \/ \E d \in Drafts : PushDistOK(d) \/ PushDistFail(d) \/ PushMainOK(d) \/ PushMainFail(d) \/ VisitorPushDist Spec == Init /\ [][Next]_vars ---------------------------------------------------------------------------- (* Invariants *) (* Whatever serving returns was pushed by the owner. Load-bearing on the *) (* receive-pack guard: with GuardDist = FALSE this is violated. *) ServedIsOwnerAuthored == Served.author = "owner" (* Once both pushes of publish d have completed and no newer publish has *) (* started, serving returns draft d. *) ServedCoherence == \A d \in Drafts : (phase[d] = "done" /\ \A e \in Drafts : e > d => phase[e] = "idle") => Served.id = d ====

SPECIFICATION Spec CONSTANT GuardDist = TRUE INVARIANT TypeOK INVARIANT ServedIsOwnerAuthored INVARIANT ServedCoherence CHECK_DEADLOCK FALSE