aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
| | | | This seemes to be making it slower though....
* make displayGravatar Jason Gross2017-06-17
|
* Make use of non-uniform tuple-based addGravatar Jason Gross2017-06-17
| | | | Maybe it'll result in better output code with fewer zeros?
* make displayGravatar Jason Gross2017-06-17
|
* Enable profiling in integration test mont 256Gravatar Jason Gross2017-06-17
|
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
|
* make displayGravatar Jason Gross2017-06-17
|
* Add extra simplification to simplifier for adcGravatar Jason Gross2017-06-17
|
* Make displayGravatar Jason Gross2017-06-17
|
* Add more constantsGravatar Jason Gross2017-06-17
|
* Unfold Z.mul_split_at_bitwidth for reificationGravatar Jason Gross2017-06-17
| | | | Also reimplement it with a shift and a mask
* Don't make curves proofs on travis (hopefully fast enough build)Gravatar Jason Gross2017-06-17
|
* Make displayGravatar Jason Gross2017-06-17
|
* Add some more display constantsGravatar Jason Gross2017-06-17
|
* Add bool into P256Gravatar Jason Gross2017-06-17
|
* make displayGravatar Jason Gross2017-06-17
| | | | Need to fix the display of mulsplit and addwithcarry
* Finish MontgomeryP256 (less conditional subtract)Gravatar Jason Gross2017-06-17
|
* Remove fails; if we fail too strongly, we miss debugging informationGravatar Jason Gross2017-06-17
|
* Try to fail a bit faster in bad reificationGravatar Jason Gross2017-06-17
|
* Add back failure at level 100Gravatar Jason Gross2017-06-17
| | | | We still need to idtac, because tc resolution eats messages from fail at any level
* Better error messages in reificationGravatar Jason Gross2017-06-17
|
* Add initial IntegrationTestMontgomeryP256.vGravatar Jason Gross2017-06-17
|
* Better reification tactic debuggingGravatar Jason Gross2017-06-17
|
* Fix a typoGravatar Jason Gross2017-06-17
|
* Define m in p256Gravatar Jason Gross2017-06-17
|
* Fix spellingGravatar Jason Gross2017-06-17
|
* fix WWMM partial evaluationGravatar Andres Erbsen2017-06-16
|
* Unfold more things in src/Specific/MontgomreyP256Gravatar Jason Gross2017-06-16
| | | | | It seems that something gets unfolded which should not get unfolded. But we no longer block on lists.
* finish tuple-ifying Montgomery APIGravatar jadep2017-06-16
|
* Switch to using tuples for word-by-word montgomeryGravatar Jason Gross2017-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 buildGravatar Jason Gross2017-06-16
|
* Revert PR #203Gravatar Jason Gross2017-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.
* update ocq2C sed scriptGravatar Andres Erbsen2017-06-16
|
* make displayGravatar Jason Gross2017-06-16
| | | | | Note that the sed rules for addcarryx and sbb need to change, to use arrays.
* Make use of CArrayNotationsGravatar Jason Gross2017-06-16
|
* Fix CArrayNotationsGravatar Jason Gross2017-06-16
| | | | | | Work around [bug #5608](https://coq.inria.fr/bugs/show_bug.cgi?id=5608), Anomaly: No printing rule found for _ _ [1] = { _ } ; return ( _ , _ , .. , _ ). Please report at http://coq.inria.fr/bugs/.
* Revert "Revert "Add CArrayNotations""Gravatar Jason Gross2017-06-16
| | | | This reverts commit 29ad742d76dca90ec9c8d03ab6f4359ccf053a90.
* montgomery p256 in Specific WIPGravatar Andres Erbsen2017-06-16
|
* make displayGravatar Jason Gross2017-06-15
|
* Fix notation-overriden warning issuesGravatar Jason Gross2017-06-15
| | | | This change is necessary because we've added -compat 8.6.
* Revert "Add CArrayNotations"Gravatar Jason Gross2017-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)Gravatar Jason Gross2017-06-15
| | | This closes #182.
* ed448 mul: use two carry chains to fix bounds (still silly otherwise)Gravatar Andres Erbsen2017-06-15
|
* Add CArrayNotationsGravatar Jason Gross2017-06-15
|
* CPSify montgomery wbw reductionGravatar Jason Gross2017-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)Gravatar jadep2017-06-15
|
* Add -compat 8.6 to _CoqProjectGravatar Jason Gross2017-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).
* Show the bounds going wrong in karatsubaGravatar Jason Gross2017-06-15
|
* Display Z operations with ℤ attachedGravatar Jason Gross2017-06-15
| | | | This is the lighter-weight solution to #197.
* Eliminate well-bounded IdWithAlt from final outputGravatar Jason Gross2017-06-15
| | | | This closes #195
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 20:25:54 +0000