diff --git a/.claude/board/ISSUES.md b/.claude/board/ISSUES.md index b161dd94f..705dff450 100644 --- a/.claude/board/ISSUES.md +++ b/.claude/board/ISSUES.md @@ -78,7 +78,7 @@ ## ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN — `normalize` can leave a program wider than as written (2026-10-16) -**Status:** RESOLVED in PR (D-CMR-1, branch `claude/eager-albattani-iufugq`): absorption is matched against flattened sibling sets in `contract::set_algebra::normalize`; TEST-PINNED by `absorption_after_de_morgan_matches_flattened_siblings` (contract) and `tests/absorption_n17.rs` (relalg), both disable-verified red. **Was:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs). +**Status:** RESOLVED by #1644 (merged `c05a313`; holo-h14d-probe stage 1 now widens 0 of 2,000): absorption is matched against flattened sibling sets in `contract::set_algebra::normalize`; TEST-PINNED by `absorption_after_de_morgan_matches_flattened_siblings` (contract) and `tests/absorption_n17.rs` (relalg), both disable-verified red. **Was:** OPEN. **Basis:** MEASURED (D-HOLO-H14d stage 1, `crates/holo-h14d-probe`, 2 of 2,000 generated programs). - `¬(x ∧ (x ∨ y))` with `x = P1 ∧ P4` should reduce by absorption to `¬x = ¬P1 ∨ ¬P4`. `lance-graph-relalg::normalize` pushes the negation inward first (De Morgan), flattens, and returns `¬P1 ∨ ¬P4 ∨ ((¬P1 ∨ ¬P4) ∧ ¬P5 ∧ ¬P7)`: the dual absorption pattern `a ∨ (a ∧ b)` is present but `a` is spread across the flattened `Or`, so the rule no longer matches. - Consequence: the rewritten program needs more scratch slots than the original; the original answers, the rewrite is refused (`MAX_SLOTS` = 8). Answers are never wrong; only width. diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index e6a815869..366a29240 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,4 +1,9 @@ -## 2026-10-20 — D-CMR-1 / D-RA-2: single-table set algebra in the contract (in PR) +## 2026-10-21 — main after #1644 (merged `c05a313`) + +- **On main:** #1641 (D-RELALG-UNIFIED plan), #1643 (U1 `jc-batch-probe`, walk_mask follow-up), #1644 (D-CMR-1 / D-RA-2, `contract::set_algebra`; inventory delta below under 2026-10-20). +- holo-h14d-probe stage 1 after #1644: 0 of 2,000 programs widened by the rewrite (was 2). + +## 2026-10-20 — D-CMR-1 / D-RA-2: single-table set algebra in the contract (#1644, merged `c05a313`) - **Contract (new module):** `set_algebra::{SetExpr, Res, Cmp, normalize, Runs, OutOfUniverse}`. `SetExpr` = `All | Empty | Sym(u32) | Res(Res) | And | Or | Not`; `Sym` is an opaque two-valued set (no storage layout named), `Res` a residual predicate on one lane. `normalize` is the one implementation of the single-table rewrites (De Morgan, associative flattening, idempotence, complement pairs, per-lane interval fusion and merge, absorption matched against flattened siblings). `Runs` = sorted disjoint half-open row intervals with `∩ ∪ ∖` and `complement(universe)`, refused (`OutOfUniverse`) past the declared universe. No dependency added; no lowering, join or gather. - **relalg:** `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`) and delegates; public API unchanged; the 16 pre-existing tests pass unchanged. Closes `ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN` (N17). Entry `entries/2026-10-20-d-cmr-1-set-algebra.md`. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index 9f2eb51a7..473798b66 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,3 +1,10 @@ +## 2026-10-21 — lance-graph PR #1644 (merged `c05a313`, branch `claude/eager-albattani-iufugq`, head `6fc04a4`) — D-CMR-1 / D-RA-2: the contract owns single-table set algebra + +- **Added:** `lance_graph_contract::set_algebra::{SetExpr, Res, Cmp, normalize, Runs, OutOfUniverse}` (zero deps); relalg `tests/absorption_n17.rs`; entry `2026-10-20-d-cmr-1-set-algebra.md`. +- **Locked:** relalg's `normalize` converts `Rel` ⇄ `SetExpr` and delegates; its public API is unchanged and its 16 earlier tests pass unchanged. Absorption is matched against flattened siblings in two forms, which closes N17. `Runs` set operations are O(n+m). `complement` needs an explicit universe. crepe-plan-probe's N17 pin is flipped to `m_the_known_absorption_gap_is_closed_and_not_produced`. +- **Deferred / open:** D-CMR-6 catalogue (owner open); repointing crepe and Quack; measures on `Runs`. +- **Confidence:** measured. Bitset differential over 3,000 random expressions. Five disable runs, each red. holo-h14d-probe stage 1: widened by rewrite 0 of 2,000, against 2 before. + ## 2026-10-20 — lance-graph PR #1626 (merged `bc8012da`, branch `ccr-08f48cec-lbv9l4-amx`, head `2976e117`) — D-RMAP-2 §5a-AMX: the tile arm on the AMX tier - **Added:** D-RMAP-2 §5a-AMX (five runs on a host where ndarray reports `AMX TDPBF16PS`); entry `D-RMAP-2-AMX`; STATUS_BOARD D-RMAP-2 row. No code change. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 68d54c147..c439b4509 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -243,7 +243,7 @@ Plan: `.claude/plans/relalg-v1.md`. Crate: `crates/lance-graph-relalg` (own work | **D-HOLO-H14c** | Thought-first positional reads `Thought(t)[Table(a)[i] : Table(b)[i]]`: point projection, presence/Hamming populations through mask-risc, explicit terminal rows; memory and fragmentation of positional tables; Lance 13 masked I/O; coordinate identity across rewrites (sub-ids -1 … -6) | Measured 2026-10-15 (v4, entry 2026-10-15-d-holo-h14c-thought-first): acceptance A–E met (tables consulted == k for every U; k = 2 read at U = 31 0.90–1.16x U = 2); C vs B on query-shaped reads mixed; uniform 1 % positional tables ≈ 93x payload resident (flagged); Lance prediction holds (uniform 1 % mask 1.00x bytes, clustered 0.24x); stale maps omit silently, refused by the version check; returned to the operator | tables consulted == requested lanes for every touched count; at k = 2, U = 31 read <= 1.25x U = 2; populations load no value; no row materialized outside the terminal; no wrong coordinate across rewrites; Lance prediction (1 % uniform mask does not halve bytes_read, 1 % clustered does) | | **D-HOLO-H14d** | C's own operation in four stages, C only: (1) relalg symbolic reduction of the thought's set expression, (2) materialize `R = P_a ∧ P_b ∧ A` (or `∨`) over presence planes, (3) Lance 13 read pruned by `R`, (4) COUNT/EXISTS from `R` or the operation on `T_a[i], T_b[i]` for survivors; sub-ids -1 … -5 | Measured 2026-10-16 (v4, entry 2026-10-16-d-holo-h14d-logic-mask-read): stage 1 decides 675/2,000 programs with 0 runs, 396 answered only after the rewrite, 2 widened (ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN), passes 1,065 vs 5,898; R costs 2–10 ns per 64-address word; Lance scans exactly |R| everywhere, bytes 1.00x at uniform 1 % full tile, 0.19x clustered 1 %, 0.01–0.12x inside a 1,024/8,192 aperture; payload ~6 ns per lane load, reads == |R| × k, not flat at small |R| (fixed word scan; prediction 4 falsified); fused Σ ~1.3 ns per value; point query 8–45 ns hot; returned to the operator | `R` == per-address reference; rewritten == as written on 2,000 programs; payload reads == |R| × k; Lance rows == |R| with reference values; five disable runs red | | **D-RA-1** | `Rel` + `normalize` + `symbolic` + R2IL lowering | Shipped #1546 `c21bd165` (11 tests, 11 disable runs red; four comparisons on one lane 8 → 2 ops; 70/2,000 small descriptions refused as written, all run rewritten) | == row oracle over 400 generated descriptions × 5 measures | -| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). In PR with D-CMR-1: relalg `normalize` delegates to `contract::set_algebra::normalize`; repointing crepe follows D-CMR-6 | relalg tests pass unchanged against the contract IR | +| **D-RA-2** | Rules into the contract set IR (D-CMR-1/-6); relalg keeps only lowering or is deleted | DECISION 2026-10-20: option A, the contract owns the single-table set-algebra rewrites; relalg keeps relational planning, joins and lowering (`entries/2026-10-20-six-decisions.md` §2). No general relational AST for JC or Quack (`d-relalg-unified-v1.md` § Decisions). D-CMR-1 shipped (#1644): relalg `normalize` delegates to `contract::set_algebra::normalize`; repointing crepe follows D-CMR-6 | relalg tests pass unchanged against the contract IR | | **D-RA-3** | Datalog rules as algebra values; names are labels resolved through the label codebook, never strings in a rule — council v3 (2026-10-16) places the Datalog VALUES in `metta::datalog`; D-RA-2 still gates relalg | Queued (after D-RA-2) | codebook-built rules == hand-written `Rel`; unknown label refused at resolution | | **D-RA-4** | **⛔ VIOLATION — GATHER. DO NOT BUILD. CORRECT: D-HOLO-H14c / H14d.** Bound recursion via external frontier driver over D-CMR-5 preimage | Queued (after D-CMR-5) | == row-oracle closure; frontier past bound refused | @@ -254,7 +254,7 @@ Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RES | D-id | scope | status | gate / falsifier | |---|---|---|---| | **D-CMR-0** | Plan, identity matrix, inventory, board rows | Shipped #1532 (docs) | docs only; every inventory row cites code | -| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | In PR (branch `claude/eager-albattani-iufugq`): `contract::set_algebra::{SetExpr, Res, Runs, normalize}`; measures not yet (`entries/2026-10-20-d-cmr-1-set-algebra.md`) | algebra laws vs materialized bitsets as oracle | +| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | Shipped (#1644, `c05a313`): `contract::set_algebra::{SetExpr, Res, Runs, normalize}`; measures not yet (`entries/2026-10-20-d-cmr-1-set-algebra.md`) | algebra laws vs materialized bitsets as oracle | | **D-CMR-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | Queued (after D-CMR-1; lowering reaches mask-risc through core via `lance_graph::fold`, #1537 — there is no contract → mask-risc edge) | == row oracle; `Count` without residual reads zero rows | | **D-CMR-3** | Quack frontend: `Filter` → set IR (extent hoisting falls out) | Queued | identical answers on the quack suite; other-basis range stays residual | | **D-CMR-4** | Two dimensions: `Rect` over composite coordinates, row-major or Morton runs | Queued | rectangle ∩ == bitset oracle | diff --git a/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md index e86db05df..79bb27113 100644 --- a/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md +++ b/.claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md @@ -1,6 +1,6 @@ # 2026-10-20 — D-CMR-1 / D-RA-2: the contract owns single-table set algebra -**Status:** TEST-PINNED (in PR, branch `claude/eager-albattani-iufugq`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`). +**Status:** TEST-PINNED, merged in #1644 (`c05a313`). MEASURED after merge: holo-h14d-probe stage 1 widens 0 of 2,000 programs (was 2; `cargo test --manifest-path crates/holo-h14d-probe/Cargo.toml stage1_answers_agree -- --nocapture`). **Basis:** `ADR-2026-10-20-SIX` §2 (`entries/2026-10-20-six-decisions.md`). - **Moved:** relalg's rewrite rules to `lance_graph_contract::set_algebra::normalize`, unchanged except absorption. relalg's `normalize` converts `Rel` ↔ `SetExpr` (`Plane(i)` ↔ `Sym(i)`, `Atom` ↔ `Res`) and delegates. `symbolic`, `run`, lowering and the public API are unchanged. The contract stays dependency-free. - **Absorption** is matched against flattened sibling sets, removing one child at a time against the children still kept, in two forms: (1) a member of the dual child is a sibling, or a junction of siblings; (2) a sibling junction's members all occur in the dual child (`x ∨ (x ∧ y)` with `x` itself a conjunction). That closes N17 (`ISS-RELALG-ABSORPTION-AFTER-DE-MORGAN`) for `x` a leaf, an `And` or an `Or`. Form 2 was found by crepe-plan-probe's N17 pin (CI `probe`), which this PR flips to assert the reduction.