aboutsummaryrefslogtreecommitdiff
path: root/src/Reflection/Z
Commit message (Collapse)AuthorAge
* Add [Proof using] to most proofsGravatar Jason Gross2017-04-04
| | | | | | | | This closes #146 and makes `make quick` faster. The changes were generated by adding [Global Set Suggest Proof Using.] to GlobalSettings.v, and then following [the instructions for a script I wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).
* Move sigma MapProjections to a separate fileGravatar Jason Gross2017-04-04
| | | | Allows for more fine-grained imports
* Split off liftn_sig, add lift{3,4}_sigGravatar Jason Gross2017-04-03
|
* Fuse Pipeline.{Composition,ReflectiveTactics}Gravatar Jason Gross2017-04-03
| | | | | They need to be modified together to keep track of the ordering of side-conditions.
* Fix missing unfold in proofGravatar Jason Gross2017-04-03
|
* Add missing parenthesesGravatar Jason Gross2017-04-03
|
* Use projT2_mapGravatar Jason Gross2017-04-03
|
* Finally, a fully working IntegrationTestGravatar Jason Gross2017-04-03
|
* Rework and doc reflective pipeline (more Gallina)Gravatar Jason Gross2017-04-03
|
* Add an initial stab at doing the pipeline mostly in GallinaGravatar Jason Gross2017-04-03
|
* Add a bit more documentationGravatar Jason Gross2017-04-03
|
* Pipeline: reduce away reflective constantsGravatar Jason Gross2017-04-03
| | | | | This makes it so that the term that shows up when the reflective subgoal is solved doesn't include things like [Interp]
* Start adding comments to Pipeline/ReflectiveTactics.vGravatar Jason Gross2017-04-03
|
* Rename PreDefinitions to OutputTypeGravatar Jason Gross2017-04-03
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/141#discussion_r109312653
* Add and update documentation in Pipeline/Glue.vGravatar Jason Gross2017-04-03
|
* An approximately first stab DeBruijn word-size-selGravatar Jason Gross2017-04-03
|
* Remove old reflective pipeline, making way the newGravatar Jason Gross2017-04-03
|
* Remove the bits of the new reflective pipeline in masterGravatar Jason Gross2017-04-02
| | | | This way, we can keep all of new pipeline code together in the PR
* Generalize Z.InterpInlineConstGravatar Jason Gross2017-04-02
|
* Better version of inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
| | | | Now it doesn't introduce needless dependencies
* Add inversion_ProcessedReflectivePackageGravatar Jason Gross2017-04-02
|
* Add PreDefinitions pipeline fileGravatar Jason Gross2017-04-02
|
* Add Z instantiations of InlineConstGravatar Jason Gross2017-04-02
|
* Add Z.Bounds.MapCastByDeBruijn instantiationGravatar Jason Gross2017-04-02
|
* Add Z instantiation of MapCastByDeBruijnInterpGravatar Jason Gross2017-04-02
|
* Add reflective_interp rewrite dbGravatar Jason Gross2017-04-02
|
* Add an initial glue file in the pipeline, no option in boundsGravatar Jason Gross2017-04-01
| | | | | | | We can do bounds analysis without options. Also, add some tactics from another branch for the glue to start the reflective pipeline.
* Add back word hex constant notationsGravatar Jason Gross2017-04-01
|
* Add wf proof for arithmetic simpliferGravatar Jason Gross2017-04-01
|
* Add interp proof for arithmetic simplifierGravatar Jason Gross2017-04-01
|
* Add an arithmetic simplifierGravatar Jason Gross2017-04-01
|
* Alter relax_output_bounds statementGravatar Jason Gross2017-04-01
| | | | It needs to fit the actual statement of MapBounds correctness
* Add a bounds relaxation lemmaGravatar Jason Gross2017-03-31
|
* Fix inversion_base_typeGravatar Jason Gross2017-03-31
|
* Add inversion_base_type for Z.Syntax.base_typeGravatar Jason Gross2017-03-31
|
* Add Bounds.is_tighter_thanbGravatar Jason Gross2017-03-31
|
* Use a better order of arguments for Bounds.is_bounded_byGravatar Jason Gross2017-03-31
| | | | This lines up with conventions that we use elsewhere
* Start instantiating MapCastByDeBruijn in Z/Gravatar Jason Gross2017-03-30
|
* Don't linearize and eta in MapCastByDeBruijnGravatar Jason Gross2017-03-30
|
* Revert "Update CNotations, JavaNotations"Gravatar Jason Gross2017-03-30
| | | | | | This reverts commit 16d3eb50638fc280b790aff9cdaa6d28cbb42c8a. I forgot that I hadn't merged the changes to Z.Syntax.op yet.
* Update CNotations, JavaNotationsGravatar Jason Gross2017-03-30
|
* Rename Bounds to ZRange, use Prop, not boolGravatar Jason Gross2017-03-30
| | | | | | As per @andres-erbsen's comments at https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565223, https://github.com/mit-plv/fiat-crypto/commit/ba864554da71ebe20b2494b1e8adf04779cd904b#commitcomment-21565200
* Use Bounds in BoundsInterpretationsGravatar Jason Gross2017-03-30
|
* More robust reifierGravatar Jason Gross2017-03-29
| | | | | We no longer need to rely on judgmental equality in the interpretation of OpConst.
* Add Z.FoldTypes.{Min,Max}TypeUsedGravatar Jason Gross2017-03-28
|
* Add Bounds.dec_eq_interp_flat_typeGravatar Jason Gross2017-03-27
|
* Add cast_back_flat_constGravatar Jason Gross2017-03-22
|
* Make Z.ltb_to_lt a bit strongerGravatar Jason Gross2017-03-21
| | | | | | | | Now it works not just at top-level, but also in, e.g., arguments to hypotheses. We had to change some proofs because it no longer moves the hypotheses it changes to the bottom.
* Add dummy TWord constructor to syntax typeGravatar Jason Gross2017-03-19
| | | | | This will allow us to use the same syntax type for the new version of word-size selection without needing to rip out all of the old things.
* make 8.5 happyGravatar Andres Erbsen2017-03-02
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 23:31:57 +0000