Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 7 additions & 7 deletions .trinity/seals/Formats.json
Original file line number Diff line number Diff line change
@@ -1,14 +1,14 @@
{
"gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c",
"gen_hash_rust": "sha256:c2308d6bdaf84065b67074f1171706f7551009a14c7ac751e0f0b6a82b4e2ee1",
"gen_hash_verilog": "sha256:e2e287dcc092af6489366350edddc6da283b9ef2a0d540aae3d9c3c58b334fc5",
"gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b",
"gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e",
"gen_hash_rust": "sha256:8068e00e78c5781b2f5713197a5316c240491b2ad195db5806f8b3ff72ae6b2e",
"gen_hash_verilog": "sha256:b01c3b9a08bdbabf642292fe1dec44815984fe63d9b533a347592105f1cf9efb",
"gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02",
"module": "Formats",
"ring": 12,
"sealed_at": "2026-10-04T10:29:26Z",
"spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8",
"sealed_at": "2026-10-06T14:10:41Z",
"spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c",
"spec_path": "specs/numeric/formats.t27",
"tests": {
"blocked": "does not compile: /var/folders/yt/_nxm8bn90wd6y67z19vg_6bh0000gn/T/t27c-test-report-formats-60959/gf16.zig:1:1: error: unable to load 'gf16.zig': FileNotFound"
"blocked": "does not compile: /tmp/t27c-test-report-formats-3840268/spec.zig:30:5: error: not yet implemented"
}
}
14 changes: 7 additions & 7 deletions .trinity/seals/numeric_Formats.json
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
{
"gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c",
"gen_hash_rust": "sha256:c2308d6bdaf84065b67074f1171706f7551009a14c7ac751e0f0b6a82b4e2ee1",
"gen_hash_verilog": "sha256:e2e287dcc092af6489366350edddc6da283b9ef2a0d540aae3d9c3c58b334fc5",
"gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b",
"gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e",
"gen_hash_rust": "sha256:8068e00e78c5781b2f5713197a5316c240491b2ad195db5806f8b3ff72ae6b2e",
"gen_hash_verilog": "sha256:b01c3b9a08bdbabf642292fe1dec44815984fe63d9b533a347592105f1cf9efb",
"gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02",
"module": "Formats",
"ring": 12,
"sealed_at": "2026-10-04T10:29:26Z",
"sealed_at": "2026-10-06T14:10:41Z",
"sealed_by": "t27c-bootstrap@0.4.0",
"spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8",
"spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c",
"spec_path": "specs/numeric/formats.t27",
"tests": {
"blocked": "does not compile: /var/folders/yt/_nxm8bn90wd6y67z19vg_6bh0000gn/T/t27c-test-report-formats-60959/gf16.zig:1:1: error: unable to load 'gf16.zig': FileNotFound"
"blocked": "does not compile: /tmp/t27c-test-report-formats-3840268/spec.zig:30:5: error: not yet implemented"
}
}
11 changes: 11 additions & 0 deletions docs/now/2026-10-04-ring-096-and-formats-t27-agree-on-f32.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
# NOW -- ring-096 and formats.t27 agree on f32 (2026-10-04)

## ring-096 and formats.t27 agree on f32 (Closes #5746)

