From 314014b065fc0bb6088d4e95df149d2fab146a61 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 1 Mar 2025 01:38:51 -0800 Subject: [PATCH] Use Listable to prove equality of registers and opcodes 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% ```

--- src/Assembly/Equality.v | 20 +- src/Assembly/Equivalence.v | 4 +- src/Assembly/EquivalenceProofs.v | 4 +- src/Assembly/Parse.v | 20 -- src/Assembly/Symbolic.v | 20 +- src/Assembly/Syntax.v | 359 ++++++++++------------ src/Assembly/SyntaxTests.v | 155 ++++++++++ src/Assembly/WithBedrock/Proofs.v | 36 ++- src/Assembly/WithBedrock/Semantics.v | 8 +- src/Assembly/WithBedrock/SymbolicProofs.v | 4 +- src/Util/Listable.v | 1 + 11 files changed, 365 insertions(+), 266 deletions(-) create mode 100644 src/Assembly/SyntaxTests.v diff --git a/src/Assembly/Equality.v b/src/Assembly/Equality.v index 4575629772..336da900e8 100644 --- a/src/Assembly/Equality.v +++ b/src/Assembly/Equality.v @@ -35,8 +35,8 @@ Bind Scope REG_scope with REG. Infix "=?" := REG_beq : REG_scope. Global Instance REG_beq_spec : reflect_rel (@eq REG) REG_beq | 10 - := reflect_of_beq internal_REG_dec_bl internal_REG_dec_lb. -Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@internal_REG_dec_bl _ _) (@internal_REG_dec_lb _ _). + := reflect_of_beq REG_dec_bl REG_dec_lb. +Definition REG_beq_eq x y : (x =? y)%REG = true <-> x = y := conj (@REG_dec_bl _ _) (@REG_dec_lb _ _). Lemma REG_beq_neq x y : (x =? y)%REG = false <-> x <> y. Proof. rewrite <- REG_beq_eq; destruct (x =? y)%REG; intuition congruence. Qed. Global Instance REG_beq_compat : Proper (eq ==> eq ==> eq) REG_beq | 10. @@ -95,8 +95,8 @@ Bind Scope AccessSize_scope with AccessSize. Infix "=?" := AccessSize_beq : AccessSize_scope. Global Instance AccessSize_beq_spec : reflect_rel (@eq AccessSize) AccessSize_beq | 10 - := reflect_of_beq internal_AccessSize_dec_bl internal_AccessSize_dec_lb. -Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@internal_AccessSize_dec_bl _ _) (@internal_AccessSize_dec_lb _ _). + := reflect_of_beq AccessSize_dec_bl AccessSize_dec_lb. +Definition AccessSize_beq_eq x y : (x =? y)%AccessSize = true <-> x = y := conj (@AccessSize_dec_bl _ _) (@AccessSize_dec_lb _ _). Lemma AccessSize_beq_neq x y : (x =? y)%AccessSize = false <-> x <> y. Proof. rewrite <- AccessSize_beq_eq; destruct (x =? y)%AccessSize; intuition congruence. Qed. Global Instance AccessSize_beq_compat : Proper (eq ==> eq ==> eq) AccessSize_beq | 10. @@ -141,8 +141,8 @@ Bind Scope FLAG_scope with FLAG. Infix "=?" := FLAG_beq : FLAG_scope. Global Instance FLAG_beq_spec : reflect_rel (@eq FLAG) FLAG_beq | 10 - := reflect_of_beq internal_FLAG_dec_bl internal_FLAG_dec_lb. -Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@internal_FLAG_dec_bl _ _) (@internal_FLAG_dec_lb _ _). + := reflect_of_beq FLAG_dec_bl FLAG_dec_lb. +Definition FLAG_beq_eq x y : (x =? y)%FLAG = true <-> x = y := conj (@FLAG_dec_bl _ _) (@FLAG_dec_lb _ _). Lemma FLAG_beq_neq x y : (x =? y)%FLAG = false <-> x <> y. Proof. rewrite <- FLAG_beq_eq; destruct (x =? y)%FLAG; intuition congruence. Qed. Global Instance FLAG_beq_compat : Proper (eq ==> eq ==> eq) FLAG_beq | 10. @@ -155,8 +155,8 @@ Bind Scope OpCode_scope with OpCode. Infix "=?" := OpCode_beq : OpCode_scope. Global Instance OpCode_beq_spec : reflect_rel (@eq OpCode) OpCode_beq | 10 - := reflect_of_beq internal_OpCode_dec_bl internal_OpCode_dec_lb. -Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@internal_OpCode_dec_bl _ _) (@internal_OpCode_dec_lb _ _). + := reflect_of_beq OpCode_dec_bl OpCode_dec_lb. +Definition OpCode_beq_eq x y : (x =? y)%OpCode = true <-> x = y := conj (@OpCode_dec_bl _ _) (@OpCode_dec_lb _ _). Lemma OpCode_beq_neq x y : (x =? y)%OpCode = false <-> x <> y. Proof. rewrite <- OpCode_beq_eq; destruct (x =? y)%OpCode; intuition congruence. Qed. Global Instance OpCode_beq_compat : Proper (eq ==> eq ==> eq) OpCode_beq | 10. @@ -169,8 +169,8 @@ Bind Scope OpPrefix_scope with OpPrefix. Infix "=?" := OpPrefix_beq : OpPrefix_scope. Global Instance OpPrefix_beq_spec : reflect_rel (@eq OpPrefix) OpPrefix_beq | 10 - := reflect_of_beq internal_OpPrefix_dec_bl internal_OpPrefix_dec_lb. -Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@internal_OpPrefix_dec_bl _ _) (@internal_OpPrefix_dec_lb _ _). + := reflect_of_beq OpPrefix_dec_bl OpPrefix_dec_lb. +Definition OpPrefix_beq_eq x y : (x =? y)%OpPrefix = true <-> x = y := conj (@OpPrefix_dec_bl _ _) (@OpPrefix_dec_lb _ _). Lemma OpPrefix_beq_neq x y : (x =? y)%OpPrefix = false <-> x <> y. Proof. rewrite <- OpPrefix_beq_eq; destruct (x =? y)%OpPrefix; intuition congruence. Qed. Global Instance OpPrefix_beq_compat : Proper (eq ==> eq ==> eq) OpPrefix_beq | 10. diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index aff15463cd..bf5dc1f3fc 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -1275,10 +1275,10 @@ Definition init_symbolic_state_descr : description := Build_description "init_sy Definition init_symbolic_state (d : dag) : symbolic_state := let _ := init_symbolic_state_descr in - let '(initial_reg_idxs, d) := dag_gensym_n 16 d in + let '(initial_reg_idxs, d) := dag_gensym_n (List.length widest_registers) d in {| dag_state := d; - symbolic_reg_state := Tuple.from_list_default None 16 (List.map Some initial_reg_idxs); + symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs); symbolic_mem_state := []; symbolic_flag_state := Tuple.repeat None 6; |}. diff --git a/src/Assembly/EquivalenceProofs.v b/src/Assembly/EquivalenceProofs.v index a4340e146f..f086330c74 100644 --- a/src/Assembly/EquivalenceProofs.v +++ b/src/Assembly/EquivalenceProofs.v @@ -1847,7 +1847,7 @@ Qed. (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *) Lemma get_reg_set_reg_full s rn rn' v : get_reg (set_reg s rn v) rn' - = if ((rn n) _ s)) && (rn =? rn'))%nat%bool + = if ((rn N.of_nat n) _ s)) && (rn =? rn'))%N%bool then Some v else get_reg s rn'. Proof. @@ -1863,7 +1863,7 @@ Qed. (* TODO: this is Symbolic.get_reg; move to SymbolicProofs? *) Local Lemma get_reg_set_reg_same s rn v - (H : (rn < (fun n (_ : Tuple.tuple _ n) => n) _ s)%nat) + (H : (rn < (fun n (_ : Tuple.tuple _ n) => N.of_nat n) _ s)%N) : get_reg (set_reg s rn v) rn = Some v. Proof. rewrite get_reg_set_reg_full; break_innermost_match; reflect_hyps; cbv beta in *; try reflexivity; lia. diff --git a/src/Assembly/Parse.v b/src/Assembly/Parse.v index 7b0f313d2a..486c886602 100644 --- a/src/Assembly/Parse.v +++ b/src/Assembly/Parse.v @@ -22,34 +22,18 @@ Local Open Scope list_scope. Local Open Scope string_scope. Local Open Scope parse_scope. -Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable. -Proof. prove_ListableDerive. Qed. -Global Existing Instances REG_Listable REG_FinitelyListable. - Global Instance show_REG : Show REG. Proof. prove_Show_enum (). Defined. Global Instance show_lvl_REG : ShowLevel REG := show_REG. -Derive FLAG_Listable SuchThat (@FinitelyListable FLAG FLAG_Listable) As FLAG_FinitelyListable. -Proof. prove_ListableDerive. Qed. -Global Existing Instances FLAG_Listable FLAG_FinitelyListable. - Global Instance show_FLAG : Show FLAG. Proof. prove_Show_enum (). Defined. Global Instance show_lvl_FLAG : ShowLevel FLAG := show_FLAG. -Derive OpCode_Listable SuchThat (@FinitelyListable OpCode OpCode_Listable) As OpCode_FinitelyListable. -Proof. prove_ListableDerive. Qed. -Global Existing Instances OpCode_Listable OpCode_FinitelyListable. - Global Instance show_OpCode : Show OpCode. Proof. prove_Show_enum (). Defined. Global Instance show_lvl_OpCode : ShowLevel OpCode := show_OpCode. -Derive OpPrefix_Listable SuchThat (@FinitelyListable OpPrefix OpPrefix_Listable) As OpPrefix_FinitelyListable. -Proof. prove_ListableDerive. Qed. -Global Existing Instances OpPrefix_Listable OpPrefix_FinitelyListable. - Global Instance show_OpPrefix : Show OpPrefix. Proof. prove_Show_enum (). Defined. Global Instance show_lvl_OpPrefix : ShowLevel OpPrefix := show_OpPrefix. @@ -72,10 +56,6 @@ Definition parse_FLAG_list : list (string * FLAG) Definition parse_FLAG : ParserAction FLAG := parse_strs parse_FLAG_list. -Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable. -Proof. prove_ListableDerive. Qed. -Global Existing Instances AccessSize_Listable AccessSize_FinitelyListable. - Global Instance show_AccessSize : Show AccessSize. Proof. prove_Show_enum (). Defined. Global Instance show_lvl_AccessSize : ShowLevel AccessSize := show_AccessSize. diff --git a/src/Assembly/Symbolic.v b/src/Assembly/Symbolic.v index 593a30c720..f2a2c93cc3 100644 --- a/src/Assembly/Symbolic.v +++ b/src/Assembly/Symbolic.v @@ -3829,7 +3829,7 @@ Definition simplify {opts : symbolic_options_computed_opt} (dag : dag) (e : node Lemma eval_simplify {opts : symbolic_options_computed_opt} G d n v : gensym_dag_ok G d -> eval_node G d n v -> eval G d (simplify d n) v. Proof using Type. eauto using Rewrite.eval_expr, eval_node_reveal_node_at_least. Qed. -Definition reg_state := Tuple.tuple (option idx) 16. +Definition reg_state := Tuple.tuple (option idx) (compute! (List.length widest_registers)). Definition flag_state := Tuple.tuple (option idx) 6. Definition mem_state := list (idx * idx). @@ -3863,16 +3863,16 @@ Definition reverse_lookup_flag (st : flag_state) (i : idx) : option FLAG (List.find (fun v => option_beq N.eqb (Some i) (fst v)) (Tuple.to_list _ (Tuple.map2 (@pair _ _) st (CF, PF, AF, ZF, SF, OF)))). -Definition get_reg (st : reg_state) (ri : nat) : option idx - := Tuple.nth_default None ri st. -Definition set_reg (st : reg_state) ri (i : idx) : reg_state +Definition get_reg (st : reg_state) (ri : N) : option idx + := Tuple.nth_default None (N.to_nat ri) st. +Definition set_reg (st : reg_state) (ri : N) (i : idx) : reg_state := Tuple.from_list_default None _ (ListUtil.set_nth - ri + (N.to_nat ri) (Some i) (Tuple.to_list _ st)). Definition reverse_lookup_widest_reg (st : reg_state) (i : idx) : option REG := option_map - (fun v => widest_register_of_index (fst v)) + (fun v => widest_register_of_index (N.of_nat (fst v))) (List.find (fun v => option_beq N.eqb (Some i) (snd v)) (List.enumerate (Tuple.to_list _ st))). @@ -3906,7 +3906,7 @@ Definition update_mem_with (st : symbolic_state) (f : mem_state -> mem_state) : := {| dag_state := st.(dag_state); symbolic_reg_state := st.(symbolic_reg_state) ; symbolic_flag_state := st.(symbolic_flag_state) ; symbolic_mem_state := f st.(symbolic_mem_state) |}. Global Instance show_reg_state : Show reg_state := fun st => - show (List.map (fun '(n, v) => (widest_register_of_index n, v)) (ListUtil.List.enumerate (Option.List.map id (Tuple.to_list _ st)))). + show (List.combine widest_registers (Option.List.map id (Tuple.to_list _ st))). Global Instance show_flag_state : Show flag_state := fun '(cfv, pfv, afv, zfv, sfv, ofv) => ( @@ -3953,7 +3953,7 @@ Module error. Local Unset Decidable Equality Schemes. Variant error := | get_flag (f : FLAG) (s : flag_state) - | get_reg (r : nat + REG) (s : reg_state) + | get_reg (r : N + REG) (s : reg_state) | load (a : idx) (s : symbolic_state) | remove (a : idx) (s : symbolic_state) | remove_has_duplicates (a : idx) (vs : list idx) (s : symbolic_state) @@ -3977,7 +3977,7 @@ Module error. => ["In flag state " ++ show_flag_state s; "Flag " ++ show f ++ " was read without being set."] | get_reg (inl i) s - => ["Invalid reg index " ++ show_nat i] + => ["Invalid reg index " ++ show i] | get_reg (inr r) s => ["In reg state " ++ show_reg_state s; "Register " ++ show (r : REG) ++ " read without being set."] @@ -4042,7 +4042,7 @@ Definition mapM_ {A B} (f: A -> M B) l : M unit := _ <- mapM f l; ret tt. Definition error_get_reg_of_reg_index ri : symbolic_state -> error := error.get_reg (let r := widest_register_of_index ri in - if (reg_index r =? ri)%nat + if (reg_index r =? ri)%N then inr r else inl ri). diff --git a/src/Assembly/Syntax.v b/src/Assembly/Syntax.v index 50dd2e5046..29638b22a2 100644 --- a/src/Assembly/Syntax.v +++ b/src/Assembly/Syntax.v @@ -3,7 +3,11 @@ From Coq Require Import NArith. From Coq Require Import String. From Coq Require Import List. From Coq Require Import Derive. +Require Import Crypto.Util.Prod. Require Import Crypto.Util.Option. +Require Import Crypto.Util.Bool.Reflect. +Require Import Crypto.Util.Listable. +Require Import Crypto.Util.ListUtil. Require Crypto.Util.Tuple. Require Crypto.Util.OptionList. Import ListNotations. @@ -11,8 +15,6 @@ Import ListNotations. Local Open Scope list_scope. Local Set Implicit Arguments. -Local Set Boolean Equality Schemes. -Local Set Decidable Equality Schemes. Local Set Primitive Projections. Inductive REG := @@ -22,10 +24,27 @@ Inductive REG := | ah | al | ch | cl | dh | dl | bh | bl | spl | bpl | sil | dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b . +Derive REG_Listable SuchThat (@FinitelyListable REG REG_Listable) As REG_FinitelyListable. +Proof. prove_ListableDerive. Qed. +Global Existing Instances REG_Listable REG_FinitelyListable. +Definition REG_beq : REG -> REG -> bool := eqb_of_listable. +Definition REG_dec_bl : forall x y, REG_beq x y = true -> x = y := eqb_of_listable_bl. +Definition REG_dec_lb : forall x y, x = y -> REG_beq x y = true := eqb_of_listable_lb. +Definition REG_eq_dec : forall x y : REG, {x = y} + {x <> y} := eq_dec_of_listable. + Definition CONST := Z. Coercion CONST_of_Z (x : Z) : CONST := x. Inductive AccessSize := byte | word | dword | qword. + +Derive AccessSize_Listable SuchThat (@FinitelyListable AccessSize AccessSize_Listable) As AccessSize_FinitelyListable. +Proof. prove_ListableDerive. Qed. +Global Existing Instances AccessSize_Listable AccessSize_FinitelyListable. +Definition AccessSize_beq : AccessSize -> AccessSize -> bool := eqb_of_listable. +Definition AccessSize_dec_bl : forall x y, AccessSize_beq x y = true -> x = y := eqb_of_listable_bl. +Definition AccessSize_dec_lb : forall x y, x = y -> AccessSize_beq x y = true := eqb_of_listable_lb. +Definition AccessSize_eq_dec : forall x y : AccessSize, {x = y} + {x <> y} := eq_dec_of_listable. + Coercion bits_of_AccessSize (x : AccessSize) : N := match x with | byte => 8 @@ -41,12 +60,28 @@ Definition mem_of_reg (r : REG) : MEM := Inductive FLAG := CF | PF | AF | ZF | SF | OF. +Derive FLAG_Listable SuchThat (@FinitelyListable FLAG FLAG_Listable) As FLAG_FinitelyListable. +Proof. prove_ListableDerive. Qed. +Global Existing Instances FLAG_Listable FLAG_FinitelyListable. +Definition FLAG_beq : FLAG -> FLAG -> bool := eqb_of_listable. +Definition FLAG_dec_bl : forall x y, FLAG_beq x y = true -> x = y := eqb_of_listable_bl. +Definition FLAG_dec_lb : forall x y, x = y -> FLAG_beq x y = true := eqb_of_listable_lb. +Definition FLAG_eq_dec : forall x y : FLAG, {x = y} + {x <> y} := eq_dec_of_listable. + Inductive OpPrefix := | rep | repz | repnz . +Derive OpPrefix_Listable SuchThat (@FinitelyListable OpPrefix OpPrefix_Listable) As OpPrefix_FinitelyListable. +Proof. prove_ListableDerive. Qed. +Global Existing Instances OpPrefix_Listable OpPrefix_FinitelyListable. +Definition OpPrefix_beq : OpPrefix -> OpPrefix -> bool := eqb_of_listable. +Definition OpPrefix_dec_bl : forall x y, OpPrefix_beq x y = true -> x = y := eqb_of_listable_bl. +Definition OpPrefix_dec_lb : forall x y, x = y -> OpPrefix_beq x y = true := eqb_of_listable_lb. +Definition OpPrefix_eq_dec : forall x y : OpPrefix, {x = y} + {x <> y} := eq_dec_of_listable. + Inductive OpCode := | adc | adcx @@ -62,10 +97,10 @@ Inductive OpCode := | cmovo | cmp | db +| dw | dd -| dec | dq -| dw +| dec | imul | inc | je @@ -95,6 +130,64 @@ Inductive OpCode := | xor . +Derive OpCode_Listable SuchThat (@FinitelyListable OpCode OpCode_Listable) As OpCode_FinitelyListable. +Proof. prove_ListableDerive. Qed. +Global Existing Instances OpCode_Listable OpCode_FinitelyListable. +Definition OpCode_beq : OpCode -> OpCode -> bool := eqb_of_listable. +Definition OpCode_dec_bl : forall x y, OpCode_beq x y = true -> x = y := eqb_of_listable_bl. +Definition OpCode_dec_lb : forall x y, x = y -> OpCode_beq x y = true := eqb_of_listable_lb. +Definition OpCode_eq_dec : forall x y : OpCode, {x = y} + {x <> y} := eq_dec_of_listable. + +Definition accesssize_of_declaration (opc : OpCode) : option AccessSize := + match opc with + | db => Some byte + | dd => Some dword + | dq => Some qword + | dw => Some word + | adc + | adcx + | add + | adox + | and + | bzhi + | call + | clc + | cmovb + | cmovc + | cmovnz + | cmovo + | cmp + | dec + | imul + | inc + | je + | jmp + | lea + | mov + | movzx + | mul + | mulx + | or + | pop + | push + | rcr + | ret + | sar + | sbb + | setc + | seto + | shl + | shlx + | shr + | shrx + | shrd + | sub + | test + | xchg + | xor + => None + end. + Record JUMP_LABEL := { jump_near : bool ; label_name : string }. Inductive ARG := reg (r : REG) | mem (m : MEM) | const (c : CONST) | label (l : JUMP_LABEL). @@ -172,154 +265,73 @@ Definition operand_size (x : ARG) (operation_size : N) : N := | None => operation_size end. - -Definition reg_index (r : REG) : nat - := match r with - | rax - | eax - | ax - |(ah | al) - => 0 - | rcx - | ecx - | cx - |(ch | cl) - => 1 - | rdx - | edx - | dx - |(dh | dl) - => 2 - | rbx - | ebx - | bx - |(bh | bl) - => 3 - | rsp - | esp - | sp - |( spl) - => 4 - | rbp - | ebp - | bp - |( bpl) - => 5 - | rsi - | esi - | si - |( sil) - => 6 - | rdi - | edi - | di - |( dil) - => 7 - | r8 - | r8d - | r8w - | r8b - => 8 - | r9 - | r9d - | r9w - | r9b - => 9 - | r10 - | r10d - | r10w - | r10b - => 10 - | r11 - | r11d - | r11w - | r11b - => 11 - | r12 - | r12d - | r12w - | r12b - => 12 - | r13 - | r13d - | r13w - | r13b - => 13 - | r14 - | r14d - | r14w - | r14b - => 14 - | r15 - | r15d - | r15w - | r15b - => 15 - end. Definition reg_offset (r : REG) : N := - match r with - |( rax | rcx | rdx | rbx | rsp | rbp | rsi | rdi | r8 | r9 | r10 | r11 | r12 | r13 | r14 | r15 ) - |( eax | ecx | edx | ebx | esp | ebp | esi | edi | r8d | r9d | r10d | r11d | r12d | r13d | r14d | r15d) - |( ax | cx | dx | bx | sp | bp | si | di | r8w | r9w | r10w | r11w | r12w | r13w | r14w | r15w) - |( al | cl | dl | bl | spl | bpl | sil | dil | r8b | r9b | r10b | r11b | r12b | r13b | r14b | r15b) - => 0 - |(ah | ch | dh | bh ) - => 8 - end. -Definition index_and_shift_and_bitcount_of_reg (r : REG) := - (reg_index r, reg_offset r, reg_size r). + match r with + |(ah | ch | dh | bh ) + => 8 + | _ => 0 + end. -Definition regs_of_index (index : nat) : list (list REG) := - match index with - | 0 => [ [ al ; ah] ; [ ax] ; [ eax] ; [rax] ] - | 1 => [ [ cl ; ch] ; [ cx] ; [ ecx] ; [rcx] ] - | 2 => [ [ dl ; dh] ; [ dx] ; [ edx] ; [rdx] ] - | 3 => [ [ bl ; bh] ; [ bx] ; [ ebx] ; [rbx] ] - | 4 => [ [ spl ] ; [ sp] ; [ esp] ; [rsp] ] - | 5 => [ [ bpl ] ; [ bp] ; [ ebp] ; [rbp] ] - | 6 => [ [ sil ] ; [ si] ; [ esi] ; [rsi] ] - | 7 => [ [ dil ] ; [ di] ; [ edi] ; [rdi] ] - | 8 => [ [ r8b ] ; [ r8w] ; [ r8d] ; [r8 ] ] - | 9 => [ [ r9b ] ; [ r9w] ; [ r9d] ; [r9 ] ] - | 10 => [ [r10b ] ; [r10w] ; [r10d] ; [r10] ] - | 11 => [ [r11b ] ; [r11w] ; [r11d] ; [r11] ] - | 12 => [ [r12b ] ; [r12w] ; [r12d] ; [r12] ] - | 13 => [ [r13b ] ; [r13w] ; [r13d] ; [r13] ] - | 14 => [ [r14b ] ; [r14w] ; [r14d] ; [r14] ] - | 15 => [ [r15b ] ; [r15w] ; [r15d] ; [r15] ] - | _ => [] +Definition widest_register_of (r : REG) : REG := + match r with + | ((al | ah) | ax | eax | rax) => rax + | ((cl | ch) | cx | ecx | rcx) => rcx + | ((dl | dh) | dx | edx | rdx) => rdx + | ((bl | bh) | bx | ebx | rbx) => rbx + | (spl | sp | esp | rsp) => rsp + | (bpl | bp | ebp | rbp) => rbp + | (sil | si | esi | rsi) => rsi + | (dil | di | edi | rdi) => rdi + | (r8b | r8w | r8d | r8) => r8 + | (r9b | r9w | r9d | r9) => r9 + | (r10b | r10w | r10d | r10) => r10 + | (r11b | r11w | r11d | r11) => r11 + | (r12b | r12w | r12d | r12) => r12 + | (r13b | r13w | r13d | r13) => r13 + | (r14b | r14w | r14d | r14) => r14 + | (r15b | r15w | r15d | r15) => r15 end. +Definition widest_registers := Eval lazy in List.filter (fun x => REG_beq x (widest_register_of x)) (list_all REG). + +Definition wide_reg_index_pairs := Eval lazy in List.map (fun '(n, r) => (N.of_nat n, r)) (List.enumerate widest_registers). + +Definition eta_reg {A} : (REG -> A) -> (REG -> A). +Proof. + intros f r; pose (f r) as fr; destruct r. + all: let v := eval cbv in fr in exact v. +Defined. + +Definition reg_index (r : REG) : N := Eval lazy in + eta_reg (fun r => + Option.value + (option_map (@fst _ _) (find (fun '(n, r') => REG_beq (widest_register_of r) r') wide_reg_index_pairs)) + 0%N) + r. + +Definition widest_register_of_index_opt (n : N) : option REG + := List.nth_error (List.map (@snd _ _) wide_reg_index_pairs) (N.to_nat n). + (** convenience printing function *) -Definition widest_register_of_index (n : nat) : REG - := match n with - | 0 => rax - | 1 => rcx - | 2 => rdx - | 3 => rbx - | 4 => rsp - | 5 => rbp - | 6 => rsi - | 7 => rdi - | 8 => r8 - | 9 => r9 - | 10 => r10 - | 11 => r11 - | 12 => r12 - | 13 => r13 - | 14 => r14 - | 15 => r15 - | _ => rax - end%nat. +Definition widest_register_of_index (n : N) : REG + := Option.value (widest_register_of_index_opt n) rax. + +Definition widest_reg_size_of (r : REG) : N := + reg_size (widest_register_of_index (reg_index r)). + +Definition index_and_shift_and_bitcount_of_reg (r : REG) := + (reg_index r, reg_offset r, reg_size r). + +Definition overlapping_registers (r : REG) : list REG := Eval lazy in eta_reg + (fun r => List.filter (fun r' => REG_beq (widest_register_of r) (widest_register_of r')) (list_all REG)) + r. Definition reg_of_index_and_shift_and_bitcount_opt := fun '(index, offset, size) => - let sz := N.log2 (size / 8) in - let offset_n := (offset / 8)%N in - if ((8 * 2^sz =? size) && (offset =? offset_n * 8))%N%bool - then (rs <- nth_error (regs_of_index index) (N.to_nat sz); - nth_error rs (N.to_nat offset_n))%option - else None. + (wr <- widest_register_of_index_opt index; + let rs := overlapping_registers wr in + List.find (fun r => ((reg_size r =? size) && (reg_offset r =? offset))%N%bool) rs)%option. + Definition reg_of_index_and_shift_and_bitcount := fun '(index, offset, size) => match reg_of_index_and_shift_and_bitcount_opt (index, offset, size) with @@ -327,59 +339,6 @@ Definition reg_of_index_and_shift_and_bitcount := | None => widest_register_of_index index end. -Lemma widest_register_of_index_correct - : forall n, - (~exists r, reg_index r = n) - \/ (let r := widest_register_of_index n in reg_index r = n - /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N). -Proof. - intro n; set (r := widest_register_of_index n). - cbv in r. - repeat match goal with r := context[match ?n with _ => _ end] |- _ => destruct n; [ right | ] end; - [ .. | left; intros [ [] H]; cbv in H; congruence ]. - all: subst r; split; [ reflexivity | ]. - all: intros [] H; cbv in H; try (exfalso; congruence). - all: try (left; reflexivity). - all: try (right; vm_compute; reflexivity). -Qed. - -Lemma reg_of_index_and_shift_and_bitcount_opt_correct v r - : reg_of_index_and_shift_and_bitcount_opt v = Some r <-> index_and_shift_and_bitcount_of_reg r = v. -Proof. - split; [ | intro; subst; destruct r; vm_compute; reflexivity ]. - cbv [index_and_shift_and_bitcount_of_reg]; destruct v as [ [index shift] bitcount ]. - cbv [reg_of_index_and_shift_and_bitcount_opt]. - generalize (shift / 8)%N (N.log2 (bitcount / 8)); intros *. - repeat first [ congruence - | progress subst - | match goal with - | [ H : _ /\ _ |- _ ] => destruct H - | [ H : N.to_nat _ = _ |- _ ] => apply (f_equal N.of_nat) in H; rewrite N2Nat.id in H; subst - | [ |- Some _ = Some _ -> _ ] => inversion 1; subst - | [ |- context[match ?x with _ => _ end] ] => destruct x eqn:?; subst - end - | progress cbv [regs_of_index] - | match goal with - | [ |- context[nth_error _ ?n] ] => destruct n eqn:?; cbn [nth_error Option.bind] - end - | rewrite Bool.andb_true_iff, ?N.eqb_eq in * |- ]. - all: vm_compute; reflexivity. -Qed. - -Lemma reg_of_index_and_shift_and_bitcount_of_reg r - : reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r. -Proof. destruct r; vm_compute; reflexivity. Qed. - -Lemma reg_of_index_and_shift_and_bitcount_eq v r - : reg_of_index_and_shift_and_bitcount v = r - -> (index_and_shift_and_bitcount_of_reg r = v - \/ ((~exists r, index_and_shift_and_bitcount_of_reg r = v) - /\ r = widest_register_of_index (fst (fst v)))). -Proof. - cbv [reg_of_index_and_shift_and_bitcount]. - destruct v as [ [index offset] size ]. - destruct reg_of_index_and_shift_and_bitcount_opt eqn:H; - [ left | right; split; [ intros [r' H'] | ] ]; subst; try reflexivity. - { rewrite reg_of_index_and_shift_and_bitcount_opt_correct in H; assumption. } - { rewrite <- reg_of_index_and_shift_and_bitcount_opt_correct in H'; congruence. } -Qed. +Class assembly_program_options := { + default_rel : bool ; +}. diff --git a/src/Assembly/SyntaxTests.v b/src/Assembly/SyntaxTests.v new file mode 100644 index 0000000000..4659c239df --- /dev/null +++ b/src/Assembly/SyntaxTests.v @@ -0,0 +1,155 @@ +From Coq Require Import ZArith. +From Coq Require Import NArith. +From Coq Require Import String. +From Coq Require Import List. +From Coq Require Import Derive. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Bool.Reflect. +Require Import Crypto.Util.Listable. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Assembly.Syntax. +Require Crypto.Util.Tuple. +Require Crypto.Util.OptionList. +Import ListNotations. + +Local Open Scope list_scope. + +Local Set Implicit Arguments. +Local Set Primitive Projections. + +Local Coercion N.of_nat : nat >-> N. + +Lemma reg_of_index_and_shift_and_bitcount_opt_of_index_and_shift_and_bitcount_of_reg : forall r : REG, reg_of_index_and_shift_and_bitcount_opt (index_and_shift_and_bitcount_of_reg r) = Some r. +Proof. destruct r; vm_compute; try reflexivity. Defined. + +Lemma reg_of_index_and_shift_and_bitcount_of_index_and_shift_and_bitcount_of_reg : forall r : REG, reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r. +Proof. destruct r; vm_compute; reflexivity. Defined. + +Lemma reg_index_widest_register_of : forall r : REG, reg_index (widest_register_of r) = reg_index r. +Proof. destruct r; reflexivity. Defined. + +Lemma reg_index_widest_register_of_index_opt : forall index : N, (N.to_nat index option_map reg_index (widest_register_of_index_opt index) = Some index. +Proof. + intros index; cbv [widest_register_of_index_opt]. + rewrite <- (N2Nat.id index), Nat2N.id; generalize (N.to_nat index); clear index; intro index. + vm_compute List.map. + vm_compute List.length. + cbv [Nat.ltb]; cbn [Nat.leb]. + repeat lazymatch goal with + | [ |- false = true -> _ ] => discriminate + | [ |- (?index <=? _) = true -> _ ] => + is_var index; destruct index; [ reflexivity | cbn [Nat.leb] ] + end. +Qed. + +Lemma widest_register_of_index_opt_Some_length_iff : forall index : N, (exists r, widest_register_of_index_opt index = Some r) <-> (N.to_nat index _ ] => is_var index; destruct index; cbn [nth_error] + | [ |- _ <-> false = true ] => split; [ | discriminate ] + | [ |- _ <-> true = true ] => repeat esplit + | [ |- _ <-> (?index <=? _) = true ] => + is_var index; destruct index; cbn [Nat.leb nth_error] + end. + all: intros [? H]; discriminate. +Qed. + +Lemma reg_index_widest_register_of_index : forall index : N, (N.to_nat index reg_index (widest_register_of_index index) = index. +Proof. + intros index H; cbv [widest_register_of_index]. + apply reg_index_widest_register_of_index_opt in H. + destruct widest_register_of_index_opt; cbv [option_map] in *; inversion H; subst. + reflexivity. +Qed. + +Lemma reg_index_overlapping_registers : forall r r' n, nth_error (overlapping_registers r) n = Some r' -> reg_index r' = reg_index r. +Proof. + intros r r' n; destruct r. + all: vm_compute overlapping_registers. + all: repeat lazymatch goal with + | [ |- nth_error (_ :: _) ?v = Some _ -> _ ] => is_var v; destruct v; cbn [nth_error] + | [ |- nth_error [] ?v = Some _ -> _ ] => is_var v; destruct v; cbn [nth_error] + | [ |- Some _ = Some _ -> _ ] => let H := fresh in intro H; inversion H + | [ |- None = Some _ -> _ ] => let H := fresh in intro H; inversion H + end. + all: subst; reflexivity. +Qed. + +Lemma reg_of_index_and_shift_and_bitcount_of_reg r + : reg_of_index_and_shift_and_bitcount (index_and_shift_and_bitcount_of_reg r) = r. +Proof. destruct r; vm_compute; reflexivity. Qed. + +Lemma widest_register_of_index_opt_correct + : forall n r, widest_register_of_index_opt n = Some r -> + reg_index r = n + /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N. +Proof. + intros n r H. + epose proof (proj1 (widest_register_of_index_opt_Some_length_iff _) (ex_intro _ _ H)) as H'. + pose proof H' as H''. + apply reg_index_widest_register_of_index_opt in H''. + rewrite H in H''; cbn in H''; inversion H''; subst. + split; [ reflexivity | ]. + destruct r, r'. + all: vm_compute; try (constructor; reflexivity); try discriminate. +Qed. + +Lemma widest_register_of_index_correct + : forall n, + (~exists r, reg_index r = n) + \/ (let r := widest_register_of_index n in reg_index r = n + /\ forall r', reg_index r' = n -> r = r' \/ (reg_size r' < reg_size r)%N). +Proof. + intro n; pose proof (widest_register_of_index_opt_correct n) as H. + cbv [widest_register_of_index]. + destruct (widest_register_of_index_opt n) as [r |] eqn:H'; [ right; apply H; reflexivity | left ]. + intros [ [] H'' ]; subst; cbv in H'. + all: inversion H'. +Qed. + +Lemma reg_of_index_and_shift_and_bitcount_opt_correct v r + : reg_of_index_and_shift_and_bitcount_opt v = Some r <-> index_and_shift_and_bitcount_of_reg r = v. +Proof. + split; [ | intro; subst; destruct r; vm_compute; reflexivity ]. + cbv [index_and_shift_and_bitcount_of_reg]; destruct v as [ [index shift] bitcount ]. + cbv [reg_of_index_and_shift_and_bitcount_opt]. + pose proof (reg_index_widest_register_of_index index) as H''. + cbv [widest_register_of_index] in H''. + rewrite <- widest_register_of_index_opt_Some_length_iff in H''. + destruct widest_register_of_index_opt eqn:H; [ | intro H'; cbv in H'; now inversion H' ]. + cbv [Option.bind Option.sequence_return] in *. + specialize (H'' (ex_intro _ _ eq_refl)). + subst. + rewrite find_some_iff. + repeat first + [ progress intros + | progress destruct_head'_ex + | progress destruct_head'_and + | progress reflect_hyps + | progress subst + | match goal with + | [ H : nth_error (overlapping_registers _) _ = Some _ |- _ ] => + apply reg_index_overlapping_registers in H; try rewrite H + end + | reflexivity ]. +Qed. + +Lemma reg_of_index_and_shift_and_bitcount_eq v r + : reg_of_index_and_shift_and_bitcount v = r + -> (index_and_shift_and_bitcount_of_reg r = v + \/ ((~exists r, index_and_shift_and_bitcount_of_reg r = v) + /\ r = widest_register_of_index (fst (fst v)))). +Proof. + cbv [reg_of_index_and_shift_and_bitcount]. + destruct v as [ [index offset] size ]. + destruct reg_of_index_and_shift_and_bitcount_opt eqn:H; + [ left | right; split; [ intros [r' H'] | ] ]; subst; try reflexivity. + { rewrite reg_of_index_and_shift_and_bitcount_opt_correct in H; assumption. } + { rewrite <- reg_of_index_and_shift_and_bitcount_opt_correct in H'; congruence. } +Qed. diff --git a/src/Assembly/WithBedrock/Proofs.v b/src/Assembly/WithBedrock/Proofs.v index aa0cf55824..08ec58e652 100644 --- a/src/Assembly/WithBedrock/Proofs.v +++ b/src/Assembly/WithBedrock/Proofs.v @@ -245,7 +245,7 @@ Definition init_symbolic_state_G (m : machine_state) let '(initial_reg_idxs, (G, d)) := dag_gensym_n_G vals st in (G, {| dag_state := d - ; symbolic_reg_state := Tuple.from_list_default None 16 (List.map Some initial_reg_idxs) + ; symbolic_reg_state := Tuple.from_list_default None _ (List.map Some initial_reg_idxs) ; symbolic_flag_state := Tuple.repeat None 6 ; symbolic_mem_state := [] |}). @@ -254,7 +254,7 @@ Lemma init_symbolic_state_eq_G G d m : init_symbolic_state d = snd (init_symbolic_state_G m (G, d)). Proof. cbv [init_symbolic_state init_symbolic_state_G]. - epose proof (dag_gensym_n_eq_G G d (Tuple.to_list 16 m.(machine_reg_state))) as H. + epose proof (dag_gensym_n_eq_G G d (Tuple.to_list _ m.(machine_reg_state))) as H. rewrite Tuple.length_to_list in H; rewrite H; clear H. eta_expand; cbn [fst snd]. reflexivity. @@ -266,7 +266,7 @@ Lemma init_symbolic_state_G_ok m G d G' ss (H : init_symbolic_state_G m (G, d) = (G', ss)) (d' := ss.(dag_state)) (Hframe : frame m) - (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list 16 m.(machine_reg_state))) + (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state))) : R frame G' ss m /\ (forall reg, Option.is_Some (Symbolic.get_reg ss.(symbolic_reg_state) (reg_index reg)) = true) /\ gensym_dag_ok G' d' @@ -291,11 +291,11 @@ Proof. by (eapply dag_gensym_n_G_ok; [ | eta_expand; reflexivity | ]; assumption). clear; cbv [reg_index]; break_innermost_match; lia. } set (v := dag_gensym_n_G _ _) in *; clearbody v; destruct_head'_prod; cbn [fst snd] in *. - eassert (H' : Tuple.to_list 16 m.(machine_reg_state) = _). + eassert (H' : Tuple.to_list _ m.(machine_reg_state) = _). { repeat match goal with H : _ |- _ => clear H end. cbv [Tuple.to_list Tuple.to_list']. set_evars; eta_expand; subst_evars; reflexivity. } - generalize dependent (Tuple.to_list 16 m.(machine_reg_state)); intros; subst. + generalize dependent (Tuple.to_list _ m.(machine_reg_state)); intros; subst. repeat match goal with H : context[?x :: _] |- _ => assert_fails is_var x; set x in * end. repeat match goal with H : Forall2 _ ?v (_ :: _) |- _ => is_var v; inversion H; clear H; subst end. repeat match goal with H : Forall2 _ ?v nil |- _ => is_var v; inversion H; clear H; subst end. @@ -313,7 +313,7 @@ Lemma init_symbolic_state_ok m G d (Hd : gensym_dag_ok G d) (ss := init_symbolic_state d) (d' := ss.(dag_state)) - (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list 16 m.(machine_reg_state))) + (Hbounds : Forall (fun v => (0 <= v < 2^64)%Z) (Tuple.to_list _ m.(machine_reg_state))) (Hframe : frame m) : exists G', R frame G' ss m @@ -332,12 +332,12 @@ Lemma get_reg_of_R_regs G d r mr reg : forall idx', Symbolic.get_reg r (reg_index reg) = Some idx' -> eval_idx_Z G d idx' (Semantics.get_reg mr reg). Proof. assert (reg_offset reg = 0%N) by now destruct reg. - assert (reg_index reg < length (Tuple.to_list _ r)) + assert (N.to_nat (reg_index reg) < List.length (Tuple.to_list _ r)) by now rewrite Tuple.length_to_list; destruct reg; cbv [reg_index]; lia. cbv [Symbolic.get_reg Semantics.get_reg R_regs] in *. rewrite Tuple.fieldwise_to_list_iff in Hreg. erewrite @Forall2_forall_iff in Hreg by now rewrite !Tuple.length_to_list. - specialize (Hreg (reg_index reg) ltac:(assumption)); rewrite !@Tuple.nth_default_to_list in *. + specialize (Hreg (N.to_nat (reg_index reg)) ltac:(assumption)); rewrite !@Tuple.nth_default_to_list in *. cbv [index_and_shift_and_bitcount_of_reg] in *. generalize dependent (reg_size reg); intros; subst. generalize dependent (reg_offset reg); intros; subst. @@ -464,7 +464,7 @@ Definition R_regs_preserved_v rn (m : Semantics.reg_state) := Z.land (Tuple.nth_default 0%Z rn m) (Z.ones 64). Definition R_regs_preserved G d G' d' (m : Semantics.reg_state) rs rs' - := forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v rn m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v. + := forall rn idx, Symbolic.get_reg rs' rn = Some idx -> exists idx', Symbolic.get_reg rs rn = Some idx' /\ let v := R_regs_preserved_v (N.to_nat rn) m in eval_idx_Z G d idx' v -> eval_idx_Z G' d' idx v. Global Instance R_regs_preserved_Reflexive G d m : Reflexive (R_regs_preserved G d G d m) | 100. Proof. intro; cbv [R_regs_preserved]; eauto. Qed. @@ -476,19 +476,22 @@ Lemma R_regs_subsumed_get_reg_same_eval G d G' d' rs rs' rm Proof. cbv [R_regs Symbolic.get_reg R_regs_preserved R_regs_preserved_v] in *. rewrite @Tuple.fieldwise_to_list_iff, @Forall2_forall_iff_nth_error in *. - intro i; specialize (H i); specialize (H_impl i). + intro i; specialize (H i); specialize (H_impl (N.of_nat i)). rewrite <- !@Tuple.nth_default_to_list in *. cbv [nth_default option_eq] in *. repeat first [ progress destruct_head'_and | progress destruct_head'_ex + | progress inversion_option | rewrite @Tuple.length_to_list in * | progress cbv [R_reg eval_idx_Z] in * | progress break_innermost_match | progress break_innermost_match_hyps + | rewrite !Nat2N.id in * | now auto | progress intros | progress subst | match goal with + | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ] => rewrite H in H' | [ H : nth_error _ _ = None |- _ ] => apply nth_error_error_length in H | [ H : ?i >= ?n, H' : context[nth_error (Tuple.to_list ?n _) ?i] |- _ ] => rewrite nth_error_length_error in H' by now rewrite Tuple.length_to_list; lia @@ -501,12 +504,13 @@ Qed. Lemma R_regs_preserved_set_reg G d G' d' rs rs' ri rm v (H : R_regs_preserved G d G' d' rm rs rs') - (H_same : (ri < 16)%nat -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v ri rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') + (H_same : (ri < N.of_nat (List.length widest_registers))%N -> exists idx, Symbolic.get_reg rs ri = Some idx /\ let v' := R_regs_preserved_v (N.to_nat ri) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') : R_regs_preserved G d G' d' rm rs (Symbolic.set_reg rs' ri v). Proof. cbv [R_regs_preserved] in *. intros rn idx; specialize (H rn). rewrite get_reg_set_reg_full; intro. + vm_compute (length widest_registers) in *. repeat first [ progress break_innermost_match_hyps | progress inversion_option | progress subst @@ -527,7 +531,7 @@ Qed. Lemma R_regs_preserved_fold_left_set_reg_index {T1 T2} G d G' d' rs rs' rm (r_idxs : list (_ * (_ * T1 + _ * T2))) (H : R_regs_preserved G d G' d' rm rs rs') - (H_same : Forall (fun '(r, v) => let v := match v with inl (v, _) => v | inr (v, _) => v end in exists idx, Symbolic.get_reg rs (reg_index r) = Some idx /\ let v' := R_regs_preserved_v (reg_index r) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') r_idxs) + (H_same : Forall (fun '(r, v) => let v := match v with inl (v, _) => v | inr (v, _) => v end in exists idx, Symbolic.get_reg rs (reg_index r) = Some idx /\ let v' := R_regs_preserved_v (N.to_nat (reg_index r)) rm in eval_idx_Z G d idx v' -> eval_idx_Z G' d' v v') r_idxs) : R_regs_preserved G d G' d' rm rs @@ -548,12 +552,12 @@ Qed. Lemma Semantics_get_reg_eq_nth_default_of_R_regs G d ss ms r (Hsz : reg_size r = 64%N) (HR : R_regs G d ss ms) - : Semantics.get_reg ms r = Tuple.nth_default 0%Z (reg_index r) (ms : Semantics.reg_state). + : Semantics.get_reg ms r = Tuple.nth_default 0%Z (N.to_nat (reg_index r)) (ms : Semantics.reg_state). Proof. assert (Hro : reg_offset r = 0%N) by now revert Hsz; clear; cbv; destruct r; lia. cbv [R_regs R_reg] in HR. rewrite Tuple.fieldwise_to_list_iff, Forall2_forall_iff_nth_error in HR. - specialize (HR (reg_index r)). + specialize (HR (N.to_nat (reg_index r))). cbv [Semantics.get_reg index_and_shift_and_bitcount_of_reg]. rewrite Hro, Hsz; change (Z.of_N 0) with 0%Z; change (Z.of_N 64) with 64%Z. rewrite Z.shiftr_0_r, <- Tuple.nth_default_to_list; cbv [nth_default option_eq] in *. @@ -563,7 +567,7 @@ Qed. Lemma Semantics_get_reg_eq_nth_default_of_R frame G ss ms r (Hsz : reg_size r = 64%N) (HR : R frame G ss ms) - : Semantics.get_reg ms r = Tuple.nth_default 0%Z (reg_index r) (ms : Semantics.reg_state). + : Semantics.get_reg ms r = Tuple.nth_default 0%Z (N.to_nat (reg_index r)) (ms : Semantics.reg_state). Proof. destruct ss, ms; eapply Semantics_get_reg_eq_nth_default_of_R_regs; try eassumption; apply HR. Qed. @@ -586,7 +590,7 @@ Lemma Forall2_R_regs_preserved_same_helper G d reg_available idxs m rs : Forall (fun '(r, v) => let v := match v with inl (v, _) => v | inr (v, _) => v end in exists idx, Symbolic.get_reg rs (reg_index r) = Some idx - /\ let v' := R_regs_preserved_v (reg_index r) m in eval_idx_Z G d idx v' -> eval_idx_Z G d v v') + /\ let v' := R_regs_preserved_v (N.to_nat (reg_index r)) m in eval_idx_Z G d idx v' -> eval_idx_Z G d v v') (List.combine reg_available idxs). Proof. cbv [get_asm_reg] in *. diff --git a/src/Assembly/WithBedrock/Semantics.v b/src/Assembly/WithBedrock/Semantics.v index f436d155d7..695e4aa6c2 100644 --- a/src/Assembly/WithBedrock/Semantics.v +++ b/src/Assembly/WithBedrock/Semantics.v @@ -53,23 +53,23 @@ Definition havoc_flag (st : flag_state) (f : FLAG) : flag_state Definition havoc_flags : flag_state := (None, None, None, None, None, None). -Definition reg_state := Tuple.tuple Z 16. +Definition reg_state := Tuple.tuple Z (compute! (List.length widest_registers)). Definition bitmask_of_reg (r : REG) : Z := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in Z.shiftl (Z.ones (Z.of_N bitcount)) (Z.of_N shift). Definition get_reg (st : reg_state) (r : REG) : Z := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in - let rv := Tuple.nth_default 0%Z idx st in + let rv := Tuple.nth_default 0%Z (N.to_nat idx) st in Z.land (Z.shiftr rv (Z.of_N shift)) (Z.ones (Z.of_N bitcount)). Definition set_reg (st : reg_state) (r : REG) (v : Z) : reg_state := let '(idx, shift, bitcount) := index_and_shift_and_bitcount_of_reg r in Tuple.from_list_default 0%Z _ (ListUtil.update_nth - idx + (N.to_nat idx) (fun curv => Z.lor (Z.shiftl (Z.land v (Z.ones (Z.of_N bitcount))) (Z.of_N shift)) (Z.ldiff curv (Z.shiftl (Z.ones (Z.of_N bitcount)) (Z.of_N shift)))) (Tuple.to_list _ st)). Definition annotate_reg_state (st : reg_state) : list (REG * Z) - := List.map (fun '(n, v) => (widest_register_of_index n, v)) (enumerate (Tuple.to_list _ st)). + := List.combine widest_registers (Tuple.to_list _ st). Ltac print_reg_state st := let st' := (eval cbv in (annotate_reg_state st)) in idtac st'. (* Kludge since [byte] isn't present in Coq 8.9 *) diff --git a/src/Assembly/WithBedrock/SymbolicProofs.v b/src/Assembly/WithBedrock/SymbolicProofs.v index 38e9c0ccaf..a5ffb70215 100644 --- a/src/Assembly/WithBedrock/SymbolicProofs.v +++ b/src/Assembly/WithBedrock/SymbolicProofs.v @@ -314,7 +314,7 @@ Qed. Lemma get_reg_R_regs d s m (HR : R_regs d s m) ri : forall i, Symbolic.get_reg s ri = Some i -> - exists v, eval d i v /\ Tuple.nth_default 0 ri m = v. + exists v, eval d i v /\ Tuple.nth_default 0 (N.to_nat ri) m = v. Proof using Type. cbv [Symbolic.get_reg]; intros. rewrite <-Tuple.nth_default_to_list in H. @@ -336,7 +336,7 @@ Qed. Lemma get_reg_R s m (HR : R s m) ri : forall i, Symbolic.get_reg s ri = Some i -> - exists v, eval s i v /\ Tuple.nth_default 0 ri (m : reg_state) = v. + exists v, eval s i v /\ Tuple.nth_default 0 (N.to_nat ri) (m : reg_state) = v. Proof using Type. destruct s, m; apply get_reg_R_regs, HR. Qed. diff --git a/src/Util/Listable.v b/src/Util/Listable.v index feaad2c888..f898c909e7 100644 --- a/src/Util/Listable.v +++ b/src/Util/Listable.v @@ -7,6 +7,7 @@ Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Bool.Reflect. Import ListNotations. +(* TODO: move to using [N] for performance instead of [nat] *) Class Listable T := { list_all : list T ; find_index : T -> nat }. Arguments find_index {T} {_} _.