aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Support for 128-bit wordsGravatar Jason Gross2016-11-14
* Add word-size-independent interpretationsGravatar Jason Gross2016-11-14
* Add SpecificGen/GF*Gravatar Jason Gross2016-11-13
* make update-_CoqProjectGravatar Jason Gross2016-11-11
* Don't build autogenerated files for nowGravatar jadep2016-11-11
* Automatically generate code for field operations with different primesGravatar jadep2016-11-11
* Freeze stubsGravatar Jason Gross2016-11-11
* Split up GF25519Reflective.Common: faster+parallelGravatar Jason Gross2016-11-09
* Factor related_Z_op (except conditional_sub)Gravatar Jason Gross2016-11-08
* Add IffT, some Proper prod lemmasGravatar Jason Gross2016-11-07
* implement X25519Gravatar Andres Erbsen2016-11-06
* Split off some things from InterpretationsGravatar Jason Gross2016-11-05
* separate Ed25519Extraction.v, add extraction to MakefileGravatar Andres Erbsen2016-11-03
* Move hlist to new fileGravatar Jason Gross2016-11-01
* Add Reflection.ApplicationGravatar Jason Gross2016-10-31
* Switch to reflective bounded word in Ed25519Gravatar Jason Gross2016-10-31
* Add src/Specific/GF25519Reflective.vGravatar Jason Gross2016-10-31
* Switch to a faster way of proving wfGravatar Jason Gross2016-10-30
* Add PartiallyReifiedPropGravatar Jason Gross2016-10-30
* Add reification of various operationsGravatar Jason Gross2016-10-30
* Add initial work on reifying GF25519 stuffGravatar Jason Gross2016-10-30
* Add InterpWfGravatar Jason Gross2016-10-28
* Add InterpWfRelGravatar Jason Gross2016-10-28
* Add beginnings of various interpretations of expression treesGravatar Jason Gross2016-10-27
* Merge pull request #84 from mit-plv/rsloan-phoasGravatar Jason Gross2016-10-27
|\
* | Add syntax and reification for the ops in GF25519Gravatar Jason Gross2016-10-27
* | Factor out cmov{l,ne} and negGravatar Jason Gross2016-10-27
* | Add WfRelReflectiveGravatar Jason Gross2016-10-27
* | Add WfReflectiveGenGravatar Jason Gross2016-10-27
* | Add Wf proofs about MapInterpGravatar Jason Gross2016-10-27
| * Merge branch 'master' into rsloan-phoasGravatar Jason Gross2016-10-27
| |\ | |/ |/|
* | Switch to bounded ZGravatar Jason Gross2016-10-25
| * Fix 8.4 buildGravatar Jason Gross2016-10-22
| * Merge branch 'master' into pr/84Gravatar Jason Gross2016-10-22
| |\ | |/ |/|
* | Fix src/Experiments/Ed25519.v for Coq 8.4Gravatar Jason Gross2016-10-22
| * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 22:21:37 +0000