From 4999e48aaf98285fd21908d5643eb5207c910c8d Mon Sep 17 00:00:00 2001 From: SSD DDD Date: Sat, 8 Aug 2026 02:45:21 +0700 Subject: [PATCH] spec: legalize Verilog-reserved identifiers + fix a stale tri_a2a test; icarus KAT runs all 30 lowerable specs Three specs used Verilog/SystemVerilog reserved words as identifiers, which broke their generated testbenches: tri_a2a_wire ('class' -> msg_class), tri_compute_bitnet ('packed' -> packed_w), tri_depin ('small' -> small_acc). tri_a2a's hosted_skill_set test still asserted 0xA511 is not hosted -- but 0xA511 is SKILL_GFT32_MUL and IS hosted; the test predates the GF-T32 skills and was never executed until the icarus flow ran it (now asserts on 0xA512, an unknown-op id). With upstream t27#1899 (test-local reg decls + 64-bit __mul_noop), every icarus-lowerable ring spec simulates clean; the gft-verilog-kat run grows 8 -> 30 specs (crypto_frame and discovery are not lowerable). Local validation: 30/30 sim pass, full cargo gate ok. Co-Authored-By: Claude Fable 5 --- .github/workflows/gft-verilog-kat.yml | 41 +++++++++++++++++++-------- specs/tri_a2a.t27 | 2 +- specs/tri_a2a_wire.t27 | 26 ++++++++--------- specs/tri_compute_bitnet.t27 | 40 +++++++++++++------------- specs/tri_depin.t27 | 4 +-- 5 files changed, 65 insertions(+), 48 deletions(-) diff --git a/.github/workflows/gft-verilog-kat.yml b/.github/workflows/gft-verilog-kat.yml index 46a94f17..d45f6aad 100644 --- a/.github/workflows/gft-verilog-kat.yml +++ b/.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" diff --git a/specs/tri_a2a.t27 b/specs/tri_a2a.t27 index c4a38314..af349545 100644 --- a/specs/tri_a2a.t27 +++ b/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"); } diff --git a/specs/tri_a2a_wire.t27 b/specs/tri_a2a_wire.t27 index af267836..bdd1481c 100644 --- a/specs/tri_a2a_wire.t27 +++ b/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"); } diff --git a/specs/tri_compute_bitnet.t27 b/specs/tri_compute_bitnet.t27 index bab573f7..342a5ea5 100644 --- a/specs/tri_compute_bitnet.t27 +++ b/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"); diff --git a/specs/tri_depin.t27 b/specs/tri_depin.t27 index d09ed794..c1f30b51 100644 --- a/specs/tri_depin.t27 +++ b/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.