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..f1b65e49a --- /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 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 (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 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 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 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 *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. 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..34c820e31 --- /dev/null +++ b/.claude/plans/ascent-byods-dr-fold-polyfill-v1.md @@ -0,0 +1,135 @@ +# 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 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. + +## 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 (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 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]: + 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.; 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 +``` + +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 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** | 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: tuple by construction, tuple by search, join as index + +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 +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. +``` + +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. + +**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 a logical perspective, not a new tuple type + +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). + +**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. + +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. + +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. + +**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 + +**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: + +`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. + +**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. + +## 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. +- **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 + +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. + +## 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 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. + +**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.