Дважды сменить знак — получить число обратно

Вы узнаете

Как тест свойства ловит ошибку в один символ, которую пропускает единичный пример.

Попробуйте

Найдите, сколько проходов были пустыми; затем вернитесь к плееру прошлого урока, сами замените XOR на OR и посмотрите, поймает ли это и браузер.

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
}

Открыть спеку урока в плеере ↗

Все уроки

• Модуль 1 · Лаборатория: наши исследования

  Свой формат чисел, честная таблица результатов и таблицы модели, перемноженные на плате.

  1. 01 T27: наш собственный формат чисел
  2. 02 Честная таблица результатов
  3. 03 Таблицы модели на плате

• Модуль 2 · ИИ-числа: блок MX

  Как ИИ-чипы хранят веса в нескольких битах: один общий масштаб на блок, сам байт масштаба и что один выброс делает с соседями.

  1. 04 Один масштаб на блок весов
  2. 05 Байт масштаба на настоящей машине
  3. 06 Один выброс, много нулей

• Модуль 3 · Тернарные веса

  Веса, которые бывают только минус масштаб, ноль или плюс масштаб, пять правил, которые должен пройти тернарный алфавит, и прогон тестов, который ничего не проверил.

  1. 07 Веса минус фи, ноль и плюс фи
  2. 08 Прогон, который ничего не проверил
  3. 09 Пять правил для алфавита весов

• Модуль 4 · Тернарный формат Ternary Network Float

  Правило, которое компилятор проверяет до запуска любого теста, и 17-битное число с плавающей точкой, порядок которого — четыре сбалансированных трита.

  1. 10 Заблокирован — не значит провален
  2. 11 Число, у которого порядок — четыре трита
  3. 12 Дважды сменить знак — получить число обратно

• Модуль 5 · Арифметика чисел со знаком

  Умножить два числа со знаком, сложить их, когда знаки разные, и сделать то и другое сразу в умножении с накоплением.

  1. 13 Знак — это один бит
  2. 14 Разные знаки — вычитание
  3. 15 Умножить, потом сложить

• Модуль 6 · Части нейрона

  ReLU с изломом в нуле, степень двойки для softmax и argmax, который называет ответ.

  1. 16 Излом в нуле
  2. 17 Два в степени x
  3. 18 Выбрать наибольшее

• Модуль 7 · Обучение на ошибке

  Потеря, которая оценивает неверную догадку в битах, один шаг, который сдвигает вес против градиента, и скрытый слой, который нужен XOR.

  1. 19 Потеря в битах
  2. 20 Один шаг вниз по склону
  3. 21 XOR нужен излом

• Модуль 8 · BitNet: тернарные сети

  Порог, который сжимает сумму обратно до трёх значений, один нейрон, который становится другой функцией при смене весов, и нейрон, который читает входы по 27 тритов за раз.

  1. 22 Обратно в три значения
  2. 23 Тот же нейрон, другие веса
  3. 24 Нейрон по кускам

• Модуль 9 · Тернарный MAC как чип

  Скалярное произведение 27 тритов как провода без регистра, та же сумма, которую регистр копит на каждом такте, и небольшая целая сеть в конце курса.

  1. 25 Скалярное произведение из проводов
  2. 26 Складывать на каждом такте
  3. 27 Целая сеть