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 | |
| |