From 3060131ca84447d669cf39b5a3fce101583c1da1 Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sat, 23 May 2026 19:23:56 -0400 Subject: [PATCH 1/3] =?UTF-8?q?backlog(B-0716):=20file=20Soraya=20round-53?= =?UTF-8?q?=20scope-correction=20=E2=80=94=20B-0709=20enumeration=20under-?= =?UTF-8?q?counted=20by=203=20LSM-tree=20Spine=20specs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Soraya's eighth autonomous routing tick (round 53, post-PR #4790 merge). B-0709 (round 42) enumerated 11 unregistered specs. Round-53 re-audit identified 14 unregistered — B-0709 missed the LSM-tree Spine cluster (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla) with O'Neil 1996 LSM-paper anchor. Coverage ratio correction: 7/21 = 0.33 (worse than B-0709's claimed 0.52; correct direction — auditor surfacing latent debt including its own first-pass-incompleteness). NOT a duplicate of B-0709; explicit scope-correction sub-finding. P3 because B-0709 is already filed and Kenji owns the umbrella; integration-time cost of authoring 3 additional Spine rows alongside the 11 is near-zero. Routing: existing TLA+ for *.tla, Alloy for *.als (no tool change). Failure at registry layer, identical class to B-0709/B-0713/B-0715. TLA+-hammer guard: N/A. Effort: S (marginal cost over B-0709-as-filed: near-zero). P3. Assignee: kenji. Substrate-honest framing: auditor's own first-pass-incompleteness, surfaced by re-audit. Filing as scope-correction (not supersession) keeps B-0709 umbrella intact while pinning on-disk truth. The auditor surfacing the gap in its own earlier enumeration is the same discipline applied recursively. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships immediately. Authored via git plumbing fallback. --- docs/BACKLOG.md | 1 + ...correction-3-lsm-spine-specs-2026-05-23.md | 97 +++++++++++++++++++ 2 files changed, 98 insertions(+) create mode 100644 docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index 37e1677462..ebb037e698 100644 --- a/docs/BACKLOG.md +++ b/docs/BACKLOG.md @@ -792,5 +792,6 @@ are closed (status: closed in frontmatter)._ - [ ] **[B-0689](backlog/P3/B-0689-otto-vscode-surface-sender-ids-extension-bootstream-2026-05-21.md)** Otto-VSCode third foreground surface — add otto-vscode to SENDER_IDS + canonical cold-boot bootstream at docs/launch/ - [ ] **[B-0696](backlog/P3/B-0696-substrate-surface-change-bus-envelope-cross-ai-coordination-mechanization-2026-05-21.md)** substrate-surface-change bus envelope — cross-AI coordination of load-bearing-substrate changes via tools/bus (mechanizes the human-as-coordination-substrate pattern) - [ ] **[B-0699](backlog/P3/B-0699-dual-adinkra-time-aware-default-dumb-fast-version-with-case-by-case-performance-justification-mika-2026-05-18.md)** Dual-Adinkra architecture — full time-aware retractable default + dumb fast version with case-by-case performance justification (Aaron + Mika 2026-05-18) +- [ ] **[B-0716](backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md)** Soraya round-53 scope-correction — B-0709 enumeration under-counted by 3 LSM-tree Spine specs (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla) diff --git a/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md new file mode 100644 index 0000000000..b3c1ac63bb --- /dev/null +++ b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md @@ -0,0 +1,97 @@ +--- +id: B-0716 +priority: P3 +status: open +title: "Soraya round-53 scope-correction — B-0709 enumeration under-counted by 3 LSM-tree Spine specs (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla)" +created: 2026-05-23 +last_updated: 2026-05-23 +classification: buildable-now +decomposition: atomic +assignee: kenji +discovered_by: soraya +owners: [kenji, formal-verification-expert] +type: scope-correction +composes_with: + - docs/backlog/P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md + - tools/alloy/specs/Spine.als + - tools/tla/specs/SpineAsyncProtocol.tla + - tools/tla/specs/SpineMergeInvariants.tla + - docs/research/verification-registry.md +--- + +# B-0716 — B-0709 scope-correction: 3 LSM-tree Spine specs missed in original enumeration (Soraya round-53 hand-off) + +## Origin + +Soraya's eighth autonomous routing tick (2026-05-23 — round 53, post-PR #4790 merge of B-0715). NOT a duplicate of B-0709; an explicit scope-correction sub-finding. + +## Finding + +B-0709 (round 42) enumerated **11 unregistered specs**. Soraya round 53 re-audit identified **14 unregistered**: B-0709 missed the **LSM-tree Spine cluster** — three artifacts with established literature anchor (O'Neil, Cheng, Gawlick, O'Neil 1996 *Acta Informatica* LSM paper): + +| Spec | Tool | Target | Anchor | +|---|---|---|---| +| `tools/alloy/specs/Spine.als` | Alloy | LSM-tree structural model | O'Neil 1996 | +| `tools/tla/specs/SpineAsyncProtocol.tla` | TLA+ | Spine async protocol behavioural model | O'Neil 1996 | +| `tools/tla/specs/SpineMergeInvariants.tla` | TLA+ | Spine merge invariants safety | O'Neil 1996 | + +None of the 3 appear in `docs/research/verification-registry.md`; none appear in B-0709's enumeration list. + +## Coverage ratio correction + +B-0709 claimed coverage ratio of **0.52** (numerator 7, denominator 17 TLA+/Lean + 3 Alloy = 20, minus 5 already-registered = 11 unregistered + 7 registered = 18 → 7/18 ≈ 0.39 actual; B-0709's 0.52 was computed against a different denominator). + +Round-53 on-disk truth: +- 16 TLA+ specs + 3 Alloy specs + 2 Lean theorems = **21 artifacts total** +- 7 already registered +- **14 unregistered** (not 11 — B-0709 missed the 3 Spine specs) +- Ratio: 7/21 = **0.33** (worse than B-0709's claimed 0.52; correct direction — auditor surfacing latent debt) + +## Distinct from prior session findings + +This is a **scope-correction** on an existing row (B-0709), NOT a new umbrella. Specifically: + +- B-0709 is the umbrella (round 42); this row amends its enumeration without superseding it +- B-0710/B-0711/B-0712 (rounds 43-45) — different cross-check axes +- B-0713 (round 50) — Lean exploratory artifact (different artifact) +- B-0714 (round 51) — TLA+ runnability (different axis) +- B-0715 (round 52) — Lean axiom-registry (different artifact + scope) + +P3 priority because B-0709 is already filed and Kenji owns the umbrella; integration-time cost of authoring the Spine rows alongside the other 11 is near-zero. + +## Routing decision (Soraya) + +- **Primary tool**: existing TLA+/TLC for `SpineAsyncProtocol` + `SpineMergeInvariants`; existing Alloy for `Spine.als` (no tool change needed — failure is at registry layer, identical class to B-0709/B-0713/B-0715) +- **Cross-check**: warranted only after registry rows land (per BP-16 cross-check triage) +- **Wrong-tool cost at TOOL axis**: zero (tool choices on-disk are correct) +- **Cost at REGISTRY axis**: the auditor `verification-drift-auditor` cannot flag future Class 1/2/3 drift on 3 specs that aren't even registered as needing audit + +## TLA+-hammer guard + +N/A — finding is enumeration completeness on existing umbrella, not tool routing. On-disk tool choices for Spine cluster are correct (Alloy for structural / TLA+ for behavioural; both appropriate). + +## Acceptance criteria + +1. B-0709's body amended (in-place edit OR follow-up commit) to enumerate 14 unregistered specs instead of 11 — add Spine cluster (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla) +2. When Kenji executes B-0709, all 14 rows land in `verification-registry.md` (not just the original 11) +3. Each Spine row cites O'Neil 1996 paper anchor + brief preconditions diff +4. Coverage ratio metric refreshed in B-0709's body: 7/21 = 0.33 baseline for round 53 +5. `verification-drift-auditor` skill can now audit Spine specs against paper-fidelity (currently invisible to it) + +## Effort + +S (3 additional rows in the same registry-row-authoring pass that B-0709 already requires). Marginal cost over B-0709-as-filed: near-zero. + +## Composes with + +- [`docs/backlog/P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md`](../P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md) — umbrella row this corrects +- [`tools/alloy/specs/Spine.als`](../../../tools/alloy/specs/Spine.als) — missed target #1 +- [`tools/tla/specs/SpineAsyncProtocol.tla`](../../../tools/tla/specs/SpineAsyncProtocol.tla) — missed target #2 +- [`tools/tla/specs/SpineMergeInvariants.tla`](../../../tools/tla/specs/SpineMergeInvariants.tla) — missed target #3 +- [`docs/research/verification-registry.md`](../../research/verification-registry.md) — destination +- B-0710 / B-0711 / B-0712 / B-0713 / B-0714 / B-0715 (sibling Soraya hand-offs this session) +- `memory/persona/soraya/NOTEBOOK.md` round-53 entry (pending append) + +## Substrate-honest framing + +B-0709's enumeration was incomplete (under-counted by 3 specs in the same LSM-tree cluster). This is the auditor's own first-pass-incompleteness, surfaced by re-audit. Filing as scope-correction (not supersession) keeps B-0709's umbrella intact while pinning the actual on-disk truth. The auditor's job is surfacing debt; surfacing the gap in its OWN earlier enumeration is the same discipline applied recursively. From 2793c8b349e9e35fa2861b52159b96467c58d67e Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sat, 23 May 2026 19:35:01 -0400 Subject: [PATCH 2/3] =?UTF-8?q?fix(PR=20#4791):=20MD032=20blank-line=20+?= =?UTF-8?q?=20BACKLOG.md=20regen=20=E2=80=94=20mechanical=20only?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Addresses the 2 failing required checks (`lint (markdownlint)` + `check docs/BACKLOG.md generated-index drift`). Does NOT address the 2 unresolved review threads on the row's arithmetic — those need design-judgment + author resolution (see PR comment). Mechanical fixes: 1. MD032: added blank line between "Round-53 on-disk truth:" header text and the immediately-following bullet list at line 45 2. BACKLOG.md: regenerated via `BACKLOG_WRITE_FORCE=1 bun tools/backlog/generate-index.ts` NOT fixing here (out of mechanical scope): - Line 42 arithmetic contradictions ("20 - 5 = 15" stated as "11 unregistered" + "11 + 7 = 18 total" — three internally- inconsistent claims about same registry state). Author/Soraya needs to clarify intent + the 5-vs-7 registered ambiguity - Line 48 spec count: `tools/tla/specs/` actually contains 19 TLA+ specs (verified `ls tools/tla/specs/*.tla | wc -l`), not 16 as B-0716 claims. Downstream "= 21 artifacts total" + "14 unregistered" + "Ratio: 7/21 = 0.33" all chain from this base. Re-derivation needs full registry-membership-semantics pass that mechanical fix can't safely make in isolation Threads remain unresolved — see PR comment. Co-Authored-By: Claude --- docs/BACKLOG.md | 1 - ...ound53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index ebb037e698..981d4f1447 100644 --- a/docs/BACKLOG.md +++ b/docs/BACKLOG.md @@ -664,7 +664,6 @@ are closed (status: closed in frontmatter)._ - [ ] **[B-0694](backlog/P2/B-0694-otto-vscode-pr8-standing-query-codegen-iincrementalgenerator-2026-05-21.md)** Standing-query codegen — IIncrementalGenerator that rewrites circuit expressions to fused IL (Otto-VSCode 8-PR campaign PR #8 — the capstone) - [ ] **[B-0695](backlog/P2/B-0695-fast-life-branch-experiment-hourly-batched-gates-cost-reduction-2026-05-21.md)** fast/life branch experiment — hourly batched CI gates with promotion-path; per-PR CI cost reduction is burst-dependent (cost-neutral at 1 PR/hr; ~33% reduction at example 6 PRs/hr burst per corrected math; Phase 5 measures empirical savings) while preserving Copilot/Codex 100k-line review capability + Soraya-promotion-gate - [ ] **[B-0698](backlog/P2/B-0698-zsetw-phase-2-operator-and-algorithm-migration-plan-2026-05-21.md)** ZSetW Phase 2 plan — operator + algorithm migration onto polymorphic Z-set substrate; tier-A operator parity (map/filter/cartesian/join/distinct/weightedCount); two worked-example algorithms (TropicalSemiring shortest-path; IntervalRing propagation); migration documentation for callers -- [ ] **[B-0700](backlog/P2/B-0700-soraya-continuous-loop-substrate-with-bus-escalation-2026-05-17.md)** Soraya continuous-loop substrate with bus escalation - [ ] **[B-0703](backlog/P2/B-0703-multi-oracle-consensus-with-bft-inside-dst-agreement-across-trust-gradient-architecture-aaron-2026-05-21.md)** Multi-oracle consensus with BFT-inside + DST-agreement-across: trust-gradient architecture beyond single-layer BFT (Aaron 2026-05-21) - [ ] **[B-0704](backlog/P2/B-0704-secret-message-over-reticulum-via-spectre-tile-position-pressure-no-copy-by-geometry-aaron-2026-05-21.md)** Secret-message-over-Reticulum via spectre-tile position-pressure — no-copy by geometry, not by cryptography (Aaron 2026-05-21) - [ ] **[B-0705](backlog/P2/B-0705-autocomplete-as-traveler-consent-event-shadow-star-marker-as-cryptographic-receipt-lior-website-2026-05-22.md)** Autocomplete-as-Traveler-consent-event — (shadow*) marker as cryptographic receipt of cross-temporal consent event diff --git a/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md index b3c1ac63bb..d98c80394e 100644 --- a/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md +++ b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md @@ -42,6 +42,7 @@ None of the 3 appear in `docs/research/verification-registry.md`; none appear in B-0709 claimed coverage ratio of **0.52** (numerator 7, denominator 17 TLA+/Lean + 3 Alloy = 20, minus 5 already-registered = 11 unregistered + 7 registered = 18 → 7/18 ≈ 0.39 actual; B-0709's 0.52 was computed against a different denominator). Round-53 on-disk truth: + - 16 TLA+ specs + 3 Alloy specs + 2 Lean theorems = **21 artifacts total** - 7 already registered - **14 unregistered** (not 11 — B-0709 missed the 3 Spine specs) From abe193c4f5ee492766d96de28cc2a2d156679e5e Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sat, 23 May 2026 20:04:36 -0400 Subject: [PATCH 3/3] fix(B-0716): correct arithmetic + on-disk counts per Codex P2 + Copilot reviews - Codex P2 (line 42): denominator math was internally contradictory (20 - 5 = 15 vs "11 unregistered + 7 registered = 18"). Mixed file-counts with theorem-entry counts. - Copilot (line 49): claimed 16 TLA+ specs but tools/tla/specs/ holds 19 (BftConsensus, EngagementLiveness, RecursiveSignedSemiNaive among the 14 named). On-disk truth (file-level, uniform unit-of-measure): - 19 TLA+ + 3 Alloy + 2 Lean spec files (excl. Lean4.lean root) = 24 total artifacts - 6 registered files (5 TLA+ + DbspChainRule.lean) in the registry - 18 unregistered files; B-0709 enumerated 11; this row surfaces the 3 missed Spine specs; remaining 4 tracked under sibling rows Acceptance criteria #4 updated: 7/21=0.33 -> 6/24~=0.25 baseline. Verification commands run: ls tools/tla/specs/*.tla | wc -l # 19 ls tools/alloy/specs/*.als | wc -l # 3 find tools/lean4 -name '*.lean' # Lean4.lean, ToyModel.lean, # DbspChainRule.lean Co-Authored-By: Claude --- ...e-correction-3-lsm-spine-specs-2026-05-23.md | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md index d98c80394e..376c4b3eb6 100644 --- a/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md +++ b/docs/backlog/P3/B-0716-soraya-round53-b0709-scope-correction-3-lsm-spine-specs-2026-05-23.md @@ -39,14 +39,17 @@ None of the 3 appear in `docs/research/verification-registry.md`; none appear in ## Coverage ratio correction -B-0709 claimed coverage ratio of **0.52** (numerator 7, denominator 17 TLA+/Lean + 3 Alloy = 20, minus 5 already-registered = 11 unregistered + 7 registered = 18 → 7/18 ≈ 0.39 actual; B-0709's 0.52 was computed against a different denominator). +B-0709 (round 42) reported coverage ratio **0.52** with the framing "7 registered / 11 unregistered". That framing was incomplete on both axes: the enumeration missed the LSM-tree Spine cluster, and the denominator arithmetic mixed file-counts with theorem-entry counts. -Round-53 on-disk truth: +Round-53 on-disk truth (file-level, uniform unit-of-measure): -- 16 TLA+ specs + 3 Alloy specs + 2 Lean theorems = **21 artifacts total** -- 7 already registered -- **14 unregistered** (not 11 — B-0709 missed the 3 Spine specs) -- Ratio: 7/21 = **0.33** (worse than B-0709's claimed 0.52; correct direction — auditor surfacing latent debt) +- **19 TLA+ specs** in `tools/tla/specs/*.tla` +- **3 Alloy specs** in `tools/alloy/specs/*.als` +- **2 Lean spec files** in `tools/lean4/` (excluding the `Lean4.lean` library root) — `Lean4/DbspChainRule.lean` + `ImaginaryStack/ToyModel.lean` +- **24 verification artifacts total** +- **6 registered files** in `docs/research/verification-registry.md` (5 TLA+ files + `DbspChainRule.lean` carrying 2 theorem entries) +- **18 unregistered files** (24 − 6) — B-0709 enumerated 11 of these; this row surfaces the 3 missed Spine specs (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla), bringing the visible-to-this-PR count to 14; the remaining 4 (e.g., `ImaginaryStack/ToyModel.lean`) are tracked under sibling Soraya hand-offs (B-0713 etc.) +- **File-level coverage ratio for round 53: 6 / 24 ≈ 0.25** — worse than B-0709's claimed 0.52, correct direction (auditor surfacing latent debt that the round-42 enumeration also under-counted) ## Distinct from prior session findings @@ -76,7 +79,7 @@ N/A — finding is enumeration completeness on existing umbrella, not tool routi 1. B-0709's body amended (in-place edit OR follow-up commit) to enumerate 14 unregistered specs instead of 11 — add Spine cluster (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla) 2. When Kenji executes B-0709, all 14 rows land in `verification-registry.md` (not just the original 11) 3. Each Spine row cites O'Neil 1996 paper anchor + brief preconditions diff -4. Coverage ratio metric refreshed in B-0709's body: 7/21 = 0.33 baseline for round 53 +4. Coverage ratio metric refreshed in B-0709's body using file-level uniform unit-of-measure: 6 / 24 ≈ 0.25 baseline for round 53 (correcting B-0709's mixed-unit 0.52) 5. `verification-drift-auditor` skill can now audit Spine specs against paper-fidelity (currently invisible to it) ## Effort