When is it safe to omit features in a state machine modeling a hardware device?

[samuelgruetter]

Here's an attempt (not successful yet) to formalize what I meant in #840 by "omitting features safely": I define a predicate state_machine_extends SM1 SM2, intended to capture the fact that state machine SM1 is an extended (ie, having more features) version of state machine SM2, and that any program proven correct against SM2 would also run correctly on a device implementing SM1.

If we do end-to-end proofs, we will not need this: We can just prove the software and hardware against the same state machine and have the state machine, which is an intermediate specification, cancel out.

The reason I still started this experiment is for the case where we prove a bedrock2 program against some state machine, but omit some features in this state machine, and we need to argue why it is safe to omit these features. In any case, this argument will not be carried out in Coq (because if we had actually modeled all features, we could just prove the bedrock2 program against the complete state machine), but I still wanted to try to formally state the notion of "a state machine extends another state machine", and to see if it preserves bedrock2 program logic proofs, so that part of the non-Coq argument could be supported by a Coq proof.

However, I got stuck on details for which I don't quite know whether they are technical details or more fundamental, and since this is not needed for end-to-end proofs, and also not needed if we model hardware devices fully, I decided to stop working on it and just post it here FYI.

[samuelgruetter]

Closing this as it's not needed in the end-to-end proofs that we're currently focusing on, and it's already tracked as a TODO item in #840.