| Commit message (Expand) | Author | Age |
* | Moved a tactic to Util/Tactics.v | jadep | 2016-08-24 |
* | Merge. | jadep | 2016-08-21 |
|\ |
|
* | | Proved some leftover admits in Pow2BaseProofs.v | jadep | 2016-08-21 |
* | | Finished [split_index] proofs and reworked conversion proofs to match. | jadep | 2016-08-21 |
| * | More 8.4 Admitted fixes | Jason Gross | 2016-08-17 |
| * | More fixes for 8.4 | Jason Gross | 2016-08-17 |
|/ |
|
* | More 8.4 compat | Jason Gross | 2016-08-16 |
* | Fixes for Coq 8.4 | Jason Gross | 2016-08-16 |
* | Add some list util, and decode'_map_mul | Jason Gross | 2016-08-16 |
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-08-16 |
|\ |
|
* \ | Merge of conversion development branch with master | jadep | 2016-08-16 |
|\ \ |
|
| | * | Add decode_shift_app | Jason Gross | 2016-08-16 |
| |/
|/| |
|
| * | Pow2BaseProofs.v : removed Z lemmas that are now in ZUtil, updated the way [c... | jadep | 2016-08-16 |
* | | Factor decode_shift_uniform | Jason Gross | 2016-08-15 |
| * | Proved remaining lemmas directly about conversion loop; still need to prove l... | jadep | 2016-08-14 |
| * | Conversion: main step proof done | jadep | 2016-08-13 |
* | | Add decode_nonneg | Jason Gross | 2016-08-12 |
* | | Add upper_bound_uniform | Jason Gross | 2016-08-12 |
* | | Weaker UniformBase assumptions | Jason Gross | 2016-08-12 |
* | | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-08-12 |
|\ \ |
|
* | | | added convenience lemma about [bounded] and [upper_bound] in Pow2BaseProofs.v | jadep | 2016-08-12 |
| | * | New and improved conversion proofs (final conditions proven, invariant step u... | jadep | 2016-08-12 |
| |/
|/| |
|
| * | Don't take advantage of design flaws (auto with *) | Jason Gross | 2016-08-11 |
|/ |
|
* | merge | jadep | 2016-08-11 |
|\ |
|
* | | Tweaks for 8.4 compatibility | jadep | 2016-08-11 |
* | | Removed old conversion cruft and fixed Testbit to fit new decode_bitwise proofs | jadep | 2016-08-11 |
* | | removed defunct lemmas/admits, proved helper function for conversion is correct | jadep | 2016-08-10 |
| * | Add ext_limb_widths_upper_bound | Jason Gross | 2016-08-10 |
* | | Made decode_bitwise proofs go away, and proved sane lemmas about Z.testbit (B... | jadep | 2016-08-10 |
* | | Convert defined and mostly proven, modulo several admitted lemmas about Z ope... | jadep | 2016-08-09 |
|/ |
|
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-07-25 |
|\ |
|
* | | Put ModularBaseSystem carries in terms of [carry_gen], and pushed this change... | jadep | 2016-07-25 |
| * | Make the library 20% faster: [auto with *] is evil | Jason Gross | 2016-07-22 |
|/ |
|
* | Changed name of [carry_and_reduce_single] to [carry_single], since it does no... | jadep | 2016-07-21 |
* | merge | jadep | 2016-07-20 |
|\ |
|
| * | Remove stuff from PseudoMersenneBaseParamProofs.v | Jason Gross | 2016-07-19 |
| * | Fix side-condition from previous commit | Jason Gross | 2016-07-19 |
| * | Add another lemma to distr_length | Jason Gross | 2016-07-19 |
* | | merge | jadep | 2016-07-19 |
|\| |
|
* | | merge | jadep | 2016-07-19 |
|\ \ |
|
| | * | Add a lemma about base_from_limb_widths and app | Jason Gross | 2016-07-18 |
| | * | Make Pow2BaseProofs independent of the def of add_to_nth | Jason Gross | 2016-07-18 |
| | * | Express carry_simple in terms of carry_gen | Jason Gross | 2016-07-18 |
| |/ |
|
* | | changed base notation | jadep | 2016-07-18 |
| * | Move some definitions to Pow2Base (#24) | Jason Gross | 2016-07-18 |
|/ |
|
* | rewrote Testbit and factored out some necessary lemmas about 'uniform' bases ... | jadep | 2016-07-18 |
* | Merged changes, including new ZUtil conventions. | jadep | 2016-07-06 |
* | Factored out some proofs that rely only on base being powers of two, and defi... | jadep | 2016-07-06 |