aboutsummaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
* Define String.replaceGravatar Jason Gross2019-01-18
|
* Be stricter about rejecting command line argumentsGravatar Jason Gross2019-01-18
| | | | | | | | | | | | | We no longer accept `1,1` as a valid bitwidth. This closes #488. It does not quite fix the issue as stated, but it resolves the underlying confusion that generated it (the difference between passing `1,1` as a `c` vs passing `1,1` as a bitwidth). It still might be nice to someday emit warnings as suggested in the bug report. I've also factored out a bit of code to make it easier to report parse failures, by folding over a list of parses.
* Don't allow r[0~>0] ranges in fancy synthesisGravatar Jason Gross2019-01-17
| | | | | | | | This disables the optimization that was recently introduced for replacing things known to be 0 from the bounds analyzer with the constant 0. It was messing up some of the other fancy synthesis stages. Fixes #498
* Remove ? notationGravatar Jason Gross2019-01-17
| | | | It was colliding with the ?[a] notation for fresh evars
* remove reference to Toplevel2 in MakefileGravatar jadep2019-01-17
|
* Move print statements to Barrett and Montgomery filesGravatar jadep2019-01-17
|
* prune dependencies from Barrett256 and Montgomery256Gravatar jadep2019-01-17
|
* Prune dependencies of Prod.v and fix upGravatar jadep2019-01-17
|
* Rename Translation.vGravatar jadep2019-01-17
|
* Prune Translation.v deps and move tactics from other files [WIP]Gravatar jadep2019-01-17
|
* clean up and prune deps of Spec.vGravatar jadep2019-01-17
|
* Fix up MontgomeryGravatar jadep2019-01-17
|
* Make Montgomery take arguments separately instead of as a pairGravatar jadep2019-01-17
|
* separate toplevel2 into several files; fix up final barrett proofGravatar jadep2019-01-17
|
* Constant-propogate 0+x and x+0 after boundsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43% -------------------------------------------------------------------------------------------- 4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88% 3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68% 2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22% 1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27% 1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01% 1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77% 0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34% 0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63% 0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25% 0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73% 0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80% 0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28% 0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28% 0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45% 0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75% 0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35% 0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77% 0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37% 0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09% 0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12% 0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73% 0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63% 0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18% 0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32% 0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93% 0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40% 0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73% 0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88% 0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16% 0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35% 0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58% 0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78% 0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22% 0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00%
* Add a rewrite rule to collapse constant castsGravatar Jason Gross2019-01-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | If, e.g., we know from bounds analysis that the result of an operation fits in the range r[0~>0], we now just replace it with the literal constant. Fixes #493 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05% -------------------------------------------------------------------------------------------- 4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23% 3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11% 2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28% 1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42% 1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31% 1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20% 0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06% 0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38% 0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38% 0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39% 0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65% 0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49% 0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11% 0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75% 0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35% 0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94% 0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00% 0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09% 0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08% 0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39% 0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42% 0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59% 0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50% 0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33% 0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75% 0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57% 0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40% 0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49% 0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45% 0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33% 0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74% 0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73% 0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00% 0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14% 0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43%
* Add some more basic ZRange lemmasGravatar Jason Gross2019-01-15
|
* Move StringMap into Strings/Gravatar Jason Gross2019-01-15
|
* Add StringMapGravatar Jason Gross2019-01-15
|
* Add String_as_OTGravatar Jason Gross2019-01-15
| | | | | Copied verbatim from https://github.com/mit-plv/fiat/blob/master/src/Common/String_as_OT.v
* Ensure that we only left-shift on unsigned valuesGravatar Jason Gross2019-01-15
| | | | As per https://github.com/mit-plv/fiat-crypto/pull/490/files#r247737121
* Fix computation of INTX_MINGravatar Jason Gross2019-01-15
| | | | The minimum is -2^(bitwidth-1), not -2^bitwidth. Oops.
* Don't cast signed to unsigned before shiftingGravatar Jason Gross2019-01-15
| | | | | | | | | | | Unfortunately, signed->unsigned casts do not commute with shifts. We take care to only extend the range when it needs extending, now. This was previously causing issues with subborrow. We should really get proofs about casts in C semantics at some point soon. Fixes #489
* Delete p484_32.cGravatar Jason Gross2019-01-14
| | | It's too slow to generate each time
* Comment out a slow .c fileGravatar Jason Gross2019-01-14
|
* We don't need to encode c with taps in WBW montgomeryGravatar Jason Gross2019-01-14
|
* Autocompute s and c in WBW MontgomeryGravatar Jason Gross2019-01-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This allows us to support primes which are not a power of 2. We also add p484 as an example. To support this, I added a small parser combinator library which can parse arithmetic expressions involving `()^*/+-` and decimal digits. Closes #486 Closes #342 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 22m14.42s | Total | 12m14.76s || +9m59.65s | +81.61% -------------------------------------------------------------------------------------------- 9m41.91s | p484_32.c | N/A || +9m41.90s | ∞ 0m11.51s | p484_64.c | N/A || +0m11.50s | ∞ 3m16.22s | p384_32.c | 3m12.02s || +0m04.19s | +2.18% 4m12.18s | PushButtonSynthesis.vo | 4m10.16s || +0m02.02s | +0.80% 0m45.08s | ExtractionHaskell/word_by_word_montgomery | 0m45.24s || -0m00.16s | -0.35% 0m38.14s | p521_32.c | 0m38.12s || +0m00.02s | +0.05% 0m31.80s | p521_64.c | 0m31.78s || +0m00.01s | +0.06% 0m31.09s | ExtractionHaskell/unsaturated_solinas | 0m30.77s || +0m00.32s | +1.03% 0m24.18s | ExtractionHaskell/saturated_solinas | 0m24.21s || -0m00.03s | -0.12% 0m17.38s | ExtractionOCaml/word_by_word_montgomery | 0m17.35s || +0m00.02s | +0.17% 0m13.39s | secp256k1_32.c | 0m13.59s || -0m00.19s | -1.47% 0m13.14s | p256_32.c | 0m13.04s || +0m00.10s | +0.76% 0m10.58s | ExtractionOCaml/unsaturated_solinas | 0m10.73s || -0m00.15s | -1.39% 0m10.23s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.34s || -0m00.10s | -1.06% 0m07.88s | ExtractionOCaml/saturated_solinas | 0m07.94s || -0m00.06s | -0.75% 0m06.78s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.86s || -0m00.08s | -1.16% 0m06.28s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || -0m00.13s | -2.18% 0m06.00s | p224_32.c | 0m05.97s || +0m00.03s | +0.50% 0m05.50s | p384_64.c | 0m05.35s || +0m00.15s | +2.80% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.08s || +0m00.20s | +3.93% 0m05.10s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.98s || +0m00.11s | +2.40% 0m04.12s | ExtractionHaskell/saturated_solinas.hs | 0m04.15s || -0m00.03s | -0.72% 0m02.14s | curve25519_32.c | 0m02.28s || -0m00.13s | -6.14% 0m01.44s | CLI.vo | 0m01.42s || +0m00.02s | +1.40% 0m01.44s | curve25519_64.c | 0m01.57s || -0m00.13s | -8.28% 0m01.14s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.02s | +2.70% 0m01.12s | p256_64.c | 0m00.98s || +0m00.14s | +14.28% 0m01.11s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.05s | -5.12% 0m01.03s | secp256k1_64.c | 0m01.15s || -0m00.11s | -10.43% 0m01.02s | p224_64.c | 0m00.99s || +0m00.03s | +3.03% 0m00.21s | Util/Strings/ParseArithmetic.vo | N/A || +0m00.21s | ∞
* Move ALL_C_FILES above c-filesGravatar Jason Gross2019-01-13
| | | | Or else it doesn't build anything at all
* Makefile: remove *CURVES_PROOFS*Gravatar Andres Erbsen2019-01-11
|
* remove redundant travis CI stagesGravatar Andres Erbsen2019-01-10
|
* link to papers in readmeGravatar Andres Erbsen2019-01-10
|
* fix typo in README.mdGravatar Andres Erbsen2019-01-10
|
* remove old pipelineGravatar Andres Erbsen2019-01-09
|
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
|
* Fix for 8.7Gravatar Jason Gross2019-01-07
| | | | `2: {` is not valid in 8.7
* Merge remote-tracking branch 'origin/fix_fancy4'Gravatar Andres Erbsen2019-01-07
|\
* | Update README.mdGravatar Jason Gross2019-01-05
| |
* | prove admitGravatar Andres Erbsen2019-01-05
| |
* | build on Coq masterGravatar Andres Erbsen2019-01-05
| |
* | new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP WIP Try to remove assumption that s = weight n After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 14m03.04s | Total | 20m54.46s || -6m51.41s | -32.79% -------------------------------------------------------------------------------------------------------------------- 0m01.18s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.83s || -6m17.64s | -99.68% N/A | Experiments/NewPipeline/Toplevel1.vo | 4m36.32s || -4m36.31s | -100.00% 4m17.06s | Experiments/NewPipeline/PushButtonSynthesis.vo | N/A || +4m17.06s | ∞ 1m28.64s | Experiments/NewPipeline/Toplevel2.vo | 1m38.21s || -0m09.57s | -9.74% 3m10.57s | p384_32.c | 3m18.05s || -0m07.48s | -3.77% 0m06.36s | Experiments/NewPipeline/BoundsPipeline.vo | N/A || +0m06.36s | ∞ 0m06.16s | Experiments/NewPipeline/COperationSpecifications.vo | N/A || +0m06.16s | ∞ 0m05.66s | p384_64.c | 0m10.80s || -0m05.14s | -47.59% 0m38.24s | p521_32.c | 0m41.31s || -0m03.07s | -7.43% 0m31.64s | p521_64.c | 0m33.94s || -0m02.29s | -6.77% 0m45.06s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m43.83s || +0m01.23s | +2.80% 0m30.57s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.56s || +0m01.01s | +3.41% 0m13.52s | secp256k1_32.c | 0m14.60s || -0m01.08s | -7.39% 0m01.00s | p256_64.c | 0m02.03s || -0m01.02s | -50.73% 0m24.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m23.62s || +0m00.57s | +2.41% 0m16.66s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.40s || +0m00.26s | +1.58% 0m13.34s | p256_32.c | 0m14.00s || -0m00.66s | -4.71% 0m10.40s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.08s || +0m00.32s | +3.17% 0m10.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.81s || +0m00.29s | +3.05% 0m07.84s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.66s || +0m00.17s | +2.34% 0m07.09s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.62s || +0m00.46s | +7.09% 0m06.89s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.42s || +0m00.46s | +7.32% 0m06.26s | p224_32.c | 0m06.54s || -0m00.28s | -4.28% 0m05.24s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.99s || +0m00.25s | +5.01% 0m04.96s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.94s || +0m00.01s | +0.40% 0m04.19s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.09s | +2.19% 0m02.13s | curve25519_32.c | 0m02.30s || -0m00.16s | -7.39% 0m01.46s | curve25519_64.c | 0m01.65s || -0m00.18s | -11.51% 0m01.44s | Experiments/NewPipeline/CLI.vo | 0m01.37s || +0m00.06s | +5.10% 0m01.31s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.30s || +0m00.01s | +0.76% 0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.25s || +0m00.01s | +0.80% 0m01.15s | secp256k1_64.c | 0m01.91s || -0m00.76s | -39.79% 0m01.03s | p224_64.c | 0m02.02s || -0m00.99s | -49.00% 0m00.44s | Experiments/NewPipeline/PushButtonSynthesis/ReificationCache.vo | N/A || +0m00.44s | ∞
| * Update fancy rewriter output with new compilation outputGravatar Jason Gross2019-01-03
| |
| * Finish proving fancy rewrite rulesGravatar Jason Gross2019-01-03
| |
| * Fix bounds checking on shiftGravatar Jason Gross2019-01-03
| |
| * comment out broken code so things buildGravatar jadep2019-01-03
| |
| * try to fix fancy rewrite rules; current output is incorrectGravatar jadep2019-01-03
| |
| * WIPGravatar jadep2019-01-03
| |
| * remove dead codeGravatar jadep2019-01-03
| |
| * remove whitespace, print statements, and some dead tacticsGravatar jadep2019-01-03
| |
| * fixed up some of the fancy rewrite rulesGravatar jadep2019-01-03
| |
| * WIP: prove that barrett_red256 is a valid expression modulo some issues with ↵Gravatar jadep2019-01-03
| | | | | | | | rewrite rules (too-tight bound on RSHI and ADDC (0,x,y) not being converted to ADD (x,y)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 10:54:58 +0000