spec: legalize Verilog-reserved identifiers + fix a stale tri_a2a test; icarus KAT runs all 30 lowerable specs

.github/workflows/gft-verilog-kat.yml

@@ -7,11 +7,33 @@ on:
       - "specs/tri_gft_add.t27"
       - "specs/tri_gft_sub.t27"
       - "specs/tri_gft_ladder.t27"
+      - "specs/tri_gft_arith.t27"
+      - "specs/tri_a2a.t27"
+      - "specs/tri_a2a_card.t27"
+      - "specs/tri_a2a_wire.t27"
+      - "specs/tri_challenge.t27"
+      - "specs/tri_compute_account.t27"
+      - "specs/tri_compute_bitnet.t27"
+      - "specs/tri_compute_bond.t27"
+      - "specs/tri_compute_challenge.t27"
       - "specs/tri_compute_gfvalid.t27"
       - "specs/tri_compute_optimistic.t27"
+      - "specs/tri_compute_payout.t27"
+      - "specs/tri_compute_pool.t27"
+      - "specs/tri_compute_receipt.t27"
+      - "specs/tri_compute_reputation.t27"
       - "specs/tri_compute_safety.t27"
+      - "specs/tri_compute_settle.t27"
+      - "specs/tri_depin.t27"
+      - "specs/tri_fec.t27"
+      - "specs/tri_ilv.t27"
+      - "specs/tri_ledger.t27"
+      - "specs/tri_merkle.t27"
       - "specs/tri_node_identity.t27"
       - "specs/tri_receipt_verify.t27"
+      - "specs/tri_settle.t27"
+      - "specs/tri_sha256.t27"
+      - "specs/tri_slash.t27"
       - ".github/workflows/gft-verilog-kat.yml"
 
 # Execute the GF-T specs' own test blocks IN SIMULATED HARDWARE: t27c
@@ -22,17 +44,12 @@ on:
 # too, so a codegen or spec regression on the hardware side cannot land
 # silently. Requires t27c >= gHashTag/t27#1885 (assert lowering).
 #
-# Sweep result (2026-08-08, t27c @ 8f4319364): 26 of 28 ring specs are
-# icarus-lowerable (crypto_frame and discovery are not). Excluded from the run:
-#   tri_gft_arith -- GF-T32 u64-helper tests fail on the gen-verilog u64
-#     width-truncation bug (gHashTag/t27#1886)
-#   tri_a2a, tri_a2a_card, tri_a2a_wire, tri_challenge, tri_compute_account,
-#   tri_compute_bitnet, tri_compute_bond, tri_compute_challenge,
-#   tri_compute_payout, tri_compute_pool, tri_compute_receipt,
-#   tri_compute_reputation, tri_compute_settle, tri_depin, tri_fec, tri_ilv,
-#   tri_ledger, tri_merkle, tri_settle, tri_sha256, tri_slash -- testbench
-#     emits named test-block locals without reg declarations
-#     (gHashTag/t27#1894); add them back as upstream fixes land.
+# Sweep result (2026-08-08, t27c with #1885+#1899): every icarus-lowerable ring
+# spec (30 of 32; crypto_frame and discovery are not lowerable) simulates clean
+# and runs here. Unlocked by upstream t27#1885 (assert lowering), t27#1894
+# (test-block reg declarations), t27#1886 (64-bit __mul_noop) and tri-net-side
+# spec legalization (Verilog reserved words class/packed/small renamed; one
+# stale tri_a2a hosted-skill test corrected -- caught by the simulation).
 
 jobs:
   icarus-kat:
@@ -66,7 +83,7 @@ jobs:
         run: |
           T27C=../t27/target/release/t27c
           STATUS=0
-          for spec in tri_gft_add tri_gft_sub tri_gft_ladder tri_compute_gfvalid tri_compute_optimistic tri_compute_safety tri_node_identity tri_receipt_verify; do
+          for spec in tri_gft_add tri_gft_sub tri_gft_ladder tri_gft_arith tri_a2a tri_a2a_card tri_a2a_wire tri_challenge tri_compute_account tri_compute_bitnet tri_compute_bond tri_compute_challenge tri_compute_gfvalid tri_compute_optimistic tri_compute_payout tri_compute_pool tri_compute_receipt tri_compute_reputation tri_compute_safety tri_compute_settle tri_depin tri_fec tri_ilv tri_ledger tri_merkle tri_node_identity tri_receipt_verify tri_settle tri_sha256 tri_slash; do
             echo "== ${spec}"
             if ! $T27C icarus-simulate specs/${spec}.t27; then
               echo "::error file=specs/${spec}.t27::icarus-simulate failed for specs/${spec}.t27"

specs/tri_a2a.t27

