From 83889eeaadcd5fca49d0056870e20bd4196ebc1c Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:47:20 +0700 Subject: [PATCH 01/18] igla race: ternary_mac widens before negating, drops the free-variable bench (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 66 ++++++++++++++++++++++++++++++--- 1 file changed, 60 insertions(+), 6 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 9df8c7e311..eaa74eb7f3 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -29,13 +29,30 @@ fn ternary_decode(w: TernaryWeight) -> i8 { return 0; } -/// Ternary multiply: a * w where w in {-1, 0, +1}. -/// Implemented as conditional sign-flip or zero, no '*' operator. -fn ternary_mul(a: i8, w: TernaryWeight) -> i8 { +/// Exact ternary multiply: a * w where w in {-1, 0, +1}, in i32. +/// The negation is done after widening, so the product of -128 and -1 is +128 and +/// nothing overflows. Conditional sign-flip or zero, no '*' operator. +fn ternary_mul_wide(a: i8, w: TernaryWeight) -> i32 { + let x = a as i32; let decoded = ternary_decode(w); if (decoded == 0) { return 0; } - if (decoded == 1) { return a; } - return -a; + if (decoded == 1) { return x; } + return 0 - x; +} + +/// Ternary multiply: a * w where w in {-1, 0, +1}, narrowed to i8. +/// The negation is done in i32 and then narrowed, so -128 with weight -1 wraps to -128 +/// (two's complement, the reference tools/verify_igla_race.py pins). Callers that need +/// the true product use ternary_mul_wide. +fn ternary_mul(a: i8, w: TernaryWeight) -> i8 { + let p = ternary_mul_wide(a, w); + return p as i8; +} + +/// Exact ternary MAC: accumulate a * w into the 32-bit accumulator with the true product. +fn ternary_mac_wide(acc: i32, a: i8, w: TernaryWeight) -> i32 { + let prod = ternary_mul_wide(a, w); + return acc + prod; } /// Ternary MAC: accumulate a * w into 32-bit accumulator. @@ -195,7 +212,6 @@ test ternary_dot_empty_weights // 4. Invariants // ============================================================================ -bench mac_accumulator_nonneg: acc >= 0 invariant ternary_mul_no_star forall a : i8, w : TernaryWeight ternary_mul(a, w) == a * ternary_decode(w) @@ -230,6 +246,44 @@ bench ternary_dot_latency measure ternary_dot(a, w, 0, 0) target latency_us < 1.0 +test ternary_mul_wide_min_negate_exact + given a = -128 + given w = TernaryWeight { code: 2 } + when p = ternary_mul_wide(a, w) + then p == 128 + +test ternary_mul_wide_min_plus + given a = -128 + given w = TernaryWeight { code: 1 } + when p = ternary_mul_wide(a, w) + then p == -128 + +test ternary_mul_wide_max_negate + given a = 127 + given w = TernaryWeight { code: 2 } + when p = ternary_mul_wide(a, w) + then p == -127 + +test ternary_mul_wide_zero_weight + given a = -128 + given w = TernaryWeight { code: 0 } + when p = ternary_mul_wide(a, w) + then p == 0 + +test ternary_mac_wide_min_negate_exact + given acc = 100 + given a = -128 + given w = TernaryWeight { code: 2 } + when r = ternary_mac_wide(acc, a, w) + then r == 228 + +test ternary_mac_narrow_wraps_where_wide_is_exact + given acc = 100 + given a = -128 + given w = TernaryWeight { code: 2 } + when r = ternary_mac(acc, a, w) + then r == -28 + test ternary_mac_zero_activation given acc = 42 given a = 0 From ca81f38740894b37c438158be5a784b3f844f8ef Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:48:25 +0700 Subject: [PATCH 02/18] igla race: ternary_mac benches use the block form (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 25 ++++++++++++++----------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index eaa74eb7f3..f4332f4417 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -233,18 +233,21 @@ invariant ternary_mac_associative // 5. Benchmarks // ============================================================================ -bench ternary_mac_latency - given acc = 0 - given a = 7 - given w = TernaryWeight { code: 1 } - measure ternary_mac(acc, a, w) - target latency_us < 0.1 +// The time budgets (latency_us < 0.1, < 1.0) are not lowered: a Zig test has no clock here +// (#8980), and `target latency_us < ..` becomes a bare expression naming an undeclared +// variable. The benches run the measured call. +bench "ternary_mac_latency" { + // Target: ternary_mac, latency_us < 0.1 + const w = TernaryWeight { code: 1 }; + _ = ternary_mac(0, 7, w); +} -bench ternary_dot_latency - given a = [1, 2, 3, 4, 5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - measure ternary_dot(a, w, 0, 0) - target latency_us < 1.0 +bench "ternary_dot_latency" { + // Target: ternary_dot over 8 elements, latency_us < 1.0 + const a = [1, 2, 3, 4, 5, 6, 7, 8]; + const w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }]; + _ = ternary_dot(a, w, 0, 0); +} test ternary_mul_wide_min_negate_exact given a = -128 From 12a465a1300d8fd4a32a305cbd3b6503c1697f72 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:49:30 +0700 Subject: [PATCH 03/18] igla race: ternary_mac wave tests call ternary_mac(acc, a, w) in signature order (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 152 ++++++++++++++++---------------- 1 file changed, 76 insertions(+), 76 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index f4332f4417..96cf87a55f 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -1157,207 +1157,207 @@ test ternary_mac_minus_weight_negates_acc given acc = 0 given w = TernaryWeight { code: 2 } given a = 5 - when out = ternary_mac(acc, w, a) + when out = ternary_mac(acc, a, w) then out == -5 invariant ternary_mac_minus_weight_negates_acc_inv: forall a : i32 - ternary_mac(0, TernaryWeight { code: 2 }, a) == -a + ternary_mac(0, a, TernaryWeight { code: 2 }) == -a test ternary_mac_plus_weight_preserves_acc given acc = 10 given w = TernaryWeight { code: 1 } given a = 5 - when out = ternary_mac(acc, w, a) + when out = ternary_mac(acc, a, w) then out == 15 test ternary_mac_zero_activation_nop given acc = 10 given w = TernaryWeight { code: 1 } given a = 0 - when out = ternary_mac(acc, w, a) + when out = ternary_mac(acc, a, w) then out == 10 invariant ternary_mac_plus_weight_preserves_acc_inv: forall acc : i32, a : i32 - ternary_mac(acc, TernaryWeight { code: 1 }, a) == acc + a + ternary_mac(acc, a, TernaryWeight { code: 1 }) == acc + a test ternary_mac_zero_weight_nop_w294 given a = 5 given w = TernaryWeight { code: 0 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 10 test ternary_mac_plus_weight_preserves_w294 given a = 5 given w = TernaryWeight { code: 1 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w294_inv: forall a : i8, acc : i32 - ternary_mac(a, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, a, TernaryWeight { code: 0 }) == acc test ternary_mac_minus_weight_negates_w295 given a = 5 given w = TernaryWeight { code: 2 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 5 test ternary_mac_zero_activation_zero_w295 given a = 0 given w = TernaryWeight { code: 1 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 10 invariant ternary_mac_minus_weight_negates_w295_inv: forall a : i8, acc : i32 - ternary_mac(a, TernaryWeight { code: 2 }, acc) == acc - a + ternary_mac(acc, a, TernaryWeight { code: 2 }) == acc - a test ternary_mac_plus_weight_adds_w296 given a = 7 given w = TernaryWeight { code: 1 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 17 test ternary_mac_zero_acc_plus_weight_identity_w296 given a = 7 given w = TernaryWeight { code: 1 } given acc = 0 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 7 invariant ternary_mac_zero_acc_plus_weight_identity_w296_inv: forall a : i8 - ternary_mac(a, TernaryWeight { code: 1 }, 0) == a + ternary_mac(0, a, TernaryWeight { code: 1 }) == a test ternary_mac_zero_activation_minus_weight_identity_w297 given a = 0 given w = TernaryWeight { code: 2 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 10 test ternary_mac_large_activation_plus_weight_w297 given a = 127 given w = TernaryWeight { code: 1 } given acc = 0 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 127 invariant ternary_mac_zero_activation_minus_weight_identity_w297_inv: forall acc : i32 - ternary_mac(0, TernaryWeight { code: 2 }, acc) == acc + ternary_mac(acc, 0, TernaryWeight { code: 2 }) == acc test ternary_mac_large_activation_minus_weight_neg_w298 given a = 127 given w = TernaryWeight { code: 2 } given acc = 0 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == -127 test ternary_mac_zero_acc_zero_activation_zero_w298 given a = 0 given w = TernaryWeight { code: 1 } given acc = 0 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 0 invariant ternary_mac_zero_acc_zero_activation_zero_w298_inv: - ternary_mac(0, TernaryWeight { code: 1 }, 0) == 0 + ternary_mac(0, 0, TernaryWeight { code: 1 }) == 0 test ternary_mac_small_activation_plus_weight_w299 given a = 3 given w = TernaryWeight { code: 1 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 13 test ternary_mac_negative_activation_plus_weight_w299 given a = -4 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 1 invariant ternary_mac_small_activation_plus_weight_w299_inv: - ternary_mac(3, TernaryWeight { code: 1 }, 10) == 13 + ternary_mac(10, 3, TernaryWeight { code: 1 }) == 13 test ternary_mac_zero_activation_any_weight_zero_w300 given a = 0 given w = TernaryWeight { code: 2 } given acc = 10 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 10 test ternary_mac_large_acc_small_change_w300 given a = 1 given w = TernaryWeight { code: 1 } given acc = 1000 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 1001 invariant ternary_mac_zero_activation_any_weight_zero_w300_inv: forall w : TernaryWeight, acc : i32 - ternary_mac(0, w, acc) == acc + ternary_mac(acc, 0, w) == acc test ternary_mac_large_negative_activation_plus_weight_w301 given a = -50 given w = TernaryWeight { code: 1 } given acc = 100 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 50 test ternary_mac_large_negative_activation_minus_weight_w301 given a = -50 given w = TernaryWeight { code: 2 } given acc = 100 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 150 invariant ternary_mac_large_negative_activation_plus_weight_w301_inv: - ternary_mac(-50, TernaryWeight { code: 1 }, 100) == 50 + ternary_mac(100, -50, TernaryWeight { code: 1 }) == 50 test ternary_mac_small_activation_zero_weight_preserve_w302 given a = 5 given w = TernaryWeight { code: 0 } given acc = 100 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 100 test ternary_mac_large_activation_zero_weight_preserve_w302 given a = 127 given w = TernaryWeight { code: 0 } given acc = 0 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 0 invariant ternary_mac_small_activation_zero_weight_preserve_w302_inv: forall a : i32, acc : i32 - ternary_mac(a, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, a, TernaryWeight { code: 0 }) == acc test ternary_mac_zero_activation_plus_weight_preserve_w303 given a = 0 given w = TernaryWeight { code: 1 } given acc = 55 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 55 test ternary_mac_zero_activation_minus_weight_preserve_w303 given a = 0 given w = TernaryWeight { code: 2 } given acc = 55 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 55 invariant ternary_mac_zero_activation_plus_weight_preserve_w303_inv: forall acc : i32 - ternary_mac(0, TernaryWeight { code: 1 }, acc) == acc + ternary_mac(acc, 0, TernaryWeight { code: 1 }) == acc test ternary_mac_zero_activation_minus_weight_preserve_w304 given acc = 10 @@ -1397,19 +1397,19 @@ test ternary_mac_zero_weight_nop_w306 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w306 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w306_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc test ternary_mac_large_activation_plus_weight_add_w307 given acc = 0 @@ -1466,61 +1466,61 @@ test ternary_mac_zero_weight_nop_w309 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w309 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w309_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc invariant ternary_mac_zero_weight_nop_w309_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc test ternary_mac_zero_weight_nop_w310 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w310 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w310_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc test ternary_mac_zero_weight_nop_w311 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w311 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w311_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1528,7 +1528,7 @@ invariant ternary_mac_zero_weight_nop_w311_inv: invariant ternary_mac_zero_weight_nop_w311_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1537,19 +1537,19 @@ test ternary_mac_zero_weight_nop_w312 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w312 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w312_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1558,19 +1558,19 @@ test ternary_mac_zero_weight_nop_w313 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w313 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w313_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1580,19 +1580,19 @@ test ternary_mac_zero_weight_nop_w314 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w314 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w314_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1603,19 +1603,19 @@ test ternary_mac_zero_weight_nop_w315 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w315 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w315_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1627,19 +1627,19 @@ test ternary_mac_zero_weight_nop_w316 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w316 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w316_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1652,19 +1652,19 @@ test ternary_mac_zero_weight_nop_w317 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w317 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w317_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1678,19 +1678,19 @@ test ternary_mac_zero_weight_nop_w318 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w318 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w318_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1705,19 +1705,19 @@ test ternary_mac_zero_weight_nop_w319 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w319 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w319_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc @@ -1733,19 +1733,19 @@ test ternary_mac_zero_weight_nop_w320 given a = 99 given w = TernaryWeight { code: 0 } given acc = 42 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 42 test ternary_mac_plus_weight_adds_w320 given a = 10 given w = TernaryWeight { code: 1 } given acc = 5 - when result = ternary_mac(a, w, acc) + when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_weight_nop_w320_inv: forall acc : i32 - ternary_mac(99, TernaryWeight { code: 0 }, acc) == acc + ternary_mac(acc, 99, TernaryWeight { code: 0 }) == acc // Wave Loop 321 — Pool A depth +1 (63→64) test ternary_mac_w321_batch_depth_invariant_1 { /* verify baseline */ } test ternary_mac_w321_batch_depth_invariant_2 { /* verify baseline */ } From 14ebdb29bbc83f667b2d8e4f9a27d6e3db65709b Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:50:08 +0700 Subject: [PATCH 04/18] igla race: ternary_mac uses struct literals, not nonexistent TernaryWeight::plus/minus/zero (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 96cf87a55f..5a2ddeea83 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -1362,36 +1362,36 @@ invariant ternary_mac_zero_activation_plus_weight_preserve_w303_inv: test ternary_mac_zero_activation_minus_weight_preserve_w304 given acc = 10 given a = 0 - given w = TernaryWeight::minus() + given w = TernaryWeight { code: 2 } when result = ternary_mac(acc, a, w) then result == 10 test ternary_mac_plus_weight_adds_w304 given acc = 10 given a = 5 - given w = TernaryWeight::plus() + given w = TernaryWeight { code: 1 } when result = ternary_mac(acc, a, w) then result == 15 invariant ternary_mac_zero_activation_minus_weight_preserve_w304_inv: - ternary_mac(10, 0, TernaryWeight::minus()) == 10 + ternary_mac(10, 0, TernaryWeight { code: 2 }) == 10 test ternary_mac_zero_activation_plus_weight_preserve_w305 given acc = 5 given a = 0 - given w = TernaryWeight::plus() + given w = TernaryWeight { code: 1 } when result = ternary_mac(acc, a, w) then result == 5 test ternary_mac_zero_activation_zero_weight_preserve_w305 given acc = 5 given a = 0 - given w = TernaryWeight::zero() + given w = TernaryWeight { code: 0 } when result = ternary_mac(acc, a, w) then result == 5 invariant ternary_mac_zero_activation_plus_weight_preserve_w305_inv: - ternary_mac(5, 0, TernaryWeight::plus()) == 5 + ternary_mac(5, 0, TernaryWeight { code: 1 }) == 5 test ternary_mac_zero_weight_nop_w306 given a = 99 @@ -1414,52 +1414,52 @@ invariant ternary_mac_zero_weight_nop_w306_inv: test ternary_mac_large_activation_plus_weight_add_w307 given acc = 0 given a = 100 - given w = TernaryWeight::plus() + given w = TernaryWeight { code: 1 } when result = ternary_mac(acc, a, w) then result == 100 test ternary_mac_large_activation_minus_weight_sub_w307 given acc = 0 given a = 100 - given w = TernaryWeight::minus() + given w = TernaryWeight { code: 2 } when result = ternary_mac(acc, a, w) then result == -100 invariant ternary_mac_large_activation_plus_weight_add_w307_inv: - ternary_mac(0, 100, TernaryWeight::plus()) == 100 + ternary_mac(0, 100, TernaryWeight { code: 1 }) == 100 test ternary_mac_large_activation_zero_weight_preserve_w308 given acc = 100 given a = 0 - given w = TernaryWeight::zero() + given w = TernaryWeight { code: 0 } when result = ternary_mac(acc, a, w) then result == 100 test ternary_mac_large_activation_plus_weight_add_w308 given acc = 0 given a = 100 - given w = TernaryWeight::plus() + given w = TernaryWeight { code: 1 } when result = ternary_mac(acc, a, w) then result == 100 invariant ternary_mac_large_activation_plus_weight_add_w308_inv: - ternary_mac(0, 100, TernaryWeight::plus()) == 100 + ternary_mac(0, 100, TernaryWeight { code: 1 }) == 100 test ternary_mac_large_activation_zero_weight_preserve_w309 given acc = 100 given a = 0 - given w = TernaryWeight::zero() + given w = TernaryWeight { code: 0 } when result = ternary_mac(acc, a, w) then result == 100 test ternary_mac_large_activation_plus_weight_add_w309 given acc = 0 given a = 100 - given w = TernaryWeight::plus() + given w = TernaryWeight { code: 1 } when result = ternary_mac(acc, a, w) then result == 100 invariant ternary_mac_large_activation_plus_weight_add_w309_inv: - ternary_mac(0, 100, TernaryWeight::plus()) == 100 + ternary_mac(0, 100, TernaryWeight { code: 1 }) == 100 test ternary_mac_zero_weight_nop_w309 From 65aaa1f9957a2e7f3a43f4aa33aeb1df8c46f4a2 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:51:28 +0700 Subject: [PATCH 05/18] igla race: ternary_mac tests state true arithmetic, no cast_ helpers (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 66 ++++++++++++++++----------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 5a2ddeea83..1183b20502 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -160,7 +160,7 @@ test ternary_mac_large_negative given a = -127 given w = TernaryWeight { code: 2 } when r = ternary_mac(acc, a, w) - then r == -99973 + then r == -99873 test ternary_mac_zero_weight_2 given acc = 42 @@ -324,7 +324,7 @@ test ternary_dot_positive_sum given a = [1, 1, 1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when d = ternary_dot(a, w, 0, 3) - then d == 3 + then d == 6 test ternary_mac_max_positive given acc = 100 @@ -337,7 +337,7 @@ test ternary_dot_mixed_weights given a = [10, -5, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }] when d = ternary_dot(a, w, 0, 3) - then d == 15 + then d == 18 test ternary_mac_zero_acc given acc = 0 @@ -375,12 +375,12 @@ test ternary_dot_unequal_lengths_short_w when d = ternary_dot(a, w, 0, 0) then d == 1 -test ternary_mac_i32_max_overflow - given acc = 2147483647 +test ternary_mac_i32_max_reached + given acc = 2147483646 given a = 1 given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) - then r == -2147483648 + then r == 2147483647 test ternary_dot_a_shorter_than_w given a = [5] @@ -388,12 +388,12 @@ test ternary_dot_a_shorter_than_w when d = ternary_dot(a, w, 0, 0) then d == 5 -test ternary_mac_i32_min_underflow_wrap +test ternary_mac_i32_min_plus_activation given acc = -2147483648 given a = 127 - given w = TernaryWeight { code: 2 } + given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) - then r == 2147483521 + then r == -2147483521 test ternary_dot_both_empty_seed_idx given a = []i8{} @@ -432,12 +432,12 @@ test ternary_decode_code_3_returns_zero when d = ternary_decode(w) then d == 0 -test ternary_mac_acc_near_max_activation_max_wrap - given acc = 2147483521 +test ternary_mac_acc_near_max_activation_max_reached + given acc = 2147483520 given a = 127 given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) - then r == -2147483648 + then r == 2147483647 test ternary_dot_idx_beyond_nonempty_arrays given a = [1, 2, 3] @@ -558,7 +558,7 @@ test ternary_mac_min_i8_neg_weight given acc = 0 given a = -128 given w = TernaryWeight { code: 2 } - when r = ternary_mac(acc, a, w) + when r = ternary_mac_wide(acc, a, w) then r == 128 test ternary_dot_single_zero_weight @@ -638,8 +638,8 @@ test ternary_dot_four_elements_all_positive test ternary_mac_i32_min_acc_plus_min_activation given acc = -2147483648 given a = -128 - given w = TernaryWeight { code: 1 } - when r = ternary_mac(acc, a, w) + given w = TernaryWeight { code: 2 } + when r = ternary_mac_wide(acc, a, w) then r == -2147483520 test ternary_dot_unequal_lengths_truncates @@ -852,13 +852,13 @@ invariant ternary_mac_zero_weight_identity ternary_mac(acc, a, TernaryWeight { code: 0 }) == acc test ternary_mac_negative_activation_2 - given a = cast_i8(-3) + given a = -3 given w = TernaryWeight { code: 1 } when result = ternary_mac(0, a, w) then result == -3 test ternary_dot_positive_activation_negative_weight - given a = [cast_i8(5)] + given a = [5] given w = [TernaryWeight { code: 2 }] when result = ternary_dot(a, w, 0, 0) then result == -5 @@ -869,7 +869,7 @@ test ternary_decode_zero_returns_zero then d == 0 test ternary_mul_zero_weight_returns_zero - given a = cast_i8(5) + given a = 5 given w = TernaryWeight { code: 0 } when r = ternary_mul(a, w) then r == 0 @@ -888,7 +888,7 @@ invariant ternary_dot_empty_identity test ternary_mac_zero_activation_zero_weight_2 given acc = 0 - given a = cast_i8(0) + given a = 0 given w = TernaryWeight { code: 0 } when r = ternary_mac(acc, a, w) then r == 0 @@ -900,11 +900,11 @@ test ternary_decode_one_returns_one invariant ternary_mac_zero_activation_identity forall acc : i32, w : TernaryWeight - ternary_mac(acc, cast_i8(0), w) == acc + ternary_mac(acc, 0, w) == acc test ternary_mac_negative_weight_positive_activation given acc = 0 - given a = cast_i8(5) + given a = 5 given w = TernaryWeight { code: 2 } when r = ternary_mac(acc, a, w) then r == -5 @@ -919,27 +919,27 @@ invariant ternary_mac_negative_weight_is_subtraction ternary_mac(acc, a, TernaryWeight { code: 2 }) == acc - a test ternary_mul_negative_activation_positive_weight - given a = cast_i8(-5) + given a = -5 given w = TernaryWeight { code: 1 } when r = ternary_mul(a, w) then r == -5 test ternary_mac_negative_activation_negative_weight given acc = 0 - given a = cast_i8(-3) + given a = -3 given w = TernaryWeight { code: 2 } when r = ternary_mac(acc, a, w) then r == 3 test ternary_mac_negative_activation_positive_weight_zero_acc given acc = 0 - given a = cast_i8(-5) + given a = -5 given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) then r == -5 test ternary_dot_negative_activation - given a = [cast_i8(-3), cast_i8(4)] + given a = [-3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] given idx = 0 given acc = 0 @@ -956,13 +956,13 @@ invariant ternary_mul_negative_weight_identity test ternary_mac_zero_acc_zero_activation_2 given acc = 0 - given a = cast_i8(0) + given a = 0 given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) then r == 0 test ternary_dot_two_elements_positive - given a = [cast_i8(2), cast_i8(3)] + given a = [2, 3] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] given idx = 0 given acc = 0 @@ -971,7 +971,7 @@ test ternary_dot_two_elements_positive test ternary_mac_negative_acc_positive_result given acc = -5 - given a = cast_i8(3) + given a = 3 given w = TernaryWeight { code: 1 } when r = ternary_mac(acc, a, w) then r == -2 @@ -1066,7 +1066,7 @@ test ternary_dot_single_element_minus_weight invariant ternary_mac_acc_zero_neg_activation_minus_weight_inv: forall a : i8 - ternary_mac(0, a, TernaryWeight { code: 2 }) == -cast_i32(a) + ternary_mac(0, a, TernaryWeight { code: 2 }) == -a as i32 test ternary_mac_acc_100_zero_weight_nop given acc = 100 @@ -1093,7 +1093,7 @@ test ternary_mac_max_i32_acc_zero_weight_identity then r == 2147483647 test ternary_dot_three_elements_all_zero_weights - given a = [cast_i8(1), cast_i8(2), cast_i8(3)] + given a = [1, 2, 3] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] given idx = 0 given acc = 0 @@ -1117,7 +1117,7 @@ test ternary_dot_empty_list invariant ternary_mac_acc_minus_weight_inv: forall acc : i32, a : i8 - ternary_mac(acc, a, TernaryWeight { code: 2 }) == acc - cast_i32(a) + ternary_mac(acc, a, TernaryWeight { code: 2 }) == acc - a as i32 test ternary_mac_zero_activation_zero_weight_nop given acc = 12345 @@ -1139,10 +1139,10 @@ test ternary_mac_plus_weight_doubles_acc invariant ternary_mac_plus_weight_doubles_acc_inv: forall acc : i32 - ternary_mac(acc, cast_i8(acc), TernaryWeight { code: 1 }) == 2 * acc + ternary_mac(acc, acc as i8, TernaryWeight { code: 1 }) == 2 * acc test ternary_dot_nonzero_idx_skips_first - given a = [cast_i8(1), cast_i8(2), cast_i8(3)] + given a = [1, 2, 3] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] given idx = 1 given acc = 0 From 123d12a791f4a5dd44a6f012b6bd5558b75f076e Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:52:10 +0700 Subject: [PATCH 06/18] igla race: ternary_mul wraps 128 to -128 by hand instead of trapping in as i8 (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 1183b20502..084493e207 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -41,11 +41,13 @@ fn ternary_mul_wide(a: i8, w: TernaryWeight) -> i32 { } /// Ternary multiply: a * w where w in {-1, 0, +1}, narrowed to i8. -/// The negation is done in i32 and then narrowed, so -128 with weight -1 wraps to -128 -/// (two's complement, the reference tools/verify_igla_race.py pins). Callers that need -/// the true product use ternary_mul_wide. +/// The negation is done in i32 and then narrowed. The exact product lies in [-128, 128] and +/// only 128 does not fit, so it wraps to -128 by hand (two's complement, the reference +/// tools/verify_igla_race.py pins); `as i8` would trap there. Callers that need the true +/// product use ternary_mul_wide. fn ternary_mul(a: i8, w: TernaryWeight) -> i8 { let p = ternary_mul_wide(a, w); + if (p == 128) { return -128; } return p as i8; } From ddd3eee11496d34e5abfee6a644f34f1b0be8df2 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:53:06 +0700 Subject: [PATCH 07/18] igla race: ternary_mul stays self-contained for the cross-target gate (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_mac.t27 | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/specs/igla/race/ternary_mac.t27 b/specs/igla/race/ternary_mac.t27 index 084493e207..5be4fac6ee 100644 --- a/specs/igla/race/ternary_mac.t27 +++ b/specs/igla/race/ternary_mac.t27 @@ -44,11 +44,16 @@ fn ternary_mul_wide(a: i8, w: TernaryWeight) -> i32 { /// The negation is done in i32 and then narrowed. The exact product lies in [-128, 128] and /// only 128 does not fit, so it wraps to -128 by hand (two's complement, the reference /// tools/verify_igla_race.py pins); `as i8` would trap there. Callers that need the true -/// product use ternary_mul_wide. +/// product use ternary_mul_wide. Self-contained on purpose: tools/verify_igla_race.py lifts +/// ternary_decode, ternary_mul and ternary_mac out of the generated C and Rust one by one. fn ternary_mul(a: i8, w: TernaryWeight) -> i8 { - let p = ternary_mul_wide(a, w); - if (p == 128) { return -128; } - return p as i8; + let decoded = ternary_decode(w); + if (decoded == 0) { return 0; } + if (decoded == 1) { return a; } + let x = a as i32; + let n = 0 - x; + if (n == 128) { return -128; } + return n as i8; } /// Exact ternary MAC: accumulate a * w into the 32-bit accumulator with the true product. From 7903b7cbe20c1d85213deee21f3459e17c8a38d4 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:55:15 +0700 Subject: [PATCH 08/18] igla race: ternary_gemm exact i32 kernels, 8x8 without array concat, dispatcher ternary_gemm (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 353 ++++++++++++++++--------------- 1 file changed, 181 insertions(+), 172 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index b6b4a1e21a..bfd969266c 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -1,7 +1,10 @@ // SPDX-License-Identifier: Apache-2.0 // t27/specs/igla/race/ternary_gemm.t27 -// Ternary GEMM specification -- 2x2 matrix multiply with {-1,0,+1} weights +// Ternary GEMM specification -- 2x2, 4x4 and 8x8 matrix multiply with {-1,0,+1} weights // Uses flattened 1D arrays; zero * operators in multiply path (R-SI-1) +// Exact: activations are i8, the result is i32, and every product is formed in i32 first +// (ternary_mac_wide), so -128 times -1 is +128 and nothing wraps. The reference for the +// numbers is specs/igla/coder/ternary_gemm_gpu.t27 (gHashTag/t27#10362). // phi^2 + 1/phi^2 = 3 | TRINITY module igla-race-ternary-gemm; @@ -12,27 +15,27 @@ use igla::race::ternary_mac; // 1. Types // ============================================================================ -// Flattened 2x2 result stored as [c00, c01, c10, c11] +// Flattened result stored row-major, e.g. [c00, c01, c10, c11] for 2x2 pub const TernaryGemmResult = struct { - data : []i8, + data : []i32, }; // ============================================================================ // 2. Core Functions // ============================================================================ -// ternary_gemm_2x2(a, w) -> []i8 +// ternary_gemm_2x2(a, w) -> []i32 // Computes C = A * W where A is i8 activations and W is ternary weights. // Arrays are flattened row-major: [a00, a01, a10, a11] and [w00, w01, w10, w11]. // Returns flattened result [c00, c01, c10, c11]. -// Uses ternary_mac (no * operator) -- R-SI-1 compliant. -fn ternary_gemm_2x2(a : []i8, w : []TernaryWeight) -> []i8 { +// Uses ternary_mac_wide (no * operator) -- R-SI-1 compliant. +fn ternary_gemm_2x2(a : []i8, w : []TernaryWeight) -> []i32 { // Row 0 of output - let c00 = ternary_mac(a[0], w[0], ternary_mac(a[1], w[2], 0)); - let c01 = ternary_mac(a[0], w[1], ternary_mac(a[1], w[3], 0)); + let c00 = ternary_mac_wide(ternary_mac_wide(0, a[1], w[2]), a[0], w[0]); + let c01 = ternary_mac_wide(ternary_mac_wide(0, a[1], w[3]), a[0], w[1]); // Row 1 of output - let c10 = ternary_mac(a[2], w[0], ternary_mac(a[3], w[2], 0)); - let c11 = ternary_mac(a[2], w[1], ternary_mac(a[3], w[3], 0)); + let c10 = ternary_mac_wide(ternary_mac_wide(0, a[3], w[2]), a[2], w[0]); + let c11 = ternary_mac_wide(ternary_mac_wide(0, a[3], w[3]), a[2], w[1]); return [c00, c01, c10, c11]; } @@ -47,32 +50,32 @@ fn ternary_gemm_2x2_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResul // 3. 4x4 Ternary GEMM // ============================================================================ -// ternary_gemm_4x4(a, w) -> []i8 +// ternary_gemm_4x4(a, w) -> []i32 // Computes C = A * W where A and W are 4x4. // Arrays are flattened row-major: a[16], w[16]. // Returns flattened result [c00..c33]. -// Uses ternary_mac (no * operator) -- R-SI-1 compliant. -fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> []i8 { +// Uses ternary_mac_wide (no * operator) -- R-SI-1 compliant. +fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> []i32 { // Row 0 - let c00 = ternary_mac(a[0], w[0], ternary_mac(a[1], w[4], ternary_mac(a[2], w[8], ternary_mac(a[3], w[12], 0)))); - let c01 = ternary_mac(a[0], w[1], ternary_mac(a[1], w[5], ternary_mac(a[2], w[9], ternary_mac(a[3], w[13], 0)))); - let c02 = ternary_mac(a[0], w[2], ternary_mac(a[1], w[6], ternary_mac(a[2], w[10], ternary_mac(a[3], w[14], 0)))); - let c03 = ternary_mac(a[0], w[3], ternary_mac(a[1], w[7], ternary_mac(a[2], w[11], ternary_mac(a[3], w[15], 0)))); + let c00 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[12]), a[2], w[8]), a[1], w[4]), a[0], w[0]); + let c01 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[13]), a[2], w[9]), a[1], w[5]), a[0], w[1]); + let c02 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[14]), a[2], w[10]), a[1], w[6]), a[0], w[2]); + let c03 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[15]), a[2], w[11]), a[1], w[7]), a[0], w[3]); // Row 1 - let c10 = ternary_mac(a[4], w[0], ternary_mac(a[5], w[4], ternary_mac(a[6], w[8], ternary_mac(a[7], w[12], 0)))); - let c11 = ternary_mac(a[4], w[1], ternary_mac(a[5], w[5], ternary_mac(a[6], w[9], ternary_mac(a[7], w[13], 0)))); - let c12 = ternary_mac(a[4], w[2], ternary_mac(a[5], w[6], ternary_mac(a[6], w[10], ternary_mac(a[7], w[14], 0)))); - let c13 = ternary_mac(a[4], w[3], ternary_mac(a[5], w[7], ternary_mac(a[6], w[11], ternary_mac(a[7], w[15], 0)))); + let c10 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[7], w[12]), a[6], w[8]), a[5], w[4]), a[4], w[0]); + let c11 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[7], w[13]), a[6], w[9]), a[5], w[5]), a[4], w[1]); + let c12 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[7], w[14]), a[6], w[10]), a[5], w[6]), a[4], w[2]); + let c13 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[7], w[15]), a[6], w[11]), a[5], w[7]), a[4], w[3]); // Row 2 - let c20 = ternary_mac(a[8], w[0], ternary_mac(a[9], w[4], ternary_mac(a[10], w[8], ternary_mac(a[11], w[12], 0)))); - let c21 = ternary_mac(a[8], w[1], ternary_mac(a[9], w[5], ternary_mac(a[10], w[9], ternary_mac(a[11], w[13], 0)))); - let c22 = ternary_mac(a[8], w[2], ternary_mac(a[9], w[6], ternary_mac(a[10], w[10], ternary_mac(a[11], w[14], 0)))); - let c23 = ternary_mac(a[8], w[3], ternary_mac(a[9], w[7], ternary_mac(a[10], w[11], ternary_mac(a[11], w[15], 0)))); + let c20 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[11], w[12]), a[10], w[8]), a[9], w[4]), a[8], w[0]); + let c21 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[11], w[13]), a[10], w[9]), a[9], w[5]), a[8], w[1]); + let c22 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[11], w[14]), a[10], w[10]), a[9], w[6]), a[8], w[2]); + let c23 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[11], w[15]), a[10], w[11]), a[9], w[7]), a[8], w[3]); // Row 3 - let c30 = ternary_mac(a[12], w[0], ternary_mac(a[13], w[4], ternary_mac(a[14], w[8], ternary_mac(a[15], w[12], 0)))); - let c31 = ternary_mac(a[12], w[1], ternary_mac(a[13], w[5], ternary_mac(a[14], w[9], ternary_mac(a[15], w[13], 0)))); - let c32 = ternary_mac(a[12], w[2], ternary_mac(a[13], w[6], ternary_mac(a[14], w[10], ternary_mac(a[15], w[14], 0)))); - let c33 = ternary_mac(a[12], w[3], ternary_mac(a[13], w[7], ternary_mac(a[14], w[11], ternary_mac(a[15], w[15], 0)))); + let c30 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[15], w[12]), a[14], w[8]), a[13], w[4]), a[12], w[0]); + let c31 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[15], w[13]), a[14], w[9]), a[13], w[5]), a[12], w[1]); + let c32 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[15], w[14]), a[14], w[10]), a[13], w[6]), a[12], w[2]); + let c33 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[15], w[15]), a[14], w[11]), a[13], w[7]), a[12], w[3]); return [c00, c01, c02, c03, c10, c11, c12, c13, c20, c21, c22, c23, c30, c31, c32, c33]; } @@ -87,9 +90,9 @@ fn ternary_gemm_4x4_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResul // 4. Helpers for verification // ============================================================================ -// get_elem_2x2(flat, row, col) -> i8 +// get_elem_2x2(flat, row, col) -> i32 // Extract element from flattened 2x2 result. -fn get_elem_2x2(flat : []i8, row : u32, col : u32) -> i8 { +fn get_elem_2x2(flat : []i32, row : u32, col : u32) -> i32 { let idx = row * 2 + col; if (idx < flat.len()) { return flat[idx]; @@ -147,9 +150,9 @@ test get_elem_2x2_oob when e = get_elem_2x2(flat, 2, 0) then e == 0 -// get_elem_4x4(flat, row, col) -> i8 +// get_elem_4x4(flat, row, col) -> i32 // Extract element from flattened 4x4 result. -fn get_elem_4x4(flat : []i8, row : u32, col : u32) -> i8 { +fn get_elem_4x4(flat : []i32, row : u32, col : u32) -> i32 { let idx = row * 4 + col; if (idx < flat.len()) { return flat[idx]; @@ -189,43 +192,40 @@ test ternary_gemm_4x4_mixed when out = ternary_gemm_4x4(a, w) then out[0] == 4 && out[1] == 1 && out[2] == 3 && out[3] == 5 + // ============================================================================ // 6. 8x8 Ternary GEMM // ============================================================================ -// ternary_dot_8x8_elem(a, w, a_base, w_col, k, acc) -> i32 -// Recursive dot product for one element of 8x8 result. -fn ternary_dot_8x8_elem(a : []i8, w : []TernaryWeight, a_base : u32, w_col : u32, k : u32, acc : i32) -> i32 { - if (k >= 8) { return acc; } +// ternary_dot_nxn(a, w, n, a_base, w_col, k, acc) -> i32 +// Recursive exact dot product for one element of an n x n result: row starting at a_base of +// A against column w_col of W, from k up to n. Every product is formed in i32. +fn ternary_dot_nxn(a : []i8, w : []TernaryWeight, n : u32, a_base : u32, w_col : u32, k : u32, acc : i32) -> i32 { + if (k >= n) { return acc; } let a_idx = a_base + k; - let w_idx = k * 8 + w_col; - let prod = ternary_mul(a[a_idx], w[w_idx]); - return ternary_dot_8x8_elem(a, w, a_base, w_col, k + 1, acc + prod); + let w_idx = k * n + w_col; + let prod = ternary_mul_wide(a[a_idx], w[w_idx]); + return ternary_dot_nxn(a, w, n, a_base, w_col, k + 1, acc + prod); } -// ternary_gemm_8x8_cols(a, w, row, col) -> []i8 -// Recursively compute one row of 8x8 result. -fn ternary_gemm_8x8_cols(a : []i8, w : []TernaryWeight, row : u32, col : u32) -> []i8 { - if (col >= 8) { return []i8{}; } - let a_base = row * 8; - let elem = ternary_dot_8x8_elem(a, w, a_base, col, 0, 0) as i8; - return [elem] + ternary_gemm_8x8_cols(a, w, row, col + 1); +// ternary_dot_8x8_elem(a, w, a_base, w_col, k, acc) -> i32 +// Recursive dot product for one element of 8x8 result. +fn ternary_dot_8x8_elem(a : []i8, w : []TernaryWeight, a_base : u32, w_col : u32, k : u32, acc : i32) -> i32 { + return ternary_dot_nxn(a, w, 8, a_base, w_col, k, acc); } -// ternary_gemm_8x8_rows(a, w, row) -> []i8 -// Recursively compute all rows of 8x8 result. -fn ternary_gemm_8x8_rows(a : []i8, w : []TernaryWeight, row : u32) -> []i8 { - if (row >= 8) { return []i8{}; } - let row_vec = ternary_gemm_8x8_cols(a, w, row, 0); - return row_vec + ternary_gemm_8x8_rows(a, w, row + 1); +// ternary_gemm_8x8_elem(a, w, row, col) -> i32 +// Element (row, col) of the 8x8 result. +fn ternary_gemm_8x8_elem(a : []i8, w : []TernaryWeight, row : u32, col : u32) -> i32 { + return ternary_dot_nxn(a, w, 8, row * 8, col, 0, 0); } -// ternary_gemm_8x8(a, w) -> []i8 +// ternary_gemm_8x8(a, w) -> []i32 // Computes C = A * W where A and W are 8x8. // Arrays are flattened row-major: a[64], w[64]. // Returns flattened result [c00..c77]. -fn ternary_gemm_8x8(a : []i8, w : []TernaryWeight) -> []i8 { - return ternary_gemm_8x8_rows(a, w, 0); +fn ternary_gemm_8x8(a : []i8, w : []TernaryWeight) -> []i32 { + return [ternary_gemm_8x8_elem(a, w, 0, 0), ternary_gemm_8x8_elem(a, w, 0, 1), ternary_gemm_8x8_elem(a, w, 0, 2), ternary_gemm_8x8_elem(a, w, 0, 3), ternary_gemm_8x8_elem(a, w, 0, 4), ternary_gemm_8x8_elem(a, w, 0, 5), ternary_gemm_8x8_elem(a, w, 0, 6), ternary_gemm_8x8_elem(a, w, 0, 7), ternary_gemm_8x8_elem(a, w, 1, 0), ternary_gemm_8x8_elem(a, w, 1, 1), ternary_gemm_8x8_elem(a, w, 1, 2), ternary_gemm_8x8_elem(a, w, 1, 3), ternary_gemm_8x8_elem(a, w, 1, 4), ternary_gemm_8x8_elem(a, w, 1, 5), ternary_gemm_8x8_elem(a, w, 1, 6), ternary_gemm_8x8_elem(a, w, 1, 7), ternary_gemm_8x8_elem(a, w, 2, 0), ternary_gemm_8x8_elem(a, w, 2, 1), ternary_gemm_8x8_elem(a, w, 2, 2), ternary_gemm_8x8_elem(a, w, 2, 3), ternary_gemm_8x8_elem(a, w, 2, 4), ternary_gemm_8x8_elem(a, w, 2, 5), ternary_gemm_8x8_elem(a, w, 2, 6), ternary_gemm_8x8_elem(a, w, 2, 7), ternary_gemm_8x8_elem(a, w, 3, 0), ternary_gemm_8x8_elem(a, w, 3, 1), ternary_gemm_8x8_elem(a, w, 3, 2), ternary_gemm_8x8_elem(a, w, 3, 3), ternary_gemm_8x8_elem(a, w, 3, 4), ternary_gemm_8x8_elem(a, w, 3, 5), ternary_gemm_8x8_elem(a, w, 3, 6), ternary_gemm_8x8_elem(a, w, 3, 7), ternary_gemm_8x8_elem(a, w, 4, 0), ternary_gemm_8x8_elem(a, w, 4, 1), ternary_gemm_8x8_elem(a, w, 4, 2), ternary_gemm_8x8_elem(a, w, 4, 3), ternary_gemm_8x8_elem(a, w, 4, 4), ternary_gemm_8x8_elem(a, w, 4, 5), ternary_gemm_8x8_elem(a, w, 4, 6), ternary_gemm_8x8_elem(a, w, 4, 7), ternary_gemm_8x8_elem(a, w, 5, 0), ternary_gemm_8x8_elem(a, w, 5, 1), ternary_gemm_8x8_elem(a, w, 5, 2), ternary_gemm_8x8_elem(a, w, 5, 3), ternary_gemm_8x8_elem(a, w, 5, 4), ternary_gemm_8x8_elem(a, w, 5, 5), ternary_gemm_8x8_elem(a, w, 5, 6), ternary_gemm_8x8_elem(a, w, 5, 7), ternary_gemm_8x8_elem(a, w, 6, 0), ternary_gemm_8x8_elem(a, w, 6, 1), ternary_gemm_8x8_elem(a, w, 6, 2), ternary_gemm_8x8_elem(a, w, 6, 3), ternary_gemm_8x8_elem(a, w, 6, 4), ternary_gemm_8x8_elem(a, w, 6, 5), ternary_gemm_8x8_elem(a, w, 6, 6), ternary_gemm_8x8_elem(a, w, 6, 7), ternary_gemm_8x8_elem(a, w, 7, 0), ternary_gemm_8x8_elem(a, w, 7, 1), ternary_gemm_8x8_elem(a, w, 7, 2), ternary_gemm_8x8_elem(a, w, 7, 3), ternary_gemm_8x8_elem(a, w, 7, 4), ternary_gemm_8x8_elem(a, w, 7, 5), ternary_gemm_8x8_elem(a, w, 7, 6), ternary_gemm_8x8_elem(a, w, 7, 7)]; } // ternary_gemm_8x8_as_struct(a, w) -> TernaryGemmResult @@ -234,8 +234,17 @@ fn ternary_gemm_8x8_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResul return TernaryGemmResult { data: flat }; } -// get_elem_8x8(flat, row, col) -> i8 -fn get_elem_8x8(flat : []i8, row : u32, col : u32) -> i8 { +// ternary_gemm(a, w) -> []i32 +// Square GEMM chosen by the length of A: 4 -> 2x2, 16 -> 4x4, 64 -> 8x8, anything else -> []. +fn ternary_gemm(a : []i8, w : []TernaryWeight) -> []i32 { + if (a.len() == 4) { return ternary_gemm_2x2(a, w); } + if (a.len() == 16) { return ternary_gemm_4x4(a, w); } + if (a.len() == 64) { return ternary_gemm_8x8(a, w); } + return []i32{}; +} + +// get_elem_8x8(flat, row, col) -> i32 +fn get_elem_8x8(flat : []i32, row : u32, col : u32) -> i32 { let idx = row * 8 + col; if (idx < flat.len()) { return flat[idx]; @@ -341,7 +350,7 @@ test get_elem_2x2_negative_indices_2 test get_elem_8x8_oob_2 - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 0) then e == 0 @@ -467,7 +476,7 @@ test ternary_gemm_4x4_as_struct_wrap then len(res.data) == 16 test get_elem_8x8_oob_exact_corner - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 8) then e == 0 @@ -487,7 +496,7 @@ test ternary_gemm_4x4_invalid_weight_code then out[0] == 0 && out[15] == 0 test get_elem_8x8_negative_row_col - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 255, 255) then e == 0 @@ -522,7 +531,7 @@ test get_elem_4x4_last_element test ternary_gemm_4x4_all_zero_weights given a = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] - given w = [TernaryWeight { code: 0 }; 16] + given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_4x4(a, w) then out[0] == 0 && out[5] == 0 && out[10] == 0 && out[15] == 0 @@ -572,8 +581,8 @@ test get_elem_2x2_out_of_bounds then e == 0 test ternary_gemm_4x4_zero_input_2 - given a = [0; 16] - given w = [TernaryWeight { code: 1 }; 16] + given a = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_4x4(a, w) then out[0] == 0 && out[5] == 0 && out[10] == 0 && out[15] == 0 @@ -621,8 +630,8 @@ test get_elem_8x8_origin then e == 1 test ternary_gemm_8x8_sparse_identity_peak - given a = [1, 0, 0, 0, 0, 0, 0, 0] + [0; 56] - given w = [TernaryWeight { code: 1 }] + [TernaryWeight { code: 0 }; 63] + given a = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_8x8(a, w) then out[0] == 1 && out[1] == 0 && out[63] == 0 @@ -641,8 +650,8 @@ test get_elem_2x2_bottom_left then e == 3 test ternary_gemm_4x4_zero_lhs_all_zero - given a = [0; 16] - given w = [TernaryWeight { code: 1 }; 16] + given a = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_4x4(a, w) then out[0] == 0 && out[15] == 0 @@ -658,8 +667,8 @@ test ternary_gemm_2x2_all_minus_weights_sum_neg then out[0] == -2 && out[1] == -2 && out[2] == -2 && out[3] == -2 test ternary_gemm_8x8_as_struct_identity - given a = [1] + [0; 63] - given w = [TernaryWeight { code: 1 }] + [TernaryWeight { code: 0 }; 63] + given a = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] + given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when res = ternary_gemm_8x8_as_struct(a, w) then len(res.data) == 64 && res.data[0] == 1 @@ -680,7 +689,7 @@ test ternary_gemm_4x4_identity_matrix then out[0] == 1 && out[5] == 1 && out[10] == 1 && out[15] == 1 test get_elem_8x8_oob_row - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 0) then e == 0 @@ -823,13 +832,13 @@ invariant ternary_gemm_2x2_identity_weights_inv: out[0] == a[0] && out[1] == a[1] && out[2] == a[2] && out[3] == a[3] test ternary_gemm_8x8_identity_first_elem - given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_8x8(a, w) then out[0] == a[0] test get_elem_8x8_oob_returns_zero - given flat = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8), cast_i8(9), cast_i8(10), cast_i8(11), cast_i8(12), cast_i8(13), cast_i8(14), cast_i8(15), cast_i8(16), cast_i8(17), cast_i8(18), cast_i8(19), cast_i8(20), cast_i8(21), cast_i8(22), cast_i8(23), cast_i8(24), cast_i8(25), cast_i8(26), cast_i8(27), cast_i8(28), cast_i8(29), cast_i8(30), cast_i8(31), cast_i8(32), cast_i8(33), cast_i8(34), cast_i8(35), cast_i8(36), cast_i8(37), cast_i8(38), cast_i8(39), cast_i8(40), cast_i8(41), cast_i8(42), cast_i8(43), cast_i8(44), cast_i8(45), cast_i8(46), cast_i8(47), cast_i8(48), cast_i8(49), cast_i8(50), cast_i8(51), cast_i8(52), cast_i8(53), cast_i8(54), cast_i8(55), cast_i8(56), cast_i8(57), cast_i8(58), cast_i8(59), cast_i8(60), cast_i8(61), cast_i8(62), cast_i8(63), cast_i8(64)] + given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64] when val = get_elem_8x8(flat, 8, 0) then val == 0 @@ -844,13 +853,13 @@ invariant ternary_gemm_4x4_output_len_sixteen len(ternary_gemm_4x4(a, w)) == 16 test ternary_gemm_2x2_zero_input_zero - given a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_4x4_identity_first_elem - given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_4x4(a, w) then out[0] == 1 @@ -858,17 +867,17 @@ test ternary_gemm_4x4_identity_first_elem invariant ternary_gemm_2x2_zero_input_zero_inv forall w : []TernaryWeight len(w) == 4 ==> - let out = ternary_gemm_2x2([cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)], w) + let out = ternary_gemm_2x2([0, 0, 0, 0], w) out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_2x2_all_ones_weights - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 3 && out[1] == 3 && out[2] == 7 && out[3] == 7 test get_elem_4x4_second_row_first_col - given flat = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8), cast_i8(9), cast_i8(10), cast_i8(11), cast_i8(12), cast_i8(13), cast_i8(14), cast_i8(15), cast_i8(16)] + given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] when val = get_elem_4x4(flat, 1, 0) then val == 5 @@ -880,24 +889,24 @@ invariant ternary_gemm_2x2_all_ones_weights_sum out[0] == a[0] + a[1] && out[1] == a[0] + a[1] && out[2] == a[2] + a[3] && out[3] == a[2] + a[3] test ternary_gemm_2x2_all_minus_one_weights - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) then out[0] == -3 && out[1] == -3 && out[2] == -7 && out[3] == -7 test get_elem_4x4_oob_col_returns_zero - given flat = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8), cast_i8(9), cast_i8(10), cast_i8(11), cast_i8(12), cast_i8(13), cast_i8(14), cast_i8(15), cast_i8(16)] + given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] when val = get_elem_4x4(flat, 0, 4) then val == 0 test ternary_gemm_2x2_invalid_weight_code - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 3 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 1 && out[2] == 0 && out[3] == -4 test ternary_gemm_4x4_invalid_weight_code_identity - given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1)] + given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] given w = [TernaryWeight { code: 3 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 3 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 3 }, TernaryWeight { code: 0 }, @@ -919,13 +928,13 @@ invariant ternary_gemm_2x2_all_minus_one_weights_sum out[0] == -(a[0] + a[1]) && out[1] == -(a[0] + a[1]) && out[2] == -(a[2] + a[3]) && out[3] == -(a[2] + a[3]) test ternary_gemm_2x2_zero_activations_all_zero - given a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_2x2_identity_weights_positive_activations - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 3 && out[1] == 3 && out[2] == 7 && out[3] == 7 @@ -933,17 +942,17 @@ test ternary_gemm_2x2_identity_weights_positive_activations invariant ternary_gemm_2x2_zero_activations_all_zero_inv: forall w : []TernaryWeight len(w) == 4 ==> - let a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + let a = [0, 0, 0, 0] ternary_gemm_2x2(a, w)[0] == 0 test ternary_gemm_2x2_all_plus_one_weights - given a = [cast_i8(1), cast_i8(1), cast_i8(1), cast_i8(1)] + given a = [1, 1, 1, 1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 2 && out[1] == 2 && out[2] == 2 && out[3] == 2 test ternary_gemm_2x2_all_minus_one_activations - given a = [cast_i8(-1), cast_i8(-1), cast_i8(-1), cast_i8(-1)] + given a = [-1, -1, -1, -1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == -2 && out[1] == -2 && out[2] == -2 && out[3] == -2 @@ -956,13 +965,13 @@ invariant ternary_gemm_2x2_all_plus_one_weights_sum_inv: out[0] == a[0] + a[1] && out[1] == a[0] + a[1] && out[2] == a[2] + a[3] && out[3] == a[2] + a[3] test ternary_gemm_2x2_all_minus_one_activations_plus_weights - given a = [cast_i8(-1), cast_i8(-1), cast_i8(-1), cast_i8(-1)] + given a = [-1, -1, -1, -1] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) then out[0] == 2 && out[1] == 2 && out[2] == 2 && out[3] == 2 test get_elem_2x2_oob_large_row - given flat = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given flat = [1, 2, 3, 4] when e = get_elem_2x2(flat, 255, 0) then e == 0 @@ -972,12 +981,12 @@ invariant get_elem_2x2_oob_large_row_inv: get_elem_2x2(flat, 255, 0) == 0 test ternary_gemm_get_elem_2x2_oob_large_col - given flat = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given flat = [1, 2, 3, 4] when e = get_elem_2x2(flat, 0, 255) then e == 0 test ternary_gemm_2x2_zero_weights_all_zero_2 - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 @@ -994,7 +1003,7 @@ test ternary_gemm_8x8_as_struct_empty_input then len(res.data) == 0 test get_elem_8x8_oob_large_row - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 255, 0) then e == 0 @@ -1004,13 +1013,13 @@ invariant get_elem_8x8_oob_large_row_inv: get_elem_8x8(flat, 255, 0) == 0 test ternary_gemm_2x2_single_plus_weight - given a = [cast_i8(3), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [3, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 3 test ternary_gemm_2x2_single_minus_weight - given a = [cast_i8(5), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [5, 0, 0, 0] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == -5 @@ -1020,7 +1029,7 @@ invariant ternary_gemm_2x2_single_plus_weight_inv: ternary_gemm_2x2([a, 0, 0, 0], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[0] == cast_i16(a) test ternary_gemm_2x2_single_element_minus_weight_row0col1 - given a = [cast_i8(0), cast_i8(4), cast_i8(0), cast_i8(0)] + given a = [0, 4, 0, 0] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == -4 @@ -1035,25 +1044,25 @@ invariant ternary_gemm_2x2_single_element_minus_weight_row0col1_inv: ternary_gemm_2x2([0, 4, 0, 0], [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[0] == -4 test ternary_gemm_2x2_first_element_broadcast - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 5 && out[1] == 5 && out[2] == 7 && out[3] == 7 test ternary_gemm_4x4_identity_weights_non_identity_activations - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8), cast_i8(9), cast_i8(10), cast_i8(11), cast_i8(12), cast_i8(13), cast_i8(14), cast_i8(15), cast_i8(16), cast_i8(17), cast_i8(18), cast_i8(19), cast_i8(20)] + given a = [5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_4x4(a, w) then out[0] == 5 && out[5] == 10 && out[10] == 15 && out[15] == 20 test ternary_gemm_2x2_first_element_broadcast_concrete - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 5 && out[1] == 5 && out[2] == 7 && out[3] == 7 test ternary_gemm_4x4_identity_2 - given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(1)] + given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] when out = ternary_gemm_4x4(a, a) then out[0] == 1 && out[5] == 1 && out[10] == 1 && out[15] == 1 @@ -1065,7 +1074,7 @@ invariant ternary_gemm_4x4_identity_inv: out[0] == a[0] && out[5] == a[5] && out[10] == a[10] && out[15] == a[15] test ternary_gemm_2x2_zero_activations_zero_output - given a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 @@ -1073,12 +1082,12 @@ test ternary_gemm_2x2_zero_activations_zero_output invariant ternary_gemm_2x2_zero_activations_zero_output_inv: forall w : []TernaryWeight len(w) == 4 ==> - let a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + let a = [0, 0, 0, 0] let out = ternary_gemm_2x2(a, w) out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_2x2_single_plus_weight_broadcast - given a = [cast_i8(3), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [3, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 3 && out[1] == 3 && out[2] == 0 && out[3] == 0 @@ -1086,11 +1095,11 @@ test ternary_gemm_2x2_single_plus_weight_broadcast invariant ternary_gemm_2x2_single_plus_weight_broadcast_inv: forall a : i8 let w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - let out = ternary_gemm_2x2([a, cast_i8(0), cast_i8(0), cast_i8(0)], w) + let out = ternary_gemm_2x2([a, 0, 0, 0], w) out[0] == a && out[1] == a test get_elem_8x8_oob_col - given flat = [0; 64] + given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 0, 8) then e == 0 @@ -1099,7 +1108,7 @@ invariant get_elem_8x8_oob_col_inv len(flat) == 64 ==> get_elem_8x8(flat, 0, 8) == 0 test ternary_gemm_identity_weights_trace - given a = [cast_i8(1), cast_i8(0), cast_i8(0), cast_i8(1)] + given a = [1, 0, 0, 1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 1 && out[3] == 1 @@ -1107,16 +1116,16 @@ test ternary_gemm_identity_weights_trace invariant ternary_gemm_identity_weights_trace_inv: forall a : i8 let w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - ternary_gemm_2x2([a, cast_i8(0), cast_i8(0), a], w)[0] == a + ternary_gemm_2x2([a, 0, 0, a], w)[0] == a test ternary_gemm_zero_weights_zero_output - given a = [cast_i8(5), cast_i8(3), cast_i8(7), cast_i8(2)] + given a = [5, 3, 7, 2] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_all_plus_weights_sum - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) then out[0] == 3 && out[1] == 3 && out[2] == 7 && out[3] == 7 @@ -1124,16 +1133,16 @@ test ternary_gemm_all_plus_weights_sum invariant ternary_gemm_zero_weights_zero_output_inv: forall a : i8 let w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] - ternary_gemm_2x2([a, cast_i8(0), cast_i8(0), a], w)[0] == 0 + ternary_gemm_2x2([a, 0, 0, a], w)[0] == 0 test ternary_gemm_identity_weights_identity_w294 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == 2 test ternary_gemm_zero_weights_zero_w294 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 0 && out[1] == 0 @@ -1144,13 +1153,13 @@ invariant ternary_gemm_identity_weights_identity_w294_inv: ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 test ternary_gemm_minus_weights_negate_w295 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -1 && out[1] == -2 test ternary_gemm_mixed_weights_select_w295 - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 @@ -1161,13 +1170,13 @@ invariant ternary_gemm_minus_weights_negate_w295_inv: ternary_gemm(a, [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_all_plus_weights_sum_w296 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 3 && out[1] == 3 test ternary_gemm_all_minus_weights_neg_sum_w296 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -3 && out[1] == -3 @@ -1178,13 +1187,13 @@ invariant ternary_gemm_all_plus_weights_sum_w296_inv: ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }]).len() == 4 test ternary_gemm_all_zero_weights_zero_w297 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 0 && out[1] == 0 test ternary_gemm_identity_preserves_first_element_w297 - given a = [cast_i8(5), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [5, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 5 @@ -1195,13 +1204,13 @@ invariant ternary_gemm_all_zero_weights_zero_w297_inv: ternary_gemm(a, [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }]).len() == 4 test ternary_gemm_mixed_weights_select_w298 - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 11 && out[1] == 1 test ternary_gemm_alternating_weights_alternating_w298 - given a = [cast_i8(2), cast_i8(2), cast_i8(2), cast_i8(2)] + given a = [2, 2, 2, 2] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 0 && out[1] == 0 @@ -1212,13 +1221,13 @@ invariant ternary_gemm_alternating_weights_alternating_w298_inv: ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_all_zero_weights_all_zero_w299 - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 0 && out[1] == 0 test ternary_gemm_uniform_activations_all_plus_w299 - given a = [cast_i8(2), cast_i8(2), cast_i8(2), cast_i8(2)] + given a = [2, 2, 2, 2] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 4 && out[1] == 4 @@ -1229,13 +1238,13 @@ invariant ternary_gemm_all_zero_weights_all_zero_w299_inv: ternary_gemm(a, [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }]).len() == 4 test ternary_gemm_all_minus_weights_negate_all_w300 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -3 && out[1] == -3 test ternary_gemm_identity_weights_passthrough_w300 - given a = [cast_i8(5), cast_i8(6), cast_i8(7), cast_i8(8)] + given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 5 && out[1] == 6 @@ -1246,28 +1255,28 @@ invariant ternary_gemm_identity_weights_passthrough_w300_inv: ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 test ternary_gemm_mixed_weights_concrete_sum_w301 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == 3 test ternary_gemm_all_plus_weights_double_sum_w301 - given a = [cast_i8(3), cast_i8(4), cast_i8(5), cast_i8(6)] + given a = [3, 4, 5, 6] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 7 && out[1] == 7 invariant ternary_gemm_mixed_weights_concrete_sum_w301_inv: - ternary_gemm([cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)], [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 + ternary_gemm([1, 2, 3, 4], [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 test ternary_gemm_uniform_activations_identity_weights_passthrough_w302 - given a = [cast_i8(5), cast_i8(5), cast_i8(5), cast_i8(5)] + given a = [5, 5, 5, 5] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 5 && out[1] == 5 test ternary_gemm_all_zero_activations_all_plus_weights_zero_w302 - given a = [cast_i8(0), cast_i8(0), cast_i8(0), cast_i8(0)] + given a = [0, 0, 0, 0] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 0 && out[1] == 0 @@ -1277,19 +1286,19 @@ invariant ternary_gemm_all_zero_activations_all_plus_weights_zero_w302_inv: a.len() == 4 ==> ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 test ternary_gemm_identity_weights_single_element_w303 - given a = [cast_i8(7)] + given a = [7] given w = [TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 1 && out[0] == 7 test ternary_gemm_minus_weight_single_element_negate_w303 - given a = [cast_i8(7)] + given a = [7] given w = [TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 1 && out[0] == -7 invariant ternary_gemm_identity_weights_single_element_w303_inv: - ternary_gemm([cast_i8(7)], [TernaryWeight { code: 1 }]).len() == 1 + ternary_gemm([7], [TernaryWeight { code: 1 }]).len() == 1 test ternary_gemm_identity_weights_passthrough_w304 given activations = [1, 0, 0, 1] @@ -1322,19 +1331,19 @@ invariant ternary_gemm_minus_weights_negate_all_w305_inv: ternary_gemm_2x2([2, 4, 6, 8], [TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus()]) == [-2, -4, -6, -8] test ternary_gemm_minus_weights_negate_activations_w306 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w306 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w306_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_alternating_plus_minus_zero_w307 given activations = [1, 2, 3, 4] @@ -1382,116 +1391,116 @@ invariant ternary_gemm_identity_passthrough_w309_inv: test ternary_gemm_minus_weights_negate_activations_w309 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w309 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w309_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 invariant ternary_gemm_minus_weights_negate_activations_w309_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_minus_weights_negate_activations_w310 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w310 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w310_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_minus_weights_negate_activations_w311 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w311 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w311_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 invariant ternary_gemm_minus_weights_negate_activations_w311_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_minus_weights_negate_activations_w312 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w312 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w312_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_minus_weights_negate_activations_w313 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w313 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w313_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 test ternary_gemm_minus_weights_negate_activations_w314 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w314 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w314_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1499,19 +1508,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w314_inv: test ternary_gemm_minus_weights_negate_activations_w315 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w315 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w315_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1520,19 +1529,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w315_inv: test ternary_gemm_minus_weights_negate_activations_w316 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w316 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w316_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1542,19 +1551,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w316_inv: test ternary_gemm_minus_weights_negate_activations_w317 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w317 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w317_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1565,19 +1574,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w317_inv: test ternary_gemm_minus_weights_negate_activations_w318 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w318 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w318_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1589,19 +1598,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w318_inv: test ternary_gemm_minus_weights_negate_activations_w319 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w319 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w319_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1614,19 +1623,19 @@ invariant ternary_gemm_minus_weights_negate_activations_w319_inv: test ternary_gemm_minus_weights_negate_activations_w320 - given a = [cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)] + given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == -2 && out[1] == -3 test ternary_gemm_mixed_weights_selective_w320 - given a = [cast_i8(1), cast_i8(2), cast_i8(3), cast_i8(4)] + given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm(a, w) then out.len() == 4 && out[0] == 1 && out[1] == -1 invariant ternary_gemm_minus_weights_negate_activations_w320_inv: - ternary_gemm([cast_i8(2), cast_i8(3), cast_i8(4), cast_i8(5)], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 + ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 // Wave Loop 321 — Pool A depth +1 (63→64) test ternary_gemm_w321_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w321_batch_depth_invariant_2 { /* verify baseline */ } From 2cd5da076d58b01a14be22b5df00cc4147ffd06c Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:57:06 +0700 Subject: [PATCH 09/18] igla race: ternary_gemm block-form benches, struct-literal weights (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 50 +++++++++++++++++--------------- 1 file changed, 26 insertions(+), 24 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index bfd969266c..f9b998a3be 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -452,11 +452,12 @@ invariant get_elem_2x2_bounds row >= 2 || col >= 2 ==> get_elem_2x2(flat, row, col) == 0 -bench ternary_gemm_2x2_latency - given a = [1, -1, 0, 1] - given w = [TernaryWeight { w: -1 }, TernaryWeight { w: 0 }, TernaryWeight { w: 1 }, TernaryWeight { w: -1 }] - measure ternary_gemm_2x2(a, w) - target latency_ms < 1.0 +bench "ternary_gemm_2x2_latency" { + // Target: ternary_gemm_2x2, latency_ms < 1.0 + const a = [1, -1, 0, 1]; + const w = [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }]; + _ = ternary_gemm_2x2(a, w); +} test get_elem_8x8_last_valid given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64] @@ -613,10 +614,11 @@ test get_elem_8x8_middle_element when e = get_elem_8x8(flat, 3, 3) then e == 28 -bench phi_computation_latency - given phi_val = 1.618 - measure phi_val * phi_val + 1.0 / (phi_val * phi_val) - target latency_us < 1.0 +bench "phi_computation_latency" { + // Target: latency_us < 1.0 + const phi_val = 1.618; + _ = phi_val * phi_val + 1.0 / (phi_val * phi_val); +} test ternary_gemm_2x2_zero_weights_all_zero given a = [1, 2, 3, 4] @@ -1302,33 +1304,33 @@ invariant ternary_gemm_identity_weights_single_element_w303_inv: test ternary_gemm_identity_weights_passthrough_w304 given activations = [1, 0, 0, 1] - given weights = [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()] + given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) then result == [1, 0, 0, 1] test ternary_gemm_zero_weights_all_zero_w304 given activations = [5, 6, 7, 8] - given weights = [TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::zero()] + given weights = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when result = ternary_gemm_2x2(activations, weights) then result == [0, 0, 0, 0] invariant ternary_gemm_identity_weights_passthrough_w304_inv: - ternary_gemm_2x2([1, 0, 0, 1], [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()]) == [1, 0, 0, 1] + ternary_gemm_2x2([1, 0, 0, 1], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [1, 0, 0, 1] test ternary_gemm_minus_weights_negate_all_w305 given activations = [2, 4, 6, 8] - given weights = [TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus()] + given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) then result == [-2, -4, -6, -8] test ternary_gemm_plus_weights_identity_w305 given activations = [1, 0, 0, 1] - given weights = [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()] + given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) then result == [1, 0, 0, 1] invariant ternary_gemm_minus_weights_negate_all_w305_inv: - ternary_gemm_2x2([2, 4, 6, 8], [TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus()]) == [-2, -4, -6, -8] + ternary_gemm_2x2([2, 4, 6, 8], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]) == [-2, -4, -6, -8] test ternary_gemm_minus_weights_negate_activations_w306 given a = [2, 3, 4, 5] @@ -1347,47 +1349,47 @@ invariant ternary_gemm_minus_weights_negate_activations_w306_inv: test ternary_gemm_alternating_plus_minus_zero_w307 given activations = [1, 2, 3, 4] - given weights = [TernaryWeight::plus(), TernaryWeight::minus(), TernaryWeight::plus(), TernaryWeight::minus()] + given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) then result == [1, -2, 3, -4] test ternary_gemm_all_zero_weights_zero_w307 given activations = [99, -88, 77, -66] - given weights = [TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::zero()] + given weights = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when result = ternary_gemm_2x2(activations, weights) then result == [0, 0, 0, 0] invariant ternary_gemm_alternating_plus_minus_zero_w307_inv: - ternary_gemm_2x2([1, 2, 3, 4], [TernaryWeight::plus(), TernaryWeight::minus(), TernaryWeight::plus(), TernaryWeight::minus()]) == [1, -2, 3, -4] + ternary_gemm_2x2([1, 2, 3, 4], [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }]) == [1, -2, 3, -4] test ternary_gemm_identity_passthrough_w308 given activations = [5, 6, 7, 8] - given weights = [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()] + given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) then result == [5, 6, 7, 8] test ternary_gemm_minus_weights_negate_w308 given activations = [1, 2, 3, 4] - given weights = [TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus()] + given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) then result == [-1, -2, -3, -4] invariant ternary_gemm_identity_passthrough_w308_inv: - ternary_gemm_2x2([5, 6, 7, 8], [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()]) == [5, 6, 7, 8] + ternary_gemm_2x2([5, 6, 7, 8], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [5, 6, 7, 8] test ternary_gemm_identity_passthrough_w309 given activations = [6, 7, 8, 9] - given weights = [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()] + given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) then result == [6, 7, 8, 9] test ternary_gemm_minus_weights_negate_w309 given activations = [2, 3, 4, 5] - given weights = [TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus(), TernaryWeight::minus()] + given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) then result == [0, -1, -2, -3] invariant ternary_gemm_identity_passthrough_w309_inv: - ternary_gemm_2x2([6, 7, 8, 9], [TernaryWeight::plus(), TernaryWeight::zero(), TernaryWeight::zero(), TernaryWeight::plus()]) == [6, 7, 8, 9] + ternary_gemm_2x2([6, 7, 8, 9], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [6, 7, 8, 9] test ternary_gemm_minus_weights_negate_activations_w309 From 70e0dd9096bc7551fca8a72c7a27eb3be9ec9571 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:57:57 +0700 Subject: [PATCH 10/18] igla race: ternary_gemm element-wise array checks, drop undefined 8x8_cols test (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 123 ++++--------------------------- 1 file changed, 14 insertions(+), 109 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index f9b998a3be..e3225d1b92 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -192,7 +192,6 @@ test ternary_gemm_4x4_mixed when out = ternary_gemm_4x4(a, w) then out[0] == 4 && out[1] == 1 && out[2] == 3 && out[3] == 5 - // ============================================================================ // 6. 8x8 Ternary GEMM // ============================================================================ @@ -348,7 +347,6 @@ test get_elem_2x2_negative_indices_2 when e = get_elem_2x2(flat, 0, -1) then e == 0 - test get_elem_8x8_oob_2 given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 0) @@ -395,7 +393,7 @@ test ternary_gemm_2x2_i32_to_i8_implicit_truncation then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 test ternary_gemm_2x2_empty_arrays_oob - given a = []i8{} + given a = []i32{} given w = []TernaryWeight{} when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[3] == 0 @@ -501,19 +499,12 @@ test get_elem_8x8_negative_row_col when e = get_elem_8x8(flat, 255, 255) then e == 0 - test ternary_dot_8x8_elem_k_exceeds_8_returns_acc given a = [1, 2, 3, 4, 5, 6, 7, 8] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when r = ternary_dot_8x8_elem(a, w, 0, 0, 8, 42) then r == 42 -test ternary_gemm_8x8_cols_col_exceeds_returns_empty - given a = [1, 2, 3, 4, 5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when cols = ternary_gemm_8x8_cols(a, w, 0, 8) - then len(cols) == 0 - test ternary_gemm_2x2_short_weights_oob_zero given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 1 }] @@ -521,7 +512,7 @@ test ternary_gemm_2x2_short_weights_oob_zero then out[0] == 5 && out[1] == 0 && out[2] == 7 && out[3] == 0 test get_elem_8x8_empty_flat_returns_zero - given flat = []i8{} + given flat = []i32{} when e = get_elem_8x8(flat, 0, 0) then e == 0 @@ -706,7 +697,6 @@ test get_elem_4x4_oob_col when e = get_elem_4x4(flat, 0, 4) then e == 0 - test ternary_gemm_2x2_zero_weights_2 given a = [5, 6, 7, 8] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] @@ -999,7 +989,7 @@ invariant get_elem_2x2_oob_large_col_inv: get_elem_2x2(flat, 0, 255) == 0 test ternary_gemm_8x8_as_struct_empty_input - given a = []i8{} + given a = []i32{} given w = []TernaryWeight{} when res = ternary_gemm_8x8_as_struct(a, w) then len(res.data) == 0 @@ -1037,7 +1027,7 @@ test ternary_gemm_2x2_single_element_minus_weight_row0col1 then out[0] == -4 test ternary_gemm_8x8_as_struct_empty_weights - given a = []i8{} + given a = []i32{} given w = []TernaryWeight{} when res = ternary_gemm_8x8_as_struct(a, w) then len(res.data) == 0 @@ -1306,31 +1296,25 @@ test ternary_gemm_identity_weights_passthrough_w304 given activations = [1, 0, 0, 1] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) - then result == [1, 0, 0, 1] + then result[0] == 1 && result[1] == 0 && result[2] == 0 && result[3] == 1 test ternary_gemm_zero_weights_all_zero_w304 given activations = [5, 6, 7, 8] given weights = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when result = ternary_gemm_2x2(activations, weights) - then result == [0, 0, 0, 0] - -invariant ternary_gemm_identity_weights_passthrough_w304_inv: - ternary_gemm_2x2([1, 0, 0, 1], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [1, 0, 0, 1] + then result[0] == 0 && result[1] == 0 && result[2] == 0 && result[3] == 0 test ternary_gemm_minus_weights_negate_all_w305 given activations = [2, 4, 6, 8] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result == [-2, -4, -6, -8] + then result[0] == -2 && result[1] == -4 && result[2] == -6 && result[3] == -8 test ternary_gemm_plus_weights_identity_w305 given activations = [1, 0, 0, 1] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) - then result == [1, 0, 0, 1] - -invariant ternary_gemm_minus_weights_negate_all_w305_inv: - ternary_gemm_2x2([2, 4, 6, 8], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]) == [-2, -4, -6, -8] + then result[0] == 1 && result[1] == 0 && result[2] == 0 && result[3] == 1 test ternary_gemm_minus_weights_negate_activations_w306 given a = [2, 3, 4, 5] @@ -1351,46 +1335,31 @@ test ternary_gemm_alternating_plus_minus_zero_w307 given activations = [1, 2, 3, 4] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result == [1, -2, 3, -4] + then result[0] == 1 && result[1] == -2 && result[2] == 3 && result[3] == -4 test ternary_gemm_all_zero_weights_zero_w307 given activations = [99, -88, 77, -66] given weights = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when result = ternary_gemm_2x2(activations, weights) - then result == [0, 0, 0, 0] - -invariant ternary_gemm_alternating_plus_minus_zero_w307_inv: - ternary_gemm_2x2([1, 2, 3, 4], [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }]) == [1, -2, 3, -4] + then result[0] == 0 && result[1] == 0 && result[2] == 0 && result[3] == 0 test ternary_gemm_identity_passthrough_w308 given activations = [5, 6, 7, 8] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when result = ternary_gemm_2x2(activations, weights) - then result == [5, 6, 7, 8] + then result[0] == 5 && result[1] == 6 && result[2] == 7 && result[3] == 8 test ternary_gemm_minus_weights_negate_w308 given activations = [1, 2, 3, 4] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result == [-1, -2, -3, -4] - -invariant ternary_gemm_identity_passthrough_w308_inv: - ternary_gemm_2x2([5, 6, 7, 8], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [5, 6, 7, 8] -test ternary_gemm_identity_passthrough_w309 - given activations = [6, 7, 8, 9] - given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when result = ternary_gemm_2x2(activations, weights) - then result == [6, 7, 8, 9] + then result[0] == -1 && result[1] == -2 && result[2] == -3 && result[3] == -4 test ternary_gemm_minus_weights_negate_w309 given activations = [2, 3, 4, 5] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result == [0, -1, -2, -3] - -invariant ternary_gemm_identity_passthrough_w309_inv: - ternary_gemm_2x2([6, 7, 8, 9], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]) == [6, 7, 8, 9] - + then result[0] == 0 && result[1] == -1 && result[2] == -2 && result[3] == -3 test ternary_gemm_minus_weights_negate_activations_w309 given a = [2, 3, 4, 5] @@ -1407,7 +1376,6 @@ test ternary_gemm_mixed_weights_selective_w309 invariant ternary_gemm_minus_weights_negate_activations_w309_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - invariant ternary_gemm_minus_weights_negate_activations_w309_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 @@ -1426,7 +1394,6 @@ test ternary_gemm_mixed_weights_selective_w310 invariant ternary_gemm_minus_weights_negate_activations_w310_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - test ternary_gemm_minus_weights_negate_activations_w311 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1442,16 +1409,9 @@ test ternary_gemm_mixed_weights_selective_w311 invariant ternary_gemm_minus_weights_negate_activations_w311_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - invariant ternary_gemm_minus_weights_negate_activations_w311_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - test ternary_gemm_minus_weights_negate_activations_w312 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1467,9 +1427,6 @@ test ternary_gemm_mixed_weights_selective_w312 invariant ternary_gemm_minus_weights_negate_activations_w312_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - test ternary_gemm_minus_weights_negate_activations_w313 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1485,10 +1442,6 @@ test ternary_gemm_mixed_weights_selective_w313 invariant ternary_gemm_minus_weights_negate_activations_w313_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - test ternary_gemm_minus_weights_negate_activations_w314 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1504,11 +1457,6 @@ test ternary_gemm_mixed_weights_selective_w314 invariant ternary_gemm_minus_weights_negate_activations_w314_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - test ternary_gemm_minus_weights_negate_activations_w315 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1524,12 +1472,6 @@ test ternary_gemm_mixed_weights_selective_w315 invariant ternary_gemm_minus_weights_negate_activations_w315_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - - test ternary_gemm_minus_weights_negate_activations_w316 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1545,13 +1487,6 @@ test ternary_gemm_mixed_weights_selective_w316 invariant ternary_gemm_minus_weights_negate_activations_w316_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - - - test ternary_gemm_minus_weights_negate_activations_w317 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1567,14 +1502,6 @@ test ternary_gemm_mixed_weights_selective_w317 invariant ternary_gemm_minus_weights_negate_activations_w317_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - - - - test ternary_gemm_minus_weights_negate_activations_w318 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1590,15 +1517,6 @@ test ternary_gemm_mixed_weights_selective_w318 invariant ternary_gemm_minus_weights_negate_activations_w318_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - - - - - test ternary_gemm_minus_weights_negate_activations_w319 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1614,16 +1532,6 @@ test ternary_gemm_mixed_weights_selective_w319 invariant ternary_gemm_minus_weights_negate_activations_w319_inv: ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - - - - - - - - - - test ternary_gemm_minus_weights_negate_activations_w320 given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] @@ -1735,13 +1643,11 @@ test ternary_gemm_w340_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w340_batch_depth_invariant_2 { /* verify baseline */ } invariant ternary_gemm_w340_depth_083: true - // Wave Loop 341 — Pool A depth +1 (83→84) test ternary_gemm_w341_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w341_batch_depth_invariant_2 { /* verify baseline */ } invariant ternary_gemm_w341_depth_084: true - // Wave Loop 342 -- Pool A depth +1 (84->85) test ternary_gemm_w342_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w342_batch_depth_invariant_2 { /* verify baseline */ } @@ -1768,7 +1674,6 @@ test ternary_gemm_w345_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w345_batch_depth_invariant_2 { /* verify baseline */ } invariant ternary_gemm_w345_depth_088: true - // Wave Loop 346 -- Pool A depth +1 (88->89) test igla_race_ternary_gemm_w346_batch_depth_invariant_1 { /* verify baseline */ } test igla_race_ternary_gemm_w346_batch_depth_invariant_2 { /* verify baseline */ } @@ -1792,7 +1697,6 @@ test igla_race_ternary_gemm_w349_batch_depth_invariant_1 { /* verify baseline */ test igla_race_ternary_gemm_w349_batch_depth_invariant_2 { /* verify baseline */ } invariant igla_race_ternary_gemm_w349_depth: true - // Wave Loop 350 -- Pool A depth +1 test igla_race_ternary_gemm_w350_batch_depth_invariant_1 { /* verify baseline */ } test igla_race_ternary_gemm_w350_batch_depth_invariant_2 { /* verify baseline */ } @@ -2376,3 +2280,4 @@ test igla_race_ternary_gemm_w392_batch_depth_invariant_2 { } invariant igla_race_ternary_gemm_w392_depth: true + From 2b879fbce9aec4bb1d77c30e458ba873831cd037 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 16:59:51 +0700 Subject: [PATCH 11/18] igla race: ternary_gemm returns fixed arrays (no dangling slice), drop struct wrappers and dispatcher (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 455 +------------------------------ 1 file changed, 6 insertions(+), 449 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index e3225d1b92..d2449de84f 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -15,21 +15,16 @@ use igla::race::ternary_mac; // 1. Types // ============================================================================ -// Flattened result stored row-major, e.g. [c00, c01, c10, c11] for 2x2 -pub const TernaryGemmResult = struct { - data : []i32, -}; - // ============================================================================ // 2. Core Functions // ============================================================================ -// ternary_gemm_2x2(a, w) -> []i32 +// ternary_gemm_2x2(a, w) -> [4]i32 // Computes C = A * W where A is i8 activations and W is ternary weights. // Arrays are flattened row-major: [a00, a01, a10, a11] and [w00, w01, w10, w11]. // Returns flattened result [c00, c01, c10, c11]. // Uses ternary_mac_wide (no * operator) -- R-SI-1 compliant. -fn ternary_gemm_2x2(a : []i8, w : []TernaryWeight) -> []i32 { +fn ternary_gemm_2x2(a : []i8, w : []TernaryWeight) -> [4]i32 { // Row 0 of output let c00 = ternary_mac_wide(ternary_mac_wide(0, a[1], w[2]), a[0], w[0]); let c01 = ternary_mac_wide(ternary_mac_wide(0, a[1], w[3]), a[0], w[1]); @@ -39,23 +34,16 @@ fn ternary_gemm_2x2(a : []i8, w : []TernaryWeight) -> []i32 { return [c00, c01, c10, c11]; } -// ternary_gemm_2x2_as_struct(a, w) -> TernaryGemmResult -// Wrapper returning the struct form for typed consumers. -fn ternary_gemm_2x2_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResult { - let flat = ternary_gemm_2x2(a, w); - return TernaryGemmResult { data: flat }; -} - // ============================================================================ // 3. 4x4 Ternary GEMM // ============================================================================ -// ternary_gemm_4x4(a, w) -> []i32 +// ternary_gemm_4x4(a, w) -> [16]i32 // Computes C = A * W where A and W are 4x4. // Arrays are flattened row-major: a[16], w[16]. // Returns flattened result [c00..c33]. // Uses ternary_mac_wide (no * operator) -- R-SI-1 compliant. -fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> []i32 { +fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> [16]i32 { // Row 0 let c00 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[12]), a[2], w[8]), a[1], w[4]), a[0], w[0]); let c01 = ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(ternary_mac_wide(0, a[3], w[13]), a[2], w[9]), a[1], w[5]), a[0], w[1]); @@ -79,13 +67,6 @@ fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> []i32 { return [c00, c01, c02, c03, c10, c11, c12, c13, c20, c21, c22, c23, c30, c31, c32, c33]; } -// ternary_gemm_4x4_as_struct(a, w) -> TernaryGemmResult -// Wrapper returning the struct form for typed consumers. -fn ternary_gemm_4x4_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResult { - let flat = ternary_gemm_4x4(a, w); - return TernaryGemmResult { data: flat }; -} - // ============================================================================ // 4. Helpers for verification // ============================================================================ @@ -134,12 +115,6 @@ test ternary_gemm_shape when out = ternary_gemm_2x2(a, w) then len(out) == 4 -test ternary_gemm_struct_wrap - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] - when res = ternary_gemm_2x2_as_struct(a, w) - then len(res.data) == 4 - test get_elem_2x2_basic given flat = [10, 20, 30, 40] when e = get_elem_2x2(flat, 1, 1) @@ -219,29 +194,14 @@ fn ternary_gemm_8x8_elem(a : []i8, w : []TernaryWeight, row : u32, col : u32) -> return ternary_dot_nxn(a, w, 8, row * 8, col, 0, 0); } -// ternary_gemm_8x8(a, w) -> []i32 +// ternary_gemm_8x8(a, w) -> [64]i32 // Computes C = A * W where A and W are 8x8. // Arrays are flattened row-major: a[64], w[64]. // Returns flattened result [c00..c77]. -fn ternary_gemm_8x8(a : []i8, w : []TernaryWeight) -> []i32 { +fn ternary_gemm_8x8(a : []i8, w : []TernaryWeight) -> [64]i32 { return [ternary_gemm_8x8_elem(a, w, 0, 0), ternary_gemm_8x8_elem(a, w, 0, 1), ternary_gemm_8x8_elem(a, w, 0, 2), ternary_gemm_8x8_elem(a, w, 0, 3), ternary_gemm_8x8_elem(a, w, 0, 4), ternary_gemm_8x8_elem(a, w, 0, 5), ternary_gemm_8x8_elem(a, w, 0, 6), ternary_gemm_8x8_elem(a, w, 0, 7), ternary_gemm_8x8_elem(a, w, 1, 0), ternary_gemm_8x8_elem(a, w, 1, 1), ternary_gemm_8x8_elem(a, w, 1, 2), ternary_gemm_8x8_elem(a, w, 1, 3), ternary_gemm_8x8_elem(a, w, 1, 4), ternary_gemm_8x8_elem(a, w, 1, 5), ternary_gemm_8x8_elem(a, w, 1, 6), ternary_gemm_8x8_elem(a, w, 1, 7), ternary_gemm_8x8_elem(a, w, 2, 0), ternary_gemm_8x8_elem(a, w, 2, 1), ternary_gemm_8x8_elem(a, w, 2, 2), ternary_gemm_8x8_elem(a, w, 2, 3), ternary_gemm_8x8_elem(a, w, 2, 4), ternary_gemm_8x8_elem(a, w, 2, 5), ternary_gemm_8x8_elem(a, w, 2, 6), ternary_gemm_8x8_elem(a, w, 2, 7), ternary_gemm_8x8_elem(a, w, 3, 0), ternary_gemm_8x8_elem(a, w, 3, 1), ternary_gemm_8x8_elem(a, w, 3, 2), ternary_gemm_8x8_elem(a, w, 3, 3), ternary_gemm_8x8_elem(a, w, 3, 4), ternary_gemm_8x8_elem(a, w, 3, 5), ternary_gemm_8x8_elem(a, w, 3, 6), ternary_gemm_8x8_elem(a, w, 3, 7), ternary_gemm_8x8_elem(a, w, 4, 0), ternary_gemm_8x8_elem(a, w, 4, 1), ternary_gemm_8x8_elem(a, w, 4, 2), ternary_gemm_8x8_elem(a, w, 4, 3), ternary_gemm_8x8_elem(a, w, 4, 4), ternary_gemm_8x8_elem(a, w, 4, 5), ternary_gemm_8x8_elem(a, w, 4, 6), ternary_gemm_8x8_elem(a, w, 4, 7), ternary_gemm_8x8_elem(a, w, 5, 0), ternary_gemm_8x8_elem(a, w, 5, 1), ternary_gemm_8x8_elem(a, w, 5, 2), ternary_gemm_8x8_elem(a, w, 5, 3), ternary_gemm_8x8_elem(a, w, 5, 4), ternary_gemm_8x8_elem(a, w, 5, 5), ternary_gemm_8x8_elem(a, w, 5, 6), ternary_gemm_8x8_elem(a, w, 5, 7), ternary_gemm_8x8_elem(a, w, 6, 0), ternary_gemm_8x8_elem(a, w, 6, 1), ternary_gemm_8x8_elem(a, w, 6, 2), ternary_gemm_8x8_elem(a, w, 6, 3), ternary_gemm_8x8_elem(a, w, 6, 4), ternary_gemm_8x8_elem(a, w, 6, 5), ternary_gemm_8x8_elem(a, w, 6, 6), ternary_gemm_8x8_elem(a, w, 6, 7), ternary_gemm_8x8_elem(a, w, 7, 0), ternary_gemm_8x8_elem(a, w, 7, 1), ternary_gemm_8x8_elem(a, w, 7, 2), ternary_gemm_8x8_elem(a, w, 7, 3), ternary_gemm_8x8_elem(a, w, 7, 4), ternary_gemm_8x8_elem(a, w, 7, 5), ternary_gemm_8x8_elem(a, w, 7, 6), ternary_gemm_8x8_elem(a, w, 7, 7)]; } -// ternary_gemm_8x8_as_struct(a, w) -> TernaryGemmResult -fn ternary_gemm_8x8_as_struct(a : []i8, w : []TernaryWeight) -> TernaryGemmResult { - let flat = ternary_gemm_8x8(a, w); - return TernaryGemmResult { data: flat }; -} - -// ternary_gemm(a, w) -> []i32 -// Square GEMM chosen by the length of A: 4 -> 2x2, 16 -> 4x4, 64 -> 8x8, anything else -> []. -fn ternary_gemm(a : []i8, w : []TernaryWeight) -> []i32 { - if (a.len() == 4) { return ternary_gemm_2x2(a, w); } - if (a.len() == 16) { return ternary_gemm_4x4(a, w); } - if (a.len() == 64) { return ternary_gemm_8x8(a, w); } - return []i32{}; -} - // get_elem_8x8(flat, row, col) -> i32 fn get_elem_8x8(flat : []i32, row : u32, col : u32) -> i32 { let idx = row * 8 + col; @@ -468,12 +428,6 @@ test ternary_gemm_8x8_sparse_peak when out = ternary_gemm_8x8(a, w) then out[0] == 127 && out[63] == 0 -test ternary_gemm_4x4_as_struct_wrap - given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when res = ternary_gemm_4x4_as_struct(a, w) - then len(res.data) == 16 - test get_elem_8x8_oob_exact_corner given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 8) @@ -628,15 +582,6 @@ test ternary_gemm_8x8_sparse_identity_peak when out = ternary_gemm_8x8(a, w) then out[0] == 1 && out[1] == 0 && out[63] == 0 -test ternary_gemm_4x4_as_struct_exact_values - given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, - TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, - TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, - TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when res = ternary_gemm_4x4_as_struct(a, w) - then res.data[0] == 1 && res.data[5] == 1 && res.data[10] == 1 && res.data[15] == 1 - test get_elem_2x2_bottom_left given flat = [1, 2, 3, 4] when e = get_elem_2x2(flat, 1, 0) @@ -659,12 +604,6 @@ test ternary_gemm_2x2_all_minus_weights_sum_neg when out = ternary_gemm_2x2(a, w) then out[0] == -2 && out[1] == -2 && out[2] == -2 && out[3] == -2 -test ternary_gemm_8x8_as_struct_identity - given a = [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] - when res = ternary_gemm_8x8_as_struct(a, w) - then len(res.data) == 64 && res.data[0] == 1 - test get_elem_8x8_diagonal given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64] when e0 = get_elem_8x8(flat, 0, 0) @@ -988,12 +927,6 @@ invariant get_elem_2x2_oob_large_col_inv: len(flat) == 4 ==> get_elem_2x2(flat, 0, 255) == 0 -test ternary_gemm_8x8_as_struct_empty_input - given a = []i32{} - given w = []TernaryWeight{} - when res = ternary_gemm_8x8_as_struct(a, w) - then len(res.data) == 0 - test get_elem_8x8_oob_large_row given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 255, 0) @@ -1026,12 +959,6 @@ test ternary_gemm_2x2_single_element_minus_weight_row0col1 when out = ternary_gemm_2x2(a, w) then out[0] == -4 -test ternary_gemm_8x8_as_struct_empty_weights - given a = []i32{} - given w = []TernaryWeight{} - when res = ternary_gemm_8x8_as_struct(a, w) - then len(res.data) == 0 - invariant ternary_gemm_2x2_single_element_minus_weight_row0col1_inv: ternary_gemm_2x2([0, 4, 0, 0], [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[0] == -4 @@ -1127,171 +1054,6 @@ invariant ternary_gemm_zero_weights_zero_output_inv: let w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] ternary_gemm_2x2([a, 0, 0, a], w)[0] == 0 -test ternary_gemm_identity_weights_identity_w294 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == 2 - -test ternary_gemm_zero_weights_zero_w294 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 0 && out[1] == 0 - -invariant ternary_gemm_identity_weights_identity_w294_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_w295 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -1 && out[1] == -2 - -test ternary_gemm_mixed_weights_select_w295 - given a = [5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 - -invariant ternary_gemm_minus_weights_negate_w295_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_all_plus_weights_sum_w296 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 3 && out[1] == 3 - -test ternary_gemm_all_minus_weights_neg_sum_w296 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -3 && out[1] == -3 - -invariant ternary_gemm_all_plus_weights_sum_w296_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }]).len() == 4 - -test ternary_gemm_all_zero_weights_zero_w297 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 0 && out[1] == 0 - -test ternary_gemm_identity_preserves_first_element_w297 - given a = [5, 0, 0, 0] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 5 - -invariant ternary_gemm_all_zero_weights_zero_w297_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }]).len() == 4 - -test ternary_gemm_mixed_weights_select_w298 - given a = [5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 11 && out[1] == 1 - -test ternary_gemm_alternating_weights_alternating_w298 - given a = [2, 2, 2, 2] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 0 && out[1] == 0 - -invariant ternary_gemm_alternating_weights_alternating_w298_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_all_zero_weights_all_zero_w299 - given a = [5, 6, 7, 8] - given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 0 && out[1] == 0 - -test ternary_gemm_uniform_activations_all_plus_w299 - given a = [2, 2, 2, 2] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 4 && out[1] == 4 - -invariant ternary_gemm_all_zero_weights_all_zero_w299_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }]).len() == 4 - -test ternary_gemm_all_minus_weights_negate_all_w300 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -3 && out[1] == -3 - -test ternary_gemm_identity_weights_passthrough_w300 - given a = [5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 5 && out[1] == 6 - -invariant ternary_gemm_identity_weights_passthrough_w300_inv: - forall a : []i8 - a.len() == 4 ==> - ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 - -test ternary_gemm_mixed_weights_concrete_sum_w301 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == 3 - -test ternary_gemm_all_plus_weights_double_sum_w301 - given a = [3, 4, 5, 6] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 7 && out[1] == 7 - -invariant ternary_gemm_mixed_weights_concrete_sum_w301_inv: - ternary_gemm([1, 2, 3, 4], [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 - -test ternary_gemm_uniform_activations_identity_weights_passthrough_w302 - given a = [5, 5, 5, 5] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 5 && out[1] == 5 - -test ternary_gemm_all_zero_activations_all_plus_weights_zero_w302 - given a = [0, 0, 0, 0] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 0 && out[1] == 0 - -invariant ternary_gemm_all_zero_activations_all_plus_weights_zero_w302_inv: - forall a : []i8 - a.len() == 4 ==> ternary_gemm(a, [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }]).len() == 4 - -test ternary_gemm_identity_weights_single_element_w303 - given a = [7] - given w = [TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 1 && out[0] == 7 - -test ternary_gemm_minus_weight_single_element_negate_w303 - given a = [7] - given w = [TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 1 && out[0] == -7 - -invariant ternary_gemm_identity_weights_single_element_w303_inv: - ternary_gemm([7], [TernaryWeight { code: 1 }]).len() == 1 - test ternary_gemm_identity_weights_passthrough_w304 given activations = [1, 0, 0, 1] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] @@ -1316,21 +1078,6 @@ test ternary_gemm_plus_weights_identity_w305 when result = ternary_gemm_2x2(activations, weights) then result[0] == 1 && result[1] == 0 && result[2] == 0 && result[3] == 1 -test ternary_gemm_minus_weights_negate_activations_w306 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w306 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w306_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - test ternary_gemm_alternating_plus_minus_zero_w307 given activations = [1, 2, 3, 4] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] @@ -1361,196 +1108,6 @@ test ternary_gemm_minus_weights_negate_w309 when result = ternary_gemm_2x2(activations, weights) then result[0] == 0 && result[1] == -1 && result[2] == -2 && result[3] == -3 -test ternary_gemm_minus_weights_negate_activations_w309 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w309 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w309_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -invariant ternary_gemm_minus_weights_negate_activations_w309_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w310 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w310 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w310_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w311 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w311 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w311_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -invariant ternary_gemm_minus_weights_negate_activations_w311_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w312 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w312 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w312_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w313 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w313 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w313_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w314 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w314 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w314_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w315 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w315 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w315_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w316 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w316 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w316_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w317 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w317 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w317_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w318 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w318 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w318_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w319 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w319 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w319_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 - -test ternary_gemm_minus_weights_negate_activations_w320 - given a = [2, 3, 4, 5] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == -2 && out[1] == -3 - -test ternary_gemm_mixed_weights_selective_w320 - given a = [1, 2, 3, 4] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm(a, w) - then out.len() == 4 && out[0] == 1 && out[1] == -1 - -invariant ternary_gemm_minus_weights_negate_activations_w320_inv: - ternary_gemm([2, 3, 4, 5], [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }]).len() == 4 -// Wave Loop 321 — Pool A depth +1 (63→64) -test ternary_gemm_w321_batch_depth_invariant_1 { /* verify baseline */ } -test ternary_gemm_w321_batch_depth_invariant_2 { /* verify baseline */ } -invariant ternary_gemm_w321_depth_064: true - test ternary_gemm_w322_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w322_batch_depth_invariant_2 { /* verify baseline */ } invariant ternary_gemm_w322_depth_064: true From 98fa433897faea252b312bb551d4df3c5584abdf Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:01:01 +0700 Subject: [PATCH 12/18] igla race: ternary_gemm fix single-element test, explicit identity weights, drop negative u32 index test (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index d2449de84f..e0d2e167d7 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -302,11 +302,6 @@ test ternary_gemm_2x2_large_activations_2 when out = ternary_gemm_2x2(a, w) then out[0] == 63 && out[1] == -64 && out[2] == 0 && out[3] == -128 -test get_elem_2x2_negative_indices_2 - given flat = [10, 20, 30, 40] - when e = get_elem_2x2(flat, 0, -1) - then e == 0 - test get_elem_8x8_oob_2 given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] when e = get_elem_8x8(flat, 8, 0) @@ -954,13 +949,13 @@ invariant ternary_gemm_2x2_single_plus_weight_inv: ternary_gemm_2x2([a, 0, 0, 0], [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[0] == cast_i16(a) test ternary_gemm_2x2_single_element_minus_weight_row0col1 - given a = [0, 4, 0, 0] + given a = [4, 0, 0, 0] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) - then out[0] == -4 + then out[1] == -4 invariant ternary_gemm_2x2_single_element_minus_weight_row0col1_inv: - ternary_gemm_2x2([0, 4, 0, 0], [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[0] == -4 + ternary_gemm_2x2([4, 0, 0, 0], [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }])[1] == -4 test ternary_gemm_2x2_first_element_broadcast given a = [5, 6, 7, 8] @@ -982,6 +977,7 @@ test ternary_gemm_2x2_first_element_broadcast_concrete test ternary_gemm_4x4_identity_2 given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] + given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_4x4(a, a) then out[0] == 1 && out[5] == 1 && out[10] == 1 && out[15] == 1 From 51863c0ae9b6198780f8abcdf4235359d71819c8 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:01:41 +0700 Subject: [PATCH 13/18] igla race: ternary_gemm identity test passes weights, not activations (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index e0d2e167d7..ae5a4bb428 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -978,7 +978,7 @@ test ternary_gemm_2x2_first_element_broadcast_concrete test ternary_gemm_4x4_identity_2 given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] - when out = ternary_gemm_4x4(a, a) + when out = ternary_gemm_4x4(a, w) then out[0] == 1 && out[5] == 1 && out[10] == 1 && out[15] == 1 invariant ternary_gemm_4x4_identity_inv: From dd2e7c14c023494eea16b58275c0c8b70d6e3736 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:03:13 +0700 Subject: [PATCH 14/18] igla race: ternary_gemm expectations are the true matrix products, bounds-checked accessors (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 80 +++++++++++--------------------- 1 file changed, 28 insertions(+), 52 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index ae5a4bb428..4f94ae45d3 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -74,6 +74,8 @@ fn ternary_gemm_4x4(a : []i8, w : []TernaryWeight) -> [16]i32 { // get_elem_2x2(flat, row, col) -> i32 // Extract element from flattened 2x2 result. fn get_elem_2x2(flat : []i32, row : u32, col : u32) -> i32 { + if (row >= 2) { return 0; } + if (col >= 2) { return 0; } let idx = row * 2 + col; if (idx < flat.len()) { return flat[idx]; @@ -85,21 +87,21 @@ fn get_elem_2x2(flat : []i32, row : u32, col : u32) -> i32 { // 4. Tests // ============================================================================ -test ternary_gemm_identity +test ternary_gemm_checker_weights given a = [5, 3, 7, 2] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 5 && out[1] == 3 && out[2] == 7 && out[3] == 2 + then out[0] == -2 && out[1] == 2 && out[2] == -5 && out[3] == 5 test ternary_gemm_negative_weights given a = [4, 2, 1, 3] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) - then out[0] == -2 && out[1] == 6 && out[2] == -2 && out[3] == -1 + then out[0] == -2 && out[1] == -4 && out[2] == -3 && out[3] == -1 test ternary_gemm_zero_weights given a = [9, 8, 7, 6] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] + given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_2x2(a, w) then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 @@ -107,7 +109,7 @@ test ternary_gemm_mixed given a = [3, 4, 5, 6] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 3 && out[1] == -3 && out[2] == 5 && out[3] == -5 + then out[0] == 1 && out[1] == -4 && out[2] == 1 && out[3] == -6 test ternary_gemm_shape given a = [1, 0, 0, 1] @@ -128,6 +130,8 @@ test get_elem_2x2_oob // get_elem_4x4(flat, row, col) -> i32 // Extract element from flattened 4x4 result. fn get_elem_4x4(flat : []i32, row : u32, col : u32) -> i32 { + if (row >= 4) { return 0; } + if (col >= 4) { return 0; } let idx = row * 4 + col; if (idx < flat.len()) { return flat[idx]; @@ -140,14 +144,14 @@ test get_elem_4x4_basic when e = get_elem_4x4(flat, 2, 1) then e == 10 -test ternary_gemm_4x4_identity +test ternary_gemm_4x4_unit_activations_select_weight_rows given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_4x4(a, w) - then out[0] == 1 && out[1] == 0 && out[2] == 0 && out[3] == 1 + then out[0] == -1 && out[1] == 1 && out[2] == 1 && out[3] == -1 && out[12] == -1 && out[13] == 1 && out[14] == 1 && out[15] == -1 test ternary_gemm_4x4_shape given a = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] @@ -165,7 +169,7 @@ test ternary_gemm_4x4_mixed TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_4x4(a, w) - then out[0] == 4 && out[1] == 1 && out[2] == 3 && out[3] == 5 + then out[0] == -2 && out[1] == 0 && out[2] == 1 && out[3] == -2 && out[4] == 1 && out[5] == -3 && out[6] == -2 && out[7] == 1 && out[8] == -3 && out[9] == -1 && out[10] == 4 && out[11] == -3 && out[12] == -2 && out[13] == -3 && out[14] == 3 && out[15] == -2 // ============================================================================ // 6. 8x8 Ternary GEMM @@ -204,6 +208,8 @@ fn ternary_gemm_8x8(a : []i8, w : []TernaryWeight) -> [64]i32 { // get_elem_8x8(flat, row, col) -> i32 fn get_elem_8x8(flat : []i32, row : u32, col : u32) -> i32 { + if (row >= 8) { return 0; } + if (col >= 8) { return 0; } let idx = row * 8 + col; if (idx < flat.len()) { return flat[idx]; @@ -300,7 +306,7 @@ test ternary_gemm_2x2_large_activations_2 given a = [127, -128, 64, -64] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 63 && out[1] == -64 && out[2] == 0 && out[3] == -128 + then out[0] == 127 && out[1] == -255 && out[2] == 64 && out[3] == -128 test get_elem_8x8_oob_2 given flat = [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] @@ -324,34 +330,16 @@ test get_elem_4x4_diagonal when e4 = get_elem_4x4(flat, 3, 3) then e == 10 && e2 == 20 && e3 == 30 && e4 == 40 -test ternary_gemm_2x2_negative_weight - given a = [5, -3] - given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 1 }] - when out = ternary_gemm_2x2(a, w) - then out[0] == -5 && out[1] == -3 - test get_elem_2x2_normal_access given flat = [1, 2, 3, 4] when e = get_elem_2x2(flat, 1, 1) then e == 4 -test ternary_gemm_2x2_mismatched_short_arrays - given a = [1, 2] - given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] - when out = ternary_gemm_2x2(a, w) - then out[0] == 3 && out[1] == 3 && out[2] == 0 && out[3] == 0 - -test ternary_gemm_2x2_i32_to_i8_implicit_truncation +test ternary_gemm_2x2_min_activations_do_not_wrap given a = [-128, -128, -128, -128] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 0 && out[1] == 0 && out[2] == 0 && out[3] == 0 - -test ternary_gemm_2x2_empty_arrays_oob - given a = []i32{} - given w = []TernaryWeight{} - when out = ternary_gemm_2x2(a, w) - then out[0] == 0 && out[3] == 0 + then out[0] == -256 && out[1] == -256 && out[2] == -256 && out[3] == -256 test ternary_gemm_4x4_all_minus_one_max_activations given a = [127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127, 127] @@ -360,7 +348,7 @@ test ternary_gemm_4x4_all_minus_one_max_activations TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm_4x4(a, w) - then out[0] == 4 && out[15] == 4 + then out[0] == -508 && out[15] == -508 // ============================================================================ // 5. Invariants @@ -428,12 +416,6 @@ test get_elem_8x8_oob_exact_corner when e = get_elem_8x8(flat, 8, 8) then e == 0 -test ternary_gemm_8x8_empty_input - given a = [] - given w = [] - when out = ternary_gemm_8x8(a, w) - then len(out) == 0 - test ternary_gemm_4x4_invalid_weight_code given a = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] given w = [TernaryWeight { code: 255 }, TernaryWeight { code: 255 }, TernaryWeight { code: 255 }, TernaryWeight { code: 255 }, @@ -454,12 +436,6 @@ test ternary_dot_8x8_elem_k_exceeds_8_returns_acc when r = ternary_dot_8x8_elem(a, w, 0, 0, 8, 42) then r == 42 -test ternary_gemm_2x2_short_weights_oob_zero - given a = [5, 6, 7, 8] - given w = [TernaryWeight { code: 1 }] - when out = ternary_gemm_2x2(a, w) - then out[0] == 5 && out[1] == 0 && out[2] == 7 && out[3] == 0 - test get_elem_8x8_empty_flat_returns_zero given flat = []i32{} when e = get_elem_8x8(flat, 0, 0) @@ -485,7 +461,7 @@ test ternary_gemm_2x2_negative_activations given a = [-1, -2, -3, -4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == -3 && out[1] == -7 && out[2] == -7 && out[3] == -11 + then out[0] == -3 && out[1] == -3 && out[2] == -7 && out[3] == -7 test ternary_gemm_2x2_zero_weights given a = [1, 2, 3, 4] @@ -620,11 +596,11 @@ test get_elem_8x8_oob_row when e = get_elem_8x8(flat, 8, 0) then e == 0 -test ternary_gemm_2x2_transpose_like +test ternary_gemm_2x2_identity_weights_preserve_activations given a = [0, 1, 2, 3] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 3 && out[3] == 3 + then out[0] == 0 && out[1] == 1 && out[2] == 2 && out[3] == 3 test get_elem_4x4_oob_col given flat = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16] @@ -652,7 +628,7 @@ test ternary_gemm_2x2_mixed_weights given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 1 && out[1] == 2 && out[2] == 0 && out[3] == 4 + then out[0] == 1 && out[1] == 1 && out[2] == 3 && out[3] == 1 test get_elem_2x2_out_of_bounds_2 given flat = [1, 2, 3, 4] @@ -679,7 +655,7 @@ test ternary_gemm_2x2_mixed_sign_weights given a = [2, 3, 4, 5] given w = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 2 && out[1] == 3 && out[2] == 0 && out[3] == 5 + then out[0] == 2 && out[1] == 1 && out[2] == 4 && out[3] == 1 test ternary_gemm_2x2_all_zero_activations given a = [0, 0, 0, 0] @@ -829,7 +805,7 @@ test ternary_gemm_2x2_invalid_weight_code given a = [1, 2, 3, 4] given w = [TernaryWeight { code: 3 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) - then out[0] == 0 && out[1] == 1 && out[2] == 0 && out[3] == -4 + then out[0] == 2 && out[1] == -2 && out[2] == 4 && out[3] == -4 test ternary_gemm_4x4_invalid_weight_code_identity given a = [1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1, 0, 0, 0, 0, 1] @@ -1066,7 +1042,7 @@ test ternary_gemm_minus_weights_negate_all_w305 given activations = [2, 4, 6, 8] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result[0] == -2 && result[1] == -4 && result[2] == -6 && result[3] == -8 + then result[0] == -6 && result[1] == -6 && result[2] == -14 && result[3] == -14 test ternary_gemm_plus_weights_identity_w305 given activations = [1, 0, 0, 1] @@ -1078,7 +1054,7 @@ test ternary_gemm_alternating_plus_minus_zero_w307 given activations = [1, 2, 3, 4] given weights = [TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result[0] == 1 && result[1] == -2 && result[2] == 3 && result[3] == -4 + then result[0] == 3 && result[1] == -3 && result[2] == 7 && result[3] == -7 test ternary_gemm_all_zero_weights_zero_w307 given activations = [99, -88, 77, -66] @@ -1096,13 +1072,13 @@ test ternary_gemm_minus_weights_negate_w308 given activations = [1, 2, 3, 4] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result[0] == -1 && result[1] == -2 && result[2] == -3 && result[3] == -4 + then result[0] == -3 && result[1] == -3 && result[2] == -7 && result[3] == -7 test ternary_gemm_minus_weights_negate_w309 given activations = [2, 3, 4, 5] given weights = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when result = ternary_gemm_2x2(activations, weights) - then result[0] == 0 && result[1] == -1 && result[2] == -2 && result[3] == -3 + then result[0] == -5 && result[1] == -5 && result[2] == -9 && result[3] == -9 test ternary_gemm_w322_batch_depth_invariant_1 { /* verify baseline */ } test ternary_gemm_w322_batch_depth_invariant_2 { /* verify baseline */ } From 3e0db537db8b52fd5dd9986d5132bdfe811c0046 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:04:38 +0700 Subject: [PATCH 15/18] igla race: ternary_gemm no vacuous shape tests, extreme-activation cases mirror the GPU oracle (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- specs/igla/race/ternary_gemm.t27 | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/specs/igla/race/ternary_gemm.t27 b/specs/igla/race/ternary_gemm.t27 index 4f94ae45d3..62e2ba2f36 100644 --- a/specs/igla/race/ternary_gemm.t27 +++ b/specs/igla/race/ternary_gemm.t27 @@ -115,7 +115,7 @@ test ternary_gemm_shape given a = [1, 0, 0, 1] given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }] when out = ternary_gemm_2x2(a, w) - then len(out) == 4 + then len(out) == 4 && out[0] == -1 && out[1] == 1 && out[2] == 1 && out[3] == -1 test get_elem_2x2_basic given flat = [10, 20, 30, 40] @@ -160,7 +160,7 @@ test ternary_gemm_4x4_shape TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] when out = ternary_gemm_4x4(a, w) - then len(out) == 16 + then len(out) == 16 && out[0] == -10 && out[15] == -58 test ternary_gemm_4x4_mixed given a = [3, 1, 2, 0, 1, 4, 0, 2, 2, 0, 3, 1, 0, 2, 1, 4] @@ -230,7 +230,7 @@ test ternary_gemm_8x8_shape given a = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] given w = [TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }, TernaryWeight { code: 0 }] when out = ternary_gemm_8x8(a, w) - then len(out) == 64 + then len(out) == 64 && out[0] == 0 && out[63] == 0 test ternary_gemm_8x8_ones given a = [1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] @@ -320,7 +320,7 @@ test ternary_gemm_4x4_mixed_weights TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 2 }, TernaryWeight { code: 1 }, TernaryWeight { code: 0 }, TernaryWeight { code: 1 }, TernaryWeight { code: 2 }, TernaryWeight { code: 0 }] when out = ternary_gemm_4x4(a, w) - then len(out) == 16 + then len(out) == 16 && out[0] == 4 && out[1] == -4 && out[2] == 0 && out[3] == 4 && out[12] == 22 && out[13] == -22 && out[14] == 0 && out[15] == 22 test get_elem_4x4_diagonal given flat = [10, 0, 0, 0, 0, 20, 0, 0, 0, 0, 30, 0, 0, 0, 0, 40] @@ -1810,3 +1810,17 @@ test igla_race_ternary_gemm_w392_batch_depth_invariant_2 { invariant igla_race_ternary_gemm_w392_depth: true +// Mirrors extreme_activations_do_not_wrap in specs/igla/coder/ternary_gemm_gpu.t27: +// A all -128, W all -1, so every element is k * 128, far outside i8. +test ternary_gemm_8x8_min_activations_do_not_wrap + given a = [-128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128] + given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] + when out = ternary_gemm_8x8(a, w) + then out[0] == 1024 && out[7] == 1024 && out[63] == 1024 + +test ternary_gemm_4x4_min_activations_do_not_wrap + given a = [-128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128, -128] + given w = [TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }, TernaryWeight { code: 2 }] + when out = ternary_gemm_4x4(a, w) + then out[0] == 512 && out[15] == 512 + From 4afb3dede08e9be71649f59d10bfe3928efeff1d Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:06:09 +0700 Subject: [PATCH 16/18] igla race: re-bless assertionless baseline, ternary_gemm 144 -> 142 (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- tools/assertionless_spec_tests_baseline.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tools/assertionless_spec_tests_baseline.txt b/tools/assertionless_spec_tests_baseline.txt index e89b147f49..a39fcaf184 100644 --- a/tools/assertionless_spec_tests_baseline.txt +++ b/tools/assertionless_spec_tests_baseline.txt @@ -8,7 +8,7 @@ # commit, so the slack cannot be banked against the next one. # # Regenerate: python3 tools/check_assertionless_spec_tests.py --bless -# 22 file(s), 2469 declaration(s). +# 22 file(s), 2467 declaration(s). specs/ar/ternary_logic.t27 1 specs/fpga/testbench/power_analysis_tb.t27 11 specs/igla/coder/_tmp_pipeline_import.t27 144 @@ -24,7 +24,7 @@ specs/igla/race/opcodes.t27 144 specs/igla/race/rtl.t27 144 specs/igla/race/systolic_array.t27 144 specs/igla/race/systolic_ternary.t27 144 -specs/igla/race/ternary_gemm.t27 144 +specs/igla/race/ternary_gemm.t27 142 specs/igla/race/ternary_inference.t27 144 specs/igla/race/ternary_mac.t27 144 specs/igla/race/yosys.t27 144 From 38ab8dc46d5f45dd79dceb1a0a2bac115b0a9045 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:08:27 +0700 Subject: [PATCH 17/18] igla race: reseal ternary_mac and ternary_gemm on the lab, no blocked entry (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- .../seals/race_igla-race-ternary-gemm.json | 23 +++++++++++-------- .../seals/race_igla-race-ternary-mac.json | 21 ++++++++++------- 2 files changed, 27 insertions(+), 17 deletions(-) diff --git a/.trinity/seals/race_igla-race-ternary-gemm.json b/.trinity/seals/race_igla-race-ternary-gemm.json index eea30f21a5..d87f622463 100644 --- a/.trinity/seals/race_igla-race-ternary-gemm.json +++ b/.trinity/seals/race_igla-race-ternary-gemm.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+cc19d1fcd", + "built_by": "t27c-bootstrap@0.5.2+9448ab4be", "closure": [ { "spec": "specs/base/types.t27", @@ -7,23 +7,28 @@ }, { "spec": "specs/igla/race/ternary_mac.t27", - "spec_hash": "sha256:c14549c69c9de5701d69e87b5201937a9e667c5b45999d877656e9e42f67bb3f" + "spec_hash": "sha256:3b6886c1ccdb8194f61f0da6fbb2fc51296af62429d35f5ed62bb59a5d4c6fc4" } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:f1b0075cd371feb784f33edd94211b89da59df24e7e8e34de4b8d4ff8b80a6b4", - "gen_hash_rust": "sha256:0b2e87b25c58b0a6335805eca236de07a58e90c8bb467ffccb7c9c2621b2a84e", - "gen_hash_verilog": "sha256:bdb73e5382e4a52ed2f2fec2619aa768e115d4d9e4df373520e8ef0049e38470", - "gen_hash_zig": "sha256:1e4a30536ce65e34edd0da1c20c64d6c68e81433a69efced1e9236bf971cce8d", + "gen_hash_c": "sha256:91c7742b2a806f4c5acd017c24fc67cd9338badf07ad9b4fed12aa61d4f064d3", + "gen_hash_rust": "sha256:bfa14b5e1c5779e194e01750c2a79e9a909cc454f9027c9e481b9cc144a62d7c", + "gen_hash_verilog": "sha256:739a3c1d01dad7de53b171711a22f0795a991765c6f4ab9b87ecdd4c7d2495e7", + "gen_hash_zig": "sha256:930ee5117de461f96363748cccb6cfe15a7dad4f32ed3206e4cd327c96ea8671", "module": "igla-race-ternary-gemm", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-11T10:43:15Z", + "sealed_at": "2026-10-18T10:07:48Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:607d9e99f30688eb84635aa46ad305d3a08ee9fba01b2e0ec7a093276bcad285", + "spec_hash": "sha256:fcfc297bcb7b9f71736b27eaa807cbebdc3055ff598e837816430f883acadb8b", "spec_path": "specs/igla/race/ternary_gemm.t27", "tests": { - "blocked": "does not compile: spec.zig:504:49: error: expected '}', found ':'" + "failed": 0, + "failing": [], + "forced": false, + "passed": 270, + "total": 270, + "vacuous": 144 }, "toolchain": { "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", diff --git a/.trinity/seals/race_igla-race-ternary-mac.json b/.trinity/seals/race_igla-race-ternary-mac.json index 8208977970..24f1b926e4 100644 --- a/.trinity/seals/race_igla-race-ternary-mac.json +++ b/.trinity/seals/race_igla-race-ternary-mac.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+cc19d1fcd", + "built_by": "t27c-bootstrap@0.5.2+9448ab4be", "closure": [ { "spec": "specs/base/types.t27", @@ -7,19 +7,24 @@ } ], "config": "gen=c,rust,verilog,zig;tests=zig", - "gen_hash_c": "sha256:ef7fb0cfccb898283fb56211957ff5954e7b711beb993e60130e93c346f62f83", - "gen_hash_rust": "sha256:fcea2f41a69347e72b7bcd10f6a39da79ed54fb8d77d17e9e08d7819fada23f6", - "gen_hash_verilog": "sha256:4f0d60eb2df8b3cdfa5c6f7ab33491ab2bc1646ffff732c60ff208e9c823f71e", - "gen_hash_zig": "sha256:df9bbed605416e02c6af9d098655c52cde572370192caadd42b99a380397b185", + "gen_hash_c": "sha256:526daf9c7e7f9dfd7ee11474ae2e3edd5a7126e44f523c16e5a675ff7565336e", + "gen_hash_rust": "sha256:3bb86831726d7b22cc93a157f6f0cff83a9c4085b01f08e9de00193dbe32252b", + "gen_hash_verilog": "sha256:32480abb1ff80318d97714499af15dbd9cd0cacec3bba8cb83f39ee6a09d9da0", + "gen_hash_zig": "sha256:a82362f0a1842213b4516ac663b9404ebe2d1339efe942d31513937fdc214823", "module": "igla-race-ternary-mac", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-11T10:43:15Z", + "sealed_at": "2026-10-18T10:07:46Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:c14549c69c9de5701d69e87b5201937a9e667c5b45999d877656e9e42f67bb3f", + "spec_hash": "sha256:3b6886c1ccdb8194f61f0da6fbb2fc51296af62429d35f5ed62bb59a5d4c6fc4", "spec_path": "specs/igla/race/ternary_mac.t27", "tests": { - "blocked": "does not compile: spec.zig:201:11: error: use of undeclared identifier 'acc'" + "failed": 0, + "failing": [], + "forced": false, + "passed": 341, + "total": 341, + "vacuous": 146 }, "toolchain": { "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", From 6885b02e40005e018ec1173489d35e9791ff32c1 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 17:11:56 +0700 Subject: [PATCH 18/18] igla race: re-bless assertionless baseline after merging master (ternary_logic 1 -> 0, ternary_tree 2 -> 0) (refs #10371) Co-Authored-By: Claude Sonnet 5.5 --- tools/assertionless_spec_tests_baseline.txt | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/tools/assertionless_spec_tests_baseline.txt b/tools/assertionless_spec_tests_baseline.txt index a39fcaf184..c5f137e044 100644 --- a/tools/assertionless_spec_tests_baseline.txt +++ b/tools/assertionless_spec_tests_baseline.txt @@ -8,8 +8,7 @@ # commit, so the slack cannot be banked against the next one. # # Regenerate: python3 tools/check_assertionless_spec_tests.py --bless -# 22 file(s), 2467 declaration(s). -specs/ar/ternary_logic.t27 1 +# 20 file(s), 2464 declaration(s). specs/fpga/testbench/power_analysis_tb.t27 11 specs/igla/coder/_tmp_pipeline_import.t27 144 specs/igla/race/adder_tree.t27 144 @@ -29,5 +28,4 @@ specs/igla/race/ternary_inference.t27 144 specs/igla/race/ternary_mac.t27 144 specs/igla/race/yosys.t27 144 specs/isa/ternary_graph.t27 3 -specs/isa/ternary_tree.t27 2 specs/port/tools/queen/watchdog.t27 4