Add BoolSpec instances for verify

mit-plv / riscv-coq

RISC-V Specification in Coq

BSD 3-Clause "New" or "Revised" License

109 stars 17 forks source link

Add BoolSpec instances for verify #31

Open JasonGross opened 2 years ago

JasonGross commented 2 years ago

This unfortunately makes src/riscv/Spec/Decode.v a bit slower; I can speed it up if desired by setting boolean equality only for InstructionSet. This is to help with https://github.com/mit-plv/bedrock2/issues/285 ... which I just saw that 5a084e4bb05db8e1fb6a51b2c10bd38c0a652e82 does. So I guess feel free to ignore this if you don't like it. (Good thing I didn't spend too long working on this.)

samuelgruetter commented 2 years ago

Ah oops, sorry for not announcing that I was already working on it... Note that if we still want to use this, the changes to Decode.v would need to go to hs-to-coq's preamble, because this file is autogenerated.

JasonGross commented 2 years ago

No worries