wave-17: import ring-090 Simulator -- HIR cycle-accurate sim primitives (Closes #721)#722
Merged
Merged
Conversation
…es (Closes #721) - rings/ring-090-rust/: new crate, 547 LOC, 19 tests (all pass locally on Rust 1.83.0) - Faithful Rust mirror of specs/fpga/simulator.t27 - SimState (5 variants, tags 0..=4) with tag/from_tag round-trip - SimConfig (7 fields), SimResult, ProbePoint, TraceEntry - DEFAULT_CLOCK_FREQ_HZ = 100_000_000 matches the spec's hard-coded constructor - Constructor const fns: sim_config, sim_config_with_trace, sim_ok, sim_error, probe, trace_entry - Queries: is_idle, is_done, is_error, has_errors, passed - Time conversions: sim_time_ns, sim_time_us, sim_time_ms, cycles_for_time_ns (u64 intermediate -- the spec's pure-u32 multiplication overflows at its own canonical case 100 cycles @ 100MHz, documented inline) - validate_sim_config - identity_witness(): phi^2 + 1/phi^2 == 3 to f64 1e-15 - #![no_std] (test cfg pulls std), #![forbid(unsafe_code)], #![deny(missing_docs)], zero external dependencies - Tests: 13 mirrored from spec test blocks + 4 from spec invariant blocks + identity_witness_holds + sim_state_tag_roundtrip = 19 total, all green on first run (no bug-fix cycle this time, unlike Wave 16) - rings/COMPILE_STATUS.md: promote ring-090 from claimed-only to check+test; shrink claimed-only table to ring-091..ring-099 - README.md: append Wave 17 footer - docs/NOW.md: prepend Wave 17 entry above wave-16 Constitutional: L1 (Closes #721 in commit + PR), L2 (zero gen/coq/specs edits), L3 (ASCII + English), L4 (19 #[test]), L5 (anchor present), L6 (no spec change, all constants and field shapes mirrored byte-for-byte), L7 (no new *.sh). R5-HONEST: Wave-11 narrative quoted 2143 LOC for ring-090; honest measurement is 547 LOC. Third LOC correction in the import series: ring-088 (961 -> 439), ring-089 (334 -> 635), ring-090 (2143 -> 547). Out-of-scope layers explicitly excluded (scheduler, VCD writer, event queue, clock-domain crossing, RTL). Closes #721
|
📓 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 17 -- Simulator import: ring-090 (Closes #721)
Continues the honest Wave-11 import series. Wave 15 landed ring-088 (GF16 MAC); Wave 16 landed ring-089 (TNN ISA); Wave 17 lands ring-090 -- a faithful Rust mirror of
specs/fpga/simulator.t27.What this PR does
rings/ring-090-rust/-- new crate (547 LOC, 19#[test]):SimStateenum (5 variants, tag values0..=4exactly per the spec'senum(i8) SimState)SimConfig7-field struct withDEFAULT_CLOCK_FREQ_HZ = 100_000_000matching the spec's hard-coded constructorSimResult,ProbePoint,TraceEntrywith identical field orderconst fns:sim_config,sim_config_with_trace,sim_ok,sim_error,probe,trace_entryis_idle,is_done,is_error,has_errors,passedsim_time_ns,sim_time_us,sim_time_ms,cycles_for_time_nsvalidate_sim_configidentity_witness()-- universal anchorphi^2 + 1/phi^2 == 3to f64 1e-15#,#![forbid(unsafe_code)],#![deny(missing_docs)], zero external dependenciesrings/COMPILE_STATUS.md-- promotes ring-090 fromclaimed-onlytocheck + test; claimed-only table is now ring-091..ring-099README.md-- Wave 17 footer linedocs/NOW.md-- Wave 17 entry prepended above wave-16 (NOW Sync Gate)Local verification (Rust 1.83.0, matching
Dockerfile.rust)cargo check --all-targetscargo test --libAll 13
testblocks from the spec + all 4invariantblocks +identity_witness_holds+sim_state_tag_roundtrip= 19. Unlike Wave 16, no bug-fix cycle was needed: the spec was tight enough that the first compile gave 19/19 green.Time-conversion overflow note (R5-HONEST, documented inline)
The source spec uses pure
u32forcycles * 1_000_000_000 / clock_freq_hz. At the spec's own canonical case (clock_freq_hz = 100_000_000,cycles = 100),100 * 1_000_000_000 = 1e11exceedsu32::MAX(~4.29e9) and the spec's own assertionsim_time_ns(_, 100) == 1000would fail. We faithfully implement the formula with au64intermediate and narrow back tou32; the public signature staysu32 -> u32exactly as in the spec, but the intermediate arithmetic is the minimum width needed to make the spec's own canonical test pass. Over-large results saturate atu32::MAX. The doc-comment onsim_time_nsexplains this in detail.Honest scope (R5-HONEST)
vcd_trace.t27,clock_domain.t27,formal.t27) and are out of scope for Wave 17.specs/fpga/simulator.t27byte-for-byte (L6 CEILING).Constitutional compliance
Closes #721in commit and PRgen/,coq/,trios-coq/,proofs/,bootstrap/,specs/,conformance/,architecture/#[test]blocks, all green locally on Rust 1.83.0identity_witness_holdsexercises the anchor.t27source*.shfilesThe
rings-rustmatrix (Wave-13,continue-on-error: true) will re-confirmcheck + testfor this crate on the merge commit.Anchor: phi^2 + 1/phi^2 = 3
Closes #721