Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add UnfoldArg | Jason Gross | 2017-07-08 |
| | |||
* | automate P256 integration | Andres Erbsen | 2017-07-02 |
| | |||
* | Reorganization of saturated arithmetic | jadep | 2017-06-29 |
| | |||
* | Add nonzero synthesis | Jason Gross | 2017-06-26 |
| | |||
* | Weierstrass Jacobian mixed addition | Andres Erbsen | 2017-06-23 |
| | |||
* | Add (partially admitted) integration tests for add, sub, opp | Jason Gross | 2017-06-22 |
| | |||
* | move Specifi p256 files into their own directory | Andres Erbsen | 2017-06-22 |
| | |||
* | src/Demo.v: a 200-line introduction to BaseSystem ideas | Andres Erbsen | 2017-06-21 |
| | |||
* | Add fold_left_orb_true, fold_left_orb_pull | Jason Gross | 2017-06-20 |
| | |||
* | Add ModInv | Jason Gross | 2017-06-18 |
| | | | | This closes #209. | ||
* | compile X25519 C code from Makefile | Andres Erbsen | 2017-06-18 |
| | |||
* | add 128-bit display file | Jason Gross | 2017-06-17 |
| | |||
* | Add 128-bit version of montgomery for testing | Jason Gross | 2017-06-17 |
| | |||
* | Finish MontgomeryP256 (less conditional subtract) | Jason Gross | 2017-06-17 |
| | |||
* | Add initial IntegrationTestMontgomeryP256.v | Jason Gross | 2017-06-17 |
| | |||
* | Fix spelling | Jason Gross | 2017-06-17 |
| | |||
* | 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. | ||
* | Fix build | Jason Gross | 2017-06-16 |
| | |||
* | Revert PR #203 | Jason Gross | 2017-06-16 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | As per https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309060964 and https://github.com/mit-plv/fiat-crypto/pull/203#issuecomment-309101747 Revert "update ocq2C sed script" This reverts commit 4a39f39e195b9b7273810a83de78dfd1d150783e. Revert "make display" This reverts commit cbf6d013c533d5165d749d0f9405a15d1ff0b43e. Revert "Make use of CArrayNotations" This reverts commit cae0e80ae76b76091e7fb86fcd794358a4fe55bb. Revert "Fix CArrayNotations" This reverts commit d0d0fbd4499296a2164e209466227892671556f0. Revert "Revert "Revert "Add CArrayNotations""" This reverts commit b2b8403ca76f6fd461d9a71ac2e9add4359bba8c. | ||
* | Revert "Revert "Add CArrayNotations"" | Jason Gross | 2017-06-16 |
| | | | | This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90. | ||
* | Revert "Add CArrayNotations" | Jason Gross | 2017-06-15 |
| | | | | | | | This reverts commit 44359b29d99ab52154dcfdf2b2b16bca7dbaf339. It triggers [bug #5469](https://coq.inria.fr/bugs/show_bug.cgi?id=5469), which is present in 8.6, but not v8.6 (nor 8.6.1, once it comes out). | ||
* | Finish karatsuba mul, add display file (#199) | Jason Gross | 2017-06-15 |
| | | | This closes #182. | ||
* | Add CArrayNotations | Jason Gross | 2017-06-15 |
| | |||
* | Add -compat 8.6 to _CoqProject | Jason Gross | 2017-06-15 |
| | | | | | | This allows fiat-crypto to continue working with trunk, after the merge of https://github.com/coq/coq/pull/220. We will remove this when we migrate to requiring 8.6.1 or 8.7 (neither of which is released yet). | ||
* | Add ZUtil.Z2Nat | Jason Gross | 2017-06-15 |
| | |||
* | Edwards coordinates precomputed addition formula | Andres Erbsen | 2017-06-15 |
| | |||
* | move CPS notations to Util.CPSNotations | Andres Erbsen | 2017-06-15 |
| | |||
* | ScalarMult: Z -> G -> G (closes #193) | Andres Erbsen | 2017-06-14 |
| | |||
* | Stronger invert_op tactic | Jason Gross | 2017-06-13 |
| | | | | Now it can handle ops that return (Tbase TZ) | ||
* | Add Z.peano_rect | Jason Gross | 2017-06-13 |
| | |||
* | Add Z.mul_split | Jason Gross | 2017-06-13 |
| | |||
* | WBW-montgomery: Fill in most context variables | Jason Gross | 2017-06-13 |
| | |||
* | Add CompileInterpSideConditions.v | Jason Gross | 2017-06-12 |
| | |||
* | Add snd_interpf_side_conditions_gen_Some | Jason Gross | 2017-06-12 |
| | |||
* | Add Named.InterpSideConditions | Jason Gross | 2017-06-12 |
| | |||
* | Add Z.InterpSideConditions | Jason Gross | 2017-06-12 |
| | |||
* | Add InterpSideConditions | Jason Gross | 2017-06-12 |
| | |||
* | Factor karatsuba through IdfunWithAlt, add test | Jason Gross | 2017-06-11 |
| | | | | | | | | | | | Currently the refinement is commented out. Also, we drop the proof of equality early (and probably won't use it in the first place); there's no way we can carry around such a proof in reflective-land, so we'll need to add an arithmetical-equality semi-decider to reflective-land that can prove the relevant equalities (or we'll need to leave them over as side-conditions). I expeect this may make things significantly easier on @jadephilipoom. | ||
* | Add IdfunWithAlt | Jason Gross | 2017-06-11 |
| | |||
* | Add clearbody_all | Jason Gross | 2017-06-11 |
| | |||
* | Remove temporary file | Jason Gross | 2017-06-10 |
| | | | | It's been migrated to Definitions.v and Proofs.v in the same directory | ||
* | Add initial proofs for word-by-word | Jason Gross | 2017-06-10 |
| | |||
* | Make it clear that the combined definition/proof file is a work in progress | Jason Gross | 2017-06-09 |
| | |||
* | Add pair-programmed wbw montgomery | Jason Gross | 2017-06-09 |
| | | | | Partial progress with @andres-erbsen | ||
* | add Specific/Karatsuba to CoqProject | jadep | 2017-06-07 |
| | |||
* | Add experimental loops | Jason Gross | 2017-06-02 |
| | | | | Written via pair-programming with Andres. | ||
* | Add compiler optimization for add-with-carry | Jason Gross | 2017-05-17 |
| | | | | | | | | | | | This closes #171. It's unfortunately a bit fragile, and takes a really long time (about 60s) to prove correct, because Coq is bad at deep dependent pattern matching. We enable a-normal form for the freeze test, because the rewriter only works when the arguments to adc are var or const. | ||
* | Add reflective machinery for adc, zselect | Jason Gross | 2017-05-17 |
| | |||
* | Add context_equiv and prove some Proper lemmas | Jason Gross | 2017-05-16 |
| | |||
* | Add Named.ExprInversion | Jason Gross | 2017-05-15 |
| |