tweak definition of [exec] and [exec_recover]
tweak definition of [exec] and [exec_recover]

[exec] no longer discards pending writes on crash.
this should lead to simpler exec hoare specs.

[exec_recover] now discards pending writes using [possible_crash],
so the idempotence proofs might have to reason about [crash_xform].

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