-
Notifications
You must be signed in to change notification settings - Fork 19
/
Copy path_CoqProject
218 lines (214 loc) · 9.55 KB
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
-Q theories VerdiRaft
-Q extraction/vard/coq VerdiRaft
-Q extraction/vard-serialized/coq VerdiRaft
-Q extraction/vard-log/coq VerdiRaft
-Q extraction/vard-serialized-log/coq VerdiRaft
-Q extraction/vard-debug/coq VerdiRaft
theories/Raft/CommonTheorems.v
theories/Raft/AppliedImpliesInputInterface.v
theories/Raft/VotesVotesWithLogCorrespondInterface.v
theories/Raft/InLogInAllEntriesInterface.v
theories/Raft/AllEntriesCandidateEntriesInterface.v
theories/Raft/SpecLemmas.v
theories/Raft/StateMachineSafetyPrimeInterface.v
theories/Raft/VotedForTermSanityInterface.v
theories/Raft/CroniesCorrectInterface.v
theories/Raft/AppliedEntriesMonotonicInterface.v
theories/Raft/RaftLinearizableProofs.v
theories/Raft/TransitiveCommitInterface.v
theories/Raft/VotedForMoreUpToDateInterface.v
theories/Raft/LeaderLogsTermSanityInterface.v
theories/Raft/LastAppliedLeCommitIndexInterface.v
theories/Raft/RefinementSpecLemmas.v
theories/Raft/AllEntriesLeaderLogsInterface.v
theories/Raft/LeaderLogsCandidateEntriesInterface.v
theories/Raft/RaftMsgRefinementInterface.v
theories/Raft/VotesWithLogSortedInterface.v
theories/Raft/StateMachineSafetyInterface.v
theories/Raft/AllEntriesLeaderSublogInterface.v
theories/Raft/DecompositionWithPostState.v
theories/Raft/GhostLogCorrectInterface.v
theories/Raft/LeaderLogsPreservedInterface.v
theories/Raft/LogsLeaderLogsInterface.v
theories/Raft/PrevLogLeaderSublogInterface.v
theories/Raft/AppendEntriesRequestReplyCorrespondenceInterface.v
theories/Raft/LeaderLogsSortedInterface.v
theories/Raft/MatchIndexSanityInterface.v
theories/Raft/LeadersHaveLeaderLogsInterface.v
theories/Raft/LeaderCompletenessInterface.v
theories/Raft/VotesWithLogTermSanityInterface.v
theories/Raft/Linearizability.v
theories/Raft/AppendEntriesLeaderInterface.v
theories/Raft/CandidateTermGtLogInterface.v
theories/Raft/GhostLogAllEntriesInterface.v
theories/Raft/OneLeaderPerTermInterface.v
theories/Raft/MatchIndexAllEntriesInterface.v
theories/Raft/CausalOrderPreservedInterface.v
theories/Raft/CroniesTermInterface.v
theories/Raft/UniqueIndicesInterface.v
theories/Raft/CurrentTermGtZeroInterface.v
theories/Raft/LeaderSublogInterface.v
theories/Raft/LogMatchingInterface.v
theories/Raft/InputBeforeOutputInterface.v
theories/Raft/CandidatesVoteForSelvesInterface.v
theories/Raft/RequestVoteReplyMoreUpToDateInterface.v
theories/Raft/StateMachineCorrectInterface.v
theories/Raft/CandidateEntriesInterface.v
theories/Raft/LastAppliedCommitIndexMatchingInterface.v
theories/Raft/RaftState.v
theories/Raft/NextIndexSafetyInterface.v
theories/Raft/NoAppendEntriesToSelfInterface.v
theories/Raft/LogAllEntriesInterface.v
theories/Raft/RefinementCommonTheorems.v
theories/Raft/LeadersHaveLeaderLogsStrongInterface.v
theories/Raft/NoAppendEntriesToLeaderInterface.v
theories/Raft/OneLeaderLogPerTermInterface.v
theories/Raft/TermsAndIndicesFromOneInterface.v
theories/Raft/AllEntriesLogMatchingInterface.v
theories/Raft/RequestVoteTermSanityInterface.v
theories/Raft/GhostLogsLogPropertiesInterface.v
theories/Raft/RequestVoteReplyTermSanityInterface.v
theories/Raft/MatchIndexLeaderInterface.v
theories/Raft/OutputImpliesAppliedInterface.v
theories/Raft/GhostLogLogMatchingInterface.v
theories/Raft/EveryEntryWasCreatedHostLogInterface.v
theories/Raft/AppendEntriesReplySublogInterface.v
theories/Raft/AppendEntriesRequestsCameFromLeadersInterface.v
theories/Raft/CommonDefinitions.v
theories/Raft/PrefixWithinTermInterface.v
theories/Raft/AppendEntriesRequestTermSanityInterface.v
theories/Raft/AllEntriesLeaderLogsTermInterface.v
theories/Raft/SortedInterface.v
theories/Raft/VotesLeCurrentTermInterface.v
theories/Raft/Raft.v
theories/Raft/OutputGreatestIdInterface.v
theories/Raft/CommitRecordedCommittedInterface.v
theories/Raft/VotesCorrectInterface.v
theories/Raft/VotesReceivedMoreUpToDateInterface.v
theories/Raft/AllEntriesIndicesGt0Interface.v
theories/Raft/LeaderLogsVotesWithLogInterface.v
theories/Raft/NoAppendEntriesRepliesToSelfInterface.v
theories/Raft/AppendEntriesRequestLeaderLogsInterface.v
theories/Raft/LeaderLogsLogPropertiesInterface.v
theories/Raft/LeaderLogsSublogInterface.v
theories/Raft/LeaderLogsContiguousInterface.v
theories/Raft/TermSanityInterface.v
theories/Raft/TermsAndIndicesFromOneLogInterface.v
theories/Raft/PrevLogCandidateEntriesTermInterface.v
theories/Raft/StateTraceInvariant.v
theories/Raft/AllEntriesTermSanityInterface.v
theories/Raft/RefinedLogMatchingLemmasInterface.v
theories/Raft/AllEntriesLogInterface.v
theories/Raft/AllEntriesVotesWithLogInterface.v
theories/Raft/LeaderLogsLogMatchingInterface.v
theories/Raft/MaxIndexSanityInterface.v
theories/Raft/RequestVoteMaxIndexMaxTermInterface.v
theories/Raft/OutputCorrectInterface.v
theories/Raft/RaftRefinementInterface.v
theories/Raft/TraceUtil.v
theories/Raft/EveryEntryWasCreatedInterface.v
theories/Raft/RefinementCommonDefinitions.v
theories/RaftProofs/StateMachineSafetyProof.v
theories/RaftProofs/NoAppendEntriesToLeaderProof.v
theories/RaftProofs/GhostLogsLogPropertiesProof.v
theories/RaftProofs/TermSanityProof.v
theories/RaftProofs/MatchIndexSanityProof.v
theories/RaftProofs/OneLeaderPerTermProof.v
theories/RaftProofs/CroniesCorrectProof.v
theories/RaftProofs/LogMatchingProof.v
theories/RaftProofs/SortedProof.v
theories/RaftProofs/RequestVoteReplyMoreUpToDateProof.v
theories/RaftProofs/EveryEntryWasCreatedProof.v
theories/RaftProofs/TransitiveCommitProof.v
theories/RaftProofs/AllEntriesLeaderLogsProof.v
theories/RaftProofs/TermsAndIndicesFromOneLogProof.v
theories/RaftProofs/EveryEntryWasCreatedHostLogProof.v
theories/RaftProofs/VotedForTermSanityProof.v
theories/RaftProofs/OutputCorrectProof.v
theories/RaftProofs/OutputImpliesAppliedProof.v
theories/RaftProofs/LeaderLogsSublogProof.v
theories/RaftProofs/AllEntriesLogProof.v
theories/RaftProofs/RequestVoteTermSanityProof.v
theories/RaftProofs/GhostLogAllEntriesProof.v
theories/RaftProofs/AppliedImpliesInputProof.v
theories/RaftProofs/LeaderLogsVotesWithLogProof.v
theories/RaftProofs/LeaderLogsTermSanityProof.v
theories/RaftProofs/LastAppliedCommitIndexMatchingProof.v
theories/RaftProofs/AllEntriesLogMatchingProof.v
theories/RaftProofs/VotesReceivedMoreUpToDateProof.v
theories/RaftProofs/CandidateEntriesProof.v
theories/RaftProofs/CroniesTermProof.v
theories/RaftProofs/VotesWithLogTermSanityProof.v
theories/RaftProofs/CandidateTermGtLogProof.v
theories/RaftProofs/AppendEntriesRequestsCameFromLeadersProof.v
theories/RaftProofs/AppendEntriesReplySublogProof.v
theories/RaftProofs/MatchIndexLeaderProof.v
theories/RaftProofs/AppendEntriesRequestTermSanityProof.v
theories/RaftProofs/StateMachineSafetyPrimeProof.v
theories/RaftProofs/LogsLeaderLogsProof.v
theories/RaftProofs/AllEntriesLeaderLogsTermProof.v
theories/RaftProofs/OutputGreatestIdProof.v
theories/RaftProofs/AppendEntriesRequestLeaderLogsProof.v
theories/RaftProofs/PrefixWithinTermProof.v
theories/RaftProofs/AppendEntriesRequestReplyCorrespondenceProof.v
theories/RaftProofs/OneLeaderLogPerTermProof.v
theories/RaftProofs/RefinedLogMatchingLemmasProof.v
theories/RaftProofs/CurrentTermGtZeroProof.v
theories/RaftProofs/LeaderLogsSortedProof.v
theories/RaftProofs/AppendEntriesLeaderProof.v
theories/RaftProofs/MatchIndexAllEntriesProof.v
theories/RaftProofs/NoAppendEntriesToSelfProof.v
theories/RaftProofs/InputBeforeOutputProof.v
theories/RaftProofs/LeaderLogsContiguousProof.v
theories/RaftProofs/VotesWithLogSortedProof.v
theories/RaftProofs/UniqueIndicesProof.v
theories/RaftProofs/AppliedEntriesMonotonicProof.v
theories/RaftProofs/TermsAndIndicesFromOneProof.v
theories/RaftProofs/LeadersHaveLeaderLogsProof.v
theories/RaftProofs/AllEntriesVotesWithLogProof.v
theories/RaftProofs/LeadersHaveLeaderLogsStrongProof.v
theories/RaftProofs/LastAppliedLeCommitIndexProof.v
theories/RaftProofs/CausalOrderPreservedProof.v
theories/RaftProofs/StateMachineCorrectProof.v
theories/RaftProofs/RequestVoteReplyTermSanityProof.v
theories/RaftProofs/RaftRefinementProof.v
theories/RaftProofs/VotesVotesWithLogCorrespondProof.v
theories/RaftProofs/LogAllEntriesProof.v
theories/RaftProofs/VotedForMoreUpToDateProof.v
theories/RaftProofs/AllEntriesTermSanityProof.v
theories/RaftProofs/NextIndexSafetyProof.v
theories/RaftProofs/LeaderLogsLogMatchingProof.v
theories/RaftProofs/GhostLogLogMatchingProof.v
theories/RaftProofs/AllEntriesCandidateEntriesProof.v
theories/RaftProofs/PrevLogCandidateEntriesTermProof.v
theories/RaftProofs/AllEntriesLeaderSublogProof.v
theories/RaftProofs/AllEntriesIndicesGt0Proof.v
theories/RaftProofs/GhostLogCorrectProof.v
theories/RaftProofs/VotesCorrectProof.v
theories/RaftProofs/LeaderLogsPreservedProof.v
theories/RaftProofs/RaftMsgRefinementProof.v
theories/RaftProofs/EndToEndLinearizability.v
theories/RaftProofs/NoAppendEntriesRepliesToSelfProof.v
theories/RaftProofs/LeaderCompletenessProof.v
theories/RaftProofs/CandidatesVoteForSelvesProof.v
theories/RaftProofs/InLogInAllEntriesProof.v
theories/RaftProofs/RequestVoteMaxIndexMaxTermProof.v
theories/RaftProofs/LeaderLogsCandidateEntriesProof.v
theories/RaftProofs/LeaderLogsLogPropertiesProof.v
theories/RaftProofs/LeaderSublogProof.v
theories/RaftProofs/PrevLogLeaderSublogProof.v
theories/RaftProofs/VotesLeCurrentTermProof.v
theories/Systems/VarDRaftSerializedLogCorrect.v
theories/Systems/VarDRaftCorrect.v
theories/Systems/VarDRaftSerializedCorrect.v
theories/Systems/VarDRaftSerializedLog.v
theories/Systems/VarDRaftLogCorrect.v
theories/Systems/VarDRaftSerialized.v
theories/Systems/VarDRaftSerializers.v
theories/Systems/VarDRaftLog.v
theories/Systems/VarDRaft.v
extraction/vard/coq/ExtractVarDRaft.v
extraction/vard-serialized/coq/ExtractVarDRaftSerialized.v
extraction/vard-log/coq/ExtractVarDRaftLog.v
extraction/vard-serialized-log/coq/ExtractVarDRaftSerializedLog.v
extraction/vard-debug/coq/ExtractVarDRaftDebug.v