Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Shuffle some ZUtil lemmas around | Jason Gross | 2018-07-08 | |
| | ||||
* | Add ZUtil.Sorting | Jason Gross | 2018-06-29 | |
| | ||||
* | Add specialize_all_ways, fix a proof in ↵ | Jason Gross | 2018-06-26 | |
| | | | | src/Compilers/Z/ArithmeticSimplifierInterp.v | |||
* | New pipeline, split among files | Jason Gross | 2018-06-17 | |
| | ||||
* | Add ErrorT monad, and Show class | Jason Gross | 2018-06-15 | |
| | ||||
* | Add PrimitiveHList, PrimitiveProd | Jason Gross | 2018-06-13 | |
| | ||||
* | Move Option.List.map to OptionList.map to fix name clashes in Tuple | Jason Gross | 2018-06-04 | |
| | ||||
* | make update-_CoqProject | Jason Gross | 2018-05-05 | |
| | ||||
* | Merge pull request #335 from mit-plv/cpsloops | Andres Erbsen | 2018-04-18 | |
|\ | | | | | comprehensive loops framework with complete proof theory | |||
* | | Add new assembly-mimicking operations rshi, cc_m, and cc_l | Jade Philipoom | 2018-04-11 | |
| | | ||||
* | | Update number/string conversions | Jason Gross | 2018-04-09 | |
| | | | | | | | | To updated version of https://github.com/coq/coq/pull/6597 | |||
| * | move Loops from Experiments to Util | Andres Erbsen | 2018-03-27 | |
| | | ||||
| * | remove old loops code | Andres Erbsen | 2018-03-27 | |
|/ | ||||
* | Add Algebra.SubsetoidRing | Jason Gross | 2018-03-12 | |
| | ||||
* | make update-_CoqProject | Jason Gross | 2018-03-10 | |
| | ||||
* | Prove another Barrett reduction variant. | David Benjamin | 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 | Jade Philipoom | 2018-02-23 | |
| | ||||
* | Add pointed types | Jason Gross | 2018-02-18 | |
| | | | | For filling in default values | |||
* | Add a file to parse taps with Coq notations | Jason Gross | 2018-02-14 | |
| | ||||
* | Add some string utility functions | Jason Gross | 2018-02-13 | |
| | ||||
* | Add string conversions | Jason Gross | 2018-02-11 | |
| | ||||
* | Split off ZRange lemmas | Jason Gross | 2018-02-10 | |
| | ||||
* | Add some ZRange operations | Jason Gross | 2018-02-10 | |
| | ||||
* | minor updates needed to make it compile with bbv | Samuel Gruetter | 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 ↵ | Samuel Gruetter | 2018-02-05 | |
| | | | | directory | |||
* | Add x25519 donna versions with the new way of generating C code | Jason Gross | 2018-01-15 | |
| | ||||
* | Generate fecarry for solinas | Jason Gross | 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 | Jason Gross | 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 | Andres Erbsen | 2018-01-09 | |
| | ||||
* | Jacobian coordinates | Andres Erbsen | 2018-01-09 | |
| | ||||
* | Add Tactics.RunTacticAsConstr | Jason Gross | 2017-11-26 | |
| | ||||
* | Move DemoWithReification.v => Experiments/SimplyTypedArithmetic.v | Jason Gross | 2017-11-24 | |
| | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/271#discussion_r152720545 | |||
* | Make a copy of Demo.v | Jason Gross | 2017-11-24 | |
| | ||||
* | Add ModInv autosolver | Jason Gross | 2017-11-16 | |
| | ||||
* | Update GeneralizeVar to ensure Wf | Jason Gross | 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 | Jason Gross | 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 | Jason Gross | 2017-11-13 | |
| | ||||
* | Add autosolve admit package | Jason Gross | 2017-11-12 | |
| | ||||
* | automatic modifications to _Coqproject with new files | jadep | 2017-11-12 | |
| | ||||
* | Add Decidable2Bool | Jason Gross | 2017-11-11 | |
| | ||||
* | Add ListUtil.Forall | Jason Gross | 2017-11-11 | |
| | ||||
* | More modularity in autosolve | Jason Gross | 2017-11-10 | |
| | ||||
* | Add HeadUnderBinders | Jason Gross | 2017-11-07 | |
| | ||||
* | A bit more reorganization of autosolve | Jason Gross | 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 | Jason Gross | 2017-11-07 | |
| | ||||
* | Add SideConditionFramework | Jason Gross | 2017-11-07 | |
| | ||||
* | Add type of bounded Z | Jason Gross | 2017-11-02 | |
| | ||||
* | make update-_CoqProject | Jason Gross | 2017-11-02 | |
| | ||||
* | Add MapBaseType | Jason Gross | 2017-10-31 | |
| | ||||
* | Add unextend_op | Jason Gross | 2017-10-31 | |
| |