From 61f7a60ec1bfd655f2a8a509d14829868ea7c051 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 4 Oct 2026 13:42:34 +0700 Subject: [PATCH 1/4] ring-096 and formats.t27 agree on f32 (Closes #5746) check_ring_spec_drift.py reported ring-096-rust DRIFTED against specs/numeric/formats.t27 on five functions. The constitution decides which side moves: Article SSOT-MATH gives numeric meaning "one normative source of truth: specifications in the t27 language", so the spec is the truth and the ring follows it. The spec itself was wrong in one place: gf16_to_f32, ternary_to_f32 and quantize_value returned `gf16` (a u16 encoding) while their names and callers mean a float. They now return f32, which is the boundary the L6 codec specs/numeric/gf16.t27 already uses (gf16_encode_f32(f32), gf16_decode_to_f32(GF16) f32). Its tests stop calling gf16.to_f64, which gf16.t27 does not declare; gf16_to_f32_normal_one uses 0x3E00, which is 1.0 under FORMAT-SPEC-001.json's GF16 bias 31 (0x3C00 is 0.5). rings/ring-096-rust moves its five functions from f64 to f32. A new test re-encodes all 63,488 normal GF16 codes through the f32 boundary and gets the same 16 bits back. 43 ring tests pass. Both formats seals resealed with `t27c seal specs/numeric/formats.t27 --save`. Drift: ring-096 DRIFTED (differing 5, rc 1) -> CONVERGED (differing 0, rc 0). Part of #5906. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/Formats.json | 17 +-- .trinity/seals/numeric_Formats.json | 17 +-- ...4-ring-096-and-formats-t27-agree-on-f32.md | 11 ++ rings/ring-096-rust/README.md | 14 ++- rings/ring-096-rust/src/lib.rs | 89 +++++++++----- specs/numeric/formats.t27 | 114 +++++++++--------- 6 files changed, 159 insertions(+), 103 deletions(-) create mode 100644 docs/now/2026-10-04-ring-096-and-formats-t27-agree-on-f32.md diff --git a/.trinity/seals/Formats.json b/.trinity/seals/Formats.json index ca1eaf0d94..527e721a1a 100644 --- a/.trinity/seals/Formats.json +++ b/.trinity/seals/Formats.json @@ -1,11 +1,14 @@ { - "gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c", - "gen_hash_rust": "sha256:08b0cc1498148250d7300020d922d7de55656e92afaa89f1b8b16593118dbb4e", - "gen_hash_verilog": "sha256:c47193ddf0dae29fa75b4a5b35d859edf515434b188a172e4e3aade69d7bb3f6", - "gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b", + "gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e", + "gen_hash_rust": "sha256:109f805147545d90154c5dd8e89625fac9c5ebe6d0a44a6d46f289b506afe956", + "gen_hash_verilog": "sha256:9affcbc25cc916b0fa16bab710b35c7124d1fae0184f80dd8d9a7350ec07907d", + "gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02", "module": "Formats", "ring": 12, - "sealed_at": "2026-09-24T14:54:04Z", - "spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8", - "spec_path": "specs/numeric/formats.t27" + "sealed_at": "2026-10-04T06:28:22Z", + "spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c", + "spec_path": "specs/numeric/formats.t27", + "tests": { + "blocked": "does not compile: /var/folders/cm/2n1qdh892xldd1rc2ly1jv8r0000gn/T/t27c-test-report-formats-47677/spec.zig:30:5: error: not yet implemented" + } } \ No newline at end of file diff --git a/.trinity/seals/numeric_Formats.json b/.trinity/seals/numeric_Formats.json index 901e265702..1e491982e3 100644 --- a/.trinity/seals/numeric_Formats.json +++ b/.trinity/seals/numeric_Formats.json @@ -1,12 +1,15 @@ { - "gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c", - "gen_hash_rust": "sha256:08b0cc1498148250d7300020d922d7de55656e92afaa89f1b8b16593118dbb4e", - "gen_hash_verilog": "sha256:c47193ddf0dae29fa75b4a5b35d859edf515434b188a172e4e3aade69d7bb3f6", - "gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b", + "gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e", + "gen_hash_rust": "sha256:109f805147545d90154c5dd8e89625fac9c5ebe6d0a44a6d46f289b506afe956", + "gen_hash_verilog": "sha256:9affcbc25cc916b0fa16bab710b35c7124d1fae0184f80dd8d9a7350ec07907d", + "gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02", "module": "Formats", "ring": 12, - "sealed_at": "2026-09-24T14:54:04Z", + "sealed_at": "2026-10-04T06:28:22Z", "sealed_by": "t27c-bootstrap@0.4.0", - "spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8", - "spec_path": "specs/numeric/formats.t27" + "spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c", + "spec_path": "specs/numeric/formats.t27", + "tests": { + "blocked": "does not compile: /var/folders/cm/2n1qdh892xldd1rc2ly1jv8r0000gn/T/t27c-test-report-formats-47677/spec.zig:30:5: error: not yet implemented" + } } \ No newline at end of file diff --git a/docs/now/2026-10-04-ring-096-and-formats-t27-agree-on-f32.md b/docs/now/2026-10-04-ring-096-and-formats-t27-agree-on-f32.md new file mode 100644 index 0000000000..aa120d50f7 --- /dev/null +++ b/docs/now/2026-10-04-ring-096-and-formats-t27-agree-on-f32.md @@ -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` diff --git a/rings/ring-096-rust/README.md b/rings/ring-096-rust/README.md index f2e01e5c9c..124ed10123 100644 --- a/rings/ring-096-rust/README.md +++ b/rings/ring-096-rust/README.md @@ -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 diff --git a/rings/ring-096-rust/src/lib.rs b/rings/ring-096-rust/src/lib.rs index a788dc5924..0f469100c5 100644 --- a/rings/ring-096-rust/src/lib.rs +++ b/rings/ring-096-rust/src/lib.rs @@ -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)] @@ -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 @@ -143,15 +149,15 @@ 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 } @@ -159,7 +165,11 @@ fn is_inf(x: f64) -> bool { // 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. @@ -168,7 +178,7 @@ 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; @@ -176,26 +186,26 @@ pub fn gf16_to_f32(x: u16) -> 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. @@ -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 @@ -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)) @@ -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 { @@ -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, @@ -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 @@ -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)), @@ -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] @@ -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); @@ -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); } } diff --git a/specs/numeric/formats.t27 b/specs/numeric/formats.t27 index f3a25b6800..69e563f9aa 100644 --- a/specs/numeric/formats.t27 +++ b/specs/numeric/formats.t27 @@ -43,9 +43,15 @@ module Formats { // Handles signed zero, denormals, normals, infinities, and NaN. // ======================================================================== - // gf16_to_f32(x: u16) -> gf16 + // gf16_to_f32(x: u16) -> f32 // Decode GF16 to f32 // + // The decoded value is an IEEE binary32 float, the same boundary type as + // the numeric SSOT codec in gf16.t27: gf16_decode_to_f32(GF16) f32 and + // gf16_encode_f32(f32) GF16, where GF16 = u16 (law L6). It was declared + // `-> gf16` here, which lowers to u16 -- an encoding, not a decoded value + // (#5746). + // // Algorithm: // 1. Extract sign (bit 15) // 2. Extract exponent (bits 14-9) and mantissa (bits 8-0) @@ -58,7 +64,7 @@ module Formats { // value = (-1)^s * (1 + m/2^9) * 2^(e - Bias) // // Complexity: O(1) - pub fn gf16_to_f32(x: u16) -> gf16 { } + pub fn gf16_to_f32(x: u16) -> f32 { } // ======================================================================== // 3. f32 -> GF16 (encode, round-to-nearest) @@ -100,12 +106,12 @@ module Formats { // Complexity: O(1) pub fn f32_to_ternary(x: f32) -> Trit { } - // ternary_to_f32(t: Trit) -> gf16 + // ternary_to_f32(t: Trit) -> f32 // Convert ternary to f32 // // Mapping: -1 -> -1.0, 0 -> 0.0, +1 -> 1.0 // Complexity: O(1) - pub fn ternary_to_f32(t: Trit) -> gf16 { } + pub fn ternary_to_f32(t: Trit) -> f32 { } // ======================================================================== // 5. Format Enum @@ -129,64 +135,68 @@ module Formats { // 6. Quantization Utility // ======================================================================== - // quantize_value(x: f32, fmt: Format) -> gf16 - // Quantize f32 to target format + // quantize_value(x: f32, fmt: Format) -> f32 + // Quantize f32 to target format: the value x takes after a round trip + // through fmt, returned as f32 (so quantize_value(x, .ternary) equals + // ternary_to_f32(f32_to_ternary(x))) // // Complexity: O(1) - pub fn quantize_value(x: f32, fmt: Format) -> gf16 { } + pub fn quantize_value(x: f32, fmt: Format) -> f32 { } // ======================================================================== // TDD - Tests // ======================================================================== + // + // gf16_to_f32, ternary_to_f32 and quantize_value return f32, so their + // results are compared as f32 directly. These tests used to unwrap them + // with `gf16.to_f64(...)`, which gf16.t27 does not declare (#5746). test gf16_to_f32_zero_positive { - // Verify: zero encodes to zero + // Verify: +0 decodes to +0.0 const x : u16 = 0; const result = gf16_to_f32(x); - assert(gf16.to_f64(result) == 0.0); + assert(result == 0.0); } test gf16_to_f32_zero_negative { - // Verify: negative zero encodes to -0 + // Verify: negative zero decodes to -0.0 const x : u16 = 0x8000; const result = gf16_to_f32(x); - assert(gf16.to_f64(result) == -0.0); + assert(result == -0.0); } test gf16_to_f32_denormal { // Verify: denormal value decodes to small positive const x : u16 = 0x0080; const result = gf16_to_f32(x); - const val = gf16.to_f64(result); - assert(val > 0.0 and val < 1.0); + assert(result > 0.0 and result < 1.0); } test gf16_to_f32_normal_one { - // Verify: 1.0 encodes correctly - const x : u16 = 0x3C00; + // Verify: 1.0 decodes correctly. 1.0 = 2^(31 - Bias) with m = 0, so + // its encoding is 31 << ExpShift = 0x3E00. (0x3C00 is e = 30, i.e. + // 0.5 -- the IEEE binary16 encoding of 1.0, not the GF16 one.) + const x : u16 = 0x3E00; const result = gf16_to_f32(x); - const decoded = gf16.to_f64(result); - assert(decoded == 1.0); + assert(result == 1.0); } test gf16_to_f32_positive_inf { - // Verify: positive infinity encodes correctly + // Verify: positive infinity decodes correctly const x : u16 = 0x7E00; const result = gf16_to_f32(x); - const decoded = gf16.to_f64(result); - assert(decoded == std.math.inf(f32)); + assert(result == std.math.inf(f32)); } test gf16_to_f32_negative_inf { - // Verify: negative infinity encodes correctly + // Verify: negative infinity decodes correctly const x : u16 = 0xFE00; const result = gf16_to_f32(x); - const decoded = gf16.to_f64(result); - assert(decoded == -std.math.inf(f32)); + assert(result == -std.math.inf(f32)); } test gf16_to_f32_nan { - // Verify: NaN encodes to NaN + // Verify: NaN decodes to NaN const x : u16 = 0x7F01; const result = gf16_to_f32(x); assert(result != result); // NaN check @@ -210,8 +220,7 @@ module Formats { // Verify: 1.0 encodes and roundtrips correctly const a : f32 = 1.0; const encoded = f32_to_gf16(a); - const decoded = gf16_to_f32(encoded); - const recovered = gf16.to_f64(decoded); + const recovered = gf16_to_f32(encoded); assert(recovered >= 0.99 and recovered <= 1.01); } @@ -275,24 +284,21 @@ module Formats { // Verify: pos maps to 1.0 const t : Trit = .pos; const result = ternary_to_f32(t); - const result_val = gf16.to_f64(result); - assert(result_val == 1.0); + assert(result == 1.0); } test ternary_to_f32_zero { // Verify: zero maps to 0.0 const t : Trit = .zero; const result = ternary_to_f32(t); - const result_val = gf16.to_f64(result); - assert(result_val == 0.0); + assert(result == 0.0); } test ternary_to_f32_negative { // Verify: neg maps to -1.0 const t : Trit = .neg; const result = ternary_to_f32(t); - const result_val = gf16.to_f64(result); - assert(result_val == -1.0); + assert(result == -1.0); } test format_bytes_fp32 { @@ -317,8 +323,7 @@ module Formats { // Verify: quantizing to fp32 preserves value const x : f32 = 1.5; const result = quantize_value(x, .fp32); - const result_val = gf16.to_f64(result); - assert(result_val >= 1.49 and result_val <= 1.51); + assert(result >= 1.49 and result <= 1.51); } test quantize_value_ternary { @@ -335,23 +340,22 @@ module Formats { invariant gf16_to_f32_preserves_zero { // Zero should decode to zero - assert(gf16.to_f64(gf16_to_f32(0)) == 0.0); - assert(gf16.to_f64(gf16_to_f32(0x8000)) == -0.0); + assert(gf16_to_f32(0) == 0.0); + assert(gf16_to_f32(0x8000) == -0.0); } invariant gf16_to_f32_preserves_infinity { // Infinity should decode to infinity - assert(gf16.to_f64(gf16_to_f32(0x7E00)) == std.math.inf(f32)); - assert(gf16.to_f64(gf16_to_f32(0xFE00)) == -std.math.inf(f32)); + assert(gf16_to_f32(0x7E00) == std.math.inf(f32)); + assert(gf16_to_f32(0xFE00) == -std.math.inf(f32)); } invariant f32_to_gf16_roundtrip_loss { // Roundtrip should be within tolerance for normal values - const original = gf16.from_f64(1.5); - const encoded = f32_to_gf16(gf16.to_f64(original)); - const decoded = gf16_to_f32(encoded); - const error = gf16.abs(gf16.sub(original, decoded)); - assert(gf16.to_f64(error) < gf16.from_f64(0.01)); + const original : f32 = 1.5; + const decoded = gf16_to_f32(f32_to_gf16(original)); + const err = decoded - original; + assert(err < 0.01 and err > -0.01); } invariant ternary_quantization_symmetric { @@ -360,18 +364,18 @@ module Formats { const n = f32_to_ternary(-0.5); const p_decoded = ternary_to_f32(p); const n_decoded = ternary_to_f32(n); - assert(gf16.to_f64(p_decoded) == -gf16.to_f64(n_decoded)); + assert(p_decoded == -n_decoded); } invariant ternary_to_f32_is_inverse { - // ternary_to_f32 is inverse of f32_to_ternary - const values = [5]f32{ -1.0, -0.5, 0.0, 0.5, 1.0 }; - for i in 0..5 { - const v = values[i]; - const t = f32_to_ternary(v); - const recovered = ternary_to_f32(t); - const diff = gf16.abs(gf16.sub(v, recovered)); - assert(gf16.eq(v, recovered) or (gf16.to_f64(diff) < gf16.from_f64(0.01))); + // f32_to_ternary is a left inverse of ternary_to_f32: every trit + // survives the trip through f32. The other direction does not hold -- + // 0.5 quantizes to zero and comes back as 0.0 -- which is why this + // ranges over trits, not over f32 values. + const trits = [3]Trit{ .neg, .zero, .pos }; + for i in 0..3 { + const t = trits[i]; + assert(f32_to_ternary(ternary_to_f32(t)) == t); } } @@ -390,8 +394,8 @@ module Formats { // Measure: cycles for gf16_to_f32 conversion // Target: < 50 cycles (simple bit extraction + lookup) @setEvalBranchQuota(10000); - var result : gf16; - const test_value: u16 = 0x3C00; + var result : f32; + const test_value: u16 = 0x3E00; for _ in 0..1000 { result = gf16_to_f32(test_value); } @@ -426,7 +430,7 @@ module Formats { // Measure: cycles for ternary_to_f32 conversion // Target: < 10 cycles (simple switch) @setEvalBranchQuota(10000); - var result : gf16; + var result : f32; const test_trit: Trit = .pos; for _ in 0..1000 { result = ternary_to_f32(test_trit); From dbb0fc5025a32a2ae219747d8b12d68d17096fc8 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Tue, 6 Oct 2026 21:07:46 +0700 Subject: [PATCH 2/4] chore(seals): take master's formats seals before merging master (Refs #5746) The two seal files conflict only because master's compiler changed the generated hashes (#5994, #5904); they are re-sealed against the merged tree in the next commit. Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/Formats.json | 14 +++++++------- .trinity/seals/numeric_Formats.json | 14 +++++++------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/.trinity/seals/Formats.json b/.trinity/seals/Formats.json index 527e721a1a..2470335b31 100644 --- a/.trinity/seals/Formats.json +++ b/.trinity/seals/Formats.json @@ -1,14 +1,14 @@ { - "gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e", - "gen_hash_rust": "sha256:109f805147545d90154c5dd8e89625fac9c5ebe6d0a44a6d46f289b506afe956", - "gen_hash_verilog": "sha256:9affcbc25cc916b0fa16bab710b35c7124d1fae0184f80dd8d9a7350ec07907d", - "gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02", + "gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c", + "gen_hash_rust": "sha256:c2308d6bdaf84065b67074f1171706f7551009a14c7ac751e0f0b6a82b4e2ee1", + "gen_hash_verilog": "sha256:e2e287dcc092af6489366350edddc6da283b9ef2a0d540aae3d9c3c58b334fc5", + "gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b", "module": "Formats", "ring": 12, - "sealed_at": "2026-10-04T06:28:22Z", - "spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c", + "sealed_at": "2026-10-04T10:29:26Z", + "spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8", "spec_path": "specs/numeric/formats.t27", "tests": { - "blocked": "does not compile: /var/folders/cm/2n1qdh892xldd1rc2ly1jv8r0000gn/T/t27c-test-report-formats-47677/spec.zig:30:5: error: not yet implemented" + "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" } } \ No newline at end of file diff --git a/.trinity/seals/numeric_Formats.json b/.trinity/seals/numeric_Formats.json index 1e491982e3..11859d5512 100644 --- a/.trinity/seals/numeric_Formats.json +++ b/.trinity/seals/numeric_Formats.json @@ -1,15 +1,15 @@ { - "gen_hash_c": "sha256:2fecf76cd99861843bab42a006620d609457aed840a6acc580e84007c2c8012e", - "gen_hash_rust": "sha256:109f805147545d90154c5dd8e89625fac9c5ebe6d0a44a6d46f289b506afe956", - "gen_hash_verilog": "sha256:9affcbc25cc916b0fa16bab710b35c7124d1fae0184f80dd8d9a7350ec07907d", - "gen_hash_zig": "sha256:a8e0d3be436fea959d7d3723d710829f9b792ecd178ab64e71f756cbe2af3d02", + "gen_hash_c": "sha256:c9019b00543b767b47295b362d186bf296173291efe97478d7dfc956896c2e8c", + "gen_hash_rust": "sha256:c2308d6bdaf84065b67074f1171706f7551009a14c7ac751e0f0b6a82b4e2ee1", + "gen_hash_verilog": "sha256:e2e287dcc092af6489366350edddc6da283b9ef2a0d540aae3d9c3c58b334fc5", + "gen_hash_zig": "sha256:9bbe3a67208d6b61260118c3407d51b2c58904eedd82737936347ab6f1c5121b", "module": "Formats", "ring": 12, - "sealed_at": "2026-10-04T06:28:22Z", + "sealed_at": "2026-10-04T10:29:26Z", "sealed_by": "t27c-bootstrap@0.4.0", - "spec_hash": "sha256:3b29f3303a263165da4a578331bbf07bb4960553d1173ef58d0f010077fd4d8c", + "spec_hash": "sha256:a4f199a6e60aee624ca0bb259ea60eef7162b0b017ddafef783723ad59fdddc8", "spec_path": "specs/numeric/formats.t27", "tests": { - "blocked": "does not compile: /var/folders/cm/2n1qdh892xldd1rc2ly1jv8r0000gn/T/t27c-test-report-formats-47677/spec.zig:30:5: error: not yet implemented" + "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" } } \ No newline at end of file From b18894484e2ce55e3e46e5f80b104f0a1266c4b1 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Tue, 6 Oct 2026 21:08:01 +0700 Subject: [PATCH 3/4] chore(policy): one-time exception for ring-096 lib.rs (Refs #5746) #5921 carries the owner-approved-foreign label; the pre-push hook reads only the exceptions file, so the labelled edit is listed here and removed again after merge. Co-Authored-By: Claude Opus 5.5 --- tools/policy/foreign-exceptions.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tools/policy/foreign-exceptions.txt b/tools/policy/foreign-exceptions.txt index 1e855c5c0e..7c191f775f 100644 --- a/tools/policy/foreign-exceptions.txt +++ b/tools/policy/foreign-exceptions.txt @@ -16,6 +16,10 @@ # gen-zig fixes land as exceptions, one class per PR (#6315, #6451, #6532, #6533, #6295), label # owner-approved-foreign. The debt is #5980 (t27core self-host): these fixes move to t27core there. bootstrap/src/compiler.rs +# owner 2026-10-06, #5921 (label owner-approved-foreign; owner decision on #5921: the spec side is authoritative, +# the boundary type is f32 as specs/numeric/formats.t27 declares): ring-096 follows the spec. This drift is +# what keeps spec-guards red on master and on every bee PR. One-time: removed again right after merge. +rings/ring-096-rust/src/lib.rs # owner 2026-10-05, same approval, #6315: this test pinned the bare `side(1);` that Zig rejects; it now pins `_ = side(1);`. bootstrap/tests/bare_semicolon_zig.rs # owner 2026-10-06, label owner-approved-foreign on issue #6508 (t27core DDC): t27core's buffers shrink to From cf00317444b5a7b733ddae23523f9a0f365b80ff Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Tue, 6 Oct 2026 21:14:36 +0700 Subject: [PATCH 4/4] chore(seals): re-seal formats.t27 against master's compiler (Refs #5746) Sealed on the Railway t27c lab at b18894484 (t27c built from that tree). There check_seal_currency.py exits 0 and check_ring_spec_drift.py exits 0: ring-096-rust CONVERGED with specs/numeric/formats.t27 (6 shared, 0 differing). Co-Authored-By: Claude Opus 5.5 --- .trinity/seals/Formats.json | 14 +++++++------- .trinity/seals/numeric_Formats.json | 14 +++++++------- 2 files changed, 14 insertions(+), 14 deletions(-) diff --git a/.trinity/seals/Formats.json b/.trinity/seals/Formats.json index 2470335b31..8ee500d07b 100644 --- a/.trinity/seals/Formats.json +++ b/.trinity/seals/Formats.json @@ -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" } } \ No newline at end of file diff --git a/.trinity/seals/numeric_Formats.json b/.trinity/seals/numeric_Formats.json index 11859d5512..cc75c2ec0d 100644 --- a/.trinity/seals/numeric_Formats.json +++ b/.trinity/seals/numeric_Formats.json @@ -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" } } \ No newline at end of file