fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	More partial proofs	Jason Gross	2016-11-06
\|
*	Prove inversion principles for bounded words	Jason Gross	2016-11-06
\|
*	Plug in boundedness proofs	Jason Gross	2016-11-05
\| \| \| \| \|	We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely.
*	Add better bounded lemmas to reified things	Jason Gross	2016-11-05
\|
*	Add eta-expansion in GF25519BoundedCommon.v	Jason Gross	2016-11-05
\| \| \| \|	It'll be needed to vm_compute some proofs in GF25519Reflective/Reified/*
*	Add proofs about boundedness to GF25519Reflective/Common.v	Jason Gross	2016-11-05
\|
*	Add unfold_is_bounded	Jason Gross	2016-11-05
\|
*	Add related_word64_boundsi'	Jason Gross	2016-11-05
\| \| \| \|	This definition needs a better name...
*	Add code for overflow check (disabled bc freeze)	Jason Gross	2016-11-05
\| \| \| \| \| \| \|	Currently freeze overflows; Jade says this is because the carry chain got reversed, and that she'll work on fixing this. We should enable the sanity checks at some point after this is fixed, to fail early if things overflow.
*	Split off some things from Interpretations	Jason Gross	2016-11-05
\|
*	Fix implicit arguments	Jason Gross	2016-11-05
\|
*	Remove pasted code that shouldn't've been in a file	Jason Gross	2016-11-05
\|
*	Add proj1_from_option2	Jason Gross	2016-11-05
\|
*	Fix implicits	Jason Gross	2016-11-05
\|
*	Fix a proof broken by previous commit	Jason Gross	2016-11-05
\|
*	Another projection function	Jason Gross	2016-11-05
\|
*	Z.ltb_to_lt now works in the goal, too	Jason Gross	2016-11-05
\|
*	Add reflect_iff_gen to Bool.v	Jason Gross	2016-11-05
\|
*	More judgmental unification in Z.Interpretations	Jason Gross	2016-11-05
\|
*	Add proj_option2 to Z.Interpretations	Jason Gross	2016-11-05
\|
*	Work around a bug in 8.4 vm_compute	Jason Gross	2016-11-05
\|
*	Fix implicits of Let for 8.4	Jason Gross	2016-11-04
\|
*	put EdDSA encoding sign bit at the MSB	Andres Erbsen	2016-11-04
\|
*	fix extraction directives -- tested enc((l+1)B)=enc(B)	Andres Erbsen	2016-11-03
\|
*	separate Ed25519Extraction.v, add extraction to Makefile	Andres Erbsen	2016-11-03
\| \| \| \| \|	@JasonGross: src/Specific/GF25519Bounded.v has another constant that I think needs a extraction-friendly version, I added a comment
*	Shove Z.Interpretations into closer alignment	Jason Gross	2016-11-03
\| \| \| \|	There's some really terrible code taking advantage of the fact that we only interpret a single type
*	fix Word64 constants for extraction, check in more extraction directives	Andres Erbsen	2016-11-03
\|
*	Rearrangement to different judgmentally equal terms	Jason Gross	2016-11-03
\| \| \| \|	This will hopefully help out the reification algorithm
*	Add more projections in interpretations	Jason Gross	2016-11-03
\|
*	Fix 8.4 build partially	Jason Gross	2016-11-03
\|
*	Add more interpretation things	Jason Gross	2016-11-03
\|
*	Fix build	Jason Gross	2016-11-03
\|
*	More relatedness	Jason Gross	2016-11-03
\|
*	Make apply things go through interp_flat_type	Jason Gross	2016-11-03
\|
*	Make apply things go through interp_flat_type	Jason Gross	2016-11-03
\|
*	Versions of [Apply] that guarantee flat things	Jason Gross	2016-11-03
\|
*	Add more relatedness things	Jason Gross	2016-11-03
\|
*	Make [freeze] proofs consider machine integer width and hard input bounds ↵	jadep	2016-11-03
\| \| \| \|	separately
*	Fix bounds that were reversed	Jason Gross	2016-11-03
\|
*	Fix Not_found exception in 8.4	Jason Gross	2016-11-03
\| \| \| \| \|	Caused by rewriting with a hypothesis with a type of the form [?1 x y] where [?1] is an evar.
*	Clean up fe25519_word64ize, give examples	Jason Gross	2016-11-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/commit/dc8a141d13984bc39cf7523856b678a48428dbcc#commitcomment-19672297 Previously, the proofs were not unfolding the boolean comparisons that eliminate opaque proofs from the resulting proof term. We have to jump through a number of hoops because Coq is really bad at dealing with big terms, and so since we can't unfold all of the identifiers early, we unfold some of them and alias other ones, so that we can unfold the right ones with a hopefully-not-too-long cbv list at the end. (This would be a lot prettier if wish #4473 (https://coq.inria.fr/bugs/show_bug.cgi?id=4473) were granted.)
*	fix and prove ERepDec_correct	Andres Erbsen	2016-11-02
\|
*	add type-compatible SHA512 wrapper	Andres Erbsen	2016-11-02
\|
*	Fix divergence of Ltac match in 8.4	Jason Gross	2016-11-02
\|
*	Fix diverging Qed in 8.5{,pl1} ([f_equal] is broken)	Jason Gross	2016-11-02
\|
*	Fix broken proof	Jason Gross	2016-11-02
\| \| \| \|	See https://github.com/mit-plv/fiat-crypto/commit/254aa1f3ce33dd190f7fee8946fb3c950142aa4c#commitcomment-19671361
*	Fix a possibly-diverging Qed in 8.4 (feEnc_correct)	Jason Gross	2016-11-02
\|
*	Work around divergence of unification in Coq 8.5{,pl1}	Jason Gross	2016-11-02
\|
*	Write code to lift option types over tuples	Jason Gross	2016-11-02
\|
*	Ed25519: use fully qualified names for [a] and [d]	Andres Erbsen	2016-11-02
\|