The scale byte on a real machine

You will learn

What the native compiler checks in the same spec, including what the browser skipped.

Try it

Find how many invariants the test report proved at compile time, and compare its pass count with the player's.

specs/numeric/e8m0.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/e8m0.t27
// E8M0 -- the OCP Microscaling shared scale, and the trit count it does not have.
//
// WHY THIS EXISTS. `specs/numeric/formats_catalog.t27` is the numeric SSOT and it
// names `e8m0` FIVE times as the storage of another format --
//
//     mxfp8   storage=u8_plus_shared_e8m0
//     mxfp6   storage=u8_packed_plus_e8m0
//     mxfp4   storage=u8_packed_plus_e8m0
//     mxgf6   storage=u8_packed_plus_e8m0
//     mxgf4   storage=u8_packed_plus_e8m0
//
// -- and `grep "id=e8m0 "` over the same file returns ZERO. The SSOT depends on a
// component it never defines. This file defines it. Measured 2026-08-16.
//
// LAYOUT.  E8M0 = [ exponent(8) ].  No sign. No mantissa. No implicit one.
//
//     value = 2^(E - 127),   E in [0, 254]
//     E = 255                is NaN
//
// Source: OCP Microscaling Formats (MX) Specification v1.0, Rouhani et al. 2023,
// arXiv:2310.10537 -- the citation the catalogue already carries for every one of
// the five dependants.
//
// THE RESULT THIS MIGRATION PRODUCED, which is why it is worth a spec and not a
// constant. E8M0's exponent takes 255 distinct finite values, e in [-127, +127].
// Five balanced trits span 3^5 = 243 and six span 3^6 = 729, so
//
//     243 < 255 < 729
//
// and E8M0's exponent field is NOT a whole number of trits. It needs six and
// uses 255 of 729 -- 35 percent. Contrast `specs/numeric/tnf17.t27`, whose
// offset field holds exactly 81 = 3^4 values and uses 81 of 81. That contrast is
// stated below as a comptime invariant rather than as prose, because it is the
// only thing this format tells us that its own standard does not.
//
// WHAT THIS IS NOT. E8M0 is a SHARED SCALE, applied once per block of elements,
// not a weight code. Under the golden sieve (specs/numeric/golden_sieve.t27) it
// is not a candidate at all: S1 asks |A| = 3^k and 255 is not a power of three.
// It is also, for the same reason it is cheap, exempt from the sieve's concerns
// -- a pure power of two applied to a whole block is one shift, one lane, no
// DSP, and it never enters a neuron's truth table.
//
// phi^2 + phi^-2 = 3 | TRINITY

module E8M0 {

    // ---- Field geometry, from the OCP MX v1.0 specification ----

    const E8M0_BITS       : u32 = 8;
    const E8M0_BIAS       : i32 = 127;   // code 127 == 2^0
    const E8M0_NAN_CODE   : u32 = 255;   // the one reserved code
    const E8M0_MAX_FINITE : u32 = 254;   // largest finite code, 2^127
    const E8M0_MIN_FINITE : u32 = 0;     // smallest finite code, 2^-127
    const E8M0_ONE        : u32 = 127;   // the code whose value is 1.0

    // Distinct finite values the field can hold: 0..254 inclusive.
    const E8M0_FINITE_CODES : u32 = 255;

    // Trit spans, written out because the numeric core has no exponentiation.
    //
    // W781 DEFECT, caught by the comptime invariant that is the reason this file
    // has invariants at all: the first version of this table started at 3^5, so
    // `trits_needed(81)` answered 5 and `packs_exactly(81)` came back FALSE for a
    // number that is exactly 3^4. The table must reach DOWN to every power a
    // caller might land on, not only up to the one the subject format needs.
    const THREE_POW_3 : u32 = 27;
    const THREE_POW_4 : u32 = 81;
    const THREE_POW_5 : u32 = 243;
    const THREE_POW_6 : u32 = 729;

    // TNF17e's offset field, for the contrast invariant below. Kept as a local
    // constant rather than an import so this file stays self-contained; the
    // value is checked against tnf17.t27's own TNF_OFFSET_MAX + 1.
    const TNF17_OFFSET_VALUES : u32 = 81;    // 3^4, and it uses all 81

    // ---- Decode ----

    // The unbiased exponent. Returns the exponent of a FINITE code; callers must
    // test e8m0_is_nan first, exactly as the standard requires.
    fn e8m0_exponent(x: u32) -> i32 {
        return ((x as i32) - E8M0_BIAS);
    }

