feat(phd/igla): L-S40 MeshDeterminismCorrect — 2×2 GF16 mesh determinism under RR NoC#798
Open
gHashTag wants to merge 1 commit into
Open
feat(phd/igla): L-S40 MeshDeterminismCorrect — 2×2 GF16 mesh determinism under RR NoC#798gHashTag wants to merge 1 commit into
gHashTag wants to merge 1 commit into
Conversation
…ism under RR NoC Closes #797 Formal proof that the 2×2 GF16 mesh is deterministic under round-robin NoC arbitration. Given the same initial mesh state, any two runs with cycle offsets congruent mod 4 produce identical outputs for all step counts. Key results - Lemma rr_period_4: rr_step (s+4) ms = rr_step s ms - Theorem mesh_determinism: forall init s1 s2 n, s1 mod 4 = s2 mod 4 -> rr_run init s1 n = rr_run init s2 n - Zero Admitted; all proofs end Qed - coqc 8.20.1 exit 0 Anchor: φ²+φ⁻²=3 | RR period 4 | DOI 10.5281/zenodo.19227877 Foundation for Wave-12 cross-die ledger receipt v2 Also: create docs/phd/artifacts/coq_citation_map.json mapping MeshDeterminismCorrect.mesh_determinism → gf16_mesh_2x2_top.v arbiter Apache-2.0 | Author: Dmitrii Vasilev <admin@t27.ai>
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.
Closes #797
Summary
Formal Coq proof (L-S40) that the 2×2 GF16 mesh is deterministic under round-robin NoC arbitration.
Given the same initial mesh state and the same input flit sequence, any two runs with global cycle offsets that are congruent modulo 4 produce identical outputs for all step counts. This establishes phase-offset independence of the arbitration result.
Anchor
Key results (zero
Admitted)rr_period_4forall s ms, rr_step (s+4) ms = rr_step s msmesh_determinismforall init s1 s2 n, s1 mod 4 = s2 mod 4 -> rr_run init s1 n = rr_run init s2 nFiles changed
docs/phd/theorems/igla/MeshDeterminismCorrect.v— Coq source (193 loc, 0 Admitted, all Qed)docs/phd/artifacts/coq_citation_map.json— new file mappingMeshDeterminismCorrect.mesh_determinism→gf16_mesh_2x2_top.varbiterVerification
Foundation
This proof is the foundation for Wave-12 cross-die ledger receipt v2.
Apache-2.0 | Author: Dmitrii Vasilev admin@t27.ai