fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	remove eq_dec from Monoid	Andres Erbsen	2016-08-23
\|
*	[cbv beta] in the beginning of Obligation Tactic for 8.5	Andres Erbsen	2016-08-08
\|
*	[F] has its own module now	Andres Erbsen	2016-08-05
\| \| \| \| \| \|	[ZToField] -> [F.of_Z] [FieldToZ] -> [F.to_Z] [Zmod.lem] -> [F.lem]
*	Refactor ModularArithmetic into Zmod, expand Decidable	Andres Erbsen	2016-08-04
\| \| \| \| \| \| \| \| \| \| \| \|	ModularArithmetic now uses Algebra lemmas in various places instead of custom manual proofs. Similarly, Util.Decidable is used to state and prove the relevant decidability results. Backwards-incompatible changes: F_some_lemma -> Zmod.some_lemma Arguments ZToField _%Z _%Z : clear implicits. inv_spec says inv x * x = 1, not x * inv x = 1
*	compute on [F q]!	Andres Erbsen	2016-07-20
\|
*	remove field_algebra	Andres Erbsen	2016-07-11
\|
*	added proofs about addition chain exponentiation for later use in ↵	jadep	2016-07-10
\| \| \| \|	ModularBaseSystem [pow], which we need for sqrt and inversion.
*	Define the spec of Weierstrass curves (#6)	Jason Gross	2016-07-03
\| \| \| \| \|	Define the spec of Weierstrass curves This is the start of work on P256.
*	scalarmult support; EdDSA.sign produces valid signatures	Andres Erbsen	2016-06-27
\|
*	EdDSA: prove things about spec	Andres Erbsen	2016-06-25
\|
*	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\|
*	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\|
*	Handle renaming of NPeano.pow to Nat.pow (#3)	Jason Gross	2016-06-22
\| \| \| \|	We leave ambiguous which [pow] and [modulo] we refer to, so that this builds in both 8.4 and 8.5
*	EdDSA.v: resolve ambiguity based on ed25519.py	Andres Erbsen	2016-06-21
\|
*	Whitespace change	Jason Gross	2016-06-21
\|
*	use Local Obligation Tactic (8.5-compat)	Andres Erbsen	2016-06-21
\|
*	remove trailing whitespace from src/	Andres Erbsen	2016-06-20
\|
*	Remove anything incompatible with new algebraic hierarcy	Andres Erbsen	2016-06-20
\| \| \| \| \| \|	- PointEncoding (these will hopefully come back soon) - EdDSAProofs (not a priority to bring back, but not hard either) - Ed25519 spec bits and pieces which were not finished anyway
*	Merge branch 'field-experiment'	Andres Erbsen	2016-06-20
\|\ \| \| \| \| \| \|	includes broken files to be removed in next commit
\| *	port EdDSA spec	Andres Erbsen	2016-06-20
\| \|
\| *	move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems	Andres Erbsen	2016-06-17
\| \|
\| *	port edwards curve spec	Andres Erbsen	2016-06-16
\| \|
* \|	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
\| *	before changing SRep from N to F l	Andres Erbsen	2016-05-27
\|/
*	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
\|
*	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.
*	consolidate and rename Edwards curve lemmas	Andres Erbsen	2016-04-25
\|
*	Reorganization and revision of Encoding code and redefinition of sign_bit ↵	jadep	2016-04-25
\| \| \| \|	function.
*	point_eq_dec	Andres Erbsen	2016-04-22
\|
*	ed25519: continue derivation	Andres Erbsen	2016-04-08
\|
*	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
\|
*	instantiate ed25519 sign in spec	Andres Erbsen	2016-03-20
\|
*	Ed25519: d is nonsquare	Andres Erbsen	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 ```
*	Factor out some bedrock dependencies into WordUtil	Jason Gross	2016-02-25
\| \| \| \|	Also move a definition about words, with a TODO about location, into WordUtil.
*	efficient powmod	Andres Erbsen	2016-02-17
\|
*	removed Print Assumptions	Jade Philipoom	2016-02-16
\|
*	moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from ↵	Jade Philipoom	2016-02-16
\| \| \| \|	CompleteEdwardsCurve, where the precondition is not in scope.
*	proved most of point encoding admits, fixed some build system issues (dead ↵	Jade Philipoom	2016-02-16
\| \| \| \|	imports of PointFormats and Galois things)
*	added point encodings; some admits remain	Jade Philipoom	2016-02-16
\|
*	EdDSA: tweaked l_bound	Jade Philipoom	2016-02-15
\|
*	merge	Jade Philipoom	2016-02-15
\|\
* \|	instantiated FqEncoding and FlEncoding (also fixed indentation, which is why ↵	Jade Philipoom	2016-02-15
\| \| \| \| \| \| \| \|	the commit looks huge)
* \|	added generic encoding spec	Jade Philipoom	2016-02-15
\| \|
\| *	Finish seperating our specs: remove old non-specified code	Andres Erbsen	2016-02-15
\|/