| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add decidable equality with nil |  Jason Gross | 2017-08-13 |
| | | |||
| * | Make some tactics a bit more powerful | Jason Gross | 2017-07-08 |
| | | |||
| * | More fine-grained tactics imports | Jason Gross | 2017-07-08 |
| | | |||
| * | More fine-grained imports | Jason Gross | 2017-07-08 |
| | | |||
| * | Add UnfoldArg | Jason Gross | 2017-07-08 |
| | | |||
| * | prove an admit in ArithmeticSynthesisTest |  Andres Erbsen | 2017-07-06 |
| | | |||
| * | Add wrappers for subborrow and add_with_get_carry so they work when it is ↵ |  jadep | 2017-06-29 |
| | | | | | not known that they split on a power of 2 | ||
| * | remove unused admit (has been moved to Tuple.v) | jadep | 2017-06-26 |
| | | |||
| * | Prove map2_append | Jason Gross | 2017-06-25 |
| | | |||
| * | write and prove Tuple.map2_cps | jadep | 2017-06-25 |
| | | |||
| * | Fix a typo in push_Zmod that was causing looping | Jason Gross | 2017-06-22 |
| | | |||
| * | Fix some minor naming bugs in sig_assoc tactics | Jason Gross | 2017-06-22 |
| | | |||
| * | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| | | |||
| * | Prove In_to_list_left_tl, In_left_hd, to_list_left_append | Jason Gross | 2017-06-21 |
| | | |||
| * | Add is_bounded_by_None_repeat_In_iff_lt | Jason Gross | 2017-06-20 |
| | | |||
| * | Add fold_left_orb_true, fold_left_orb_pull | Jason Gross | 2017-06-20 |
| | | |||
| * | Add is_bounded_by_None_repeat_In_iff | Jason Gross | 2017-06-20 |
| | | |||
| * | [Require NatUtil] should not change [tauto] | Jason Gross | 2017-06-19 |
| | | | | | | | | | | Work around [bug #5444](https://coq.inria.fr/bugs/show_bug.cgi?id=5444), [Require Nsatz] should not change the behavior of [tauto]. Because [tauto] is stupid and checks to see whether or not [Classical_Prop] has been *required* to decide whether or not to use classical axioms. Aren't side-effects of [Require] wonderful? Since we're not actually using nsatz or psatz in NatUtil, we now simply [Require Import Lia]. | ||
| * | Add ModInv | Jason Gross | 2017-06-18 |
| | | | | | This closes #209. | ||
| * | Stronger zero_bounds | Jason Gross | 2017-06-18 |
| | | |||
| * | Add div_nonneg to zarith | Jason Gross | 2017-06-18 |
| | | |||
| * | Add Z.div_nonneg | Jason Gross | 2017-06-18 |
| | | |||
| * | Add eq_ZToWord | Jason Gross | 2017-06-17 |
| | | |||
| * | Unfold Z.mul_split_at_bitwidth for reification | Jason Gross | 2017-06-17 |
| | | | | | Also reimplement it with a shift and a mask | ||
| * | finish tuple-ifying Montgomery API | jadep | 2017-06-16 |
| | | |||
| * | CPSify Saturated API in preparation for CPSifying Montgomery (see #194) | jadep | 2017-06-15 |
| | | |||
| * | Don't force [Require Import String] for debug msgs | Jason Gross | 2017-06-15 |
| | | |||
| * | Fix a changed case in the proof in loop.v | Jason Gross | 2017-06-15 |
| | | |||
| * | Better for_loop induction principle | Jason Gross | 2017-06-15 |
| | | | | | Don't require that the test be strict | ||
| * | Export ZUtil.Z2Nat in ZUtil | Jason Gross | 2017-06-15 |
| | | |||
| * | Add ZUtil.Z2Nat | Jason Gross | 2017-06-15 |
| | | |||
| * | Add for_cps_unroll1 | Jason Gross | 2017-06-15 |
| | | | | | It unrolls a for-loop once at the head of the loop | ||
| * | Add eq_loop_cps_large_n | Jason Gross | 2017-06-15 |
| | | |||
| * | move CPS notations to Util.CPSNotations | Andres Erbsen | 2017-06-15 |
| | | |||
| * | Loop changes, ScalarMultBase_correct with admits | Andres Erbsen | 2017-06-14 |
| | | |||
| * | loops WIP | Andres Erbsen | 2017-06-14 |
| | | |||
| * | ScalarMult: Z -> G -> G (closes #193) | Andres Erbsen | 2017-06-14 |
| | | |||
| * | Add mul_split_at_bitwidth, define things in terms of that | Jason Gross | 2017-06-13 |
| | | | | | | This will make it easier on the reflective machinery, because it won't have to carry around such large constants. | ||
| * | Add Z.peano_rect_strong | Jason Gross | 2017-06-13 |
| | | | | | This version provides hypotheses about the non{negativity,positivity} of the Z. | ||
| * | Add dec_eq_comparison | Jason Gross | 2017-06-13 |
| | | |||
| * | Add Z.peano_rect | Jason Gross | 2017-06-13 |
| | | |||
| * | Add Z.mul_split | Jason Gross | 2017-06-13 |
| | | |||
| * | Fix zrange notation levels | Jason Gross | 2017-06-12 |
| | | | | | So that it doesn't interfere with [~> R] and [A ~> B]. | ||
| * | Add unfold lemmas for id_with_alt | Jason Gross | 2017-06-11 |
| | | |||
| * | Add IdfunWithAlt | Jason Gross | 2017-06-11 |
| | | |||
| * | Add script to remake Tactics.v file | Jason Gross | 2017-06-11 |
| | | |||
| * | Add clearbody_all | Jason Gross | 2017-06-11 |
| | | |||
| * | Fix loop notations, add for loops | Jason Gross | 2017-06-11 |
| | | |||
| * | Reserve some more notations | Jason Gross | 2017-06-11 |
| | | |||
| * | cps notations WIP... | Andres Erbsen | 2017-06-11 |
| | | |||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |