aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* WIPGravatar jadep2019-01-03
|
* remove dead codeGravatar jadep2019-01-03
|
* remove whitespace, print statements, and some dead tacticsGravatar jadep2019-01-03
|
* fixed up some of the fancy rewrite rulesGravatar jadep2019-01-03
|
* WIP: prove that barrett_red256 is a valid expression modulo some issues with ↵Gravatar jadep2019-01-03
| | | | rewrite rules (too-tight bound on RSHI and ADDC (0,x,y) not being converted to ADD (x,y)
* WIP: expand valid_ident and prove of_prefancy_correct using itGravatar jadep2019-01-03
|
* WIP : made everything more concrete and proved of_Expr. Still to do for ↵Gravatar jadep2019-01-03
| | | | of_Expr : expand valid_ident
* WIPGravatar jadep2019-01-03
|
* WIPGravatar jadep2019-01-03
|
* WIPGravatar jadep2019-01-03
|
* WIPGravatar jadep2019-01-03
|
* Prove that convert_bases partitionsGravatar Jason Gross2019-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unfortunately, the proof is rather slow :-( After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 22m46.26s | Total | 22m03.36s || +0m42.90s | +3.24% -------------------------------------------------------------------------------------------------------------------- 1m57.06s | Experiments/NewPipeline/Arithmetic.vo | 1m15.08s || +0m41.98s | +55.91% 0m42.39s | p521_32.c | 0m39.92s || +0m02.46s | +6.18% 0m35.40s | p521_64.c | 0m33.02s || +0m02.37s | +7.20% 3m15.80s | p384_32.c | 3m17.10s || -0m01.29s | -0.65% 6m19.46s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.91s || +0m00.54s | +0.14% 4m34.80s | Experiments/NewPipeline/Toplevel1.vo | 4m35.56s || -0m00.75s | -0.27% 1m36.64s | Experiments/NewPipeline/Toplevel2.vo | 1m36.64s || +0m00.00s | +0.00% 0m43.22s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.18s || -0m00.96s | -2.17% 0m29.24s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.83s || -0m00.58s | -1.97% 0m22.83s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.87s || -0m00.04s | -0.17% 0m16.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.73s || -0m00.62s | -3.70% 0m14.24s | p256_32.c | 0m13.75s || +0m00.49s | +3.56% 0m14.22s | secp256k1_32.c | 0m14.19s || +0m00.03s | +0.21% 0m11.01s | p384_64.c | 0m10.50s || +0m00.50s | +4.85% 0m09.71s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.86s || -0m00.14s | -1.52% 0m09.69s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.35s || -0m00.66s | -6.37% 0m07.41s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.74s || -0m00.33s | -4.26% 0m06.65s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.52s || +0m00.13s | +1.99% 0m06.50s | p224_32.c | 0m06.47s || +0m00.03s | +0.46% 0m06.24s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.38s || -0m00.13s | -2.19% 0m05.10s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.97s || +0m00.12s | +2.61% 0m04.82s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.04s || -0m00.21s | -4.36% 0m03.95s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.02s || -0m00.06s | -1.74% 0m02.31s | curve25519_32.c | 0m02.24s || +0m00.06s | +3.12% 0m02.03s | p224_64.c | 0m01.92s || +0m00.10s | +5.72% 0m01.91s | secp256k1_64.c | 0m02.00s || -0m00.09s | -4.50% 0m01.90s | p256_64.c | 0m01.86s || +0m00.03s | +2.15% 0m01.54s | curve25519_64.c | 0m01.61s || -0m00.07s | -4.34% 0m01.51s | Experiments/NewPipeline/CLI.vo | 0m01.49s || +0m00.02s | +1.34% 0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.29s || +0m00.00s | +0.00% 0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.32s || -0m00.04s | -3.03%
* Do not rely on `Refine Instance Mode`Gravatar Maxime Dénès2019-01-02
| | | | | This option is soon going to be turned off by default. See https://github.com/coq/coq/pull/9270
* Remove WBW Mont lemmas from push_evalGravatar Jason Gross2018-12-26
| | | | autorewrite is slow and not customiziable enough.
* Add eval_* lemmas for WBW Mont Arith operationsGravatar Jason Gross2018-12-26
| | | | | This allows us to push the evaluations with just `autorewrite with push_eval`
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
|
* from_montgomery{_ => }mod, for consistency with other namingGravatar Jason Gross2018-12-24
|
* Add correctness in arithmetic for mulx, addcarryx, subborrowxGravatar Jason Gross2018-12-21
|
* Add has_body tacticGravatar Jason Gross2018-12-21
|
* Add eval_freeze_to_bytesmod to push_evalGravatar Jason Gross2018-12-21
|
* Add length_encode_no_reduce to distr_lengthGravatar Jason Gross2018-12-21
|
* Add `Proof using` directives in ArithmeticGravatar Jason Gross2018-12-21
|
* Fix a few minor things in ArithmeticGravatar Jason Gross2018-12-21
|
* remove unneeded lemma and do some micro-performance-optimization at one ↵Gravatar jadep2018-12-21
| | | | sticky point
* remove proof duplicationGravatar jadep2018-12-21
|
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
|
* prove [small_sub_then_maybe_add]Gravatar jadep2018-12-21
|
* prove [eval_sub_then_maybe_add]Gravatar jadep2018-12-21
|
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
|
* prove [small_conditional_sub]Gravatar jadep2018-12-21
|
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
|
* move weight proofs up above Positional so they can be used to prove ↵Gravatar jadep2018-12-21
| | | | eval_drop_high_to_length
* modify a proof because in 8.7 [auto] doesn't solve the goalGravatar jadep2018-12-21
|
* prove admitGravatar jadep2018-12-21
|
* prove admitGravatar jadep2018-12-21
|
* Add Wf_reifyGravatar Jason Gross2018-12-20
|
* Add Wf_APP, Interp_reifyGravatar Jason Gross2018-12-20
|
* Remove glue admits in Toplevel1Gravatar Jason Gross2018-12-20
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Update .travis.ymlGravatar Jason Gross2018-12-20
| | | | Update 8.8.0 to 8.8.2, add v8.9 branch
* Add uweight_partition_unique, move weight_1 to uweight_1, add ↵Gravatar Jason Gross2018-12-20
| | | | | | 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.
* Finish rewriter proofs modulo funextGravatar Jason Gross2018-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Add eq_subst_types_pattern_collect_vars_empty_iffGravatar Jason Gross2018-12-18
|
* Add rawexpr_types_okGravatar Jason Gross2018-12-14
|
* Fix an issue with setoid_rewrite being weaker before 8.9Gravatar Jason Gross2018-12-14
|
* Add reify_and_let_binds_base_interp_relatedGravatar Jason Gross2018-12-14
|
* add interp_related_gen_of_wfGravatar Jason Gross2018-12-12
|
* Remove useless assumptionsGravatar Jason Gross2018-12-12
|
* Generalize expr.interp_relatedGravatar Jason Gross2018-12-12
| | | | This is needed to handle exprs whose var types are value
* Move fancy rewrites after bounds analysisGravatar Jason Gross2018-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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%
* Fix a bug in 0672c92921e45b942fa8a75c45457b8c7b32565dGravatar Jason Gross2018-12-12
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 21:27:17 +0000