fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	ed25519: integrate FRepPow and FRepInv	Andres Erbsen	2016-05-24
\|
*	ed25519: continue refactor	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...
*	unifiedAddM1Rep_sig: almost there	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.
*	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).
*	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
\| \|
\| *	reduce admits related to point negation	Andres Erbsen	2016-04-25
\|/
*	point_eq_dec	Andres Erbsen	2016-04-22
\|
*	added GF1305 (modulus is 2^130 - 5, base has length 5 with all digits having ↵	jadep	2016-04-21
\| \| \| \|	weight 2^26)
*	automated most of the code in GF25519	jadep	2016-04-21
\|
*	Cleanup of GF25519	jadep	2016-04-20
\|
*	Pulled generalized code out of GF25519 so that it can be used for other moduli	jadep	2016-04-20
\|
*	GF25519 addition	jadep	2016-04-20
\|
*	GF25519: boring stuff -- fixed indentation and removed commented-out code	jadep	2016-04-20
\|
*	ed25519 derivation: down to final encoding	Andres Erbsen	2016-04-17
\|
*	ed25519 derivation: use representation of F	Andres Erbsen	2016-04-17
\|
*	ed25519 derivation: wrangle non-unique representations	Andres Erbsen	2016-04-16
\|
*	ed25519 derivation: stuck at main loop	Andres Erbsen	2016-04-16
\|
*	ed25519 derivation down to word until main equation	Andres Erbsen	2016-04-16
\|
*	Retrieved updated version of Util/IterAssocOp and modified ↵	jadep	2016-04-14
\| \| \| \|	ExtendedCoordinates and Ed25519 to use it.
*	Fixed syntax error (missing bracket) in Ed25519 to make merge build	jadep	2016-04-12
\|
*	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-04-12
\|\
* \|	Finished refactor of GF25519 (partial evaluation); code builds but needs to ↵	jadep	2016-04-12
\| \| \| \| \| \| \| \|	be reorganized, since many of the theorems in GF25519 are now generalized and do not need to be in Specific/.
* \|	Merge and refactor of GF25519	jadep	2016-04-11
\| \|
\| *	ed25519: continue derivation	Andres Erbsen	2016-04-08
\| \|
* \|	Merge branch 'master' of github.mit.edu:plv/fiat-crypto	jadep	2016-03-30
\|\\|
\| *	Drop second projections in Ed25519	Jason Gross	2016-03-29
\| \|
\| *	ed25519 derivation: pair programming with jgross... slow progress	Andres Erbsen	2016-03-24
\| \|
\| *	nicer verify() derivation starter	Andres Erbsen	2016-03-21
\| \|
\| *	state top-level derivation for Ed25519.verify	Andres Erbsen	2016-03-20
\| \|
* \|	fix of GF25519 in progress; created instantiation of PseudoMersenneBaseParams	Jade Philipoom	2016-03-20
\| \|
\| *	Finish absolutizing imports	Jason Gross	2016-03-10
\|/ \| \| \| \| \| \| \| \| \| \| \|	The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" \| xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-02-16
\| \| \| \|	imports of PointFormats and Galois things)
*	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\|
*	ported some of EdDSA25519 to new field framework	Jade Philipoom	2016-02-15
\|
*	port ModularBaseSystem.v and GF25519.v to F m	Andres Erbsen	2016-02-14
\|
*	Merge branch 'spec' of github.mit.edu:plv/fiat-crypto	Jade Philipoom	2016-02-12
\|\
* \|	EdDSA25519: progress on proving PointEncoding admits; code still unorganized	Jade Philipoom	2016-02-12
\| \|
\| *	port several theorems from GF to F	Andres Erbsen	2016-02-11
\| \|
\| *	remove a dangling About	Andres Erbsen	2016-02-07
\|/