From 0a3c197ca07861f3d8447514b3298b0f0aa1e58a Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 5 Oct 2026 04:49:37 +0700 Subject: [PATCH 1/2] fix(conformance): stop reading header comments as receipt-key instantiations key_default_check.py matched module names in raw source. The header of formal/tern_tc_layer_rtl_tb.v names fpga/portable/trinet_node_core.v twice, and the check read both as instantiations without a key, so receipt-keys has been red on every scheduled run on main since 2026-09-28. The real instantiation, line 42, passes .RECEIPT_KEY(128'h0). Blank comments and string literals before matching, keeping newlines so line numbers still point into the file. This also closes the reverse hole: a key written only in a comment inside #( ... ) was accepted as passed. Mutants, run on a copy of main's tree in-process: mutant old checker new checker clean tree (must pass) rc 1, 2 RULE rc 0 tern_tc bench drops its key 3 RULE 1 RULE, :42 tern_tc key only in a comment 2 RULE, not 1 RULE, :42 at :42 v2 bench drops its key (workflow mutant) 3 RULE 1 RULE non-null default (workflow mutant) 3 RULE 1 RULE 1 non-null default only in a comment (pass) rc 1 rc 0 module name in a $display string (pass) rc 1 rc 0 Add a guard step for the comment case. It looks up the bench's instantiation line instead of hard-coding 42, and requires exactly one RULE 2 there. Closes #877 Co-Authored-By: Claude Opus 5.5 --- .github/workflows/trinet-portability.yml | 32 ++++++++++++++++++++++++ conformance/key_default_check.py | 17 +++++++++++-- 2 files changed, 47 insertions(+), 2 deletions(-) diff --git a/.github/workflows/trinet-portability.yml b/.github/workflows/trinet-portability.yml index 3a9be357c1..61e09f3c30 100644 --- a/.github/workflows/trinet-portability.yml +++ b/.github/workflows/trinet-portability.yml @@ -75,6 +75,38 @@ jobs: echo "::error::the guard failed, but not on rule 2"; cat /tmp/r2.log; exit 1; } cp /tmp/tb.bak formal/trinet_node_v2_tb.v + # The guard blanks comments before matching, because tern_tc_layer_rtl_tb.v + # names the core in its header and was read as two keyless instantiations. + # The other side of that must hold too: a key written only in a comment is + # not a key passed, and the failure must point at the real instantiation. + - name: The guard must reject a key that is only in a comment + run: | + tb=formal/tern_tc_layer_rtl_tb.v + cp "$tb" /tmp/tc.bak + inst_line=$(grep -n 'trinet_node_core #(' "$tb" | cut -d: -f1 || true) + one_inst=false; [ "$(printf '%s\n' "$inst_line" | grep -c '^[0-9][0-9]*$')" = 1 ] && one_inst=true + if [ "$one_inst" = false ]; then + echo "::error::want exactly one 'trinet_node_core #(' in $tb, got line(s): $inst_line"; exit 1 + fi + sed -i "s|\.RECEIPT_KEY(128'h0)|/* .RECEIPT_KEY(128'h0) */|" "$tb" + mutated=false; grep -q "/\* \.RECEIPT_KEY(128'h0) \*/" "$tb" && mutated=true + accepted=false; python3 conformance/key_default_check.py > /tmp/r3.log 2>&1 && accepted=true + cp /tmp/tc.bak "$tb" + if [ "$mutated" = false ]; then + echo "::error::the mutation did not apply; the bench no longer passes .RECEIPT_KEY(128'h0)"; exit 1 + fi + if [ "$accepted" = true ]; then + echo "::error::the key guard accepted a key written only in a comment" + cat /tmp/r3.log; exit 1 + fi + rules=$(grep -c '^ RULE' /tmp/r3.log || true) + at_inst=false; grep -q "RULE 2 $tb:$inst_line:" /tmp/r3.log && at_inst=true + placed=false; [ "$at_inst" = true ] && [ "$rules" = 1 ] && placed=true + if [ "$placed" = false ]; then + echo "::error::want exactly one RULE 2 at $tb:$inst_line, got $rules rule line(s)" + cat /tmp/r3.log; exit 1 + fi + equivalence: # The AX7203 wrapper must still behave exactly like the node it wraps. runs-on: ubuntu-latest diff --git a/conformance/key_default_check.py b/conformance/key_default_check.py index 6ac86426e8..c961219522 100644 --- a/conformance/key_default_check.py +++ b/conformance/key_default_check.py @@ -35,6 +35,19 @@ DEFAULT_RE = re.compile( r"parameter\s*(?:\[[^\]]*\]\s*)?RECEIPT_KEY\s*=\s*([^,;)\n]+)", re.I) +# A comment that names a module is not an instantiation of it, and a RECEIPT_KEY +# written in a comment is not a key passed. formal/tern_tc_layer_rtl_tb.v names +# fpga/portable/trinet_node_core.v twice in its header, and this check read both +# as instantiations without a key: red on every scheduled run on main from +# 2026-09-28. Comments and string literals are blanked before matching, newlines +# kept, so line numbers still point into the file. +CODE_ONLY_RE = re.compile(r'//[^\n]*|/\*.*?\*/|"(?:\\.|[^"\\\n])*"', re.S) + + +def code_only(src: str) -> str: + """src with every comment and string literal blanked, newlines kept.""" + return CODE_ONLY_RE.sub(lambda m: re.sub(r"[^\n]", " ", m.group(0)), src) + def is_null_literal(text: str) -> bool: """True for 128'h0, 128'd0, 0, 128'h0000_0000_..., and nothing else.""" @@ -48,7 +61,7 @@ def is_null_literal(text: str) -> bool: def modules_with_key(path: pathlib.Path): """Yield (module_name, default_text) for modules declaring RECEIPT_KEY.""" - src = path.read_text(errors="replace") + src = code_only(path.read_text(errors="replace")) for mm in re.finditer(r"\bmodule\s+(\w+)", src): name = mm.group(1) end = src.find("endmodule", mm.end()) @@ -59,7 +72,7 @@ def modules_with_key(path: pathlib.Path): def instantiations(path: pathlib.Path, known: set): """Yield (module, passes_key, line) for instantiations of known modules.""" - src = path.read_text(errors="replace") + src = code_only(path.read_text(errors="replace")) for name in known: # name #( ... ) inst ( ... ) or name inst ( ... ) for m in re.finditer(r"\b" + re.escape(name) + r"\s*(#\s*\()?", src): From b40cbbf4ed85a4bdb7fbeae16671b4afcc1acf8b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Mon, 5 Oct 2026 05:06:12 +0700 Subject: [PATCH 2/2] ci(trinet): watch the bench the comment-key guard mutates The new guard step reads and mutates formal/tern_tc_layer_rtl_tb.v, but the workflow's paths: lists did not name it, so the Workflow path gate (research/audit_workflow_paths.py) failed this PR with "BUILT BUT NOT WATCHED". Add it to both the push and pull_request lists. The comment sits on its own line: the gate's paths parser keeps a trailing "# ..." as part of the entry and then reports it as a dead path. Part of #877. Co-Authored-By: Claude Opus 5.5 --- .github/workflows/trinet-portability.yml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.github/workflows/trinet-portability.yml b/.github/workflows/trinet-portability.yml index 61e09f3c30..bad0dc6bba 100644 --- a/.github/workflows/trinet-portability.yml +++ b/.github/workflows/trinet-portability.yml @@ -19,6 +19,8 @@ on: - 'fpga/vivado/trinet_node_v2_ax7203.v' - 'fpga/openxc7-synth/trinet_siphash24.v' - 'formal/trinet_node_v2_tb.v' + # the comment-key guard mutates this bench (#877) + - 'formal/tern_tc_layer_rtl_tb.v' - 'conformance/key_default_check.py' - '.github/workflows/trinet-portability.yml' # the scripts this job runs: fixing a check must re-run it @@ -29,6 +31,7 @@ on: - 'fpga/vivado/trinet_node_v2_ax7203.v' - 'fpga/openxc7-synth/trinet_siphash24.v' - 'formal/trinet_node_v2_tb.v' + - 'formal/tern_tc_layer_rtl_tb.v' - 'conformance/key_default_check.py' schedule: - cron: '41 5 * * *'