diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index 3cd0619fae..a3aea6561f 100644 --- a/docs/BACKLOG.md +++ b/docs/BACKLOG.md @@ -670,6 +670,9 @@ are closed (status: closed in frontmatter)._ - [x] **[B-0707](backlog/P2/B-0707-manifesto-citation-time-series-tracking-2026-05-23.md)** Manifesto citation time-series tracking — persistent snapshots + delta-over-time - [x] **[B-0708](backlog/P2/B-0708-stale-pointer-cleanup-from-razor-cadence-pass-2026-05-23.md)** Stale-pointer cleanup across `.claude/rules/` — 87 candidates surfaced by razor-cadence pass 2026-05-23 - [ ] **[B-0709](backlog/P2/B-0709-soraya-registry-coverage-drift-register-11-unregistered-specs-2026-05-23.md)** Soraya round-42 hand-off — register 11 unregistered formal-verification specs in verification-registry.md (Class 0 drift) +- [ ] **[B-0710](backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md)** Soraya round-43 hand-off — DBSP chain rule BP-16 cross-check (FsCheck cross-trace + Z3 pointwise lemma) +- [ ] **[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) ## P3 — convenience / deferred diff --git a/docs/backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md b/docs/backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md new file mode 100644 index 0000000000..881f9a4907 --- /dev/null +++ b/docs/backlog/P2/B-0710-soraya-round43-dbsp-chain-rule-bp16-cross-check-fscheck-z3-2026-05-23.md @@ -0,0 +1,68 @@ +--- +id: B-0710 +priority: P2 +status: open +title: "Soraya round-43 hand-off — DBSP chain rule BP-16 cross-check (FsCheck cross-trace + Z3 pointwise lemma)" +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: cross-check-gap +composes_with: + - tools/lean4/Lean4/DbspChainRule.lean + - docs/research/verification-registry.md + - tests/Tests.FSharp/Formal/Z3.Laws.Tests.fs +--- + +# B-0710 — DBSP chain rule BP-16 cross-check (round-43 hand-off) + +## Origin + +Soraya's second autonomous routing tick (2026-05-23 — round 43). Highest-leverage publication-readiness gap on the DBSP chain rule artifact per Aaron's DBSP-publication arc. + +## Finding + +`tools/lean4/Lean4/DbspChainRule.lean` has **ZERO BP-16 cross-checks**. Currently A-with-CI-green-since-2026-05-17 but single-tool (Lean only). Per BP-16, P0 invariants require ≥2 cross-checks. + +**Empirical**: + +- 17 theorems/lemmas in Lean artifact +- 0 hits for `chain_rule_proposition` / `Qdelta` / `Dop_LTI` in `tests/Tests.FSharp/Formal/Z3.Laws.Tests.fs` +- 0 hits across all 19 TLA+ specs in `tools/tla/specs/` + +**Historical anchor**: April 2026 Class 1 drift catch (`chain_rule` mis-named a Theorem-3.3 corollary as Proposition 3.2) is exhibit-A that single-tool review missed the failure mode the first time. Cross-check would have caught it independently. + +## Routing decision (Soraya) + +- Cross-check 2: **FsCheck cross-trace** on `Qdelta(Q1 ∘ Q2)(s) = Qdelta Q1 (Qdelta Q2 s)` at bounded depth. Effort: S. +- Cross-check 3: **Z3 pointwise lemma** on `D ∘ I = id` + `Dop_LTI_commute` arithmetic step (QF_LRA). Effort: S. + +## TLA+-hammer guard + +TLA+ was tempting. **REJECTED**: chain rule is a pointwise algebraic identity over operators, NOT a state-machine safety invariant. TLC would enumerate the product state space of two iterations and time out before catching the definitional-drift class. FsCheck + Z3 close the actual axes (real-code behaviour + arithmetic identity); TLA+ closes a different axis (interleaving) that nothing in the chain-rule statement depends on. + +## Acceptance criteria + +1. New FsCheck file `tests/Tests.FSharp/Formal/DbspChainRule.Properties.fs` (or extend existing Z3.Laws.Tests.fs) with property covering `chain_rule_proposition_3_2` and `Dop_LTI_commute` at bounded depth +2. Z3 lemma covering `D ∘ I = id` + `Dop_LTI_commute` arithmetic step (QF_LRA encoding) +3. Both cross-checks wired into CI (existing dotnet test gate is sufficient for FsCheck; Z3 may need explicit invocation) +4. `verification-registry.md` rows for `chain_rule_proposition_3_2` + `Dop_LTI_commute` updated to reflect 3-tool cross-check status + +## Publication-readiness alignment + +Per Soraya: "Single-tool evidence does not survive Budiu-grade peer review; converting from 'A-with-CI, single-tool' to 'A-with-CI, three-tool BP-16 compliant' is the line publication crosses." **This is the gap that gets the chain-rule artifact past the publication line** (after PR #4772 closed gaps #1+#2 — README + CI badge). + +## Effort + +S + S = total S+ (one evening per cross-check). Assignee: kenji. + +## Composes with + +- [`tools/lean4/Lean4/DbspChainRule.lean`](../../../tools/lean4/Lean4/DbspChainRule.lean) — the artifact needing cross-checks +- [`tools/lean4/README.md`](../../../tools/lean4/README.md) — landed via PR #4772; documents the artifact for reviewers +- [`docs/research/verification-registry.md`](../../research/verification-registry.md) — registry rows for `chain_rule_proposition_3_2` + `Dop_LTI_commute` +- [`docs/research/chain-rule-proof-log.md`](../../research/chain-rule-proof-log.md) — round-35 paper-drift audit substrate +- `memory/persona/soraya/NOTEBOOK.md` — Round 43 entry (pending NOTEBOOK update; locate by `## Round 43` heading once landed; pruned-preserved) diff --git a/docs/backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md b/docs/backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md new file mode 100644 index 0000000000..5f47d218e2 --- /dev/null +++ b/docs/backlog/P2/B-0711-soraya-round44-residuated-fscheck-property-file-2026-05-23.md @@ -0,0 +1,72 @@ +--- +id: B-0711 +priority: P2 +status: open +title: "Soraya round-44 hand-off — Residuated FsCheck property file (Galois + residual + retraction equivalence)" +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: cross-check-gap +composes_with: + - src/Core/Residuated.fs + - tests/Tests.FSharp/Crdt/PNCounter.Tests.fs + - docs/research/proof-tool-coverage.md +--- + +# B-0711 — Residuated FsCheck property file (round-44 hand-off) + +## Origin + +Soraya's third autonomous routing tick (2026-05-23 — round 44). Compound option (c+d): cross-check gap + publication-readiness on a genuine framework novelty. + +## Finding + +`src/Core/Residuated.fs` (129 LoC, `ResidualMax` IVM operator for O(log k) retraction of non-invertible aggregates like `max`) has **ZERO FsCheck properties**. + +**Sanity-checked across CRDT/sketch family**: PNCounter, OrSet, Lww, GCounter, DeltaCrdt, Bloom, CountMin, Haar, HyperLogLog, HyperMinHash all have FsCheck tests. **Residuated.fs is the ONLY CRDT-class file with zero FsCheck coverage**. + +Gap named in `docs/research/proof-tool-coverage.md` §5 since 2026-04-17; 30+ rounds open. + +## Routing decision (Soraya) + +Algebraic-law identity → **FsCheck primary** (mirrors `tests/Tests.FSharp/Crdt/PNCounter.Tests.fs` template). Three properties: + +1. **Galois connection**: `a·x ≤ b ⇔ x ≤ a\b` +2. **Residual under max**: `a\b = b if a≤b else a` +3. **Retraction equivalence**: `ResidualMax(insert+retract trace) = max(positive-only trace)` + +## Regression-guard urgency + +Round-17 history: `Residuated.fs` previously advertised "O(1) amortised" retraction that was actually O(n) under adversarial retract-top. Harsh-critic caught it. Current `SortedSet` revision is the fix. + +**Without a property test pinning the law, a future "perf optimization" can silently re-introduce the same correctness gap.** FsCheck IS the regression guard the round-17 incident asked for. + +## TLA+-hammer guard + +TLA+ was tempting (file carries internal state `SortedSet<'K>`). **REJECTED**: state is single-thread BST holding domain values; concurrency is at the circuit-runtime layer (covered by other specs). Property IS pointwise algebraic identity — FsCheck-shape, NOT TLC-shape. TLC would enumerate BST state space and time out. + +## Acceptance criteria + +1. New file `tests/Tests.FSharp/Algebra/Residuated.Tests.fs` mirroring `PNCounter.Tests.fs` shape +2. Three FsCheck properties covering Galois + residual + retraction equivalence +3. Tests wired into existing dotnet test gate — `tests/Tests.FSharp/Tests.FSharp.fsproj` uses explicit `` registration (96 entries; not glob-based), so the new file MUST be added to the `.fsproj` in the correct compile order alongside the other Crdt/Algebra entries; `dotnet test Zeta.sln -c Release` picks it up once registered +4. `proof-tool-coverage.md` §5 updated to mark Residuated FsCheck-covered + +## Publication-readiness alignment + +Per Soraya: "Residuated-lattice IVM is one of the framework's genuine novelties — citable if backed by a machine-checked property; currently ships with prose-only justification." SECOND publication-readiness gap alongside round-43 chain-rule. + +## Effort + +S (one evening). Assignee: kenji. + +## Composes with + +- [`src/Core/Residuated.fs`](../../../src/Core/Residuated.fs) — target needing FsCheck +- [`tests/Tests.FSharp/Crdt/PNCounter.Tests.fs`](../../../tests/Tests.FSharp/Crdt/PNCounter.Tests.fs) — template +- [`docs/research/proof-tool-coverage.md`](../../research/proof-tool-coverage.md) §5 — gap named since 2026-04-17 +- `memory/persona/soraya/NOTEBOOK.md` — Round 44 entry (pending NOTEBOOK update; locate by `## Round 44` heading once landed; pruned-preserved) diff --git a/docs/backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md b/docs/backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md new file mode 100644 index 0000000000..48442af83e --- /dev/null +++ b/docs/backlog/P2/B-0712-soraya-round45-witnessdurable-commit-protocol-tla-z3-fscheck-triple-2026-05-23.md @@ -0,0 +1,76 @@ +--- +id: B-0712 +priority: P2 +status: open +title: "Soraya round-45 hand-off — WitnessDurable commit protocol (TLA+ spec + Z3 quorum-arithmetic lemma + FsCheck cross-check)" +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: missing-routing-decision +composes_with: + - src/Core/Durability.fs + - docs/research/proof-tool-coverage.md + - tools/tla/specs/TwoPCSink.tla +--- + +# B-0712 — WitnessDurable commit protocol formal verification triple (round-45 hand-off) + +## Origin + +Soraya's fourth autonomous routing tick (2026-05-23 — round 45). Option (b) missing routing decision: a property class with NO tool wired in ANY surface. + +## Finding + +`src/Core/Durability.fs:14-22` carries a **self-declared formal-verification prereq**: + +> "`WitnessDurable` variant is a research target — the protocol has not been specified yet and there is no in-tree paper draft. It's defined here as a skeleton so callers can type against it. The implementing `WitnessDurableBackingStore` below throws on `Save` until the paper's protocol is fully implemented and TLA+-verified." + +**The type itself is the gate.** Substrate-verified: zero `.tla` files match `Witness*` / `Wdc*` / `Durab*` across all 19 specs in `tools/tla/specs/`. + +Gap named in `docs/research/proof-tool-coverage.md` §2 line 100 since 2026-04-17 (~5 weeks ago); untouched. + +## Routing decision (Soraya — P0 triple per BP-16 cross-check triage) + +Two property classes mixed; split obligations across tools: + +1. **(a) State-machine safety + concurrency race**: "Every acked `Save` survives witness-quorum failures under interleavings." + - **Primary tool**: TLA+/TLC + - **Scale**: 3 witnesses × 2 writers × 4 keys (mirrors `SpineAsyncProtocol`) + - **Effort**: M +2. **(b) Quorum-intersection arithmetic**: `N ≥ 2F+1`. + - **Primary tool**: Z3 (QF_LIA) + - **Effort**: S +3. **Cross-check (third leg)**: FsCheck firing the real F# `WitnessDurableBackingStore` under simulated witness failures, asserting the TLA+ invariant on the executing code path. + - **Effort**: S + +## TLA+-hammer guard + +TLA+ IS the right primary for (a). The guard fires the **INVERSE** direction: do NOT bundle (b)'s quorum arithmetic into the spec. TLC would enumerate the arithmetic state-space; Z3 closes it in seconds. **Split the obligations.** + +## Acceptance criteria + +1. New file `tools/tla/specs/WitnessDurable.tla` covering state-machine safety + concurrency interleaving (3w × 2w × 4k) +2. New Z3 lemma (either standalone or extension to existing Z3 test surface) proving quorum-intersection arithmetic `N ≥ 2F+1` +3. New FsCheck file `tests/Tests.FSharp/Storage/WitnessDurable.Properties.fs` (sibling of existing `tests/Tests.FSharp/Storage/Durability.Tests.fs` — no `Durability/` directory in current test layout) exercising the real `WitnessDurableBackingStore` under simulated witness failures; register via explicit `` in `tests/Tests.FSharp/Tests.FSharp.fsproj` +4. All 3 cross-checks land green in CI BEFORE the source-side `throw` gate in `Durability.fs:WitnessDurableBackingStore.Save` is removed +5. `verification-registry.md` row added for `WitnessDurable` with all 3 cross-check references + +## Structural cousin (reviewer reference) + +`tools/tla/specs/TwoPCSink.tla` — same pattern (commit protocol + quorum + interleaving). Reviewers will read both. + +## Effort + +M + S + S (total ~M+). Assignee: kenji. + +## Composes with + +- [`src/Core/Durability.fs`](../../../src/Core/Durability.fs):14-22 — self-declared TLA+ prereq +- [`docs/research/proof-tool-coverage.md`](../../research/proof-tool-coverage.md) §2 line 100 — gap named 2026-04-17 +- [`tools/tla/specs/TwoPCSink.tla`](../../../tools/tla/specs/TwoPCSink.tla) — structural cousin +- `memory/persona/soraya/NOTEBOOK.md` — Round 45 entry (pending NOTEBOOK update; locate by `## Round 45` heading once landed; pruned-preserved) +- B-0710 + B-0711 (sibling Soraya hand-offs from same session)