From 538e4985d06e287cad65464c25e0be28b9f8b0b3 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 14:37:11 +0700 Subject: [PATCH 1/3] feat(claw): claw/t27f annotations -- one check-run annotation per row that is not sealed, 50 per request (Refs #10268) - specs/claw/t27f_gate.t27: t27f_annotations writes path, line, level, title and message per row that is not sealed, with a --batch line after every 50 (GitHub's per-request limit; github_surface.t27 row check-annotations). notice for neutral rows, failure for failing ones, warning for a failing row in the reporting repository. Unreadable input and annotations that do not fit write nothing; the summary stays the place every finding is shown. - gate-topology.yml claw-t27f: the harness gains mode a; the job posts the first batch with the check-run and PATCHes the rest onto it, with the same three-scope token. - gen/c/claw/t27f_gate.c regenerated; ClawT27fGate seal remade. - Own-language offset: scripts/gen_w381_lean.py deleted; its port specs/port/scripts/gen_w381_lean.t27 landed in #6910 and nothing runs the python. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/gate-topology.yml | 7 +- scripts/gen_w381_lean.py | 140 ---------------------- specs/claw/t27f_gate.t27 | 176 ++++++++++++++++++++++++++++ 3 files changed, 180 insertions(+), 143 deletions(-) delete mode 100644 scripts/gen_w381_lean.py diff --git a/.github/workflows/gate-topology.yml b/.github/workflows/gate-topology.yml index fadfebda09..4bc20ebafb 100644 --- a/.github/workflows/gate-topology.yml +++ b/.github/workflows/gate-topology.yml @@ -98,14 +98,15 @@ jobs: for f in t27c checksums-$V.txt; do curl -fsSLo $f $B/$f; curl -fsSLo $f.sigstore.json $B/$f.sigstore.json cosign verify-blob $f --bundle $f.sigstore.json --certificate-oidc-issuer https://token.actions.githubusercontent.com --certificate-identity-regexp "^https://github.com/gHashTag/t27/.github/workflows/t27o-release.yml@refs/tags/$V$"; done sha256sum -c --ignore-missing checksums-$V.txt; chmod +x t27c; T=/tmp/t27c - printf '#include "%s/gen/c/claw/t27f_gate.c"\n#include \n#include \nint main(int c,char**v){size_t k=1<<24,m;uint8_t*b=malloc(k),*o=malloc(k);size_t n=fread(b,1,k,stdin);if(n==k)return 2;\nif(c>1){m=t27f_scope(b,n,o,k);if(m>k)return 3;}else m=t27f_report(b,n,o,65000);fwrite(o,1,m,stdout);return 0;}\n' "$GITHUB_WORKSPACE" > h.c; cc -O1 -w -o law h.c; L=/tmp/law; set +e + printf '#include "%s/gen/c/claw/t27f_gate.c"\n#include \n#include \nint main(int c,char**v){size_t k=1<<24,m;uint8_t*b=malloc(k),*o=malloc(k);size_t n=fread(b,1,k,stdin);if(n==k)return 2;\nif(c>1&&*v[1]==97)m=t27f_annotations(b,n,o,k);else if(c>1){m=t27f_scope(b,n,o,k);if(m>k)return 3;}else m=t27f_report(b,n,o,65000);fwrite(o,1,m,stdout);return 0;}\n' "$GITHUB_WORKSPACE" > h.c; cc -O1 -w -o law h.c; L=/tmp/law; set +e gh api --paginate /installation/repositories -q '.repositories[].full_name' | while read -r r; do gh pr list -R $r -L 100 --json number,headRefOid,baseRefName,files -q '.[]|select(any(.files[];.path|endswith(".t27")))|"\(.number) \(.headRefOid) \(.baseRefName)"' ../scope || echo --unreadable > ../scope - { printf 'repo\t%s\n' $r; while read -r f; do if [ "$f" = --unreadable ]; then echo $f; else printf '@\t%s\t%s\thttps://raw.githubusercontent.com/%s/%s/%s\n' "$f" "$(sha256sum < "$f" | cut -c1-64)" $r $s "$f"; $T seal "$f" --verify 2>&1 ../out - jq -Rs --arg s $s 'split("\n") as $l | {name: $l[0], head_sha: $s, status: "completed", conclusion: $l[1], output: {title: $l[2], summary: ($l[3:] | join("\n"))}}' ../out | gh api -X POST repos/$r/check-runs --input - > /dev/null ); [ $? = 0 ] || echo "::warning::claw/t27f did not check $r#$n" + { printf 'repo\t%s\n' $r; while read -r f; do if [ "$f" = --unreadable ]; then echo $f; else printf '@\t%s\t%s\thttps://raw.githubusercontent.com/%s/%s/%s\n' "$f" "$(sha256sum < "$f" | cut -c1-64)" $r $s "$f"; $T seal "$f" --verify 2>&1 ../in; $L < ../in > ../out; $L a < ../in > ../ann + jq -Rs --arg s $s --rawfile a ../ann 'split("\n") as $l | [$a | split("--batch\n")[] | [split("\n")[] | select(. != "") | split("\t") | {path: .[0], start_line: (.[1] | tonumber), end_line: (.[1] | tonumber), annotation_level: .[2], title: .[3], message: .[4]}]] as $b | {title: $l[2], summary: ($l[3:] | join("\n"))} as $o | ({name: $l[0], head_sha: $s, status: "completed", conclusion: $l[1], output: ($o + {annotations: ($b[0] // [])})}, ($b[1:][] | {output: ($o + {annotations: .})})) | tojson' ../out > ../bodies + I=$(head -1 ../bodies | gh api -X POST repos/$r/check-runs --input - -q .id); tail -n +2 ../bodies | while read -r j; do printf '%s' "$j" | gh api -X PATCH repos/$r/check-runs/$I --input - > /dev/null; done ); [ $? = 0 ] || echo "::warning::claw/t27f did not check $r#$n" done done diff --git a/scripts/gen_w381_lean.py b/scripts/gen_w381_lean.py deleted file mode 100644 index 38bc355235..0000000000 --- a/scripts/gen_w381_lean.py +++ /dev/null @@ -1,140 +0,0 @@ -#!/usr/bin/env python3 -"""Append Wave Loop 381 generic theorems to Trinity.TernaryInference.lean.""" - -from pathlib import Path - -# The repository root, derived from where this file sits, not from the -# machine it was written on. This was an absolute path into one -# developer's home directory, so it could run for exactly one person -- -# and the secret-scan gate rejects that path, which is how it was found. -# (The old literal is deliberately not quoted here: a comment naming it -# trips the same gate.) -ROOT = Path(__file__).resolve().parent.parent -LEAN_FILE = ROOT / "proofs" / "lean4" / "Trinity" / "TernaryInference.lean" - - -def var_names(n: int) -> list[str]: - skip = {"at", "by", "do", "if", "in", "or", "to"} - names = [] - i = 0 - while len(names) < n: - if i < 26: - candidate = chr(ord("a") + i) - else: - first = chr(ord("a") + (i - 26) // 26) - second = chr(ord("a") + (i - 26) % 26) - candidate = first + second - i += 1 - if candidate in skip: - continue - names.append(candidate) - return names - - -def nest_mac(base: str, activations: list[str], weight: str) -> str: - expr = base - for act in activations: - expr = f"ternaryMac ({expr}) {act} (TernaryWeight.mk .{weight})" - return expr - - -def plus_chain(n: int) -> tuple[str, str]: - names = var_names(n) - lhs = nest_mac("0", names, "plus") - rhs = " + ".join(names) - return lhs, rhs - - -def minus_chain(n: int) -> tuple[str, str]: - names = var_names(n) - lhs = nest_mac("0", names, "minus") - rhs = " + ".join(names) - return lhs, rhs - - -def cancellation_chain(depth: int) -> str: - expr = "x" - for i in range(depth): - w = "plus" if i % 2 == 0 else "minus" - expr = f"ternaryMac ({expr}) a (TernaryWeight.mk .{w})" - return expr - - -def zero_weight_closure(before: int, after: int) -> tuple[str, str]: - total = before + 1 + after - names = var_names(total) - plus_idx = before - - def chain(acts: list[str]) -> str: - expr = "x" - for i, act in enumerate(acts): - w = "plus" if i == plus_idx else "zero" - expr = f"ternaryMac ({expr}) {act} (TernaryWeight.mk .{w})" - return expr - - lhs = chain(names) - reordered = list(names) - reordered[0], reordered[-1] = reordered[-1], reordered[0] - rhs = chain(reordered) - return lhs, rhs - - -def theorem_block(name: str, doc: str, vars: str, lhs: str, rhs: str) -> str: - return f"""/-- {doc} -/ - -theorem {name} ({vars} : Int) : - {lhs} = {rhs} := by - simp [ternaryMac_eq_acc_plus_mul, ternaryMul, ternaryDecode] - <;> try omega -""" - - -def main() -> None: - text = LEAN_FILE.read_text() - if "ternaryMacZeroWeightSixteenPairClosureGeneric" in text: - print("W381 Lean theorems already present.") - return - - blocks: list[str] = [] - - # 59-variable plus accumulation - lhs, rhs = plus_chain(59) - vars = " ".join(var_names(59)) - blocks.append(theorem_block( - "ternaryMacAccumulateFiftyNinePlusGeneric", - "Generic theorem: 59-variable plus accumulation. **265 generic ∀ milestone.**", - vars, lhs, rhs, - )) - - # 58-variable minus accumulation - lhs, rhs = minus_chain(58) - vars = " ".join(var_names(58)) - blocks.append(theorem_block( - "ternaryMacAccumulateFiftyEightMinusGeneric", - "Generic theorem: 58-variable minus accumulation lattice.", - vars, lhs, f"-({rhs})", - )) - - # depth-38 cancellation - lhs = cancellation_chain(38) - blocks.append(theorem_block( - "ternaryMacDuotrigintupleSeptemCancellationGeneric", - "Generic theorem: depth-38 activation cancellation. mac^38(x,a,[.plus,.minus,...]) = x.", - "x a", lhs, "x", - )) - - # zero-weight closure: 16 zero before + plus + 16 zero after - lhs, rhs = zero_weight_closure(16, 16) - vars = " ".join(var_names(33)) - blocks.append(theorem_block( - "ternaryMacZeroWeightSixteenPairClosureGeneric", - "Generic theorem: 16 zero-weight MACs before and after a plus-weight MAC are transparent. **268 generic ∀ milestone.**", - f"x {vars}", lhs, rhs, - )) - - LEAN_FILE.write_text(text + "\n\n" + "\n\n".join(blocks) + "\n") - print("Appended W381 theorems to TernaryInference.lean") - - -if __name__ == "__main__": - main() diff --git a/specs/claw/t27f_gate.t27 b/specs/claw/t27f_gate.t27 index acc0beea76..dfdc058cbb 100644 --- a/specs/claw/t27f_gate.t27 +++ b/specs/claw/t27f_gate.t27 @@ -19,6 +19,11 @@ ; name, the conclusion, the title and the summary table. The job that posts it (claw-t27f in ; .github/workflows/gate-topology.yml) is I/O only: it lists the App's installations, fetches each ; pull request head, runs t27c from the signed t27o release and hands the bytes to this law. +; - What the annotations say: t27f_annotations writes one line per row that is not sealed, cut into +; batches of ANNOTATIONS_PER_PATCH (50), GitHub's limit per check-run request; the job posts the +; first batch with the check-run and PATCHes the rest onto it (specs/claw/github_surface.t27, row +; check-annotations). Every annotation points at line 1 of its spec: the seal says which file is +; off, not which line. ; - A head commit that already carries a claw/t27f check-run is not checked again; the workflow does ; that lookup, the rule is stated here. ; -- @@ -123,6 +128,27 @@ pub const TABLE_HEAD : str = "| path | digest | nodes | edges | verdict | decisi pub const TABLE_RULE : str = "|---|---|---|---|---|---|---|$"; pub const SUMMARY_FOOT : str = "nodes and edges are not measured here: the T27F exporter is t27f.wasm in the viewer, not t27c. The graph link passes the spec's raw URL as src=; the viewer does not read src= yet and opens its own spec list.$"; +/// The annotations: one line per row that is not sealed -- path, line, level, title, message, +/// tab-separated -- with a MARK_BATCH line after every ANNOTATIONS_PER_PATCH of them, because GitHub +/// takes at most 50 annotations in one check-run POST or PATCH (specs/claw/github_surface.t27, row +/// check-annotations). VERDICT_TEXTS is in VERDICT_NAMES order. +pub const ANNOTATIONS_PER_PATCH : u32 = 50; +pub const ANNOTATION_LINE : u32 = 1; +pub const MARK_BATCH : str = "--batch$"; +pub const LEVEL_NOTICE : u8 = 0; +pub const LEVEL_WARNING : u8 = 1; +pub const LEVEL_FAILURE : u8 = 2; +pub const LEVEL_NAMES : [3]str = [ "notice$", "warning$", "failure$" ]; +pub const ANNOTATION_TITLE : str = "T27F seal: $"; +pub const VERDICT_TEXTS : [6]str = [ + "The spec matches its saved seal.$", + "The spec bytes match the saved seal, but its generated code does not: the compiler moved since sealing. Reseal it with t27c seal --save.$", + "This spec has no saved seal under .trinity/seals/. Seal it with t27c seal --save; until then this check cannot show it sealed.$", + "The saved seal was made for other bytes of this spec. Reseal it with t27c seal --save once its tests hold.$", + "The saved seal is vacuous: the spec tests assert nothing that can fail. Add such a test, then reseal.$", + "t27c seal --verify printed nothing this check can read for this spec, or its record line was malformed.$" +]; + /// A consumer repository's role. pub const ROLE_CHECK : u8 = 0; pub const ROLE_REPORT : u8 = 1; @@ -509,6 +535,65 @@ pub fn t27f_report(buf: []const u8, n: usize, out: []u8, cap: usize) -> usize { return p; } +/// The annotation level of a row state in a role: notice for a neutral row, failure for a failing +/// one, and warning for a failing one in a reporting repository, whose check posts it as neutral. +pub fn verdict_level(v: u8, role: u8) -> u8 { + const c : u8 = verdict_conclusion(v); + if (c != CONCL_FAILURE) { return LEVEL_NOTICE; } + if (role == ROLE_REPORT) { return LEVEL_WARNING; } + return LEVEL_FAILURE; +} + +/// Write the annotation line of the record at r whose block ends at b, in role `role`. +pub fn put_annotation(out: []u8, w: usize, cap: usize, buf: []const u8, r: usize, b: usize, role: u8) -> usize { + const e : usize = line_end(buf, r, b); + const x : usize = text_end(buf, r, e); + const p1 : usize = first_tab(buf, r, x); + const p2 : usize = first_tab(buf, p1 + 1, x); + const v : u8 = record_verdict(buf, r, b); + var p : usize = put_range(out, w, cap, buf, p1 + 1, p2); + p = put(out, p, cap, '\t'); + p = put_decimal(out, p, cap, ANNOTATION_LINE); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, LEVEL_NAMES[verdict_level(v, role)]); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, ANNOTATION_TITLE); + p = put_msg(out, p, cap, VERDICT_NAMES[v]); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, VERDICT_TEXTS[v]); + return put(out, p, cap, '\n'); +} + +/// The annotations for the input buf[0..n], written to out[0..cap]: one line per record that is not +/// sealed, a MARK_BATCH line between every ANNOTATIONS_PER_PATCH of them. A record whose path field is +/// empty gets none: an annotation must name a file. An unreadable input, and annotations that do not +/// fit, write nothing -- the check-run's own conclusion already says failure for the first, and an +/// annotation is a pointer to a row of the summary, never the only place a finding is shown. +pub fn t27f_annotations(buf: []const u8, n: usize, out: []u8, cap: usize) -> usize { + if (input_readable(buf, n) == false) { return 0; } + const role : u8 = input_role(buf, n); + var p : usize = 0; + var k : u32 = 0; + var r : usize = next_record(buf, 0, n); + while (r < n) { + const b : usize = next_record(buf, line_end(buf, r, n) + 1, n); + const x : usize = text_end(buf, r, line_end(buf, r, b)); + const p1 : usize = first_tab(buf, r, x); + const p2 : usize = first_tab(buf, p1 + 1, x); + if (record_verdict(buf, r, b) != V_SEALED and p2 > p1 + 1) { + if (k > 0 and k % ANNOTATIONS_PER_PATCH == 0) { + p = put_msg(out, p, cap, MARK_BATCH); + p = put(out, p, cap, '\n'); + } + p = put_annotation(out, p, cap, buf, r, b, role); + k += 1; + } + r = b; + } + if (p > cap) { return 0; } + return p; +} + /// Is buf[f..t] a .t27 path this check can read: not quoted, a name before the extension, and the /// extension SPEC_EXT in any case? pub fn scope_spec(buf: []const u8, f: usize, t: usize) -> bool { @@ -811,6 +896,97 @@ test numbers_and_query_values_are_written_exactly { assert holds(&out, 0, w, "a%20b%26c/d:e%23$") == true; } +test every_row_that_is_not_sealed_gets_one_annotation_line { + var out : [4096]u8 = undefined; + const inp : str = "repo\tgHashTag/tt-trinity-phi\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MATCH\ngen_hash_zig: MATCH\ngen_hash_verilog: MATCH\ngen_hash_c: MATCH\ngen_hash_rust: MATCH\n@\tspecs/b.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: No saved seal found at .trinity/seals/B.json. Run with --save first.\n@\tspecs/c.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MISMATCH (saved=sha256:aa, current=sha256:bb)\n$"; + const w : usize = t27f_annotations(inp, lit_len(inp), &out, 4096); + assert w > 0; + assert holds(&out, 0, w, "specs/b.t27\t1\tnotice\tT27F seal: unsealed\tThis spec has no saved seal under .trinity/seals/.$") == true; + assert holds(&out, 0, w, "specs/c.t27\t1\tfailure\tT27F seal: stale-seal\tThe saved seal was made for other bytes of this spec.$") == true; + assert holds(&out, 0, w, "specs/a.t27$") == false; + assert holds(&out, 0, w, "--batch$") == false; + var lines : u32 = 0; + var i : usize = 0; + while (i < w) { + if (out[i] == '\n') { lines += 1; } + i += 1; + } + assert lines == 2; +} + +test the_published_copy_annotates_a_failure_as_a_warning { + var out : [4096]u8 = undefined; + const stale : str = "repo\tgHashTag/ghashtag.github.io\n@\tt27/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MISMATCH (saved=sha256:aa, current=sha256:bb)\n$"; + const w : usize = t27f_annotations(stale, lit_len(stale), &out, 4096); + assert holds(&out, 0, w, "t27/a.t27\t1\twarning\tT27F seal: stale-seal\t$") == true; + assert verdict_level(V_STALE, ROLE_CHECK) == LEVEL_FAILURE; + assert verdict_level(V_UNREADABLE, ROLE_REPORT) == LEVEL_WARNING; + assert verdict_level(V_TOOLCHAIN, ROLE_REPORT) == LEVEL_NOTICE; +} + +test the_annotations_are_cut_into_batches_of_fifty { + var inp : [16384]u8 = undefined; + var out : [32768]u8 = undefined; + var rows : u32 = 100; + while (rows <= 101) { + var n : usize = put_msg(&inp, 0, 16384, "repo\tgHashTag/trios\n$"); + var j : u32 = 0; + while (j < rows) { + n = put_msg(&inp, n, 16384, "@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: No saved seal found\n$"); + j += 1; + } + assert n < 16384; + const w : usize = t27f_annotations(&inp, n, &out, 32768); + var marks : u32 = 0; + var before : u32 = 0; + var lines : u32 = 0; + var s : usize = 0; + while (s < w) { + const e : usize = line_end(&out, s, w); + if (has_prefix(MARK_BATCH, &out, s, e)) { + if (marks == 0) { before = lines; } + marks += 1; + } else { + lines += 1; + } + s = e + 1; + } + assert lines == rows; + assert before == ANNOTATIONS_PER_PATCH; + if (rows == 100) { assert marks == 1; } + if (rows == 101) { assert marks == 2; } + rows += 1; + } +} + +test negative_control_unreadable_input_or_no_room_writes_no_annotation { + var out : [4096]u8 = undefined; + const marked : str = "repo\tgHashTag/trios\n--unreadable\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert t27f_annotations(marked, lit_len(marked), &out, 4096) == 0; + const inp : str = "repo\tgHashTag/trios\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert t27f_annotations(inp, lit_len(inp), &out, 4096) > 0; + assert t27f_annotations(inp, lit_len(inp), &out, 20) == 0; + const no_path : str = "repo\tgHashTag/trios\n@\t\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert t27f_annotations(no_path, lit_len(no_path), &out, 4096) == 0; + const few_tabs : str = "repo\tgHashTag/trios\n@\tspecs/a.t27\nspec_hash: MATCH\n$"; + const w : usize = t27f_annotations(few_tabs, lit_len(few_tabs), &out, 4096); + assert holds(&out, 0, w, "specs/a.t27\t1\tfailure\tT27F seal: unreadable\t$") == true; +} + +test no_annotation_text_can_break_its_line { + var v : usize = 0; + while (v < 6) { + var k : usize = 0; + while (VERDICT_TEXTS[v][k] != LIST_END) { + assert VERDICT_TEXTS[v][k] != '\t'; + assert VERDICT_TEXTS[v][k] != '\n'; + k += 1; + } + assert k > 20; + v += 1; + } +} + invariant the_conclusions_order_success_neutral_failure { assert CONCL_SUCCESS < CONCL_NEUTRAL; assert CONCL_NEUTRAL < CONCL_FAILURE; From 6ace36058f77c6d2b878ddea9ae661d21fd225e7 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 14:39:22 +0700 Subject: [PATCH 2/3] pins(claw): pin VERDICT_TEXTS, LEVEL_NAMES and MARK_BATCH against .len (Refs #10268) Co-Authored-By: Claude Opus 5.5 --- specs/claw/t27f_gate_pins.t27 | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/specs/claw/t27f_gate_pins.t27 b/specs/claw/t27f_gate_pins.t27 index 710fd83a1f..4b28b75133 100644 --- a/specs/claw/t27f_gate_pins.t27 +++ b/specs/claw/t27f_gate_pins.t27 @@ -46,7 +46,14 @@ test lit_len_agrees_with_len_on_every_table { for i in 0..3 { assert t27f_gate::lit_len(t27f_gate::CONCL_NAMES[i]) + 1 == t27f_gate::CONCL_NAMES[i].len; } + for i in 0..6 { + assert t27f_gate::lit_len(t27f_gate::VERDICT_TEXTS[i]) + 1 == t27f_gate::VERDICT_TEXTS[i].len; + } + for i in 0..3 { + assert t27f_gate::lit_len(t27f_gate::LEVEL_NAMES[i]) + 1 == t27f_gate::LEVEL_NAMES[i].len; + } assert t27f_gate::lit_len(t27f_gate::CHECK_NAME) == 9; + assert t27f_gate::lit_len(t27f_gate::MARK_BATCH) == 7; } test negative_control_a_wrong_label_is_caught { From 96f647e8b06cacef4b438a4cc27efd03ebabe91b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 14:47:44 +0700 Subject: [PATCH 3/3] seals(claw): regenerate gen/c/claw/t27f_gate.c, reseal ClawT27fGate + pins; post compact bodies (Refs #10268) - gen/c/claw/t27f_gate.c regenerated with t27c gen-c on the Railway lab (0 UNRESOLVED), so the spec-guards freshness diff stays empty. - claw_ClawT27fGate.json and claw_ClawT27fGatePins.json resealed after the annotations law and the new pins; all five claw seals verify. - gate-topology.yml: jq -c instead of `| tojson`. tojson printed every body as a quoted JSON string, which gh api --input would have sent as a string, not an object. Each body is now one compact object per line: the POST carries name, head_sha, status, conclusion and the first 50 annotations, every PATCH carries output with the next 50. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/gate-topology.yml | 2 +- .trinity/seals/claw_ClawT27fGate.json | 16 +- .trinity/seals/claw_ClawT27fGatePins.json | 10 +- gen/c/claw/t27f_gate.c | 177 +++++++++++++++++++++- 4 files changed, 190 insertions(+), 15 deletions(-) diff --git a/.github/workflows/gate-topology.yml b/.github/workflows/gate-topology.yml index 4bc20ebafb..eb31d01371 100644 --- a/.github/workflows/gate-topology.yml +++ b/.github/workflows/gate-topology.yml @@ -106,7 +106,7 @@ jobs: git fetch -q origin "pull/$n/head"; git sparse-checkout set --no-cone '*.t27' '/.trinity/seals/'; git checkout -q FETCH_HEAD { git diff --name-only --diff-filter=d "origin/$b...HEAD"; echo --graph; if [ -d specs ]; then $T use-edges --specs-dir specs; fi; } | $L s > ../scope || echo --unreadable > ../scope { printf 'repo\t%s\n' $r; while read -r f; do if [ "$f" = --unreadable ]; then echo $f; else printf '@\t%s\t%s\thttps://raw.githubusercontent.com/%s/%s/%s\n' "$f" "$(sha256sum < "$f" | cut -c1-64)" $r $s "$f"; $T seal "$f" --verify 2>&1 ../in; $L < ../in > ../out; $L a < ../in > ../ann - jq -Rs --arg s $s --rawfile a ../ann 'split("\n") as $l | [$a | split("--batch\n")[] | [split("\n")[] | select(. != "") | split("\t") | {path: .[0], start_line: (.[1] | tonumber), end_line: (.[1] | tonumber), annotation_level: .[2], title: .[3], message: .[4]}]] as $b | {title: $l[2], summary: ($l[3:] | join("\n"))} as $o | ({name: $l[0], head_sha: $s, status: "completed", conclusion: $l[1], output: ($o + {annotations: ($b[0] // [])})}, ($b[1:][] | {output: ($o + {annotations: .})})) | tojson' ../out > ../bodies + jq -cRs --arg s $s --rawfile a ../ann 'split("\n") as $l | [$a | split("--batch\n")[] | [split("\n")[] | select(. != "") | split("\t") | {path: .[0], start_line: (.[1] | tonumber), end_line: (.[1] | tonumber), annotation_level: .[2], title: .[3], message: .[4]}]] as $b | {title: $l[2], summary: ($l[3:] | join("\n"))} as $o | ({name: $l[0], head_sha: $s, status: "completed", conclusion: $l[1], output: ($o + {annotations: ($b[0] // [])})}, ($b[1:][] | {output: ($o + {annotations: .})}))' ../out > ../bodies I=$(head -1 ../bodies | gh api -X POST repos/$r/check-runs --input - -q .id); tail -n +2 ../bodies | while read -r j; do printf '%s' "$j" | gh api -X PATCH repos/$r/check-runs/$I --input - > /dev/null; done ); [ $? = 0 ] || echo "::warning::claw/t27f did not check $r#$n" done done diff --git a/.trinity/seals/claw_ClawT27fGate.json b/.trinity/seals/claw_ClawT27fGate.json index 2c27180ca4..712fbb49ea 100644 --- a/.trinity/seals/claw_ClawT27fGate.json +++ b/.trinity/seals/claw_ClawT27fGate.json @@ -19,23 +19,23 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:75cfffcfd6a4ba47ac96aa1c0ebbc232f9cbb9c85003eb458014abffc2ee8350", - "gen_hash_rust": "sha256:79e0722227eb57bccb498fb165c69f59e0f38b0d93e0bfb5b803263289c56e33", - "gen_hash_verilog": "sha256:1d75c13c148bb32ac17685f94d1dba57ec103911c3c0074bdfd169bc10882a91", - "gen_hash_zig": "sha256:a5fcd394b3d9538a3fc58fc2dad169db8ca0a43d722ee12f65a8a79dc8e2d55d", + "gen_hash_c": "sha256:f04634c3086d38301f1099fd9e14e5a10f61abac58441271c080bc1abcab9c9c", + "gen_hash_rust": "sha256:cdafe83e3bfa9e4fae5d727c58ff3ea74be36bff109ae7f643b32770db78e7e5", + "gen_hash_verilog": "sha256:0eff930fe14e25bf33a511ab0015c3040678d2ff0818000f6a80efdc0527278c", + "gen_hash_zig": "sha256:bdbcb346f994bed18e49299cd96c51abb8ac22a128b8ab02a48079a69b490e46", "module": "ClawT27fGate", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T07:27:09Z", + "sealed_at": "2026-10-18T07:41:52Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:d971531b23c57834d5ffbfd200748db34f51a291f44b87716dcb02910f8e1993", + "spec_hash": "sha256:856be049f9ef3de20cce2f7d18ca3b78a5f4a8ad660dddd8f2cf1aa97bc61ee7", "spec_path": "specs/claw/t27f_gate.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 23, - "total": 23, + "passed": 28, + "total": 28, "vacuous": 0 }, "toolchain": { diff --git a/.trinity/seals/claw_ClawT27fGatePins.json b/.trinity/seals/claw_ClawT27fGatePins.json index 3a40171719..8b84ae2bbe 100644 --- a/.trinity/seals/claw_ClawT27fGatePins.json +++ b/.trinity/seals/claw_ClawT27fGatePins.json @@ -3,7 +3,7 @@ "closure": [ { "spec": "specs/claw/t27f_gate.t27", - "spec_hash": "sha256:d971531b23c57834d5ffbfd200748db34f51a291f44b87716dcb02910f8e1993" + "spec_hash": "sha256:856be049f9ef3de20cce2f7d18ca3b78a5f4a8ad660dddd8f2cf1aa97bc61ee7" }, { "spec": "specs/t27f/hot.t27", @@ -11,16 +11,16 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:e4d2bd19107fff5f42908395ebd42a855bc4821f85014db435196d0a360aff79", + "gen_hash_c": "sha256:e35b884c19d8d6c37ed63beac053d40a5e86f9c73fa2941ff6cd0039c81bda84", "gen_hash_rust": "sha256:4dc02033cea4ae56d81cca417e99faf450bfd97ffcbd7fed702b56b30119ce25", "gen_hash_verilog": "sha256:a5a99dff99da4b4ebd3c15c210a92a3cb487039215158b2bb3c89a83eab168df", - "gen_hash_zig": "sha256:50ca11596eb89c8ffac6476a97349bd9efd9ec5e64ef6ea5ed1bf42793aeb8c9", + "gen_hash_zig": "sha256:e39bb7edf0cb96766984159a1d7c9f3b79f432094cd7c74cd6a9b660a3195efb", "module": "ClawT27fGatePins", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T07:27:10Z", + "sealed_at": "2026-10-18T07:41:53Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:8cc4c19346755daeec7f6ad0e004bbd5b496fdf105eef7c36b4db2bb976c6f34", + "spec_hash": "sha256:1a4fc11a3ee61e990b6226621b4379fe34a727f0d1c830004bfddb5640836666", "spec_path": "specs/claw/t27f_gate_pins.t27", "tests": { "failed": 0, diff --git a/gen/c/claw/t27f_gate.c b/gen/c/claw/t27f_gate.c index 683eb2c86b..feb31d4306 100644 --- a/gen/c/claw/t27f_gate.c +++ b/gen/c/claw/t27f_gate.c @@ -68,6 +68,15 @@ static const const char* DECISION_LABELS[4] = { "reuse$", "rebuild_spec$", "rebu #define TABLE_HEAD "| path | digest | nodes | edges | verdict | decision | graph |$" #define TABLE_RULE "|---|---|---|---|---|---|---|$" #define SUMMARY_FOOT "nodes and edges are not measured here: the T27F exporter is t27f.wasm in the viewer, not t27c. The graph link passes the spec's raw URL as src=; the viewer does not read src= yet and opens its own spec list.$" +#define ANNOTATIONS_PER_PATCH 50 +#define ANNOTATION_LINE 1 +#define MARK_BATCH "--batch$" +#define LEVEL_NOTICE 0 +#define LEVEL_WARNING 1 +#define LEVEL_FAILURE 2 +static const const char* LEVEL_NAMES[3] = { "notice$", "warning$", "failure$" }; +#define ANNOTATION_TITLE "T27F seal: $" +static const const char* VERDICT_TEXTS[6] = { "The spec matches its saved seal.$", "The spec bytes match the saved seal, but its generated code does not: the compiler moved since sealing. Reseal it with t27c seal --save.$", "This spec has no saved seal under .trinity/seals/. Seal it with t27c seal --save; until then this check cannot show it sealed.$", "The saved seal was made for other bytes of this spec. Reseal it with t27c seal --save once its tests hold.$", "The saved seal is vacuous: the spec tests assert nothing that can fail. Add such a test, then reseal.$", "t27c seal --verify printed nothing this check can read for this spec, or its record line was malformed.$" }; #define ROLE_CHECK 0 #define ROLE_REPORT 1 #define CONSUMERS 16 @@ -120,6 +129,9 @@ size_t put_query(uint8_t* out, size_t w, size_t cap, uint8_t* buf, size_t f, siz size_t put_row(uint8_t* out, size_t w, size_t cap, uint8_t* buf, size_t r, size_t b); size_t put_overflow(uint8_t* out, size_t cap); size_t t27f_report(uint8_t* buf, size_t n, uint8_t* out, size_t cap); +uint8_t verdict_level(uint8_t v, uint8_t role); +size_t put_annotation(uint8_t* out, size_t w, size_t cap, uint8_t* buf, size_t r, size_t b, uint8_t role); +size_t t27f_annotations(uint8_t* buf, size_t n, uint8_t* out, size_t cap); bool scope_spec(uint8_t* buf, size_t f, size_t t); size_t t27f_scope(uint8_t* buf, size_t n, uint8_t* set, size_t scap); uint32_t census_specs(void); @@ -567,6 +579,65 @@ size_t t27f_report(uint8_t* buf, size_t n, uint8_t* out, size_t cap) { return p; } +uint8_t verdict_level(uint8_t v, uint8_t role) { + uint8_t c = verdict_conclusion(v); + if ((c != CONCL_FAILURE)) { + return LEVEL_NOTICE; + } + if ((role == ROLE_REPORT)) { + return LEVEL_WARNING; + } + return LEVEL_FAILURE; +} + +size_t put_annotation(uint8_t* out, size_t w, size_t cap, uint8_t* buf, size_t r, size_t b, uint8_t role) { + size_t e = line_end(buf, r, b); + size_t x = text_end(buf, r, e); + size_t p1 = first_tab(buf, r, x); + size_t p2 = first_tab(buf, (p1 + 1), x); + uint8_t v = record_verdict(buf, r, b); + size_t p = put_range(out, w, cap, buf, (p1 + 1), p2); + p = put(out, p, cap, '\t'); + p = put_decimal(out, p, cap, ANNOTATION_LINE); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, LEVEL_NAMES[verdict_level(v, role)]); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, ANNOTATION_TITLE); + p = put_msg(out, p, cap, VERDICT_NAMES[v]); + p = put(out, p, cap, '\t'); + p = put_msg(out, p, cap, VERDICT_TEXTS[v]); + return put(out, p, cap, '\n'); +} + +size_t t27f_annotations(uint8_t* buf, size_t n, uint8_t* out, size_t cap) { + if ((input_readable(buf, n) == false)) { + return 0; + } + uint8_t role = input_role(buf, n); + size_t p = 0; + uint32_t k = 0; + size_t r = next_record(buf, 0, n); + while ((r < n)) { + size_t b = next_record(buf, (line_end(buf, r, n) + 1), n); + size_t x = text_end(buf, r, line_end(buf, r, b)); + size_t p1 = first_tab(buf, r, x); + size_t p2 = first_tab(buf, (p1 + 1), x); + if (((record_verdict(buf, r, b) != V_SEALED) && (p2 > (p1 + 1)))) { + if (((k > 0) && ((k % ANNOTATIONS_PER_PATCH) == 0))) { + p = put_msg(out, p, cap, MARK_BATCH); + p = put(out, p, cap, '\n'); + } + p = put_annotation(out, p, cap, buf, r, b, role); + k += 1; + } + r = b; + } + if ((p > cap)) { + return 0; + } + return p; +} + bool scope_spec(uint8_t* buf, size_t f, size_t t) { size_t k = lit_len(SPEC_EXT); if ((t <= (f + k))) { @@ -1110,6 +1181,105 @@ void test_numbers_and_query_values_are_written_exactly(void) { assert((holds(&out, 0, w, "a%20b%26c/d:e%23$") == true)); } +void test_every_row_that_is_not_sealed_gets_one_annotation_line(void) { + uint8_t out[4096] = {0}; + const char* inp = "repo\tgHashTag/tt-trinity-phi\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MATCH\ngen_hash_zig: MATCH\ngen_hash_verilog: MATCH\ngen_hash_c: MATCH\ngen_hash_rust: MATCH\n@\tspecs/b.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: No saved seal found at .trinity/seals/B.json. Run with --save first.\n@\tspecs/c.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MISMATCH (saved=sha256:aa, current=sha256:bb)\n$"; + size_t w = t27f_annotations(inp, lit_len(inp), &out, 4096); + assert((w > 0)); + assert((holds(&out, 0, w, "specs/b.t27\t1\tnotice\tT27F seal: unsealed\tThis spec has no saved seal under .trinity/seals/.$") == true)); + assert((holds(&out, 0, w, "specs/c.t27\t1\tfailure\tT27F seal: stale-seal\tThe saved seal was made for other bytes of this spec.$") == true)); + assert((holds(&out, 0, w, "specs/a.t27$") == false)); + assert((holds(&out, 0, w, "--batch$") == false)); + uint32_t lines = 0; + size_t i = 0; + while ((i < w)) { + if ((out[i] == '\n')) { + lines += 1; + } + i += 1; + } + assert((lines == 2)); +} + +void test_the_published_copy_annotates_a_failure_as_a_warning(void) { + uint8_t out[4096] = {0}; + const char* stale = "repo\tgHashTag/ghashtag.github.io\n@\tt27/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nspec_hash: MISMATCH (saved=sha256:aa, current=sha256:bb)\n$"; + size_t w = t27f_annotations(stale, lit_len(stale), &out, 4096); + assert((holds(&out, 0, w, "t27/a.t27\t1\twarning\tT27F seal: stale-seal\t$") == true)); + assert((verdict_level(V_STALE, ROLE_CHECK) == LEVEL_FAILURE)); + assert((verdict_level(V_UNREADABLE, ROLE_REPORT) == LEVEL_WARNING)); + assert((verdict_level(V_TOOLCHAIN, ROLE_REPORT) == LEVEL_NOTICE)); +} + +void test_the_annotations_are_cut_into_batches_of_fifty(void) { + uint8_t inp[16384] = {0}; + uint8_t out[32768] = {0}; + uint32_t rows = 100; + while ((rows <= 101)) { + size_t n = put_msg(&inp, 0, 16384, "repo\tgHashTag/trios\n$"); + uint32_t j = 0; + while ((j < rows)) { + n = put_msg(&inp, n, 16384, "@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: No saved seal found\n$"); + j += 1; + } + assert((n < 16384)); + size_t w = t27f_annotations(&inp, n, &out, 32768); + uint32_t marks = 0; + uint32_t before = 0; + uint32_t lines = 0; + size_t s = 0; + while ((s < w)) { + size_t e = line_end(&out, s, w); + if (has_prefix(MARK_BATCH, &out, s, e)) { + if ((marks == 0)) { + before = lines; + } + marks += 1; + } else { + lines += 1; + } + s = (e + 1); + } + assert((lines == rows)); + assert((before == ANNOTATIONS_PER_PATCH)); + if ((rows == 100)) { + assert((marks == 1)); + } + if ((rows == 101)) { + assert((marks == 2)); + } + rows += 1; + } +} + +void test_negative_control_unreadable_input_or_no_room_writes_no_annotation(void) { + uint8_t out[4096] = {0}; + const char* marked = "repo\tgHashTag/trios\n--unreadable\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert((t27f_annotations(marked, lit_len(marked), &out, 4096) == 0)); + const char* inp = "repo\tgHashTag/trios\n@\tspecs/a.t27\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert((t27f_annotations(inp, lit_len(inp), &out, 4096) > 0)); + assert((t27f_annotations(inp, lit_len(inp), &out, 20) == 0)); + const char* no_path = "repo\tgHashTag/trios\n@\t\t0123456789abcdef0123456789abcdef0123456789abcdef0123456789abcdef\turl\nError: parse error\n$"; + assert((t27f_annotations(no_path, lit_len(no_path), &out, 4096) == 0)); + const char* few_tabs = "repo\tgHashTag/trios\n@\tspecs/a.t27\nspec_hash: MATCH\n$"; + size_t w = t27f_annotations(few_tabs, lit_len(few_tabs), &out, 4096); + assert((holds(&out, 0, w, "specs/a.t27\t1\tfailure\tT27F seal: unreadable\t$") == true)); +} + +void test_no_annotation_text_can_break_its_line(void) { + size_t v = 0; + while ((v < 6)) { + size_t k = 0; + while ((VERDICT_TEXTS[v][k] != LIST_END)) { + assert((VERDICT_TEXTS[v][k] != '\t')); + assert((VERDICT_TEXTS[v][k] != '\n')); + k += 1; + } + assert((k > 20)); + v += 1; + } +} + /* ------------------------------------------------------- Test runner (compile with -DT27_TEST_MAIN to execute) @@ -1141,7 +1311,12 @@ int main(void) { test_negative_control_an_import_does_not_put_what_it_imports_in_scope(); test_negative_control_a_scope_without_its_marker_or_room_fails_closed(); test_numbers_and_query_values_are_written_exactly(); - printf("All %d tests passed.\n", 23); + test_every_row_that_is_not_sealed_gets_one_annotation_line(); + test_the_published_copy_annotates_a_failure_as_a_warning(); + test_the_annotations_are_cut_into_batches_of_fifty(); + test_negative_control_unreadable_input_or_no_room_writes_no_annotation(); + test_no_annotation_text_can_break_its_line(); + printf("All %d tests passed.\n", 28); return 0; } #endif /* T27_TEST_MAIN */