fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Fix a typo in the previous commit	Jason Gross	2016-10-14
\|
*	Fix exponential blowup in some doubling ops	Jason Gross	2016-10-14
\| \| \| \|	Thanks @andres-erbsen !
*	Work around bug 5401 (bad let '(x, y))	Jason Gross	2016-10-13
\| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5140, destructuring let under binders of a class with an argument gives "Anomaly: index to an anonymous variable. Please report at http://coq.inria.fr/bugs/."
*	Work around bug 5003 (broken omega on projections)	Jason Gross	2016-10-10
\| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5003, [xlia] ([lia], [nia]) constructs ill typed terms when projections from records are involved.
*	Add repeated multiple	Jason Gross	2016-10-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------------------------- 0m04.24s \| Total \| 0m04.12s \|\| +0m00.12s --------------------------------------------------------------------------------------------------------- 0m01.01s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.03s \|\| -0m00.02s 0m00.58s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.56s \|\| +0m00.01s 0m00.56s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.54s \|\| +0m00.02s 0m00.56s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.50s \|\| +0m00.06s 0m00.55s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.56s \|\| -0m00.01s 0m00.50s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| 0m00.46s \|\| +0m00.03s 0m00.48s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| 0m00.47s \|\| +0m00.01s
*	Add shl,shr,shrd to repeated doubling	Jason Gross	2016-10-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------------------------- 0m03.99s \| Total \| 0m03.08s \|\| +0m00.90s --------------------------------------------------------------------------------------------------------- 0m01.14s \| BoundedArithmetic/Double/Repeated/Proofs/Decode \| 0m01.02s \|\| +0m00.11s 0m00.52s \| BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr \| 0m00.53s \|\| -0m00.01s 0m00.51s \| BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub \| 0m00.51s \|\| +0m00.00s 0m00.47s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate \| N/A \|\| +0m00.47s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate \| 0m00.54s \|\| -0m00.08s 0m00.46s \| BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight \| N/A \|\| +0m00.46s 0m00.44s \| BoundedArithmetic/Double/Repeated/Proofs/SelectConditional \| 0m00.49s \|\| -0m00.04s
*	Add proofs for doubling shl,shr,shrd	Jason Gross	2016-10-09
\| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change ------------------------------------------------------------------------------------------------ 0m14.81s \| Total \| 0m00.00s \|\| +0m14.81s ------------------------------------------------------------------------------------------------ 0m08.87s \| BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate \| N/A \|\| +0m08.86s 0m02.82s \| BoundedArithmetic/Double/Proofs/ShiftLeft \| N/A \|\| +0m02.81s 0m02.72s \| BoundedArithmetic/Double/Proofs/ShiftRight \| N/A \|\| +0m02.72s 0m00.40s \| BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic \| N/A \|\| +0m00.40s
*	Some work on x86 and bounded repeated things	Jason Gross	2016-10-09
\|
*	Add some bounded decode/and things	Jason Gross	2016-10-09
\|
*	Split up DoubleBoundedProofs, add proofs	Jason Gross	2016-10-07
	Some help from jadep on BitwiseOr. After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------------- 0m39.26s \| Total \| 0m36.03s \|\| +0m03.23s -------------------------------------------------------------------------------------- N/A \| BoundedArithmetic/DoubleBoundedProofs \| 0m21.20s \|\| -0m21.19s 0m07.47s \| BoundedArithmetic/Double/Proofs/Multiply \| N/A \|\| +0m07.46s 0m06.70s \| BoundedArithmetic/Double/Proofs/SpreadLeftImmediate \| N/A \|\| +0m06.70s 0m05.14s \| BoundedArithmetic/Double/Proofs/RippleCarryAddSub \| N/A \|\| +0m05.13s 0m02.75s \| BoundedArithmetic/Double/Proofs/Decode \| N/A \|\| +0m02.75s 0m08.06s \| BoundedArithmetic/ArchitectureToZLikeProofs \| 0m08.05s \|\| +0m00.00s 0m02.01s \| Specific/FancyMachine256/Barrett \| 0m02.13s \|\| -0m00.12s 0m02.00s \| Specific/FancyMachine256/Montgomery \| 0m02.06s \|\| -0m00.06s 0m01.75s \| Specific/FancyMachine256/Core \| 0m01.66s \|\| +0m00.09s 0m00.90s \| BoundedArithmetic/Double/Proofs/LoadImmediate \| N/A \|\| +0m00.90s 0m00.88s \| BoundedArithmetic/Double/Proofs/BitwiseOr \| N/A \|\| +0m00.88s 0m00.58s \| BoundedArithmetic/Double/Proofs/SelectConditional \| N/A \|\| +0m00.57s 0m00.53s \| BoundedArithmetic/ArchitectureToZLike \| 0m00.47s \|\| +0m00.06s 0m00.49s \| BoundedArithmetic/Double/Core \| N/A \|\| +0m00.49s N/A \| BoundedArithmetic/DoubleBounded \| 0m00.46s \|\| -0m00.46s