Negate twice, get the number back
You will learn
How a test of a property catches a one-character bug that a single example misses.
The browser skipped 24 checks of tnf17.t27; the native t27c runs all 34 tests, all pass, and none is vacuous. Negation flips the sign bit with XOR. The recording swaps XOR for OR, a one-character bug. Negating a positive number still looks right, so the test that negates one still passes. But negating a negative number now leaves it negative, so negating twice no longer gives the number back. Exactly one test fails, negate_is_an_involution, the one that states that property. Every byte in the recording was printed by the command; only the typing is staged.
Try it
Find how many passes were vacuous; then go back to the player of the previous lesson, change the XOR to OR yourself, and see whether the browser catches it too.
t27c on the t27c lab (Railway), spec at t27 5ff0ec512: 34 tests pass natively; negating with OR instead of XOR fails exactly one test, the involution; git restores the spec.
specs/numeric/tnf17.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/tnf17.t27
// TNF17e -- Ternary Network Float, the signed accumulator format.
//
// WHY THIS EXISTS. Measured 2026-08-13: the string "TNF" appears in ZERO of the
// 1,064 .t27 specs. It has a 2,353-line article (docs/theory/TNF_ARTICLE_RU.md),
// a dedicated skill, and an erratum -- and no implementation. This file is the
// first one.
//
// LAYOUT. TNF17e = [ sign(1) | offset(7) | mantissa(9) ]
//
// value = (-1)^s * (1 + mant/512) * 2^(offset - 40)
//
// The offset field carries 81 values (0..80), which is exactly 3^4 -- FOUR
// BALANCED-TERNARY TRITS -- giving e in [-40, +40]. That is the ternary claim,
// and it is a claim about the ENCODING OF THE EXPONENT FIELD, not about the
// scale: the scale is 2^e, and by the article's own radix theorem a binary scale
// is correct, because a radix-3 scale would oscillate by log2(3) = 1.585 bits of
// effective precision against binary's 1.
//
// RELATION TO GF-T16. The magnitude half is bit-identical to the GF-T16 already
// implemented and silicon-proven in specs/ternary/gft_dot2.t27 (BIAS=40,
// OFFSET_MAX=80, MANT_ONE=512). TNF17e = GF-T16 + a sign bit. That is deliberate:
// the article's own silicon table lists TNF17e as the RECOMMENDED rung, and
// reusing the proven magnitude path means the sign is the only new thing to
// verify.
//
// DISCREPANCY IN THE SOURCE, RECORDED RATHER THAN PAPERED OVER. The article's
// format section writes "TNF16 = [s | E=4 trits | M=11 bits]" while its own
// precision table and ladder use M=9 for rung 16 (and 2^-(M+1) = 9.77e-4 = 2^-10
// confirms M=9). Those cannot both hold: with M=11 the significand 1 + M/2^9
// ranges over [1,5), which is not normalized. The width rule 1+E+M=N counts
// POSITIONS, and a trit is not a bit, so "16 positions" is not "16 bits" -- on a
// binary fabric 4 trits cost 7 bits and 1+7+9 = 17. We therefore implement the
// unambiguous 17-bit rung the silicon table calls TNF17e, and leave TNF16c to a
// wave that can resolve what it trades.
//
// phi^2 + 1/phi^2 = 3 | TRINITY
module TNF17 {
use base::types;
// ---- Field geometry ----
const TNF_MANT_BITS : u32 = 9;
const TNF_MANT_ONE : u32 = 512; // 1 << 9
const TNF_MANT_MASK : u32 = 511;
const TNF_OFFSET_BITS : u32 = 7;
const TNF_BIAS : i32 = 40; // offset 40 == 2^0
const TNF_OFFSET_MAX : i32 = 80; // 3^4 - 1; the 81st value is the top row
const TNF_TRITS : u32 = 4; // 3^4 = 81 exponent steps
const TNF_EXP_STEPS : i32 = 81;
const TNF_WIDTH : u32 = 17; // 1 + 7 + 9
// ---- Field positions ----
const TNF_SIGN_SHIFT : u32 = 16;
const TNF_OFF_SHIFT : u32 = 9;
// ---- Canonical codes ----
// +1.0 = (1 + 0/512) * 2^0 -> sign 0, offset 40, mant 0 -> 40<<9 = 20480
const TNF_ONE : u32 = 20480;
const TNF_MINUS_ONE: u32 = 86016; // 20480 + (1<<16) = 20480 + 65536
// +2.0 = (1 + 0/512) * 2^1 -> offset 41 -> 41<<9 = 20992
const TNF_TWO : u32 = 20992;
// ---- Field extraction ----
fn tnf_sign(x: u32) -> u32 {
return ((x >> TNF_SIGN_SHIFT) & 1);
}
fn tnf_offset(x: u32) -> i32 {
return (((x >> TNF_OFF_SHIFT) & 127) as i32);
}
fn tnf_mant(x: u32) -> u32 {
return (x & TNF_MANT_MASK);
}
// Unbiased exponent, the value the four trits encode.
fn tnf_exponent(x: u32) -> i32 {
return (tnf_offset(x) - TNF_BIAS);
}
fn tnf_pack(sign: u32, offset: i32, mant: u32) -> u32 {
return (((sign & 1) << TNF_SIGN_SHIFT) | ((offset as u32) << TNF_OFF_SHIFT) | (mant & TNF_MANT_MASK));
}
// ---- Sign algebra: the whole of what TNF adds to GF-T16 ----
fn tnf_negate(x: u32) -> u32 {
return (x ^ (1 << TNF_SIGN_SHIFT));
}
fn tnf_abs(x: u32) -> u32 {
return (x & 65535);
}
fn tnf_is_negative(x: u32) -> bool {
return (tnf_sign(x) == 1);
}
// ---- Balanced-ternary view of the exponent ----
//
// e in [-40,40] is exactly 4 balanced trits, e = t0 + 3*t1 + 9*t2 + 27*t3
// with each t_i in {-1,0,+1}.
//
// The trits are extracted from the BIASED OFFSET, in unsigned arithmetic,
// by the excess-1 identity: 40 = 1 + 3 + 9 + 27, so subtracting the bias
// subtracts exactly ONE from every base-3 digit. Therefore
//
// trit_i(e) = digit_i(offset) - 1, offset = e + 40 in [0,80]
//
// and no signed division or remainder is needed anywhere. Verified on
// offsets 0, 33, 40, 53, 80 against a reference conversion.
//
// W655: this is not merely tidier. The first draft used `e % 3` on an i32
// and the Zig backend emitted a raw `%`, which Zig rejects outright --
// "signed integers and floats must use @rem or @mod". Unsigned digit
// extraction sidesteps a real backend gap AND is the cheaper hardware,
// because the offset is what the field already holds.
fn digit0(off: u32) -> u32 {
return (off % 3);
}
fn digit1(off: u32) -> u32 {
return ((off / 3) % 3);
}
fn digit2(off: u32) -> u32 {
return ((off / 9) % 3);
}
fn digit3(off: u32) -> u32 {
return ((off / 27) % 3);
}
fn trit0(off: u32) -> i32 {
return ((digit0(off) as i32) - 1);
}
fn trit1(off: u32) -> i32 {
return ((digit1(off) as i32) - 1);
}
fn trit2(off: u32) -> i32 {
return ((digit2(off) as i32) - 1);
}
fn trit3(off: u32) -> i32 {
return ((digit3(off) as i32) - 1);
}
// Reconstruct e from its four trits -- the round trip that makes the
// "four balanced trits" claim checkable rather than decorative.
fn trits_to_exponent(t0: i32, t1: i32, t2: i32, t3: i32) -> i32 {
return (t0 + 3 * t1 + 9 * t2 + 27 * t3);
}
// ---- Combinational port surface (T81: without this the module has no
// boundary and synthesises to nothing) ----
// Negate, then return the exponent: exercises the sign path and the offset
// path in one function.
fn on_comb(x: u32) -> u32 {
return tnf_negate(x);
}
// ---- Tests ----
test one_has_offset_forty
given o = tnf_offset(TNF_ONE)
then o == 40
test one_has_zero_exponent
given e = tnf_exponent(TNF_ONE)
then e == 0
test one_has_zero_mantissa
given m = tnf_mant(TNF_ONE)
then m == 0
test one_is_positive
given s = tnf_sign(TNF_ONE)
then s == 0
test two_has_offset_fortyone
given o = tnf_offset(TNF_TWO)
then o == 41
test two_has_exponent_one
given e = tnf_exponent(TNF_TWO)
then e == 1
// ---- Sign algebra ----
test negate_one_gives_minus_one
given n = tnf_negate(TNF_ONE)
then n == 86016
test minus_one_is_negative
given b = tnf_is_negative(TNF_MINUS_ONE)
then b == true
test one_is_not_negative
given b = tnf_is_negative(TNF_ONE)
then b == false
test negate_is_an_involution
given r = tnf_negate(tnf_negate(TNF_ONE))
then r == 20480
test abs_strips_the_sign
given a = tnf_abs(TNF_MINUS_ONE)
then a == 20480
test abs_of_a_positive_is_itself
given a = tnf_abs(TNF_ONE)
then a == 20480
// Negation must not disturb the magnitude -- the property that makes
// TNF17e = GF-T16 + sign rather than a different format.
test negate_preserves_the_offset
given o = tnf_offset(tnf_negate(TNF_TWO))
then o == 41
test negate_preserves_the_mantissa
given m = tnf_mant(tnf_negate(TNF_ONE))
then m == 0
// ---- Packing ----
test pack_rebuilds_one
given p = tnf_pack(0, 40, 0)
then p == 20480
test pack_rebuilds_minus_one
given p = tnf_pack(1, 40, 0)
then p == 86016
test pack_carries_the_mantissa
given m = tnf_mant(tnf_pack(0, 40, 256))
then m == 256
// ---- The balanced-ternary exponent, checked as arithmetic ----
// Trits are taken from the OFFSET (= e + 40), unsigned throughout.
// offset 40 == e 0 -> every trit is zero
test exponent_zero_is_all_zero_trits
given t = trit0(40)
then t == 0
test exponent_zero_top_trit
given t = trit3(40)
then t == 0
// offset 41 == e 1 -> lowest trit +1
test exponent_one_lowest_trit
given t = trit0(41)
then t == 1
// offset 42 == e 2 = 3 - 1 -> lowest trit -1, next +1
test exponent_two_is_minus_one_carry
given t = trit0(42)
then t == -1
test exponent_two_next_trit_is_one
given t = trit1(42)
then t == 1
// offset 80 == e 40 = 27+9+3+1 -> all four trits +1, the top of the range
test forty_is_all_plus_trits
given t = trit3(80)
then t == 1
test forty_third_trit
given t = trit2(80)
then t == 1
test forty_second_trit
given t = trit1(80)
then t == 1
test forty_first_trit
given t = trit0(80)
then t == 1
// offset 0 == e -40 -> the mirror, all four trits -1
test minus_forty_is_all_minus_trits
given t = trit3(0)
then t == -1
test minus_forty_first_trit
given t = trit0(0)
then t == -1
// Round trip: the four trits reconstruct the exponent exactly.
test round_trip_zero
given e = trits_to_exponent(trit0(40), trit1(40), trit2(40), trit3(40))
then e == 0
test round_trip_forty
given e = trits_to_exponent(trit0(80), trit1(80), trit2(80), trit3(80))
then e == 40
test round_trip_minus_forty
given e = trits_to_exponent(trit0(0), trit1(0), trit2(0), trit3(0))
then e == -40
// offset 53 == e 13
test round_trip_thirteen
given e = trits_to_exponent(trit0(53), trit1(53), trit2(53), trit3(53))
then e == 13
// offset 33 == e -7
test round_trip_minus_seven
given e = trits_to_exponent(trit0(33), trit1(33), trit2(33), trit3(33))
then e == -7
// ---- Port surface ----
test comb_surface_negates
given r = on_comb(TNF_ONE)
then r == 86016
// ---- Invariants ----
// Four balanced trits span exactly 81 values, and the offset field must
// agree. This is the ternary claim, stated as a checkable identity.
invariant four_trits_span_eighty_one
assert TNF_EXP_STEPS == TNF_OFFSET_MAX + 1
invariant bias_centres_the_exponent
assert TNF_BIAS * 2 == TNF_OFFSET_MAX
invariant trit_count_is_four
assert TNF_TRITS == 4
// The width rule 1 + E + M = N, in BITS: 1 sign + 7 offset + 9 mantissa.
invariant width_rule_holds_in_bits
assert TNF_WIDTH == 1 + TNF_OFFSET_BITS + TNF_MANT_BITS
// The mantissa's implicit one must match its bit count.
invariant mantissa_one_matches_its_width
assert TNF_MANT_ONE == TNF_MANT_MASK + 1
// 81 values need 7 bits and waste 47 of 128 -- the article's no-free-range
// theorem, made local: rho = 81/128, and a ternary field never spans more
// values per bit than a binary one on a binary fabric.
invariant offset_field_is_seven_bits
assert TNF_OFFSET_BITS == 7
// Unity must sit exactly at the bias with a zero mantissa.
invariant unity_is_bias_shifted
assert TNF_ONE == 20480
// Negation is a single bit flip at position 16, so -1 and +1 differ by
// exactly 2^16.
invariant negation_costs_one_bit
assert TNF_MINUS_ONE == TNF_ONE + 65536
invariant sign_sits_above_the_magnitude
assert TNF_SIGN_SHIFT == TNF_OFFSET_BITS + TNF_MANT_BITS
// The excess-1 identity that makes unsigned digit extraction exact:
// the bias must equal 1 + 3 + 9 + 27, i.e. (3^4 - 1)/2.
invariant bias_is_the_repunit_of_base_three
assert TNF_BIAS == 1 + 3 + 9 + 27
}
All lessons
Module 1 · Lab: our own research
A number format of our own, an honest scoreboard, and a model's tables multiplied on the board.
Module 2 · AI numbers: the MX block
How AI chips keep weights in a few bits: one shared scale per block, the scale byte itself, and what one outlier does to its neighbours.
Module 3 · Ternary weights
Weights that are only minus, zero or plus a scale, the five rules a ternary alphabet must pass, and a test pass that checked nothing.
Module 4 · The Ternary Network Float
A rule the compiler enforces before any test runs, and a 17-bit float whose exponent is four balanced trits.
Module 5 · Arithmetic on signed numbers
Multiply two signed numbers, add them when their signs differ, and do both at once in a multiply-accumulate.
Module 6 · Parts of a neuron
A ReLU that bends at zero, a power of two for softmax, and an argmax that names the answer.
Module 7 · Learning from a mistake
A loss that prices a wrong guess in bits, one step that moves a weight against its gradient, and the hidden layer that XOR needs.
Module 8 · BitNet: ternary networks
A threshold that squeezes a sum back to three values, one neuron that becomes a different function when its weights change, and a neuron that reads its inputs 27 trits at a time.
Module 9 · The ternary MAC as a chip
The 27-trit dot product as wires with no register, the same sum added into a register on every clock, and a small whole network to close the course.