fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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.
*	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 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.
*	Split off BoundedWord.v from IntegrationTest.v	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
\|
*	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
\|
*	Add a bounds relaxation lemma	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
*	Start instantiating MapCastByDeBruijn in Z/	Jason Gross	2017-03-30
\|
*	Don't linearize and eta in MapCastByDeBruijn	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
*	Add a file dedicated to the definition of Z bounds	Jason Gross	2017-03-30
\|
*	Add Z.FoldTypes.{Min,Max}TypeUsed	Jason Gross	2017-03-28
\|
*	Add FoldTypes	Jason Gross	2017-03-28
\|
*	make update-_CoqProject	Jason Gross	2017-03-28
\|
*	Added saturated arithmetic file, including [compact] code and proof	jadep	2017-03-24
\|
*	Add aborted CompileProperties	Jason Gross	2017-03-22
\| \| \| \| \|	This is an attempt to prove that the default counts of let binders are enough.
*	Add aborted MapCastByDeBruijnWf	Jason Gross	2017-03-19
\| \| \| \| \| \| \| \|	I'm not sure exactly why the wf proof requires cast_backb in map_cast; it seems to be used as a dumb way of instantiating the context-extension on the input expression tree (since we're only given the context-extension values on the output expression, which has a different type).
*	Add MapCastWf	Jason Gross	2017-03-19
\|
*	Most of the way towards a complete MapCastCorrect	Jason Gross	2017-03-19
\|
*	Add Named/PositiveContext/DefaultsProperties.v	Jason Gross	2017-03-19
\|
*	Split up ContextProperties	Jason Gross	2017-03-19
\|
*	Add IdContext	Jason Gross	2017-03-17
\|
*	Add MapCastByDeBruijn on PHOAS syntax	Jason Gross	2017-03-17
\|
*	Add aborted in-process compile-{wf,interp} proofs	Jason Gross	2017-03-17
\|
*	Add a Named version of MapCast	Jason Gross	2017-03-17
\| \| \| \|	Based on Andres' work towards #123.
*	Add NameUtilProperties	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOASInterp	Jason Gross	2017-03-14
\|
*	Add Wf_InterpToPHOAS	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOAS	Jason Gross	2017-03-14
\|
*	Add ContextProperties	Jason Gross	2017-03-14
\|
*	Move ContextOk to ContextDefinitions	Jason Gross	2017-03-14
\|
*	Add lemma about wff and interpf of Named	Jason Gross	2017-03-14
\|
*	Add FMapContext, PositiveContext	Jason Gross	2017-03-08
\| \| \| \| \|	Also copy some definitions from Syntax out of it, in prep for removing them
*	Separated out specific test cases for new base system	jadep	2017-03-04
\|
*	remove dangling file...	Andres Erbsen	2017-03-02
\|
*	deleted src/Specific/GF25519ExtendedAddCoordinates.v	Andres Erbsen	2017-03-02
\|
*	fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v	Andres Erbsen	2017-03-02
\|
*	PrimeFieldTheorems: inv for isomorphic fields	Andres Erbsen	2017-03-02
\|
*	address some code review comments	Andres Erbsen	2017-03-02
\|
*	Weierstrass curve is a group	Andres Erbsen	2017-03-02
\|