| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add InterpEta |  Jason Gross | 2017-04-02 |
| | | | | | It's a version of [Interp] that works even when there are destructuring lets. | ||
| * | Remove the bits of the new reflective pipeline in master | Jason Gross | 2017-04-02 |
| | | | | | This way, we can keep all of new pipeline code together in the PR | ||
| * | Remove all the .v files in SpecificGen | Jason Gross | 2017-04-02 |
| | | | | | This gets most of the way to 10 in #14. | ||
| * | More extensive comment in NewBaseSystem | Jason Gross | 2017-04-02 |
| | | | | | As per Andres' request on #138. | ||
| * | Work around bug #5434 | Jason Gross | 2017-04-02 |
| | | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5434, [vm_compute] breaks an invariant asserted on line 115 of pretyping/constr_matching.ml. This was triggering whenever we tried to reify one of the operations. | ||
| * | Coalesce Tuple.pointwise2 and Tuple.fieldwise | Jason Gross | 2017-04-02 |
| | | | | | | | We don't need both of them. We keep the definition of pointwise2 because it's needed for reification to work, and we keep the name of fieldwise because it's used in more places. This closes #137. | ||
| * | Generalize Z.InterpInlineConst | Jason Gross | 2017-04-02 |
| | | |||
| * | Better version of inversion_ProcessedReflectivePackage | Jason Gross | 2017-04-02 |
| | | | | | Now it doesn't introduce needless dependencies | ||
| * | Add inversion_ProcessedReflectivePackage | Jason Gross | 2017-04-02 |
| | | |||
| * | Add PreDefinitions pipeline file | Jason Gross | 2017-04-02 |
| | | |||
| * | Add Z instantiations of InlineConst | Jason Gross | 2017-04-02 |
| | | |||
| * | Add Z.Bounds.MapCastByDeBruijn instantiation | Jason Gross | 2017-04-02 |
| | | |||
| * | Add Z instantiation of MapCastByDeBruijnInterp | Jason Gross | 2017-04-02 |
| | | |||
| * | Add reflective_interp rewrite db | Jason Gross | 2017-04-02 |
| | | |||
| * | Rewrite in Op arguments before rewriting in Op | Jason Gross | 2017-04-01 |
| | | | | | This fixes the rewriter to actually simplify deeply nested expressions. | ||
| * | Also do eta under lets in Reflection/Eta.v | Jason Gross | 2017-04-01 |
| | | |||
| * | Add an initial glue file in the pipeline, no option in bounds | Jason Gross | 2017-04-01 |
| | | | | | | | | We can do bounds analysis without options. Also, add some tactics from another branch for the glue to start the reflective pipeline. | ||
| * | Fix definition of BoundedWord | Jason Gross | 2017-04-01 |
| | | | | | | | | We need to take log2, because wordT takes lg(wordsize). We need to pass None rather than Some, because None means "the original output type of the function we're reifying is a tuple of Z" (as opposed to a tuple of words), which is the situation we're in. | ||
| * | Split off BoundedWord.v from IntegrationTest.v | Jason Gross | 2017-04-01 |
| | | |||
| * | Add back word hex constant notations | Jason Gross | 2017-04-01 |
| | | |||
| * | Add RenameBinders | Jason Gross | 2017-04-01 |
| | | | | | | It will someday allow for nicely named PHOAS binders (conditional on https://coq.inria.fr/bugs/show_bug.cgi?id=5414 being solved). | ||
| * | Add wf proof for arithmetic simplifer | Jason Gross | 2017-04-01 |
| | | |||
| * | Fix a name (sprurious interp) | Jason Gross | 2017-04-01 |
| | | |||
| * | Add interp proof for arithmetic simplifier | Jason Gross | 2017-04-01 |
| | | |||
| * | Handle inversion of homogenous products in reflective type inversion | Jason Gross | 2017-04-01 |
| | | |||
| * | Add an arithmetic simplifier | Jason Gross | 2017-04-01 |
| | | |||
| * | Add correctness of Rewriter | Jason Gross | 2017-04-01 |
| | | |||
| * | Add Reflection/Rewriter.v | Jason Gross | 2017-04-01 |
| | | |||
| * | Split out Tactics.SubstLet | Jason Gross | 2017-04-01 |
| | | |||
| * | Remove trailing whitespace in NewBaseSystem | Jason Gross | 2017-04-01 |
| | | |||
| * | Add Tuple.eta | Jason Gross | 2017-04-01 |
| | | |||
| * | insert a reduce step in the correct place of the carry chain |  jadep | 2017-04-01 |
| | | |||
| * | Alter relax_output_bounds statement | Jason Gross | 2017-04-01 |
| | | | | | It needs to fit the actual statement of MapBounds correctness | ||
| * | Add a bounds relaxation lemma | Jason Gross | 2017-03-31 |
| | | |||
| * | Add Z.log2_up_le_pow2_full | Jason Gross | 2017-03-31 |
| | | |||
| * | Fix inversion_base_type | Jason Gross | 2017-03-31 |
| | | |||
| * | Add inversion_base_type for Z.Syntax.base_type | Jason Gross | 2017-03-31 |
| | | |||
| * | Add Bounds.is_tighter_thanb | Jason Gross | 2017-03-31 |
| | | |||
| * | Use a better order of arguments for Bounds.is_bounded_by | Jason Gross | 2017-03-31 |
| | | | | | This lines up with conventions that we use elsewhere | ||
| * | Add is_tighter_than_bool to zrange | Jason Gross | 2017-03-31 |
| | | |||
| * | More compatibility for etransitivity | Jason Gross | 2017-03-31 |
| | | |||
| * | Add [change_with_curried] to Curry.v | Jason Gross | 2017-03-31 |
| | | |||
| * | Add [etransitivity y], [etransitivity_rev] tactics | Jason Gross | 2017-03-31 |
| | | |||
| * | use improved fsatz on various elliptic curve things |  Andres Erbsen | 2017-03-31 |
| | | | | | | | | | partial correctness of projective addition stronger projective addition proof fixup | ||
| * | Add a comment explaining bounds_exp | Jason Gross | 2017-03-30 |
| | | |||
| * | Add wordToZ{_gen,}_range | Jason Gross | 2017-03-30 |
| | | |||
| * | Update IntegrationTest with actual bounds | Jason Gross | 2017-03-30 |
| | | | | | Also make mulZ not opaque. | ||
| * | Start instantiating MapCastByDeBruijn in Z/ | Jason Gross | 2017-03-30 |
| | | |||
| * | Created test file for newbasesystem/word-size-selection integration | jadep | 2017-03-30 |
| | | |||
| * | turn [Let]s into [Definition]s so they persist after the section | jadep | 2017-03-30 |
| | | |||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |