Add generated p434_32 file #1595
Draft
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Ignore p424_32 in the table below, it's from a different version of this
commit.
<details><summary>Timing</summary>
<p>
```
Time | Peak Mem | File Name
-------------------------------------------------------------------------------------------------------------------
254m50.98s | 3857976 ko | Total Time / Peak Mem
-------------------------------------------------------------------------------------------------------------------
9m09.24s | 2340948 ko | Bedrock/End2End/X25519/GarageDoor.vo
6m52.61s | 2067876 ko | Curves/Weierstrass/AffineProofs.vo
5m24.81s | 2846272 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo
4m43.41s | 3857976 ko | fiat-json/src/p434_32.json
4m41.94s | 3549180 ko | fiat-java/src/FiatP434.java
4m40.51s | 3510128 ko | fiat-go/32/p434/p434.go
4m38.01s | 3112012 ko | fiat-rust/src/p434_32.rs
4m36.06s | 1005000 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
4m35.63s | 3460760 ko | fiat-c/src/p434_32.c
4m24.81s | 3479832 ko | fiat-bedrock2/src/p434_32.c
4m21.82s | 1805944 ko | Curves/EdwardsMontgomery.vo
4m16.62s | 969388 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo
4m05.49s | 3689096 ko | fiat-zig/src/p434_32.zig
4m02.12s | 2558072 ko | Assembly/WithBedrock/Proofs.vo
3m45.39s | 1784600 ko | Rewriter/Passes/ArithWithCasts.vo
3m21.77s | 3298648 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
3m14.18s | 2606244 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo
3m01.52s | 1449620 ko | Curves/Weierstrass/Projective.vo
2m51.65s | 781792 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo
2m43.49s | 1590284 ko | Curves/Montgomery/XZProofs.vo
2m41.57s | 1467320 ko | Curves/Montgomery/AffineProofs.vo
2m30.06s | 1114396 ko | Fancy/Compiler.vo
2m16.49s | 1561432 ko | Rewriter/Passes/NBE.vo
1m58.96s | 2787304 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo
1m56.94s | 2010232 ko | fiat-json/src/p384_scalar_32.json
1m54.69s | 442236 ko | Spec/Test/X25519.vo
1m54.17s | 2271728 ko | fiat-bedrock2/src/p384_scalar_32.c
1m53.70s | 1745936 ko | fiat-zig/src/p384_32.zig
1m53.52s | 2115820 ko | fiat-go/32/p384/p384.go
1m53.19s | 1674280 ko | fiat-json/src/p384_32.json
1m53.14s | 1628960 ko | fiat-java/src/FiatP384.java
1m53.05s | 1699924 ko | fiat-rust/src/p384_scalar_32.rs
1m52.61s | 1822712 ko | fiat-bedrock2/src/p384_32.c
1m51.65s | 1604284 ko | Bedrock/End2End/X25519/Field25519.vo
1m51.49s | 1435476 ko | Rewriter/Passes/ToFancyWithCasts.vo
1m51.33s | 1635188 ko | fiat-c/src/p384_scalar_32.c
1m49.51s | 1953272 ko | fiat-rust/src/p384_32.rs
1m49.44s | 2074092 ko | fiat-c/src/p384_32.c
1m47.54s | 2392824 ko | Fancy/Barrett256.vo
1m46.52s | 1924084 ko | fiat-go/32/p384scalar/p384scalar.go
1m46.35s | 1693196 ko | fiat-zig/src/p384_scalar_32.zig
1m45.28s | 2107680 ko | fiat-java/src/FiatP384Scalar.java
1m33.15s | 860988 ko | Util/FSets/FMapTrie.vo
1m28.26s | 2040924 ko | SlowPrimeSynthesisExamples.vo
1m22.76s | 744076 ko | rupicola/bedrock2/compiler/src/compiler/MMIO.vo
1m21.24s | 607772 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo
1m20.59s | 1528152 ko | Assembly/EquivalenceProofs.vo
1m20.11s | 750284 ko | Arithmetic/SolinasReduction.vo
1m19.98s | 1135724 ko | UnsaturatedSolinasHeuristics/Tests.vo
1m19.07s | 1580872 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo
1m16.09s | 1015848 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo
1m09.19s | 1436812 ko | Assembly/WithBedrock/SymbolicProofs.vo
1m07.33s | 803216 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo
1m04.55s | 881276 ko | AbstractInterpretation/Wf.vo
1m04.51s | 931300 ko | Curves/Weierstrass/Jacobian.vo
1m03.62s | 782744 ko | Rewriter/Rewriter/Wf.vo
0m59.64s | 704332 ko | Rewriter/RulesProofs.vo
0m57.69s | 733928 ko | Rewriter/Language/UnderLetsProofs.vo
0m56.72s | 1004580 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo
0m53.99s | 833600 ko | AbstractInterpretation/ZRangeProofs.vo
0m53.23s | 1044640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo
0m52.35s | 944996 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo
0m51.52s | 625496 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo
0m51.41s | 1011348 ko | Rewriter/Rewriter/Examples.vo
0m51.35s | 1023708 ko | Rewriter/Passes/MultiRetSplit.vo
0m50.98s | 831264 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo
0m50.20s | 1302956 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo
0m47.60s | 584048 ko | Demo.vo
0m46.50s | 854544 ko | Rewriter/Rewriter/InterpProofs.vo
0m45.91s | 1745024 ko | Fancy/Montgomery256.vo
0m45.90s | 804912 ko | Rewriter/Rewriter/ProofsCommon.vo
0m44.99s | 1530768 ko | Assembly/Symbolic.vo
0m44.72s | 1102468 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo
0m44.72s | 2147808 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
0m43.59s | 2147776 ko | ExtractionOCaml/bedrock2_solinas_reduction
0m43.31s | 2147552 ko | ExtractionOCaml/solinas_reduction
0m42.97s | 2147820 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
0m41.82s | 67656 ko | fiat-go/32/p521/p521.go
0m41.14s | 569868 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo
0m41.05s | 625248 ko | rupicola/bedrock2/compiler/src/compiler/Spilling.vo
0m41.01s | 2148412 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
0m40.68s | 2148192 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
0m40.68s | 1072812 ko | Rewriter/Passes/Arith.vo
0m40.36s | 2147748 ko | ExtractionOCaml/word_by_word_montgomery
0m39.88s | 1003376 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo
0m38.76s | 60548 ko | fiat-java/src/FiatP521.java
0m38.74s | 142728 ko | fiat-bedrock2/src/p521_32.c
0m38.68s | 110444 ko | fiat-json/src/p521_32.json
0m38.44s | 58400 ko | fiat-zig/src/p521_32.zig
0m38.17s | 1691492 ko | ExtractionOCaml/unsaturated_solinas
0m37.93s | 1633424 ko | ExtractionOCaml/bedrock2_dettman_multiplication
0m37.93s | 59156 ko | fiat-c/src/p521_32.c
0m37.73s | 1623156 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
0m37.70s | 708548 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo
0m37.54s | 1624828 ko | ExtractionOCaml/with_bedrock2_base_conversion
0m37.33s | 1624096 ko | ExtractionOCaml/bedrock2_saturated_solinas
0m37.21s | 1622976 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
0m37.17s | 1620288 ko | ExtractionOCaml/bedrock2_base_conversion
0m36.76s | 1623680 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
0m35.29s | 1415796 ko | ExtractionOCaml/dettman_multiplication
0m34.64s | 1538708 ko | ExtractionOCaml/base_conversion
0m34.35s | 60732 ko | fiat-rust/src/p521_32.rs
0m34.33s | 1415896 ko | ExtractionOCaml/saturated_solinas
0m34.18s | 2237120 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
0m33.80s | 2211416 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
0m33.32s | 2211048 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
0m33.32s | 877940 ko | Rewriter/Passes/MulSplit.vo
0m33.30s | 1255200 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo
0m32.38s | 2133140 ko | ExtractionOCaml/solinas_reduction.ml
0m32.05s | 566656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo
0m31.56s | 1232064 ko | ExtractionOCaml/perf_word_by_word_montgomery
0m31.38s | 2108664 ko | ExtractionOCaml/word_by_word_montgomery.ml
0m30.75s | 1232248 ko | ExtractionOCaml/perf_unsaturated_solinas
0m30.68s | 2116064 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
0m30.48s | 617376 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo
0m30.13s | 2115380 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
0m30.01s | 1516352 ko | StandaloneDebuggingExamples.vo
0m29.81s | 702960 ko | AbstractInterpretation/Proofs.vo
0m28.53s | 2028924 ko | ExtractionOCaml/unsaturated_solinas.ml
0m28.11s | 664744 ko | rupicola/src/Rupicola/Examples/Utf8/Utf8.vo
0m27.87s | 876328 ko | Rewriter/Rewriter/Examples/PrefixSums.vo
0m27.32s | 2051412 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
0m26.62s | 687116 ko | Rewriter/Language/Wf.vo
0m26.58s | 2005604 ko | ExtractionOCaml/bedrock2_base_conversion.ml
0m26.45s | 1996160 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
0m26.36s | 2005536 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
0m26.27s | 1996184 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
0m26.18s | 1999292 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
0m26.15s | 1998300 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
0m25.87s | 590672 ko | Rewriter/Language/Inversion.vo
0m25.26s | 1371200 ko | PerfTesting/PerfTestSearch.vo
0m25.09s | 1938912 ko | ExtractionOCaml/dettman_multiplication.ml
0m24.54s | 1924440 ko | ExtractionOCaml/saturated_solinas.ml
0m24.23s | 1921016 ko | ExtractionOCaml/base_conversion.ml
0m23.60s | 1179724 ko | PushButtonSynthesis/UnsaturatedSolinas.vo
0m23.31s | 874692 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo
0m22.72s | 499960 ko | Arithmetic/Saturated.vo
0m21.95s | 1329776 ko | Bedrock/End2End/RupicolaCrypto/Low.vo
0m20.78s | 813596 ko | Bedrock/Field/Translation/Proofs/Expr.vo
0m20.30s | 1149392 ko | PushButtonSynthesis/WordByWordMontgomery.vo
0m20.07s | 747300 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo
0m19.54s | 629200 ko | Util/FSets/FMapBool.vo
0m19.45s | 694948 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.vo
0m19.35s | 1838828 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
0m19.22s | 680380 ko | rupicola/bedrock2/compiler/src/compiler/FlatImp.vo
0m19.16s | 1828412 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
0m18.94s | 313308 ko | fiat-go/64/p434/p434.go
0m18.72s | 244116 ko | fiat-zig/src/p434_64.zig
0m18.38s | 634116 ko | Util/FSets/FMapProd.vo
0m17.79s | 281552 ko | fiat-json/src/p434_64.json
0m17.78s | 487432 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c
0m17.74s | 1370888 ko | PerfTesting/PerfTestSearchPattern.vo
0m17.71s | 302348 ko | fiat-bedrock2/src/p434_64.c
0m17.68s | 431072 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig
0m17.67s | 379652 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json
0m17.58s | 1155688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo
0m17.52s | 255060 ko | fiat-c/src/p434_64.c
0m17.50s | 1128196 ko | Bedrock/Field/Translation/Proofs/Func.vo
0m17.50s | 397092 ko | fiat-bedrock2/src/p256_scalar_32.c
0m17.41s | 1120356 ko | Bedrock/End2End/Poly1305/Field1305.vo
0m17.33s | 376544 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
0m17.32s | 373956 ko | fiat-json/src/p256_scalar_32.json
0m17.30s | 407340 ko | fiat-json/src/secp256k1_montgomery_32.json
0m17.26s | 567160 ko | Util/FSets/FMapSum.vo
0m17.26s | 363444 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java
0m17.20s | 306884 ko | fiat-rust/src/p434_64.rs
0m17.17s | 1109240 ko | Assembly/Parse/TestAsm.vo
0m17.17s | 438860 ko | fiat-java/src/FiatP256Scalar.java
0m17.13s | 413312 ko | fiat-go/32/p256scalar/p256scalar.go
0m17.06s | 415760 ko | fiat-json/src/curve25519_scalar_32.json
0m17.03s | 396804 ko | fiat-zig/src/secp256k1_montgomery_32.zig
0m16.90s | 395476 ko | fiat-bedrock2/src/curve25519_scalar_32.c
0m16.90s | 436536 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c
0m16.88s | 422848 ko | fiat-java/src/FiatSecp256K1Montgomery.java
0m16.85s | 542932 ko | Arithmetic/WordByWordMontgomery.vo
0m16.84s | 344632 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go
0m16.79s | 384576 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c
0m16.77s | 345256 ko | fiat-rust/src/p256_scalar_32.rs
0m16.68s | 323816 ko | fiat-java/src/FiatCurve25519Scalar.java
0m16.64s | 340412 ko | fiat-go/32/curve25519scalar/curve25519scalar.go
0m16.63s | 620464 ko | Util/ZUtil/ArithmeticShiftr.vo
0m16.63s | 407304 ko | fiat-zig/src/curve25519_scalar_32.zig
0m16.60s | 1200944 ko | Bedrock/Field/Synthesis/New/Signature.vo
0m16.60s | 365388 ko | fiat-c/src/p256_scalar_32.c
0m16.57s | 368480 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs
0m16.53s | 833896 ko | Curves/Edwards/XYZT/Basic.vo
0m16.50s | 2124656 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs
0m16.39s | 2120524 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs
0m16.38s | 432820 ko | fiat-json/src/p256_32.json
0m16.37s | 430104 ko | fiat-zig/src/p256_scalar_32.zig
0m16.35s | 330524 ko | fiat-c/src/curve25519_scalar_32.c
0m16.32s | 349716 ko | fiat-zig/src/p256_32.zig
0m16.27s | 2013724 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs
0m16.24s | 364604 ko | fiat-rust/src/curve25519_scalar_32.rs
0m16.19s | 402376 ko | fiat-rust/src/secp256k1_montgomery_32.rs
0m16.04s | 765616 ko | Language/IdentifiersGENERATED.vo
0m16.01s | 563772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo
0m16.00s | 573536 ko | Bedrock/Field/Synthesis/Examples/redc.vo
0m15.97s | 2014024 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs
0m15.89s | 421264 ko | fiat-c/src/secp256k1_montgomery_32.c
0m15.84s | 364416 ko | fiat-java/src/FiatP256.java
0m15.77s | 395208 ko | fiat-bedrock2/src/p256_32.c
0m15.71s | 1964864 ko | ExtractionHaskell/solinas_reduction.hs
0m15.69s | 323896 ko | fiat-c/src/p256_32.c
0m15.66s | 726776 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo
0m15.62s | 405156 ko | fiat-go/32/p256/p256.go
0m15.55s | 766356 ko | Curves/Edwards/AffineProofs.vo
0m15.37s | 568164 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo
0m15.33s | 370928 ko | fiat-rust/src/p256_32.rs
0m15.29s | 1983440 ko | ExtractionHaskell/word_by_word_montgomery.hs
0m15.19s | 520360 ko | Arithmetic/BarrettReduction.vo
0m15.12s | 425240 ko | rupicola/bedrock2/deps/coqutil/test/TestGoals.vo
0m14.91s | 516204 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo
0m14.84s | 1909292 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs
0m14.83s | 596008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo
0m14.79s | 463028 ko | Algebra/Field.vo
0m14.67s | 1999460 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs
0m14.66s | 1860044 ko | ExtractionHaskell/unsaturated_solinas.hs
0m14.61s | 1998800 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs
0m14.55s | 487988 ko | rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo
0m14.49s | 565196 ko | Util/FSets/FMapOption.vo
0m14.47s | 1910172 ko | ExtractionHaskell/bedrock2_base_conversion.hs
0m14.45s | 1896592 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs
0m14.35s | 1917576 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs
0m14.30s | 1897756 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs
0m14.22s | 1917456 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs
0m14.19s | 593376 ko | Language/IdentifiersGENERATEDProofs.vo
0m14.13s | 526388 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
0m14.01s | 660304 ko | Bedrock/Group/AdditionChains.vo
0m13.89s | 462944 ko | Util/Structures/Orders/Prod.vo
0m13.85s | 491540 ko | rupicola/src/Rupicola/Examples/Arrays.vo
0m13.83s | 544744 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo
0m13.79s | 498032 ko | rupicola/src/Rupicola/Examples/CMove/CMove.vo
0m13.77s | 598308 ko | Bedrock/Field/Common/Util.vo
0m13.61s | 1811276 ko | ExtractionHaskell/dettman_multiplication.hs
0m13.60s | 1846816 ko | ExtractionHaskell/saturated_solinas.hs
0m13.55s | 492116 ko | rupicola/src/Rupicola/Examples/Loops.vo
0m13.46s | 538316 ko | rupicola/src/Rupicola/Examples/KVStore/Manual.vo
0m13.27s | 1793716 ko | ExtractionHaskell/base_conversion.hs
0m13.21s | 649252 ko | Bedrock/Group/ScalarMult/LadderStep.vo
0m12.82s | 494032 ko | Arithmetic/Core.vo
0m11.93s | 1026788 ko | BoundsPipeline.vo
0m11.86s | 637944 ko | Rewriter/Demo.vo
0m11.73s | 545076 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo
0m11.72s | 707092 ko | Util/ZRange/LandLorBounds.vo
0m11.52s | 484076 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo
0m11.38s | 1677648 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo
0m11.28s | 165124 ko | fiat-go/64/p384scalar/p384scalar.go
0m11.23s | 153540 ko | fiat-c/src/p384_scalar_64.c
0m11.20s | 197432 ko | fiat-json/src/p384_scalar_64.json
0m11.13s | 192732 ko | fiat-bedrock2/src/p384_scalar_64.c
0m11.10s | 165668 ko | fiat-zig/src/p384_scalar_64.zig
0m11.00s | 658176 ko | rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo
0m10.96s | 165272 ko | fiat-rust/src/p384_scalar_64.rs
0m10.65s | 505684 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo
0m10.64s | 476416 ko | Primitives/MxDHRepChange.vo
0m10.41s | 742196 ko | Assembly/Syntax.vo
0m10.37s | 1339924 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo
0m10.32s | 459448 ko | Util/Structures/Orders/List.vo
0m10.24s | 451276 ko | Algebra/Ring.vo
0m10.12s | 622652 ko | Bedrock/Field/Translation/Proofs/Flatten.vo
0m10.02s | 579416 ko | PushButtonSynthesis/BYInversionReificationCache.vo
0m09.85s | 182968 ko | fiat-c/src/p384_64.c
0m09.77s | 173092 ko | fiat-json/src/p384_64.json
0m09.76s | 164688 ko | fiat-go/64/p384/p384.go
0m09.66s | 139760 ko | fiat-zig/src/p384_64.zig
0m09.62s | 872852 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo
0m09.59s | 250704 ko | fiat-zig/src/p224_32.zig
0m09.52s | 238320 ko | fiat-json/src/p224_32.json
0m09.49s | 230008 ko | fiat-go/32/p224/p224.go
0m09.47s | 203968 ko | fiat-bedrock2/src/p384_64.c
0m09.47s | 272744 ko | fiat-java/src/FiatP224.java
0m09.43s | 658732 ko | Bedrock/Group/ScalarMult/CSwap.vo
0m09.43s | 595324 ko | Stringification/IR.vo
0m09.40s | 558640 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo
0m09.37s | 554444 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo
0m09.32s | 258236 ko | fiat-bedrock2/src/p224_32.c
0m09.29s | 177692 ko | fiat-rust/src/p384_64.rs
0m09.28s | 1030020 ko | PushButtonSynthesis/BaseConversion.vo
0m09.27s | 270084 ko | fiat-c/src/p224_32.c
0m09.24s | 550836 ko | rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo
0m09.10s | 230652 ko | fiat-rust/src/p224_32.rs
0m09.01s | 506588 ko | Rewriter/Language/IdentifiersLibraryProofs.vo
0m08.90s | 497908 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI.vo
0m08.58s | 123780 ko | fiat-json/src/p448_solinas_32.json
0m08.35s | 600540 ko | Language/IdentifiersBasicGENERATED.vo
0m08.33s | 1038828 ko | PushButtonSynthesis/Primitives.vo
0m08.23s | 998908 ko | PushButtonSynthesis/SmallExamples.vo
0m08.15s | 785760 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo
0m08.14s | 912272 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo
0m08.14s | 59548 ko | fiat-rust/src/p448_solinas_32.rs
0m08.03s | 58124 ko | fiat-zig/src/p448_solinas_32.zig
0m07.90s | 58212 ko | fiat-c/src/p448_solinas_32.c
0m07.80s | 527792 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.vo
0m07.77s | 462448 ko | rupicola/src/Rupicola/Examples/KVStore/Automated.vo
0m07.70s | 587264 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo
0m07.52s | 491008 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.vo
0m07.45s | 471188 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo
0m07.44s | 468880 ko | Util/ZRange/CornersMonotoneBounds.vo
0m07.26s | 1031232 ko | PushButtonSynthesis/SolinasReduction.vo
0m07.15s | 659224 ko | Util/FSets/FMapTrieEx.vo
0m06.85s | 471788 ko | rupicola/src/Rupicola/Examples/L64X128.vo
0m06.84s | 708648 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo
0m06.79s | 459008 ko | rupicola/src/Rupicola/Examples/Expr.vo
0m06.74s | 450284 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add.vo
0m06.54s | 492712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/bsearch.vo
0m06.50s | 546780 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo
0m06.41s | 467236 ko | Arithmetic/FancyMontgomeryReduction.vo
0m06.37s | 1134776 ko | CLI.vo
0m06.33s | 49900 ko | fiat-go/64/p521/p521.go
0m06.32s | 1037180 ko | PushButtonSynthesis/BarrettReduction.vo
0m06.31s | 679460 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo
0m06.31s | 457988 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo
0m06.19s | 458048 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo
0m06.18s | 1132992 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo
0m06.16s | 543604 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo
0m06.06s | 902704 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo
0m06.06s | 438980 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo
0m06.05s | 574516 ko | Rewriter/Passes/NoSelect.vo
0m06.03s | 480020 ko | rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo
0m06.01s | 671264 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo
0m05.97s | 486436 ko | Util/ZUtil/Modulo.vo
0m05.86s | 466112 ko | Util/ListUtil.vo
0m05.85s | 469760 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo
0m05.57s | 51132 ko | fiat-json/src/p521_64.json
0m05.56s | 682812 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.vo
0m05.54s | 65620 ko | fiat-bedrock2/src/p521_64.c
0m05.51s | 36024 ko | fiat-zig/src/p521_64.zig
0m05.45s | 460124 ko | Util/MSets/MSetSum.vo
0m05.45s | 36640 ko | fiat-c/src/p521_64.c
0m05.43s | 532688 ko | Fancy/Prod.vo
0m05.41s | 576128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo
0m05.40s | 614228 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo
0m05.40s | 36120 ko | fiat-rust/src/p521_64.rs
0m05.36s | 461088 ko | rupicola/bedrock2/compiler/src/compiler/ExprImp.vo
0m05.28s | 453952 ko | Rewriter/Util/ListUtil.vo
0m05.12s | 513604 ko | Arithmetic/BYInv.vo
0m05.10s | 454392 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FlatConstMem.vo
0m04.95s | 470428 ko | rupicola/src/Rupicola/Lib/Loops.vo
0m04.94s | 467968 ko | Util/FsatzAutoLemmas.vo
0m04.93s | 432264 ko | Spec/Curve25519.vo
0m04.83s | 462000 ko | rupicola/src/Rupicola/Examples/CRC32/CRC32.vo
0m04.73s | 498572 ko | Curves/Edwards/Pre.vo
0m04.72s | 550548 ko | Language/InversionExtra.vo
0m04.61s | 455752 ko | Util/FSets/FMapIso.vo
0m04.59s | 448220 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.vo
0m04.55s | 472888 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo
0m04.49s | 1063260 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo
0m04.42s | 465320 ko | Util/ZRange/BasicLemmas.vo
0m04.38s | 445356 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo
0m04.38s | 444300 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo
0m04.37s | 1028072 ko | PushButtonSynthesis/DettmanMultiplication.vo
0m04.32s | 1034544 ko | PushButtonSynthesis/SaturatedSolinas.vo
0m04.28s | 553116 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo
0m04.26s | 460864 ko | Util/FSets/FMapSect.vo
0m04.24s | 434096 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/BenchCancel256.vo
0m04.24s | 470912 ko | rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo
0m04.19s | 446352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo
0m04.18s | 955212 ko | Assembly/Equivalence.vo
0m04.13s | 445192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo
0m04.10s | 474136 ko | Algebra/Field_test.vo
0m04.02s | 434628 ko | Arithmetic/MontgomeryReduction/Proofs.vo
0m04.00s | 470212 ko | Rewriter/Language/IdentifiersBasicLibrary.vo
0m03.97s | 492300 ko | COperationSpecifications.vo
0m03.96s | 1483248 ko | Bedrock/Everything.vo
0m03.95s | 565888 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo
0m03.92s | 461212 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memequal.vo
0m03.89s | 438292 ko | rupicola/src/Rupicola/Examples/Cells/IndirectAdd.vo
0m03.84s | 1047084 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo
0m03.76s | 460392 ko | rupicola/src/Rupicola/Examples/Uppercase.vo
0m03.74s | 487816 ko | Curves/Montgomery/Affine.vo
0m03.62s | 1341008 ko | Everything.vo
0m03.51s | 451668 ko | Arithmetic/BarrettReduction/Generalized.vo
0m03.50s | 456840 ko | CastLemmas.vo
0m03.49s | 545604 ko | PushButtonSynthesis/BaseConversionReificationCache.vo
0m03.47s | 415800 ko | rupicola/bedrock2/deps/coqutil/test/SlowGoals.vo
0m03.42s | 394996 ko | Algebra/Group.vo
0m03.42s | 453312 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memswap.vo
0m03.37s | 460156 ko | UnsaturatedSolinasHeuristics.vo
0m03.36s | 435964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo
0m03.35s | 454600 ko | Arithmetic/UniformWeight.vo
0m03.33s | 444692 ko | Util/ZUtil/LandLorShiftBounds.vo
0m03.27s | 448912 ko | rupicola/src/Rupicola/Examples/Arithmetic.vo
0m03.24s | 434864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo
0m03.21s | 449104 ko | Arithmetic/BarrettReduction/HAC.vo
0m03.20s | 449096 ko | Util/ZUtil/LandLorBounds.vo
0m03.15s | 1006432 ko | Bedrock/Field/Translation/Cmd.vo
0m03.14s | 677116 ko | Bedrock/Group/ScalarMult/ScalarMult.vo
0m03.13s | 1070140 ko | Rewriter/PerfTesting/Core.vo
0m03.10s | 446044 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo
0m03.07s | 1343548 ko | PerfTesting/PerfTestPrint.vo
0m03.06s | 446136 ko | Util/Structures/Orders.vo
0m02.99s | 446820 ko | rupicola/src/Rupicola/Examples/RevComp.vo
0m02.97s | 1002728 ko | Bedrock/Field/Translation/Func.vo
0m02.95s | 1066612 ko | Bedrock/Field/Stringification/Stringification.vo
0m02.95s | 609264 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo
0m02.90s | 442416 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo
0m02.89s | 75160 ko | fiat-json/src/p256_scalar_64.json
0m02.84s | 411248 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo
0m02.84s | 61996 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
0m02.82s | 84244 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c
0m02.82s | 72148 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json
0m02.80s | 1103808 ko | StandaloneOCamlMain.vo
0m02.80s | 84916 ko | fiat-bedrock2/src/p256_scalar_64.c
0m02.80s | 427948 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo
0m02.79s | 64876 ko | fiat-go/64/p256scalar/p256scalar.go
0m02.78s | 439896 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ipow.vo
0m02.77s | 1059012 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo
0m02.77s | 57088 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig
0m02.75s | 1143348 ko | Bedrock/Standalone/StandaloneHaskellMain.vo
0m02.75s | 431748 ko | Util/Structures/Orders/Option.vo
0m02.75s | 433944 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo
0m02.74s | 1103744 ko | StandaloneHaskellMain.vo
0m02.74s | 56376 ko | fiat-c/src/p256_scalar_64.c
0m02.74s | 60560 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs
0m02.74s | 451660 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediate.vo
0m02.73s | 61824 ko | fiat-zig/src/p256_scalar_64.zig
0m02.72s | 1064916 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo
0m02.71s | 519732 ko | Rewriter/Passes/Test.vo
0m02.71s | 61076 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c
0m02.71s | 60028 ko | fiat-rust/src/p256_scalar_64.rs
0m02.70s | 535708 ko | Rewriter/Passes/AddAssocLeft.vo
0m02.68s | 51016 ko | fiat-go/64/p448solinas/p448solinas.go
0m02.67s | 442740 ko | Arithmetic/Primitives.vo
0m02.65s | 438452 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap_by_add.vo
0m02.64s | 1143212 ko | Bedrock/Standalone/StandaloneOCamlMain.vo
0m02.60s | 443440 ko | rupicola/src/Rupicola/Examples/IO/Echo.vo
0m02.59s | 549304 ko | Util/FSets/FMapTrie/ShapeEx.vo
0m02.58s | 1129176 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
0m02.58s | 434880 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo
0m02.57s | 621908 ko | Bedrock/Field/Interface/Compilation2.vo
0m02.56s | 1042648 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo
0m02.55s | 71208 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go
0m02.55s | 75224 ko | fiat-json/src/secp256k1_montgomery_64.json
0m02.54s | 1043268 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo
0m02.52s | 59660 ko | fiat-zig/src/secp256k1_montgomery_64.zig
0m02.50s | 1043292 ko | Bedrock/Field/Translation/Parameters/FE310.vo
0m02.48s | 426684 ko | Util/ZUtil/ZSimplify/Autogenerated.vo
0m02.48s | 68740 ko | fiat-json/src/curve25519_scalar_64.json
0m02.47s | 57260 ko | fiat-c/src/secp256k1_montgomery_64.c
0m02.46s | 1038448 ko | Bedrock/Field/Translation/Parameters/Defaults.vo
0m02.43s | 82756 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c
0m02.43s | 447172 ko | rupicola/src/Rupicola/Lib/Core.vo
0m02.42s | 537004 ko | Rewriter/Passes/FlattenThunkedRects.vo
0m02.42s | 64252 ko | fiat-rust/src/secp256k1_montgomery_64.rs
0m02.41s | 425468 ko | Util/Bool/Reflect.vo
0m02.41s | 441108 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/rpmul.vo
0m02.40s | 423368 ko | Rewriter/Util/Bool/Reflect.vo
0m02.40s | 470248 ko | Util/ZUtil/Morphisms.vo
0m02.38s | 467216 ko | MiscCompilerPassesProofs.vo
0m02.38s | 468844 ko | rupicola/bedrock2/bedrock2/src/bedrock2/unzify.vo
0m02.38s | 443668 ko | rupicola/src/Rupicola/Examples/DownTo.vo
0m02.37s | 67816 ko | fiat-go/64/curve25519scalar/curve25519scalar.go
0m02.36s | 449676 ko | Util/MSets/MSetIso.vo
0m02.36s | 77284 ko | fiat-bedrock2/src/curve25519_scalar_64.c
0m02.35s | 545536 ko | Bedrock/Field/Translation/Expr.vo
0m02.34s | 55824 ko | fiat-zig/src/curve25519_scalar_64.zig
0m02.30s | 459484 ko | Spec/MontgomeryCurve.vo
0m02.29s | 448692 ko | rupicola/src/Rupicola/Examples/LinkedList/Find.vo
0m02.28s | 444516 ko | Util/ZUtil/Shift.vo
0m02.28s | 61352 ko | fiat-c/src/curve25519_scalar_64.c
0m02.26s | 61228 ko | fiat-rust/src/curve25519_scalar_64.rs
0m02.26s | 463064 ko | rupicola/bedrock2/compiler/src/compiler/Pipeline.vo
0m02.24s | 429604 ko | Util/ZUtil/TwosComplement.vo
0m02.17s | 456624 ko | rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo
0m02.16s | 35384 ko | fiat-go/32/curve25519/curve25519.go
0m02.13s | 611384 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo
0m02.12s | 434664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseHyps.vo
0m02.12s | 446464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo
0m02.09s | 67276 ko | fiat-bedrock2/src/p448_solinas_64.c
0m02.08s | 51372 ko | fiat-json/src/p448_solinas_64.json
0m02.05s | 456784 ko | Arithmetic/Freeze.vo
0m02.04s | 541056 ko | Stringification/Language.vo
0m02.01s | 417420 ko | rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo
0m01.97s | 61072 ko | fiat-go/64/p224/p224.go
0m01.97s | 75016 ko | fiat-json/src/p224_64.json
0m01.97s | 35100 ko | fiat-zig/src/p448_solinas_64.zig
0m01.96s | 63284 ko | fiat-bedrock2/src/curve25519_32.c
0m01.96s | 34764 ko | fiat-rust/src/p448_solinas_64.rs
0m01.95s | 456464 ko | Arithmetic/BaseConversion.vo
0m01.95s | 435856 ko | Util/ZUtil/Testbit.vo
0m01.95s | 49468 ko | fiat-json/src/curve25519_32.json
0m01.94s | 464252 ko | Curves/TableMult/TableMult.vo
0m01.92s | 445120 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memconst.vo
0m01.91s | 389284 ko | Util/Wf2.vo
0m01.91s | 77496 ko | fiat-bedrock2/src/p224_64.c
0m01.90s | 34496 ko | fiat-c/src/p448_solinas_64.c
0m01.89s | 66076 ko | fiat-go/64/p256/p256.go
0m01.89s | 62320 ko | fiat-zig/src/p224_64.zig
0m01.88s | 431764 ko | Util/ZUtil/ModInv.vo
0m01.88s | 34152 ko | fiat-java/src/FiatCurve25519.java
0m01.88s | 66424 ko | fiat-json/src/p256_64.json
0m01.86s | 56312 ko | fiat-c/src/p224_64.c
0m01.86s | 441768 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.vo
0m01.85s | 55924 ko | fiat-zig/src/p256_64.zig
0m01.83s | 536604 ko | Rewriter/Passes/UnfoldValueBarrier.vo
0m01.83s | 77644 ko | fiat-bedrock2/src/p256_64.c
0m01.83s | 33544 ko | fiat-zig/src/curve25519_32.zig
0m01.82s | 33528 ko | fiat-c/src/curve25519_32.c
0m01.81s | 535512 ko | Rewriter/Passes/StripLiteralCasts.vo
0m01.81s | 66316 ko | fiat-rust/src/p224_64.rs
0m01.79s | 429896 ko | Util/ZUtil/Div.vo
0m01.79s | 61824 ko | fiat-c/src/p256_64.c
0m01.76s | 34144 ko | fiat-rust/src/curve25519_32.rs
0m01.75s | 433864 ko | Arithmetic/BarrettReduction/RidiculousFish.vo
0m01.75s | 59120 ko | fiat-rust/src/p256_64.rs
0m01.75s | 435556 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc.vo
0m01.74s | 419580 ko | Util/ListUtil/Forall.vo
0m01.71s | 634084 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo
0m01.69s | 463032 ko | Arithmetic/DettmanMultiplication.vo
0m01.67s | 446804 ko | Arithmetic/ModularArithmeticTheorems.vo
0m01.67s | 438212 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo
0m01.64s | 454032 ko | Arithmetic/ModOps.vo
0m01.63s | 446228 ko | Util/FSets/FMapFacts.vo
0m01.63s | 456584 ko | rupicola/src/Rupicola/Lib/Arrays.vo
0m01.61s | 536468 ko | Rewriter/Passes/ToFancy.vo
0m01.60s | 481268 ko | Assembly/Parse.vo
0m01.59s | 427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo
0m01.55s | 605636 ko | Bedrock/Field/Common/Names/MakeNames.vo
0m01.54s | 511864 ko | AbstractInterpretation/AbstractInterpretation.vo
0m01.54s | 589320 ko | CompilersTestCases.vo
0m01.54s | 433340 ko | Util/Tuple.vo
0m01.52s | 461152 ko | Util/FSets/FMapUnit.vo
0m01.49s | 451136 ko | rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo
0m01.48s | 518524 ko | AbstractInterpretation/ZRange.vo
0m01.48s | 462156 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo
0m01.48s | 464356 ko | rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo
0m01.48s | 430244 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo
0m01.47s | 458800 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo
0m01.47s | 436092 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo
0m01.45s | 435748 ko | rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo
0m01.44s | 436208 ko | rupicola/src/Rupicola/Examples/Conditionals.vo
0m01.43s | 446448 ko | rupicola/src/Rupicola/Examples/Nondeterminism/StackAlloc.vo
0m01.41s | 423320 ko | Algebra/ScalarMult.vo
0m01.40s | 411744 ko | Rewriter/Util/ListUtil/Forall.vo
0m01.38s | 541876 ko | Stringification/Go.vo
0m01.38s | 385056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/StringdumpDemo.vo
0m01.37s | 452204 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo
0m01.37s | 411588 ko | Coqprime/Z/Pmod.vo
0m01.37s | 436708 ko | Spec/WeierstrassCurve.vo
0m01.37s | 430856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo
0m01.37s | 434736 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo
0m01.37s | 438944 ko | rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo
0m01.34s | 438172 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Impl.vo
0m01.33s | 448576 ko | Util/ZRange/SplitRangeBounds.vo
0m01.33s | 435892 ko | Util/ZUtil/Pow2Mod.vo
0m01.33s | 415496 ko | Util/ZUtil/Rshi.vo
0m01.33s | 414960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo
0m01.30s | 452228 ko | rupicola/bedrock2/compiler/src/compiler/FitsStack.vo
0m01.29s | 414900 ko | Util/ListUtil/StdlibCompat.vo
0m01.28s | 468404 ko | Rewriter/Language/IdentifiersLibrary.vo
0m01.26s | 436408 ko | Util/ZUtil/TruncatingShiftl.vo
0m01.26s | 425820 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FrameRule.vo
0m01.26s | 439488 ko | rupicola/src/Rupicola/Lib/Compiler.vo
0m01.25s | 445464 ko | rupicola/src/Rupicola/Lib/InlineTables.vo
0m01.23s | 408764 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo
0m01.22s | 438096 ko | Util/ZUtil/Bitwise.vo
0m01.21s | 413612 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo
0m01.20s | 442084 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponderProofs.vo
0m01.18s | 424488 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo
0m01.15s | 624520 ko | Bedrock/Specs/Field.vo
0m01.15s | 438748 ko | Util/ZUtil/Quot.vo
0m01.14s | 431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo
0m01.10s | 418728 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo
0m01.09s | 430968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo
0m01.08s | 446720 ko | Arithmetic/Partition.vo
0m01.08s | 467272 ko | Arithmetic/PrimeFieldTheorems.vo
0m01.08s | 410040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo
0m01.08s | 411032 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo
0m01.06s | 445080 ko | Util/ZRange/SplitBounds.vo
0m01.06s | 424436 ko | Util/ZUtil/AddGetCarry.vo
0m01.05s | 603076 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo
0m01.03s | 427980 ko | rupicola/bedrock2/bedrock2/src/bedrock2/sepapp.vo
0m01.03s | 434252 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap.vo
0m01.03s | 434100 ko | rupicola/src/Rupicola/Examples/Cells/Swap.vo
0m01.03s | 442092 ko | rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo
0m01.02s | 596904 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo
0m01.02s | 443508 ko | Fancy/Spec.vo
0m01.02s | 466996 ko | Rewriter/Rewriter/Rewriter.vo
0m01.01s | 359856 ko | Util/Wf1.vo
0m00.98s | 536992 ko | Stringification/JSON.vo
0m00.97s | 442992 ko | Curves/Edwards/XYZT/Precomputed.vo
0m00.97s | 434212 ko | Util/ZUtil/Ones.vo
0m00.97s | 425836 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZWordMem.vo
0m00.96s | 414848 ko | Coqprime/PrimalityTest/EGroup.vo
0m00.96s | 408248 ko | Coqprime/PrimalityTest/LucasLehmer.vo
0m00.95s | 539748 ko | Bedrock/Field/Translation/LoadStoreList.vo
0m00.95s | 538524 ko | Stringification/C.vo
0m00.95s | 443136 ko | rupicola/src/Rupicola/Examples/Nondeterminism/Peek.vo
0m00.94s | 476676 ko | Rewriter/Rewriter/Reify.vo
0m00.92s | 442380 ko | rupicola/src/Rupicola/Examples/LinkedList/LinkedList.vo
0m00.90s | 432192 ko | Rewriter/Language/Language.vo
0m00.90s | 427340 ko | Util/ZUtil/OnesFrom.vo
0m00.89s | 420356 ko | Util/NatUtil.vo
0m00.89s | 426296 ko | Util/Strings/ParseArithmetic.vo
0m00.88s | 413948 ko | Rewriter/Util/NatUtil.vo
0m00.88s | 431960 ko | Util/Structures/Orders/Sum.vo
0m00.87s | 537912 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo
0m00.87s | 537860 ko | Stringification/Zig.vo
0m00.85s | 535744 ko | Stringification/Rust.vo
0m00.84s | 615480 ko | Bedrock/Field/Interface/Representation.vo
0m00.84s | 408404 ko | Coqprime/Z/ZCAux.vo
0m00.83s | 535716 ko | Stringification/Java.vo
0m00.82s | 534452 ko | Bedrock/Field/Common/Types.vo
0m00.82s | 619304 ko | Bedrock/Group/Point.vo
0m00.82s | 428464 ko | Curves/Montgomery/AffineInstances.vo
0m00.82s | 418484 ko | Util/Strings/String_as_OT.vo
0m00.80s | 560708 ko | Util/FSets/FMapZ.vo
0m00.79s | 410708 ko | Coqprime/PrimalityTest/Pocklington.vo
0m00.79s | 413884 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo
0m00.78s | 434556 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalNoMul.vo
0m00.78s | 416052 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/bverify.vo
0m00.75s | 489812 ko | Rewriter/Rewriter/AllTactics.vo
0m00.73s | 433592 ko | Arithmetic/BarrettReduction/Wikipedia.vo
0m00.73s | 590460 ko | Bedrock/Field/Common/Tactics.vo
0m00.73s | 505840 ko | Language/APINotations.vo
0m00.73s | 429952 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ArrayCasts.vo
0m00.72s | 545876 ko | Bedrock/Field/Stringification/FlattenVarData.vo
0m00.72s | 535532 ko | Bedrock/Field/Translation/Flatten.vo
0m00.72s | 442796 ko | rupicola/src/Rupicola/Examples/IO/Stdout.vo
0m00.71s | 422452 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo
0m00.71s | 434000 ko | rupicola/src/Rupicola/Examples/Cells/Incr.vo
0m00.71s | 442724 ko | rupicola/src/Rupicola/Examples/Tree/Tree.vo
0m00.70s | 451800 ko | Assembly/Equality.vo
0m00.70s | 526724 ko | Util/FSets/FMapN.vo
0m00.70s | 416512 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo
0m00.70s | 417860 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo
0m00.69s | 540192 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo
0m00.68s | 535428 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo
0m00.68s | 438932 ko | Rewriter/Rules.vo
0m00.68s | 437028 ko | Util/NumTheoryUtil.vo
0m00.68s | 446204 ko | rupicola/src/Rupicola/Lib/ExprCompiler.vo
0m00.67s | 506924 ko | AbstractInterpretation/WfExtra.vo
0m00.67s | 546884 ko | Rewriter/All.vo
0m00.67s | 422328 ko | Util/ErrorT/List.vo
0m00.67s | 455056 ko | Util/FSets/FMapFlip.vo
0m00.67s | 325760 ko | Util/PartiallyReifiedProp.vo
0m00.66s | 412636 ko | Coqprime/PrimalityTest/Root.vo
0m00.66s | 382464 ko | Util/Decidable.vo
0m00.66s | 415468 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo
0m00.65s | 503196 ko | MiscCompilerPassesProofsExtra.vo
0m00.65s | 382116 ko | Rewriter/Util/Decidable.vo
0m00.64s | 502268 ko | Language/WfExtra.vo
0m00.64s | 512104 ko | PushButtonSynthesis/ReificationCache.vo
0m00.63s | 520828 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo
0m00.63s | 32184 ko | fiat-go/64/curve25519/curve25519.go
0m00.62s | 511348 ko | Language/API.vo
0m00.62s | 502280 ko | Rewriter/AllTacticsExtra.vo
0m00.62s | 459732 ko | Util/FSets/FMapEmpty.vo
0m00.61s | 420704 ko | Algebra/IntegralDomain.vo
0m00.61s | 412776 ko | Coqprime/PrimalityTest/Cyclic.vo
0m00.61s | 410172 ko | Coqprime/PrimalityTest/PGroup.vo
0m00.60s | 422004 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo
0m00.60s | 442884 ko | rupicola/src/Rupicola/Examples/IO/IO.vo
0m00.59s | 506272 ko | Language/UnderLetsProofsExtra.vo
0m00.59s | 444160 ko | Util/Structures/OrdersEx.vo
0m00.58s | 452780 ko | Bedrock/Group/Loops.vo
0m00.58s | 410960 ko | Coqprime/Z/ZSum.vo
0m00.58s | 429976 ko | Util/Arg.vo
0m00.58s | 422924 ko | Util/CPSUtil.vo
0m00.58s | 409592 ko | Util/OptionList.vo
0m00.58s | 445376 ko | Util/QUtil.vo
0m00.58s | 417484 ko | Util/Strings/ParseArithmeticToTaps.vo
0m00.57s | 419668 ko | Algebra/SubsetoidRing.vo
0m00.57s | 441260 ko | Util/MSets/MSetN.vo
0m00.57s | 414972 ko | Util/ZUtil/Modulo/PullPush.vo
0m00.57s | 420508 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/DisjointUnion.vo
0m00.57s | 443676 ko | rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo
0m00.55s | 121780 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
0m00.55s | 459972 ko | Rewriter/Language/IdentifiersGenerate.vo
0m00.55s | 472808 ko | Rewriter/Rewriter/ProofsCommonTactics.vo
0m00.55s | 503488 ko | Util/Strings/ParseFlagOptions.vo
0m00.55s | 427604 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Trace.vo
0m00.55s | 437368 ko | rupicola/src/Rupicola/Lib/NoExprReflection.vo
0m00.54s | 414808 ko | Util/Structures/Orders/Flip.vo
0m00.53s | 123852 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
0m00.53s | 119860 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
0m00.53s | 121504 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
0m00.53s | 120132 ko | ExtractionOCaml/word_by_word_montgomery.cmi
0m00.53s | 439364 ko | Util/ZRange/OperationsBounds.vo
0m00.53s | 421736 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo
0m00.53s | 442848 ko | rupicola/src/Rupicola/Examples/KVStore/Properties.vo
0m00.53s | 442324 ko | rupicola/src/Rupicola/Lib/ExprReflection.vo
0m00.53s | 441816 ko | rupicola/src/Rupicola/Lib/SepLocals.vo
0m00.52s | 463832 ko | ArithmeticCPS/WordByWordMontgomery.vo
0m00.52s | 117456 ko | ExtractionOCaml/base_conversion.cmi
0m00.52s | 120696 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
0m00.52s | 121620 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
0m00.52s | 118688 ko | ExtractionOCaml/solinas_reduction.cmi
0m00.52s | 483816 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo
0m00.52s | 437180 ko | Util/FSets/FMapTrie/Shape.vo
0m00.52s | 37768 ko | fiat-bedrock2/src/curve25519_64.c
0m00.51s | 461376 ko | ArithmeticCPS/Freeze.vo
0m00.51s | 123816 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
0m00.51s | 458244 ko | MiscCompilerPasses.vo
0m00.51s | 433796 ko | Util/ZUtil/CC.vo
0m00.51s | 434188 ko | Util/ZUtil/Stabilization.vo
0m00.51s | 426748 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo
0m00.50s | 450952 ko | Bedrock/Specs/Group.vo
0m00.50s | 119804 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
0m00.50s | 121292 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
0m00.50s | 121036 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
0m00.50s | 119196 ko | ExtractionOCaml/saturated_solinas.cmi
0m00.50s | 120512 ko | ExtractionOCaml/unsaturated_solinas.cmi
0m00.50s | 123036 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
0m00.50s | 481664 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo
0m00.50s | 480192 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo
0m00.50s | 415196 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/OperatorOverloading.vo
0m00.50s | 410648 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo
0m00.49s | 121232 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
0m00.49s | 458452 ko | Rewriter/Language/IdentifiersGenerateProofs.vo
0m00.49s | 427212 ko | Util/Decidable/Decidable2Bool.vo
0m00.49s | 414848 ko | Util/Structures/Orders/Bool.vo
0m00.49s | 359872 ko | Util/Wf.vo
0m00.49s | 32564 ko | fiat-json/src/curve25519_64.json
0m00.49s | 415904 ko | rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo
0m00.49s | 402296 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo
0m00.48s | 468584 ko | Assembly/WithBedrock/Semantics.vo
0m00.48s | 413160 ko | Coqprime/PrimalityTest/Zp.vo
0m00.48s | 119488 ko | ExtractionOCaml/dettman_multiplication.cmi
0m00.48s | 494280 ko | Rewriter/Util/plugins/RewriterBuild.vo
0m00.48s | 411076 ko | Util/ListUtil/SetoidListFlatMap.vo
0m00.48s | 412388 ko | Util/Loops.vo
0m00.48s | 27008 ko | fiat-zig/src/curve25519_64.zig
0m00.48s | 413600 ko | rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo
0m00.48s | 434564 ko | rupicola/src/Rupicola/Examples/Swap/Properties.vo
0m00.47s | 442008 ko | Rewriter/Language/IdentifiersBasicGenerate.vo
0m00.47s | 425064 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo
0m00.46s | 449188 ko | ArithmeticCPS/Core.vo
0m00.46s | 449384 ko | Util/FSets/FMapString.vo
0m00.46s | 452064 ko | Util/MSets/MSetPositive/Show.vo
0m00.46s | 27256 ko | fiat-c/src/curve25519_64.c
0m00.46s | 413232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo
0m00.46s | 430640 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo
0m00.45s | 456604 ko | ArithmeticCPS/ModOps.vo
0m00.45s | 475284 ko | Bedrock/End2End/RupicolaCrypto/Spec.vo
0m00.45s | 26156 ko | fiat-rust/src/curve25519_64.rs
0m00.45s | 415424 ko | rupicola/bedrock2/compiler/src/compiler/NaiveRiscvWordProperties.vo
0m00.45s | 350324 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo
0m00.45s | 442172 ko | rupicola/src/Rupicola/Examples/Utf8/Utils.vo
0m00.44s | 451428 ko | ArithmeticCPS/Saturated.vo
0m00.44s | 418984 ko | rupicola/bedrock2/compiler/src/compiler/Registers.vo
0m00.44s | 392856 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_to_string.vo
0m00.44s | 405496 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo
0m00.43s | 461376 ko | ArithmeticCPS/BaseConversion.vo
0m00.43s | 408168 ko | Coqprime/Z/ZCmisc.vo
0m00.43s | 434424 ko | Util/Strings/NamingConventions.vo
0m00.43s | 429284 ko | Util/ZUtil/Log2.vo
0m00.43s | 436420 ko | Util/ZUtil/SignBit.vo
0m00.43s | 40432 ko | fiat-bedrock2/src/curve25519_solinas_64.c
0m00.43s | 419836 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ZList.vo
0m00.43s | 405960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo
0m00.43s | 420352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo
0m00.43s | 442260 ko | rupicola/src/Rupicola/Examples/KVStore/KVStore.vo
0m00.42s | 430812 ko | Util/MSets/MSetString.vo
0m00.42s | 429680 ko | Util/ZUtil/Divide.vo
0m00.42s | 436336 ko | Util/ZUtil/Lxor.vo
0m00.42s | 37240 ko | fiat-go/64/curve25519solinas/curve25519solinas.go
0m00.42s | 39236 ko | fiat-json/src/curve25519_solinas_64.json
0m00.42s | 36340 ko | fiat-zig/src/curve25519_solinas_64.zig
0m00.42s | 422916 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo
0m00.42s | 411132 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo
0m00.42s | 442280 ko | rupicola/src/Rupicola/Examples/Cells/Cells.vo
0m00.41s | 470096 ko | Arithmetic/FLia.vo
0m00.41s | 433732 ko | Util/ZUtil/Land.vo
0m00.41s | 35504 ko | fiat-c/src/curve25519_solinas_64.c
0m00.41s | 431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo
0m00.41s | 429580 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder.vo
0m00.41s | 430800 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo
0m00.41s | 423376 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo
0m00.41s | 438972 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo
0m00.41s | 438804 ko | rupicola/src/Rupicola/Lib/Alloc.vo
0m00.41s | 437364 ko | rupicola/src/Rupicola/Lib/SepReflection.vo
0m00.40s | 428624 ko | Util/Listable.vo
0m00.40s | 384448 ko | Util/Sum.vo
0m00.40s | 36040 ko | fiat-rust/src/curve25519_solinas_64.rs
0m00.40s | 461144 ko | rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo
0m00.40s | 425220 ko | rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo
0m00.39s | 395832 ko | Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.vo
0m00.39s | 441064 ko | Rewriter/Language/Reify.vo
0m00.39s | 426988 ko | Util/ZBounded.vo
0m00.39s | 429644 ko | Util/ZUtil/Divide/Bool.vo
0m00.39s | 400344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoExports.vo
0m00.39s | 415396 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo
0m00.39s | 421432 ko | rupicola/src/Rupicola/Examples/KVStore/kv.vo
0m00.38s | 412772 ko | Util/ListUtil/GroupAllBy.vo
0m00.38s | 431556 ko | Util/ZUtil/EquivModulo.vo
0m00.38s | 422764 ko | rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo
0m00.38s | 411464 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo
0m00.38s | 417720 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo
0m00.38s | 420828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo
0m00.38s | 426000 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo
0m00.38s | 405528 ko | rupicola/src/Rupicola/Examples/CRC32/Table.vo
0m00.37s | 430116 ko | Arithmetic/ModularArithmeticPre.vo
0m00.37s | 413572 ko | Language/IdentifierParameters.vo
0m00.37s | 420780 ko | Util/HList.vo
0m00.37s | 422648 ko | Util/Level.vo
0m00.37s | 426960 ko | Util/ZRange.vo
0m00.37s | 420356 ko | Util/ZUtil/Ltz.vo
0m00.37s | 426472 ko | Util/ZUtil/Pow.vo
0m00.37s | 427680 ko | rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo
0m00.37s | 431904 ko | rupicola/bedrock2/bedrock2/src/bedrock2/RecordPredicates.vo
0m00.37s | 427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/chacha20.vo
0m00.37s | 438128 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo
0m00.37s | 443552 ko | rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo
0m00.37s | 430788 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo
0m00.37s | 424720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo
0m00.37s | 443060 ko | rupicola/src/Rupicola/Examples/IO/Writer.vo
0m00.36s | 385140 ko | Coqprime/List/UList.vo
0m00.36s | 419844 ko | Util/Structures/Equalities/List.vo
0m00.36s | 427828 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo
0m00.36s | 419892 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo
0m00.36s | 417232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo
0m00.36s | 426352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo
0m00.36s | 443080 ko | rupicola/src/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
0m00.35s | 385364 ko | Coqprime/List/Permutation.vo
0m00.35s | 384172 ko | Rewriter/Util/Sum.vo
0m00.35s | 429404 ko | Util/Strings/Show.vo
0m00.35s | 412512 ko | Util/Strings/String.vo
0m00.35s | 421004 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Result.vo
0m00.35s | 439560 ko | rupicola/src/Rupicola/Lib/Conditionals.vo
0m00.34s | 408188 ko | Coqprime/PrimalityTest/IGroup.vo
0m00.34s | 393816 ko | Language/PreExtra.vo
0m00.34s | 402648 ko | Rewriter/TestRules.vo
0m00.34s | 412756 ko | Rewriter/Util/Strings/ParseArithmetic.vo
0m00.34s | 393864 ko | Util/Strings/String_as_OT_old.vo
0m00.34s | 410768 ko | Util/ZUtil/CPS.vo
0m00.34s | 415816 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Demos.vo
0m00.34s | 401728 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo
0m00.33s | 375960 ko | Util/ZUtil.vo
0m00.33s | 400708 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLib.vo
0m00.33s | 414856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo
0m00.33s | 375792 ko | rupicola/src/Rupicola/Examples/KVStore/Tactics.vo
0m00.33s | 398752 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
0m00.32s | 409072 ko | Coqprime/PrimalityTest/Euler.vo
0m00.32s | 424228 ko | Curves/Weierstrass/Affine.vo
0m00.32s | 354496 ko | Util/ZUtil/Lor.vo
0m00.32s | 353664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo
0m00.32s | 372204 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo
0m00.32s | 376436 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo
0m00.32s | 375132 ko | rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo
0m00.32s | 420972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo
0m00.32s | 369524 ko | rupicola/src/Rupicola/Lib/Api.vo
0m00.32s | 419200 ko | rupicola/src/Rupicola/Lib/Monads.vo
0m00.31s | 408224 ko | Coqprime/PrimalityTest/Lagrange.vo
0m00.31s | 375364 ko | Rewriter/Util/MSetPositive/Facts.vo
0m00.31s | 421500 ko | Spec/CompleteEdwardsCurve.vo
0m00.31s | 377312 ko | Util/MSets/MSetPositive/Facts.vo
0m00.31s | 377252 ko | Util/Strings/Sorting.vo
0m00.31s | 351748 ko | Util/ZUtil/Land/Fold.vo
0m00.31s | 355732 ko | Util/ZUtil/Tactics/SolveRange.vo
0m00.30s | 384652 ko | Algebra/Monoid.vo
0m00.30s | 383176 ko | Coqprime/List/ListAux.vo
0m00.30s | 342728 ko | Util/Strings/Show/Enum.vo
0m00.30s | 391212 ko | Util/Structures/Orders/Unit.vo
0m00.30s | 319900 ko | Util/ZUtil/Tactics.vo
0m00.30s | 350824 ko | Util/ZUtil/Tactics/SolveTestbit.vo
0m00.30s | 353168 ko | rupicola/bedrock2/bedrock2/src/bedrock2/safe_f_equal.vo
0m00.30s | 368372 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo
0m00.30s | 357516 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo
0m00.30s | 379772 ko | rupicola/src/Rupicola/Lib/Notations.vo
0m00.30s | 364432 ko | rupicola/src/Rupicola/Lib/Tactics.vo
0m00.30s | 357996 ko | rupicola/src/Rupicola/Lib/WordNotations.vo
0m00.29s | 364272 ko | Rewriter/TestRulesProofs.vo
0m00.29s | 333924 ko | Spec/ModularArithmetic.vo
0m00.29s | 25660 ko | fiat-go/32/poly1305/poly1305.go
0m00.29s | 352048 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo
0m00.29s | 345272 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo
0m00.29s | 341028 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCallsExports.vo
0m00.29s | 349008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo
0m00.29s | 354512 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
0m00.29s | 338736 ko | rupicola/src/Rupicola/Examples/Swap/Swap.vo
0m00.29s | 381560 ko | rupicola/src/Rupicola/Lib/Invariants.vo
0m00.29s | 411108 ko | rupicola/src/Rupicola/Lib/ToCString.vo
0m00.28s | 392356 ko | Rewriter/Language/UnderLets.vo
0m00.28s | 382364 ko | Util/Structures/Equalities/Sum.vo
0m00.28s | 378252 ko | Util/Structures/Orders/Empty.vo
0m00.28s | 360100 ko | Util/Structures/Orders/Iso.vo
0m00.28s | 342356 ko | Util/ZUtil/Tactics/Ztestbit.vo
0m00.28s | 310160 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifyHeapletwise.vo
0m00.28s | 334436 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo
0m00.28s | 342680 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediateDef.vo
0m00.28s | 354192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo
0m00.27s | 385140 ko | Coqprime/List/Iterator.vo
0m00.27s | 367396 ko | Curves/Montgomery/XZ.vo
0m00.27s | 337868 ko | Rewriter/Util/MSetPositive/Equality.vo
0m00.27s | 347388 ko | Util/ListUtil/SetoidList.vo
0m00.27s | 369612 ko | Util/ZUtil/Combine.vo
0m00.27s | 379216 ko | Util/ZUtil/Le.vo
0m00.27s | 349972 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo
0m00.27s | 377088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo
0m00.27s | 379772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo
0m00.26s | 368384 ko | Rewriter/Util/Strings/String.vo
0m00.26s | 376924 ko | Util/ZUtil/Peano.vo
0m00.26s | 360084 ko | Util/ZUtil/Tactics/LtbToLt.vo
0m00.26s | 340944 ko | Util/ZUtil/Tactics/RewriteModSmall.vo
0m00.26s | 32592 ko | fiat-bedrock2/src/poly1305_32.c
0m00.26s | 346712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb_spec.vo
0m00.26s | 339000 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo
0m00.26s | 377484 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo
0m00.26s | 385172 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo
0m00.25s | 334716 ko | Util/ListUtil/Filter.vo
0m00.25s | 338148 ko | Util/MSets/MSetPositive/Equality.vo
0m00.25s | 362452 ko | Util/ZRange/Operations.vo
0m00.25s | 325960 ko | Util/ZUtil/Tactics/LinearSubstitute.vo
0m00.25s | 29108 ko | fiat-json/src/poly1305_32.json
0m00.25s | 288032 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo
0m00.25s | 292340 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo
0m00.25s | 389460 ko | rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo
0m00.25s | 337192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo
0m00.25s | 374904 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo
0m00.25s | 325428 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo
0m00.24s | 311644 ko | Algebra/Nsatz.vo
0m00.24s | 326236 ko | Arithmetic/MontgomeryReduction/Definition.vo
0m00.24s | 360664 ko | Util/AdditionChainExponentiation.vo
0m00.24s | 322652 ko | Util/MSets/Show.vo
0m00.24s | 340708 ko | Util/NUtil/WithoutReferenceToZ.vo
0m00.24s | 318760 ko | Util/ZRange/Show.vo
0m00.24s | 328440 ko | Util/ZUtil/Odd.vo
0m00.24s | 308944 ko | Util/ZUtil/Opp.vo
0m00.24s | 316532 ko | Util/ZUtil/Tactics/RewriteModDivide.vo
0m00.24s | 321008 ko | rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo
0m00.24s | 353544 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo
0m00.24s | 341560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo
0m00.23s | 300228 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo
0m00.23s | 377268 ko | Coqprime/List/ZProgression.vo
0m00.23s | 313720 ko | Rewriter/Util/Option.vo
0m00.23s | 320764 ko | Util/ErrorT/Show.vo
0m00.23s | 333864 ko | Util/ListUtil/Permutation.vo
0m00.23s | 323108 ko | Util/NUtil/Testbit.vo
0m00.23s | 286696 ko | Util/Strings/StringMap.vo
0m00.23s | 348464 ko | Util/Structures/Equalities/Prod.vo
0m00.23s | 25268 ko | fiat-java/src/FiatPoly1305.java
0m00.23s | 300056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo
0m00.23s | 314040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/RecordSetters.vo
0m00.22s | 333880 ko | Coqprime/PrimalityTest/FGroup.vo
0m00.22s | 310312 ko | Rewriter/Language/PreLemmas.vo
0m00.22s | 324896 ko | Rewriter/Language/UnderLetsCacheProofs.vo
0m00.22s | 345352 ko | Rewriter/Util/ListUtil/SetoidList.vo
0m00.22s | 313848 ko | Util/Option.vo
0m00.22s | 291212 ko | Util/SideConditions/ModInvPackage.vo
0m00.22s | 287668 ko | Util/ZUtil/Definitions.vo
0m00.22s | 279424 ko | Util/ZUtil/Sgn.vo
0m00.22s | 321444 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo
0m00.22s | 259676 ko | Util/ZUtil/Tactics/SplitMinMax.vo
0m00.22s | 318104 ko | Util/ZUtil/Tactics/ZeroBounds.vo
0m00.22s | 23992 ko | fiat-c/src/poly1305_32.c
0m00.22s | 24364 ko | fiat-rust/src/poly1305_32.rs
0m00.22s | 24480 ko | fiat-zig/src/poly1305_32.zig
0m00.22s | 312072 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifySep.vo
0m00.22s | 299808 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepClause.vo
0m00.22s | 329056 ko | rupicola/bedrock2/compiler/src/compiler/mod4_0.vo
0m00.22s | 308236 ko | rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo
0m00.22s | 298992 ko | rupicola/bedrock2/compiler/src/compiler/util/Common.vo
0m00.22s | 315128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Byte.vo
0m00.22s | 336016 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo
0m00.22s | 289828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo
0m00.22s | 299720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo
0m00.22s | 314352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo
0m00.22s | 300972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo
0m00.21s | 315792 ko | Util/IdfunWithAlt.vo
0m00.21s | 262576 ko | Util/NUtil/Sorting.vo
0m00.21s | 292716 ko | Util/Strings/Parse/Common.vo
0m00.21s | 265724 ko | Util/ZUtil/Hints/PullPush.vo
0m00.21s | 310364 ko | Util/ZUtil/Z2Nat.vo
0m00.21s | 305796 ko | Util/ZUtil/ZSimplify/Simple.vo
0m00.21s | 273568 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListIndexNotations.vo
0m00.21s | 277260 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepBulletPoints.vo
0m00.21s | 283964 ko | rupicola/bedrock2/bedrock2/src/bedrock2/cancel_div.vo
0m00.21s | 313100 ko | rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo
0m00.21s | 359956 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo
0m00.21s | 274236 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo
0m00.21s | 328060 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo
0m00.21s | 310856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SoftmulInsts.vo
0m00.21s | 301280 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo
0m00.21s | 278812 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo
0m00.21s | 276044 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo
0m00.21s | 307864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo
0m00.21s | 294416 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/D…
Although we can't add the p434_32 file for Java, as it exceeds the 65535
byte per-method codesize limit, giving
```
fiat-java/src/FiatP434.java:136: error: code too large
public static void fiat_P434_mul(int[] out1, final int[] arg1, final int[] arg2) {
^
fiat-java/src/FiatP434.java:3778: error: code too large
public static void fiat_P434_square(int[] out1, final int[] arg1) {
^
fiat-java/src/FiatP434.java:10139: error: code too large
public static void fiat_P434_to_montgomery(int[] out1, final int[] arg1) {
^
```
<details><summary>Timing</summary>
<p>
```
Time | Peak Mem | File Name
-------------------------------------------------------------------------------------------------------------------
254m50.98s | 3857976 ko | Total Time / Peak Mem
-------------------------------------------------------------------------------------------------------------------
9m09.24s | 2340948 ko | Bedrock/End2End/X25519/GarageDoor.vo
6m52.61s | 2067876 ko | Curves/Weierstrass/AffineProofs.vo
5m24.81s | 2846272 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo
4m43.41s | 3857976 ko | fiat-json/src/p434_32.json
4m41.94s | 3549180 ko | fiat-java/src/FiatP434.java
4m40.51s | 3510128 ko | fiat-go/32/p434/p434.go
4m38.01s | 3112012 ko | fiat-rust/src/p434_32.rs
4m36.06s | 1005000 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo
4m35.63s | 3460760 ko | fiat-c/src/p434_32.c
4m24.81s | 3479832 ko | fiat-bedrock2/src/p434_32.c
4m21.82s | 1805944 ko | Curves/EdwardsMontgomery.vo
4m16.62s | 969388 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo
4m05.49s | 3689096 ko | fiat-zig/src/p434_32.zig
4m02.12s | 2558072 ko | Assembly/WithBedrock/Proofs.vo
3m45.39s | 1784600 ko | Rewriter/Passes/ArithWithCasts.vo
3m21.77s | 3298648 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo
3m14.18s | 2606244 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo
3m01.52s | 1449620 ko | Curves/Weierstrass/Projective.vo
2m51.65s | 781792 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo
2m43.49s | 1590284 ko | Curves/Montgomery/XZProofs.vo
2m41.57s | 1467320 ko | Curves/Montgomery/AffineProofs.vo
2m30.06s | 1114396 ko | Fancy/Compiler.vo
2m16.49s | 1561432 ko | Rewriter/Passes/NBE.vo
1m58.96s | 2787304 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo
1m56.94s | 2010232 ko | fiat-json/src/p384_scalar_32.json
1m54.69s | 442236 ko | Spec/Test/X25519.vo
1m54.17s | 2271728 ko | fiat-bedrock2/src/p384_scalar_32.c
1m53.70s | 1745936 ko | fiat-zig/src/p384_32.zig
1m53.52s | 2115820 ko | fiat-go/32/p384/p384.go
1m53.19s | 1674280 ko | fiat-json/src/p384_32.json
1m53.14s | 1628960 ko | fiat-java/src/FiatP384.java
1m53.05s | 1699924 ko | fiat-rust/src/p384_scalar_32.rs
1m52.61s | 1822712 ko | fiat-bedrock2/src/p384_32.c
1m51.65s | 1604284 ko | Bedrock/End2End/X25519/Field25519.vo
1m51.49s | 1435476 ko | Rewriter/Passes/ToFancyWithCasts.vo
1m51.33s | 1635188 ko | fiat-c/src/p384_scalar_32.c
1m49.51s | 1953272 ko | fiat-rust/src/p384_32.rs
1m49.44s | 2074092 ko | fiat-c/src/p384_32.c
1m47.54s | 2392824 ko | Fancy/Barrett256.vo
1m46.52s | 1924084 ko | fiat-go/32/p384scalar/p384scalar.go
1m46.35s | 1693196 ko | fiat-zig/src/p384_scalar_32.zig
1m45.28s | 2107680 ko | fiat-java/src/FiatP384Scalar.java
1m33.15s | 860988 ko | Util/FSets/FMapTrie.vo
1m28.26s | 2040924 ko | SlowPrimeSynthesisExamples.vo
1m22.76s | 744076 ko | rupicola/bedrock2/compiler/src/compiler/MMIO.vo
1m21.24s | 607772 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo
1m20.59s | 1528152 ko | Assembly/EquivalenceProofs.vo
1m20.11s | 750284 ko | Arithmetic/SolinasReduction.vo
1m19.98s | 1135724 ko | UnsaturatedSolinasHeuristics/Tests.vo
1m19.07s | 1580872 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo
1m16.09s | 1015848 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo
1m09.19s | 1436812 ko | Assembly/WithBedrock/SymbolicProofs.vo
1m07.33s | 803216 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo
1m04.55s | 881276 ko | AbstractInterpretation/Wf.vo
1m04.51s | 931300 ko | Curves/Weierstrass/Jacobian.vo
1m03.62s | 782744 ko | Rewriter/Rewriter/Wf.vo
0m59.64s | 704332 ko | Rewriter/RulesProofs.vo
0m57.69s | 733928 ko | Rewriter/Language/UnderLetsProofs.vo
0m56.72s | 1004580 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo
0m53.99s | 833600 ko | AbstractInterpretation/ZRangeProofs.vo
0m53.23s | 1044640 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo
0m52.35s | 944996 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo
0m51.52s | 625496 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo
0m51.41s | 1011348 ko | Rewriter/Rewriter/Examples.vo
0m51.35s | 1023708 ko | Rewriter/Passes/MultiRetSplit.vo
0m50.98s | 831264 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo
0m50.20s | 1302956 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo
0m47.60s | 584048 ko | Demo.vo
0m46.50s | 854544 ko | Rewriter/Rewriter/InterpProofs.vo
0m45.91s | 1745024 ko | Fancy/Montgomery256.vo
0m45.90s | 804912 ko | Rewriter/Rewriter/ProofsCommon.vo
0m44.99s | 1530768 ko | Assembly/Symbolic.vo
0m44.72s | 1102468 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo
0m44.72s | 2147808 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery
0m43.59s | 2147776 ko | ExtractionOCaml/bedrock2_solinas_reduction
0m43.31s | 2147552 ko | ExtractionOCaml/solinas_reduction
0m42.97s | 2147820 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery
0m41.82s | 67656 ko | fiat-go/32/p521/p521.go
0m41.14s | 569868 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo
0m41.05s | 625248 ko | rupicola/bedrock2/compiler/src/compiler/Spilling.vo
0m41.01s | 2148412 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas
0m40.68s | 2148192 ko | ExtractionOCaml/bedrock2_unsaturated_solinas
0m40.68s | 1072812 ko | Rewriter/Passes/Arith.vo
0m40.36s | 2147748 ko | ExtractionOCaml/word_by_word_montgomery
0m39.88s | 1003376 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo
0m38.76s | 60548 ko | fiat-java/src/FiatP521.java
0m38.74s | 142728 ko | fiat-bedrock2/src/p521_32.c
0m38.68s | 110444 ko | fiat-json/src/p521_32.json
0m38.44s | 58400 ko | fiat-zig/src/p521_32.zig
0m38.17s | 1691492 ko | ExtractionOCaml/unsaturated_solinas
0m37.93s | 1633424 ko | ExtractionOCaml/bedrock2_dettman_multiplication
0m37.93s | 59156 ko | fiat-c/src/p521_32.c
0m37.73s | 1623156 ko | ExtractionOCaml/with_bedrock2_saturated_solinas
0m37.70s | 708548 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo
0m37.54s | 1624828 ko | ExtractionOCaml/with_bedrock2_base_conversion
0m37.33s | 1624096 ko | ExtractionOCaml/bedrock2_saturated_solinas
0m37.21s | 1622976 ko | ExtractionOCaml/with_bedrock2_solinas_reduction
0m37.17s | 1620288 ko | ExtractionOCaml/bedrock2_base_conversion
0m36.76s | 1623680 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication
0m35.29s | 1415796 ko | ExtractionOCaml/dettman_multiplication
0m34.64s | 1538708 ko | ExtractionOCaml/base_conversion
0m34.35s | 60732 ko | fiat-rust/src/p521_32.rs
0m34.33s | 1415896 ko | ExtractionOCaml/saturated_solinas
0m34.18s | 2237120 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml
0m33.80s | 2211416 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
0m33.32s | 2211048 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
0m33.32s | 877940 ko | Rewriter/Passes/MulSplit.vo
0m33.30s | 1255200 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo
0m32.38s | 2133140 ko | ExtractionOCaml/solinas_reduction.ml
0m32.05s | 566656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo
0m31.56s | 1232064 ko | ExtractionOCaml/perf_word_by_word_montgomery
0m31.38s | 2108664 ko | ExtractionOCaml/word_by_word_montgomery.ml
0m30.75s | 1232248 ko | ExtractionOCaml/perf_unsaturated_solinas
0m30.68s | 2116064 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
0m30.48s | 617376 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo
0m30.13s | 2115380 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
0m30.01s | 1516352 ko | StandaloneDebuggingExamples.vo
0m29.81s | 702960 ko | AbstractInterpretation/Proofs.vo
0m28.53s | 2028924 ko | ExtractionOCaml/unsaturated_solinas.ml
0m28.11s | 664744 ko | rupicola/src/Rupicola/Examples/Utf8/Utf8.vo
0m27.87s | 876328 ko | Rewriter/Rewriter/Examples/PrefixSums.vo
0m27.32s | 2051412 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml
0m26.62s | 687116 ko | Rewriter/Language/Wf.vo
0m26.58s | 2005604 ko | ExtractionOCaml/bedrock2_base_conversion.ml
0m26.45s | 1996160 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
0m26.36s | 2005536 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
0m26.27s | 1996184 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml
0m26.18s | 1999292 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
0m26.15s | 1998300 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml
0m25.87s | 590672 ko | Rewriter/Language/Inversion.vo
0m25.26s | 1371200 ko | PerfTesting/PerfTestSearch.vo
0m25.09s | 1938912 ko | ExtractionOCaml/dettman_multiplication.ml
0m24.54s | 1924440 ko | ExtractionOCaml/saturated_solinas.ml
0m24.23s | 1921016 ko | ExtractionOCaml/base_conversion.ml
0m23.60s | 1179724 ko | PushButtonSynthesis/UnsaturatedSolinas.vo
0m23.31s | 874692 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo
0m22.72s | 499960 ko | Arithmetic/Saturated.vo
0m21.95s | 1329776 ko | Bedrock/End2End/RupicolaCrypto/Low.vo
0m20.78s | 813596 ko | Bedrock/Field/Translation/Proofs/Expr.vo
0m20.30s | 1149392 ko | PushButtonSynthesis/WordByWordMontgomery.vo
0m20.07s | 747300 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo
0m19.54s | 629200 ko | Util/FSets/FMapBool.vo
0m19.45s | 694948 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.vo
0m19.35s | 1838828 ko | ExtractionOCaml/perf_unsaturated_solinas.ml
0m19.22s | 680380 ko | rupicola/bedrock2/compiler/src/compiler/FlatImp.vo
0m19.16s | 1828412 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
0m18.94s | 313308 ko | fiat-go/64/p434/p434.go
0m18.72s | 244116 ko | fiat-zig/src/p434_64.zig
0m18.38s | 634116 ko | Util/FSets/FMapProd.vo
0m17.79s | 281552 ko | fiat-json/src/p434_64.json
0m17.78s | 487432 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c
0m17.74s | 1370888 ko | PerfTesting/PerfTestSearchPattern.vo
0m17.71s | 302348 ko | fiat-bedrock2/src/p434_64.c
0m17.68s | 431072 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig
0m17.67s | 379652 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json
0m17.58s | 1155688 ko | Bedrock/Field/Translation/Proofs/Cmd.vo
0m17.52s | 255060 ko | fiat-c/src/p434_64.c
0m17.50s | 1128196 ko | Bedrock/Field/Translation/Proofs/Func.vo
0m17.50s | 397092 ko | fiat-bedrock2/src/p256_scalar_32.c
0m17.41s | 1120356 ko | Bedrock/End2End/Poly1305/Field1305.vo
0m17.33s | 376544 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
0m17.32s | 373956 ko | fiat-json/src/p256_scalar_32.json
0m17.30s | 407340 ko | fiat-json/src/secp256k1_montgomery_32.json
0m17.26s | 567160 ko | Util/FSets/FMapSum.vo
0m17.26s | 363444 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java
0m17.20s | 306884 ko | fiat-rust/src/p434_64.rs
0m17.17s | 1109240 ko | Assembly/Parse/TestAsm.vo
0m17.17s | 438860 ko | fiat-java/src/FiatP256Scalar.java
0m17.13s | 413312 ko | fiat-go/32/p256scalar/p256scalar.go
0m17.06s | 415760 ko | fiat-json/src/curve25519_scalar_32.json
0m17.03s | 396804 ko | fiat-zig/src/secp256k1_montgomery_32.zig
0m16.90s | 395476 ko | fiat-bedrock2/src/curve25519_scalar_32.c
0m16.90s | 436536 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c
0m16.88s | 422848 ko | fiat-java/src/FiatSecp256K1Montgomery.java
0m16.85s | 542932 ko | Arithmetic/WordByWordMontgomery.vo
0m16.84s | 344632 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go
0m16.79s | 384576 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c
0m16.77s | 345256 ko | fiat-rust/src/p256_scalar_32.rs
0m16.68s | 323816 ko | fiat-java/src/FiatCurve25519Scalar.java
0m16.64s | 340412 ko | fiat-go/32/curve25519scalar/curve25519scalar.go
0m16.63s | 620464 ko | Util/ZUtil/ArithmeticShiftr.vo
0m16.63s | 407304 ko | fiat-zig/src/curve25519_scalar_32.zig
0m16.60s | 1200944 ko | Bedrock/Field/Synthesis/New/Signature.vo
0m16.60s | 365388 ko | fiat-c/src/p256_scalar_32.c
0m16.57s | 368480 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs
0m16.53s | 833896 ko | Curves/Edwards/XYZT/Basic.vo
0m16.50s | 2124656 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs
0m16.39s | 2120524 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs
0m16.38s | 432820 ko | fiat-json/src/p256_32.json
0m16.37s | 430104 ko | fiat-zig/src/p256_scalar_32.zig
0m16.35s | 330524 ko | fiat-c/src/curve25519_scalar_32.c
0m16.32s | 349716 ko | fiat-zig/src/p256_32.zig
0m16.27s | 2013724 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs
0m16.24s | 364604 ko | fiat-rust/src/curve25519_scalar_32.rs
0m16.19s | 402376 ko | fiat-rust/src/secp256k1_montgomery_32.rs
0m16.04s | 765616 ko | Language/IdentifiersGENERATED.vo
0m16.01s | 563772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo
0m16.00s | 573536 ko | Bedrock/Field/Synthesis/Examples/redc.vo
0m15.97s | 2014024 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs
0m15.89s | 421264 ko | fiat-c/src/secp256k1_montgomery_32.c
0m15.84s | 364416 ko | fiat-java/src/FiatP256.java
0m15.77s | 395208 ko | fiat-bedrock2/src/p256_32.c
0m15.71s | 1964864 ko | ExtractionHaskell/solinas_reduction.hs
0m15.69s | 323896 ko | fiat-c/src/p256_32.c
0m15.66s | 726776 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo
0m15.62s | 405156 ko | fiat-go/32/p256/p256.go
0m15.55s | 766356 ko | Curves/Edwards/AffineProofs.vo
0m15.37s | 568164 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo
0m15.33s | 370928 ko | fiat-rust/src/p256_32.rs
0m15.29s | 1983440 ko | ExtractionHaskell/word_by_word_montgomery.hs
0m15.19s | 520360 ko | Arithmetic/BarrettReduction.vo
0m15.12s | 425240 ko | rupicola/bedrock2/deps/coqutil/test/TestGoals.vo
0m14.91s | 516204 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo
0m14.84s | 1909292 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs
0m14.83s | 596008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo
0m14.79s | 463028 ko | Algebra/Field.vo
0m14.67s | 1999460 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs
0m14.66s | 1860044 ko | ExtractionHaskell/unsaturated_solinas.hs
0m14.61s | 1998800 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs
0m14.55s | 487988 ko | rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo
0m14.49s | 565196 ko | Util/FSets/FMapOption.vo
0m14.47s | 1910172 ko | ExtractionHaskell/bedrock2_base_conversion.hs
0m14.45s | 1896592 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs
0m14.35s | 1917576 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs
0m14.30s | 1897756 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs
0m14.22s | 1917456 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs
0m14.19s | 593376 ko | Language/IdentifiersGENERATEDProofs.vo
0m14.13s | 526388 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo
0m14.01s | 660304 ko | Bedrock/Group/AdditionChains.vo
0m13.89s | 462944 ko | Util/Structures/Orders/Prod.vo
0m13.85s | 491540 ko | rupicola/src/Rupicola/Examples/Arrays.vo
0m13.83s | 544744 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo
0m13.79s | 498032 ko | rupicola/src/Rupicola/Examples/CMove/CMove.vo
0m13.77s | 598308 ko | Bedrock/Field/Common/Util.vo
0m13.61s | 1811276 ko | ExtractionHaskell/dettman_multiplication.hs
0m13.60s | 1846816 ko | ExtractionHaskell/saturated_solinas.hs
0m13.55s | 492116 ko | rupicola/src/Rupicola/Examples/Loops.vo
0m13.46s | 538316 ko | rupicola/src/Rupicola/Examples/KVStore/Manual.vo
0m13.27s | 1793716 ko | ExtractionHaskell/base_conversion.hs
0m13.21s | 649252 ko | Bedrock/Group/ScalarMult/LadderStep.vo
0m12.82s | 494032 ko | Arithmetic/Core.vo
0m11.93s | 1026788 ko | BoundsPipeline.vo
0m11.86s | 637944 ko | Rewriter/Demo.vo
0m11.73s | 545076 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo
0m11.72s | 707092 ko | Util/ZRange/LandLorBounds.vo
0m11.52s | 484076 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo
0m11.38s | 1677648 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo
0m11.28s | 165124 ko | fiat-go/64/p384scalar/p384scalar.go
0m11.23s | 153540 ko | fiat-c/src/p384_scalar_64.c
0m11.20s | 197432 ko | fiat-json/src/p384_scalar_64.json
0m11.13s | 192732 ko | fiat-bedrock2/src/p384_scalar_64.c
0m11.10s | 165668 ko | fiat-zig/src/p384_scalar_64.zig
0m11.00s | 658176 ko | rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo
0m10.96s | 165272 ko | fiat-rust/src/p384_scalar_64.rs
0m10.65s | 505684 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo
0m10.64s | 476416 ko | Primitives/MxDHRepChange.vo
0m10.41s | 742196 ko | Assembly/Syntax.vo
0m10.37s | 1339924 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo
0m10.32s | 459448 ko | Util/Structures/Orders/List.vo
0m10.24s | 451276 ko | Algebra/Ring.vo
0m10.12s | 622652 ko | Bedrock/Field/Translation/Proofs/Flatten.vo
0m10.02s | 579416 ko | PushButtonSynthesis/BYInversionReificationCache.vo
0m09.85s | 182968 ko | fiat-c/src/p384_64.c
0m09.77s | 173092 ko | fiat-json/src/p384_64.json
0m09.76s | 164688 ko | fiat-go/64/p384/p384.go
0m09.66s | 139760 ko | fiat-zig/src/p384_64.zig
0m09.62s | 872852 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo
0m09.59s | 250704 ko | fiat-zig/src/p224_32.zig
0m09.52s | 238320 ko | fiat-json/src/p224_32.json
0m09.49s | 230008 ko | fiat-go/32/p224/p224.go
0m09.47s | 203968 ko | fiat-bedrock2/src/p384_64.c
0m09.47s | 272744 ko | fiat-java/src/FiatP224.java
0m09.43s | 658732 ko | Bedrock/Group/ScalarMult/CSwap.vo
0m09.43s | 595324 ko | Stringification/IR.vo
0m09.40s | 558640 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo
0m09.37s | 554444 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo
0m09.32s | 258236 ko | fiat-bedrock2/src/p224_32.c
0m09.29s | 177692 ko | fiat-rust/src/p384_64.rs
0m09.28s | 1030020 ko | PushButtonSynthesis/BaseConversion.vo
0m09.27s | 270084 ko | fiat-c/src/p224_32.c
0m09.24s | 550836 ko | rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo
0m09.10s | 230652 ko | fiat-rust/src/p224_32.rs
0m09.01s | 506588 ko | Rewriter/Language/IdentifiersLibraryProofs.vo
0m08.90s | 497908 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI.vo
0m08.58s | 123780 ko | fiat-json/src/p448_solinas_32.json
0m08.35s | 600540 ko | Language/IdentifiersBasicGENERATED.vo
0m08.33s | 1038828 ko | PushButtonSynthesis/Primitives.vo
0m08.23s | 998908 ko | PushButtonSynthesis/SmallExamples.vo
0m08.15s | 785760 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo
0m08.14s | 912272 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo
0m08.14s | 59548 ko | fiat-rust/src/p448_solinas_32.rs
0m08.03s | 58124 ko | fiat-zig/src/p448_solinas_32.zig
0m07.90s | 58212 ko | fiat-c/src/p448_solinas_32.c
0m07.80s | 527792 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.vo
0m07.77s | 462448 ko | rupicola/src/Rupicola/Examples/KVStore/Automated.vo
0m07.70s | 587264 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo
0m07.52s | 491008 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.vo
0m07.45s | 471188 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo
0m07.44s | 468880 ko | Util/ZRange/CornersMonotoneBounds.vo
0m07.26s | 1031232 ko | PushButtonSynthesis/SolinasReduction.vo
0m07.15s | 659224 ko | Util/FSets/FMapTrieEx.vo
0m06.85s | 471788 ko | rupicola/src/Rupicola/Examples/L64X128.vo
0m06.84s | 708648 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo
0m06.79s | 459008 ko | rupicola/src/Rupicola/Examples/Expr.vo
0m06.74s | 450284 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add.vo
0m06.54s | 492712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/bsearch.vo
0m06.50s | 546780 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo
0m06.41s | 467236 ko | Arithmetic/FancyMontgomeryReduction.vo
0m06.37s | 1134776 ko | CLI.vo
0m06.33s | 49900 ko | fiat-go/64/p521/p521.go
0m06.32s | 1037180 ko | PushButtonSynthesis/BarrettReduction.vo
0m06.31s | 679460 ko | Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo
0m06.31s | 457988 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo
0m06.19s | 458048 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo
0m06.18s | 1132992 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo
0m06.16s | 543604 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo
0m06.06s | 902704 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo
0m06.06s | 438980 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo
0m06.05s | 574516 ko | Rewriter/Passes/NoSelect.vo
0m06.03s | 480020 ko | rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo
0m06.01s | 671264 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo
0m05.97s | 486436 ko | Util/ZUtil/Modulo.vo
0m05.86s | 466112 ko | Util/ListUtil.vo
0m05.85s | 469760 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo
0m05.57s | 51132 ko | fiat-json/src/p521_64.json
0m05.56s | 682812 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.vo
0m05.54s | 65620 ko | fiat-bedrock2/src/p521_64.c
0m05.51s | 36024 ko | fiat-zig/src/p521_64.zig
0m05.45s | 460124 ko | Util/MSets/MSetSum.vo
0m05.45s | 36640 ko | fiat-c/src/p521_64.c
0m05.43s | 532688 ko | Fancy/Prod.vo
0m05.41s | 576128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo
0m05.40s | 614228 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo
0m05.40s | 36120 ko | fiat-rust/src/p521_64.rs
0m05.36s | 461088 ko | rupicola/bedrock2/compiler/src/compiler/ExprImp.vo
0m05.28s | 453952 ko | Rewriter/Util/ListUtil.vo
0m05.12s | 513604 ko | Arithmetic/BYInv.vo
0m05.10s | 454392 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FlatConstMem.vo
0m04.95s | 470428 ko | rupicola/src/Rupicola/Lib/Loops.vo
0m04.94s | 467968 ko | Util/FsatzAutoLemmas.vo
0m04.93s | 432264 ko | Spec/Curve25519.vo
0m04.83s | 462000 ko | rupicola/src/Rupicola/Examples/CRC32/CRC32.vo
0m04.73s | 498572 ko | Curves/Edwards/Pre.vo
0m04.72s | 550548 ko | Language/InversionExtra.vo
0m04.61s | 455752 ko | Util/FSets/FMapIso.vo
0m04.59s | 448220 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.vo
0m04.55s | 472888 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo
0m04.49s | 1063260 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo
0m04.42s | 465320 ko | Util/ZRange/BasicLemmas.vo
0m04.38s | 445356 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo
0m04.38s | 444300 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo
0m04.37s | 1028072 ko | PushButtonSynthesis/DettmanMultiplication.vo
0m04.32s | 1034544 ko | PushButtonSynthesis/SaturatedSolinas.vo
0m04.28s | 553116 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo
0m04.26s | 460864 ko | Util/FSets/FMapSect.vo
0m04.24s | 434096 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/BenchCancel256.vo
0m04.24s | 470912 ko | rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo
0m04.19s | 446352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo
0m04.18s | 955212 ko | Assembly/Equivalence.vo
0m04.13s | 445192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo
0m04.10s | 474136 ko | Algebra/Field_test.vo
0m04.02s | 434628 ko | Arithmetic/MontgomeryReduction/Proofs.vo
0m04.00s | 470212 ko | Rewriter/Language/IdentifiersBasicLibrary.vo
0m03.97s | 492300 ko | COperationSpecifications.vo
0m03.96s | 1483248 ko | Bedrock/Everything.vo
0m03.95s | 565888 ko | Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo
0m03.92s | 461212 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memequal.vo
0m03.89s | 438292 ko | rupicola/src/Rupicola/Examples/Cells/IndirectAdd.vo
0m03.84s | 1047084 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo
0m03.76s | 460392 ko | rupicola/src/Rupicola/Examples/Uppercase.vo
0m03.74s | 487816 ko | Curves/Montgomery/Affine.vo
0m03.62s | 1341008 ko | Everything.vo
0m03.51s | 451668 ko | Arithmetic/BarrettReduction/Generalized.vo
0m03.50s | 456840 ko | CastLemmas.vo
0m03.49s | 545604 ko | PushButtonSynthesis/BaseConversionReificationCache.vo
0m03.47s | 415800 ko | rupicola/bedrock2/deps/coqutil/test/SlowGoals.vo
0m03.42s | 394996 ko | Algebra/Group.vo
0m03.42s | 453312 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memswap.vo
0m03.37s | 460156 ko | UnsaturatedSolinasHeuristics.vo
0m03.36s | 435964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo
0m03.35s | 454600 ko | Arithmetic/UniformWeight.vo
0m03.33s | 444692 ko | Util/ZUtil/LandLorShiftBounds.vo
0m03.27s | 448912 ko | rupicola/src/Rupicola/Examples/Arithmetic.vo
0m03.24s | 434864 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo
0m03.21s | 449104 ko | Arithmetic/BarrettReduction/HAC.vo
0m03.20s | 449096 ko | Util/ZUtil/LandLorBounds.vo
0m03.15s | 1006432 ko | Bedrock/Field/Translation/Cmd.vo
0m03.14s | 677116 ko | Bedrock/Group/ScalarMult/ScalarMult.vo
0m03.13s | 1070140 ko | Rewriter/PerfTesting/Core.vo
0m03.10s | 446044 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo
0m03.07s | 1343548 ko | PerfTesting/PerfTestPrint.vo
0m03.06s | 446136 ko | Util/Structures/Orders.vo
0m02.99s | 446820 ko | rupicola/src/Rupicola/Examples/RevComp.vo
0m02.97s | 1002728 ko | Bedrock/Field/Translation/Func.vo
0m02.95s | 1066612 ko | Bedrock/Field/Stringification/Stringification.vo
0m02.95s | 609264 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo
0m02.90s | 442416 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo
0m02.89s | 75160 ko | fiat-json/src/p256_scalar_64.json
0m02.84s | 411248 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo
0m02.84s | 61996 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go
0m02.82s | 84244 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c
0m02.82s | 72148 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json
0m02.80s | 1103808 ko | StandaloneOCamlMain.vo
0m02.80s | 84916 ko | fiat-bedrock2/src/p256_scalar_64.c
0m02.80s | 427948 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo
0m02.79s | 64876 ko | fiat-go/64/p256scalar/p256scalar.go
0m02.78s | 439896 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ipow.vo
0m02.77s | 1059012 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo
0m02.77s | 57088 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig
0m02.75s | 1143348 ko | Bedrock/Standalone/StandaloneHaskellMain.vo
0m02.75s | 431748 ko | Util/Structures/Orders/Option.vo
0m02.75s | 433944 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo
0m02.74s | 1103744 ko | StandaloneHaskellMain.vo
0m02.74s | 56376 ko | fiat-c/src/p256_scalar_64.c
0m02.74s | 60560 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs
0m02.74s | 451660 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediate.vo
0m02.73s | 61824 ko | fiat-zig/src/p256_scalar_64.zig
0m02.72s | 1064916 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo
0m02.71s | 519732 ko | Rewriter/Passes/Test.vo
0m02.71s | 61076 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c
0m02.71s | 60028 ko | fiat-rust/src/p256_scalar_64.rs
0m02.70s | 535708 ko | Rewriter/Passes/AddAssocLeft.vo
0m02.68s | 51016 ko | fiat-go/64/p448solinas/p448solinas.go
0m02.67s | 442740 ko | Arithmetic/Primitives.vo
0m02.65s | 438452 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap_by_add.vo
0m02.64s | 1143212 ko | Bedrock/Standalone/StandaloneOCamlMain.vo
0m02.60s | 443440 ko | rupicola/src/Rupicola/Examples/IO/Echo.vo
0m02.59s | 549304 ko | Util/FSets/FMapTrie/ShapeEx.vo
0m02.58s | 1129176 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo
0m02.58s | 434880 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo
0m02.57s | 621908 ko | Bedrock/Field/Interface/Compilation2.vo
0m02.56s | 1042648 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo
0m02.55s | 71208 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go
0m02.55s | 75224 ko | fiat-json/src/secp256k1_montgomery_64.json
0m02.54s | 1043268 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo
0m02.52s | 59660 ko | fiat-zig/src/secp256k1_montgomery_64.zig
0m02.50s | 1043292 ko | Bedrock/Field/Translation/Parameters/FE310.vo
0m02.48s | 426684 ko | Util/ZUtil/ZSimplify/Autogenerated.vo
0m02.48s | 68740 ko | fiat-json/src/curve25519_scalar_64.json
0m02.47s | 57260 ko | fiat-c/src/secp256k1_montgomery_64.c
0m02.46s | 1038448 ko | Bedrock/Field/Translation/Parameters/Defaults.vo
0m02.43s | 82756 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c
0m02.43s | 447172 ko | rupicola/src/Rupicola/Lib/Core.vo
0m02.42s | 537004 ko | Rewriter/Passes/FlattenThunkedRects.vo
0m02.42s | 64252 ko | fiat-rust/src/secp256k1_montgomery_64.rs
0m02.41s | 425468 ko | Util/Bool/Reflect.vo
0m02.41s | 441108 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/rpmul.vo
0m02.40s | 423368 ko | Rewriter/Util/Bool/Reflect.vo
0m02.40s | 470248 ko | Util/ZUtil/Morphisms.vo
0m02.38s | 467216 ko | MiscCompilerPassesProofs.vo
0m02.38s | 468844 ko | rupicola/bedrock2/bedrock2/src/bedrock2/unzify.vo
0m02.38s | 443668 ko | rupicola/src/Rupicola/Examples/DownTo.vo
0m02.37s | 67816 ko | fiat-go/64/curve25519scalar/curve25519scalar.go
0m02.36s | 449676 ko | Util/MSets/MSetIso.vo
0m02.36s | 77284 ko | fiat-bedrock2/src/curve25519_scalar_64.c
0m02.35s | 545536 ko | Bedrock/Field/Translation/Expr.vo
0m02.34s | 55824 ko | fiat-zig/src/curve25519_scalar_64.zig
0m02.30s | 459484 ko | Spec/MontgomeryCurve.vo
0m02.29s | 448692 ko | rupicola/src/Rupicola/Examples/LinkedList/Find.vo
0m02.28s | 444516 ko | Util/ZUtil/Shift.vo
0m02.28s | 61352 ko | fiat-c/src/curve25519_scalar_64.c
0m02.26s | 61228 ko | fiat-rust/src/curve25519_scalar_64.rs
0m02.26s | 463064 ko | rupicola/bedrock2/compiler/src/compiler/Pipeline.vo
0m02.24s | 429604 ko | Util/ZUtil/TwosComplement.vo
0m02.17s | 456624 ko | rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo
0m02.16s | 35384 ko | fiat-go/32/curve25519/curve25519.go
0m02.13s | 611384 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo
0m02.12s | 434664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseHyps.vo
0m02.12s | 446464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo
0m02.09s | 67276 ko | fiat-bedrock2/src/p448_solinas_64.c
0m02.08s | 51372 ko | fiat-json/src/p448_solinas_64.json
0m02.05s | 456784 ko | Arithmetic/Freeze.vo
0m02.04s | 541056 ko | Stringification/Language.vo
0m02.01s | 417420 ko | rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo
0m01.97s | 61072 ko | fiat-go/64/p224/p224.go
0m01.97s | 75016 ko | fiat-json/src/p224_64.json
0m01.97s | 35100 ko | fiat-zig/src/p448_solinas_64.zig
0m01.96s | 63284 ko | fiat-bedrock2/src/curve25519_32.c
0m01.96s | 34764 ko | fiat-rust/src/p448_solinas_64.rs
0m01.95s | 456464 ko | Arithmetic/BaseConversion.vo
0m01.95s | 435856 ko | Util/ZUtil/Testbit.vo
0m01.95s | 49468 ko | fiat-json/src/curve25519_32.json
0m01.94s | 464252 ko | Curves/TableMult/TableMult.vo
0m01.92s | 445120 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memconst.vo
0m01.91s | 389284 ko | Util/Wf2.vo
0m01.91s | 77496 ko | fiat-bedrock2/src/p224_64.c
0m01.90s | 34496 ko | fiat-c/src/p448_solinas_64.c
0m01.89s | 66076 ko | fiat-go/64/p256/p256.go
0m01.89s | 62320 ko | fiat-zig/src/p224_64.zig
0m01.88s | 431764 ko | Util/ZUtil/ModInv.vo
0m01.88s | 34152 ko | fiat-java/src/FiatCurve25519.java
0m01.88s | 66424 ko | fiat-json/src/p256_64.json
0m01.86s | 56312 ko | fiat-c/src/p224_64.c
0m01.86s | 441768 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.vo
0m01.85s | 55924 ko | fiat-zig/src/p256_64.zig
0m01.83s | 536604 ko | Rewriter/Passes/UnfoldValueBarrier.vo
0m01.83s | 77644 ko | fiat-bedrock2/src/p256_64.c
0m01.83s | 33544 ko | fiat-zig/src/curve25519_32.zig
0m01.82s | 33528 ko | fiat-c/src/curve25519_32.c
0m01.81s | 535512 ko | Rewriter/Passes/StripLiteralCasts.vo
0m01.81s | 66316 ko | fiat-rust/src/p224_64.rs
0m01.79s | 429896 ko | Util/ZUtil/Div.vo
0m01.79s | 61824 ko | fiat-c/src/p256_64.c
0m01.76s | 34144 ko | fiat-rust/src/curve25519_32.rs
0m01.75s | 433864 ko | Arithmetic/BarrettReduction/RidiculousFish.vo
0m01.75s | 59120 ko | fiat-rust/src/p256_64.rs
0m01.75s | 435556 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc.vo
0m01.74s | 419580 ko | Util/ListUtil/Forall.vo
0m01.71s | 634084 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo
0m01.69s | 463032 ko | Arithmetic/DettmanMultiplication.vo
0m01.67s | 446804 ko | Arithmetic/ModularArithmeticTheorems.vo
0m01.67s | 438212 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo
0m01.64s | 454032 ko | Arithmetic/ModOps.vo
0m01.63s | 446228 ko | Util/FSets/FMapFacts.vo
0m01.63s | 456584 ko | rupicola/src/Rupicola/Lib/Arrays.vo
0m01.61s | 536468 ko | Rewriter/Passes/ToFancy.vo
0m01.60s | 481268 ko | Assembly/Parse.vo
0m01.59s | 427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo
0m01.55s | 605636 ko | Bedrock/Field/Common/Names/MakeNames.vo
0m01.54s | 511864 ko | AbstractInterpretation/AbstractInterpretation.vo
0m01.54s | 589320 ko | CompilersTestCases.vo
0m01.54s | 433340 ko | Util/Tuple.vo
0m01.52s | 461152 ko | Util/FSets/FMapUnit.vo
0m01.49s | 451136 ko | rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo
0m01.48s | 518524 ko | AbstractInterpretation/ZRange.vo
0m01.48s | 462156 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo
0m01.48s | 464356 ko | rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo
0m01.48s | 430244 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo
0m01.47s | 458800 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo
0m01.47s | 436092 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo
0m01.45s | 435748 ko | rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo
0m01.44s | 436208 ko | rupicola/src/Rupicola/Examples/Conditionals.vo
0m01.43s | 446448 ko | rupicola/src/Rupicola/Examples/Nondeterminism/StackAlloc.vo
0m01.41s | 423320 ko | Algebra/ScalarMult.vo
0m01.40s | 411744 ko | Rewriter/Util/ListUtil/Forall.vo
0m01.38s | 541876 ko | Stringification/Go.vo
0m01.38s | 385056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/StringdumpDemo.vo
0m01.37s | 452204 ko | Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo
0m01.37s | 411588 ko | Coqprime/Z/Pmod.vo
0m01.37s | 436708 ko | Spec/WeierstrassCurve.vo
0m01.37s | 430856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo
0m01.37s | 434736 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo
0m01.37s | 438944 ko | rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo
0m01.34s | 438172 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Impl.vo
0m01.33s | 448576 ko | Util/ZRange/SplitRangeBounds.vo
0m01.33s | 435892 ko | Util/ZUtil/Pow2Mod.vo
0m01.33s | 415496 ko | Util/ZUtil/Rshi.vo
0m01.33s | 414960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo
0m01.30s | 452228 ko | rupicola/bedrock2/compiler/src/compiler/FitsStack.vo
0m01.29s | 414900 ko | Util/ListUtil/StdlibCompat.vo
0m01.28s | 468404 ko | Rewriter/Language/IdentifiersLibrary.vo
0m01.26s | 436408 ko | Util/ZUtil/TruncatingShiftl.vo
0m01.26s | 425820 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FrameRule.vo
0m01.26s | 439488 ko | rupicola/src/Rupicola/Lib/Compiler.vo
0m01.25s | 445464 ko | rupicola/src/Rupicola/Lib/InlineTables.vo
0m01.23s | 408764 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo
0m01.22s | 438096 ko | Util/ZUtil/Bitwise.vo
0m01.21s | 413612 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo
0m01.20s | 442084 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponderProofs.vo
0m01.18s | 424488 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo
0m01.15s | 624520 ko | Bedrock/Specs/Field.vo
0m01.15s | 438748 ko | Util/ZUtil/Quot.vo
0m01.14s | 431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo
0m01.10s | 418728 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo
0m01.09s | 430968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo
0m01.08s | 446720 ko | Arithmetic/Partition.vo
0m01.08s | 467272 ko | Arithmetic/PrimeFieldTheorems.vo
0m01.08s | 410040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo
0m01.08s | 411032 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo
0m01.06s | 445080 ko | Util/ZRange/SplitBounds.vo
0m01.06s | 424436 ko | Util/ZUtil/AddGetCarry.vo
0m01.05s | 603076 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo
0m01.03s | 427980 ko | rupicola/bedrock2/bedrock2/src/bedrock2/sepapp.vo
0m01.03s | 434252 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap.vo
0m01.03s | 434100 ko | rupicola/src/Rupicola/Examples/Cells/Swap.vo
0m01.03s | 442092 ko | rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo
0m01.02s | 596904 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo
0m01.02s | 443508 ko | Fancy/Spec.vo
0m01.02s | 466996 ko | Rewriter/Rewriter/Rewriter.vo
0m01.01s | 359856 ko | Util/Wf1.vo
0m00.98s | 536992 ko | Stringification/JSON.vo
0m00.97s | 442992 ko | Curves/Edwards/XYZT/Precomputed.vo
0m00.97s | 434212 ko | Util/ZUtil/Ones.vo
0m00.97s | 425836 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZWordMem.vo
0m00.96s | 414848 ko | Coqprime/PrimalityTest/EGroup.vo
0m00.96s | 408248 ko | Coqprime/PrimalityTest/LucasLehmer.vo
0m00.95s | 539748 ko | Bedrock/Field/Translation/LoadStoreList.vo
0m00.95s | 538524 ko | Stringification/C.vo
0m00.95s | 443136 ko | rupicola/src/Rupicola/Examples/Nondeterminism/Peek.vo
0m00.94s | 476676 ko | Rewriter/Rewriter/Reify.vo
0m00.92s | 442380 ko | rupicola/src/Rupicola/Examples/LinkedList/LinkedList.vo
0m00.90s | 432192 ko | Rewriter/Language/Language.vo
0m00.90s | 427340 ko | Util/ZUtil/OnesFrom.vo
0m00.89s | 420356 ko | Util/NatUtil.vo
0m00.89s | 426296 ko | Util/Strings/ParseArithmetic.vo
0m00.88s | 413948 ko | Rewriter/Util/NatUtil.vo
0m00.88s | 431960 ko | Util/Structures/Orders/Sum.vo
0m00.87s | 537912 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo
0m00.87s | 537860 ko | Stringification/Zig.vo
0m00.85s | 535744 ko | Stringification/Rust.vo
0m00.84s | 615480 ko | Bedrock/Field/Interface/Representation.vo
0m00.84s | 408404 ko | Coqprime/Z/ZCAux.vo
0m00.83s | 535716 ko | Stringification/Java.vo
0m00.82s | 534452 ko | Bedrock/Field/Common/Types.vo
0m00.82s | 619304 ko | Bedrock/Group/Point.vo
0m00.82s | 428464 ko | Curves/Montgomery/AffineInstances.vo
0m00.82s | 418484 ko | Util/Strings/String_as_OT.vo
0m00.80s | 560708 ko | Util/FSets/FMapZ.vo
0m00.79s | 410708 ko | Coqprime/PrimalityTest/Pocklington.vo
0m00.79s | 413884 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo
0m00.78s | 434556 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalNoMul.vo
0m00.78s | 416052 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/bverify.vo
0m00.75s | 489812 ko | Rewriter/Rewriter/AllTactics.vo
0m00.73s | 433592 ko | Arithmetic/BarrettReduction/Wikipedia.vo
0m00.73s | 590460 ko | Bedrock/Field/Common/Tactics.vo
0m00.73s | 505840 ko | Language/APINotations.vo
0m00.73s | 429952 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ArrayCasts.vo
0m00.72s | 545876 ko | Bedrock/Field/Stringification/FlattenVarData.vo
0m00.72s | 535532 ko | Bedrock/Field/Translation/Flatten.vo
0m00.72s | 442796 ko | rupicola/src/Rupicola/Examples/IO/Stdout.vo
0m00.71s | 422452 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo
0m00.71s | 434000 ko | rupicola/src/Rupicola/Examples/Cells/Incr.vo
0m00.71s | 442724 ko | rupicola/src/Rupicola/Examples/Tree/Tree.vo
0m00.70s | 451800 ko | Assembly/Equality.vo
0m00.70s | 526724 ko | Util/FSets/FMapN.vo
0m00.70s | 416512 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo
0m00.70s | 417860 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo
0m00.69s | 540192 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo
0m00.68s | 535428 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo
0m00.68s | 438932 ko | Rewriter/Rules.vo
0m00.68s | 437028 ko | Util/NumTheoryUtil.vo
0m00.68s | 446204 ko | rupicola/src/Rupicola/Lib/ExprCompiler.vo
0m00.67s | 506924 ko | AbstractInterpretation/WfExtra.vo
0m00.67s | 546884 ko | Rewriter/All.vo
0m00.67s | 422328 ko | Util/ErrorT/List.vo
0m00.67s | 455056 ko | Util/FSets/FMapFlip.vo
0m00.67s | 325760 ko | Util/PartiallyReifiedProp.vo
0m00.66s | 412636 ko | Coqprime/PrimalityTest/Root.vo
0m00.66s | 382464 ko | Util/Decidable.vo
0m00.66s | 415468 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo
0m00.65s | 503196 ko | MiscCompilerPassesProofsExtra.vo
0m00.65s | 382116 ko | Rewriter/Util/Decidable.vo
0m00.64s | 502268 ko | Language/WfExtra.vo
0m00.64s | 512104 ko | PushButtonSynthesis/ReificationCache.vo
0m00.63s | 520828 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo
0m00.63s | 32184 ko | fiat-go/64/curve25519/curve25519.go
0m00.62s | 511348 ko | Language/API.vo
0m00.62s | 502280 ko | Rewriter/AllTacticsExtra.vo
0m00.62s | 459732 ko | Util/FSets/FMapEmpty.vo
0m00.61s | 420704 ko | Algebra/IntegralDomain.vo
0m00.61s | 412776 ko | Coqprime/PrimalityTest/Cyclic.vo
0m00.61s | 410172 ko | Coqprime/PrimalityTest/PGroup.vo
0m00.60s | 422004 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo
0m00.60s | 442884 ko | rupicola/src/Rupicola/Examples/IO/IO.vo
0m00.59s | 506272 ko | Language/UnderLetsProofsExtra.vo
0m00.59s | 444160 ko | Util/Structures/OrdersEx.vo
0m00.58s | 452780 ko | Bedrock/Group/Loops.vo
0m00.58s | 410960 ko | Coqprime/Z/ZSum.vo
0m00.58s | 429976 ko | Util/Arg.vo
0m00.58s | 422924 ko | Util/CPSUtil.vo
0m00.58s | 409592 ko | Util/OptionList.vo
0m00.58s | 445376 ko | Util/QUtil.vo
0m00.58s | 417484 ko | Util/Strings/ParseArithmeticToTaps.vo
0m00.57s | 419668 ko | Algebra/SubsetoidRing.vo
0m00.57s | 441260 ko | Util/MSets/MSetN.vo
0m00.57s | 414972 ko | Util/ZUtil/Modulo/PullPush.vo
0m00.57s | 420508 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/DisjointUnion.vo
0m00.57s | 443676 ko | rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo
0m00.55s | 121780 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi
0m00.55s | 459972 ko | Rewriter/Language/IdentifiersGenerate.vo
0m00.55s | 472808 ko | Rewriter/Rewriter/ProofsCommonTactics.vo
0m00.55s | 503488 ko | Util/Strings/ParseFlagOptions.vo
0m00.55s | 427604 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Trace.vo
0m00.55s | 437368 ko | rupicola/src/Rupicola/Lib/NoExprReflection.vo
0m00.54s | 414808 ko | Util/Structures/Orders/Flip.vo
0m00.53s | 123852 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi
0m00.53s | 119860 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi
0m00.53s | 121504 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi
0m00.53s | 120132 ko | ExtractionOCaml/word_by_word_montgomery.cmi
0m00.53s | 439364 ko | Util/ZRange/OperationsBounds.vo
0m00.53s | 421736 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo
0m00.53s | 442848 ko | rupicola/src/Rupicola/Examples/KVStore/Properties.vo
0m00.53s | 442324 ko | rupicola/src/Rupicola/Lib/ExprReflection.vo
0m00.53s | 441816 ko | rupicola/src/Rupicola/Lib/SepLocals.vo
0m00.52s | 463832 ko | ArithmeticCPS/WordByWordMontgomery.vo
0m00.52s | 117456 ko | ExtractionOCaml/base_conversion.cmi
0m00.52s | 120696 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi
0m00.52s | 121620 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi
0m00.52s | 118688 ko | ExtractionOCaml/solinas_reduction.cmi
0m00.52s | 483816 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo
0m00.52s | 437180 ko | Util/FSets/FMapTrie/Shape.vo
0m00.52s | 37768 ko | fiat-bedrock2/src/curve25519_64.c
0m00.51s | 461376 ko | ArithmeticCPS/Freeze.vo
0m00.51s | 123816 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi
0m00.51s | 458244 ko | MiscCompilerPasses.vo
0m00.51s | 433796 ko | Util/ZUtil/CC.vo
0m00.51s | 434188 ko | Util/ZUtil/Stabilization.vo
0m00.51s | 426748 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo
0m00.50s | 450952 ko | Bedrock/Specs/Group.vo
0m00.50s | 119804 ko | ExtractionOCaml/bedrock2_base_conversion.cmi
0m00.50s | 121292 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi
0m00.50s | 121036 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi
0m00.50s | 119196 ko | ExtractionOCaml/saturated_solinas.cmi
0m00.50s | 120512 ko | ExtractionOCaml/unsaturated_solinas.cmi
0m00.50s | 123036 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi
0m00.50s | 481664 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo
0m00.50s | 480192 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo
0m00.50s | 415196 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/OperatorOverloading.vo
0m00.50s | 410648 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo
0m00.49s | 121232 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi
0m00.49s | 458452 ko | Rewriter/Language/IdentifiersGenerateProofs.vo
0m00.49s | 427212 ko | Util/Decidable/Decidable2Bool.vo
0m00.49s | 414848 ko | Util/Structures/Orders/Bool.vo
0m00.49s | 359872 ko | Util/Wf.vo
0m00.49s | 32564 ko | fiat-json/src/curve25519_64.json
0m00.49s | 415904 ko | rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo
0m00.49s | 402296 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo
0m00.48s | 468584 ko | Assembly/WithBedrock/Semantics.vo
0m00.48s | 413160 ko | Coqprime/PrimalityTest/Zp.vo
0m00.48s | 119488 ko | ExtractionOCaml/dettman_multiplication.cmi
0m00.48s | 494280 ko | Rewriter/Util/plugins/RewriterBuild.vo
0m00.48s | 411076 ko | Util/ListUtil/SetoidListFlatMap.vo
0m00.48s | 412388 ko | Util/Loops.vo
0m00.48s | 27008 ko | fiat-zig/src/curve25519_64.zig
0m00.48s | 413600 ko | rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo
0m00.48s | 434564 ko | rupicola/src/Rupicola/Examples/Swap/Properties.vo
0m00.47s | 442008 ko | Rewriter/Language/IdentifiersBasicGenerate.vo
0m00.47s | 425064 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo
0m00.46s | 449188 ko | ArithmeticCPS/Core.vo
0m00.46s | 449384 ko | Util/FSets/FMapString.vo
0m00.46s | 452064 ko | Util/MSets/MSetPositive/Show.vo
0m00.46s | 27256 ko | fiat-c/src/curve25519_64.c
0m00.46s | 413232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo
0m00.46s | 430640 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo
0m00.45s | 456604 ko | ArithmeticCPS/ModOps.vo
0m00.45s | 475284 ko | Bedrock/End2End/RupicolaCrypto/Spec.vo
0m00.45s | 26156 ko | fiat-rust/src/curve25519_64.rs
0m00.45s | 415424 ko | rupicola/bedrock2/compiler/src/compiler/NaiveRiscvWordProperties.vo
0m00.45s | 350324 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo
0m00.45s | 442172 ko | rupicola/src/Rupicola/Examples/Utf8/Utils.vo
0m00.44s | 451428 ko | ArithmeticCPS/Saturated.vo
0m00.44s | 418984 ko | rupicola/bedrock2/compiler/src/compiler/Registers.vo
0m00.44s | 392856 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_to_string.vo
0m00.44s | 405496 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo
0m00.43s | 461376 ko | ArithmeticCPS/BaseConversion.vo
0m00.43s | 408168 ko | Coqprime/Z/ZCmisc.vo
0m00.43s | 434424 ko | Util/Strings/NamingConventions.vo
0m00.43s | 429284 ko | Util/ZUtil/Log2.vo
0m00.43s | 436420 ko | Util/ZUtil/SignBit.vo
0m00.43s | 40432 ko | fiat-bedrock2/src/curve25519_solinas_64.c
0m00.43s | 419836 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ZList.vo
0m00.43s | 405960 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo
0m00.43s | 420352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo
0m00.43s | 442260 ko | rupicola/src/Rupicola/Examples/KVStore/KVStore.vo
0m00.42s | 430812 ko | Util/MSets/MSetString.vo
0m00.42s | 429680 ko | Util/ZUtil/Divide.vo
0m00.42s | 436336 ko | Util/ZUtil/Lxor.vo
0m00.42s | 37240 ko | fiat-go/64/curve25519solinas/curve25519solinas.go
0m00.42s | 39236 ko | fiat-json/src/curve25519_solinas_64.json
0m00.42s | 36340 ko | fiat-zig/src/curve25519_solinas_64.zig
0m00.42s | 422916 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo
0m00.42s | 411132 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo
0m00.42s | 442280 ko | rupicola/src/Rupicola/Examples/Cells/Cells.vo
0m00.41s | 470096 ko | Arithmetic/FLia.vo
0m00.41s | 433732 ko | Util/ZUtil/Land.vo
0m00.41s | 35504 ko | fiat-c/src/curve25519_solinas_64.c
0m00.41s | 431584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo
0m00.41s | 429580 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder.vo
0m00.41s | 430800 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo
0m00.41s | 423376 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo
0m00.41s | 438972 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo
0m00.41s | 438804 ko | rupicola/src/Rupicola/Lib/Alloc.vo
0m00.41s | 437364 ko | rupicola/src/Rupicola/Lib/SepReflection.vo
0m00.40s | 428624 ko | Util/Listable.vo
0m00.40s | 384448 ko | Util/Sum.vo
0m00.40s | 36040 ko | fiat-rust/src/curve25519_solinas_64.rs
0m00.40s | 461144 ko | rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo
0m00.40s | 425220 ko | rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo
0m00.39s | 395832 ko | Assembly/Parse/Examples/boringssl_nasm_full_mul_p256.vo
0m00.39s | 441064 ko | Rewriter/Language/Reify.vo
0m00.39s | 426988 ko | Util/ZBounded.vo
0m00.39s | 429644 ko | Util/ZUtil/Divide/Bool.vo
0m00.39s | 400344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoExports.vo
0m00.39s | 415396 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo
0m00.39s | 421432 ko | rupicola/src/Rupicola/Examples/KVStore/kv.vo
0m00.38s | 412772 ko | Util/ListUtil/GroupAllBy.vo
0m00.38s | 431556 ko | Util/ZUtil/EquivModulo.vo
0m00.38s | 422764 ko | rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo
0m00.38s | 411464 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo
0m00.38s | 417720 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo
0m00.38s | 420828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo
0m00.38s | 426000 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo
0m00.38s | 405528 ko | rupicola/src/Rupicola/Examples/CRC32/Table.vo
0m00.37s | 430116 ko | Arithmetic/ModularArithmeticPre.vo
0m00.37s | 413572 ko | Language/IdentifierParameters.vo
0m00.37s | 420780 ko | Util/HList.vo
0m00.37s | 422648 ko | Util/Level.vo
0m00.37s | 426960 ko | Util/ZRange.vo
0m00.37s | 420356 ko | Util/ZUtil/Ltz.vo
0m00.37s | 426472 ko | Util/ZUtil/Pow.vo
0m00.37s | 427680 ko | rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo
0m00.37s | 431904 ko | rupicola/bedrock2/bedrock2/src/bedrock2/RecordPredicates.vo
0m00.37s | 427624 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/chacha20.vo
0m00.37s | 438128 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo
0m00.37s | 443552 ko | rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo
0m00.37s | 430788 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo
0m00.37s | 424720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo
0m00.37s | 443060 ko | rupicola/src/Rupicola/Examples/IO/Writer.vo
0m00.36s | 385140 ko | Coqprime/List/UList.vo
0m00.36s | 419844 ko | Util/Structures/Equalities/List.vo
0m00.36s | 427828 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo
0m00.36s | 419892 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo
0m00.36s | 417232 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo
0m00.36s | 426352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo
0m00.36s | 443080 ko | rupicola/src/Rupicola/Examples/Nondeterminism/NonDeterminism.vo
0m00.35s | 385364 ko | Coqprime/List/Permutation.vo
0m00.35s | 384172 ko | Rewriter/Util/Sum.vo
0m00.35s | 429404 ko | Util/Strings/Show.vo
0m00.35s | 412512 ko | Util/Strings/String.vo
0m00.35s | 421004 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Result.vo
0m00.35s | 439560 ko | rupicola/src/Rupicola/Lib/Conditionals.vo
0m00.34s | 408188 ko | Coqprime/PrimalityTest/IGroup.vo
0m00.34s | 393816 ko | Language/PreExtra.vo
0m00.34s | 402648 ko | Rewriter/TestRules.vo
0m00.34s | 412756 ko | Rewriter/Util/Strings/ParseArithmetic.vo
0m00.34s | 393864 ko | Util/Strings/String_as_OT_old.vo
0m00.34s | 410768 ko | Util/ZUtil/CPS.vo
0m00.34s | 415816 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Demos.vo
0m00.34s | 401728 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo
0m00.33s | 375960 ko | Util/ZUtil.vo
0m00.33s | 400708 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLib.vo
0m00.33s | 414856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo
0m00.33s | 375792 ko | rupicola/src/Rupicola/Examples/KVStore/Tactics.vo
0m00.33s | 398752 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo
0m00.32s | 409072 ko | Coqprime/PrimalityTest/Euler.vo
0m00.32s | 424228 ko | Curves/Weierstrass/Affine.vo
0m00.32s | 354496 ko | Util/ZUtil/Lor.vo
0m00.32s | 353664 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo
0m00.32s | 372204 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo
0m00.32s | 376436 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo
0m00.32s | 375132 ko | rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo
0m00.32s | 420972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo
0m00.32s | 369524 ko | rupicola/src/Rupicola/Lib/Api.vo
0m00.32s | 419200 ko | rupicola/src/Rupicola/Lib/Monads.vo
0m00.31s | 408224 ko | Coqprime/PrimalityTest/Lagrange.vo
0m00.31s | 375364 ko | Rewriter/Util/MSetPositive/Facts.vo
0m00.31s | 421500 ko | Spec/CompleteEdwardsCurve.vo
0m00.31s | 377312 ko | Util/MSets/MSetPositive/Facts.vo
0m00.31s | 377252 ko | Util/Strings/Sorting.vo
0m00.31s | 351748 ko | Util/ZUtil/Land/Fold.vo
0m00.31s | 355732 ko | Util/ZUtil/Tactics/SolveRange.vo
0m00.30s | 384652 ko | Algebra/Monoid.vo
0m00.30s | 383176 ko | Coqprime/List/ListAux.vo
0m00.30s | 342728 ko | Util/Strings/Show/Enum.vo
0m00.30s | 391212 ko | Util/Structures/Orders/Unit.vo
0m00.30s | 319900 ko | Util/ZUtil/Tactics.vo
0m00.30s | 350824 ko | Util/ZUtil/Tactics/SolveTestbit.vo
0m00.30s | 353168 ko | rupicola/bedrock2/bedrock2/src/bedrock2/safe_f_equal.vo
0m00.30s | 368372 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo
0m00.30s | 357516 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo
0m00.30s | 379772 ko | rupicola/src/Rupicola/Lib/Notations.vo
0m00.30s | 364432 ko | rupicola/src/Rupicola/Lib/Tactics.vo
0m00.30s | 357996 ko | rupicola/src/Rupicola/Lib/WordNotations.vo
0m00.29s | 364272 ko | Rewriter/TestRulesProofs.vo
0m00.29s | 333924 ko | Spec/ModularArithmetic.vo
0m00.29s | 25660 ko | fiat-go/32/poly1305/poly1305.go
0m00.29s | 352048 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo
0m00.29s | 345272 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo
0m00.29s | 341028 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCallsExports.vo
0m00.29s | 349008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo
0m00.29s | 354512 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo
0m00.29s | 338736 ko | rupicola/src/Rupicola/Examples/Swap/Swap.vo
0m00.29s | 381560 ko | rupicola/src/Rupicola/Lib/Invariants.vo
0m00.29s | 411108 ko | rupicola/src/Rupicola/Lib/ToCString.vo
0m00.28s | 392356 ko | Rewriter/Language/UnderLets.vo
0m00.28s | 382364 ko | Util/Structures/Equalities/Sum.vo
0m00.28s | 378252 ko | Util/Structures/Orders/Empty.vo
0m00.28s | 360100 ko | Util/Structures/Orders/Iso.vo
0m00.28s | 342356 ko | Util/ZUtil/Tactics/Ztestbit.vo
0m00.28s | 310160 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifyHeapletwise.vo
0m00.28s | 334436 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo
0m00.28s | 342680 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediateDef.vo
0m00.28s | 354192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo
0m00.27s | 385140 ko | Coqprime/List/Iterator.vo
0m00.27s | 367396 ko | Curves/Montgomery/XZ.vo
0m00.27s | 337868 ko | Rewriter/Util/MSetPositive/Equality.vo
0m00.27s | 347388 ko | Util/ListUtil/SetoidList.vo
0m00.27s | 369612 ko | Util/ZUtil/Combine.vo
0m00.27s | 379216 ko | Util/ZUtil/Le.vo
0m00.27s | 349972 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo
0m00.27s | 377088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo
0m00.27s | 379772 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo
0m00.26s | 368384 ko | Rewriter/Util/Strings/String.vo
0m00.26s | 376924 ko | Util/ZUtil/Peano.vo
0m00.26s | 360084 ko | Util/ZUtil/Tactics/LtbToLt.vo
0m00.26s | 340944 ko | Util/ZUtil/Tactics/RewriteModSmall.vo
0m00.26s | 32592 ko | fiat-bedrock2/src/poly1305_32.c
0m00.26s | 346712 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb_spec.vo
0m00.26s | 339000 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo
0m00.26s | 377484 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo
0m00.26s | 385172 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo
0m00.25s | 334716 ko | Util/ListUtil/Filter.vo
0m00.25s | 338148 ko | Util/MSets/MSetPositive/Equality.vo
0m00.25s | 362452 ko | Util/ZRange/Operations.vo
0m00.25s | 325960 ko | Util/ZUtil/Tactics/LinearSubstitute.vo
0m00.25s | 29108 ko | fiat-json/src/poly1305_32.json
0m00.25s | 288032 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo
0m00.25s | 292340 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo
0m00.25s | 389460 ko | rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo
0m00.25s | 337192 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo
0m00.25s | 374904 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo
0m00.25s | 325428 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo
0m00.24s | 311644 ko | Algebra/Nsatz.vo
0m00.24s | 326236 ko | Arithmetic/MontgomeryReduction/Definition.vo
0m00.24s | 360664 ko | Util/AdditionChainExponentiation.vo
0m00.24s | 322652 ko | Util/MSets/Show.vo
0m00.24s | 340708 ko | Util/NUtil/WithoutReferenceToZ.vo
0m00.24s | 318760 ko | Util/ZRange/Show.vo
0m00.24s | 328440 ko | Util/ZUtil/Odd.vo
0m00.24s | 308944 ko | Util/ZUtil/Opp.vo
0m00.24s | 316532 ko | Util/ZUtil/Tactics/RewriteModDivide.vo
0m00.24s | 321008 ko | rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo
0m00.24s | 353544 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo
0m00.24s | 341560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo
0m00.23s | 300228 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo
0m00.23s | 377268 ko | Coqprime/List/ZProgression.vo
0m00.23s | 313720 ko | Rewriter/Util/Option.vo
0m00.23s | 320764 ko | Util/ErrorT/Show.vo
0m00.23s | 333864 ko | Util/ListUtil/Permutation.vo
0m00.23s | 323108 ko | Util/NUtil/Testbit.vo
0m00.23s | 286696 ko | Util/Strings/StringMap.vo
0m00.23s | 348464 ko | Util/Structures/Equalities/Prod.vo
0m00.23s | 25268 ko | fiat-java/src/FiatPoly1305.java
0m00.23s | 300056 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo
0m00.23s | 314040 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/RecordSetters.vo
0m00.22s | 333880 ko | Coqprime/PrimalityTest/FGroup.vo
0m00.22s | 310312 ko | Rewriter/Language/PreLemmas.vo
0m00.22s | 324896 ko | Rewriter/Language/UnderLetsCacheProofs.vo
0m00.22s | 345352 ko | Rewriter/Util/ListUtil/SetoidList.vo
0m00.22s | 313848 ko | Util/Option.vo
0m00.22s | 291212 ko | Util/SideConditions/ModInvPackage.vo
0m00.22s | 287668 ko | Util/ZUtil/Definitions.vo
0m00.22s | 279424 ko | Util/ZUtil/Sgn.vo
0m00.22s | 321444 ko | Util/ZUtil/Tactics/SimplifyFractionsLe.vo
0m00.22s | 259676 ko | Util/ZUtil/Tactics/SplitMinMax.vo
0m00.22s | 318104 ko | Util/ZUtil/Tactics/ZeroBounds.vo
0m00.22s | 23992 ko | fiat-c/src/poly1305_32.c
0m00.22s | 24364 ko | fiat-rust/src/poly1305_32.rs
0m00.22s | 24480 ko | fiat-zig/src/poly1305_32.zig
0m00.22s | 312072 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifySep.vo
0m00.22s | 299808 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepClause.vo
0m00.22s | 329056 ko | rupicola/bedrock2/compiler/src/compiler/mod4_0.vo
0m00.22s | 308236 ko | rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo
0m00.22s | 298992 ko | rupicola/bedrock2/compiler/src/compiler/util/Common.vo
0m00.22s | 315128 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Byte.vo
0m00.22s | 336016 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo
0m00.22s | 289828 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo
0m00.22s | 299720 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo
0m00.22s | 314352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo
0m00.22s | 300972 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo
0m00.21s | 315792 ko | Util/IdfunWithAlt.vo
0m00.21s | 262576 ko | Util/NUtil/Sorting.vo
0m00.21s | 292716 ko | Util/Strings/Parse/Common.vo
0m00.21s | 265724 ko | Util/ZUtil/Hints/PullPush.vo
0m00.21s | 310364 ko | Util/ZUtil/Z2Nat.vo
0m00.21s | 305796 ko | Util/ZUtil/ZSimplify/Simple.vo
0m00.21s | 273568 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListIndexNotations.vo
0m00.21s | 277260 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepBulletPoints.vo
0m00.21s | 283964 ko | rupicola/bedrock2/bedrock2/src/bedrock2/cancel_div.vo
0m00.21s | 313100 ko | rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo
0m00.21s | 359956 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo
0m00.21s | 274236 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo
0m00.21s | 328060 ko | rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo
0m00.…
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
No description provided.