aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Split up DoubleBoundedProofs, add proofsGravatar Jason Gross2016-10-07
* Add a variant of [map] on reflective things that changes the interp functionGravatar Jason Gross2016-10-07
* Moved PointEncoding out of SpecGravatar jadep2016-10-06
* Moved conversion logic out of Pow2BaseProofs into its own fileGravatar jadep2016-10-06
* Add some more instructionsGravatar Jason Gross2016-10-04
* Wrote proofs necessary to fill in all point-encoding related context variable...Gravatar jadep2016-10-03
* Spec: add ed25519Gravatar Andres Erbsen2016-10-03
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 06:47:36 +0000