fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
...
*	Add MulSplitUnfolder	Jason Gross	2017-10-17
\|
*	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.
*	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
*	Add UniformWeightInstances	Jason Gross	2017-10-09
\|
*	Add cbv_runtime in Arithmetic/Core	Jason Gross	2017-07-08
\| \| \| \|	This way, files importing Core don't have to keep track of the list of runtime operations, for unfoling.
*	More fine-grained tactics imports	Jason Gross	2017-07-08
\|
*	Remove some admitted lemmas	Jason Gross	2017-07-07
\|
*	enforce use of [F.zero], [F.one]; prove Ed25519 admits	Andres Erbsen	2017-07-07
\|
*	prove ModularArithmeticTheorems admits	Andres Erbsen	2017-07-06
\|
*	Fix a typo that ends up not mattering	Jason Gross	2017-07-06
\|
*	Closed under the global context	Andres Erbsen	2017-07-02
\|
*	prove [MontgomeryAPI.small_add]	Andres Erbsen	2017-07-02
\|
*	fix [small_div] arguments	Andres Erbsen	2017-07-02
\|
*	[small] admits progress...	Andres Erbsen	2017-07-01
\|
*	proved small_sat_add	jadep	2017-07-01
\|
*	change opp to runtime_opp	jadep	2017-07-01
\|
*	proved remaining [eval] admits in MontgomeryAPI	jadep	2017-07-01
\|
*	Prove saturated carrying-subtraction-chain correct	jadep	2017-07-01
\|
*	Prove saturated carrying-addition-chain correct	jadep	2017-06-30
\|
*	Reorganization of saturated arithmetic	jadep	2017-06-29
\|
*	create directory for saturated arithmetic in preparation for splitting into ↵	jadep	2017-06-29
\| \| \| \|	multiple files
*	Merge branch 'addsubchains'	jadep	2017-06-29
\|\
* \|	new add/carry chain logic with admitted proofs	jadep	2017-06-29
\| \|
* \|	Skeleton for add/subtract chains (see #222)	jadep	2017-06-29
\| \|
\| *	Fix the sense of op_{get,with}_carry in Saturated	Jason Gross	2017-06-29
\| \| \| \| \| \| \| \|	Now it lines up with the things in Z.Definitions
\| *	Adapt to new arguments of saturated things	Jason Gross	2017-06-29
\| \|
\| *	Fix type signatures of saturated things for WBW	Jason Gross	2017-06-29
\| \| \| \| \| \| \| \| \| \|	This required admitting some proofs. @jadephilipoom, please sanity-check this.
\| *	new add/carry chain logic with admitted proofs	jadep	2017-06-29
\| \|
\| *	Skeleton for add/subtract chains (see #222)	jadep	2017-06-28
\|/
*	proved eval_mod and eval_div (last remaining eval_ admits in Saturated)	jadep	2017-06-27
\|
*	Add a comment for nonzero_cps	Jason Gross	2017-06-26
\|
*	Fix a broken proof	Jason Gross	2017-06-26
\|
*	Factor out admitted proof into admitted lemma	Jason Gross	2017-06-26
\|
*	Add nonzero synthesis	Jason Gross	2017-06-26
\|
*	indentation	Jason Gross	2017-06-25
\|
*	Prove map2_zselect	Jason Gross	2017-06-25
\|
*	Fixes #219	jadep	2017-06-25
\|
*	Clean up some montgomery wbw instantiation, make display	Jason Gross	2017-06-24
\|
*	Fill in axioms for sub_then_maybe_add; this required fiddling with updated ↵	jadep	2017-06-24
\| \| \| \|	arguments since more context variables were used in the definitions than in the placeholder axioms
*	made conditional_add a wrapper, defined and proved sub_then_maybe_add	jadep	2017-06-24
\|
*	Make a 'conditionals' section in Columns, and move conditional_add there	jadep	2017-06-24
\|
*	Add (partially admitted) integration tests for add, sub, opp	Jason Gross	2017-06-22
\|
*	P256: Partial work on add, sub, opp	Jason Gross	2017-06-22
\| \| \| \|	Partial work towards #218
*	Account for future changes of #219	Jason Gross	2017-06-22
\| \| \| \| \|	Note that this makes the axiom we added false. It has a very long and descriptive name to account for this fact.
*	Prove In_to_list_left_tl, In_left_hd, to_list_left_append	Jason Gross	2017-06-21
\|
*	Prove some admitted lemmas about uweight	Jason Gross	2017-06-21
\| \| \| \|	Not sure if locally adding hypotheses is the best way to do it.
*	changed number of limbs partway through conditional_sub; was n, now S n	jadep	2017-06-20
\|
*	Make use of new conditional_subtract	Jason Gross	2017-06-20
\|