From d1d8d74fab9c1f5d2c86af4f5c7294551ae0458a Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 11:09:32 +0700 Subject: [PATCH] spec(t27f): spec_graph_outline -- the outline wording and decisions in t27 (Closes #10200) The templates for the outline and refusal lines, shows_in_outline, span_is_range, refusal_index and the exact tested_by view of calls edges, with eight tests (mark counts of every template, a negative control). Co-Authored-By: Claude Sonnet 5.5 --- specs/t27f/spec_graph_outline.t27 | 212 ++++++++++++++++++++++++++++++ 1 file changed, 212 insertions(+) create mode 100644 specs/t27f/spec_graph_outline.t27 diff --git a/specs/t27f/spec_graph_outline.t27 b/specs/t27f/spec_graph_outline.t27 new file mode 100644 index 0000000000..7ef23ceceb --- /dev/null +++ b/specs/t27f/spec_graph_outline.t27 @@ -0,0 +1,212 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/t27f/spec_graph_outline.t27 -- the T27F outline: a spec graph as compact text, the decisions and the words +; (gHashTag/t27-mcp tool t27f_outline; epic gHashTag/trinity#1648, RFC gHashTag/trinity#1649; epic #10066). +; -- +; t27f_outline reads a .t27 spec through its graph (spec_graph_export.t27) instead of the whole file. The host +; used to decide what to print and in which words, and that was JavaScript. This spec holds all of it, as +; spec_brief.t27 does for the brief row: the line templates, the refusal wording, and the three decisions the +; text depends on. The host only writes the spec's bytes in, reads the graph out and fills the `{}` marks of a +; template with the numbers and names it reads, in order. It decides nothing. +; Decisions held here, each with a test below: +; - exact only: shows_in_outline(label) is true for EXACT alone, so a derived, suggested or unknown fact is +; never printed as if it were read from the source (the exporter emits exact facts only; this is the guard +; for a graph that came from somewhere else); +; - a line span prints as one line when its two ends agree and as a-b when they do not (span_is_range); +; - refusal_index(verdict) picks the template of a refused graph; a graph over the cap is refused as such and +; never printed in part; +; - tested_by_count / tested_by_of: for a fn, the tests, invariants and benches that call it through an EXACT +; calls edge, in edge order. This is the tested_by view of those edges, read backwards; the host prints it +; under the heading OUTLINE_TEXT[3], which says it is derived. It reads calls edges only, so it holds for the +; exporter's graph, which has no tested_by edges of its own. +; Not claimed: t27 has no string building, so a template is filled by the host, and nothing here proves the host +; fills it in the right order. The order of the marks is part of each template's comment below. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module t27f_spec_graph_outline; + +use t27f::spec_graph::SpecGraph; +use t27f::spec_graph::tutorial_08_graph; +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::EDGE_CALLS; +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::ERR_TOO_MANY_NODES; +use t27f::spec_graph::ERR_TOO_MANY_EDGES; +use t27f::spec_graph::GRAPH_OK; +use t27f::spec_graph::ERR_MODULE; +use t27f::spec_graph::NO_INDEX; + +/// One template per part of an outline. `{}` marks what the host fills, left to right: +/// 0 header : spec path, line count, node count, edge count, MAX_NODES, MAX_EDGES +/// 1 nodes : (heading, no marks) +/// 2 edges : (heading, no marks) +/// 3 derived : (heading, no marks) +/// 4 node : index, node kind, node name, span (see span_is_range), label +/// 5 edge : edge kind, from index, from name, to index, to name, line +/// 6 tested : fn name, the test names joined with "; " +/// 7 untested: fn name +/// The span of a node (4) is the text of its first line, plus "-" and the last line when span_is_range. +pub const OUTLINE_TEXT : [8]str = [ + "{}: {} lines, {} nodes, {} edges (cap {} nodes / {} edges); exact only, no derived edges", + "nodes (kind name lines a-b label):", + "edges (kind from -> to, line of first use):", + "derived (the tested_by view of the exact calls edges from a test to a fn):", + " {} {} {} lines {} {}", + " {} {} {} -> {} {} line {}", + " fn {} is tested by: {}", + " fn {} is called by no test" +]; + +/// One template per refusal, chosen by refusal_index. `{}` marks, left to right: +/// 0 too many nodes : spec path, node count found, MAX_NODES +/// 1 too many edges : spec path, edge count found, MAX_EDGES +/// 2 any other verdict : spec path, the verdict's name, the verdict's code +pub const REFUSAL_TEXT : [3]str = [ + "{}: refused, too many nodes: {} nodes found, the graph holds at most {}. No graph is drawn or truncated.", + "{}: refused, too many edges: {} edges found, the graph holds at most {}. No graph is drawn or truncated.", + "{}: refused, {} (verdict {})." +]; + +pub const REFUSE_NODES : u32 = 0; +pub const REFUSE_EDGES : u32 = 1; +pub const REFUSE_OTHER : u32 = 2; + +/// Which refusal template a verdict takes. GRAPH_OK is not a refusal; it answers REFUSE_OTHER, which a host +/// never asks for, and the test below pins that. +pub fn refusal_index(verdict: u8) -> u32 { + if (verdict == ERR_TOO_MANY_NODES) { return REFUSE_NODES; } + if (verdict == ERR_TOO_MANY_EDGES) { return REFUSE_EDGES; } + return REFUSE_OTHER; +} + +/// A fact is printed in the outline's node and edge lists only when it is EXACT. +pub fn shows_in_outline(label: u8) -> bool { + return label == LABEL_EXACT; +} + +/// A span prints as "a-b" when its ends differ, as "a" when they agree. +pub fn span_is_range(a: u32, b: u32) -> bool { + return b > a; +} + +fn is_testing_kind(k: u8) -> bool { + return k == NODE_TEST or k == NODE_INVARIANT or k == NODE_BENCH; +} + +/// How many tests, invariants and benches call node f through an EXACT calls edge. Zero for a node that is +/// not a fn. +pub fn tested_by_count(g: SpecGraph, f: u32) -> u32 { + if (f >= g.node_count) { return 0; } + if (g.node_kind[f as usize] != NODE_FN) { return 0; } + var c : u32 = 0; + var j : u32 = 0; + while (j < g.edge_count) { + let m : usize = j as usize; + if (g.edge_kind[m] == EDGE_CALLS and g.edge_label[m] == LABEL_EXACT and (g.edge_to[m] as u32) == f and is_testing_kind(g.node_kind[g.edge_from[m] as usize])) { + c = c + 1; + } + j = j + 1; + } + return c; +} + +/// The node index of the n-th (from 0, in edge order) test that calls fn f, or NO_INDEX when there is none. +pub fn tested_by_of(g: SpecGraph, f: u32, n: u32) -> u32 { + if (f >= g.node_count) { return NO_INDEX; } + if (g.node_kind[f as usize] != NODE_FN) { return NO_INDEX; } + var seen : u32 = 0; + var j : u32 = 0; + while (j < g.edge_count) { + let m : usize = j as usize; + if (g.edge_kind[m] == EDGE_CALLS and g.edge_label[m] == LABEL_EXACT and (g.edge_to[m] as u32) == f and is_testing_kind(g.node_kind[g.edge_from[m] as usize])) { + if (seen == n) { return g.edge_from[m] as u32; } + seen = seen + 1; + } + j = j + 1; + } + return NO_INDEX; +} + +/// How many `{}` marks a template holds: the number of values the host has to fill into it. +pub fn mark_count(t: str) -> u32 { + var c : u32 = 0; + var k : usize = 0; + while (k + 1 < t.len) { + if (t[k] == '{' and t[k + 1] == '}') { c = c + 1; k = k + 2; } else { k = k + 1; } + } + return c; +} + +test shows_in_outline_only_an_exact_fact_is_printed { + assert shows_in_outline(LABEL_EXACT); + assert shows_in_outline(LABEL_DERIVED) == false; + assert shows_in_outline(LABEL_SUGGESTED) == false; + assert shows_in_outline(LABEL_UNKNOWN) == false; +} + +test span_is_range_one_line_alone_two_lines_a_range { + assert span_is_range(22, 22) == false; + assert span_is_range(37, 39); + assert span_is_range(5, 4) == false; +} + +test refusal_index_over_the_cap_is_named { + assert refusal_index(ERR_TOO_MANY_NODES) == REFUSE_NODES; + assert refusal_index(ERR_TOO_MANY_EDGES) == REFUSE_EDGES; + assert refusal_index(9) == REFUSE_OTHER; + assert refusal_index(GRAPH_OK) == REFUSE_OTHER; +} + +test refusal_indices_are_distinct { + assert refusal_index(ERR_TOO_MANY_NODES) != refusal_index(ERR_TOO_MANY_EDGES); + assert refusal_index(ERR_TOO_MANY_EDGES) != refusal_index(ERR_MODULE); + assert refusal_index(ERR_TOO_MANY_NODES) != refusal_index(ERR_MODULE); +} + +test templates_carry_the_marks_their_comments_name { + // the number of `{}` marks the host fills, per template (see the comments above each table) + assert mark_count(OUTLINE_TEXT[0]) == 6; + assert mark_count(OUTLINE_TEXT[1]) == 0; + assert mark_count(OUTLINE_TEXT[2]) == 0; + assert mark_count(OUTLINE_TEXT[3]) == 0; + assert mark_count(OUTLINE_TEXT[4]) == 5; + assert mark_count(OUTLINE_TEXT[5]) == 6; + assert mark_count(OUTLINE_TEXT[6]) == 2; + assert mark_count(OUTLINE_TEXT[7]) == 1; + assert mark_count(REFUSAL_TEXT[0]) == 3; + assert mark_count(REFUSAL_TEXT[1]) == 3; + assert mark_count(REFUSAL_TEXT[2]) == 3; +} + + +test tested_by_on_tutorial_08_each_fn_has_its_one_test { + let g : SpecGraph = tutorial_08_graph(); + // fns: 4 scaled_width, 8 power_of_two, 9 bias_for_width; their callers are tests 12, 10 and 11. + assert tested_by_count(g, 4) == 1; + assert tested_by_count(g, 8) == 1; + assert tested_by_count(g, 9) == 1; + assert tested_by_of(g, 4, 0) == 12; + assert tested_by_of(g, 8, 0) == 10; + assert tested_by_of(g, 9, 0) == 11; +} + +test tested_by_a_second_index_and_a_non_fn_answer_no_test { + let g : SpecGraph = tutorial_08_graph(); + assert tested_by_of(g, 4, 1) == NO_INDEX; + assert tested_by_count(g, 2) == 0; + assert tested_by_of(g, 2, 0) == NO_INDEX; + assert tested_by_count(g, 99) == 0; +} + +test negative_control_a_node_that_is_not_a_fn_has_no_tests { + let g : SpecGraph = tutorial_08_graph(); + // node 13 is the invariant: it constrains a const and calls no fn, and a test is not a fn either + assert tested_by_count(g, 13) == 0; + assert tested_by_count(g, 10) == 0; + assert tested_by_of(g, 13, 0) == NO_INDEX; +}