| Commit message (Expand) | Author | Age |
* | Factor out cmov{l,ne} and neg | Jason Gross | 2016-10-27 |
* | Slightly loosen freeze preconditions (in particular, I had failed to properly... | jadep | 2016-10-27 |
* | Created separate definitions for cmovne and cmovl for reification | jadep | 2016-10-23 |
* | final touches/fixes for freeze restructuring | jadep | 2016-10-22 |
* | Modified [freeze] to be more reifyable | jadep | 2016-10-22 |
* | Define carry_opp in terms of carry_sub | Jason Gross | 2016-10-19 |
* | Add opt versions of add, sub, opp | Jason Gross | 2016-10-19 |
* | Added top-level modulus comparison operation so field-element decoding can re... | jadep | 2016-10-12 |
* | Fix compatibility with sigT notation | Jason Gross | 2016-10-10 |
* | Moved conversion logic out of Pow2BaseProofs into its own file | jadep | 2016-10-06 |
* | map -> List.map (not Tuple.map) | Jason Gross | 2016-09-29 |
* | Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl... | jadep | 2016-09-17 |
* | deduplicate Let_In into src/Util/LetIn.v | Andres Erbsen | 2016-09-17 |
* | Finished sqrt in GF25519 | jadep | 2016-09-06 |
* | Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani... | jadep | 2016-09-06 |
* | Added square roots to GF1305, started reworking freeze_opt in preparation for... | jadep | 2016-08-31 |
* | Generalized exponentiation chains so inverse and square roots can use the sam... | jadep | 2016-08-31 |
* | Removed some commented-out code that will probably not be needed. | jadep | 2016-08-31 |
* | Changed definition of [sub] to require proof that the modulus multiple actual... | jadep | 2016-08-25 |
* | Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem... | jadep | 2016-08-24 |
* | Work around lack of Fixpoint 'equation' lemmas in Coq < 8.4pl6 | jadep | 2016-08-24 |
* | Added optimized [inv] operation to Specific, and removed dependencies on Modu... | jadep | 2016-08-24 |
* | Shifted around some of the proofs in ModularBaseSystemField.v and propagated ... | jadep | 2016-08-23 |
* | Merge of conversion development branch with master | jadep | 2016-08-16 |
|\ |
|
| * | Added optimized versions of [pack] and [unpack] to ModularBaseSystemOpt. Furt... | jadep | 2016-08-16 |
* | | Add length lemmas | Jason Gross | 2016-08-12 |
|/ |
|
* | Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci... | jadep | 2016-08-09 |
* | Massively speed up construct_params (#48) | Jason Gross | 2016-08-08 |
* | Fix 8.4 build. | jadep | 2016-07-25 |
* | 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 |
|/ |
|
* | Fix 8.4{pl1,pl2} builds | jadep | 2016-07-21 |
* | Changed name of [carry_and_reduce_single] to [carry_single], since it does no... | jadep | 2016-07-21 |
* | Fixes #29 | jadep | 2016-07-21 |
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ... | jadep | 2016-07-21 |
* | merge | jadep | 2016-07-20 |
|\ |
|
* | | restructured ModularBaseSystem pipeline to put tuple conversion before Modula... | jadep | 2016-07-20 |
| * | Remove dependency of ext_base on pseudomersenne | Jason Gross | 2016-07-20 |
|/ |
|
* | ext_base: now defined in terms of ext_limb_widths | Jason Gross | 2016-07-18 |
* | Express carry_simple in terms of carry_gen | Jason Gross | 2016-07-18 |
* | Move some definitions to Pow2Base (#24) | Jason Gross | 2016-07-18 |
* | pushing through a tweak to the arguments of [sub], and defining a field over ... | jadep | 2016-07-12 |
* | Make [base] and [log_cap] notations | Jason Gross | 2016-07-11 |
* | Merge of fixedlength and master | jadep | 2016-07-11 |
|\ |
|
* | | unstuck carry_mul_opt_cps using from_list_default | jadep | 2016-07-08 |
| * | 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 |
* | | | stuck trying to figure out dependently typed continuation passing style | Andres Erbsen | 2016-07-06 |
* | | | remove PseudoMersenneRep | Andres Erbsen | 2016-07-03 |