proposition: Lemma disk_correct_reboot : forall net h d ops, disk_correct (nwdoDisk net h) h (nwdoState net h) -> do_log_reboot snapshot_interval h (disk_to_channel (nwdoDisk net h)) = (d, ops) -> disk_correct (apply_ops (nwdoDisk net h) ops) h d.
proof: Proof. Proof using. intros net h d dsk H_correct H_reboot. unfold do_log_reboot, disk_to_channel, channel_to_log, from_channel in *. unfold disk_correct in *. break_exists. intuition. repeat find_rewrite. repeat rewrite IOStreamWriter.channel_wrap_unwrap in *. repeat rewrite serialize_deserialize_id_nil in H_reboot. rewrite <- (app_nil_r (IOStreamWriter.unwrap _)) in H_reboot. repeat find_rewrite. rewrite list_serialize_deserialize_id_rec in H_reboot. find_inversion. exists (IOStreamWriter.empty). exists []. exists (reboot (apply_log h x1 x0)). intuition. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)