diff --git a/.claude/board/INTEGRATION_PLANS.md b/.claude/board/INTEGRATION_PLANS.md index f25d2512a..94faaa222 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` (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` **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..8253c0ec6 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, 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 | ## 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..c5347ca45 --- /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` → 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`. + +**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..74cc8a3e2 --- /dev/null +++ b/.claude/plans/d-sag-6-w-dogfood-mcp-workbench-v1.md @@ -0,0 +1,174 @@ +# 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, 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 | + +## 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. + +**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): + +| 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` — **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`) | +|---|---|---|---| +| 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` | +| 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` | +| 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..9e2a9e918 --- /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` (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 + +| 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..8fcc12945 --- /dev/null +++ b/crates/sag6-workbench-probe/src/lib.rs @@ -0,0 +1,688 @@ +//! 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()); + } + // 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() + .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..aac6a3a4d --- /dev/null +++ b/crates/sag6-workbench-probe/tests/falsifiers.rs @@ -0,0 +1,439 @@ +//! 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); + } +} + +/// 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 { .. } + )); +}