aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Small example of bounds-calculation with dependent types (#61)Gravatar Jason Gross2016-09-29
* montgomery-curveGravatar Andres Erbsen2016-09-28
* Merge pull request #69 from JasonGross/scalable-scalarsGravatar Jason Gross2016-09-26
|\
* | add Montgomery x-coordinate Diffie-Hellman and Curve25519Gravatar Andres Erbsen2016-09-26
| * Make use of named syntax, do reg assign for fancyGravatar Jason Gross2016-09-22
| * Add dead code eliminationGravatar Jason Gross2016-09-22
| * Add a non-higher-order syntax, and reg assignmentGravatar Jason Gross2016-09-22
|/
* Revert "Update _CoqProject"Gravatar Jason Gross2016-09-22
* move eddsa rep changeGravatar Andres Erbsen2016-09-22
* Update _CoqProjectGravatar Jason Gross2016-09-22
* Add some util files for reflective let bindingsGravatar Jason Gross2016-09-21
* deduplicate Let_In into src/Util/LetIn.vGravatar Andres Erbsen2016-09-17
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Add generalized version of Wf parameterized on relGravatar Jason Gross2016-09-15
* Move FancyMachine from Experiments to SpecificGravatar Jason Gross2016-09-08
* Add Barrett and Montgomery for the 256-bit machineGravatar Jason Gross2016-09-07
* Add Common Subexpression EliminationGravatar Jason Gross2016-09-06
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05
* Add LinearizeWfGravatar Jason Gross2016-09-05
* Fix order of binders, and add WfProofsGravatar Jason Gross2016-09-05
* Fix _CoqProjectGravatar Jason Gross2016-09-05
* Remove ReifyDirectGravatar Jason Gross2016-09-05
* A helper lemma for [Wf]Gravatar Jason Gross2016-09-05
* PHOAS syntaxGravatar Jason Gross2016-09-05
* Add a file about pointed PropsGravatar Jason Gross2016-09-05
* Rename congrunce_option to inversion_option, add [inversion_prod]Gravatar Jason Gross2016-08-31
* Integrate suggestions from AndresGravatar Jason Gross2016-08-25
* Rework bounded proofsGravatar Jason Gross2016-08-24
* Merge remote-tracking branch 'upstream/master' into bounded-interfaceGravatar Jason Gross2016-08-24
|\
| * Removed now-obsolete ModularBaseSystemField.v; field lemmas for ModularBaseSy...Gravatar jadep2016-08-24
* | Update _CoqProjectGravatar Jason Gross2016-08-23
* | Hook up the bounded interface, finish proofsGravatar Jason Gross2016-08-23
* | Initial work on an architecture interface for ℤ/nℤGravatar Jason Gross2016-08-23
|/
* Specify a type of bounded integers for mod arithGravatar Jason Gross2016-08-09
* Define Montgomery reduction / multiplication on Z (#42)Gravatar Jason Gross2016-08-05
* Implement Barrett Reduction following HAC 14.42 (#45)Gravatar Jason Gross2016-08-04
* Add a generalized version of Barrett Reduction (#44)Gravatar Jason Gross2016-08-04
* Add ZUtil lemmas, and Util.BoolGravatar Jason Gross2016-08-03
* Add HProp, IsomorphismGravatar Jason Gross2016-07-29
* Set Asymmetric Patterns, add util lemmas about sigGravatar Jason Gross2016-07-29
* Make the library 20% faster: [auto with *] is evilGravatar Jason Gross2016-07-22
* re-introduced extra field isomorphism layer for 8.4 compatibility and better ...Gravatar jadep2016-07-21
* Merge branch 'master' of github.com:mit-plv/fiat-cryptoGravatar jadep2016-07-20
|\
| * Move mul_rep_extended (do we actually care about this?)Gravatar Jason Gross2016-07-20
* | restructured ModularBaseSystem pipeline to put tuple conversion before Modula...Gravatar jadep2016-07-20
* | Converted non-canonicalization sections of ModularBaseSystemProofs to tuples.Gravatar jadep2016-07-19
|/
* Experiments/SpecificCurve25519.v: curve25519 addition using small Z-sGravatar Andres Erbsen2016-07-13
* Merge of fixedlength and masterGravatar jadep2016-07-11
|\
| * wrap nsatz in AlgebraGravatar Andres Erbsen2016-07-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 22:35:00 +0000