proposition: Lemma log_input_handlers_spec : forall h m st ops out st' l dsk dsk', disk_correct dsk h st -> log_input_handlers snapshot_interval h m st = (ops, out, st', l) -> apply_ops dsk ops = dsk' -> disk_correct dsk' h st'.
proof: Proof. Proof using. intros. unfold disk_correct in *. unfold log_input_handlers, log_handler_result in *; break_if; do 2 break_let. - find_inversion. simpl. exists IOStreamWriter.empty, [], d. intuition. - find_inversion. simpl. break_exists. intuition. match goal with | _ : dsk Log = Some ?s, _ : apply_log _ ?d ?entries = _ |- _ => exists (s +$+ (serialize (inl m : entry))), (entries ++ [inl m]), d end. intuition. + match goal with | H : context [log_num_entries] |- _ => rewrite H end. rewrite app_length. simpl. rewrite Nat.add_1_r. reflexivity. + break_match. * find_inversion. reflexivity. * congruence. + cheerios_crush. rewrite serialize_snoc. match goal with | H : IOStreamWriter.unwrap _ = IOStreamWriter.unwrap _ |- _ => rewrite H end. reflexivity. + match goal with | H : context [log_num_entries] |- _ => rewrite H end. rewrite app_length. simpl. rewrite Nat.add_1_r. reflexivity. + rewrite apply_log_app. match goal with | H : context [apply_log] |- _ => rewrite H end. simpl. match goal with | H : context [input_handlers] |- _ => rewrite H end. reflexivity. Qed.
imports: Verdi(Verdi) Cheerios(Cheerios) Verdi(Log) Coq(FunctionalExtensionality)