wave-15: canonical GF16 import -- ring-088 (real, tested, cross-kernel identity) (Closes #717)#718
Merged
Merged
Conversation
…ty check) (Closes #717) NEW (additive, rings-only): - rings/ring-088-rust/Cargo.toml standalone, no workspace - rings/ring-088-rust/src/lib.rs (439) GF16 codec + mac_dot + identity_witness - rings/ring-088-rust/README.md usage + test table GF16 codec faithful to specs/numeric/gf16.t27: [S(1) E(6) M(9)], BIAS=31, special exp=0x3F (Inf/NaN), separate +0/-0, canonical NaN 0xFE01. mac_dot(&[Gf16], &[Gf16]) -> Option<f32>: streaming, alloc-free, None on length mismatch. identity_witness(): true iff phi^2 + 1/phi^2 == 3 (f64, 1e-15). no_std (test cfg pulls std), forbid(unsafe_code), deny(missing_docs), zero external dependencies. Inline ldexp/frexp/floor helpers. Tests (13, all pass locally on Rust 1.83.0): 8 mandatory from specs/02-gf16-format.tri: gf16_roundtrip_phi, gf16_from_zero_{pos,neg}, gf16_phi_identity, gf16_quantization_roundtrip_pi, gf16_better_phi_distance_than_f16, gf16_inf_roundtrip, gf16_nan_propagates 4 MAC: mac_dot_{empty,length_mismatch,simple,phi_identity} 1 universal: identity_witness_holds Critical: mac_dot_phi_identity -- FIRST cross-kernel exercise of the phi^2 + 1/phi^2 = 3 anchor (GF16 encode -> MAC -> f32 decode). R5-HONEST audit: Wave-11 narrative claimed 12 crates ring-088..099 at ~9930 LOC authored 'in another sandbox'. None on disk. Wave 15 imports ring-088 for real; remaining 11 reclassified from 'off-disk' to 'claimed-only' in rings/COMPILE_STATUS.md with explicit warning that LOC numbers are quotes from past narrative, not measurements. L1 TRACEABILITY/L2 GENERATION/L3 PURITY/L4 TESTABILITY/L5 IDENTITY/ L6 CEILING/L7 UNITY: all green. Anchor: phi^2 + 1/phi^2 = 3 Closes #717
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wave 15 — Canonical GF16 Import (ring-088)
Closes #717
What
The first honestly-authored Wave-11 crate.
rings/ring-088-rust/lands with a real GF16 codec, a real allocation-freemac_dotkernel, and the project's first cross-kernel identity test.rings/ring-088-rust/Cargo.tomlexclude = [..., "rings"])rings/ring-088-rust/src/lib.rsmac_dot+identity_witnessrings/ring-088-rust/README.mdR5-HONEST audit (the reason this wave exists)
Wave 11's narrative claimed 12 Rust crates
ring-088..ring-099totalling ~9 930 LOC had been authored "in another sandbox". A full search of this repository, the past-session context, and every reachable workspace location found zero source files for any of those 12 rings. Wave-13COMPILE_STATUS.mdlabelled themoff-disk, but that was a placeholder, not a deliverable.Wave 15 starts the real import with the most foundational ring (GF16) and reclassifies the remaining 11 to
claimed-onlyuntil each receives the same real-source treatment.What ring-088 actually does
f32 ↔ Gf16faithful tospecs/numeric/gf16.t27— bit layout[S(1) E(6) M(9)],BIAS = 31, special exp0x3F, separate+0/-0, canonical NaN0xFE01. No new spec; all constants mirror existing spec byte-for-byte (L6 CEILING).mac_dot(&[Gf16], &[Gf16]) -> Option<f32>— streaming, allocation-free dot product.Noneon length mismatch. Saturation on overflow. Subnormals flush to zero.identity_witness()—trueiffphi^2 + 1/phi^2 == 3to f64 1e-15.#,#![forbid(unsafe_code)],#![deny(missing_docs)], zero external dependencies. Inlineldexp/frexp/floorhelpers.Local verification (Rust 1.83.0)
The critical test
mac_dot_phi_identityis the first time in the project that the anchorφ² + 1/φ² = 3is exercised through actual numeric kernels:Up until now
identity_witnesswas a free-standing f64 assertion. This test wires the anchor into a real numeric pipeline.COMPILE_STATUS promotions / reclassifications
ring-088-rust—off-disk→check+testring-089..ring-099(11 crates) —off-disk→claimed-only(legend gains a new row spelling out exactly what that means; LOC column relabelled "LOC (claimed)" with a preamble warning)Constitutional compliance
Closes #717in title, body, commitgen/,coq/,trios-coq/,proofs/,bootstrap/,specs/,conformance/,architecture/, rootCargo.toml#[test]s (8 mandatory-from-spec + 4 MAC + 1 universal)*.sh; new files are.toml,.rs,.mdAnchor: φ² + 1/φ² = 3