GF12: twelve bits
You will learn
The twelve-bit GoldenFloat, 1 + 4 + 7, bias 7, and how a test name can promise more than its assert.
gf12.t27 holds 12 bits: 1 sign, 4 exponent, 7 mantissa bits, and bias 7. Its ratio E / M is 4 / 7 = 0.571, and PHI_DISTANCE is 0.0466. The test that checks it is named gf12_phi_distance_lowest, but it asserts only that the distance is under 0.05, and a comment in the spec calls GF12 the closest of all formats. The family says otherwise: GF14 in the next lesson sits 0.007 from 1 / phi, and GF32 0.0135. Read a test by its assert, not by its name. MEMORY_RATIO_VS_FP32 is 12 / 32 = 0.375.
Try it
Find PHI_DISTANCE and the test gf12_phi_distance_lowest in gf12.t27. Then compare the distance with GF14 and GF32 and say what the test name claims that its assert does not.
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
}
All lessons
Module 1 · The rule and its numbers
One rule splits every width, the ratio it aims at, and the Lucas numbers behind the 3.
Module 2 · Why phi, why three
Why the split is phi, why base three, and how a spec checks GF16 keeps phi.
Module 3 · The small rungs: GF4 to GF8
GF4, GF6 and GF8, the fewest bits, where rounding to whole bits costs the most.
Module 4 · Ten to fourteen bits
GF10, GF12 and GF14, and how the distance from 1 / phi moves as the word grows.
Module 5 · GF16 at work
The primary 16-bit format, a two-term dot product in GF-T16, then GF20 and GF24.
Module 6 · GF32 to GF64
GF32 beside IEEE single, GF48 with no IEEE twin, GF64 beside IEEE double.
Module 7 · GF96 to GF256
GF96, GF128 and GF256, where the specs hold the layout with invariants.
Module 8 · The widest rungs, then trits
GF512 and GF1024, the two widest rungs, then GF-T8, where the exponent moves to trits.
Module 9 · More trits, then the decode
GF-T16 and GF-T32, then why fixed fields decode in parallel and a posit does not.