Conversation
There was a problem hiding this comment.
Pull request overview
This PR fixes the CircuitRegistration TLA+ spec so TLC can actually evaluate the invariant referenced by its .cfg, and wires that spec into the existing F# TLC test runner so the fix is exercised in CI. It fits the repo’s formal-verification suite by moving one previously broken deferred spec into the checked set.
Changes:
- Define
SafetyinCircuitRegistration.tlasoCircuitRegistration.cfgno longer points at an undefined invariant. - Update the TLC runner comments to reflect CircuitRegistration’s fixed status.
- Add a new xUnit TLC test for
CircuitRegistrationso CI validates the spec.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
tools/tla/specs/CircuitRegistration.tla |
Adds the missing Safety operator required by the TLC config. |
tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs |
Updates verification notes and adds a TLC test for CircuitRegistration. |
Merged
2 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…6-05-03 EOD progress (#1402) Reflects substantive progress this session across the math-proofs honest assessment matrix. Key state changes: **P0 items — 3 of 3 closed:** - Lean lake-build CI job ✓ (#1394) - A4 registry rows ✓ (#1393) - Peer-review email draft ✓ (#1387) - Stryker B3 → partial (config-fix #1395; CI wire deferred to follow-up substantial-design) **P1 items — significant progress:** - Alloy B2 → A ✓ (#1396 — silent-no-op was the failure mode; spec-path fixed) - Semgrep B4 → A ✓ (verify-then-claim correction; was already in CI) - B1 4 deferred specs → 2 of 4 done: - DbspSpec ✓ #1397 (1M states / 11s) - CircuitRegistration ✓ #1401 (B-0180 closed; 3538 states / <1s) - SpineAsyncProtocol B-0179 still open (counterexample inv.) - SpineMergeInvariants B-0181 still open (counterexample inv.) **Sibling work tracked:** - Phase 0 substrate-discovery PoC ✓ (#1392 — 4.0 MB AOT binary on osx-arm64; cross-platform CI matrix) - 3 broken-spec backlog rows filed (#1398 → B-0179 + B-0180 + B-0181); B-0180 closed (#1401) - `.ts/.sh` parity bug in `tools/backlog/generate-index.ts` closed ✓ (#1400 — both generators byte-identical) This update is bounded substrate work documenting the actual state of the matrix; doesn't add new work, just captures completion. Future matrix re-grades happen as work-items land (per the assessment doc's audit-trail discipline). Composes with #1383 (the original assessment) + every PR referenced above. §33 archive-header lint passes.
3 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…bering source-controlled specs (#1403) The cache for `tools/tla` + `tools/alloy` was caching ENTIRE directories, including source-controlled spec files (`tools/tla/specs/*.tla` / `*.cfg`, `tools/alloy/specs/*.als`, `tools/alloy/AlloyRunner.java`). On cache hit, actions/cache restored the cached versions, OVERWRITING the freshly-checked-out PR-modified specs. **Failure mode (silent + invisible):** PR edits to spec files were reverted by cache restoration. CI ran the OLD spec text but reported it as the new test result. The "PR's fix" was never actually checked. **Surfaced by:** PR #1401's CircuitRegistration `Safety` invariant fix passes locally (`Model checking completed. No error has been found.` 3538 states / depth 14) but failed on CI with the exact pre-fix error (`Error: The invariant Safety specified in the configuration file is not defined in the specification.`). Diff: local ran the fixed spec; CI ran the cache-restored old spec. **Fix:** 1. Narrow cache path to specific jar files only (`tools/tla/ tla2tools.jar`, `tools/alloy/alloy.jar`) 2. Bump cache key suffix to `-v2` to bust the existing stale cache (otherwise the new path config wouldn't apply until the manifest hash changed) **Why this is the right scope:** - Jars are the only intended artifact (per the existing comment "Jars are JVM bytecode so arch-neutral") - Source-controlled spec files are tracked in git; checkout provides the canonical version - Compiled `AlloyRunner.class` regenerates fast; not worth caching **Latent risk before this fix:** EVERY PR that modified specs/ silently failed to actually test its changes. The test report would show the OLD spec passing. This is a discovery-by-luck class — only surfaced when a PR introduced a NEW invariant referenced by the cfg, because then the test FAILED instead of silently passing on stale state. Composes with: - #1401 (the CircuitRegistration Safety fix that surfaced this) - B-0180 (the backlog row #1401 closes; will become unblockable once this cache fix lands and the cache busts) - The math-proofs assessment (test-fidelity is fundamental to the A/B/C grading; a clobbered cache means tests don't actually run the spec they claim to)
…egister in CI Per B-0180 (filed in #1398) — `CircuitRegistration.cfg` referenced `INVARIANT Safety` but the spec didn't define a `Safety` operator, causing TLC to error out: Error: The invariant Safety specified in the configuration file is not defined in the specification. The intended composite invariant is documented at the bottom of the spec via the THEOREM `Spec => [](TypeOK /\ NoRegisterAfterBuild)`. Defined `Safety` as exactly that conjunction so the cfg directive resolves without changing TLC's check semantics. **Local verification:** - `java -cp tools/tla/tla2tools.jar tlc2.TLC -workers 4 -config tools/tla/specs/CircuitRegistration.cfg tools/tla/specs/CircuitRegistration.tla` → "Model checking completed. No error has been found." 3538 distinct states explored, depth 14, <1s wall. - `dotnet test --filter "FullyQualifiedName~CircuitRegistration"` passes in 1.7s. **Composes with:** - B-0180 (the backlog row this closes; one of 3 broken-spec follow-ups from #1397's verify-then-claim sweep) - #1397 (DbspSpec → CI; the partial-B1 closure) - #1383 math-proofs honest assessment (the matrix this incrementally closes — 2 of 4 deferred B1 specs now in CI; remaining: B-0179 SpineAsyncProtocol + B-0181 SpineMergeInvariants both need counterexample investigation, not config fixes) **Discipline note:** the original spec author left "Safety:" as a prose comment label on `NoRegisterAfterBuild` (line 81) and on `ConnectAtMostOnce` (line 85), implying both were intended as "safety properties" but never finished the operator definition. The THEOREM at line 96 disambiguates: only `TypeOK /\ NoRegisterAfterBuild` belongs in INVARIANT (a state property); `ConnectAtMostOnce` uses `[]_vars` and is a temporal PROPERTY (deferred — not in this fix's scope).
AceHack
force-pushed
the
fix/b0180-circuitregistration-safety-invariant
branch
from
9bfba5b to
43c118d
Compare
…tration test comment Reviewer #1401 caught: the comment said 'per the spec's THEOREM at line ~96' but the actual line drifts as the spec evolves (currently line 106 after my Safety operator addition). Reworded to reference the THEOREM by content rather than line: 'matching the spec's stated THEOREM Spec => [](TypeOK /NoRegisterAfterBuild)'. Doesn't drift, doesn't require maintenance when the spec is edited.
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…-paths.ts`) — Aaron's "make it not lucky next time" **Two parts** addressing the silent CI cache-clobber bug discovered via #1401's CircuitRegistration test failure: ## Part 1 — `.github/workflows/low-memory.yml` cache fix Same broad-path bug as gate.yml (#1403 fixes that one): cache path `tools/tla` + `tools/alloy` overwrites source-controlled spec files on cache hit. Narrowed to specific jar files only; bumped key suffix to `-v2` to bust stale cache. Without this fix, low-memory.yml would have the same silent clobber bug as gate.yml had pre-#1403. ## Part 2 — `tools/hygiene/audit-ci-cache-paths.ts` (the not-lucky mechanism) Aaron 2026-05-03: *"lucky catch how can you make it not lucky next time for same class or similar class"* The structural answer: a CI-on-CI audit that flags any `actions/ cache` `path:` in `.github/workflows/*.yml` overlapping with `git ls-files`. The discipline rule: *"actions/cache paths are mutually exclusive with git ls-files — cache only DERIVED files (downloaded jars, built artefacts, user-home tool state), never source-controlled content."* Implementation: - Walks `.github/workflows/*.yml` parsing `path:` blocks (handles both single-line `path: foo` and multi-line `path: |` forms) - For each path, checks if it equals or contains a `git ls-files` entry - Allowlists user-home paths (`~/...`, `/...`) — never tracked - Reports per-violation: workflow + step name + cache path + example tracked file - Includes "Why this is a bug" + "How to fix" output for actionable CI failures **Local verification:** runs against current main (pre-#1403 merge); correctly flags gate.yml's `tools/tla` + `tools/alloy` paths as violations (2). Once #1403 merges + this PR's low-memory.yml fix lands, the audit returns clean. ## Not-yet-done (follow-up): - Wire the audit into CI as a lint job (after #1403 merges so the audit returns clean as a baseline) - Memory file capturing the full discipline (cache-paths-mutually- exclusive-with-git-ls-files) This PR ships the *tool*; the CI wire-up is a deliberate follow-up PR so the lint-job-add can land cleanly on a green baseline. Composes with: - #1401 (CircuitRegistration Safety fix that surfaced this) - #1403 (gate.yml cache fix; sibling of low-memory.yml fix here) - #1383 math-proofs honest assessment (test-fidelity is fundamental to A/B/C grading)
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…e it not lucky next time") (#1404) * fix(ci): low-memory.yml cache fix + structural audit (`audit-ci-cache-paths.ts`) — Aaron's "make it not lucky next time" **Two parts** addressing the silent CI cache-clobber bug discovered via #1401's CircuitRegistration test failure: ## Part 1 — `.github/workflows/low-memory.yml` cache fix Same broad-path bug as gate.yml (#1403 fixes that one): cache path `tools/tla` + `tools/alloy` overwrites source-controlled spec files on cache hit. Narrowed to specific jar files only; bumped key suffix to `-v2` to bust stale cache. Without this fix, low-memory.yml would have the same silent clobber bug as gate.yml had pre-#1403. ## Part 2 — `tools/hygiene/audit-ci-cache-paths.ts` (the not-lucky mechanism) Aaron 2026-05-03: *"lucky catch how can you make it not lucky next time for same class or similar class"* The structural answer: a CI-on-CI audit that flags any `actions/ cache` `path:` in `.github/workflows/*.yml` overlapping with `git ls-files`. The discipline rule: *"actions/cache paths are mutually exclusive with git ls-files — cache only DERIVED files (downloaded jars, built artefacts, user-home tool state), never source-controlled content."* Implementation: - Walks `.github/workflows/*.yml` parsing `path:` blocks (handles both single-line `path: foo` and multi-line `path: |` forms) - For each path, checks if it equals or contains a `git ls-files` entry - Allowlists user-home paths (`~/...`, `/...`) — never tracked - Reports per-violation: workflow + step name + cache path + example tracked file - Includes "Why this is a bug" + "How to fix" output for actionable CI failures **Local verification:** runs against current main (pre-#1403 merge); correctly flags gate.yml's `tools/tla` + `tools/alloy` paths as violations (2). Once #1403 merges + this PR's low-memory.yml fix lands, the audit returns clean. ## Not-yet-done (follow-up): - Wire the audit into CI as a lint job (after #1403 merges so the audit returns clean as a baseline) - Memory file capturing the full discipline (cache-paths-mutually- exclusive-with-git-ls-files) This PR ships the *tool*; the CI wire-up is a deliberate follow-up PR so the lint-job-add can land cleanly on a green baseline. Composes with: - #1401 (CircuitRegistration Safety fix that surfaced this) - #1403 (gate.yml cache fix; sibling of low-memory.yml fix here) - #1383 math-proofs honest assessment (test-fidelity is fundamental to A/B/C grading) * fix(audit-ci-cache-paths): address 3 review findings on #1404 — absolute paths + glob expansion + read-failure exit Three #1404 reviewer findings addressed: **P1 — Don't exempt absolute paths.** Original code skipped any path starting with `/` as "user-home equivalent". But actions/cache absolute paths can point INTO the checked-out workspace (e.g. `/home/runner/work/<repo>/<repo>/...`) — same clobber failure mode as relative paths. Now `isUserHomePath` returns true only for `~/...`. Comment added at the function explaining the rationale. **P2 — Expand globs before overlap detection.** actions/cache paths can contain wildcards (`*`, `**`, `?`); the original implementation only did exact/prefix string matching, so a glob path like `tools/tla/specs/*.tla` would be considered non-overlapping with any tracked file. Added `globToRegex()` (* matches non-`/`, ** matches anything including `/`, ? matches single non-`/` char, escapes regex meta-chars) and `pathHasGlob()`; `overlapsTrackedFile` now branches on glob-vs-literal and matches accordingly. **P2 — Return exit 2 on workflow read failure.** Documented exit codes promised exit 2 on workflow read failure but the code logged + skipped + still reported "OK" if no other violations. That's exactly the false-pass class the audit was designed to catch. Added `readFailures` counter; returns exit 2 with explicit error message before the violation summary. **Verification post-fix:** - `bun tools/hygiene/audit-ci-cache-paths.ts` → "OK: 12 workflow(s) audited; no cache paths overlap git-tracked files" (returns clean now that #1403 + this PR's low-memory fix have rebased on top of merged main) - All 3 reviewer findings addressed within the same audit tool Composes with: - #1403 (gate.yml cache fix; merged) - #1404 (this PR; low-memory.yml + audit-tool) - The "not-lucky-next-time" structural answer to Aaron's question * fix(audit-ci-cache-paths): address 3 more #1404 review findings — content-shadow rename + repo-root cache-path edge Three additional reviewer findings: **Variable shadowing in parseCachePaths.** Inner shadowed the outer parameter (the workflow YAML text). Renamed inner to (the per-line trimmed value) for clarity. **Repo-root cache-path false-pass.** Cache paths like `.` or `./` normalised to `""` and silently false-passed (no tracked file equals "" or starts with "/"). High-impact bug class — a workflow caching the entire repo root would not be flagged. Added explicit repo-root branch: if cp is "" or "." after normalisation, return the first tracked file (overlap is 100%). **Header-comment claim about glob expansion.** Already addressed in the prior commit (added globToRegex + pathHasGlob); this thread duplicates the P2 finding. Local verification: audit returns clean (12 workflows audited; no overlap).
…structions §282 Reviewer #1401 caught: my CircuitRegistration test comments + the Safety operator's spec comment carried historical narrative (B-0180 ticket ID, #1397 PR ref, 2026-05-03 sweep date, 'Closes 1 of 3 broken sibling specs', 'was missing until B-0180 fixed', etc.) on current-state surfaces. Per .github/copilot-instructions.md §282: *Documentation is current state, not history. Historical narrative lives in docs/ROUND-HISTORY.md and ADRs under docs/DECISIONS/; everywhere else in docs/ edit in place.* Same rule applies to spec files + test comments — they describe what the artifact currently does, not how it got there. Stripped: - Test comments now describe ONLY the current invariants checked + cfg coverage scope + complementary-coverage pointers (no ticket IDs, no dates, no PR refs) - Spec's Safety operator comment now says only what Safety is (composite safety invariant matching the THEOREM) without the B-0180 / 2026-05-03 / verify-then-claim history - Compatible-coverage pointers retained (FsCheck Z-set tests + Lean proof) since those are current-state composes-with refs Build still 0/0; functional behavior unchanged.
2 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…ster + cache-clobber discipline encoded (#1408) Substantial multi-tick session shard. 18 PRs touched (#1383 + #1387 + #1392-#1407 inclusive); 14 merged + 4 in-flight as of shard time. **Math-proofs assessment progress** (#1383 outstanding-work matrix): - A1+A2 → A-with-CI ✓ (#1394 Lean lake-build workflow) - A4 registry rows ✓ (#1393) - B1 → 2 of 4 deferred specs in CI ✓ (#1397 DbspSpec + #1401 CircuitRegistration B-0180 closed) - B2 Alloy → A ✓ (#1396 silent-no-op spec-path fix) - B4 Semgrep → A ✓ (correction) - Peer-review email template ✓ (#1387) - Phase 0 substrate-discovery PoC ✓ (#1392) - Stryker config-fix ✓ (#1395; CI wire deferred) - 3 broken-spec backlog rows filed ✓ (#1398) **Cache-clobber silent-bug class discovered + fully encoded:** B-0180 fix passing locally + failing CI → verify-then-claim identified gate.yml + low-memory.yml caching whole tools/tla and tools/alloy directories. Fix cluster: #1403 (gate.yml) + #1404 (low-memory.yml + audit-ci-cache-paths.ts) + #1406 (CI lint gate) + #1407 (memory file + bug-locus disambiguation per Aaron's 'real github bug?' question — answer: usage-bug, not tool-bug). **Other substrate work:** #1399 BACKLOG.md regen, #1400 .ts/.sh parity bug, #1402 assessment matrix doc update, #1405 B-0182 backlog row (Linux-only formal verification — orthogonal-axes split per Aaron 2026-05-03). **Discipline lessons captured:** chat-is-assertion-channel, substrate-corrections-cluster, search-first-before-architectural- expansion, verify-then-claim CI fidelity, documentation-is- current-state-not-history. Carved sentence: 'When a lucky catch surfaces a class of bug, build the structural fix that eliminates the luck — audit + lint gate + carved-sentence rule + memory file.'
3 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…l counterexample) (#1411) * fix(B-0179): SpineAsyncProtocol — add CHECK_DEADLOCK FALSE; not a real counterexample Per B-0179 verify-then-claim sweep. Re-running TLC on SpineAsyncProtocol revealed: TLC reports "Deadlock reached" at the all-done quiescent state (processed=NumBatches, channel empty, both PCs idle). This is intended termination, not bug-deadlock. Local TLC run before fix: Error: Deadlock reached. 21 states generated, 15 distinct states found, 0 states left on queue. Depth 9. The 3 invariants (InvMonotonic, InvEventuallyDrains, InvFlushTerminates) all hold across all 15 explored states. The ONLY violation is the deadlock-at-terminal warning. Fix: add CHECK_DEADLOCK FALSE to SpineAsyncProtocol.cfg (same pattern as CircuitRegistration.cfg + TwoPCSink.cfg + several others). Tells TLC that reaching quiescence is acceptable for bounded protocols. Local verification: Model checking completed. No error has been found. 21 states generated, 15 distinct states found, 0 states left on queue. Added [Fact] entry registering SpineAsyncProtocol in TLC test list. Closes B-0179 P2 backlog row. B1 progress: 3 of 4 deferred specs now in CI (DbspSpec via #1397, CircuitRegistration via #1401, SpineAsyncProtocol via this PR). Remaining: B-0181 SpineMergeInvariants (depth-17 trace; substantial counterexample investigation possibly indicating real bug). * fix(tlc-runner): correct SpineAsyncProtocol comment — state invariants, not temporal liveness Reviewer #1411 caught: my comment described the 3 invariants as if they were temporal-liveness properties (eventually-drains, flush-terminates), but the actual TLC-checked predicates are state invariants. The 'eventually' / 'terminates' naming is historical from the spec author's intent comments — the actual predicates are conditional state assertions (when channel empty, processed = sent at that instant). Updated comment to: - Mark them explicitly as STATE invariants - Describe each predicate's actual TLC-checkable form - Note that real liveness would require LTL properties + WF/SF fairness assumptions (not what this spec does) This is the documentation-is-current-state-not-history rule applied to comment-vs-implementation alignment: comments must describe what TLC actually checks, not what the spec author labeled the property in their intent.
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Closes B-0180. CircuitRegistration.cfg referenced
INVARIANT Safetybut the spec didn't define aSafetyoperator, causing TLC to error out:The intended composite invariant is documented at the spec's THEOREM:
Defined
Safetyas exactly that conjunction. Fixes the config bug without changing TLC's check semantics.Local verification
java -cp tla2tools.jar tlc2.TLC ...dotnet test --filter CircuitRegistrationMath-proofs assessment matrix progress
This closes the 2nd of 4 deferred B1 specs (after DbspSpec in #1397):
Composes with
🤖 Generated with Claude Code