fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add things like app_7 to GF25519BoundedCommonWord.v	Jason Gross	2016-10-29
\|
*	Add interp_type_gen_rel_pointwise2, _gen =>	Jason Gross	2016-10-28
\|
*	Add {un,}curry_wire_digits	Jason Gross	2016-10-27
\|
*	Add {un,}curry_{bin,un}op_fe25519	Jason Gross	2016-10-27
\|
*	Add length_fe25519	Jason Gross	2016-10-27
\| \| \| \|	It'll be needed for generic reification and uncurrying
*	Factor out cmov{l,ne} and neg	Jason Gross	2016-10-27
\| \| \| \|	This way we will have a faster build of reification things
*	Simplify proof of proj1_fe25519_encode	Jason Gross	2016-10-27
\|
*	Add lemmas about GF25519BoundedCommon.{encode,decode}	Jason Gross	2016-10-27
\|
*	Switch to bounded Z	Jason Gross	2016-10-25
\| \| \| \| \|	We don't have working word code yet, because the reification code currently does spurious word->N->Z->N->word conversions everywhere. So we use Z instead.
*	Adjust bound on final word in wire_digits to 31	Jason Gross	2016-10-24
\|
*	Fix bounds on wire_digits	Jason Gross	2016-10-24
\| \| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/86#issuecomment-255839706
*	Add pack, unpack, ge_modulus to axioms to be reified	Jason Gross	2016-10-24
\|
*	Created separate definitions for cmovne and cmovl for reification	jadep	2016-10-23
\|
*	Finish twedprm_ERep proof	Jason Gross	2016-10-23
\| \| \| \|	(cc @andres-erbsen)
*	Make some things instances	Jason Gross	2016-10-23
\|
*	Generalize field_from_redundant_representation	Jason Gross	2016-10-23
\| \| \| \|	Note that the old version did not need phi', but the new version does
*	Add decode to GF25519BoundedCommon	Jason Gross	2016-10-22
\|
*	Make [vm_compute] on Bounded word reasonable	Jason Gross	2016-10-22
\| \| \| \|	We no longer store the type of proofs of [<=] in the term itself; this makes it amenable to vm_compute
*	Fix divergence in src/Specific/GF25519Bounded.v	Jason Gross	2016-10-22
\| \| \| \|	Not sure how I missed this...
*	Unfold interp stuff in Assembly/GF25519BoundedInstantiation	Jason Gross	2016-10-22
\|
*	Add bounded sqrt	Jason Gross	2016-10-22
\|
*	final touches/fixes for freeze restructuring	jadep	2016-10-22
\|
*	add arguments that I forgot	jadep	2016-10-22
\|
*	Modified [freeze] to be more reifyable	jadep	2016-10-22
\|
*	pow, not pow_opt, in Specific/GF25519	Jason Gross	2016-10-21
\|
*	Add word64eqb_Zeqb	Jason Gross	2016-10-21
\|
*	Sane fieldwiseb	Jason Gross	2016-10-21
\|
*	Make eqb sane (help from Jade)	Jason Gross	2016-10-21
\|
*	Remove axioms from src/Specific/GF25519Bounded.v, plug assembly	Jason Gross	2016-10-21
\|
*	A bit of initial setup on correct_and_bounded proofs in ↵	Jason Gross	2016-10-20
\| \| \| \|	GF25519BoundedInstantiation
*	Plug bounded into assembly stuff	Jason Gross	2016-10-20
\|
*	Remove code that should have been removed	Jason Gross	2016-10-20
\|
*	Split up GF25519Bounded to avoid circular dependencies	Jason Gross	2016-10-20
\|
*	Add todo	Jason Gross	2016-10-20
\|
*	Switch from bounded Z to bounded word	Jason Gross	2016-10-20
\|
*	More specific bounded requirements, implement inv	Jason Gross	2016-10-19
\|
*	First pass at bounded version of GF25519	Jason Gross	2016-10-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Boundedness is axiomatized as ```coq Axiom ExprBinOp : Type. Axiom ExprUnOp : Type. Axiom interp_bexpr : ExprBinOp -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519. Axiom interp_uexpr : ExprUnOp -> Specific.GF25519.fe25519 -> Specific.GF25519.fe25519. Axiom radd : ExprBinOp. Axiom rsub : ExprBinOp. Axiom rmul : ExprBinOp. Axiom ropp : ExprUnOp. Axiom rinv : ExprUnOp. Axiom radd_correct : forall x y, interp_bexpr radd x y = carry_add x y. Axiom rsub_correct : forall x y, interp_bexpr rsub x y = carry_sub x y. Axiom rmul_correct : forall x y, interp_bexpr rmul x y = mul x y. Axiom ropp_correct : forall x, interp_uexpr ropp x = carry_opp x. Axiom rinv_correct : forall x, interp_uexpr rinv x = inv x. Axiom check_bbounds : ExprBinOp -> bool. Axiom check_ubounds : ExprUnOp -> bool. Axiom radd_bounded : check_bbounds radd = true. Axiom rsub_bounded : check_bbounds rsub = true. Axiom rmul_bounded : check_bbounds rmul = true. Axiom ropp_bounded : check_ubounds ropp = true. Axiom rinv_bounded : check_ubounds rinv = true. Axiom bbounds_correct : forall rexpr, check_bbounds rexpr = true -> forall x y, is_bounded x = true -> is_bounded y = true -> is_bounded (interp_bexpr rexpr x y) = true. Axiom ubounds_correct : forall rexpr, check_ubounds rexpr = true -> forall x, is_bounded x = true -> is_bounded (interp_uexpr rexpr x) = true. ``` Questions: - Some of this is very general and probably doesn't belong in this file (e.g., [correct_le_le]). Should it stay, or move elsewhere? - There's a lot of type munging that could be generalized to arbitrary heterogenous lists; should it be generalized? - How do we do [div] on bounded things? Currently, I have ```coq Axiom div : forall (f g : fe25519), fe25519. Axiom div_correct : forall a b : fe25519, ModularBaseSystem.eq (proj1_fe25519 (div a b)) (ModularBaseSystem.div (proj1_fe25519 a) (proj1_fe25519 b)). ```
*	Removed the lingering TODO and print statement that @JasonGross helpfully ↵	jadep	2016-10-19
\| \| \| \|	pointed out
*	Fill in admits for field with carry_add, carry_opp, and carry_sub	jadep	2016-10-19
\|
*	Define carry_opp in terms of carry_sub	Jason Gross	2016-10-19
\|
*	Add opt versions of add, sub, opp	Jason Gross	2016-10-19
\|
*	Fix out of memory error for 8.5,8.5pl1	Jason Gross	2016-10-19
\|
*	Fix for Coq 8.4 evar propogation	Jason Gross	2016-10-18
\|
*	Fix missing imports	Jason Gross	2016-10-17
\|
*	Remove broken imports	Jason Gross	2016-10-17
\|
*	Rename and clean up exponent code	Jason Gross	2016-10-17
\|
*	Remove admits with the help of Andres	Jason Gross	2016-10-17
\|
*	Fill in more proofs	Jason Gross	2016-10-17
\|
*	Initial work on exponent field as Z	Jason Gross	2016-10-17
\|
*	Clean up ge_modulus definition in Specific	jadep	2016-10-12
\|