feat(openspec): Audit and move DBSP Operators spec (B-0171.4)

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.

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 == <<a, b, c>>
+
+(*
+    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))
+
+=============================================================================

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.