    fn e8m0_is_nan(x: u32) -> bool {
        return (x == E8M0_NAN_CODE);
    }

    fn e8m0_is_finite(x: u32) -> bool {
        return (x <= E8M0_MAX_FINITE);
    }

    // ---- Encode ----

    // The inverse of e8m0_exponent, for e in [-127, +127]. Out-of-range inputs
    // return the NaN code rather than wrapping: a scale that cannot be
    // represented is not a scale, and silently aliasing it to a representable
    // one is how a block of elements acquires the wrong magnitude.
    fn e8m0_encode(e: i32) -> u32 {
        if (e < (0 - E8M0_BIAS)) { return E8M0_NAN_CODE; }
        if (e > E8M0_BIAS) { return E8M0_NAN_CODE; }
        return ((e + E8M0_BIAS) as u32);
    }

    // ---- Trit accounting: the part the standard does not state ----

    // Whether `n` distinct values fit in five balanced trits, six, or neither
    // exactly. Returns the number of trits NEEDED; 0 means more than six.
    fn trits_needed(n: u32) -> u32 {
        if (n <= THREE_POW_3) { return 3; }
        if (n <= THREE_POW_4) { return 4; }
        if (n <= THREE_POW_5) { return 5; }
        if (n <= THREE_POW_6) { return 6; }
        return 0;
    }

    // The codes a trit count leaves unused. This is the substrate tax on the
    // exponent field, in the same units the rest of the numeric line uses.
    fn trit_waste(n: u32) -> u32 {
        if (trits_needed(n) == 3) { return (THREE_POW_3 - n); }
        if (trits_needed(n) == 4) { return (THREE_POW_4 - n); }
        if (trits_needed(n) == 5) { return (THREE_POW_5 - n); }
        if (trits_needed(n) == 6) { return (THREE_POW_6 - n); }
        return 0;
    }

    // Does `n` land exactly on a power of three, i.e. pack with zero waste?
    fn packs_exactly(n: u32) -> bool {
        return (trit_waste(n) == 0);
    }

    // ---- Combinational port surface (T81: without this the module has no
    // boundary and synthesises to nothing) ----
    //
    // Round-trip a code through decode and encode. Exercises the bias path in
    // both directions and the NaN guard, in one function.
    fn on_comb(x: u32) -> u32 {
        if (e8m0_is_nan(x)) { return E8M0_NAN_CODE; }
        return e8m0_encode(e8m0_exponent(x));
    }

    // ---- Tests ----

    test one_is_code_one_two_seven
        given e = e8m0_exponent(E8M0_ONE)
        then e == 0

    test smallest_finite_is_minus_one_two_seven
        given e = e8m0_exponent(E8M0_MIN_FINITE)
        then e == -127

    test largest_finite_is_plus_one_two_seven
        given e = e8m0_exponent(E8M0_MAX_FINITE)
        then e == 127

    test nan_code_is_detected
        given r = e8m0_is_nan(E8M0_NAN_CODE)
        then r == true

    test max_finite_is_not_nan
        given r = e8m0_is_nan(E8M0_MAX_FINITE)
        then r == false

    test nan_code_is_not_finite
        given r = e8m0_is_finite(E8M0_NAN_CODE)
        then r == false

    test encode_zero_gives_one
        given c = e8m0_encode(0)
        then c == 127

    test encode_minus_one_two_seven
        given c = e8m0_encode(-127)
        then c == 0

    test encode_plus_one_two_seven
        given c = e8m0_encode(127)
        then c == 254

    // The guard, and the reason it exists: 2^128 has no E8M0 code, and returning
    // code 1 for it would scale a whole block by 2^-126.
    test encode_out_of_range_is_nan
        given c = e8m0_encode(128)
        then c == 255

    test encode_below_range_is_nan
        given c = e8m0_encode(-128)
        then c == 255

    // ---- Trit accounting ----

    test exponent_field_needs_six_trits
        given t = trits_needed(E8M0_FINITE_CODES)
        then t == 6

    test exponent_field_wastes_four_hundred_seventy_four
        given w = trit_waste(E8M0_FINITE_CODES)
        then w == 474

    test tnf17_offset_needs_exactly_four_trits
        given t = trits_needed(TNF17_OFFSET_VALUES)
        then t == 4

    test tnf17_offset_wastes_nothing
        given w = trit_waste(TNF17_OFFSET_VALUES)
        then w == 0

    // ---- Port surface ----

    test comb_round_trips_one
        given r = on_comb(E8M0_ONE)
        then r == 127

