Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | partition -> Partition.partition to prevent confusion with List.partition | jadep | 2019-04-03 |
| | |||
* | update _CoqProject, fix indentations, and prune dependencies of new ↵ | jadep | 2019-04-03 |
| | | | | Arithmetic files | ||
* | split up Arithmetic (imports etc. not yet fixed, does not build) | jadep | 2019-04-03 |
| | |||
* | 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 | ||
| * | 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 |
| | |||
* | Factor out admitted proof into admitted lemma | Jason Gross | 2017-06-26 |
| | |||
* | Add nonzero synthesis | Jason Gross | 2017-06-26 |
| | |||
* | Prove map2_zselect | Jason Gross | 2017-06-25 |
| | |||
* | Fixes #219 | jadep | 2017-06-25 |
| | |||
* | 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 |
| | |||
* | 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 |
| | |||
* | Remove duplicate [small p] hypothesis from small_conditional_sub | Jason Gross | 2017-06-20 |
| | |||
* | Add conditional_sub_id to uncps globally | Jason Gross | 2017-06-20 |
| | |||
* | defined conditional_sub (see #207) -- small_conditional_sub admitted, ↵ | jadep | 2017-06-20 |
| | | | | eval_conditional_sub proven | ||
* | rename Columns.sub_cps to make it clear that no balance is added | jadep | 2017-06-20 |
| | |||
* | Don't depend on classical axioms for small_add | Jason Gross | 2017-06-20 |
| | | | | See [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444). | ||
* | Weaken preconditions on small_add | Jason Gross | 2017-06-20 |
| | |||
* | Strip trailing whitespace | Jason Gross | 2017-06-20 |
| | |||
* | fixed precondition on small_add | jadep | 2017-06-19 |
| | |||
* | proved small_scmul | jadep | 2017-06-18 |
| | |||
* | proved eval_scmul | jadep | 2017-06-18 |
| | |||
* | proved small_zero | jadep | 2017-06-18 |
| | |||
* | proved small_drop_high | jadep | 2017-06-18 |
| | |||
* | proved eval_drop_high | jadep | 2017-06-18 |
| | |||
* | define strong small and re-prove small_add and small_compact with that ↵ | jadep | 2017-06-18 |
| | | | | definition | ||
* | make scmul discard its carry in a saner way; rather than concatenating it in ↵ | jadep | 2017-06-18 |
| | | | | and then dropping it, we just ignore it | ||
* | Drop the 0-carry bit before bounds analysis | Jason Gross | 2017-06-17 |
| | |||
* | Fix scmul bounds issue | jadep | 2017-06-17 |
| | |||
* | More eye-catching naming scheme for nm in saturated | Jason Gross | 2017-06-17 |
| | |||
* | Make use of non-uniform tuple-based add | Jason Gross | 2017-06-17 |
| | | | | Maybe it'll result in better output code with fewer zeros? | ||
* | finish tuple-ifying Montgomery API | jadep | 2017-06-16 |
| | |||
* | Switch to using tuples for word-by-word montgomery | Jason Gross | 2017-06-16 |
| | | | | | | | The new parameterized definitions and proofs are in WordByWord/Abstract/Dependent/*; the old ones are untouched (and unused) in WordByWord/Abstract/*. I replaced definitions I didn't know how to write in the Saturated API with the use of an axiom. | ||
* | CPSify montgomery wbw reduction | Jason Gross | 2017-06-15 |
| | | | | | | I didn't want to bother redoing all of the proofs that I'd already done, so instead I prove the cps'ified version equal to the non-cps version, and transfer over the proofs that way. | ||
* | CPSify Saturated API in preparation for CPSifying Montgomery (see #194) | jadep | 2017-06-15 |
| | |||
* | Fill in mul_split to wbw montgomery | 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 | ||
* | add zero (as per #157) | jadep | 2017-06-08 |
| | |||
* | start saturated-arithmetic API for use in Montgomery (see discussion in #157) | jadep | 2017-06-08 |
| | |||
* | Don't rely on autogenerated names | Jason Gross | 2017-06-05 |
| | | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch). |