From 9daaf6e9067291d6f2e1bd67f4c048b6b647b2ce Mon Sep 17 00:00:00 2001 From: eigmax Date: Thu, 27 Aug 2026 13:51:26 +0000 Subject: [PATCH 1/4] tla: model-check verifier-challenge gaps for issues #429 and #431 Two TLA+ specs (node/tla/) formalising the unauthorized-kickoff -> uncontested Take1 threat, verified against the real dev (gc-v2) source and reproduced under TLC. VerifierKickoffFailOpen (issue #429) - LIVE on dev. handle_kickoff_sent_verifier is one-shot and fail-open: when GOAT SPV lags the kickoff height it returns Ok(()) with no push_local_unhandled_messages_with_ reason, so the KickoffSent message is marked Processed and the Challenge is never retried (detect_kickoff only re-scans OperatorDataPushed; should_always_ challenge is never called). The committee handler defers the same lag; the verifier does not. - VerifierKickoffFailOpen.cfg -> FAILS (NoUnauthorizedTake1, 3-step CEX) - VerifierKickoffFailOpenFixed.cfg -> passes (defer/retry, mirroring committee) KickoffScanCoverage (issue #431) - FIXED on dev by 2bce25d (#451). detect_kickoff's per-operator round-robin (fetch_first_graph_per_operator_by_ status) watched only the lowest-nonce graph, so a kickoff on a later graph was never observed. scan_kickoff_chain now walks confirmed prekickoff successors from the idle root, closing the filed 2-graph attack; detect_take1_or_challenge and process_graph_challenge also moved to fetch_all_graphs_by_status. - KickoffScanCoverage.cfg -> FAILS (original one-per-operator select) - KickoffScanCoverageFixed.cfg -> passes (chain walk, adequate depth) - KickoffScanCoverageResidual.cfg -> FAILS (chain deeper than the MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 cap) Root cause (shared): the challenge defense is built from best-effort, at-most-once local scheduling primitives (round-robin selection, one-shot message handlers) rather than a persistent challenge obligation created by complete observation and retired only by an on-chain Challenge. #431 is the completeness face; #429 is the persistence face. --- node/tla/KickoffScanCoverage.cfg | 7 ++ node/tla/KickoffScanCoverage.tla | 80 +++++++++++++ node/tla/KickoffScanCoverageFixed.cfg | 8 ++ node/tla/KickoffScanCoverageResidual.cfg | 7 ++ node/tla/VerifierKickoffFailOpen.cfg | 8 ++ node/tla/VerifierKickoffFailOpen.tla | 136 ++++++++++++++++++++++ node/tla/VerifierKickoffFailOpenFixed.cfg | 7 ++ 7 files changed, 253 insertions(+) create mode 100644 node/tla/KickoffScanCoverage.cfg create mode 100644 node/tla/KickoffScanCoverage.tla create mode 100644 node/tla/KickoffScanCoverageFixed.cfg create mode 100644 node/tla/KickoffScanCoverageResidual.cfg create mode 100644 node/tla/VerifierKickoffFailOpen.cfg create mode 100644 node/tla/VerifierKickoffFailOpen.tla create mode 100644 node/tla/VerifierKickoffFailOpenFixed.cfg diff --git a/node/tla/KickoffScanCoverage.cfg b/node/tla/KickoffScanCoverage.cfg new file mode 100644 index 00000000..c4382ae3 --- /dev/null +++ b/node/tla/KickoffScanCoverage.cfg @@ -0,0 +1,7 @@ +\* ORIGINAL #431 @ f2f0285e: detect_kickoff watches only the lowest-nonce +\* graph per operator (no chain walk). ScanDepth=0. Operator has 3 graphs. +\* Expected to FAIL: kicking nonce 1 or 2 escapes coverage. +CONSTANTS NumGraphs = 3 ScanDepth = 0 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/KickoffScanCoverage.tla b/node/tla/KickoffScanCoverage.tla new file mode 100644 index 00000000..3e1467ba --- /dev/null +++ b/node/tla/KickoffScanCoverage.tla @@ -0,0 +1,80 @@ +---- MODULE KickoffScanCoverage ---- +(***************************************************************************) +(* Model of GOATNetwork/bitvm-node issue #431: *) +(* "detect_kickoff watches only the lowest-nonce graph per operator, so *) +(* a kickoff on a later graph is never Challenged (unauthorized Take1)". *) +(* *) +(* THE ORIGINAL BUG (gc-v2 @ f2f0285e): detect_kickoff sourced its graphs *) +(* from fetch_on_turn_graph_by_status, which keeps ONE row per *) +(* operator_pubkey - the lowest kickoff_index still at OperatorDataPushed *) +(* (SQL: ORDER BY operator_pubkey, kickoff_index; Rust keeps the first per *) +(* operator). An operator with two posted graphs leaves nonce 0 idle and *) +(* kicks nonce >= 1; the kicked graph is never in the watched set, so no *) +(* KickoffSent / Challenge is ever created for it, and after the ConnectorA *) +(* CSV the operator Take1s with pegBTC never burned. Distinct from #429 *) +(* (there the message exists but the verifier skips it on SPV lag). *) +(* *) +(* THE FIX (commit 2bce25d, "Fix graph maintenance logic" #451, on current *) +(* dev): detect_kickoff now runs scan_kickoff_chain from each root, which *) +(* walks confirmed_prekickoff_successor forward - following each graph's *) +(* on-chain-confirmed next_prekickoff to the successor (validated *) +(* kickoff_index == prev+1) - so the idle lowest-nonce decoy no longer *) +(* hides a kicked successor. This closes the filed 2-graph attack. *) +(* *) +(* THE RESIDUAL: the walk is capped at MAX_PREKICKOFF_SUCCESSORS_PER_SCAN *) +(* = 32 (graph_maintenance_tasks.rs). The perpetually-idle root (never *) +(* kicked, so never advancing out of OperatorDataPushed) means the scan *) +(* window never slides; a chain of > 32 idle decoys with the kicked graph *) +(* beyond depth 32 is never reached on any tick. Expensive (33+ confirmed *) +(* on-chain prekickoffs, capital-locked) but structurally open. *) +(* *) +(* This spec is a COVERAGE abstraction (same static-Init idiom as *) +(* Take2DisproveRace.tla): the operator kicks graph `kicked`, keeping the *) +(* root idle; detect_kickoff covers exactly the confirmed chain reachable *) +(* from the root within ScanDepth. Property: the kicked graph is covered *) +(* (hence Challenged). ScanDepth=0 models the original no-walk selection; *) +(* ScanDepth>=NumGraphs-1 models the fix with an adequate depth budget; *) +(* 0= NumGraphs-1 = shipped fix with adequate budget (real MAX = 32) + \* 0 < d < NumGraphs-1 = depth-limit residual + +Graphs == 0 .. (NumGraphs - 1) + +\* The operator keeps the lowest-nonce graph idle as the decoy; it is the +\* single root detect_kickoff selects per operator (fetch_first_graph_per_ +\* operator_by_status). Because it is never kicked it never leaves +\* OperatorDataPushed, so the scan window never advances past it. +Root == 0 + +VARIABLE kicked \* the graph whose kickoff the operator broadcasts (no L2 initWithdraw) +vars == <> + +TypeOK == kicked \in Graphs + +\* To broadcast graph `kicked`'s kickoff the operator must have confirmed the +\* prekickoff chain Root..kicked on Bitcoin (each successor's prekickoff spends +\* the prior next_prekickoff). scan_kickoff_chain therefore CAN follow that +\* confirmed chain from Root - but only up to ScanDepth successors deep. A +\* graph g is covered (its kickoff observed -> KickoffSent -> Challenge) iff +\* the walk reaches it: it lies on the confirmed chain (g <= kicked) and within +\* the depth budget (g <= ScanDepth). +WalkedSet == { g \in Graphs : g <= kicked /\ g <= ScanDepth } + +Init == kicked \in Graphs +Next == UNCHANGED vars \* exhaustive over the Init choice of `kicked` +Spec == Init /\ [][Next]_vars + +-------------------------------------------------------------------------- +\* Safety: every unauthorized kickoff is covered by detect_kickoff (so a +\* Challenge can fire before the operator's uncontested Take1). +\* kicked \in WalkedSet <=> kicked <= ScanDepth. +KickoffAlwaysCovered == kicked \in WalkedSet + +==== diff --git a/node/tla/KickoffScanCoverageFixed.cfg b/node/tla/KickoffScanCoverageFixed.cfg new file mode 100644 index 00000000..7299a8b0 --- /dev/null +++ b/node/tla/KickoffScanCoverageFixed.cfg @@ -0,0 +1,8 @@ +\* SHIPPED FIX (commit 2bce25d / #451): scan_kickoff_chain walks confirmed +\* prekickoff successors from the root. Modeled with a depth budget covering +\* the whole chain (real cap MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32). +\* Expected to PASS: every kicked graph on the confirmed chain is covered. +CONSTANTS NumGraphs = 4 ScanDepth = 3 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/KickoffScanCoverageResidual.cfg b/node/tla/KickoffScanCoverageResidual.cfg new file mode 100644 index 00000000..47e535fe --- /dev/null +++ b/node/tla/KickoffScanCoverageResidual.cfg @@ -0,0 +1,7 @@ +\* DEPTH-LIMIT RESIDUAL: a chain of idle decoys deeper than the scan cap. +\* ScanDepth=2 with 4 graphs (real analogue: >32 decoys, kick beyond depth 32). +\* Expected to FAIL: kicking the graph beyond the depth budget still escapes. +CONSTANTS NumGraphs = 4 ScanDepth = 2 +SPECIFICATION Spec +INVARIANT TypeOK +INVARIANT KickoffAlwaysCovered diff --git a/node/tla/VerifierKickoffFailOpen.cfg b/node/tla/VerifierKickoffFailOpen.cfg new file mode 100644 index 00000000..c8f239c0 --- /dev/null +++ b/node/tla/VerifierKickoffFailOpen.cfg @@ -0,0 +1,8 @@ +\* Models the CURRENT gc-v2 code (issue #429): the verifier consumes the +\* KickoffSent message and skips the Challenge when GOAT SPV lags the kickoff +\* height, with no defer/retry - expected to FAIL (fail-open). This is a live +\* bug, not a historical artifact. +SPECIFICATION FairSpec +CHECK_DEADLOCK FALSE +INVARIANT TypeOK +INVARIANT NoUnauthorizedTake1 diff --git a/node/tla/VerifierKickoffFailOpen.tla b/node/tla/VerifierKickoffFailOpen.tla new file mode 100644 index 00000000..30bdcf9a --- /dev/null +++ b/node/tla/VerifierKickoffFailOpen.tla @@ -0,0 +1,136 @@ +---- MODULE VerifierKickoffFailOpen ---- +(***************************************************************************) +(* Model of GOATNetwork/bitvm-node issue #429: *) +(* "[Security] Verifier KickoffSent challenge is one-shot and fail-open *) +(* (unauthorized Take1)" - checked on gc-v2 @ f2f0285e. *) +(* *) +(* BRANCH STATUS: dev (gc-v2) IS the default/shipping branch and it *) +(* CONTAINS this bug - verified live at handle.rs handle_kickoff_sent_ *) +(* verifier (the goat_confirmed_btc_height SPV-lag branch returns Ok(()) *) +(* with no push_local_unhandled; should_always_challenge is never called; *) +(* detect_kickoff only scans OperatorDataPushed). The stale origin/HEAD *) +(* points at main (d74bf3c, 218 commits behind), whose older Actor:: *) +(* Challenger KickoffSent handler defers via save_unhandle_message and *) +(* calls should_challenge - i.e. main lacks this code path; it is a *) +(* gc-v2 regression that is live on the branch actually shipped. *) +(* *) +(* Threat: an operator broadcasts a kickoff with NO L2 initWithdraw (no *) +(* pegBTC burned). The automated defense is the verifier's *) +(* handle_kickoff_sent_verifier (node/src/handle.rs): if the L2 withdraw *) +(* status for the graph is None/Canceled, it must broadcast a Challenge, *) +(* forcing the operator off the uncontested Take1 fast-exit. *) +(* *) +(* THE BUG (node/src/handle.rs handle_kickoff_sent_verifier): *) +(* *) +(* if [None, Canceled].contains(&withdraw_status) { *) +(* if kickoff_height >= goat_confirmed_btc_height { *) +(* tracing::warn!(...); return Ok(()); // <-- NO defer/retry *) +(* } else { send_challenge_tx(...); } *) +(* } *) +(* *) +(* At first confirmation GOAT's SPV view lags the Bitcoin tip, so *) +(* `kickoff_height >= goat_confirmed_btc_height` is the COMMON case (and, *) +(* because the check is a strict `>` on the send side, it also skips when *) +(* SPV == kickoff_height). On that branch the handler returns Ok(()) *) +(* WITHOUT push_local_unhandled_messages_with_reason, so node/src/action.rs*) +(* marks the KickoffSent message `Processed`. Nothing re-enqueues it: *) +(* detect_kickoff (graph_maintenance_tasks.rs) only scans OperatorDataPushed*) +(* graphs, and upsert_message(is_update=false) will not recreate *) +(* `{graph_id}_KickoffSent`. So every online honest verifier processes *) +(* once, skips, and is done. After the ConnectorA CSV the operator signs *) +(* Take1 (n-of-n pre-signed on connector_0) and exits - pegBTC never *) +(* burned. handle_kickoff_sent_committee DOES defer the same SPV lag; the *) +(* verifier does not. *) +(* *) +(* This is the classic "consume-without-retry on a transient guard" fail- *) +(* open, the same shape as MessageStateRace but on the Challenge defense. *) +(* NOT #418 (the Take1/Challenge CSV margin) - per the issue, the scripts *) +(* are fine IF a Challenge is actually sent; the defect is that it is *) +(* never sent. So this spec abstracts the CSV margin as adequate and *) +(* checks only the control-flow question: does the Challenge ever fire *) +(* before the operator's uncontested Take1? *) +(***************************************************************************) + +MsgStates == {"Pending", "Processed"} + +VARIABLES + msg, \* local-queue state of the {graph_id}_KickoffSent message + spvLags, \* kickoff_height >= goat_confirmed_btc_height (GOAT SPV not strictly past the kickoff) + challengeSent, \* verifier broadcast send_challenge_tx for this unauthorized kickoff + take1 \* operator completed the uncontested Take1 (unauthorized withdrawal) + +vars == <> + +TypeOK == + /\ msg \in MsgStates + /\ spvLags \in BOOLEAN + /\ challengeSent \in BOOLEAN + /\ take1 \in BOOLEAN + +\* detect_kickoff enqueued KickoffSent to Actor::All; at first confirm GOAT +\* SPV lags the Bitcoin tip (the common case, and the == case the strict `>` +\* also skips); withdraw status for this graph is the unauthorized None. +Init == + /\ msg = "Pending" + /\ spvLags = TRUE + /\ challengeSent = FALSE + /\ take1 = FALSE + +-------------------------------------------------------------------------- +\* GOAT SPV eventually catches up to the already-confirmed kickoff (the lag +\* always closes with time). +SpvCatchesUp == + /\ spvLags + /\ spvLags' = FALSE + /\ UNCHANGED <> + +\* BUGGY handle_kickoff_sent_verifier: consumes the message either way. When +\* SPV still lags it returns Ok(()) with no defer -> Processed, NO challenge; +\* only when SPV is strictly past does it send the Challenge. +VerifierProcessBuggy == + /\ msg = "Pending" + /\ msg' = "Processed" + /\ challengeSent' = (IF spvLags THEN challengeSent ELSE TRUE) + /\ UNCHANGED <> + +\* FIXED (issue's suggested fix): on None/Canceled while SPV is not strictly +\* past the kickoff, push_local_unhandled_messages_with_reason - i.e. DEFER, +\* leaving the message Pending to be retried - so the verifier only finalises +\* the message once SPV has caught up and the Challenge is actually sent. +VerifierProcessFixed == + /\ msg = "Pending" + /\ ~spvLags + /\ msg' = "Processed" + /\ challengeSent' = TRUE + /\ UNCHANGED <> + +\* After the ConnectorA CSV the operator broadcasts Take1. It is an +\* unauthorized withdrawal only if no Challenge was ever sent (a sent +\* Challenge forces the long dispute path; per the issue the CSV margin is +\* adequate once the Challenge fires). The verifier's one-shot handling has +\* run to a final decision by the time Take1 is spendable (msg = Processed). +OperatorTake1 == + /\ msg = "Processed" + /\ ~challengeSent + /\ ~take1 + /\ take1' = TRUE + /\ UNCHANGED <> + +Next == SpvCatchesUp \/ VerifierProcessBuggy \/ OperatorTake1 +NextFixed == SpvCatchesUp \/ VerifierProcessFixed \/ OperatorTake1 + +Spec == Init /\ [][Next]_vars +FairSpec == Spec /\ WF_vars(Next) +SpecFixed == Init /\ [][NextFixed]_vars +FairSpecFixed == SpecFixed /\ WF_vars(NextFixed) + +-------------------------------------------------------------------------- +\* Safety (fail-open check): an unauthorized kickoff must never reach a +\* completed Take1 without the verifier's Challenge defense having fired. +\* Buggy: violated - process while SPV lags -> Processed, no Challenge, +\* never retried -> Take1. Fixed: holds - the message is deferred until the +\* Challenge is sent, so Take1's guard (Processed /\ ~challengeSent) is +\* never reachable. +NoUnauthorizedTake1 == take1 => challengeSent + +==== diff --git a/node/tla/VerifierKickoffFailOpenFixed.cfg b/node/tla/VerifierKickoffFailOpenFixed.cfg new file mode 100644 index 00000000..d2d7e82c --- /dev/null +++ b/node/tla/VerifierKickoffFailOpenFixed.cfg @@ -0,0 +1,7 @@ +\* The issue's suggested fix: defer (push_local_unhandled_messages_with_reason) +\* while SPV lags, so the Challenge is retried and actually sent before the +\* operator's Take1 - expected to PASS. +SPECIFICATION FairSpecFixed +CHECK_DEADLOCK FALSE +INVARIANT TypeOK +INVARIANT NoUnauthorizedTake1 From 68832fb38ba34dac94c56c858c60d06e310a08bf Mon Sep 17 00:00:00 2001 From: eigmax Date: Thu, 27 Aug 2026 14:00:53 +0000 Subject: [PATCH 2/4] ci: run TLA+ check on every PR; add issue #429/#431 specs to the gate - pull_request trigger now runs on ANY base branch (was main/dev/gc-v2), so the tla-plus gate (and the CI behind it) runs on every PR. - must-pass step now also runs VerifierKickoffFailOpenFixed (#429 fix design) and KickoffScanCoverageFixed (#431 shipped fix) - both must pass. - bug-reproduction step now also tracks VerifierKickoffFailOpen (#429, LIVE), KickoffScanCoverage (#431, fixed by #451), and KickoffScanCoverageResidual (#431 depth-cap residual) as reproduction pointers; an unexpected PASS on any still fails the job as a drift signal. - reproduction-step summary reworded: the list is no longer all-fixed-by-991faaa. Verified locally: must-pass step exits 0 (11 specs), bug step exits 0 (all reproduce, no drift). --- .github/workflows/ci.yml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 65ed43d2..9e1beebe 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,11 +7,9 @@ on: - dev tags: - v[0-9]+.* + # Run on every pull request regardless of base branch, so the TLA+ formal- + # verification gate (and the rest of CI behind it) runs on ANY PR. pull_request: - branches: - - main - - dev - - gc-v2 env: CARGO_TERM_COLOR: always @@ -69,6 +67,10 @@ jobs: java -jar "$JAR" -config InstanceBridgeOutRaceFixed.cfg InstanceBridgeOutRace.tla java -jar "$JAR" -config MessageStateRaceFixed.cfg MessageStateRace.tla java -jar "$JAR" -config Take1ChallengeRaceFixed.cfg Take1ChallengeRace.tla + # Issue #429 fix design (defer/retry) and issue #431 shipped fix + # (scan_kickoff_chain, adequate depth) - must pass. + java -jar "$JAR" -config VerifierKickoffFailOpenFixed.cfg VerifierKickoffFailOpen.tla + java -jar "$JAR" -config KickoffScanCoverageFixed.cfg KickoffScanCoverage.tla # This job's earlier design (while all 8 findings from this round were # still genuinely unfixed) made this step - and everything gated # behind it - fail for as long as any bug config still reproduced its @@ -93,12 +95,14 @@ jobs: run: | JAR=~/.local/share/tlaplus/tla2tools.jar { - echo "## TLA+ audit: historical bug-reproduction specs" + echo "## TLA+ audit: bug-reproduction specs" echo - echo "These model the PRE-FIX code as a permanent historical record (all" - echo "findings below were fixed in commit 991faaa - see" - echo "\`audit/TLAPlus-20260630.md\`). Still correctly reproducing their" - echo "original counterexample below is expected and does not fail this job." + echo "Each spec below models a known defect. Most are historical (fixed:" + echo "Findings 1-9 in commit 991faaa; issue #431 in #451). Some are still" + echo "LIVE (issue #429; the #431 depth-cap residual). Correctly reproducing" + echo "the counterexample is EXPECTED and does NOT fail this job - it is a" + echo "reproduction pointer; only an unexpected PASS (drift) fails. See" + echo "\`audit/TLAPlus-20260630.md\` and issues #429/#431." echo } >> "$GITHUB_STEP_SUMMARY" while IFS='|' read -r cfg tla finding; do @@ -116,6 +120,9 @@ jobs: InstanceBridgeOutRace.cfg|InstanceBridgeOutRace.tla|Finding 6: InstanceBridgeOutStatus resurrection MessageStateRace.cfg|MessageStateRace.tla|Finding 7: MessageState resurrection Take1ChallengeRace.cfg|Take1ChallengeRace.tla|Finding 9: connector_a has no margin check + VerifierKickoffFailOpen.cfg|VerifierKickoffFailOpen.tla|Issue #429: verifier KickoffSent challenge is one-shot & fail-open (LIVE on dev - defense skipped on SPV lag, never retried) + KickoffScanCoverage.cfg|KickoffScanCoverage.tla|Issue #431: detect_kickoff one-per-operator coverage gap (fixed on dev by #451; kept as historical record) + KickoffScanCoverageResidual.cfg|KickoffScanCoverage.tla|Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 scan-depth cap still leaves a deeper decoy chain uncovered BUGS fmt: name: Rustfmt From 6df27668e1f05a85a70d42b0ae9bcbcf95ef5c52 Mon Sep 17 00:00:00 2001 From: eigmax Date: Thu, 27 Aug 2026 15:11:02 +0000 Subject: [PATCH 3/4] ci: generic tier-based TLA+ gate (pass / historical / live) Replace the two ad-hoc TLA+ steps with a single declarative spec table + a generic router. Every spec carries a tier and the script routes by it - no per-issue logic: pass - fix/baseline design; MUST verify clean (else a fix regressed). historical - a bug fixed in code, kept as a frozen regression record; MUST still reproduce its counterexample (an unexpected PASS = spec drift or a reverted fix -> hard fail). live - a known-unfixed bug; while its frozen spec still reproduces the counterexample it is an OPEN finding that BLOCKS merge. Clear it by fixing the code and moving the row's tier to `historical`. Adding any future finding is one row; fixing a live bug is one word. This makes the gate generic for all similar issues instead of hardcoding each one. Current live (blocking) rows: issue #429 (verifier KickoffSent fail-open) and the issue #431 depth-cap residual. All Findings 1-9 and issue #431 are historical (informational). Verified locally: pass specs verify, historical specs reproduce, the 2 live rows are flagged OPEN and the step exits 1 (blocks merge, as intended). --- .github/workflows/ci.yml | 155 ++++++++++++++++++++++----------------- 1 file changed, 86 insertions(+), 69 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9e1beebe..4244f519 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -47,83 +47,100 @@ jobs: mkdir -p ~/.local/share/tlaplus curl -sL -o ~/.local/share/tlaplus/tla2tools.jar \ https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar - # This audit pass proves bugs exist in CURRENT code and proves correct - # fix designs for them - the fixes are NOT yet applied to the Rust code - # (see node/README.md's "Known gap" sections). These configs model the - # verified fix designs (or a baseline that was never buggy) and must - # always pass. See root README.md's "Formal verification (TLA+)" - # section for what each spec covers. - - name: Run baseline + proposed-fix specs (must pass) - working-directory: node/tla - run: | - set -e - JAR=~/.local/share/tlaplus/tla2tools.jar - java -jar "$JAR" -config GraphLifecycleCoreOnly.cfg GraphLifecycle.tla - java -jar "$JAR" -config GraphLifecycleFixed.cfg GraphLifecycle.tla - java -jar "$JAR" -config GraphLifecycleFineGrainedFixed.cfg GraphLifecycleFineGrainedFixed.tla - java -jar "$JAR" -config InstancePresignedFixed.cfg InstancePresigned.tla - java -jar "$JAR" -config Take2DisproveRace.cfg Take2DisproveRace.tla - java -jar "$JAR" -config MultiActorRace.cfg MultiActorRace.tla - java -jar "$JAR" -config InstanceBridgeOutRaceFixed.cfg InstanceBridgeOutRace.tla - java -jar "$JAR" -config MessageStateRaceFixed.cfg MessageStateRace.tla - java -jar "$JAR" -config Take1ChallengeRaceFixed.cfg Take1ChallengeRace.tla - # Issue #429 fix design (defer/retry) and issue #431 shipped fix - # (scan_kickoff_chain, adequate depth) - must pass. - java -jar "$JAR" -config VerifierKickoffFailOpenFixed.cfg VerifierKickoffFailOpen.tla - java -jar "$JAR" -config KickoffScanCoverageFixed.cfg KickoffScanCoverage.tla - # This job's earlier design (while all 8 findings from this round were - # still genuinely unfixed) made this step - and everything gated - # behind it - fail for as long as any bug config still reproduced its - # counterexample. As of commit 991faaa, every one of those findings - # has actually been fixed in the shipped Rust code (see - # audit/TLAPlus-20260630.md) - keeping the job permanently red past - # that point stopped being useful: these bug configs' constants are - # frozen historical snapshots (e.g. Take1ChallengeRace.tla's - # ConnectorA), not live readings of the current Rust source, so they - # can never detect a real code regression by themselves - they will - # keep reproducing the same counterexample forever regardless of - # what the Rust code does. Their only genuine ongoing signal is the - # OPPOSITE direction: if one of them ever unexpectedly STOPS - # reproducing its counterexample, that means the spec itself was - # edited into no longer demonstrating the bug it's supposed to - - # that's the one case this step still treats as a hard failure. - # Otherwise, a bug config correctly still failing is expected and - # does not fail the job - it's just printed as an informational - # reproduction pointer. - - name: Confirm known-bug specs still reproduce their counterexample + # One declarative spec table + a generic router. Each spec carries a + # `tier`: + # pass - a fix/baseline design; MUST verify clean (else a fix + # design regressed). + # historical - a bug already fixed in the code; the frozen spec MUST + # still reproduce its counterexample. An unexpected PASS + # means the spec drifted (no longer demonstrates the bug) + # or a landed fix was reverted -> hard fail. + # live - a known-unfixed bug; while its spec still reproduces the + # counterexample it is an OPEN finding that BLOCKS merge. + # To clear it: fix the code, then change its tier to + # `historical` here (the spec is frozen and cannot detect + # the code fix on its own). + # Adding any future finding is one row; that is the whole maintenance + # surface. No per-issue logic lives in the script below. + - name: TLA+ formal verification (verify fixes, reproduce fixed bugs, block live ones) working-directory: node/tla run: | + set -u JAR=~/.local/share/tlaplus/tla2tools.jar + live_open=0 { - echo "## TLA+ audit: bug-reproduction specs" + echo "## TLA+ formal verification" echo - echo "Each spec below models a known defect. Most are historical (fixed:" - echo "Findings 1-9 in commit 991faaa; issue #431 in #451). Some are still" - echo "LIVE (issue #429; the #431 depth-cap residual). Correctly reproducing" - echo "the counterexample is EXPECTED and does NOT fail this job - it is a" - echo "reproduction pointer; only an unexpected PASS (drift) fails. See" - echo "\`audit/TLAPlus-20260630.md\` and issues #429/#431." + echo "Specs routed by \`tier\`: **pass** (fix/baseline, must verify), **historical**" + echo "(fixed bug, must still reproduce its counterexample or it drifted), **live**" + echo "(unfixed bug - blocks merge until the code is fixed and the row moved to historical)." echo } >> "$GITHUB_STEP_SUMMARY" - while IFS='|' read -r cfg tla finding; do - [ -z "$cfg" ] && continue - if java -jar "$JAR" -config "$cfg" "$tla" | grep -q "Model checking completed. No error has been found."; then - echo "::error::$tla / $cfg was expected to keep reproducing its historical counterexample but passed instead - the spec itself was likely edited into no longer demonstrating the bug it's supposed to. If the underlying Rust fix was somehow reverted, this is also how you'd find out - either way, investigate before trusting this spec again." - exit 1 - fi + # verifies CFG TLA -> true iff TLC reports no violation (spec holds) + verifies() { java -jar "$JAR" -config "$1" "$2" 2>/dev/null | grep -q "Model checking completed. No error has been found."; } + while IFS='|' read -r tier cfg tla desc; do + tier="$(echo "$tier" | tr -d '[:space:]')" + cfg="$(echo "$cfg" | tr -d '[:space:]')" + tla="$(echo "$tla" | tr -d '[:space:]')" + desc="$(echo "$desc" | sed 's/^ *//; s/ *$//')" + [ -z "$tier" ] && continue + case "$tier" in \#*) continue ;; esac repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla" - echo "- **$finding** - reproduce: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" - done <<'BUGS' - GraphLifecycle.cfg|GraphLifecycle.tla|Finding 1: Graph.status race - GraphLifecycleFineGrained.cfg|GraphLifecycleFineGrained.tla|Finding 1b: naive guard still unsafe - InstancePresignedBug.cfg|InstancePresigned.tla|Finding 2: Instance.status regression past Presigned - InstanceBridgeOutRace.cfg|InstanceBridgeOutRace.tla|Finding 6: InstanceBridgeOutStatus resurrection - MessageStateRace.cfg|MessageStateRace.tla|Finding 7: MessageState resurrection - Take1ChallengeRace.cfg|Take1ChallengeRace.tla|Finding 9: connector_a has no margin check - VerifierKickoffFailOpen.cfg|VerifierKickoffFailOpen.tla|Issue #429: verifier KickoffSent challenge is one-shot & fail-open (LIVE on dev - defense skipped on SPV lag, never retried) - KickoffScanCoverage.cfg|KickoffScanCoverage.tla|Issue #431: detect_kickoff one-per-operator coverage gap (fixed on dev by #451; kept as historical record) - KickoffScanCoverageResidual.cfg|KickoffScanCoverage.tla|Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 scan-depth cap still leaves a deeper decoy chain uncovered - BUGS + if verifies "$cfg" "$tla"; then result=pass; else result=violation; fi + case "$tier" in + pass) + if [ "$result" != pass ]; then + echo "::error::[pass] $cfg / $tla did NOT verify - a fix or baseline design regressed. Repro: $repro" + exit 1 + fi + echo "- **[verified] $desc**" >> "$GITHUB_STEP_SUMMARY" ;; + historical) + if [ "$result" = pass ]; then + echo "::error::[historical] $cfg / $tla unexpectedly PASSED - the spec drifted (no longer demonstrates its fixed bug) or a landed fix was reverted. Investigate. Repro: $repro" + exit 1 + fi + echo "- **[fixed] $desc** - still reproduces (regression record). Repro: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" ;; + live) + if [ "$result" = pass ]; then + echo "::warning::[live] $cfg / $tla no longer reproduces - if you fixed the code, move its tier to 'historical'. Repro: $repro" + echo "- **[live?] $desc** - no longer reproducing (fixed? move to historical)" >> "$GITHUB_STEP_SUMMARY" + else + echo "::error::OPEN BUG (blocks merge): $desc - repro: $repro" + echo "- **[OPEN - blocks merge] $desc** - repro: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" + live_open=$((live_open + 1)) + fi ;; + *) echo "::error::unknown tier '$tier' for $cfg (use pass|historical|live)"; exit 1 ;; + esac + done <<'SPECS' + pass | GraphLifecycleCoreOnly.cfg | GraphLifecycle.tla | baseline chain-scan state machine is sound + pass | GraphLifecycleFixed.cfg | GraphLifecycle.tla | Finding 1 fix - atomic guard closes Graph.status race + pass | GraphLifecycleFineGrainedFixed.cfg | GraphLifecycleFineGrainedFixed.tla | Finding 1b fix - single-statement atomic CAS + pass | InstancePresignedFixed.cfg | InstancePresigned.tla | Finding 2 fix - Instance.status regression guarded + pass | Take2DisproveRace.cfg | Take2DisproveRace.tla | Finding 4 - Take2 vs Disprove margin holds (real shipped values) + pass | MultiActorRace.cfg | MultiActorRace.tla | Finding 5/10 - 1-of-N watchtower/verifier + operator_commit margin + pass | InstanceBridgeOutRaceFixed.cfg | InstanceBridgeOutRace.tla | Finding 6 fix - terminal-status guard closes resurrection + pass | MessageStateRaceFixed.cfg | MessageStateRace.tla | Finding 7 fix - terminal-guarded resurrect + pass | Take1ChallengeRaceFixed.cfg | Take1ChallengeRace.tla | Finding 9 fix - connector_a margin check added + pass | VerifierKickoffFailOpenFixed.cfg | VerifierKickoffFailOpen.tla | Issue #429 fix design - defer/retry mirrors committee + pass | KickoffScanCoverageFixed.cfg | KickoffScanCoverage.tla | Issue #431 fix - scan_kickoff_chain with adequate depth + historical | GraphLifecycle.cfg | GraphLifecycle.tla | Finding 1: Graph.status race (fixed 991faaa) + historical | GraphLifecycleFineGrained.cfg | GraphLifecycleFineGrained.tla | Finding 1b: naive guard still unsafe (fixed 991faaa) + historical | InstancePresignedBug.cfg | InstancePresigned.tla | Finding 2: Instance.status regression past Presigned (fixed 991faaa) + historical | InstanceBridgeOutRace.cfg | InstanceBridgeOutRace.tla | Finding 6: InstanceBridgeOutStatus resurrection (fixed 991faaa) + historical | MessageStateRace.cfg | MessageStateRace.tla | Finding 7: MessageState resurrection (fixed 991faaa) + historical | Take1ChallengeRace.cfg | Take1ChallengeRace.tla | Finding 9: connector_a has no margin check (fixed 991faaa) + historical | KickoffScanCoverage.cfg | KickoffScanCoverage.tla | Issue #431: detect_kickoff one-per-operator coverage gap (fixed by #451) + live | VerifierKickoffFailOpen.cfg | VerifierKickoffFailOpen.tla | Issue #429: verifier KickoffSent fail-open (SPV lag skips Challenge, never retried) + live | KickoffScanCoverageResidual.cfg | KickoffScanCoverage.tla | Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 depth cap leaves deeper decoy chains uncovered + SPECS + if [ "$live_open" -gt 0 ]; then + { + echo + echo "**$live_open live, TLA+-proven bug(s) block merge.** Fix the code, then move each row's tier from \`live\` to \`historical\` in .github/workflows/ci.yml. See issues #429 / #431." + } >> "$GITHUB_STEP_SUMMARY" + echo "::error::$live_open live TLA+-proven bug(s) remain unfixed and block merge (see annotations above)." + exit 1 + fi fmt: name: Rustfmt needs: tla-plus From 0582be30738e54d36496d81dcf7646035915ed9a Mon Sep 17 00:00:00 2001 From: eigmax Date: Thu, 27 Aug 2026 17:28:16 +0000 Subject: [PATCH 4/4] ci: run every TLA+ spec and report results dynamically; ungate the jobs - The TLA+ step now runs ALL specs (no early exit on the first failure) and prints a dynamic result table in the job summary - each row shows the spec's actual TLC outcome (verified / counterexample) and a computed status, instead of static pre-written labels. It accumulates failures and exits 1 at the end if any (still blocking merge on live bugs). - Removed `needs: tla-plus` from fmt/clippy/test so every check runs on every PR in parallel, regardless of the TLA+ outcome. tla-plus is now a first-class parallel check rather than a hard gate that skips the others. Verified locally: all 20 specs run, table renders, 2 live bugs -> exit 1. --- .github/workflows/ci.yml | 81 ++++++++++++++++++---------------------- 1 file changed, 36 insertions(+), 45 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4244f519..0213728c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -19,20 +19,12 @@ concurrency: cancel-in-progress: true jobs: - # Runs first and gates everything else (fmt/clippy/test all `needs: tla-plus` - # below) - it's the fastest job (seconds, no Rust toolchain to build) and a - # failure here means either a real regression the other, much slower jobs - # can't catch, or a stale/broken spec - either way not worth burning 30+ - # minutes of Cargo Test/Clippy compute on before finding out. - # - # All 8 findings from audit/TLAPlus-20260630.md were fixed in commit - # 991faaa, so this job is expected to be GREEN. Its steps still run every - # bug config that reproduced the original counterexamples, but a bug - # config correctly still failing is no longer treated as a job failure - - # see the second step's own comment for why (its constants are frozen - # historical snapshots, not a live read of the Rust source, so they can't - # detect a regression by staying red; only an unexpected PASS is a real - # drift signal now). + # Runs independently and in parallel with fmt/clippy/test (no `needs:` gating) + # so EVERY check runs on every PR regardless of the others' outcome. It is a + # first-class check: it fails (and blocks merge, if branch protection requires + # it) whenever a `live` bug spec still reproduces its counterexample. See the + # step below - it runs every spec, prints each one's actual TLC result in the + # job summary, and routes by tier (pass / historical / live). tla-plus: name: TLA+ Formal Verification runs-on: ubuntu-latest @@ -67,16 +59,19 @@ jobs: run: | set -u JAR=~/.local/share/tlaplus/tla2tools.jar + hard_fail=0 live_open=0 { echo "## TLA+ formal verification" echo - echo "Specs routed by \`tier\`: **pass** (fix/baseline, must verify), **historical**" - echo "(fixed bug, must still reproduce its counterexample or it drifted), **live**" - echo "(unfixed bug - blocks merge until the code is fixed and the row moved to historical)." + echo "Every spec is run and its live TLC result reported below. Tiers:" + echo "**pass** must verify; **historical** (fixed bug) must still reproduce" + echo "its counterexample; **live** (unfixed bug) blocks merge while it does." echo + echo "| Spec | Tier | TLC result | Status |" + echo "|---|---|---|---|" } >> "$GITHUB_STEP_SUMMARY" - # verifies CFG TLA -> true iff TLC reports no violation (spec holds) + # true iff TLC reports the spec holds (no violation found) verifies() { java -jar "$JAR" -config "$1" "$2" 2>/dev/null | grep -q "Model checking completed. No error has been found."; } while IFS='|' read -r tier cfg tla desc; do tier="$(echo "$tier" | tr -d '[:space:]')" @@ -86,31 +81,30 @@ jobs: [ -z "$tier" ] && continue case "$tier" in \#*) continue ;; esac repro="cd node/tla && java -jar ~/.local/share/tlaplus/tla2tools.jar -config $cfg $tla" - if verifies "$cfg" "$tla"; then result=pass; else result=violation; fi + # run the check - never short-circuit; record the real outcome + if verifies "$cfg" "$tla"; then tlc="verified (no violation)"; ok=1; else tlc="counterexample found"; ok=0; fi case "$tier" in pass) - if [ "$result" != pass ]; then - echo "::error::[pass] $cfg / $tla did NOT verify - a fix or baseline design regressed. Repro: $repro" - exit 1 - fi - echo "- **[verified] $desc**" >> "$GITHUB_STEP_SUMMARY" ;; + if [ "$ok" = 1 ]; then status="OK"; else + status="REGRESSED - fix/baseline no longer verifies"; hard_fail=$((hard_fail+1)) + echo "::error::[pass] $cfg / $tla did NOT verify ($desc). Repro: $repro" + fi ;; historical) - if [ "$result" = pass ]; then - echo "::error::[historical] $cfg / $tla unexpectedly PASSED - the spec drifted (no longer demonstrates its fixed bug) or a landed fix was reverted. Investigate. Repro: $repro" - exit 1 - fi - echo "- **[fixed] $desc** - still reproduces (regression record). Repro: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" ;; + if [ "$ok" = 0 ]; then status="OK - reproduces (regression record)"; else + status="DRIFT - no longer reproduces (spec edited or fix reverted)"; hard_fail=$((hard_fail+1)) + echo "::error::[historical] $cfg / $tla unexpectedly verified ($desc) - investigate drift/revert. Repro: $repro" + fi ;; live) - if [ "$result" = pass ]; then - echo "::warning::[live] $cfg / $tla no longer reproduces - if you fixed the code, move its tier to 'historical'. Repro: $repro" - echo "- **[live?] $desc** - no longer reproducing (fixed? move to historical)" >> "$GITHUB_STEP_SUMMARY" + if [ "$ok" = 0 ]; then + status="OPEN - blocks merge"; live_open=$((live_open+1)); hard_fail=$((hard_fail+1)) + echo "::error::OPEN BUG (blocks merge): $desc. Repro: $repro" else - echo "::error::OPEN BUG (blocks merge): $desc - repro: $repro" - echo "- **[OPEN - blocks merge] $desc** - repro: \`$repro\`" >> "$GITHUB_STEP_SUMMARY" - live_open=$((live_open + 1)) + status="review - no longer reproduces; if fixed, move tier to historical" + echo "::warning::[live] $cfg / $tla no longer reproduces ($desc) - move its tier to 'historical' if the code is fixed. Repro: $repro" fi ;; - *) echo "::error::unknown tier '$tier' for $cfg (use pass|historical|live)"; exit 1 ;; + *) status="UNKNOWN TIER"; hard_fail=$((hard_fail+1)); echo "::error::unknown tier '$tier' for $cfg (use pass|historical|live)" ;; esac + echo "| \`$tla\` (\`$cfg\`) | $tier | $tlc | $status - $desc |" >> "$GITHUB_STEP_SUMMARY" done <<'SPECS' pass | GraphLifecycleCoreOnly.cfg | GraphLifecycle.tla | baseline chain-scan state machine is sound pass | GraphLifecycleFixed.cfg | GraphLifecycle.tla | Finding 1 fix - atomic guard closes Graph.status race @@ -133,17 +127,16 @@ jobs: live | VerifierKickoffFailOpen.cfg | VerifierKickoffFailOpen.tla | Issue #429: verifier KickoffSent fail-open (SPV lag skips Challenge, never retried) live | KickoffScanCoverageResidual.cfg | KickoffScanCoverage.tla | Issue #431 residual: MAX_PREKICKOFF_SUCCESSORS_PER_SCAN=32 depth cap leaves deeper decoy chains uncovered SPECS - if [ "$live_open" -gt 0 ]; then - { - echo - echo "**$live_open live, TLA+-proven bug(s) block merge.** Fix the code, then move each row's tier from \`live\` to \`historical\` in .github/workflows/ci.yml. See issues #429 / #431." - } >> "$GITHUB_STEP_SUMMARY" - echo "::error::$live_open live TLA+-proven bug(s) remain unfixed and block merge (see annotations above)." + { + echo + echo "**Result: $hard_fail check(s) failing, $live_open live bug(s) open.**" + } >> "$GITHUB_STEP_SUMMARY" + if [ "$hard_fail" -gt 0 ]; then + echo "::error::$hard_fail TLA+ check(s) failed ($live_open live bug(s) block merge). See the result table in the job summary." exit 1 fi fmt: name: Rustfmt - needs: tla-plus runs-on: ubuntu-latest steps: - uses: actions/checkout@v5 @@ -160,7 +153,6 @@ jobs: args: --all -- --check clippy: name: Clippy - needs: tla-plus runs-on: ubuntu-latest steps: - uses: actions/checkout@v5 @@ -179,7 +171,6 @@ jobs: cargo clippy --all-targets -- -D warnings test: name: Cargo Test - needs: tla-plus runs-on: ubuntu-latest strategy: matrix: