Consistently use From-Require to enable module relocation

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.

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.

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.

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.

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.

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}.

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}.

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}.

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}.

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}.

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}.

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}.

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}.

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}.