feat: close stage 10 with ProviderRetry and opossum's breaker

ROADMAP.md

@@ -133,8 +133,8 @@ Taken on 2026-11-07:
 | 7. Intents and the review view | `intent` declarations; the human view (intent, specification, examples, counterexamples, open cases, surviving mutants, what wasn't proved); the agent view as structured diagnostics | The review of `gate-rule` and an outside-domain rule is readable without their code | Built, check moved to the public phase ([#46](https://github.com/sequelcore/accord/issues/46)): the [gate and Cedar packets](docs/design/stage-7-review/README.md) await a reader from outside the project |
 | 8. TypeScript output | Accord compiled to a TypeScript module | Tesota's own tests pass with the generated rule in place of the original | Done ([#47](https://github.com/sequelcore/accord/issues/47)): `accord build` ([reference](docs/typescript.md)), checked against the interpreter; Tesota's typecheck and tests pass with the generated rules (`scripts/check-tesota.sh`), and axios-retry's lint and specs with its generated request predicates (`scripts/check-axios-retry.sh`) |
 | 9. Whole rules | Calls between functions, proved through the callee's contract; `all`, `any` and `count` over lists; length and indexing: what `verdict-rule`, the largest rule, and Cedar's policy-set evaluation need | `verdict-rule` and Cedar's policy-set evaluation ported and proved | Done ([#69](https://github.com/sequelcore/accord/issues/69)): `verdict-rule` in `conformance/programs/tesota/`, where Tesota's typecheck and tests pass with it generated (`scripts/check-tesota.sh`), and Cedar's policy-set evaluation in `conformance/programs/cedar/`, each with planted faults refuted; calls (`conformance/cases/call*.accord`) and lists (`list-*.accord`); [proof cost and undecided rate](docs/design/measurements/2026-11-12-stage-9-proof-cost/README.md) |
-| 10. State machines | `machine` declarations, invariants, explicit-state model checking, planted faults | A Tesota design model ported, its faults detected; the circuit breaker of [opossum](https://github.com/nodeshift/opossum) (Apache-2.0), closed, open and half-open, proved, and opossum's tests pass with the generated module | Next ([#82](https://github.com/sequelcore/accord/issues/82)) |
-| 11. Structured data | Records, sum types and `match`, recursion with `decreases`, `Text` operations beyond equality | Version comparison from [node-semver](https://github.com/npm/node-semver) (ISC) proved, and node-semver's tests for it pass with the generated module | |
+| 10. State machines | `machine` declarations, invariants, explicit-state model checking, planted faults | A Tesota design model ported, its faults detected; the circuit breaker of [opossum](https://github.com/nodeshift/opossum) (Apache-2.0), closed, open and half-open, proved, and opossum's tests pass with the generated module | Done ([#82](https://github.com/sequelcore/accord/issues/82)): machines checked by the solvers and an explorer, and written as TypeScript ([syntax](docs/design/syntax.md#machines), [TypeScript](docs/typescript.md)); Tesota's ProviderRetry model in `conformance/cases/provider-retry.accord`, its two faults refuted and its 148 states matching tla-ts ([measurement](docs/design/measurements/2026-11-12-stage-10-machines/README.md)); opossum's breaker in `conformance/programs/opossum/`, proved, with opossum's lint and tests passing with the generated module (`scripts/check-opossum.sh`) |
+| 11. Structured data | Records, sum types and `match`, recursion with `decreases`, `Text` operations beyond equality | Version comparison from [node-semver](https://github.com/npm/node-semver) (ISC) proved, and node-semver's tests for it pass with the generated module || Next ([#83](https://github.com/sequelcore/accord/issues/83)) |
 | 12. Complete programs | Effects (files, standard input and output, exit codes) declared in types, errors as values, a `main` | `wc` from [uutils/coreutils](https://github.com/uutils/coreutils) (MIT) written only in Accord, its effects in its types and its proofs still fail-closed; uutils' tests for `wc` pass against it | |
 | 13. Standard library and modules | Maps and sets, generic types, imports between packages, as stages 11 and 12's programs need them | Accord's own E2 tooling (`docs/design/e2-human-review/materials.py` and `score.py`) rewritten in Accord; their self-tests and CI check pass | |
 | 14. Native code | A native backend (LLVM), and validation of its output before it relies on a proof | Stage 12's `wc` compiled natively; uutils' tests pass, and a published measurement against uutils' Rust `wc`, with the same algorithm and each side's safety checks stated | |

conformance/README.md

@@ -84,6 +84,32 @@ Node 20, so CI doesn't run it. The port is licensed under Apache-2.0;
 attribution is in [`programs/axios-retry/NOTICE`](programs/axios-retry/NOTICE)
 and the source header.
 
+## opossum circuit breaker
+
+[`programs/opossum/`](programs/opossum) ports the state and decisions of
+opossum's `CircuitBreaker` from opossum 10.0.0 at commit
+`decbedf63d7815049233e544dcb351590ff0c84e` as a machine, with two faults,
+`opossum-admits-call-fault` and `opossum-trip-fault`, in [`cases/`](cases). Emitted events, timers, the cache,
+the semaphore, the rolling statistics and fallbacks stay in opossum. Where
+opossum's behaviour isn't what its states suggest, the port keeps it and
+claims no more: any success while half-open closes the breaker, a late one
+included. Two divergences are deliberate: the error rate is compared exactly,
+so `errorThresholdPercentage` must be a whole number, and a restored state
+that says it is both closed and half-open is rejected.
+
+[`adapter.patch`](programs/opossum/adapter.patch) is written by hand: it makes
+opossum's own `lib/circuit.js` keep its state in the generated `breaker.ts`,
+copied into opossum as `lib/breaker.mts` (in a `"type": "commonjs"` package,
+Node loads it only under that extension), and ask it for each decision. It
+throws a `TypeError` at construction for a fractional threshold.
+`scripts/check-opossum.sh <empty folder>` runs opossum's lint and tests as
+released and with the generated module in place. It needs git, Node 22 or
+later and network access, so CI doesn't run it. On the machine it was written
+on, test 331, a rolling window of 10 ms, and tests 547 to 549, health-check
+timers that fire after their test ended, fail in both runs; the check accepts
+those only. The port is licensed under Apache-2.0; attribution is in
+[`programs/opossum/NOTICE`](programs/opossum/NOTICE).
+
 ## Cedar partial authorization
 
 [`programs/cedar/`](programs/cedar) ports the Boolean decision in Cedar's

conformance/cases/opossum-admits-call-fault.accord

@@ -0,0 +1,110 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, passed
+// opossum's breaker (conformance/programs/opossum) with a planted fault:
+// `admits_call` forgets that a shut-down breaker runs nothing.
+
+/// Where the breaker stands.
+pub enum BreakerPhase { Closed, Open, HalfOpen, Shutdown }
+
+/// A circuit breaker's state, without its timers, statistics or cache.
+pub machine Breaker {
+    intent "Let calls through while closed, refuse them while open, let one probe through when the reset timeout ends, and let nothing through once shut down."
+
+    state {
+        phase: BreakerPhase,
+        pending_close: Bool,
+        enabled: Bool,
+        warming_up: Bool,
+    }
+
+    init initial(is_enabled: Bool, is_warming_up: Bool) {
+        next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    /// A breaker restored from `options.state`; `open_expired` is whether more
+    /// than the reset timeout has passed since the saved `lastTimerAt`.
+    init restored(is_enabled: Bool, is_warming_up: Bool, closed: Bool, half_open: Bool, shut_down: Bool, open_expired: Bool)
+        requires not (closed and half_open)
+    decide {
+        | shut_down               => next { phase: Shutdown, pending_close: half_open, enabled: false, warming_up: is_warming_up }
+        | closed                  => next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+        | half_open or open_expired => next { phase: HalfOpen, pending_close: true, enabled: is_enabled, warming_up: is_warming_up }
+        | otherwise               => next { phase: Open, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    event close() {
+        if phase == Closed {
+            next { }
+        } else {
+            next { phase: Closed, pending_close: false }
+        }
+    }
+
+    /// opossum's `open()`; `open` is an Accord keyword.
+    event trip() {
+        if phase == Open {
+            next { }
+        } else {
+            next { phase: Open, pending_close: false }
+        }
+    }
+
+    /// The reset timeout ended: the next call is the probe.
+    event reset_elapsed() {
+        next { phase: HalfOpen, pending_close: true }
+    }
+
+    /// A protected call was let through; a half-open breaker's probe is used.
+    event call_admitted() {
+        next { pending_close: false }
+    }
+
+    event shut_down() {
+        next { phase: Shutdown, enabled: false }
+    }
+
+    event enable() {
+        next { enabled: true }
+    }
+
+    event disable() {
+        next { enabled: false }
+    }
+
+    event warm_up_ended() {
+        next { warming_up: false }
+    }
+
+    /// Whether a protected call runs now: closed, or holding its half-open probe.
+    fn admits() -> Bool {
+        phase == Closed or pending_close
+    }
+
+    /// Whether `fire()` runs the action at all: never once shut down, always
+    /// when disabled, and otherwise as `admits` says.
+    fn admits_call() -> Bool
+        ensures phase == Shutdown implies not result
+        ensures phase == Open and enabled implies not result
+    {
+        not enabled or phase == Closed or pending_close
+    }
+
+    /// Whether a failure opens the breaker, given the rolling window's counts.
+    fn opens_on_failure(fires: i64, failures: i64, volume_threshold: i64, threshold: i64) -> Bool
+        requires fires >= 0 and failures >= 0 and failures <= fires and fires <= 1000000000000
+        requires threshold >= 0 and threshold <= 1000000
+    decide {
+        | warming_up                                     => false
+        | fires < volume_threshold and phase != HalfOpen => false
+        | otherwise                                      => failures * 100 > threshold * fires or phase == HalfOpen
+    }
+
+    invariant pending_close_is_half_open: pending_close implies phase == HalfOpen or phase == Shutdown
+}
+
+example Breaker
+    initial(is_enabled: true, is_warming_up: false)
+    trip()
+    reset_elapsed()
+    call_admitted()
+    close()
+    gives phase == Closed and not pending_close

conformance/cases/opossum-trip-fault.accord

@@ -0,0 +1,111 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, passed
+// opossum's breaker (conformance/programs/opossum) with a planted fault:
+// `trip` keeps `pending_close`, so a half-open breaker that trips is open and
+// still holds a probe.
+
+/// Where the breaker stands.
+pub enum BreakerPhase { Closed, Open, HalfOpen, Shutdown }
+
+/// A circuit breaker's state, without its timers, statistics or cache.
+pub machine Breaker {
+    intent "Let calls through while closed, refuse them while open, let one probe through when the reset timeout ends, and let nothing through once shut down."
+
+    state {
+        phase: BreakerPhase,
+        pending_close: Bool,
+        enabled: Bool,
+        warming_up: Bool,
+    }
+
+    init initial(is_enabled: Bool, is_warming_up: Bool) {
+        next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    /// A breaker restored from `options.state`; `open_expired` is whether more
+    /// than the reset timeout has passed since the saved `lastTimerAt`.
+    init restored(is_enabled: Bool, is_warming_up: Bool, closed: Bool, half_open: Bool, shut_down: Bool, open_expired: Bool)
+        requires not (closed and half_open)
+    decide {
+        | shut_down               => next { phase: Shutdown, pending_close: half_open, enabled: false, warming_up: is_warming_up }
+        | closed                  => next { phase: Closed, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+        | half_open or open_expired => next { phase: HalfOpen, pending_close: true, enabled: is_enabled, warming_up: is_warming_up }
+        | otherwise               => next { phase: Open, pending_close: false, enabled: is_enabled, warming_up: is_warming_up }
+    }
+
+    event close() {
+        if phase == Closed {
+            next { }
+        } else {
+            next { phase: Closed, pending_close: false }
+        }
+    }
+
+    /// opossum's `open()`; `open` is an Accord keyword.
+    event trip() {
+        if phase == Open {
+            next { }
+        } else {
+            next { phase: Open }
+        }
+    }
+
+    /// The reset timeout ended: the next call is the probe.
+    event reset_elapsed() {
+        next { phase: HalfOpen, pending_close: true }
+    }
+
+    /// A protected call was let through; a half-open breaker's probe is used.
+    event call_admitted() {
+        next { pending_close: false }
+    }
+
+    event shut_down() {
+        next { phase: Shutdown, enabled: false }
+    }
+
+    event enable() {
+        next { enabled: true }
+    }
+
+    event disable() {
+        next { enabled: false }
+    }
+
+    event warm_up_ended() {
+        next { warming_up: false }
+    }
+
+    /// Whether a protected call runs now: closed, or holding its half-open probe.
+    fn admits() -> Bool {
+        phase == Closed or pending_close
+    }
+
+    /// Whether `fire()` runs the action at all: never once shut down, always
+    /// when disabled, and otherwise as `admits` says.
+    fn admits_call() -> Bool
+        ensures phase == Shutdown implies not result
+        ensures phase == Open and enabled implies not result
+    {
+        phase != Shutdown and (not enabled or phase == Closed or pending_close)
+    }
+
+    /// Whether a failure opens the breaker, given the rolling window's counts.
+    fn opens_on_failure(fires: i64, failures: i64, volume_threshold: i64, threshold: i64) -> Bool
+        requires fires >= 0 and failures >= 0 and failures <= fires and fires <= 1000000000000
+        requires threshold >= 0 and threshold <= 1000000
+    decide {
+        | warming_up                                     => false
+        | fires < volume_threshold and phase != HalfOpen => false
+        | otherwise                                      => failures * 100 > threshold * fires or phase == HalfOpen
+    }
+
+    invariant pending_close_is_half_open: pending_close implies phase == HalfOpen or phase == Shutdown
+}
+
+example Breaker
+    initial(is_enabled: true, is_warming_up: false)
+    trip()
+    reset_elapsed()
+    call_admitted()
+    close()
+    gives phase == Closed and not pending_close

conformance/cases/provider-retry-ignore-cancel-fault.accord

@@ -0,0 +1,104 @@
+// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved
+// The model's `IgnoreCancel` fault: the post-wait guard ignores cancellation,
+// so a retry that starts after `cancel` makes another call.
+
+/// Where a retried model call stands.
+enum RetryPhase { Failed, Waiting, Calling, Ended }
+
+/// A failed model call, retried within a budget and a time window.
+machine ProviderRetry {
+    intent "Retry a failed model call at most three times within its window, wait before each retry, never call again after cancellation, and never repeat a completed tool."
+
+    state {
+        phase: RetryPhase,
+        time: i32,
+        due: i32,
+        retries: i32,
+        calls: i32,
+        stopped: Bool,
+        calls_at_stop: i32,
+        terminal: Bool,
+        last_start: i32,
+        last_due: i32,
+        tools: i32,
+    }
+
+    init start(is_terminal: Bool) {
+        next {
+            phase: Failed,
+            time: 0,
+            due: 0,
+            retries: 0,
+            calls: 1,
+            stopped: false,
+            calls_at_stop: 0,
+            terminal: is_terminal,
+            last_start: 0,
+            last_due: 0,
+            tools: 1,
+        }
+    }
+
+    event schedule(delay: i32)
+        requires phase == Failed
+        requires delay == 1 or delay == 60 or delay == 121
+    {
+        if not terminal and not stopped and retries < 3 and time + delay < 120 {
+            next { phase: Waiting, due: time + delay, retries: retries + 1 }
+        } else {
+            next { phase: Ended }
+        }
+    }
+
+    event advance_to_due()
+        requires phase == Waiting and time < 120 and due >= time
+    {
+        next { time: due }
+    }
+
+    event advance_to_end()
+        requires phase == Waiting and time < 120
+    {
+        next { time: 120 }
+    }
+
+    event cancel()
+        requires not stopped and phase != Ended
+    {
+        next { stopped: true, calls_at_stop: calls }
+    }
+
+    event start_call()
+        requires phase == Waiting and time >= due and time < 120
+    {
+        next { phase: Calling, calls: calls + 1, last_start: time, last_due: due }
+    }
+
+    event stop_wait()
+        requires phase == Waiting and (stopped or time >= 120)
+    {
+        next { phase: Ended }
+    }
+
+    event failure(is_terminal: Bool)
+        requires phase == Calling
+    {
+        next { phase: Failed, terminal: is_terminal }
+    }
+
+    event success()
+        requires phase == Calling
+    {
+        next { phase: Ended }
+    }
+
+    invariant bounds: retries <= 3 and calls <= 4 and last_start < 120
+    invariant cancel_stops_calls: stopped implies calls == calls_at_stop
+    invariant wait_respected: last_start >= last_due
+    invariant tools_stay: tools == 1
+
+    helper invariant calls_follow_retries: calls <= retries + 1
+    helper invariant waiting_before_call: phase == Waiting implies calls <= retries
+    helper invariant time_in_window: time <= 120
+    helper invariant due_in_window: due <= 120
+}