fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Finish proofs about eliminating useless carries	Jason Gross	2016-11-17
\|
*	Add another admitted lemma	Jason Gross	2016-11-17
\|
*	Add GF25519BoundedExtendedAddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	The lemma is currently admitted
*	Add src/Specific/GF25519BoundedAddCoordinates.v	Jason Gross	2016-11-17
\|
*	Add ReflectiveAddCoordinates	Jason Gross	2016-11-17
\|
*	Fix some problems with previous commit	Jason Gross	2016-11-17
\|
*	Remove admits, fill templates, copy bounds	Jason Gross	2016-11-17
\|
*	Update AddCoordinates	Jason Gross	2016-11-17
\| \| \| \|	Now the _correct_and_bounded lemma goes through
*	Minor change in AddCoordinates	Jason Gross	2016-11-17
\|
*	Move util definitions to util folder	Jason Gross	2016-11-17
\|
*	Add reified mostly-bounds-checked add_coordinates	Jason Gross	2016-11-17
\|
*	Move ExtendedAddCoordinates to new file, SpecGen	Jason Gross	2016-11-17
\|
*	Add fieldwise_eq_edwards_extended_add_coordinates_carry_nocarry	Jason Gross	2016-11-17
\|
*	Work around bug #5205 (arguments naming weirdness)	Jason Gross	2016-11-16
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5205, Bogus "Error: Wrong argument name: n." error message in 8.4, 8.5
*	Split fixedpoint in interpf	Jason Gross	2016-11-16
\|
*	Add more things to Reflective/Common	Jason Gross	2016-11-16
\| \| \| \|	Preparation for reflective add_coordinates
*	Fix for Coq 8.5 (more unfolding)	Jason Gross	2016-11-15
\|
*	Handle both kinds of sqrt	Jason Gross	2016-11-14
\|
*	More generic sqrt	Jason Gross	2016-11-14
\|
*	Fix postfreezeW_correct_and_bounded	Jason Gross	2016-11-14
\|
*	Speed up some GF25519 tactics	Jason Gross	2016-11-14
\|
*	Support for 128-bit words	Jason Gross	2016-11-14
\| \| \| \| \|	I haven't found a good way to genericize the proofs of relatedness things, mostly because Modules and functors are annoying.
*	Fix some sqrt things	Jason Gross	2016-11-14
\|
*	Fix a missing unfold	Jason Gross	2016-11-14
\|
*	Update bounds things with prefreeze	Jason Gross	2016-11-14
\|
*	Add mulW_noinline	Jason Gross	2016-11-14
\|
*	Work around bug #5198 (broken tc resolution)	Jason Gross	2016-11-12
\| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5198, Inlining lets breaks typechecking of [Definition]s
*	More 8.4pl2 fixes	Jason Gross	2016-11-12
\| \| \| \|	Also, I meant 8.4pl2 in the previous commit, not 8.2
*	Fix for Coq 8.2	Jason Gross	2016-11-12
\|
*	Fixes for 8.4 (instantiate)	Jason Gross	2016-11-12
\|
*	GF25519: add ErepAdd	Andres Erbsen	2016-11-11
\|
*	GF25519: add optimized addition chain	Andres Erbsen	2016-11-11
\|
*	Proved postfreezeW_correct_and_bounded	jadep	2016-11-11
\|
*	Remove dead code in rebuild-reified.py	Jason Gross	2016-11-11
\|
*	Begin filling in @JasonGross's stubs	jadep	2016-11-11
\|
*	separate freeze into two parts	jadep	2016-11-11
\|
*	8.4-compatible universe handling	Jason Gross	2016-11-11
\|
*	Remove 8.6 only syntax	Jason Gross	2016-11-11
\|
*	Freeze stubs	Jason Gross	2016-11-11
\|
*	Fix bug in 8.4 build	Jason Gross	2016-11-09
\|
*	Split up GF25519Reflective.Common: faster+parallel	Jason Gross	2016-11-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------- 2m53.12s \| Total \| 2m52.26s \|\| +0m00.85s -------------------------------------------------------------------------------- 0m01.38s \| Specific/GF25519Reflective/Common \| 0m43.51s \|\| -0m42.12s 0m14.82s \| Specific/GF25519Reflective/CommonBinOp \| N/A \|\| +0m14.82s 0m10.91s \| Specific/GF25519Reflective/CommonUnOp \| N/A \|\| +0m10.91s 0m10.44s \| Specific/GF25519Reflective/CommonUnOpWireToFE \| N/A \|\| +0m10.43s 0m06.42s \| Specific/GF25519Reflective/CommonUnOpFEToWire \| N/A \|\| +0m06.41s 1m18.24s \| Experiments/Ed25519 \| 1m18.57s \|\| -0m00.32s 0m07.97s \| Specific/GF25519Reflective/Reified/Mul \| 0m08.45s \|\| -0m00.47s 0m07.89s \| Specific/GF25519Reflective/Reified/Freeze \| 0m07.84s \|\| +0m00.04s 0m06.87s \| Specific/GF25519Reflective \| 0m06.92s \|\| -0m00.04s 0m03.53s \| Specific/GF25519Reflective/Reified/CarrySub \| 0m03.63s \|\| -0m00.10s 0m03.27s \| Specific/GF25519Reflective/Reified/CarryAdd \| 0m03.28s \|\| -0m00.00s 0m03.18s \| Specific/GF25519Reflective/Reified/CarryOpp \| 0m03.15s \|\| +0m00.03s 0m02.24s \| Specific/GF25519Reflective/Reified/Unpack \| 0m02.21s \|\| +0m00.03s 0m02.19s \| Specific/GF25519Reflective/Reified/Pack \| 0m02.28s \|\| -0m00.08s 0m02.16s \| Specific/GF25519Reflective/Reified/Sub \| 0m02.15s \|\| +0m00.01s 0m02.14s \| Specific/GF25519Bounded \| 0m02.07s \|\| +0m00.07s 0m02.07s \| Experiments/Ed25519Extraction \| 0m02.16s \|\| -0m00.09s 0m01.99s \| Specific/GF25519Reflective/Reified/Add \| 0m01.81s \|\| +0m00.17s 0m01.82s \| Specific/GF25519Reflective/Reified/Opp \| 0m01.78s \|\| +0m00.04s 0m01.76s \| Specific/GF25519Reflective/Reified/GeModulus \| 0m01.71s \|\| +0m00.05s 0m00.97s \| Specific/GF25519Reflective/CommonUnOpFEToZ \| N/A \|\| +0m00.97s 0m00.86s \| Specific/GF25519Reflective/Reified \| 0m00.75s \|\| +0m00.10s
*	move B_order_l and prime_q	Andres Erbsen	2016-11-06
\|
*	Refactor various reflective things	Jason Gross	2016-11-06
\| \| \| \| \|	We now have a more principled approach in many places, and some of the tuple-specific reasoning has been filled in.
*	Connect [is_bounded] to [bounded_by]	Jason Gross	2016-11-06
\| \| \| \| \|	This hooks up the boundedness constraints on [freeze] in GF25519Bounded to those in Ed25519.
*	The fix in 8.4 broke 8.5/8.6, so we fix that	Jason Gross	2016-11-06
\| \| \| \|	Grrrr, evars
*	Add syntactic tuples	Jason Gross	2016-11-06
\|
*	Add support for dependent reification	Jason Gross	2016-11-06
\|
*	Work around broken evars in 8.4	Jason Gross	2016-11-06
\|
*	Plug in boundedness proofs	Jason Gross	2016-11-05
\| \| \| \| \|	We no longer admit the boundedness proofs (other than freeze); a significant chunk of the boundedness proofs now line up nicely.
*	Add better bounded lemmas to reified things	Jason Gross	2016-11-05
\|