fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Add split_andb tactic	Jason Gross	2017-01-21
\|
*	Add reflect_iff_gen to Bool.v	Jason Gross	2016-11-05
\|
*	Add Bool lemmas about if statements	Jason Gross	2016-10-21
\|
*	Remove Bool.absorption_andb Bool.absorption_orb, not present in < 8.4pl5	Jason Gross	2016-08-03
\|
*	Add ZUtil lemmas, and Util.Bool	Jason Gross	2016-08-03
	After \| File Name \| Before \|\| Change ---------------------------------------------------------------------------------- 1m43.58s \| Total \| 1m44.69s \|\| -0m01.10s ---------------------------------------------------------------------------------- 0m32.94s \| Specific/GF25519 \| 0m33.18s \|\| -0m00.24s 0m15.34s \| ModularArithmetic/ModularBaseSystemProofs \| 0m15.35s \|\| -0m00.00s 0m11.42s \| Experiments/SpecEd25519 \| 0m11.46s \|\| -0m00.04s 0m07.12s \| Specific/GF1305 \| 0m07.38s \|\| -0m00.25s 0m04.04s \| ModularArithmetic/Pow2BaseProofs \| 0m04.09s \|\| -0m00.04s 0m03.82s \| ModularArithmetic/Tutorial \| 0m03.79s \|\| +0m00.02s 0m03.81s \| BaseSystemProofs \| 0m03.71s \|\| +0m00.10s 0m03.16s \| ModularArithmetic/ModularBaseSystemOpt \| 0m03.23s \|\| -0m00.06s 0m02.76s \| Util/ZUtil \| 0m02.79s \|\| -0m00.03s 0m01.63s \| ModularArithmetic/PrimeFieldTheorems \| 0m01.65s \|\| -0m00.02s 0m01.58s \| Encoding/PointEncodingPre \| 0m01.51s \|\| +0m00.07s 0m01.57s \| ModularArithmetic/ModularArithmeticTheorems \| 0m01.59s \|\| -0m00.02s 0m01.33s \| BaseSystem \| 0m01.50s \|\| -0m00.16s 0m01.09s \| ModularArithmetic/ExtendedBaseVector \| 0m01.13s \|\| -0m00.03s 0m00.95s \| Experiments/DerivationsOptionRectLetInEncoding \| 0m00.97s \|\| -0m00.02s 0m00.93s \| ModularArithmetic/BarrettReduction/Z \| 0m00.98s \|\| -0m00.04s 0m00.91s \| Util/NumTheoryUtil \| 0m01.19s \|\| -0m00.27s 0m00.91s \| ModularArithmetic/ModularBaseSystemField \| 0m00.91s \|\| +0m00.00s 0m00.81s \| ModularArithmetic/ModularBaseSystemListProofs \| 0m00.81s \|\| +0m00.00s 0m00.74s \| Experiments/SpecificCurve25519 \| 0m00.70s \|\| +0m00.04s 0m00.65s \| Encoding/ModularWordEncodingTheorems \| 0m00.72s \|\| -0m00.06s 0m00.65s \| Encoding/ModularWordEncodingPre \| 0m00.62s \|\| +0m00.03s 0m00.64s \| Testbit \| 0m00.66s \|\| -0m00.02s 0m00.63s \| ModularArithmetic/ExtPow2BaseMulProofs \| 0m00.63s \|\| +0m00.00s 0m00.63s \| Spec/ModularWordEncoding \| 0m00.63s \|\| +0m00.00s 0m00.60s \| ModularArithmetic/ModularBaseSystem \| 0m00.57s \|\| +0m00.03s 0m00.59s \| ModularArithmetic/ModularBaseSystemList \| 0m00.61s \|\| -0m00.02s 0m00.57s \| ModularArithmetic/PseudoMersenneBaseParamProofs \| 0m00.61s \|\| -0m00.04s 0m00.56s \| ModularArithmetic/Pre \| 0m00.48s \|\| +0m00.08s 0m00.41s \| ModularArithmetic/Pow2Base \| 0m00.42s \|\| -0m00.01s 0m00.38s \| ModularArithmetic/PseudoMersenneBaseParams \| 0m00.43s \|\| -0m00.04s 0m00.38s \| Spec/ModularArithmetic \| 0m00.39s \|\| -0m00.01s 0m00.04s \| Util/Bool \| N/A \|\| +0m00.04s