aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Add λn reserved notationGravatar Jason Gross2016-09-16
* Fix for Coq 8.5Gravatar Jason Gross2016-09-16
* Add more prop_of_optionGravatar Jason Gross2016-09-16
* Derive EdDSA.verify from equational specificationGravatar Andres Erbsen2016-09-16
* Algebra: prove an admit, add eq_r_opp_r_invGravatar Andres Erbsen2016-09-16
* IterAssocOp: parameters before argumentsGravatar Andres Erbsen2016-09-16
* ModularArithmetic: conversions between [F] and [nat]Gravatar Andres Erbsen2016-09-16
* Generalize InlineConstGravatar Jason Gross2016-09-16
* Split off lemmas about [InlineConst]Gravatar Jason Gross2016-09-16
* Equality for nat in natutilGravatar Jason Gross2016-09-16
* Add arguments for smartvalGravatar Jason Gross2016-09-16
* Fix a bad lineGravatar Jason Gross2016-09-16
* Add SmartValGravatar Jason Gross2016-09-16
* Add generalized version of Wf parameterized on relGravatar Jason Gross2016-09-15
* More 8.4 compatibilityGravatar jadep2016-09-14
* Tweaked automation for 8.4 compatibilityGravatar jadep2016-09-14
* Automated and cleaned up [freeze] carry-loop proofsGravatar jadep2016-09-13
* Update old carry loop bounds proof; now is automated and also has analogous s...Gravatar jadep2016-09-13
* Moved lemmas to ZUtilGravatar jadep2016-09-13
* Finished off last admits for proofs of bounds after 3 carry loops.Gravatar jadep2016-09-13
* [freeze] proofs : Mostly-complete proofs of bounds after 3 carry loopsGravatar jadep2016-09-13
* [freeze] proofs : proved bounds for second carry loop.Gravatar jadep2016-09-13
* Merge pull request #63 from JasonGross/fancy-barrett-montgomeryGravatar Jason Gross2016-09-08
|\
* | Fully qualify [Require]sGravatar Jason Gross2016-09-08
| * Move FancyMachine from Experiments to SpecificGravatar Jason Gross2016-09-08
| * Address code review, add come comments and cleanupGravatar Jason Gross2016-09-08
| * Add Barrett and Montgomery for the 256-bit machineGravatar Jason Gross2016-09-07
|/
* Fixes for Coq 8.4Gravatar Jason Gross2016-09-07
* Remove the need for coercions in well-typing of ReifyGravatar Jason Gross2016-09-07
* Add fastpath to reify, add coercionsGravatar Jason Gross2016-09-07
* Work around bug #5073 (lia)Gravatar Jason Gross2016-09-07
* Better spec in Montgomery.ZBoundedGravatar Jason Gross2016-09-07
* Key on the head of the operation in reificationGravatar Jason Gross2016-09-07
* Add Common Subexpression EliminationGravatar Jason Gross2016-09-06
* Fix for 8.4's type inferencer being brokenGravatar Jason Gross2016-09-06
* Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refoldingGravatar Jason Gross2016-09-06
* Fix for 8.6 (context (correctly) no longer defaults to type_scope)Gravatar Jason Gross2016-09-06
* make 8.4 happierGravatar jadep2016-09-06
* Finished sqrt in GF25519Gravatar jadep2016-09-06
* Pushed [freeze] through to GF25519 in preparation for defining [sqrt], cleani...Gravatar jadep2016-09-06
* Add interp_flat_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Add correctness of interpretation of linearize and inline_constGravatar Jason Gross2016-09-05
* Add instances for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interp_type_gen_rel_pointwiseGravatar Jason Gross2016-09-05
* Better implicits for interpf, pointwise-lifting of rels over interp_type_genGravatar Jason Gross2016-09-05
* Better implicits for interpfGravatar Jason Gross2016-09-05
* Better implicits for interpGravatar Jason Gross2016-09-05
* Better implicits for InterpGravatar Jason Gross2016-09-05
* Add LinearizeWfGravatar Jason Gross2016-09-05
* Reorder WfProofs argumentsGravatar Jason Gross2016-09-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-24 02:41:59 +0000