Skip to content

fix(ci/gate): narrow verifier-jars cache path — was clobbering source-controlled specs (P0; unblocks #1401)#1403

Merged
AceHack merged 1 commit intomainfrom
fix/verifier-jars-cache-too-broad-clobbers-specs
May 3, 2026
Merged

fix(ci/gate): narrow verifier-jars cache path — was clobbering source-controlled specs (P0; unblocks #1401)#1403
AceHack merged 1 commit intomainfrom
fix/verifier-jars-cache-too-broad-clobbers-specs

Conversation

@AceHack
Copy link
Copy Markdown
Member

@AceHack AceHack commented May 3, 2026

Summary

P0 silent-bug found via verify-then-claim sweep on #1401's CI failure. The verifier-jars cache in gate.yml uses tools/tla + tools/alloy as whole-directory paths. On cache hit, actions/cache OVERWRITES the freshly-checked-out PR-modified spec files with cached versions.

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.

How surfaced

PR #1401 (CircuitRegistration Safety invariant fix):

Environment Result
Local "Model checking completed. No error has been found." 3538 states / depth 14
CI "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

Why P0

Latent silent failure: every PR that modified tools/tla/specs/** or tools/alloy/** silently failed to actually test its changes. The test report would show the OLD spec passing. Discovery-by-luck class — only surfaced when a PR introduced a new invariant referenced by the cfg.

Test plan

🤖 Generated with Claude Code

@AceHack
fix(ci/gate): narrow verifier-jars cache path to jars only — was clob…
0abca99 
…bering source-controlled specs

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)
Copilot AI review requested due to automatic review settings May 3, 2026 13:03
@AceHack AceHack enabled auto-merge (squash) May 3, 2026 13:03
Copilot AI reviewed May 3, 2026
View reviewed changes
Copy link
Copy Markdown

Copilot AI left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Pull request overview

This PR narrows the verifier cache in the main CI gate so spec-source files under tools/tla and tools/alloy are no longer overwritten by restored cache contents. It fits into the repository's CI/formal-verification infrastructure by making the gate actually test the checked-out verifier specs instead of stale cached copies.

Changes:

  • Restrict the actions/cache verifier cache in gate.yml from whole directories to the two jar files only.
  • Bump the verifier cache key suffix to -v2 to invalidate previously poisoned cache entries.
  • Add an in-file incident note documenting the prior silent spec-clobbering failure mode and the #1401 reproduction.

Comment thread .github/workflows/gate.yml
@AceHack AceHack mentioned this pull request May 3, 2026
Merged
3 tasks
@AceHack AceHack merged commit 5982c6b into main May 3, 2026
29 checks passed
@AceHack AceHack deleted the fix/verifier-jars-cache-too-broad-clobbers-specs branch May 3, 2026 13:09
AceHack added a commit that referenced this pull request May 3, 2026
@AceHack
fix(ci): low-memory.yml cache fix + structural audit (`audit-ci-cache…
08e1baf 
…-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
@AceHack
fix(audit-ci-cache-paths): address 3 review findings on #1404 — absol…
691aaae 
…ute 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
AceHack added a commit that referenced this pull request May 3, 2026
@AceHack
fix(ci): low-memory.yml cache + audit-ci-cache-paths.ts (Aaron's "mak…
45baaa0 
…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).
@AceHack AceHack mentioned this pull request May 3, 2026
Merged
2 tasks
AceHack added a commit that referenced this pull request May 3, 2026
@AceHack
ci(audit): wire audit-ci-cache-paths.ts as lint job — closes #1404 fo…
e1a9cae 
…llow-up (#1406)

Wires the structural cache-path audit (shipped in #1404) into CI as
a dedicated lint workflow. The audit fires on:

- Any change to .github/workflows/** (catches new workflow files
  that might introduce broad cache paths)
- Any change to tools/hygiene/audit-ci-cache-paths.ts (catches
  bugs in the audit itself before they affect future PRs)
- workflow_dispatch (manual triage)

Job runs the .ts audit; non-zero exit fails the workflow, blocking
merge if any actions/cache path overlaps with git-tracked files.

This closes the not-lucky-next-time loop: future PRs that introduce
the silent-clobber bug class CANNOT pass this gate. The audit's
detailed violation output (workflow + step + tracked file +
'Why this is a bug' + 'How to fix') makes the failure self-
diagnosing.

Local verification: 13 workflows audited (including this new one);
no overlap. The audit returns clean as a baseline.

Composes with #1404 (the audit tool itself), #1403 (the gate.yml
fix that proved the bug), the math-proofs assessment's test-
fidelity discipline.
This was referenced May 3, 2026
Merged
Merged
AceHack added a commit that referenced this pull request May 3, 2026
@AceHack
memory: cache-paths-mutually-exclusive-with-git-ls-files discipline (…
52661d7 
…silent-clobber bug class) (#1407)

* memory: cache-paths-mutually-exclusive-with-git-ls-files discipline (silent-clobber bug class)

Captures the durable substrate for the discipline rule the session
surfaced via the CircuitRegistration cache-clobber discovery
(#1403 + #1404 + #1406):

  *actions/cache paths must be mutually exclusive with git ls-files —
   cache only DERIVED files (downloaded jars, built artefacts,
   user-home tool state), never source-controlled content.*

Memory file structure (per chat-is-assertion-channel discipline +
substrate-or-it-didn't-happen):

- Rule (carved sentence)
- Why this is load-bearing (the silent + invisible failure mode)
- Triggering case (CircuitRegistration B-0180 fix; verbatim error
  text)
- How to apply (3 layers: workflow-author-time + verify-then-claim-
  time + structurally enforced via audit + lint gate)
- Composes with (DST + verify-then-claim + test-fidelity contract +
  CI-on-CI audit pattern)
- Tooling lineage (4 substrate refs)
- Future-Otto reference (when-tempted + when-CI-fails)
- Reasoning lineage (Aaron's 'lucky catch' question)

MEMORY.md updated with newest-first pointer.

Composes with the earlier cluster (#1403 cache fix + #1404 audit
tool + #1406 CI lint gate) — this memory file is the chat→substrate
discipline-encoding step that closes the loop.

* memory(cache-paths): add bug-locus disambiguation per Aaron's question — usage-bug not GitHub-bug

Aaron 2026-05-03: 'is the a real github bug or was a bug in our code?'

Honest answer: NOT a GitHub bug, IS a bug in our workflow config.
actions/cache does exactly what its docs promise — restores cached
files at the configured paths. We asked it to cache a path that
contained source-controlled files; it did. The fix is on our side:
narrow the cache path.

Added 'Bug-locus disambiguation' section to the memory file
clarifying:
- This is a usage bug in workflow configuration, not a tool bug
- The existing actions/cache behavior is documented
- A reasonable upstream feature request (warn-on-overlap-with-git)
  would be an enhancement, not a bug fix

Future-Otto reading this memory: don't pattern-match the discovery
as 'GitHub broken' when reaching for the discipline. The structural
fix (audit + lint gate) is correct because OUR usage was wrong, not
because the action was wrong.
AceHack added a commit that referenced this pull request May 3, 2026
@AceHack
hygiene(tick-history): 2026-05-03T13:30Z — math-proofs assessment clu…
8b52d7d 
…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.'
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

Copilot code review Copilot Copilot left review comments

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@AceHack