fiat-crypto - fast, formally verified cryptography

	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
*	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.
*	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
\|
*	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
\|
*	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
*	Start instantiating MapCastByDeBruijn in Z/	Jason Gross	2017-03-30
\|
*	Reorder arguments to Wf_MapCast for eauto	Jason Gross	2017-03-30
\| \| \| \|	This way we pick up the equality hypothesis first.
*	Don't linearize and eta in MapCastByDeBruijn	Jason Gross	2017-03-30
\|
*	Revert "Update CNotations, JavaNotations"	Jason Gross	2017-03-30
\| \| \| \| \| \|	This reverts commit 16d3eb50638fc280b790aff9cdaa6d28cbb42c8a. I forgot that I hadn't merged the changes to Z.Syntax.op yet.
*	Update CNotations, JavaNotations	Jason Gross	2017-03-30
\|
*	Rename Bounds to ZRange, use Prop, not bool	Jason Gross	2017-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 BoundsInterpretations	Jason Gross	2017-03-30
\|
*	More robust reifier	Jason Gross	2017-03-29
\| \| \| \| \|	We no longer need to rely on judgmental equality in the interpretation of OpConst.
*	Add Z.FoldTypes.{Min,Max}TypeUsed	Jason Gross	2017-03-28
\|
*	Add FoldTypes	Jason Gross	2017-03-28
\|
*	Add Wf_MapCast_arrow	Jason Gross	2017-03-28
\|
*	Add InterpExprEta_arrow	Jason Gross	2017-03-28
\|
*	Add Wf_MapCast to wf database	Jason Gross	2017-03-28
\|
*	Break up MapCast into separate pieces for easier debugging	Jason Gross	2017-03-28
\|
*	Finish proof of wf_map_cast	Jason Gross	2017-03-28
\| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change --------------------------------------------------------------------- 0m20.75s \| Total \| 0m15.19s \|\| +0m05.56s --------------------------------------------------------------------- 0m19.33s \| Reflection/Named/MapCastWf \| 0m13.82s \|\| +0m05.50s 0m00.79s \| Reflection/MapCastByDeBruijnInterp \| 0m00.75s \|\| +0m00.04s 0m00.64s \| Reflection/MapCastByDeBruijnWf \| 0m00.62s \|\| +0m00.02s
*	Do more subst in ContextProperties/Tactics	Jason Gross	2017-03-28
\|
*	Add find_Name_and_val_SmartFlatTypeMapUnInterp2_Some_Some	Jason Gross	2017-03-28
\|
*	Add SmartVarfMap3 arguments	Jason Gross	2017-03-28
\|
*	Add SmartVarfMap3	Jason Gross	2017-03-28
\|
*	Add Bounds.dec_eq_interp_flat_type	Jason Gross	2017-03-27
\|
*	Fix binder counting in MapCastByDB	Jason Gross	2017-03-22
\| \| \| \| \|	We were previously counting the names we'd need before linearizing. Oops.
*	Add aborted CompileProperties	Jason Gross	2017-03-22
\| \| \| \| \|	This is an attempt to prove that the default counts of let binders are enough.