fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Split off ZUtil.Stabilization, finish IsBoundedBy!	Jason Gross	2017-04-09
\|
*	More wip on bounds	Jason Gross	2017-04-09
\|
*	More progress on bounds	Jason Gross	2017-04-09
\|
*	Don't take abs in upper_lor_and_bounds	Jason Gross	2017-04-09
\|
*	Take more abs in Bounds.Interpretation	Jason Gross	2017-04-09
\|
*	Factor out Z.{lor,land} proofs a bit more	Jason Gross	2017-04-09
\|
*	Finish shift cases, extract out land, lor facts	Jason Gross	2017-04-09
\|
*	WIP on bounds lemma	Jason Gross	2017-04-08
\|
*	More WIP on PullCast	Jason Gross	2017-04-08
\|
*	Add interpToZ_range	Jason Gross	2017-04-08
\|
*	Add ZToInterp_eq_inj	Jason Gross	2017-04-08
\|
*	Use Z.max 0, not an if statement	Jason Gross	2017-04-08
\| \| \| \|	Leads to fewer match branches
*	Add interpToZ_ZToInterp_mod	Jason Gross	2017-04-08
\|
*	Add cast_const_mod lemmas	Jason Gross	2017-04-08
\|
*	Add cast_const_split_mod	Jason Gross	2017-04-08
\|
*	More WIP on PullCast	Jason Gross	2017-04-08
\|
*	Add cast_const_idempotent_small	Jason Gross	2017-04-08
\|
*	WIP on pullcast	Jason Gross	2017-04-08
\|
*	Work in progress on proving PullCast	Jason Gross	2017-04-07
\|
*	Remove useless imports	Jason Gross	2017-04-07
\|
*	Split up Compilers/Z/Bounds/InterpretationLemmas	Jason Gross	2017-04-07
\|
*	Parameterize bounds analysis over round_up	Jason Gross	2017-04-07
\|
*	Add inversion_base_type_constr	Jason Gross	2017-04-07
\|
*	Slightly faster reification	Jason Gross	2017-04-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Be better at what we do and don't unfold for when proving interpretation via [reflexivity]. This lets us handle the reification part of the pipeline when we chose to have only one limb. After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------- 5m50.80s \| Total \| 5m53.13s \|\| -0m02.33s -------------------------------------------------------------------------------- 3m41.27s \| Specific/IntegrationTestLadderstep \| 3m43.35s \|\| -0m02.07s 1m30.39s \| Specific/IntegrationTestLadderstep130 \| 1m29.79s \|\| +0m00.60s 0m13.60s \| Specific/IntegrationTestMul \| 0m13.52s \|\| +0m00.08s 0m11.00s \| Specific/IntegrationTestSub \| 0m11.36s \|\| -0m00.35s 0m03.50s \| Compilers/TestCase \| 0m03.64s \|\| -0m00.14s 0m03.14s \| Specific/FancyMachine256/Montgomery \| 0m03.26s \|\| -0m00.11s 0m02.97s \| Specific/FancyMachine256/Barrett \| 0m03.06s \|\| -0m00.08s 0m01.88s \| Specific/FancyMachine256/Core \| 0m01.94s \|\| -0m00.06s 0m00.68s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics \| 0m00.78s \|\| -0m00.09s 0m00.53s \| Compilers/Z/Bounds/Pipeline \| 0m00.54s \|\| -0m00.01s 0m00.48s \| Compilers/InputSyntax \| 0m00.51s \|\| -0m00.03s 0m00.46s \| Compilers/Z/Reify \| 0m00.50s \|\| -0m00.03s 0m00.46s \| Compilers/Z/Bounds/Pipeline/Glue \| 0m00.51s \|\| -0m00.04s 0m00.44s \| Compilers/Reify \| 0m00.38s \|\| +0m00.06s
*	Display un-interped C code	Jason Gross	2017-04-07
\|
*	Add Display files and targets	Jason Gross	2017-04-07
\|
*	Merge branch 'rename-everything'. Closes #14.	Andres Erbsen	2017-04-06
\|
*	rename-everything	Andres Erbsen	2017-04-06