|
|
Other than the use of function extensionality in a particular place,
this completes the proofs of the rewriter.
It was rather painful to figure out the right way to phrase rewriter
correctness. I tried a number of more lax approaches (e.g., various
variants of saying what it means for two rawexprs to be equivalent,
saying what it means for two values to be equivalent, etc), but ran into
issues with incomparable relations. The right approach was to find the
most precise thing that could be said, and to relate each kind of thing
(rawexpr, value, expr, etc) to an interpreted value, and push that
around throughout the proof. The only exception to this pattern is
`eval_decision_tree`, for which a fine-grained notion of rawexpr
equivalence can be stated (basically, the equivalence-closure of the
reveal-rawexpr operation), and a couple of `Proper` lemmas can be proven
about this relation.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
22m34.75s | Total | 21m57.98s || +0m36.77s | +2.78%
--------------------------------------------------------------------------------------------------------------------
0m45.98s | Experiments/NewPipeline/RewriterInterpProofs1.vo | N/A || +0m45.97s | ∞
3m14.10s | p384_32.c | 3m20.53s || -0m06.43s | -3.20%
1m36.96s | Experiments/NewPipeline/Toplevel2.vo | 1m34.65s || +0m02.31s | +2.44%
0m29.87s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m31.03s || -0m01.16s | -3.73%
6m18.63s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.96s || -0m00.32s | -0.08%
4m40.50s | Experiments/NewPipeline/Toplevel1.vo | 4m40.32s || +0m00.18s | +0.06%
0m45.34s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m45.43s || -0m00.08s | -0.19%
0m44.53s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.71s || -0m00.17s | -0.40%
0m39.82s | p521_32.c | 0m39.83s || -0m00.00s | -0.02%
0m33.14s | p521_64.c | 0m33.22s || -0m00.07s | -0.24%
0m26.94s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m27.04s || -0m00.09s | -0.36%
0m23.22s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m23.82s || -0m00.60s | -2.51%
0m18.91s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m18.82s || +0m00.08s | +0.47%
0m14.02s | p256_32.c | 0m14.38s || -0m00.36s | -2.50%
0m13.92s | secp256k1_32.c | 0m14.42s || -0m00.50s | -3.46%
0m10.83s | p384_64.c | 0m10.97s || -0m00.14s | -1.27%
0m09.84s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m10.12s || -0m00.27s | -2.76%
0m06.58s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.62s || -0m00.04s | -0.60%
0m06.42s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m07.11s || -0m00.69s | -9.70%
0m06.37s | p224_32.c | 0m06.42s || -0m00.04s | -0.77%
0m05.02s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.92s || +0m00.09s | +2.03%
0m04.91s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || -0m00.60s | -11.05%
0m04.11s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.44s || -0m00.33s | -7.43%
0m02.21s | curve25519_32.c | 0m02.36s || -0m00.14s | -6.35%
0m02.08s | p224_64.c | 0m02.08s || +0m00.00s | +0.00%
0m01.94s | p256_64.c | 0m01.87s || +0m00.06s | +3.74%
0m01.87s | secp256k1_64.c | 0m02.07s || -0m00.19s | -9.66%
0m01.51s | curve25519_64.c | 0m01.54s || -0m00.03s | -1.94%
0m01.50s | Experiments/NewPipeline/CLI.vo | 0m01.42s || +0m00.08s | +5.63%
0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.04s | +3.20%
0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.22s || +0m00.06s | +4.91%
0m01.12s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.90s || +0m00.22s | +24.44%
|
Jason Gross