From 8c48cdd37b87c4e41032116f7a7d08fb1cdd19e5 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 06:47:49 +0000 Subject: [PATCH 1/9] docs: mark references to the method layer #1524 removed Three docs still presented glove-parity's `method.rs` / `awareness.rs` as shipped after D-CMR-RESET moved them to backup/session-011BMJ-2026-10-12: - INTEGRATION_PLANS.md: the capstone, SAG-5 and SAG-1 index lines (append-only, so a dated note under each bullet). - software-awareness-provenance-parity.md: SoftwareGraph/MethodTable in the READ BY header, the crosswalk and the source map. - iam-substrate-sag-dir-sim-v1.md: the awareness.rs row (:29) and the "main's shipped EffectClass" sentence (:108). The notes name glove-parity::method::EffectClass explicitly: main still has an unrelated EffectClass (Cohen's d) in lance-graph-cognitive's search/certificate.rs, which a search would return as if the action-shape anchor had survived. Docs only; supersession index regenerates unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/INTEGRATION_PLANS.md | 3 +++ .claude/knowledge/software-awareness-provenance-parity.md | 4 +++- .claude/plans/iam-substrate-sag-dir-sim-v1.md | 6 +++++- 3 files changed, 11 insertions(+), 2 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index ff37d79d8..57fc4af6f 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -3,6 +3,7 @@ **Status:** CURRENT-CONTRACT for naming and vocabulary; nothing built. - `ProposedMethod` is canonical (rewrite shape on `awareness::Candidate`, action shape on `EffectClass::Propose`); six aliases retired; scheduler selection renamed `SchedulerDecision`. + - ⊘ 2026-10-13: both anchors were removed by #1524 (D-CMR-RESET): `glove-parity::awareness::Candidate` and `glove-parity::method::EffectClass::Propose`. Code on `backup/session-011BMJ-2026-10-12`. The name and the two shapes stand; the anchors are re-decided with the D-CMR rebuild. (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.) - One four-state status (Witnessed / Refuted / Undetermined / Conflicted) maps the five PR vocabularies; unread is never missing. - Stale claims listed (second hop refused, defects A/B unverified); contradictions on Ruff's role, ONA pin and execution-class names resolved. @@ -11,6 +12,7 @@ **Status:** PROPOSAL D-SAG-5-0..10. Only D-SAG-5-0 documentation is in this PR, based on merged #1509. - Reuses shipped MethodTable/SoftwareGraph/Quack one-hop behavior, compiler tiers, source seals and H1 cost/refusal ledger. Two-hop, persistence and applying optimizations remain blocked or queued. + - ⊘ 2026-10-13: `MethodTable` and `SoftwareGraph` are no longer shipped; #1524 (D-CMR-RESET) moved them to `backup/session-011BMJ-2026-10-12`. Nothing in this plan can reuse them until the D-CMR rebuild. - Source-indexed .arxiv excerpts connect Wang/ONA internal events, Hyperon reflexive reasoning and affective modulators, BALD vs noise, Miner surprise, metagraph fold laws, evidence fusion/fission and egg rewrite certificates. - Claude Code prompt demands exact source/answer parity, context-token measurement, independent epistemic and attention ablations, and explicit refusal on unsupported semantics. Functional Emberglow, Steelwind, Woodwarm and Velvetpause labels authorize no CE64 bit change. - No runtime feature, second IR, self-certified result, automatic code mutation, new opcode or schema is created. @@ -20,6 +22,7 @@ **Status:** MEASURED for one concept's methods (D-SAG-1-0..3 and D-SAG-1-5 in the PR); D-SAG-1-4 and D-SAG-1-6 queued. - A `MethodTable` projects to typed rows (class, method, field, condition, fold, law, program, primitive, lowering, refusal, claim, capability, test). Each row has a tier (declared / derived / compiled / verified / hypothesis) and a provenance. + - ⊘ 2026-10-13: withdrawn by #1524 (D-CMR-RESET) with the whole method layer; D-SAG-1-0..6 are marked Withdrawn on `STATUS_BOARD.md`. Code and tests on `backup/session-011BMJ-2026-10-12`. - The edge table is a Quack table: dependency questions are Drafts lowered and run on mask-risc. Validation is the compiler's verdicts recorded as edges. - H1 (fuse a predicate into `MaskedSumI32`) comes from the rows. Measured gap: 1.6–1.8× against a single-pass scalar reference on two tiers. Missing: `Pred` fusion and a sum `FusedFold`. - First blocker: multi-hop questions need a relation carrier, not a mask fed between programs. 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/iam-substrate-sag-dir-sim-v1.md b/.claude/plans/iam-substrate-sag-dir-sim-v1.md index 0db00dee3..a3e120abe 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,6 +105,10 @@ class Grant { policy, witnesses, effective_during } class Change { preview, validate, approve, execute, verify, revert } ``` + + +> ⊘ 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:** 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. ## 7. Falsifiers and acceptance matrix From c402d4f1c6eec86ce97cbc5c32eeeaecfe47afd6 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 06:48:59 +0000 Subject: [PATCH 2/9] board: reset entry names the backup test cases and both anchors The reset inventory said the code was recoverable but not that the tests were: polyfill.rs (15), ordered.rs (3), distinct.rs (6), relation.rs (8) and awareness.rs (19) are on backup/session-011BMJ-2026-10-12 at 8ae5bce. Each calls the removed MethodBody API, so the entry records that a case is re-expressed against a Compiled program and its row-loop answer re-run before it counts as an oracle. The OPEN line named one ProposedMethod anchor; there were two (the rewrite shape on awareness::Candidate, the action shape on method::EffectClass::Propose). Both named with their crate path. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .../entries/2026-10-12-session-reset-inventory.md | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) 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..07968ac17 100644 --- a/.claude/board/entries/2026-10-12-session-reset-inventory.md +++ b/.claude/board/entries/2026-10-12-session-reset-inventory.md @@ -52,5 +52,16 @@ 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. +**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 undecided. From 4d56c419faa3f6df376b1608bae2c19663e5c7a0 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 06:53:29 +0000 Subject: [PATCH 3/9] capstone: anchor the action shape of ProposedMethod on the action gate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Decision for the action shape (capstone §2.1): a proposal is an ActionInvocation in state Pending, advanced only by ActionInvocation::commit_via (lance-graph-contract/src/action.rs:327: def match, RBAC grant, StateGuard, MUL GateDecision). OGAR's IR form (ogar-vocab ActionInvocation, same four states) and ogar-from-schema::action_ws::submit_to_invocation already build Pending invocations; ogar-action-handler's executors run after the gate. §2.1 also lists six things the gate does not carry against the capstone's life cycle: source version, policy revision, stored simulated impact, separate approval and authorization, an UnknownOutcome state (Failed covers both unauthorized and runtime failure), and re-observation. Nothing is built. The rewrite shape still waits on the D-CMR binding. The reset entry's OPEN line now points at §2.1. Not related: ogar-proposal (schema MappingProposal drafts). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/SUPERSESSION-INDEX.md | 7 +-- .../2026-10-12-session-reset-inventory.md | 4 +- .claude/plans/sag-capstone-alignment-v1.md | 45 +++++++++++++++++++ 3 files changed, 52 insertions(+), 4 deletions(-) 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 07968ac17..927b882b8 100644 --- a/.claude/board/entries/2026-10-12-session-reset-inventory.md +++ b/.claude/board/entries/2026-10-12-session-reset-inventory.md @@ -64,4 +64,6 @@ 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 undecided. +rebuilt binding. The action anchor is the action gate: a `Pending` +`ActionInvocation` advanced only by `commit_via` (capstone §2.1, which lists +what the gate does not carry yet). diff --git a/.claude/plans/sag-capstone-alignment-v1.md b/.claude/plans/sag-capstone-alignment-v1.md index 5f6ca0120..f025bceb9 100644 --- a/.claude/plans/sag-capstone-alignment-v1.md +++ b/.claude/plans/sag-capstone-alignment-v1.md @@ -46,6 +46,51 @@ 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`. +**SCOPE.** The action shape only. The rewrite shape anchors on the rebuilt +D-CMR fold binding (`classid × WideFieldMask → Compiled` program) and waits +for it. +**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. + +None of the six 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 +six gaps is closed. + The life cycle is shared, and each arrow is a separate fact with its own receipt: From a0dbdcf8985ce10931643a7251b95fd3caf17519 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 07:44:31 +0000 Subject: [PATCH 4/9] board: reset root cause and the concept-chain rule for D-CMR The reset entry recorded what was removed but gave the cause only as "a second algebra, slower than the row loop". The root cause, read in the removed code on backup/session-011BMJ-2026-10-12: each method was evaluated on its own (run_quack built population-sized scratch per call, tiled path, no Compiled, no Lowering::Range), hops stacked per-row key reads instead of intersecting ranges, and the optimization went into identity structures instead of the data path. The rebuild section gains the concept-chain rule: methods in a pure chain are unresolved relations; the whole chain is normalized with proven identities before lowering and only the irreducible remainder is compiled. Quack's tree holds Quack-bound chains, NAL stays R2IL-bound, no new IR. SUM uses the existing fold over the minimized extent; prefix lanes are a separate measured candidate. Coordinates need a proven ordering. Disabling an optimization keeps the answer; removing a semantic guard must fail. The capstone's rewrite-shape anchor points at the rule. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .../2026-10-12-session-reset-inventory.md | 44 +++++++++++++++++++ .claude/plans/sag-capstone-alignment-v1.md | 4 ++ 2 files changed, 48 insertions(+) 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 927b882b8..46f19edfa 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,6 +67,35 @@ 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. +**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. +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), diff --git a/.claude/plans/sag-capstone-alignment-v1.md b/.claude/plans/sag-capstone-alignment-v1.md index f025bceb9..5de62721d 100644 --- a/.claude/plans/sag-capstone-alignment-v1.md +++ b/.claude/plans/sag-capstone-alignment-v1.md @@ -54,6 +54,10 @@ advance it is `ActionInvocation::commit_via`. **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: From 9e6b01ec3c604e736086fd4a895fabb56a3da4c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 07:56:05 +0000 Subject: [PATCH 5/9] plan: D-CMR concept-chain normalization (D-CMR-0) Proposal for the D-CMR rebuild: preserve the equation, not the intermediate result. Methods in a pure chain are unresolved relations; the whole chain is normalized with proven identities and only the irreducible remainder is lowered once into a Compiled program. (a+b)-a means a+b never exists, not that it needs a wider accumulator. Inventory read in code at c157c0a: fold_ranges (every Quack lowering), survivor skip, sql_where, ternlog fusion, Lowering::Range (Count/Any only), Compiled, execute_extent. Quack never emits an extent; only NAL does, by hand via bound_aperture. No value-arithmetic IR exists, so the cancellation identity first appears at the aggregate level: Sum(A) - Sum(A and B) = Sum(A and not B). Identity matrix with legality conditions (exact, wrapping, checked, IEEE, three-valued, bag vs set, _sym). Path D-CMR-1..7: extent hoisting in Quack, lazy binding, fixpoint driver, complement, relational difference, equality-saturation probe only on evidence, benchmark against eager materialization and the row loop. Docs only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/INTEGRATION_PLANS.md | 8 + .claude/board/STATUS_BOARD.md | 15 ++ .../d-cmr-concept-chain-normalization-v1.md | 140 ++++++++++++++++++ 3 files changed, 163 insertions(+) create mode 100644 .claude/plans/d-cmr-concept-chain-normalization-v1.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 57fc4af6f..5207b768e 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,11 @@ +## 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..7. Only D-CMR-0 (plan, board rows) is in the PR; no code, no dependency, no new IR. + +- 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). + ## 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..c7c210d66 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,3 +1,18 @@ +## 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. No new IR, 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** | Extent hoisting: a top-level range conjunct becomes the `execute_extent` extent in Quack; the rest stays residual | Queued | == unhoisted == row oracle; a range on another coordinate basis must not hoist | +| **D-CMR-2** | Lazy binding: methods yield `Filter` fragments composed into one `Query` before lowering | Queued (after NAL lands in core) | k methods lower once; no scratch per link | +| **D-CMR-3** | Fixpoint driver over existing passes, step budget, size non-increase | Queued | a second rule fires only because the first did | +| **D-CMR-4** | Complement rule `Count(¬A) = N − Count(A)`, two-valued guard | Queued | removing the guard fails on a nullable column | +| **D-CMR-5** | Relational difference `Sum(A) − Sum(A∧B) = Sum(A∧¬B)` | Queued | == exact `i128` oracle; `_sym` and checked variants refuse | +| **D-CMR-6** | Equality-saturation probe (`egg`/`egglog` as references) | Queued (only if rules compete) | compared against D-CMR-3; no dependency without evidence | +| **D-CMR-7** | Benchmark: eager materialization vs normalized chain 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/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md new file mode 100644 index 000000000..dd74956a2 --- /dev/null +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -0,0 +1,140 @@ +# d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result + +**Status:** PROPOSAL (D-CMR-0..7). Only D-CMR-0 (this document and its board +rows) is in the PR that adds it. No code, no dependency, no new IR. +**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. Rule catalogue (the Tafelwerk), in existing representations + +A rule is an identity, not a stored result. Each entry has six fields: +pattern, semantic preconditions, rewrite, proof (independent oracle plus a +negative control), cost effect, scope. The lookup key is the pattern **and** +its preconditions: `Count(¬A)` under three-valued logic is a different entry +from `Count(¬A)` under Boolean logic. + +- **Home.** Quack-bound chains: passes over `Filter`/`Query` in the quack + crate, next to `fold_ranges`. Global NAL methods: rules applied while the + core NAL module emits its R2IL procedure. No new IR. A `Rule` type exists + only if the fixpoint driver (D-CMR-3) cannot be written over plain passes; + the insufficiency is recorded first. +- **Application.** Repeat until no rule fires or a step budget is reached. + Every rule must not increase expression size, so the loop terminates. +- **Heuristics** order the rules; they never replace a proof. + +## 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 | + +## 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. Minimal implementation path (no second algebra) + +| D-id | step | gate / falsifier | +|---|---|---| +| D-CMR-1 | **Extent hoisting.** A top-level range conjunct that `fold_ranges` produced becomes the `execute_extent` extent; the rest of the filter runs as the residual (Experiment C) | answers == unhoisted == row oracle; disabling hoisting keeps answers; a range on a different coordinate basis must not hoist (negative control) | +| D-CMR-2 | **Lazy binding.** A bound method yields a `Filter` fragment plus aggregate, composed into one `Query` before lowering; no per-link execution | chain of k methods lowers once; no scratch allocated per link | +| D-CMR-3 | **Fixpoint driver** over the existing passes, with a step budget and size non-increase | Experiment D: a second rule fires only because the first did | +| D-CMR-4 | **Complement rule**, guarded on two-valued leaves | removing the guard fails on a nullable column | +| D-CMR-5 | **Relational difference rule** `Sum(A) − Sum(A∧B) → Sum(A∧¬B)` (Experiment A at the aggregate level) | equal to the exact `i128` oracle; the `_sym` and checked variants refuse | +| D-CMR-6 | **Equality-saturation probe** (`egg`, `egglog`, as references only) | runs only if two rules compete and order changes the result; compared against D-CMR-3 with extraction cost taken from the real lowerings; no dependency without that evidence | +| D-CMR-7 | **Benchmark** (section 8) | answers asserted before timing | + +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 the extent, the predicate stays residual (D-CMR-1). +- **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-1) | +| chains composed before lowering | OPEN (D-CMR-2) | +| repeated rule application | OPEN (D-CMR-3) | +| complement, relational difference | OPEN (D-CMR-4, -5) | +| 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-6) | + +## 10. Ownership + +D-CMR-1..5 touch quack and the core NAL module. The other session is moving +R2IL and NAL into core; D-CMR-1 (quack only) can start independently, +D-CMR-2..5 after NAL lands in core. Owner to be assigned. From a931b461739fa3fb707bd370af5c804abb256108 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 08:04:15 +0000 Subject: [PATCH 6/9] plan: D-CMR revision, a set-theory IR for concept-chain normalization MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The normalization gets one new IR. Insufficiency proof (plan §3.1, read in code): everything set-like is a predicate (Quack Filter; fold_ranges gives at most one interval per column, never merges under Or) or a materialized bitset (EvidenceMask, mask-risc masks); WideFieldMask holds fields; no interval-set type exists. Four things have no home: a set's universe (proven ordering), an intersection result as a value (empty, point, one or several intervals), mappings between universes (the hop as preimage), and measures as functions of a set. The IR: universe over a basis, intervals, sorted disjoint runs, 2-D rectangles over composite coordinates, an opaque residual, set operations, preimage; measures Count, Sum, Exists. Normal form runs ∩ residual; sets are stored by their edges, so cost scales with edges, not rows. Lives in the contract; Quack and NAL lower into it. Two-valued, sets not bags, intersection within one universe. Lithography reading (layer booleans on edges before exposure, rasterization once) and three measurement levels: geometry (no row read), optics (fused filter + count, nothing written), etch (materialize only when the set itself is needed). Path recut to D-CMR-1..9; board rows updated; the reset entry notes that "no new universal IR" is superseded. Docs only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/INTEGRATION_PLANS.md | 1 + .claude/board/STATUS_BOARD.md | 18 +- .../2026-10-12-session-reset-inventory.md | 4 + .../d-cmr-concept-chain-normalization-v1.md | 167 ++++++++++++++---- 4 files changed, 149 insertions(+), 41 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 5207b768e..213c68a04 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -5,6 +5,7 @@ - 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. ## 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` diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index c7c210d66..b89a798b7 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -1,17 +1,19 @@ ## 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. No new IR, no method-body algebra, no dependency. +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** | Extent hoisting: a top-level range conjunct becomes the `execute_extent` extent in Quack; the rest stays residual | Queued | == unhoisted == row oracle; a range on another coordinate basis must not hoist | -| **D-CMR-2** | Lazy binding: methods yield `Filter` fragments composed into one `Query` before lowering | Queued (after NAL lands in core) | k methods lower once; no scratch per link | -| **D-CMR-3** | Fixpoint driver over existing passes, step budget, size non-increase | Queued | a second rule fires only because the first did | -| **D-CMR-4** | Complement rule `Count(¬A) = N − Count(A)`, two-valued guard | Queued | removing the guard fails on a nullable column | -| **D-CMR-5** | Relational difference `Sum(A) − Sum(A∧B) = Sum(A∧¬B)` | Queued | == exact `i128` oracle; `_sym` and checked variants refuse | -| **D-CMR-6** | Equality-saturation probe (`egg`/`egglog` as references) | Queued (only if rules compete) | compared against D-CMR-3; no dependency without evidence | -| **D-CMR-7** | Benchmark: eager materialization vs normalized chain vs row loop | Queued | answers asserted before timing; tier from the build's report | +| **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) 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 46f19edfa..09546982e 100644 --- a/.claude/board/entries/2026-10-12-session-reset-inventory.md +++ b/.claude/board/entries/2026-10-12-session-reset-inventory.md @@ -79,6 +79,10 @@ lowering; only the irreducible remainder becomes a `Compiled` program. 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. diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index dd74956a2..8ca8d0889 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -1,7 +1,10 @@ # d-cmr-concept-chain-normalization-v1 — preserve the equation, not the intermediate result -**Status:** PROPOSAL (D-CMR-0..7). Only D-CMR-0 (this document and its board -rows) is in the PR that adds it. No code, no dependency, no new IR. +**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. **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. @@ -37,22 +40,114 @@ steps survive once the chain is simplified. 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. Rule catalogue (the Tafelwerk), in existing representations +## 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. + +### 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. Cost scales with + the number of edges, never with the number of rows. +- **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:** `lance-graph-contract`, next to `ClassView`. The algebra itself + needs no dependency; its lowering needs mask-risc, which the contract gains + in the agreed restructure. Quack's `Filter` and the core NAL module lower + **into** this IR, so 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 | `mask_ternlog_popcount`, `Lowering::Ternlog` → `Count`, `execute_extent` | +| 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. -A rule is an identity, not a stored result. Each entry has six fields: -pattern, semantic preconditions, rewrite, proof (independent oracle plus a -negative control), cost effect, scope. The lookup key is the pattern **and** -its preconditions: `Count(¬A)` under three-valued logic is a different entry -from `Count(¬A)` under Boolean logic. +### 3.5 Rule catalogue (the Tafelwerk) over the set IR -- **Home.** Quack-bound chains: passes over `Filter`/`Query` in the quack - crate, next to `fold_ranges`. Global NAL methods: rules applied while the - core NAL module emits its R2IL procedure. No new IR. A `Rule` type exists - only if the fixpoint driver (D-CMR-3) cannot be written over plain passes; - the insufficiency is recorded first. -- **Application.** Repeat until no rule fires or a step budget is reached. - Every rule must not increase expression size, so the loop terminates. -- **Heuristics** order the rules; they never replace a proof. +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. ## 4. Identity matrix with semantic conditions @@ -76,17 +171,19 @@ from `Count(¬A)` under Boolean logic. delays rounding or quantization to a named boundary. Allowed only where declared, never inferred from "the result looks more accurate". -## 6. Minimal implementation path (no second algebra) +## 6. Implementation path | D-id | step | gate / falsifier | |---|---|---| -| D-CMR-1 | **Extent hoisting.** A top-level range conjunct that `fold_ranges` produced becomes the `execute_extent` extent; the rest of the filter runs as the residual (Experiment C) | answers == unhoisted == row oracle; disabling hoisting keeps answers; a range on a different coordinate basis must not hoist (negative control) | -| D-CMR-2 | **Lazy binding.** A bound method yields a `Filter` fragment plus aggregate, composed into one `Query` before lowering; no per-link execution | chain of k methods lowers once; no scratch allocated per link | -| D-CMR-3 | **Fixpoint driver** over the existing passes, with a step budget and size non-increase | Experiment D: a second rule fires only because the first did | -| D-CMR-4 | **Complement rule**, guarded on two-valued leaves | removing the guard fails on a nullable column | -| D-CMR-5 | **Relational difference rule** `Sum(A) − Sum(A∧B) → Sum(A∧¬B)` (Experiment A at the aggregate level) | equal to the exact `i128` oracle; the `_sym` and checked variants refuse | -| D-CMR-6 | **Equality-saturation probe** (`egg`, `egglog`, as references only) | runs only if two rules compete and order changes the result; compared against D-CMR-3 with extraction cost taken from the real lowerings; no dependency without that evidence | -| D-CMR-7 | **Benchmark** (section 8) | answers asserted before timing | +| 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 | == row oracle; a `Count` with no residual reads zero rows (instrumented); disabling level 1 or 2 keeps answers | +| D-CMR-3 | **Quack frontend:** `Filter` → set IR (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 frontend:** aperture → `Runs` (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 | Prefix lanes stay a separate, measured candidate (ordering, overflow, NULL, update and maintenance laws), never a precondition for `SUM`. @@ -100,7 +197,8 @@ update and maintenance laws), never a precondition for `SUM`. 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 the extent, the predicate stays residual (D-CMR-1). + 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 @@ -125,16 +223,19 @@ median of 101, tier named from the build's own report, answers asserted first. | `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-1) | -| chains composed before lowering | OPEN (D-CMR-2) | -| repeated rule application | OPEN (D-CMR-3) | -| complement, relational difference | OPEN (D-CMR-4, -5) | +| 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 (`mask_ternlog_popcount`, `Lowering::Ternlog`) | +| 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-6) | +| equality saturation | research (D-CMR-8) | ## 10. Ownership -D-CMR-1..5 touch quack and the core NAL module. The other session is moving -R2IL and NAL into core; D-CMR-1 (quack only) can start independently, -D-CMR-2..5 after NAL lands in core. Owner to be assigned. +- D-CMR-1 (pure algebra in the contract) can start now. +- D-CMR-2 needs the contract → mask-risc dependency (agreed, not yet landed). +- D-CMR-3..6 touch quack; D-CMR-7 waits until NAL lands in core. +- Owner to be assigned. From 30642032a97327faf7fb361a122e10ad411c8316 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 12:32:00 +0000 Subject: [PATCH 7/9] Correct three D-CMR plan claims flagged in review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Plan §3.2: lowering is blocked on the contract -> mask-risc change, which has not landed; the contract Cargo.toml still declares it dependency-free. If the change does not land, lowering goes in an adapter crate. - Plan §3.4 / §9 / D-CMR-2: level 2 (fused filter + count, nothing written) is shipped for resident planes only. fused_ternlog declines Pred, so a residual comparison runs tiled and writes scratch; predicate fusion joins D-CMR-2's scope. - Capstone §2.1: commit_via is a requirement, not yet a property of the code. commit (admin bypass) advances the same Pending invocation and is what lance-graph-ogar documents; added as OPEN item 7. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .../plans/d-cmr-concept-chain-normalization-v1.md | 15 +++++++++------ .claude/plans/sag-capstone-alignment-v1.md | 13 ++++++++++--- 2 files changed, 19 insertions(+), 9 deletions(-) diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index 8ca8d0889..e5b4e9bdb 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -94,9 +94,12 @@ M ::= Count(S) | Sum_x(S) | Exists(S) 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:** `lance-graph-contract`, next to `ClassView`. The algebra itself - needs no dependency; its lowering needs mask-risc, which the contract gains - in the agreed restructure. Quack's `Filter` and the core NAL module lower +- **Home:** the algebra lives in `lance-graph-contract`, next to `ClassView`, + and needs no dependency. Its lowering needs mask-risc. Today the contract's + `Cargo.toml` declares it dependency-free (even of optional path deps); the + agreed contract → mask-risc change has not landed. Until it does, D-CMR-2 + is blocked, and if it does not land, the lowering lives in an adapter crate + that depends on both, never in the contract. Quack's `Filter` and the core NAL module lower **into** this IR, so neither frontend implements intervals of its own. ### 3.3 The lithography reading @@ -134,7 +137,7 @@ 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 | `mask_ternlog_popcount`, `Lowering::Ternlog` → `Count`, `execute_extent` | +| 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 @@ -176,7 +179,7 @@ the expression. Heuristics order rules; they never replace a proof. | 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 | == row oracle; a `Count` with no residual reads zero rows (instrumented); disabling level 1 or 2 keeps answers | +| 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 frontend:** `Filter` → set IR (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 | @@ -224,7 +227,7 @@ median of 101, tier named from the build's own report, answers asserted first. | ≤ 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 (`mask_ternlog_popcount`, `Lowering::Ternlog`) | +| 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) | diff --git a/.claude/plans/sag-capstone-alignment-v1.md b/.claude/plans/sag-capstone-alignment-v1.md index 5de62721d..b56e788a1 100644 --- a/.claude/plans/sag-capstone-alignment-v1.md +++ b/.claude/plans/sag-capstone-alignment-v1.md @@ -50,7 +50,11 @@ code anchor is re-decided when the class-method rebuild (D-CMR) lands: **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`. +advance it is `ActionInvocation::commit_via` (the `ClassRbac` grant registry, +no admin bypass). 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. @@ -89,11 +93,14 @@ ontology registry) and the Cohen's d `EffectClass` in `lance-graph-cognitive`. 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 six is built by this note; each lands, if at all, in the gate's +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 -six gaps is closed. +seven gaps is closed. The life cycle is shared, and each arrow is a separate fact with its own receipt: From e69f4412b1781f0266169ecea66ebde0b0abece3 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 12:44:04 +0000 Subject: [PATCH 8/9] Apply CodeRabbit review on the D-CMR docs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - INTEGRATION_PLANS: restore the three 2026-10-12 entries unchanged; their reset corrections move into the new 2026-10-13 entry. Status line now names D-CMR-0..9 and the set-theory IR. - Reset inventory: two methods advance a Pending invocation (commit_via, commit with admin bypass); which a proposal must pass stays OPEN. - Capstone §2.1: commit_via consults ClassRbac only when required_role is Some, so a proposed action must set it or carry its own check. - D-CMR plan: the edges-not-rows cost claim holds for interval-only operations; residuals and rectangle lowering scale with what they visit. - iam plan: the execution-class names are withdrawn pre-reset vocabulary, not shipped behaviour. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/INTEGRATION_PLANS.md | 9 +++++---- .../board/entries/2026-10-12-session-reset-inventory.md | 4 +++- .claude/plans/d-cmr-concept-chain-normalization-v1.md | 6 ++++-- .claude/plans/iam-substrate-sag-dir-sim-v1.md | 2 +- .claude/plans/sag-capstone-alignment-v1.md | 4 +++- 5 files changed, 16 insertions(+), 9 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 213c68a04..d3ca5ed05 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,18 +1,21 @@ ## 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..7. Only D-CMR-0 (plan, board rows) is in the PR; no code, no dependency, no new IR. +**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. +- 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. - `ProposedMethod` is canonical (rewrite shape on `awareness::Candidate`, action shape on `EffectClass::Propose`); six aliases retired; scheduler selection renamed `SchedulerDecision`. - - ⊘ 2026-10-13: both anchors were removed by #1524 (D-CMR-RESET): `glove-parity::awareness::Candidate` and `glove-parity::method::EffectClass::Propose`. Code on `backup/session-011BMJ-2026-10-12`. The name and the two shapes stand; the anchors are re-decided with the D-CMR rebuild. (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.) - One four-state status (Witnessed / Refuted / Undetermined / Conflicted) maps the five PR vocabularies; unread is never missing. - Stale claims listed (second hop refused, defects A/B unverified); contradictions on Ruff's role, ONA pin and execution-class names resolved. @@ -21,7 +24,6 @@ **Status:** PROPOSAL D-SAG-5-0..10. Only D-SAG-5-0 documentation is in this PR, based on merged #1509. - Reuses shipped MethodTable/SoftwareGraph/Quack one-hop behavior, compiler tiers, source seals and H1 cost/refusal ledger. Two-hop, persistence and applying optimizations remain blocked or queued. - - ⊘ 2026-10-13: `MethodTable` and `SoftwareGraph` are no longer shipped; #1524 (D-CMR-RESET) moved them to `backup/session-011BMJ-2026-10-12`. Nothing in this plan can reuse them until the D-CMR rebuild. - Source-indexed .arxiv excerpts connect Wang/ONA internal events, Hyperon reflexive reasoning and affective modulators, BALD vs noise, Miner surprise, metagraph fold laws, evidence fusion/fission and egg rewrite certificates. - Claude Code prompt demands exact source/answer parity, context-token measurement, independent epistemic and attention ablations, and explicit refusal on unsupported semantics. Functional Emberglow, Steelwind, Woodwarm and Velvetpause labels authorize no CE64 bit change. - No runtime feature, second IR, self-certified result, automatic code mutation, new opcode or schema is created. @@ -31,7 +33,6 @@ **Status:** MEASURED for one concept's methods (D-SAG-1-0..3 and D-SAG-1-5 in the PR); D-SAG-1-4 and D-SAG-1-6 queued. - A `MethodTable` projects to typed rows (class, method, field, condition, fold, law, program, primitive, lowering, refusal, claim, capability, test). Each row has a tier (declared / derived / compiled / verified / hypothesis) and a provenance. - - ⊘ 2026-10-13: withdrawn by #1524 (D-CMR-RESET) with the whole method layer; D-SAG-1-0..6 are marked Withdrawn on `STATUS_BOARD.md`. Code and tests on `backup/session-011BMJ-2026-10-12`. - The edge table is a Quack table: dependency questions are Drafts lowered and run on mask-risc. Validation is the compiler's verdicts recorded as edges. - H1 (fuse a predicate into `MaskedSumI32`) comes from the rows. Measured gap: 1.6–1.8× against a single-pass scalar reference on two tiers. Missing: `Pred` fusion and a sum `FusedFold`. - First blocker: multi-hop questions need a relation carrier, not a mask fed between programs. 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 09546982e..c478b43af 100644 --- a/.claude/board/entries/2026-10-12-session-reset-inventory.md +++ b/.claude/board/entries/2026-10-12-session-reset-inventory.md @@ -113,5 +113,7 @@ 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` advanced only by `commit_via` (capstone §2.1, which lists +`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/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index e5b4e9bdb..f4ff71915 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -83,8 +83,10 @@ 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. Cost scales with - the number of edges, never with the number of rows. +- **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 diff --git a/.claude/plans/iam-substrate-sag-dir-sim-v1.md b/.claude/plans/iam-substrate-sag-dir-sim-v1.md index a3e120abe..311f7beb7 100644 --- a/.claude/plans/iam-substrate-sag-dir-sim-v1.md +++ b/.claude/plans/iam-substrate-sag-dir-sim-v1.md @@ -109,7 +109,7 @@ class Change { preview, validate, approve, execute, verify, revert } > ⊘ 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:** 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. +**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 b56e788a1..c6fc5d01a 100644 --- a/.claude/plans/sag-capstone-alignment-v1.md +++ b/.claude/plans/sag-capstone-alignment-v1.md @@ -51,7 +51,9 @@ code anchor is re-decided when the class-method rebuild (D-CMR) lands: **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). This is a requirement, not yet a property of the code: the +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). From 33dc9f475e3e15b8d0b2559f3f35472d81249aba Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 12:49:38 +0000 Subject: [PATCH 9/9] D-CMR plan: align with the eight-point concept-chain 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, and what is shared is the rule catalogue (identities, preconditions, costs). Records that the IR describes and never executes, enforced by a test; puts lowering in core rather than the contract; names constraint propagation, rewriting and cost selection as the mechanism with equality saturation and Ruler as research references; states today's exact-integer numeric contract and the compile-time vs per-call binding split. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013z2e1YXkm6o6HNrDn5BPWA --- .claude/board/INTEGRATION_PLANS.md | 1 + .../d-cmr-concept-chain-normalization-v1.md | 53 +++++++++++++++---- 2 files changed, 44 insertions(+), 10 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index d3ca5ed05..eb4050f40 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -6,6 +6,7 @@ - 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. diff --git a/.claude/plans/d-cmr-concept-chain-normalization-v1.md b/.claude/plans/d-cmr-concept-chain-normalization-v1.md index f4ff71915..7668eb0f3 100644 --- a/.claude/plans/d-cmr-concept-chain-normalization-v1.md +++ b/.claude/plans/d-cmr-concept-chain-normalization-v1.md @@ -5,6 +5,14 @@ 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. @@ -64,7 +72,10 @@ Four things therefore have no home: 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. +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 @@ -97,12 +108,14 @@ M ::= Count(S) | Sum_x(S) | Exists(S) 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. Its lowering needs mask-risc. Today the contract's - `Cargo.toml` declares it dependency-free (even of optional path deps); the - agreed contract → mask-risc change has not landed. Until it does, D-CMR-2 - is blocked, and if it does not land, the lowering lives in an adapter crate - that depends on both, never in the contract. Quack's `Filter` and the core NAL module lower - **into** this IR, so neither frontend implements intervals of its own. + 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 @@ -154,6 +167,16 @@ 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 | @@ -168,6 +191,12 @@ the expression. Heuristics order rules; they never replace a proof. | `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 @@ -182,14 +211,18 @@ the expression. Heuristics order rules; they never replace a proof. |---|---|---| | 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 frontend:** `Filter` → set IR (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-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 frontend:** aperture → `Runs` (after NAL lands in core) | NAL W2 tests unchanged | +| 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`. @@ -241,6 +274,6 @@ median of 101, tier named from the build's own report, answers asserted first. ## 10. Ownership - D-CMR-1 (pure algebra in the contract) can start now. -- D-CMR-2 needs the contract → mask-risc dependency (agreed, not yet landed). +- 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.