fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Show the bounds going wrong in karatsuba	Jason Gross	2017-06-15
\|
*	Display Z operations with ℤ attached	Jason Gross	2017-06-15
\| \| \| \|	This is the lighter-weight solution to #197.
*	Eliminate well-bounded IdWithAlt from final output	Jason Gross	2017-06-15
\| \| \| \|	This closes #195
*	Improve replace_match_with_destructuring_match	Jason Gross	2017-06-15
\| \| \| \| \|	Now it handles matches under binders, e.g., under dlet. This fixes https://github.com/mit-plv/fiat-crypto/issues/195#issuecomment-308724129.
*	Fix debugging code	Jason Gross	2017-06-15
\| \| \| \|	It was previously trying to run constrs and erroring when we turned on debugging
*	Don't force [Require Import String] for debug msgs	Jason Gross	2017-06-15
\|
*	Fix a changed case in the proof in loop.v	Jason Gross	2017-06-15
\|
*	Better for_loop induction principle	Jason Gross	2017-06-15
\| \| \| \|	Don't require that the test be strict
*	Export ZUtil.Z2Nat in ZUtil	Jason Gross	2017-06-15
\|
*	Add ZUtil.Z2Nat	Jason Gross	2017-06-15
\|
*	Add for_cps_unroll1	Jason Gross	2017-06-15
\| \| \| \|	It unrolls a for-loop once at the head of the loop
*	Add eq_loop_cps_large_n	Jason Gross	2017-06-15
\|
*	Edwards coordinates precomputed addition formula	Andres Erbsen	2017-06-15
\|
*	move CPS notations to Util.CPSNotations	Andres Erbsen	2017-06-15
\|
*	fix wrong number of limbs for square as well	jadep	2017-06-15
\|
*	fix wrong number of limbs	jadep	2017-06-15
\|
*	Added reduce to karatsuba synthesis	jadep	2017-06-15
\|
*	eddsa spec fix	Andres Erbsen	2017-06-14
\|
*	typofix	Andres Erbsen	2017-06-14
\|
*	fix goldilocks karatsuba; TODO implement reduce	Andres Erbsen	2017-06-14
\|
*	Loop changes, ScalarMultBase_correct with admits	Andres Erbsen	2017-06-14
\|
*	loops WIP	Andres Erbsen	2017-06-14
\|
*	ScalarMult: Z -> G -> G (closes #193)	Andres Erbsen	2017-06-14
\|
*	Fix the use of TARGETS on travis	Jason Gross	2017-06-14
\|
*	Add a printlite target to display lite files	Jason Gross	2017-06-14
\|
*	Error if Makefile.vo_closure doesn't exist and we need it	Jason Gross	2017-06-14
\|
*	Also test the 'lite' target on 8.6 in travis	Jason Gross	2017-06-14
\|
*	Add constant-pushing IdWithAlt optimization	Jason Gross	2017-06-14
\|
*	Rework and speed up arithmetic simplifier proofs	Jason Gross	2017-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Induction is so much faster than brute force. After \| File Name \| Before \|\| Change -------------------------------------------------------------------------------- 6m15.02s \| Total \| 7m14.18s \|\| -0m59.15s -------------------------------------------------------------------------------- 0m11.62s \| Compilers/Z/ArithmeticSimplifierWf \| 0m42.97s \|\| -0m31.35s 0m06.52s \| Compilers/Z/ArithmeticSimplifierInterp \| 0m34.28s \|\| -0m27.76s 2m47.55s \| Specific/IntegrationTestLadderstep \| 2m48.14s \|\| -0m00.58s 1m09.50s \| Specific/IntegrationTestKaratsubaMul \| 1m08.86s \|\| +0m00.64s 1m03.53s \| Specific/IntegrationTestLadderstep130 \| 1m04.05s \|\| -0m00.51s 0m16.39s \| Specific/IntegrationTestFreeze \| 0m16.29s \|\| +0m00.10s 0m13.60s \| Specific/IntegrationTestMul \| 0m13.60s \|\| +0m00.00s 0m11.58s \| Specific/IntegrationTestSub \| 0m11.36s \|\| +0m00.22s 0m09.79s \| Specific/IntegrationTestSquare \| 0m09.71s \|\| +0m00.07s 0m03.64s \| Compilers/Z/Bounds/Pipeline/Definition \| 0m03.54s \|\| +0m00.10s 0m00.75s \| Compilers/Z/Bounds/Pipeline/ReflectiveTactics \| 0m00.80s \|\| -0m00.05s 0m00.55s \| Compilers/Z/Bounds/Pipeline \| 0m00.58s \|\| -0m00.02s
*	Make rewrite_eta_match_base_type_impl a bit faster	Jason Gross	2017-06-13
\|
*	Fix a typo	Jason Gross	2017-06-13
\|
*	Add rewrite_eta_match_base_type_impl	Jason Gross	2017-06-13
\|
*	Add eta_match_base_type_impl	Jason Gross	2017-06-13
\|
*	Stronger invert_op tactic	Jason Gross	2017-06-13
\| \| \| \|	Now it can handle ops that return (Tbase TZ)
*	Fix a major bug in C-notation printing	Jason Gross	2017-06-13
\| \| \| \| \| \| \|	Binary operations with casts were wrongly parenthesized. Luckily, this impacted nothing in A-normal form, and it impacted nothing that is currently displayed. It does, however, impact the display of karatsuba mul.
*	Don't unfold id_with_alt	Jason Gross	2017-06-13
\| \| \| \|	Oops
*	Move temporary CNotations import	Jason Gross	2017-06-13
\|
*	Reify Z.mul_with_split_at_bitwidth	Jason Gross	2017-06-13
\|
*	Add mul_split_at_bitwidth, define things in terms of that	Jason Gross	2017-06-13
\| \| \| \| \|	This will make it easier on the reflective machinery, because it won't have to carry around such large constants.
*	Update WBW montgomery comments	Jason Gross	2017-06-13
\| \| \| \|	As per https://github.com/mit-plv/fiat-crypto/commit/b4b711cba32a21806c6c0aae53be40c04af60cb3#commitcomment-22521097
*	Add Z.peano_rect_strong	Jason Gross	2017-06-13
\| \| \| \|	This version provides hypotheses about the non{negativity,positivity} of the Z.
*	Add dec_eq_comparison	Jason Gross	2017-06-13
\|
*	Add Z.peano_rect	Jason Gross	2017-06-13
\|
*	Fill in mul_split to wbw montgomery	Jason Gross	2017-06-13
\|
*	Add Z.mul_split	Jason Gross	2017-06-13
\|
*	WBW-montgomery: Fill in most context variables	Jason Gross	2017-06-13
\|
*	finish computational portions of operations needed for Montgomery, and ↵	jadep	2017-06-12
\| \| \| \|	sketch out some of the proofs as discussed in #157
*	Remove use of id_tuple_with_alt_proof	Jason Gross	2017-06-12
\| \| \| \|	We (@jadephilipoom?) should now remove the dead-code admits.
*	Add a Show to keep track of where we are in karatsuba	Jason Gross	2017-06-12
\|
*	Handle IdWithAlt in the simplifier	Jason Gross	2017-06-12
\| \| \| \| \|	It now knows how to deal with _ + 0 involving words, and also eliminates IdWithAlt when both the first argument and the output are the same size word.