Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
With Coq-8.15.0-OCaml-4.14.0-transparent-rooster-noht-tb-nops-schedutil-haswell
<details><summary>Timing Diff</summary>
<p>
```
Time | Peak Mem | File Name
-----------------------------------------------------------------------------------------------------------------
217m05.57s | 5261276 ko | Total Time / Peak Mem
-----------------------------------------------------------------------------------------------------------------
10m12.13s | 5261276 ko | Bedrock/End2End/X25519/GarageDoor.vo
7m16.76s | 2072424 ko | Curves/Weierstrass/AffineProofs.vo
5m25.01s | 2720684 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo
4m36.85s | 1002592 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
4m22.66s | 966788 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo
4m15.66s | 2534848 ko | Assembly/WithBedrock/Proofs.vo
4m13.18s | 4060544 ko | Curves/EdwardsMontgomery.vo
3m17.19s | 1652800 ko | Rewriter/Passes/ArithWithCasts.vo
3m13.39s | 2906972 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
3m11.56s | 807652 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo
3m03.06s | 1447868 ko | Curves/Weierstrass/Projective.vo
2m55.14s | 1448832 ko | Curves/Montgomery/XZProofs.vo
2m43.25s | 1609372 ko | Rewriter/Passes/NBE.vo
2m42.82s | 1440664 ko | Curves/Montgomery/AffineProofs.vo
2m40.23s | 1130088 ko | Fancy/Compiler.vo
2m16.73s | 1527808 ko | Rewriter/Passes/ToFancyWithCasts.vo
2m14.55s | 1144932 ko | Rewriter/Rewriter/Wf.vo
2m05.77s | 2752144 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo
1m58.84s | 1028352 ko | fiat-rust/src/p384_scalar_32.rs
1m57.21s | 1084716 ko | fiat-json/src/p384_32.json
1m57.12s | 1134892 ko | fiat-java/src/FiatP384Scalar.java
1m56.93s | 1052888 ko | fiat-bedrock2/src/p384_scalar_32.c
1m56.87s | 1430232 ko | Bedrock/Field/Synthesis/Examples/X25519_64.vo
1m56.81s | 940076 ko | fiat-c/src/p384_scalar_32.c
1m56.62s | 900848 ko | AbstractInterpretation/Wf.vo
1m56.60s | 1013960 ko | fiat-rust/src/p384_32.rs
1m55.87s | 928076 ko | fiat-java/src/FiatP384.java
1m54.12s | 1085840 ko | fiat-bedrock2/src/p384_32.c
1m53.75s | 1109764 ko | fiat-go/32/p384/p384.go
1m52.74s | 1014028 ko | fiat-zig/src/p384_32.zig
1m52.35s | 1016136 ko | fiat-c/src/p384_32.c
1m51.91s | 1586240 ko | Bedrock/End2End/X25519/Field25519.vo
1m50.34s | 2118952 ko | Fancy/Barrett256.vo
1m48.32s | 1071548 ko | fiat-json/src/p384_scalar_32.json
1m47.61s | 1026564 ko | fiat-go/32/p384scalar/p384scalar.go
1m44.72s | 1108040 ko | fiat-zig/src/p384_scalar_32.zig
1m35.98s | 871244 ko | Util/FSets/FMapTrie.vo
1m30.50s | 1488160 ko | Assembly/EquivalenceProofs.vo
1m26.18s | 1933828 ko | SlowPrimeSynthesisExamples.vo
1m26.17s | 435096 ko | Spec/Test/X25519.vo
1m22.54s | 746764 ko | rupicola/bedrock2/compiler/src/compiler/MMIO.vo
1m20.86s | 596052 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo
1m18.14s | 1122748 ko | UnsaturatedSolinasHeuristics/Tests.vo
1m15.95s | 1571688 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo
1m10.41s | 801800 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo
1m09.28s | 1398964 ko | Assembly/WithBedrock/SymbolicProofs.vo
1m05.65s | 1729084 ko | Bedrock/Field/Synthesis/Examples/p224_64.vo
1m05.17s | 1692264 ko | Bedrock/Field/Synthesis/Examples/p256_64.vo
1m04.96s | 948932 ko | Curves/Weierstrass/Jacobian.vo
1m04.27s | 728228 ko | Rewriter/Language/UnderLetsProofs.vo
1m01.34s | 932300 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo
0m59.65s | 851776 ko | AbstractInterpretation/ZRangeProofs.vo
0m59.48s | 631996 ko | rupicola/bedrock2/compiler/src/compiler/Spilling.vo
0m58.82s | 997964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo
0m58.72s | 735644 ko | AbstractInterpretation/Proofs.vo
0m58.44s | 1028636 ko | Rewriter/Passes/MultiRetSplit.vo
0m57.56s | 696180 ko | Rewriter/RulesProofs.vo
0m55.78s | 1041296 ko | Rewriter/Rewriter/Examples.vo
0m55.51s | 1414976 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo
0m55.27s | 1093640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo
0m53.41s | 897680 ko | Rewriter/Rewriter/InterpProofs.vo
0m52.70s | 641944 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo
0m51.92s | 936052 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo
0m50.61s | 1000796 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LiveVerif/swap.vo
0m49.65s | 1117392 ko | Rewriter/Passes/Arith.vo
0m49.57s | 790532 ko | Rewriter/Rewriter/ProofsCommon.vo
0m48.83s | 1096396 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo
0m47.72s | 580056 ko | Demo.vo
0m47.51s | 1676808 ko | Fancy/Montgomery256.vo
0m44.93s | 576568 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo
0m42.35s | 1025324 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo
0m41.43s | 1799488 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
0m40.66s | 1797864 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
0m38.33s | 1473660 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
0m38.02s | 1457308 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
0m37.04s | 1622556 ko | ExtractionOCaml/word_by_word_montgomery
0m35.95s | 1622420 ko | ExtractionOCaml/unsaturated_solinas
0m35.40s | 657656 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo
0m35.20s | 920532 ko | Rewriter/Passes/MulSplit.vo
0m34.66s | 1414824 ko | ExtractionOCaml/bedrock2_saturated_solinas
0m34.51s | 1414836 ko | ExtractionOCaml/bedrock2_base_conversion
0m34.23s | 1414996 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
0m34.03s | 1414936 ko | ExtractionOCaml/with_bedrock2_base_conversion
0m33.39s | 1485396 ko | Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo
0m32.89s | 1313536 ko | Assembly/Symbolic.vo
0m32.56s | 1379176 ko | Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo
0m32.27s | 1414416 ko | ExtractionOCaml/base_conversion
0m32.05s | 1414056 ko | ExtractionOCaml/saturated_solinas
0m31.85s | 606620 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo
0m31.80s | 1235756 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo
0m31.21s | 1154960 ko | PushButtonSynthesis/UnsaturatedSolinas.vo
0m30.89s | 927256 ko | Rewriter/Rewriter/Examples/PrefixSums.vo
0m30.74s | 527504 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo
0m29.60s | 2068968 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
0m29.43s | 2068908 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
0m28.97s | 1413148 ko | ExtractionOCaml/perf_word_by_word_montgomery
0m28.95s | 656404 ko | rupicola/src/Rupicola/Examples/Utf8/Utf8.vo
0m28.49s | 680996 ko | Rewriter/Language/Wf.vo
0m28.23s | 1413340 ko | ExtractionOCaml/perf_unsaturated_solinas
0m27.71s | 1957748 ko | ExtractionOCaml/word_by_word_montgomery.ml
0m27.31s | 1999600 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
0m26.96s | 1187532 ko | Bedrock/Field/Synthesis/Examples/LadderStep.vo
0m26.79s | 498920 ko | Arithmetic/Saturated.vo
0m26.31s | 1999460 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
0m25.47s | 1909160 ko | ExtractionOCaml/unsaturated_solinas.ml
0m25.31s | 1136428 ko | PushButtonSynthesis/WordByWordMontgomery.vo
0m24.29s | 1923348 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
0m24.25s | 1923312 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
0m24.22s | 1922696 ko | ExtractionOCaml/bedrock2_base_conversion.ml
0m24.07s | 883440 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo
0m23.83s | 804672 ko | Bedrock/Field/Translation/Proofs/Expr.vo
0m23.50s | 1922688 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
0m23.41s | 1330528 ko | Bedrock/End2End/RupicolaCrypto/Low.vo
0m23.11s | 673152 ko | rupicola/bedrock2/compiler/src/compiler/FlatImp.vo
0m22.70s | 1807096 ko | ExtractionOCaml/saturated_solinas.ml
0m22.60s | 1808704 ko | ExtractionOCaml/base_conversion.ml
0m21.51s | 1241680 ko | StandaloneDebuggingExamples.vo
0m21.24s | 1129532 ko | Bedrock/Field/Synthesis/Examples/X1305_32.vo
0m20.63s | 750492 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo
0m20.50s | 694900 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.vo
0m20.22s | 618820 ko | Util/FSets/FMapBool.vo
0m19.12s | 1168800 ko | Bedrock/End2End/RupicolaCrypto/Derive.vo
0m19.06s | 1740448 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
0m19.04s | 183824 ko | fiat-bedrock2/src/secp256k1_scalar_32.c
0m18.74s | 1127704 ko | Bedrock/Field/Translation/Proofs/Cmd.vo
0m18.73s | 151320 ko | fiat-go/64/p434/p434.go
0m18.72s | 623428 ko | Util/FSets/FMapProd.vo
0m18.54s | 173804 ko | fiat-json/src/p434_64.json
0m18.38s | 149204 ko | fiat-rust/src/p434_64.rs
0m18.26s | 1098916 ko | Bedrock/Field/Translation/Proofs/Func.vo
0m18.25s | 1767996 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
0m18.22s | 219348 ko | fiat-bedrock2/src/p256_scalar_32.c
0m18.14s | 154956 ko | fiat-c/src/p434_64.c
0m18.11s | 575464 ko | Rewriter/Language/Inversion.vo
0m17.78s | 224112 ko | fiat-bedrock2/src/secp256k1_32.c
0m17.72s | 210576 ko | fiat-bedrock2/src/curve25519_scalar_32.c
0m17.58s | 532192 ko | Arithmetic/WordByWordMontgomery.vo
0m17.51s | 151244 ko | fiat-bedrock2/src/p434_64.c
0m17.50s | 1098944 ko | Bedrock/End2End/Poly1305/Field1305.vo
0m17.47s | 562084 ko | Util/FSets/FMapSum.vo
0m17.46s | 186200 ko | fiat-go/32/p256scalar/p256scalar.go
0m17.36s | 231444 ko | fiat-java/src/FiatSecp256K1Scalar.java
0m17.32s | 825688 ko | Curves/Edwards/XYZT/Basic.vo
0m17.31s | 527196 ko | rupicola/src/Rupicola/Examples/KVStore/Manual.vo
0m17.30s | 1170992 ko | Bedrock/Field/Synthesis/New/Signature.vo
0m17.29s | 224328 ko | fiat-zig/src/secp256k1_32.zig
0m17.21s | 216684 ko | fiat-java/src/FiatP256Scalar.java
0m17.17s | 194264 ko | fiat-go/32/secp256k1scalar/secp256k1scalar.go
0m17.17s | 270480 ko | fiat-json/src/secp256k1_scalar_32.json
0m17.16s | 131808 ko | fiat-zig/src/p434_64.zig
0m17.06s | 178772 ko | fiat-zig/src/p256_scalar_32.zig
0m17.04s | 616824 ko | Util/ZUtil/ArithmeticShiftr.vo
0m17.03s | 213084 ko | fiat-rust/src/secp256k1_32.rs
0m17.02s | 218628 ko | fiat-zig/src/secp256k1_scalar_32.zig
0m17.00s | 223588 ko | fiat-java/src/FiatSecp256K1.java
0m17.00s | 223244 ko | fiat-rust/src/secp256k1_scalar_32.rs
0m16.96s | 223260 ko | fiat-rust/src/p256_scalar_32.rs
0m16.92s | 191004 ko | fiat-c/src/p256_scalar_32.c
0m16.90s | 223148 ko | fiat-go/32/curve25519scalar/curve25519scalar.go
0m16.81s | 242052 ko | fiat-json/src/curve25519_scalar_32.json
0m16.77s | 207016 ko | fiat-c/src/secp256k1_scalar_32.c
0m16.76s | 492964 ko | rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo
0m16.75s | 223528 ko | fiat-rust/src/curve25519_scalar_32.rs
0m16.73s | 224220 ko | fiat-bedrock2/src/p256_32.c
0m16.70s | 757508 ko | Language/IdentifiersGENERATED.vo
0m16.64s | 264428 ko | fiat-json/src/p256_scalar_32.json
0m16.61s | 215196 ko | fiat-json/src/p256_32.json
0m16.52s | 219336 ko | fiat-go/32/p256/p256.go
0m16.46s | 223452 ko | fiat-zig/src/curve25519_scalar_32.zig
0m16.39s | 215968 ko | fiat-zig/src/p256_32.zig
0m16.38s | 245448 ko | fiat-json/src/secp256k1_32.json
0m16.35s | 194332 ko | fiat-c/src/secp256k1_32.c
0m16.29s | 224252 ko | fiat-go/32/secp256k1/secp256k1.go
0m16.22s | 734940 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo
0m16.15s | 574264 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo
0m16.12s | 1113680 ko | Assembly/Parse/TestAsm.vo
0m16.09s | 206844 ko | fiat-java/src/FiatP256.java
0m16.01s | 181176 ko | fiat-rust/src/p256_32.rs
0m15.91s | 1903988 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs
0m15.87s | 724204 ko | Curves/Edwards/AffineProofs.vo
0m15.87s | 1903904 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs
0m15.87s | 216764 ko | fiat-java/src/FiatCurve25519Scalar.java
0m15.73s | 211304 ko | fiat-c/src/p256_32.c
0m15.66s | 515552 ko | Arithmetic/BarrettReduction.vo
0m15.64s | 222876 ko | fiat-c/src/curve25519_scalar_32.c
0m15.47s | 422064 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/TestGoals.vo
0m15.44s | 1828560 ko | ExtractionHaskell/word_by_word_montgomery.hs
0m15.24s | 1858344 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs
0m15.23s | 513560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo
0m15.22s | 460028 ko | Algebra/Field.vo
0m14.97s | 524376 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
0m14.81s | 563976 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo
0m14.72s | 485888 ko | Arithmetic/Core.vo
0m14.63s | 561164 ko | Util/FSets/FMapOption.vo
0m14.60s | 1758712 ko | ExtractionHaskell/unsaturated_solinas.hs
0m14.44s | 1858416 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs
0m14.40s | 485672 ko | rupicola/src/Rupicola/Examples/Arrays.vo
0m14.37s | 591088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo
0m14.33s | 458092 ko | Util/Structures/Orders/Prod.vo
0m14.31s | 494256 ko | rupicola/src/Rupicola/Examples/CMove/CMove.vo
0m14.17s | 601156 ko | Bedrock/Field/Common/Util.vo
0m14.17s | 1811448 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs
0m14.15s | 1811484 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs
0m14.12s | 1737052 ko | ExtractionHaskell/saturated_solinas.hs
0m14.11s | 1795228 ko | ExtractionHaskell/bedrock2_base_conversion.hs
0m14.06s | 486664 ko | rupicola/src/Rupicola/Examples/Loops.vo
0m14.00s | 670832 ko | Bedrock/Group/AdditionChains.vo
0m13.82s | 591028 ko | Language/IdentifiersGENERATEDProofs.vo
0m13.46s | 1795324 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs
0m13.34s | 1668244 ko | ExtractionHaskell/base_conversion.hs
0m13.30s | 537068 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo
0m13.24s | 1046976 ko | PushButtonSynthesis/SmallExamples.vo
0m13.11s | 659764 ko | Bedrock/Group/ScalarMult/LadderStep.vo
0m13.09s | 483044 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SepAutoArrayTests.vo
0m12.89s | 481820 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo
0m12.36s | 636972 ko | Rewriter/Demo.vo
0m12.20s | 735328 ko | Util/ZRange/LandLorBounds.vo
0m11.74s | 103264 ko | fiat-bedrock2/src/p384_scalar_64.c
0m11.73s | 1622576 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo
0m11.45s | 541116 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo
0m11.44s | 651768 ko | rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo
0m11.41s | 98044 ko | fiat-go/64/p384scalar/p384scalar.go
0m11.24s | 110568 ko | fiat-json/src/p384_scalar_64.json
0m11.23s | 594984 ko | Stringification/IR.vo
0m11.14s | 98128 ko | fiat-rust/src/p384_scalar_64.rs
0m11.00s | 90372 ko | fiat-c/src/p384_scalar_64.c
0m10.99s | 1284108 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo
0m10.93s | 614628 ko | Bedrock/Field/Translation/Proofs/Flatten.vo
0m10.80s | 99248 ko | fiat-zig/src/p384_scalar_64.zig
0m10.79s | 503152 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo
0m10.78s | 473188 ko | Primitives/MxDHRepChange.vo
0m10.75s | 741856 ko | Assembly/Syntax.vo
0m10.60s | 456828 ko | Util/Structures/Orders/List.vo
0m10.46s | 450624 ko | Algebra/Ring.vo
0m10.36s | 1001632 ko | PushButtonSynthesis/BaseConversion.vo
0m09.86s | 557840 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo
0m09.82s | 99184 ko | fiat-bedrock2/src/p384_64.c
0m09.80s | 142228 ko | fiat-bedrock2/src/p224_32.c
0m09.80s | 549460 ko | rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo
0m09.75s | 91820 ko | fiat-go/64/p384/p384.go
0m09.70s | 135000 ko | fiat-json/src/p224_32.json
0m09.54s | 92000 ko | fiat-rust/src/p384_64.rs
0m09.50s | 132800 ko | fiat-java/src/FiatP224.java
0m09.46s | 653844 ko | Bedrock/Group/ScalarMult/CSwap.vo
0m09.46s | 506320 ko | Rewriter/Language/IdentifiersLibraryProofs.vo
0m09.37s | 1020956 ko | PushButtonSynthesis/Primitives.vo
0m09.36s | 865720 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo
0m09.33s | 134492 ko | fiat-rust/src/p224_32.rs
0m09.30s | 104276 ko | fiat-json/src/p384_64.json
0m09.29s | 119988 ko | fiat-zig/src/p224_32.zig
0m09.27s | 90684 ko | fiat-c/src/p384_64.c
0m09.27s | 142488 ko | fiat-go/32/p224/p224.go
0m09.07s | 88600 ko | fiat-zig/src/p384_64.zig
0m09.00s | 494776 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI.vo
0m08.82s | 597092 ko | Language/IdentifiersBasicGENERATED.vo
0m08.62s | 138364 ko | fiat-c/src/p224_32.c
0m08.52s | 106696 ko | fiat-json/src/p448_solinas_32.json
0m08.50s | 581828 ko | PushButtonSynthesis/BYInversionReificationCache.vo
0m08.44s | 582600 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo
0m08.26s | 960340 ko | BoundsPipeline.vo
0m08.25s | 915244 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo
0m08.24s | 654160 ko | Util/FSets/FMapTrieEx.vo
0m08.18s | 50048 ko | fiat-zig/src/p448_solinas_32.zig
0m08.18s | 481300 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.vo
0m08.16s | 458180 ko | rupicola/src/Rupicola/Examples/KVStore/Automated.vo
0m08.02s | 779672 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo
0m08.00s | 49540 ko | fiat-c/src/p448_solinas_32.c
0m07.80s | 50080 ko | fiat-rust/src/p448_solinas_32.rs
0m07.78s | 464228 ko | Util/ZRange/CornersMonotoneBounds.vo
0m07.53s | 469368 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo
0m07.48s | 1065652 ko | Bedrock/Field/Synthesis/Examples/EncodeDecode.vo
0m07.23s | 518084 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.vo
0m07.02s | 468896 ko | rupicola/src/Rupicola/Examples/L64X128.vo
0m06.95s | 464568 ko | Util/ListUtil.vo
0m06.94s | 437656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo
0m06.84s | 455668 ko | rupicola/src/Rupicola/Examples/Expr.vo
0m06.79s | 464808 ko | Arithmetic/FancyMontgomeryReduction.vo
0m06.77s | 1013476 ko | PushButtonSynthesis/BarrettReduction.vo
0m06.75s | 542464 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo
0m06.69s | 566244 ko | Rewriter/Passes/NoSelect.vo
0m06.66s | 475500 ko | rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo
0m06.51s | 702456 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo
0m06.47s | 481220 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/bsearch.vo
0m06.36s | 455648 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo
0m06.32s | 455644 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo
0m06.23s | 456448 ko | Rewriter/Util/ListUtil.vo
0m06.23s | 470824 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo
0m06.21s | 1068400 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo
0m06.19s | 900864 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo
0m06.08s | 481440 ko | Util/ZUtil/Modulo.vo
0m05.98s | 459748 ko | Util/MSets/MSetSum.vo
0m05.93s | 671196 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo
0m05.76s | 459516 ko | rupicola/bedrock2/compiler/src/compiler/ExprImp.vo
0m05.74s | 466072 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo
0m05.71s | 661996 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo
0m05.69s | 451720 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FlatConstMem.vo
0m05.68s | 482496 ko | rupicola/bedrock2/compiler/src/compiler/EmitsValid.vo
0m05.56s | 530728 ko | Fancy/Prod.vo
0m05.53s | 576848 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo
0m05.51s | 500584 ko | Arithmetic/BYInv.vo
0m05.51s | 1017016 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo
0m05.47s | 1051320 ko | Bedrock/Field/Synthesis/Examples/MulTwice.vo
0m05.35s | 544092 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo
0m05.28s | 469276 ko | rupicola/src/Rupicola/Lib/Loops.vo
0m05.15s | 459452 ko | Util/FsatzAutoLemmas.vo
0m05.13s | 490540 ko | COperationSpecifications.vo
0m05.05s | 551944 ko | Language/InversionExtra.vo
0m05.00s | 430368 ko | Spec/Curve25519.vo
0m04.96s | 457264 ko | rupicola/src/Rupicola/Examples/CRC32/CRC32.vo
0m04.86s | 499464 ko | Curves/Edwards/Pre.vo
0m04.77s | 453980 ko | Util/FSets/FMapIso.vo
0m04.74s | 434740 ko | Arithmetic/MontgomeryReduction/Proofs.vo
0m04.74s | 998948 ko | PushButtonSynthesis/SaturatedSolinas.vo
0m04.72s | 613908 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo
0m04.72s | 1036088 ko | CLI.vo
0m04.52s | 458800 ko | Util/FSets/FMapSect.vo
0m04.52s | 463872 ko | Util/ZRange/BasicLemmas.vo
0m04.42s | 441476 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo
0m04.40s | 441320 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo
0m04.35s | 442008 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add.vo
0m04.32s | 548684 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo
0m04.30s | 442520 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo
0m04.26s | 474496 ko | Algebra/Field_test.vo
0m04.24s | 469296 ko | Rewriter/Language/IdentifiersBasicLibrary.vo
0m04.23s | 1035172 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo
0m04.17s | 442600 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo
0m04.13s | 469776 ko | rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo
0m04.11s | 34140 ko | fiat-go/64/p521/p521.go
0m04.08s | 458280 ko | UnsaturatedSolinasHeuristics.vo
0m04.04s | 436532 ko | rupicola/src/Rupicola/Examples/Cells/IndirectAdd.vo
0m04.01s | 924828 ko | Assembly/Equivalence.vo
0m03.97s | 458116 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memequal.vo
0m03.87s | 559596 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo
0m03.85s | 483824 ko | Curves/Montgomery/Affine.vo
0m03.74s | 446176 ko | rupicola/src/Rupicola/Examples/Uppercase.vo
0m03.70s | 606268 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo
0m03.68s | 454304 ko | CastLemmas.vo
0m03.66s | 451728 ko | Arithmetic/BarrettReduction/Generalized.vo
0m03.63s | 40652 ko | fiat-bedrock2/src/p521_64.c
0m03.63s | 433604 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo
0m03.60s | 412004 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SlowGoals.vo
0m03.59s | 452800 ko | Arithmetic/UniformWeight.vo
0m03.44s | 445992 ko | Util/ZUtil/LandLorBounds.vo
0m03.43s | 392728 ko | Algebra/Group.vo
0m03.41s | 449716 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memswap.vo
0m03.39s | 440256 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo
0m03.36s | 447124 ko | rupicola/src/Rupicola/Examples/Arithmetic.vo
0m03.35s | 979616 ko | Bedrock/Field/Translation/Cmd.vo
0m03.35s | 422232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo
0m03.33s | 443044 ko | Util/ZUtil/LandLorShiftBounds.vo
0m03.27s | 445992 ko | Arithmetic/BarrettReduction/HAC.vo
0m03.27s | 432564 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo
0m03.24s | 436396 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo
0m03.23s | 1047460 ko | Rewriter/PerfTesting/Core.vo
0m03.17s | 28152 ko | fiat-rust/src/p521_64.rs
0m03.16s | 442160 ko | rupicola/src/Rupicola/Examples/RevComp.vo
0m03.14s | 447236 ko | Util/Structures/Orders.vo
0m03.13s | 26548 ko | fiat-c/src/p521_64.c
0m03.10s | 45808 ko | fiat-bedrock2/src/p256_scalar_64.c
0m03.07s | 532612 ko | Rewriter/Passes/AddAssocLeft.vo
0m03.03s | 977664 ko | Bedrock/Field/Translation/Func.vo
0m03.03s | 44604 ko | fiat-bedrock2/src/secp256k1_scalar_64.c
0m03.01s | 1048452 ko | Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo
0m03.00s | 541084 ko | PushButtonSynthesis/BaseConversionReificationCache.vo
0m03.00s | 40520 ko | fiat-json/src/p521_64.json
0m02.99s | 465048 ko | MiscCompilerPassesProofs.vo
0m02.96s | 515800 ko | Rewriter/Passes/Test.vo
0m02.96s | 431820 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo
0m02.95s | 29800 ko | fiat-zig/src/p521_64.zig
0m02.92s | 672252 ko | Bedrock/Group/ScalarMult/ScalarMult.vo
0m02.92s | 426316 ko | Util/Structures/Orders/Option.vo
0m02.90s | 1022712 ko | Bedrock/Field/Stringification/Stringification.vo
0m02.90s | 411140 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo
0m02.90s | 1044812 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
0m02.83s | 1041236 ko | Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo
0m02.83s | 40984 ko | fiat-go/64/p256scalar/p256scalar.go
0m02.83s | 40136 ko | fiat-go/64/secp256k1scalar/secp256k1scalar.go
0m02.81s | 463212 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI_live.vo
0m02.81s | 426692 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo
0m02.80s | 437392 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ipow.vo
0m02.76s | 1031416 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo
0m02.75s | 36912 ko | fiat-rust/src/secp256k1_scalar_64.rs
0m02.74s | 43424 ko | fiat-json/src/p256_scalar_64.json
0m02.73s | 44380 ko | fiat-bedrock2/src/secp256k1_64.c
0m02.73s | 46692 ko | fiat-json/src/secp256k1_scalar_64.json
0m02.73s | 40144 ko | fiat-rust/src/p256_scalar_64.rs
0m02.72s | 616588 ko | Bedrock/Field/Interface/Compilation2.vo
0m02.72s | 1060852 ko | Bedrock/Standalone/StandaloneOCamlMain.vo
0m02.72s | 40940 ko | fiat-zig/src/p256_scalar_64.zig
0m02.72s | 36540 ko | fiat-zig/src/secp256k1_scalar_64.zig
0m02.70s | 440668 ko | Arithmetic/Primitives.vo
0m02.69s | 34376 ko | fiat-go/64/p448solinas/p448solinas.go
0m02.69s | 441296 ko | rupicola/src/Rupicola/Examples/IO/Echo.vo
0m02.67s | 1017728 ko | Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo
0m02.66s | 38816 ko | fiat-c/src/p256_scalar_64.c
0m02.65s | 39184 ko | fiat-c/src/secp256k1_scalar_64.c
0m02.64s | 423828 ko | Util/ZUtil/ZSimplify/Autogenerated.vo
0m02.63s | 543028 ko | Bedrock/Field/Translation/Expr.vo
0m02.63s | 423108 ko | Util/Bool/Reflect.vo
0m02.63s | 444224 ko | rupicola/src/Rupicola/Lib/Core.vo
0m02.61s | 1035052 ko | StandaloneOCamlMain.vo
0m02.61s | 434480 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo
0m02.60s | 1028068 ko | Bedrock/Field/Synthesis/Generic/Operation.vo
0m02.60s | 1024824 ko | Bedrock/Field/Synthesis/Specialized/Tactics.vo
0m02.58s | 1038520 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo
0m02.56s | 1060612 ko | Bedrock/Standalone/StandaloneHaskellMain.vo
0m02.55s | 986832 ko | Bedrock/Field/Translation/Parameters/FE310.vo
0m02.55s | 39316 ko | fiat-bedrock2/src/curve25519_scalar_64.c
0m02.54s | 1025016 ko | Bedrock/Field/Synthesis/Generic/Tactics.vo
0m02.54s | 546288 ko | Util/FSets/FMapTrie/ShapeEx.vo
0m02.54s | 50932 ko | fiat-json/src/secp256k1_64.json
0m02.53s | 448436 ko | Util/MSets/MSetIso.vo
0m02.52s | 535292 ko | Rewriter/Passes/FlattenThunkedRects.vo
0m02.51s | 423264 ko | Rewriter/Util/Bool/Reflect.vo
0m02.50s | 1034624 ko | StandaloneHaskellMain.vo
0m02.50s | 440728 ko | rupicola/src/Rupicola/Examples/DownTo.vo
0m02.49s | 41252 ko | fiat-go/64/secp256k1/secp256k1.go
0m02.48s | 466816 ko | Util/ZUtil/Morphisms.vo
0m02.47s | 984164 ko | Bedrock/Field/Translation/Parameters/Defaults.vo
0m02.47s | 986788 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo
0m02.47s | 986744 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo
0m02.46s | 444920 ko | rupicola/src/Rupicola/Examples/LinkedList/Find.vo
0m02.45s | 39832 ko | fiat-rust/src/secp256k1_64.rs
0m02.43s | 42408 ko | fiat-bedrock2/src/p448_solinas_64.c
0m02.42s | 459260 ko | rupicola/bedrock2/compiler/src/compiler/Pipeline.vo
0m02.40s | 39704 ko | fiat-c/src/secp256k1_64.c
0m02.40s | 43164 ko | fiat-json/src/curve25519_scalar_64.json
0m02.40s | 435272 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/rpmul.vo
0m02.39s | 38408 ko | fiat-go/64/curve25519scalar/curve25519scalar.go
0m02.39s | 41528 ko | fiat-zig/src/secp256k1_64.zig
0m02.35s | 459832 ko | Spec/MontgomeryCurve.vo
0m02.34s | 439088 ko | Util/ZUtil/Shift.vo
0m02.33s | 427068 ko | Util/ZUtil/TwosComplement.vo
0m02.32s | 37540 ko | fiat-zig/src/curve25519_scalar_64.zig
0m02.27s | 454376 ko | Arithmetic/Freeze.vo
0m02.26s | 39660 ko | fiat-c/src/curve25519_scalar_64.c
0m02.25s | 592276 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo
0m02.25s | 444148 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo
0m02.24s | 41588 ko | fiat-bedrock2/src/curve25519_32.c
0m02.22s | 38600 ko | fiat-rust/src/curve25519_scalar_64.rs
0m02.21s | 456920 ko | rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo
0m02.10s | 45040 ko | fiat-bedrock2/src/p224_64.c
0m02.08s | 26264 ko | fiat-go/32/curve25519/curve25519.go
0m02.04s | 454084 ko | Arithmetic/BaseConversion.vo
0m02.04s | 387496 ko | Util/Wf2.vo
0m02.04s | 42584 ko | fiat-bedrock2/src/p256_64.c
0m02.00s | 541216 ko | Stringification/Language.vo
0m02.00s | 26940 ko | fiat-zig/src/p448_solinas_64.zig
0m01.99s | 429952 ko | Util/ZUtil/ModInv.vo
0m01.99s | 441364 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memconst.vo
0m01.97s | 40088 ko | fiat-json/src/p448_solinas_64.json
0m01.97s | 414464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo
0m01.96s | 437900 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder_live.vo
0m01.94s | 432696 ko | Util/ZUtil/Testbit.vo
0m01.94s | 26908 ko | fiat-rust/src/p448_solinas_64.rs
0m01.93s | 38160 ko | fiat-go/64/p256/p256.go
0m01.91s | 449192 ko | Curves/TableMult/TableMult.vo
0m01.90s | 46628 ko | fiat-json/src/p224_64.json
0m01.89s | 40776 ko | fiat-go/64/p224/p224.go
0m01.88s | 428304 ko | Util/ZUtil/Div.vo
0m01.88s | 46516 ko | fiat-json/src/p256_64.json
0m01.86s | 40220 ko | fiat-json/src/curve25519_32.json
0m01.86s | 36540 ko | fiat-rust/src/p224_64.rs
0m01.84s | 417332 ko | Util/ListUtil/Forall.vo
0m01.84s | 26408 ko | fiat-c/src/p448_solinas_64.c
0m01.83s | 535736 ko | Rewriter/Passes/StripLiteralCasts.vo
0m01.83s | 25660 ko | fiat-zig/src/curve25519_32.zig
0m01.82s | 632940 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo
0m01.82s | 36624 ko | fiat-c/src/p224_64.c
0m01.82s | 451524 ko | rupicola/src/Rupicola/Lib/Arrays.vo
0m01.81s | 533880 ko | Rewriter/Passes/UnfoldValueBarrier.vo
0m01.80s | 430840 ko | Arithmetic/BarrettReduction/RidiculousFish.vo
0m01.80s | 27820 ko | fiat-java/src/FiatCurve25519.java
0m01.79s | 41736 ko | fiat-zig/src/p256_64.zig
0m01.79s | 436900 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo
0m01.78s | 42492 ko | fiat-rust/src/p256_64.rs
0m01.78s | 37828 ko | fiat-zig/src/p224_64.zig
0m01.78s | 424064 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo
0m01.75s | 25776 ko | fiat-rust/src/curve25519_32.rs
0m01.74s | 451940 ko | Arithmetic/ModOps.vo
0m01.74s | 434256 ko | Util/Tuple.vo
0m01.74s | 447092 ko | rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo
0m01.72s | 39840 ko | fiat-c/src/p256_64.c
0m01.71s | 26564 ko | fiat-c/src/curve25519_32.c
0m01.70s | 431084 ko | rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo
0m01.69s | 472052 ko | Assembly/Parse.vo
0m01.68s | 442980 ko | Util/FSets/FMapFacts.vo
0m01.66s | 443780 ko | Arithmetic/ModularArithmeticTheorems.vo
0m01.66s | 584544 ko | CompilersTestCases.vo
0m01.65s | 603032 ko | Bedrock/Field/Common/Names/MakeNames.vo
0m01.65s | 531068 ko | Rewriter/Passes/ToFancy.vo
0m01.59s | 510048 ko | AbstractInterpretation/AbstractInterpretation.vo
0m01.59s | 428844 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo
0m01.54s | 459460 ko | Util/FSets/FMapUnit.vo
0m01.51s | 516024 ko | AbstractInterpretation/ZRange.vo
0m01.50s | 433684 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo
0m01.49s | 443820 ko | rupicola/src/Rupicola/Examples/Nondeterminism/StackAlloc.vo
0m01.47s | 428160 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo
0m01.47s | 436180 ko | rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo
0m01.46s | 409824 ko | Rewriter/Util/ListUtil/Forall.vo
0m01.45s | 536264 ko | Stringification/Go.vo
0m01.43s | 454408 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo
0m01.43s | 450476 ko | rupicola/bedrock2/compiler/src/compiler/FitsStack.vo
0m01.43s | 433224 ko | rupicola/src/Rupicola/Examples/Conditionals.vo
0m01.42s | 420152 ko | Algebra/ScalarMult.vo
0m01.41s | 408824 ko | Coqprime/Z/Pmod.vo
0m01.41s | 413016 ko | Util/ZUtil/Rshi.vo
0m01.40s | 459592 ko | rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo
0m01.40s | 410608 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo
0m01.39s | 435088 ko | Spec/WeierstrassCurve.vo
0m01.37s | 446388 ko | Util/ZRange/SplitRangeBounds.vo
0m01.37s | 432816 ko | Util/ZUtil/Pow2Mod.vo
0m01.37s | 424576 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FrameRule.vo
0m01.37s | 435384 ko | rupicola/src/Rupicola/Lib/InlineTables.vo
0m01.35s | 433820 ko | Util/ZUtil/TruncatingShiftl.vo
0m01.35s | 428028 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo
0m01.34s | 450632 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo
0m01.33s | 414076 ko | Util/ListUtil/StdlibCompat.vo
0m01.32s | 454524 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo
0m01.32s | 424344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo
0m01.31s | 411512 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo
0m01.30s | 436368 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Impl.vo
0m01.28s | 467212 ko | Rewriter/Language/IdentifiersLibrary.vo
0m01.28s | 435744 ko | rupicola/src/Rupicola/Lib/Compiler.vo
0m01.27s | 409364 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo
0m01.26s | 438180 ko | Util/ZUtil/Bitwise.vo
0m01.26s | 423264 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo
0m01.25s | 623484 ko | Bedrock/Specs/Field.vo
0m01.22s | 438248 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponderProofs.vo
0m01.19s | 437148 ko | Util/ZUtil/Quot.vo
0m01.18s | 443560 ko | Arithmetic/Partition.vo
0m01.18s | 466532 ko | Arithmetic/PrimeFieldTheorems.vo
0m01.18s | 429872 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo
0m01.14s | 443184 ko | Util/ZRange/SplitBounds.vo
0m01.11s | 475504 ko | Rewriter/Rewriter/Reify.vo
0m01.10s | 601768 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo
0m01.10s | 465820 ko | Rewriter/Rewriter/Rewriter.vo
0m01.10s | 407124 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo
0m01.09s | 532408 ko | Stringification/JSON.vo
0m01.09s | 419140 ko | Util/ZUtil/AddGetCarry.vo
0m01.08s | 431204 ko | rupicola/src/Rupicola/Examples/Cells/Swap.vo
0m01.07s | 416912 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo
0m01.05s | 594808 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo
0m01.05s | 535932 ko | Bedrock/Field/Translation/LoadStoreList.vo
0m01.03s | 438440 ko | Curves/Edwards/XYZT/Precomputed.vo
0m01.03s | 358112 ko | Util/Wf1.vo
0m01.02s | 446996 ko | Fancy/Spec.vo
0m01.01s | 440072 ko | rupicola/src/Rupicola/Examples/LinkedList/LinkedList.vo
0m00.99s | 410348 ko | Coqprime/PrimalityTest/EGroup.vo
0m00.99s | 424208 ko | Util/ZUtil/OnesFrom.vo
0m00.97s | 535348 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo
0m00.97s | 536592 ko | Stringification/C.vo
0m00.96s | 433792 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ArrayLoadStore.vo
0m00.96s | 439972 ko | rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo
0m00.95s | 412692 ko | Rewriter/Util/NatUtil.vo
0m00.95s | 531716 ko | Stringification/Java.vo
0m00.95s | 418692 ko | Util/NatUtil.vo
0m00.95s | 431852 ko | Util/ZUtil/Ones.vo
0m00.94s | 406912 ko | Coqprime/PrimalityTest/LucasLehmer.vo
0m00.94s | 440968 ko | rupicola/src/Rupicola/Examples/Nondeterminism/Peek.vo
0m00.92s | 587240 ko | Bedrock/Field/Common/Tactics.vo
0m00.91s | 532372 ko | Stringification/Zig.vo
0m00.90s | 405552 ko | Coqprime/Z/ZCAux.vo
0m00.90s | 531844 ko | Stringification/Rust.vo
0m00.90s | 423268 ko | Util/Strings/ParseArithmetic.vo
0m00.89s | 613116 ko | Bedrock/Group/Point.vo
0m00.87s | 424344 ko | Curves/Montgomery/AffineInstances.vo
0m00.87s | 488780 ko | Rewriter/Rewriter/AllTactics.vo
0m00.87s | 427288 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ArrayCasts.vo
0m00.85s | 553924 ko | Util/FSets/FMapZ.vo
0m00.84s | 611944 ko | Bedrock/Field/Interface/Representation.vo
0m00.84s | 432084 ko | Util/Structures/Orders/Sum.vo
0m00.84s | 383216 ko | rupicola/bedrock2/bedrock2/src/bedrock2/StringdumpDemo.vo
0m00.83s | 408144 ko | Coqprime/PrimalityTest/Pocklington.vo
0m00.83s | 444896 ko | Rewriter/Language/Language.vo
0m00.81s | 431008 ko | rupicola/src/Rupicola/Examples/Cells/Incr.vo
0m00.79s | 534280 ko | Bedrock/Field/Common/Types.vo
0m00.79s | 536312 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo
0m00.79s | 431668 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalNoMul.vo
0m00.78s | 448596 ko | Assembly/Equality.vo
0m00.78s | 418604 ko | Util/Strings/String_as_OT.vo
0m00.78s | 421204 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo
0m00.77s | 518616 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo
0m00.77s | 541264 ko | Bedrock/Field/Stringification/FlattenVarData.vo
0m00.77s | 532564 ko | Bedrock/Field/Translation/Flatten.vo
0m00.77s | 532900 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo
0m00.77s | 503348 ko | Language/APINotations.vo
0m00.77s | 423948 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListIndexNotations.vo
0m00.77s | 416776 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo
0m00.76s | 408684 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo
0m00.76s | 431672 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap.vo
0m00.75s | 431404 ko | Arithmetic/BarrettReduction/Wikipedia.vo
0m00.75s | 431596 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc.vo
0m00.75s | 440648 ko | rupicola/src/Rupicola/Examples/IO/Stdout.vo
0m00.74s | 524552 ko | Util/FSets/FMapN.vo
0m00.74s | 440356 ko | rupicola/src/Rupicola/Examples/Tree/Tree.vo
0m00.73s | 379628 ko | Rewriter/Util/Decidable.vo
0m00.73s | 414332 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo
0m00.73s | 440844 ko | rupicola/src/Rupicola/Examples/IO/IO.vo
0m00.72s | 440384 ko | Util/NumTheoryUtil.vo
0m00.71s | 437168 ko | Rewriter/Rules.vo
0m00.71s | 325128 ko | Util/PartiallyReifiedProp.vo
0m00.71s | 442668 ko | rupicola/src/Rupicola/Lib/ExprCompiler.vo
0m00.70s | 407580 ko | Coqprime/PrimalityTest/PGroup.vo
0m00.70s | 544704 ko | Rewriter/All.vo
0m00.70s | 379600 ko | Util/Decidable.vo
0m00.70s | 421208 ko | Util/ErrorT/List.vo
0m00.69s | 457056 ko | Rewriter/Language/IdentifiersGenerate.vo
0m00.69s | 442496 ko | rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo
0m00.67s | 408356 ko | Coqprime/PrimalityTest/Root.vo
0m00.67s | 499400 ko | Rewriter/AllTacticsExtra.vo
0m00.67s | 457660 ko | Util/FSets/FMapEmpty.vo
0m00.67s | 453476 ko | Util/FSets/FMapFlip.vo
0m00.67s | 425748 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Trace.vo
0m00.66s | 450304 ko | Bedrock/Group/Loops.vo
0m00.66s | 409852 ko | Coqprime/PrimalityTest/Cyclic.vo
0m00.66s | 499060 ko | Language/WfExtra.vo
0m00.66s | 500704 ko | MiscCompilerPassesProofsExtra.vo
0m00.66s | 408568 ko | Util/OptionList.vo
0m00.66s | 25272 ko | fiat-go/64/curve25519/curve25519.go
0m00.65s | 499192 ko | Language/UnderLetsProofsExtra.vo
0m00.64s | 482340 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo
0m00.64s | 420624 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo
0m00.63s | 503652 ko | AbstractInterpretation/WfExtra.vo
0m00.63s | 419648 ko | Algebra/IntegralDomain.vo
0m00.63s | 417516 ko | Algebra/SubsetoidRing.vo
0m00.63s | 440092 ko | Util/MSets/MSetN.vo
0m00.62s | 458040 ko | Rewriter/Language/IdentifiersGenerateProofs.vo
0m00.61s | 509812 ko | Language/API.vo
0m00.61s | 471452 ko | Rewriter/Rewriter/ProofsCommonTactics.vo
0m00.61s | 480356 ko | Rewriter/Util/plugins/RewriterBuild.vo
0m00.61s | 443020 ko | Util/Structures/OrdersEx.vo
0m00.61s | 412924 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo
0m00.60s | 441384 ko | Util/QUtil.vo
0m00.60s | 415140 ko | Util/Strings/ParseArithmeticToTaps.vo
0m00.60s | 417372 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/DisjointUnion.vo
0m00.59s | 407660 ko | Coqprime/Z/ZSum.vo
0m00.59s | 509704 ko | PushButtonSynthesis/ReificationCache.vo
0m00.59s | 412944 ko | Util/Structures/Orders/Flip.vo
0m00.58s | 428728 ko | Util/Arg.vo
0m00.58s | 420844 ko | Util/CPSUtil.vo
0m00.58s | 28232 ko | fiat-bedrock2/src/curve25519_64.c
0m00.58s | 440700 ko | rupicola/src/Rupicola/Examples/KVStore/Properties.vo
0m00.58s | 439868 ko | rupicola/src/Rupicola/Lib/SepLocals.vo
0m00.57s | 424584 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo
0m00.57s | 434968 ko | rupicola/src/Rupicola/Lib/NoExprReflection.vo
0m00.56s | 455576 ko | MiscCompilerPasses.vo
0m00.56s | 436956 ko | Util/ZRange/OperationsBounds.vo
0m00.56s | 430704 ko | Util/ZUtil/CC.vo
0m00.56s | 412736 ko | Util/ZUtil/Modulo/PullPush.vo
0m00.55s | 440124 ko | rupicola/src/Rupicola/Lib/ExprReflection.vo
0m00.54s | 458908 ko | ArithmeticCPS/Freeze.vo
0m00.54s | 479240 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo
0m00.53s | 480148 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo
0m00.53s | 423756 ko | Util/Decidable/Decidable2Bool.vo
0m00.53s | 434128 ko | Util/FSets/FMapTrie/Shape.vo
0m00.53s | 409360 ko | Util/Loops.vo
0m00.53s | 432392 ko | Util/ZUtil/Stabilization.vo
0m00.52s | 449280 ko | ArithmeticCPS/Saturated.vo
0m00.52s | 462080 ko | ArithmeticCPS/WordByWordMontgomery.vo
0m00.52s | 28072 ko | fiat-json/src/curve25519_64.json
0m00.52s | 425868 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder.vo
0m00.52s | 420656 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo
0m00.51s | 410920 ko | Coqprime/PrimalityTest/Zp.vo
0m00.51s | 409288 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo
0m00.50s | 413552 ko | Util/Structures/Orders/Bool.vo
0m00.50s | 422380 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo
0m00.50s | 425588 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/chacha20.vo
0m00.50s | 411832 ko | rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo
0m00.50s | 410504 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo
0m00.49s | 453760 ko | ArithmeticCPS/ModOps.vo
0m00.49s | 357724 ko | Util/Wf.vo
0m00.49s | 413560 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/OperatorOverloading.vo
0m00.49s | 428648 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo
0m00.48s | 433632 ko | Util/ZUtil/Lxor.vo
0m00.48s | 392392 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo
0m00.48s | 432316 ko | rupicola/src/Rupicola/Examples/Swap/Properties.vo
0m00.47s | 448480 ko | Bedrock/Specs/Group.vo
0m00.47s | 450912 ko | Util/MSets/MSetPositive/Show.vo
0m00.47s | 425988 ko | Util/ZUtil/Log2.vo
0m00.47s | 21964 ko | fiat-zig/src/curve25519_64.zig
0m00.47s | 429056 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo
0m00.47s | 412540 ko | rupicola/bedrock2/compiler/src/compiler/NaiveRiscvWordProperties.vo
0m00.47s | 417224 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo
0m00.47s | 433216 ko | rupicola/src/Rupicola/Lib/SepReflection.vo
0m00.46s | 409804 ko | Util/ListUtil/SetoidListFlatMap.vo
0m00.46s | 431544 ko | Util/ZUtil/Land.vo
0m00.46s | 22420 ko | fiat-c/src/curve25519_64.c
0m00.46s | 409344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo
0m00.46s | 414456 ko | rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo
0m00.46s | 432048 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpSepLog.vo
0m00.46s | 421344 ko | rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo
0m00.46s | 402892 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo
0m00.46s | 440140 ko | rupicola/src/Rupicola/Examples/Cells/Cells.vo
0m00.45s | 473492 ko | Bedrock/End2End/RupicolaCrypto/Spec.vo
0m00.45s | 417460 ko | rupicola/bedrock2/compiler/src/compiler/Registers.vo
0m00.45s | 419340 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo
0m00.45s | 348172 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo
0m00.45s | 435316 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo
0m00.45s | 435004 ko | rupicola/src/Rupicola/Lib/Alloc.vo
0m00.44s | 405980 ko | Coqprime/Z/ZCmisc.vo
0m00.44s | 441160 ko | Rewriter/Language/IdentifiersBasicGenerate.vo
0m00.44s | 429536 ko | Util/ZUtil/EquivModulo.vo
0m00.44s | 22420 ko | fiat-rust/src/curve25519_64.rs
0m00.44s | 408516 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo
0m00.44s | 408884 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo
0m00.43s | 458904 ko | ArithmeticCPS/BaseConversion.vo
0m00.43s | 446844 ko | ArithmeticCPS/Core.vo
0m00.43s | 419368 ko | Util/HList.vo
0m00.43s | 424220 ko | Util/ZBounded.vo
0m00.42s | 381596 ko | Rewriter/Util/Sum.vo
0m00.42s | 420832 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo
0m00.42s | 400060 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoExports.vo
0m00.42s | 424000 ko | rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo
0m00.42s | 414788 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo
0m00.42s | 404484 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo
0m00.42s | 440948 ko | rupicola/src/Rupicola/Examples/IO/Writer.vo
0m00.42s | 409360 ko | rupicola/src/Rupicola/Lib/ToCString.vo
0m00.41s | 467072 ko | Arithmetic/FLia.vo
0m00.41s | 409704 ko | Language/IdentifierParameters.vo
0m00.41s | 399776 ko | Rewriter/TestRules.vo
0m00.41s | 427872 ko | Util/Strings/NamingConventions.vo
0m00.41s | 426876 ko | Util/Strings/Show.vo
0m00.41s | 435292 ko | Util/ZUtil/SignBit.vo
0m00.41s | 428856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo
0m00.41s | 418792 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo
0m00.41s | 441724 ko | rupicola/src/Rupicola/Examples/Utf8/Utils.vo
0m00.41s | 436020 ko | rupicola/src/Rupicola/Lib/Conditionals.vo
0m00.40s | 465652 ko | Assembly/WithBedrock/Semantics.vo
0m00.40s | 382880 ko | Coqprime/List/UList.vo
0m00.40s | 391340 ko | Util/Strings/String_as_OT_old.vo
0m00.40s | 426724 ko | rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo
0m00.40s | 457948 ko | rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo
0m00.40s | 440268 ko | rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo
0m00.40s | 440244 ko | rupicola/src/Rupicola/Examples/KVStore/KVStore.vo
0m00.39s | 428756 ko | Arithmetic/ModularArithmeticPre.vo
0m00.39s | 410320 ko | Util/Strings/String.vo
0m00.39s | 417104 ko | Util/ZUtil/Ltz.vo
0m00.39s | 427696 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo
0m00.38s | 421440 ko | Util/Level.vo
0m00.38s | 418448 ko | Util/Structures/Equalities/List.vo
0m00.38s | 348752 ko | Util/ZUtil/Tactics/SolveRange.vo
0m00.38s | 425508 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo
0m00.38s | 410772 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Demos.vo
0m00.38s | 433904 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo
0m00.38s | 419664 ko | rupicola/src/Rupicola/Examples/KVStore/kv.vo
0m00.38s | 364632 ko | rupicola/src/Rupicola/Lib/Api.vo
0m00.37s | 420136 ko | Spec/CompleteEdwardsCurve.vo
0m00.37s | 411032 ko | Util/ListUtil/GroupAllBy.vo
0m00.37s | 427452 ko | Util/ZUtil/Divide.vo
0m00.37s | 339212 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCallsExports.vo
0m00.37s | 419544 ko | rupicola/bedrock2/compiler/src/compiler/util/Result.vo
0m00.37s | 413692 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo
0m00.37s | 364452 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo
0m00.37s | 402824 ko | rupicola/src/Rupicola/Examples/CRC32/Table.vo
0m00.36s | 389748 ko | Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.vo
0m00.36s | 424724 ko | Rewriter/Language/Reify.vo
0m00.36s | 362152 ko | Util/ZUtil.vo
0m00.36s | 348296 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc_empty_post.vo
0m00.36s | 398640 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo
0m00.36s | 403944 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo
0m00.35s | 390560 ko | Language/PreExtra.vo
0m00.35s | 360968 ko | Rewriter/TestRulesProofs.vo
0m00.35s | 423576 ko | Util/ZUtil/Pow.vo
0m00.35s | 410008 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo
0m00.35s | 414704 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo
0m00.35s | 424564 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo
0m00.35s | 424864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo
0m00.35s | 372704 ko | rupicola/src/Rupicola/Examples/KVStore/Tactics.vo
0m00.35s | 441192 ko | rupicola/src/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
0m00.35s | 353312 ko | rupicola/src/Rupicola/Lib/WordNotations.vo
0m00.34s | 406604 ko | Coqprime/PrimalityTest/Euler.vo
0m00.34s | 372748 ko | Util/Strings/Sorting.vo
0m00.34s | 350800 ko | Util/ZUtil/Lor.vo
0m00.34s | 340528 ko | Util/ZUtil/Tactics/Ztestbit.vo
0m00.34s | 349404 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo
0m00.34s | 344916 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo
0m00.34s | 423288 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo
0m00.33s | 382496 ko | Coqprime/List/Permutation.vo
0m00.33s | 406240 ko | Coqprime/PrimalityTest/IGroup.vo
0m00.33s | 405116 ko | Coqprime/PrimalityTest/Lagrange.vo
0m00.33s | 421400 ko | Curves/Weierstrass/Affine.vo
0m00.33s | 389044 ko | Rewriter/Language/UnderLets.vo
0m00.33s | 425536 ko | Util/Listable.vo
0m00.33s | 381812 ko | Util/Sum.vo
0m00.33s | 345844 ko | Util/ZUtil/Tactics/SolveTestbit.vo
0m00.33s | 373512 ko | rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo
0m00.33s | 393652 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
0m00.33s | 418268 ko | rupicola/src/Rupicola/Lib/Monads.vo
0m00.32s | 371836 ko | Rewriter/Util/MSetPositive/Facts.vo
0m00.32s | 423832 ko | Util/ZRange.vo
0m00.32s | 358420 ko | Util/ZRange/Operations.vo
0m00.32s | 408336 ko | Util/ZUtil/CPS.vo
0m00.32s | 380580 ko | Util/ZUtil/Le.vo
0m00.32s | 394464 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
0m00.31s | 382176 ko | Coqprime/List/ListAux.vo
0m00.31s | 411728 ko | Rewriter/Util/Strings/ParseArithmetic.vo
0m00.31s | 329268 ko | Spec/ModularArithmetic.vo
0m00.31s | 336372 ko | Util/MSets/MSetPositive/Equality.vo
0m00.31s | 380800 ko | Util/Structures/Equalities/Sum.vo
0m00.31s | 374688 ko | Util/Structures/Orders/Unit.vo
0m00.31s | 314968 ko | Util/ZUtil/Tactics.vo
0m00.31s | 25748 ko | fiat-bedrock2/src/poly1305_32.c
0m00.31s | 341504 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo
0m00.31s | 370436 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo
0m00.31s | 414748 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ZList.vo
0m00.31s | 349656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo
0m00.31s | 418368 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo
0m00.31s | 374612 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo
0m00.31s | 370300 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo
0m00.31s | 340412 ko | rupicola/src/Rupicola/Examples/Swap/Swap.vo
0m00.31s | 374668 ko | rupicola/src/Rupicola/Lib/Notations.vo
0m00.30s | 372352 ko | Util/MSets/MSetPositive/Facts.vo
0m00.30s | 362320 ko | Util/ZUtil/Tactics/LtbToLt.vo
0m00.30s | 335556 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo
0m00.30s | 372148 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo
0m00.30s | 297512 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo
0m00.30s | 373100 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo
0m00.30s | 360712 ko | rupicola/src/Rupicola/Lib/Tactics.vo
0m00.29s | 328908 ko | Util/ListUtil/Filter.vo
0m00.29s | 354864 ko | rupicola/bedrock2/bedrock2/src/bedrock2/autorew.vo
0m00.29s | 354492 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo
0m00.28s | 375524 ko | Coqprime/List/ZProgression.vo
0m00.28s | 336268 ko | Rewriter/Util/MSetPositive/Equality.vo
0m00.28s | 367928 ko | Rewriter/Util/Strings/String.vo
0m00.28s | 317768 ko | Util/MSets/Show.vo
0m00.28s | 360040 ko | Util/Structures/Orders/Empty.vo
0m00.28s | 374164 ko | Util/ZUtil/Combine.vo
0m00.28s | 22020 ko | fiat-go/32/poly1305/poly1305.go
0m00.28s | 347760 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo
0m00.28s | 333268 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo
0m00.28s | 379128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo
0m00.28s | 372968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo
0m00.28s | 382844 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo
0m00.28s | 374124 ko | rupicola/src/Rupicola/Lib/Invariants.vo
0m00.27s | 72384 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
0m00.27s | 72384 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
0m00.27s | 73752 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
0m00.27s | 354508 ko | Util/AdditionChainExponentiation.vo
0m00.27s | 346172 ko | Util/ListUtil/SetoidList.vo
0m00.27s | 271932 ko | Util/ZUtil/Modulo/Bootstrap.vo
0m00.27s | 389820 ko | rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo
0m00.27s | 340740 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb_spec.vo
0m00.26s | 330628 ko | Coqprime/PrimalityTest/FGroup.vo
0m00.26s | 73784 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
0m00.26s | 73664 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
0m00.26s | 69800 ko | ExtractionOCaml/word_by_word_montgomery.cmi
0m00.26s | 314236 ko | Rewriter/Util/Option.vo
0m00.26s | 262424 ko | Util/Strings/StringMap.vo
0m00.26s | 336960 ko | Util/Structures/Orders/Iso.vo
0m00.26s | 315264 ko | Util/ZRange/Show.vo
0m00.26s | 287808 ko | Util/ZUtil/N2Z.vo
0m00.26s | 343948 ko | Util/ZUtil/Tactics/RewriteModSmall.vo
0m00.26s | 25372 ko | fiat-json/src/poly1305_32.json
0m00.26s | 284376 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo
0m00.26s | 341840 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo
0m00.26s | 319092 ko | rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo
0m00.26s | 338704 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo
0m00.26s | 334488 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo
0m00.25s | 324388 ko | Arithmetic/MontgomeryReduction/Definition.vo
0m00.25s | 382884 ko | Coqprime/List/Iterator.vo
0m00.25s | 71604 ko | ExtractionOCaml/unsaturated_solinas.cmi
0m00.25s | 73708 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
0m00.25s | 323504 ko | Rewriter/Language/UnderLetsCacheProofs.vo
0m00.25s | 345744 ko | Rewriter/Util/ListUtil/SetoidList.vo
0m00.25s | 317008 ko | Util/ErrorT/Show.vo
0m00.25s | 332768 ko | Util/ListUtil/Permutation.vo
0m00.25s | 313588 ko | Util/Option.vo
0m00.25s | 347564 ko | Util/Structures/Equalities/Prod.vo
0m00.25s | 284664 ko | Util/ZUtil/Definitions.vo
0m00.25s | 378604 ko | Util/ZUtil/Peano.vo
0m00.25s | 317076 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo
0m00.25s | 387984 ko | rupicola/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.vo
0m00.25s | 310356 ko | rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo
0m00.25s | 325000 ko | rupicola/bedrock2/compiler/src/compiler/mod4_0.vo
0m00.25s | 296620 ko | rupicola/bedrock2/compiler/src/compiler/util/Common.vo
0m00.25s | 257832 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth64.vo
0m00.25s | 331524 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo
0m00.25s | 321328 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo
0m00.25s | 300356 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MkMachineWidth.vo
0m00.25s | 407012 ko | rupicola/src/Rupicola/Examples/Assoc/Assoc.vo
0m00.24s | 383060 ko | Algebra/Monoid.vo
0m00.24s | 294572 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo
0m00.24s | 72928 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
0m00.24s | 72840 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
0m00.24s | 294992 ko | Util/ZUtil/MulSplit.vo
0m00.24s | 262100 ko | Util/ZUtil/ZSimplify/Core.vo
0m00.24s | 300420 ko | Util/ZUtil/ZSimplify/Simple.vo
0m00.24s | 350956 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo
0m00.24s | 279620 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfOptionListZ.vo
0m00.24s | 285828 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Z_keyed_SortedListMap.vo
0m00.24s | 297560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo
0m00.24s | 293360 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSR.vo
0m00.24s | 276892 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo
0m00.24s | 293816 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl64.vo
0m00.23s | 69692 ko | ExtractionOCaml/base_conversion.cmi
0m00.23s | 259636 ko | Util/FSets/FMapInterface.vo
0m00.23s | 337476 ko | Util/NUtil/WithoutReferenceToZ.vo
0m00.23s | 262572 ko | Util/SideConditions/RingPackage.vo
0m00.23s | 328020 ko | Util/ZUtil/Tactics/LinearSubstitute.vo
0m00.23s | 314428 ko | Util/ZUtil/Tactics/ZeroBounds.vo
0m00.23s | 297424 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepClause.vo
0m00.23s | 309400 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SoftmulInsts.vo
0m00.23s | 286708 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicRiscvMachine.vo
0m00.23s | 311456 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo
0m00.23s | 304820 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo
0m00.23s | 298136 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo
0m00.22s | 363612 ko | Curves/Montgomery/XZ.vo
0m00.22s | 313284 ko | Util/IdfunWithAlt.vo
0m00.22s | 288884 ko | Util/SideConditions/ModInvPackage.vo
0m00.22s | 288824 ko | Util/Strings/Parse/Common.vo
0m00.22s | 279160 ko | Util/ZUtil/Ge.vo
0m00.22s | 261860 ko | Util/ZUtil/Hints.vo
0m00.22s | 265140 ko | Util/ZUtil/Hints/PullPush.vo
0m00.22s | 260820 ko | Util/ZUtil/Hints/ZArith.vo
0m00.22s | 295136 ko | Util/ZUtil/Nat2Z.vo
0m00.22s | 313108 ko | Util/ZUtil/Opp.vo
0m00.22s | 247464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/Separation.vo
0m00.22s | 294264 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo
0m00.22s | 295576 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/MultipleReturnValues.vo
0m00.22s | 266132 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ToConversion.vo
0m00.22s | 263340 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd.vo
0m00.22s | 259472 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/rewr.vo
0m00.22s | 287464 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo
0m00.22s | 273244 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo
0m00.22s | 259328 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words32Naive.vo
0m00.22s | 259500 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words64Naive.vo
0m00.21s | 68720 ko | ExtractionOCaml/saturated_solinas.cmi
0m00.21s | 261752 ko | PushButtonSynthesis/InvertHighLow.vo
0m00.21s | 307668 ko | Rewriter/Language/PreLemmas.vo
0m00.21s | 275432 ko | Util/ListUtil/SetoidListRev.vo
0m00.21s | 260968 ko | Util/ZUtil/Div/Bootstrap.vo
0m00.21s | 259328 ko | Util/ZUtil/Mul.vo
0m00.21s | 278088 ko | Util/ZUtil/Pow2.vo
0m00.21s | 276496 ko | Util/ZUtil/Sgn.vo
0m00.21s | 269308 ko | Util/ZUtil/Sorting.vo
0m00.21s | 257528 ko | Util/ZUtil/Tactics/DivideExistsMul.vo
0m00.21s | 20792 ko | fiat-c/src/poly1305_32.c
0m00.21s | 21600 ko | fiat-java/src/FiatPoly1305.java
0m00.21s | 21308 ko | fiat-rust/src/poly1305_32.rs
0m00.21s | 249784 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WordSimpl.vo
0m00.21s | 271844 ko | rupicola/bedrock2/bedrock2/src/bedrock2/groundcbv.vo
0m00.21s | 309484 ko | rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo
0m00.21s | 244748 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Inhabited.vo
0m00.21s | 252420 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Empty_set_keyed_map.vo
0m00.21s | 287744 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Interface.vo
0m00.21s | 271712 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo
0m00.21s | 244544 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString.vo
0m00.21s | 259224 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Simp.vo
0m00.21s | 257700 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/Lia.vo
0m00.21s | 267372 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRField.vo
0m00.21s | 277392 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/PseudoInstructions.vo
0m00.21s | 293408 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl32.vo
0m00.20s | 311516 ko | Algebra/Nsatz.vo
0m00.20s | 251672 ko | Rewriter/Util/Strings/Decimal.vo
0m00.20s | 267804 ko | Rewriter/Util/Strings/Parse/Common.vo
0m00.20s | 233024 ko | Util/Decidable/Bool2Prop.vo
0m00.20s | 278904 ko | Util/Factorize.vo
0m00.20s | 261452 ko | Util/ZUtil/Lnot.vo
0m00.20s | 331124 ko | Util/ZUtil/Odd.vo
0m00.20s | 257308 ko | Util/ZUtil/Tactics/CompareToSgn.vo
0m00.20s | 259964 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo
0m00.20s | 258240 ko | Util/ZUtil/Tactics/SplitMinMax.vo
0m00.20s | 303928 ko | Util/ZUtil/Z2Nat.vo
0m00.20s | 21504 ko | fiat-zig/src/poly1305_32.zig
0m00.20s | 300384 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/split_alt.vo
0m00.20s | 325116 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/String.vo
0m00.20s | 327384 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListWord.vo
0m00.20s | 276328 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_word_hints.vo
0m00.20s | 257800 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth32.vo
0m00.20s | 325692 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo
0m00.20s | 255504 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionCoercions.vo
0m00.20s | 285420 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionNotations.vo
0m00.19s | 59572 ko | ExtractionOCaml/perf_word_by_word_montgomer…- Loading branch information
1 parent
186faff
commit 637c7ce