aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* 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%
* 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
|
* Add type.eq_subst_types_pattern_collect_varsGravatar Jason Gross2018-12-12
|
* Make unify_pattern' a bit stricterGravatar Jason Gross2018-12-12
| | | | This way we have access to the hypothesis that the types are in the evar map, when doing the proofs
* Add projT1_app_with_unification_resultTGravatar Jason Gross2018-12-12
|
* Add rawexpr_interp_related_Proper_rawexpr_equiv_rew_genGravatar Jason Gross2018-12-12
|
* Add ZRange.cc_m, ZRange.is_bounded_by_bool_cc_mGravatar Jason Gross2018-12-11
|
* Add ZRange.is_bounded_by_bool_normalize_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.normalize_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.is_bounded_by_bool_constantGravatar Jason Gross2018-12-11
|
* Add ZRange.OperationBoundsGravatar Jason Gross2018-12-11
|
* remove pattern.ident.type_varsGravatar Jason Gross2018-12-11
| | | | | | | | | | | | | | | | | | | 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.
* Use Fixpoint, not list_rect, for {app,lam}_forall_varsGravatar Jason Gross2018-12-11
| | | | This makes it much easier to read goals involving these combinators.
* Add In_elements_mem_iffGravatar Jason Gross2018-12-11
|
* Add eqv_iff_eq_of_funextGravatar Jason Gross2018-12-11
|
* Prove pattern.ident.type_vars_enoughGravatar Jason Gross2018-12-08
|
* Add value_of_rawexpr_interp_relatedGravatar Jason Gross2018-12-07
|
* Switch to a more precise version of interp_related for rewritesGravatar Jason Gross2018-12-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This version is hopefully the right one. It seems to be basically exactly what we want to say, and no more and no less. The rule for let-ins, which is almost the only freedom we have here, is chosen to match exactly with the rule for App+Abs. Note that using Leibniz equality is essential in the places where it's used. The recursive relation here might actually be a bit clearer as an inductive relation, but I wanted it to simplify under reduction. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 30m04.79s | Total | 29m51.25s || +0m13.54s | +0.75% -------------------------------------------------------------------------------------------------------------------- 1m53.11s | Experiments/NewPipeline/RewriterRulesInterpGood.vo | 1m35.74s || +0m17.36s | +18.14% 0m19.40s | Experiments/NewPipeline/RewriterWf1.vo | 0m24.54s || -0m05.14s | -20.94% 6m13.78s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m14.86s || -0m01.08s | -0.28% 4m39.23s | Experiments/NewPipeline/Toplevel1.vo | 4m38.21s || +0m01.02s | +0.36% 1m31.62s | Experiments/NewPipeline/Toplevel2.vo | 1m32.68s || -0m01.06s | -1.14% 0m40.01s | Experiments/NewPipeline/AbstractInterpretationWf.vo | 0m38.77s || +0m01.23s | +3.19% 3m19.74s | p384_32.c | 3m19.71s || +0m00.03s | +0.01% 1m58.86s | Experiments/NewPipeline/RewriterWf2.vo | 1m58.30s || +0m00.56s | +0.47% 1m02.04s | Experiments/NewPipeline/RewriterRulesGood.vo | 1m02.41s || -0m00.36s | -0.59% 0m40.71s | p521_32.c | 0m40.51s || +0m00.20s | +0.49% 0m39.90s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m39.85s || +0m00.04s | +0.12% 0m36.76s | Experiments/NewPipeline/Rewriter.vo | 0m36.81s || -0m00.05s | -0.13% 0m35.34s | Experiments/NewPipeline/LanguageInversion.vo | 0m35.16s || +0m00.18s | +0.51% 0m33.80s | p521_64.c | 0m33.82s || -0m00.02s | -0.05% 0m28.97s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo | 0m29.54s || -0m00.57s | -1.92% 0m27.65s | Experiments/NewPipeline/LanguageWf.vo | 0m28.11s || -0m00.46s | -1.63% 0m25.94s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m25.39s || +0m00.55s | +2.16% 0m25.63s | Experiments/NewPipeline/UnderLetsProofs.vo | 0m25.15s || +0m00.48s | +1.90% 0m22.84s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs.vo | 0m23.11s || -0m00.26s | -1.16% 0m18.51s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m18.69s || -0m00.17s | -0.96% 0m17.42s | Experiments/NewPipeline/AbstractInterpretationProofs.vo | 0m17.29s || +0m00.13s | +0.75% 0m15.12s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m14.96s || +0m00.15s | +1.06% 0m14.43s | secp256k1_32.c | 0m14.22s || +0m00.20s | +1.47% 0m14.19s | p256_32.c | 0m14.46s || -0m00.27s | -1.86% 0m12.72s | Experiments/NewPipeline/CStringification.vo | 0m12.80s || -0m00.08s | -0.62% 0m10.88s | p384_64.c | 0m10.99s || -0m00.10s | -1.00% 0m09.16s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m08.87s || +0m00.29s | +3.26% 0m09.14s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.33s || -0m00.18s | -2.03% 0m07.96s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo | 0m07.96s || +0m00.00s | +0.00% 0m06.61s | p224_32.c | 0m06.52s || +0m00.09s | +1.38% 0m06.37s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.29s || +0m00.08s | +1.27% 0m05.96s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m05.60s || +0m00.36s | +6.42% 0m05.92s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.82s || +0m00.09s | +1.71% 0m04.70s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.35s || +0m00.35s | +8.04% 0m04.50s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.63s || -0m00.12s | -2.80% 0m03.82s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.62s || +0m00.19s | +5.52% 0m02.62s | Experiments/NewPipeline/MiscCompilerPassesProofs.vo | 0m02.56s || +0m00.06s | +2.34% 0m02.31s | curve25519_32.c | 0m02.40s || -0m00.08s | -3.74% 0m02.09s | secp256k1_64.c | 0m02.18s || -0m00.09s | -4.12% 0m02.05s | p224_64.c | 0m02.04s || +0m00.00s | +0.49% 0m01.96s | p256_64.c | 0m01.94s || +0m00.02s | +1.03% 0m01.56s | curve25519_64.c | 0m01.54s || +0m00.02s | +1.29% 0m01.53s | Experiments/NewPipeline/CLI.vo | 0m01.57s || -0m00.04s | -2.54% 0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.26s || +0m00.00s | +0.00% 0m01.22s | Experiments/NewPipeline/Language.vo | 0m01.26s || -0m00.04s | -3.17% 0m01.22s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.21s || +0m00.01s | +0.82% 0m01.08s | Experiments/NewPipeline/CompilersTestCases.vo | 0m00.99s || +0m00.09s | +9.09% 0m01.06s | Experiments/NewPipeline/AbstractInterpretation.vo | 0m01.02s || +0m00.04s | +3.92% 0m00.87s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.97s || -0m00.09s | -10.30% 0m00.74s | Experiments/NewPipeline/MiscCompilerPasses.vo | 0m00.72s || +0m00.02s | +2.77% 0m00.48s | Experiments/NewPipeline/UnderLets.vo | 0m00.52s || -0m00.04s | -7.69%
* Add Forall2_update_nthGravatar Jason Gross2018-12-06
|
* Fix broken proofsGravatar Jason Gross2018-12-04
|
* Add more Forall2 lemmasGravatar Jason Gross2018-12-04
|
* Add more ListUtil Forall LemmasGravatar Jason Gross2018-12-04
|
* Yet more repeat fixingGravatar Jason Gross2018-12-04
|
* More repeat fixingGravatar Jason Gross2018-12-04
|
* Add some ListUtil lemmas about Forall2Gravatar Jason Gross2018-12-04
|
* Fix bugs introduced by previous commitGravatar Jason Gross2018-12-04
|
* Remove ListUtil.List.repeatGravatar Jason Gross2018-12-04
| | | | | We are no longer checking against Coq 8.5, and it's simpler to not have two versions of `List.repeat` floating around.
* Revert "Add inversion_clear tactics"Gravatar Jason Gross2018-12-04
| | | | | | This reverts commit e6044c2fe0cc7b5662076bb1f26342a4d590132e. Actually not needed; the tactics already clear the relevant hypotheses.
* Add inversion_clear tacticsGravatar Jason Gross2018-12-04
|
* Add value_or_expr_interp_okGravatar Jason Gross2018-11-29
|
* Add unfold_value'_interp_arrowGravatar Jason Gross2018-11-28
|
* Add value_interp_ok_{arrow,base}Gravatar Jason Gross2018-11-28
|
* Add some more rawexpr equiv lemmasGravatar Jason Gross2018-11-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 09:20:53 +0000