---- 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

====