proposition: Lemma step_failure_deserialized_simulation : forall net net' failed failed' tr, @step_failure _ _ serialized_failure_params (failed, net) (failed', net') tr -> @step_failure _ _ orig_failure_params (failed, deserialize_net net) (failed', deserialize_net net') tr \/ (deserialize_net net' = deserialize_net net /\ failed = failed').
proof: Proof. Proof using. move => net net' failed failed' tr H_st. rewrite -2!pt_map_net_deserialize_net. have H_eq_n: failed = map (@tot_map_name _ _ _ _ multi_params_orig_name_tot_map) failed by rewrite /tot_map_name /= map_id. rewrite {1}H_eq_n. have H_eq_n': failed' = map (@tot_map_name _ _ _ _ multi_params_orig_name_tot_map) failed' by rewrite /tot_map_name /= map_id. rewrite {1}H_eq_n'. have ->: tr = filterMap (@pt_map_trace_occ _ _ _ _ _ orig_multi_params_name_tot_map) tr. rewrite /pt_map_trace_occ /= /id. clear. elim: tr => //=. case => a; case => b l IH; first by rewrite -IH. rewrite -IH. set fm := filterMap _ _. have H_b: b = fm. rewrite /fm {fm}. elim: b => //=. move => o l' IH'. by rewrite -IH'. by rewrite H_b. apply step_failure_pt_mapped_simulation_1 in H_st. case: H_st => H_st; first by left. right. by break_and. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)