| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixed admit left from fsatz port |  jadep | 2017-03-02 |
| | | |||
| * | make 8.5 happy |  Andres Erbsen | 2017-03-02 |
| | | |||
| * | fixup NewBasesystem | Andres Erbsen | 2017-03-02 |
| | | |||
| * | remove dangling file that gives a warning | Andres Erbsen | 2017-03-02 |
| | | |||
| * | remove undeclared lines from Ed25519Extraction.v | Andres Erbsen | 2017-03-02 |
| | | |||
| * | move large non-building chunks of Ed25519.v | Andres Erbsen | 2017-03-02 |
| | | |||
| * | deleted src/Specific/GF25519ExtendedAddCoordinates.v | Andres Erbsen | 2017-03-02 |
| | | |||
| * | fix src/Specific/GF25519Reflective/Reified/AddCoordinates.v | Andres Erbsen | 2017-03-02 |
| | | |||
| * | remove PointEncoding | Andres Erbsen | 2017-03-02 |
| | | |||
| * | CompleteEdwardsCurveTheorems: point compression | Andres Erbsen | 2017-03-02 |
| | | |||
| * | PrimeFieldTheorems: inv for isomorphic fields | Andres Erbsen | 2017-03-02 |
| | | |||
| * | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | Andres Erbsen | 2017-03-02 |
| | | |||
| * | rewrite ExtendedCoordinates, fix Ed25519 | Andres Erbsen | 2017-03-02 |
| | | |||
| * | edwards curves over isomorphic fields | Andres Erbsen | 2017-03-02 |
| | | |||
| * | src/Tactics/Algebra_syntax/Nsatz.v: power 1 only | Andres Erbsen | 2017-03-02 |
| | | |||
| * | WIP | Andres Erbsen | 2017-03-02 |
| | | |||
| * | address some code review comments | Andres Erbsen | 2017-03-02 |
| | | |||
| * | Weierstrass curve is a group | Andres Erbsen | 2017-03-02 |
| | | |||
| * | Attempt Weierstrass associativity again, good progress. | Andres Erbsen | 2017-03-02 |
| | | |||
| * | change weierstrass spec, prove most cases of associativity | Andres Erbsen | 2017-03-02 |
| | | |||
| * | split the algebra library; use fsatz more | Andres Erbsen | 2017-03-02 |
| | | |||
| * | fsatz, nsatz_solve_nonzero | Andres Erbsen | 2017-03-02 |
| | | |||
| * | use field_nsatz in CompleteEdwardsCurve.Pre | Andres Erbsen | 2017-03-02 |
| | | |||
| * | field_nsatz | Andres Erbsen | 2017-03-02 |
| | | |||
| * | make assert_preconditions way more sane; use vm_decide to kill most subgoals | jadep | 2017-03-02 |
| | | |||
| * | Separated out [carry] from other operations. | jadep | 2017-03-02 |
| | | |||
| * | Modify/add to NewBaseSystem to match with what is needed for proof of ring ↵ | jadep | 2017-03-01 |
| | | | | | isomorphism to F | ||
| * | Fixed carry bugs (indexes need to be reversed, and we need to convert ↵ | jadep | 2017-03-01 |
| | | | | | to/from Positional every time we carry) and added an [encode] function | ||
| * | Defined [div] and [mod]; removed liftn_sig lemmas because they were actually ↵ | jadep | 2017-03-01 |
| | | | | | no longer needed | ||
| * | Adjust implicits of flatten_binding_list_same_in_eq |  Jason Gross | 2017-03-01 |
| | | |||
| * | Add flatten_binding_list_In_eq_iff, flatten_binding_list_same_in_eq | Jason Gross | 2017-03-01 |
| | | |||
| * | Add η principles for sigma types | Jason Gross | 2017-03-01 |
| | | |||
| * | Add dlet_nd notation | Jason Gross | 2017-03-01 |
| | | | | | This is for non-dependent [dlet]s, to help Coq's type inference | ||
| * | Switch to fully uncurried form for reflection | Jason Gross | 2017-03-01 |
| | | | | | | | | | | | | This will eventually make a number of proofs easier. Unfortunately, the correctness lemmas for AddCoordinates and LadderStep no longer work (because of different arities), and there's a proof in Experiments/Ed25519 that I've admitted. The correctness lemmas will be easy to re-add when we have a more general version that handle arbitrary type shapes. | ||
| * | Add interp_flat_type_rel_pointwise_SmartVarfMap, ↵ | Jason Gross | 2017-02-28 |
| | | | | | interp_flat_type_rel_pointwise_Reflexive | ||
| * | Add SmartVarfMap Proper instance | Jason Gross | 2017-02-28 |
| | | |||
| * | Add strip_eta_tuple lemmas | Jason Gross | 2017-02-28 |
| | | |||
| * | Better tuple_eta arguments | Jason Gross | 2017-02-28 |
| | | |||
| * | Add eta_tuple functions | Jason Gross | 2017-02-28 |
| | | | | | | These are for getting nicely reduced forms of, e.g., Tuple.map, without knowing exactly what the tuple is | ||
| * | Deduplicate code | Jason Gross | 2017-02-28 |
| | | | | | There was duplicate code in Reflection.Equality and Reflection.TypeInversion | ||
| * | Defined zero and one for NewBaseSystem | jadep | 2017-02-27 |
| | | |||
| * | Added operation (including creating ) | jadep | 2017-02-27 |
| | | |||
| * | Added subtraction | jadep | 2017-02-27 |
| | | |||
| * | added Positional wrappers for Associational operations, added correctness ↵ | jadep | 2017-02-27 |
| | | | | | proof of | ||
| * | changed names of ops in NewBaseSystem to reflect that they are sig and not sigT | jadep | 2017-02-27 |
| | | |||
| * | Modified lemma and created tactic to handle it; added reduce step to ↵ | jadep | 2017-02-26 |
| | | | | | multiplication operation; introduced modular equality to NewBaseSystem | ||
| * | removed leftover saturated stuff (will probably end up in a separate file ↵ | jadep | 2017-02-26 |
| | | | | | someday) | ||
| * | speed up NewBaseystem synthesis | Andres Erbsen | 2017-02-23 |
| | | | | | | | Use a vm_compute hack fromhttps://arxiv.org/pdf/1305.6543.pdf section 5.5: pattern terms over what to keep opaque, then reduce the lambda using vm_compute. | ||
| * | Add BoundsInterpretations | Jason Gross | 2017-02-23 |
| | | |||
| * | Add log and non-log versions of FixedWordSizes lem | Jason Gross | 2017-02-23 |
| | | |||
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |