fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	isomorphism_to_subgroup_group	Andres Erbsen	2016-06-24
\|
*	Use Decidable machinery for is_eq_dec	Jason Gross	2016-06-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows us to rely entirely on typeclass resolution to resolve these instances, without having to do ad-hoc things for [and]. After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------ 2m21.71s \| Total \| 2m22.59s \|\| -0m00.87s ------------------------------------------------------------------------------------ 0m28.82s \| Specific/GF25519 \| 0m29.86s \|\| -0m01.03s 0m29.60s \| ModularArithmetic/ModularBaseSystemProofs \| 0m29.40s \|\| +0m00.20s 0m21.25s \| Experiments/SpecEd25519 \| 0m21.28s \|\| -0m00.03s 0m18.15s \| CompleteEdwardsCurve/ExtendedCoordinates \| 0m18.14s \|\| +0m00.00s 0m11.95s \| CompleteEdwardsCurve/CompleteEdwardsCurveTheorems \| 0m11.94s \|\| +0m00.00s 0m07.26s \| Specific/GF1305 \| 0m07.28s \|\| -0m00.02s 0m03.77s \| ModularArithmetic/Tutorial \| 0m03.75s \|\| +0m00.02s 0m03.76s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.75s \|\| +0m00.00s 0m03.61s \| CompleteEdwardsCurve/Pre \| 0m03.63s \|\| -0m00.02s 0m02.15s \| ModularArithmetic/ModularArithmeticTheorems \| 0m02.12s \|\| +0m00.02s 0m01.88s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.89s \|\| -0m00.01s 0m01.75s \| Algebra \| 0m01.73s \|\| +0m00.02s 0m01.21s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m01.17s \|\| +0m00.04s 0m01.14s \| ModularArithmetic/ExtendedBaseVector \| 0m01.14s \|\| +0m00.00s 0m01.01s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.98s \|\| +0m00.03s 0m00.62s \| Encoding/ModularWordEncodingTheorems \| 0m00.63s \|\| -0m00.01s 0m00.60s \| Encoding/ModularWordEncodingPre \| 0m00.61s \|\| -0m00.01s 0m00.59s \| Util/Decidable \| 0m00.64s \|\| -0m00.05s 0m00.58s \| Spec/EdDSA \| 0m00.61s \|\| -0m00.03s 0m00.57s \| ModularArithmetic/ModularBaseSystem \| 0m00.61s \|\| -0m00.04s 0m00.56s \| Spec/ModularWordEncoding \| 0m00.56s \|\| +0m00.00s 0m00.51s \| ModularArithmetic/PseudoMersenneBaseRep \| 0m00.53s \|\| -0m00.02s 0m00.37s \| Spec/CompleteEdwardsCurve \| 0m00.34s \|\| +0m00.02s
*	nsatz_contradict can now handle invalid _ <> _ hypotheses	Jason Gross	2016-06-23
\|
*	Update _CoqProject	Jason Gross	2016-06-23
\|
*	Add Unit.v	Jason Gross	2016-06-23
\|
*	Add equality on sum types	Jason Gross	2016-06-23
\|
*	Merge pull request #8 from mit-plv/rsloan-pipeline-example-init	Jason Gross	2016-06-23
\|\ \| \| \| \|	Make Pipeline.v Build on 8.4
\| *	Remove examples for 8.4 compatibility	Robert Sloan	2016-06-23
\| \|
\| *	Remove vestigal BoundedWord machinery	Robert Sloan	2016-06-23
\| \|
* \|	Improve some tactics and lemmas	Jason Gross	2016-06-23
\| \|
* \|	[break_match] should not be local	Jason Gross	2016-06-23
\| \|
\| *	Remove vestigal GaloisField machinery	Robert Sloan	2016-06-23
\| \|
* \|	Add tactics to Tactics, at most 2 sq-roots to Algebra	Jason Gross	2016-06-23
\| \|
\| *	Update _CoqProject	Robert Sloan	2016-06-23
\| \|
\| *	Make Pipeline.v Build on 8.4	Robert Sloan	2016-06-23
\|/
*	Merge pull request #7 from mit-plv/rsloan-unstable	Rob Sloan	2016-06-23
\|\ \| \| \| \|	Merge Assembly Machinery into Master
\| *	Remove unstable Pipeline.v examples from _CoqProject	Robert Sloan	2016-06-23
\| \|
\| *	Add Language.v, Conversion.v to _CoqProject	Robert Sloan	2016-06-23
\| \|
* \|	surjective homomorphism from group makes a group	Andres Erbsen	2016-06-23
\| \|
\| *	Merge branch 'master' of github.com:mit-plv/fiat-crypto into ↵	Robert Sloan	2016-06-23
\| \|\ \| \|/ \|/\| \| \|	public/rsloan-unstable
\| *	QhasmUtil.v: Remove 8.4-incompatible intro name	Robert Sloan	2016-06-23
\| \|
\| *	Pipeline: several new examples	Robert Sloan	2016-06-23
\| \|
* \|	Make [nsatz_contradict] better at inequalities	Jason Gross	2016-06-23
\| \|
\| *	Pseudize Lemmas for Dual Operations	Robert Sloan	2016-06-23
\| \|
* \|	[field_algebra] now knows that 0 <> -0 is false	Jason Gross	2016-06-23
\| \|
* \|	Work around bug #4851 in nsatz	Jason Gross	2016-06-23
\| \| \| \| \| \| \| \| \| \|	Now our [nsatz] does not barf when you have duplicate equations in the context.
* \|	Add tactics for canonicalizing field (in)equalities	Jason Gross	2016-06-23
\| \|
* \|	Rename the nonzero lemma to an iff lemma	Jason Gross	2016-06-23
\| \|
* \|	Add mul_nonzero_nonzero_and to Algebra.v	Jason Gross	2016-06-23
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Integrate Pseudize into Pipeline.v	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In with minor notations	Robert Sloan	2016-06-23
\| \|
\| *	Pseudize Let_In	Robert Sloan	2016-06-23
\| \|
\| *	Add Pseudize, Vectorize, Wordize to the build process	Robert Sloan	2016-06-22
\| \|
\| *	Make Assembly modules 8.5-compatible	Robert Sloan	2016-06-22
\| \|
\| *	Merge with public master	Robert Sloan	2016-06-22
\| \|\ \| \|/ \|/\|
* \|	EdDSA.Notations: indentation	Andres Erbsen	2016-06-22
\| \|
* \|	Fix broken notations (hopefully)	Jason Gross	2016-06-22
\| \|
* \|	Fix missing notations	Jason Gross	2016-06-22
\| \|
* \|	Aggregate all level specifications not in Spec/*	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \|	This prevents notation conflicts (see comment in Notations.v for more explanation).
* \|	Fix for broken abstract	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \|	It breaks when used in [Instance ... := _.]
\| *	Replace NPeano -> Nat in src/Spec/EdDSA	Robert Sloan	2016-06-22
\| \|
* \|	Update _CoqProject	Jason Gross	2016-06-22
\| \|
* \|	Add decidability util file	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \| \| \|	This will be useful for the Weierstrass curves, which require case-splitting on field equality.
* \|	Flip the sense of the conditional in the makefile	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \|	This way, we treat trunk as 8.5.
* \|	Make Coq 8.5 the default target for Fiat-Crypto	Jason Gross	2016-06-22
\| \| \| \| \| \| \| \|	Instructions for 8.4 build in the README
* \|	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
* \|	Add coq-scripts submodule for timing scripts	Jason Gross	2016-06-22
\| \|
* \|	Also build with Coq 8.5 on travis	Jason Gross	2016-06-22
\| \|