GF4: четыре бита

Вы узнаете

Самый маленький GoldenFloat: один бит знака, один бит порядка, два бита мантиссы, смещение 0.

Попробуйте

Найдите EXP_BIAS и PHI_DISTANCE в gf4.t27, затем инвариант, который ограничивает расстояние. Откройте функцию decode и найдите два масштаба, которые даёт один бит порядка.

specs/numeric/gf4.t27

// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/gf4.t27
// GoldenFloat4 — 4-bit φ-structured floating point
// NUMERIC-STANDARD-001 — Agent 2 (P1)

module GF4 {
    // Import base format family
    use numeric::goldenfloat_family;
    use numeric::phi_ratio;

    // ═════════════════════════════════════════════════════════════════
    // 1. Format Definition
    // ═════════════════════════════════════════════════════════════════════════

    // GF4 bit layout: [S|E|MM]
    //   S: 1 bit  (sign)
    //   E: 1 bit  (exponent)
    //   M: 2 bits (mantissa)

    const BITS : u8 = 4;
    const SIGN_BITS : u8 = 1;
    const EXP_BITS : u8 = 1;
    const MANT_BITS : u8 = 2;

    // Bias for exponent (0-biased for GF4)
    const EXP_BIAS : u8 = 0;

    // φ-ratio: exp/mant = 1/2 = 0.5 (phi_distance = 0.118)
    const PHI_DISTANCE : f64 = 0.1180339887498949;

    // ═════════════════════════════════════════════════════════════════
    // 2. GoldenFloat4 Type
    // ═════════════════════════════════════════════════════════════════════════

    struct GF4 {
        raw : u4,  // 4-bit raw value
    }

    // ═════════════════════════════════════════════════════════════════
    // 3. Encoding/Decoding
    // ═════════════════════════════════════════════════════════════════════════

    // Encode f32 to GF4
    fn encode(value: f32) -> GF4 {
        // Special cases
        if (value == 0.0) {
            return GF4{ raw = 0b0000 };
        }
        if (value < 0.0) {
            const pos = encode(-value).raw;
            return GF4{ raw = pos | 0b1000 };  // Set sign bit
        }

        // For GF4, quantize to available values
        // Available positive values (mant * exp_scale):
        // mant=0.00, exp=1.0 → 0.00
        // mant=0.25, exp=1.0 → 0.25
        // mant=0.50, exp=1.0 → 0.50
        // mant=0.75, exp=1.0 → 0.75
        // mant=0.00, exp=2.0 → 0.00
        // mant=0.25, exp=2.0 → 0.50
        // mant=0.50, exp=2.0 → 1.00
        // mant=0.75, exp=2.0 → 1.50

        // Unique positive non-zero values: 0.25, 0.5, 0.75, 1.0, 1.5

        if (value <= 0.375) {
            // 0.25
            return GF4{ raw = 0b0001 };
        } else if (value <= 0.625) {
            // 0.5
            return GF4{ raw = 0b0010 };
        } else if (value <= 0.875) {
            // 0.75
            return GF4{ raw = 0b0011 };
        } else if (value <= 1.25) {
            // 1.0
            return GF4{ raw = 0b0101 };
        } else {
            // 1.5 (max)
            return GF4{ raw = 0b0111 };
        }
    }

    // Decode GF4 to f32
    fn decode(gf: GF4) -> f32 {
        const sign_bit = (gf.raw & 0b1000) != 0;
        const exp_bit = (gf.raw & 0b0100) != 0;
        const mant_bits = gf.raw & 0b0011;

        // Zero
        if (gf.raw == 0) {
            return 0.0;
        }

        // Decode mantissa (2 bits → values 0, 0.25, 0.5, 0.75)
        const mant = (mant_bits as f32) / 4.0;

        // Decode exponent (1 bit → 1.0 or 2.0)
        const exp_scale = if (exp_bit) { 2.0 } else { 1.0 };

        const value = mant * exp_scale;

        if (sign_bit) {
            return -value;
        }
        return value;
    }

