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
3 changes: 2 additions & 1 deletion .claude/board/STATUS_BOARD.md
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,8 @@ Plans in #1667 (`d-rft-relalg-thought-git-frontier-v1.md`, `d-qsp-classview-quac
|---|---|---|---|
| **D-RFT-0 / D-QSP-0** | K3 normalization safety: rewrites keep SQL three-valued TRUE rows | Shipped (#1668; EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/031`; `entries/2026-10-21-d-rft-0-kleene-normalization.md`): `normalize_kleene`; `SetNormalize` admits it under `ThreeValued`. MEASURED: PostgreSQL 16.14 = Kleene oracle = `normalize_kleene` on 2000/2000; the two-valued form is wrong on 474 | Kleene evaluator over random expressions + PostgreSQL differential; 5 disables red. Remainder open: NULL literals, `COALESCE`, nullable arithmetic, empty `SUM`, `COUNT(expr)` |
| **D-QSP-0 remainder, slice 1** | scalar aggregates under SQL NULL: empty / all-NULL `SUM` is NULL, `COUNT(x)` vs `COUNT(*)`, MIN/MAX/AVG | In PR (EXO-50 claim `session_013z2e1YXkm6o6HNrDn5BPWA/026`; `entries/2026-10-21-d-qsp-0-scalar-aggregates-null.md`): Quack `lower_sum` + `sum_finish` over existing terminals. MEASURED: PostgreSQL 16.15 = Quack = Kleene oracle on 3600/3600 queries | `tests/sql_aggregate_null.rs` (4 disables red); `examples/qsp_agg_pg_parity.rs` (SKIP without a server) |
| **D-RFT-1..5, D-LFA-0** | composition, substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
| **D-RFT-1** | typed composition: membership × role carriers over one slot coordinate; Distinct/Bag from the cardinality witness; NULL key matches nothing; XOR, seal mismatch, stale binding, bag overflow refused | In PR, PROBE (EXO-50 claim `session_01G22yT6htkcdyXsihxxXdrg/036`; `crates/dir-rmap-probe/src/compose.rs`; `entries/2026-10-21-d-rft-1-typed-composition.md`). r2il polyfill: `IntXor`, `ANY`, `ALL` + procedures. MEASURED: PostgreSQL 16.14 lane equal over 600 users × 64 roles, bag 1421 = `count(*)`, distinct 1374 = `count(DISTINCT)`; composition 310 µs vs the same plan in direct SIMD 14 µs | IAM diamond (Bag 2, Distinct 1); independent DFS oracle lane-equal; 7 compose + 5 r2il disables red |
| **D-RFT-2..5, D-LFA-0** | substitution, recursion, frontier, replay; flow census | PROPOSAL (`entries/2026-10-21-d-rft-d-lfa-0-assessment.md`) | per-row falsifiers in the entry; unclaimed |
| **D-LFA-1 / D-LFA-2** (amended 2026-10-21) | guarded-control verification of a Rubicon flow; integration with the existing drivers | PROPOSAL (plan amendment, `d-lfa-…-v1.md` § Amendment 2026-10-21; map `entries/2026-10-21-coresearch-plans-mapping-foresight.md`) | GKAT equivalence + separate no-commit-without-revision-and-MUL trace check; 3 disables; `GoTo`/`GoBack` refused; unclaimed |
| **D-GKAT-0** | GKAT fixture probe: G1 factoring, G2 nondeterminism refusal, G5 declared atom bound | In PR, PROBE (EXO-50 claim `session_01VncKoyG6JkpsoqhqTGTv3f/026`; `crates/gkat-probe`; `entries/2026-10-21-d-gkat-0-probe.md`). TEST-PINNED: Rubicon reference ≡ optimized, both safe; CHECK-authorized flows equivalent and unsafe; ≤ 8 tests (256 atoms) else refused | 3 flow disables + 11 checker disables red; independent bounded oracle; not a production verifier |

Expand Down
101 changes: 101 additions & 0 deletions .claude/board/entries/2026-10-21-d-rft-1-typed-composition.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
# 2026-10-21 — D-RFT-1-COMPOSE: typed composition over the DR256 slot coordinate (D-RFT-1)

**Status:** PROBE (lab, `crates/dir-rmap-probe`). TEST-PINNED and MEASURED as stated below; no production ABI changes.
**Claim:** EXO-50 `session_01G22yT6htkcdyXsihxxXdrg/036`, status in `/038`.
**Plan:** `.claude/plans/d-rft-relalg-thought-git-frontier-v1.md` (D-RFT-1); assessment `entries/2026-10-21-d-rft-d-lfa-0-assessment.md`.

## What landed

**`dir-rmap-probe::compose`.** It composes user → group membership (`Page.member`) with the role carriers (`Qr.role_slots`, and `Qr.role` for the slot-major direction).
- Both operands share one coordinate, the 256 slots, and one `Witness`.
- Per coordinate (user `i`, role `r`), the path mask is `member_i ∧ valid_i ∧ carriers_r`.
- Bag is the path count and Distinct is its existence. They are two readings of one computation, never two computations.

**Laws, each TEST-PINNED with a disable that goes red:**

| law | how |
|---|---|
| Stratum comes from a witness, not the caller | Distinct when the left fan (present keys per user) or the right fan (carrier slots per role) is ≤ 1, else Bag |
| A NULL key matches nothing | a key whose payload bit is set but whose presence bit is clear contributes no path (the same model as Quack's validity plane) |
| XOR is refused | an even number of parallel paths would read 0, an answer neither stratum gives |
| Seal mismatch is refused | the two operands were bound to different registers |
| A stale binding is refused | the caller's current `Witness` differs from the binding's |
| A page answers only for its own binding | `Page` carries the `Witness` it was resolved against; an old page beside a newly bound register is a seal mismatch |
| The bag sum is checked | `add_bag` refuses a wrap |
| The IAM diamond | two direct groups reaching one role: Bag 2, Distinct 1 |

**Execution.** Every count, existence and mask equality is an r2il procedure. Each is compiled once by `FoldDialect` and replayed through mask-risc `execute_into` over zero-copy row slices (a prepared statement):

| step | procedure | rows |
|---|---|---|
| present keys | `keep(intersect(member_i, valid_i))` | 256 slots |
| support (the user's roles) | `keep(union(role[s] for s in present_i))` | 64 roles |
| path count, support coordinates only | `count_and(member_i, valid_i, carriers_r)` | 256 slots |
| distinct | `count` over the support plane | `users × 64` |

Coordinates outside the support have no path by construction and are never evaluated. The probe has no counting loop of its own. The two pointer tables, of present slots and of supported roles, are the inversion from a plane to its local positions.

**r2il polyfill** (`lance-graph-r2il`):
- `IntXor` (R2IL ordinal 22) lowers to `MaskOp::Xor`, or to `BoolExpr::Xor` when fused.
- `ANY` and `ALL` lower to `Terminal::Any`/`All` and push 1 or 0.
- New procedures: `exists`, `all`, `differ` (`IntXor` then `ANY`, mask equality as a fold), `intersect`, `union`, `keep`, `count_and`.
- 5 r2il disables go red.

## Evidence

- **Independent oracle.** A depth-first walk over the `Prepared` CSRs (nesting restricted to security groups), not `Qr`'s Warshall closure. It is compared lane to lane over every page of `Spec::small()`, with supports compared by `differ`. Anti-vacuity: coordinates with count 1 and with count ≥ 2 both occur.
- **PostgreSQL 16.14** (`examples/rft1_pg_parity.rs`, with a recursive CTE): the per-coordinate lane is equal over 600 users × 64 roles; bag 1421 = `count(*)` and distinct 1374 = `count(DISTINCT (u, role))`. Every 7th user also has a membership row with a NULL group, which matches nothing in PostgreSQL either.
- **Disables.** 7 on compose (valid plane ignored, stratum forced to Bag, seal check, stale check, unchecked bag, support loop truncated, union dropping keys) plus 5 on r2il. All red.

## Measured (`examples/rft1_bench.rs`, release, median of 101 runs, 600 users / 3 pages)

| step / arm | time | allocations per run |
|---|---|---|
| bind (`Qr::bind`) | 46 µs | |
| pages | 39 µs | |
| program prep (`Composer::new`) | 1.4 µs | |
| A — composition (r2il procedures through mask-risc) | 310 µs | 39 |
| C — every coordinate, direct `ndarray::simd` | 131 µs | 0 |
| C+ — A's support-first plan, direct `ndarray::simd` | 14 µs | 0 |
| B — tuple baseline, LAB ONLY, not a candidate | 134–146 µs | 10 |

All arms agree on (bag, distinct) before anything is timed.

**History:** the first wiring ran one r2il fold per (user, role) coordinate and took 17 ms with 78 210 allocations. The fold count was the cause, not the algebra.

## Open

- **Per-execution cost.** A − C+ is about 296 µs for about 2 600 executions, roughly 115 ns of fixed cost per mask-risc `execute_into` on 4-word planes. The plan and the answers are the same, so the gap is execution overhead. UNKNOWN which part dominates (validation, scratch carving, tile loop); not profiled.
- **No count-product terminal.** mask-risc has no terminal that produces many coordinates' counts in one execution (a bit-matrix count product, or a masked positional popcount). The support-first plan is what keeps the execution count down. ndarray has no positional popcount either.
- **Fused wide chains.** `union`/`intersect` reuse two scratch slots in `BoolMode::InPlace` (`call_owned`), so a user with any number of present groups composes. In `BoolMode::Fused` a 24-leaf chain is refused (`ScratchBufferTooSmall`): mask-risc's `fuse` gives each ternlog group its own slot. Pinned as a refusal; not changed here.
- **Fixture scale.** `Spec::iam(8000)` exceeds 256 security slots (`Refusal::TooLarge`), so the bench runs `Spec::small()`.
- **Not done:** recursion over composed strata (D-RFT-3), a second composition law beyond Count/Exists, and a PostgreSQL arm in CI (the example prints SKIP without a server).

## Update — PostgreSQL primitive polyfill (bingo card, same PR)

Each PostgreSQL primitive is either an r2il opcode the dialect now lowers, or a procedure (a call sequence that adds no opcode). WHERE-shaped primitives leave a mask. Kept with `KEEP`, that mask is a Lance 13 read mask: `with_row_addr_prefilter(RowAddrMask)`, which `crepe-plan-probe` (#1633) measured as scanning exactly the masked rows (P2). Aggregates leave a scalar.

| PostgreSQL | r2il | status |
|---|---|---|
| `=`, `<`, `<=`, `>`, `>=` (int) | `IntEqual`, `IntSLess`, `and_cmp_i32` | existing |
| `IS NULL` / `IS NOT NULL` | `is_null` / `is_not_null` over the presence plane | NEW (proc) |
| `BETWEEN` (NULL dropped, empty range keeps nothing) | `and_between_i32` | NEW (proc) |
| `IN (…)`, `IN ()` | `in_u32` | NEW (proc) |
| `COUNT(*)` / `COUNT(x)` | `count` / `count_valid` | NEW: `count_valid` |
| `SUM`, `MIN`, `MAX` | `sum`, `min`, `max` | existing |
| `AVG` | `avg_parts` (SUM and COUNT; `avg(int)` is `numeric`, so the caller divides) | NEW (proc) |
| `COUNT(DISTINCT k)` on a key-ordered lane | `KEY_RUNS` → `CountKeyRunsU32`; `count_distinct_sorted` | NEW (opcode + proc); an unordered lane is refused |
| `bool_or` / `bool_and` (`every`) | `bool_or` / `bool_and` | NEW (proc); an empty selection reads 0 / 1 where PostgreSQL reads NULL |
| `EXISTS` / `NOT EXISTS` | `exists` (`ANY`) / `not_exists` | NEW |
| `INTERSECT` / `UNION` / `EXCEPT` (same rows) | `intersect` / `union` / `except` | NEW |
| `UNION ALL` counts | `count_union_all` (`IntAdd`) | NEW |
| bigint `+`, `*`, `/` on aggregates | `IntAdd`, `IntMult`, `IntSDiv`, checked | NEW (opcodes); overflow and division by zero refused |

Tests: one row-rule reference per primitive (`postgresql_primitives_match_row_rule_references`), the unordered-lane refusal, and the arithmetic refusals. 6 disables, all red: no division-by-zero guard, wrapping add, `COUNT(x)` ignoring presence, exclusive `BETWEEN` upper bound, `EXCEPT` without its NOT, and `KEY_RUNS` counting rows.

**Not on the card** (open):
- K3 `NOT IN (…, NULL)` and `IS DISTINCT FROM`: Quack `sql_where` holds the (T, F) pair, and r2il procedures are two-valued.
- `CASE` (`BLEND`) and grouped `COUNT` (`GroupReduce`): not wired.
- `COUNT(DISTINCT)` on an unordered lane: no seen-set by design.
- `ORDER BY` / `LIMIT`, string predicates, nullable arithmetic, `COALESCE`.
- A PostgreSQL differential for the new procedures: the references are row rules, not a server.
3 changes: 2 additions & 1 deletion .claude/board/entries/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately
opposite directions; the stranding this convention prevents shows up in
exactly one of them, never both.

423 entries, 2026-08-06 .. 2026-10-21.
424 entries, 2026-08-06 .. 2026-10-21.

| date | entry id | finding | file |
|---|---|---|---|
Expand All @@ -42,6 +42,7 @@ exactly one of them, never both.
| 2026-10-21 | `D-RU-6-LAB-2` | | [2026-10-21-d-ru-6-sparse-compute.md](2026-10-21-d-ru-6-sparse-compute.md) |
| 2026-10-21 | `D-RU-6-LAB-3` | | [2026-10-21-d-ru-6-dirty-frontier.md](2026-10-21-d-ru-6-dirty-frontier.md) |
| 2026-10-21 | `D-RFT-1` | | [2026-10-21-d-rft-d-lfa-0-assessment.md](2026-10-21-d-rft-d-lfa-0-assessment.md) |
| 2026-10-21 | `D-RFT-1-COMPOSE` | | [2026-10-21-d-rft-1-typed-composition.md](2026-10-21-d-rft-1-typed-composition.md) |
| 2026-10-21 | `D-RFT-0` | | [2026-10-21-d-rft-0-kleene-normalization.md](2026-10-21-d-rft-0-kleene-normalization.md) |
| 2026-10-21 | `D-RA-2` | | [2026-10-21-d-ra-2-relalg-symbolic-repoint.md](2026-10-21-d-ra-2-relalg-symbolic-repoint.md) |
| 2026-10-21 | `D-QSP` | | [2026-10-21-d-qsp-d-rft-d-lfa-classview-quack-plan.md](2026-10-21-d-qsp-d-rft-d-lfa-classview-quack-plan.md) |
Expand Down
2 changes: 1 addition & 1 deletion .claude/plans/metta-datalog-assimilation-v1-council-v3.md
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ F12. No model identifier in any committed artifact; status words are `MEASURED/V
| `crates/lance-graph-relalg/Cargo.toml` deps: mask-risc, r2il, ogar-loco, ogar-r2il (git main) | no quack, no contract direct | dependency decision below (R-2) |
| `crates/lance-graph-quack/src/lib.rs:340` `pub enum Filter` (`EqU32Via` :358, `Semijoin { fk, foreign }` :387; `pub fn lower` :1383; `pub struct Query` :1301); deps mask-risc + contract only | the SHIPPED hop lowering (D-MTP-1 used it: `crates/lance-graph-metta/examples/join_probe.rs:1-12,27,75-79`) | parity oracle for D-ASM-2's `Program` bytes |
| `crates/lance-graph-mask-risc/src/ir.rs:127-205` `Pred` (incl. `EqU32Via{fk,key,v} :158`, `Range :180`, `EqU32Strided :184`, `MatchFacet16Strided :200`); `:210-287` `MaskOp` (incl. `Gather :277`); `:288-470` `Terminal` (incl. `Count :290`, `Keep :321`, `ScatterOrU32 :338`, `ScatterCountU32 :364`, `CountKeyRunsU32 :389`, `GroupSumI32 :399`, `GroupReduce :442`, `GroupPowerSumsI32 :465`) | the whole word set D-ASM-2/3 may use | F2: nothing added without proof |
| `crates/lance-graph-r2il/src/lib.rs:260` `pub struct FoldDialect` (`new(planes, foreign)` :327, `with_keep` :366, `last_program` :447, `emit_pred` :589) | the only path relalg takes to a `Program` | gate G4 (byte-identical `Program`) reads `last_program()` |
| `crates/lance-graph-r2il/src/lib.rs` `pub struct FoldDialect` (`new(planes, foreign)`, `with_keep`, `last_program`, `emit_pred`) | the only path relalg takes to a `Program` | gate G4 (byte-identical `Program`) reads `last_program()` |
| `crates/lance-graph-metta/Cargo.toml` deps: mask-risc, quack; dev datafrog (fork master); `src/lib.rs` 7 lines (stub); `examples/common/mod.rs:23 Relation2`, `:46 ingest`, `:139 pairs`, `:180 preimage`, `:200 range_pairs`, `:236 oracle`; `examples/join_probe.rs`, `join_range_probe.rs` | D-MTP-1/1b probes, MEASURED; no `Space` impl yet; no hyperon dependency yet | D-ASM-1/4 land here |
| `crates/lance-graph-nal/src/lib.rs:94` `pub enum Copula` (Inheritance=1, Similarity=2, Implication=3, Equivalence=4; `Statement` :117, `Belief` :130, `guid` :157-170 = `FacetCascade::from_semantic_tiles([class>>16, class, s, copula, p, id, 0, 0])`, `WEIGHT_SCALE/HORIZON/MAX_CONFIDENCE_CODE/evidence classes` :212-244, `NalError` :494-530, 10 variants counted 2026-10-16) | arity-2 fact already laid out as 6 u16 tiles + 2 spare | D-ASM-1 reuses the tile layout for `(f a₁…aₖ)`, k ≤ 5 |
| `crates/lance-graph-contract/src/nars.rs:12` `pub enum InferenceType` (Deduction, Induction, Abduction, Revision, Synthesis; doc drift: described as CAM search modes) | out of tranche; inventory §6 item | non-goal here |
Expand Down
4 changes: 4 additions & 0 deletions .github/workflows/dir-rmap-probe.yml
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,8 @@ on:
- crates/lance-graph-dir-sim/**
- crates/lance-graph-quack/**
- crates/lance-graph-mask-risc/**
- crates/lance-graph-r2il/**
- crates/lance-graph-contract/**
- .github/workflows/dir-rmap-probe.yml
- rust-toolchain.toml
push:
Expand All @@ -21,6 +23,8 @@ on:
- crates/lance-graph-dir-sim/**
- crates/lance-graph-quack/**
- crates/lance-graph-mask-risc/**
- crates/lance-graph-r2il/**
- crates/lance-graph-contract/**
- .github/workflows/dir-rmap-probe.yml
- rust-toolchain.toml
workflow_dispatch:
Expand Down
15 changes: 14 additions & 1 deletion crates/dir-rmap-probe/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,12 @@ ndarray = { git = "https://github.com/AdaWorldAPI/ndarray", branch = "master", d
# fixture's own integer ids (never dir-sim ordinals). AdaWorldAPI fork, by
# branch (no pins), as in crepe-plan-probe.
crepe = { git = "https://github.com/AdaWorldAPI/crepe", branch = "ccr-d3ce1263-ied9yh" }
# D-RFT-1 (src/compose.rs): every count, existence and mask equality of the
# composition is an r2il procedure (`count_and`, `count`, `differ`) folded by
# mask-risc. The probe holds no counting loop of its own.
lance-graph-r2il = { path = "../lance-graph-r2il" }
# The planes a FoldDialect folds over (`Planes`, `Foreign`).
lance-graph-mask-risc = { path = "../lance-graph-mask-risc" }

# Same patches as lance-graph-dir-sim: one ndarray identity, and the OGAR
# sibling checkout so a paired OGAR change is tested before it merges.
Expand All @@ -43,7 +49,6 @@ lance-graph-contract = { path = "../lance-graph-contract" }
# a population is lent as a `Rel::Plane` and folded by relalg's existing
# mask-risc lowering. No evaluator of the probe's own.
lance-graph-relalg = { path = "../lance-graph-relalg" }
lance-graph-mask-risc = { path = "../lance-graph-mask-risc" }

[patch."https://github.com/AdaWorldAPI/ndarray"]
ndarray = { path = "../../../ndarray" }
Expand All @@ -53,3 +58,11 @@ ogar-dir-core = { path = "../../../OGAR/crates/ogar-dir-core" }
ogar-dir-sim = { path = "../../../OGAR/crates/ogar-dir-sim" }
ogar-ad = { path = "../../../OGAR/crates/ogar-ad" }
ogar-az = { path = "../../../OGAR/crates/ogar-az" }
ogar-loco = { path = "../../../OGAR/crates/ogar-loco" }
ogar-r2il = { path = "../../../OGAR/crates/ogar-r2il" }

# ogar-loco / ogar-r2il take the contract by git `main`; map it onto the
# in-tree crate so the graph holds one contract (the lance-graph root does
# the same).
[patch."https://github.com/AdaWorldAPI/lance-graph"]
lance-graph-contract = { path = "../lance-graph-contract" }
Loading
Loading