[Sequela02]

Closes stage 10. Its done criterion was "a Tesota design model ported, its faults detected; the circuit breaker of opossum, closed, open and half-open, proved, and opossum's tests pass with the generated module". Both halves hold. No compiler code changes in this PR.

ProviderRetry (Tesota)

conformance/cases/provider-retry.accord ports models/ProviderRetry.tla at Tesota 4ef9b191.

• Advance's choice of the next time depends on the state, so it becomes two events, advance_to_due and advance_to_end.
• 21 obligations proved with the four helper invariants the stage 10 probe found. The explorer reaches all 148 states.
• Both planted faults (IgnoreCancel, ReplayTool) are refuted by their shortest runs.
• Against tla-ts, running Tesota's own model: the same 148 distinct states and the same fault traces, step for step. Recorded in the stage 10 measurement.

opossum's breaker

conformance/programs/opossum/breaker.accord ports the breaker's state and decisions from opossum 10.0.0 (decbedf), faithfully. It's verified: 32 obligations and 1 example.

• What it proves:
  • a pending probe implies half-open or shut down;
  • admits_call() lets nothing through once shut down, nor while open and enabled.
• Owner decision (Stage 10: state machines #82, option A): a faithful port can't prove "pending close implies half-open", because opossum's shutdown() keeps pendingClose while half-open. So the invariant includes shut down, and the behaviour is listed.
• opossum behaviours kept and listed, not claimed:
  • a late success closes a half-open breaker;
  • close() or open() after shutdown();
  • disable();
  • shutdown() keeping pendingClose.
• Deliberate divergences:
  • the error rate is compared exactly, so a fractional threshold is rejected, at construction in the adapter;
  • a restored state that is both closed and half-open is rejected.
• Two planted faults are refuted by runs:
  • trip keeps pending_close;
  • admits_call ignores shutdown.
• Integration: adapter.patch makes opossum's own lib/circuit.js keep its state in the generated module (copied as lib/breaker.mts). scripts/check-opossum.sh runs opossum's lint and tests as released and with the module. Both runs pass 546 of 550, with the same four failures, which are known on this machine: a 10 ms timing test and a health-check timer that fires after its test.
• The half-open stale-success behaviour, reproduced against the patched opossum, is unchanged.

Verification

• cargo fmt --all --check and cargo clippy --workspace --all-targets --locked -- -D warnings are clean.
• cargo test --workspace --locked with the pinned solvers: 97 passed, 1 ignored. That includes both ports and the four fault cases.
• The E2 materials step (score.py --self-test, materials.py) passes, without a bytecode cache.
• scripts/check-opossum.sh run end to end: exit 0, 53 s, both runs 546 of 550, with the same failing tests.

Not established:

• The opossum check runs only on this Windows machine; CI doesn't run it. It needs network and npm.
• opossum names no copyright holder: its LICENSE is the bare Apache-2.0 text and it has no NOTICE. The NOTICE credits Red Hat, Inc. as the author, per opossum's package.json, and states nothing more.

Risk note

Two-way door: conformance programs, a hand-written patch, a check script and docs. No compiler change. Blast radius: none for users; it sets stage 10 as done in the roadmap and stage 11 as next. Evidence: the conformance run, the opossum check and the tla-ts comparison above.

Closes #82