- decided by the law, not by taste: Constitution Article SSOT-MATH gives numeric meaning "one normative source of truth: specifications in the t27 language", and the numeric SSOT codec in `specs/numeric/gf16.t27` (L6) crosses the float boundary as `f32` -- `gf16_encode_f32(f32)`, `gf16_decode_to_f32(GF16) f32`
- `specs/numeric/formats.t27`: `gf16_to_f32`, `ternary_to_f32` and `quantize_value` returned `gf16` (lowers to `u16`, an encoding) and now return `f32`; inputs were already `f32`
- its tests unwrapped results with `gf16.to_f64(...)`, which gf16.t27 does not declare; they now compare f32 directly. `gf16_to_f32_normal_one` used `0x3C00` (e=30, i.e. 0.5 -- binary16's 1.0) and now uses GF16's `0x3E00` (FORMAT-SPEC-001.json: bias 31, so 1.0 is E=31); `ternary_to_f32_is_inverse` claimed 0.5 survives the trip and now ranges over trits
- `rings/ring-096-rust`: the five functions take and return `f32` instead of `f64`; a new test re-encodes every one of the 63,488 normal GF16 codes through the f32 boundary and gets the same 16 bits back (43 tests pass, was 42)
- `check_ring_spec_drift.py`: ring-096 DRIFTED (differing 5, rc 1) -> CONVERGED (differing 0, rc 0); both formats seals resealed (tests BLOCKED: the spec's functions have no bodies, before and after)
- not fixed, now visible: as a CONVERGED pair ring-096 enters the differential step, which exits 2 on it -- gen-rust emits the spec's `u5`/`u4` consts verbatim, `Trit`/`Format` cannot be synthesised, the spec side is `unimplemented!()`, and the harness compares f32 with `==`, so code 0xFFFF (NaN on both sides) would read as a disagreement; all four are outside this issue's boundary
- left open, outside the boundary: gf16.t27 is not self-consistent -- its decode formula puts 1.0 at `0x3E00`, its `pow2_table` and `gf16_from_components` tests say `0x3C00`; its NaN is `0xFE01` where formats.t27 and the ring use `0x7F01`
14 changes: 9 additions & 5 deletions rings/ring-096-rust/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,17 @@ Mirrors `specs/numeric/formats.t27` byte-for-byte.
## Primitives

- **GF16 bit layout**: `SIGN_MASK=0x8000`, `EXP_MASK=0x7E00`, `MANT_MASK=0x01FF`, `BIAS=31`
- **`gf16_to_f32(u16) -> f64`** — decode: handles signed zero, denormals, normals, Inf, NaN
- **`f32_to_gf16(f64) -> u16`** — encode (round-to-nearest): handles signed zero, Inf, NaN, overflow, underflow
- **`f32_to_ternary(f64) -> Trit`** — ternary quantization with threshold 0.5
- **`ternary_to_f32(Trit) -> f64`** — convert ternary back to float
- **`gf16_to_f32(u16) -> f32`** — decode: handles signed zero, denormals, normals, Inf, NaN
- **`f32_to_gf16(f32) -> u16`** — encode (round-to-nearest): handles signed zero, Inf, NaN, overflow, underflow
- **`f32_to_ternary(f32) -> Trit`** — ternary quantization with threshold 0.5
- **`ternary_to_f32(Trit) -> f32`** — convert ternary back to float
- **`Format` enum** — `Fp32`, `Fp16`, `Bf16`, `Gf16`, `Ternary`
- **`format_bytes(Format) -> usize`** — byte size lookup
- **`quantize_value(f64, Format) -> f64`** — generic quantization utility
- **`quantize_value(f32, Format) -> f32`** — generic quantization utility

The float boundary is `f32`, as the spec declares and as the numeric SSOT codec
`specs/numeric/gf16.t27` does. It was `f64` until #5746, which is what
`tools/check_ring_spec_drift.py` reported as five drifted signatures.

## no_std math

Expand Down
89 changes: 60 additions & 29 deletions rings/ring-096-rust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,12 @@
// - Format enum + format_bytes + quantize_value utility
//
// no_std: no libm. All math via private helpers (pow_u64).
//
// Boundary type is f32, as the spec declares and as the numeric SSOT codec in
// specs/numeric/gf16.t27 does (gf16_encode_f32(f32) / gf16_decode_to_f32 -> f32).
// This crate used f64 at every boundary until #5746. Internally the encoder
// still normalises in f64: every f32 is exactly an f64, and every finite GF16
// value is exactly an f32, so neither widening nor narrowing loses a bit.

#![no_std]
#![deny(warnings)]
Expand All @@ -37,7 +43,7 @@ pub const EXP_MAX: u16 = 63;
pub const EXP_MIN: u16 = 0;

/// Threshold for ternary quantization: |w| > 0.5 -> +/-1.
pub const TERNARY_THRESHOLD: f64 = 0.5;
pub const TERNARY_THRESHOLD: f32 = 0.5;

// ============================================================================
// 2. Errors
Expand Down Expand Up @@ -143,23 +149,27 @@ fn fabs_no_std(x: f64) -> f64 {
}

/// Check NaN: x != x.
fn is_nan(x: f64) -> bool {
fn is_nan(x: f32) -> bool {
x != x
}

/// Infinity sentinel via f64::INFINITY.
const INF: f64 = f64::INFINITY;
const NEG_INF: f64 = f64::NEG_INFINITY;
/// Infinity sentinel via f32::INFINITY.
const INF: f32 = f32::INFINITY;
const NEG_INF: f32 = f32::NEG_INFINITY;

fn is_inf(x: f64) -> bool {
fn is_inf(x: f32) -> bool {
x == INF || x == NEG_INF
}

// ============================================================================
// 6. GF16 codec
// ============================================================================

/// Decode GF16 (u16) to f64 (we use f64 as the canonical decoded value).
/// Decode GF16 (u16) to f32.
///
/// The arithmetic is done in f64 and narrowed once at the end. The narrowing
/// is exact: a finite GF16 value has a 10-bit significand and an exponent in
/// [-39, 31], all of which an f32 represents without rounding.
///
/// Algorithm:
/// - Extract sign, exponent, mantissa.
Expand All @@ -168,34 +178,34 @@ fn is_inf(x: f64) -> bool {
/// - e=EXP_MAX, m=0 -> +/- Inf.
/// - e=EXP_MAX, m!=0 -> NaN.
/// - Normal: value = (-1)^s * (1 + m/2^9) * 2^(e - bias).
pub fn gf16_to_f32(x: u16) -> f64 {
pub fn gf16_to_f32(x: u16) -> f32 {
let s = (x & SIGN_MASK) >> SIGN_SHIFT;
let e = (x & EXP_MASK) >> EXP_SHIFT;
let m = x & MANT_MASK;
let sign = if s == 1 { -1.0_f64 } else { 1.0_f64 };

if e == EXP_MIN {
if m == 0 {
return sign * 0.0;
return (sign * 0.0) as f32;
}
// Denormal: (-1)^s * (m / 2^9) * 2^(1 - bias)
let mantissa = m as f64 / pow_u64(2.0, EXP_SHIFT as i32);
return sign * mantissa * pow_u64(2.0, 1 - BIAS);
return (sign * mantissa * pow_u64(2.0, 1 - BIAS)) as f32;
}

if e == EXP_MAX {
if m == 0 {
return if s == 1 { NEG_INF } else { INF };
}
return f64::NAN;
return f32::NAN;
}

// Normal: (-1)^s * (1 + m / 2^9) * 2^(e - bias)
let mantissa = 1.0 + (m as f64 / pow_u64(2.0, EXP_SHIFT as i32));
sign * mantissa * pow_u64(2.0, e as i32 - BIAS)
(sign * mantissa * pow_u64(2.0, e as i32 - BIAS)) as f32
}

/// Encode f64 to GF16 (u16), round-to-nearest.
/// Encode f32 to GF16 (u16), round-to-nearest.
///
/// Algorithm:
/// 1. Signed zero preserved.
Expand All @@ -204,7 +214,7 @@ pub fn gf16_to_f32(x: u16) -> f64 {
/// 4. Find e such that magnitude in [2^(e-bias), 2^(e-bias+1)).
/// 5. Mantissa = (mag / 2^(e - bias) - 1.0) * 2^9, round-to-nearest.
/// 6. Underflow -> 0 (with sign), overflow -> Inf.
pub fn f32_to_gf16(a: f64) -> u16 {
pub fn f32_to_gf16(a: f32) -> u16 {
// Signed zero
if a == 0.0 {
// distinguish -0 from +0
Expand All @@ -225,7 +235,10 @@ pub fn f32_to_gf16(a: f64) -> u16 {
}

let sign: u16 = if a < 0.0 { 1 } else { 0 };
let mag = fabs_no_std(a);
// Widened to f64 (exact), so the normalisation below is the arithmetic
// this crate has always done and `+ 0.5` before each truncating cast
// rounds exactly once (in f32 it can round first in the subnormal range).
let mag = fabs_no_std(a as f64);

// Find exponent e such that 2^(e - bias) <= mag < 2^(e - bias + 1)
// i.e. e - bias = floor(log2(mag))
Expand Down Expand Up @@ -283,8 +296,8 @@ pub fn f32_to_gf16(a: f64) -> u16 {
// 7. Ternary quantization
// ============================================================================

/// Quantize f64 to ternary using threshold 0.5.
pub fn f32_to_ternary(x: f64) -> Trit {
/// Quantize f32 to ternary using threshold 0.5.
pub fn f32_to_ternary(x: f32) -> Trit {
if x > TERNARY_THRESHOLD {
Trit::Pos
} else if x < -TERNARY_THRESHOLD {
Expand All @@ -294,8 +307,8 @@ pub fn f32_to_ternary(x: f64) -> Trit {
}
}

/// Convert ternary back to f64: -1, 0, +1.
pub fn ternary_to_f32(t: Trit) -> f64 {
/// Convert ternary back to f32: -1, 0, +1.
pub fn ternary_to_f32(t: Trit) -> f32 {
match t {
Trit::Pos => 1.0,
Trit::Zero => 0.0,
Expand All @@ -307,7 +320,7 @@ pub fn ternary_to_f32(t: Trit) -> f64 {
// 8. quantize_value utility
// ============================================================================

/// Quantize an f64 to the target format.
/// Quantize an f32 to the target format.
///
/// For Fp32 / Fp16 / Bf16 we model "preserve value within format precision"
/// by returning the original value (these formats are wider than GF16 in
Expand All @@ -316,7 +329,7 @@ pub fn ternary_to_f32(t: Trit) -> f64 {
///
/// For Gf16: round-trip via GF16 codec.
/// For Ternary: round-trip via f32_to_ternary / ternary_to_f32.
pub fn quantize_value(x: f64, fmt: Format) -> f64 {
pub fn quantize_value(x: f32, fmt: Format) -> f32 {
match fmt {
Format::Fp32 | Format::Fp16 | Format::Bf16 => x,
Format::Gf16 => gf16_to_f32(f32_to_gf16(x)),
Expand Down Expand Up @@ -451,21 +464,39 @@ mod tests {

#[test]
fn f32_to_gf16_nan() {
assert_eq!(f32_to_gf16(f64::NAN), 0x7F01);
assert_eq!(f32_to_gf16(f32::NAN), 0x7F01);
}

#[test]
fn f32_to_gf16_roundtrip_normal_values() {
// Roundtrip various normal values within 1% tolerance.
let values = [1.5_f64, 2.0, 0.5, -1.5, 100.0, -100.0, 0.125];
let values = [1.5_f32, 2.0, 0.5, -1.5, 100.0, -100.0, 0.125];
for &v in &values {
let enc = f32_to_gf16(v);
let dec = gf16_to_f32(enc);
let err = fabs_no_std(dec - v) / fabs_no_std(v);
let err = fabs_no_std((dec - v) as f64) / fabs_no_std(v as f64);
assert!(err < 0.01, "v={} dec={} rel_err={}", v, dec, err);
}
}

#[test]
fn f32_boundary_is_lossless_for_every_normal_code() {
// The boundary type is f32 (#5746). That is only safe if no finite
// normal GF16 code is changed by passing through it: decode to f32,
// encode back, and get the same 16 bits -- for all 2 * 62 * 512 codes.
let mut checked = 0u32;
for x in 0u32..=0xFFFF {
let x = x as u16;
let e = (x & EXP_MASK) >> EXP_SHIFT;
if e == EXP_MIN || e == EXP_MAX {
continue;
}
assert_eq!(f32_to_gf16(gf16_to_f32(x)), x, "code {:#06x}", x);
checked += 1;
}
assert_eq!(checked, 2 * 62 * 512);
}

// ---- Ternary ----

#[test]
Expand Down Expand Up @@ -619,9 +650,9 @@ mod tests {
let pre = phi_sq + phi_inv_sq;
assert!((pre - 3.0).abs() < 1e-9);

// Round-trip through GF16 codec
let enc_a = f32_to_gf16(phi_sq);
let enc_b = f32_to_gf16(phi_inv_sq);
// Round-trip through GF16 codec (the codec boundary is f32)
let enc_a = f32_to_gf16(phi_sq as f32);
let enc_b = f32_to_gf16(phi_inv_sq as f32);
let dec_a = gf16_to_f32(enc_a);
let dec_b = gf16_to_f32(enc_b);

Expand All @@ -634,8 +665,8 @@ mod tests {
);

// Also exercise quantize_value route
let q_a = quantize_value(phi_sq, Format::Gf16);
let q_b = quantize_value(phi_inv_sq, Format::Gf16);
let q_a = quantize_value(phi_sq as f32, Format::Gf16);
let q_b = quantize_value(phi_inv_sq as f32, Format::Gf16);
assert!((q_a + q_b - 3.0).abs() < 0.03);
}
}
Loading
Loading