From 2affbaf276bd3d0d09850c5fdc018f5f6e39d3a9 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Dec 2023 10:33:42 -0800 Subject: [PATCH] More fine-grained bounds analysis Of `if` and `Z.{max,min,ltb,leb,gtb,geb}` Splitting out a bit of https://github.com/mit-plv/fiat-crypto/pull/1609 that can be merged in isolation
Timing Diff

``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 118m07.69s | 2852656 ko | Total Time / Peak Mem | 120m57.22s | 2852384 ko || -2m49.52s || 272 ko | -2.33% | +0.00% ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ 8m11.53s | 2656284 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m35.13s | 2651116 ko || -0m23.60s || 5168 ko | -4.58% | +0.19% 1m42.29s | 1598056 ko | fiat-rust/src/p384_32.rs | 1m53.13s | 1711156 ko || -0m10.84s || -113100 ko | -9.58% | -6.60% 1m40.37s | 1910616 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m50.67s | 1914612 ko || -0m10.29s || -3996 ko | -9.30% | -0.20% 1m44.95s | 1868664 ko | fiat-go/32/p384scalar/p384scalar.go | 1m53.23s | 1629028 ko || -0m08.27s || 239636 ko | -7.31% | +14.71% 1m44.01s | 1694084 ko | fiat-json/src/p384_32.json | 1m52.15s | 2062740 ko || -0m08.14s || -368656 ko | -7.25% | -17.87% 1m43.70s | 1598448 ko | fiat-go/32/p384/p384.go | 1m51.29s | 2096096 ko || -0m07.58s || -497648 ko | -6.82% | -23.74% 1m43.12s | 1970240 ko | fiat-c/src/p384_scalar_32.c | 1m50.95s | 1753688 ko || -0m07.82s || 216552 ko | -7.05% | +12.34% 1m47.93s | 1777564 ko | fiat-zig/src/p384_scalar_32.zig | 1m54.10s | 1960872 ko || -0m06.16s || -183308 ko | -5.40% | -9.34% 1m45.63s | 1859004 ko | fiat-rust/src/p384_scalar_32.rs | 1m52.38s | 1691776 ko || -0m06.75s || 167228 ko | -6.00% | +9.88% 1m41.00s | 2040020 ko | fiat-c/src/p384_32.c | 1m47.40s | 1613808 ko || -0m06.40s || 426212 ko | -5.95% | +26.41% 1m49.12s | 1707240 ko | fiat-json/src/p384_scalar_32.json | 1m55.04s | 1915948 ko || -0m05.91s || -208708 ko | -5.14% | -10.89% 1m47.23s | 1742608 ko | fiat-zig/src/p384_32.zig | 1m51.91s | 1965108 ko || -0m04.68s || -222500 ko | -4.18% | -11.32% 0m34.08s | 108600 ko | fiat-json/src/p521_32.json | 0m38.51s | 110272 ko || -0m04.42s || -1672 ko | -11.50% | -1.51% 1m51.33s | 1766248 ko | fiat-java/src/FiatP384Scalar.java | 1m55.23s | 1672896 ko || -0m03.89s || 93352 ko | -3.38% | +5.58% 1m49.07s | 1677504 ko | fiat-java/src/FiatP384.java | 1m52.11s | 1829396 ko || -0m03.04s || -151892 ko | -2.71% | -8.30% 1m48.39s | 2087004 ko | fiat-bedrock2/src/p384_32.c | 1m51.44s | 2002744 ko || -0m03.04s || 84260 ko | -2.73% | +4.20% 0m41.56s | 2147648 ko | ExtractionOCaml/bedrock2_solinas_reduction | 0m43.56s | 2147620 ko || -0m02.00s || 28 ko | -4.59% | +0.00% 0m16.06s | 305752 ko | fiat-rust/src/p434_64.rs | 0m18.74s | 245968 ko || -0m02.67s || 59784 ko | -14.30% | +24.30% 5m29.05s | 2852656 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m30.35s | 2852384 ko || -0m01.30s || 272 ko | -0.39% | +0.00% 1m18.17s | 1527676 ko | Assembly/EquivalenceProofs.vo | 1m19.80s | 1528936 ko || -0m01.62s || -1260 ko | -2.04% | -0.08% 0m54.68s | 864844 ko | AbstractInterpretation/ZRangeProofs.vo | 0m53.49s | 847940 ko || +0m01.18s || 16904 ko | +2.22% | +1.99% 0m41.26s | 2147868 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery | 0m43.00s | 2147828 ko || -0m01.74s || 40 ko | -4.04% | +0.00% 0m40.43s | 2147800 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery | 0m42.31s | 2147868 ko || -0m01.88s || -68 ko | -4.44% | -0.00% 0m39.00s | 2148408 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas | 0m40.19s | 2148288 ko || -0m01.18s || 120 ko | -2.96% | +0.00% 0m36.59s | 1642524 ko | ExtractionOCaml/bedrock2_dettman_multiplication | 0m38.32s | 1642028 ko || -0m01.72s || 496 ko | -4.51% | +0.03% 0m36.09s | 1624132 ko | ExtractionOCaml/bedrock2_saturated_solinas | 0m37.77s | 1622392 ko || -0m01.67s || 1740 ko | -4.44% | +0.10% 0m35.64s | 1618740 ko | ExtractionOCaml/bedrock2_base_conversion | 0m37.32s | 1620464 ko || -0m01.67s || -1724 ko | -4.50% | -0.10% 0m35.51s | 1627416 ko | ExtractionOCaml/with_bedrock2_saturated_solinas | 0m36.77s | 1623636 ko || -0m01.26s || 3780 ko | -3.42% | +0.23% 0m35.32s | 1618208 ko | ExtractionOCaml/with_bedrock2_base_conversion | 0m36.78s | 1620312 ko || -0m01.46s || -2104 ko | -3.96% | -0.12% 0m35.16s | 1624836 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication | 0m36.65s | 1624768 ko || -0m01.49s || 68 ko | -4.06% | +0.00% 0m28.09s | 1232176 ko | ExtractionOCaml/perf_unsaturated_solinas | 0m29.26s | 1232192 ko || -0m01.17s || -16 ko | -3.99% | -0.00% 0m17.56s | 306028 ko | fiat-go/64/p434/p434.go | 0m18.81s | 312620 ko || -0m01.25s || -6592 ko | -6.64% | -2.10% 0m17.14s | 233816 ko | fiat-c/src/p434_64.c | 0m18.20s | 233352 ko || -0m01.05s || 464 ko | -5.82% | +0.19% 0m15.36s | 426148 ko | fiat-json/src/curve25519_scalar_32.json | 0m16.62s | 378608 ko || -0m01.26s || 47540 ko | -7.58% | +12.55% 4m01.16s | 2561424 ko | Assembly/WithBedrock/Proofs.vo | 4m00.36s | 2560184 ko || +0m00.79s || 1240 ko | +0.33% | +0.04% 3m13.40s | 2602832 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 3m13.52s | 2602864 ko || -0m00.12s || -32 ko | -0.06% | -0.00% 1m51.86s | 1595228 ko | Bedrock/End2End/X25519/Field25519.vo | 1m51.80s | 1594816 ko || +0m00.06s || 412 ko | +0.05% | +0.02% 1m48.00s | 1749600 ko | fiat-bedrock2/src/p384_scalar_32.c | 1m48.76s | 2096800 ko || -0m00.75s || -347200 ko | -0.69% | -16.55% 1m47.72s | 2435524 ko | Fancy/Barrett256.vo | 1m47.86s | 2427488 ko || -0m00.14s || 8036 ko | -0.12% | +0.33% 1m28.12s | 2041012 ko | SlowPrimeSynthesisExamples.vo | 1m28.22s | 2041020 ko || -0m00.09s || -8 ko | -0.11% | -0.00% 1m08.85s | 1435264 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m08.65s | 1437236 ko || +0m00.19s || -1972 ko | +0.29% | -0.13% 1m01.35s | 875184 ko | AbstractInterpretation/Wf.vo | 1m01.39s | 875564 ko || -0m00.03s || -380 ko | -0.06% | -0.04% 0m47.33s | 1517272 ko | Assembly/Symbolic.vo | 0m47.25s | 1517300 ko || +0m00.07s || -28 ko | +0.16% | -0.00% 0m45.93s | 1761576 ko | Fancy/Montgomery256.vo | 0m45.85s | 1758788 ko || +0m00.07s || 2788 ko | +0.17% | +0.15% 0m45.55s | 1106852 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m45.30s | 1108620 ko || +0m00.25s || -1768 ko | +0.55% | -0.15% 0m41.79s | 2146792 ko | ExtractionOCaml/solinas_reduction | 0m41.41s | 2146912 ko || +0m00.38s || -120 ko | +0.91% | -0.00% 0m40.94s | 66976 ko | fiat-go/32/p521/p521.go | 0m41.62s | 62044 ko || -0m00.67s || 4932 ko | -1.63% | +7.94% 0m40.04s | 2148432 ko | ExtractionOCaml/bedrock2_unsaturated_solinas | 0m41.02s | 2148352 ko || -0m00.98s || 80 ko | -2.38% | +0.00% 0m39.54s | 2146728 ko | ExtractionOCaml/word_by_word_montgomery | 0m39.44s | 2146928 ko || +0m00.10s || -200 ko | +0.25% | -0.00% 0m38.92s | 143296 ko | fiat-bedrock2/src/p521_32.c | 0m38.94s | 140708 ko || -0m00.01s || 2588 ko | -0.05% | +1.83% 0m38.60s | 1013256 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m38.76s | 1014568 ko || -0m00.15s || -1312 ko | -0.41% | -0.12% 0m38.33s | 64612 ko | fiat-zig/src/p521_32.zig | 0m38.23s | 64104 ko || +0m00.10s || 508 ko | +0.26% | +0.79% 0m37.84s | 61744 ko | fiat-java/src/FiatP521.java | 0m38.30s | 62888 ko || -0m00.45s || -1144 ko | -1.20% | -1.81% 0m37.61s | 63940 ko | fiat-rust/src/p521_32.rs | 0m38.25s | 60432 ko || -0m00.64s || 3508 ko | -1.67% | +5.80% 0m37.53s | 60244 ko | fiat-c/src/p521_32.c | 0m38.16s | 61116 ko || -0m00.62s || -872 ko | -1.65% | -1.42% 0m36.96s | 1652372 ko | ExtractionOCaml/unsaturated_solinas | 0m36.97s | 1652860 ko || -0m00.00s || -488 ko | -0.02% | -0.02% 0m36.39s | 1319040 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m36.96s | 1319208 ko || -0m00.57s || -168 ko | -1.54% | -0.01% 0m35.47s | 1626948 ko | ExtractionOCaml/with_bedrock2_solinas_reduction | 0m35.91s | 1623640 ko || -0m00.43s || 3308 ko | -1.22% | +0.20% 0m35.40s | 1532564 ko | ExtractionOCaml/base_conversion | 0m34.76s | 1534804 ko || +0m00.64s || -2240 ko | +1.84% | -0.14% 0m34.67s | 1556164 ko | ExtractionOCaml/dettman_multiplication | 0m34.66s | 1555920 ko || +0m00.01s || 244 ko | +0.02% | +0.01% 0m34.04s | 2239244 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml | 0m34.06s | 2241716 ko || -0m00.02s || -2472 ko | -0.05% | -0.11% 0m33.88s | 1279440 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m34.21s | 1279492 ko || -0m00.32s || -52 ko | -0.96% | -0.00% 0m33.55s | 1536436 ko | ExtractionOCaml/saturated_solinas | 0m33.64s | 1537180 ko || -0m00.09s || -744 ko | -0.26% | -0.04% 0m33.12s | 2217312 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml | 0m33.14s | 2203232 ko || -0m00.02s || 14080 ko | -0.06% | +0.63% 0m33.07s | 2216360 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml | 0m33.22s | 2203556 ko || -0m00.14s || 12804 ko | -0.45% | +0.58% 0m32.66s | 2139416 ko | ExtractionOCaml/solinas_reduction.ml | 0m32.73s | 2136004 ko || -0m00.07s || 3412 ko | -0.21% | +0.15% 0m31.59s | 2121628 ko | ExtractionOCaml/word_by_word_montgomery.ml | 0m31.75s | 2120436 ko || -0m00.16s || 1192 ko | -0.50% | +0.05% 0m30.49s | 2124060 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml | 0m30.19s | 2135432 ko || +0m00.29s || -11372 ko | +0.99% | -0.53% 0m30.12s | 2124092 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml | 0m30.10s | 2136124 ko || +0m00.01s || -12032 ko | +0.06% | -0.56% 0m29.34s | 701176 ko | AbstractInterpretation/Proofs.vo | 0m29.28s | 704144 ko || +0m00.05s || -2968 ko | +0.20% | -0.42% 0m29.30s | 1522160 ko | StandaloneDebuggingExamples.vo | 0m29.30s | 1518292 ko || +0m00.00s || 3868 ko | +0.00% | +0.25% 0m28.80s | 2031644 ko | ExtractionOCaml/unsaturated_solinas.ml | 0m28.59s | 2032480 ko || +0m00.21s || -836 ko | +0.73% | -0.04% 0m28.79s | 1232252 ko | ExtractionOCaml/perf_word_by_word_montgomery | 0m29.69s | 1232280 ko || -0m00.90s || -28 ko | -3.03% | -0.00% 0m27.14s | 2070388 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml | 0m27.14s | 2071988 ko || +0m00.00s || -1600 ko | +0.00% | -0.07% 0m26.26s | 2000772 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml | 0m26.20s | 1996072 ko || +0m00.06s || 4700 ko | +0.22% | +0.23% 0m26.18s | 2038572 ko | ExtractionOCaml/bedrock2_base_conversion.ml | 0m26.15s | 2039460 ko || +0m00.03s || -888 ko | +0.11% | -0.04% 0m26.06s | 2000140 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml | 0m26.06s | 1997496 ko || +0m00.00s || 2644 ko | +0.00% | +0.13% 0m26.03s | 2000976 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml | 0m26.06s | 1997080 ko || -0m00.02s || 3896 ko | -0.11% | +0.19% 0m25.96s | 2001216 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml | 0m26.02s | 1997732 ko || -0m00.05s || 3484 ko | -0.23% | +0.17% 0m25.50s | 2038700 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml | 0m26.34s | 2040380 ko || -0m00.83s || -1680 ko | -3.18% | -0.08% 0m25.39s | 1943804 ko | ExtractionOCaml/dettman_multiplication.ml | 0m25.29s | 1940856 ko || +0m00.10s || 2948 ko | +0.39% | +0.15% 0m25.29s | 1370488 ko | PerfTesting/PerfTestSearch.vo | 0m25.48s | 1373524 ko || -0m00.19s || -3036 ko | -0.74% | -0.22% 0m24.75s | 1921636 ko | ExtractionOCaml/base_conversion.ml | 0m24.79s | 1921920 ko || -0m00.03s || -284 ko | -0.16% | -0.01% 0m24.52s | 1930464 ko | ExtractionOCaml/saturated_solinas.ml | 0m24.58s | 1930692 ko || -0m00.05s || -228 ko | -0.24% | -0.01% 0m23.82s | 1184144 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m23.87s | 1184016 ko || -0m00.05s || 128 ko | -0.20% | +0.01% 0m21.72s | 1350932 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m21.72s | 1350828 ko || +0m00.00s || 104 ko | +0.00% | +0.00% 0m20.50s | 1158648 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m20.70s | 1157940 ko || -0m00.19s || 708 ko | -0.96% | +0.06% 0m20.43s | 797092 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m20.43s | 794660 ko || +0m00.00s || 2432 ko | +0.00% | +0.30% 0m19.00s | 1129620 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m19.03s | 1130752 ko || -0m00.03s || -1132 ko | -0.15% | -0.10% 0m18.97s | 1826476 ko | ExtractionOCaml/perf_unsaturated_solinas.ml | 0m18.96s | 1826428 ko || +0m00.00s || 48 ko | +0.05% | +0.00% 0m18.96s | 1869440 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml | 0m19.48s | 1869604 ko || -0m00.51s || -164 ko | -2.66% | -0.00% 0m18.88s | 742056 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m18.85s | 737320 ko || +0m00.02s || 4736 ko | +0.15% | +0.64% 0m18.59s | 291896 ko | fiat-bedrock2/src/p434_64.c | 0m18.16s | 352412 ko || +0m00.42s || -60516 ko | +2.36% | -17.17% 0m17.88s | 252104 ko | fiat-zig/src/p434_64.zig | 0m17.38s | 250948 ko || +0m00.50s || 1156 ko | +2.87% | +0.46% 0m17.59s | 1373672 ko | PerfTesting/PerfTestSearchPattern.vo | 0m17.59s | 1373380 ko || +0m00.00s || 292 ko | +0.00% | +0.02% 0m17.56s | 497844 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_32.c | 0m17.66s | 489084 ko || -0m00.10s || 8760 ko | -0.56% | +1.79% 0m17.41s | 291724 ko | fiat-json/src/p434_64.json | 0m17.60s | 312988 ko || -0m00.19s || -21264 ko | -1.07% | -6.79% 0m17.35s | 404072 ko | fiat-bedrock2/src/p256_scalar_32.c | 0m17.40s | 428080 ko || -0m00.04s || -24008 ko | -0.28% | -5.60% 0m17.26s | 1206516 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.32s | 1208232 ko || -0m00.05s || -1716 ko | -0.34% | -0.14% 0m17.20s | 338132 ko | fiat-java/src/FiatSecp256K1MontgomeryScalar.java | 0m17.22s | 362240 ko || -0m00.01s || -24108 ko | -0.11% | -6.65% 0m17.18s | 1127712 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.07s | 1127832 ko || +0m00.10s || -120 ko | +0.64% | -0.01% 0m17.11s | 1145988 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m17.13s | 1146100 ko || -0m00.01s || -112 ko | -0.11% | -0.00% 0m17.06s | 387120 ko | fiat-bedrock2/src/secp256k1_montgomery_32.c | 0m16.54s | 443456 ko || +0m00.51s || -56336 ko | +3.14% | -12.70% 0m16.96s | 422020 ko | fiat-bedrock2/src/curve25519_scalar_32.c | 0m17.02s | 405584 ko || -0m00.05s || 16436 ko | -0.35% | +4.05% 0m16.81s | 422192 ko | fiat-java/src/FiatP256Scalar.java | 0m16.85s | 342228 ko || -0m00.04s || 79964 ko | -0.23% | +23.36% 0m16.66s | 442624 ko | fiat-zig/src/p256_scalar_32.zig | 0m16.95s | 409628 ko || -0m00.28s || 32996 ko | -1.71% | +8.05% 0m16.65s | 438324 ko | fiat-zig/src/secp256k1_montgomery_scalar_32.zig | 0m17.11s | 346784 ko || -0m00.46s || 91540 ko | -2.68% | +26.39% 0m16.64s | 407624 ko | fiat-json/src/p256_scalar_32.json | 0m17.19s | 455400 ko || -0m00.55s || -47776 ko | -3.19% | -10.49% 0m16.53s | 345100 ko | fiat-go/32/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m17.28s | 346872 ko || -0m00.75s || -1772 ko | -4.34% | -0.51% 0m16.53s | 396644 ko | fiat-zig/src/secp256k1_montgomery_32.zig | 0m16.02s | 435648 ko || +0m00.51s || -39004 ko | +3.18% | -8.95% 0m16.51s | 2094100 ko | ExtractionHaskell/with_bedrock2_solinas_reduction.hs | 0m15.61s | 2095512 ko || +0m00.90s || -1412 ko | +5.76% | -0.06% 0m16.49s | 406684 ko | fiat-zig/src/curve25519_scalar_32.zig | 0m15.98s | 345112 ko || +0m00.50s || 61572 ko | +3.19% | +17.84% 0m16.37s | 2093460 ko | ExtractionHaskell/bedrock2_solinas_reduction.hs | 0m16.35s | 2093640 ko || +0m00.01s || -180 ko | +0.12% | -0.00% 0m16.34s | 355372 ko | fiat-go/32/p256scalar/p256scalar.go | 0m17.01s | 336536 ko || -0m00.67s || 18836 ko | -3.93% | +5.59% 0m16.30s | 406028 ko | fiat-java/src/FiatCurve25519Scalar.java | 0m16.86s | 405600 ko || -0m00.55s || 428 ko | -3.32% | +0.10% 0m16.28s | 398648 ko | fiat-c/src/secp256k1_montgomery_scalar_32.c | 0m16.65s | 410752 ko || -0m00.36s || -12104 ko | -2.22% | -2.94% 0m16.26s | 392892 ko | fiat-json/src/secp256k1_montgomery_32.json | 0m16.20s | 380020 ko || +0m00.06s || 12872 ko | +0.37% | +3.38% 0m16.21s | 404640 ko | fiat-rust/src/p256_scalar_32.rs | 0m16.94s | 345940 ko || -0m00.73s || 58700 ko | -4.30% | +16.96% 0m16.13s | 2010332 ko | ExtractionHaskell/with_bedrock2_word_by_word_montgomery.hs | 0m16.34s | 2010428 ko || -0m00.21s || -96 ko | -1.28% | -0.00% 0m16.08s | 423192 ko | fiat-rust/src/secp256k1_montgomery_scalar_32.rs | 0m16.70s | 439012 ko || -0m00.62s || -15820 ko | -3.71% | -3.60% 0m16.07s | 414412 ko | fiat-java/src/FiatSecp256K1Montgomery.java | 0m16.78s | 368320 ko || -0m00.71s || 46092 ko | -4.23% | +12.51% 0m16.06s | 408448 ko | fiat-bedrock2/src/p256_32.c | 0m15.79s | 364756 ko || +0m00.26s || 43692 ko | +1.70% | +11.97% 0m16.06s | 335964 ko | fiat-c/src/p256_scalar_32.c | 0m16.56s | 343336 ko || -0m00.50s || -7372 ko | -3.01% | -2.14% 0m15.90s | 330100 ko | fiat-rust/src/secp256k1_montgomery_32.rs | 0m16.81s | 440356 ko || -0m00.90s || -110256 ko | -5.41% | -25.03% 0m15.85s | 428928 ko | fiat-json/src/secp256k1_montgomery_scalar_32.json | 0m16.40s | 361916 ko || -0m00.54s || 67012 ko | -3.35% | +18.51% 0m15.83s | 352752 ko | fiat-go/32/curve25519scalar/curve25519scalar.go | 0m15.84s | 439340 ko || -0m00.00s || -86588 ko | -0.06% | -19.70% 0m15.81s | 436524 ko | fiat-c/src/secp256k1_montgomery_32.c | 0m16.19s | 429096 ko || -0m00.38s || 7428 ko | -2.34% | +1.73% 0m15.75s | 443548 ko | fiat-go/32/secp256k1montgomery/secp256k1montgomery.go | 0m16.69s | 436064 ko || -0m00.94s || 7484 ko | -5.63% | +1.71% 0m15.74s | 2031652 ko | ExtractionHaskell/solinas_reduction.hs | 0m15.71s | 2027732 ko || +0m00.02s || 3920 ko | +0.19% | +0.19% 0m15.72s | 346384 ko | fiat-rust/src/curve25519_scalar_32.rs | 0m16.45s | 356200 ko || -0m00.72s || -9816 ko | -4.43% | -2.75% 0m15.56s | 387008 ko | fiat-c/src/curve25519_scalar_32.c | 0m16.01s | 416392 ko || -0m00.45s || -29384 ko | -2.81% | -7.05% 0m15.50s | 355240 ko | fiat-zig/src/p256_32.zig | 0m15.72s | 414944 ko || -0m00.22s || -59704 ko | -1.39% | -14.38% 0m15.42s | 1983776 ko | ExtractionHaskell/word_by_word_montgomery.hs | 0m15.41s | 1985996 ko || +0m00.00s || -2220 ko | +0.06% | -0.11% 0m15.41s | 2010140 ko | ExtractionHaskell/bedrock2_word_by_word_montgomery.hs | 0m16.13s | 2007524 ko || -0m00.71s || 2616 ko | -4.46% | +0.13% 0m15.14s | 387292 ko | fiat-java/src/FiatP256.java | 0m15.80s | 394640 ko || -0m00.66s || -7348 ko | -4.17% | -1.86% 0m15.12s | 1950604 ko | ExtractionHaskell/bedrock2_unsaturated_solinas.hs | 0m15.19s | 1950624 ko || -0m00.07s || -20 ko | -0.46% | -0.00% 0m15.07s | 354004 ko | fiat-rust/src/p256_32.rs | 0m15.96s | 390952 ko || -0m00.89s || -36948 ko | -5.57% | -9.45% 0m14.87s | 415960 ko | fiat-c/src/p256_32.c | 0m15.48s | 320752 ko || -0m00.61s || 95208 ko | -3.94% | +29.68% 0m14.86s | 360644 ko | fiat-json/src/p256_32.json | 0m15.39s | 446864 ko || -0m00.53s || -86220 ko | -3.44% | -19.29% 0m14.62s | 1933488 ko | ExtractionHaskell/unsaturated_solinas.hs | 0m14.75s | 1929252 ko || -0m00.13s || 4236 ko | -0.88% | +0.21% 0m14.53s | 341776 ko | fiat-go/32/p256/p256.go | 0m15.15s | 362036 ko || -0m00.62s || -20260 ko | -4.09% | -5.59% 0m14.47s | 1951532 ko | ExtractionHaskell/with_bedrock2_unsaturated_solinas.hs | 0m15.34s | 1950416 ko || -0m00.86s || 1116 ko | -5.67% | +0.05% 0m14.40s | 1886356 ko | ExtractionHaskell/with_bedrock2_dettman_multiplication.hs | 0m14.39s | 1887008 ko || +0m00.00s || -652 ko | +0.06% | -0.03% 0m14.35s | 1886684 ko | ExtractionHaskell/bedrock2_dettman_multiplication.hs | 0m14.27s | 1886136 ko || +0m00.08s || 548 ko | +0.56% | +0.02% 0m14.31s | 1932196 ko | ExtractionHaskell/with_bedrock2_base_conversion.hs | 0m14.24s | 1932776 ko || +0m00.07s || -580 ko | +0.49% | -0.03% 0m14.21s | 1862464 ko | ExtractionHaskell/with_bedrock2_saturated_solinas.hs | 0m14.21s | 1862348 ko || +0m00.00s || 116 ko | +0.00% | +0.00% 0m14.20s | 1932440 ko | ExtractionHaskell/bedrock2_base_conversion.hs | 0m13.64s | 1933348 ko || +0m00.55s || -908 ko | +4.10% | -0.04% 0m14.09s | 1863000 ko | ExtractionHaskell/bedrock2_saturated_solinas.hs | 0m14.17s | 1861768 ko || -0m00.08s || 1232 ko | -0.56% | +0.06% 0m13.88s | 1858476 ko | ExtractionHaskell/dettman_multiplication.hs | 0m13.90s | 1855680 ko || -0m00.01s || 2796 ko | -0.14% | +0.15% 0m13.70s | 1848820 ko | ExtractionHaskell/saturated_solinas.hs | 0m13.69s | 1847424 ko || +0m00.00s || 1396 ko | +0.07% | +0.07% 0m13.63s | 601740 ko | Bedrock/Field/Common/Util.vo | 0m13.74s | 607744 ko || -0m00.10s || -6004 ko | -0.80% | -0.98% 0m13.51s | 1849984 ko | ExtractionHaskell/base_conversion.hs | 0m13.43s | 1850900 ko || +0m00.08s || -916 ko | +0.59% | -0.04% 0m13.39s | 664432 ko | Bedrock/Group/AdditionChains.vo | 0m13.36s | 664280 ko || +0m00.03s || 152 ko | +0.22% | +0.02% 0m13.06s | 668412 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m13.13s | 667172 ko || -0m00.07s || 1240 ko | -0.53% | +0.18% 0m11.81s | 1031712 ko | BoundsPipeline.vo | 0m11.79s | 1030480 ko || +0m00.02s || 1232 ko | +0.16% | +0.11% 0m11.41s | 1698212 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.35s | 1698080 ko || +0m00.06s || 132 ko | +0.52% | +0.00% 0m11.02s | 165236 ko | fiat-go/64/p384scalar/p384scalar.go | 0m11.23s | 165448 ko || -0m00.21s || -212 ko | -1.86% | -0.12% 0m11.01s | 216400 ko | fiat-bedrock2/src/p384_scalar_64.c | 0m11.03s | 194560 ko || -0m00.01s || 21840 ko | -0.18% | +11.22% 0m10.89s | 191528 ko | fiat-zig/src/p384_scalar_64.zig | 0m11.07s | 193528 ko || -0m00.17s || -2000 ko | -1.62% | -1.03% 0m10.83s | 202864 ko | fiat-json/src/p384_scalar_64.json | 0m11.00s | 176204 ko || -0m00.16s || 26660 ko | -1.54% | +15.13% 0m10.72s | 142328 ko | fiat-rust/src/p384_scalar_64.rs | 0m10.83s | 141448 ko || -0m00.10s || 880 ko | -1.01% | +0.62% 0m10.59s | 140712 ko | fiat-c/src/p384_scalar_64.c | 0m11.00s | 154528 ko || -0m00.41s || -13816 ko | -3.72% | -8.94% 0m10.10s | 1296876 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.21s | 1296864 ko || -0m00.11s || 12 ko | -1.07% | +0.00% 0m09.85s | 626712 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.86s | 624056 ko || -0m00.00s || 2656 ko | -0.10% | +0.42% 0m09.79s | 215236 ko | fiat-bedrock2/src/p384_64.c | 0m09.43s | 215444 ko || +0m00.35s || -208 ko | +3.81% | -0.09% 0m09.41s | 597268 ko | Stringification/IR.vo | 0m09.43s | 596100 ko || -0m00.01s || 1168 ko | -0.21% | +0.19% 0m09.33s | 165208 ko | fiat-zig/src/p384_64.zig | 0m09.60s | 159780 ko || -0m00.26s || 5428 ko | -2.81% | +3.39% 0m09.32s | 1035796 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.26s | 1035900 ko || +0m00.06s || -104 ko | +0.64% | -0.01% 0m09.26s | 660684 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m09.22s | 660736 ko || +0m00.03s || -52 ko | +0.43% | -0.00% 0m09.09s | 281340 ko | fiat-bedrock2/src/p224_32.c | 0m09.37s | 256532 ko || -0m00.27s || 24808 ko | -2.98% | +9.67% 0m09.07s | 253804 ko | fiat-zig/src/p224_32.zig | 0m09.26s | 253128 ko || -0m00.18s || 676 ko | -2.05% | +0.26% 0m09.06s | 179420 ko | fiat-go/64/p384/p384.go | 0m09.53s | 159216 ko || -0m00.46s || 20204 ko | -4.93% | +12.68% 0m09.06s | 144912 ko | fiat-rust/src/p384_64.rs | 0m09.38s | 191232 ko || -0m00.32s || -46320 ko | -3.41% | -24.22% 0m09.01s | 261152 ko | fiat-json/src/p224_32.json | 0m08.97s | 238644 ko || +0m00.03s || 22508 ko | +0.44% | +9.43% 0m09.00s | 174204 ko | fiat-c/src/p384_64.c | 0m09.24s | 151968 ko || -0m00.24s || 22236 ko | -2.59% | +14.63% 0m09.00s | 224252 ko | fiat-go/32/p224/p224.go | 0m09.37s | 252692 ko || -0m00.36s || -28440 ko | -3.94% | -11.25% 0m08.95s | 244668 ko | fiat-java/src/FiatP224.java | 0m09.45s | 244680 ko || -0m00.50s || -12 ko | -5.29% | -0.00% 0m08.88s | 194884 ko | fiat-json/src/p384_64.json | 0m09.21s | 174104 ko || -0m00.33s || 20780 ko | -3.58% | +11.93% 0m08.85s | 274884 ko | fiat-rust/src/p224_32.rs | 0m08.84s | 269904 ko || +0m00.00s || 4980 ko | +0.11% | +1.84% 0m08.77s | 221004 ko | fiat-c/src/p224_32.c | 0m09.15s | 240672 ko || -0m00.38s || -19668 ko | -4.15% | -8.17% 0m08.45s | 1042428 ko | PushButtonSynthesis/Primitives.vo | 0m08.48s | 1043676 ko || -0m00.03s || -1248 ko | -0.35% | -0.11% 0m08.35s | 124484 ko | fiat-json/src/p448_solinas_32.json | 0m08.62s | 117952 ko || -0m00.26s || 6532 ko | -3.13% | +5.53% 0m08.15s | 1001028 ko | PushButtonSynthesis/SmallExamples.vo | 0m08.22s | 1000832 ko || -0m00.07s || 196 ko | -0.85% | +0.01% 0m08.11s | 59512 ko | fiat-zig/src/p448_solinas_32.zig | 0m07.90s | 57868 ko || +0m00.20s || 1644 ko | +2.65% | +2.84% 0m07.95s | 57108 ko | fiat-c/src/p448_solinas_32.c | 0m08.13s | 58904 ko || -0m00.18s || -1796 ko | -2.21% | -3.04% 0m07.89s | 58248 ko | fiat-rust/src/p448_solinas_32.rs | 0m08.17s | 59288 ko || -0m00.28s || -1040 ko | -3.42% | -1.75% 0m07.55s | 912244 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m07.51s | 911348 ko || +0m00.04s || 896 ko | +0.53% | +0.09% 0m07.17s | 1033452 ko | PushButtonSynthesis/SolinasReduction.vo | 0m07.22s | 1033556 ko || -0m00.04s || -104 ko | -0.69% | -0.01% 0m06.46s | 1041532 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.43s | 1042724 ko || +0m00.03s || -1192 ko | +0.46% | -0.11% 0m06.28s | 1121372 ko | CLI.vo | 0m06.27s | 1121452 ko || +0m00.01s || -80 ko | +0.15% | -0.00% 0m06.20s | 50120 ko | fiat-go/64/p521/p521.go | 0m06.31s | 49576 ko || -0m00.10s || 544 ko | -1.74% | +1.09% 0m06.07s | 1131040 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.03s | 1131092 ko || +0m00.04s || -52 ko | +0.66% | -0.00% 0m05.91s | 906776 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m05.90s | 905968 ko || +0m00.00s || 808 ko | +0.16% | +0.08% 0m05.66s | 66172 ko | fiat-bedrock2/src/p521_64.c | 0m05.56s | 63552 ko || +0m00.10s || 2620 ko | +1.79% | +4.12% 0m05.45s | 36044 ko | fiat-c/src/p521_64.c | 0m05.36s | 36052 ko || +0m00.08s || -8 ko | +1.67% | -0.02% 0m05.45s | 35768 ko | fiat-zig/src/p521_64.zig | 0m05.45s | 35820 ko || +0m00.00s || -52 ko | +0.00% | -0.14% 0m05.44s | 50680 ko | fiat-json/src/p521_64.json | 0m05.49s | 50400 ko || -0m00.04s || 280 ko | -0.91% | +0.55% 0m05.41s | 36092 ko | fiat-rust/src/p521_64.rs | 0m05.49s | 36672 ko || -0m00.08s || -580 ko | -1.45% | -1.58% 0m05.31s | 616344 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.26s | 619692 ko || +0m00.04s || -3348 ko | +0.95% | -0.54% 0m04.69s | 1030320 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.56s | 1030476 ko || +0m00.13s || -156 ko | +2.85% | -0.01% 0m04.50s | 1065264 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.52s | 1065392 ko || -0m00.01s || -128 ko | -0.44% | -0.01% 0m04.40s | 1038916 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.39s | 1038120 ko || +0m00.01s || 796 ko | +0.22% | +0.07% 0m04.27s | 525664 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m04.20s | 526132 ko || +0m00.06s || -468 ko | +1.66% | -0.08% 0m04.02s | 955384 ko | Assembly/Equivalence.vo | 0m04.01s | 958996 ko || +0m00.00s || -3612 ko | +0.24% | -0.37% 0m03.93s | 1050124 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.99s | 1050092 ko || -0m00.06s || 32 ko | -1.50% | +0.00% 0m03.88s | 1502888 ko | Bedrock/Everything.vo | 0m04.05s | 1502796 ko || -0m00.16s || 92 ko | -4.19% | +0.00% 0m03.52s | 1365580 ko | Everything.vo | 0m03.57s | 1365508 ko || -0m00.04s || 72 ko | -1.40% | +0.00% 0m03.40s | 667052 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m03.41s | 668512 ko || -0m00.01s || -1460 ko | -0.29% | -0.21% 0m03.09s | 1072420 ko | Rewriter/PerfTesting/Core.vo | 0m03.11s | 1072220 ko || -0m00.02s || 200 ko | -0.64% | +0.01% 0m03.05s | 1006368 ko | Bedrock/Field/Translation/Cmd.vo | 0m03.04s | 1007684 ko || +0m00.00s || -1316 ko | +0.32% | -0.13% 0m03.04s | 614916 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.07s | 613648 ko || -0m00.02s || 1268 ko | -0.97% | +0.20% 0m02.99s | 1348660 ko | PerfTesting/PerfTestPrint.vo | 0m02.98s | 1346496 ko || +0m00.01s || 2164 ko | +0.33% | +0.16% 0m02.89s | 1068352 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.86s | 1068140 ko || +0m00.03s || 212 ko | +1.04% | +0.01% 0m02.83s | 86440 ko | fiat-bedrock2/src/secp256k1_montgomery_scalar_64.c | 0m02.78s | 92448 ko || +0m00.05s || -6008 ko | +1.79% | -6.49% 0m02.82s | 83512 ko | fiat-bedrock2/src/p256_scalar_64.c | 0m02.82s | 83824 ko || +0m00.00s || -312 ko | +0.00% | -0.37% 0m02.81s | 1004916 ko | Bedrock/Field/Translation/Func.vo | 0m02.82s | 1004904 ko || -0m00.00s || 12 ko | -0.35% | +0.00% 0m02.79s | 73300 ko | fiat-json/src/p256_scalar_64.json | 0m02.77s | 72208 ko || +0m00.02s || 1092 ko | +0.72% | +1.51% 0m02.78s | 74696 ko | fiat-json/src/secp256k1_montgomery_scalar_64.json | 0m02.76s | 70564 ko || +0m00.02s || 4132 ko | +0.72% | +5.85% 0m02.76s | 1061320 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.69s | 1061296 ko || +0m00.06s || 24 ko | +2.60% | +0.00% 0m02.76s | 61376 ko | fiat-zig/src/p256_scalar_64.zig | 0m02.74s | 61368 ko || +0m00.01s || 8 ko | +0.72% | +0.01% 0m02.73s | 59516 ko | fiat-c/src/secp256k1_montgomery_scalar_64.c | 0m02.70s | 60860 ko || +0m00.02s || -1344 ko | +1.11% | -2.20% 0m02.73s | 62232 ko | fiat-go/64/secp256k1montgomeryscalar/secp256k1montgomeryscalar.go | 0m02.78s | 62084 ko || -0m00.04s || 148 ko | -1.79% | +0.23% 0m02.73s | 57104 ko | fiat-zig/src/secp256k1_montgomery_scalar_64.zig | 0m02.70s | 58912 ko || +0m00.02s || -1808 ko | +1.11% | -3.06% 0m02.71s | 64476 ko | fiat-go/64/p256scalar/p256scalar.go | 0m02.78s | 71348 ko || -0m00.06s || -6872 ko | -2.51% | -9.63% 0m02.70s | 1103800 ko | StandaloneOCamlMain.vo | 0m02.74s | 1103804 ko || -0m00.04s || -4 ko | -1.45% | -0.00% 0m02.69s | 1145340 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.71s | 1145380 ko || -0m00.02s || -40 ko | -0.73% | -0.00% 0m02.69s | 1103604 ko | StandaloneHaskellMain.vo | 0m02.69s | 1103632 ko || +0m00.00s || -28 ko | +0.00% | -0.00% 0m02.69s | 61060 ko | fiat-c/src/p256_scalar_64.c | 0m02.69s | 61428 ko || +0m00.00s || -368 ko | +0.00% | -0.59% 0m02.69s | 60672 ko | fiat-rust/src/secp256k1_montgomery_scalar_64.rs | 0m02.76s | 60612 ko || -0m00.06s || 60 ko | -2.53% | +0.09% 0m02.66s | 58680 ko | fiat-rust/src/p256_scalar_64.rs | 0m02.75s | 58604 ko || -0m00.08s || 76 ko | -3.27% | +0.12% 0m02.65s | 1045356 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.58s | 1044768 ko || +0m00.06s || 588 ko | +2.71% | +0.05% 0m02.65s | 1131240 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.64s | 1131204 ko || +0m00.00s || 36 ko | +0.37% | +0.00% 0m02.64s | 621660 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.59s | 621772 ko || +0m00.05s || -112 ko | +1.93% | -0.01% 0m02.64s | 1066352 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.65s | 1066344 ko || -0m00.00s || 8 ko | -0.37% | +0.00% 0m02.64s | 1145296 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.58s | 1145232 ko || +0m00.06s || 64 ko | +2.32% | +0.00% 0m02.58s | 81752 ko | fiat-bedrock2/src/secp256k1_montgomery_64.c | 0m02.51s | 88460 ko || +0m00.07s || -6708 ko | +2.78% | -7.58% 0m02.58s | 50260 ko | fiat-go/64/p448solinas/p448solinas.go | 0m02.66s | 50540 ko || -0m00.08s || -280 ko | -3.00% | -0.55% 0m02.54s | 1046728 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.57s | 1045428 ko || -0m00.02s || 1300 ko | -1.16% | +0.12% 0m02.53s | 1044668 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.53s | 1044656 ko || +0m00.00s || 12 ko | +0.00% | +0.00% 0m02.53s | 75236 ko | fiat-json/src/secp256k1_montgomery_64.json | 0m02.52s | 75144 ko || +0m00.00s || 92 ko | +0.39% | +0.12% 0m02.47s | 57796 ko | fiat-zig/src/secp256k1_montgomery_64.zig | 0m02.46s | 58824 ko || +0m00.01s || -1028 ko | +0.40% | -1.74% 0m02.46s | 1042628 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.46s | 1041412 ko || +0m00.00s || 1216 ko | +0.00% | +0.11% 0m02.46s | 69376 ko | fiat-go/64/secp256k1montgomery/secp256k1montgomery.go | 0m02.45s | 69576 ko || +0m00.00s || -200 ko | +0.40% | -0.28% 0m02.42s | 60312 ko | fiat-c/src/secp256k1_montgomery_64.c | 0m02.45s | 59556 ko || -0m00.03s || 756 ko | -1.22% | +1.26% 0m02.40s | 78108 ko | fiat-bedrock2/src/curve25519_scalar_64.c | 0m02.39s | 76948 ko || +0m00.00s || 1160 ko | +0.41% | +1.50% 0m02.37s | 64204 ko | fiat-rust/src/secp256k1_montgomery_64.rs | 0m02.45s | 63840 ko || -0m00.08s || 364 ko | -3.26% | +0.57% 0m02.35s | 67972 ko | fiat-json/src/curve25519_scalar_64.json | 0m02.44s | 67576 ko || -0m00.08s || 396 ko | -3.68% | +0.58% 0m02.32s | 55900 ko | fiat-zig/src/curve25519_scalar_64.zig | 0m02.32s | 55884 ko || +0m00.00s || 16 ko | +0.00% | +0.02% 0m02.28s | 67752 ko | fiat-go/64/curve25519scalar/curve25519scalar.go | 0m02.33s | 67920 ko || -0m00.05s || -168 ko | -2.14% | -0.24% 0m02.22s | 62560 ko | fiat-c/src/curve25519_scalar_64.c | 0m02.27s | 60776 ko || -0m00.04s || 1784 ko | -2.20% | +2.93% 0m02.21s | 64476 ko | fiat-rust/src/curve25519_scalar_64.rs | 0m02.23s | 64472 ko || -0m00.02s || 4 ko | -0.89% | +0.00% 0m02.11s | 35492 ko | fiat-go/32/curve25519/curve25519.go | 0m02.14s | 37076 ko || -0m00.03s || -1584 ko | -1.40% | -4.27% 0m02.09s | 67444 ko | fiat-bedrock2/src/p448_solinas_64.c | 0m02.09s | 66572 ko || +0m00.00s || 872 ko | +0.00% | +1.30% 0m02.05s | 616152 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.00s | 615540 ko || +0m00.04s || 612 ko | +2.49% | +0.09% 0m02.01s | 51624 ko | fiat-json/src/p448_solinas_64.json | 0m02.05s | 51400 ko || -0m00.04s || 224 ko | -1.95% | +0.43% 0m01.99s | 65960 ko | fiat-bedrock2/src/curve25519_32.c | 0m02.00s | 64112 ko || -0m00.01s || 1848 ko | -0.50% | +2.88% 0m01.98s | 34908 ko | fiat-zig/src/p448_solinas_64.zig | 0m01.98s | 35076 ko || +0m00.00s || -168 ko | +0.00% | -0.47% 0m01.97s | 544384 ko | Stringification/Language.vo | 0m01.85s | 545284 ko || +0m00.11s || -900 ko | +6.48% | -0.16% 0m01.94s | 80484 ko | fiat-bedrock2/src/p224_64.c | 0m01.92s | 80632 ko || +0m00.02s || -148 ko | +1.04% | -0.18% 0m01.93s | 36480 ko | fiat-c/src/p448_solinas_64.c | 0m01.97s | 35164 ko || -0m00.04s || 1316 ko | -2.03% | +3.74% 0m01.91s | 68372 ko | fiat-json/src/p224_64.json | 0m01.88s | 68740 ko || +0m00.03s || -368 ko | +1.59% | -0.53% 0m01.90s | 34104 ko | fiat-rust/src/p448_solinas_64.rs | 0m01.97s | 34452 ko || -0m00.07s || -348 ko | -3.55% | -1.01% 0m01.89s | 76504 ko | fiat-bedrock2/src/p256_64.c | 0m01.84s | 76436 ko || +0m00.04s || 68 ko | +2.71% | +0.08% 0m01.85s | 636172 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.83s | 636080 ko || +0m00.02s || 92 ko | +1.09% | +0.01% 0m01.85s | 62188 ko | fiat-go/64/p224/p224.go | 0m01.91s | 62196 ko || -0m00.05s || -8 ko | -3.14% | -0.01% 0m01.84s | 64332 ko | fiat-zig/src/p224_64.zig | 0m01.86s | 62296 ko || -0m00.02s || 2036 ko | -1.07% | +3.26% 0m01.83s | 67704 ko | fiat-json/src/p256_64.json | 0m01.90s | 67196 ko || -0m00.06s || 508 ko | -3.68% | +0.75% 0m01.82s | 57896 ko | fiat-zig/src/p256_64.zig | 0m01.83s | 58884 ko || -0m00.01s || -988 ko | -0.54% | -1.67% 0m01.81s | 68648 ko | fiat-go/64/p256/p256.go | 0m01.85s | 68732 ko || -0m00.04s || -84 ko | -2.16% | -0.12% 0m01.81s | 48104 ko | fiat-json/src/curve25519_32.json | 0m01.89s | 51216 ko || -0m00.07s || -3112 ko | -4.23% | -6.07% 0m01.81s | 61896 ko | fiat-rust/src/p224_64.rs | 0m01.84s | 61188 ko || -0m00.03s || 708 ko | -1.63% | +1.15% 0m01.80s | 34044 ko | fiat-java/src/FiatCurve25519.java | 0m01.85s | 34004 ko || -0m00.05s || 40 ko | -2.70% | +0.11% 0m01.78s | 33848 ko | fiat-c/src/curve25519_32.c | 0m01.80s | 33848 ko || -0m00.02s || 0 ko | -1.11% | +0.00% 0m01.78s | 62420 ko | fiat-c/src/p224_64.c | 0m01.78s | 56260 ko || +0m00.00s || 6160 ko | +0.00% | +10.94% 0m01.78s | 33040 ko | fiat-zig/src/curve25519_32.zig | 0m01.79s | 33284 ko || -0m00.01s || -244 ko | -0.55% | -0.73% 0m01.77s | 59716 ko | fiat-rust/src/p256_64.rs | 0m01.80s | 59012 ko || -0m00.03s || 704 ko | -1.66% | +1.19% 0m01.76s | 61788 ko | fiat-c/src/p256_64.c | 0m01.76s | 61780 ko || +0m00.00s || 8 ko | +0.00% | +0.01% 0m01.75s | 33880 ko | fiat-rust/src/curve25519_32.rs | 0m01.79s | 34012 ko || -0m00.04s || -132 ko | -2.23% | -0.38% 0m01.56s | 606924 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.60s | 607788 ko || -0m00.04s || -864 ko | -2.50% | -0.14% 0m01.51s | 590192 ko | CompilersTestCases.vo | 0m01.50s | 590212 ko || +0m00.01s || -20 ko | +0.66% | -0.00% 0m01.44s | 51944 ko | fiat-bedrock2/src/secp256k1_dettman_32.c | 0m01.45s | 51804 ko || -0m00.01s || 140 ko | -0.68% | +0.27% 0m01.43s | 511832 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m01.49s | 511940 ko || -0m00.06s || -108 ko | -4.02% | -0.02% 0m01.39s | 522448 ko | AbstractInterpretation/ZRange.vo | 0m01.41s | 522640 ko || -0m00.02s || -192 ko | -1.41% | -0.03% 0m01.38s | 543168 ko | Stringification/Go.vo | 0m01.36s | 541976 ko || +0m00.01s || 1192 ko | +1.47% | +0.21% 0m01.27s | 41988 ko | fiat-json/src/secp256k1_dettman_32.json | 0m01.27s | 41052 ko || +0m00.00s || 936 ko | +0.00% | +2.28% 0m01.24s | 26744 ko | fiat-java/src/FiatSecp256K1Dettman.java | 0m01.23s | 26564 ko || +0m00.01s || 180 ko | +0.81% | +0.67% 0m01.23s | 25760 ko | fiat-zig/src/secp256k1_dettman_32.zig | 0m01.22s | 25624 ko || +0m00.01s || 136 ko | +0.81% | +0.53% 0m01.20s | 25752 ko | fiat-go/32/secp256k1dettman/secp256k1dettman.go | 0m01.23s | 25676 ko || -0m00.03s || 76 ko | -2.43% | +0.29% 0m01.20s | 25744 ko | fiat-rust/src/secp256k1_dettman_32.rs | 0m01.22s | 25596 ko || -0m00.02s || 148 ko | -1.63% | +0.57% 0m01.19s | 25720 ko | fiat-c/src/secp256k1_dettman_32.c | 0m01.21s | 25612 ko || -0m00.02s || 108 ko | -1.65% | +0.42% 0m01.15s | 628108 ko | Bedrock/Specs/Field.vo | 0m01.25s | 627916 ko || -0m00.10s || 192 ko | -8.00% | +0.03% 0m01.06s | 609396 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.06s | 608640 ko || +0m00.00s || 756 ko | +0.00% | +0.12% 0m01.02s | 601076 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.04s | 601192 ko || -0m00.02s || -116 ko | -1.92% | -0.01% 0m00.94s | 539300 ko | Stringification/C.vo | 0m00.94s | 539324 ko || +0m00.00s || -24 ko | +0.00% | -0.00% 0m00.92s | 537052 ko | Stringification/JSON.vo | 0m00.89s | 537668 ko || +0m00.03s || -616 ko | +3.37% | -0.11% 0m00.87s | 614388 ko | Bedrock/Field/Interface/Representation.vo | 0m00.86s | 615708 ko || +0m00.01s || -1320 ko | +1.16% | -0.21% 0m00.85s | 617724 ko | Bedrock/Group/Point.vo | 0m00.88s | 617624 ko || -0m00.03s || 100 ko | -3.40% | +0.01% 0m00.84s | 535920 ko | Stringification/Zig.vo | 0m00.82s | 541188 ko || +0m00.02s || -5268 ko | +2.43% | -0.97% 0m00.83s | 535816 ko | Stringification/Java.vo | 0m00.81s | 535704 ko || +0m00.01s || 112 ko | +2.46% | +0.02% 0m00.81s | 535004 ko | Stringification/Rust.vo | 0m00.81s | 535796 ko || +0m00.00s || -792 ko | +0.00% | -0.14% 0m00.77s | 587864 ko | Bedrock/Field/Common/Tactics.vo | 0m00.75s | 587696 ko || +0m00.02s || 168 ko | +2.66% | +0.02% 0m00.73s | 546720 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.71s | 546700 ko || +0m00.02s || 20 ko | +2.81% | +0.00% 0m00.67s | 521656 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.72s | 521652 ko || -0m00.04s || 4 ko | -6.94% | +0.00% 0m00.67s | 541484 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.68s | 541716 ko || -0m00.01s || -232 ko | -1.47% | -0.04% 0m00.64s | 516760 ko | AbstractInterpretation/WfExtra.vo | 0m00.67s | 515528 ko || -0m00.03s || 1232 ko | -4.47% | +0.23% 0m00.62s | 32864 ko | fiat-go/64/curve25519/curve25519.go | 0m00.63s | 32848 ko || -0m00.01s || 16 ko | -1.58% | +0.04% 0m00.54s | 120072 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi | 0m00.52s | 119948 ko || +0m00.02s || 124 ko | +3.84% | +0.10% 0m00.53s | 120544 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi | 0m00.53s | 123744 ko || +0m00.00s || -3200 ko | +0.00% | -2.58% 0m00.52s | 120996 ko | ExtractionOCaml/bedrock2_base_conversion.cmi | 0m00.51s | 120016 ko || +0m00.01s || 980 ko | +1.96% | +0.81% 0m00.52s | 123028 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi | 0m00.52s | 122568 ko || +0m00.00s || 460 ko | +0.00% | +0.37% 0m00.52s | 120064 ko | ExtractionOCaml/dettman_multiplication.cmi | 0m00.51s | 119968 ko || +0m00.01s || 96 ko | +1.96% | +0.08% 0m00.52s | 119192 ko | ExtractionOCaml/saturated_solinas.cmi | 0m00.49s | 117920 ko || +0m00.03s || 1272 ko | +6.12% | +1.07% 0m00.52s | 119152 ko | ExtractionOCaml/unsaturated_solinas.cmi | 0m00.51s | 119976 ko || +0m00.01s || -824 ko | +1.96% | -0.68% 0m00.52s | 38008 ko | fiat-bedrock2/src/curve25519_64.c | 0m00.52s | 38160 ko || +0m00.00s || -152 ko | +0.00% | -0.39% 0m00.51s | 119300 ko | ExtractionOCaml/base_conversion.cmi | 0m00.49s | 119472 ko || +0m00.02s || -172 ko | +4.08% | -0.14% 0m00.51s | 120180 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi | 0m00.53s | 122568 ko || -0m00.02s || -2388 ko | -3.77% | -1.94% 0m00.51s | 121068 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi | 0m00.52s | 119812 ko || -0m00.01s || 1256 ko | -1.92% | +1.04% 0m00.51s | 120416 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi | 0m00.52s | 121088 ko || -0m00.01s || -672 ko | -1.92% | -0.55% 0m00.51s | 120260 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi | 0m00.50s | 120972 ko || +0m00.01s || -712 ko | +2.00% | -0.58% 0m00.51s | 120244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi | 0m00.51s | 122452 ko || +0m00.00s || -2208 ko | +0.00% | -1.80% 0m00.51s | 123296 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi | 0m00.51s | 121612 ko || +0m00.00s || 1684 ko | +0.00% | +1.38% 0m00.51s | 118932 ko | ExtractionOCaml/word_by_word_montgomery.cmi | 0m00.51s | 118492 ko || +0m00.00s || 440 ko | +0.00% | +0.37% 0m00.51s | 32760 ko | fiat-json/src/curve25519_64.json | 0m00.50s | 33336 ko || +0m00.01s || -576 ko | +2.00% | -1.72% 0m00.50s | 120092 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi | 0m00.51s | 120440 ko || -0m00.01s || -348 ko | -1.96% | -0.28% 0m00.50s | 120028 ko | ExtractionOCaml/solinas_reduction.cmi | 0m00.50s | 119036 ko || +0m00.00s || 992 ko | +0.00% | +0.83% 0m00.49s | 120812 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi | 0m00.51s | 123016 ko || -0m00.02s || -2204 ko | -3.92% | -1.79% 0m00.49s | 26340 ko | fiat-zig/src/curve25519_64.zig | 0m00.48s | 26368 ko || +0m00.01s || -28 ko | +2.08% | -0.10% 0m00.46s | 27368 ko | fiat-c/src/curve25519_64.c | 0m00.46s | 27064 ko || +0m00.00s || 304 ko | +0.00% | +1.12% 0m00.46s | 26276 ko | fiat-rust/src/curve25519_64.rs | 0m00.46s | 25892 ko || +0m00.00s || 384 ko | +0.00% | +1.48% 0m00.43s | 40400 ko | fiat-bedrock2/src/curve25519_solinas_64.c | 0m00.42s | 40528 ko || +0m00.01s || -128 ko | +2.38% | -0.31% 0m00.42s | 37480 ko | fiat-json/src/curve25519_solinas_64.json | 0m00.44s | 37636 ko || -0m00.02s || -156 ko | -4.54% | -0.41% 0m00.41s | 36396 ko | fiat-zig/src/curve25519_solinas_64.zig | 0m00.41s | 36708 ko || +0m00.00s || -312 ko | +0.00% | -0.84% 0m00.40s | 36716 ko | fiat-c/src/curve25519_solinas_64.c | 0m00.40s | 35712 ko || +0m00.00s || 1004 ko | +0.00% | +2.81% 0m00.40s | 36604 ko | fiat-go/64/curve25519solinas/curve25519solinas.go | 0m00.40s | 36456 ko || +0m00.00s || 148 ko | +0.00% | +0.40% 0m00.39s | 36344 ko | fiat-rust/src/curve25519_solinas_64.rs | 0m00.41s | 36104 ko || -0m00.01s || 240 ko | -4.87% | +0.66% 0m00.28s | 25548 ko | fiat-go/32/poly1305/poly1305.go | 0m00.28s | 25516 ko || +0m00.00s || 32 ko | +0.00% | +0.12% 0m00.26s | 30308 ko | fiat-json/src/poly1305_32.json | 0m00.24s | 30076 ko || +0m00.02s || 232 ko | +8.33% | +0.77% 0m00.25s | 32436 ko | fiat-bedrock2/src/poly1305_32.c | 0m00.25s | 32300 ko || +0m00.00s || 136 ko | +0.00% | +0.42% 0m00.24s | 24584 ko | fiat-rust/src/poly1305_32.rs | 0m00.22s | 24716 ko || +0m00.01s || -132 ko | +9.09% | -0.53% 0m00.23s | 29680 ko | fiat-bedrock2/src/secp256k1_dettman_64.c | 0m00.23s | 29712 ko || +0m00.00s || -32 ko | +0.00% | -0.10% 0m00.23s | 24356 ko | fiat-go/64/secp256k1dettman/secp256k1dettman.go | 0m00.24s | 24104 ko || -0m00.00s || 252 ko | -4.16% | +1.04% 0m00.23s | 23996 ko | fiat-zig/src/poly1305_32.zig | 0m00.21s | 24020 ko || +0m00.02s || -24 ko | +9.52% | -0.09% 0m00.22s | 25188 ko | fiat-java/src/FiatPoly1305.java | 0m00.23s | 25100 ko || -0m00.01s || 88 ko | -4.34% | +0.35% 0m00.21s | 24128 ko | fiat-c/src/poly1305_32.c | 0m00.22s | 24272 ko || -0m00.01s || -144 ko | -4.54% | -0.59% 0m00.19s | 20896 ko | fiat-rust/src/secp256k1_dettman_64.rs | 0m00.18s | 21240 ko || +0m00.01s || -344 ko | +5.55% | -1.61% 0m00.18s | 23760 ko | fiat-json/src/secp256k1_dettman_64.json | 0m00.20s | 24196 ko || -0m00.02s || -436 ko | -10.00% | -1.80% 0m00.18s | 21172 ko | fiat-zig/src/secp256k1_dettman_64.zig | 0m00.17s | 20636 ko || +0m00.00s || 536 ko | +5.88% | +2.59% 0m00.17s | 20852 ko | fiat-c/src/secp256k1_dettman_64.c | 0m00.19s | 20816 ko || -0m00.01s || 36 ko | -10.52% | +0.17% 0m00.17s | 25992 ko | fiat-go/64/poly1305/poly1305.go | 0m00.17s | 25912 ko || +0m00.00s || 80 ko | +0.00% | +0.30% 0m00.16s | 58684 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi | 0m00.18s | 59896 ko || -0m00.01s || -1212 ko | -11.11% | -2.02% 0m00.15s | 59116 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi | 0m00.15s | 58856 ko || +0m00.00s || 260 ko | +0.00% | +0.44% 0m00.13s | 27404 ko | fiat-json/src/poly1305_64.json | 0m00.14s | 27292 ko || -0m00.01s || 112 ko | -7.14% | +0.41% 0m00.13s | 23064 ko | fiat-zig/src/poly1305_64.zig | 0m00.12s | 23072 ko || +0m00.01s || -8 ko | +8.33% | -0.03% 0m00.12s | 23284 ko | fiat-c/src/poly1305_64.c | 0m00.12s | 23028 ko || +0m00.00s || 256 ko | +0.00% | +1.11% 0m00.11s | 28008 ko | fiat-bedrock2/src/poly1305_64.c | 0m00.13s | 28304 ko || -0m00.02s || -296 ko | -15.38% | -1.04% 0m00.11s | 22892 ko | fiat-rust/src/poly1305_64.rs | 0m00.12s | 22952 ko || -0m00.00s || -60 ko | -8.33% | -0.26% ```

--- src/AbstractInterpretation/ZRange.v | 40 +++++++++++--- src/AbstractInterpretation/ZRangeProofs.v | 67 +++++++++++++++++++++++ 2 files changed, 99 insertions(+), 8 deletions(-) diff --git a/src/AbstractInterpretation/ZRange.v b/src/AbstractInterpretation/ZRange.v index 200ede3e75..7e61de8c8e 100644 --- a/src/AbstractInterpretation/ZRange.v +++ b/src/AbstractInterpretation/ZRange.v @@ -282,6 +282,29 @@ Module Compilers. Lemma interp_beq_lb {t x y} : x = y -> @interp_beq t t x y = true. Proof. apply reflect_to_beq; exact _. Qed. + Fixpoint union {t} : interp t -> interp t -> interp t + := match t return interp t -> interp t -> interp t with + | base.type.type_base base.type.Z => Option.map2 ZRange.union + | base.type.type_base _ as t + | base.type.unit as t + => fun x y + => if @interp_beq t t x y + then x + else None + | base.type.prod A B => fun '(a, b) '(a', b') => + (@union A a a', @union B b b') + | base.type.list A => fun la lb => Option.bind2 la lb (fun la lb => + if Nat.eqb (length la) (length lb) + then Datatypes.Some (List.map (uncurry (@union A)) (List.combine la lb)) + else Datatypes.None) + | base.type.option A => fun oa ob => Option.bind2 oa ob (fun l r => + match l, r return option (option (interp A)) with + | Datatypes.Some l, Datatypes.Some r => Datatypes.Some (Datatypes.Some (union l r)) + | Datatypes.None, Datatypes.None => Datatypes.Some Datatypes.None + | _, _ => Datatypes.None + end) + end. + Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool := match t with | base.type.type_base base.type.Z as t @@ -573,12 +596,6 @@ Module Compilers. | None => None end | ident.Z_eqb as idc - | ident.Z_leb as idc - | ident.Z_ltb as idc - | ident.Z_geb as idc - | ident.Z_gtb as idc - | ident.Z_max as idc - | ident.Z_min as idc | ident.Z_pow as idc | ident.Z_lxor as idc | ident.Z_modulo as idc @@ -623,13 +640,13 @@ Module Compilers. => fun t f b => match b with | Some b => if b then t tt else f tt - | None => ZRange.type.base.option.None + | None => type.base.option.union (t tt) (f tt) end | ident.bool_rect_nodep _ => fun t f b => match b with | Some b => if b then t else f - | None => ZRange.type.base.option.None + | None => type.base.option.union t f end | ident.option_rect _ _ => fun s n o @@ -737,10 +754,17 @@ Module Compilers. | ident.List_app _ => fun ls1 ls2 => ls1 <- ls1; ls2 <- ls2; Some (List.app ls1 ls2) | ident.List_rev _ => option_map (@List.rev _) + | ident.Z_leb as idc + | ident.Z_ltb as idc + | ident.Z_geb as idc + | ident.Z_gtb as idc + => fun x y => x <- x; y <- y; ZRange.ToConstant.four_corners Bool.eqb (ident.interp idc) x y | ident.Z_opp as idc | ident.Z_log2 as idc | ident.Z_log2_up as idc => fun x => x <- x; Some (ZRange.two_corners (ident.interp idc) x) + | ident.Z_max as idc + | ident.Z_min as idc | ident.Z_add as idc | ident.Z_mul as idc | ident.Z_sub as idc diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v index f09333f70a..aad9dd774c 100644 --- a/src/AbstractInterpretation/ZRangeProofs.v +++ b/src/AbstractInterpretation/ZRangeProofs.v @@ -41,6 +41,7 @@ Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.PrintGoal. +Require Import Crypto.Util.Tactics.DoWithHyp. Require Import Crypto.Language.PreExtra. Require Import Crypto.CastLemmas. Require Import Crypto.AbstractInterpretation.ZRange. @@ -58,6 +59,61 @@ Module Compilers. Module option. Lemma is_bounded_by_None t v : ZRange.type.base.option.is_bounded_by (@ZRange.type.base.option.None t) v = true. Proof. induction t; cbn; cbv [andb]; break_innermost_match; eauto. Qed. + + Lemma tighter_than_union t (rx ry : ZRange.type.base.option.interp t) : + ZRange.type.base.option.is_tighter_than rx (ZRange.type.base.option.union rx ry) = true /\ + ZRange.type.base.option.is_tighter_than ry (ZRange.type.base.option.union rx ry) = true. + Proof. + induction t; [destruct t|..]; destruct rx, ry; + cbn [ + ZRange.type.base.interp + ZRange.type.base.option.interp + ZRange.type.base.option.is_tighter_than + ZRange.type.base.is_tighter_than + ZRange.type.base.option.union + Option.map2 + Option.bind2 + ] in *; auto 2. + all: fold (@ZRange.type.base.option.interp) in *. + all: break_innermost_match; reflect_hyps; inversion_option; subst; auto 2. + all: split_and. + all: cbn [option_beq]. + all: rewrite ?Bool.andb_true_iff; auto. + all: try now split; first [ apply ZRange.is_tighter_than_bool_union_l | apply ZRange.is_tighter_than_bool_union_r ]. + all: do 2 try (match goal with + | [ |- context[?x = true] ] + => lazymatch x with true => fail | false => fail | _ => idtac end; + destruct x eqn:?; progress reflect_hyps + end; + cbn [ZRange.type.base.option.None] in *; + auto 2; subst; try congruence). + { rewrite 2 fold_andb_map_map. + rewrite 2 fold_andb_map_iff. + rewrite List.combine_length. + do_with_hyp' ltac:(fun H => rewrite H). + rewrite Nat.min_id. + repeat split; intros *; destruct_head'_prod; cbn [uncurry fst snd]. + all: rewrite In_nth_error_iff. + all: intros [n H']; revert H'. + all: rewrite !nth_error_combine. + all: break_innermost_match; intros; inversion_option; inversion_pair; subst; auto. } + Qed. + + Lemma is_bounded_by_union_l t (rx ry : ZRange.type.base.option.interp t) x : + ZRange.type.base.option.is_bounded_by rx x = true -> + ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) x = true. + Proof. + eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption; + eapply tighter_than_union. + Qed. + + Lemma is_bounded_by_union_r t (rx ry : ZRange.type.base.option.interp t) y : + ZRange.type.base.option.is_bounded_by ry y = true -> + ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union rx ry) y = true. + Proof. + eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; try eassumption; + eapply tighter_than_union. + Qed. End option. End base. @@ -484,6 +540,16 @@ Module Compilers. | [ H : (forall a b, ?R0 a b = true -> forall c d, ?R1 c d = true -> forall e f, (forall g h, ?R3 g h = true -> ?R4 (e g) (f h) = true) -> forall i j, ?R5 i j = true -> ?R6 (?F _ _ _ _) (?G _ _ _ _) = true) |- ?R6 (?F _ _ _ _) (?G _ _ _ _) = true ] => apply H; clear H + end + | match goal with + | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ true) = true ] + => apply ZRange.type.base.option.is_bounded_by_union_l + | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.Thunked.bool_rect _ _ _ false) = true ] + => apply ZRange.type.base.option.is_bounded_by_union_r + | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ true) = true ] + => apply ZRange.type.base.option.is_bounded_by_union_l + | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ false) = true ] + => apply ZRange.type.base.option.is_bounded_by_union_r end ]. Local Lemma mul_by_halves_bounds x y n : @@ -751,6 +817,7 @@ Module Compilers. end | intros; mul_by_halves_t ]. all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ]. + all: try solve [ cbv [ZRange.ToConstant.four_corners ZRange.ToConstant.Option.four_corners ZRange.ToConstant.Option.apply_to_range ZRange.ToConstant.Option.two_corners ZRange.ToConstant.Option.union option_beq Bool.eqb] in *; non_arith_t; Z.ltb_to_lt; lia ]. (** For command-line debugging, we display goals that should not remain *) all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ]. Qed.