Split off all of the arithmetic rules that need bounds info

Because we need to do extra passes of DCE and subst01 to fully reduce
things, we generalize some of the interp proofs over cast behavior.

For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].

We also factor out the rewriting wrapper inside the pipeline module into
its own definition.

After     | File Name                                                            | Before    || Change    | % Change
---------------------------------------------------------------------------------------------------------------------
32m09.80s | Total                                                                | 26m07.22s || +6m02.58s | +23.13%
---------------------------------------------------------------------------------------------------------------------
6m41.53s  | p384_32.c                                                            | 0m28.22s  || +6m13.30s | +1322.85%
1m19.67s  | Experiments/NewPipeline/Rewriter.vo                                  | 2m22.97s  || -1m03.29s | -44.27%
0m21.90s  | secp256k1_32.c                                                       | 0m06.46s  || +0m15.43s | +239.00%
0m21.24s  | p256_32.c                                                            | 0m06.32s  || +0m14.91s | +236.07%
6m18.26s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m13.65s  || +0m04.61s | +1.23%
0m14.12s  | p384_64.c                                                            | 0m10.22s  || +0m03.89s | +38.16%
0m07.86s  | p224_32.c                                                            | 0m03.92s  || +0m03.94s | +100.51%
4m34.19s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m37.15s  || -0m02.95s | -1.06%
1m41.50s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m38.62s  || +0m02.87s | +2.92%
0m37.69s  | p521_64.c                                                            | 0m35.62s  || +0m02.07s | +5.81%
0m29.75s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m27.09s  || +0m02.66s | +9.81%
0m17.88s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m15.52s  || +0m02.35s | +15.20%
1m47.75s  | Experiments/NewPipeline/RewriterRulesInterpGood.vo                   | 1m46.74s  || +0m01.00s | +0.94%
0m44.38s  | p521_32.c                                                            | 0m42.47s  || +0m01.91s | +4.49%
0m43.92s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m41.97s  || +0m01.95s | +4.64%
0m24.99s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m26.52s  || -0m01.53s | -5.76%
0m20.62s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m22.26s  || -0m01.64s | -7.36%
0m11.42s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m12.88s  || -0m01.46s | -11.33%
0m08.44s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m07.12s  || +0m01.31s | +18.53%
1m50.48s  | Experiments/NewPipeline/RewriterWf2.vo                               | 1m50.18s  || +0m00.29s | +0.27%
1m15.53s  | Experiments/NewPipeline/RewriterRulesGood.vo                         | 1m15.26s  || +0m00.26s | +0.35%
0m43.94s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m43.00s  || +0m00.93s | +2.18%
0m10.25s  | Experiments/NewPipeline/RewriterWf1.vo                               | 0m10.46s  || -0m00.21s | -2.00%
0m07.27s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m07.41s  || -0m00.14s | -1.88%
0m06.29s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m05.75s  || +0m00.54s | +9.39%
0m05.54s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m06.24s  || -0m00.70s | -11.21%
0m04.86s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m05.62s  || -0m00.75s | -13.52%
0m02.86s  | curve25519_32.c                                                      | 0m02.43s  || +0m00.42s | +17.69%
0m02.80s  | secp256k1_64.c                                                       | 0m02.29s  || +0m00.50s | +22.27%
0m02.74s  | p256_64.c                                                            | 0m02.67s  || +0m00.07s | +2.62%
0m02.13s  | curve25519_64.c                                                      | 0m02.38s  || -0m00.25s | -10.50%
0m01.97s  | p224_64.c                                                            | 0m01.86s  || +0m00.10s | +5.91%
0m01.46s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.52s  || -0m00.06s | -3.94%
0m01.36s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.25s  || +0m00.11s | +8.80%
0m01.22s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.19s  || +0m00.03s | +2.52%
0m01.02s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m01.05s  || -0m00.03s | -2.85%
0m00.97s  | Experiments/NewPipeline/RewriterProofs.vo                            | 0m00.94s  || +0m00.03s | +3.19%

0 files changed, 0 insertions, 0 deletions