From e550a66a0a5afd6ddc18ac4a682904c7fcca96c4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 4 Mar 2025 20:26:01 -0800 Subject: [PATCH] Use Listable to prove equality of registers and opcodes (#2020) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 … --- 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} {_} _.