proposition: Theorem log_step_failure_step : forall net net' failed failed' tr tr', @step_failure_disk_ops_star _ _ log_failure_params step_failure_disk_ops_init (failed, net) tr -> @step_failure_disk_ops _ _ log_failure_params (failed, net) (failed', net') tr' -> step_failure (failed, revertLogNetwork net) (failed', revertLogNetwork net') tr'.
proof: Proof. Proof using. intros. assert (revert_packets : forall net, nwPackets (revertLogNetwork net) = map revertPacket (nwdoPackets net)) by reflexivity. assert (revert_send : forall l h, map revertPacket (do_send_packets h l) = send_packets h l). { induction l. * reflexivity. * intros. simpl. now rewrite IHl. } assert (apply_if : forall h d, (fun h0 : name => log_data (if name_eq_dec h0 h then d else nwdoState net h0)) = (fun h0 : name => if name_eq_dec h0 h then log_data d else log_data (nwdoState net h0))). { intros. extensionality h0. break_if; reflexivity. } invcs H0. - unfold revertLogNetwork. simpl. find_rewrite. repeat rewrite map_app. simpl. rewrite revert_send. assert (revert_packet : do_pDst p = pDst (revertPacket p)) by reflexivity. rewrite revert_packet in *. apply @StepFailure_deliver with (xs := map revertPacket xs) (ys := map revertPacket ys) (d := log_data d) (l := l). + reflexivity. + assumption. + simpl. unfold log_net_handlers, log_handler_result in *. break_let. break_let. break_if; find_inversion; rewrite revert_packet in *; assumption. + simpl. rewrite apply_if. reflexivity. - unfold revertLogNetwork. simpl. repeat rewrite map_app. rewrite revert_send. apply @StepFailure_input with (d := log_data d) (l := l). + assumption. + unfold log_input_handlers, log_handler_result in *. do 2 break_let. break_if; find_inversion; assumption. + rewrite apply_if. reflexivity. - unfold revertLogNetwork. simpl. find_rewrite. rewrite map_app. simpl. apply @StepFailure_drop with (xs := map revertPacket xs) (p := revertPacket p) (ys := map revertPacket ys). + reflexivity. + rewrite map_app. reflexivity. - unfold revertLogNetwork. simpl. find_rewrite. rewrite map_app. simpl. apply (@StepFailure_dup _ _ _ _ _ _ (revertPacket p) (map revertPacket xs) (map revertPacket ys)). + reflexivity. + reflexivity. - constructor. - apply @StepFailure_reboot with (h := h). + assumption. + reflexivity. + unfold revertLogNetwork. simpl. apply reboot_invariant with (h := h) (d := d) (dsk := ops) in H. * rewrite <- H. rewrite apply_if. reflexivity. * assumption. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)