aboutsummaryrefslogtreecommitdiff
path: root/src/Compilers/Z
Commit message (Collapse)AuthorAge
...
* Add more constant notationsGravatar Jason Gross2017-11-02
|
* Add more constant notationsGravatar Jason Gross2017-11-02
|
* Add more constant notationsGravatar Jason Gross2017-11-01
|
* Add more constant notationsGravatar Jason Gross2017-11-01
|
* Add more constant notationsGravatar Jason Gross2017-11-01
|
* Add more constant notationsGravatar Jason Gross2017-10-31
|
* Add more constant notationsGravatar Jason Gross2017-10-29
|
* Add InlineConstAndOpByRewriteGravatar Jason Gross2017-10-23
|
* Add inline_const_and_op{f,} specializationsGravatar Jason Gross2017-10-22
|
* Add Z.InlineConstAndOp*Gravatar Jason Gross2017-10-20
|
* Add more constant notationsGravatar Jason Gross2017-10-18
|
* Extract rexpr_sig from the recordGravatar Jason Gross2017-10-18
| | | | | | In the full synthesis, I expect that we will first reify the various Z operations, and then manually compose them with carry, and then after that run the pipeline.
* Extract evars from reflective pipelineGravatar Jason Gross2017-10-18
| | | | | They should not depend on v', and I want to be able to package them separately for the full synthesis pipeline.
* Package reflective pipeline side-conditions into a recordGravatar Jason Gross2017-10-18
|
* Add more notation constantsGravatar Jason Gross2017-10-18
|
* Make use of faster interp rewritingGravatar Jason Gross2017-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change --------------------------------------------------------------------------------------- 10m34.32s | Total | 11m10.14s || -0m35.81s --------------------------------------------------------------------------------------- 0m04.75s | Compilers/Z/Bounds/Pipeline/Definition | 0m41.89s || -0m37.14s 1m24.64s | Specific/IntegrationTestKaratsubaMul | 1m20.20s || +0m04.43s 1m59.10s | Specific/X25519/C64/ladderstep | 2m00.27s || -0m01.17s 1m14.55s | Specific/IntegrationTestLadderstep130 | 1m13.12s || +0m01.42s 0m49.89s | Specific/X25519/C32/femul | 0m51.34s || -0m01.45s 0m26.72s | Specific/X25519/C32/fesquare | 0m27.79s || -0m01.07s 1m51.04s | Specific/NISTP256/AMD64/femul | 1m50.92s || +0m00.11s 0m25.48s | Specific/IntegrationTestMontgomeryP256_128 | 0m24.72s || +0m00.76s 0m18.54s | Specific/NISTP256/AMD64/fesub | 0m18.60s || -0m00.06s 0m15.57s | Specific/NISTP256/AMD64/feadd | 0m15.78s || -0m00.20s 0m14.93s | Specific/NISTP256/AMD64/feopp | 0m15.09s || -0m00.16s 0m12.13s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m12.34s || -0m00.20s 0m11.78s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m12.35s || -0m00.57s 0m11.06s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.24s || -0m00.17s 0m10.16s | Specific/X25519/C64/femul | 0m10.18s || -0m00.01s 0m09.78s | Specific/NISTP256/AMD64/fenz | 0m10.10s || -0m00.32s 0m09.06s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.26s || -0m00.19s 0m08.63s | Specific/IntegrationTestSub | 0m08.32s || +0m00.31s 0m07.84s | Specific/IntegrationTestFreeze | 0m07.87s || -0m00.03s 0m07.27s | Specific/X25519/C64/fesquare | 0m07.25s || +0m00.01s 0m00.80s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.81s || -0m00.01s 0m00.61s | Compilers/Z/Bounds/Pipeline | 0m00.70s || -0m00.08s
* Turn on parenthetization in C outputGravatar Jason Gross2017-10-17
|
* Unify notation printing to allow changing it all at onceGravatar Jason Gross2017-10-17
|
* Add support for parenthesizing all CNotations expressionsGravatar Jason Gross2017-10-16
|
* Add more constantsGravatar Jason Gross2017-10-16
|
* Add some more power-of-two notationsGravatar Jason Gross2017-10-16
|
* Add more notationsGravatar Jason Gross2017-10-16
|
* Add some constants from montgomeryGravatar Jason Gross2017-10-15
|
* Add more constant notations from solinas primesGravatar Jason Gross2017-10-15
|
* Fix a spelling errorGravatar Jason Gross2017-10-13
|
* Factor out truncation_boundsGravatar Jason Gross2017-10-13
| | | | This makes it easier to extend the bounds analysis framework.
* Add comment to Compilers/Z/Bounds/Interpretation.vGravatar Jason Gross2017-10-13
| | | | | Hopefully this will help with extending the framework. Also remove [t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
* Add reflective compose, notation for Z.Syntax.{Expr,Interp}Gravatar Jason Gross2017-10-12
|
* 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
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:41:10 +0000