From d839f890b8ac43341bef44d57e8b3a56f861cd77 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 7 Dec 2023 12:28:12 -0800 Subject: [PATCH] Add more identifiers for saturated solinas (#1773) For https://github.com/mit-plv/fiat-crypto/pull/1609 Slow identifiers are commented out. I'll have to figure out a different way to prove the ZRange bounds proof that isn't so slow. Co-authored-by: Andres Erbsen
Timing Diff

``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 65m48.78s | 2852620 ko | Total Time / Peak Mem | 67m03.79s | 2852280 ko || -1m15.01s || 340 ko | -1.86% | +0.01% -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 8m28.52s | 2657300 ko | Bedrock/End2End/X25519/GarageDoor.vo | 8m49.71s | 2656156 ko || -0m21.19s || 1144 ko | -4.00% | +0.04% 2m27.88s | 1666316 ko | Rewriter/Passes/NBE.vo | 2m15.45s | 1554568 ko || +0m12.43s || 111748 ko | +9.17% | +7.18% 1m42.99s | 1885360 ko | Bedrock/End2End/X25519/AddPrecomputed.vo | 1m55.09s | 1888072 ko || -0m12.09s || -2712 ko | -10.51% | -0.14% 3m02.83s | 2603460 ko | Bedrock/End2End/RupicolaCrypto/ChaCha20.vo | 3m13.15s | 2603344 ko || -0m10.31s || 116 ko | -5.34% | +0.00% 5m25.01s | 2852620 ko | Bedrock/Field/Synthesis/Examples/p224_64_new.vo | 5m33.56s | 2852280 ko || -0m08.55s || 340 ko | -2.56% | +0.01% 0m11.49s | 542800 ko | AbstractInterpretation/ZRangeCommonProofs.vo | 0m04.40s | 537448 ko || +0m07.08s || 5352 ko | +161.13% | +0.99% 3m31.55s | 1773972 ko | Rewriter/Passes/ArithWithCasts.vo | 3m36.07s | 1682328 ko || -0m04.51s || 91644 ko | -2.09% | +5.44% 0m48.69s | 1127200 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Expr.vo | 0m44.14s | 1100028 ko || +0m04.54s || 27172 ko | +10.30% | +2.47% 1m50.06s | 1603060 ko | Bedrock/End2End/X25519/Field25519.vo | 1m53.33s | 1600868 ko || -0m03.26s || 2192 ko | -2.88% | +0.13% 0m36.82s | 712856 ko | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m40.41s | 710156 ko || -0m03.58s || 2700 ko | -8.88% | +0.38% 2m26.61s | 1119660 ko | Fancy/Compiler.vo | 2m29.14s | 1127580 ko || -0m02.52s || -7920 ko | -1.69% | -0.70% 1m47.35s | 1418720 ko | Rewriter/Passes/ToFancyWithCasts.vo | 1m49.39s | 1437288 ko || -0m02.04s || -18568 ko | -1.86% | -1.29% 1m46.98s | 2428052 ko | Fancy/Barrett256.vo | 1m49.19s | 2411004 ko || -0m02.21s || 17048 ko | -2.02% | +0.70% 1m22.34s | 945488 ko | AbstractInterpretation/Fancy/Wf.vo | 1m24.45s | 901548 ko || -0m02.10s || 43940 ko | -2.49% | +4.87% 0m29.23s | 1554548 ko | StandaloneDebuggingExamples.vo | 0m31.54s | 1544348 ko || -0m02.30s || 10200 ko | -7.32% | +0.66% 0m59.32s | 876092 ko | AbstractInterpretation/Bottomify/Wf.vo | 1m00.44s | 882844 ko || -0m01.11s || -6752 ko | -1.85% | -0.76% 0m58.11s | 710572 ko | Rewriter/RulesProofs.vo | 0m59.51s | 710680 ko || -0m01.39s || -108 ko | -2.35% | -0.01% 0m46.54s | 773492 ko | AbstractInterpretation/Fancy/Proofs.vo | 0m47.54s | 771488 ko || -0m01.00s || 2004 ko | -2.10% | +0.25% 0m39.38s | 1072512 ko | Rewriter/Passes/Arith.vo | 0m40.40s | 1087364 ko || -0m01.01s || -14852 ko | -2.52% | -1.36% 0m37.80s | 1016072 ko | Bedrock/Group/ScalarMult/MontgomeryLadder.vo | 0m39.02s | 1016376 ko || -0m01.22s || -304 ko | -3.12% | -0.02% 0m33.76s | 1284448 ko | Bedrock/End2End/X25519/MontgomeryLadder.vo | 0m35.26s | 1286640 ko || -0m01.50s || -2192 ko | -4.25% | -0.17% 0m21.18s | 1357384 ko | Bedrock/End2End/RupicolaCrypto/Low.vo | 0m22.28s | 1355956 ko || -0m01.10s || 1428 ko | -4.93% | +0.10% 0m17.74s | 1142436 ko | Bedrock/Field/Translation/Proofs/Func.vo | 0m19.06s | 1133464 ko || -0m01.32s || 8972 ko | -6.92% | +0.79% 0m17.34s | 1379920 ko | PerfTesting/PerfTestSearchPattern.vo | 0m18.52s | 1378460 ko || -0m01.17s || 1460 ko | -6.37% | +0.10% 0m16.93s | 792296 ko | Language/IdentifiersGENERATED.vo | 0m15.81s | 765508 ko || +0m01.11s || 26788 ko | +7.08% | +3.49% 3m55.44s | 2545572 ko | Assembly/WithBedrock/Proofs.vo | 3m54.51s | 2541224 ko || +0m00.93s || 4348 ko | +0.39% | +0.17% 1m27.57s | 2144112 ko | SlowPrimeSynthesisExamples.vo | 1m26.76s | 2088940 ko || +0m00.80s || 55172 ko | +0.93% | +2.64% 1m15.72s | 1526800 ko | Assembly/EquivalenceProofs.vo | 1m16.33s | 1522940 ko || -0m00.60s || 3860 ko | -0.79% | +0.25% 1m15.72s | 990208 ko | PushButtonSynthesis/SolinasReductionReificationCache.vo | 1m16.02s | 1010076 ko || -0m00.29s || -19868 ko | -0.39% | -1.96% 1m06.04s | 1437348 ko | Assembly/WithBedrock/SymbolicProofs.vo | 1m06.56s | 1433052 ko || -0m00.51s || 4296 ko | -0.78% | +0.29% 0m55.24s | 866644 ko | AbstractInterpretation/ZRangeProofs.vo | 0m54.79s | 864800 ko || +0m00.45s || 1844 ko | +0.82% | +0.21% 0m50.66s | 836408 ko | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 0m51.33s | 831040 ko || -0m00.67s || 5368 ko | -1.30% | +0.64% 0m49.88s | 1029676 ko | Rewriter/Passes/MultiRetSplit.vo | 0m49.97s | 1027180 ko || -0m00.08s || 2496 ko | -0.18% | +0.24% 0m46.64s | 1780880 ko | Fancy/Montgomery256.vo | 0m47.17s | 1839968 ko || -0m00.53s || -59088 ko | -1.12% | -3.21% 0m45.28s | 1517332 ko | Assembly/Symbolic.vo | 0m45.54s | 1519112 ko || -0m00.25s || -1780 ko | -0.57% | -0.11% 0m38.05s | 1327100 ko | Bedrock/End2End/X25519/GarageDoorTop.vo | 0m38.96s | 1322972 ko || -0m00.91s || 4128 ko | -2.33% | +0.31% 0m32.34s | 913332 ko | Rewriter/Passes/MulSplit.vo | 0m32.16s | 879740 ko || +0m00.18s || 33592 ko | +0.55% | +3.81% 0m28.26s | 702272 ko | AbstractInterpretation/Bottomify/Proofs.vo | 0m28.53s | 707212 ko || -0m00.26s || -4940 ko | -0.94% | -0.69% 0m25.06s | 1380588 ko | PerfTesting/PerfTestSearch.vo | 0m26.01s | 1380864 ko || -0m00.95s || -276 ko | -3.65% | -0.01% 0m22.67s | 1186572 ko | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m22.89s | 1182588 ko || -0m00.21s || 3984 ko | -0.96% | +0.33% 0m19.99s | 813092 ko | Bedrock/Field/Translation/Proofs/Expr.vo | 0m19.87s | 794980 ko || +0m00.11s || 18112 ko | +0.60% | +2.27% 0m19.55s | 1168644 ko | PushButtonSynthesis/WordByWordMontgomery.vo | 0m19.73s | 1164252 ko || -0m00.17s || 4392 ko | -0.91% | +0.37% 0m18.91s | 748880 ko | Bedrock/Field/Translation/Proofs/LoadStoreList.vo | 0m19.52s | 739932 ko || -0m00.60s || 8948 ko | -3.12% | +1.20% 0m16.82s | 1222464 ko | Bedrock/Field/Synthesis/New/Signature.vo | 0m17.65s | 1218392 ko || -0m00.82s || 4072 ko | -4.70% | +0.33% 0m16.73s | 1137776 ko | Bedrock/End2End/Poly1305/Field1305.vo | 0m17.62s | 1133672 ko || -0m00.89s || 4104 ko | -5.05% | +0.36% 0m16.26s | 1161904 ko | Bedrock/Field/Translation/Proofs/Cmd.vo | 0m16.39s | 1153720 ko || -0m00.12s || 8184 ko | -0.79% | +0.70% 0m14.51s | 603548 ko | Language/IdentifiersGENERATEDProofs.vo | 0m13.92s | 598200 ko || +0m00.58s || 5348 ko | +4.23% | +0.89% 0m13.35s | 604016 ko | Bedrock/Field/Common/Util.vo | 0m13.39s | 603924 ko || -0m00.04s || 92 ko | -0.29% | +0.01% 0m13.05s | 682576 ko | Bedrock/Group/AdditionChains.vo | 0m13.57s | 680296 ko || -0m00.51s || 2280 ko | -3.83% | +0.33% 0m12.72s | 667548 ko | Bedrock/Group/ScalarMult/LadderStep.vo | 0m13.15s | 653356 ko || -0m00.42s || 14192 ko | -3.26% | +2.17% 0m12.63s | 576512 ko | PushButtonSynthesis/DettmanMultiplicationReificationCache.vo | 0m13.46s | 579232 ko || -0m00.83s || -2720 ko | -6.16% | -0.46% 0m11.38s | 1034268 ko | BoundsPipeline.vo | 0m11.49s | 1034352 ko || -0m00.10s || -84 ko | -0.95% | -0.00% 0m11.30s | 1705800 ko | Bedrock/Field/Synthesis/New/WordByWordMontgomery.vo | 0m11.77s | 1703840 ko || -0m00.46s || 1960 ko | -3.99% | +0.11% 0m10.29s | 602260 ko | Stringification/IR.vo | 0m09.58s | 598276 ko || +0m00.70s || 3984 ko | +7.41% | +0.66% 0m10.02s | 627072 ko | Bedrock/Field/Translation/Proofs/Flatten.vo | 0m09.47s | 625248 ko || +0m00.54s || 1824 ko | +5.80% | +0.29% 0m09.97s | 1303428 ko | Bedrock/End2End/X25519/MontgomeryLadderProperties.vo | 0m10.50s | 1301292 ko || -0m00.52s || 2136 ko | -5.04% | +0.16% 0m08.98s | 1040220 ko | PushButtonSynthesis/BaseConversion.vo | 0m09.14s | 1038228 ko || -0m00.16s || 1992 ko | -1.75% | +0.19% 0m08.89s | 664948 ko | Bedrock/Group/ScalarMult/CSwap.vo | 0m09.35s | 663156 ko || -0m00.45s || 1792 ko | -4.91% | +0.27% 0m08.80s | 610724 ko | Language/IdentifiersBasicGENERATED.vo | 0m08.35s | 600648 ko || +0m00.45s || 10076 ko | +5.38% | +1.67% 0m08.55s | 563324 ko | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m09.11s | 559056 ko || -0m00.55s || 4268 ko | -6.14% | +0.76% 0m08.19s | 583492 ko | PushButtonSynthesis/BYInversionReificationCache.vo | 0m08.78s | 586752 ko || -0m00.58s || -3260 ko | -6.71% | -0.55% 0m08.04s | 1048948 ko | PushButtonSynthesis/Primitives.vo | 0m08.03s | 1046980 ko || +0m00.00s || 1968 ko | +0.12% | +0.18% 0m07.82s | 1006888 ko | PushButtonSynthesis/SmallExamples.vo | 0m07.83s | 1005592 ko || -0m00.00s || 1296 ko | -0.12% | +0.12% 0m07.51s | 913956 ko | Bedrock/Field/Translation/Proofs/EquivalenceProperties.vo | 0m07.32s | 911976 ko || +0m00.18s || 1980 ko | +2.59% | +0.21% 0m07.40s | 585988 ko | Rewriter/Passes/RelaxBitwidthAdcSbb.vo | 0m07.36s | 587760 ko || +0m00.04s || -1772 ko | +0.54% | -0.30% 0m06.92s | 1038440 ko | PushButtonSynthesis/SolinasReduction.vo | 0m06.91s | 1038112 ko || +0m00.00s || 328 ko | +0.14% | +0.03% 0m06.20s | 1129984 ko | CLI.vo | 0m06.05s | 1130104 ko || +0m00.15s || -120 ko | +2.47% | -0.01% 0m06.13s | 1048216 ko | PushButtonSynthesis/BarrettReduction.vo | 0m06.05s | 1045296 ko || +0m00.08s || 2920 ko | +1.32% | +0.27% 0m05.99s | 1142012 ko | Bedrock/Field/Synthesis/New/UnsaturatedSolinas.vo | 0m06.30s | 1140152 ko || -0m00.30s || 1860 ko | -4.92% | +0.16% 0m05.77s | 543492 ko | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.72s | 544060 ko || +0m00.04s || -568 ko | +0.87% | -0.10% 0m05.77s | 573064 ko | Rewriter/Passes/NoSelect.vo | 0m05.75s | 574592 ko || +0m00.01s || -1528 ko | +0.34% | -0.26% 0m05.54s | 909144 ko | Bedrock/Field/Translation/Proofs/UsedVarnames.vo | 0m05.65s | 908360 ko || -0m00.11s || 784 ko | -1.94% | +0.08% 0m05.49s | 551392 ko | PushButtonSynthesis/FancyMontgomeryReductionReificationCache.vo | 0m06.26s | 549176 ko || -0m00.76s || 2216 ko | -12.30% | +0.40% 0m05.34s | 538884 ko | Fancy/Prod.vo | 0m05.41s | 538800 ko || -0m00.07s || 84 ko | -1.29% | +0.01% 0m05.15s | 618708 ko | Bedrock/End2End/RupicolaCrypto/Broadcast.vo | 0m05.10s | 617832 ko || +0m00.05s || 876 ko | +0.98% | +0.14% 0m04.92s | 552816 ko | Language/InversionExtra.vo | 0m04.68s | 551468 ko || +0m00.24s || 1348 ko | +5.12% | +0.24% 0m04.49s | 1037344 ko | PushButtonSynthesis/DettmanMultiplication.vo | 0m04.60s | 1037096 ko || -0m00.10s || 248 ko | -2.39% | +0.02% 0m04.34s | 1071460 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Cmd.vo | 0m04.51s | 1070156 ko || -0m00.16s || 1304 ko | -3.76% | +0.12% 0m04.12s | 1043552 ko | PushButtonSynthesis/SaturatedSolinas.vo | 0m04.21s | 1042528 ko || -0m00.08s || 1024 ko | -2.13% | +0.09% 0m04.04s | 1509780 ko | Bedrock/Everything.vo | 0m04.30s | 1507700 ko || -0m00.25s || 2080 ko | -6.04% | +0.13% 0m03.88s | 955608 ko | Assembly/Equivalence.vo | 0m03.85s | 955484 ko || +0m00.02s || 124 ko | +0.77% | +0.01% 0m03.77s | 1058376 ko | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m03.68s | 1056232 ko || +0m00.08s || 2144 ko | +2.44% | +0.20% 0m03.46s | 1367392 ko | Everything.vo | 0m03.83s | 1357220 ko || -0m00.37s || 10172 ko | -9.66% | +0.74% 0m03.42s | 462772 ko | CastLemmas.vo | 0m03.52s | 460708 ko || -0m00.10s || 2064 ko | -2.84% | +0.44% 0m02.95s | 619192 ko | Bedrock/Field/Synthesis/Generic/Bignum.vo | 0m03.21s | 615928 ko || -0m00.25s || 3264 ko | -8.09% | +0.52% 0m02.93s | 547416 ko | PushButtonSynthesis/BaseConversionReificationCache.vo | 0m03.08s | 545340 ko || -0m00.14s || 2076 ko | -4.87% | +0.38% 0m02.86s | 1013968 ko | Bedrock/Field/Translation/Cmd.vo | 0m02.90s | 1011888 ko || -0m00.04s || 2080 ko | -1.37% | +0.20% 0m02.84s | 1351068 ko | PerfTesting/PerfTestPrint.vo | 0m03.07s | 1351172 ko || -0m00.23s || -104 ko | -7.49% | -0.00% 0m02.77s | 538024 ko | Rewriter/Passes/ArithWithRelaxedCasts.vo | 0m02.84s | 535952 ko || -0m00.06s || 2072 ko | -2.46% | +0.38% 0m02.73s | 1074352 ko | Bedrock/Field/Stringification/Stringification.vo | 0m02.91s | 1073232 ko || -0m00.18s || 1120 ko | -6.18% | +0.10% 0m02.69s | 1080972 ko | Rewriter/PerfTesting/Core.vo | 0m02.90s | 1080988 ko || -0m00.20s || -16 ko | -7.24% | -0.00% 0m02.68s | 669512 ko | Bedrock/Group/ScalarMult/ScalarMult.vo | 0m03.67s | 672696 ko || -0m00.98s || -3184 ko | -26.97% | -0.47% 0m02.67s | 1124652 ko | StandaloneHaskellMain.vo | 0m02.85s | 1128712 ko || -0m00.18s || -4060 ko | -6.31% | -0.35% 0m02.66s | 519056 ko | Rewriter/Passes/Test.vo | 0m02.64s | 519224 ko || +0m00.02s || -168 ko | +0.75% | -0.03% 0m02.65s | 1010364 ko | Bedrock/Field/Translation/Func.vo | 0m02.78s | 1009000 ko || -0m00.12s || 1364 ko | -4.67% | +0.13% 0m02.65s | 1137252 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo | 0m02.82s | 1135256 ko || -0m00.16s || 1996 ko | -6.02% | +0.17% 0m02.64s | 1151424 ko | Bedrock/Standalone/StandaloneHaskellMain.vo | 0m02.84s | 1149244 ko || -0m00.19s || 2180 ko | -7.04% | +0.18% 0m02.64s | 536980 ko | Rewriter/Passes/AddAssocLeft.vo | 0m02.73s | 538840 ko || -0m00.08s || -1860 ko | -3.29% | -0.34% 0m02.62s | 1126724 ko | StandaloneOCamlMain.vo | 0m02.81s | 1124820 ko || -0m00.18s || 1904 ko | -6.76% | +0.16% 0m02.60s | 1151328 ko | Bedrock/Standalone/StandaloneOCamlMain.vo | 0m02.82s | 1149340 ko || -0m00.21s || 1988 ko | -7.80% | +0.17% 0m02.57s | 1067372 ko | Bedrock/Field/Translation/Proofs/ValidComputable/Func.vo | 0m02.83s | 1066028 ko || -0m00.26s || 1344 ko | -9.18% | +0.12% 0m02.51s | 1070256 ko | Bedrock/Field/Synthesis/New/ComputedOp.vo | 0m02.69s | 1069024 ko || -0m00.18s || 1232 ko | -6.69% | +0.11% 0m02.46s | 623592 ko | Bedrock/Field/Interface/Compilation2.vo | 0m02.63s | 624284 ko || -0m00.16s || -692 ko | -6.46% | -0.11% 0m02.45s | 548060 ko | Bedrock/Field/Translation/Expr.vo | 0m02.31s | 545488 ko || +0m00.14s || 2572 ko | +6.06% | +0.47% 0m02.34s | 537832 ko | Rewriter/Passes/FlattenThunkedRects.vo | 0m02.28s | 535868 ko || +0m00.06s || 1964 ko | +2.63% | +0.36% 0m02.29s | 1049416 ko | Bedrock/Field/Translation/Parameters/Defaults64.vo | 0m02.36s | 1049520 ko || -0m00.06s || -104 ko | -2.96% | -0.00% 0m02.26s | 1046904 ko | Bedrock/Field/Translation/Parameters/Defaults.vo | 0m02.35s | 1046768 ko || -0m00.09s || 136 ko | -3.82% | +0.01% 0m02.26s | 1049440 ko | Bedrock/Field/Translation/Parameters/FE310.vo | 0m02.41s | 1048624 ko || -0m00.15s || 816 ko | -6.22% | +0.07% 0m02.25s | 1049404 ko | Bedrock/Field/Translation/Parameters/Defaults32.vo | 0m02.38s | 1049464 ko || -0m00.12s || -60 ko | -5.46% | -0.00% 0m02.03s | 616408 ko | Bedrock/Field/Common/Arrays/MakeAccessSizes.vo | 0m02.14s | 616276 ko || -0m00.11s || 132 ko | -5.14% | +0.02% 0m02.01s | 545060 ko | Stringification/Language.vo | 0m02.01s | 543272 ko || +0m00.00s || 1788 ko | +0.00% | +0.32% 0m01.74s | 539000 ko | Rewriter/Passes/StripLiteralCasts.vo | 0m01.72s | 537668 ko || +0m00.02s || 1332 ko | +1.16% | +0.24% 0m01.71s | 639164 ko | Bedrock/Group/ScalarMult/MontgomeryEquivalence.vo | 0m01.87s | 638432 ko || -0m00.16s || 732 ko | -8.55% | +0.11% 0m01.69s | 536832 ko | Rewriter/Passes/UnfoldValueBarrier.vo | 0m01.77s | 540684 ko || -0m00.08s || -3852 ko | -4.51% | -0.71% 0m01.60s | 514120 ko | AbstractInterpretation/Fancy/AbstractInterpretation.vo | 0m01.64s | 512084 ko || -0m00.03s || 2036 ko | -2.43% | +0.39% 0m01.59s | 540756 ko | Rewriter/Passes/ToFancy.vo | 0m01.59s | 534608 ko || +0m00.00s || 6148 ko | +0.00% | +1.15% 0m01.57s | 522584 ko | AbstractInterpretation/ZRange.vo | 0m01.57s | 520536 ko || +0m00.00s || 2048 ko | +0.00% | +0.39% 0m01.54s | 612044 ko | Bedrock/Field/Common/Names/MakeNames.vo | 0m01.64s | 612792 ko || -0m00.09s || -748 ko | -6.09% | -0.12% 0m01.50s | 511852 ko | AbstractInterpretation/Bottomify/AbstractInterpretation.vo | 0m01.56s | 512044 ko || -0m00.06s || -192 ko | -3.84% | -0.03% 0m01.46s | 593628 ko | CompilersTestCases.vo | 0m01.44s | 592128 ko || +0m00.02s || 1500 ko | +1.38% | +0.25% 0m01.32s | 543916 ko | Stringification/Go.vo | 0m01.30s | 543816 ko || +0m00.02s || 100 ko | +1.53% | +0.01% 0m01.24s | 528640 ko | AbstractInterpretation/Proofs.vo | 0m01.20s | 528576 ko || +0m00.04s || 64 ko | +3.33% | +0.01% 0m01.08s | 633492 ko | Bedrock/Specs/Field.vo | 0m01.23s | 631456 ko || -0m00.14s || 2036 ko | -12.19% | +0.32% 0m01.02s | 610084 ko | Bedrock/Field/Common/Arrays/MaxBounds.vo | 0m01.13s | 610100 ko || -0m00.10s || -16 ko | -9.73% | -0.00% 0m00.98s | 603908 ko | Bedrock/Field/Common/Arrays/ByteBounds.vo | 0m01.01s | 604044 ko || -0m00.03s || -136 ko | -2.97% | -0.02% 0m00.90s | 539712 ko | Bedrock/Field/Translation/LoadStoreList.vo | 0m00.91s | 538964 ko || -0m00.01s || 748 ko | -1.09% | +0.13% 0m00.88s | 541444 ko | Stringification/C.vo | 0m00.89s | 541524 ko || -0m00.01s || -80 ko | -1.12% | -0.01% 0m00.87s | 539148 ko | Stringification/JSON.vo | 0m00.90s | 537108 ko || -0m00.03s || 2040 ko | -3.33% | +0.37% 0m00.84s | 541104 ko | Stringification/Zig.vo | 0m00.81s | 537096 ko || +0m00.02s || 4008 ko | +3.70% | +0.74% 0m00.83s | 616196 ko | Bedrock/Field/Interface/Representation.vo | 0m00.87s | 616296 ko || -0m00.04s || -100 ko | -4.59% | -0.01% 0m00.81s | 536436 ko | Bedrock/Field/Common/Types.vo | 0m00.82s | 535080 ko || -0m00.00s || 1356 ko | -1.21% | +0.25% 0m00.81s | 539924 ko | Bedrock/Field/Translation/Proofs/Equivalence.vo | 0m00.81s | 538976 ko || +0m00.00s || 948 ko | +0.00% | +0.17% 0m00.79s | 620084 ko | Bedrock/Group/Point.vo | 0m00.86s | 621820 ko || -0m00.06s || -1736 ko | -8.13% | -0.27% 0m00.78s | 537940 ko | Stringification/Rust.vo | 0m00.81s | 537864 ko || -0m00.03s || 76 ko | -3.70% | +0.01% 0m00.77s | 537780 ko | Stringification/Java.vo | 0m00.81s | 537972 ko || -0m00.04s || -192 ko | -4.93% | -0.03% 0m00.75s | 590292 ko | Bedrock/Field/Common/Tactics.vo | 0m00.74s | 592228 ko || +0m00.01s || -1936 ko | +1.35% | -0.32% 0m00.72s | 505868 ko | Language/APINotations.vo | 0m00.73s | 505972 ko || -0m00.01s || -104 ko | -1.36% | -0.02% 0m00.69s | 548152 ko | Bedrock/Field/Stringification/FlattenVarData.vo | 0m00.68s | 548924 ko || +0m00.00s || -772 ko | +1.47% | -0.14% 0m00.68s | 541572 ko | Bedrock/Field/Stringification/LoadStoreListVarData.vo | 0m00.70s | 542352 ko || -0m00.01s || -780 ko | -2.85% | -0.14% 0m00.66s | 517348 ko | AbstractInterpretation/Wf.vo | 0m00.61s | 518040 ko || +0m00.05s || -692 ko | +8.19% | -0.13% 0m00.65s | 516864 ko | AbstractInterpretation/Fancy/WfExtra.vo | 0m00.62s | 515400 ko || +0m00.03s || 1464 ko | +4.83% | +0.28% 0m00.65s | 537532 ko | Bedrock/Field/Translation/Flatten.vo | 0m00.64s | 537568 ko || +0m00.01s || -36 ko | +1.56% | -0.00% 0m00.64s | 523068 ko | Bedrock/Field/Common/Arrays/MakeListLengths.vo | 0m00.68s | 523072 ko || -0m00.04s || -4 ko | -5.88% | -0.00% 0m00.64s | 439920 ko | Rewriter/Rules.vo | 0m00.68s | 442548 ko || -0m00.04s || -2628 ko | -5.88% | -0.59% 0m00.63s | 550452 ko | Rewriter/All.vo | 0m00.62s | 548168 ko || +0m00.01s || 2284 ko | +1.61% | +0.41% 0m00.62s | 536664 ko | Bedrock/Field/Translation/Proofs/VarnameSet.vo | 0m00.67s | 537484 ko || -0m00.05s || -820 ko | -7.46% | -0.15% 0m00.62s | 504536 ko | MiscCompilerPassesProofsExtra.vo | 0m00.66s | 505220 ko || -0m00.04s || -684 ko | -6.06% | -0.13% 0m00.61s | 515352 ko | AbstractInterpretation/Bottomify/WfExtra.vo | 0m00.63s | 515384 ko || -0m00.02s || -32 ko | -3.17% | -0.00% 0m00.61s | 502908 ko | Language/WfExtra.vo | 0m00.63s | 502392 ko || -0m00.02s || 516 ko | -3.17% | +0.10% 0m00.60s | 503684 ko | AbstractInterpretation/AbstractInterpretation.vo | 0m00.66s | 503728 ko || -0m00.06s || -44 ko | -9.09% | -0.00% 0m00.60s | 518640 ko | AbstractInterpretation/WfExtra.vo | 0m00.59s | 518248 ko || +0m00.01s || 392 ko | +1.69% | +0.07% 0m00.60s | 513080 ko | Language/API.vo | 0m00.60s | 511192 ko || +0m00.00s || 1888 ko | +0.00% | +0.36% 0m00.60s | 502224 ko | Language/UnderLetsProofsExtra.vo | 0m00.60s | 503052 ko || +0m00.00s || -828 ko | +0.00% | -0.16% 0m00.60s | 511968 ko | PushButtonSynthesis/ReificationCache.vo | 0m00.58s | 512032 ko || +0m00.02s || -64 ko | +3.44% | -0.01% 0m00.55s | 503160 ko | Rewriter/AllTacticsExtra.vo | 0m00.60s | 502504 ko || -0m00.04s || 656 ko | -8.33% | +0.13% 0m00.35s | 405512 ko | Rewriter/TestRules.vo | 0m00.37s | 403052 ko || -0m00.02s || 2460 ko | -5.40% | +0.61% 0m00.34s | 437584 ko | Language/PreExtra.vo | 0m00.31s | 393984 ko || +0m00.03s || 43600 ko | +9.67% | +11.06% 0m00.32s | 415460 ko | Language/IdentifierParameters.vo | 0m00.33s | 413516 ko || -0m00.01s || 1944 ko | -3.03% | +0.47% 0m00.30s | 366268 ko | Rewriter/TestRulesProofs.vo | 0m00.33s | 364416 ko || -0m00.03s || 1852 ko | -9.09% | +0.50% ```

--- src/AbstractInterpretation/ZRange.v | 43 ++- .../ZRangeCommonProofs.v | 13 +- src/AbstractInterpretation/ZRangeProofs.v | 296 ++++++++++++++++-- src/Assembly/Equivalence.v | 66 ++-- src/BoundsPipeline.v | 1 + src/Language/APINotations.v | 30 +- src/Language/IdentifierParameters.v | 17 + src/Language/PreExtra.v | 72 +++++ src/Stringification/IR.v | 14 + src/Stringification/Language.v | 41 ++- 10 files changed, 510 insertions(+), 83 deletions(-) diff --git a/src/AbstractInterpretation/ZRange.v b/src/AbstractInterpretation/ZRange.v index 7e61de8c8e..a2cdff28bb 100644 --- a/src/AbstractInterpretation/ZRange.v +++ b/src/AbstractInterpretation/ZRange.v @@ -536,13 +536,17 @@ Module Compilers. | ident.Nat_pred as idc => option_map (ident.interp idc) | ident.Z_of_nat as idc - => option_map (fun n => r[Z.of_nat n~>Z.of_nat n]%zrange) + | ident.Z_pos as idc + => option_map (fun n => r[ident.interp idc n~>ident.interp idc n]%zrange) | ident.Z_to_nat as idc + | ident.Z_to_pos as idc => fun v => v <- to_literal v; Some (ident.interp idc v) | ident.List_length _ => option_map (@List.length _) | ident.value_barrier => fun x => x + | ident.Pos_mul as idc + | ident.Pos_add as idc | ident.Nat_max as idc | ident.Nat_mul as idc | ident.Nat_add as idc @@ -675,18 +679,22 @@ Module Compilers. n | None => ZRange.type.base.option.None end - | ident.nat_rect_arrow _ _ - | ident.eager_nat_rect_arrow _ _ - => fun O_case S_case n v - => match n with + | ident.nat_rect_arrow _ _ as idc + | ident.eager_nat_rect_arrow _ _ as idc + (* + | ident.nat_rect_fbb_b _ _ _ as idc + | ident.nat_rect_fbb_b_b _ _ _ _ as idc + *) + => fun O_case S_case n + => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in + match n return type.option.interp t with | Some n => nat_rect _ O_case (fun n' rec => S_case (Some n') rec) n - v - | None => ZRange.type.base.option.None + | None => ZRange.type.option.None end | ident.list_rect _ _ | ident.eager_list_rect _ _ @@ -700,18 +708,25 @@ Module Compilers. ls | None => ZRange.type.base.option.None end - | ident.list_rect_arrow _ _ _ - | ident.eager_list_rect_arrow _ _ _ - => fun N C ls v - => match ls with + | ident.list_rect_arrow _ _ _ as idc + | ident.eager_list_rect_arrow _ _ _ as idc + (* + | ident.list_rect_fbb_b _ _ _ _ as idc + | ident.list_rect_fbb_b_b _ _ _ _ _ as idc + | ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc + | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc + | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ as idc + *) + => fun N C ls + => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in + match ls return type.option.interp t with | Some ls => list_rect _ N (fun x xs rec => C x (Some xs) rec) ls - v - | None => ZRange.type.base.option.None + | None => ZRange.type.option.None end | ident.list_case _ _ => fun N C ls @@ -763,6 +778,8 @@ Module Compilers. | 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_abs as idc + => fun x => x <- x; Some (ZRange.two_corners_and_zero (ident.interp idc) x) | ident.Z_max as idc | ident.Z_min as idc | ident.Z_add as idc diff --git a/src/AbstractInterpretation/ZRangeCommonProofs.v b/src/AbstractInterpretation/ZRangeCommonProofs.v index 1a6992810b..2fb7f87210 100644 --- a/src/AbstractInterpretation/ZRangeCommonProofs.v +++ b/src/AbstractInterpretation/ZRangeCommonProofs.v @@ -9,6 +9,7 @@ Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.ZUtil.Morphisms. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.DoWithHyp. Require Import Crypto.AbstractInterpretation.ZRange. Module Compilers. @@ -36,6 +37,14 @@ Module Compilers. | progress inversion_option | discriminate | solve [ eauto ] + | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq ==> eq)%signature) + | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq)%signature) + | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq)%signature) + | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature) + | apply (@list_rect_Proper_gen _ ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature) + | apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature) + | apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature) + | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature) | apply NatUtil.nat_rect_Proper_nondep | apply ListUtil.list_rect_Proper | apply ListUtil.list_rect_arrow_Proper @@ -43,7 +52,6 @@ Module Compilers. | apply ListUtil.pointwise_map | apply ListUtil.fold_right_Proper | apply ListUtil.update_nth_Proper - | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature) | cbn; apply (f_equal (@Some _)) | progress cbn [ZRange.ident.option.interp] | progress cbv [zrange_rect] @@ -54,7 +62,8 @@ Module Compilers. | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl) | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ] => specialize (H y); rewrite H1, H2 in H - end ]. + end + | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) ]. Qed. End interp_related. End option. diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v index aad9dd774c..a109f24723 100644 --- a/src/AbstractInterpretation/ZRangeProofs.v +++ b/src/AbstractInterpretation/ZRangeProofs.v @@ -436,7 +436,7 @@ Module Compilers. | break_innermost_match_step | break_innermost_match_hyps_step | progress cbn [id - ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp] in * + ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp ZRange.type.option.None] in * | progress ident.fancy.cbv_fancy_in_all | progress destruct_head'_bool | solve [ auto with nocore ] @@ -482,16 +482,43 @@ Module Compilers. | [ |- and _ _ ] => apply conj end | progress cbv [bool_eq Bool.eqb option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool zrange_beq] in * + | let rec do_rect_head lhs rhs k := + lazymatch lhs with + | nat_rect ?P ?O ?S ?n + => lazymatch rhs with + | nat_rect ?P' ?O' ?S' n + => is_var n; + k (); + induction n; cbn [nat_rect]; + generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S'); + intros + end + | list_rect ?P ?N ?C ?ls + => lazymatch rhs with + | list_rect ?P' ?N' ?C' ?ls' + => lazymatch goal with + | [ H : length ls = length ls' |- _ ] + => is_var ls; is_var ls'; k (); + let IH := fresh "IH" in + (revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in * ); + [ + | exfalso; discriminate | exfalso; discriminate + | specialize (IH ls'); + generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ]; + intros + end + end + | ?f ?x + => lazymatch rhs with + | ?g ?y + => is_var x; is_var y; + do_rect_head f g ltac:(fun _ => k (); revert dependent x; try revert dependent y) + end + end in + lazymatch goal with + | [ |- ?R ?lhs ?rhs = true ] => do_rect_head lhs rhs ltac:(fun _ => idtac) + end | match goal with - | [ |- ?R (nat_rect ?P ?O ?S ?n) (nat_rect ?P' ?O' ?S' ?n) = true ] - => is_var n; induction n; cbn [nat_rect]; - generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S'); - intros - | [ |- ?R (nat_rect ?P ?O ?S ?n ?x) (nat_rect ?P' ?O' ?S' ?n ?y) = true ] - => is_var n; is_var x; is_var y; - revert dependent x; revert dependent y; induction n; cbn [nat_rect]; - generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S'); - intros | [ H : length ?ls = length ?ls' |- ?R (List.fold_right ?f ?x ?ls) (List.fold_right ?f' ?x' ?ls') = true ] => is_var ls; is_var ls'; let IH := fresh "IH" in @@ -510,25 +537,6 @@ Module Compilers. | specialize (IH ls'); generalize dependent (List.fold_right f x); generalize dependent (List.fold_right f' x') ]; intros - | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls) (list_rect ?P' ?N' ?C' ?ls') = true ] - => is_var ls; is_var ls'; - let IH := fresh "IH" in - revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *; - [ - | exfalso; discriminate | exfalso; discriminate - | specialize (IH ls'); - generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ]; - intros - | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls ?x) (list_rect ?P' ?N' ?C' ?ls' ?y) = true ] - => is_var ls; is_var ls'; is_var x; is_var y; - revert dependent y; try revert dependent x; - let IH := fresh "IH" in - revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *; - [ - | exfalso; discriminate | exfalso; discriminate - | specialize (IH ls'); - generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ]; - intros | [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ] => apply H; clear H @@ -550,7 +558,8 @@ Module Compilers. => 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 ]. + end + | do_with_hyp' ltac:(fun H => apply H; clear H; now non_arith_t) ]. Local Lemma mul_by_halves_bounds x y n : (0 <= x < 2^ (n / 2))%Z -> @@ -723,6 +732,15 @@ Module Compilers. all: change (@list_rect_arrow_nodep) with (fun A P Q => @list_rect A (fun _ => P -> Q)). all: change (@Thunked.list_case) with (fun A P PNil => @list_case A (fun _ => P) (PNil Datatypes.tt)) in *. all: change (@Thunked.option_rect) with (fun A P PS PN => @option_rect A (fun _ => P) PS (PN Datatypes.tt)) in *. + all: cbv [ + nat_rect_fbb_b + nat_rect_fbb_b_b + list_rect_fbb_b + list_rect_fbb_b_b + list_rect_fbb_b_b_b + list_rect_fbb_b_b_b_b + list_rect_fbb_b_b_b_b_b + ] in *. all: cbv [respectful_hetero option_map option_rect zrange_rect list_case]. all: intros. all: destruct_head_hnf' prod. @@ -786,6 +804,9 @@ Module Compilers. | [ Hx : is_bounded_by_bool _ ?x = true |- is_bounded_by_bool _ (ZRange.two_corners ?f ?x) = true ] => apply (fun pf => @ZRange.monotoneb_two_corners_gen f pf x _ Hx); intros; auto with zarith + | [ Hx : is_bounded_by_bool _ ?x = true + |- is_bounded_by_bool _ (ZRange.two_corners_and_zero ?f ?x) = true ] + => apply (fun pf1 pf2 => @ZRange.monotoneb_two_corners_and_zero_gen f pf1 pf2 x _ Hx); intros; auto with zarith | [ |- is_bounded_by_bool (if _ then _ else _) (ZRange.four_corners _ _ _) = true ] => apply ZRange.is_bounded_by_bool_Proper_if_bool_union_dep; intros; Z.ltb_to_lt | [ _ : is_bounded_by_bool ?x1 ?r1 = true, @@ -817,6 +838,7 @@ Module Compilers. end | intros; mul_by_halves_t ]. all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ]. + all: try solve [ non_arith_t; try match goal with |- ?x = true => destruct x eqn:? end; reflect_hyps; subst; nia ]. 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 () .. ]. @@ -831,11 +853,221 @@ Module Compilers. all: try apply ZRange.ident.option.interp_Proper. all: try assumption. all: try reflexivity. } - { destruct idc. + { (* + pose proof (interp_related idc) as Hir. + pose proof (ident.interp_Proper idc idc eq_refl) as Hip. + pose proof (ZRange.ident.option.interp_Proper assume_cast_truncates idc idc eq_refl) as Hzip. + *) + destruct idc. all: try (apply Bool.diff_true_false in Hho; exfalso; exact Hho). + (* + all: cbn [interp_is_related_and_Proper type.interp type.related interp_is_related] in *; + cbv [Proper respectful respectful_hetero] in *. + all: cbn [ZRange.ident.option.interp ident.interp]. + all: cbn [ZRange.type.base.option.interp ZRange.type.option.None ZRange.type.base.interp]. + all: cbn [base.interp IdentifiersBasicGENERATED.Compilers.base_interp]. + all: cbv [ + nat_rect_fbb_b + nat_rect_fbb_b_b + list_rect_fbb_b + list_rect_fbb_b_b + list_rect_fbb_b_b_b + list_rect_fbb_b_b_b_b + list_rect_fbb_b_b_b_b_b + ] in *. + all: cbn [Language.Compilers.base.interp IdentifiersBasicGENERATED.Compilers.base_interp ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by base.interp_beq]. + all: lazymatch goal with + | [ |- (forall (a1 : ?A1) (a2 : @?A2 a1) (a3 : @?A3 a1 a2) (a4 : @?A4 a1 a2 a3) (a5 : @?A5 a1 a2 a3 a4) (a6 : @?A6 a1 a2 a3 a4 a5) (a7 a8 : ?optT) (a9 : a7 = a8), @?AP a1 a2 a4 a5 a7 a8) + /\ (forall (b1 : ?B1) (b2 : @?B2 b1) (b3 : @?B3 b1 b2) (b4 : @?B4 b1 b2 b3) (b5 : @?B5 b1 b2 b3 b4) (b6 : @?B6 b1 b2 b3 b4 b5) (b7 b8 : ?T) (b9 : b7 = b8), @?BP b1 b2 b4 b5 b7 b8) + /\ (forall (c1 : ?C1) (c2 : @?C2 c1) (c3 : @?C3 c1 c2), + (forall (d4 : @?D4 c1 c2 c3) (d5 : @?D5 c1 c2 c3 d4) (d6 : @?D6 c1 c2 c3 d4 d5) (d7 d8 : ?optT) (d9 : d7 = d8), @?DP c1 c2 d4 d5 d7 d8) + /\ (forall (e4 : @?E4 c1 c2 c3) (e5 : @?E5 c1 c2 c3 e4) (e6 : @?E6 c1 c2 c3 e4 e5) (e7 e8 : ?T) (e9 : e7 = e8), @?EP c1 c2 e4 e5 e7 e8) + /\ (forall (f4 : @?F4 c1 c2 c3) (f5 : @?F5 c1 c2 c3 f4) (f6 : @?F6 c1 c2 c3 f4 f5), + (forall (g7 g8 : ?optT) (g9 : g7 = g8), @?GP c1 c2 f4 f5 g7 g8) + /\ (forall (h7 h8 : ?T) (h9 : h7 = h8), @?HP c1 c2 f4 f5 h7 h8) + /\ (forall (i7 : ?optT) (i8 : ?T) (i9 : @?TR i7 i8), @?IP c1 c2 f4 f5 i7 i8))) ] + => let G' + := constr:(forall (i7 : optT) (i8 : T), + (forall (a1 : A1) (a2 : A2 a1) (a3 : A3 a1 a2) (a4 : A4 a1 a2 a3) (a5 : A5 a1 a2 a3 a4) (a6 : A6 a1 a2 a3 a4 a5), AP a1 a2 a4 a5 i7 i7) + /\ (forall (b1 : B1) (b2 : B2 b1) (b3 : B3 b1 b2) (b4 : B4 b1 b2 b3) (b5 : B5 b1 b2 b3 b4) (b6 : B6 b1 b2 b3 b4 b5), BP b1 b2 b4 b5 i8 i8) + /\ (forall (c1 : C1) (c2 : C2 c1) (c3 : C3 c1 c2), + (forall (d4 : D4 c1 c2 c3) (d5 : D5 c1 c2 c3 d4) (d6 : D6 c1 c2 c3 d4 d5), DP c1 c2 d4 d5 i7 i7) + /\ (forall (e4 : E4 c1 c2 c3) (e5 : E5 c1 c2 c3 e4) (e6 : E6 c1 c2 c3 e4 e5), EP c1 c2 e4 e5 i8 i8) + /\ (forall (f4 : F4 c1 c2 c3) (f5 : F5 c1 c2 c3 f4) (f6 : F6 c1 c2 c3 f4 f5), + GP c1 c2 f4 f5 i7 i7 + /\ HP c1 c2 f4 f5 i8 i8 + /\ (TR i7 i8 -> IP c1 c2 f4 f5 i7 i8)))) in + cut G'; + [ clear; + change (G' + -> ((forall (a1 : A1) (a2 : A2 a1) (a3 : A3 a1 a2) (a4 : A4 a1 a2 a3) (a5 : A5 a1 a2 a3 a4) (a6 : A6 a1 a2 a3 a4 a5) (a7 a8 : optT) (a9 : a7 = a8), AP a1 a2 a4 a5 a7 a8) + /\ (forall (b1 : B1) (b2 : B2 b1) (b3 : B3 b1 b2) (b4 : B4 b1 b2 b3) (b5 : B5 b1 b2 b3 b4) (b6 : B6 b1 b2 b3 b4 b5) (b7 b8 : T) (b9 : b7 = b8), BP b1 b2 b4 b5 b7 b8) + /\ (forall (c1 : C1) (c2 : C2 c1) (c3 : C3 c1 c2), + (forall (d4 : D4 c1 c2 c3) (d5 : D5 c1 c2 c3 d4) (d6 : D6 c1 c2 c3 d4 d5) (d7 d8 : optT) (d9 : d7 = d8), DP c1 c2 d4 d5 d7 d8) + /\ (forall (e4 : E4 c1 c2 c3) (e5 : E5 c1 c2 c3 e4) (e6 : E6 c1 c2 c3 e4 e5) (e7 e8 : T) (e9 : e7 = e8), EP c1 c2 e4 e5 e7 e8) + /\ (forall (f4 : F4 c1 c2 c3) (f5 : F5 c1 c2 c3 f4) (f6 : F6 c1 c2 c3 f4 f5), + (forall (g7 g8 : optT) (g9 : g7 = g8), GP c1 c2 f4 f5 g7 g8) + /\ (forall (h7 h8 : T) (h9 : h7 = h8), HP c1 c2 f4 f5 h7 h8) + /\ (forall (i7 : optT) (i8 : T) (i9 : TR i7 i8), IP c1 c2 f4 f5 i7 i8))))); + intro H'; revert H'; + try generalize AP BP DP EP GP HP IP; + try generalize optT T; + try generalize F6; + try generalize E6; + try generalize D6; + try generalize C3; + try generalize B3 B6; + try generalize A3 A6; + intros + | shelve ] + | _ => (** For command-line debugging, we display goals that should not remain *) + idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal (); + shelve + end. + all: repeat split; repeat intro; subst; eapply H'. + all: try eassumption. + all: try reflexivity. + all: try solve [ constructor ]. + all: fail. + Unshelve. + all: cbv beta. + Time + all: intros [x|] y; + [ revert x; induction y; cbn [nat_rect list_rect]; + [ intro x; induction x; cbn [nat_rect list_rect]; + [ solve [ + repeat split; intros; + auto; + repeat first [ do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) + | reflexivity ] + ] + | pose 1 as GOAL ] + | intro x; + repeat match goal with + | [ y : ?T |- _ ] + => lazymatch T with + | nat => idtac + | list _ => idtac + end; + tryif constr_eq y x then fail else revert dependent y + end; + induction x; cbn [nat_rect list_rect]; + [ pose 2 as GOAL + | pose 3 as GOAL ] ] + | induction y; cbn [nat_rect list_rect]; + [ repeat split; intros; auto; + solve [ + repeat first [ lazymatch goal with + | [ |- ZRange.type.base.option.is_bounded_by ZRange.type.base.option.None _ = true ] + => apply type.base.option.is_bounded_by_None + end + | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) + | reflexivity ] + ] + | pose 4 as GOAL ] + ]. + Time + all: + lazymatch goal with + | [ GOAL := 1 |- _ ] + => try time (repeat split; intros; auto; + reflect_hyps; destruct_head'_False; + solve [ + repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ]) + | do_with_exactly_one_hyp ltac:(fun H => apply H); intros; auto + | reflexivity + | solve [ auto ] + | progress subst + | progress intros ] + ] + ) + | _ => idtac + end. + Time + all: + lazymatch goal with + | [ GOAL := 4 |- _ ] + => try time + (repeat split; intros; auto; + let rec go _ := + repeat first [ lazymatch goal with + | [ |- ZRange.type.base.option.is_bounded_by ZRange.type.base.option.None _ = true ] + => apply type.base.option.is_bounded_by_None + end + | do_with_hyp' ltac:(fun H => solve [ apply H; auto ]) + | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros + | reflexivity + | solve [ auto ] + | progress subst + | progress intros + | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in + solve [ go () ]) + | _ => idtac + end. + Time + all: + lazymatch goal with + | [ GOAL := 2 |- _ ] + => try time + (repeat split; intros; auto; + reflect_hyps; destruct_head'_False; + solve [ + repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ]) + | do_with_exactly_one_hyp ltac:(fun H => apply H); intros; auto + | reflexivity + | solve [ auto ] + | solve [ constructor ] + | progress subst + | progress intros ] + ] + ) + | _ => idtac + end. + Time + all: + lazymatch goal with + | [ GOAL := 3 |- _ ] + => try time + (repeat split; intros; auto; + let rec go _ := + repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ]) + | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros + | reflexivity + | solve [ auto ] + | solve [ constructor ] + | progress subst + | progress intros + | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in + solve [ go () ]) + | _ => idtac + end. + Time + all: + lazymatch goal with + | [ GOAL := 3 |- _ ] + => try time + (repeat split; intros; auto; + cbn [fold_andb_map] in *; + lazymatch goal with + | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H; destruct H + | _ => idtac + end; + let rec go _ := + repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ]) + | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros + | reflexivity + | solve [ auto ] + | solve [ constructor ] + | progress subst + | progress intros + | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in + solve [ go () ]) + | _ => idtac + end. + *) (** For command-line debugging, we display goals that should not remain *) all: [ > idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal () .. ]. } - Qed. + Time Qed. End interp_related. End option. End ident. diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v index 5acc755847..07f93c8808 100644 --- a/src/Assembly/Equivalence.v +++ b/src/Assembly/Equivalence.v @@ -1042,26 +1042,12 @@ Proof. | ident.Literal base.type.Z v => App (const v, nil) | ident.Z_add => fun x y => App (addZ, [x; y]) - - | ident.Z_modulo - => symex_T_error (Unhandled_identifier idc) | ident.Z_mul => fun x y => App (mulZ, [x; y]) - | ident.Z_pow - => symex_T_error (Unhandled_identifier idc) | ident.Z_sub => fun x y => y' <- App (negZ, [y]); App (addZ, [x;y']) - | ident.Z_opp - | ident.Z_div - | ident.Z_log2 - | ident.Z_log2_up - | ident.Z_to_nat - => symex_T_error (Unhandled_identifier idc) | ident.Z_shiftr => fun x y => App (shrZ, [x; y]) | ident.Z_shiftl => fun x y => App (shlZ, [x; y]) | ident.Z_land => fun x y => App (andZ, [x; y]) | ident.Z_lor => fun x y => App (orZ, [x; y]) - | ident.Z_min - | ident.Z_max - => symex_T_error (Unhandled_identifier idc) | ident.Z_mul_split => fun bs x y => vs <- RevealWidth bs; s <- App (const (Z.of_N vs), nil); v <- App (mulZ, [x; y]); @@ -1096,21 +1082,10 @@ Proof. a <- App (add s, [x;y';z']); c <- App (subborrowZ s, [x;y;z]); symex_return (a, c) - | ident.Z_ltz - => symex_T_error (Unhandled_identifier idc) | ident.Z_zselect => fun c x y => App (Symbolic.selectznz, [c; x; y]) - | ident.Z_add_modulo - => symex_T_error (Unhandled_identifier idc) | ident.Z_truncating_shiftl => fun s x y => s <- RevealConstant s; App (shl s, [x; y]) - | ident.Z_bneg - | ident.Z_lnot_modulo - | ident.Z_lxor - | ident.Z_rshi - | ident.Z_cc_m - | ident.Z_combine_at_bitwidth - => symex_T_error (Unhandled_identifier idc) | ident.comment _ | ident.comment_no_keep _ @@ -1119,11 +1094,6 @@ Proof. => fun v => symex_return v | ident.tt => symex_return tt - | ident.Literal base.type.bool _ as idc - | ident.Literal base.type.string _ as idc - | ident.None _ as idc - | ident.Some _ as idc - => symex_T_error (Unhandled_identifier idc) | ident.Literal base.type.zrange v | ident.Literal base.type.nat v => symex_return v @@ -1176,6 +1146,29 @@ Proof. | ident.Z_of_nat => fun n => App (const (Z.of_nat n), nil) + | ident.Z_modulo + | ident.Z_pow + | ident.Z_opp + | ident.Z_div + | ident.Z_log2 + | ident.Z_log2_up + | ident.Z_to_nat + | ident.Z_min + | ident.Z_max + | ident.Z_abs + | ident.Z_ltz + | ident.Z_add_modulo + | ident.Z_bneg + | ident.Z_lnot_modulo + | ident.Z_lxor + | ident.Z_rshi + | ident.Z_cc_m + | ident.Z_combine_at_bitwidth + | ident.Literal base.type.bool _ + | ident.Literal base.type.string _ + | ident.Literal base.type.positive _ + | ident.None _ + | ident.Some _ | ident.Z_eqb | ident.Z_leb | ident.Z_ltb @@ -1194,6 +1187,15 @@ Proof. | ident.eager_list_rect _ _ | ident.list_rect_arrow _ _ _ | ident.eager_list_rect_arrow _ _ _ + (* + | ident.nat_rect_fbb_b _ _ _ + | ident.nat_rect_fbb_b_b _ _ _ _ + | ident.list_rect_fbb_b _ _ _ _ + | ident.list_rect_fbb_b_b _ _ _ _ _ + | ident.list_rect_fbb_b_b_b _ _ _ _ _ _ + | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ + | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ + *) | ident.list_case _ _ | ident.List_map _ _ | ident.List_flat_map _ _ @@ -1203,6 +1205,10 @@ Proof. | ident.List_update_nth _ | ident.option_rect _ _ | ident.zrange_rect _ + | ident.Pos_add + | ident.Pos_mul + | ident.Z_pos + | ident.Z_to_pos | ident.fancy_add | ident.fancy_addc | ident.fancy_sub diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v index 5df6d6a5e7..5666bb1945 100644 --- a/src/BoundsPipeline.v +++ b/src/BoundsPipeline.v @@ -459,6 +459,7 @@ Module Pipeline. | base.type.unit => fun 'tt 'tt => (false, nil, nil) | base.type.type_base base.type.nat + | base.type.type_base base.type.positive | base.type.type_base base.type.bool | base.type.type_base base.type.zrange | base.type.type_base base.type.string diff --git a/src/Language/APINotations.v b/src/Language/APINotations.v index df583c1653..cd6472a763 100644 --- a/src/Language/APINotations.v +++ b/src/Language/APINotations.v @@ -81,10 +81,21 @@ Module Compilers. Global Arguments ident_nat_rect_arrow {_ _} : assert. Global Arguments ident_eager_nat_rect {_} : assert. Global Arguments ident_eager_nat_rect_arrow {_ _} : assert. + (* + Global Arguments ident_nat_rect_fbb_b {_ _ _} : assert. + Global Arguments ident_nat_rect_fbb_b_b {_ _ _ _} : assert. +*) Global Arguments ident_list_rect {_ _} : assert. - Global Arguments ident_list_rect_arrow {_ _ _} : assert. Global Arguments ident_eager_list_rect {_ _} : assert. Global Arguments ident_eager_list_rect_arrow {_ _ _} : assert. + Global Arguments ident_list_rect_arrow {_ _ _} : assert. + (* + Global Arguments ident_list_rect_fbb_b {_ _ _ _} : assert. + Global Arguments ident_list_rect_fbb_b_b {_ _ _ _ _} : assert. + Global Arguments ident_list_rect_fbb_b_b_b {_ _ _ _ _ _} : assert. + Global Arguments ident_list_rect_fbb_b_b_b_b {_ _ _ _ _ _ _} : assert. + Global Arguments ident_list_rect_fbb_b_b_b_b_b {_ _ _ _ _ _ _ _} : assert. +*) Global Arguments ident_list_case {_ _} : assert. Global Arguments ident_List_length {_} : assert. Global Arguments ident_List_firstn {_} : assert. @@ -165,6 +176,7 @@ Module Compilers. Import IdentifiersBasicGENERATED.Compilers. Notation base := base (only parsing). Notation Z := Z (only parsing). + Notation positive := positive (only parsing). Notation nat := nat (only parsing). Notation zrange := zrange (only parsing). Notation bool := bool (only parsing). @@ -245,10 +257,21 @@ Module Compilers. Notation nat_rect_arrow := Compilers.ident_nat_rect_arrow (only parsing). Notation eager_nat_rect := Compilers.ident_eager_nat_rect (only parsing). Notation eager_nat_rect_arrow := Compilers.ident_eager_nat_rect_arrow (only parsing). + (* + Notation nat_rect_fbb_b := Compilers.ident_nat_rect_fbb_b (only parsing). + Notation nat_rect_fbb_b_b := Compilers.ident_nat_rect_fbb_b_b (only parsing). +*) Notation list_rect := Compilers.ident_list_rect (only parsing). Notation list_rect_arrow := Compilers.ident_list_rect_arrow (only parsing). Notation eager_list_rect := Compilers.ident_eager_list_rect (only parsing). Notation eager_list_rect_arrow := Compilers.ident_eager_list_rect_arrow (only parsing). + (* + Notation list_rect_fbb_b := Compilers.ident_list_rect_fbb_b (only parsing). + Notation list_rect_fbb_b_b := Compilers.ident_list_rect_fbb_b_b (only parsing). + Notation list_rect_fbb_b_b_b := Compilers.ident_list_rect_fbb_b_b_b (only parsing). + Notation list_rect_fbb_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b (only parsing). + Notation list_rect_fbb_b_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b_b (only parsing). +*) Notation list_case := Compilers.ident_list_case (only parsing). Notation List_length := Compilers.ident_List_length (only parsing). Notation List_seq := Compilers.ident_List_seq (only parsing). @@ -266,6 +289,8 @@ Module Compilers. Notation List_update_nth := Compilers.ident_List_update_nth (only parsing). Notation List_nth_default := Compilers.ident_List_nth_default (only parsing). Notation eager_List_nth_default := Compilers.ident_eager_List_nth_default (only parsing). + Notation Pos_add := Compilers.ident_Pos_add (only parsing). + Notation Pos_mul := Compilers.ident_Pos_mul (only parsing). Notation Z_add := Compilers.ident_Z_add (only parsing). Notation Z_mul := Compilers.ident_Z_mul (only parsing). Notation Z_pow := Compilers.ident_Z_pow (only parsing). @@ -282,12 +307,15 @@ Module Compilers. Notation Z_gtb := Compilers.ident_Z_gtb (only parsing). Notation Z_of_nat := Compilers.ident_Z_of_nat (only parsing). Notation Z_to_nat := Compilers.ident_Z_to_nat (only parsing). + Notation Z_pos := Compilers.ident_Z_pos (only parsing). + Notation Z_to_pos := Compilers.ident_Z_to_pos (only parsing). Notation Z_shiftr := Compilers.ident_Z_shiftr (only parsing). Notation Z_shiftl := Compilers.ident_Z_shiftl (only parsing). Notation Z_land := Compilers.ident_Z_land (only parsing). Notation Z_lor := Compilers.ident_Z_lor (only parsing). Notation Z_min := Compilers.ident_Z_min (only parsing). Notation Z_max := Compilers.ident_Z_max (only parsing). + Notation Z_abs := Compilers.ident_Z_abs (only parsing). Notation Z_bneg := Compilers.ident_Z_bneg (only parsing). Notation Z_lnot_modulo := Compilers.ident_Z_lnot_modulo (only parsing). Notation Z_lxor := Compilers.ident_Z_lxor (only parsing). diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v index 66aa4b36bc..3876026ac3 100644 --- a/src/Language/IdentifierParameters.v +++ b/src/Language/IdentifierParameters.v @@ -80,6 +80,7 @@ Definition var_like_idents : InductiveHList.hlist Definition base_type_list_named : InductiveHList.hlist := [with_name Z BinInt.Z + ; with_name positive BinPos.positive ; with_name bool Datatypes.bool ; with_name nat Datatypes.nat ; with_name zrange ZRange.zrange @@ -110,10 +111,21 @@ Definition all_ident_named_interped : InductiveHList.hlist ; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect)) ; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep) ; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep)) + (* + ; with_name ident_nat_rect_fbb_b (@nat_rect_fbb_b) + ; with_name ident_nat_rect_fbb_b_b (@nat_rect_fbb_b_b) +*) ; with_name ident_list_rect (@Thunked.list_rect) ; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect)) ; with_name ident_list_rect_arrow (@list_rect_arrow_nodep) ; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep)) + (* + ; with_name ident_list_rect_fbb_b (@list_rect_fbb_b) + ; with_name ident_list_rect_fbb_b_b (@list_rect_fbb_b_b) + ; with_name ident_list_rect_fbb_b_b_b (@list_rect_fbb_b_b_b) + ; with_name ident_list_rect_fbb_b_b_b_b (@list_rect_fbb_b_b_b_b) + ; with_name ident_list_rect_fbb_b_b_b_b_b (@list_rect_fbb_b_b_b_b_b) +*) ; with_name ident_list_case (@Thunked.list_case) ; with_name ident_List_length (@List.length) ; with_name ident_List_seq (@List.seq) @@ -131,6 +143,8 @@ Definition all_ident_named_interped : InductiveHList.hlist ; with_name ident_List_update_nth (@update_nth) ; with_name ident_List_nth_default (@nth_default) ; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default)) + ; with_name ident_Pos_add Pos.add + ; with_name ident_Pos_mul Pos.mul ; with_name ident_Z_add Z.add ; with_name ident_Z_mul Z.mul ; with_name ident_Z_pow Z.pow @@ -147,12 +161,15 @@ Definition all_ident_named_interped : InductiveHList.hlist ; with_name ident_Z_log2_up Z.log2_up ; with_name ident_Z_of_nat Z.of_nat ; with_name ident_Z_to_nat Z.to_nat + ; with_name ident_Z_pos Z.pos + ; with_name ident_Z_to_pos Z.to_pos ; with_name ident_Z_shiftr Z.shiftr ; with_name ident_Z_shiftl Z.shiftl ; with_name ident_Z_land Z.land ; with_name ident_Z_lor Z.lor ; with_name ident_Z_min Z.min ; with_name ident_Z_max Z.max + ; with_name ident_Z_abs Z.abs ; with_name ident_Z_mul_split Z.mul_split ; with_name ident_Z_mul_high Z.mul_high ; with_name ident_Z_add_get_carry Z.add_get_carry_full diff --git a/src/Language/PreExtra.v b/src/Language/PreExtra.v index 4bc9d22bdc..a06230d5d9 100644 --- a/src/Language/PreExtra.v +++ b/src/Language/PreExtra.v @@ -135,3 +135,75 @@ Module Thunked. Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing). Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing). End Thunked. + +Definition nat_rect_fbb_b {A B C} := + @Coq.Init.Datatypes.nat_rect (fun _ => (A -> B) -> C). +Definition nat_rect_fbb_b_b {A B C D} := + @Coq.Init.Datatypes.nat_rect (fun _ => (A -> B) -> C -> D). + +Definition list_rect_fbb_b {T A B C} := + @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C). +Definition list_rect_fbb_b_b {T A B C D} := + @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D). +Definition list_rect_fbb_b_b_b {T A B C D E} := + @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E). +Definition list_rect_fbb_b_b_b_b {T A B C D E F} := + @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E -> F). +Definition list_rect_fbb_b_b_b_b_b {T A B C D E F G} := + @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E -> F -> G). + +Lemma unfold1_nat_rect_fbb_b {A B C} fO fS n k : + @nat_rect_fbb_b A B C fO fS n k = + if Nat.eqb 0 n then fO k else fS (pred n) (nat_rect_fbb_b fO fS (pred n)) k. +Proof. case n; trivial. Qed. + +Lemma unfold1_nat_rect_fbb_b_b {A B C D} fO fS n k x : + @nat_rect_fbb_b_b A B C D fO fS n k x = + if Nat.eqb 0 n then fO k x else fS (pred n) (nat_rect_fbb_b_b fO fS (pred n)) k x. +Proof. case n; trivial. Qed. + +Lemma unfold1_list_rect_fbb_b {T A B C} fnil fcons l k : + @list_rect_fbb_b T A B C fnil fcons l k = + match l with + | nil => fnil k + | cons x l => fcons x l (list_rect_fbb_b fnil fcons l) k + end. +Proof. case l; trivial. Qed. + +Lemma unfold1_list_rect_fbb_b_b {T A B C D} fnil fcons l k c : + @list_rect_fbb_b_b T A B C D fnil fcons l k c = + match l with + | nil => fnil k c + | cons x l => fcons x l (list_rect_fbb_b_b fnil fcons l) k c + end. +Proof. case l; trivial. Qed. + +Lemma unfold1_list_rect_fbb_b_b_b {T A B C D E} fnil fcons l k c d : + @list_rect_fbb_b_b_b T A B C D E fnil fcons l k c d = + match l with + | nil => fnil k c d + | cons x l => fcons x l (list_rect_fbb_b_b_b fnil fcons l) k c d + end. +Proof. case l; trivial. Qed. + +Lemma unfold1_list_rect_fbb_b_b_b_b {T A B C D E F} fnil fcons l k c d e : + @list_rect_fbb_b_b_b_b T A B C D E F fnil fcons l k c d e = + match l with + | nil => fnil k c d e + | cons x l => fcons x l (list_rect_fbb_b_b_b_b fnil fcons l) k c d e + end. +Proof. case l; trivial. Qed. + +Lemma unfold1_list_rect_fbb_b_b_b_b_b {T A B C D E F G} fnil fcons l k c d e f : + @list_rect_fbb_b_b_b_b_b T A B C D E F G fnil fcons l k c d e f = + match l with + | nil => fnil k c d e f + | cons x l => fcons x l (list_rect_fbb_b_b_b_b_b fnil fcons l) k c d e f + end. +Proof. case l; trivial. Qed. + +Import Coq.Classes.Morphisms. + +Global Instance Proper_nat_rect_fbb_b {A B C} : + Proper (((eq ==> eq) ==> eq) ==> (eq ==> ((eq ==> eq) ==> eq) ==> (eq ==> eq) ==> eq) ==> eq ==> (eq ==> eq) ==> eq) (@nat_rect_fbb_b A B C) | 10. +Proof. cbv -[nat_rect]; intros ??? ??? n m ?; subst m. induction n; cbn; eauto. Qed. diff --git a/src/Stringification/IR.v b/src/Stringification/IR.v index 3459964df1..abe9e67816 100644 --- a/src/Stringification/IR.v +++ b/src/Stringification/IR.v @@ -793,6 +793,8 @@ Module Compilers. | ident.Nat_add | ident.Nat_sub | ident.Nat_eqb + | ident.Pos_add + | ident.Pos_mul | ident.prod_rect _ _ _ | ident.bool_rect _ | ident.bool_rect_nodep _ @@ -807,6 +809,15 @@ Module Compilers. | ident.eager_list_rect _ _ | ident.list_rect_arrow _ _ _ | ident.eager_list_rect_arrow _ _ _ + (* + | ident.nat_rect_fbb_b _ _ _ + | ident.nat_rect_fbb_b_b _ _ _ _ + | ident.list_rect_fbb_b _ _ _ _ + | ident.list_rect_fbb_b_b _ _ _ _ _ + | ident.list_rect_fbb_b_b_b _ _ _ _ _ _ + | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ + | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ + *) | ident.list_case _ _ | ident.List_length _ | ident.List_seq @@ -834,10 +845,13 @@ Module Compilers. | ident.Z_gtb | ident.Z_min | ident.Z_max + | ident.Z_abs | ident.Z_log2 | ident.Z_log2_up | ident.Z_of_nat | ident.Z_to_nat + | ident.Z_pos + | ident.Z_to_pos | ident.Z_ltz | ident.Z_zselect | ident.Z_mul_split diff --git a/src/Stringification/Language.v b/src/Stringification/Language.v index 570a40e5f7..a7cca8915e 100644 --- a/src/Stringification/Language.v +++ b/src/Stringification/Language.v @@ -177,6 +177,7 @@ Module Compilers. := match t return ShowLevel (ZRange.type.base.interp t) with | base.type.unit => @show_lvl unit _ | base.type.type_base base.type.Z => @show_lvl zrange _ + | base.type.type_base base.type.positive => @show_lvl positive _ | base.type.type_base base.type.bool => @show_lvl bool _ | base.type.type_base base.type.nat => @show_lvl nat _ | base.type.type_base base.type.zrange => @show_lvl zrange _ @@ -191,11 +192,7 @@ Module Compilers. Fixpoint show_lvl_interp {t} : ShowLevel (ZRange.type.base.option.interp t) := match t return ShowLevel (ZRange.type.base.option.interp t) with | base.type.unit => @show_lvl unit _ - | base.type.type_base base.type.Z => @show_lvl (option zrange) _ - | base.type.type_base base.type.bool => @show_lvl (option bool) _ - | base.type.type_base base.type.nat => @show_lvl (option nat) _ - | base.type.type_base base.type.zrange => @show_lvl (option zrange) _ - | base.type.type_base base.type.string => @show_lvl (option string) _ + | base.type.type_base _ as t => @show_lvl (option (ZRange.type.base.interp t)) _ | base.type.prod A B => @show_lvl (ZRange.type.base.option.interp A * ZRange.type.base.option.interp B) _ | base.type.list A => @show_lvl (option (list (ZRange.type.base.option.interp A))) _ | base.type.option A => @show_lvl (option (option (ZRange.type.base.option.interp A))) _ @@ -222,6 +219,7 @@ Module Compilers. Global Instance show_base : Show base.type.base := fun t => match t with | base.type.Z => "ℤ" + | base.type.positive => "ℤ⁺" | base.type.bool => "𝔹" | base.type.nat => "ℕ" | base.type.zrange => "zrange" @@ -246,6 +244,7 @@ Module Compilers. := match t with | base.type.Z => @show_lvl Z _ | base.type.bool => @show_lvl bool _ + | base.type.positive => @show_lvl positive _ | base.type.nat => @show_lvl nat _ | base.type.zrange => @show_lvl zrange _ | base.type.string => @show_lvl string _ @@ -398,6 +397,8 @@ Module Compilers. | ident.Nat_add => neg_wrap_parens "Nat.add" | ident.Nat_sub => neg_wrap_parens "Nat.sub" | ident.Nat_eqb => neg_wrap_parens "Nat.eqb" + | ident.Pos_mul => neg_wrap_parens "Pos.mul" + | ident.Pos_add => neg_wrap_parens "Pos.add" | ident.nil t => neg_wrap_parens "[]" | ident.cons t => fun _ => "(::)" | ident.pair A B => fun _ => "(,)" @@ -410,6 +411,15 @@ Module Compilers. | ident.eager_nat_rect P => neg_wrap_parens "eager_nat_rect" | ident.nat_rect_arrow P Q => neg_wrap_parens "nat_rect(→)" | ident.eager_nat_rect_arrow P Q => neg_wrap_parens "eager_nat_rect(→)" + (* + | @ident.nat_rect_fbb_b A B C => neg_wrap_parens "nat_rect_fbb_b" + | @ident.nat_rect_fbb_b_b A B C D => neg_wrap_parens "nat_rect_fbb_b_b" + | @ident.list_rect_fbb_b T A B C => neg_wrap_parens "list_rect_fbb_b" + | @ident.list_rect_fbb_b_b T A B C D => neg_wrap_parens "list_rect_fbb_b_b" + | @ident.list_rect_fbb_b_b_b T A B C D E => neg_wrap_parens "list_rect_fbb_b_b" + | @ident.list_rect_fbb_b_b_b_b T A B C D E F => neg_wrap_parens "list_rect_fbb_b_b" + | @ident.list_rect_fbb_b_b_b_b_b T A B C D E F G => neg_wrap_parens "list_rect_fbb_b_b" + *) | ident.list_rect A P => neg_wrap_parens "list_rect" | ident.eager_list_rect A P => neg_wrap_parens "eager_list_rect" | ident.list_rect_arrow A P Q => neg_wrap_parens "list_rect(→)" @@ -448,10 +458,13 @@ Module Compilers. | ident.Z_gtb => fun _ => "(>)" | ident.Z_min => neg_wrap_parens "min" | ident.Z_max => neg_wrap_parens "max" + | ident.Z_abs => neg_wrap_parens "abs" | ident.Z_log2 => neg_wrap_parens "log₂" | ident.Z_log2_up => neg_wrap_parens "⌈log₂⌉" | ident.Z_of_nat => fun _ => "(ℕ→ℤ)" | ident.Z_to_nat => fun _ => "(ℤ→ℕ)" + | ident.Z_pos => fun _ => "(ℤ⁺→ℤ)" + | ident.Z_to_pos => fun _ => "(ℤ→ℤ⁺)" | ident.Z_shiftr => fun _ => "(>>)" | ident.Z_shiftl => fun _ => "(<<)" | ident.Z_land => fun _ => "(&)" @@ -505,6 +518,8 @@ Module Compilers. ; ("+ℕ", (add_assoc, add_lvl)) ; ("-ℕ", (sub_assoc, sub_lvl)) ; ("=ℕ", (NoAssoc, Level.level 70)) + ; ("*ℤ⁺", (mul_assoc, mul_lvl)) + ; ("+ℤ⁺", (add_assoc, add_lvl)) ; ("::", (RightAssoc, Level.level 60)) ; ("++", (FullyAssoc, Level.level 60)) ; ("*", (mul_assoc, mul_lvl)) @@ -575,6 +590,8 @@ Module Compilers. | ident.Nat_add => "+ℕ" | ident.Nat_sub => "-ℕ" | ident.Nat_eqb => "=ℕ" + | ident.Pos_mul => "*ℤ⁺" + | ident.Pos_add => "+ℤ⁺" | ident.cons _ => "::" | ident.List_app _ => "++" | ident.Z_mul => "*" @@ -627,6 +644,8 @@ Module Compilers. | ident.Nat_add as idc | ident.Nat_sub as idc | ident.Nat_eqb as idc + | ident.Pos_mul as idc + | ident.Pos_add as idc | ident.cons _ as idc | ident.List_app _ as idc | ident.Z_mul as idc @@ -687,6 +706,15 @@ Module Compilers. | ident.eager_nat_rect _ as idc | ident.eager_nat_rect_arrow _ _ as idc | ident.nat_rect_arrow _ _ as idc + (* + | @ident.nat_rect_fbb_b _ _ _ as idc + | @ident.nat_rect_fbb_b_b _ _ _ _ as idc + | @ident.list_rect_fbb_b _ _ _ _ as idc + | @ident.list_rect_fbb_b_b _ _ _ _ _ as idc + | @ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc + | @ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc + | @ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ as idc + *) | ident.option_rect _ _ as idc | ident.list_rect _ _ as idc | ident.eager_list_rect _ _ as idc @@ -710,8 +738,11 @@ Module Compilers. | ident.Z_log2_up as idc | ident.Z_of_nat as idc | ident.Z_to_nat as idc + | ident.Z_pos as idc + | ident.Z_to_pos as idc | ident.Z_min as idc | ident.Z_max as idc + | ident.Z_abs as idc | ident.Z_mul_split as idc | ident.Z_mul_high as idc | ident.Z_add_get_carry as idc