Branch for fixing the self-writing bug with overlapping non-identical addresses - #18
Open
kristinas wants to merge 8 commits into
Open
Branch for fixing the self-writing bug with overlapping non-identical addresses#18kristinas wants to merge 8 commits into
kristinas wants to merge 8 commits into
Conversation
apply, Done, getRd, getR1, getR2, and depSet were unused within ISA.hs itself, along with the now-unreferenced Data.Set and Data.Maybe imports they required. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
GitHub changed its archive tarball generation format, so the sha256 hashes pinned for the PLSec-VU/pantomime, pantomime-base, and pantomime-clash GitHub archives no longer matched what GitHub serves, breaking CI's dependency install step. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The obligations in Proof.Functional.Induction and Proof.SMT.Sanity are discharged by the Pantomime plugin while GHC compiles them, so building those modules needs an SMT solver on PATH. Z3 is the only one packaged for Ubuntu and does not finish these queries in useful time, which is why the CI job ran until it was killed rather than failing. Move the two modules under proof-smt/ and gate them on a new smt-proof flag, on by default and off in CI, and drop the z3 install from the workflow. Everything else still runs there: the QuickCheck harness goes through the same Proof.Functional.Obligation definitions the symbolic proof does, so CI still checks the obligations on sampled states, along with driver/driverRef agreement, driver-case coverage and both rv32ui suites. Locally the flag stays on and bitwuzla discharges all seven properties in about a minute; package.yaml carries the invocation. Also add IsaSpec, which runs the ISA model itself against rv32ui. The refinement proof is stated against ISA, so it cannot say whether ISA is right; the only check until now was transitive, via the core passing the same suite, which validates the specification through the implementation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
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
2 participants
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.
No description provided.