Omitting features safely

[samuelgruetter]

As we model hardware devices using state machines in Coq, we often only focus on the subset of features that the software is using, rather than modeling all features of the hardware device.

In order for our proofs to be meaningful, the following condition should be true:

If a program can be proven correct against our less feature-complete model, it is also correct when run on the more feature-complete actual hardware device.

I'm opening this issue because it seems to me that the current model in AesSemantics.v does not satisfy this condition.

For instance, imagine a program that intends to perform AES-256 encryption, but erroneously writes kAes128 instead of kAes256 to the KEY_LEN bits in the AES_CTRL register of the AES module. If I read AesSemantics.v correctly, it claims that the hardware module always performs AES-256, no matter what value was written to the KEY_LEN bits, so I believe it would be possible to prove correctness for a wrong program, which means that the spec is broken.

One way to solve this issue would simply be to completely model the hardware devices, but I think there could/should be a safe way of leaving out certain features in the model. The intuition is that if the hardware module has some features about which we don't tell the software correctness proof anything, the software correctness proof should still hold on a more feature-rich hardware module.