aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* 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
|
* 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
|
* 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
* Improve replace_match_with_destructuring_matchGravatar Jason Gross2017-06-15
| | | | | Now it handles matches under binders, e.g., under dlet. This fixes https://github.com/mit-plv/fiat-crypto/issues/195#issuecomment-308724129.
* Fix debugging codeGravatar Jason Gross2017-06-15
| | | | It was previously trying to run constrs and erroring when we turned on debugging
* Don't force [Require Import String] for debug msgsGravatar Jason Gross2017-06-15
|
* Fix a changed case in the proof in loop.vGravatar Jason Gross2017-06-15
|
* Better for_loop induction principleGravatar Jason Gross2017-06-15
| | | | Don't require that the test be strict
* Export ZUtil.Z2Nat in ZUtilGravatar Jason Gross2017-06-15
|
* Add ZUtil.Z2NatGravatar Jason Gross2017-06-15
|
* Add for_cps_unroll1Gravatar Jason Gross2017-06-15
| | | | It unrolls a for-loop once at the head of the loop
* Add eq_loop_cps_large_nGravatar Jason Gross2017-06-15
|
* Edwards coordinates precomputed addition formulaGravatar Andres Erbsen2017-06-15
|
* move CPS notations to Util.CPSNotationsGravatar Andres Erbsen2017-06-15
|
* fix wrong number of limbs for square as wellGravatar jadep2017-06-15
|
* fix wrong number of limbsGravatar jadep2017-06-15
|
* Added reduce to karatsuba synthesisGravatar jadep2017-06-15
|
* eddsa spec fixGravatar Andres Erbsen2017-06-14
|
* typofixGravatar Andres Erbsen2017-06-14
|
* fix goldilocks karatsuba; TODO implement reduceGravatar Andres Erbsen2017-06-14
|
* Loop changes, ScalarMultBase_correct with admitsGravatar Andres Erbsen2017-06-14
|
* loops WIPGravatar Andres Erbsen2017-06-14
|
* ScalarMult: Z -> G -> G (closes #193)Gravatar Andres Erbsen2017-06-14
|
* Add constant-pushing IdWithAlt optimizationGravatar Jason Gross2017-06-14
|
* Rework and speed up arithmetic simplifier proofsGravatar Jason Gross2017-06-14
| | | | | | | | | | | | | | | | | | | | | Induction is so much faster than brute force. After | File Name | Before || Change -------------------------------------------------------------------------------- 6m15.02s | Total | 7m14.18s || -0m59.15s -------------------------------------------------------------------------------- 0m11.62s | Compilers/Z/ArithmeticSimplifierWf | 0m42.97s || -0m31.35s 0m06.52s | Compilers/Z/ArithmeticSimplifierInterp | 0m34.28s || -0m27.76s 2m47.55s | Specific/IntegrationTestLadderstep | 2m48.14s || -0m00.58s 1m09.50s | Specific/IntegrationTestKaratsubaMul | 1m08.86s || +0m00.64s 1m03.53s | Specific/IntegrationTestLadderstep130 | 1m04.05s || -0m00.51s 0m16.39s | Specific/IntegrationTestFreeze | 0m16.29s || +0m00.10s 0m13.60s | Specific/IntegrationTestMul | 0m13.60s || +0m00.00s 0m11.58s | Specific/IntegrationTestSub | 0m11.36s || +0m00.22s 0m09.79s | Specific/IntegrationTestSquare | 0m09.71s || +0m00.07s 0m03.64s | Compilers/Z/Bounds/Pipeline/Definition | 0m03.54s || +0m00.10s 0m00.75s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.05s 0m00.55s | Compilers/Z/Bounds/Pipeline | 0m00.58s || -0m00.02s
* Make rewrite_eta_match_base_type_impl a bit fasterGravatar Jason Gross2017-06-13
|
* Fix a typoGravatar Jason Gross2017-06-13
|
* Add rewrite_eta_match_base_type_implGravatar Jason Gross2017-06-13
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 16:34:47 +0000