--------------------------- MODULE PodLifecycle ---------------------------
(***************************************************************************)
(* Sandbox/terminal lifecycle for codepod (worker/index.ts, worker/boot.ts,*)
(* src/main.ts).  One container per user (Cloudflare Sandbox DO).  The     *)
(* container sleeps after 30 idle minutes and sleep WIPES THE DISK: the    *)
(* next wake is a brand-new incarnation with none of the provisioning      *)
(* (tmux, bun, claude, repo clone, .bashrc tmux hook) that boot.sh         *)
(* installed on the previous one.  Incarnations are modeled by a bounded   *)
(* counter `inc`; every wake increments it.                                *)
(*                                                                         *)
(* Container states: "asleep" (no disk state), "fresh" (awake but never    *)
(* provisioned -- what an implicit SDK wake produces), "provisioning"      *)
(* (boot.sh running), "ready" (boot.sh completed on THIS incarnation).     *)
(* Clients (browser tabs, at most 2) run: idle -> booting (POST /api/boot) *)
(* -> believes (boot returned ok, the tab now assumes the pod is ready     *)
(* forever) -> attached (WS /ws/terminal).  SandboxAddon auto-reconnects a *)
(* dropped WS, which re-attaches while still merely *believing* readiness. *)
(* "reset pod" (POST /api/destroy) has the same abstract effect as an idle *)
(* sleep -- container gone, disk wiped, next wake is a new incarnation --  *)
(* so one Sleep action models both.                                        *)
(*                                                                         *)
(* GuardedAttach selects the design variant:                               *)
(*   FALSE = the unguarded design: /ws/terminal reaches the sandbox        *)
(*     directly; if the container slept, the SDK wakes a FRESH container   *)
(*     and attaches to it without re-running boot.sh.  The frontend runs   *)
(*     /api/boot exactly once per page load (src/main.ts main()).          *)
(*   TRUE  = the guarded design: an attach that would land on a non-ready  *)
(*     container instead sends the client back through the boot flow       *)
(*     (e.g. the frontend re-POSTs /api/boot whenever SandboxAddon         *)
(*     reconnects, or the worker probes the ready marker before proxying). *)
(***************************************************************************)
EXTENDS Naturals

CONSTANTS
  Clients,       \* browser tabs of the one user, e.g. {c1, c2}
  MaxInc,        \* bound on container incarnations (wakes)
  GuardedAttach  \* BOOLEAN: design variant, see header

ASSUME GuardedAttach \in BOOLEAN

Incs      == 0..MaxInc
CtrStates == {"asleep", "fresh", "provisioning", "ready"}
Phases    == {"idle", "booting", "believes", "attached"}

VARIABLES
  ctr,     \* container state of the current incarnation
  inc,     \* current incarnation number (0 = never woken)
  client   \* client[c] = [phase, bootInc, attInc]:
           \*   bootInc = incarnation c's last /api/boot ran against
           \*   attInc  = incarnation c's live WS attached to

vars == <<ctr, inc, client>>

ClientState == [phase: Phases, bootInc: Incs, attInc: Incs]

TypeOK ==
  /\ ctr \in CtrStates
  /\ inc \in Incs
  /\ client \in [Clients -> ClientState]

Awake == ctr # "asleep"

Init ==
  /\ ctr = "asleep"
  /\ inc = 0
  /\ client = [c \in Clients |-> [phase |-> "idle", bootInc |-> 0, attInc |-> 0]]

(* POST /api/boot: getSandbox wakes an asleep container (new incarnation), *)
(* then boot.sh starts.  On an already-ready container the marker check    *)
(* makes it a no-op, so ctr stays "ready"; on a fresh/provisioning one it  *)
(* (re)runs, which is the "provisioning" state.                            *)
StartBoot(c) ==
  /\ client[c].phase = "idle"
  /\ IF ctr = "asleep"
       THEN /\ inc < MaxInc
            /\ inc' = inc + 1
            /\ ctr' = "provisioning"
       ELSE /\ inc' = inc
            /\ ctr' = IF ctr = "ready" THEN "ready" ELSE "provisioning"
  /\ client' = [client EXCEPT ![c].phase = "booting", ![c].bootInc = inc']

(* boot.sh printed its ok marker on the incarnation it started on: the     *)
(* container is now provisioned.  Marks Ready even if a second concurrent  *)
(* boot is still running (idempotency).                                    *)
FinishBoot(c) ==
  /\ client[c].phase = "booting"
  /\ Awake
  /\ client[c].bootInc = inc
  /\ ctr' = "ready"
  /\ client' = [client EXCEPT ![c].phase = "believes"]
  /\ UNCHANGED inc

