From a3dc4e42142e765e88c6e107236c79be239cdab1 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 18:48:24 +0200 Subject: [PATCH 1/8] docs(.arxiv): extract BYODS primary paper and DR-fold falsifiers --- ...yods_ascent_custom_relations_dr_excerpt.md | 50 +++++++++++++++++++ 1 file changed, 50 insertions(+) create mode 100644 .arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md diff --git a/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md new file mode 100644 index 000000000..5feb7c51e --- /dev/null +++ b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md @@ -0,0 +1,50 @@ +# Sahebolamri et al. (OOPSLA 2023): BYODS / Ascent custom relations vs DR-native folds + +**Type:** primary-paper excerpt and transfer audit, **not an arXiv preprint**. Filed under `.arxiv/` as the project's research shelf. +**Paper:** Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher K. Micinski, *Bring Your Own Data Structures to Datalog*, PACMPL 7 (OOPSLA2), Article 264, October 2023, 26 pp. [DOI: 10.1145/3622840](https://doi.org/10.1145/3622840), [author-hosted paper](https://kmicinski.com/assets/byods.pdf), [SPLASH publication](https://2023.splashcon.org/details/splash-2023-oopsla/74/Bring-Your-Own-Data-Structures-to-Datalog). +**Implementation:** [Ascent BYODS.md](https://github.com/s-arash/ascent/blob/master/BYODS.MD), [AdaWorldAPI/ascent fork](https://github.com/AdaWorldAPI/ascent), [RelIndexRead source](https://github.com/s-arash/ascent/blob/master/ascent/src/rel_index_read.rs). +**Read:** 2026-10-22, paper pp. 1–7 and §§5.1–5.5 (primary source); provider trait/docs read. This **fills the OOPSLA paper-not-read gap** in [the existing evaluation](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md); it does not supersede that evaluation's operator decision. +**Status:** RESEARCH / EXCERPT only. No code or admission. + +## Primary-source observations (paraphrased, not executable claims) + +1. **Problem: representation-imposed complexity** (paper §§1–2, pp. 2–4). Ordinary Datalog compilers generate tuple joins over generic maps/trees. Some logical relations have exponentially or quadratically larger explicit extensions than their specialized physical representations. A `K`-element equivalence class, for example, has `K²` ordered pairs, but union-find represents the classes compactly. BYODS does not say that tuples are always slow; it isolates *a mismatch between logical relation and physical representation*. + +2. **Formal custom-relation contract** (§3, pp. 5–7): a relation is associated with `(D, inj, γ)`, where `D` is a join-semilattice/domain, `inj: T → D` incorporates a tuple, and `γ: D → P(T)` defines which logical tuples the structure denotes. The ordinary powerset model is a special case. The immediate-consequence operator consults `γ` for rule bodies and `inj` for rule heads. Theorem 3.1 gives **monotone concretization** as a sufficient condition for a monotone immediate-consequence operator. This is a semantic condition, **not** a claim that `γ` itself should materialize its full powerset during execution. + +3. **Incremental semantics is a separate obligation** (§3–4). The paper develops semantics for semi-naive/delta evaluation over these abstract relations. A compact relation representation is useful only if deriving new facts, detecting changed closure and iterating to a fixed point preserve the appropriate semantics. Mere result parity in a one-shot scan does not prove correct delta maintenance. + +4. **Equivalence relations** (§5.1–5.2). Union-find-backed `eqrel` avoids constructing every equivalence pair, while explicit transitive/symmetric/reflexive Datalog rules can experience quadratic blow-up. The paper includes Steensgaard analysis. This supports a custom *equality-class carrier*, but **does not automatically provide e-node congruence rebuilding, proof objects, or e-graph extraction**. + +5. **Transitive relations and workload specificity** (§5.3–5.4). `trrel` improves the rule schedule for closure; `trrel_uf` additionally exploits strongly connected components. The latter excels on graphs with useful community/SCC structure, but the paper acknowledges cases with no asymptotic improvement and overhead. A fixed DR256 focus cannot represent arbitrary global closure without an explicit larger-domain strategy. + +6. **Index sharing** (§5.5). Multiple logical index orders need not imply independent physical copies. Index sharing is a relevant conceptual precedent for the project's *global-to-local ordinal mapping and borrowed projections*. That is a transfer hypothesis, not evidence that existing BYODS implements the specific DR pointer-table view. + +7. **Actual Ascent backend interface**, verified in `BYODS.MD` and `RelIndexRead`: `#[ds(provider)]` causes macro-generated code to use provider macros `rel_ind!`/`rel_ind_common!` and `ToRelIndex`, `RelIndexRead::index_get`, `RelIndexReadAll::iter_all`, `RelIndexWrite`, `RelIndexMerge`; concurrent variants exist. Both `index_get` and `iter_all` expose **iterators of values**. These traits replace storage/indexing, not necessarily Ascent's tuple-at-a-time rule-body loops or head emission. This is the limiting boundary for zero-copy native mask folding. + +8. **Ascent is not egglog.** `eqrel` is an optimized equivalence relation, not full e-graph congruence closure; `egglog` includes functional dependencies, union/congruence rebuilding, saturation and extraction. Both may model a logical relation, but only egglog already supplies the built-in equality-saturation machinery. See [egglog research excerpt](2304.04332_egglog_equality_saturation_datalog_excerpt.md) and [eggcc effect-safe extraction map](2026-10_eggcc_effect_safe_extraction_statewalk_r2il_map.md). + +## Why this does **not** overturn the project's 2026-10-21 decision + +Existing [evaluation map](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP** for Ascent/Datafrog/egglog as hot runtime executors: tuple-oriented iteration, materialized heads, second evaluator, and P0 fold-only/no-owned-tuples doctrine. BYODS changes *relation backing*, but Ascent's current code-generation protocol still asks for value iterators. It cannot be credited with a vectorized DR-native `And`/`Or`/`PopCount` terminal without proof that the emitted loop has disappeared. + +**Better question:** can Ascent's *rule analysis, SCC/strata, indices, deltas and relation semantics* be harvested **offline**, then compiled into the already-owned `contract → relalg/Quack → R2IL/mask-risc` or direct bound DR SIMD execution? Alternatively, can a BYODS adapter expose a native mask terminal *without* any tuple-value iteration? Both are research questions; the latter may be impossible without changing Ascent's compiler contract. + +Do not import Ascent's evaluator, provide an upstream crate dependency to production, or relabel the tuple-valued iterator as a zero-copy fold. + +## Transfer hypotheses and must-fail tests + +| Question | Paper basis | Test / failure | +| --- | --- | --- | +| Can a DR plane be a well-behaved abstract relation? | `(D,inj,γ)`, Thm. 3.1 | Define finite-focus `γ` mathematically; monotonicity, same-coordinate identity, snapshot seal, and delta/cycle tests. If `γ` changes across a stale snapshot, refuse. | +| Does BYODS allow **native** mask evaluation? | §4 + value-iterator protocol | Inspect expanded `ascent!` / `#[ds]` code; count per-result `next()`/head writes, owned values, index memory. If every match is enumerated, classify BYODS as *interface-only*, not executor. | +| Can logical indexing be translated into borrowed positions? | §5.5 | Compare one sealed, independently attested global-to-local `$i` index with duplicate physical maps. No cross-table value-driven positional gather, including preparation. | +| Can recursion use masks? | semi-naive + §5.3/5.4 | Verify frontier/total/new independently via direct bitset closure over ≤256 sealed coordinates; a 257th unseen index or cyclic/stale case refuses. No claim of EXO-73 production driver. | +| Does `eqrel` replace egglog e-graphs? | §5.1 vs egglog | Union two term classes and require newly implied congruence between parent terms; without rebuilding and proof reconstruction, mark explicitly **NOT an e-graph**. | +| Is reuse actually cheaper? | index-sharing | Measure compile/setup/attest/projection/read/fold/verification separately, plus 256 rules × 4096 reuses and a deliberately nonsharing suite. Never infer run-time win from reduced tuple counts. | + +**Constraints:** P0 fold-only, no tuple materialization even for test outputs; no millisecond result reported as a success; use AdaWorldAPI forks; exact Set versus Bag/Distinct and K3 validity; `ADMISSION=B` for counted same-table seeks only; no foreign-value-driven gathers; proofs, source witnesses and commit receipts remain separate. + +**Existing plans, not duplicated:** [D-MPS-9](../.claude/plans/mork-pathmap-schnellverschluss-v1.md), [D-MTP](../.claude/plans/metta-polyfill-v1.md), [D-RU](../.claude/plans/d-relalg-unified-v1.md), [Ascent/datafrog/egglog assessment](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). Proposed stages live in [Ascent BYODS DR plan](../.claude/plans/ascent-byods-dr-fold-polyfill-v1.md). + +**Bottom line:** BYODS confirms the *formal possibility* of replacing relational storage without changing the logic. It does **not** yet solve DR-native rule execution. The immediate opportunity is to extract the compiler's rule schedule and relation abstraction, avoiding its tuple engine. From ef70d908c0d5980ec35f7a2e64c1b466bf2c3746 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 18:52:02 +0200 Subject: [PATCH 2/8] docs(plan): scope Ascent BYODS cold compiler to DR-native fold falsifiers --- .../plans/ascent-byods-dr-fold-polyfill-v1.md | 88 +++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 .claude/plans/ascent-byods-dr-fold-polyfill-v1.md diff --git a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md new file mode 100644 index 000000000..6749d4691 --- /dev/null +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -0,0 +1,88 @@ +# Ascent/BYODS → DR-native fold polyfill: staged falsification and cold-compiler plan + +**Status:** PROPOSAL / documentation only, 2026-10-22. No implementation, dependency, P0 policy, or production admission change authorized by this PR. +**Scope:** harvest Ascent's *logic compiler* capabilities and BYODS formalism to produce existing RelAlg/R2IL/DR procedures; do not create an Ascent-backed runtime, another database, or a competing MeTTa AST. +**Sources:** [BYODS primary-source excerpt](../../.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md), [author PDF](https://kmicinski.com/assets/byods.pdf), [AdaWorldAPI/ascent](https://github.com/AdaWorldAPI/ascent), [2026-10-21 prior evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). +**Ownership:** [EXO-87](https://linear.app/exo-red/issue/EXO-87) D-SRAM; [EXO-84](https://linear.app/exo-red/issue/EXO-84) D-MTP; [EXO-85](https://linear.app/exo-red/issue/EXO-85) D-ASM; [EXO-79](https://linear.app/exo-red/issue/EXO-79) D-MPS-9; [EXO-86](https://linear.app/exo-red/issue/EXO-86) D-RA/D-CMR; [EXO-102](https://linear.app/exo-red/issue/EXO-102) D-RU; [EXO-46](https://linear.app/exo-red/issue/EXO-46) BIND admission; [EXO-73](https://linear.app/exo-red/issue/EXO-73) recursion driver; [EXO-50](https://linear.app/exo-red/issue/EXO-50) coordination. + +## 0. Hypothesis, counter-hypothesis, and existing ruling + +**Question:** can Ascent's compile-time rule dependency, SCC/stratification, bound/free matching and abstract-relation semantics be compiled into **already available**, certified RelAlg polyfill templates that produce R2IL or direct prebound DR SIMD? Then MeTTa and MORK are front-end aliases, not owners of a second execution model. + +**Counter-hypothesis:** Ascent BYODS only substitutes its *relation provider*; its generated join loops and head writes still iterate over individual tuple bindings. A DR-backed `RelIndexRead` that yields bit positions one at a time is not a DR-native mask fold. + +**Binding ruling:** [2026-10-21 egglog/datafrog/Ascent evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) already ruled **SKIP** for Ascent as a hot runtime and withdrew tuple-native oracle roles. This research does not quietly reverse it. The difference is **cold compiler reuse**, not runtime delegation. + +```text +COLD [candidate only]: + static Ascent rule analysis / BYODS (D,inj,γ) semantic contract + -> find genuinely missing schedule or relation law beyond existing crepe_plan! + -> canonical, typed contract/relalg template + -> independent proof/guards, bounded compiler work + -> compiled R2IL FoldDialect recipe or direct prebound DR SIMD recipe +HOT [unchanged]: + MeTTa/MORK/Datalog aliases -> Quack binding -> admitted compiled recipe + -> R2IL/mask-risc/ndarray OR direct prebound DR bit folds + -> Count/Any/Keep/etc.; no tuple expansion +OFFLINE PROOF [separate owners]: + egglog congruence, proof; Ruler/Enumo law candidates; eggcc effect extraction +``` + +Do not manufacture an extra compiler representation when `crepe_plan!`, contract set_algebra, relalg and Quack already cover the operation. No hidden MORK/PathMap execution dependency. + +## 1. Stages + +| Stage | Narrow task | Falsifier / result gate | Status | +|---|---|---|---| +| **A0 source/ownership audit** | Extract BYODS formal model and compare Ascent source to D-SRAM, D-MTP, existing crepe-plan-probe and D-RU. Record conflict with old hot-path SKIP. | If no unique cold compiler feature is missing, PARK. | This docs PR | +| **A1 generated-code microscope** | Inspect fork `#[ds]` expansion, `rel_ind!`/`rel_ind_common!`, `RelIndexRead::index_get`, `RelIndexWrite` and one `R(x,y), S(y,z)` rule. Count per-binding iteration, owned tuples, head writes and indices. Source/codegen inspection before building anything. | If generated loops enumerate each match, **BYODS-only is NOT native fold execution**. Do not retrofit a new Ascent runtime in response. | Queued, lab-only authorization required | +| **A2 mathematical relation contract** | Specify finite-focus `D, inj, γ` (abstract lattice/domain, inject tuple logically, concretize without actually enumerating it) over sealed DR coordinates. Validate monotone `γ`, bottom, join laws and delta/total/new fixed-point semantics. | 257th out-of-focus slot, stale seal/ABA, non-monotone delta, changed coordinate identity or missing completeness must refuse. | Queued, docs/math first | +| **A3 *cold* static rule planning** | Compare SCC, negation strata, lattice preconditions, binding propagation, join-order metadata with existing `crepe_plan!`, `set_rules` and Quack on identical fixed rules. No second AST or executor. | If metadata gives no new lawful plan shape or only a second spelling, PARK. Test negative cycle, repeated variable, disconnected rule and nested expression refusal. | Queued, requires EXO-87 coordination | +| **A4 DR-native lowering** | On presealed co-addressed source/target frame, translate one positive 2-hop rule into native `AND` + fold; compare existing direct bitmask/RelAlg execution. Preserve `ADMISSION=B`. | Any per-result `next()`/write, foreign value-driven gather, owned tuple, stale source, wrong bag fan-out, NULL/FALSE conflation, unadmitted bind or silent result truncation kills the path. | Gated on A1/A2/A3 and EXO-46 | +| **A5 equality and recursion boundary** | Counterexample: `a ≡ b` should imply `f(a) ≡ f(b)` under congruence; an `eqrel` provider alone cannot supply rebuilding/proofs. Separately check a ≤256-slot cyclic/diamond closure by *independent mask algorithm* against frontier folds. | No claim Ascent = egglog e-graph; no claim recursion is production (EXO-73). Refuse cross-version and out-of-scope closures. | Optional follow-up | +| **A6 reuse economics** | Compare direct existing relalg/DR compile+execute to offline Ascent-derived schedule plus same hot recipe. Test shared-core 256 templates ×4096 focus frames, nonsharing control, cold cache hit/miss/staleness and negative syntax. | Net win only with *same workload and semantics*, accounting separately for cold compile, proof/verify, bind/attest, hot fold, outputs and memory. Avoid counting reduced tuple volume as a fold speedup. | Gated on real A3/A4 benefit | + +## 2. Cold versus hot accounting: operator clarification requested + +**New operator observation, 2026-10-22:** a previously rejected **400–600 ms** overhead must be evaluated as possible *one-time cold compilation*, not automatically against the nanosecond *hot* target; the previous MeTTa/MORK workloads can run for many seconds. These measurements are **not paired on identical inputs** and must not be treated as a measured acceleration. + +Mathematical break-even, for the **same program and output semantics**, with one compile reused `N` times: + +`T_compiled_total(N) = T_cold + N × (T_bind + T_execute + T_verify)` +`T_baseline_total(N) = N × T_interpreted` + +Admit an **economic hypothesis** only when `T_baseline_total(N) > T_compiled_total(N)` for measured matched workloads. Also show cold-only, warm-only, first-call and nonsharing arms; cache invalidation by proof-law version, source generation, coordinate basis and compiler version. + +**Policy conflict requiring an explicit owner amendment before publishing any timings as PASS:** `CLAUDE.md` P0 currently says “no millisecond results anywhere, ever,” including labs and PRs. This PR **does not edit or silently override** that ruling. Request operator decision to distinguish offline compiler economics (which may be measured with appropriate time units) from immutable hot-path fold constraints, while retaining P0 no owned tuple/materialized row responses. Until then, keep reported timings descriptive of independent past measurements, never as an admitted result or benchmark PASS. + +## 3. Required independent semantics/refusals + +- **Set/Distinct versus Bag:** count duplicate derivations and foreign fan-out separately. Boolean OR path existence is not a bag count and XOR is not OR. Repeatedly derived value does not imply new NARS evidence. +- **Bool2 versus SQL K3:** valid FALSE is not invalid NULL or an independent UNKNOWN. No unsafe negation or complement rewrite. +- **E-class versus entity identity:** an egglog union is mathematical congruence, never an authority to merge external identities or GUIDs. +- **Snapshots and local coordinate binding:** the same ordinal in two contexts need not denote the same object. Check axis/source/codebook/permission generation before reuse. +- **Pure versus effectful extraction:** proof of equality does not commit a Lance write, authorize a read, or allow moving effects across version barriers. +- **No independent tuple oracle:** compare direct fold against independently implemented mask/reference folds; no owned-pair vector, BTreeSet answer, or hidden row materialization. +- **No runtime Ascent, MORK or datafrog fallback:** if template unsupported, typed refusal or separately authorized frontend behavior, never silently invoke another evaluator. + +## 4. Concrete first lab question + +Generate a *static*, rule-bounded reachability fixture with a shared intermediate coordinate: + +`Reach(x,z) :- Left(x,y), Right(y,z).` + +- Baseline A: existing Quack/RelAlg co-addressed direct bitmask fold. +- Candidate B: Ascent-generated **plan metadata only**, translated into the same mask fold, without executing Ascent runtime. +- Diagnostic C: source-audited `#[ds]` generated code illustrating whether BYODS retains tuple enumeration. Do not use C as a runtime contender if it violates P0. +- Negative: same `y` ordinal from another seal; 257th focus; two distinct intermediate paths (OR true/XOR false); duplicate bag answers; cyclic recursion candidate not admitted; no-sharing workload. +- If B is byte-identical and no cheaper or more broadly legal than A, **stop**, keep Ascent as literature/reference rather than introducing optimizer machinery. +- If B exposes a genuinely missing legal transformation, propose **one** owner-scoped lab code PR, with a separate build/test plan, not an architecture rewrite. + +## 5. Decision requested in EXO-50 + +1. Confirm cold-compiler amortization accounting as a *separate* explicit P0 exception/rule revision, rather than weakening the hot path. Until decided, no timing result promoted. +2. Authorize **A1 source/codegen audit only**, not a BYODS runtime adapter or a new Ascent/RelAlg executor. +3. Assign any A3 translator work to existing EXO-87 / D-SRAM and EXO-86 / D-RA owners, after their acknowledgement. No new plan family issue or D-id unless a unique deficiency survives A1–A3. +4. Keep egglog proof ownership and #1690–#1704 DR Math Foundry independent; no duplicate e-graph or proof verifier. + +**Outcome sought:** either precise evidence that Ascent contributes a reusable cold optimization to native DR folds, or a documented reason to leave the existing RelAlg/DR compiler alone. From ea30db9ba135fca809feac4b14c515c87d135a54 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:02:19 +0200 Subject: [PATCH 3/8] docs(plan): restore virtual tuple as DR mask intersection; sync P0 cold exception --- .../plans/ascent-byods-dr-fold-polyfill-v1.md | 47 +++++++++++++------ 1 file changed, 32 insertions(+), 15 deletions(-) diff --git a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md index 6749d4691..4790d76c6 100644 --- a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -1,7 +1,7 @@ # Ascent/BYODS → DR-native fold polyfill: staged falsification and cold-compiler plan **Status:** PROPOSAL / documentation only, 2026-10-22. No implementation, dependency, P0 policy, or production admission change authorized by this PR. -**Scope:** harvest Ascent's *logic compiler* capabilities and BYODS formalism to produce existing RelAlg/R2IL/DR procedures; do not create an Ascent-backed runtime, another database, or a competing MeTTa AST. +**Scope:** harvest Ascent's *logic compiler* capabilities and BYODS formalism to produce existing RelAlg/R2IL/DR procedures. A logical tuple is a **virtual relational projection through intersected masks and original lanes**, not an owned pair/row. Do not create an Ascent-backed runtime, another database, or a competing MeTTa AST. **Sources:** [BYODS primary-source excerpt](../../.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md), [author PDF](https://kmicinski.com/assets/byods.pdf), [AdaWorldAPI/ascent](https://github.com/AdaWorldAPI/ascent), [2026-10-21 prior evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). **Ownership:** [EXO-87](https://linear.app/exo-red/issue/EXO-87) D-SRAM; [EXO-84](https://linear.app/exo-red/issue/EXO-84) D-MTP; [EXO-85](https://linear.app/exo-red/issue/EXO-85) D-ASM; [EXO-79](https://linear.app/exo-red/issue/EXO-79) D-MPS-9; [EXO-86](https://linear.app/exo-red/issue/EXO-86) D-RA/D-CMR; [EXO-102](https://linear.app/exo-red/issue/EXO-102) D-RU; [EXO-46](https://linear.app/exo-red/issue/EXO-46) BIND admission; [EXO-73](https://linear.app/exo-red/issue/EXO-73) recursion driver; [EXO-50](https://linear.app/exo-red/issue/EXO-50) coordination. @@ -9,9 +9,9 @@ **Question:** can Ascent's compile-time rule dependency, SCC/stratification, bound/free matching and abstract-relation semantics be compiled into **already available**, certified RelAlg polyfill templates that produce R2IL or direct prebound DR SIMD? Then MeTTa and MORK are front-end aliases, not owners of a second execution model. -**Counter-hypothesis:** Ascent BYODS only substitutes its *relation provider*; its generated join loops and head writes still iterate over individual tuple bindings. A DR-backed `RelIndexRead` that yields bit positions one at a time is not a DR-native mask fold. +**Counter-hypothesis (about unmodified Ascent codegen only):** BYODS substitutes a *relation provider*, but Ascent's current generated join loops and head writes still iterate over individual bindings. A DR-backed `RelIndexRead` that yields positions one at a time is not itself a DR-native mask fold. **This does not reject a compiler rewrite** from Ascent's *logical* tuple operations to co-addressed mask intersections and borrowed lane projections. -**Binding ruling:** [2026-10-21 egglog/datafrog/Ascent evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) already ruled **SKIP** for Ascent as a hot runtime and withdrew tuple-native oracle roles. This research does not quietly reverse it. The difference is **cold compiler reuse**, not runtime delegation. +**Prior ruling and explicit correction:** [2026-10-21 evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP for Ascent's unmodified tuple-oriented runtime** and withdrew tuple-native oracle roles. The operator's counterproposal was to **intersect two masks and use the result as a logical tuple selector**. Rejection of owned tuple materialization must **not** be extrapolated to rejection of a virtual tuple computed by folds. This remains a cold compiler/lowering research question, not a claim that BYODS already generates DR-native code. ```text COLD [candidate only]: @@ -23,7 +23,7 @@ COLD [candidate only]: HOT [unchanged]: MeTTa/MORK/Datalog aliases -> Quack binding -> admitted compiled recipe -> R2IL/mask-risc/ndarray OR direct prebound DR bit folds - -> Count/Any/Keep/etc.; no tuple expansion + -> Count/Any/Keep/etc.; logical tuple = intersected presence + borrowed lane template, no owned row OFFLINE PROOF [separate owners]: egglog congruence, proof; Ruler/Enumo law candidates; eggcc effect extraction ``` @@ -35,16 +35,33 @@ Do not manufacture an extra compiler representation when `crepe_plan!`, contract | Stage | Narrow task | Falsifier / result gate | Status | |---|---|---|---| | **A0 source/ownership audit** | Extract BYODS formal model and compare Ascent source to D-SRAM, D-MTP, existing crepe-plan-probe and D-RU. Record conflict with old hot-path SKIP. | If no unique cold compiler feature is missing, PARK. | This docs PR | -| **A1 generated-code microscope** | Inspect fork `#[ds]` expansion, `rel_ind!`/`rel_ind_common!`, `RelIndexRead::index_get`, `RelIndexWrite` and one `R(x,y), S(y,z)` rule. Count per-binding iteration, owned tuples, head writes and indices. Source/codegen inspection before building anything. | If generated loops enumerate each match, **BYODS-only is NOT native fold execution**. Do not retrofit a new Ascent runtime in response. | Queued, lab-only authorization required | +| **A1 generated-code microscope** | Inspect fork `#[ds]` expansion and one `R(x,y), S(y,z)` rule. Classify (a) *logical* tuple bindings, (b) per-binding loop and head-emission code in current Ascent, (c) which logical joins could instead lower to intersected co-addressed masks. Count index and tuple allocations in existing code only. | If default generated loops enumerate each match, **BYODS-only is NOT a native fold**. That does **not** falsify an independent cold rewrite into DR masks. No runtime adapter unless separately authorized. | Queued, lab-only authorization required | | **A2 mathematical relation contract** | Specify finite-focus `D, inj, γ` (abstract lattice/domain, inject tuple logically, concretize without actually enumerating it) over sealed DR coordinates. Validate monotone `γ`, bottom, join laws and delta/total/new fixed-point semantics. | 257th out-of-focus slot, stale seal/ABA, non-monotone delta, changed coordinate identity or missing completeness must refuse. | Queued, docs/math first | | **A3 *cold* static rule planning** | Compare SCC, negation strata, lattice preconditions, binding propagation, join-order metadata with existing `crepe_plan!`, `set_rules` and Quack on identical fixed rules. No second AST or executor. | If metadata gives no new lawful plan shape or only a second spelling, PARK. Test negative cycle, repeated variable, disconnected rule and nested expression refusal. | Queued, requires EXO-87 coordination | -| **A4 DR-native lowering** | On presealed co-addressed source/target frame, translate one positive 2-hop rule into native `AND` + fold; compare existing direct bitmask/RelAlg execution. Preserve `ADMISSION=B`. | Any per-result `next()`/write, foreign value-driven gather, owned tuple, stale source, wrong bag fan-out, NULL/FALSE conflation, unadmitted bind or silent result truncation kills the path. | Gated on A1/A2/A3 and EXO-46 | +| **A4 DR-native *virtual tuple* lowering** | Lower a shared-coordinate conjunction to `eligible = mask_left AND mask_right`; use `eligible` as the index selector to borrow the original side lanes without producing `(x,z)` objects. Compare direct RelAlg/DR, test both functional and one-to-many facts. Preserve `ADMISSION=B`. | Wrong support coordinates, stale/mismatched basis, forbidden gather, owned-row allocations or wrong observable answers kill the rewrite. Multi-valued `y` requires factorized combinations or counted fan-out; an `AND` plane alone cannot emit the bag or `DISTINCT(x,z)`. An Ascent default per-result `next()` does not invalidate this alternate lowering. | Gated on A1/A2/A3 and EXO-46 | | **A5 equality and recursion boundary** | Counterexample: `a ≡ b` should imply `f(a) ≡ f(b)` under congruence; an `eqrel` provider alone cannot supply rebuilding/proofs. Separately check a ≤256-slot cyclic/diamond closure by *independent mask algorithm* against frontier folds. | No claim Ascent = egglog e-graph; no claim recursion is production (EXO-73). Refuse cross-version and out-of-scope closures. | Optional follow-up | | **A6 reuse economics** | Compare direct existing relalg/DR compile+execute to offline Ascent-derived schedule plus same hot recipe. Test shared-core 256 templates ×4096 focus frames, nonsharing control, cold cache hit/miss/staleness and negative syntax. | Net win only with *same workload and semantics*, accounting separately for cold compile, proof/verify, bind/attest, hot fold, outputs and memory. Avoid counting reduced tuple volume as a fold speedup. | Gated on real A3/A4 benefit | -## 2. Cold versus hot accounting: operator clarification requested +## 2. Physical interpretation of a logical tuple (operator correction) -**New operator observation, 2026-10-22:** a previously rejected **400–600 ms** overhead must be evaluated as possible *one-time cold compilation*, not automatically against the nanosecond *hot* target; the previous MeTTa/MORK workloads can run for many seconds. These measurements are **not paired on identical inputs** and must not be treated as a measured acceleration. +In an already witnessed *shared* intermediate coordinate domain `y`, let `L[y]` and `R[y]` be bit planes indicating that the left and right predicates have at least one matching binding. Then: + +```text +eligible_y = L_present & R_present // relational conjunction +EXISTS = Any(eligible_y) // existential question +COUNT_matching_y = PopCount(eligible_y) // count of eligible y slots, NOT bag pairs +virtual_binding(i) = (LeftLane[i], RightLane[i]), selected under eligible_y +``` + +`virtual_binding` means an address-level **template for reading original values**, not a created tuple. No `Vec<(x,z)>`, `BTreeSet`, per-result object, or re-sort is needed. A tuple-like *semantics* survives even when tuple *materialization* is forbidden. + +The equation by itself is **only a conjunction/existence mask**. If `Left(x,y)` or `Right(y,z)` has multiple values per `y`, the resulting logical bag contains a product of per-`y` fan-outs: `Σ_y left_count[y] × right_count[y]` for bag counting. If projected `DISTINCT(x,z)` is requested, de-duplicate pairs across `y` using an explicitly costed/falsified factorized representation or refuse the unsupported shape. Do not promise an `AND` mask is a complete general join. + +**Specific compiler hypothesis:** convert Ascent's logical tuple-at-a-time *rule IR* into a predicate/mask-template graph **before** its current iterator-and-head-emitter lowering. The present BYODS runtime remains ineligible, but it does not prove this compiler route impossible. Test a functionally unique `y` binding first, then non-functional and duplicate paths as mandatory counterexamples. + +## 3. Cold versus hot accounting: now recorded as scoped P0 exception + +**Operator observation, 2026-10-22:** an offline stage in the hundreds of thousands of microseconds is not comparable to a single nanosecond-scale fold; the MeTTa/MORK reference workloads can take many seconds. These are **not paired identical workloads**, so no acceleration is claimed. The same-day `CLAUDE.md` P0 amendment now explicitly permits reporting cold compiler/oracle costs in **µs, labelled 'reported, not gates'**. Mathematical break-even, for the **same program and output semantics**, with one compile reused `N` times: @@ -53,19 +70,19 @@ Mathematical break-even, for the **same program and output semantics**, with one Admit an **economic hypothesis** only when `T_baseline_total(N) > T_compiled_total(N)` for measured matched workloads. Also show cold-only, warm-only, first-call and nonsharing arms; cache invalidation by proof-law version, source generation, coordinate basis and compiler version. -**Policy conflict requiring an explicit owner amendment before publishing any timings as PASS:** `CLAUDE.md` P0 currently says “no millisecond results anywhere, ever,” including labs and PRs. This PR **does not edit or silently override** that ruling. Request operator decision to distinguish offline compiler economics (which may be measured with appropriate time units) from immutable hot-path fold constraints, while retaining P0 no owned tuple/materialized row responses. Until then, keep reported timings descriptive of independent past measurements, never as an admitted result or benchmark PASS. +**Already resolved P0 timing scope:** the existing 2026-10-22 `CLAUDE.md` **SCOPED EXCEPTION** allows cold compilation/proof and differential-oracle costs to be reported in **µs as informational, not gates**. Hot encode/lower/execute/terminals remain strictly constrained; no millisecond in-fold result is licensed. This PR does not edit P0 or claim a new exception. Only matched end-to-end economics can establish an amortization win, separately from hot-path acceptance. -## 3. Required independent semantics/refusals +## 4. Required independent semantics/refusals - **Set/Distinct versus Bag:** count duplicate derivations and foreign fan-out separately. Boolean OR path existence is not a bag count and XOR is not OR. Repeatedly derived value does not imply new NARS evidence. - **Bool2 versus SQL K3:** valid FALSE is not invalid NULL or an independent UNKNOWN. No unsafe negation or complement rewrite. - **E-class versus entity identity:** an egglog union is mathematical congruence, never an authority to merge external identities or GUIDs. - **Snapshots and local coordinate binding:** the same ordinal in two contexts need not denote the same object. Check axis/source/codebook/permission generation before reuse. - **Pure versus effectful extraction:** proof of equality does not commit a Lance write, authorize a read, or allow moving effects across version barriers. -- **No independent tuple oracle:** compare direct fold against independently implemented mask/reference folds; no owned-pair vector, BTreeSet answer, or hidden row materialization. +- **Logical tuple is not an owned tuple:** a logical pair may be represented by intersected membership masks and position-indexed borrowed lanes. Compare results using independent mask/reference folds; no owned-pair vector, BTreeSet answer, or hidden row materialization. - **No runtime Ascent, MORK or datafrog fallback:** if template unsupported, typed refusal or separately authorized frontend behavior, never silently invoke another evaluator. -## 4. Concrete first lab question +## 5. Concrete first lab question Generate a *static*, rule-bounded reachability fixture with a shared intermediate coordinate: @@ -78,10 +95,10 @@ Generate a *static*, rule-bounded reachability fixture with a shared intermediat - If B is byte-identical and no cheaper or more broadly legal than A, **stop**, keep Ascent as literature/reference rather than introducing optimizer machinery. - If B exposes a genuinely missing legal transformation, propose **one** owner-scoped lab code PR, with a separate build/test plan, not an architecture rewrite. -## 5. Decision requested in EXO-50 +## 6. Decision requested in EXO-50 -1. Confirm cold-compiler amortization accounting as a *separate* explicit P0 exception/rule revision, rather than weakening the hot path. Until decided, no timing result promoted. -2. Authorize **A1 source/codegen audit only**, not a BYODS runtime adapter or a new Ascent/RelAlg executor. +1. **Acknowledge the existing 2026-10-22 P0 cold-cost exception**: cold/opaque oracle costs reported in µs, not gate results. Preserve separate hot-fold admission; no further P0 amendment proposed. +2. Authorize **A1 source/codegen audit plus a docs-level logical tuple → AND-mask lowering sketch**, not a BYODS runtime adapter or a new Ascent/RelAlg executor. 3. Assign any A3 translator work to existing EXO-87 / D-SRAM and EXO-86 / D-RA owners, after their acknowledgement. No new plan family issue or D-id unless a unique deficiency survives A1–A3. 4. Keep egglog proof ownership and #1690–#1704 DR Math Foundry independent; no duplicate e-graph or proof verifier. From 1fb79d2e179b5c9b7b9940e4fd678109c30c2b87 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:02:58 +0200 Subject: [PATCH 4/8] docs(.arxiv): distinguish logical tuple mask intersection from tuple materialization --- ...opsla_byods_ascent_custom_relations_dr_excerpt.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md index 5feb7c51e..9eac21545 100644 --- a/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md +++ b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md @@ -26,25 +26,25 @@ ## Why this does **not** overturn the project's 2026-10-21 decision -Existing [evaluation map](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP** for Ascent/Datafrog/egglog as hot runtime executors: tuple-oriented iteration, materialized heads, second evaluator, and P0 fold-only/no-owned-tuples doctrine. BYODS changes *relation backing*, but Ascent's current code-generation protocol still asks for value iterators. It cannot be credited with a vectorized DR-native `And`/`Or`/`PopCount` terminal without proof that the emitted loop has disappeared. +Existing [evaluation map](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP** for unmodified Ascent/Datafrog/egglog hot runtime executors: tuple-oriented iteration, materialized heads, second evaluator, and P0 fold-only/no-owned-tuples doctrine. **Clarification:** a *logical tuple* is not the same as an *owned materialized tuple*. The operator's proposal is to compute matching bindings by two co-addressed mask intersections and borrow values through the resulting coordinate selector. The prior SKIP does not itself disprove that alternative compiler lowering. BYODS changes *relation backing*, but Ascent's current code-generation protocol still asks for value iterators. It cannot be credited with a vectorized DR-native `And`/`Or`/`PopCount` terminal without proof that the emitted loop has disappeared. -**Better question:** can Ascent's *rule analysis, SCC/strata, indices, deltas and relation semantics* be harvested **offline**, then compiled into the already-owned `contract → relalg/Quack → R2IL/mask-risc` or direct bound DR SIMD execution? Alternatively, can a BYODS adapter expose a native mask terminal *without* any tuple-value iteration? Both are research questions; the latter may be impossible without changing Ascent's compiler contract. +**Better question:** can Ascent's *logical rule bodies and tuple bindings* be compiled **before tuple code generation** into `eligible = left_mask AND right_mask` over an attested common address domain, with a borrowed lane-index template rather than an owned output pair? Can its SCC/strata/delta metadata then schedule the existing `contract → relalg/Quack → R2IL/mask-risc` or direct bound DR SIMD execution? Merely swapping Ascent storage through BYODS is a different, insufficient hypothesis. -Do not import Ascent's evaluator, provide an upstream crate dependency to production, or relabel the tuple-valued iterator as a zero-copy fold. +Do not import Ascent's evaluator, provide an upstream crate dependency to production, or relabel a tuple-valued iterator as a zero-copy fold. But **do not reject** a logical tuple compiled into a direct mask intersection on the grounds that Ascent's existing evaluator enumerates tuples. One-to-many `y` fan-out and `DISTINCT(x,z)` require additional factorized semantics or explicit refusal. ## Transfer hypotheses and must-fail tests | Question | Paper basis | Test / failure | | --- | --- | --- | | Can a DR plane be a well-behaved abstract relation? | `(D,inj,γ)`, Thm. 3.1 | Define finite-focus `γ` mathematically; monotonicity, same-coordinate identity, snapshot seal, and delta/cycle tests. If `γ` changes across a stale snapshot, refuse. | -| Does BYODS allow **native** mask evaluation? | §4 + value-iterator protocol | Inspect expanded `ascent!` / `#[ds]` code; count per-result `next()`/head writes, owned values, index memory. If every match is enumerated, classify BYODS as *interface-only*, not executor. | +| Can Ascent logical joins become a **native** mask fold? | §4 + BYODS value-iterator protocol | Inspect generated iterator/head code **and** independently sketch a compiler lowering of `R(x,y),S(y,z)` to co-addressed `AND` masks plus borrowed-lane projection. If unmodified code enumerates, classify *BYODS-only* as interface-only; separately test the alternate non-enumerating compiler lowering. Functional one-to-one first, then duplicated fan-out counterexamples. | | Can logical indexing be translated into borrowed positions? | §5.5 | Compare one sealed, independently attested global-to-local `$i` index with duplicate physical maps. No cross-table value-driven positional gather, including preparation. | | Can recursion use masks? | semi-naive + §5.3/5.4 | Verify frontier/total/new independently via direct bitset closure over ≤256 sealed coordinates; a 257th unseen index or cyclic/stale case refuses. No claim of EXO-73 production driver. | | Does `eqrel` replace egglog e-graphs? | §5.1 vs egglog | Union two term classes and require newly implied congruence between parent terms; without rebuilding and proof reconstruction, mark explicitly **NOT an e-graph**. | | Is reuse actually cheaper? | index-sharing | Measure compile/setup/attest/projection/read/fold/verification separately, plus 256 rules × 4096 reuses and a deliberately nonsharing suite. Never infer run-time win from reduced tuple counts. | -**Constraints:** P0 fold-only, no tuple materialization even for test outputs; no millisecond result reported as a success; use AdaWorldAPI forks; exact Set versus Bag/Distinct and K3 validity; `ADMISSION=B` for counted same-table seeks only; no foreign-value-driven gathers; proofs, source witnesses and commit receipts remain separate. +**Constraints:** P0 fold-only, no **owned** tuple materialization even for test outputs; a logical tuple can be an `AND` mask plus borrowed-lane template. The 2026-10-22 `CLAUDE.md` scoped exception permits **cold** compilation/proof/oracle costs to be reported in µs labelled *reported, not gates*; hot execution limits remain strict. Use AdaWorldAPI forks; exact Set versus Bag/Distinct and K3 validity; `ADMISSION=B` for counted same-table seeks only; no foreign-value-driven gathers; proofs, source witnesses and commit receipts remain separate. **Existing plans, not duplicated:** [D-MPS-9](../.claude/plans/mork-pathmap-schnellverschluss-v1.md), [D-MTP](../.claude/plans/metta-polyfill-v1.md), [D-RU](../.claude/plans/d-relalg-unified-v1.md), [Ascent/datafrog/egglog assessment](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). Proposed stages live in [Ascent BYODS DR plan](../.claude/plans/ascent-byods-dr-fold-polyfill-v1.md). -**Bottom line:** BYODS confirms the *formal possibility* of replacing relational storage without changing the logic. It does **not** yet solve DR-native rule execution. The immediate opportunity is to extract the compiler's rule schedule and relation abstraction, avoiding its tuple engine. +**Bottom line:** BYODS confirms the *formal possibility* of replacing relational storage without changing the logic, but its current tuple-generating backend is not a native DR fold. The stronger open hypothesis is to compile Ascent's **logical** tuple construction into a mask intersection and a *borrowed projection* before that backend runs. The first step is to falsify this lowering on non-functional, duplicated, stale and multi-coordinate joins, not to dismiss it because the unmodified backend emits tuples. From de8381b5854ba255c77ab1c99dfa3be45d08cf98 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:05:18 +0200 Subject: [PATCH 5/8] docs(plan): distinguish direct virtual tuple, search intersection and index-as-join --- .../plans/ascent-byods-dr-fold-polyfill-v1.md | 44 ++++++++++++------- 1 file changed, 29 insertions(+), 15 deletions(-) diff --git a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md index 4790d76c6..4594cc8c2 100644 --- a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -1,7 +1,7 @@ # Ascent/BYODS → DR-native fold polyfill: staged falsification and cold-compiler plan **Status:** PROPOSAL / documentation only, 2026-10-22. No implementation, dependency, P0 policy, or production admission change authorized by this PR. -**Scope:** harvest Ascent's *logic compiler* capabilities and BYODS formalism to produce existing RelAlg/R2IL/DR procedures. A logical tuple is a **virtual relational projection through intersected masks and original lanes**, not an owned pair/row. Do not create an Ascent-backed runtime, another database, or a competing MeTTa AST. +**Scope:** harvest Ascent's *logic compiler* capabilities and BYODS formalism to produce existing RelAlg/R2IL/DR procedures. A logical tuple is an **addressed projection of original lanes**. When the index itself witnesses the join, no mask intersection is required; when searching/filtering, intersect masks to obtain eligible addresses. Neither case constructs an owned pair/row. Do not create an Ascent-backed runtime, another database, or a competing MeTTa AST. **Sources:** [BYODS primary-source excerpt](../../.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md), [author PDF](https://kmicinski.com/assets/byods.pdf), [AdaWorldAPI/ascent](https://github.com/AdaWorldAPI/ascent), [2026-10-21 prior evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). **Ownership:** [EXO-87](https://linear.app/exo-red/issue/EXO-87) D-SRAM; [EXO-84](https://linear.app/exo-red/issue/EXO-84) D-MTP; [EXO-85](https://linear.app/exo-red/issue/EXO-85) D-ASM; [EXO-79](https://linear.app/exo-red/issue/EXO-79) D-MPS-9; [EXO-86](https://linear.app/exo-red/issue/EXO-86) D-RA/D-CMR; [EXO-102](https://linear.app/exo-red/issue/EXO-102) D-RU; [EXO-46](https://linear.app/exo-red/issue/EXO-46) BIND admission; [EXO-73](https://linear.app/exo-red/issue/EXO-73) recursion driver; [EXO-50](https://linear.app/exo-red/issue/EXO-50) coordination. @@ -9,9 +9,9 @@ **Question:** can Ascent's compile-time rule dependency, SCC/stratification, bound/free matching and abstract-relation semantics be compiled into **already available**, certified RelAlg polyfill templates that produce R2IL or direct prebound DR SIMD? Then MeTTa and MORK are front-end aliases, not owners of a second execution model. -**Counter-hypothesis (about unmodified Ascent codegen only):** BYODS substitutes a *relation provider*, but Ascent's current generated join loops and head writes still iterate over individual bindings. A DR-backed `RelIndexRead` that yields positions one at a time is not itself a DR-native mask fold. **This does not reject a compiler rewrite** from Ascent's *logical* tuple operations to co-addressed mask intersections and borrowed lane projections. +**Counter-hypothesis (about unmodified Ascent codegen only):** BYODS substitutes a *relation provider*, but Ascent's current generated join loops and head writes still iterate over individual bindings. A DR-backed `RelIndexRead` that yields positions one at a time is not itself a DR-native mask fold. **This does not reject a compiler rewrite** from Ascent's *logical* tuple operations to shared index/address projections, using mask intersections only for search/filtering. -**Prior ruling and explicit correction:** [2026-10-21 evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP for Ascent's unmodified tuple-oriented runtime** and withdrew tuple-native oracle roles. The operator's counterproposal was to **intersect two masks and use the result as a logical tuple selector**. Rejection of owned tuple materialization must **not** be extrapolated to rejection of a virtual tuple computed by folds. This remains a cold compiler/lowering research question, not a claim that BYODS already generates DR-native code. +**Prior ruling and explicit correction:** [2026-10-21 evaluation](../board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP for Ascent's unmodified tuple-oriented runtime** and withdrew tuple-native oracle roles. The operator's counterproposal distinguishes **tuple by index** from **tuple search**: values `A[i]` and `B[i]` form a virtual tuple at known `i`; mask intersections identify candidate `i` when searching. If a witnessed relationship index *is the join*, lookup needs neither a separate relational join nor unconditional intersection. Rejection of owned tuple materialization must **not** be extrapolated to rejection of any of these virtual forms. This remains a cold compiler/lowering research question, not a claim that BYODS already generates DR-native code. ```text COLD [candidate only]: @@ -23,7 +23,7 @@ COLD [candidate only]: HOT [unchanged]: MeTTa/MORK/Datalog aliases -> Quack binding -> admitted compiled recipe -> R2IL/mask-risc/ndarray OR direct prebound DR bit folds - -> Count/Any/Keep/etc.; logical tuple = intersected presence + borrowed lane template, no owned row + -> Count/Any/Keep/etc.; logical tuple = witnessed index + borrowed lane template; intersect selection masks only when needed; no owned row OFFLINE PROOF [separate owners]: egglog congruence, proof; Ruler/Enumo law candidates; eggcc effect extraction ``` @@ -35,25 +35,39 @@ Do not manufacture an extra compiler representation when `crepe_plan!`, contract | Stage | Narrow task | Falsifier / result gate | Status | |---|---|---|---| | **A0 source/ownership audit** | Extract BYODS formal model and compare Ascent source to D-SRAM, D-MTP, existing crepe-plan-probe and D-RU. Record conflict with old hot-path SKIP. | If no unique cold compiler feature is missing, PARK. | This docs PR | -| **A1 generated-code microscope** | Inspect fork `#[ds]` expansion and one `R(x,y), S(y,z)` rule. Classify (a) *logical* tuple bindings, (b) per-binding loop and head-emission code in current Ascent, (c) which logical joins could instead lower to intersected co-addressed masks. Count index and tuple allocations in existing code only. | If default generated loops enumerate each match, **BYODS-only is NOT a native fold**. That does **not** falsify an independent cold rewrite into DR masks. No runtime adapter unless separately authorized. | Queued, lab-only authorization required | +| **A1 generated-code microscope** | Inspect fork `#[ds]` expansion and one `R(x,y), S(y,z)` rule. Classify (a) *logical* tuple bindings, (b) per-binding loop and head-emission code in current Ascent, (c) which logical joins could lower to (i) indexed borrowed reads where the index is the join, or (ii) mask-intersection search over a shared coordinate. Count index and tuple allocations in existing code only. | If default generated loops enumerate each match, **BYODS-only is NOT a native fold**. That does **not** falsify an independent cold rewrite into DR masks. No runtime adapter unless separately authorized. | Queued, lab-only authorization required | | **A2 mathematical relation contract** | Specify finite-focus `D, inj, γ` (abstract lattice/domain, inject tuple logically, concretize without actually enumerating it) over sealed DR coordinates. Validate monotone `γ`, bottom, join laws and delta/total/new fixed-point semantics. | 257th out-of-focus slot, stale seal/ABA, non-monotone delta, changed coordinate identity or missing completeness must refuse. | Queued, docs/math first | | **A3 *cold* static rule planning** | Compare SCC, negation strata, lattice preconditions, binding propagation, join-order metadata with existing `crepe_plan!`, `set_rules` and Quack on identical fixed rules. No second AST or executor. | If metadata gives no new lawful plan shape or only a second spelling, PARK. Test negative cycle, repeated variable, disconnected rule and nested expression refusal. | Queued, requires EXO-87 coordination | -| **A4 DR-native *virtual tuple* lowering** | Lower a shared-coordinate conjunction to `eligible = mask_left AND mask_right`; use `eligible` as the index selector to borrow the original side lanes without producing `(x,z)` objects. Compare direct RelAlg/DR, test both functional and one-to-many facts. Preserve `ADMISSION=B`. | Wrong support coordinates, stale/mismatched basis, forbidden gather, owned-row allocations or wrong observable answers kill the rewrite. Multi-valued `y` requires factorized combinations or counted fan-out; an `AND` plane alone cannot emit the bag or `DISTINCT(x,z)`. An Ascent default per-result `next()` does not invalidate this alternate lowering. | Gated on A1/A2/A3 and EXO-46 | +| **A4 DR-native *virtual tuple* lowering** | Three distinct lowering shapes: (A) given `i`, read `LeftLane[i]` / `RightLane[i]` as an addressed virtual tuple; (B) unknown `i`, derive `eligible = mask_left AND mask_right`, then fold/projection; (C) a sealed global-to-local relationship index provides witnessed left/right offsets, so the **index is the join** and no second join is run. Compare direct RelAlg/DR, test both functional and one-to-many facts. Preserve `ADMISSION=B`. | Wrong support coordinates, stale/mismatched basis, forbidden gather, owned-row allocations or wrong observable answers kill the rewrite. Multi-valued `y` requires factorized combinations or counted fan-out; an `AND` plane alone cannot emit the bag or `DISTINCT(x,z)`. An Ascent default per-result `next()` does not invalidate this alternate lowering. | Gated on A1/A2/A3 and EXO-46 | | **A5 equality and recursion boundary** | Counterexample: `a ≡ b` should imply `f(a) ≡ f(b)` under congruence; an `eqrel` provider alone cannot supply rebuilding/proofs. Separately check a ≤256-slot cyclic/diamond closure by *independent mask algorithm* against frontier folds. | No claim Ascent = egglog e-graph; no claim recursion is production (EXO-73). Refuse cross-version and out-of-scope closures. | Optional follow-up | | **A6 reuse economics** | Compare direct existing relalg/DR compile+execute to offline Ascent-derived schedule plus same hot recipe. Test shared-core 256 templates ×4096 focus frames, nonsharing control, cold cache hit/miss/staleness and negative syntax. | Net win only with *same workload and semantics*, accounting separately for cold compile, proof/verify, bind/attest, hot fold, outputs and memory. Avoid counting reduced tuple volume as a fold speedup. | Gated on real A3/A4 benefit | -## 2. Physical interpretation of a logical tuple (operator correction) +## 2. Physical interpretation: tuple by construction, tuple by search, join as index -In an already witnessed *shared* intermediate coordinate domain `y`, let `L[y]` and `R[y]` be bit planes indicating that the left and right predicates have at least one matching binding. Then: +The operator's PowerShell shorthand `$hashA[$i].Value:$hashB[$i].Value` means the **logical composite view at a given address**, not allocation of an object. Three separate execution situations must not be conflated: ```text -eligible_y = L_present & R_present // relational conjunction -EXISTS = Any(eligible_y) // existential question -COUNT_matching_y = PopCount(eligible_y) // count of eligible y slots, NOT bag pairs -virtual_binding(i) = (LeftLane[i], RightLane[i]), selected under eligible_y +A. KNOWN ADDRESS (no search) + i is given and both lanes are complete at i: + logical_tuple(i) := LeftLane[i] : RightLane[i] // borrowed read only + +B. SEARCH (index not known) + selected_i := PredicateMaskLeft & PredicateMaskRight // same witnessed axis + fold selected_i over the borrowed original lanes + Any(selected_i) // existence, not tuple emission + +C. JOIN ALREADY ENCODED IN THE INDEX + binding[i] := { left_position, right_position } // compact address map, not value tuple + virtual_tuple(i) := LeftLane[binding[i].left] : RightLane[binding[i].right] + // No additional join operation or AND is inherent to the read. + // Only apply validity/presence/filter masks not guaranteed by the binding witness. ``` -`virtual_binding` means an address-level **template for reading original values**, not a created tuple. No `Vec<(x,z)>`, `BTreeSet`, per-result object, or re-sort is needed. A tuple-like *semantics* survives even when tuple *materialization* is forbidden. +Case C can collapse to case A when both sides are co-addressed at the same slot. A binding is sufficient only if it attests which keys were equated, completeness, source versions, coordinate bases, authorization and the claimed cardinality. A pointer map that encodes a value-derived foreign-row read not permitted by `ADMISSION=B` must refuse; an index is *not* a loophole for prohibited gathers. Counting preparation and attestation costs is mandatory. + +No `Vec<(x,z)>`, `BTreeSet`, result-object materialization or per-result sorting is required. The logical tuple is a **template over borrowed values**, and the relationship may be precompiled into its index. + +For case B, when `L[y]` and `R[y]` are presence masks on a common attested coordinate, `L & R` identifies eligible `y` slots. `PopCount(L & R)` counts matching **slots**, not necessarily joined logical result tuples or bag multiplicity. The equation by itself is **only a conjunction/existence mask**. If `Left(x,y)` or `Right(y,z)` has multiple values per `y`, the resulting logical bag contains a product of per-`y` fan-outs: `Σ_y left_count[y] × right_count[y]` for bag counting. If projected `DISTINCT(x,z)` is requested, de-duplicate pairs across `y` using an explicitly costed/falsified factorized representation or refuse the unsupported shape. Do not promise an `AND` mask is a complete general join. @@ -79,7 +93,7 @@ Admit an **economic hypothesis** only when `T_baseline_total(N) > T_compiled_tot - **E-class versus entity identity:** an egglog union is mathematical congruence, never an authority to merge external identities or GUIDs. - **Snapshots and local coordinate binding:** the same ordinal in two contexts need not denote the same object. Check axis/source/codebook/permission generation before reuse. - **Pure versus effectful extraction:** proof of equality does not commit a Lance write, authorize a read, or allow moving effects across version barriers. -- **Logical tuple is not an owned tuple:** a logical pair may be represented by intersected membership masks and position-indexed borrowed lanes. Compare results using independent mask/reference folds; no owned-pair vector, BTreeSet answer, or hidden row materialization. +- **Logical tuple is not an owned tuple:** a logical pair can be a *direct borrowed read at a known index*, an *AND-mask search* selecting indices, or a *witnessed relationship index that already is the join*. Compare results using independent mask/reference folds; no owned-pair vector, BTreeSet answer, or hidden row materialization. - **No runtime Ascent, MORK or datafrog fallback:** if template unsupported, typed refusal or separately authorized frontend behavior, never silently invoke another evaluator. ## 5. Concrete first lab question @@ -98,7 +112,7 @@ Generate a *static*, rule-bounded reachability fixture with a shared intermediat ## 6. Decision requested in EXO-50 1. **Acknowledge the existing 2026-10-22 P0 cold-cost exception**: cold/opaque oracle costs reported in µs, not gate results. Preserve separate hot-fold admission; no further P0 amendment proposed. -2. Authorize **A1 source/codegen audit plus a docs-level logical tuple → AND-mask lowering sketch**, not a BYODS runtime adapter or a new Ascent/RelAlg executor. +2. Authorize **A1 source/codegen audit plus a docs-level three-case lowering sketch (direct index / AND-mask search / index-as-join)**, not a BYODS runtime adapter or a new Ascent/RelAlg executor. 3. Assign any A3 translator work to existing EXO-87 / D-SRAM and EXO-86 / D-RA owners, after their acknowledgement. No new plan family issue or D-id unless a unique deficiency survives A1–A3. 4. Keep egglog proof ownership and #1690–#1704 DR Math Foundry independent; no duplicate e-graph or proof verifier. From 54cead4ee5a57be0e255cbb895e130fda4d9dca6 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:05:42 +0200 Subject: [PATCH 6/8] docs(.arxiv): distinguish tuple by index from mask search and index-as-join --- ...opsla_byods_ascent_custom_relations_dr_excerpt.md | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md index 9eac21545..f1b65e49a 100644 --- a/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md +++ b/.arxiv/2023_oopsla_byods_ascent_custom_relations_dr_excerpt.md @@ -26,25 +26,25 @@ ## Why this does **not** overturn the project's 2026-10-21 decision -Existing [evaluation map](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP** for unmodified Ascent/Datafrog/egglog hot runtime executors: tuple-oriented iteration, materialized heads, second evaluator, and P0 fold-only/no-owned-tuples doctrine. **Clarification:** a *logical tuple* is not the same as an *owned materialized tuple*. The operator's proposal is to compute matching bindings by two co-addressed mask intersections and borrow values through the resulting coordinate selector. The prior SKIP does not itself disprove that alternative compiler lowering. BYODS changes *relation backing*, but Ascent's current code-generation protocol still asks for value iterators. It cannot be credited with a vectorized DR-native `And`/`Or`/`PopCount` terminal without proof that the emitted loop has disappeared. +Existing [evaluation map](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md) ruled **SKIP** for unmodified Ascent/Datafrog/egglog hot runtime executors: tuple-oriented iteration, materialized heads, second evaluator, and P0 fold-only/no-owned-tuples doctrine. **Clarification:** a *logical tuple* is not the same as an *owned materialized tuple*. The operator's proposal has three distinct cases: (1) a known index directly addresses a virtual tuple of borrowed lanes, without intersection, (2) unknown indices are located by intersecting co-addressed selection masks, and (3) a witnessed global-to-local relationship index already represents the join, so neither a new join nor an unconditional AND is required to read. No case entails an owned tuple object. The prior SKIP does not itself disprove that alternative compiler lowering. BYODS changes *relation backing*, but Ascent's current code-generation protocol still asks for value iterators. It cannot be credited with a vectorized DR-native `And`/`Or`/`PopCount` terminal without proof that the emitted loop has disappeared. -**Better question:** can Ascent's *logical rule bodies and tuple bindings* be compiled **before tuple code generation** into `eligible = left_mask AND right_mask` over an attested common address domain, with a borrowed lane-index template rather than an owned output pair? Can its SCC/strata/delta metadata then schedule the existing `contract → relalg/Quack → R2IL/mask-risc` or direct bound DR SIMD execution? Merely swapping Ascent storage through BYODS is a different, insufficient hypothesis. +**Better question:** can Ascent's *logical rule bodies and tuple bindings* be compiled **before tuple code generation** into (a) direct borrowed reads under a known address, (b) `eligible = left_mask AND right_mask` for searches over an attested common address domain, or (c) direct reads through an attested relationship index that *is the join*, rather than an owned output pair? Can its SCC/strata/delta metadata then schedule the existing `contract → relalg/Quack → R2IL/mask-risc` or direct bound DR SIMD execution? Merely swapping Ascent storage through BYODS is a different, insufficient hypothesis. -Do not import Ascent's evaluator, provide an upstream crate dependency to production, or relabel a tuple-valued iterator as a zero-copy fold. But **do not reject** a logical tuple compiled into a direct mask intersection on the grounds that Ascent's existing evaluator enumerates tuples. One-to-many `y` fan-out and `DISTINCT(x,z)` require additional factorized semantics or explicit refusal. +Do not import Ascent's evaluator, provide an upstream crate dependency to production, or relabel a tuple-valued iterator as a zero-copy fold. But **do not reject** a logical tuple compiled into direct borrowed indexed reads, an indexed join view, or a search mask intersection on the grounds that Ascent's existing evaluator enumerates tuples. One-to-many `y` fan-out and `DISTINCT(x,z)` require additional factorized semantics or explicit refusal. ## Transfer hypotheses and must-fail tests | Question | Paper basis | Test / failure | | --- | --- | --- | | Can a DR plane be a well-behaved abstract relation? | `(D,inj,γ)`, Thm. 3.1 | Define finite-focus `γ` mathematically; monotonicity, same-coordinate identity, snapshot seal, and delta/cycle tests. If `γ` changes across a stale snapshot, refuse. | -| Can Ascent logical joins become a **native** mask fold? | §4 + BYODS value-iterator protocol | Inspect generated iterator/head code **and** independently sketch a compiler lowering of `R(x,y),S(y,z)` to co-addressed `AND` masks plus borrowed-lane projection. If unmodified code enumerates, classify *BYODS-only* as interface-only; separately test the alternate non-enumerating compiler lowering. Functional one-to-one first, then duplicated fan-out counterexamples. | +| Can Ascent logical joins become a **native** mask fold? | §4 + BYODS value-iterator protocol | Inspect generated iterator/head code **and** independently sketch three lowerings of `R(x,y),S(y,z)`: known-address borrowed projection; predicate-mask intersection for search; attested global-to-local relationship index-as-join with no redundant intersection. If unmodified code enumerates, classify *BYODS-only* as interface-only; separately test the alternate non-enumerating compiler lowering. Functional one-to-one first, then duplicated fan-out counterexamples. | | Can logical indexing be translated into borrowed positions? | §5.5 | Compare one sealed, independently attested global-to-local `$i` index with duplicate physical maps. No cross-table value-driven positional gather, including preparation. | | Can recursion use masks? | semi-naive + §5.3/5.4 | Verify frontier/total/new independently via direct bitset closure over ≤256 sealed coordinates; a 257th unseen index or cyclic/stale case refuses. No claim of EXO-73 production driver. | | Does `eqrel` replace egglog e-graphs? | §5.1 vs egglog | Union two term classes and require newly implied congruence between parent terms; without rebuilding and proof reconstruction, mark explicitly **NOT an e-graph**. | | Is reuse actually cheaper? | index-sharing | Measure compile/setup/attest/projection/read/fold/verification separately, plus 256 rules × 4096 reuses and a deliberately nonsharing suite. Never infer run-time win from reduced tuple counts. | -**Constraints:** P0 fold-only, no **owned** tuple materialization even for test outputs; a logical tuple can be an `AND` mask plus borrowed-lane template. The 2026-10-22 `CLAUDE.md` scoped exception permits **cold** compilation/proof/oracle costs to be reported in µs labelled *reported, not gates*; hot execution limits remain strict. Use AdaWorldAPI forks; exact Set versus Bag/Distinct and K3 validity; `ADMISSION=B` for counted same-table seeks only; no foreign-value-driven gathers; proofs, source witnesses and commit receipts remain separate. +**Constraints:** P0 fold-only, no **owned** tuple materialization even for test outputs; a logical tuple can be borrowed lanes at a known `i`, a search-selected mask, or a sealed index containing the join mapping. The 2026-10-22 `CLAUDE.md` scoped exception permits **cold** compilation/proof/oracle costs to be reported in µs labelled *reported, not gates*; hot execution limits remain strict. Use AdaWorldAPI forks; exact Set versus Bag/Distinct and K3 validity; `ADMISSION=B` for counted same-table seeks only; no foreign-value-driven gathers; proofs, source witnesses and commit receipts remain separate. **Existing plans, not duplicated:** [D-MPS-9](../.claude/plans/mork-pathmap-schnellverschluss-v1.md), [D-MTP](../.claude/plans/metta-polyfill-v1.md), [D-RU](../.claude/plans/d-relalg-unified-v1.md), [Ascent/datafrog/egglog assessment](../.claude/board/entries/2026-10-21-eval-egglog-datafrog-ascent.md). Proposed stages live in [Ascent BYODS DR plan](../.claude/plans/ascent-byods-dr-fold-polyfill-v1.md). -**Bottom line:** BYODS confirms the *formal possibility* of replacing relational storage without changing the logic, but its current tuple-generating backend is not a native DR fold. The stronger open hypothesis is to compile Ascent's **logical** tuple construction into a mask intersection and a *borrowed projection* before that backend runs. The first step is to falsify this lowering on non-functional, duplicated, stale and multi-coordinate joins, not to dismiss it because the unmodified backend emits tuples. +**Bottom line:** BYODS confirms the *formal possibility* of replacing relational storage without changing the logic, but its current tuple-generating backend is not a native DR fold. The stronger open hypothesis is to compile Ascent's **logical** tuple construction into *borrowed indexed projections*: intersect masks only when searching, and avoid a redundant join where the relationship index itself is the join. The first step is to falsify this lowering on non-functional, duplicated, stale and multi-coordinate joins, not to dismiss it because the unmodified backend emits tuples. From 6421bb867495a044136dc2a61bd2b892a718bc26 Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:07:37 +0200 Subject: [PATCH 7/8] docs(plan): DR Inception already owns nested virtual tuple/address perspectives --- .claude/plans/ascent-byods-dr-fold-polyfill-v1.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md index 4594cc8c2..9c96268a9 100644 --- a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -73,6 +73,21 @@ The equation by itself is **only a conjunction/existence mask**. If `Left(x,y)` **Specific compiler hypothesis:** convert Ascent's logical tuple-at-a-time *rule IR* into a predicate/mask-template graph **before** its current iterator-and-head-emitter lowering. The present BYODS runtime remains ineligible, but it does not prove this compiler route impossible. Test a functionally unique `y` binding first, then non-functional and duplicate paths as mandatory counterexamples. +### DR Inception is the preexisting virtual tuple carrier + +This is **not a proposal to introduce another tuple type**. Existing DR/Inception already expresses reusable nested perspectives over `WORLD × ANGLE × THOUGHT`: the *world* owns immutable source SoA lanes, the *angle* declares a witnessed global-to-local coordinate/address view, and the *thought* contributes focus-dependent masks and deltas. Descending into another perspective reuses the parent binding and extends the local mapping, without copying the underlying values. + +**At a bound coordinate `i`, the DR address frame is already a logical tuple/view**: it records which source-lane positions correspond, together with the coordinate/source-generation and mask/presence witnesses. The tuple's value is a *projection*, not a heap object. A DR/Inception node can also carry topology/frontier/provenance metadata and child perspectives; those are more expressive than a conventional pair tuple, not grounds for creating another record type. + +- **Already bound:** read the original `$hashA[$i].Value:$hashB[$i].Value` through DR/Inception's existing position map; no mask intersection or new join required. +- **Search:** intersect witnessed selection/presence masks to find matching local positions, then borrow original lane values at each selected position. +- **Join as index:** when a precomputed, independently verified relationship index binds A/B positions, that index **is** the compiled join, and later reads do not repeat it. +- **Nested Inception:** a deeper angle can refine the mask/coordinate view using the parent mapping, carrying the frontier into the child and reducing a result upward. Do not flatten all levels into an owned tuple table. + +**Scope distinction:** representing a virtual tuple is not the same as proving arbitrary join semantics. Multiple candidates per coordinate still require retained offsets/witnesses and a factorized bag/count or dedup strategy. An existing prepared index is valid only under the recorded `ADMISSION=B` snapshot, completeness and authorization tests. + +**Action for Ascent:** compile its *logical tuple/binding* into an **existing DR/Inception perspective and mask operator**, not a new `Tuple` structure and not a merely pointer-backed Ascent tuple iterator. Reuse the DR rules before minting an additional abstraction. + ## 3. Cold versus hot accounting: now recorded as scoped P0 exception **Operator observation, 2026-10-22:** an offline stage in the hundreds of thousands of microseconds is not comparable to a single nanosecond-scale fold; the MeTTa/MORK reference workloads can take many seconds. These are **not paired identical workloads**, so no acceleration is claimed. The same-day `CLAUDE.md` P0 amendment now explicitly permits reporting cold compiler/oracle costs in **µs, labelled 'reported, not gates'**. From e5c681cb97d8d280a4f1860f74615ef6481d5d5d Mon Sep 17 00:00:00 2001 From: AdaWorldAPI Date: Thu, 22 Oct 2026 19:09:32 +0200 Subject: [PATCH 8/8] docs(plan): make DR reasoning behavior explicit; distinguish probe from proposed Inception --- .../plans/ascent-byods-dr-fold-polyfill-v1.md | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md index 9c96268a9..34c820e31 100644 --- a/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -73,20 +73,21 @@ The equation by itself is **only a conjunction/existence mask**. If `Left(x,y)` **Specific compiler hypothesis:** convert Ascent's logical tuple-at-a-time *rule IR* into a predicate/mask-template graph **before** its current iterator-and-head-emitter lowering. The present BYODS runtime remains ineligible, but it does not prove this compiler route impossible. Test a functionally unique `y` binding first, then non-functional and duplicate paths as mandatory counterexamples. -### DR Inception is the preexisting virtual tuple carrier +### DR/Inception is a logical perspective, not a new tuple type -This is **not a proposal to introduce another tuple type**. Existing DR/Inception already expresses reusable nested perspectives over `WORLD × ANGLE × THOUGHT`: the *world* owns immutable source SoA lanes, the *angle* declares a witnessed global-to-local coordinate/address view, and the *thought* contributes focus-dependent masks and deltas. Descending into another perspective reuses the parent binding and extends the local mapping, without copying the underlying values. +The repository already has the required **conceptual separation**: canonical SoA values, an independently witnessed RelationshipMap / focus-index binding, and a thought-specific mask or delta. The expression `Thought(t)[T_a[i] : T_b[i]]` is the existing zero-copy logical-tuple idiom, not a request to allocate a tuple object. `WORLD × ANGLE × THOUGHT` is **navigation terminology**, not a concrete runtime `Inception` struct, tensor or new register (D-RPR §11.1 explicitly warns against that reading). -**At a bound coordinate `i`, the DR address frame is already a logical tuple/view**: it records which source-lane positions correspond, together with the coordinate/source-generation and mask/presence witnesses. The tuple's value is a *projection*, not a heap object. A DR/Inception node can also carry topology/frontier/provenance metadata and child perspectives; those are more expressive than a conventional pair tuple, not grounds for creating another record type. +**Implementation grade matters:** `Focus`, `CsrPred`, DR tiles and `ThoughtDelta` exist as measured/probe shapes in `mork-pathmap-probe`. The canonical RelationshipMap/MapPalette/ThoughtMapPaletteBinding store, lawful production global→local binding, and recursive child-angle driver remain proposed/gated. Do not cite a general nested Inception mechanism as already shipped. -- **Already bound:** read the original `$hashA[$i].Value:$hashB[$i].Value` through DR/Inception's existing position map; no mask intersection or new join required. -- **Search:** intersect witnessed selection/presence masks to find matching local positions, then borrow original lane values at each selected position. -- **Join as index:** when a precomputed, independently verified relationship index binds A/B positions, that index **is** the compiled join, and later reads do not repeat it. -- **Nested Inception:** a deeper angle can refine the mask/coordinate view using the parent mapping, carrying the frontier into the child and reducing a result upward. Do not flatten all levels into an owned tuple table. +The prospective **superpower** is the ability to encode *reasoning behavior* as a reusable, typed program over those already-owned carriers, with separate semantic proof, source witness and commit authority: +- **KNOWN i:** `A[i]:B[i]` is a virtual tuple/address projection; no search or mask intersection. +- **SEARCH:** intersect predicate/presence masks over a single attested domain to select qualifying `i`; the result remains a mask. +- **INDEX-AS-JOIN:** a legally prepared relationship map is itself the factored join mapping. Read the underlying lanes through that map; do not repeat an equijoin or add redundant intersections. +- **INFERENCE TRANSITION:** a rule-licensed, typed fold maps bound input masks to derived masks/frontiers; a thought delta records hypotheses while a proof/receipt records *why* the transformation is justified. For recursion, iterate the frontier only under a lawful driver and explicit convergence/complete-scope contract. -**Scope distinction:** representing a virtual tuple is not the same as proving arbitrary join semantics. Multiple candidates per coordinate still require retained offsets/witnesses and a factorized bag/count or dedup strategy. An existing prepared index is valid only under the recorded `ADMISSION=B` snapshot, completeness and authorization tests. +This is **not** an automatic theorem or proof: a mask encodes selected coordinates, and a register encodes a bounded relation, but a semantic inference needs its original premises, law/plan identity, snapshot scope, truth algebra and independent proof. Repeated proofs do not create independent CE64 evidence. A one-to-many relationship still needs factorized bag semantics or an explicit refusal. -**Action for Ascent:** compile its *logical tuple/binding* into an **existing DR/Inception perspective and mask operator**, not a new `Tuple` structure and not a merely pointer-backed Ascent tuple iterator. Reuse the DR rules before minting an additional abstraction. +**Ascent integration test:** preserve the Ascent rule's logic while replacing its physical tuple enumeration with one of the already permitted `KNOWN i`, `SEARCH` or `INDEX-AS-JOIN` shapes, plus an external/frontier schedule where needed. Do not build a separate Ascent tuple type, pretend BYODS auto-vectorizes, or use a precomputed pointer map to bypass `ADMISSION=B`. ## 3. Cold versus hot accounting: now recorded as scoped P0 exception