fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Also display the carry chain in a comment	Jason Gross	2019-01-26
\|
*	Give slightly more standard usage strings	Jason Gross	2019-01-23
\|
*	Mention the separator (spaces) of the list arg	Jason Gross	2019-01-23
\|
*	Split up PushButtonSynthesis.v	Jason Gross	2019-01-18
\| \| \| \|	Closes #497
*	Be stricter about rejecting command line arguments	Jason Gross	2019-01-18
\| \| \| \| \| \| \| \| \| \| \| \| \|	We no longer accept `1,1` as a valid bitwidth. This closes #488. It does not quite fix the issue as stated, but it resolves the underlying confusion that generated it (the difference between passing `1,1` as a `c` vs passing `1,1` as a bitwidth). It still might be nice to someday emit warnings as suggested in the bug report. I've also factored out a bit of code to make it easier to report parse failures, by folding over a list of parses.
*	Autocompute s and c in WBW Montgomery	Jason Gross	2019-01-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes #486 Closes #342 After \| File Name \| Before \|\| Change \| % Change -------------------------------------------------------------------------------------------- 22m14.42s \| Total \| 12m14.76s \|\| +9m59.65s \| +81.61% -------------------------------------------------------------------------------------------- 9m41.91s \| p484_32.c \| N/A \|\| +9m41.90s \| ∞ 0m11.51s \| p484_64.c \| N/A \|\| +0m11.50s \| ∞ 3m16.22s \| p384_32.c \| 3m12.02s \|\| +0m04.19s \| +2.18% 4m12.18s \| PushButtonSynthesis.vo \| 4m10.16s \|\| +0m02.02s \| +0.80% 0m45.08s \| ExtractionHaskell/word_by_word_montgomery \| 0m45.24s \|\| -0m00.16s \| -0.35% 0m38.14s \| p521_32.c \| 0m38.12s \|\| +0m00.02s \| +0.05% 0m31.80s \| p521_64.c \| 0m31.78s \|\| +0m00.01s \| +0.06% 0m31.09s \| ExtractionHaskell/unsaturated_solinas \| 0m30.77s \|\| +0m00.32s \| +1.03% 0m24.18s \| ExtractionHaskell/saturated_solinas \| 0m24.21s \|\| -0m00.03s \| -0.12% 0m17.38s \| ExtractionOCaml/word_by_word_montgomery \| 0m17.35s \|\| +0m00.02s \| +0.17% 0m13.39s \| secp256k1_32.c \| 0m13.59s \|\| -0m00.19s \| -1.47% 0m13.14s \| p256_32.c \| 0m13.04s \|\| +0m00.10s \| +0.76% 0m10.58s \| ExtractionOCaml/unsaturated_solinas \| 0m10.73s \|\| -0m00.15s \| -1.39% 0m10.23s \| ExtractionOCaml/word_by_word_montgomery.ml \| 0m10.34s \|\| -0m00.10s \| -1.06% 0m07.88s \| ExtractionOCaml/saturated_solinas \| 0m07.94s \|\| -0m00.06s \| -0.75% 0m06.78s \| ExtractionOCaml/unsaturated_solinas.ml \| 0m06.86s \|\| -0m00.08s \| -1.16% 0m06.28s \| ExtractionHaskell/word_by_word_montgomery.hs \| 0m06.42s \|\| -0m00.13s \| -2.18% 0m06.00s \| p224_32.c \| 0m05.97s \|\| +0m00.03s \| +0.50% 0m05.50s \| p384_64.c \| 0m05.35s \|\| +0m00.15s \| +2.80% 0m05.28s \| ExtractionOCaml/saturated_solinas.ml \| 0m05.08s \|\| +0m00.20s \| +3.93% 0m05.10s \| ExtractionHaskell/unsaturated_solinas.hs \| 0m04.98s \|\| +0m00.11s \| +2.40% 0m04.12s \| ExtractionHaskell/saturated_solinas.hs \| 0m04.15s \|\| -0m00.03s \| -0.72% 0m02.14s \| curve25519_32.c \| 0m02.28s \|\| -0m00.13s \| -6.14% 0m01.44s \| CLI.vo \| 0m01.42s \|\| +0m00.02s \| +1.40% 0m01.44s \| curve25519_64.c \| 0m01.57s \|\| -0m00.13s \| -8.28% 0m01.14s \| StandaloneOCamlMain.vo \| 0m01.11s \|\| +0m00.02s \| +2.70% 0m01.12s \| p256_64.c \| 0m00.98s \|\| +0m00.14s \| +14.28% 0m01.11s \| StandaloneHaskellMain.vo \| 0m01.17s \|\| -0m00.05s \| -5.12% 0m01.03s \| secp256k1_64.c \| 0m01.15s \|\| -0m00.11s \| -10.43% 0m01.02s \| p224_64.c \| 0m00.99s \|\| +0m00.03s \| +3.03% 0m00.21s \| Util/Strings/ParseArithmetic.vo \| N/A \|\| +0m00.21s \| ∞
*	move src/Experiments/NewPipeline/ to src/	Andres Erbsen	2019-01-09