backlog(B-0714): file Soraya round-51 hand-off — 3 TLA+ specs missing .cfg files (runnability gap)#4789
Merged
AceHack merged 1 commit intoMay 23, 2026
Conversation
… .cfg files (runnability gap) Soraya's sixth autonomous routing tick (round 51, post-PR #4783 merge). Three TLA+ specs (AsyncStreamEnumerator.tla 71 LOC, ConsistentHashRebalance.tla 63 LOC, DictionaryStripedCAS.tla 59 LOC) exist in tools/tla/specs/ but have no companion .cfg files. Without .cfg, TLC cannot be invoked — the specs look like coverage but provide zero runtime verification. Distinct from B-0709 (round-42 registry-coverage axis). B-0709 = Class 0 drift in verification-registry.md. This row = runnability axis: a spec can be registered yet still unrunnable for lack of .cfg. The two axes compose; B-0709 + B-0714 together close both for these specs. Soraya routing: TLA+/TLC correct for all three (state-machine safety + concurrency race). Cross-check not yet warranted; .cfg is prerequisite for any cross-check work per BP-16. TLA+-hammer guard: CONFIRMING direction (stay with TLC); FsCheck-only would miss interleavings — CPU-month to reproduce on real hardware. Effort: S each, total ~M. Assignee: kenji. Acceptance: 3 new .cfg files mirroring OperatorLifecycleRace.cfg shape + bounded constants + CI wiring + each .cfg TLC-runs-clean locally. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships immediately. Authored via git plumbing fallback (dotgit-saturation-resilient).
AceHack
deleted the
otto/soraya-round51-b0714-tla-cfg-runnability-2026-05-23
branch
There was a problem hiding this comment.
Pull request overview
Adds a new backlog row (B-0714) documenting a TLA+/TLC runnability gap: three existing specs under tools/tla/specs/ lack companion .cfg files, preventing TLC execution and CI gating.
Changes:
- Add
docs/backlog/P2/B-0714-…mdcapturing the finding, routing rationale, and acceptance criteria for authoring the missing.cfgfiles. - Update
docs/BACKLOG.mdto include the new B-0714 row in the P2 index.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| docs/backlog/P2/B-0714-soraya-round51-tla-cfg-runnability-gap-3-specs-2026-05-23.md | New backlog row describing missing .cfg files for three TLA+ specs and required CI wiring. |
| docs/BACKLOG.md | Adds B-0714 to the generated backlog index under P2. |
Comment on lines
+32
to
+36
| | Spec | LOC | `.cfg` present? | Target | | ||
| |---|---|---|---| | ||
| | `tools/tla/specs/AsyncStreamEnumerator.tla` | 71 | ❌ | F# IAsyncEnumerator contract (state-machine + concurrency) | | ||
| | `tools/tla/specs/ConsistentHashRebalance.tla` | 63 | ❌ | Consistent-hash / Jump-Memento wrapper (state evolution of bucket assignment) | | ||
| | `tools/tla/specs/DictionaryStripedCAS.tla` | 59 | ❌ | DiskBackingStore stripe-CAS (multi-writer race) | |
Comment on lines
675
to
+678
| - [ ] **[B-0711](backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md)** Soraya round-44 hand-off — Residuated FsCheck property file (Galois + residual + retraction equivalence) | ||
| - [ ] **[B-0712](backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md)** Soraya round-45 hand-off — WitnessDurable commit protocol (TLA+ spec + Z3 quorum-arithmetic lemma + FsCheck cross-check) | ||
| - [ ] **[B-0713](backlog/P2/B-0713-soraya-round50-imaginary-stack-toy-model-registry-gap-lean-2026-05-23.md)** Soraya round-50 hand-off — register Lean ImaginaryStack/ToyModel in verification-registry.md (sorry-bearing artifact with HaPPY-paper fidelity claim) | ||
| - [ ] **[B-0714](backlog/P2/B-0714-soraya-round51-tla-cfg-runnability-gap-3-specs-2026-05-23.md)** Soraya round-51 hand-off — author 3 missing TLA+ `.cfg` files (AsyncStreamEnumerator / ConsistentHashRebalance / DictionaryStripedCAS) — runnability gap distinct from B-0709 registry gap |
AceHack
added a commit
that referenced
this pull request
May 23, 2026
…iant axiom in verification-registry (#4790) Soraya's seventh autonomous routing tick (round 52, post-PR #4789 merge). tools/lean4/Lean4/DbspChainRule.lean:272 defines IsTimeInvariant as structure with commute_zInv : forall s n, f (zInv s) n = zInv (f s) n. This is a de facto axiom (no proof obligation; callers discharge per- operator). Both registered theorems (chain_rule_proposition_3_2 + Dop_LTI_commute) take it as hypothesis — but the axiom itself has no registry row. The artifact's own strikethrough revision history (Prop 3.5 -> Theorem 3.3 correction round 35, 2026-05-05) proves the drift class this row is designed to catch already fired empirically on THIS exact axiom. Registry rows are the structural prevention; currently missing for the axiom. Distinct from B-0709 (TLA+/Alloy portfolio coverage), B-0713 (Lean ImaginaryStack exploratory), B-0714 (TLA+ runnability). New axis: registered theorems depending on unregistered axiom in same artifact. Soraya routing: Lean 4 correct primary (structure-with-axiom is Mathlib idiomatic); cross-check NONE today (axiom is structural not pointwise; Z3/FsCheck inapplicable; paper-fidelity is human-grade registry-audit). Cost lives at REGISTRY axis, not TOOL axis. TLA+-hammer guard: N/A. Effort: S. Assignee: kenji. Acceptance: 1 new registry row + 2 back-pointer cross-refs from existing theorem rows' Preconditions-diff sections. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships immediately. Authored via git plumbing fallback.
This was referenced May 24, 2026
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
Soraya autonomous round 51 — runnability gap distinct from B-0709 registry gap.
Three TLA+ specs exist in
tools/tla/specs/but have no companion.cfgfile:.cfg?AsyncStreamEnumerator.tlaConsistentHashRebalance.tlaDictionaryStripedCAS.tlaWithout
.cfg, TLC cannot be invoked — specs look like coverage but provide zero runtime verification.Distinct from B-0709
B-0709 = registry-coverage axis (Class 0 drift in
verification-registry.md). This row = runnability axis. A spec can be registered yet still unrunnable for lack of.cfg. B-0709 + B-0714 together close both axes for these specs.Routing decision
.cfgis prerequisite per BP-16Effort
S each, total ~M. Assignee: kenji.
Policy-flip authorization
Per Aaron's 2026-05-23 21:30Z direction: Otto auto-ships Soraya findings immediately.
Test plan