@@ -628,7 +628,7 @@ module TriA2A {
         assert(is_hosted_skill(SKILL_GF16_MUL) == 1, "GF16 mul is hosted");
         assert(is_hosted_skill(SKILL_GFT8_ADD) == 1, "GF-T8 add is hosted");
         assert(is_hosted_skill(0xA412) == 0, "a GF-T4-looking id (0xA412) is NOT hosted");
-        assert(is_hosted_skill(0xA511) == 0, "a GF-T32-looking id is NOT hosted");
+        assert(is_hosted_skill(0xA512) == 0, "a GF-T32-looking id with an unknown op is NOT hosted");
         assert(is_hosted_skill(0xDEAD) == 0, "garbage skill is NOT hosted");
     }
 

specs/tri_a2a_wire.t27

@@ -4,7 +4,7 @@
 // demuxed by port, per tri_a2a). Fixed-length header (no variable-length parsing,
 // so no length-confusion / injection surface, unlike JSON-RPC A2A):
 //
-//   [ class(1) | task_id(4, big-endian) | skill(2, big-endian) | body... ]
+//   [ msg_class(1) | task_id(4, big-endian) | skill(2, big-endian) | body... ]
 //
 // taskAssign body = GF operands; taskResult body = the compute receipt.
 
@@ -37,16 +37,16 @@ module TriA2AWire {
         return OFF_BODY;
     }
 
