| Commit message (Expand) | Author | Age |
* | reorganized lemmas; moved several to ListUtil and ZUtil. | Jade Philipoom | 2015-11-24 |
* | ModularBaseSystem: added definition to perform a specific sequence of carries... | Jade Philipoom | 2015-11-24 |
* | ModularBaseSystem: relocated base_succ to PsuedoMersenneBaseParams, proved ca... | Jade Philipoom | 2015-11-20 |
* | Added base_succ precondition to BaseSystem to help prove carrying. | Jade Philipoom | 2015-11-19 |
* | ModularBaseSystem: proving reduce case of carry_rep. | Jade Philipoom | 2015-11-18 |
* | ModularBaseSystem: carry_rep has boring modular arithmetic proofs | Andres Erbsen | 2015-11-17 |
* | ModularBaseSystem: introduced lemmas about breaking lists; working on carry_r... | Jade Philipoom | 2015-11-17 |
* | ModularBaseSystem.carry: implement, state lemmas, some progress on proofs | Andres Erbsen | 2015-11-17 |
* | BaseSystem: finish first pass of prettifying proofs | Andres Erbsen | 2015-11-11 |
* | BaseSystem: more prettyfication | Andres Erbsen | 2015-11-10 |
* | ModularBaseSystem: Implemented and proved subtraction, completing implementat... | Jade Philipoom | 2015-11-10 |
* | BaseSystem: implemented and proved subtraction. | Jade Philipoom | 2015-11-10 |
* | ModularBaseSystem: implemented fromGF and proved correct, moved inline admits... | Jade Philipoom | 2015-11-10 |
* | Merge of local changes and most recent changes in mit-plv master | Jade Philipoom | 2015-11-10 |
|\ |
|
* | | BaseSystem: added encode definition, included b0_1 precondition in BaseCoefs ... | Jade Philipoom | 2015-11-10 |
| * | BaseSystem: more boring | Andres Erbsen | 2015-11-10 |
| * | BaseSystem: more hints, more boring | Andres Erbsen | 2015-11-10 |
|/ |
|
* | ModularBaseSystem: finished most admits for addition and multiplication, move... | Jade Philipoom | 2015-11-09 |
* | ModularBaseSystem: proved addition and multiplication. | Jade Philipoom | 2015-11-07 |
* | BaseSystem: removed confusing notations and added mul_length lemma (currently... | Jade Philipoom | 2015-11-07 |
* | ModularBaseSystem: finish base_good | Andres Erbsen | 2015-11-07 |
* | ModularBaseSystem: prove some admits in mase system extension | Andres Erbsen | 2015-11-07 |
* | ModularBaseSystem: continuing to prove base_good. | Jade Philipoom | 2015-11-07 |
* | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | Jade Philipoom | 2015-11-06 |
|\ |
|
* | | Starting to prove base_good in ModularBaseSystem | Jade Philipoom | 2015-11-06 |
| * | Specific: PseudoMersenneBaseParams for GF25519Base25Point5. | Andres Erbsen | 2015-11-06 |
| * | Merge remote-tracking branch 'jadep/master' | Andres Erbsen | 2015-11-06 |
| |\
| |/
|/| |
|
* | | ModularBaseSystem: finished proving all admits for reduce_rep; proved base_po... | Jade Philipoom | 2015-11-05 |
* | | Added lemmas to ListUtil and BaseSystem to help in ModularBaseSystem. | Jade Philipoom | 2015-11-05 |
* | | ModularBaseSystem: Implemented reduce and proved reduce_rep, currently workin... | Jade Philipoom | 2015-11-05 |
* | | ModularBaseSystem: defined an extended base system to represent unreduced pro... | Jade Philipoom | 2015-11-04 |
* | | Relocated boring tactic to ListUtil and added combine_truncate lemma. | Jade Philipoom | 2015-11-04 |
* | | Merge branch 'master' of github.mit.edu:plv/fiat-crypto | Jade Philipoom | 2015-11-03 |
|\| |
|
* | | ModularBaseSystem skeleton | Andres Erbsen | 2015-10-30 |
| * | BaseSystem to Util.ListUtil: separate out generic list lemmas | Andres Erbsen | 2015-10-29 |
| * | Merge branch 'master' of github.mit.edu:rsloan/fiat-crypto | Andres Erbsen | 2015-10-29 |
| |\ |
|
| * | | remove SearchAbouts | Andres Erbsen | 2015-10-28 |
* | | | BaseSystem: removed axiom b0_1. | Jade Philipoom | 2015-10-28 |
* | | | Merge branch 'master' into jade | Jade Philipoom | 2015-10-28 |
|\| | |
|
* | | | BaseSystem: proved all admits. | Jade Philipoom | 2015-10-28 |
| * | | Proof improvements in BaseSystem | Adam Chlipala | 2015-10-28 |
* | | | Proved add_same_length lemma. | Jade Philipoom | 2015-10-27 |
* | | | Multiply rep mostly proven, working on admits. | Jade Philipoom | 2015-10-27 |
| | * | patches for galois | Robert Sloan | 2015-10-27 |
* | | | More work on proving linearity of multiply. | Jade Philipoom | 2015-10-26 |
* | | | Modified to use formal preconditions for b0_1 and base_positive. | Jade Philipoom | 2015-10-25 |
| * | | pos_pow_nat_pos | Andres Erbsen | 2015-10-25 |
| * | | nth_tac | Andres Erbsen | 2015-10-25 |
* | | | Merge branch 'base0_1' into jade | Jade Philipoom | 2015-10-25 |
|\ \ \ |
|
* \ \ \ | Merge https://github.com/mit-plv/fiat-crypto into jade | Jade Philipoom | 2015-10-25 |
|\ \ \ \
| | |/ /
| |/| | |
|