Express device_implements_state_machine using only run1, without runUntilResp

[fshaked]

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]

@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).

[samuelgruetter]

I wonder how common it is that postcondition contains let repr' := update input repr in ... and whether that would justify making it an argument of postcondition.