Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge pull request #335 from mit-plv/cpsloops | 2018-04-18 | |
|\ | | | | | comprehensive loops framework with complete proof theory | ||
* | | Add new assembly-mimicking operations rshi, cc_m, and cc_l | 2018-04-11 | |
| | | |||
* | | Update number/string conversions | 2018-04-09 | |
| | | | | | | | | To updated version of https://github.com/coq/coq/pull/6597 | ||
| * | move Loops from Experiments to Util | 2018-03-27 | |
| | | |||
| * | remove old loops code | 2018-03-27 | |
|/ | |||
* | Add Algebra.SubsetoidRing | 2018-03-12 | |
| | |||
* | make update-_CoqProject | 2018-03-10 | |
| | |||
* | Prove another Barrett reduction variant. | 2018-03-09 | |
| | | | | | | | | | | This variant comes from http://www.ridiculousfish.com/blog/posts/labor-of-division-episode-i.html. It was useful for https://boringssl-review.googlesource.com/#/c/boringssl/+/25887. TODO - Talk to Andres to figure out all the ways this could be done more cleanly. It was originally a standalone file. | ||
* | Add new modular addition operation on Z | 2018-02-23 | |
| | |||
* | Add pointed types | 2018-02-18 | |
| | | | | For filling in default values | ||
* | Add a file to parse taps with Coq notations | 2018-02-14 | |
| | |||
* | Add some string utility functions | 2018-02-13 | |
| | |||
* | Add string conversions | 2018-02-11 | |
| | |||
* | Split off ZRange lemmas | 2018-02-10 | |
| | |||
* | Add some ZRange operations | 2018-02-10 | |
| | |||
* | minor updates needed to make it compile with bbv | 2018-02-05 | |
| | | | | removing lemma wordToNat_wzero is ok because it's already in bbv | ||
* | add bedrock bit vectors library (bbv) as a submodule replacing the Bedrock ↵ | 2018-02-05 | |
| | | | | directory | ||
* | Add x25519 donna versions with the new way of generating C code | 2018-01-15 | |
| | |||
* | Generate fecarry for solinas | 2018-01-10 | |
| | | | | | | | This is a one-line change in generate_parameters.py (plus some whitespace trimming), and running `make regenerate-curves` This handles part of #294 | ||
* | Factor out fsatz lemmas | 2018-01-09 | |
| | | | | | | | | | After | File Name | Before || Change | % Change ------------------------------------------------------------------------- 1m11.42s | Total | 1m53.75s || -0m42.33s | -37.21% ------------------------------------------------------------------------- 1m06.02s | Curves/Weierstrass/Jacobian | 1m53.76s || -0m47.73s | -41.96% 0m05.40s | Util/FsatzAutoLemmas | N/A || +0m05.40s | ∞ | ||
* | @davidben merged Jacobian+affine into Jacobian+Jacobian | 2018-01-09 | |
| | |||
* | Jacobian coordinates | 2018-01-09 | |
| | |||
* | Add Tactics.RunTacticAsConstr | 2017-11-26 | |
| | |||
* | Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v | 2017-11-24 | |
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545 | ||
* | Make a copy of Demo.v | 2017-11-24 | |
| | |||
* | Add ModInv autosolver | 2017-11-16 | |
| | |||
* | Update GeneralizeVar to ensure Wf | 2017-11-13 | |
| | | | | | This will hopefully pave the way for not needing to prove Wf anywhere in the bounds pipeline. | ||
* | Make pipeline options more easily extensible | 2017-11-13 | |
| | | | | | Also add a dummy option about renaming binders, to be used in an upcoming commit. | ||
* | Add faster version of intros [a b] for reflective stuff | 2017-11-13 | |
| | |||
* | Add autosolve admit package | 2017-11-12 | |
| | |||
* | automatic modifications to _Coqproject with new files | 2017-11-12 | |
| | |||
* | Add Decidable2Bool | 2017-11-11 | |
| | |||
* | Add ListUtil.Forall | 2017-11-11 | |
| | |||
* | More modularity in autosolve | 2017-11-10 | |
| | |||
* | Add HeadUnderBinders | 2017-11-07 | |
| | |||
* | A bit more reorganization of autosolve | 2017-11-07 | |
| | | | | This lets other files import evar_package without having to be rebuilt every time a new package alias is added to Autosolve | ||
* | Move SideConditionFramework | 2017-11-07 | |
| | |||
* | Add SideConditionFramework | 2017-11-07 | |
| | |||
* | Add type of bounded Z | 2017-11-02 | |
| | |||
* | make update-_CoqProject | 2017-11-02 | |
| | |||
* | Add MapBaseType | 2017-10-31 | |
| | |||
* | Add unextend_op | 2017-10-31 | |
| | |||
* | make update-_CoqProject | 2017-10-29 | |
| | |||
* | Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit | 2017-10-24 | |
| | |||
* | Add MapBaseType | 2017-10-23 | |
| | |||
* | Add InlineConstAndOpByRewrite | 2017-10-23 | |
| | |||
* | Add ZExtended/InlineConstAndOp.v | 2017-10-22 | |
| | |||
* | Add StripExpr | 2017-10-22 | |
| | |||
* | Add tight and loose bounds, no carry in add, sub | 2017-10-22 | |
| | | | | | | | | Following Andres' suggestions to allow making ladderstep from other synthesis things. It went though mostly without a hitch, though there were a number of boilerplate changes needed. | ||
* | Add MapType | 2017-10-21 | |
| |