    // ═════════════════════════════════════════════════════════════════
    // 4. Format Properties
    // ═════════════════════════════════════════════════════════════════════════

    fn max_value() -> f32 {
        // Max: mant=0.75, exp=2.0 → 1.5
        return 1.5;
    }

    fn min_positive() -> f32 {
        // Min positive: mant=0.25, exp=1.0 → 0.25
        return 0.25;
    }

    fn epsilon() -> f32 {
        // Smallest representable difference at 1.0
        return 0.25;
    }

    // ═════════════════════════════════════════════════════════════════
    // 5. Validation
    // ═════════════════════════════════════════════════════════════════════════

    fn validate_format() -> bool {
        // Check that we match the goldenfloat_family definition
        const fmt = goldenfloat_family::get_format_by_name("GF4");
        return (fmt != null) &&
               (fmt.?.bits == BITS) &&
               (fmt.?.exp_bits == EXP_BITS) &&
               (fmt.?.mant_bits == MANT_BITS);
    }

    // ═════════════════════════════════════════════════════════════════
    // 6. Use Cases
    // ═════════════════════════════════════════════════════════════════════════

    // GF4 is optimal for:
    // - Extreme compression (87.5% smaller than FP32)
    // - Binary/ternary classification
    // - Attention masks
    // - Activation sparsity indicators

    // Memory: 4 bits = 0.5 bytes (8x FP32 in same space)
    const MEMORY_RATIO_VS_FP32 : f32 = 4.0 / 32.0;  // 0.125

    // ═══════════════════════════════════════════════════════════════════════════════════════════════════════
    // TDD-Inside-Spec: Tests and Invariants for GF4
    // ═══════════════════════════════════════════════════════════════════════════════════════════════════════

    test gf4_decode_zero
        given gf = GF4{ raw = 0b0000 }
        when value = decode(gf)
        then value == 0.0

    test gf4_decode_positive_max
        given gf = GF4{ raw = 0b0111 }
        when value = decode(gf)
        then value == 1.5

    test gf4_decode_negative
        given gf = GF4{ raw = 0b1001 }
        when value = decode(gf)
        then value < 0.0

    test gf4_encode_zero_roundtrip
        given original = 0.0
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then decoded == original

    test gf4_encode_0_25
        given original = 0.25
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 0.25) < 0.01

    test gf4_encode_0_5
        given original = 0.5
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 0.5) < 0.01

    test gf4_encode_0_75
        given original = 0.75
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 0.75) < 0.01

    test gf4_encode_1_0
        given original = 1.0
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 1.0) < 0.01

    test gf4_encode_1_5
        given original = 1.5
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 1.5) < 0.01

    test gf4_encode_negative_values
        given original = -0.5
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then decoded < 0.0 and abs(decoded - (-0.5)) < 0.01

    test gf4_encode_clamps_to_max
        given original = 10.0
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then decoded <= 1.5

    test gf4_encode_quantization_small
        given original = 0.3
        and   encoded = encode(original)
        and   decoded = decode(encoded)
        then abs(decoded - 0.25) < 0.01

    test gf4_max_value_is_1_5
        given max_val = max_value()
        then max_val == 1.5

    test gf4_min_positive_is_0_25
        given min_pos = min_positive()
        then min_pos == 0.25

    test gf4_bits_sum_correct
        given total = SIGN_BITS + EXP_BITS + MANT_BITS
        then total == BITS

    test gf4_exp_mant_ratio_matches_phi_split
        given ratio = (EXP_BITS as f64) / (MANT_BITS as f64)
        and   expected = 0.5
        then abs(ratio - expected) < 0.01

    test gf4_memory_ratio_vs_fp32
        given ratio = MEMORY_RATIO_VS_FP32
        then ratio == 0.125

    test gf4_validate_format_success
        given valid = validate_format()
        then valid == true

    invariant gf4_bits_constant
        assert BITS == 4

    invariant gf4_sign_bits_is_one
        assert SIGN_BITS == 1

    invariant gf4_exp_bits_is_one
        assert EXP_BITS == 1

    invariant gf4_mant_bits_is_two
        assert MANT_BITS == 2

    invariant gf4_max_value_positive
        assert max_value() > 0.0

    invariant gf4_min_positive_greater_than_zero
        assert min_positive() > 0.0

    invariant gf4_epsilon_positive
        assert epsilon() > 0.0

    invariant gf4_max_ge_min_positive
        assert max_value() >= min_positive()

    invariant gf4_phi_distance_within_tolerance
        assert PHI_DISTANCE < 0.12

    invariant gf4_encode_decode_roundtrip
        given encoded = encode(x) for x in {0.25, 0.5, 0.75, 1.0, 1.5}
        when decoded = decode(encoded)
        then abs(decoded - x) < 0.01

    invariant gf4_encode_zero_returns_zero
        assert encode(0.0).raw == 0b0000

    invariant gf4_encode_positive_no_sign_bit
        given result = encode(1.0)
        when has_sign = (result.raw & 0b1000) != 0
        then has_sign == false

    invariant gf4_encode_negative_has_sign_bit
        given result = encode(-1.0)
        when has_sign = (result.raw & 0b1000) != 0
        then has_sign == true

    bench gf4_encode_latency
        measure: nanoseconds to encode(1.0)
        target: < 100ns

    bench gf4_decode_latency
        measure: nanoseconds to decode(GF4{raw = 0b0101})
        target: < 50ns
}

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

