fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Unfold tuple arguments in reflective pipeline	Jason Gross	2017-07-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This closes #239 After \| File Name \| Before \|\| Change --------------------------------------------------------------------------------------- 10m04.12s \| Total \| 10m05.68s \|\| -0m01.55s --------------------------------------------------------------------------------------- 2m45.12s \| Specific/X25519/C64/ladderstep \| 2m48.45s \|\| -0m03.32s 1m06.06s \| Specific/IntegrationTestLadderstep130 \| 1m04.76s \|\| +0m01.29s 2m03.02s \| Specific/NISTP256/AMD64/femul \| 2m02.29s \|\| +0m00.72s 1m20.35s \| Specific/IntegrationTestKaratsubaMul \| 1m20.10s \|\| +0m00.25s 0m25.29s \| Specific/IntegrationTestMontgomeryP256_128 \| 0m25.17s \|\| +0m00.11s 0m16.66s \| Specific/IntegrationTestFreeze \| 0m16.18s \|\| +0m00.48s 0m14.81s \| Specific/NISTP256/AMD64/feadd \| 0m15.09s \|\| -0m00.27s 0m14.58s \| Specific/NISTP256/AMD64/fesub \| 0m14.48s \|\| +0m00.09s 0m13.23s \| Specific/X25519/C64/femul \| 0m13.54s \|\| -0m00.30s 0m12.00s \| Specific/NISTP256/AMD64/feopp \| 0m12.07s \|\| -0m00.07s 0m11.25s \| Specific/IntegrationTestMontgomeryP256_128_Add \| 0m11.44s \|\| -0m00.18s 0m11.23s \| Specific/IntegrationTestMontgomeryP256_128_Sub \| 0m11.19s \|\| +0m00.04s 0m11.06s \| Specific/IntegrationTestSub \| 0m11.24s \|\| -0m00.17s 0m10.39s \| Specific/IntegrationTestMontgomeryP256_128_Opp \| 0m10.41s \|\| -0m00.01s 0m09.85s \| Specific/X25519/C64/fesquare \| 0m09.75s \|\| +0m00.09s 0m09.19s \| Specific/NISTP256/AMD64/fenz \| 0m09.04s \|\| +0m00.15s 0m08.76s \| Specific/IntegrationTestMontgomeryP256_128_Nonzero \| 0m09.11s \|\| -0m00.34s 0m00.69s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics \| 0m00.80s \|\| -0m00.11s 0m00.59s \| Compilers/Z/Bounds/Pipeline \| 0m00.57s \|\| +0m00.02s
*	Fix CSE_sym denote	Jason Gross	2017-07-07
\|
*	Fix proofs broken by previous commit	Jason Gross	2017-07-07
\|
*	Stronger contexts	Jason Gross	2017-07-07
\|
*	Remove some admitted lemmas	Jason Gross	2017-07-07
\|
*	Fix a mis-aligned comment marker in CNotations script	Jason Gross	2017-07-03
\|
*	change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`	Jason Gross	2017-06-29
\| \| \| \|	This closes #228
*	Fix comment-in-string issues	Jason Gross	2017-06-29
\|
*	More C Notations for uin8_t-valued addcarryx	Jason Gross	2017-06-29
\|
*	Remove a [Check]	Jason Gross	2017-06-29
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	Allow disabling adc-fusion	Jason Gross	2017-06-25
\|
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-25
\| \| \| \|	Actually this time
*	Revert "Convert adc to sbb when doing [0 - x]"	Jason Gross	2017-06-25
\| \| \| \| \| \|	This reverts commit ecff47dbc867261b81c6e268eca99e5b5ab28805. It was wrong
*	Convert adc to sbb when doing [0 - x]	Jason Gross	2017-06-24
\|
*	Propogate neg through constant multiplication	Jason Gross	2017-06-24
\|
*	Add notation for logical or	Jason Gross	2017-06-22
\|
*	Work around bug #5615 (constr not being updated)	Jason Gross	2017-06-22
\| \| \| \| \| \|	This is https://coq.inria.fr/bugs/show_bug.cgi?id=5615, Ltac should be able to bind references and not just names, in which names are slippery, slippery objects.
*	Also key adc->sbb on the carry-bit being negative	Jason Gross	2017-06-20
\| \| \| \|	This is needed when we're subtracting 0 >.>
*	Add more simplification passes (de-doubling opp)	Jason Gross	2017-06-20
\|
*	Add more simplification passes (de-doubling opp)	Jason Gross	2017-06-20
\|
*	Add more Z-notations	Jason Gross	2017-06-20
\|
*	Add another fusion to adc-fusion	Jason Gross	2017-06-20
\| \| \| \| \| \| \|	Might have something to do with #213. Also, RewriteAddToAdcInterp is now a bit more stable under changes to the rewriting strategy (the parts are now more separate).
*	Use solve_wf_side_condition to synch the depth of auto with wf	Jason Gross	2017-06-20
\|
*	Add more constant notations	Jason Gross	2017-06-20
\|
*	Add more constants	Jason Gross	2017-06-18
\|
*	Better simplification of mulsplit	Jason Gross	2017-06-18
\|
*	Fix typo in format	Jason Gross	2017-06-18
\|
*	Add fake notation for addcarryx_u128 and similar	Jason Gross	2017-06-18
\|
*	Add some notations for mulx	Jason Gross	2017-06-18
\|
*	Better test for simplifier	Jason Gross	2017-06-18
\| \| \| \|	This one catches more things
*	Stronger simplification of adc too add when we can prove the carry is 0	Jason Gross	2017-06-18
\|
*	Add cnotations for addcarryx with uint8_t	Jason Gross	2017-06-18
\|
*	Add convenience for supporting uint8	Jason Gross	2017-06-18
\|
*	Add notations	Jason Gross	2017-06-18
\|
*	Adding more (possibly unneeded) simplification	Jason Gross	2017-06-18
\|
*	Try more simplification	Jason Gross	2017-06-17
\|
*	Drop the 0-carry bit before bounds analysis	Jason Gross	2017-06-17
\|
*	Be a bit more forceful in eliminating zeros in arith simpl	Jason Gross	2017-06-17
\|
*	More arithmetic simplification for adc, mul	Jason Gross	2017-06-17
\|
*	Add more simplification to pipeline	Jason Gross	2017-06-17
\| \| \| \|	This seemes to be making it slower though....
*	Add linearization to inline pairs in post-bounds pipeline	Jason Gross	2017-06-17
\|
*	Add extra simplification to simplifier for adc	Jason Gross	2017-06-17
\|
*	Add more constants	Jason Gross	2017-06-17
\|
*	Unfold Z.mul_split_at_bitwidth for reification	Jason Gross	2017-06-17
\| \| \| \|	Also reimplement it with a shift and a mask
*	Add some more display constants	Jason Gross	2017-06-17
\|
*	Add bool into P256	Jason Gross	2017-06-17
\|
*	Remove fails; if we fail too strongly, we miss debugging information	Jason Gross	2017-06-17
\|
*	Try to fail a bit faster in bad reification	Jason Gross	2017-06-17
\|
*	Add back failure at level 100	Jason Gross	2017-06-17
\| \| \| \|	We still need to idtac, because tc resolution eats messages from fail at any level