proposition: Lemma inputs_eq_outputs_plus_inc_plus_ack : forall net tr, step_async_star (params := Counter_MultiParams) step_async_init net tr -> trace_inputs tr = trace_outputs tr + inc_in_flight_to_backup (nwPackets net) + ack_in_flight_to_primary (nwPackets net).
proof: Proof. intros. remember step_async_init as y in *. revert Heqy. induction H using refl_trans_1n_trace_n1_ind; intros; subst. - reflexivity. - concludes. match goal with | [ H : step_async _ _ _ |- _ ] => invc H end; simpl. + find_apply_lem_hyp net_handlers_NetHandler. repeat find_rewrite. rewrite trace_inputs_app. rewrite trace_outputs_app. rewrite cons_is_app with (x := p) in *. repeat rewrite inc_in_flight_to_backup_app in *. repeat rewrite ack_in_flight_to_primary_app in *. find_apply_lem_hyp NetHandler_trace_preserved. destruct (pDst p) eqn:?. * erewrite inc_in_flight_to_backup_cons_primary_dst in * by eauto. rewrite trace_inputs_output in *. simpl in *. lia. * rewrite ack_in_flight_to_primary_backup in * by auto. rewrite trace_outputs_backup in *. unfold send_packets in *. simpl in *. rewrite <- plus_n_O in *. lia. + find_apply_lem_hyp input_handlers_InputHandlers. find_apply_lem_hyp InputHandler_trace_preserved. rewrite cons_is_app. repeat rewrite trace_inputs_app. repeat rewrite trace_outputs_app. repeat rewrite inc_in_flight_to_backup_app in *. repeat rewrite ack_in_flight_to_primary_app in *. rewrite trace_outputs_input. rewrite trace_inputs_output. unfold send_packets in *. simpl in *. lia. Qed.
imports: Verdi(Verdi HandlerMonad)