diff --git a/.claude/board/entries/2026-11-11-codegraph-recon-1.md b/.claude/board/entries/2026-11-11-codegraph-recon-1.md new file mode 100644 index 000000000..e8e2f10cc --- /dev/null +++ b/.claude/board/entries/2026-11-11-codegraph-recon-1.md @@ -0,0 +1,18 @@ +# 2026-11-11 — Codegraph over real Charon stores: false unaffected for public symbols + +**Status:** MEASURED (probe). `.claude/probes/2026-11-11-codegraph-recon-1/`. Board: EXO-229, EXO-230. + +Charon → ruff_charon → `lance-graph-codegraph` ran on dt64, contract, quack and r2il (library targets, +9,138 positions). A sweep of `impact` + `callers` over every position took 1.2 s with 0 refusals. +`ClosureWidth(64)` and the 256-id tile are single-tile `Cube::closure` limits; Codegraph uses +`closure_wide` (`MAX_POSITIONS = 2^20 − 256`). + +**Finding:** `impact` of a `PUBLIC` symbol whose callers sit in crates outside the store returns an +empty set, not UNKNOWN. On dt64, 261 of 370 public symbols do this (`BindStore::admit`, `method_ref`: +~140 external call sites). The `cg_query` example now prints `UNKNOWN external-callers-unobserved`; +the library is unchanged. OPEN (EXO-230): should `Graded.unknown` carry it. + +rust-analyzer (`sag-ra-probe GRAPH=1`) misses calls inside macro arguments (it marks the macro region), +does not index `#[cfg(test)]` unit modules at all, and records 6,280 constructions as calls. Recall of +the curated Mermaid call edges, over observed files: Charon 61/87, RA 91/99. Most of the gap is +variant construction, which Charon does not model as a call. diff --git a/.claude/board/entries/README.md b/.claude/board/entries/README.md index 5b33a3236..6a6e823bb 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. -596 entries, 2026-08-06 .. 2026-11-10. +597 entries, 2026-08-06 .. 2026-11-11. | date | entry id | finding | file | |---|---|---|---| +| 2026-11-11 | `codegraph-recon-1` | | [2026-11-11-codegraph-recon-1.md](2026-11-11-codegraph-recon-1.md) | | 2026-11-10 | `lab-resolve-borrow-all` | | [2026-11-10-lab-resolve-borrow-all.md](2026-11-10-lab-resolve-borrow-all.md) | | 2026-11-10 | `int8-direct-packed-b` | | [2026-11-10-int8-direct-packed-b.md](2026-11-10-int8-direct-packed-b.md) | | 2026-11-10 | `D-FOUNDRY-PARITY-1` | | [2026-11-10-foundry-parity-1-lab.md](2026-11-10-foundry-parity-1-lab.md) | diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/REPORT.md b/.claude/probes/2026-11-11-codegraph-recon-1/REPORT.md new file mode 100644 index 000000000..eebc08d9c --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/REPORT.md @@ -0,0 +1,243 @@ +# D-CODEGRAPH-RECON-1: Mermaid ↔ Codegraph × Kythe × R2IL, reconstruction and review oracle + +**Status:** probe, draft. Board: EXO-229 (compiler intake), EXO-230 (navigation). Nothing here changes +lance-graph-contract, ClassView, DT64 admission, Quack/mask-RISC, XLOG, Charon/ruff_charon formats, +crai-rs semantics or Thought-Git. No new database, store, authority or executor. + +Revision: lance-graph `9f4563b` (origin/main) for every crate read; this branch adds only the read-only +`cg_query` example, this probe directory, and the regenerated `.codegraph/coverage.tsv` row it causes. + +## 1. Corpus + +`corpus.tsv`: 444 relationships from `.mermaid/03-dr-dt64-binding.md` (223), `05-methods.md` (102) and +`06-authorization.md` (119). Each row has subject, relation, object, type, page status, the cited source, +the verified current `path:line`, how it could be recovered, and the prover. + +| recoverable | rows | +|---|---| +| MECHANICAL-SYNTAX | 240 | +| MECHANICAL-CALLGRAPH | 119 | +| INTERPRETATION | 61 | +| NOT-RECOVERABLE | 24 | + +Verification against source: 435 confirmed at a current line, 7 contradicted (all partial), 2 moved, 0 not +found. Two claims were re-read by hand before use (R266: `register_derived` also inserts; R417/R422: +`walk_rails_authorized` takes a caller-supplied `allowed` closure, so the drawn `ScopedDecision → +walk_rails_authorized` edge has no call site). The pages still mark #1996 as open, though it is merged. +Ten rows carry that stale label. + +## 2. Compiler intake (EXO-229 Gate A, then B) + +Charon `c69e231` (nightly-2026-09-17; cargo-miri absent, so std bodies are opaque) → `ruff_charon import` +→ `lance-graph-codegraph`. Library targets only, default features, x86_64-unknown-linux-gnu. + +| crate | charon s | import s | rows | residual | +|---|---|---|---|---| +| lance-graph-dt64 | 29 | 1.2 | 2,636 | 0 | +| lance-graph-contract | 21 | 7 | 31,017 | 1 (`REFERENCE_NOT_NAMED rung_schedule::requires_of`) | +| lance-graph-quack | 14 | 1 | 1,799 | 0 | +| lance-graph-r2il | 7 | 1 | 2,322 | 0 | + +- Four-crate store: 9,138 positions. `open` takes 159 ms. `impact` + `callers` over every position, in + one process, take 1,224 ms with **0 refusals**. +- **Correction to the brief.** `ClosureWidth(64)` and the 256-id tile belong to the single-tile + `Cube::closure`. Codegraph on main builds `Cube::new_tiled` and answers with `closure_wide` + (`lance-graph-xlog/src/wide.rs`, `MAX_POSITIONS = 2^20 − 256`). A query on this store does not meet + those two limits. The refusal path is not exercised by these stores; the crate's own + `Inject::Closure` / `Inject::Stage` tests cover it. +- **Defect: false unaffected.** `impact` of a `PUBLIC` symbol returns an empty set when its callers are in + crates the store does not hold. On dt64 alone, 261 of 370 public symbols do this, including + `BindStore::admit` and `method_ref`, which have about 140 call sites in other crates. The store holds + the `PUBLIC` row and its observed files, so it has what it needs to say UNKNOWN. crai-rs ranks a false + unaffected above UNKNOWN in severity. `examples/cg_query.rs` now prints an + `UNKNOWN external-callers-unobserved` line for every public symbol and lists the observed files. + Disable run: removing the check drops the line (1 → 0). The library API is unchanged; whether + `Graded.unknown` should carry this is an EXO-230 decision. +- A cross-crate edge is recovered: `lance_graph_r2il::binding::prepare → BindStore::admit` (CONFIRMED). +- Grep false positive caught: `lance-graph-quack/src/bind.rs` has five `.admit(` calls. They are quack's + own test-only typed code space, and quack does not depend on dt64. + +### rust-analyzer (sag-ra-probe, `GRAPH=1`, whole workspace) + +108 s, 1,214 files, 84,391 call rows, 547 MIR errors (480 `NotSupported`). Coverage limits, all measured: + +- **Calls inside macro arguments have no call row.** All 7 `LaneBinding::check` sites in + `dt64/tests/lane_socket.rs` are inside `assert_eq!`. The probe does emit a `macro` region for each, so a + consumer can mark those regions UNKNOWN. +- **`#[cfg(test)]` unit modules are not indexed at all.** For example, `report/src/lane_source/tests.rs` + gets no `file` row, so an absent row cannot tell unobserved from absent. +- 7,247 call rows have callee kind `Unknown` (unresolved). 6,280 are constructions (`EnumMember`, + `Struct`), not calls. +- Crates in the workspace `exclude` list (most probes and labs) are not loaded. + +## 3. Reconstruction (`recon.py`) + +- `machine-recovered.mmd`: built from store rows only. `seeds.txt` names 15 nodes; it names no edges, and + `recover` never opens the corpus. Result: 70 confirmed edges, 4 `possible` (dispatch), 0 stale, and 14 + `callers outside …: UNKNOWN` nodes for public seeds. Byte-identical on a second run. +- `reconciled.mmd`: the same plus labelled human rows. 25 GAP nodes (`:::gap`, never an edge), 6 LAB, + 10 proposed/open-PR, and 7 contradicted rows, shown as notes, not edges. +- The original `.mermaid/` files are unchanged. + +### Recall of the corpus' call edges (`score.tsv`) + +A hit means a compiler call row sits at the row's cited `path:line` (or on one of the next two lines). +Rows citing a file the tool never saw are UNOBSERVED, not misses. + +| arm | hit | miss | unobserved | recall over observed | +|---|---|---|---|---| +| Charon store | 61 | 26 | 32 | 61/87 | +| rust-analyzer | 91 | 8 | 20 | 91/99 | + +The headline gap is mostly about what each tool calls a call: + +- 19 of Charon's 26 misses are variant or struct construction (`Err(Refusal::X {..})`, + `Ok(MethodRef {..})`). These are the diagram's refuses/returns edges. RA records them as call rows; + Charon lowers them to aggregate construction. Of RA's 91 hits, 23 are construction only, so it scores + 68 on real call sites. +- 5 rows cite a definition or doc line, not a call (R184, R206, R305, R415, R422), and miss under both + tools. R422 is the contradicted `ScopedDecision → walk_rails_authorized` edge, which both tools + correctly fail to find. +- On true call sites Charon misses 3: two chained `.routed_at(..)?` calls (the span starts on the + receiver line) and one `borrow` inside a closure. + +## 4. Negative tests (`recon.py --self-test`, 15 tests) + +| negative | test | disable run | +|---|---|---| +| stale facts cannot claim current code | 01 | red | +| renamed / same-name symbols keep their own identity | 02 | red | +| dynamic call never absent, never confirmed | 03 | red | +| macro-hidden call stays UNKNOWN | 04 | red | +| missing artifact is not empty | 05 | red | +| guard-only field read is not omitted | 06 | red | +| public symbol reports external callers UNKNOWN | 06b | red | +| RBAC gap never rendered as an edge | 07 | red | +| a source reference is not a call | 08 | red after a fix: the first version only checked `confirmed`, and stayed green under the disable | +| lab / proposed / merged stay distinct | 09 | red | +| reconstruction cannot pass by copying | 10 | red | +| a Rust function is not an R2IL method | 08b | red | +| a caller reached only through a stale edge is not confirmed | 11 | red | +| dispatch reaches the implementation (`IMPLEMENTS` → `MAY_DISPATCH`) | 12 | red | +| an edge from a missing source file is never drawn as verified | 13 | red | + +Tests 11–13 came from review on #2000. Each was written first and failed for the reason the review +gave, then the fix made it pass, and disabling the fix turns it red again. The dispatch join is coarse +for std traits: `BoundLanes::next` implements `Iterator::next`, so every generic `Iterator::next` +dispatch in the store becomes a POSSIBLE caller of it (8 in contract). That is correct as POSSIBLE, and +it is what `Codegraph::callers` reports too. + +Each disable asserts that its patch applied. The same check also ran on real data: a one-line edit inside +`LaneBinding::check` turned the packet `stale: true` (`packet-stale.json`), and the restored tree gives +`FRESH`. + +## 5. Review evidence packet (`packet-LaneBinding-check.json`) + +This is a read-only prototype of the crai-rs `ReviewEvidencePacket`. It uses the CR-H0 §3 OUT fields, +the CR-H1 identity fields and the five CR-H0-REVIEW-SEMANTICS axes. It carries evidence, never a verdict. +`severity` is null, `permission_state` is `NOT_DERIVED`, and every test is `NOT_RUN`. For a change to +`LaneBinding::check`: + +- **Confirmed:** `lane` (lane.rs:360) and `borrow_all` (lane.rs:386). +- **Unknown:** external callers (the symbol is `PUBLIC`), plus test and example targets. +- **Contracts:** `LaneSource::lane_of` (dispatch). +- **Tests:** 48 name-matched candidate sites, all `SOURCE_STRUCTURE / POSSIBLE`. 23 are inside macro + regions and 25 are in files RA does not index. None is confirmed by a compiler row, and none counts as + TEST_OBSERVED, because nothing ran. +- **Gap:** `cargo_lock_sha` is `NOT_TRACKED`, because the repository tracks no Cargo.lock. CR-H1's + identity assumes one. + +## 6. Retrieval measurement (4 paths × 2 runs × 10 questions, same revision) + +Arms: +- **A:** source only. +- **B:** `.codegraph/` first, freshness-checked, then source. +- **C:** compiler facts only: `cg_query` over the 4-crate store plus the RA graph. It could read source + only at a line a tool had cited. +- **D:** hybrid. + +Each arm had its own inputs and an explicit list of what it must not read. One grader graded all 80 +answers against a held-out, source-checked key, with run labels randomised. + +| run | correct | partial | wrong | tokens | tool calls | seconds | +|---|---|---|---|---|---|---| +| A1 | 8 | 2 | 0 | 545,985 | 45 | 272 | +| A2 | 7 | 3 | 0 | 519,347 | 31 | 198 | +| B1 | 6 | 4 | 0 | 515,749 | 33 | 215 | +| B2 | 7 | 3 | 0 | 536,113 | 35 | 230 | +| C1 | 7 | 3 | 0 | 541,365 | 54 | 385 | +| C2 | 8 | 2 | 0 | 537,291 | 43 | 340 | +| D1 | 7 | 3 | 0 | 534,740 | 48 | 320 | +| D2 | 9 | 1 | 0 | 546,203 | 49 | 344 | + +Every run carries ~425k of shared base context, so compare differences, not totals. + +All 80 answers were coverage-honest: none presented an unobserved region as empty, and none stated a +false item as fact. That is the main change from MEM-1, where the index arm under-reported Q3. + +| question | what separated the arms | +|---|---| +| Q3 test callers | C is PARTIAL in both runs. It sees the 2 in-crate callers and correctly marks the test sites UNKNOWN (macro regions, cfg(test), test targets), but cannot name them. A, B and D grep them. | +| Q8 blast radius | Only C and D give compiler-resolved counts (WideFieldMask 259 refs in 4 crates; MethodBinding 46 in 3). A and B give text counts (49 files / 23 crates) that mix code, tests and doc comments. Only D2 gives both, with the doc-only split. | +| Q4 reachability | Text arms list fixture functions named `method_ref` as call sites (D1), or misfile a test file as non-test (B1). C has no such errors but sees no test callers. | +| Q1 impls | B is PARTIAL in both runs: miscounting or misfiling impls while working from text. | + +Reading: +- Compiler facts bought precision on reference and call questions and cost coverage of tests. +- The hybrid arm got the best single run (9/10). +- No arm was more accurate overall with n = 2; the spread inside an arm is as large as between arms. +- Facts-backed arms were 25–90% slower in wall time, with more tool calls. Their token use was no + higher. + +### Confounds, stated + +- `.codegraph/coverage.tsv` was stale while B and D ran. This branch's new `cg_query` example had changed + the codegraph crate's row. Every B and D run reported the failed `--check` and verified against source. + The guard fired on real drift, and it is regenerated on this branch. +- C2 says a recursive Cargo.toml grep printed four lines under `.claude/probes/`. It says it did not use + them. The run is kept and marked. +- The grader found two errors in the key. Both were verified in source and corrected: + - Q4: the four r2il test callers call `method_ref`, not `admit`. + - Q6: `foundry-parity-lab/src/method.rs:218-266` lowers WHEN to mask-RISC as a LAB path outside R2IL. + + No cell was graded around them. Ten further true facts the key lacked are listed in the grader notes. + +## 7. What R2IL contributes here + +- R2IL reads registered DT64 `MethodBinding` effects. `prepare` (`r2il/src/binding.rs:321`) admits the + binding, refuses WHEN (`:336`) and three-valued truth (`:339`), and binds each effect to an opcode. +- For an ordinary Rust function, such as `LaneBinding::check`, the packet records `r2il.method = + NOT_A_METHOD, body_semantics = UNKNOWN`. Negative test 08b covers this; its disable run is red. +- **Not done:** readable per-method step reports (`Prepared::steps()`). They need a store with registered + bindings, and the only such fixtures live in r2il's integration tests, which cannot be imported. It + would be a new r2il example, which is new surface beyond this probe. + +## 8. Open + +- **crai-rs seam:** the packet is a prototype. Field-level reads (`field_readers`) and test sites are + name matches (POSSIBLE). A resolved receiver needs RA occurrence rows joined to spans, which is the + next step. +- **The mission brief is cut off** at §8 "Each finding should include: Source revision and diff". Each + packet finding carries the identity block and `changed_source.diff`. Anything specified after that + sentence is not implemented. +- **Whether `Codegraph::impact` should return UNKNOWN for public symbols** (today it is example-side + only) is an EXO-230 decision. +- **Charon test targets:** artifacts for test targets and consumer crates would close Q3 for the + compiler arm (EXO-229). + +## Reproduce + +Artifacts are not committed (build outputs; ~60 MB). From a checkout with Charon `c69e231` and +`ruff_charon` built: + +```sh +# per crate, from crates// +CARGO_TARGET_DIR=$T CARGO_PROFILE_DEV_DEBUG=0 charon cargo --no-dedup-serialized-ast --dest-file $T/.llbc +# from crates/ +ruff_charon import $STORE $T/.llbc +# rust-analyzer facts, from the repo root (≈110 s) +GRAPH=1 crates/sag-ra-probe/target/release/sag-ra-probe "$PWD" > ra_graph.tsv +# queries +cargo run --release --manifest-path crates/lance-graph-codegraph/Cargo.toml --example cg_query -- $STORE . sweep +python3 .claude/probes/2026-11-11-codegraph-recon-1/recon.py score --store $STORE --src . --corpus corpus.tsv --ra ra_graph.tsv +``` diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/corpus.tsv b/.claude/probes/2026-11-11-codegraph-recon-1/corpus.tsv new file mode 100644 index 000000000..65701653f --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/corpus.tsv @@ -0,0 +1,445 @@ +id page page_line subject relation object rel_type status source_cited verified_line recoverable prover note +R001 03-dr-dt64-binding.md 3 lance-graph-dt64 is a member of lance-graph workspace DEPENDS IMPLEMENTED - Cargo.toml:24 (members list 2-50) MECHANICAL-SYNTAX cargo-metadata +R002 03-dr-dt64-binding.md 5 DT64 joins (without copying values) class(ClassId via ClassView) + route + frame + lane INVARIANT IMPLEMENTED - crates/lance-graph-dt64/src/lane.rs:153-165 (LaneBinding holds class,route,frame,lane addrs); crates/lance-graph-dt64/src/lib.rs:49-57 INTERPRETATION human-review +R003 03-dr-dt64-binding.md 12 lance-graph-dt64 holds no business value, evaluator or persistence path - INVARIANT IMPLEMENTED lib.rs:24-30 crates/lance-graph-dt64/src/lib.rs:26-30; crates/lance-graph-dt64/Cargo.toml:10 (only dep: lance-graph-contract) INTERPRETATION cargo-metadata dependency half is mechanical (no mask-risc/lance dep); 'no evaluator' is interpretation +R004 03-dr-dt64-binding.md 12 lance-graph-dt64 depends on lance-graph-contract (only) DEPENDS IMPLEMENTED - crates/lance-graph-dt64/Cargo.toml:10 MECHANICAL-SYNTAX cargo-metadata +R005 03-dr-dt64-binding.md 18 RouteLog and MapTable tick one shared VersionClock - INVARIANT IMPLEMENTED - CONTRADICTED(partial): sharing is opt-in only; crates/lance-graph-dt64/src/dr.rs:158-165,235,885 with_clock(shared clone); default RouteLog::new/MapTable::new own separate clocks crates/lance-graph-dt64/src/dr.rs:229-231,879-881 INTERPRETATION dt64-runtime-test unconditional wording on page; true only when constructed from clones of one clock (tests/dr.rs:535-536, dt64-lance lib.rs:218). BindStore owns its RouteLog (lib.rs:777) and has no MapTable +R006 03-dr-dt64-binding.md 23 Width DEFINES enum Width DEFINES IMPLEMENTED dr.rs:32-45 crates/lance-graph-dt64/src/dr.rs:32 MECHANICAL-SYNTAX syntax-index (#1999) +R007 03-dr-dt64-binding.md 25 Width VARIANT W64 VARIANT IMPLEMENTED dr.rs:32-45 crates/lance-graph-dt64/src/dr.rs:33 MECHANICAL-SYNTAX syntax-index (#1999) +R008 03-dr-dt64-binding.md 26 Width VARIANT W256 VARIANT IMPLEMENTED dr.rs:32-45 crates/lance-graph-dt64/src/dr.rs:34 MECHANICAL-SYNTAX syntax-index (#1999) +R009 03-dr-dt64-binding.md 27 Width DEFINES fn positions DEFINES IMPLEMENTED dr.rs:32-45 crates/lance-graph-dt64/src/dr.rs:38 MECHANICAL-SYNTAX syntax-index (#1999) +R010 03-dr-dt64-binding.md 29 Axis DEFINES struct Axis DEFINES IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:48 MECHANICAL-SYNTAX syntax-index (#1999) +R011 03-dr-dt64-binding.md 30 Axis FIELD tile: Width FIELD IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:49 MECHANICAL-SYNTAX syntax-index (#1999) +R012 03-dr-dt64-binding.md 31 Axis FIELD tiles: u32 FIELD IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:50 MECHANICAL-SYNTAX syntax-index (#1999) +R013 03-dr-dt64-binding.md 32 Axis DEFINES fn reserved DEFINES IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:59 MECHANICAL-SYNTAX syntax-index (#1999) +R014 03-dr-dt64-binding.md 33 Axis DEFINES fn for_survivors DEFINES IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:69 MECHANICAL-SYNTAX syntax-index (#1999) +R015 03-dr-dt64-binding.md 35 Extent DEFINES struct Extent DEFINES IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:97 MECHANICAL-SYNTAX syntax-index (#1999) +R016 03-dr-dt64-binding.md 36 Extent FIELD identity: Axis FIELD IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:98 MECHANICAL-SYNTAX syntax-index (#1999) +R017 03-dr-dt64-binding.md 37 Extent FIELD property: Axis FIELD IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:99 MECHANICAL-SYNTAX syntax-index (#1999) +R018 03-dr-dt64-binding.md 38 Extent FIELD predicate: Axis FIELD IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:101 MECHANICAL-SYNTAX syntax-index (#1999) +R019 03-dr-dt64-binding.md 39 Extent DEFINES fn reserved_cells DEFINES IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:128 MECHANICAL-SYNTAX syntax-index (#1999) +R020 03-dr-dt64-binding.md 40 Extent DEFINES fn tile_bytes DEFINES IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:135 MECHANICAL-SYNTAX syntax-index (#1999) +R021 03-dr-dt64-binding.md 42 VersionClock DEFINES struct VersionClock DEFINES IMPLEMENTED dr.rs:165-186 crates/lance-graph-dt64/src/dr.rs:167 MECHANICAL-SYNTAX syntax-index (#1999) cited range ends 2 lines short of fork() (185-187) +R022 03-dr-dt64-binding.md 43 VersionClock DEFINES fn current DEFINES IMPLEMENTED dr.rs:165-186 crates/lance-graph-dt64/src/dr.rs:175 MECHANICAL-SYNTAX syntax-index (#1999) +R023 03-dr-dt64-binding.md 44 VersionClock DEFINES fn tick DEFINES IMPLEMENTED dr.rs:165-186 crates/lance-graph-dt64/src/dr.rs:180 MECHANICAL-SYNTAX syntax-index (#1999) +R024 03-dr-dt64-binding.md 45 VersionClock DEFINES fn fork DEFINES IMPLEMENTED dr.rs:165-186 crates/lance-graph-dt64/src/dr.rs:185 MECHANICAL-SYNTAX syntax-index (#1999) +R025 03-dr-dt64-binding.md 47 RouteLog DEFINES struct RouteLog DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:210 MECHANICAL-SYNTAX syntax-index (#1999) +R026 03-dr-dt64-binding.md 48 RouteLog DEFINES fn route(position,class,identity) DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:255 MECHANICAL-SYNTAX syntax-index (#1999) +R027 03-dr-dt64-binding.md 49 RouteLog DEFINES fn check(position,class,identity) DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:268 MECHANICAL-SYNTAX syntax-index (#1999) +R028 03-dr-dt64-binding.md 50 RouteLog DEFINES fn retract(position) DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:281 MECHANICAL-SYNTAX syntax-index (#1999) +R029 03-dr-dt64-binding.md 51 RouteLog DEFINES fn routed_at(version,position) DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:296 MECHANICAL-SYNTAX syntax-index (#1999) +R030 03-dr-dt64-binding.md 52 RouteLog DEFINES fn claimed(class,extent,version) DEFINES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:319 MECHANICAL-SYNTAX syntax-index (#1999) +R031 03-dr-dt64-binding.md 54 RouteRefusal DEFINES enum RouteRefusal DEFINES IMPLEMENTED dr.rs:190-208 crates/lance-graph-dt64/src/dr.rs:192 MECHANICAL-SYNTAX syntax-index (#1999) +R032 03-dr-dt64-binding.md 56 RouteRefusal VARIANT OutsideReservation VARIANT IMPLEMENTED dr.rs:190-208 crates/lance-graph-dt64/src/dr.rs:194 MECHANICAL-SYNTAX syntax-index (#1999) +R033 03-dr-dt64-binding.md 57 RouteRefusal VARIANT FutureVersion VARIANT IMPLEMENTED dr.rs:190-208 crates/lance-graph-dt64/src/dr.rs:200 MECHANICAL-SYNTAX syntax-index (#1999) +R034 03-dr-dt64-binding.md 59 MapTable DEFINES struct MapTable DEFINES IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:871 MECHANICAL-SYNTAX syntax-index (#1999) +R035 03-dr-dt64-binding.md 60 MapTable DEFINES fn advance DEFINES IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:970 MECHANICAL-SYNTAX syntax-index (#1999) +R036 03-dr-dt64-binding.md 61 MapTable DEFINES fn advance_at DEFINES IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:997 MECHANICAL-SYNTAX syntax-index (#1999) +R037 03-dr-dt64-binding.md 62 MapTable RETURNS Frame (from seal()) RETURNS IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1045 MECHANICAL-SYNTAX syntax-index (#1999) +R038 03-dr-dt64-binding.md 63 MapTable RETURNS TileMap (from map(frame,tile)) RETURNS IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1057 MECHANICAL-SYNTAX syntax-index (#1999) actual return is Result; diagram elides the Result +R039 03-dr-dt64-binding.md 64 MapTable DEFINES fn diagnose_at(version,tile) DEFINES IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1075 MECHANICAL-SYNTAX syntax-index (#1999) +R040 03-dr-dt64-binding.md 66 LocalMap DEFINES struct LocalMap DEFINES IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:573 MECHANICAL-SYNTAX syntax-index (#1999) +R041 03-dr-dt64-binding.md 67 LocalMap DEFINES fn prepare(width,globals) DEFINES IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:586 MECHANICAL-SYNTAX syntax-index (#1999) +R042 03-dr-dt64-binding.md 68 LocalMap RETURNS u8 (from local(global)) RETURNS IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:622 MECHANICAL-SYNTAX syntax-index (#1999) actual: Result +R043 03-dr-dt64-binding.md 69 LocalMap RETURNS Option (from global(local)) RETURNS IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:631 MECHANICAL-SYNTAX syntax-index (#1999) Option +R044 03-dr-dt64-binding.md 71 MapRefusal DEFINES enum MapRefusal DEFINES IMPLEMENTED dr.rs:555-566 crates/lance-graph-dt64/src/dr.rs:557 MECHANICAL-SYNTAX syntax-index (#1999) +R045 03-dr-dt64-binding.md 73 MapRefusal VARIANT TooMany VARIANT IMPLEMENTED dr.rs:555-566 crates/lance-graph-dt64/src/dr.rs:559 MECHANICAL-SYNTAX syntax-index (#1999) +R046 03-dr-dt64-binding.md 74 MapRefusal VARIANT Duplicate VARIANT IMPLEMENTED dr.rs:555-566 crates/lance-graph-dt64/src/dr.rs:561 MECHANICAL-SYNTAX syntax-index (#1999) +R047 03-dr-dt64-binding.md 75 MapRefusal VARIANT Unmapped VARIANT IMPLEMENTED dr.rs:555-566 crates/lance-graph-dt64/src/dr.rs:563 MECHANICAL-SYNTAX syntax-index (#1999) +R048 03-dr-dt64-binding.md 76 MapRefusal VARIANT OutOfTile VARIANT IMPLEMENTED dr.rs:555-566 crates/lance-graph-dt64/src/dr.rs:565 MECHANICAL-SYNTAX syntax-index (#1999) +R049 03-dr-dt64-binding.md 78 Axis FIELD tile -> Width FIELD IMPLEMENTED dr.rs:47-95 crates/lance-graph-dt64/src/dr.rs:49 MECHANICAL-SYNTAX syntax-index (#1999) +R050 03-dr-dt64-binding.md 79 Extent FIELD identity, property, predicate -> Axis FIELD IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:98-101 MECHANICAL-SYNTAX syntax-index (#1999) +R051 03-dr-dt64-binding.md 80 RouteLog CALLS VersionClock::tick (ticks) CALLS IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:286 (RouteLog::push); field crates/lance-graph-dt64/src/dr.rs:214 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R052 03-dr-dt64-binding.md 81 MapTable CALLS VersionClock::tick (ticks) CALLS IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:976 (MapTable::advance -> self.frames.clock.tick()); crates/lance-graph-dt64/src/dr.rs:872 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R053 03-dr-dt64-binding.md 82 RouteLog::check REFUSES RouteRefusal::OutsideReservation REFUSES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:271 MECHANICAL-CALLGRAPH charon-codegraph +R054 03-dr-dt64-binding.md 82 RouteLog::routed_at REFUSES RouteRefusal::FutureVersion REFUSES IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:303 MECHANICAL-CALLGRAPH charon-codegraph +R055 03-dr-dt64-binding.md 83 LocalMap::prepare REFUSES MapRefusal::TooMany REFUSES IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:588 MECHANICAL-CALLGRAPH charon-codegraph +R056 03-dr-dt64-binding.md 83 LocalMap::prepare REFUSES MapRefusal::Duplicate REFUSES IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:595 MECHANICAL-CALLGRAPH charon-codegraph +R057 03-dr-dt64-binding.md 83 LocalMap::local REFUSES MapRefusal::Unmapped REFUSES IMPLEMENTED dr.rs:568-660 crates/lance-graph-dt64/src/dr.rs:627 MECHANICAL-CALLGRAPH charon-codegraph +R058 03-dr-dt64-binding.md 84 MapTable FIELD one TileLog (of LocalMaps) per tile FIELD IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:873 (tiles: BTreeMap); crates/lance-graph-dt64/src/dr.rs:721 (TileLog::append takes LocalMap) MECHANICAL-SYNTAX syntax-index (#1999) +R059 03-dr-dt64-binding.md 89 Width INVARIANT W64=64 positions, W256=256 positions INVARIANT IMPLEMENTED dr.rs:32-45 crates/lance-graph-dt64/src/dr.rs:38-43 INTERPRETATION dt64-runtime-test literal values live in a match body, not in a signature +R060 03-dr-dt64-binding.md 90 Extent.predicate INVARIANT is the axis for the class's methods INVARIANT IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:100-101 (doc comment) INTERPRETATION human-review +R061 03-dr-dt64-binding.md 90 RouteLog::claimed INVARIANT reservation costs nothing; only touched identity tiles count as claimed INVARIANT IMPLEMENTED dr.rs:97-140 crates/lance-graph-dt64/src/dr.rs:91-95,319-335 INTERPRETATION dt64-runtime-test +R062 03-dr-dt64-binding.md 91 RouteLog INVARIANT append-only; only routing versioned INVARIANT IMPLEMENTED dr.rs:208-336 crates/lance-graph-dt64/src/dr.rs:206-208,285-292 (no remove/update fn in impl RouteLog 228-336) INTERPRETATION dt64-runtime-test absence claim over a closed impl block; retract appends a None event +R063 03-dr-dt64-binding.md 92 MapTable INVARIANT changes only by appending; old frame replays layout in force when sealed INVARIANT IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:859-869,1057-1060,1016-1042 INTERPRETATION dt64-runtime-test +R064 03-dr-dt64-binding.md 93 MapTable::diagnose_at TAKES bare RouteVersion TAKES IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1075-1078 MECHANICAL-SYNTAX syntax-index (#1999) +R065 03-dr-dt64-binding.md 93 MapTable::diagnose_at RETURNS MapDiagnostic (not TileMap) RETURNS IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1079,831 MECHANICAL-SYNTAX syntax-index (#1999) +R066 03-dr-dt64-binding.md 93 MapDiagnostic INVARIANT is not executable; execution only via MapTable::map with a frame INVARIANT IMPLEMENTED dr.rs:860-1100 crates/lance-graph-dt64/src/dr.rs:1062-1074 (compile_fail doctest) INTERPRETATION dt64-runtime-test type-level, enforced by compile_fail doctest +R067 03-dr-dt64-binding.md 114 FrameRevisions DEFINES struct FrameRevisions DEFINES IMPLEMENTED dr.rs:355-365 crates/lance-graph-dt64/src/dr.rs:357 MECHANICAL-SYNTAX syntax-index (#1999) +R068 03-dr-dt64-binding.md 115 FrameRevisions FIELD source: u64 FIELD IMPLEMENTED dr.rs:355-365 crates/lance-graph-dt64/src/dr.rs:358 MECHANICAL-SYNTAX syntax-index (#1999) +R069 03-dr-dt64-binding.md 116 FrameRevisions FIELD relation_map: u64 FIELD IMPLEMENTED dr.rs:355-365 crates/lance-graph-dt64/src/dr.rs:359 MECHANICAL-SYNTAX syntax-index (#1999) +R070 03-dr-dt64-binding.md 117 FrameRevisions FIELD coordinates: u64 FIELD IMPLEMENTED dr.rs:355-365 crates/lance-graph-dt64/src/dr.rs:360 MECHANICAL-SYNTAX syntax-index (#1999) +R071 03-dr-dt64-binding.md 119 FrameStore DEFINES struct FrameStore DEFINES IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:379 MECHANICAL-SYNTAX syntax-index (#1999) +R072 03-dr-dt64-binding.md 120 FrameStore RETURNS Frame (seal()) RETURNS IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:414 MECHANICAL-SYNTAX syntax-index (#1999) +R073 03-dr-dt64-binding.md 121 FrameStore RETURNS RouteVersion (advance(revisions)) RETURNS IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:426 MECHANICAL-SYNTAX syntax-index (#1999) +R074 03-dr-dt64-binding.md 122 FrameStore RETURNS RouteVersion (issued(frame)) RETURNS IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:441 MECHANICAL-SYNTAX syntax-index (#1999) actual Result +R075 03-dr-dt64-binding.md 123 FrameStore DEFINES fn check(frame) DEFINES IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:462 MECHANICAL-SYNTAX syntax-index (#1999) +R076 03-dr-dt64-binding.md 125 Frame DEFINES struct Frame DEFINES IMPLEMENTED dr.rs:484-511 crates/lance-graph-dt64/src/dr.rs:486 MECHANICAL-SYNTAX syntax-index (#1999) +R077 03-dr-dt64-binding.md 126 Frame RETURNS RouteVersion (version()) RETURNS IMPLEMENTED dr.rs:484-511 crates/lance-graph-dt64/src/dr.rs:495 MECHANICAL-SYNTAX syntax-index (#1999) +R078 03-dr-dt64-binding.md 127 Frame RETURNS FrameRevisions (revisions()) RETURNS IMPLEMENTED dr.rs:484-511 crates/lance-graph-dt64/src/dr.rs:500 MECHANICAL-SYNTAX syntax-index (#1999) +R079 03-dr-dt64-binding.md 128 Frame DEFINES fn same_issue(other) DEFINES IMPLEMENTED dr.rs:484-511 crates/lance-graph-dt64/src/dr.rs:505 MECHANICAL-SYNTAX syntax-index (#1999) +R080 03-dr-dt64-binding.md 130 FrameRefusal DEFINES enum FrameRefusal DEFINES IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:365 MECHANICAL-SYNTAX syntax-index (#1999) +R081 03-dr-dt64-binding.md 132 FrameRefusal VARIANT ForeignFrame VARIANT IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:367 MECHANICAL-SYNTAX syntax-index (#1999) +R082 03-dr-dt64-binding.md 133 FrameRefusal VARIANT SourceChanged VARIANT IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:368 MECHANICAL-SYNTAX syntax-index (#1999) +R083 03-dr-dt64-binding.md 134 FrameRefusal VARIANT MapChanged VARIANT IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:369 MECHANICAL-SYNTAX syntax-index (#1999) +R084 03-dr-dt64-binding.md 135 FrameRefusal VARIANT CoordinatesChanged VARIANT IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:370 MECHANICAL-SYNTAX syntax-index (#1999) +R085 03-dr-dt64-binding.md 136 FrameRefusal VARIANT FrameResealed VARIANT IMPLEMENTED dr.rs:365-378 crates/lance-graph-dt64/src/dr.rs:372 MECHANICAL-SYNTAX syntax-index (#1999) +R086 03-dr-dt64-binding.md 138 Focus DEFINES struct Focus DEFINES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:513 MECHANICAL-SYNTAX syntax-index (#1999) +R087 03-dr-dt64-binding.md 139 Focus FIELD revision: u64 FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:514 MECHANICAL-SYNTAX syntax-index (#1999) +R088 03-dr-dt64-binding.md 141 Scope DEFINES struct Scope DEFINES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:520 MECHANICAL-SYNTAX syntax-index (#1999) +R089 03-dr-dt64-binding.md 142 Scope FIELD id: u64 FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:521 MECHANICAL-SYNTAX syntax-index (#1999) +R090 03-dr-dt64-binding.md 144 Guards DEFINES struct Guards DEFINES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:526 MECHANICAL-SYNTAX syntax-index (#1999) +R091 03-dr-dt64-binding.md 145 Guards FIELD frame: Frame FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:527 MECHANICAL-SYNTAX syntax-index (#1999) +R092 03-dr-dt64-binding.md 146 Guards FIELD focus: Focus FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:528 MECHANICAL-SYNTAX syntax-index (#1999) +R093 03-dr-dt64-binding.md 147 Guards FIELD scope: Scope FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:529 MECHANICAL-SYNTAX syntax-index (#1999) +R094 03-dr-dt64-binding.md 148 Guards DEFINES fn check(store, now) DEFINES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:543 MECHANICAL-SYNTAX syntax-index (#1999) +R095 03-dr-dt64-binding.md 150 GuardRefusal DEFINES enum GuardRefusal DEFINES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:534 MECHANICAL-SYNTAX syntax-index (#1999) +R096 03-dr-dt64-binding.md 152 GuardRefusal VARIANT Frame(FrameRefusal) VARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:535 MECHANICAL-SYNTAX syntax-index (#1999) +R097 03-dr-dt64-binding.md 153 GuardRefusal VARIANT FocusChanged VARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:536 MECHANICAL-SYNTAX syntax-index (#1999) +R098 03-dr-dt64-binding.md 154 GuardRefusal VARIANT ScopeChanged VARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:537 MECHANICAL-SYNTAX syntax-index (#1999) +R099 03-dr-dt64-binding.md 156 FrameStore FIELD current: FrameRevisions FIELD IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:381 MECHANICAL-SYNTAX syntax-index (#1999) +R100 03-dr-dt64-binding.md 157 FrameStore RETURNS Frame (issues; no public ctor) RETURNS IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:414; Frame fields private crates/lance-graph-dt64/src/dr.rs:487-490; impl Frame has only version/revisions/same_issue crates/lance-graph-dt64/src/dr.rs:493-508 MECHANICAL-SYNTAX syntax-index (#1999) also asserts L168 'Frame has no public constructor' (negative; needs whole-crate scan of pub fns returning Frame; MapTable::seal delegates to FrameStore::seal :1045-1046) +R101 03-dr-dt64-binding.md 158 FrameStore::check REFUSES FrameRefusal (all five variants) REFUSES IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:462-478 (ForeignFrame 464; Source 471; Map 473; Coordinates 475; Resealed 477) MECHANICAL-CALLGRAPH charon-codegraph +R102 03-dr-dt64-binding.md 159 Guards FIELD frame: Frame FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:527 MECHANICAL-SYNTAX syntax-index (#1999) +R103 03-dr-dt64-binding.md 160 Guards FIELD focus: Focus FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:528 MECHANICAL-SYNTAX syntax-index (#1999) +R104 03-dr-dt64-binding.md 161 Guards FIELD scope: Scope FIELD IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:529 MECHANICAL-SYNTAX syntax-index (#1999) +R105 03-dr-dt64-binding.md 162 Guards::check REFUSES GuardRefusal (Frame via store.check, FocusChanged, ScopeChanged) REFUSES IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:544,546,549 MECHANICAL-CALLGRAPH charon-codegraph +R106 03-dr-dt64-binding.md 163 GuardRefusal VARIANT Frame carries FrameRefusal VARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:535 MECHANICAL-SYNTAX syntax-index (#1999) +R107 03-dr-dt64-binding.md 169 FrameStore::check INVARIANT accepts only the store's current seal; foreign frame is ForeignFrame even at equal numbers INVARIANT IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:459-468 INTERPRETATION dt64-runtime-test +R108 03-dr-dt64-binding.md 169 FrameStore::check SEQUENCE stale frame names FIRST moved revision (source, map, coordinates) else FrameResealed SEQUENCE IMPLEMENTED dr.rs:379-484 crates/lance-graph-dt64/src/dr.rs:469-478 MECHANICAL-CALLGRAPH charon-codegraph +R109 03-dr-dt64-binding.md 170 Focus INVARIANT is motion not reference: new focus over same frame is not a new frame INVARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:510-511 (doc comment); Frame identity excludes focus crates/lance-graph-dt64/src/dr.rs:505-507 INTERPRETATION human-review +R110 03-dr-dt64-binding.md 171 Scope INVARIANT opaque u64 id; DT64 compares ids and does not decide who may read INVARIANT IMPLEMENTED dr.rs:513-555 crates/lance-graph-dt64/src/dr.rs:517-522,548 (Guards::check compares scope != now.1) INTERPRETATION human-review compare-only half is visible in Guards::check; 'does not decide who may read' is absence of any rbac dependency (Cargo.toml:10) +R111 03-dr-dt64-binding.md 188 ClassView DEFINES trait ClassView (contract) DEFINES IMPLEMENTED class_view.rs:1057-1120 crates/lance-graph-contract/src/class_view.rs:1057 MECHANICAL-SYNTAX syntax-index (#1999) +R112 03-dr-dt64-binding.md 190 ClassView DEFINES fn fields(class) DEFINES IMPLEMENTED class_view.rs:1057-1120 crates/lance-graph-contract/src/class_view.rs:1061 MECHANICAL-SYNTAX syntax-index (#1999) +R113 03-dr-dt64-binding.md 191 ClassView DEFINES fn fields_at(class,rev) DEFINES IMPLEMENTED class_view.rs:1057-1120 crates/lance-graph-contract/src/class_view.rs:1105 MECHANICAL-SYNTAX syntax-index (#1999) +R114 03-dr-dt64-binding.md 192 ClassView DEFINES fn lens_fields(lens) DEFINES IMPLEMENTED class_view.rs:1057-1120 crates/lance-graph-contract/src/class_view.rs:1084 MECHANICAL-SYNTAX syntax-index (#1999) +R115 03-dr-dt64-binding.md 194 ClassSchema DEFINES struct ClassSchema DEFINES IMPLEMENTED lib.rs:253-262 crates/lance-graph-dt64/src/lib.rs:254 MECHANICAL-SYNTAX syntax-index (#1999) cited range 253-262 vs actual struct 249-258 (drift 4) +R116 03-dr-dt64-binding.md 195 ClassSchema FIELD schema_rev: SchemaRev FIELD IMPLEMENTED lib.rs:253-262 crates/lance-graph-dt64/src/lib.rs:255 MECHANICAL-SYNTAX syntax-index (#1999) +R117 03-dr-dt64-binding.md 196 ClassSchema FIELD field_count: usize FIELD IMPLEMENTED lib.rs:253-262 crates/lance-graph-dt64/src/lib.rs:256 MECHANICAL-SYNTAX syntax-index (#1999) +R118 03-dr-dt64-binding.md 197 ClassSchema FIELD extent: Extent FIELD IMPLEMENTED lib.rs:253-262 crates/lance-graph-dt64/src/lib.rs:257 MECHANICAL-SYNTAX syntax-index (#1999) +R119 03-dr-dt64-binding.md 199 MethodBinding DEFINES struct MethodBinding DEFINES IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:215 MECHANICAL-SYNTAX syntax-index (#1999) +R120 03-dr-dt64-binding.md 200 MethodBinding FIELD id: MethodId FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:216 MECHANICAL-SYNTAX syntax-index (#1999) +R121 03-dr-dt64-binding.md 201 MethodBinding FIELD sig_rev: SigRev FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:217 MECHANICAL-SYNTAX syntax-index (#1999) +R122 03-dr-dt64-binding.md 202 MethodBinding FIELD on: WideFieldMask FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:222 MECHANICAL-SYNTAX syntax-index (#1999) +R123 03-dr-dt64-binding.md 203 MethodBinding FIELD when: Option FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:224 MECHANICAL-SYNTAX syntax-index (#1999) +R124 03-dr-dt64-binding.md 204 MethodBinding FIELD reads: WideFieldMask FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:225 MECHANICAL-SYNTAX syntax-index (#1999) +R125 03-dr-dt64-binding.md 205 MethodBinding FIELD effects: Vec FIELD IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:227 MECHANICAL-SYNTAX syntax-index (#1999) +R126 03-dr-dt64-binding.md 207 BindStore DEFINES struct BindStore DEFINES IMPLEMENTED lib.rs:772-795 crates/lance-graph-dt64/src/lib.rs:772 MECHANICAL-SYNTAX syntax-index (#1999) +R127 03-dr-dt64-binding.md 208 BindStore DEFINES fn register(view,class,schema,methods) DEFINES IMPLEMENTED lib.rs:772-795 crates/lance-graph-dt64/src/lib.rs:814 MECHANICAL-SYNTAX syntax-index (#1999) +R128 03-dr-dt64-binding.md 209 BindStore DEFINES fn route(position,class) DEFINES IMPLEMENTED lib.rs:772-795 crates/lance-graph-dt64/src/lib.rs:1018 MECHANICAL-SYNTAX syntax-index (#1999) +R129 03-dr-dt64-binding.md 210 BindStore RETURNS Resolved (resolve(view,class,rev)) RETURNS IMPLEMENTED lib.rs:1073-1095 crates/lance-graph-dt64/src/lib.rs:1073-1078 MECHANICAL-SYNTAX syntax-index (#1999) +R130 03-dr-dt64-binding.md 211 BindStore RETURNS MethodRef (method_ref(class,method)) RETURNS IMPLEMENTED lib.rs:1136-1160 crates/lance-graph-dt64/src/lib.rs:1136 MECHANICAL-SYNTAX syntax-index (#1999) +R131 03-dr-dt64-binding.md 212 BindStore RETURNS MethodBinding (admit(method_ref)) RETURNS IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1180 MECHANICAL-SYNTAX syntax-index (#1999) +R132 03-dr-dt64-binding.md 213 BindStore DEFINES fn bind_lanes(view,frames,source,request) DEFINES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:171 MECHANICAL-SYNTAX syntax-index (#1999) +R133 03-dr-dt64-binding.md 215 Resolved DEFINES struct Resolved DEFINES IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:646 MECHANICAL-SYNTAX syntax-index (#1999) +R134 03-dr-dt64-binding.md 216 Resolved DEFINES fn field_view(mask) DEFINES IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:683 MECHANICAL-SYNTAX syntax-index (#1999) +R135 03-dr-dt64-binding.md 217 Resolved DEFINES fn field_meaning(mask,schema) DEFINES IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:700 MECHANICAL-SYNTAX syntax-index (#1999) +R136 03-dr-dt64-binding.md 218 Resolved DEFINES fn mask_where(schema,pred) DEFINES IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:719 MECHANICAL-SYNTAX syntax-index (#1999) +R137 03-dr-dt64-binding.md 219 Resolved DEFINES fn action_ordinals() DEFINES IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:760 MECHANICAL-SYNTAX syntax-index (#1999) +R138 03-dr-dt64-binding.md 221 LaneSource DEFINES trait LaneSource DEFINES IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:51 MECHANICAL-SYNTAX syntax-index (#1999) +R139 03-dr-dt64-binding.md 223 LaneSource DEFINES fn lane_of(class,rev,field,basis,frame) DEFINES IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:57 MECHANICAL-SYNTAX syntax-index (#1999) +R140 03-dr-dt64-binding.md 224 LaneSource DEFINES fn borrow(addr) DEFINES IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:66 MECHANICAL-SYNTAX syntax-index (#1999) +R141 03-dr-dt64-binding.md 225 LaneSource RETURNS FrameStore (frames()) RETURNS IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:79 MECHANICAL-SYNTAX syntax-index (#1999) +R142 03-dr-dt64-binding.md 227 LaneAddr DEFINES struct LaneAddr DEFINES IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:36 MECHANICAL-SYNTAX syntax-index (#1999) +R143 03-dr-dt64-binding.md 228 LaneAddr FIELD space: CoordSpace FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:37 MECHANICAL-SYNTAX syntax-index (#1999) +R144 03-dr-dt64-binding.md 229 LaneAddr FIELD lane: u16 FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:38 MECHANICAL-SYNTAX syntax-index (#1999) +R145 03-dr-dt64-binding.md 230 LaneAddr FIELD scope: Scope FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:39 MECHANICAL-SYNTAX syntax-index (#1999) +R146 03-dr-dt64-binding.md 232 LaneRequest DEFINES struct LaneRequest DEFINES IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:91 MECHANICAL-SYNTAX syntax-index (#1999) +R147 03-dr-dt64-binding.md 233 LaneRequest FIELD route: RouteAt FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:92 MECHANICAL-SYNTAX syntax-index (#1999) +R148 03-dr-dt64-binding.md 234 LaneRequest FIELD rev: SchemaRev FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:93 MECHANICAL-SYNTAX syntax-index (#1999) +R149 03-dr-dt64-binding.md 235 LaneRequest FIELD fields: WideFieldMask FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:94 MECHANICAL-SYNTAX syntax-index (#1999) +R150 03-dr-dt64-binding.md 236 LaneRequest FIELD frame: Frame FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:95 MECHANICAL-SYNTAX syntax-index (#1999) +R151 03-dr-dt64-binding.md 237 LaneRequest FIELD scope: Scope FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:97 MECHANICAL-SYNTAX syntax-index (#1999) +R152 03-dr-dt64-binding.md 238 LaneRequest FIELD selection: CoordSpace FIELD IMPLEMENTED lane.rs:26-142 crates/lance-graph-dt64/src/lane.rs:99 MECHANICAL-SYNTAX syntax-index (#1999) +R153 03-dr-dt64-binding.md 240 LaneBinding DEFINES struct LaneBinding DEFINES IMPLEMENTED lane.rs:151-165 crates/lance-graph-dt64/src/lane.rs:153 MECHANICAL-SYNTAX syntax-index (#1999) +R154 03-dr-dt64-binding.md 241 LaneBinding DEFINES fn addr(field) DEFINES IMPLEMENTED lane.rs:264-396 crates/lance-graph-dt64/src/lane.rs:292 MECHANICAL-SYNTAX syntax-index (#1999) +R155 03-dr-dt64-binding.md 242 LaneBinding DEFINES fn check(store,view,frames,source) DEFINES IMPLEMENTED lane.rs:264-396 crates/lance-graph-dt64/src/lane.rs:307 MECHANICAL-SYNTAX syntax-index (#1999) +R156 03-dr-dt64-binding.md 243 LaneBinding DEFINES fn lane(store,view,frames,source,field) DEFINES IMPLEMENTED lane.rs:264-396 crates/lance-graph-dt64/src/lane.rs:352 MECHANICAL-SYNTAX syntax-index (#1999) +R157 03-dr-dt64-binding.md 244 LaneBinding DEFINES fn borrow_all(store,view,frames,source) DEFINES IMPLEMENTED lane.rs:264-396 crates/lance-graph-dt64/src/lane.rs:379 MECHANICAL-SYNTAX syntax-index (#1999) +R158 03-dr-dt64-binding.md 246 BindStore FIELD ClassSchema per class (via ClassEntry) FIELD IMPLEMENTED lib.rs:772-795 crates/lance-graph-dt64/src/lib.rs:773 (classes: BTreeMap); ClassEntry.schema built crates/lance-graph-dt64/src/lib.rs:897-903 MECHANICAL-SYNTAX syntax-index (#1999) indirect: BindStore -> ClassEntry -> ClassSchema +R159 03-dr-dt64-binding.md 247 BindStore FIELD MethodBinding per method (via ClassEntry.methods) FIELD IMPLEMENTED lib.rs:772-795 crates/lance-graph-dt64/src/lib.rs:899 (ClassEntry{methods}) MECHANICAL-SYNTAX syntax-index (#1999) indirect +R160 03-dr-dt64-binding.md 248 BindStore CALLS ClassView::fields_at / fields / lens_fields(_at) (reads basis through) CALLS IMPLEMENTED lib.rs:1220-1245 crates/lance-graph-dt64/src/lib.rs:1283-1285 (basis_at); called from insert crates/lance-graph-dt64/src/lib.rs:871 and resolve->check_basis crates/lance-graph-dt64/src/lib.rs:1083,1234 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R161 03-dr-dt64-binding.md 249 BindStore::resolve RETURNS Resolved RETURNS IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:1078 MECHANICAL-SYNTAX syntax-index (#1999) +R162 03-dr-dt64-binding.md 250 BindStore::bind_lanes RETURNS LaneBinding RETURNS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:177 MECHANICAL-SYNTAX syntax-index (#1999) +R163 03-dr-dt64-binding.md 251 BindStore::bind_lanes TAKES LaneRequest TAKES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:176 MECHANICAL-SYNTAX syntax-index (#1999) +R164 03-dr-dt64-binding.md 252 LaneBinding FIELD one LaneAddr per field FIELD IMPLEMENTED lane.rs:151-165 crates/lance-graph-dt64/src/lane.rs:161 (lanes: Vec<(u8, LaneAddr)>) MECHANICAL-SYNTAX syntax-index (#1999) +R165 03-dr-dt64-binding.md 253 LaneBinding CALLS LaneSource::lane_of / borrow (asks and borrows) CALLS IMPLEMENTED lane.rs:264-396 crates/lance-graph-dt64/src/lane.rs:336 (check->lane_of); crates/lance-graph-dt64/src/lane.rs:362 (lane->borrow); crates/lance-graph-dt64/src/lane.rs:409 (BoundLanes::next->borrow) MECHANICAL-CALLGRAPH kythe/rust-analyzer +R166 03-dr-dt64-binding.md 258 MethodBinding INVARIANT is ON x WHEN x DO (on = trigger mask, when = optional guard, effects = ordered DO list) INVARIANT IMPLEMENTED lib.rs:213-251 crates/lance-graph-dt64/src/lib.rs:212-213,221-227 INTERPRETATION human-review +R167 03-dr-dt64-binding.md 259 BindStore::method_ref CALLS stamps MethodRef with store identity (Stamp.issuer = Arc::downgrade(identity)) CALLS IMPLEMENTED lib.rs:1136-1160 crates/lance-graph-dt64/src/lib.rs:1147-1155 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R168 03-dr-dt64-binding.md 259 BindStore::admit REFUSES SignatureRevisionMismatch REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1193 MECHANICAL-CALLGRAPH charon-codegraph +R169 03-dr-dt64-binding.md 259 BindStore::admit REFUSES GuardDropped REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1202 MECHANICAL-CALLGRAPH charon-codegraph +R170 03-dr-dt64-binding.md 259 BindStore::admit REFUSES GuardAdded REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1203 MECHANICAL-CALLGRAPH charon-codegraph +R171 03-dr-dt64-binding.md 259 BindStore::admit REFUSES GuardMismatch REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1205 MECHANICAL-CALLGRAPH charon-codegraph +R172 03-dr-dt64-binding.md 259 BindStore::admit REFUSES BindingMismatch REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1208 MECHANICAL-CALLGRAPH charon-codegraph +R173 03-dr-dt64-binding.md 259 BindStore::admit REFUSES ForeignStore (via check_issuer) REFUSES IMPLEMENTED lib.rs:1180-1215 crates/lance-graph-dt64/src/lib.rs:1210 -> crates/lance-graph-dt64/src/lib.rs:1165 MECHANICAL-CALLGRAPH charon-codegraph page's list omits UnknownClass (1184) and UnknownMethod (1190), which admit also returns +R174 03-dr-dt64-binding.md 260 Resolved INVARIANT is an answer, not a witness (public fields; hand-built proves nothing) INVARIANT IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:638-652 INTERPRETATION human-review +R175 03-dr-dt64-binding.md 260 Resolved::field_meaning CALLS PropertySchema::get(row.predicate) -> PropertySpec (joined by predicate) CALLS IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:709-712 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R176 03-dr-dt64-binding.md 261 PropertySpec FIELD marking: Marking FIELD IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:58 MECHANICAL-SYNTAX syntax-index (#1999) +R177 03-dr-dt64-binding.md 261 Marking VARIANT Public VARIANT IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:773 MECHANICAL-SYNTAX syntax-index (#1999) +R178 03-dr-dt64-binding.md 261 Marking VARIANT Internal VARIANT IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:776 MECHANICAL-SYNTAX syntax-index (#1999) +R179 03-dr-dt64-binding.md 261 Marking VARIANT Pii VARIANT IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:778 MECHANICAL-SYNTAX syntax-index (#1999) +R180 03-dr-dt64-binding.md 261 Marking VARIANT Financial VARIANT IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:780 MECHANICAL-SYNTAX syntax-index (#1999) +R181 03-dr-dt64-binding.md 261 Marking VARIANT Restricted VARIANT IMPLEMENTED property.rs:769-783 crates/lance-graph-contract/src/property.rs:782 MECHANICAL-SYNTAX syntax-index (#1999) +R182 03-dr-dt64-binding.md 261 Resolved::mask_where INVARIANT a field with no spec is never selected INVARIANT IMPLEMENTED lib.rs:640-770 crates/lance-graph-dt64/src/lib.rs:717-718,724 (schema.get(..).is_some_and(pred)) INTERPRETATION dt64-runtime-test body-level behaviour +R183 03-dr-dt64-binding.md 262 LaneBinding INVARIANT holds addresses only, never a value INVARIANT IMPLEMENTED lane.rs:151-165 crates/lance-graph-dt64/src/lane.rs:150-165 (fields: class,rev,route,frame,scope,selection,fields mask,lanes of LaneAddr,basis digest) INTERPRETATION human-review field types are mechanical; 'never a value' is a closed-world reading of them +R184 03-dr-dt64-binding.md 292 Caller CALLS BindStore::bind_lanes(view,frames,source,request) CALLS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:171 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R185 03-dr-dt64-binding.md 293 BindStore::bind_lanes CALLS source_owns -> FrameStore::same_store(source.frames()) CALLS IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:178,220-226 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R186 03-dr-dt64-binding.md 293 BindStore::bind_lanes SEQUENCE order: source_owns, frame check, route lookup, current_route, resolve, then per-field (basis, lane_of, coord space, scope) SEQUENCE IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:178-203 MECHANICAL-CALLGRAPH charon-codegraph spans L293-L327 of the diagram +R187 03-dr-dt64-binding.md 294 BindStore::bind_lanes REFUSES Frame(ForeignFrame) when frames is not the source store REFUSES IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:224 MECHANICAL-CALLGRAPH charon-codegraph +R188 03-dr-dt64-binding.md 297 BindStore::bind_lanes CALLS FrameStore::check(request.frame) CALLS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:179 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R189 03-dr-dt64-binding.md 298 BindStore::bind_lanes REFUSES Frame(SourceChanged|MapChanged|CoordinatesChanged|FrameResealed) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:179 via crates/lance-graph-dt64/src/dr.rs:470-477 MECHANICAL-CALLGRAPH charon-codegraph +R190 03-dr-dt64-binding.md 301 BindStore::bind_lanes CALLS routed_at(route.version, position) CALLS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:181 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R191 03-dr-dt64-binding.md 302 BindStore::bind_lanes REFUSES Bind(Unrouted) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:182-185 MECHANICAL-CALLGRAPH charon-codegraph +R192 03-dr-dt64-binding.md 302 BindStore::bind_lanes REFUSES Bind(FutureVersion) (from routed_at) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:181 via crates/lance-graph-dt64/src/lib.rs:631-633,1069 MECHANICAL-CALLGRAPH charon-codegraph +R193 03-dr-dt64-binding.md 305 BindStore::bind_lanes CALLS current_route: route at current version equals bound class CALLS IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:186,229-240 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R194 03-dr-dt64-binding.md 306 BindStore::bind_lanes REFUSES RouteChanged REFUSES IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:234 MECHANICAL-CALLGRAPH charon-codegraph +R195 03-dr-dt64-binding.md 309 BindStore::bind_lanes CALLS BindStore::resolve(class, rev) which reads field basis from ClassView CALLS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:187; crates/lance-graph-dt64/src/lib.rs:1083 -> check_basis crates/lance-graph-dt64/src/lib.rs:1234 -> basis_at crates/lance-graph-dt64/src/lib.rs:1283-1285 MECHANICAL-CALLGRAPH kythe/rust-analyzer LABEL-IMPRECISE: arrow B->V is labelled resolve but resolve is BindStore's own method (self-call); ClassView receives fields_at/fields/lens_fields +R196 03-dr-dt64-binding.md 310 BindStore::resolve REFUSES Bind(UnknownClass) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lib.rs:1082 MECHANICAL-CALLGRAPH charon-codegraph +R197 03-dr-dt64-binding.md 310 BindStore::resolve REFUSES Bind(SchemaRevisionMismatch) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lib.rs:1228 MECHANICAL-CALLGRAPH charon-codegraph +R198 03-dr-dt64-binding.md 310 BindStore::resolve REFUSES Bind(PredicateBasisChanged) REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lib.rs:1238 MECHANICAL-CALLGRAPH charon-codegraph +R199 03-dr-dt64-binding.md 313 BindStore::bind_lanes SEQUENCE loops over each requested field in ascending order 0..=255 SEQUENCE IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:192-204 MECHANICAL-CALLGRAPH charon-codegraph +R200 03-dr-dt64-binding.md 314 BindStore::bind_lanes REFUSES FieldNotInBasis REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:196-198 MECHANICAL-CALLGRAPH charon-codegraph +R201 03-dr-dt64-binding.md 317 BindStore::bind_lanes CALLS LaneSource::lane_of(class,rev,field,basis,frame) CALLS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:199-200 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R202 03-dr-dt64-binding.md 318 BindStore::bind_lanes REFUSES Unbound REFUSES IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:201 MECHANICAL-CALLGRAPH charon-codegraph +R203 03-dr-dt64-binding.md 321 BindStore::bind_lanes REFUSES CoordinateSpace (via admit_lane) REFUSES IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:202 -> crates/lance-graph-dt64/src/lane.rs:248-253 MECHANICAL-CALLGRAPH charon-codegraph +R204 03-dr-dt64-binding.md 324 BindStore::bind_lanes REFUSES Scope (via admit_lane) REFUSES IMPLEMENTED lane.rs:220-263 crates/lance-graph-dt64/src/lane.rs:202 -> crates/lance-graph-dt64/src/lane.rs:255-260 MECHANICAL-CALLGRAPH charon-codegraph +R205 03-dr-dt64-binding.md 328 BindStore::bind_lanes RETURNS LaneBinding with addresses only RETURNS IMPLEMENTED lane.rs:171-217 crates/lance-graph-dt64/src/lane.rs:205-215 MECHANICAL-SYNTAX syntax-index (#1999) +R206 03-dr-dt64-binding.md 330 Caller CALLS LaneBinding::borrow_all(store,view,frames,source) CALLS IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:379 MECHANICAL-CALLGRAPH kythe/rust-analyzer LABEL-IMPRECISE: diagram routes this message to participant BindStore; borrow_all is a LaneBinding method taking the store as an argument +R207 03-dr-dt64-binding.md 331 LaneBinding::borrow_all CALLS LaneBinding::check once (frame, route, basis digest, every lane again) CALLS IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:386; check body crates/lance-graph-dt64/src/lane.rs:314-347 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R208 03-dr-dt64-binding.md 331 LaneBinding::check SEQUENCE source_owns, frame check, current_route, resolve_counted + basis-witness compare, then per-lane lane_of + admit_lane SEQUENCE IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:314-347 MECHANICAL-CALLGRAPH charon-codegraph +R209 03-dr-dt64-binding.md 332 LaneBinding::check REFUSES StoreBasisMismatch REFUSES IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:326 MECHANICAL-CALLGRAPH charon-codegraph +R210 03-dr-dt64-binding.md 335 LaneBinding::check REFUSES MappingChanged REFUSES IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:338 MECHANICAL-CALLGRAPH charon-codegraph +R211 03-dr-dt64-binding.md 338 LaneBinding::borrow_all RETURNS BoundLanes iterator in ascending field order RETURNS IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:385-390 MECHANICAL-SYNTAX syntax-index (#1999) 'ascending' follows from bind_lanes' 0..=255 loop pushing in order (crates/lance-graph-dt64/src/lane.rs:192-203) and borrow_all doc crates/lance-graph-dt64/src/lane.rs:365-366 +R212 03-dr-dt64-binding.md 339 BoundLanes::next CALLS LaneSource::borrow(addr) per lane CALLS IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:409 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R213 03-dr-dt64-binding.md 341 BoundLanes::next REFUSES Err(Vanished) at that field, iteration continues REFUSES IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:411 (item type 402; next 404-413) MECHANICAL-CALLGRAPH charon-codegraph LABEL-IMPRECISE: diagram draws it as S-->>C; it is produced by the iterator when source.borrow returns None +R214 03-dr-dt64-binding.md 349 LaneBinding::borrow_all INVARIANT every refusal fires before any lane is borrowed; N lanes cost N source lookups, not N^2 INVARIANT IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:365-375,386 INTERPRETATION dt64-runtime-test ordering is visible; cost bound needs counting source lookups +R215 03-dr-dt64-binding.md 350 LaneBinding::lane CALLS LaneBinding::check on every call CALLS IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:360 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R216 03-dr-dt64-binding.md 350 LaneBinding::lane REFUSES NotBound for a field outside the binding REFUSES IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:361 MECHANICAL-CALLGRAPH charon-codegraph +R217 03-dr-dt64-binding.md 351 LaneBinding::check INVARIANT does not re-hash basis: compares u128 witness, revision and field count INVARIANT IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:296-306,324-327 INTERPRETATION dt64-runtime-test +R218 03-dr-dt64-binding.md 351 LaneBinding::check INVARIANT same-count basis reorder after bind caught only when source maps lanes by predicate INVARIANT IMPLEMENTED lane.rs:297-350 crates/lance-graph-dt64/src/lane.rs:303-306 (documented limitation) INTERPRETATION human-review +R219 03-dr-dt64-binding.md 352 BoundLanes INVARIANT Vanished is yielded per lane and the iterator carries on INVARIANT IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:373-375,404-412 INTERPRETATION dt64-runtime-test +R220 03-dr-dt64-binding.md 353 LaneBinding::borrow_all INVARIANT returned lanes are as current as the check; no lock held on the source INVARIANT IMPLEMENTED lane.rs:352-418 crates/lance-graph-dt64/src/lane.rs:377-378 (doc) INTERPRETATION human-review +R221 03-dr-dt64-binding.md 370 DT64 INVARIANT does not decide who may read; Scope is an id the source stamps on a lane INVARIANT IMPLEMENTED lib.rs:24-30 crates/lance-graph-dt64/src/lane.rs:33-40 (LaneAddr.scope), crates/lance-graph-dt64/src/dr.rs:517-522; crates/lance-graph-dt64/Cargo.toml:10 INTERPRETATION cargo-metadata no rbac dependency is mechanical; 'does not decide' is interpretation +R222 03-dr-dt64-binding.md 371 DT64 INVARIANT does not evaluate anything; evaluation belongs to mask-risc INVARIANT IMPLEMENTED lib.rs:24-30 crates/lance-graph-dt64/src/lib.rs:16,30; mask-risc executes: crates/lance-graph-mask-risc/src/exec.rs:1343 INTERPRETATION cargo-metadata +R223 03-dr-dt64-binding.md 372 DT64 INVARIANT does not persist anything; keeps bindings and route log only INVARIANT IMPLEMENTED lib.rs:24-30 crates/lance-graph-dt64/src/lib.rs:26-30 INTERPRETATION cargo-metadata dt64 has no lance/arrow/io dependency (Cargo.toml:10); persistence is in separate crate lance-graph-dt64-lance (workspace exclude, Cargo.toml:182) +R224 05-methods.md 5 DT64 INVARIANT keeps the binding and executes nothing INVARIANT IMPLEMENTED lib.rs:1-27 crates/lance-graph-dt64/src/lib.rs:4,16,30 (module doc); crates/lance-graph-dt64/Cargo.toml:10 (no mask-risc dep) INTERPRETATION cargo-metadata +R225 05-methods.md 6 WHEN (relalg+mask-risc lab) and DO (r2il) INVARIANT are run by other crates, separately INVARIANT IMPLEMENTED - WHEN: crates/foundry-parity-lab/src/method.rs:200-292; DO: crates/lance-graph-r2il/src/binding.rs:321-365; MethodBinding.effects empty in lab crates/foundry-parity-lab/src/method.rs:89 INTERPRETATION human-review +R226 05-methods.md 22 MethodBinding FIELD id, sig_rev, on, when(Guard), reads, effects FIELD IMPLEMENTED lib.rs:215-231 crates/lance-graph-dt64/src/lib.rs:216-227 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L199-205 FIELD rows +R227 05-methods.md 23 BindStore::register CALLS insert -> validate (unique MethodIds, basis fits extent) CALLS IMPLEMENTED lib.rs:814-823 crates/lance-graph-dt64/src/lib.rs:821 -> crates/lance-graph-dt64/src/lib.rs:851 -> crates/lance-graph-dt64/src/lib.rs:1346-1351 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R228 05-methods.md 23 BindStore::register REFUSES DuplicateMethodId REFUSES IMPLEMENTED lib.rs:814-823 crates/lance-graph-dt64/src/lib.rs:1347 MECHANICAL-CALLGRAPH charon-codegraph +R229 05-methods.md 23 BindStore::register REFUSES FieldBasisChanged (basis check) REFUSES IMPLEMENTED lib.rs:814-823 crates/lance-graph-dt64/src/lib.rs:871-878 MECHANICAL-CALLGRAPH charon-codegraph +R230 05-methods.md 23 BindStore::register INVARIANT a bound class never changes (BehaviourImmutable on any different re-register) INVARIANT IMPLEMENTED lib.rs:814-823 crates/lance-graph-dt64/src/lib.rs:904-906 INTERPRETATION dt64-runtime-test +R231 05-methods.md 24 BindStore::method_ref RETURNS MethodRef carrying a Stamp RETURNS IMPLEMENTED lib.rs:1136-1157 crates/lance-graph-dt64/src/lib.rs:1136,1147-1155 MECHANICAL-SYNTAX syntax-index (#1999) +R232 05-methods.md 25 BindStore::admit SEQUENCE checks identity, signature revision, guard witness, binding digest, issuer in fixed order SEQUENCE IMPLEMENTED lib.rs:1180-1211 crates/lance-graph-dt64/src/lib.rs:1181-1210 (class 1184, method 1190, sig_rev 1192, guard 1200-1206, digest 1207, issuer 1210) MECHANICAL-CALLGRAPH charon-codegraph +R233 05-methods.md 26 BindStore::admit REFUSES UnknownMethod REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1190 MECHANICAL-CALLGRAPH charon-codegraph page cites exact Refusal arm lines 554/555/562/564/566/571/574: all match +R234 05-methods.md 26 BindStore::admit REFUSES SignatureRevisionMismatch REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1193 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R235 05-methods.md 26 BindStore::admit REFUSES GuardDropped REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1202 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R236 05-methods.md 26 BindStore::admit REFUSES GuardAdded REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1203 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R237 05-methods.md 26 BindStore::admit REFUSES GuardMismatch REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1205 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R238 05-methods.md 26 BindStore::admit REFUSES BindingMismatch REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1208 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R239 05-methods.md 26 BindStore::admit REFUSES ForeignStore REFUSES IMPLEMENTED lib.rs:473-575 (554,555,562,564,566,571,574) crates/lance-graph-dt64/src/lib.rs:1210 MECHANICAL-CALLGRAPH charon-codegraph same fact as page 03 L259 +R240 05-methods.md 28 MethodBinding TAKES BindStore::register takes Vec TAKES IMPLEMENTED lib.rs:814-823 crates/lance-graph-dt64/src/lib.rs:819 MECHANICAL-SYNTAX syntax-index (#1999) +R241 05-methods.md 28 BindStore::register SEQUENCE lifecycle order register -> method_ref -> admit (method_ref needs a registered class; admit checks the stamped ref) SEQUENCE IMPLEMENTED lib.rs:814-823,1136-1157,1180-1211 crates/lance-graph-dt64/src/lib.rs:1139-1145 (method_ref looks up registered entry); crates/lance-graph-dt64/src/lib.rs:1207-1210 (admit checks stamp) INTERPRETATION human-review usage-order claim across three methods, not a call edge +R242 05-methods.md 31 BindStore::admit -> rel_from_set SEQUENCE admitted binding's WHEN guard is converted SetExpr -> Rel SEQUENCE OPEN-PR normalize.rs:124-130 (PR #1996 branch only) crates/foundry-parity-lab/src/method.rs:217-218 (admit, take when guard); crates/foundry-parity-lab/src/method.rs:251 (rename); crates/foundry-parity-lab/src/method.rs:266 (rel_from_set); crates/lance-graph-relalg/src/normalize.rs:128 MECHANICAL-CALLGRAPH charon-codegraph STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R243 05-methods.md 31 rel_from_set TAKES &SetExpr TAKES OPEN-PR normalize.rs:124-130 crates/lance-graph-relalg/src/normalize.rs:128 MECHANICAL-SYNTAX syntax-index (#1999) STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R244 05-methods.md 31 rel_from_set RETURNS Rel RETURNS OPEN-PR normalize.rs:124-130 crates/lance-graph-relalg/src/normalize.rs:128 MECHANICAL-SYNTAX syntax-index (#1999) STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R245 05-methods.md 32 PreparedMethod::prepare CALLS run_with_program(Query{rel_from_set(guard),Keep}) CALLS IMPLEMENTED method.rs:211-292 crates/foundry-parity-lab/src/method.rs:264-269; crates/lance-graph-relalg/src/lower.rs:70-92 (normalize 75, symbolic 76, lower_and_run 84) MECHANICAL-CALLGRAPH kythe/rust-analyzer +R246 05-methods.md 33 run_with_program RETURNS Option: one mask-risc Program (None when answered symbolically) RETURNS IMPLEMENTED lower.rs:70-100 crates/lance-graph-relalg/src/lower.rs:74,76-83 MECHANICAL-SYNTAX syntax-index (#1999) +R247 05-methods.md 33 relalg lowering INVARIANT keeps only the LAST fold's program (so a multi-fold lowering cannot be reused) INVARIANT IMPLEMENTED method.rs:211-292 crates/lance-graph-relalg/src/lower.rs:148 (d.last_program()); crates/foundry-parity-lab/src/method.rs:274-280 INTERPRETATION charon-codegraph page 05 notes L136-138 states the consequence (Folds refusal) +R248 05-methods.md 33 PreparedMethod FIELD program: Program kept per binding FIELD OPEN-PR method.rs:200-292 crates/foundry-parity-lab/src/method.rs:204,285-291 MECHANICAL-SYNTAX syntax-index (#1999) STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R249 05-methods.md 34 PreparedMethod::run CALLS execute_into(program, planes, Foreign::NONE, scratch, Out::Mask) CALLS IMPLEMENTED mask-risc exec.rs:1343 crates/foundry-parity-lab/src/method.rs:302-308; crates/lance-graph-mask-risc/src/exec.rs:1343 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R250 05-methods.md 35 PreparedMethod DEFINES prepare (cold) and run (hot) DEFINES OPEN-PR method.rs:200-292 crates/foundry-parity-lab/src/method.rs:200,211,295 MECHANICAL-SYNTAX syntax-index (#1999) STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R251 05-methods.md 36 rel_from_set CALLS used by PreparedMethod (dashed edge RFS -.-> LAB) CALLS OPEN-PR - crates/foundry-parity-lab/src/method.rs:31,266 MECHANICAL-CALLGRAPH kythe/rust-analyzer LEGEND-INCONSISTENT: legend says dashed = gap, yet this edge exists in code (and on main). STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R252 05-methods.md 37 Program FIELD held by PreparedMethod (dashed edge PROG -.-> LAB) FIELD OPEN-PR - crates/foundry-parity-lab/src/method.rs:204 MECHANICAL-SYNTAX syntax-index (#1999) LEGEND-INCONSISTENT as above +R253 05-methods.md 39 r2il binding::prepare CALLS BindStore::admit then binds each effect to an opcode CALLS IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:334,344-355 (opcode() 350, defined 542) MECHANICAL-CALLGRAPH kythe/rust-analyzer cited range 321-355 ends 10 lines before prepare ends (365) +R254 05-methods.md 40 binding_native::prepare_native TAKES Prepared plan (keeps compiled programs) TAKES IMPLEMENTED binding_native.rs:203-216 crates/lance-graph-r2il/src/binding_native.rs:203-210; ProgramPlan holds CompiledProgram crates/lance-graph-r2il/src/binding_native.rs:76-77 MECHANICAL-SYNTAX syntax-index (#1999) +R255 05-methods.md 41 binding_native::run_native CALLS ExecPermit check (permit.methods.contains) CALLS IMPLEMENTED binding_native.rs:351-417 crates/lance-graph-r2il/src/binding_native.rs:368-370 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R256 05-methods.md 42 run_native RETURNS Receipt with plan_id, method, frame, output RETURNS IMPLEMENTED binding.rs:223-231 CONTRADICTED(partial): run_native returns NativeReceipt {plan_id, frame, programs_run, len, values} (no method, no steps_executed) crates/lance-graph-r2il/src/binding_native.rs:178-187,359; the Receipt{plan_id,method,frame,steps_executed,programs_run,output} is returned by binding::run crates/lance-graph-r2il/src/binding.rs:223-231,385 MECHANICAL-SYNTAX syntax-index (#1999) flowchart node RCPT is fed from run_native; the sequence diagram L187 correctly lists the run() fields +R257 05-methods.md 43 r2il binding::prepare REFUSES GuardNotExecutable when the binding has a WHEN guard REFUSES IMPLEMENTED binding.rs:251-252,336-338 crates/lance-graph-r2il/src/binding.rs:335-337 (declared crates/lance-graph-r2il/src/binding.rs:252) MECHANICAL-CALLGRAPH charon-codegraph +R258 05-methods.md 45 xlog bag_count_admitted TAKES a MethodBinding (from admit) + words reader + Intake + MapTable TAKES IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:384-390 MECHANICAL-SYNTAX syntax-index (#1999) +R259 05-methods.md 45 xlog bag_count_admitted REFUSES NotBag unless Population::Bag REFUSES IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:391-393 MECHANICAL-CALLGRAPH charon-codegraph +R260 05-methods.md 45 xlog bag_count_admitted REFUSES Shape unless steps are GroupCount, GroupCount, MulI64 REFUSES IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:399-401 MECHANICAL-CALLGRAPH charon-codegraph +R261 05-methods.md 47 ExecPermit issuer GAP not decided GAP MISSING binding.rs:125-131 crates/lance-graph-r2il/src/binding.rs:124-126 (doc: 'who issues it is not decided') NOT-RECOVERABLE human-review +R262 05-methods.md 48 one executor for WHEN and DO GAP not built GAP MISSING .claude/plans/foundry-parity-v1.md (cited as plan) .claude/plans/foundry-parity-v1.md:125 (row 5 'One executor for WHEN and DO'); WHEN refused in r2il crates/lance-graph-r2il/src/binding.rs:335-337; lab binding has empty effects crates/foundry-parity-lab/src/method.rs:89 NOT-RECOVERABLE human-review absence claim; closed search: foundry-parity-lab, lance-graph-r2il +R263 05-methods.md 49 ExecPermit issuer GAP edge to run (dashed PERMIT -.-> RUN) GAP MISSING - crates/lance-graph-r2il/src/binding.rs:124-126; run requires permit crates/lance-graph-r2il/src/binding.rs:393-395 NOT-RECOVERABLE human-review +R264 05-methods.md 50 one executor GAP edge to execute_into (dashed ONE -.-> EXEC) GAP MISSING - crates/foundry-parity-lab/src/method.rs:302-308 (WHEN only) NOT-RECOVERABLE human-review +R265 05-methods.md 51 one executor GAP edge to run_native (dashed ONE -.-> RUN) GAP MISSING - crates/lance-graph-r2il/src/binding_native.rs:351-417 (DO only) NOT-RECOVERABLE human-review +R266 05-methods.md 56 BindStore::register INVARIANT is the only way a binding enters a store INVARIANT IMPLEMENTED lib.rs:814-823 CONTRADICTED(partial): BindStore::register_derived crates/lance-graph-dt64/src/lib.rs:826-841 also inserts a binding via the private insert (840) INTERPRETATION syntax-index (#1999) both public entry points funnel through private insert {LIB}:843; claim holds only for 'register or register_derived' +R267 05-methods.md 57 BindStore::method_ref INVARIANT is the only way a MethodRef is issued INVARIANT IMPLEMENTED lib.rs:1136-1157 crates/lance-graph-dt64/src/lib.rs:352-359 (MethodRef fields are pub), crates/lance-graph-dt64/src/lib.rs:1136 INTERPRETATION syntax-index (#1999) MethodRef has pub fields so it can be constructed elsewhere; the stamp is what is restricted +R268 05-methods.md 58 Stamp INVARIANT has private fields so a reference built elsewhere cannot carry a valid stamp INVARIANT IMPLEMENTED lib.rs:353-374 CONTRADICTED(partial): fields private crates/lance-graph-dt64/src/lib.rs:371-374 but Stamp derives Clone (crates/lance-graph-dt64/src/lib.rs:370) and the source says a builder 'can only copy the stamp of a reference that store issued' crates/lance-graph-dt64/src/lib.rs:348-351 INTERPRETATION dt64-runtime-test admit still checks every other field against the binding; page wording 'cannot' is stronger than the code +R269 05-methods.md 60 BindStore::admit RETURNS the stored binding only after all checks pass RETURNS IMPLEMENTED lib.rs:1180-1211 crates/lance-graph-dt64/src/lib.rs:1180,1211 MECHANICAL-SYNTAX syntax-index (#1999) +R270 05-methods.md 61 admit order SEQUENCE identity, signature revision, guard witness, binding digest, issuer SEQUENCE IMPLEMENTED lib.rs:1180-1211 crates/lance-graph-dt64/src/lib.rs:1184-1210 MECHANICAL-CALLGRAPH charon-codegraph same as L25 row +R271 05-methods.md 63 WHEN path SEQUENCE goes through relalg and ends in one mask-risc program SEQUENCE IMPLEMENTED lower.rs:70-100 crates/foundry-parity-lab/src/method.rs:264-280 (run_with_program, one-program check); crates/lance-graph-relalg/src/lower.rs:75-91 MECHANICAL-CALLGRAPH charon-codegraph 'one program' enforced by the Folds tripwire (method.rs:276-280) +R272 05-methods.md 64 code that holds and re-runs the program INVARIANT is the G6 lab PreparedMethod on the open PR #1996 branch, not on main; rel_from_set also new in that PR INVARIANT OPEN-PR method.rs:200-292; normalize.rs:124-130 MOVED: now on main - crates/foundry-parity-lab/src/method.rs:200 and crates/lance-graph-relalg/src/normalize.rs:128 exist in a64422af4 (PR #1996 merged as 83d532759) INTERPRETATION human-review STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R273 05-methods.md 68 r2il prepare SEQUENCE runs once and is cold; run and run_native are hot SEQUENCE IMPLEMENTED binding.rs:12-61 crates/lance-graph-r2il/src/binding.rs:12-17 (doc); prepare crates/lance-graph-r2il/src/binding.rs:321; run crates/lance-graph-r2il/src/binding.rs:377; run_native crates/lance-graph-r2il/src/binding_native.rs:351 INTERPRETATION dt64-runtime-test cold/hot is a documented discipline; checks inside run are visible +R274 05-methods.md 70 run / run_native CALLS check frame, focus, scope (Guards::check), route (check_route) and ExecPermit CALLS IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:389-395; crates/lance-graph-r2il/src/binding_native.rs:364-370 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R275 05-methods.md 72 r2il prepare REFUSES a binding that has a WHEN guard REFUSES IMPLEMENTED binding.rs:251-252,336-338 crates/lance-graph-r2il/src/binding.rs:335-337 MECHANICAL-CALLGRAPH charon-codegraph +R276 05-methods.md 73 WHEN (lab) and DO (r2il) GAP nothing yet runs both for one method GAP MISSING - .claude/plans/foundry-parity-v1.md:125 NOT-RECOVERABLE human-review same fact as the 'one executor' rows +R277 05-methods.md 75 ExecPermit INVARIANT is a lab permission; who issues it is not decided INVARIANT IMPLEMENTED binding.rs:125-131 crates/lance-graph-r2il/src/binding.rs:124-126 INTERPRETATION human-review +R278 05-methods.md 112 G6 lab INVARIANT lives in crates/foundry-parity-lab, PR #1996 (open) INVARIANT OPEN-PR - MOVED: crates/foundry-parity-lab/src/method.rs exists on main; PR #1996 merged (83d532759). foundry-parity-lab is in the workspace exclude list (Cargo.toml:240) INTERPRETATION cargo-metadata STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R279 05-methods.md 112 PreparedMethod::prepare CALLS BindStore::admit(MethodRef) CALLS LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:217 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R280 05-methods.md 113 BindStore::admit RETURNS MethodBinding or Refusal RETURNS IMPLEMENTED lib.rs:1180-1211 crates/lance-graph-dt64/src/lib.rs:1180 (Result<&MethodBinding, Refusal>) MECHANICAL-SYNTAX syntax-index (#1999) +R281 05-methods.md 114 PreparedMethod::prepare CALLS World::bind -> bind_lanes(reads + storeId lane), then borrow_all CALLS LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:219-223,229; crates/foundry-parity-lab/src/bind.rs:162-184 (bind -> store.bind_lanes) MECHANICAL-CALLGRAPH kythe/rust-analyzer +R282 05-methods.md 115 borrow_all INVARIANT returns borrowed planes, no copy INVARIANT LAB - crates/lance-graph-dt64/src/lane.rs:42-45 (LaneSource::borrow must not copy) INTERPRETATION dt64-runtime-test +R283 05-methods.md 116 PreparedMethod::prepare CALLS rename(guard.expr, slots): field positions -> bound planes CALLS LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:251 (rename defined crates/foundry-parity-lab/src/method.rs:159) MECHANICAL-CALLGRAPH kythe/rust-analyzer +R284 05-methods.md 118 PreparedMethod::prepare CALLS conjoin SetExpr::ne_u32(id_lane, DENIED_STORE) when authorization is set CALLS LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:252-257 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R285 05-methods.md 120 PreparedMethod::prepare CALLS run_with_program(Query{rel_from_set(guard),Keep}) CALLS LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:264-269 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R286 05-methods.md 121 run_with_program CALLS lower_and_run (normalize, lower, run once) CALLS IMPLEMENTED lower.rs:70-100 crates/lance-graph-relalg/src/lower.rs:75,84 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R287 05-methods.md 122 run_with_program RETURNS Run + Option RETURNS IMPLEMENTED lower.rs:70-100 crates/lance-graph-relalg/src/lower.rs:74 MECHANICAL-SYNTAX syntax-index (#1999) +R288 05-methods.md 123 PreparedMethod::prepare REFUSES MethodRefusal::Folds unless exactly one program ran REFUSES LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:276-280 MECHANICAL-CALLGRAPH charon-codegraph +R289 05-methods.md 125 PreparedMethod::run CALLS execute_into(program, planes, Out::Mask(keep)) per question CALLS LAB method.rs:295-320 crates/foundry-parity-lab/src/method.rs:302-309 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R290 05-methods.md 127 PreparedMethod::run SEQUENCE reads identity lane (ids) at the set bits of the keep mask SEQUENCE LAB method.rs:295-320 crates/foundry-parity-lab/src/method.rs:311-318 MECHANICAL-CALLGRAPH charon-codegraph +R291 05-methods.md 133 guard INVARIANT is a SetExpr over field positions; mask fields Sym(field); value fields comparisons on a lane INVARIANT LAB method.rs:47-61 crates/foundry-parity-lab/src/method.rs:47-61 (SetExpr::Sym, SetExpr::i32) MECHANICAL-SYNTAX syntax-index (#1999) +R292 05-methods.md 136 PreparedMethod INVARIANT keeps the one program relalg returns INVARIANT LAB method.rs:105-135 crates/foundry-parity-lab/src/method.rs:273,285-291 INTERPRETATION human-review +R293 05-methods.md 137 PreparedMethod::prepare REFUSES MethodRefusal::Folds when the guard lowered into more than one fold REFUSES LAB method.rs:105-135 crates/foundry-parity-lab/src/method.rs:118-120,276-280 MECHANICAL-CALLGRAPH charon-codegraph why: relalg keeps only the last fold's program (crates/lance-graph-relalg/src/lower.rs:148) +R294 05-methods.md 139 reader scope in lab INVARIANT is a stand-in written into the program, not the RBAC decision INVARIANT LAB method.rs:211-292 crates/foundry-parity-lab/src/method.rs:14-16,252-257 INTERPRETATION human-review +R295 05-methods.md 142 foundry-parity-lab arm C REFUSES CostRefusal::NotBound when a demanded cost lane is not bound REFUSES LAB arm_c.rs:66-92 crates/foundry-parity-lab/src/arm_c.rs:82,182 MECHANICAL-CALLGRAPH charon-codegraph +R296 05-methods.md 143 arm C (#1995) INVARIANT is merged and separate from the method path INVARIANT LAB - crates/foundry-parity-lab/src/arm_c.rs (commit 15d4b4cb4 '(#1995)'); arm_c.rs has no use of method.rs INTERPRETATION cargo-metadata merge status read from commit subject; separation = no module reference +R297 05-methods.md 168 r2il binding::prepare TAKES store, view, lens, Resolution, frames, now TAKES IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:321-328 MECHANICAL-SYNTAX syntax-index (#1999) +R298 05-methods.md 169 binding::prepare CALLS Guards::check(frames, now) CALLS IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:329 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R299 05-methods.md 170 binding::prepare CALLS check_route then BindStore::resolve(view, class, schema_rev) CALLS IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:330-333; check_route crates/lance-graph-r2il/src/binding.rs:483 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R300 05-methods.md 171 binding::prepare CALLS BindStore::admit(MethodRef) CALLS IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:334 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R301 05-methods.md 172 binding::prepare REFUSES GuardNotExecutable (WHEN guard) REFUSES IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:335-337 MECHANICAL-CALLGRAPH charon-codegraph +R302 05-methods.md 172 binding::prepare REFUSES ThreeValuedNotExecutable (three-valued truth) REFUSES IMPLEMENTED binding.rs:321-355 crates/lance-graph-r2il/src/binding.rs:338-340 MECHANICAL-CALLGRAPH charon-codegraph +R303 05-methods.md 173 binding::prepare CALLS opcode(): lens, label alias (polyfill) or vocabulary name, EXECUTABLE, arity per effect CALLS IMPLEMENTED binding.rs:236-317 crates/lance-graph-r2il/src/binding.rs:350,542-602,606-629; EXECUTABLE check crates/lance-graph-r2il/src/binding.rs:582; arity crates/lance-graph-r2il/src/binding.rs:590-597,620-626; alias crates/lance-graph-r2il/src/binding.rs:613-619 MECHANICAL-CALLGRAPH kythe/rust-analyzer EXECUTABLE is checked on the R2IL-fold-reading path (crates/lance-graph-r2il/src/binding.rs:582); the POLYFILL_LENS path returns the table opcode without it (polyfill positions are the EXECUTABLE set by construction, polyfill.rs:25) +R304 05-methods.md 174 binding::prepare RETURNS Prepared (plan_id, steps) RETURNS IMPLEMENTED binding.rs:165-176 crates/lance-graph-r2il/src/binding.rs:328,357-364; Prepared crates/lance-graph-r2il/src/binding.rs:165-175 MECHANICAL-SYNTAX syntax-index (#1999) +R305 05-methods.md 177 binding_native::prepare_native CALLS runs the plan's steps once through FoldDialect and keeps the compiled programs CALLS IMPLEMENTED binding_native.rs:203-216 crates/lance-graph-r2il/src/binding_native.rs:196-216 (doc + signature); ProgramPlan{cp: CompiledProgram} crates/lance-graph-r2il/src/binding_native.rs:76-77 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R306 05-methods.md 179 binding_native::prepare_native REFUSES FoldResultFeedsFold (fold consuming a fold result) REFUSES IMPLEMENTED binding_native.rs:203-216 crates/lance-graph-r2il/src/binding_native.rs:244,261 MECHANICAL-CALLGRAPH charon-codegraph +R307 05-methods.md 179 binding_native::prepare_native RETURNS NativePlan RETURNS IMPLEMENTED binding_native.rs:203-216 crates/lance-graph-r2il/src/binding_native.rs:210 MECHANICAL-SYNTAX syntax-index (#1999) +R308 05-methods.md 182 binding::run TAKES plan, store, frames, now, ExecPermit, fields, dialect TAKES IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:377-385 MECHANICAL-SYNTAX syntax-index (#1999) +R309 05-methods.md 183 binding::run CALLS BindStore::check_issuer(plan.method) CALLS IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:386-388; native crates/lance-graph-r2il/src/binding_native.rs:361-363 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R310 05-methods.md 184 binding::run CALLS Guards::check(frames, now) and check_route CALLS IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:389-392; native crates/lance-graph-r2il/src/binding_native.rs:364-367 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R311 05-methods.md 185 binding::run REFUSES NotPermitted unless permit lists this exact MethodRef REFUSES IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:393-395; native crates/lance-graph-r2il/src/binding_native.rs:368-370 MECHANICAL-CALLGRAPH charon-codegraph +R312 05-methods.md 186 binding::run CALLS run_steps over FoldDialect (native: execute_compiled per program) CALLS IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:397,404; native crates/lance-graph-r2il/src/binding_native.rs:379-393 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R313 05-methods.md 187 binding::run RETURNS Receipt(plan_id, method, frame, steps_executed, programs_run, output) RETURNS IMPLEMENTED binding.rs:223-231 crates/lance-graph-r2il/src/binding.rs:223-231,385 MECHANICAL-SYNTAX syntax-index (#1999) +R314 05-methods.md 187 binding::run check order SEQUENCE issuer, guards, route, permit, then steps SEQUENCE IMPLEMENTED binding.rs:377-404 crates/lance-graph-r2il/src/binding.rs:386-396 MECHANICAL-CALLGRAPH charon-codegraph +R315 05-methods.md 192 binding::run INVARIANT never reads the ClassView or the vocabulary again INVARIANT IMPLEMENTED binding.rs:12-61 crates/lance-graph-r2il/src/binding.rs:377-385 (no view parameter), crates/lance-graph-r2il/src/binding.rs:12-17 (doc) MECHANICAL-SYNTAX syntax-index (#1999) 'no ClassView param' is a signature fact; 'never reads the vocabulary' needs a body/callgraph check (charon-codegraph) +R316 05-methods.md 195 BindStore::admit INVARIANT succeeding is not permission to run; permit must list the exact MethodRef INVARIANT IMPLEMENTED binding.rs:125-131 crates/lance-graph-r2il/src/binding.rs:59-61,124-126,393-395 INTERPRETATION dt64-runtime-test +R317 05-methods.md 197 Receipt INVARIANT is bounded by number of steps; not a row trace or logical provenance INVARIANT IMPLEMENTED binding.rs:223-231 crates/lance-graph-r2il/src/binding.rs:219-221; NativeReceipt fixed array crates/lance-graph-r2il/src/binding_native.rs:186 INTERPRETATION human-review +R318 05-methods.md 199 binding_native::run_native REFUSES PlanesChanged when plane shape differs from the prepared one REFUSES IMPLEMENTED binding_native.rs:351-417 crates/lance-graph-r2il/src/binding_native.rs:371-377 MECHANICAL-CALLGRAPH charon-codegraph +R319 05-methods.md 201 xlog bag_count_admitted REFUSES NotBag (population != Bag) REFUSES IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:391-393 MECHANICAL-CALLGRAPH charon-codegraph duplicate of L45 row +R320 05-methods.md 201 xlog bag_count_admitted REFUSES Shape (steps != GroupCount, GroupCount, MulI64) REFUSES IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:399-401 MECHANICAL-CALLGRAPH charon-codegraph duplicate of L45 row +R321 05-methods.md 204 xlog Intake::bag_count CALLS MapTable::map(frame, tile) on every query (frame re-check) CALLS IMPLEMENTED xlog lib.rs:363-405 crates/lance-graph-xlog/src/lib.rs:345-347,334-336 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R322 05-methods.md 222 one executor for WHEN and DO GAP not built; plan lists it as the missing contract for the computed-function row GAP MISSING - .claude/plans/foundry-parity-v1.md:125 NOT-RECOVERABLE human-review +R323 05-methods.md 224 ExecPermit issuer GAP undecided GAP MISSING - crates/lance-graph-r2il/src/binding.rs:124-126 NOT-RECOVERABLE human-review +R324 05-methods.md 225 Operation::Act decision (lance-graph-rbac) INVARIANT is a natural candidate issuer of ExecPermit; candidate only INVARIANT PROPOSED - .claude/plans/foundry-parity-v1.md:295 ('natural issuer'); Operation::Act exists crates/lance-graph-contract/src/rbac.rs:359 and is handled crates/lance-graph-rbac/src/authorize.rs:160 INTERPRETATION human-review +R325 05-methods.md 228 PreparedMethod and rel_from_set INVARIANT are on PR #1996 and not merged INVARIANT OPEN-PR - CONTRADICTED: merged (83d532759 in origin/main); crates/foundry-parity-lab/src/method.rs:200, crates/lance-graph-relalg/src/normalize.rs:128 on main INTERPRETATION human-review STALE-STATUS: page says PR #1996 open/not merged; origin/main (a64422af4) contains merge 83d532759 'Merge pull request #1996', and the file is present in this tree (identical to origin/main for crates/ and .mermaid/) +R326 06-authorization.md 7 authorization decision GAP nothing yet applies it to a DT64 binding GAP MISSING - crates/lance-graph-dt64|r2il|xlog|quack|mask-risc Cargo.toml: no lance-graph-rbac dependency (grep 'rbac' hits only a doc comment at lib.rs:745) NOT-RECOVERABLE cargo-metadata dependency absence is mechanical (cargo-metadata); that no other path applies it is a closed-world claim +R327 06-authorization.md 12 ogar-auth, ogar-rbac DEPENDS live in the OGAR repository, not lance-graph DEPENDS IMPLEMENTED - OGAR/crates/ogar-auth, OGAR/crates/ogar-rbac (path /home/user/OGAR) MECHANICAL-SYNTAX cargo-metadata +R328 06-authorization.md 21 Identity assertion INVARIANT has federated, local or kiosk forms INVARIANT IMPLEMENTED - OGAR/crates/ogar-auth/src/user.rs:259 (federated), :218 (local), :205 (kiosk) MECHANICAL-SYNTAX syntax-index (#1999) +R329 06-authorization.md 23 ogar-auth establish SEQUENCE verify, trusted issuer, resolve (issuer, subject) SEQUENCE IMPLEMENTED federation.rs:244-283 OGAR/crates/ogar-auth/src/federation.rs:263 (verify), :264-266 (provider_of), :267-270 (resolve_external) MECHANICAL-CALLGRAPH charon-codegraph +R330 06-authorization.md 23 VerifiedLogin INVARIANT only producer is establish INVARIANT IMPLEMENTED federation.rs:206-216 OGAR/crates/ogar-auth/src/federation.rs:202-204 (doc), :271 (only struct literal in source; other hit is a compile_fail forging doctest OGAR/crates/ogar-auth/src/federation.rs:60-67; ogar-flow-m365/src/tests.rs:25 only names the type in a fn signature) MECHANICAL-SYNTAX syntax-index (#1999) negative claim over a closed search (grep 'VerifiedLogin {' in OGAR/crates) +R331 06-authorization.md 24 AuthenticatedUser FIELD user + AuthContext FIELD IMPLEMENTED user.rs:290-335 OGAR/crates/ogar-auth/src/user.rs:305,307 MECHANICAL-SYNTAX syntax-index (#1999) +R332 06-authorization.md 24 AuthenticatedUser DEFINES acting_party() DEFINES IMPLEMENTED user.rs:290-335 OGAR/crates/ogar-auth/src/user.rs:328 MECHANICAL-SYNTAX syntax-index (#1999) +R333 06-authorization.md 32 establish RETURNS VerifiedLogin RETURNS IMPLEMENTED federation.rs:244-283 OGAR/crates/ogar-auth/src/federation.rs:257-262 MECHANICAL-SYNTAX syntax-index (#1999) +R334 06-authorization.md 32 VerifiedLogin FIELD user: AuthenticatedUser FIELD IMPLEMENTED federation.rs:206-216 OGAR/crates/ogar-auth/src/federation.rs:207 MECHANICAL-SYNTAX syntax-index (#1999) +R335 06-authorization.md 33 OgarRbac::authorize_user TAKES &AuthenticatedUser (not a bare actor string) TAKES IMPLEMENTED ogar-rbac lib.rs:122-162 OGAR/crates/ogar-rbac/src/lib.rs:155-159 MECHANICAL-SYNTAX syntax-index (#1999) +R336 06-authorization.md 33 OgarRbac::authorize_user CALLS lance-graph-rbac authorize_scoped CALLS IMPLEMENTED ogar-rbac lib.rs:122-162 OGAR/crates/ogar-rbac/src/lib.rs:161; import OGAR/crates/ogar-rbac/src/lib.rs:71 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R337 06-authorization.md 33 authorize_scoped RETURNS ScopedDecision RETURNS IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:210-215 MECHANICAL-SYNTAX syntax-index (#1999) +R338 06-authorization.md 34 OgarRbac::authorize_identity (free fn authorize_identity) TAKES &AuthenticatedUser + RbacBinding TAKES IMPLEMENTED ogar-rbac lib.rs:225-345 OGAR/crates/ogar-rbac/src/lib.rs:327-332 MECHANICAL-SYNTAX syntax-index (#1999) +R339 06-authorization.md 34 authorize_identity CALLS IdentityActors::new and authorize_memberships CALLS IMPLEMENTED ogar-rbac lib.rs:225-345 OGAR/crates/ogar-rbac/src/lib.rs:333-334; import OGAR/crates/ogar-rbac/src/lib.rs:70 MECHANICAL-CALLGRAPH kythe/rust-analyzer flowchart box says 'ogar-rbac authorize_identity: binding + IdentityActors' +R340 06-authorization.md 34 authorize_memberships RETURNS MembershipDecision RETURNS IMPLEMENTED authorize.rs:299-345 crates/lance-graph-rbac/src/authorize.rs:299-304 MECHANICAL-SYNTAX syntax-index (#1999) +R341 06-authorization.md 39 establish SEQUENCE verifier first, then trusted issuer, then resolve; no fallback to email SEQUENCE IMPLEMENTED federation.rs:244-283 OGAR/crates/ogar-auth/src/federation.rs:246-250 (doc), :263-270 MECHANICAL-CALLGRAPH charon-codegraph +R342 06-authorization.md 44 VerifiedLogin INVARIANT has private fields and no public constructor INVARIANT IMPLEMENTED federation.rs:206-216 OGAR/crates/ogar-auth/src/federation.rs:205-210 (private fields), :212-242 (impl has accessors only) MECHANICAL-SYNTAX syntax-index (#1999) +R343 06-authorization.md 45 AuthenticatedUser INVARIANT has public fields; descriptive, building one proves nothing about login INVARIANT IMPLEMENTED user.rs:290-335 OGAR/crates/ogar-auth/src/user.rs:298-308 INTERPRETATION human-review pub fields are mechanical; 'proves nothing' is interpretation +R344 06-authorization.md 47 refusing unauthenticated actors INVARIANT is a deployment policy, not a grant rule INVARIANT IMPLEMENTED ogar-rbac lib.rs:122-162 OGAR/crates/ogar-rbac/src/lib.rs:146-153 INTERPRETATION human-review +R345 06-authorization.md 50 OgarRbac::authorize_user INVARIANT adds only the identity to the generic kernel call INVARIANT IMPLEMENTED ogar-rbac lib.rs:122-162 OGAR/crates/ogar-rbac/src/lib.rs:142-144,161 INTERPRETATION charon-codegraph body is a single call; mechanical via callgraph +R346 06-authorization.md 52 authorize_identity SEQUENCE binds every membership of the user to the user's tenant, then calls authorize_memberships SEQUENCE IMPLEMENTED ogar-rbac lib.rs:225-345 OGAR/crates/ogar-rbac/src/lib.rs:308-319 (memberships_of: tenant scope), :333-334 MECHANICAL-CALLGRAPH charon-codegraph +R347 06-authorization.md 54 authorize_identity RETURNS MembershipDecision, not ScopedDecision RETURNS IMPLEMENTED ogar-rbac lib.rs:225-345 OGAR/crates/ogar-rbac/src/lib.rs:332 MECHANICAL-SYNTAX syntax-index (#1999) +R348 06-authorization.md 55 delegated login INVARIANT authorizes as the user whose authority the token carries; acting party recorded, holds no role INVARIANT IMPLEMENTED ogar-rbac lib.rs:225-345 OGAR/crates/ogar-rbac/src/lib.rs:249-254 (doc), :280-285 (roles from identity.user.roles; acting kept separately) INTERPRETATION human-review +R349 06-authorization.md 76 Operation VARIANT Read{depth} VARIANT IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:349 MECHANICAL-SYNTAX syntax-index (#1999) +R350 06-authorization.md 76 Operation VARIANT Write{predicate} VARIANT IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:354 MECHANICAL-SYNTAX syntax-index (#1999) +R351 06-authorization.md 76 Operation VARIANT Act{action} VARIANT IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:359 MECHANICAL-SYNTAX syntax-index (#1999) +R352 06-authorization.md 77 Stage 1 authorize CALLS ClassRbac::grant_permits over actor roles (positive and op gate) CALLS IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:66-86 (authorize), :229 (grant_permits in stage 2 uses same predicate) MECHANICAL-CALLGRAPH kythe/rust-analyzer +R353 06-authorization.md 78 authorize_scoped SEQUENCE non-Allow short-circuits to scope None and field_mask FULL (no stage 2) SEQUENCE IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:216-224 MECHANICAL-CALLGRAPH charon-codegraph +R354 06-authorization.md 78 AccessDecision VARIANT Deny or Escalate are the non-Allow results VARIANT IMPLEMENTED access.rs:5-13 crates/lance-graph-rbac/src/access.rs:5-12 MECHANICAL-SYNTAX syntax-index (#1999) Escalate is declared (access.rs:12) but across lance-graph/crates the only construction is a unit test (access.rs:47); consumers match it (callcenter unified_bridge.rs:455,468). authorize/op_denied/authorize_memberships return only Allow or Deny +R355 06-authorization.md 79 authorize_scoped stage 2 SEQUENCE folds only the granting roles (actor_roles AND grant_permits) SEQUENCE IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:225-245 MECHANICAL-CALLGRAPH charon-codegraph +R356 06-authorization.md 80 authorize_scoped CALLS ScopeSpec::intersect over granting roles' Some scopes; None (global) leaves the fold untouched CALLS IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:236-241 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R357 06-authorization.md 81 authorize_scoped CALLS WideFieldMask::union of role field_masks CALLS IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:243 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R358 06-authorization.md 82 ScopedDecision::visible_fields RETURNS field_mask if Allow else EMPTY RETURNS IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:193-199 MECHANICAL-SYNTAX syntax-index (#1999) +R359 06-authorization.md 83 authorize_memberships CALLS unions ScopeSet members; any unscoped granting membership means unrestricted CALLS IMPLEMENTED authorize.rs:255-345 crates/lance-graph-rbac/src/authorize.rs:318-331,338 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R360 06-authorization.md 91 authorize_memberships SEQUENCE edge from stage 1 (dashed 'memberships route') SEQUENCE IMPLEMENTED authorize.rs:255-345 crates/lance-graph-rbac/src/authorize.rs:299-341 (independent loop over rbac.memberships + grant_permits; does not call authorize() or authorize_scoped) INTERPRETATION charon-codegraph LABEL-IMPRECISE: authorize_memberships is a sibling kernel, not a branch of stage 1; doc {AZ}:296-297 says verdict matches authorize() +R361 06-authorization.md 96 refused decision INVARIANT field_mask holds the open default FULL; use visible_fields() which returns EMPTY unless Allow INVARIANT IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:218-223,193-199 INTERPRETATION dt64-runtime-test +R362 06-authorization.md 99 authorize_scoped INVARIANT intersects scopes of granting roles; one more role can only narrow INVARIANT IMPLEMENTED authorize.rs:210-253 crates/lance-graph-rbac/src/authorize.rs:236-241; crates/lance-graph-contract/src/rbac.rs:166-194 (intersect never widens) INTERPRETATION human-review +R363 06-authorization.md 101 authorize_memberships INVARIANT is the permissive counterpart: each granting membership adds its own scope; scopes unioned INVARIANT IMPLEMENTED authorize.rs:255-345 crates/lance-graph-rbac/src/authorize.rs:284-294 (doc), :324-331 INTERPRETATION human-review +R364 06-authorization.md 103 Operation::Write FIELD names a predicate FIELD IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:354-357 MECHANICAL-SYNTAX syntax-index (#1999) +R365 06-authorization.md 104 Operation::Act FIELD names an action FIELD IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:359-362 MECHANICAL-SYNTAX syntax-index (#1999) +R366 06-authorization.md 105 Operation::Read FIELD carries a depth FIELD IMPLEMENTED rbac.rs:340-364 crates/lance-graph-contract/src/rbac.rs:349-352 MECHANICAL-SYNTAX syntax-index (#1999) +R367 06-authorization.md 106 OpMask FIELD const READ FIELD IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:458 MECHANICAL-SYNTAX syntax-index (#1999) page calls these 'verb bit per class (OpMask)' +R368 06-authorization.md 106 OpMask FIELD const WRITE FIELD IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:460 MECHANICAL-SYNTAX syntax-index (#1999) page calls these 'verb bit per class (OpMask)' +R369 06-authorization.md 106 OpMask FIELD const CREATE FIELD IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:462 MECHANICAL-SYNTAX syntax-index (#1999) page calls these 'verb bit per class (OpMask)' +R370 06-authorization.md 106 OpMask FIELD const DELETE FIELD IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:464 MECHANICAL-SYNTAX syntax-index (#1999) page calls these 'verb bit per class (OpMask)' +R371 06-authorization.md 106 OpMask FIELD const ACT FIELD IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:466 MECHANICAL-SYNTAX syntax-index (#1999) page calls these 'verb bit per class (OpMask)' +R372 06-authorization.md 106 grants_permit CALLS ClassGrant::permits over granted set (OpMask::permits + canon-compat classid) CALLS IMPLEMENTED rbac.rs:548-550 crates/lance-graph-contract/src/rbac.rs:548-550,538-541 MECHANICAL-CALLGRAPH kythe/rust-analyzer +R373 06-authorization.md 108 depth/predicate/action-name check INVARIANT layers above the OpMask verb gate INVARIANT IMPLEMENTED rbac.rs:453-466 crates/lance-graph-contract/src/rbac.rs:443-452 (doc); crates/lance-graph-rbac/src/authorize.rs:157-161 (ClassGrants::grant_permits uses can_read_at/can_write/can_act) INTERPRETATION human-review +R374 06-authorization.md 124 ScopedDecision DEFINES struct ScopedDecision DEFINES IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:170 MECHANICAL-SYNTAX syntax-index (#1999) +R375 06-authorization.md 125 ScopedDecision FIELD decision: AccessDecision FIELD IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:172 MECHANICAL-SYNTAX syntax-index (#1999) +R376 06-authorization.md 126 ScopedDecision FIELD scope: Option FIELD IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:175 MECHANICAL-SYNTAX syntax-index (#1999) +R377 06-authorization.md 127 ScopedDecision FIELD field_mask: WideFieldMask FIELD IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:181 MECHANICAL-SYNTAX syntax-index (#1999) +R378 06-authorization.md 128 ScopedDecision DEFINES fn visible_fields() -> WideFieldMask DEFINES IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:193 MECHANICAL-SYNTAX syntax-index (#1999) +R379 06-authorization.md 130 MembershipDecision DEFINES struct MembershipDecision DEFINES IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:257 MECHANICAL-SYNTAX syntax-index (#1999) +R380 06-authorization.md 131 MembershipDecision FIELD decision: AccessDecision FIELD IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:259 MECHANICAL-SYNTAX syntax-index (#1999) +R381 06-authorization.md 132 MembershipDecision FIELD scope: Option FIELD IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:263 MECHANICAL-SYNTAX syntax-index (#1999) +R382 06-authorization.md 133 MembershipDecision FIELD field_mask: WideFieldMask FIELD IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:267 MECHANICAL-SYNTAX syntax-index (#1999) +R383 06-authorization.md 134 MembershipDecision DEFINES fn visible_fields() -> WideFieldMask DEFINES IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:275 MECHANICAL-SYNTAX syntax-index (#1999) +R384 06-authorization.md 136 ScopeSpec DEFINES struct ScopeSpec DEFINES IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:115 MECHANICAL-SYNTAX syntax-index (#1999) +R385 06-authorization.md 137 ScopeSpec FIELD tenant: Option FIELD IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:117 MECHANICAL-SYNTAX syntax-index (#1999) +R386 06-authorization.md 138 ScopeSpec FIELD predicate_key: u32 FIELD IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:120 MECHANICAL-SYNTAX syntax-index (#1999) +R387 06-authorization.md 139 ScopeSpec FIELD path: ScopePath FIELD IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:123 MECHANICAL-SYNTAX syntax-index (#1999) +R388 06-authorization.md 140 ScopeSpec FIELD deny: bool FIELD IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:131 MECHANICAL-SYNTAX syntax-index (#1999) +R389 06-authorization.md 141 ScopeSpec DEFINES fn admits(&ScopePath) -> bool DEFINES IMPLEMENTED rbac.rs:144-151 crates/lance-graph-contract/src/rbac.rs:149 MECHANICAL-SYNTAX syntax-index (#1999) +R390 06-authorization.md 142 ScopeSpec DEFINES fn intersect(other) -> ScopeSpec DEFINES IMPLEMENTED rbac.rs:153-191 crates/lance-graph-contract/src/rbac.rs:166 MECHANICAL-SYNTAX syntax-index (#1999) cited range ends at 191; fn ends 194 +R391 06-authorization.md 144 ScopeSet DEFINES struct ScopeSet DEFINES IMPLEMENTED rbac.rs:236-267 crates/lance-graph-contract/src/rbac.rs:236 MECHANICAL-SYNTAX syntax-index (#1999) +R392 06-authorization.md 145 ScopeSet FIELD members: Vec (private) FIELD IMPLEMENTED rbac.rs:236-267 crates/lance-graph-contract/src/rbac.rs:237 MECHANICAL-SYNTAX syntax-index (#1999) +R393 06-authorization.md 146 ScopeSet DEFINES fn admits(&ScopePath) -> bool DEFINES IMPLEMENTED rbac.rs:236-267 crates/lance-graph-contract/src/rbac.rs:265 MECHANICAL-SYNTAX syntax-index (#1999) +R394 06-authorization.md 148 PropertySpec DEFINES struct PropertySpec DEFINES IMPLEMENTED property.rs:41-58 crates/lance-graph-contract/src/property.rs:41 MECHANICAL-SYNTAX syntax-index (#1999) +R395 06-authorization.md 149 PropertySpec FIELD predicate FIELD IMPLEMENTED property.rs:41-58 crates/lance-graph-contract/src/property.rs:43 MECHANICAL-SYNTAX syntax-index (#1999) +R396 06-authorization.md 150 PropertySpec FIELD kind FIELD IMPLEMENTED property.rs:41-58 crates/lance-graph-contract/src/property.rs:45 MECHANICAL-SYNTAX syntax-index (#1999) +R397 06-authorization.md 151 PropertySpec FIELD marking: Marking FIELD IMPLEMENTED property.rs:41-58 crates/lance-graph-contract/src/property.rs:58 MECHANICAL-SYNTAX syntax-index (#1999) +R398 06-authorization.md 153 Marking DEFINES enum Marking DEFINES IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:771 MECHANICAL-SYNTAX syntax-index (#1999) +R399 06-authorization.md 154 Marking VARIANT Public VARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:773 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L261 VARIANT rows +R400 06-authorization.md 155 Marking VARIANT Internal VARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:776 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L261 VARIANT rows +R401 06-authorization.md 156 Marking VARIANT Pii VARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:778 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L261 VARIANT rows +R402 06-authorization.md 157 Marking VARIANT Financial VARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:780 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L261 VARIANT rows +R403 06-authorization.md 158 Marking VARIANT Restricted VARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:782 MECHANICAL-SYNTAX syntax-index (#1999) duplicate of page 03 L261 VARIANT rows +R404 06-authorization.md 160 ScopedDecision FIELD scope -> ScopeSpec FIELD IMPLEMENTED authorize.rs:164-208 crates/lance-graph-rbac/src/authorize.rs:175 MECHANICAL-SYNTAX syntax-index (#1999) +R405 06-authorization.md 161 MembershipDecision FIELD scope -> ScopeSet FIELD IMPLEMENTED authorize.rs:255-278 crates/lance-graph-rbac/src/authorize.rs:263 MECHANICAL-SYNTAX syntax-index (#1999) +R406 06-authorization.md 162 ScopeSet FIELD members -> ScopeSpec FIELD IMPLEMENTED rbac.rs:236-267 crates/lance-graph-contract/src/rbac.rs:237 MECHANICAL-SYNTAX syntax-index (#1999) +R407 06-authorization.md 163 PropertySpec FIELD marking -> Marking FIELD IMPLEMENTED property.rs:41-58 crates/lance-graph-contract/src/property.rs:58 MECHANICAL-SYNTAX syntax-index (#1999) +R408 06-authorization.md 168 ScopeSpec::admits INVARIANT true when not deny and the row's path is at or below the scope's path; tenant matched by the owning store INVARIANT IMPLEMENTED rbac.rs:144-151 crates/lance-graph-contract/src/rbac.rs:144-151 INTERPRETATION dt64-runtime-test body expression !self.deny && self.path.contains(at); tenant half is a doc statement +R409 06-authorization.md 172 ScopeSpec::intersect INVARIANT never widens; deny absorbs INVARIANT IMPLEMENTED rbac.rs:153-191 crates/lance-graph-contract/src/rbac.rs:167-169 INTERPRETATION dt64-runtime-test +R410 06-authorization.md 174 ScopeSpec::intersect SEQUENCE two paths on different branches give DENY SEQUENCE IMPLEMENTED rbac.rs:153-191 crates/lance-graph-contract/src/rbac.rs:170-176 MECHANICAL-CALLGRAPH charon-codegraph +R411 06-authorization.md 175 ScopeSpec::intersect SEQUENCE two different tenants give DENY SEQUENCE IMPLEMENTED rbac.rs:153-191 crates/lance-graph-contract/src/rbac.rs:185-192 MECHANICAL-CALLGRAPH charon-codegraph +R412 06-authorization.md 176 ScopeSpec::intersect SEQUENCE a None tenant takes the other side's tenant SEQUENCE IMPLEMENTED rbac.rs:153-191 crates/lance-graph-contract/src/rbac.rs:178-184 MECHANICAL-CALLGRAPH charon-codegraph +R413 06-authorization.md 177 ScopeSpec.predicate_key INVARIANT is reserved, OR-combined, not interpreted INVARIANT IMPLEMENTED rbac.rs:114-132 crates/lance-graph-contract/src/rbac.rs:118-120,177 INTERPRETATION human-review +R414 06-authorization.md 179 Marking INVARIANT default is Internal INVARIANT IMPLEMENTED property.rs:768-783 crates/lance-graph-contract/src/property.rs:56,775-776 (#[default] Internal) MECHANICAL-SYNTAX syntax-index (#1999) +R415 06-authorization.md 181 Resolved::mask_where CALLS builds a field mask from PropertySpec meaning (e.g. marking >= Pii) CALLS IMPLEMENTED lib.rs:714-723 crates/lance-graph-dt64/src/lib.rs:715-725 (doc example :716) MECHANICAL-CALLGRAPH kythe/rust-analyzer cited range 714-723 stops 2 lines short of fn end 725 +R416 06-authorization.md 183 mask_where mask INVARIANT is a field selector, not an authorization decision INVARIANT IMPLEMENTED lib.rs:714-723 crates/lance-graph-dt64/src/lib.rs:715-725 (takes only schema+pred; no actor/RbacDecision param) INTERPRETATION human-review +R417 06-authorization.md 197 walk_rails_authorized INVARIANT applies visible_fields() and decides nothing INVARIANT IMPLEMENTED selection.rs:308-360 CONTRADICTED(partial): fn takes a caller-supplied `allowed: impl Fn(ClassId)->WideFieldMask` crates/lance-graph-contract/src/selection.rs:335-348; it never calls visible_fields(); doc says 'typically visible_fields()' crates/lance-graph-contract/src/selection.rs:315-321. 'decides nothing' confirmed crates/lance-graph-contract/src/selection.rs:321 INTERPRETATION human-review no production call site in lance-graph (only selection.rs tests, :689); OGAR ogar-doc-ir/src/resolve.rs:466 calls it through an Access{fields,admits} closure struct and documents visible_fields() as the source (:259-261), but contains no rbac dependency (Cargo.toml:23 depends on contract only) +R418 06-authorization.md 206 ScopedDecision (scope + visible_fields()) DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-rbac/src/authorize.rs:170,193 MECHANICAL-SYNTAX syntax-index (#1999) +R419 06-authorization.md 207 Resolved::mask_where (marking mask) DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-dt64/src/lib.rs:719 MECHANICAL-SYNTAX syntax-index (#1999) +R420 06-authorization.md 208 BindStore::bind_lanes + LaneBinding::borrow_all DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-dt64/src/lane.rs:171,379 MECHANICAL-SYNTAX syntax-index (#1999) +R421 06-authorization.md 209 Quack Binder::live (validity plane seam) DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-quack/src/bind.rs:96 MECHANICAL-SYNTAX syntax-index (#1999) +R422 06-authorization.md 210 walk_rails_authorized (applies visible_fields()) CALLS green node RAIL + solid edge SD --> RAIL CALLS IMPLEMENTED selection.rs:308-360 CONTRADICTED(partial): see row for L197; no call site joins ScopedDecision to walk_rails_authorized in lance-graph/crates or OGAR/crates (crates/lance-graph-contract/src/selection.rs:335) MECHANICAL-CALLGRAPH kythe/rust-analyzer solid edge = 'in code on main' per legend, but there is no code edge +R423 06-authorization.md 211 ExecPermit (lab permission) DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-r2il/src/binding.rs:124-128 MECHANICAL-SYNTAX syntax-index (#1999) page colours ExecPermit green/shipped but its own doc calls it a lab permission +R424 06-authorization.md 212 Operation::Act decision DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-contract/src/rbac.rs:359; crates/lance-graph-rbac/src/authorize.rs:160 MECHANICAL-SYNTAX syntax-index (#1999) +R425 06-authorization.md 213 auth_classid, acting_party (identity for the audit) DEFINES exists on main (green node) DEFINES IMPLEMENTED - crates/lance-graph-rbac/src/auth.rs:372-381 MECHANICAL-SYNTAX syntax-index (#1999) +R426 06-authorization.md 215 per-row scope lane (resident plane) GAP not built GAP MISSING - no lane/plane named scope in lance-graph-dt64/lane.rs; plan .claude/plans/foundry-parity-v1.md:291 NOT-RECOVERABLE human-review +R427 06-authorization.md 216 visible_fields() limiting bound fields GAP not built GAP MISSING - LaneRequest.fields is caller-supplied (lane.rs:94); no rbac use in dt64 (Cargo.toml:10) NOT-RECOVERABLE human-review +R428 06-authorization.md 217 ExecPermit issuer GAP undecided GAP MISSING - crates/lance-graph-r2il/src/binding.rs:124-126 NOT-RECOVERABLE human-review +R429 06-authorization.md 218 one record per answer (identity + receipt + witness) GAP not built GAP MISSING - .claude/plans/foundry-parity-v1.md:37 (Provenance row); receipts crates/lance-graph-r2il/src/binding.rs:223-231; auth_classid crates/lance-graph-rbac/src/auth.rs:379 NOT-RECOVERABLE human-review +R430 06-authorization.md 220 ScopedDecision GAP per-row scope lane (G2A) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R431 06-authorization.md 221 Quack Binder::live GAP per-row scope lane (G2A) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R432 06-authorization.md 222 per-row scope lane GAP BindStore::bind_lanes (G2A->BL) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R433 06-authorization.md 223 ScopedDecision GAP visible_fields limits bound fields (G2B) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R434 06-authorization.md 224 Resolved::mask_where GAP visible_fields limits bound fields (G2B) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R435 06-authorization.md 225 visible_fields limit GAP BindStore::bind_lanes (G2B->BL) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R436 06-authorization.md 226 Operation::Act decision GAP ExecPermit issuer ('candidate only') GAP PROPOSED - absence; see rows L215-218 NOT-RECOVERABLE human-review +R437 06-authorization.md 227 ExecPermit issuer GAP ExecPermit (ISS->PERM) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R438 06-authorization.md 228 auth_classid/acting_party GAP one record per answer (AUDIT->JOIN) GAP MISSING - absence; see rows L215-218 NOT-RECOVERABLE human-review +R439 06-authorization.md 236 DT64, r2il, xlog, Quack, mask-risc code GAP use lance-graph-rbac GAP MISSING Cargo.toml:1-9 of lance-graph-rbac + search note Cargo.toml of lance-graph-dt64 (:10), -r2il, -xlog, -quack, -mask-risc: no lance-graph-rbac; lance-graph-rbac/Cargo.toml:8 depends on contract only MECHANICAL-SYNTAX cargo-metadata dependency absence is a cargo-metadata fact; classed GAP because it asserts a missing integration. Callers elsewhere exist (lance-graph-callcenter, consumer-conformance, dir-sim depend on lance-graph-rbac) +R440 06-authorization.md 239 lab reader scope INVARIANT is a stand-in: one reader denied one store id, written into the program; not IAM INVARIANT LAB method.rs:14-16,252-257 crates/foundry-parity-lab/src/method.rs:14-16,252-257 INTERPRETATION human-review +R441 06-authorization.md 242 Quack Binder::live INVARIANT is the existing seam where a scope plane could enter INVARIANT PROPOSED bind.rs:91-97 crates/lance-graph-quack/src/bind.rs:96 (fn live -> Mask); plan .claude/plans/foundry-parity-v1.md:291 INTERPRETATION human-review +R442 06-authorization.md 244 ExecPermit issuer GAP r2il source says it is not decided; Operation::Act is a candidate only GAP PROPOSED binding.rs:125-131 crates/lance-graph-r2il/src/binding.rs:124-126; .claude/plans/foundry-parity-v1.md:295 NOT-RECOVERABLE human-review +R443 06-authorization.md 249 ResolvedIdentity::auth_classid INVARIANT is documented as the identity for the audit INVARIANT IMPLEMENTED auth.rs:376-381 crates/lance-graph-rbac/src/auth.rs:376-381 (struct ResolvedIdentity :256, impl :275) INTERPRETATION human-review doc says 'for the audit witness' +R444 06-authorization.md 250 receipts, commit witnesses and identity GAP nothing joins them into one record per answer GAP MISSING - .claude/plans/foundry-parity-v1.md:37 (Provenance row 'One record per answer joining them'); no join type found NOT-RECOVERABLE human-review absence claim; closed search = lance-graph/crates diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/gate-a-b-record.md b/.claude/probes/2026-11-11-codegraph-recon-1/gate-a-b-record.md new file mode 100644 index 000000000..469ff581a --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/gate-a-b-record.md @@ -0,0 +1,82 @@ +# EXO-229 Gate A — lance-graph-dt64 through Charon → ruff_charon → Codegraph + +## Identity +- source revision: lance-graph c70e7d8 (dt64 + contract trees identical to origin/main 9f4563b) +- charon: AdaWorldAPI/charon c69e231, toolchain nightly-2026-09-17; cargo-miri absent → default sysroot (std/core bodies opaque) +- crate instance: lance-graph-dt64 lib target only, default features, x86_64-unknown-linux-gnu +- ruff_charon: `import` (rows.tsv #version 2, files.tsv fnv64, rows.bin, effects.tsv, residuals.tsv) +- reader: `lance-graph-codegraph` via the new read-only example `cg_query` + +## Cost +- charon LLBC: 29 s; ruff_charon import: 1.2 s; `Codegraph::open` + one query: 4–6 ms +- full sweep of `impact` over all 735 positions: 3.7 s wall, i.e. ~5 ms per process launch + +## Facts recovered +| predicate | rows | +|---|---| +| CALLS_RESOLVED | 1355 | +| DEFINES | 517 | +| PUBLIC | 370 | +| IMPLEMENTS | 347 | +| SYNTHETIC | 26 | +| MAY_DISPATCH | 10 | +| REFERENCES | 8 | +| CRATE | 1 | +residuals: 0 rows (header only). effects: present (e.g. `Overflow:Mul` asserts). + +Observed files: `src/dr.rs`, `src/lane.rs`, `src/lib.rs`. **Unobserved:** `tests/*.rs`, `examples/`, benches, every other crate. + +## Cube limits (measured, not assumed) +- 735 positions (517 defined + external callees), `open` did not refuse. +- `impact` over all 735: **0 refusals** (no ClosureWidth(64), no TooMany(256) at this size); 381 non-empty, 354 empty. +- Conclusion: the limits are not exercised by a 500-symbol crate. A larger crate or a multi-crate store is needed to observe them; this run cannot be cited as "limits never bind". + +## Answer-key checks +| question | Codegraph | source | verdict | +|---|---|---|---| +| callers of `LaneBinding::check` | `lane` (lane.rs:360), `borrow_all` (lane.rs:386), CONFIRMED | same 2 in-crate; plus ≥8 in `tests/lane_socket.rs` (227, 277, 314, 373, 403, 407, 424, …) | in-crate exact; test callers **unobserved and not reported as such** | +| callees of `LaneBinding::check` | `admit_lane`, `source_owns`, `current_route`, `FrameStore::check`, `BindStore::resolve_counted`, `LaneAddr::eq`, `Vec::into_iter` (25 sites) | matches lane.rs body | correct | +| impact of `BindStore::resolve_counted` | `check`, `lane`, `borrow_all` | correct transitive in-crate set | correct | +| callers/impact of `BindStore::admit`, `method_ref` | **empty**, rc=0 | ~140 call sites across ~20 files in other crates (quack `bind.rs`, r2il tests, report, dir-rmap, probes, labs …) | **false unaffected** | +| dynamic dispatch | 10 MAY_DISPATCH rows, e.g. `ClassView::fields_at via Clause`, `LaneSource::borrow via Clause` | trait-object / generic calls in lane.rs | kept POSSIBLE, never CONFIRMED | + +## The finding +261 of 370 `PUBLIC` symbols return an empty `impact` set (339 of 517 defined symbols overall). +The store already carries both facts needed to say "open beyond this crate" — the `PUBLIC` row and the +observed-files list — but `Codegraph::impact` returns `Graded { confirmed, possible, unknown }` with +`unknown` empty. Under crai-rs CR-H0 ("UNKNOWN is a value, not an absence"; "false unaffected is more +severe than UNKNOWN") this is the most serious defect found: an empty answer that reads as "nothing +depends on this". + +Fix shape, not applied (no Codegraph API change in this mission): a reader-side rule — a `PUBLIC` +symbol whose crate artifact is the only one loaded gets `unknown = {EXTERNAL_CALLERS_UNOBSERVED}`; any +query result carries the observed-file set so test callers show as not covered. `cg_query` can print +this today from `PUBLIC` + `files.tsv` without touching the library. + +## Not covered by this gate +- test and example targets (charon was run on the lib target only) +- other crates' calls into dt64 (needs one artifact per consumer crate) +- macro-expanded bodies are in LLBC, but their spans point at the macro call site +- std/core bodies (opaque: no miri sysroot) + +# Gate B — four-crate store (dt64 + contract + quack + r2il), same charon/ruff_charon config + +| crate | charon s | import s | harvested | represented | residual | +|---|---|---|---|---|---| +| lance-graph-contract | 21 | 7 | 31015 | 31014 | 1 (`REFERENCE_NOT_NAMED rung_schedule::requires_of`) | +| lance-graph-quack | 14 | 1 | 1796 | 1796 | 0 | +| lance-graph-r2il | 7 | 1 | 2319 | 2319 | 0 | +| lance-graph-dt64 (Gate A) | 29 | 1.2 | — | — | 0 | + +- 9,138 positions; `open` + `symbols` 159 ms. In-process sweep of `impact` + `callers` over all + positions: **1,224 ms, 0 refusals** (9,569 answered, 8,707 empty). +- **Correction to the brief:** `ClosureWidth(64)` and the 256-id tile bound belong to the + single-tile `Cube::closure`. Codegraph on main builds `Cube::new_tiled` and answers with + `closure_wide` (`lance-graph-xlog/src/wide.rs`, `MAX_POSITIONS = 2^20 − 256`). They are not + the limits a Codegraph query meets. The sweep's refusal arm is not disable-proven by this store + (nothing refuses); the crate's own `Inject::Closure` / `Inject::Stage` tests cover that plumbing. +- **Cross-crate edge recovered:** `lance_graph_r2il::binding::prepare → BindStore::admit`, CONFIRMED. + `method_ref` still has no observed caller (its callers are in tests/probes/labs, unloaded). +- **Grep false positive caught by the compiler arm:** `lance-graph-quack/src/bind.rs` has five + `.admit(` calls; they are quack's own test-only typed code space, and quack does not depend on + dt64. A name grep counts them as DT64 users; Codegraph correctly does not. diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/machine-recovered.mmd b/.claude/probes/2026-11-11-codegraph-recon-1/machine-recovered.mmd new file mode 100644 index 000000000..6bcddecc6 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/machine-recovered.mmd @@ -0,0 +1,156 @@ +flowchart LR +%% machine-recovered from compiler facts only; no curated edge +classDef stale fill:#fdd,stroke:#c00 +classDef unknown fill:#eee,stroke:#888,stroke-dasharray:3 3 + n2324220d2d["impl_Clone_for_WideFieldMask::clone"] + nf0dd7eb4d4["WideFieldMask::count"] + n0fe9c0c703["WideFieldMask::has"] + n6effced490["ogar_codebook::classid_concept"] + n5880d6a6d2["impl_PartialEq_Truth_for_Truth::eq"] + n85f692868e["lance_graph_dt64::basis_at"] + n5c9d9be11c["lance_graph_dt64::basis_key"] + n30c0933001["lance_graph_dt64::check_basis"] + n9a358a34e7["impl_Clone_for_Frame::clone"] + ncea87a6cc8["impl_Clone_for_Guards::clone"] + n23b6de894b["FrameStore::check"] + nb3e6a1cf11["FrameStore::revisions"] + n139286eb5c["Guards::check"] + nc7b837b3cb["impl_Clone_for_MethodRef::clone"] + n7fb6db5dce["impl_PartialEq_ClassEntry_for_ClassEntry::eq"] + n41d921fb1f["impl_PartialEq_GuardWitness_for_GuardWitness::eq"] + nfb81872bac["LaneSource::borrow"] + nc321749ee8["LaneSource::lane_of"] + neffab0ab1b["lane::admit_lane"] + n8e44b69cf6["lane::current_route"] + nf82f64d778["impl_Iterator_for_BoundLanes::next"] + nf14d98b062["impl_PartialEq_LaneAddr_for_LaneAddr::eq"] + n834e7f0057["lane::source_owns"] + n2d47678468["BindStore::bind_lanes"] + n7c402f07e0["LaneBinding::addr"] + nd3c67ef2b2["LaneBinding::borrow_all"] + n6ee36d71b5["LaneBinding::check"] + n11cbb761a0["LaneBinding::lane"] + na638ff5529["lance_graph_dt64::validate"] + nc9fd69b271["BasisDigest::of"] + nca939019e2["BindStore::admit"] + n77e7ca84bd["BindStore::arity"] + ne8f5ae53b5["BindStore::bound_basis"] + n3b3358f47f["BindStore::check_issuer"] + nd976eba76b["BindStore::insert"] + n0bf65fd17d["BindStore::method_ref"] + n56217912b2["BindStore::register"] + n628dec15fb["BindStore::resolve"] + n728b4e948f["BindStore::resolve_counted"] + nff6be43a65["BindStore::routed_at"] + necac4f0cca["Guard::witness"] + nb80f13b646["exec::execute_compiled"] + nb1030f7f31["exec::scratch_words_for"] + nae37e07664["exec::tile_words_for"] + n6cce1c48bd["Scratch<'a>::over"] + nb940628aab["impl_Clone_for_Program::clone"] + n603aa31300["CompiledProgram::compiled"] + nf52b6be669["CompiledProgram::new"] + n448472ea7d["binding::call_step"] + nbb79e9a73c["binding::check_compare"] + nb950916031["binding::check_route"] + nab16acdce2["impl_Clone_for_Prepared::clone"] + na70926968a["binding::lane"] + n6f2b33fcea["binding::plan_id"] + n9f0aa095b5["binding::prepare"] + n394d8cf7a9["binding::run"] + n5e4579653e["binding::run_steps"] + nd18e8d838f["binding_native::prepare_native"] + n3a26fe8187["binding_native::run_native"] + nb0f12d5420["binding_native::shape_of"] + n07a94d728c["FoldDialect<'p>::discard_pending"] + n7422030821["FoldDialect<'p>::last_program"] + n3e900d22cd["FoldDialect<'p>::new"] + n8fa0cd24a9["FoldDialect<'p>::programs_run"] + nf82f64d778 -.->|possible| nfb81872bac %% crates/lance-graph-dt64/src/lane.rs:408 + n2d47678468 --> n2324220d2d %% crates/lance-graph-dt64/src/lane.rs:212 + n2d47678468 --> nf0dd7eb4d4 %% crates/lance-graph-dt64/src/lane.rs:191 + n2d47678468 --> n0fe9c0c703 %% crates/lance-graph-dt64/src/lane.rs:193 + n2d47678468 --> n9a358a34e7 %% crates/lance-graph-dt64/src/lane.rs:209 + n2d47678468 --> n23b6de894b %% crates/lance-graph-dt64/src/lane.rs:179 + n2d47678468 -.->|possible| nc321749ee8 %% crates/lance-graph-dt64/src/lane.rs:199 + n2d47678468 --> neffab0ab1b %% crates/lance-graph-dt64/src/lane.rs:202 + n2d47678468 --> n8e44b69cf6 %% crates/lance-graph-dt64/src/lane.rs:186 + n2d47678468 --> n834e7f0057 %% crates/lance-graph-dt64/src/lane.rs:178 + n2d47678468 --> ne8f5ae53b5 %% crates/lance-graph-dt64/src/lane.rs:188 + n2d47678468 --> n628dec15fb %% crates/lance-graph-dt64/src/lane.rs:187 + n2d47678468 --> nff6be43a65 %% crates/lance-graph-dt64/src/lane.rs:180 + nd3c67ef2b2 --> n6ee36d71b5 %% crates/lance-graph-dt64/src/lane.rs:386 + n6ee36d71b5 --> n23b6de894b %% crates/lance-graph-dt64/src/lane.rs:315 + n6ee36d71b5 -.->|possible| nc321749ee8 %% crates/lance-graph-dt64/src/lane.rs:336 + n6ee36d71b5 --> neffab0ab1b %% crates/lance-graph-dt64/src/lane.rs:346 + n6ee36d71b5 --> n8e44b69cf6 %% crates/lance-graph-dt64/src/lane.rs:316 + n6ee36d71b5 --> nf14d98b062 %% crates/lance-graph-dt64/src/lane.rs:337 + n6ee36d71b5 --> n834e7f0057 %% crates/lance-graph-dt64/src/lane.rs:314 + n6ee36d71b5 --> n728b4e948f %% crates/lance-graph-dt64/src/lane.rs:324 + n11cbb761a0 -.->|possible| nfb81872bac %% crates/lance-graph-dt64/src/lane.rs:362 + n11cbb761a0 --> n7c402f07e0 %% crates/lance-graph-dt64/src/lane.rs:361 + n11cbb761a0 --> n6ee36d71b5 %% crates/lance-graph-dt64/src/lane.rs:360 + nca939019e2 --> n41d921fb1f %% crates/lance-graph-dt64/src/lib.rs:1204 + nca939019e2 --> n3b3358f47f %% crates/lance-graph-dt64/src/lib.rs:1210 + nca939019e2 --> necac4f0cca %% crates/lance-graph-dt64/src/lib.rs:1204 + nd976eba76b --> n85f692868e %% crates/lance-graph-dt64/src/lib.rs:871 + nd976eba76b --> n5c9d9be11c %% crates/lance-graph-dt64/src/lib.rs:880 + nd976eba76b --> n7fb6db5dce %% crates/lance-graph-dt64/src/lib.rs:905 + nd976eba76b --> na638ff5529 %% crates/lance-graph-dt64/src/lib.rs:851 + nd976eba76b --> nc9fd69b271 %% crates/lance-graph-dt64/src/lib.rs:879 + nd976eba76b --> n77e7ca84bd %% crates/lance-graph-dt64/src/lib.rs:855 + n56217912b2 --> nd976eba76b %% crates/lance-graph-dt64/src/lib.rs:821 + n628dec15fb --> n30c0933001 %% crates/lance-graph-dt64/src/lib.rs:1083 + n9f0aa095b5 --> n6effced490 %% crates/lance-graph-r2il/src/binding.rs:341 + n9f0aa095b5 --> n5880d6a6d2 %% crates/lance-graph-r2il/src/binding.rs:338 + n9f0aa095b5 --> ncea87a6cc8 %% crates/lance-graph-r2il/src/binding.rs:361 + n9f0aa095b5 --> n139286eb5c %% crates/lance-graph-r2il/src/binding.rs:329 + n9f0aa095b5 --> nc7b837b3cb %% crates/lance-graph-r2il/src/binding.rs:358 + n9f0aa095b5 --> nca939019e2 %% crates/lance-graph-r2il/src/binding.rs:334 + n9f0aa095b5 --> n628dec15fb %% crates/lance-graph-r2il/src/binding.rs:331 + n9f0aa095b5 --> nb950916031 %% crates/lance-graph-r2il/src/binding.rs:330 + n9f0aa095b5 --> n6f2b33fcea %% crates/lance-graph-r2il/src/binding.rs:356 + n394d8cf7a9 --> n139286eb5c %% crates/lance-graph-r2il/src/binding.rs:389 + n394d8cf7a9 --> n3b3358f47f %% crates/lance-graph-r2il/src/binding.rs:386 + n394d8cf7a9 --> nb950916031 %% crates/lance-graph-r2il/src/binding.rs:392 + n394d8cf7a9 --> n5e4579653e %% crates/lance-graph-r2il/src/binding.rs:397 + n394d8cf7a9 --> n07a94d728c %% crates/lance-graph-r2il/src/binding.rs:396 + n394d8cf7a9 --> n07a94d728c %% crates/lance-graph-r2il/src/binding.rs:398 + nd18e8d838f --> n139286eb5c %% crates/lance-graph-r2il/src/binding_native.rs:214 + nd18e8d838f --> n3b3358f47f %% crates/lance-graph-r2il/src/binding_native.rs:211 + nd18e8d838f --> nb1030f7f31 %% crates/lance-graph-r2il/src/binding_native.rs:323 + nd18e8d838f --> nae37e07664 %% crates/lance-graph-r2il/src/binding_native.rs:320 + nd18e8d838f --> nb940628aab %% crates/lance-graph-r2il/src/binding_native.rs:263 + nd18e8d838f --> nf52b6be669 %% crates/lance-graph-r2il/src/binding_native.rs:277 + nd18e8d838f --> n448472ea7d %% crates/lance-graph-r2il/src/binding_native.rs:250 + nd18e8d838f --> nbb79e9a73c %% crates/lance-graph-r2il/src/binding_native.rs:247 + nd18e8d838f --> nb950916031 %% crates/lance-graph-r2il/src/binding_native.rs:217 + nd18e8d838f --> nab16acdce2 %% crates/lance-graph-r2il/src/binding_native.rs:331 + nd18e8d838f --> na70926968a %% crates/lance-graph-r2il/src/binding_native.rs:229 + nd18e8d838f --> nb0f12d5420 %% crates/lance-graph-r2il/src/binding_native.rs:333 + nd18e8d838f --> n7422030821 %% crates/lance-graph-r2il/src/binding_native.rs:263 + nd18e8d838f --> n3e900d22cd %% crates/lance-graph-r2il/src/binding_native.rs:218 + nd18e8d838f --> n8fa0cd24a9 %% crates/lance-graph-r2il/src/binding_native.rs:249 + nd18e8d838f --> n8fa0cd24a9 %% crates/lance-graph-r2il/src/binding_native.rs:259 + n3a26fe8187 --> nb3e6a1cf11 %% crates/lance-graph-r2il/src/binding_native.rs:412 + n3a26fe8187 --> n139286eb5c %% crates/lance-graph-r2il/src/binding_native.rs:364 + n3a26fe8187 --> n3b3358f47f %% crates/lance-graph-r2il/src/binding_native.rs:361 + n3a26fe8187 --> nb80f13b646 %% crates/lance-graph-r2il/src/binding_native.rs:385 + n3a26fe8187 --> n6cce1c48bd %% crates/lance-graph-r2il/src/binding_native.rs:384 + n3a26fe8187 --> n603aa31300 %% crates/lance-graph-r2il/src/binding_native.rs:386 + n3a26fe8187 --> nb950916031 %% crates/lance-graph-r2il/src/binding_native.rs:367 + n3a26fe8187 --> nb0f12d5420 %% crates/lance-graph-r2il/src/binding_native.rs:371 + nf82f64d778_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nf82f64d778 + n2d47678468_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n2d47678468 + nd3c67ef2b2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nd3c67ef2b2 + n6ee36d71b5_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n6ee36d71b5 + n11cbb761a0_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n11cbb761a0 + nca939019e2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nca939019e2 + n3b3358f47f_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n3b3358f47f + n0bf65fd17d_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n0bf65fd17d + n56217912b2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n56217912b2 + n628dec15fb_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n628dec15fb + n9f0aa095b5_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n9f0aa095b5 + n394d8cf7a9_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n394d8cf7a9 + nd18e8d838f_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nd18e8d838f + n3a26fe8187_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n3a26fe8187 diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/GRADES.tsv b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/GRADES.tsv new file mode 100644 index 000000000..600edd781 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/GRADES.tsv @@ -0,0 +1,81 @@ +file q verdict coverage_honest reason +X30 Q1 PARTIAL yes Definition and all 35 crates/ impl sites listed with lib/test split; minor slip: states "36 + 1 doc" impls while its own list has 37 (35 crates + 2 .claude); no compiler-index scope note (text-only method). +X30 Q2 PARTIAL yes All 16 dependents correct; minor slip: says all are normal except dir-sim, but math-polyfill-probe/Cargo.toml:30 is also [dev-dependencies]. +X30 Q3 CORRECT yes lane.rs:360/386, lane_socket 7 sites, report tests 320/341/418/623, dir-sim 1328; false friends excluded; transitive lab callers true. +X30 Q4 CORRECT yes Callees check_issuer/Guard::witness/eq; r2il prepare plus lab/probe/test callers of admit and method_ref receiver-checked; collisions excluded; sibling repos stated unsearched. +X30 Q5 CORRECT yes Full prepare sequence guards->route->resolve->admit(334)->when/three-valued refusals->lens->effects->Prepared; prepare_native consumes Prepared. +X30 Q6 CORRECT yes r2il prepare refuses any when (335-336); lab lowering in foundry PreparedMethod and grammar compose (true; see key error 2). +X30 Q7 CORRECT yes No path; ScopedDecision authorize.rs:170; dt64/rbac deps; dir-sim only via patch/ogar-rbac; WideFieldMask manual bridge only (walk_rails covered in Q10). +X30 Q8 PARTIAL yes True text counts (505 lines/49 files/23 crates; 101/22/11) with scope caveats; no compiler-resolved counts and no code/test/doc split. +X30 Q9 CORRECT yes Known callees incl admit_lane/LaneAddr compare, callers 360/386; possible ClassView/LaneSource dispatch with 7 impls; unknowns stated. +X30 Q10 CORRECT yes Gap nodes PERMIT/ONE/G2A/G2B/ISS/JOIN, SD-->RAIL not a call (closure), status/PR and design-intent claims all classified as not recoverable. +X44 Q1 CORRECT yes Definition and all 35 impl sites with lib/test split; AiwarClassView flagged UNKNOWN (it has no trait impl); OGAR impl noted external. +X44 Q2 CORRECT yes All 16 with Cargo.toml lines; dev/normal split explicitly not examined. +X44 Q3 CORRECT yes All direct callers incl tests; collisions excluded; indirect lane/borrow_all callers listed. +X44 Q4 PARTIAL yes Callees correct; method_ref callers omit r2il tests, grammar, report, dir-sim, xlog-relcomp, dt64-admission fixture; admit callers omit dt64-admission-probe/src/lib.rs:182 and r2il/report/dir-sim tests; grammar line given as 424 (actual 421). +X44 Q5 CORRECT yes Steps register->route->method_ref->Resolution->prepare checks a-h->prepare_native->run, all true. +X44 Q6 CORRECT yes Foundry and grammar lab lowering, r2il refusal at 335-337 and test 644; unopened candidates listed. +X44 Q7 CORRECT yes No path; no common direct dep; walk_rails closure; dir-sim patch-only/ogar-rbac external (visible_fields line 184 vs 193 is a citation slip). +X44 Q8 PARTIAL yes True text counts per crate; no compiler-resolved counts or code/test/doc split. +X44 Q9 PARTIAL yes Callees/callers/LaneSource impls correct; minor false count "40+ impls" of ClassView (35 in crates/). +X44 Q10 CORRECT yes Gap/absence nodes, SD-->RAIL closure-only, data-flow-through-caller, cross-repo, status labels classified. +X50 Q1 CORRECT yes Definition + RA 13 impls in 9 files with scope (workspace members, cfg(test) off), notes excluded crates/cfg(test) missed. +X50 Q2 CORRECT yes All 16 with correct normal/dev split (dir-sim, math-polyfill dev); line refs are root Cargo.toml member lines. +X50 Q3 PARTIAL yes Confirmed 2 in-crate callers; test callers left UNKNOWN (honestly explained as cfg(test)/macro gaps); key test sites missing. +X50 Q4 CORRECT yes Callees incl check_issuer/Guard::witness/GuardWitness::eq; admit<-prepare; method_ref <- 4 r2il test helpers; beyond-scope callers stated unobserved. +X50 Q5 CORRECT yes Prepare chain correct; adds true fact register_derived->insert (lib.rs:826/840). +X50 Q6 CORRECT yes None lower via dt64/r2il; refusal at 335-336; foundry lab named as unobserved excluded crate. +X50 Q7 CORRECT yes No path in facts; shared WideFieldMask only; rbac dependents incl dir-sim (consistent with key); scope stated. +X50 Q8 PARTIAL yes RA counts match key (WideFieldMask 179/52/17/11; MethodBinding 27/17/2) with src/test split; no doc-only/excluded-mention split. +X50 Q9 CORRECT yes Callees, callers, MAY_DISPATCH lane_of and ClassView dispatch, unknowns (tests, excluded crates, external). +X50 Q10 CORRECT yes Gaps, SD-->RAIL not a call, xlog bag_count not calling admit, "only way" exclusivity contradicted, status labels. +X54 Q1 PARTIAL yes Full 35 list + .claude copies; minor misclassification: lance-graph-codegraph publication.rs:65 PubView put under cfg(test)/test, it is lib code. +X54 Q2 CORRECT yes 14 from index + 2 missing found in source = 16; .claude probes separate; dir-sim dev noted. +X54 Q3 CORRECT yes All direct and indirect callers; collisions excluded (RouteLog::check location cited wrong but excluded correctly). +X54 Q4 PARTIAL yes Callees and callers broadly complete; minor slip: lance-graph-report/src/lane_source/tests.rs:258 listed among "non-test source" method_ref callers. +X54 Q5 CORRECT yes Steps correct incl register_derived mention, admit at 334, refusals, opcode, Prepared, native/run. +X54 Q6 CORRECT yes r2il refusal; foundry and grammar lab lowering with refusal variants; unread parts stated. +X54 Q7 CORRECT yes No code path; deps; walk_rails closure; type-level WideFieldMask seam; citation slips only (visible_fields :184, dir-sim Cargo.toml:39). +X54 Q8 PARTIAL yes True text counts incl .claude (51 files/513 lines; 24/116); no compiler-resolved counts or code/test/doc split. +X54 Q9 CORRECT yes Callees in order, callers, dyn/LaneSource possibilities with 7 impls, unknowns. +X54 Q10 PARTIAL yes Gap edges, status, cross-repo, data-flow classified; omits the drawn solid SD --> walk_rails_authorized edge. +X66 Q1 CORRECT yes Definition + exactly 35 impl sites under crates/ with lib/lab/test split; OGAR impl external. +X66 Q2 CORRECT yes 14 normal + 2 dev = 16, correct split; ogar-behavior-probe declares but never imports dt64 (true). +X66 Q3 CORRECT yes All direct callers incl tests and dir-sim; indirect lab callers; name collision noted. +X66 Q4 CORRECT yes Complete callees and receiver-checked callers of both, free fn method_ref distinguished, collisions excluded, bag_count_admitted noted. +X66 Q5 CORRECT yes Full chain incl insert validation, route, Resolution, prepare checks, prepare_native, run. +X66 Q6 CORRECT yes Foundry and grammar lab lowering; r2il refusal; relalg/Kleene unknowns stated. +X66 Q7 PARTIAL yes Conclusion and evidence correct (incl walk_rails only called by its own test, true); minor slip: calls dir-sim's Cargo.toml:78 a dev-dep, it is a [patch] entry. +X66 Q8 PARTIAL yes True text counts plus true non-comment split (430/42, 79/17); no compiler-resolved counts or test-only split. +X66 Q9 CORRECT yes Callees, callers, dispatch possibilities (~35 ClassView, 7 LaneSource), unknowns. +X66 Q10 CORRECT yes Gaps incl one executor/row scope/visible_fields/one record, SD-->RAIL solid-but-not-code, status, cross-repo, data flow. +X68 Q1 CORRECT yes Definition + RA 13 impls with scope; excluded crates/cfg-gated impls stated unobserved. +X68 Q2 CORRECT yes All 16 with correct normal/dev split and workspace membership. +X68 Q3 PARTIAL yes 2 confirmed callers; test callers not observed and explicitly not claimed absent (macro regions, excluded crates). +X68 Q4 CORRECT yes method_ref <- 4 r2il test helpers, admit <- prepare, callees incl check_issuer/Guard::witness/GuardWitness::eq; excluded callers stated unobserved. +X68 Q5 CORRECT yes Prepare chain with lines; prepare_native separate; register callers not traced (stated). +X68 Q6 CORRECT yes None observed lowering via dt64/r2il; refusal 335-337; foundry bridge UNKNOWN (excluded). +X68 Q7 PARTIAL yes No observed path, correct; minor slip: "rbac [dependencies] :78" for dir-sim, line 78 is under [patch."...lance-graph"]. +X68 Q8 PARTIAL yes RA counts match key exactly (259/179,52,11,17; 46/27,17,2) with src/tests/examples split; no doc-only mentions. +X68 Q9 CORRECT yes Confirmed callees/callers, MAY_DISPATCH lane_of and ClassView targets, unknowns. +X68 Q10 CORRECT yes DYN/TYPE/NEG/XREPO classification; gap nodes; SD-->RAIL not an observed call; status labels. +X84 Q1 CORRECT yes RA 13 with scope plus 22 source-only sites (=35) explicitly attributed to excluded crates/examples/cfg(test). +X84 Q2 CORRECT yes 16 dependents with correct dev split (dir-sim, math-polyfill); index gaps noted. +X84 Q3 CORRECT yes Confirmed 2 + all test sites with reason RA misses them; indirect callers. +X84 Q4 CORRECT yes Callees and callers (RA + receiver-checked source) for both, incl r2il test 536/641 for admit; external unknown. +X84 Q5 CORRECT yes Steps correct; only compiler edge prepare->admit identified. +X84 Q6 CORRECT yes Foundry/grammar/set_lower lowering, r2il refusal, admit witness checks. +X84 Q7 CORRECT yes No path; no crate with both deps directly; dir-sim patch-only; walk_rails closure. +X84 Q8 CORRECT yes RA counts match key with src/test file split, plus text counts (51/24 files) flagged as including docs/comments. +X84 Q9 PARTIAL yes Callees/callers/7 LaneSource impls correct; minor slip: claims the Charon store dropped LaneSource::lane_of, key records it as MAY_DISPATCH. +X84 Q10 CORRECT yes Gaps (G), SD-->RAIL no call edge (F), protocol/ordering, status, cross-repo. +X93 Q1 CORRECT yes Definition, 35 source impl sites with split, RA 13 with scope and the 22 it misses. +X93 Q2 PARTIAL yes 16 with correct dev split; minor false aside: "only lance-graph-dt64-lance is excluded", but most lab/probe dependents and codegraph are in root exclude. +X93 Q3 CORRECT yes Confirmed 2 + all test sites, with RA macro-region explanation. +X93 Q4 PARTIAL yes Callees right; method_ref grep counts dt64-admission tests' free fixture fn method_ref (14+1) as call sites without distinguishing; admit list omits dt64-admission-probe lib.rs:182, bench.rs:181, xlog-relcomp test. +X93 Q5 CORRECT yes Prepare chain correct with compiler confirmation. +X93 Q6 CORRECT yes r2il refusal; foundry/grammar/set_lower lowering; unknowns stated. +X93 Q7 CORRECT yes Not observed; deps; dir-sim patch; WideFieldMask seam (visible_fields :184 citation slip). +X93 Q8 PARTIAL yes RA counts (40+6/7 files; 244+14+1/16 files) and true text counts incl .claude; no per-crate RA numbers or src/test/doc split. +X93 Q9 CORRECT yes Callees with refusals, LaneSource/ClassView possibilities, unknowns. +X93 Q10 CORRECT yes Gaps, SD-->RAIL caller-supplied mask, ordering, "only way" claims, status, cross-repo. diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/NOTES.md b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/NOTES.md new file mode 100644 index 000000000..692285fa1 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/NOTES.md @@ -0,0 +1,50 @@ +# Grading notes (D-CODEGRAPH-RECON-1, blind) + +Source checked: /home/user/lance-graph working tree (HEAD 40c138ca1), read only. + +## Per-file totals + +| file | correct | partial | wrong | coverage-honest | +|---|---|---|---|---| +| X30 | 7 | 3 | 0 | 10/10 | +| X44 | 7 | 3 | 0 | 10/10 | +| X50 | 8 | 2 | 0 | 10/10 | +| X54 | 6 | 4 | 0 | 10/10 | +| X66 | 8 | 2 | 0 | 10/10 | +| X68 | 7 | 3 | 0 | 10/10 | +| X84 | 9 | 1 | 0 | 10/10 | +| X93 | 7 | 3 | 0 | 10/10 | + +## How the rules were applied + +- WRONG was kept for a false member of the answer set (a non-caller listed as a caller, a non-dependent, a non-impl), a false count of the answer set, or "none" where items exist. No cell met that bar. +- A peripheral false statement was marked PARTIAL and named in the reason. Examples: dependency kind (X30 Q2, X66 Q7, X68 Q7), a test/lib bucket (X54 Q1, X54 Q4), a supporting count (X30 Q1, X44 Q9), a workspace-membership aside (X93 Q2), a tool-output claim (X84 Q9). +- Line-number citation slips were noted and not penalised. Examples: visible_fields :184 (actual 193), grammar when.rs:424 (actual 421), RouteLog::check placed at lib.rs:1045 (actual dr.rs:268). +- Q1, Q4: the key's full-credit rule accepts a scoped count. A compiler-only answer that gives the RA 13 impls / the RA callers and states that excluded crates and cfg(test) code were unobserved was graded CORRECT. A text-search answer that gives the full 35-site list with a lib/test split was also graded CORRECT. +- Q8: CORRECT needs compiler-resolved counts with their scope, plus a code / test / doc split. Text-only counts are true in every file, but those answers were graded PARTIAL. Of the RA-count answers, only X84 also gives the text superset with its doc caveat. +- Q10: no answer reproduces the corpus row counts (24 GAP / 61 INTERPRETATION). Full credit was given for naming the gap nodes (PERMIT, ONE, G2A, G2B, ISS, JOIN), the solid SD --> walk_rails_authorized edge as not a call, and the status/intent claims. + +## Key gaps (true facts in answers that the key does not cover) + +1. `BindStore::register_derived` (dt64 lib.rs:826) also calls `insert` (:840), so `register` is not the only entry (X50, X54). +2. `lance_graph_xlog::bag_count_admitted` (xlog lib.rs:384) takes `&MethodBinding` and never calls `admit`. Its admit happens in the caller, xlog-relcomp-probe/tests/dto_binding.rs:244. +3. Q2 dependency kinds: lance-graph-dir-sim (:51) and math-polyfill-probe (:30) are `[dev-dependencies]`; the other 14 are normal. Five `.claude/probes` manifests also depend on dt64. +4. Q3 transitive callers through `lane` / `borrow_all`: foundry-parity-lab arm_b.rs:155, arm_c.rs:163, method.rs:229; soa64-u64-lab socket.rs:206/207/227; dr-isa-stream-lab gemm/int8/shape/cube. +5. Q9: seven `LaneSource` impls exist in source (dt64 tests lane_socket.rs:91, foundry source.rs:178, soa64 socket.rs:136, dr-isa source.rs:225 and int8.rs:159, report lane_source.rs:143, dir-sim ordinal_chain_lab.rs:1109). RA sees two. +6. Q7/Q10: `walk_rails_authorized` (contract selection.rs:335) has exactly one caller, its own test at selection.rs:689. +7. Q1: lance-graph-codegraph publication.rs:65 `PubView` is library code, not test code. Two further impls sit in .claude/probes (main.rs:72, v2_compose.rs:90). `AiwarClassView` has only an inherent impl. +8. Q4: r2il tests hold 7 `.method_ref(` call sites in 4 files (binding.rs 312/680/721/864, binding_native.rs 313, polyfill.rs 182, polyfill_views.rs 208). The key's "4 r2il test callers" counts the helper functions RA resolves. dt64-admission-probe/src/fixture.rs:221 is a free fn named `method_ref`, and its ~15 test call sites are not direct BindStore::method_ref calls. +9. Q8 text counts (crates/, whole word, includes comments): WideFieldMask 505 lines in 49 files across 23 crates, 430 lines in 42 files excluding `//` lines. MethodBinding 101 lines in 22 files across 11 crates, 79 in 17 excluding `//`. Including .claude, the counts are 513/51 and 116/24. +10. ogar-behavior-probe declares the dt64 dependency but no .rs file names `lance_graph_dt64`. + +## Key errors + +1. **Q4, admit callers.** The key lists "r2il integration tests (RA: polyfill_views::prep, polyfill::mref, binding_native::mref, binding::mref)" as callers of `admit`. Those four helpers call `method_ref`, not `admit`: + - crates/lance-graph-r2il/tests/integration/binding.rs:311-312 `fn mref` → `s.method_ref(...)` + - binding_native.rs:312-313 + - polyfill.rs:181-182 + - polyfill_views.rs:200,208 + The direct `admit` call sites in r2il tests are binding.rs:536 and :641. The key repeats the same four helpers correctly under method_ref, which suggests a copy error. No answer was penalised for it: the compiler-only answers (X50, X68) list admit <- prepare and treat the helpers as transitive callers, which is correct. +2. **Q6, "WHEN evaluation exists only in grammar-constraints-probe (lab)".** This is false. crates/foundry-parity-lab/src/method.rs:217-280 (`PreparedMethod::prepare`) admits the binding, takes `binding.when` (:218), renames `guard.expr` onto bound planes, and lowers it with `rel_from_set` + `run_with_program` into one mask-risc `Program`. It refuses with `Symbolic` or `Folds` otherwise, and the module doc (:9-11) says so. The key's main claim stands: no WHEN guard lowers into R2IL, and binding.rs:335-337 refuses it. Answers that cite foundry lowering were not penalised. + +Imprecision, not counted as an error: Q7 says lance-graph-dir-sim "depends on both". dir-sim has no direct lance-graph-rbac dependency. It names it only in `[patch."https://github.com/AdaWorldAPI/lance-graph"]` (Cargo.toml:76-78), which redirects the transitive dependency of the optional OGAR crate `ogar-rbac` (:44, feature `rbac`). The statement holds transitively. Answers that say "patch only, not a dependency" are also true. diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/answer-key.md b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/answer-key.md new file mode 100644 index 000000000..2254269dd --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/answer-key.md @@ -0,0 +1,85 @@ +# D-CODEGRAPH-RECON-1 held-out answer key + +Revision: lance-graph working tree = origin/main 9f4563b for crates/ (plus the cg_query example only). +Built by the orchestrator from source reads, the Charon store (gateB) and the rust-analyzer GRAPH run, +each fact re-read in source. Coverage of each tool is stated, because several answers depend on scope. + +Scoring per question: CORRECT (all key items, no false items), PARTIAL (subset, no false items), +WRONG (any false item stated as fact), plus COVERAGE-HONEST yes/no (did the answer say what it did not see). + +## Q1 Where is ClassView defined, and what implements it? +- Definition: `crates/lance-graph-contract/src/class_view.rs:1057` `pub trait ClassView`. +- Implementations: 35 `impl … ClassView for …` sites in 30 files (syntactic, every crate dir incl. excluded + crates, tests, examples). rust-analyzer resolves 13 of them in 9 files of loaded workspace code; the other 21 + files are excluded crates, examples, cfg(test) unit modules, or test modules inside class_view.rs. +- Full credit needs the definition, an impl count with its scope, and the note that excluded crates / test + modules are outside a compiler index. + +## Q2 Which crates depend on DT64? +- 16 crates declare `lance-graph-dt64 =` in Cargo.toml: cognitive-polyfill-probe, dr-isa-stream-lab, + drisa-register-probe, dt64-admission-probe, foundry-parity-lab, grammar-constraints-probe, + lance-graph-codegraph, lance-graph-dir-sim, lance-graph-dt64-lance, lance-graph-r2il, lance-graph-report, + lance-graph-xlog, math-polyfill-probe, ogar-behavior-probe, soa64-u64-lab, xlog-relcomp-probe. +- NOT a dependent: lance-graph-quack (its `.admit(` calls are its own test-only typed code space). + +## Q3 Who uses LaneBinding::check, including tests? +- In-crate: `lane.rs:360` (`LaneBinding::lane`), `lane.rs:386` (`LaneBinding::borrow_all`). CONFIRMED by Charon and RA. +- Tests: `crates/lance-graph-dt64/tests/lane_socket.rs` 227, 277, 314, 373, 403, 406(-407), 423(-424) — all inside + macro arguments; RA emits no call row for any of them (it marks the macro region); Charon (lib target) does + not see test targets at all. +- `crates/lance-graph-report/src/lane_source/tests.rs` 320, 341, 418 (+1 in the same file) — cfg(test) unit module, + not indexed by RA, not in the Charon lib artifact. +- `crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:1328` — lab test. +- False friends: `dir-rmap-probe` `.check(` calls and dt64 `tests/dr.rs` `g.check` / `store.check` are other types. + +## Q4 What is reachable from BindStore::method_ref / BindStore::admit? +- admit: callees `check_issuer`, `Guard::witness`, `GuardWitness::eq` (CONFIRMED, Charon). Callers observed: + `lance_graph_r2il::binding::prepare` (lib), plus r2il integration tests (RA: polyfill_views::prep, + polyfill::mref, binding_native::mref, binding::mref) and ~140 call sites in ~20 other files (tests, probes, + labs) visible only to source search. +- method_ref: no lib caller in the four compiled crates; 4 r2il test callers (RA); the rest in tests/probes. +- Full credit needs "callers beyond the loaded crates are unobserved", not "none". + +## Q5 How does a MethodBinding get from DT64 to R2IL preparation? +- `lance_graph_r2il::binding::prepare` (`crates/lance-graph-r2il/src/binding.rs:321`): guards.check → check_route → + store.resolve → `store.admit(r.method)` (line 334) returns `&MethodBinding` → refusals on `when` (336) and + three-valued truth (339) → lens check (342) → binds `binding.effects` into `Prepared.steps`. +- `prepare_native` (binding_native.rs) takes a `Prepared`, so it inherits every check above. + +## Q6 Which WHEN guards lower, and where does execution refuse them? +- None lower into R2IL. `prepare` returns `ExecRefusal::GuardNotExecutable` when `binding.when.is_some()` + (`binding.rs:336`). WHEN evaluation exists only in grammar-constraints-probe (lab), not on the R2IL path. + +## Q7 Can a ScopedDecision reach the DT64 lane path? +- No compiled path. `ScopedDecision` is defined in `lance-graph-rbac/src/authorize.rs:170`. dt64, quack, r2il and + report do not depend on lance-graph-rbac. lance-graph-dir-sim depends on both but uses LaneBinding only in a + lab test and never consumes a ScopedDecision. `walk_rails_authorized` takes a caller-supplied `allowed` + closure, not a ScopedDecision. This is a MISSING integration (corpus R326, R417, R422, R430–R435), never an edge. + +## Q8 What changes if WideFieldMask or MethodBinding changes? +- WideFieldMask: RA resolves 259 references in 4 crates (contract 179, dt64 52, rbac 17, r2il 11) of loaded, + non-test code; source search adds cfg(test) modules (e.g. report lane_source/tests.rs, 10 mentions), excluded + crates and doc-only mentions (lance-graph soa_config.rs, lance-graph-ogar recipe_vocab.rs — docs, not code). +- MethodBinding: RA resolves 46 references in 3 crates (dt64 27, r2il 17, xlog 2). +- Full credit needs both counts with their scope and the split between code, test-only and doc-only mentions. + +## Q9 For LaneBinding::check: what is known, possible, unknown? +- Known: 2 in-crate callers; callees admit_lane, source_owns, current_route, FrameStore::check, + BindStore::resolve_counted, LaneAddr::eq. +- Possible: trait-dispatched calls on its generic `V: ClassView` / `S: LaneSource` (Charon MAY_DISPATCH: + `LaneSource::borrow`, `LaneSource::lane_of`, `LaneSource::frames`, `ClassView::fields_at` …). +- Unknown: callers in other crates and in test targets (it is PUBLIC); calls inside macro arguments; + cfg(test) unit modules; excluded crates. + +## Q10 Which Mermaid edges in 03/05/06 cannot be recovered from compiler facts? +- The 24 GAP rows (corpus R261–R265, R276, R322, R323, R326, R426–R438, R442, R444): ExecPermit issuer, one + executor for WHEN and DO, per-row scope lane, visible_fields limiting bound fields, one record per answer. +- The drawn solid edge `ScopedDecision --> walk_rails_authorized` (R417/R422): no call site exists. +- The 61 INTERPRETATION rows (status/plan claims, "only way" claims) are not compiler facts either. + +## Corrections after grading (verified in source by the orchestrator) +- Q4: the four r2il integration-test callers (polyfill_views::prep, polyfill::mref, binding_native::mref, + binding::mref) call `method_ref`, not `admit`. Direct `admit` calls in r2il tests: binding.rs:536, :641. +- Q6: WHEN guards DO lower outside R2IL in the lab: foundry-parity-lab/src/method.rs:218-266 reads + `binding.when` and lowers it via `rel_from_set` + `run_with_program` into a mask-RISC program (LAB). + The key's main claim stands: none lowers into R2IL; `prepare` refuses at binding.rs:336. diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/blind-map.json b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/blind-map.json new file mode 100644 index 000000000..e5bf366e2 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/blind-map.json @@ -0,0 +1 @@ +{"A1": "X66", "A2": "X44", "B1": "X54", "B2": "X30", "C1": "X68", "C2": "X50", "D1": "X93", "D2": "X84"} \ No newline at end of file diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/questions.md b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/questions.md new file mode 100644 index 000000000..f9192674a --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/questions.md @@ -0,0 +1,15 @@ +Answer each question with exact references (path:line, or the symbol identity the tool printed) and end each +answer with a line `COVERAGE: `. Never write "none" or "no callers" unless you +can name the closed search space that proves it; otherwise write UNKNOWN and say what was not observed. + +Q1 Where is the `ClassView` trait defined, and what implements it? +Q2 Which crates depend on lance-graph-dt64? +Q3 Who calls `LaneBinding::check` (lance-graph-dt64/src/lane.rs), including tests? +Q4 What is reachable from `BindStore::method_ref` and `BindStore::admit` (callers and callees)? +Q5 How does a `MethodBinding` get from DT64 into R2IL preparation? Name each step. +Q6 Which WHEN guards lower to an executable form, and where does execution refuse them? +Q7 Can a `ScopedDecision` (lance-graph-rbac) reach the DT64 lane path? Show the path or show why not. +Q8 What code would be affected if `WideFieldMask` or `MethodBinding` changed? Give counts and their scope. +Q9 For `LaneBinding::check`: list what is known (confirmed), possible (e.g. dynamic dispatch) and unknown. +Q10 Which edges drawn in .mermaid/03-dr-dt64-binding.md, 05-methods.md and 06-authorization.md cannot be + recovered from compiler facts (call graph, definitions, references)? Classify each. diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/measurement/usage.tsv b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/usage.tsv new file mode 100644 index 000000000..2efcb6002 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/measurement/usage.tsv @@ -0,0 +1,9 @@ +run tokens tool_calls ms +A2 519347 31 198015 +B1 515749 33 215147 +B2 536113 35 230571 +A1 545985 45 272094 +D1 534740 48 320172 +C2 537291 43 340107 +D2 546203 49 344984 +C1 541365 54 385987 diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/packet-LaneBinding-check.json b/.claude/probes/2026-11-11-codegraph-recon-1/packet-LaneBinding-check.json new file mode 100644 index 000000000..50b4a66fd --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/packet-LaneBinding-check.json @@ -0,0 +1,553 @@ +{ + "packet": "ReviewEvidencePacket (prototype, read-only; not a vendor API)", + "identity": { + "repo_id": "AdaWorldAPI/lance-graph", + "commit_sha": "0c9ae23ac6a20ca6cd0c50da7e7a69e0f5df34eb", + "cargo_lock_sha": "NOT_TRACKED (repository tracks no Cargo.lock)", + "crate_instance": "lance_graph_dt64 (lib target)", + "features": "default", + "target_triple": "x86_64-unknown-linux-gnu", + "rustc_version": "nightly-2026-09-17 (charon)", + "file_blob_sha": "a0aa6e6658872d07c93990095d2fab2beff1487d", + "source_span": { + "file": "crates/lance-graph-dt64/src/lane.rs", + "bytes": [ + 10592, + 12497 + ], + "lines": [ + 307, + 349 + ] + } + }, + "changed_source": { + "subject": "lance_graph_dt64::lane::{LaneBinding}::check", + "base": "0c9ae23ac6a20ca6cd0c50da7e7a69e0f5df34eb", + "diff": "diff --git a/crates/lance-graph-dt64/src/lane.rs b/crates/lance-graph-dt64/src/lane.rs\nindex a0aa6e665..d21a5b602 100644\n--- a/crates/lance-graph-dt64/src/lane.rs\n+++ b/crates/lance-graph-dt64/src/lane.rs\n@@ -312,7 +312,7 @@ impl LaneBinding {\n source: &S,\n ) -> Result<(), LaneRefusal> {\n source_owns(frames, source)?;\n- frames.check(&self.frame).map_err(LaneRefusal::Frame)?;\n+ frames.check(&self.frame).map_err(LaneRefusal::Frame)?; // probe edit\n current_route(store, self.route.position, self.class)?;\n // Revision and count only: the ordered predicate witness was checked\n // when the binding was made (bind_lanes resolves through the\n", + "stale": false, + "freshness": "FRESH", + "dependency_evidence_stale": false + }, + "affected_symbols": { + "confirmed": [ + "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "lance_graph_dt64::lane::{LaneBinding}::lane" + ], + "possible": [], + "stale": [], + "unknown": [ + { + "what": "callers in crates outside the store", + "observed_crates": [ + "lance_graph_contract", + "lance_graph_dt64", + "lance_graph_quack", + "lance_graph_r2il" + ], + "why": "symbol is PUBLIC; only these crates' library targets were compiled" + }, + { + "what": "test targets, examples, cfg(test) modules", + "why": "store holds library targets only" + } + ] + }, + "witnessed_edges": [ + { + "caller": "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "callee": "lance_graph_dt64::lane::{LaneBinding}::check", + "sites": [ + "crates/lance-graph-dt64/src/lane.rs:386" + ], + "fresh": true + }, + { + "caller": "lance_graph_dt64::lane::{LaneBinding}::lane", + "callee": "lance_graph_dt64::lane::{LaneBinding}::check", + "sites": [ + "crates/lance-graph-dt64/src/lane.rs:360" + ], + "fresh": true + } + ], + "possible_edges": [ + { + "dispatch_target": "lance_graph_dt64::lane::LaneSource::lane_of" + } + ], + "co_changed_only": "NOT_RUN (no history projection in this prototype)", + "unsupported_regions": [ + "crates/cognitive-polyfill-probe/tests/p0.rs", + "crates/dir-rmap-probe/tests/equivalence.rs", + "crates/dr-isa-stream-lab/tests/integration/g2l.rs", + "crates/dr-math-binding-probe/tests/binding.rs", + "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs", + "crates/lance-graph-dt64/tests/dr.rs", + "crates/lance-graph-dt64/tests/lane_socket.rs", + "crates/lance-graph-report/src/lane_source/tests.rs", + "crates/thought-git-probe/tests/receipt.rs", + "crates/xlog-relcomp-probe/tests/dto_binding.rs" + ], + "findings": [ + { + "id": "dependents", + "summary": "2 confirmed transitive in-store callers; external callers UNKNOWN", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "confidence": "as graded per item", + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "PARTIAL" + }, + { + "id": "tests", + "summary": "48 candidate test call sites by name; none run", + "severity": null, + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "items": [ + { + "site": "crates/cognitive-polyfill-probe/tests/p0.rs:271", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/cognitive-polyfill-probe/tests/p0.rs:275", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:234", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:238", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:249", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:481", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:522", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:663", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:677", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:678", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:680", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-isa-stream-lab/tests/integration/g2l.rs:136", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-isa-stream-lab/tests/integration/g2l.rs:263", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-math-binding-probe/tests/binding.rs:234", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:162", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:722", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:1012", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:1328", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:58", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:60", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:72", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:82", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:86", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:89", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:90", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:93", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:776", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:777", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:808", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:814", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:824", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:827", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:828", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:227", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:277", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:314", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:369", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:373", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:403", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:407", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:424", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/thought-git-probe/tests/receipt.rs:715", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/thought-git-probe/tests/receipt.rs:715", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/xlog-relcomp-probe/tests/dto_binding.rs:233", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:320", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:341", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:418", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:623", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + } + ], + "provenance": { + "tool": "source search + rust-analyzer GRAPH=1 (ra_ap 0.0.358)" + }, + "lifecycle": "open", + "run_status": "NOT_RUN" + }, + { + "id": "contracts", + "summary": "trait methods the symbol dispatches through (a change may interact with any impl)", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "qualifier": "POSSIBLE", + "items": [ + "lance_graph_dt64::lane::LaneSource::lane_of" + ], + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "COMPLETE" + }, + { + "id": "execution_paths", + "summary": "entry points (in-store callers with no in-store caller)", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "items": [ + "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "lance_graph_dt64::lane::{LaneBinding}::lane" + ], + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "PARTIAL" + } + ], + "r2il": { + "method": "NOT_A_METHOD", + "body_semantics": "UNKNOWN", + "why": "R2IL describes the effects of a registered DT64 MethodBinding (prepare binds them to opcodes); a Rust function found by the compiler is not one, so its body has no R2IL reading" + }, + "expected_behavior": "NOT_SUPPLIED (must come from intent/tests, independently of this packet)", + "candidate_behavior": "NOT_INFERRED", + "missing_necessary_evidence": [ + "test runs (TEST_OBSERVED needs a run that can fail, CR-H0 \u00a75)", + "compiler artifacts of consumer crates and test targets", + "a resolved receiver for each name-matched test site" + ], + "permission_state": "NOT_DERIVED (never from confidence)" +} diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/packet-stale.json b/.claude/probes/2026-11-11-codegraph-recon-1/packet-stale.json new file mode 100644 index 000000000..f07f7b0bd --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/packet-stale.json @@ -0,0 +1,544 @@ +{ + "packet": "ReviewEvidencePacket (prototype, read-only; not a vendor API)", + "identity": { + "repo_id": "AdaWorldAPI/lance-graph", + "commit_sha": "be3cb111149b7f0282ad5b6c8a3d1a3e91a65685", + "cargo_lock_sha": "NOT_TRACKED (repository tracks no Cargo.lock)", + "crate_instance": "lance_graph_dt64 (lib target)", + "features": "default", + "target_triple": "x86_64-unknown-linux-gnu", + "rustc_version": "nightly-2026-09-17 (charon)", + "file_blob_sha": "d21a5b602cc9febb8872d0c0eec4a667a1468d00", + "source_span": { + "file": "crates/lance-graph-dt64/src/lane.rs", + "bytes": [ + 10592, + 12497 + ], + "lines": [ + 307, + 348 + ] + } + }, + "changed_source": { + "subject": "lance_graph_dt64::lane::{LaneBinding}::check", + "base": "be3cb111149b7f0282ad5b6c8a3d1a3e91a65685", + "diff": "diff --git a/crates/lance-graph-dt64/src/lane.rs b/crates/lance-graph-dt64/src/lane.rs\nindex a0aa6e665..d21a5b602 100644\n--- a/crates/lance-graph-dt64/src/lane.rs\n+++ b/crates/lance-graph-dt64/src/lane.rs\n@@ -312,7 +312,7 @@ impl LaneBinding {\n source: &S,\n ) -> Result<(), LaneRefusal> {\n source_owns(frames, source)?;\n- frames.check(&self.frame).map_err(LaneRefusal::Frame)?;\n+ frames.check(&self.frame).map_err(LaneRefusal::Frame)?; // probe edit\n current_route(store, self.route.position, self.class)?;\n // Revision and count only: the ordered predicate witness was checked\n // when the binding was made (bind_lanes resolves through the\n", + "stale": true, + "freshness": "STALE" + }, + "affected_symbols": { + "confirmed": [ + "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "lance_graph_dt64::lane::{LaneBinding}::lane" + ], + "possible": [], + "unknown": [ + { + "what": "callers in crates outside the store", + "observed_crates": [ + "lance_graph_contract", + "lance_graph_dt64", + "lance_graph_quack", + "lance_graph_r2il" + ], + "why": "symbol is PUBLIC; only these crates' library targets were compiled" + }, + { + "what": "test targets, examples, cfg(test) modules", + "why": "store holds library targets only" + } + ] + }, + "witnessed_edges": [ + { + "caller": "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "callee": "lance_graph_dt64::lane::{LaneBinding}::check", + "sites": [ + "crates/lance-graph-dt64/src/lane.rs:385" + ] + }, + { + "caller": "lance_graph_dt64::lane::{LaneBinding}::lane", + "callee": "lance_graph_dt64::lane::{LaneBinding}::check", + "sites": [ + "crates/lance-graph-dt64/src/lane.rs:359" + ] + } + ], + "possible_edges": [ + { + "dispatch_target": "lance_graph_dt64::lane::LaneSource::lane_of" + } + ], + "co_changed_only": "NOT_RUN (no history projection in this prototype)", + "unsupported_regions": [ + "crates/cognitive-polyfill-probe/tests/p0.rs", + "crates/dir-rmap-probe/tests/equivalence.rs", + "crates/dr-isa-stream-lab/tests/integration/g2l.rs", + "crates/dr-math-binding-probe/tests/binding.rs", + "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs", + "crates/lance-graph-dt64/tests/dr.rs", + "crates/lance-graph-dt64/tests/lane_socket.rs", + "crates/lance-graph-report/src/lane_source/tests.rs", + "crates/thought-git-probe/tests/receipt.rs", + "crates/xlog-relcomp-probe/tests/dto_binding.rs" + ], + "findings": [ + { + "id": "dependents", + "summary": "2 confirmed transitive in-store callers; external callers UNKNOWN", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "confidence": "as graded per item", + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "PARTIAL" + }, + { + "id": "tests", + "summary": "48 candidate test call sites by name; none run", + "severity": null, + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "items": [ + { + "site": "crates/cognitive-polyfill-probe/tests/p0.rs:271", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/cognitive-polyfill-probe/tests/p0.rs:275", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:234", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:238", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:249", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:481", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:522", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:663", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:677", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:678", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dir-rmap-probe/tests/equivalence.rs:680", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-isa-stream-lab/tests/integration/g2l.rs:136", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-isa-stream-lab/tests/integration/g2l.rs:263", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/dr-math-binding-probe/tests/binding.rs:234", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:162", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:722", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:1012", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dir-sim/tests/ordinal_chain_lab.rs:1328", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:58", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:60", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:72", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:82", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:86", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:89", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:90", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:93", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:776", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:777", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:808", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:814", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:824", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:827", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/dr.rs:828", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:227", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:277", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:314", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:369", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:373", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:403", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:407", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-dt64/tests/lane_socket.rs:424", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: inside a macro region", + "run_status": "NOT_RUN" + }, + { + "site": "crates/thought-git-probe/tests/receipt.rs:715", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/thought-git-probe/tests/receipt.rs:715", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/xlog-relcomp-probe/tests/dto_binding.rs:233", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:320", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:341", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:418", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + }, + { + "site": "crates/lance-graph-report/src/lane_source/tests.rs:623", + "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", + "why": "method-name match, receiver unresolved", + "ra": "UNKNOWN: file not indexed", + "run_status": "NOT_RUN" + } + ], + "provenance": { + "tool": "source search + rust-analyzer GRAPH=1 (ra_ap 0.0.358)" + }, + "lifecycle": "open", + "run_status": "NOT_RUN" + }, + { + "id": "contracts", + "summary": "trait methods the symbol dispatches through (a change may interact with any impl)", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "qualifier": "POSSIBLE", + "items": [ + "lance_graph_dt64::lane::LaneSource::lane_of" + ], + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "COMPLETE" + }, + { + "id": "execution_paths", + "summary": "entry points (in-store callers with no in-store caller)", + "severity": null, + "evidence_class": "COMPILER_DERIVED", + "items": [ + "lance_graph_dt64::lane::{LaneBinding}::borrow_all", + "lance_graph_dt64::lane::{LaneBinding}::lane" + ], + "provenance": { + "tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", + "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)" + }, + "lifecycle": "open", + "run_status": "PARTIAL" + } + ], + "expected_behavior": "NOT_SUPPLIED (must come from intent/tests, independently of this packet)", + "candidate_behavior": "NOT_INFERRED", + "missing_necessary_evidence": [ + "test runs (TEST_OBSERVED needs a run that can fail, CR-H0 \u00a75)", + "compiler artifacts of consumer crates and test targets", + "a resolved receiver for each name-matched test site" + ], + "permission_state": "NOT_DERIVED (never from confidence)" +} diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/recon.py b/.claude/probes/2026-11-11-codegraph-recon-1/recon.py new file mode 100644 index 000000000..91d112d7f --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/recon.py @@ -0,0 +1,576 @@ +#!/usr/bin/env python3 +"""D-CODEGRAPH-RECON-1: rebuild an architecture diagram from compiler facts, score it against the +hand-curated Mermaid corpus, and emit a read-only review evidence packet. + +Inputs are never written. Commands: + + recover --store DIR --src ROOT --seeds FILE machine-recovered Mermaid (facts only) + score --store DIR --src ROOT --corpus TSV [--ra TSV] recall of the corpus' call edges + reconcile --store DIR --src ROOT --seeds FILE --corpus TSV machine diagram + labelled human rows + packet --store DIR --src ROOT --ra TSV --symbol SYM [--diff FILE] [--rev SHA] + --self-test the D-CODEGRAPH-RECON-1 negatives + +`--store` is a ruff_charon store (`.rows.tsv`, `.files.tsv`). `--ra` is the +`GRAPH=1` output of crates/sag-ra-probe. A missing store is an error (ARTIFACT_MISSING, exit 3), +never an empty diagram. The machine diagram reads the store only: the corpus is not opened by +`recover`, and the seed list names nodes, never edges. +""" + +import argparse +import hashlib +import json +import re +import subprocess +import sys +import tempfile +import unittest +from collections import defaultdict +from pathlib import Path + +CALL = "CALLS_RESOLVED" +MAY = "MAY_DISPATCH" +LOCAL = ("lance_graph_",) # callees outside these prefixes (core, alloc, std) are not drawn + + +class ArtifactMissing(Exception): + pass + + +def fnv64(data): + # Same hash as ruff_charon's files.tsv and .claude/tools/codegraph_index.py. + h = 0xCBF29CE484222325 + for b in data: + h ^= b + h = (h * 0x100000001B3) & 0xFFFFFFFFFFFFFFFF + return f"{h:016x}" + + +def read_schema_tsv(path): + cols, rows = None, [] + for line in path.read_text().splitlines(): + if line.startswith("#schema "): + cols = line[len("#schema "):].split("\t") + elif line and not line.startswith("#"): + rows.append(dict(zip(cols, line.split("\t")))) + return rows + + +class Store: + """The rows of every crate in a ruff_charon store directory, plus file freshness.""" + + def __init__(self, store, src): + store, self.src = Path(store), Path(src) + files = sorted(store.glob("*.rows.tsv")) if store.is_dir() else [] + if not files: + raise ArtifactMissing(f"ARTIFACT_MISSING\tno *.rows.tsv in {store}") + self.crates = [f.name[: -len(".rows.tsv")] for f in files] + self.rows = [r for f in files for r in read_schema_tsv(f)] + self.fresh = {} + for c in self.crates: + ft = store / f"{c}.files.tsv" + if not ft.exists(): + raise ArtifactMissing(f"ARTIFACT_MISSING\t{ft}") + for r in read_schema_tsv(ft): + p = self.src / r["path"] + self.fresh[r["path"]] = ( + "MISSING_SOURCE" if not p.exists() + else "FRESH" if fnv64(p.read_bytes()) == r["fnv64"] else "STALE") + self.public = {r["subject"] for r in self.rows if r["predicate"] == "PUBLIC"} + self.defines = {r["subject"]: r for r in self.rows if r["predicate"] == "DEFINES"} + + def line(self, path, offset): + p = self.src / path + if not p.exists(): + return None + return p.read_bytes()[: int(offset)].count(b"\n") + 1 + + def edges(self): + """(caller, callee, kind, file, line, freshness) for every call row; dispatch rows keep + their target only (`X via Clause` -> X).""" + out = [] + for r in self.rows: + if r["predicate"] not in (CALL, MAY): + continue + callee = r["object"].split(" via ")[0] + out.append((r["subject"], callee, r["predicate"], r["file"], + self.line(r["file"], r["start"]), self.fresh.get(r["file"], "UNOBSERVED"))) + return out + + +def short(sym): + parts = re.sub(r"\{([^}]*)\}", r"\1", sym).split("::") + return "::".join(parts[-2:]) if len(parts) > 1 else sym + + +def node_id(sym): + return "n" + hashlib.sha1(sym.encode()).hexdigest()[:10] + + +def recover(store, seeds): + """Mermaid flowchart of the seeds' direct local callees, from store rows only.""" + seeds = sorted(set(seeds)) + present = [s for s in seeds if s in store.defines] + missing = [s for s in seeds if s not in store.defines] + lines = ["flowchart LR", "%% machine-recovered from compiler facts only; no curated edge", + "classDef stale fill:#fdd,stroke:#c00", "classDef unknown fill:#eee,stroke:#888,stroke-dasharray:3 3"] + nodes, edges = {}, set() + for caller, callee, kind, f, ln, fr in store.edges(): + if caller not in present or not callee.startswith(LOCAL): + continue + nodes[caller] = nodes[callee] = None + edges.add((caller, callee, kind, f, ln, fr)) + for s in present: + nodes[s] = None + for s in sorted(nodes): + lines.append(f' {node_id(s)}["{short(s)}"]') + for caller, callee, kind, f, ln, fr in sorted(edges, key=lambda e: (e[0], e[1], e[2], e[3], e[4] or 0)): + a, b = node_id(caller), node_id(callee) + if fr != "FRESH": + # STALE, MISSING_SOURCE or UNOBSERVED: never drawn as a verified edge. + lines.append(f" {a} -. {fr} .-> {b} %% {f}:{ln if ln is not None else '?'}") + elif kind == MAY: + lines.append(f" {a} -.->|possible| {b} %% {f}:{ln}") + else: + lines.append(f" {a} --> {b} %% {f}:{ln}") + for s in present: + if s in store.public: + u = node_id(s) + "_ext" + lines.append(f' {u}["callers outside {", ".join(store.crates)}: UNKNOWN"]:::unknown -.-> {node_id(s)}') + for s in missing: + lines.append(f' %% seed not in store (UNOBSERVED, not absent): {s}') + return "\n".join(lines) + "\n" + + +def cited_site(cell): + """First `path:line` in a corpus `verified_line` cell, normalised to a repo-relative path.""" + m = re.search(r"((?:crates|OGAR/crates)/[\w./-]+\.rs):(\d+)", cell) + return (m.group(1), int(m.group(2))) if m else None + + +def read_corpus(path): + lines = Path(path).read_text().splitlines() + head = lines[0].split("\t") + return [dict(zip(head, ln.split("\t"))) for ln in lines[1:] if ln.strip()] + + +def ra_calls(ra_path, src): + """(file, line) of every rust-analyzer `call` row, plus the files it saw and its macro regions.""" + sites, files, macros, cache = set(), set(), defaultdict(list), {} + for ln in Path(ra_path).read_text().splitlines(): + p = ln.split("\t") + if p[0] == "file": + files.add(p[1]) + elif p[0] == "macro": + macros[p[1]].append((int(p[2]), int(p[3]))) + elif p[0] == "call": + f, s = p[4], int(p[5]) + if f not in cache: + fp = Path(src) / f + cache[f] = fp.read_bytes() if fp.exists() else b"" + sites.add((f, cache[f][:s].count(b"\n") + 1)) + return sites, files, macros + + +def score(store, corpus, ra=None): + """For every MECHANICAL-CALLGRAPH corpus row, does a compiler call site sit at its cited line + (exact, or within the cited row's following two lines for multi-line calls)?""" + st_sites = {(f, ln) for _, _, _, f, ln, _ in store.edges()} + st_files = set(store.fresh) + ra_sites, ra_files = (ra[0], ra[1]) if ra else (set(), set()) + out = [] + for r in corpus: + if r.get("recoverable") != "MECHANICAL-CALLGRAPH": + continue + site = cited_site(r.get("verified_line", "")) + row = {"id": r["id"], "site": site and f"{site[0]}:{site[1]}"} + for arm, sites, files in (("charon", st_sites, st_files), ("ra", ra_sites, ra_files)): + if arm == "ra" and not ra: + continue + if site is None: + row[arm] = "NO_SITE" + elif site[0] not in files: + row[arm] = "UNOBSERVED" + else: + row[arm] = "HIT" if any((site[0], site[1] + d) in sites for d in (0, 1, 2)) else "MISS" + out.append(row) + return out + + +def reconcile(store, seeds, corpus): + """The machine diagram plus corpus rows that compiler facts cannot carry, each labelled as + human interpretation with its corpus id. A GAP is never drawn as a solid edge.""" + base = recover(store, seeds).rstrip("\n").split("\n") + base += ["%% --- human interpretation (corpus rows; not compiler facts) ---", + "classDef gap fill:#fff3cd,stroke:#b58900,stroke-dasharray:5 5", + "classDef lab fill:#e8f4ff,stroke:#268bd2", + "classDef proposed fill:#f3e8ff,stroke:#6c71c4,stroke-dasharray:2 2", + "classDef contradicted fill:#fdd,stroke:#c00"] + for r in corpus: + rid, status, rec = r["id"], r.get("status", ""), r.get("recoverable", "") + label = re.sub(r'["\[\]{}|<>]', " ", f'{rid}: {r.get("subject", "")} / {r.get("object", "")}')[:90] + if rec == "NOT-RECOVERABLE" or status == "MISSING": + base.append(f' {rid}["{label}"]:::gap') + elif status in ("LAB", "PROPOSED", "OPEN-PR") and rec != "MECHANICAL-CALLGRAPH": + cls = {"LAB": "lab", "PROPOSED": "proposed", "OPEN-PR": "proposed"}[status] + base.append(f' {rid}["{label} ({status})"]:::{cls}') + if "CONTRADICTED" in r.get("verified_line", ""): + base.append(f' {rid}_c["{rid} CONTRADICTED by source; not drawn as an edge"]:::contradicted') + return "\n".join(base) + "\n" + + +def git(src, *args): + try: + return subprocess.run(["git", "-C", str(src), *args], capture_output=True, text=True, check=True).stdout.strip() + except (subprocess.CalledProcessError, FileNotFoundError): + return None + + +def field_readers(store, field): + """(function, path:line) for every DEFINES span whose body text reads `.field` (not a call).""" + pat = re.compile(rb"\.%s\b(?!\s*\()" % re.escape(field.encode())) + out, cache = [], {} + for sym, d in sorted(store.defines.items()): + f = d["file"] + if f not in cache: + fp = store.src / f + cache[f] = fp.read_bytes() if fp.exists() else b"" + body = cache[f][int(d["start"]):int(d["end"])] + for m in pat.finditer(body): + out.append((sym, f"{f}:{cache[f][:int(d['start']) + m.start()].count(b'\n') + 1}")) + return out + + +def packet(store, ra, symbol, diff_text=None, rev=None): + """A read-only ReviewEvidencePacket (crai-rs CR-H0 §3 OUT fields, CR-H1 identity fields, + CR-H0-REVIEW-SEMANTICS axes) for a change to `symbol`. It holds evidence, never a verdict.""" + d = store.defines.get(symbol) + if d is None: + # Not a function: maybe a field (`Type::field`). Compiler facts carry no field reads, so a + # read that sits only in a guard (`if b.when.is_some()`) would vanish from a call graph. + # Report every in-store function body that reads `.field` as SOURCE_STRUCTURE / POSSIBLE. + readers = field_readers(store, symbol.split("::")[-1]) + return {"subject": symbol, "status": "UNKNOWN", "reason": "not a function in the store", + "observed_crates": store.crates, + "field_readers": [{"function": f, "site": site, "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", "why": "field-name match, receiver type unresolved"} + for f, site in readers]} + src = store.src + callers, possible = defaultdict(set), defaultdict(set) + sites, fresh_of = defaultdict(list), {} + for caller, callee, kind, f, ln, fr in store.edges(): + (callers if kind == CALL else possible)[callee].add(caller) + sites[(caller, callee)].append(f"{f}:{ln if ln is not None else '?'}") + # An edge is current only if every row behind it sits in a FRESH file. + fresh_of[(caller, callee)] = fresh_of.get((caller, callee), True) and fr == "FRESH" + + def closure(seeds): + """Callers reachable from `seeds` through resolved calls: (all-fresh path, reached only + through stale evidence).""" + ok, stale_only, frontier = set(), {}, [(x, True) for x in seeds] + while frontier: + x, fresh = frontier.pop() + for c in callers.get(x, ()): + if c == symbol: + continue + f = fresh and fresh_of.get((c, x), True) + if f and c not in ok: + ok.add(c) + stale_only.pop(c, None) + frontier.append((c, True)) + elif not f and c not in ok and c not in stale_only: + stale_only[c] = sites[(c, x)] + frontier.append((c, False)) + return ok, stale_only + + confirmed, stale = closure([symbol]) + # Dispatch: callers of a trait method this symbol implements may reach it (the + # IMPLEMENTS -> MAY_DISPATCH join Codegraph::callers makes), and so may their callers. + traits = {r["object"] for r in store.rows if r["predicate"] == "IMPLEMENTS" and r["subject"] == symbol} + may_direct = set().union(*(possible.get(t, set()) for t in traits | {symbol})) - {symbol} + may_up, may_stale = closure(sorted(may_direct)) + possible_all = (may_direct | may_up) - confirmed + roots = sorted(c for c in confirmed if not callers.get(c)) + contracts = sorted({callee for caller, callee, kind, *_ in store.edges() if caller == symbol and kind == MAY}) + leaf = symbol.split("::")[-1] + ra_sites, ra_files, macros = ra + # Test call sites: source search by method name in test code, graded SOURCE_STRUCTURE/POSSIBLE + # unless a compiler row confirms them. A name match is not a call of this method. + tests = [] + for p in sorted(src.glob("crates/*/tests/**/*.rs")) + sorted(src.glob("crates/*/src/**/tests.rs")): + rel = str(p.relative_to(src)) + data = p.read_bytes() + for m in re.finditer(rb"\.%s\(" % re.escape(leaf.encode()), data): + ln = data[: m.start()].count(b"\n") + 1 + in_macro = any(a <= m.start() < b for a, b in macros.get(rel, ())) + tests.append({"site": f"{rel}:{ln}", "evidence_class": "SOURCE_STRUCTURE", + "qualifier": "POSSIBLE", "why": "method-name match, receiver unresolved", + "ra": ("CONFIRMED" if (rel, ln) in ra_sites else + "UNKNOWN: inside a macro region" if in_macro else + "UNKNOWN: file not indexed" if rel not in ra_files else "no call row"), + "run_status": "NOT_RUN"}) + span_lines = (store.line(d["file"], d["start"]), store.line(d["file"], d["end"])) + blob = git(src, "hash-object", d["file"]) + unknown = [] + if symbol in store.public: + unknown.append({"what": "callers in crates outside the store", "observed_crates": store.crates, + "why": "symbol is PUBLIC; only these crates' library targets were compiled"}) + unknown.append({"what": "test targets, examples, cfg(test) modules", "why": "store holds library targets only"}) + prov = {"tool": "charon c69e231 -> ruff_charon import (rows.tsv v2)", "toolchain": "nightly-2026-09-17", + "sysroot": "default (cargo-miri absent; std bodies opaque)"} + freshness = store.fresh.get(d["file"], "UNOBSERVED") + return { + "packet": "ReviewEvidencePacket (prototype, read-only; not a vendor API)", + "identity": {"repo_id": "AdaWorldAPI/lance-graph", "commit_sha": rev or git(src, "rev-parse", "HEAD"), + "cargo_lock_sha": "NOT_TRACKED (repository tracks no Cargo.lock)", + "crate_instance": d["subject"].split("::")[0] + " (lib target)", "features": "default", + "target_triple": "x86_64-unknown-linux-gnu", "rustc_version": "nightly-2026-09-17 (charon)", + "file_blob_sha": blob, "source_span": {"file": d["file"], "bytes": [int(d["start"]), int(d["end"])], + "lines": list(span_lines)}}, + "changed_source": {"subject": symbol, "base": rev or git(src, "rev-parse", "HEAD"), + "diff": diff_text if diff_text is not None else "NOT_SUPPLIED (prototype: change of the whole span)", + "stale": freshness != "FRESH", "freshness": freshness, + "dependency_evidence_stale": bool(stale or may_stale)}, + "affected_symbols": {"confirmed": sorted(confirmed), + "possible": sorted(possible_all), + "stale": [{"caller": c, "sites": st} for c, st in sorted({**may_stale, **stale}.items())], + "unknown": unknown}, + "witnessed_edges": [{"caller": c, "callee": symbol, "sites": sites[(c, symbol)], + "fresh": fresh_of.get((c, symbol), True)} for c in sorted(callers.get(symbol, ()))], + "possible_edges": [{"dispatch_target": t} for t in contracts], + "co_changed_only": "NOT_RUN (no history projection in this prototype)", + "unsupported_regions": sorted({t["site"].split(":")[0] for t in tests if not t["ra"].startswith("CONFIRMED")}), + "findings": [ + {"id": "dependents", "summary": f"{len(confirmed)} confirmed transitive in-store callers; external callers UNKNOWN", + "severity": None, "evidence_class": "COMPILER_DERIVED", "confidence": "as graded per item", + "provenance": prov, "lifecycle": "open", "run_status": "PARTIAL"}, + {"id": "tests", "summary": f"{len(tests)} candidate test call sites by name; none run", + "severity": None, "evidence_class": "SOURCE_STRUCTURE", "qualifier": "POSSIBLE", + "items": tests, "provenance": {"tool": "source search + rust-analyzer GRAPH=1 (ra_ap 0.0.358)"}, + "lifecycle": "open", "run_status": "NOT_RUN"}, + {"id": "contracts", "summary": "trait methods the symbol dispatches through (a change may interact with any impl)", + "severity": None, "evidence_class": "COMPILER_DERIVED", "qualifier": "POSSIBLE", "items": contracts, + "provenance": prov, "lifecycle": "open", "run_status": "COMPLETE"}, + {"id": "execution_paths", "summary": "entry points (in-store callers with no in-store caller)", + "severity": None, "evidence_class": "COMPILER_DERIVED", "items": roots, + "provenance": prov, "lifecycle": "open", "run_status": "PARTIAL"}, + ], + "r2il": {"method": "NOT_A_METHOD", "body_semantics": "UNKNOWN", + "why": "R2IL describes the effects of a registered DT64 MethodBinding (prepare binds them to " + "opcodes); a Rust function found by the compiler is not one, so its body has no R2IL reading"}, + "expected_behavior": "NOT_SUPPLIED (must come from intent/tests, independently of this packet)", + "candidate_behavior": "NOT_INFERRED", + "missing_necessary_evidence": ["test runs (TEST_OBSERVED needs a run that can fail, CR-H0 §5)", + "compiler artifacts of consumer crates and test targets", + "a resolved receiver for each name-matched test site"], + "permission_state": "NOT_DERIVED (never from confidence)", + } + + +# --------------------------------------------------------------------------------------------- +# Negative tests (D-CODEGRAPH-RECON-1 §7). Each builds a tiny synthetic store. + +def mk_store(td, files, rows, crate="lance_graph_x"): + td = Path(td) + (td / "src").mkdir(parents=True, exist_ok=True) + st = td / "store" + st.mkdir(exist_ok=True) + for path, body in files.items(): + p = td / "src" / path + p.parent.mkdir(parents=True, exist_ok=True) + p.write_bytes(body) + (st / f"{crate}.files.tsv").write_text("#version 1\n#schema path\tfnv64\n" + + "".join(f"{p}\t{fnv64(b)}\n" for p, b in files.items())) + (st / f"{crate}.rows.tsv").write_text("#version 2\n#schema predicate\tsubject\tobject\tgrade\tfile\tstart\tend\n" + + "".join("\t".join(map(str, r)) + "\n" for r in rows)) + return st, td / "src" + + +LIB = b"fn a() { b(); }\nfn b() {}\nfn c(x: &dyn T) { x.m(); }\n" +ROWS = [("DEFINES", "lance_graph_x::a", "lance_graph_x::a", "COMPILER", "lib.rs", 0, 15), + ("DEFINES", "lance_graph_x::b", "lance_graph_x::b", "COMPILER", "lib.rs", 16, 26), + ("DEFINES", "lance_graph_x::c", "lance_graph_x::c", "COMPILER", "lib.rs", 27, 55), + ("PUBLIC", "lance_graph_x::b", "lance_graph_x::b", "COMPILER", "lib.rs", 16, 26), + ("CALLS_RESOLVED", "lance_graph_x::a", "lance_graph_x::b", "COMPILER", "lib.rs", 9, 12), + ("MAY_DISPATCH", "lance_graph_x::c", "lance_graph_x::T::m via Clause", "COMPILER", "lib.rs", 46, 49)] + + +class Negatives(unittest.TestCase): + def setUp(self): + self.td = tempfile.TemporaryDirectory() + self.st, self.src = mk_store(self.td.name, {"lib.rs": LIB}, ROWS) + + def tearDown(self): + self.td.cleanup() + + def test_01_stale_facts_cannot_claim_current_code(self): + (self.src / "lib.rs").write_bytes(LIB + b"// edited\n") + out = recover(Store(self.st, self.src), ["lance_graph_x::a"]) + self.assertIn("-. STALE .->", out) + self.assertNotIn(" --> ", out) + + def test_02_renamed_symbol_keeps_its_own_identity(self): + rows = ROWS + [("DEFINES", "lance_graph_x::{F}::check", "lance_graph_x::{F}::check", "COMPILER", "lib.rs", 0, 1), + ("DEFINES", "lance_graph_x::{L}::check", "lance_graph_x::{L}::check", "COMPILER", "lib.rs", 2, 3), + ("CALLS_RESOLVED", "lance_graph_x::a", "lance_graph_x::{F}::check", "COMPILER", "lib.rs", 9, 12)] + st, src = mk_store(self.td.name + "/r", {"lib.rs": LIB}, rows) + p = packet(Store(st, src), (set(), set(), {}), "lance_graph_x::{L}::check") + self.assertEqual(p["affected_symbols"]["confirmed"], []) # F::check's caller is not L::check's + self.assertEqual(packet(Store(st, src), (set(), set(), {}), "lance_graph_x::{F}::check") + ["affected_symbols"]["confirmed"], ["lance_graph_x::a"]) + + def test_03_dynamic_call_is_never_absent_nor_confirmed(self): + out = recover(Store(self.st, self.src), ["lance_graph_x::c"]) + self.assertIn("-.->|possible|", out) + self.assertNotRegex(out, r"n\w+ --> n\w+") + + def test_04_macro_hidden_call_stays_unknown(self): + tests = self.src / "crates" / "lance_graph_x" / "tests" + tests.mkdir(parents=True) + body = b"fn t() { assert_eq!(z.b(), 1); }\n" + (tests / "t.rs").write_bytes(body) + rel = "crates/lance_graph_x/tests/t.rs" + ra = (set(), {rel}, {rel: [(9, 31)]}) + p = packet(Store(self.st, self.src), ra, "lance_graph_x::b") + items = [i for f in p["findings"] if f["id"] == "tests" for i in f["items"]] + self.assertEqual([i["ra"] for i in items], ["UNKNOWN: inside a macro region"]) + self.assertIn(rel, p["unsupported_regions"]) + + def test_05_missing_artifact_is_not_empty(self): + with self.assertRaises(ArtifactMissing): + Store(Path(self.td.name) / "nope", self.src) + (self.st / "lance_graph_x.files.tsv").unlink() + with self.assertRaises(ArtifactMissing): + Store(self.st, self.src) + + def test_06_guard_only_dependency_is_not_omitted(self): + # A field read only inside a guard has no call row; it must still be reported. + body = b"fn p(b: &B) -> u8 { if b.when.is_some() { return 1; } 0 }\nfn q(b: &B) { b.other(); }\n" + rows = [("DEFINES", "lance_graph_x::p", "lance_graph_x::p", "COMPILER", "lib.rs", 0, 57), + ("DEFINES", "lance_graph_x::q", "lance_graph_x::q", "COMPILER", "lib.rs", 58, 85)] + st, src = mk_store(self.td.name + "/g", {"lib.rs": body}, rows) + p = packet(Store(st, src), (set(), set(), {}), "lance_graph_x::{MethodBinding}::when") + self.assertEqual([r["function"] for r in p["field_readers"]], ["lance_graph_x::p"]) + + def test_06b_public_symbol_reports_external_callers_unknown(self): + # A public symbol whose only dependents are outside the store must report UNKNOWN, not none. + p = packet(Store(self.st, self.src), (set(), set(), {}), "lance_graph_x::b") + self.assertTrue(any("outside the store" in u["what"] for u in p["affected_symbols"]["unknown"])) + p = packet(Store(self.st, self.src), (set(), set(), {}), "lance_graph_x::a") + self.assertFalse(any("outside the store" in u["what"] for u in p["affected_symbols"]["unknown"])) + + def test_07_rbac_gap_is_never_rendered_as_an_edge(self): + corpus = [{"id": "R9", "subject": "ScopedDecision", "object": "bind_lanes", "status": "MISSING", + "recoverable": "NOT-RECOVERABLE", "verified_line": ""}] + out = reconcile(Store(self.st, self.src), ["lance_graph_x::a"], corpus) + line = [ln for ln in out.splitlines() if "R9" in ln] + self.assertTrue(line and all(":::gap" in ln and "-->" not in ln for ln in line)) + + def test_08_a_source_reference_is_not_a_call(self): + rows = ROWS + [("REFERENCES", "lance_graph_x::c", "lance_graph_x::b", "COMPILER", "lib.rs", 30, 31)] + st, src = mk_store(self.td.name + "/q", {"lib.rs": LIB}, rows) + p = packet(Store(st, src), (set(), set(), {}), "lance_graph_x::b") + self.assertEqual(p["affected_symbols"]["confirmed"], ["lance_graph_x::a"]) + self.assertEqual(p["affected_symbols"]["possible"], []) # a reference is not a dispatch either + out = recover(Store(st, src), ["lance_graph_x::c"]) + self.assertNotIn(node_id("lance_graph_x::b"), out) # c only references b: no edge, no node + + def test_08b_a_rust_function_is_not_an_r2il_method(self): + p = packet(Store(self.st, self.src), (set(), set(), {}), "lance_graph_x::b") + self.assertEqual((p["r2il"]["method"], p["r2il"]["body_semantics"]), ("NOT_A_METHOD", "UNKNOWN")) + + def test_11_stale_caller_evidence_is_not_confirmed(self): + # The caller's file changed after the store was built; the queried function's file did not. + files = {"a.rs": b"fn a() { b(); }\n", "b.rs": b"fn b() {}\n"} + rows = [("DEFINES", "lance_graph_x::a", "lance_graph_x::a", "COMPILER", "a.rs", 0, 15), + ("DEFINES", "lance_graph_x::b", "lance_graph_x::b", "COMPILER", "b.rs", 0, 9), + ("CALLS_RESOLVED", "lance_graph_x::a", "lance_graph_x::b", "COMPILER", "a.rs", 9, 12)] + st, src = mk_store(self.td.name + "/s", files, rows) + (src / "a.rs").write_bytes(b"fn a() {}\n") # b() removed + p = packet(Store(st, src), (set(), set(), {}), "lance_graph_x::b") + self.assertEqual(p["affected_symbols"]["confirmed"], []) + self.assertEqual([s["caller"] for s in p["affected_symbols"]["stale"]], ["lance_graph_x::a"]) + self.assertTrue(p["changed_source"]["dependency_evidence_stale"]) + + def test_12_dispatch_reaches_the_implementation(self): + rows = [("DEFINES", "lance_graph_x::b", "lance_graph_x::b", "COMPILER", "lib.rs", 16, 26), + ("DEFINES", "lance_graph_x::c", "lance_graph_x::c", "COMPILER", "lib.rs", 27, 55), + ("DEFINES", "lance_graph_x::a", "lance_graph_x::a", "COMPILER", "lib.rs", 0, 15), + ("IMPLEMENTS", "lance_graph_x::b", "lance_graph_x::T::m", "COMPILER", "lib.rs", 16, 26), + ("MAY_DISPATCH", "lance_graph_x::c", "lance_graph_x::T::m via Clause", "COMPILER", "lib.rs", 46, 49), + ("CALLS_RESOLVED", "lance_graph_x::a", "lance_graph_x::c", "COMPILER", "lib.rs", 9, 12)] + st, src = mk_store(self.td.name + "/d", {"lib.rs": LIB}, rows) + p = packet(Store(st, src), (set(), set(), {}), "lance_graph_x::b") + self.assertEqual(p["affected_symbols"]["possible"], ["lance_graph_x::a", "lance_graph_x::c"]) + self.assertEqual(p["affected_symbols"]["confirmed"], []) + + def test_13_missing_source_is_never_drawn_as_verified(self): + (self.src / "lib.rs").unlink() + out = recover(Store(self.st, self.src), ["lance_graph_x::a"]) + self.assertIn("-. MISSING_SOURCE .->", out) + self.assertNotIn(" --> ", out) + self.assertNotIn(":None", out) + + def test_09_lab_proposed_merged_stay_distinct(self): + corpus = [{"id": f"R{i}", "subject": "s", "object": "o", "status": s, "recoverable": "INTERPRETATION", + "verified_line": ""} for i, s in enumerate(["LAB", "PROPOSED", "IMPLEMENTED"])] + out = reconcile(Store(self.st, self.src), ["lance_graph_x::a"], corpus) + self.assertIn(":::lab", [ln for ln in out.splitlines() if "R0" in ln][0]) + self.assertIn(":::proposed", [ln for ln in out.splitlines() if "R1" in ln][0]) + self.assertFalse([ln for ln in out.splitlines() if '"R2' in ln or " R2[" in ln]) + + def test_10_reconstruction_cannot_pass_by_copying(self): + # recover never reads the corpus: identical output whatever the corpus says, and an edge that + # exists only in the corpus is never drawn. + s = Store(self.st, self.src) + out = recover(s, ["lance_graph_x::a", "lance_graph_x::c"]) + self.assertNotIn("ghost", out) + corpus = [{"id": "R1", "subject": "lance_graph_x::a", "object": "ghost", "status": "IMPLEMENTED", + "recoverable": "MECHANICAL-CALLGRAPH", "verified_line": "crates/x/src/lib.rs:1"}] + self.assertEqual(score(s, corpus)[0]["charon"], "UNOBSERVED") + self.assertEqual(out, recover(Store(self.st, self.src), ["lance_graph_x::c", "lance_graph_x::a"])) + + +def main(argv): + ap = argparse.ArgumentParser() + ap.add_argument("cmd", nargs="?") + ap.add_argument("--store"); ap.add_argument("--src"); ap.add_argument("--seeds") + ap.add_argument("--corpus"); ap.add_argument("--ra"); ap.add_argument("--symbol") + ap.add_argument("--diff"); ap.add_argument("--rev"); ap.add_argument("--self-test", action="store_true") + a = ap.parse_args(argv) + if a.self_test: + r = unittest.TextTestRunner(verbosity=2).run(unittest.defaultTestLoader.loadTestsFromTestCase(Negatives)) + return 0 if r.wasSuccessful() else 1 + try: + st = Store(a.store, a.src) + except ArtifactMissing as e: + print(e) + return 3 + seeds = [s for s in Path(a.seeds).read_text().splitlines() if s and not s.startswith("#")] if a.seeds else [] + if a.cmd == "recover": + sys.stdout.write(recover(st, seeds)) + elif a.cmd == "reconcile": + sys.stdout.write(reconcile(st, seeds, read_corpus(a.corpus))) + elif a.cmd == "score": + ra = ra_calls(a.ra, a.src) if a.ra else None + res = score(st, read_corpus(a.corpus), ra) + for r in res: + print("\t".join(str(r.get(k, "-")) for k in ("id", "site", "charon", "ra"))) + for arm in ("charon", "ra"): + vals = [r[arm] for r in res if arm in r] + if vals: + c = {k: vals.count(k) for k in ("HIT", "MISS", "UNOBSERVED", "NO_SITE")} + seen = c["HIT"] + c["MISS"] + print(f"#summary\t{arm}\t" + "\t".join(f"{k}={v}" for k, v in c.items()) + + f"\trecall_over_observed={c['HIT']}/{seen}") + elif a.cmd == "packet": + diff = Path(a.diff).read_text() if a.diff else None + json.dump(packet(st, ra_calls(a.ra, a.src), a.symbol, diff, a.rev), sys.stdout, indent=1) + print() + else: + ap.print_help() + return 2 + return 0 + + +if __name__ == "__main__": + sys.exit(main(sys.argv[1:])) diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/reconciled.mmd b/.claude/probes/2026-11-11-codegraph-recon-1/reconciled.mmd new file mode 100644 index 000000000..073372e23 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/reconciled.mmd @@ -0,0 +1,209 @@ +flowchart LR +%% machine-recovered from compiler facts only; no curated edge +classDef stale fill:#fdd,stroke:#c00 +classDef unknown fill:#eee,stroke:#888,stroke-dasharray:3 3 + n2324220d2d["impl_Clone_for_WideFieldMask::clone"] + nf0dd7eb4d4["WideFieldMask::count"] + n0fe9c0c703["WideFieldMask::has"] + n6effced490["ogar_codebook::classid_concept"] + n5880d6a6d2["impl_PartialEq_Truth_for_Truth::eq"] + n85f692868e["lance_graph_dt64::basis_at"] + n5c9d9be11c["lance_graph_dt64::basis_key"] + n30c0933001["lance_graph_dt64::check_basis"] + n9a358a34e7["impl_Clone_for_Frame::clone"] + ncea87a6cc8["impl_Clone_for_Guards::clone"] + n23b6de894b["FrameStore::check"] + nb3e6a1cf11["FrameStore::revisions"] + n139286eb5c["Guards::check"] + nc7b837b3cb["impl_Clone_for_MethodRef::clone"] + n7fb6db5dce["impl_PartialEq_ClassEntry_for_ClassEntry::eq"] + n41d921fb1f["impl_PartialEq_GuardWitness_for_GuardWitness::eq"] + nfb81872bac["LaneSource::borrow"] + nc321749ee8["LaneSource::lane_of"] + neffab0ab1b["lane::admit_lane"] + n8e44b69cf6["lane::current_route"] + nf82f64d778["impl_Iterator_for_BoundLanes::next"] + nf14d98b062["impl_PartialEq_LaneAddr_for_LaneAddr::eq"] + n834e7f0057["lane::source_owns"] + n2d47678468["BindStore::bind_lanes"] + n7c402f07e0["LaneBinding::addr"] + nd3c67ef2b2["LaneBinding::borrow_all"] + n6ee36d71b5["LaneBinding::check"] + n11cbb761a0["LaneBinding::lane"] + na638ff5529["lance_graph_dt64::validate"] + nc9fd69b271["BasisDigest::of"] + nca939019e2["BindStore::admit"] + n77e7ca84bd["BindStore::arity"] + ne8f5ae53b5["BindStore::bound_basis"] + n3b3358f47f["BindStore::check_issuer"] + nd976eba76b["BindStore::insert"] + n0bf65fd17d["BindStore::method_ref"] + n56217912b2["BindStore::register"] + n628dec15fb["BindStore::resolve"] + n728b4e948f["BindStore::resolve_counted"] + nff6be43a65["BindStore::routed_at"] + necac4f0cca["Guard::witness"] + nb80f13b646["exec::execute_compiled"] + nb1030f7f31["exec::scratch_words_for"] + nae37e07664["exec::tile_words_for"] + n6cce1c48bd["Scratch<'a>::over"] + nb940628aab["impl_Clone_for_Program::clone"] + n603aa31300["CompiledProgram::compiled"] + nf52b6be669["CompiledProgram::new"] + n448472ea7d["binding::call_step"] + nbb79e9a73c["binding::check_compare"] + nb950916031["binding::check_route"] + nab16acdce2["impl_Clone_for_Prepared::clone"] + na70926968a["binding::lane"] + n6f2b33fcea["binding::plan_id"] + n9f0aa095b5["binding::prepare"] + n394d8cf7a9["binding::run"] + n5e4579653e["binding::run_steps"] + nd18e8d838f["binding_native::prepare_native"] + n3a26fe8187["binding_native::run_native"] + nb0f12d5420["binding_native::shape_of"] + n07a94d728c["FoldDialect<'p>::discard_pending"] + n7422030821["FoldDialect<'p>::last_program"] + n3e900d22cd["FoldDialect<'p>::new"] + n8fa0cd24a9["FoldDialect<'p>::programs_run"] + nf82f64d778 -.->|possible| nfb81872bac %% crates/lance-graph-dt64/src/lane.rs:408 + n2d47678468 --> n2324220d2d %% crates/lance-graph-dt64/src/lane.rs:212 + n2d47678468 --> nf0dd7eb4d4 %% crates/lance-graph-dt64/src/lane.rs:191 + n2d47678468 --> n0fe9c0c703 %% crates/lance-graph-dt64/src/lane.rs:193 + n2d47678468 --> n9a358a34e7 %% crates/lance-graph-dt64/src/lane.rs:209 + n2d47678468 --> n23b6de894b %% crates/lance-graph-dt64/src/lane.rs:179 + n2d47678468 -.->|possible| nc321749ee8 %% crates/lance-graph-dt64/src/lane.rs:199 + n2d47678468 --> neffab0ab1b %% crates/lance-graph-dt64/src/lane.rs:202 + n2d47678468 --> n8e44b69cf6 %% crates/lance-graph-dt64/src/lane.rs:186 + n2d47678468 --> n834e7f0057 %% crates/lance-graph-dt64/src/lane.rs:178 + n2d47678468 --> ne8f5ae53b5 %% crates/lance-graph-dt64/src/lane.rs:188 + n2d47678468 --> n628dec15fb %% crates/lance-graph-dt64/src/lane.rs:187 + n2d47678468 --> nff6be43a65 %% crates/lance-graph-dt64/src/lane.rs:180 + nd3c67ef2b2 --> n6ee36d71b5 %% crates/lance-graph-dt64/src/lane.rs:386 + n6ee36d71b5 --> n23b6de894b %% crates/lance-graph-dt64/src/lane.rs:315 + n6ee36d71b5 -.->|possible| nc321749ee8 %% crates/lance-graph-dt64/src/lane.rs:336 + n6ee36d71b5 --> neffab0ab1b %% crates/lance-graph-dt64/src/lane.rs:346 + n6ee36d71b5 --> n8e44b69cf6 %% crates/lance-graph-dt64/src/lane.rs:316 + n6ee36d71b5 --> nf14d98b062 %% crates/lance-graph-dt64/src/lane.rs:337 + n6ee36d71b5 --> n834e7f0057 %% crates/lance-graph-dt64/src/lane.rs:314 + n6ee36d71b5 --> n728b4e948f %% crates/lance-graph-dt64/src/lane.rs:324 + n11cbb761a0 -.->|possible| nfb81872bac %% crates/lance-graph-dt64/src/lane.rs:362 + n11cbb761a0 --> n7c402f07e0 %% crates/lance-graph-dt64/src/lane.rs:361 + n11cbb761a0 --> n6ee36d71b5 %% crates/lance-graph-dt64/src/lane.rs:360 + nca939019e2 --> n41d921fb1f %% crates/lance-graph-dt64/src/lib.rs:1204 + nca939019e2 --> n3b3358f47f %% crates/lance-graph-dt64/src/lib.rs:1210 + nca939019e2 --> necac4f0cca %% crates/lance-graph-dt64/src/lib.rs:1204 + nd976eba76b --> n85f692868e %% crates/lance-graph-dt64/src/lib.rs:871 + nd976eba76b --> n5c9d9be11c %% crates/lance-graph-dt64/src/lib.rs:880 + nd976eba76b --> n7fb6db5dce %% crates/lance-graph-dt64/src/lib.rs:905 + nd976eba76b --> na638ff5529 %% crates/lance-graph-dt64/src/lib.rs:851 + nd976eba76b --> nc9fd69b271 %% crates/lance-graph-dt64/src/lib.rs:879 + nd976eba76b --> n77e7ca84bd %% crates/lance-graph-dt64/src/lib.rs:855 + n56217912b2 --> nd976eba76b %% crates/lance-graph-dt64/src/lib.rs:821 + n628dec15fb --> n30c0933001 %% crates/lance-graph-dt64/src/lib.rs:1083 + n9f0aa095b5 --> n6effced490 %% crates/lance-graph-r2il/src/binding.rs:341 + n9f0aa095b5 --> n5880d6a6d2 %% crates/lance-graph-r2il/src/binding.rs:338 + n9f0aa095b5 --> ncea87a6cc8 %% crates/lance-graph-r2il/src/binding.rs:361 + n9f0aa095b5 --> n139286eb5c %% crates/lance-graph-r2il/src/binding.rs:329 + n9f0aa095b5 --> nc7b837b3cb %% crates/lance-graph-r2il/src/binding.rs:358 + n9f0aa095b5 --> nca939019e2 %% crates/lance-graph-r2il/src/binding.rs:334 + n9f0aa095b5 --> n628dec15fb %% crates/lance-graph-r2il/src/binding.rs:331 + n9f0aa095b5 --> nb950916031 %% crates/lance-graph-r2il/src/binding.rs:330 + n9f0aa095b5 --> n6f2b33fcea %% crates/lance-graph-r2il/src/binding.rs:356 + n394d8cf7a9 --> n139286eb5c %% crates/lance-graph-r2il/src/binding.rs:389 + n394d8cf7a9 --> n3b3358f47f %% crates/lance-graph-r2il/src/binding.rs:386 + n394d8cf7a9 --> nb950916031 %% crates/lance-graph-r2il/src/binding.rs:392 + n394d8cf7a9 --> n5e4579653e %% crates/lance-graph-r2il/src/binding.rs:397 + n394d8cf7a9 --> n07a94d728c %% crates/lance-graph-r2il/src/binding.rs:396 + n394d8cf7a9 --> n07a94d728c %% crates/lance-graph-r2il/src/binding.rs:398 + nd18e8d838f --> n139286eb5c %% crates/lance-graph-r2il/src/binding_native.rs:214 + nd18e8d838f --> n3b3358f47f %% crates/lance-graph-r2il/src/binding_native.rs:211 + nd18e8d838f --> nb1030f7f31 %% crates/lance-graph-r2il/src/binding_native.rs:323 + nd18e8d838f --> nae37e07664 %% crates/lance-graph-r2il/src/binding_native.rs:320 + nd18e8d838f --> nb940628aab %% crates/lance-graph-r2il/src/binding_native.rs:263 + nd18e8d838f --> nf52b6be669 %% crates/lance-graph-r2il/src/binding_native.rs:277 + nd18e8d838f --> n448472ea7d %% crates/lance-graph-r2il/src/binding_native.rs:250 + nd18e8d838f --> nbb79e9a73c %% crates/lance-graph-r2il/src/binding_native.rs:247 + nd18e8d838f --> nb950916031 %% crates/lance-graph-r2il/src/binding_native.rs:217 + nd18e8d838f --> nab16acdce2 %% crates/lance-graph-r2il/src/binding_native.rs:331 + nd18e8d838f --> na70926968a %% crates/lance-graph-r2il/src/binding_native.rs:229 + nd18e8d838f --> nb0f12d5420 %% crates/lance-graph-r2il/src/binding_native.rs:333 + nd18e8d838f --> n7422030821 %% crates/lance-graph-r2il/src/binding_native.rs:263 + nd18e8d838f --> n3e900d22cd %% crates/lance-graph-r2il/src/binding_native.rs:218 + nd18e8d838f --> n8fa0cd24a9 %% crates/lance-graph-r2il/src/binding_native.rs:249 + nd18e8d838f --> n8fa0cd24a9 %% crates/lance-graph-r2il/src/binding_native.rs:259 + n3a26fe8187 --> nb3e6a1cf11 %% crates/lance-graph-r2il/src/binding_native.rs:412 + n3a26fe8187 --> n139286eb5c %% crates/lance-graph-r2il/src/binding_native.rs:364 + n3a26fe8187 --> n3b3358f47f %% crates/lance-graph-r2il/src/binding_native.rs:361 + n3a26fe8187 --> nb80f13b646 %% crates/lance-graph-r2il/src/binding_native.rs:385 + n3a26fe8187 --> n6cce1c48bd %% crates/lance-graph-r2il/src/binding_native.rs:384 + n3a26fe8187 --> n603aa31300 %% crates/lance-graph-r2il/src/binding_native.rs:386 + n3a26fe8187 --> nb950916031 %% crates/lance-graph-r2il/src/binding_native.rs:367 + n3a26fe8187 --> nb0f12d5420 %% crates/lance-graph-r2il/src/binding_native.rs:371 + nf82f64d778_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nf82f64d778 + n2d47678468_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n2d47678468 + nd3c67ef2b2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nd3c67ef2b2 + n6ee36d71b5_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n6ee36d71b5 + n11cbb761a0_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n11cbb761a0 + nca939019e2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nca939019e2 + n3b3358f47f_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n3b3358f47f + n0bf65fd17d_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n0bf65fd17d + n56217912b2_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n56217912b2 + n628dec15fb_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n628dec15fb + n9f0aa095b5_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n9f0aa095b5 + n394d8cf7a9_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n394d8cf7a9 + nd18e8d838f_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> nd18e8d838f + n3a26fe8187_ext["callers outside lance_graph_contract, lance_graph_dt64, lance_graph_quack, lance_graph_r2il: UNKNOWN"]:::unknown -.-> n3a26fe8187 +%% --- human interpretation (corpus rows; not compiler facts) --- +classDef gap fill:#fff3cd,stroke:#b58900,stroke-dasharray:5 5 +classDef lab fill:#e8f4ff,stroke:#268bd2 +classDef proposed fill:#f3e8ff,stroke:#6c71c4,stroke-dasharray:2 2 +classDef contradicted fill:#fdd,stroke:#c00 + R005_c["R005 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R243["R243: rel_from_set / &SetExpr (OPEN-PR)"]:::proposed + R244["R244: rel_from_set / Rel (OPEN-PR)"]:::proposed + R248["R248: PreparedMethod / program: Program kept per binding (OPEN-PR)"]:::proposed + R250["R250: PreparedMethod / prepare (cold) and run (hot) (OPEN-PR)"]:::proposed + R252["R252: Program / held by PreparedMethod (dashed edge PROG -.- LAB) (OPEN-PR)"]:::proposed + R256_c["R256 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R261["R261: ExecPermit issuer / not decided"]:::gap + R262["R262: one executor for WHEN and DO / not built"]:::gap + R263["R263: ExecPermit issuer / edge to run (dashed PERMIT -.- RUN)"]:::gap + R264["R264: one executor / edge to execute_into (dashed ONE -.- EXEC)"]:::gap + R265["R265: one executor / edge to run_native (dashed ONE -.- RUN)"]:::gap + R266_c["R266 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R268_c["R268 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R272["R272: code that holds and re-runs the program / is the G6 lab PreparedMethod on the open P (OPEN-PR)"]:::proposed + R276["R276: WHEN (lab) and DO (r2il) / nothing yet runs both for one method"]:::gap + R278["R278: G6 lab / lives in crates/foundry-parity-lab, PR #1996 (open) (OPEN-PR)"]:::proposed + R282["R282: borrow_all / returns borrowed planes, no copy (LAB)"]:::lab + R291["R291: guard / is a SetExpr over field positions; mask fields Sym(field); value fields comp (LAB)"]:::lab + R292["R292: PreparedMethod / keeps the one program relalg returns (LAB)"]:::lab + R294["R294: reader scope in lab / is a stand-in written into the program, not the RBAC decision (LAB)"]:::lab + R296["R296: arm C (#1995) / is merged and separate from the method path (LAB)"]:::lab + R322["R322: one executor for WHEN and DO / not built; plan lists it as the missing contract for "]:::gap + R323["R323: ExecPermit issuer / undecided"]:::gap + R324["R324: Operation::Act decision (lance-graph-rbac) / is a natural candidate issuer of ExecPe (PROPOSED)"]:::proposed + R325["R325: PreparedMethod and rel_from_set / are on PR #1996 and not merged (OPEN-PR)"]:::proposed + R325_c["R325 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R326["R326: authorization decision / nothing yet applies it to a DT64 binding"]:::gap + R417_c["R417 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R422_c["R422 CONTRADICTED by source; not drawn as an edge"]:::contradicted + R426["R426: per-row scope lane (resident plane) / not built"]:::gap + R427["R427: visible_fields() limiting bound fields / not built"]:::gap + R428["R428: ExecPermit issuer / undecided"]:::gap + R429["R429: one record per answer (identity + receipt + witness) / not built"]:::gap + R430["R430: ScopedDecision / per-row scope lane (G2A)"]:::gap + R431["R431: Quack Binder::live / per-row scope lane (G2A)"]:::gap + R432["R432: per-row scope lane / BindStore::bind_lanes (G2A- BL)"]:::gap + R433["R433: ScopedDecision / visible_fields limits bound fields (G2B)"]:::gap + R434["R434: Resolved::mask_where / visible_fields limits bound fields (G2B)"]:::gap + R435["R435: visible_fields limit / BindStore::bind_lanes (G2B- BL)"]:::gap + R436["R436: Operation::Act decision / ExecPermit issuer ('candidate only')"]:::gap + R437["R437: ExecPermit issuer / ExecPermit (ISS- PERM)"]:::gap + R438["R438: auth_classid/acting_party / one record per answer (AUDIT- JOIN)"]:::gap + R439["R439: DT64, r2il, xlog, Quack, mask-risc code / use lance-graph-rbac"]:::gap + R440["R440: lab reader scope / is a stand-in: one reader denied one store id, written into the p (LAB)"]:::lab + R441["R441: Quack Binder::live / is the existing seam where a scope plane could enter (PROPOSED)"]:::proposed + R442["R442: ExecPermit issuer / r2il source says it is not decided; Operation::Act is a candidat"]:::gap + R444["R444: receipts, commit witnesses and identity / nothing joins them into one record per ans"]:::gap diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/score.tsv b/.claude/probes/2026-11-11-codegraph-recon-1/score.tsv new file mode 100644 index 000000000..e91d3baff --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/score.tsv @@ -0,0 +1,121 @@ +R051 crates/lance-graph-dt64/src/dr.rs:286 HIT HIT +R052 crates/lance-graph-dt64/src/dr.rs:976 HIT HIT +R053 crates/lance-graph-dt64/src/dr.rs:271 MISS HIT +R054 crates/lance-graph-dt64/src/dr.rs:303 MISS HIT +R055 crates/lance-graph-dt64/src/dr.rs:588 MISS HIT +R056 crates/lance-graph-dt64/src/dr.rs:595 MISS HIT +R057 crates/lance-graph-dt64/src/dr.rs:627 MISS HIT +R101 crates/lance-graph-dt64/src/dr.rs:462 HIT HIT +R105 crates/lance-graph-dt64/src/dr.rs:544 HIT HIT +R108 crates/lance-graph-dt64/src/dr.rs:469 HIT HIT +R160 crates/lance-graph-dt64/src/lib.rs:1283 HIT HIT +R165 crates/lance-graph-dt64/src/lane.rs:336 HIT HIT +R167 crates/lance-graph-dt64/src/lib.rs:1147 MISS HIT +R168 crates/lance-graph-dt64/src/lib.rs:1193 MISS HIT +R169 crates/lance-graph-dt64/src/lib.rs:1202 HIT HIT +R170 crates/lance-graph-dt64/src/lib.rs:1203 HIT HIT +R171 crates/lance-graph-dt64/src/lib.rs:1205 HIT HIT +R172 crates/lance-graph-dt64/src/lib.rs:1208 HIT HIT +R173 crates/lance-graph-dt64/src/lib.rs:1210 HIT HIT +R175 crates/lance-graph-dt64/src/lib.rs:709 HIT HIT +R184 crates/lance-graph-dt64/src/lane.rs:171 MISS MISS +R185 crates/lance-graph-dt64/src/lane.rs:178 HIT HIT +R186 crates/lance-graph-dt64/src/lane.rs:178 HIT HIT +R187 crates/lance-graph-dt64/src/lane.rs:224 MISS HIT +R188 crates/lance-graph-dt64/src/lane.rs:179 HIT HIT +R189 crates/lance-graph-dt64/src/lane.rs:179 HIT HIT +R190 crates/lance-graph-dt64/src/lane.rs:181 MISS HIT +R191 crates/lance-graph-dt64/src/lane.rs:182 MISS HIT +R192 crates/lance-graph-dt64/src/lane.rs:181 MISS HIT +R193 crates/lance-graph-dt64/src/lane.rs:186 HIT HIT +R194 crates/lance-graph-dt64/src/lane.rs:234 MISS HIT +R195 crates/lance-graph-dt64/src/lane.rs:187 HIT HIT +R196 crates/lance-graph-dt64/src/lib.rs:1082 HIT HIT +R197 crates/lance-graph-dt64/src/lib.rs:1228 MISS HIT +R198 crates/lance-graph-dt64/src/lib.rs:1238 MISS HIT +R199 crates/lance-graph-dt64/src/lane.rs:192 HIT HIT +R200 crates/lance-graph-dt64/src/lane.rs:196 HIT HIT +R201 crates/lance-graph-dt64/src/lane.rs:199 HIT HIT +R202 crates/lance-graph-dt64/src/lane.rs:201 HIT HIT +R203 crates/lance-graph-dt64/src/lane.rs:202 HIT HIT +R204 crates/lance-graph-dt64/src/lane.rs:202 HIT HIT +R206 crates/lance-graph-dt64/src/lane.rs:379 MISS MISS +R207 crates/lance-graph-dt64/src/lane.rs:386 HIT HIT +R208 crates/lance-graph-dt64/src/lane.rs:314 HIT HIT +R209 crates/lance-graph-dt64/src/lane.rs:326 HIT HIT +R210 crates/lance-graph-dt64/src/lane.rs:338 MISS HIT +R212 crates/lance-graph-dt64/src/lane.rs:409 MISS HIT +R213 crates/lance-graph-dt64/src/lane.rs:411 MISS HIT +R215 crates/lance-graph-dt64/src/lane.rs:360 HIT HIT +R216 crates/lance-graph-dt64/src/lane.rs:361 HIT HIT +R227 crates/lance-graph-dt64/src/lib.rs:821 HIT HIT +R228 crates/lance-graph-dt64/src/lib.rs:1347 MISS HIT +R229 crates/lance-graph-dt64/src/lib.rs:871 HIT HIT +R232 crates/lance-graph-dt64/src/lib.rs:1181 HIT HIT +R233 crates/lance-graph-dt64/src/lib.rs:1190 HIT HIT +R234 crates/lance-graph-dt64/src/lib.rs:1193 MISS HIT +R235 crates/lance-graph-dt64/src/lib.rs:1202 HIT HIT +R236 crates/lance-graph-dt64/src/lib.rs:1203 HIT HIT +R237 crates/lance-graph-dt64/src/lib.rs:1205 HIT HIT +R238 crates/lance-graph-dt64/src/lib.rs:1208 HIT HIT +R239 crates/lance-graph-dt64/src/lib.rs:1210 HIT HIT +R242 crates/foundry-parity-lab/src/method.rs:217 UNOBSERVED UNOBSERVED +R245 crates/foundry-parity-lab/src/method.rs:264 UNOBSERVED UNOBSERVED +R249 crates/foundry-parity-lab/src/method.rs:302 UNOBSERVED UNOBSERVED +R251 crates/foundry-parity-lab/src/method.rs:31 UNOBSERVED UNOBSERVED +R253 crates/lance-graph-r2il/src/binding.rs:334 HIT HIT +R255 crates/lance-graph-r2il/src/binding_native.rs:368 HIT HIT +R257 crates/lance-graph-r2il/src/binding.rs:335 HIT HIT +R259 crates/lance-graph-xlog/src/lib.rs:391 UNOBSERVED HIT +R260 crates/lance-graph-xlog/src/lib.rs:399 UNOBSERVED HIT +R270 crates/lance-graph-dt64/src/lib.rs:1184 HIT HIT +R271 crates/foundry-parity-lab/src/method.rs:264 UNOBSERVED UNOBSERVED +R274 crates/lance-graph-r2il/src/binding.rs:389 HIT HIT +R275 crates/lance-graph-r2il/src/binding.rs:335 HIT HIT +R279 crates/foundry-parity-lab/src/method.rs:217 UNOBSERVED UNOBSERVED +R281 crates/foundry-parity-lab/src/method.rs:219 UNOBSERVED UNOBSERVED +R283 crates/foundry-parity-lab/src/method.rs:251 UNOBSERVED UNOBSERVED +R284 crates/foundry-parity-lab/src/method.rs:252 UNOBSERVED UNOBSERVED +R285 crates/foundry-parity-lab/src/method.rs:264 UNOBSERVED UNOBSERVED +R286 crates/lance-graph-relalg/src/lower.rs:75 UNOBSERVED HIT +R288 crates/foundry-parity-lab/src/method.rs:276 UNOBSERVED UNOBSERVED +R289 crates/foundry-parity-lab/src/method.rs:302 UNOBSERVED UNOBSERVED +R290 crates/foundry-parity-lab/src/method.rs:311 UNOBSERVED UNOBSERVED +R293 crates/foundry-parity-lab/src/method.rs:118 UNOBSERVED UNOBSERVED +R295 crates/foundry-parity-lab/src/arm_c.rs:82 UNOBSERVED UNOBSERVED +R298 crates/lance-graph-r2il/src/binding.rs:329 HIT HIT +R299 crates/lance-graph-r2il/src/binding.rs:330 HIT HIT +R300 crates/lance-graph-r2il/src/binding.rs:334 HIT HIT +R301 crates/lance-graph-r2il/src/binding.rs:335 HIT HIT +R302 crates/lance-graph-r2il/src/binding.rs:338 HIT HIT +R303 crates/lance-graph-r2il/src/binding.rs:350 HIT HIT +R305 crates/lance-graph-r2il/src/binding_native.rs:196 MISS MISS +R306 crates/lance-graph-r2il/src/binding_native.rs:244 HIT HIT +R309 crates/lance-graph-r2il/src/binding.rs:386 HIT HIT +R310 crates/lance-graph-r2il/src/binding.rs:389 HIT HIT +R311 crates/lance-graph-r2il/src/binding.rs:393 HIT HIT +R312 crates/lance-graph-r2il/src/binding.rs:397 HIT HIT +R314 crates/lance-graph-r2il/src/binding.rs:386 HIT HIT +R318 crates/lance-graph-r2il/src/binding_native.rs:371 HIT HIT +R319 crates/lance-graph-xlog/src/lib.rs:391 UNOBSERVED HIT +R320 crates/lance-graph-xlog/src/lib.rs:399 UNOBSERVED HIT +R321 crates/lance-graph-xlog/src/lib.rs:345 UNOBSERVED HIT +R329 OGAR/crates/ogar-auth/src/federation.rs:263 UNOBSERVED UNOBSERVED +R336 OGAR/crates/ogar-rbac/src/lib.rs:161 UNOBSERVED UNOBSERVED +R339 OGAR/crates/ogar-rbac/src/lib.rs:333 UNOBSERVED UNOBSERVED +R341 OGAR/crates/ogar-auth/src/federation.rs:246 UNOBSERVED UNOBSERVED +R346 OGAR/crates/ogar-rbac/src/lib.rs:308 UNOBSERVED UNOBSERVED +R352 crates/lance-graph-rbac/src/authorize.rs:66 UNOBSERVED MISS +R353 crates/lance-graph-rbac/src/authorize.rs:216 UNOBSERVED HIT +R355 crates/lance-graph-rbac/src/authorize.rs:225 UNOBSERVED MISS +R356 crates/lance-graph-rbac/src/authorize.rs:236 UNOBSERVED HIT +R357 crates/lance-graph-rbac/src/authorize.rs:243 UNOBSERVED HIT +R359 crates/lance-graph-rbac/src/authorize.rs:318 UNOBSERVED HIT +R372 crates/lance-graph-contract/src/rbac.rs:548 HIT HIT +R410 crates/lance-graph-contract/src/rbac.rs:170 HIT HIT +R411 crates/lance-graph-contract/src/rbac.rs:185 MISS HIT +R412 crates/lance-graph-contract/src/rbac.rs:178 MISS MISS +R415 crates/lance-graph-dt64/src/lib.rs:715 MISS MISS +R422 crates/lance-graph-contract/src/selection.rs:335 MISS MISS +#summary charon HIT=61 MISS=26 UNOBSERVED=32 NO_SITE=0 recall_over_observed=61/87 +#summary ra HIT=91 MISS=8 UNOBSERVED=20 NO_SITE=0 recall_over_observed=91/99 diff --git a/.claude/probes/2026-11-11-codegraph-recon-1/seeds.txt b/.claude/probes/2026-11-11-codegraph-recon-1/seeds.txt new file mode 100644 index 000000000..e0307b375 --- /dev/null +++ b/.claude/probes/2026-11-11-codegraph-recon-1/seeds.txt @@ -0,0 +1,16 @@ +# Seed NODES for the machine-recovered diagram (human-chosen; no edges). Symbols as the store names them. +lance_graph_dt64::{BindStore}::register +lance_graph_dt64::{BindStore}::insert +lance_graph_dt64::{BindStore}::resolve +lance_graph_dt64::{BindStore}::method_ref +lance_graph_dt64::{BindStore}::admit +lance_graph_dt64::{BindStore}::check_issuer +lance_graph_dt64::lane::{BindStore}::bind_lanes +lance_graph_dt64::lane::{LaneBinding}::check +lance_graph_dt64::lane::{LaneBinding}::lane +lance_graph_dt64::lane::{LaneBinding}::borrow_all +lance_graph_dt64::lane::impl_Iterator_for_BoundLanes::next +lance_graph_r2il::binding::prepare +lance_graph_r2il::binding::run +lance_graph_r2il::binding_native::prepare_native +lance_graph_r2il::binding_native::run_native diff --git a/.codegraph/coverage.tsv b/.codegraph/coverage.tsv index c7b8a1694..c2e4302d6 100644 --- a/.codegraph/coverage.tsv +++ b/.codegraph/coverage.tsv @@ -36,7 +36,7 @@ lance-graph-benches 0 10 0 macro-generated items invisible;fn-local use not scan lance-graph-callcenter 35 6 3 macro-generated items invisible;fn-local use not scanned lance-graph-catalog 9 1 0 macro-generated items invisible;fn-local use not scanned lance-graph-codec-research 10 0 0 macro-generated items invisible;fn-local use not scanned -lance-graph-codegraph 8 10 0 macro-generated items invisible;fn-local use not scanned +lance-graph-codegraph 8 11 0 macro-generated items invisible;fn-local use not scanned lance-graph-cognitive 60 0 0 macro-generated items invisible;fn-local use not scanned lance-graph-consumer-conformance 2 0 0 macro-generated items invisible;fn-local use not scanned lance-graph-contract 175 35 2 macro-generated items invisible;fn-local use not scanned diff --git a/crates/lance-graph-codegraph/examples/cg_query.rs b/crates/lance-graph-codegraph/examples/cg_query.rs new file mode 100644 index 000000000..4b4975ef8 --- /dev/null +++ b/crates/lance-graph-codegraph/examples/cg_query.rs @@ -0,0 +1,207 @@ +//! Read-only command-line access to the four Codegraph queries, for agents and +//! people who would otherwise have to write Rust to ask one question. +//! +//! ```text +//! cargo run --release --example cg_query -- symbols [SUBSTRING] +//! cargo run --release --example cg_query -- callers|callees|impact|refs SYMBOL +//! ``` +//! +//! Output is tab-separated, one fact per line. Every result line carries its +//! grade (`CONFIRMED`, `POSSIBLE`, `UNKNOWN`); a refusal is printed verbatim +//! with `REFUSED` and exit code 3, never as an empty answer. Callers and impact of +//! a `PUBLIC` symbol always add an `UNKNOWN external-callers-unobserved` line, and +//! every graded answer lists the files the store observed. `src_root` is the +//! directory the store's file paths are relative to; it is used only to turn a +//! byte offset into a 1-based line. + +use std::path::{Path, PathBuf}; +use std::process::ExitCode; + +use lance_graph_codegraph::Codegraph; + +fn line_of(src_root: &Path, file: &str, offset: u32) -> String { + match std::fs::read(src_root.join(file)) { + Ok(bytes) => { + let end = (offset as usize).min(bytes.len()); + (bytes[..end].iter().filter(|&&b| b == b'\n').count() + 1).to_string() + } + Err(_) => "?".to_string(), + } +} + +fn names(g: &Codegraph, mask: &[u64]) -> Vec { + let mut out = Vec::new(); + for (w, &word) in mask.iter().enumerate() { + let mut bits = word; + while bits != 0 { + let b = bits.trailing_zeros(); + bits &= bits - 1; + if let Some(s) = g.symbol((w as u32) * 64 + b) { + out.push(s.to_string()); + } + } + } + out.sort(); + out +} + +fn bit(mask: &[u64], p: u32) -> bool { + mask.get((p / 64) as usize) + .is_some_and(|w| w >> (p % 64) & 1 == 1) +} + +/// Files that contributed at least one row. Anything else (tests, examples, +/// other crates) was not observed by this store. +fn observed_files(g: &Codegraph) -> Vec { + let mut files: Vec = (0..g.rows()) + .filter_map(|r| g.site(r).map(|(f, _, _)| f.to_string())) + .collect(); + files.sort(); + files.dedup(); + files +} + +fn main() -> ExitCode { + let args: Vec = std::env::args().skip(1).collect(); + if args.len() < 3 { + eprintln!("usage: cg_query symbols [SUBSTR] | callers|callees|impact|refs SYMBOL"); + return ExitCode::from(2); + } + let (store, src, cmd) = ( + PathBuf::from(&args[0]), + PathBuf::from(&args[1]), + args[2].as_str(), + ); + let mut g = match Codegraph::open(&store) { + Ok(g) => g, + Err(e) => { + println!("REFUSED\topen\t{e:?}"); + return ExitCode::from(3); + } + }; + if cmd == "symbols" { + let sub = args.get(3).map(String::as_str).unwrap_or(""); + let mut p = 0u32; + while let Some(s) = g.symbol(p) { + if s.contains(sub) { + println!("symbol\t{p}\t{s}"); + } + p += 1; + } + return ExitCode::SUCCESS; + } + if cmd == "sweep" { + // Runs `impact` and `callers` for every position in one process and counts + // answers, refusals (by kind) and empty sets. Measures where the cube's + // limits bind on this store; prints nothing per symbol. + let started = std::time::Instant::now(); + let (mut ok, mut empty) = (0u32, 0u32); + let mut refused: std::collections::BTreeMap = Default::default(); + let mut p = 0u32; + while g.symbol(p).is_some() { + for which in ["impact", "callers"] { + let r = match which { + "impact" => g.impact(p).map(|i| { + i.confirmed + .iter() + .chain(&i.possible) + .chain(&i.unknown) + .any(|w| *w != 0) + }), + _ => g.callers(p).map(|c| c.sites > 0), + }; + match r { + Ok(true) => ok += 1, + Ok(false) => empty += 1, + Err(e) => { + let kind = format!("{e:?}"); + let kind = kind + .split(['(', '{', ' ']) + .take(2) + .collect::>() + .join(" "); + *refused.entry(format!("{which} {kind}")).or_default() += 1; + } + } + } + p += 1; + } + println!( + "sweep\tpositions={p}\tanswered={ok}\tempty={empty}\tms={}", + started.elapsed().as_millis() + ); + for (k, n) in refused { + println!("sweep\tREFUSED\t{k}\t{n}"); + } + return ExitCode::SUCCESS; + } + let Some(sym) = args.get(3) else { + eprintln!("{cmd} needs a SYMBOL"); + return ExitCode::from(2); + }; + let Some(pos) = g.pos(sym) else { + println!("UNKNOWN\tsymbol-not-in-store\t{sym}"); + return ExitCode::from(4); + }; + let graded = match cmd { + "callers" => g.callers(pos).map(|c| (c.graded, Some(c.sites))), + "callees" => g.callees(pos).map(|c| (c.graded, Some(c.sites))), + "impact" => g.impact(pos).map(|i| (i, None)), + "refs" => { + let s = g.references(pos); + for (w, &word) in s.rows.iter().enumerate() { + let mut bits = word; + while bits != 0 { + let b = bits.trailing_zeros(); + bits &= bits - 1; + let row = w * 64 + b as usize; + let at = g + .site(row) + .map(|(f, st, _)| format!("{f}:{}", line_of(&src, f, st))) + .unwrap_or_else(|| "-".into()); + println!( + "ref\t{}\t{}\t{at}", + g.row_predicate(row), + g.row_subject(row) + ); + } + } + println!("sites\tconfirmed={}\tpossible={}", s.confirmed, s.possible); + return ExitCode::SUCCESS; + } + _ => { + eprintln!("unknown command {cmd}"); + return ExitCode::from(2); + } + }; + match graded { + Ok((gr, sites)) => { + for (grade, mask) in [ + ("CONFIRMED", &gr.confirmed), + ("POSSIBLE", &gr.possible), + ("UNKNOWN", &gr.unknown), + ] { + for n in names(&g, mask) { + println!("{cmd}\t{grade}\t{n}"); + } + } + if let Some(s) = sites { + println!("sites\t{s}"); + } + // The store only sees the crates it was built from. A public symbol can + // have callers anywhere else, so an empty answer is "not observed", never + // "none". This is printed on every answer, not only on empty ones. + if cmd != "callees" && bit(g.public(), pos) { + println!("{cmd}\tUNKNOWN\texternal-callers-unobserved\t{sym} is PUBLIC"); + } + for f in observed_files(&g) { + println!("coverage\tobserved-file\t{f}"); + } + ExitCode::SUCCESS + } + Err(e) => { + println!("REFUSED\t{cmd}\t{e:?}"); + ExitCode::from(3) + } + } +}