aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
| * | | Fix build processGravatar Robert Sloan2016-06-22
| * | | Full automation for relevant parts of pseudo conversion except letsGravatar Robert Sloan2016-06-22
| * | | Reorganization of wordize.vGravatar Robert Sloan2016-06-22
| * | | Merging wordization and bounding together in Wordize.vGravatar Robert Sloan2016-06-22
| * | | Really complex derivation of wand correctnessGravatar Robert Sloan2016-06-22
| * | | Proper word-based vectorizationGravatar Robert Sloan2016-06-22
| * | | ed25519: indentation fixGravatar Andres Erbsen2016-06-22
| * | | ed25519: integrate FRepPow and FRepInvGravatar Andres Erbsen2016-06-22
| * | | ed25519: continue refactorGravatar Andres Erbsen2016-06-22
| * | | PrimeFieldTheorems fermat inverse lemma: prove admitGravatar Andres Erbsen2016-06-22
| * | | Factor some rewrites into a single [autorewrite]Gravatar Jason Gross2016-06-22
| * | | Remove unfolding, rewrite -> setoid_rewriteGravatar Jason Gross2016-06-22
| * | | Fix some issues in Ed25519 tacticsGravatar Jason Gross2016-06-22
| * | | F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more brok...Gravatar Andres Erbsen2016-06-22
| * | | F: pow_nat_iter_op_correctGravatar Andres Erbsen2016-06-22
| * | | F: fermat inversion lemma refactorGravatar Andres Erbsen2016-06-22
| * | | unifiedAddM1Rep_sig: almost thereGravatar Andres Erbsen2016-06-22
| * | | slightly nicer edwards curve extended coordinates additionGravatar Andres Erbsen2016-06-22
| * | | Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ...Gravatar jadep2016-06-22
| * | | First stage of canonicalization proofs complete; proved 3 carry loops reduce ...Gravatar jadep2016-06-22
| * | | Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ...Gravatar jadep2016-06-22
| * | | Changed name of Encoding to CanonicalEncoding, and changed notation to match.Gravatar jadep2016-06-22
| * | | Moved sign_bit definition to Spec.Gravatar jadep2016-06-22
| * | | Proved decode_point_eq in Ed25519 (comparing encodings is equivalent toGravatar jadep2016-06-22
| * | | Cleanup: mostly moving lemmas to Util files, some moving lemmas to more gener...Gravatar jadep2016-06-22
| * | | Completed encoding reorganization; factored sign_bit out of PointEncodings an...Gravatar jadep2016-06-22
| * | | ed25519: solve elliptic curve math admitsGravatar Andres Erbsen2016-06-22
| * | | consolidate and rename Edwards curve lemmasGravatar Andres Erbsen2016-06-22
| * | | refactor field lemmas out of ed25519Gravatar Andres Erbsen2016-06-22
| * | | reduce admits related to point negationGravatar Andres Erbsen2016-06-22
| * | | Reorganization and revision of Encoding code and redefinition of sign_bit fun...Gravatar jadep2016-06-22
| * | | point_eq_decGravatar Andres Erbsen2016-06-22
| * | | finished last cases of nonzero proofs for associativityGravatar jadep2016-06-22
| * | | added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ...Gravatar jadep2016-06-22
| * | | automated most of the code in GF25519Gravatar jadep2016-06-22
| * | | Cleanup of GF25519Gravatar jadep2016-06-22
| * | | Pulled generalized code out of GF25519 so that it can be used for other moduliGravatar jadep2016-06-22
| * | | moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-06-22
| * | | GF25519 additionGravatar jadep2016-06-22
| * | | GF25519: boring stuff -- fixed indentation and removed commented-out codeGravatar jadep2016-06-22
| * | | Add a tactic for field inequalitiesGravatar Jason Gross2016-06-22
| * | | ed25519 derivation: down to final encodingGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: use representation of FGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: wrangle non-unique representationsGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation: stuck at main loopGravatar Andres Erbsen2016-06-22
| * | | ed25519 derivation down to word until main equationGravatar Andres Erbsen2016-06-22
| * | | Defined a testbit variant for BaseSystem vectors and proved equivalence to Z....Gravatar jadep2016-06-22
| * | | Added lemmas to Util/ that are needed for testbit.Gravatar jadep2016-06-22
| * | | Cleaned up and revised DoubleAndAdd.Gravatar jadep2016-06-22
| * | | Removed old iter_op version and its last dependency.Gravatar jadep2016-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 02:22:33 +0000