From 9b2520f79f4de8e18042c0d5e8c4a88317e0419a Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:39:39 +0000 Subject: [PATCH 1/3] D-SAG-6-W0/W1: dogfood workbench amendment + read-only lab fixture W0 (docs): amends D-SAG-6 (#1760) with a project-graph projection beside D-SAG-6-2: reuse matrix, data contract, falsifier results, debt/EXO-50 references, open prerequisites; W2-W4 plan for a read-only MCP surface, a /board view over the same handler table, and an isolated Railway service (deployment not authorized). W1 (lab): crates/sag6-workbench-probe, own [workspace], excluded from the root. 19 real records read 2026-10-27 (Linear EXO-111/112/140/148/50 relations; the source lines they name pinned at aa569bc; their ISSUES.md rows; cited PRs; one session id; one inferred edge graded Hypothesis). One-hop queries run through Quack lower + mask-risc execute_into; frame staleness reuses dr-math-binding-probe FrameStore; multi-hop is refused (EXO-140, ISS-GATHER-HOP-1616); no OGAR classid is bound. cargo test: 15 passed. Eight disable runs each turned the named test red. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01XAqKMLnsLW2mFBBbEAT6Ch --- .claude/board/INTEGRATION_PLANS.md | 5 + .claude/board/STATUS_BOARD.md | 5 + .../2026-10-27-d-sag-6-w-dogfood-workbench.md | 15 + .claude/board/entries/README.md | 3 +- .../d-sag-6-w-dogfood-mcp-workbench-v1.md | 171 +++++ .../plans/d-sag-6-w-mcp-board-railway-v1.md | 190 +++++ Cargo.toml | 3 + crates/sag6-workbench-probe/Cargo.toml | 26 + crates/sag6-workbench-probe/src/fixture.rs | 278 +++++++ crates/sag6-workbench-probe/src/lib.rs | 683 ++++++++++++++++++ .../sag6-workbench-probe/tests/falsifiers.rs | 412 +++++++++++ 11 files changed, 1790 insertions(+), 1 deletion(-) create mode 100644 .claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md create mode 100644 .claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md create mode 100644 .claude/plans/d-sag-6-w-mcp-board-railway-v1.md create mode 100644 crates/sag6-workbench-probe/Cargo.toml create mode 100644 crates/sag6-workbench-probe/src/fixture.rs create mode 100644 crates/sag6-workbench-probe/src/lib.rs create mode 100644 crates/sag6-workbench-probe/tests/falsifiers.rs diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index f25d2512a..4e3fedc41 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,3 +1,8 @@ +## 2026-10-27 — D-SAG-6-W: dogfood MCP workbench → `.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md` (+ `d-sag-6-w-mcp-board-railway-v1.md`) + +**Status:** W0 PROPOSAL docs; W1 LAB fixture `crates/sag6-workbench-probe` (15/15 tests, 8/8 disables red); W2-W3 PROPOSED; W4 deployment NOT AUTHORIZED. Amends D-SAG-6 (#1760) with a project-graph projection beside D-SAG-6-2. **Board:** [entry](entries/2026-10-27-d-sag-6-w-dogfood-workbench.md), [STATUS_BOARD](STATUS_BOARD.md) D-SAG-6-W0..W4. One-hop runs on Quack + mask-risc; multi-hop refused (EXO-140, ISS-GATHER-HOP-1616); no OGAR classid bound (no GitHub/Linear port). +**Confidence:** LAB on a 19-record real slice; no timing; nothing beyond the slice claimed. + ## 2026-10-26 — D-TFLP v2: synergy revision → `.claude/plans/d-tflp-tflite-palette-polyfill-capstone-v2.md` **Status:** PROPOSAL, docs only; revises v1 (#1785). **Board:** [entry](entries/2026-10-26-d-tflp-v2-synergy-revision.md), [STATUS_BOARD](STATUS_BOARD.md) D-TFLP. Folds GPT's six #1785 corrections; rescopes D-TFLP-4 to the source reciprocal from #1800; splits prepared-object identity into numeric cache key + semantic receipt from #1800/#1801; adds D-TFLP-5a (intake bake-off, #1802 pattern); records boundaries with DT64-5 and DR256/DQM. diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index 25053e566..d2551731b 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -117,6 +117,11 @@ | **D-SAG-6-3** | Datalog/Ascent candidates versus Datafrog/independent Rust oracle | PROPOSED; separate approval | pure filter/count vs impure-closure/panic/Bag/K3 controls | | **D-SAG-6-4** | egglog guarded law + effect-aware extraction + proof/replay traceroute | PROPOSED; separate approval | independent checker gap explicit; no effect reorder or forged proof promotion | | **D-SAG-6-5** | optional approved Rust source edit and comparative MLIR lowering | PROPOSED; separate approval | rustc/tests/differential target parity; FMA/NaN/signed-zero and effect gates | +| **D-SAG-6-W0** | dogfood workbench amendment: project-graph projection beside D-SAG-6-2, reuse matrix, MCP/board/Railway plan ([plan](../plans/d-sag-6-w-dogfood-mcp-workbench-v1.md), [W2-W4](../plans/d-sag-6-w-mcp-board-railway-v1.md)) | DOCS / PROPOSAL | no deployment, no mint, no DT64/DR64³ runtime | +| **D-SAG-6-W1** | `crates/sag6-workbench-probe`: real Linear/GitHub/debt-row slice, one-hop queries via Quack `lower` + mask-risc `execute_into`, `FrameStore` reused, multi-hop and method binding refused | LAB, 15/15 tests, 8/8 disables red (2026-10-27) | F01/F04/F06/F07/F10/F11/F13/F14/F15 + W-cache + W-replay | +| **D-SAG-6-W2** | read-only MCP surface (rmcp streamable HTTP), seven tools over W1 functions | PROPOSED; separate approval | no write tool; opaque frame handles; NOT_HELD only under complete coverage | +| **D-SAG-6-W3** | `/board` server-rendered views over the same handler table | PROPOSED; separate approval | no frontend business logic | +| **D-SAG-6-W4** | isolated Railway service + read-only sync job | NOT AUTHORIZED | domain (`mcp.exo.red` is `adarail-production`), ownership, read-only tokens: operator | ## D-ONNX-NATIVE — ONNX vocabulary over existing native functions (2026-10-23) diff --git a/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md b/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md new file mode 100644 index 000000000..5a044d9fc --- /dev/null +++ b/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md @@ -0,0 +1,15 @@ +# D-SAG-6-W — dogfood MCP workbench: read-only project graph over Quack + +**Date:** 2026-10-27. **Status:** W0 docs + W1 LAB (`crates/sag6-workbench-probe`, own `[workspace]`, excluded from root); W2–W3 PROPOSED; W4 deployment NOT AUTHORIZED. **Source:** [`d-sag-6-w-dogfood-mcp-workbench-v1.md`](../../plans/d-sag-6-w-dogfood-mcp-workbench-v1.md), [`d-sag-6-w-mcp-board-railway-v1.md`](../../plans/d-sag-6-w-mcp-board-railway-v1.md). Parent: D-SAG-6 (#1760). + +**Measured (W1):** `cd crates/sag6-workbench-probe && cargo test` → 15 passed. Eight disable runs (coverage, frame check, symbol revision, inverse column, chain refusal, grade laundering, method binding) each turned the named test red; tree clean after restore. The Quack + mask-risc path equals a `GlobalId`-keyed scalar oracle for every identity × predicate × direction of the fixture; `blocked_by` equals Linear's own `blockedBy` lists, and only the two `blocks` rows are stored. + +**Fixture:** 19 real records read 2026-10-27 — Linear EXO-111/112/140/148/50 relations, the source lines the issues name pinned at lance-graph `aa569bc` (`mul.rs:1086`, quack `lib.rs:387`, `rmap.rs:70`), their `ISSUES.md` rows (:74, :176), cited PRs #1640/#1730/#1732, one recorded session id, and one inferred edge (`graph_hop.rs:55`) graded `Hypothesis`. + +**Found while building it:** +- One-hop project-graph questions are an edge table under Quack's existing `Filter::and[EqU32, EqU32]` — no DR64², DR64³ or DT64 code is needed for W1, and none exists (DT64: 0 code files). +- Multi-hop has no admitted path on two independent grounds: `Filter::Semijoin` unclassified under ADMISSION B (EXO-140) and `OutgoingHop` quarantined (ISS-GATHER-HOP-1616). The workbench refuses it instead of emulating it. +- OGAR already has `PROJECT_WORK_ITEM` / `PROJECT_RELATION` / `PROJECT_REPOSITORY` / `PROJECT_CHANGESET` (Redmine/OpenProject ports); there is no GitHub or Linear port and no PullRequest or SourceSymbol concept, so nothing is bound. +- `mcp.exo.red` is the live `adarail-production` service (write tools, write-scoped secrets); the workbench must be a separate service on a separate host name. + +**OPEN:** OGAR port/concepts (OGAR owner); ADMISSION B (EXO-140, operator); DurableRef home (EXO-148, D-RST-1); domain, Railway ownership, read-only tokens, Redis yes/no (operator). diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 96134545d..1c9eec868 100644 --- a/.claude/board/entries/README.md +++ b/.claude/board/entries/README.md @@ -25,10 +25,11 @@ 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. -487 entries, 2026-08-06 .. 2026-10-26. +488 entries, 2026-08-06 .. 2026-10-27. | date | entry id | finding | file | |---|---|---|---| +| 2026-10-27 | `D-SAG-6-W` | | [2026-10-27-d-sag-6-w-dogfood-workbench.md](2026-10-27-d-sag-6-w-dogfood-workbench.md) | | 2026-10-26 | `D-ONNX-INTAKE-0` | | [2026-10-26-onnx-frontend-intake-bakeoff.md](2026-10-26-onnx-frontend-intake-bakeoff.md) | | 2026-10-26 | `D-DT64-0` | | [2026-10-26-dt64-holographic-interface.md](2026-10-26-dt64-holographic-interface.md) | | 2026-10-26 | `D-DR64C-A` | | [2026-10-26-dr64-cubed-amendment.md](2026-10-26-dr64-cubed-amendment.md) | diff --git a/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md new file mode 100644 index 000000000..7c224379b --- /dev/null +++ b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md @@ -0,0 +1,171 @@ +# D-SAG-6-W — Dogfood MCP workbench: a read-only project-graph projection + +**Date:** 2026-10-27. **Status:** PROPOSAL + LAB FIXTURE (`crates/sag6-workbench-probe`, read-only, own `[workspace]`, excluded from the root workspace). **Implementation:** W1 lab only; deployment NOT authorized. No production Rust in the root workspace, no ABI, no policy, no storage, no CI and no Railway change is authorized by this document. +**Parent:** D-SAG-6 [#1760](https://github.com/AdaWorldAPI/lance-graph/pull/1760) (merged, 4c8f5b9; `d-sag-6-rust-codegraph-math-logic-tracert-v1.md`). **Coordination:** [Linear EXO-50](https://linear.app/exo-red/issue/EXO-50/agent-message-bus-gpt-xgrok-ccsession-id), an append-only bus, not an approval. +**Related:** [DT64 board entry](../board/entries/2026-10-26-dt64-holographic-interface.md) (docs merged, no code). Source pins are lance-graph main `aa569bc5c41ca38edf1ce3db945007543b0c82f6`. + +## 0. Thesis and authority boundaries + +The workbench answers questions about our own project (issues, pull requests, source symbols, debt rows) as **S–P–O facts**: + +- **S** is a source-attested identity: a source system, that system's upstream key, and a source revision where the key is revision-scoped. +- **P** is a predicate whose meaning resolves through a `ClassId`. No predicate here has one yet: each is a fixture-local key with `class_id: None` and, where one exists, an OGAR convergence candidate that is reported but not bound. +- **O** is a typed edge to another identity, carried with a witness (the snapshot it was read from). + +Every answer is one of five outcomes (§3), never a bare boolean. + +**This amendment is NOT:** a second graph engine; a DT64 runtime (DT64 has docs only, `grep -E 'Dt64|DT64|dt64' crates/**/*.rs` finds 0 files); DR64³ (NFR-OP-2 is OPEN, "no DR64³ runtime"); method execution; a writer to GitHub, Linear or source; a minter of OGAR concepts; an approval for deployment. + +## 1. Placement in D-SAG-6 + +D-SAG-6-2 is the Rust MIR/Codegraph projection and stays future. D-SAG-6-W is a **project-graph projection beside it**: the same discipline (source identity, frame-bound ordinals, UNKNOWN is not FALSE) applied to issue, PR and symbol records instead of MIR. It borrows the parent's F-gates (§5) and adds no new tier to the tower. + +| D-id | Deliverable | Gate | Status | +|---|---|---|---| +| **D-SAG-6-W0** | this document | scope and authority statements explicit | docs only | +| **D-SAG-6-W1** | lab fixture `crates/sag6-workbench-probe` | §5 gates with independent scalar baseline and disable-red-runs | LAB, 15/15 tests, 8/8 disables red (2026-10-27) | +| **D-SAG-6-W2** | read-only MCP surface (`rmcp`, streamable HTTP) over the W1 query contract | all W1 gates unchanged; no write tool exists | PROPOSED, separate approval | +| **D-SAG-6-W3** | `/board` view over the same query contract | same contract; no second query path | PROPOSED, separate approval | +| **D-SAG-6-W4** | Railway deployment | separate operator authorization (§7) | NOT AUTHORIZED | + +## 2. Existing-code reuse matrix + +Verdicts: REUSE-BY-DEPENDENCY, REUSE-SHAPE (copy the shape, not the type), CONVERGE (align with an existing owner, bind later), NOT-REUSABLE, MISSING. + +| Concern | Existing code | Verdict | Note | +|---|---|---|---| +| Frame seal and staleness | `dr-math-binding-probe/src/lib.rs` `FrameStore{new, seal, advance, check -> Result<(), Refusal>}`; `Refusal::{ForeignFrame, SourceChanged, MapChanged, CoordinatesChanged, FrameResealed, ...}` | REUSE-BY-DEPENDENCY | Frames compare by identity of issue (`Weak::ptr_eq`), not value. Pulls egglog (git) and sha2; `cargo check` 53 s cold. | +| One-hop evaluation | `lance-graph-quack` `Filter::{cmp, and, ...}`, `Cmp::EqU32`, `Agg::{Count, Rows, ...}`, `lower(&Query) -> Result`; mask-risc `execute_into(program, &Planes{n_rows, masks, lanes}, &Foreign::NONE, &mut Scratch, Out)` | REUSE-BY-DEPENDENCY | Edge table with subject/predicate/object ordinal lanes plus `Filter::and[EqU32, EqU32]`: admitted, no gather, no foreign plane. | +| Multi-hop | `Filter::Semijoin` (quack `lib.rs:387`, builder `:419`) unclassified, ISSUES.md `ISS-ADMISSION-B-CALL-SITE-CLASSIFICATION-NOT-STARTED` (:74), Linear EXO-140; mask-risc `graph_hop.rs:55` `OutgoingHop` quarantined behind off-by-default feature `quarantined-gather-hop`, `ISS-GATHER-HOP-1616` (ISSUES.md:206) | MISSING / REFUSED | Two independent grounds. STATUS_BOARD D-RST-8: "multi-hop over a large domain | BLOCKED on admission A2". | +| Answer shape | dir-sim `RoleEvidence {Held{grant,path}, NotHeld, Undetermined{unread}, NotDeclared}` (`actors.rs:84-102`) | REUSE-SHAPE | Mirrored by the §3 answer enum. | +| Refusal shape | contract `epistemic_state5` `Epi5ReadError{UndeclaredClass(ClassId), GenerationMismatch, UnknownProvenance}` | REUSE-SHAPE | Typed refusal reasons, not strings. | +| Deterministic digest | contract `hash::fnv1a` | REUSE-BY-DEPENDENCY | Frame and catalogue digests. | +| Set semantics | contract `set_rules` `Truth{TwoValued, ThreeValued}`, `Population{Distinct, Bag}` | REUSE-SHAPE | Edge relation is `Distinct`; `NotHeld` is meaningful only under declared coverage. | +| Identity minting | contract `NodeGuid::mint_for(TailVariant, classid, ...)` (`canonical_node.rs:387`) | NOT used | Needs a `classid`; none exists for these entities, and the fixture does not invent one. | +| Project-work concepts | OGAR `ogar-vocab` (main 68cb29b): `PROJECT_WORK_ITEM 0x0102`, `PROJECT_STATUS 0x0105`, `PROJECT_REPOSITORY 0x010A`, `PROJECT_RELATION`, `PROJECT_CHANGESET`, via `RedminePort`/`OpenProjectPort` aliases (`ports.rs:225-258`) | CONVERGE | Recorded as convergence candidates, unbound. | +| GitHub / Linear port; PullRequest, SourceSymbol concepts | none in `ogar-vocab` | MISSING | An OGAR change per `HOTPLUG-MIGRATION-GUIDE`; out of scope here. | +| String-id graph | contract `literal_graph` (String ids) | NOT-REUSABLE | Identity must not be a string on the hot path. | +| DT64 binding | docs #1794-#1799, #1804; 0 code files | MISSING | Not consumed; W1 does not claim DT64 conformance. | +| DR64² relation tile | existing lab surface | optional | Not needed for W1; Quack lanes suffice. DR64² only after cost proof. | +| DR64³ | NFR-OP-2 OPEN | MISSING | Not used. | +| DurableRef / ThoughtCommitId | doc comments only (`mork-pathmap-probe/src/rmap.rs:70`, `:690`); EXO-148, D-RST-1 | MISSING | No durable-replay claims. | +| MCP transport | rmcp 1.x `StreamableHttpService`, `surrealdb/surrealdb/mcp/src/service.rs:941-943` | REUSE-BY-DEPENDENCY at W2 | Precedent only; W1 has no transport. | +| `adarail_mcp` as host | Python/FastAPI at `mcp.exo.red`; write tools `ingest`, `post`, `message`, `upload_image`; ~30 secret env names incl. `GITHUB_TOKEN` and a writable Upstash | NOT-REUSABLE | A read-only workbench must not share a process with write tools or write-scoped secrets. | + +## 3. Data contract (conceptual; lab types, not ABI) + +**GlobalId** = (source system, upstream key bytes, source revision for revision-scoped keys). Linear and PR keys are stable, but their content is snapshot-scoped. Source symbols are revision-scoped (repo, commit, path, item path), so the same symbol name at two revisions is two identities (F01). A cold intern table maps GlobalId to a frame-local ordinal; strings never enter the hot path. + +**SourceSnapshot** = (system, upstream revision, object read, fetched_at). A Linear edge's snapshot is the issue it was read from at that issue's `updatedAt`; a source symbol is pinned at the commit it was checked at. + +**Canonical records (W1).** The `Record`s in `src/fixture.rs`, each carrying its snapshot, upstream locator and grade, plus the declared coverage (`Corpus::mark_complete`). Everything a `Workbench` holds (interned ids, the four `u32` lanes, the frame) is derived from them and rebuilt on load. Storing the raw upstream payloads as fetched is a W2 sync-job deliverable, not part of W1. + +**Frame.** `Workbench` owns a `dr_math_binding_probe::FrameStore`. On each load it advances to `FrameRevisions { source, relation_map, coordinates }`, each an `fnv1a` digest (of the snapshots, the predicate catalogue and the interned identity list). A `LocalRef` carries the `Frame` it was issued under; frames compare by identity of issue, not by value, so a coordinate from another workbench is `ForeignFrame` even at equal numbers, and any reload makes earlier coordinates `SourceChanged` / `MapChanged` / `CoordinatesChanged` / `FrameResealed` (F07, F11). + +**Predicate catalogue** (fixture-local ordinals; not DT64 slots, not classids): + +| Predicate | Shape | Symmetric | Inverse (projection, never stored) | ClassId convergence candidate | +|---|---|---|---|---| +| `blocks` | issue → issue | no | `blocked_by` | `PROJECT_RELATION` | +| `related_to` | issue ↔ issue | yes | — | `PROJECT_RELATION` | +| `mentions_symbol` | issue → source line at a commit | no | `mentioned_by` | none (no SourceSymbol concept) | +| `tracked_by_debt_row` | issue → `ISSUES.md` row at a commit | no | `tracks` | none | +| `cites_pr` | issue → pull request | no | `cited_by` | none (no PullRequest concept) | +| `authored_in_session` | artifact → Claude Code session id | no | `authored` | none | + +A `merged_as` (PR → commit) predicate would converge onto `PROJECT_CHANGESET`; it is not in W1 because no fixture record needs it. + +**Evidence grades** (`Grade`): `ObservedSource`, `CompilerDerived`, `LogicallyDerived`, `Tested`, `IndependentlyVerified`, `Hypothesis` — the parent plan §2 list. W1 uses two: every record is `ObservedSource` except one inferred edge, which is `Hypothesis` and is listed by `list_unverified_claims`. Stale evidence is not a grade: it is a frame refusal. + +**Answer** (never `bool`): `Witnessed { witnesses, complete }` | `NotHeld` (only when the edge set was declared complete) | `Undetermined { unread }` | `Refused(Reason)` | `Unsupported(op)`. `Reason` = `Frame(FrameRefusal)` | `MultiHopNotAdmitted` | `PredicateUnbound` | `Executor(..)`. This mirrors dir-sim's `RoleEvidence`. + +## 4. Execution path + +| Question shape | Path | Verdict | +|---|---|---| +| One-hop forward ("what does X block?") | edge table; `Filter::and[subject == X, predicate == blocks]` lowered by Quack, run by mask-risc `execute_into` | ADMITTED | +| One-hop inverse ("what blocks X?") | `Filter::and[object == X, predicate == blocks]`: `blockedBy` is a column read of `blocks`, never stored twice. Cross-checked against Linear's own `blockedBy` list as an oracle. | ADMITTED | +| Symmetric (`related_to`) | one stored direction, queried on both columns | ADMITTED | +| Multi-hop, transitive blocker chains | would need `Semijoin` (EXO-140, ISS-ADMISSION-B...:74) or `OutgoingHop` (ISS-GATHER-HOP-1616, ISSUES.md:206) | REFUSED: `Refused(MultiHopNotAdmitted)`, citing both | +| Provenance of an identity (every edge touching it) | `Filter::or[subject == X, object == X]` | ADMITTED | +| Unverified claims | `Filter::cmp(grade == Hypothesis)` over the grade lane | ADMITTED | +| Method inspection / binding for a predicate | no prepared methods exist; no predicate has a classid | `inspect_predicate` → `Unsupported`; `prepare_method` → `Refused(PredicateUnbound)` for any classid | +| Snapshot comparison | set difference of the canonical records | cold audit, not a query path | + +The independent scalar baseline is a plain loop over the original edge records, **test-only**. It is never a fallback inside a served path. + +## 5. Falsifiers — W1 results + +Run: `cd crates/sag6-workbench-probe && cargo test` — **15 passed, 0 failed** (2026-10-27, lance-graph `aa569bc` + this crate). Every test names what makes it fail; the baseline oracle compares by `GlobalId` over the raw records and shares no code with the ordinal lanes or the Quack program. + +| # | Falsifier | Parent gate | Test (`tests/falsifiers.rs`) | +|---|---|---|---| +| 1 | Same path at two revisions is two identities; each answers only for its own revision | F01 | `the_same_symbol_at_two_revisions_is_two_identities` | +| 2 | A coordinate from another workbench, same corpus and same ordinal, is `ForeignFrame`; the silence twin accepts it where issued | F07 | `a_coordinate_from_another_frame_is_refused` | +| 3 | An unread edge set answers `Undetermined`, an incomplete one `complete: false` | F06 | `missing_coverage_is_undetermined_not_false` | +| 3b | Silence twin: a fully read empty edge set answers `NotHeld` | F06 | `a_fully_read_empty_edge_set_is_not_held` | +| 4 | Reload refuses earlier coordinates: identical corpus `FrameResealed`, changed snapshot `SourceChanged` | F11 | `a_reload_invalidates_every_earlier_coordinate` | +| 5 | No predicate binds a prepared method, even with a real OGAR classid (`0x0102`) | F04 / F14 | `an_unbound_predicate_refuses_every_prepared_method` | +| 6 | Queries leave the canonical records unchanged (W1 has no write path; all query methods take `&self`) | F13 | `queries_do_not_change_the_canonical_records` | +| 7 | The inferred edge is listed as unverified and keeps grade `Hypothesis` in answers | F15 | `an_inferred_edge_is_reported_as_a_hypothesis` | +| 8 | Quack + mask-risc equals the scalar baseline for every identity × predicate × direction (≥ 20 non-empty comparisons, asserted) | F10 | `quack_matches_the_independent_baseline_everywhere` | +| 8b | `blocked_by` equals Linear's own `blockedBy` lists; only the 2 `blocks` rows are stored | DT64-3 inverse parity | `blocked_by_is_a_projection_that_matches_linear` | +| 9 | Derived state is disposable: a workbench rebuilt from the records alone answers identically. W1 has no Redis; this is the property a cache must preserve | new W-gate | `derived_state_is_disposable` | +| 10 | Importing the same records twice changes neither the corpus nor the snapshot diff | new W-gate | `a_replayed_import_is_idempotent` | +| — | Multi-hop is refused; the one-hop parts of `explain_blocker` still answer | F04 / D-RST-8 | `multi_hop_is_refused_not_emulated` | +| — | `compare_snapshots` reports exactly an added record | — | `compare_snapshots_reports_exactly_the_change` | +| — | Every witness carries a snapshot revision and an `https://` locator | F15 | `every_witness_carries_its_source` | + +**Disable runs** (each patch asserted to apply exactly once, then restored with `git checkout`; tree clean after): + +| Disable | Tests that went red | +|---|---| +| D1 coverage always complete | `missing_coverage_is_undetermined_not_false`, `multi_hop_is_refused_not_emulated` | +| D2 coverage never complete | `a_fully_read_empty_edge_set_is_not_held`, `blocked_by_is_a_projection_that_matches_linear` | +| D3 frame check removed | `a_coordinate_from_another_frame_is_refused`, `a_reload_invalidates_every_earlier_coordinate` | +| D4 symbol identity drops its revision | `the_same_symbol_at_two_revisions_is_two_identities` | +| D5 inverse reads the forward column | 6 tests incl. the baseline and the Linear projection check | +| D6 `query_chain` answers `NotHeld` | `multi_hop_is_refused_not_emulated` | +| D7 witness grade laundered to `ObservedSource` | `an_inferred_edge_is_reported_as_a_hypothesis` | +| D8 `prepare_method` returns `Ok` | `an_unbound_predicate_refuses_every_prepared_method` | + +**Not claimed:** no timing (the fixture is 19 records; a timing would measure nothing); no claim beyond this bounded slice; no DT64 conformance. + +## 6. Technical-debt and EXO-50 references + +| Item | Status / relation (read 2026-10-27) | +|---|---| +| EXO-111 | Backlog; blockedBy EXO-112; related EXO-50 | +| EXO-112 | Backlog; blocks EXO-111; related EXO-50; label "CC: Operator Decision" | +| EXO-140 | Backlog; related EXO-46, EXO-114, EXO-135; "CC: Operator Decision"; names `Filter::Semijoin`; cites #1640, #1732 | +| EXO-148 | Backlog; blocks EXO-55; related EXO-45, EXO-50; cites #1730; DurableRef / ThoughtCommitId do not exist | +| EXO-50 | Done (2026-10-26); append-only bus, not an approval | + +| ISSUES.md row | Line | Relevance | +|---|---|---| +| `ISS-DURABLEREF-THOUGHTCOMMITID` | :176 | OPEN, owned by D-RST-1; blocks any durable-replay claim | +| `ISS-ADMISSION-B-CALL-SITE-CLASSIFICATION-NOT-STARTED` | :74 | `Semijoin` unclassified; blocks multi-hop | +| `ISS-GATHER-HOP-1616` | :206 | `OutgoingHop` quarantined; blocks multi-hop | + +STATUS_BOARD: **D-RST-1** (DurableRef, "LAB ONLY ... Queued", :281), **D-RST-6** (queued on A1), **D-RST-8** (multi-hop, BLOCKED on admission A2). + +## 7. Open prerequisites (owner decisions) + +| Owner | Question | Blocks | +|---|---|---| +| OGAR owner | Add a GitHub / Linear port and PullRequest / SourceSymbol concepts, or confirm convergence onto the `PROJECT_*` ids? | binding predicates to ClassIds (W2 method inspection) | +| Operator (EXO-140) | ADMISSION B classification of `Filter::Semijoin` | multi-hop answers (any stage) | +| D-RST-1 owner (EXO-148) | Home for DurableRef / ThoughtCommitId | durable replay claims | +| Operator | Domain: `mcp.exo.red` is occupied by `adarail-production`; proposed `workbench.mcp.exo.red` | W4 | +| Operator | Railway workspace and service ownership; a separate service, not co-hosted with `adarail_mcp` | W4 | +| Operator | Read-only GitHub and Linear tokens, held by a separate sync job, not by the query service | W2 sync, W4 | +| Operator | Is Redis/Upstash used at all? If yes: cache only, read-only key namespace, rebuildable | W2 | +| Operator | Resolve `railway.toml` (DOCKERFILE, hc 100 s) vs `railway.json` (NIXPACKS, hc 10 s) disagreement if either file is reused | W4 | + +## 8. Proposed first implementation PR (separate from deployment) + +**Title (PROPOSED):** `D-SAG-6-W0/W1: dogfood workbench amendment + read-only lab fixture`. +**Scope:** this document; `crates/sag6-workbench-probe` (own `[workspace]`, excluded from root; deps `lance-graph-quack`, `lance-graph-mask-risc`, `lance-graph-contract` for `hash::fnv1a`, `dr-math-binding-probe` for `FrameStore`); its tests; board rows (STATUS_BOARD D-ids W0-W4, an `entries/` finding, regenerated indexes in the same commit). +**Not included:** any MCP server or transport; `/board` view; Railway or domain change; GitHub/Linear sync or tokens; Redis; OGAR concept mint or ClassId; multi-hop; DR64³; DurableRef; writes to any external system; changes to `adarail_mcp`; CI. The root `Cargo.toml` gains one `exclude` entry for the probe and nothing else. + +**This amendment is NOT a deployed service, a DT64 or DR64³ runtime, a second graph engine, an OGAR concept mint, a multi-hop reasoner, or an authorization to merge, deploy or write to GitHub, Linear or source.** diff --git a/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md b/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md new file mode 100644 index 000000000..e1756848f --- /dev/null +++ b/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md @@ -0,0 +1,190 @@ +# D-SAG-6-W: MCP read surface, /board UI, Railway plan (W2-W4) v1 + +- **Date:** 2026-10-27 +- **Status:** PROPOSAL / docs only. Covers W2-W4 of D-SAG-6-W (sibling doc `d-sag-6-w-dogfood-mcp-workbench-v1.md`). Deployment is NOT authorized by this document. +- **Depends on:** W1 lab crate `crates/sag6-workbench-probe`. Every function named below exists there and is covered by `tests/falsifiers.rs` (15 tests). Fields marked **W2** do not exist in W1 and need the sync job's richer snapshots. +- **Sources:** design-notes facts only (Linear read 2026-10-27; lance-graph main `aa569bc`). + +## 0. Scope and non-goals + +| In scope | Out of scope | +|---|---| +| Seven read-only query tools over a snapshot of project-graph records | Executing methods, ActionDefs or any write path | +| A plain server-rendered `/board` over the same seven functions | Any client-side graph engine | +| A deployment proposal for an isolated Railway service | Touching `adarail_mcp` or its secrets | + +Rules that hold for every tool: + +- No tool executes methods, reads the filesystem, modifies code, or mutates issues (GitHub or Linear). +- MCP tool annotations on all seven: `readOnlyHint=true`, `destructiveHint=false`, `idempotentHint=true`, `openWorldHint=false`. +- Inputs are bounded: ids are strings of at most 128 bytes; every list has a `limit` (default 25, max 100); unknown fields are rejected. +- Answer kinds (mirrors dir-sim `RoleEvidence`; never a bare bool): + +| Kind | Meaning | +|---|---| +| WITNESSED | A record in the sealed frame supports the answer; the witness is returned. | +| NOT_HELD | Absence, returned ONLY when coverage of the queried source set is complete. | +| UNDETERMINED | Coverage is incomplete; the unread sources are listed in `unread[]`. | +| REFUSED | The operation is not admitted (reason and issue ids returned). | +| UNSUPPORTED | The operation needs a capability that does not exist (for example an unminted predicate binding). | + +- Multi-hop traversal is REFUSED, citing EXO-140 (`Filter::Semijoin` unclassified under ADMISSION B; operator decision) and ISS-GATHER-HOP-1616 (`OutgoingHop` quarantined behind `quarantined-gather-hop`). +- Method binding is refused for every predicate. There is no OGAR GitHub port and no Linear port; PullRequest and SourceSymbol have no OGAR concept. Every `Predicate` has `class_id: None`; no ClassId is invented. +- An identity that no snapshot mentions is never NOT_HELD: absence from what was read is not evidence that it does not exist upstream. + +### 0.1 Common envelope + +```json +{ + "answer": "WITNESSED | NOT_HELD | UNDETERMINED | REFUSED | UNSUPPORTED", + "frame": "string (opaque server handle of the seal the answer was computed under)", + "complete": "bool (WITNESSED only: the edge set was read in full)", + "witnesses": [ { "id": { "system": "linear|github|claude_session", "key": "string", "revision": "string|null" }, + "snapshot": { "system": "string", "object": "string", "revision": "string", "fetched_at": "string" }, + "locator": "https://...", "grade": "observed_source | ... | hypothesis" } ], + "unread": [ { "subject": "GlobalId", "predicate": "string", "direction": "forward|inverse" } ], + "refusal": { "reason": "frame: | multi_hop_not_admitted | predicate_unbound | executor", "cites": ["string"] } +} +``` + +Each field is a direct rendering of W1's `Answer` / `Witness` / `Reason`. **Frames on the wire.** A W1 `LocalRef` carries a `Frame` that compares by identity of issue, so it cannot be serialized as a number. The W2 server keeps the `LocalRef`s it issued and hands out an opaque `frame` handle; a request naming a handle that is not the current seal is REFUSED with the `FrameStore` reason. A client never sees or sends an ordinal. + +## 1. MCP tool specification (read-only) + +| Tool | W1 function | Input (all strings ≤ 128 bytes, unknown fields rejected) | Result | Refusal / unknown cases | +|---|---|---|---|---| +| `resolve_identity` | `Workbench::resolve_identity` | `system`, `key`, `revision` (required for revision-scoped keys: symbols, debt rows) | `{ global_id, frame }` | Not in any read snapshot → UNDETERMINED (never NOT_HELD). Revision-scoped key without `revision` → REFUSED. | +| `query_relationships` | `Workbench::query_relationships` | `subject`, `predicate` (one of `blocks`, `related_to`, `mentions_symbol`, `tracked_by_debt_row`, `cites_pr`, `authored_in_session`), `direction` (`forward`/`inverse`), `hops` (const 1), `limit` ≤ 100 | `witnesses[]`, `complete` | `hops > 1` → REFUSED `multi_hop_not_admitted` citing EXO-140 + ISS-GATHER-HOP-1616. Empty + complete → NOT_HELD. Empty + incomplete → UNDETERMINED with `unread`. Stale frame → REFUSED. | +| `trace_provenance` | `Workbench::trace_provenance` | `id` | every edge touching `id`: `witnesses[]` with snapshot, locator, grade | No edge → UNDETERMINED. `DurableRef` / `ThoughtCommitId` lookups → UNSUPPORTED (types do not exist; EXO-148, D-RST-1). | +| `inspect_predicate` | `Workbench::inspect_predicate`, `Workbench::prepare_method` | `key`, `bind_method` (bool) | `{ key, symmetric, inverse, class_id: null, convergence }`; e.g. `blocks` → `convergence: "ogar_vocab::class_ids::PROJECT_RELATION"` (a candidate, not a binding) | `bind_method=true` → REFUSED `predicate_unbound`, for every predicate and every classid named. Unknown key → UNSUPPORTED. | +| `explain_blocker` | `Workbench::explain_blocker` | `id` | `{ blocked_by: Answer, debt_rows: Answer, transitive: Answer }` | `transitive` is always REFUSED `multi_hop_not_admitted`. **W2:** a blocker's status and labels (e.g. "CC: Operator Decision") once the sync job stores them; W1 records carry no labels. | +| `compare_snapshots` | `Workbench::compare_snapshots` | `a`, `b` (retained snapshot ids) | `{ added: Record[], removed: Record[] }` | Either snapshot not retained → UNDETERMINED. This is a set difference of records; it does not claim temporal-version semantics and is not `QueryReference::at`. **W2:** field-level diffs need stored payloads. | +| `list_unverified_claims` | `Workbench::list_unverified_claims` | `limit` ≤ 100, `cursor` | records graded `hypothesis` | **W2:** additional reasons (no oracle cross-check, stale source, detached result per #1792's 1,032 vs 31) need the sync job; W1 lists grade only. | + +### 1.1 Worked example: `explain_blocker` on EXO-111 + +This is what W1 returns on its fixture (`tests/falsifiers.rs::multi_hop_is_refused_not_emulated` asserts the three parts), rendered in the envelope: + +```json +{ + "blocked_by": { + "answer": "WITNESSED", "complete": true, + "witnesses": [ { "id": { "system": "linear", "key": "EXO-112", "revision": null }, + "snapshot": { "system": "linear", "object": "EXO-112", + "revision": "2026-10-23T08:48:48.110Z", "fetched_at": "2026-10-27" }, + "locator": "https://linear.app/exo-red/issue/EXO-112", "grade": "observed_source" } ] + }, + "debt_rows": { "answer": "UNDETERMINED", + "unread": [ { "subject": "linear:EXO-111", "predicate": "tracked_by_debt_row", "direction": "forward" } ] }, + "transitive": { "answer": "REFUSED", + "refusal": { "reason": "multi_hop_not_admitted", "cites": ["EXO-140", "ISS-GATHER-HOP-1616"] } } +} +``` + +`blocked_by` is complete because EXO-111's relation list was read in full, and it equals Linear's own `blockedBy` (`[EXO-112]`). `debt_rows` is UNDETERMINED, not NOT_HELD: nobody checked whether a board row tracks EXO-111. What blocks EXO-112 would be a second hop, so it is refused rather than answered. (That EXO-112 is an operator decision is true in Linear, but is a W2 field: W1 does not store labels.) + +## 2. /board UI plan (minimal) + +Principle: one handler table, two transports. Each of the seven functions is registered once; MCP (streamable HTTP) and plain GET JSON for `/board` both call the same handler with the same JSON contract. The frontend contains no business logic and no client-side graph engine. Pages are server-rendered HTML (askama, matching the a2ui-rs / medcare precedent). Every page shows its `source_links` and the snapshot revision and `frame_id` in a footer. + +| View | Route | Backing function(s) | +|---|---|---| +| Overview and entry | `GET /board` | `list_unverified_claims` (summary), snapshot header | +| Subject neighborhood | `GET /board/subject/{id}` | `resolve_identity`, `query_relationships` | +| Predicate / ClassId inspection | `GET /board/predicate/{key}` | `inspect_predicate` | +| Technical-debt blockers and ownership | `GET /board/blockers` | `explain_blocker` over the open issue set | +| Provenance trace | `GET /board/trace/{id}` | `trace_provenance` | +| Snapshot comparison | `GET /board/compare?a=&b=` | `compare_snapshots` | +| Unverified / stale queue | `GET /board/unverified` | `list_unverified_claims` | + +Notes: + +- REFUSED, UNSUPPORTED and UNDETERMINED answers render as labelled states with their reason; they are never rendered as empty results. +- Query parameters are validated against the same input schemas as section 1. +- Pages are GET only; there are no forms and no write endpoints. + +## 3. Railway deployment plan (W4, NOT authorized here) + +### 3.1 Existing deployment facts + +- `mcp.exo.red` is the Railway service `adarail-production` (adarail_mcp): Python 3.11 FastAPI, SSE transport, write-capable tools (`ingest`, `post`, `message`, `upload_image`), roughly thirty secret environment names including `GITHUB_TOKEN` and a writable Upstash credential. +- Its two Railway config files disagree. `railway.toml`: builder `DOCKERFILE`, healthcheck `/health`, timeout 100 s, restart ON_FAILURE (max 3). `railway.json`: builder `NIXPACKS`, healthcheck `/health`, timeout 10 s, same restart policy. Which one Railway honors for that service has not been verified here; the workbench service must not inherit either and should declare its own builder explicitly. +- Precedent for the server side: `surrealdb/surrealdb/mcp/src/service.rs` builds a `StreamableHttpService` (rmcp 1.x) with a `LocalSessionManager` and stateful mode, behind an auth middleware. + +### 3.2 Topology + +``` + Railway workspace (existing) + +---------------------------+ +-----------------------------+ + | sag6-workbench-sync (cron)| | sag6-workbench (query) | + | read-only GitHub + Linear | | no upstream tokens | + | writes immutable snapshots|---->| mounts volume READ-ONLY | + +---------------------------+ vol +-----------------------------+ + | /mcp /board /healthz /readyz + workbench.mcp.exo.red (proposed) +``` + +- A new, isolated Railway service named `sag6-workbench`, built from a Dockerfile in lance-graph. It is not co-hosted with adarail_mcp and shares no environment variables with it. +- Two processes: (a) the query service, read-only, holding no upstream tokens; (b) the sync job (separate service or Railway cron) holding read-only GitHub and Linear credentials and writing immutable snapshot files to a Railway volume. The query service mounts that volume read-only. +- Optional cache: a Redis instance, cache only, never canonical, rebuildable from snapshots. Whether to have one at all is an operator decision. + +### 3.3 Domain + +Bare `mcp.exo.red` is occupied. Proposed: `workbench.mcp.exo.red`. Serving under `mcp.exo.red/workbench` would require changing adarail_mcp and is not recommended. Operator decision. + +### 3.4 Environment variables (names only) + +| Name | Process | Purpose | +|---|---|---| +| `WORKBENCH_BEARER_TOKENS` | query | Accepted bearer tokens, stored hashed | +| `WORKBENCH_SNAPSHOT_DIR` | query, sync | Snapshot directory on the volume | +| `PORT` | query | Listen port injected by Railway | +| `RUST_LOG` | both | Log filter | +| `GITHUB_READONLY_TOKEN` | sync only | Fine-grained token: `contents:read`, `pull_requests:read`, `issues:read` on named repositories | +| `LINEAR_READONLY_API_KEY` | sync only | Read-only Linear API key | +| `WORKBENCH_SYNC_REPOS` | sync only | Named repositories to sync | +| `WORKBENCH_SYNC_LINEAR_ISSUES` | sync only | Named Linear issues or filters to sync | +| `WORKBENCH_REDIS_URL` | query, optional | Cache only | + +No variable is shared with adarail_mcp. No secret value appears in this repository, the image, or the snapshots. + +### 3.5 Endpoints + +| Path | Behaviour | +|---|---| +| `POST/GET /mcp` | MCP streamable HTTP via rmcp `StreamableHttpService`; bearer required | +| `GET /healthz` | Liveness only; returns no data | +| `GET /readyz` | Ready only when a snapshot is loaded, the frame is sealed, and snapshot age is under a configured threshold | +| `GET /board/*` | Section 2 pages; bearer required | + +### 3.6 Authentication + +Bearer token required on `/mcp` and `/board`; scope is read only; per-token rate limit; no anonymous access; no CORS wildcard; TLS terminated by the Railway edge. `/healthz` and `/readyz` expose no snapshot content. + +### 3.7 Source sync + +- Each sync writes one append-only, immutable snapshot (raw upstream JSON as fetched, plus revision and `fetched_at`) to a temporary path and publishes it by atomic rename. +- On a new snapshot the query service re-seals a new frame; earlier frames then refuse as stale (FrameStore semantics). Replaying the same snapshot is idempotent. +- Snapshot files are the canonical record. Redis, if present, only caches derived reads. + +### 3.8 Resource budget (PROPOSED, to be measured) + +Small instance; memory bounded in proportion to snapshot size; volume sized for retained snapshots. No measured numbers exist yet; W1 measurement must set them before any request is made to the operator. + +### 3.9 Rollback and recovery + +- Redeploy the previous image. Snapshots on the volume are untouched by a redeploy. +- Loss of Redis is harmless (cache only). +- Deleting the service removes nothing upstream: the service holds no write credentials and the sync tokens are read-only. + +### 3.10 Unresolved prerequisites (operator) + +1. Domain (`workbench.mcp.exo.red` or other). +2. Railway workspace, and who owns the new service. +3. Issuance of the read-only GitHub and Linear credentials. +4. Whether a Redis cache is used at all. +5. Linear workspace consent for the read-only API key. + +### 3.11 Later and optional + +Ghidra may later become a source-analysis adapter feeding symbol records. It is not a prerequisite for W2-W4. diff --git a/Cargo.toml b/Cargo.toml index 03604ac1b..2eac5d02c 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -140,6 +140,9 @@ exclude = [ "crates/lance-graph-ogar", # D-DRF-P1 lab probe (immutable DR64 focus lease). Own [workspace]; ndarray only. "crates/drf-focus-probe", + # D-SAG-6-W1 lab probe (read-only source-attested project graph over Quack). + # Own [workspace]; pulls dr-math-binding-probe (egglog git) for FrameStore. + "crates/sag6-workbench-probe", # A lance-graph ReportResult as an addressed OGAR ObjectSlot source # (implements ogar-doc-ir's DocObjectSource::grid_of). EXCLUDED for the same # reason as lance-graph-ogar: path-deps the OGAR sibling. Verify via diff --git a/crates/sag6-workbench-probe/Cargo.toml b/crates/sag6-workbench-probe/Cargo.toml new file mode 100644 index 000000000..795b50098 --- /dev/null +++ b/crates/sag6-workbench-probe/Cargo.toml @@ -0,0 +1,26 @@ +# sag6-workbench-probe — D-SAG-6-W1, lab only. A read-only, source-attested +# project graph (GitHub PRs / commits / source symbols, Linear issues and +# relations, technical-debt rows, Claude session ids) evaluated through the +# existing Quack lowering and the mask-risc executor. No second graph engine, +# no DT64 runtime, no DR64³, no writes to any source system. +# Plan: .claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md +# Own [workspace] root, excluded from the lance-graph workspace. Run from here: +# cargo test +[package] +name = "sag6-workbench-probe" +version = "0.0.0" +edition = "2024" +publish = false +description = "Lab probe D-SAG-6-W1: source-attested project-graph fixture, one-hop queries through Quack + mask-risc, frame staleness through dr-math-binding-probe's FrameStore, typed refusals for multi-hop and unminted predicates." + +[workspace] + +[dependencies] +# One-hop evaluation: Filter/Cmp/Agg lowered by Quack, executed by mask-risc. +lance-graph-quack = { path = "../lance-graph-quack" } +lance-graph-mask-risc = { path = "../lance-graph-mask-risc" } +# `hash::fnv1a`, the workspace's one deterministic digest. +lance-graph-contract = { path = "../lance-graph-contract" } +# FrameStore / Frame / Refusal: the one implementation of frame staleness and +# foreign-frame refusal (D-DRMC lab). Reused, not mirrored. +dr-math-binding-probe = { path = "../dr-math-binding-probe" } diff --git a/crates/sag6-workbench-probe/src/fixture.rs b/crates/sag6-workbench-probe/src/fixture.rs new file mode 100644 index 000000000..e8623545e --- /dev/null +++ b/crates/sag6-workbench-probe/src/fixture.rs @@ -0,0 +1,278 @@ +//! The smallest lawful fixture: a bounded slice of real upstream records, +//! read on 2026-10-27, each with the snapshot it came from. +//! +//! Sources, exactly as read: +//! - Linear issues EXO-111, EXO-112, EXO-140, EXO-148 and EXO-50, with their +//! relation lists (`blocks`, `blockedBy`, `relatedTo`) and descriptions. +//! Each record's snapshot is the issue it was read from, at that issue's +//! `updatedAt`. +//! - lance-graph at `main` = [`LANCE_GRAPH_MAIN`]: the source lines the issues +//! name, and the `.claude/board/ISSUES.md` rows that track them, checked at +//! that commit. +//! +//! What is deliberately NOT here: +//! - Relations of issues that were not read (EXO-55, EXO-45, EXO-46, EXO-114, +//! EXO-135). They appear as objects, and their own edge sets are not marked +//! complete, so questions about them answer `Undetermined`. +//! - EXO-50's full `relatedTo` list (more than 80 issues). Only the three edges +//! the other issues report are imported, and EXO-50's `relatedTo` is not +//! marked complete. +//! - Any edge inferred from a name match. The one inferred edge is imported +//! as [`Grade::Hypothesis`] and says so in its locator. + +use crate::{Corpus, Direction, GlobalId, Grade, Predicate, Record, Snapshot, SourceSystem}; + +/// lance-graph `main` at the time of the read. +pub const LANCE_GRAPH_MAIN: &str = "aa569bc5c41ca38edf1ce3db945007543b0c82f6"; +pub const REPO: &str = "AdaWorldAPI/lance-graph"; +pub const FETCHED_AT: &str = "2026-10-27"; + +/// `updatedAt` of each Linear issue that was read. +pub const LINEAR_READ: [(&str, &str); 5] = [ + ("EXO-111", "2026-10-23T09:25:53.396Z"), + ("EXO-112", "2026-10-23T08:48:48.110Z"), + ("EXO-140", "2026-10-23T08:58:42.268Z"), + ("EXO-148", "2026-10-25T15:52:08.088Z"), + ("EXO-50", "2026-10-26T22:11:29.036Z"), +]; + +/// Linear's own `blockedBy` lists for the issues read, kept apart from the +/// imported records. The workbench never stores `blocked_by`; it projects it +/// from `blocks`, and the tests compare that projection against this list. +pub const LINEAR_BLOCKED_BY: [(&str, &[&str]); 5] = [ + ("EXO-111", &["EXO-112"]), + ("EXO-112", &[]), + ("EXO-140", &[]), + ("EXO-148", &[]), + ("EXO-50", &[]), +]; + +fn linear_snapshot(issue: &str) -> Snapshot { + let revision = LINEAR_READ + .iter() + .find(|(id, _)| *id == issue) + .map(|(_, at)| *at) + .expect("only issues that were read have snapshots"); + Snapshot { + system: SourceSystem::Linear, + revision: revision.to_owned(), + object: issue.to_owned(), + fetched_at: FETCHED_AT.to_owned(), + } +} + +fn linear_url(issue: &str) -> String { + format!("https://linear.app/exo-red/issue/{issue}") +} + +fn blob_url(path: &str, line: u32) -> String { + format!("https://github.com/{REPO}/blob/{LANCE_GRAPH_MAIN}/{path}#L{line}") +} + +fn edge( + subject: GlobalId, + predicate: Predicate, + object: GlobalId, + from_issue: &str, + locator: String, + grade: Grade, +) -> Record { + Record { + subject, + predicate, + object, + snapshot: linear_snapshot(from_issue), + locator, + grade, + } +} + +/// The fixture's records. +pub fn records() -> Vec { + use Grade::*; + use Predicate::*; + let l = GlobalId::linear; + let sym = |path: &str, line: u32| GlobalId::symbol(REPO, LANCE_GRAPH_MAIN, path, line); + let row = |anchor: &str| GlobalId::debt_row(REPO, LANCE_GRAPH_MAIN, anchor); + let pr = |n: u32| GlobalId::pull_request(REPO, n); + + vec![ + // Linear relations, read from the issue that lists them. + edge( + l("EXO-112"), + Blocks, + l("EXO-111"), + "EXO-112", + linear_url("EXO-112"), + ObservedSource, + ), + edge( + l("EXO-148"), + Blocks, + l("EXO-55"), + "EXO-148", + linear_url("EXO-148"), + ObservedSource, + ), + edge( + l("EXO-111"), + RelatedTo, + l("EXO-50"), + "EXO-111", + linear_url("EXO-111"), + ObservedSource, + ), + edge( + l("EXO-112"), + RelatedTo, + l("EXO-50"), + "EXO-112", + linear_url("EXO-112"), + ObservedSource, + ), + edge( + l("EXO-148"), + RelatedTo, + l("EXO-45"), + "EXO-148", + linear_url("EXO-148"), + ObservedSource, + ), + edge( + l("EXO-148"), + RelatedTo, + l("EXO-50"), + "EXO-148", + linear_url("EXO-148"), + ObservedSource, + ), + edge( + l("EXO-140"), + RelatedTo, + l("EXO-46"), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + edge( + l("EXO-140"), + RelatedTo, + l("EXO-114"), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + edge( + l("EXO-140"), + RelatedTo, + l("EXO-135"), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + // Source locations the issue texts name, pinned at LANCE_GRAPH_MAIN. + edge( + l("EXO-111"), + MentionsSymbol, + sym("crates/lance-graph-contract/src/mul.rs", 1086), + "EXO-111", + blob_url("crates/lance-graph-contract/src/mul.rs", 1086), + ObservedSource, + ), + edge( + l("EXO-140"), + MentionsSymbol, + sym("crates/lance-graph-quack/src/lib.rs", 387), + "EXO-140", + blob_url("crates/lance-graph-quack/src/lib.rs", 387), + ObservedSource, + ), + edge( + l("EXO-148"), + MentionsSymbol, + sym("crates/mork-pathmap-probe/src/rmap.rs", 70), + "EXO-148", + blob_url("crates/mork-pathmap-probe/src/rmap.rs", 70), + ObservedSource, + ), + // Technical-debt rows the issue texts name as their GitHub row. + edge( + l("EXO-140"), + TrackedByDebtRow, + row("ISS-ADMISSION-B-CALL-SITE-CLASSIFICATION-NOT-STARTED"), + "EXO-140", + blob_url(".claude/board/ISSUES.md", 74), + ObservedSource, + ), + edge( + l("EXO-148"), + TrackedByDebtRow, + row("ISS-DURABLEREF-THOUGHTCOMMITID"), + "EXO-148", + blob_url(".claude/board/ISSUES.md", 176), + ObservedSource, + ), + // Pull requests the issue texts cite. + edge( + l("EXO-140"), + CitesPr, + pr(1640), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + edge( + l("EXO-140"), + CitesPr, + pr(1732), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + edge( + l("EXO-148"), + CitesPr, + pr(1730), + "EXO-148", + linear_url("EXO-148"), + ObservedSource, + ), + // The session id EXO-140's text records. + edge( + l("EXO-140"), + AuthoredInSession, + GlobalId::session("session_019fbZ92dFKQ5BJHrA3YcH9A"), + "EXO-140", + linear_url("EXO-140"), + ObservedSource, + ), + // The one inference: EXO-140 says "the gather hop, behind an opt-in + // feature" and does not name a file. graph_hop.rs:55 is the reader's + // guess, so it is a hypothesis, not an observed edge. + edge( + l("EXO-140"), + MentionsSymbol, + sym("crates/lance-graph-mask-risc/src/graph_hop.rs", 55), + "EXO-140", + "inferred: EXO-140 names 'the gather hop, behind an opt-in feature' but no file" + .to_owned(), + Hypothesis, + ), + ] +} + +/// The fixture corpus, with the edge sets that were read in full. +pub fn corpus() -> Corpus { + let mut c = Corpus::default(); + c.import(records()); + for (issue, _) in LINEAR_READ { + let id = GlobalId::linear(issue); + c.mark_complete(id.clone(), Predicate::Blocks, Direction::Forward); + c.mark_complete(id.clone(), Predicate::Blocks, Direction::Inverse); + // EXO-50's relatedTo list was read but not imported in full. + if issue != "EXO-50" { + c.mark_complete(id, Predicate::RelatedTo, Direction::Forward); + } + } + c +} diff --git a/crates/sag6-workbench-probe/src/lib.rs b/crates/sag6-workbench-probe/src/lib.rs new file mode 100644 index 000000000..0627ca04b --- /dev/null +++ b/crates/sag6-workbench-probe/src/lib.rs @@ -0,0 +1,683 @@ +//! D-SAG-6-W1 — a read-only, source-attested project graph, evaluated through +//! the existing Quack lowering and the mask-risc executor. +//! +//! **Lab only.** Nothing here is a production binding store, a DT64 adapter, +//! a DR64³ axis, a method registry or an MCP server. It answers one question +//! shape — "which identities does this identity reach through this predicate, +//! and on what evidence" — and refuses every shape that has no admitted +//! execution path. +//! +//! Three things are kept apart and never inferred from one another: +//! +//! - **Identity** ([`GlobalId`]): the upstream system's own key, plus the +//! revision for keys that only mean something at a revision (a source +//! symbol is `path@commit`, never `path`). +//! - **Coordinate** ([`LocalRef`]): a frame-local ordinal. It is only valid +//! together with the [`Frame`] it was issued under, and only while that +//! frame is the store's current seal. Frame staleness is +//! `dr_math_binding_probe::FrameStore`, reused, not restated. +//! - **Evidence** ([`Witness`]): which snapshot an edge was read from, where +//! to find it upstream, and how well it is established ([`Grade`]). +//! +//! An answer is never a bare `bool`. An empty result is `NotHeld` only when +//! the edge set for that subject, predicate and direction was read in full; +//! otherwise it is `Undetermined` and names what was not read. + +pub mod fixture; + +use std::collections::{BTreeMap, BTreeSet}; + +use dr_math_binding_probe::{Frame, FrameRevisions, FrameStore, Refusal as FrameRefusal}; +use lance_graph_contract::hash::fnv1a; +use lance_graph_mask_risc::{Foreign, LaneRef, Out, Planes, Scratch, execute_into, words_for}; +use lance_graph_quack::{Agg, Cmp, Col, Filter, Query, lower}; + +/// The upstream system that owns an identity. The workbench reads from these +/// and never writes to them. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum SourceSystem { + /// GitHub: pull requests, commits, files and symbols at a commit, and the + /// board rows committed to a repository. + GitHub, + /// Linear: issues and their typed relations. + Linear, + /// A Claude Code session id, as recorded by the artifact that names it. + ClaudeSession, +} + +/// A globally stable, source-attested identity. Equality is the upstream key +/// and, for revision-scoped keys, the revision. Two symbols with the same +/// path at different commits are different identities. +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct GlobalId { + pub system: SourceSystem, + pub key: String, + /// `Some` for keys that are only meaningful at a revision (source + /// symbols, board rows); `None` for keys the upstream keeps stable + /// (a Linear issue id, a pull request number). + pub revision: Option, +} + +impl GlobalId { + pub fn linear(issue: &str) -> Self { + Self { + system: SourceSystem::Linear, + key: issue.to_owned(), + revision: None, + } + } + + pub fn pull_request(repo: &str, number: u32) -> Self { + Self { + system: SourceSystem::GitHub, + key: format!("{repo}#{number}"), + revision: None, + } + } + + /// A source location at a commit: `path#Lline`, scoped to `commit`. + pub fn symbol(repo: &str, commit: &str, path: &str, line: u32) -> Self { + Self { + system: SourceSystem::GitHub, + key: format!("{repo}:{path}#L{line}"), + revision: Some(commit.to_owned()), + } + } + + /// A technical-debt row (`.claude/board/ISSUES.md` anchor) at a commit. + pub fn debt_row(repo: &str, commit: &str, row: &str) -> Self { + Self { + system: SourceSystem::GitHub, + key: format!("{repo}:.claude/board/ISSUES.md#{row}"), + revision: Some(commit.to_owned()), + } + } + + pub fn session(id: &str) -> Self { + Self { + system: SourceSystem::ClaudeSession, + key: id.to_owned(), + revision: None, + } + } +} + +/// One read of one upstream object: which system, which revision of it, and +/// when it was read. An edge is only ever as current as its snapshot. +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Snapshot { + pub system: SourceSystem, + /// The upstream revision: a commit SHA, or a Linear `updatedAt`. + pub revision: String, + /// The object the snapshot was read from (an issue id, a repository). + pub object: String, + pub fetched_at: String, +} + +/// The predicate catalogue of this fixture. Ordinals are fixture-local; they +/// are not DT64 slots and not OGAR classids. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Predicate { + /// Linear `blocks`. Its inverse, `blocked_by`, is a projection of the + /// same rows and is never stored a second time. + Blocks, + /// Linear `relatedTo`, symmetric. + RelatedTo, + /// An issue names a source location. + MentionsSymbol, + /// An issue is tracked by a technical-debt row on the GitHub board. + TrackedByDebtRow, + /// An issue cites a pull request. + CitesPr, + /// An artifact records the Claude Code session that wrote it. + AuthoredInSession, +} + +impl Predicate { + pub const ALL: [Predicate; 6] = [ + Predicate::Blocks, + Predicate::RelatedTo, + Predicate::MentionsSymbol, + Predicate::TrackedByDebtRow, + Predicate::CitesPr, + Predicate::AuthoredInSession, + ]; + + fn ordinal(self) -> u32 { + self as u32 + } + + pub fn spec(self) -> PredicateSpec { + use Predicate::*; + let (key, symmetric, inverse, convergence) = match self { + Blocks => ( + "blocks", + false, + Some("blocked_by"), + Some("ogar_vocab::class_ids::PROJECT_RELATION"), + ), + RelatedTo => ( + "related_to", + true, + None, + Some("ogar_vocab::class_ids::PROJECT_RELATION"), + ), + MentionsSymbol => ("mentions_symbol", false, Some("mentioned_by"), None), + TrackedByDebtRow => ("tracked_by_debt_row", false, Some("tracks"), None), + CitesPr => ("cites_pr", false, Some("cited_by"), None), + AuthoredInSession => ("authored_in_session", false, Some("authored"), None), + }; + PredicateSpec { + predicate: self, + key, + symmetric, + inverse, + convergence, + } + } +} + +/// What a predicate is, as declared by this fixture. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct PredicateSpec { + pub predicate: Predicate, + pub key: &'static str, + pub symmetric: bool, + /// The name of the inverse projection, if the predicate is directed. + pub inverse: Option<&'static str>, + /// The existing OGAR concept this predicate would converge onto, if one + /// exists. A candidate, not a binding: no GitHub or Linear port maps it. + pub convergence: Option<&'static str>, +} + +/// How well an edge is established. The first five are observations or +/// derivations with a source; `Hypothesis` is an inference nobody has +/// checked against its source, and is never reported as a proven relation. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Grade { + ObservedSource, + CompilerDerived, + LogicallyDerived, + Tested, + IndependentlyVerified, + Hypothesis, +} + +/// Which way a directed predicate is read. +#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub enum Direction { + /// subject → object (`blocks`). + Forward, + /// object → subject (`blocked_by`), read from the same rows. + Inverse, +} + +/// One source-attested edge as imported. The canonical record; everything +/// else in a [`Workbench`] is derived from these and rebuildable. +#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)] +pub struct Record { + pub subject: GlobalId, + pub predicate: Predicate, + pub object: GlobalId, + pub snapshot: Snapshot, + /// Where to see the edge upstream. + pub locator: String, + pub grade: Grade, +} + +/// The edge sets that were read in full. Only these can answer `NotHeld`. +pub type Covered = (GlobalId, Predicate, Direction); + +/// The canonical, cold-side record set. Import is idempotent: the same +/// record imported twice is one record. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct Corpus { + records: BTreeSet, + coverage: BTreeSet, +} + +impl Corpus { + pub fn import(&mut self, records: impl IntoIterator) { + self.records.extend(records); + } + + /// Declare that every `predicate` edge of `subject` in `direction` was + /// read. For a symmetric predicate the direction is ignored. + pub fn mark_complete(&mut self, subject: GlobalId, predicate: Predicate, direction: Direction) { + let direction = if predicate.spec().symmetric { + Direction::Forward + } else { + direction + }; + self.coverage.insert((subject, predicate, direction)); + } + + pub fn records(&self) -> impl Iterator { + self.records.iter() + } + + pub fn len(&self) -> usize { + self.records.len() + } + + pub fn is_empty(&self) -> bool { + self.records.is_empty() + } +} + +/// A witnessed answer item: the identity reached, and the evidence for it. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct Witness { + pub id: GlobalId, + pub snapshot: Snapshot, + pub locator: String, + pub grade: Grade, +} + +/// Why a question was not answered. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Reason { + /// The coordinate was issued under a frame that is not the current seal. + Frame(FrameRefusal), + /// Multi-hop has no admitted execution path: `Filter::Semijoin` is + /// unclassified under ADMISSION B (ISSUES.md + /// ISS-ADMISSION-B-CALL-SITE-CLASSIFICATION-NOT-STARTED, Linear EXO-140), + /// and mask-risc's `OutgoingHop` is quarantined behind the off-by-default + /// `quarantined-gather-hop` feature (ISS-GATHER-HOP-1616). + MultiHopNotAdmitted, + /// The predicate has no OGAR classid binding, so no prepared method can + /// be bound to it, whatever classid the caller names. + PredicateUnbound, + /// The lowering or the executor refused the program. + Executor(String), +} + +/// An answer. Never a bare `bool`. +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Answer { + /// At least one edge was found. `complete` is true only when the edge set + /// was read in full; otherwise more edges may exist upstream. + Witnessed { + witnesses: Vec, + complete: bool, + }, + /// No edge, and the edge set was read in full. + NotHeld, + /// No edge found, but the edge set was not read in full. This is UNKNOWN, + /// not FALSE. + Undetermined { + unread: Vec, + }, + Refused(Reason), + /// The question shape has no implementation here. + Unsupported(&'static str), +} + +/// An identity lookup. +#[derive(Clone, Debug)] +pub enum Resolution { + Resolved(LocalRef), + /// No read snapshot mentions this identity. Not evidence that it does + /// not exist upstream. + NotInSnapshot, +} + +/// A frame-local coordinate. Only [`Workbench::resolve_identity`] issues one, +/// and it is only valid under the frame it carries. +#[derive(Clone, Debug)] +pub struct LocalRef { + frame: Frame, + ordinal: u32, +} + +impl LocalRef { + pub fn ordinal(&self) -> u32 { + self.ordinal + } +} + +/// What [`Workbench::inspect_predicate`] reports. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct PredicateInspection { + pub spec: PredicateSpec, + /// Always `None` here: no GitHub or Linear port exists in OGAR, so no + /// predicate of this fixture resolves to a classid. + pub class_id: Option, + pub method: Answer, +} + +/// [`Workbench::explain_blocker`]'s report. +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct BlockerReport { + pub blocked_by: Answer, + pub debt_rows: Answer, + /// What blocks the blockers. Multi-hop, so refused. + pub transitive: Answer, +} + +/// The difference between two corpora, as source records. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct SnapshotDiff { + pub added: Vec, + pub removed: Vec, +} + +// Lane positions in `Planes::lanes`. +const SUBJECT: Col = Col(0); +const PREDICATE: Col = Col(1); +const OBJECT: Col = Col(2); +const GRADE: Col = Col(3); + +/// The sealed, queryable view of a [`Corpus`]: interned identities, four +/// `u32` lanes over the records in their stored order, and a frame. +#[derive(Debug)] +pub struct Workbench { + corpus: Corpus, + rows: Vec, + ids: Vec, + index: BTreeMap, + subject: Vec, + predicate: Vec, + object: Vec, + grade: Vec, + store: FrameStore, +} + +impl Workbench { + pub fn new(corpus: Corpus) -> Self { + let mut wb = Self { + corpus: Corpus::default(), + rows: Vec::new(), + ids: Vec::new(), + index: BTreeMap::new(), + subject: Vec::new(), + predicate: Vec::new(), + object: Vec::new(), + grade: Vec::new(), + store: FrameStore::new(FrameRevisions { + source: 0, + relation_map: 0, + coordinates: 0, + }), + }; + wb.load(corpus); + wb + } + + /// Replace the corpus. Every coordinate issued before is refused from now + /// on, even when the new corpus is identical: re-sealing is a new frame. + pub fn reload(&mut self, corpus: Corpus) { + self.load(corpus); + } + + fn load(&mut self, corpus: Corpus) { + let rows: Vec = corpus.records().cloned().collect(); + let mut ids = BTreeSet::new(); + for r in &rows { + ids.insert(r.subject.clone()); + ids.insert(r.object.clone()); + } + let ids: Vec = ids.into_iter().collect(); + let index: BTreeMap = ids + .iter() + .enumerate() + .map(|(i, id)| (id.clone(), i as u32)) + .collect(); + self.subject = rows.iter().map(|r| index[&r.subject]).collect(); + self.predicate = rows.iter().map(|r| r.predicate.ordinal()).collect(); + self.object = rows.iter().map(|r| index[&r.object]).collect(); + self.grade = rows.iter().map(|r| r.grade as u32).collect(); + let revisions = FrameRevisions { + source: digest(rows.iter().map(|r| { + format!( + "{:?}|{}|{}|{}", + r.snapshot.system, + r.snapshot.object, + r.snapshot.revision, + r.snapshot.fetched_at + ) + })), + relation_map: digest(Predicate::ALL.iter().map(|p| p.spec().key.to_owned())), + coordinates: digest(ids.iter().map(|id| format!("{id:?}"))), + }; + self.rows = rows; + self.ids = ids; + self.index = index; + self.corpus = corpus; + self.store.advance(revisions); + } + + /// The identity's frame-local coordinate under the current seal. + pub fn resolve_identity(&self, id: &GlobalId) -> Resolution { + match self.index.get(id) { + Some(&ordinal) => Resolution::Resolved(LocalRef { + frame: self.store.seal(), + ordinal, + }), + None => Resolution::NotInSnapshot, + } + } + + /// One hop from `at` through `predicate`, read in `direction`. + pub fn query_relationships( + &self, + at: &LocalRef, + predicate: Predicate, + direction: Direction, + ) -> Answer { + if let Err(r) = self.store.check(&at.frame) { + return Answer::Refused(Reason::Frame(r)); + } + let spec = predicate.spec(); + let p = Filter::cmp(PREDICATE, Cmp::EqU32(predicate.ordinal())); + let as_subject = Filter::and([Filter::cmp(SUBJECT, Cmp::EqU32(at.ordinal)), p.clone()]); + let as_object = Filter::and([Filter::cmp(OBJECT, Cmp::EqU32(at.ordinal)), p]); + let filter = match (spec.symmetric, direction) { + (true, _) => Filter::or([as_subject, as_object]), + (false, Direction::Forward) => as_subject, + (false, Direction::Inverse) => as_object, + }; + let kept = match self.keep(filter) { + Ok(kept) => kept, + Err(reason) => return Answer::Refused(reason), + }; + let mut witnesses = Vec::new(); + for row in set_bits(&kept) { + let other = if self.subject[row] == at.ordinal && self.object[row] != at.ordinal { + self.object[row] + } else if self.object[row] == at.ordinal { + self.subject[row] + } else { + self.object[row] + }; + witnesses.push(self.witness(row, other)); + } + let direction = if spec.symmetric { + Direction::Forward + } else { + direction + }; + let covered = (self.ids[at.ordinal as usize].clone(), predicate, direction); + let complete = self.corpus.coverage.contains(&covered); + match (witnesses.is_empty(), complete) { + (false, _) => Answer::Witnessed { + witnesses, + complete, + }, + (true, true) => Answer::NotHeld, + (true, false) => Answer::Undetermined { + unread: vec![covered], + }, + } + } + + /// More than one hop. There is no admitted execution path; see + /// [`Reason::MultiHopNotAdmitted`]. + pub fn query_chain(&self, _at: &LocalRef, _path: &[(Predicate, Direction)]) -> Answer { + Answer::Refused(Reason::MultiHopNotAdmitted) + } + + /// Every edge that touches `at`, with its snapshot, locator and grade. + pub fn trace_provenance(&self, at: &LocalRef) -> Answer { + if let Err(r) = self.store.check(&at.frame) { + return Answer::Refused(Reason::Frame(r)); + } + let filter = Filter::or([ + Filter::cmp(SUBJECT, Cmp::EqU32(at.ordinal)), + Filter::cmp(OBJECT, Cmp::EqU32(at.ordinal)), + ]); + match self.keep(filter) { + Ok(kept) => { + let witnesses: Vec = set_bits(&kept) + .map(|row| { + let other = if self.subject[row] == at.ordinal { + self.object[row] + } else { + self.subject[row] + }; + self.witness(row, other) + }) + .collect(); + if witnesses.is_empty() { + Answer::Undetermined { unread: Vec::new() } + } else { + Answer::Witnessed { + witnesses, + complete: false, + } + } + } + Err(reason) => Answer::Refused(reason), + } + } + + pub fn inspect_predicate(&self, predicate: Predicate) -> PredicateInspection { + PredicateInspection { + spec: predicate.spec(), + class_id: None, + method: Answer::Unsupported( + "no prepared method: the predicate has no OGAR classid binding (no GitHub or Linear port)", + ), + } + } + + /// Bind a prepared method to `predicate` under `class_id`. Refused for + /// every predicate and every classid here, because none is bound; a + /// caller naming the convergence candidate's classid does not create a + /// binding. + pub fn prepare_method(&self, predicate: Predicate, class_id: u16) -> Result<(), Reason> { + let _ = (predicate, class_id); + Err(Reason::PredicateUnbound) + } + + /// What blocks `at`, and which debt rows track it. The blockers' + /// blockers would be a second hop, so that part is refused. + pub fn explain_blocker(&self, at: &LocalRef) -> BlockerReport { + BlockerReport { + blocked_by: self.query_relationships(at, Predicate::Blocks, Direction::Inverse), + debt_rows: self.query_relationships( + at, + Predicate::TrackedByDebtRow, + Direction::Forward, + ), + transitive: self.query_chain( + at, + &[ + (Predicate::Blocks, Direction::Inverse), + (Predicate::Blocks, Direction::Inverse), + ], + ), + } + } + + /// Edges graded `Hypothesis`: claims nobody has checked against their + /// source. + pub fn list_unverified_claims(&self) -> Result, Reason> { + let kept = self.keep(Filter::cmp(GRADE, Cmp::EqU32(Grade::Hypothesis as u32)))?; + Ok(set_bits(&kept).map(|row| &self.rows[row]).collect()) + } + + /// The source records in `after` that are not in `before`, and the + /// reverse. A cold comparison of the canonical records, not a query. + pub fn compare_snapshots(before: &Corpus, after: &Corpus) -> SnapshotDiff { + SnapshotDiff { + added: after.records.difference(&before.records).cloned().collect(), + removed: before.records.difference(&after.records).cloned().collect(), + } + } + + pub fn corpus(&self) -> &Corpus { + &self.corpus + } + + fn witness(&self, row: usize, other: u32) -> Witness { + let r = &self.rows[row]; + Witness { + id: self.ids[other as usize].clone(), + snapshot: r.snapshot.clone(), + locator: r.locator.clone(), + grade: r.grade, + } + } + + /// Lower `filter` with Quack and run it on mask-risc over the four lanes. + /// The kept rows come back as a mask; nothing is copied out of the lanes. + fn keep(&self, filter: Filter) -> Result, Reason> { + let n = self.rows.len(); + let mut kept = vec![0u64; words_for(n)]; + if n == 0 { + return Ok(kept); + } + let program = lower(&Query { + filter, + agg: Agg::Rows, + }) + .map_err(|e| Reason::Executor(format!("{e:?}")))?; + let lanes = [ + LaneRef::U32(&self.subject), + LaneRef::U32(&self.predicate), + LaneRef::U32(&self.object), + LaneRef::U32(&self.grade), + ]; + let planes = Planes { + n_rows: n, + masks: &[], + lanes: &lanes, + }; + let mut scratch = + Scratch::for_program(&program, n).map_err(|e| Reason::Executor(format!("{e:?}")))?; + execute_into( + &program, + &planes, + &Foreign::NONE, + &mut scratch, + Out::Mask(&mut kept), + ) + .map_err(|e| Reason::Executor(format!("{e:?}")))?; + Ok(kept) + } +} + +fn digest(parts: impl Iterator) -> u64 { + let mut joined = String::new(); + for p in parts { + joined.push_str(&p); + joined.push('\n'); + } + fnv1a(joined.as_bytes()) +} + +/// Positions of the set bits, in row order. +fn set_bits(words: &[u64]) -> impl Iterator + '_ { + words.iter().enumerate().flat_map(|(w, &word)| { + let mut bits = word; + std::iter::from_fn(move || { + if bits == 0 { + return None; + } + let t = bits.trailing_zeros() as usize; + bits &= bits - 1; + Some(w * 64 + t) + }) + }) +} diff --git a/crates/sag6-workbench-probe/tests/falsifiers.rs b/crates/sag6-workbench-probe/tests/falsifiers.rs new file mode 100644 index 000000000..2e5733650 --- /dev/null +++ b/crates/sag6-workbench-probe/tests/falsifiers.rs @@ -0,0 +1,412 @@ +//! D-SAG-6-W1 falsifiers. Gate ids are the D-SAG-6 F-gates +//! (`.claude/plans/d-sag-6-rust-codegraph-math-logic-tracert-v1.md` §5); +//! W-gates are new to the workbench. + +use dr_math_binding_probe::Refusal as FrameRefusal; +use sag6_workbench_probe::fixture::{self, LANCE_GRAPH_MAIN, LINEAR_BLOCKED_BY, REPO}; +use sag6_workbench_probe::{ + Answer, Corpus, Direction, GlobalId, Grade, Predicate, Reason, Record, Resolution, Witness, + Workbench, +}; + +fn local(wb: &Workbench, id: &GlobalId) -> sag6_workbench_probe::LocalRef { + match wb.resolve_identity(id) { + Resolution::Resolved(r) => r, + Resolution::NotInSnapshot => panic!("{id:?} is in the fixture"), + } +} + +fn ids(answer: &Answer) -> Vec { + match answer { + Answer::Witnessed { witnesses, .. } => { + let mut v: Vec = witnesses.iter().map(|w| w.id.clone()).collect(); + v.sort(); + v + } + _ => Vec::new(), + } +} + +/// The independent baseline: a scan of the canonical records by `GlobalId`, +/// sharing no code with the ordinal lanes or the Quack program. +fn oracle(corpus: &Corpus, at: &GlobalId, p: Predicate, d: Direction) -> Vec { + let mut out = Vec::new(); + for r in corpus.records().filter(|r| r.predicate == p) { + let symmetric = p.spec().symmetric; + if (symmetric || d == Direction::Forward) && &r.subject == at { + out.push(r.object.clone()); + } + if (symmetric || d == Direction::Inverse) && &r.object == at { + out.push(r.subject.clone()); + } + } + out.sort(); + out +} + +fn every_identity(corpus: &Corpus) -> Vec { + let mut v: Vec = corpus + .records() + .flat_map(|r| [r.subject.clone(), r.object.clone()]) + .collect(); + v.sort(); + v.dedup(); + v +} + +/// F10. FAILS IF the Quack + mask-risc path and the scalar oracle disagree +/// on any identity, predicate and direction of the fixture. +#[test] +fn quack_matches_the_independent_baseline_everywhere() { + let corpus = fixture::corpus(); + let wb = Workbench::new(corpus.clone()); + let mut compared = 0; + let mut non_empty = 0; + for id in every_identity(&corpus) { + let at = local(&wb, &id); + for p in Predicate::ALL { + for d in [Direction::Forward, Direction::Inverse] { + let expected = oracle(&corpus, &id, p, d); + assert_eq!( + ids(&wb.query_relationships(&at, p, d)), + expected, + "{id:?} {p:?} {d:?}" + ); + compared += 1; + non_empty += usize::from(!expected.is_empty()); + } + } + } + // Anti-vacuity: the comparison covers real edges, not only empty answers. + assert!(non_empty >= 20, "only {non_empty} non-empty comparisons"); + assert_eq!( + compared, + every_identity(&corpus).len() * Predicate::ALL.len() * 2 + ); +} + +/// Inverse projection. FAILS IF `blocked_by` is not exactly Linear's own +/// `blockedBy` list for every issue that was read, or if any `blocked_by` +/// row was stored (the inverse is a projection of `blocks`). +#[test] +fn blocked_by_is_a_projection_that_matches_linear() { + let wb = Workbench::new(fixture::corpus()); + for (issue, linear_says) in LINEAR_BLOCKED_BY { + let at = local(&wb, &GlobalId::linear(issue)); + let mut expected: Vec = linear_says.iter().map(|i| GlobalId::linear(i)).collect(); + expected.sort(); + let answer = wb.query_relationships(&at, Predicate::Blocks, Direction::Inverse); + assert_eq!(ids(&answer), expected, "{issue}"); + if expected.is_empty() { + assert_eq!(answer, Answer::NotHeld, "{issue} was read in full"); + } + } + let blocks_rows = wb + .corpus() + .records() + .filter(|r| r.predicate == Predicate::Blocks) + .count(); + assert_eq!( + blocks_rows, 2, + "EXO-112 blocks EXO-111, EXO-148 blocks EXO-55; nothing else" + ); +} + +/// F06. FAILS IF an edge set that was not read answers `NotHeld`. +#[test] +fn missing_coverage_is_undetermined_not_false() { + let wb = Workbench::new(fixture::corpus()); + // EXO-55 appears only as an object; its own relations were never read. + let exo55 = local(&wb, &GlobalId::linear("EXO-55")); + match wb.query_relationships(&exo55, Predicate::Blocks, Direction::Forward) { + Answer::Undetermined { unread } => { + assert_eq!( + unread, + vec![( + GlobalId::linear("EXO-55"), + Predicate::Blocks, + Direction::Forward + )] + ) + } + other => panic!("expected Undetermined, got {other:?}"), + } + // EXO-50's relatedTo list was not imported in full: three edges, incomplete. + let exo50 = local(&wb, &GlobalId::linear("EXO-50")); + match wb.query_relationships(&exo50, Predicate::RelatedTo, Direction::Forward) { + Answer::Witnessed { + witnesses, + complete, + } => { + assert_eq!(witnesses.len(), 3); + assert!(!complete); + } + other => panic!("expected an incomplete witness set, got {other:?}"), + } +} + +/// F06, the silence twin. FAILS IF an edge set that WAS read in full and is +/// empty answers anything but `NotHeld` — a guard that always says UNKNOWN +/// is as useless as one that never does. +#[test] +fn a_fully_read_empty_edge_set_is_not_held() { + let wb = Workbench::new(fixture::corpus()); + let exo50 = local(&wb, &GlobalId::linear("EXO-50")); + assert_eq!( + wb.query_relationships(&exo50, Predicate::Blocks, Direction::Inverse), + Answer::NotHeld + ); + let exo112 = local(&wb, &GlobalId::linear("EXO-112")); + assert_eq!( + wb.query_relationships(&exo112, Predicate::Blocks, Direction::Inverse), + Answer::NotHeld + ); +} + +/// F01. FAILS IF the same path at two revisions collapses into one identity, +/// or a question about one revision returns the other. +#[test] +fn the_same_symbol_at_two_revisions_is_two_identities() { + let path = "crates/lance-graph-contract/src/mul.rs"; + let at_main = GlobalId::symbol(REPO, LANCE_GRAPH_MAIN, path, 1086); + let at_other = GlobalId::symbol(REPO, "0000000000000000000000000000000000000000", path, 1086); + assert_eq!(at_main.key, at_other.key, "same path and line"); + assert_ne!(at_main, at_other); + + let mut corpus = fixture::corpus(); + let original: Vec = corpus + .records() + .filter(|r| r.object == at_main) + .cloned() + .collect(); + assert_eq!(original.len(), 1); + let mut moved = original[0].clone(); + moved.subject = GlobalId::linear("EXO-999"); + moved.object = at_other.clone(); + corpus.import([moved]); + + let wb = Workbench::new(corpus); + let a = local(&wb, &at_main); + let b = local(&wb, &at_other); + assert_ne!(a.ordinal(), b.ordinal()); + assert_eq!( + ids(&wb.query_relationships(&a, Predicate::MentionsSymbol, Direction::Inverse)), + vec![GlobalId::linear("EXO-111")] + ); + assert_eq!( + ids(&wb.query_relationships(&b, Predicate::MentionsSymbol, Direction::Inverse)), + vec![GlobalId::linear("EXO-999")] + ); +} + +/// F07. FAILS IF a coordinate issued by one workbench is accepted by another +/// built from the identical corpus, where the same ordinal names the same +/// identity by coincidence. +#[test] +fn a_coordinate_from_another_frame_is_refused() { + let a = Workbench::new(fixture::corpus()); + let b = Workbench::new(fixture::corpus()); + let id = GlobalId::linear("EXO-111"); + let from_a = local(&a, &id); + assert_eq!( + from_a.ordinal(), + local(&b, &id).ordinal(), + "same numbers on purpose" + ); + assert_eq!( + b.query_relationships(&from_a, Predicate::Blocks, Direction::Inverse), + Answer::Refused(Reason::Frame(FrameRefusal::ForeignFrame)) + ); + // Silence twin: the same coordinate is accepted where it was issued. + assert!(matches!( + a.query_relationships(&from_a, Predicate::Blocks, Direction::Inverse), + Answer::Witnessed { .. } + )); +} + +/// F11. FAILS IF a coordinate survives a reload: a changed source refuses +/// as `SourceChanged`, an identical reload as `FrameResealed`. +#[test] +fn a_reload_invalidates_every_earlier_coordinate() { + let mut wb = Workbench::new(fixture::corpus()); + let id = GlobalId::linear("EXO-148"); + let before = local(&wb, &id); + + wb.reload(fixture::corpus()); + assert_eq!( + wb.query_relationships(&before, Predicate::Blocks, Direction::Forward), + Answer::Refused(Reason::Frame(FrameRefusal::FrameResealed)) + ); + + let resealed = local(&wb, &id); + let mut changed = fixture::corpus(); + let mut r = changed.records().next().cloned().expect("non-empty"); + r.snapshot.revision = "2026-10-28T00:00:00.000Z".to_owned(); + changed.import([r]); + wb.reload(changed); + assert_eq!( + wb.query_relationships(&resealed, Predicate::Blocks, Direction::Forward), + Answer::Refused(Reason::Frame(FrameRefusal::SourceChanged)) + ); + // A fresh coordinate under the new seal answers again. + let fresh = local(&wb, &id); + assert_eq!( + ids(&wb.query_relationships(&fresh, Predicate::Blocks, Direction::Forward)), + vec![GlobalId::linear("EXO-55")] + ); +} + +/// F04 / F14. FAILS IF a prepared method binds to a predicate that has no +/// classid binding, including when the caller names a real OGAR classid. +#[test] +fn an_unbound_predicate_refuses_every_prepared_method() { + let wb = Workbench::new(fixture::corpus()); + // 0x0102 = ogar_vocab::class_ids::PROJECT_WORK_ITEM, a real classid. + for p in Predicate::ALL { + assert_eq!(wb.prepare_method(p, 0x0102), Err(Reason::PredicateUnbound)); + let inspection = wb.inspect_predicate(p); + assert_eq!(inspection.class_id, None); + assert!(matches!(inspection.method, Answer::Unsupported(_))); + } + // The convergence candidate is reported, and is not a binding. + assert_eq!( + wb.inspect_predicate(Predicate::Blocks).spec.convergence, + Some("ogar_vocab::class_ids::PROJECT_RELATION") + ); +} + +/// Multi-hop. FAILS IF a chain of hops is answered instead of refused. +#[test] +fn multi_hop_is_refused_not_emulated() { + let wb = Workbench::new(fixture::corpus()); + let at = local(&wb, &GlobalId::linear("EXO-111")); + let report = wb.explain_blocker(&at); + assert_eq!( + report.transitive, + Answer::Refused(Reason::MultiHopNotAdmitted) + ); + // The one-hop parts still answer. + assert_eq!(ids(&report.blocked_by), vec![GlobalId::linear("EXO-112")]); + assert!(matches!( + report.blocked_by, + Answer::Witnessed { complete: true, .. } + )); + assert!(matches!(report.debt_rows, Answer::Undetermined { .. })); +} + +/// F15. FAILS IF the inferred edge is dropped, hidden, or reported with any +/// grade other than `Hypothesis`. +#[test] +fn an_inferred_edge_is_reported_as_a_hypothesis() { + let wb = Workbench::new(fixture::corpus()); + let hop = GlobalId::symbol( + REPO, + LANCE_GRAPH_MAIN, + "crates/lance-graph-mask-risc/src/graph_hop.rs", + 55, + ); + let unverified = wb.list_unverified_claims().expect("runs"); + assert_eq!(unverified.len(), 1); + assert_eq!(unverified[0].object, hop); + + let at = local(&wb, &GlobalId::linear("EXO-140")); + let Answer::Witnessed { witnesses, .. } = + wb.query_relationships(&at, Predicate::MentionsSymbol, Direction::Forward) + else { + panic!("EXO-140 names symbols") + }; + let graded: Vec<(&GlobalId, Grade)> = witnesses + .iter() + .map(|w: &Witness| (&w.id, w.grade)) + .collect(); + assert!(graded.contains(&(&hop, Grade::Hypothesis))); + assert_eq!( + graded + .iter() + .filter(|(_, g)| *g == Grade::ObservedSource) + .count(), + 1 + ); +} + +/// F13. FAILS IF any query changes the canonical records. +#[test] +fn queries_do_not_change_the_canonical_records() { + let corpus = fixture::corpus(); + let wb = Workbench::new(corpus.clone()); + for id in every_identity(&corpus) { + let at = local(&wb, &id); + for p in Predicate::ALL { + let _ = wb.query_relationships(&at, p, Direction::Forward); + let _ = wb.query_relationships(&at, p, Direction::Inverse); + } + let _ = wb.trace_provenance(&at); + let _ = wb.explain_blocker(&at); + } + let _ = wb.list_unverified_claims(); + assert_eq!(wb.corpus(), &corpus); +} + +/// W-cache. FAILS IF the derived state carries anything the canonical +/// records do not: a workbench rebuilt from the records alone answers +/// identically to the one it replaces. +#[test] +fn derived_state_is_disposable() { + let first = Workbench::new(fixture::corpus()); + let answers = |wb: &Workbench| -> Vec { + every_identity(wb.corpus()) + .iter() + .flat_map(|id| { + let at = local(wb, id); + Predicate::ALL.map(|p| wb.query_relationships(&at, p, Direction::Forward)) + }) + .collect() + }; + let before = answers(&first); + drop(first); + let rebuilt = Workbench::new(fixture::corpus()); + assert_eq!(answers(&rebuilt), before); +} + +/// W-replay. FAILS IF importing the same records twice changes the corpus +/// or any answer. +#[test] +fn a_replayed_import_is_idempotent() { + let once = fixture::corpus(); + let mut twice = fixture::corpus(); + twice.import(fixture::records()); + assert_eq!(twice.len(), once.len()); + assert_eq!(twice, once); + let diff = Workbench::compare_snapshots(&once, &twice); + assert!(diff.added.is_empty() && diff.removed.is_empty()); +} + +/// compare_snapshots. FAILS IF a new record is not reported, or an +/// unchanged one is. +#[test] +fn compare_snapshots_reports_exactly_the_change() { + let before = fixture::corpus(); + let mut after = fixture::corpus(); + let mut r = before.records().next().cloned().expect("non-empty"); + r.object = GlobalId::linear("EXO-777"); + after.import([r.clone()]); + let diff = Workbench::compare_snapshots(&before, &after); + assert_eq!(diff.added, vec![r]); + assert!(diff.removed.is_empty()); +} + +/// Every witness carries its source. FAILS IF a witness has no snapshot +/// revision or no locator. +#[test] +fn every_witness_carries_its_source() { + let wb = Workbench::new(fixture::corpus()); + let at = local(&wb, &GlobalId::linear("EXO-148")); + let Answer::Witnessed { witnesses, .. } = wb.trace_provenance(&at) else { + panic!("EXO-148 has edges") + }; + assert_eq!(witnesses.len(), 6); + for w in witnesses { + assert!(!w.snapshot.revision.is_empty()); + assert!(w.locator.starts_with("https://"), "{}", w.locator); + } +} From 5aff617f0646deaa8f0d8fc312b12ca3c213e5f6 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 08:45:14 +0000 Subject: [PATCH 2/3] sag6-workbench-probe: intern identities declared in coverage An identity read in full with no edge at all was never interned, so it resolved as NotInSnapshot and its NotHeld was unreachable (codex review on #1812). load() now also interns every covered subject. New test a_fully_read_identity_with_no_edges_is_not_held reproduced the failure before the fix; its silence twin keeps an undeclared direction Undetermined. 16 passed. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01XAqKMLnsLW2mFBBbEAT6Ch --- .claude/board/INTEGRATION_PLANS.md | 2 +- .claude/board/STATUS_BOARD.md | 2 +- .../2026-10-27-d-sag-6-w-dogfood-workbench.md | 2 +- .../d-sag-6-w-dogfood-mcp-workbench-v1.md | 5 ++-- .../plans/d-sag-6-w-mcp-board-railway-v1.md | 2 +- crates/sag6-workbench-probe/src/lib.rs | 5 ++++ .../sag6-workbench-probe/tests/falsifiers.rs | 27 +++++++++++++++++++ 7 files changed, 39 insertions(+), 6 deletions(-) diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index 4e3fedc41..94faaa222 100644 --- a/.claude/board/INTEGRATION_PLANS.md +++ b/.claude/board/INTEGRATION_PLANS.md @@ -1,6 +1,6 @@ ## 2026-10-27 — D-SAG-6-W: dogfood MCP workbench → `.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md` (+ `d-sag-6-w-mcp-board-railway-v1.md`) -**Status:** W0 PROPOSAL docs; W1 LAB fixture `crates/sag6-workbench-probe` (15/15 tests, 8/8 disables red); W2-W3 PROPOSED; W4 deployment NOT AUTHORIZED. Amends D-SAG-6 (#1760) with a project-graph projection beside D-SAG-6-2. **Board:** [entry](entries/2026-10-27-d-sag-6-w-dogfood-workbench.md), [STATUS_BOARD](STATUS_BOARD.md) D-SAG-6-W0..W4. One-hop runs on Quack + mask-risc; multi-hop refused (EXO-140, ISS-GATHER-HOP-1616); no OGAR classid bound (no GitHub/Linear port). +**Status:** W0 PROPOSAL docs; W1 LAB fixture `crates/sag6-workbench-probe` (16/16 tests, 8/8 disables red); W2-W3 PROPOSED; W4 deployment NOT AUTHORIZED. Amends D-SAG-6 (#1760) with a project-graph projection beside D-SAG-6-2. **Board:** [entry](entries/2026-10-27-d-sag-6-w-dogfood-workbench.md), [STATUS_BOARD](STATUS_BOARD.md) D-SAG-6-W0..W4. One-hop runs on Quack + mask-risc; multi-hop refused (EXO-140, ISS-GATHER-HOP-1616); no OGAR classid bound (no GitHub/Linear port). **Confidence:** LAB on a 19-record real slice; no timing; nothing beyond the slice claimed. ## 2026-10-26 — D-TFLP v2: synergy revision → `.claude/plans/d-tflp-tflite-palette-polyfill-capstone-v2.md` diff --git a/.claude/board/STATUS_BOARD.md b/.claude/board/STATUS_BOARD.md index d2551731b..8253c0ec6 100644 --- a/.claude/board/STATUS_BOARD.md +++ b/.claude/board/STATUS_BOARD.md @@ -118,7 +118,7 @@ | **D-SAG-6-4** | egglog guarded law + effect-aware extraction + proof/replay traceroute | PROPOSED; separate approval | independent checker gap explicit; no effect reorder or forged proof promotion | | **D-SAG-6-5** | optional approved Rust source edit and comparative MLIR lowering | PROPOSED; separate approval | rustc/tests/differential target parity; FMA/NaN/signed-zero and effect gates | | **D-SAG-6-W0** | dogfood workbench amendment: project-graph projection beside D-SAG-6-2, reuse matrix, MCP/board/Railway plan ([plan](../plans/d-sag-6-w-dogfood-mcp-workbench-v1.md), [W2-W4](../plans/d-sag-6-w-mcp-board-railway-v1.md)) | DOCS / PROPOSAL | no deployment, no mint, no DT64/DR64³ runtime | -| **D-SAG-6-W1** | `crates/sag6-workbench-probe`: real Linear/GitHub/debt-row slice, one-hop queries via Quack `lower` + mask-risc `execute_into`, `FrameStore` reused, multi-hop and method binding refused | LAB, 15/15 tests, 8/8 disables red (2026-10-27) | F01/F04/F06/F07/F10/F11/F13/F14/F15 + W-cache + W-replay | +| **D-SAG-6-W1** | `crates/sag6-workbench-probe`: real Linear/GitHub/debt-row slice, one-hop queries via Quack `lower` + mask-risc `execute_into`, `FrameStore` reused, multi-hop and method binding refused | LAB, 16/16 tests, 8/8 disables red (2026-10-27) | F01/F04/F06/F07/F10/F11/F13/F14/F15 + W-cache + W-replay | | **D-SAG-6-W2** | read-only MCP surface (rmcp streamable HTTP), seven tools over W1 functions | PROPOSED; separate approval | no write tool; opaque frame handles; NOT_HELD only under complete coverage | | **D-SAG-6-W3** | `/board` server-rendered views over the same handler table | PROPOSED; separate approval | no frontend business logic | | **D-SAG-6-W4** | isolated Railway service + read-only sync job | NOT AUTHORIZED | domain (`mcp.exo.red` is `adarail-production`), ownership, read-only tokens: operator | diff --git a/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md b/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md index 5a044d9fc..c5347ca45 100644 --- a/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md +++ b/.claude/board/entries/2026-10-27-d-sag-6-w-dogfood-workbench.md @@ -2,7 +2,7 @@ **Date:** 2026-10-27. **Status:** W0 docs + W1 LAB (`crates/sag6-workbench-probe`, own `[workspace]`, excluded from root); W2–W3 PROPOSED; W4 deployment NOT AUTHORIZED. **Source:** [`d-sag-6-w-dogfood-mcp-workbench-v1.md`](../../plans/d-sag-6-w-dogfood-mcp-workbench-v1.md), [`d-sag-6-w-mcp-board-railway-v1.md`](../../plans/d-sag-6-w-mcp-board-railway-v1.md). Parent: D-SAG-6 (#1760). -**Measured (W1):** `cd crates/sag6-workbench-probe && cargo test` → 15 passed. Eight disable runs (coverage, frame check, symbol revision, inverse column, chain refusal, grade laundering, method binding) each turned the named test red; tree clean after restore. The Quack + mask-risc path equals a `GlobalId`-keyed scalar oracle for every identity × predicate × direction of the fixture; `blocked_by` equals Linear's own `blockedBy` lists, and only the two `blocks` rows are stored. +**Measured (W1):** `cd crates/sag6-workbench-probe && cargo test` → 16 passed. Eight disable runs (coverage, frame check, symbol revision, inverse column, chain refusal, grade laundering, method binding) each turned the named test red; tree clean after restore. The Quack + mask-risc path equals a `GlobalId`-keyed scalar oracle for every identity × predicate × direction of the fixture; `blocked_by` equals Linear's own `blockedBy` lists, and only the two `blocks` rows are stored. **Fixture:** 19 real records read 2026-10-27 — Linear EXO-111/112/140/148/50 relations, the source lines the issues name pinned at lance-graph `aa569bc` (`mul.rs:1086`, quack `lib.rs:387`, `rmap.rs:70`), their `ISSUES.md` rows (:74, :176), cited PRs #1640/#1730/#1732, one recorded session id, and one inferred edge (`graph_hop.rs:55`) graded `Hypothesis`. diff --git a/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md index 7c224379b..2ba1f18e5 100644 --- a/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md +++ b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md @@ -23,7 +23,7 @@ D-SAG-6-2 is the Rust MIR/Codegraph projection and stays future. D-SAG-6-W is a | D-id | Deliverable | Gate | Status | |---|---|---|---| | **D-SAG-6-W0** | this document | scope and authority statements explicit | docs only | -| **D-SAG-6-W1** | lab fixture `crates/sag6-workbench-probe` | §5 gates with independent scalar baseline and disable-red-runs | LAB, 15/15 tests, 8/8 disables red (2026-10-27) | +| **D-SAG-6-W1** | lab fixture `crates/sag6-workbench-probe` | §5 gates with independent scalar baseline and disable-red-runs | LAB, 16/16 tests, 8/8 disables red (2026-10-27) | | **D-SAG-6-W2** | read-only MCP surface (`rmcp`, streamable HTTP) over the W1 query contract | all W1 gates unchanged; no write tool exists | PROPOSED, separate approval | | **D-SAG-6-W3** | `/board` view over the same query contract | same contract; no second query path | PROPOSED, separate approval | | **D-SAG-6-W4** | Railway deployment | separate operator authorization (§7) | NOT AUTHORIZED | @@ -96,7 +96,7 @@ The independent scalar baseline is a plain loop over the original edge records, ## 5. Falsifiers — W1 results -Run: `cd crates/sag6-workbench-probe && cargo test` — **15 passed, 0 failed** (2026-10-27, lance-graph `aa569bc` + this crate). Every test names what makes it fail; the baseline oracle compares by `GlobalId` over the raw records and shares no code with the ordinal lanes or the Quack program. +Run: `cd crates/sag6-workbench-probe && cargo test` — **16 passed, 0 failed** (2026-10-27, lance-graph `aa569bc` + this crate). Every test names what makes it fail; the baseline oracle compares by `GlobalId` over the raw records and shares no code with the ordinal lanes or the Quack program. | # | Falsifier | Parent gate | Test (`tests/falsifiers.rs`) | |---|---|---|---| @@ -104,6 +104,7 @@ Run: `cd crates/sag6-workbench-probe && cargo test` — **15 passed, 0 failed** | 2 | A coordinate from another workbench, same corpus and same ordinal, is `ForeignFrame`; the silence twin accepts it where issued | F07 | `a_coordinate_from_another_frame_is_refused` | | 3 | An unread edge set answers `Undetermined`, an incomplete one `complete: false` | F06 | `missing_coverage_is_undetermined_not_false` | | 3b | Silence twin: a fully read empty edge set answers `NotHeld` | F06 | `a_fully_read_empty_edge_set_is_not_held` | +| 3c | An identity read in full with no edge at all still resolves and answers `NotHeld` (codex review #1812) | F06 | `a_fully_read_identity_with_no_edges_is_not_held` | | 4 | Reload refuses earlier coordinates: identical corpus `FrameResealed`, changed snapshot `SourceChanged` | F11 | `a_reload_invalidates_every_earlier_coordinate` | | 5 | No predicate binds a prepared method, even with a real OGAR classid (`0x0102`) | F04 / F14 | `an_unbound_predicate_refuses_every_prepared_method` | | 6 | Queries leave the canonical records unchanged (W1 has no write path; all query methods take `&self`) | F13 | `queries_do_not_change_the_canonical_records` | diff --git a/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md b/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md index e1756848f..9e2a9e918 100644 --- a/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md +++ b/.claude/plans/d-sag-6-w-mcp-board-railway-v1.md @@ -2,7 +2,7 @@ - **Date:** 2026-10-27 - **Status:** PROPOSAL / docs only. Covers W2-W4 of D-SAG-6-W (sibling doc `d-sag-6-w-dogfood-mcp-workbench-v1.md`). Deployment is NOT authorized by this document. -- **Depends on:** W1 lab crate `crates/sag6-workbench-probe`. Every function named below exists there and is covered by `tests/falsifiers.rs` (15 tests). Fields marked **W2** do not exist in W1 and need the sync job's richer snapshots. +- **Depends on:** W1 lab crate `crates/sag6-workbench-probe`. Every function named below exists there and is covered by `tests/falsifiers.rs` (16 tests). Fields marked **W2** do not exist in W1 and need the sync job's richer snapshots. - **Sources:** design-notes facts only (Linear read 2026-10-27; lance-graph main `aa569bc`). ## 0. Scope and non-goals diff --git a/crates/sag6-workbench-probe/src/lib.rs b/crates/sag6-workbench-probe/src/lib.rs index 0627ca04b..8fcc12945 100644 --- a/crates/sag6-workbench-probe/src/lib.rs +++ b/crates/sag6-workbench-probe/src/lib.rs @@ -417,6 +417,11 @@ impl Workbench { ids.insert(r.subject.clone()); ids.insert(r.object.clone()); } + // An identity read in full with no edge at all still resolves, so its + // NotHeld is reachable. + for (subject, _, _) in &corpus.coverage { + ids.insert(subject.clone()); + } let ids: Vec = ids.into_iter().collect(); let index: BTreeMap = ids .iter() diff --git a/crates/sag6-workbench-probe/tests/falsifiers.rs b/crates/sag6-workbench-probe/tests/falsifiers.rs index 2e5733650..aac6a3a4d 100644 --- a/crates/sag6-workbench-probe/tests/falsifiers.rs +++ b/crates/sag6-workbench-probe/tests/falsifiers.rs @@ -410,3 +410,30 @@ fn every_witness_carries_its_source() { assert!(w.locator.starts_with("https://"), "{}", w.locator); } } + +/// F06, isolated identity (codex review on #1812). FAILS IF an identity that +/// was read in full but has no edge at all cannot be resolved, which would +/// leave its honest `NotHeld` unreachable. +#[test] +fn a_fully_read_identity_with_no_edges_is_not_held() { + let mut corpus = fixture::corpus(); + let isolated = GlobalId::linear("EXO-900"); + assert!( + corpus + .records() + .all(|r| r.subject != isolated && r.object != isolated), + "the identity must have no edge, or this test measures nothing" + ); + corpus.mark_complete(isolated.clone(), Predicate::Blocks, Direction::Forward); + let wb = Workbench::new(corpus); + let at = local(&wb, &isolated); + assert_eq!( + wb.query_relationships(&at, Predicate::Blocks, Direction::Forward), + Answer::NotHeld + ); + // Silence twin: a direction that was not declared read stays UNKNOWN. + assert!(matches!( + wb.query_relationships(&at, Predicate::Blocks, Direction::Inverse), + Answer::Undetermined { .. } + )); +} From 2f934bd8c8a619fa51364db090badd39493227dd Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 27 Oct 2026 12:01:28 +0000 Subject: [PATCH 3/3] docs(D-SAG-6-W0): state what a W1 read receipt is not Linear updatedAt and Corpus::mark_complete are read receipts, not owner-issued snapshot pins, ACL attestations or complete negative observations; FrameStore refuses stale lab coordinates only and is not proposed for DT64-Q0. Reuse for Q0, #1811 or EXO-46 needs its own attested witness. Docs only, per cross-session review on #1812. Co-Authored-By: Claude Claude-Session: https://claude.ai/code/session_01XAqKMLnsLW2mFBBbEAT6Ch --- .claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md index 2ba1f18e5..74cc8a3e2 100644 --- a/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md +++ b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md @@ -60,6 +60,8 @@ Verdicts: REUSE-BY-DEPENDENCY, REUSE-SHAPE (copy the shape, not the type), CONVE **Canonical records (W1).** The `Record`s in `src/fixture.rs`, each carrying its snapshot, upstream locator and grade, plus the declared coverage (`Corpus::mark_complete`). Everything a `Workbench` holds (interned ids, the four `u32` lanes, the frame) is derived from them and rebuilt on load. Storing the raw upstream payloads as fetched is a W2 sync-job deliverable, not part of W1. +**Source-to-witness boundary (what a W1 receipt is NOT).** A W1 snapshot is a *read receipt*: which object was read, at which upstream revision string (a Linear `updatedAt`, a commit SHA), on which date. `Corpus::mark_complete` records that *this reader* read an edge set in full. Neither is an owner-issued physical snapshot pin, a permission or ACL attestation, or a complete negative observation across sources, so `NotHeld` here means "empty in what this fixture read", nothing wider. The `FrameStore` frame refuses stale *lab coordinates* only; it is not a production source snapshot and is not proposed for DT64-Q0. Reusing any W1 assertion for DT64-Q0, Report destination binding (#1811) or EXO-46 admission needs its own attested source, permission and coverage witness; an equal ordinal or digest alone must refuse. + **Frame.** `Workbench` owns a `dr_math_binding_probe::FrameStore`. On each load it advances to `FrameRevisions { source, relation_map, coordinates }`, each an `fnv1a` digest (of the snapshots, the predicate catalogue and the interned identity list). A `LocalRef` carries the `Frame` it was issued under; frames compare by identity of issue, not by value, so a coordinate from another workbench is `ForeignFrame` even at equal numbers, and any reload makes earlier coordinates `SourceChanged` / `MapChanged` / `CoordinatesChanged` / `FrameResealed` (F07, F11). **Predicate catalogue** (fixture-local ordinals; not DT64 slots, not classids):