search

project-oak / silveroak

Formal specification and verification of hardware, especially for security and privacy.
Apache License 2.0
123 stars 20 forks source link

Express device_implements_state_machine using only run1, without runUntilResp #965

Closed fshaked closed 2 years ago

fshaked commented 2 years ago

This PR includes @samuelgruetter's #960 (which should probably be closed without merging).

Fix the problems of runUntilResp, discussed in #960. Change the IncrWait end2end proof to use the invariant-spec. Fix TL: save the address of the outstanding request, instead of using the address from the input (which might change). Fix TL spec. Split the IncrWait device file to cava+spec, and end2end proof.

fshaked commented 2 years ago

@jadephilipoom, notice that I use the invariant-spec in the big proof in firmware/IncrementWait/CavaIncrementDevice.v, showing that it is indeed very useful (no need to reason about Cava at all). But, (in that file) I never use output_correct_pf. In fact, the postcondition of the incr device is just True, because it is not needed. This is because the device class from InternalMMIOMachine.v includes the function last_d2h, from cava-device-state to cava-output, which is then used instead of the real output. We did this because, in principal, we need to record the device output in order to know if the input of the next step will be accepted (TL protocol), and we didn't want to do that, so instead the device class shifts the responsibility to the cava device, and now the cava device state must record enough information so that the output can be computed from the state alone (i.e., the cava output must be a function of the let/delay bindings, and must not include the input bindings), which happened to be the case anyway in the incr device (and the hmac_top, but that might change soon).