aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
...
| * merge rsloan-phoas refactors into masterGravatar Robert Sloan2016-10-21
| |\ | |/ |/|
| * committing unstable refactors to patch masterGravatar Robert Sloan2016-10-21
* | Split up GF25519Bounded to avoid circular dependenciesGravatar Jason Gross2016-10-20
* | Merge branch 'master' into instantiation-rsloan-phoasGravatar Jason Gross2016-10-20
|\ \
| * | First pass at bounded version of GF25519Gravatar Jason Gross2016-10-19
* | | Start instantiating boundedness thingsGravatar Jason Gross2016-10-19
| |/ |/|
| * 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
* | Making sub bounds actually tightGravatar Robert Sloan2016-10-14
* | Minor refactors waiting for the code generation to finishGravatar Robert Sloan2016-10-13
| * 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
* | Merge _CoqProjectGravatar Rob Sloan2016-10-06
|\ \
| | * 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
| * Complete example + GF25519 outline in Pipeline.vGravatar Robert Sloan2016-10-02
* | 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
| | * Fix merge with masterGravatar Robert Sloan2016-09-24
| | |\ | |_|/ |/| |
| | * Large-scale refactoring of src/AssemblyGravatar Robert Sloan2016-09-24
| * | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 06:01:46 +0000