Conversation
…xternal-citation-fidelity gap from #1383) Per the math-proofs honest assessment (#1383) outstanding-work matrix, registry rows for the 5 TLA+ specs in CI close the external-citation-fidelity gap on A4. Without rows, the specs are A-grade on internal correctness only; with rows, they become A-grade on both internal correctness AND external-citation fidelity. 5 new rows + format extension: - **TwoPCSink** — full external-citation row (Skeen 1981 + Skeen/Stonebraker 1983 nonblocking commit literature). Per- tick DBSP variant scoped to in-process scheduler-as- coordinator + ISink-as-participants; preconditions diff documents the DBSP narrowing (no coordinator-failure recovery, no async network reordering — both intentional). Definition map links each TLA+ variable to its paper-side counterpart. - **TickMonotonicity** + **TransactionInterleaving** + **OperatorLifecycleRace** + **SmokeCheck** — internal- correctness rows. Format extension: substitute "Internal correctness target" for "Paper", "Internal correctness claim" for "Paper statement", and "Spec-vs-implementation alignment" for the Preconditions-diff + Definition-map pair. SmokeCheck is meta (validates the TLC harness itself, not a Zeta artifact); audit cadence may be looser. Format extension documented in the "How to add a new row" section so future rows for either external-citation or internal-correctness specs can land cleanly. Composes with #1383 (the assessment), the `verification-drift-auditor` skill (which audits these rows on cadence), and `tests/Tests.FSharp/TlcRunnerTests.fs` (the CI runner that exercises the specs). §33 lint passes; memory-references lint passes.
AceHack
deleted the
research/verification-registry-tla-cluster-rows-2026-05-03
branch
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 22625fa513
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
|
||
| - **Artifact.** `tools/tla/specs/TwoPCSink.tla` (TLA+ spec | ||
| with `.cfg`; runs in CI via | ||
| `tests/Tests.FSharp/TlcRunnerTests.fs`). |
There was a problem hiding this comment.
This row links CI execution to tests/Tests.FSharp/TlcRunnerTests.fs, but that file does not exist in this commit; the runner lives at tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs. Keeping a non-existent path here breaks the audit trail this registry is supposed to provide, because reviewers cannot follow the documented evidence chain from spec rows to the actual CI gate.
Useful? React with 👍 / 👎.
Comment on lines
+130
to
+134
| The 5 TLA+ specs that run in CI via `tests/Tests.FSharp/ | ||
| TlcRunnerTests.fs` get registry rows so the math-proofs | ||
| honest assessment (`docs/research/2026-05-03-math-proofs- | ||
| honest-assessment.md`) can claim A-grade for both the *spec | ||
| runs* claim AND the *spec matches source* claim. |
There was a problem hiding this comment.
The section asserts there are only 5 TLA+ specs running in CI, but tests/Tests.FSharp/Formal/Tlc.Runner.Tests.fs in the same commit also runs TLC for InfoTheoreticSharder, RecursiveCountingLFP, and FeatureFlagsResolution (plus SmokeCheck). Because those CI-validated specs are omitted from this registry update, the stated closure of the external-fidelity gap is incomplete and drift audits will miss active CI specs.
Useful? React with 👍 / 👎.
|
|
||
| - **Artifact.** `tools/tla/specs/TransactionInterleaving.tla` | ||
| (TLA+ spec with `.cfg`; runs in CI). | ||
| - **Internal correctness target.** `TransactionZ1Op.fs` |
There was a problem hiding this comment.
This target names TransactionZ1Op.fs, but no such file exists in this commit; the TransactionZ1Op implementation is in src/Core/Transaction.fs. Referencing a non-existent source file makes the spec-to-implementation mapping unverifiable, which undermines the purpose of this internal-correctness row.
Useful? React with 👍 / 👎.
There was a problem hiding this comment.
Pull request overview
This PR updates the verification registry to add TLA+ registry entries and extend the registry format for internally-scoped specs, with the stated goal of closing the formal-verification fidelity gap called out in #1383.
Changes:
- Adds a new TLA+ section in the verification registry with rows for selected CI-run specs.
- Documents a proposed internal-correctness row shape alongside the existing external-citation format.
- Updates the “How to add a new row” guidance to cover these new registry entries.
Comment on lines
+275
to
+279
| 1. New verification artifact with an external citation OR | ||
| internal-correctness spec lands. | ||
| 2. Author (or the auditor, if unclaimed) drops a row here in | ||
| the same round. | ||
| 3. Fill all seven fields (Artifact, Paper, Paper statement, | ||
| Our statement, Preconditions diff, Definition map, Last | ||
| audit). | ||
| 3. For external-citation rows: fill all seven fields |
Comment on lines
+282
to
+286
| For internal-correctness rows: substitute "Internal | ||
| correctness target" for "Paper", "Internal correctness | ||
| claim" for "Paper statement", and "Spec-vs-implementation | ||
| alignment" for the Preconditions diff + Definition map | ||
| pair. |
Comment on lines
+130
to
+131
| The 5 TLA+ specs that run in CI via `tests/Tests.FSharp/ | ||
| TlcRunnerTests.fs` get registry rows so the math-proofs |
Comment on lines
+147
to
+149
| - **Artifact.** `tools/tla/specs/TwoPCSink.tla` (TLA+ spec | ||
| with `.cfg`; runs in CI via | ||
| `tests/Tests.FSharp/TlcRunnerTests.fs`). |
| (TLA+ spec with `.cfg`; runs in CI). | ||
| - **Internal correctness target.** `Circuit.tick` field | ||
| in `src/Core/Circuit.fs`; specifically the | ||
| `Interlocked.Increment(ref _tick)` + `[<VolatileField>]` |
Comment on lines
+130
to
+134
| The 5 TLA+ specs that run in CI via `tests/Tests.FSharp/ | ||
| TlcRunnerTests.fs` get registry rows so the math-proofs | ||
| honest assessment (`docs/research/2026-05-03-math-proofs- | ||
| honest-assessment.md`) can claim A-grade for both the *spec | ||
| runs* claim AND the *spec matches source* claim. |
Comment on lines
+163
to
+168
| instances. Spec verifies four invariants: | ||
| `Idempotent` (epoch commits at most once), `AllOrNothing` | ||
| (committed → all sinks done-or-pending), | ||
| `AbortSafe` (aborted → no sinks done), `NoOrphans` | ||
| (every preCommitted tx eventually committed-or-aborted | ||
| after checkpoint). |
Comment on lines
+209
to
+213
| ObserveTick / ReleaseStep` actions; implementation | ||
| uses `Interlocked.Increment` (atomic) + | ||
| `[<VolatileField>]` (read fence). Spec checks | ||
| `Monotone` invariant + `MaxIncrements` count match; | ||
| implementation enforces same via .NET memory model. |
|
|
||
| - **Artifact.** `tools/tla/specs/TransactionInterleaving.tla` | ||
| (TLA+ spec with `.cfg`; runs in CI). | ||
| - **Internal correctness target.** `TransactionZ1Op.fs` |
Comment on lines
+224
to
+231
| `state ≤ pending` reachability holds; under | ||
| `autoCommit`, `state = pending` after every `Tick`; no | ||
| two concurrent `Commit` calls double-advance. | ||
| - **Spec-vs-implementation alignment.** Spec models | ||
| `state`, `pending`, `autoCommit`, `inputVal`, | ||
| `tickPhase` per-thread; implementation uses | ||
| `Interlocked.CompareExchange` for the CAS. Spec checks | ||
| the three claimed invariants directly. |
Merged
4 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
… A1+A2 → A-with-CI) (#1394) * ci(lean-proof): add CI gate for DbspChainRule.lean type-check (closes A1+A2 → A-with-CI) Per the math-proofs honest assessment (#1383) outstanding-work matrix, the Lean proof of DBSP chain rule (Prop 3.2 + Dop_LTI_commute) was A-grade today hand-run but missing CI gating. Peer reviewers expect "runs in CI" as the line for an A-grade artifact. This PR ships `.github/workflows/lean-proof.yml`: - Path-filter: only runs on `tools/lean4/**` changes (or workflow itself). Out-of-band from gate.yml because Mathlib's lake cache is multi-GB and Lean toolchain setup is heavier than the existing build-and-test surface. - Caches `tools/lean4/.lake` keyed on lean-toolchain + lakefile.toml + lake-manifest.json (busts cleanly on either change). - Caches `~/.elan` with same key shape as gate.yml's elan cache (shared cache space). - Uses `lake exe cache get` to download Mathlib pre-built oleans from S3 — skips the multi-hour Mathlib build. - Type-checks via `lake env lean Lean4/DbspChainRule.lean`. Verified locally: `lake env lean` returns silent + exit 0 (success) on the current proof. Two corrections to #1383 captured in same PR: 1. **Semgrep is already in CI** — original B4 grading was wrong. Verified by grep: `.github/workflows/gate.yml` line ~422 has `lint (semgrep)` job running `semgrep --config .semgrep.yml --error --metrics=off`. Effective grade upgraded to A; outstanding-work item closed. This illustrates the verify-then-claim discipline. 2. **Outstanding-work matrix updated** with Status column tracking each item: "Done" (Semgrep, A4 registry rows #1393, peer-review email #1387), "In flight" (Lean CI — this PR), "open" (Stryker, B1, B2, C-grade items). Composes with verification-registry.md (rows for both A1+A2 benefit) + the verification-drift-auditor skill (every CI fire is implicit drift-check) + #1383 (the assessment doc this upgrades). Workflow safe-pattern compliant per FACTORY-HYGIENE row #43: SHA-pinned actions, contents:read permissions, concurrency group, pinned runs-on, path-filter narrows trigger. * fix(lean-proof): address review threads — add GITHUB_TOKEN env + dedupe outstanding-work row Three review threads on #1394 addressed: 1. + 3. **GITHUB_TOKEN missing**: mise's aqua: backend uses the GitHub API for release-tag lookups during install.sh; without GITHUB_TOKEN it hits the unauthenticated 60/hr rate limit and fails. Added workflow-level env: with secrets.GITHUB_TOKEN — same pattern as gate.yml. Inherits contents:read, no escalation. 2. **Outstanding-work row duplicated**: the Peer-review email draft row was inserted twice (Done + empty status). Removed the empty-status duplicate; single Done row remains.
4 tasks
AceHack
added a commit
that referenced
this pull request
May 3, 2026
…4 deferred specs) (#1397) * ci(tla/tlc): add DbspSpec to TLC test list (closes B1 partial — 1 of 4 deferred specs) Per the math-proofs honest assessment (#1383) outstanding-work matrix B1 entry, "TLA+ specs with .cfg but not in CI (4 specs)": verify-then-claim sweep on 2026-05-03 found 1 of 4 actually passes; the other 3 have real issues blocking CI registration. **Verify-then-claim findings (local TLC runs, 2026-05-03):** - **DbspSpec**: PASSES — 1M distinct states explored in ~11s wall; full state-space coverage. Now registered as `[<Fact>] TLC validates DbspSpec`. - **SpineAsyncProtocol**: FAILS — TLC dumps trace file (`SpineAsyncProtocol_TTrace_<ts>.tla`), indicating counterexample / invariant violation at depth 9. - **CircuitRegistration**: FAILS — config bug. `.cfg` references invariant `Safety` not defined in `.tla`. ("The invariant Safety specified in the configuration file is not defined in the specification.") - **SpineMergeInvariants**: FAILS — TLC dumps trace file at depth 17, indicating counterexample. The 3 failing specs remain intentionally unregistered. They need spec/config fixes in follow-up PRs before CI registration. The test-file comment documents this so future-Otto doesn't blanket-register them and ship 3 immediate red builds. This closes 1 of 4 entries in B1, partial progress on B1 → A. Full B1 closure requires fixing the 3 broken specs. Composes with: - #1383 math-proofs honest assessment (the matrix entry this partially closes) - #1393 verification-registry rows for the 5 in-CI specs (DbspSpec was NOT yet registered there; future tick adds the registry row for it) - proof-tool-coverage.md §2 (the original "deliberately skipped pending re-verification" framing — re-verification has now happened, with mixed results) Local verification: dotnet test --filter DisplayName~DbspSpec passes in 12.8s including TLC run + xunit overhead. * fix(tlc-runner): correct DbspSpec coverage-scope claim — positive weights only, retraction NOT exercised Reviewer #1397 caught: original test comment claimed the DbspSpec model-check 'proves the operator-algebra invariants hold across the configured state space', but DbspSpec.cfg sets W = {0..9} (positives only). Retraction (negative-weight) cases aren't exercised — that coverage lives elsewhere (FsCheck Z-set property tests + Lean Prop 3.2 proof which is general over abelian-group weights). Updated comment now: - Lists the 9 specific invariants verified by name - Documents the cfg's coverage scope verbatim (K = 2-key, W = positives only) - Names the complementary coverage paths (FsCheck + Lean) for retraction cases - Notes the future-work path (enlarging W vs refining the spec model) tied to chain_rule_poly follow-on - References B-0179 + B-0180 + B-0181 for the 3 broken sibling specs (replaces the looser 'follow-up PRs' phrasing) No behavioral change to the test itself — only the comment is updated to match what the cfg actually verifies.
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.
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.'
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
P0 outstanding item from #1383 math-proofs honest assessment. Adds registry rows for the 5 TLA+ specs in CI:
Format extension
For internal-correctness specs (no external paper to drift against), the registry format extends to use:
Documented in the "How to add a new row" section.
Why this closes the A4 gap
Per #1383, A4 (5 TLA+ specs in CI) was A-grade on the spec runs claim but only B-grade on spec matches source. Registry rows close that — now A-grade on both axes, with drift-audit cadence applying.
Test plan
tests/Tests.FSharp/TlcRunnerTests.fs(the CI runner) + the verification-drift-auditor skill🤖 Generated with Claude Code