fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add UnfoldArg	Jason Gross	2017-07-08
\|
*	automate P256 integration	Andres Erbsen	2017-07-02
\|
*	Reorganization of saturated arithmetic	jadep	2017-06-29
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	Weierstrass Jacobian mixed addition	Andres Erbsen	2017-06-23
\|
*	Add (partially admitted) integration tests for add, sub, opp	Jason Gross	2017-06-22
\|
*	move Specifi p256 files into their own directory	Andres Erbsen	2017-06-22
\|
*	src/Demo.v: a 200-line introduction to BaseSystem ideas	Andres Erbsen	2017-06-21
\|
*	Add fold_left_orb_true, fold_left_orb_pull	Jason Gross	2017-06-20
\|
*	Add ModInv	Jason Gross	2017-06-18
\| \| \| \|	This closes #209.
*	compile X25519 C code from Makefile	Andres Erbsen	2017-06-18
\|
*	add 128-bit display file	Jason Gross	2017-06-17
\|
*	Add 128-bit version of montgomery for testing	Jason Gross	2017-06-17
\|
*	Finish MontgomeryP256 (less conditional subtract)	Jason Gross	2017-06-17
\|
*	Add initial IntegrationTestMontgomeryP256.v	Jason Gross	2017-06-17
\|
*	Fix spelling	Jason Gross	2017-06-17
\|
*	Switch to using tuples for word-by-word montgomery	Jason Gross	2017-06-16
\| \| \| \| \| \| \|	The new parameterized definitions and proofs are in WordByWord/Abstract/Dependent/; the old ones are untouched (and unused) in WordByWord/Abstract/. I replaced definitions I didn't know how to write in the Saturated API with the use of an axiom.
*	Fix build	Jason Gross	2017-06-16
\|
*	Revert PR #203	Jason Gross	2017-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964 and https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747 Revert "update ocq2C sed script" This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e. Revert "make display" This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e. Revert "Make use of CArrayNotations" This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb. Revert "Fix CArrayNotations" This reverts commit d0d0fbd4499296a2164e209466227892671556f0. Revert "Revert "Revert "Add CArrayNotations""" This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c.
*	Revert "Revert "Add CArrayNotations""	Jason Gross	2017-06-16
\| \| \| \|	This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
*	Revert "Add CArrayNotations"	Jason Gross	2017-06-15
\| \| \| \| \| \| \|	This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339. It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469), which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out).
*	Finish karatsuba mul, add display file (#199)	Jason Gross	2017-06-15
\| \| \|	This closes #182.
*	Add CArrayNotations	Jason Gross	2017-06-15
\|
*	Add -compat 8.6 to _CoqProject	Jason Gross	2017-06-15
\| \| \| \| \| \|	This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet).
*	Add ZUtil.Z2Nat	Jason Gross	2017-06-15
\|
*	Edwards coordinates precomputed addition formula	Andres Erbsen	2017-06-15
\|
*	move CPS notations to Util.CPSNotations	Andres Erbsen	2017-06-15
\|
*	ScalarMult: Z -> G -> G (closes #193)	Andres Erbsen	2017-06-14
\|
*	Stronger invert_op tactic	Jason Gross	2017-06-13
\| \| \| \|	Now it can handle ops that return (Tbase TZ)
*	Add Z.peano_rect	Jason Gross	2017-06-13
\|
*	Add Z.mul_split	Jason Gross	2017-06-13
\|
*	WBW-montgomery: Fill in most context variables	Jason Gross	2017-06-13
\|
*	Add CompileInterpSideConditions.v	Jason Gross	2017-06-12
\|
*	Add snd_interpf_side_conditions_gen_Some	Jason Gross	2017-06-12
\|
*	Add Named.InterpSideConditions	Jason Gross	2017-06-12
\|
*	Add Z.InterpSideConditions	Jason Gross	2017-06-12
\|
*	Add InterpSideConditions	Jason Gross	2017-06-12
\|
*	Factor karatsuba through IdfunWithAlt, add test	Jason Gross	2017-06-11
\| \| \| \| \| \| \| \| \| \| \|	Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom.
*	Add IdfunWithAlt	Jason Gross	2017-06-11
\|
*	Add clearbody_all	Jason Gross	2017-06-11
\|
*	Remove temporary file	Jason Gross	2017-06-10
\| \| \| \|	It's been migrated to Definitions.v and Proofs.v in the same directory
*	Add initial proofs for word-by-word	Jason Gross	2017-06-10
\|
*	Make it clear that the combined definition/proof file is a work in progress	Jason Gross	2017-06-09
\|
*	Add pair-programmed wbw montgomery	Jason Gross	2017-06-09
\| \| \| \|	Partial progress with @andres-erbsen
*	add Specific/Karatsuba to CoqProject	jadep	2017-06-07
\|
*	Add experimental loops	Jason Gross	2017-06-02
\| \| \| \|	Written via pair-programming with Andres.
*	Add compiler optimization for add-with-carry	Jason Gross	2017-05-17
\| \| \| \| \| \| \| \| \| \| \|	This closes #171. It's unfortunately a bit fragile, and takes a really long time (about 60s) to prove correct, because Coq is bad at deep dependent pattern matching. We enable a-normal form for the freeze test, because the rewriter only works when the arguments to adc are var or const.
*	Add reflective machinery for adc, zselect	Jason Gross	2017-05-17
\|
*	Add context_equiv and prove some Proper lemmas	Jason Gross	2017-05-16
\|
*	Add Named.ExprInversion	Jason Gross	2017-05-15
\|