support for 8-bit and 16-bit MMIO

[samuelgruetter]

All MMIO-related definitions are generalized to take a nat which has to be 1, 2, or 4 and indicates the number of bytes to be read or written.

@blaxill can I ask you for a review? The most interesting file for you I guess is HmacSemantics.v: It defines the state machine against which I will prove the bedrock2 driver code, and I might soon bug you to prove some Cava code against it, so it would be good to agree on whether that file makes sense 😉
Another interesting part is StateMachineSemantics.parameters.ok, which contains properties that should be true for any state machine describing a hardware module.

[blaxill]

Looking good to me. So the HMAC state machine you have doesn't include initial key set? I think thats fine, but the hardware state will not initially be initialised with the key value.

Are the bedrock changes local changes to support 8/16 bits? Do you think you will upstream them?

[samuelgruetter]

Looking good to me. So the HMAC state machine you have doesn't include initial key set? I think thats fine, but the hardware state will not initially be initialised with the key value.

So far I've only modeled the SHA mode of HMAC, which does not need any keys (this is one reason I opened #840).

Are the bedrock changes local changes to support 8/16 bits? Do you think you will upstream them?

bedrock2 and its compiler don't know anything about MMIO -- they are more general, and work for any kind of external calls, so there's nothing to upstream into bedrock2 or the compiler, unless we think that the StateMachineMMIO compiler is of general interest and should go into bedrock2's compilerExamples (as an example of an external calls compiler).
Besides that, the RiscvMachine instances in investigations/bedrock2/Riscv/ would be candidates for upstreaming into riscv-coq, but that would require updating the proof that the Kami processor correctly implements the riscv-coq model, and after spending some time trying to update that proof, I decided that this is not the best use of my time right now... On the other hand, the RiscvMachine instances in investigations/bedrock2/Riscv/ could also be just be moved as new files to riscv-coq, which I might do once the proofs work out.

[blaxill]

So far I've only modeled the SHA mode of HMAC, which does not need any keys (this is one reason I opened #840).

Ah ok, I presume the HMAC mode would be used in siliconcreator/ROM for verification but I haven't checked.