aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Rename and clean up exponent codeGravatar Jason Gross2016-10-17
* Initial work on exponent field as ZGravatar Jason Gross2016-10-17
* Add Z as ZBoundedGravatar Jason Gross2016-10-16
* Add src/BoundedArithmetic/Eta.vGravatar Jason Gross2016-10-13
* remove EncodingLemmas from _CoqProject (file deleted by Andres in commit 9379...Gravatar jadep2016-10-12
* Add Ed25519 to _CoqProjectGravatar Jason Gross2016-10-12
* Add some admitted x86->ZLike proofsGravatar Jason Gross2016-10-10
* Update _CoqProjectGravatar Jason Gross2016-10-10
* Add shl,shr,shrd to repeated doublingGravatar Jason Gross2016-10-09
* Add proofs for doubling shl,shr,shrdGravatar Jason Gross2016-10-09
* Some work on x86 and bounded repeated thingsGravatar Jason Gross2016-10-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 01:55:26 +0000