| Commit message (Expand) | Author | Age |
* | Speed up src/Specific/GF25519.v (#54) | Jason Gross | 2016-08-18 |
* | Updated GF files to reflect change in [repeat] | jadep | 2016-08-16 |
* | Added specific versions of [pack] and [unpack] to GF1305.v | jadep | 2016-08-16 |
* | Merge of conversion development branch with master | jadep | 2016-08-16 |
|\ |
|
| * | Added specific versions of [pack] and [unpack] to GF25519 | jadep | 2016-08-16 |
|/ |
|
* | Tweaked structure of GF [carry_mul] so that carry chain is specified in Speci... | jadep | 2016-08-09 |
* | Refactor ModularArithmetic into Zmod, expand Decidable | Andres Erbsen | 2016-08-04 |
* | Removed lingering print statement. | jadep | 2016-07-21 |
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ... | jadep | 2016-07-21 |
* | restructured ModularBaseSystem pipeline to put tuple conversion before Modula... | jadep | 2016-07-20 |
* | Fixed unsimplified multiplication definitions in Specific by separating out t... | jadep | 2016-07-18 |
* | more changes to Specific for 8.4 compatibility | jadep | 2016-07-15 |
* | re-cleaned operations in Specific and updated GF25519 to match GF1305 | jadep | 2016-07-12 |
* | cleaned Specific operations so they produce code without proof terms, and pro... | jadep | 2016-07-12 |
* | pushing through a tweak to the arguments of [sub], and defining a field over ... | jadep | 2016-07-12 |
* | ported Specific files to use ModularBaseSystemInterface | jadep | 2016-07-11 |
* | defined some group operations, stated group lemma for tuple-based [add] (in t... | jadep | 2016-07-08 |
* | stuck trying to figure out dependently typed continuation passing style | Andres Erbsen | 2016-07-06 |
* | Aggregate all level specifications not in Spec/* | Jason Gross | 2016-06-22 |
* | remove obsolete rep mechanism | Andres Erbsen | 2016-06-20 |
* | GF25519: quiet | Andres Erbsen | 2016-06-20 |
* | Merge branch 'field-experiment' | Andres Erbsen | 2016-06-20 |
|\ |
|
* | | Canonicalization is now automated in GF25519 and added to GF1305. | jadep | 2016-06-17 |
* | | Specific version of freeze for GF25519 (automation still needs a little work) | jadep | 2016-06-17 |
* | | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly b... | jadep | 2016-06-15 |
* | | Another fix for an anomaly in 8.4pl2 | Jason Gross | 2016-06-11 |
* | | Work around bug #4811 (slow f_equal) | Jason Gross | 2016-06-11 |
| * | ed25519: refactor some Proper | Andres Erbsen | 2016-06-06 |
| * | rewrite in Let_In binder by tactic | Andres Erbsen | 2016-06-04 |
| * | Let_In rewriting | Andres Erbsen | 2016-06-03 |
| * | leibniz equal version of topdown rewriting of sigma types: nicer | Andres Erbsen | 2016-06-01 |
| * | leibniz equal version of topdown rewriting of sigma types | Andres Erbsen | 2016-06-01 |
| * | E impl: proper morphisms are hard to dow without setoids | Andres Erbsen | 2016-05-30 |
| * | ERep add | Andres Erbsen | 2016-05-29 |
| * | --amend | Andres Erbsen | 2016-05-28 |
| * | verify derivation, EdDSA layer: allow arbitrary equivalence relation for ERep... | Andres Erbsen | 2016-05-28 |
| * | verify derivation, EdDSA layer: remove unused context variables | Andres Erbsen | 2016-05-28 |
| * | verify derivation: EdDSA layer | Andres Erbsen | 2016-05-28 |
| * | right after scalars to F l | Andres Erbsen | 2016-05-27 |
| * | before changing SRep from N to F l | Andres Erbsen | 2016-05-27 |
|/ |
|
* | ed25519: indentation fix | Andres Erbsen | 2016-05-24 |
* | ed25519: integrate FRepPow and FRepInv | Andres Erbsen | 2016-05-24 |
* | ed25519: continue refactor | Andres Erbsen | 2016-05-24 |
* | Factor some rewrites into a single [autorewrite] | Jason Gross | 2016-05-24 |
* | Remove unfolding, rewrite -> setoid_rewrite | Jason Gross | 2016-05-24 |
* | Fix some issues in Ed25519 tactics | Jason Gross | 2016-05-24 |
* | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok... | Andres Erbsen | 2016-05-24 |
* | unifiedAddM1Rep_sig: almost there | Andres Erbsen | 2016-05-18 |
* | Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ... | jadep | 2016-05-09 |
* | Moved sign_bit definition to Spec. | jadep | 2016-04-29 |