diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 0b26517..b5cb69c 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,6 +18,7 @@ jobs: matrix: image: - 'coqorg/coq:dev' + - 'coqorg/coq:8.18' - 'coqorg/coq:8.17' - 'coqorg/coq:8.16' - 'coqorg/coq:8.15' diff --git a/meta.yml b/meta.yml index 783e001..5641255 100644 --- a/meta.yml +++ b/meta.yml @@ -52,6 +52,7 @@ supported_coq_versions: tested_coq_opam_versions: - version: dev +- version: '8.18' - version: '8.17' - version: '8.16' - version: '8.15' diff --git a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v index 0ec67f8..9583d96 100644 --- a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v +++ b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v @@ -264,7 +264,7 @@ Section AppendEntriesRequestReplyCorrespondence. match goal with | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ => assert (nwPackets net' = xs ++ p :: (ys ++ l)) - by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto); + by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto); clear H end. eapply @RIR_handleMessage with (net := net') (p := p); @@ -325,7 +325,7 @@ Section AppendEntriesRequestReplyCorrespondence. match goal with | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ => assert (nwPackets net' = xs ++ p :: (ys ++ l)) - by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto); + by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto); clear H end. eapply @RIR_handleMessage with (net := net') (p := p); @@ -364,7 +364,7 @@ Section AppendEntriesRequestReplyCorrespondence. match goal with | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ => assert (nwPackets net' = xs ++ p :: (ys ++ l)) - by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto); + by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto); clear H end. eapply @RIR_handleMessage with (net := net') (p := p); @@ -401,7 +401,7 @@ Section AppendEntriesRequestReplyCorrespondence. match goal with | H : nwPackets net' = (?xs ++ ?p :: ?ys) ++ ?l |- _ => assert (nwPackets net' = xs ++ p :: (ys ++ l)) - by (find_rewrite_lem app_ass; rewrite app_comm_cons; auto); + by (rewrite <- app_assoc in H; rewrite app_comm_cons; auto); clear H end. eapply @RIR_handleMessage with (net := net') (p := p); diff --git a/raft-proofs/LogsLeaderLogsProof.v b/raft-proofs/LogsLeaderLogsProof.v index 428a1a5..3c21edb 100644 --- a/raft-proofs/LogsLeaderLogsProof.v +++ b/raft-proofs/LogsLeaderLogsProof.v @@ -298,7 +298,7 @@ Section LogsLeaderLogs. simpl in *. rewrite update_elections_data_appendEntries_leaderLogs. auto. * rewrite removeAfterIndex_in_app; auto. - rewrite app_ass. repeat find_rewrite. auto. + rewrite <- app_assoc. repeat find_rewrite. auto. * repeat find_rewrite. do_in_app. intuition; eauto. + (* we share an entry with the leader, so we can use log matching to make sure our old entries match. we'll @@ -318,7 +318,7 @@ Section LogsLeaderLogs. simpl in *. rewrite update_elections_data_appendEntries_leaderLogs. auto. * rewrite removeAfterIndex_in_app; auto. - repeat find_rewrite. rewrite app_ass. + repeat find_rewrite. rewrite <- app_assoc. find_copy_eapply_lem_hyp leaderLogs_sorted_invariant; eauto. f_equal. eapply thing; eauto using lift_logs_sorted; @@ -343,7 +343,7 @@ Section LogsLeaderLogs. simpl in *. rewrite update_elections_data_appendEntries_leaderLogs. auto. * rewrite removeAfterIndex_in_app; auto. - repeat find_rewrite. rewrite app_ass. + repeat find_rewrite. rewrite <- app_assoc. f_equal. assert (x2 = []). { @@ -504,7 +504,7 @@ Section LogsLeaderLogs. end; intuition. + find_higher_order_rewrite; update_destruct; subst; rewrite_update; eauto; simpl in *; rewrite update_elections_data_client_request_leaderLogs; eauto. - + break_if; eauto using app_ass; do_bool; lia. + + break_if; eauto using app_assoc; do_bool; lia. + simpl in *. intuition; subst; eauto. - find_copy_apply_lem_hyp maxIndex_is_max; eauto using lift_logs_sorted. find_apply_hyp_hyp. break_exists_exists; intuition; diff --git a/raft-proofs/MatchIndexAllEntriesProof.v b/raft-proofs/MatchIndexAllEntriesProof.v index 5425bab..a9b96a1 100644 --- a/raft-proofs/MatchIndexAllEntriesProof.v +++ b/raft-proofs/MatchIndexAllEntriesProof.v @@ -349,7 +349,7 @@ Section MatchIndexAllEntries. Proof using. unfold handleAppendEntries, advanceCurrentTerm. intros. repeat break_match; repeat find_inversion; simpl in *; repeat do_bool; eauto; - eexists; f_equal; eauto using NPeano.Nat.le_antisymm. + eexists; f_equal; eauto using Nat.le_antisymm. Qed. Lemma not_empty_true_elim : diff --git a/raft-proofs/NextIndexSafetyProof.v b/raft-proofs/NextIndexSafetyProof.v index 55319d5..cd096d6 100644 --- a/raft-proofs/NextIndexSafetyProof.v +++ b/raft-proofs/NextIndexSafetyProof.v @@ -173,7 +173,7 @@ Section NextIndexSafety. + destruct (name_eq_dec h' (pSrc p)). * subst. rewrite get_set_same_default. unfold getNextIndex. - apply NPeano.Nat.le_le_pred. + apply Nat.le_le_pred. auto. * rewrite get_set_diff_default by auto. auto. @@ -229,7 +229,7 @@ Section NextIndexSafety. intuition; repeat find_rewrite. + auto. + unfold assoc_default. simpl. - auto using NPeano.Nat.le_le_pred. + auto using Nat.le_le_pred. - auto. Qed. diff --git a/raft-proofs/OutputCorrectProof.v b/raft-proofs/OutputCorrectProof.v index 55145ba..527c234 100644 --- a/raft-proofs/OutputCorrectProof.v +++ b/raft-proofs/OutputCorrectProof.v @@ -398,7 +398,7 @@ Section OutputCorrect. intuition. pose proof (deduplicate_log_app xs ys). break_exists. repeat find_rewrite. - rewrite app_ass in *. simpl in *. + rewrite <- app_assoc in *. simpl in *. eexists. eexists. eexists. eexists. eexists. intuition eauto. Qed. @@ -880,7 +880,7 @@ Section OutputCorrect. pose proof deduplicate_log_app l l'; break_exists; find_rewrite end. repeat eexists; intuition eauto; repeat find_rewrite; auto. - rewrite app_ass. simpl. repeat f_equal. + rewrite <- app_assoc. simpl. repeat f_equal. Defined. Next Obligation. unfold in_output_trace in *. intuition. diff --git a/raft-proofs/RaftMsgRefinementProof.v b/raft-proofs/RaftMsgRefinementProof.v index 8ea6ca2..cf1f438 100644 --- a/raft-proofs/RaftMsgRefinementProof.v +++ b/raft-proofs/RaftMsgRefinementProof.v @@ -130,7 +130,7 @@ Section RaftMsgRefinement. end. simpl. f_equal; auto. - - repeat rewrite app_ass. auto. + - repeat rewrite <- app_assoc. auto. - apply functional_extensionality. intros. repeat break_if; simpl; auto. - repeat find_rewrite; auto. @@ -218,7 +218,7 @@ Section RaftMsgRefinement. end. simpl. f_equal; auto. - - repeat rewrite app_ass. auto. + - repeat rewrite <- app_assoc. auto. - apply functional_extensionality. intros. repeat break_if; simpl; auto. - repeat find_rewrite; auto. diff --git a/raft-proofs/StateMachineCorrectProof.v b/raft-proofs/StateMachineCorrectProof.v index 0c9f2cd..6b3af4d 100644 --- a/raft-proofs/StateMachineCorrectProof.v +++ b/raft-proofs/StateMachineCorrectProof.v @@ -917,7 +917,7 @@ Section StateMachineCorrect. find_apply_hyp_hyp. break_exists. intuition. repeat find_rewrite. find_inversion. - repeat eexists; eauto using app_ass. + repeat eexists; eauto using app_assoc. Qed. Lemma getLastId_clientCache_to_ks_assoc : @@ -1025,7 +1025,7 @@ Section StateMachineCorrect. end. repeat find_rewrite. repeat eexists; eauto. - rewrite app_ass. + rewrite <- app_assoc. rewrite <- app_comm_cons. eauto. - do_bool. repeat find_inversion. copy_eapply_prop_hyp applyEntries applyEntries; @@ -1045,7 +1045,7 @@ Section StateMachineCorrect. end. repeat find_rewrite. repeat eexists; eauto. - rewrite app_ass. + rewrite <- app_assoc. rewrite <- app_comm_cons. eauto. - do_bool. subst. destruct (clientId_eq_dec (eClient x) client). @@ -1101,7 +1101,7 @@ Section StateMachineCorrect. end. repeat find_rewrite. repeat eexists; eauto. - rewrite app_ass. + rewrite <- app_assoc. rewrite <- app_comm_cons. eauto. - do_bool. subst. destruct (clientId_eq_dec (eClient x) client). @@ -1157,7 +1157,7 @@ Section StateMachineCorrect. end. repeat find_rewrite. repeat eexists; eauto. - rewrite app_ass. + rewrite <- app_assoc. rewrite <- app_comm_cons. eauto. Qed. @@ -1223,7 +1223,7 @@ Section StateMachineCorrect. intuition. pose proof (deduplicate_log_app xs ys). break_exists. repeat find_rewrite. - rewrite app_ass in *. simpl in *. + rewrite <- app_assoc in *. simpl in *. eexists. eexists. eexists. eexists. eexists. intuition eauto. Qed. @@ -1236,7 +1236,7 @@ Section StateMachineCorrect. induction l; intros; simpl in *. - find_inversion. auto. - repeat break_let. - rewrite app_ass. + rewrite <- app_assoc. eauto. Qed. @@ -1603,7 +1603,7 @@ Section StateMachineCorrect. (exists (l ++ xs), e, ys) end. unfold execute_log. - repeat rewrite app_ass. + repeat rewrite <- app_assoc. rewrite execute_log'_app. break_let. get_invariant_pre state_machine_log_invariant. diff --git a/raft-proofs/StateMachineSafetyProof.v b/raft-proofs/StateMachineSafetyProof.v index 8d02b22..c27d2ff 100644 --- a/raft-proofs/StateMachineSafetyProof.v +++ b/raft-proofs/StateMachineSafetyProof.v @@ -1944,7 +1944,7 @@ Section StateMachineSafetyProof. repeat match goal with | [ H : _ <= _, H': _ |- _ ] => rewrite H' in H end. - find_apply_lem_hyp NPeano.Nat.max_le. break_or_hyp. + find_apply_lem_hyp Nat.max_le. break_or_hyp. + (* my log is just the entries in the incoming AE. so e was in the incoming entries. but eIndex e <= old commit index. @@ -2016,7 +2016,7 @@ Section StateMachineSafetyProof. repeat match goal with | [ H : _ <= _, H': _ |- _ ] => rewrite H' in H end. - find_apply_lem_hyp NPeano.Nat.max_le. break_or_hyp. + find_apply_lem_hyp Nat.max_le. break_or_hyp. + (* eIndex e <= old commit index *) repeat find_rewrite. match goal with diff --git a/raft/CommonTheorems.v b/raft/CommonTheorems.v index f07ba52..3558ed0 100644 --- a/raft/CommonTheorems.v +++ b/raft/CommonTheorems.v @@ -281,7 +281,8 @@ Section CommonTheorems. induction xs; intros; simpl in *; intuition; break_match; try discriminate. - subst. do_bool. congruence. - do_bool. break_if; eauto. - do_bool. find_apply_hyp_hyp. intuition. + do_bool. find_apply_hyp_hyp. + lia. Qed. Lemma findAtIndex_removeAfterIndex_agree : @@ -344,8 +345,8 @@ Section CommonTheorems. Proof using. induction entries; intros. - simpl in *. intuition. - - simpl in *. break_if; intuition. - + subst. in_crush. + - simpl in *. break_if; intuition auto with datatypes. + + subst. in_crush_tac (intuition auto). + subst. do_bool. lia. + do_bool. find_apply_hyp_hyp. lia. Qed. @@ -468,10 +469,10 @@ Section CommonTheorems. intros new current prev e Hsorted Huniq Hinv. intros. red. intros. intuition. - destruct (le_lt_dec i prev). - + unfold contiguous_range_exact_lo in *. intuition. + + unfold contiguous_range_exact_lo in *. intuition auto. match goal with | H: forall _, _ < _ <= _ current -> _, H' : In _ current |- _ => - specialize (H i); apply maxIndex_is_max in H'; auto; forward H; intuition + specialize (H i); apply maxIndex_is_max in H'; auto; forward H; intuition auto with zarith end. break_exists. exists x. intuition. apply in_or_app. right. subst. @@ -481,15 +482,15 @@ Section CommonTheorems. unfold contiguous_range_exact_lo in *. intuition. match goal with | H: forall _, _ < _ <= _ new -> _ |- _ => - specialize (H i); auto; forward H; intuition - end. break_exists. exists x. intuition. + specialize (H i); auto; forward H; intuition auto with zarith + end. break_exists. exists x. intuition auto with datatypes. * subst. simpl in *. clean. exfalso. pose proof maxIndex_removeAfterIndex current (eIndex e) e. - intuition. + intuition lia. - unfold contiguous_range_exact_lo in *. do_in_app. intuition. - + firstorder auto with zarith. + + firstorder lia. + firstorder using removeAfterIndex_in. Qed. @@ -503,7 +504,7 @@ Section CommonTheorems. In y (es ++ (removeAfterIndex log i)). Proof using. intros. - exists x. intuition. + exists x. intuition auto with datatypes. Qed. Lemma findGtIndex_necessary : @@ -538,7 +539,7 @@ Section CommonTheorems. maxIndex (findGtIndex entries x) <= maxIndex entries. Proof using. intros. destruct entries; simpl; auto. - break_if; simpl; intuition. + break_if; simpl; intuition auto with arith. Qed. Lemma findAtIndex_uniq_equal : @@ -1375,8 +1376,10 @@ Section CommonTheorems. eapply applyEntries_spec_ind; eauto. Qed. + (* FIXME: move to StructTact *) Functional Scheme div2_ind := Induction for div2 Sort Prop. + (* FIXME: move to StructTact *) Theorem div2_correct' : forall n, n <= div2 n + S (div2 n). @@ -1384,6 +1387,7 @@ Section CommonTheorems. intro n. functional induction (div2 n); lia. Qed. + (* FIXME: move to StructTact *) Theorem div2_correct : forall c a b, a > div2 c -> @@ -1424,7 +1428,7 @@ Section CommonTheorems. Proof using. induction log; intros. - simpl. rewrite app_nil_r. auto. - - simpl. break_let. rewrite IHlog. rewrite app_ass. simpl. + - simpl. break_let. rewrite IHlog. rewrite <- app_assoc. simpl. rewrite IHlog with (tr := [(eInput a, o)]). auto. Qed. @@ -1497,9 +1501,9 @@ Section CommonTheorems. contiguous_range_exact_lo (a :: b :: l) i -> eIndex a = S (eIndex b) /\ eIndex a > i. Proof using. - intros. unfold contiguous_range_exact_lo in *. intuition. + intros. unfold contiguous_range_exact_lo in *. intuition auto with datatypes. assert (i < S (eIndex b) <= eIndex a). - simpl in *. intuition. specialize (H0 b). concludes. intuition. + simpl in *. intuition auto with arith. specialize (H0 b). concludes. intuition auto with arith. specialize (H1 (S (eIndex b))). concludes. break_exists. simpl In in *. intuition; subst. - auto. @@ -1517,7 +1521,7 @@ Section CommonTheorems. - apply contiguous_nil. - eapply contiguous_index_adjacent in H; eauto. unfold contiguous_range_exact_lo in *. break_and. - intuition. simpl maxIndex in *. specialize (H0 i0). + intuition auto with datatypes. simpl maxIndex in *. specialize (H0 i0). assert (i < i0 <= eIndex a0) by lia. concludes. break_exists. intuition. simpl in *. intuition; subst. + lia. @@ -1590,8 +1594,6 @@ Section CommonTheorems. simpl; intuition. Qed. - - Lemma sorted_NoDup : forall l, sorted l -> NoDup l. @@ -1601,7 +1603,8 @@ Section CommonTheorems. - constructor; intuition. match goal with | H : forall _, _ |- _ => specialize (H a) - end. intuition. + end. + intuition lia. Qed. Lemma sorted_Permutation_eq : @@ -1616,9 +1619,9 @@ Section CommonTheorems. - destruct l'. + apply Permutation_nil. apply Permutation_sym. assumption. + simpl in *. intuition. - find_copy_eapply_lem_hyp Permutation_in; intuition. + find_copy_eapply_lem_hyp Permutation_in; intuition auto with datatypes. find_copy_apply_lem_hyp Permutation_sym. - find_copy_eapply_lem_hyp Permutation_in; intuition. + find_copy_eapply_lem_hyp Permutation_in; intuition auto with datatypes. simpl in *. intuition; try (subst a; f_equal; eauto using Permutation_cons_inv). repeat find_apply_hyp_hyp. intuition. @@ -1849,7 +1852,8 @@ Section CommonTheorems. try congruence. symmetry. apply findGtIndex_nil. intros. find_apply_lem_hyp removeAfterIndex_in. - find_apply_hyp_hyp. intuition. + find_apply_hyp_hyp. + lia. Qed. Lemma findGtIndex_app_1 : @@ -1874,8 +1878,10 @@ Section CommonTheorems. break_if; do_bool; auto. - f_equal. eauto. - exfalso. - destruct l'; simpl in *; intuition. - specialize (H1 e); conclude_using intuition; intuition. + destruct l'; simpl in *; [lia|]; + specialize (H1 e). + conclude_using ltac:(intuition auto with datatypes); + lia. Qed. Lemma thing3 : @@ -1885,12 +1891,13 @@ Section CommonTheorems. In e (l ++ l') -> eIndex e <= maxIndex l' -> In e l'. - Proof using. + Proof using. induction l; intros; simpl in *; intuition. subst. destruct l'; simpl in *; intuition. - - exfalso. specialize (H0 e). intuition. - - exfalso. specialize (H3 e0). conclude_using intuition. - intuition. + - exfalso. specialize (H0 e). intuition lia. + - exfalso. specialize (H3 e0). + conclude_using ltac:(intuition auto with datatypes); + lia. Qed. Lemma findGtIndex_non_empty : @@ -1898,11 +1905,11 @@ Section CommonTheorems. i < maxIndex l -> findGtIndex l i <> []. Proof using. - intros. induction l; simpl in *; intuition. - break_if; do_bool; simpl in *; intuition. + intros. induction l; simpl in *; [lia|]. + break_if; do_bool; simpl in *; [|lia]. congruence. Qed. - + Lemma sorted_Prefix_in_eq : forall l' l, sorted l -> @@ -1938,7 +1945,7 @@ Section CommonTheorems. (removeAfterIndex l (eIndex e)) ++ l'. Proof using. induction l; intros; simpl in *; intuition; - subst; break_if; do_bool; eauto using app_ass. + subst; break_if; do_bool; eauto using app_assoc. lia. Qed. @@ -1950,7 +1957,7 @@ Section CommonTheorems. removeAfterIndex l' (eIndex e). Proof using. induction l; intros; simpl in *; intuition; - subst; break_if; do_bool; eauto using app_ass. + subst; break_if; do_bool; eauto using app_assoc. specialize (H a). intuition. lia. Qed. @@ -1969,7 +1976,7 @@ Section CommonTheorems. contiguous_range_exact_lo [x] n. Proof using. red. intuition. - - exists x. intuition. simpl in *. inv H2; [reflexivity | lia]. + - exists x. intuition auto with datatypes. simpl in *. inv H2; [reflexivity | lia]. - simpl in *. intuition. subst. lia. Qed. @@ -1981,11 +1988,11 @@ Section CommonTheorems. Proof using. intros. unfold contiguous_range_exact_lo in *. intuition. - invc H4. - + eexists; intuition. + + eexists; intuition auto with datatypes. + find_rewrite. find_apply_lem_hyp Nat.succ_inj. subst. assert (i < i0 <= maxIndex (y :: l)). simpl. lia. find_apply_hyp_hyp. break_exists. simpl in *. - intuition; subst; eexists; intuition. + intuition; subst; eexists; intuition auto. - simpl in *. intuition; subst; auto. specialize (H2 y). concludes. lia. Qed. @@ -2026,7 +2033,7 @@ Section CommonTheorems. In x l2 -> In x l. Proof using. - intros. subst. intuition. + intros. subst. intuition auto with datatypes. Qed. Lemma app_contiguous_maxIndex_le_eq : @@ -2042,7 +2049,7 @@ Section CommonTheorems. simpl in *. break_match; intuition. subst. simpl in *. unfold contiguous_range_exact_lo in *. - intuition. specialize (H0 e0). conclude_using intuition. + intuition. specialize (H0 e0). conclude_using ltac:(intuition auto with datatypes). lia. Qed. @@ -2051,8 +2058,8 @@ Section CommonTheorems. sorted (l1 ++ l2) -> sorted l1. Proof using. - intros. induction l1; simpl in *; intuition; - eapply H0; intuition. + intros. induction l1; simpl in *; intuition auto with datatypes; + eapply H0; intuition auto with datatypes. Qed. Lemma Prefix_maxIndex : @@ -2076,7 +2083,7 @@ Section CommonTheorems. match goal with | [ H : forall _, _ = _ \/ In _ _ -> _, _ : eIndex _ <= eIndex ?e |- _ ] => specialize (H e) - end; intuition. + end; intuition lia. Qed. Lemma app_maxIndex_In_l : @@ -2087,10 +2094,10 @@ Section CommonTheorems. In e l. Proof using. induction l; intros; simpl in *; intuition. - - destruct l'; simpl in *; intuition; subst; intuition. - find_apply_hyp_hyp. intuition. + - destruct l'; simpl in *; intuition auto; subst; try lia. + find_apply_hyp_hyp. lia. - do_in_app. intuition. right. eapply IHl; eauto. - intuition. + intuition auto with datatypes. Qed. Lemma contiguous_app_prefix_contiguous : @@ -2118,8 +2125,8 @@ Section CommonTheorems. eTerm e <= eTerm e'. Proof using. intros. - induction l; simpl in *; intuition; repeat subst; auto; - find_apply_hyp_hyp; intuition. + induction l; simpl in *; intuition auto; repeat subst; auto; + find_apply_hyp_hyp; lia. Qed. Lemma contiguous_app_prefix_2 : @@ -2152,11 +2159,11 @@ Section CommonTheorems. end. intuition. + subst. simpl in *. intuition. destruct l2; simpl in *. - * unfold contiguous_range_exact_lo in *. intuition. + * unfold contiguous_range_exact_lo in *. intuition auto with datatypes. * match goal with | H : _ |- eIndex _ > eIndex ?e => specialize (H e) - end. conclude_using intuition. intuition. + end. conclude_using ltac:(intuition auto with datatypes). intuition. + find_apply_lem_hyp cons_contiguous_sorted; eauto. simpl in *. intuition. Qed. @@ -2185,12 +2192,12 @@ Section CommonTheorems. induction l; intros; intuition. simpl in *. repeat break_if; simpl in *; repeat break_if; - repeat (do_bool; intuition); try lia. + repeat (do_bool; intuition auto); try lia. simpl. f_equal. rewrite IHl; eauto. apply removeAfterIndex_eq. intros. - find_apply_hyp_hyp. intuition. + find_apply_hyp_hyp. lia. Qed. Lemma findGtIndex_removeAfterIndex_i'_le_i : diff --git a/raft/Linearizability.v b/raft/Linearizability.v index e79634c..a530ee0 100644 --- a/raft/Linearizability.v +++ b/raft/Linearizability.v @@ -786,7 +786,7 @@ Section Linearizability. Proof using. intros. rewrite app_comm_cons. - replace (xs ++ I k :: ys) with ((xs ++ [I k]) ++ ys) by now rewrite app_ass. + replace (xs ++ I k :: ys) with ((xs ++ [I k]) ++ ys) by now rewrite <- app_assoc. auto using op_equiv_app_tail, op_equivalent_all_Is_I. Qed. @@ -926,7 +926,7 @@ Section Linearizability. Proof using. intros. rewrite app_comm_cons. - replace (xs ++ O k :: ys) with ((xs ++ [O k]) ++ ys) by now rewrite app_ass. + replace (xs ++ O k :: ys) with ((xs ++ [O k]) ++ ys) by now rewrite <- app_assoc. auto using op_equiv_app_tail, op_equivalent_all_Is_O. Qed. @@ -1310,17 +1310,17 @@ Section Linearizability. apply In_app_before; auto using op_eq_dec. find_rewrite_lem get_op_input_keys_app. rewrite get_op_input_keys_defn in *. intro. eapply NoDup_remove_2; eauto using in_or_app, get_op_input_keys_complete. - + repeat rewrite app_ass. + + repeat rewrite <- app_assoc. rewrite acknowledge_all_ops_func_defn. break_if. * constructor. { eapply IR_equiv_trans. - apply op_equiv_AAOF_IR_equiv. - rewrite <- app_ass. + rewrite app_assoc. eauto using op_equivalent_all_Is_O_middle, no_Ik_in_first2. - simpl. constructor. rewrite acknowledge_all_ops_func_target_ext with (t' := ir). - + rewrite app_ass. + + rewrite <- app_assoc. apply IHP; auto. * eauto using O_IRO_preserved. * eauto using IRO_O_preserved. diff --git a/raft/Raft.v b/raft/Raft.v index 86fa6dc..842b676 100644 --- a/raft/Raft.v +++ b/raft/Raft.v @@ -773,7 +773,7 @@ Section Raft. {| nwPackets := (xs ++ ys) ++ (send_packets (pDst p) l0); nwState := update name_eq_dec (nwState net) (pDst p) r - |}) by (eapply RIR_handleMessage; eauto; in_crush). + |}) by (eapply RIR_handleMessage; eauto; in_crush_tac (intuition auto)). assert (raft_intermediate_reachable {| @@ -781,7 +781,7 @@ Section Raft. (send_packets (pDst p) l1) ; nwState := (update name_eq_dec (update name_eq_dec (nwState net) (pDst p) r) (pDst p) r0) |}) by (eapply RIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop raft_net_invariant_do_generic_server. eauto. eapply_prop raft_net_invariant_do_leader. eauto. eapply raft_invariant_handle_message with (P := P); eauto using in_app_or. @@ -794,7 +794,7 @@ Section Raft. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. in_crush. + simpl. in_crush_tac (intuition auto with datatypes). + unfold RaftInputHandler in *. repeat break_let. repeat find_inversion. assert @@ -802,14 +802,14 @@ Section Raft. {| nwPackets := nwPackets net ++ send_packets h l0; nwState := update name_eq_dec (nwState net) h r |}) - by (eapply RIR_handleInput; eauto; in_crush). + by (eapply RIR_handleInput; eauto; in_crush_tac (intuition auto)). assert (raft_intermediate_reachable {| nwPackets := ((nwPackets net ++ send_packets h l0) ++ send_packets h l2) ; nwState := update name_eq_dec (update name_eq_dec (nwState net) h r) h r0 |}) by (eapply RIR_doLeader; eauto; - [simpl in *; break_if; try congruence; eauto| in_crush]). + [simpl in *; break_if; try congruence; eauto| in_crush_tac (intuition auto)]). eapply_prop raft_net_invariant_do_generic_server. eauto. eapply_prop raft_net_invariant_do_leader. eauto. eapply raft_invariant_handle_input with (P := P); eauto using in_app_or. @@ -823,7 +823,7 @@ Section Raft. break_if; subst; repeat rewrite update_same by auto; repeat rewrite update_neq by auto; auto. - simpl. unfold send_packets. intros. in_crush. + simpl. unfold send_packets. intros. in_crush_tac (intuition auto with datatypes). + match goal with | [ H : nwPackets ?net = _ |- _ {| nwPackets := ?ps ; nwState := ?st |} ] => assert (forall p, In p (nwPackets {| nwPackets := ps ; nwState := st |}) -> diff --git a/raft/RaftLinearizableProofs.v b/raft/RaftLinearizableProofs.v index fedd06b..6eca2a4 100644 --- a/raft/RaftLinearizableProofs.v +++ b/raft/RaftLinearizableProofs.v @@ -959,7 +959,7 @@ Section RaftLinearizableProofs. simpl. eapply_prop_hyp execute_log execute_log; auto. + find_rewrite. simpl in *. - rewrite <- app_ass. + rewrite app_assoc. rewrite log_to_IR_app. simpl. specialize (H x). conclude_using eauto. @@ -972,7 +972,7 @@ Section RaftLinearizableProofs. * apply exported_snoc_IU; auto. + intros. apply H. intuition. + intros. subst. eapply (H0 _ (ys ++ [x])). - rewrite app_ass. simpl. eauto. + rewrite <- app_assoc. simpl. eauto. eauto. eauto. eauto. diff --git a/raft/StateTraceInvariant.v b/raft/StateTraceInvariant.v index 3bd4ed0..31a2d13 100644 --- a/raft/StateTraceInvariant.v +++ b/raft/StateTraceInvariant.v @@ -89,10 +89,10 @@ Section ST. apply refl_trans_n1_1n_trace; auto. + eapply H_RT_input with (failed:=failed); eauto. * apply refl_trans_n1_1n_trace; auto. - * eapply T_snoc_inv. rewrite app_ass. simpl. eauto. + * eapply T_snoc_inv. rewrite <- app_assoc. simpl. eauto. * eapply IHrefl_trans_n1_trace; eauto. eapply T_snoc_inv. eapply T_snoc_inv. - rewrite app_ass. simpl. eauto. + rewrite <- app_assoc. simpl. eauto. + rewrite app_nil_r in *. eapply H_RT_drop with (failed:=failed); eauto. apply refl_trans_n1_1n_trace. eauto.