Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix for Coq < 8.6 | 2016-09-22 | |
| | |||
* | Don't inline everything in Montgomery and Barrett | 2016-09-22 | |
| | | | | | | We still use CSE in fancy machine, because we want to lift the ldi's above the rest of the code. However, on a quick inspection, the algorithm no longer needs CSE to be duplicate-free. | ||
* | Make use of named syntax, do reg assign for fancy | 2016-09-22 | |
| | |||
* | Add dead code elimination | 2016-09-22 | |
| | |||
* | Add a non-higher-order syntax, and reg assignment | 2016-09-22 | |
| | | | | | | | | | | | | | | The register assigner will return [None] if you give it an invalid assignment (too short, attempting to eliminate live code, attempting to merge registers that can't be merged). No correctness proofs yet, nor any sort of automatic register assignment. I'm planning to write a dead-code-eliminator register assigner next. It should also be moderately straight-forward to write a default register allocator, or perhaps a register post-allocator, that takes a manual register allocation, and renumbers variables in a greedy way. (This would let you pre-specify that some registers should be merged, but leave the rest of the assignment up to the algorithm.) | ||
* | Revert "Add a locked version of [let] with fewer reductions" | 2016-09-22 | |
| | | | | | | This reverts commit a4565d0c0c506a56a0db0ca09e9ac7af8b8eaee2. It's not needed. | ||
* | Revert "Fix LockedLet" | 2016-09-22 | |
| | | | | This reverts commit e9fb194f228321f9477a26bf18617047722fd42a. | ||
* | Fix a typo | 2016-09-22 | |
| | |||
* | Add a form of Let_In that carries a proof | 2016-09-22 | |
| | |||
* | move eddsa rep change | 2016-09-22 | |
| | |||
* | alternative signing derivation | 2016-09-22 | |
| | | | | cleanup | ||
* | Util.LetIn: fix proper instance | 2016-09-22 | |
| | |||
* | Fix LockedLet | 2016-09-22 | |
| | | | | | We want beta-iota-delta to leave behind a zeta-redex (a let-in), even when unfolding locked_let. | ||
* | Add a locked version of [let] with fewer reductions | 2016-09-22 | |
| | |||
* | Generalize count_lets | 2016-09-21 | |
| | |||
* | Deduplicate code | 2016-09-21 | |
| | |||
* | Add some util files for reflective let bindings | 2016-09-21 | |
| | |||
* | Reorganization, moving of lemmas to correct files, and 8.4 compatibility | 2016-09-21 | |
| | |||
* | Proved specification of constant-time modulus comparison (except for one ↵ | 2016-09-21 | |
| | | | | ZUtil lemma) | ||
* | Generalize InlineConst | 2016-09-20 | |
| | | | | Now it can inline expressions as well as constants and variables | ||
* | Change [Let ... in ...] to [dlet ... in ...] (#67) | 2016-09-19 | |
| | | | | For "definition". This fixes #65; [Let] conflicts with the vernacular [Let] in Coq 8.4. | ||
* | Make the example a function for reification | 2016-09-18 | |
| | |||
* | Add dec eq for option, list | 2016-09-18 | |
| | |||
* | Better arguments for SmartVarMap | 2016-09-18 | |
| | |||
* | Arguments for SmartVarMap | 2016-09-18 | |
| | |||
* | Generalize SmartVarVar | 2016-09-18 | |
| | |||
* | Fix the 8.4 build by changing a couple standard library names | 2016-09-18 | |
| | |||
* | Util.Notations: change Let to match slet\ | 2016-09-18 | |
| | |||
* | Add reserved notation for Let, change # | 2016-09-17 | |
| | | | | | We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q. | ||
* | Move side lemmas to appropriate files | 2016-09-17 | |
| | |||
* | Partially flesh out [freeze] proofs; also parameterize [sqrt_5mod8] over ↵ | 2016-09-17 | |
| | | | | implementations of [mul] and [pow] so bounds can be threaded through | ||
* | Proved bounds for [encode] results; fleshed out some structure for [freeze] ↵ | 2016-09-17 | |
| | | | | proofs; bundled [freeze] preconditions. | ||
* | Fix missing parenthesis | 2016-09-17 | |
| | |||
* | Remove unused lemma and standardized use of notations for [freeze] proofs | 2016-09-17 | |
| | |||
* | deduplicate Let_In into src/Util/LetIn.v | 2016-09-17 | |
| | |||
* | Add λn reserved notation | 2016-09-16 | |
| | |||
* | Fix for Coq 8.5 | 2016-09-16 | |
| | |||
* | 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 | |
| |