| Commit message (Expand) | Author | Age |
* | Fix 8.4 build partially | Jason Gross | 2016-11-03 |
* | Make [freeze] proofs consider machine integer width and hard input bounds sep... | jadep | 2016-11-03 |
* | Lift conversion correctness proofs to ModularBaseSystem by providing [pack_re... | jadep | 2016-11-02 |
* | Changes to sqrt for easier bounds proofs; currently blocked on broken proof i... | jadep | 2016-11-02 |
* | Progress proving ERepDec_correct (included tweaking preconditions for Modular... | jadep | 2016-11-02 |
* | remove commented-out lemma | jadep | 2016-10-30 |
* | proved feSign_correct | jadep | 2016-10-29 |
* | Slightly loosen freeze preconditions (in particular, I had failed to properly... | jadep | 2016-10-27 |
* | Modified [freeze] to be more reifyable | jadep | 2016-10-22 |
* | Removed the lingering TODO and print statement that @JasonGross helpfully poi... | jadep | 2016-10-19 |
* | Fill in admits for field with carry_add, carry_opp, and carry_sub | jadep | 2016-10-19 |
* | Add opt versions of add, sub, opp | Jason Gross | 2016-10-19 |
* | map -> List.map (not Tuple.map) | Jason Gross | 2016-09-29 |
* | Finished remaining admits in [freeze] proofs | jadep | 2016-09-23 |
* | Reorganization, moving of lemmas to correct files, and 8.4 compatibility | jadep | 2016-09-21 |
* | Fix the 8.4 build by changing a couple standard library names | jadep | 2016-09-18 |
* | Move side lemmas to appropriate files | jadep | 2016-09-17 |
* | Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over impl... | jadep | 2016-09-17 |
* | Proved bounds for [encode] results; fleshed out some structure for [freeze] p... | jadep | 2016-09-17 |
* | Fix missing parenthesis | jadep | 2016-09-17 |
* | Remove unused lemma and standardized use of notations for [freeze] proofs | jadep | 2016-09-17 |
* | Tweaked automation for 8.4 compatibility | jadep | 2016-09-14 |
* | Automated and cleaned up [freeze] carry-loop proofs | jadep | 2016-09-13 |
* | Update old carry loop bounds proof; now is automated and also has analogous s... | jadep | 2016-09-13 |
* | Moved lemmas to ZUtil | jadep | 2016-09-13 |
* | Finished off last admits for proofs of bounds after 3 carry loops. | jadep | 2016-09-13 |
* | [freeze] proofs : Mostly-complete proofs of bounds after 3 carry loops | jadep | 2016-09-13 |
* | [freeze] proofs : proved bounds for second carry loop. | jadep | 2016-09-13 |
* | Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani... | jadep | 2016-09-06 |
* | Generalized exponentiation chains so inverse and square roots can use the sam... | jadep | 2016-08-31 |
* | Compatibility for 8.5; clear assumptions for an admitted canonicalization proof. | jadep | 2016-08-31 |
* | Proofs for MBS square roots. | jadep | 2016-08-31 |
* | Changed definition of [sub] to require proof that the modulus multiple actual... | jadep | 2016-08-25 |
* | Proper proofs for all ModularBaseSystem operations except [sub] | jadep | 2016-08-24 |
* | Replaced placeholdeer [opp] operation in ModularBaseSystem with a real implem... | jadep | 2016-08-24 |
* | Shifted around some of the proofs in ModularBaseSystemField.v and propagated ... | jadep | 2016-08-23 |
* | Defined real versions of [pow] and [inv] in ModularBaseSystem, replacing plac... | jadep | 2016-08-23 |
* | Merge of conversion development branch with master | jadep | 2016-08-16 |
|\ |
|
| * | Instantiated conversion both to (pack) and from (unpack) another set of limb ... | jadep | 2016-08-16 |
* | | Fix build for Coq < 8.6 | Jason Gross | 2016-08-12 |
|/ |
|
* | Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci... | jadep | 2016-08-09 |
* | [F] has its own module now | Andres Erbsen | 2016-08-05 |
* | Refactor ModularArithmetic into Zmod, expand Decidable | Andres Erbsen | 2016-08-04 |
* | Move most notation level declarations into Util | Jason Gross | 2016-07-27 |
* | Fix 8.6 build | Jason Gross | 2016-07-26 |
* | 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 |
|/ |
|
* | Merge branch 'master' of github.com:mit-plv/fiat-crypto | jadep | 2016-07-20 |
|\ |
|