Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | Add MulSplitUnfolder | 2017-10-17 | ||
| | ||||
* | Add faster arithmetic unfolding | 2017-10-15 | ||
| | ||||
* | Extend basesystem_partial_evaluation_RHS | 2017-10-15 | ||
| | | | | | Now there's a version that handles things in Saturated.Core, and in Wrappers. | |||
* | Fix a typo in the previous commit | 2017-10-14 | ||
| | ||||
* | Split up solve_op_mod_eq | 2017-10-14 | ||
| | | | | This way, we can reuse it even when we can't fully compute the values | |||
* | Add UniformWeightInstances | 2017-10-09 | ||
| | ||||
* | Add cbv_runtime in Arithmetic/Core | 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 | 2017-07-08 | ||
| | ||||
* | Remove some admitted lemmas | 2017-07-07 | ||
| | ||||
* | enforce use of [F.zero], [F.one]; prove Ed25519 admits | 2017-07-07 | ||
| | ||||
* | prove ModularArithmeticTheorems admits | 2017-07-06 | ||
| | ||||
* | Fix a typo that ends up not mattering | 2017-07-06 | ||
| | ||||
* | Closed under the global context | 2017-07-02 | ||
| | ||||
* | prove [MontgomeryAPI.small_add] | 2017-07-02 | ||
| | ||||
* | fix [small_div] arguments | 2017-07-02 | ||
| | ||||
* | [small] admits progress... | 2017-07-01 | ||
| | ||||
* | proved small_sat_add | 2017-07-01 | ||
| | ||||
* | change opp to runtime_opp | 2017-07-01 | ||
| | ||||
* | proved remaining [eval] admits in MontgomeryAPI | 2017-07-01 | ||
| | ||||
* | Prove saturated carrying-subtraction-chain correct | 2017-07-01 | ||
| | ||||
* | Prove saturated carrying-addition-chain correct | 2017-06-30 | ||
| | ||||
* | Reorganization of saturated arithmetic | 2017-06-29 | ||
| | ||||
* | create directory for saturated arithmetic in preparation for splitting into ↵ | 2017-06-29 | ||
| | | | | multiple files | |||
* | Merge branch 'addsubchains' | 2017-06-29 | ||
|\ | ||||
* | | new add/carry chain logic with admitted proofs | 2017-06-29 | ||
| | | ||||
* | | Skeleton for add/subtract chains (see #222) | 2017-06-29 | ||
| | | ||||
| * | Fix the sense of op_{get,with}_carry in Saturated | 2017-06-29 | ||
| | | | | | | | | Now it lines up with the things in Z.Definitions | |||
| * | Adapt to new arguments of saturated things | 2017-06-29 | ||
| | | ||||
| * | Fix type signatures of saturated things for WBW | 2017-06-29 | ||
| | | | | | | | | | | This required admitting some proofs. @jadephilipoom, please sanity-check this. | |||
| * | new add/carry chain logic with admitted proofs | 2017-06-29 | ||
| | | ||||
| * | Skeleton for add/subtract chains (see #222) | 2017-06-28 | ||
|/ | ||||
* | proved eval_mod and eval_div (last remaining eval_ admits in Saturated) | 2017-06-27 | ||
| | ||||
* | Add a comment for nonzero_cps | 2017-06-26 | ||
| | ||||
* | Fix a broken proof | 2017-06-26 | ||
| | ||||
* | Factor out admitted proof into admitted lemma | 2017-06-26 | ||
| | ||||
* | Add nonzero synthesis | 2017-06-26 | ||
| | ||||
* | indentation | 2017-06-25 | ||
| | ||||
* | Prove map2_zselect | 2017-06-25 | ||
| | ||||
* | Fixes #219 | 2017-06-25 | ||
| | ||||
* | Clean up some montgomery wbw instantiation, make display | 2017-06-24 | ||
| | ||||
* | Fill in axioms for sub_then_maybe_add; this required fiddling with updated ↵ | 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 | 2017-06-24 | ||
| | ||||
* | Make a 'conditionals' section in Columns, and move conditional_add there | 2017-06-24 | ||
| | ||||
* | Add (partially admitted) integration tests for add, sub, opp | 2017-06-22 | ||
| | ||||
* | P256: Partial work on add, sub, opp | 2017-06-22 | ||
| | | | | Partial work towards #218 | |||
* | Account for future changes of #219 | 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 | 2017-06-21 | ||
| | ||||
* | Prove some admitted lemmas about uweight | 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 | 2017-06-20 | ||
| | ||||
* | Make use of new conditional_subtract | 2017-06-20 | ||
| |