-    // A message is well-formed iff its class is one of the known classes.
-    fn class_valid(class: u32) -> bool {
-        if (class == MSG_TASK_ASSIGN) { return class == class; }
-        else { if (class == MSG_TASK_RESULT) { return class == class; }
-        else { return class == MSG_HEARTBEAT; } }
+    // A message is well-formed iff its msg_class is one of the known classes.
+    fn class_valid(msg_class: u32) -> bool {
+        if (msg_class == MSG_TASK_ASSIGN) { return msg_class == msg_class; }
+        else { if (msg_class == MSG_TASK_RESULT) { return msg_class == msg_class; }
+        else { return msg_class == MSG_HEARTBEAT; } }
     }
 
     // Only a taskResult carries a receipt in its body (matches tri_a2a.carries_receipt).
-    fn body_has_receipt(class: u32) -> bool {
-        return class == MSG_TASK_RESULT;
+    fn body_has_receipt(msg_class: u32) -> bool {
+        return msg_class == MSG_TASK_RESULT;
     }
 
     // A signed taskResult body is the receipt fields followed by the executor's
@@ -56,8 +56,8 @@ module TriA2AWire {
     const SIG_LEN: u32 = 64;   // Ed25519 signature = 64 bytes
 
     // Only a taskResult carries a signature (a taskAssign has no result to sign).
-    fn body_has_signature(class: u32) -> bool {
-        return class == MSG_TASK_RESULT;
+    fn body_has_signature(msg_class: u32) -> bool {
+        return msg_class == MSG_TASK_RESULT;
     }
 
     // Byte offset of the signature inside the datagram, after a receipt body of the
@@ -118,7 +118,7 @@ module TriA2AWire {
 
     // The header is fixed-length; the body starts right after it.
     test header_layout {
-        assert(HDR_LEN == 7, "class(1)+task(4)+skill(2)");
+        assert(HDR_LEN == 7, "msg_class(1)+task(4)+skill(2)");
         assert(body_offset() == OFF_BODY, "body after the fixed header");
         assert(OFF_SKILL == 5, "skill at byte 5");
     }
@@ -127,8 +127,8 @@ module TriA2AWire {
     test class_rules {
         assert(class_valid(MSG_TASK_ASSIGN) == true, "assign is valid");
         assert(class_valid(MSG_TASK_RESULT) == true, "result is valid");
-        assert(class_valid(0) == false, "class 0 is malformed");
-        assert(class_valid(99) == false, "unknown class is malformed");
+        assert(class_valid(0) == false, "msg_class 0 is malformed");
+        assert(class_valid(99) == false, "unknown msg_class is malformed");
         assert(body_has_receipt(MSG_TASK_RESULT) == true, "result carries a receipt");
         assert(body_has_receipt(MSG_TASK_ASSIGN) == false, "assign carries no receipt");
     }

specs/tri_compute_bitnet.t27

@@ -2,7 +2,7 @@
 // GF16 activations. This is the target workload the whole GF-vs-ternary analysis
 // points at -- weights are the 0-DSP part (sign-select / popcount, as in
 // trinet_mac32), the GF16 activation and accumulated result are the value part
-// (magnitude, DSP or -nodsp soft-logic). One receipt binds BOTH: the packed
+// (magnitude, DSP or -nodsp soft-logic). One receipt binds BOTH: the packed_w
 // ternary weight code, the GF16 activation hash, and the GF16 result. It also
 // exposes the sparsity the ternary part exploits (zero weights are skipped).
 //
@@ -29,7 +29,7 @@ module TriComputeBitnet {
         return d ^ (d >> 16);
     }
 
-    // Count active (nonzero) ternary weights in a packed 4-trit word (2 bits each).
+    // Count active (nonzero) ternary weights in a packed_w 4-trit word (2 bits each).
     // This is the sparsity the 0-DSP path exploits: zero weights contribute
     // nothing and cost nothing.
     // A single 2-bit trit is ACTIVE (a real +1 or -1 weight) iff it is exactly 01
@@ -50,13 +50,13 @@ module TriComputeBitnet {
         }
     }
 
-    fn active_weights4(packed: u32) -> u32 {
-        return is_active(packed & 3) + is_active((packed >> 2) & 3)
-             + is_active((packed >> 4) & 3) + is_active((packed >> 6) & 3);
+    fn active_weights4(packed_w: u32) -> u32 {
+        return is_active(packed_w & 3) + is_active((packed_w >> 2) & 3)
+             + is_active((packed_w >> 4) & 3) + is_active((packed_w >> 6) & 3);
     }
 
     // Canonical packing: since 00 AND 11 both decode to 0, the SAME logical weight
-    // vector has multiple packed encodings (e.g. [0,0,0,0] is 0x00 or 0xFF or any
+    // vector has multiple packed_w encodings (e.g. [0,0,0,0] is 0x00 or 0xFF or any
     // mix), each hashing to a DIFFERENT bitnet_leaf -- weight malleability: one
     // logical matrix, many valid receipts. Fix a canonical form: a trit is
     // canonical iff it is NOT 0b11 (zero is always 00). A packing is canonical iff
@@ -71,13 +71,13 @@ module TriComputeBitnet {
         }
     }
 
-    fn weights_canonical4(packed: u32) -> u32 {
-        return trit_canonical(packed & 3) + trit_canonical((packed >> 2) & 3)
-             + trit_canonical((packed >> 4) & 3) + trit_canonical((packed >> 6) & 3);
+    fn weights_canonical4(packed_w: u32) -> u32 {
+        return trit_canonical(packed_w & 3) + trit_canonical((packed_w >> 2) & 3)
+             + trit_canonical((packed_w >> 4) & 3) + trit_canonical((packed_w >> 6) & 3);
     }
 
-    fn packing_is_canonical(packed: u32) -> bool {
-        return weights_canonical4(packed) == 4;
+    fn packing_is_canonical(packed_w: u32) -> bool {
+        return weights_canonical4(packed_w) == 4;
     }
 
     // ---- Signed decode: what the 0-DSP popcount-MAC actually sums ----
@@ -104,20 +104,20 @@ module TriComputeBitnet {
         }
     }
 
-    fn pos_weights4(packed: u32) -> u32 {
-        return is_pos(packed & 3) + is_pos((packed >> 2) & 3)
-             + is_pos((packed >> 4) & 3) + is_pos((packed >> 6) & 3);
+    fn pos_weights4(packed_w: u32) -> u32 {
+        return is_pos(packed_w & 3) + is_pos((packed_w >> 2) & 3)
+             + is_pos((packed_w >> 4) & 3) + is_pos((packed_w >> 6) & 3);
     }
 
-    fn neg_weights4(packed: u32) -> u32 {
-        return is_neg(packed & 3) + is_neg((packed >> 2) & 3)
-             + is_neg((packed >> 4) & 3) + is_neg((packed >> 6) & 3);
+    fn neg_weights4(packed_w: u32) -> u32 {
+        return is_neg(packed_w & 3) + is_neg((packed_w >> 2) & 3)
+             + is_neg((packed_w >> 4) & 3) + is_neg((packed_w >> 6) & 3);
     }
 
     // The signed ternary sum for unit activations, biased by 4 to fit u32: value 4
     // is a net zero, 8 is all +1, 0 is all -1. This is the popcount-MAC's core.
-    fn sign_balance_biased(packed: u32) -> u32 {
-        return (pos_weights4(packed) + 4) - neg_weights4(packed);
+    fn sign_balance_biased(packed_w: u32) -> u32 {
+        return (pos_weights4(packed_w) + 4) - neg_weights4(packed_w);
     }
 
     // Verifiable ternary part: the analogue of a GF-value recompute in a dispute.
@@ -179,7 +179,7 @@ module TriComputeBitnet {
 
     // Sparsity: nonzero trits are counted, zeros are skipped.
     test sparsity_count {
-        // packed 0x61 = trits [t0=+1, t1=0, t2=-1, t3=+1] -> 3 active
+        // packed_w 0x61 = trits [t0=+1, t1=0, t2=-1, t3=+1] -> 3 active
         assert(active_weights4(0x61) == 3, "three nonzero weights");
         assert(active_weights4(0x00) == 0, "all-zero weights -> nothing active");
         assert(active_weights4(0x55) == 4, "0x55 = four +1 trits -> 4 active");

specs/tri_depin.t27

@@ -126,9 +126,9 @@ module TriDepin {
 
     // Size-binding at the accumulator: same digest, different byte count -> diff acc.
     test absorb_size_bound {
-        small = relay_absorb(TRI_GENESIS, 0xAAAA0001, 70);
+        small_acc = relay_absorb(TRI_GENESIS, 0xAAAA0001, 70);
         big   = relay_absorb(TRI_GENESIS, 0xAAAA0001, 1200);
-        assert(small != big, "bytes bound in acc");
+        assert(small_acc != big, "bytes bound in acc");
     }
 
     // Identity-binding: identical work, different node key -> different seal.