---- MODULE MirroredImage ----
EXTENDS Naturals, FiniteSets, TLC

CONSTANTS Tagged, Safe, AllowRemoval, AllowFailure, AllowRetry, RetryStageSet, MaxEpoch, MaxRetries

Stages == {"prepare", "promotion", "cleanup"}
Repos == {"candidate", "mirror"}
Children == {"amd64", "arm64"}
Phases == {"absent", "pending", "queued", "running", "published", "succeeded", "failed"}
Terminal(p) == p \in {"succeeded", "failed"}

VARIABLES desired, managed, retired, attempts, workflows, scanned, verdict,
          stored, temporary, durableTags, promoted, copies, retryCount, retryAck,
          cleanupObserved, grace, epoch, retryStage, badPromotion

vars == <<desired, managed, retired, attempts, workflows, scanned, verdict,
          stored, temporary, durableTags, promoted, copies, retryCount, retryAck,
          cleanupObserved, grace, epoch, retryStage, badPromotion>>

Available(r) == stored[r] /\ (temporary[r] \/ durableTags[r] # {})
Active == \E s \in Stages : attempts[s] # "absent" /\ ~Terminal(attempts[s])

Init ==
    /\ desired = TRUE
    /\ managed = FALSE
    /\ retired = FALSE
    /\ attempts = [s \in Stages |-> "absent"]
    /\ workflows = [s \in Stages |-> "absent"]
    /\ scanned = {}
    /\ verdict = "pending"
    /\ stored = [r \in Repos |-> FALSE]
    /\ temporary = [r \in Repos |-> FALSE]
    /\ durableTags = [r \in Repos |-> {}]
    /\ promoted = FALSE
    /\ copies = 0
    /\ retryCount = 0
    /\ retryAck = FALSE
    /\ cleanupObserved = FALSE
    /\ grace = [r \in Repos |-> FALSE]
    /\ epoch = 1
    /\ retryStage = "none" /\ badPromotion = FALSE

Manage ==
    /\ desired /\ ~managed /\ ~retired
    /\ managed' = TRUE
    /\ UNCHANGED <<desired, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Plan(s) ==
    /\ managed /\ ~Active /\ attempts[s] = "absent"
    /\ CASE s = "prepare" -> desired /\ attempts["cleanup"] = "absent"
         [] s = "promotion" -> desired /\ attempts["cleanup"] = "absent"
                              /\ attempts["prepare"] = "succeeded" /\ verdict = "accepted"
         [] s = "cleanup" -> ~desired
    /\ attempts' = [attempts EXCEPT ![s] = "pending"]
    /\ UNCHANGED <<desired, managed, retired, workflows, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Submit(s) ==
    /\ attempts[s] = "pending" /\ workflows[s] = "absent"
    /\ s = "cleanup" => \A t \in {"prepare", "promotion"} : attempts[t] = "absent" \/ Terminal(attempts[t])
    /\ workflows' = [workflows EXCEPT ![s] = "queued"]
    /\ retryAck' = (retryAck \/ (retryCount > 0 /\ s = retryStage))
    /\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   cleanupObserved, grace, epoch, retryStage, badPromotion>>

Start(s) ==
    /\ workflows[s] = "queued"
    /\ ~\E t \in Stages : workflows[t] \in {"running", "published"}
    /\ workflows' = [workflows EXCEPT ![s] = "running"]
    /\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

PartialCopy(s) ==
    /\ s \in {"prepare", "promotion"} /\ workflows[s] = "running"
    /\ s = "promotion" => Available("candidate")
    /\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
       IN /\ ~stored[r]
          /\ stored' = [stored EXCEPT ![r] = TRUE]
          /\ temporary' = [temporary EXCEPT ![r] = TRUE]
          /\ grace' = [grace EXCEPT ![r] = FALSE]
    /\ badPromotion' = (badPromotion \/ (s = "promotion" /\ (~Safe \/ verdict # "accepted" \/ scanned # Children)))
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   durableTags, promoted, copies, retryCount, retryAck,
                   cleanupObserved, epoch, retryStage>>

Publish(s) ==
    /\ s \in {"prepare", "promotion"} /\ workflows[s] = "running"
    /\ s = "promotion" => Available("candidate")
    /\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
       IN /\ stored' = [stored EXCEPT ![r] = TRUE]
          /\ temporary' = [temporary EXCEPT ![r] = TRUE]
          /\ durableTags' = [durableTags EXCEPT ![r] = @ \cup {"retention"}]
          /\ grace' = [grace EXCEPT ![r] = FALSE]
    /\ promoted' = (promoted \/ (s = "promotion" /\ attempts["cleanup"] = "absent"))
    /\ copies' = IF s = "promotion" THEN copies + 1 ELSE copies
    /\ badPromotion' = (badPromotion \/ (s = "promotion" /\ (~Safe \/ verdict # "accepted" \/ scanned # Children)))
    /\ workflows' = [workflows EXCEPT ![s] = "published"]
    /\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
                   retryCount, retryAck, cleanupObserved, epoch, retryStage>>

Alias(s) ==
    /\ Tagged /\ s \in {"prepare", "promotion"} /\ workflows[s] = "published"
    /\ LET r == IF s = "prepare" THEN "candidate" ELSE "mirror"
       IN /\ "declared" \notin durableTags[r]
          /\ durableTags' = [durableTags EXCEPT ![r] = @ \cup {"declared"}]
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, promoted, copies, retryCount, retryAck,
                   cleanupObserved, grace, epoch, retryStage, badPromotion>>

Delete(r) ==
    /\ workflows["cleanup"] = "running"
    /\ durableTags[r] # {}
    /\ durableTags' = [durableTags EXCEPT ![r] = {}]
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, promoted, copies, retryCount, retryAck,
                   cleanupObserved, grace, epoch, retryStage, badPromotion>>

Finish(s, success) ==
    /\ workflows[s] \in {"running", "published"}
    /\ success \/ AllowFailure \/ (s = "promotion" /\ ~Available("candidate"))
    /\ success => IF s = "cleanup" THEN \A r \in Repos : durableTags[r] = {}
                  ELSE /\ workflows[s] = "published"
                       /\ Tagged => "declared" \in durableTags[IF s = "prepare" THEN "candidate" ELSE "mirror"]
    /\ workflows' = [workflows EXCEPT ![s] = IF success THEN "succeeded" ELSE "failed"]
    /\ UNCHANGED <<desired, managed, retired, attempts, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Observe(s) ==
    /\ attempts[s] = "pending" /\ Terminal(workflows[s])
    /\ attempts' = [attempts EXCEPT ![s] = workflows[s]]
    /\ UNCHANGED <<desired, managed, retired, workflows, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Scan(c) ==
    /\ desired /\ attempts["prepare"] = "succeeded"
    /\ attempts["cleanup"] = "absent" /\ verdict = "pending"
    /\ Available("candidate") /\ c \notin scanned
    /\ scanned' = scanned \cup {c}
    /\ verdict' = IF ~Safe /\ c = "arm64" THEN "rejected"
                   ELSE IF scanned' = Children THEN "accepted" ELSE "pending"
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Expire(r) ==
    /\ temporary[r]
    /\ temporary' = [temporary EXCEPT ![r] = FALSE]
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   stored, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Age(r) ==
    /\ stored[r] /\ ~Available(r) /\ ~grace[r]
    /\ grace' = [grace EXCEPT ![r] = TRUE]
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, epoch, retryStage, badPromotion>>

Collect(r) ==
    /\ stored[r] /\ ~Available(r) /\ grace[r]
    /\ stored' = [stored EXCEPT ![r] = FALSE]
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Remove ==
    /\ AllowRemoval /\ desired
    /\ desired' = FALSE
    /\ UNCHANGED <<managed, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, durableTags, promoted, copies, retryCount,
                   retryAck, cleanupObserved, grace, epoch, retryStage, badPromotion>>

Forget ==
    /\ managed /\ ~Active /\ attempts["cleanup"] = "succeeded"
    /\ \A r \in Repos : ~stored[r]
    /\ managed' = desired
    /\ retired' = ~desired
    /\ cleanupObserved' = ~desired
    /\ attempts' = IF desired THEN [s \in Stages |-> "absent"] ELSE attempts
    /\ workflows' = IF desired THEN [s \in Stages |-> "absent"] ELSE workflows
    /\ scanned' = IF desired THEN {} ELSE scanned
    /\ verdict' = IF desired THEN "pending" ELSE verdict
    /\ promoted' = IF desired THEN FALSE ELSE promoted
    /\ retryAck' = IF desired THEN FALSE ELSE retryAck
    /\ UNCHANGED <<desired, stored, temporary, durableTags, copies, retryCount, grace, epoch, retryStage, badPromotion>>

Readd ==
    /\ ~desired /\ epoch < MaxEpoch
    /\ desired' = TRUE /\ epoch' = epoch + 1
    /\ retired' = FALSE /\ promoted' = FALSE /\ cleanupObserved' = FALSE
    /\ attempts' = IF managed THEN attempts ELSE [s \in Stages |-> "absent"]
    /\ workflows' = IF managed THEN workflows ELSE [s \in Stages |-> "absent"]
    /\ scanned' = IF managed THEN scanned ELSE {}
    /\ verdict' = IF managed THEN verdict ELSE "pending"
    /\ retryAck' = IF managed THEN retryAck ELSE FALSE
    /\ UNCHANGED <<managed, stored, temporary, durableTags, copies, retryCount, grace, retryStage, badPromotion>>

ObservePromoted ==
    /\ desired /\ ~promoted /\ attempts["promotion"] = "succeeded"
    /\ attempts["cleanup"] = "absent" /\ Available("mirror")
    /\ promoted' = TRUE
    /\ UNCHANGED <<desired, managed, retired, attempts, workflows, scanned, verdict,
                   stored, temporary, durableTags, copies, retryCount, retryAck,
                   cleanupObserved, grace, epoch, retryStage, badPromotion>>

Retry(s) ==
    /\ AllowRetry /\ retryCount < MaxRetries /\ managed /\ ~Active
    /\ Terminal(attempts[s])
    /\ attempts' = [t \in Stages |->
        IF t = s THEN "pending"
        ELSE IF s = "prepare" /\ t = "promotion" THEN "absent"
        ELSE IF t = "cleanup" /\ attempts[t] # "absent" THEN "pending"
        ELSE attempts[t]]
    /\ workflows' = [t \in Stages |->
        IF t = s \/ (s = "prepare" /\ t = "promotion") \/ t = "cleanup"
        THEN "absent" ELSE workflows[t]]
    /\ scanned' = IF s = "prepare" THEN {} ELSE scanned
    /\ verdict' = IF s = "prepare" THEN "pending" ELSE verdict
    /\ retryCount' = retryCount + 1
    /\ retryStage' = s
    /\ retryAck' = FALSE
    /\ UNCHANGED <<desired, managed, retired,
                   stored, temporary, durableTags, promoted, copies,
                   cleanupObserved, grace, epoch, badPromotion>>

