aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* 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
* 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 | ∞
* 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)
| * WIP: expand valid_ident and prove of_prefancy_correct using itGravatar jadep2019-01-03
| |
| * WIP : made everything more concrete and proved of_Expr. Still to do for ↵Gravatar jadep2019-01-03
| | | | | | | | of_Expr : expand valid_ident
| * WIPGravatar jadep2019-01-03
| |
| * WIPGravatar jadep2019-01-03
| |
| * WIPGravatar jadep2019-01-03
| |
| * WIPGravatar jadep2019-01-03
|/
* Prove that convert_bases partitionsGravatar Jason Gross2019-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unfortunately, the proof is rather slow :-( After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 22m46.26s | Total | 22m03.36s || +0m42.90s | +3.24% -------------------------------------------------------------------------------------------------------------------- 1m57.06s | Experiments/NewPipeline/Arithmetic.vo | 1m15.08s || +0m41.98s | +55.91% 0m42.39s | p521_32.c | 0m39.92s || +0m02.46s | +6.18% 0m35.40s | p521_64.c | 0m33.02s || +0m02.37s | +7.20% 3m15.80s | p384_32.c | 3m17.10s || -0m01.29s | -0.65% 6m19.46s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m18.91s || +0m00.54s | +0.14% 4m34.80s | Experiments/NewPipeline/Toplevel1.vo | 4m35.56s || -0m00.75s | -0.27% 1m36.64s | Experiments/NewPipeline/Toplevel2.vo | 1m36.64s || +0m00.00s | +0.00% 0m43.22s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m44.18s || -0m00.96s | -2.17% 0m29.24s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m29.83s || -0m00.58s | -1.97% 0m22.83s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m22.87s || -0m00.04s | -0.17% 0m16.11s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m16.73s || -0m00.62s | -3.70% 0m14.24s | p256_32.c | 0m13.75s || +0m00.49s | +3.56% 0m14.22s | secp256k1_32.c | 0m14.19s || +0m00.03s | +0.21% 0m11.01s | p384_64.c | 0m10.50s || +0m00.50s | +4.85% 0m09.71s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m09.86s || -0m00.14s | -1.52% 0m09.69s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m10.35s || -0m00.66s | -6.37% 0m07.41s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m07.74s || -0m00.33s | -4.26% 0m06.65s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m06.52s || +0m00.13s | +1.99% 0m06.50s | p224_32.c | 0m06.47s || +0m00.03s | +0.46% 0m06.24s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m06.38s || -0m00.13s | -2.19% 0m05.10s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.97s || +0m00.12s | +2.61% 0m04.82s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m05.04s || -0m00.21s | -4.36% 0m03.95s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m04.02s || -0m00.06s | -1.74% 0m02.31s | curve25519_32.c | 0m02.24s || +0m00.06s | +3.12% 0m02.03s | p224_64.c | 0m01.92s || +0m00.10s | +5.72% 0m01.91s | secp256k1_64.c | 0m02.00s || -0m00.09s | -4.50% 0m01.90s | p256_64.c | 0m01.86s || +0m00.03s | +2.15% 0m01.54s | curve25519_64.c | 0m01.61s || -0m00.07s | -4.34% 0m01.51s | Experiments/NewPipeline/CLI.vo | 0m01.49s || +0m00.02s | +1.34% 0m01.29s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.29s || +0m00.00s | +0.00% 0m01.28s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.32s || -0m00.04s | -3.03%
* Do not rely on `Refine Instance Mode`Gravatar Maxime Dénès2019-01-02
| | | | | This option is soon going to be turned off by default. See https://github.com/coq/coq/pull/9270
* Remove WBW Mont lemmas from push_evalGravatar Jason Gross2018-12-26
| | | | autorewrite is slow and not customiziable enough.
* Add eval_* lemmas for WBW Mont Arith operationsGravatar Jason Gross2018-12-26
| | | | | This allows us to push the evaluations with just `autorewrite with push_eval`
* Move le_{add,sub}_1_* to ZUtil.LeGravatar Jason Gross2018-12-25
|
* from_montgomery{_ => }mod, for consistency with other namingGravatar Jason Gross2018-12-24
|
* Add correctness in arithmetic for mulx, addcarryx, subborrowxGravatar Jason Gross2018-12-21
|
* Add has_body tacticGravatar Jason Gross2018-12-21
|
* Add eval_freeze_to_bytesmod to push_evalGravatar Jason Gross2018-12-21
|
* Add length_encode_no_reduce to distr_lengthGravatar Jason Gross2018-12-21
|
* Add `Proof using` directives in ArithmeticGravatar Jason Gross2018-12-21
|
* Fix a few minor things in ArithmeticGravatar Jason Gross2018-12-21
|
* remove unneeded lemma and do some micro-performance-optimization at one ↵Gravatar jadep2018-12-21
| | | | sticky point
* remove proof duplicationGravatar jadep2018-12-21
|
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
|
* prove [small_sub_then_maybe_add]Gravatar jadep2018-12-21
|
* prove [eval_sub_then_maybe_add]Gravatar jadep2018-12-21
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 05:51:35 +0000