spec(t27f): spec_graph_outline -- the outline wording and decisions in t27 (Closes #10200)

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;
+}