fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Update .travis.yml to be 8.7-only	Jason Gross	2017-10-18
\|
*	projective Weierstrass: (P2 = 2Q -> P = Q) -> not exceptional	Andres Erbsen	2017-10-18
\| \| \| \|	(Squashed and rebased by Jason Gross)
*	Revert "Add -compat 8.6 to _CoqProject"	Jason Gross	2017-10-18
\| \| \| \|	This reverts commit 131f341f368b606fd50b57f135e602e40e132b46.
*	Add a Require Import FunInd (Function isn't loaded by default anymore)	Pierre Letouzey	2017-10-18
\| \| \| \|	See PR #220 https://github.com/coq/coq/pull/220
*	Add some more things to basesystem_partial_evaluation_unfolder	Jason Gross	2017-10-18
\|
*	Add basesystem_partial_evaluation_unfolder db	Jason Gross	2017-10-18
\|
*	Unfold more things in core unfolder	Jason Gross	2017-10-18
\|
*	Allow instantiating type arguments without reducing matches	Jason Gross	2017-10-18
\|
*	Allow instantiating type arguments without reducing matches	Jason Gross	2017-10-17
\|
*	Allow instantiating type arguments without reducing matches	Jason Gross	2017-10-17
\|
*	Pattern more things in arithmetic/core	Jason Gross	2017-10-17
\|
*	Allow instantiation of cps type arguments by unfolding	Jason Gross	2017-10-17
\|
*	Make use of faster interp rewriting	Jason Gross	2017-10-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------- 10m34.32s \| Total \| 11m10.14s \|\| -0m35.81s --------------------------------------------------------------------------------------- 0m04.75s \| Compilers/Z/Bounds/Pipeline/Definition \| 0m41.89s \|\| -0m37.14s 1m24.64s \| Specific/IntegrationTestKaratsubaMul \| 1m20.20s \|\| +0m04.43s 1m59.10s \| Specific/X25519/C64/ladderstep \| 2m00.27s \|\| -0m01.17s 1m14.55s \| Specific/IntegrationTestLadderstep130 \| 1m13.12s \|\| +0m01.42s 0m49.89s \| Specific/X25519/C32/femul \| 0m51.34s \|\| -0m01.45s 0m26.72s \| Specific/X25519/C32/fesquare \| 0m27.79s \|\| -0m01.07s 1m51.04s \| Specific/NISTP256/AMD64/femul \| 1m50.92s \|\| +0m00.11s 0m25.48s \| Specific/IntegrationTestMontgomeryP256_128 \| 0m24.72s \|\| +0m00.76s 0m18.54s \| Specific/NISTP256/AMD64/fesub \| 0m18.60s \|\| -0m00.06s 0m15.57s \| Specific/NISTP256/AMD64/feadd \| 0m15.78s \|\| -0m00.20s 0m14.93s \| Specific/NISTP256/AMD64/feopp \| 0m15.09s \|\| -0m00.16s 0m12.13s \| Specific/IntegrationTestMontgomeryP256_128_Sub \| 0m12.34s \|\| -0m00.20s 0m11.78s \| Specific/IntegrationTestMontgomeryP256_128_Add \| 0m12.35s \|\| -0m00.57s 0m11.06s \| Specific/IntegrationTestMontgomeryP256_128_Opp \| 0m11.24s \|\| -0m00.17s 0m10.16s \| Specific/X25519/C64/femul \| 0m10.18s \|\| -0m00.01s 0m09.78s \| Specific/NISTP256/AMD64/fenz \| 0m10.10s \|\| -0m00.32s 0m09.06s \| Specific/IntegrationTestMontgomeryP256_128_Nonzero \| 0m09.26s \|\| -0m00.19s 0m08.63s \| Specific/IntegrationTestSub \| 0m08.32s \|\| +0m00.31s 0m07.84s \| Specific/IntegrationTestFreeze \| 0m07.87s \|\| -0m00.03s 0m07.27s \| Specific/X25519/C64/fesquare \| 0m07.25s \|\| +0m00.01s 0m00.80s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics \| 0m00.81s \|\| -0m00.01s 0m00.61s \| Compilers/Z/Bounds/Pipeline \| 0m00.70s \|\| -0m00.08s
*	Add InterpRewriting	Jason Gross	2017-10-17
\| \| \| \| \|	This is a faster version of [autorewrite with reflective_interp] on large chains of expressions.
*	Add CacheTerm	Jason Gross	2017-10-17
\| \| \| \| \|	The real use of this is with the 8.7-only transparent_abstract, but we can do some things even when we can only cache proofs.
*	Turn on parenthetization in C output	Jason Gross	2017-10-17
\|
*	Unify notation printing to allow changing it all at once	Jason Gross	2017-10-17
\|
*	Allow unfolding of mapi_with_cps to specialize the function to the type ↵	Jason Gross	2017-10-17
\| \| \| \|	argument it gets passed
*	Work around bug #5341	Jason Gross	2017-10-17
\|
*	Fix some type annotations for better non-unfolding	Jason Gross	2017-10-17
\|
*	Add MulSplitUnfolder	Jason Gross	2017-10-17
\|
*	Remove outdated json file, reorder remake_curves.sh	Jason Gross	2017-10-17
\|
*	Add more json files	Jason Gross	2017-10-16
\|
*	Add support for parenthesizing all CNotations expressions	Jason Gross	2017-10-16
\|
*	Don't print ".0" for integer bases in the json files	Jason Gross	2017-10-16
\|
*	bugfixes from messy rebase; remade json files	jadep	2017-10-16
\|
*	change limit for max # limbs to allow, add commented-out pretty-printing	jadep	2017-10-16
\|
*	express montgomery-friendly moduli in a more script-friendly way, since we ↵	jadep	2017-10-16
\| \| \| \|	don't have extra support for them anyway
*	Add more constants	Jason Gross	2017-10-16
\|
*	Add some more power-of-two notations	Jason Gross	2017-10-16
\|
*	Add more notations	Jason Gross	2017-10-16
\|
*	Fix base generation	Jason Gross	2017-10-16
\|
*	Add more json files	Jason Gross	2017-10-16
\|
*	Don't error if we can't open a file	Jason Gross	2017-10-16
\|
*	Handle more primes	Jason Gross	2017-10-16
\|
*	Regenerate json files	Jason Gross	2017-10-16
\|
*	Fix various issues with generate_parameters.py	Jason Gross	2017-10-16
\| \| \| \| \| \| \|	Some of the sizes were too small because python3 generates floats on division, while python2 rounds down. Also add better error handling
*	generate_parameters.py: Don't overwrite files with identical contents	Jason Gross	2017-10-16
\|
*	Add faster arithmetic unfolding	Jason Gross	2017-10-15
\|
*	Extend basesystem_partial_evaluation_RHS	Jason Gross	2017-10-15
\| \| \| \| \|	Now there's a version that handles things in Saturated.Core, and in Wrappers.
*	Add strip_subst_local	Jason Gross	2017-10-15
\|
*	Add some constants from montgomery	Jason Gross	2017-10-15
\|
*	Fix some issues with reification debug printing	Jason Gross	2017-10-15
\|
*	Remove *Display.vo from, e.g., selected-specific	Jason Gross	2017-10-15
\|
*	Add more constant notations from solinas primes	Jason Gross	2017-10-15
\|
*	Fix a typo in the previous commit	Jason Gross	2017-10-14
\|
*	Split up solve_op_mod_eq	Jason Gross	2017-10-14
\| \| \| \|	This way, we can reuse it even when we can't fully compute the values
*	Prettier json file generation	Jason Gross	2017-10-14
\|
*	Generate sz as an int in python2	Jason Gross	2017-10-14
\|
*	Add generated json files from generate_parameters.py	Jason Gross	2017-10-14
\|