Add more identifiers for saturated solinas (mit-plv#1773)

For mit-plv#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 <[email protected]>

<details><summary>Timing Diff</summary>
<p>

```
    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%

```
</p>
</details>

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

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,14 +37,21 @@ 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
                            | apply ListUtil.list_case_Proper
                            | 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.