diff --git a/.claude/probes/2026-11-03-d-bag-fold/DECISION-PACKET.md b/.claude/probes/2026-11-03-d-bag-fold/DECISION-PACKET.md new file mode 100644 index 000000000..96e5e6173 --- /dev/null +++ b/.claude/probes/2026-11-03-d-bag-fold/DECISION-PACKET.md @@ -0,0 +1,273 @@ +# D-BAG-FOLD: operator decision packet (EXO-140 / EXO-46) + +**Status: DRAFT / PROPOSED / NOT IN FORCE.** This is decision preparation. It grants no +admission and authorizes no implementation. No code, probe, Linear status or +execution path is changed. + +**Evidence:** +- `main` @ `119787fc4`; +- #1937 (virtual composition, Arm P vs Arm L); +- #1938 (v3, production witness gaps, 26/26); +- #1939 (v4, construction-time attestation and candidate-gated execution, 21/21); +- this folder: `ARM-L-DECISION-MEMO.md`, `REPORT-V3.md`, `REPORT-V4.md`. + +EXO-50 was read to 2026-11-03 11:50. No operator message supersedes ADMISSION B, the +#1590 gather ban or the 2026-10-21 `$i` doctrine. + +## Source facts (read, not inferred) + +1. **ADMISSION B** (`.claude/board/entries/2026-10-20-six-decisions.md` §1): + - preparation may do "counted, version-witnessed, same-table key-range seeks over + an attested sorted key" and "construct a projection for subsequent co-addressed + evaluation"; + - "a position derived from another relational column or table is not admissible as + a read address"; + - "Execution remains co-addressed"; + - `Semijoin` / `EqU32Via` / `Gather` "need call-site classification". +2. **ISS-ADMISSION-PREP-BINDING** (ruled): the admitted evidence shape is a fold program + with no `Gather`. +3. **`CLAUDE.md`, 2026-10-21:** the only materialization the inversion makes is the + pointer table `$i`; everything else is "read in place through `$i`", one pointer per + column. +4. **`OrderedLaneWitness::forged(version, n_rows, digest)` is `pub`** + (`#[doc(hidden)]`, documented "falsifier-only", `crates/lance-graph-contract/src/ordered_lane.rs`). +5. **`lance_graph_dt64::dr::Frame` has no public constructor** + (`crates/lance-graph-dt64/src/dr.rs`). + - It is issued only by `FrameStore::seal`, and its identity is the issuing store + (`Weak` pointers; `same_issue`, `issued`). + - `Frame::revisions()` and `FrameStore::revisions()` expose the plain-data + `FrameRevisions { source, relation_map, coordinates }`. + - `FrameStore::check` accepts only the current seal and names only the first changed + revision (source → map → coordinates). +6. **mask-risc** `MaskOp::Gather { under: Option }`: an out-of-range index is the + zero-fallback. **Quack** `Node::Gather { under: Option }`: `gate_walk` gates an + `And`'s conjuncts by one resident plane only. +7. **v4 lab evidence:** + - construction-time presence witness and pointer lens; + - a forged pointer table whose digest is re-sealed passes digest verification (A7c); + - presence verification costs more than gated execution; + - register-gated execution scales with the candidate count. + +## 1. Authority is not integrity + +**Integrity** answers "is this the value that was recorded?" A digest or an +`OrderedLaneWitness` answers it. + +**Authority** answers "was this produced by the party allowed to produce it, by the +allowed method?" Neither a digest nor an `OrderedLaneWitness` can answer it: + +- `OrderedLaneWitness::forged` is public. Any crate can build a witness with any + version, row count and digest. +- A digest can be recomputed by anyone who holds the bytes (v4 A7c). + +So an ordered-lane witness, or any digest, **must not be treated as an authorization +token.** It is an integrity check that a party already holding authority uses. + +**What the certified lens needs instead:** + +- **Issuer-controlled construction:** no public constructor. Only the key-lane owner can + mint one, the way only `FrameStore::seal` can issue a `Frame`. +- **Immutable provenance:** the lens records the issue it was minted under and cannot + be changed afterwards. + +`Frame` is the existing model for that pattern. `OrderedLaneWitness` is not. + +**Current dependents of `forged`.** Classified here; nothing is changed in this PR. + +| site | kind | needs `pub`? | +|---|---|---| +| `crates/lance-graph-contract/src/ordered_lane.rs` lines 618, 624, 630, 808 | the contract's own `#[cfg(test)]` module | no: same crate | +| `crates/lance-graph-quack/src/lib.rs` lines 4589, 4705 | `#[cfg(test)] mod diamond_lowering_tests` | yes: cross-crate test | +| `crates/lance-graph-nal/tests/w2.rs` line 235 (`a_stale_witness_refuses_to_bind`) | integration test | yes: cross-crate test | + +No production caller exists. The two cross-crate test paths are the only compatibility +dependence. If the contract owner later restricts `forged`, those tests need another +route to a stale witness, for example a feature-gated test constructor or a real +reseal. That is the owner's call, not part of this PR. + +## 2. Pointer and presence lifetimes + +| evidence | depends on | invalidated by | should not be invalidated by | +|---|---|---|---| +| pointer lens `$i` | coordinate / key layout | a `coordinates` revision advance; a key reseal | a source-only (presence) mutation | +| presence attestation | the current relation facts | a `source` (or `relation_map`) revision advance | — | + +A source-only mutation therefore retires presence evidence without reminting `$i`. + +**Today's admission is coarser, and that is the binding behaviour.** +`FrameStore::check` refuses the whole frame on any change, which retires both. v4 A4′ +showed exactly that. + +**The narrower per-axis route is a proposal, not an existing admission:** + +- **Revision counters are not authority.** `FrameRevisions` is plain data, public + fields and `Copy`, so anyone can build one. A consumer comparing + `Frame::revisions()` against numbers it holds would be trusting values it cannot + authenticate. +- **The issuer must decide per axis.** A sound per-axis check is an *issuer-side* + operation. Given a `Frame` that `same_issue` / `issued` show to be its own, the + `FrameStore` answers "is the coordinates axis of this frame still current?" + separately from "is the source axis current?". That needs a new issuer method, or a + lens and attestation each holding their own issued token per axis. +- **Owner:** DT64 owner (`FrameStore`), with the contract owner for the lens types. It + is not built and not admitted. +- **Unknown:** whether such a per-axis answer stays sound across a reseal at equal + revisions (`FrameRefusal::FrameResealed`) is unchecked. + +**Blocked part.** No existing owner model forces a presence writer to advance `source`. +The planes are separate memory, with no write path through the frame store. Until the +plane / mailbox owner binds every presence write to the advance, a silent writer is +caught only after the fact, by the key-bound presence witness (v4 A5). It is not +refused at the write. **BLOCKED pending that owner.** + +**Cost classes, kept separate:** + +| class | cost | +|---|---| +| key-version mint | cold, once per coordinates revision | +| presence attestation | per source revision; v4 crossed 1 ms at ~14k rows with a full re-sort | +| per-query validation | O(1): issue identity plus revision checks | +| hot fold | µs, scales with candidates (v4 B3) | + +Cheap per-query validation is sound only if a mutation cannot bypass the advance. +Until that binding exists, cached verification is a correctness liability. Whether +mint and attestation costs fall under the no-ms rule's cold-cost exception is +**unclassified**; that is an operator decision and is not granted here. Copying +presence planes remains excluded. + +## 3. Recommended rulings — PROPOSED / NOT IN FORCE + +> **PROPOSED / NOT IN FORCE. Enacts nothing.** +> +> **EXO-140 (recommended).** A same-table, coordinate-derived, issuer-certified `$i` +> should be **eligible for classification as co-addressed execution**, although it +> lowers to `MaskOp::Gather`, provided all of these hold: +> +> 1. **Resident source planes:** only planes of the same table, never a mask any +> program produced. +> 2. **Verified provenance:** minted by the key-lane owner, through witnessed +> `SealedFacetLane` seeks keyed by arithmetic on each row's own key. Authority +> comes from issuer-controlled construction (§1), never from a digest. +> 3. **Correct frame and scope:** an issue of the right store; ClassId and prefix scope +> checked at mint. +> 4. **Bounds:** every pointer checked at mint. An out-of-range pointer is a refusal, +> never `Gather`'s zero-fallback. +> 5. **Generation:** valid only while its coordinates revision is current; the presence +> it reads is attested for the current source revision (§2). +> 6. **In-program gating:** the gather runs gated inside one program, and its result +> never leaves the program as a mask. +> +> **Remain prohibited:** +> - value-derived `Gather` (an index from any value lane or another table); +> - reuse of produced masks; +> - copied presence projections (Arm P); +> - scattered intermediates; +> - `OutgoingHop`; +> - recursion (EXO-73); +> - Bag multiplicity (EXO-108). +> +> **EXO-46 (recommended).** The `$i` pointer table is admissible in production +> execution only as such a certified lens: +> +> - **Mint:** the key-lane owner only. +> - **Mutate:** nobody; the lens is immutable. +> - **Invalidate:** the issuer, on a coordinates revision. +> - **Consume:** any fold that presents it, after the issuer-side validity check. + +**Reconciliation required before this can bind.** ADMISSION B says "execution remains +co-addressed", and its admitted pattern contains no `Gather`. The interpretation above +becomes binding only once **the operator explicitly reconciles that wording**. If the +operator reads "co-addressed" as "same row index", ADMISSION B excludes the +recommendation as written. The only zero-copy route left would then be a layout with +ancestor presence already at the candidate's row, which needs a derived population +(#1791, not authorized). + +**Strongest counterargument.** At execution time a certified read and a value-directed +gather are the same instruction. Their difference lives entirely in the mint, and +today no contract type records or enforces that provenance: + +- `OrderedLaneWitness` is forgeable; +- the certified lens type does not exist. + +Classifying the instruction before that type exists would admit it on trust. That is +why the ruling is phrased as *eligibility*, conditional on the lens type. + +## 4. Ownership and implementation gates + +Every implementation gate stays closed until its owner and the EXO-140 / EXO-46 +interpretation have acted. + +| owner | decides / owns | gate | +|---|---|---| +| **EXO-140 / EXO-46 operator** | the admission interpretation and its scope (§3); reconciliation of ADMISSION B; who owns call-site classification; whether mint and attestation costs fall under the cold-cost exception | closed: no ruling yet | +| **Contract owner** | the certified lens type (issuer-controlled, immutable); the presence attestation type; key uniqueness in sealing; lens identity (a second `SemanticLens`, or out of scope); the future of `forged` | closed until the operator rules | +| **DT64 owner** (`FrameStore`) | an issuer-side per-axis validity check; presence-writer binding to `source`, with the plane / mailbox owner | closed; per-axis route is only a proposal | +| **Quack owner** | candidate-gated lowering: gate each `Semijoin` conjunct of an `And` by the accumulated in-program register | closed until the lens type exists | +| **DT64 owner, later** | method-binding admission for a three-hop existence method (`GuardNotExecutable`, restricted DO shape) | separate gate; not touched | + +Quack lowering detail, for the owner: + +- sound for `And` (`x ∧ y = x ∧ (y under x)`); +- not sound inside `Or`; +- inside `Not`, the gate passes through but is never dropped; +- the register must come from conjuncts already lowered; +- mask-risc unchanged (`under: Some(Operand::Scratch)` already accepted). + +Tests the Quack owner would need: + +- existing lowering suites unchanged; +- a randomized `And` / `Or` / `Not` differential against a row oracle; +- v4 B1 parity and both B2 disables through Quack; +- a program-shape assertion; +- a no-ms timing comparison against v4 B3. + +## 5. Admission falsifiers + +| control | must be refused at | today | evidence | +|---|---|---|---| +| plane misaligned at construction | presence mint / first verify | lab only | v4 A2 | +| plane permuted after construction | presence verify (per generation) | lab only | v4 A3 | +| stale generation via the API | issuer check | production (whole frame) | v4 A4 | +| presence write without advance | the write (owner) | not enforceable | v4 A5 | +| duplicate key | seal / mint | lab only | v3 4a, v4 A6 | +| forged pointer table | mint authority | not enforceable (digest re-seal passes) | v4 A7c | +| pointer out of bounds | mint | lab only | v4 A7a/b | +| foreign ClassId pointer | mint | lab only | v4 A7d | +| wrong frame | issuer check | production | v4 A8a | +| stale key version | issuer check | production | v4 A8b | +| wrong lens | mint | not constructible | v4 A8c | +| value-derived index | mint | lab only | v3 7a, v4 A7c′ | +| produced mask as source plane | lowering / execution | not enforced | — | + +Silence twins: v4 B1 parity and the B2 disables must stay green under every check. + +## 6. Remaining decisions + +**Operator, decidable now:** + +1. EXO-140: is a certified `$i` read eligible for classification as co-addressed, and + how is ADMISSION B's wording reconciled? +2. EXO-46: does lens authority come from issuer-controlled construction by the key-lane + owner? +3. Who owns the EXO-140 call-site classification. + +**Owners, after 1 and 2:** the contract, DT64 and Quack items in §4. + +**Lacking evidence (do not decide yet):** + +- cold-cost classification of minting and attestation; +- whether an order-independent presence digest is acceptable (collision and + provenance not analysed); +- soundness of an issuer-side per-axis check across `FrameResealed`. + +## Next engineering step: OWNER DECISION + +- **No implementation is authorized or ready.** The experimental evidence is complete. + The remaining step is the operator's explicit ruling on §6 items 1–3. +- **If the operator rules yes:** the first engineering step would be for the contract + owner to *specify* the certified-lens and presence-attestation types against §5, + still without changing execution. +- **Until those types exist:** Quack lowering and any production `Gather` through `$i` + stay **NO-GO**. + +This packet closes the D-BAG-FOLD investigation. diff --git a/.claude/probes/2026-11-03-d-bag-fold/README.md b/.claude/probes/2026-11-03-d-bag-fold/README.md index 9fa92910c..ef86168a0 100644 --- a/.claude/probes/2026-11-03-d-bag-fold/README.md +++ b/.claude/probes/2026-11-03-d-bag-fold/README.md @@ -25,6 +25,7 @@ ndarray: the sibling checkout at `../ndarray` relative to the repo root | `REPORT-V3.md` | v3 results and the GO / NO-GO / NEEDS OWNER DECISION matrix | new | | `probe-v4/` | A: construction-time presence and pointer witnesses on production types; B: candidate-gated execution in one mask-risc program | new | | `REPORT-V4.md` | v4 results and the decision memo | new | +| `DECISION-PACKET.md` | operator decision packet for EXO-140 / EXO-46; DRAFT / PROPOSED / NOT IN FORCE | new | The originals are copies of artifacts that existed in this session's scratchpad. Nothing in `original/` was reconstructed.