MemLog.v: prove [flush_ok]
MemLog.v: prove [flush_ok]

interestingly, not unfolding [rep] still works, because [flush] calls
only helper functions whose specs are already in terms of [rep]; this
makes [hoare] run much faster.

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