// A model of the agent loop as docs/Architecture.md describes it (PR #90):
// work items from assigned issues and conversations, restatements and
// go-aheads, park-and-switch, blocked dependencies, harness-owned milestones,
// waiting for merges, review follow-ups, and crashes at any point.
//
// Unlike orchestrator.qnt, this models a design, not code: the new loop
// doesn't exist yet, so a counterexample here is a gap in the architecture.
//
// Everything lives in one record, `s`. Durable state (the state store,
// Gitea, the build VM's disk) survives a crash; volatile state (work in
// flight) does not. Ghost fields record what the properties need to know
// and the agent never reads.
//
// Run:  quint run specs/loop.qnt --invariant=all_properties
module loop {

  // ---- bounds --------------------------------------------------------------

  pure val MAX_ITEMS = 3     // work items per run
  pure val MAX_REV = 3       // restatement revisions per item
  pure val MAX_MS = 2        // milestones per item
  pure val MAX_INBOX = 3     // operator messages not yet handled
  pure val PROJECTS = Set("A", "B")
  pure val ISSUES = Set(1, 2)          // issues the operator can file and assign
  pure val DEP_ISSUES = Set(101, 102)  // other issues an item can be blocked by

  // ---- state ---------------------------------------------------------------

  type Item = {
    status: str,       // ready / waiting / blocked / closed (active is s.active)
    src: str,          // issue / conv
    issue: int,        // its record issue, 0 if none yet
    project: str,
    bug: bool,
    waitFor: str,      // goahead / grace / answer / agree / merge, when waiting
    question: bool,    // a question to the operator is pending (L2)
    rev: int,          // latest restatement put up (L3)
    needRestate: bool, // an answer changed the understanding: restate again
    started: bool,     // scope agreed: a go-ahead, or a bug's grace period over (D1)
    ms: int,           // current milestone, 0 before the first
    attempt: int,      // a redo of a milestone whose PR was closed gets a new branch
    stage: str,        // none / working / pr
    review: bool,      // a review comment is waiting to be answered (D5)
    unpushed: bool,    // work on the build VM not yet pushed
    deps: Set[int],    // recorded dependencies (L1)
  }

  type Issue = { open: bool, assigned: bool, linked: int }
  type Msg = { item: int, kind: str, saw: int }

  type Sys = {
    // -- durable: the state store --
    items: int -> Item,
    nextItem: int,
    active: int,              // 0: none (L1)
    intents: Set[int],        // pending publish intents, by PR key (L8)
    // -- durable: Gitea --
    issues: int -> Issue,
    depOpen: int -> bool,
    prs: int -> str,          // PR key -> open / merged / closed
    opened: int -> int,       // PR key -> PRs ever opened for it
    // -- durable: Matrix holds messages until the agent handles them --
    inbox: List[Msg],
    // -- volatile --
    work: str,                // none / publish
    pubStage: int,
    pending: int,             // a record issue created but not yet linked
    // -- ghosts --
    badGo: bool,              // work started on a revision the operator never saw
    earlyMs: bool,            // a milestone started before the previous merged
    lostFix: bool,            // a review fix pushed to a PR no longer open
    lostWork: bool,           // a parked item's unpushed work was set aside or wiped
  }

  var s: Sys

  pure def prKey(i: int, ms: int, a: int): int = i * 100 + ms * 10 + a
  pure def keyOf(t: Sys, i: int): int = prKey(i, t.items.get(i).ms, t.items.get(i).attempt)
  pure def prOf(t: Sys, i: int): str = {
    val k = keyOf(t, i)
    if (t.prs.keys().contains(k)) t.prs.get(k) else ""
  }
  pure def upd(t: Sys, i: int, it: Item): Sys = { ...t, items: t.items.set(i, it) }
  pure def itm(t: Sys, i: int): Item = t.items.get(i)
  pure def live(t: Sys): Set[int] = t.items.keys().filter(i => t.items.get(i).status != "closed")

  pure def newItem(src: str, issue: int, project: str, bug: bool): Item = {
    status: "ready", src: src, issue: issue, project: project, bug: bug,
    waitFor: "", question: false, rev: 0, needRestate: false, started: false,
    ms: 0, attempt: 0, stage: "none", review: false, unpushed: false, deps: Set(),
  }

  pure def wait(it: Item, why: str, q: bool): Item =
    { ...it, status: "waiting", waitFor: why, question: q }
  pure def ready(it: Item): Item = { ...it, status: "ready", waitFor: "", question: false }

