| Commit message (Collapse) | Author | Age |
... | |
|
|
|
| |
autorewrite is slow and not customiziable enough.
|
|
|
|
|
| |
This allows us to push the evaluations with just `autorewrite with
push_eval`
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
sticky point
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
eval_drop_high_to_length
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
20m47.54s | Total | 20m48.81s || -0m01.26s | -0.10%
--------------------------------------------------------------------------------------------------------------------
3m14.11s | p384_32.c | 3m19.20s || -0m05.08s | -2.55%
6m18.53s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m14.62s || +0m03.90s | +1.04%
4m38.90s | Experiments/NewPipeline/Toplevel1.vo | 4m37.97s || +0m00.92s | +0.33%
1m36.44s | Experiments/NewPipeline/Toplevel2.vo | 1m36.23s || +0m00.21s | +0.21%
0m44.38s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.09s || +0m00.28s | +0.65%
0m39.93s | p521_32.c | 0m40.58s || -0m00.64s | -1.60%
0m32.86s | p521_64.c | 0m33.84s || -0m00.98s | -2.89%
0m29.52s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.66s || -0m00.14s | -0.47%
0m22.76s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.88s || -0m00.11s | -0.52%
0m16.76s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.66s || +0m00.10s | +0.60%
0m14.01s | secp256k1_32.c | 0m14.03s || -0m00.01s | -0.14%
0m13.88s | p256_32.c | 0m13.79s || +0m00.09s | +0.65%
0m10.63s | p384_64.c | 0m10.67s || -0m00.03s | -0.37%
0m10.16s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.07s || +0m00.08s | +0.89%
0m09.76s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.92s || -0m00.16s | -1.61%
0m07.83s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.65s || +0m00.17s | +2.35%
0m06.60s | p224_32.c | 0m06.35s || +0m00.25s | +3.93%
0m06.54s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.48s || +0m00.05s | +0.92%
0m06.42s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.40s || +0m00.01s | +0.31%
0m04.99s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.94s || +0m00.04s | +1.01%
0m04.92s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.96s || -0m00.04s | -0.80%
0m04.12s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.06s || +0m00.06s | +1.47%
0m02.40s | curve25519_32.c | 0m02.40s || +0m00.00s | +0.00%
0m01.90s | p224_64.c | 0m02.02s || -0m00.12s | -5.94%
0m01.84s | p256_64.c | 0m01.83s || +0m00.01s | +0.54%
0m01.84s | secp256k1_64.c | 0m01.84s || +0m00.00s | +0.00%
0m01.48s | Experiments/NewPipeline/CLI.vo | 0m01.48s || +0m00.00s | +0.00%
0m01.48s | curve25519_64.c | 0m01.63s || -0m00.14s | -9.20%
0m01.28s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.24s || +0m00.04s | +3.22%
0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.32s || -0m00.04s | -3.03%
|
|
|
|
|
|
| |
Positional.eval_mul_each
uweight_partition_unique can probably be generalized to not be specific to uniform weights, but that is left to a future person.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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%
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This is needed to handle exprs whose var types are value
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Now they are all actually proven.
We also add zrange arguments for value and flag, in preparation for
things Jade wants to do.
Unfortunately, some things got much slower, because the rewriter
meta-compilation phase is nonlinear in the number of rewrite rules.
After | File Name | Before || Change | % Change
--------------------------------------------------------------------------------------------------------------------
29m31.98s | Total | 26m34.58s || +2m57.39s | +11.12%
--------------------------------------------------------------------------------------------------------------------
2m06.72s | Experiments/NewPipeline/Rewriter.vo | 0m34.70s || +1m32.01s | +265.18%
1m44.58s | Experiments/NewPipeline/RewriterRulesGood.vo | 0m55.12s || +0m49.46s | +89.73%
1m51.98s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m47.38s || +0m04.59s | +4.28%
0m44.83s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m40.58s || +0m04.25s | +10.47%
0m29.46s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m24.94s || +0m04.51s | +18.12%
0m26.62s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m21.95s || +0m04.67s | +21.27%
0m22.75s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m18.07s || +0m04.67s | +25.89%
0m18.44s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m13.97s || +0m04.47s | +31.99%
0m43.64s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m40.11s || +0m03.53s | +8.80%
1m58.64s | Experiments/NewPipeline/RewriterWf2.vo | 1m55.94s || +0m02.70s | +2.32%
6m13.06s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m11.83s || +0m01.23s | +0.33%
4m37.06s | Experiments/NewPipeline/Toplevel1.vo | 4m38.14s || -0m01.07s | -0.38%
3m13.92s | p384_32.c | 3m15.11s || -0m01.19s | -0.60%
1m32.26s | Experiments/NewPipeline/Toplevel2.vo | 1m31.34s || +0m00.91s | +1.00%
0m39.36s | p521_32.c | 0m39.90s || -0m00.53s | -1.35%
0m32.61s | p521_64.c | 0m33.49s || -0m00.88s | -2.62%
0m19.77s | Experiments/NewPipeline/RewriterWf1.vo | 0m19.44s || +0m00.32s | +1.69%
0m13.76s | secp256k1_32.c | 0m13.43s || +0m00.33s | +2.45%
0m13.50s | p256_32.c | 0m13.55s || -0m00.05s | -0.36%
0m10.64s | p384_64.c | 0m10.62s || +0m00.02s | +0.18%
0m09.70s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.04s || +0m00.66s | +7.30%
0m06.47s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.05s || +0m00.41s | +6.94%
0m06.39s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.87s || +0m00.51s | +8.85%
0m06.24s | p224_32.c | 0m06.23s || +0m00.00s | +0.16%
0m04.98s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.47s || +0m00.51s | +11.40%
0m04.88s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.26s || +0m00.62s | +14.55%
0m04.08s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.58s || +0m00.50s | +13.96%
0m02.22s | curve25519_32.c | 0m02.37s || -0m00.14s | -6.32%
0m02.04s | p224_64.c | 0m01.92s || +0m00.12s | +6.25%
0m01.99s | secp256k1_64.c | 0m01.91s || +0m00.08s | +4.18%
0m01.84s | p256_64.c | 0m02.01s || -0m00.16s | -8.45%
0m01.50s | curve25519_64.c | 0m01.49s || +0m00.01s | +0.67%
0m01.42s | Experiments/NewPipeline/CLI.vo | 0m01.42s || +0m00.00s | +0.00%
0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.27s || +0m00.02s | +1.57%
0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.23s || +0m00.03s | +2.43%
0m01.12s | Experiments/NewPipeline/CompilersTestCases.vo | 0m00.92s || +0m00.20s | +21.73%
0m00.96s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.94s || +0m00.02s | +2.12%
|
| |
|
| |
|
|
|
|
| |
This way we have access to the hypothesis that the types are in the evar map, when doing the proofs
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
It was not serving any good purpose, and was interfering with proofs.
Any type variable that appears in an identifier's arguments will
either (a) show up in the type of the identifier, (b) show up in
another type somewhere else in the pattern, or (c) not be needed to
well-type anything that is not an argument to that identifier. (There
is actually a case (d), where the type variable shows up in the
arguments to another identifier but no-where else, but I'll get to
that in a moment.) In case (a), the type-unification will pick it up
automatically. In case (b), pattern-type unification elsewhere will
pick up that type variable. And in case (c), it is the responsibility
of the function that describes the arguments to the identifier to
handle any dependencies. Case (d), where there is non-linear matching
on identifier type-arguments, is now forbidden; we will allow the
author of the rewrite-rule to deal with such equalities manually.
This allows some proofs about type unification to actually go through
now.
|
|
|
|
| |
This makes it much easier to read goals involving these combinators.
|
| |
|
| |
|
| |
|