Next ==
    \/ Manage
    \/ \E s \in Stages : Plan(s) \/ Submit(s) \/ Start(s) \/ Observe(s)
                         \/ \E success \in BOOLEAN : Finish(s, success)
    \/ \E s \in {"prepare", "promotion"} : PartialCopy(s) \/ Publish(s) \/ Alias(s)
    \/ \E r \in Repos : Delete(r) \/ Expire(r) \/ Age(r) \/ Collect(r)
    \/ \E c \in Children : Scan(c)
    \/ Remove \/ Forget \/ (\E s \in RetryStageSet : Retry(s)) \/ Readd \/ ObservePromoted

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

FairSpec == Spec
    /\ WF_vars(Manage) /\ WF_vars(Forget) /\ WF_vars(ObservePromoted)
    /\ (\A s \in Stages : WF_vars(Plan(s)) /\ WF_vars(Submit(s))
                          /\ WF_vars(Start(s)) /\ WF_vars(Observe(s))
                          /\ WF_vars(Finish(s, TRUE) \/ Finish(s, FALSE)))
    /\ (\A s \in {"prepare", "promotion"} : WF_vars(Publish(s)) /\ WF_vars(Alias(s)))
    /\ (\A r \in Repos : WF_vars(Delete(r)) /\ WF_vars(Expire(r))
                         /\ WF_vars(Age(r)) /\ WF_vars(Collect(r)))
    /\ (\A c \in Children : WF_vars(Scan(c)))

