blob: ee9fca7eb496d6216f89ca8c3fa724ece5ca6a6c (
plain)
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
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
|
Time | Peak Mem | File Name
------------------------------------------------------------------------------------
39m02.51s | 1980772 ko | Total Time / Peak Mem
------------------------------------------------------------------------------------
3m26.96s | 1980772 ko | Kami/Ex/Multiplier64
3m22.44s | 899104 ko | bedrock2/compiler/src/FlatToRiscv
2m19.56s | 1730872 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI
2m11.59s | 1411224 ko | Kami/Ex/Divider64
1m44.22s | 997556 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeCSR
1m44.11s | 1131272 ko | Kami/Ex/Multiplier32
1m41.50s | 564436 ko | bedrock2/bedrock2/src/Examples/bsearch
1m08.57s | 1312068 ko | Kami/Ex/ProcFDInl
1m07.92s | 590104 ko | bedrock2/deps/riscv-coq/src/Platform/MinimalMMIO
1m01.07s | 798376 ko | Kami/Ex/FifoCorrect
1m00.73s | 847228 ko | Kami/Ex/Divider32
0m50.15s | 573560 ko | bedrock2/deps/riscv-coq/src/Proofs/EncodeBound
0m40.64s | 588832 ko | bedrock2/bedrock2/src/Examples/FE310CompilerDemo
0m40.29s | 668564 ko | Kami/InlineFacts
0m39.12s | 563328 ko | Kami/Renaming
0m37.44s | 672092 ko | Kami/Ex/SimpleFifoCorrect
0m37.08s | 601836 ko | Kami/SemFacts
0m36.08s | 562540 ko | ─preprbedrock2/deps/coqutil/src/Map/TestGoals
0m32.76s | 885880 ko | Kami/ModularFacts
0m28.68s | 639092 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA
0m26.60s | 741048 ko | Kami/Lib/Word
0m26.55s | 632108 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_SB
0m26.45s | 605916 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeA64
0m25.80s | 650288 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeI64
0m25.47s | 729768 ko | bedrock2/processor/src/KamiRiscv
0m23.66s | 610544 ko | bedrock2/compiler/src/EmitsValid
0m22.68s | 653084 ko | Kami/Ex/InDepthTutorial
0m22.60s | 589708 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM
0m21.68s | 506640 ko | Kami/Specialize
0m21.59s | 525428 ko | bedrock2/bedrock2/src/Examples/lightbulb
0m19.20s | 526372 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_66
0m19.19s | 580040 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_UJ
0m17.33s | 724164 ko | Kami/Ex/ProcDecInl
0m15.63s | 555732 ko | bedrock2/compiler/src/examples/MMIO
0m14.78s | 561068 ko | Kami/ParametricSyntax
0m12.11s | 518652 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_S
0m11.74s | 501100 ko | bedrock2/deps/riscv-coq/src/Platform/MetricMinimal
0m09.95s | 568468 ko | bedrock2/deps/coqutil/src/Word/Properties
0m09.77s | 523092 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeM64
0m09.56s | 537308 ko | Kami/Lib/FMap
0m09.35s | 496100 ko | bedrock2/bedrock2/src/Examples/ipow
0m09.26s | 504428 ko | Kami/StepDet
0m09.19s | 663884 ko | bedrock2/bedrock2/src/WeakestPreconditionProperties
0m09.16s | 495544 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_Fence
0m08.98s | 511956 ko | Kami/RefinementFacts
0m08.68s | 494004 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R_atomic
0m08.26s | 505664 ko | bedrock2/compiler/src/FlatToRiscv32
0m07.55s | 534616 ko | Kami/Ex/Fifo
0m07.54s | 454624 ko | ─ensbedrock2/deps/coqutil/src/Map/SlowGoals
0m06.99s | 482444 ko | bedrock2/deps/riscv-coq/src/Platform/Minimal
0m06.89s | 480324 ko | bedrock2/compiler/src/GoFlatToRiscv
0m06.82s | 485168 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I
0m06.72s | 485544 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_FenceI
0m06.50s | 501300 ko | Kami/Semantics
0m06.36s | 478692 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_shift_57
0m06.32s | 478812 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_R
0m06.24s | 509232 ko | Kami/PartialInlineFacts
0m06.02s | 486764 ko | bedrock2/deps/coqutil/src/Map/Properties
0m05.62s | 535096 ko | Kami/Ex/ProcThreeStage
0m05.56s | 507520 ko | Kami/Decomposition
0m05.12s | 505436 ko | Kami/Amortization
0m05.07s | 561800 ko | Kami/Ex/SCMMInl
0m04.71s | 470712 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_I_system
0m04.46s | 468412 ko | bedrock2/deps/riscv-coq/src/Proofs/invert_encode_U
0m04.19s | 509168 ko | Kami/ParametricInline
0m04.13s | 512264 ko | Kami/Ex/ProcDec
0m03.88s | 478956 ko | bedrock2/bedrock2/src/Examples/swap
0m03.81s | 510132 ko | Kami/Ex/SC
0m03.64s | 472892 ko | bedrock2/bedrock2/src/FE310CSemantics
0m03.39s | 517872 ko | Kami/Tutorial
0m03.30s | 510956 ko | bedrock2/compiler/src/examples/Fibonacci
0m03.17s | 486656 ko | Kami/Label
0m03.17s | 492768 ko | Kami/ModuleBoundEx
0m03.10s | 492424 ko | Kami/ParametricEquiv
0m03.06s | 499932 ko | Kami/Wf
0m02.50s | 505076 ko | bedrock2/compiler/src/Pipeline
0m02.42s | 526316 ko | Kami/Ex/ProcFDInv
0m02.42s | 489812 ko | Kami/ParamDup
0m02.39s | 487424 ko | Kami/Duplicate
0m02.19s | 489072 ko | Kami/ParametricWf
0m02.11s | 508168 ko | Kami/Ex/ProcFetchDecode
0m02.06s | 465924 ko | bedrock2/bedrock2/src/Examples/ARPResponder
0m01.94s | 494008 ko | Kami/MapReifyEx
0m01.89s | 479116 ko | Kami/Syntax
0m01.88s | 521816 ko | Kami/Ex/IsaRv32/PgmGcd
0m01.87s | 522776 ko | Kami/Ex/IsaRv32/PgmBankerWorker1
0m01.87s | 519908 ko | Kami/Ex/IsaRv32/PgmMatMulReport
0m01.85s | 520188 ko | Kami/Ex/IsaRv32/PgmBankerWorker3
0m01.83s | 524584 ko | Kami/Ex/IsaRv32/PgmDekker2
0m01.83s | 522312 ko | Kami/Ex/IsaRv32/PgmFact
0m01.83s | 519240 ko | Kami/Ex/IsaRv32/PgmMatMulNormal1
0m01.81s | 522124 ko | Kami/Ex/IsaRv32/PgmBankerInit
0m01.81s | 521416 ko | Kami/Ex/IsaRv32/PgmMatMulInit
0m01.81s | 519724 ko | Kami/Ex/IsaRv32/PgmMatMulNormal2
0m01.81s | 495792 ko | Kami/Ex/RegFile
0m01.80s | 520460 ko | Kami/Ex/IsaRv32/PgmBankerWorker2
0m01.80s | 519680 ko | Kami/Ex/IsaRv32/PgmPeterson1
0m01.80s | 519696 ko | Kami/Ex/IsaRv32/PgmPeterson2
0m01.80s | 461200 ko | bedrock2/bedrock2/src/ptsto_bytes
0m01.78s | 520604 ko | Kami/Ex/IsaRv32/PgmDekker1
0m01.78s | 495196 ko | Kami/Ex/ProcDecInv
0m01.76s | 433996 ko | bedrock2/bedrock2/src/Map/SeparationLogic
0m01.75s | 521896 ko | Kami/Ex/IsaRv32/PgmBsort
0m01.74s | 522080 ko | Kami/Ex/IsaRv32/PgmHanoi
0m01.70s | 490720 ko | Kami/Ex/NativeFifo
0m01.52s | 429812 ko | Kami/Lib/NatLib
0m01.51s | 473632 ko | bedrock2/processor/src/Test
0m01.48s | 476176 ko | Kami/SymEval
0m01.47s | 497260 ko | Kami/Ex/MemAtomic
0m01.44s | 498104 ko | Kami/Ex/ProcThreeStInv
0m01.35s | 457132 ko | bedrock2/bedrock2/src/Array
0m01.34s | 461368 ko | bedrock2/bedrock2/src/TailRecursion
0m01.30s | 509008 ko | Kami/Ex/IsaRv32
0m01.29s | 485936 ko | Kami/ModuleBound
0m01.29s | 418180 ko | bedrock2/bedrock2/src/Byte
0m01.25s | 435736 ko | bedrock2/bedrock2/src/Examples/chacha20
0m01.19s | 495240 ko | Kami/Ex/ProcThreeStDec
0m01.18s | 457564 ko | bedrock2/bedrock2/src/Scalars
0m01.17s | 444076 ko | bedrock2/deps/riscv-coq/src/Utility/ListLib
0m01.15s | 487776 ko | Kami/Ex/OneEltFifo
0m01.14s | 449412 ko | bedrock2/bedrock2/src/Examples/Trace
0m01.13s | 457912 ko | bedrock2/bedrock2/src/TODO_absint
0m01.10s | 419492 ko | bedrock2/compiler/lib/LibTactics
0m01.08s | 421756 ko | Kami/Lib/StringAsList
0m01.00s | 442912 ko | bedrock2/deps/coqutil/src/Z/ZLib
0m00.99s | 435576 ko | Kami/Lib/Struct
0m00.98s | 426872 ko | bedrock2/compiler/src/examples/toposort
0m00.95s | 441452 ko | bedrock2/deps/riscv-coq/src/Utility/prove_Zeq_bitwise
0m00.94s | 450352 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncodeProver
0m00.94s | 454504 ko | bedrock2/deps/riscv-coq/src/Spec/ExecuteI
0m00.93s | 493232 ko | Kami/Ex/ProcDecSC
0m00.92s | 550756 ko | Kami/Ex/IsaRv32PgmExt
0m00.90s | 421100 ko | Kami/Lib/Indexer
0m00.89s | 484828 ko | Kami/Tactics
0m00.88s | 427540 ko | bedrock2/compiler/src/util/ListLib
0m00.87s | 460284 ko | Kami/Notations
0m00.84s | 443020 ko | bedrock2/bedrock2/src/Memory
0m00.83s | 526908 ko | Kami/Ex/ProcFDCorrect
0m00.83s | 439724 ko | bedrock2/deps/riscv-coq/src/Utility/ZBitOps
0m00.82s | 507796 ko | Kami/Ex/IsaRv32Pgm
0m00.82s | 422368 ko | Kami/Lib/ilist
0m00.81s | 488468 ko | Kami/Ex/ProcDecSCN
0m00.81s | 439216 ko | bedrock2/deps/coqutil/src/Z/BitOps
0m00.80s | 527136 ko | Kami/Ex/ProcFourStDec
0m00.80s | 499980 ko | bedrock2/compiler/src/examples/EditDistExample
0m00.79s | 477872 ko | Kami/Ext/BSyntax
0m00.79s | 488532 ko | Kami/Ext/Extraction
0m00.77s | 486708 ko | Kami/ParametricInlineLtac
0m00.76s | 409784 ko | bedrock2/deps/riscv-coq/src/Platform/Example64Literal
0m00.76s | 459200 ko | bedrock2/deps/riscv-coq/src/Spec/MetricPrimitives
0m00.75s | 490144 ko | Kami/Ex/ProcThreeStInl
0m00.74s | 485920 ko | Kami/Kami
0m00.74s | 501084 ko | bedrock2/compiler/src/examples/CompileExamples
0m00.74s | 505316 ko | bedrock2/compiler/src/examples/swap_bytes_over_uart_hexdump
0m00.74s | 460380 ko | bedrock2/deps/riscv-coq/src/Platform/MinimalLogging
0m00.72s | 473852 ko | Kami/Substitute
0m00.72s | 458732 ko | bedrock2/compiler/src/examples/TestExprImp
0m00.72s | 457772 ko | bedrock2/deps/riscv-coq/src/Spec/Primitives
0m00.71s | 452980 ko | Kami/Ex/MemTypes
0m00.71s | 483356 ko | bedrock2/compiler/src/examples/InlineAssemblyMacro
0m00.71s | 459820 ko | bedrock2/compiler/src/examples/TestFlatImp
0m00.71s | 449484 ko | bedrock2/deps/riscv-coq/src/Platform/Memory
0m00.71s | 446048 ko | bedrock2/deps/riscv-coq/src/Spec/Decode
0m00.70s | 469696 ko | Kami/Inline
0m00.70s | 423260 ko | Kami/Lib/StringAsOT
0m00.69s | 466532 ko | bedrock2/compiler/src/FlatToRiscvDef
0m00.68s | 447424 ko | bedrock2/compiler/src/Rem4
0m00.67s | 474056 ko | Kami/SymEvalTac
0m00.67s | 446424 ko | bedrock2/compiler/src/SimplWordExpr
0m00.67s | 446648 ko | bedrock2/deps/riscv-coq/src/Utility/Encode
0m00.66s | 441912 ko | bedrock2/bedrock2/src/Semantics
0m00.63s | 420276 ko | Kami/Lib/StringStringAsOT
0m00.63s | 426168 ko | bedrock2/deps/coqutil/src/Datatypes/PropSet
0m00.61s | 446012 ko | bedrock2/compiler/src/UnmappedMemForExtSpec
0m00.61s | 357880 ko | bedrock2/deps/riscv-coq/src/Utility/Monads
0m00.60s | 426440 ko | bedrock2/deps/coqutil/src/Map/SortedList
0m00.59s | 442252 ko | Kami/Synthesize
0m00.59s | 371952 ko | bedrock2/compiler/src/util/Common
0m00.59s | 440596 ko | bedrock2/deps/coqutil/src/Map/SortedListWord
0m00.58s | 415316 ko | bedrock2/deps/coqutil/src/Word/Naive
0m00.58s | 408744 ko | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet_Run
0m00.57s | 403188 ko | bedrock2/bedrock2/src/BasicC64Semantics
0m00.57s | 358716 ko | bedrock2/deps/riscv-coq/src/Utility/Utility
0m00.56s | 432120 ko | Kami/Lib/WordSupport
0m00.56s | 410516 ko | bedrock2/bedrock2/src/WeakestPrecondition
0m00.55s | 413664 ko | Kami/Lib/StringEq
0m00.55s | 387552 ko | bedrock2/bedrock2/src/BasicC32Semantics
0m00.55s | 420416 ko | bedrock2/compiler/src/examples/highlevel/FuncMut
0m00.55s | 401008 ko | bedrock2/deps/riscv-coq/src/Spec/ExecuteI64
0m00.55s | 376020 ko | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl32
0m00.54s | 310296 ko | bedrock2/bedrock2/src/Examples/MultipleReturnValues
0m00.53s | 386872 ko | bedrock2/compiler/src/RegAlloc2
0m00.53s | 387416 ko | bedrock2/deps/riscv-coq/src/Spec/ExecuteM
0m00.52s | 371960 ko | bedrock2/bedrock2/src/ProgramLogic
0m00.52s | 374676 ko | bedrock2/deps/riscv-coq/src/Platform/Run
0m00.52s | 375816 ko | bedrock2/deps/riscv-coq/src/Spec/ExecuteM64
0m00.52s | 375840 ko | bedrock2/deps/riscv-coq/src/Utility/DefaultMemImpl64
0m00.52s | 346660 ko | bedrock2/deps/riscv-coq/src/Utility/Words32Naive
0m00.50s | 322924 ko | bedrock2/bedrock2/src/BasicCSyntax
0m00.50s | 385968 ko | bedrock2/compiler/src/Basic32Semantics
0m00.50s | 389304 ko | bedrock2/compiler/src/RegAlloc3
0m00.49s | 411496 ko | bedrock2/bedrock2/src/BytedumpTest
0m00.49s | 411496 ko | bedrock2/bedrock2/src/BytedumpTestα
0m00.49s | 365272 ko | bedrock2/deps/coqutil/src/Map/Z_keyed_SortedListMap
0m00.49s | 375808 ko | bedrock2/deps/riscv-coq/src/Spec/Machine
0m00.49s | 360632 ko | bedrock2/deps/riscv-coq/src/Utility/MkMachineWidth
0m00.49s | 346980 ko | bedrock2/deps/riscv-coq/src/Utility/Words64Naive
0m00.48s | 276676 ko | bedrock2/bedrock2/src/ToCString
0m00.48s | 352200 ko | bedrock2/compiler/src/SeparationLogic
0m00.48s | 375156 ko | bedrock2/deps/coqutil/src/Decidable
0m00.48s | 362608 ko | bedrock2/deps/riscv-coq/src/Platform/MetricRiscvMachine
0m00.48s | 370692 ko | bedrock2/deps/riscv-coq/src/Platform/RiscvMachine
0m00.47s | 321560 ko | bedrock2/bedrock2/src/BasicC64Syntax
0m00.47s | 338992 ko | bedrock2/deps/riscv-coq/src/Spec/PseudoInstructions
0m00.46s | 351756 ko | bedrock2/compiler/src/ZNameGen
0m00.46s | 344552 ko | bedrock2/deps/riscv-coq/src/Platform/MetricLogging
0m00.45s | 350576 ko | bedrock2/compiler/src/RegAllocAnnotatedNotations
0m00.45s | 358800 ko | bedrock2/processor/src/KamiWord
0m00.44s | 305528 ko | bedrock2/deps/coqutil/src/Map/SortedListString_test
0m00.44s | 321736 ko | bedrock2/deps/coqutil/src/Tactics/Tactics
0m00.44s | 336624 ko | bedrock2/deps/riscv-coq/src/Spec/Execute
0m00.44s | 340268 ko | bedrock2/deps/riscv-coq/src/Utility/InstructionNotations
0m00.43s | 289244 ko | bedrock2/bedrock2/src/Map/Separation
0m00.43s | 362292 ko | bedrock2/compiler/src/RiscvWordProperties
0m00.43s | 321032 ko | bedrock2/deps/riscv-coq/src/Spec/VirtualMemory
0m00.43s | 313976 ko | bedrock2/deps/riscv-coq/src/Utility/InstructionCoercions
0m00.42s | 374624 ko | bedrock2/deps/riscv-coq/src/Proofs/DecodeEncode
0m00.40s | 282384 ko | bedrock2/compiler/src/util/Tactics
0m00.40s | 323944 ko | bedrock2/deps/coqutil/src/Map/Interface
0m00.39s | 303504 ko | bedrock2/deps/coqutil/src/Z/HexNotation
0m00.38s | 319992 ko | Kami/Lib/CommonTactics
0m00.38s | 363832 ko | Kami/Lib/Nomega
0m00.38s | 294268 ko | bedrock2/bedrock2/src/ZNamesSyntax
0m00.37s | 316400 ko | bedrock2/deps/coqutil/src/Map/Funext
0m00.37s | 295668 ko | bedrock2/deps/riscv-coq/src/Utility/div_mod_to_quot_rem
0m00.36s | 271052 ko | Kami/Ex/Names
0m00.36s | 338456 ko | Kami/Lib/Concat
0m00.36s | 272052 ko | bedrock2/bedrock2/src/string2ident
0m00.36s | 298624 ko | bedrock2/compiler/src/Simp
0m00.36s | 312496 ko | bedrock2/deps/coqutil/src/Map/Solver
0m00.36s | 298516 ko | bedrock2/deps/riscv-coq/src/Utility/nat_div_mod_to_quot_rem
0m00.35s | 299684 ko | Kami/Lib/Misc
0m00.35s | 272888 ko | bedrock2/bedrock2/src/Examples/StructAccess
0m00.35s | 267768 ko | bedrock2/bedrock2/src/StructNotations
0m00.35s | 295952 ko | bedrock2/deps/coqutil/src/Map/Empty_set_keyed_map
0m00.35s | 289456 ko | bedrock2/deps/coqutil/src/Map/SortedListString
0m00.34s | 328692 ko | Kami/Lib/Reflection
0m00.34s | 272812 ko | bedrock2/bedrock2/src/Bytedump
0m00.34s | 294376 ko | bedrock2/deps/riscv-coq/src/Utility/Tactics
0m00.33s | 301112 ko | bedrock2/bedrock2/src/NotationsCustomEntry
0m00.33s | 289700 ko | bedrock2/compiler/src/util/MyOmega
0m00.32s | 274924 ko | bedrock2/bedrock2/src/Hexdump
0m00.32s | 286108 ko | bedrock2/compiler/src/NameGen
0m00.31s | 301996 ko | bedrock2/compiler/lib/LibTacticsMin
0m00.30s | 252388 ko | bedrock2/bedrock2/src/StringNamesSyntax
0m00.30s | 282580 ko | bedrock2/compiler/src/util/Set
0m00.30s | 290132 ko | bedrock2/compiler/src/util/SetSolverTests
0m00.29s | 252176 ko | bedrock2/deps/coqutil/src/Datatypes/String
0m00.27s | 227732 ko | bedrock2/deps/coqutil/src/Word/LittleEndian
0m00.27s | 255852 ko | bedrock2/deps/riscv-coq/src/Utility/MonadTests
0m00.26s | 238732 ko | bedrock2/deps/coqutil/src/Z/div_mod_to_equations
0m00.23s | 212520 ko | bedrock2/deps/riscv-coq/src/Utility/MonadT
0m00.19s | 172428 ko | bedrock2/bedrock2/src/NotationsInConstr
0m00.19s | 180476 ko | bedrock2/deps/coqutil/src/Datatypes/HList
0m00.17s | 180940 ko | Kami/Lib/VectorFacts
0m00.17s | 184664 ko | bedrock2/deps/riscv-coq/src/Utility/JMonad
0m00.14s | 160816 ko | Kami/Lib/DepEq
0m00.13s | 142092 ko | Kami/Lib/FinNotations
0m00.13s | 144616 ko | bedrock2/bedrock2/src/ListPred
0m00.13s | 149744 ko | bedrock2/bedrock2/src/Variables
0m00.13s | 142420 ko | bedrock2/deps/coqutil/src/Datatypes/List
0m00.12s | 146976 ko | bedrock2/deps/riscv-coq/src/Utility/MonadNotations
0m00.09s | 116312 ko | bedrock2/bedrock2/src/Lift1Prop
0m00.09s | 108600 ko | bedrock2/deps/coqutil/src/Datatypes/Option
0m00.09s | 93184 ko | bedrock2/deps/coqutil/src/Datatypes/Prod
0m00.07s | 87856 ko | Kami/Lib/BasicLogic
0m00.07s | 93508 ko | bedrock2/bedrock2/src/Syntax
0m00.06s | 76484 ko | Kami/Lib/DepEqNat
0m00.06s | 67708 ko | bedrock2/deps/coqutil/src/Macros/symmetry
0m00.05s | 56680 ko | bedrock2/compiler/lib/fiat_crypto_tactics/Not
0m00.05s | 70976 ko | bedrock2/compiler/src/util/Misc
0m00.05s | 65768 ko | bedrock2/deps/riscv-coq/src/Utility/PowerFunc
0m00.05s | 65120 ko | bedrock2/deps/riscv-coq/src/Utility/runsToNonDet
0m00.04s | 57444 ko | bedrock2/bedrock2/src/Markers
0m00.04s | 56396 ko | bedrock2/bedrock2/src/Notations
0m00.04s | 55660 ko | bedrock2/compiler/lib/fiat_crypto_tactics/Test
0m00.04s | 57340 ko | bedrock2/compiler/lib/fiat_crypto_tactics/UniquePose
0m00.04s | 57364 ko | bedrock2/compiler/src/NoActionSyntaxParams
0m00.04s | 56364 ko | bedrock2/compiler/src/eqexact
0m00.04s | 55764 ko | bedrock2/compiler/src/examples/highlevel/For
0m00.04s | 56680 ko | bedrock2/compiler/src/on_hyp_containing
0m00.04s | 58420 ko | bedrock2/compiler/src/util/Learning
0m00.04s | 56232 ko | bedrock2/deps/coqutil/src/Datatypes/PrimitivePair
0m00.04s | 54100 ko | bedrock2/deps/coqutil/src/Macros/subst
0m00.04s | 54384 ko | bedrock2/deps/coqutil/src/Macros/unique
0m00.04s | 55016 ko | bedrock2/deps/coqutil/src/Tactics/eabstract
0m00.04s | 55296 ko | bedrock2/deps/coqutil/src/Tactics/letexists
0m00.04s | 54916 ko | bedrock2/deps/coqutil/src/Tactics/rdelta
0m00.04s | 56184 ko | bedrock2/deps/coqutil/src/Tactics/syntactic_unify
0m00.04s | 54440 ko | bedrock2/deps/coqutil/src/dlet
0m00.04s | 54804 ko | bedrock2/deps/coqutil/src/sanity
0m00.04s | 56096 ko | bedrock2/deps/riscv-coq/src/Utility/MMIOTrace
0m00.03s | 54716 ko | bedrock2/compiler/src/util/LogGoal
|
