aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add some Proper lemmas to ListUtilGravatar Jason Gross2019-03-07
|
* Update .out filesGravatar Jason Gross2019-03-07
|
* Reify most rewrite rulesGravatar Jason Gross2019-03-07
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Currently we don't handle rules that require "concrete list of cons cells" nor rules that require "concrete nat literal to do recursion on"; both of these require special treatment, to be implemented in an upcoming commit. The reifier is kind-of slow, alas. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m52.72s | Total | 21m20.90s || +0m31.82s | +2.48% -------------------------------------------------------------------------------------------- 1m12.22s | Rewriter.vo | 0m47.38s || +0m24.83s | +52.42% 3m14.35s | p384_32.c | 3m19.59s || -0m05.24s | -2.62% 1m45.12s | RewriterRulesGood.vo | 1m39.44s || +0m05.68s | +5.71% 0m40.82s | ExtractionHaskell/unsaturated_solinas | 0m37.58s || +0m03.24s | +8.62% 1m35.04s | RewriterRulesInterpGood.vo | 1m32.48s || +0m02.56s | +2.76% 0m59.49s | ExtractionHaskell/word_by_word_montgomery | 0m56.71s || +0m02.78s | +4.90% 1m45.10s | Fancy/Barrett256.vo | 1m47.00s || -0m01.90s | -1.77% 0m40.21s | p521_64.c | 0m38.97s || +0m01.24s | +3.18% 0m24.42s | SlowPrimeSynthesisExamples.vo | 0m25.67s || -0m01.25s | -4.86% 0m20.48s | secp256k1_32.c | 0m19.27s || +0m01.21s | +6.27% 1m47.10s | RewriterWf2.vo | 1m47.22s || -0m00.12s | -0.11% 0m47.85s | p521_32.c | 0m47.47s || +0m00.38s | +0.80% 0m45.66s | RewriterInterpProofs1.vo | 0m45.74s || -0m00.08s | -0.17% 0m37.18s | Fancy/Montgomery256.vo | 0m37.14s || +0m00.03s | +0.10% 0m36.26s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.14s || +0m00.11s | +0.33% 0m28.38s | ExtractionHaskell/saturated_solinas | 0m28.04s || +0m00.33s | +1.21% 0m26.80s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.83s || -0m00.02s | -0.11% 0m24.00s | RewriterWf1.vo | 0m23.96s || +0m00.03s | +0.16% 0m19.82s | ExtractionOCaml/word_by_word_montgomery | 0m20.34s || -0m00.51s | -2.55% 0m19.65s | p256_32.c | 0m19.24s || +0m00.41s | +2.13% 0m18.54s | p448_solinas_64.c | 0m19.24s || -0m00.69s | -3.63% 0m16.18s | p434_64.c | 0m16.49s || -0m00.30s | -1.87% 0m13.67s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.47s || -0m00.80s | -5.52% 0m13.22s | ExtractionOCaml/unsaturated_solinas | 0m13.72s || -0m00.50s | -3.64% 0m09.91s | p224_32.c | 0m09.89s || +0m00.01s | +0.20% 0m09.85s | ExtractionOCaml/saturated_solinas | 0m09.83s || +0m00.01s | +0.20% 0m08.66s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.86s || +0m00.79s | +10.17% 0m08.36s | p384_64.c | 0m08.46s || -0m00.10s | -1.18% 0m07.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m08.29s || -0m00.56s | -6.87% 0m06.66s | BoundsPipeline.vo | 0m06.73s || -0m00.07s | -1.04% 0m06.50s | ExtractionHaskell/unsaturated_solinas.hs | 0m06.56s || -0m00.05s | -0.91% 0m06.22s | ExtractionOCaml/saturated_solinas.ml | 0m05.69s || +0m00.52s | +9.31% 0m05.50s | ExtractionHaskell/saturated_solinas.hs | 0m05.88s || -0m00.37s | -6.46% 0m03.51s | PushButtonSynthesis/Primitives.vo | 0m03.48s || +0m00.02s | +0.86% 0m03.34s | PushButtonSynthesis/SmallExamples.vo | 0m03.32s || +0m00.02s | +0.60% 0m03.31s | curve25519_32.c | 0m03.13s || +0m00.18s | +5.75% 0m03.15s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.12s || +0m00.02s | +0.96% 0m03.11s | PushButtonSynthesis/BarrettReduction.vo | 0m03.08s || +0m00.02s | +0.97% 0m02.80s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.86s || -0m00.06s | -2.09% 0m02.13s | curve25519_64.c | 0m02.02s || +0m00.10s | +5.44% 0m01.58s | p256_64.c | 0m01.66s || -0m00.07s | -4.81% 0m01.53s | p224_64.c | 0m01.60s || -0m00.07s | -4.37% 0m01.49s | secp256k1_64.c | 0m01.72s || -0m00.23s | -13.37% 0m01.34s | CLI.vo | 0m01.23s || +0m00.11s | +8.94% 0m01.16s | RewriterProofs.vo | 0m01.10s || +0m00.05s | +5.45% 0m01.16s | StandaloneOCamlMain.vo | 0m01.13s || +0m00.03s | +2.65% 0m01.10s | CompilersTestCases.vo | 0m01.09s || +0m00.01s | +0.91% 0m01.07s | StandaloneHaskellMain.vo | 0m01.04s || +0m00.03s | +2.88%
* Fix reification of interpreted identsGravatar Jason Gross2019-03-06
|
* Add support for reifying fancy identifiersGravatar Jason Gross2019-03-06
|
* Add reserved notations for \inGravatar Jason Gross2019-03-05
|
* Allow reifying Z.cast2Gravatar Jason Gross2019-03-05
|
* Fix unfolding of pattern.base.lookup_defaultGravatar Jason Gross2019-03-05
|
* Actually fix reification of literalsGravatar Jason Gross2019-03-05
|
* Revert "Fix reification of literals"Gravatar Jason Gross2019-03-05
| | | | | | | This reverts commit 36da58eb94445de10f78c17cb01f01ef62a815b9. It doesn't work without access to var in reification of ident (also we need to produce ident, not expr)
* Fix reification of literalsGravatar Jason Gross2019-03-05
|
* Add UnderLets.flat_mapGravatar Jason Gross2019-03-05
|
* Fix another instance of reductionGravatar Jason Gross2019-03-04
|
* Fix reductionGravatar Jason Gross2019-03-04
|
* Fix an issue with a proof from the previous commitGravatar Jason Gross2019-03-04
| | | | | Also move lam_type_of_list to Rewriter (in prep for reifying rewrite rules).
* Add some things to GENERATED rewriter fileGravatar Jason Gross2019-03-04
|
* Allow reifying cast and literalsGravatar Jason Gross2019-03-04
|
* Add some minor reflect thingsGravatar Jason Gross2019-03-04
|
* Make [reflect] a typeclass and add a bunch of lemmasGravatar Jason Gross2019-03-04
|
* Update a proof to work with previous commitGravatar Jason Gross2019-02-27
|
* Add UnderLets.mapGravatar Jason Gross2019-02-27
|
* finish porting barrett and montgomery code to new glue styleGravatar jadep2019-02-21
|
* adapt barrett to new glue codeGravatar jadep2019-02-21
|
* Make Qed not take foreverGravatar jadep2019-02-21
|
* start adapting Montgomery to new glue codeGravatar jadep2019-02-21
|
* Add base.{base_,}interp_beqGravatar Jason Gross2019-02-20
| | | | These are the canonical boolean equality functions for the interpretations of the various base types. This will probably come in handy for side conditions in proofs about reifications of rewrite rules.
* Update .out filesGravatar Jason Gross2019-02-18
|
* Add support for reifying `zrange` and `option`Gravatar Jason Gross2019-02-18
| | | | This is needed to reify statements for the rewriter.
* fix cast admits in FancyGravatar jadep2019-02-15
|
* Fix missing "= true" in a tactic so [Admitted] is unneccesary.Gravatar jadep2019-02-15
| | | | Co-authored-by: Jason Gross <jgross@mit.edu>
* Add Option.{lift,map,combine}, List.Option.liftGravatar Jason Gross2019-02-11
| | | | These will be useful for extending the AST with `option` types.
* Insert casts before literals during bounds analysisGravatar Jason Gross2019-02-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Unless we explicitly say not to. The ability to explicitly say not to is required for, e.g., eta-expansion where we want to replace variable lists of known length with with cons cells indexing into the variable list, but don't want to pollute the code with casts. Uniformity in this way allows rewrite rules to not blow up exponentially (in the number of wildcards); we previously required a separate rewrite rule for each way of choosing between wildcard and literal. To preserve output of the pipeline, we add another pass that just strips the casts off of literals at the end. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 20m27.24s | Total | 22m39.70s || -2m12.46s | -9.74% -------------------------------------------------------------------------------------------- 0m44.27s | Rewriter.vo | 2m11.58s || -1m27.31s | -66.35% 1m15.23s | RewriterRulesInterpGood.vo | 1m50.28s || -0m35.04s | -31.78% 1m40.19s | RewriterRulesGood.vo | 1m58.05s || -0m17.85s | -15.12% 0m26.99s | AbstractInterpretationProofs.vo | 0m16.91s || +0m10.07s | +59.60% 3m15.98s | p384_32.c | 3m07.78s || +0m08.19s | +4.36% 0m42.52s | ExtractionHaskell/word_by_word_montgomery | 0m44.60s || -0m02.07s | -4.66% 0m28.63s | ExtractionHaskell/unsaturated_solinas | 0m31.38s || -0m02.75s | -8.76% 0m21.76s | ExtractionHaskell/saturated_solinas | 0m24.56s || -0m02.79s | -11.40% 0m09.87s | ExtractionOCaml/unsaturated_solinas | 0m11.28s || -0m01.41s | -12.50% 1m59.22s | RewriterWf2.vo | 2m00.09s || -0m00.87s | -0.72% 1m07.03s | Fancy/Montgomery256.vo | 1m07.31s || -0m00.28s | -0.41% 0m52.60s | Fancy/Barrett256.vo | 0m53.16s || -0m00.55s | -1.05% 0m48.17s | RewriterInterpProofs1.vo | 0m48.72s || -0m00.54s | -1.12% 0m40.16s | AbstractInterpretationWf.vo | 0m40.23s || -0m00.07s | -0.17% 0m38.35s | p521_32.c | 0m38.26s || +0m00.09s | +0.23% 0m31.56s | p521_64.c | 0m31.53s || +0m00.02s | +0.09% 0m24.64s | RewriterWf1.vo | 0m24.01s || +0m00.62s | +2.62% 0m23.54s | AbstractInterpretationZRangeProofs.vo | 0m23.64s || -0m00.10s | -0.42% 0m23.48s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m23.26s || +0m00.21s | +0.94% 0m20.92s | SlowPrimeSynthesisExamples.vo | 0m20.62s || +0m00.30s | +1.45% 0m19.92s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.80s || +0m00.12s | +0.60% 0m16.60s | ExtractionOCaml/word_by_word_montgomery | 0m17.56s || -0m00.95s | -5.46% 0m14.72s | p448_solinas_64.c | 0m14.66s || +0m00.06s | +0.40% 0m13.70s | secp256k1_32.c | 0m13.45s || +0m00.25s | +1.85% 0m13.68s | p256_32.c | 0m13.33s || +0m00.34s | +2.62% 0m13.28s | CStringification.vo | 0m13.26s || +0m00.01s | +0.15% 0m11.88s | p484_64.c | 0m11.74s || +0m00.14s | +1.19% 0m09.96s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.24s || -0m00.27s | -2.73% 0m07.47s | ExtractionOCaml/saturated_solinas | 0m07.93s || -0m00.46s | -5.80% 0m06.78s | BoundsPipeline.vo | 0m05.96s || +0m00.82s | +13.75% 0m06.72s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.03s || -0m00.31s | -4.40% 0m06.38s | p224_32.c | 0m06.54s || -0m00.16s | -2.44% 0m06.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.34s || -0m00.12s | -2.05% 0m05.45s | p384_64.c | 0m05.18s || +0m00.27s | +5.21% 0m04.82s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.84s || -0m00.01s | -0.41% 0m04.80s | ExtractionOCaml/saturated_solinas.ml | 0m05.07s || -0m00.27s | -5.32% 0m03.83s | ExtractionHaskell/saturated_solinas.hs | 0m04.07s || -0m00.24s | -5.89% 0m03.30s | PushButtonSynthesis/Primitives.vo | 0m03.31s || -0m00.01s | -0.30% 0m03.26s | PushButtonSynthesis/SmallExamples.vo | 0m03.24s || +0m00.01s | +0.61% 0m03.08s | PushButtonSynthesis/SaturatedSolinas.vo | 0m02.96s || +0m00.12s | +4.05% 0m02.16s | curve25519_32.c | 0m02.16s || +0m00.00s | +0.00% 0m01.57s | curve25519_64.c | 0m01.47s || +0m00.10s | +6.80% 0m01.40s | CLI.vo | 0m01.32s || +0m00.07s | +6.06% 0m01.27s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.19s || +0m00.08s | +6.72% 0m01.26s | StandaloneHaskellMain.vo | 0m01.18s || +0m00.08s | +6.77% 0m01.22s | PushButtonSynthesis/BarrettReduction.vo | 0m01.29s || -0m00.07s | -5.42% 0m01.13s | RewriterProofs.vo | 0m01.10s || +0m00.02s | +2.72% 0m01.10s | secp256k1_64.c | 0m01.01s || +0m00.09s | +8.91% 0m01.08s | StandaloneOCamlMain.vo | 0m01.13s || -0m00.04s | -4.42% 0m01.06s | p256_64.c | 0m01.02s || +0m00.04s | +3.92% 0m01.05s | AbstractInterpretation.vo | 0m01.00s || +0m00.05s | +5.00% 0m01.00s | CompilersTestCases.vo | 0m01.08s || -0m00.08s | -7.40% 0m01.00s | p224_64.c | 0m01.00s || +0m00.00s | +0.00%
* clean up and factor out cast-admit so that [Print Assumptions] is more ↵Gravatar jadep2019-02-08
| | | | fine-grained
* cleanupGravatar jadep2019-02-08
|
* remove some TODOs -- actually, the final proof does not rely on the unused ↵Gravatar jadep2019-02-08
| | | | values
* fix Montgomery proof and clean up a littleGravatar jadep2019-02-08
|
* remove 2: syntax so 8.7 buildsGravatar jadep2019-02-07
|
* Fix instruction-order admit; still neads cleanupGravatar jadep2019-02-07
|
* Use Preconditions: Postconditions:, rather than /\ and ->Gravatar Jason Gross2019-02-02
|
* More minor improvements in docstringsGravatar Jason Gross2019-02-02
|
* Rename docstring generator based on Andres' suggestionGravatar Jason Gross2019-02-02
|
* Update with davidben's and Andres' suggestionsGravatar Jason Gross2019-02-02
|
* Drop `map λ` bits in docstringsGravatar Jason Gross2019-02-02
| | | | | | | | | They are redundant with the bounds pre- and post-conditions in WBW montgomery. Also drop the fiat_p... prefix from the `from_montgomery` bits in most of the docstrings, under the assumption that shorter strings with less repetition are more readable.
* Address code review comments to improve docstringsGravatar Jason Gross2019-02-02
|
* Add autogenerated docstrings to synthesized codeGravatar Jason Gross2019-02-02
| | | | | | | | | We now stringify the correctness conditions to generate docstrings for the synthesized code. Closes #512 Time commitment: about 6 hours
* Add zrange_rect{,_Proper,_Proper_dep}Gravatar Jason Gross2019-02-02
|
* Add option_beq_heteroGravatar Jason Gross2019-02-02
|
* Remove an unused argumentGravatar Jason Gross2019-02-01
|
* Uncps unify_extractedGravatar Jason Gross2019-02-01
| | | | We never used the cps form, and this form is easier to read.
* Reduce more in mulmod and squaremodGravatar Jason Gross2019-01-26
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After some debugging with Andres, the issue seems to be that when we have multiple TAPs, the first reduction will leave some of the partial products past the end of the table, because it "folds over" the partial products table at the location of each TAP. In the worst case, if we have a TAP at 1 and a TAP at the second-highest limb, we will have to reduce as many times as there are limbs. To prevent quadratic blowup, we short-circuit the repeat_reduce calculation whenever the list of high terms is nil. We deliberately do not support primes with a TAP in the highest limb. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 17m49.68s | Total | 17m34.83s || +0m14.84s | +1.40% ----------------------------------------------------------------------------------------------------------- 2m22.88s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m21.60s || +0m01.28s | +0.90% 2m19.62s | Arithmetic.vo | 2m17.66s || +0m01.96s | +1.42% 0m34.02s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m32.24s || +0m01.78s | +5.52% 0m32.06s | ExtractionHaskell/unsaturated_solinas | 0m30.99s || +0m01.07s | +3.45% 0m19.95s | SlowPrimeSynthesisExamples.vo | 0m18.40s || +0m01.55s | +8.42% 3m12.02s | p384_32.c | 3m12.03s || -0m00.00s | -0.00% 1m02.14s | Fancy/Montgomery256.vo | 1m02.09s || +0m00.04s | +0.08% 0m51.24s | Fancy/Barrett256.vo | 0m51.28s || -0m00.03s | -0.07% 0m45.72s | ExtractionHaskell/word_by_word_montgomery | 0m45.05s || +0m00.67s | +1.48% 0m38.67s | p521_32.c | 0m38.24s || +0m00.42s | +1.12% 0m31.94s | p521_64.c | 0m31.38s || +0m00.56s | +1.78% 0m24.85s | ExtractionHaskell/saturated_solinas | 0m24.45s || +0m00.40s | +1.63% 0m23.53s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m22.79s || +0m00.74s | +3.24% 0m21.96s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m21.88s || +0m00.08s | +0.36% 0m19.60s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m19.56s || +0m00.04s | +0.20% 0m17.76s | ExtractionOCaml/word_by_word_montgomery | 0m17.26s || +0m00.50s | +2.89% 0m14.90s | p448_solinas_64.c | 0m14.91s || -0m00.00s | -0.06% 0m13.55s | secp256k1_32.c | 0m13.39s || +0m00.16s | +1.19% 0m13.31s | p256_32.c | 0m13.06s || +0m00.25s | +1.91% 0m13.30s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m12.44s || +0m00.86s | +6.91% 0m11.47s | p484_64.c | 0m11.31s || +0m00.16s | +1.41% 0m11.43s | ExtractionOCaml/unsaturated_solinas | 0m11.15s || +0m00.27s | +2.51% 0m10.55s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.66s || -0m00.10s | -1.03% 0m08.42s | ExtractionOCaml/saturated_solinas | 0m08.24s || +0m00.17s | +2.18% 0m07.07s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.04s || +0m00.03s | +0.42% 0m06.66s | COperationSpecifications.vo | 0m06.31s || +0m00.35s | +5.54% 0m06.50s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.39s || +0m00.11s | +1.72% 0m06.19s | p224_32.c | 0m05.99s || +0m00.20s | +3.33% 0m05.35s | p384_64.c | 0m05.24s || +0m00.10s | +2.09% 0m05.26s | ExtractionOCaml/saturated_solinas.ml | 0m05.24s || +0m00.01s | +0.38% 0m05.24s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.17s || +0m00.07s | +1.35% 0m04.23s | ExtractionHaskell/saturated_solinas.hs | 0m04.12s || +0m00.11s | +2.66% 0m04.14s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m03.89s || +0m00.24s | +6.42% 0m03.68s | PushButtonSynthesis/Primitives.vo | 0m03.62s || +0m00.06s | +1.65% 0m03.58s | PushButtonSynthesis/SmallExamples.vo | 0m03.30s || +0m00.28s | +8.48% 0m03.49s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.25s || +0m00.24s | +7.38% 0m02.38s | curve25519_32.c | 0m02.28s || +0m00.10s | +4.38% 0m01.66s | PushButtonSynthesis/BarrettReduction.vo | 0m01.39s || +0m00.27s | +19.42% 0m01.47s | curve25519_64.c | 0m01.42s || +0m00.05s | +3.52% 0m01.34s | CLI.vo | 0m01.45s || -0m00.10s | -7.58% 0m01.32s | PushButtonSynthesis/MontgomeryReduction.vo | 0m01.30s || +0m00.02s | +1.53% 0m01.08s | secp256k1_64.c | 0m01.04s || +0m00.04s | +3.84% 0m01.07s | StandaloneOCamlMain.vo | 0m01.10s || -0m00.03s | -2.72% 0m01.04s | StandaloneHaskellMain.vo | 0m01.12s || -0m00.08s | -7.14% 0m01.04s | p224_64.c | 0m01.14s || -0m00.09s | -8.77% 0m01.00s | p256_64.c | 0m00.98s || +0m00.02s | +2.04%
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-05 18:06:16 +0000