# Packages matching: installed
# Name # Installed # Synopsis
base-bigarray base
base-threads base
base-unix base
conf-gmp 4 Virtual package relying on a GMP lib system installation
coq dev The Coq Proof Assistant
coq-core dev The Coq Proof Assistant -- Core Binaries and Tools
coq-stdlib dev The Coq Proof Assistant -- Standard Library
coqide-server dev The Coq Proof Assistant, XML protocol server
dune 3.12.1 Fast, portable, and opinionated build system
ocaml 4.14.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.14.0 Official release 4.14.0
ocaml-config 2 OCaml Switch Configuration
ocaml-options-vanilla 1 Ensure that OCaml is compiled with no special options enabled
ocamlfind 1.9.6 A library manager for OCaml
zarith 1.13 Implements arithmetic and logical operations over arbitrary-precision integers
# opam file:
opam-version: "2.0"
maintainer: "palmskog@gmail.com"
homepage: "https://github.com/uwplse/verdi-raft"
dev-repo: "git+https://github.com/uwplse/verdi-raft.git"
bug-reports: "https://github.com/uwplse/verdi-raft/issues"
license: "BSD-2-Clause"
synopsis: "Verified implementation of the Raft distributed consensus protocol in Coq"
description: """
Raft is a distributed consensus algorithm that is designed to be easy to understand
and is equivalent to Paxos in fault tolerance and performance. Verdi Raft is a
verified implementation of Raft in Coq, constructed using the Verdi framework.
Included is a verified fault-tolerant key-value store using Raft."""
build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.14"}
"coq-verdi" {= "dev"}
"coq-struct-tact" {= "dev"}
"coq-cheerios" {= "dev"}
]
tags: [
"category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems"
"keyword:program verification"
"keyword:distributed algorithms"
"keyword:fault tolerance"
"keyword:key-value store"
"keyword:raft"
"logpath:VerdiRaft"
]
authors: [
"Justin Adsuara"
"Steve Anton"
"Ryan Doenges"
"Karl Palmskog"
"Pavel Panchekha"
"Zachary Tatlock"
"James R. Wilcox"
"Doug Woos"
]
url {
src: "git+https://github.com/uwplse/verdi-raft.git#master"
}
trueDry install with the current Coq version:
opam install -y --show-action coq-verdi-raft.dev coq.devDry install without Coq/switch base, to test if the problem was incompatibility with the current Coq/OCaml version:
trueopam list; echo; ulimit -Sv 4000000; timeout 4h opam install -y --deps-only coq-verdi-raft.dev coq.devopam list; echo; ulimit -Sv 16000000; timeout 4h opam install -y coq-verdi-raft.dev coq.devTotal: 34 M
../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesCorrectProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SpecLemmas.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogMatchingProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementSpecLemmas.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrefixWithinTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexAllEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineCorrectProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonTheorems.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderSublogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogsLeaderLogsProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputCorrectProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestLeaderLogsProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderSublogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftMsgRefinementProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InputBeforeOutputProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesVotesWithLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedImpliesInputProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Raft.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesLeaderProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogMatchingProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyMoreUpToDateProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftLinearizableProofs.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputGreatestIdProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonTheorems.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedEntriesMonotonicProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsStrongProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/SortedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftRefinementProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForMoreUpToDateProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogCandidateEntriesTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SpecLemmas.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Linearizability.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineCorrectProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NextIndexSafetyProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RefinedLogMatchingLemmasProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrefixWithinTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogMatchingProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidatesVoteForSelvesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSublogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Linearizability.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializers.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogLeaderSublogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftRefinementInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Raft.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogLogMatchingProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftMsgRefinementInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputImpliesAppliedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteMaxIndexMaxTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftRefinementInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesCandidateEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesReceivedMoreUpToDateProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftMsgRefinementInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftLinearizableProofs.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogAllEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsPreservedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/DecompositionWithPostState.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftMsgRefinementProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyPrimeProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogMatchingProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementSpecLemmas.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputCorrectProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexAllEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderLogPerTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogCorrectProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsVotesWithLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderCompletenessProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesCorrectProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsCandidateEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogAllEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateTermGtLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsContiguousProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EndToEndLinearizability.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonTheorems.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesVotesWithLogCorrespondProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftRefinementProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogSortedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CausalOrderPreservedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSublogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedLeCommitIndexProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedCorrect.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesRepliesToSelfProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InputBeforeOutputProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogsLeaderLogsProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InLogInAllEntriesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSortedProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesCorrectProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrefixWithinTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogMatchingProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/DecompositionWithPostState.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesIndicesGt0Proof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RefinedLogMatchingLemmasProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonTheorems.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedImpliesInputProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderSublogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesLeCurrentTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexLeaderProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToSelfProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedEntriesMonotonicProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogCandidateEntriesTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/SortedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineCorrectProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CurrentTermGtZeroProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinedLogMatchingLemmasInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogsLogPropertiesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestLeaderLogsProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogPropertiesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogMatchingProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateTraceInvariant.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogLogMatchingProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLogCorrect.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLogCorrect.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyPrimeProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogMatchingProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftCorrect.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesLeaderProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderCompletenessProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TraceUtil.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedCommitIndexMatchingProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputGreatestIdProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToLeaderProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonDefinitions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Linearizability.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftState.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesVotesWithLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SpecLemmas.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexAllEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesReplySublogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SortedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftMsgRefinementProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderSublogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializers.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftLinearizableProofs.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogMatchingInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsStrongProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogsLeaderLogsProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogLeaderSublogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/Raft.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogsLeaderLogsInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesCorrectInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderCompletenessInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderLogPerTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsVotesWithLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesCorrectInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderPerTermProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedCommitIndexMatchingInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NextIndexSafetyProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineCorrectInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TransitiveCommitProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyMoreUpToDateInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputCorrectProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedImpliesInputInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderSublogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForMoreUpToDateInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestLeaderLogsInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedEntriesMonotonicInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputImpliesAppliedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrefixWithinTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EndToEndLinearizability.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesReceivedMoreUpToDateInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteMaxIndexMaxTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyPrimeInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonTheorems.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesLeaderInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexAllEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsStrongInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesVotesWithLogCorrespondInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonDefinitions.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogCorrectInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSublogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesVotesWithLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestTermSanityProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsVotesWithLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderSublogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CausalOrderPreservedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogsLogPropertiesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InputBeforeOutputProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsPreservedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogLeaderSublogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogPropertiesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderLogPerTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestReplyCorrespondenceInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogMatchingInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestsCameFromLeadersInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TransitiveCommitInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogLogMatchingInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/UniqueIndicesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogAllEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsPreservedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputImpliesAppliedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogMatchingInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogAllEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesReplySublogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputGreatestIdInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommitRecordedCommittedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToLeaderInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogCandidateEntriesTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InLogInAllEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InputBeforeOutputInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesLeCurrentTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestTermSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesCorrectProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsCandidateEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedHostLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsContiguousInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogSortedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RaftRefinementProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputCorrectInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesCandidateEntriesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSortedInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesIndicesGt0Interface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderPerTermInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToSelfInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MaxIndexSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexSanityInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateTermGtLogInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexLeaderInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLog.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesRepliesToSelfInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NextIndexSafetyInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidatesVoteForSelvesInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CurrentTermGtZeroInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerialized.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedLeCommitIndexInterface.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftState.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLog.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/UniqueIndicesProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedHostLogProof.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerializedLog.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftRefinementInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementSpecLemmas.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftLog.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerialized.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaft.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogMatchingProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogCorrectProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftDebug.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaft.vo../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestLeaderLogsProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftMsgRefinementInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesCandidateEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateTraceInvariant.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogLogMatchingProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/SortedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EndToEndLinearizability.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogAllEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyMoreUpToDateProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedEntriesMonotonicProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsContiguousProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonDefinitions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinedLogMatchingLemmasInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogAllEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsCandidateEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/StateMachineSafetyPrimeProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderSublogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogSortedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesCorrectProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogCandidateEntriesTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedLeCommitIndexProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLogMatchingProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSortedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TraceUtil.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogsLogPropertiesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForMoreUpToDateProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesReceivedMoreUpToDateProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputGreatestIdProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CausalOrderPreservedProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesVotesWithLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogMatchingInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppliedImpliesInputProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesIndicesGt0Proof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesLeaderProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/DecompositionWithPostState.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedCorrect.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSublogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderSublogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteMaxIndexMaxTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderCompletenessProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesLeCurrentTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/PrevLogLeaderSublogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InLogInAllEntriesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyMoreUpToDateProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogPropertiesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToLeaderProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedCommitIndexMatchingProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsVotesWithLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesCandidateEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogAllEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SortedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsCandidateEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogsLeaderLogsInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CroniesTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LogAllEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NextIndexSafetyProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OutputImpliesAppliedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderLogPerTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsPreservedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsStrongProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogCorrectProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesRepliesToSelfProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidatesVoteForSelvesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForMoreUpToDateProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesCorrectProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesReplySublogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializers.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TermsAndIndicesFromOneLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesVotesWithLogCorrespondProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderCompletenessInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexLeaderProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteReplyTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToSelfProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CurrentTermGtZeroProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestLeaderLogsInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateTermGtLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteMaxIndexMaxTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedCommitIndexMatchingInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesReceivedMoreUpToDateProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonTheorems.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderLogPerTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedLeCommitIndexProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsContiguousProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/GhostLogsLogPropertiesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsSortedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogSortedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesCorrectInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RequestVoteTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/RefinedLogMatchingLemmasProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedCorrect.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RaftState.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesIndicesGt0Proof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotedForTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesCorrectInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeaderLogsLogPropertiesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineCorrectInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedImpliesInputInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyPrimeInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/InLogInAllEntriesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LastAppliedCommitIndexMatchingProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderPerTermProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyMoreUpToDateInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderSublogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesLeCurrentTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesVotesWithLogCorrespondInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TraceUtil.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestReplyCorrespondenceInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesRepliesToSelfProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/MatchIndexLeaderProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CausalOrderPreservedProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/LeadersHaveLeaderLogsProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonDefinitions.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesVotesWithLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CurrentTermGtZeroProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidateTermGtLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForMoreUpToDateInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedEntriesMonotonicInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToSelfProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CausalOrderPreservedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesReceivedMoreUpToDateInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/CandidatesVoteForSelvesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsVotesWithLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogCorrectInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogLeaderSublogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLogCorrect.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteMaxIndexMaxTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsStrongInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLogCorrect.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestTermSanityProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AllEntriesLeaderLogsProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommonDefinitions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexAllEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/NoAppendEntriesToLeaderProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesLeaderInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateTraceInvariant.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrefixWithinTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestsCameFromLeadersInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftCorrect.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinedLogMatchingLemmasInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputImpliesAppliedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsPreservedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSublogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesWithLogTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InputBeforeOutputInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/VotesVotesWithLogCorrespondProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesReplySublogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputGreatestIdInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogPropertiesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToLeaderInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderSublogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogCandidateEntriesTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/UniqueIndicesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogMatchingInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesReplySublogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TransitiveCommitInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLog.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogsLogPropertiesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogAllEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsCandidateEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogAllEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToSelfInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderPerTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesRepliesToSelfInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MaxIndexSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogMatchingInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogMatchingInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesCandidateEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InLogInAllEntriesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesTermSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateTermGtLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesLeCurrentTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogSortedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommitRecordedCommittedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/OneLeaderPerTermProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsContiguousInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputCorrectInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedHostLogInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/UniqueIndicesProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexSanityInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexLeaderInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSortedInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NextIndexSafetyInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TransitiveCommitProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogLogMatchingInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesTermInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerialized.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidatesVoteForSelvesInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesIndicesGt0Interface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedHostLogProof.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/SortedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CurrentTermGtZeroInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedLeCommitIndexInterface.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogsLeaderLogsInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedCommitIndexMatchingInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLog.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderLogPerTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderCompletenessInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesCorrectInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/AppendEntriesRequestTermSanityProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineCorrectInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLogCorrect.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyPrimeInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderSublogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/StateMachineSafetyInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLogCorrect.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesCorrectInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedImpliesInputInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaft.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestLeaderLogsInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestReplyCorrespondenceInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrefixWithinTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerializedLog.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyMoreUpToDateInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/TransitiveCommitProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesVotesWithLogCorrespondInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CausalOrderPreservedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogLeaderSublogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogCorrectInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForMoreUpToDateInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TermsAndIndicesFromOneInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesReceivedMoreUpToDateInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsVotesWithLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/UniqueIndicesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppliedEntriesMonotonicInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/PrevLogCandidateEntriesTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerializedLog.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftCorrect.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftLog.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RefinementCommonDefinitions.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/UniqueIndicesProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesLeaderInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteMaxIndexMaxTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsStrongInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerialized.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesVotesWithLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogsLogPropertiesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogPropertiesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexAllEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputGreatestIdInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/RaftProofs/EveryEntryWasCreatedHostLogProof.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InputBeforeOutputInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CommitRecordedCommittedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputImpliesAppliedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestsCameFromLeadersInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderSublogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftSerialized.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSublogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToLeaderInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteReplyTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsCandidateEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLeaderLogsTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MaxIndexSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/EveryEntryWasCreatedHostLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesReplySublogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/TransitiveCommitInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogAllEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AppendEntriesRequestTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesCandidateEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsLogMatchingInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsPreservedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesLogMatchingInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesRepliesToSelfInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/GhostLogLogMatchingInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeadersHaveLeaderLogsInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsContiguousInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/RequestVoteTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotedForTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NoAppendEntriesToSelfInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogSortedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OneLeaderPerTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LeaderLogsSortedInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesWithLogTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexLeaderInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidateTermGtLogInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/MatchIndexSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LogAllEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerializedLog.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/VotesLeCurrentTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/InLogInAllEntriesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesIndicesGt0Interface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/AllEntriesTermSanityInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaftLog.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CandidatesVoteForSelvesInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftSerialized.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftLog.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/LastAppliedLeCommitIndexInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/NextIndexSafetyInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CroniesTermInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftDebug.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/CurrentTermGtZeroInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaft.glob../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Raft/OutputCorrectInterface.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/Systems/VarDRaft.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaftDebug.v../ocaml-base-compiler.4.14.0/lib/coq/user-contrib/VerdiRaft/ExtractVarDRaft.vopam remove -y coq-verdi-raft.dev