fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	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
\|
*	Add {firstn,skipn}_seq	Jason Gross	2017-03-19
\|
*	Finish CompileInterp proof	Jason Gross	2017-03-19
\|
*	Split up ContextProperties	Jason Gross	2017-03-19
\|
*	Add mname_list_unique_nil	Jason Gross	2017-03-19
\|
*	Add more ContextProperties	Jason Gross	2017-03-19
\|
*	generalize In_firstn_skipn_split	Jason Gross	2017-03-19
\|
*	Add In_firstn_skipn_split	Jason Gross	2017-03-19
\|
*	Add {m,o,}name_list_unique	Jason Gross	2017-03-19
\|
*	Add firstn_firstn_min	Jason Gross	2017-03-19
\|
*	Add Addmitted correctness for MapCastByDeBruijn	Jason Gross	2017-03-19
\|
*	Add dummy TWord constructor to syntax type	Jason Gross	2017-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.
*	Minor simplification in SmartBound	Jason Gross	2017-03-18
\|
*	Add dec_eq_positive	Jason Gross	2017-03-17
\|
*	Switch to more robust automation in MapCastInterp	Jason Gross	2017-03-17
\|
*	Add default_names_for{,f}	Jason Gross	2017-03-17
\|
*	Add IdContext	Jason Gross	2017-03-17
\|
*	Revert "Have cast_op return exprf instead of op"	Jason Gross	2017-03-17
\| \| \| \| \| \|	This reverts commit bcfcb5e91011ad0dda68e2b41f871058cf890a3c. Doesn't actually build
*	Have cast_op return exprf instead of op	Jason Gross	2017-03-17
\| \| \| \|	cc @andres-erbsen
*	Add MapCastByDeBruijn on PHOAS syntax	Jason Gross	2017-03-17
\|
*	Don't pass a wf proof into InterpToPHOAS	Jason Gross	2017-03-17
\| \| \| \| \|	Use a fail-value instead. This makes it easier to compose with other transformations.
*	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.
*	Update crypto-defects.md	Andres Erbsen	2017-03-16
\| \| \|	https://blogs.adobe.com/security/2017/03/critical-vulnerability-uncovered-in-json-encryption.html
*	[travis] Only build the lite target on Coq 8.5	Jason Gross	2017-03-16
\| \| \| \|	This closes #122
*	Add a "lite" target	Jason Gross	2017-03-15
\| \| \| \| \| \| \|	This builds everything in the default target except WeierstrassCurveTheorems.vo, which, I believe, is the slowest file. This closes #129.
*	Fix a name clash	Jason Gross	2017-03-14
\|
*	Add split_{m,o,}names_firstn_skipn and co.	Jason Gross	2017-03-14
\|
*	Add firstn_skipn	Jason Gross	2017-03-14
\|
*	Add split_prod	Jason Gross	2017-03-14
\|
*	Add NameUtilProperties	Jason Gross	2017-03-14
\|
*	Add skipn_skipn	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOASInterp	Jason Gross	2017-03-14
\|
*	Add Wf_InterpToPHOAS	Jason Gross	2017-03-14
\|
*	Remove useless hyps	Jason Gross	2017-03-14
\|
*	Add InterpretToPHOAS	Jason Gross	2017-03-14
\|
*	Move find_if_eq to Decidable.v, use Decidable in Named	Jason Gross	2017-03-14
\|
*	Add ContextProperties	Jason Gross	2017-03-14
\|
*	Remove useless imports	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 faster versions of destruct_head_*	Jason Gross	2017-03-14
\| \| \| \|	Sometimes, it's a performance bottleneck
*	Fix more unfolding	Jason Gross	2017-03-10
\|
*	Fix more unfolding that shouldn't happen	Jason Gross	2017-03-10
\|
*	Make sure interp_flat_type isn't unfolded in SmartMap	Jason Gross	2017-03-10
\|
*	Add better SmartFlatTypeMapInterp2	Jason Gross	2017-03-08
\|
*	Remove interp_genf from Named/Syntax	Jason Gross	2017-03-08
\|
*	Remove stuff from Reflection/Named/Syntax	Jason Gross	2017-03-08
\|