diff --git a/ROADMAP.md b/ROADMAP.md index b606ce5..f942ec1 100644 --- a/ROADMAP.md +++ b/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 | | diff --git a/conformance/README.md b/conformance/README.md index a7bfecc..35e00a3 100644 --- a/conformance/README.md +++ b/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 ` 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 diff --git a/conformance/cases/opossum-admits-call-fault.accord b/conformance/cases/opossum-admits-call-fault.accord new file mode 100644 index 0000000..19fddfa --- /dev/null +++ b/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 diff --git a/conformance/cases/opossum-trip-fault.accord b/conformance/cases/opossum-trip-fault.accord new file mode 100644 index 0000000..5f43874 --- /dev/null +++ b/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 diff --git a/conformance/cases/provider-retry-ignore-cancel-fault.accord b/conformance/cases/provider-retry-ignore-cancel-fault.accord new file mode 100644 index 0000000..aa57c44 --- /dev/null +++ b/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 +} diff --git a/conformance/cases/provider-retry-replay-tool-fault.accord b/conformance/cases/provider-retry-replay-tool-fault.accord new file mode 100644 index 0000000..62b4d1f --- /dev/null +++ b/conformance/cases/provider-retry-replay-tool-fault.accord @@ -0,0 +1,103 @@ +// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, refuted, proved, proved, proved, proved, proved, proved, proved, proved, proved +// The model's `ReplayTool` fault: a retry replays the completed tool. + +/// 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 and not stopped + { + next { phase: Calling, calls: calls + 1, last_start: time, last_due: due, tools: tools + 1 } + } + + 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 +} diff --git a/conformance/cases/provider-retry.accord b/conformance/cases/provider-retry.accord new file mode 100644 index 0000000..9f1d72f --- /dev/null +++ b/conformance/cases/provider-retry.accord @@ -0,0 +1,109 @@ +// expect: proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved, proved +// Tesota's ProviderRetry design model (models/ProviderRetry.tla at +// 4ef9b191), as a machine. Each choice the model leaves open is an event's +// parameter, or two events where it depends on the state: `Advance` sets the +// time to `due` or to the end of the window, so it is `advance_to_due` and +// `advance_to_end`. The constant `route` and the stuttering `Done` are left +// out. The four invariants aren't inductive on their own; the four helper +// invariants make them so. + +/// 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 and not stopped + { + 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 +} diff --git a/conformance/programs/opossum/NOTICE b/conformance/programs/opossum/NOTICE new file mode 100644 index 0000000..e6c570c --- /dev/null +++ b/conformance/programs/opossum/NOTICE @@ -0,0 +1,10 @@ +opossum circuit breaker state +Author: Red Hat, Inc. (opossum's package.json) + +The port in breaker.accord is derived from opossum, +https://github.com/nodeshift/opossum, release 10.0.0 at commit +decbedf63d7815049233e544dcb351590ff0c84e (lib/circuit.js). +It is licensed under Apache-2.0 (see LICENSE-APACHE at the repository root). +The port states the breaker's state and its decisions as a machine; +adapter.patch changes opossum's own lib/circuit.js to keep its state in the +generated module and to ask it for each decision. diff --git a/conformance/programs/opossum/adapter.patch b/conformance/programs/opossum/adapter.patch new file mode 100644 index 0000000..36de688 --- /dev/null +++ b/conformance/programs/opossum/adapter.patch @@ -0,0 +1,299 @@ +diff --git a/lib/circuit.js b/lib/circuit.js +index 82dd77f..012b177 100644 +--- a/lib/circuit.js ++++ b/lib/circuit.js +@@ -4,19 +4,13 @@ const EventEmitter = require('events'); + const Status = require('./status'); + const Semaphore = require('./semaphore'); + const MemoryCache = require('./cache'); ++const Breaker = require('./breaker.mts'); + + const STATE = Symbol('state'); +-const OPEN = Symbol('open'); +-const CLOSED = Symbol('closed'); +-const HALF_OPEN = Symbol('half-open'); +-const PENDING_CLOSE = Symbol('pending-close'); +-const SHUTDOWN = Symbol('shutdown'); + const FALLBACK_FUNCTION = Symbol('fallback'); + const STATUS = Symbol('status'); + const NAME = Symbol('name'); + const GROUP = Symbol('group'); +-const ENABLED = Symbol('Enabled'); +-const WARMING_UP = Symbol('warming-up'); + const VOLUME_THRESHOLD = Symbol('volume-threshold'); + const OUR_ERROR = Symbol('our-error'); + const RESET_TIMEOUT = Symbol('reset-timeout'); +@@ -180,6 +174,13 @@ class CircuitBreaker extends EventEmitter { + this.options.resetTimeout = options.resetTimeout ?? 30000; + this.options.errorThresholdPercentage = + options.errorThresholdPercentage ?? 50; ++ // The state machine compares the error rate exactly, so the threshold ++ // must be a whole number. ++ if (!Number.isInteger(this.options.errorThresholdPercentage)) { ++ throw new TypeError( ++ 'options.errorThresholdPercentage must be a whole number' ++ ); ++ } + this.options.rollingCountTimeout = options.rollingCountTimeout ?? 10000; + this.options.rollingCountBuckets = options.rollingCountBuckets ?? 10; + this.options.rollingPercentilesEnabled = +@@ -238,7 +239,7 @@ class CircuitBreaker extends EventEmitter { + this[VOLUME_THRESHOLD] = Number.isInteger(options.volumeThreshold) + ? options.volumeThreshold + : 0; +- this[WARMING_UP] = options.allowWarmUp === true; ++ const allowWarmUp = options.allowWarmUp === true; + + // The user can pass in a Status object to initialize the Status/stats + if (this.options.status) { +@@ -252,31 +253,30 @@ class CircuitBreaker extends EventEmitter { + this[STATUS] = new Status(this.options); + } + +- this[STATE] = CLOSED; +- ++ let restored = null; + if (options.state) { +- this[ENABLED] = options.state.enabled !== false; +- this[WARMING_UP] = options.state.warmUp || this[WARMING_UP]; +- // Closed if nothing is passed in +- this[CLOSED] = options.state.closed !== false; +- // These should be in sync +- this[HALF_OPEN] = this[PENDING_CLOSE] = options.state.halfOpen || false; +- // Open should be the opposite of closed, +- // but also the opposite of half_open +- this[OPEN] = !this[CLOSED] && !this[HALF_OPEN]; +- this[SHUTDOWN] = options.state.shutdown || false; ++ const saved = options.state; ++ const closed = saved.closed !== false; ++ const halfOpen = Boolean(saved.halfOpen || false); ++ const shutdown = Boolean(saved.shutdown || false); ++ const expired = saved.lastTimerAt !== undefined && ++ (Date.now() - saved.lastTimerAt) > this.options.resetTimeout; ++ this[STATE] = Breaker.restored(saved.enabled !== false, ++ Boolean(saved.warmUp || allowWarmUp), closed, halfOpen, shutdown, ++ expired); ++ if (shutdown) restored = 'shutdown'; ++ else if (!closed && !halfOpen) restored = expired ? 'halfOpen' : 'open'; + } else { +- this[PENDING_CLOSE] = false; +- this[ENABLED] = options.enabled !== false; ++ this[STATE] = Breaker.initial(options.enabled !== false, allowWarmUp); + } + + this[FALLBACK_FUNCTION] = null; + this[NAME] = options.name || action.name || nextName(); + this[GROUP] = options.group || this[NAME]; + +- if (this[WARMING_UP]) { ++ if (this[STATE].warmingUp) { + const timer = this[WARMUP_TIMEOUT] = setTimeout( +- _ => (this[WARMING_UP] = false), ++ _ => (this[STATE] = Breaker.warmUpEnded(this[STATE])), + this.options.rollingCountTimeout + ); + if (typeof timer.unref === 'function') { +@@ -331,8 +331,7 @@ class CircuitBreaker extends EventEmitter { + * @returns {void} + */ + function _halfOpen (circuit) { +- circuit[STATE] = HALF_OPEN; +- circuit[PENDING_CLOSE] = true; ++ circuit[STATE] = Breaker.resetElapsed(circuit[STATE]); + circuit._renewAbortControllerIfNeeded(); + /** + * Emitted after `options.resetTimeout` has elapsed, allowing for +@@ -353,24 +352,15 @@ class CircuitBreaker extends EventEmitter { + }); + + // Prepopulate the State of the Breaker +- if (this[SHUTDOWN]) { +- this[STATE] = SHUTDOWN; ++ if (restored === 'shutdown') { + this.shutdown(); +- } else if (this[CLOSED]) { +- this.close(); +- } else if (this[OPEN]) { +- // If the state being passed in is OPEN but more time has elapsed +- // than the resetTimeout, then we should be in halfOpen state +- if (this.options.state.lastTimerAt !== undefined && +- (Date.now() - this.options.state.lastTimerAt) > +- this.options.resetTimeout) { +- _halfOpen(this); +- } else { +- this.open(); +- } +- } else if (this[HALF_OPEN]) { +- // Not sure if anything needs to be done here +- this[STATE] = HALF_OPEN; ++ } else if (restored === 'open') { ++ this.emit('open'); ++ } else if (restored === 'halfOpen') { ++ // More time has elapsed than the resetTimeout since the saved state ++ // was opened, so the breaker is half-open. ++ this._renewAbortControllerIfNeeded(); ++ this.emit('halfOpen', this.options.resetTimeout); + } + } + +@@ -395,12 +385,11 @@ class CircuitBreaker extends EventEmitter { + * @returns {void} + */ + close () { +- if (this[STATE] !== CLOSED) { ++ if (this[STATE].phase !== 'closed') { + if (this[RESET_TIMEOUT]) { + clearTimeout(this[RESET_TIMEOUT]); + } +- this[STATE] = CLOSED; +- this[PENDING_CLOSE] = false; ++ this[STATE] = Breaker.close(this[STATE]); + this._renewAbortControllerIfNeeded(); + /** + * Emitted when the breaker is reset allowing the action to execute again +@@ -420,9 +409,8 @@ class CircuitBreaker extends EventEmitter { + * @returns {void} + */ + open () { +- if (this[STATE] !== OPEN) { +- this[STATE] = OPEN; +- this[PENDING_CLOSE] = false; ++ if (this[STATE].phase !== 'open') { ++ this[STATE] = Breaker.trip(this[STATE]); + /** + * Emitted when the breaker opens because the action has + * failure percentage greater than `options.errorThresholdPercentage`. +@@ -453,7 +441,7 @@ class CircuitBreaker extends EventEmitter { + clearTimeout(this[WARMUP_TIMEOUT]); + } + this.status.shutdown(); +- this[STATE] = SHUTDOWN; ++ this[STATE] = Breaker.shutDown(this[STATE]); + + // clear cache on shutdown + this.clearCache(); +@@ -464,7 +452,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get isShutdown () { +- return this[STATE] === SHUTDOWN; ++ return this[STATE].phase === 'shutdown'; + } + + /** +@@ -488,7 +476,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get pendingClose () { +- return this[PENDING_CLOSE]; ++ return this[STATE].pendingClose; + } + + /** +@@ -496,7 +484,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get closed () { +- return this[STATE] === CLOSED; ++ return this[STATE].phase === 'closed'; + } + + /** +@@ -504,7 +492,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get opened () { +- return this[STATE] === OPEN; ++ return this[STATE].phase === 'open'; + } + + /** +@@ -512,7 +500,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get halfOpen () { +- return this[STATE] === HALF_OPEN; ++ return this[STATE].phase === 'half_open'; + } + + /** +@@ -553,7 +541,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get enabled () { +- return this[ENABLED]; ++ return this[STATE].enabled; + } + + /** +@@ -561,7 +549,7 @@ class CircuitBreaker extends EventEmitter { + * @type {Boolean} + */ + get warmUp () { +- return this[WARMING_UP]; ++ return this[STATE].warmingUp; + } + + /** +@@ -656,7 +644,7 @@ class CircuitBreaker extends EventEmitter { + this.emit('fire', args); + + // Protection, caches and coalesce disabled. +- if (!this[ENABLED]) { ++ if (!this[STATE].enabled) { + const result = this.action.apply(context, args); + return (typeof result.then === 'function') + ? result +@@ -708,7 +696,7 @@ class CircuitBreaker extends EventEmitter { + this.emit('coalesceCacheMiss'); + } + +- if (!this.closed && !this.pendingClose) { ++ if (!Breaker.admits(this[STATE])) { + /** + * Emitted when the circuit breaker is open and failing fast + * @event CircuitBreaker#reject +@@ -721,7 +709,7 @@ class CircuitBreaker extends EventEmitter { + return fallback(this, error, args) || + Promise.reject(error); + } +- this[PENDING_CLOSE] = false; ++ this[STATE] = Breaker.callAdmitted(this[STATE]); + + let timeout; + let timeoutError = false; +@@ -898,7 +886,7 @@ class CircuitBreaker extends EventEmitter { + * @returns {void} + */ + enable () { +- this[ENABLED] = true; ++ this[STATE] = Breaker.enable(this[STATE]); + this.status.startListeneningForRotateEvent(); + } + +@@ -908,7 +896,7 @@ class CircuitBreaker extends EventEmitter { + * @returns {void} + */ + disable () { +- this[ENABLED] = false; ++ this[STATE] = Breaker.disable(this[STATE]); + this.status.removeRotateBucketControllerListener(); + } + +@@ -985,14 +973,9 @@ function fail (circuit, err, args, latency) { + * @type {Error} + */ + circuit.emit('failure', err, latency, args); +- if (circuit.warmUp) return; +- +- // check stats to see if the circuit should be opened + const stats = circuit.stats; +- if ((stats.fires < circuit.volumeThreshold) && !circuit.halfOpen) return; +- const errorRate = stats.failures / stats.fires * 100; +- if (errorRate > circuit.options.errorThresholdPercentage || +- circuit.halfOpen) { ++ if (Breaker.opensOnFailure(circuit[STATE], stats.fires, stats.failures, ++ circuit.volumeThreshold, circuit.options.errorThresholdPercentage)) { + circuit.open(); + } + } diff --git a/conformance/programs/opossum/breaker.accord b/conformance/programs/opossum/breaker.accord new file mode 100644 index 0000000..f1d2956 --- /dev/null +++ b/conformance/programs/opossum/breaker.accord @@ -0,0 +1,129 @@ +// 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, proved, proved, proved, proved, proved, proved, proved, proved, passed +// SPDX-License-Identifier: Apache-2.0 +// Derived from opossum, by Red Hat, Inc. according to its package.json; its +// LICENSE names no copyright holder. Licensed under Apache-2.0; see NOTICE. +// The state and decisions of opossum's CircuitBreaker (opossum 10.0.0, commit +// decbedf63d7815049233e544dcb351590ff0c84e, lib/circuit.js), ported +// faithfully as a machine. Emitted events, timers, the cache, the semaphore, +// the rolling statistics and fallbacks stay in opossum; its adapter.patch +// calls this module for every state change and decision. +// +// 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 success from a +// call admitted before it opened included (`close` from `HalfOpen`); +// - `close()` or `open()` after `shutdown()` leaves the shut-down state; +// - `disable()` lets calls through whatever the state; +// - `shutdown()` while half-open keeps `pending_close`. +// Two divergences are deliberate: the error rate is compared exactly, +// `failures * 100 > threshold * fires`, where opossum divides in floating +// point, so a threshold must be a whole number; and a restored state that +// says it is both closed and half-open, which opossum's own `toJSON` never +// writes, is rejected. + +/// 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 + { + 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 diff --git a/docs/design/measurements/2026-11-12-stage-10-machines/README.md b/docs/design/measurements/2026-11-12-stage-10-machines/README.md index 32becf0..6ebf378 100644 --- a/docs/design/measurements/2026-11-12-stage-10-machines/README.md +++ b/docs/design/measurements/2026-11-12-stage-10-machines/README.md @@ -147,3 +147,28 @@ violation in the correct model. - Solver times: each file ran once with a 10-second limit, and none timed out. - That the stand-in matches opossum on paths its tests don't reach. + +## The port against tla-ts, 2026-11-12 + +Once machines were checked, the ProviderRetry port +(`conformance/cases/provider-retry.accord`) was compared with Tesota's TLA+ +model run by [tla-ts](https://github.com/aidenybai/tla-ts), a TLC +replacement in TypeScript, at `8067c48`: + +``` +node /packages/tla-ts/dist/cli.js ProviderRetry.tla -config +``` + +with the model and its three configurations from Tesota at `4ef9b191`. + +| Configuration | tla-ts | Accord's explorer | +| --- | --- | --- | +| `ProviderRetry.cfg` | 148 distinct states, no violation | 148 states, all of them; every obligation proved | +| `ProviderRetry-no-cancel.cfg` | `CancelStopsCalls` violated after Schedule, Advance, Cancel, StartCall | `start_call` refuted after `schedule(1)`, `advance_to_due()`, `cancel()`, `start_call()` | +| `ProviderRetry-replay-tool.cfg` | `ToolsAndRouteStay` violated after Schedule, Advance, StartCall | `start_call` refuted after `schedule(1)`, `advance_to_due()`, `start_call()` | + +The state counts agree, and so do the shortest traces, step for step. The +port writes `Advance`'s choice of the next time as two events, since the +choice depends on the state; the states it reaches are the model's. This is +agreement with a second checker on one model, not a proof that the explorer +is complete. diff --git a/scripts/check-opossum.sh b/scripts/check-opossum.sh new file mode 100644 index 0000000..f4f625a --- /dev/null +++ b/scripts/check-opossum.sh @@ -0,0 +1,58 @@ +#!/usr/bin/env bash +# Stage 10's check against a state machine from outside Tesota: opossum's own +# lint and tests, run once as released and once with its breaker state and +# decisions kept in the module `accord build` writes from +# conformance/programs/opossum, through adapter.patch. +# +# Usage: scripts/check-opossum.sh [opossum repository] +# It needs git, Node 22 or later, npm with network access, and the solvers +# (ACCORD_Z3 and ACCORD_CVC5). Both runs' output is kept in the folder. +# +# A few tests are known to fail in both runs on a slow or Windows machine: +# a rolling-window test with a 10 ms window, and health-check timers that +# fire after their test ended. A run passes when lint passes and every failing +# assertion is one of those. +set -euo pipefail + +work="${1:?usage: scripts/check-opossum.sh [opossum repository]}" +repository="${2:-https://github.com/nodeshift/opossum}" +commit=decbedf63d7815049233e544dcb351590ff0c84e +root="$(cd "$(dirname "$0")/.." && pwd)" +port="$root/conformance/programs/opossum" +repo="$work/opossum" +known='^not ok [0-9]+ (failures reset because no event emitter is provided and rollingCountTimeout set to 10ms|\.end\(\) already called.*|plan != count)$' + +if [ -e "$work" ] && [ -n "$(ls -A "$work")" ]; then + echo "$work: not empty" >&2 + exit 2 +fi +git -c core.autocrlf=false clone --quiet --no-checkout "$repository" "$repo" +git -C "$repo" -c core.autocrlf=false checkout --quiet "$commit" +(cd "$repo" && npm ci --ignore-scripts --no-audit --no-fund > "$work/npm.log" 2>&1) + +run() { # label + local log="$work/$1.log" status=0 + ( + cd "$repo" + npx eslint --ignore-path .gitignore . + npx tape test/*.js + ) > "$log" 2>&1 || status=$? + echo "$1: $(grep -E '^# (tests|pass|fail)' "$log" | tr '\n' ' ') (output in $log)" + local others + others="$(grep -E '^not ok' "$log" | tr -d '\r' | grep -Ev "$known" || true)" + if ! grep -qE '^# tests ' "$log" || [ -n "$others" ]; then + echo "$1: failed beyond the known tests (exit $status)" >&2 + [ -n "$others" ] && echo "$others" >&2 + return 1 + fi +} + +failed=0 +run original || failed=1 + +(cd "$root" && cargo run --release --quiet -- build "$port" --out "$work/generated") +cp "$work/generated/breaker.ts" "$repo/lib/breaker.mts" +git -C "$repo" apply "$port/adapter.patch" +git -C "$repo" status --short +run generated || failed=1 +exit "$failed"