| Commit message (Expand) | Author | Age |
|---|
| * | Fill in admits for field with carry_add, carry_opp, and carry_sub |  jadep | 2016-10-19 |
| * | 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 |
| * | Fix a proof | Jason Gross | 2016-10-16 |
| * | Don't inline as much in ZBoundedZ | Jason Gross | 2016-10-16 |
| * | Add Z as ZBounded | Jason Gross | 2016-10-16 |
| * | Added top-level modulus comparison operation so field-element decoding can re... | jadep | 2016-10-12 |
| * | Bundle arguments to Barrett Reduction | Jason Gross | 2016-10-10 |
| * | Fix compatibility with sigT notation | Jason Gross | 2016-10-10 |
| * | More zsimplify lemmas, stronger Ztestbit | Jason Gross | 2016-10-07 |
| * | Moved lemma to ZUtil and added an extra lemma jgross needed | jadep | 2016-10-06 |
| * | 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 |
| * | Merge pull request #69 from JasonGross/scalable-scalars |  Jason Gross | 2016-09-26 |
| |\ |
|
| * | | Finished remaining admits in [freeze] proofs | jadep | 2016-09-23 |
| | * | Drop CSE from Fancy Machine | Jason Gross | 2016-09-22 |
| |/ |
|
| * | alternative signing derivation |  Andres Erbsen | 2016-09-22 |
| * | Reorganization, moving of lemmas to correct files, and 8.4 compatibility | jadep | 2016-09-21 |
| * | Proved specification of constant-time modulus comparison (except for one ZUti... | jadep | 2016-09-21 |
| * | Fix the 8.4 build by changing a couple standard library names | jadep | 2016-09-18 |
| * | Add reserved notation for Let, change # | Jason Gross | 2016-09-17 |
| * | 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 |
| * | deduplicate Let_In into src/Util/LetIn.v | Andres Erbsen | 2016-09-17 |
| * | ModularArithmetic: conversions between [F] and [nat] | Andres Erbsen | 2016-09-16 |
| * | 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 |
| * | Fully qualify [Require]s |  Jason Gross | 2016-09-08 |
| * | Better spec in Montgomery.ZBounded | Jason Gross | 2016-09-07 |
| * | Finished sqrt in GF25519 | jadep | 2016-09-06 |
| * | Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani... | jadep | 2016-09-06 |
| * | Add correctness theorems to Montgomery.ZBounded | Jason Gross | 2016-08-31 |
| * | 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 |
| * | Compatibility for 8.5; clear assumptions for an admitted canonicalization proof. | jadep | 2016-08-31 |
| * | Proofs for MBS square roots. | jadep | 2016-08-31 |
| * | fixed typo; extra argument | jadep | 2016-08-31 |
| * | Parameterized square roots for primes that are 5 mod 8 over any computation o... | jadep | 2016-08-31 |
| * | Reworked square root theorems to prove they are valid iff a square root exist... | jadep | 2016-08-31 |
| * | Add runtime equality comparison and square root functions to ModularBaseSystem. | jadep | 2016-08-31 |
| * | fix duplicate name in PrimeFieldTheorems | jadep | 2016-08-31 |
jadep
Jason Gross
Jason Gross
Andres Erbsen
Jason Gross