(* The container slept (or slept and was re-woken by someone else) while   *)
(* this client's exec was in flight: the RPC fails, /api/boot returns 500, *)
(* the tab shows "boot failed" and the client is back to square one.       *)
BootLost(c) ==
  /\ client[c].phase = "booting"
  /\ (ctr = "asleep" \/ client[c].bootInc # inc)
  /\ client' = [client EXCEPT ![c].phase = "idle"]
  /\ UNCHANGED <<ctr, inc>>

(* WS /ws/terminal against a ready container: the normal, correct attach.  *)
AttachReady(c) ==
  /\ client[c].phase = "believes"
  /\ ctr = "ready"
  /\ client' = [client EXCEPT ![c].phase = "attached", ![c].attInc = inc]
  /\ UNCHANGED <<ctr, inc>>

(* Unguarded design only: attach reaches an asleep sandbox and the SDK     *)
(* implicitly wakes a FRESH container -- empty disk, no boot.sh -- and     *)
(* hands the client a terminal on it.  This is the bug transition.         *)
AttachWakesFresh(c) ==
  /\ ~GuardedAttach
  /\ client[c].phase = "believes"
  /\ ctr = "asleep"
  /\ inc < MaxInc
  /\ inc' = inc + 1
  /\ ctr' = "fresh"
  /\ client' = [client EXCEPT ![c].phase = "attached", ![c].attInc = inc']

(* Unguarded design only: attach to an awake but not-yet-ready container   *)
(* (fresh from an implicit wake, or mid-provisioning) also just connects.  *)
AttachAwakeNotReady(c) ==
  /\ ~GuardedAttach
  /\ client[c].phase = "believes"
  /\ ctr \in {"fresh", "provisioning"}
  /\ client' = [client EXCEPT ![c].phase = "attached", ![c].attInc = inc]
  /\ UNCHANGED <<ctr, inc>>

(* Guarded design only: an attach that would land on a non-ready container *)
(* is refused/detected and the client re-enters the boot flow instead.     *)
AttachGuarded(c) ==
  /\ GuardedAttach
  /\ client[c].phase = "believes"
  /\ ctr # "ready"
  /\ client' = [client EXCEPT ![c].phase = "idle"]
  /\ UNCHANGED <<ctr, inc>>

(* SandboxAddon auto-reconnect: the WS died (container slept, or a new     *)
(* incarnation replaced the one we were attached to), the addon retries -- *)
(* the client is back to merely believing the pod is ready.                *)
Reconnect(c) ==
  /\ client[c].phase = "attached"
  /\ (ctr = "asleep" \/ client[c].attInc # inc)
  /\ client' = [client EXCEPT ![c].phase = "believes"]
  /\ UNCHANGED <<ctr, inc>>

(* 30-minute idle timeout, or POST /api/destroy ("reset pod"): the         *)
(* container is gone and its disk with it.  Nondeterministic: can fire in  *)
(* any awake state, including mid-provisioning.                            *)
Sleep ==
  /\ Awake
  /\ ctr' = "asleep"
  /\ UNCHANGED <<inc, client>>

Next ==
  \/ Sleep
  \/ \E c \in Clients :
       \/ StartBoot(c) \/ FinishBoot(c) \/ BootLost(c)
       \/ AttachReady(c) \/ AttachWakesFresh(c) \/ AttachAwakeNotReady(c)
       \/ AttachGuarded(c) \/ Reconnect(c)

Spec == Init /\ [][Next]_vars

----------------------------------------------------------------------------
(* Invariants *)

(* A live terminal (attached, container awake, attachment on the current   *)
(* incarnation) exists only on a container that boot.sh provisioned, i.e.  *)
(* the shell the user is typing into really has tmux/bashrc/repo.          *)
(* Violated by the unguarded design (GuardedAttach = FALSE): see header.   *)
NoAttachWithoutShellSetup ==
  \A c \in Clients :
    (client[c].phase = "attached" /\ Awake /\ client[c].attInc = inc)
      => ctr = "ready"

(* Boot idempotency: once a client's boot has completed on the current     *)
(* incarnation and the container is still awake, the container is Ready -- *)
(* a second concurrent boot never demotes it to a non-Ready state.  Holds  *)
(* in both design variants.                                                *)
BootIdempotent ==
  \A c \in Clients :
    (client[c].phase \in {"believes", "attached"}
        /\ Awake /\ client[c].bootInc = inc)
      => ctr = "ready"

====