Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Refactor ModularArithmetic into Zmod, expand Decidable | Andres Erbsen | 2016-08-04 |
| | | | | | | | | | | | | ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1 | ||
* | Removed lingering print statement. | jadep | 2016-07-21 |
| | |||
* | re-introduced extra field isomorphism layer for 8.4 compatibility and better ↵ | jadep | 2016-07-21 |
| | | | | organization of reasoning. | ||
* | restructured ModularBaseSystem pipeline to put tuple conversion before ↵ | jadep | 2016-07-20 |
| | | | | ModularBaseSystem is fully defined, rather than after ModularBaseSystemOpt | ||
* | Fixed unsimplified multiplication definitions in Specific by separating out ↵ | jadep | 2016-07-18 |
| | | | | the zsimplify step; after inserting clauses, we can't rewrite under the binders, but we can do the rewrite and insertions in different definitions. | ||
* | 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 ↵ | jadep | 2016-07-12 |
| | | | | proved that GF1305 is a field | ||
* | pushing through a tweak to the arguments of [sub], and defining a field over ↵ | jadep | 2016-07-12 |
| | | | | ModularBaseSystemInterface using some placeholder operations. | ||
* | ported Specific files to use ModularBaseSystemInterface | jadep | 2016-07-11 |
| | |||
* | defined some group operations, stated group lemma for tuple-based [add] (in ↵ | jadep | 2016-07-08 |
| | | | | terms of isomorphism to ModularArithmetic.F), proved lemma about tuple-based [mul] based on the goals generated by the group constructor | ||
* | stuck trying to figure out dependently typed continuation passing style | Andres Erbsen | 2016-07-06 |
| | |||
* | Canonicalization is now automated in GF25519 and added to GF1305. | jadep | 2016-06-17 |
| | |||
* | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵ | jadep | 2016-06-15 |
| | | | | base-length digit vectors) | ||
* | Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵ | jadep | 2016-05-09 |
| | | | | unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want. | ||
* | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵ | jadep | 2016-04-21 |
weight 2^26) |