Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .claude/board/ISSUES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
7 changes: 6 additions & 1 deletion .claude/board/LATEST_STATE.md
Original file line number Diff line number Diff line change
@@ -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`.
Expand Down
7 changes: 7 additions & 0 deletions .claude/board/PR_ARC_INVENTORY.md
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
4 changes: 2 additions & 2 deletions .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 |

Expand All @@ -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 |
Expand Down
2 changes: 1 addition & 1 deletion .claude/board/entries/2026-10-20-d-cmr-1-set-algebra.md
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
Loading