Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Add more prop_of_option | 2016-09-16 | ||
| | ||||
* | Derive EdDSA.verify from equational specification | 2016-09-16 | ||
| | | | | Experiments/SpecEd25519 will come back soon | |||
* | Algebra: prove an admit, add eq_r_opp_r_inv | 2016-09-16 | ||
| | ||||
* | IterAssocOp: parameters before arguments | 2016-09-16 | ||
| | ||||
* | ModularArithmetic: conversions between [F] and [nat] | 2016-09-16 | ||
| | ||||
* | Generalize InlineConst | 2016-09-16 | ||
| | | | | | Should now support constant subexpression evaluation (removing things like (_ + 0)). | |||
* | Split off lemmas about [InlineConst] | 2016-09-16 | ||
| | ||||
* | Equality for nat in natutil | 2016-09-16 | ||
| | ||||
* | Add arguments for smartval | 2016-09-16 | ||
| | ||||
* | Fix a bad line | 2016-09-16 | ||
| | ||||
* | Add SmartVal | 2016-09-16 | ||
| | ||||
* | Add generalized version of Wf parameterized on rel | 2016-09-15 | ||
| | | | | | | This should allow a nice elegant abstract way of doing bounds analysis. It's possible that wf should be redefined in terms of rel_wf. | |||
* | More 8.4 compatibility | 2016-09-14 | ||
| | ||||
* | Tweaked automation for 8.4 compatibility | 2016-09-14 | ||
| | ||||
* | Automated and cleaned up [freeze] carry-loop proofs | 2016-09-13 | ||
| | ||||
* | Update old carry loop bounds proof; now is automated and also has analogous ↵ | 2016-09-13 | ||
| | | | | structure to subsequent carry loop proofs | |||
* | Moved lemmas to ZUtil | 2016-09-13 | ||
| | ||||
* | Finished off last admits for proofs of bounds after 3 carry loops. | 2016-09-13 | ||
| | ||||
* | [freeze] proofs : Mostly-complete proofs of bounds after 3 carry loops | 2016-09-13 | ||
| | ||||
* | [freeze] proofs : proved bounds for second carry loop. | 2016-09-13 | ||
| | ||||
* | Merge pull request #63 from JasonGross/fancy-barrett-montgomery | 2016-09-08 | ||
|\ | | | | | Add Barrett and Montgomery for the 256-bit machine | |||
* | | Fully qualify [Require]s | 2016-09-08 | ||
| | | | | | | | | This way they won't become ambiguous if we add new files | |||
| * | Move FancyMachine from Experiments to Specific | 2016-09-08 | ||
| | | | | | | | | | | | | | | | | | | | | Quoting Andres: > I am leaning towards putting this in Specifc instead of Experiments -- it > seems like complete result on its own, these files are unlikely to be reused > for something else, and I don't think we are expecting to need to remove it > any time soon. Currently, `Specific` code does not quantify over anything (no > context variables), but this seems secondary. We could make versions of this > with the curve constants plugged in, though. | |||
| * | Address code review, add come comments and cleanup | 2016-09-08 | ||
| | | ||||
| * | Add Barrett and Montgomery for the 256-bit machine | 2016-09-07 | ||
|/ | | | | | | | | | | After | File Name | Before || Change ------------------------------------------------------------------------ 0m12.69s | Total | 0m00.00s || +0m12.69s ------------------------------------------------------------------------ 0m06.96s | Experiments/FancyMachineMontgomery256 | N/A || +0m06.96s 0m03.07s | Experiments/FancyMachineBarrett256 | N/A || +0m03.06s 0m02.67s | Experiments/FancyMachine256 | N/A || +0m02.67s | |||
* | Fixes for Coq 8.4 | 2016-09-07 | ||
| | ||||
* | Bump submodule for better timing | 2016-09-07 | ||
| | ||||
* | Remove the need for coercions in well-typing of Reify | 2016-09-07 | ||
| | ||||
* | Add fastpath to reify, add coercions | 2016-09-07 | ||
| | | | | The lack of exported coercions broke some automation. | |||
* | Work around bug #5073 (lia) | 2016-09-07 | ||
| | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5073, lia got weaker in the past few days (sometimes can't handle biconditionals) | |||
* | Better spec in Montgomery.ZBounded | 2016-09-07 | ||
| | ||||
* | Key on the head of the operation in reification | 2016-09-07 | ||
| | | | | | | Hopefully fixes #62 Also, don't export InputSyntax in Reify | |||
* | Add Common Subexpression Elimination | 2016-09-06 | ||
| | ||||
* | Fix for 8.4's type inferencer being broken | 2016-09-06 | ||
| | ||||
* | Fix for changes in 8.4/8.5 behavior of [intro] w.r.t. refolding | 2016-09-06 | ||
| | ||||
* | Fix for 8.6 (context (correctly) no longer defaults to type_scope) | 2016-09-06 | ||
| | ||||
* | make 8.4 happier | 2016-09-06 | ||
| | ||||
* | Finished sqrt in GF25519 | 2016-09-06 | ||
| | ||||
* | Pushed [freeze] through to GF25519 in preparation for defining [sqrt], ↵ | 2016-09-06 | ||
| | | | | cleaning up freeze-related organization and definitions along the way | |||
* | Add interp_flat_type_gen_rel_pointwise | 2016-09-05 | ||
| | ||||
* | Add correctness of interpretation of linearize and inline_const | 2016-09-05 | ||
| | ||||
* | Add instances for interp_type_gen_rel_pointwise | 2016-09-05 | ||
| | ||||
* | Better implicits for interp_type_gen_rel_pointwise | 2016-09-05 | ||
| | ||||
* | Better implicits for interpf, pointwise-lifting of rels over interp_type_gen | 2016-09-05 | ||
| | ||||
* | Better implicits for interpf | 2016-09-05 | ||
| | ||||
* | Better implicits for interp | 2016-09-05 | ||
| | ||||
* | Better implicits for Interp | 2016-09-05 | ||
| | ||||
* | Add LinearizeWf | 2016-09-05 | ||
| | | | | The proof of wf-preservation for inline_const isn't finished yet, though... | |||
* | Reorder WfProofs arguments | 2016-09-05 | ||
| | ||||
* | Fix order of binders, and add WfProofs | 2016-09-05 | ||
| |