    test comb_round_trips_max_finite
        given r = on_comb(E8M0_MAX_FINITE)
        then r == 254

    test comb_passes_nan_through
        given r = on_comb(E8M0_NAN_CODE)
        then r == 255

    // ---- Invariants ----

    // The field holds 2^8 codes, of which exactly one is reserved.
    invariant one_code_is_reserved
        assert E8M0_FINITE_CODES + 1 == 256

    invariant bias_centres_the_range
        assert E8M0_BIAS * 2 == (E8M0_MAX_FINITE as i32)

    invariant one_sits_at_the_bias
        assert (E8M0_ONE as i32) == E8M0_BIAS

    invariant nan_is_the_code_above_max_finite
        assert E8M0_NAN_CODE == E8M0_MAX_FINITE + 1

    // THE RESULT. E8M0's exponent does not pack into trits and TNF17e's does.
    // Stated as an assertion so the contrast is checked at compile time rather
    // than asserted in a comment that can rot.
    invariant e8m0_exponent_does_not_pack_into_trits
        assert packs_exactly(E8M0_FINITE_CODES) == false

    invariant tnf17_offset_packs_exactly
        assert packs_exactly(TNF17_OFFSET_VALUES) == true

    // 243 < 255 < 729 -- the reason it needs six trits and cannot use five.
    invariant two_hundred_fifty_five_sits_between_the_powers
        assert THREE_POW_5 < E8M0_FINITE_CODES

    invariant two_hundred_fifty_five_is_below_three_to_the_six
        assert E8M0_FINITE_CODES < THREE_POW_6

    // The waste is the tax, and it is 65 percent of a six-trit field.
    invariant six_trit_field_is_mostly_unused
        assert trit_waste(E8M0_FINITE_CODES) > (E8M0_FINITE_CODES + 200)

    // ---- Bench ----

    bench e8m0_decode_encode
        assert e8m0_exponent(E8M0_ONE) == 0
        assert e8m0_encode(0) == E8M0_ONE
        assert on_comb(E8M0_MAX_FINITE) == E8M0_MAX_FINITE
}

// phi^2 + 1/phi^2 = 3 | TRINITY

Open the lesson's spec in the player ↗

All lessons

• Module 1 · The chip

  What an FPGA is, which chip we use, and how its pins meet the board.

  1. 01 An FPGA is a grid you configure
  2. 02 Which chip is this?
  3. 03 Pins, balls and the package

• Module 2 · Numbers in hardware

  Bits, trits and number formats, and what arithmetic costs in logic.

  1. 04 Bits, trits and GF16
  2. 05 What arithmetic costs
  3. 06 How much fits on the chip

• Module 3 · Your t27 program

  Write a spec, test it, and see why compiling is not the same as being right.

  1. 07 Hello, t27
  2. 08 Tests are part of the spec
  3. 09 Compiles is not the same as correct

• Module 4 · Inside t27c

  How the compiler reads a spec and what it writes, including the native t27b.

  1. 10 The stages of t27c
  2. 11 t27c on a real machine
  3. 12 Seven backends, and t27b

• Module 5 · From spec to hardware

  The Verilog t27c writes, the cells it becomes, and what one LUT does.

  1. 13 From a spec to Verilog
  2. 14 Count the cells
  3. 15 One LUT, up close

• Module 6 · Reading synthesis

  What yosys reports about your design, and which warnings matter.

  1. 16 Synthesis warnings that matter
  2. 17 State machines
  3. 18 Where the LUTs go

• Module 7 · Place, route, timing

  Where the cells land on the die, and whether the clock is met.

  1. 19 Placement: where the cells land
  2. 20 Logic depth
  3. 21 Timing and slack

• Module 8 · The bitstream

  How a routed design becomes the bits the chip loads, with no Vivado.

  1. 22 From FASM to frames
  2. 23 A build, itemised
  3. 24 Read a bitstream

• Module 9 · On the board

  Ask the chip who it is, load the bits, and check them.

  1. 25 JTAG asks the chip
  2. 26 The same bits, on the board
  3. 27 Capstone: out-guess yosys

• Module 10 · Lab: our own research

  A number format of our own, an honest scoreboard, and a model's tables multiplied on the board.

  1. 28 T27: a number format of our own
  2. 29 An honest scoreboard
  3. 30 A model's tables on the board

• Module 11 · 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.

  1. 31 One scale for a block of weights
  2. 32 The scale byte on a real machine
  3. 33 One outlier, many zeros