From ee8fca9889868f19c0a5ab38927d592d10040986 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Mar 2025 20:26:01 -0800 Subject: [PATCH] Full timing diff for: Use Listable to prove equality of registers and opcodes (#2020) This is much faster, especially as we add more registers and opcodes Timing diff seems to be mostly noise, except for the 85% time decrease in Assembly/Syntax.vo
Timing Diff

``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 238m06.36s | 2820232 ko | Total Time / Peak Mem | 238m08.20s | 2820076 ko || -0m01.83s || 156 ko | -0.01% | +0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 77m10.48s | 417044 ko | fiat-amd64/p434-mul.status | 75m28.97s | 417220 ko || +1m41.50s || -176 ko | +2.24% | -0.04% 64m06.25s | 365376 ko | fiat-amd64/p434-square.status | 65m40.64s | 376592 ko || -1m34.38s || -11216 ko | -2.39% | -2.97% 7m12.38s | 99668 ko | fiat-amd64/p384-mul.status | 7m32.67s | 97048 ko || -0m20.29s || 2620 ko | -4.48% | +2.69% 0m01.60s | 427080 ko | Assembly/Syntax.vo | 0m10.79s | 694672 ko || -0m09.18s || -267592 ko | -85.17% | -38.52% 2m09.25s | 2388212 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.vo | 2m00.80s | 2385948 ko || +0m08.45s || 2264 ko | +6.99% | +0.09% 0m24.32s | 906976 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m19.63s | 905608 ko || +0m04.69s || 1368 ko | +23.89% | +0.15% 2m16.38s | 1983744 ko | Rewriter/Passes/ArithWithCasts.vo | 2m13.56s | 1926736 ko || +0m02.81s || 57008 ko | +2.11% | +2.95% 1m20.75s | 795352 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExpr.vo | 1m23.09s | 799756 ko || -0m02.34s || -4404 ko | -2.81% | -0.55% 0m47.32s | 1318412 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 0m49.33s | 1319436 ko || -0m02.00s || -1024 ko | -4.07% | -0.07% 0m45.86s | 585020 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.vo | 0m47.87s | 582700 ko || -0m02.00s || 2320 ko | -4.19% | +0.39% 0m36.79s | 754024 ko | rupicola/bedrock2/compiler/src/compiler/MMIO.vo | 0m34.38s | 755868 ko || +0m02.40s || -1844 ko | +7.00% | -0.24% 0m36.58s | 1065048 ko | Rewriter/Passes/Arith.vo | 0m34.04s | 1065324 ko || +0m02.53s || -276 ko | +7.46% | -0.02% 0m31.21s | 1856352 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m29.20s | 1856104 ko || +0m02.01s || 248 ko | +6.88% | +0.01% 0m20.99s | 883976 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m18.86s | 886684 ko || +0m02.12s || -2708 ko | +11.29% | -0.30% 0m15.28s | 677156 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m17.58s | 676088 ko || -0m02.29s || 1068 ko | -13.08% | +0.15% 0m14.27s | 573132 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI64.vo | 0m11.67s | 573136 ko || +0m02.59s || -4 ko | +22.27% | -0.00% 0m09.77s | 513268 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA64.vo | 0m12.18s | 514516 ko || -0m02.41s || -1248 ko | -19.78% | -0.24% 0m08.40s | 561800 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m05.95s | 561412 ko || +0m02.45s || 388 ko | +41.17% | +0.06% 0m07.76s | 448060 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM64.vo | 0m05.58s | 448180 ko || +0m02.17s || -120 ko | +39.06% | -0.02% 2m39.12s | 888848 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.vo | 2m37.75s | 889736 ko || +0m01.37s || -888 ko | +0.86% | -0.09% 1m16.92s | 66464 ko | fiat-amd64/p448_solinas-carry_mul.status | 1m15.17s | 68056 ko || +0m01.75s || -1592 ko | +2.32% | -2.33% 0m58.12s | 1074880 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 0m57.11s | 1073384 ko || +0m01.00s || 1496 ko | +1.76% | +0.13% 0m42.64s | 1083548 ko | Rewriter/Rewriter/Examples.vo | 0m44.61s | 1081328 ko || -0m01.96s || 2220 ko | -4.41% | +0.20% 0m41.39s | 2820232 ko | ExtractionOCaml/WithBedrock/fiat_crypto | 0m39.72s | 2820028 ko || +0m01.67s || 204 ko | +4.20% | +0.00% 0m37.03s | 40036 ko | fiat-amd64/secp256k1_montgomery-mul.status | 0m38.03s | 39932 ko || -0m01.00s || 104 ko | -2.62% | +0.26% 0m34.75s | 999824 ko | Rewriter/Passes/MultiRetSplit.vo | 0m35.80s | 997900 ko || -0m01.04s || 1924 ko | -2.93% | +0.19% 0m32.67s | 1855664 ko | ExtractionOCaml/unsaturated_solinas | 0m31.02s | 1855396 ko || +0m01.65s || 268 ko | +5.31% | +0.01% 0m32.26s | 1855536 ko | ExtractionOCaml/solinas_reduction | 0m33.50s | 1855860 ko || -0m01.24s || -324 ko | -3.70% | -0.01% 0m30.94s | 1856096 ko | ExtractionOCaml/bedrock2_base_conversion | 0m29.22s | 1852000 ko || +0m01.72s || 4096 ko | +5.88% | +0.22% 0m29.76s | 1855416 ko | ExtractionOCaml/saturated_solinas | 0m28.05s | 1616204 ko || +0m01.71s || 239212 ko | +6.09% | +14.80% 0m29.25s | 1856068 ko | ExtractionOCaml/WithBedrock/unsaturated_solinas | 0m30.51s | 1833680 ko || -0m01.26s || 22388 ko | -4.12% | +1.22% 0m29.22s | 1616952 ko | ExtractionOCaml/WithBedrock/dettman_multiplication | 0m30.31s | 1617108 ko || -0m01.08s || -156 ko | -3.59% | -0.00% 0m29.20s | 1616592 ko | ExtractionOCaml/WithBedrock/saturated_solinas | 0m30.42s | 1616836 ko || -0m01.22s || -244 ko | -4.01% | -0.01% 0m26.05s | 537276 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeBound.vo | 0m24.99s | 535468 ko || +0m01.06s || 1808 ko | +4.24% | +0.33% 0m18.86s | 575976 ko | Stringification/IR.vo | 0m17.55s | 578168 ko || +0m01.30s || -2192 ko | +7.46% | -0.37% 0m10.13s | 570076 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m09.00s | 569848 ko || +0m01.13s || 228 ko | +12.55% | +0.04% 0m10.05s | 530892 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m08.96s | 529964 ko || +0m01.08s || 928 ko | +12.16% | +0.17% 0m09.29s | 531060 ko | Util/FSets/FMapSum.vo | 0m10.75s | 527476 ko || -0m01.46s || 3584 ko | -13.58% | +0.67% 0m07.33s | 450684 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/BenchCancel256.vo | 0m05.59s | 451748 ko || +0m01.74s || -1064 ko | +31.12% | -0.23% 0m05.76s | 508092 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m04.73s | 507572 ko || +0m01.02s || 520 ko | +21.77% | +0.10% 6m32.54s | 96452 ko | fiat-amd64/p384-square.status | 6m33.35s | 97592 ko || -0m00.81s || -1140 ko | -0.20% | -1.16% 1m50.50s | 1792976 ko | Rewriter/Passes/NBE.vo | 1m49.69s | 1801984 ko || +0m00.81s || -9008 ko | +0.73% | -0.49% 1m28.73s | 69788 ko | fiat-amd64/p521-carry_mul.status | 1m28.90s | 71128 ko || -0m00.17s || -1340 ko | -0.19% | -1.88% 1m10.42s | 1478516 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m09.58s | 1478164 ko || +0m00.84s || 352 ko | +1.20% | +0.02% 1m04.10s | 753988 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.vo | 1m04.72s | 749336 ko || -0m00.62s || 4652 ko | -0.95% | +0.62% 1m01.52s | 690572 ko | Rewriter/RulesProofs.vo | 1m02.41s | 691060 ko || -0m00.88s || -488 ko | -1.42% | -0.07% 0m50.59s | 876060 ko | Util/FSets/FMapTrie.vo | 0m50.73s | 878052 ko || -0m00.13s || -1992 ko | -0.27% | -0.22% 0m46.58s | 2384944 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml | 0m45.89s | 2424644 ko || +0m00.68s || -39700 ko | +1.50% | -1.63% 0m46.03s | 2385620 ko | ExtractionOCaml/WithBedrock/fiat_crypto.ml | 0m46.56s | 2424440 ko || -0m00.53s || -38820 ko | -1.13% | -1.60% 0m44.76s | 785900 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 0m45.65s | 785868 ko || -0m00.89s || 32 ko | -1.94% | +0.00% 0m44.37s | 2232888 ko | ExtractionOCaml/fiat_crypto.ml | 0m44.26s | 2226148 ko || +0m00.10s || 6740 ko | +0.24% | +0.30% 0m43.98s | 685468 ko | Arithmetic/SolinasReduction.vo | 0m44.07s | 683264 ko || -0m00.09s || 2204 ko | -0.20% | +0.32% 0m40.76s | 2820076 ko | ExtractionOCaml/bedrock2_fiat_crypto | 0m40.37s | 2820076 ko || +0m00.39s || 0 ko | +0.96% | +0.00% 0m40.74s | 909784 ko | AbstractInterpretation/ZRangeProofs.vo | 0m40.55s | 910860 ko || +0m00.19s || -1076 ko | +0.46% | -0.11% 0m40.12s | 2819340 ko | ExtractionOCaml/fiat_crypto | 0m40.00s | 2819440 ko || +0m00.11s || -100 ko | +0.29% | -0.00% 0m39.68s | 45644 ko | fiat-amd64/p224-mul.status | 0m39.78s | 43292 ko || -0m00.10s || 2352 ko | -0.25% | +5.43% 0m38.71s | 789876 ko | AbstractInterpretation/Wf.vo | 0m39.24s | 788112 ko || -0m00.53s || 1764 ko | -1.35% | +0.22% 0m36.40s | 1477180 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.vo | 0m36.56s | 1475444 ko || -0m00.16s || 1736 ko | -0.43% | +0.11% 0m34.63s | 1856560 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m33.70s | 1874972 ko || +0m00.92s || -18412 ko | +2.75% | -0.98% 0m34.58s | 42156 ko | fiat-amd64/p224-square.status | 0m35.34s | 42720 ko || -0m00.76s || -564 ko | -2.15% | -1.32% 0m34.05s | 662836 ko | rupicola/bedrock2/compiler/src/compiler/Spilling.vo | 0m33.49s | 660024 ko || +0m00.55s || 2812 ko | +1.67% | +0.42% 0m33.59s | 1855268 ko | ExtractionOCaml/word_by_word_montgomery | 0m33.70s | 1855652 ko || -0m00.10s || -384 ko | -0.32% | -0.02% 0m33.59s | 49640 ko | fiat-amd64/p448_solinas-carry_square.status | 0m33.13s | 48328 ko || +0m00.46s || 1312 ko | +1.38% | +2.71% 0m33.58s | 1856236 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m34.11s | 1856348 ko || -0m00.53s || -112 ko | -1.55% | -0.00% 0m33.46s | 1856040 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m32.97s | 1856092 ko || +0m00.49s || -52 ko | +1.48% | -0.00% 0m33.30s | 39492 ko | fiat-amd64/secp256k1_montgomery-square.status | 0m33.34s | 39648 ko || -0m00.04s || -156 ko | -0.11% | -0.39% 0m33.21s | 1019472 ko | Rewriter/Language/Wf.vo | 0m33.02s | 1019596 ko || +0m00.18s || -124 ko | +0.57% | -0.01% 0m32.78s | 1982164 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m32.80s | 2010996 ko || -0m00.01s || -28832 ko | -0.06% | -1.43% 0m32.06s | 1957600 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m31.88s | 1982116 ko || +0m00.18s || -24516 ko | +0.56% | -1.23% 0m31.91s | 47768 ko | fiat-amd64/p521-carry_square.status | 0m31.63s | 48196 ko || +0m00.28s || -428 ko | +0.88% | -0.88% 0m31.10s | 1932084 ko | ExtractionOCaml/solinas_reduction.ml | 0m31.25s | 1913324 ko || -0m00.14s || 18760 ko | -0.47% | +0.98% 0m29.92s | 2160332 ko | ExtractionOCaml/WithBedrock/word_by_word_montgomery | 0m28.93s | 2105412 ko || +0m00.99s || 54920 ko | +3.42% | +2.60% 0m29.86s | 1855312 ko | ExtractionOCaml/dettman_multiplication | 0m29.54s | 1616244 ko || +0m00.32s || 239068 ko | +1.08% | +14.79% 0m29.59s | 1856064 ko | ExtractionOCaml/bedrock2_dettman_multiplication | 0m30.56s | 1856356 ko || -0m00.96s || -292 ko | -3.17% | -0.01% 0m29.51s | 1941896 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m30.03s | 1926792 ko || -0m00.51s || 15104 ko | -1.73% | +0.78% 0m29.21s | 725820 ko | Rewriter/Rewriter/Wf.vo | 0m28.58s | 726480 ko || +0m00.63s || -660 ko | +2.20% | -0.09% 0m29.12s | 1904532 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m28.97s | 1918588 ko || +0m00.15s || -14056 ko | +0.51% | -0.73% 0m29.05s | 695572 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/LAN9250.vo | 0m29.04s | 696216 ko || +0m00.01s || -644 ko | +0.03% | -0.09% 0m28.22s | 1959800 ko | ExtractionOCaml/WithBedrock/word_by_word_montgomery.ml | 0m28.33s | 1982140 ko || -0m00.10s || -22340 ko | -0.38% | -1.12% 0m27.53s | 1855748 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m27.55s | 1865072 ko || -0m00.01s || -9324 ko | -0.07% | -0.49% 0m27.52s | 1855356 ko | ExtractionOCaml/base_conversion | 0m27.84s | 1616404 ko || -0m00.32s || 238952 ko | -1.14% | +14.78% 0m27.33s | 882160 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.vo | 0m26.89s | 881676 ko || +0m00.43s || 484 ko | +1.63% | +0.05% 0m27.32s | 1260196 ko | Assembly/Symbolic.vo | 0m28.04s | 1269368 ko || -0m00.71s || -9172 ko | -2.56% | -0.72% 0m26.46s | 1896048 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml | 0m26.51s | 1912452 ko || -0m00.05s || -16404 ko | -0.18% | -0.85% 0m26.32s | 1616492 ko | ExtractionOCaml/WithBedrock/solinas_reduction | 0m27.27s | 1617100 ko || -0m00.94s || -608 ko | -3.48% | -0.03% 0m26.17s | 1617012 ko | ExtractionOCaml/WithBedrock/base_conversion | 0m26.89s | 1617204 ko || -0m00.71s || -192 ko | -2.67% | -0.01% 0m26.14s | 1906108 ko | ExtractionOCaml/WithBedrock/unsaturated_solinas.ml | 0m26.10s | 1889812 ko || +0m00.03s || 16296 ko | +0.15% | +0.86% 0m26.12s | 1871116 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m25.45s | 1889916 ko || +0m00.67s || -18800 ko | +2.63% | -0.99% 0m25.95s | 834592 ko | Rewriter/Passes/MulSplit.vo | 0m26.75s | 837740 ko || -0m00.80s || -3148 ko | -2.99% | -0.37% 0m25.81s | 672284 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m25.36s | 670376 ko || +0m00.44s || 1908 ko | +1.77% | +0.28% 0m25.55s | 1875840 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m25.53s | 1889564 ko || +0m00.01s || -13724 ko | +0.07% | -0.72% 0m25.00s | 1798452 ko | ExtractionOCaml/dettman_multiplication.ml | 0m25.12s | 1794492 ko || -0m00.12s || 3960 ko | -0.47% | +0.22% 0m25.00s | 1361292 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m24.58s | 1363792 ko || +0m00.42s || -2500 ko | +1.70% | -0.18% 0m24.74s | 720104 ko | Rewriter/Language/UnderLetsProofs.vo | 0m24.84s | 720112 ko || -0m00.10s || -8 ko | -0.40% | -0.00% 0m24.72s | 1769508 ko | ExtractionOCaml/base_conversion.ml | 0m24.65s | 1772020 ko || +0m00.07s || -2512 ko | +0.28% | -0.14% 0m24.42s | 1771988 ko | ExtractionOCaml/saturated_solinas.ml | 0m24.66s | 1788136 ko || -0m00.23s || -16148 ko | -0.97% | -0.90% 0m24.13s | 1352136 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m25.10s | 1350916 ko || -0m00.97s || 1220 ko | -3.86% | +0.09% 0m24.09s | 38248 ko | fiat-amd64/p256-mul.status | 0m23.78s | 38604 ko || +0m00.30s || -356 ko | +1.30% | -0.92% 0m23.80s | 973964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.vo | 0m23.38s | 971940 ko || +0m00.42s || 2024 ko | +1.79% | +0.20% 0m23.29s | 1877608 ko | ExtractionOCaml/WithBedrock/dettman_multiplication.ml | 0m23.11s | 1889940 ko || +0m00.17s || -12332 ko | +0.77% | -0.65% 0m23.11s | 1873460 ko | ExtractionOCaml/WithBedrock/base_conversion.ml | 0m23.11s | 1889972 ko || +0m00.00s || -16512 ko | +0.00% | -0.87% 0m23.09s | 1875588 ko | ExtractionOCaml/WithBedrock/solinas_reduction.ml | 0m23.18s | 1887908 ko || -0m00.08s || -12320 ko | -0.38% | -0.65% 0m22.91s | 1875808 ko | ExtractionOCaml/WithBedrock/saturated_solinas.ml | 0m23.07s | 1889576 ko || -0m00.16s || -13768 ko | -0.69% | -0.72% 0m22.60s | 600116 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m22.01s | 599588 ko || +0m00.58s || 528 ko | +2.68% | +0.08% 0m22.39s | 621748 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/EncodeDecode.vo | 0m23.06s | 622352 ko || -0m00.66s || -604 ko | -2.90% | -0.09% 0m21.77s | 465084 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricSane.vo | 0m20.86s | 465252 ko || +0m00.91s || -168 ko | +4.36% | -0.03% 0m20.92s | 824652 ko | Rewriter/Rewriter/InterpProofs.vo | 0m21.07s | 824932 ko || -0m00.14s || -280 ko | -0.71% | -0.03% 0m20.06s | 1010236 ko | rupicola/bedrock2/compiler/src/compiler/memory_mapped_ext_calls_compiler.vo | 0m20.48s | 1009088 ko || -0m00.42s || 1148 ko | -2.05% | +0.11% 0m19.90s | 721048 ko | Language/IdentifiersGENERATEDProofs.vo | 0m19.15s | 720336 ko || +0m00.75s || 712 ko | +3.91% | +0.09% 0m19.34s | 37156 ko | fiat-amd64/p256-square.status | 0m18.98s | 38964 ko || +0m00.35s || -1808 ko | +1.89% | -4.64% 0m19.32s | 1227656 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.vo | 0m18.83s | 1227836 ko || +0m00.49s || -180 ko | +2.60% | -0.01% 0m18.79s | 741784 ko | Rewriter/Rewriter/ProofsCommon.vo | 0m18.70s | 745572 ko || +0m00.08s || -3788 ko | +0.48% | -0.50% 0m17.59s | 1651528 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m17.98s | 1666020 ko || -0m00.39s || -14492 ko | -2.16% | -0.86% 0m17.55s | 1722236 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m17.62s | 1729168 ko || -0m00.07s || -6932 ko | -0.39% | -0.40% 0m17.06s | 533208 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/kyberslash.vo | 0m16.44s | 534844 ko || +0m00.61s || -1636 ko | +3.77% | -0.30% 0m16.94s | 904916 ko | Language/IdentifiersGENERATED.vo | 0m17.30s | 904416 ko || -0m00.35s || 500 ko | -2.08% | +0.05% 0m16.89s | 659124 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memmove.vo | 0m16.65s | 659564 ko || +0m00.24s || -440 ko | +1.44% | -0.06% 0m15.98s | 622916 ko | rupicola/src/Rupicola/Examples/Utf8/Utf8.vo | 0m15.85s | 627160 ko || +0m00.13s || -4244 ko | +0.82% | -0.67% 0m15.26s | 596900 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvLiterals.vo | 0m15.43s | 597444 ko || -0m00.16s || -544 ko | -1.10% | -0.09% 0m14.97s | 662048 ko | AbstractInterpretation/Proofs.vo | 0m14.96s | 663496 ko || +0m00.00s || -1448 ko | +0.06% | -0.21% 0m14.32s | 581144 ko | rupicola/bedrock2/compiler/src/compiler/RegAlloc.vo | 0m13.86s | 581420 ko || +0m00.46s || -276 ko | +3.31% | -0.04% 0m14.02s | 514152 ko | Arithmetic/WordByWordMontgomery.vo | 0m14.06s | 512124 ko || -0m00.04s || 2028 ko | -0.28% | +0.39% 0m13.97s | 494672 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_66.vo | 0m13.58s | 494916 ko || +0m00.39s || -244 ko | +2.87% | -0.04% 0m12.90s | 543520 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_SB.vo | 0m13.34s | 544228 ko || -0m00.43s || -708 ko | -3.29% | -0.13% 0m12.80s | 476612 ko | Arithmetic/Saturated.vo | 0m12.73s | 476172 ko || +0m00.07s || 440 ko | +0.54% | +0.09% 0m12.21s | 714992 ko | Language/IdentifiersBasicGENERATED.vo | 0m12.87s | 715132 ko || -0m00.65s || -140 ko | -5.12% | -0.01% 0m12.06s | 561348 ko | Rewriter/Language/Inversion.vo | 0m12.00s | 558696 ko || +0m00.06s || 2652 ko | +0.50% | +0.47% 0m11.55s | 578872 ko | Util/FSets/FMapProd.vo | 0m11.67s | 579788 ko || -0m00.11s || -916 ko | -1.02% | -0.15% 0m11.49s | 524736 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FE310CompilerDemo.vo | 0m12.37s | 523304 ko || -0m00.87s || 1432 ko | -7.11% | +0.27% 0m11.23s | 546088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeA.vo | 0m11.28s | 541796 ko || -0m00.04s || 4292 ko | -0.44% | +0.79% 0m10.72s | 772012 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m10.89s | 774044 ko || -0m00.16s || -2032 ko | -1.56% | -0.26% 0m10.41s | 934252 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m10.45s | 935216 ko || -0m00.03s || -964 ko | -0.38% | -0.10% 0m09.75s | 573072 ko | Util/ZUtil/ArithmeticShiftr.vo | 0m09.91s | 573360 ko || -0m00.16s || -288 ko | -1.61% | -0.05% 0m09.73s | 622172 ko | rupicola/bedrock2/compiler/src/compiler/FlatImp.vo | 0m09.95s | 619344 ko || -0m00.21s || 2828 ko | -2.21% | +0.45% 0m09.64s | 921372 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m09.64s | 925888 ko || +0m00.00s || -4516 ko | +0.00% | -0.48% 0m09.10s | 482376 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_UJ.vo | 0m09.62s | 484600 ko || -0m00.51s || -2224 ko | -5.40% | -0.45% 0m08.79s | 494240 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/IPChecksum.vo | 0m08.70s | 489220 ko || +0m00.08s || 5020 ko | +1.03% | +1.02% 0m08.75s | 459868 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl.vo | 0m08.70s | 460160 ko || +0m00.05s || -292 ko | +0.57% | -0.06% 0m08.65s | 436480 ko | Algebra/Field.vo | 0m09.21s | 435284 ko || -0m00.56s || 1196 ko | -6.08% | +0.27% 0m08.61s | 475052 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.vo | 0m08.57s | 474716 ko || +0m00.03s || 336 ko | +0.46% | +0.07% 0m08.59s | 535124 ko | Util/FSets/FMapOption.vo | 0m09.16s | 535928 ko || -0m00.57s || -804 ko | -6.22% | -0.15% 0m08.58s | 515648 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeM.vo | 0m08.35s | 517008 ko || +0m00.23s || -1360 ko | +2.75% | -0.26% 0m08.24s | 478632 ko | rupicola/bedrock2/compiler/src/compiler/RunInstruction.vo | 0m08.03s | 479860 ko || +0m00.21s || -1228 ko | +2.61% | -0.25% 0m08.19s | 559176 ko | Bedrock/Field/Common/Util.vo | 0m08.19s | 558736 ko || +0m00.00s || 440 ko | +0.00% | +0.07% 0m08.15s | 467992 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/SPI.vo | 0m08.43s | 467980 ko || -0m00.27s || 12 ko | -3.32% | +0.00% 0m08.15s | 476648 ko | rupicola/src/Rupicola/Examples/CMove/CMove.vo | 0m08.36s | 473984 ko || -0m00.20s || 2664 ko | -2.51% | +0.56% 0m08.05s | 446704 ko | Util/Structures/Orders/Prod.vo | 0m08.18s | 447056 ko || -0m00.12s || -352 ko | -1.58% | -0.07% 0m07.96s | 467612 ko | rupicola/src/Rupicola/Examples/Arrays.vo | 0m07.96s | 473484 ko || +0m00.00s || -5872 ko | +0.00% | -1.24% 0m07.85s | 468876 ko | rupicola/src/Rupicola/Examples/Loops.vo | 0m07.90s | 468948 ko || -0m00.05s || -72 ko | -0.63% | -0.01% 0m07.65s | 468196 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ct.vo | 0m07.52s | 468940 ko || +0m00.13s || -744 ko | +1.72% | -0.15% 0m07.40s | 558600 ko | Rewriter/Passes/NoSelect.vo | 0m08.21s | 560664 ko || -0m00.81s || -2064 ko | -9.86% | -0.36% 0m07.35s | 691312 ko | Util/ZRange/LandLorBounds.vo | 0m07.15s | 691716 ko || +0m00.19s || -404 ko | +2.79% | -0.05% 0m07.32s | 666144 ko | Rewriter/Demo.vo | 0m07.91s | 666936 ko || -0m00.58s || -792 ko | -7.45% | -0.11% 0m07.23s | 416284 ko | test/TestGoals.vo | 0m07.14s | 416008 ko || +0m00.09s || 276 ko | +1.26% | +0.06% 0m07.10s | 470348 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/uint128_32.vo | 0m06.65s | 468220 ko || +0m00.44s || 2128 ko | +6.76% | +0.45% 0m07.07s | 464848 ko | Arithmetic/Core.vo | 0m07.12s | 463232 ko || -0m00.04s || 1616 ko | -0.70% | +0.34% 0m07.00s | 508044 ko | rupicola/src/Rupicola/Examples/KVStore/Manual.vo | 0m07.27s | 505604 ko || -0m00.26s || 2440 ko | -3.71% | +0.48% 0m06.94s | 447492 ko | Util/Structures/Orders/List.vo | 0m07.12s | 445604 ko || -0m00.17s || 1888 ko | -2.52% | +0.42% 0m06.74s | 449372 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_S.vo | 0m07.01s | 448216 ko || -0m00.26s || 1156 ko | -3.85% | +0.25% 0m06.68s | 474944 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/bsearch.vo | 0m07.43s | 475476 ko || -0m00.75s || -532 ko | -10.09% | -0.11% 0m06.67s | 438404 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add.vo | 0m05.83s | 437468 ko || +0m00.83s || 936 ko | +14.40% | +0.21% 0m06.66s | 448060 ko | Util/ZRange/CornersMonotoneBounds.vo | 0m06.70s | 448036 ko || -0m00.04s || 24 ko | -0.59% | +0.00% 0m06.66s | 424800 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Minimal.vo | 0m07.26s | 426492 ko || -0m00.59s || -1692 ko | -8.26% | -0.39% 0m06.63s | 928996 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m06.59s | 929244 ko || +0m00.04s || -248 ko | +0.60% | -0.02% 0m06.63s | 457972 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/metric_ipow.vo | 0m06.93s | 457816 ko || -0m00.29s || 156 ko | -4.32% | +0.03% 0m06.49s | 671628 ko | rupicola/bedrock2/compiler/src/compiler/FlatToRiscvDef.vo | 0m06.47s | 674128 ko || +0m00.02s || -2500 ko | +0.30% | -0.37% 0m06.33s | 520320 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m06.39s | 522384 ko || -0m00.05s || -2064 ko | -0.93% | -0.39% 0m06.27s | 443108 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R_atomic.vo | 0m05.88s | 441800 ko || +0m00.38s || 1308 ko | +6.63% | +0.29% 0m06.08s | 1039452 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m05.99s | 1038824 ko || +0m00.08s || 628 ko | +1.50% | +0.06% 0m05.99s | 32188 ko | fiat-amd64/curve25519-carry_mul.status | 0m06.00s | 32396 ko || -0m00.00s || -208 ko | -0.16% | -0.64% 0m05.98s | 436264 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.vo | 0m05.89s | 435788 ko || +0m00.09s || 476 ko | +1.52% | +0.10% 0m05.83s | 436452 ko | Algebra/Ring.vo | 0m05.58s | 436384 ko || +0m00.25s || 68 ko | +4.48% | +0.01% 0m05.83s | 435144 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/FlatConstMem.vo | 0m05.43s | 434740 ko || +0m00.40s || 404 ko | +7.36% | +0.09% 0m05.75s | 441968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_Fence.vo | 0m06.09s | 440976 ko || -0m00.33s || 992 ko | -5.58% | +0.22% 0m05.56s | 618780 ko | Util/FSets/FMapTrieEx.vo | 0m05.64s | 617672 ko || -0m00.08s || 1108 ko | -1.41% | +0.17% 0m05.56s | 453984 ko | rupicola/src/Rupicola/Examples/L64X128.vo | 0m05.62s | 457868 ko || -0m00.06s || -3884 ko | -1.06% | -0.84% 0m05.54s | 31116 ko | fiat-amd64/curve25519_solinas-mul.status | 0m05.45s | 30840 ko || +0m00.08s || 276 ko | +1.65% | +0.89% 0m05.30s | 436408 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/stackalloc.vo | 0m04.67s | 436528 ko || +0m00.62s || -120 ko | +13.49% | -0.02% 0m05.20s | 538584 ko | rupicola/bedrock2/compiler/src/compiler/SpillingMapGoals.vo | 0m05.11s | 542404 ko || +0m00.08s || -3820 ko | +1.76% | -0.70% 0m05.11s | 451428 ko | Util/MSets/MSetSum.vo | 0m05.13s | 451660 ko || -0m00.01s || -232 ko | -0.38% | -0.05% 0m05.10s | 821668 ko | PushButtonSynthesis/BaseConversion.vo | 0m05.14s | 825580 ko || -0m00.04s || -3912 ko | -0.77% | -0.47% 0m05.09s | 434600 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZListEqProver.vo | 0m05.14s | 433600 ko || -0m00.04s || 1000 ko | -0.97% | +0.23% 0m05.06s | 542684 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRFile.vo | 0m05.29s | 543956 ko || -0m00.23s || -1272 ko | -4.34% | -0.23% 0m05.02s | 521884 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m04.77s | 520860 ko || +0m00.25s || 1024 ko | +5.24% | +0.19% 0m05.01s | 536840 ko | rupicola/bedrock2/compiler/src/compiler/ToplevelLoop.vo | 0m05.00s | 537256 ko || +0m00.00s || -416 ko | +0.19% | -0.07% 0m04.99s | 424104 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_R.vo | 0m04.48s | 421240 ko || +0m00.50s || 2864 ko | +11.38% | +0.67% 0m04.93s | 468728 ko | MiscCompilerPassesProofs.vo | 0m05.24s | 466776 ko || -0m00.31s || 1952 ko | -5.91% | +0.41% 0m04.87s | 831204 ko | BoundsPipeline.vo | 0m04.92s | 836116 ko || -0m00.04s || -4912 ko | -1.01% | -0.58% 0m04.85s | 518452 ko | Rewriter/Passes/AddAssocLeft.vo | 0m04.24s | 515564 ko || +0m00.60s || 2888 ko | +14.38% | +0.56% 0m04.85s | 480780 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediate.vo | 0m04.85s | 481016 ko || +0m00.00s || -236 ko | +0.00% | -0.04% 0m04.82s | 459512 ko | Util/ZUtil/Modulo.vo | 0m04.78s | 458996 ko || +0m00.04s || 516 ko | +0.83% | +0.11% 0m04.75s | 454452 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memequal.vo | 0m05.09s | 457548 ko || -0m00.33s || -3096 ko | -6.67% | -0.67% 0m04.72s | 512860 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m04.67s | 515796 ko || +0m00.04s || -2936 ko | +1.07% | -0.56% 0m04.64s | 448272 ko | UnsaturatedSolinasHeuristics.vo | 0m04.56s | 448500 ko || +0m00.08s || -228 ko | +1.75% | -0.05% 0m04.60s | 669968 ko | coqutil/Word/Properties.vo | 0m04.63s | 670448 ko || -0m00.03s || -480 ko | -0.64% | -0.07% 0m04.51s | 424188 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_FenceI.vo | 0m04.28s | 421344 ko || +0m00.22s || 2844 ko | +5.37% | +0.67% 0m04.50s | 536924 ko | Language/InversionExtra.vo | 0m04.49s | 536148 ko || +0m00.00s || 776 ko | +0.22% | +0.14% 0m04.46s | 424268 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I.vo | 0m03.98s | 426192 ko || +0m00.48s || -1924 ko | +12.06% | -0.45% 0m04.44s | 427292 ko | Util/ZUtil/LandLorBounds.vo | 0m04.63s | 425828 ko || -0m00.18s || 1464 ko | -4.10% | +0.34% 0m04.42s | 800508 ko | Assembly/Equivalence.vo | 0m05.05s | 807304 ko || -0m00.62s || -6796 ko | -12.47% | -0.84% 0m04.32s | 422288 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_shift_57.vo | 0m04.38s | 420636 ko || -0m00.05s || 1652 ko | -1.36% | +0.39% 0m04.29s | 451880 ko | rupicola/src/Rupicola/Examples/CRC32/CRC32.vo | 0m04.39s | 450700 ko || -0m00.09s || 1180 ko | -2.27% | +0.26% 0m04.21s | 495228 ko | Rewriter/Language/IdentifiersLibraryProofs.vo | 0m04.28s | 493948 ko || -0m00.07s || 1280 ko | -1.63% | +0.25% 0m04.18s | 824624 ko | PushButtonSynthesis/SolinasReduction.vo | 0m04.36s | 829332 ko || -0m00.18s || -4708 ko | -4.12% | -0.56% 0m04.18s | 439676 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memswap.vo | 0m04.42s | 439720 ko || -0m00.24s || -44 ko | -5.42% | -0.01% 0m04.11s | 513660 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m03.65s | 512788 ko || +0m00.46s || 872 ko | +12.60% | +0.17% 0m04.09s | 831464 ko | PushButtonSynthesis/Primitives.vo | 0m04.11s | 837376 ko || -0m00.02s || -5912 ko | -0.48% | -0.70% 0m04.06s | 420704 ko | Arithmetic/MontgomeryReduction/Proofs.vo | 0m04.02s | 421464 ko || +0m00.04s || -760 ko | +0.99% | -0.18% 0m04.01s | 680568 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseAutoSplitMerge.vo | 0m03.96s | 681140 ko || +0m00.04s || -572 ko | +1.26% | -0.08% 0m04.00s | 466888 ko | rupicola/bedrock2/compiler/src/compiler/DeadCodeElimDef.vo | 0m03.89s | 468512 ko || +0m00.10s || -1624 ko | +2.82% | -0.34% 0m03.98s | 447012 ko | CastLemmas.vo | 0m04.40s | 448560 ko || -0m00.42s || -1548 ko | -9.54% | -0.34% 0m03.93s | 456228 ko | Util/ZRange/BasicLemmas.vo | 0m03.83s | 457792 ko || +0m00.10s || -1564 ko | +2.61% | -0.34% 0m03.91s | 438844 ko | Arithmetic/ModOps.vo | 0m03.95s | 438808 ko || -0m00.04s || 36 ko | -1.01% | +0.00% 0m03.85s | 442972 ko | rupicola/src/Rupicola/Examples/KVStore/Automated.vo | 0m03.89s | 440932 ko || -0m00.04s || 2040 ko | -1.02% | +0.46% 0m03.76s | 503600 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.01s | 503648 ko || +0m00.75s || -48 ko | +24.91% | -0.00% 0m03.76s | 429404 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/rpmul.vo | 0m03.32s | 429084 ko || +0m00.43s || 320 ko | +13.25% | +0.07% 0m03.73s | 449428 ko | Util/FSets/FMapSect.vo | 0m03.90s | 451940 ko || -0m00.16s || -2512 ko | -4.35% | -0.55% 0m03.70s | 425484 ko | Util/ZUtil/LandLorShiftBounds.vo | 0m03.88s | 425436 ko || -0m00.17s || 48 ko | -4.63% | +0.01% 0m03.65s | 491252 ko | rupicola/bedrock2/compiler/src/compiler/DeadCodeElim.vo | 0m03.58s | 491228 ko || +0m00.06s || 24 ko | +1.95% | +0.00% 0m03.60s | 436776 ko | rupicola/src/Rupicola/Examples/Uppercase.vo | 0m03.58s | 435800 ko || +0m00.02s || 976 ko | +0.55% | +0.22% 0m03.53s | 446396 ko | Util/FSets/FMapIso.vo | 0m03.42s | 445492 ko || +0m00.10s || 904 ko | +3.21% | +0.20% 0m03.51s | 425340 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap_by_add.vo | 0m03.12s | 424888 ko || +0m00.38s || 452 ko | +12.49% | +0.10% 0m03.50s | 415140 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_I_system.vo | 0m03.72s | 415512 ko || -0m00.22s || -372 ko | -5.91% | -0.08% 0m03.47s | 29100 ko | fiat-amd64/curve25519_solinas-square.status | 0m03.39s | 30416 ko || +0m00.08s || -1316 ko | +2.35% | -4.32% 0m03.46s | 430088 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO.vo | 0m04.18s | 430028 ko || -0m00.71s || 60 ko | -17.22% | +0.01% 0m03.43s | 439228 ko | rupicola/src/Rupicola/Examples/Arithmetic.vo | 0m03.31s | 439348 ko || +0m00.12s || -120 ko | +3.62% | -0.02% 0m03.41s | 442388 ko | rupicola/src/Rupicola/Examples/Expr.vo | 0m03.44s | 443376 ko || -0m00.02s || -988 ko | -0.87% | -0.22% 0m03.40s | 457636 ko | Util/ListUtil.vo | 0m03.47s | 457052 ko || -0m00.07s || 584 ko | -2.01% | +0.12% 0m03.40s | 29076 ko | fiat-amd64/curve25519-carry_square.status | 0m03.30s | 29556 ko || +0m00.10s || -480 ko | +3.03% | -1.62% 0m03.34s | 430596 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ipow.vo | 0m04.01s | 429012 ko || -0m00.67s || 1584 ko | -16.70% | +0.36% 0m03.32s | 885392 ko | CLI.vo | 0m03.35s | 890280 ko || -0m00.03s || -4888 ko | -0.89% | -0.54% 0m03.30s | 468072 ko | Arithmetic/BYInv.vo | 0m03.23s | 468596 ko || +0m00.06s || -524 ko | +2.16% | -0.11% 0m03.29s | 513060 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m03.62s | 513372 ko || -0m00.33s || -312 ko | -9.11% | -0.06% 0m03.21s | 435992 ko | rupicola/src/Rupicola/Examples/RevComp.vo | 0m03.08s | 434748 ko || +0m00.12s || 1244 ko | +4.22% | +0.28% 0m03.15s | 435696 ko | Arithmetic/UniformWeight.vo | 0m03.01s | 435360 ko || +0m00.14s || 336 ko | +4.65% | +0.07% 0m03.14s | 409000 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/invert_encode_U.vo | 0m03.25s | 414696 ko || -0m00.10s || -5696 ko | -3.38% | -1.37% 0m03.08s | 821860 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m03.08s | 825852 ko || +0m00.00s || -3992 ko | +0.00% | -0.48% 0m02.91s | 824204 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.01s | 828032 ko || -0m00.09s || -3828 ko | -3.32% | -0.46% 0m02.89s | 430772 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricLeakageSemantics.vo | 0m02.93s | 432704 ko || -0m00.04s || -1932 ko | -1.36% | -0.44% 0m02.87s | 445124 ko | Rewriter/Util/ListUtil.vo | 0m02.73s | 445800 ko || +0m00.14s || -676 ko | +5.12% | -0.15% 0m02.79s | 447844 ko | rupicola/src/Rupicola/Lib/Loops.vo | 0m02.73s | 448080 ko || +0m00.06s || -236 ko | +2.19% | -0.05% 0m02.77s | 452624 ko | COperationSpecifications.vo | 0m02.81s | 452680 ko || -0m00.04s || -56 ko | -1.42% | -0.01% 0m02.71s | 455692 ko | rupicola/bedrock2/bedrock2/src/bedrock2/unzify.vo | 0m02.65s | 455764 ko || +0m00.06s || -72 ko | +2.26% | -0.01% 0m02.67s | 480992 ko | rupicola/bedrock2/compiler/src/compiler/LowerPipeline.vo | 0m02.68s | 480452 ko || -0m00.01s || 540 ko | -0.37% | +0.11% 0m02.62s | 435536 ko | rupicola/bedrock2/compiler/src/compiler/ExprImp.vo | 0m02.64s | 441120 ko || -0m00.02s || -5584 ko | -0.75% | -1.26% 0m02.61s | 415504 ko | Util/ZUtil/TwosComplement.vo | 0m02.51s | 415212 ko || +0m00.10s || 292 ko | +3.98% | +0.07% 0m02.59s | 512560 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m02.99s | 513580 ko || -0m00.40s || -1020 ko | -13.37% | -0.19% 0m02.57s | 438788 ko | Arithmetic/Freeze.vo | 0m02.49s | 438836 ko || +0m00.07s || -48 ko | +3.21% | -0.01% 0m02.57s | 459960 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/e1000.vo | 0m02.77s | 460084 ko || -0m00.20s || -124 ko | -7.22% | -0.02% 0m02.56s | 435152 ko | rupicola/src/Rupicola/Examples/DownTo.vo | 0m02.55s | 433956 ko || +0m00.01s || 1196 ko | +0.39% | +0.27% 0m02.54s | 425280 ko | rupicola/bedrock2/bedrock2/src/bedrock2/HeapletwiseHyps.vo | 0m02.48s | 425372 ko || +0m00.06s || -92 ko | +2.41% | -0.02% 0m02.49s | 514796 ko | Bedrock/Field/Translation/Expr.vo | 0m02.48s | 516816 ko || +0m00.01s || -2020 ko | +0.40% | -0.39% 0m02.45s | 512024 ko | Rewriter/Passes/ToFancy.vo | 0m02.71s | 512464 ko || -0m00.25s || -440 ko | -9.59% | -0.08% 0m02.45s | 421932 ko | Util/ZUtil/Shift.vo | 0m03.01s | 421808 ko || -0m00.55s || 124 ko | -18.60% | +0.02% 0m02.41s | 423812 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/WMMFree.vo | 0m01.95s | 424364 ko || +0m00.46s || -552 ko | +23.58% | -0.13% 0m02.34s | 433040 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/memconst.vo | 0m02.71s | 434012 ko || -0m00.37s || -972 ko | -13.65% | -0.22% 0m02.32s | 416364 ko | Util/ZUtil/Testbit.vo | 0m02.11s | 416820 ko || +0m00.20s || -456 ko | +9.95% | -0.10% 0m02.31s | 440388 ko | Util/MSets/MSetIso.vo | 0m02.48s | 440180 ko || -0m00.16s || 208 ko | -6.85% | +0.04% 0m02.31s | 28296 ko | fiat-amd64/secp256k1_dettman-mul.status | 0m02.33s | 28564 ko || -0m00.02s || -268 ko | -0.85% | -0.93% 0m02.28s | 446248 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/Properties.vo | 0m02.26s | 442428 ko || +0m00.02s || 3820 ko | +0.88% | +0.86% 0m02.26s | 431780 ko | coqutil/Datatypes/List.vo | 0m02.35s | 431484 ko || -0m00.09s || 296 ko | -3.82% | +0.06% 0m02.23s | 499264 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LeakageSemantics.vo | 0m02.28s | 497496 ko || -0m00.04s || 1768 ko | -2.19% | +0.35% 0m02.21s | 414040 ko | Util/Bool/Reflect.vo | 0m02.19s | 415100 ko || +0m00.02s || -1060 ko | +0.91% | -0.25% 0m02.16s | 459784 ko | rupicola/bedrock2/compiler/src/compiler/Pipeline.vo | 0m02.17s | 456704 ko || -0m00.00s || 3080 ko | -0.46% | +0.67% 0m02.14s | 463828 ko | Rewriter/Language/IdentifiersBasicLibrary.vo | 0m02.21s | 465780 ko || -0m00.06s || -1952 ko | -3.16% | -0.41% 0m02.13s | 431076 ko | rupicola/src/Rupicola/Examples/Cells/IndirectAdd.vo | 0m02.20s | 432244 ko || -0m00.07s || -1168 ko | -3.18% | -0.27% 0m02.08s | 24776 ko | fiat-amd64/poly1305-carry_mul.status | 0m02.01s | 24256 ko || +0m00.07s || 520 ko | +3.48% | +2.14% 0m02.06s | 512480 ko | Stringification/Go.vo | 0m02.08s | 512384 ko || -0m00.02s || 96 ko | -0.96% | +0.01% 0m02.06s | 425280 ko | Util/Structures/Orders.vo | 0m02.04s | 428784 ko || +0m00.02s || -3504 ko | +0.98% | -0.81% 0m02.05s | 408972 ko | test/SlowGoals.vo | 0m02.05s | 408124 ko || +0m00.00s || 848 ko | +0.00% | +0.20% 0m02.04s | 420020 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SemanticsRelations.vo | 0m02.08s | 419732 ko || -0m00.04s || 288 ko | -1.92% | +0.06% 0m02.03s | 428476 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponderProofs.vo | 0m02.07s | 427808 ko || -0m00.04s || 668 ko | -1.93% | +0.15% 0m02.03s | 470956 ko | rupicola/bedrock2/compiler/src/compiler/load_save_regs_correct.vo | 0m02.08s | 470096 ko || -0m00.05s || 860 ko | -2.40% | +0.18% 0m01.99s | 519596 ko | Stringification/Language.vo | 0m01.99s | 519964 ko || +0m00.00s || -368 ko | +0.00% | -0.07% 0m01.96s | 421048 ko | Arithmetic/Primitives.vo | 0m01.98s | 421828 ko || -0m00.02s || -780 ko | -1.01% | -0.18% 0m01.95s | 420356 ko | Util/ZUtil/Div.vo | 0m02.14s | 420780 ko || -0m00.19s || -424 ko | -8.87% | -0.10% 0m01.94s | 433932 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoArray.vo | 0m01.99s | 434236 ko || -0m00.05s || -304 ko | -2.51% | -0.07% 0m01.90s | 517508 ko | Util/FSets/FMapTrie/ShapeEx.vo | 0m02.20s | 518232 ko || -0m00.30s || -724 ko | -13.63% | -0.13% 0m01.88s | 548160 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.14s | 547880 ko || -0m00.26s || 280 ko | -12.14% | +0.05% 0m01.87s | 435724 ko | rupicola/bedrock2/compiler/src/compiler/memory_mapped_ext_calls_riscv.vo | 0m01.89s | 440572 ko || -0m00.01s || -4848 ko | -1.05% | -1.10% 0m01.80s | 435500 ko | Arithmetic/BaseConversion.vo | 0m01.65s | 436588 ko || +0m00.15s || -1088 ko | +9.09% | -0.24% 0m01.80s | 411132 ko | Util/ZUtil/ZSimplify/Autogenerated.vo | 0m01.83s | 410912 ko || -0m00.03s || 220 ko | -1.63% | +0.05% 0m01.79s | 380984 ko | Algebra/Group.vo | 0m01.72s | 380528 ko || +0m00.07s || 456 ko | +4.06% | +0.11% 0m01.79s | 543820 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.79s | 543624 ko || +0m00.00s || 196 ko | +0.00% | +0.03% 0m01.77s | 409068 ko | Coqprime/PrimalityTest/PocklingtonCertificat.vo | 0m01.71s | 409692 ko || +0m00.06s || -624 ko | +3.50% | -0.15% 0m01.74s | 428148 ko | coqutil/Map/Properties.vo | 0m01.80s | 428868 ko || -0m00.06s || -720 ko | -3.33% | -0.16% 0m01.73s | 515248 ko | Stringification/C.vo | 0m01.86s | 513104 ko || -0m00.13s || 2144 ko | -6.98% | +0.41% 0m01.68s | 425700 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/swap.vo | 0m01.33s | 426932 ko || +0m00.34s || -1232 ko | +26.31% | -0.28% 0m01.67s | 423724 ko | Util/Tuple.vo | 0m01.62s | 426764 ko || +0m00.04s || -3040 ko | +3.08% | -0.71% 0m01.67s | 403700 ko | rupicola/bedrock2/bedrock2/src/bedrock2/AbsintWordToZ.vo | 0m01.65s | 403096 ko || +0m00.02s || 604 ko | +1.21% | +0.14% 0m01.66s | 510072 ko | Stringification/JSON.vo | 0m01.46s | 510096 ko || +0m00.19s || -24 ko | +13.69% | -0.00% 0m01.62s | 802152 ko | Bedrock/Field/Translation/Cmd.vo | 0m01.60s | 805592 ko || +0m00.02s || -3440 ko | +1.25% | -0.42% 0m01.61s | 438660 ko | Arithmetic/DettmanMultiplication.vo | 0m01.59s | 437872 ko || +0m00.02s || 788 ko | +1.25% | +0.17% 0m01.61s | 436172 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Impl.vo | 0m01.46s | 436244 ko || +0m00.15s || -72 ko | +10.27% | -0.01% 0m01.60s | 864544 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m01.61s | 867440 ko || -0m00.01s || -2896 ko | -0.62% | -0.33% 0m01.59s | 446232 ko | Util/ZUtil/Morphisms.vo | 0m01.99s | 446236 ko || -0m00.39s || -4 ko | -20.10% | -0.00% 0m01.58s | 506520 ko | Stringification/Rust.vo | 0m01.76s | 506372 ko || -0m00.17s || 148 ko | -10.22% | +0.02% 0m01.56s | 432932 ko | rupicola/src/Rupicola/Examples/IO/Echo.vo | 0m01.59s | 432364 ko || -0m00.03s || 568 ko | -1.88% | +0.13% 0m01.56s | 435740 ko | rupicola/src/Rupicola/Examples/Nondeterminism/StackAlloc.vo | 0m01.44s | 435220 ko || +0m00.12s || 520 ko | +8.33% | +0.11% 0m01.54s | 839736 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m01.51s | 845464 ko || +0m00.03s || -5728 ko | +1.98% | -0.67% 0m01.54s | 23188 ko | fiat-amd64/poly1305-carry_square.status | 0m01.55s | 23372 ko || -0m00.01s || -184 ko | -0.64% | -0.78% 0m01.49s | 404044 ko | Util/Structures/Orders/Option.vo | 0m01.45s | 404416 ko || +0m00.04s || -372 ko | +2.75% | -0.09% 0m01.49s | 415004 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/InstructionSetOrder.vo | 0m01.31s | 418676 ko || +0m00.17s || -3672 ko | +13.74% | -0.87% 0m01.48s | 24968 ko | fiat-amd64/secp256k1_dettman-square.status | 0m01.45s | 24708 ko || +0m00.03s || 260 ko | +2.06% | +1.05% 0m01.47s | 420424 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricSemantics.vo | 0m01.49s | 420036 ko || -0m00.02s || 388 ko | -1.34% | +0.09% 0m01.47s | 414388 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Fib.vo | 0m01.80s | 414596 ko || -0m00.33s || -208 ko | -18.33% | -0.05% 0m01.46s | 504436 ko | AbstractInterpretation/ZRange.vo | 0m01.62s | 503540 ko || -0m00.16s || 896 ko | -9.87% | +0.17% 0m01.45s | 835684 ko | Bedrock/Field/Stringification/Stringification.vo | 0m01.42s | 838988 ko || +0m00.03s || -3304 ko | +2.11% | -0.39% 0m01.45s | 424024 ko | Util/ZRange/SplitBounds.vo | 0m01.48s | 423740 ko || -0m00.03s || 284 ko | -2.02% | +0.06% 0m01.45s | 428360 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl_ltac1.vo | 0m01.54s | 429240 ko || -0m00.09s || -880 ko | -5.84% | -0.20% 0m01.43s | 408104 ko | Util/ListUtil/Forall.vo | 0m01.41s | 407168 ko || +0m00.02s || 936 ko | +1.41% | +0.22% 0m01.41s | 436124 ko | rupicola/src/Rupicola/Lib/Core.vo | 0m01.42s | 440968 ko || -0m00.01s || -4844 ko | -0.70% | -1.09% 0m01.39s | 448752 ko | Util/FSets/FMapUnit.vo | 0m01.53s | 450880 ko || -0m00.14s || -2128 ko | -9.15% | -0.47% 0m01.39s | 432248 ko | rupicola/src/Rupicola/Examples/LinkedList/Find.vo | 0m01.37s | 432448 ko || +0m00.01s || -200 ko | +1.45% | -0.04% 0m01.38s | 418916 ko | Rewriter/Util/Bool/Reflect.vo | 0m01.38s | 416396 ko || +0m00.00s || 2520 ko | +0.00% | +0.60% 0m01.38s | 509648 ko | Stringification/Zig.vo | 0m01.43s | 507924 ko || -0m00.05s || 1724 ko | -3.49% | +0.33% 0m01.35s | 423824 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricLoops.vo | 0m01.38s | 421704 ko || -0m00.02s || 2120 ko | -2.17% | +0.50% 0m01.34s | 799804 ko | Bedrock/Field/Translation/Func.vo | 0m01.31s | 804668 ko || +0m00.03s || -4864 ko | +2.29% | -0.60% 0m01.33s | 505712 ko | Stringification/Java.vo | 0m01.74s | 506104 ko || -0m00.40s || -392 ko | -23.56% | -0.07% 0m01.33s | 415568 ko | Util/ZUtil/Ones.vo | 0m01.15s | 414528 ko || +0m00.18s || 1040 ko | +15.65% | +0.25% 0m01.30s | 431952 ko | Arithmetic/ModularArithmeticTheorems.vo | 0m01.29s | 431880 ko || +0m00.01s || 72 ko | +0.77% | +0.01% 0m01.29s | 421708 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LeakageLoops.vo | 0m01.28s | 426440 ko || +0m00.01s || -4732 ko | +0.78% | -1.10% 0m01.28s | 803448 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m01.17s | 804608 ko || +0m00.11s || -1160 ko | +9.40% | -0.14% 0m01.22s | 496360 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.35s | 499012 ko || -0m00.13s || -2652 ko | -9.62% | -0.53% 0m01.22s | 842156 ko | Rewriter/PerfTesting/Core.vo | 0m01.25s | 841872 ko || -0m00.03s || 284 ko | -2.40% | +0.03% 0m01.21s | 435140 ko | Util/FSets/FMapFacts.vo | 0m01.10s | 436188 ko || +0m00.10s || -1048 ko | +9.99% | -0.24% 0m01.21s | 419228 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimalMMIO.vo | 0m01.12s | 418404 ko || +0m00.08s || 824 ko | +8.03% | +0.19% 0m01.18s | 408248 ko | Util/ListUtil/StdlibCompat.vo | 0m00.96s | 409084 ko || +0m00.21s || -836 ko | +22.91% | -0.20% 0m01.18s | 418072 ko | Util/ZUtil/Pow2Mod.vo | 0m01.21s | 417632 ko || -0m00.03s || 440 ko | -2.47% | +0.10% 0m01.16s | 421420 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWordsTests.vo | 0m01.22s | 421268 ko || -0m00.06s || 152 ko | -4.91% | +0.03% 0m01.15s | 427980 ko | rupicola/bedrock2/bedrock2/src/bedrock2/memory_mapped_ext_spec.vo | 0m01.09s | 431172 ko || +0m00.05s || -3192 ko | +5.50% | -0.74% 0m01.13s | 415560 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LeakageWeakestPreconditionProperties.vo | 0m01.15s | 414756 ko || -0m00.02s || 804 ko | -1.73% | +0.19% 0m01.12s | 406116 ko | coqutil/Map/MapEauto.vo | 0m01.05s | 404892 ko || +0m00.07s || 1224 ko | +6.66% | +0.30% 0m01.11s | 418556 ko | Util/ZUtil/TruncatingShiftl.vo | 0m01.43s | 420572 ko || -0m00.31s || -2016 ko | -22.37% | -0.47% 0m01.09s | 500760 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m01.08s | 500168 ko || +0m00.01s || 592 ko | +0.92% | +0.11% 0m01.09s | 407524 ko | Coqprime/Z/Pmod.vo | 0m01.12s | 406312 ko || -0m00.03s || 1212 ko | -2.67% | +0.29% 0m01.09s | 424104 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_adder.vo | 0m01.10s | 423348 ko || -0m00.01s || 756 ko | -0.90% | +0.17% 0m01.07s | 498828 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m01.17s | 498960 ko || -0m00.09s || -132 ko | -8.54% | -0.02% 0m01.07s | 412332 ko | Util/ZUtil/OnesFrom.vo | 0m00.95s | 412172 ko || +0m00.12s || 160 ko | +12.63% | +0.03% 0m01.07s | 425328 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_sub.vo | 0m01.05s | 425360 ko || +0m00.02s || -32 ko | +1.90% | -0.00% 0m01.04s | 827148 ko | StandaloneOCamlMain.vo | 0m01.07s | 832504 ko || -0m00.03s || -5356 ko | -2.80% | -0.64% 0m01.02s | 419988 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Loops.vo | 0m01.12s | 420380 ko || -0m00.10s || -392 ko | -8.92% | -0.09% 0m01.01s | 425080 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/shrd.vo | 0m01.15s | 424572 ko || -0m00.13s || 508 ko | -12.17% | +0.11% 0m00.96s | 435548 ko | rupicola/bedrock2/compiler/src/compiler/GoFlatToRiscv.vo | 0m00.94s | 435792 ko || +0m00.02s || -244 ko | +2.12% | -0.05% 0m00.95s | 428236 ko | Assembly/Parse.vo | 0m01.68s | 447016 ko || -0m00.73s || -18780 ko | -43.45% | -4.20% 0m00.95s | 406540 ko | Rewriter/Rewriter/Examples/PerfTesting/Harness.vo | 0m00.97s | 407920 ko || -0m00.02s || -1380 ko | -2.06% | -0.33% 0m00.95s | 408164 ko | coqutil/Map/SeparationLogic.vo | 0m00.90s | 410116 ko || +0m00.04s || -1952 ko | +5.55% | -0.47% 0m00.91s | 414168 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FrameRule.vo | 0m00.87s | 414308 ko || +0m00.04s || -140 ko | +4.59% | -0.03% 0m00.91s | 416768 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricWeakestPreconditionProperties.vo | 0m00.93s | 417076 ko || -0m00.02s || -308 ko | -2.15% | -0.07% 0m00.91s | 403968 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/bverify.vo | 0m00.77s | 404308 ko || +0m00.14s || -340 ko | +18.18% | -0.08% 0m00.90s | 417116 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZWordMem.vo | 0m00.99s | 420880 ko || -0m00.08s || -3764 ko | -9.09% | -0.89% 0m00.90s | 421112 ko | rupicola/bedrock2/compiler/src/compiler/SeparationLogic.vo | 0m00.94s | 421832 ko || -0m00.03s || -720 ko | -4.25% | -0.17% 0m00.89s | 417416 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Semantics.vo | 0m00.91s | 418684 ko || -0m00.02s || -1268 ko | -2.19% | -0.30% 0m00.89s | 430840 ko | rupicola/src/Rupicola/Examples/Conditionals.vo | 0m00.92s | 431592 ko || -0m00.03s || -752 ko | -3.26% | -0.17% 0m00.88s | 415592 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Scalars.vo | 0m00.82s | 418340 ko || +0m00.06s || -2748 ko | +7.31% | -0.65% 0m00.87s | 405812 ko | Util/ZUtil/Rshi.vo | 0m00.81s | 405924 ko || +0m00.05s || -112 ko | +7.40% | -0.02% 0m00.86s | 442916 ko | Util/MSets/MSetN.vo | 0m00.81s | 442708 ko || +0m00.04s || 208 ko | +6.17% | +0.04% 0m00.86s | 442888 ko | rupicola/bedrock2/compiler/src/compiler/CompilerInvariant.vo | 0m00.83s | 442176 ko || +0m00.03s || 712 ko | +3.61% | +0.16% 0m00.85s | 401436 ko | Rewriter/Util/ListUtil/Forall.vo | 0m00.80s | 401292 ko || +0m00.04s || 144 ko | +6.24% | +0.03% 0m00.85s | 419432 ko | coqutil/Tactics/ident_of_string.vo | 0m00.88s | 420644 ko || -0m00.03s || -1212 ko | -3.40% | -0.28% 0m00.85s | 430540 ko | rupicola/bedrock2/bedrock2/src/bedrock2/e1000_read_write_step.vo | 0m00.83s | 431728 ko || +0m00.02s || -1188 ko | +2.40% | -0.27% 0m00.83s | 435884 ko | rupicola/src/Rupicola/Lib/Arrays.vo | 0m00.84s | 433384 ko || -0m00.01s || 2500 ko | -1.19% | +0.57% 0m00.82s | 437900 ko | Arithmetic/PrimeFieldTheorems.vo | 0m00.89s | 437328 ko || -0m00.07s || 572 ko | -7.86% | +0.13% 0m00.82s | 408068 ko | Coqprime/PrimalityTest/EGroup.vo | 0m00.80s | 404176 ko || +0m00.01s || 3892 ko | +2.49% | +0.96% 0m00.81s | 491084 ko | Bedrock/Field/Translation/Flatten.vo | 0m00.79s | 490828 ko || +0m00.02s || 256 ko | +2.53% | +0.05% 0m00.81s | 350628 ko | Util/Wf1.vo | 0m00.74s | 350960 ko || +0m00.07s || -332 ko | +9.45% | -0.09% 0m00.80s | 415024 ko | Assembly/Equality.vo | 0m00.91s | 420336 ko || -0m00.10s || -5312 ko | -12.08% | -1.26% 0m00.79s | 430080 ko | Util/NumTheoryUtil.vo | 0m00.67s | 429196 ko || +0m00.12s || 884 ko | +17.91% | +0.20% 0m00.79s | 414988 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPreconditionProperties.vo | 0m00.85s | 414292 ko || -0m00.05s || 696 ko | -7.05% | +0.16% 0m00.78s | 491844 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m00.74s | 491324 ko || +0m00.04s || 520 ko | +5.40% | +0.10% 0m00.78s | 403084 ko | Coqprime/PrimalityTest/LucasLehmer.vo | 0m00.62s | 401840 ko || +0m00.16s || 1244 ko | +25.80% | +0.30% 0m00.77s | 399720 ko | Coqprime/Z/ZCAux.vo | 0m00.75s | 400064 ko || +0m00.02s || -344 ko | +2.66% | -0.08% 0m00.77s | 402588 ko | coqutil/Datatypes/PropSet.vo | 0m00.82s | 401624 ko || -0m00.04s || 964 ko | -6.09% | +0.24% 0m00.77s | 417064 ko | rupicola/bedrock2/bedrock2/src/bedrock2/bottom_up_simpl_perf.vo | 0m00.79s | 417208 ko || -0m00.02s || -144 ko | -2.53% | -0.03% 0m00.76s | 470260 ko | Util/Strings/ParseFlagOptions.vo | 0m00.74s | 469572 ko || +0m00.02s || 688 ko | +2.70% | +0.14% 0m00.76s | 404932 ko | coqutil/Word/LittleEndianList.vo | 0m00.75s | 405612 ko || +0m00.01s || -680 ko | +1.33% | -0.16% 0m00.76s | 414408 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ArrayCasts.vo | 0m00.73s | 412512 ko || +0m00.03s || 1896 ko | +4.10% | +0.45% 0m00.76s | 438168 ko | rupicola/src/Rupicola/Lib/ControlFlow/CondSwap.vo | 0m00.76s | 431504 ko || +0m00.00s || 6664 ko | +0.00% | +1.54% 0m00.75s | 488648 ko | Bedrock/Field/Common/Types.vo | 0m00.72s | 488804 ko || +0m00.03s || -156 ko | +4.16% | -0.03% 0m00.74s | 429896 ko | Rewriter/Rules.vo | 0m01.22s | 431040 ko || -0m00.48s || -1144 ko | -39.34% | -0.26% 0m00.74s | 421736 ko | rupicola/bedrock2/bedrock2/src/bedrock2/sepapp.vo | 0m00.76s | 422244 ko || -0m00.02s || -508 ko | -2.63% | -0.12% 0m00.73s | 458044 ko | Rewriter/Rewriter/Rewriter.vo | 0m00.74s | 457344 ko || -0m00.01s || 700 ko | -1.35% | +0.15% 0m00.73s | 400864 ko | Rewriter/Util/NatUtil.vo | 0m00.76s | 401012 ko || -0m00.03s || -148 ko | -3.94% | -0.03% 0m00.72s | 427156 ko | rupicola/src/Rupicola/Lib/InlineTables.vo | 0m00.75s | 428224 ko || -0m00.03s || -1068 ko | -4.00% | -0.24% 0m00.71s | 404968 ko | Algebra/ScalarMult.vo | 0m00.70s | 404888 ko || +0m00.01s || 80 ko | +1.42% | +0.01% 0m00.71s | 481740 ko | Language/UnderLetsProofsExtra.vo | 0m00.74s | 482056 ko || -0m00.03s || -316 ko | -4.05% | -0.06% 0m00.71s | 411784 ko | Util/Strings/String_as_OT.vo | 0m00.72s | 412372 ko || -0m00.01s || -588 ko | -1.38% | -0.14% 0m00.71s | 421524 ko | Util/Structures/Orders/Sum.vo | 0m00.66s | 422004 ko || +0m00.04s || -480 ko | +7.57% | -0.11% 0m00.71s | 431776 ko | rupicola/src/Rupicola/Examples/Cells/Swap.vo | 0m00.71s | 431904 ko || +0m00.00s || -128 ko | +0.00% | -0.02% 0m00.71s | 431128 ko | rupicola/src/Rupicola/Examples/LinkedList/LinkedList.vo | 0m00.78s | 431712 ko || -0m00.07s || -584 ko | -8.97% | -0.13% 0m00.71s | 430376 ko | rupicola/src/Rupicola/Lib/ControlFlow/DownTo.vo | 0m00.73s | 429776 ko || -0m00.02s || 600 ko | -2.73% | +0.13% 0m00.70s | 454560 ko | Rewriter/Language/IdentifiersLibrary.vo | 0m00.69s | 456624 ko || +0m00.01s || -2064 ko | +1.44% | -0.45% 0m00.70s | 407948 ko | Util/NatUtil.vo | 0m00.71s | 408608 ko || -0m00.01s || -660 ko | -1.40% | -0.16% 0m00.70s | 423320 ko | Util/ZRange/OperationsBounds.vo | 0m00.72s | 422172 ko || -0m00.02s || 1148 ko | -2.77% | +0.27% 0m00.69s | 411812 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ptsto_bytes.vo | 0m00.73s | 411212 ko || -0m00.04s || 600 ko | -5.47% | +0.14% 0m00.68s | 426856 ko | Arithmetic/Partition.vo | 0m00.72s | 426716 ko || -0m00.03s || 140 ko | -5.55% | +0.03% 0m00.68s | 462864 ko | Rewriter/Rewriter/Reify.vo | 0m00.68s | 465152 ko || +0m00.00s || -2288 ko | +0.00% | -0.49% 0m00.68s | 409456 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Array.vo | 0m00.62s | 410960 ko || +0m00.06s || -1504 ko | +9.67% | -0.36% 0m00.67s | 410608 ko | Util/ZUtil/AddGetCarry.vo | 0m00.71s | 410456 ko || -0m00.03s || 152 ko | -5.63% | +0.03% 0m00.67s | 434896 ko | rupicola/bedrock2/compiler/src/compiler/FitsStack.vo | 0m00.66s | 436900 ko || +0m00.01s || -2004 ko | +1.51% | -0.45% 0m00.66s | 491224 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.66s | 497860 ko || +0m00.00s || -6636 ko | +0.00% | -1.33% 0m00.66s | 505512 ko | Util/FSets/FMapZ.vo | 0m00.58s | 507172 ko || +0m00.08s || -1660 ko | +13.79% | -0.32% 0m00.66s | 415132 ko | Util/Strings/ParseArithmetic.vo | 0m00.66s | 413172 ko || +0m00.00s || 1960 ko | +0.00% | +0.47% 0m00.66s | 431940 ko | rupicola/src/Rupicola/Examples/Nondeterminism/Peek.vo | 0m00.71s | 433292 ko || -0m00.04s || -1352 ko | -7.04% | -0.31% 0m00.65s | 432120 ko | rupicola/src/Rupicola/Lib/Compiler.vo | 0m00.62s | 430244 ko || +0m00.03s || 1876 ko | +4.83% | +0.43% 0m00.64s | 403544 ko | Coqprime/PrimalityTest/Pocklington.vo | 0m00.67s | 403408 ko || -0m00.03s || 136 ko | -4.47% | +0.03% 0m00.64s | 439008 ko | Util/FSets/FMapTrie/Shape.vo | 0m00.58s | 438028 ko || +0m00.06s || 980 ko | +10.34% | +0.22% 0m00.63s | 409396 ko | Algebra/IntegralDomain.vo | 0m00.60s | 409600 ko || +0m00.03s || -204 ko | +5.00% | -0.04% 0m00.63s | 514568 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.82s | 508864 ko || -0m00.18s || 5704 ko | -23.17% | +1.12% 0m00.63s | 432600 ko | rupicola/src/Rupicola/Examples/Tree/Tree.vo | 0m00.63s | 432508 ko || +0m00.00s || 92 ko | +0.00% | +0.02% 0m00.62s | 483788 ko | MiscCompilerPassesProofsExtra.vo | 0m00.73s | 484820 ko || -0m00.10s || -1032 ko | -15.06% | -0.21% 0m00.62s | 442524 ko | Util/FSets/FMapFlip.vo | 0m00.68s | 443124 ko || -0m00.06s || -600 ko | -8.82% | -0.13% 0m00.62s | 411048 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/mmio_read_write_step_based_ext_spec.vo | 0m00.69s | 410960 ko || -0m00.06s || 88 ko | -10.14% | +0.02% 0m00.61s | 412416 ko | Util/ErrorT/List.vo | 0m00.63s | 412084 ko || -0m00.02s || 332 ko | -3.17% | +0.08% 0m00.60s | 464424 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.74s | 463940 ko || -0m00.14s || 484 ko | -18.91% | +0.10% 0m00.59s | 422300 ko | rupicola/bedrock2/bedrock2/src/bedrock2/to_from_anybytes.vo | 0m00.60s | 421464 ko || -0m00.01s || 836 ko | -1.66% | +0.19% 0m00.59s | 431476 ko | rupicola/src/Rupicola/Examples/IO/Stdout.vo | 0m00.63s | 432884 ko || -0m00.04s || -1408 ko | -6.34% | -0.32% 0m00.58s | 401868 ko | coqutil/Z/BitOps.vo | 0m00.54s | 400088 ko || +0m00.03s || 1780 ko | +7.40% | +0.44% 0m00.57s | 414756 ko | Util/Arg.vo | 0m00.68s | 414516 ko || -0m00.11s || 240 ko | -16.17% | +0.05% 0m00.56s | 410636 ko | Util/CPSUtil.vo | 0m00.55s | 410624 ko || +0m00.01s || 12 ko | +1.81% | +0.00% 0m00.56s | 405300 ko | coqutil/Word/BigEndian.vo | 0m00.54s | 404540 ko || +0m00.02s || 760 ko | +3.70% | +0.18% 0m00.55s | 400868 ko | Coqprime/PrimalityTest/Root.vo | 0m00.53s | 400880 ko || +0m00.02s || -12 ko | +3.77% | -0.00% 0m00.55s | 451220 ko | MiscCompilerPasses.vo | 0m00.59s | 452496 ko || -0m00.03s || -1276 ko | -6.77% | -0.28% 0m00.55s | 439672 ko | Rewriter/Language/Language.vo | 0m00.55s | 439544 ko || +0m00.00s || 128 ko | +0.00% | +0.02% 0m00.54s | 432696 ko | rupicola/src/Rupicola/Examples/Cells/Incr.vo | 0m00.53s | 431756 ko || +0m00.01s || 940 ko | +1.88% | +0.21% 0m00.53s | 377708 ko | Util/Decidable.vo | 0m00.55s | 377060 ko || -0m00.02s || 648 ko | -3.63% | +0.17% 0m00.53s | 415788 ko | Util/ZUtil/Divide.vo | 0m00.58s | 415908 ko || -0m00.04s || -120 ko | -8.62% | -0.02% 0m00.52s | 464184 ko | Language/API.vo | 0m00.55s | 464356 ko || -0m00.03s || -172 ko | -5.45% | -0.03% 0m00.52s | 481412 ko | Language/WfExtra.vo | 0m00.63s | 481800 ko || -0m00.10s || -388 ko | -17.46% | -0.08% 0m00.52s | 485352 ko | Util/FSets/FMapN.vo | 0m00.59s | 483808 ko || -0m00.06s || 1544 ko | -11.86% | +0.31% 0m00.50s | 435544 ko | Util/MSets/MSetPositive/Show.vo | 0m00.50s | 433936 ko || +0m00.00s || 1608 ko | +0.00% | +0.37% 0m00.50s | 407496 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRGetSet.vo | 0m00.46s | 408976 ko || +0m00.03s || -1480 ko | +8.69% | -0.36% 0m00.49s | 100844 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.40s | 102360 ko || +0m00.08s || -1516 ko | +22.49% | -1.48% 0m00.49s | 102488 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi | 0m00.38s | 101964 ko || +0m00.10s || 524 ko | +28.94% | +0.51% 0m00.49s | 479464 ko | Language/APINotations.vo | 0m00.55s | 482016 ko || -0m00.06s || -2552 ko | -10.90% | -0.52% 0m00.49s | 426084 ko | Language/PreExtra.vo | 0m00.45s | 426620 ko || +0m00.03s || -536 ko | +8.88% | -0.12% 0m00.49s | 482588 ko | Rewriter/AllTacticsExtra.vo | 0m00.47s | 483080 ko || +0m00.02s || -492 ko | +4.25% | -0.10% 0m00.49s | 419840 ko | Util/Strings/NamingConventions.vo | 0m00.45s | 420316 ko || +0m00.03s || -476 ko | +8.88% | -0.11% 0m00.49s | 418324 ko | Util/ZUtil/CC.vo | 0m00.52s | 417264 ko || -0m00.03s || 1060 ko | -5.76% | +0.25% 0m00.49s | 406916 ko | Util/ZUtil/Modulo/PullPush.vo | 0m00.52s | 405872 ko || -0m00.03s || 1044 ko | -5.76% | +0.25% 0m00.49s | 420448 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Trace.vo | 0m00.49s | 421204 ko || +0m00.00s || -756 ko | +0.00% | -0.17% 0m00.49s | 418844 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/Example64Literal.vo | 0m00.66s | 417732 ko || -0m00.17s || 1112 ko | -25.75% | +0.26% 0m00.48s | 97980 ko | ExtractionOCaml/dettman_multiplication.cmi | 0m00.36s | 98960 ko || +0m00.12s || -980 ko | +33.33% | -0.99% 0m00.48s | 400828 ko | Util/OptionList.vo | 0m00.47s | 401068 ko || +0m00.01s || -240 ko | +2.12% | -0.05% 0m00.48s | 408632 ko | Util/Strings/ParseArithmeticToTaps.vo | 0m00.46s | 408616 ko || +0m00.01s || 16 ko | +4.34% | +0.00% 0m00.48s | 418976 ko | Util/ZUtil/Stabilization.vo | 0m00.55s | 418852 ko || -0m00.07s || 124 ko | -12.72% | +0.02% 0m00.47s | 417800 ko | Util/ZUtil/EquivModulo.vo | 0m00.40s | 417944 ko || +0m00.06s || -144 ko | +17.49% | -0.03% 0m00.46s | 506012 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.43s | 503968 ko || +0m00.03s || 2044 ko | +6.97% | +0.40% 0m00.46s | 426188 ko | rupicola/bedrock2/compiler/src/compiler/RiscvEventLoop.vo | 0m00.41s | 425964 ko || +0m00.05s || 224 ko | +12.19% | +0.05% 0m00.46s | 328316 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicMinimal.vo | 0m00.38s | 328480 ko || +0m00.08s || -164 ko | +21.05% | -0.04% 0m00.46s | 421536 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRs.vo | 0m00.55s | 424208 ko || -0m00.09s || -2672 ko | -16.36% | -0.62% 0m00.46s | 412008 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Primitives.vo | 0m00.52s | 412244 ko || -0m00.06s || -236 ko | -11.53% | -0.05% 0m00.45s | 99864 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.37s | 99888 ko || +0m00.08s || -24 ko | +21.62% | -0.02% 0m00.45s | 99532 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.35s | 99876 ko || +0m00.10s || -344 ko | +28.57% | -0.34% 0m00.45s | 99376 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.42s | 98968 ko || +0m00.03s || 408 ko | +7.14% | +0.41% 0m00.45s | 376516 ko | Rewriter/Util/Decidable.vo | 0m00.45s | 376280 ko || +0m00.00s || 236 ko | +0.00% | +0.06% 0m00.45s | 411204 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Examples/SMTVerif.vo | 0m00.54s | 410888 ko || -0m00.09s || 316 ko | -16.66% | +0.07% 0m00.45s | 417096 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalMMIO_Post.vo | 0m00.41s | 417060 ko || +0m00.04s || 36 ko | +9.75% | +0.00% 0m00.44s | 401208 ko | Coqprime/PrimalityTest/Cyclic.vo | 0m00.46s | 401680 ko || -0m00.02s || -472 ko | -4.34% | -0.11% 0m00.44s | 98728 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.32s | 97332 ko || +0m00.12s || 1396 ko | +37.50% | +1.43% 0m00.44s | 439168 ko | Rewriter/Language/IdentifiersGenerate.vo | 0m00.31s | 441416 ko || +0m00.13s || -2248 ko | +41.93% | -0.50% 0m00.44s | 418840 ko | Util/MSets/MSetString.vo | 0m00.41s | 418700 ko || +0m00.03s || 140 ko | +7.31% | +0.03% 0m00.44s | 443184 ko | Util/Structures/OrdersEx.vo | 0m00.51s | 442956 ko || -0m00.07s || 228 ko | -13.72% | +0.05% 0m00.43s | 486260 ko | AbstractInterpretation/WfExtra.vo | 0m00.50s | 486148 ko || -0m00.07s || 112 ko | -14.00% | +0.02% 0m00.43s | 402948 ko | Coqprime/Z/ZSum.vo | 0m00.47s | 403144 ko || -0m00.03s || -196 ko | -8.51% | -0.04% 0m00.43s | 432676 ko | rupicola/src/Rupicola/Examples/KVStore/Properties.vo | 0m00.37s | 433988 ko || +0m00.06s || -1312 ko | +16.21% | -0.30% 0m00.42s | 415140 ko | Arithmetic/ModularArithmeticPre.vo | 0m00.36s | 414828 ko || +0m00.06s || 312 ko | +16.66% | +0.07% 0m00.42s | 440884 ko | ArithmeticCPS/WordByWordMontgomery.vo | 0m00.40s | 440120 ko || +0m00.01s || 764 ko | +4.99% | +0.17% 0m00.42s | 103044 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.35s | 102336 ko || +0m00.07s || 708 ko | +20.00% | +0.69% 0m00.42s | 97800 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.38s | 96804 ko || +0m00.03s || 996 ko | +10.52% | +1.02% 0m00.42s | 409472 ko | Util/Strings/Sorting.vo | 0m00.43s | 409184 ko || -0m00.01s || 288 ko | -2.32% | +0.07% 0m00.42s | 398680 ko | coqutil/Z/PushPullMod.vo | 0m00.40s | 399296 ko || +0m00.01s || -616 ko | +4.99% | -0.15% 0m00.42s | 415848 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLib.vo | 0m00.38s | 415776 ko || +0m00.03s || 72 ko | +10.52% | +0.01% 0m00.42s | 407644 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCString.vo | 0m00.33s | 407084 ko || +0m00.08s || 560 ko | +27.27% | +0.13% 0m00.42s | 429232 ko | rupicola/src/Rupicola/Lib/ExprCompiler.vo | 0m00.45s | 429536 ko || -0m00.03s || -304 ko | -6.66% | -0.07% 0m00.41s | 431712 ko | ArithmeticCPS/Core.vo | 0m00.36s | 431336 ko || +0m00.04s || 376 ko | +13.88% | +0.08% 0m00.41s | 402640 ko | Coqprime/PrimalityTest/PGroup.vo | 0m00.44s | 400708 ko || -0m00.03s || 1932 ko | -6.81% | +0.48% 0m00.41s | 100004 ko | ExtractionOCaml/base_conversion.cmi | 0m00.42s | 99120 ko || -0m00.01s || 884 ko | -2.38% | +0.89% 0m00.41s | 420448 ko | Util/ZUtil/SignBit.vo | 0m00.44s | 420048 ko || -0m00.03s || 400 ko | -6.81% | +0.09% 0m00.41s | 400264 ko | coqutil/Word/LittleEndian.vo | 0m00.41s | 401844 ko || +0m00.00s || -1580 ko | +0.00% | -0.39% 0m00.41s | 408088 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/DisjointUnion.vo | 0m00.43s | 406924 ko || -0m00.02s || 1164 ko | -4.65% | +0.28% 0m00.41s | 414524 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/MetricPrimitives.vo | 0m00.34s | 415108 ko || +0m00.06s || -584 ko | +20.58% | -0.14% 0m00.41s | 430920 ko | rupicola/src/Rupicola/Examples/Utf8/Utils.vo | 0m00.43s | 431332 ko || -0m00.02s || -412 ko | -4.65% | -0.09% 0m00.40s | 512864 ko | Bedrock/Field/Common/Tactics.vo | 0m00.44s | 514300 ko || -0m00.03s || -1436 ko | -9.09% | -0.27% 0m00.40s | 414852 ko | Util/ZUtil/Log2.vo | 0m00.42s | 413992 ko || -0m00.01s || 860 ko | -4.76% | +0.20% 0m00.39s | 407736 ko | Rewriter/Rewriter/Examples/PerfTesting/Sample.vo | 0m00.39s | 408056 ko || +0m00.00s || -320 ko | +0.00% | -0.07% 0m00.39s | 417820 ko | Util/ZUtil/Divide/Bool.vo | 0m00.44s | 417612 ko || -0m00.04s || 208 ko | -11.36% | +0.04% 0m00.38s | 414604 ko | Util/Strings/Show.vo | 0m00.46s | 413744 ko || -0m00.08s || 860 ko | -17.39% | +0.20% 0m00.38s | 411124 ko | Util/ZUtil/Ltz.vo | 0m00.33s | 411336 ko || +0m00.04s || -212 ko | +15.15% | -0.05% 0m00.38s | 411784 ko | coqutil/Datatypes/ZList.vo | 0m00.34s | 410916 ko || +0m00.03s || 868 ko | +11.76% | +0.21% 0m00.38s | 413484 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Memory.vo | 0m00.35s | 415704 ko || +0m00.03s || -2220 ko | +8.57% | -0.53% 0m00.38s | 423876 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/e1000_stateless.vo | 0m00.38s | 423624 ko || +0m00.00s || 252 ko | +0.00% | +0.05% 0m00.37s | 416072 ko | Util/ZUtil/Lxor.vo | 0m00.43s | 416064 ko || -0m00.06s || 8 ko | -13.95% | +0.00% 0m00.37s | 403004 ko | coqutil/Datatypes/ListSet.vo | 0m00.39s | 402824 ko || -0m00.02s || 180 ko | -5.12% | +0.04% 0m00.37s | 414896 ko | rupicola/bedrock2/bedrock2/src/bedrock2/FE310CSemantics.vo | 0m00.31s | 413556 ko || +0m00.06s || 1340 ko | +19.35% | +0.32% 0m00.37s | 424044 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/e1000_wp.vo | 0m00.41s | 424156 ko || -0m00.03s || -112 ko | -9.75% | -0.02% 0m00.37s | 432912 ko | rupicola/src/Rupicola/Examples/Cells/Cells.vo | 0m00.30s | 431672 ko || +0m00.07s || 1240 ko | +23.33% | +0.28% 0m00.37s | 432464 ko | rupicola/src/Rupicola/Examples/IO/IO.vo | 0m00.46s | 432760 ko || -0m00.09s || -296 ko | -19.56% | -0.06% 0m00.37s | 431856 ko | rupicola/src/Rupicola/Examples/KVStore/KVStore.vo | 0m00.27s | 431632 ko || +0m00.09s || 224 ko | +37.03% | +0.05% 0m00.36s | 439796 ko | ArithmeticCPS/Freeze.vo | 0m00.43s | 438688 ko || -0m00.07s || 1108 ko | -16.27% | +0.25% 0m00.36s | 473884 ko | Rewriter/Rewriter/AllTactics.vo | 0m00.32s | 476580 ko || +0m00.03s || -2696 ko | +12.49% | -0.56% 0m00.36s | 422820 ko | Util/QUtil.vo | 0m00.45s | 423216 ko || -0m00.09s || -396 ko | -20.00% | -0.09% 0m00.36s | 415832 ko | Util/ZUtil/Land.vo | 0m00.41s | 416208 ko || -0m00.04s || -376 ko | -12.19% | -0.09% 0m00.36s | 420504 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/ARPResponder.vo | 0m00.37s | 420648 ko || -0m00.01s || -144 ko | -2.70% | -0.03% 0m00.36s | 406604 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeProver.vo | 0m00.35s | 405800 ko || +0m00.01s || 804 ko | +2.85% | +0.19% 0m00.36s | 408216 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI.vo | 0m00.36s | 408716 ko || +0m00.00s || -500 ko | +0.00% | -0.12% 0m00.35s | 428368 ko | Util/FSets/FMapString.vo | 0m00.37s | 428000 ko || -0m00.02s || 368 ko | -5.40% | +0.08% 0m00.35s | 415060 ko | Util/ZUtil/Pow.vo | 0m00.35s | 414500 ko || +0m00.00s || 560 ko | +0.00% | +0.13% 0m00.35s | 408984 ko | coqutil/Datatypes/OperatorOverloading.vo | 0m00.32s | 407148 ko || +0m00.02s || 1836 ko | +9.37% | +0.45% 0m00.35s | 432188 ko | rupicola/src/Rupicola/Lib/SepLocals.vo | 0m00.36s | 431164 ko || -0m00.01s || 1024 ko | -2.77% | +0.23% 0m00.34s | 407708 ko | Algebra/SubsetoidRing.vo | 0m00.49s | 405340 ko || -0m00.14s || 2368 ko | -30.61% | +0.58% 0m00.34s | 103608 ko | ExtractionOCaml/WithBedrock/fiat_crypto.cmi | 0m00.37s | 104932 ko || -0m00.02s || -1324 ko | -8.10% | -1.26% 0m00.34s | 103908 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi | 0m00.37s | 103716 ko || -0m00.02s || 192 ko | -8.10% | +0.18% 0m00.34s | 102400 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.36s | 100456 ko || -0m00.01s || 1944 ko | -5.55% | +1.93% 0m00.34s | 103880 ko | ExtractionOCaml/fiat_crypto.cmi | 0m00.46s | 101852 ko || -0m00.12s || 2028 ko | -26.08% | +1.99% 0m00.34s | 463220 ko | Rewriter/Rewriter/ProofsCommonTactics.vo | 0m00.28s | 462492 ko || +0m00.06s || 728 ko | +21.42% | +0.15% 0m00.34s | 417356 ko | Util/Listable.vo | 0m00.35s | 421440 ko || -0m00.00s || -4084 ko | -2.85% | -0.96% 0m00.34s | 403040 ko | Util/Structures/Orders/Flip.vo | 0m00.30s | 402004 ko || +0m00.04s || 1036 ko | +13.33% | +0.25% 0m00.34s | 416060 ko | Util/ZRange.vo | 0m00.40s | 414484 ko || -0m00.06s || 1576 ko | -15.00% | +0.38% 0m00.34s | 400512 ko | coqutil/Z/ZLib.vo | 0m00.38s | 399768 ko || -0m00.03s || 744 ko | -10.52% | +0.18% 0m00.34s | 403408 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WordPushDownLemmas.vo | 0m00.34s | 402124 ko || +0m00.00s || 1284 ko | +0.00% | +0.31% 0m00.34s | 412088 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec_wp.vo | 0m00.31s | 410108 ko || +0m00.03s || 1980 ko | +9.67% | +0.48% 0m00.33s | 100404 ko | ExtractionOCaml/WithBedrock/saturated_solinas.cmi | 0m00.35s | 99956 ko || -0m00.01s || 448 ko | -5.71% | +0.44% 0m00.33s | 411472 ko | Util/Level.vo | 0m00.43s | 411684 ko || -0m00.09s || -212 ko | -23.25% | -0.05% 0m00.33s | 400136 ko | Util/Strings/String.vo | 0m00.29s | 401752 ko || +0m00.04s || -1616 ko | +13.79% | -0.40% 0m00.33s | 408860 ko | coqutil/Map/OfListWord.vo | 0m00.35s | 409152 ko || -0m00.01s || -292 ko | -5.71% | -0.07% 0m00.33s | 401352 ko | rupicola/bedrock2/compiler/src/compiler/ZLemmas.vo | 0m00.29s | 401616 ko || +0m00.04s || -264 ko | +13.79% | -0.06% 0m00.33s | 406184 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Decode.vo | 0m00.25s | 406280 ko || +0m00.08s || -96 ko | +32.00% | -0.02% 0m00.32s | 431844 ko | ArithmeticCPS/Saturated.vo | 0m00.35s | 431904 ko || -0m00.02s || -60 ko | -8.57% | -0.01% 0m00.32s | 403760 ko | Coqprime/PrimalityTest/Zp.vo | 0m00.27s | 402820 ko || +0m00.04s || 940 ko | +18.51% | +0.23% 0m00.32s | 102688 ko | ExtractionOCaml/WithBedrock/word_by_word_montgomery.cmi | 0m00.31s | 100768 ko || +0m00.01s || 1920 ko | +3.22% | +1.90% 0m00.32s | 101444 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.37s | 101132 ko || -0m00.04s || 312 ko | -13.51% | +0.30% 0m00.32s | 402548 ko | Util/ListUtil/SetoidListFlatMap.vo | 0m00.35s | 401104 ko || -0m00.02s || 1444 ko | -8.57% | +0.36% 0m00.32s | 399656 ko | coqutil/Z/bitblast.vo | 0m00.32s | 403224 ko || +0m00.00s || -3568 ko | +0.00% | -0.88% 0m00.32s | 424996 ko | rupicola/bedrock2/bedrock2/src/bedrock2/NetworkPackets.vo | 0m00.31s | 424536 ko || +0m00.01s || 460 ko | +3.22% | +0.10% 0m00.32s | 424452 ko | rupicola/bedrock2/bedrock2/src/bedrock2/e1000_state.vo | 0m00.33s | 424048 ko || -0m00.01s || 404 ko | -3.03% | +0.09% 0m00.32s | 431936 ko | rupicola/src/Rupicola/Examples/Nondeterminism/NonDeterminism.vo | 0m00.30s | 433604 ko || +0m00.02s || -1668 ko | +6.66% | -0.38% 0m00.31s | 439888 ko | ArithmeticCPS/BaseConversion.vo | 0m00.37s | 438772 ko || -0m00.06s || 1116 ko | -16.21% | +0.25% 0m00.31s | 101832 ko | ExtractionOCaml/WithBedrock/solinas_reduction.cmi | 0m00.35s | 101244 ko || -0m00.03s || 588 ko | -11.42% | +0.58% 0m00.31s | 409720 ko | Util/ZUtil/Combine.vo | 0m00.29s | 409000 ko || +0m00.02s || 720 ko | +6.89% | +0.17% 0m00.31s | 400944 ko | coqutil/Word/Naive.vo | 0m00.27s | 401468 ko || +0m00.03s || -524 ko | +14.81% | -0.13% 0m00.31s | 406160 ko | coqutil/Z/prove_Zeq_bitwise.vo | 0m00.29s | 406192 ko || +0m00.02s || -32 ko | +6.89% | -0.00% 0m00.31s | 423320 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ByteListPredicates.vo | 0m00.33s | 424772 ko || -0m00.02s || -1452 ko | -6.06% | -0.34% 0m00.31s | 413616 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TransferSepsOrder.vo | 0m00.32s | 415816 ko || -0m00.01s || -2200 ko | -3.12% | -0.52% 0m00.31s | 408168 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Memory.vo | 0m00.24s | 407668 ko || +0m00.07s || 500 ko | +29.16% | +0.12% 0m00.31s | 349296 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Monads.vo | 0m00.27s | 349820 ko || +0m00.03s || -524 ko | +14.81% | -0.14% 0m00.30s | 437908 ko | ArithmeticCPS/ModOps.vo | 0m00.25s | 436364 ko || +0m00.04s || 1544 ko | +19.99% | +0.35% 0m00.30s | 400908 ko | Coqprime/PrimalityTest/IGroup.vo | 0m00.28s | 400828 ko || +0m00.01s || 80 ko | +7.14% | +0.01% 0m00.30s | 100248 ko | ExtractionOCaml/WithBedrock/base_conversion.cmi | 0m00.32s | 100792 ko || -0m00.02s || -544 ko | -6.25% | -0.53% 0m00.30s | 101624 ko | ExtractionOCaml/WithBedrock/dettman_multiplication.cmi | 0m00.35s | 100512 ko || -0m00.04s || 1112 ko | -14.28% | +1.10% 0m00.30s | 101680 ko | ExtractionOCaml/WithBedrock/unsaturated_solinas.cmi | 0m00.34s | 102372 ko || -0m00.04s || -692 ko | -11.76% | -0.67% 0m00.30s | 404636 ko | coqutil/Map/SortedList.vo | 0m00.33s | 406472 ko || -0m00.03s || -1836 ko | -9.09% | -0.45% 0m00.30s | 410784 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TraceInspection.vo | 0m00.29s | 418256 ko || +0m00.01s || -7472 ko | +3.44% | -1.78% 0m00.30s | 412300 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/Demos.vo | 0m00.28s | 411072 ko || +0m00.01s || 1228 ko | +7.14% | +0.29% 0m00.30s | 404832 ko | rupicola/bedrock2/compiler/src/compiler/DivisibleBy4.vo | 0m00.30s | 404620 ko || +0m00.00s || 212 ko | +0.00% | +0.05% 0m00.30s | 413720 ko | rupicola/bedrock2/compiler/src/compiler/UniqueSepLog.vo | 0m00.30s | 411796 ko || +0m00.00s || 1924 ko | +0.00% | +0.46% 0m00.30s | 429568 ko | rupicola/src/Rupicola/Lib/NoExprReflection.vo | 0m00.29s | 427900 ko || +0m00.01s || 1668 ko | +3.44% | +0.38% 0m00.29s | 401268 ko | Coqprime/List/ZProgression.vo | 0m00.30s | 400212 ko || -0m00.01s || 1056 ko | -3.33% | +0.26% 0m00.29s | 400704 ko | Coqprime/PrimalityTest/Lagrange.vo | 0m00.28s | 400196 ko || +0m00.00s || 508 ko | +3.57% | +0.12% 0m00.29s | 462452 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo | 0m00.27s | 462480 ko || +0m00.01s || -28 ko | +7.40% | -0.00% 0m00.29s | 377776 ko | Util/Sum.vo | 0m00.28s | 379128 ko || +0m00.00s || -1352 ko | +3.57% | -0.35% 0m00.29s | 400812 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricLogging.vo | 0m00.27s | 400712 ko || +0m00.01s || 100 ko | +7.40% | +0.02% 0m00.29s | 411444 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Refinement.vo | 0m00.29s | 411780 ko || +0m00.00s || -336 ko | +0.00% | -0.08% 0m00.29s | 420856 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/chacha20.vo | 0m00.32s | 420808 ko || -0m00.03s || 48 ko | -9.37% | +0.01% 0m00.29s | 404588 ko | rupicola/bedrock2/compiler/src/compiler/NaiveRiscvWordProperties.vo | 0m00.30s | 404696 ko || -0m00.01s || -108 ko | -3.33% | -0.02% 0m00.29s | 378920 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/StringRecords.vo | 0m00.21s | 380132 ko || +0m00.07s || -1212 ko | +38.09% | -0.31% 0m00.29s | 428556 ko | rupicola/src/Rupicola/Lib/ExprReflection.vo | 0m00.31s | 428336 ko || -0m00.02s || 220 ko | -6.45% | +0.05% 0m00.28s | 316536 ko | Arithmetic/MontgomeryReduction/Definition.vo | 0m00.23s | 315780 ko || +0m00.05s || 756 ko | +21.73% | +0.23% 0m00.28s | 401516 ko | Coqprime/Z/ZCmisc.vo | 0m00.29s | 400568 ko || -0m00.00s || 948 ko | -3.44% | +0.23% 0m00.28s | 496492 ko | Rewriter/All.vo | 0m00.29s | 498284 ko || -0m00.00s || -1792 ko | -3.44% | -0.35% 0m00.28s | 403200 ko | Util/ListUtil/GroupAllBy.vo | 0m00.31s | 402616 ko || -0m00.02s || 584 ko | -9.67% | +0.14% 0m00.28s | 411644 ko | Util/Structures/Equalities/List.vo | 0m00.30s | 408732 ko || -0m00.01s || 2912 ko | -6.66% | +0.71% 0m00.28s | 406016 ko | Util/ZUtil/Le.vo | 0m00.27s | 407180 ko || +0m00.01s || -1164 ko | +3.70% | -0.28% 0m00.28s | 402364 ko | rupicola/bedrock2/compiler/src/compiler/Registers.vo | 0m00.29s | 402844 ko || -0m00.00s || -480 ko | -3.44% | -0.11% 0m00.28s | 413692 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Sane.vo | 0m00.36s | 414196 ko || -0m00.07s || -504 ko | -22.22% | -0.12% 0m00.27s | 380260 ko | Coqprime/List/Permutation.vo | 0m00.29s | 381068 ko || -0m00.01s || -808 ko | -6.89% | -0.21% 0m00.27s | 380576 ko | Coqprime/List/UList.vo | 0m00.25s | 380540 ko || +0m00.02s || 36 ko | +8.00% | +0.00% 0m00.27s | 401708 ko | Coqprime/PrimalityTest/Euler.vo | 0m00.26s | 401400 ko || +0m00.01s || 308 ko | +3.84% | +0.07% 0m00.27s | 365612 ko | Util/ZRange/Operations.vo | 0m00.21s | 365816 ko || +0m00.06s || -204 ko | +28.57% | -0.05% 0m00.27s | 410792 ko | coqutil/Map/OfFunc.vo | 0m00.28s | 407484 ko || -0m00.01s || 3308 ko | -3.57% | +0.81% 0m00.27s | 386580 ko | coqutil/Tactics/ident_to_string.vo | 0m00.29s | 386228 ko || -0m00.01s || 352 ko | -6.89% | +0.09% 0m00.27s | 421728 ko | rupicola/bedrock2/bedrock2/src/bedrock2/RecordPredicates.vo | 0m00.30s | 421332 ko || -0m00.02s || 396 ko | -9.99% | +0.09% 0m00.27s | 421080 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCalls.vo | 0m00.30s | 420144 ko || -0m00.02s || 936 ko | -9.99% | +0.22% 0m00.27s | 423340 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/MultipleReturnValues.vo | 0m00.37s | 422912 ko || -0m00.09s || 428 ko | -27.02% | +0.10% 0m00.27s | 343060 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/LogInstructionTrace.vo | 0m00.24s | 341136 ko || +0m00.03s || 1924 ko | +12.50% | +0.56% 0m00.27s | 375916 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA64.vo | 0m00.22s | 374784 ko || +0m00.05s || 1132 ko | +22.72% | +0.30% 0m00.27s | 405184 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Encode.vo | 0m00.22s | 404896 ko || +0m00.05s || 288 ko | +22.72% | +0.07% 0m00.26s | 403584 ko | Rewriter/Util/Strings/ParseArithmetic.vo | 0m00.26s | 405456 ko || +0m00.00s || -1872 ko | +0.00% | -0.46% 0m00.26s | 415600 ko | rupicola/bedrock2/bedrock2/src/bedrock2/OperatorOverloading.vo | 0m00.30s | 414472 ko || -0m00.03s || 1128 ko | -13.33% | +0.27% 0m00.26s | 411748 ko | rupicola/bedrock2/compiler/src/compiler/StringNameGen.vo | 0m00.24s | 412732 ko || +0m00.02s || -984 ko | +8.33% | -0.23% 0m00.26s | 320520 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/FE310ExtSpec.vo | 0m00.21s | 320560 ko || +0m00.05s || -40 ko | +23.80% | -0.01% 0m00.25s | 390416 ko | Language/IdentifierParameters.vo | 0m00.23s | 389240 ko || +0m00.01s || 1176 ko | +8.69% | +0.30% 0m00.25s | 432208 ko | Rewriter/Language/IdentifiersBasicGenerate.vo | 0m00.24s | 438304 ko || +0m00.01s || -6096 ko | +4.16% | -1.39% 0m00.25s | 439628 ko | Rewriter/Language/IdentifiersGenerateProofs.vo | 0m00.27s | 438180 ko || -0m00.02s || 1448 ko | -7.40% | +0.33% 0m00.25s | 459324 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo | 0m00.26s | 460964 ko || -0m00.01s || -1640 ko | -3.84% | -0.35% 0m00.25s | 346336 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMinimal.vo | 0m00.31s | 347776 ko || -0m00.06s || -1440 ko | -19.35% | -0.41% 0m00.25s | 374884 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalCSRsDet.vo | 0m00.23s | 374500 ko || +0m00.01s || 384 ko | +8.69% | +0.10% 0m00.25s | 431500 ko | rupicola/src/Rupicola/Examples/IO/Writer.vo | 0m00.33s | 432720 ko || -0m00.08s || -1220 ko | -24.24% | -0.28% 0m00.25s | 429520 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/Spec.vo | 0m00.26s | 428740 ko || -0m00.01s || 780 ko | -3.84% | +0.18% 0m00.24s | 378372 ko | Algebra/Monoid.vo | 0m00.23s | 382772 ko || +0m00.00s || -4400 ko | +4.34% | -1.14% 0m00.24s | 300952 ko | Util/ZUtil/Tactics/RewriteModDivide.vo | 0m00.20s | 300740 ko || +0m00.03s || 212 ko | +19.99% | +0.07% 0m00.24s | 400056 ko | coqutil/Datatypes/String.vo | 0m00.24s | 399484 ko || +0m00.00s || 572 ko | +0.00% | +0.14% 0m00.24s | 224744 ko | rupicola/bedrock2/bedrock2/src/bedrock2/cancel_div.vo | 0m00.24s | 223496 ko || +0m00.00s || 1248 ko | +0.00% | +0.55% 0m00.24s | 383356 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/StateMachineBasedExtSpec.vo | 0m00.23s | 384228 ko || +0m00.00s || -872 ko | +4.34% | -0.22% 0m00.24s | 292888 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM64.vo | 0m00.16s | 294088 ko || +0m00.07s || -1200 ko | +49.99% | -0.40% 0m00.23s | 378924 ko | Rewriter/Util/Sum.vo | 0m00.24s | 378356 ko || -0m00.00s || 568 ko | -4.16% | +0.15% 0m00.23s | 462912 ko | Rewriter/Util/plugins/RewriterBuild.vo | 0m00.23s | 462132 ko || +0m00.00s || 780 ko | +0.00% | +0.16% 0m00.23s | 460852 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo | 0m00.23s | 460892 ko || +0m00.00s || -40 ko | +0.00% | -0.00% 0m00.23s | 371688 ko | Util/ZUtil/Tactics/LtbToLt.vo | 0m00.20s | 371836 ko || +0m00.03s || -148 ko | +15.00% | -0.03% 0m00.23s | 310968 ko | Util/ZUtil/Tactics/SolveRange.vo | 0m00.31s | 311848 ko || -0m00.07s || -880 ko | -25.80% | -0.28% 0m00.23s | 306164 ko | Util/ZUtil/Tactics/Ztestbit.vo | 0m00.22s | 306200 ko || +0m00.01s || -36 ko | +4.54% | -0.01% 0m00.23s | 408000 ko | coqutil/Datatypes/Result.vo | 0m00.24s | 407756 ko || -0m00.00s || 244 ko | -4.16% | +0.05% 0m00.23s | 421608 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpUniqueSepLog.vo | 0m00.23s | 420288 ko || +0m00.00s || 1320 ko | +0.00% | +0.31% 0m00.23s | 371260 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricMaterializeRiscvProgram.vo | 0m00.27s | 371848 ko || -0m00.04s || -588 ko | -14.81% | -0.15% 0m00.23s | 334112 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MinimalLogging.vo | 0m00.18s | 334076 ko || +0m00.05s || 36 ko | +27.77% | +0.01% 0m00.23s | 409716 ko | rupicola/src/Rupicola/Examples/KVStore/kv.vo | 0m00.23s | 410916 ko || +0m00.00s || -1200 ko | +0.00% | -0.29% 0m00.23s | 423496 ko | rupicola/src/Rupicola/Examples/Swap/Properties.vo | 0m00.20s | 422936 ko || +0m00.03s || 560 ko | +15.00% | +0.13% 0m00.23s | 427208 ko | rupicola/src/Rupicola/Lib/SepReflection.vo | 0m00.22s | 427232 ko || +0m00.01s || -24 ko | +4.54% | -0.00% 0m00.22s | 290136 ko | Spec/ModularArithmetic.vo | 0m00.21s | 290432 ko || +0m00.01s || -296 ko | +4.76% | -0.10% 0m00.22s | 412748 ko | Util/ZUtil/ModInv.vo | 0m00.23s | 414164 ko || -0m00.01s || -1416 ko | -4.34% | -0.34% 0m00.22s | 366748 ko | Util/ZUtil/Peano.vo | 0m00.17s | 367280 ko || +0m00.04s || -532 ko | +29.41% | -0.14% 0m00.22s | 313952 ko | Util/ZUtil/Tactics/SolveTestbit.vo | 0m00.27s | 312768 ko || -0m00.05s || 1184 ko | -18.51% | +0.37% 0m00.22s | 403964 ko | coqutil/Word/ZifyLittleEndian.vo | 0m00.20s | 404576 ko || +0m00.01s || -612 ko | +9.99% | -0.15% 0m00.22s | 330824 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC32Semantics.vo | 0m00.18s | 330580 ko || +0m00.04s || 244 ko | +22.22% | +0.07% 0m00.22s | 356816 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringExprTypecheckingTest.vo | 0m00.18s | 354504 ko || +0m00.04s || 2312 ko | +22.22% | +0.65% 0m00.22s | 370804 ko | rupicola/bedrock2/bedrock2/src/bedrock2/footpr.vo | 0m00.22s | 370952 ko || +0m00.00s || -148 ko | +0.00% | -0.03% 0m00.22s | 424252 ko | rupicola/bedrock2/compiler/src/compiler/ForeverSafe.vo | 0m00.16s | 424312 ko || +0m00.06s || -60 ko | +37.50% | -0.01% 0m00.22s | 286288 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/AtomicRiscvMachine.vo | 0m00.20s | 289708 ko || +0m00.01s || -3420 ko | +9.99% | -1.18% 0m00.22s | 300768 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/Run.vo | 0m00.20s | 300964 ko || +0m00.01s || -196 ko | +9.99% | -0.06% 0m00.22s | 376440 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteCSR.vo | 0m00.27s | 376676 ko || -0m00.05s || -236 ko | -18.51% | -0.06% 0m00.22s | 295964 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MkMachineWidth.vo | 0m00.18s | 297656 ko || +0m00.04s || -1692 ko | +22.22% | -0.56% 0m00.22s | 398068 ko | rupicola/src/Rupicola/Examples/CRC32/Table.vo | 0m00.23s | 397164 ko || -0m00.01s || 904 ko | -4.34% | +0.22% 0m00.21s | 380296 ko | Coqprime/List/Iterator.vo | 0m00.19s | 380776 ko || +0m00.01s || -480 ko | +10.52% | -0.12% 0m00.21s | 428064 ko | Rewriter/Language/Reify.vo | 0m00.20s | 429816 ko || +0m00.00s || -1752 ko | +4.99% | -0.40% 0m00.21s | 376720 ko | Rewriter/Util/MSetPositive/Facts.vo | 0m00.19s | 377372 ko || +0m00.01s || -652 ko | +10.52% | -0.17% 0m00.21s | 307360 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifyHeapletwise.vo | 0m00.16s | 307200 ko || +0m00.04s || 160 ko | +31.24% | +0.05% 0m00.21s | 303764 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PurifySep.vo | 0m00.15s | 304040 ko || +0m00.06s || -276 ko | +40.00% | -0.09% 0m00.21s | 342708 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WeakestPrecondition.vo | 0m00.22s | 343736 ko || -0m00.01s || -1028 ko | -4.54% | -0.29% 0m00.21s | 367740 ko | rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb_spec.vo | 0m00.18s | 368520 ko || +0m00.03s || -780 ko | +16.66% | -0.21% 0m00.21s | 443156 ko | rupicola/bedrock2/compiler/src/compiler/ExprImpEventLoopSpec.vo | 0m00.21s | 444084 ko || +0m00.00s || -928 ko | +0.00% | -0.20% 0m00.21s | 338700 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MaterializeRiscvProgram.vo | 0m00.17s | 339016 ko || +0m00.03s || -316 ko | +23.52% | -0.09% 0m00.21s | 291252 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricRiscvMachine.vo | 0m00.21s | 290216 ko || +0m00.00s || 1036 ko | +0.00% | +0.35% 0m00.21s | 262296 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRField.vo | 0m00.14s | 263776 ko || +0m00.06s || -1480 ko | +49.99% | -0.56% 0m00.21s | 428888 ko | rupicola/src/Rupicola/Lib/Alloc.vo | 0m00.23s | 429128 ko || -0m00.02s || -240 ko | -8.69% | -0.05% 0m00.20s | 296680 ko | Util/ErrorT/Show.vo | 0m00.19s | 296636 ko || +0m00.01s || 44 ko | +5.26% | +0.01% 0m00.20s | 349556 ko | Util/ListUtil/Permutation.vo | 0m00.18s | 350996 ko || +0m00.02s || -1440 ko | +11.11% | -0.41% 0m00.20s | 379636 ko | Util/Structures/Equalities/Sum.vo | 0m00.22s | 380036 ko || -0m00.01s || -400 ko | -9.09% | -0.10% 0m00.20s | 314568 ko | Util/ZUtil/Land/Fold.vo | 0m00.23s | 314608 ko || -0m00.03s || -40 ko | -13.04% | -0.01% 0m00.20s | 353372 ko | Util/ZUtil/Tactics/RewriteModSmall.vo | 0m00.20s | 353404 ko || +0m00.00s || -32 ko | +0.00% | -0.00% 0m00.20s | 306960 ko | coqutil/Datatypes/RecordSetters.vo | 0m00.19s | 314576 ko || +0m00.01s || -7616 ko | +5.26% | -2.42% 0m00.20s | 356856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricWeakestPrecondition.vo | 0m00.19s | 357040 ko || +0m00.01s || -184 ko | +5.26% | -0.05% 0m00.20s | 379464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAutoExports.vo | 0m00.21s | 378616 ko || -0m00.00s || 848 ko | -4.76% | +0.22% 0m00.20s | 427464 ko | rupicola/bedrock2/bedrock2/src/bedrock2/e1000_packet_trace.vo | 0m00.19s | 426180 ko || +0m00.01s || 1284 ko | +5.26% | +0.30% 0m00.20s | 298556 ko | rupicola/bedrock2/bedrock2/src/bedrock2/is_emp.vo | 0m00.17s | 299112 ko || +0m00.03s || -556 ko | +17.64% | -0.18% 0m00.20s | 368736 ko | rupicola/bedrock2/bedrock2/src/bedrock2/safe_implication.vo | 0m00.18s | 368524 ko || +0m00.02s || 212 ko | +11.11% | +0.05% 0m00.20s | 377176 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteA.vo | 0m00.23s | 376488 ko || -0m00.03s || 688 ko | -13.04% | +0.18% 0m00.20s | 405344 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/LeakageOfInstr.vo | 0m00.23s | 405268 ko || -0m00.03s || 76 ko | -13.04% | +0.01% 0m00.20s | 324404 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Machine.vo | 0m00.22s | 323840 ko || -0m00.01s || 564 ko | -9.09% | +0.17% 0m00.20s | 265636 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Tactics.vo | 0m00.11s | 266084 ko || +0m00.09s || -448 ko | +81.81% | -0.16% 0m00.20s | 429596 ko | rupicola/src/Rupicola/Lib/Conditionals.vo | 0m00.18s | 428864 ko || +0m00.02s || 732 ko | +11.11% | +0.17% 0m00.20s | 426868 ko | rupicola/src/Rupicola/Lib/Monads.vo | 0m00.17s | 427056 ko || +0m00.03s || -188 ko | +17.64% | -0.04% 0m00.20s | 406732 ko | rupicola/src/Rupicola/Lib/ToCString.vo | 0m00.19s | 402872 ko || +0m00.01s || 3860 ko | +5.26% | +0.95% 0m00.19s | 380556 ko | Coqprime/List/ListAux.vo | 0m00.20s | 379940 ko || -0m00.01s || 616 ko | -5.00% | +0.16% 0m00.19s | 342884 ko | Coqprime/PrimalityTest/FGroup.vo | 0m00.15s | 342308 ko || +0m00.04s || 576 ko | +26.66% | +0.16% 0m00.19s | 304384 ko | Rewriter/Language/PreLemmas.vo | 0m00.13s | 303988 ko || +0m00.06s || 396 ko | +46.15% | +0.13% 0m00.19s | 298488 ko | Util/MSets/Show.vo | 0m00.22s | 297072 ko || -0m00.03s || 1416 ko | -13.63% | +0.47% 0m00.19s | 347288 ko | Util/Structures/Equalities/Prod.vo | 0m00.18s | 347756 ko || +0m00.01s || -468 ko | +5.55% | -0.13% 0m00.19s | 346352 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepAuto.vo | 0m00.15s | 346428 ko || +0m00.04s || -76 ko | +26.66% | -0.02% 0m00.19s | 341700 ko | rupicola/bedrock2/compiler/src/compiler/mod4_0.vo | 0m00.18s | 341072 ko || +0m00.01s || 628 ko | +5.55% | +0.18% 0m00.19s | 339560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/RiscvMachine.vo | 0m00.29s | 340048 ko || -0m00.09s || -488 ko | -34.48% | -0.14% 0m00.19s | 289560 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl32.vo | 0m00.18s | 290072 ko || +0m00.01s || -512 ko | +5.55% | -0.17% 0m00.18s | 324076 ko | Algebra/Nsatz.vo | 0m00.14s | 323624 ko || +0m00.03s || 452 ko | +28.57% | +0.13% 0m00.18s | 292932 ko | Bedrock/Field/Common/Names/VarnameGenerator.vo | 0m00.16s | 292832 ko || +0m00.01s || 100 ko | +12.49% | +0.03% 0m00.18s | 349012 ko | Rewriter/Util/MSetPositive/Equality.vo | 0m00.17s | 347952 ko || +0m00.00s || 1060 ko | +5.88% | +0.30% 0m00.18s | 346276 ko | Util/ListUtil/SetoidList.vo | 0m00.23s | 345076 ko || -0m00.05s || 1200 ko | -21.73% | +0.34% 0m00.18s | 296040 ko | Util/Strings/Show/Enum.vo | 0m00.20s | 295048 ko || -0m00.02s || 992 ko | -10.00% | +0.33% 0m00.18s | 319232 ko | Util/Structures/Orders/Unit.vo | 0m00.18s | 319272 ko || +0m00.00s || -40 ko | +0.00% | -0.01% 0m00.18s | 291516 ko | Util/ZRange/Show.vo | 0m00.21s | 292096 ko || -0m00.03s || -580 ko | -14.28% | -0.19% 0m00.18s | 314136 ko | Util/ZUtil/Lor.vo | 0m00.22s | 314076 ko || -0m00.04s || 60 ko | -18.18% | +0.01% 0m00.18s | 267116 ko | coqutil/Word/Bitwidth64.vo | 0m00.16s | 266516 ko || +0m00.01s || 600 ko | +12.49% | +0.22% 0m00.18s | 329588 ko | rupicola/bedrock2/bedrock2/src/bedrock2/BasicC64Semantics.vo | 0m00.20s | 329988 ko || -0m00.02s || -400 ko | -10.00% | -0.12% 0m00.18s | 371124 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LeakageWeakestPrecondition.vo | 0m00.18s | 371192 ko || +0m00.00s || -68 ko | +0.00% | -0.01% 0m00.18s | 266584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricCosts.vo | 0m00.16s | 264820 ko || +0m00.01s || 1764 ko | +12.49% | +0.66% 0m00.18s | 306284 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepLogAddrArith.vo | 0m00.19s | 307572 ko || -0m00.01s || -1288 ko | -5.26% | -0.41% 0m00.18s | 318140 ko | rupicola/bedrock2/compiler/src/compiler/regs_initialized.vo | 0m00.13s | 317712 ko || +0m00.04s || 428 ko | +38.46% | +0.13% 0m00.18s | 254468 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Platform/MetricLogging.vo | 0m00.16s | 255088 ko || +0m00.01s || -620 ko | +12.49% | -0.24% 0m00.18s | 251856 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/VirtualMemory.vo | 0m00.15s | 255004 ko || +0m00.03s || -3148 ko | +20.00% | -1.23% 0m00.18s | 289332 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Utility.vo | 0m00.17s | 288912 ko || +0m00.00s || 420 ko | +5.88% | +0.14% 0m00.17s | 305660 ko | Util/Option.vo | 0m00.17s | 305716 ko || +0m00.00s || -56 ko | +0.00% | -0.01% 0m00.17s | 338872 ko | Util/Structures/Orders/Iso.vo | 0m00.18s | 339592 ko || -0m00.00s || -720 ko | -5.55% | -0.21% 0m00.17s | 274828 ko | Util/ZUtil/AddModulo.vo | 0m00.17s | 276264 ko || +0m00.00s || -1436 ko | +0.00% | -0.51% 0m00.17s | 304904 ko | Util/ZUtil/Nat2Z.vo | 0m00.15s | 306404 ko || +0m00.02s || -1500 ko | +13.33% | -0.48% 0m00.17s | 289664 ko | Util/ZUtil/Pow2.vo | 0m00.17s | 294676 ko || +0m00.00s || -5012 ko | +0.00% | -1.70% 0m00.17s | 315040 ko | coqutil/Byte.vo | 0m00.16s | 315640 ko || +0m00.01s || -600 ko | +6.25% | -0.19% 0m00.17s | 269148 ko | coqutil/Tactics/Simp.vo | 0m00.15s | 268992 ko || +0m00.02s || 156 ko | +13.33% | +0.05% 0m00.17s | 264820 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListIndexNotations.vo | 0m00.15s | 263320 ko || +0m00.02s || 1500 ko | +13.33% | +0.56% 0m00.17s | 329036 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ProgramLogic.vo | 0m00.15s | 328224 ko || +0m00.02s || 812 ko | +13.33% | +0.24% 0m00.17s | 329340 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepappBulletPoints.vo | 0m00.14s | 327132 ko || +0m00.03s || 2208 ko | +21.42% | +0.67% 0m00.17s | 293756 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ZnWords.vo | 0m00.20s | 295684 ko || -0m00.03s || -1928 ko | -15.00% | -0.65% 0m00.17s | 292412 ko | rupicola/bedrock2/bedrock2/src/bedrock2/cancel_div_ltac1.vo | 0m00.16s | 292592 ko || +0m00.01s || -180 ko | +6.25% | -0.06% 0m00.17s | 292784 ko | rupicola/bedrock2/compiler/src/compiler/util/Common.vo | 0m00.18s | 291504 ko || -0m00.00s || 1280 ko | -5.55% | +0.43% 0m00.17s | 270756 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSRSpec.vo | 0m00.23s | 269568 ko || -0m00.06s || 1188 ko | -26.08% | +0.44% 0m00.17s | 290352 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/DefaultMemImpl64.vo | 0m00.18s | 288928 ko || -0m00.00s || 1424 ko | -5.55% | +0.49% 0m00.17s | 297184 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionNotations.vo | 0m00.17s | 298440 ko || +0m00.00s || -1256 ko | +0.00% | -0.42% 0m00.16s | 421936 ko | Rewriter/Language/UnderLets.vo | 0m00.19s | 421808 ko || -0m00.03s || 128 ko | -15.78% | +0.03% 0m00.16s | 307308 ko | Rewriter/Util/Option.vo | 0m00.14s | 305104 ko || +0m00.01s || 2204 ko | +14.28% | +0.72% 0m00.16s | 303904 ko | Util/IdfunWithAlt.vo | 0m00.19s | 303540 ko || -0m00.03s || 364 ko | -15.78% | +0.11% 0m00.16s | 263808 ko | Util/ListUtil/SetoidListRev.vo | 0m00.13s | 262716 ko || +0m00.03s || 1092 ko | +23.07% | +0.41% 0m00.16s | 315924 ko | Util/NUtil/Testbit.vo | 0m00.16s | 314080 ko || +0m00.00s || 1844 ko | +0.00% | +0.58% 0m00.16s | 271972 ko | Util/ZUtil/Hints/ZArith.vo | 0m00.16s | 269076 ko || +0m00.00s || 2896 ko | +0.00% | +1.07% 0m00.16s | 305304 ko | Util/ZUtil/MulSplit.vo | 0m00.19s | 305444 ko || -0m00.03s || -140 ko | -15.78% | -0.04% 0m00.16s | 316564 ko | Util/ZUtil/Opp.vo | 0m00.19s | 318692 ko || -0m00.03s || -2128 ko | -15.78% | -0.66% 0m00.16s | 275284 ko | Util/ZUtil/Tactics/ReplaceNegWithPos.vo | 0m00.14s | 273208 ko || +0m00.01s || 2076 ko | +14.28% | +0.75% 0m00.16s | 304064 ko | Util/ZUtil/Tactics/ZeroBounds.vo | 0m00.21s | 305264 ko || -0m00.04s || -1200 ko | -23.80% | -0.39% 0m00.16s | 272112 ko | Util/ZUtil/ZSimplify/Core.vo | 0m00.14s | 270908 ko || +0m00.01s || 1204 ko | +14.28% | +0.44% 0m00.16s | 317508 ko | Util/ZUtil/ZSimplify/Simple.vo | 0m00.15s | 318016 ko || +0m00.01s || -508 ko | +6.66% | -0.15% 0m00.16s | 303756 ko | coqutil/Map/Interface.vo | 0m00.12s | 305124 ko || +0m00.04s || -1368 ko | +33.33% | -0.44% 0m00.16s | 296280 ko | coqutil/Map/SortedListZ.vo | 0m00.15s | 292280 ko || +0m00.01s || 4000 ko | +6.66% | +1.36% 0m00.16s | 291236 ko | coqutil/Sorting/OrderToPermutation.vo | 0m00.12s | 291028 ko || +0m00.04s || 208 ko | +33.33% | +0.07% 0m00.16s | 326528 ko | coqutil/Word/DebugWordEq.vo | 0m00.16s | 326000 ko || +0m00.00s || 528 ko | +0.00% | +0.16% 0m00.16s | 275108 ko | coqutil/Z/Lia.vo | 0m00.15s | 277504 ko || +0m00.01s || -2396 ko | +6.66% | -0.86% 0m00.16s | 344916 ko | rupicola/bedrock2/bedrock2/src/bedrock2/NotationsCustomEntry.vo | 0m00.16s | 343516 ko || +0m00.00s || 1400 ko | +0.00% | +0.40% 0m00.16s | 282728 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepBulletPoints.vo | 0m00.16s | 281504 ko || +0m00.00s || 1224 ko | +0.00% | +0.43% 0m00.16s | 294856 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepClause.vo | 0m00.19s | 293184 ko || -0m00.03s || 1672 ko | -15.78% | +0.57% 0m00.16s | 308468 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteI64.vo | 0m00.18s | 308720 ko || -0m00.01s || -252 ko | -11.11% | -0.08% 0m00.16s | 273036 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/PseudoInstructions.vo | 0m00.16s | 269800 ko || +0m00.00s || 3236 ko | +0.00% | +1.19% 0m00.15s | 369600 ko | Rewriter/Util/Strings/String.vo | 0m00.16s | 367424 ko || -0m00.01s || 2176 ko | -6.25% | +0.59% 0m00.15s | 291364 ko | TAPSort.vo | 0m00.16s | 291560 ko || -0m00.01s || -196 ko | -6.25% | -0.06% 0m00.15s | 297472 ko | Util/Strings/Parse/Common.vo | 0m00.14s | 298900 ko || +0m00.00s || -1428 ko | +7.14% | -0.47% 0m00.15s | 246148 ko | Util/Strings/Subscript.vo | 0m00.15s | 245404 ko || +0m00.00s || 744 ko | +0.00% | +0.30% 0m00.15s | 300332 ko | Util/ZUtil/Definitions.vo | 0m00.14s | 300636 ko || +0m00.00s || -304 ko | +7.14% | -0.10% 0m00.15s | 270856 ko | Util/ZUtil/Hints/Core.vo | 0m00.14s | 271756 ko || +0m00.00s || -900 ko | +7.14% | -0.33% 0m00.15s | 273020 ko | Util/ZUtil/Hints/PullPush.vo | 0m00.14s | 272480 ko || +0m00.00s || 540 ko | +7.14% | +0.19% 0m00.15s | 272404 ko | Util/ZUtil/Lnot.vo | 0m00.14s | 271868 ko || +0m00.00s || 536 ko | +7.14% | +0.19% 0m00.15s | 334980 ko | Util/ZUtil/Odd.vo | 0m00.17s | 336184 ko || -0m00.02s || -1204 ko | -11.76% | -0.35% 0m00.15s | 266312 ko | Util/ZUtil/Tactics/CompareToSgn.vo | 0m00.14s | 263732 ko || +0m00.00s || 2580 ko | +7.14% | +0.97% 0m00.15s | 269160 ko | Util/ZUtil/Tactics/DivModToQuotRem.vo | 0m00.15s | 268868 ko || +0m00.00s || 292 ko | +0.00% | +0.10% 0m00.15s | 336960 ko | Util/ZUtil/Tactics/LinearSubstitute.vo | 0m00.19s | 336320 ko || -0m00.04s || 640 ko | -21.05% | +0.19% 0m00.15s | 269076 ko | Util/ZUtil/Tactics/SplitMinMax.vo | 0m00.15s | 267312 ko || +0m00.00s || 1764 ko | +0.00% | +0.65% 0m00.15s | 288600 ko | Util/ZUtil/Zselect.vo | 0m00.17s | 284388 ko || -0m00.02s || 4212 ko | -11.76% | +1.48% 0m00.15s | 284948 ko | coqutil/Map/Funext.vo | 0m00.12s | 283056 ko || +0m00.03s || 1892 ko | +25.00% | +0.66% 0m00.15s | 257492 ko | coqutil/Map/Separation.vo | 0m00.11s | 256876 ko || +0m00.03s || 616 ko | +36.36% | +0.23% 0m00.15s | 340480 ko | coqutil/Map/SortedListWord.vo | 0m00.18s | 341204 ko || -0m00.03s || -724 ko | -16.66% | -0.21% 0m00.15s | 298124 ko | coqutil/Map/Z_keyed_SortedListMap.vo | 0m00.15s | 298264 ko || +0m00.00s || -140 ko | +0.00% | -0.04% 0m00.15s | 342800 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LeakageProgramLogic.vo | 0m00.17s | 341292 ko || -0m00.02s || 1508 ko | -11.76% | +0.44% 0m00.15s | 255580 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/SeparationLogic.vo | 0m00.13s | 254812 ko || +0m00.01s || 768 ko | +15.38% | +0.30% 0m00.15s | 304604 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/split_alt.vo | 0m00.17s | 303864 ko || -0m00.02s || 740 ko | -11.76% | +0.24% 0m00.15s | 199748 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PrintString.vo | 0m00.13s | 198676 ko || +0m00.01s || 1072 ko | +15.38% | +0.53% 0m00.15s | 282044 ko | rupicola/bedrock2/bedrock2/src/bedrock2/groundcbv.vo | 0m00.14s | 283224 ko || +0m00.00s || -1180 ko | +7.14% | -0.41% 0m00.15s | 334848 ko | rupicola/bedrock2/bedrock2/src/bedrock2/old_dma/circular_buffer_slice_based_on_list_of_addrs.vo | 0m00.16s | 334336 ko || -0m00.01s || 512 ko | -6.25% | +0.15% 0m00.15s | 282848 ko | rupicola/bedrock2/bedrock2/src/bedrock2/syntactic_f_equal_with_ZnWords.vo | 0m00.18s | 283584 ko || -0m00.03s || -736 ko | -16.66% | -0.25% 0m00.15s | 309448 ko | rupicola/bedrock2/compiler/src/compiler/FixEq.vo | 0m00.14s | 310176 ko || +0m00.00s || -728 ko | +7.14% | -0.23% 0m00.15s | 348340 ko | rupicola/bedrock2/compiler/src/compiler/MemoryLayout.vo | 0m00.15s | 346340 ko || +0m00.00s || 2000 ko | +0.00% | +0.57% 0m00.15s | 320428 ko | rupicola/bedrock2/compiler/src/compiler/UseImmediateDef.vo | 0m00.12s | 323184 ko || +0m00.03s || -2756 ko | +25.00% | -0.85% 0m00.15s | 265952 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/Execute.vo | 0m00.20s | 264528 ko || -0m00.05s || 1424 ko | -25.00% | +0.53% 0m00.15s | 300932 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/ExecuteM.vo | 0m00.18s | 300912 ko || -0m00.03s || 20 ko | -16.66% | +0.00% 0m00.15s | 253768 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words64Naive.vo | 0m00.15s | 251996 ko || +0m00.00s || 1772 ko | +0.00% | +0.70% 0m00.15s | 346000 ko | rupicola/src/Rupicola/Lib/Tactics.vo | 0m00.14s | 347280 ko || +0m00.00s || -1280 ko | +7.14% | -0.36% 0m00.14s | 310420 ko | Language/TreeCaching.vo | 0m00.16s | 308836 ko || -0m00.01s || 1584 ko | -12.49% | +0.51% 0m00.14s | 246820 ko | Rewriter/Util/Strings/Decimal.vo | 0m00.14s | 247500 ko || +0m00.00s || -680 ko | +0.00% | -0.27% 0m00.14s | 240248 ko | Util/Decidable/Bool2Prop.vo | 0m00.10s | 240460 ko || +0m00.04s || -212 ko | +40.00% | -0.08% 0m00.14s | 269852 ko | Util/ZUtil/Div/Bootstrap.vo | 0m00.15s | 269820 ko || -0m00.00s || 32 ko | -6.66% | +0.01% 0m00.14s | 266788 ko | Util/ZUtil/Hints/Ztestbit.vo | 0m00.15s | 265976 ko || -0m00.00s || 812 ko | -6.66% | +0.30% 0m00.14s | 277264 ko | Util/ZUtil/ModExp.vo | 0m00.15s | 276052 ko || -0m00.00s || 1212 ko | -6.66% | +0.43% 0m00.14s | 281872 ko | Util/ZUtil/Modulo/Bootstrap.vo | 0m00.14s | 280080 ko || +0m00.00s || 1792 ko | +0.00% | +0.63% 0m00.14s | 296604 ko | Util/ZUtil/N2Z.vo | 0m00.13s | 296564 ko || +0m00.01s || 40 ko | +7.69% | +0.01% 0m00.14s | 272252 ko | Util/ZUtil/Tactics/PullPush/Modulo.vo | 0m00.19s | 272064 ko || -0m00.04s || 188 ko | -26.31% | +0.06% 0m00.14s | 254368 ko | coqutil/Datatypes/Inhabited.vo | 0m00.15s | 254320 ko || -0m00.00s || 48 ko | -6.66% | +0.01% 0m00.14s | 271588 ko | coqutil/Datatypes/RecordSettersUsingExistingGetters.vo | 0m00.12s | 272036 ko || +0m00.02s || -448 ko | +16.66% | -0.16% 0m00.14s | 268764 ko | coqutil/Decidable.vo | 0m00.16s | 267652 ko || -0m00.01s || 1112 ko | -12.49% | +0.41% 0m00.14s | 232012 ko | coqutil/Ltac2Lib/Lia.vo | 0m00.12s | 230880 ko || +0m00.02s || 1132 ko | +16.66% | +0.49% 0m00.14s | 260800 ko | coqutil/Map/Empty_set_keyed_map.vo | 0m00.12s | 258552 ko || +0m00.02s || 2248 ko | +16.66% | +0.86% 0m00.14s | 292532 ko | coqutil/Map/OfOptionListZ.vo | 0m00.12s | 291024 ko || +0m00.02s || 1508 ko | +16.66% | +0.51% 0m00.14s | 272748 ko | coqutil/Tactics/Tactics.vo | 0m00.15s | 273420 ko || -0m00.00s || -672 ko | -6.66% | -0.24% 0m00.14s | 266816 ko | coqutil/Word/Bitwidth.vo | 0m00.12s | 267272 ko || +0m00.02s || -456 ko | +16.66% | -0.17% 0m00.14s | 354960 ko | coqutil/Word/SimplWordExpr.vo | 0m00.14s | 353220 ko || +0m00.00s || 1740 ko | +0.00% | +0.49% 0m00.14s | 339640 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ToCStringStackallocLoopTest.vo | 0m00.16s | 336312 ko || -0m00.01s || 3328 ko | -12.49% | +0.98% 0m00.14s | 341040 ko | rupicola/bedrock2/bedrock2/src/bedrock2/canceling_sepapps.vo | 0m00.15s | 340948 ko || -0m00.00s || 92 ko | -6.66% | +0.02% 0m00.14s | 312412 ko | rupicola/bedrock2/compiler/src/compiler/FlatImpConstraints.vo | 0m00.13s | 312064 ko || +0m00.01s || 348 ko | +7.69% | +0.11% 0m00.14s | 358564 ko | rupicola/bedrock2/compiler/src/compiler/FlattenExprDef.vo | 0m00.14s | 360712 ko || +0m00.00s || -2148 ko | +0.00% | -0.59% 0m00.14s | 245088 ko | rupicola/bedrock2/compiler/src/compiler/NameGen.vo | 0m00.14s | 244132 ko || +0m00.00s || 956 ko | +0.00% | +0.39% 0m00.14s | 318604 ko | rupicola/bedrock2/compiler/src/compiler/ZNameGen.vo | 0m00.15s | 317192 ko || -0m00.00s || 1412 ko | -6.66% | +0.44% 0m00.14s | 263876 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/RegisterNames.vo | 0m00.11s | 261628 ko || +0m00.03s || 2248 ko | +27.27% | +0.85% 0m00.14s | 356004 ko | rupicola/src/Rupicola/Examples/KVStore/Tactics.vo | 0m00.17s | 355088 ko || -0m00.03s || 916 ko | -17.64% | +0.25% 0m00.14s | 376532 ko | rupicola/src/Rupicola/Examples/Net/IPChecksum/SpecExtraction.vo | 0m00.12s | 376540 ko || +0m00.02s || -8 ko | +16.66% | -0.00% 0m00.14s | 314576 ko | rupicola/src/Rupicola/Examples/Swap/Swap.vo | 0m00.16s | 315980 ko || -0m00.01s || -1404 ko | -12.49% | -0.44% 0m00.13s | 220308 ko | Algebra/Hierarchy.vo | 0m00.12s | 222164 ko || +0m00.01s || -1856 ko | +8.33% | -0.83% 0m00.13s | 343428 ko | Rewriter/Util/ListUtil/SetoidList.vo | 0m00.14s | 342956 ko || -0m00.01s || 472 ko | -7.14% | +0.13% 0m00.13s | 214600 ko | Util/DebugMonad.vo | 0m00.09s | 213036 ko || +0m00.04s || 1564 ko | +44.44% | +0.73% 0m00.13s | 279088 ko | Util/Factorize.vo | 0m00.14s | 278752 ko || -0m00.01s || 336 ko | -7.14% | +0.12% 0m00.13s | 305584 ko | Util/ListUtil/FoldBool.vo | 0m00.12s | 305592 ko || +0m00.01s || -8 ko | +8.33% | -0.00% 0m00.13s | 321720 ko | Util/NUtil/WithoutReferenceToZ.vo | 0m00.21s | 323188 ko || -0m00.07s || -1468 ko | -38.09% | -0.45% 0m00.13s | 280708 ko | Util/Prod.vo | 0m00.09s | 280316 ko || +0m00.04s || 392 ko | +44.44% | +0.13% 0m00.13s | 209496 ko | Util/Strings/Ascii.vo | 0m00.12s | 212604 ko || +0m00.01s || -3108 ko | +8.33% | -1.46% 0m00.13s | 267676 ko | Util/ZUtil/Tactics/DivideExistsMul.vo | 0m00.13s | 266404 ko || +0m00.00s || 1272 ko | +0.00% | +0.47% 0m00.13s | 321016 ko | Util/ZUtil/Z2Nat.vo | 0m00.13s | 320168 ko || +0m00.00s || 848 ko | +0.00% | +0.26% 0m00.13s | 278404 ko | coqutil/Datatypes/ToConversion.vo | 0m00.15s | 277072 ko || -0m00.01s || 1332 ko | -13.33% | +0.48% 0m00.13s | 364076 ko | coqutil/Map/MapKeys.vo | 0m00.17s | 365048 ko || -0m00.04s || -972 ko | -23.52% | -0.26% 0m00.13s | 284208 ko | coqutil/Map/Solver.vo | 0m00.15s | 289348 ko || -0m00.01s || -5140 ko | -13.33% | -1.77% 0m00.13s | 214180 ko | coqutil/Tactics/fwd_core.vo | 0m00.11s | 214068 ko || +0m00.02s || 112 ko | +18.18% | +0.05% 0m00.13s | 271132 ko | coqutil/Tactics/rewr.vo | 0m00.14s | 270988 ko || -0m00.01s || 144 ko | -7.14% | +0.05% 0m00.13s | 251264 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Map/Separation.vo | 0m00.12s | 251636 ko || +0m00.01s || -372 ko | +8.33% | -0.14% 0m00.13s | 327180 ko | rupicola/bedrock2/bedrock2/src/bedrock2/MetricProgramLogic.vo | 0m00.16s | 326612 ko || -0m00.03s || 568 ko | -18.75% | +0.17% 0m00.13s | 316568 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SepCallsExports.vo | 0m00.17s | 313792 ko || -0m00.04s || 2776 ko | -23.52% | +0.88% 0m00.13s | 307820 ko | rupicola/bedrock2/compiler/src/compiler/RiscvWordProperties.vo | 0m00.15s | 308384 ko || -0m00.01s || -564 ko | -13.33% | -0.18% 0m00.13s | 261432 ko | rupicola/bedrock2/compiler/src/compiler/Symbols.vo | 0m00.15s | 260744 ko || -0m00.01s || 688 ko | -13.33% | +0.26% 0m00.13s | 294904 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Spec/CSR.vo | 0m00.19s | 293644 ko || -0m00.06s || 1260 ko | -31.57% | +0.42% 0m00.13s | 247512 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/InstructionCoercions.vo | 0m00.12s | 249184 ko || +0m00.01s || -1672 ko | +8.33% | -0.67% 0m00.13s | 254016 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/Words32Naive.vo | 0m00.15s | 255196 ko || -0m00.01s || -1180 ko | -13.33% | -0.46% 0m00.13s | 276932 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/nat_div_mod_to_quot_rem.vo | 0m00.13s | 279452 ko || +0m00.00s || -2520 ko | +0.00% | -0.90% 0m00.13s | 328896 ko | rupicola/src/Rupicola/Examples/Assoc/Assoc.vo | 0m00.13s | 330104 ko || +0m00.00s || -1208 ko | +0.00% | -0.36% 0m00.13s | 329544 ko | rupicola/src/Rupicola/Examples/CapitalizeThird/CapitalizeThird.vo | 0m00.13s | 332788 ko || +0m00.00s || -3244 ko | +0.00% | -0.97% 0m00.13s | 362664 ko | rupicola/src/Rupicola/Lib/Notations.vo | 0m00.12s | 360824 ko || +0m00.01s || 1840 ko | +8.33% | +0.50% 0m00.13s | 338988 ko | rupicola/src/Rupicola/Lib/WordNotations.vo | 0m00.13s | 338020 ko || +0m00.00s || 968 ko | +0.00% | +0.28% 0m00.12s | 311192 ko | Rewriter/Util/FMapPositive/Equality.vo | 0m00.13s | 311164 ko || -0m00.01s || 28 ko | -7.69% | +0.00% 0m00.12s | 253340 ko | Util/FSets/FMapInterface.vo | 0m00.11s | 252760 ko || +0m00.00s || 580 ko | +9.09% | +0.22% 0m00.12s | 327504 ko | Util/ListUtil/Filter.vo | 0m00.16s | 328116 ko || -0m00.04s || -612 ko | -25.00% | -0.18% 0m00.12s | 177772 ko | Util/ListUtil/IndexOf.vo | 0m00.11s | 177852 ko || +0m00.00s || -80 ko | +9.09% | -0.04% 0m00.12s | 305952 ko | Util/PointedProp.vo | 0m00.12s | 305032 ko || +0m00.00s || 920 ko | +0.00% | +0.30% 0m00.12s | 246712 ko | Util/Strings/Decimal.vo | 0m00.15s | 248316 ko || -0m00.03s || -1604 ko | -20.00% | -0.64% 0m00.12s | 271160 ko | Util/ZUtil/Hints.vo | 0m00.14s | 269444 ko || -0m00.02s || 1716 ko | -14.28% | +0.63% 0m00.12s | 266968 ko | Util/ZUtil/Tactics/PeelLe.vo | 0m00.15s | 269244 ko || -0m00.03s || -2276 ko | -20.00% | -0.84% 0m00.12s | 220372 ko | Util/ZUtil/Tactics/PrimeBound.vo | 0m00.12s | 219636 ko || +0m00.00s || 736 ko | +0.00% | +0.33% 0m00.12s | 237052 ko | Util/ZUtil/Tactics/PullPush.vo | 0m00.16s | 236892 ko || -0m00.04s || 160 ko | -25.00% | +0.06% 0m00.12s | 198872 ko | coqutil/Ltac2Lib/Ring.vo | 0m00.11s | 197712 ko || +0m00.00s || 1160 ko | +9.09% | +0.58% 0m00.12s | 331412 ko | coqutil/Map/Domain.vo | 0m00.15s | 330000 ko || -0m00.03s || 1412 ko | -20.00% | +0.42% 0m00.12s | 256656 ko | coqutil/Map/SortedListString.vo | 0m00.13s | 254764 ko || -0m00.01s || 1892 ko | -7.69% | +0.74% 0m00.12s | 252440 ko | coqutil/Tactics/SafeSimpl.vo | 0m00.12s | 253456 ko || +0m00.00s || -1016 ko | +0.00% | -0.40% 0m00.12s | 256620 ko | coqutil/Tactics/fwd.vo | 0m00.14s | 256660 ko || -0m00.02s || -40 ko | -14.28% | -0.01% 0m00.12s | 198960 ko | coqutil/Tactics/fwd_arith_hints.vo | 0m00.13s | 198520 ko || -0m00.01s || 440 ko | -7.69% | +0.22% 0m00.12s | 270440 ko | coqutil/Tactics/fwd_word_hints.vo | 0m00.12s | 270560 ko || +0m00.00s || -120 ko | +0.00% | -0.04% 0m00.12s | 265232 ko | coqutil/Word/Bitwidth32.vo | 0m00.13s | 267116 ko || -0m00.01s || -1884 ko | -7.69% | -0.70% 0m00.12s | 229120 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TacticError.vo | 0m00.12s | 229636 ko || +0m00.00s || -516 ko | +0.00% | -0.22% 0m00.12s | 323588 ko | rupicola/bedrock2/compiler/src/compiler/ElfPrinter.vo | 0m00.13s | 329680 ko || -0m00.01s || -6092 ko | -7.69% | -1.84% 0m00.12s | 237540 ko | rupicola/bedrock2/compiler/src/compiler/MetricsToRiscv.vo | 0m00.11s | 238136 ko || +0m00.00s || -596 ko | +9.09% | -0.25% 0m00.12s | 290636 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncode.vo | 0m00.10s | 288060 ko || +0m00.01s || 2576 ko | +19.99% | +0.89% 0m00.12s | 236440 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadTests.vo | 0m00.09s | 238588 ko || +0m00.03s || -2148 ko | +33.33% | -0.90% 0m00.12s | 348376 ko | rupicola/src/Rupicola/Lib/Api.vo | 0m00.15s | 347100 ko || -0m00.03s || 1276 ko | -20.00% | +0.36% 0m00.12s | 364184 ko | rupicola/src/Rupicola/Lib/Invariants.vo | 0m00.10s | 362804 ko || +0m00.01s || 1380 ko | +19.99% | +0.38% 0m00.11s | 213948 ko | Util/ListUtil/NthExt.vo | 0m00.12s | 213808 ko || -0m00.00s || 140 ko | -8.33% | +0.06% 0m00.11s | 256956 ko | Util/NUtil/Sorting.vo | 0m00.16s | 258632 ko || -0m00.05s || -1676 ko | -31.25% | -0.64% 0m00.11s | 251384 ko | Util/Structures/Equalities/Option.vo | 0m00.13s | 251808 ko || -0m00.02s || -424 ko | -15.38% | -0.16% 0m00.11s | 203484 ko | coqutil/Macros/ident_to_string.vo | 0m00.11s | 202552 ko || +0m00.00s || 932 ko | +0.00% | +0.46% 0m00.11s | 254872 ko | coqutil/Tactics/fwd_list_hints.vo | 0m00.11s | 254272 ko || +0m00.00s || 600 ko | +0.00% | +0.23% 0m00.11s | 203384 ko | rupicola/bedrock2/bedrock2/src/bedrock2/PrintListByte.vo | 0m00.12s | 203056 ko || -0m00.00s || 328 ko | -8.33% | +0.16% 0m00.11s | 206000 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ident_to_string.vo | 0m00.13s | 206948 ko || -0m00.02s || -948 ko | -15.38% | -0.45% 0m00.11s | 179164 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadT.vo | 0m00.09s | 174608 ko || +0m00.02s || 4556 ko | +22.22% | +2.60% 0m00.11s | 181140 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/RegisterNameNotations.vo | 0m00.11s | 182792 ko || +0m00.00s || -1652 ko | +0.00% | -0.90% 0m00.11s | 237856 ko | rupicola/src/Rupicola/Lib/IdentParsing.vo | 0m00.11s | 236988 ko || +0m00.00s || 868 ko | +0.00% | +0.36% 0m00.10s | 318876 ko | Rewriter/Language/UnderLetsCacheProofs.vo | 0m00.13s | 319988 ko || -0m00.03s || -1112 ko | -23.07% | -0.34% 0m00.10s | 273344 ko | Rewriter/Util/Prod.vo | 0m00.10s | 274184 ko || +0m00.00s || -840 ko | +0.00% | -0.30% 0m00.10s | 209328 ko | Rewriter/Util/Strings/Ascii.vo | 0m00.11s | 209236 ko || -0m00.00s || 92 ko | -9.09% | +0.04% 0m00.10s | 179456 ko | Util/ListUtil/ForallIn.vo | 0m00.09s | 180468 ko || +0m00.01s || -1012 ko | +11.11% | -0.56% 0m00.10s | 250080 ko | Util/ListUtil/Partition.vo | 0m00.10s | 250480 ko || +0m00.00s || -400 ko | +0.00% | -0.15% 0m00.10s | 331604 ko | Util/Sorting/Sorted/Proper.vo | 0m00.14s | 332000 ko || -0m00.04s || -396 ko | -28.57% | -0.11% 0m00.10s | 219252 ko | coqutil/Macros/WithQualName.vo | 0m00.09s | 218576 ko || +0m00.01s || 676 ko | +11.11% | +0.30% 0m00.10s | 254628 ko | coqutil/Tactics/fwd_map_hints.vo | 0m00.13s | 255880 ko || -0m00.03s || -1252 ko | -23.07% | -0.48% 0m00.10s | 188696 ko | coqutil/Z/div_mod_to_equations.vo | 0m00.11s | 188564 ko || -0m00.00s || 132 ko | -9.09% | +0.07% 0m00.10s | 178580 ko | coqutil/Z/div_to_equations.vo | 0m00.11s | 178176 ko || -0m00.00s || 404 ko | -9.09% | +0.22% 0m00.10s | 221232 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Syntax.vo | 0m00.11s | 219988 ko || -0m00.00s || 1244 ko | -9.09% | +0.56% 0m00.10s | 194628 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Variables.vo | 0m00.12s | 195800 ko || -0m00.01s || -1172 ko | -16.66% | -0.59% 0m00.10s | 169212 ko | rupicola/bedrock2/bedrock2/src/bedrock2/WordNotations.vo | 0m00.07s | 169276 ko || +0m00.03s || -64 ko | +42.85% | -0.03% 0m00.10s | 287472 ko | test/SortedListString_test.vo | 0m00.08s | 291584 ko || +0m00.02s || -4112 ko | +25.00% | -1.41% 0m00.09s | 266128 ko | Coqprime/N/NatAux.vo | 0m00.10s | 265500 ko || -0m00.01s || 628 ko | -10.00% | +0.23% 0m00.09s | 57128 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.12s | 55480 ko || -0m00.03s || 1648 ko | -25.00% | +2.97% 0m00.09s | 55204 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.14s | 55168 ko || -0m00.05s || 36 ko | -35.71% | +0.06% 0m00.09s | 270152 ko | Rewriter/Util/OptionList.vo | 0m00.08s | 269944 ko || +0m00.00s || 208 ko | +12.49% | +0.07% 0m00.09s | 220800 ko | Rewriter/Util/Sigma.vo | 0m00.10s | 220552 ko || -0m00.01s || 248 ko | -10.00% | +0.11% 0m00.09s | 271372 ko | Rewriter/Util/Strings/Parse/Common.vo | 0m00.11s | 270776 ko || -0m00.02s || 596 ko | -18.18% | +0.22% 0m00.09s | 229256 ko | Util/Sigma.vo | 0m00.07s | 228268 ko || +0m00.01s || 988 ko | +28.57% | +0.43% 0m00.09s | 183024 ko | Util/ZUtil/Notations.vo | 0m00.10s | 182360 ko || -0m00.01s || 664 ko | -10.00% | +0.36% 0m00.09s | 238456 ko | Util/ZUtil/ZSimplify.vo | 0m00.10s | 238836 ko || -0m00.01s || -380 ko | -10.00% | -0.15% 0m00.09s | 156760 ko | coqutil/Datatypes/HList.vo | 0m00.09s | 157608 ko || +0m00.00s || -848 ko | +0.00% | -0.53% 0m00.09s | 205720 ko | coqutil/Macros/WithBaseName.vo | 0m00.10s | 207196 ko || -0m00.01s || -1476 ko | -10.00% | -0.71% 0m00.09s | 258676 ko | coqutil/Word/Interface.vo | 0m00.12s | 258700 ko || -0m00.03s || -24 ko | -25.00% | -0.00% 0m00.09s | 120512 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ListPushPullIf.vo | 0m00.08s | 117412 ko || +0m00.00s || 3100 ko | +12.49% | +2.64% 0m00.09s | 182108 ko | rupicola/bedrock2/bedrock2/src/bedrock2/LogSidecond.vo | 0m00.10s | 182020 ko || -0m00.01s || 88 ko | -10.00% | +0.04% 0m00.09s | 283988 ko | rupicola/bedrock2/bedrock2/src/bedrock2/TracePredicate.vo | 0m00.15s | 284876 ko || -0m00.06s || -888 ko | -40.00% | -0.31% 0m00.09s | 206656 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/FreeMonad.vo | 0m00.08s | 205592 ko || +0m00.00s || 1064 ko | +12.49% | +0.51% 0m00.09s | 153488 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/JMonad.vo | 0m00.09s | 155124 ko || +0m00.00s || -1636 ko | +0.00% | -1.05% 0m00.09s | 190800 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MMIOTrace.vo | 0m00.09s | 190668 ko || +0m00.00s || 132 ko | +0.00% | +0.06% 0m00.09s | 189400 ko | rupicola/src/Rupicola/Lib/Gensym.vo | 0m00.08s | 190800 ko || +0m00.00s || -1400 ko | +12.49% | -0.73% 0m00.08s | 182888 ko | Util/ListUtil/PermutationCompat.vo | 0m00.09s | 182320 ko || -0m00.00s || 568 ko | -11.11% | +0.31% 0m00.08s | 198284 ko | Util/PrimitiveProd.vo | 0m00.05s | 198436 ko || +0m00.03s || -152 ko | +60.00% | -0.07% 0m00.08s | 218476 ko | Util/Relations.vo | 0m00.08s | 217268 ko || +0m00.00s || 1208 ko | +0.00% | +0.55% 0m00.08s | 111080 ko | Util/Tactics/AllInstances.vo | 0m00.08s | 112456 ko || +0m00.00s || -1376 ko | +0.00% | -1.22% 0m00.08s | 95776 ko | Util/Tactics/SpecializeUnderBindersBy.vo | 0m00.06s | 94744 ko || +0m00.02s || 1032 ko | +33.33% | +1.08% 0m00.08s | 243012 ko | Util/Telescope/Equality.vo | 0m00.06s | 242968 ko || +0m00.02s || 44 ko | +33.33% | +0.01% 0m00.08s | 190116 ko | coqutil/Tactics/destr.vo | 0m00.09s | 188888 ko || -0m00.00s || 1228 ko | -11.11% | +0.65% 0m00.08s | 201512 ko | coqutil/Tactics/reference_to_string.vo | 0m00.10s | 201816 ko || -0m00.02s || -304 ko | -20.00% | -0.15% 0m00.08s | 139124 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/ExtensibleRecords.vo | 0m00.07s | 137288 ko || +0m00.00s || 1836 ko | +14.28% | +1.33% 0m00.07s | 121496 ko | Rewriter/Language/Pre.vo | 0m00.06s | 121340 ko || +0m00.01s || 156 ko | +16.66% | +0.12% 0m00.07s | 119496 ko | Rewriter/Language/PreCommon.vo | 0m00.07s | 119152 ko || +0m00.00s || 344 ko | +0.00% | +0.28% 0m00.07s | 116848 ko | Rewriter/Util/PrimitiveHList.vo | 0m00.07s | 116192 ko || +0m00.00s || 656 ko | +0.00% | +0.56% 0m00.07s | 191288 ko | Rewriter/Util/PrimitiveProd.vo | 0m00.06s | 191184 ko || +0m00.01s || 104 ko | +16.66% | +0.05% 0m00.07s | 157976 ko | Rewriter/Util/PrimitiveSigma.vo | 0m00.04s | 158756 ko || +0m00.03s || -780 ko | +75.00% | -0.49% 0m00.07s | 68124 ko | Rewriter/Util/Tactics2/Char.vo | 0m00.05s | 68332 ko || +0m00.02s || -208 ko | +40.00% | -0.30% 0m00.07s | 156736 ko | Util/Bool.vo | 0m00.06s | 157828 ko || +0m00.01s || -1092 ko | +16.66% | -0.69% 0m00.07s | 111700 ko | Util/ListUtil/CombineExtend.vo | 0m00.06s | 111540 ko || +0m00.01s || 160 ko | +16.66% | +0.14% 0m00.07s | 111900 ko | Util/ListUtil/Concat.vo | 0m00.06s | 112676 ko || +0m00.01s || -776 ko | +16.66% | -0.68% 0m00.07s | 115244 ko | Util/ListUtil/FoldMap.vo | 0m00.07s | 114024 ko || +0m00.00s || 1220 ko | +0.00% | +1.06% 0m00.07s | 118112 ko | Util/PrimitiveHList.vo | 0m00.06s | 117656 ko || +0m00.01s || 456 ko | +16.66% | +0.38% 0m00.07s | 234208 ko | Util/Structures/Equalities.vo | 0m00.07s | 234152 ko || +0m00.00s || 56 ko | +0.00% | +0.02% 0m00.07s | 150932 ko | Util/Structures/Equalities/Iso.vo | 0m00.07s | 150448 ko || +0m00.00s || 484 ko | +0.00% | +0.32% 0m00.07s | 110468 ko | Util/Tactics/AllSuccesses.vo | 0m00.08s | 112904 ko || -0m00.00s || -2436 ko | -12.49% | -2.15% 0m00.07s | 182032 ko | Util/Telescope/Instances.vo | 0m00.08s | 184668 ko || -0m00.00s || -2636 ko | -12.49% | -1.42% 0m00.07s | 141460 ko | coqutil/Tactics/Records.vo | 0m00.07s | 141292 ko || +0m00.00s || 168 ko | +0.00% | +0.11% 0m00.07s | 105312 ko | rupicola/bedrock2/bedrock2/src/bedrock2/ReversedListNotations.vo | 0m00.06s | 108592 ko || +0m00.01s || -3280 ko | +16.66% | -3.02% 0m00.07s | 245584 ko | rupicola/bedrock2/bedrock2/src/bedrock2/find_hyp.vo | 0m00.06s | 245504 ko || +0m00.01s || 80 ko | +16.66% | +0.03% 0m00.07s | 114328 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/MonadNotations.vo | 0m00.07s | 112492 ko || +0m00.00s || 1836 ko | +0.00% | +1.63% 0m00.06s | 138908 ko | Rewriter/Rewriter/Examples/PerfTesting/ListRectInstances.vo | 0m00.08s | 138732 ko || -0m00.02s || 176 ko | -25.00% | +0.12% 0m00.06s | 68400 ko | Rewriter/Util/Tactics2/DestCast.vo | 0m00.04s | 69044 ko || +0m00.01s || -644 ko | +49.99% | -0.93% 0m00.06s | 107180 ko | Util/Compose.vo | 0m00.06s | 107776 ko || +0m00.00s || -596 ko | +0.00% | -0.55% 0m00.06s | 106404 ko | Util/LetIn.vo | 0m00.04s | 105940 ko || +0m00.01s || 464 ko | +49.99% | +0.43% 0m00.06s | 109352 ko | Util/ListUtil/RemoveN.vo | 0m00.08s | 110088 ko || -0m00.02s || -736 ko | -25.00% | -0.66% 0m00.06s | 116012 ko | Util/Structures/Equalities/Unit.vo | 0m00.06s | 115992 ko || +0m00.00s || 20 ko | +0.00% | +0.01% 0m00.06s | 93132 ko | Util/Tactics/InHypUnderBindersDo.vo | 0m00.04s | 93028 ko || +0m00.01s || 104 ko | +49.99% | +0.11% 0m00.06s | 115672 ko | coqutil/Sorting/Permutation.vo | 0m00.05s | 115620 ko || +0m00.00s || 52 ko | +19.99% | +0.04% 0m00.05s | 128488 ko | Rewriter/Util/Bool.vo | 0m00.05s | 129752 ko || +0m00.00s || -1264 ko | +0.00% | -0.97% 0m00.05s | 98052 ko | Rewriter/Util/LetIn.vo | 0m00.05s | 97996 ko || +0m00.00s || 56 ko | +0.00% | +0.05% 0m00.05s | 96260 ko | Rewriter/Util/Logic/ExistsEqAnd.vo | 0m00.05s | 96100 ko || +0m00.00s || 160 ko | +0.00% | +0.16% 0m00.05s | 112028 ko | Rewriter/Util/Sigma/Related.vo | 0m00.04s | 113856 ko || +0m00.01s || -1828 ko | +25.00% | -1.60% 0m00.05s | 68888 ko | Rewriter/Util/Tactics2/DestCoFix.vo | 0m00.02s | 69356 ko || +0m00.03s || -468 ko | +150.00% | -0.67% 0m00.05s | 67800 ko | Rewriter/Util/Tactics2/DestConstructor.vo | 0m00.05s | 68768 ko || +0m00.00s || -968 ko | +0.00% | -1.40% 0m00.05s | 70504 ko | Rewriter/Util/Tactics2/DestEvar.vo | 0m00.04s | 69384 ko || +0m00.01s || 1120 ko | +25.00% | +1.61% 0m00.05s | 68888 ko | Rewriter/Util/Tactics2/FixNotationsForPerformance.vo | 0m00.04s | 67884 ko || +0m00.01s || 1004 ko | +25.00% | +1.47% 0m00.05s | 69636 ko | Rewriter/Util/Tactics2/Head.vo | 0m00.03s | 69896 ko || +0m00.02s || -260 ko | +66.66% | -0.37% 0m00.05s | 68760 ko | Rewriter/Util/Tactics2/Ident.vo | 0m00.05s | 68324 ko || +0m00.00s || 436 ko | +0.00% | +0.63% 0m00.05s | 69472 ko | Rewriter/Util/Tactics2/Iterate.vo | 0m00.03s | 68428 ko || +0m00.02s || 1044 ko | +66.66% | +1.52% 0m00.05s | 69324 ko | Rewriter/Util/Tactics2/Ltac1.vo | 0m00.05s | 68404 ko || +0m00.00s || 920 ko | +0.00% | +1.34% 0m00.05s | 69460 ko | Rewriter/Util/Tactics2/Notations.vo | 0m00.03s | 67912 ko || +0m00.02s || 1548 ko | +66.66% | +2.27% 0m00.05s | 111892 ko | Util/DynList.vo | 0m00.07s | 112060 ko || -0m00.02s || -168 ko | -28.57% | -0.14% 0m00.05s | 131448 ko | Util/ErrorT.vo | 0m00.04s | 131624 ko || +0m00.01s || -176 ko | +25.00% | -0.13% 0m00.05s | 106336 ko | Util/Structures/Equalities/Project.vo | 0m00.07s | 108752 ko || -0m00.02s || -2416 ko | -28.57% | -2.22% 0m00.05s | 98212 ko | Util/Tactics/GeneralizeOverHoles.vo | 0m00.06s | 97644 ko || -0m00.00s || 568 ko | -16.66% | +0.58% 0m00.05s | 104660 ko | Util/Telescope/Core.vo | 0m00.04s | 104684 ko || +0m00.01s || -24 ko | +25.00% | -0.02% 0m00.05s | 67876 ko | coqutil/Ltac2Lib/Ident.vo | 0m00.04s | 67516 ko || +0m00.01s || 360 ko | +25.00% | +0.53% 0m00.05s | 67968 ko | coqutil/Ltac2Lib/Std.vo | 0m00.06s | 66588 ko || -0m00.00s || 1380 ko | -16.66% | +2.07% 0m00.05s | 66528 ko | coqutil/Tactics/RecordEta.vo | 0m00.03s | 67692 ko || +0m00.02s || -1164 ko | +66.66% | -1.71% 0m00.05s | 69564 ko | coqutil/Tactics/fold_hyps.vo | 0m00.05s | 66808 ko || +0m00.00s || 2756 ko | +0.00% | +4.12% 0m00.05s | 66768 ko | coqutil/Tactics/foreach_hyp.vo | 0m00.04s | 66884 ko || +0m00.01s || -116 ko | +25.00% | -0.17% 0m00.05s | 66760 ko | coqutil/Tactics/grepeat.vo | 0m00.05s | 67400 ko || +0m00.00s || -640 ko | +0.00% | -0.94% 0m00.04s | 75952 ko | Rewriter/Util/CPSNotations.vo | 0m00.03s | 75508 ko || +0m00.01s || 444 ko | +33.33% | +0.58% 0m00.04s | 139388 ko | Rewriter/Util/Equality.vo | 0m00.05s | 139336 ko || -0m00.01s || 52 ko | -20.00% | +0.03% 0m00.04s | 90344 ko | Rewriter/Util/HProp.vo | 0m00.05s | 90352 ko || -0m00.01s || -8 ko | -20.00% | -0.00% 0m00.04s | 80816 ko | Rewriter/Util/Logic/ProdForall.vo | 0m00.03s | 81716 ko || +0m00.01s || -900 ko | +33.33% | -1.10% 0m00.04s | 84772 ko | Rewriter/Util/Pointed.vo | 0m00.04s | 85808 ko || +0m00.00s || -1036 ko | +0.00% | -1.20% 0m00.04s | 62848 ko | Rewriter/Util/Tactics/GetGoal.vo | 0m00.02s | 62552 ko || +0m00.02s || 296 ko | +100.00% | +0.47% 0m00.04s | 68032 ko | Rewriter/Util/Tactics2/Constr/Unsafe/MakeAbbreviations.vo | 0m00.03s | 68168 ko || +0m00.01s || -136 ko | +33.33% | -0.19% 0m00.04s | 69044 ko | Rewriter/Util/Tactics2/DestApp.vo | 0m00.03s | 68400 ko || +0m00.01s || 644 ko | +33.33% | +0.94% 0m00.04s | 69228 ko | Rewriter/Util/Tactics2/DestMeta.vo | 0m00.03s | 70572 ko || +0m00.01s || -1344 ko | +33.33% | -1.90% 0m00.04s | 68920 ko | Rewriter/Util/Tactics2/DestRel.vo | 0m00.04s | 70328 ko || +0m00.00s || -1408 ko | +0.00% | -2.00% 0m00.04s | 68996 ko | Rewriter/Util/Tactics2/DestVar.vo | 0m00.03s | 67704 ko || +0m00.01s || 1292 ko | +33.33% | +1.90% 0m00.04s | 69008 ko | Rewriter/Util/Tactics2/HeadReference.vo | 0m00.04s | 68624 ko || +0m00.00s || 384 ko | +0.00% | +0.55% 0m00.04s | 72544 ko | Rewriter/Util/Tactics2/InFreshContext.vo | 0m00.04s | 68644 ko || +0m00.00s || 3900 ko | +0.00% | +5.68% 0m00.04s | 69752 ko | Rewriter/Util/Tactics2/InstantiateEvar.vo | 0m00.02s | 68128 ko || +0m00.02s || 1624 ko | +100.00% | +2.38% 0m00.04s | 69608 ko | Rewriter/Util/Tactics2/List.vo | 0m00.03s | 68200 ko || +0m00.01s || 1408 ko | +33.33% | +2.06% 0m00.04s | 67804 ko | Rewriter/Util/Tactics2/Message.vo | 0m00.05s | 68224 ko || -0m00.01s || -420 ko | -20.00% | -0.61% 0m00.04s | 68520 ko | Rewriter/Util/Tactics2/Proj.vo | 0m00.04s | 68276 ko || +0m00.00s || 244 ko | +0.00% | +0.35% 0m00.04s | 68968 ko | Rewriter/Util/Tactics2/ReplaceByPattern.vo | 0m00.04s | 69424 ko || +0m00.00s || -456 ko | +0.00% | -0.65% 0m00.04s | 66764 ko | Rewriter/Util/plugins/Ltac2Extra.vo | 0m00.05s | 68360 ko || -0m00.01s || -1596 ko | -20.00% | -2.33% 0m00.04s | 79196 ko | Util/Bool/LeCompat.vo | 0m00.03s | 80040 ko || +0m00.01s || -844 ko | +33.33% | -1.05% 0m00.04s | 146016 ko | Util/Equality.vo | 0m00.04s | 146980 ko || +0m00.00s || -964 ko | +0.00% | -0.65% 0m00.04s | 71584 ko | Util/Isomorphism.vo | 0m00.03s | 69752 ko || +0m00.01s || 1832 ko | +33.33% | +2.62% 0m00.04s | 97360 ko | Util/Notations.vo | 0m00.02s | 97892 ko || +0m00.02s || -532 ko | +100.00% | -0.54% 0m00.04s | 78480 ko | Util/Tactics/BreakMatch.vo | 0m00.04s | 78592 ko || +0m00.00s || -112 ko | +0.00% | -0.14% 0m00.04s | 69124 ko | Util/Tactics/ConstrFail.vo | 0m00.01s | 68832 ko || +0m00.03s || 292 ko | +300.00% | +0.42% 0m00.04s | 89468 ko | Util/Tactics/DebugPrint.vo | 0m00.03s | 88532 ko || +0m00.01s || 936 ko | +33.33% | +1.05% 0m00.04s | 83176 ko | Util/Tactics/DestructHead.vo | 0m00.04s | 82056 ko || +0m00.00s || 1120 ko | +0.00% | +1.36% 0m00.04s | 75596 ko | Util/Tactics/DoWithHyp.vo | 0m00.03s | 75192 ko || +0m00.01s || 404 ko | +33.33% | +0.53% 0m00.04s | 69196 ko | Util/Tactics/HasBody.vo | 0m00.03s | 69320 ko || +0m00.01s || -124 ko | +33.33% | -0.17% 0m00.04s | 97608 ko | Util/Tactics/RewriteHyp.vo | 0m00.05s | 95408 ko || -0m00.01s || 2200 ko | -20.00% | +2.30% 0m00.04s | 74188 ko | Util/Tactics/SetoidSubst.vo | 0m00.03s | 72016 ko || +0m00.01s || 2172 ko | +33.33% | +3.01% 0m00.04s | 78288 ko | Util/Tactics/Zeta1.vo | 0m00.04s | 79444 ko || +0m00.00s || -1156 ko | +0.00% | -1.45% 0m00.04s | 67520 ko | coqutil/Ltac2Lib/Char.vo | 0m00.03s | 67148 ko || +0m00.01s || 372 ko | +33.33% | +0.55% 0m00.04s | 65908 ko | coqutil/Ltac2Lib/Control.vo | 0m00.03s | 68200 ko || +0m00.01s || -2292 ko | +33.33% | -3.36% 0m00.04s | 66192 ko | coqutil/Ltac2Lib/Failf.vo | 0m00.03s | 67500 ko || +0m00.01s || -1308 ko | +33.33% | -1.93% 0m00.04s | 66960 ko | coqutil/Ltac2Lib/List.vo | 0m00.04s | 66776 ko || +0m00.00s || 184 ko | +0.00% | +0.27% 0m00.04s | 67932 ko | coqutil/Ltac2Lib/String.vo | 0m00.04s | 66740 ko || +0m00.00s || 1192 ko | +0.00% | +1.78% 0m00.04s | 67504 ko | coqutil/Tactics/ParamRecords.vo | 0m00.04s | 66328 ko || +0m00.00s || 1176 ko | +0.00% | +1.77% 0m00.04s | 79028 ko | coqutil/Tactics/eplace.vo | 0m00.02s | 79072 ko || +0m00.02s || -44 ko | +100.00% | -0.05% 0m00.04s | 67316 ko | coqutil/Tactics/ident_ops.vo | 0m00.04s | 65860 ko || +0m00.00s || 1456 ko | +0.00% | +2.21% 0m00.04s | 62480 ko | coqutil/Tactics/let_binding_to_eq.vo | 0m00.03s | 62404 ko || +0m00.01s || 76 ko | +33.33% | +0.12% 0m00.04s | 135648 ko | coqutil/Tactics/pattern_tuple.vo | 0m00.03s | 133200 ko || +0m00.01s || 2448 ko | +33.33% | +1.83% 0m00.04s | 85336 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Hexdump.vo | 0m00.05s | 85640 ko || -0m00.01s || -304 ko | -20.00% | -0.35% 0m00.04s | 74644 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/runsToNonDet.vo | 0m00.03s | 76100 ko || +0m00.01s || -1456 ko | +33.33% | -1.91% 0m00.03s | 70296 ko | Rewriter/Util/Bool/Equality.vo | 0m00.01s | 69968 ko || +0m00.01s || 328 ko | +199.99% | +0.46% 0m00.03s | 74064 ko | Rewriter/Util/Comparison.vo | 0m00.03s | 73976 ko || +0m00.00s || 88 ko | +0.00% | +0.11% 0m00.03s | 73508 ko | Rewriter/Util/FixCoqMistakes.vo | 0m00.03s | 73772 ko || +0m00.00s || -264 ko | +0.00% | -0.35% 0m00.03s | 83036 ko | Rewriter/Util/IffT.vo | 0m00.03s | 82524 ko || +0m00.00s || 512 ko | +0.00% | +0.62% 0m00.03s | 64608 ko | Rewriter/Util/InductiveHList.vo | 0m00.03s | 64240 ko || +0m00.00s || 368 ko | +0.00% | +0.57% 0m00.03s | 84720 ko | Rewriter/Util/Notations.vo | 0m00.02s | 84148 ko || +0m00.00s || 572 ko | +49.99% | +0.67% 0m00.03s | 62308 ko | Rewriter/Util/Tactics/ConstrFail.vo | 0m00.01s | 61232 ko || +0m00.01s || 1076 ko | +199.99% | +1.75% 0m00.03s | 81440 ko | Rewriter/Util/Tactics/DebugPrint.vo | 0m00.02s | 80536 ko || +0m00.00s || 904 ko | +49.99% | +1.12% 0m00.03s | 67040 ko | Rewriter/Util/Tactics/DoWithHyp.vo | 0m00.02s | 66252 ko || +0m00.00s || 788 ko | +49.99% | +1.18% 0m00.03s | 60944 ko | Rewriter/Util/Tactics/EvarNormalize.vo | 0m00.02s | 65176 ko || +0m00.00s || -4232 ko | +49.99% | -6.49% 0m00.03s | 66692 ko | Rewriter/Util/Tactics/HeadUnderBinders.vo | 0m00.02s | 66528 ko || +0m00.00s || 164 ko | +49.99% | +0.24% 0m00.03s | 66864 ko | Rewriter/Util/Tactics/RunTacticAsConstr.vo | 0m00.02s | 66140 ko || +0m00.00s || 724 ko | +49.99% | +1.09% 0m00.03s | 63316 ko | Rewriter/Util/Tactics/SetoidSubst.vo | 0m00.03s | 64212 ko || +0m00.00s || -896 ko | +0.00% | -1.39% 0m00.03s | 65760 ko | Rewriter/Util/Tactics/SpecializeAllWays.vo | 0m00.02s | 66764 ko || +0m00.00s || -1004 ko | +49.99% | -1.50% 0m00.03s | 68824 ko | Rewriter/Util/Tactics/SplitInContext.vo | 0m00.02s | 67916 ko || +0m00.00s || 908 ko | +49.99% | +1.33% 0m00.03s | 63004 ko | Rewriter/Util/Tactics/Test.vo | 0m00.02s | 62164 ko || +0m00.00s || 840 ko | +49.99% | +1.35% 0m00.03s | 67704 ko | Rewriter/Util/Tactics/TransparentAssert.vo | 0m00.03s | 62292 ko || +0m00.00s || 5412 ko | +0.00% | +8.68% 0m00.03s | 68964 ko | Rewriter/Util/Tactics2/Array.vo | 0m00.03s | 68076 ko || +0m00.00s || 888 ko | +0.00% | +1.30% 0m00.03s | 69060 ko | Rewriter/Util/Tactics2/Constr.vo | 0m00.04s | 67768 ko || -0m00.01s || 1292 ko | -25.00% | +1.90% 0m00.03s | 69196 ko | Rewriter/Util/Tactics2/DecomposeLambda.vo | 0m00.03s | 70112 ko || +0m00.00s || -916 ko | +0.00% | -1.30% 0m00.03s | 68336 ko | Rewriter/Util/Tactics2/DestCase.vo | 0m00.04s | 68276 ko || -0m00.01s || 60 ko | -25.00% | +0.08% 0m00.03s | 68412 ko | Rewriter/Util/Tactics2/DestFix.vo | 0m00.04s | 68344 ko || -0m00.01s || 68 ko | -25.00% | +0.09% 0m00.03s | 69416 ko | Rewriter/Util/Tactics2/DestInd.vo | 0m00.05s | 69656 ko || -0m00.02s || -240 ko | -40.00% | -0.34% 0m00.03s | 68284 ko | Rewriter/Util/Tactics2/DestLetIn.vo | 0m00.03s | 68928 ko || +0m00.00s || -644 ko | +0.00% | -0.93% 0m00.03s | 69860 ko | Rewriter/Util/Tactics2/DestProd.vo | 0m00.03s | 72200 ko || +0m00.00s || -2340 ko | +0.00% | -3.24% 0m00.03s | 68464 ko | Rewriter/Util/Tactics2/DestProj.vo | 0m00.04s | 68392 ko || -0m00.01s || 72 ko | -25.00% | +0.10% 0m00.03s | 70304 ko | Rewriter/Util/Tactics2/Option.vo | 0m00.03s | 68840 ko || +0m00.00s || 1464 ko | +0.00% | +2.12% 0m00.03s | 63416 ko | Rewriter/Util/plugins/StrategyTactic.vo | 0m00.03s | 62328 ko || +0m00.00s || 1088 ko | +0.00% | +1.74% 0m00.03s | 79420 ko | Util/Bool/Equality.vo | 0m00.03s | 79084 ko || +0m00.00s || 336 ko | +0.00% | +0.42% 0m00.03s | 84140 ko | Util/CPSNotations.vo | 0m00.03s | 83408 ko || +0m00.00s || 732 ko | +0.00% | +0.87% 0m00.03s | 81316 ko | Util/Comparison.vo | 0m00.02s | 81672 ko || +0m00.00s || -356 ko | +49.99% | -0.43% 0m00.03s | 80152 ko | Util/FixCoqMistakes.vo | 0m00.03s | 80592 ko || +0m00.00s || -440 ko | +0.00% | -0.54% 0m00.03s | 70872 ko | Util/FueledLUB.vo | 0m00.02s | 72020 ko || +0m00.00s || -1148 ko | +49.99% | -1.59% 0m00.03s | 96824 ko | Util/HProp.vo | 0m00.05s | 97780 ko || -0m00.02s || -956 ko | -40.00% | -0.97% 0m00.03s | 89560 ko | Util/IffT.vo | 0m00.03s | 90428 ko || +0m00.00s || -868 ko | +0.00% | -0.95% 0m00.03s | 87916 ko | Util/Logic.vo | 0m00.04s | 87332 ko || -0m00.01s || 584 ko | -25.00% | +0.66% 0m00.03s | 78072 ko | Util/Logic/Exists.vo | 0m00.03s | 77748 ko || +0m00.00s || 324 ko | +0.00% | +0.41% 0m00.03s | 79272 ko | Util/Logic/Forall.vo | 0m00.04s | 79536 ko || -0m00.01s || -264 ko | -25.00% | -0.33% 0m00.03s | 93732 ko | Util/Pointed.vo | 0m00.03s | 93180 ko || +0m00.00s || 552 ko | +0.00% | +0.59% 0m00.03s | 69248 ko | Util/Tactics/Contains.vo | 0m00.03s | 69088 ko || +0m00.00s || 160 ko | +0.00% | +0.23% 0m00.03s | 75848 ko | Util/Tactics/DestructHyps.vo | 0m00.04s | 76352 ko || -0m00.01s || -504 ko | -25.00% | -0.66% 0m00.03s | 74912 ko | Util/Tactics/ETransitivity.vo | 0m00.01s | 73988 ko || +0m00.01s || 924 ko | +199.99% | +1.24% 0m00.03s | 73340 ko | Util/Tactics/Head.vo | 0m00.02s | 74056 ko || +0m00.00s || -716 ko | +49.99% | -0.96% 0m00.03s | 69284 ko | Util/Tactics/NormalizeCommutativeIdentifier.vo | 0m00.03s | 70280 ko || +0m00.00s || -996 ko | +0.00% | -1.41% 0m00.03s | 69644 ko | Util/Tactics/OnSubterms.vo | 0m00.03s | 69344 ko || +0m00.00s || 300 ko | +0.00% | +0.43% 0m00.03s | 70812 ko | Util/Tactics/PrintContext.vo | 0m00.03s | 70200 ko || +0m00.00s || 612 ko | +0.00% | +0.87% 0m00.03s | 69732 ko | Util/Tactics/Revert.vo | 0m00.03s | 70148 ko || +0m00.00s || -416 ko | +0.00% | -0.59% 0m00.03s | 74500 ko | Util/Tactics/RunTacticAsConstr.vo | 0m00.03s | 75528 ko || +0m00.00s || -1028 ko | +0.00% | -1.36% 0m00.03s | 71468 ko | Util/Tactics/SetEvars.vo | 0m00.04s | 70084 ko || -0m00.01s || 1384 ko | -25.00% | +1.97% 0m00.03s | 75968 ko | Util/Tactics/SpecializeBy.vo | 0m00.03s | 74372 ko || +0m00.00s || 1596 ko | +0.00% | +2.14% 0m00.03s | 75740 ko | Util/Tactics/SplitInContext.vo | 0m00.03s | 76656 ko || +0m00.00s || -916 ko | +0.00% | -1.19% 0m00.03s | 70092 ko | Util/Tactics/SubstLet.vo | 0m00.03s | 70208 ko || +0m00.00s || -116 ko | +0.00% | -0.16% 0m00.03s | 75964 ko | Util/Tactics/UniquePose.vo | 0m00.03s | 76148 ko || +0m00.00s || -184 ko | +0.00% | -0.24% 0m00.03s | 75968 ko | Util/Unit.vo | 0m00.03s | 76808 ko || +0m00.00s || -840 ko | +0.00% | -1.09% 0m00.03s | 88880 ko | coqutil/Datatypes/Bool.vo | 0m00.03s | 87868 ko || +0m00.00s || 1012 ko | +0.00% | +1.15% 0m00.03s | 108368 ko | coqutil/Datatypes/Option.vo | 0m00.04s | 106852 ko || -0m00.01s || 1516 ko | -25.00% | +1.41% 0m00.03s | 93192 ko | coqutil/Datatypes/Prod.vo | 0m00.04s | 91508 ko || -0m00.01s || 1684 ko | -25.00% | +1.84% 0m00.03s | 125488 ko | coqutil/Lift1Prop.vo | 0m00.04s | 126252 ko || -0m00.01s || -764 ko | -25.00% | -0.60% 0m00.03s | 65932 ko | coqutil/Ltac2Lib/Constr.vo | 0m00.05s | 66560 ko || -0m00.02s || -628 ko | -40.00% | -0.94% 0m00.03s | 67832 ko | coqutil/Ltac2Lib/Ltac2.vo | 0m00.03s | 65592 ko || +0m00.00s || 2240 ko | +0.00% | +3.41% 0m00.03s | 67240 ko | coqutil/Ltac2Lib/Notations.vo | 0m00.03s | 68176 ko || +0m00.00s || -936 ko | +0.00% | -1.37% 0m00.03s | 66560 ko | coqutil/Ltac2Lib/Pervasives.vo | 0m00.04s | 66716 ko || -0m00.01s || -156 ko | -25.00% | -0.23% 0m00.03s | 67584 ko | coqutil/Ltac2Lib/rdelta.vo | 0m00.02s | 65920 ko || +0m00.00s || 1664 ko | +49.99% | +2.52% 0m00.03s | 72204 ko | coqutil/Macros/symmetry.vo | 0m00.03s | 73908 ko || +0m00.00s || -1704 ko | +0.00% | -2.30% 0m00.03s | 99600 ko | coqutil/Semantics/OmniSmallstepCombinators.vo | 0m00.03s | 100112 ko || +0m00.00s || -512 ko | +0.00% | -0.51% 0m00.03s | 61080 ko | coqutil/Tactics/ProveInversion.vo | 0m00.02s | 60920 ko || +0m00.00s || 160 ko | +49.99% | +0.26% 0m00.03s | 61556 ko | coqutil/Tactics/eabstract.vo | 0m00.01s | 61672 ko || +0m00.01s || -116 ko | +199.99% | -0.18% 0m00.03s | 66432 ko | coqutil/Tactics/evar_free.vo | 0m00.04s | 67088 ko || -0m00.01s || -656 ko | -25.00% | -0.97% 0m00.03s | 62192 ko | coqutil/Tactics/invert_hyp.vo | 0m00.01s | 61608 ko || +0m00.01s || 584 ko | +199.99% | +0.94% 0m00.03s | 63560 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Markers.vo | 0m00.04s | 65032 ko || -0m00.01s || -1472 ko | -25.00% | -2.26% 0m00.03s | 63396 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Notations.vo | 0m00.02s | 63060 ko || +0m00.00s || 336 ko | +49.99% | +0.53% 0m00.03s | 70344 ko | rupicola/bedrock2/bedrock2/src/bedrock2/SuppressibleWarnings.vo | 0m00.03s | 70012 ko || +0m00.00s || 332 ko | +0.00% | +0.47% 0m00.03s | 62088 ko | rupicola/bedrock2/bedrock2/src/bedrock2/enable_frame_trick.vo | 0m00.02s | 61812 ko || +0m00.00s || 276 ko | +49.99% | +0.44% 0m00.03s | 74648 ko | rupicola/bedrock2/compiler/src/compiler/util/Misc.vo | 0m00.03s | 75676 ko || +0m00.00s || -1028 ko | +0.00% | -1.35% 0m00.02s | 61868 ko | Coqprime/Tactic/Tactic.vo | 0m00.01s | 62208 ko || +0m00.01s || -340 ko | +100.00% | -0.54% 0m00.02s | 61980 ko | Rewriter/Util/GlobalSettings.vo | 0m00.03s | 62244 ko || -0m00.00s || -264 ko | -33.33% | -0.42% 0m00.02s | 70500 ko | Rewriter/Util/Tactics/BreakMatch.vo | 0m00.04s | 70560 ko || -0m00.02s || -60 ko | -50.00% | -0.08% 0m00.02s | 64128 ko | Rewriter/Util/Tactics/CPSId.vo | 0m00.02s | 63396 ko || +0m00.00s || 732 ko | +0.00% | +1.15% 0m00.02s | 65956 ko | Rewriter/Util/Tactics/CacheTerm.vo | 0m00.02s | 66500 ko || +0m00.00s || -544 ko | +0.00% | -0.81% 0m00.02s | 63224 ko | Rewriter/Util/Tactics/ClearFree.vo | 0m00.03s | 61384 ko || -0m00.00s || 1840 ko | -33.33% | +2.99% 0m00.02s | 65288 ko | Rewriter/Util/Tactics/Contains.vo | 0m00.02s | 61716 ko || +0m00.00s || 3572 ko | +0.00% | +5.78% 0m00.02s | 75240 ko | Rewriter/Util/Tactics/DestructHead.vo | 0m00.03s | 73848 ko || -0m00.00s || 1392 ko | -33.33% | +1.88% 0m00.02s | 69008 ko | Rewriter/Util/Tactics/DestructHyps.vo | 0m00.03s | 67584 ko || -0m00.00s || 1424 ko | -33.33% | +2.10% 0m00.02s | 65648 ko | Rewriter/Util/Tactics/Head.vo | 0m00.02s | 67452 ko || +0m00.00s || -1804 ko | +0.00% | -2.67% 0m00.02s | 62668 ko | Rewriter/Util/Tactics/Not.vo | 0m00.03s | 61456 ko || -0m00.00s || 1212 ko | -33.33% | +1.97% 0m00.02s | 62664 ko | Rewriter/Util/Tactics/PrintContext.vo | 0m00.03s | 62576 ko || -0m00.00s || 88 ko | -33.33% | +0.14% 0m00.02s | 87992 ko | Rewriter/Util/Tactics/RewriteHyp.vo | 0m00.03s | 89076 ko || -0m00.00s || -1084 ko | -33.33% | -1.21% 0m00.02s | 62808 ko | Rewriter/Util/Tactics/SetEvars.vo | 0m00.02s | 62480 ko || +0m00.00s || 328 ko | +0.00% | +0.52% 0m00.02s | 61488 ko | Rewriter/Util/Tactics/SubstEvars.vo | 0m00.02s | 61028 ko || +0m00.00s || 460 ko | +0.00% | +0.75% 0m00.02s | 68020 ko | Rewriter/Util/Tactics/UniquePose.vo | 0m00.03s | 66840 ko || -0m00.00s || 1180 ko | -33.33% | +1.76% 0m00.02s | 62044 ko | Rewriter/Util/Tactics/WarnIfGoalsRemain.vo | 0m00.01s | 61212 ko || +0m00.01s || 832 ko | +100.00% | +1.35% 0m00.02s | 67872 ko | Rewriter/Util/Tactics2/DestConstant.vo | 0m00.04s | 68172 ko || -0m00.02s || -300 ko | -50.00% | -0.44% 0m00.02s | 68584 ko | Rewriter/Util/Tactics2/DestLambda.vo | 0m00.03s | 68464 ko || -0m00.00s || 120 ko | -33.33% | +0.17% 0m00.02s | 67772 ko | Rewriter/Util/Tactics2/DestSort.vo | 0m00.03s | 68604 ko || -0m00.00s || -832 ko | -33.33% | -1.21% 0m00.02s | 63908 ko | Rewriter/Util/TypeList.vo | 0m00.03s | 65608 ko || -0m00.00s || -1700 ko | -33.33% | -2.59% 0m00.02s | 69812 ko | Util/GlobalSettings.vo | 0m00.02s | 69816 ko || +0m00.00s || -4 ko | +0.00% | -0.00% 0m00.02s | 79788 ko | Util/PER.vo | 0m00.04s | 79856 ko || -0m00.02s || -68 ko | -50.00% | -0.08% 0m00.02s | 77240 ko | Util/Tactics/AppendUnderscores.vo | 0m00.03s | 73668 ko || -0m00.00s || 3572 ko | -33.33% | +4.84% 0m00.02s | 75016 ko | Util/Tactics/FindHyp.vo | 0m00.03s | 73816 ko || -0m00.00s || 1200 ko | -33.33% | +1.62% 0m00.02s | 68860 ko | Util/Tactics/GetGoal.vo | 0m00.03s | 68908 ko || -0m00.00s || -48 ko | -33.33% | -0.06% 0m00.02s | 70216 ko | Util/Tactics/Not.vo | 0m00.01s | 69320 ko || +0m00.01s || 896 ko | +100.00% | +1.29% 0m00.02s | 71824 ko | Util/Tactics/PrintGoal.vo | 0m00.03s | 69796 ko || -0m00.00s || 2028 ko | -33.33% | +2.90% 0m00.02s | 71248 ko | Util/Tactics/SimplifyRepeatedIfs.vo | 0m00.02s | 70644 ko || +0m00.00s || 604 ko | +0.00% | +0.85% 0m00.02s | 74708 ko | Util/Tactics/SpecializeAllWays.vo | 0m00.05s | 74760 ko || -0m00.03s || -52 ko | -60.00% | -0.06% 0m00.02s | 70112 ko | Util/Tactics/Test.vo | 0m00.03s | 69752 ko || -0m00.00s || 360 ko | -33.33% | +0.51% 0m00.02s | 71300 ko | Util/Tactics/WarnIfGoalsRemain.vo | 0m00.02s | 70244 ko || +0m00.00s || 1056 ko | +0.00% | +1.50% 0m00.02s | 62800 ko | coqutil/Datatypes/dlist.vo | 0m00.03s | 61948 ko || -0m00.00s || 852 ko | -33.33% | +1.37% 0m00.02s | 61864 ko | coqutil/Macros/subst.vo | 0m00.02s | 60252 ko || +0m00.00s || 1612 ko | +0.00% | +2.67% 0m00.02s | 61616 ko | coqutil/Macros/unique.vo | 0m00.02s | 61948 ko || +0m00.00s || -332 ko | +0.00% | -0.53% 0m00.02s | 65288 ko | coqutil/Tactics/autoforward.vo | 0m00.03s | 67224 ko || -0m00.00s || -1936 ko | -33.33% | -2.87% 0m00.02s | 66864 ko | coqutil/Tactics/forward.vo | 0m00.03s | 67244 ko || -0m00.00s || -380 ko | -33.33% | -0.56% 0m00.02s | 62640 ko | coqutil/Tactics/letexists.vo | 0m00.02s | 62328 ko || +0m00.00s || 312 ko | +0.00% | +0.50% 0m00.02s | 64272 ko | coqutil/Tactics/ltac_list_ops.vo | 0m00.03s | 64840 ko || -0m00.00s || -568 ko | -33.33% | -0.87% 0m00.02s | 62408 ko | coqutil/Tactics/rdelta.vo | 0m00.01s | 60892 ko || +0m00.01s || 1516 ko | +100.00% | +2.48% 0m00.02s | 65992 ko | coqutil/Tactics/safe_auto.vo | 0m00.01s | 67664 ko || +0m00.01s || -1672 ko | +100.00% | -2.47% 0m00.02s | 63332 ko | coqutil/Tactics/simpl_rewrite.vo | 0m00.03s | 63940 ko || -0m00.00s || -608 ko | -33.33% | -0.95% 0m00.02s | 61340 ko | coqutil/dlet.vo | 0m00.02s | 61872 ko || +0m00.00s || -532 ko | +0.00% | -0.85% 0m00.02s | 59956 ko | coqutil/sanity.vo | 0m00.02s | 59992 ko || +0m00.00s || -36 ko | +0.00% | -0.06% 0m00.02s | 63888 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Logging.vo | 0m00.03s | 64784 ko || -0m00.00s || -896 ko | -33.33% | -1.38% 0m00.02s | 67508 ko | rupicola/bedrock2/bedrock2/src/bedrock2/anyval.vo | 0m00.03s | 67248 ko || -0m00.00s || 260 ko | -33.33% | +0.38% 0m00.02s | 62500 ko | rupicola/bedrock2/bedrock2/src/bedrock2/tweak_tacs.vo | 0m00.04s | 63988 ko || -0m00.02s || -1488 ko | -50.00% | -2.32% 0m00.02s | 79280 ko | rupicola/bedrock2/compiler/src/compiler/GenericForeverSafe.vo | 0m00.02s | 80464 ko || +0m00.00s || -1184 ko | +0.00% | -1.47% 0m00.02s | 63656 ko | rupicola/bedrock2/compiler/src/compiler/eqexact.vo | 0m00.01s | 62580 ko || +0m00.01s || 1076 ko | +100.00% | +1.71% 0m00.02s | 62488 ko | rupicola/bedrock2/compiler/src/compiler/on_hyp_containing.vo | 0m00.02s | 64276 ko || +0m00.00s || -1788 ko | +0.00% | -2.78% 0m00.02s | 63772 ko | rupicola/bedrock2/compiler/src/compiler/util/Learning.vo | 0m00.03s | 64608 ko || -0m00.00s || -836 ko | -33.33% | -1.29% 0m00.02s | 63116 ko | rupicola/bedrock2/compiler/src/compiler/util/LogGoal.vo | 0m00.02s | 62760 ko || +0m00.00s || 356 ko | +0.00% | +0.56% 0m00.02s | 72216 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/PowerFunc.vo | 0m00.02s | 70852 ko || +0m00.00s || 1364 ko | +0.00% | +1.92% 0m00.01s | 63048 ko | Rewriter/Util/Isomorphism.vo | 0m00.03s | 63716 ko || -0m00.01s || -668 ko | -66.66% | -1.04% 0m00.01s | 66380 ko | Rewriter/Util/Tactics/AssertSucceedsPreserveError.vo | 0m00.03s | 66524 ko || -0m00.01s || -144 ko | -66.66% | -0.21% 0m00.01s | 67000 ko | Rewriter/Util/Tactics/FindHyp.vo | 0m00.02s | 67200 ko || -0m00.01s || -200 ko | -50.00% | -0.29% 0m00.01s | 67724 ko | Rewriter/Util/Tactics/SpecializeBy.vo | 0m00.03s | 66876 ko || -0m00.01s || 848 ko | -66.66% | +1.26% 0m00.01s | 67604 ko | Rewriter/Util/Tactics2/String.vo | 0m00.06s | 67692 ko || -0m00.05s || -88 ko | -83.33% | -0.13% 0m00.01s | 89472 ko | Util/Logic/ProdForall.vo | 0m00.03s | 88228 ko || -0m00.01s || 1244 ko | -66.66% | +1.40% 0m00.01s | 74528 ko | Util/Tactics/CountBinders.vo | 0m00.01s | 75560 ko || +0m00.00s || -1032 ko | +0.00% | -1.36% 0m00.01s | 69916 ko | Util/Tactics/SubstEvars.vo | 0m00.04s | 69408 ko || -0m00.03s || 508 ko | -75.00% | +0.73% 0m00.01s | 63812 ko | coqutil/Datatypes/PrimitivePair.vo | 0m00.02s | 63948 ko || -0m00.01s || -136 ko | -50.00% | -0.21% 0m00.01s | 64652 ko | coqutil/Tactics/syntactic_unify.vo | 0m00.02s | 63712 ko || -0m00.01s || 940 ko | -50.00% | +1.47% 0m00.01s | 68212 ko | rupicola/bedrock2/deps/riscv-coq/src/riscv/Utility/record_set_why_anonymous_getters.vo | 0m00.02s | 66752 ko || -0m00.01s || 1460 ko | -50.00% | +2.18% 0m00.00s | 63280 ko | Rewriter/Util/Tactics/PrintGoal.vo | 0m00.02s | 61328 ko || -0m00.02s || 1952 ko | -100.00% | +3.18% 0m00.00s | 65212 ko | rupicola/bedrock2/bedrock2/src/bedrock2/Lift1Prop.vo | 0m00.01s | 66988 ko || -0m00.01s || -1776 ko | -100.00% | -2.65% ```