proposition: Lemma reboot_invariant : forall net failed tr, @step_failure_disk_ops_star _ _ log_failure_params step_failure_disk_ops_init (failed, net) tr -> forall h d dsk, do_reboot h (disk_to_channel (nwdoDisk net h)) = (d, dsk) -> log_data d = reboot (log_data (nwdoState net h)).
proof: Proof. Proof using. intros net failed tr H_st h d dsk H_reboot. apply disk_correct_invariant with (h := h) in H_st. unfold disk_correct in *. break_exists. intuition. simpl in *. unfold do_log_reboot, channel_to_log, disk_to_channel in *. find_inversion. simpl. repeat match goal with | H : nwdoDisk net h _ = Some _ |- _ => rewrite H end. unfold from_channel. repeat rewrite IOStreamWriter.channel_wrap_unwrap in *. rewrite serialize_deserialize_id_nil. rewrite <- (app_nil_r (IOStreamWriter.unwrap _)). match goal with | H : IOStreamWriter.unwrap _ = IOStreamWriter.unwrap _ |- _ => rewrite H end. rewrite nat_serialize_deserialize_id. rewrite <- (app_nil_r (IOStreamWriter.unwrap _)). rewrite list_serialize_deserialize_id_rec. find_rewrite. reflexivity. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)