proposition: Lemma disk_correct_invariant : forall net failed tr, @step_failure_disk_ops_star _ _ log_failure_params step_failure_disk_ops_init (failed, net) tr -> forall h, disk_correct (nwdoDisk net h) h (nwdoState net h).
proof: Proof. Proof using. intros net failed tr H_st h. remember step_failure_disk_ops_init as x. change net with (snd (failed, net)). induction H_st using refl_trans_1n_trace_n1_ind. - subst. intros. simpl in *. unfold disk_correct. simpl. exists IOStreamWriter.empty, [], (init_handlers h). intuition. - concludes. match goal with H : step_failure_disk_ops _ _ _ |- _ => invcs H end. + break_if. * rewrite e in *. intuition. match goal with | [G : disk_correct _ _ _, H : log_net_handlers _ _ _ _ _ = _ |- _] => apply (log_net_handlers_spec _ _ _ _ _ _ _ _ _ _ G H) end. reflexivity. * assumption. + break_if. * rewrite e in *. match goal with | [G : disk_correct _ _ _, H : log_input_handlers _ _ _ _ = _ |- _] => apply (log_input_handlers_spec _ _ _ _ _ _ _ _ _ G H) end. reflexivity. * assumption. + assumption. + assumption. + assumption. + break_if. * repeat find_rewrite. find_apply_lem_hyp disk_correct_reboot; assumption. * assumption. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)