fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
\| * \|	More Coq 8.4pl2 fixes	Jason Gross	2016-06-11
\| \| \|
\| * \|	Fix for Coq 8.4pl2	Jason Gross	2016-06-11
\| \| \|
\| * \|	Work around bug #4811 (slow f_equal)	Jason Gross	2016-06-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=4811, [f_equal] loops(?) in 8.5pl1 (fixed already in 8.5.dev)
* \| \|	starting rewrite using different definition of map	jadep	2016-06-11
\| \| \|
\| * \|	Minor 8.5 changes	Jason Gross	2016-06-10
\| \| \|
\| * \|	More changes for 8.5	Jason Gross	2016-06-10
\| \| \| \| \| \| \| \| \| \| \| \|	[Local Coercion :=] changed meanings. Use [Let] and [Local Coercion] for consistent behavior
\| * \|	8.5 fixes	Jason Gross	2016-06-10
\|/ /
\| *	improved generic field library	Andres Erbsen	2016-06-10
\| \|
\| *	improve generic field library	Andres Erbsen	2016-06-10
\| \|
\| *	experiment	Andres Erbsen	2016-06-07
\| \|
\| *	generic field definition	Andres Erbsen	2016-06-07
\| \|
\| *	ed25519: refactor some Proper	Andres Erbsen	2016-06-06
\| \|
\| *	rewrite in Let_In binder by tactic	Andres Erbsen	2016-06-04
\| \|
\| *	Let_In rewriting	Andres Erbsen	2016-06-03
\| \|
\| *	leibniz equal version of topdown rewriting of sigma types: nicer	Andres Erbsen	2016-06-01
\| \|
\| *	leibniz equal version of topdown rewriting of sigma types	Andres Erbsen	2016-06-01
\| \|
\| *	E impl: proper morphisms are hard to dow without setoids	Andres Erbsen	2016-05-30
\| \|
\| *	ERep add	Andres Erbsen	2016-05-29
\| \|
\| *	--amend	Andres Erbsen	2016-05-28
\| \|
\| *	verify derivation, EdDSA layer: allow arbitrary equivalence relation for ↵	Andres Erbsen	2016-05-28
\| \| \| \| \| \| \| \|	ERep and SRep
\| *	verify derivation, EdDSA layer: remove unused context variables	Andres Erbsen	2016-05-28
\| \|
\| *	verify derivation: EdDSA layer	Andres Erbsen	2016-05-28
\| \|
\| *	right after scalars to F l	Andres Erbsen	2016-05-27
\| \|
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-05-25
\|\
* \|	Fixed Encoding/PointEncodingTheorems; imports had been deleted, but for some ↵	jadep	2016-05-25
\| \| \| \| \| \| \| \|	reason I wasn't affected. Also updated the same file to use E module.
\| *	ed25519: indentation fix	Andres Erbsen	2016-05-24
\| \|
\| *	ed25519: integrate FRepPow and FRepInv	Andres Erbsen	2016-05-24
\| \|
\| *	ed25519: continue refactor	Andres Erbsen	2016-05-24
\| \|
\| *	PrimeFieldTheorems fermat inverse lemma: prove admit	Andres Erbsen	2016-05-24
\| \|
\| *	Factor some rewrites into a single [autorewrite]	Jason Gross	2016-05-24
\| \| \| \| \| \| \| \|	Slightly less [apply f_equal] beforehand, more automation.
\| *	Remove unfolding, rewrite -> setoid_rewrite	Jason Gross	2016-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Moving the [scalar] argument to the beginning of [iter_op] makes inference of the [Proper] lemmas a bit easier. Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows [setoid_rewrite] to work; since [setoid_rewrite] does more unfolding than [rewrite], we no longer need to unfold things to make the [rewrite] work.
\| *	Fix some issues in Ed25519 tactics	Jason Gross	2016-05-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Use replace rather than refine to speed up [Defined] and make the tactics easier to read - Use [apply f_equal] in place of [reflexivity] for unknown presumably arcane reasons to satisfy Coq's unifier - Factor out some tactics into tactic scripts - Write a lemma to pull functions out of [Let_In] - Fix autoindentation in emacs by wrapping [Let_In_unRep] in parentheses (probably a ProofGeneral regexp gone wrong) - Write a kludgy tactic to unfold [proj1_sig] only when applied to [exist] (Pair programming with Andres)
\| *	F,Ed25519: integrate F representation for mul,add,sub. Ed25519 even more ↵	Andres Erbsen	2016-05-24
\| \| \| \| \| \| \| \|	broken...
* \|	First stage of canonicalization proofs complete; proved 3 carry loops reduce ↵	jadep	2016-05-20
\| \| \| \| \| \| \| \|	input digits to their minimal widths. Remaining : name fixes and second stage -- proving that we subtract q iff the reduced input is over q (in the range [2^k-c, 2^k-1])
\| *	F: pow_nat_iter_op_correct	Andres Erbsen	2016-05-18
\| \|
\| *	F: fermat inversion lemma refactor	Andres Erbsen	2016-05-18
\| \|
\| *	unifiedAddM1Rep_sig: almost there	Andres Erbsen	2016-05-18
\| \|
\| *	slightly nicer edwards curve extended coordinates addition	Andres Erbsen	2016-05-18
\|/
*	Implemented subtraction mod q as as (sub a b = sub (add a (2*q)) b) to avoid ↵	jadep	2016-05-09
\| \| \| \|	unsigned integer underflow. Also changed rep in Specific proofs so that it is PseudoMersenneBaseRep.rep rather than ModularBaseSystem.rep; these are equivalent but the first is the abstraction level we want.
*	Changed name of Encoding to CanonicalEncoding, and changed notation to match.	jadep	2016-04-29
\|
*	Moved sign_bit definition to Spec.	jadep	2016-04-29
\|
*	Proved decode_point_eq in Ed25519 (comparing encodings is equivalent to	jadep	2016-04-29
\| \| \| \|	comparing points).
*	Cleanup: mostly moving lemmas to Util files, some moving lemmas to more ↵	jadep	2016-04-28
\| \| \| \|	general contexts.
*	Completed encoding reorganization; factored sign_bit out of PointEncodings ↵	jadep	2016-04-28
\| \| \| \|	and finished encoding admits.
*	ed25519: solve elliptic curve math admits	Andres Erbsen	2016-04-25
\|
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-25
\|\
* \|	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-04-25
\| \| \| \| \| \| \| \|	function.
\| *	refactor field lemmas out of ed25519	Andres Erbsen	2016-04-25
\| \|