| Commit message (Expand) | 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 |
| * | Fix a typo in the previous commit | Jason Gross | 2017-10-14 |
| * | Split up solve_op_mod_eq | Jason Gross | 2017-10-14 |
| * | Add UniformWeightInstances | Jason Gross | 2017-10-09 |
| * | Add cbv_runtime in Arithmetic/Core | Jason Gross | 2017-07-08 |
| * | 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 m... | jadep | 2017-06-29 |
| * | 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 |
| | * | 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 |
| | * | 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 ar... | jadep | 2017-06-24 |
| * | 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 |
| * | Account for future changes of #219 | Jason Gross | 2017-06-22 |
| * | 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 |
| * | 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 |
Jason Gross
Andres Erbsen
jadep