From 73238551eaa176cc81306d6a778a770df55d53c4 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 20:13:52 +0000 Subject: [PATCH 1/7] board: record D-FOUNDRY-PARITY-1 (#1991, #1995) and the LGJ knowledge transfer PR_ARC_INVENTORY gets arc entries for #1991 and #1995; LATEST_STATE a row for main after both; STATUS_BOARD marks D-FOUNDRY-PARITY-1 shipped and G1 partial (per-store cost done, limiting resource open as P1b); INTEGRATION_PLANS points at the new entry and EXO-223. New entry D-FOUNDRY-PARITY-1-P1A records arm C and the read-only LGJ crosswalk (the R11 layout-witness gap is D-DRISA-M1). Entries index regenerated; supersession index unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/board/INTEGRATION_PLANS.md | 2 +- .claude/board/LATEST_STATE.md | 6 ++++ .claude/board/PR_ARC_INVENTORY.md | 14 ++++++++ .claude/board/STATUS_BOARD.md | 4 +-- .../2026-11-10-foundry-parity-1-arm-c.md | 36 +++++++++++++++++++ .claude/board/entries/README.md | 3 +- 6 files changed, 61 insertions(+), 4 deletions(-) create mode 100644 .claude/board/entries/2026-11-10-foundry-parity-1-arm-c.md diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 458374e17..66f64fc64 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,6 +1,6 @@ ## 2026-11-10 — D-FOUNDRY-PARITY-1: DR × DT64 as an operational ontology → `.claude/plans/foundry-parity-v1.md` -**Status:** ACTIVE; Level R lab landed (`crates/foundry-parity-lab`). Evidence matrix over 18 Foundry capability rows, missing-contract register G1–G6, roadmap P0–P5. [entry](entries/2026-11-10-foundry-parity-1-lab.md) · STATUS_BOARD D-FOUNDRY-*. +**Status:** ACTIVE; Level R lab landed (#1991) and P1a arm C per-store cost (#1995); P1b (min/argmin) open. Evidence matrix over 18 Foundry capability rows, missing-contract register G1–G6, roadmap P0–P5. [entry](entries/2026-11-10-foundry-parity-1-lab.md) · [P1a](entries/2026-11-10-foundry-parity-1-arm-c.md) · STATUS_BOARD D-FOUNDRY-* · Linear EXO-223. **Confidence:** lab MEASURED; every Foundry-side cell is documented capability only (no comparator). No row claims parity. ## 2026-11-06 — D-LANESOCK: DR × DT64 property-to-lane socket and joint version witness → `.claude/plans/d-lanesock-dr-dt64-lane-socket-v1.md` diff --git a/.claude/board/LATEST_STATE.md b/.claude/board/LATEST_STATE.md index 574d06b0d..a644a0772 100644 --- a/.claude/board/LATEST_STATE.md +++ b/.claude/board/LATEST_STATE.md @@ -1,3 +1,9 @@ +## 2026-11-10 — main after #1991 (merged `637d638`) and #1995 (merged `15d4b4c`) — D-FOUNDRY-PARITY-1 + +- `crates/foundry-parity-lab` (excluded, own workspace): a 64-store × 64-category operating network over DT64 `LaneBinding` + mask-RISC. Arms A (materialized objects), B (`CanCook` / `CanFulfill` / `NetworkCapacity` / network cost, 0 bytes copied) and C (per-store cost as one INT8 GEMM via `ndarray::simd::int8_gemm_packed_strided`), against an independent scalar oracle; 24 tests. +- Refusals: stale frame, foreign scope, other row order, unmapped / unbound field, missing demanded cost lane, `u8` overflow, foreign menu revision, out-of-range quantity. Unknown stock is never zero; the denied store is `NotAuthorized`. +- Open: G1 remainder (limiting resource, P1b), G2–G6. Linear EXO-223. [entry](entries/2026-11-10-foundry-parity-1-arm-c.md) + ## 2026-11-06 — branch `ccr-fd2682ed-sai06j-scope-inventory` (D-LANESOCK-4, in PR) - Spec §8 records where a sealed reader scope and its issuer can live: OGAR `VerifiedLogin` is the only login proof, decisions are values not witnesses, `FrameStore` is the sealing precedent, and the issuer belongs in OGAR or downstream (dependency direction). No code. diff --git a/.claude/board/PR_ARC_INVENTORY.md b/.claude/board/PR_ARC_INVENTORY.md index e7f6e8919..0b92989cd 100644 --- a/.claude/board/PR_ARC_INVENTORY.md +++ b/.claude/board/PR_ARC_INVENTORY.md @@ -1,3 +1,17 @@ +## 2026-11-10 — lance-graph PR #1995 (merged `15d4b4c`) — D-FOUNDRY-PARITY-1 P1a: per-store cost via INT8 packed GEMM + +- **Added:** `foundry-parity-lab::arm_c` (`PreparedDemand` packed once per menu revision, `CostQuery::open` stages A once per binding, `per_store` runs one GEMM); `Network::set_unit_cost`; fair arm A comparator `store_costs`; bench rows; 8 integration tests; plan §5a. +- **Locked (measured):** oracle and null-model parity over 64 × 8 × q ∈ {1, 3, 128}; arm C summed over arm B's mask equals `network_cost`; refusals for missing demanded lane (Codex P2, red before the fix), `u8` overflow, stale frame, foreign menu revision, bad q; five disable runs red. Per-store cost 0.65–1.17 µs vs fair arm A 1.19–1.66 µs; 4 096 B staged. +- **Not done:** limiting resource / per-store max (P1b); scalar tier not run; scaling not measured. +- **Confidence:** CI green on merged head `288f130`. + +## 2026-11-10 — lance-graph PR #1991 (merged `637d638`) — D-FOUNDRY-PARITY-1: evidence matrix and 64-store lab + +- **Added:** `crates/foundry-parity-lab` (fixture, source owner implementing `LaneSource`, `World::bind`, arms A and B, scalar oracle, bench); `.claude/plans/foundry-parity-v1.md` (18-row matrix, G1–G6 register, roadmap); board entry, STATUS_BOARD and INTEGRATION_PLANS rows. +- **Locked (measured):** 16 tests at merge (oracle + null-model parity; refusals; negative controls; `answers()` validates q, Codex P2); `CanCook` 470 ns with 0 bytes copied; layer-cake per-store max ~15 µs vs 1.8 µs over built objects. +- **Not done:** element-wise arithmetic (G1); IAM, overlay frame, action gate, bound relations, method lowering (G2–G6). +- **Confidence:** CI green on the merged head. + ## 2026-11-06 — lance-graph PR #1970 (merged `fb27c46`) — D-LANESOCK-3: one field basis, test-only scope admission - **Added:** `LaneSource::lane_of(.., basis: &FieldRef, ..)` carries the field DT64 validated; `AbiLanes` holds no ClassView; three implementers updated; `AbiLanes::unwitnessed` and its suite moved to `#[cfg(test)]`, the `unwitnessed-scope` feature removed; spec §8 consumer contract and reader-scope inventory; board for #1969. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 19b13af4e..c8959c117 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -4,8 +4,8 @@ Execution admitted = meaning valid (OGAR/DT64) ∧ representation compatible (DR | D-id | Deliverable | Status | |---|---|---| -| D-FOUNDRY-PARITY-1 | Foundry parity evidence matrix + 64-store read-only lab (`crates/foundry-parity-lab`): CanCook / CanFulfill / NetworkCapacity / network cost via DT64 `borrow_all` + mask-RISC, oracle + materialized null model, refusals, negative controls | In PR | -| D-FOUNDRY-G1 | Element-wise cross-lane arithmetic (per-store max / limiting resource / per-store cost) in an admitted operator | Queued (decision needed) | +| D-FOUNDRY-PARITY-1 | Foundry parity evidence matrix + 64-store read-only lab (`crates/foundry-parity-lab`): CanCook / CanFulfill / NetworkCapacity / network cost via DT64 `borrow_all` + mask-RISC, oracle + materialized null model, refusals, negative controls; arm C per-store cost via INT8 GEMM | Shipped (#1991, #1995) | +| D-FOUNDRY-G1 | Element-wise cross-lane arithmetic (per-store max / limiting resource / per-store cost) in an admitted operator | Partial: per-store cost shipped (#1995); limiting resource / per-store max queued (P1b, decision needed) | | D-FOUNDRY-G2..G6 | IAM in the read path; scenario overlay frame; governed action gate; bound relations; method lowering from `MethodRef` | Queued | | D-SC-E1 | `MapTable::map_at` fenced as `diagnose_at` → `MapDiagnostic`; executable maps only via `map(frame)` | Shipped (#1981) | | D-SC-E2a | dt64 `CodeTable` (versioned code space, advances the lanes' FrameStore) + quack `bind_typed` / `TypedQuery::admit` (`StaleCodeSpace`, `Unwitnessed`) | In PR | diff --git a/.claude/board/entries/2026-11-10-foundry-parity-1-arm-c.md b/.claude/board/entries/2026-11-10-foundry-parity-1-arm-c.md new file mode 100644 index 000000000..ad1eeb82f --- /dev/null +++ b/.claude/board/entries/2026-11-10-foundry-parity-1-arm-c.md @@ -0,0 +1,36 @@ +# 2026-11-10 — D-FOUNDRY-PARITY-1-P1A: per-store cost as one INT8 GEMM; LGJ knowledge transfer + +**Status:** MEASURED (lab, read-only Level R). Crate `crates/foundry-parity-lab` +(arm C, `src/arm_c.rs`), merged in #1995 (`15d4b4c`). Plan: +`.claude/plans/foundry-parity-v1.md` §5a. Linear: EXO-223. + +**Question.** Can the per-store ingredient cost that mask-RISC cannot express +(register G1) be answered over the same DT64 binding with exact parity? + +**Answer.** Yes. `C[store][item] = Σ_k cost[store][k]·demand[k][item]` is one +`u8 × i8 → i32` GEMM through `ndarray::simd::int8_gemm_packed_strided` +(ndarray#418, AMX `TDPBUSD` tier on the lab host). 24 tests agree with the +scalar oracle and the materialized null model (64 stores × 8 items × +q ∈ {1, 3, 128}); arm C summed over arm B's `CanCook` mask equals arm B's +`network_cost`. Refused: a binding missing a demanded cost lane (`NotBound`, +Codex P2 on #1995), a cost that does not fit `u8` (never truncated), a stale +frame after a price change, a demand band from another menu revision, q +outside `1..=128`. Per-store cost 0.65–1.17 µs against 1.19–1.66 µs for arm A +over hoisted recipes; A is staged once per binding (4 096 B, counted). + +**Not established:** the limiting resource (element-wise min/argmin, the G1 +remainder, P1b — a decision); the kernel's scalar tier (the host has AMX); +scaling past one mask word. + +**LGJ knowledge transfer (read-only; EXO-223 comment).** lance-graph-java is +read as a consumer, never a dependency. Already solved in DT64: lazy +filtering with one crossing per terminal, projection without hydration, +named materialisation, lookup counting. Transferable: generated vocabularies +must dispatch through `ClassView`; a mechanical consumer-surface guard; a +source declaring a second stride reading of the same bytes (would remove arm +C's staging). R11: identity is already layout-free (`LaneAddr` has no stride), +but nothing witnesses layout — `FrameRevisions` has no layout field, so a +re-layout is invisible to `check`. That is D-DRISA-M1. LGJ `rbac.rs` unread. + +**OPEN:** G1 remainder (P1b); D-DRISA-M1 layout witness; generator from +`Resolved` to a typed vocabulary; G2–G6 unchanged. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index c0ba84432..8614214ad 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,13 +25,14 @@ index row, (3) no duplicate entry id. Checks 1 and 2 are deliberately opposite directions; the stranding this convention prevents shows up in exactly one of them, never both. -594 entries, 2026-08-06 .. 2026-11-10. +595 entries, 2026-08-06 .. 2026-11-10. | date | entry id | finding | file | |---|---|---|---| | 2026-11-10 | `lab-resolve-borrow-all` | | [2026-11-10-lab-resolve-borrow-all.md](2026-11-10-lab-resolve-borrow-all.md) | | 2026-11-10 | `int8-direct-packed-b` | | [2026-11-10-int8-direct-packed-b.md](2026-11-10-int8-direct-packed-b.md) | | 2026-11-10 | `D-FOUNDRY-PARITY-1` | | [2026-11-10-foundry-parity-1-lab.md](2026-11-10-foundry-parity-1-lab.md) | +| 2026-11-10 | `D-FOUNDRY-PARITY-1-P1A` | | [2026-11-10-foundry-parity-1-arm-c.md](2026-11-10-foundry-parity-1-arm-c.md) | | 2026-11-10 | `dt64-lane-borrow-all` | | [2026-11-10-dt64-lane-borrow-all.md](2026-11-10-dt64-lane-borrow-all.md) | | 2026-11-10 | `dt64-int8-facet-stride` | | [2026-11-10-dt64-int8-facet-stride.md](2026-11-10-dt64-int8-facet-stride.md) | | 2026-11-10 | `D-DT64-GEMM-SHAPE-1` | | [2026-11-10-dt64-gemm-shape.md](2026-11-10-dt64-gemm-shape.md) | From fcee68c9089ac5cd0a56d18a01e5d77a8fcaa23f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 20:36:23 +0000 Subject: [PATCH 2/7] foundry-parity-lab: CanCook as a registered DT64 method, lowered once per binding (G6) World::new registers one MethodBinding per (item, quantity in {1, 3}). Each binding's WHEN guard states the CanCook condition as a SetExpr over field positions, and its reads are exactly the fields the guard names. PreparedMethod::prepare does the following once per binding: - admits the MethodRef; - binds and borrows the reads plus storeId; - renames field positions to the bound planes and conjoins the reader scope (the IAM stand-in, never part of the method); - lowers the guard through relalg and keeps the returned mask-RISC program. run only executes that program. The lab writes no lowering. relalg gains rel_from_set, a public wrapper over the SetExpr -> Rel conversion run_program already applied (from_set stays crate-private), plus a round-trip test. The lab patches lance-graph-contract to the path crate, so its graph holds one contract and one ndarray. prepare refuses a lowering of more than one fold, because relalg keeps only the last fold's program. That cannot happen today, and a test pins that every guard shape lowers to one fold. Eight tests: - oracle parity for all 16 methods; - row-order independence; - the reader scope is load-bearing; - admit refuses a forged guard, another signature revision and another store's reference; - a method whose reads miss a guard field is refused NotBound; - repeated runs of one prepared method equal the first; - every guard shape lowers to one fold. Seven disable runs turned the suite red, each restored afterwards. A question takes 359-400 ns, level with arm B's hand-written program (474 ns). The first version re-lowered on every call and took ~21 us. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 56 ++- crates/foundry-parity-lab/Cargo.toml | 7 + crates/foundry-parity-lab/src/bin/bench.rs | 30 ++ crates/foundry-parity-lab/src/bind.rs | 8 +- crates/foundry-parity-lab/src/lib.rs | 3 + crates/foundry-parity-lab/src/method.rs | 331 ++++++++++++++++++ .../tests/integration/main.rs | 1 + .../tests/integration/method.rs | 211 +++++++++++ crates/lance-graph-relalg/src/lib.rs | 2 +- crates/lance-graph-relalg/src/normalize.rs | 21 ++ 10 files changed, 666 insertions(+), 4 deletions(-) create mode 100644 crates/foundry-parity-lab/src/method.rs create mode 100644 crates/foundry-parity-lab/tests/integration/method.rs diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index f9ba08321..20fde263b 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -32,6 +32,8 @@ instance; Foundry columns cite its public documentation only, as evidence of - [x] Bench in ns/µs (§6). - [x] P1a (2026-11-10): per-store cost through the INT8 packed GEMM (ndarray#418), arm C — oracle-exact, staged A counted (§5a, §6). - [ ] P1b: element-wise cross-lane arithmetic in an admitted operator (per-store max without the sweep, limiting resource) — see §7 G1. +- [x] P2 / G6 (2026-11-10): `CanCook` registered as a DT64 `MethodBinding` and executed from its `MethodRef`; the WHEN guard is lowered by relalg once per binding and executed per question, no lab lowering (§5b, §6). +- [ ] P2 / G5: recipe demand as bound relation lanes (§7 G5; waits on ADMISSION B, EXO-140). - [ ] P3: scenario overlay frame (§7 G3); governed action / writeback gate (§7 G4). - [ ] Production IAM in the read path instead of the lab stand-in (§7 G2). @@ -157,6 +159,46 @@ are defensive; no admitted fixture can reach them (feasibility predicates are all `≥ threshold(q)` with thresholds non-decreasing in q). They are labelled, not claimed as tested. +### 5b. G6 — `CanCook` as a registered method (P2, part) + +`crates/foundry-parity-lab/src/method.rs`. `World::new` registers one +`MethodBinding` per (item, quantity), quantity ∈ {1, 3}: the quantity is a +constant of the guard, and DT64 guards take no parameters, so it is part of +the method id. The WHEN guard says "this store can make `q` of item `m`" as a +`SetExpr` over field positions: mask fields as `Sym(field)`, value fields as +residuals on lane `field` (`stock_k ≥ d_k·q`, `staff ≥ ⌈q / per_staff⌉`, +offered, equipment, every demanded category known). `reads` is exactly the +fields the guard names; `effects` is empty (read-only). + +`PreparedMethod::prepare` admits the `MethodRef` (`BindStore::admit`), binds +`reads` + `storeId`, borrows them once, and renames field positions to the +bound planes. The reader scope (IAM stand-in) is conjoined there, never stored +in the method. `prepare` then lowers the guard ONCE through relalg +(`rel_from_set` + `run_with_program`) and keeps the returned mask-RISC +program; `run` only executes it (`execute_into`, `Out::Mask`). The lab writes +no lowering. `rel_from_set` is the one relalg addition: a public wrapper over +the conversion `run_program` already applied (`from_set`, crate-private). +`prepare` refuses a lowering of more than one fold (`Folds`), since relalg +keeps only the last fold's program; that tripwire cannot fire today, and a +test pins that every guard shape lowers to one fold. + +Tests (8, in `tests/integration/method.rs`): every registered method equals +the oracle's feasible set and count; another row order answers identically by +identity; the reader scope is load-bearing and outside the method; a reference +with another guard (`GuardMismatch`) or signature revision is refused, as is +one issued by another store (`ForeignStore`); a method whose `reads` misses a +field its guard names is refused (`NotBound`), never answered with the field +read as absent; repeated runs of one prepared method equal the first (the +scratch is reused); every guard shape lowers to one fold. Disable runs, each +red and restored: drop the staff conjunct; drop the known conjuncts; stock +threshold off by one; drop the reader scope; skip the identity mapping; lower +`All` instead of the guard; treat an unbound field as `All`. + +**Measured:** the first version called `run_program` per question, which +re-lowers every time: ~21 µs per question. Lowering once per binding brings a +question to 359–400 ns, level with arm B's hand-written program (474 ns), +and moves the one lowering into `prepare` (~15 µs, was ~9 µs). + ## 6. Measurement (MEASURED) `cargo run --release --manifest-path crates/foundry-parity-lab/Cargo.toml --bin bench`; @@ -181,6 +223,9 @@ three runs, ranges across runs: | arm C cold: prepare demand band (once per menu revision) | 452–629 | | arm C warm: per-store cost, 64 stores × 8 items, AMX `TDPBUSD` | 654–1 170 | | arm A: per-store cost, 64 × 8 (recipes read once) | 1 188–1 661 | +| G6: `method_ref` + `admit` | 5 054–5 254 | +| G6 cold: `PreparedMethod::prepare` (admit + bind + borrow + one lowering) | 14 874–15 193 | +| G6 warm: `CanCook(item 0, q 3)` run, cached mask-RISC program | 359–400 | Reading, not spin: a single WHERE-shaped question is ~4× cheaper in arm B and copies nothing; but the per-store maximum and the network capacity are ~8× @@ -197,6 +242,12 @@ once. A first comparator called `fx::recipe` per (store, item) and measured comparison. At 64 × 64 × 16 the GEMM is tiny; the per-call fixed cost (tile configuration, output mapping) likely dominates, and scaling is OPEN. +G6 (four runs; one more under load measured 600 ns and is excluded): a +registered method's question costs the same as arm B's hand-written program +once relalg's program is cached per binding (§5b). `admit` is ~5 µs (the +guard witness is normalized on issue and on admit). `World::new` now registers 16 +methods and costs ~48 µs (was ~25 µs with none); not separated further. + ## 7. Missing-contract register | Id | Missing operation | Why the current contract cannot express it | Lawful alternative today | Smallest test | Needs | @@ -206,7 +257,7 @@ comparison. At 64 × 64 × 16 the GEMM is tiny; the per-call fixed cost | G3 | Scenario overlay over a binding | No frame witness for a proposed, non-canonical plane | Oracle only | Store 12 closed: overlay answer = oracle, canonical frame unchanged | Overlay frame contract (H3) | | G4 | Governed action / writeback | No command identity, preconditions, idempotency, atomic commit or audit on this path; `MethodBinding::effects` is descriptive | none | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Separate gate; not in a read-only lab | | G5 | Bound relations (recipe → ingredient, menu → recipe) | Value-directed traversal is Gather, banned outside ADMISSION B | Relations as fixture functions (lab) | Bind recipe demand as lanes and answer without Gather | ADMISSION B decision | -| G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing; programs are hand-written | Hand-written programs | `CanCook` registered as a `MethodBinding`, lowered and executed | Lowering PR | +| G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing. LAB since §5b: admitted, bound, lowered once by relalg, executed per question at arm B's cost | — | Done in the lab: oracle parity, refusals, 359–400 ns per question | Production: who holds the prepared program across questions (no owner named) | ## 8. The three hypotheses @@ -231,7 +282,8 @@ None is chosen over the others; all three hold in part. enters mask-RISC/Quack, then re-run per-store max and limiting resource against the oracle. - **P2:** G6 + G5 — `CanCook` as a registered method lowered from its - `MethodRef`; recipe demand as bound relation lanes. + `MethodRef` (LAB, §5b, lowered once per binding); recipe demand as bound + relation lanes (waits on ADMISSION B). - **P3:** G3 scenario overlay frame; G4 action gate (preview vs commit) as a separate workstream; G2 IAM in the read path. - **P4:** real source connectors, a2ui screens, deployment. diff --git a/crates/foundry-parity-lab/Cargo.toml b/crates/foundry-parity-lab/Cargo.toml index 29b7a72c5..51a990bf7 100644 --- a/crates/foundry-parity-lab/Cargo.toml +++ b/crates/foundry-parity-lab/Cargo.toml @@ -22,10 +22,17 @@ description = "D-FOUNDRY-PARITY-1 lab: can source-owned planes, a DT64 lane bind lance-graph-dt64 = { path = "../lance-graph-dt64" } lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } lance-graph-contract = { path = "../lance-graph-contract" } +# G6: the WHEN guard of a registered method lowers through relalg (SetProgram -> R2IL -> one mask-RISC program). +lance-graph-relalg = { path = "../lance-graph-relalg" } # Arm C: the INT8 packed GEMM (ndarray#418), from the same coordinate # mask-risc uses, so the graph keeps one ndarray package. ndarray = { git = "https://github.com/AdaWorldAPI/ndarray", branch = "master", default-features = false, features = ["std"] } +# OGAR (via relalg -> r2il) depends on lance-graph-contract by git; patch it to +# the path crate so the graph holds ONE contract (relalg does the same). +[patch."https://github.com/AdaWorldAPI/lance-graph"] +lance-graph-contract = { path = "../lance-graph-contract" } + [[test]] name = "integration" path = "tests/integration/main.rs" diff --git a/crates/foundry-parity-lab/src/bin/bench.rs b/crates/foundry-parity-lab/src/bin/bench.rs index bc9b06891..c7538de6d 100644 --- a/crates/foundry-parity-lab/src/bin/bench.rs +++ b/crates/foundry-parity-lab/src/bin/bench.rs @@ -10,6 +10,7 @@ use foundry_parity_lab::arm_b::{demanded_fields, Guards, ItemQuery}; use foundry_parity_lab::arm_c::{cost_fields, CostQuery, PreparedDemand}; use foundry_parity_lab::bind::{World, READER, SPACE_A}; use foundry_parity_lab::fixture::{MENU_REV, STORES}; +use foundry_parity_lab::method::{method_id, PreparedMethod}; use foundry_parity_lab::source::{Network, Order}; use lance_graph_dt64::LaneSource; @@ -164,4 +165,33 @@ fn main() { black_box(objects.store_costs(black_box(3))); }), ); + + println!(); + let mref = world + .store + .method_ref(foundry_parity_lab::bind::CLASS, method_id(0, 3)) + .unwrap(); + report( + "G6: method_ref + admit", + median(|| { + let r = world + .store + .method_ref(foundry_parity_lab::bind::CLASS, method_id(0, 3)) + .unwrap(); + black_box(world.store.admit(&r).unwrap()); + }), + ); + report( + "G6 cold: prepare (admit+bind+borrow+lower)", + median(|| { + black_box(PreparedMethod::prepare(&world, &net, &mref, true).unwrap()); + }), + ); + let prepared = PreparedMethod::prepare(&world, &net, &mref, true).unwrap(); + report( + "G6: CanCook run (cached mask-RISC program)", + median(|| { + black_box(prepared.run().unwrap()); + }), + ); } diff --git a/crates/foundry-parity-lab/src/bind.rs b/crates/foundry-parity-lab/src/bind.rs index cdd861cb8..06c234927 100644 --- a/crates/foundry-parity-lab/src/bind.rs +++ b/crates/foundry-parity-lab/src/bind.rs @@ -121,7 +121,13 @@ impl Default for World { } impl World { + /// The class with every `CanCook` method of [`crate::method::methods`]. pub fn new() -> World { + World::with_methods(crate::method::methods()) + } + + /// The class with exactly `methods` registered. + pub fn with_methods(methods: Vec) -> World { let view = View( (0..FIELD_COUNT) .map(|f| FieldRef::new(predicate(field(f as u8)), format!("F{f}"))) @@ -137,7 +143,7 @@ impl World { field_count: FIELD_COUNT, extent: Extent::DR256_SQ_X64, }, - Vec::new(), + methods, ) .expect("the network class registers"); let version = store.route(POSITION, CLASS).expect("the class routes"); diff --git a/crates/foundry-parity-lab/src/lib.rs b/crates/foundry-parity-lab/src/lib.rs index d71b6a6f1..2572d0c7c 100644 --- a/crates/foundry-parity-lab/src/lib.rs +++ b/crates/foundry-parity-lab/src/lib.rs @@ -12,6 +12,8 @@ //! * [`bind`] is the class: its 211-field basis, route and demanded binding. //! * [`arm_b`] answers through `borrow_all` + mask-RISC programs. //! * [`arm_c`] answers per-store cost as one INT8 GEMM over staged A. +//! * [`method`] registers `CanCook` as a DT64 method and executes it from its +//! `MethodRef`, lowering the guard through relalg (G6). //! * [`arm_a`] is the materialized-object null model. //! * [`oracle`] answers from the fixture alone, and also evaluates the one //! scenario (Level S) the DR path cannot: no overlay contract exists. @@ -24,5 +26,6 @@ pub mod arm_b; pub mod arm_c; pub mod bind; pub mod fixture; +pub mod method; pub mod oracle; pub mod source; diff --git a/crates/foundry-parity-lab/src/method.rs b/crates/foundry-parity-lab/src/method.rs new file mode 100644 index 000000000..177a7d3ba --- /dev/null +++ b/crates/foundry-parity-lab/src/method.rs @@ -0,0 +1,331 @@ +//! G6 (P2, part): `CanCook` as a registered DT64 method, executed from its +//! `MethodRef`. +//! +//! DT64 binds behaviour and executes nothing. Here the store holds one +//! `MethodBinding` per (item, quantity) whose WHEN guard states "this store can +//! make `q` of item `m`" as a [`SetExpr`] over the class's field positions: +//! mask fields as `Sym(field)`, value fields as residuals on lane `field`. The +//! executor admits the reference, binds exactly the method's `reads`, renames +//! field positions to the bound planes, and lowers the guard through relalg +//! ONCE per binding in `prepare` (`run_with_program`, keeping the returned +//! mask-RISC program). `run` only executes that program. The lab writes no +//! lowering of its own; the rename is the only lab step. +//! +//! The reader scope (the IAM stand-in) is NOT part of the method. It is +//! conjoined at execution, so the registered behaviour stays the same for +//! every reader (gap G2 is where it is supplied for real). +//! +//! The quantity is a constant of the guard, so it is part of the method's +//! identity ([`method_id`]): DT64 guards carry no parameters. Only the +//! quantities in [`QS`] are registered. + +use lance_graph_contract::class_view::WideFieldMask; +use lance_graph_contract::set_algebra::{Cmp, Logic, Res, SetExpr}; +use lance_graph_contract::set_rules::{Population, Truth}; +use lance_graph_dt64::{ + Guard, LaneRefusal, MethodBinding, MethodId, MethodRef, Refusal, SigRev, ValueDemand, +}; +use lance_graph_mask_risc::{ + execute_into, tile_words_for, ExecError, Foreign, LaneRef, Out, Planes, Program, Scratch, +}; +use lance_graph_relalg::{rel_from_set, run_with_program, Measure, Query, RelError}; + +use crate::bind::{World, EQUIP0, KNOWN0, OFFERED0, READER, STAFF0, STOCK0, STORE_ID}; +use crate::fixture::{self as fx, DENIED_STORE, ITEMS, STORES, STORE_ID_BASE}; +use crate::source::{Network, Plane}; +use lance_graph_dt64::LaneSource; + +/// The quantities a `CanCook` method is registered for. +pub const QS: [i32; 2] = [1, 3]; + +/// The method id of `CanCook(item m, quantity q)`. +pub fn method_id(m: usize, q: i32) -> MethodId { + MethodId(((m as u32) << 8) | q as u32) +} + +/// "This store can make `q` of item `m`", over field positions. +pub fn can_cook_guard(m: usize, q: i32) -> SetExpr { + let r = fx::recipe(m); + let mut all = vec![ + SetExpr::Sym((OFFERED0 + m) as u32), + SetExpr::Sym((EQUIP0 + r.equipment) as u32), + ]; + for &(k, d) in &r.demand { + all.push(SetExpr::Sym((KNOWN0 + k) as u32)); + all.push(SetExpr::i32((STOCK0 + k) as u16, Cmp::Ge, d * q)); + } + // staff · per_staff ≥ q ⇔ staff ≥ ⌈q / per_staff⌉ for positive per_staff. + let staff = (q + r.per_staff - 1) / r.per_staff; + all.push(SetExpr::i32((STAFF0 + r.skill) as u16, Cmp::Ge, staff)); + SetExpr::And(all) +} + +/// The field positions a guard names. +fn guard_fields(e: &SetExpr, out: &mut Vec) { + match e { + SetExpr::Sym(f) => out.push(*f as u8), + SetExpr::Res(Res::I32 { lane, .. }) | SetExpr::Res(Res::U32 { lane, .. }) => { + out.push(*lane as u8) + } + SetExpr::And(cs) | SetExpr::Or(cs) => cs.iter().for_each(|c| guard_fields(c, out)), + SetExpr::Not(c) => guard_fields(c, out), + SetExpr::All | SetExpr::Empty => {} + } +} + +/// The binding of `CanCook(m, q)`: reads exactly the fields its guard names. +pub fn can_cook_method(m: usize, q: i32) -> MethodBinding { + let guard = can_cook_guard(m, q); + let mut fields = Vec::new(); + guard_fields(&guard, &mut fields); + let reads = WideFieldMask::from_positions(&fields); + MethodBinding { + id: method_id(m, q), + sig_rev: SigRev(1), + name: format!("CanCook(item {m}, q {q})"), + on: reads.clone(), + when: Some(Guard::new(guard, Logic::TwoValued)), + reads, + effects: Vec::new(), + population: Population::Distinct, + truth: Truth::TwoValued, + demand: ValueDemand::Values, + } +} + +/// Every registered `CanCook` method. +pub fn methods() -> Vec { + (0..ITEMS) + .flat_map(|m| QS.into_iter().map(move |q| can_cook_method(m, q))) + .collect() +} + +/// Why a method could not be executed. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum MethodRefusal { + /// The store did not admit the reference. + Admit(Refusal), + Lane(LaneRefusal), + /// relalg refused to lower the guard. + Lower(RelError), + /// The guard was answered from its description alone, so there is no + /// program to reuse; never expected for a CanCook guard. + Symbolic, + /// The guard lowered into more than one fold, so its last program alone + /// is not the answer and cannot be reused. A tripwire for a change in + /// relalg's lowering: today every `SetExpr` lowers to one fold under + /// `Keep` (pinned by `every_guard_shape_lowers_to_one_reusable_fold`). + Folds { + programs: usize, + }, + /// The lowered program could not run. + Exec(ExecError), + /// The method has no WHEN guard to execute. + NoGuard, + /// The guard names a field the method does not read. + NotBound { + field: u8, + }, + /// A bound plane had another kind than the guard uses it as. + PlaneKind { + field: u8, + }, + /// `storeId` was not bound. + NoIdentity, +} + +impl From for MethodRefusal { + fn from(r: LaneRefusal) -> Self { + MethodRefusal::Lane(r) + } +} + +/// The stores (bit = store row, by identity) that satisfy the guard, and how +/// many. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct Executed { + pub stores: u64, + pub count: u64, +} + +/// Where each bound field sits in the relalg planes. +#[derive(Clone, Copy)] +enum Slot { + Mask(u32), + I32(u16), + U32(u16), +} + +fn rename(e: &SetExpr, slots: &[Option; 256]) -> Result { + Ok(match e { + SetExpr::Sym(f) => match slots[*f as usize] { + Some(Slot::Mask(i)) => SetExpr::Sym(i), + Some(_) => return Err(MethodRefusal::PlaneKind { field: *f as u8 }), + None => return Err(MethodRefusal::NotBound { field: *f as u8 }), + }, + SetExpr::Res(Res::I32 { lane, op, t }) => match slots[*lane as usize] { + Some(Slot::I32(i)) => SetExpr::i32(i, *op, *t), + Some(_) => return Err(MethodRefusal::PlaneKind { field: *lane as u8 }), + None => return Err(MethodRefusal::NotBound { field: *lane as u8 }), + }, + SetExpr::Res(Res::U32 { lane, eq, v }) => match slots[*lane as usize] { + Some(Slot::U32(i)) => SetExpr::Res(Res::U32 { + lane: i, + eq: *eq, + v: *v, + }), + Some(_) => return Err(MethodRefusal::PlaneKind { field: *lane as u8 }), + None => return Err(MethodRefusal::NotBound { field: *lane as u8 }), + }, + SetExpr::And(cs) => SetExpr::And( + cs.iter() + .map(|c| rename(c, slots)) + .collect::>()?, + ), + SetExpr::Or(cs) => SetExpr::Or( + cs.iter() + .map(|c| rename(c, slots)) + .collect::>()?, + ), + SetExpr::Not(c) => SetExpr::negated(rename(c, slots)?), + SetExpr::All => SetExpr::All, + SetExpr::Empty => SetExpr::Empty, + }) +} + +/// A method made ready once per binding: admitted, its reads bound and +/// borrowed, its guard renamed onto the bound planes and lowered by relalg +/// once into a mask-RISC program. [`PreparedMethod::run`] only executes that +/// program, once per question. +pub struct PreparedMethod<'s> { + masks: Vec<&'s [u64]>, + lanes: Vec>, + ids: &'s [u32], + program: Program, + scratch: std::cell::RefCell>, +} + +impl<'s> PreparedMethod<'s> { + /// Admit `r`, bind the method's reads plus `storeId`, and rename its + /// guard (conjoined with the reader scope when `authorization`). + pub fn prepare( + world: &World, + source: &'s Network, + r: &MethodRef, + authorization: bool, + ) -> Result, MethodRefusal> { + let binding = world.store.admit(r).map_err(MethodRefusal::Admit)?; + let guard = binding.when.as_ref().ok_or(MethodRefusal::NoGuard)?; + let mut fields: Vec = (0..=255u8).filter(|&f| binding.reads.has(f)).collect(); + fields.push(STORE_ID as u8); + fields.sort_unstable(); + fields.dedup(); + let lanes_bound = world.bind(source, &fields, source.order().space(), READER)?; + + let mut masks: Vec<&'s [u64]> = Vec::new(); + let mut lanes: Vec> = Vec::new(); + let mut slots: [Option; 256] = [None; 256]; + let mut ids: Option<&'s [u32]> = None; + for lane in lanes_bound.borrow_all(&world.store, &world.view, source.frames(), source)? { + let (field, plane) = lane?; + let at = usize::from(field); + slots[at] = Some(match plane { + Plane::Mask(w) => { + masks.push(w); + Slot::Mask((masks.len() - 1) as u32) + } + Plane::I32(v) => { + lanes.push(LaneRef::I32(v)); + Slot::I32((lanes.len() - 1) as u16) + } + Plane::U32(v) => { + if at == STORE_ID { + ids = Some(v); + } + lanes.push(LaneRef::U32(v)); + Slot::U32((lanes.len() - 1) as u16) + } + }); + } + let ids = ids.ok_or(MethodRefusal::NoIdentity)?; + let mut query = rename(&guard.expr, &slots)?; + if authorization { + let Some(Slot::U32(id_lane)) = slots[STORE_ID] else { + return Err(MethodRefusal::NoIdentity); + }; + query = SetExpr::And(vec![query, SetExpr::ne_u32(id_lane, DENIED_STORE)]); + } + let planes = Planes { + n_rows: STORES, + masks: &masks, + lanes: &lanes, + }; + let mut keep = [0u64; 1]; + let (lowered, program) = run_with_program( + &Query { + rel: rel_from_set(&query), + measure: Measure::Keep, + }, + &planes, + Some(&mut keep[..]), + ) + .map_err(MethodRefusal::Lower)?; + let program = program.ok_or(MethodRefusal::Symbolic)?; + // relalg keeps only the LAST fold's program. Re-running it alone is the + // whole answer only when the lowering was one fold. + if lowered.programs != 1 { + return Err(MethodRefusal::Folds { + programs: lowered.programs, + }); + } + let scratch = std::cell::RefCell::new(Scratch::new( + tile_words_for(STORES), + program.scratch_slots as usize, + )); + Ok(PreparedMethod { + masks, + lanes, + ids, + program, + scratch, + }) + } + + /// One question: the stores satisfying the guard, and how many. + pub fn run(&self) -> Result { + let planes = Planes { + n_rows: STORES, + masks: &self.masks, + lanes: &self.lanes, + }; + let mut keep = [0u64; 1]; + execute_into( + &self.program, + &planes, + &Foreign::NONE, + &mut self.scratch.borrow_mut(), + Out::Mask(&mut keep[..]), + ) + .map_err(MethodRefusal::Exec)?; + let count = u64::from(keep[0].count_ones()); + // Positions become stores only by reading `storeId` at the set bits. + let mut stores = 0u64; + let mut w = keep[0]; + while w != 0 { + let row = w.trailing_zeros() as usize; + stores |= 1 << (self.ids[row] - STORE_ID_BASE); + w &= w - 1; + } + Ok(Executed { stores, count }) + } +} + +/// [`PreparedMethod::prepare`] then one [`PreparedMethod::run`]. +pub fn execute_can_cook( + world: &World, + source: &Network, + r: &MethodRef, + authorization: bool, +) -> Result { + PreparedMethod::prepare(world, source, r, authorization)?.run() +} diff --git a/crates/foundry-parity-lab/tests/integration/main.rs b/crates/foundry-parity-lab/tests/integration/main.rs index 5c54dd5b6..6e48c8fef 100644 --- a/crates/foundry-parity-lab/tests/integration/main.rs +++ b/crates/foundry-parity-lab/tests/integration/main.rs @@ -4,5 +4,6 @@ pub mod common; pub mod controls; pub mod cost; +pub mod method; pub mod parity; pub mod refusals; diff --git a/crates/foundry-parity-lab/tests/integration/method.rs b/crates/foundry-parity-lab/tests/integration/method.rs new file mode 100644 index 000000000..70a7fd630 --- /dev/null +++ b/crates/foundry-parity-lab/tests/integration/method.rs @@ -0,0 +1,211 @@ +//! G6: `CanCook` registered as a DT64 method and executed from its +//! `MethodRef`; its WHEN guard is lowered through relalg, never hand-written. + +use foundry_parity_lab::bind::{World, CLASS, KNOWN0, STOCK0}; +use foundry_parity_lab::fixture::{self as fx, STORES}; +use foundry_parity_lab::method::{ + can_cook_method, execute_can_cook, method_id, MethodRefusal, PreparedMethod, QS, +}; +use foundry_parity_lab::oracle::{Cook, Oracle}; +use foundry_parity_lab::source::{Network, Order}; +use lance_graph_contract::set_algebra::{Logic, SetExpr}; +use lance_graph_dt64::{Guard, MethodRef, Refusal, SigRev}; + +/// Store rows the oracle says can make `q` of `m`. +fn oracle_set(m: usize, q: i32) -> u64 { + (0..STORES) + .filter(|&s| { + matches!( + Oracle::BASELINE.can_cook(s, m, q), + Cook::Known { feasible: true, .. } + ) + }) + .fold(0u64, |w, s| w | 1 << s) +} + +fn mref(world: &World, m: usize, q: i32) -> MethodRef { + world.store.method_ref(CLASS, method_id(m, q)).unwrap() +} + +#[test] +fn every_registered_can_cook_method_matches_the_oracle() { + let world = World::new(); + let net = Network::ingest(Order::Identity); + for m in 0..fx::ITEMS { + for q in QS { + let got = execute_can_cook(&world, &net, &mref(&world, m, q), true).unwrap(); + let want = oracle_set(m, q); + assert_eq!(got.stores, want, "item {m} q {q}"); + assert_eq!(got.count, u64::from(want.count_ones()), "item {m} q {q}"); + } + } + // Anti-vacuity: the guard selects some stores and rejects others. + let s = oracle_set(0, 3); + assert!(s != 0 && s.count_ones() < STORES as u32); +} + +#[test] +fn another_row_order_answers_identically_by_identity() { + let world = World::new(); + let a = Network::ingest(Order::Identity); + let b = Network::ingest(Order::Reversed); + for m in 0..fx::ITEMS { + let x = execute_can_cook(&world, &a, &mref(&world, m, 1), true).unwrap(); + let y = execute_can_cook(&world, &b, &mref(&world, m, 1), true).unwrap(); + assert_eq!(x.stores, y.stores, "item {m}"); + } +} + +#[test] +fn the_reader_scope_is_load_bearing_and_separate_from_the_method() { + let world = World::new(); + let net = Network::ingest(Order::Identity); + let row = fx::case::HIDDEN; + let with = execute_can_cook(&world, &net, &mref(&world, 0, 1), true).unwrap(); + let without = execute_can_cook(&world, &net, &mref(&world, 0, 1), false).unwrap(); + assert_eq!( + with.stores >> row & 1, + 0, + "the denied store is never answered" + ); + assert_eq!( + without.stores >> row & 1, + 1, + "its stock would satisfy the guard" + ); + assert_eq!(with.stores, without.stores & !(1 << row)); +} + +#[test] +fn a_reference_with_another_guard_is_refused() { + let world = World::new(); + let net = Network::ingest(Order::Identity); + let forged = MethodRef { + guard: Some(Guard::new(SetExpr::All, Logic::TwoValued).witness()), + ..mref(&world, 0, 1) + }; + assert!(matches!( + execute_can_cook(&world, &net, &forged, true), + Err(MethodRefusal::Admit(Refusal::GuardMismatch { .. })) + )); + let other_rev = MethodRef { + sig_rev: SigRev(2), + ..mref(&world, 0, 1) + }; + assert!(matches!( + execute_can_cook(&world, &net, &other_rev, true), + Err(MethodRefusal::Admit( + Refusal::SignatureRevisionMismatch { .. } + )) + )); + // Silent half: the issued reference executes. + assert!(execute_can_cook(&world, &net, &mref(&world, 0, 1), true).is_ok()); +} + +#[test] +fn a_reference_issued_by_another_store_is_refused() { + let world = World::new(); + let other = World::new(); + let net = Network::ingest(Order::Identity); + assert!(matches!( + execute_can_cook(&world, &net, &mref(&other, 0, 1), true), + Err(MethodRefusal::Admit(Refusal::ForeignStore { .. })) + )); +} + +#[test] +fn a_method_whose_reads_miss_a_guard_field_is_refused() { + let k = fx::recipe(0).demand[0].0; + let mut bad = can_cook_method(0, 1); + bad.reads = lance_graph_contract::class_view::WideFieldMask::from_positions( + &(0..=255u8) + .filter(|&f| bad.reads.has(f) && usize::from(f) != STOCK0 + k) + .collect::>(), + ); + bad.on = bad.reads.clone(); + let world = World::with_methods(vec![bad]); + let net = Network::ingest(Order::Identity); + match execute_can_cook(&world, &net, &mref(&world, 0, 1), true) { + Err(MethodRefusal::NotBound { field }) => assert_eq!(usize::from(field), STOCK0 + k), + other => panic!("expected NotBound, got {other:?}"), + } + // The known-mask field of the same category is still read: only the + // dropped value lane is missing. + assert!(can_cook_method(0, 1).reads.has((KNOWN0 + k) as u8)); +} + +/// The invariant `PreparedMethod` relies on to reuse relalg's program: a +/// `Keep` over any `SetExpr` shape lowers to exactly one fold. If relalg ever +/// lowers one into several, `prepare` refuses (`Folds`) and this test names +/// the shape. +#[test] +fn every_guard_shape_lowers_to_one_reusable_fold() { + use lance_graph_contract::set_algebra::Cmp; + use lance_graph_mask_risc::{LaneRef, Planes}; + use lance_graph_relalg::{rel_from_set, run_with_program, Measure, Query}; + let m = [0xF0F0u64]; + let l: Vec = (0..64).collect(); + let u: Vec = (0..64).collect(); + let masks: [&[u64]; 2] = [&m, &m]; + let lanes = [LaneRef::I32(&l), LaneRef::U32(&u)]; + let planes = Planes { + n_rows: 64, + masks: &masks, + lanes: &lanes, + }; + let shapes = [ + SetExpr::And(vec![SetExpr::Sym(0), SetExpr::i32(0, Cmp::Ge, 3)]), + SetExpr::Or(vec![SetExpr::Sym(0), SetExpr::i32(0, Cmp::Ge, 30)]), + SetExpr::negated(SetExpr::And(vec![SetExpr::Sym(1), SetExpr::ne_u32(1, 5)])), + SetExpr::Or(vec![ + SetExpr::And(vec![SetExpr::Sym(0), SetExpr::negated(SetExpr::Sym(1))]), + SetExpr::And(vec![SetExpr::i32(0, Cmp::Lt, 9), SetExpr::eq_u32(1, 4)]), + ]), + can_cook_guard_on_dense_planes(), + ]; + for e in shapes { + let mut keep = [0u64; 1]; + let (run, program) = run_with_program( + &Query { + rel: rel_from_set(&e), + measure: Measure::Keep, + }, + &planes, + Some(&mut keep[..]), + ) + .unwrap(); + assert_eq!(run.programs, 1, "{e:?}"); + assert!(program.is_some(), "{e:?}"); + } +} + +/// A CanCook-shaped conjunction (masks AND thresholds) over the two dense +/// planes the shape test supplies. +fn can_cook_guard_on_dense_planes() -> SetExpr { + use lance_graph_contract::set_algebra::Cmp; + SetExpr::And(vec![ + SetExpr::Sym(0), + SetExpr::Sym(1), + SetExpr::i32(0, Cmp::Ge, 2), + SetExpr::i32(0, Cmp::Ge, 5), + SetExpr::ne_u32(1, 7), + ]) +} + +/// The program is lowered once and its scratch reused: every later run of one +/// prepared method must equal the first and the oracle. +#[test] +fn a_prepared_method_answers_the_same_on_every_run() { + let world = World::new(); + let net = Network::ingest(Order::Identity); + for m in 0..fx::ITEMS { + for q in QS { + let p = PreparedMethod::prepare(&world, &net, &mref(&world, m, q), true).unwrap(); + let first = p.run().unwrap(); + assert_eq!(first.stores, oracle_set(m, q), "item {m} q {q}"); + for _ in 0..3 { + assert_eq!(p.run().unwrap(), first, "item {m} q {q}"); + } + } + } +} diff --git a/crates/lance-graph-relalg/src/lib.rs b/crates/lance-graph-relalg/src/lib.rs index 760708f94..313237a3f 100644 --- a/crates/lance-graph-relalg/src/lib.rs +++ b/crates/lance-graph-relalg/src/lib.rs @@ -36,5 +36,5 @@ pub mod program; pub use ir::{Atom, Cmp, Measure, Query, Rel}; pub use lower::{run, run_as_written, run_with_program, Answer, RelError, Run}; -pub use normalize::{normalize, symbolic}; +pub use normalize::{normalize, rel_from_set, symbolic}; pub use program::{run_program, run_recompute, ProgramCost, ProgramError, ProgramRun}; diff --git a/crates/lance-graph-relalg/src/normalize.rs b/crates/lance-graph-relalg/src/normalize.rs index f7f7efcc9..f28d061d8 100644 --- a/crates/lance-graph-relalg/src/normalize.rs +++ b/crates/lance-graph-relalg/src/normalize.rs @@ -121,10 +121,31 @@ pub(crate) fn from_set(e: &SetExpr) -> Rel { } } +/// The relalg form of a contract [`SetExpr`]: the conversion [`crate::run_program`] +/// applies to every let and query. Public so a caller can lower one +/// description ONCE with [`crate::run_with_program`], keep the returned +/// mask-risc program, and execute it per question instead of re-lowering. +pub fn rel_from_set(e: &SetExpr) -> Rel { + from_set(e) +} + #[cfg(test)] mod tests { use super::*; + /// FAILS IF: the public conversion is not the inverse of `to_set`. + #[test] + fn rel_from_set_is_the_inverse_of_to_set() { + let rels = [ + Rel::And(vec![Rel::Plane(0), Rel::i32(1, Cmp::Ge, 5)]), + Rel::Or(vec![Rel::Plane(3), Rel::eq_u32(2, 7), Rel::ne_u32(1, 9)]), + Rel::Not(Box::new(Rel::eq_u32(2, 7))), + ]; + for r in rels { + assert_eq!(rel_from_set(&to_set(&r)), r); + } + } + /// FAILS IF: the conversion is lossy. Order of variants and fields is /// shared with the contract, so sorting agrees on both sides. #[test] From ba4779ccf8e9ce45d9f5d229ea0bb94daea09065 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 20:45:41 +0000 Subject: [PATCH 3/7] plan: matrix rows 5-6 reflect G6 (registered methods execute in the lab) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index 20fde263b..5e0d86dad 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -87,8 +87,8 @@ compared against Foundry. | 2 | Stable identity + provenance | DR route + witnessed coordinate; global id lane | `RouteAt`, `CoordSpace`, `Frame`; lab reorder test | LAB | No per-value provenance (who wrote this stock, from which system) | Two sources disagree on a value; no witness says which wins | PARTIAL → MISSING for provenance | | 3 | Link types / traversal (search-around) | Relation lanes; `graph_hop::OutgoingHop` | mask-RISC `graph_hop` is feature-gated OFF (value-directed gather banned, ADMISSION B) | BLOCKED | Admitted relation traversal over source-owned planes; recipe→ingredient is a fixture function here, not a bound relation | Bind recipe demand as a relation lane and traverse without Gather | BLOCKED | | 4 | Object sets, filtering (WHERE) | Scoped WHERE population = mask program | lab `cook_mask`, `fulfill_mask` | LAB | — | Parity suite (8 items × 3 q × 64 stores) | FUNCTIONALLY-RELATED; LOWER-LEVEL-ADVANTAGE-HYPOTHESIS (0 bytes copied, 470 ns / question at 64 rows) | -| 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; mask-RISC terminals | `lib.rs:215`, `:353`; DT64 "executes nothing" | PARTIAL | Executable lowering from a `MethodRef` to a mask-RISC program (the lab hand-writes the programs) | Register `CanCook` as a MethodBinding and execute it via `admit` | PARTIAL | -| 6 | Versioned method behaviour | `SigRev`, `GuardWitness`, `Stamp` | `lib.rs:345-370` | IMPLEMENTED (identity) / ABSENT (execution) | Same as 5 | Stale `SigRev` refused at execution | PARTIAL | +| 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; WHEN guard lowered by relalg to one mask-RISC program | `lib.rs:215`, `:353`; lab `method.rs` (§5b) | LAB (read-only guards) | Production owner of a prepared program; DO effects still not executed | `every_registered_can_cook_method_matches_the_oracle` | FUNCTIONALLY-RELATED (read-only) | +| 6 | Versioned method behaviour | `SigRev`, `GuardWitness`, `Stamp` checked by `admit` before execution | `lib.rs:345-370`; lab `method.rs` | IMPLEMENTED (identity) / LAB (execution) | Same as 5 | `a_reference_with_another_guard_is_refused` (forged guard, other `SigRev`), foreign store refused | FUNCTIONALLY-RELATED (read-only) | | 7 | Actions / state changes | none on this path | `MethodBinding::effects` is descriptive | ABSENT | Governed transition contract (§7 G4) | — | MISSING | | 8 | Multiple sources + sync | `LaneSource` per owner, `FrameStore` per source | `lane.rs` `source_owns`; lab uses one source | PARTIAL | Cross-source composition; G2L across differing spaces is refused, not translated | Two sources, different orders, one question | BLOCKED (G2L OPEN in the locality contract) | | 9 | Source ownership, logical materialization | One canonical owner; borrowed lanes | lab: arm B copies 0 bytes; arm A copies 51 968 | LAB | — | `only_demanded_fields_are_bound_and_borrowed_once` | LOWER-LEVEL-ADVANTAGE-HYPOTHESIS | From 8d5ab7a8f64d141df8984f1751748996951ed9ed Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 21:08:36 +0000 Subject: [PATCH 4/7] plan: correct G2-G4 / provenance after auditing auth, rbac, thought-git, xlog The first matrix marked authorization, scenarios, actions and provenance as having no contract without reading ogar-auth, ogar-rbac, lance-graph-rbac, thought-git-probe or lance-graph-xlog. The authorization decision is implemented (row scope + WideFieldMask via ScopedDecision); branches, a single write path with commit witnesses, receipts with replay and a two-phase edge write exist as probes. The gaps are restated as composition on this path. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 30 ++++++++++++++++++------------ 1 file changed, 18 insertions(+), 12 deletions(-) diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index 5e0d86dad..12c298188 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -89,18 +89,18 @@ compared against Foundry. | 4 | Object sets, filtering (WHERE) | Scoped WHERE population = mask program | lab `cook_mask`, `fulfill_mask` | LAB | — | Parity suite (8 items × 3 q × 64 stores) | FUNCTIONALLY-RELATED; LOWER-LEVEL-ADVANTAGE-HYPOTHESIS (0 bytes copied, 470 ns / question at 64 rows) | | 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; WHEN guard lowered by relalg to one mask-RISC program | `lib.rs:215`, `:353`; lab `method.rs` (§5b) | LAB (read-only guards) | Production owner of a prepared program; DO effects still not executed | `every_registered_can_cook_method_matches_the_oracle` | FUNCTIONALLY-RELATED (read-only) | | 6 | Versioned method behaviour | `SigRev`, `GuardWitness`, `Stamp` checked by `admit` before execution | `lib.rs:345-370`; lab `method.rs` | IMPLEMENTED (identity) / LAB (execution) | Same as 5 | `a_reference_with_another_guard_is_refused` (forged guard, other `SigRev`), foreign store refused | FUNCTIONALLY-RELATED (read-only) | -| 7 | Actions / state changes | none on this path | `MethodBinding::effects` is descriptive | ABSENT | Governed transition contract (§7 G4) | — | MISSING | +| 7 | Actions / state changes | thought-git write path; xlog two-phase edge writes; rbac write/act grants | `thought-git-probe` `Outcome::{Commit,Plan,Prune,Veto}`, `VersionStore::commit_cycle` (one sealed version + `CommitWitness` per cycle), `MetadataTable::stage`/`seal`; `lance-graph-xlog` `Cube::stage` (checks, no version) / `commit` (cannot refuse); `lance-graph-rbac` `Operation::{Write,Act}`, `PermissionSpec::can_write`/`can_act`; durable map writes in #1993 (open) | LAB (probe) / PROPOSED (`thought-git-lifecycle-contract-v1`: CONTRACT, docs only) | Not composed for this domain: no store-network action passes authorize(Write/Act) → stage → commit → witness; no precondition on a source value (only frame / sealed-version refusals) | Reassign order 12→17: authorized stage, stale-precondition refusal, commit, witness | PARTIAL (pieces exist, not composed) | | 8 | Multiple sources + sync | `LaneSource` per owner, `FrameStore` per source | `lane.rs` `source_owns`; lab uses one source | PARTIAL | Cross-source composition; G2L across differing spaces is refused, not translated | Two sources, different orders, one question | BLOCKED (G2L OPEN in the locality contract) | | 9 | Source ownership, logical materialization | One canonical owner; borrowed lanes | lab: arm B copies 0 bytes; arm A copies 51 968 | LAB | — | `only_demanded_fields_are_bound_and_borrowed_once` | LOWER-LEVEL-ADVANTAGE-HYPOTHESIS | -| 10 | Security / authorization | DR `Scope` (consistency only) + `lance-graph-rbac` (class/op grants) | `rbac/src/lib.rs`; lab stand-in `NeU32` | PARTIAL | Row-level authorization decided by IAM and applied in the read path; RBAC is not wired to DT64 | `bypassing_authorization_reveals_the_denied_store` | MISSING (production) | -| 11 | History / replay | `FrameStore` revisions; Lance versions | lab stale-frame refusal + rebind | LAB (invalidation) / UNKNOWN (replay at a past version through DT64) | Bind at a historical frame | Answer at frame N after the source moved to N+1 | PARTIAL | +| 10 | Security / authorization | `ogar-auth` `establish` → `VerifiedLogin` → `ogar-rbac` `authorize_user` / `authorize_identity` → `lance-graph-rbac` `ScopedDecision` / `MembershipDecision`: row scope (`ScopeSpec`: tenant + path, restrictive AND) and field projection (`WideFieldMask`, union; `visible_fields()` empty on refusal); delegation (`acting_party`); DT64 `Resolved::mask_where` over `PropertySpec::marking` | `lance-graph-rbac/src/authorize.rs:165-250`; `ogar-rbac/src/lib.rs:155,327`; `contract::selection::walk_rails_authorized` consumes the field mask | IMPLEMENTED (decision) / ABSENT (applied in a DT64 binding) | Apply the decision on this path: `ScopeSpec` needs a per-row scope lane and becomes a resident plane (Quack `Binder::live`); `visible_fields()` ∩ the marking mask restricts which fields `bind_lanes` may bind | Lab: replace the `NeU32` stand-in with an `authorize_scoped` decision; a narrowed role binds fewer fields and sees fewer stores | PARTIAL (decision built; read-path wiring missing) | +| 11 | History / replay | `FrameStore` revisions; Lance versions; thought-git receipts | lab stale-frame refusal + rebind; `thought-git-probe` `Receipt` + `replay` / `replay_landed` (recompute from a sealed base, refusing `SourceChanged` / `ConfigChanged` / `OutputMismatch`) | LAB (invalidation; replay in the probe) | Bind a DT64 lane at a historical frame | Answer at frame N after the source moved to N+1 | PARTIAL | | 12 | Derived state + invalidation | `LaneBinding::check` on every open | lab `a_stale_frame_is_refused_and_a_rebind_sees_the_restock` | LAB | Incremental recompute of only the changed subset (lab recomputes the whole question; it is 64 rows) | — | FUNCTIONALLY-RELATED | -| 13 | What-if scenarios (beta in Foundry docs) | `contract::scenario::ScenarioBranch` (facade) | `lance-graph-contract/src/scenario.rs` | PARTIAL; DR path BLOCKED | Overlay frame witness for DT64 bindings (§7 G3) | lab `the_scenario_is_oracle_only_and_lowers_capacity` (oracle only) | BLOCKED | +| 13 | What-if scenarios (beta in Foundry docs) | `contract::scenario::ScenarioBranch`; thought-git branches; xlog staged preview | `thought-git-probe` `SlotPool::branch` (from main or a live thought), `next_version` (from-scratch oracle recording contradictions and divergences), `squash_gate`; `lance-graph-xlog` `Cube::stage_closure` (the derived result as it would be after commit, changing nothing) | LAB (probe) | A branch as an overlay a DT64 binding reads (overlay frame witness, §7 G3) | Store 12 closed on a branch: answer = oracle, main's frame unchanged | PARTIAL | | 14 | Aggregations / analytics | mask-RISC `Count`, `MaskedSumI32`, group terminals; ndarray INT8 packed GEMM | lab `network_capacity`, `network_cost`; arm C `per_store` (per-store cost) | LAB | Per-row min / argmin across lanes (§7 G1) | Limiting resource through an admitted operator | PARTIAL | | 15 | Operational applications | a2ui-rs / consumer CustomObject | not exercised here | UNKNOWN | — | — | NOT-COMPARABLE here | -| 16 | Audit / decision provenance | Witnesses (route, frame, basis) per answer | `LaneBinding` fields | PARTIAL | Decision record: who asked, which witnesses, which answer | — | MISSING | +| 16 | Audit / decision provenance | Binding witnesses; thought-git receipts and commit witnesses; rbac identity | `LaneBinding` (route, frame, basis); `thought-git-probe` `Receipt` (base, program, inputs, seed, config, source fold, roots, output), `CommitWitness` (data version, cycle, cohort); `lance-graph-rbac` `ResolvedIdentity::auth_classid` (doc: "for the audit"), `acting_party` | PARTIAL (pieces in the probe and the rbac crate) | One record per answer joining who asked (identity, delegation), which binding witnesses and which result | — | PARTIAL | | 17 | Data connections / egress | Source adapters (OGAR, Lance) | outside this lab | UNKNOWN | — | — | NOT-COMPARABLE here | -| 18 | AI-assisted, governed decisions | none on this path | — | ABSENT | Depends on 7, 10, 16 | — | MISSING | +| 18 | AI-assisted, governed decisions | none on this path | — | ABSENT | Depends on 7, 10, 16 being composed | — | MISSING | Correspondence hypotheses (§4 of the brief), graded: `ClassView` ↔ object type: FUNCTIONALLY-RELATED, but ClassView alone carries no security, search, @@ -253,9 +253,9 @@ methods and costs ~48 µs (was ~25 µs with none); not separated further. | Id | Missing operation | Why the current contract cannot express it | Lawful alternative today | Smallest test | Needs | |---|---|---|---|---|---| | G1 | Element-wise cross-lane arithmetic: `min_k ⌊stock_k / d_k⌋` per row, argmin (limiting resource). (Per-row weighted sum — per-store cost — is now LAB via arm C, §5a.) | mask-RISC terminals reduce over rows; predicates compare a lane to a constant; min/argmin is not a matrix product | Layer-cake over monotone masks (max only, ~30× programs); none for argmin | Per-store max and limiting resource in one program, equal to oracle | Decision + mask-RISC/Quack PR (H2) | -| G2 | Row-level authorization from IAM in the read path | DR `Scope` is per lane and consistency-only; RBAC grants are class/op, not wired to DT64 | Lab stand-in predicate on the identity lane | Same lab tests with the predicate supplied by `lance-graph-rbac` | Decision on where IAM evaluates (H3) | -| G3 | Scenario overlay over a binding | No frame witness for a proposed, non-canonical plane | Oracle only | Store 12 closed: overlay answer = oracle, canonical frame unchanged | Overlay frame contract (H3) | -| G4 | Governed action / writeback | No command identity, preconditions, idempotency, atomic commit or audit on this path; `MethodBinding::effects` is descriptive | none | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Separate gate; not in a read-only lab | +| G2 | Row-level authorization from IAM in the read path | The decision exists (`ogar-rbac` → `lance-graph-rbac::ScopedDecision`: row `ScopeSpec` + `WideFieldMask`); nothing applies it to a DT64 binding, and the lab has no per-row scope lane | Lab stand-in predicate on the identity lane | Lab: `authorize_scoped` decision as a resident plane plus `visible_fields()` limiting bound fields | A per-row scope lane on the source; where the decision is applied (Quack `Binder::live` is the existing seam) | +| G3 | Scenario overlay over a binding | Branches exist in the thought-git probe (`SlotPool::branch`, `next_version`) and as xlog staged previews; no frame witness lets a DT64 binding read a branch | Oracle only | Store 12 closed on a branch: overlay answer = oracle, canonical frame unchanged | Overlay frame contract joining a thought-git branch to `FrameStore` | +| G4 | Governed action / writeback | Pieces exist: thought-git Rubicon outcomes, `commit_cycle` (one write path, `CommitWitness`, `AlreadySealed` / `DuplicateThought` refusals), `MetadataTable::stage`/`seal`; xlog `Cube::stage`/`commit`; rbac `Operation::{Write,Act}`. Not composed: no action over this domain is authorized, staged, checked against a source-value precondition, committed and witnessed | none in this lab | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Composition over the existing pieces; `thought-git-lifecycle-contract-v1` (CONTRACT) is the contract | | G5 | Bound relations (recipe → ingredient, menu → recipe) | Value-directed traversal is Gather, banned outside ADMISSION B | Relations as fixture functions (lab) | Bind recipe demand as lanes and answer without Gather | ADMISSION B decision | | G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing. LAB since §5b: admitted, bound, lowered once by relalg, executed per question at arm B's cost | — | Done in the lab: oracle parity, refusals, 359–400 ns per question | Production: who holds the prepared program across questions (no owner named) | @@ -268,9 +268,15 @@ methods and costs ~48 µs (was ~25 µs with none); not separated further. - **H2 (missing algebra):** *supported by G1, G5, narrowed by arm C.* The per-store cost IS expressible, as an INT8 GEMM over staged A (§5a). The limiting resource still cannot be expressed; the maximum only by a sweep. -- **H3 (infrastructure):** *supported by G2, G3, G4, G6* but untested in - depth here: authorization, scenarios, actions and method execution all lack - a contract on this path. +- **H3 (infrastructure):** *narrowed (2026-11-10 audit).* The first matrix + said authorization, scenarios and actions had no contract; that was written + without reading `ogar-auth`, `ogar-rbac`, `lance-graph-rbac`, + `thought-git-probe` or `lance-graph-xlog`. They exist: the authorization + decision is implemented (row scope + field mask), and branches, a single + write path with commit witnesses, receipts with replay and a two-phase edge + write exist as probes. What is missing is COMPOSITION on this path: + applying the decision to a DT64 binding (G2), letting a binding read a + branch (G3), and one governed action end to end (G4). None is chosen over the others; all three hold in part. From 5ff998401940f16f795ee3f7205d8540b599b9d5 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 21:10:22 +0000 Subject: [PATCH 5/7] plan: current Foundry parity report (section 0) and status line Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 37 +++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index 12c298188..951ae1c3d 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -1,6 +1,7 @@ # D-FOUNDRY-PARITY-1 — DR × DT64 as an operational ontology: evidence matrix and first lab -> **Status:** ACTIVE (lab slice landed in this PR; everything past Level R is OPEN). +> **Status:** ACTIVE. Level R lab merged (#1991, #1995); G6 in #1996. Governance +> (G2–G4) is composition work over existing pieces (§0, corrected 2026-11-10). > **Lab:** `crates/foundry-parity-lab` (own workspace root, not a member). > **Contract read first:** `.claude/knowledge/dr-dt64-locality-execution-contract.md` > (its own evidence table grades Foundry parity HYPOTHESIS; this plan does not @@ -8,6 +9,40 @@ > **Verify:** `cargo test --release --manifest-path crates/foundry-parity-lab/Cargo.toml` > and `cargo run --release --manifest-path crates/foundry-parity-lab/Cargo.toml --bin bench`. +## 0. Report (current, 2026-11-10) + +**Verdict.** No Foundry parity is claimed; nothing was compared against a +running Foundry. On the read side, DR + DT64 + mask-RISC answer operational +questions over source-owned planes with exact oracle parity, correct +refusals and zero copies. On the governance side, the parts exist in other +crates but are not composed on this path. + +**What the lab shows (32 tests, every guard disable-verified):** + +| Question | Path | Measured (64 rows) | +|---|---|---| +| `CanCook` | arm B, hand-written mask-RISC | 470 ns, 0 B copied | +| `CanCook` as a registered method | G6: `admit` → bind → relalg lowered once → execute | 359–400 ns | +| per-store cost, 64 × 8 | arm C, INT8 packed GEMM (AMX) | 0.65–1.17 µs | +| per-store maximum | arm B layer-cake sweep | ~15–19 µs (8× slower than objects: no min/argmin) | +| same over objects | arm A | ~1.8 µs + 21 µs and 51 968 B to build | + +**What exists elsewhere and what is missing (audited 2026-11-10):** + +| Area | Exists | Missing on this path | +|---|---|---| +| Authorization (G2) | `ogar-auth` → `ogar-rbac` → `lance-graph-rbac::ScopedDecision`: row `ScopeSpec` + `WideFieldMask`, delegation; DT64 `mask_where` over markings | Apply it to a DT64 binding: per-row scope lane → resident plane; `visible_fields()` limits bound fields | +| Scenarios (G3) | thought-git branches, `next_version`, squash gate; xlog `stage_closure` preview | An overlay frame a DT64 binding can read | +| Actions / writeback (G4) | thought-git Rubicon outcomes, `commit_cycle` + `CommitWitness`, `stage`/`seal`; xlog `stage`/`commit`; rbac Write/Act; #1993 durable map writes | One authorized, preconditioned, committed, witnessed action end to end | +| Provenance | binding witnesses, thought-git receipts + replay, commit witnesses, rbac audit identity | One record per answer joining them | +| Algebra (G1) | counts, sums, GEMM | element-wise min/argmin (decision P1b) | +| Relations (G5) | — | ADMISSION B decision (EXO-140) | + +**Next step with the most value:** G2 in the lab, using the existing +`authorize_scoped` decision instead of the stand-in. + +Architecture maps: `.mermaid/` (D-FOUNDRY-MAP-1). + ## 1. Overview The question is not "can we clone Foundry". It is: can source-owned SoA planes, From 92bb6a8549d0e228e310c5d0862efdc3032ca49f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 21:13:01 +0000 Subject: [PATCH 6/7] plan: r2il binding executes DO effects (ExecPermit, Receipt); G6 row corrected Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index 951ae1c3d..dc20f5f80 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -122,7 +122,7 @@ compared against Foundry. | 2 | Stable identity + provenance | DR route + witnessed coordinate; global id lane | `RouteAt`, `CoordSpace`, `Frame`; lab reorder test | LAB | No per-value provenance (who wrote this stock, from which system) | Two sources disagree on a value; no witness says which wins | PARTIAL → MISSING for provenance | | 3 | Link types / traversal (search-around) | Relation lanes; `graph_hop::OutgoingHop` | mask-RISC `graph_hop` is feature-gated OFF (value-directed gather banned, ADMISSION B) | BLOCKED | Admitted relation traversal over source-owned planes; recipe→ingredient is a fixture function here, not a bound relation | Bind recipe demand as a relation lane and traverse without Gather | BLOCKED | | 4 | Object sets, filtering (WHERE) | Scoped WHERE population = mask program | lab `cook_mask`, `fulfill_mask` | LAB | — | Parity suite (8 items × 3 q × 64 stores) | FUNCTIONALLY-RELATED; LOWER-LEVEL-ADVANTAGE-HYPOTHESIS (0 bytes copied, 470 ns / question at 64 rows) | -| 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; WHEN guard lowered by relalg to one mask-RISC program | `lib.rs:215`, `:353`; lab `method.rs` (§5b) | LAB (read-only guards) | Production owner of a prepared program; DO effects still not executed | `every_registered_can_cook_method_matches_the_oracle` | FUNCTIONALLY-RELATED (read-only) | +| 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; WHEN guard lowered by relalg to one mask-RISC program | `lib.rs:215`, `:353`; lab `method.rs` (§5b, WHEN guards); `lance-graph-r2il` `binding::prepare`/`run` and `binding_native::prepare_native`/`run_native` (DO effects: admitted, lowered once, compiled programs run hot, explicit `ExecPermit`, bounded `Receipt`; WHEN refused there) | LAB (both halves, separately) | One executor for WHEN and DO; who issues `ExecPermit` ("not decided", `binding.rs`) | `every_registered_can_cook_method_matches_the_oracle`; r2il binding tests | FUNCTIONALLY-RELATED | | 6 | Versioned method behaviour | `SigRev`, `GuardWitness`, `Stamp` checked by `admit` before execution | `lib.rs:345-370`; lab `method.rs` | IMPLEMENTED (identity) / LAB (execution) | Same as 5 | `a_reference_with_another_guard_is_refused` (forged guard, other `SigRev`), foreign store refused | FUNCTIONALLY-RELATED (read-only) | | 7 | Actions / state changes | thought-git write path; xlog two-phase edge writes; rbac write/act grants | `thought-git-probe` `Outcome::{Commit,Plan,Prune,Veto}`, `VersionStore::commit_cycle` (one sealed version + `CommitWitness` per cycle), `MetadataTable::stage`/`seal`; `lance-graph-xlog` `Cube::stage` (checks, no version) / `commit` (cannot refuse); `lance-graph-rbac` `Operation::{Write,Act}`, `PermissionSpec::can_write`/`can_act`; durable map writes in #1993 (open) | LAB (probe) / PROPOSED (`thought-git-lifecycle-contract-v1`: CONTRACT, docs only) | Not composed for this domain: no store-network action passes authorize(Write/Act) → stage → commit → witness; no precondition on a source value (only frame / sealed-version refusals) | Reassign order 12→17: authorized stage, stale-precondition refusal, commit, witness | PARTIAL (pieces exist, not composed) | | 8 | Multiple sources + sync | `LaneSource` per owner, `FrameStore` per source | `lane.rs` `source_owns`; lab uses one source | PARTIAL | Cross-source composition; G2L across differing spaces is refused, not translated | Two sources, different orders, one question | BLOCKED (G2L OPEN in the locality contract) | @@ -292,7 +292,7 @@ methods and costs ~48 µs (was ~25 µs with none); not separated further. | G3 | Scenario overlay over a binding | Branches exist in the thought-git probe (`SlotPool::branch`, `next_version`) and as xlog staged previews; no frame witness lets a DT64 binding read a branch | Oracle only | Store 12 closed on a branch: overlay answer = oracle, canonical frame unchanged | Overlay frame contract joining a thought-git branch to `FrameStore` | | G4 | Governed action / writeback | Pieces exist: thought-git Rubicon outcomes, `commit_cycle` (one write path, `CommitWitness`, `AlreadySealed` / `DuplicateThought` refusals), `MetadataTable::stage`/`seal`; xlog `Cube::stage`/`commit`; rbac `Operation::{Write,Act}`. Not composed: no action over this domain is authorized, staged, checked against a source-value precondition, committed and witnessed | none in this lab | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Composition over the existing pieces; `thought-git-lifecycle-contract-v1` (CONTRACT) is the contract | | G5 | Bound relations (recipe → ingredient, menu → recipe) | Value-directed traversal is Gather, banned outside ADMISSION B | Relations as fixture functions (lab) | Bind recipe demand as lanes and answer without Gather | ADMISSION B decision | -| G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing. LAB since §5b: admitted, bound, lowered once by relalg, executed per question at arm B's cost | — | Done in the lab: oracle parity, refusals, 359–400 ns per question | Production: who holds the prepared program across questions (no owner named) | +| G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing. LAB since §5b: admitted, bound, lowered once by relalg, executed per question at arm B's cost | — | Done in the lab for WHEN guards; `lance-graph-r2il::binding_native` already does the same for DO effects (prior art the first G6 pass missed) | Production: who holds a prepared program, and who issues `ExecPermit` (the natural issuer is an `lance-graph-rbac` `Operation::Act` decision) | ## 8. The three hypotheses From 7a944aacbea7391e3378652dab7c1d05890967e5 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 10 Nov 2026 21:25:33 +0000 Subject: [PATCH 7/7] plan(foundry-parity): correct auth routes, name the shipped cycle writer, #1993 merged Mapping for #1997 found three errors. authorize_identity reaches authorize_memberships (MembershipDecision), not authorize_scoped. The production LanceCycleWriter (WalSink::commit_cycle) is on main beside the probe's stand-in, so G4 composes shipped pieces. #1993 merged as b34d195. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01XAqKMPJjVvasjwqhjJ6c9p --- .claude/plans/foundry-parity-v1.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.claude/plans/foundry-parity-v1.md b/.claude/plans/foundry-parity-v1.md index dc20f5f80..a3cbcdf70 100644 --- a/.claude/plans/foundry-parity-v1.md +++ b/.claude/plans/foundry-parity-v1.md @@ -124,10 +124,10 @@ compared against Foundry. | 4 | Object sets, filtering (WHERE) | Scoped WHERE population = mask program | lab `cook_mask`, `fulfill_mask` | LAB | — | Parity suite (8 items × 3 q × 64 stores) | FUNCTIONALLY-RELATED; LOWER-LEVEL-ADVANTAGE-HYPOTHESIS (0 bytes copied, 470 ns / question at 64 rows) | | 5 | Computed properties / functions | `MethodBinding` (ON×WHEN×DO) + `MethodRef`; WHEN guard lowered by relalg to one mask-RISC program | `lib.rs:215`, `:353`; lab `method.rs` (§5b, WHEN guards); `lance-graph-r2il` `binding::prepare`/`run` and `binding_native::prepare_native`/`run_native` (DO effects: admitted, lowered once, compiled programs run hot, explicit `ExecPermit`, bounded `Receipt`; WHEN refused there) | LAB (both halves, separately) | One executor for WHEN and DO; who issues `ExecPermit` ("not decided", `binding.rs`) | `every_registered_can_cook_method_matches_the_oracle`; r2il binding tests | FUNCTIONALLY-RELATED | | 6 | Versioned method behaviour | `SigRev`, `GuardWitness`, `Stamp` checked by `admit` before execution | `lib.rs:345-370`; lab `method.rs` | IMPLEMENTED (identity) / LAB (execution) | Same as 5 | `a_reference_with_another_guard_is_refused` (forged guard, other `SigRev`), foreign store refused | FUNCTIONALLY-RELATED (read-only) | -| 7 | Actions / state changes | thought-git write path; xlog two-phase edge writes; rbac write/act grants | `thought-git-probe` `Outcome::{Commit,Plan,Prune,Veto}`, `VersionStore::commit_cycle` (one sealed version + `CommitWitness` per cycle), `MetadataTable::stage`/`seal`; `lance-graph-xlog` `Cube::stage` (checks, no version) / `commit` (cannot refuse); `lance-graph-rbac` `Operation::{Write,Act}`, `PermissionSpec::can_write`/`can_act`; durable map writes in #1993 (open) | LAB (probe) / PROPOSED (`thought-git-lifecycle-contract-v1`: CONTRACT, docs only) | Not composed for this domain: no store-network action passes authorize(Write/Act) → stage → commit → witness; no precondition on a source value (only frame / sealed-version refusals) | Reassign order 12→17: authorized stage, stale-precondition refusal, commit, witness | PARTIAL (pieces exist, not composed) | +| 7 | Actions / state changes | thought-git write path; xlog two-phase edge writes; rbac write/act grants | `thought-git-probe` `Outcome::{Commit,Plan,Prune,Veto}`, `VersionStore::commit_cycle` (one sealed version + `CommitWitness` per cycle), `MetadataTable::stage`/`seal`; `lance-graph-xlog` `Cube::stage` (checks, no version) / `commit` (cannot refuse); `lance-graph-rbac` `Operation::{Write,Act}`, `PermissionSpec::can_write`/`can_act`; durable map writes in #1993 (merged, `b34d195`); the production cycle writer `WalSink::commit_cycle` (`lance-graph-planner/src/persist_sink.rs:551`), implemented by `LanceCycleWriter` (`lance-graph/src/graph/cycle_sink.rs:1050`), on main beside the probe's `VersionStore` stand-in | LAB (probe) / PROPOSED (`thought-git-lifecycle-contract-v1`: CONTRACT, docs only) | Not composed for this domain: no store-network action passes authorize(Write/Act) → stage → commit → witness; no precondition on a source value (only frame / sealed-version refusals) | Reassign order 12→17: authorized stage, stale-precondition refusal, commit, witness | PARTIAL (pieces exist, not composed) | | 8 | Multiple sources + sync | `LaneSource` per owner, `FrameStore` per source | `lane.rs` `source_owns`; lab uses one source | PARTIAL | Cross-source composition; G2L across differing spaces is refused, not translated | Two sources, different orders, one question | BLOCKED (G2L OPEN in the locality contract) | | 9 | Source ownership, logical materialization | One canonical owner; borrowed lanes | lab: arm B copies 0 bytes; arm A copies 51 968 | LAB | — | `only_demanded_fields_are_bound_and_borrowed_once` | LOWER-LEVEL-ADVANTAGE-HYPOTHESIS | -| 10 | Security / authorization | `ogar-auth` `establish` → `VerifiedLogin` → `ogar-rbac` `authorize_user` / `authorize_identity` → `lance-graph-rbac` `ScopedDecision` / `MembershipDecision`: row scope (`ScopeSpec`: tenant + path, restrictive AND) and field projection (`WideFieldMask`, union; `visible_fields()` empty on refusal); delegation (`acting_party`); DT64 `Resolved::mask_where` over `PropertySpec::marking` | `lance-graph-rbac/src/authorize.rs:165-250`; `ogar-rbac/src/lib.rs:155,327`; `contract::selection::walk_rails_authorized` consumes the field mask | IMPLEMENTED (decision) / ABSENT (applied in a DT64 binding) | Apply the decision on this path: `ScopeSpec` needs a per-row scope lane and becomes a resident plane (Quack `Binder::live`); `visible_fields()` ∩ the marking mask restricts which fields `bind_lanes` may bind | Lab: replace the `NeU32` stand-in with an `authorize_scoped` decision; a narrowed role binds fewer fields and sees fewer stores | PARTIAL (decision built; read-path wiring missing) | +| 10 | Security / authorization | `ogar-auth` `establish` → `VerifiedLogin` → `ogar-rbac` `authorize_user` → `lance-graph-rbac` `authorize_scoped` → `ScopedDecision`, or `authorize_identity` → `authorize_memberships` → `MembershipDecision` (two routes; only the first carries `ScopeSpec` + `WideFieldMask`): row scope (`ScopeSpec`: tenant + path, restrictive AND) and field projection (`WideFieldMask`, union; `visible_fields()` empty on refusal); delegation (`acting_party`); DT64 `Resolved::mask_where` over `PropertySpec::marking` | `lance-graph-rbac/src/authorize.rs:165-250`; `ogar-rbac/src/lib.rs:155,327`; `contract::selection::walk_rails_authorized` consumes the field mask | IMPLEMENTED (decision) / ABSENT (applied in a DT64 binding) | Apply the decision on this path: `ScopeSpec` needs a per-row scope lane and becomes a resident plane (Quack `Binder::live`); `visible_fields()` ∩ the marking mask restricts which fields `bind_lanes` may bind | Lab: replace the `NeU32` stand-in with an `authorize_scoped` decision; a narrowed role binds fewer fields and sees fewer stores | PARTIAL (decision built; read-path wiring missing) | | 11 | History / replay | `FrameStore` revisions; Lance versions; thought-git receipts | lab stale-frame refusal + rebind; `thought-git-probe` `Receipt` + `replay` / `replay_landed` (recompute from a sealed base, refusing `SourceChanged` / `ConfigChanged` / `OutputMismatch`) | LAB (invalidation; replay in the probe) | Bind a DT64 lane at a historical frame | Answer at frame N after the source moved to N+1 | PARTIAL | | 12 | Derived state + invalidation | `LaneBinding::check` on every open | lab `a_stale_frame_is_refused_and_a_rebind_sees_the_restock` | LAB | Incremental recompute of only the changed subset (lab recomputes the whole question; it is 64 rows) | — | FUNCTIONALLY-RELATED | | 13 | What-if scenarios (beta in Foundry docs) | `contract::scenario::ScenarioBranch`; thought-git branches; xlog staged preview | `thought-git-probe` `SlotPool::branch` (from main or a live thought), `next_version` (from-scratch oracle recording contradictions and divergences), `squash_gate`; `lance-graph-xlog` `Cube::stage_closure` (the derived result as it would be after commit, changing nothing) | LAB (probe) | A branch as an overlay a DT64 binding reads (overlay frame witness, §7 G3) | Store 12 closed on a branch: answer = oracle, main's frame unchanged | PARTIAL | @@ -290,7 +290,7 @@ methods and costs ~48 µs (was ~25 µs with none); not separated further. | G1 | Element-wise cross-lane arithmetic: `min_k ⌊stock_k / d_k⌋` per row, argmin (limiting resource). (Per-row weighted sum — per-store cost — is now LAB via arm C, §5a.) | mask-RISC terminals reduce over rows; predicates compare a lane to a constant; min/argmin is not a matrix product | Layer-cake over monotone masks (max only, ~30× programs); none for argmin | Per-store max and limiting resource in one program, equal to oracle | Decision + mask-RISC/Quack PR (H2) | | G2 | Row-level authorization from IAM in the read path | The decision exists (`ogar-rbac` → `lance-graph-rbac::ScopedDecision`: row `ScopeSpec` + `WideFieldMask`); nothing applies it to a DT64 binding, and the lab has no per-row scope lane | Lab stand-in predicate on the identity lane | Lab: `authorize_scoped` decision as a resident plane plus `visible_fields()` limiting bound fields | A per-row scope lane on the source; where the decision is applied (Quack `Binder::live` is the existing seam) | | G3 | Scenario overlay over a binding | Branches exist in the thought-git probe (`SlotPool::branch`, `next_version`) and as xlog staged previews; no frame witness lets a DT64 binding read a branch | Oracle only | Store 12 closed on a branch: overlay answer = oracle, canonical frame unchanged | Overlay frame contract joining a thought-git branch to `FrameStore` | -| G4 | Governed action / writeback | Pieces exist: thought-git Rubicon outcomes, `commit_cycle` (one write path, `CommitWitness`, `AlreadySealed` / `DuplicateThought` refusals), `MetadataTable::stage`/`seal`; xlog `Cube::stage`/`commit`; rbac `Operation::{Write,Act}`. Not composed: no action over this domain is authorized, staged, checked against a source-value precondition, committed and witnessed | none in this lab | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Composition over the existing pieces; `thought-git-lifecycle-contract-v1` (CONTRACT) is the contract | +| G4 | Governed action / writeback | Pieces exist: the shipped `LanceCycleWriter` (`WalSink::commit_cycle`, refusals `Fenced` / `HashConflict` / …); thought-git Rubicon outcomes, the probe's `commit_cycle` stand-in (one write path, `CommitWitness`, `AlreadySealed` / `DuplicateThought` refusals), `MetadataTable::stage`/`seal`; xlog `Cube::stage`/`commit`; rbac `Operation::{Write,Act}`. Not composed: no action over this domain is authorized, staged, checked against a source-value precondition, committed and witnessed | none in this lab | Preview vs commit of "reassign order 12→17" with a stale-precondition refusal | Composition over the existing pieces; `thought-git-lifecycle-contract-v1` (CONTRACT) is the contract | | G5 | Bound relations (recipe → ingredient, menu → recipe) | Value-directed traversal is Gather, banned outside ADMISSION B | Relations as fixture functions (lab) | Bind recipe demand as lanes and answer without Gather | ADMISSION B decision | | G6 | Methods executed from `MethodRef` | DT64 binds behaviour, executes nothing. LAB since §5b: admitted, bound, lowered once by relalg, executed per question at arm B's cost | — | Done in the lab for WHEN guards; `lance-graph-r2il::binding_native` already does the same for DO effects (prior art the first G6 pass missed) | Production: who holds a prepared program, and who issues `ExecPermit` (the natural issuer is an `lance-graph-rbac` `Operation::Act` decision) |