| Commit message (Expand) | Author | Age |
|---|
| * | use [positive] for [F] modulus, char_ge_C instead of char_gt_C |  Andres Erbsen | 2017-03-02 |
| * | 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 |
| |/ |
|
Andres Erbsen
Jason Gross
jadep
Jason Gross