Use Listable to prove equality of registers and opcodes #2020

JasonGross · 2025-03-03T22:27:17Z

This is much faster, especially as we add more registers and opcodes

JasonGross · 2025-03-03T22:33:48Z

I want to run timing numbers on this before merging

JasonGross · 2025-03-04T06:30:50Z

Attempting to run timing at https://github.com/JasonGross/fiat-crypto/actions/runs/13647667831

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 <details><summary>Timing Diff</summary> <p> ``` 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 …

JasonGross · 2025-03-05T04:25:45Z

Previous build succeeded except for ocaml/setup-ocaml#938, going to merge

… 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 <details><summary>Timing Diff</summary> <p> ``` 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/…

JasonGross marked this pull request as draft March 3, 2025 22:33

JasonGross force-pushed the rework-widest-register branch 3 times, most recently from 2e2434a to 540e6a2 Compare March 4, 2025 06:28

JasonGross force-pushed the rework-widest-register branch from 540e6a2 to dcc91eb Compare March 4, 2025 16:17

JasonGross force-pushed the rework-widest-register branch from dcc91eb to 314014b Compare March 5, 2025 04:25

JasonGross marked this pull request as ready for review March 5, 2025 04:25

JasonGross merged commit e550a66 into mit-plv:master Mar 5, 2025
15 checks passed

JasonGross deleted the rework-widest-register branch March 5, 2025 04:26

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use Listable to prove equality of registers and opcodes #2020

Use Listable to prove equality of registers and opcodes #2020

JasonGross commented Mar 3, 2025

JasonGross commented Mar 3, 2025

JasonGross commented Mar 4, 2025

JasonGross commented Mar 5, 2025

Use Listable to prove equality of registers and opcodes #2020

Use Listable to prove equality of registers and opcodes #2020

Conversation

JasonGross commented Mar 3, 2025

JasonGross commented Mar 3, 2025

JasonGross commented Mar 4, 2025

JasonGross commented Mar 5, 2025