Все уроки

• Модуль 1 · Правило и его числа

  Одно правило делит каждую ширину, отношение, к которому оно стремится, и числа Люка за тройкой 3.

  1. 01 Число с плавающей точкой, разрезанное по phi
  2. 02 Phi как отношение
  3. 03 Числа Люка остаются целыми

• Модуль 2 · Почему phi, почему три

  Почему деление идёт по phi, почему основание три и как спека проверяет, что GF16 хранит phi.

  1. 04 Почему деление по phi
  2. 05 Почему основание три
  3. 06 Phi в шестнадцати битах

• Модуль 3 · Малые ступени: от GF4 до GF8

  GF4, GF6 и GF8 — меньше всего битов, и округление до целых битов стоит здесь дороже всего.

  1. 07 GF4: четыре бита
  2. 08 GF6: шесть битов
  3. 09 GF8: один байт

• Модуль 4 · От десяти до четырнадцати битов

  GF10, GF12 и GF14 и то, как расстояние до 1 / phi меняется с ростом слова.

  1. 10 GF10: десять битов
  2. 11 GF12: двенадцать битов
  3. 12 GF14: четырнадцать битов

• Модуль 5 · GF16 в работе

  Основной 16-битный формат, скалярное произведение из двух слагаемых в GF-T16, затем GF20 и GF24.

  1. 13 GF16: основной формат
  2. 14 Два произведения, одна сумма
  3. 15 GF20 и GF24

• Модуль 6 · От GF32 до GF64

  GF32 рядом с IEEE single, GF48 без пары в IEEE, GF64 рядом с IEEE double.

  1. 16 GF32: одинарная точность
  2. 17 GF48: сорок восемь битов
  3. 18 GF64: двойная точность

• Модуль 7 · От GF96 до GF256

  GF96, GF128 и GF256, где спеки держат раскладку инвариантами.

  1. 19 GF96: девяносто шесть битов
  2. 20 GF128: четверная точность
  3. 21 GF256: двести пятьдесят шесть битов

• Модуль 8 · Самые широкие ступени, затем триты

  GF512 и GF1024, две самые широкие ступени, затем GF-T8, где порядок уходит в триты.

  1. 22 GF512: пятьсот двенадцать битов
  2. 23 GF1024: один килобит
  3. 24 GF-T8: порядок в тритах

• Модуль 9 · Ещё триты, затем декодирование

  GF-T16 и GF-T32, затем почему фиксированные поля декодируются параллельно, а posit — нет.

  1. 25 GF-T16: шесть тритов
  2. 26 GF-T32: двенадцать тритов
  3. 27 Раскодировать за один шаг