From 1bb16605110c610c98a1599d1a61228bf1f1271b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 11:04:24 +0700 Subject: [PATCH] spec(t27f): derive pass adds tested_by, data_flow and UNKNOWN call targets (Closes #10191) derive_graph(g, src) appends what the exporter must not claim: DERIVED tested_by (calls read backwards), DERIVED data_flow (a const or use named in a fn's return statement) and UNKNOWN opaque nodes for undeclared qualified call targets. It never changes an EXACT fact. Exporter plus derive equal the tutorial 08 fixture: 15 of 15 nodes, 16 of 16 edges, no special case. Co-Authored-By: Claude Sonnet 5.5 --- .claude/skills/t27f/SKILL.md | 15 +- specs/OWNERS.md | 2 +- specs/t27f/spec_graph_derive.t27 | 691 +++++++++++++++++++++++++++++++ 3 files changed, 701 insertions(+), 7 deletions(-) create mode 100644 specs/t27f/spec_graph_derive.t27 diff --git a/.claude/skills/t27f/SKILL.md b/.claude/skills/t27f/SKILL.md index 32f0641a8d..d6d94a81ef 100644 --- a/.claude/skills/t27f/SKILL.md +++ b/.claude/skills/t27f/SKILL.md @@ -60,7 +60,8 @@ the reels. Describing T27F as #1677 is the error this section exists to stop (ow |---|---|---| | Spec -> graph IR schema (the core) | `specs/t27f/spec_graph.t27` (t27#10020) | spec with tests: node / edge kinds, labels, spans, `validate_graph`, line -> node mapping, node -> ui_plan widget, one hand-read fixture (`specs/tutorial/08_modules_and_arrays.t27`) | | Graph view: layout of a spec graph | `specs/t27f/spec_graph_view.t27` (t27#10034) | spec with tests: one column per node kind, size / colour / dash / row order from the inference label, UNKNOWN nodes alone in a band, every edge with a source line, node -> widget through `node_widget`; numbers only, laid out on the hand-read fixture; drawn by the MCP tool `t27f_graph` (gHashTag/t27-mcp#9) | -| Spec -> graph IR exporter | `specs/t27f/spec_graph_export.t27` (t27#10162) | spec with tests: `export_graph(path, src)` is a deterministic byte scanner over the source, `export_verdict` is `validate_graph` of the result. One node per top-level declaration (a leading `pub ` is allowed), spans to the matching closing brace, every node and edge EXACT or (unclassifiable) OPAQUE + UNKNOWN, CALLS / USES / CONSTRAINS edges with the line of the use, refusal past 192 nodes or 254 edges. On the tutorial 08 snapshot it equals the hand-read fixture on all 14 declaration nodes and all 9 EXACT edges; it does not emit the fixture's `std.testing` UNKNOWN node, nor its 7 DERIVED edges (4 data flow, 3 tested_by), because a scanner never derives. Limits: textual matching without scope or type resolution, no block comments, no struct/enum bodies, no cross-spec `use` resolution, capacity 192 nodes and 254 edges (about 98 percent of specs in specs/ fit; the rest are refused), takes a `[]const u8` slice rather than `[65536]u8` plus a length. Not wired to a host: the MCP tool does not call it. AST/IR audit is trinity#1650, pilot choice #1651 | +| Spec -> graph IR exporter | `specs/t27f/spec_graph_export.t27` (t27#10162) | spec with tests: `export_graph(path, src)` is a deterministic byte scanner over the source, `export_verdict` is `validate_graph` of the result. One node per top-level declaration (a leading `pub ` is allowed), spans to the matching closing brace, every node and edge EXACT or (unclassifiable) OPAQUE + UNKNOWN, CALLS / USES / CONSTRAINS edges with the line of the use, refusal past 192 nodes or 254 edges. On the tutorial 08 snapshot it equals the hand-read fixture on all 14 declaration nodes and all 9 EXACT edges; it does not emit the fixture's `std.testing` UNKNOWN node, nor its 7 DERIVED edges (4 data flow, 3 tested_by), because a scanner never derives; the derive pass below adds them. Limits: textual matching without scope or type resolution, no block comments, no struct/enum bodies, no cross-spec `use` resolution, capacity 192 nodes and 254 edges (about 98 percent of specs in specs/ fit; the rest are refused), takes a `[]const u8` slice rather than `[65536]u8` plus a length. Not wired to a host: the MCP tool does not call it. AST/IR audit is trinity#1650, pilot choice #1651 | +| Graph IR derive pass | `specs/t27f/spec_graph_derive.t27` (t27#10191) | spec with tests: `derive_graph(g, src)` appends what the exporter must not claim and changes nothing it holds. R1 DERIVED `tested_by` = every EXACT CALLS edge from a test, invariant or bench to a fn read backwards (no line). R2 DERIVED `data_flow` = a const or `use` that an EXACT USES edge ties to a fn and that is named inside one of the fn's return statements (from `return` to the next `;`), on the line of the first such name. R3 UNKNOWN opaque node = an undeclared qualified call target of three or more segments (`std.testing.expectEqual(` names `std.testing`), spanning the lines that call through it. Exporter plus derive equal the tutorial 08 fixture as sets: 15 of 15 nodes, 16 of 16 edges, no special case. Limits: names matched as text; call results and flow through locals are not derived; R3 needs 3 or more segments (two cannot be told from a method call); a graph that does not validate, or a source of another line count, comes back unchanged; past 192 nodes or 254 edges the result is refused with the too-many verdict. Not wired to a host: the MCP tool does not call it | | UI plan IR + trusted widget catalog | `specs/t27f/ui_plan.t27` (t27#9962) | spec with tests; no renderer draws a plan yet | | Honeycomb focus+context geometry | `specs/t27f/reel.t27` | spec; stills drawn by the MCP tool `t27f_view` | | Renderer in the Trinity UI | gHashTag/trinity | **missing**; no T27F widget is live | @@ -84,10 +85,12 @@ is not progress on the core. 3. Show it as a table (node, kind, span, label) and, if useful, a diagram whose every arrow is a row of that table. Nothing is drawn that the table does not back. 4. Say plainly that this is a manual reading unless a graph came out of `export_graph` - (`specs/t27f/spec_graph_export.t27`). The exporter reads declarations, spans and exact - CALLS / USES / CONSTRAINS edges only, within 192 nodes and 254 edges; DERIVED edges (tested_by, - data flow), UNKNOWN regions and anything larger are still a manual reading, and no host runs - the exporter yet. Name that gap rather than hide it. + (`specs/t27f/spec_graph_export.t27`), with `derive_graph` (`specs/t27f/spec_graph_derive.t27`) + on top. The exporter reads declarations, spans and exact CALLS / USES / CONSTRAINS edges only, + within 192 nodes and 254 edges; the derive pass adds DERIVED tested_by and data_flow edges + and UNKNOWN opaque nodes for undeclared qualified call targets, by its three stated rules. + Anything the rules do not reach (SUGGESTED explanations, call-result flow, anything larger) + is still a manual reading, and no host runs either pass yet. Name that gap rather than hide it. ## Application: topic map (gHashTag/trinity#1677) @@ -191,6 +194,6 @@ journey is saved, save it as a `.t27` data module, not JSON. Saving follows the ## What this skill does not claim -The graph IR is a schema (`specs/t27f/spec_graph.t27`) and `specs/t27f/spec_graph_export.t27` turns source into it, but only exact declarations, spans and edges within the IR's capacity, and no host calls that exporter yet; no renderer draws a T27F view in the Trinity UI, no +The graph IR is a schema (`specs/t27f/spec_graph.t27`) and `specs/t27f/spec_graph_export.t27` turns source into it, but only exact declarations, spans and edges within the IR's capacity, with `specs/t27f/spec_graph_derive.t27` adding the derived and unknown part by stated rules, and no host calls either yet; no renderer draws a T27F view in the Trinity UI, no runtime dispatches Bees from a spec, and nothing publishes on its own. If a step needs one of them, say that it is missing; do not simulate it. diff --git a/specs/OWNERS.md b/specs/OWNERS.md index 08608d167c..c42f775cf5 100644 --- a/specs/OWNERS.md +++ b/specs/OWNERS.md @@ -28,7 +28,7 @@ | `docs/` | **Z-Zeta** (with **T-Queen** for `chapters/queen.t27`) | The system documentation of `t27.ai/#/docs` as `.t27` specs (`docs/system.t27`, `KIND = "docs"`; `docs/chapters/.t27`, `KIND = "docs-chapter"`): chapter ids, sections, sources, the figure and table the site generates; English prose in `docs/system/.md`, Russian via `i18n/docs-ru.t27` | | `ui/` | **T-Queen** | The site's viewport contract as a `.t27` spec (`ui/viewport.t27`, `KIND = "viewport"`): tiers by CSS viewport width, panes per tier, the 44 px touch minimum, the six-size QA matrix and the Queen rail capacity read from `Queen.css`; the site (gHashTag/trinity) generates `viewport.generated.ts` / `.css` from a vendored copy and evaluates the spec's own test blocks; `ui/queen_evidence.t27` (`module ui_queen_evidence`): the evidence constants of the Queen's FFN and Ternary Check panel, from which the site generates `queenEvidence.generated.ts`; canonical here since S10, byte-identical to the copy the site carried alone | | `catalog/` | **T-Queen** | How the site's spec catalog and the Queen map find the repositories that write `.t27` (`catalog/discovery.t27`, `KIND = "discovery"`): the GitHub owners scanned, the exclusions, what makes a candidate qualify (a declaration in the compiler's AST, not a file extension) and the limits; the site (gHashTag/trinity) vendors a byte-identical copy and `scripts/discover-t27-worlds.mjs` reads it through the compiler wasm before touching GitHub | -| `t27f/` | **T-Queen** | T27F, the visual spec of a .t27 file (gHashTag/trinity#1648, RFC #1649; definition in `.claude/skills/t27f/SKILL.md`): `t27f/spec_graph.t27` (module `t27f_spec_graph`): the core graph IR a spec becomes -- node and edge kinds, inference labels, source spans, `validate_graph`, source mapping both ways and the node -> ui_plan widget binding, with one hand-read fixture; `t27f/spec_graph_export.t27` (module `t27f_spec_graph_export`): the exporter, a deterministic byte scanner from spec source to that graph -- declarations, brace-matched spans, exact calls/uses/constrains edges, refusal past the IR capacity, checked against the hand-read fixture; `t27f/spec_graph_view.t27` (module `t27f_spec_graph_view`): the graph view, a deterministic layout of a spec graph -- one column per node kind, style and row order from the inference label, UNKNOWN nodes drawn alone, every edge with a source line; numbers only, a host draws them; `t27f/ui_plan.t27` (module `t27f_ui_plan`): the renderer-neutral UI plan IR and the trusted widget catalog. Applications built on it: the topic-to-value map of gHashTag/trinity#1677 (`t27f/topic_engine.t27`, module `T27fTopicEngine`): the 3 x 9 = 27 lesson shape, intake and gap rules, keyword routing to one domain, the Bee dispatch cap, the evidence and approval gates, and progression that is never money; driven by the Claude Code skill `.claude/skills/t27f/SKILL.md` through the t27 MCP server; `t27f/reel.t27` (module `T27fReel`): the video format of a topic map and the still views of a Claude Code answer -- honeycomb geometry, focus+context camera, scene catalog, per-target limits, gap styling, the posting gate and the channel per host; numbers only, a host draws them; `t27f/deck.t27` (module `T27fDeck`): the default look of a reel, every scene a presentation slide -- layouts per scene, regions, type sizes, glass card, palette kept off the status colours, contrast and card fades | +| `t27f/` | **T-Queen** | T27F, the visual spec of a .t27 file (gHashTag/trinity#1648, RFC #1649; definition in `.claude/skills/t27f/SKILL.md`): `t27f/spec_graph.t27` (module `t27f_spec_graph`): the core graph IR a spec becomes -- node and edge kinds, inference labels, source spans, `validate_graph`, source mapping both ways and the node -> ui_plan widget binding, with one hand-read fixture; `t27f/spec_graph_export.t27` (module `t27f_spec_graph_export`): the exporter, a deterministic byte scanner from spec source to that graph -- declarations, brace-matched spans, exact calls/uses/constrains edges, refusal past the IR capacity, checked against the hand-read fixture; `t27f/spec_graph_derive.t27` (module `t27f_spec_graph_derive`): the derive pass, a second deterministic scan that appends DERIVED tested_by and data_flow edges and UNKNOWN opaque nodes for undeclared qualified call targets by three stated rules and never changes an exact fact -- exporter plus derive equal the tutorial 08 fixture; `t27f/spec_graph_view.t27` (module `t27f_spec_graph_view`): the graph view, a deterministic layout of a spec graph -- one column per node kind, style and row order from the inference label, UNKNOWN nodes drawn alone, every edge with a source line; numbers only, a host draws them; `t27f/ui_plan.t27` (module `t27f_ui_plan`): the renderer-neutral UI plan IR and the trusted widget catalog. Applications built on it: the topic-to-value map of gHashTag/trinity#1677 (`t27f/topic_engine.t27`, module `T27fTopicEngine`): the 3 x 9 = 27 lesson shape, intake and gap rules, keyword routing to one domain, the Bee dispatch cap, the evidence and approval gates, and progression that is never money; driven by the Claude Code skill `.claude/skills/t27f/SKILL.md` through the t27 MCP server; `t27f/reel.t27` (module `T27fReel`): the video format of a topic map and the still views of a Claude Code answer -- honeycomb geometry, focus+context camera, scene catalog, per-target limits, gap styling, the posting gate and the channel per host; numbers only, a host draws them; `t27f/deck.t27` (module `T27fDeck`): the default look of a reel, every scene a presentation slide -- layouts per scene, regions, type sizes, glass card, palette kept off the status colours, contrast and card fades | | `t27mcp/` | **T-Queen** | The decisions of the t27 MCP server (gHashTag/t27-mcp) as `.t27` specs, compiled to wasm that the server runs: `t27mcp/check_hints.t27` (module `T27mcpCheckHints`): which short "write this instead" hint a compiler message gets for foreign syntax (`in` as a name, `as u3`, `x++`, `a ? b : c`, `match`), and the line number a message names; `t27mcp/examples.t27` (module `T27mcpExamples`): which short slice of the published corpus, pinned to one commit, answers a question about clocked or combinational modules, `fn`, `test` blocks and the reset styles; `t27mcp/spec_brief.t27` (module `T27mcpSpecBrief`): which manifest fields a short spec row keeps and why a failing spec fails (a bit set of reasons plus their text templates); the server's JavaScript is I/O glue and holds no rule | | `trinity/` | **T-Queen** + **A-Architect** | The project manifest of gHashTag/trinity as `.t27` specs (`trinity/project.t27`, `KIND = "project"`; `trinity/capabilities/.t27`, `KIND = "capability"`): the pinned consumer revision, profiles, dispositions and evidence tags, dialect and build counts, dependency pins and the work packages of gHashTag/trinity#988; each card names its owner, canonical spec, implementation and generated paths, build targets, acceptance command and evidence; `tools/trinity_manifest.py` derives the inventory from a clean pinned checkout and holds the cards to it; `trinity/compiler_matrix.t27` (`KIND = "compiler-matrix"`) names the pinned compiler, the backends, the stages and the features of the executable subset with their fixtures under `bootstrap/tests/fixtures/trinity_matrix/`, and `tools/trinity_compiler_matrix.py` measures them; `trinity/build_graph.t27` (`KIND = "build-graph"`) declares the consumer's toolchain, pins, profiles, generated-file boundaries and receipt policy, and `tools/trinity_build_receipt.py` derives the graph, writes the receipts and judges drift; the consumer vendors a byte-identical copy and generates its manifest from it (S12). Shared contracts stay in their own subtrees (`numeric/`, `vsa/`, `queen/`, `tools/`, `docs/`, `ui/`) and are cited, never copied | diff --git a/specs/t27f/spec_graph_derive.t27 b/specs/t27f/spec_graph_derive.t27 new file mode 100644 index 0000000000..78cb8b736f --- /dev/null +++ b/specs/t27f/spec_graph_derive.t27 @@ -0,0 +1,691 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/t27f/spec_graph_derive.t27 -- the T27F derive pass: SpecGraph + spec source -> SpecGraph +; with the facts a scanner must not claim (RFC gHashTag/trinity#1649, epic gHashTag/trinity#1648, +; tracked in gHashTag/t27#10191). +; specs/t27f/spec_graph_export.t27 reads only EXACT facts. The hand-read fixture +; tutorial_08_graph() holds more: 4 DATA_FLOW and 3 TESTED_BY edges (DERIVED) and node 14, +; std.testing (UNKNOWN). This file is the second pass that adds them, and only them. +; It is a separate module, not an extension of the exporter, so that the exporter's promise "the +; scanner never emits DERIVED or SUGGESTED" (its test the_scanner_never_emits_derived_or_suggested) +; stays true and checkable on its own; this file reuses the exporter's byte helpers through `use`. +; derive_graph(g, src) never changes or removes anything in g. It appends, in this order, and every +; rule below follows EDGE_FROM_KINDS / EDGE_TO_KINDS of spec_graph.t27: +; R1 TESTED_BY (DERIVED). For every EXACT CALLS edge from a test, invariant or bench t to a fn f, +; add TESTED_BY f -> t, with no source line. This is the rule spec_graph states for the +; fixture ("tested_by is calls read backwards"; tested_by_matches_calls). A CALLS edge from a +; fn is not a test and adds nothing. +; R2 DATA_FLOW (DERIVED). For every EXACT USES edge from a fn f to a const or `use` c, where the +; name c is matched by appears in a return statement of f (from the word `return` to the next +; `;`, outside strings, character literals and comments), add DATA_FLOW c -> f on the line of +; the first such name. This is the fixture's own comment: "the named values are operands of +; each return expression, so they reach the result". A name used in a `let`, in a condition, +; after the return statement's `;`, or from a test, invariant or bench body is a USES edge +; (the exporter's) and no DATA_FLOW. +; R3 UNKNOWN external call target. In the body of a fn, test, invariant or bench, a call +; `a.b.c(` of a qualified path of three or more segments whose first segment is not a declared +; fn, const or `use` name of the spec adds one NODE_OPAQUE with LABEL_UNKNOWN per distinct +; path-without-its-last-segment (here "a.b"), spanning the first through the last line that +; calls through it. This is the fixture's own comment: the tests call std.testing.expectEqual, +; "no `use` in the file declares std", so what it is cannot be read from this source. An +; UNKNOWN node has no edge in or out (validate_edge refuses one), so R3 adds none. +; Why each added fact has its label: R1 and R2 are computed from EXACT facts by a stated rule, so +; they are DERIVED; R3 is a name the source uses and does not define, so it is UNKNOWN. +; Findings on the tutorial 08 fixture: all 7 DERIVED edges and node 14 come out of R1, R2 and R3 +; with no special case. Two choices are the rules' own and not read off the fixture, and are +; stated so nobody takes them for measured: (a) R3 needs three or more path segments, because the +; fixture has the only instance (std.testing.expectEqual, three) and a two-segment `x.f(` cannot +; be told from a method call on a local value; (b) R2 reads only names, not call results, because +; no fixture edge is a fn result flowing into a caller (`return f()` adds nothing). +; Not claimed here: +; - Names are matched as text, as in the exporter: a local named like a const counts as a use. +; - The half of the hand-reader's reason that says std "is not a corpus spec" cannot be checked +; from one source: a first segment that names another spec's module but is not imported is +; reported as UNKNOWN, which is the weakest claim and so still honest. +; - DATA_FLOW into a test, invariant or bench, from an opaque region or from a call result, and +; flow through a local variable, are not derived. +; - If g does not validate, or src is not the source g was read from (its line count differs), +; derive_graph returns g unchanged: it will not guess spans. +; - Capacity: past 192 nodes or 254 edges the count keeps going, so validate_graph answers +; ERR_TOO_MANY_NODES or ERR_TOO_MANY_EDGES; the result is refused, never truncated. +; - The tutorial 08 source is the exporter's snapshot (sha256 +; c291e925d9dabef8b72b5a64aef153a2126c0b0b43d67bc08b1b2d7eaa98039a), not the live file. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module t27f_spec_graph_derive; + +use t27f::spec_graph::SpecGraph; +use t27f::spec_graph::blank_graph; +use t27f::spec_graph::with_node; +use t27f::spec_graph::with_edge; +use t27f::spec_graph::validate_graph; +use t27f::spec_graph::tutorial_08_graph; +use t27f::spec_graph::with_suggestion; +use t27f::spec_graph::tested_by_matches_calls; +use t27f::spec_graph::kind_bit; +use t27f::spec_graph::has_edge; +use t27f::spec_graph::count_node_kind; +use t27f::spec_graph::count_node_label; +use t27f::spec_graph::count_edge_kind; +use t27f::spec_graph::count_edge_label; +use t27f::spec_graph::NODE_MODULE; +use t27f::spec_graph::NODE_CONST; +use t27f::spec_graph::NODE_FN; +use t27f::spec_graph::NODE_TEST; +use t27f::spec_graph::NODE_INVARIANT; +use t27f::spec_graph::NODE_BENCH; +use t27f::spec_graph::NODE_USE; +use t27f::spec_graph::NODE_OPAQUE; +use t27f::spec_graph::EDGE_CALLS; +use t27f::spec_graph::EDGE_USES; +use t27f::spec_graph::EDGE_TESTED_BY; +use t27f::spec_graph::EDGE_DATA_FLOW; +use t27f::spec_graph::EDGE_FROM_KINDS; +use t27f::spec_graph::EDGE_TO_KINDS; +use t27f::spec_graph::LABEL_EXACT; +use t27f::spec_graph::LABEL_DERIVED; +use t27f::spec_graph::LABEL_SUGGESTED; +use t27f::spec_graph::LABEL_UNKNOWN; +use t27f::spec_graph::MAX_NODES; +use t27f::spec_graph::MAX_EDGES; +use t27f::spec_graph::NO_LINE; +use t27f::spec_graph::NO_INDEX; +use t27f::spec_graph::GRAPH_OK; +use t27f::spec_graph::ERR_TOO_MANY_NODES; +use t27f::spec_graph::ERR_TOO_MANY_EDGES; +use t27f::spec_graph_export::export_graph; +use t27f::spec_graph_export::TUTORIAL_08_SRC; +use t27f::spec_graph_export::count_lines; +use t27f::spec_graph_export::skip_space; +use t27f::spec_graph_export::word_end; +use t27f::spec_graph_export::ex_word; +use t27f::spec_graph_export::skip_lit; +use t27f::spec_graph_export::line_end_at; +use t27f::spec_graph_export::classify; +use t27f::spec_graph_export::Decl; +use t27f::spec_graph_export::edge_seen; +use t27f::spec_graph_export::node_matches; +use t27f::spec_graph_export::nodes_in_common; +use t27f::spec_graph_export::edge_in; +use t27f::spec_graph_export::edges_shared; + +/// The fewest path segments a call must have for R3 to read its namespace. +pub const DV_MIN_SEGMENTS : u32 = 3; + +/// The byte offset where 1-based `line` starts, or src.len when the source has fewer lines. +pub fn dv_line_start(src: []const u8, line: u32) -> usize { + var cur : u32 = 1; + var k : usize = 0; + while (k < src.len and cur < line) { + if (src[k] == '\n') { cur += 1; } + k += 1; + } + return k; +} + +/// The text an identifier must equal to refer to node t: its name, or a `use` path's last +/// segment. Read from the node's own declaration line, the way the exporter read it. +pub fn dv_match_text(g: SpecGraph, src: []const u8, t: u32) -> str { + const p : usize = dv_line_start(src, g.line_start[t as usize]); + if (p >= src.len) { return ""; } + const d : Decl = classify(src, p, line_end_at(src, p)); + return src[d.sa .. d.sb]; +} + +/// The first line of node f's span on which `want` is a name inside a return statement, or +/// NO_LINE. A return statement runs from the word `return` to the next `;` (it may span lines). +pub fn dv_return_use_line(g: SpecGraph, src: []const u8, f: u32, want: str) -> u32 { + const fs : usize = f as usize; + const last : u32 = g.line_end[fs]; + var line : u32 = g.line_start[fs]; + var p : usize = dv_line_start(src, line); + var in_ret : bool = false; + while (line <= last and p < src.len) { + const b : usize = line_end_at(src, p); + var i : usize = skip_space(src, p, b); + if (i < b and src[i] == ';') { i = b; } + while (i < b) { + const c : u8 = src[i]; + if (c == '/' and i + 1 < b and src[i + 1] == '/') { + i = b; + } else { + const j : usize = skip_lit(src, b, i); + if (j != i) { + i = j; + } else { + if (ex_word(c)) { + const e : usize = word_end(src, i, b); + if (c < '0' or c > '9') { + const tok : str = src[i .. e]; + if (tok == "return") { in_ret = true; } + if (in_ret and tok == want) { return line; } + } + i = e; + } else { + if (c == ';') { in_ret = false; } + i += 1; + } + } + } + } + p = b + 1; + line += 1; + } + return NO_LINE; +} + +/// R1: for each of the first e0 edges that is an EXACT CALLS from a test, invariant or bench to a +/// fn, the TESTED_BY edge back. +pub fn dv_tested_by(g0: SpecGraph, e0: u32) -> SpecGraph { + var g : SpecGraph = g0; + const checkers : u32 = kind_bit(NODE_TEST) | kind_bit(NODE_INVARIANT) | kind_bit(NODE_BENCH); + var j : u32 = 0; + while (j < e0) { + const m : usize = j as usize; + if (g.edge_kind[m] == EDGE_CALLS and g.edge_label[m] == LABEL_EXACT) { + const f : u32 = g.edge_from[m] as u32; + const t : u32 = g.edge_to[m] as u32; + const fk : u8 = g.node_kind[f as usize]; + if (g.node_kind[t as usize] == NODE_FN and (kind_bit(fk) & checkers) != 0) { + if (edge_seen(g, EDGE_TESTED_BY, t, f) == false) { + g = with_edge(g, EDGE_TESTED_BY, t as u8, f as u8, LABEL_DERIVED, NO_LINE); + } + } + } + j += 1; + } + return g; +} + +/// R2: for each of the first e0 edges that is an EXACT USES from a fn to a const or `use`, the +/// DATA_FLOW into the fn when the used name is in one of the fn's return statements. +pub fn dv_data_flow(g0: SpecGraph, src: []const u8, e0: u32) -> SpecGraph { + var g : SpecGraph = g0; + var j : u32 = 0; + while (j < e0) { + const m : usize = j as usize; + if (g.edge_kind[m] == EDGE_USES and g.edge_label[m] == LABEL_EXACT) { + const f : u32 = g.edge_from[m] as u32; + const c : u32 = g.edge_to[m] as u32; + const ck : u8 = g.node_kind[c as usize]; + if (g.node_kind[f as usize] == NODE_FN and (ck == NODE_CONST or ck == NODE_USE)) { + const line : u32 = dv_return_use_line(g, src, f, dv_match_text(g, src, c)); + if (line != NO_LINE and edge_seen(g, EDGE_DATA_FLOW, c, f) == false) { + g = with_edge(g, EDGE_DATA_FLOW, c as u8, f as u8, LABEL_DERIVED, line); + } + } + } + j += 1; + } + return g; +} + +/// Is `tok` the name of a fn, const or `use` among the first n0 nodes? +pub fn dv_declared(g: SpecGraph, src: []const u8, n0: u32, tok: str) -> bool { + var t : u32 = 1; + while (t < n0) { + const k : u8 = g.node_kind[t as usize]; + if (k == NODE_FN or k == NODE_CONST or k == NODE_USE) { + const m : str = dv_match_text(g, src, t); + if (m == tok) { return true; } + } + t += 1; + } + return false; +} + +/// The stored UNKNOWN opaque node named `name`, or NO_INDEX. +pub fn dv_find_unknown(g: SpecGraph, name: str) -> u32 { + var t : u32 = 1; + while (t < g.node_count and t < MAX_NODES) { + const s : usize = t as usize; + if (g.node_kind[s] == NODE_OPAQUE and g.node_label[s] == LABEL_UNKNOWN) { + const nm : str = g.node_name[s]; + if (nm == name) { return t; } + } + t += 1; + } + return NO_INDEX; +} + +/// Record a call through namespace `ns` on `line`: a new UNKNOWN node, or a wider span for one +/// this pass already added (a node that was in g is left as it was). +pub fn dv_note_unknown(g0: SpecGraph, n0: u32, ns: str, line: u32) -> SpecGraph { + var g : SpecGraph = g0; + const at : u32 = dv_find_unknown(g, ns); + if (at == NO_INDEX) { + return with_node(g, NODE_OPAQUE, LABEL_UNKNOWN, ns, line, line); + } + if (at >= n0) { + const s : usize = at as usize; + if (line > g.line_end[s]) { g.line_end[s] = line; } + if (line < g.line_start[s]) { g.line_start[s] = line; } + } + return g; +} + +/// R3 on one source line src[p..b] of a body: every name path outside strings, character +/// literals and comments. +pub fn dv_line_unknowns(g0: SpecGraph, src: []const u8, n0: u32, p: usize, b: usize, line: u32) -> SpecGraph { + var g : SpecGraph = g0; + var i : usize = skip_space(src, p, b); + if (i < b and src[i] == ';') { return g; } + while (i < b) { + const c : u8 = src[i]; + if (c == '/' and i + 1 < b and src[i + 1] == '/') { + i = b; + } else { + const j : usize = skip_lit(src, b, i); + if (j != i) { + i = j; + } else { + if (ex_word(c)) { + const e : usize = word_end(src, i, b); + var next : usize = e; + if ((c < '0' or c > '9') and (i == p or src[i - 1] != '.')) { + var segs : u32 = 1; + var last_start : usize = i; + var k : usize = e; + while (k + 1 < b and src[k] == '.' and ex_word(src[k + 1]) and (src[k + 1] < '0' or src[k + 1] > '9')) { + last_start = k + 1; + k = word_end(src, k + 1, b); + segs += 1; + } + const q : usize = skip_space(src, k, b); + if (segs >= DV_MIN_SEGMENTS and q < b and src[q] == '(') { + const head : str = src[i .. e]; + if (dv_declared(g, src, n0, head) == false) { + g = dv_note_unknown(g, n0, src[i .. last_start - 1], line); + } + } + next = k; + } + i = next; + } else { + i += 1; + } + } + } + } + return g; +} + +/// R3 over the whole spec: the body of every EXACT fn, test, invariant and bench among the first +/// n0 nodes, line by line. +pub fn dv_unknown_targets(g0: SpecGraph, src: []const u8, n0: u32) -> SpecGraph { + var g : SpecGraph = g0; + var k : u32 = 1; + while (k < n0) { + const ks : usize = k as usize; + const kind : u8 = g.node_kind[ks]; + if ((kind == NODE_FN or kind == NODE_TEST or kind == NODE_INVARIANT or kind == NODE_BENCH) and g.node_label[ks] == LABEL_EXACT and g.line_start[ks] != NO_LINE) { + const last : u32 = g.line_end[ks]; + var line : u32 = g.line_start[ks]; + var p : usize = dv_line_start(src, line); + while (line <= last and p < src.len) { + const b : usize = line_end_at(src, p); + g = dv_line_unknowns(g, src, n0, p, b, line); + p = b + 1; + line += 1; + } + } + k += 1; + } + return g; +} + +/// g plus everything R1, R2 and R3 derive from it and from `src`, the source g was read from. +/// Returned unchanged when g does not validate or src has a different number of lines than g. +pub fn derive_graph(g: SpecGraph, src: []const u8) -> SpecGraph { + if (validate_graph(g) != GRAPH_OK) { return g; } + if (count_lines(src) != g.line_count) { return g; } + const n0 : u32 = g.node_count; + const e0 : u32 = g.edge_count; + var h : SpecGraph = g; + h = dv_tested_by(h, e0); + h = dv_data_flow(h, src, e0); + h = dv_unknown_targets(h, src, n0); + return h; +} + +/// Does b still hold every node and edge of a, unchanged in every field and at the same index? +pub fn dv_prefix_kept(a: SpecGraph, b: SpecGraph) -> bool { + if (b.node_count < a.node_count or b.edge_count < a.edge_count) { return false; } + var i : u32 = 0; + while (i < a.node_count and i < MAX_NODES) { + const k : usize = i as usize; + if (a.node_kind[k] != b.node_kind[k] or a.node_label[k] != b.node_label[k]) { return false; } + if (a.line_start[k] != b.line_start[k] or a.line_end[k] != b.line_end[k]) { return false; } + const an : str = a.node_name[k]; + const bn : str = b.node_name[k]; + if ((an == bn) == false) { return false; } + i += 1; + } + var j : u32 = 0; + while (j < a.edge_count and j < MAX_EDGES) { + const m : usize = j as usize; + if (a.edge_kind[m] != b.edge_kind[m] or a.edge_from[m] != b.edge_from[m] or a.edge_to[m] != b.edge_to[m]) { return false; } + if (a.edge_label[m] != b.edge_label[m] or a.edge_line[m] != b.edge_line[m]) { return false; } + j += 1; + } + return true; +} + +test derive_after_export_equals_the_tutorial_08_fixture { + const path : str = "specs/tutorial/08_modules_and_arrays.t27"; + const e : SpecGraph = export_graph(path, TUTORIAL_08_SRC); + const d : SpecGraph = derive_graph(e, TUTORIAL_08_SRC); + const f : SpecGraph = tutorial_08_graph(); + assert validate_graph(d) == GRAPH_OK; + assert d.spec_path == f.spec_path; + assert d.line_count == f.line_count; + // nodes: 15 by index, each equal in kind, label, name and span + assert d.node_count == 15; + assert nodes_in_common(d, f) == 15; + assert node_matches(d, f, 14); + assert d.node_name[14] == "std.testing"; + assert d.node_kind[14] == NODE_OPAQUE; + assert d.node_label[14] == LABEL_UNKNOWN; + assert d.line_start[14] == 79 and d.line_end[14] == 89; + // edges: 16, equal as sets in kind, endpoints, label and line, in both directions + assert d.edge_count == 16; + assert edges_shared(d, f) == 16; + assert edges_shared(f, d) == 16; + // each rule supplies exactly its share of the fixture's seven DERIVED edges + assert count_edge_kind(d, EDGE_TESTED_BY) == 3; + assert count_edge_kind(d, EDGE_DATA_FLOW) == 4; + assert count_edge_label(d, LABEL_DERIVED) == 7; + assert edge_in(d, EDGE_TESTED_BY, 8, 10, LABEL_DERIVED, NO_LINE); + assert edge_in(d, EDGE_TESTED_BY, 9, 11, LABEL_DERIVED, NO_LINE); + assert edge_in(d, EDGE_TESTED_BY, 4, 12, LABEL_DERIVED, NO_LINE); + assert edge_in(d, EDGE_DATA_FLOW, 2, 4, LABEL_DERIVED, 38); + assert edge_in(d, EDGE_DATA_FLOW, 3, 4, LABEL_DERIVED, 38); + assert edge_in(d, EDGE_DATA_FLOW, 6, 8, LABEL_DERIVED, 67); + assert edge_in(d, EDGE_DATA_FLOW, 7, 9, LABEL_DERIVED, 71); + // the SpecGraph rule for the fixture's TESTED_BY edges holds for the derived ones + assert tested_by_matches_calls(d); + // negative controls: the exporter alone is short of the fixture by exactly this pass + assert e.node_count == 14 and e.edge_count == 9; + assert nodes_in_common(e, f) == 14; + assert edges_shared(f, e) == 9; + assert edges_shared(f, e) != edges_shared(f, d); + // and the comparison can fail: a moved span, a shifted edge line, a changed label + var moved : SpecGraph = tutorial_08_graph(); + moved.line_end[14] = 90; + assert node_matches(d, moved, 14) == false; + assert nodes_in_common(d, moved) == 14; + var shifted : SpecGraph = tutorial_08_graph(); + shifted.edge_line[5] = 37; + assert edges_shared(d, shifted) == 15; + var relabeled : SpecGraph = tutorial_08_graph(); + relabeled.node_label[14] = LABEL_DERIVED; + assert node_matches(d, relabeled, 14) == false; +} + +test r1_tested_by_is_calls_read_backwards { + const src : []const u8 = "module m;\nfn f() u8 { return 1; }\nfn g() u8 { return f(); }\ntest \"t\" {\n assert f() == 1;\n assert f() == 1;\n}\ninvariant inv\n assert f() == 1\nbench \"b\" {\n f();\n}\n"; + const e : SpecGraph = export_graph("specs/x.t27", src); + assert validate_graph(e) == GRAPH_OK; + assert e.node_count == 6; + assert count_edge_kind(e, EDGE_CALLS) == 4; + const d : SpecGraph = derive_graph(e, src); + assert validate_graph(d) == GRAPH_OK; + // f is tested by the test (3), the invariant (4) and the bench (5); the line of a derived edge is none + assert edge_in(d, EDGE_TESTED_BY, 1, 3, LABEL_DERIVED, NO_LINE); + assert edge_in(d, EDGE_TESTED_BY, 1, 4, LABEL_DERIVED, NO_LINE); + assert edge_in(d, EDGE_TESTED_BY, 1, 5, LABEL_DERIVED, NO_LINE); + assert count_edge_kind(d, EDGE_TESTED_BY) == 3; + // two calls from one test are one TESTED_BY edge, not two + assert d.edge_count == e.edge_count + 3; + assert tested_by_matches_calls(d); + // negative controls: g calls f, but g is a fn and not a test, so f is not tested by g; and + // nothing is tested by what it calls itself (no edge back from a test to a fn it is not tested by) + assert has_edge(d, EDGE_TESTED_BY, 1, 2) == false; + assert has_edge(d, EDGE_TESTED_BY, 3, 1) == false; + // a spec whose tests call nothing derives no TESTED_BY at all + const quiet : []const u8 = "module m;\nfn f() u8 { return 1; }\ntest \"t\" { assert 1 == 1; }\n"; + assert count_edge_kind(derive_graph(export_graph("specs/x.t27", quiet), quiet), EDGE_TESTED_BY) == 0; +} + +test r2_data_flow_needs_the_name_in_a_return_statement { + const src : []const u8 = "module m;\nuse a::imp;\nconst K : u8 = 1;\nconst L : u8 = 2;\nconst M : u8 = 3;\nfn ret() u8 {\n let x = L;\n return K\n + imp;\n}\nfn late() u8 {\n return 0;\n let y = M;\n}\nfn inline_() u8 { if (true) { return L; } return 0; }\ntest \"t\" {\n return K;\n}\n"; + const e : SpecGraph = export_graph("specs/x.t27", src); + assert validate_graph(e) == GRAPH_OK; + assert e.node_count == 9; + // the exporter's USES edges: ret -> L (7), K (8), imp (9); late -> M (13); inline_ -> L (15); test -> K (17) + assert edge_in(e, EDGE_USES, 5, 3, LABEL_EXACT, 7); + assert edge_in(e, EDGE_USES, 6, 4, LABEL_EXACT, 13); + assert edge_in(e, EDGE_USES, 8, 2, LABEL_EXACT, 17); + const d : SpecGraph = derive_graph(e, src); + assert validate_graph(d) == GRAPH_OK; + // K and the import are operands of ret's return statement, which runs over two lines: the line is the use's + assert edge_in(d, EDGE_DATA_FLOW, 2, 5, LABEL_DERIVED, 8); + assert edge_in(d, EDGE_DATA_FLOW, 1, 5, LABEL_DERIVED, 9); + // a return inside a one-line fn body + assert edge_in(d, EDGE_DATA_FLOW, 3, 7, LABEL_DERIVED, 15); + assert count_edge_kind(d, EDGE_DATA_FLOW) == 3; + // negative controls: L in a `let` (ret), M after the return statement's `;` (late), and K in + // a test, which is not a fn, are used and do not flow + assert has_edge(d, EDGE_DATA_FLOW, 3, 5) == false; + assert has_edge(d, EDGE_DATA_FLOW, 4, 6) == false; + assert has_edge(d, EDGE_DATA_FLOW, 2, 8) == false; + // every flow edge sits on a USES edge of the same endpoints, and goes const/import -> fn + assert has_edge(d, EDGE_USES, 5, 2); + assert has_edge(d, EDGE_USES, 5, 1); + assert has_edge(d, EDGE_USES, 7, 3); + // a call result is not derived: `return f()` makes a CALLS edge and no DATA_FLOW + const call : []const u8 = "module m;\nfn f() u8 { return 1; }\nfn g() u8 { return f(); }\n"; + const c : SpecGraph = derive_graph(export_graph("specs/x.t27", call), call); + assert has_edge(c, EDGE_CALLS, 2, 1); + assert count_edge_kind(c, EDGE_DATA_FLOW) == 0; + // a name in a string or comment inside a return statement is not a use + const lit : []const u8 = "module m;\nconst K : u8 = 1;\nfn f() u8 {\n let x = K;\n return 0; // K\n}\nfn g() u8 { return \"K\"; }\n"; + const l : SpecGraph = derive_graph(export_graph("specs/x.t27", lit), lit); + assert has_edge(l, EDGE_USES, 2, 1); + assert count_edge_kind(l, EDGE_DATA_FLOW) == 0; +} + +test r3_an_undeclared_qualified_call_target_is_an_unknown_opaque_node { + const src : []const u8 = "module m;\nuse a::lib;\ntest \"t1\" {\n try std.testing.expect(true);\n lib.mod.run();\n x.run();\n std.testing.expect(true);\n std.math.sqrt(2);\n}\ntest \"t2\" {\n // std.other.thing(1);\n let s = \"std.str.thing(1)\";\n std.testing.expect(false);\n std.testing.field;\n}\n"; + const e : SpecGraph = export_graph("specs/x.t27", src); + assert validate_graph(e) == GRAPH_OK; + assert e.node_count == 4; + const d : SpecGraph = derive_graph(e, src); + assert validate_graph(d) == GRAPH_OK; + // std.testing is called on lines 4, 7 and 13, std.math once on line 8; one node each + assert d.node_count == 6; + assert count_node_label(d, LABEL_UNKNOWN) == 2; + assert d.node_kind[4] == NODE_OPAQUE and d.node_label[4] == LABEL_UNKNOWN; + assert d.node_name[4] == "std.testing"; + assert d.line_start[4] == 4 and d.line_end[4] == 13; + assert d.node_name[5] == "std.math"; + assert d.line_start[5] == 8 and d.line_end[5] == 8; + // an UNKNOWN node draws alone: no edge reaches it, and the existing edges are untouched + assert d.edge_count == e.edge_count; + assert count_node_kind(d, NODE_OPAQUE) == 2; + // negative controls: lib.mod.run( starts at a name `use a::lib` declares; x.run( has two + // segments; a comment, a string and a path with no `(` name nothing + assert d.node_name[4] != "lib.mod"; + assert count_node_kind(d, NODE_USE) == 1; + // a path whose first segment is declared by a `use` makes no node, and the same call + // without the `use` makes one + const covered : []const u8 = "module m;\nuse a::std;\ntest \"t\" { std.testing.expect(true); }\n"; + assert derive_graph(export_graph("specs/x.t27", covered), covered).node_count == 3; + const bare : []const u8 = "module m;\ntest \"t\" { std.testing.expect(true); }\n"; + assert derive_graph(export_graph("specs/x.t27", bare), bare).node_count == 3; + assert count_node_label(derive_graph(export_graph("specs/x.t27", bare), bare), LABEL_UNKNOWN) == 1; + assert count_node_label(derive_graph(export_graph("specs/x.t27", covered), covered), LABEL_UNKNOWN) == 0; +} + +test derive_changes_no_exact_fact_and_adds_only_derived_or_unknown { + const e : SpecGraph = export_graph("specs/tutorial/08_modules_and_arrays.t27", TUTORIAL_08_SRC); + const d : SpecGraph = derive_graph(e, TUTORIAL_08_SRC); + assert dv_prefix_kept(e, d); + assert count_edge_label(d, LABEL_EXACT) == count_edge_label(e, LABEL_EXACT); + assert count_node_label(d, LABEL_EXACT) == count_node_label(e, LABEL_EXACT); + // everything added is DERIVED (edges) or UNKNOWN (nodes); nothing is SUGGESTED + assert d.edge_count - e.edge_count == count_edge_label(d, LABEL_DERIVED); + assert d.node_count - e.node_count == count_node_label(d, LABEL_UNKNOWN); + assert count_edge_label(d, LABEL_SUGGESTED) == 0; + assert count_node_label(d, LABEL_SUGGESTED) == 0; + // negative controls: the check fails for a moved EXACT edge line, a relabeled EXACT node, + // and a dropped node + var t1 : SpecGraph = d; + t1.edge_line[0] = 99; + assert dv_prefix_kept(e, t1) == false; + var t2 : SpecGraph = d; + t2.node_label[3] = LABEL_DERIVED; + assert dv_prefix_kept(e, t2) == false; + assert dv_prefix_kept(d, e) == false; +} + +test derive_is_idempotent_and_leaves_a_complete_graph_alone { + const e : SpecGraph = export_graph("specs/tutorial/08_modules_and_arrays.t27", TUTORIAL_08_SRC); + const d : SpecGraph = derive_graph(e, TUTORIAL_08_SRC); + const dd : SpecGraph = derive_graph(d, TUTORIAL_08_SRC); + assert dd.node_count == d.node_count and dd.edge_count == d.edge_count; + assert dv_prefix_kept(d, dd); + // the hand-read fixture already holds all of it, so deriving over it adds nothing + const f : SpecGraph = derive_graph(tutorial_08_graph(), TUTORIAL_08_SRC); + assert f.node_count == 15 and f.edge_count == 16; + // and a suggested explanation on top of it is left exactly as it was + const s : SpecGraph = derive_graph(with_suggestion(), TUTORIAL_08_SRC); + assert s.node_count == 16 and s.edge_count == 17; + assert dv_prefix_kept(with_suggestion(), s); + // negative control: without the derive pass the exported graph does differ from d + assert e.edge_count != d.edge_count; +} + +test derive_returns_the_input_when_it_cannot_trust_it { + const e : SpecGraph = export_graph("specs/tutorial/08_modules_and_arrays.t27", TUTORIAL_08_SRC); + // a source of another length is not the source the spans were read from + const wrong : SpecGraph = derive_graph(e, "module m;\n"); + assert wrong.node_count == e.node_count and wrong.edge_count == e.edge_count; + // a graph that does not validate (no path) is returned as it came + var bad : SpecGraph = e; + bad.spec_path = ""; + assert validate_graph(bad) != GRAPH_OK; + assert derive_graph(bad, TUTORIAL_08_SRC).edge_count == e.edge_count; + // negative control: the right source and a valid graph do derive + assert derive_graph(e, TUTORIAL_08_SRC).edge_count == 16; +} + +test past_the_node_capacity_the_verdict_is_too_many_nodes { + // module, 190 consts and one test that calls std.testing.x(): 192 nodes, exactly full + const src : []const u8 = "module m;\nconst k : u8 = 1;\ntest \"t\" { std.testing.x(); }\n"; + var g : SpecGraph = blank_graph(); + g.spec_path = "specs/x.t27"; + g.line_count = 3; + g = with_node(g, NODE_MODULE, LABEL_EXACT, "m", 1, 3); + var a : u32 = 0; + while (a < 190) { + g = with_node(g, NODE_CONST, LABEL_EXACT, "k", 2, 2); + a = a + 1; + } + g = with_node(g, NODE_TEST, LABEL_EXACT, "t", 3, 3); + assert g.node_count == MAX_NODES; + assert validate_graph(g) == GRAPH_OK; + // the derived UNKNOWN node is the 193rd: counted, refused, not dropped silently + const d : SpecGraph = derive_graph(g, src); + assert d.node_count == MAX_NODES + 1; + assert validate_graph(d) == ERR_TOO_MANY_NODES; + assert validate_graph(d) != ERR_TOO_MANY_EDGES; + assert validate_graph(d) != GRAPH_OK; + // negative control: one const fewer leaves room, and the same pass is valid at exactly 192 + var h : SpecGraph = blank_graph(); + h.spec_path = "specs/x.t27"; + h.line_count = 3; + h = with_node(h, NODE_MODULE, LABEL_EXACT, "m", 1, 3); + var b : u32 = 0; + while (b < 189) { + h = with_node(h, NODE_CONST, LABEL_EXACT, "k", 2, 2); + b = b + 1; + } + h = with_node(h, NODE_TEST, LABEL_EXACT, "t", 3, 3); + assert validate_graph(h) == GRAPH_OK; + const ok : SpecGraph = derive_graph(h, src); + assert ok.node_count == MAX_NODES; + assert validate_graph(ok) == GRAPH_OK; + // a graph that is already past capacity is returned as it came, so the verdict is still its own + const over : SpecGraph = derive_graph(d, src); + assert over.node_count == d.node_count; + assert validate_graph(over) == ERR_TOO_MANY_NODES; +} + +test past_the_edge_capacity_the_verdict_is_too_many_edges { + // fn a, fn b and 127 tests that each call both: 254 EXACT CALLS edges, exactly full + const src : []const u8 = "module m;\nfn a() u8 { return 1; }\ntest \"t\" { a(); }\n"; + var g : SpecGraph = blank_graph(); + g.spec_path = "specs/x.t27"; + g.line_count = 3; + g = with_node(g, NODE_MODULE, LABEL_EXACT, "m", 1, 3); + g = with_node(g, NODE_FN, LABEL_EXACT, "a", 2, 2); + g = with_node(g, NODE_FN, LABEL_EXACT, "b", 2, 2); + var t : u32 = 0; + while (t < 127) { + g = with_node(g, NODE_TEST, LABEL_EXACT, "t", 3, 3); + g = with_edge(g, EDGE_CALLS, (3 + t) as u8, 1, LABEL_EXACT, 3); + g = with_edge(g, EDGE_CALLS, (3 + t) as u8, 2, LABEL_EXACT, 3); + t = t + 1; + } + assert g.edge_count == MAX_EDGES; + assert validate_graph(g) == GRAPH_OK; + // R1 would add 254 TESTED_BY edges: counted, refused, not truncated + const d : SpecGraph = derive_graph(g, src); + assert d.edge_count == 2 * MAX_EDGES; + assert validate_graph(d) == ERR_TOO_MANY_EDGES; + assert validate_graph(d) != ERR_TOO_MANY_NODES; + assert validate_graph(d) != GRAPH_OK; + // negative control: 2 fns and 60 tests make 120 CALLS and 120 TESTED_BY = 240, which fits + var h : SpecGraph = blank_graph(); + h.spec_path = "specs/x.t27"; + h.line_count = 3; + h = with_node(h, NODE_MODULE, LABEL_EXACT, "m", 1, 3); + h = with_node(h, NODE_FN, LABEL_EXACT, "a", 2, 2); + h = with_node(h, NODE_FN, LABEL_EXACT, "b", 2, 2); + var u : u32 = 0; + while (u < 60) { + h = with_node(h, NODE_TEST, LABEL_EXACT, "t", 3, 3); + h = with_edge(h, EDGE_CALLS, (3 + u) as u8, 1, LABEL_EXACT, 3); + h = with_edge(h, EDGE_CALLS, (3 + u) as u8, 2, LABEL_EXACT, 3); + u = u + 1; + } + const ok : SpecGraph = derive_graph(h, src); + assert ok.edge_count == 240; + assert validate_graph(ok) == GRAPH_OK; +} + +invariant every_rule_follows_the_edge_kind_masks { + // R1: TESTED_BY goes fn -> test | invariant | bench + assert (EDGE_FROM_KINDS[EDGE_TESTED_BY as usize] & kind_bit(NODE_FN)) != 0; + assert (EDGE_TO_KINDS[EDGE_TESTED_BY as usize] & kind_bit(NODE_TEST)) != 0; + assert (EDGE_TO_KINDS[EDGE_TESTED_BY as usize] & kind_bit(NODE_INVARIANT)) != 0; + assert (EDGE_TO_KINDS[EDGE_TESTED_BY as usize] & kind_bit(NODE_BENCH)) != 0; + // R2: DATA_FLOW goes const | use -> fn + assert (EDGE_FROM_KINDS[EDGE_DATA_FLOW as usize] & kind_bit(NODE_CONST)) != 0; + assert (EDGE_FROM_KINDS[EDGE_DATA_FLOW as usize] & kind_bit(NODE_USE)) != 0; + assert (EDGE_TO_KINDS[EDGE_DATA_FLOW as usize] & kind_bit(NODE_FN)) != 0; + // R3: an opaque node exists as a kind, and no mask lets an UNKNOWN node out of a CALLS edge + assert (EDGE_TO_KINDS[EDGE_CALLS as usize] & kind_bit(NODE_OPAQUE)) == 0; + assert (EDGE_FROM_KINDS[EDGE_CALLS as usize] & kind_bit(NODE_OPAQUE)) == 0; +} + +invariant the_fixture_holds_only_what_the_three_rules_derive { + // an invariant is evaluated at compile time, so it states the cheap part: in the hand-read + // fixture every DERIVED edge is a TESTED_BY or a DATA_FLOW (R1, R2), every UNKNOWN node is + // opaque (R3), and the namespace has the DV_MIN_SEGMENTS the rule needs: std.testing.expectEqual + const f : SpecGraph = tutorial_08_graph(); + assert count_edge_label(f, LABEL_DERIVED) == count_edge_kind(f, EDGE_TESTED_BY) + count_edge_kind(f, EDGE_DATA_FLOW); + assert count_node_label(f, LABEL_UNKNOWN) == count_node_kind(f, NODE_OPAQUE); + assert DV_MIN_SEGMENTS == 3; +} + +test derive_closes_the_gap_between_the_exporter_and_the_fixture { + const e : SpecGraph = export_graph("specs/tutorial/08_modules_and_arrays.t27", TUTORIAL_08_SRC); + const d : SpecGraph = derive_graph(e, TUTORIAL_08_SRC); + const f : SpecGraph = tutorial_08_graph(); + assert validate_graph(d) == GRAPH_OK; + assert nodes_in_common(d, f) == f.node_count; + assert edges_shared(d, f) == f.edge_count; + assert edges_shared(f, d) == d.edge_count; + assert dv_prefix_kept(e, d); +}