diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index ff37d79d8..eb4050f40 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,17 @@ +## 2026-10-13 (1) — d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result → `.claude/plans/d-cmr-concept-chain-normalization-v1.md` + +**Status:** PROPOSAL D-CMR-0..9, revised to a set-theory IR (see the last bullet). Only D-CMR-0 (plan, board rows) is in the PR; no code, no dependency. + +- Methods in a pure chain are unresolved relations; the chain is normalized with proven identities and only the irreducible remainder is compiled. `(a+b)−a` means `a+b` never exists, not a wider accumulator. +- Inventory, read in code: `fold_ranges`, survivor skip, `sql_where`, ternlog fusion, `Lowering::Range` (Count/Any only), `Compiled`, `execute_extent`. Quack never emits an extent; NAL does by hand (127 ns vs 195 µs). +- Path: extent hoisting in Quack (D-CMR-1), lazy binding (-2), fixpoint driver (-3), complement (-4), relational difference `Sum(A)−Sum(A∧B)=Sum(A∧¬B)` (-5), equality-saturation probe only on evidence (-6), benchmark against eager materialization and the row loop (-7). +- Revision (same day): the normalization lives in a set-theory IR in the contract (sets with a universe, interval runs as values, 2-D rectangles, preimage, measures; edges, not content), with an insufficiency proof in §3.1. Measurement levels: geometry (no row read), optics (fused filter + count, nothing written), etch (materialize). Path recut to D-CMR-1..9. Reverses point 3 of the concept-chain rule. +- Revision 2 (same day, aligned with the eight-point ruling): the set IR is the shared semantic domain of normalization, not a frontend syntax; Quack's `Filter` stays home for Quack compositions, NAL stays on R2IL; shared are the rules, their preconditions and costs. The IR describes and never executes (enforced by a test). Lowering in core, algebra in the contract. +- Corrections to the 2026-10-12 entries below, made by #1524 (D-CMR-RESET); code is on `backup/session-011BMJ-2026-10-12`: + - (6) sag-capstone-alignment: both `ProposedMethod` anchors are gone (`glove-parity::awareness::Candidate`, `glove-parity::method::EffectClass::Propose`). The name and the two shapes stand; the anchors are re-decided with the D-CMR rebuild. Not the Cohen's-d `EffectClass` in `lance-graph-cognitive`, which is unrelated. + - (5) sag-reflexive-cognition: `MethodTable` and `SoftwareGraph` are no longer shipped; nothing in that plan can reuse them until the rebuild. + - (4) software-awareness-graph: withdrawn with the whole method layer; D-SAG-1-0..6 are Withdrawn on `STATUS_BOARD.md`. + ## 2026-10-12 (6) — sag-capstone-alignment-v1 — one alignment over the six SAG research PRs (#1510, #1511, #1512, #1513, #1515, #1517) → `.claude/plans/sag-capstone-alignment-v1.md` **Status:** CURRENT-CONTRACT for naming and vocabulary; nothing built. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index bf43fd205..b89a798b7 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,20 @@ +## D-CMR — Concept-chain normalization: preserve the equation, not the intermediate result (2026-10-13) + +Plan: `.claude/plans/d-cmr-concept-chain-normalization-v1.md`. Parent: D-CMR-RESET. One new IR (set theory, plan §3.1 insufficiency proof); no method-body algebra, no dependency. + +| D-id | scope | status | gate / falsifier | +|---|---|---|---| +| **D-CMR-0** | Plan, identity matrix, inventory, board rows | In PR | docs only; every inventory row cites code | +| **D-CMR-1** | Set-theory IR core in the contract: `Runs` (∩ ∪ ∖, complement), residual `Res`, measures; pure | Queued | algebra laws vs materialized bitsets as oracle | +| **D-CMR-2** | Lowering: runs → extents, residual → predicates per run; measurement levels geometry / optics / etch | Queued (after contract → mask-risc) | == 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 | +| **D-CMR-5** | Preimage `f⁻¹(S)` under a proven mapping (the hop) | Queued | == row oracle; many-to-one image refused | +| **D-CMR-6** | Rule catalogue + fixpoint driver: complement, relational difference | Queued | Experiments A, D, E; each guard removal fails | +| **D-CMR-7** | NAL frontend: aperture → `Runs` | Queued (after NAL lands in core) | NAL W2 tests unchanged | +| **D-CMR-8** | Equality-saturation probe (`egg`/`egglog` as references) | Queued (only if rules compete) | compared against D-CMR-6; no dependency without evidence | +| **D-CMR-9** | Benchmark: eager materialization vs set IR vs row loop | Queued | answers asserted before timing; tier from the build's report | + ## D-SAG-5 — Reflexive cognition and proposal safety from SAG #1509 (2026-10-12) **Status:** PROPOSAL. Plan: .claude/plans/sag-reflexive-cognition-from-1509-v1.md. Docs only; no runtime authorization. diff --git a/.claude/board/SUPERSESSION-INDEX.md b/.claude/board/SUPERSESSION-INDEX.md index 8657cc50b..0867eef6d 100644 --- a/.claude/board/SUPERSESSION-INDEX.md +++ b/.claude/board/SUPERSESSION-INDEX.md @@ -56,7 +56,7 @@ coverage instead. | `persist_cycle` | BLOCKED | — | 12 | 8 | 5 | | `CognitiveMarkers` | REPURPOSE | `Commit` | 1 | 0 | 0 | | `DominoCascade` | REPURPOSE | `Commit` | 7 | 1 | 0 | -| `GateDecision` | REPURPOSE | — | 25 | 28 | 25 | +| `GateDecision` | REPURPOSE | — | 25 | 29 | 26 | | `GateState` | REPURPOSE | — | 14 | 1 | 1 | | `MergeMode` | REPURPOSE | — | 8 | 14 | 13 | | `ResonanceDto` | REPURPOSE | `PerturbationDto` | 2 | 12 | 7 | @@ -64,7 +64,7 @@ coverage instead. | `CollapseGateEmission` | RETIRE | — | 5 | 14 | 12 | | `ThinkingStyle` | RETIRE-toward-contract | — | 53 | 28 | 24 | -## Table 2 — plans naming a ruled symbol without citing the ruling (76) +## Table 2 — plans naming a ruled symbol without citing the ruling (77) Route is **mechanical triage, not a verdict**: `ARCHIVE?` = the plan's own status says it shipped; `RESCOPE` = it targets a symbol marked RETIRE; `READ` = neither signal fires @@ -96,6 +96,7 @@ a licence to act on it. | **READ** | `persistence-artifact-backed-commit-v1` | `persist_cycle` | RATIFIED (operator ruling 2026-08-09). Phase | 0/0 | | **READ** | `post-teardown-buildup-survey-v1` | `StepMask` | SURVEY, read-only, plan-only (no code, no te | 2/5 | | **READ** | `r2il-bpe-typed-genetic-recombination-v1` | `GateDecision` | PROPOSAL, §7's three falsifiers now RUN (see | 1/1 | +| **READ** | `sag-capstone-alignment-v1` | `GateDecision` | CURRENT-CONTRACT for the documents it aligns | 7/13 | | **READ** | `scientific-kg-substrate-v1` | `GateDecision` | PROPOSED — **scoping doc**, no code. Records | 3/9 | | **READ** | `self-reasoning-substrate-v1` | `GateDecision` | PROPOSED — doc-only. No code, no contract ch | 4/5 | | **READ** | `v3-convergence-wiring-v1` | `GateDecision` | ACTIVE (2026-07-01). Operator: "I'm all in f | 0/0 | @@ -158,5 +159,5 @@ a licence to act on it. - **ARCHIVE?**: 0 - **RESCOPE**: 56 -- **READ**: 20 +- **READ**: 21 - ruled symbols tracked: 14 diff --git a/.claude/board/entries/2026-10-12-session-reset-inventory.md b/.claude/board/entries/2026-10-12-session-reset-inventory.md index 9a9a2e5ea..c478b43af 100644 --- a/.claude/board/entries/2026-10-12-session-reset-inventory.md +++ b/.claude/board/entries/2026-10-12-session-reset-inventory.md @@ -9,6 +9,21 @@ for the row loop (1,048,576 rows, AVX-512, release). Its hops were foreign-key reads; the graph has none. Everything here is moved to backup and rebuilt. +**Root cause (2026-10-13, VERIFIED-IN-CODE on the backup branch):** each +method was evaluated on its own, so a chain never existed as one expression +that could be simplified before execution. +1. *Materialized per call:* `run_quack` (old `method.rs:788`) built a fresh + population-sized `Scratch::for_program(program, n_rows)` on every call and + ran the tiled path; `Compiled` and `Lowering::Range` were never used. +2. *Gather stacking instead of differences:* hops were per-row key reads + (`Relation { fk }`, `ForeignLane`, `Cond::Reaches/Via`), stacked further by + the chained gather (#358, #1522); cost grew with rows × hops. The tree already + intersects ranges symbolically (`fold_ranges`, quack `lib.rs:1918`) and + answers `Count` as `hi − lo` (`Lowering::Range`). +3. *Optimized in the wrong place:* the care went into identity structures + (`MethodKey`, the FNV body digest, `SchemaSeal`, linear `digests` search, + `edges.retain`), not into the data path. Their own cost was not measured. + ## Where the old state lives | repo | branch | what | @@ -52,5 +67,53 @@ hops are coordinate-range intersections inside the same program. A fold that does not exist is reported as a gap in the fold catalogue, not built in the method layer. -OPEN: #1523 anchors `ProposedMethod` on `awareness::Candidate`, which this -reset removes; the anchor moves to the rebuilt binding. +**Concept chains (DECISION 2026-10-13; SCOPE: the D-CMR rebuild and every +composition of pure methods; BASIS: the root cause above; REVISIT WHEN a rule +needs information no existing IR can carry).** Methods in a pure chain are +unresolved relations, not executions. The whole chain is normalized before +lowering; only the irreducible remainder becomes a `Compiled` program. +1. A chained method returns a relation, never an intermediate population. +2. Normalization uses proven identities only: intersections, complements, + differences, coordinate transformations, Boolean truth tables (ternlog), + applicable law tables. +3. Existing IRs and folds only. Quack's `Filter`/`Query` tree holds + Quack-bound chains; global NAL methods stay R2IL-bound and are not routed + through Quack. No second method algebra, no new universal IR. + ⊘ 2026-10-13: the "no new universal IR" half is superseded by one + set-theory IR (`plans/d-cmr-concept-chain-normalization-v1.md` §3, with + its insufficiency proof); Quack and NAL become frontends lowering into it. + "No second method algebra" stands. +4. `SUM` first uses the existing fold over the minimized extent. A prefix lane + (`P[hi] − P[lo]`) is a separate, measured candidate with its own ordering, + overflow, NULL, update and maintenance laws. +5. A coordinate is valid only under a proven ordering or index mapping. + Constraints on one coordinate basis intersect symbolically; different bases + need a checked transformation or an index; otherwise the predicate is a + residual over the already-reduced extent. Two fields never share an order + by assumption. +6. Rules compile once; parameter bounds bind per call as a small boundary + computation, with no population scan and no materialized mask. +7. Every rewrite is checked against the unrewritten form and an independent + row oracle. Disabling an optimization leaves the answer unchanged; removing + a required semantic guard (three-valued logic, bag vs set, overflow) must + produce a failing counterexample. +8. A missing law is a rule-catalogue gap; a missing fold is a physical-catalogue + gap. Neither is built as an executor in the method layer. + +**Test cases to port into the rebuild** (on `backup/session-011BMJ-2026-10-12`, +`8ae5bce`, under `crates/lance-graph-glove-parity/tests/`): `polyfill.rs` (15 +tests, NARS revision as data; W3 of #42), `ordered.rs` (3, MIN/MAX), +`distinct.rs` (6, distinct hop targets), `relation.rs` (8, functional +relations), `awareness.rs` (19, the H1 candidate). They call the removed +`MethodBody` API, so each case is re-expressed against a `Compiled` program, +and its row-loop answer is re-read and re-run before it counts as an oracle. + +OPEN: #1523 anchors `ProposedMethod` on two removed types: the rewrite shape +on `glove-parity::awareness::Candidate`, the action shape on +`glove-parity::method::EffectClass::Propose` (not the unrelated Cohen's d +`EffectClass` in `lance-graph-cognitive`). The rewrite anchor moves to the +rebuilt binding. The action anchor is the action gate: a `Pending` +`ActionInvocation`. Today two methods advance it: `commit_via` (no admin +bypass) and `commit` (admin bypass). Which one a proposal must pass is OPEN +(capstone §2.1 item 7, which also lists +what the gate does not carry yet). diff --git a/.claude/knowledge/software-awareness-provenance-parity.md b/.claude/knowledge/software-awareness-provenance-parity.md index d852e6109..829960b73 100644 --- a/.claude/knowledge/software-awareness-provenance-parity.md +++ b/.claude/knowledge/software-awareness-provenance-parity.md @@ -3,6 +3,8 @@ **Type:** cross-repo method and validation checklist. **READ BY:** anyone changing SoftwareGraph/MethodTable, Ruff SPO/AST frontends, SAG prediction loops, OGAR ActionDef, Quack/R2IL or NARS evidence. **Status:** proposed guardrail, with source-grounded possible defects to *test*, not confirmed bugs. +> ⊘ 2026-10-13: `SoftwareGraph` and `MethodTable` (`lance-graph-glove-parity`'s `method.rs` / `awareness.rs`) were removed from `main` by #1524 (D-CMR-RESET); the code is on `backup/session-011BMJ-2026-10-12`. Wherever this doc names them, read them as the withdrawn first build. The separation-of-concerns rules still apply to the D-CMR rebuild, whose binding replaces them. + ## Separation of concerns | Question | Evidence source | Permitted conclusion | @@ -75,7 +77,7 @@ If a new result cannot be expressed through existing Quack/OGAR/R2IL, return an - [#1504 method parity](https://github.com/AdaWorldAPI/lance-graph/pull/1504) - [#1506 DAG range](https://github.com/AdaWorldAPI/lance-graph/pull/1506) - [#1508 predicate reuse](https://github.com/AdaWorldAPI/lance-graph/pull/1508) -- [#1509 SoftwareGraph](https://github.com/AdaWorldAPI/lance-graph/pull/1509) +- [#1509 SoftwareGraph](https://github.com/AdaWorldAPI/lance-graph/pull/1509) (withdrawn by #1524; backup branch above) - [Ruff #117 ordered behavioral ore](https://github.com/AdaWorldAPI/ruff/pull/117) - [Ruff #118 C linkage semantics](https://github.com/AdaWorldAPI/ruff/pull/118) - [Ruff #120 Odoo inherit_id](https://github.com/AdaWorldAPI/ruff/pull/120) diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md new file mode 100644 index 000000000..7668eb0f3 --- /dev/null +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -0,0 +1,279 @@ +# d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result + +**Status:** PROPOSAL (D-CMR-0..9). Only D-CMR-0 (this document and its board +rows) is in the PR that adds it. No code, no dependency. +**Revision 2026-10-13:** the normalization gets one new IR, a set-theory IR +(§3). This reverses point 3 of the concept-chain rule in the reset entry +("no new universal IR"); §3.1 is the insufficiency proof that justifies it. +**Revision 2, 2026-10-13 (aligned with the eight-point ruling):** the set IR +is the shared *semantic domain* of normalization, not a third frontend +syntax. Quack's `Filter`/`Query` stays the home of Quack compositions and NAL +stays on R2IL. What is shared is the rule catalogue: identities, their +preconditions and their cost effects, plus the set values they compute over. +**DECISION:** the IR describes and never executes. Thinking in abstract +relations before materializing is the point; what #1524 removed was a layer +that executed early. §3.1 justifies the IR; it is not a review gate. +**Date:** 2026-10-13. **Repo:** lance-graph (Quack, mask-risc, core NAL module). +**Parents:** D-CMR-RESET (`entries/2026-10-12-session-reset-inventory.md`, +root cause and the eight-point concept-chain rule), #1524, #1532. + +## 1. Definition + +A method in a pure chain contributes an unresolved relation, never a computed +intermediate. The chain stays unresolved until normalization has seen every +relation in it. Normalization applies proven identities; only the irreducible +remainder is lowered, once, into a `Compiled` program. + +The test case is `(a+b)−a`. It does not mean "accumulate `a+b` in a wider +register". It means `a+b` never has to exist: the identity leaves `b`. A wider +accumulator only repairs a step that did not need to happen. + +The goal is not faster or more precise intermediate steps. It is to find which +steps survive once the chain is simplified. + +## 2. Inventory: normalization that exists today (VERIFIED-IN-CODE, `c157c0a`) + +| mechanism | where | what it does | limit | +|---|---|---|---| +| `fold_ranges` | quack `lib.rs:1918`, called by `lower_with` (`:1956`), so by every Quack lowering | `Range ∧ Range → Range` via `max(lo)`, `min(hi)` | same `col`, siblings of one `AND`; no `OR`/`NOT` crossing | +| survivor skip, `gate_walk` + `hoist_gate_subset` | quack `:2026`, `:2010` | evaluates the rest of an `AND` only under an established gate | one gate per `AND` path | +| `sql_where` | quack `:549` | rewrites a filter into SQL three-valued `WHERE` for listed nullable columns | a semantic guard source, not a simplification; NULL literals, `COALESCE`, nullable arithmetic out of scope | +| `fuse` / `emit_fused` | mask-risc `fuse.rs:194`, quack `:2314` | any Boolean subtree over ≤ 3 leaves → one ternlog table | `lower_fused` only | +| lowering recognition | mask-risc `ir.rs:1349` | `Range` (`Count`/`Any` as `hi − lo`), `Ternlog`, `TernlogKeep`, `Tern2`, `Tern3`, else `Tiled` | `Range` folds only `Count` and `Any` | +| `Compiled` / `execute_compiled` | mask-risc `ir.rs:1388`, `exec.rs:1469` | recognize once, execute many times | — | +| `execute_extent` | mask-risc `exec.rs:1393` | runs a program over a row range | **Quack never emits an extent** (`lower_with` returns only a `Program`; no "extent" in `quack/src/lib.rs`). NAL uses it by hand via `bound_aperture` (`ordered_lane.rs:344`): 127 ns as extent vs 195 µs as an ANDed mask at 1,048,576 rows | +| aggregate laws | quack `lower_avg` (`:1522`, SUM+COUNT); `Terminal::merge_group_sink`; `PowerSums::checked_merge` | combine partial aggregates by each fold's own law | — | +| arithmetic semantics of folds | ndarray `masked_sum_i32` (exact `i64` over `i32` rows); keyed sums `wrapping_add` | fixes which cancellations are exact | no value-arithmetic IR anywhere (NAL §4 C, D-SQLP nullable arithmetic: OPEN) | + +So `(a+b)−a` has no home today at the value level. It appears first at the +aggregate level: `Sum(A) − Sum(A∧B) = Sum(A∧¬B)`. + +## 3. The set-theory IR + +### 3.1 Why a new IR (insufficiency proof, VERIFIED-IN-CODE at `c157c0a`) + +Everything set-like in the tree is either a predicate or a materialized bitset: +- Quack's `Filter` is predicates, lowered straight to masks. `fold_ranges` + yields at most one interval per column, never merges ranges under `Or`, and + its doc names `col` as the only order identity. +- `EvidenceMask` (`revision.rs:31`, `union`/`intersection`/`difference`) and + mask-risc masks are set algebra after materialization. +- `WideFieldMask` (`intersect`/`difference`) is sets of fields, not of rows. +- No interval-set type exists anywhere in `crates/`. + +Four things therefore have no home: +1. **The universe of a set:** which proven ordering (coordinate basis) of + which population it lives in. +2. **An intersection result as a value** before materialization: empty, one + point, one interval, or several disjoint intervals. +3. **Mappings between universes:** a hop is the preimage `f⁻¹(S)`, not a + stacked key read. +4. **Measures as functions of a set:** `Count(S)`, `Sum_x(S)`, `Exists(S)`, + computed from the set's description where that description is known. + +The IR exists only to hold these four. It is not a second method algebra and +not a second executor: execution stays in mask-risc. This is enforced by a +test, not by convention: the IR module holds no row data and calls no +mask-risc execution function; its only output is a normalized description +handed to lowering. + +### 3.2 The IR + +``` +U_b universe over basis b (a proven ordering of one population) +S ::= ∅ + | [lo,hi)_b interval; a point is [p, p+1) + | Runs_b{[l1,h1), …} sorted, disjoint intervals (one scanline) + | Rect_{b1×b2} product of intervals over a composite coordinate + | Res_b(p) residual: an opaque predicate over basis b + | S ∩ S | S ∪ S | U_b ∖ S + | f⁻¹(S') preimage under a proven mapping b → b' +M ::= Count(S) | Sum_x(S) | Exists(S) +``` + +- **Normal form:** `Runs_b ∩ Res_b`. Interval sets are closed under `∩`, `∪` + and `∖` at a cost linear in the number of intervals, with no row read; `∅` + is a proof that the answer is 0. The residual stays opaque. +- **Edges, not content.** A set is stored by its boundaries. Interval-only + operations scale with the number of edges, never with rows. Evaluating a + residual and lowering a rectangle (one run per `hi`) scale with the rows or + coordinate extent they visit. +- **Two dimensions.** A condition on `hi` and one on `lo` of a composite + coordinate (`hi·stride + lo`, the `_pair` family) form a rectangle. It + becomes 1-D runs only at lowering: one run per `hi` in row-major order, or a + few aligned runs in Morton order (`mask_shift_morton`, the HHTL prefixes). +- **Limits the IR enforces:** two-valued only (three-valued logic is resolved + by `sql_where` into the TRUE set first; complements only over two-valued + sets); sets, not bags (preimage gives a set; the image of a many-to-one + mapping is refused and stays a physical aggregation); intersection only + within one universe, otherwise through a proven `f`, otherwise residual. +- **Home:** the algebra lives in `lance-graph-contract`, next to `ClassView`, + and needs no dependency (the contract's `Cargo.toml` stays dependency-free). + Lowering lives in core, which depends on mask-risc, Quack and R2IL (the + other session's step (b)); it is never in the contract. +- **Frontends keep their representations.** A normalization pass over Quack's + `Filter` (and later over NAL's R2IL program) computes set values in this + domain with the shared rules: ranges on a proven basis become `Runs`, + everything else stays residual. The frontend tree is rewritten to the + irreducible remainder; neither frontend implements intervals of its own. + +### 3.3 The lithography reading + +A chip is designed as set algebra over polygon edges, entirely before any wafer +is exposed. A transistor exists where poly ∩ active is non-empty; a via where +metal1 ∩ via ∩ metal2 is. Layout tools compute layer booleans on edges with a +scanline, at a cost in edges, never in area. Rasterization happens once, in the +mask writer, at the end; exposure processes only the final mask. + +| lithography | IR | +|---|---| +| wafer and its coordinate frame | `U_b` | +| one mask layer | a set `S`, stored as edges | +| device = layer intersection | `∩`, possibly empty, one point or many | +| positive / negative resist | `S` / `U_b ∖ S` | +| etch / deposit | `∖` / `∪` | +| overlay alignment between layers | intersection only within one basis or through a proven `f` | +| layer booleans and design-rule checks | normalization | +| optical proximity correction tables | the rule catalogue (§3.5) | +| rasterization in the mask writer | lowering to mask words, once | +| exposure and etch | execution in mask-risc | +| minimum feature size, writer grid | one row; 64-row words (an unaligned edge costs an edge merge, `execute_extent` doc) | + +The withdrawn method layer exposed and etched each layer before the design was +complete, then tried to combine the etched wafers. + +### 3.4 Measurement levels (the laser-filter reading) + +A measure is light through a stack of masks onto a detector: light passes only +where every mask is open, so the stack forms the intersection and the detector +integrates it. Three levels, cheapest first; lowering picks the first that +applies: + +| level | when | how | in the tree | +|---|---|---|---| +| 1. geometry, no light | no residual | `Count(Runs) = Σ(hᵢ − lᵢ)`; `Exists = Runs ≠ ∅` | `Lowering::Range` (one interval, `Count`/`Any`) | +| 2. optics, no etch | residual present, caller needs a measure | residual predicates fused into one filter, one pass per run as extent, nothing written | **resident planes only:** `mask_ternlog_popcount`, `Lowering::Ternlog` → `Count`, `execute_extent`. A residual *comparison* is a `Pred`, which `fused_ternlog` declines (`ir.rs` doc), so it takes `Lowering::Tiled` and writes scratch. Predicate fusion is missing (part of D-CMR-2) | +| 3. etch | caller needs the set itself | materialize the mask for the surviving runs only | `Keep` / `Out::Mask` | + +`Sum_x(S)` is a graded filter: the existing masked sum fold over the runs as +extents (level 2). A prefix lane would move it to level 1; it stays a separate, +measured candidate. + +### 3.5 Rule catalogue (the Tafelwerk) over the set IR + +A rule is an identity, not a stored result: pattern, semantic preconditions, +rewrite, proof (independent oracle plus a negative control), cost effect, +scope. The key is the pattern **and** its preconditions. Rules are applied +until none fires or a step budget is reached, and none may increase the size of +the expression. Heuristics order rules; they never replace a proof. + +The mechanism has three known parts, used in this order and only as far as +measured need goes: **constraint propagation** (narrow bounds, detect `∅`, the +interval part of `fold_ranges` generalized), **term rewriting** with the +catalogue, and **cost-based selection** among valid forms. Equality saturation +(egg, egglog) keeps competing forms instead of committing to one; it is a +research reference (D-CMR-8), justified only if a bounded local rewriter +measurably commits to worse forms. Rules found automatically (Ruler) are +candidates only, admitted after validation under the type, overflow and NULL +conditions of §4. + +## 4. Identity matrix with semantic conditions + +| identity | legal when | illegal when | +|---|---|---| +| `(a+b)−a → b` | exact integers; wrapping two's complement (a group mod 2⁶⁴) | checked arithmetic (removes an overflow the original would report); IEEE stepwise rounding (unless an exact-expression contract is declared) | +| `Sum(A) − Sum(A∧B) → Sum(A∧¬B)` | exact `i64` sums of `i32` within the row bound; wrapping sums | the `_sym` family (`SYM_EMPTY_I64` marks "no row", not a value); three-valued `B` | +| `⋂[lo,hi) → [max lo, min hi)` | same proven coordinate basis | different orderings; a bound past `n_rows` | +| `Count([lo,hi)) → max(0, hi−lo)` | valid interval on the population's own row order | bag after fan-out | +| `Count(¬A) → N − Count(A)` | two-valued `A`, fixed universe `N` | `A` may be UNKNOWN; `N` not the same population | +| `Sum([lo,hi)) → P[hi] − P[lo]` | a prefix lane exists, cannot overflow, matches the snapshot | the population changed since `P` was built | +| `A∧A → A`, absorption, De Morgan, ≤ 6 planes → truth tables | two-valued planes | three-valued leaves without `sql_where` | +| `hi·stride+lo` as one coordinate | `lo < stride` (enforced: ndarray `group_of` drops `lo ≥ stride`), no overflow | otherwise | +| NAL truth laws | the W4 law representation, parity in codes | before W4 | + +**Numeric contract today:** mask-risc sums are exact (`i32` into `i64`, row +count bounded so the total cannot overflow, `ir.rs:296`, `:461`); there is no +floating point on the surface. The IR therefore assumes exact integers and +refuses any other operand. A per-method declaration of numeric rules is added +when the first floating-point or quantized column arrives, not before. + +## 5. Symbolic preservation is not numerical precision + +- **Exact semantic preservation:** the rewritten form gives the same result + under the original contract. Allowed silently. +- **Explicit semantic refinement:** a newly declared exact-expression contract + delays rounding or quantization to a named boundary. Allowed only where + declared, never inferred from "the result looks more accurate". + +## 6. Implementation path + +| D-id | step | gate / falsifier | +|---|---|---| +| D-CMR-1 | **Set IR core** in the contract: `Runs` with `∩ ∪ ∖` and complement, `Res`, measures; pure, no lowering | algebra laws (closure, distributivity, De Morgan, `∅`) checked against materialized bitsets as oracle on random and edge-case runs | +| D-CMR-2 | **Lowering** to mask-risc: runs → extents, residual → predicates within each run, the three measurement levels. Level 2 for residual comparisons needs predicate fusion in mask-risc (`fused_ternlog` declines `Pred` today) | == row oracle; a `Count` with no residual reads zero rows (instrumented); disabling level 1 or 2 keeps answers | +| D-CMR-3 | **Quack normalization pass:** over `Filter`, computing set values (ranges on a proven basis → `Runs`, other leaves → `Res`, `sql_where` first). Extent hoisting falls out of this (Experiment C) | answers identical to today's `lower` path on the quack suite; a range on another basis stays residual (negative control) | +| D-CMR-4 | **Two dimensions:** `Rect` over composite coordinates, linearized row-major or in Morton order | rectangle `∩` == bitset oracle; run count within the stated bound | +| D-CMR-5 | **Preimage** `f⁻¹(S)` under a proven mapping (the hop) | == row oracle; a many-to-one image is refused | +| D-CMR-6 | **Rule catalogue and fixpoint driver**: complement, relational difference `Sum(A) − Sum(A∧B) → Sum(A∧¬B)` | Experiments A, D, E; each guard removal fails | +| D-CMR-7 | **NAL normalization pass:** aperture → `Runs` over the R2IL program, R2IL route unchanged (after NAL lands in core) | NAL W2 tests unchanged | +| D-CMR-8 | **Equality-saturation probe** (`egg`, `egglog` as references only) | only if rules compete; compared against D-CMR-6; no dependency without evidence | +| D-CMR-9 | **Benchmark** (section 8) | answers asserted before timing | + +Compile-time normalization is separate from runtime binding: a parameter +known only per call (W3's range) is bound per call with a small boundary +calculation, never a population scan, a materialized mask or a re-lowering. + +Prefix lanes stay a separate, measured candidate (ordering, overflow, NULL, +update and maintenance laws), never a precondition for `SUM`. + +## 7. Experiments, each with an independent oracle and a negative control + +- **A. Cancellation.** At the aggregate level: `Sum(A) − Sum(A∧B)` against + `Sum(A∧¬B)` and an exact `i128` oracle; an eager variant accumulating into + `i32` shows the loss. Under checked arithmetic the rewrite must refuse. +- **B. Range intersection.** k compatible ranges intersect before any row is + read. Baseline: `fold_ranges` and `Lowering::Range` (tests at quack + `lib.rs:5204–5248`). +- **C. Mixed.** A sorted-coordinate range plus an unsorted value predicate: + the range becomes `Runs` and the extent, the predicate stays `Res` and is + measured at level 2 (D-CMR-2, D-CMR-3). +- **D. Composition.** Two identities on one expression, the second enabled by + the first (intersection, then `Count = hi − lo`). +- **E. Invalid rewrites.** NULL, overflow, incompatible coordinates, IEEE + rounding, impure operations: each refuses or keeps the original. + +Every rule: disabling the optimization leaves the answer; removing the +required semantic guard produces a failing counterexample. + +## 8. Benchmark plan + +Three arms on the same data: eager materialization (one mask per link, AND, +fold), the normalized chain, and the plain row loop (the performance floor: +the withdrawn layer measured 430–480 µs against 283 µs). Report rows scanned, +bytes materialized, preparation cost, per-call boundary cost and latency; +median of 101, tier named from the build's own report, answers asserted first. + +## 9. Gap ledger + +| item | state | +|---|---| +| range intersection within one `AND` | SHIPPED (`fold_ranges`) | +| `Count`/`Any` over a range without row reads | SHIPPED (`Lowering::Range`) | +| ≤ 6-plane Boolean → truth tables | SHIPPED (`Ternlog`/`Tern2`/`Tern3`) | +| compile once | SHIPPED (`Compiled`) | +| range as execution extent | SHIPPED in mask-risc and NAL; **missing in Quack** (D-CMR-3) | +| fused filter + count without writing a mask (level 2) | SHIPPED for resident planes only; **missing for residual comparisons** (`fused_ternlog` declines `Pred`, so they run tiled) — D-CMR-2 | +| sets with a universe, interval sets as values | OPEN (D-CMR-1) | +| multi-run extents, two-dimensional sets, preimage | OPEN (D-CMR-2, -4, -5) | +| chains composed before lowering | OPEN (D-CMR-3, -7) | +| repeated rule application, complement, relational difference | OPEN (D-CMR-6) | +| prefix aggregates | candidate | +| value-arithmetic IR (`a+b` as an expression) | OPEN, shared with NAL §4 C and D-SQLP | +| equality saturation | research (D-CMR-8) | + +## 10. Ownership + +- D-CMR-1 (pure algebra in the contract) can start now. +- D-CMR-2 lives in core and needs core's dependency on mask-risc, Quack and R2IL (step (b)); no contract dependency is needed. +- D-CMR-3..6 touch quack; D-CMR-7 waits until NAL lands in core. +- Owner to be assigned. diff --git a/.claude/plans/iam-substrate-sag-dir-sim-v1.md b/.claude/plans/iam-substrate-sag-dir-sim-v1.md index 0db00dee3..311f7beb7 100644 --- a/.claude/plans/iam-substrate-sag-dir-sim-v1.md +++ b/.claude/plans/iam-substrate-sag-dir-sim-v1.md @@ -26,7 +26,7 @@ Three distinct questions must survive every projection: | `dir-sim/src/actors.rs` | `GroupRoles::from_policy`, `role_evidence` and `RoleImpact::between`; SID/security-group paths; `Held/NotHeld/Undetermined/NotDeclared` | Role evidence is version-specific and role-scope binding is consumer-owned; don't reinterpret a distribution group as a security group | | `dir-sim/src/log.rs`, `image.rs`, `lance-graph-dir-sim-lance` | Persist/replay ingredients with logical VersionId distinct from Lance batch versions; torn-save refusal contract | Availability in production does not imply multi-system transaction or tenant snapshot equivalence | | `crates/lance-graph-contract/src/hotplug.rs` and `class_view.rs` | Per-plug authority activation, checked reading, ordered field basis, WideFieldMask | WideFieldMask is field selection, not row-RBAC or access verdict; slab physical reading is distinct from semantic view | -| `crates/lance-graph-glove-parity/src/awareness.rs` (#1509) | `SoftwareGraph::project` from prepared MethodTable; method/field/program/capability/refusal edges with tier and provenance; Quack Binder | In-memory one-hop projection, caller-supplied revision, limited digest; neither a directory membership store nor persistent general graph engine | +| `crates/lance-graph-glove-parity/src/awareness.rs` (#1509) — ⊘ removed by #1524 (D-CMR-RESET), code on `backup/session-011BMJ-2026-10-12` | `SoftwareGraph::project` from prepared MethodTable; method/field/program/capability/refusal edges with tier and provenance; Quack Binder | In-memory one-hop projection, caller-supplied revision, limited digest; neither a directory membership store nor persistent general graph engine | | `crates/lance-graph-quack/src/bind.rs`, `crates/lance-graph-r2il` | `Draft::bind`, Quack lowering into mask-risc; R2IL FoldDialect execution over borrowed planes | Multi-hop relation composition not automatically solved; cannot carry result masks as an undeclared population between programs | | `crates/lance-graph-rbac`, OGAR `GroupRolePolicy` | Separate policy authority and scope/grant primitives | Not an entitlement-certification UI or PDP/PEP for arbitrary external systems | | OGAR MethodDecl / `ogar-loco` Inventory / class-method RFC | Source method metadata and keyed body inventory exist; binding composer proposed | `MethodDecl::body_source` is not an executable method; no implicit DO capability | @@ -105,7 +105,11 @@ class Grant { policy, witnesses, effective_during } class Change { preview, validate, approve, execute, verify, revert } ``` -**Execution class:** these are main's shipped `EffectClass::{Pure, ReadVersion, Propose, ExternalMutate}` (`method.rs`); use those names. `Pure` uses existing Quack/R2IL and dir_sim primitives. `Propose` builds a `ProposedMethod` and is legal only on an Action body; every call on it refuses with `NotPure`. `ExternalMutate` is not a Quack opcode and must refuse unless independently authorized, with fresh source preconditions and external connector attestation. An absent field, alias, authority, schema seal, body, read scope, source version, evidence completeness or capability causes an explicit typed refusal. + + +> ⊘ 2026-10-13: this type is no longer on `main`. `glove-parity::method::EffectClass` was removed by #1524 (D-CMR-RESET) and is on `backup/session-011BMJ-2026-10-12`; the four names stand as vocabulary until the D-CMR rebuild chooses an anchor. (Not the `EffectClass` still on `main` at `crates/lance-graph-cognitive/src/search/certificate.rs`: that one classifies Cohen's d effect sizes and is unrelated.) + +**Execution class:** the names `Pure`, `ReadVersion`, `Propose` and `ExternalMutate` come from the withdrawn pre-reset `glove-parity::method::EffectClass` (see the note above); keep them as vocabulary until the D-CMR rebuild chooses an anchor. Nothing below is available on `main`. As intended: `Pure` uses existing Quack/R2IL and dir_sim primitives. `Propose` builds a `ProposedMethod` and is legal only on an Action body. `ExternalMutate` is not a Quack opcode and must refuse unless independently authorized, with fresh source preconditions and external connector attestation. An absent field, alias, authority, schema seal, body, read scope, source version, evidence completeness or capability causes an explicit typed refusal. ## 7. Falsifiers and acceptance matrix diff --git a/.claude/plans/sag-capstone-alignment-v1.md b/.claude/plans/sag-capstone-alignment-v1.md index 5f6ca0120..c6fc5d01a 100644 --- a/.claude/plans/sag-capstone-alignment-v1.md +++ b/.claude/plans/sag-capstone-alignment-v1.md @@ -46,6 +46,64 @@ code anchor is re-decided when the class-method rebuild (D-CMR) lands: | **rewrite** — a pure, structural optimization | `awareness::Candidate { kind, methods, obligations }` ("never a rewrite") | the candidate, its open `Obligation`s, evidence tier and provenance, and a read-only verification query | not applied: it still needs a semantic-equivalence oracle (NULL / bag / set), a cost measurement and an operator decision | | **action** — an external effect | `EffectClass::Propose` on `MethodBody::Action` ("builds an inert proposal"); every call refuses with `NotPure` | the effect, its preconditions (source ETag/version, policy revision, target identity) and its simulated impact | not dispatched: it needs fresh OGAR authorization, then provider receipt and re-observation | +### 2.1 Anchors after the reset (2026-10-13) + +**DECISION.** The action shape anchors on the action gate that already exists: +a proposal is an `ActionInvocation` in state `Pending`, and the gate that may +advance it is `ActionInvocation::commit_via` (the `ClassRbac` grant registry, +no admin bypass). `commit_via` consults the registry only when +`ActionDef.required_role` is `Some`, so a proposed action must set +`required_role` or carry a separate authorization check. This is a requirement, not yet a property of the code: the +older `ActionInvocation::commit` (`action.rs:265`) makes the same transitions +with an admin bypass, is public, and `lance-graph-ogar/src/actions.rs` +directs consumers to it (OPEN item 7). +**SCOPE.** The action shape only. The rewrite shape anchors on the rebuilt +D-CMR fold binding (`classid × WideFieldMask → Compiled` program) and waits +for it. +A rewrite-shape `ProposedMethod` is then the output of concept-chain +normalization: an equivalent, cheaper form of a chain, proven against the +unrewritten form and a row oracle (rules in +`entries/2026-10-12-session-reset-inventory.md`, "Concept chains"). +**BASIS.** The removed `glove-parity::method::EffectClass` documented that only +OGAR's action gate runs `ExternalMutate`, so `Propose` sits in front of that +gate. Read in code: + +| piece | where | what it already gives a proposal | +|---|---|---| +| the gate | `lance-graph-contract/src/action.rs` `ActionInvocation::commit_via` (`:327`; `commit` at `:265` is the older variant with an admin bypass) | sticky terminal states, then def match → RBAC grant (`ClassRbac`, `Operation::Act`) → `StateGuard` → MUL `GateDecision`; `Pending → Committed / Failed / Cancelled`, and `Hold` keeps it `Pending` | +| the inert record | `ActionInvocation::pending(..)` (`:218`) | target as a full `NodeGuid`, `cycle`, `idempotency_key`, `trace_id`; `emitted_at_millis` stays `None` until commit | +| OGAR's IR form | `ogar-vocab` `ActionDef` / `ActionInvocation` / `ActionState` (same four states, String identities, plus `parent_invocation` and `failure_reason`) | the producer-side record | +| building a `Pending` invocation from a request | `ogar-from-schema/src/action_ws.rs` `submit_to_invocation` | HIRO `submitAction` → `Pending`; the doc comment says it then passes `commit_via` before `Committed` | +| running it | `ogar-action-handler` `CapabilityExecutor` impls; the doc comments say `commit_via` runs upstream of them, in rs-graph-llm's `graph-flow-action` (not read here) | execution plus `Receipt` and `sendActionResult` | + +Not related: `ogar-proposal` (schema `MappingProposal` drafts for the +ontology registry) and the Cohen's d `EffectClass` in `lance-graph-cognitive`. + +**What the gate does not carry yet** (OPEN, against the life cycle below): +1. *Source version / ETag precondition.* `StateGuard` is `field == value` on + the current instance; no version of the source the proposal was made + against. +2. *Policy revision.* RBAC is evaluated at commit against the current grants; + the proposal records no revision. +3. *Simulated impact.* The MUL `GateDecision` is an input to `commit_via`, + not stored on the invocation. +4. *Separate approval and authorization.* The life cycle keeps "approved" + and "authorized" as two facts; `commit_via` decides RBAC and impact in one + call. +5. *`UnknownOutcome`.* `ActionState::Failed` covers both an unauthorized actor + and a runtime failure (`action.rs:50`), and there is no state for a + timed-out external call, which the life cycle requires never to read as + "not applied". +6. *Re-observation.* Nothing records the target's state after the effect. +7. *A second gate.* `commit` (admin bypass) can advance the same `Pending` + invocation without the `ClassRbac` check. Either retire, privatize or + redirect it, or document both gates and their different authorization. + +None of the seven is built by this note; each lands, if at all, in the gate's +own types. +**REVISIT WHEN** the D-CMR rebuild lands (rewrite anchor), or when any of the +seven gaps is closed. + The life cycle is shared, and each arrow is a separate fact with its own receipt: