aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Fix .mailmap (correct name on the left)Gravatar Jason Gross2016-06-18
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-06-17
|\
* | Canonicalization is now automated in GF25519 and added to GF1305.Gravatar jadep2016-06-17
| |
* | Specific version of freeze for GF25519 (automation still needs a little work)Gravatar jadep2016-06-17
| |
| * Be a bit more quiet on make unless VERBOSE=1 is passedGravatar Jason Gross2016-06-16
| |
* | PseudoMersenneBaseRep.mul now carries by default (made possible by strictly ↵Gravatar jadep2016-06-15
| | | | | | | | base-length digit vectors)
* | changed representation definition to require digits vector to be the exact ↵Gravatar jadep2016-06-15
| | | | | | | | length of the base vector
* | Added canonicalization to ModularBaseSystemOpt.Gravatar jadep2016-06-15
| |
| * Add .mailmapGravatar Jason Gross2016-06-15
| |
| * Update README so it's good for both github.com and github.mit.eduGravatar Jason Gross2016-06-15
|/
* MergeGravatar jadep2016-06-14
|\
* | Finished admits for canonicalization proofs.Gravatar jadep2016-06-14
| |
* | reversed modulus_digits and proved a few admitsGravatar jadep2016-06-13
| |
* | progress on second stage (conditional constant-time subtraction) of ↵Gravatar jadep2016-06-13
| | | | | | | | canonicalization proofs
| * Another fix for an anomaly in 8.4pl2Gravatar Jason Gross2016-06-11
| |
| * More Coq 8.4pl2 fixesGravatar Jason Gross2016-06-11
| |
| * Fix for Coq 8.4pl2Gravatar Jason Gross2016-06-11
| |
| * Work around bug #4811 (slow f_equal)Gravatar Jason Gross2016-06-11
| | | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev)
* | starting rewrite using different definition of mapGravatar jadep2016-06-11
| |
| * Minor 8.5 changesGravatar Jason Gross2016-06-10
| |
| * More changes for 8.5Gravatar Jason Gross2016-06-10
| | | | | | | | [Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
| * 8.5 fixesGravatar Jason Gross2016-06-10
| |
| * Set Asymmetric PatternsGravatar Jason Gross2016-06-10
| |
| * Add coqprime that works with 8.5, bundle bedrockGravatar Jason Gross2016-06-10
|/ | | | | | This simplifes the build process, and also allows us to try to build with 8.5. We autodetect the version of Coq in the Makefile to decide which version of coqprime to build.
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-05-25
|\
* | Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ↵Gravatar jadep2016-05-25
| | | | | | | | reason I wasn't affected. Also updated the same file to use E module.
| * ed25519: indentation fixGravatar Andres Erbsen2016-05-24
| |
| * ed25519: integrate FRepPow and FRepInvGravatar Andres Erbsen2016-05-24
| |
| * ed25519: continue refactorGravatar Andres Erbsen2016-05-24
| |
| * PrimeFieldTheorems fermat inverse lemma: prove admitGravatar Andres Erbsen2016-05-24
| |
| * Factor some rewrites into a single [autorewrite]Gravatar Jason Gross2016-05-24
| | | | | | | | Slightly less [apply f_equal] beforehand, more automation.
| * Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-05-24
| | | | | | | | | | | | | | | | | | | | Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work.
| * Fix some issues in Ed25519 tacticsGravatar Jason Gross2016-05-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - Use replace rather than refine to speed up [Defined] and make the tactics easier to read - Use [apply f_equal] in place of [reflexivity] for unknown presumably arcane reasons to satisfy Coq's unifier - Factor out some tactics into tactic scripts - Write a lemma to pull functions out of [Let_In] - Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses (probably a ProofGeneral regexp gone wrong) - Write a kludgy tactic to unfold [proj1_sig] only when applied to [exist] (Pair programming with Andres)
| * F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵Gravatar Andres Erbsen2016-05-24
| | | | | | | | broken...
* | First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵Gravatar jadep2016-05-20
| | | | | | | | input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
| * F: pow_nat_iter_op_correctGravatar Andres Erbsen2016-05-18
| |
| * F: fermat inversion lemma refactorGravatar Andres Erbsen2016-05-18
| |
| * unifiedAddM1Rep_sig: almost thereGravatar Andres Erbsen2016-05-18
| |
| * slightly nicer edwards curve extended coordinates additionGravatar Andres Erbsen2016-05-18
|/
* removed subtraction from todoGravatar jadep2016-05-09
|
* Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵Gravatar jadep2016-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.
* Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-04-29
|
* Merge branch 'master' of github.mit.edu:plv/fiat-cryptoGravatar jadep2016-04-29
|\
* | Moved sign_bit definition to Spec.Gravatar jadep2016-04-29
| |
* | Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-04-29
| | | | | | | | comparing points).
| * remove line from todoGravatar Andres Erbsen2016-04-28
|/
* Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵Gravatar jadep2016-04-28
| | | | general contexts.
* Completed encoding reorganization; factored sign_bit out of PointEncodings ↵Gravatar jadep2016-04-28
| | | | and finished encoding admits.
* ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-04-25
|
* consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-04-25
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 11:55:53 +0000