Revision history - refs/tags/v0.0.13 - origin: https://github.com/mit-plv/fiat-crypto

visit type:

Revision	Author	Date	Message	Commit Date
36ef68f	Jason Gross	29 March 2022, 22:51:08 UTC	Add support for SKIP_COQSCRIPTS_INCLUDE=1	29 March 2022, 22:51:08 UTC
894e084	dependabot[bot]	29 March 2022, 20:17:17 UTC	Bump rewriter from `10c6a00` to `2c2d78e` (#1175)	29 March 2022, 20:17:17 UTC
8ab610a	Jason Gross	29 March 2022, 18:51:58 UTC	Bump rupicola to get fixed install targets	29 March 2022, 18:51:58 UTC
d698f07	dependabot[bot]	28 March 2022, 20:33:48 UTC	Bump rupicola from `f5fbc4e` to `60a187d` (#1174)	28 March 2022, 20:33:48 UTC
8b7f703	Jason Gross	27 March 2022, 04:14:40 UTC	Skip bedrock2 code on Windows It's just too slow, at least for now :-(	27 March 2022, 20:56:01 UTC
59864b6	Jason Gross	26 March 2022, 03:05:16 UTC	Fix some broken parameters	27 March 2022, 20:56:01 UTC
f01aa32	Jason Gross	19 February 2022, 23:47:49 UTC	Rework equivalence checker proofs to be based on remove This gets us almost all the way to the end of the proof. The primary remaining issue is the fact that the current spec constrains the registers holding the input and output values to not change across the proof. We need to rework how we're handling registers in the spec a bit. Ensure that we can prove goals not about register equality After chatting with Andres, the way to spec these is to add asm_in/out arguments that track only the arrays, and have these be the arguments that are passed to both inputs and outputs. Then both the inputs and the outputs can mandate that there exist asm_in/out arguments which also apply to scalar arguments, and spec the rest in terms of these. <details><summary>Timing Diff</summary> <p> ``` After \| Peak Mem \| File Name \| Before \| Peak Mem \|\| Change \|\| Change (mem) \| % Change \| % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 193m13.13s \| 4088604 ko \| Total Time / Peak Mem \| 188m56.89s \| 4088744 ko \|\| +4m16.24s \|\| -140 ko \| +2.26% \| -0.00% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 5m36.38s \| 3054028 ko \| Assembly/WithBedrock/Proofs.vo \| 0m49.93s \| 993444 ko \|\| +4m46.44s \|\| 2060584 ko \| +573.70% \| +207.41% 7m08.11s \| 964412 ko \| fiat-go/32/p384/p384.go \| 7m58.16s \| 1030768 ko \|\| -0m50.04s \|\| -66356 ko \| -10.46% \| -6.43% 0m57.88s \| 1016920 ko \| Assembly/EquivalenceProofs.vo \| 0m42.19s \| 981188 ko \|\| +0m15.69s \|\| 35732 ko \| +37.18% \| +3.64% 2m23.75s \| 1632616 ko \| Rewriter/Passes/NBE.vo \| 2m36.85s \| 1609124 ko \|\| -0m13.09s \|\| 23492 ko \| -8.35% \| +1.45% 7m53.10s \| 1011348 ko \| fiat-c/src/p384_32.c \| 7m42.05s \| 992272 ko \|\| +0m11.05s \|\| 19076 ko \| +2.39% \| +1.92% 4m21.97s \| 1390132 ko \| PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo \| 4m14.80s \| 1397512 ko \|\| +0m07.17s \|\| -7380 ko \| +2.81% \| -0.52% 7m48.63s \| 965904 ko \| fiat-java/src/FiatP384.java \| 7m43.82s \| 942416 ko \|\| +0m04.81s \|\| 23488 ko \| +1.03% \| +2.49% 7m48.03s \| 1198288 ko \| fiat-json/src/p384_32.json \| 7m44.86s \| 1131728 ko \|\| +0m03.16s \|\| 66560 ko \| +0.68% \| +5.88% 7m15.14s \| 1125288 ko \| fiat-zig/src/p384_32.zig \| 7m19.06s \| 992304 ko \|\| -0m03.92s \|\| 132984 ko \| -0.89% \| +13.40% 7m13.06s \| 1084172 ko \| fiat-bedrock2/src/p384_32.c \| 7m10.54s \| 990920 ko \|\| +0m02.51s \|\| 93252 ko \| +0.58% \| +9.41% 0m31.13s \| 255036 ko \| fiat-json/src/secp256k1_32.json \| 0m28.86s \| 207112 ko \|\| +0m02.26s \|\| 47924 ko \| +7.86% \| +23.13% 0m30.24s \| 189332 ko \| fiat-c/src/secp256k1_32.c \| 0m27.51s \| 208784 ko \|\| +0m02.72s \|\| -19452 ko \| +9.92% \| -9.31% 0m27.64s \| 212428 ko \| fiat-go/32/p256/p256.go \| 0m29.89s \| 227992 ko \|\| -0m02.25s \|\| -15564 ko \| -7.52% \| -6.82% 2m59.73s \| 789248 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo \| 3m01.25s \| 788988 ko \|\| -0m01.52s \|\| 260 ko \| -0.83% \| +0.03% 2m01.32s \| 1591124 ko \| Rewriter/Passes/ToFancyWithCasts.vo \| 2m02.47s \| 1591164 ko \|\| -0m01.15s \|\| -40 ko \| -0.93% \| -0.00% 1m56.71s \| 2413724 ko \| Bedrock/End2End/X25519/MontgomeryLadder.vo \| 1m54.96s \| 2413440 ko \|\| +0m01.75s \|\| 284 ko \| +1.52% \| +0.01% 1m33.39s \| 1596664 ko \| SlowPrimeSynthesisExamples.vo \| 1m34.44s \| 1596504 ko \|\| -0m01.04s \|\| 160 ko \| -1.11% \| +0.01% 0m30.56s \| 217712 ko \| fiat-java/src/FiatSecp256K1.java \| 0m31.86s \| 199004 ko \|\| -0m01.30s \|\| 18708 ko \| -4.08% \| +9.40% 0m30.46s \| 218356 ko \| fiat-zig/src/secp256k1_32.zig \| 0m31.60s \| 222192 ko \|\| -0m01.14s \|\| -3836 ko \| -3.60% \| -1.72% 0m27.44s \| 1233240 ko \| ExtractionOCaml/perf_unsaturated_solinas \| 0m26.25s \| 1155756 ko \|\| +0m01.19s \|\| 77484 ko \| +4.53% \| +6.70% 0m23.61s \| 1736432 ko \| ExtractionOCaml/bedrock2_unsaturated_solinas.ml \| 0m24.64s \| 1732968 ko \|\| -0m01.03s \|\| 3464 ko \| -4.18% \| +0.19% 0m16.39s \| 1887428 ko \| ExtractionHaskell/bedrock2_word_by_word_montgomery.hs \| 0m17.62s \| 1889036 ko \|\| -0m01.23s \|\| -1608 ko \| -6.98% \| -0.08% 0m15.51s \| 134808 ko \| fiat-bedrock2/src/p224_32.c \| 0m14.09s \| 145772 ko \|\| +0m01.41s \|\| -10964 ko \| +10.07% \| -7.52% 7m49.67s \| 1063652 ko \| fiat-rust/src/p384_32.rs \| 7m50.04s \| 1081104 ko \|\| -0m00.37s \|\| -17452 ko \| -0.07% \| -1.61% 6m57.85s \| 2075164 ko \| Curves/Weierstrass/AffineProofs.vo \| 6m58.31s \| 2081684 ko \|\| -0m00.45s \|\| -6520 ko \| -0.10% \| -0.31% 4m14.13s \| 4088604 ko \| Curves/EdwardsMontgomery.vo \| 4m14.55s \| 4088744 ko \|\| -0m00.42s \|\| -140 ko \| -0.16% \| -0.00% 3m11.62s \| 1778848 ko \| Rewriter/Passes/ArithWithCasts.vo \| 3m11.53s \| 1778888 ko \|\| +0m00.09s \|\| -40 ko \| +0.04% \| -0.00% 2m56.32s \| 1448332 ko \| Curves/Weierstrass/Projective.vo \| 2m56.51s \| 1404040 ko \|\| -0m00.18s \|\| 44292 ko \| -0.10% \| +3.15% 2m47.02s \| 1441796 ko \| Curves/Montgomery/XZProofs.vo \| 2m47.55s \| 1447212 ko \|\| -0m00.53s \|\| -5416 ko \| -0.31% \| -0.37% 2m36.49s \| 1231416 ko \| Curves/Montgomery/AffineProofs.vo \| 2m36.51s \| 1231432 ko \|\| -0m00.01s \|\| -16 ko \| -0.01% \| -0.00% 2m31.48s \| 1115940 ko \| Fancy/Compiler.vo \| 2m31.68s \| 1119736 ko \|\| -0m00.20s \|\| -3796 ko \| -0.13% \| -0.33% 2m15.81s \| 1030820 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo \| 2m15.69s \| 1030824 ko \|\| +0m00.12s \|\| -4 ko \| +0.08% \| -0.00% 2m08.08s \| 1193704 ko \| Rewriter/Rewriter/Wf.vo \| 2m08.81s \| 1193664 ko \|\| -0m00.72s \|\| 40 ko \| -0.56% \| +0.00% 2m01.88s \| 2785816 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.vo \| 2m01.94s \| 2785760 ko \|\| -0m00.06s \|\| 56 ko \| -0.04% \| +0.00% 1m50.27s \| 901316 ko \| AbstractInterpretation/Wf.vo \| 1m50.36s \| 901316 ko \|\| -0m00.08s \|\| 0 ko \| -0.08% \| +0.00% 1m42.59s \| 1346872 ko \| Fancy/Barrett256.vo \| 1m42.33s \| 1346192 ko \|\| +0m00.26s \|\| 680 ko \| +0.25% \| +0.05% 1m41.07s \| 1048152 ko \| Bedrock/Field/Synthesis/Examples/X25519_64.vo \| 1m40.24s \| 1048008 ko \|\| +0m00.82s \|\| 144 ko \| +0.82% \| +0.01% 1m19.07s \| 1208384 ko \| Bedrock/End2End/X25519/Field25519.vo \| 1m19.14s \| 1208488 ko \|\| -0m00.07s \|\| -104 ko \| -0.08% \| -0.00% 1m18.08s \| 745944 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MMIO.vo \| 1m18.29s \| 745948 ko \|\| -0m00.20s \|\| -4 ko \| -0.26% \| -0.00% 1m17.05s \| 435240 ko \| Spec/Test/X25519.vo \| 1m17.15s \| 435276 ko \|\| -0m00.10s \|\| -36 ko \| -0.12% \| -0.00% 1m15.79s \| 1046156 ko \| UnsaturatedSolinasHeuristics/Tests.vo \| 1m15.57s \| 1046108 ko \|\| +0m00.21s \|\| 48 ko \| +0.29% \| +0.00% 1m14.11s \| 1578696 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo \| 1m14.23s \| 1578676 ko \|\| -0m00.12s \|\| 20 ko \| -0.16% \| +0.00% 1m02.38s \| 943344 ko \| Curves/Weierstrass/Jacobian.vo \| 1m02.25s \| 943240 ko \|\| +0m00.13s \|\| 104 ko \| +0.20% \| +0.01% 1m02.31s \| 1335652 ko \| Bedrock/Field/Synthesis/Examples/p224_64.vo \| 1m01.86s \| 1335560 ko \|\| +0m00.45s \|\| 92 ko \| +0.72% \| +0.00% 1m01.62s \| 729280 ko \| Rewriter/Language/UnderLetsProofs.vo \| 1m01.82s \| 729232 ko \|\| -0m00.20s \|\| 48 ko \| -0.32% \| +0.00% 0m59.66s \| 975008 ko \| PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo \| 0m59.89s \| 974848 ko \|\| -0m00.23s \|\| 160 ko \| -0.38% \| +0.01% 0m59.30s \| 1272772 ko \| Bedrock/Field/Synthesis/Examples/p256_64.vo \| 0m58.87s \| 1272872 ko \|\| +0m00.42s \|\| -100 ko \| +0.73% \| -0.00% 0m56.82s \| 635744 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Spilling.vo \| 0m56.75s \| 635680 ko \|\| +0m00.07s \|\| 64 ko \| +0.12% \| +0.01% 0m56.70s \| 843772 ko \| AbstractInterpretation/ZRangeProofs.vo \| 0m56.77s \| 844460 ko \|\| -0m00.07s \|\| -688 ko \| -0.12% \| -0.08% 0m55.88s \| 723056 ko \| AbstractInterpretation/Proofs.vo \| 0m55.73s \| 723564 ko \|\| +0m00.15s \|\| -508 ko \| +0.26% \| -0.07% 0m54.99s \| 2462412 ko \| ExtractionOCaml/bedrock2_word_by_word_montgomery \| 0m55.10s \| 2462596 ko \|\| -0m00.10s \|\| -184 ko \| -0.19% \| -0.00% 0m54.54s \| 694904 ko \| Rewriter/RulesProofs.vo \| 0m54.82s \| 694060 ko \|\| -0m00.28s \|\| 844 ko \| -0.51% \| +0.12% 0m53.28s \| 1025948 ko \| Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo \| 0m53.14s \| 1025904 ko \|\| +0m00.14s \|\| 44 ko \| +0.26% \| +0.00% 0m51.41s \| 944972 ko \| Rewriter/Rewriter/InterpProofs.vo \| 0m51.37s \| 944996 ko \|\| +0m00.03s \|\| -24 ko \| +0.07% \| -0.00% 0m50.18s \| 1048308 ko \| Rewriter/Passes/MultiRetSplit.vo \| 0m50.19s \| 1048504 ko \|\| -0m00.00s \|\| -196 ko \| -0.01% \| -0.01% 0m50.16s \| 957260 ko \| Assembly/WithBedrock/SymbolicProofs.vo \| 0m50.48s \| 957440 ko \|\| -0m00.32s \|\| -180 ko \| -0.63% \| -0.01% 0m49.16s \| 937444 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo \| 0m49.18s \| 937380 ko \|\| -0m00.02s \|\| 64 ko \| -0.04% \| +0.00% 0m48.69s \| 2145732 ko \| ExtractionOCaml/word_by_word_montgomery \| 0m49.34s \| 2145532 ko \|\| -0m00.65s \|\| 200 ko \| -1.31% \| +0.00% 0m48.14s \| 792992 ko \| Rewriter/Rewriter/ProofsCommon.vo \| 0m48.05s \| 792968 ko \|\| +0m00.09s \|\| 24 ko \| +0.18% \| +0.00% 0m46.75s \| 1112048 ko \| Rewriter/Passes/Arith.vo \| 0m46.77s \| 1112112 ko \|\| -0m00.02s \|\| -64 ko \| -0.04% \| -0.00% 0m46.59s \| 1076312 ko \| Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo \| 0m47.37s \| 1076452 ko \|\| -0m00.77s \|\| -140 ko \| -1.64% \| -0.01% 0m44.87s \| 577176 ko \| Demo.vo \| 0m44.94s \| 577156 ko \|\| -0m00.07s \|\| 20 ko \| -0.15% \| +0.00% 0m43.85s \| 1326816 ko \| Fancy/Montgomery256.vo \| 0m43.27s \| 1324368 ko \|\| +0m00.57s \|\| 2448 ko \| +1.34% \| +0.18% 0m39.77s \| 567524 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo \| 0m39.81s \| 567312 ko \|\| -0m00.03s \|\| 212 ko \| -0.10% \| +0.03% 0m38.33s \| 2347268 ko \| ExtractionOCaml/bedrock2_word_by_word_montgomery.ml \| 0m38.53s \| 2359096 ko \|\| -0m00.20s \|\| -11828 ko \| -0.51% \| -0.50% 0m37.26s \| 1862916 ko \| ExtractionOCaml/bedrock2_unsaturated_solinas \| 0m37.34s \| 1862948 ko \|\| -0m00.08s \|\| -32 ko \| -0.21% \| -0.00% 0m36.90s \| 2242368 ko \| ExtractionOCaml/word_by_word_montgomery.ml \| 0m37.12s \| 2218472 ko \|\| -0m00.21s \|\| 23896 ko \| -0.59% \| +1.07% 0m35.20s \| 1650584 ko \| ExtractionOCaml/unsaturated_solinas \| 0m35.59s \| 1650372 ko \|\| -0m00.39s \|\| 212 ko \| -1.09% \| +0.01% 0m34.59s \| 1072932 ko \| Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo \| 0m34.66s \| 1073056 ko \|\| -0m00.06s \|\| -124 ko \| -0.20% \| -0.01% 0m33.72s \| 1410252 ko \| ExtractionOCaml/bedrock2_saturated_solinas \| 0m33.93s \| 1430984 ko \|\| -0m00.21s \|\| -20732 ko \| -0.61% \| -1.44% 0m33.62s \| 1409276 ko \| ExtractionOCaml/bedrock2_base_conversion \| 0m33.56s \| 1422496 ko \|\| +0m00.05s \|\| -13220 ko \| +0.17% \| -0.92% 0m33.14s \| 228364 ko \| fiat-bedrock2/src/secp256k1_32.c \| 0m33.53s \| 220936 ko \|\| -0m00.39s \|\| 7428 ko \| -1.16% \| +3.36% 0m32.08s \| 225244 ko \| fiat-bedrock2/src/p256_32.c \| 0m32.30s \| 222652 ko \|\| -0m00.21s \|\| 2592 ko \| -0.68% \| +1.16% 0m30.90s \| 898584 ko \| Rewriter/Passes/MulSplit.vo \| 0m30.66s \| 898356 ko \|\| +0m00.23s \|\| 228 ko \| +0.78% \| +0.02% 0m30.68s \| 218588 ko \| fiat-go/32/secp256k1/secp256k1.go \| 0m30.84s \| 217548 ko \|\| -0m00.16s \|\| 1040 ko \| -0.51% \| +0.47% 0m30.68s \| 192712 ko \| fiat-java/src/FiatP256.java \| 0m30.97s \| 218100 ko \|\| -0m00.28s \|\| -25388 ko \| -0.93% \| -11.64% 0m30.43s \| 598344 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo \| 0m30.67s \| 598168 ko \|\| -0m00.24s \|\| 176 ko \| -0.78% \| +0.02% 0m30.36s \| 194132 ko \| fiat-rust/src/secp256k1_32.rs \| 0m30.14s \| 217280 ko \|\| +0m00.21s \|\| -23148 ko \| +0.72% \| -10.65% 0m30.14s \| 235172 ko \| fiat-json/src/p256_32.json \| 0m30.21s \| 226308 ko \|\| -0m00.07s \|\| 8864 ko \| -0.23% \| +3.91% 0m29.95s \| 215276 ko \| fiat-zig/src/p256_32.zig \| 0m30.20s \| 215876 ko \|\| -0m00.25s \|\| -600 ko \| -0.82% \| -0.27% 0m29.65s \| 528308 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo \| 0m29.48s \| 528064 ko \|\| +0m00.16s \|\| 244 ko \| +0.57% \| +0.04% 0m29.58s \| 1154380 ko \| Bedrock/Field/Synthesis/Generic/UnsaturatedSolinas.vo \| 0m29.30s \| 1155644 ko \|\| +0m00.27s \|\| -1264 ko \| +0.95% \| -0.10% 0m29.55s \| 1233348 ko \| ExtractionOCaml/perf_word_by_word_montgomery \| 0m30.09s \| 1233332 ko \|\| -0m00.53s \|\| 16 ko \| -1.79% \| +0.00% 0m29.37s \| 218388 ko \| fiat-rust/src/p256_32.rs \| 0m29.90s \| 217936 ko \|\| -0m00.52s \|\| 452 ko \| -1.77% \| +0.20% 0m29.28s \| 218320 ko \| fiat-c/src/p256_32.c \| 0m28.92s \| 198000 ko \|\| +0m00.35s \|\| 20320 ko \| +1.24% \| +10.26% 0m29.26s \| 916216 ko \| Bedrock/Group/ScalarMult/MontgomeryLadder.vo \| 0m29.31s \| 916064 ko \|\| -0m00.04s \|\| 152 ko \| -0.17% \| +0.01% 0m29.21s \| 953928 ko \| PushButtonSynthesis/BYInversionReificationCache.vo \| 0m29.17s \| 954144 ko \|\| +0m00.03s \|\| -216 ko \| +0.13% \| -0.02% 0m29.05s \| 1234908 ko \| ExtractionOCaml/base_conversion \| 0m29.27s \| 1233792 ko \|\| -0m00.21s \|\| 1116 ko \| -0.75% \| +0.09% 0m28.98s \| 1233556 ko \| ExtractionOCaml/saturated_solinas \| 0m29.01s \| 1235808 ko \|\| -0m00.03s \|\| -2252 ko \| -0.10% \| -0.18% 0m27.92s \| 1085444 ko \| Bedrock/Field/Synthesis/Generic/WordByWordMontgomery.vo \| 0m28.62s \| 1086312 ko \|\| -0m00.69s \|\| -868 ko \| -2.44% \| -0.07% 0m27.61s \| 879320 ko \| Rewriter/Rewriter/Examples.vo \| 0m27.71s \| 879392 ko \|\| -0m00.10s \|\| -72 ko \| -0.36% \| -0.00% 0m27.34s \| 914916 ko \| PushButtonSynthesis/BarrettReductionReificationCache.vo \| 0m27.38s \| 914916 ko \|\| -0m00.03s \|\| 0 ko \| -0.14% \| +0.00% 0m26.97s \| 848176 ko \| PushButtonSynthesis/UnsaturatedSolinas.vo \| 0m26.76s \| 848004 ko \|\| +0m00.20s \|\| 172 ko \| +0.78% \| +0.02% 0m25.98s \| 679452 ko \| Rewriter/Language/Wf.vo \| 0m26.22s \| 679228 ko \|\| -0m00.23s \|\| 224 ko \| -0.91% \| +0.03% 0m25.41s \| 496364 ko \| Arithmetic/Saturated.vo \| 0m25.51s \| 496112 ko \|\| -0m00.10s \|\| 252 ko \| -0.39% \| +0.05% 0m25.25s \| 840144 ko \| Rewriter/Rewriter/Examples/PrefixSums.vo \| 0m25.20s \| 840272 ko \|\| +0m00.05s \|\| -128 ko \| +0.19% \| -0.01% 0m24.79s \| 161720 ko \| fiat-bedrock2/src/p434_64.c \| 0m24.45s \| 160508 ko \|\| +0m00.33s \|\| 1212 ko \| +1.39% \| +0.75% 0m24.51s \| 749724 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegRename.vo \| 0m24.65s \| 749784 ko \|\| -0m00.13s \|\| -60 ko \| -0.56% \| -0.00% 0m23.27s \| 860088 ko \| Bedrock/Field/Synthesis/Examples/LadderStep.vo \| 0m23.08s \| 860492 ko \|\| +0m00.19s \|\| -404 ko \| +0.82% \| -0.04% 0m23.23s \| 154380 ko \| fiat-go/64/p434/p434.go \| 0m23.26s \| 154688 ko \|\| -0m00.03s \|\| -308 ko \| -0.12% \| -0.19% 0m23.19s \| 143704 ko \| fiat-zig/src/p434_64.zig \| 0m22.84s \| 155548 ko \|\| +0m00.35s \|\| -11844 ko \| +1.53% \| -7.61% 0m23.09s \| 171980 ko \| fiat-json/src/p434_64.json \| 0m23.13s \| 166400 ko \|\| -0m00.03s \|\| 5580 ko \| -0.17% \| +3.35% 0m23.08s \| 145104 ko \| fiat-rust/src/p434_64.rs \| 0m22.98s \| 142824 ko \|\| +0m00.09s \|\| 2280 ko \| +0.43% \| +1.59% 0m22.89s \| 783268 ko \| Bedrock/Field/Translation/Proofs/Expr.vo \| 0m22.63s \| 783300 ko \|\| +0m00.26s \|\| -32 ko \| +1.14% \| -0.00% 0m22.71s \| 1679396 ko \| ExtractionOCaml/unsaturated_solinas.ml \| 0m23.11s \| 1703648 ko \|\| -0m00.39s \|\| -24252 ko \| -1.73% \| -1.42% 0m22.55s \| 138676 ko \| fiat-c/src/p434_64.c \| 0m22.27s \| 149828 ko \|\| +0m00.28s \|\| -11152 ko \| +1.25% \| -7.44% 0m22.10s \| 854936 ko \| Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo \| 0m22.06s \| 855036 ko \|\| +0m00.04s \|\| -100 ko \| +0.18% \| -0.01% 0m20.73s \| 807068 ko \| PushButtonSynthesis/WordByWordMontgomery.vo \| 0m20.73s \| 807072 ko \|\| +0m00.00s \|\| -4 ko \| +0.00% \| -0.00% 0m20.63s \| 732620 ko \| Bedrock/Field/Translation/Proofs/LoadStoreList.vo \| 0m19.83s \| 732368 ko \|\| +0m00.80s \|\| 252 ko \| +4.03% \| +0.03% 0m20.05s \| 1679792 ko \| ExtractionOCaml/bedrock2_saturated_solinas.ml \| 0m20.21s \| 1682344 ko \|\| -0m00.16s \|\| -2552 ko \| -0.79% \| -0.15% 0m19.53s \| 1664260 ko \| ExtractionOCaml/bedrock2_base_conversion.ml \| 0m20.39s \| 1668252 ko \|\| -0m00.85s \|\| -3992 ko \| -4.21% \| -0.23% 0m18.75s \| 1622948 ko \| ExtractionOCaml/base_conversion.ml \| 0m19.39s \| 1607864 ko \|\| -0m00.64s \|\| 15084 ko \| -3.30% \| +0.93% 0m18.68s \| 1594048 ko \| ExtractionOCaml/saturated_solinas.ml \| 0m18.92s \| 1602896 ko \|\| -0m00.24s \|\| -8848 ko \| -1.26% \| -0.55% 0m18.60s \| 1833352 ko \| ExtractionOCaml/perf_word_by_word_montgomery.ml \| 0m18.69s \| 1831936 ko \|\| -0m00.08s \|\| 1416 ko \| -0.48% \| +0.07% 0m18.32s \| 808128 ko \| Bedrock/Field/Synthesis/Examples/X1305_32.vo \| 0m18.27s \| 807988 ko \|\| +0m00.05s \|\| 140 ko \| +0.27% \| +0.01% 0m18.03s \| 1114624 ko \| Bedrock/End2End/X25519/MontgomeryLadderProperties.vo \| 0m18.07s \| 1114660 ko \|\| -0m00.03s \|\| -36 ko \| -0.22% \| -0.00% 0m17.19s \| 580008 ko \| Rewriter/Language/Inversion.vo \| 0m17.26s \| 579736 ko \|\| -0m00.07s \|\| 272 ko \| -0.40% \| +0.04% 0m17.07s \| 831256 ko \| Curves/Edwards/XYZT/Basic.vo \| 0m17.09s \| 831384 ko \|\| -0m00.01s \|\| -128 ko \| -0.11% \| -0.01% 0m17.06s \| 907288 ko \| StandaloneDebuggingExamples.vo \| 0m17.07s \| 907212 ko \|\| -0m00.01s \|\| 76 ko \| -0.05% \| +0.00% 0m17.03s \| 1808088 ko \| ExtractionOCaml/perf_unsaturated_solinas.ml \| 0m17.43s \| 1807948 ko \|\| -0m00.39s \|\| 140 ko \| -2.29% \| +0.00% 0m16.96s \| 614488 ko \| Util/ZUtil/ArithmeticShiftr.vo \| 0m16.97s \| 614396 ko \|\| -0m00.00s \|\| 92 ko \| -0.05% \| +0.01% 0m16.94s \| 755036 ko \| PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo \| 0m16.70s \| 754868 ko \|\| +0m00.24s \|\| 168 ko \| +1.43% \| +0.02% 0m16.91s \| 1876404 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo \| 0m17.01s \| 1876420 ko \|\| -0m00.10s \|\| -16 ko \| -0.58% \| -0.00% 0m16.78s \| 666748 ko \| Assembly/Symbolic.vo \| 0m16.81s \| 666904 ko \|\| -0m00.02s \|\| -156 ko \| -0.17% \| -0.02% 0m16.55s \| 531296 ko \| Arithmetic/WordByWordMontgomery.vo \| 0m16.62s \| 531124 ko \|\| -0m00.07s \|\| 172 ko \| -0.42% \| +0.03% 0m16.17s \| 796320 ko \| Bedrock/Field/Translation/Proofs/Cmd.vo \| 0m15.76s \| 796180 ko \|\| +0m00.41s \|\| 140 ko \| +2.60% \| +0.01% 0m15.95s \| 752088 ko \| Language/IdentifiersGENERATED.vo \| 0m15.88s \| 752120 ko \|\| +0m00.06s \|\| -32 ko \| +0.44% \| -0.00% 0m15.68s \| 486504 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo \| 0m15.71s \| 486368 ko \|\| -0m00.03s \|\| 136 ko \| -0.19% \| +0.02% 0m15.65s \| 779256 ko \| Bedrock/Field/Translation/Proofs/Func.vo \| 0m16.13s \| 778948 ko \|\| -0m00.47s \|\| 308 ko \| -2.97% \| +0.03% 0m15.61s \| 1810056 ko \| ExtractionHaskell/word_by_word_montgomery.hs \| 0m15.59s \| 1818656 ko \|\| +0m00.01s \|\| -8600 ko \| +0.12% \| -0.47% 0m15.23s \| 573772 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo \| 0m15.13s \| 573784 ko \|\| +0m00.09s \|\| -12 ko \| +0.66% \| -0.00% 0m15.10s \| 726436 ko \| Curves/Edwards/AffineProofs.vo \| 0m15.00s \| 726160 ko \|\| +0m00.09s \|\| 276 ko \| +0.66% \| +0.03% 0m14.99s \| 514772 ko \| Arithmetic/BarrettReduction.vo \| 0m14.94s \| 514192 ko \|\| +0m00.05s \|\| 580 ko \| +0.33% \| +0.11% 0m14.66s \| 785452 ko \| Bedrock/End2End/Poly1305/Field1305.vo \| 0m14.66s \| 785424 ko \|\| +0m00.00s \|\| 28 ko \| +0.00% \| +0.00% 0m14.57s \| 422128 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/TestGoals.vo \| 0m14.80s \| 422124 ko \|\| -0m00.23s \|\| 4 ko \| -1.55% \| +0.00% 0m14.49s \| 460208 ko \| Algebra/Field.vo \| 0m14.49s \| 460528 ko \|\| +0m00.00s \|\| -320 ko \| +0.00% \| -0.06% 0m14.48s \| 512676 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo \| 0m14.41s \| 512792 ko \|\| +0m00.07s \|\| -116 ko \| +0.48% \| -0.02% 0m14.36s \| 706744 ko \| Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo \| 0m14.37s \| 706712 ko \|\| -0m00.00s \|\| 32 ko \| -0.06% \| +0.00% 0m14.19s \| 562732 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo \| 0m14.11s \| 562584 ko \|\| +0m00.08s \|\| 148 ko \| +0.56% \| +0.02% 0m13.95s \| 480456 ko \| Arithmetic/Core.vo \| 0m14.02s \| 480536 ko \|\| -0m00.07s \|\| -80 ko \| -0.49% \| -0.01% 0m13.76s \| 594340 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo \| 0m13.72s \| 594392 ko \|\| +0m00.03s \|\| -52 ko \| +0.29% \| -0.00% 0m13.75s \| 135240 ko \| fiat-go/32/p224/p224.go \| 0m13.74s \| 129076 ko \|\| +0m00.00s \|\| 6164 ko \| +0.07% \| +4.77% 0m13.71s \| 594428 ko \| Language/IdentifiersGENERATEDProofs.vo \| 0m13.62s \| 594192 ko \|\| +0m00.09s \|\| 236 ko \| +0.66% \| +0.03% 0m13.70s \| 138104 ko \| fiat-zig/src/p224_32.zig \| 0m13.00s \| 138088 ko \|\| +0m00.69s \|\| 16 ko \| +5.38% \| +0.01% 0m13.56s \| 584684 ko \| Bedrock/Field/Common/Util.vo \| 0m13.53s \| 584784 ko \|\| +0m00.03s \|\| -100 ko \| +0.22% \| -0.01% 0m13.54s \| 557484 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImp.vo \| 0m13.58s \| 557628 ko \|\| -0m00.04s \|\| -144 ko \| -0.29% \| -0.02% 0m13.45s \| 143240 ko \| fiat-rust/src/p224_32.rs \| 0m13.81s \| 134244 ko \|\| -0m00.36s \|\| 8996 ko \| -2.60% \| +6.70% 0m13.43s \| 132436 ko \| fiat-c/src/p224_32.c \| 0m13.09s \| 141264 ko \|\| +0m00.33s \|\| -8828 ko \| +2.59% \| -6.24% 0m13.30s \| 653748 ko \| Bedrock/Group/AdditionChains.vo \| 0m13.57s \| 653968 ko \|\| -0m00.26s \|\| -220 ko \| -1.98% \| -0.03% 0m13.03s \| 133060 ko \| fiat-json/src/p224_32.json \| 0m13.94s \| 150044 ko \|\| -0m00.91s \|\| -16984 ko \| -6.52% \| -11.31% 0m12.95s \| 146448 ko \| fiat-java/src/FiatP224.java \| 0m13.90s \| 141984 ko \|\| -0m00.95s \|\| 4464 ko \| -6.83% \| +3.14% 0m12.90s \| 647192 ko \| Bedrock/Group/ScalarMult/LadderStep.vo \| 0m12.97s \| 647116 ko \|\| -0m00.07s \|\| 76 ko \| -0.53% \| +0.01% 0m12.63s \| 540816 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo \| 0m12.68s \| 540600 ko \|\| -0m00.04s \|\| 216 ko \| -0.39% \| +0.03% 0m12.46s \| 1446936 ko \| ExtractionHaskell/unsaturated_solinas.hs \| 0m12.27s \| 1449476 ko \|\| +0m00.19s \|\| -2540 ko \| +1.54% \| -0.17% 0m12.41s \| 105600 ko \| fiat-bedrock2/src/p384_64.c \| 0m12.21s \| 109020 ko \|\| +0m00.19s \|\| -3420 ko \| +1.63% \| -3.13% 0m12.35s \| 1512072 ko \| ExtractionHaskell/bedrock2_unsaturated_solinas.hs \| 0m12.82s \| 1511508 ko \|\| -0m00.47s \|\| 564 ko \| -3.66% \| +0.03% 0m12.12s \| 478328 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo \| 0m12.17s \| 478424 ko \|\| -0m00.05s \|\| -96 ko \| -0.41% \| -0.02% 0m12.01s \| 1083092 ko \| Assembly/Parse/TestAsm.vo \| 0m11.72s \| 1083280 ko \|\| +0m00.28s \|\| -188 ko \| +2.47% \| -0.01% 0m11.85s \| 704252 ko \| Util/ZRange/LandLorBounds.vo \| 0m11.94s \| 710768 ko \|\| -0m00.08s \|\| -6516 ko \| -0.75% \| -0.91% 0m11.83s \| 1444260 ko \| ExtractionHaskell/bedrock2_base_conversion.hs \| 0m11.15s \| 1444976 ko \|\| +0m00.67s \|\| -716 ko \| +6.09% \| -0.04% 0m11.56s \| 616532 ko \| Rewriter/Demo.vo \| 0m11.51s \| 616680 ko \|\| +0m00.05s \|\| -148 ko \| +0.43% \| -0.02% 0m11.55s \| 829672 ko \| PushButtonSynthesis/SmallExamples.vo \| 0m11.55s \| 829764 ko \|\| +0m00.00s \|\| -92 ko \| +0.00% \| -0.01% 0m11.05s \| 1449268 ko \| ExtractionHaskell/bedrock2_saturated_solinas.hs \| 0m11.71s \| 1447492 ko \|\| -0m00.66s \|\| 1776 ko \| -5.63% \| +0.12% 0m11.03s \| 1326800 ko \| ExtractionHaskell/saturated_solinas.hs \| 0m11.03s \| 1326804 ko \|\| +0m00.00s \|\| -4 ko \| +0.00% \| -0.00% 0m10.99s \| 651332 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo \| 0m10.85s \| 651460 ko \|\| +0m00.14s \|\| -128 ko \| +1.29% \| -0.01% 0m10.97s \| 1365584 ko \| ExtractionHaskell/base_conversion.hs \| 0m10.94s \| 1332792 ko \|\| +0m00.03s \|\| 32792 ko \| +0.27% \| +2.46% 0m10.82s \| 97544 ko \| fiat-go/64/p384/p384.go \| 0m10.92s \| 97136 ko \|\| -0m00.09s \|\| 408 ko \| -0.91% \| +0.42% 0m10.77s \| 101016 ko \| fiat-json/src/p384_64.json \| 0m10.65s \| 111348 ko \|\| +0m00.11s \|\| -10332 ko \| +1.12% \| -9.27% 0m10.67s \| 539820 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo \| 0m10.61s \| 539860 ko \|\| +0m00.06s \|\| -40 ko \| +0.56% \| -0.00% 0m10.58s \| 786952 ko \| Bedrock/Field/Synthesis/New/Signature.vo \| 0m10.49s \| 786388 ko \|\| +0m00.08s \|\| 564 ko \| +0.85% \| +0.07% 0m10.56s \| 97940 ko \| fiat-zig/src/p384_64.zig \| 0m10.44s \| 97852 ko \|\| +0m00.12s \|\| 88 ko \| +1.14% \| +0.08% 0m10.52s \| 96952 ko \| fiat-c/src/p384_64.c \| 0m09.90s \| 102812 ko \|\| +0m00.61s \|\| -5860 ko \| +6.26% \| -5.69% 0m10.46s \| 604532 ko \| Bedrock/Field/Translation/Proofs/Flatten.vo \| 0m10.54s \| 604552 ko \|\| -0m00.07s \|\| -20 ko \| -0.75% \| -0.00% 0m10.38s \| 473080 ko \| Primitives/MxDHRepChange.vo \| 0m10.29s \| 473000 ko \|\| +0m00.09s \|\| 80 ko \| +0.87% \| +0.01% 0m10.30s \| 582964 ko \| Stringification/IR.vo \| 0m10.28s \| 583004 ko \|\| +0m00.02s \|\| -40 ko \| +0.19% \| -0.00% 0m10.21s \| 504468 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo \| 0m10.25s \| 504480 ko \|\| -0m00.03s \|\| -12 ko \| -0.39% \| -0.00% 0m10.12s \| 505216 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo \| 0m10.21s \| 505368 ko \|\| -0m00.09s \|\| -152 ko \| -0.88% \| -0.03% 0m09.93s \| 91068 ko \| fiat-rust/src/p384_64.rs \| 0m10.58s \| 96060 ko \|\| -0m00.65s \|\| -4992 ko \| -6.14% \| -5.19% 0m09.83s \| 447432 ko \| Algebra/Ring.vo \| 0m09.84s \| 447508 ko \|\| -0m00.00s \|\| -76 ko \| -0.10% \| -0.01% 0m09.73s \| 551904 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo \| 0m09.76s \| 551956 ko \|\| -0m00.02s \|\| -52 ko \| -0.30% \| -0.00% 0m09.32s \| 637232 ko \| Bedrock/Group/ScalarMult/CSwap.vo \| 0m09.43s \| 637200 ko \|\| -0m00.10s \|\| 32 ko \| -1.16% \| +0.00% 0m09.14s \| 867948 ko \| Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.vo \| 0m09.15s \| 867840 ko \|\| -0m00.00s \|\| 108 ko \| -0.10% \| +0.01% 0m08.83s \| 105964 ko \| fiat-json/src/p448_solinas_32.json \| 0m08.72s \| 104548 ko \|\| +0m00.10s \|\| 1416 ko \| +1.26% \| +1.35% 0m08.59s \| 505520 ko \| Rewriter/Language/IdentifiersLibraryProofs.vo \| 0m08.48s \| 505512 ko \|\| +0m00.10s \|\| 8 ko \| +1.29% \| +0.00% 0m08.37s \| 44580 ko \| fiat-zig/src/p448_solinas_32.zig \| 0m08.35s \| 47676 ko \|\| +0m00.01s \|\| -3096 ko \| +0.23% \| -6.49% 0m08.28s \| 47976 ko \| fiat-rust/src/p448_solinas_32.rs \| 0m08.25s \| 44228 ko \|\| +0m00.02s \|\| 3748 ko \| +0.36% \| +8.47% 0m08.25s \| 48156 ko \| fiat-c/src/p448_solinas_32.c \| 0m07.87s \| 44324 ko \|\| +0m00.37s \|\| 3832 ko \| +4.82% \| +8.64% 0m08.17s \| 900220 ko \| Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo \| 0m08.19s \| 900160 ko \|\| -0m00.01s \|\| 60 ko \| -0.24% \| +0.00% 0m08.09s \| 679932 ko \| PushButtonSynthesis/BaseConversion.vo \| 0m08.04s \| 679748 ko \|\| +0m00.05s \|\| 184 ko \| +0.62% \| +0.02% 0m08.05s \| 594508 ko \| Language/IdentifiersBasicGENERATED.vo \| 0m08.01s \| 594540 ko \|\| +0m00.04s \|\| -32 ko \| +0.49% \| -0.00% 0m07.84s \| 782012 ko \| Assembly/Parse/Examples/fiat_p256_square_optimised_seed6.vo \| 0m07.73s \| 782044 ko \|\| +0m00.10s \|\| -32 ko \| +1.42% \| -0.00% 0m07.81s \| 587180 ko \| Rewriter/Passes/RelaxBitwidthAdcSbb.vo \| 0m07.74s \| 587092 ko \|\| +0m00.06s \|\| 88 ko \| +0.90% \| +0.01% 0m07.51s \| 696672 ko \| Assembly/Syntax.vo \| 0m07.48s \| 696764 ko \|\| +0m00.02s \|\| -92 ko \| +0.40% \| -0.01% 0m07.32s \| 458304 ko \| Util/ZRange/CornersMonotoneBounds.vo \| 0m07.34s \| 458500 ko \|\| -0m00.01s \|\| -196 ko \| -0.27% \| -0.04% 0m07.16s \| 466564 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo \| 0m07.17s \| 466384 ko \|\| -0m00.00s \|\| 180 ko \| -0.13% \| +0.03% 0m06.83s \| 682160 ko \| PushButtonSynthesis/Primitives.vo \| 0m06.74s \| 682212 ko \|\| +0m00.08s \|\| -52 ko \| +1.33% \| -0.00% 0m06.73s \| 473952 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ExprImp.vo \| 0m06.73s \| 474124 ko \|\| +0m00.00s \|\| -172 ko \| +0.00% \| -0.03% 0m06.62s \| 436720 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo \| 0m06.69s \| 436920 ko \|\| -0m00.07s \|\| -200 ko \| -1.04% \| -0.04% 0m06.57s \| 461396 ko \| Arithmetic/FancyMontgomeryReduction.vo \| 0m06.48s \| 461236 ko \|\| +0m00.08s \|\| 160 ko \| +1.38% \| +0.03% 0m06.38s \| 600516 ko \| PushButtonSynthesis/SaturatedSolinasReificationCache.vo \| 0m06.31s \| 600460 ko \|\| +0m00.07s \|\| 56 ko \| +1.10% \| +0.00% 0m06.23s \| 828944 ko \| Bedrock/Field/Translation/Proofs/UsedVarnames.vo \| 0m06.10s \| 829180 ko \|\| +0m00.13s \|\| -236 ko \| +2.13% \| -0.02% 0m06.21s \| 456172 ko \| Util/ListUtil.vo \| 0m06.17s \| 455860 ko \|\| +0m00.04s \|\| 312 ko \| +0.64% \| +0.06% 0m06.17s \| 702500 ko \| Assembly/Parse/Examples/fiat_p256_mul_optimised_seed4.vo \| 0m06.22s \| 702464 ko \|\| -0m00.04s \|\| 36 ko \| -0.80% \| +0.00% 0m06.11s \| 564092 ko \| Rewriter/Passes/NoSelect.vo \| 0m06.22s \| 564032 ko \|\| -0m00.10s \|\| 60 ko \| -1.76% \| +0.01% 0m06.08s \| 455768 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo \| 0m05.99s \| 455596 ko \|\| +0m00.08s \|\| 172 ko \| +1.50% \| +0.03% 0m06.03s \| 454952 ko \| Rewriter/Util/ListUtil.vo \| 0m06.09s \| 454680 ko \|\| -0m00.05s \|\| 272 ko \| -0.98% \| +0.05% 0m06.02s \| 455140 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo \| 0m06.07s \| 455148 ko \|\| -0m00.05s \|\| -8 ko \| -0.82% \| -0.00% 0m05.87s \| 478160 ko \| Util/ZUtil/Modulo.vo \| 0m05.87s \| 477880 ko \|\| +0m00.00s \|\| 280 ko \| +0.00% \| +0.05% 0m05.70s \| 671228 ko \| Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.vo \| 0m05.75s \| 671024 ko \|\| -0m00.04s \|\| 204 ko \| -0.86% \| +0.03% 0m05.70s \| 453928 ko \| Util/MSets/Sum.vo \| 0m05.80s \| 453856 ko \|\| -0m00.09s \|\| 72 ko \| -1.72% \| +0.01% 0m05.65s \| 480568 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/EmitsValid.vo \| 0m05.55s \| 480464 ko \|\| +0m00.10s \|\| 104 ko \| +1.80% \| +0.02% 0m05.62s \| 663932 ko \| Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.vo \| 0m05.56s \| 663864 ko \|\| +0m00.06s \|\| 68 ko \| +1.07% \| +0.01% 0m05.59s \| 523872 ko \| Fancy/Prod.vo \| 0m05.55s \| 523656 ko \|\| +0m00.04s \|\| 216 ko \| +0.72% \| +0.04% 0m05.46s \| 628212 ko \| BoundsPipeline.vo \| 0m05.39s \| 627912 ko \|\| +0m00.07s \|\| 300 ko \| +1.29% \| +0.04% 0m05.43s \| 576296 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Properties.vo \| 0m05.37s \| 576076 ko \|\| +0m00.05s \|\| 220 ko \| +1.11% \| +0.03% 0m05.40s \| 500184 ko \| Arithmetic/BYInv.vo \| 0m05.40s \| 500496 ko \|\| +0m00.00s \|\| -312 ko \| +0.00% \| -0.06% 0m05.37s \| 466732 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo \| 0m05.34s \| 466900 ko \|\| +0m00.03s \|\| -168 ko \| +0.56% \| -0.03% 0m05.30s \| 724352 ko \| Bedrock/Field/Synthesis/Examples/EncodeDecode.vo \| 0m05.42s \| 724516 ko \|\| -0m00.12s \|\| -164 ko \| -2.21% \| -0.02% 0m05.23s \| 467376 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Loops.vo \| 0m05.22s \| 467476 ko \|\| +0m00.01s \|\| -100 ko \| +0.19% \| -0.02% 0m05.10s \| 490588 ko \| COperationSpecifications.vo \| 0m05.08s \| 490496 ko \|\| +0m00.01s \|\| 92 ko \| +0.39% \| +0.01% 0m04.96s \| 430160 ko \| Spec/Curve25519.vo \| 0m04.96s \| 430296 ko \|\| +0m00.00s \|\| -136 ko \| +0.00% \| -0.03% 0m04.93s \| 459736 ko \| Util/FsatzAutoLemmas.vo \| 0m04.95s \| 459640 ko \|\| -0m00.02s \|\| 96 ko \| -0.40% \| +0.02% 0m04.82s \| 545324 ko \| Language/InversionExtra.vo \| 0m04.91s \| 545332 ko \|\| -0m00.08s \|\| -8 ko \| -1.83% \| -0.00% 0m04.79s \| 500796 ko \| Curves/Edwards/Pre.vo \| 0m04.85s \| 500768 ko \|\| -0m00.05s \|\| 28 ko \| -1.23% \| +0.00% 0m04.61s \| 671700 ko \| PushButtonSynthesis/BarrettReduction.vo \| 0m04.70s \| 671660 ko \|\| -0m00.08s \|\| 40 ko \| -1.91% \| +0.00% 0m04.57s \| 429152 ko \| Arithmetic/MontgomeryReduction/Proofs.vo \| 0m04.57s \| 429128 ko \|\| +0m00.00s \|\| 24 ko \| +0.00% \| +0.00% 0m04.48s \| 472764 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo \| 0m04.50s \| 472612 ko \|\| -0m00.01s \|\| 152 ko \| -0.44% \| +0.03% 0m04.33s \| 458704 ko \| Util/ZRange/BasicLemmas.vo \| 0m04.38s \| 458720 ko \|\| -0m00.04s \|\| -16 ko \| -1.14% \| -0.00% 0m04.28s \| 441536 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo \| 0m04.23s \| 441536 ko \|\| +0m00.04s \|\| 0 ko \| +1.18% \| +0.00% 0m04.26s \| 547908 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo \| 0m04.26s \| 547852 ko \|\| +0m00.00s \|\| 56 ko \| +0.00% \| +0.01% 0m04.19s \| 441516 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo \| 0m04.22s \| 441528 ko \|\| -0m00.02s \|\| -12 ko \| -0.71% \| -0.00% 0m04.18s \| 31108 ko \| fiat-go/64/p521/p521.go \| 0m03.76s \| 31108 ko \|\| +0m00.41s \|\| 0 ko \| +11.17% \| +0.00% 0m04.17s \| 468056 ko \| Rewriter/Language/IdentifiersBasicLibrary.vo \| 0m04.11s \| 467792 ko \|\| +0m00.05s \|\| 264 ko \| +1.45% \| +0.05% 0m04.08s \| 442436 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo \| 0m04.00s \| 442248 ko \|\| +0m00.08s \|\| 188 ko \| +2.00% \| +0.04% 0m04.08s \| 474804 ko \| Algebra/Field_test.vo \| 0m04.09s \| 474804 ko \|\| -0m00.00s \|\| 0 ko \| -0.24% \| +0.00% 0m04.07s \| 442312 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo \| 0m04.11s \| 442244 ko \|\| -0m00.04s \|\| 68 ko \| -0.97% \| +0.01% 0m03.89s \| 452624 ko \| UnsaturatedSolinasHeuristics.vo \| 0m03.87s \| 452732 ko \|\| +0m00.02s \|\| -108 ko \| +0.51% \| -0.02% 0m03.89s \| 43892 ko \| fiat-bedrock2/src/p521_64.c \| 0m03.49s \| 40668 ko \|\| +0m00.39s \|\| 3224 ko \| +11.46% \| +7.92% 0m03.86s \| 484156 ko \| Curves/Montgomery/Affine.vo \| 0m03.83s \| 484128 ko \|\| +0m00.02s \|\| 28 ko \| +0.78% \| +0.00% 0m03.84s \| 460308 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Core.vo \| 0m03.84s \| 460252 ko \|\| +0m00.00s \|\| 56 ko \| +0.00% \| +0.01% 0m03.79s \| 559560 ko \| Assembly/Parse/Examples/fiat_p256_square_optimised_seed46.vo \| 0m03.81s \| 559600 ko \|\| -0m00.02s \|\| -40 ko \| -0.52% \| -0.00% 0m03.62s \| 734040 ko \| Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo \| 0m03.69s \| 733860 ko \|\| -0m00.06s \|\| 180 ko \| -1.89% \| +0.02% 0m03.57s \| 446520 ko \| Arithmetic/BarrettReduction/Generalized.vo \| 0m03.54s \| 446656 ko \|\| +0m00.02s \|\| -136 ko \| +0.84% \| -0.03% 0m03.55s \| 411908 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SlowGoals.vo \| 0m03.58s \| 412004 ko \|\| -0m00.03s \|\| -96 ko \| -0.83% \| -0.02% 0m03.53s \| 452752 ko \| Arithmetic/UniformWeight.vo \| 0m03.55s \| 452712 ko \|\| -0m00.02s \|\| 40 ko \| -0.56% \| +0.00% 0m03.42s \| 448052 ko \| CastLemmas.vo \| 0m03.49s \| 448100 ko \|\| -0m00.07s \|\| -48 ko \| -2.00% \| -0.01% 0m03.38s \| 422240 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ident_of_string.vo \| 0m03.38s \| 422216 ko \|\| +0m00.00s \|\| 24 ko \| +0.00% \| +0.00% 0m03.35s \| 711840 ko \| Bedrock/Field/Synthesis/Examples/MulTwice.vo \| 0m03.22s \| 711944 ko \|\| +0m00.12s \|\| -104 ko \| +4.03% \| -0.01% 0m03.34s \| 439820 ko \| Util/ZUtil/LandLorShiftBounds.vo \| 0m03.29s \| 439684 ko \|\| +0m00.04s \|\| 136 ko \| +1.51% \| +0.03% 0m03.30s \| 433500 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalNoMul.vo \| 0m03.32s \| 433436 ko \|\| -0m00.02s \|\| 64 ko \| -0.60% \| +0.01% 0m03.27s \| 440028 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo \| 0m03.24s \| 439920 ko \|\| +0m00.02s \|\| 108 ko \| +0.92% \| +0.02% 0m03.26s \| 564952 ko \| PushButtonSynthesis/BaseConversionReificationCache.vo \| 0m03.23s \| 564760 ko \|\| +0m00.02s \|\| 192 ko \| +0.92% \| +0.03% 0m03.26s \| 27064 ko \| fiat-zig/src/p521_64.zig \| 0m02.91s \| 26824 ko \|\| +0m00.34s \|\| 240 ko \| +12.02% \| +0.89% 0m03.23s \| 392780 ko \| Algebra/Group.vo \| 0m03.23s \| 392668 ko \|\| +0m00.00s \|\| 112 ko \| +0.00% \| +0.02% 0m03.23s \| 443740 ko \| Util/ZUtil/LandLorBounds.vo \| 0m03.24s \| 443512 ko \|\| -0m00.01s \|\| 228 ko \| -0.30% \| +0.05% 0m03.23s \| 26944 ko \| fiat-rust/src/p521_64.rs \| 0m03.18s \| 25740 ko \|\| +0m00.04s \|\| 1204 ko \| +1.57% \| +4.67% 0m03.20s \| 432564 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo \| 0m03.20s \| 432792 ko \|\| +0m00.00s \|\| -228 ko \| +0.00% \| -0.05% 0m03.20s \| 439772 ko \| Arithmetic/BarrettReduction/HAC.vo \| 0m03.26s \| 439880 ko \|\| -0m00.05s \|\| -108 ko \| -1.84% \| -0.02% 0m03.19s \| 598172 ko \| Bedrock/Field/Synthesis/Generic/Bignum.vo \| 0m03.21s \| 598220 ko \|\| -0m00.02s \|\| -48 ko \| -0.62% \| -0.00% 0m03.13s \| 679816 ko \| PushButtonSynthesis/FancyMontgomeryReduction.vo \| 0m03.15s \| 679856 ko \|\| -0m00.02s \|\| -40 ko \| -0.63% \| -0.00% 0m03.11s \| 653740 ko \| Bedrock/Group/ScalarMult/ScalarMult.vo \| 0m03.01s \| 653740 ko \|\| +0m00.10s \|\| 0 ko \| +3.32% \| +0.00% 0m03.09s \| 46548 ko \| fiat-bedrock2/src/secp256k1_64.c \| 0m03.04s \| 41768 ko \|\| +0m00.04s \|\| 4780 ko \| +1.64% \| +11.44% 0m03.07s \| 462952 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Pipeline.vo \| 0m03.02s \| 462896 ko \|\| +0m00.04s \|\| 56 ko \| +1.65% \| +0.01% 0m03.04s \| 38324 ko \| fiat-json/src/p521_64.json \| 0m03.33s \| 38320 ko \|\| -0m00.29s \|\| 4 ko \| -8.70% \| +0.01% 0m02.99s \| 464536 ko \| MiscCompilerPassesProofs.vo \| 0m03.02s \| 464532 ko \|\| -0m00.02s \|\| 4 ko \| -0.99% \| +0.00% 0m02.99s \| 514468 ko \| Rewriter/Passes/Test.vo \| 0m02.95s \| 514388 ko \|\| +0m00.04s \|\| 80 ko \| +1.35% \| +0.01% 0m02.94s \| 411368 ko \| Coqprime/PrimalityTest/PocklingtonCertificat.vo \| 0m02.94s \| 411456 ko \|\| +0m00.00s \|\| -88 ko \| +0.00% \| -0.02% 0m02.93s \| 532408 ko \| Rewriter/Passes/AddAssocLeft.vo \| 0m02.90s \| 532476 ko \|\| +0m00.03s \|\| -68 ko \| +1.03% \| -0.01% 0m02.92s \| 430468 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Properties.vo \| 0m02.94s \| 430764 ko \|\| -0m00.02s \|\| -296 ko \| -0.68% \| -0.06% 0m02.91s \| 696072 ko \| Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo \| 0m02.90s \| 696152 ko \|\| +0m00.01s \|\| -80 ko \| +0.34% \| -0.01% 0m02.89s \| 606684 ko \| Bedrock/Field/Interface/Compilation2.vo \| 0m02.98s \| 606636 ko \|\| -0m00.08s \|\| 48 ko \| -3.02% \| +0.00% 0m02.89s \| 678700 ko \| PushButtonSynthesis/SaturatedSolinas.vo \| 0m02.90s \| 678680 ko \|\| -0m00.00s \|\| 20 ko \| -0.34% \| +0.00% 0m02.87s \| 25412 ko \| fiat-c/src/p521_64.c \| 0m03.17s \| 25180 ko \|\| -0m00.29s \|\| 232 ko \| -9.46% \| +0.92% 0m02.77s \| 426736 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo \| 0m02.77s \| 426508 ko \|\| +0m00.00s \|\| 228 ko \| +0.00% \| +0.05% 0m02.76s \| 35212 ko \| fiat-go/64/p448solinas/p448solinas.go \| 0m02.77s \| 33020 ko \|\| -0m00.01s \|\| 2192 ko \| -0.36% \| +6.63% 0m02.71s \| 436380 ko \| Arithmetic/Primitives.vo \| 0m02.71s \| 436244 ko \|\| +0m00.00s \|\| 136 ko \| +0.00% \| +0.03% 0m02.70s \| 434284 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/List.vo \| 0m02.64s \| 434396 ko \|\| +0m00.06s \|\| -112 ko \| +2.27% \| -0.02% 0m02.70s \| 43976 ko \| fiat-bedrock2/src/p448_solinas_64.c \| 0m02.68s \| 43764 ko \|\| +0m00.02s \|\| 212 ko \| +0.74% \| +0.48% 0m02.69s \| 41792 ko \| fiat-go/64/secp256k1/secp256k1.go \| 0m02.70s \| 45244 ko \|\| -0m00.01s \|\| -3452 ko \| -0.37% \| -7.62% 0m02.64s \| 52116 ko \| fiat-json/src/secp256k1_64.json \| 0m02.67s \| 52444 ko \|\| -0m00.02s \|\| -328 ko \| -1.12% \| -0.62% 0m02.62s \| 40232 ko \| fiat-bedrock2/src/curve25519_32.c \| 0m02.59s \| 39884 ko \|\| +0m00.03s \|\| 348 ko \| +1.15% \| +0.87% 0m02.62s \| 44520 ko \| fiat-zig/src/secp256k1_64.zig \| 0m02.61s \| 42560 ko \|\| +0m00.01s \|\| 1960 ko \| +0.38% \| +4.60% 0m02.60s \| 703184 ko \| CLI.vo \| 0m02.70s \| 703008 ko \|\| -0m00.10s \|\| 176 ko \| -3.70% \| +0.02% 0m02.58s \| 42084 ko \| fiat-rust/src/secp256k1_64.rs \| 0m02.54s \| 44504 ko \|\| +0m00.04s \|\| -2420 ko \| +1.57% \| -5.43% 0m02.56s \| 528432 ko \| Bedrock/Field/Translation/Expr.vo \| 0m02.54s \| 528460 ko \|\| +0m00.02s \|\| -28 ko \| +0.78% \| -0.00% 0m02.55s \| 422912 ko \| Util/Bool/Reflect.vo \| 0m02.54s \| 422836 ko \|\| +0m00.00s \|\| 76 ko \| +0.39% \| +0.01% 0m02.54s \| 42752 ko \| fiat-c/src/secp256k1_64.c \| 0m02.50s \| 43268 ko \|\| +0m00.04s \|\| -516 ko \| +1.60% \| -1.19% 0m02.51s \| 530012 ko \| Rewriter/Passes/FlattenThunkedRects.vo \| 0m02.45s \| 530016 ko \|\| +0m00.05s \|\| -4 ko \| +2.44% \| -0.00% 0m02.51s \| 423120 ko \| Rewriter/Util/Bool/Reflect.vo \| 0m02.50s \| 423044 ko \|\| +0m00.00s \|\| 76 ko \| +0.39% \| +0.01% 0m02.51s \| 421536 ko \| Util/ZUtil/ZSimplify/Autogenerated.vo \| 0m02.54s \| 421548 ko \|\| -0m00.03s \|\| -12 ko \| -1.18% \| -0.00% 0m02.48s \| 444144 ko \| Util/MSets/Iso.vo \| 0m02.50s \| 444224 ko \|\| -0m00.02s \|\| -80 ko \| -0.80% \| -0.01% 0m02.45s \| 432772 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/MulTrapHandler.vo \| 0m02.42s \| 432952 ko \|\| +0m00.03s \|\| -180 ko \| +1.23% \| -0.04% 0m02.41s \| 463948 ko \| Util/ZUtil/Morphisms.vo \| 0m02.33s \| 463972 ko \|\| +0m00.08s \|\| -24 ko \| +3.43% \| -0.00% 0m02.39s \| 42920 ko \| fiat-bedrock2/src/p224_64.c \| 0m02.39s \| 43876 ko \|\| +0m00.00s \|\| -956 ko \| +0.00% \| -2.17% 0m02.37s \| 460120 ko \| Spec/MontgomeryCurve.vo \| 0m02.31s \| 460076 ko \|\| +0m00.06s \|\| 44 ko \| +2.59% \| +0.00% 0m02.32s \| 442392 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo \| 0m02.33s \| 442460 ko \|\| -0m00.01s \|\| -68 ko \| -0.42% \| -0.01% 0m02.30s \| 45680 ko \| fiat-bedrock2/src/p256_64.c \| 0m02.24s \| 44508 ko \|\| +0m00.05s \|\| 1172 ko \| +2.67% \| +2.63% 0m02.25s \| 454636 ko \| Arithmetic/Freeze.vo \| 0m02.18s \| 454636 ko \|\| +0m00.06s \|\| 0 ko \| +3.21% \| +0.00% 0m02.23s \| 584688 ko \| Bedrock/Field/Common/Arrays/MakeAccessSizes.vo \| 0m02.28s \| 584628 ko \|\| -0m00.04s \|\| 60 ko \| -2.19% \| +0.01% 0m02.23s \| 427044 ko \| Util/ZUtil/TwosComplement.vo \| 0m02.19s \| 427068 ko \|\| +0m00.04s \|\| -24 ko \| +1.82% \| -0.00% 0m02.19s \| 435780 ko \| Util/ZUtil/Shift.vo \| 0m02.35s \| 435832 ko \|\| -0m00.16s \|\| -52 ko \| -6.80% \| -0.01% 0m02.16s \| 24724 ko \| fiat-go/32/curve25519/curve25519.go \| 0m02.18s \| 24904 ko \|\| -0m00.02s \|\| -180 ko \| -0.91% \| -0.72% 0m02.10s \| 40616 ko \| fiat-json/src/p448_solinas_64.json \| 0m02.03s \| 38896 ko \|\| +0m00.07s \|\| 1720 ko \| +3.44% \| +4.42% 0m02.06s \| 40488 ko \| fiat-go/64/p224/p224.go \| 0m02.04s \| 42936 ko \|\| +0m00.02s \|\| -2448 ko \| +0.98% \| -5.70% 0m02.01s \| 25764 ko \| fiat-zig/src/p448_solinas_64.zig \| 0m02.00s \| 25696 ko \|\| +0m00.00s \|\| 68 ko \| +0.49% \| +0.26% 0m02.00s \| 387516 ko \| Util/Wf2.vo \| 0m01.97s \| 387556 ko \|\| +0m00.03s \|\| -40 ko \| +1.52% \| -0.01% 0m02.00s \| 39732 ko \| fiat-go/64/p256/p256.go \| 0m02.03s \| 43468 ko \|\| -0m00.02s \|\| -3736 ko \| -1.47% \| -8.59% 0m02.00s \| 25556 ko \| fiat-rust/src/p448_solinas_64.rs \| 0m01.97s \| 24312 ko \|\| +0m00.03s \|\| 1244 ko \| +1.52% \| +5.11% 0m01.98s \| 25544 ko \| fiat-c/src/p448_solinas_64.c \| 0m01.95s \| 24592 ko \|\| +0m00.03s \|\| 952 ko \| +1.53% \| +3.87% 0m01.97s \| 53188 ko \| fiat-json/src/p224_64.json \| 0m02.03s \| 49100 ko \|\| -0m00.05s \|\| 4088 ko \| -2.95% \| +8.32% 0m01.97s \| 46956 ko \| fiat-json/src/p256_64.json \| 0m02.01s \| 48880 ko \|\| -0m00.03s \|\| -1924 ko \| -1.99% \| -3.93% 0m01.96s \| 526404 ko \| Stringification/Language.vo \| 0m01.99s \| 526492 ko \|\| -0m00.03s \|\| -88 ko \| -1.50% \| -0.01% 0m01.94s \| 453880 ko \| Arithmetic/BaseConversion.vo \| 0m01.96s \| 453824 ko \|\| -0m00.02s \|\| 56 ko \| -1.02% \| +0.01% 0m01.93s \| 414308 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo \| 0m01.95s \| 414048 ko \|\| -0m00.02s \|\| 260 ko \| -1.02% \| +0.06% 0m01.92s \| 428044 ko \| Util/ZUtil/ModInv.vo \| 0m01.83s \| 428092 ko \|\| +0m00.08s \|\| -48 ko \| +4.91% \| -0.01% 0m01.92s \| 38772 ko \| fiat-json/src/curve25519_32.json \| 0m01.91s \| 38952 ko \|\| +0m00.01s \|\| -180 ko \| +0.52% \| -0.46% 0m01.91s \| 41480 ko \| fiat-zig/src/p224_64.zig \| 0m01.96s \| 43928 ko \|\| -0m00.05s \|\| -2448 ko \| -2.55% \| -5.57% 0m01.90s \| 44580 ko \| fiat-c/src/p224_64.c \| 0m01.91s \| 41984 ko \|\| -0m00.01s \|\| 2596 ko \| -0.52% \| +6.18% 0m01.90s \| 43336 ko \| fiat-c/src/p256_64.c \| 0m01.80s \| 43060 ko \|\| +0m00.09s \|\| 276 ko \| +5.55% \| +0.64% 0m01.88s \| 440560 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Arrays.vo \| 0m01.89s \| 440620 ko \|\| -0m00.01s \|\| -60 ko \| -0.52% \| -0.01% 0m01.88s \| 40040 ko \| fiat-rust/src/p224_64.rs \| 0m01.89s \| 40532 ko \|\| -0m00.01s \|\| -492 ko \| -0.52% \| -1.21% 0m01.88s \| 41504 ko \| fiat-zig/src/p256_64.zig \| 0m01.88s \| 41216 ko \|\| +0m00.00s \|\| 288 ko \| +0.00% \| +0.69% 0m01.87s \| 429832 ko \| Util/ZUtil/Testbit.vo \| 0m01.94s \| 429784 ko \|\| -0m00.06s \|\| 48 ko \| -3.60% \| +0.01% 0m01.86s \| 528316 ko \| Rewriter/Passes/StripLiteralCasts.vo \| 0m01.86s \| 528520 ko \|\| +0m00.00s \|\| -204 ko \| +0.00% \| -0.03% 0m01.86s \| 26004 ko \| fiat-java/src/FiatCurve25519.java \| 0m01.87s \| 26364 ko \|\| -0m00.01s \|\| -360 ko \| -0.53% \| -1.36% 0m01.85s \| 38684 ko \| fiat-rust/src/p256_64.rs \| 0m01.89s \| 43788 ko \|\| -0m00.03s \|\| -5104 ko \| -2.11% \| -11.65% 0m01.83s \| 23956 ko \| fiat-zig/src/curve25519_32.zig \| 0m01.84s \| 24060 ko \|\| -0m00.01s \|\| -104 ko \| -0.54% \| -0.43% 0m01.82s \| 601768 ko \| Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo \| 0m01.74s \| 601716 ko \|\| +0m00.08s \|\| 52 ko \| +4.59% \| +0.00% 0m01.82s \| 580636 ko \| CompilersTestCases.vo \| 0m01.67s \| 580620 ko \|\| +0m00.15s \|\| 16 ko \| +8.98% \| +0.00% 0m01.81s \| 447124 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo \| 0m01.90s \| 447468 ko \|\| -0m00.08s \|\| -344 ko \| -4.73% \| -0.07% 0m01.81s \| 25412 ko \| fiat-c/src/curve25519_32.c \| 0m01.81s \| 24256 ko \|\| +0m00.00s \|\| 1156 ko \| +0.00% \| +4.76% 0m01.80s \| 424956 ko \| Util/ZUtil/Div.vo \| 0m01.82s \| 425024 ko \|\| -0m00.02s \|\| -68 ko \| -1.09% \| -0.01% 0m01.80s \| 25528 ko \| fiat-rust/src/curve25519_32.rs \| 0m01.79s \| 25408 ko \|\| +0m00.01s \|\| 120 ko \| +0.55% \| +0.47% 0m01.79s \| 526480 ko \| Rewriter/Passes/UnfoldValueBarrier.vo \| 0m01.77s \| 526512 ko \|\| +0m00.02s \|\| -32 ko \| +1.12% \| -0.00% 0m01.74s \| 435652 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo \| 0m01.68s \| 435560 ko \|\| +0m00.06s \|\| 92 ko \| +3.57% \| +0.02% 0m01.73s \| 593480 ko \| Bedrock/Field/Common/Names/MakeNames.vo \| 0m01.61s \| 593268 ko \|\| +0m00.11s \|\| 212 ko \| +7.45% \| +0.03% 0m01.71s \| 413816 ko \| Util/ListUtil/Forall.vo \| 0m01.74s \| 413720 ko \|\| -0m00.03s \|\| 96 ko \| -1.72% \| +0.02% 0m01.70s \| 632444 ko \| Bedrock/Field/Translation/Cmd.vo \| 0m01.69s \| 632568 ko \|\| +0m00.01s \|\| -124 ko \| +0.59% \| -0.01% 0m01.69s \| 446236 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo \| 0m01.75s \| 446208 ko \|\| -0m00.06s \|\| 28 ko \| -3.42% \| +0.00% 0m01.68s \| 451852 ko \| Arithmetic/ModOps.vo \| 0m01.72s \| 451908 ko \|\| -0m00.04s \|\| -56 ko \| -2.32% \| -0.01% 0m01.66s \| 440448 ko \| Arithmetic/ModularArithmeticTheorems.vo \| 0m01.58s \| 440576 ko \|\| +0m00.07s \|\| -128 ko \| +5.06% \| -0.02% 0m01.63s \| 430540 ko \| Util/Tuple.vo \| 0m01.64s \| 430760 ko \|\| -0m00.01s \|\| -220 ko \| -0.60% \| -0.05% 0m01.62s \| 428244 ko \| Arithmetic/BarrettReduction/RidiculousFish.vo \| 0m01.72s \| 428352 ko \|\| -0m00.09s \|\| -108 ko \| -5.81% \| -0.02% 0m01.61s \| 430556 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo \| 0m01.62s \| 430604 ko \|\| -0m00.01s \|\| -48 ko \| -0.61% \| -0.01% 0m01.61s \| 504728 ko \| AbstractInterpretation/AbstractInterpretation.vo \| 0m01.59s \| 504488 ko \|\| +0m00.02s \|\| 240 ko \| +1.25% \| +0.04% 0m01.60s \| 525448 ko \| Rewriter/Passes/ToFancy.vo \| 0m01.70s \| 525552 ko \|\| -0m00.09s \|\| -104 ko \| -5.88% \| -0.01% 0m01.53s \| 431264 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo \| 0m01.59s \| 431124 ko \|\| -0m00.06s \|\| 140 ko \| -3.77% \| +0.03% 0m01.53s \| 508128 ko \| AbstractInterpretation/ZRange.vo \| 0m01.46s \| 508272 ko \|\| +0m00.07s \|\| -144 ko \| +4.79% \| -0.02% 0m01.52s \| 434244 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo \| 0m01.56s \| 434400 ko \|\| -0m00.04s \|\| -156 ko \| -2.56% \| -0.03% 0m01.50s \| 409480 ko \| Rewriter/Util/ListUtil/Forall.vo \| 0m01.45s \| 409360 ko \|\| +0m00.05s \|\| 120 ko \| +3.44% \| +0.02% 0m01.48s \| 458412 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo \| 0m01.51s \| 458392 ko \|\| -0m00.03s \|\| 20 ko \| -1.98% \| +0.00% 0m01.46s \| 465076 ko \| Assembly/Parse.vo \| 0m01.39s \| 465260 ko \|\| +0m00.07s \|\| -184 ko \| +5.03% \| -0.03% 0m01.45s \| 427540 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo \| 0m01.45s \| 427300 ko \|\| +0m00.00s \|\| 240 ko \| +0.00% \| +0.05% 0m01.45s \| 626784 ko \| Bedrock/Field/Translation/Func.vo \| 0m01.51s \| 626580 ko \|\| -0m00.06s \|\| 204 ko \| -3.97% \| +0.03% 0m01.43s \| 449096 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FitsStack.vo \| 0m01.42s \| 449184 ko \|\| +0m00.01s \|\| -88 ko \| +0.70% \| -0.01% 0m01.42s \| 435444 ko \| Spec/WeierstrassCurve.vo \| 0m01.37s \| 435260 ko \|\| +0m00.04s \|\| 184 ko \| +3.64% \| +0.04% 0m01.40s \| 409140 ko \| Coqprime/Z/Pmod.vo \| 0m01.46s \| 409228 ko \|\| -0m00.06s \|\| -88 ko \| -4.10% \| -0.02% 0m01.39s \| 711096 ko \| Rewriter/PerfTesting/Core.vo \| 0m01.34s \| 711044 ko \|\| +0m00.04s \|\| 52 ko \| +3.73% \| +0.00% 0m01.38s \| 433516 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/InlineTables.vo \| 0m01.38s \| 433380 ko \|\| +0m00.00s \|\| 136 ko \| +0.00% \| +0.03% 0m01.38s \| 454604 ko \| Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed10.vo \| 0m01.30s \| 454608 ko \|\| +0m00.07s \|\| -4 ko \| +6.15% \| -0.00% 0m01.37s \| 410304 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapEauto.vo \| 0m01.43s \| 410500 ko \|\| -0m00.05s \|\| -196 ko \| -4.19% \| -0.04% 0m01.37s \| 415992 ko \| Algebra/ScalarMult.vo \| 0m01.37s \| 415896 ko \|\| +0m00.00s \|\| 96 ko \| +0.00% \| +0.02% 0m01.36s \| 572144 ko \| Assembly/Equivalence.vo \| 0m01.43s \| 571988 ko \|\| -0m00.06s \|\| 156 ko \| -4.89% \| +0.02% 0m01.36s \| 413152 ko \| Util/ZUtil/Rshi.vo \| 0m01.34s \| 413040 ko \|\| +0m00.02s \|\| 112 ko \| +1.49% \| +0.02% 0m01.33s \| 434008 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Compiler.vo \| 0m01.36s \| 433912 ko \|\| -0m00.03s \|\| 96 ko \| -2.20% \| +0.02% 0m01.32s \| 408692 ko \| Rewriter/Rewriter/Examples/PerfTesting/Harness.vo \| 0m01.30s \| 408784 ko \|\| +0m00.02s \|\| -92 ko \| +1.53% \| -0.02% 0m01.31s \| 432220 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo \| 0m01.36s \| 432216 ko \|\| -0m00.05s \|\| 4 ko \| -3.67% \| +0.00% 0m01.31s \| 454544 ko \| Assembly/Parse/Examples/fiat_25519_carry_square_optimised.vo \| 0m01.37s \| 454696 ko \|\| -0m00.06s \|\| -152 ko \| -4.37% \| -0.03% 0m01.31s \| 522020 ko \| Stringification/Go.vo \| 0m01.27s \| 521924 ko \|\| +0m00.04s \|\| 96 ko \| +3.14% \| +0.01% 0m01.31s \| 414164 ko \| Util/ListUtil/StdlibCompat.vo \| 0m01.27s \| 414268 ko \|\| +0m00.04s \|\| -104 ko \| +3.14% \| -0.02% 0m01.30s \| 450640 ko \| Assembly/Parse/Examples/fiat_25519_carry_square_optimised_seed20.vo \| 0m01.30s \| 450692 ko \|\| +0m00.00s \|\| -52 ko \| +0.00% \| -0.01% 0m01.28s \| 443376 ko \| Util/ZRange/SplitRangeBounds.vo \| 0m01.34s \| 443164 ko \|\| -0m00.06s \|\| 212 ko \| -4.47% \| +0.04% 0m01.28s \| 429496 ko \| Util/ZUtil/Pow2Mod.vo \| 0m01.34s \| 429380 ko \|\| -0m00.06s \|\| 116 ko \| -4.47% \| +0.02% 0m01.25s \| 430392 ko \| Util/ZUtil/TruncatingShiftl.vo \| 0m01.28s \| 430448 ko \|\| -0m00.03s \|\| -56 ko \| -2.34% \| -0.01% 0m01.24s \| 465864 ko \| Rewriter/Language/IdentifiersLibrary.vo \| 0m01.27s \| 465584 ko \|\| -0m00.03s \|\| 280 ko \| -2.36% \| +0.06% 0m01.22s \| 433156 ko \| Util/ZUtil/Bitwise.vo \| 0m01.25s \| 432972 ko \|\| -0m00.03s \|\| 184 ko \| -2.40% \| +0.04% 0m01.19s \| 609700 ko \| Bedrock/Specs/Field.vo \| 0m01.18s \| 610060 ko \|\| +0m00.01s \|\| -360 ko \| +0.84% \| -0.05% 0m01.18s \| 681288 ko \| Bedrock/Field/Stringification/Stringification.vo \| 0m01.26s \| 681464 ko \|\| -0m00.08s \|\| -176 ko \| -6.34% \| -0.02% 0m01.18s \| 702344 ko \| Bedrock/Field/Synthesis/Specialized/UnsaturatedSolinas.vo \| 0m01.15s \| 702240 ko \|\| +0m00.03s \|\| 104 ko \| +2.60% \| +0.01% 0m01.17s \| 423336 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo \| 0m01.14s \| 423156 ko \|\| +0m00.03s \|\| 180 ko \| +2.63% \| +0.04% 0m01.16s \| 425680 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo \| 0m01.21s \| 425508 ko \|\| -0m00.05s \|\| 172 ko \| -4.13% \| +0.04% 0m01.15s \| 428836 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo \| 0m01.16s \| 428756 ko \|\| -0m00.01s \|\| 80 ko \| -0.86% \| +0.01% 0m01.15s \| 720468 ko \| Rewriter/PerfTesting/StandaloneOCamlMain.vo \| 0m01.19s \| 720628 ko \|\| -0m00.04s \|\| -160 ko \| -3.36% \| -0.02% 0m01.14s \| 714344 ko \| Bedrock/Field/Synthesis/Specialized/WordByWordMontgomery.vo \| 0m01.18s \| 713952 ko \|\| -0m00.04s \|\| 392 ko \| -3.38% \| +0.05% 0m01.12s \| 407644 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PropSet.vo \| 0m01.14s \| 407440 ko \|\| -0m00.01s \|\| 204 ko \| -1.75% \| +0.05% 0m01.11s \| 443592 ko \| Arithmetic/Partition.vo \| 0m01.14s \| 443372 ko \|\| -0m00.02s \|\| 220 ko \| -2.63% \| +0.04% 0m01.11s \| 733252 ko \| Bedrock/Standalone/StandaloneHaskellMain.vo \| 0m01.04s \| 733492 ko \|\| +0m00.07s \|\| -240 ko \| +6.73% \| -0.03% 0m01.11s \| 434276 ko \| Util/ZUtil/Quot.vo \| 0m01.12s \| 434052 ko \|\| -0m00.01s \|\| 224 ko \| -0.89% \| +0.05% 0m01.10s \| 416528 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndianList.vo \| 0m01.04s \| 416508 ko \|\| +0m00.06s \|\| 20 ko \| +5.76% \| +0.00% 0m01.10s \| 689776 ko \| Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo \| 0m01.16s \| 689800 ko \|\| -0m00.05s \|\| -24 ko \| -5.17% \| -0.00% 0m01.08s \| 466632 ko \| Arithmetic/PrimeFieldTheorems.vo \| 0m01.08s \| 466648 ko \|\| +0m00.00s \|\| -16 ko \| +0.00% \| -0.00% 0m01.07s \| 410140 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo \| 0m01.06s \| 410200 ko \|\| +0m00.01s \|\| -60 ko \| +0.94% \| -0.01% 0m01.07s \| 686328 ko \| Bedrock/Field/Synthesis/Generic/Operation.vo \| 0m01.13s \| 686144 ko \|\| -0m00.05s \|\| 184 ko \| -5.30% \| +0.02% 0m01.07s \| 438488 ko \| Curves/Edwards/XYZT/Precomputed.vo \| 0m01.10s \| 438344 ko \|\| -0m00.03s \|\| 144 ko \| -2.72% \| +0.03% 0m01.07s \| 446848 ko \| Fancy/Spec.vo \| 0m01.06s \| 447116 ko \|\| +0m00.01s \|\| -268 ko \| +0.94% \| -0.05% 0m01.06s \| 438612 ko \| Util/ZRange/SplitBounds.vo \| 0m01.06s \| 438640 ko \|\| +0m00.00s \|\| -28 ko \| +0.00% \| -0.00% 0m01.04s \| 415964 ko \| Util/ZUtil/AddGetCarry.vo \| 0m01.07s \| 415900 ko \|\| -0m00.03s \|\| 64 ko \| -2.80% \| +0.01% 0m01.03s \| 593856 ko \| Bedrock/Field/Common/Arrays/MaxBounds.vo \| 0m00.99s \| 593808 ko \|\| +0m00.04s \|\| 48 ko \| +4.04% \| +0.00% 0m01.03s \| 682588 ko \| Bedrock/Field/Synthesis/Generic/Tactics.vo \| 0m01.05s \| 682344 ko \|\| -0m00.02s \|\| 244 ko \| -1.90% \| +0.03% 0m01.02s \| 699716 ko \| Bedrock/Field/Synthesis/New/ComputedOp.vo \| 0m01.03s \| 699468 ko \|\| -0m00.01s \|\| 248 ko \| -0.97% \| +0.03% 0m01.01s \| 438076 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo \| 0m00.98s \| 438208 ko \|\| +0m00.03s \|\| -132 ko \| +3.06% \| -0.03% 0m01.01s \| 691648 ko \| Bedrock/Field/Synthesis/Specialized/ReifiedOperation.vo \| 0m01.00s \| 691560 ko \|\| +0m00.01s \|\| 88 ko \| +1.00% \| +0.01% 0m01.00s \| 733380 ko \| Bedrock/Standalone/StandaloneOCamlMain.vo \| 0m01.11s \| 733324 ko \|\| -0m00.11s \|\| 56 ko \| -9.90% \| +0.00% 0m01.00s \| 410608 ko \| Coqprime/PrimalityTest/EGroup.vo \| 0m00.93s \| 410812 ko \|\| +0m00.06s \|\| -204 ko \| +7.52% \| -0.04% 0m01.00s \| 697828 ko \| StandaloneOCamlMain.vo \| 0m01.07s \| 698004 ko \|\| -0m00.07s \|\| -176 ko \| -6.54% \| -0.02% 0m01.00s \| 518768 ko \| Stringification/JSON.vo \| 0m00.92s \| 518808 ko \|\| +0m00.07s \|\| -40 ko \| +8.69% \| -0.00% 0m00.99s \| 584952 ko \| Bedrock/Field/Common/Arrays/ByteBounds.vo \| 0m00.98s \| 584960 ko \|\| +0m00.01s \|\| -8 ko \| +1.02% \| -0.00% 0m00.99s \| 684160 ko \| Bedrock/Field/Synthesis/Specialized/Tactics.vo \| 0m00.98s \| 684260 ko \|\| +0m00.01s \|\| -100 ko \| +1.02% \| -0.01% 0m00.97s \| 512012 ko \| Bedrock/Field/Translation/LoadStoreList.vo \| 0m00.97s \| 512096 ko \|\| +0m00.00s \|\| -84 ko \| +0.00% \| -0.01% 0m00.97s \| 641968 ko \| Bedrock/Field/Translation/Parameters/Defaults32.vo \| 0m00.92s \| 641872 ko \|\| +0m00.04s \|\| 96 ko \| +5.43% \| +0.01% 0m00.97s \| 697840 ko \| StandaloneHaskellMain.vo \| 0m00.95s \| 697940 ko \|\| +0m00.02s \|\| -100 ko \| +2.10% \| -0.01% 0m00.96s \| 637552 ko \| Bedrock/Field/Translation/Parameters/Defaults.vo \| 0m00.93s \| 637636 ko \|\| +0m00.02s \|\| -84 ko \| +3.22% \| -0.01% 0m00.96s \| 407340 ko \| Coqprime/PrimalityTest/LucasLehmer.vo \| 0m00.96s \| 407348 ko \|\| +0m00.00s \|\| -8 ko \| +0.00% \| -0.00% 0m00.96s \| 358124 ko \| Util/Wf1.vo \| 0m01.01s \| 358384 ko \|\| -0m00.05s \|\| -260 ko \| -4.95% \| -0.07% 0m00.93s \| 641700 ko \| Bedrock/Field/Translation/Parameters/Defaults64.vo \| 0m00.96s \| 641752 ko \|\| -0m00.02s \|\| -52 ko \| -3.12% \| -0.00% 0m00.93s \| 463776 ko \| Rewriter/Rewriter/Rewriter.vo \| 0m00.98s \| 463776 ko \|\| -0m00.04s \|\| 0 ko \| -5.10% \| +0.00% 0m00.93s \| 424112 ko \| Util/ZUtil/OnesFrom.vo \| 0m00.95s \| 424136 ko \|\| -0m00.01s \|\| -24 ko \| -2.10% \| -0.00% 0m00.92s \| 444264 ko \| Rewriter/Language/Language.vo \| 0m00.85s \| 444088 ko \|\| +0m00.07s \|\| 176 ko \| +8.23% \| +0.03% 0m00.92s \| 415308 ko \| Util/NatUtil.vo \| 0m00.89s \| 415368 ko \|\| +0m00.03s \|\| -60 ko \| +3.37% \| -0.01% 0m00.92s \| 428652 ko \| Util/ZUtil/Ones.vo \| 0m00.96s \| 428748 ko \|\| -0m00.03s \|\| -96 ko \| -4.16% \| -0.02% 0m00.91s \| 413196 ko \| Rewriter/Util/NatUtil.vo \| 0m00.96s \| 413224 ko \|\| -0m00.04s \|\| -28 ko \| -5.20% \| -0.00% 0m00.90s \| 512048 ko \| Bedrock/Field/Translation/Proofs/Equivalence.vo \| 0m00.92s \| 512088 ko \|\| -0m00.02s \|\| -40 ko \| -2.17% \| -0.00% 0m00.88s \| 601512 ko \| Bedrock/Field/Interface/Representation.vo \| 0m00.84s \| 601476 ko \|\| +0m00.04s \|\| 36 ko \| +4.76% \| +0.00% 0m00.88s \| 482796 ko \| Rewriter/Rewriter/AllTactics.vo \| 0m00.90s \| 482812 ko \|\| -0m00.02s \|\| -16 ko \| -2.22% \| -0.00% 0m00.86s \| 408248 ko \| Coqprime/PrimalityTest/Pocklington.vo \| 0m00.81s \| 408256 ko \|\| +0m00.04s \|\| -8 ko \| +6.17% \| -0.00% 0m00.85s \| 521776 ko \| Stringification/C.vo \| 0m00.88s \| 521964 ko \|\| -0m00.03s \|\| -188 ko \| -3.40% \| -0.03% 0m00.84s \| 405852 ko \| Coqprime/Z/ZCAux.vo \| 0m00.83s \| 405644 ko \|\| +0m00.01s \|\| 208 ko \| +1.20% \| +0.05% 0m00.83s \| 603944 ko \| Bedrock/Group/Point.vo \| 0m00.92s \| 604004 ko \|\| -0m00.09s \|\| -60 ko \| -9.78% \| -0.00% 0m00.83s \| 424504 ko \| Curves/Montgomery/AffineInstances.vo \| 0m00.81s \| 424620 ko \|\| +0m00.01s \|\| -116 ko \| +2.46% \| -0.02% 0m00.81s \| 430196 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalNoMul.vo \| 0m00.74s \| 430284 ko \|\| +0m00.07s \|\| -88 ko \| +9.45% \| -0.02% 0m00.80s \| 517880 ko \| Stringification/Zig.vo \| 0m00.83s \| 517984 ko \|\| -0m00.02s \|\| -104 ko \| -3.61% \| -0.02% 0m00.79s \| 463924 ko \| Rewriter/Rewriter/Reify.vo \| 0m00.86s \| 464180 ko \|\| -0m00.06s \|\| -256 ko \| -8.13% \| -0.05% 0m00.79s \| 518268 ko \| Stringification/Rust.vo \| 0m00.80s \| 518188 ko \|\| -0m00.01s \|\| 80 ko \| -1.25% \| +0.01% 0m00.79s \| 418868 ko \| Util/Strings/String_as_OT.vo \| 0m00.83s \| 418860 ko \|\| -0m00.03s \|\| 8 ko \| -4.81% \| +0.00% 0m00.78s \| 580036 ko \| Bedrock/Field/Common/Tactics.vo \| 0m00.81s \| 579928 ko \|\| -0m00.03s \|\| 108 ko \| -3.70% \| +0.01% 0m00.77s \| 408048 ko \| Rewriter/Rewriter/Examples/PerfTesting/Sample.vo \| 0m00.69s \| 407916 ko \|\| +0m00.08s \|\| 132 ko \| +11.59% \| +0.03% 0m00.75s \| 510924 ko \| Bedrock/Field/Common/Types.vo \| 0m00.79s \| 511192 ko \|\| -0m00.04s \|\| -268 ko \| -5.06% \| -0.05% 0m00.74s \| 518220 ko \| Stringification/Java.vo \| 0m00.75s \| 518308 ko \|\| -0m00.01s \|\| -88 ko \| -1.33% \| -0.01% 0m00.73s \| 414036 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/BigEndian.vo \| 0m00.66s \| 414300 ko \|\| +0m00.06s \|\| -264 ko \| +10.60% \| -0.06% 0m00.73s \| 497624 ko \| Language/APINotations.vo \| 0m00.75s \| 497704 ko \|\| -0m00.02s \|\| -80 ko \| -2.66% \| -0.01% 0m00.71s \| 416256 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/LittleEndian.vo \| 0m00.67s \| 416260 ko \|\| +0m00.03s \|\| -4 ko \| +5.97% \| -0.00% 0m00.71s \| 507392 ko \| Bedrock/Field/Translation/Flatten.vo \| 0m00.77s \| 507384 ko \|\| -0m00.06s \|\| 8 ko \| -7.79% \| +0.00% 0m00.71s \| 507168 ko \| Bedrock/Field/Translation/Proofs/VarnameSet.vo \| 0m00.75s \| 507148 ko \|\| -0m00.04s \|\| 20 ko \| -5.33% \| +0.00% 0m00.70s \| 420280 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo \| 0m00.75s \| 420260 ko \|\| -0m00.05s \|\| 20 ko \| -6.66% \| +0.00% 0m00.70s \| 428528 ko \| Arithmetic/BarrettReduction/Wikipedia.vo \| 0m00.64s \| 428684 ko \|\| +0m00.05s \|\| -156 ko \| +9.37% \| -0.03% 0m00.70s \| 511424 ko \| Bedrock/Field/Common/Arrays/MakeListLengths.vo \| 0m00.74s \| 511368 ko \|\| -0m00.04s \|\| 56 ko \| -5.40% \| +0.01% 0m00.70s \| 379800 ko \| Rewriter/Util/Decidable.vo \| 0m00.64s \| 379836 ko \|\| +0m00.05s \|\| -36 ko \| +9.37% \| -0.00% 0m00.69s \| 525364 ko \| Bedrock/Field/Stringification/LoadStoreListVarData.vo \| 0m00.73s \| 525508 ko \|\| -0m00.04s \|\| -144 ko \| -5.47% \| -0.02% 0m00.69s \| 325316 ko \| Util/PartiallyReifiedProp.vo \| 0m00.67s \| 325160 ko \|\| +0m00.01s \|\| 156 ko \| +2.98% \| +0.04% 0m00.68s \| 440404 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ExprCompiler.vo \| 0m00.70s \| 440704 ko \|\| -0m00.01s \|\| -300 ko \| -2.85% \| -0.06% 0m00.68s \| 499656 ko \| AbstractInterpretation/WfExtra.vo \| 0m00.64s \| 499648 ko \|\| +0m00.04s \|\| 8 ko \| +6.25% \| +0.00% 0m00.68s \| 495276 ko \| Language/UnderLetsProofsExtra.vo \| 0m00.68s \| 495088 ko \|\| +0m00.00s \|\| 188 ko \| +0.00% \| +0.03% 0m00.68s \| 495288 ko \| Language/WfExtra.vo \| 0m00.65s \| 495140 ko \|\| +0m00.03s \|\| 148 ko \| +4.61% \| +0.02% 0m00.68s \| 23224 ko \| fiat-go/64/curve25519/curve25519.go \| 0m00.64s \| 23220 ko \|\| +0m00.04s \|\| 4 ko \| +6.25% \| +0.01% 0m00.67s \| 441264 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo \| 0m00.67s \| 441152 ko \|\| +0m00.00s \|\| 112 ko \| +0.00% \| +0.02% 0m00.67s \| 407668 ko \| Coqprime/PrimalityTest/PGroup.vo \| 0m00.67s \| 407772 ko \|\| +0m00.00s \|\| -104 ko \| +0.00% \| -0.02% 0m00.66s \| 426736 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExprSimulation.vo \| 0m00.69s \| 426828 ko \|\| -0m00.02s \|\| -92 ko \| -4.34% \| -0.02% 0m00.66s \| 530024 ko \| Bedrock/Field/Stringification/FlattenVarData.vo \| 0m00.70s \| 529952 ko \|\| -0m00.03s \|\| 72 ko \| -5.71% \| +0.01% 0m00.66s \| 495232 ko \| Rewriter/AllTacticsExtra.vo \| 0m00.63s \| 495240 ko \|\| +0m00.03s \|\| -8 ko \| +4.76% \| -0.00% 0m00.66s \| 435220 ko \| Rewriter/Rules.vo \| 0m00.62s \| 435276 ko \|\| +0m00.04s \|\| -56 ko \| +6.45% \| -0.01% 0m00.65s \| 490328 ko \| Language/API.vo \| 0m00.59s \| 490136 ko \|\| +0m00.06s \|\| 192 ko \| +10.16% \| +0.03% 0m00.64s \| 420056 ko \| Algebra/IntegralDomain.vo \| 0m00.60s \| 419824 ko \|\| +0m00.04s \|\| 232 ko \| +6.66% \| +0.05% 0m00.64s \| 408436 ko \| Coqprime/PrimalityTest/Root.vo \| 0m00.68s \| 408436 ko \|\| -0m00.04s \|\| 0 ko \| -5.88% \| +0.00% 0m00.63s \| 419500 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo \| 0m00.62s \| 419524 ko \|\| +0m00.01s \|\| -24 ko \| +1.61% \| -0.00% 0m00.63s \| 495036 ko \| MiscCompilerPassesProofsExtra.vo \| 0m00.71s \| 495028 ko \|\| -0m00.07s \|\| 8 ko \| -11.26% \| +0.00% 0m00.63s \| 27500 ko \| fiat-bedrock2/src/curve25519_64.c \| 0m00.63s \| 27468 ko \|\| +0m00.00s \|\| 32 ko \| +0.00% \| +0.11% 0m00.62s \| 409992 ko \| Coqprime/PrimalityTest/Cyclic.vo \| 0m00.66s \| 410096 ko \|\| -0m00.04s \|\| -104 ko \| -6.06% \| -0.02% 0m00.62s \| 540268 ko \| Rewriter/All.vo \| 0m00.70s \| 540136 ko \|\| -0m00.07s \|\| 132 ko \| -11.42% \| +0.02% 0m00.61s \| 408032 ko \| Coqprime/Z/ZSum.vo \| 0m00.58s \| 407928 ko \|\| +0m00.03s \|\| 104 ko \| +5.17% \| +0.02% 0m00.61s \| 379744 ko \| Util/Decidable.vo \| 0m00.62s \| 379980 ko \|\| -0m00.01s \|\| -236 ko \| -1.61% \| -0.06% 0m00.61s \| 436372 ko \| Util/NumTheoryUtil.vo \| 0m00.64s \| 436136 ko \|\| -0m00.03s \|\| 236 ko \| -4.68% \| +0.05% 0m00.60s \| 417680 ko \| Algebra/SubsetoidRing.vo \| 0m00.54s \| 417608 ko \|\| +0m00.05s \|\| 72 ko \| +11.11% \| +0.01% 0m00.60s \| 455152 ko \| Rewriter/Language/IdentifiersGenerate.vo \| 0m00.50s \| 455384 ko \|\| +0m00.09s \|\| -232 ko \| +19.99% \| -0.05% 0m00.60s \| 469636 ko \| Rewriter/Rewriter/ProofsCommonTactics.vo \| 0m00.52s \| 469704 ko \|\| +0m00.07s \|\| -68 ko \| +15.38% \| -0.01% 0m00.60s \| 428732 ko \| Util/Arg.vo \| 0m00.57s \| 428776 ko \|\| +0m00.03s \|\| -44 ko \| +5.26% \| -0.01% 0m00.59s \| 432216 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ArrayCasts.vo \| 0m00.60s \| 432208 ko \|\| -0m00.01s \|\| 8 ko \| -1.66% \| +0.00% 0m00.59s \| 433140 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/NoExprReflection.vo \| 0m00.62s \| 433220 ko \|\| -0m00.03s \|\| -80 ko \| -4.83% \| -0.01% 0m00.59s \| 417256 ko \| Util/Strings/ParseArithmetic.vo \| 0m00.63s \| 417296 ko \|\| -0m00.04s \|\| -40 ko \| -6.34% \| -0.00% 0m00.58s \| 411684 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/BitOps.vo \| 0m00.64s \| 411612 ko \|\| -0m00.06s \|\| 72 ko \| -9.37% \| +0.01% 0m00.58s \| 423880 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo \| 0m00.58s \| 423788 ko \|\| +0m00.00s \|\| 92 ko \| +0.00% \| +0.02% 0m00.58s \| 438052 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/SepLocals.vo \| 0m00.59s \| 437924 ko \|\| -0m00.01s \|\| 128 ko \| -1.69% \| +0.02% 0m00.58s \| 443992 ko \| Assembly/Equality.vo \| 0m00.60s \| 443984 ko \|\| -0m00.02s \|\| 8 ko \| -3.33% \| +0.00% 0m00.58s \| 491008 ko \| PushButtonSynthesis/ReificationCache.vo \| 0m00.62s \| 490916 ko \|\| -0m00.04s \|\| 92 ko \| -6.45% \| +0.01% 0m00.58s \| 420780 ko \| Util/CPSUtil.vo \| 0m00.58s \| 420676 ko \|\| +0m00.00s \|\| 104 ko \| +0.00% \| +0.02% 0m00.57s \| 462088 ko \| ArithmeticCPS/WordByWordMontgomery.vo \| 0m00.45s \| 462160 ko \|\| +0m00.11s \|\| -72 ko \| +26.66% \| -0.01% 0m00.57s \| 448372 ko \| Bedrock/Group/Loops.vo \| 0m00.60s \| 448336 ko \|\| -0m00.03s \|\| 36 ko \| -5.00% \| +0.00% 0m00.57s \| 436724 ko \| Util/ZRange/OperationsBounds.vo \| 0m00.54s \| 436708 ko \|\| +0m00.02s \|\| 16 ko \| +5.55% \| +0.00% 0m00.56s \| 409176 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedList.vo \| 0m00.53s \| 409052 ko \|\| +0m00.03s \|\| 124 ko \| +5.66% \| +0.03% 0m00.56s \| 437976 ko \| Util/QUtil.vo \| 0m00.50s \| 437832 ko \|\| +0m00.06s \|\| 144 ko \| +12.00% \| +0.03% 0m00.55s \| 405568 ko \| Util/OptionList.vo \| 0m00.49s \| 405680 ko \|\| +0m00.06s \|\| -112 ko \| +12.24% \| -0.02% 0m00.54s \| 438072 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ExprReflection.vo \| 0m00.59s \| 438324 ko \|\| -0m00.04s \|\| -252 ko \| -8.47% \| -0.05% 0m00.54s \| 458708 ko \| ArithmeticCPS/Freeze.vo \| 0m00.55s \| 458584 ko \|\| -0m00.01s \|\| 124 ko \| -1.81% \| +0.02% 0m00.54s \| 435628 ko \| Util/MSetN.vo \| 0m00.55s \| 435580 ko \|\| -0m00.01s \|\| 48 ko \| -1.81% \| +0.01% 0m00.53s \| 454736 ko \| MiscCompilerPasses.vo \| 0m00.55s \| 454828 ko \|\| -0m00.02s \|\| -92 ko \| -3.63% \| -0.02% 0m00.53s \| 474808 ko \| Rewriter/Util/plugins/RewriterBuild.vo \| 0m00.57s \| 474732 ko \|\| -0m00.03s \|\| 76 ko \| -7.01% \| +0.01% 0m00.53s \| 383524 ko \| Util/Structures/Orders/Sum.vo \| 0m00.62s \| 383648 ko \|\| -0m00.08s \|\| -124 ko \| -14.51% \| -0.03% 0m00.53s \| 409684 ko \| Util/ZUtil/Modulo/PullPush.vo \| 0m00.52s \| 409948 ko \|\| +0m00.01s \|\| -264 ko \| +1.92% \| -0.06% 0m00.52s \| 414220 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo \| 0m00.52s \| 414188 ko \|\| +0m00.00s \|\| 32 ko \| +0.00% \| +0.00% 0m00.52s \| 411600 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo \| 0m00.55s \| 411600 ko \|\| -0m00.03s \|\| 0 ko \| -5.45% \| +0.00% 0m00.52s \| 461360 ko \| Assembly/WithBedrock/Semantics.vo \| 0m00.43s \| 461328 ko \|\| +0m00.09s \|\| 32 ko \| +20.93% \| +0.00% 0m00.52s \| 410996 ko \| Coqprime/PrimalityTest/Zp.vo \| 0m00.55s \| 410960 ko \|\| -0m00.03s \|\| 36 ko \| -5.45% \| +0.00% 0m00.52s \| 456224 ko \| Rewriter/Language/IdentifiersGenerateProofs.vo \| 0m00.57s \| 456184 ko \|\| -0m00.04s \|\| 40 ko \| -8.77% \| +0.00% 0m00.52s \| 476428 ko \| Rewriter/Rewriter/Examples/PerfTesting/Settings.vo \| 0m00.57s \| 476096 ko \|\| -0m00.04s \|\| 332 ko \| -8.77% \| +0.06% 0m00.52s \| 474124 ko \| Rewriter/Util/plugins/RewriterBuildRegistryImports.vo \| 0m00.58s \| 474232 ko \|\| -0m00.05s \|\| -108 ko \| -10.34% \| -0.02% 0m00.52s \| 429468 ko \| Util/ZUtil/Stabilization.vo \| 0m00.45s \| 429172 ko \|\| +0m00.07s \|\| 296 ko \| +15.55% \| +0.06% 0m00.51s \| 474364 ko \| Rewriter/Util/plugins/RewriterBuildRegistry.vo \| 0m00.60s \| 474544 ko \|\| -0m00.08s \|\| -180 ko \| -14.99% \| -0.03% 0m00.50s \| 449348 ko \| ArithmeticCPS/Saturated.vo \| 0m00.55s \| 449440 ko \|\| -0m00.05s \|\| -92 ko \| -9.09% \| -0.02% 0m00.50s \| 406712 ko \| Util/Loops.vo \| 0m00.50s \| 406684 ko \|\| +0m00.00s \|\| 28 ko \| +0.00% \| +0.00% 0m00.50s \| 411996 ko \| Util/Strings/ParseArithmeticToTaps.vo \| 0m00.50s \| 412124 ko \|\| +0m00.00s \|\| -128 ko \| +0.00% \| -0.03% 0m00.50s \| 26416 ko \| fiat-json/src/curve25519_64.json \| 0m00.54s \| 26348 ko \|\| -0m00.04s \|\| 68 ko \| -7.40% \| +0.25% 0m00.49s \| 430772 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpSepLog.vo \| 0m00.44s \| 430672 ko \|\| +0m00.04s \|\| 100 ko \| +11.36% \| +0.02% 0m00.49s \| 416880 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Registers.vo \| 0m00.51s \| 416884 ko \|\| -0m00.02s \|\| -4 ko \| -3.92% \| -0.00% 0m00.49s \| 410668 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/bitblast.vo \| 0m00.48s \| 410536 ko \|\| +0m00.01s \|\| 132 ko \| +2.08% \| +0.03% 0m00.49s \| 459184 ko \| ArithmeticCPS/BaseConversion.vo \| 0m00.46s \| 459004 ko \|\| +0m00.02s \|\| 180 ko \| +6.52% \| +0.03% 0m00.49s \| 446160 ko \| Bedrock/Specs/Group.vo \| 0m00.50s \| 446240 ko \|\| -0m00.01s \|\| -80 ko \| -2.00% \| -0.01% 0m00.49s \| 426224 ko \| Util/ZUtil/CC.vo \| 0m00.46s \| 426448 ko \|\| +0m00.02s \|\| -224 ko \| +6.52% \| -0.05% 0m00.49s \| 21092 ko \| fiat-rust/src/curve25519_64.rs \| 0m00.47s \| 21072 ko \|\| +0m00.02s \|\| 20 ko \| +4.25% \| +0.09% 0m00.48s \| 408052 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/ListSet.vo \| 0m00.49s \| 408104 ko \|\| -0m00.01s \|\| -52 ko \| -2.04% \| -0.01% 0m00.48s \| 427344 ko \| Util/Strings/NamingConventions.vo \| 0m00.42s \| 427408 ko \|\| +0m00.06s \|\| -64 ko \| +14.28% \| -0.01% 0m00.48s \| 20552 ko \| fiat-c/src/curve25519_64.c \| 0m00.46s \| 20660 ko \|\| +0m00.01s \|\| -108 ko \| +4.34% \| -0.52% 0m00.47s \| 422856 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo \| 0m00.38s \| 423140 ko \|\| +0m00.08s \|\| -284 ko \| +23.68% \| -0.06% 0m00.47s \| 348756 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo \| 0m00.45s \| 348780 ko \|\| +0m00.01s \|\| -24 ko \| +4.44% \| -0.00% 0m00.47s \| 447132 ko \| ArithmeticCPS/Core.vo \| 0m00.41s \| 447176 ko \|\| +0m00.06s \|\| -44 ko \| +14.63% \| -0.00% 0m00.47s \| 21348 ko \| fiat-zig/src/curve25519_64.zig \| 0m00.49s \| 21176 ko \|\| -0m00.02s \|\| 172 ko \| -4.08% \| +0.81% 0m00.46s \| 420364 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo \| 0m00.49s \| 420420 ko \|\| -0m00.02s \|\| -56 ko \| -6.12% \| -0.01% 0m00.46s \| 424216 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo \| 0m00.41s \| 424284 ko \|\| +0m00.05s \|\| -68 ko \| +12.19% \| -0.01% 0m00.46s \| 391960 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo \| 0m00.45s \| 391760 ko \|\| +0m00.01s \|\| 200 ko \| +2.22% \| +0.05% 0m00.46s \| 417156 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo \| 0m00.44s \| 416980 ko \|\| +0m00.02s \|\| 176 ko \| +4.54% \| +0.04% 0m00.45s \| 409220 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo \| 0m00.46s \| 409216 ko \|\| -0m00.01s \|\| 4 ko \| -2.17% \| +0.00% 0m00.45s \| 404704 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/ZLib.vo \| 0m00.41s \| 404932 ko \|\| +0m00.04s \|\| -228 ko \| +9.75% \| -0.05% 0m00.45s \| 431380 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/SepReflection.vo \| 0m00.50s \| 431560 ko \|\| -0m00.04s \|\| -180 ko \| -9.99% \| -0.04% 0m00.45s \| 357920 ko \| Util/Wf.vo \| 0m00.49s \| 357596 ko \|\| -0m00.03s \|\| 324 ko \| -8.16% \| +0.09% 0m00.44s \| 420072 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo \| 0m00.39s \| 420120 ko \|\| +0m00.04s \|\| -48 ko \| +12.82% \| -0.01% 0m00.44s \| 421268 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo \| 0m00.42s \| 421108 ko \|\| +0m00.02s \|\| 160 ko \| +4.76% \| +0.03% 0m00.44s \| 427212 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo \| 0m00.41s \| 427236 ko \|\| +0m00.03s \|\| -24 ko \| +7.31% \| -0.00% 0m00.44s \| 434048 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Conditionals.vo \| 0m00.45s \| 434272 ko \|\| -0m00.01s \|\| -224 ko \| -2.22% \| -0.05% 0m00.44s \| 430244 ko \| Util/ZUtil/Lxor.vo \| 0m00.41s \| 430108 ko \|\| +0m00.03s \|\| 136 ko \| +7.31% \| +0.03% 0m00.43s \| 403152 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/PushPullMod.vo \| 0m00.46s \| 403164 ko \|\| -0m00.03s \|\| -12 ko \| -6.52% \| -0.00% 0m00.43s \| 428876 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo \| 0m00.45s \| 428820 ko \|\| -0m00.02s \|\| 56 ko \| -4.44% \| +0.01% 0m00.43s \| 416900 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo \| 0m00.46s \| 416900 ko \|\| -0m00.03s \|\| 0 ko \| -6.52% \| +0.00% 0m00.43s \| 453372 ko \| ArithmeticCPS/ModOps.vo \| 0m00.48s \| 453260 ko \|\| -0m00.04s \|\| 112 ko \| -10.41% \| +0.02% 0m00.43s \| 406496 ko \| Coqprime/Z/ZCmisc.vo \| 0m00.41s \| 406332 ko \|\| +0m00.02s \|\| 164 ko \| +4.87% \| +0.04% 0m00.43s \| 450800 ko \| Util/MSetPositive/Show.vo \| 0m00.44s \| 450764 ko \|\| -0m00.01s \|\| 36 ko \| -2.27% \| +0.00% 0m00.42s \| 428128 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo \| 0m00.41s \| 428216 ko \|\| +0m00.01s \|\| -88 ko \| +2.43% \| -0.02% 0m00.42s \| 414424 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/ZifyLittleEndian.vo \| 0m00.48s \| 414144 ko \|\| -0m00.06s \|\| 280 ko \| -12.50% \| +0.06% 0m00.42s \| 433156 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Alloc.vo \| 0m00.39s \| 433276 ko \|\| +0m00.02s \|\| -120 ko \| +7.69% \| -0.02% 0m00.42s \| 408872 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/ToCString.vo \| 0m00.43s \| 409040 ko \|\| -0m00.01s \|\| -168 ko \| -2.32% \| -0.04% 0m00.42s \| 382764 ko \| Coqprime/List/Permutation.vo \| 0m00.29s \| 382748 ko \|\| +0m00.13s \|\| 16 ko \| +44.82% \| +0.00% 0m00.42s \| 423340 ko \| Util/Decidable/Decidable2Bool.vo \| 0m00.46s \| 423356 ko \|\| -0m00.04s \|\| -16 ko \| -8.69% \| -0.00% 0m00.42s \| 424304 ko \| Util/ZBounded.vo \| 0m00.37s \| 424136 ko \|\| +0m00.04s \|\| 168 ko \| +13.51% \| +0.03% 0m00.41s \| 432396 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo \| 0m00.41s \| 432512 ko \|\| +0m00.00s \|\| -116 ko \| +0.00% \| -0.02% 0m00.41s \| 418372 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfListWord.vo \| 0m00.42s \| 418292 ko \|\| -0m00.01s \|\| 80 ko \| -2.38% \| +0.01% 0m00.41s \| 383120 ko \| Coqprime/List/UList.vo \| 0m00.35s \| 383160 ko \|\| +0m00.06s \|\| -40 ko \| +17.14% \| -0.01% 0m00.41s \| 430980 ko \| Rewriter/Language/IdentifiersBasicGenerate.vo \| 0m00.47s \| 430888 ko \|\| -0m00.06s \|\| 92 ko \| -12.76% \| +0.02% 0m00.40s \| 439012 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo \| 0m00.44s \| 439100 ko \|\| -0m00.03s \|\| -88 ko \| -9.09% \| -0.02% 0m00.40s \| 369932 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo \| 0m00.37s \| 369840 ko \|\| +0m00.03s \|\| 92 ko \| +8.10% \| +0.02% 0m00.40s \| 362004 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Api.vo \| 0m00.35s \| 361984 ko \|\| +0m00.05s \|\| 20 ko \| +14.28% \| +0.00% 0m00.40s \| 423492 ko \| Util/ZRange.vo \| 0m00.37s \| 423484 ko \|\| +0m00.03s \|\| 8 ko \| +8.10% \| +0.00% 0m00.39s \| 456708 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo \| 0m00.36s \| 456620 ko \|\| +0m00.03s \|\| 88 ko \| +8.33% \| +0.01% 0m00.39s \| 424008 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo \| 0m00.42s \| 424228 ko \|\| -0m00.02s \|\| -220 ko \| -7.14% \| -0.05% 0m00.39s \| 415816 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Monads.vo \| 0m00.38s \| 415876 ko \|\| +0m00.01s \|\| -60 ko \| +2.63% \| -0.01% 0m00.39s \| 421216 ko \| Util/Level.vo \| 0m00.41s \| 420912 ko \|\| -0m00.01s \|\| 304 ko \| -4.87% \| +0.07% 0m00.39s \| 381816 ko \| Util/Sum.vo \| 0m00.40s \| 381756 ko \|\| -0m00.01s \|\| 60 ko \| -2.50% \| +0.01% 0m00.39s \| 422708 ko \| Util/ZUtil/Log2.vo \| 0m00.36s \| 422484 ko \|\| +0m00.03s \|\| 224 ko \| +8.33% \| +0.05% 0m00.39s \| 431344 ko \| Util/ZUtil/SignBit.vo \| 0m00.32s \| 431308 ko \|\| +0m00.07s \|\| 36 ko \| +21.87% \| +0.00% 0m00.38s \| 424640 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo \| 0m00.34s \| 424512 ko \|\| +0m00.03s \|\| 128 ko \| +11.76% \| +0.03% 0m00.38s \| 332932 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo \| 0m00.31s \| 332924 ko \|\| +0m00.07s \|\| 8 ko \| +22.58% \| +0.00% 0m00.38s \| 413340 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/OfFunc.vo \| 0m00.31s \| 413356 ko \|\| +0m00.07s \|\| -16 ko \| +22.58% \| -0.00% 0m00.38s \| 418784 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo \| 0m00.39s \| 418792 ko \|\| -0m00.01s \|\| -8 ko \| -2.56% \| -0.00% 0m00.38s \| 466992 ko \| Arithmetic/FLia.vo \| 0m00.40s \| 467088 ko \|\| -0m00.02s \|\| -96 ko \| -5.00% \| -0.02% 0m00.38s \| 385608 ko \| Language/PreExtra.vo \| 0m00.37s \| 385636 ko \|\| +0m00.01s \|\| -28 ko \| +2.70% \| -0.00% 0m00.38s \| 391756 ko \| Util/Strings/String_as_OT_old.vo \| 0m00.35s \| 391684 ko \|\| +0m00.03s \|\| 72 ko \| +8.57% \| +0.01% 0m00.37s \| 421268 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo \| 0m00.36s \| 421276 ko \|\| +0m00.01s \|\| -8 ko \| +2.77% \| -0.00% 0m00.37s \| 369300 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo \| 0m00.34s \| 369284 ko \|\| +0m00.02s \|\| 16 ko \| +8.82% \| +0.00% 0m00.37s \| 407020 ko \| Coqprime/PrimalityTest/Euler.vo \| 0m00.33s \| 407004 ko \|\| +0m00.03s \|\| 16 ko \| +12.12% \| +0.00% 0m00.37s \| 395020 ko \| Rewriter/TestRules.vo \| 0m00.36s \| 395048 ko \|\| +0m00.01s \|\| -28 ko \| +2.77% \| -0.00% 0m00.37s \| 419336 ko \| Util/HList.vo \| 0m00.39s \| 419408 ko \|\| -0m00.02s \|\| -72 ko \| -5.12% \| -0.01% 0m00.37s \| 408408 ko \| Util/ListUtil/GroupAllBy.vo \| 0m00.38s \| 408340 ko \|\| -0m00.01s \|\| 68 ko \| -2.63% \| +0.01% 0m00.37s \| 426752 ko \| Util/Strings/Show.vo \| 0m00.36s \| 426944 ko \|\| +0m00.01s \|\| -192 ko \| +2.77% \| -0.04% 0m00.37s \| 424660 ko \| Util/ZUtil/Divide.vo \| 0m00.30s \| 424500 ko \|\| +0m00.07s \|\| 160 ko \| +23.33% \| +0.03% 0m00.36s \| 361760 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo \| 0m00.34s \| 361660 ko \|\| +0m00.01s \|\| 100 ko \| +5.88% \| +0.02% 0m00.36s \| 403888 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo \| 0m00.36s \| 404044 ko \|\| +0m00.00s \|\| -156 ko \| +0.00% \| -0.03% 0m00.36s \| 372260 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Notations.vo \| 0m00.38s \| 372224 ko \|\| -0m00.02s \|\| 36 ko \| -5.26% \| +0.00% 0m00.36s \| 357752 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Tactics.vo \| 0m00.37s \| 357820 ko \|\| -0m00.01s \|\| -68 ko \| -2.70% \| -0.01% 0m00.36s \| 428728 ko \| Arithmetic/ModularArithmeticPre.vo \| 0m00.44s \| 428636 ko \|\| -0m00.08s \|\| 92 ko \| -18.18% \| +0.02% 0m00.36s \| 406384 ko \| Coqprime/PrimalityTest/IGroup.vo \| 0m00.29s \| 406392 ko \|\| +0m00.07s \|\| -8 ko \| +24.13% \| -0.00% 0m00.36s \| 328316 ko \| Spec/ModularArithmetic.vo \| 0m00.34s \| 328220 ko \|\| +0m00.01s \|\| 96 ko \| +5.88% \| +0.02% 0m00.36s \| 407536 ko \| Util/Strings/String.vo \| 0m00.35s \| 407384 ko \|\| +0m00.01s \|\| 152 ko \| +2.85% \| +0.03% 0m00.35s \| 410868 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Naive.vo \| 0m00.34s \| 410824 ko \|\| +0m00.00s \|\| 44 ko \| +2.94% \| +0.01% 0m00.35s \| 414716 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/prove_Zeq_bitwise.vo \| 0m00.37s \| 414608 ko \|\| -0m00.02s \|\| 108 ko \| -5.40% \| +0.02% 0m00.35s \| 421676 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo \| 0m00.36s \| 421712 ko \|\| -0m00.01s \|\| -36 ko \| -2.77% \| -0.00% 0m00.35s \| 405456 ko \| Coqprime/PrimalityTest/Lagrange.vo \| 0m00.32s \| 405488 ko \|\| +0m00.02s \|\| -32 ko \| +9.37% \| -0.00% 0m00.35s \| 381380 ko \| Rewriter/Util/Sum.vo \| 0m00.41s \| 381464 ko \|\| -0m00.06s \|\| -84 ko \| -14.63% \| -0.02% 0m00.35s \| 408612 ko \| Util/ZUtil/CPS.vo \| 0m00.32s \| 408548 ko \|\| +0m00.02s \|\| 64 ko \| +9.37% \| +0.01% 0m00.34s \| 336752 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo \| 0m00.32s \| 336924 ko \|\| +0m00.02s \|\| -172 ko \| +6.25% \| -0.05% 0m00.34s \| 422484 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepAddrLast.vo \| 0m00.39s \| 422368 ko \|\| -0m00.04s \|\| 116 ko \| -12.82% \| +0.02% 0m00.34s \| 418324 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo \| 0m00.34s \| 418356 ko \|\| +0m00.00s \|\| -32 ko \| +0.00% \| -0.00% 0m00.34s \| 422752 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo \| 0m00.37s \| 422672 ko \|\| -0m00.02s \|\| 80 ko \| -8.10% \| +0.01% 0m00.34s \| 371456 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Invariants.vo \| 0m00.40s \| 371344 ko \|\| -0m00.06s \|\| 112 ko \| -15.00% \| +0.03% 0m00.34s \| 350432 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/WordNotations.vo \| 0m00.38s \| 350644 ko \|\| -0m00.03s \|\| -212 ko \| -10.52% \| -0.06% 0m00.34s \| 426732 ko \| Util/ZUtil/Land.vo \| 0m00.40s \| 426652 ko \|\| -0m00.06s \|\| 80 ko \| -15.00% \| +0.01% 0m00.34s \| 414436 ko \| Util/ZUtil/Ltz.vo \| 0m00.34s \| 414276 ko \|\| +0m00.00s \|\| 160 ko \| +0.00% \| +0.03% 0m00.34s \| 347504 ko \| Util/ZUtil/Tactics/SolveRange.vo \| 0m00.36s \| 347432 ko \|\| -0m00.01s \|\| 72 ko \| -5.55% \| +0.02% 0m00.33s \| 383304 ko \| Algebra/Monoid.vo \| 0m00.25s \| 383316 ko \|\| +0m00.08s \|\| -12 ko \| +32.00% \| -0.00% 0m00.33s \| 356872 ko \| Rewriter/TestRulesProofs.vo \| 0m00.29s \| 356760 ko \|\| +0m00.04s \|\| 112 ko \| +13.79% \| +0.03% 0m00.33s \| 411692 ko \| Rewriter/Util/Strings/ParseArithmetic.vo \| 0m00.34s \| 411408 ko \|\| -0m00.01s \|\| 284 ko \| -2.94% \| +0.06% 0m00.33s \| 372104 ko \| Util/MSetPositive/Facts.vo \| 0m00.34s \| 372016 ko \|\| -0m00.01s \|\| 88 ko \| -2.94% \| +0.02% 0m00.33s \| 361108 ko \| Util/ZUtil.vo \| 0m00.32s \| 360904 ko \|\| +0m00.01s \|\| 204 ko \| +3.12% \| +0.05% 0m00.33s \| 349500 ko \| Util/ZUtil/Lor.vo \| 0m00.31s \| 349528 ko \|\| +0m00.02s \|\| -28 ko \| +6.45% \| -0.00% 0m00.33s \| 25688 ko \| fiat-bedrock2/src/poly1305_32.c \| 0m00.35s \| 25740 ko \|\| -0m00.01s \|\| -52 ko \| -5.71% \| -0.20% 0m00.32s \| 419424 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Result.vo \| 0m00.37s \| 419212 ko \|\| -0m00.04s \|\| 212 ko \| -13.51% \| +0.05% 0m00.32s \| 342200 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo \| 0m00.31s \| 342276 ko \|\| +0m00.01s \|\| -76 ko \| +3.22% \| -0.02% 0m00.32s \| 396020 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo \| 0m00.32s \| 396032 ko \|\| +0m00.00s \|\| -12 ko \| +0.00% \| -0.00% 0m00.32s \| 351936 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo \| 0m00.37s \| 351784 ko \|\| -0m00.04s \|\| 152 ko \| -13.51% \| +0.04% 0m00.32s \| 400308 ko \| Language/IdentifierParameters.vo \| 0m00.36s \| 400204 ko \|\| -0m00.03s \|\| 104 ko \| -11.11% \| +0.02% 0m00.32s \| 420332 ko \| Spec/CompleteEdwardsCurve.vo \| 0m00.35s \| 420620 ko \|\| -0m00.02s \|\| -288 ko \| -8.57% \| -0.06% 0m00.32s \| 372900 ko \| Util/Strings/Sorting.vo \| 0m00.34s \| 372752 ko \|\| -0m00.02s \|\| 148 ko \| -5.88% \| +0.03% 0m00.32s \| 396876 ko \| Util/ZUtil/EquivModulo.vo \| 0m00.28s \| 396632 ko \|\| +0m00.03s \|\| 244 ko \| +14.28% \| +0.06% 0m00.31s \| 344624 ko \| Util/ZUtil/Tactics/SolveTestbit.vo \| 0m00.30s \| 344556 ko \|\| +0m00.01s \|\| 68 ko \| +3.33% \| +0.01% 0m00.31s \| 339284 ko \| Util/ZUtil/Tactics/Ztestbit.vo \| 0m00.33s \| 339428 ko \|\| -0m00.02s \|\| -144 ko \| -6.06% \| -0.04% 0m00.30s \| 370112 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo \| 0m00.29s \| 370192 ko \|\| +0m00.01s \|\| -80 ko \| +3.44% \| -0.02% 0m00.30s \| 385232 ko \| Util/Listable.vo \| 0m00.29s \| 384972 ko \|\| +0m00.01s \|\| 260 ko \| +3.44% \| +0.06% 0m00.29s \| 409480 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/MapKeys.vo \| 0m00.26s \| 409688 ko \|\| +0m00.02s \|\| -208 ko \| +11.53% \| -0.05% 0m00.29s \| 307692 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SoftmulInsts.vo \| 0m00.23s \| 307808 ko \|\| +0m00.05s \|\| -116 ko \| +26.08% \| -0.03% 0m00.29s \| 295312 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo \| 0m00.26s \| 295328 ko \|\| +0m00.02s \|\| -16 ko \| +11.53% \| -0.00% 0m00.29s \| 386504 ko \| Rewriter/Language/UnderLets.vo \| 0m00.31s \| 386620 ko \|\| -0m00.02s \|\| -116 ko \| -6.45% \| -0.03% 0m00.29s \| 20044 ko \| fiat-go/32/poly1305/poly1305.go \| 0m00.29s \| 20064 ko \|\| +0m00.00s \|\| -20 ko \| +0.00% \| -0.09% 0m00.28s \| 389420 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo \| 0m00.31s \| 389520 ko \|\| -0m00.02s \|\| -100 ko \| -9.67% \| -0.02% 0m00.28s \| 347416 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo \| 0m00.29s \| 347348 ko \|\| -0m00.00s \|\| 68 ko \| -3.44% \| +0.01% 0m00.28s \| 382464 ko \| Coqprime/List/ListAux.vo \| 0m00.31s \| 382316 ko \|\| -0m00.02s \|\| 148 ko \| -9.67% \| +0.03% 0m00.28s \| 313772 ko \| Rewriter/Util/Option.vo \| 0m00.24s \| 313520 ko \|\| +0m00.04s \|\| 252 ko \| +16.66% \| +0.08% 0m00.28s \| 316424 ko \| Util/MSets/Show.vo \| 0m00.26s \| 316360 ko \|\| +0m00.02s \|\| 64 ko \| +7.69% \| +0.02% 0m00.28s \| 357032 ko \| Util/ZRange/Operations.vo \| 0m00.30s \| 357204 ko \|\| -0m00.01s \|\| -172 ko \| -6.66% \| -0.04% 0m00.27s \| 292976 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo \| 0m00.24s \| 292988 ko \|\| +0m00.03s \|\| -12 ko \| +12.50% \| -0.00% 0m00.27s \| 393900 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo \| 0m00.31s \| 394020 ko \|\| -0m00.03s \|\| -120 ko \| -12.90% \| -0.03% 0m00.27s \| 372980 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo \| 0m00.25s \| 372948 ko \|\| +0m00.02s \|\| 32 ko \| +8.00% \| +0.00% 0m00.27s \| 383152 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo \| 0m00.26s \| 383068 ko \|\| +0m00.01s \|\| 84 ko \| +3.84% \| +0.02% 0m00.27s \| 304624 ko \| Rewriter/Language/PreLemmas.vo \| 0m00.18s \| 304832 ko \|\| +0m00.09s \|\| -208 ko \| +50.00% \| -0.06% 0m00.27s \| 344780 ko \| Rewriter/Util/ListUtil/SetoidList.vo \| 0m00.25s \| 345040 ko \|\| +0m00.02s \|\| -260 ko \| +8.00% \| -0.07% 0m00.27s \| 373228 ko \| Util/ZUtil/Pow.vo \| 0m00.30s \| 372856 ko \|\| -0m00.02s \|\| 372 ko \| -9.99% \| +0.09% 0m00.27s \| 316008 ko \| Util/ZUtil/Tactics/SimplifyFractionsLe.vo \| 0m00.23s \| 315672 ko \|\| +0m00.04s \|\| 336 ko \| +17.39% \| +0.10% 0m00.27s \| 24392 ko \| fiat-json/src/poly1305_32.json \| 0m00.25s \| 24324 ko \|\| +0m00.02s \|\| 68 ko \| +8.00% \| +0.27% 0m00.26s \| 338412 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo \| 0m00.24s \| 338284 ko \|\| +0m00.02s \|\| 128 ko \| +8.33% \| +0.03% 0m00.26s \| 317716 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo \| 0m00.20s \| 317796 ko \|\| +0m00.06s \|\| -80 ko \| +30.00% \| -0.02% 0m00.26s \| 325272 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/mod4_0.vo \| 0m00.24s \| 325344 ko \|\| +0m00.02s \|\| -72 ko \| +8.33% \| -0.02% 0m00.26s \| 326132 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/DebugWordEq.vo \| 0m00.22s \| 326176 ko \|\| +0m00.04s \|\| -44 ko \| +18.18% \| -0.01% 0m00.26s \| 304752 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo \| 0m00.24s \| 304724 ko \|\| +0m00.02s \|\| 28 ko \| +8.33% \| +0.00% 0m00.26s \| 373200 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo \| 0m00.33s \| 373172 ko \|\| -0m00.07s \|\| 28 ko \| -21.21% \| +0.00% 0m00.26s \| 336392 ko \| Util/MSetPositive/Equality.vo \| 0m00.30s \| 336512 ko \|\| -0m00.03s \|\| -120 ko \| -13.33% \| -0.03% 0m00.26s \| 347052 ko \| Util/ZUtil/Le.vo \| 0m00.24s \| 346648 ko \|\| +0m00.02s \|\| 404 ko \| +8.33% \| +0.11% 0m00.26s \| 313780 ko \| Util/ZUtil/Tactics.vo \| 0m00.26s \| 313792 ko \|\| +0m00.00s \|\| -12 ko \| +0.00% \| -0.00% 0m00.26s \| 310200 ko \| Util/ZUtil/Tactics/RewriteModSmall.vo \| 0m00.20s \| 309692 ko \|\| +0m00.06s \|\| 508 ko \| +30.00% \| +0.16% 0m00.26s \| 275948 ko \| Util/ZUtil/Zselect.vo \| 0m00.23s \| 275724 ko \|\| +0m00.03s \|\| 224 ko \| +13.04% \| +0.08% 0m00.25s \| 324208 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo \| 0m00.23s \| 324212 ko \|\| +0m00.01s \|\| -4 ko \| +8.69% \| -0.00% 0m00.25s \| 308200 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo \| 0m00.25s \| 308128 ko \|\| +0m00.00s \|\| 72 ko \| +0.00% \| +0.02% 0m00.25s \| 291844 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/div10.vo \| 0m00.17s \| 291932 ko \|\| +0m00.07s \|\| -88 ko \| +47.05% \| -0.03% 0m00.25s \| 312432 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo \| 0m00.21s \| 312444 ko \|\| +0m00.04s \|\| -12 ko \| +19.04% \| -0.00% 0m00.25s \| 377264 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/SimplWordExpr.vo \| 0m00.34s \| 377388 ko \|\| -0m00.09s \|\| -124 ko \| -26.47% \| -0.03% 0m00.25s \| 292048 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl32.vo \| 0m00.26s \| 292244 ko \|\| -0m00.01s \|\| -196 ko \| -3.84% \| -0.06% 0m00.25s \| 375792 ko \| Coqprime/List/ZProgression.vo \| 0m00.22s \| 376084 ko \|\| +0m00.03s \|\| -292 ko \| +13.63% \| -0.07% 0m00.25s \| 421664 ko \| Curves/Weierstrass/Affine.vo \| 0m00.33s \| 421668 ko \|\| -0m00.08s \|\| -4 ko \| -24.24% \| -0.00% 0m00.25s \| 303336 ko \| Util/FMapPositive/Equality.vo \| 0m00.19s \| 303244 ko \|\| +0m00.06s \|\| 92 ko \| +31.57% \| +0.03% 0m00.25s \| 313780 ko \| Util/Option.vo \| 0m00.25s \| 313856 ko \|\| +0m00.00s \|\| -76 ko \| +0.00% \| -0.02% 0m00.25s \| 313616 ko \| Util/ZUtil/Tactics/ZeroBounds.vo \| 0m00.27s \| 313416 ko \|\| -0m00.02s \|\| 200 ko \| -7.40% \| +0.06% 0m00.25s \| 300520 ko \| Util/ZUtil/ZSimplify/Simple.vo \| 0m00.25s \| 300568 ko \|\| +0m00.00s \|\| -48 ko \| +0.00% \| -0.01% 0m00.24s \| 388148 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.vo \| 0m00.27s \| 388212 ko \|\| -0m00.03s \|\| -64 ko \| -11.11% \| -0.01% 0m00.24s \| 284544 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Z_keyed_SortedListMap.vo \| 0m00.18s \| 284644 ko \|\| +0m00.06s \|\| -100 ko \| +33.33% \| -0.03% 0m00.24s \| 276732 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_word_hints.vo \| 0m00.20s \| 276532 ko \|\| +0m00.03s \|\| 200 ko \| +19.99% \| +0.07% 0m00.24s \| 332528 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo \| 0m00.24s \| 332488 ko \|\| +0m00.00s \|\| 40 ko \| +0.00% \| +0.01% 0m00.24s \| 297532 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo \| 0m00.22s \| 297348 ko \|\| +0m00.01s \|\| 184 ko \| +9.09% \| +0.06% 0m00.24s \| 272768 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo \| 0m00.24s \| 272968 ko \|\| +0m00.00s \|\| -200 ko \| +0.00% \| -0.07% 0m00.24s \| 374544 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo \| 0m00.27s \| 374612 ko \|\| -0m00.03s \|\| -68 ko \| -11.11% \| -0.01% 0m00.24s \| 311396 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo \| 0m00.18s \| 311336 ko \|\| +0m00.06s \|\| 60 ko \| +33.33% \| +0.01% 0m00.24s \| 383160 ko \| Coqprime/List/Iterator.vo \| 0m00.29s \| 383256 ko \|\| -0m00.04s \|\| -96 ko \| -17.24% \| -0.02% 0m00.24s \| 367200 ko \| Rewriter/Util/Strings/String.vo \| 0m00.23s \| 367300 ko \|\| +0m00.00s \|\| -100 ko \| +4.34% \| -0.02% 0m00.24s \| 353320 ko \| Util/AdditionChainExponentiation.vo \| 0m00.25s \| 353316 ko \|\| -0m00.01s \|\| 4 ko \| -4.00% \| +0.00% 0m00.24s \| 315500 ko \| Util/ErrorT/Show.vo \| 0m00.21s \| 315128 ko \|\| +0m00.03s \|\| 372 ko \| +14.28% \| +0.11% 0m00.24s \| 333000 ko \| Util/ListUtil/Permutation.vo \| 0m00.24s \| 332960 ko \|\| +0m00.00s \|\| 40 ko \| +0.00% \| +0.01% 0m00.24s \| 281288 ko \| Util/Strings/Parse/Common.vo \| 0m00.23s \| 281300 ko \|\| +0m00.00s \|\| -12 ko \| +4.34% \| -0.00% 0m00.24s \| 340472 ko \| Util/ZUtil/Combine.vo \| 0m00.28s \| 340032 ko \|\| -0m00.04s \|\| 440 ko \| -14.28% \| +0.12% 0m00.24s \| 294448 ko \| Util/ZUtil/Tactics/LinearSubstitute.vo \| 0m00.26s \| 294236 ko \|\| -0m00.02s \|\| 212 ko \| -7.69% \| +0.07% 0m00.23s \| 346904 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo \| 0m00.29s \| 346940 ko \|\| -0m00.05s \|\| -36 ko \| -20.68% \| -0.01% 0m00.23s \| 295252 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Common.vo \| 0m00.18s \| 295456 ko \|\| +0m00.05s \|\| -204 ko \| +27.77% \| -0.06% 0m00.23s \| 251236 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Empty_set_keyed_map.vo \| 0m00.17s \| 251352 ko \|\| +0m00.06s \|\| -116 ko \| +35.29% \| -0.04% 0m00.23s \| 258436 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth32.vo \| 0m00.17s \| 258060 ko \|\| +0m00.06s \|\| 376 ko \| +35.29% \| +0.14% 0m00.23s \| 284960 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicRiscvMachine.vo \| 0m00.22s \| 284968 ko \|\| +0m00.01s \|\| -8 ko \| +4.54% \| -0.00% 0m00.23s \| 336644 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo \| 0m00.22s \| 336580 ko \|\| +0m00.01s \|\| 64 ko \| +4.54% \| +0.01% 0m00.23s \| 329944 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo \| 0m00.28s \| 330048 ko \|\| -0m00.05s \|\| -104 ko \| -17.85% \| -0.03% 0m00.23s \| 285500 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo \| 0m00.19s \| 285476 ko \|\| +0m00.04s \|\| 24 ko \| +21.05% \| +0.00% 0m00.23s \| 298016 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo \| 0m00.21s \| 298108 ko \|\| +0m00.02s \|\| -92 ko \| +9.52% \| -0.03% 0m00.23s \| 321248 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo \| 0m00.19s \| 321108 ko \|\| +0m00.04s \|\| 140 ko \| +21.05% \| +0.04% 0m00.23s \| 298768 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MkMachineWidth.vo \| 0m00.19s \| 298616 ko \|\| +0m00.04s \|\| 152 ko \| +21.05% \| +0.05% 0m00.23s \| 259964 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words32Naive.vo \| 0m00.17s \| 259776 ko \|\| +0m00.06s \|\| 188 ko \| +35.29% \| +0.07% 0m00.23s \| 312020 ko \| Algebra/Nsatz.vo \| 0m00.29s \| 312152 ko \|\| -0m00.05s \|\| -132 ko \| -20.68% \| -0.04% 0m00.23s \| 363992 ko \| Curves/Montgomery/XZ.vo \| 0m00.25s \| 363764 ko \|\| -0m00.01s \|\| 228 ko \| -7.99% \| +0.06% 0m00.23s \| 336044 ko \| Rewriter/Util/MSetPositive/Equality.vo \| 0m00.26s \| 336120 ko \|\| -0m00.03s \|\| -76 ko \| -11.53% \| -0.02% 0m00.23s \| 371696 ko \| Rewriter/Util/MSetPositive/Facts.vo \| 0m00.31s \| 371492 ko \|\| -0m00.07s \|\| 204 ko \| -25.80% \| +0.05% 0m00.23s \| 283912 ko \| Util/ListUtil/Filter.vo \| 0m00.22s \| 283520 ko \|\| +0m00.01s \|\| 392 ko \| +4.54% \| +0.13% 0m00.23s \| 289200 ko \| Util/SideConditions/ModInvPackage.vo \| 0m00.22s \| 289368 ko \|\| +0m00.01s \|\| -168 ko \| +4.54% \| -0.05% 0m00.23s \| 284720 ko \| Util/ZUtil/Definitions.vo \| 0m00.20s \| 284820 ko \|\| +0m00.03s \|\| -100 ko \| +15.00% \| -0.03% 0m00.23s \| 261748 ko \| Util/ZUtil/Lnot.vo \| 0m00.17s \| 261792 ko \|\| +0m00.06s \|\| -44 ko \| +35.29% \| -0.01% 0m00.23s \| 269560 ko \| Util/ZUtil/Sorting.vo \| 0m00.22s \| 269880 ko \|\| +0m00.01s \|\| -320 ko \| +4.54% \| -0.11% 0m00.23s \| 328608 ko \| Util/ZUtil/Tactics/LtbToLt.vo \| 0m00.18s \| 328320 ko \|\| +0m00.05s \|\| 288 ko \| +27.77% \| +0.08% 0m00.23s \| 263928 ko \| Util/ZUtil/Tactics/PullPush/Modulo.vo \| 0m00.20s \| 263920 ko \|\| +0m00.03s \|\| 8 ko \| +15.00% \| +0.00% 0m00.23s \| 304216 ko \| Util/ZUtil/Z2Nat.vo \| 0m00.19s \| 304444 ko \|\| +0m00.04s \|\| -228 ko \| +21.05% \| -0.07% 0m00.23s \| 20468 ko \| fiat-java/src/FiatPoly1305.java \| 0m00.24s \| 20560 ko \|\| -0m00.00s \|\| -92 ko \| -4.16% \| -0.44% 0m00.23s \| 19968 ko \| fiat-rust/src/poly1305_32.rs \| 0m00.21s \| 19896 ko \|\| +0m00.02s \|\| 72 ko \| +9.52% \| +0.36% 0m00.22s \| 322676 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo \| 0m00.24s \| 322580 ko \|\| -0m00.01s \|\| 96 ko \| -8.33% \| +0.02% 0m00.22s \| 278888 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo \| 0m00.21s \| 278664 ko \|\| +0m00.01s \|\| 224 ko \| +4.76% \| +0.08% 0m00.22s \| 281548 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo \| 0m00.25s \| 281680 ko \|\| -0m00.03s \|\| -132 ko \| -12.00% \| -0.04% 0m00.22s \| 245116 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_map_hints.vo \| 0m00.19s \| 245060 ko \|\| +0m00.03s \|\| 56 ko \| +15.78% \| +0.02% 0m00.22s \| 293236 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSR.vo \| 0m00.22s \| 293100 ko \|\| +0m00.00s \|\| 136 ko \| +0.00% \| +0.04% 0m00.22s \| 276252 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo \| 0m00.18s \| 276360 ko \|\| +0m00.04s \|\| -108 ko \| +22.22% \| -0.03% 0m00.22s \| 292584 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl64.vo \| 0m00.19s \| 292828 ko \|\| +0m00.03s \|\| -244 ko \| +15.78% \| -0.08% 0m00.22s \| 255272 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionCoercions.vo \| 0m00.20s \| 255188 ko \|\| +0m00.01s \|\| 84 ko \| +9.99% \| +0.03% 0m00.22s \| 285512 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionNotations.vo \| 0m00.21s \| 285572 ko \|\| +0m00.01s \|\| -60 ko \| +4.76% \| -0.02% 0m00.22s \| 323292 ko \| Arithmetic/MontgomeryReduction/Definition.vo \| 0m00.26s \| 323272 ko \|\| -0m00.04s \|\| 20 ko \| -15.38% \| +0.00% 0m00.22s \| 267500 ko \| Rewriter/Util/Strings/Parse/Common.vo \| 0m00.17s \| 267708 ko \|\| +0m00.04s \|\| -208 ko \| +29.41% \| -0.07% 0m00.22s \| 345472 ko \| Util/ListUtil/SetoidList.vo \| 0m00.22s \| 345392 ko \|\| +0m00.00s \|\| 80 ko \| +0.00% \| +0.02% 0m00.22s \| 291560 ko \| Util/NUtil/Testbit.vo \| 0m00.22s \| 291292 ko \|\| +0m00.00s \|\| 268 ko \| +0.00% \| +0.09% 0m00.22s \| 337700 ko \| Util/NUtil/WithoutReferenceToZ.vo \| 0m00.22s \| 337716 ko \|\| +0m00.00s \|\| -16 ko \| +0.00% \| -0.00% 0m00.22s \| 261128 ko \| Util/ZUtil/Div/Bootstrap.vo \| 0m00.19s \| 261040 ko \|\| +0m00.03s \|\| 88 ko \| +15.78% \| +0.03% 0m00.22s \| 259044 ko \| Util/ZUtil/Hints/Ztestbit.vo \| 0m00.22s \| 259148 ko \|\| +0m00.00s \|\| -104 ko \| +0.00% \| -0.04% 0m00.22s \| 295480 ko \| Util/ZUtil/Nat2Z.vo \| 0m00.22s \| 295584 ko \|\| +0m00.00s \|\| -104 ko \| +0.00% \| -0.03% 0m00.22s \| 279800 ko \| Util/ZUtil/Opp.vo \| 0m00.21s \| 279228 ko \|\| +0m00.01s \|\| 572 ko \| +4.76% \| +0.20% 0m00.22s \| 278420 ko \| Util/ZUtil/Pow2.vo \| 0m00.16s \| 278400 ko \|\| +0m00.06s \|\| 20 ko \| +37.50% \| +0.00% 0m00.22s \| 20148 ko \| fiat-zig/src/poly1305_32.zig \| 0m00.22s \| 19928 ko \|\| +0m00.00s \|\| 220 ko \| +0.00% \| +1.10% 0m00.21s \| 272084 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/groundcbv.vo \| 0m00.23s \| 272436 ko \|\| -0m00.02s \|\| -352 ko \| -8.69% \| -0.12% 0m00.21s \| 262404 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd.vo \| 0m00.20s \| 262344 ko \|\| +0m00.00s \|\| 60 ko \| +4.99% \| +0.02% 0m00.21s \| 277200 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/PseudoInstructions.vo \| 0m00.19s \| 277236 ko \|\| +0m00.01s \|\| -36 ko \| +10.52% \| -0.01% 0m00.21s \| 267392 ko \| Algebra/NsatzTactic.vo \| 0m00.14s \| 267176 ko \|\| +0m00.06s \|\| 216 ko \| +49.99% \| +0.08% 0m00.21s \| 261864 ko \| PushButtonSynthesis/InvertHighLow.vo \| 0m00.19s \| 262040 ko \|\| +0m00.01s \|\| -176 ko \| +10.52% \| -0.06% 0m00.21s \| 312480 ko \| Util/IdfunWithAlt.vo \| 0m00.25s \| 312612 ko \|\| -0m00.04s \|\| -132 ko \| -16.00% \| -0.04% 0m00.21s \| 313724 ko \| Util/ZRange/Show.vo \| 0m00.21s \| 313932 ko \|\| +0m00.00s \|\| -208 ko \| +0.00% \| -0.06% 0m00.21s \| 261100 ko \| Util/ZUtil/Hints/ZArith.vo \| 0m00.19s \| 261068 ko \|\| +0m00.01s \|\| 32 ko \| +10.52% \| +0.01% 0m00.21s \| 266968 ko \| Util/ZUtil/ModExp.vo \| 0m00.21s \| 266988 ko \|\| +0m00.00s \|\| -20 ko \| +0.00% \| -0.00% 0m00.21s \| 259488 ko \| Util/ZUtil/Mul.vo \| 0m00.14s \| 259488 ko \|\| +0m00.06s \|\| 0 ko \| +49.99% \| +0.00% 0m00.21s \| 288044 ko \| Util/ZUtil/N2Z.vo \| 0m00.16s \| 288136 ko \|\| +0m00.04s \|\| -92 ko \| +31.24% \| -0.03% 0m00.21s \| 276692 ko \| Util/ZUtil/Sgn.vo \| 0m00.20s \| 277032 ko \|\| +0m00.00s \|\| -340 ko \| +4.99% \| -0.12% 0m00.21s \| 19952 ko \| fiat-c/src/poly1305_32.c \| 0m00.23s \| 19880 ko \|\| -0m00.02s \|\| 72 ko \| -8.69% \| +0.36% 0m00.20s \| 282632 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo \| 0m00.20s \| 282436 ko \|\| +0m00.00s \|\| 196 ko \| +0.00% \| +0.06% 0m00.20s \| 271736 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString_test.vo \| 0m00.17s \| 271656 ko \|\| +0m00.03s \|\| 80 ko \| +17.64% \| +0.02% 0m00.20s \| 259488 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Simp.vo \| 0m00.23s \| 259512 ko \|\| -0m00.03s \|\| -24 ko \| -13.04% \| -0.00% 0m00.20s \| 258416 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/rewr.vo \| 0m00.20s \| 258540 ko \|\| +0m00.00s \|\| -124 ko \| +0.00% \| -0.04% 0m00.20s \| 307552 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Interface.vo \| 0m00.20s \| 307820 ko \|\| +0m00.00s \|\| -268 ko \| +0.00% \| -0.08% 0m00.20s \| 267280 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRField.vo \| 0m00.18s \| 267304 ko \|\| +0m00.02s \|\| -24 ko \| +11.11% \| -0.00% 0m00.20s \| 269028 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/RegisterNames.vo \| 0m00.26s \| 268860 ko \|\| -0m00.06s \|\| 168 ko \| -23.07% \| +0.06% 0m00.20s \| 290852 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Utility.vo \| 0m00.26s \| 290992 ko \|\| -0m00.06s \|\| -140 ko \| -23.07% \| -0.04% 0m00.20s \| 302588 ko \| Rewriter/Util/FMapPositive/Equality.vo \| 0m00.21s \| 302664 ko \|\| -0m00.00s \|\| -76 ko \| -4.76% \| -0.02% 0m00.20s \| 277796 ko \| TAPSort.vo \| 0m00.16s \| 277568 ko \|\| +0m00.04s \|\| 228 ko \| +25.00% \| +0.08% 0m00.20s \| 262824 ko \| Util/SideConditions/RingPackage.vo \| 0m00.19s \| 262748 ko \|\| +0m00.01s \|\| 76 ko \| +5.26% \| +0.02% 0m00.20s \| 262768 ko \| Util/Strings/StringMap.vo \| 0m00.24s \| 262876 ko \|\| -0m00.03s \|\| -108 ko \| -16.66% \| -0.04% 0m00.20s \| 261100 ko \| Util/ZUtil/Hints/Core.vo \| 0m00.20s \| 261312 ko \|\| +0m00.00s \|\| -212 ko \| +0.00% \| -0.08% 0m00.20s \| 260396 ko \| Util/ZUtil/Tactics/DivModToQuotRem.vo \| 0m00.20s \| 260684 ko \|\| +0m00.00s \|\| -288 ko \| +0.00% \| -0.11% 0m00.20s \| 258448 ko \| Util/ZUtil/Tactics/SplitMinMax.vo \| 0m00.20s \| 258332 ko \|\| +0m00.00s \|\| 116 ko \| +0.00% \| +0.04% 0m00.19s \| 243980 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Inhabited.vo \| 0m00.16s \| 243816 ko \|\| +0m00.03s \|\| 164 ko \| +18.75% \| +0.06% 0m00.19s \| 325440 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/String.vo \| 0m00.20s \| 325264 ko \|\| -0m00.01s \|\| 176 ko \| -5.00% \| +0.05% 0m00.19s \| 270152 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Solver.vo \| 0m00.23s \| 270116 ko \|\| -0m00.04s \|\| 36 ko \| -17.39% \| +0.01% 0m00.19s \| 246872 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricLogging.vo \| 0m00.20s \| 246756 ko \|\| -0m00.01s \|\| 116 ko \| -5.00% \| +0.04% 0m00.19s \| 257624 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Tactics.vo \| 0m00.19s \| 257588 ko \|\| +0m00.00s \|\| 36 ko \| +0.00% \| +0.01% 0m00.19s \| 223896 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/IdentParsing.vo \| 0m00.13s \| 223864 ko \|\| +0m00.06s \|\| 32 ko \| +46.15% \| +0.01% 0m00.19s \| 294788 ko \| Bedrock/Field/Common/Names/VarnameGenerator.vo \| 0m00.20s \| 294864 ko \|\| -0m00.01s \|\| -76 ko \| -5.00% \| -0.02% 0m00.19s \| 266556 ko \| Util/ZUtil/AddModulo.vo \| 0m00.15s \| 266876 ko \|\| +0m00.04s \|\| -320 ko \| +26.66% \| -0.11% 0m00.19s \| 262460 ko \| Util/ZUtil/Hints.vo \| 0m00.23s \| 262248 ko \|\| -0m00.04s \|\| 212 ko \| -17.39% \| +0.08% 0m00.19s \| 265464 ko \| Util/ZUtil/Hints/PullPush.vo \| 0m00.17s \| 265500 ko \|\| +0m00.01s \|\| -36 ko \| +11.76% \| -0.01% 0m00.19s \| 272280 ko \| Util/ZUtil/Modulo/Bootstrap.vo \| 0m00.17s \| 272524 ko \|\| +0m00.01s \|\| -244 ko \| +11.76% \| -0.08% 0m00.19s \| 345084 ko \| Util/ZUtil/Peano.vo \| 0m00.22s \| 344700 ko \|\| -0m00.03s \|\| 384 ko \| -13.63% \| +0.11% 0m00.19s \| 262828 ko \| Util/ZUtil/Tactics/ReplaceNegWithPos.vo \| 0m00.20s \| 262564 ko \|\| -0m00.01s \|\| 264 ko \| -5.00% \| +0.10% 0m00.18s \| 258460 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/SepBulletPoints.vo \| 0m00.19s \| 258564 ko \|\| -0m00.01s \|\| -104 ko \| -5.26% \| -0.04% 0m00.18s \| 253216 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/TracePredicate.vo \| 0m00.14s \| 253152 ko \|\| +0m00.03s \|\| 64 ko \| +28.57% \| +0.02% 0m00.18s \| 231320 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/MetricsToRiscv.vo \| 0m00.19s \| 231252 ko \|\| -0m00.01s \|\| 68 ko \| -5.26% \| +0.02% 0m00.18s \| 236756 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/NameGen.vo \| 0m00.18s \| 236968 ko \|\| +0m00.00s \|\| -212 ko \| +0.00% \| -0.08% 0m00.18s \| 309024 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Byte.vo \| 0m00.18s \| 308932 ko \|\| +0m00.00s \|\| 92 ko \| +0.00% \| +0.02% 0m00.18s \| 325956 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListWord.vo \| 0m00.19s \| 326040 ko \|\| -0m00.01s \|\| -84 ko \| -5.26% \| -0.02% 0m00.18s \| 262308 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Tactics.vo \| 0m00.23s \| 262328 ko \|\| -0m00.05s \|\| -20 ko \| -21.73% \| -0.00% 0m00.18s \| 258416 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/Lia.vo \| 0m00.19s \| 258268 ko \|\| -0m00.01s \|\| 148 ko \| -5.26% \| +0.05% 0m00.18s \| 260508 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/VirtualMemory.vo \| 0m00.22s \| 260660 ko \|\| -0m00.04s \|\| -152 ko \| -18.18% \| -0.05% 0m00.18s \| 248044 ko \| Algebra/Hierarchy.vo \| 0m00.16s \| 247972 ko \|\| +0m00.01s \|\| 72 ko \| +12.49% \| +0.02% 0m00.18s \| 249112 ko \| Coqprime/N/NatAux.vo \| 0m00.16s \| 249100 ko \|\| +0m00.01s \|\| 12 ko \| +12.49% \| +0.00% 0m00.18s \| 209260 ko \| Rewriter/Util/Strings/Ascii.vo \| 0m00.15s \| 209268 ko \|\| +0m00.03s \|\| -8 ko \| +20.00% \| -0.00% 0m00.18s \| 279276 ko \| Util/Factorize.vo \| 0m00.18s \| 279060 ko \|\| +0m00.00s \|\| 216 ko \| +0.00% \| +0.07% 0m00.18s \| 260272 ko \| Util/NUtil/Sorting.vo \| 0m00.11s \| 260080 ko \|\| +0m00.06s \|\| 192 ko \| +63.63% \| +0.07% 0m00.18s \| 312548 ko \| Util/PointedProp.vo \| 0m00.11s \| 312476 ko \|\| +0m00.06s \|\| 72 ko \| +63.63% \| +0.02% 0m00.18s \| 265596 ko \| Util/SideConditions/Autosolve.vo \| 0m00.22s \| 265712 ko \|\| -0m00.04s \|\| -116 ko \| -18.18% \| -0.04% 0m00.18s \| 253748 ko \| Util/Structures/Equalities/Sum.vo \| 0m00.19s \| 253892 ko \|\| -0m00.01s \|\| -144 ko \| -5.26% \| -0.05% 0m00.18s \| 279764 ko \| Util/ZUtil/Ge.vo \| 0m00.20s \| 279568 ko \|\| -0m00.02s \|\| 196 ko \| -10.00% \| +0.07% 0m00.18s \| 295072 ko \| Util/ZUtil/MulSplit.vo \| 0m00.23s \| 295276 ko \|\| -0m00.05s \|\| -204 ko \| -21.73% \| -0.06% 0m00.18s \| 297660 ko \| Util/ZUtil/Odd.vo \| 0m00.25s \| 297468 ko \|\| -0m00.07s \|\| 192 ko \| -28.00% \| +0.06% 0m00.18s \| 257696 ko \| Util/ZUtil/Tactics/CompareToSgn.vo \| 0m00.19s \| 257712 ko \|\| -0m00.01s \|\| -16 ko \| -5.26% \| -0.00% 0m00.18s \| 260260 ko \| Util/ZUtil/Tactics/PeelLe.vo \| 0m00.20s \| 260548 ko \|\| -0m00.02s \|\| -288 ko \| -10.00% \| -0.11% 0m00.18s \| 232144 ko \| Util/ZUtil/Tactics/PullPush.vo \| 0m00.19s \| 232376 ko \|\| -0m00.01s \|\| -232 ko \| -5.26% \| -0.09% 0m00.18s \| 237428 ko \| Util/ZUtil/ZSimplify.vo \| 0m00.18s \| 237328 ko \|\| +0m00.00s \|\| 100 ko \| +0.00% \| +0.04% 0m00.18s \| 262296 ko \| Util/ZUtil/ZSimplify/Core.vo \| 0m00.18s \| 262300 ko \|\| +0m00.00s \|\| -4 ko \| +0.00% \| -0.00% 0m00.17s \| 246500 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Map/Separation.vo \| 0m00.13s \| 246488 ko \|\| +0m00.04s \|\| 12 ko \| +30.76% \| +0.00% 0m00.17s \| 277028 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Funext.vo \| 0m00.19s \| 277168 ko \|\| -0m00.01s \|\| -140 ko \| -10.52% \| -0.05% 0m00.17s \| 279564 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Sorting/OrderToPermutation.vo \| 0m00.23s \| 279772 ko \|\| -0m00.06s \|\| -208 ko \| -26.08% \| -0.07% 0m00.17s \| 331056 ko \| Coqprime/PrimalityTest/FGroup.vo \| 0m00.26s \| 331120 ko \|\| -0m00.09s \|\| -64 ko \| -34.61% \| -0.01% 0m00.17s \| 263828 ko \| Rewriter/Util/Prod.vo \| 0m00.06s \| 263776 ko \|\| +0m00.11s \|\| 52 ko \| +183.33% \| +0.01% 0m00.17s \| 296644 ko \| Util/ListUtil/FoldBool.vo \| 0m00.16s \| 296824 ko \|\| +0m00.01s \|\| -180 ko \| +6.25% \| -0.06% 0m00.17s \| 186620 ko \| Util/ParseTaps.vo \| 0m00.14s \| 186784 ko \|\| +0m00.03s \|\| -164 ko \| +21.42% \| -0.08% 0m00.17s \| 266600 ko \| Util/ZUtil/LnotModulo.vo \| 0m00.22s \| 266616 ko \|\| -0m00.04s \|\| -16 ko \| -22.72% \| -0.00% 0m00.17s \| 257972 ko \| Util/ZUtil/Tactics/DivideExistsMul.vo \| 0m00.18s \| 257752 ko \|\| -0m00.00s \|\| 220 ko \| -5.55% \| +0.08% 0m00.17s \| 20748 ko \| fiat-go/64/poly1305/poly1305.go \| 0m00.18s \| 20728 ko \|\| -0m00.00s \|\| 20 ko \| -5.55% \| +0.09% 0m00.16s \| 235120 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Structs.vo \| 0m00.20s \| 235172 ko \|\| -0m00.04s \|\| -52 ko \| -20.00% \| -0.02% 0m00.16s \| 242432 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Decidable.vo \| 0m00.16s \| 242696 ko \|\| +0m00.00s \|\| -264 ko \| +0.00% \| -0.10% 0m00.16s \| 287000 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/Interface.vo \| 0m00.15s \| 287136 ko \|\| +0m00.01s \|\| -136 ko \| +6.66% \| -0.04% 0m00.16s \| 240784 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/SafeSimpl.vo \| 0m00.15s \| 240672 ko \|\| +0m00.01s \|\| 112 ko \| +6.66% \| +0.04% 0m00.16s \| 258476 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth.vo \| 0m00.18s \| 258496 ko \|\| -0m00.01s \|\| -20 ko \| -11.11% \| -0.00% 0m00.16s \| 307808 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/RecordSetters.vo \| 0m00.18s \| 307796 ko \|\| -0m00.01s \|\| 12 ko \| -11.11% \| +0.00% 0m00.16s \| 251616 ko \| Rewriter/Util/Strings/Decimal.vo \| 0m00.19s \| 251952 ko \|\| -0m00.03s \|\| -336 ko \| -15.78% \| -0.13% 0m00.16s \| 207116 ko \| Util/ListUtil/NthExt.vo \| 0m00.11s \| 207060 ko \|\| +0m00.05s \|\| 56 ko \| +45.45% \| +0.02% 0m00.16s \| 252224 ko \| Util/Strings/Decimal.vo \| 0m00.19s \| 252256 ko \|\| -0m00.03s \|\| -32 ko \| -15.78% \| -0.01% 0m00.15s \| 217032 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Bytedump.vo \| 0m00.16s \| 217112 ko \|\| -0m00.01s \|\| -80 ko \| -6.25% \| -0.03% 0m00.15s \| 247732 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.vo \| 0m00.21s \| 247668 ko \|\| -0m00.06s \|\| 64 ko \| -28.57% \| +0.02% 0m00.15s \| 243392 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Map/SortedListString.vo \| 0m00.17s \| 243292 ko \|\| -0m00.02s \|\| 100 ko \| -11.76% \| +0.04% 0m00.15s \| 258428 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Word/Bitwidth64.vo \| 0m00.23s \| 258148 ko \|\| -0m00.08s \|\| 280 ko \| -34.78% \| +0.10% 0m00.15s \| 259900 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words64Naive.vo \| 0m00.18s \| 259788 ko \|\| -0m00.03s \|\| 112 ko \| -16.66% \| +0.04% 0m00.15s \| 268072 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/nat_div_mod_to_quot_rem.vo \| 0m00.24s \| 267836 ko \|\| -0m00.09s \|\| 236 ko \| -37.50% \| +0.08% 0m00.15s \| 239028 ko \| Util/LetInMonad.vo \| 0m00.12s \| 239004 ko \|\| +0m00.03s \|\| 24 ko \| +25.00% \| +0.01% 0m00.15s \| 272508 ko \| Util/ZUtil/DistrIf.vo \| 0m00.17s \| 272392 ko \|\| -0m00.02s \|\| 116 ko \| -11.76% \| +0.04% 0m00.15s \| 23388 ko \| fiat-bedrock2/src/poly1305_64.c \| 0m00.17s \| 23120 ko \|\| -0m00.02s \|\| 268 ko \| -11.76% \| +1.15% 0m00.14s \| 213928 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Syntax.vo \| 0m00.17s \| 213892 ko \|\| -0m00.03s \|\| 36 ko \| -17.64% \| +0.01% 0m00.14s \| 190864 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Variables.vo \| 0m00.16s \| 190960 ko \|\| -0m00.01s \|\| -96 ko \| -12.49% \| -0.05% 0m00.14s \| 198372 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/ident_to_string.vo \| 0m00.11s \| 198580 ko \|\| +0m00.03s \|\| -208 ko \| +27.27% \| -0.10% 0m00.14s \| 214764 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_core.vo \| 0m00.17s \| 214676 ko \|\| -0m00.03s \|\| 88 ko \| -17.64% \| +0.04% 0m00.14s \| 256480 ko \| Rewriter/Util/OptionList.vo \| 0m00.17s \| 256616 ko \|\| -0m00.03s \|\| -136 ko \| -17.64% \| -0.05% 0m00.14s \| 221020 ko \| Rewriter/Util/Sigma.vo \| 0m00.14s \| 220932 ko \|\| +0m00.00s \|\| 88 ko \| +0.00% \| +0.03% 0m00.14s \| 233316 ko \| Util/Decidable/Bool2Prop.vo \| 0m00.19s \| 233280 ko \|\| -0m00.04s \|\| 36 ko \| -26.31% \| +0.01% 0m00.14s \| 268828 ko \| Util/Prod.vo \| 0m00.16s \| 269048 ko \|\| -0m00.01s \|\| -220 ko \| -12.49% \| -0.08% 0m00.14s \| 189548 ko \| Util/SideConditions/ReductionPackages.vo \| 0m00.12s \| 189468 ko \|\| +0m00.02s \|\| 80 ko \| +16.66% \| +0.04% 0m00.14s \| 210940 ko \| Util/Strings/Ascii.vo \| 0m00.15s \| 210760 ko \|\| -0m00.00s \|\| 180 ko \| -6.66% \| +0.08% 0m00.14s \| 22168 ko \| fiat-json/src/poly1305_64.json \| 0m00.11s \| 22720 ko \|\| +0m00.03s \|\| -552 ko \| +27.27% \| -2.42% 0m00.13s \| 147568 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/HList.vo \| 0m00.11s \| 147636 ko \|\| +0m00.02s \|\| -68 ko \| +18.18% \| -0.04% 0m00.13s \| 193192 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/destr.vo \| 0m00.14s \| 193276 ko \|\| -0m00.01s \|\| -84 ko \| -7.14% \| -0.04% 0m00.13s \| 142380 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/JMonad.vo \| 0m00.13s \| 142312 ko \|\| +0m00.00s \|\| 68 ko \| +0.00% \| +0.04% 0m00.13s \| 185900 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MMIOTrace.vo \| 0m00.10s \| 185972 ko \|\| +0m00.03s \|\| -72 ko \| +30.00% \| -0.03% 0m00.13s \| 250288 ko \| Util/ListUtil/Partition.vo \| 0m00.17s \| 250088 ko \|\| -0m00.04s \|\| 200 ko \| -23.52% \| +0.07% 0m00.13s \| 177232 ko \| Util/ListUtil/PermutationCompat.vo \| 0m00.13s \| 177004 ko \|\| +0m00.00s \|\| 228 ko \| +0.00% \| +0.12% 0m00.13s \| 253768 ko \| Util/Telescope/Equality.vo \| 0m00.15s \| 253556 ko \|\| -0m00.01s \|\| 212 ko \| -13.33% \| +0.08% 0m00.13s \| 228000 ko \| Util/ZUtil/Tactics/PrimeBound.vo \| 0m00.20s \| 227980 ko \|\| -0m00.07s \|\| 20 ko \| -35.00% \| +0.00% 0m00.13s \| 18996 ko \| fiat-zig/src/poly1305_64.zig \| 0m00.11s \| 18984 ko \|\| +0m00.02s \|\| 12 ko \| +18.18% \| +0.06% 0m00.12s \| 187324 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_arith_hints.vo \| 0m00.14s \| 187588 ko \|\| -0m00.02s \|\| -264 ko \| -14.28% \| -0.14% 0m00.12s \| 237300 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_list_hints.vo \| 0m00.18s \| 237640 ko \|\| -0m00.06s \|\| -340 ko \| -33.33% \| -0.14% 0m00.12s \| 181808 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/div_mod_to_equations.vo \| 0m00.12s \| 181816 ko \|\| +0m00.00s \|\| -8 ko \| +0.00% \| -0.00% 0m00.12s \| 173856 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Z/div_to_equations.vo \| 0m00.12s \| 174000 ko \|\| +0m00.00s \|\| -144 ko \| +0.00% \| -0.08% 0m00.12s \| 131228 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/ExtensibleRecords.vo \| 0m00.12s \| 131440 ko \|\| +0m00.00s \|\| -212 ko \| +0.00% \| -0.16% 0m00.12s \| 164716 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadT.vo \| 0m00.13s \| 164644 ko \|\| -0m00.01s \|\| 72 ko \| -7.69% \| +0.04% 0m00.12s \| 213252 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadTests.vo \| 0m00.12s \| 213020 ko \|\| +0m00.00s \|\| 232 ko \| +0.00% \| +0.10% 0m00.12s \| 161884 ko \| Rewriter/Util/PrimitiveSigma.vo \| 0m00.10s \| 161800 ko \|\| +0m00.01s \|\| 84 ko \| +19.99% \| +0.05% 0m00.12s \| 201308 ko \| Util/PrimitiveProd.vo \| 0m00.11s \| 201536 ko \|\| +0m00.00s \|\| -228 ko \| +9.09% \| -0.11% 0m00.12s \| 167896 ko \| Util/PrimitiveSigma.vo \| 0m00.14s \| 167664 ko \|\| -0m00.02s \|\| 232 ko \| -14.28% \| +0.13% 0m00.12s \| 187780 ko \| Util/Relations.vo \| 0m00.10s \| 188004 ko \|\| +0m00.01s \|\| -224 ko \| +19.99% \| -0.11% 0m00.12s \| 176516 ko \| Util/ZUtil/Notations.vo \| 0m00.14s \| 176460 ko \|\| -0m00.02s \|\| 56 ko \| -14.28% \| +0.03% 0m00.12s \| 19392 ko \| fiat-c/src/poly1305_64.c \| 0m00.11s \| 19232 ko \|\| +0m00.00s \|\| 160 ko \| +9.09% \| +0.83% 0m00.12s \| 19440 ko \| fiat-rust/src/poly1305_64.rs \| 0m00.12s \| 19304 ko \|\| +0m00.00s \|\| 136 ko \| +0.00% \| +0.70% 0m00.11s \| 186236 ko \| /home/jgross/fiat-crypto/rupicola/src/Rupicola/Lib/Gensym.vo \| 0m00.16s \| 185968 ko \|\| -0m00.05s \|\| 268 ko \| -31.25% \| +0.14% 0m00.11s \| 142596 ko \| Util/Equality.vo \| 0m00.08s \| 142300 ko \|\| +0m00.03s \|\| 296 ko \| +37.50% \| +0.20% 0m00.11s \| 226616 ko \| Util/Sigma.vo \| 0m00.12s \| 226496 ko \|\| -0m00.00s \|\| 120 ko \| -8.33% \| +0.05% 0m00.10s \| 210820 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/TacticError.vo \| 0m00.15s \| 210752 ko \|\| -0m00.04s \|\| 68 ko \| -33.33% \| +0.03% 0m00.10s \| 205552 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/FreeMonad.vo \| 0m00.13s \| 205756 ko \|\| -0m00.03s \|\| -204 ko \| -23.07% \| -0.09% 0m00.10s \| 195516 ko \| Rewriter/Util/PrimitiveProd.vo \| 0m00.09s \| 195520 ko \|\| +0m00.01s \|\| -4 ko \| +11.11% \| -0.00% 0m00.10s \| 212956 ko \| Spec/MxDH.vo \| 0m00.14s \| 212904 ko \|\| -0m00.04s \|\| 52 ko \| -28.57% \| +0.02% 0m00.10s \| 173164 ko \| Util/ListUtil/ForallIn.vo \| 0m00.11s \| 173072 ko \|\| -0m00.00s \|\| 92 ko \| -9.09% \| +0.05% 0m00.10s \| 174076 ko \| Util/ListUtil/IndexOf.vo \| 0m00.14s \| 174164 ko \|\| -0m00.04s \|\| -88 ko \| -28.57% \| -0.05% 0m00.10s \| 113864 ko \| Util/Tactics.vo \| 0m00.07s \| 114004 ko \|\| +0m00.03s \|\| -140 ko \| +42.85% \| -0.12% 0m00.09s \| 110464 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Sorting/Permutation.vo \| 0m00.04s \| 110648 ko \|\| +0m00.05s \|\| -184 ko \| +124.99% \| -0.16% 0m00.09s \| 111104 ko \| Rewriter/Language/PreCommon.vo \| 0m00.06s \| 111064 ko \|\| +0m00.03s \|\| 40 ko \| +50.00% \| +0.03% 0m00.09s \| 111476 ko \| Rewriter/Util/PrimitiveHList.vo \| 0m00.07s \| 111412 ko \|\| +0m00.01s \|\| 64 ko \| +28.57% \| +0.05% 0m00.09s \| 106788 ko \| Util/DynList.vo \| 0m00.09s \| 106816 ko \|\| +0m00.00s \|\| -28 ko \| +0.00% \| -0.02% 0m00.09s \| 127780 ko \| Util/ErrorT.vo \| 0m00.08s \| 127824 ko \|\| +0m00.00s \|\| -44 ko \| +12.49% \| -0.03% 0m00.09s \| 103768 ko \| Util/LetIn.vo \| 0m00.09s \| 104032 ko \|\| +0m00.00s \|\| -264 ko \| +0.00% \| -0.25% 0m00.09s \| 111876 ko \| Util/PrimitiveHList.vo \| 0m00.09s \| 111704 ko \|\| +0m00.00s \|\| 172 ko \| +0.00% \| +0.15% 0m00.09s \| 112928 ko \| Util/TagList.vo \| 0m00.11s \| 113048 ko \|\| -0m00.02s \|\| -120 ko \| -18.18% \| -0.10% 0m00.09s \| 88820 ko \| Util/Tower.vo \| 0m00.05s \| 88728 ko \|\| +0m00.03s \|\| 92 ko \| +79.99% \| +0.10% 0m00.09s \| 116736 ko \| tests/RecordSetTests.vo \| 0m00.06s \| 116668 ko \|\| +0m00.03s \|\| 68 ko \| +50.00% \| +0.05% 0m00.08s \| 86144 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/GenericForeverSafe.vo \| 0m00.05s \| 85868 ko \|\| +0m00.03s \|\| 276 ko \| +60.00% \| +0.32% 0m00.08s \| 120324 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/Simulation.vo \| 0m00.10s \| 120548 ko \|\| -0m00.02s \|\| -224 ko \| -20.00% \| -0.18% 0m00.08s \| 111936 ko \| Rewriter/Language/Pre.vo \| 0m00.11s \| 111844 ko \|\| -0m00.03s \|\| 92 ko \| -27.27% \| +0.08% 0m00.08s \| 137108 ko \| Rewriter/Util/Equality.vo \| 0m00.06s \| 137104 ko \|\| +0m00.02s \|\| 4 ko \| +33.33% \| +0.00% 0m00.08s \| 106664 ko \| Util/ListUtil/RemoveN.vo \| 0m00.07s \| 106664 ko \|\| +0m00.00s \|\| 0 ko \| +14.28% \| +0.00% 0m00.08s \| 118908 ko \| Util/Structures/Equalities/Iso.vo \| 0m00.09s \| 118964 ko \|\| -0m00.00s \|\| -56 ko \| -11.11% \| -0.04% 0m00.08s \| 107716 ko \| Util/Tactics/AllInstances.vo \| 0m00.07s \| 107652 ko \|\| +0m00.00s \|\| 64 ko \| +14.28% \| +0.05% 0m00.07s \| 122816 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Lift1Prop.vo \| 0m00.06s \| 122580 ko \|\| +0m00.01s \|\| 236 ko \| +16.66% \| +0.19% 0m00.07s \| 112096 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Option.vo \| 0m00.07s \| 112060 ko \|\| +0m00.00s \|\| 36 ko \| +0.00% \| +0.03% 0m00.07s \| 110440 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadNotations.vo \| 0m00.05s \| 110424 ko \|\| +0m00.02s \|\| 16 ko \| +40.00% \| +0.01% 0m00.07s \| 131200 ko \| Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo \| 0m00.07s \| 131176 ko \|\| +0m00.00s \|\| 24 ko \| +0.00% \| +0.01% 0m00.07s \| 115132 ko \| Rewriter/Util/Sigma/Related.vo \| 0m00.04s \| 114924 ko \|\| +0m00.03s \|\| 208 ko \| +75.00% \| +0.18% 0m00.07s \| 71676 ko \| Rewriter/Util/Tactics/FindHyp.vo \| 0m00.04s \| 71660 ko \|\| +0m00.03s \|\| 16 ko \| +75.00% \| +0.02% 0m00.07s \| 89036 ko \| Util/AutoRewrite.vo \| 0m00.05s \| 88672 ko \|\| +0m00.02s \|\| 364 ko \| +40.00% \| +0.41% 0m00.07s \| 76072 ko \| Util/Curry.vo \| 0m00.03s \| 75872 ko \|\| +0m00.04s \|\| 200 ko \| +133.33% \| +0.26% 0m00.07s \| 106780 ko \| Util/ListUtil/CombineExtend.vo \| 0m00.10s \| 106960 ko \|\| -0m00.03s \|\| -180 ko \| -30.00% \| -0.16% 0m00.07s \| 110764 ko \| Util/ListUtil/FoldMap.vo \| 0m00.11s \| 110788 ko \|\| -0m00.03s \|\| -24 ko \| -36.36% \| -0.02% 0m00.07s \| 110928 ko \| Util/ListUtil/Split.vo \| 0m00.09s \| 110864 ko \|\| -0m00.01s \|\| 64 ko \| -22.22% \| +0.05% 0m00.07s \| 109288 ko \| Util/Structures/Orders/Iso.vo \| 0m00.06s \| 109412 ko \|\| +0m00.01s \|\| -124 ko \| +16.66% \| -0.11% 0m00.07s \| 107416 ko \| Util/Tactics/AllSuccesses.vo \| 0m00.08s \| 107480 ko \|\| -0m00.00s \|\| -64 ko \| -12.49% \| -0.05% 0m00.07s \| 101376 ko \| Util/Tactics/RewriteHyp.vo \| 0m00.08s \| 101380 ko \|\| -0m00.00s \|\| -4 ko \| -12.49% \| -0.00% 0m00.07s \| 103160 ko \| Util/Telescope/Core.vo \| 0m00.07s \| 103352 ko \|\| +0m00.00s \|\| -192 ko \| +0.00% \| -0.18% 0m00.07s \| 78180 ko \| Util/Unit.vo \| 0m00.04s \| 78104 ko \|\| +0m00.03s \|\| 76 ko \| +75.00% \| +0.09% 0m00.07s \| 110468 ko \| tests/ListNotationTests.vo \| 0m00.07s \| 110544 ko \|\| +0m00.00s \|\| -76 ko \| +0.00% \| -0.06% 0m00.06s \| 102368 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/ReversedListNotations.vo \| 0m00.08s \| 102496 ko \|\| -0m00.02s \|\| -128 ko \| -25.00% \| -0.12% 0m00.06s \| 76880 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Log.vo \| 0m00.03s \| 76596 ko \|\| +0m00.03s \|\| 284 ko \| +100.00% \| +0.37% 0m00.06s \| 116724 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/Records.vo \| 0m00.09s \| 116720 ko \|\| -0m00.03s \|\| 4 ko \| -33.33% \| +0.00% 0m00.06s \| 83120 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/eplace.vo \| 0m00.03s \| 83020 ko \|\| +0m00.03s \|\| 100 ko \| +100.00% \| +0.12% 0m00.06s \| 99824 ko \| Rewriter/Util/Logic/ExistsEqAnd.vo \| 0m00.06s \| 99824 ko \|\| +0m00.00s \|\| 0 ko \| +0.00% \| +0.00% 0m00.06s \| 74540 ko \| Rewriter/Util/Tactics/BreakMatch.vo \| 0m00.03s \| 74700 ko \|\| +0m00.03s \|\| -160 ko \| +100.00% \| -0.21% 0m00.06s \| 67408 ko \| Rewriter/Util/Tactics/Test.vo \| 0m00.02s \| 67172 ko \|\| +0m00.03s \|\| 236 ko \| +199.99% \| +0.35% 0m00.06s \| 69432 ko \| Rewriter/Util/TypeList.vo \| 0m00.06s \| 69304 ko \|\| +0m00.00s \|\| 128 ko \| +0.00% \| +0.18% 0m00.06s \| 152924 ko \| Util/Bool.vo \| 0m00.08s \| 152996 ko \|\| -0m00.02s \|\| -72 ko \| -25.00% \| -0.04% 0m00.06s \| 101716 ko \| Util/HProp.vo \| 0m00.04s \| 101680 ko \|\| +0m00.01s \|\| 36 ko \| +49.99% \| +0.03% 0m00.06s \| 107900 ko \| Util/ListUtil/Concat.vo \| 0m00.08s \| 107708 ko \|\| -0m00.02s \|\| 192 ko \| -25.00% \| +0.17% 0m00.06s \| 105808 ko \| Util/Logic/ExistsEqAnd.vo \| 0m00.05s \| 105944 ko \|\| +0m00.00s \|\| -136 ko \| +19.99% \| -0.12% 0m00.06s \| 82292 ko \| Util/Logic/Forall.vo \| 0m00.05s \| 82216 ko \|\| +0m00.00s \|\| 76 ko \| +19.99% \| +0.09% 0m00.06s \| 75104 ko \| Util/Sigma/Associativity.vo \| 0m00.04s \| 75016 ko \|\| +0m00.01s \|\| 88 ko \| +49.99% \| +0.11% 0m00.06s \| 74688 ko \| Util/Sigma/MapProjections.vo \| 0m00.03s \| 74668 ko \|\| +0m00.03s \|\| 20 ko \| +100.00% \| +0.02% 0m00.06s \| 120692 ko \| Util/Sigma/Related.vo \| 0m00.09s \| 120812 ko \|\| -0m00.03s \|\| -120 ko \| -33.33% \| -0.09% 0m00.06s \| 94772 ko \| Util/Structures/Orders.vo \| 0m00.07s \| 94968 ko \|\| -0m00.01s \|\| -196 ko \| -14.28% \| -0.20% 0m00.06s \| 77344 ko \| Util/Tactics/CountBinders.vo \| 0m00.05s \| 77116 ko \|\| +0m00.00s \|\| 228 ko \| +19.99% \| +0.29% 0m00.06s \| 83672 ko \| Util/Tactics/DestructHead.vo \| 0m00.04s \| 83520 ko \|\| +0m00.01s \|\| 152 ko \| +49.99% \| +0.18% 0m00.06s \| 72692 ko \| Util/Tactics/PrintContext.vo \| 0m00.05s \| 72848 ko \|\| +0m00.00s \|\| -156 ko \| +19.99% \| -0.21% 0m00.06s \| 184096 ko \| Util/Telescope/Instances.vo \| 0m00.11s \| 184168 ko \|\| -0m00.05s \|\| -72 ko \| -45.45% \| -0.03% 0m00.05s \| 86264 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Hexdump.vo \| 0m00.04s \| 86376 ko \|\| +0m00.01s \|\| -112 ko \| +25.00% \| -0.12% 0m00.05s \| 68888 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/on_hyp_containing.vo \| 0m00.01s \| 68992 ko \|\| +0m00.04s \|\| -104 ko \| +400.00% \| -0.15% 0m00.05s \| 80672 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Misc.vo \| 0m00.02s \| 80996 ko \|\| +0m00.03s \|\| -324 ko \| +150.00% \| -0.40% 0m00.05s \| 98284 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/Prod.vo \| 0m00.06s \| 98412 ko \|\| -0m00.00s \|\| -128 ko \| -16.66% \| -0.13% 0m00.05s \| 77240 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/symmetry.vo \| 0m00.03s \| 77252 ko \|\| +0m00.02s \|\| -12 ko \| +66.66% \| -0.01% 0m00.05s \| 78888 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ParamRecords.vo \| 0m00.05s \| 78984 ko \|\| +0m00.00s \|\| -96 ko \| +0.00% \| -0.12% 0m00.05s \| 74112 ko \| RecordSet.vo \| 0m00.03s \| 74048 ko \|\| +0m00.02s \|\| 64 ko \| +66.66% \| +0.08% 0m00.05s \| 130576 ko \| Rewriter/Util/Bool.vo \| 0m00.08s \| 130596 ko \|\| -0m00.03s \|\| -20 ko \| -37.50% \| -0.01% 0m00.05s \| 77332 ko \| Rewriter/Util/FixCoqMistakes.vo \| 0m00.05s \| 77432 ko \|\| +0m00.00s \|\| -100 ko \| +0.00% \| -0.12% 0m00.05s \| 96476 ko \| Rewriter/Util/HProp.vo \| 0m00.06s \| 96292 ko \|\| -0m00.00s \|\| 184 ko \| -16.66% \| +0.19% 0m00.05s \| 84776 ko \| Rewriter/Util/Notations.vo \| 0m00.05s \| 84828 ko \|\| +0m00.00s \|\| -52 ko \| +0.00% \| -0.06% 0m00.05s \| 88232 ko \| Rewriter/Util/Pointed.vo \| 0m00.02s \| 88100 ko \|\| +0m00.03s \|\| 132 ko \| +150.00% \| +0.14% 0m00.05s \| 71720 ko \| Rewriter/Util/Tactics/DoWithHyp.vo \| 0m00.03s \| 71692 ko \|\| +0m00.02s \|\| 28 ko \| +66.66% \| +0.03% 0m00.05s \| 71488 ko \| Rewriter/Util/Tactics/RunTacticAsConstr.vo \| 0m00.06s \| 71428 ko \|\| -0m00.00s \|\| 60 ko \| -16.66% \| +0.08% 0m00.05s \| 72712 ko \| Rewriter/Util/Tactics/SplitInContext.vo \| 0m00.05s \| 72812 ko \|\| +0m00.00s \|\| -100 ko \| +0.00% \| -0.13% 0m00.05s \| 67276 ko \| Rewriter/Util/Tactics/SubstEvars.vo \| 0m00.01s \| 67520 ko \|\| +0m00.04s \|\| -244 ko \| +400.00% \| -0.36% 0m00.05s \| 72152 ko \| Rewriter/Util/Tactics/UniquePose.vo \| 0m00.05s \| 72252 ko \|\| +0m00.00s \|\| -100 ko \| +0.00% \| -0.13% 0m00.05s \| 82032 ko \| Util/Bool/LeCompat.vo \| 0m00.04s \| 82028 ko \|\| +0m00.01s \|\| 4 ko \| +25.00% \| +0.00% 0m00.05s \| 82844 ko \| Util/FixCoqMistakes.vo \| 0m00.04s \| 82696 ko \|\| +0m00.01s \|\| 148 ko \| +25.00% \| +0.17% 0m00.05s \| 90656 ko \| Util/Notations.vo \| 0m00.04s \| 90832 ko \|\| +0m00.01s \|\| -176 ko \| +25.00% \| -0.19% 0m00.05s \| 81108 ko \| Util/SideConditions/CorePackages.vo \| 0m00.06s \| 80952 ko \|\| -0m00.00s \|\| 156 ko \| -16.66% \| +0.19% 0m00.05s \| 80584 ko \| Util/Tactics/BreakMatch.vo \| 0m00.02s \| 80420 ko \|\| +0m00.03s \|\| 164 ko \| +150.00% \| +0.20% 0m00.05s \| 72816 ko \| Util/Tactics/ConstrFail.vo \| 0m00.02s \| 72468 ko \|\| +0m00.03s \|\| 348 ko \| +150.00% \| +0.48% 0m00.05s \| 73068 ko \| Util/Tactics/Not.vo \| 0m00.05s \| 72852 ko \|\| +0m00.00s \|\| 216 ko \| +0.00% \| +0.29% 0m00.05s \| 76728 ko \| Util/Tactics/RevertUntil.vo \| 0m00.03s \| 76992 ko \|\| +0m00.02s \|\| -264 ko \| +66.66% \| -0.34% 0m00.05s \| 73656 ko \| Util/Tactics/SimplifyProjections.vo \| 0m00.03s \| 73660 ko \|\| +0m00.02s \|\| -4 ko \| +66.66% \| -0.00% 0m00.05s \| 72688 ko \| Util/Tactics/SubstLet.vo \| 0m00.03s \| 72552 ko \|\| +0m00.02s \|\| 136 ko \| +66.66% \| +0.18% 0m00.05s \| 74000 ko \| Util/Tactics/UnifyAbstractReflexivity.vo \| 0m00.05s \| 74024 ko \|\| +0m00.00s \|\| -24 ko \| +0.00% \| -0.03% 0m00.05s \| 73304 ko \| Util/Tactics/WarnIfGoalsRemain.vo \| 0m00.03s \| 73096 ko \|\| +0m00.02s \|\| 208 ko \| +66.66% \| +0.28% 0m00.05s \| 74900 ko \| tests/SimpleRecordUpdate.vo \| 0m00.02s \| 75256 ko \|\| +0m00.03s \|\| -356 ko \| +150.00% \| -0.47% 0m00.04s \| 68160 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Notations.vo \| 0m00.05s \| 68084 ko \|\| -0m00.01s \|\| 76 ko \| -20.00% \| +0.11% 0m00.04s \| 69984 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/Learning.vo \| 0m00.04s \| 70116 ko \|\| +0m00.00s \|\| -132 ko \| +0.00% \| -0.18% 0m00.04s \| 77196 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Constr.vo \| 0m00.03s \| 77428 ko \|\| +0m00.01s \|\| -232 ko \| +33.33% \| -0.29% 0m00.04s \| 76696 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Ltac2Lib/Msg.vo \| 0m00.05s \| 76424 ko \|\| -0m00.01s \|\| 272 ko \| -20.00% \| +0.35% 0m00.04s \| 67060 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/unique.vo \| 0m00.03s \| 66908 ko \|\| +0m00.01s \|\| 152 ko \| +33.33% \| +0.22% 0m00.04s \| 67448 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/eabstract.vo \| 0m00.04s \| 67336 ko \|\| +0m00.00s \|\| 112 ko \| +0.00% \| +0.16% 0m00.04s \| 71328 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/forward.vo \| 0m00.04s \| 71216 ko \|\| +0m00.00s \|\| 112 ko \| +0.00% \| +0.15% 0m00.04s \| 68812 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/fwd_bool_hints.vo \| 0m00.04s \| 68716 ko \|\| +0m00.00s \|\| 96 ko \| +0.00% \| +0.13% 0m00.04s \| 76108 ko \| Rewriter/Util/Bool/Equality.vo \| 0m00.01s \| 76320 ko \|\| +0m00.03s \|\| -212 ko \| +300.00% \| -0.27% 0m00.04s \| 68424 ko \| Rewriter/Util/Isomorphism.vo \| 0m00.03s \| 68580 ko \|\| +0m00.01s \|\| -156 ko \| +33.33% \| -0.22% 0m00.04s \| 98656 ko \| Rewriter/Util/LetIn.vo \| 0m00.03s \| 98652 ko \|\| +0m00.01s \|\| 4 ko \| +33.33% \| +0.00% 0m00.04s \| 84708 ko \| Rewriter/Util/Logic/ProdForall.vo \| 0m00.04s \| 84956 ko \|\| +0m00.00s \|\| -248 ko \| +0.00% \| -0.29% 0m00.04s \| 71172 ko \| Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo \| 0m00.02s \| 71100 ko \|\| +0m00.02s \|\| 72 ko \| +100.00% \| +0.10% 0m00.04s \| 67180 ko \| Rewriter/Util/Tactics/ConstrFail.vo \| 0m00.04s \| 67344 ko \|\| +0m00.00s \|\| -164 ko \| +0.00% \| -0.24% 0m00.04s \| 76216 ko \| Rewriter/Util/Tactics/DebugPrint.vo \| 0m00.06s \| 76328 ko \|\| -0m00.01s \|\| -112 ko \| -33.33% \| -0.14% 0m00.04s \| 77784 ko \| Rewriter/Util/Tactics/DestructHead.vo \| 0m00.06s \| 78072 ko \|\| -0m00.01s \|\| -288 ko \| -33.33% \| -0.36% 0m00.04s \| 71228 ko \| Rewriter/Util/Tactics/Head.vo \| 0m00.03s \| 71260 ko \|\| +0m00.01s \|\| -32 ko \| +33.33% \| -0.04% 0m00.04s \| 67340 ko \| Rewriter/Util/Tactics/Not.vo \| 0m00.04s \| 67108 ko \|\| +0m00.00s \|\| 232 ko \| +0.00% \| +0.34% 0m00.04s \| 67660 ko \| Rewriter/Util/Tactics/PrintGoal.vo \| 0m00.02s \| 67508 ko \|\| +0m00.02s \|\| 152 ko \| +100.00% \| +0.22% 0m00.04s \| 95312 ko \| Rewriter/Util/Tactics/RewriteHyp.vo \| 0m00.04s \| 95572 ko \|\| +0m00.00s \|\| -260 ko \| +0.00% \| -0.27% 0m00.04s \| 81440 ko \| Util/Bool/Equality.vo \| 0m00.03s \| 81620 ko \|\| +0m00.01s \|\| -180 ko \| +33.33% \| -0.22% 0m00.04s \| 84416 ko \| Util/Comparison.vo \| 0m00.03s \| 84576 ko \|\| +0m00.01s \|\| -160 ko \| +33.33% \| -0.18% 0m00.04s \| 105384 ko \| Util/Compose.vo \| 0m00.09s \| 105268 ko \|\| -0m00.05s \|\| 116 ko \| -55.55% \| +0.11% 0m00.04s \| 73520 ko \| Util/FueledLUB.vo \| 0m00.05s \| 73596 ko \|\| -0m00.01s \|\| -76 ko \| -20.00% \| -0.10% 0m00.04s \| 80292 ko \| Util/Logic/Exists.vo \| 0m00.04s \| 80316 ko \|\| +0m00.00s \|\| -24 ko \| +0.00% \| -0.02% 0m00.04s \| 80436 ko \| Util/Logic/ImplAnd.vo \| 0m00.01s \| 80176 ko \|\| +0m00.03s \|\| 260 ko \| +300.00% \| +0.32% 0m00.04s \| 90480 ko \| Util/Logic/ProdForall.vo \| 0m00.05s \| 90400 ko \|\| -0m00.01s \|\| 80 ko \| -20.00% \| +0.08% 0m00.04s \| 80728 ko \| Util/PER.vo \| 0m00.02s \| 80580 ko \|\| +0m00.02s \|\| 148 ko \| +100.00% \| +0.18% 0m00.04s \| 93440 ko \| Util/Pointed.vo \| 0m00.04s \| 93428 ko \|\| +0m00.00s \|\| 12 ko \| +0.00% \| +0.01% 0m00.04s \| 94940 ko \| Util/Sumbool.vo \| 0m00.04s \| 94912 ko \|\| +0m00.00s \|\| 28 ko \| +0.00% \| +0.02% 0m00.04s \| 73180 ko \| Util/Tactics/ClearDuplicates.vo \| 0m00.05s \| 73148 ko \|\| -0m00.01s \|\| 32 ko \| -20.00% \| +0.04% 0m00.04s \| 72952 ko \| Util/Tactics/Contains.vo \| 0m00.03s \| 72644 ko \|\| +0m00.01s \|\| 308 ko \| +33.33% \| +0.42% 0m00.04s \| 81700 ko \| Util/Tactics/DebugPrint.vo \| 0m00.02s \| 81644 ko \|\| +0m00.02s \|\| 56 ko \| +100.00% \| +0.06% 0m00.04s \| 78304 ko \| Util/Tactics/DestructHyps.vo \| 0m00.04s \| 78264 ko \|\| +0m00.00s \|\| 40 ko \| +0.00% \| +0.05% 0m00.04s \| 73148 ko \| Util/Tactics/DestructTrivial.vo \| 0m00.03s \| 73084 ko \|\| +0m00.01s \|\| 64 ko \| +33.33% \| +0.08% 0m00.04s \| 77284 ko \| Util/Tactics/DoWithHyp.vo \| 0m00.05s \| 77192 ko \|\| -0m00.01s \|\| 92 ko \| -20.00% \| +0.11% 0m00.04s \| 76660 ko \| Util/Tactics/ETransitivity.vo \| 0m00.05s \| 76380 ko \|\| -0m00.01s \|\| 280 ko \| -20.00% \| +0.36% 0m00.04s \| 73484 ko \| Util/Tactics/Forward.vo \| 0m00.04s \| 73268 ko \|\| +0m00.00s \|\| 216 ko \| +0.00% \| +0.29% 0m00.04s \| 72540 ko \| Util/Tactics/GetGoal.vo \| 0m00.02s \| 72732 ko \|\| +0m00.02s \|\| -192 ko \| +100.00% \| -0.26% 0m00.04s \| 72784 ko \| Util/Tactics/HasBody.vo \| 0m00.02s \| 72744 ko \|\| +0m00.02s \|\| 40 ko \| +100.00% \| +0.05% 0m00.04s \| 76948 ko \| Util/Tactics/Head.vo \| 0m00.06s \| 76936 ko \|\| -0m00.01s \|\| 12 ko \| -33.33% \| +0.01% 0m00.04s \| 85300 ko \| Util/Tactics/MoveLetIn.vo \| 0m00.06s \| 85512 ko \|\| -0m00.01s \|\| -212 ko \| -33.33% \| -0.24% 0m00.04s \| 72788 ko \| Util/Tactics/Revert.vo \| 0m00.02s \| 72932 ko \|\| +0m00.02s \|\| -144 ko \| +100.00% \| -0.19% 0m00.04s \| 73296 ko \| Util/Tactics/SimplifyRepeatedIfs.vo \| 0m00.01s \| 73164 ko \|\| +0m00.03s \|\| 132 ko \| +300.00% \| +0.18% 0m00.04s \| 75328 ko \| tests/RegressionTests.vo \| 0m00.04s \| 75228 ko \|\| +0m00.00s \|\| 100 ko \| +0.00% \| +0.13% 0m00.04s \| 81468 ko \| tests/coqpl_2021.vo \| 0m00.05s \| 81584 ko \|\| -0m00.01s \|\| -116 ko \| -20.00% \| -0.14% 0m00.03s \| 69224 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/bedrock2/src/bedrock2/Markers.vo \| 0m00.03s \| 68996 ko \|\| +0m00.00s \|\| 228 ko \| +0.00% \| +0.33% 0m00.03s \| 68628 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/eqexact.vo \| 0m00.03s \| 68492 ko \|\| +0m00.00s \|\| 136 ko \| +0.00% \| +0.19% 0m00.03s \| 68528 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Datatypes/PrimitivePair.vo \| 0m00.04s \| 68836 ko \|\| -0m00.01s \|\| -308 ko \| -25.00% \| -0.44% 0m00.03s \| 67916 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/letexists.vo \| 0m00.00s \| 67412 ko \|\| +0m00.03s \|\| 504 ko \| ∞ \| +0.74% 0m00.03s \| 68508 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/ltac_list_ops.vo \| 0m00.04s \| 68412 ko \|\| -0m00.01s \|\| 96 ko \| -25.00% \| +0.14% 0m00.03s \| 69344 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/syntactic_unify.vo \| 0m00.03s \| 69348 ko \|\| +0m00.00s \|\| -4 ko \| +0.00% \| -0.00% 0m00.03s \| 66952 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/dlet.vo \| 0m00.03s \| 67180 ko \|\| +0m00.00s \|\| -228 ko \| +0.00% \| -0.33% 0m00.03s \| 76752 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/PowerFunc.vo \| 0m00.02s \| 76756 ko \|\| +0m00.00s \|\| -4 ko \| +49.99% \| -0.00% 0m00.03s \| 81276 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/runsToNonDet.vo \| 0m00.05s \| 81192 ko \|\| -0m00.02s \|\| 84 ko \| -40.00% \| +0.10% 0m00.03s \| 70340 ko \| Lens.vo \| 0m00.01s \| 70160 ko \|\| +0m00.01s \|\| 180 ko \| +199.99% \| +0.25% 0m00.03s \| 78240 ko \| Rewriter/Util/CPSNotations.vo \| 0m00.02s \| 78028 ko \|\| +0m00.00s \|\| 212 ko \| +49.99% \| +0.27% 0m00.03s \| 69556 ko \| Rewriter/Util/Tactics/CPSId.vo \| 0m00.02s \| 69376 ko \|\| +0m00.00s \|\| 180 ko \| +49.99% \| +0.25% 0m00.03s \| 69628 ko \| Rewriter/Util/Tactics/CacheTerm.vo \| 0m00.04s \| 69632 ko \|\| -0m00.01s \|\| -4 ko \| -25.00% \| -0.00% 0m00.03s \| 72896 ko \| Rewriter/Util/Tactics/DestructHyps.vo \| 0m00.04s \| 72532 ko \|\| -0m00.01s \|\| 364 ko \| -25.00% \| +0.50% 0m00.03s \| 71764 ko \| Rewriter/Util/Tactics/HeadUnderBinders.vo \| 0m00.03s \| 71600 ko \|\| +0m00.00s \|\| 164 ko \| +0.00% \| +0.22% 0m00.03s \| 67284 ko \| Rewriter/Util/Tactics/SetEvars.vo \| 0m00.01s \| 67520 ko \|\| +0m00.01s \|\| -236 ko \| +199.99% \| -0.34% 0m00.03s \| 68440 ko \| Rewriter/Util/Tactics/SetoidSubst.vo \| 0m00.03s \| 68712 ko \|\| +0m00.00s \|\| -272 ko \| +0.00% \| -0.39% 0m00.03s \| 67400 ko \| Rewriter/Util/plugins/StrategyTactic.vo \| 0m00.03s \| 67344 ko \|\| +0m00.00s \|\| 56 ko \| +0.00% \| +0.08% 0m00.03s \| 84040 ko \| Util/CPSNotations.vo \| 0m00.05s \| 84008 ko \|\| -0m00.02s \|\| 32 ko \| -40.00% \| +0.03% 0m00.03s \| 73096 ko \| Util/DefaultedTypes.vo \| 0m00.05s \| 73020 ko \|\| -0m00.02s \|\| 76 ko \| -40.00% \| +0.10% 0m00.03s \| 91576 ko \| Util/IffT.vo \| 0m00.04s \| 91528 ko \|\| -0m00.01s \|\| 48 ko \| -25.00% \| +0.05% 0m00.03s \| 92040 ko \| Util/Logic.vo \| 0m00.05s \| 91868 ko \|\| -0m00.02s \|\| 172 ko \| -40.00% \| +0.18% 0m00.03s \| 74204 ko \| Util/Pos.vo \| 0m00.01s \| 74204 ko \|\| +0m00.01s \|\| 0 ko \| +199.99% \| +0.00% 0m00.03s \| 76836 ko \| Util/Tactics/AppendUnderscores.vo \| 0m00.07s \| 76964 ko \|\| -0m00.04s \|\| -128 ko \| -57.14% \| -0.16% 0m00.03s \| 73164 ko \| Util/Tactics/ChangeInAll.vo \| 0m00.01s \| 72888 ko \|\| +0m00.01s \|\| 276 ko \| +199.99% \| +0.37% 0m00.03s \| 72728 ko \| Util/Tactics/ESpecialize.vo \| 0m00.01s \| 72856 ko \|\| +0m00.01s \|\| -128 ko \| +199.99% \| -0.17% 0m00.03s \| 72824 ko \| Util/Tactics/EvarNormalize.vo \| 0m00.04s \| 73104 ko \|\| -0m00.01s \|\| -280 ko \| -25.00% \| -0.38% 0m00.03s \| 77000 ko \| Util/Tactics/FindHyp.vo \| 0m00.04s \| 77128 ko \|\| -0m00.01s \|\| -128 ko \| -25.00% \| -0.16% 0m00.03s \| 77412 ko \| Util/Tactics/HeadUnderBinders.vo \| 0m00.04s \| 77056 ko \|\| -0m00.01s \|\| 356 ko \| -25.00% \| +0.46% 0m00.03s \| 73108 ko \| Util/Tactics/NormalizeCommutativeIdentifier.vo \| 0m00.03s \| 73064 ko \|\| +0m00.00s \|\| 44 ko \| +0.00% \| +0.06% 0m00.03s \| 72652 ko \| Util/Tactics/OnSubterms.vo \| 0m00.02s \| 72696 ko \|\| +0m00.00s \|\| -44 ko \| +49.99% \| -0.06% 0m00.03s \| 72724 ko \| Util/Tactics/SideConditionsBeforeToAfter.vo \| 0m00.04s \| 72856 ko \|\| -0m00.01s \|\| -132 ko \| -25.00% \| -0.18% 0m00.03s \| 77036 ko \| Util/Tactics/SpecializeAllWays.vo \| 0m00.04s \| 77108 ko \|\| -0m00.01s \|\| -72 ko \| -25.00% \| -0.09% 0m00.03s \| 78344 ko \| Util/Tactics/SplitInContext.vo \| 0m00.02s \| 78528 ko \|\| +0m00.00s \|\| -184 ko \| +49.99% \| -0.23% 0m00.03s \| 72768 ko \| Util/Tactics/SubstEvars.vo \| 0m00.03s \| 72584 ko \|\| +0m00.00s \|\| 184 ko \| +0.00% \| +0.25% 0m00.03s \| 73516 ko \| Util/Tactics/TransparentAssert.vo \| 0m00.04s \| 73748 ko \|\| -0m00.01s \|\| -232 ko \| -25.00% \| -0.31% 0m00.03s \| 73460 ko \| Util/Tactics/VM.vo \| 0m00.03s \| 73528 ko \|\| +0m00.00s \|\| -68 ko \| +0.00% \| -0.09% 0m00.03s \| 69260 ko \| tests/LensTests.vo \| 0m00.04s \| 69296 ko \|\| -0m00.01s \|\| -36 ko \| -25.00% \| -0.05% 0m00.03s \| 73248 ko \| tests/PrintingTests.vo \| 0m00.05s \| 73288 ko \|\| -0m00.02s \|\| -40 ko \| -40.00% \| -0.05% 0m00.03s \| 70184 ko \| tests/ReadmeExampleTests.vo \| 0m00.03s \| 69948 ko \|\| +0m00.00s \|\| 236 ko \| +0.00% \| +0.33% 0m00.02s \| 68444 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/compiler/src/compiler/util/LogGoal.vo \| 0m00.04s \| 68380 ko \|\| -0m00.02s \|\| 64 ko \| -50.00% \| +0.09% 0m00.02s \| 66688 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Macros/subst.vo \| 0m00.04s \| 66688 ko \|\| -0m00.02s \|\| 0 ko \| -50.00% \| +0.00% 0m00.02s \| 67316 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/autoforward.vo \| 0m00.04s \| 67140 ko \|\| -0m00.02s \|\| 176 ko \| -50.00% \| +0.26% 0m00.02s \| 67360 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/rdelta.vo \| 0m00.03s \| 67060 ko \|\| -0m00.00s \|\| 300 ko \| -33.33% \| +0.44% 0m00.02s \| 68208 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/Tactics/simpl_rewrite.vo \| 0m00.05s \| 68312 ko \|\| -0m00.03s \|\| -104 ko \| -60.00% \| -0.15% 0m00.02s \| 68632 ko \| Coqprime/Tactic/Tactic.vo \| 0m00.03s \| 68652 ko \|\| -0m00.00s \|\| -20 ko \| -33.33% \| -0.02% 0m00.02s \| 66900 ko \| RecordUpdate.vo \| 0m00.03s \| 66884 ko \|\| -0m00.00s \|\| 16 ko \| -33.33% \| +0.02% 0m00.02s \| 66964 ko \| Rewriter/Util/GlobalSettings.vo \| 0m00.02s \| 67024 ko \|\| +0m00.00s \|\| -60 ko \| +0.00% \| -0.08% 0m00.02s \| 86400 ko \| Rewriter/Util/IffT.vo \| 0m00.06s \| 86240 ko \|\| -0m00.03s \|\| 160 ko \| -66.66% \| +0.18% 0m00.02s \| 70784 ko \| Rewriter/Util/InductiveHList.vo \| 0m00.05s \| 70648 ko \|\| -0m00.03s \|\| 136 ko \| -60.00% \| +0.19% 0m00.02s \| 67332 ko \| Rewriter/Util/Tactics/Contains.vo \| 0m00.01s \| 67384 ko \|\| +0m00.01s \|\| -52 ko \| +100.00% \| -0.07% 0m00.02s \| 67388 ko \| Rewriter/Util/Tactics/EvarNormalize.vo \| 0m00.02s \| 67472 ko \|\| +0m00.00s \|\| -84 ko \| +0.00% \| -0.12% 0m00.02s \| 67368 ko \| Rewriter/Util/Tactics/GetGoal.vo \| 0m00.03s \| 67516 ko \|\| -0m00.00s \|\| -148 ko \| -33.33% \| -0.21% 0m00.02s \| 67532 ko \| Rewriter/Util/Tactics/PrintContext.vo \| 0m00.02s \| 67608 ko \|\| +0m00.00s \|\| -76 ko \| +0.00% \| -0.11% 0m00.02s \| 71624 ko \| Rewriter/Util/Tactics/SpecializeAllWays.vo \| 0m00.02s \| 71620 ko \|\| +0m00.00s \|\| 4 ko \| +0.00% \| +0.00% 0m00.02s \| 67724 ko \| Rewriter/Util/Tactics/WarnIfGoalsRemain.vo \| 0m00.03s \| 67436 ko \|\| -0m00.00s \|\| 288 ko \| -33.33% \| +0.42% 0m00.02s \| 71880 ko \| Util/GlobalSettings.vo \| 0m00.04s \| 72084 ko \|\| -0m00.02s \|\| -204 ko \| -50.00% \| -0.28% 0m00.02s \| 90820 ko \| Util/Sigma/Lift.vo \| 0m00.04s \| 90652 ko \|\| -0m00.02s \|\| 168 ko \| -50.00% \| +0.18% 0m00.02s \| 75064 ko \| Util/Tactics/CPSId.vo \| 0m00.07s \| 74956 ko \|\| -0m00.05s \|\| 108 ko \| -71.42% \| +0.14% 0m00.02s \| 77196 ko \| Util/Tactics/ClearHead.vo \| 0m00.04s \| 77192 ko \|\| -0m00.02s \|\| 4 ko \| -50.00% \| +0.00% 0m00.02s \| 72704 ko \| Util/Tactics/ClearbodyAll.vo \| 0m00.02s \| 72716 ko \|\| +0m00.00s \|\| -12 ko \| +0.00% \| -0.01% 0m00.02s \| 73372 ko \| Util/Tactics/ConvoyDestruct.vo \| 0m00.05s \| 73608 ko \|\| -0m00.03s \|\| -236 ko \| -60.00% \| -0.32% 0m00.02s \| 72964 ko \| Util/Tactics/EvarExists.vo \| 0m00.05s \| 72892 ko \|\| -0m00.03s \|\| 72 ko \| -60.00% \| +0.09% 0m00.02s \| 72860 ko \| Util/Tactics/PoseTermWithName.vo \| 0m00.02s \| 72944 ko \|\| +0m00.00s \|\| -84 ko \| +0.00% \| -0.11% 0m00.02s \| 73212 ko \| Util/Tactics/PrintGoal.vo \| 0m00.00s \| 73368 ko \|\| +0m00.02s \|\| -156 ko \| ∞ \| -0.21% 0m00.02s \| 76848 ko \| Util/Tactics/RunTacticAsConstr.vo \| 0m00.06s \| 77016 ko \|\| -0m00.03s \|\| -168 ko \| -66.66% \| -0.21% 0m00.02s \| 72884 ko \| Util/Tactics/SetEvars.vo \| 0m00.04s \| 72860 ko \|\| -0m00.02s \|\| 24 ko \| -50.00% \| +0.03% 0m00.02s \| 73808 ko \| Util/Tactics/SetoidSubst.vo \| 0m00.03s \| 73960 ko \|\| -0m00.00s \|\| -152 ko \| -33.33% \| -0.20% 0m00.02s \| 77896 ko \| Util/Tactics/SpecializeBy.vo \| 0m00.05s \| 77828 ko \|\| -0m00.03s \|\| 68 ko \| -60.00% \| +0.08% 0m00.02s \| 73300 ko \| Util/Tactics/UnfoldArg.vo \| 0m00.04s \| 73340 ko \|\| -0m00.02s \|\| -40 ko \| -50.00% \| -0.05% 0m00.02s \| 77836 ko \| Util/Tactics/UniquePose.vo \| 0m00.06s \| 78068 ko \|\| -0m00.03s \|\| -232 ko \| -66.66% \| -0.29% 0m00.01s \| 67496 ko \| /home/jgross/fiat-crypto/rupicola/bedrock2/deps/coqutil/src/coqutil/sanity.vo \| 0m00.04s \| 67416 ko \|\| -0m00.03s \|\| 80 ko \| -75.00% \| +0.11% 0m00.01s \| 79360 ko \| Rewriter/Util/Comparison.vo \| 0m00.06s \| 79264 ko \|\| -0m00.05s \|\| 96 ko \| -83.33% \| +0.12% 0m00.01s \| 72120 ko \| Rewriter/Util/Tactics/SpecializeBy.vo \| 0m00.01s \| 72108 ko \|\| +0m00.00s \|\| 12 ko \| +0.00% \| +0.01% 0m00.01s \| 68280 ko \| Rewriter/Util/Tactics/TransparentAssert.vo \| 0m00.04s \| 68096 ko \|\| -0m00.03s \|\| 184 ko \| -75.00% \| +0.27% 0m00.01s \| 74492 ko \| Util/Bool/IsTrue.vo \| 0m00.02s \| 74468 ko \|\| -0m00.01s \|\| 24 ko \| -50.00% \| +0.03% 0m00.01s \| 73728 ko \| Util/Isomorphism.vo \| 0m00.03s \| 73536 ko \|\| -0m00.01s \|\| 192 ko \| -66.66% \| +0.26% 0m00.01s \| 75164 ko \| Util/Tactics/CacheTerm.vo \| 0m00.05s \| 74976 ko \|\| -0m00.04s \|\| 188 ko \| -80.00% \| +0.25% 0m00.01s \| 73004 ko \| Util/Tactics/ClearAll.vo \| 0m00.03s \| 72688 ko \|\| -0m00.01s \|\| 316 ko \| -66.66% \| +0.43% 0m00.01s \| 72524 ko \| Util/Tactics/Test.vo \| 0m00.03s \| 72520 ko \|\| -0m00.01s \|\| 4 ko \| -66.66% \| +0.00% ``` </p> </details>	27 March 2022, 20:56:01 UTC
451a54f	Jason Gross	26 March 2022, 01:15:57 UTC	Bump coq scripts	26 March 2022, 01:15:57 UTC
97e1354	Jason Gross	25 March 2022, 23:29:44 UTC	Bump coq-scripts	25 March 2022, 23:29:44 UTC
f4c7f37	Jason Gross	24 March 2022, 03:34:08 UTC	[CI] [Windows] Use -j2 (#1172) Maybe this will fix the issue in #1170	24 March 2022, 03:34:08 UTC
fd721fe	Pierre Roux	23 March 2022, 19:18:10 UTC	Adapt to coq/coq#15754 (#1168)	23 March 2022, 19:18:10 UTC
cc89488	Joel	22 March 2022, 04:20:11 UTC	added imul-works statement	23 March 2022, 06:57:26 UTC
b949c76	Joel	22 March 2022, 04:16:11 UTC	another test case Unable to unify: [inr [351, 349, 350]] == [inr [103, 108, 110]] Could not unify the values at index 0: [#351, #349, #350] != [#103, #108, #110] index 0: #351 != #103 (slice 0 44, [#345]) != (slice 0 44, [#100]) index 0: #345 != #100 (add 64, [#58, #95, #343]) != (add 64, [#58, #98]) (add 64, [#95, #343]) != (add 64, [#98]) (add 64, [#95, (mul 64, [#95, #331])]) != (add 64, [(mul 64, [#3, #95])]) (add 64, [#95, (mul 64, [#95, (const 4, [])])]) != (add 64, [(mul 64, [#3, #95])]) (add 64, [(or 64, [#91, #93]), (mul 64, [(or 64, [#91, #93]), (const 4, [])])]) != (add 64, [(mul 64, [(const 5, []), (or 64, [#91, #93])])])	23 March 2022, 06:57:26 UTC
e45a176	Joel	22 March 2022, 04:05:24 UTC	adding fail	23 March 2022, 06:57:26 UTC
93ceed7	Jason Gross	22 March 2022, 23:59:12 UTC	Add reveal_at_least, a more clever form of reveal (#1167) Depth determines which indices get expanded, but all references to the same index get expanded if they appear in the output. This is because Joel's latest examples require a rewriting pass that needs either uneven revealing or the ability to check expression equality modulo the dag in the middle of rewriting. https://github.com/mit-plv/fiat-crypto/pull/1134#issuecomment-1075320548 Roughly the issue is that if we want to turn `a + 4 * a` into `5 * a`, we need to reveal enough structure to see `4 * a`, but we need to see that the two instances of `a` are the same (e.g., if `a` is an ExprRef pointing to `b\|c`, and we reveal uniformly, then we need to recognize `b\|c + 4 * a`)	22 March 2022, 23:59:12 UTC
d8b3f3f	Automated Publisher	22 March 2022, 19:23:45 UTC	Automated Rust Crate Version Bump: Tue Mar 22 19:23:45 UTC 2022 6ccc6638716d4632304baf1adbb5c47c3a12ea6f	22 March 2022, 19:23:45 UTC
6ccc663	Jason Gross	22 March 2022, 01:49:47 UTC	Fix `app_consts` Roughly the issue is that app_consts leaves over spurious x * 1 that don't get removed by subsequent passes. c.f. https://github.com/mit-plv/fiat-crypto/pull/1134#issuecomment-1074461171	22 March 2022, 14:55:46 UTC
2f04776	Jason Gross	21 March 2022, 03:40:09 UTC	Slightly nicer proof	22 March 2022, 14:55:46 UTC
af54baf	Jason Gross	21 March 2022, 03:29:06 UTC	Fix proofs	22 March 2022, 14:55:46 UTC
b330c72	Jason Gross	21 March 2022, 02:53:24 UTC	Update src/Assembly/WithBedrock/SymbolicProofs.v	22 March 2022, 14:55:46 UTC
d2426f3	Joel	21 March 2022, 01:13:02 UTC	addeda print_context_and_goal ().	22 March 2022, 14:55:46 UTC
d70c006	Joel	15 March 2022, 23:02:20 UTC	fix semantics of MEM in Assembly-WBedrock	22 March 2022, 14:55:46 UTC
db8eccc	Jason Gross	12 March 2022, 22:02:55 UTC	Finish combines_to proofs	22 March 2022, 14:55:46 UTC
5c84b22	Jason Gross	10 March 2022, 21:39:48 UTC	Finish almost all of the proof of combine_consts	22 March 2022, 14:55:46 UTC
7f954bd	Joel	07 March 2022, 00:05:55 UTC	latest version of 'combines_to'	22 March 2022, 14:55:46 UTC
7f56f4b	Joel	23 February 2022, 01:55:20 UTC	adding rewrite snippet	22 March 2022, 14:55:46 UTC
9947f2a	Joel	21 February 2022, 03:32:46 UTC	Update src/Assembly/WithBedrock/Semantics.v Co-authored-by: Jason Gross <jasongross9@gmail.com>	22 March 2022, 14:55:46 UTC
a19a0c9	Joel	20 February 2022, 23:49:30 UTC	separate cases for printing assembly	22 March 2022, 14:55:46 UTC
0f806aa	Jason Gross	18 February 2022, 04:09:49 UTC	Fix parsing `parse_Z_arith_strict` permits whitespace both before and after, so we were overlapping whitespace patterns.	22 March 2022, 14:55:46 UTC
a67d258	Joel	17 February 2022, 23:55:06 UTC	not printing 1* in the common case	22 March 2022, 14:55:46 UTC
0f234a4	Joel	17 February 2022, 23:52:01 UTC	fix renamed reg in mem-record	22 March 2022, 14:55:46 UTC
97e92ff	Joel	17 February 2022, 23:51:37 UTC	print mem	22 March 2022, 14:55:46 UTC
698b510	Joel	17 February 2022, 20:52:36 UTC	show -> show_REG Co-authored-by: Jason Gross <jasongross9@gmail.com>	22 March 2022, 14:55:46 UTC
fcfd4e8	Joel	17 February 2022, 05:15:24 UTC	fixing mul(z,r) Co-authored-by: Jason Gross <jasongross9@gmail.com>	22 March 2022, 14:55:46 UTC
66d939a	Joel	17 February 2022, 04:14:32 UTC	trying to mulZ z*r	22 March 2022, 14:55:46 UTC
d4d620f	Joel	17 February 2022, 04:04:07 UTC	fixed symtax *->,	22 March 2022, 14:55:46 UTC
6debcdd	Joel	17 February 2022, 04:01:27 UTC	fixed mem-parsing	22 March 2022, 14:55:46 UTC
f52401d	Joel	17 February 2022, 04:00:37 UTC	added comments	22 March 2022, 14:55:46 UTC
b8252e8	Joel	17 February 2022, 01:34:59 UTC	new MEM-structure	22 March 2022, 14:55:46 UTC
27a3289	Joel	17 February 2022, 00:12:37 UTC	showcasing new lea's [reg] (for mov reg, [rsp]) [reg +/- z ] (for mov reg, [rsp +- 0x8], spills to memory) [reg + reg] (for lea reg, [reg + reg], to calculate 2) [z reg] (for lea reg, [2/4/8 * reg], to calculate 2, 4, 8) [reg + z reg] (for lea reg, [reg + 2*reg] to calculat	22 March 2022, 14:55:46 UTC
a203989	Jason Gross	22 March 2022, 14:55:15 UTC	Inline all functions in C, even in clang (#1165) Fixes #1164 Maybe we should do #820?	22 March 2022, 14:55:15 UTC
c148673	Jason Gross	22 March 2022, 05:35:53 UTC	Preserve permissions of generated files when uploading artifacts	22 March 2022, 05:35:53 UTC
4823727	Jason Gross	21 March 2022, 20:35:56 UTC	Improve errors a bit more	22 March 2022, 01:42:28 UTC
5cfb8f7	Jason Gross	21 March 2022, 17:02:02 UTC	Better equivalence checking errors in the face of bad loads	22 March 2022, 01:42:28 UTC
f1ccc4b	dependabot[bot]	21 March 2022, 21:41:11 UTC	Bump rupicola from `60180c1` to `f5fbc4e` (#1162)	21 March 2022, 21:41:11 UTC
708ec6b	Jason Gross	18 March 2022, 21:11:37 UTC	Parameterize over dereference_scalar in more places This will allow us to reuse the same code to load inputs and outputs, when we want to enforce the spec of reading back and removing all of the values and then saying that the resulting symbolic memory state is empty. Some of the proofs are not quite as complete as they were before, but I hope to replace them soon with a more principled approach.	21 March 2022, 13:10:12 UTC
1da0c9d	Jason Gross	20 March 2022, 21:55:36 UTC	Add revert_until	21 March 2022, 13:10:12 UTC
e1a4b62	Jason Gross	20 March 2022, 19:38:26 UTC	Fix for Coq 8.11	21 March 2022, 02:17:47 UTC
a6b4d85	Jason Gross	15 March 2022, 17:47:13 UTC	Split off the non-bedrock-dependent part of equiv proofs This will hopefully make development a bit faster; these files are so long.	21 March 2022, 02:17:47 UTC
f7bc9e1	dependabot[bot]	18 March 2022, 21:03:47 UTC	Bump rewriter from `3fc0c44` to `10c6a00` (#1160)	18 March 2022, 21:03:47 UTC
93defd9	dependabot[bot]	17 March 2022, 21:09:27 UTC	Bump etc/coq-scripts from `3be05c7` to `7e68a28` (#1159)	17 March 2022, 21:09:27 UTC
37cfe57	Jason Gross	13 March 2022, 00:03:11 UTC	Add some concat lemmas	13 March 2022, 00:03:11 UTC
8e98e20	Jason Gross	10 March 2022, 23:45:30 UTC	Add some lemmas about Forall2 and concat	10 March 2022, 23:45:30 UTC
f43ed26	Jason Gross	10 March 2022, 23:04:05 UTC	Add filter util	10 March 2022, 23:04:05 UTC
0a192c9	Jason Gross	10 March 2022, 21:42:19 UTC	Add partition_eq_filter	10 March 2022, 21:42:40 UTC
a67a862	dependabot[bot]	10 March 2022, 20:52:09 UTC	Bump rupicola from `aa662e1` to `60180c1` (#1155)	10 March 2022, 20:52:09 UTC
974ba64	dependabot[bot]	10 March 2022, 20:02:19 UTC	Bump coqprime from `24f4101` to `de0c48a` (#1156)	10 March 2022, 20:02:19 UTC
6b0f0c6	dependabot[bot]	09 March 2022, 21:24:49 UTC	Bump coqprime from `b984180` to `24f4101` (#1153)	09 March 2022, 21:24:49 UTC
b8cd846	dependabot[bot]	09 March 2022, 20:47:39 UTC	Bump rupicola from `98f70f7` to `aa662e1` (#1152)	09 March 2022, 20:47:39 UTC
b6ef305	Samuel Gruetter	09 March 2022, 04:19:39 UTC	bump rupicola/bedrock2 (#1151)	09 March 2022, 04:19:39 UTC
bf30d11	dependabot[bot]	04 March 2022, 20:30:57 UTC	Bump actions/upload-artifact from 2.3.1 to 3 (#1149)	04 March 2022, 20:30:57 UTC
e7616fd	dependabot[bot]	03 March 2022, 21:13:54 UTC	Bump rupicola from `d66e50e` to `e248b81` (#1148)	03 March 2022, 21:13:54 UTC
bac2325	dependabot[bot]	03 March 2022, 20:47:13 UTC	Bump rewriter from `5ca81b1` to `3fc0c44` (#1147)	03 March 2022, 20:47:13 UTC
5dd14e1	dependabot[bot]	03 March 2022, 16:27:59 UTC	Bump actions/checkout from 2 to 3 (#1146)	03 March 2022, 16:27:59 UTC
df77590	Andres Erbsen	02 March 2022, 15:14:07 UTC	admit riscv_word_ok instance	02 March 2022, 15:14:07 UTC
168bcc9	Andres Erbsen	02 March 2022, 12:43:24 UTC	X25519: use specs of from_wrod,cswap,copy	02 March 2022, 13:18:35 UTC
e53e02b	Jade Philipoom	05 December 2021, 18:19:53 UTC	finish proof about compiler output and factor out remaining admits WIP, working on compiler proof compiler proof statement wip separating proof WIP wip, changed ext_spec in field25519 to be parameterized wip finish proof about compiler output and factor out remaining admits	02 March 2022, 12:47:00 UTC
514951e	Andres Erbsen	02 March 2022, 01:26:54 UTC	update output-tests/Crypto.Bedrock.Group.ScalarMult.MontgomeryLadder.montladder_body.expected	02 March 2022, 12:05:52 UTC
01b94d9	Andres Erbsen	23 February 2022, 21:00:42 UTC	rm src/Bedrock/Field/Interface/Compilation.v	02 March 2022, 12:05:52 UTC
433c56e	Andres Erbsen	22 February 2022, 19:57:12 UTC	integrate from_word and cswap with montledder	02 March 2022, 12:05:52 UTC
33af4d1	Andres Erbsen	17 January 2022, 00:26:20 UTC	thread through admitted fe25519_copy	02 March 2022, 12:05:52 UTC
46dbcef	Andres Erbsen	15 January 2022, 20:29:54 UTC	Hint Rewrite @eval_cons weight_multiples : push_eval	02 March 2022, 12:05:52 UTC
4390cb9	dependabot[bot]	28 February 2022, 21:42:57 UTC	Bump actions/setup-python from 2.3.2 to 3 (#1144)	28 February 2022, 21:42:57 UTC
72a46b7	dependabot[bot]	28 February 2022, 20:02:02 UTC	Bump actions/setup-go from 2.2.0 to 3 (#1143)	28 February 2022, 20:02:02 UTC
c9172da	Jason Gross	25 February 2022, 18:57:19 UTC	Finish SymbolicProofs proof of shlx	28 February 2022, 00:25:04 UTC
1607562	Joel	21 February 2022, 23:01:52 UTC	added import to Tactics.WarnIfGoalsRemain.	28 February 2022, 00:25:04 UTC
5e92f66	Joel	21 February 2022, 21:37:45 UTC	Update src/Assembly/WithBedrock/SymbolicProofs.v Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
aa7d354	Joel	21 February 2022, 04:33:58 UTC	adding `Show.`	28 February 2022, 00:25:04 UTC
d191296	Joel	21 February 2022, 00:00:10 UTC	adding Unshelve, to see the remaining goals in the CI	28 February 2022, 00:25:04 UTC
05d1f6f	Joel	18 February 2022, 06:21:07 UTC	simplify	28 February 2022, 00:25:04 UTC
6f7f38d	Joel	18 February 2022, 06:11:52 UTC	'most' infix...	28 February 2022, 00:25:04 UTC
b25d3f1	Joel	18 February 2022, 06:05:28 UTC	negb rather than Z.z2b	28 February 2022, 00:25:04 UTC
0c700c3	Joel	18 February 2022, 05:01:52 UTC	z2b'ing it back to be able to call SetFlag	28 February 2022, 00:25:04 UTC
44ed466	Joel	18 February 2022, 04:25:29 UTC	using B2z to convert bool -> Z	28 February 2022, 00:25:04 UTC
ae98890	Joel	17 February 2022, 23:58:08 UTC	remove space	28 February 2022, 00:25:04 UTC
970f3b4	Joel	17 February 2022, 23:29:45 UTC	adding `shl,_` and `shlx,_` in DenoteNormalInstruction	28 February 2022, 00:25:04 UTC
6739378	Joel	17 February 2022, 20:57:45 UTC	xor -> lxor Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
6bac53a	Joel	17 February 2022, 03:33:25 UTC	showcasing shlx-by-2 to multiply-by-2-twice	28 February 2022, 00:25:04 UTC
25bcfb8	Joel	17 February 2022, 03:29:20 UTC	fix correctness. x10 was missing	28 February 2022, 00:25:04 UTC
d278fb7	Joel	17 February 2022, 03:18:42 UTC	moving shift to mul before flatten assoc	28 February 2022, 00:25:04 UTC
48917a3	Joel	17 February 2022, 03:15:22 UTC	amending existing file fo showcase shlx/shl to mul	28 February 2022, 00:25:04 UTC
e93e29a	Joel	17 February 2022, 03:10:00 UTC	move showcase (22 != *4) to existing file	28 February 2022, 00:25:04 UTC
59af4d4	Joel	17 February 2022, 03:06:08 UTC	moving to other PR	28 February 2022, 00:25:04 UTC
4937bbb	Joel	17 February 2022, 01:51:21 UTC	resolve syntax err. Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
7fb8749	Joel	17 February 2022, 01:45:28 UTC	remove space Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
8182d88	Joel	17 February 2022, 01:44:20 UTC	Update src/Assembly/Syntax.v Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
49727ae	Joel	17 February 2022, 01:44:13 UTC	Update src/Assembly/Parse.v Co-authored-by: Jason Gross <jasongross9@gmail.com>	28 February 2022, 00:25:04 UTC
46b1cf3	Joel	17 February 2022, 01:51:41 UTC	using cnt' instead of cnt	28 February 2022, 00:25:04 UTC
2a5e8f6	Jason Gross	17 February 2022, 01:11:44 UTC	Fix shift_to_mul definition and proof We need to truncate the expression when there's a bitwidth to truncate it to	28 February 2022, 00:25:04 UTC
3c1358e	Joel	16 February 2022, 23:46:21 UTC	adding shl->mul rewrite	28 February 2022, 00:25:04 UTC

Newer
Older