  action init = s' = {
    items: Map(), nextItem: 1, active: 0, intents: Set(),
    issues: ISSUES.mapBy(_ => { open: false, assigned: false, linked: 0 }),
    depOpen: DEP_ISSUES.mapBy(_ => true),
    prs: Map(), opened: Map(), inbox: List(),
    work: "none", pubStage: 0, pending: 0,
    badGo: false, earlyMs: false, lostFix: false, lostWork: false,
  }

  // ---- the operator ----------------------------------------------------------

  // Files an issue and assigns it to the agent (D1).
  // (Its project and `bug` label are chosen at intake.)
  action assignIssue(n: int): bool = all {
    not(s.issues.get(n).open), s.issues.get(n).linked == 0,
    s' = { ...s, issues: s.issues.set(n, { open: true, assigned: true, linked: 0 }) },
  }

  // Starts a conversation: a work item from its first message (L5).
  action converse(p: str): bool = all {
    s.nextItem <= MAX_ITEMS,
    s' = { ...s, items: s.items.put(s.nextItem, newItem("conv", 0, p, false)),
           nextItem: s.nextItem + 1 },
  }

  // Replies in an item's thread. `saw` is the revision on screen when sent.
  action say(i: int, kind: str): bool = all {
    live(s).contains(i), s.inbox.length() < MAX_INBOX,
    s' = { ...s, inbox: s.inbox.append({ item: i, kind: kind, saw: itm(s, i).rev }) },
  }

  // Merges, closes or comments on an item's open PR (D4, D5).
  action prAct(i: int, what: str): bool = {
    val k = keyOf(s, i)
    all {
      s.items.keys().contains(i), prOf(s, i) == "open",
      s' = if (what == "comment") upd(s, i, { ...itm(s, i), review: true })
           else { ...s, prs: s.prs.set(k, what) },
    }
  }

  // Closes an issue another item depends on.
  action closeDep(d: int): bool = all {
    s.depOpen.get(d), s' = { ...s, depOpen: s.depOpen.set(d, false) },
  }

  // ---- intake and the duty ---------------------------------------------------

  // The duty picks up an assigned, open issue that no item is linked to (D1).
  action intake(n: int, p: str, bug: bool): bool = {
    val known = s.issues.keys().contains(n)
    val is = s.issues.get(n)
    all {
      known, is.open, is.assigned, is.linked == 0, s.nextItem <= MAX_ITEMS,
      s' = { ...s, items: s.items.put(s.nextItem, newItem("issue", n, p, bug)),
             issues: s.issues.set(n, { ...is, linked: s.nextItem }),
             nextItem: s.nextItem + 1 },
    }
  }

  // The duty notices external truth: a merged or closed PR, a dependency
  // closed. (L1 blocked, D4 wait for the merge.)
  action observe(i: int): bool = {
    val it = itm(s, i)
    all {
      live(s).contains(i),
      any {
        all { it.status == "blocked", it.deps.forall(d => not(s.depOpen.get(d))),
              s' = upd(s, i, ready({ ...it, deps: Set() })) },
        all { it.stage == "pr", prOf(s, i) == "merged", not(it.review),
              s' = upd(s, i, ready({ ...it, stage: "none" })) },
        // D4: ready with that fact; the agent asks what next.
        // FIX 4 (D4): a redo is the same milestone on a new branch and PR.
        all { it.stage == "pr", prOf(s, i) == "closed",
              s' = upd(s, i, wait({ ...it, stage: "none", ms: it.ms - 1,
                                         attempt: it.attempt + 1 }, "answer", true)) },
        all { it.stage == "pr", it.review, it.status == "waiting",
              s' = upd(s, i, ready(it)) },
      },
    }
  }

  // ---- handling messages (conversation is not work, L1) ----------------------

  pure def handle(t: Sys, m: Msg): Sys = {
    val it = itm(t, m.item)
    if (it.status == "closed") t
    else if (m.kind == "go")
      // L3: bound to the revision up when the reply arrived.
      if (it.status == "waiting" and it.waitFor == "goahead" and m.saw == it.rev)
        { ...upd(t, m.item, ready({ ...it, started: true })), badGo: t.badGo or m.saw != it.rev }
      else t
    else if (m.kind == "answer")
      if (it.question and (it.waitFor == "answer"))
        upd(t, m.item, ready({ ...it, needRestate: not(it.started) }))
      else t
    else if (m.kind == "agree")
      // D1/L1: the operator agrees a blocker should be recorded.
      if (it.waitFor == "agree") upd(t, m.item, { ...it, status: "blocked", waitFor: "",
                                                  question: false, deps: Set(101) })
      else t
    else if (m.kind == "decline")
      if (it.waitFor == "agree") upd(t, m.item, ready(it)) else t
    else if (m.kind == "abandon")
      // L2: from any waiting point; closes the record, aborts its intents.
      if (t.active == m.item and t.work != "none") t
      else {
        val closed = upd(t, m.item, { ...it, status: "closed", question: false })
        val withIssue = if (it.issue != 0)
            { ...closed, issues: closed.issues.set(it.issue,
                { ...closed.issues.get(it.issue), open: false }) }
          else closed
        val noIntents = { ...withIssue, intents: withIssue.intents.filter(k => k / 100 != m.item) }
        // FIX 1 (L2): abandoning closes the item's open PR with a note.
        { ...noIntents, prs: noIntents.prs.keys().mapBy(k =>
            if (k / 100 == m.item and noIntents.prs.get(k) == "open") "closed"
            else noIntents.prs.get(k)) }
      }
    else t
  }

  action handleMsg: bool = all {
    s.inbox.length() > 0, s.work == "none",
    s' = { ...handle(s, s.inbox.head()), inbox: s.inbox.tail() },
  }

  // ---- the agent ---------------------------------------------------------------

  // Switching: the active item is at a safe point; parking pushes its branch (D4).
  action park: bool = {
    val it = itm(s, s.active)
    all {
      s.active != 0, s.work == "none", s.intents.size() == 0,
      Set("waiting", "blocked", "closed").contains(it.status),
      s' = { ...upd(s, s.active, { ...it, unpushed: false }), active: 0 },
    }
  }

  // Taking up a ready item: a fresh workspace on its project's build VM (D3)
  // sets aside whatever is left there.
  action activate(i: int): bool = all {
    s.active == 0, s.work == "none", live(s).contains(i), itm(s, i).status == "ready",
    s' = {
      val leftovers = s.items.keys().exists(j => j != i and itm(s, j).project == itm(s, i).project
                                                  and itm(s, j).unpushed)
      { ...s, active: i, lostWork: s.lostWork or leftovers }
    },
  }

  // Restating (D1): bug → grace period; otherwise wait for a go-ahead; or ask.
  action restate(ask: bool): bool = {
    val i = s.active
    val it = itm(s, i)
    all {
      i != 0, s.work == "none", it.status == "ready", not(it.started),
      it.rev < MAX_REV,
      s' = upd(s, i,
        if (ask) wait({ ...it, rev: it.rev + 1, needRestate: false }, "answer", true)
        else if (it.bug) wait({ ...it, rev: it.rev + 1, needRestate: false }, "grace", false)
        else wait({ ...it, rev: it.rev + 1, needRestate: false }, "goahead", false)),
    }
  }

  // A bug's grace period runs out: the item is ready to work (D1).
  action graceOver(i: int): bool = all {
    live(s).contains(i), itm(s, i).waitFor == "grace",
    s' = upd(s, i, ready({ ...itm(s, i), started: true })),
  }

  // Work on a repository needs a record issue (D1). Opening one is an
  // external effect, then the link is written: two steps.
  action createRecord: bool = {
    val it = itm(s, s.active)
    val n = 100 - s.active   // the record's issue number
    all {
      s.active != 0, s.work == "none", it.status == "ready", it.started, it.issue == 0,
      s.pending == 0,
      // FIX 5 (D1): the issue carries its work item's ID from creation, so
      // intake never takes it for new work, even before the link is stored.
      s' = { ...s, pending: s.active,
             issues: s.issues.put(n, { open: true, assigned: true, linked: s.active }) },
    }
  }

  action linkRecord: bool = {
    val n = 100 - s.pending
    all {
      s.pending != 0,
      s' = { ...upd(s, s.pending, { ...itm(s, s.pending), issue: n }),
             issues: s.issues.set(n, { ...s.issues.get(n), linked: s.pending }),
             pending: 0 },
    }
  }

  // start_milestone (D4): only after the previous milestone's PR merged.
  action startMilestone: bool = {
    val i = s.active
    val it = itm(s, i)
    all {
      i != 0, s.work == "none", it.status == "ready", it.started, it.issue != 0,
      it.stage == "none", it.ms < MAX_MS,
      s' = {
        val early = it.ms > 0 and prOf(s, i) != "merged"
        { ...upd(s, i, { ...it, ms: it.ms + 1, stage: "working", unpushed: true }),
          earlyMs: s.earlyMs or early }
      },
    }
  }

  // A turn of work: progress, a blocker to propose, or a question.
  action turn(outcome: str): bool = {
    val i = s.active
    val it = itm(s, i)
    all {
      i != 0, s.work == "none", it.status == "ready", it.stage == "working",
      s' = upd(s, i,
        if (outcome == "progress") { ...it, unpushed: true }
        else if (outcome == "blocker") wait(it, "agree", true)
        else wait(it, "answer", true)),
    }
  }

  // finish_milestone (D4): commit, push, open the PR, under an intent (L8).
  action finishMilestone: bool = {
    val it = itm(s, s.active)
    all {
      s.active != 0, s.work == "none", it.status == "ready", it.stage == "working",
      s' = { ...s, work: "publish", pubStage: 0 },
    }
  }

  action publishStep(lost: bool): bool = {
    val i = s.active
    val it = itm(s, i)
    val k = keyOf(s, i)
    all {
      s.work == "publish",
      s' =
        if (s.pubStage == 0) { ...s, intents: s.intents.union(Set(k)), pubStage: 1 }
        else if (s.pubStage == 1) {
          val pushed = upd(s, i, { ...it, unpushed: false })
          if (s.prs.keys().contains(k) and s.prs.get(k) == "open") { ...pushed, pubStage: 2 }
          // FIX 2 (D4, L8): the branch's PR was closed: report it, never open another.
          else if (s.prs.keys().contains(k) and s.prs.get(k) != "open")
            { ...upd(pushed, i, wait({ ...itm(pushed, i), stage: "pr" }, "answer", true)),
              intents: pushed.intents.exclude(Set(k)), work: "none", pubStage: 0 }
          else {
            val n = if (s.opened.keys().contains(k)) s.opened.get(k) else 0
            val withPr = { ...pushed, prs: pushed.prs.put(k, "open"),
                           opened: pushed.opened.put(k, n + 1) }
            // A lost response: Gitea opened it, the agent never heard.
            if (lost) { ...withPr, work: "none", pubStage: 0 } else { ...withPr, pubStage: 2 }
          }
        }
        else { ...upd(s, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false)),
               intents: s.intents.exclude(Set(k)), work: "none", pubStage: 0 },
    }
  }

  // Answering a review comment: commits pushed to the PR's branch (D5).
  action answerReview: bool = {
    val i = s.active
    val it = itm(s, i)
    all {
      i != 0, s.work == "none", it.status == "ready", it.stage == "pr", it.review,
      s' =
        if (prOf(s, i) == "open")
          upd(s, i, wait({ ...it, review: false, unpushed: false }, "merge", false))
        // FIX 3 (D5): the PR merged first: the fix goes out as a new PR.
        else if (prOf(s, i) == "merged")
          upd(s, i, { ...it, review: false, stage: "working", attempt: it.attempt + 1,
                      unpushed: true })
        // ...or it was closed: say so and ask.
        else upd(s, i, wait({ ...it, review: false, stage: "none" }, "answer", true)),
    }
  }

  // Finishing: the last PR merged, the agent closes the item (D1).
  action finish: bool = {
    val i = s.active
    val it = itm(s, i)
    all {
      i != 0, s.work == "none", it.status == "ready", it.ms > 0, it.stage == "none",
      prOf(s, i) == "merged",
      s' = upd(s, i, { ...it, status: "closed" }),
    }
  }

  // The build VM is wiped (D3): unpushed work on it is lost, accepted for
  // the active item, never for a parked one.
  action wipe(p: str): bool = all {
    s' = { ...s,
      items: s.items.keys().mapBy(j =>
        if (itm(s, j).project == p) { ...itm(s, j), unpushed: false } else itm(s, j)),
      lostWork: s.lostWork or s.items.keys().exists(j =>
        j != s.active and itm(s, j).project == p and itm(s, j).unpushed) },
  }

  // ---- crash and boot (L8) --------------------------------------------------

  // Volatile state is lost; boot reconciles each pending intent against
  // Gitea: an open PR is adopted, otherwise the intent is aborted and the
  // operator is told (L8 step 5).
  pure def reconcile(t: Sys, k: int): Sys = {
    val i = k / 100
    val it = itm(t, i)
    val t2 = { ...t, intents: t.intents.exclude(Set(k)) }
    if (t.prs.keys().contains(k) and t.prs.get(k) == "open")
      upd(t2, i, wait({ ...it, stage: "pr", unpushed: false }, "merge", false))
    else upd(t2, i, wait(it, "answer", true))
  }

  action crash: bool =
    s' = s.intents.fold({ ...s, work: "none", pubStage: 0, pending: 0 },
                        (t, k) => reconcile(t, k))

  // ---- step ---------------------------------------------------------------------

  action step = {
    nondet n = ISSUES.oneOf()
    nondet anyIssue = s.issues.keys().oneOf()
    nondet i = 1.to(MAX_ITEMS).oneOf()
    nondet p = PROJECTS.oneOf()
    nondet b = Set(true, false).oneOf()
    nondet kind = Set("go", "answer", "agree", "decline", "abandon").oneOf()
    nondet what = Set("merged", "closed", "comment").oneOf()
    nondet outcome = Set("progress", "blocker", "question").oneOf()
    nondet d = DEP_ISSUES.oneOf()
    any {
      assignIssue(n), converse(p), say(i, kind), prAct(i, what), closeDep(d),
      intake(anyIssue, p, b), observe(i), handleMsg,
      park, activate(i), restate(b), graceOver(i), createRecord, linkRecord,
      startMilestone, turn(outcome), finishMilestone, publishStep(b), answerReview,
      finish, wipe(p), crash,
    }
  }

  // ---- properties ---------------------------------------------------------------

  // An issue is the record of at most one work item (D1 intake).
  val one_item_per_issue = s.items.keys().forall(a => s.items.keys().forall(b =>
    (a != b and itm(s, a).issue != 0) implies itm(s, a).issue != itm(s, b).issue))

  // Every wait is for something the operator can see or a dependency (L2).
  val waits_are_explainable = live(s).forall(i => {
    val it = itm(s, i)
    and {
      it.status == "waiting" implies or {
        it.waitFor == "goahead" and it.rev > 0,
        it.waitFor == "grace",
        Set("answer", "agree").contains(it.waitFor) and it.question,
        it.waitFor == "merge" and prOf(s, i) != "",
      },
      it.status == "blocked" implies it.deps.size() > 0,
    }
  })

  // Work starts only on a go-ahead for the revision the operator saw (L3).
  val go_binds = not(s.badGo)

  // The next milestone starts only after the previous PR merged (D4).
  val milestone_after_merge = not(s.earlyMs)

  // A parked item's work is never set aside or wiped (D4 parking).
  val parked_work_safe = not(s.lostWork)

  // Never more than one PR opened for a milestone (L8).
  val one_pr_per_milestone = s.opened.keys().forall(k => s.opened.get(k) <= 1)

  // A review fix always lands on an open PR (D5).
  val review_fixes_land = not(s.lostFix)

  // A closed item leaves no open PR and no pending intent behind (L2).
  val closed_items_leave_nothing = s.items.keys().forall(i =>
    itm(s, i).status == "closed" implies and {
      s.prs.keys().forall(k => k / 100 == i implies s.prs.get(k) != "open"),
      s.intents.forall(k => k / 100 != i),
    })

  val all_properties = and {
    one_item_per_issue, waits_are_explainable, go_binds, milestone_after_merge,
    parked_work_safe, one_pr_per_milestone, review_fixes_land, closed_items_leave_nothing,
  }

  // ---- reachability witnesses (each should be violated) --------------------------
  val w_pr_opened = s.opened.keys().size() == 0
  val w_merged = not(s.prs.keys().exists(k => s.prs.get(k) == "merged"))
  val w_second_ms = not(s.items.keys().exists(i => itm(s, i).ms == 2))
  val w_blocked = not(s.items.keys().exists(i => itm(s, i).status == "blocked"))
  val w_review = not(s.items.keys().exists(i => itm(s, i).review))
  val w_record = not(s.items.keys().exists(i => itm(s, i).src == "conv" and itm(s, i).issue != 0))
  val w_finished = not(s.items.keys().exists(i => itm(s, i).status == "closed" and itm(s, i).ms > 0))
}