opencompl
feature: RiscV dialect base and semantics,
This PR contains a Risc-V dialect for a 64-bit address space. We support the base ISA, M and B extensions as well as part of the different Z extensions. The semantics faithfully implement the semantics specified in Sail. We have partially removed the toInt's and toNat's in the semantics definition, part of this transformation is still wip and marked as such.
![github-actions[bot] avatar](https://avatars.githubusercontent.com/in/15368?v=4 "Published by a pub.dev verified publisher"){kind=small}
Jesus, that's a chonky PR!
I will hit "approve", but I would like us to think about the following questions:
- How do we know that this faithfully implements Sail? Is it possible, in a future PR, to directly reuse Sail's definitions? (adding sail as a dependency, of course).
- Is it possible to auto-generate this ourselves? I guess this is the same as the above question: Can we somehow directly hook into sail, instead of having to trust this implementation?
Regarding the sail part, I have proofs for every translation step in Lean, hence an end-to-end proof that the provided semantics are correct even when removing toInt and toNats. In my own project I had sail as a dependency. I didn't included the file containing the proof because I assumed that would be too much. Autogenerating the definitions from Sail would be nice but the original sail def contain toInts and toNats which is impractical if we want to use bv_decide to prove the rewrites correct.
- I didn't include the pretty printer for the moment, there is one but I will wait until this is approved.
Right. I feel it would be worth it to add Sail as a dependency, and the proofs of equivalence as a follow up PR @salinhkuhn. Let's see what @alexkeizer and @tobiasgrosser think.