search

project-oak / silveroak

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

express `device_implements_state_machine` using only `run1`, without `runUntilResp` (on top of #959) #960

Open samuelgruetter opened 2 years ago

samuelgruetter commented 2 years ago

I'm trying to work top-down from device_implements_state_machine towards Cava Hmac, and the first too-high-level item that I encountered was that the read/write steps in device_implements_state_machine talk about several device steps at once (because they're using runUntilResp). I wrote an alternative device_implements_state_machine that only uses run1, but not runUntilResp. That should bring the interface closer to the structure of Cava proofs, hopefully. Unfortunately, the proofs for CavaIncrementDevice.v break badly, and I haven't fixed them yet, so this is still a draft, but I'm posting it here because I'd be interested to know what @fshaked thinks about the changes I made in MMIOToCava.v, and whether they could simplify what you're working on?

fshaked commented 2 years ago

I haven't really looked at this PR yet but I noticed yesterday that runUntilResp is behaving wrong with respect to the TL protocol. The function should only send the h2d packet with a_valid=1 until it gets a d2h packet with a_ready=1, and then it should keep sending h2d packets with a_valid=0 and d_ready=1, until it gets back a d2h packet with d_valid=1. Also note that the tlul_adapter_reg implementation sends the a_ready=1 signal in the d2h packet prior to the h2d with a_valid=1. So runUntilResp must start by sending a nop_h2d (i.e. a_valid=0), check the a_ready in the returned packet, to determine if the next h2d packet will be received, and only then send the valid h2d packet.

Also, I'm redoing CavaIncrementDevice.v anyway so don't worry about breaking it.

samuelgruetter commented 2 years ago

I added one more file, Bedrock2StateMachineToCavaHmac.v, where I wrote some invariant for hmac_top, but then, when I started to think about what update_repr for hmac_top should look like, taking into account response delays that I would not want to specify deterministically, I noticed that I first should understand TLUL better, so I sketched a tlul_step that's supposed to specify the TLUL interaction at a high level. I'm not sure if that definition tlul_step will show up as-is anywhere in the final specs and proofs, but I'd still be interested in @fshaked's feedback on whether that looks about right?