From d2bc871618c98b6e85e4e384eb61dc6dc49e7dbf Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 14 Dec 2018 18:12:56 -0500 Subject: Finish rewriter proofs modulo funext MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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% --- _CoqProject | 1 + 1 file changed, 1 insertion(+) (limited to '_CoqProject') diff --git a/_CoqProject b/_CoqProject index 9fdef01d8..4dec8ffeb 100644 --- a/_CoqProject +++ b/_CoqProject @@ -262,6 +262,7 @@ src/Experiments/NewPipeline/LanguageWf.v src/Experiments/NewPipeline/MiscCompilerPasses.v src/Experiments/NewPipeline/MiscCompilerPassesProofs.v src/Experiments/NewPipeline/Rewriter.v +src/Experiments/NewPipeline/RewriterInterpProofs1.v src/Experiments/NewPipeline/RewriterProofs.v src/Experiments/NewPipeline/RewriterRulesGood.v src/Experiments/NewPipeline/RewriterRulesInterpGood.v -- cgit v1.2.3