From f7def3d3fdc603d047dac80b33d93ed2217e6f75 Mon Sep 17 00:00:00 2001 From: Lior Date: Thu, 28 May 2026 13:09:33 -0400 Subject: [PATCH 1/2] feat(openspec): Audit and move DBSP Operators spec (B-0171.4) This change implements the final item from the OpenSpec catch-up Phase 1 audit. - Moves the existing 'DbspSpec.tla' into the OpenSpec framework at 'openspec/specs/dbsp-operators/'. - Creates a new README in the same directory to provide context for the TLA+ spec. - Creates the backlog item 'B-0171.4' to track the work. --- docs/backlog/P1/B-0171.4-author-dbsp-spec.md | 31 ++++++++ openspec/specs/dbsp-operators/DbspSpec.tla | 75 ++++++++++++++++++++ openspec/specs/dbsp-operators/README.md | 25 +++++++ 3 files changed, 131 insertions(+) create mode 100644 docs/backlog/P1/B-0171.4-author-dbsp-spec.md create mode 100644 openspec/specs/dbsp-operators/DbspSpec.tla create mode 100644 openspec/specs/dbsp-operators/README.md diff --git a/docs/backlog/P1/B-0171.4-author-dbsp-spec.md b/docs/backlog/P1/B-0171.4-author-dbsp-spec.md new file mode 100644 index 0000000000..73aec2f5ae --- /dev/null +++ b/docs/backlog/P1/B-0171.4-author-dbsp-spec.md @@ -0,0 +1,31 @@ +--- +id: B-0171.4 +priority: P1 +status: open +title: "OpenSpec catch-up - audit and update DBSP Operators spec" +created: 2026-05-28 +last_updated: 2026-05-28 +parent: B-0171 +depends_on: [B-0171.1] +classification: buildable-now +decomposition: atomic +owners: [lior] +type: spec-authoring +--- + +# B-0171.4 — Audit and update DBSP Operators spec + +This task implements the fourth and final item from the Phase 1 audit of the OpenSpec catch-up project (B-0171). It involves auditing the existing TLA+ spec for DBSP and moving it into the OpenSpec framework. + +## Scope + +This task is focused on bringing the existing `DbspSpec.tla` into the `openspec` directory and ensuring it is up-to-date. The work will involve: +- Moving `tools/tla/specs/DbspSpec.tla` to `openspec/specs/dbsp-operators/`. +- Creating a `README.md` in the same directory to provide context and explanation for the TLA+ spec. +- Auditing the spec for completeness against the current state of DBSP research in the repository. + +## Acceptance Criteria + +- The file `tools/tla/specs/DbspSpec.tla` is moved to `openspec/specs/dbsp-operators/DbspSpec.tla`. +- A new `README.md` file is created at `openspec/specs/dbsp-operators/README.md`. +- The README provides a high-level overview of the DBSP operators and explains the purpose of the TLA+ spec. diff --git a/openspec/specs/dbsp-operators/DbspSpec.tla b/openspec/specs/dbsp-operators/DbspSpec.tla new file mode 100644 index 0000000000..ebab582494 --- /dev/null +++ b/openspec/specs/dbsp-operators/DbspSpec.tla @@ -0,0 +1,75 @@ +------------------------------ MODULE DbspSpec ------------------------------ +(* + TLA+ specification of the DBSP algebraic axioms, checkable by TLC. + The "state" here is a tuple of arbitrary Z-sets picked non-deterministically; + TLC enumerates every combination and checks the invariants hold for each. + + Run with: + java -cp tla2tools.jar tlc2.TLC -config DbspSpec.cfg DbspSpec.tla + + At |K|=2, |W|={-2,-1,0,1,2}, TLC exhaustively verifies the axioms across + all 5^8 = 390 625 tuples of four Z-sets in under a second. +*) +EXTENDS Integers, FiniteSets, Sequences, TLC + +CONSTANTS + K, \* finite key domain + W \* finite weight domain (must include 0 + negatives) + +VARIABLES a, b, c + +vars == <> + +(* + Z-set = function K -> W. +*) +ZSet == [K -> W] + +EmptyZSet == [k \in K |-> 0] + +ZAdd(x, y) == [k \in K |-> x[k] + y[k]] +ZNeg(x) == [k \in K |-> -x[k]] +ZSub(x, y) == [k \in K |-> x[k] - y[k]] +ZDistinct(x) == [k \in K |-> IF x[k] > 0 THEN 1 ELSE 0] + +\* `H` — the incremental-distinct function from the paper (Proposition 4.7). +H(i, delta) == [k \in K |-> + IF i[k] > 0 /\ (i[k] + delta[k]) <= 0 THEN -1 + ELSE IF i[k] <= 0 /\ (i[k] + delta[k]) > 0 THEN 1 + ELSE 0] + +(* + State: three arbitrary Z-sets. TLC enumerates all combinations. +*) +Init == + /\ a \in ZSet + /\ b \in ZSet + /\ c \in ZSet + +Next == UNCHANGED vars + +Spec == Init /\ [][Next]_vars + +(* + ═══════════════════════════════════════════════════════════════════ + ═ DBSP axioms — exhaustive verification over finite W × K ═ + ═══════════════════════════════════════════════════════════════════ +*) + +\* Group axioms. +InvAssoc == ZAdd(ZAdd(a, b), c) = ZAdd(a, ZAdd(b, c)) +InvCommute == ZAdd(a, b) = ZAdd(b, a) +InvIdentity == ZAdd(a, EmptyZSet) = a +InvInverse == ZAdd(a, ZNeg(a)) = EmptyZSet +InvDoubleNeg == ZNeg(ZNeg(a)) = a +InvNegDistributes == ZNeg(ZAdd(a, b)) = ZAdd(ZNeg(a), ZNeg(b)) +InvSubIsAddNeg == ZSub(a, b) = ZAdd(a, ZNeg(b)) + +\* Distinct idempotence (Proposition A in the paper). +InvDistinctIdempotent == ZDistinct(ZDistinct(a)) = ZDistinct(a) + +\* Incremental distinct (Proposition 4.7, the H function) — this is the +\* crucial identity our `ZSet.distinctIncremental` must respect. +InvHCorrectness == ZDistinct(ZAdd(a, b)) = ZAdd(ZDistinct(a), H(a, b)) + +============================================================================= diff --git a/openspec/specs/dbsp-operators/README.md b/openspec/specs/dbsp-operators/README.md new file mode 100644 index 0000000000..da082c5798 --- /dev/null +++ b/openspec/specs/dbsp-operators/README.md @@ -0,0 +1,25 @@ +# OpenSpec: DBSP Operators + +This document provides context for the TLA+ specification of the DBSP (Differential Bulk Synchronous Parallel) operators. + +**Parent:** B-0171.4 + +## 1. Core Concept + +DBSP is a calculus for incremental computation on top of the Z-Set algebra. It provides a set of operators for expressing complex dataflows in a way that can be efficiently updated as the input data changes. + +The core of DBSP is the `D` (differentiate) and `I` (integrate) operators, which allow for the transformation of streams of changes. The formal properties of these operators are what allow for efficient, incremental view maintenance. + +## 2. TLA+ Specification + +The formal specification of the core DBSP algebraic axioms is located in `DbspSpec.tla`. This spec uses the TLA+ model checker to exhaustively verify the correctness of the axioms over a finite domain. + +### 2.1. Key Invariants Verified + +The TLA+ spec verifies several key invariants, including: + +- **Group Axioms:** It confirms that Z-Sets form an Abelian group under the `add` operation. +- **`distinct` Idempotence:** It verifies that `distinct(distinct(a)) = distinct(a)`. +- **Incremental `distinct` Correctness:** It verifies the correctness of the incremental `distinct` operator (`H` function), which is a cornerstone of efficient DBSP computation. + +This formal verification provides a high degree of confidence in the correctness of the foundational algebra upon which the Zeta factory's data processing is built. From 30d728298bb53da0668949b7be9eb259b9fdad4a Mon Sep 17 00:00:00 2001 From: "Otto-CLI (Claude)" Date: Fri, 29 May 2026 01:33:48 -0400 Subject: [PATCH 2/2] fix(openspec): markdownlint MD032 + canonical DBSP expansion (B-0171.4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mechanical review-fixes on Lior's PR #5886 (Otto-CLI assisting per operator background-worker brief; additive commit, no force): - docs/backlog/P1/B-0171.4-author-dbsp-spec.md:22-23 — add blank line before list (MD032/blanks-around-lists); this was the only REQUIRED gate blocker (lint markdownlint). - openspec/specs/dbsp-operators/README.md:3 — correct DBSP expansion from 'Differential Bulk Synchronous Parallel' (0 occurrences in repo) to 'Database Stream Processing' (canonical repo form; resolves Copilot thread). Design-level Copilot threads (move-vs-copy semantics, .cfg colocation, OpenSpec spec.md/profiles placement) left for Lior — they touch PR design intent with TLC-runner blast radius and are not Otto's to decide unilaterally. Forward-signal comment posted on the PR. Co-Authored-By: Claude Opus 4.8 --- docs/backlog/P1/B-0171.4-author-dbsp-spec.md | 1 + openspec/specs/dbsp-operators/README.md | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/backlog/P1/B-0171.4-author-dbsp-spec.md b/docs/backlog/P1/B-0171.4-author-dbsp-spec.md index 73aec2f5ae..b1be20e3a5 100644 --- a/docs/backlog/P1/B-0171.4-author-dbsp-spec.md +++ b/docs/backlog/P1/B-0171.4-author-dbsp-spec.md @@ -20,6 +20,7 @@ This task implements the fourth and final item from the Phase 1 audit of the Ope ## Scope This task is focused on bringing the existing `DbspSpec.tla` into the `openspec` directory and ensuring it is up-to-date. The work will involve: + - Moving `tools/tla/specs/DbspSpec.tla` to `openspec/specs/dbsp-operators/`. - Creating a `README.md` in the same directory to provide context and explanation for the TLA+ spec. - Auditing the spec for completeness against the current state of DBSP research in the repository. diff --git a/openspec/specs/dbsp-operators/README.md b/openspec/specs/dbsp-operators/README.md index da082c5798..5e8464b734 100644 --- a/openspec/specs/dbsp-operators/README.md +++ b/openspec/specs/dbsp-operators/README.md @@ -1,6 +1,6 @@ # OpenSpec: DBSP Operators -This document provides context for the TLA+ specification of the DBSP (Differential Bulk Synchronous Parallel) operators. +This document provides context for the TLA+ specification of the DBSP (Database Stream Processing) operators. **Parent:** B-0171.4