fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix for 8.4 compatibility	Jason Gross	2016-09-05
\|
*	Remove ReifyDirect	Jason Gross	2016-09-05
\| \| \| \|	It's probably not going to be used
*	A helper lemma for [Wf]	Jason Gross	2016-09-05
\| \| \| \| \| \| \| \| \|	This method allows a proof term that's linear in the term being proven well-founded, rather than exponential in it. By factoring out all of the reasoning about expressions, we can incur overhead equal to (the number of constants) + (the number of let-bindings) + (the number of variables used), all without mentioning the term itself; [vm_compute] can do the appropriate reduction for us.
*	PHOAS syntax	Jason Gross	2016-09-05
\| \| \| \| \| \| \|	We also have linearization of function application / lets, constant-inlining, and reification. This closes #58.
*	Add nth_error_In from 8.6	Jason Gross	2016-09-05
\|
*	Add connectives about option pointed_Prop	Jason Gross	2016-09-05
\|
*	Add a coercion [bool >-> option pointed_Prop]	Jason Gross	2016-09-05
\|
*	Fix a typo	Jason Gross	2016-09-05
\|
*	Add a file about pointed Props	Jason Gross	2016-09-05
\|
*	Add a lemma about semidecidable things to Decidable	Jason Gross	2016-09-05
\|
*	Make [inversion_{prod,sigma}] stronger	Jason Gross	2016-09-05
\| \| \| \|	It can now handle paths used in dependent places.
*	Transparent version of f_equal2	Jason Gross	2016-09-05
\|
*	Reserve [->] like in 8.5, so we can redefine it in 8.4	Jason Gross	2016-09-05
\|
*	Add path_prod_eta	Jason Gross	2016-09-03
\|
*	Make [inversion_option] work on Prop options	Jason Gross	2016-09-03
\|
*	Reserve λ notation	Jason Gross	2016-09-02
\|
*	Add reserved syntax-let notation	Jason Gross	2016-09-02
\|
*	Don't zeta-reduce in [simplify_projections]	Jason Gross	2016-09-02
\|
*	Add prod_beq	Jason Gross	2016-09-02
\|
*	Strip <infomsg>; it messes things up in Coq 8.6 display	Jason Gross	2016-09-02
\|
*	Slightly better cfail	Jason Gross	2016-09-02
\|
*	Fix [ring] reference broken by moving [Require] outside a module	Jason Gross	2016-09-02
\|
*	Silence a warning about [Require] in 8.6	Jason Gross	2016-09-02
\|
*	Add cfail{2,3}	Jason Gross	2016-09-02
\|
*	Add [idtac_goal]	Jason Gross	2016-09-02
\|
*	Add constr-based idtac tactics	Jason Gross	2016-09-02
\|
*	Add another reserved notation	Jason Gross	2016-09-01
\|
*	Add more reserved infixes	Jason Gross	2016-08-31
\|
*	Add correctness theorems to Montgomery.ZBounded	Jason Gross	2016-08-31
\|
*	Rename congrunce_option to inversion_option, add [inversion_prod]	Jason Gross	2016-08-31
\|
*	Add congruence_option tactic	Jason Gross	2016-08-31
\|
*	updated GF25519 to match new exponentiation chain code	jadep	2016-08-31
\|
*	Added square roots to GF1305, started reworking freeze_opt in preparation ↵	jadep	2016-08-31
\| \| \| \|	for instantiating it in GF25519 (needed for equality comparison in sqrt_5mod8)
*	Generalized exponentiation chains so inverse and square roots can use the ↵	jadep	2016-08-31
\| \| \| \|	same typeclass.
*	Removed some commented-out code that will probably not be needed.	jadep	2016-08-31
\|
*	Compatibility for 8.5; clear assumptions for an admitted canonicalization proof.	jadep	2016-08-31
\|
*	Removed lingering SearchAbout.	jadep	2016-08-31
\|
*	Proofs for MBS square roots.	jadep	2016-08-31
\|
*	fixed typo; extra argument	jadep	2016-08-31
\|
*	Parameterized square roots for primes that are 5 mod 8 over any computation ↵	jadep	2016-08-31
\| \| \| \|	of sqrt (-1)
*	Reworked square root theorems to prove they are valid iff a square root ↵	jadep	2016-08-31
\| \| \| \|	exists, not just if one exists.
*	Add runtime equality comparison and square root functions to ModularBaseSystem.	jadep	2016-08-31
\|
*	fix duplicate name in PrimeFieldTheorems	jadep	2016-08-31
\|
*	square roots modulo p for [p mod 4 = 3]; we now have modular sqrt for all ↵	jadep	2016-08-31
\| \| \| \|	primes except 2 and primes that are 1 mod 8.
*	Defined an equality comparison for tuples that uses bool instead of Prop ↵	jadep	2016-08-31
\| \| \| \|	(like Z.eqb). This is necessary for the runtime equality comparison on tuples that will appear in square root calculations during point-decoding.
*	Add reduce via partial to Montgomery ZBounded	Jason Gross	2016-08-29
\|
*	Merge pull request #52 from JasonGross/bounded-interface	Jason Gross	2016-08-25
\|\ \| \| \| \|	Initial work on an architecture interface for ℤ/nℤ
\| *	Integrate suggestions from Andres	Jason Gross	2016-08-25
\| \|
* \|	Changed definition of [sub] to require proof that the modulus multiple ↵	jadep	2016-08-25
\| \| \| \| \| \| \| \|	actually is a multiple of the modulus. This allows for proving the Proper properties of [sub] based on its correctness proof alone, which has the modulus multiple correctness as a precondition.
* \|	Proper proofs for all ModularBaseSystem operations except [sub]	jadep	2016-08-24
\| \|