Timings for LeaderLogsLogMatchingProof.v

1. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-verdi-raft.dev/./raft-proofs/LeaderLogsLogMatchingProof.v.timing
2. /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-verdi-raft.dev/./raft-proofs/LeaderLogsLogMatchingProof.v.timing

Require Import Verdi.GhostSimulations.
Require Import VerdiRaft.Raft.
Require Import VerdiRaft.RaftRefinementInterface.

Require Import VerdiRaft.CommonTheorems.

Require Import VerdiRaft.SpecLemmas.
Require Import VerdiRaft.RefinementSpecLemmas.

Local Arguments update {_} {_} _ _ _ _ _ : simpl never.

Require Import VerdiRaft.LogMatchingInterface.
Require Import VerdiRaft.LeaderLogsTermSanityInterface.
Require Import VerdiRaft.LeaderLogsSortedInterface.
Require Import VerdiRaft.SortedInterface.
Require Import VerdiRaft.LeaderLogsSublogInterface.
Require Import VerdiRaft.LeaderLogsContiguousInterface.
Require Import VerdiRaft.TermsAndIndicesFromOneInterface.

Require Import VerdiRaft.LeaderLogsLogMatchingInterface.

Section LeaderLogsLogMatching.

  Context {orig_base_params : BaseParams}.
  Context {one_node_params : OneNodeParams orig_base_params}.
  Context {raft_params : RaftParams orig_base_params}.

  Context {rri : raft_refinement_interface}.
  Context {lmi : log_matching_interface}.
  Context {lltsi : leaderLogs_term_sanity_interface}.
  Context {llsi : leaderLogs_sorted_interface}.
  Context {si : sorted_interface}.
  Context {llsli : leaderLogs_sublog_interface}.
  Context {llci : leaderLogs_contiguous_interface}.
  Context {taifoi : terms_and_indices_from_one_interface}.

  Definition leaderLogs_entries_match_nw (net : network) : Prop :=
    forall h llt ll p t src pli plt es ci,
      In (llt, ll) (leaderLogs (fst (nwState net h))) ->
      In p (nwPackets net) ->
      pBody p = AppendEntries t src pli plt es ci ->
      (forall e1 e2,
         eIndex e1 = eIndex e2 ->
         eTerm e1 = eTerm e2 ->
         In e1 es ->
         In e2 ll ->
         (forall e3,
            eIndex e3 <= eIndex e1 ->
            In e3 es ->
            In e3 ll) /\
         (pli <> 0 ->
          exists e4,
            eIndex e4 = pli /\
            eTerm e4 = plt /\
            In e4 ll)).

  Definition leaderLogs_entries_match (net : network) : Prop :=
    leaderLogs_entries_match_host net /\
    leaderLogs_entries_match_nw net.

  Lemma leaderLogs_entries_match_init :
    refined_raft_net_invariant_init leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_init, leaderLogs_entries_match,
           leaderLogs_entries_match_host, leaderLogs_entries_match_nw.
    simpl.
    intuition.
  Qed.

  Lemma entries_match_cons_gt_maxTerm :
    forall x xs ys,
      sorted xs ->
      sorted ys ->
      eIndex x > maxIndex xs ->
      eTerm x > maxTerm ys ->
      entries_match xs ys ->
      entries_match (x :: xs) ys.
  Proof using.
 
    unfold entries_match.
    intuition; simpl in *; intuition; subst; subst;
    try match goal with
        | [ H : In _ _ |- _ ] => apply maxTerm_is_max in H; [| solve[auto]]; lia
        | [ H : In _ _ |- _ ] => apply maxIndex_is_max in H; [| solve[auto]]; lia
      end.
    -
 match goal with
        | [ H : _ |- _ ] => solve [eapply H; eauto]
      end.
    -
 right.
 match goal with
        | [ H : _ |- _ ] => solve [eapply H; eauto]
      end.
  Qed.

  Lemma entries_match_cons_sublog :
    forall x xs ys,
      sorted xs ->
      sorted ys ->
      eIndex x > maxIndex xs ->
      entries_match xs ys ->
      (forall y, In y ys -> eTerm x = eTerm y -> In y xs) ->
      entries_match (x :: xs) ys.
  Proof using.
 
    unfold entries_match.
    intuition; simpl in *; intuition; subst; subst;
    try solve [
         exfalso; try find_apply_hyp_hyp;
          match goal with
            | [ H : In _ _ |- _ ] => apply maxIndex_is_max in H; [| solve[auto]]; lia
          end].
    -
 match goal with
        | [ H : _ |- _ ] => solve [eapply H; eauto]
      end.
    -
 right.
 match goal with
        | [ H : _ |- _ ] => solve [eapply H; eauto]
      end.
  Qed.

  Lemma entries_match_nil :
    forall l,
      entries_match l [].
  Proof using.
 
    red.
    simpl.
    intuition.
  Qed.

  Lemma lifted_logs_sorted_nw :
    forall net p t n plt plti es ci,
      refined_raft_intermediate_reachable net ->
      In p (nwPackets net) ->
      pBody p = AppendEntries t n plt plti es ci ->
      sorted es.
  Proof using si rri.
 
    intros.
    pose proof (lift_prop _ logs_sorted_invariant).
    find_insterU.
 conclude_using eauto.
    unfold logs_sorted in *.
 break_and.
    unfold logs_sorted_nw in *.
    eapply H3.
    -
 unfold deghost.
 simpl.
      apply in_map_iff.
 eauto.
    -
 simpl.
 eauto.
  Qed.

  Lemma lifted_logs_sorted_host :
    forall net h ,
      refined_raft_intermediate_reachable net ->
      sorted (log (snd (nwState net h))).
  Proof using si rri.
 
    intros.
    pose proof (lift_prop _ logs_sorted_invariant).
    find_insterU.
 conclude_using eauto.
    unfold logs_sorted in *.
 break_and.
    unfold logs_sorted_host in *.
    find_insterU.
    find_rewrite_lem deghost_spec.
    eauto.
  Qed.

  Lemma leaderLogs_entries_match_nw_packet_set :
    forall net net',
      leaderLogs_entries_match_nw net ->
      (forall p, In p (nwPackets net') ->
                 is_append_entries (pBody p) ->
                 In p (nwPackets net)) ->
      (forall h, leaderLogs (fst (nwState net' h)) = leaderLogs (fst (nwState net h))) ->
      leaderLogs_entries_match_nw net'.
  Proof using.
 
    unfold leaderLogs_entries_match_nw.
    intros.
    eapply_prop_hyp In nwPackets; [|eauto 10].
    match goal with
      | [ H : _ |- _ ] =>
        solve [eapply H; eauto;
               repeat find_higher_order_rewrite;
               eauto]
    end.
  Qed.

  Lemma leaderLogs_entries_match_host_state_same :
    forall net net',
      leaderLogs_entries_match_host net ->
      (forall h, leaderLogs (fst (nwState net' h)) = leaderLogs (fst (nwState net h))) ->
      (forall h, log (snd (nwState net' h)) = log (snd (nwState net h))) ->
      leaderLogs_entries_match_host net'.
  Proof using.
 
    unfold leaderLogs_entries_match_host.
    intuition.
    repeat find_higher_order_rewrite.
 eauto.
  Qed.

  Lemma handleClientRequest_no_send :
    forall h st client id c out st' ms,
      handleClientRequest h st client id c = (out, st', ms) ->
      ms = [].
  Proof using.
 
    unfold handleClientRequest.
    intros.
    repeat break_match; repeat find_inversion; auto.
  Qed.

  Lemma leaderLogs_entries_match_client_request :
    refined_raft_net_invariant_client_request leaderLogs_entries_match.
  Proof using llsli si llsi lltsi rri.
 
    unfold refined_raft_net_invariant_client_request, leaderLogs_entries_match.
    intros.
    split.
    -
 {
 unfold leaderLogs_entries_match_host.
        simpl.
 intuition.
 subst.
 repeat find_higher_order_rewrite.
        repeat update_destruct_simplify.
        -
 find_rewrite_lem update_elections_data_client_request_leaderLogs.
          destruct (log d) using (handleClientRequest_log_ind ltac:(eauto)).
          +
 eauto.
          +
 destruct ll.
            *
 apply entries_match_nil.
            *
 {
 apply entries_match_cons_gt_maxTerm; eauto.
                -
 eauto using lifted_logs_sorted_host.
                -
 eapply leaderLogs_sorted_invariant; eauto.
                -
 lia.
                -
 find_copy_apply_lem_hyp leaderLogs_currentTerm_invariant; auto.
                  find_copy_apply_lem_hyp leaderLogs_term_sanity_invariant.
                  unfold leaderLogs_term_sanity in *.
                  eapply_prop_hyp In In; simpl; eauto.
 repeat find_rewrite.
                  simpl in *.
 lia.
              }
        -
 destruct (log d) using (handleClientRequest_log_ind ltac:(eauto)).
          +
 eauto.
          +
 apply entries_match_cons_sublog; eauto.
            *
 eauto using lifted_logs_sorted_host.
            *
 eapply leaderLogs_sorted_invariant; eauto.
            *
 lia.
            *
 intros.
              eapply leaderLogs_sublog_invariant; eauto.
              simpl in *.
 congruence.
        -
 find_rewrite_lem update_elections_data_client_request_leaderLogs.
          eauto.
        -
 eauto.
      }
    -
 eapply leaderLogs_entries_match_nw_packet_set with (net:=net); intuition.
      +
 find_apply_hyp_hyp.
 intuition eauto.
        erewrite handleClientRequest_no_send with (ms := l) in * by eauto.
        simpl in *.
 intuition.
      +
 simpl.
 subst.
 find_higher_order_rewrite.
        rewrite update_fun_comm.
 simpl.
        rewrite update_fun_comm.
 simpl.
        rewrite update_elections_data_client_request_leaderLogs.
        now rewrite update_nop_ext' by auto.
  Qed.

  Lemma leaderLogs_entries_match_timeout :
    refined_raft_net_invariant_timeout leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_timeout, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto;
      simpl; intros; subst; find_higher_order_rewrite;
      repeat update_destruct_simplify; rewrite_update; auto;
      try rewrite update_elections_data_timeout_leaderLogs;
      try erewrite handleTimeout_log_same by eauto; eauto.
    -
 eapply leaderLogs_entries_match_nw_packet_set with (net:=net); intuition.
      +
 simpl in *.
 find_apply_hyp_hyp.
  intuition.
        do_in_map.
 subst.
 simpl in *.
        exfalso.
 eapply handleTimeout_not_is_append_entries; eauto 10.
      +
 simpl.
 repeat find_higher_order_rewrite.
        rewrite update_fun_comm.
 simpl.
        rewrite update_fun_comm.
 simpl.
        rewrite update_elections_data_timeout_leaderLogs.
        rewrite update_nop_ext'; auto.
  Qed.

  Lemma lifted_log_matching :
    forall net,
      refined_raft_intermediate_reachable net ->
      log_matching (deghost net).
  Proof using lmi rri.
 
    intros.
    pose proof (lift_prop _ log_matching_invariant).
    find_insterU.
 conclude_using eauto.
    auto.
  Qed.

  Lemma lifted_log_matching_host :
    forall net,
      refined_raft_intermediate_reachable net ->
      (forall h h',
         entries_match (log (snd (nwState net h))) (log (snd (nwState net h')))) /\
      (forall h i,
         1 <= i <= maxIndex (log (snd (nwState net h))) ->
         exists e, eIndex e = i /\ In e (log (snd (nwState net h)))) /\
      (forall h e,
         In e (log (snd (nwState net h))) -> eIndex e > 0).
  Proof using lmi rri.
 
    intros.
    find_apply_lem_hyp lifted_log_matching.
    unfold log_matching, log_matching_hosts in *.
    rename net into net0.
    intuition; repeat rewrite <- deghost_spec with (net := net0).
    -
 auto.
    -
 match goal with
        | [ H : _ |- _ ] => solve [apply H; rewrite deghost_spec; auto]
      end.
    -
 match goal with
        | [ H : _ |- _ ] => solve [eapply H; rewrite deghost_spec; eauto]
      end.
  Qed.

  Lemma lifted_log_matching_nw :
    forall net,
      refined_raft_intermediate_reachable net ->
      forall p t leaderId prevLogIndex prevLogTerm entries leaderCommit,
        In p (nwPackets net) ->
        pBody p = AppendEntries t leaderId prevLogIndex prevLogTerm entries leaderCommit ->
        (forall h e1 e2,
           In e1 entries ->
           In e2 (log (snd (nwState net h))) ->
           eIndex e1 = eIndex e2 ->
           eTerm e1 = eTerm e2 ->
           (forall e3,
              eIndex e3 <= eIndex e1 ->
              In e3 entries ->
              In e3 (log (snd (nwState net h)))) /\
           (prevLogIndex <> 0 ->
            exists e4,
              eIndex e4 = prevLogIndex /\
              eTerm e4 = prevLogTerm /\
              In e4 (log (snd (nwState net h))))) /\
        (forall i,
           prevLogIndex < i <= maxIndex entries ->
           exists e,
             eIndex e = i /\
             In e entries) /\
        (forall e,
           In e entries ->
           prevLogIndex < eIndex e).
  Proof using lmi rri.
 
    intros.
    find_apply_lem_hyp lifted_log_matching.
    unfold log_matching, log_matching_nw in *.
    break_and.
    match goal with
      | [ H : forall _ : packet , _ |- _ ] =>
        do 7 insterU H;
          conclude H ltac:(unfold deghost; simpl; eapply in_map_iff; eexists; eauto);
          conclude H ltac:(simpl; eauto)
    end.
    rename net into net0.
    intuition.
    -
 rewrite <- deghost_spec with (net := net0).
      eapply H3 with (e1:=e1)(e2:=e2); eauto.
      rewrite deghost_spec.
  auto.
    -
 rewrite <- deghost_spec with (net := net0).
      eapply H3 with (e1:=e1)(e2:=e2); eauto.
      rewrite deghost_spec.
  auto.
  Qed.

  Ltac use_log_matching_nw :=
    pose proof (lifted_log_matching_nw _ ltac:(eauto));
    match goal with
      | [ H : _  |- _ ] =>
        eapply H; [|eauto];
        repeat find_rewrite; intuition
    end.

  Lemma handleAppendEntries_doesn't_send_AE :
    forall n st t i l t' l' l'' st' m,
      handleAppendEntries n st t i l t' l' l'' = (st', m) ->
      ~ is_append_entries m.
  Proof using.
 
    unfold handleAppendEntries.
    intros.
    repeat break_match; find_inversion; intro; break_exists; discriminate.
  Qed.

  Lemma leaderLogs_entries_match_append_entries :
    refined_raft_net_invariant_append_entries leaderLogs_entries_match.
  Proof using taifoi si llsi lmi rri.
 
    unfold refined_raft_net_invariant_append_entries, leaderLogs_entries_match.
    intuition.
    -
 unfold leaderLogs_entries_match_host in *.
 intros.
      {
        intros.
 simpl in *.
 repeat find_higher_order_rewrite.
        find_rewrite_lem update_fun_comm.
 simpl in *.
        find_rewrite_lem update_fun_comm.
        find_rewrite_lem update_elections_data_appendEntries_leaderLogs.
        find_erewrite_lem update_nop_ext'.
        update_destruct_simplify; rewrite_update;
        try rewrite update_elections_data_appendEntries_leaderLogs in *; eauto.
        destruct (log d) using (handleAppendEntries_log_ind ltac:(eauto)); eauto.
        +
 subst.
 eapply @entries_match_scratch with (plt := plt).
          *
 eauto using lifted_logs_sorted_nw.
          *
 apply sorted_uniqueIndices.
            eapply leaderLogs_sorted_invariant; eauto.
          *
 eapply_prop leaderLogs_entries_match_nw; eauto.
          *
 use_log_matching_nw.
          *
 use_log_matching_nw.
          *
 match goal with
              | [ H : In _ (leaderLogs _) |- _ ] =>
                eapply terms_and_indices_from_one_invariant in H; [|solve[auto]]
            end.
            unfold terms_and_indices_from_one in *.
 intros.
            find_apply_hyp_hyp.
 intuition.
        +
 eapply entries_match_append; eauto.
          *
 eauto using lifted_logs_sorted_host.
          *
 eapply leaderLogs_sorted_invariant; eauto.
          *
 eauto using lifted_logs_sorted_nw.
          *
 use_log_matching_nw.
          *
 use_log_matching_nw.
          *
 eapply findAtIndex_intro; eauto using lifted_logs_sorted_host, sorted_uniqueIndices.
      }
    -
 (* nw *)
     
 unfold leaderLogs_entries_match_nw in *.
      intros.
 simpl in *.
 repeat find_higher_order_rewrite.
      find_rewrite_lem update_fun_comm.
 simpl in *.
      find_rewrite_lem update_fun_comm.
      find_rewrite_lem update_elections_data_appendEntries_leaderLogs.
      find_erewrite_lem update_nop_ext'.
      find_apply_hyp_hyp.
 break_or_hyp.
      +
 intuition; match goal with
            | [ H : _ |- _ ] => solve [eapply (H _ _ _ p0); eauto with *]
          end.
      +
 simpl in *.
        find_copy_apply_lem_hyp handleAppendEntries_doesn't_send_AE.
        exfalso.
 eauto 10.
  Qed.

  Lemma leaderLogs_entries_match_append_entries_reply :
    refined_raft_net_invariant_append_entries_reply leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_append_entries_reply, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; simpl; intros;
      repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto.
      erewrite handleAppendEntriesReply_same_log by eauto.
 auto.
    -
 eapply leaderLogs_entries_match_nw_packet_set; eauto; simpl.
      +
 intros.
 find_apply_hyp_hyp.
 repeat find_rewrite.
 intuition; [eauto with *|].
        find_apply_lem_hyp handleAppendEntriesReply_packets.
 subst.
 simpl in *.
 intuition.
      +
 intros.
 repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto; find_rewrite; auto.
  Qed.

  Lemma handleRequestVote_packets :
    forall h st t candidate lli llt st' m,
      handleRequestVote h st t candidate lli llt = (st', m) ->
      ~ is_append_entries m.
  Proof using.
 
    intros.
 unfold handleRequestVote, advanceCurrentTerm in *.
    repeat break_match; find_inversion;
    subst; intuition; break_exists; congruence.
  Qed.

  Lemma leaderLogs_entries_match_request_vote :
    refined_raft_net_invariant_request_vote leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_request_vote, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; simpl; intros;
      repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto.
      +
 now rewrite leaderLogs_update_elections_data_requestVote.
      +
 erewrite handleRequestVote_log; eauto.
    -
 eapply leaderLogs_entries_match_nw_packet_set; eauto; simpl.
      +
 intros.
 find_apply_hyp_hyp.
 repeat find_rewrite.
 intuition; [eauto with *|].
        find_apply_lem_hyp handleRequestVote_packets.
 subst.
 simpl in *.
 intuition.
      +
 intros.
 repeat find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto.
        now rewrite leaderLogs_update_elections_data_requestVote.
  Qed.

  Lemma leaderLogs_entries_match_request_vote_reply :
    refined_raft_net_invariant_request_vote_reply leaderLogs_entries_match.
  Proof using lmi rri.
 
    unfold refined_raft_net_invariant_request_vote_reply, leaderLogs_entries_match.
    intuition.
    -
 unfold leaderLogs_entries_match_host in *.
      intros.
 simpl in *.
 subst.
      repeat find_higher_order_rewrite.
      rewrite update_fun_comm.
 simpl.
      rewrite update_fun_comm.
 simpl.
      rewrite update_nop_ext' by now rewrite handleRequestVoteReply_same_log.
      find_rewrite_lem update_fun_comm.
 simpl in *.
      update_destruct_simplify; rewrite_update; eauto.
      find_eapply_lem_hyp leaderLogs_update_elections_data_RVR; eauto.
      intuition eauto.
      subst.
      rewrite handleRequestVoteReply_same_log.
      apply lifted_log_matching_host.
 auto.
    -
 unfold leaderLogs_entries_match_nw in *.
      intros.
 simpl in *.
 subst.
      repeat find_higher_order_rewrite.
      find_rewrite_lem update_fun_comm.
 simpl in *.
      find_rewrite_lem update_fun_comm.
      update_destruct_simplify; rewrite_update.
      +
 find_eapply_lem_hyp leaderLogs_update_elections_data_RVR; eauto.
        break_or_hyp.
        *
 repeat find_reverse_rewrite.
 eauto.
        *
 break_and.
 subst.
          rewrite handleRequestVoteReply_same_log.
          find_rewrite_lem handleRequestVoteReply_same_log.
          pose proof (lifted_log_matching_nw _ ltac:(eauto)).
          repeat find_reverse_rewrite.
          match goal with
            | [ H : _, pkt : packet  |- _ ] =>
              solve [eapply H with (p := pkt); eauto]
          end.
      +
 repeat find_reverse_rewrite.
 eauto.
  Qed.

  Lemma doLeader_messages :
    forall st h os st' ms,
      doLeader st h = (os, st', ms) ->
      ms = [] \/
      ms = map (replicaMessage st' h)
               (filter (fun h' : name => if name_eq_dec h h' then false else true)
                       nodes).
  Proof using.
 
    unfold doLeader.
    intros.
    repeat break_match; repeat find_inversion; auto.
  Qed.

  Lemma leaderLogs_entries_match_do_leader :
    refined_raft_net_invariant_do_leader leaderLogs_entries_match.
  Proof using llci si llsi rri.
 
    unfold refined_raft_net_invariant_do_leader, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; simpl; intros;
      find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto.
      +
 find_rewrite.
 auto.
      +
 erewrite doLeader_same_log by eauto.
 find_rewrite.
 auto.
    -
 unfold leaderLogs_entries_match_nw in *.
 intros.
 simpl in *.
      repeat find_higher_order_rewrite.
      find_rewrite_lem update_fun_comm.
 simpl in *.
      match goal with
        | [ H : _ |- _ ] =>
          rewrite update_nop_ext' in H by (find_rewrite; auto)
      end.
      find_apply_hyp_hyp.
 break_or_hyp.
      +
 find_reverse_rewrite.
 eauto.
      +
 do_in_map.
 subst.
 simpl in *.
        find_copy_apply_lem_hyp doLeader_messages.
        break_or_hyp.
        *
 simpl in *.
 intuition.
        *
 do_in_map.
 find_apply_lem_hyp filter_In.
          break_and.
 break_if; try discriminate.
          unfold replicaMessage in *.
 subst.
 simpl in *.
 find_inversion.
          {
 intuition.
            -
 repeat find_erewrite_lem doLeader_same_log.
              eapply_prop leaderLogs_entries_match_host; eauto.
              +
 match goal with
                  | [ H : _ |- _ ] => rewrite H
                end.
 simpl.
                eauto using findGtIndex_in.
              +
 auto with *.
              +
 find_rewrite.
 simpl.
 eauto using findGtIndex_in.
            -
 find_copy_apply_lem_hyp leaderLogs_contiguous_invariant; auto.
              unfold contiguous_range_exact_lo in *.
 break_and.
              match goal with
                | [ H : forall _, _ < _ <= _ -> _ |- context [eIndex _ = ?x]] =>
                  remember (x) as index;
                  specialize (H index); forward H
              end.
              +
 intuition; auto using Nat.neq_0_lt_0.
                find_apply_lem_hyp findGtIndex_necessary.
 break_and.
                eapply Nat.le_trans.
                *
 apply Nat.lt_le_incl.
 eauto.
                *
 repeat find_rewrite.
 eapply maxIndex_is_max; auto.
                  eapply leaderLogs_sorted_invariant; eauto.
              +
 concludes.
 break_exists_exists.
 intuition.
                match goal with
                  | [ H : context [leaderLogs_entries_match_host],
                     H' : context [leaderLogs] |- _ ] =>
                    eapply H with (h := src)(e := e1)(e' := e2)(e'' := x) in H'; auto
                end.
                *
 pose proof lifted_logs_sorted_host net src ltac:(auto).
                  repeat find_rewrite.
 simpl in *.
                  repeat find_erewrite_lem doLeader_same_log.
                  erewrite doLeader_same_log by eauto.
                  erewrite findAtIndex_intro; eauto using sorted_uniqueIndices.
                *
 find_apply_lem_hyp findGtIndex_necessary.
 break_and.
                  repeat find_erewrite_lem doLeader_same_log.
                  repeat find_rewrite.
 simpl in *.
                  auto.
                *
 find_apply_lem_hyp findGtIndex_necessary.
 break_and.
                  lia.
          }
  Qed.

  Lemma doGenericServer_packets :
    forall h st os st' ps,
      doGenericServer h st = (os, st', ps) ->
      ps = [].
  Proof using.
 
    intros.
 unfold doGenericServer in *.
    repeat break_match; find_inversion; subst; auto.
  Qed.

  Lemma leaderLogs_entries_match_do_generic_server :
    refined_raft_net_invariant_do_generic_server leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_do_generic_server, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; simpl; intros;
      find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto.
      +
 find_rewrite.
 auto.
      +
 erewrite doGenericServer_log by eauto.
 find_rewrite.
 auto.
    -
 eapply leaderLogs_entries_match_nw_packet_set; eauto; simpl.
      +
 intros.
 find_apply_hyp_hyp.
 intuition.
        find_apply_lem_hyp doGenericServer_packets.
 subst.
 simpl in *.
 intuition.
      +
 intros.
 find_higher_order_rewrite; update_destruct_simplify; rewrite_update; auto; find_rewrite; auto.
  Qed.

  Lemma leaderLogs_entries_match_state_same_packet_subset :
    refined_raft_net_invariant_state_same_packet_subset leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_state_same_packet_subset, leaderLogs_entries_match.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; intros; find_higher_order_rewrite; auto.
    -
 eapply leaderLogs_entries_match_nw_packet_set; eauto; intros; find_higher_order_rewrite; auto.
  Qed.

  Lemma leaderLogs_entries_match_reboot :
    refined_raft_net_invariant_reboot leaderLogs_entries_match.
  Proof using.
 
    unfold refined_raft_net_invariant_reboot, leaderLogs_entries_match, reboot.
    intuition.
    -
 eapply leaderLogs_entries_match_host_state_same; eauto; intros; find_higher_order_rewrite;
      update_destruct_simplify; rewrite_update; auto; find_rewrite; auto.
    -
 eapply leaderLogs_entries_match_nw_packet_set; eauto; try find_rewrite; intuition.
      find_higher_order_rewrite; update_destruct_simplify; rewrite_update; try find_rewrite; auto.
  Qed.

  Lemma leaderLogs_entries_match_invariant :
    forall net,
      refined_raft_intermediate_reachable net ->
      leaderLogs_entries_match net.
  Proof using taifoi llci llsli si llsi lltsi lmi rri.
 
    intros.
    apply refined_raft_net_invariant; auto.
    -
 apply leaderLogs_entries_match_init.
    -
 apply leaderLogs_entries_match_client_request.
    -
 apply leaderLogs_entries_match_timeout.
    -
 apply leaderLogs_entries_match_append_entries.
    -
 apply leaderLogs_entries_match_append_entries_reply.
    -
 apply leaderLogs_entries_match_request_vote.
    -
 apply leaderLogs_entries_match_request_vote_reply.
    -
 apply leaderLogs_entries_match_do_leader.
    -
 apply leaderLogs_entries_match_do_generic_server.
    -
 apply leaderLogs_entries_match_state_same_packet_subset.
    -
 apply leaderLogs_entries_match_reboot.
  Qed.

  Instance lllmi : leaderLogs_entries_match_interface : Prop.
  Proof.
    split.
    apply leaderLogs_entries_match_invariant.
  Qed.
End LeaderLogsLogMatching.