GF12: двенадцать битов
Вы узнаете
GoldenFloat в двенадцать битов, 1 + 4 + 7, смещение 7, и как имя теста может обещать больше, чем его проверка.
gf12.t27 держит 12 битов: 1 бит знака, 4 бита порядка, 7 битов мантиссы и смещение 7. Его отношение E / M равно 4 / 7 = 0.571, а PHI_DISTANCE равно 0.0466. Тест, который это проверяет, называется gf12_phi_distance_lowest, но утверждает лишь, что расстояние меньше 0.05, а комментарий в спеке называет GF12 ближайшим из всех форматов. Семейство говорит иначе: GF14 в следующем уроке стоит в 0.007 от 1 / phi, а GF32 в 0.0135. Читайте тест по его assert, а не по имени. MEMORY_RATIO_VS_FP32 равно 12 / 32 = 0.375.
Попробуйте
Найдите PHI_DISTANCE и тест gf12_phi_distance_lowest в gf12.t27. Затем сравните расстояние с GF14 и GF32 и скажите, что обещает имя теста, чего не проверяет его assert.
GF12: 12 bits as the spec lays them out, read from gf12.t27. Lesson 11 of the GoldenFloat course.
specs/numeric/gf12.t27
// SPDX-License-Identifier: Apache-2.0
// t27/specs/numeric/gf12.t27
// GoldenFloat12 — 12-bit φ-structured floating point
// NUMERIC-STANDARD-001 — Agent 4 (P1)
module GF12 {
// Import base format family
use numeric::goldenfloat_family;
use numeric::phi_ratio;
// ═════════════════════════════════════════════════════════════════
// 1. Format Definition
// ═════════════════════════════════════════════════════════════════════════
// GF12 bit layout: [S|EEEE|MMM MMMM]
// S: 1 bit (sign)
// E: 4 bits (exponent)
// M: 7 bits (mantissa)
const BITS : u8 = 12;
const SIGN_BITS : u8 = 1;
const EXP_BITS : u8 = 4;
const MANT_BITS : u8 = 7;
// Bias for exponent (2^(4-1) - 1 = 7)
const EXP_BIAS : u8 = 7;
// φ-ratio: exp/mant = 4/7 ≈ 0.571 (phi_distance = 0.047)
// This is the closest to 1/φ among all formats
const PHI_DISTANCE : f64 = 0.04660512288042107;
// ═════════════════════════════════════════════════════════════════
// 2. GoldenFloat12 Type
// ═════════════════════════════════════════════════════════════════════════
struct GF12 {
raw : u16, // 12-bit value stored in u16
}
// ═════════════════════════════════════════════════════════════════
// 3. Encoding/Decoding
// ═════════════════════════════════════════════════════════════════════════
// Encode f32 to GF12
fn encode(value: f32) -> GF12 {
if (value == 0.0) {
return GF12{ raw = 0 };
}
const sign = if (value < 0.0) { 1 } else { 0 };
const abs_val = if (value < 0.0) { -value } else { value };
// Extract exponent (unbiased)
const exp_unbiased = floor_log2(abs_val) as i8;
const exp_biased = (exp_unbiased + EXP_BIAS as i8) as u8;
// Clamp exponent
const exp_clamped = clamp(exp_biased, 0, (1 << EXP_BITS) - 1);
// Extract mantissa (7 bits)
const mant = extract_mantissa(abs_val, exp_unbiased, MANT_BITS);
return GF12{
raw = ((sign as u16) << 11) | ((exp_clamped as u16) << MANT_BITS) | (mant as u16)
};
}
// Decode GF12 to f32
fn decode(gf: GF12) -> f32 {
const sign = (gf.raw >> 11) as u8;
const exp_biased = ((gf.raw >> MANT_BITS) & 0x0F) as u8;
const mant = (gf.raw & 0x7F) as u8;
// Zero
if (exp_biased == 0 && mant == 0) {
return 0.0;
}
// Exponent
const exp_unbiased = if (exp_biased == 0) {
-EXP_BIAS as i8 + 1
} else {
(exp_biased as i8) - EXP_BIAS as i8
};
// Mantissa
const mant_normalized = if (exp_biased == 0) {
(mant as f32) / 128.0
} else {
1.0 + (mant as f32) / 128.0
};
const value = mant_normalized * pow(2.0, exp_unbiased as f32);
if (sign != 0) {
return -value;
}
return value;
}
// ═════════════════════════════════════════════════════════════════
// 4. Format Properties
// ═════════════════════════════════════════════════════════════════════════
fn max_value() -> f32 {
const mant_max = 1.0 + 127.0 / 128.0;
const exp_max = (1 << EXP_BITS) - 1 - EXP_BIAS;
return mant_max * pow(2.0, exp_max as f32);
}
fn min_positive() -> f32 {
const mant_min = 1.0 / 128.0;
const exp_min = -EXP_BIAS as i8 + 1;
return mant_min * pow(2.0, exp_min as f32);
}
fn epsilon() -> f32 {
return 1.0 / 128.0; // 0.0078125
}
// ═════════════════════════════════════════════════════════════════
// 5. Validation
// ═════════════════════════════════════════════════════════════════════════
fn validate_format() -> bool {
const fmt = goldenfloat_family::get_format_by_name("GF12");
return (fmt != null) &&
(fmt.?.bits == BITS) &&
(fmt.?.exp_bits == EXP_BITS) &&
(fmt.?.mant_bits == MANT_BITS);
}
// ═════════════════════════════════════════════════════════════════
// 6. Use Cases
// ═════════════════════════════════════════════════════════════════════════
// GF12 is optimal for:
// - Best φ-approximation (lowest phi_distance)
// - High-precision quantization
// - Critical path weights
// - Attention matrices
// Memory: 12 bits = 1.5 bytes (~2.67x FP32 in same space)
const MEMORY_RATIO_VS_FP32 : f32 = 12.0 / 32.0; // 0.375
// ═════════════════════════════════════════════════════════════════
// 7. Helper Functions
// ═════════════════════════════════════════════════════════════════════════
fn floor_log2(x: f32) -> i8 {
if (x <= 0.0) { return -128; }
let mut exp : i8 = 0;
while (x >= 2.0) {
x = x / 2.0;
exp = exp + 1;
}
while (x < 1.0) {
x = x * 2.0;
exp = exp - 1;
}
return exp;
}
fn extract_mantissa(value: f32, exp: i8, mant_bits: u8) -> u8 {
const normalized = value / pow(2.0, exp as f32);
const frac = normalized - 1.0;
const max_mant = (1 << mant_bits) - 1;
return (frac * (max_mant as f32 + 1.0)) as u8;
}
fn clamp(x: u8, min: u8, max: u8) -> u8 {
if (x < min) { return min; }
if (x > max) { return max; }
return x;
}
fn pow(base: f32, exp: f32) -> f32 {
// Efficient power function for GF12
// Integer exponent: binary exponentiation
// Fractional exponent: use logarithm approximation
if (base <= 0.0 || exp == 0.0) {
if (exp == 0.0) {
return 1.0;
}
if (base == 0.0 && exp > 0.0) {
return 0.0;
}
return 0.0 / 0.0; // NaN for negative base with non-integer exp
}
// Check if exponent is (approximately) integer
const is_integer = exp == floor(exp);
if (is_integer) {
// Binary exponentiation for integer exponents
let exp_int = exp as i32;
let mut result = 1.0;
let mut base_acc = base;
let mut e = exp_int;
if (e < 0) {
e = -e;
base_acc = 1.0 / base_acc;
}
while (e > 0) {
if (e % 2 == 1) {
result = result * base_acc;
}
base_acc = base_acc * base_acc;
e = e / 2;
}
return result;
}
// Fractional exponent: x^y = exp(y * ln(x))
const ln_val = ln_approx(base);
return exp_approx(exp * ln_val);
}
// Natural logarithm approximation
fn ln_approx(x: f32) -> f32 {
if (x <= 0.0) {
return 0.0 / 0.0; // NaN
}
if (x == 1.0) {
return 0.0;
}
// Series: ln(x) = 2 * ((x-1)/(x+1) + 1/3*((x-1)/(x+1))^3 + ...)
const t = (x - 1.0) / (x + 1.0);
const t2 = t * t;
const t3 = t2 * t;
const t5 = t3 * t2;
const t7 = t5 * t2;
return 2.0 * (t + t3 / 3.0 + t5 / 5.0 + t7 / 7.0);
}
// Exponential approximation
fn exp_approx(x: f32) -> f32 {
if (x == 0.0) {
return 1.0;
}
// Taylor series: e^x = 1 + x + x^2/2! + x^3/3! + ...
let mut result = 1.0;
let mut term = 1.0;
let mut exp_x = x;
// Scale down for large inputs
if (exp_x > 5.0 || exp_x < -5.0) {
const k = floor(exp_x / 5.0) as i32;
exp_x = exp_x - (k as f32) * 5.0;
}
for (i in 1..=8) {
term = term * exp_x / (i as f32);
result = result + term;
}
// Scale back if needed
if (x > 5.0 || x < -5.0) {
const k = floor(x / 5.0) as i32;
if (k > 0) {
for (i in 0..k) {
result = result * exp_approx(5.0);
}
} else if (k < 0) {
for (i in k..0) {
result = result / exp_approx(5.0);
}
}
}
return result;
}
// Floor function
fn floor(x: f32) -> f32 {
let xi = x as i32;
if (x >= 0.0 || x == xi as f32) {
return xi as f32;
}
return (xi - 1) as f32;
}
// ═══════════════════════════════════════════════════════════════════════════════════════════════════════
// TDD-Inside-Spec: Tests and Invariants for GF12
// ═══════════════════════════════════════════════════════════════════════════════════════════════════════
test gf12_decode_zero
given gf = GF12{ raw = 0 }
when value = decode(gf)
then value == 0.0
test gf12_encode_zero_roundtrip
given original = 0.0
and encoded = encode(original)
and decoded = decode(encoded)
then decoded == original
test gf12_bits_sum_correct
given total = SIGN_BITS + EXP_BITS + MANT_BITS
then total == BITS
test gf12_max_value_positive
given max_val = max_value()
then max_val > 0.0
test gf12_min_positive_greater_than_zero
given min_pos = min_positive()
then min_pos > 0.0
test gf12_epsilon_positive
given eps = epsilon()
then eps > 0.0
test gf12_phi_distance_lowest
given phi_dist = PHI_DISTANCE
then phi_dist < 0.05
test gf12_memory_ratio_vs_fp32
given ratio = MEMORY_RATIO_VS_FP32
then abs(ratio - 0.375) < 0.01
test gf12_validate_format_success
given valid = validate_format()
then valid == true
test gf12_floor_log2_power_of_two
given log_result = floor_log2(8.0)
then log_result == 3
test gf12_extract_mantissa_in_range
given mant = extract_mantissa(1.5, 0, 7)
then mant < 128
invariant gf12_bits_constant
assert BITS == 12
invariant gf12_sign_bits_is_one
assert SIGN_BITS == 1
invariant gf12_exp_bits_is_four
assert EXP_BITS == 4
invariant gf12_mant_bits_is_seven
assert MANT_BITS == 7
invariant gf12_max_ge_min_positive
assert max_value() >= min_positive()
invariant gf12_phi_distance_below_threshold
assert PHI_DISTANCE < 0.05
invariant gf12_exp_bias_positive
assert EXP_BIAS > 0
test gf12_pow_zero_exponent_returns_one
given result = pow(2.0, 0.0)
then abs(result - 1.0) < 1e-6
test gf12_pow_one_exponent_returns_base
given result = pow(5.0, 1.0)
then abs(result - 5.0) < 1e-6
test gf12_pow_positive_integer_exponent
given result = pow(2.0, 5.0)
and expected = 32.0
then abs(result - expected) < 1e-5
test gf12_pow_negative_integer_exponent
given result = pow(2.0, -3.0)
and expected = 0.125
then abs(result - expected) < 1e-5
test gf12_pow_fractional_exponent
given result = pow(4.0, 0.5)
and expected = 2.0
then abs(result - expected) < 1e-4
test gf12_pow_zero_base_positive_exponent
given result = pow(0.0, 5.0)
then result == 0.0
test gf12_pow_one_base_any_exponent
given result1 = pow(1.0, 10.0)
and result2 = pow(1.0, -5.0)
then abs(result1 - 1.0) < 1e-6 and abs(result2 - 1.0) < 1e-6
test gf12_ln_approx_of_one
given result = ln_approx(1.0)
then abs(result) < 1e-6
test gf12_ln_approx_of_e
given e = 2.718281828459045 as f32
and result = ln_approx(e)
then abs(result - 1.0) < 0.01
test gf12_ln_approx_negative_returns_nan
given result = ln_approx(-1.0)
then result != result // NaN check
test gf12_exp_approx_zero
given result = exp_approx(0.0)
then abs(result - 1.0) < 1e-6
test gf12_exp_approx_one
given e = 2.718281828459045 as f32
and result = exp_approx(1.0)
then abs(result - e) < 0.01
test gf12_exp_approx_negative
given result = exp_approx(-1.0)
and expected = 1.0 / 2.718281828459045 as f32
then abs(result - expected) < 0.01
test gf12_floor_positive
given result = floor(3.7)
then abs(result - 3.0) < 1e-6
test gf12_floor_negative
given result = floor(-3.2)
then abs(result - (-4.0)) < 1e-6
test gf12_floor_integer
given result = floor(5.0)
then abs(result - 5.0) < 1e-6
invariant gf12_pow_zero_exponent_identity
// For every positive x; checked at three points, one on each side of 1.
given x1 = 0.5
and x2 = 2.5
and x3 = 7.0
assert abs(pow(x1, 0.0) - 1.0) < 1e-6 and abs(pow(x2, 0.0) - 1.0) < 1e-6 and abs(pow(x3, 0.0) - 1.0) < 1e-6
invariant gf12_pow_one_exponent_identity
// For every valid x; checked at three points.
given x1 = 0.5
and x2 = 2.5
and x3 = 7.0
assert abs(pow(x1, 1.0) - x1) < 1e-5 and abs(pow(x2, 1.0) - x2) < 1e-5 and abs(pow(x3, 1.0) - x3) < 1e-5
invariant gf12_ln_exp_inversion
given x = 2.0
and y = ln_approx(x)
then abs(exp_approx(y) - x) < 0.01
invariant gf12_floor_returns_integer
// floor returns a whole number, and the floor of a whole number is itself.
given r1 = floor(3.7)
and r2 = floor(-3.2)
assert abs(floor(r1) - r1) < 1e-6 and abs(floor(r2) - r2) < 1e-6
invariant gf12_floor_monotonic
given x1 = 2.5
and x2 = 3.5
assert floor(x1) <= floor(x2)
bench gf12_pow_integer_exponent
measure: nanoseconds to compute pow(2.0, 10.0)
target: < 500ns
bench gf12_ln_latency
measure: nanoseconds to compute ln_approx(2.0)
target: < 300ns
bench gf12_exp_latency
measure: nanoseconds to compute exp_approx(1.0)
target: < 500ns
bench gf12_floor_latency
measure: nanoseconds to compute floor(3.7)
target: < 50ns
invariant gf12_floor_log2_non_negative_input
assert floor_log2(1.0) >= 0
invariant gf12_extract_mantissa_in_valid_range
assert extract_mantissa(1.0, 0, 7) < 128
bench gf12_encode_latency
measure: nanoseconds to encode(1.0)
target: < 150ns
bench gf12_decode_latency
measure: nanoseconds to decode(GF12{raw = 1024})
target: < 100ns
}
Все уроки
Модуль 1 · Правило и его числа
Одно правило делит каждую ширину, отношение, к которому оно стремится, и числа Люка за тройкой 3.
Модуль 2 · Почему phi, почему три
Почему деление идёт по phi, почему основание три и как спека проверяет, что GF16 хранит phi.
Модуль 3 · Малые ступени: от GF4 до GF8
GF4, GF6 и GF8 — меньше всего битов, и округление до целых битов стоит здесь дороже всего.
Модуль 4 · От десяти до четырнадцати битов
GF10, GF12 и GF14 и то, как расстояние до 1 / phi меняется с ростом слова.
Модуль 5 · GF16 в работе
Основной 16-битный формат, скалярное произведение из двух слагаемых в GF-T16, затем GF20 и GF24.
Модуль 6 · От GF32 до GF64
GF32 рядом с IEEE single, GF48 без пары в IEEE, GF64 рядом с IEEE double.
Модуль 7 · От GF96 до GF256
GF96, GF128 и GF256, где спеки держат раскладку инвариантами.
Модуль 8 · Самые широкие ступени, затем триты
GF512 и GF1024, две самые широкие ступени, затем GF-T8, где порядок уходит в триты.
Модуль 9 · Ещё триты, затем декодирование
GF-T16 и GF-T32, затем почему фиксированные поля декодируются параллельно, а posit — нет.