Factor out rewriter rules

Move rewrite rule definitions, and the proofs about them, into separate
files.

We don't yet make use of the separate interp proofs of rewrite rules;
the next step is to refactor the interp proof machinery so that we can
easily prove the relevant interp relations, given the equality proofs in
`src/RewriterRulesProofs.v`

After     | File Name                                    | Before    || Change    | % Change
--------------------------------------------------------------------------------------------
23m01.93s | Total                                        | 22m37.08s || +0m24.84s | +1.83%
--------------------------------------------------------------------------------------------
0m24.10s  | RewriterRulesProofs.vo                       |    N/A    || +0m24.10s | ∞
1m12.13s  | Rewriter.vo                                  | 1m20.61s  || -0m08.48s | -10.51%
0m41.17s  | ExtractionHaskell/unsaturated_solinas        | 0m37.57s  || +0m03.60s | +9.58%
1m42.40s  | Fancy/Barrett256.vo                          | 1m40.22s  || +0m02.18s | +2.17%
0m45.56s  | p521_32.c                                    | 0m48.16s  || -0m02.59s | -5.39%
0m14.48s  | ExtractionOCaml/word_by_word_montgomery.ml   | 0m12.47s  || +0m02.00s | +16.11%
1m48.48s  | RewriterWf2.vo                               | 1m46.70s  || +0m01.77s | +1.66%
0m15.06s  | ExtractionOCaml/unsaturated_solinas          | 0m14.06s  || +0m01.00s | +7.11%
0m06.26s  | ExtractionHaskell/unsaturated_solinas.hs     | 0m07.29s  || -0m01.03s | -14.12%
0m04.71s  | ExtractionHaskell/saturated_solinas.hs       | 0m06.05s  || -0m01.33s | -22.14%
3m22.17s  | p384_32.c                                    | 3m23.06s  || -0m00.88s | -0.43%
1m57.31s  | RewriterRulesInterpGood.vo                   | 1m56.61s  || +0m00.70s | +0.60%
1m35.20s  | RewriterRulesGood.vo                         | 1m35.80s  || -0m00.59s | -0.62%
0m57.50s  | ExtractionHaskell/word_by_word_montgomery    | 0m56.53s  || +0m00.96s | +1.71%
0m45.71s  | RewriterInterpProofs1.vo                     | 0m46.13s  || -0m00.42s | -0.91%
0m39.66s  | p521_64.c                                    | 0m38.90s  || +0m00.75s | +1.95%
0m36.22s  | PushButtonSynthesis/UnsaturatedSolinas.vo    | 0m36.42s  || -0m00.20s | -0.54%
0m34.39s  | Fancy/Montgomery256.vo                       | 0m34.45s  || -0m00.06s | -0.17%
0m33.16s  | RewriterWf1.vo                               | 0m32.96s  || +0m00.19s | +0.60%
0m32.21s  | ExtractionHaskell/saturated_solinas          | 0m31.53s  || +0m00.67s | +2.15%
0m26.94s  | PushButtonSynthesis/WordByWordMontgomery.vo  | 0m27.20s  || -0m00.25s | -0.95%
0m25.89s  | SlowPrimeSynthesisExamples.vo                | 0m25.59s  || +0m00.30s | +1.17%
0m23.37s  | ExtractionOCaml/word_by_word_montgomery      | 0m22.90s  || +0m00.47s | +2.05%
0m21.19s  | PushButtonSynthesis/BarrettReduction.vo      | 0m20.79s  || +0m00.40s | +1.92%
0m18.30s  | p256_32.c                                    | 0m18.54s  || -0m00.23s | -1.29%
0m18.29s  | p448_solinas_64.c                            | 0m18.58s  || -0m00.28s | -1.56%
0m17.92s  | secp256k1_32.c                               | 0m18.41s  || -0m00.48s | -2.66%
0m14.06s  | p434_64.c                                    | 0m13.92s  || +0m00.14s | +1.00%
0m11.61s  | ExtractionOCaml/saturated_solinas            | 0m11.57s  || +0m00.03s | +0.34%
0m08.90s  | p224_32.c                                    | 0m09.12s  || -0m00.21s | -2.41%
0m08.49s  | ExtractionOCaml/unsaturated_solinas.ml       | 0m08.85s  || -0m00.35s | -4.06%
0m08.45s  | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.62s  || -0m00.16s | -1.97%
0m08.02s  | p384_64.c                                    | 0m07.04s  || +0m00.97s | +13.92%
0m07.01s  | ExtractionOCaml/saturated_solinas.ml         | 0m06.57s  || +0m00.43s | +6.69%
0m06.67s  | BoundsPipeline.vo                            | 0m06.87s  || -0m00.20s | -2.91%
0m03.39s  | PushButtonSynthesis/Primitives.vo            | 0m03.44s  || -0m00.04s | -1.45%
0m03.36s  | PushButtonSynthesis/SmallExamples.vo         | 0m03.38s  || -0m00.02s | -0.59%
0m03.23s  | PushButtonSynthesis/SaturatedSolinas.vo      | 0m03.21s  || +0m00.02s | +0.62%
0m03.04s  | curve25519_32.c                              | 0m02.68s  || +0m00.35s | +13.43%
0m02.74s  | PushButtonSynthesis/MontgomeryReduction.vo   | 0m02.55s  || +0m00.19s | +7.45%
0m02.19s  | curve25519_64.c                              | 0m01.81s  || +0m00.37s | +20.99%
0m01.72s  | secp256k1_64.c                               | 0m01.46s  || +0m00.26s | +17.80%
0m01.56s  | p256_64.c                                    | 0m01.22s  || +0m00.34s | +27.86%
0m01.49s  | p224_64.c                                    | 0m01.56s  || -0m00.07s | -4.48%
0m01.32s  | CLI.vo                                       | 0m01.32s  || +0m00.00s | +0.00%
0m01.14s  | StandaloneHaskellMain.vo                     | 0m01.08s  || +0m00.05s | +5.55%
0m01.06s  | CompilersTestCases.vo                        | 0m01.04s  || +0m00.02s | +1.92%
0m01.06s  | StandaloneOCamlMain.vo                       | 0m01.12s  || -0m00.06s | -5.35%
0m01.00s  | RewriterProofs.vo                            | 0m01.13s  || -0m00.12s | -11.50%
0m00.64s  | RewriterRules.vo                             |    N/A    || +0m00.64s | ∞

0 files changed, 0 insertions, 0 deletions