Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 | ||
* | 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 |
| | |||
* | make update-_CoqProject | Jason Gross | 2017-10-29 |
| | |||
* | Add MapBaseTypeWf, generalize src/Compilers/MapBaseType.v a bit | Jason Gross | 2017-10-24 |
| | |||
* | Add MapBaseType | Jason Gross | 2017-10-23 |
| | |||
* | Add InlineConstAndOpByRewrite | Jason Gross | 2017-10-23 |
| | |||
* | Add ZExtended/InlineConstAndOp.v | Jason Gross | 2017-10-22 |
| | |||
* | Add StripExpr | Jason Gross | 2017-10-22 |
| | |||
* | Add tight and loose bounds, no carry in add, sub | Jason Gross | 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 | Jason Gross | 2017-10-21 |
| | |||
* | Add ZExtended/Syntax.v | Jason Gross | 2017-10-20 |
| | |||
* | Add GeneralizeVar{Wf,Interp}.v | Jason Gross | 2017-10-20 |
| | |||
* | Add GeneralizeVar | Jason Gross | 2017-10-20 |
| |