aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
...
* Add type.related_heteroGravatar Jason Gross2018-07-30
|
* Fix some issues in previous commitGravatar Jason Gross2018-07-30
|
* Add nat_rect_Proper_nondep_genGravatar Jason Gross2018-07-30
|
* Allow proving force ∘ thunk = id extensionallyGravatar Jason Gross2018-07-30
|
* Add UnderLets.wf_Proper_listGravatar Jason Gross2018-07-30
|
* Add wf_spliceGravatar Jason Gross2018-07-30
|
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
|
* Some WIP on Rewiter correctnessGravatar Jason Gross2018-07-30
|
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Now the only admits remaining in Toplevel1 are glue ones about freeze/to_bytes/from_bytes/fe_nonzero. What remains (beyond those admits, and the ones about word-by-word montgomery building blocks in Arithmetic), are the proofs about abstract interpretation and the rewriter. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------- 12m13.17s | Total | 11m45.42s || +0m27.75s | +3.93% -------------------------------------------------------------------------------------------------------- 3m47.20s | Experiments/NewPipeline/Toplevel1 | 3m27.51s || +0m19.68s | +9.48% 0m17.98s | Experiments/NewPipeline/UnderLetsProofs | N/A || +0m17.98s | ∞ N/A | Experiments/NewPipeline/UnderLetsWf | 0m17.94s || -0m17.94s | -100.00% 4m49.57s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 4m45.22s || +0m04.34s | +1.52% 1m16.28s | Experiments/NewPipeline/Toplevel2 | 1m13.33s || +0m02.95s | +4.02% 0m02.96s | Experiments/NewPipeline/MiscCompilerPassesProofs | N/A || +0m02.96s | ∞ N/A | Experiments/NewPipeline/MiscCompilerPassesWf | 0m02.91s || -0m02.91s | -100.00% 0m58.32s | Experiments/NewPipeline/Rewriter | 0m58.58s || -0m00.25s | -0.44% 0m28.19s | Experiments/NewPipeline/LanguageInversion | 0m28.02s || +0m00.17s | +0.60% 0m13.14s | Experiments/NewPipeline/LanguageWf | 0m13.09s || +0m00.05s | +0.38% 0m10.11s | Experiments/NewPipeline/CStringification | 0m10.12s || -0m00.00s | -0.09% 0m01.21s | Experiments/NewPipeline/CLI | 0m01.19s || +0m00.02s | +1.68% 0m01.11s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.13s || -0m00.01s | -1.76% 0m01.09s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.08s || +0m00.01s | +0.92% 0m01.05s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.07s || -0m00.02s | -1.86% 0m00.98s | Experiments/NewPipeline/Language | 0m00.96s || +0m00.02s | +2.08% 0m00.96s | Experiments/NewPipeline/AbstractInterpretation | 0m00.90s || +0m00.05s | +6.66% 0m00.90s | Experiments/NewPipeline/CompilersTestCases | 0m00.92s || -0m00.02s | -2.17% 0m00.66s | Experiments/NewPipeline/RewriterProofs | N/A || +0m00.66s | ∞ 0m00.64s | Experiments/NewPipeline/MiscCompilerPasses | 0m00.65s || -0m00.01s | -1.53% 0m00.42s | Experiments/NewPipeline/UnderLets | 0m00.38s || +0m00.03s | +10.52% 0m00.40s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.42s || -0m00.01s | -4.76%
* Add wf and interp proofs for LetBindReturnGravatar Jason Gross2018-07-27
| | | | | | | | After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------- 0m17.96s | Total | 0m00.90s || +0m17.07s | +1896.66% ---------------------------------------------------------------------------------- 0m17.97s | Experiments/NewPipeline/UnderLetsWf | 0m00.90s || +0m17.07s | +1896.66%
* More proofs about wf / interpGravatar Jason Gross2018-07-27
|
* Add wf about reify/reflect listGravatar Jason Gross2018-07-27
|
* Stronger inversionGravatar Jason Gross2018-07-27
|
* Add invert_nil, invert_consGravatar Jason Gross2018-07-27
|
* Set arguments of ident.{gen_,}interpGravatar Jason Gross2018-07-27
|
* Move rewrites to the correct tacticGravatar Jason Gross2018-07-26
|
* Shuffle transport lemmas around, add more inversionGravatar Jason Gross2018-07-26
|
* Add Wf proofs about MiscCompilerPassesGravatar Jason Gross2018-07-26
|
* Move the associator pass to the rewriterGravatar Jason Gross2018-07-26
| | | | | | This makes it somewhat more ad-hoc (we don't support arbitrary numbers of multiplications), but it should hopefully be much easier to prove things about.
* Improve wf tacticsGravatar Jason Gross2018-07-26
|
* Minor improvements to wf frameworkGravatar Jason Gross2018-07-26
|
* Move some tactics to their proper placeGravatar Jason Gross2018-07-26
|
* Add Wf lemmas about SubstVarGravatar Jason Gross2018-07-26
| | | | | | | | | After | File Name | Before || Change | % Change --------------------------------------------------------------------------------- 0m11.74s | Total | 0m10.83s || +0m00.91s | +8.40% --------------------------------------------------------------------------------- 0m10.85s | Experiments/NewPipeline/LanguageWf | 0m10.83s || +0m00.01s | +0.18% 0m00.89s | Experiments/NewPipeline/UnderLetsWf | N/A || +0m00.89s | ∞
* Put == in type_scope, so that we don't need to go around opening etype_scopeGravatar Jason Gross2018-07-26
|
* Add basic wf proofsGravatar Jason Gross2018-07-26
| | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------- 0m10.67s | Total | 0m00.00s || +0m10.67s | N/A -------------------------------------------------------------------------------- 0m10.68s | Experiments/NewPipeline/LanguageWf | N/A || +0m10.67s | ∞
* Actually improve expr.invert_oneGravatar Jason Gross2018-07-26
|
* Try again to fix expr inversionGravatar Jason Gross2018-07-26
|
* Improve expr.invert_one (hopefully)Gravatar Jason Gross2018-07-26
|
* Add more proper instancesGravatar Jason Gross2018-07-26
|
* Add type.eqv for interp equivalenceGravatar Jason Gross2018-07-26
|
* Add some inversion lemmas and tacticsGravatar Jason Gross2018-07-25
|
* Add invert_LetInGravatar Jason Gross2018-07-25
|
* Reserve ==, ===, ~=Gravatar Jason Gross2018-07-25
|
* Improve rewriter speedGravatar Jason Gross2018-07-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Andres and I met yesterday, and discovered that there's a source of non-linear complexity in the rewriter which is not type casts. In adding side-conditions to the rewrite rules (which are not discussed in the pattern-matching compilation paper), I represented them by allowing rewrite rules to fail. So, for example, # + x ~~> x (when # == 0) is represented as # + x ~~> if (# =? 0) then Some x else None In the case that a rewrite rule fails, we need to try all other rewrite rules that might still apply. However, doing this in the naive-CPS way leads to non-linear blowup, because wildcard rewrite rules get duplicated in the failure branches. (This is similar to the issue that `match x with "some string" => true | _ => false end%string` will generate a large number of "false" branches, and duplicate "false" across all of them, rather than having a single default case.) For example, if we had the rewrite rules # + # ~~> literal sum x + (-y) ~~> x - y (-x) + y ~~> y - x then the compiled code would look like fun x y => if x is a literal then if y is a literal then literal sum else if y is an opp then x - y else x + y else if y is an opp then x - y else if x is an opp then y - x else x + y where we actually want the code fun x y => if x is a literal then if y is a literal then return (literal sum); if y is an opp then return (x - y); if x is an opp then return (y - x); return (x + y) in the sequence+return monad. i.e., we want to not duplicate the "if y is an opp" code multiple times. I think the solution to this is to have the discrimination tree evaluator return an option, and to have the function that computes the discrimination tree not duplicate rewrite rules among different cases. Note that this leads to slightly inefficient matching sometimes: when two rules with the same structure are separated by a rule with a wildcard instead of structure, we will now try to match on the structure twice. It might be useful to be able to denote that some rewrite rules can be commuted. Also, we remove `Module pident := pattern.ident.` to work around https://github.com/coq/coq/issues/8152, now that we're no longer unfolding all of the `pattern.ident` stuff (because not unfolding it gives slightly nicer output code). After | File Name | Before || Change | % Change --------------------------------------------------------------------------------------------------------------------- 17m41.82s | Total | 29m58.10s || -12m16.27s | -40.94% --------------------------------------------------------------------------------------------------------------------- 1m08.84s | Experiments/NewPipeline/Rewriter | 5m16.96s || -4m08.11s | -78.28% 0m37.50s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 2m03.59s || -1m26.09s | -69.65% 0m17.35s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m41.56s || -1m24.21s | -82.91% 0m24.10s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m43.33s || -1m19.22s | -76.67% 0m38.44s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m28.64s || -0m50.20s | -56.63% 0m20.86s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m06.91s || -0m46.04s | -68.82% 0m11.46s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.64s || -0m44.17s | -79.40% 0m04.17s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m22.22s || -0m18.04s | -81.23% 1m31.73s | Experiments/NewPipeline/Toplevel2 | 1m49.50s || -0m17.76s | -16.22% 0m06.12s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m23.22s || -0m17.09s | -73.64% 0m08.69s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m22.12s || -0m13.43s | -60.71% 0m05.80s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m15.32s || -0m09.51s | -62.14% 0m04.10s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m13.20s || -0m09.09s | -68.93% 0m03.30s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m13.02s || -0m09.71s | -74.65% 5m47.58s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m52.86s || -0m05.28s | -1.49% 4m02.15s | Experiments/NewPipeline/Toplevel1 | 4m04.75s || -0m02.59s | -1.06% 0m11.40s | p384_64.c | 0m09.04s || +0m02.36s | +26.10% 0m34.20s | p521_64.c | 0m32.80s || +0m01.40s | +4.26% 0m23.40s | p384_32.c | 0m21.95s || +0m01.44s | +6.60% 0m38.90s | p521_32.c | 0m39.34s || -0m00.44s | -1.11% 0m03.40s | p256_32.c | 0m03.63s || -0m00.23s | -6.33% 0m03.24s | secp256k1_32.c | 0m03.37s || -0m00.12s | -3.85% 0m02.14s | curve25519_32.c | 0m02.00s || +0m00.14s | +7.00% 0m02.13s | p256_64.c | 0m01.72s || +0m00.40s | +23.83% 0m01.82s | p224_32.c | 0m01.82s || +0m00.00s | +0.00% 0m01.44s | p224_64.c | 0m01.48s || -0m00.04s | -2.70% 0m01.40s | secp256k1_64.c | 0m01.97s || -0m00.57s | -28.93% 0m01.35s | curve25519_64.c | 0m01.34s || +0m00.01s | +0.74% 0m01.34s | Experiments/NewPipeline/CLI | 0m01.32s || +0m00.02s | +1.51% 0m01.20s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.16s || +0m00.04s | +3.44% 0m01.20s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.25s || -0m00.05s | -4.00% 0m01.08s | Experiments/NewPipeline/CompilersTestCases | 0m01.07s || +0m00.01s | +0.93%
* Add option sequencing/returnGravatar Jason Gross2018-07-25
|
* Reserve ;;;, fix level of prefix # to not clash with infix #Gravatar Jason Gross2018-07-25
|
* Revert "Improve rewriter speed"Gravatar Jason Gross2018-07-24
| | | | | | | This reverts commit 152094f4d9d83e4a5689536e0cd68d4f006517e1. It is actually incorrect. We need to bubble up failures, not just let-bind the default case. Will fix tomorrow.
* Improve rewriter speedGravatar Jason Gross2018-07-24
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Andres and I met today, and discovered that there's a source of non-linear complexity in the rewriter which is not type casts. In adding side-conditions to the rewrite rules (which are not discussed in the pattern-matching compilation paper), I represented them by allowing rewrite rules to fail. So, for example, # + x ~~> x (when # == 0) is represented as # + x ~~> if (# =? 0) then Some x else None In the case that a rewrite rule fails, we need to try all other rewrite rules that might still apply. However, doing this in the naive-CPS way leads to non-linear blowup, because wildcard rewrite rules get duplicated in the failure branches. (This is similar to the issue that `match x with "some string" => true | _ => false end%string` will generate a large number of "false" branches, and duplicate "false" across all of them, rather than having a single default case.) For example, if we had the rewrite rules # + # ~~> literal sum x + (-y) ~~> x - y (-x) + y ~~> y - x then the compiled code would look like fun x y => if x is a literal then if y is a literal then literal sum else if y is an opp then x - y else x + y else if y is an opp then x - y else if x is an opp then y - x else x + y where we actually want the code fun x y => if x is a literal then if y is a literal then return (literal sum); if y is an opp then return (x - y); if x is an opp then return (y - x); return (x + y) in the sequence+return monad. i.e., we want to not duplicate the "if y is an opp" code multiple times. I think the solution to this is to have the discrimination tree evaluator return an option, and to have the function that computes the discrimination tree not duplicate rewrite rules among different cases. Note that this leads to slightly inefficient matching sometimes: when two rules with the same structure are separated by a rule with a wildcard instead of structure, we will now try to match on the structure twice. It might be useful to be able to denote that some rewrite rules can be commuted. After | File Name | Before || Change | % Change ---------------------------------------------------------------------------------------------------------------------- 40m35.83s | Total | 30m00.99s || +10m34.84s | +35.24% ---------------------------------------------------------------------------------------------------------------------- 21m46.37s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 6m01.39s || +15m44.97s | +261.48% 6m37.40s | p384_32.c | 0m22.47s || +6m14.92s | +1668.58% 0m18.00s | Experiments/NewPipeline/Rewriter | 5m16.50s || -4m58.50s | -94.31% 0m30.49s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 1m54.20s || -1m23.71s | -73.30% 0m27.41s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 1m39.40s || -1m11.99s | -72.42% 0m47.78s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 1m54.50s || -1m06.71s | -58.27% 0m40.28s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 1m23.77s || -0m43.48s | -51.91% 0m15.21s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m55.86s || -0m40.64s | -72.77% 0m23.39s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 1m00.22s || -0m36.82s | -61.15% 0m21.85s | p256_32.c | 0m04.01s || +0m17.84s | +444.88% 0m20.97s | secp256k1_32.c | 0m03.26s || +0m17.71s | +543.25% 0m04.60s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m20.33s || -0m15.72s | -77.37% 0m09.48s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m23.28s || -0m13.80s | -59.27% 1m33.63s | Experiments/NewPipeline/Toplevel2 | 1m45.56s || -0m11.93s | -11.30% 0m08.29s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m18.64s || -0m10.35s | -55.52% 0m05.93s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m16.74s || -0m10.80s | -64.57% 0m32.41s | p521_64.c | 0m41.42s || -0m09.01s | -21.75% 0m04.93s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m14.92s || -0m09.99s | -66.95% 0m04.40s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m12.57s || -0m08.16s | -64.99% 0m08.52s | p224_32.c | 0m01.95s || +0m06.56s | +336.92% 0m13.99s | p384_64.c | 0m10.64s || +0m03.34s | +31.48% 4m07.13s | Experiments/NewPipeline/Toplevel1 | 4m05.83s || +0m01.29s | +0.52% 0m38.96s | p521_32.c | 0m40.09s || -0m01.13s | -2.81% 0m02.28s | p224_64.c | 0m01.66s || +0m00.61s | +37.34% 0m02.27s | curve25519_32.c | 0m01.98s || +0m00.29s | +14.64% 0m01.78s | p256_64.c | 0m01.65s || +0m00.13s | +7.87% 0m01.70s | secp256k1_64.c | 0m01.96s || -0m00.26s | -13.26% 0m01.65s | curve25519_64.c | 0m01.51s || +0m00.13s | +9.27% 0m01.37s | Experiments/NewPipeline/CLI | 0m01.26s || +0m00.11s | +8.73% 0m01.15s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.21s || -0m00.06s | -4.95% 0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.16s || -0m00.02s | -1.72% 0m01.07s | Experiments/NewPipeline/CompilersTestCases | 0m01.05s || +0m00.02s | +1.90%
* Add ListUtil.{take,drop}_whileGravatar Jason Gross2018-07-24
|
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------- 18m19.81s | Total | 14m31.66s || +3m48.14s | +26.17% -------------------------------------------------------------------------------------------------------- 4m04.77s | Experiments/NewPipeline/Toplevel1 | 1m38.04s || +2m26.73s | +149.66% 5m12.44s | Experiments/NewPipeline/Rewriter | 4m20.00s || +0m52.43s | +20.16% 1m26.58s | Experiments/NewPipeline/Arithmetic | 0m55.51s || +0m31.07s | +55.97% 5m44.19s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m45.62s || -0m01.43s | -0.41% 1m29.48s | Experiments/NewPipeline/Toplevel2 | 1m29.73s || -0m00.25s | -0.27% 0m12.75s | Experiments/NewPipeline/CStringification | 0m12.71s || +0m00.03s | +0.31% 0m01.32s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.20s || +0m00.12s | +10.00% 0m01.31s | Experiments/NewPipeline/CLI | 0m01.33s || -0m00.02s | -1.50% 0m01.18s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.22s || -0m00.04s | -3.27% 0m01.12s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.21s || -0m00.08s | -7.43% 0m01.11s | Experiments/NewPipeline/Language | 0m01.14s || -0m00.02s | -2.63% 0m01.08s | Experiments/NewPipeline/AbstractInterpretation | 0m01.16s || -0m00.07s | -6.89% 0m00.90s | Experiments/NewPipeline/MiscCompilerPasses | 0m00.87s || +0m00.03s | +3.44% 0m00.74s | Experiments/NewPipeline/CompilersTestCases | 0m01.03s || -0m00.29s | -28.15% 0m00.44s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.40s || +0m00.03s | +9.99% 0m00.41s | Experiments/NewPipeline/UnderLets | 0m00.50s || -0m00.09s | -18.00% After | File Name | Before || Change | % Change ------------------------------------------------------------------------------------------------------------------------- 107m58.13s | Total | 102m35.85s || +5m22.27s | +5.23% ------------------------------------------------------------------------------------------------------------------------- 4m32.58s | Experiments/NewPipeline/Toplevel1 | 1m50.07s || +2m42.50s | +147.64% N/A | ─abstract | 1m54.94s || -1m54.93s | -100.00% 1m54.19s | Specific/X2448/Karatsuba/C64/femul | N/A || +1m54.18s | ∞ 7m58.19s | Experiments/NewPipeline/Rewriter | 6m45.32s || +1m12.87s | +17.97% 2m13.30s | Experiments/NewPipeline/Arithmetic | 1m34.69s || +0m38.61s | +40.77% 5m30.50s | Curves/Weierstrass/Projective | 5m09.44s || +0m21.06s | +6.80% 12m00.73s | Curves/Weierstrass/AffineProofs | 11m43.07s || +0m17.65s | +2.51% 0m54.76s | Compilers/Z/ArithmeticSimplifierWf | 0m43.68s || +0m11.07s | +25.36% 10m06.67s | Experiments/SimplyTypedArithmetic | 9m58.44s || +0m08.22s | +1.37% 1m05.15s | Arithmetic/Karatsuba | 0m58.76s || +0m06.39s | +10.87% 0m41.15s | Specific/NISTP256/AMD128/femul | 0m47.16s || -0m06.00s | -12.74% 5m46.39s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m52.03s || -0m05.63s | -1.60% 2m14.99s | Specific/X25519/C64/ladderstep | 2m20.69s || -0m05.69s | -4.05% 0m48.64s | Specific/X25519/C32/freeze | 0m43.24s || +0m05.39s | +12.48% 0m26.80s | Specific/X25519/C64/fesquare | 0m20.83s || +0m05.97s | +28.66% 0m27.22s | Specific/X25519/C32/feadd | 0m31.34s || -0m04.12s | -13.14% 0m23.26s | Specific/NISTP256/AMD64/fenz | 0m19.10s || +0m04.16s | +21.78% 0m21.24s | Specific/NISTP256/AMD128/fesub | 0m25.24s || -0m04.00s | -15.84% 3m38.32s | Curves/Montgomery/XZProofs | 3m34.65s || +0m03.66s | +1.70% 1m14.93s | Compilers/Z/ArithmeticSimplifierInterp | 1m11.88s || +0m03.05s | +4.24% 0m16.16s | Arithmetic/Saturated/MontgomeryAPI | 0m12.26s || +0m03.90s | +31.81% 0m07.54s | Compilers/Z/Bounds/InterpretationLemmas/PullCast | 0m10.65s || -0m03.11s | -29.20% 2m29.22s | Specific/NISTP256/AMD64/femul | 2m31.90s || -0m02.68s | -1.76% 2m02.88s | Compilers/Named/MapCastInterp | 2m00.84s || +0m02.03s | +1.68% 1m54.19s | Curves/Weierstrass/Jacobian | 1m52.12s || +0m02.06s | +1.84% 1m30.98s | Specific/X25519/C32/femul | 1m28.28s || +0m02.70s | +3.05% 1m30.59s | Experiments/NewPipeline/Toplevel2 | 1m32.97s || -0m02.37s | -2.55% 1m20.73s | Demo | 1m18.51s || +0m02.21s | +2.82% 1m07.85s | Specific/X25519/C32/fesquare | 1m09.85s || -0m02.00s | -2.86% 0m31.78s | Specific/X25519/C32/fesub | 0m34.25s || -0m02.46s | -7.21% 0m31.18s | Arithmetic/Core | 0m33.92s || -0m02.74s | -8.07% 0m26.24s | Compilers/Z/CNotations | 0m28.35s || -0m02.11s | -7.44% 0m22.15s | Specific/X25519/C64/fecarry | 0m19.73s || +0m02.41s | +12.26% 0m21.61s | Arithmetic/Saturated/AddSub | 0m18.87s || +0m02.73s | +14.52% 0m21.58s | Specific/X25519/C64/fesub | 0m19.14s || +0m02.43s | +12.74% 0m14.37s | Arithmetic/Saturated/Core | 0m16.57s || -0m02.20s | -13.27% 2m57.98s | Curves/Montgomery/AffineProofs | 2m59.71s || -0m01.73s | -0.96% 1m46.10s | Spec/Test/X25519 | 1m47.38s || -0m01.28s | -1.19% 0m40.69s | Primitives/EdDSARepChange | 0m42.34s || -0m01.65s | -3.89% 0m40.29s | Specific/X25519/C32/fecarry | 0m42.21s || -0m01.92s | -4.54% 0m33.64s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs | 0m31.88s || +0m01.76s | +5.52% 0m31.96s | Specific/NISTP256/AMD64/feadd | 0m30.27s || +0m01.69s | +5.58% 0m23.14s | Specific/NISTP256/AMD128/feadd | 0m24.34s || -0m01.19s | -4.93% 0m18.76s | Specific/NISTP256/AMD128/feopp | 0m20.20s || -0m01.43s | -7.12% 0m18.62s | Compilers/Z/Syntax/Equality | 0m17.08s || +0m01.54s | +9.01% 0m15.06s | Util/ZUtil | 0m13.95s || +0m01.11s | +7.95% 0m14.13s | LegacyArithmetic/ArchitectureToZLikeProofs | 0m12.75s || +0m01.38s | +10.82% 0m12.43s | Compilers/Named/CompileInterpSideConditions | 0m10.85s || +0m01.58s | +14.56% 0m10.06s | Specific/NISTP256/AMD64/Synthesis | 0m11.31s || -0m01.25s | -11.05% 0m08.04s | Arithmetic/BarrettReduction/Generalized | 0m09.68s || -0m01.64s | -16.94% 0m06.25s | Specific/Framework/ArithmeticSynthesis/Montgomery | 0m05.18s || +0m01.07s | +20.65% 0m05.70s | LegacyArithmetic/InterfaceProofs | 0m07.21s || -0m01.50s | -20.94% 0m05.50s | Compilers/Z/Bounds/Pipeline/Definition | 0m06.57s || -0m01.07s | -16.28% 0m04.54s | LegacyArithmetic/Double/Proofs/Decode | 0m05.59s || -0m01.04s | -18.78% 0m04.32s | Compilers/Z/ArithmeticSimplifier | 0m05.36s || -0m01.04s | -19.40% 0m02.15s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m03.49s || -0m01.34s | -38.39% N/A | Coqprime/PrimalityTest/EGroup | 0m01.32s || -0m01.32s | -100.00% N/A | Coqprime/Z/ZCAux | 0m01.08s || -0m01.08s | -100.00% 1m21.20s | Compilers/Z/Named/RewriteAddToAdcInterp | 1m21.80s || -0m00.59s | -0.73% 0m43.90s | Spec/Ed25519 | 0m43.40s || +0m00.50s | +1.15% 0m40.68s | Compilers/CommonSubexpressionEliminationWf | 0m40.81s || -0m00.13s | -0.31% 0m34.84s | Specific/NISTP256/AMD64/fesub | 0m33.87s || +0m00.97s | +2.86% 0m32.80s | Specific/X25519/C64/femul | 0m31.99s || +0m00.80s | +2.53% 0m30.69s | Curves/Edwards/XYZT/Basic | 0m30.20s || +0m00.49s | +1.62% 0m27.90s | Compilers/Named/MapCastWf | 0m27.10s || +0m00.79s | +2.95% 0m27.80s | Specific/X25519/C32/Synthesis | 0m28.14s || -0m00.33s | -1.20% 0m27.70s | bbv/Word | 0m27.58s || +0m00.12s | +0.43% 0m26.05s | Specific/NISTP256/AMD64/feopp | 0m26.52s || -0m00.46s | -1.77% 0m25.59s | Specific/X25519/C64/freeze | 0m25.20s || +0m00.39s | +1.54% 0m25.40s | Curves/Edwards/AffineProofs | 0m24.70s || +0m00.69s | +2.83% 0m22.94s | Compilers/Named/ContextProperties/NameUtil | 0m23.02s || -0m00.07s | -0.34% 0m22.14s | Algebra/Field | 0m21.80s || +0m00.33s | +1.55% 0m21.99s | Specific/NISTP256/AMD128/fenz | 0m21.30s || +0m00.68s | +3.23% 0m21.68s | Compilers/Named/ContextProperties/SmartMap | 0m22.15s || -0m00.46s | -2.12% 0m20.08s | Experiments/NewPipeline/CStringification | 0m19.13s || +0m00.94s | +4.96% 0m19.91s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs | 0m19.60s || +0m00.30s | +1.58% 0m19.57s | Specific/X25519/C64/feadd | 0m19.12s || +0m00.44s | +2.35% 0m17.58s | Primitives/MxDHRepChange | 0m17.59s || -0m00.01s | -0.05% 0m17.56s | LegacyArithmetic/Double/Proofs/Multiply | 0m18.42s || -0m00.86s | -4.66% 0m15.44s | Arithmetic/MontgomeryReduction/Proofs | 0m14.96s || +0m00.47s | +3.20% 0m14.54s | Specific/X2448/Karatsuba/C64/Synthesis | 0m14.15s || +0m00.38s | +2.75% 0m14.18s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate | 0m13.57s || +0m00.60s | +4.49% 0m13.88s | Algebra/Ring | 0m13.58s || +0m00.30s | +2.20% 0m13.44s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate | 0m13.40s || +0m00.03s | +0.29% 0m11.85s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub | 0m11.82s || +0m00.02s | +0.25% 0m11.46s | Compilers/InlineConstAndOpWf | 0m11.58s || -0m00.11s | -1.03% 0m11.43s | Compilers/Named/RegisterAssignInterp | 0m11.26s || +0m00.16s | +1.50% 0m11.29s | Arithmetic/BarrettReduction/RidiculousFish | 0m10.73s || +0m00.55s | +5.21% 0m10.27s | Arithmetic/Saturated/MulSplit | 0m10.24s || +0m00.02s | +0.29% 0m10.07s | Util/ZUtil/ZSimplify/Autogenerated | 0m09.74s || +0m00.33s | +3.38% 0m09.72s | Util/FixedWordSizesEquality | 0m10.08s || -0m00.35s | -3.57% 0m09.25s | LegacyArithmetic/Pow2BaseProofs | 0m09.10s || +0m00.15s | +1.64% 0m08.74s | Compilers/InlineWf | 0m08.45s || +0m00.29s | +3.43% 0m08.65s | Util/FsatzAutoLemmas | 0m08.94s || -0m00.28s | -3.24% 0m08.30s | Util/ListUtil | 0m08.37s || -0m00.06s | -0.83% 0m08.12s | Compilers/LinearizeWf | 0m08.43s || -0m00.31s | -3.67% 0m07.92s | Specific/X25519/C64/Synthesis | 0m07.90s || +0m00.01s | +0.25% 0m07.72s | Arithmetic/BarrettReduction/HAC | 0m07.57s || +0m00.14s | +1.98% 0m07.64s | Compilers/Z/HexNotationConstants | 0m08.06s || -0m00.42s | -5.21% 0m07.62s | Util/ZUtil/Modulo | 0m07.58s || +0m00.04s | +0.52% 0m07.54s | Curves/Edwards/Pre | 0m07.92s || -0m00.37s | -4.79% 0m07.34s | Compilers/WfProofs | 0m06.72s || +0m00.62s | +9.22% 0m06.86s | Algebra/Field_test | 0m07.34s || -0m00.47s | -6.53% 0m06.80s | Compilers/Z/BinaryNotationConstants | 0m06.76s || +0m00.04s | +0.59% 0m06.00s | LegacyArithmetic/Double/Proofs/ShiftRight | 0m06.00s || +0m00.00s | +0.00% 0m05.58s | Compilers/Named/CompileWf | 0m05.85s || -0m00.26s | -4.61% 0m05.58s | Curves/Montgomery/Affine | 0m06.52s || -0m00.93s | -14.41% 0m05.31s | Specific/NISTP256/AMD128/Synthesis | 0m04.90s || +0m00.40s | +8.36% 0m05.17s | LegacyArithmetic/Double/Proofs/ShiftLeft | 0m05.14s || +0m00.03s | +0.58% 0m05.14s | Arithmetic/ModularArithmeticTheorems | 0m05.32s || -0m00.18s | -3.38% 0m04.93s | LegacyArithmetic/ZBoundedZ | 0m05.51s || -0m00.58s | -10.52% 0m04.90s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy | 0m05.62s || -0m00.71s | -12.81% 0m04.76s | Compilers/TestCase | 0m04.72s || +0m00.04s | +0.84% 0m04.74s | Arithmetic/MontgomeryReduction/WordByWord/Proofs | 0m05.51s || -0m00.76s | -13.97% 0m04.48s | Util/WordUtil | 0m04.51s || -0m00.02s | -0.66% 0m04.32s | Spec/MontgomeryCurve | 0m03.77s || +0m00.55s | +14.58% 0m04.13s | Compilers/InlineInterp | 0m04.29s || -0m00.16s | -3.72% 0m04.09s | Util/ZUtil/Div | 0m03.82s || +0m00.27s | +7.06% 0m03.96s | LegacyArithmetic/BarretReduction | 0m04.49s || -0m00.53s | -11.80% 0m03.93s | Compilers/EtaWf | 0m03.94s || -0m00.00s | -0.25% 0m03.81s | Compilers/Named/ContextProperties | 0m04.33s || -0m00.52s | -12.00% 0m03.69s | Specific/NISTP256/FancyMachine256/Montgomery | 0m03.77s || -0m00.08s | -2.12% 0m03.65s | Algebra/Group | 0m03.95s || -0m00.30s | -7.59% 0m03.63s | Arithmetic/Saturated/Freeze | 0m03.63s || +0m00.00s | +0.00% 0m03.54s | Compilers/Z/RewriteAddToAdcInterp | 0m03.26s || +0m00.28s | +8.58% 0m03.49s | Compilers/Named/CompileInterp | 0m03.55s || -0m00.05s | -1.69% 0m03.47s | Compilers/Z/Bounds/Relax | 0m03.12s || +0m00.35s | +11.21% 0m03.31s | Specific/NISTP256/FancyMachine256/Barrett | 0m03.70s || -0m00.39s | -10.54% 0m03.21s | Compilers/Named/NameUtilProperties | 0m03.16s || +0m00.04s | +1.58% 0m03.15s | Specific/NISTP256/FancyMachine256/Core | 0m02.96s || +0m00.18s | +6.41% 0m03.14s | Compilers/Named/ContextProperties/Proper | 0m03.67s || -0m00.52s | -14.44% 0m03.06s | Compilers/Z/JavaNotations | 0m03.18s || -0m00.12s | -3.77% 0m03.00s | Compilers/CommonSubexpressionEliminationProperties | 0m02.91s || +0m00.08s | +3.09% 0m02.94s | Compilers/WfReflective | 0m02.18s || +0m00.75s | +34.86% 0m02.91s | Util/ZUtil/Quot | 0m02.24s || +0m00.67s | +29.91% 0m02.80s | Arithmetic/CoreUnfolder | 0m02.53s || +0m00.27s | +10.67% 0m02.78s | Util/ZUtil/AddGetCarry | 0m02.78s || +0m00.00s | +0.00% 0m02.67s | Spec/WeierstrassCurve | 0m02.45s || +0m00.21s | +8.97% 0m02.54s | Compilers/Named/WfFromUnit | 0m02.61s || -0m00.06s | -2.68% 0m02.51s | Specific/Framework/ReificationTypes | 0m02.57s || -0m00.06s | -2.33% 0m02.45s | Arithmetic/BarrettReduction/Wikipedia | 0m02.72s || -0m00.27s | -9.92% 0m02.41s | Specific/Framework/OutputType | 0m02.49s || -0m00.08s | -3.21% 0m02.35s | Compilers/Named/InterpretToPHOASWf | 0m02.44s || -0m00.08s | -3.68% 0m02.31s | Util/NatUtil | 0m02.31s || +0m00.00s | +0.00% 0m02.26s | LegacyArithmetic/MontgomeryReduction | 0m02.40s || -0m00.14s | -5.83% 0m02.25s | Util/ZUtil/Pow2Mod | 0m02.19s || +0m00.06s | +2.73% 0m02.21s | Specific/Framework/ArithmeticSynthesis/Base | 0m02.23s || -0m00.02s | -0.89% 0m02.20s | Curves/Edwards/XYZT/Precomputed | 0m02.07s || +0m00.13s | +6.28% 0m02.16s | Arithmetic/PrimeFieldTheorems | 0m01.58s || +0m00.58s | +36.70% 0m02.16s | LegacyArithmetic/Double/Proofs/BitwiseOr | 0m02.20s || -0m00.04s | -1.81% 0m02.12s | LegacyArithmetic/Double/Proofs/LoadImmediate | 0m02.20s || -0m00.08s | -3.63% 0m02.06s | Util/QUtil | 0m02.08s || -0m00.02s | -0.96% 0m02.03s | Compilers/Relations | 0m02.31s || -0m00.28s | -12.12% 0m02.02s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes | 0m01.99s || +0m00.03s | +1.50% 0m02.00s | Util/Tuple | 0m01.75s || +0m00.25s | +14.28% 0m01.87s | Algebra/ScalarMult | 0m01.76s || +0m00.11s | +6.25% 0m01.82s | Arithmetic/Saturated/CoreUnfolder | 0m01.76s || +0m00.06s | +3.40% 0m01.82s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.43s || +0m00.39s | +27.27% 0m01.82s | LegacyArithmetic/BaseSystemProofs | 0m01.98s || -0m00.15s | -8.08% 0m01.80s | Compilers/LinearizeInterp | 0m01.76s || +0m00.04s | +2.27% 0m01.80s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.47s || +0m00.33s | +22.44% 0m01.76s | Compilers/MultiSizeTest | 0m01.78s || -0m00.02s | -1.12% 0m01.76s | Compilers/Z/RewriteAddToAdcWf | 0m01.70s || +0m00.06s | +3.52% 0m01.76s | Experiments/NewPipeline/Language | 0m01.67s || +0m00.09s | +5.38% 0m01.72s | Experiments/NewPipeline/AbstractInterpretation | 0m01.72s || +0m00.00s | +0.00% 0m01.66s | Util/ZUtil/Stabilization | 0m01.55s || +0m00.10s | +7.09% 0m01.64s | Specific/Framework/IntegrationTestDisplayCommon | 0m01.75s || -0m00.11s | -6.28% 0m01.58s | Compilers/Named/InterpretToPHOASInterp | 0m01.59s || -0m00.01s | -0.62% 0m01.54s | Util/ZUtil/Modulo/PullPush | 0m01.26s || +0m00.28s | +22.22% 0m01.51s | Util/NumTheoryUtil | 0m01.33s || +0m00.17s | +13.53% 0m01.51s | Util/ZRange/CornersMonotoneBounds | 0m01.88s || -0m00.36s | -19.68% 0m01.45s | Arithmetic/Saturated/UniformWeight | 0m01.30s || +0m00.14s | +11.53% 0m01.42s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m01.49s || -0m00.07s | -4.69% 0m01.37s | Compilers/Z/CommonSubexpressionElimination | 0m01.45s || -0m00.07s | -5.51% 0m01.36s | Compilers/MapCastByDeBruijnInterp | 0m01.32s || +0m00.04s | +3.03% 0m01.34s | Specific/X25519/C32/CurveParameters | 0m01.25s || +0m00.09s | +7.20% 0m01.32s | Compilers/Z/Syntax/Util | 0m01.12s || +0m00.19s | +17.85% 0m01.32s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.90s || +0m00.42s | +46.66% 0m01.31s | Algebra/IntegralDomain | 0m01.31s || +0m00.00s | +0.00% 0m01.31s | Arithmetic/Saturated/MulSplitUnfolder | 0m01.32s || -0m00.01s | -0.75% 0m01.31s | Compilers/Named/CompileProperties | 0m01.30s || +0m00.01s | +0.76% 0m01.31s | Util/ZUtil/Testbit | 0m01.66s || -0m00.34s | -21.08% 0m01.30s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m01.29s || +0m00.01s | +0.77% 0m01.30s | Experiments/NewPipeline/CLI | 0m01.28s || +0m00.02s | +1.56% 0m01.27s | bbv/NatLib | 0m01.06s || +0m00.20s | +19.81% 0m01.26s | Arithmetic/Saturated/FreezeUnfolder | 0m00.84s || +0m00.42s | +50.00% 0m01.24s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m01.31s || -0m00.07s | -5.34% 0m01.22s | Util/ZUtil/EquivModulo | 0m01.16s || +0m00.06s | +5.17% 0m01.21s | Specific/Framework/MontgomeryReificationTypes | 0m01.19s || +0m00.02s | +1.68% 0m01.19s | Specific/Framework/ReificationTypesPackage | 0m00.85s || +0m00.34s | +40.00% 0m01.19s | Specific/Framework/SynthesisFramework | 0m01.04s || +0m00.14s | +14.42% 0m01.17s | Experiments/NewPipeline/MiscCompilerPasses | 0m01.25s || -0m00.08s | -6.40% 0m01.15s | Compilers/Named/AListContext | 0m01.08s || +0m00.06s | +6.48% 0m01.14s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m01.18s || -0m00.04s | -3.38% 0m01.14s | Arithmetic/Saturated/Wrappers | 0m00.85s || +0m00.28s | +34.11% 0m01.14s | Specific/Framework/ArithmeticSynthesis/HelperTactics | 0m01.12s || +0m00.01s | +1.78% 0m01.14s | Util/PartiallyReifiedProp | 0m01.12s || +0m00.01s | +1.78% 0m01.14s | Util/ZRange/BasicLemmas | 0m01.26s || -0m00.12s | -9.52% 0m01.13s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.86s || +0m00.26s | +31.39% 0m01.12s | Compilers/InlineConstAndOpInterp | 0m00.90s || +0m00.22s | +24.44% 0m01.12s | Compilers/WfInversion | 0m01.18s || -0m00.05s | -5.08% 0m01.12s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.77s || +0m00.35s | +45.45% 0m01.11s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m01.13s || -0m00.01s | -1.76% 0m01.08s | Compilers/Named/FMapContext | 0m01.27s || -0m00.18s | -14.96% 0m01.08s | Curves/Montgomery/AffineInstances | 0m01.16s || -0m00.07s | -6.89% 0m01.08s | Util/ZUtil/Peano | 0m01.10s || -0m00.02s | -1.81% 0m01.08s | Util/ZUtil/ZSimplify/Simple | 0m00.88s || +0m00.20s | +22.72% 0m01.07s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m01.14s || -0m00.06s | -6.14% 0m01.06s | LegacyArithmetic/Double/Proofs/SelectConditional | 0m01.09s || -0m00.03s | -2.75% 0m01.04s | Compilers/InterpByIsoProofs | 0m01.16s || -0m00.11s | -10.34% 0m01.03s | Compilers/SmartMap | 0m01.04s || -0m00.01s | -0.96% 0m01.03s | Compilers/Z/Bounds/Pipeline | 0m00.85s || +0m00.18s | +21.17% 0m01.03s | Util/ZUtil/Morphisms | 0m01.23s || -0m00.19s | -16.26% 0m01.02s | Curves/Montgomery/XZ | 0m00.96s || +0m00.06s | +6.25% 0m01.01s | Arithmetic/Saturated/WrappersUnfolder | 0m01.59s || -0m00.58s | -36.47% 0m01.01s | Compilers/Named/InterpSideConditionsInterp | 0m01.12s || -0m00.11s | -9.82% 0m01.00s | Util/CPSUtil | 0m01.09s || -0m00.09s | -8.25% 0m00.99s | Compilers/CommonSubexpressionElimination | 0m00.78s || +0m00.20s | +26.92% 0m00.96s | Util/ZUtil/CC | 0m00.89s || +0m00.06s | +7.86% 0m00.95s | Compilers/MapBaseTypeWf | 0m00.78s || +0m00.16s | +21.79% 0m00.95s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m01.10s || -0m00.15s | -13.63% 0m00.94s | Compilers/Z/Reify | 0m00.96s || -0m00.02s | -2.08% 0m00.93s | Compilers/Z/Bounds/Pipeline/Glue | 0m00.88s || +0m00.05s | +5.68% 0m00.92s | Arithmetic/Saturated/UniformWeightInstances | 0m01.10s || -0m00.18s | -16.36% 0m00.92s | Compilers/Z/Bounds/MapCastByDeBruijnInterp | 0m00.90s || +0m00.02s | +2.22% 0m00.89s | Compilers/Z/MapCastByDeBruijnInterp | 0m00.87s || +0m00.02s | +2.29% 0m00.89s | Curves/Weierstrass/Affine | 0m00.79s || +0m00.09s | +12.65% 0m00.89s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.76s || +0m00.13s | +17.10% 0m00.89s | Util/ZUtil/Tactics/RewriteModSmall | 0m01.13s || -0m00.23s | -21.23% 0m00.88s | Compilers/Named/WfInterp | 0m00.76s || +0m00.12s | +15.78% 0m00.88s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.80s || +0m00.07s | +9.99% 0m00.88s | Util/Decidable | 0m00.81s || +0m00.06s | +8.64% 0m00.88s | Util/Factorize | 0m00.92s || -0m00.04s | -4.34% 0m00.88s | Util/ZUtil/Rshi | 0m01.11s || -0m00.23s | -20.72% 0m00.86s | Compilers/Z/Bounds/RoundUpLemmas | 0m00.90s || -0m00.04s | -4.44% 0m00.86s | LegacyArithmetic/Double/Core | 0m00.90s || -0m00.04s | -4.44% 0m00.85s | Arithmetic/ModularArithmeticPre | 0m00.82s || +0m00.03s | +3.65% N/A | Coqprime/Z/ZSum | 0m00.85s || -0m00.85s | -100.00% 0m00.85s | Specific/Framework/ArithmeticSynthesis/Ladderstep | 0m01.10s || -0m00.25s | -22.72% 0m00.84s | Compilers/Z/Bounds/InterpretationLemmas/Tactics | 0m00.88s || -0m00.04s | -4.54% 0m00.84s | Compilers/Z/Bounds/MapCastByDeBruijnWf | 0m00.85s || -0m00.01s | -1.17% 0m00.84s | LegacyArithmetic/ZBounded | 0m00.80s || +0m00.03s | +4.99% 0m00.84s | Spec/EdDSA | 0m00.55s || +0m00.28s | +52.72% 0m00.83s | Compilers/Z/Bounds/MapCastByDeBruijn | 0m00.87s || -0m00.04s | -4.59% 0m00.83s | LegacyArithmetic/BaseSystem | 0m00.78s || +0m00.04s | +6.41% 0m00.82s | Compilers/Z/MapCastByDeBruijnWf | 0m00.89s || -0m00.07s | -7.86% 0m00.82s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic | 0m00.82s || +0m00.00s | +0.00% 0m00.82s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.92s || -0m00.10s | -10.86% 0m00.81s | Compilers/Z/CommonSubexpressionEliminationInterp | 0m00.80s || +0m00.01s | +1.25% 0m00.80s | Compilers/Z/FoldTypes | 0m00.76s || +0m00.04s | +5.26% 0m00.80s | Compilers/Z/MapCastByDeBruijn | 0m00.77s || +0m00.03s | +3.89% N/A | Coqprime/PrimalityTest/Root | 0m00.80s || -0m00.80s | -100.00% 0m00.79s | Arithmetic/MontgomeryReduction/Definition | 0m00.71s || +0m00.08s | +11.26% 0m00.79s | Compilers/GeneralizeVarInterp | 0m00.75s || +0m00.04s | +5.33% 0m00.79s | Compilers/MapCastByDeBruijnWf | 0m01.12s || -0m00.33s | -29.46% 0m00.79s | Compilers/Z/CommonSubexpressionEliminationWf | 0m00.79s || +0m00.00s | +0.00% 0m00.79s | Experiments/NewPipeline/CompilersTestCases | 0m01.62s || -0m00.83s | -51.23% 0m00.79s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.78s || +0m00.01s | +1.28% 0m00.78s | Compilers/Z/InlineConstAndOpInterp | 0m00.72s || +0m00.06s | +8.33% 0m00.78s | Compilers/Z/InlineConstAndOpWf | 0m00.80s || -0m00.02s | -2.50% 0m00.78s | Util/ZBounded | 0m00.81s || -0m00.03s | -3.70% 0m00.77s | Compilers/GeneralizeVarWf | 0m00.76s || +0m00.01s | +1.31% 0m00.77s | Compilers/Z/RewriteAddToAdc | 0m00.78s || -0m00.01s | -1.28% 0m00.77s | Util/NUtil | 0m00.84s || -0m00.06s | -8.33% 0m00.76s | Algebra/SubsetoidRing | 0m00.94s || -0m00.17s | -19.14% 0m00.76s | Compilers/Z/InlineConstAndOpByRewriteInterp | 0m00.75s || +0m00.01s | +1.33% N/A | Coqprime/PrimalityTest/Cyclic | 0m00.76s || -0m00.76s | -100.00% 0m00.76s | Util/HList | 0m00.80s || -0m00.04s | -5.00% 0m00.75s | Compilers/Z/Bounds/Interpretation | 0m00.70s || +0m00.05s | +7.14% 0m00.75s | Compilers/Z/InlineConstAndOpByRewriteWf | 0m00.73s || +0m00.02s | +2.73% 0m00.75s | Compilers/Z/InlineWf | 0m00.82s || -0m00.06s | -8.53% 0m00.75s | Compilers/Z/InterpSideConditions | 0m00.55s || +0m00.19s | +36.36% 0m00.75s | Compilers/ZExtended/MapBaseType | 0m00.68s || +0m00.06s | +10.29% 0m00.75s | Util/Loops | 0m00.90s || -0m00.15s | -16.66% 0m00.74s | Compilers/Named/DeadCodeEliminationInterp | 0m00.70s || +0m00.04s | +5.71% 0m00.74s | Compilers/Named/PositiveContext/DefaultsProperties | 0m00.74s || +0m00.00s | +0.00% 0m00.74s | LegacyArithmetic/Interface | 0m01.04s || -0m00.30s | -28.84% 0m00.73s | Compilers/Z/GeneralizeVarInterp | 0m00.70s || +0m00.03s | +4.28% 0m00.73s | Spec/CompleteEdwardsCurve | 0m00.90s || -0m00.17s | -18.88% 0m00.72s | Algebra/Nsatz | 0m00.75s || -0m00.03s | -4.00% 0m00.72s | Compilers/InterpRewriting | 0m00.66s || +0m00.05s | +9.09% 0m00.72s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.70s || +0m00.02s | +2.85% 0m00.71s | Compilers/InterpProofs | 0m00.71s || +0m00.00s | +0.00% 0m00.71s | Compilers/Z/InlineConstAndOp | 0m00.51s || +0m00.19s | +39.21% 0m00.71s | Compilers/Z/Named/RewriteAddToAdc | 0m00.98s || -0m00.27s | -27.55% 0m00.71s | Compilers/ZExtended/Syntax | 0m00.54s || +0m00.16s | +31.48% 0m00.71s | Specific/X25519/C64/CurveParameters | 0m00.50s || +0m00.20s | +41.99% 0m00.70s | Compilers/InterpWf | 0m00.72s || -0m00.02s | -2.77% 0m00.70s | LegacyArithmetic/ArchitectureToZLike | 0m00.84s || -0m00.14s | -16.66% 0m00.70s | Util/ZRange | 0m00.70s || +0m00.00s | +0.00% 0m00.69s | Compilers/InputSyntax | 0m00.74s || -0m00.05s | -6.75% 0m00.69s | Compilers/Z/InlineConstAndOpByRewrite | 0m00.86s || -0m00.17s | -19.76% 0m00.69s | Spec/ModularArithmetic | 0m00.66s || +0m00.02s | +4.54% 0m00.68s | Compilers/CommonSubexpressionEliminationInterp | 0m00.98s || -0m00.29s | -30.61% 0m00.68s | Compilers/InterpWfRel | 0m00.78s || -0m00.09s | -12.82% 0m00.68s | Util/ZUtil/CPS | 0m00.61s || +0m00.07s | +11.47% 0m00.67s | Compilers/Z/Syntax | 0m00.66s || +0m00.01s | +1.51% 0m00.67s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m00.60s || +0m00.07s | +11.66% 0m00.66s | Compilers/Reify | 0m00.60s || +0m00.06s | +10.00% 0m00.66s | Specific/Framework/CurveParameters | 0m00.64s || +0m00.02s | +3.12% 0m00.66s | Util/ZRange/Operations | 0m00.64s || +0m00.02s | +3.12% 0m00.64s | Experiments/PartialEvaluationWithLetIn | 0m00.61s || +0m00.03s | +4.91% 0m00.62s | Algebra/Monoid | 0m00.57s || +0m00.05s | +8.77% 0m00.62s | Compilers/InlineConstAndOp | 0m00.61s || +0m00.01s | +1.63% 0m00.62s | Compilers/InlineConstAndOpByRewriteWf | 0m00.78s || -0m00.16s | -20.51% 0m00.62s | Compilers/Named/WeakListContext | 0m00.62s || +0m00.00s | +0.00% 0m00.62s | Compilers/WfReflectiveGen | 0m00.60s || +0m00.02s | +3.33% 0m00.62s | Compilers/Z/GeneralizeVarWf | 0m00.75s || -0m00.13s | -17.33% 0m00.62s | Specific/Framework/RawCurveParameters | 0m00.58s || +0m00.04s | +6.89% 0m00.61s | Compilers/CommonSubexpressionEliminationDenote | 0m00.41s || +0m00.20s | +48.78% 0m00.61s | Compilers/Named/RegisterAssign | 0m00.60s || +0m00.01s | +1.66% 0m00.61s | Compilers/Z/Inline | 0m00.56s || +0m00.04s | +8.92% 0m00.61s | Util/BoundedWord | 0m00.57s || +0m00.04s | +7.01% 0m00.60s | Compilers/InlineConstAndOpByRewriteInterp | 0m00.68s || -0m00.08s | -11.76% 0m00.60s | Compilers/MapCastByDeBruijn | 0m00.61s || -0m00.01s | -1.63% 0m00.60s | LegacyArithmetic/Pow2Base | 0m00.73s || -0m00.13s | -17.80% 0m00.59s | Compilers/Z/Named/DeadCodeElimination | 0m00.51s || +0m00.07s | +15.68% 0m00.58s | Compilers/Linearize | 0m00.56s || +0m00.01s | +3.57% 0m00.58s | Compilers/Named/MapCast | 0m00.56s || +0m00.01s | +3.57% 0m00.58s | Compilers/Z/Bounds/Pipeline/OutputType | 0m00.61s || -0m00.03s | -4.91% 0m00.58s | Compilers/ZExtended/InlineConstAndOpWf | 0m00.53s || +0m00.04s | +9.43% 0m00.58s | Util/FixedWordSizes | 0m00.53s || +0m00.04s | +9.43% 0m00.58s | Util/ZUtil/Tactics/SimplifyFractionsLe | 0m00.43s || +0m00.14s | +34.88% 0m00.57s | Compilers/GeneralizeVar | 0m00.56s || +0m00.00s | +1.78% 0m00.57s | Compilers/Z/Named/DeadCodeEliminationInterp | 0m00.69s || -0m00.12s | -17.39% N/A | Coqprime/PrimalityTest/Zp | 0m00.57s || -0m00.56s | -100.00% 0m00.57s | Util/ZUtil/MulSplit | 0m00.48s || +0m00.08s | +18.74% 0m00.56s | Compilers/Z/OpInversion | 0m00.56s || +0m00.00s | +0.00% 0m00.56s | Compilers/Z/TypeInversion | 0m00.39s || +0m00.17s | +43.58% 0m00.56s | Specific/NISTP256/AMD64/CurveParameters | 0m00.61s || -0m00.04s | -8.19% 0m00.56s | Util/Decidable/Decidable2Bool | 0m00.81s || -0m00.25s | -30.86% 0m00.55s | Compilers/FilterLive | 0m00.47s || +0m00.08s | +17.02% 0m00.55s | Compilers/Named/IdContext | 0m00.50s || +0m00.05s | +10.00% 0m00.55s | Compilers/ZExtended/InlineConstAndOpByRewrite | 0m00.50s || +0m00.05s | +10.00% 0m00.55s | Compilers/ZExtended/InlineConstAndOpByRewriteWf | 0m00.45s || +0m00.10s | +22.22% 0m00.55s | Compilers/ZExtended/Syntax/Util | 0m00.58s || -0m00.02s | -5.17% 0m00.55s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.38s || +0m00.17s | +44.73% 0m00.54s | Compilers/Inline | 0m00.54s || +0m00.00s | +0.00% 0m00.54s | Compilers/Named/InterpSideConditions | 0m00.40s || +0m00.14s | +35.00% 0m00.54s | Compilers/Named/Wf | 0m00.49s || +0m00.05s | +10.20% 0m00.53s | Compilers/Named/ContextDefinitions | 0m00.55s || -0m00.02s | -3.63% 0m00.53s | Compilers/ZExtended/InlineConstAndOpByRewriteInterp | 0m00.51s || +0m00.02s | +3.92% 0m00.53s | Compilers/ZExtended/InlineConstAndOpInterp | 0m00.58s || -0m00.04s | -8.62% 0m00.53s | Specific/Framework/CurveParametersPackage | 0m00.44s || +0m00.09s | +20.45% 0m00.53s | Util/ZRange/Show | 0m00.56s || -0m00.03s | -5.35% 0m00.53s | Util/ZUtil/Tactics/ZeroBounds | 0m00.40s || +0m00.13s | +32.50% 0m00.52s | Compilers/Named/Context | 0m00.47s || +0m00.05s | +10.63% 0m00.52s | Compilers/Named/CountLets | 0m00.44s || +0m00.08s | +18.18% 0m00.52s | Compilers/Named/GetNames | 0m00.50s || +0m00.02s | +4.00% 0m00.52s | Compilers/Named/InterpretToPHOAS | 0m00.55s || -0m00.03s | -5.45% 0m00.52s | Compilers/Tuple | 0m00.53s || -0m00.01s | -1.88% 0m00.52s | Util/ZUtil/Sgn | 0m00.51s || +0m00.01s | +1.96% 0m00.52s | Util/ZUtil/Tactics/PullPush/Modulo | 0m00.48s || +0m00.04s | +8.33% 0m00.51s | Compilers/CountLets | 0m00.42s || +0m00.09s | +21.42% 0m00.51s | Compilers/Named/ContextOn | 0m00.49s || +0m00.02s | +4.08% 0m00.51s | Util/AdditionChainExponentiation | 0m00.62s || -0m00.10s | -17.74% 0m00.51s | Util/Strings/String | 0m00.58s || -0m00.06s | -12.06% 0m00.51s | Util/ZUtil/Tactics/Ztestbit | 0m00.43s || +0m00.08s | +18.60% 0m00.50s | Compilers/ExprInversion | 0m00.46s || +0m00.03s | +8.69% 0m00.50s | Compilers/FoldTypes | 0m00.51s || -0m00.01s | -1.96% 0m00.50s | Compilers/InlineConstAndOpByRewrite | 0m00.50s || +0m00.00s | +0.00% 0m00.50s | Compilers/Z/InlineInterp | 0m00.59s || -0m00.08s | -15.25% N/A | Coqprime/List/UList | 0m00.50s || -0m00.50s | -100.00% 0m00.49s | Util/ZUtil/Hints/PullPush | 0m00.41s || +0m00.08s | +19.51% 0m00.48s | Compilers/Named/ContextProperties/Tactics | 0m00.53s || -0m00.05s | -9.43% 0m00.48s | Compilers/Z/GeneralizeVar | 0m00.49s || -0m00.01s | -2.04% 0m00.48s | Compilers/ZExtended/InlineConstAndOp | 0m00.52s || -0m00.04s | -7.69% 0m00.48s | Util/ZUtil/Hints/Ztestbit | 0m00.50s || -0m00.02s | -4.00% 0m00.48s | Util/ZUtil/ZSimplify/Core | 0m00.44s || +0m00.03s | +9.09% 0m00.48s | Util/ZUtil/Zselect | 0m00.44s || +0m00.03s | +9.09% 0m00.47s | Compilers/InterpByIso | 0m00.47s || +0m00.00s | +0.00% 0m00.47s | Util/IdfunWithAlt | 0m00.59s || -0m00.12s | -20.33% 0m00.47s | Util/ZUtil/Hints/ZArith | 0m00.49s || -0m00.02s | -4.08% 0m00.46s | Compilers/Named/DeadCodeElimination | 0m00.58s || -0m00.11s | -20.68% N/A | Coqprime/List/Permutation | 0m00.46s || -0m00.46s | -100.00% 0m00.46s | Experiments/NewPipeline/UnderLets | 0m00.72s || -0m00.25s | -36.11% 0m00.46s | Util/Sum | 0m00.44s || +0m00.02s | +4.54% 0m00.45s | Compilers/Named/SmartMap | 0m00.54s || -0m00.09s | -16.66% 0m00.45s | Util/ZUtil/Z2Nat | 0m00.41s || +0m00.04s | +9.75% 0m00.44s | Compilers/MapBaseType | 0m00.46s || -0m00.02s | -4.34% 0m00.44s | Util/Strings/HexString | 0m00.44s || +0m00.00s | +0.00% 0m00.44s | Util/ZUtil/Div/Bootstrap | 0m00.50s || -0m00.06s | -12.00% 0m00.44s | Util/ZUtil/Hints/Core | 0m00.52s || -0m00.08s | -15.38% 0m00.43s | Compilers/Named/EstablishLiveness | 0m00.38s || +0m00.04s | +13.15% 0m00.43s | Compilers/Named/ExprInversion | 0m00.56s || -0m00.13s | -23.21% 0m00.43s | Compilers/StripExpr | 0m00.50s || -0m00.07s | -14.00% 0m00.43s | Util/ZUtil/Tactics/LtbToLt | 0m00.54s || -0m00.11s | -20.37% 0m00.42s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Definition | 0m00.43s || -0m00.01s | -2.32% 0m00.42s | Util/ZUtil/Hints | 0m00.40s || +0m00.01s | +4.99% 0m00.42s | Util/ZUtil/Le | 0m00.43s || -0m00.01s | -2.32% 0m00.42s | Util/ZUtil/ZSimplify | 0m00.28s || +0m00.13s | +49.99% 0m00.42s | bbv/Nomega | 0m00.45s || -0m00.03s | -6.66% 0m00.41s | Util/ZUtil/Sorting | 0m00.47s || -0m00.06s | -12.76% 0m00.41s | Util/ZUtil/Tactics/PrimeBound | 0m00.36s || +0m00.04s | +13.88% 0m00.41s | bbv/HexNotationWord | 0m00.45s || -0m00.04s | -8.88% 0m00.40s | Compilers/Named/PositiveContext | 0m00.59s || -0m00.18s | -32.20% 0m00.40s | Compilers/Named/Syntax | 0m00.50s || -0m00.09s | -19.99% N/A | Coqprime/List/ListAux | 0m00.40s || -0m00.40s | -100.00% 0m00.40s | Util/SideConditions/RingPackage | 0m00.37s || +0m00.03s | +8.10% 0m00.40s | Util/ZUtil/Tactics/DivModToQuotRem | 0m00.38s || +0m00.02s | +5.26% 0m00.40s | Util/ZUtil/Tactics/LinearSubstitute | 0m00.42s || -0m00.01s | -4.76% 0m00.39s | Compilers/Equality | 0m00.38s || +0m00.01s | +2.63% 0m00.39s | Util/SideConditions/Autosolve | 0m00.28s || +0m00.10s | +39.28% 0m00.39s | Util/SideConditions/ModInvPackage | 0m00.41s || -0m00.01s | -4.87% 0m00.39s | bbv/HexNotation | 0m00.38s || +0m00.01s | +2.63% N/A | Coqprime/PrimalityTest/Lagrange | 0m00.38s || -0m00.38s | -100.00% 0m00.38s | Specific/NISTP256/AMD128/CurveParameters | 0m00.58s || -0m00.19s | -34.48% 0m00.38s | Util/ZUtil/AddModulo | 0m00.28s || +0m00.09s | +35.71% 0m00.38s | Util/ZUtil/Modulo/Bootstrap | 0m00.40s || -0m00.02s | -5.00% 0m00.38s | Util/ZUtil/Tactics/CompareToSgn | 0m00.43s || -0m00.04s | -11.62% 0m00.38s | Util/ZUtil/Tactics/DivideExistsMul | 0m00.38s || +0m00.00s | +0.00% 0m00.38s | bbv/WordScope | 0m00.40s || -0m00.02s | -5.00% 0m00.37s | Algebra/Hierarchy | 0m00.40s || -0m00.03s | -7.50% 0m00.37s | Compilers/Named/Compile | 0m00.50s || -0m00.13s | -26.00% N/A | Coqprime/List/ZProgression | 0m00.37s || -0m00.37s | -100.00% N/A | Coqprime/PrimalityTest/IGroup | 0m00.37s || -0m00.37s | -100.00% 0m00.37s | Util/ZUtil/Ge | 0m00.33s || +0m00.03s | +12.12% 0m00.37s | Util/ZUtil/Land | 0m00.43s || -0m00.06s | -13.95% 0m00.36s | Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition | 0m00.42s || -0m00.06s | -14.28% 0m00.36s | Compilers/Named/MapType | 0m00.33s || +0m00.02s | +9.09% 0m00.36s | Compilers/Named/PositiveContext/Defaults | 0m00.57s || -0m00.20s | -36.84% 0m00.36s | Util/Strings/OctalString | 0m00.33s || +0m00.02s | +9.09% 0m00.36s | Util/ZUtil/Definitions | 0m00.40s || -0m00.04s | -10.00% 0m00.36s | Util/ZUtil/Tactics/PullPush | 0m00.39s || -0m00.03s | -7.69% 0m00.36s | Util/ZUtil/Tactics/ReplaceNegWithPos | 0m00.33s || +0m00.02s | +9.09% 0m00.36s | bbv/BinNotation | 0m00.37s || -0m00.01s | -2.70% N/A | Coqprime/PrimalityTest/Euler | 0m00.35s || -0m00.35s | -100.00% 0m00.35s | Spec/MxDH | 0m00.39s || -0m00.04s | -10.25% 0m00.35s | Util/Decidable/Bool2Prop | 0m00.22s || +0m00.12s | +59.09% 0m00.35s | Util/ZUtil/Tactics | 0m00.48s || -0m00.13s | -27.08% 0m00.35s | Util/ZUtil/Tactics/PeelLe | 0m00.44s || -0m00.09s | -20.45% 0m00.35s | Util/ZUtil/Tactics/SplitMinMax | 0m00.35s || +0m00.00s | +0.00% 0m00.34s | Util/Option | 0m00.31s || +0m00.03s | +9.67% 0m00.34s | Util/ZUtil/ModInv | 0m00.38s || -0m00.03s | -10.52% 0m00.34s | bbv/BinNotationZ | 0m00.34s || +0m00.00s | +0.00% 0m00.34s | bbv/HexNotationZ | 0m00.37s || -0m00.02s | -8.10% 0m00.34s | bbv/NLib | 0m00.42s || -0m00.07s | -19.04% 0m00.33s | Util/Strings/Show | 0m00.45s || -0m00.12s | -26.66% N/A | Coqprime/List/Iterator | 0m00.31s || -0m00.31s | -100.00% 0m00.31s | Util/PointedProp | 0m00.30s || +0m00.01s | +3.33% 0m00.29s | Util/LetInMonad | 0m00.29s || +0m00.00s | +0.00% 0m00.28s | Compilers/EtaInterp | 0m00.34s || -0m00.06s | -17.64% 0m00.28s | Compilers/InSet/TypeifyInterp | 0m00.18s || +0m00.10s | +55.55% 0m00.28s | Util/Strings/BinaryString | 0m00.32s || -0m00.03s | -12.49% 0m00.28s | Util/Strings/Equality | 0m00.29s || -0m00.00s | -3.44% N/A | Coqprime/PrimalityTest/FGroup | 0m00.27s || -0m00.27s | -100.00% 0m00.27s | Util/Strings/Ascii | 0m00.33s || -0m00.06s | -18.18% 0m00.27s | Util/Strings/Decimal | 0m00.26s || +0m00.01s | +3.84% N/A | Coqprime/N/NatAux | 0m00.26s || -0m00.26s | -100.00% 0m00.26s | Util/ParseTaps | 0m00.29s || -0m00.02s | -10.34% 0m00.25s | Util/SideConditions/ReductionPackages | 0m00.24s || +0m00.01s | +4.16% 0m00.24s | Util/ZUtil/Notations | 0m00.29s || -0m00.04s | -17.24% 0m00.20s | Compilers/Conversion | 0m00.12s || +0m00.08s | +66.66% 0m00.20s | Util/ListUtil/FoldBool | 0m00.20s || +0m00.00s | +0.00% 0m00.19s | Compilers/Named/NameUtil | 0m00.18s || +0m00.01s | +5.55% 0m00.19s | Compilers/Wf | 0m00.20s || -0m00.01s | -5.00% 0m00.18s | Specific/Framework/Packages | 0m00.17s || +0m00.00s | +5.88% 0m00.18s | Util/PrimitiveProd | 0m00.19s || -0m00.01s | -5.26% 0m00.18s | Util/Relations | 0m00.14s || +0m00.03s | +28.57% 0m00.18s | bbv/DepEq | 0m00.22s || -0m00.04s | -18.18% 0m00.17s | Util/ListUtil/Forall | 0m00.18s || -0m00.00s | -5.55% 0m00.17s | Util/Sigma | 0m00.14s || +0m00.03s | +21.42% 0m00.16s | Compilers/RewriterWf | 0m00.16s || +0m00.00s | +0.00% 0m00.16s | Util/TagList | 0m00.20s || -0m00.04s | -20.00% 0m00.14s | Compilers/RewriterInterp | 0m00.12s || +0m00.02s | +16.66% 0m00.14s | Compilers/TypeInversion | 0m00.14s || +0m00.00s | +0.00% 0m00.12s | Compilers/InSet/Syntax | 0m00.09s || +0m00.03s | +33.33% 0m00.12s | Compilers/InterpSideConditions | 0m00.07s || +0m00.04s | +71.42% 0m00.12s | Util/AutoRewrite | 0m00.09s || +0m00.03s | +33.33% 0m00.12s | Util/Equality | 0m00.13s || -0m00.01s | -7.69% 0m00.12s | Util/PrimitiveHList | 0m00.14s || -0m00.02s | -14.28% 0m00.12s | Util/Prod | 0m00.18s || -0m00.06s | -33.33% 0m00.11s | Compilers/RenameBinders | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Compilers/Rewriter | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Compilers/TypeUtil | 0m00.08s || +0m00.03s | +37.50% 0m00.11s | Util/HProp | 0m00.10s || +0m00.00s | +9.99% 0m00.11s | Util/IffT | 0m00.05s || +0m00.06s | +120.00% 0m00.11s | Util/Tactics | 0m00.08s || +0m00.03s | +37.50% 0m00.10s | Compilers/Eta | 0m00.11s || -0m00.00s | -9.09% 0m00.10s | Compilers/Syntax | 0m00.13s || -0m00.03s | -23.07% 0m00.10s | Util/Bool | 0m00.08s || +0m00.02s | +25.00% 0m00.10s | Util/Isomorphism | 0m00.12s || -0m00.01s | -16.66% 0m00.10s | Util/LetIn | 0m00.09s || +0m00.01s | +11.11% 0m00.10s | Util/Sumbool | 0m00.09s || +0m00.01s | +11.11% 0m00.10s | Util/Tactics/MoveLetIn | 0m00.09s || +0m00.01s | +11.11% 0m00.10s | Util/Tactics/Revert | 0m00.07s || +0m00.03s | +42.85% 0m00.10s | Util/Tower | 0m00.10s || +0m00.00s | +0.00% 0m00.10s | bbv/DepEqNat | 0m00.06s || +0m00.04s | +66.66% 0m00.09s | Compilers/InSet/Typeify | 0m00.12s || -0m00.03s | -25.00% 0m00.09s | Util/Tactics/Contains | 0m00.04s || +0m00.05s | +124.99% 0m00.09s | Util/Tactics/ConvoyDestruct | 0m00.05s || +0m00.03s | +79.99% 0m00.09s | Util/Tactics/DestructHead | 0m00.10s || -0m00.01s | -10.00% 0m00.09s | Util/Tactics/ETransitivity | 0m00.08s || +0m00.00s | +12.49% 0m00.09s | Util/Tactics/SpecializeBy | 0m00.06s || +0m00.03s | +50.00% 0m00.08s | Compilers/Intros | 0m00.08s || +0m00.00s | +0.00% 0m00.08s | Compilers/Map | 0m00.10s || -0m00.02s | -20.00% 0m00.08s | Util/Bool/IsTrue | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Util/ErrorT | 0m00.07s || +0m00.00s | +14.28% 0m00.08s | Util/Logic | 0m00.08s || +0m00.00s | +0.00% 0m00.08s | Util/Pointed | 0m00.08s || +0m00.00s | +0.00% 0m00.08s | Util/Pos | 0m00.04s || +0m00.04s | +100.00% 0m00.08s | Util/SideConditions/AdmitPackage | 0m00.08s || +0m00.00s | +0.00% 0m00.08s | Util/Sigma/Lift | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Util/Tactics/CacheTerm | 0m00.08s || +0m00.00s | +0.00% 0m00.08s | Util/Tactics/DebugPrint | 0m00.10s || -0m00.02s | -20.00% 0m00.08s | Util/Tactics/DestructTrivial | 0m00.05s || +0m00.03s | +60.00% 0m00.08s | Util/Tactics/GetGoal | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Util/Tactics/Head | 0m00.07s || +0m00.00s | +14.28% 0m00.08s | Util/Tactics/RewriteHyp | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Util/Tactics/SubstEvars | 0m00.07s || +0m00.00s | +14.28% 0m00.08s | Util/Tactics/UnifyAbstractReflexivity | 0m00.06s || +0m00.02s | +33.33% 0m00.08s | Util/Tactics/VM | 0m00.08s || +0m00.00s | +0.00% 0m00.07s | LegacyArithmetic/VerdiTactics | 0m00.10s || -0m00.03s | -30.00% 0m00.07s | Util/Bool/Equality | 0m00.07s || +0m00.00s | +0.00% 0m00.07s | Util/CPSNotations | 0m00.09s || -0m00.01s | -22.22% 0m00.07s | Util/Logic/ImplAnd | 0m00.07s || +0m00.00s | +0.00% 0m00.07s | Util/Tactics/BreakMatch | 0m00.06s || +0m00.01s | +16.66% 0m00.07s | Util/Tactics/DestructHyps | 0m00.07s || +0m00.00s | +0.00% 0m00.07s | Util/Tactics/DoWithHyp | 0m00.09s || -0m00.01s | -22.22% 0m00.07s | Util/Tactics/ESpecialize | 0m00.08s || -0m00.00s | -12.49% 0m00.07s | Util/Tactics/HeadUnderBinders | 0m00.06s || +0m00.01s | +16.66% 0m00.07s | Util/Tactics/Not | 0m00.07s || +0m00.00s | +0.00% 0m00.07s | Util/Tactics/PoseTermWithName | 0m00.06s || +0m00.01s | +16.66% 0m00.07s | Util/Tactics/PrintContext | 0m00.06s || +0m00.01s | +16.66% 0m00.07s | Util/Tactics/SetEvars | 0m00.05s || +0m00.02s | +40.00% 0m00.07s | Util/Tactics/SpecializeAllWays | 0m00.08s || -0m00.00s | -12.49% 0m00.07s | Util/Tactics/SplitInContext | 0m00.07s || +0m00.00s | +0.00% 0m00.07s | Util/Tactics/TransparentAssert | 0m00.06s || +0m00.01s | +16.66% 0m00.07s | Util/Unit | 0m00.06s || +0m00.01s | +16.66% 0m00.06s | Util/Curry | 0m00.08s || -0m00.02s | -25.00% 0m00.06s | Util/DefaultedTypes | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Util/FixCoqMistakes | 0m00.09s || -0m00.03s | -33.33% 0m00.06s | Util/GlobalSettings | 0m00.12s || -0m00.06s | -50.00% 0m00.06s | Util/SideConditions/CorePackages | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Util/Sigma/Associativity | 0m00.08s || -0m00.02s | -25.00% 0m00.06s | Util/Sigma/MapProjections | 0m00.05s || +0m00.00s | +19.99% 0m00.06s | Util/Tactics/ClearDuplicates | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Util/Tactics/ClearbodyAll | 0m00.07s || -0m00.01s | -14.28% 0m00.06s | Util/Tactics/EvarExists | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Util/Tactics/Forward | 0m00.04s || +0m00.01s | +49.99% 0m00.06s | Util/Tactics/OnSubterms | 0m00.04s || +0m00.01s | +49.99% 0m00.06s | Util/Tactics/RunTacticAsConstr | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Util/Tactics/SideConditionsBeforeToAfter | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Util/Tactics/SimplifyProjections | 0m00.08s || -0m00.02s | -25.00% 0m00.06s | Util/Tactics/SubstLet | 0m00.06s || +0m00.00s | +0.00% 0m00.06s | Util/Tactics/Test | 0m00.07s || -0m00.01s | -14.28% 0m00.05s | Util/ChangeInAll | 0m00.06s || -0m00.00s | -16.66% 0m00.05s | Util/Notations | 0m00.08s || -0m00.03s | -37.50% 0m00.05s | Util/Tactics/SimplifyRepeatedIfs | 0m00.06s || -0m00.00s | -16.66% 0m00.05s | Util/Tactics/UnfoldArg | 0m00.08s || -0m00.03s | -37.50% 0m00.05s | Util/Tactics/UniquePose | 0m00.06s || -0m00.00s | -16.66% 0m00.04s | Util/OptionList | 0m00.09s || -0m00.05s | -55.55% 0m00.04s | Util/Tactics/ChangeInAll | 0m00.08s || -0m00.04s | -50.00% 0m00.04s | Util/Tactics/SetoidSubst | 0m00.05s || -0m00.01s | -20.00% 0m00.03s | Util/Tactics/ClearAll | 0m00.06s || -0m00.03s | -50.00% N/A | Coqprime/Tactic/Tactic | 0m00.02s || -0m00.02s | -100.00%
* Support reification of firstn, skipnGravatar Jason Gross2018-07-18
|
* Make Z.modinv run on wf proofsGravatar Jason Gross2018-07-18
| | | | | | | This version extracts better. The previous version was computing 2^256 as a nat before running. We also reduce the fuel to a saner amount, for better performance in cbv/vm/native.
* vm_compute in peel_interp_appGravatar Jason Gross2018-07-18
| | | | | | | | | | | | | | | | With some help from @ppedrot in tracking things down. C.f. https://github.com/mit-plv/fiat-crypto/pull/394#issuecomment-406010106 After | File Name | Before || Change | % Change ------------------------------------------------------------------------------------------------ 8m48.43s | Total | 9m07.60s || -0m19.16s | -3.50% ------------------------------------------------------------------------------------------------ 5m35.98s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m45.63s || -0m09.64s | -2.79% 1m29.20s | Experiments/NewPipeline/Toplevel2 | 1m38.67s || -0m09.46s | -9.59% 1m39.78s | Experiments/NewPipeline/Toplevel1 | 1m39.77s || +0m00.00s | +0.01% 0m01.18s | Experiments/NewPipeline/CLI | 0m01.31s || -0m00.13s | -9.92% 0m01.16s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.09s || +0m00.06s | +6.42% 0m01.14s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.14s || +0m00.00s | +0.00%
* Thunk nat_rect for better perf, list_{rect=>case}Gravatar Jason Gross2018-07-17
| | | | | | | | | | | | | | | | See https://github.com/coq/coq/issues/8019#issuecomment-405743213 After | File Name | Before || Change | % Change ------------------------------------------------------------------------------------------------ 8m18.36s | Total | 9m46.11s || -1m27.74s | -14.97% ------------------------------------------------------------------------------------------------ 4m51.13s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m46.00s || -0m54.87s | -15.85% 1m20.26s | Experiments/NewPipeline/Toplevel2 | 1m56.98s || -0m36.71s | -31.38% 1m21.02s | Experiments/NewPipeline/Toplevel1 | 1m18.08s || +0m02.93s | +3.76% 0m42.56s | Experiments/NewPipeline/Arithmetic | 0m41.71s || +0m00.85s | +2.03% 0m01.15s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.09s || +0m00.05s | +5.50% 0m01.14s | Experiments/NewPipeline/CLI | 0m01.18s || -0m00.04s | -3.38% 0m01.11s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.08s || +0m00.03s | +2.77%
* Handle Z.pow in push_Zmod tacticGravatar Jason Gross2018-07-17
|
* Remove a lemma that's been moved to NatUtilGravatar Jason Gross2018-07-17
|
* Handle Z.pow in {push,pull}_ZmodGravatar Jason Gross2018-07-17
|
* Add minor lemmas to utilGravatar Jason Gross2018-07-17
|
* Allow reification of nat_rect (fun _ => _ -> _)Gravatar Jason Gross2018-07-15
| | | | | We now support reification of nat_rect returning an arrow. This is needed for montgomery.
* Add a stronger version of eval_reduceGravatar Jason Gross2018-07-14
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 02:50:02 +0000