| Commit message (Expand) | Author | Age |
... | |
* | | Update README.md | Jason Gross | 2019-01-05 |
* | | prove admit | Andres Erbsen | 2019-01-05 |
* | | build on Coq master | Andres Erbsen | 2019-01-05 |
* | | new pipeline: refactor glue, split into more files | Jason Gross | 2019-01-05 |
| * | Update fancy rewriter output with new compilation output | Jason Gross | 2019-01-03 |
| * | Finish proving fancy rewrite rules | Jason Gross | 2019-01-03 |
| * | Fix bounds checking on shift | Jason Gross | 2019-01-03 |
| * | comment out broken code so things build | jadep | 2019-01-03 |
| * | try to fix fancy rewrite rules; current output is incorrect | jadep | 2019-01-03 |
| * | WIP | jadep | 2019-01-03 |
| * | remove dead code | jadep | 2019-01-03 |
| * | remove whitespace, print statements, and some dead tactics | jadep | 2019-01-03 |
| * | fixed up some of the fancy rewrite rules | jadep | 2019-01-03 |
| * | WIP: prove that barrett_red256 is a valid expression modulo some issues with ... | jadep | 2019-01-03 |
| * | WIP: expand valid_ident and prove of_prefancy_correct using it | jadep | 2019-01-03 |
| * | WIP : made everything more concrete and proved of_Expr. Still to do for of_Ex... | jadep | 2019-01-03 |
| * | WIP | jadep | 2019-01-03 |
| * | WIP | jadep | 2019-01-03 |
| * | WIP | jadep | 2019-01-03 |
| * | WIP | jadep | 2019-01-03 |
|/ |
|
* | Prove that convert_bases partitions | Jason Gross | 2019-01-03 |
* | Do not rely on `Refine Instance Mode` | Maxime Dénès | 2019-01-02 |
* | Remove WBW Mont lemmas from push_eval | Jason Gross | 2018-12-26 |
* | Add eval_* lemmas for WBW Mont Arith operations | Jason Gross | 2018-12-26 |
* | Move le_{add,sub}_1_* to ZUtil.Le | Jason Gross | 2018-12-25 |
* | from_montgomery{_ => }mod, for consistency with other naming | Jason Gross | 2018-12-24 |
* | Add correctness in arithmetic for mulx, addcarryx, subborrowx | Jason Gross | 2018-12-21 |
* | Add has_body tactic | Jason Gross | 2018-12-21 |
* | Add eval_freeze_to_bytesmod to push_eval | Jason Gross | 2018-12-21 |
* | Add length_encode_no_reduce to distr_length | Jason Gross | 2018-12-21 |
* | Add `Proof using` directives in Arithmetic | Jason Gross | 2018-12-21 |
* | Fix a few minor things in Arithmetic | Jason Gross | 2018-12-21 |
* | remove unneeded lemma and do some micro-performance-optimization at one stick... | jadep | 2018-12-21 |
* | remove proof duplication | jadep | 2018-12-21 |
* | fix hints and [Proof using] statements so that proofs go through | jadep | 2018-12-21 |
* | prove [small_sub_then_maybe_add] | jadep | 2018-12-21 |
* | prove [eval_sub_then_maybe_add] | jadep | 2018-12-21 |
* | fix hints and [Proof using] statements so that proofs go through | jadep | 2018-12-21 |
* | prove [small_conditional_sub] | jadep | 2018-12-21 |
* | prove [eval_conditional_sub] | jadep | 2018-12-21 |
* | move weight proofs up above Positional so they can be used to prove eval_drop... | jadep | 2018-12-21 |
* | modify a proof because in 8.7 [auto] doesn't solve the goal | jadep | 2018-12-21 |
* | prove admit | jadep | 2018-12-21 |
* | prove admit | jadep | 2018-12-21 |
* | Add Wf_reify | Jason Gross | 2018-12-20 |
* | Add Wf_APP, Interp_reify | Jason Gross | 2018-12-20 |
* | Remove glue admits in Toplevel1 | Jason Gross | 2018-12-20 |
* | Add uweight_partition_unique, move weight_1 to uweight_1, add Positional.eval... | Jason Gross | 2018-12-20 |
* | Finish rewriter proofs modulo funext | Jason Gross | 2018-12-19 |
* | Add eq_subst_types_pattern_collect_vars_empty_iff | Jason Gross | 2018-12-18 |