checkpoint an attempt at hoare quadruples to represent crashes
checkpoint an attempt at hoare quadruples to represent crashes

new syntax:

  {{ pre }} p {{ postok }} {{ postcrash }}

means that, starting from a precondition pre, running p will either
ensure postok (if there were no crashes), or ensure postcrash (if
there was a crash and recovery ran).

not sure if recover_corr is defined correctly yet, and haven't proved
recover_corr_sound yet either.

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl