fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add NameUtilProperties	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
\|
*	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
\|
*	Add FMapContext, PositiveContext	Jason Gross	2017-03-08
\| \| \| \| \|	Also copy some definitions from Syntax out of it, in prep for removing them
*	make 8.5 happy	Andres Erbsen	2017-03-02
\|
*	Adjust implicits of flatten_binding_list_same_in_eq	Jason Gross	2017-03-01
\|
*	Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq	Jason Gross	2017-03-01
\|
*	Switch to fully uncurried form for reflection	Jason Gross	2017-03-01
\| \| \| \| \| \| \| \| \| \| \|	This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes.
*	Add interp_flat_type_rel_pointwise_SmartVarfMap, ↵	Jason Gross	2017-02-28
\| \| \| \|	interp_flat_type_rel_pointwise_Reflexive
*	Add SmartVarfMap Proper instance	Jason Gross	2017-02-28
\|
*	Deduplicate code	Jason Gross	2017-02-28
\| \| \| \|	There was duplicate code in Reflection.Equality and Reflection.TypeInversion
*	Add BoundsInterpretations	Jason Gross	2017-02-23
\|
*	Minor change to reflection naming	Jason Gross	2017-02-23
\|
*	Add various reflection improvements, boundbycast	Jason Gross	2017-02-21
\|
*	Add interpf_smart_bound without exprf	Jason Gross	2017-02-21
\|
*	Rename Interp lemmas	Jason Gross	2017-02-21
\| \| \| \| \| \|	```bash $ git grep --name-only 'Interp_InlineCast\\|Interp_InlineConst\\|Interp_Linearize' \| xargs sed s'/Interp_/Interp/g' -i ```
*	Add non-exprf version of interpf_smart_unbound	Jason Gross	2017-02-16
\|
*	Add MapCastInterp	Jason Gross	2017-02-16
\|
*	Add InterpByIsoProofs	Jason Gross	2017-02-16
\|
*	Fix typo	Jason Gross	2017-02-16
\|
*	Add InterpByIso	Jason Gross	2017-02-16
\| \| \| \| \| \|	It's actually closer to interp_by_retraction... This lets you do [interp] on, e.g., products with fail-values (var * interp_base), as long as [var] is pointed.
*	Add rudimentary Java and C notation files, display	Jason Gross	2017-02-15
\|
*	Remove useless comment	Jason Gross	2017-02-14
\|
*	Mostly finish Wf_Boundify	Jason Gross	2017-02-14
\|
*	Prove wff_bound_op	Jason Gross	2017-02-14
\|
*	Stub for wff_bound_op	Jason Gross	2017-02-14
\|
*	Add Wf_MapInterpCast to wf database	Jason Gross	2017-02-14
\|
*	A bit more progress on BoundByCastWf	Jason Gross	2017-02-14
\|
*	Add partially finished MapCastWf	Jason Gross	2017-02-14
\|
*	Add src/Reflection/BoundByCastWf.v	Jason Gross	2017-02-14
\|
*	Update assumptions in src/Reflection/SmartBoundWf.v	Jason Gross	2017-02-14
\|
*	Add SmartBoundWf	Jason Gross	2017-02-14
\|
*	Prove nicer version of wf_SmartAbs	Jason Gross	2017-02-13
\|
*	Add partially admitted lemma wf_SmartAbs	Jason Gross	2017-02-13
\|
*	More uniform naming	Jason Gross	2017-02-13
\|
*	Generalize EtaWf some (still one admit)	Jason Gross	2017-02-13
\|
*	Add InlineCastInterp.v	Jason Gross	2017-02-13
\|