TypeOK ==
    /\ desired \in BOOLEAN /\ managed \in BOOLEAN /\ retired \in BOOLEAN
    /\ attempts \in [Stages -> Phases] /\ workflows \in [Stages -> Phases]
    /\ scanned \subseteq Children /\ verdict \in {"pending", "accepted", "rejected"}
    /\ stored \in [Repos -> BOOLEAN] /\ temporary \in [Repos -> BOOLEAN]
    /\ durableTags \in [Repos -> SUBSET {"retention", "declared", "retry"}]
    /\ promoted \in BOOLEAN /\ copies \in Nat /\ epoch \in 1..MaxEpoch
    /\ retryCount \in 0..MaxRetries /\ retryAck \in BOOLEAN
    /\ retryStage \in Stages \cup {"none"} /\ badPromotion \in BOOLEAN
    /\ cleanupObserved \in BOOLEAN /\ grace \in [Repos -> BOOLEAN]

PromotionRequiresAcceptance == ~badPromotion
DeclaredPromotionRetained == desired /\ promoted => Available("mirror")
DeclaredCandidateRetained == desired /\ attempts["cleanup"] = "absent" /\ attempts["prepare"] = "succeeded" => Available("candidate")
CleanupObservedMeansGone == cleanupObserved => \A r \in Repos : ~stored[r]
DeclaredAliasOnlyWhenRequested == ~Tagged => \A r \in Repos : "declared" \notin durableTags[r]
RetryPreservesTagIdentity == \A r \in Repos : durableTags[r] \subseteq {"retention", "declared"}
RetryAcknowledgedAfterCreation == retryAck => retryStage # "none" /\ workflows[retryStage] # "absent"
CleanupExcludesCopy == workflows["cleanup"] \in {"running", "published"} =>
    \A s \in {"prepare", "promotion"} : workflows[s] \notin {"running", "published"}

EventuallyPromoted == (desired /\ managed) ~> (~desired \/ promoted)
EventuallyRetired == (~desired /\ managed) ~> (retired \/ desired)
EventuallyRejected == <>(verdict = "rejected")

====