diff --git a/extraction/vard-debug/coq/ExtractVarDRaftDebug.v b/extraction/vard-debug/coq/ExtractVarDRaftDebug.v index ca8bd68c..35e33ab6 100644 --- a/extraction/vard-debug/coq/ExtractVarDRaftDebug.v +++ b/extraction/vard-debug/coq/ExtractVarDRaftDebug.v @@ -1,16 +1,8 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import VerdiRaft.VarDRaft. - -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlNatInt. -Require Import ExtrOcamlString. - -Require Import Verdi.ExtrOcamlBasicExt. -Require Import Verdi.ExtrOcamlNatIntExt. - -Require Import Verdi.ExtrOcamlBool. -Require Import Verdi.ExtrOcamlList. -Require Import Verdi.ExtrOcamlFinInt. - -Extraction "extraction/vard-debug/ml/VarDRaftDebug.ml" seq vard_raft_base_params vard_raft_multi_params vard_raft_failure_params. +From Verdi Require Import Verdi VarD. +From VerdiRaft Require Import VarDRaft. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString. +From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt. +From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt. + +Extraction "extraction/vard-debug/ml/VarDRaftDebug.ml" seq vard_raft_base_params + vard_raft_multi_params vard_raft_failure_params. diff --git a/extraction/vard-log/coq/ExtractVarDRaftLog.v b/extraction/vard-log/coq/ExtractVarDRaftLog.v index 60d5c720..605bbc0e 100644 --- a/extraction/vard-log/coq/ExtractVarDRaftLog.v +++ b/extraction/vard-log/coq/ExtractVarDRaftLog.v @@ -1,24 +1,11 @@ -Require Import Verdi.Verdi. -Require Import Cheerios.Cheerios. - -Require Import Verdi.VarD. -Require Import VerdiRaft.VarDRaftLog. - -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlNatInt. -Require Import ExtrOcamlString. - -Require Import Verdi.ExtrOcamlBasicExt. -Require Import Verdi.ExtrOcamlNatIntExt. - -Require Import Verdi.ExtrOcamlBool. -Require Import Verdi.ExtrOcamlList. -Require Import Verdi.ExtrOcamlFinInt. -Require Import Verdi.ExtrOcamlDiskOp. - -Require Import Cheerios.ExtrOcamlCheeriosBasic. -Require Import Cheerios.ExtrOcamlCheeriosNatInt. -Require Import Cheerios.ExtrOcamlCheeriosString. -Require Import Cheerios.ExtrOcamlCheeriosFinInt. - -Extraction "extraction/vard-log/ml/VarDRaftLog.ml" seq transformed_base_params transformed_multi_params transformed_failure_params. +From Verdi Require Import Verdi VarD. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import VarDRaftLog. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString. +From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt. +From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt ExtrOcamlDiskOp. +From Cheerios Require Import ExtrOcamlCheeriosBasic ExtrOcamlCheeriosNatInt. +From Cheerios Require Import ExtrOcamlCheeriosString ExtrOcamlCheeriosFinInt. + +Extraction "extraction/vard-log/ml/VarDRaftLog.ml" seq transformed_base_params + transformed_multi_params transformed_failure_params. diff --git a/extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v b/extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v index bef30ec7..afb40611 100644 --- a/extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v +++ b/extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v @@ -1,24 +1,11 @@ -Require Import Verdi.Verdi. -Require Import Cheerios.Cheerios. - -Require Import Verdi.VarD. -Require Import VerdiRaft.VarDRaftSerializedLog. - -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlNatInt. -Require Import ExtrOcamlString. - -Require Import Verdi.ExtrOcamlBasicExt. -Require Import Verdi.ExtrOcamlNatIntExt. - -Require Import Verdi.ExtrOcamlBool. -Require Import Verdi.ExtrOcamlList. -Require Import Verdi.ExtrOcamlFinInt. -Require Import Verdi.ExtrOcamlDiskOp. - -Require Import Cheerios.ExtrOcamlCheeriosBasic. -Require Import Cheerios.ExtrOcamlCheeriosNatInt. -Require Import Cheerios.ExtrOcamlCheeriosString. -Require Import Cheerios.ExtrOcamlCheeriosFinInt. - -Extraction "extraction/vard-serialized-log/ml/VarDRaftSerializedLog.ml" seq transformed_base_params transformed_multi_params transformed_failure_params. +From Verdi Require Import Verdi VarD. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import VarDRaftSerializedLog. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString. +From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt. +From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt ExtrOcamlDiskOp. +From Cheerios Require Import ExtrOcamlCheeriosBasic ExtrOcamlCheeriosNatInt. +From Cheerios Require Import ExtrOcamlCheeriosString ExtrOcamlCheeriosFinInt. + +Extraction "extraction/vard-serialized-log/ml/VarDRaftSerializedLog.ml" seq transformed_base_params + transformed_multi_params transformed_failure_params. diff --git a/extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v b/extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v index a92740fa..e7d23980 100644 --- a/extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v +++ b/extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v @@ -1,23 +1,11 @@ -Require Import Verdi.Verdi. -Require Import Cheerios.Cheerios. - -Require Import Verdi.VarD. -Require Import VerdiRaft.VarDRaftSerialized. - -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlNatInt. -Require Import ExtrOcamlString. - -Require Import Verdi.ExtrOcamlBasicExt. -Require Import Verdi.ExtrOcamlNatIntExt. - -Require Import Verdi.ExtrOcamlBool. -Require Import Verdi.ExtrOcamlList. -Require Import Verdi.ExtrOcamlFinInt. - -Require Import Cheerios.ExtrOcamlCheeriosBasic. -Require Import Cheerios.ExtrOcamlCheeriosNatInt. -Require Import Cheerios.ExtrOcamlCheeriosString. -Require Import Cheerios.ExtrOcamlCheeriosFinInt. - -Extraction "extraction/vard-serialized/ml/VarDRaftSerialized.ml" seq transformed_base_params transformed_multi_params transformed_failure_params. +From Verdi Require Import Verdi VarD. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import VarDRaftSerialized. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString. +From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt. +From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt. +From Cheerios Require Import ExtrOcamlCheeriosBasic ExtrOcamlCheeriosNatInt. +From Cheerios Require Import ExtrOcamlCheeriosString ExtrOcamlCheeriosFinInt. + +Extraction "extraction/vard-serialized/ml/VarDRaftSerialized.ml" seq transformed_base_params + transformed_multi_params transformed_failure_params. diff --git a/extraction/vard/coq/ExtractVarDRaft.v b/extraction/vard/coq/ExtractVarDRaft.v index 4c5d5db7..0eec7b12 100644 --- a/extraction/vard/coq/ExtractVarDRaft.v +++ b/extraction/vard/coq/ExtractVarDRaft.v @@ -1,16 +1,8 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import VerdiRaft.VarDRaft. - -Require Import ExtrOcamlBasic. -Require Import ExtrOcamlNatInt. -Require Import ExtrOcamlString. - -Require Import Verdi.ExtrOcamlBasicExt. -Require Import Verdi.ExtrOcamlNatIntExt. - -Require Import Verdi.ExtrOcamlBool. -Require Import Verdi.ExtrOcamlList. -Require Import Verdi.ExtrOcamlFinInt. - -Extraction "extraction/vard/ml/VarDRaft.ml" seq vard_raft_base_params vard_raft_multi_params vard_raft_failure_params. +From Verdi Require Import Verdi VarD. +From VerdiRaft Require Import VarDRaft. +From Coq Require Import ExtrOcamlBasic ExtrOcamlNatInt ExtrOcamlString. +From Verdi Require Import ExtrOcamlBasicExt ExtrOcamlNatIntExt. +From Verdi Require Import ExtrOcamlBool ExtrOcamlList ExtrOcamlFinInt. + +Extraction "extraction/vard/ml/VarDRaft.ml" seq vard_raft_base_params + vard_raft_multi_params vard_raft_failure_params. diff --git a/raft-proofs/AllEntriesCandidateEntriesProof.v b/raft-proofs/AllEntriesCandidateEntriesProof.v index 040209ed..b2f0b39c 100644 --- a/raft-proofs/AllEntriesCandidateEntriesProof.v +++ b/raft-proofs/AllEntriesCandidateEntriesProof.v @@ -1,21 +1,11 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. +From VerdiRaft Require Import RefinementCommonTheorems CandidateEntriesInterface. +From VerdiRaft Require Import CroniesCorrectInterface CroniesTermInterface. +From VerdiRaft Require Import AllEntriesTermSanityInterface SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas AllEntriesCandidateEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RefinementCommonTheorems. - -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.CroniesTermInterface. -Require Import VerdiRaft.AllEntriesTermSanityInterface. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. - -Require Import VerdiRaft.AllEntriesCandidateEntriesInterface. - Section AllEntriesCandidateEntries. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AllEntriesIndicesGt0Proof.v b/raft-proofs/AllEntriesIndicesGt0Proof.v index 9ae7e6f7..86b0eefd 100644 --- a/raft-proofs/AllEntriesIndicesGt0Proof.v +++ b/raft-proofs/AllEntriesIndicesGt0Proof.v @@ -1,16 +1,11 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.RefinementSpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions RefinementSpecLemmas. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. +From VerdiRaft Require Import AllEntriesIndicesGt0Interface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. - -Require Import VerdiRaft.AllEntriesIndicesGt0Interface. - Section AllEntriesIndicesGt0. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AllEntriesLeaderLogsProof.v b/raft-proofs/AllEntriesLeaderLogsProof.v index 99dd17de..db8bf9a3 100644 --- a/raft-proofs/AllEntriesLeaderLogsProof.v +++ b/raft-proofs/AllEntriesLeaderLogsProof.v @@ -1,21 +1,14 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface LeaderLogsSortedInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. +From VerdiRaft Require Import AllEntriesLogInterface LeaderSublogInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import AllEntriesLeaderLogsInterface. Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersInterface. -Require Import VerdiRaft.AllEntriesLogInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. - -Require Import VerdiRaft.AllEntriesLeaderLogsInterface. - Section AllEntriesLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesLeaderLogsTermProof.v b/raft-proofs/AllEntriesLeaderLogsTermProof.v index 4e05dd5b..e6062886 100644 --- a/raft-proofs/AllEntriesLeaderLogsTermProof.v +++ b/raft-proofs/AllEntriesLeaderLogsTermProof.v @@ -1,14 +1,10 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementSpecLemmas SpecLemmas. +From VerdiRaft Require Import AllEntriesLeaderLogsTermInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.AllEntriesLeaderLogsTermInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. - Section AllEntriesLeaderLogsTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesLeaderSublogProof.v b/raft-proofs/AllEntriesLeaderSublogProof.v index a2eb30f1..77d9d032 100644 --- a/raft-proofs/AllEntriesLeaderSublogProof.v +++ b/raft-proofs/AllEntriesLeaderSublogProof.v @@ -1,22 +1,15 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.RefinementCommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import AllEntriesLeaderSublogInterface. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import AllEntriesCandidateEntriesInterface. +From VerdiRaft Require Import VotesCorrectInterface CroniesCorrectInterface. +From VerdiRaft Require Import LeaderSublogInterface OneLeaderPerTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.AllEntriesLeaderSublogInterface. - -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.AllEntriesCandidateEntriesInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.OneLeaderPerTermInterface. - Section AllEntriesLeaderSublog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesLogMatchingProof.v b/raft-proofs/AllEntriesLogMatchingProof.v index 3659727e..a18ee5be 100644 --- a/raft-proofs/AllEntriesLogMatchingProof.v +++ b/raft-proofs/AllEntriesLogMatchingProof.v @@ -1,18 +1,12 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RefinementCommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems RefinementCommonTheorems. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import AllEntriesLeaderSublogInterface. +From VerdiRaft Require Import LeaderSublogInterface RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import AllEntriesLogMatchingInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.AllEntriesLeaderSublogInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. - -Require Import VerdiRaft.AllEntriesLogMatchingInterface. - Section AllEntriesLogMatching. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesLogProof.v b/raft-proofs/AllEntriesLogProof.v index 7b533c95..4f6d234c 100644 --- a/raft-proofs/AllEntriesLogProof.v +++ b/raft-proofs/AllEntriesLogProof.v @@ -1,25 +1,17 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas LogsLeaderLogsInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import AllEntriesLeaderLogsTermInterface. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import LeaderLogsSortedInterface TermSanityInterface. +From VerdiRaft Require Import AllEntriesTermSanityInterface AllEntriesLogInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. - -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.AllEntriesLeaderLogsTermInterface. -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.AllEntriesTermSanityInterface. - -Require Import VerdiRaft.AllEntriesLogInterface. - Section AllEntriesLog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesTermSanityProof.v b/raft-proofs/AllEntriesTermSanityProof.v index f0919a0d..3a1cae5c 100644 --- a/raft-proofs/AllEntriesTermSanityProof.v +++ b/raft-proofs/AllEntriesTermSanityProof.v @@ -1,12 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas AllEntriesTermSanityInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.AllEntriesTermSanityInterface. - Section AllEntriesTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesVotesWithLogProof.v b/raft-proofs/AllEntriesVotesWithLogProof.v index 0bfa2cc7..e32fb88c 100644 --- a/raft-proofs/AllEntriesVotesWithLogProof.v +++ b/raft-proofs/AllEntriesVotesWithLogProof.v @@ -1,18 +1,12 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import AllEntriesVotesWithLogInterface AllEntriesLogInterface. +From VerdiRaft Require Import VotesWithLogTermSanityInterface VotesCorrectInterface. +From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. - -Require Import VerdiRaft.AllEntriesVotesWithLogInterface. -Require Import VerdiRaft.AllEntriesLogInterface. -Require Import VerdiRaft.VotesWithLogTermSanityInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.VotesVotesWithLogCorrespondInterface. - Section AllEntriesVotesWithLog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesLeaderProof.v b/raft-proofs/AppendEntriesLeaderProof.v index d20e1bbf..0475f4f3 100644 --- a/raft-proofs/AppendEntriesLeaderProof.v +++ b/raft-proofs/AppendEntriesLeaderProof.v @@ -1,18 +1,11 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface LeaderLogsTermSanityInterface. +From VerdiRaft Require Import OneLeaderPerTermInterface AppendEntriesLeaderInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.OneLeaderPerTermInterface. - -Require Import VerdiRaft.AppendEntriesLeaderInterface. - Section AppendEntriesLeader. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesReplySublogProof.v b/raft-proofs/AppendEntriesReplySublogProof.v index ea226dd0..6731bec1 100644 --- a/raft-proofs/AppendEntriesReplySublogProof.v +++ b/raft-proofs/AppendEntriesReplySublogProof.v @@ -1,13 +1,9 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft AppendEntriesReplySublogInterface. +From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface. +From VerdiRaft Require Import RaftRefinementInterface AppendEntriesLeaderInterface. Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. -Require Import VerdiRaft.AppendEntriesReplySublogInterface. - -Require Import VerdiRaft.AppendEntriesRequestReplyCorrespondenceInterface. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.AppendEntriesLeaderInterface. - Section AppendEntriesReplySublog. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v index 0da9d969..552782ab 100644 --- a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v +++ b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v @@ -1,17 +1,12 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import SortedInterface LogMatchingInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import NextIndexSafetyInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.NextIndexSafetyInterface. - Section AppendEntriesRequestLeaderLogs. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v index 9583d961..fe8b1195 100644 --- a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v +++ b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v @@ -1,13 +1,9 @@ -Require Import FunctionalExtensionality. - -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.SpecLemmas. +From Coq Require Import FunctionalExtensionality. +From VerdiRaft Require Import Raft SpecLemmas. +From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface. +From Verdi Require Import DupDropReordering. Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. -Require Import VerdiRaft.AppendEntriesRequestReplyCorrespondenceInterface. - -Require Import Verdi.DupDropReordering. Section AppendEntriesRequestReplyCorrespondence. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesRequestTermSanityProof.v b/raft-proofs/AppendEntriesRequestTermSanityProof.v index 290d4f9e..4c70ca83 100644 --- a/raft-proofs/AppendEntriesRequestTermSanityProof.v +++ b/raft-proofs/AppendEntriesRequestTermSanityProof.v @@ -1,10 +1,6 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.AppendEntriesRequestTermSanityInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface SortedInterface. +From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface. Section AppendEntriesRequestTermSanity. diff --git a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v index bda1fa3a..b06467c9 100644 --- a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v +++ b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v @@ -1,13 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersInterface. - Section AppendEntriesRequestsCameFromLeaders. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AppliedEntriesMonotonicProof.v b/raft-proofs/AppliedEntriesMonotonicProof.v index dcb569f9..81b1eeee 100644 --- a/raft-proofs/AppliedEntriesMonotonicProof.v +++ b/raft-proofs/AppliedEntriesMonotonicProof.v @@ -1,23 +1,15 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import StateMachineSafetyInterface. +From VerdiRaft Require Import SortedInterface UniqueIndicesInterface. +From VerdiRaft Require Import LogMatchingInterface MaxIndexSanityInterface. +From VerdiRaft Require Import CommitRecordedCommittedInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import SpecLemmas AppliedEntriesMonotonicInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.UniqueIndicesInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.CommitRecordedCommittedInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. - -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. - Section AppliedEntriesMonotonicProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/AppliedImpliesInputProof.v b/raft-proofs/AppliedImpliesInputProof.v index 648dcafd..61bcc80f 100644 --- a/raft-proofs/AppliedImpliesInputProof.v +++ b/raft-proofs/AppliedImpliesInputProof.v @@ -1,16 +1,10 @@ -Require Import Verdi.InverseTraceRelations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.TraceUtil. -Require Import VerdiRaft.OutputImpliesAppliedInterface. +From Verdi Require Import InverseTraceRelations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import TraceUtil OutputImpliesAppliedInterface. +From VerdiRaft Require Import SpecLemmas AppliedImpliesInputInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.AppliedImpliesInputInterface. - Section AppliedImpliesInputProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/CandidateEntriesProof.v b/raft-proofs/CandidateEntriesProof.v index dfdadcb6..2a42ae7e 100644 --- a/raft-proofs/CandidateEntriesProof.v +++ b/raft-proofs/CandidateEntriesProof.v @@ -1,20 +1,11 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.CroniesTermInterface. - -Require Import VerdiRaft.RefinementCommonTheorems. - -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems CroniesCorrectInterface. +From VerdiRaft Require Import VotesCorrectInterface TermSanityInterface. +From VerdiRaft Require Import CroniesTermInterface RefinementCommonTheorems. +From VerdiRaft Require Import SpecLemmas CandidateEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CandidateEntriesInterface. - Section CandidateEntriesProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/CandidateTermGtLogProof.v b/raft-proofs/CandidateTermGtLogProof.v index 6b00a43a..a96730be 100644 --- a/raft-proofs/CandidateTermGtLogProof.v +++ b/raft-proofs/CandidateTermGtLogProof.v @@ -1,11 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft SpecLemmas TermSanityInterface. +From VerdiRaft Require Import CandidateTermGtLogInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.CandidateTermGtLogInterface. - Section CandidateTermGtLog. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/CandidatesVoteForSelvesProof.v b/raft-proofs/CandidatesVoteForSelvesProof.v index 13dce3a8..acf83725 100644 --- a/raft-proofs/CandidatesVoteForSelvesProof.v +++ b/raft-proofs/CandidatesVoteForSelvesProof.v @@ -1,7 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.CandidatesVoteForSelvesInterface. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import CandidatesVoteForSelvesInterface. Section CandidatesVoteForSelvesProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CausalOrderPreservedProof.v b/raft-proofs/CausalOrderPreservedProof.v index 41af6a94..1e829618 100644 --- a/raft-proofs/CausalOrderPreservedProof.v +++ b/raft-proofs/CausalOrderPreservedProof.v @@ -1,13 +1,10 @@ -Require Import Verdi.TraceRelations. +From Verdi Require Import TraceRelations. +From VerdiRaft Require Import Raft CommonTheorems TraceUtil. +From VerdiRaft Require Import CausalOrderPreservedInterface. +From VerdiRaft Require Import OutputImpliesAppliedInterface. +From VerdiRaft Require Import AppliedImpliesInputInterface. +From VerdiRaft Require Import AppliedEntriesMonotonicInterface. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.TraceUtil. - -Require Import VerdiRaft.CausalOrderPreservedInterface. -Require Import VerdiRaft.OutputImpliesAppliedInterface. -Require Import VerdiRaft.AppliedImpliesInputInterface. -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section CausalOrderPreserved. diff --git a/raft-proofs/CroniesCorrectProof.v b/raft-proofs/CroniesCorrectProof.v index ea77a6ad..fd771173 100644 --- a/raft-proofs/CroniesCorrectProof.v +++ b/raft-proofs/CroniesCorrectProof.v @@ -1,11 +1,7 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CandidatesVoteForSelvesInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.VotesCorrectInterface. - -Require Import VerdiRaft.CroniesCorrectInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CandidatesVoteForSelvesInterface CommonTheorems. +From VerdiRaft Require Import VotesCorrectInterface CroniesCorrectInterface. Section CroniesCorrectProof. diff --git a/raft-proofs/CroniesTermProof.v b/raft-proofs/CroniesTermProof.v index 49f78d51..3f4beee2 100644 --- a/raft-proofs/CroniesTermProof.v +++ b/raft-proofs/CroniesTermProof.v @@ -1,12 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems CroniesTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CroniesTermInterface. - Section CroniesTermProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. @@ -34,9 +30,6 @@ Section CroniesTermProof. repeat find_rewrite. repeat break_match; simpl in *; eauto. Qed. - (* H : handleTimeout h' (snd (nwState net h')) = (out, d, l) - In h0 (cronies (update_elections_data_timeout h' (nwState net h')) t) - *) Lemma handleTimeout_spec : forall h st out st' l t h', diff --git a/raft-proofs/CurrentTermGtZeroProof.v b/raft-proofs/CurrentTermGtZeroProof.v index 69925107..37610375 100644 --- a/raft-proofs/CurrentTermGtZeroProof.v +++ b/raft-proofs/CurrentTermGtZeroProof.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft SpecLemmas CurrentTermGtZeroInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CurrentTermGtZeroInterface. - Section CurrentTermGtZero. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/EndToEndLinearizability.v b/raft-proofs/EndToEndLinearizability.v index 704065e5..da682b34 100644 --- a/raft-proofs/EndToEndLinearizability.v +++ b/raft-proofs/EndToEndLinearizability.v @@ -1,280 +1,278 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.Linearizability. +From VerdiRaft Require Import Raft. +From VerdiRaft Require Import Linearizability. -Require Import VerdiRaft.RaftLinearizableProofs. +From VerdiRaft Require Import RaftLinearizableProofs. -Require Import VerdiRaft.OutputCorrectInterface. -Require Import VerdiRaft.OutputCorrectProof. +From VerdiRaft Require Import OutputCorrectInterface. +From VerdiRaft Require Import OutputCorrectProof. -Require Import VerdiRaft.InputBeforeOutputInterface. -Require Import VerdiRaft.InputBeforeOutputProof. +From VerdiRaft Require Import InputBeforeOutputInterface. +From VerdiRaft Require Import InputBeforeOutputProof. -Require Import VerdiRaft.CausalOrderPreservedInterface. -Require Import VerdiRaft.CausalOrderPreservedProof. +From VerdiRaft Require Import CausalOrderPreservedInterface. +From VerdiRaft Require Import CausalOrderPreservedProof. -Require Import VerdiRaft.AppliedImpliesInputInterface. -Require Import VerdiRaft.AppliedImpliesInputProof. +From VerdiRaft Require Import AppliedImpliesInputInterface. +From VerdiRaft Require Import AppliedImpliesInputProof. -Require Import VerdiRaft.OutputImpliesAppliedInterface. -Require Import VerdiRaft.OutputImpliesAppliedProof. +From VerdiRaft Require Import OutputImpliesAppliedInterface. +From VerdiRaft Require Import OutputImpliesAppliedProof. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.LogMatchingProof. +From VerdiRaft Require Import LogMatchingInterface. +From VerdiRaft Require Import LogMatchingProof. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.SortedProof. +From VerdiRaft Require Import SortedInterface. +From VerdiRaft Require Import SortedProof. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.TermSanityProof. +From VerdiRaft Require Import TermSanityInterface. +From VerdiRaft Require Import TermSanityProof. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.LeaderSublogProof. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import LeaderSublogProof. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RaftRefinementProof. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import RaftRefinementProof. -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.CandidateEntriesProof. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import CandidateEntriesProof. -Require Import VerdiRaft.CroniesTermInterface. -Require Import VerdiRaft.CroniesTermProof. +From VerdiRaft Require Import CroniesTermInterface. +From VerdiRaft Require Import CroniesTermProof. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectProof. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectProof. -Require Import VerdiRaft.VotesLeCurrentTermInterface. -Require Import VerdiRaft.VotesLeCurrentTermProof. +From VerdiRaft Require Import VotesLeCurrentTermInterface. +From VerdiRaft Require Import VotesLeCurrentTermProof. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.VotesCorrectProof. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import VotesCorrectProof. -Require Import VerdiRaft.CandidatesVoteForSelvesInterface. -Require Import VerdiRaft.CandidatesVoteForSelvesProof. +From VerdiRaft Require Import CandidatesVoteForSelvesInterface. +From VerdiRaft Require Import CandidatesVoteForSelvesProof. -Require Import VerdiRaft.OneLeaderPerTermInterface. -Require Import VerdiRaft.OneLeaderPerTermProof. +From VerdiRaft Require Import OneLeaderPerTermInterface. +From VerdiRaft Require Import OneLeaderPerTermProof. -Require Import VerdiRaft.UniqueIndicesInterface. -Require Import VerdiRaft.UniqueIndicesProof. +From VerdiRaft Require Import UniqueIndicesInterface. +From VerdiRaft Require Import UniqueIndicesProof. -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. -Require Import VerdiRaft.AppliedEntriesMonotonicProof. +From VerdiRaft Require Import AppliedEntriesMonotonicInterface. +From VerdiRaft Require Import AppliedEntriesMonotonicProof. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.StateMachineSafetyProof. +From VerdiRaft Require Import StateMachineSafetyInterface. +From VerdiRaft Require Import StateMachineSafetyProof. -Require Import VerdiRaft.MaxIndexSanityInterface. +From VerdiRaft Require Import MaxIndexSanityInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.LeaderCompletenessProof. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import LeaderCompletenessProof. -Require Import VerdiRaft.TransitiveCommitInterface. -Require Import VerdiRaft.TransitiveCommitProof. +From VerdiRaft Require Import TransitiveCommitInterface. +From VerdiRaft Require Import TransitiveCommitProof. -Require Import VerdiRaft.AllEntriesLeaderLogsInterface. -Require Import VerdiRaft.AllEntriesLeaderLogsProof. +From VerdiRaft Require Import AllEntriesLeaderLogsInterface. +From VerdiRaft Require Import AllEntriesLeaderLogsProof. -Require Import VerdiRaft.CommitRecordedCommittedInterface. +From VerdiRaft Require Import CommitRecordedCommittedInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.LeaderLogsTermSanityProof. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import LeaderLogsTermSanityProof. +From VerdiRaft Require Import AllEntriesTermSanityInterface. +From VerdiRaft Require Import AllEntriesTermSanityProof. -Require Import VerdiRaft.AllEntriesTermSanityInterface. -Require Import VerdiRaft.AllEntriesTermSanityProof. +From VerdiRaft Require Import VotesWithLogTermSanityInterface. +From VerdiRaft Require Import VotesWithLogTermSanityProof. -Require Import VerdiRaft.VotesWithLogTermSanityInterface. -Require Import VerdiRaft.VotesWithLogTermSanityProof. +From VerdiRaft Require Import LeaderLogsPreservedInterface. +From VerdiRaft Require Import LeaderLogsPreservedProof. -Require Import VerdiRaft.LeaderLogsPreservedInterface. -Require Import VerdiRaft.LeaderLogsPreservedProof. +From VerdiRaft Require Import PrefixWithinTermInterface. +From VerdiRaft Require Import PrefixWithinTermProof. -Require Import VerdiRaft.PrefixWithinTermInterface. -Require Import VerdiRaft.PrefixWithinTermProof. +From VerdiRaft Require Import EveryEntryWasCreatedInterface. +From VerdiRaft Require Import EveryEntryWasCreatedProof. -Require Import VerdiRaft.EveryEntryWasCreatedInterface. -Require Import VerdiRaft.EveryEntryWasCreatedProof. +From VerdiRaft Require Import EveryEntryWasCreatedHostLogInterface. +From VerdiRaft Require Import EveryEntryWasCreatedHostLogProof. -Require Import VerdiRaft.EveryEntryWasCreatedHostLogInterface. -Require Import VerdiRaft.EveryEntryWasCreatedHostLogProof. +From VerdiRaft Require Import LeaderLogsVotesWithLogInterface. +From VerdiRaft Require Import LeaderLogsVotesWithLogProof. -Require Import VerdiRaft.LeaderLogsVotesWithLogInterface. -Require Import VerdiRaft.LeaderLogsVotesWithLogProof. +From VerdiRaft Require Import AllEntriesLogInterface. +From VerdiRaft Require Import AllEntriesLogProof. -Require Import VerdiRaft.AllEntriesLogInterface. -Require Import VerdiRaft.AllEntriesLogProof. +From VerdiRaft Require Import AllEntriesVotesWithLogInterface. +From VerdiRaft Require Import AllEntriesVotesWithLogProof. -Require Import VerdiRaft.AllEntriesVotesWithLogInterface. -Require Import VerdiRaft.AllEntriesVotesWithLogProof. +From VerdiRaft Require Import VotesWithLogSortedInterface. +From VerdiRaft Require Import VotesWithLogSortedProof. -Require Import VerdiRaft.VotesWithLogSortedInterface. -Require Import VerdiRaft.VotesWithLogSortedProof. +From VerdiRaft Require Import LeaderLogsLogMatchingInterface. +From VerdiRaft Require Import LeaderLogsLogMatchingProof. -Require Import VerdiRaft.LeaderLogsLogMatchingInterface. -Require Import VerdiRaft.LeaderLogsLogMatchingProof. +From VerdiRaft Require Import StateMachineSafetyPrimeInterface. +From VerdiRaft Require Import StateMachineSafetyPrimeProof. -Require Import VerdiRaft.StateMachineSafetyPrimeInterface. -Require Import VerdiRaft.StateMachineSafetyPrimeProof. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsProof. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsProof. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersProof. -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersInterface. -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersProof. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import LeaderLogsSortedProof. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.LeaderLogsSortedProof. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import LeaderLogsContiguousProof. -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.LeaderLogsContiguousProof. +From VerdiRaft Require Import LogsLeaderLogsInterface. +From VerdiRaft Require Import LogsLeaderLogsProof. -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.LogsLeaderLogsProof. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import OneLeaderLogPerTermProof. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.OneLeaderLogPerTermProof. +From VerdiRaft Require Import LeaderLogsSublogInterface. +From VerdiRaft Require Import LeaderLogsSublogProof. -Require Import VerdiRaft.LeaderLogsSublogInterface. -Require Import VerdiRaft.LeaderLogsSublogProof. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsProof. -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsProof. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongProof. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongProof. +From VerdiRaft Require Import NextIndexSafetyInterface. +From VerdiRaft Require Import NextIndexSafetyProof. -Require Import VerdiRaft.NextIndexSafetyInterface. -Require Import VerdiRaft.NextIndexSafetyProof. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasProof. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasProof. +From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface. +From VerdiRaft Require Import LeaderLogsCandidateEntriesProof. -Require Import VerdiRaft.LeaderLogsCandidateEntriesInterface. -Require Import VerdiRaft.LeaderLogsCandidateEntriesProof. +From VerdiRaft Require Import AllEntriesCandidateEntriesInterface. +From VerdiRaft Require Import AllEntriesCandidateEntriesProof. -Require Import VerdiRaft.AllEntriesCandidateEntriesInterface. -Require Import VerdiRaft.AllEntriesCandidateEntriesProof. +From VerdiRaft Require Import AllEntriesLogMatchingInterface. +From VerdiRaft Require Import AllEntriesLogMatchingProof. -Require Import VerdiRaft.AllEntriesLogMatchingInterface. -Require Import VerdiRaft.AllEntriesLogMatchingProof. +From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface. +From VerdiRaft Require Import AppendEntriesRequestTermSanityProof. -Require Import VerdiRaft.AppendEntriesRequestTermSanityInterface. -Require Import VerdiRaft.AppendEntriesRequestTermSanityProof. +From VerdiRaft Require Import AllEntriesLeaderSublogInterface. +From VerdiRaft Require Import AllEntriesLeaderSublogProof. -Require Import VerdiRaft.AllEntriesLeaderSublogInterface. -Require Import VerdiRaft.AllEntriesLeaderSublogProof. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingProof. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingProof. +From VerdiRaft Require Import LastAppliedLeCommitIndexInterface. +From VerdiRaft Require Import LastAppliedLeCommitIndexProof. -Require Import VerdiRaft.LastAppliedLeCommitIndexInterface. -Require Import VerdiRaft.LastAppliedLeCommitIndexProof. +From VerdiRaft Require Import AllEntriesLeaderLogsTermInterface. +From VerdiRaft Require Import AllEntriesLeaderLogsTermProof. -Require Import VerdiRaft.AllEntriesLeaderLogsTermInterface. -Require Import VerdiRaft.AllEntriesLeaderLogsTermProof. +From VerdiRaft Require Import StateMachineCorrectInterface. +From VerdiRaft Require Import StateMachineCorrectProof. -Require Import VerdiRaft.StateMachineCorrectInterface. -Require Import VerdiRaft.StateMachineCorrectProof. +From VerdiRaft Require Import OutputGreatestIdInterface. +From VerdiRaft Require Import OutputGreatestIdProof. -Require Import VerdiRaft.OutputGreatestIdInterface. -Require Import VerdiRaft.OutputGreatestIdProof. +From VerdiRaft Require Import CurrentTermGtZeroInterface. +From VerdiRaft Require Import CurrentTermGtZeroProof. -Require Import VerdiRaft.CurrentTermGtZeroInterface. -Require Import VerdiRaft.CurrentTermGtZeroProof. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneLogProof. -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneLogProof. +From VerdiRaft Require Import TermsAndIndicesFromOneInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneProof. -Require Import VerdiRaft.TermsAndIndicesFromOneInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneProof. +From VerdiRaft Require Import CandidateTermGtLogInterface. +From VerdiRaft Require Import CandidateTermGtLogProof. -Require Import VerdiRaft.CandidateTermGtLogInterface. -Require Import VerdiRaft.CandidateTermGtLogProof. +From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. +From VerdiRaft Require Import VotesVotesWithLogCorrespondProof. -Require Import VerdiRaft.VotesVotesWithLogCorrespondInterface. -Require Import VerdiRaft.VotesVotesWithLogCorrespondProof. +From VerdiRaft Require Import PrevLogLeaderSublogInterface. +From VerdiRaft Require Import PrevLogLeaderSublogProof. -Require Import VerdiRaft.PrevLogLeaderSublogInterface. -Require Import VerdiRaft.PrevLogLeaderSublogProof. +From VerdiRaft Require Import AllEntriesIndicesGt0Interface. +From VerdiRaft Require Import AllEntriesIndicesGt0Proof. -Require Import VerdiRaft.AllEntriesIndicesGt0Interface. -Require Import VerdiRaft.AllEntriesIndicesGt0Proof. +From VerdiRaft Require Import PrevLogCandidateEntriesTermInterface. +From VerdiRaft Require Import PrevLogCandidateEntriesTermProof. -Require Import VerdiRaft.PrevLogCandidateEntriesTermInterface. -Require Import VerdiRaft.PrevLogCandidateEntriesTermProof. +From VerdiRaft Require Import MatchIndexAllEntriesInterface. +From VerdiRaft Require Import MatchIndexAllEntriesProof. -Require Import VerdiRaft.MatchIndexAllEntriesInterface. -Require Import VerdiRaft.MatchIndexAllEntriesProof. +From VerdiRaft Require Import MatchIndexLeaderInterface. +From VerdiRaft Require Import MatchIndexLeaderProof. -Require Import VerdiRaft.MatchIndexLeaderInterface. -Require Import VerdiRaft.MatchIndexLeaderProof. +From VerdiRaft Require Import MatchIndexSanityInterface. +From VerdiRaft Require Import MatchIndexSanityProof. -Require Import VerdiRaft.MatchIndexSanityInterface. -Require Import VerdiRaft.MatchIndexSanityProof. +From VerdiRaft Require Import NoAppendEntriesToLeaderInterface. +From VerdiRaft Require Import NoAppendEntriesToLeaderProof. -Require Import VerdiRaft.NoAppendEntriesToLeaderInterface. -Require Import VerdiRaft.NoAppendEntriesToLeaderProof. +From VerdiRaft Require Import NoAppendEntriesToSelfInterface. +From VerdiRaft Require Import NoAppendEntriesToSelfProof. -Require Import VerdiRaft.NoAppendEntriesToSelfInterface. -Require Import VerdiRaft.NoAppendEntriesToSelfProof. +From VerdiRaft Require Import NoAppendEntriesRepliesToSelfInterface. +From VerdiRaft Require Import NoAppendEntriesRepliesToSelfProof. -Require Import VerdiRaft.NoAppendEntriesRepliesToSelfInterface. -Require Import VerdiRaft.NoAppendEntriesRepliesToSelfProof. +From VerdiRaft Require Import LogAllEntriesInterface. +From VerdiRaft Require Import LogAllEntriesProof. -Require Import VerdiRaft.LogAllEntriesInterface. -Require Import VerdiRaft.LogAllEntriesProof. +From VerdiRaft Require Import AppendEntriesReplySublogInterface. +From VerdiRaft Require Import AppendEntriesReplySublogProof. -Require Import VerdiRaft.AppendEntriesReplySublogInterface. -Require Import VerdiRaft.AppendEntriesReplySublogProof. +From VerdiRaft Require Import LeaderLogsLogPropertiesInterface. +From VerdiRaft Require Import LeaderLogsLogPropertiesProof. -Require Import VerdiRaft.LeaderLogsLogPropertiesInterface. -Require Import VerdiRaft.LeaderLogsLogPropertiesProof. +From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface. +From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceProof. -Require Import VerdiRaft.AppendEntriesRequestReplyCorrespondenceInterface. -Require Import VerdiRaft.AppendEntriesRequestReplyCorrespondenceProof. +From VerdiRaft Require Import AppendEntriesLeaderInterface. +From VerdiRaft Require Import AppendEntriesLeaderProof. -Require Import VerdiRaft.AppendEntriesLeaderInterface. -Require Import VerdiRaft.AppendEntriesLeaderProof. +From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. +From VerdiRaft Require Import RequestVoteMaxIndexMaxTermProof. -Require Import VerdiRaft.RequestVoteMaxIndexMaxTermInterface. -Require Import VerdiRaft.RequestVoteMaxIndexMaxTermProof. +From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. +From VerdiRaft Require Import RequestVoteReplyMoreUpToDateProof. -Require Import VerdiRaft.RequestVoteReplyMoreUpToDateInterface. -Require Import VerdiRaft.RequestVoteReplyMoreUpToDateProof. +From VerdiRaft Require Import RequestVoteReplyTermSanityInterface. +From VerdiRaft Require Import RequestVoteReplyTermSanityProof. -Require Import VerdiRaft.RequestVoteReplyTermSanityInterface. -Require Import VerdiRaft.RequestVoteReplyTermSanityProof. +From VerdiRaft Require Import RequestVoteTermSanityInterface. +From VerdiRaft Require Import RequestVoteTermSanityProof. -Require Import VerdiRaft.RequestVoteTermSanityInterface. -Require Import VerdiRaft.RequestVoteTermSanityProof. +From VerdiRaft Require Import VotedForMoreUpToDateInterface. +From VerdiRaft Require Import VotedForMoreUpToDateProof. -Require Import VerdiRaft.VotedForMoreUpToDateInterface. -Require Import VerdiRaft.VotedForMoreUpToDateProof. +From VerdiRaft Require Import VotedForTermSanityInterface. +From VerdiRaft Require Import VotedForTermSanityProof. -Require Import VerdiRaft.VotedForTermSanityInterface. -Require Import VerdiRaft.VotedForTermSanityProof. +From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface. +From VerdiRaft Require Import VotesReceivedMoreUpToDateProof. -Require Import VerdiRaft.VotesReceivedMoreUpToDateInterface. -Require Import VerdiRaft.VotesReceivedMoreUpToDateProof. +From VerdiRaft Require Import RaftMsgRefinementInterface. +From VerdiRaft Require Import RaftMsgRefinementProof. -Require Import VerdiRaft.RaftMsgRefinementInterface. -Require Import VerdiRaft.RaftMsgRefinementProof. +From VerdiRaft Require Import GhostLogCorrectInterface. +From VerdiRaft Require Import GhostLogCorrectProof. -Require Import VerdiRaft.GhostLogCorrectInterface. -Require Import VerdiRaft.GhostLogCorrectProof. +From VerdiRaft Require Import GhostLogsLogPropertiesInterface. +From VerdiRaft Require Import GhostLogsLogPropertiesProof. -Require Import VerdiRaft.GhostLogsLogPropertiesInterface. -Require Import VerdiRaft.GhostLogsLogPropertiesProof. +From VerdiRaft Require Import InLogInAllEntriesInterface. +From VerdiRaft Require Import InLogInAllEntriesProof. -Require Import VerdiRaft.InLogInAllEntriesInterface. -Require Import VerdiRaft.InLogInAllEntriesProof. - -Require Import VerdiRaft.GhostLogAllEntriesInterface. -Require Import VerdiRaft.GhostLogAllEntriesProof. - -Require Import VerdiRaft.GhostLogLogMatchingInterface. -Require Import VerdiRaft.GhostLogLogMatchingProof. +From VerdiRaft Require Import GhostLogAllEntriesInterface. +From VerdiRaft Require Import GhostLogAllEntriesProof. +From VerdiRaft Require Import GhostLogLogMatchingInterface. +From VerdiRaft Require Import GhostLogLogMatchingProof. #[global] Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. diff --git a/raft-proofs/EveryEntryWasCreatedHostLogProof.v b/raft-proofs/EveryEntryWasCreatedHostLogProof.v index 0f1d5aaa..b17b78a9 100644 --- a/raft-proofs/EveryEntryWasCreatedHostLogProof.v +++ b/raft-proofs/EveryEntryWasCreatedHostLogProof.v @@ -1,9 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. -Require Import VerdiRaft.EveryEntryWasCreatedInterface. -Require Import VerdiRaft.EveryEntryWasCreatedHostLogInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import EveryEntryWasCreatedInterface. +From VerdiRaft Require Import EveryEntryWasCreatedHostLogInterface. Section EveryEntryWasCreated. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/EveryEntryWasCreatedProof.v b/raft-proofs/EveryEntryWasCreatedProof.v index 2633b3c1..d3524ae5 100644 --- a/raft-proofs/EveryEntryWasCreatedProof.v +++ b/raft-proofs/EveryEntryWasCreatedProof.v @@ -1,12 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. - -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. -Require Import VerdiRaft.EveryEntryWasCreatedInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import EveryEntryWasCreatedInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import CommonTheorems. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. diff --git a/raft-proofs/GhostLogAllEntriesProof.v b/raft-proofs/GhostLogAllEntriesProof.v index f5d13f3e..a5c55249 100644 --- a/raft-proofs/GhostLogAllEntriesProof.v +++ b/raft-proofs/GhostLogAllEntriesProof.v @@ -1,16 +1,12 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RaftMsgRefinementInterface. - -Require Import VerdiRaft.InLogInAllEntriesInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RefinementSpecLemmas. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import RaftMsgRefinementInterface. +From VerdiRaft Require Import InLogInAllEntriesInterface. +From VerdiRaft Require Import GhostLogAllEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.GhostLogAllEntriesInterface. - Section GhostLogAllEntriesProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/GhostLogCorrectProof.v b/raft-proofs/GhostLogCorrectProof.v index b20f46d8..a786da1d 100644 --- a/raft-proofs/GhostLogCorrectProof.v +++ b/raft-proofs/GhostLogCorrectProof.v @@ -1,15 +1,11 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RaftMsgRefinementInterface. - -Require Import VerdiRaft.NextIndexSafetyInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import RaftMsgRefinementInterface. +From VerdiRaft Require Import NextIndexSafetyInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import GhostLogCorrectInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.GhostLogCorrectInterface. Section GhostLogCorrectProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/GhostLogLogMatchingProof.v b/raft-proofs/GhostLogLogMatchingProof.v index 15f1b9ed..32f8f26e 100644 --- a/raft-proofs/GhostLogLogMatchingProof.v +++ b/raft-proofs/GhostLogLogMatchingProof.v @@ -1,25 +1,17 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RaftMsgRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.SpecLemmas. - +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RaftMsgRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import GhostLogCorrectInterface. +From VerdiRaft Require Import GhostLogsLogPropertiesInterface. +From VerdiRaft Require Import TermSanityInterface. +From VerdiRaft Require Import AllEntriesLeaderSublogInterface. +From VerdiRaft Require Import GhostLogAllEntriesInterface. +From VerdiRaft Require Import GhostLogLogMatchingInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.GhostLogCorrectInterface. -Require Import VerdiRaft.GhostLogsLogPropertiesInterface. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.AllEntriesLeaderSublogInterface. -Require Import VerdiRaft.GhostLogAllEntriesInterface. - -Require Import VerdiRaft.GhostLogLogMatchingInterface. - - Section GhostLogLogMatching. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/GhostLogsLogPropertiesProof.v b/raft-proofs/GhostLogsLogPropertiesProof.v index 7d449dd7..12c2502a 100644 --- a/raft-proofs/GhostLogsLogPropertiesProof.v +++ b/raft-proofs/GhostLogsLogPropertiesProof.v @@ -1,11 +1,9 @@ -Require Import Verdi.GhostSimulations. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftMsgRefinementInterface. +From VerdiRaft Require Import GhostLogsLogPropertiesInterface. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftMsgRefinementInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.GhostLogsLogPropertiesInterface. - Section GhostLogsLogProperties. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/InLogInAllEntriesProof.v b/raft-proofs/InLogInAllEntriesProof.v index c2867ecd..91f731e6 100644 --- a/raft-proofs/InLogInAllEntriesProof.v +++ b/raft-proofs/InLogInAllEntriesProof.v @@ -1,14 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import InLogInAllEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.InLogInAllEntriesInterface. - Section InLogInAllEntries. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/InputBeforeOutputProof.v b/raft-proofs/InputBeforeOutputProof.v index a2c74fd0..fe0df412 100644 --- a/raft-proofs/InputBeforeOutputProof.v +++ b/raft-proofs/InputBeforeOutputProof.v @@ -1,21 +1,13 @@ -Require Import Verdi.GhostSimulations. -Require Import Verdi.InverseTraceRelations. +From Verdi Require Import GhostSimulations InverseTraceRelations. +From VerdiRaft Require Import Raft CommonTheorems TraceUtil SpecLemmas. +From VerdiRaft Require Import InputBeforeOutputInterface. +From VerdiRaft Require Import AppliedImpliesInputInterface. +From VerdiRaft Require Import OutputImpliesAppliedInterface. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import SortedInterface LogMatchingInterface. +From VerdiRaft Require Import StateMachineSafetyInterface MaxIndexSanityInterface. +From VerdiRaft Require Import UniqueIndicesInterface. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.TraceUtil. - -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.InputBeforeOutputInterface. -Require Import VerdiRaft.AppliedImpliesInputInterface. -Require Import VerdiRaft.OutputImpliesAppliedInterface. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.UniqueIndicesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section InputBeforeOutput. diff --git a/raft-proofs/LastAppliedCommitIndexMatchingProof.v b/raft-proofs/LastAppliedCommitIndexMatchingProof.v index f1b592d6..01cbb8a1 100644 --- a/raft-proofs/LastAppliedCommitIndexMatchingProof.v +++ b/raft-proofs/LastAppliedCommitIndexMatchingProof.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. - -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. +From VerdiRaft Require Import Raft CommonDefinitions. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import LogMatchingInterface StateMachineSafetyInterface. +From VerdiRaft Require Import MaxIndexSanityInterface. Section LastAppliedCommitIndexMatching. diff --git a/raft-proofs/LastAppliedLeCommitIndexProof.v b/raft-proofs/LastAppliedLeCommitIndexProof.v index 6c577274..b4a391f9 100644 --- a/raft-proofs/LastAppliedLeCommitIndexProof.v +++ b/raft-proofs/LastAppliedLeCommitIndexProof.v @@ -1,11 +1,8 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft LastAppliedLeCommitIndexInterface. +From VerdiRaft Require Import SpecLemmas CommonTheorems. -Require Import VerdiRaft.LastAppliedLeCommitIndexInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.CommonTheorems. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - Section LastAppliedLeCommitIndex. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LeaderCompletenessProof.v b/raft-proofs/LeaderCompletenessProof.v index a6e9e660..7c5d924d 100644 --- a/raft-proofs/LeaderCompletenessProof.v +++ b/raft-proofs/LeaderCompletenessProof.v @@ -1,21 +1,16 @@ -Require Import Sumbool. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.RefinementCommonDefinitions. - -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.PrefixWithinTermInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.LeaderLogsPreservedInterface. -Require Import VerdiRaft.EveryEntryWasCreatedInterface. -Require Import VerdiRaft.LeaderLogsVotesWithLogInterface. -Require Import VerdiRaft.AllEntriesVotesWithLogInterface. -Require Import VerdiRaft.VotesWithLogSortedInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneInterface. -Require Import VerdiRaft.LeaderLogsLogMatchingInterface. +From Coq Require Import Sumbool. +From VerdiRaft Require Import Raft CommonTheorems RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import PrefixWithinTermInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import LeaderLogsPreservedInterface. +From VerdiRaft Require Import EveryEntryWasCreatedInterface. +From VerdiRaft Require Import LeaderLogsVotesWithLogInterface. +From VerdiRaft Require Import AllEntriesVotesWithLogInterface. +From VerdiRaft Require Import VotesWithLogSortedInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneInterface. +From VerdiRaft Require Import LeaderLogsLogMatchingInterface. Section LeaderCompleteness. diff --git a/raft-proofs/LeaderLogsCandidateEntriesProof.v b/raft-proofs/LeaderLogsCandidateEntriesProof.v index ac0d95d6..922c9040 100644 --- a/raft-proofs/LeaderLogsCandidateEntriesProof.v +++ b/raft-proofs/LeaderLogsCandidateEntriesProof.v @@ -1,21 +1,14 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems RefinementCommonTheorems. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import CroniesTermInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RefinementCommonTheorems. - -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.CroniesTermInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. - -Require Import VerdiRaft.LeaderLogsCandidateEntriesInterface. - Section CandidateEntriesInterface. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LeaderLogsContiguousProof.v b/raft-proofs/LeaderLogsContiguousProof.v index d2d60ad0..aa24476c 100644 --- a/raft-proofs/LeaderLogsContiguousProof.v +++ b/raft-proofs/LeaderLogsContiguousProof.v @@ -1,14 +1,10 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import LogMatchingInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.LogMatchingInterface. - Section LeaderLogsContiguous. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsLogMatchingProof.v b/raft-proofs/LeaderLogsLogMatchingProof.v index ca3495be..6b4b035a 100644 --- a/raft-proofs/LeaderLogsLogMatchingProof.v +++ b/raft-proofs/LeaderLogsLogMatchingProof.v @@ -1,24 +1,17 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import LogMatchingInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import SortedInterface LeaderLogsSublogInterface. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneInterface. +From VerdiRaft Require Import LeaderLogsLogMatchingInterface. 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}. diff --git a/raft-proofs/LeaderLogsLogPropertiesProof.v b/raft-proofs/LeaderLogsLogPropertiesProof.v index e6594721..e0850d5c 100644 --- a/raft-proofs/LeaderLogsLogPropertiesProof.v +++ b/raft-proofs/LeaderLogsLogPropertiesProof.v @@ -1,10 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. +From VerdiRaft Require Import LeaderLogsLogPropertiesInterface. +From VerdiRaft Require Import RefinementSpecLemmas. -Require Import VerdiRaft.LeaderLogsLogPropertiesInterface. -Require Import VerdiRaft.RefinementSpecLemmas. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsLogProperties. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsPreservedProof.v b/raft-proofs/LeaderLogsPreservedProof.v index c191e820..709274e6 100644 --- a/raft-proofs/LeaderLogsPreservedProof.v +++ b/raft-proofs/LeaderLogsPreservedProof.v @@ -1,18 +1,15 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RefinementCommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. +From VerdiRaft Require Import RefinementCommonTheorems. +From VerdiRaft Require Import LeaderLogsPreservedInterface. +From VerdiRaft Require Import LogsLeaderLogsInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeaderLogsPreservedInterface. -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.LeaderLogsCandidateEntriesInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. - Section LeaderLogsPreserved. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsSortedProof.v b/raft-proofs/LeaderLogsSortedProof.v index 35d0cc63..ecd861fa 100644 --- a/raft-proofs/LeaderLogsSortedProof.v +++ b/raft-proofs/LeaderLogsSortedProof.v @@ -1,17 +1,11 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. - -Require Import VerdiRaft.SpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions SpecLemmas. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import SortedInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.SortedInterface. - - Section LeaderLogsSorted. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LeaderLogsSublogProof.v b/raft-proofs/LeaderLogsSublogProof.v index b2a84b34..662721f1 100644 --- a/raft-proofs/LeaderLogsSublogProof.v +++ b/raft-proofs/LeaderLogsSublogProof.v @@ -1,25 +1,17 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import EveryEntryWasCreatedInterface. +From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import RefinementCommonTheorems. +From VerdiRaft Require Import LeaderLogsSublogInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.EveryEntryWasCreatedInterface. -Require Import VerdiRaft.LeaderLogsCandidateEntriesInterface. - -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.VotesCorrectInterface. - -Require Import VerdiRaft.RefinementCommonTheorems. - -Require Import VerdiRaft.LeaderLogsSublogInterface. - Section LeaderLogsSublog. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LeaderLogsTermSanityProof.v b/raft-proofs/LeaderLogsTermSanityProof.v index b5d26a12..699fefdc 100644 --- a/raft-proofs/LeaderLogsTermSanityProof.v +++ b/raft-proofs/LeaderLogsTermSanityProof.v @@ -1,15 +1,11 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import CandidateTermGtLogInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CandidateTermGtLogInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. - Section LeaderLogsTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsVotesWithLogProof.v b/raft-proofs/LeaderLogsVotesWithLogProof.v index ba95a000..7974e743 100644 --- a/raft-proofs/LeaderLogsVotesWithLogProof.v +++ b/raft-proofs/LeaderLogsVotesWithLogProof.v @@ -1,14 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface. +From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. +From VerdiRaft Require Import LeaderLogsVotesWithLogInterface. -Require Import VerdiRaft.VotesReceivedMoreUpToDateInterface. -Require Import VerdiRaft.RequestVoteReplyMoreUpToDateInterface. - -Require Import VerdiRaft.LeaderLogsVotesWithLogInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsVotesWithLog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderSublogProof.v b/raft-proofs/LeaderSublogProof.v index e2cfd07a..5412b987 100644 --- a/raft-proofs/LeaderSublogProof.v +++ b/raft-proofs/LeaderSublogProof.v @@ -1,22 +1,16 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.OneLeaderPerTermInterface. - -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.RefinementCommonTheorems. - -Require Import VerdiRaft.LeaderSublogInterface. - -#[global] -Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. -#[global] -Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. -#[global] -Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import OneLeaderPerTermInterface. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import RefinementCommonTheorems. +From VerdiRaft Require Import LeaderSublogInterface. + +#[global] Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. +#[global] Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. +#[global] Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. Section LeaderSublogProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeadersHaveLeaderLogsProof.v b/raft-proofs/LeadersHaveLeaderLogsProof.v index 74dab59e..b5503079 100644 --- a/raft-proofs/LeadersHaveLeaderLogsProof.v +++ b/raft-proofs/LeadersHaveLeaderLogsProof.v @@ -1,12 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. - Section LeadersHaveLeaderLogs. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v index cd2ccc87..0cd675a3 100644 --- a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v +++ b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v @@ -1,11 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. - Section LeadersHaveLeaderLogsStrong. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LogAllEntriesProof.v b/raft-proofs/LogAllEntriesProof.v index c2ffaf40..7a4f306a 100644 --- a/raft-proofs/LogAllEntriesProof.v +++ b/raft-proofs/LogAllEntriesProof.v @@ -1,15 +1,11 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import TermSanityInterface. +From VerdiRaft Require Import LogAllEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.LogAllEntriesInterface. - Section LogAllEntries. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/LogMatchingProof.v b/raft-proofs/LogMatchingProof.v index bbc090bf..de559742 100644 --- a/raft-proofs/LogMatchingProof.v +++ b/raft-proofs/LogMatchingProof.v @@ -1,19 +1,10 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.UniqueIndicesInterface. -Require Import VerdiRaft.LeaderSublogInterface. - -Require Import VerdiRaft.LogMatchingInterface. - -#[global] -Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. -#[global] -Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. -#[global] -Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. +From VerdiRaft Require Import Raft SpecLemmas CommonTheorems. +From VerdiRaft Require Import SortedInterface UniqueIndicesInterface. +From VerdiRaft Require Import LeaderSublogInterface LogMatchingInterface. + +#[global] Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. +#[global] Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. +#[global] Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. Section LogMatchingProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LogsLeaderLogsProof.v b/raft-proofs/LogsLeaderLogsProof.v index 3c21edb8..12a15c35 100644 --- a/raft-proofs/LogsLeaderLogsProof.v +++ b/raft-proofs/LogsLeaderLogsProof.v @@ -1,24 +1,17 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.SpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import LogsLeaderLogsInterface. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import LeaderLogsLogMatchingInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import NextIndexSafetyInterface. +From VerdiRaft Require Import SortedInterface LeaderLogsLogPropertiesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.LeaderLogsLogMatchingInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. -Require Import VerdiRaft.NextIndexSafetyInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.LeaderLogsLogPropertiesInterface. - Section LogsLeaderLogs. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/MatchIndexAllEntriesProof.v b/raft-proofs/MatchIndexAllEntriesProof.v index a9b96a11..0db4fbb9 100644 --- a/raft-proofs/MatchIndexAllEntriesProof.v +++ b/raft-proofs/MatchIndexAllEntriesProof.v @@ -1,31 +1,25 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RefinementCommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems RefinementCommonTheorems. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import NoAppendEntriesToLeaderInterface. +From VerdiRaft Require Import NoAppendEntriesToSelfInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import LogAllEntriesInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import MatchIndexLeaderInterface. +From VerdiRaft Require Import MatchIndexSanityInterface. +From VerdiRaft Require Import AppendEntriesReplySublogInterface. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import MatchIndexAllEntriesInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.NoAppendEntriesToLeaderInterface. -Require Import VerdiRaft.NoAppendEntriesToSelfInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.LogAllEntriesInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.MatchIndexLeaderInterface. -Require Import VerdiRaft.MatchIndexSanityInterface. -Require Import VerdiRaft.AppendEntriesReplySublogInterface. -Require Import VerdiRaft.CandidateEntriesInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. - -Require Import VerdiRaft.MatchIndexAllEntriesInterface. - Section MatchIndexAllEntries. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/MatchIndexLeaderProof.v b/raft-proofs/MatchIndexLeaderProof.v index 6cc201cd..ea2b6563 100644 --- a/raft-proofs/MatchIndexLeaderProof.v +++ b/raft-proofs/MatchIndexLeaderProof.v @@ -1,13 +1,9 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft SpecLemmas. +From VerdiRaft Require Import NoAppendEntriesRepliesToSelfInterface. +From VerdiRaft Require Import MatchIndexLeaderInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.NoAppendEntriesRepliesToSelfInterface. - -Require Import VerdiRaft.MatchIndexLeaderInterface. - Section MatchIndexLeader. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/MatchIndexSanityProof.v b/raft-proofs/MatchIndexSanityProof.v index 6042879a..165b9c16 100644 --- a/raft-proofs/MatchIndexSanityProof.v +++ b/raft-proofs/MatchIndexSanityProof.v @@ -1,15 +1,10 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import AppendEntriesReplySublogInterface. +From VerdiRaft Require Import MatchIndexSanityInterface. +From VerdiRaft Require Import SortedInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.AppendEntriesReplySublogInterface. - -Require Import VerdiRaft.MatchIndexSanityInterface. -Require Import VerdiRaft.SortedInterface. - Section MatchIndexSanity. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/NextIndexSafetyProof.v b/raft-proofs/NextIndexSafetyProof.v index cd096d6a..e5d0a0db 100644 --- a/raft-proofs/NextIndexSafetyProof.v +++ b/raft-proofs/NextIndexSafetyProof.v @@ -1,15 +1,9 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import AppendEntriesReplySublogInterface. +From VerdiRaft Require Import SortedInterface NextIndexSafetyInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.AppendEntriesReplySublogInterface. -Require Import VerdiRaft.SortedInterface. - -Require Import VerdiRaft.NextIndexSafetyInterface. - Section NextIndexSafety. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/NoAppendEntriesRepliesToSelfProof.v b/raft-proofs/NoAppendEntriesRepliesToSelfProof.v index 3c91acea..8e2016f5 100644 --- a/raft-proofs/NoAppendEntriesRepliesToSelfProof.v +++ b/raft-proofs/NoAppendEntriesRepliesToSelfProof.v @@ -1,9 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.NoAppendEntriesRepliesToSelfInterface. - -Require Import VerdiRaft.NoAppendEntriesToSelfInterface. +From VerdiRaft Require Import Raft SpecLemmas. +From VerdiRaft Require Import NoAppendEntriesRepliesToSelfInterface. +From VerdiRaft Require Import NoAppendEntriesToSelfInterface. Section NoAppendEntriesRepliesToSelf. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/NoAppendEntriesToLeaderProof.v b/raft-proofs/NoAppendEntriesToLeaderProof.v index eca4aec4..873a437a 100644 --- a/raft-proofs/NoAppendEntriesToLeaderProof.v +++ b/raft-proofs/NoAppendEntriesToLeaderProof.v @@ -1,13 +1,10 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.NoAppendEntriesToSelfInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.AppendEntriesRequestsCameFromLeadersInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. - -Require Import VerdiRaft.NoAppendEntriesToLeaderInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import NoAppendEntriesToSelfInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import NoAppendEntriesToLeaderInterface. Section NoAppendEntriesToLeader. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/NoAppendEntriesToSelfProof.v b/raft-proofs/NoAppendEntriesToSelfProof.v index 5ba7d030..5dbd526d 100644 --- a/raft-proofs/NoAppendEntriesToSelfProof.v +++ b/raft-proofs/NoAppendEntriesToSelfProof.v @@ -1,7 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.NoAppendEntriesToSelfInterface. +From VerdiRaft Require Import Raft SpecLemmas. +From VerdiRaft Require Import NoAppendEntriesToSelfInterface. Section NoAppendEntriesToSelf. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OneLeaderLogPerTermProof.v b/raft-proofs/OneLeaderLogPerTermProof.v index 33fb9e0e..28c50c3c 100644 --- a/raft-proofs/OneLeaderLogPerTermProof.v +++ b/raft-proofs/OneLeaderLogPerTermProof.v @@ -1,21 +1,17 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.RefinementCommonTheorems. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import RefinementCommonTheorems. +From VerdiRaft Require Import LeaderLogsVotesWithLogInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. +From VerdiRaft Require Import LeaderLogsTermSanityInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.LeaderLogsVotesWithLogInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.VotesVotesWithLogCorrespondInterface. -Require Import VerdiRaft.LeaderLogsTermSanityInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. - Section OneLeaderLogPerTerm. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/OneLeaderPerTermProof.v b/raft-proofs/OneLeaderPerTermProof.v index 4a56ec35..c51f86d8 100644 --- a/raft-proofs/OneLeaderPerTermProof.v +++ b/raft-proofs/OneLeaderPerTermProof.v @@ -1,13 +1,9 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.VotesCorrectInterface. - -Require Import VerdiRaft.OneLeaderPerTermInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import OneLeaderPerTermInterface. Section OneLeaderPerTermProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OutputCorrectProof.v b/raft-proofs/OutputCorrectProof.v index 527c2345..edf65018 100644 --- a/raft-proofs/OutputCorrectProof.v +++ b/raft-proofs/OutputCorrectProof.v @@ -1,15 +1,10 @@ -Require Import Verdi.TraceRelations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.OutputCorrectInterface. -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. -Require Import VerdiRaft.TraceUtil. - -Require Import VerdiRaft.StateMachineCorrectInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. -Require Import VerdiRaft.LogMatchingInterface. +From Verdi Require Import TraceRelations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import OutputCorrectInterface. +From VerdiRaft Require Import AppliedEntriesMonotonicInterface. +From VerdiRaft Require Import TraceUtil StateMachineCorrectInterface. +From VerdiRaft Require Import SortedInterface LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import LogMatchingInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. diff --git a/raft-proofs/OutputGreatestIdProof.v b/raft-proofs/OutputGreatestIdProof.v index 6b8cf63d..43d05573 100644 --- a/raft-proofs/OutputGreatestIdProof.v +++ b/raft-proofs/OutputGreatestIdProof.v @@ -1,21 +1,15 @@ -Require Import Verdi.TraceRelations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.StateMachineCorrectInterface. -Require Import VerdiRaft.LastAppliedCommitIndexMatchingInterface. -Require Import VerdiRaft.TraceUtil. +From Verdi Require Import TraceRelations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import LogMatchingInterface StateMachineSafetyInterface. +From VerdiRaft Require Import AppliedEntriesMonotonicInterface. +From VerdiRaft Require Import MaxIndexSanityInterface. +From VerdiRaft Require Import StateMachineCorrectInterface. +From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. +From VerdiRaft Require Import TraceUtil SortedInterface. +From VerdiRaft Require Import OutputGreatestIdInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.SortedInterface. - -Require Import VerdiRaft.OutputGreatestIdInterface. - Section OutputGreatestId. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/OutputImpliesAppliedProof.v b/raft-proofs/OutputImpliesAppliedProof.v index 1388fccf..ea72539e 100644 --- a/raft-proofs/OutputImpliesAppliedProof.v +++ b/raft-proofs/OutputImpliesAppliedProof.v @@ -1,19 +1,13 @@ -Require Import Verdi.TraceRelations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.AppliedEntriesMonotonicInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.TraceUtil. +From Verdi Require Import TraceRelations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import LogMatchingInterface StateMachineSafetyInterface. +From VerdiRaft Require Import AppliedEntriesMonotonicInterface. +From VerdiRaft Require Import MaxIndexSanityInterface. +From VerdiRaft Require Import TraceUtil SortedInterface. +From VerdiRaft Require Import OutputImpliesAppliedInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.SortedInterface. - -Require Import VerdiRaft.OutputImpliesAppliedInterface. - Section OutputImpliesApplied. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/PrefixWithinTermProof.v b/raft-proofs/PrefixWithinTermProof.v index 8720fdb7..72b26003 100644 --- a/raft-proofs/PrefixWithinTermProof.v +++ b/raft-proofs/PrefixWithinTermProof.v @@ -1,26 +1,21 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems SpecLemmas. +From VerdiRaft Require Import PrefixWithinTermInterface. +From VerdiRaft Require Import LogsLeaderLogsInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import LeaderLogsSublogInterface. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import NextIndexSafetyInterface. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import AllEntriesLogMatchingInterface. +From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface. +From VerdiRaft Require Import AllEntriesLeaderSublogInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.PrefixWithinTermInterface. -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.LeaderLogsSublogInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.NextIndexSafetyInterface. -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.AllEntriesLogMatchingInterface. -Require Import VerdiRaft.AppendEntriesRequestTermSanityInterface. -Require Import VerdiRaft.AllEntriesLeaderSublogInterface. - Section PrefixWithinTerm. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/PrevLogCandidateEntriesTermProof.v b/raft-proofs/PrevLogCandidateEntriesTermProof.v index d9f141be..08491d35 100644 --- a/raft-proofs/PrevLogCandidateEntriesTermProof.v +++ b/raft-proofs/PrevLogCandidateEntriesTermProof.v @@ -1,19 +1,14 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CroniesTermInterface. - -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.CandidateEntriesInterface. - -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.RefinementCommonTheorems. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import CroniesTermInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import CandidateEntriesInterface. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import RefinementCommonTheorems. +From VerdiRaft Require Import PrevLogCandidateEntriesTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.PrevLogCandidateEntriesTermInterface. - Section PrevLogCandidateEntriesTerm. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/PrevLogLeaderSublogProof.v b/raft-proofs/PrevLogLeaderSublogProof.v index 31aef76c..90588451 100644 --- a/raft-proofs/PrevLogLeaderSublogProof.v +++ b/raft-proofs/PrevLogLeaderSublogProof.v @@ -1,24 +1,16 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. - -Require Import VerdiRaft.PrevLogCandidateEntriesTermInterface. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. -Require Import VerdiRaft.LeaderSublogInterface. - -Require Import VerdiRaft.PrevLogLeaderSublogInterface. - -#[global] -Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. -#[global] -Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. -#[global] -Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. - +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. +From VerdiRaft Require Import PrevLogCandidateEntriesTermInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import PrevLogLeaderSublogInterface. + +#[global] Hint Extern 4 (@BaseParams) => apply base_params : typeclass_instances. +#[global] Hint Extern 4 (@MultiParams _) => apply multi_params : typeclass_instances. +#[global] Hint Extern 4 (@FailureParams _ _) => apply failure_params : typeclass_instances. Section PrevLogLeaderSublogProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RaftMsgRefinementProof.v b/raft-proofs/RaftMsgRefinementProof.v index cf1f4384..8451449e 100644 --- a/raft-proofs/RaftMsgRefinementProof.v +++ b/raft-proofs/RaftMsgRefinementProof.v @@ -1,19 +1,14 @@ -Require Import FunctionalExtensionality. - -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import Verdi.DupDropReordering. -Require Import VerdiRaft.SpecLemmas. - -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RaftMsgRefinementInterface. +From Coq Require Import FunctionalExtensionality. +From Verdi Require Import GhostSimulations DupDropReordering. +From VerdiRaft Require Import Raft SpecLemmas. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import RaftMsgRefinementInterface. Section RaftMsgRefinement. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Lemma msg_refined_raft_invariant_handle_message P : forall xs p ys net st' ps' gd d l, msg_refined_raft_net_invariant_append_entries P -> diff --git a/raft-proofs/RaftRefinementProof.v b/raft-proofs/RaftRefinementProof.v index e4be10f8..62d1b7be 100644 --- a/raft-proofs/RaftRefinementProof.v +++ b/raft-proofs/RaftRefinementProof.v @@ -1,11 +1,6 @@ -Require Import FunctionalExtensionality. - -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.RaftRefinementInterface. - -Set Bullet Behavior "Strict Subproofs". +From Coq Require Import FunctionalExtensionality. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section RaftRefinementProof. Context {orig_base_params : BaseParams}. @@ -631,9 +626,6 @@ Section RaftRefinementProof. Qed. End RaftRefinementProof. -#[global] -Hint Extern 4 (@BaseParams) => apply raft_refined_base_params : typeclass_instances. -#[global] -Hint Extern 4 (@MultiParams _) => apply raft_refined_multi_params : typeclass_instances. -#[global] -Hint Extern 4 (@FailureParams _ _) => apply raft_refined_failure_params : typeclass_instances. +#[global] Hint Extern 4 (@BaseParams) => apply raft_refined_base_params : typeclass_instances. +#[global] Hint Extern 4 (@MultiParams _) => apply raft_refined_multi_params : typeclass_instances. +#[global] Hint Extern 4 (@FailureParams _ _) => apply raft_refined_failure_params : typeclass_instances. diff --git a/raft-proofs/RefinedLogMatchingLemmasProof.v b/raft-proofs/RefinedLogMatchingLemmasProof.v index 541426ff..3946c618 100644 --- a/raft-proofs/RefinedLogMatchingLemmasProof.v +++ b/raft-proofs/RefinedLogMatchingLemmasProof.v @@ -1,14 +1,9 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. - -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.AllEntriesIndicesGt0Interface. - -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. +From VerdiRaft Require Import LogMatchingInterface SortedInterface. +From VerdiRaft Require Import AllEntriesIndicesGt0Interface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. Section RefinedLogMatchingLemmas. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v index 4defe720..36b79855 100644 --- a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v +++ b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v @@ -1,12 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. +From VerdiRaft Require Import RequestVoteTermSanityInterface. -Require Import VerdiRaft.RequestVoteMaxIndexMaxTermInterface. -Require Import VerdiRaft.RequestVoteTermSanityInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteMaxIndexMaxTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v index 48dc3e78..b362f7d6 100644 --- a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v +++ b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v @@ -1,16 +1,11 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas CommonTheorems. +From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. +From VerdiRaft Require Import RequestVoteReplyTermSanityInterface. +From VerdiRaft Require Import VotedForMoreUpToDateInterface. +From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. -Require Import VerdiRaft.RequestVoteMaxIndexMaxTermInterface. -Require Import VerdiRaft.RequestVoteReplyTermSanityInterface. -Require Import VerdiRaft.VotedForMoreUpToDateInterface. - -Require Import VerdiRaft.RequestVoteReplyMoreUpToDateInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteReplyMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteReplyTermSanityProof.v b/raft-proofs/RequestVoteReplyTermSanityProof.v index a506ca31..9112892c 100644 --- a/raft-proofs/RequestVoteReplyTermSanityProof.v +++ b/raft-proofs/RequestVoteReplyTermSanityProof.v @@ -1,11 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface. +From VerdiRaft Require Import RequestVoteReplyTermSanityInterface. -Require Import VerdiRaft.RequestVoteTermSanityInterface. -Require Import VerdiRaft.RequestVoteReplyTermSanityInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteReplyTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteTermSanityProof.v b/raft-proofs/RequestVoteTermSanityProof.v index 6491a7dd..ac1922ff 100644 --- a/raft-proofs/RequestVoteTermSanityProof.v +++ b/raft-proofs/RequestVoteTermSanityProof.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface. -Require Import VerdiRaft.RequestVoteTermSanityInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/SortedProof.v b/raft-proofs/SortedProof.v index 4328d825..1b1e5c8d 100644 --- a/raft-proofs/SortedProof.v +++ b/raft-proofs/SortedProof.v @@ -1,8 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.SortedInterface. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import TermSanityInterface SortedInterface. Section SortedProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/StateMachineCorrectProof.v b/raft-proofs/StateMachineCorrectProof.v index 6b3af4d9..c46c8b88 100644 --- a/raft-proofs/StateMachineCorrectProof.v +++ b/raft-proofs/StateMachineCorrectProof.v @@ -1,18 +1,13 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft SpecLemmas CommonTheorems. +From VerdiRaft Require Import SortedInterface DecompositionWithPostState. +From VerdiRaft Require Import MaxIndexSanityInterface. +From VerdiRaft Require Import StateMachineSafetyInterface. +From VerdiRaft Require Import LogMatchingInterface. +From VerdiRaft Require Import StateMachineCorrectInterface. +From Coq Require Import ZArith. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.DecompositionWithPostState. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.StateMachineCorrectInterface. -Require Import ZArith. - Section StateMachineCorrect. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/StateMachineSafetyPrimeProof.v b/raft-proofs/StateMachineSafetyPrimeProof.v index f90ffe6a..ad05c63f 100644 --- a/raft-proofs/StateMachineSafetyPrimeProof.v +++ b/raft-proofs/StateMachineSafetyPrimeProof.v @@ -1,21 +1,18 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.StateMachineSafetyPrimeInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.LeaderLogsContiguousInterface. -Require Import VerdiRaft.AllEntriesLeaderLogsInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.UniqueIndicesInterface. -Require Import VerdiRaft.AppendEntriesRequestLeaderLogsInterface. -Require Import VerdiRaft.LeaderLogsSortedInterface. -Require Import VerdiRaft.LeaderLogsLogMatchingInterface. -Require Import VerdiRaft.LogsLeaderLogsInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import CommonTheorems Raft. +From VerdiRaft Require Import SortedInterface RaftRefinementInterface. +From VerdiRaft Require Import StateMachineSafetyPrimeInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import LeaderLogsContiguousInterface. +From VerdiRaft Require Import AllEntriesLeaderLogsInterface. +From VerdiRaft Require Import LogMatchingInterface. +From VerdiRaft Require Import UniqueIndicesInterface. +From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. +From VerdiRaft Require Import LeaderLogsSortedInterface. +From VerdiRaft Require Import LeaderLogsLogMatchingInterface. +From VerdiRaft Require Import LogsLeaderLogsInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. @@ -230,6 +227,7 @@ Section StateMachineSafety'. concludes. intuition. Qed. + (* FIXME: move to StructTact *) Lemma Prefix_In : forall A (l : list A) l' x, Prefix l l' -> @@ -245,7 +243,8 @@ Section StateMachineSafety'. | H : refined_raft_intermediate_reachable _ |- _ => copy_apply i H end. - + + (* FIXME: move to StructTact *) Lemma in_not_nil : forall A (l : list A) x, In x l -> @@ -254,8 +253,6 @@ Section StateMachineSafety'. destruct l; simpl; intuition congruence. Qed. - Set Bullet Behavior "Strict Subproofs". - Theorem state_machine_safety_nw'_invariant : forall net, refined_raft_intermediate_reachable net -> diff --git a/raft-proofs/StateMachineSafetyProof.v b/raft-proofs/StateMachineSafetyProof.v index c27d2ff5..aadbe940 100644 --- a/raft-proofs/StateMachineSafetyProof.v +++ b/raft-proofs/StateMachineSafetyProof.v @@ -1,36 +1,28 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.CommitRecordedCommittedInterface. -Require Import VerdiRaft.StateMachineSafetyInterface. -Require Import VerdiRaft.StateMachineSafetyPrimeInterface. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.MaxIndexSanityInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.SortedInterface. -Require Import VerdiRaft.LogMatchingInterface. -Require Import VerdiRaft.PrevLogLeaderSublogInterface. -Require Import VerdiRaft.CurrentTermGtZeroInterface. -Require Import VerdiRaft.LastAppliedLeCommitIndexInterface. -Require Import VerdiRaft.MatchIndexAllEntriesInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsInterface. -Require Import VerdiRaft.LeaderSublogInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. -Require Import VerdiRaft.GhostLogCorrectInterface. -Require Import VerdiRaft.GhostLogsLogPropertiesInterface. -Require Import VerdiRaft.GhostLogLogMatchingInterface. -Require Import VerdiRaft.TransitiveCommitInterface. -Require Import VerdiRaft.TermSanityInterface. -Require Import VerdiRaft.LeadersHaveLeaderLogsStrongInterface. -Require Import VerdiRaft.OneLeaderLogPerTermInterface. - -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. - -Require Import VerdiRaft.RaftMsgRefinementInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import CommitRecordedCommittedInterface. +From VerdiRaft Require Import StateMachineSafetyInterface. +From VerdiRaft Require Import StateMachineSafetyPrimeInterface. +From VerdiRaft Require Import RaftRefinementInterface. +From VerdiRaft Require Import MaxIndexSanityInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import SortedInterface LogMatchingInterface. +From VerdiRaft Require Import PrevLogLeaderSublogInterface. +From VerdiRaft Require Import CurrentTermGtZeroInterface. +From VerdiRaft Require Import LastAppliedLeCommitIndexInterface. +From VerdiRaft Require Import MatchIndexAllEntriesInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. +From VerdiRaft Require Import LeaderSublogInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. +From VerdiRaft Require Import GhostLogCorrectInterface. +From VerdiRaft Require Import GhostLogsLogPropertiesInterface. +From VerdiRaft Require Import GhostLogLogMatchingInterface. +From VerdiRaft Require Import TransitiveCommitInterface TermSanityInterface. +From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. +From VerdiRaft Require Import OneLeaderLogPerTermInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import RaftMsgRefinementInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. diff --git a/raft-proofs/TermSanityProof.v b/raft-proofs/TermSanityProof.v index 33641246..a532b778 100644 --- a/raft-proofs/TermSanityProof.v +++ b/raft-proofs/TermSanityProof.v @@ -1,14 +1,11 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.TermSanityInterface. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import TermSanityInterface. Section TermSanityProof. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Theorem no_entries_past_current_term_nw_packets_unchanged : forall net ps' st', no_entries_past_current_term_nw net -> diff --git a/raft-proofs/TransitiveCommitProof.v b/raft-proofs/TransitiveCommitProof.v index 25e59676..4eb0879d 100644 --- a/raft-proofs/TransitiveCommitProof.v +++ b/raft-proofs/TransitiveCommitProof.v @@ -1,19 +1,14 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.RefinedLogMatchingLemmasInterface. - -Require Import VerdiRaft.TransitiveCommitInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. +From VerdiRaft Require Import TransitiveCommitInterface. Section TransitiveCommit. - 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 {rri : raft_refinement_interface}. Context {rlmli : refined_log_matching_lemmas_interface}. Theorem transitive_commit_invariant : diff --git a/raft-proofs/UniqueIndicesProof.v b/raft-proofs/UniqueIndicesProof.v index aa9d9e41..8d64dc67 100644 --- a/raft-proofs/UniqueIndicesProof.v +++ b/raft-proofs/UniqueIndicesProof.v @@ -1,10 +1,5 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.SortedInterface. - -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.UniqueIndicesInterface. +From VerdiRaft Require Import Raft SortedInterface. +From VerdiRaft Require Import CommonTheorems UniqueIndicesInterface. Section UniqueIndices. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotedForMoreUpToDateProof.v b/raft-proofs/VotedForMoreUpToDateProof.v index c7b2f9cd..38e19efd 100644 --- a/raft-proofs/VotedForMoreUpToDateProof.v +++ b/raft-proofs/VotedForMoreUpToDateProof.v @@ -1,15 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas CommonTheorems. +From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. +From VerdiRaft Require Import VotedForTermSanityInterface. +From VerdiRaft Require Import VotedForMoreUpToDateInterface. -Require Import VerdiRaft.RequestVoteMaxIndexMaxTermInterface. -Require Import VerdiRaft.VotedForTermSanityInterface. - -Require Import VerdiRaft.VotedForMoreUpToDateInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotedForMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotedForTermSanityProof.v b/raft-proofs/VotedForTermSanityProof.v index af73b8a2..98b32297 100644 --- a/raft-proofs/VotedForTermSanityProof.v +++ b/raft-proofs/VotedForTermSanityProof.v @@ -1,12 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import RequestVoteTermSanityInterface. +From VerdiRaft Require Import VotedForTermSanityInterface. -Require Import VerdiRaft.RequestVoteTermSanityInterface. -Require Import VerdiRaft.VotedForTermSanityInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotedForTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesCorrectProof.v b/raft-proofs/VotesCorrectProof.v index 10c32b59..e1004dd9 100644 --- a/raft-proofs/VotesCorrectProof.v +++ b/raft-proofs/VotesCorrectProof.v @@ -1,15 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import VotesLeCurrentTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.VotesLeCurrentTermInterface. - -Set Bullet Behavior "Strict Subproofs". - Section VotesCorrect. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/VotesLeCurrentTermProof.v b/raft-proofs/VotesLeCurrentTermProof.v index 8564e8ca..0ba7413b 100644 --- a/raft-proofs/VotesLeCurrentTermProof.v +++ b/raft-proofs/VotesLeCurrentTermProof.v @@ -1,14 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import VotesLeCurrentTermInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.VotesLeCurrentTermInterface. - -Set Bullet Behavior "Strict Subproofs". - Section VotesLeCurrentTerm. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/VotesReceivedMoreUpToDateProof.v b/raft-proofs/VotesReceivedMoreUpToDateProof.v index 1d673569..42511f8d 100644 --- a/raft-proofs/VotesReceivedMoreUpToDateProof.v +++ b/raft-proofs/VotesReceivedMoreUpToDateProof.v @@ -1,14 +1,9 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas CommonTheorems. +From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. +From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface. -Require Import VerdiRaft.RequestVoteReplyMoreUpToDateInterface. - -Require Import VerdiRaft.VotesReceivedMoreUpToDateInterface. +Local Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesReceivedMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesVotesWithLogCorrespondProof.v b/raft-proofs/VotesVotesWithLogCorrespondProof.v index eae90d76..099313ca 100644 --- a/raft-proofs/VotesVotesWithLogCorrespondProof.v +++ b/raft-proofs/VotesVotesWithLogCorrespondProof.v @@ -1,10 +1,8 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.VotesVotesWithLogCorrespondInterface. - Section VotesVotesWithLogCorrespond. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/VotesWithLogSortedProof.v b/raft-proofs/VotesWithLogSortedProof.v index d96972a6..07489abf 100644 --- a/raft-proofs/VotesWithLogSortedProof.v +++ b/raft-proofs/VotesWithLogSortedProof.v @@ -1,16 +1,11 @@ -Require Import Verdi.GhostSimulations. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. - -Require Import VerdiRaft.SpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions SpecLemmas. +From VerdiRaft Require Import VotesWithLogSortedInterface. +From VerdiRaft Require Import SortedInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.VotesWithLogSortedInterface. -Require Import VerdiRaft.SortedInterface. - Section VotesWithLogSorted. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft-proofs/VotesWithLogTermSanityProof.v b/raft-proofs/VotesWithLogTermSanityProof.v index 005a8521..987899eb 100644 --- a/raft-proofs/VotesWithLogTermSanityProof.v +++ b/raft-proofs/VotesWithLogTermSanityProof.v @@ -1,17 +1,15 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. +From VerdiRaft Require Import VotesWithLogTermSanityInterface. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Import VerdiRaft.VotesWithLogTermSanityInterface. - Section VotesWithLogTermSanity. 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}. Ltac start := diff --git a/raft/AllEntriesCandidateEntriesInterface.v b/raft/AllEntriesCandidateEntriesInterface.v index 14f421aa..e0e37839 100644 --- a/raft/AllEntriesCandidateEntriesInterface.v +++ b/raft/AllEntriesCandidateEntriesInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. Section CandidateEntriesInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/AllEntriesIndicesGt0Interface.v b/raft/AllEntriesIndicesGt0Interface.v index cf2a05d4..7e109760 100644 --- a/raft/AllEntriesIndicesGt0Interface.v +++ b/raft/AllEntriesIndicesGt0Interface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesIndicesGt0. Context {orig_base_params : BaseParams}. diff --git a/raft/AllEntriesLeaderLogsInterface.v b/raft/AllEntriesLeaderLogsInterface.v index 8ee4b754..be7b4e3c 100644 --- a/raft/AllEntriesLeaderLogsInterface.v +++ b/raft/AllEntriesLeaderLogsInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesLeaderLogs. diff --git a/raft/AllEntriesLeaderLogsTermInterface.v b/raft/AllEntriesLeaderLogsTermInterface.v index dbfb5e02..ff4206d4 100644 --- a/raft/AllEntriesLeaderLogsTermInterface.v +++ b/raft/AllEntriesLeaderLogsTermInterface.v @@ -1,12 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesLeaderLogsTerm. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Definition allEntries_leaderLogs_term (net : network) : Prop := forall t e h, In (t, e) (allEntries (fst (nwState net h))) -> @@ -22,5 +20,4 @@ Section AllEntriesLeaderLogsTerm. refined_raft_intermediate_reachable net -> allEntries_leaderLogs_term net }. - End AllEntriesLeaderLogsTerm. diff --git a/raft/AllEntriesLeaderSublogInterface.v b/raft/AllEntriesLeaderSublogInterface.v index e971ac49..f5941a52 100644 --- a/raft/AllEntriesLeaderSublogInterface.v +++ b/raft/AllEntriesLeaderSublogInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesLeaderSublogInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/AllEntriesLogInterface.v b/raft/AllEntriesLogInterface.v index 9f9ee765..b5afe93e 100644 --- a/raft/AllEntriesLogInterface.v +++ b/raft/AllEntriesLogInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesLog. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/AllEntriesLogMatchingInterface.v b/raft/AllEntriesLogMatchingInterface.v index e6157697..794d8394 100644 --- a/raft/AllEntriesLogMatchingInterface.v +++ b/raft/AllEntriesLogMatchingInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesLogMatching. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/AllEntriesTermSanityInterface.v b/raft/AllEntriesTermSanityInterface.v index 52d3a828..7c2c6c4f 100644 --- a/raft/AllEntriesTermSanityInterface.v +++ b/raft/AllEntriesTermSanityInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft/AllEntriesVotesWithLogInterface.v b/raft/AllEntriesVotesWithLogInterface.v index 36ec16ab..6c417f84 100644 --- a/raft/AllEntriesVotesWithLogInterface.v +++ b/raft/AllEntriesVotesWithLogInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AllEntriesVotesWithLog. diff --git a/raft/AppendEntriesLeaderInterface.v b/raft/AppendEntriesLeaderInterface.v index c73a4aa6..510e9a30 100644 --- a/raft/AppendEntriesLeaderInterface.v +++ b/raft/AppendEntriesLeaderInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AppendEntriesLeader. Context {orig_base_params : BaseParams}. diff --git a/raft/AppendEntriesReplySublogInterface.v b/raft/AppendEntriesReplySublogInterface.v index 12de553c..ac0593fd 100644 --- a/raft/AppendEntriesReplySublogInterface.v +++ b/raft/AppendEntriesReplySublogInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section AppendEntriesReplySublog. Context {orig_base_params : BaseParams}. diff --git a/raft/AppendEntriesRequestLeaderLogsInterface.v b/raft/AppendEntriesRequestLeaderLogsInterface.v index ea0e23c5..f3e0235e 100644 --- a/raft/AppendEntriesRequestLeaderLogsInterface.v +++ b/raft/AppendEntriesRequestLeaderLogsInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AppendEntriesRequestLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft/AppendEntriesRequestReplyCorrespondenceInterface.v b/raft/AppendEntriesRequestReplyCorrespondenceInterface.v index 2bef581f..8288acbc 100644 --- a/raft/AppendEntriesRequestReplyCorrespondenceInterface.v +++ b/raft/AppendEntriesRequestReplyCorrespondenceInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. - +From VerdiRaft Require Import Raft. Section AppendEntriesRequestReplyCorrespondence. Context {orig_base_params : BaseParams}. @@ -26,6 +25,4 @@ Section AppendEntriesRequestReplyCorrespondence. raft_intermediate_reachable net -> append_entries_request_reply_correspondence net }. - - End AppendEntriesRequestReplyCorrespondence. diff --git a/raft/AppendEntriesRequestTermSanityInterface.v b/raft/AppendEntriesRequestTermSanityInterface.v index a4ef2f07..9960d219 100644 --- a/raft/AppendEntriesRequestTermSanityInterface.v +++ b/raft/AppendEntriesRequestTermSanityInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AppendEntriesRequestTermSanity. Context {orig_base_params : BaseParams}. @@ -21,5 +20,4 @@ Section AppendEntriesRequestTermSanity. refined_raft_intermediate_reachable net -> append_entries_request_term_sanity net }. - End AppendEntriesRequestTermSanity. diff --git a/raft/AppliedEntriesMonotonicInterface.v b/raft/AppliedEntriesMonotonicInterface.v index 654c63be..060b057b 100644 --- a/raft/AppliedEntriesMonotonicInterface.v +++ b/raft/AppliedEntriesMonotonicInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section AppliedEntriesMonotonicInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/AppliedImpliesInputInterface.v b/raft/AppliedImpliesInputInterface.v index 129b68c7..03288f9a 100644 --- a/raft/AppliedImpliesInputInterface.v +++ b/raft/AppliedImpliesInputInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft CommonDefinitions TraceUtil. Section AppliedImpliesInputInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/CandidateEntriesInterface.v b/raft/CandidateEntriesInterface.v index 6bd21535..da81a735 100644 --- a/raft/CandidateEntriesInterface.v +++ b/raft/CandidateEntriesInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. Section CandidateEntriesInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/CandidateTermGtLogInterface.v b/raft/CandidateTermGtLogInterface.v index 8a0ba22f..4347286b 100644 --- a/raft/CandidateTermGtLogInterface.v +++ b/raft/CandidateTermGtLogInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section CandidateTermGtLogInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/CandidatesVoteForSelvesInterface.v b/raft/CandidatesVoteForSelvesInterface.v index 70f818e0..9d409b75 100644 --- a/raft/CandidatesVoteForSelvesInterface.v +++ b/raft/CandidatesVoteForSelvesInterface.v @@ -1,11 +1,10 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section CandidatesVoteForSelvesInterface. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Definition candidates_vote_for_selves net := forall h, type (nwState net h) = Candidate -> diff --git a/raft/CausalOrderPreservedInterface.v b/raft/CausalOrderPreservedInterface.v index 5238dc7d..300e5255 100644 --- a/raft/CausalOrderPreservedInterface.v +++ b/raft/CausalOrderPreservedInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft CommonDefinitions TraceUtil. Section CausalOrderPreserved. Context {orig_base_params : BaseParams}. @@ -8,6 +6,7 @@ Section CausalOrderPreserved. Context {raft_params : RaftParams orig_base_params}. Section inner. + Variable client : clientId. Variable id : nat. Variable client' : clientId. @@ -18,6 +17,7 @@ Section CausalOrderPreserved. Definition entries_ordered net := before_func (has_key client id) (has_key client' id') (applied_entries (nwState net)). + End inner. Class causal_order_preserved_interface : Prop := diff --git a/raft/CommitRecordedCommittedInterface.v b/raft/CommitRecordedCommittedInterface.v index 816c4c5b..6981c27d 100644 --- a/raft/CommitRecordedCommittedInterface.v +++ b/raft/CommitRecordedCommittedInterface.v @@ -1,11 +1,9 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. -Require Import VerdiRaft.CommonDefinitions. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. +From VerdiRaft Require Import CommonDefinitions. Section CommitRecordedCommitted. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -22,5 +20,4 @@ Section CommitRecordedCommitted. refined_raft_intermediate_reachable net -> commit_recorded_committed net }. - End CommitRecordedCommitted. diff --git a/raft/CommonDefinitions.v b/raft/CommonDefinitions.v index c5c6d105..91e40fbe 100644 --- a/raft/CommonDefinitions.v +++ b/raft/CommonDefinitions.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section CommonDefinitions. Context {orig_base_params : BaseParams}. @@ -125,5 +125,4 @@ Section CommonDefinitions. forall e, In e l -> eTerm e >= 1 /\ eIndex e >= 1. - End CommonDefinitions. diff --git a/raft/CommonTheorems.v b/raft/CommonTheorems.v index 3558ed09..6c408254 100644 --- a/raft/CommonTheorems.v +++ b/raft/CommonTheorems.v @@ -1,14 +1,9 @@ -Require Import PeanoNat. - -Require Import VerdiRaft.RaftState. -Require Import VerdiRaft.Raft. +From Coq Require Import PeanoNat FunInd. +From VerdiRaft Require Import RaftState Raft. +From VerdiRaft Require Export CommonDefinitions. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. -Require Export VerdiRaft.CommonDefinitions. - -Require Import FunInd. - Section CommonTheorems. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. diff --git a/raft/CroniesCorrectInterface.v b/raft/CroniesCorrectInterface.v index 740e5e70..49107646 100644 --- a/raft/CroniesCorrectInterface.v +++ b/raft/CroniesCorrectInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section CroniesCorrectInterface. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/CroniesTermInterface.v b/raft/CroniesTermInterface.v index 64e11ce5..7eb574c3 100644 --- a/raft/CroniesTermInterface.v +++ b/raft/CroniesTermInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section CroniesTermInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/CurrentTermGtZeroInterface.v b/raft/CurrentTermGtZeroInterface.v index 31ff5c49..5f46b0e2 100644 --- a/raft/CurrentTermGtZeroInterface.v +++ b/raft/CurrentTermGtZeroInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section CurrentTermGtZeroInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/DecompositionWithPostState.v b/raft/DecompositionWithPostState.v index 2a3324d9..59f8d559 100644 --- a/raft/DecompositionWithPostState.v +++ b/raft/DecompositionWithPostState.v @@ -1,9 +1,7 @@ -Require Import FunctionalExtensionality. - -Require Import VerdiRaft.Raft. +From Coq Require Import FunctionalExtensionality. +From VerdiRaft Require Import Raft. Section DecompositionWithPostState. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -335,5 +333,4 @@ Section DecompositionWithPostState. - eapply_prop raft_net_invariant_do_leader'; eauto using RIR_doLeader. - eapply_prop raft_net_invariant_do_generic_server'; eauto using RIR_doGenericServer. Qed. - End DecompositionWithPostState. diff --git a/raft/EveryEntryWasCreatedHostLogInterface.v b/raft/EveryEntryWasCreatedHostLogInterface.v index 80dd3f37..57ce32c9 100644 --- a/raft/EveryEntryWasCreatedHostLogInterface.v +++ b/raft/EveryEntryWasCreatedHostLogInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. Section EveryEntryWasCreatedHostLogInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/EveryEntryWasCreatedInterface.v b/raft/EveryEntryWasCreatedInterface.v index 7a6fe7d6..ff4c7219 100644 --- a/raft/EveryEntryWasCreatedInterface.v +++ b/raft/EveryEntryWasCreatedInterface.v @@ -1,7 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions RefinementCommonDefinitions. Section EveryEntryWasCreated. Context {orig_base_params : BaseParams}. diff --git a/raft/GhostLogAllEntriesInterface.v b/raft/GhostLogAllEntriesInterface.v index 7988948b..118fd79c 100644 --- a/raft/GhostLogAllEntriesInterface.v +++ b/raft/GhostLogAllEntriesInterface.v @@ -1,7 +1,5 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RaftMsgRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RaftMsgRefinementInterface. Section GhostLogAllEntriesInterface. Context {orig_base_params : BaseParams}. @@ -15,13 +13,11 @@ Section GhostLogAllEntriesInterface. exists t, In (t, e) (allEntries (fst (nwState net (pSrc p)))). - Class ghost_log_allEntries_interface : Prop := { ghost_log_allEntries_invariant : forall net, msg_refined_raft_intermediate_reachable net -> ghost_log_allEntries net - }. - + }. End GhostLogAllEntriesInterface. diff --git a/raft/GhostLogCorrectInterface.v b/raft/GhostLogCorrectInterface.v index 258b330f..026a9597 100644 --- a/raft/GhostLogCorrectInterface.v +++ b/raft/GhostLogCorrectInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.RaftMsgRefinementInterface. +From VerdiRaft Require Import Raft RaftMsgRefinementInterface. Section GhostLogCorrectInterface. Context {orig_base_params : BaseParams}. @@ -20,13 +18,11 @@ Section GhostLogCorrectInterface. In e l) /\ entries = findGtIndex l prevLogIndex. - Class ghost_log_correct_interface : Prop := { ghost_log_correct_invariant : forall net, msg_refined_raft_intermediate_reachable net -> ghost_log_correct net - }. - + }. End GhostLogCorrectInterface. diff --git a/raft/GhostLogLogMatchingInterface.v b/raft/GhostLogLogMatchingInterface.v index 84cc783e..469cab3b 100644 --- a/raft/GhostLogLogMatchingInterface.v +++ b/raft/GhostLogLogMatchingInterface.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftMsgRefinementInterface. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftMsgRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section GhostLogLogMatching. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -21,5 +18,4 @@ Section GhostLogLogMatching. msg_refined_raft_intermediate_reachable net -> ghost_log_entries_match_host net }. - End GhostLogLogMatching. diff --git a/raft/GhostLogsLogPropertiesInterface.v b/raft/GhostLogsLogPropertiesInterface.v index 16375639..2f75a51c 100644 --- a/raft/GhostLogsLogPropertiesInterface.v +++ b/raft/GhostLogsLogPropertiesInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftMsgRefinementInterface. +From VerdiRaft Require Import Raft RaftMsgRefinementInterface. Section GhostLogsLogProperties. Context {orig_base_params : BaseParams}. @@ -24,5 +23,4 @@ Section GhostLogsLogProperties. msg_refined_raft_intermediate_reachable net -> log_properties_hold_on_ghost_logs net }. - End GhostLogsLogProperties. diff --git a/raft/InLogInAllEntriesInterface.v b/raft/InLogInAllEntriesInterface.v index 71d2d972..7043266c 100644 --- a/raft/InLogInAllEntriesInterface.v +++ b/raft/InLogInAllEntriesInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section InLogInAllEntries. diff --git a/raft/InputBeforeOutputInterface.v b/raft/InputBeforeOutputInterface.v index 3a40a392..007b31f3 100644 --- a/raft/InputBeforeOutputInterface.v +++ b/raft/InputBeforeOutputInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft TraceUtil. Section InputBeforeOutputInterface. Context {orig_base_params : BaseParams}. @@ -7,6 +6,7 @@ Section InputBeforeOutputInterface. Context {raft_params : RaftParams orig_base_params}. Section inner. + Variable client : clientId. Variables id : nat. diff --git a/raft/LastAppliedCommitIndexMatchingInterface.v b/raft/LastAppliedCommitIndexMatchingInterface.v index b077e21b..b9f6711b 100644 --- a/raft/LastAppliedCommitIndexMatchingInterface.v +++ b/raft/LastAppliedCommitIndexMatchingInterface.v @@ -1,7 +1,6 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section LastAppliedCommitIndexMatching. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -39,5 +38,4 @@ Section LastAppliedCommitIndexMatching. raft_intermediate_reachable net -> lastApplied_lastApplied_match net }. - End LastAppliedCommitIndexMatching. diff --git a/raft/LastAppliedLeCommitIndexInterface.v b/raft/LastAppliedLeCommitIndexInterface.v index 8df56a23..0817a757 100644 --- a/raft/LastAppliedLeCommitIndexInterface.v +++ b/raft/LastAppliedLeCommitIndexInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section LastAppliedLeCommitIndexInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderCompletenessInterface.v b/raft/LeaderCompletenessInterface.v index 9f606aa1..82d376cf 100644 --- a/raft/LeaderCompletenessInterface.v +++ b/raft/LeaderCompletenessInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderCompleteness. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -48,5 +46,4 @@ Section LeaderCompleteness. refined_raft_intermediate_reachable net -> leader_completeness net }. - End LeaderCompleteness. diff --git a/raft/LeaderLogsCandidateEntriesInterface.v b/raft/LeaderLogsCandidateEntriesInterface.v index 893285c7..8a063bb2 100644 --- a/raft/LeaderLogsCandidateEntriesInterface.v +++ b/raft/LeaderLogsCandidateEntriesInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. Section CandidateEntriesInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderLogsContiguousInterface.v b/raft/LeaderLogsContiguousInterface.v index 3e108b81..4c937517 100644 --- a/raft/LeaderLogsContiguousInterface.v +++ b/raft/LeaderLogsContiguousInterface.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems. Section LeaderLogsContiguous. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/LeaderLogsLogMatchingInterface.v b/raft/LeaderLogsLogMatchingInterface.v index b811b898..3782473f 100644 --- a/raft/LeaderLogsLogMatchingInterface.v +++ b/raft/LeaderLogsLogMatchingInterface.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section LeaderLogsLogMatching. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/LeaderLogsLogPropertiesInterface.v b/raft/LeaderLogsLogPropertiesInterface.v index 5544e566..7c08bb95 100644 --- a/raft/LeaderLogsLogPropertiesInterface.v +++ b/raft/LeaderLogsLogPropertiesInterface.v @@ -1,23 +1,21 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderLogsLogProperties. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - + Definition log_property (P : list entry -> Prop) := forall net h, refined_raft_intermediate_reachable net -> P (log (snd (nwState net h))). - + Definition log_properties_hold_on_leader_logs net := forall P h t ll, log_property P -> In (t, ll) (leaderLogs (fst (nwState net h))) -> P ll. - Class log_properties_hold_on_leader_logs_interface : Prop := { log_properties_hold_on_leader_logs_invariant : @@ -25,5 +23,4 @@ Section LeaderLogsLogProperties. refined_raft_intermediate_reachable net -> log_properties_hold_on_leader_logs net }. - End LeaderLogsLogProperties. diff --git a/raft/LeaderLogsPreservedInterface.v b/raft/LeaderLogsPreservedInterface.v index b8067c39..81af1d70 100644 --- a/raft/LeaderLogsPreservedInterface.v +++ b/raft/LeaderLogsPreservedInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderLogsPreserved. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderLogsSortedInterface.v b/raft/LeaderLogsSortedInterface.v index 407a58df..979f77df 100644 --- a/raft/LeaderLogsSortedInterface.v +++ b/raft/LeaderLogsSortedInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section LeaderLogsSorted. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderLogsSublogInterface.v b/raft/LeaderLogsSublogInterface.v index 70abe73f..414d1eaf 100644 --- a/raft/LeaderLogsSublogInterface.v +++ b/raft/LeaderLogsSublogInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderLogsSublogInterface. Context {orig_base_params : BaseParams}. @@ -21,5 +20,4 @@ Section LeaderLogsSublogInterface. refined_raft_intermediate_reachable net -> leaderLogs_sublog net }. - End LeaderLogsSublogInterface. diff --git a/raft/LeaderLogsTermSanityInterface.v b/raft/LeaderLogsTermSanityInterface.v index 2ef2adf4..6dd94225 100644 --- a/raft/LeaderLogsTermSanityInterface.v +++ b/raft/LeaderLogsTermSanityInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderLogsTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderLogsVotesWithLogInterface.v b/raft/LeaderLogsVotesWithLogInterface.v index 9d1d49c3..399ec7d3 100644 --- a/raft/LeaderLogsVotesWithLogInterface.v +++ b/raft/LeaderLogsVotesWithLogInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeaderLogsVotesWithLog. Context {orig_base_params : BaseParams}. diff --git a/raft/LeaderSublogInterface.v b/raft/LeaderSublogInterface.v index c594a7f6..66a17751 100644 --- a/raft/LeaderSublogInterface.v +++ b/raft/LeaderSublogInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section LeaderSublogInterface. Context {orig_base_params : BaseParams}. @@ -33,5 +33,4 @@ Section LeaderSublogInterface. raft_intermediate_reachable net -> leader_sublog_invariant net }. - End LeaderSublogInterface. diff --git a/raft/LeadersHaveLeaderLogsInterface.v b/raft/LeadersHaveLeaderLogsInterface.v index 7d49cc9b..3a9cb3db 100644 --- a/raft/LeadersHaveLeaderLogsInterface.v +++ b/raft/LeadersHaveLeaderLogsInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeadersHaveLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft/LeadersHaveLeaderLogsStrongInterface.v b/raft/LeadersHaveLeaderLogsStrongInterface.v index a357b2e5..1b1b9c3b 100644 --- a/raft/LeadersHaveLeaderLogsStrongInterface.v +++ b/raft/LeadersHaveLeaderLogsStrongInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LeadersHaveLeaderLogsStrong. Context {orig_base_params : BaseParams}. diff --git a/raft/Linearizability.v b/raft/Linearizability.v index a530ee09..55f8c7a7 100644 --- a/raft/Linearizability.v +++ b/raft/Linearizability.v @@ -1,4 +1,4 @@ -Require Import Verdi.Verdi. +From Verdi Require Import Verdi. Section Linearizability. Variable K : Type. @@ -1426,6 +1426,7 @@ Section Linearizability. Qed. End Linearizability. + Arguments I {_} _. Arguments O {_} _. diff --git a/raft/LogAllEntriesInterface.v b/raft/LogAllEntriesInterface.v index d0bc1c1d..3b4b4d4d 100644 --- a/raft/LogAllEntriesInterface.v +++ b/raft/LogAllEntriesInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LogAllEntries. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/LogMatchingInterface.v b/raft/LogMatchingInterface.v index c8470d72..8670fd82 100644 --- a/raft/LogMatchingInterface.v +++ b/raft/LogMatchingInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section LogMatchingInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/LogsLeaderLogsInterface.v b/raft/LogsLeaderLogsInterface.v index b83a7141..a29951c0 100644 --- a/raft/LogsLeaderLogsInterface.v +++ b/raft/LogsLeaderLogsInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section LogsLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft/MatchIndexAllEntriesInterface.v b/raft/MatchIndexAllEntriesInterface.v index d43c4036..2f027bd8 100644 --- a/raft/MatchIndexAllEntriesInterface.v +++ b/raft/MatchIndexAllEntriesInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section MatchIndexAllEntries. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -21,6 +19,5 @@ Section MatchIndexAllEntries. forall net, refined_raft_intermediate_reachable net -> match_index_all_entries net - }. - + }. End MatchIndexAllEntries. diff --git a/raft/MatchIndexLeaderInterface.v b/raft/MatchIndexLeaderInterface.v index 33bb9619..f948101f 100644 --- a/raft/MatchIndexLeaderInterface.v +++ b/raft/MatchIndexLeaderInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section MatchIndexLeader. Context {orig_base_params : BaseParams}. diff --git a/raft/MatchIndexSanityInterface.v b/raft/MatchIndexSanityInterface.v index 83b085c6..97dad9ac 100644 --- a/raft/MatchIndexSanityInterface.v +++ b/raft/MatchIndexSanityInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section MatchIndexSanity. Context {orig_base_params : BaseParams}. @@ -17,6 +17,5 @@ Section MatchIndexSanity. forall net, raft_intermediate_reachable net -> match_index_sanity net - }. - + }. End MatchIndexSanity. diff --git a/raft/MaxIndexSanityInterface.v b/raft/MaxIndexSanityInterface.v index 3857980f..2b1b3e76 100644 --- a/raft/MaxIndexSanityInterface.v +++ b/raft/MaxIndexSanityInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section MaxIndexSanity. Context {orig_base_params : BaseParams}. diff --git a/raft/NextIndexSafetyInterface.v b/raft/NextIndexSafetyInterface.v index a411bfff..70928ec4 100644 --- a/raft/NextIndexSafetyInterface.v +++ b/raft/NextIndexSafetyInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section NextIndexSafety. Context {orig_base_params : BaseParams}. diff --git a/raft/NoAppendEntriesRepliesToSelfInterface.v b/raft/NoAppendEntriesRepliesToSelfInterface.v index 747b3153..85001640 100644 --- a/raft/NoAppendEntriesRepliesToSelfInterface.v +++ b/raft/NoAppendEntriesRepliesToSelfInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section NoAppendEntriesRepliesToSelfInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/NoAppendEntriesToLeaderInterface.v b/raft/NoAppendEntriesToLeaderInterface.v index ac39d19d..408acebf 100644 --- a/raft/NoAppendEntriesToLeaderInterface.v +++ b/raft/NoAppendEntriesToLeaderInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section NoAppendEntriesToLeaderInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/NoAppendEntriesToSelfInterface.v b/raft/NoAppendEntriesToSelfInterface.v index 8f9793c7..1d391a5f 100644 --- a/raft/NoAppendEntriesToSelfInterface.v +++ b/raft/NoAppendEntriesToSelfInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section NoAppendEntriesToSelfInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/OneLeaderLogPerTermInterface.v b/raft/OneLeaderLogPerTermInterface.v index 63f733fd..53eec60d 100644 --- a/raft/OneLeaderLogPerTermInterface.v +++ b/raft/OneLeaderLogPerTermInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section OneLeaderLogPerTerm. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/OneLeaderPerTermInterface.v b/raft/OneLeaderPerTermInterface.v index 7a4b773e..70ca9174 100644 --- a/raft/OneLeaderPerTermInterface.v +++ b/raft/OneLeaderPerTermInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section OneLeaderPerTermInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/OutputCorrectInterface.v b/raft/OutputCorrectInterface.v index df1b19f4..361be22e 100644 --- a/raft/OutputCorrectInterface.v +++ b/raft/OutputCorrectInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft CommonDefinitions TraceUtil. Section OutputCorrect. Context {orig_base_params : BaseParams}. diff --git a/raft/OutputGreatestIdInterface.v b/raft/OutputGreatestIdInterface.v index 7aef2a7b..5530dcaf 100644 --- a/raft/OutputGreatestIdInterface.v +++ b/raft/OutputGreatestIdInterface.v @@ -1,19 +1,15 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft CommonDefinitions TraceUtil. Section OutputGreatestId. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Section inner. Variable client : clientId. Variable id : nat. - Definition greatest_id_for_client (net : network) : Prop := forall id', id < id' -> diff --git a/raft/OutputImpliesAppliedInterface.v b/raft/OutputImpliesAppliedInterface.v index a6a03459..59267170 100644 --- a/raft/OutputImpliesAppliedInterface.v +++ b/raft/OutputImpliesAppliedInterface.v @@ -1,19 +1,15 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.TraceUtil. +From VerdiRaft Require Import Raft CommonDefinitions TraceUtil. Section OutputImpliesApplied. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Section inner. Variable client : clientId. Variable id : nat. - Definition in_applied_entries (net : network) : Prop := exists e, eClient e = client /\ diff --git a/raft/PrefixWithinTermInterface.v b/raft/PrefixWithinTermInterface.v index 2f20d754..fe2d7280 100644 --- a/raft/PrefixWithinTermInterface.v +++ b/raft/PrefixWithinTermInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section PrefixWithinTerm. Context {orig_base_params : BaseParams}. diff --git a/raft/PrevLogCandidateEntriesTermInterface.v b/raft/PrevLogCandidateEntriesTermInterface.v index 27c5e974..51cc2d77 100644 --- a/raft/PrevLogCandidateEntriesTermInterface.v +++ b/raft/PrevLogCandidateEntriesTermInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.RefinementCommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import RefinementCommonDefinitions. Section PrevLogCandidateEntriesTermInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/PrevLogLeaderSublogInterface.v b/raft/PrevLogLeaderSublogInterface.v index 4bb1cd2a..df4cea87 100644 --- a/raft/PrevLogLeaderSublogInterface.v +++ b/raft/PrevLogLeaderSublogInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section PrevLogLeaderSublogInterface. Context {orig_base_params : BaseParams}. @@ -24,5 +24,4 @@ Section PrevLogLeaderSublogInterface. raft_intermediate_reachable net -> prevLog_leader_sublog net }. - End PrevLogLeaderSublogInterface. diff --git a/raft/Raft.v b/raft/Raft.v index 842b6764..422f9a09 100644 --- a/raft/Raft.v +++ b/raft/Raft.v @@ -1,6 +1,6 @@ -Require Export Verdi.Verdi. -Require Import VerdiRaft.RaftState. -Require Export StructTact.Fin. +From Verdi Require Export Verdi. +From VerdiRaft Require Import RaftState. +From StructTact Require Export Fin. Open Scope bool. diff --git a/raft/RaftLinearizableProofs.v b/raft/RaftLinearizableProofs.v index 6eca2a47..2443e714 100644 --- a/raft/RaftLinearizableProofs.v +++ b/raft/RaftLinearizableProofs.v @@ -1,15 +1,10 @@ -Require Import Sumbool. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.TraceUtil. -Require Import VerdiRaft.Linearizability. -Require Import VerdiRaft.OutputImpliesAppliedInterface. -Require Import VerdiRaft.AppliedImpliesInputInterface. -Require Import VerdiRaft.CausalOrderPreservedInterface. -Require Import VerdiRaft.OutputCorrectInterface. -Require Import VerdiRaft.InputBeforeOutputInterface. -Require Import VerdiRaft.OutputGreatestIdInterface. +From Coq Require Import Sumbool. +From VerdiRaft Require Import Raft CommonTheorems TraceUtil. +From VerdiRaft Require Import Linearizability OutputImpliesAppliedInterface. +From VerdiRaft Require Import AppliedImpliesInputInterface. +From VerdiRaft Require Import CausalOrderPreservedInterface. +From VerdiRaft Require Import OutputCorrectInterface InputBeforeOutputInterface. +From VerdiRaft Require Import OutputGreatestIdInterface. Section RaftLinearizableProofs. Context {orig_base_params : BaseParams}. diff --git a/raft/RaftMsgRefinementInterface.v b/raft/RaftMsgRefinementInterface.v index 76e472d7..8f92cf8f 100644 --- a/raft/RaftMsgRefinementInterface.v +++ b/raft/RaftMsgRefinementInterface.v @@ -1,7 +1,5 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.RaftRefinementInterface. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section RaftMsgRefinementInterface. Context {orig_base_params : BaseParams}. @@ -467,9 +465,6 @@ Section RaftMsgRefinementInterface. End RaftMsgRefinementInterface. -#[global] -Hint Extern 3 (@BaseParams) => apply raft_msg_refined_base_params : typeclass_instances. -#[global] -Hint Extern 3 (@MultiParams _) => apply raft_msg_refined_multi_params : typeclass_instances. -#[global] -Hint Extern 3 (@FailureParams _ _) => apply raft_msg_refined_failure_params : typeclass_instances. +#[global] Hint Extern 3 (@BaseParams) => apply raft_msg_refined_base_params : typeclass_instances. +#[global] Hint Extern 3 (@MultiParams _) => apply raft_msg_refined_multi_params : typeclass_instances. +#[global] Hint Extern 3 (@FailureParams _ _) => apply raft_msg_refined_failure_params : typeclass_instances. diff --git a/raft/RaftRefinementInterface.v b/raft/RaftRefinementInterface.v index 65d9e8f9..3617d10d 100644 --- a/raft/RaftRefinementInterface.v +++ b/raft/RaftRefinementInterface.v @@ -1,5 +1,5 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft. Section RaftRefinementInterface. Context {orig_base_params : BaseParams}. @@ -567,12 +567,8 @@ Section RaftRefinementInterface. refined_raft_intermediate_reachable net -> raft_intermediate_reachable (deghost net) }. - End RaftRefinementInterface. -#[global] -Hint Extern 4 (@BaseParams) => apply raft_refined_base_params : typeclass_instances. -#[global] -Hint Extern 4 (@MultiParams _) => apply raft_refined_multi_params : typeclass_instances. -#[global] -Hint Extern 4 (@FailureParams _ _) => apply raft_refined_failure_params : typeclass_instances. +#[global] Hint Extern 4 (@BaseParams) => apply raft_refined_base_params : typeclass_instances. +#[global] Hint Extern 4 (@MultiParams _) => apply raft_refined_multi_params : typeclass_instances. +#[global] Hint Extern 4 (@FailureParams _ _) => apply raft_refined_failure_params : typeclass_instances. diff --git a/raft/RefinedLogMatchingLemmasInterface.v b/raft/RefinedLogMatchingLemmasInterface.v index cb631b59..f18da8a7 100644 --- a/raft/RefinedLogMatchingLemmasInterface.v +++ b/raft/RefinedLogMatchingLemmasInterface.v @@ -1,7 +1,5 @@ -Require Import VerdiRaft.CommonTheorems. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import CommonTheorems Raft. +From VerdiRaft Require Import RaftRefinementInterface. Section RefinedLogMatchingLemmas. Context {orig_base_params : BaseParams}. diff --git a/raft/RefinementCommonDefinitions.v b/raft/RefinementCommonDefinitions.v index c0dc2915..d2ab0108 100644 --- a/raft/RefinementCommonDefinitions.v +++ b/raft/RefinementCommonDefinitions.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section CommonDefinitions. Context {orig_base_params : BaseParams}. diff --git a/raft/RefinementCommonTheorems.v b/raft/RefinementCommonTheorems.v index d38a4bcf..c49f48b6 100644 --- a/raft/RefinementCommonTheorems.v +++ b/raft/RefinementCommonTheorems.v @@ -1,14 +1,10 @@ -Require Import Verdi.GhostSimulations. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. - -Require Import VerdiRaft.VotesCorrectInterface. -Require Import VerdiRaft.CroniesCorrectInterface. - -Require Import VerdiRaft.CommonTheorems. -Require Export VerdiRaft.RefinementCommonDefinitions. - -Require Import VerdiRaft.SpecLemmas. +From Verdi Require Import GhostSimulations. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import VotesCorrectInterface. +From VerdiRaft Require Import CroniesCorrectInterface. +From VerdiRaft Require Import CommonTheorems. +From VerdiRaft Require Export RefinementCommonDefinitions. +From VerdiRaft Require Import SpecLemmas. Local Arguments update {_} {_} _ _ _ _ _ : simpl never. diff --git a/raft/RefinementSpecLemmas.v b/raft/RefinementSpecLemmas.v index 444cf7ac..62c973b0 100644 --- a/raft/RefinementSpecLemmas.v +++ b/raft/RefinementSpecLemmas.v @@ -1,10 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft CommonTheorems. +From VerdiRaft Require Import RaftRefinementInterface SpecLemmas. Section SpecLemmas. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -658,5 +655,4 @@ Section SpecLemmas. find_inversion; auto; do_bool; intuition; try congruence. do_bool. subst. intuition. Qed. - End SpecLemmas. diff --git a/raft/RequestVoteMaxIndexMaxTermInterface.v b/raft/RequestVoteMaxIndexMaxTermInterface.v index 33bcb382..56beb5fc 100644 --- a/raft/RequestVoteMaxIndexMaxTermInterface.v +++ b/raft/RequestVoteMaxIndexMaxTermInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section RequestVoteMaxIndexMaxTerm. Context {orig_base_params : BaseParams}. diff --git a/raft/RequestVoteReplyMoreUpToDateInterface.v b/raft/RequestVoteReplyMoreUpToDateInterface.v index d4420da5..b5149707 100644 --- a/raft/RequestVoteReplyMoreUpToDateInterface.v +++ b/raft/RequestVoteReplyMoreUpToDateInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section RequestVoteReplyMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft/RequestVoteReplyTermSanityInterface.v b/raft/RequestVoteReplyTermSanityInterface.v index 40404dd7..ea4ec8be 100644 --- a/raft/RequestVoteReplyTermSanityInterface.v +++ b/raft/RequestVoteReplyTermSanityInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section RequestVoteReplyTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft/RequestVoteTermSanityInterface.v b/raft/RequestVoteTermSanityInterface.v index 35773545..9a356634 100644 --- a/raft/RequestVoteTermSanityInterface.v +++ b/raft/RequestVoteTermSanityInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section RequestVoteTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft/SortedInterface.v b/raft/SortedInterface.v index 995601ed..1a7c76a6 100644 --- a/raft/SortedInterface.v +++ b/raft/SortedInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section SortedInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/SpecLemmas.v b/raft/SpecLemmas.v index ed5b3c60..927c2d34 100644 --- a/raft/SpecLemmas.v +++ b/raft/SpecLemmas.v @@ -1,9 +1,6 @@ -Require Import VerdiRaft.RaftState. -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. +From VerdiRaft Require Import RaftState Raft CommonTheorems. Section SpecLemmas. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -1326,6 +1323,5 @@ Section SpecLemmas. intros. repeat break_match; find_inversion; simpl in *; auto; try congruence; do_bool; try lia; eauto using Nat.le_antisymm. - Qed. - + Qed. End SpecLemmas. diff --git a/raft/StateMachineCorrectInterface.v b/raft/StateMachineCorrectInterface.v index 66fd8cee..2d229bad 100644 --- a/raft/StateMachineCorrectInterface.v +++ b/raft/StateMachineCorrectInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section StateMachineCorrect. Context {orig_base_params : BaseParams}. diff --git a/raft/StateMachineSafetyInterface.v b/raft/StateMachineSafetyInterface.v index 50d9584f..d2c2946d 100644 --- a/raft/StateMachineSafetyInterface.v +++ b/raft/StateMachineSafetyInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.CommonDefinitions. - -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import CommonDefinitions Raft. Section StateMachineSafety. Context {orig_base_params : BaseParams}. @@ -36,5 +34,4 @@ Section StateMachineSafety. raft_intermediate_reachable net -> state_machine_safety net }. - End StateMachineSafety. diff --git a/raft/StateMachineSafetyPrimeInterface.v b/raft/StateMachineSafetyPrimeInterface.v index 1d9476e0..8f5ebf84 100644 --- a/raft/StateMachineSafetyPrimeInterface.v +++ b/raft/StateMachineSafetyPrimeInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. Section StateMachineSafety'. Context {orig_base_params : BaseParams}. @@ -36,5 +35,4 @@ Section StateMachineSafety'. refined_raft_intermediate_reachable net -> state_machine_safety' net }. - End StateMachineSafety'. diff --git a/raft/StateTraceInvariant.v b/raft/StateTraceInvariant.v index 31a2d134..0fe70711 100644 --- a/raft/StateTraceInvariant.v +++ b/raft/StateTraceInvariant.v @@ -1,6 +1,5 @@ -Require Import FunctionalExtensionality. - -Require Import Verdi.Verdi. +From Coq Require Import FunctionalExtensionality. +From Verdi Require Import Verdi. Section ST. Context {B : BaseParams}. diff --git a/raft/TermSanityInterface.v b/raft/TermSanityInterface.v index dd4b3ac0..c2311556 100644 --- a/raft/TermSanityInterface.v +++ b/raft/TermSanityInterface.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section TermSanityInterface. Context {orig_base_params : BaseParams}. diff --git a/raft/TraceUtil.v b/raft/TraceUtil.v index 375d8ca3..5b97e3e7 100644 --- a/raft/TraceUtil.v +++ b/raft/TraceUtil.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.Raft. +From VerdiRaft Require Import Raft. Section TraceUtil. Context {orig_base_params : BaseParams}. diff --git a/raft/TransitiveCommitInterface.v b/raft/TransitiveCommitInterface.v index 278ebc7a..1ab41ebe 100644 --- a/raft/TransitiveCommitInterface.v +++ b/raft/TransitiveCommitInterface.v @@ -1,9 +1,7 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.LeaderCompletenessInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import LeaderCompletenessInterface. Section TransitiveCommit. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. @@ -22,6 +20,5 @@ Section TransitiveCommit. forall net, refined_raft_intermediate_reachable net -> transitive_commit net - }. - + }. End TransitiveCommit. diff --git a/raft/UniqueIndicesInterface.v b/raft/UniqueIndicesInterface.v index 5924b180..0135b161 100644 --- a/raft/UniqueIndicesInterface.v +++ b/raft/UniqueIndicesInterface.v @@ -1,9 +1,6 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section UniqueIndicesInterface. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/VotedForMoreUpToDateInterface.v b/raft/VotedForMoreUpToDateInterface.v index 0acb86ac..b6e0b504 100644 --- a/raft/VotedForMoreUpToDateInterface.v +++ b/raft/VotedForMoreUpToDateInterface.v @@ -1,12 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotedForMoreUpToDate. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Definition votedFor_moreUpToDate (net : network) : Prop := forall t h h', currentTerm (snd (nwState net h)) = t -> diff --git a/raft/VotedForTermSanityInterface.v b/raft/VotedForTermSanityInterface.v index 0f4ad6a4..e99ace3d 100644 --- a/raft/VotedForTermSanityInterface.v +++ b/raft/VotedForTermSanityInterface.v @@ -1,12 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotedForTermSanity. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Definition votedFor_term_sanity (net : network) : Prop := forall t h h', currentTerm (snd (nwState net h')) = t -> diff --git a/raft/VotesCorrectInterface.v b/raft/VotesCorrectInterface.v index 2663ebed..4de89e87 100644 --- a/raft/VotesCorrectInterface.v +++ b/raft/VotesCorrectInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotesCorrectInterface. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/VotesLeCurrentTermInterface.v b/raft/VotesLeCurrentTermInterface.v index f484a965..91d5f49c 100644 --- a/raft/VotesLeCurrentTermInterface.v +++ b/raft/VotesLeCurrentTermInterface.v @@ -1,8 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotesLeCurrentTermInterface. - Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. diff --git a/raft/VotesReceivedMoreUpToDateInterface.v b/raft/VotesReceivedMoreUpToDateInterface.v index 26c8927f..0315bf0c 100644 --- a/raft/VotesReceivedMoreUpToDateInterface.v +++ b/raft/VotesReceivedMoreUpToDateInterface.v @@ -1,12 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotesReceivedMoreUpToDate. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. - Definition votesReceived_moreUpToDate (net : network) : Prop := forall t h h', currentTerm (snd (nwState net h)) = t -> diff --git a/raft/VotesVotesWithLogCorrespondInterface.v b/raft/VotesVotesWithLogCorrespondInterface.v index 1df4e4e1..a186bf8b 100644 --- a/raft/VotesVotesWithLogCorrespondInterface.v +++ b/raft/VotesVotesWithLogCorrespondInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotesVotesWithLogCorrespond. Context {orig_base_params : BaseParams}. diff --git a/raft/VotesWithLogSortedInterface.v b/raft/VotesWithLogSortedInterface.v index 476e6438..d6376e04 100644 --- a/raft/VotesWithLogSortedInterface.v +++ b/raft/VotesWithLogSortedInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section VotesWithLogSorted. Context {orig_base_params : BaseParams}. diff --git a/raft/VotesWithLogTermSanityInterface.v b/raft/VotesWithLogTermSanityInterface.v index df38d048..76588d20 100644 --- a/raft/VotesWithLogTermSanityInterface.v +++ b/raft/VotesWithLogTermSanityInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section VotesWithLogTermSanity. Context {orig_base_params : BaseParams}. diff --git a/script/assumptions.v b/script/assumptions.v index 4d42461e..c65c4695 100644 --- a/script/assumptions.v +++ b/script/assumptions.v @@ -1,4 +1,4 @@ -Require Import VerdiRaft.EndToEndLinearizability. +From VerdiRaft Require Import EndToEndLinearizability. About raft_linearizable. Print Assumptions raft_linearizable. diff --git a/systems/VarDRaft.v b/systems/VarDRaft.v index 81990259..5b59f4d8 100644 --- a/systems/VarDRaft.v +++ b/systems/VarDRaft.v @@ -1,6 +1,6 @@ -Require Import VerdiRaft.Raft. -Require Import Verdi.VarD. -Require Import String. +From VerdiRaft Require Import Raft. +From Verdi Require Import VarD. +From Coq Require Import String. Section VarDRaft. Variable n : nat. diff --git a/systems/VarDRaftCorrect.v b/systems/VarDRaftCorrect.v index 22f3f241..38b99148 100644 --- a/systems/VarDRaftCorrect.v +++ b/systems/VarDRaftCorrect.v @@ -1,14 +1,7 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.Linearizability. -Require Import VerdiRaft.RaftLinearizableProofs. - -Require Import VerdiRaft.EndToEndLinearizability. - -Require Import VerdiRaft.VarDRaft. +From Verdi Require Import Verdi VarD. +From VerdiRaft Require Import Raft CommonDefinitions. +From VerdiRaft Require Import Linearizability RaftLinearizableProofs. +From VerdiRaft Require Import EndToEndLinearizability VarDRaft. Section VarDRaftCorrect. Variable n : nat. diff --git a/systems/VarDRaftLog.v b/systems/VarDRaftLog.v index c3dcc422..f347ca47 100644 --- a/systems/VarDRaftLog.v +++ b/systems/VarDRaftLog.v @@ -1,13 +1,6 @@ -Require Import Verdi.Verdi. -Require Import Cheerios.Cheerios. -Require Import Cheerios.Tree. - -Require Import Verdi.VarD. -Require Import Verdi.Log. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.VarDRaft. -Require Import VerdiRaft.VarDRaftSerializers. +From Verdi Require Import Verdi VarD Log. +From Cheerios Require Import Cheerios Tree. +From VerdiRaft Require Import Raft VarDRaft VarDRaftSerializers. Section Logged. Variables n snapshot_interval : nat. @@ -15,7 +8,10 @@ Section Logged. Instance raft_params : RaftParams VarD.vard_base_params := raft_params n. - Definition transformed_base_params : BaseParams := @log_base_params base_params. - Definition transformed_multi_params : DiskOpMultiParams transformed_base_params := log_multi_params snapshot_interval. - Definition transformed_failure_params : DiskOpFailureParams transformed_multi_params := log_failure_params snapshot_interval. + Definition transformed_base_params : BaseParams := + @log_base_params base_params. + Definition transformed_multi_params : DiskOpMultiParams transformed_base_params := + log_multi_params snapshot_interval. + Definition transformed_failure_params : DiskOpFailureParams transformed_multi_params := + log_failure_params snapshot_interval. End Logged. diff --git a/systems/VarDRaftLogCorrect.v b/systems/VarDRaftLogCorrect.v index 80fadbca..daa02f34 100644 --- a/systems/VarDRaftLogCorrect.v +++ b/systems/VarDRaftLogCorrect.v @@ -1,18 +1,8 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import Cheerios.Cheerios. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.Linearizability. -Require Import VerdiRaft.RaftLinearizableProofs. - -Require Import VerdiRaft.EndToEndLinearizability. - -Require Import Verdi.Log. -Require Import Verdi.LogCorrect. - -Require Import VerdiRaft.VarDRaftLog. +From Verdi Require Import Verdi VarD Log LogCorrect. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import Raft CommonDefinitions. +From VerdiRaft Require Import Linearizability RaftLinearizableProofs. +From VerdiRaft Require Import EndToEndLinearizability VarDRaftLog. Section VarDLogCorrect. Variables n snapshot_interval : nat. @@ -20,9 +10,12 @@ Section VarDLogCorrect. Instance raft_params : RaftParams VarD.vard_base_params := raft_params n. - Instance transformed_base_params : BaseParams := transformed_base_params n. - Instance transformed_multi_params : DiskOpMultiParams _ := transformed_multi_params n snapshot_interval. - Instance transformed_failure_params : DiskOpFailureParams _ := transformed_failure_params n snapshot_interval. + Instance transformed_base_params : BaseParams := + transformed_base_params n. + Instance transformed_multi_params : DiskOpMultiParams _ := + transformed_multi_params n snapshot_interval. + Instance transformed_failure_params : DiskOpFailureParams _ := + transformed_failure_params n snapshot_interval. Theorem vard_raft_log_linearizable : forall failed net tr, diff --git a/systems/VarDRaftSerialized.v b/systems/VarDRaftSerialized.v index f9300e18..c6dca368 100644 --- a/systems/VarDRaftSerialized.v +++ b/systems/VarDRaftSerialized.v @@ -1,12 +1,6 @@ -Require Import Verdi.Verdi. -Require Import Verdi.SerializedMsgParams. -Require Import Verdi.VarD. - -Require Import Cheerios.Cheerios. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.VarDRaft. -Require Import VerdiRaft.VarDRaftSerializers. +From Verdi Require Import Verdi SerializedMsgParams VarD. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import Raft VarDRaft VarDRaftSerializers. Section Serialized. Variable n : nat. diff --git a/systems/VarDRaftSerializedCorrect.v b/systems/VarDRaftSerializedCorrect.v index f2b7d23b..7b6d2c1c 100644 --- a/systems/VarDRaftSerializedCorrect.v +++ b/systems/VarDRaftSerializedCorrect.v @@ -1,17 +1,9 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import Verdi.PartialMapSimulations. -Require Import Cheerios.Cheerios. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.Linearizability. -Require Import VerdiRaft.RaftLinearizableProofs. - -Require Import VerdiRaft.EndToEndLinearizability. -Require Import Verdi.SerializedMsgParamsCorrect. - -Require Import VerdiRaft.VarDRaftSerialized. +From Verdi Require Import Verdi VarD. +From Verdi Require Import PartialMapSimulations SerializedMsgParamsCorrect. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import Raft CommonDefinitions. +From VerdiRaft Require Import Linearizability RaftLinearizableProofs. +From VerdiRaft Require Import EndToEndLinearizability VarDRaftSerialized. Section VarDSerializedCorrect. Variable n : nat. diff --git a/systems/VarDRaftSerializedLog.v b/systems/VarDRaftSerializedLog.v index b1f86b64..01af980e 100644 --- a/systems/VarDRaftSerializedLog.v +++ b/systems/VarDRaftSerializedLog.v @@ -1,14 +1,6 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import Verdi.SerializedMsgParams. -Require Import Verdi.Log. - -Require Import Cheerios.Cheerios. -Require Import Cheerios.Tree. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.VarDRaftSerializers. -Require Import VerdiRaft.VarDRaftSerialized. +From Verdi Require Import Verdi VarD SerializedMsgParams Log. +From Cheerios Require Import Cheerios Tree. +From VerdiRaft Require Import Raft VarDRaftSerializers VarDRaftSerialized. Section SerializedLog. Variables n snapshot_interval : nat. diff --git a/systems/VarDRaftSerializedLogCorrect.v b/systems/VarDRaftSerializedLogCorrect.v index 45ffe9a9..c4b9bdda 100644 --- a/systems/VarDRaftSerializedLogCorrect.v +++ b/systems/VarDRaftSerializedLogCorrect.v @@ -1,16 +1,9 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. -Require Import Cheerios.Cheerios. -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.Linearizability. -Require Import VerdiRaft.RaftLinearizableProofs. - -Require Import Verdi.LogCorrect. -Require Import VerdiRaft.VarDRaftSerializedCorrect. - -Require Import VerdiRaft.VarDRaftSerializedLog. +From Verdi Require Import Verdi VarD LogCorrect. +From Cheerios Require Import Cheerios. +From VerdiRaft Require Import Raft CommonDefinitions. +From VerdiRaft Require Import Linearizability RaftLinearizableProofs. +From VerdiRaft Require Import VarDRaftSerializedCorrect. +From VerdiRaft Require Import VarDRaftSerializedLog. Section SerializedLogCorrect. Variables n snapshot_interval : nat. @@ -18,9 +11,12 @@ Section SerializedLogCorrect. Instance raft_params : RaftParams VarD.vard_base_params := raft_params n. - Instance transformed_base_params : BaseParams := transformed_base_params n. - Instance transformed_multi_params : DiskOpMultiParams _ := transformed_multi_params n snapshot_interval. - Instance transformed_failure_params : DiskOpFailureParams _ := transformed_failure_params n snapshot_interval. + Instance transformed_base_params : BaseParams := + transformed_base_params n. + Instance transformed_multi_params : DiskOpMultiParams _ := + transformed_multi_params n snapshot_interval. + Instance transformed_failure_params : DiskOpFailureParams _ := + transformed_failure_params n snapshot_interval. Theorem vard_raft_log_linearizable : forall failed net tr, diff --git a/systems/VarDRaftSerializers.v b/systems/VarDRaftSerializers.v index 9fb9ae62..e81388eb 100644 --- a/systems/VarDRaftSerializers.v +++ b/systems/VarDRaftSerializers.v @@ -1,11 +1,6 @@ -Require Import Verdi.Verdi. -Require Import Verdi.VarD. - -Require Import Cheerios.Cheerios. -Require Import Cheerios.Tree. - -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.VarDRaft. +From Verdi Require Import Verdi VarD. +From Cheerios Require Import Cheerios Tree. +From VerdiRaft Require Import Raft VarDRaft. Import DeserializerNotations.