aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z
Commit message (Collapse)AuthorAge
* Add another constantGravatar Jason Gross2017-10-06
|
* Update constants filesGravatar Jason Gross2017-09-21
|
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This closes #239 After | File Name | Before || Change --------------------------------------------------------------------------------------- 10m04.12s | Total | 10m05.68s || -0m01.55s --------------------------------------------------------------------------------------- 2m45.12s | Specific/X25519/C64/ladderstep | 2m48.45s || -0m03.32s 1m06.06s | Specific/IntegrationTestLadderstep130 | 1m04.76s || +0m01.29s 2m03.02s | Specific/NISTP256/AMD64/femul | 2m02.29s || +0m00.72s 1m20.35s | Specific/IntegrationTestKaratsubaMul | 1m20.10s || +0m00.25s 0m25.29s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.17s || +0m00.11s 0m16.66s | Specific/IntegrationTestFreeze | 0m16.18s || +0m00.48s 0m14.81s | Specific/NISTP256/AMD64/feadd | 0m15.09s || -0m00.27s 0m14.58s | Specific/NISTP256/AMD64/fesub | 0m14.48s || +0m00.09s 0m13.23s | Specific/X25519/C64/femul | 0m13.54s || -0m00.30s 0m12.00s | Specific/NISTP256/AMD64/feopp | 0m12.07s || -0m00.07s 0m11.25s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.44s || -0m00.18s 0m11.23s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.19s || +0m00.04s 0m11.06s | Specific/IntegrationTestSub | 0m11.24s || -0m00.17s 0m10.39s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m10.41s || -0m00.01s 0m09.85s | Specific/X25519/C64/fesquare | 0m09.75s || +0m00.09s 0m09.19s | Specific/NISTP256/AMD64/fenz | 0m09.04s || +0m00.15s 0m08.76s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.11s || -0m00.34s 0m00.69s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.80s || -0m00.11s 0m00.59s | Compilers/Z/Bounds/Pipeline | 0m00.57s || +0m00.02s
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
|
* Fix a mis-aligned comment marker in CNotations scriptGravatar Jason Gross2017-07-03
|
* change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`Gravatar Jason Gross2017-06-29
| | | | This closes #228
* Fix comment-in-string issuesGravatar Jason Gross2017-06-29
|
* More C Notations for uin8_t-valued addcarryxGravatar Jason Gross2017-06-29
|
* Add nonzero synthesisGravatar Jason Gross2017-06-26
|
* Allow disabling adc-fusionGravatar Jason Gross2017-06-25
|
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-25
| | | | Actually this time
* Revert "Convert adc to sbb when doing [0 - x]"Gravatar Jason Gross2017-06-25
| | | | | | This reverts commit ecff47dbc867261b81c6e268eca99e5b5ab28805. It was wrong
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-24
|
* Propogate neg through constant multiplicationGravatar Jason Gross2017-06-24
|
* Add notation for logical orGravatar Jason Gross2017-06-22
|
* Work around bug #5615 (constr not being updated)Gravatar Jason Gross2017-06-22
| | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5615, Ltac should be able to bind references and not just names, in which names are slippery, slippery objects.
* Also key adc->sbb on the carry-bit being negativeGravatar Jason Gross2017-06-20
| | | | This is needed when we're subtracting 0 >.>
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
|
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
|
* Add more Z-notationsGravatar Jason Gross2017-06-20
|
* Add another fusion to adc-fusionGravatar Jason Gross2017-06-20
| | | | | | | Might have something to do with #213. Also, RewriteAddToAdcInterp is now a bit more stable under changes to the rewriting strategy (the parts are now more separate).
* Use solve_wf_side_condition to synch the depth of auto with wfGravatar Jason Gross2017-06-20
|
* Add more constant notationsGravatar Jason Gross2017-06-20
|
* Add more constantsGravatar Jason Gross2017-06-18
|
* Better simplification of mulsplitGravatar Jason Gross2017-06-18
|
* Fix typo in formatGravatar Jason Gross2017-06-18
|
* Add fake notation for addcarryx_u128 and similarGravatar Jason Gross2017-06-18
|
* Add some notations for mulxGravatar Jason Gross2017-06-18
|
* Better test for simplifierGravatar Jason Gross2017-06-18
| | | | This one catches more things
* Stronger simplification of adc too add when we can prove the carry is 0Gravatar Jason Gross2017-06-18
|
* Add cnotations for addcarryx with uint8_tGravatar Jason Gross2017-06-18
|
* Add convenience for supporting uint8Gravatar Jason Gross2017-06-18
|
* Add notationsGravatar Jason Gross2017-06-18
|
* Adding more (possibly unneeded) simplificationGravatar Jason Gross2017-06-18
|
* Try more simplificationGravatar Jason Gross2017-06-17
|
* Drop the 0-carry bit before bounds analysisGravatar Jason Gross2017-06-17
|
* Be a bit more forceful in eliminating zeros in arith simplGravatar Jason Gross2017-06-17
|
* More arithmetic simplification for adc, mulGravatar Jason Gross2017-06-17
|
* Add more simplification to pipelineGravatar Jason Gross2017-06-17
| | | | This seemes to be making it slower though....
* Add linearization to inline pairs in post-bounds pipelineGravatar Jason Gross2017-06-17
|
* Add extra simplification to simplifier for adcGravatar 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
* Add some more display constantsGravatar Jason Gross2017-06-17
|
* Add bool into P256Gravatar Jason Gross2017-06-17
|
* Remove fails; if we fail too strongly, we miss debugging informationGravatar 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
|
* 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.
* 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/.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 04:14:46 +0000