diff --git a/.github/workflows/trinet-portability.yml b/.github/workflows/trinet-portability.yml index 3a9be357c..bad0dc6bb 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 * * *' @@ -75,6 +78,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 6ac86426e..c96121952 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):