backlog(B-0710..B-0712): file Soraya rounds 43+44+45 hand-offs#4774
Merged
Conversation
Aaron 2026-05-23 21:30Z: 'lets try to keep things moving other than
if we need budget increases' — policy-flip authorization: Soraya
findings flow through Otto (plumbing-commit-fallback) to backlog
without per-finding maintainer pick. Aaron reviews aggregates only
(root axioms, drift reports, DORA).
Three findings filed:
B-0710 — DBSP chain rule BP-16 cross-check (round 43)
- Lean artifact is single-tool; needs FsCheck cross-trace +
Z3 pointwise lemma to cross publication line
- Composes with PR #4772 (Lean DBSP README + CI badge that
just landed) — gap #3 of the chain-rule publication arc
- Effort: S+S; assignee kenji
B-0711 — Residuated FsCheck property file (round 44)
- Residuated.fs is ONLY CRDT-class file with zero FsCheck
(sanity-checked across PNCounter, OrSet, Lww, GCounter,
DeltaCrdt, Bloom, CountMin, Haar, HyperLogLog, HyperMinHash)
- Round-17 incident (O(1) claim was actually O(n)) caught by
harsh-critic; FsCheck IS the regression guard
- Three properties: Galois + residual + retraction equivalence
- Effort: S; assignee kenji
B-0712 — WitnessDurable commit protocol triple (round 45)
- Durability.fs:14-22 self-declares TLA+ prereq; type itself
is the gate (Save throws until proven)
- P0 triple: TLA+ for state-machine safety + Z3 for quorum
arithmetic + FsCheck for real-code cross-check
- Soraya explicitly named + REJECTED the TLA+-hammer trap
(don't bundle quorum arithmetic into TLA+; Z3 closes in
seconds vs TLC enumeration)
- Effort: M+S+S; assignee kenji
All three discovered by Soraya autonomous tick across rounds
42-45 (her loop started 2026-05-23 ~20:00Z). Round 42 already
filed as B-0709 (merged earlier today).
Lands via git plumbing (6th plumbing-fallback PR this session —
sibling pattern to #4755 / #4761 / #4762 / #4765 / #4772).
Co-Authored-By: Claude <noreply@anthropic.com>
There was a problem hiding this comment.
Pull request overview
Adds three new per-row backlog entries capturing Soraya’s round-43/44/45 hand-offs as actionable backlog work items, aligned with the repo’s per-row backlog workflow under docs/backlog/P2/.
Changes:
- Adds B-0710 (DBSP chain rule BP-16 cross-check: FsCheck + Z3).
- Adds B-0711 (Residuated FsCheck property coverage).
- Adds B-0712 (WitnessDurable commit protocol verification triple: TLA+ + Z3 + FsCheck).
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 6 comments.
| File | Description |
|---|---|
| docs/backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md | New backlog row for chain rule cross-check work (FsCheck + Z3) and registry updates. |
| docs/backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md | New backlog row to add FsCheck law coverage for Residuated.fs. |
| docs/backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md | New backlog row defining a 3-tool verification plan for WitnessDurable durability mode. |
…711/B-0712 rows Two CI failures on PR #4774: 1. markdownlint MD032: B-0710 line 31 — '**Empirical**:' bullets need blank line above 2. backlog-index-integrity: docs/BACKLOG.md not regenerated after new B-NNNN rows added Fix 1: insert blank line between '**Empirical**:' paragraph and bullet list per MD032. Fix 2: BACKLOG_WRITE_FORCE=1 bun tools/backlog/generate-index.ts — 4 new index lines for the 3 new rows. Authored via git plumbing fallback under dotgit-saturation (peer-Otto + Lior contention).
Corrections to Soraya hand-off backlog rows surfaced by Copilot review. All findings empirically verified against tree state: B-0710 (round-43 chain-rule cross-check): - spec count: "20 TLA+ specs" → "19 TLA+ specs" (verified: `ls tools/tla/specs/*.tla | wc -l` = 19) - NOTEBOOK ref: `line 238` → `Round 43 entry` heading-anchor (notebook is 234 lines; line refs brittle to pruning cadence) B-0711 (round-44 Residuated FsCheck): - test-wiring claim: "should pick them up automatically" → explicit `<Compile Include="..." />` registration required (verified: tests/Tests.FSharp/Tests.FSharp.fsproj has 96 explicit Compile entries; not glob-based) - NOTEBOOK ref: `lines 308-404` → `Round 44 entry` heading-anchor B-0712 (round-45 WitnessDurable triple): - test path: `tests/Tests.FSharp/Durability/WitnessDurable.Properties.fs` → `tests/Tests.FSharp/Storage/WitnessDurable.Properties.fs` (verified: no `Durability/` directory exists; existing `tests/Tests.FSharp/Storage/Durability.Tests.fs` is the current test layout sibling) - NOTEBOOK ref: `lines 407-505` → `Round 45 entry` heading-anchor BACKLOG.md regenerated (no functional change; just current status of all rows). Co-Authored-By: Claude <noreply@anthropic.com>
AceHack
added a commit
that referenced
this pull request
May 23, 2026
…ToyModel registry gap (#4783) Soraya's fifth autonomous routing tick (round 50, post-PR #4774 merge): sorry-bearing Lean artifact (ImaginaryStack/ToyModel.lean, 177 LOC, 7 sorry placeholders) with HaPPY-paper fidelity claim (Pastawski-Yoshida- Harlow-Preskill 2015, arXiv:1503.06237) but no row in verification- registry.md. Distinct from B-0709 (round-42, scope-expanded round-49): different axis. B-0709 = portfolio-coverage of TLA+/Alloy. This row = sorry-bearing Lean artifact with external-paper fidelity claim — paper-version-drift fails silently without a registry row to pin version + preconditions against. Soraya routing: Lean is correct primary; cost is at REGISTRY axis, not TOOL axis. TLA+-hammer guard: N/A (registry-discipline, not tool-routing). Effort: S. Assignee: kenji. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships Soraya findings as backlog rows immediately (no per-finding maintainer wait). Authored via git plumbing fallback (dotgit-saturation-resilient pattern) to avoid contention with peer Otto / Lior worktree-add cycles.
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
Files Soraya's three pending findings (rounds 43+44+45) as backlog rows in one cohesive PR, per Aaron's 2026-05-23 21:30Z policy-flip authorization ("lets try to keep things moving other than if we need budget increases") — Soraya findings flow through Otto (plumbing-commit-fallback) to backlog without per-finding maintainer pick; Aaron reviews aggregates only.
Three rows
B-0710 — DBSP chain rule BP-16 cross-check
B-0711 — Residuated FsCheck property file
src/Core/Residuated.fsis the ONLY CRDT-class file with zero FsCheck (sanity-checked across PNCounter, OrSet, Lww, GCounter, DeltaCrdt, Bloom, CountMin, Haar, HyperLogLog, HyperMinHash — all have tests)B-0712 — WitnessDurable commit protocol formal verification triple
Durability.fs:14-22self-declares TLA+ prereq; type itself is the gate (Savethrows until proven)Origin
Soraya's autonomous formal-verification routing loop started 2026-05-23 ~20:00Z. Rounds 42-45 produced four findings; round 42 already filed as B-0709 (merged earlier today). Rounds 43-45 stayed pending until Aaron's policy-flip authorization just now.
All assigned to kenji per Soraya's advisory-only authority constraint (she routes; Kenji or original spec owners author).
Commit details
6th plumbing-fallback PR this session — sibling pattern to #4755 / #4761 / #4762 / #4765 / #4772.
Test plan