aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Collapse)AuthorAge
* Add interp_reify_and_let_binds_baseGravatar Jason Gross2018-10-25
|
* Add interp_reify_as_interpGravatar Jason Gross2018-10-24
|
* Add GallinaReify.reify_as_interpGravatar Jason Gross2018-10-24
|
* Add rawexpr_equiv_expr_to_type_of_rawexprGravatar Jason Gross2018-10-23
|
* Add a horribly manual proof of app_forall_vars_under_forall_vars_relation1Gravatar Jason Gross2018-10-23
| | | | | I guess I still haven't figured out how to automate reasoning about transport across equality.
* Add some equality lemmas about Positive{Map,Set}Gravatar Jason Gross2018-10-23
|
* Add under_with_unification_resultT'_relation1_gen_alwaysGravatar Jason Gross2018-10-23
|
* Add related1_app_type_of_list_under_type_of_list_relation1_cpsGravatar Jason Gross2018-10-23
|
* Update rewriter correctness conditionGravatar Jason Gross2018-10-23
| | | | | | Now we don't need any relation on values when going under binders to get the cps-id condition. This seems essential to getting the rewriter interp correctness proofs to work.
* Tactic-in-term: ensuring same scope for all occurrences of a notation variable.Gravatar Hugo Herbelin2018-10-23
|
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
| | | | | | | | | | | | | | Currently, there aren't any interesting rewrite rules in the lists, but this allows us to move rewrite rules that depend on cast behavior to after bounds analysis. Unfortunately, it takes a lot of time to build from Rewriter.v to the standalone binaries, so it'll probably make sense to inline some stuff for more rapid development. Note that we also now have a tactic that does all of the evaluation for rewrite rules (assuming the right [Arguments] commands have been issued).
* Minor changes to rewriterGravatar Jason Gross2018-10-14
| | | | | These changes make it easier to prove things about the interpretation of the rewriter.
* Guarantee that casting always returns inrangeGravatar Jason Gross2018-10-12
| | | | | | | | | | | | | | We fuse the bounds relaxation pass with the abstract interpretation pass by folding bounds relaxation into the annotation method. This allows us to not need any particular assumptions about what happens when you cast outside the range. We can therefore now guarantee that the output of casting is always bounded by the given range (rather, by the normalized version of the range), which will be required to take advantage of bounds information in the rewriter (because otherwise we're not guaranteed that casting something to within a range actually outputs something within that range).
* Add some zrange lemmasGravatar Jason Gross2018-10-11
|
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
|
* Add interp-correctness condition for rewriterGravatar Jason Gross2018-10-11
| | | | | | | | | | | | The NBE-rewrite rules are proven correct. The arith and fancy rewrite rules are reduced to lemmas about Z, most of which are inconsistent (and therefore indicate rewrite rules which are missing side-conditions). One bad rewrite rule was found in this process, and corrected in 0842563b23f8d780f4ff1080d7620fc3f368191f The next step after this will be using the rewrite rule correctness to prove the rewriter correct.
* Export more tactics in Tactics.vGravatar Jason Gross2018-10-10
|
* Rename [normalize_commutative_identifier] file to match tactic nameGravatar Jason Gross2018-10-10
|
* Add [normalize_commutative_identifier] tacticGravatar Jason Gross2018-10-10
|
* Add some natutil and listutil lemmasGravatar Jason Gross2018-10-10
|
* Restore Redirect in comment blocksGravatar Jason Gross2018-10-09
| | | | | | They were there for a reason, which is that the embedded python script has support for automatically picking up the files in /tmp, so it's nice to be able to just uncomment the block of code to get the files in /tmp
* Remove [Redirect] to absolute pathsGravatar Andres Erbsen2018-10-09
| | | | | | | | | | | | find . -name '*.v' -print0 | xargs -0 sed -i 's/^\(\s*\)\(Redirect.*\.\)$/\1(* \2 *)/g' When on a shared machine, the first user would create /tmp/outfile and then the build would fail for the second user because the file already exists and is owned by somebody else. https://github.com/coq/coq/issues/8649 tested ok on top of c4e09295f5a8e10ea1957711da0e79661177e8a6
* Fix a bad rewrite ruleGravatar Jason Gross2018-10-09
| | | | Apparently (luckily) it never triggered
* Add map_update_nth_extGravatar Jason Gross2018-10-09
|
* Add under_with_unification_resultT_relation_heteroGravatar Jason Gross2018-10-09
| | | | Might not be the best name...
* Use [reify_list] in [smart_Literal]Gravatar Jason Gross2018-10-09
| | | | | This allows slightly easier proofs, by de-duplicating the logic of reifying lists.
* Add ListUtil.ForallInGravatar Jason Gross2018-10-09
|
* Compatibility with Coq PR#8457Gravatar Frédéric Besson2018-10-04
| | | | Based on hints from @andres-erbsen
* Add some more lemmas about generated stuffGravatar Jason Gross2018-10-02
|
* Adapt to Coq's PR#8555Gravatar Maxime Dénès2018-10-02
|
* Add more gen ident proofsGravatar Jason Gross2018-10-01
|
* Add pattern.ident.to_typedGravatar Jason Gross2018-10-01
|
* Add a few rewriter definitionsGravatar Jason Gross2018-10-01
|
* Support type variables in patterns in the rewriterGravatar Jason Gross2018-09-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This paves the way for writing down interpretation proofs for the rewriter by writing down "default interpretations". Otherwise, e.g., there was not enough type information to write down any good interpretation for [map fst nil] (which would bind no type variables in the previous veresion). Unfortunately the rewriter itself got a bit slower (though the proof of rewrite-rule-correctness got a bit faster). After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 24m05.07s | Total | 24m08.92s || -0m03.85s | -0.26% -------------------------------------------------------------------------------------------------------------------- 1m13.28s | Experiments/NewPipeline/RewriterRulesGood.vo | 3m58.20s || -2m44.91s | -69.23% 2m50.62s | Experiments/NewPipeline/Rewriter.vo | 1m12.64s || +1m37.98s | +134.88% 1m45.22s | Experiments/NewPipeline/RewriterWf2.vo | 1m13.64s || +0m31.57s | +42.88% 0m16.82s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo | 0m11.46s || +0m05.35s | +46.77% 0m08.04s | Experiments/NewPipeline/RewriterWf1.vo | 0m04.52s || +0m03.51s | +77.87% 6m07.90s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m05.01s || +0m02.88s | +0.79% 0m39.74s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.09s || +0m02.64s | +7.14% 0m37.83s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m34.94s || +0m02.89s | +8.27% 0m26.05s | p384_32.c | 0m23.72s || +0m02.33s | +9.82% 0m23.37s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m21.01s || +0m02.35s | +11.23% 0m21.30s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m19.02s || +0m02.28s | +11.98% 0m16.22s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m14.01s || +0m02.20s | +15.77% 4m34.84s | Experiments/NewPipeline/Toplevel1.vo | 4m36.15s || -0m01.30s | -0.47% 1m42.79s | Experiments/NewPipeline/Toplevel2.vo | 1m44.07s || -0m01.28s | -1.22% 0m40.07s | p521_32.c | 0m38.58s || +0m01.49s | +3.86% 0m33.52s | p521_64.c | 0m32.04s || +0m01.48s | +4.61% 0m12.80s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m11.12s || +0m01.68s | +15.10% 0m09.01s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.76s || +0m00.25s | +2.85% 0m08.80s | p384_64.c | 0m08.49s || +0m00.31s | +3.65% 0m07.65s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo | 0m07.83s || -0m00.17s | -2.29% 0m05.92s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.40s || +0m00.51s | +9.62% 0m05.59s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.61s || -0m00.02s | -0.35% 0m04.40s | secp256k1_32.c | 0m03.95s || +0m00.45s | +11.39% 0m04.27s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m03.98s || +0m00.28s | +7.28% 0m04.27s | p256_32.c | 0m03.76s || +0m00.50s | +13.56% 0m04.23s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.14s || +0m00.09s | +2.17% 0m03.39s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.35s || +0m00.04s | +1.19% 0m02.56s | p224_32.c | 0m02.24s || +0m00.31s | +14.28% 0m02.37s | curve25519_32.c | 0m02.18s || +0m00.18s | +8.71% 0m01.66s | p224_64.c | 0m01.66s || +0m00.00s | +0.00% 0m01.64s | p256_64.c | 0m01.53s || +0m00.10s | +7.18% 0m01.60s | secp256k1_64.c | 0m01.50s || +0m00.10s | +6.66% 0m01.52s | curve25519_64.c | 0m01.51s || +0m00.01s | +0.66% 0m01.38s | Experiments/NewPipeline/CLI.vo | 0m01.37s || +0m00.00s | +0.72% 0m01.27s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.16s || +0m00.11s | +9.48% 0m01.19s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.29s || -0m00.10s | -7.75% 0m01.05s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.06s || -0m00.01s | -0.94% 0m00.90s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.94s || -0m00.03s | -4.25%
* Fix and prove bounds for fancymachine operationsGravatar jadep2018-09-28
|
* Add some option bind lemmasGravatar Jason Gross2018-09-27
|
* Clean up type_beq_to_eq a bitGravatar Jason Gross2018-09-27
|
* Add more reflect tacticsGravatar Jason Gross2018-09-27
|
* Add some lemmas about Bool.reflectGravatar Jason Gross2018-09-27
|
* Add destruct_head_{False,Empty_set}Gravatar Jason Gross2018-09-27
|
* Add some Proper lemmas for Option.bindGravatar Jason Gross2018-09-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Timing diff is probably mostly noise. After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 68m18.12s | Total | 69m59.63s || -1m41.51s | -2.41% -------------------------------------------------------------------------------------------------------------------- 3m42.71s | Curves/Montgomery/XZProofs.vo | 4m08.00s || -0m25.28s | -10.19% 1m22.09s | Experiments/NewPipeline/Arithmetic.vo | 1m37.69s || -0m15.59s | -15.96% 0m51.83s | Demo.vo | 1m04.94s || -0m13.10s | -20.18% 8m50.46s | Experiments/SimplyTypedArithmetic.vo | 8m59.22s || -0m08.75s | -1.62% 0m36.08s | Experiments/NewPipeline/LanguageInversion.vo | 0m40.70s || -0m04.62s | -11.35% 0m27.04s | Primitives/EdDSARepChange.vo | 0m31.77s || -0m04.73s | -14.88% 0m12.16s | Primitives/MxDHRepChange.vo | 0m16.64s || -0m04.48s | -26.92% 4m08.54s | Experiments/NewPipeline/RewriterRulesGood.vo | 4m11.60s || -0m03.06s | -1.21% 0m36.33s | Spec/Ed25519.vo | 0m39.60s || -0m03.27s | -8.25% 0m19.06s | Curves/Edwards/XYZT/Basic.vo | 0m22.22s || -0m03.16s | -14.22% 0m16.06s | Curves/Edwards/AffineProofs.vo | 0m19.36s || -0m03.30s | -17.04% 4m44.06s | Experiments/NewPipeline/Toplevel1.vo | 4m42.03s || +0m02.03s | +0.71% 0m08.29s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo | 0m10.95s || -0m02.66s | -24.29% 6m03.41s | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo | 6m04.65s || -0m01.23s | -0.34% 1m21.61s | Compilers/Named/MapCastInterp.vo | 1m22.75s || -0m01.14s | -1.37% 1m20.35s | Specific/X2448/Karatsuba/C64/femul.vo | 1m18.81s || +0m01.53s | +1.95% 1m17.46s | Experiments/NewPipeline/Rewriter.vo | 1m18.83s || -0m01.36s | -1.73% 0m49.98s | Compilers/Z/Named/RewriteAddToAdcInterp.vo | 0m51.46s || -0m01.48s | -2.87% 0m40.08s | Experiments/NewPipeline/AbstractInterpretationWf.vo | 0m41.56s || -0m01.48s | -3.56% 0m18.14s | Specific/X25519/C64/fesquare.vo | 0m17.02s || +0m01.12s | +6.58% 0m14.21s | Specific/X25519/C64/fesub.vo | 0m13.13s || +0m01.08s | +8.22% 2m09.85s | Specific/X25519/C64/ladderstep.vo | 2m09.46s || +0m00.38s | +0.30% 1m53.52s | Specific/NISTP256/AMD64/femul.vo | 1m52.76s || +0m00.76s | +0.67% 1m43.25s | Experiments/NewPipeline/Toplevel2.vo | 1m43.48s || -0m00.22s | -0.22% 1m23.40s | Experiments/NewPipeline/RewriterWf2.vo | 1m23.42s || -0m00.01s | -0.02% 1m00.91s | Specific/X25519/C32/femul.vo | 1m00.02s || +0m00.88s | +1.48% 0m50.13s | Compilers/Z/ArithmeticSimplifierInterp.vo | 0m50.62s || -0m00.48s | -0.96% 0m44.22s | Specific/X25519/C32/fesquare.vo | 0m43.65s || +0m00.57s | +1.30% 0m41.83s | Arithmetic/Karatsuba.vo | 0m42.24s || -0m00.41s | -0.97% 0m36.88s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.49s || -0m00.60s | -1.62% 0m34.72s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m35.07s || -0m00.35s | -0.99% 0m34.10s | Specific/X25519/C32/freeze.vo | 0m33.90s || +0m00.20s | +0.58% 0m31.88s | Compilers/Z/ArithmeticSimplifierWf.vo | 0m32.83s || -0m00.94s | -2.89% 0m29.11s | Compilers/CommonSubexpressionEliminationWf.vo | 0m29.30s || -0m00.19s | -0.64% 0m27.43s | Specific/NISTP256/AMD128/femul.vo | 0m27.71s || -0m00.28s | -1.01% 0m26.28s | Experiments/NewPipeline/UnderLetsProofs.vo | 0m26.40s || -0m00.11s | -0.45% 0m25.69s | Specific/X25519/C32/fecarry.vo | 0m25.42s || +0m00.26s | +1.06% 0m23.18s | Experiments/NewPipeline/AbstractInterpretationZRangeProofs.vo | 0m23.52s || -0m00.33s | -1.44% 0m22.69s | Experiments/NewPipeline/LanguageWf.vo | 0m23.42s || -0m00.73s | -3.11% 0m21.49s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.67s || +0m00.81s | +3.96% 0m21.40s | Specific/X25519/C32/fesub.vo | 0m21.31s || +0m00.08s | +0.42% 0m21.31s | Arithmetic/Core.vo | 0m21.44s || -0m00.13s | -0.60% 0m21.06s | Specific/X25519/C64/femul.vo | 0m20.44s || +0m00.61s | +3.03% 0m20.85s | Specific/NISTP256/AMD64/fesub.vo | 0m20.95s || -0m00.09s | -0.47% 0m19.43s | Specific/X25519/C32/Synthesis.vo | 0m19.62s || -0m00.19s | -0.96% 0m19.30s | Specific/X25519/C32/feadd.vo | 0m19.32s || -0m00.01s | -0.10% 0m19.04s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.91s || +0m00.12s | +0.68% 0m19.02s | Experiments/NewPipeline/AbstractInterpretationProofs.vo | 0m19.52s || -0m00.50s | -2.56% 0m18.98s | Specific/NISTP256/AMD64/feadd.vo | 0m19.82s || -0m00.83s | -4.23% 0m18.04s | Compilers/Named/MapCastWf.vo | 0m18.28s || -0m00.24s | -1.31% 0m18.02s | Compilers/Z/CNotations.vo | 0m18.45s || -0m00.42s | -2.33% 0m17.41s | Specific/X25519/C64/freeze.vo | 0m17.68s || -0m00.26s | -1.52% 0m16.00s | Specific/NISTP256/AMD64/feopp.vo | 0m15.60s || +0m00.40s | +2.56% 0m15.61s | Compilers/Named/ContextProperties/SmartMap.vo | 0m16.10s || -0m00.49s | -3.04% 0m15.22s | Compilers/Named/ContextProperties/NameUtil.vo | 0m15.78s || -0m00.55s | -3.54% 0m14.91s | Specific/NISTP256/AMD128/fesub.vo | 0m15.34s || -0m00.42s | -2.80% 0m14.78s | Specific/NISTP256/AMD128/feadd.vo | 0m14.79s || -0m00.00s | -0.06% 0m14.41s | Specific/NISTP256/AMD64/fenz.vo | 0m14.14s || +0m00.26s | +1.90% 0m14.35s | Specific/X25519/C64/fecarry.vo | 0m14.26s || +0m00.08s | +0.63% 0m14.25s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m14.13s || +0m00.11s | +0.84% 0m13.95s | Arithmetic/Saturated/AddSub.vo | 0m14.02s || -0m00.07s | -0.49% 0m13.59s | Specific/NISTP256/AMD128/fenz.vo | 0m13.65s || -0m00.06s | -0.43% 0m13.15s | Experiments/NewPipeline/CStringification.vo | 0m13.15s || +0m00.00s | +0.00% 0m12.63s | Compilers/Z/Syntax/Equality.vo | 0m12.57s || +0m00.06s | +0.47% 0m12.30s | Util/ZRange/LandLorBounds.vo | 0m12.78s || -0m00.47s | -3.75% 0m12.18s | Specific/X25519/C64/feadd.vo | 0m11.87s || +0m00.31s | +2.61% 0m12.15s | Specific/NISTP256/AMD128/feopp.vo | 0m12.28s || -0m00.12s | -1.05% 0m11.74s | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo | 0m12.46s || -0m00.72s | -5.77% 0m11.30s | Arithmetic/Saturated/MontgomeryAPI.vo | 0m11.54s || -0m00.23s | -2.07% 0m10.82s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.48s || +0m00.33s | +3.24% 0m10.71s | Arithmetic/Saturated/Core.vo | 0m11.36s || -0m00.64s | -5.72% 0m09.90s | Specific/X2448/Karatsuba/C64/Synthesis.vo | 0m09.64s || +0m00.25s | +2.69% 0m08.95s | Util/ZRange/CornersMonotoneBounds.vo | 0m09.41s || -0m00.46s | -4.88% 0m08.77s | LegacyArithmetic/Double/Proofs/Multiply.vo | 0m08.62s || +0m00.15s | +1.74% 0m08.72s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.95s || -0m00.22s | -2.56% 0m08.66s | LegacyArithmetic/ArchitectureToZLikeProofs.vo | 0m08.49s || +0m00.16s | +2.00% 0m08.53s | LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.vo | 0m08.51s || +0m00.01s | +0.23% 0m08.40s | Compilers/Named/CompileInterpSideConditions.vo | 0m07.55s || +0m00.85s | +11.25% 0m08.12s | Compilers/Named/RegisterAssignInterp.vo | 0m08.36s || -0m00.24s | -2.87% 0m07.55s | Compilers/InlineConstAndOpWf.vo | 0m07.59s || -0m00.04s | -0.52% 0m07.06s | Specific/NISTP256/AMD64/Synthesis.vo | 0m06.96s || +0m00.09s | +1.43% 0m06.47s | Arithmetic/Saturated/MulSplit.vo | 0m06.55s || -0m00.08s | -1.22% 0m06.24s | Compilers/InlineWf.vo | 0m06.17s || +0m00.07s | +1.13% 0m06.14s | Compilers/Z/Bounds/InterpretationLemmas/PullCast.vo | 0m06.34s || -0m00.20s | -3.15% 0m05.93s | Specific/X25519/C64/Synthesis.vo | 0m05.89s || +0m00.04s | +0.67% 0m05.81s | Compilers/LinearizeWf.vo | 0m05.69s || +0m00.11s | +2.10% 0m05.54s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.33s || +0m00.20s | +3.93% 0m05.54s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.62s || -0m00.08s | -1.42% 0m05.48s | Compilers/Z/HexNotationConstants.vo | 0m05.47s || +0m00.01s | +0.18% 0m05.14s | Compilers/WfProofs.vo | 0m05.06s || +0m00.08s | +1.58% 0m05.06s | LegacyArithmetic/Double/Proofs/RippleCarryAddSub.vo | 0m05.51s || -0m00.45s | -8.16% 0m04.78s | LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.vo | 0m04.97s || -0m00.18s | -3.82% 0m04.74s | Experiments/NewPipeline/RewriterWf1.vo | 0m04.78s || -0m00.04s | -0.83% 0m04.46s | Compilers/Z/BinaryNotationConstants.vo | 0m04.52s || -0m00.05s | -1.32% 0m04.38s | Compilers/Z/Bounds/Pipeline/Definition.vo | 0m04.56s || -0m00.17s | -3.94% 0m04.34s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m04.03s || +0m00.30s | +7.69% 0m04.28s | Compilers/Named/CompileWf.vo | 0m04.21s || +0m00.07s | +1.66% 0m04.13s | Specific/Framework/ArithmeticSynthesis/Montgomery.vo | 0m04.05s || +0m00.08s | +1.97% 0m04.01s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.04s || -0m00.03s | -0.74% 0m04.00s | Experiments/NewPipeline/MiscCompilerPassesProofs.vo | 0m03.92s || +0m00.08s | +2.04% 0m03.92s | Arithmetic/MontgomeryReduction/WordByWord/Proofs.vo | 0m03.88s || +0m00.04s | +1.03% 0m03.68s | Compilers/EtaWf.vo | 0m04.40s || -0m00.72s | -16.36% 0m03.47s | Compilers/Z/ArithmeticSimplifier.vo | 0m03.52s || -0m00.04s | -1.42% 0m03.36s | Specific/NISTP256/AMD128/Synthesis.vo | 0m03.25s || +0m00.10s | +3.38% 0m03.28s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.18s || +0m00.09s | +3.14% 0m03.06s | Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.vo | 0m03.02s || +0m00.04s | +1.32% 0m03.05s | Compilers/InlineInterp.vo | 0m02.95s || +0m00.09s | +3.38% 0m03.01s | LegacyArithmetic/Double/Proofs/ShiftRight.vo | 0m02.98s || +0m00.02s | +1.00% 0m02.97s | Compilers/Named/ContextProperties.vo | 0m02.94s || +0m00.03s | +1.02% 0m02.96s | LegacyArithmetic/Double/Proofs/ShiftLeft.vo | 0m02.84s || +0m00.12s | +4.22% 0m02.86s | Compilers/Named/CompileInterp.vo | 0m02.76s || +0m00.10s | +3.62% 0m02.66s | Compilers/TestCase.vo | 0m02.56s || +0m00.10s | +3.90% 0m02.61s | Arithmetic/Saturated/Freeze.vo | 0m02.52s || +0m00.08s | +3.57% 0m02.54s | Compilers/Named/ContextProperties/Proper.vo | 0m02.60s || -0m00.06s | -2.30% 0m02.52s | LegacyArithmetic/InterfaceProofs.vo | 0m02.96s || -0m00.43s | -14.86% 0m02.37s | LegacyArithmetic/Double/Proofs/Decode.vo | 0m02.42s || -0m00.04s | -2.06% 0m02.36s | Compilers/CommonSubexpressionEliminationProperties.vo | 0m02.42s || -0m00.06s | -2.47% 0m02.36s | Specific/NISTP256/FancyMachine256/Montgomery.vo | 0m02.32s || +0m00.04s | +1.72% 0m02.26s | Specific/NISTP256/FancyMachine256/Barrett.vo | 0m02.26s || +0m00.00s | +0.00% 0m02.17s | Compilers/Z/RewriteAddToAdcInterp.vo | 0m02.15s || +0m00.02s | +0.93% 0m02.15s | Compilers/Z/Bounds/Relax.vo | 0m02.23s || -0m00.08s | -3.58% 0m02.10s | Specific/Framework/ArithmeticSynthesis/Defaults.vo | 0m02.09s || +0m00.01s | +0.47% 0m02.09s | Compilers/Named/NameUtilProperties.vo | 0m02.05s || +0m00.04s | +1.95% 0m01.94s | Specific/NISTP256/FancyMachine256/Core.vo | 0m02.00s || -0m00.06s | -3.00% 0m01.93s | Compilers/WfReflective.vo | 0m01.94s || -0m00.01s | -0.51% 0m01.89s | Compilers/Z/JavaNotations.vo | 0m02.15s || -0m00.26s | -12.09% 0m01.73s | Arithmetic/CoreUnfolder.vo | 0m01.62s || +0m00.10s | +6.79% 0m01.66s | Util/Tuple.vo | 0m02.11s || -0m00.44s | -21.32% 0m01.62s | Compilers/Named/WfFromUnit.vo | 0m01.64s || -0m00.01s | -1.21% 0m01.58s | Compilers/Relations.vo | 0m01.48s || +0m00.10s | +6.75% 0m01.51s | Compilers/Named/InterpretToPHOASWf.vo | 0m01.48s || +0m00.03s | +2.02% 0m01.50s | Specific/Framework/OutputType.vo | 0m01.50s || +0m00.00s | +0.00% 0m01.46s | Experiments/NewPipeline/CLI.vo | 0m01.46s || +0m00.00s | +0.00% 0m01.36s | Util/ZRange/SplitBounds.vo | 0m01.36s || +0m00.00s | +0.00% 0m01.32s | Specific/Framework/ArithmeticSynthesis/Karatsuba.vo | 0m01.36s || -0m00.04s | -2.94% 0m01.28s | Curves/Edwards/XYZT/Precomputed.vo | 0m01.28s || +0m00.00s | +0.00% 0m01.28s | Experiments/NewPipeline/Language.vo | 0m01.49s || -0m00.20s | -14.09% 0m01.27s | Experiments/NewPipeline/StandaloneHaskellMain.vo | 0m01.29s || -0m00.02s | -1.55% 0m01.26s | Experiments/NewPipeline/StandaloneOCamlMain.vo | 0m01.28s || -0m00.02s | -1.56% 0m01.22s | Specific/Framework/ArithmeticSynthesis/Base.vo | 0m01.32s || -0m00.10s | -7.57% 0m01.20s | Compilers/LinearizeInterp.vo | 0m01.20s || +0m00.00s | +0.00% 0m01.15s | Experiments/NewPipeline/CompilersTestCases.vo | 0m01.04s || +0m00.10s | +10.57% 0m01.11s | Compilers/MultiSizeTest.vo | 0m01.14s || -0m00.02s | -2.63% 0m01.08s | Arithmetic/Saturated/CoreUnfolder.vo | 0m01.10s || -0m00.02s | -1.81% 0m01.06s | Compilers/Z/RewriteAddToAdcWf.vo | 0m01.13s || -0m00.06s | -6.19% 0m01.06s | LegacyArithmetic/Double/Proofs/BitwiseOr.vo | 0m01.10s || -0m00.04s | -3.63% 0m01.04s | Experiments/NewPipeline/AbstractInterpretation.vo | 0m01.05s || -0m00.01s | -0.95% 0m01.04s | Util/ZRange/BasicLemmas.vo | 0m01.04s || +0m00.00s | +0.00% 0m00.98s | Arithmetic/Saturated/WrappersUnfolder.vo | 0m01.03s || -0m00.05s | -4.85% 0m00.97s | Specific/Framework/IntegrationTestDisplayCommon.vo | 0m00.91s || +0m00.05s | +6.59% 0m00.97s | Specific/X25519/C32/CurveParameters.vo | 0m00.99s || -0m00.02s | -2.02% 0m00.96s | Compilers/Named/InterpretToPHOASInterp.vo | 0m01.00s || -0m00.04s | -4.00% 0m00.96s | Specific/Framework/SynthesisFramework.vo | 0m00.96s || +0m00.00s | +0.00% 0m00.95s | Experiments/NewPipeline/RewriterProofs.vo | 0m00.88s || +0m00.06s | +7.95% 0m00.93s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics.vo | 0m00.87s || +0m00.06s | +6.89% 0m00.92s | Specific/Framework/ReificationTypes.vo | 0m00.95s || -0m00.02s | -3.15% 0m00.90s | Compilers/InterpByIsoProofs.vo | 0m00.81s || +0m00.08s | +11.11% 0m00.89s | Compilers/Named/CompileProperties.vo | 0m00.84s || +0m00.05s | +5.95% 0m00.88s | Compilers/Named/InterpSideConditionsInterp.vo | 0m00.80s || +0m00.07s | +9.99% 0m00.88s | Specific/Framework/ArithmeticSynthesis/Freeze.vo | 0m00.89s || -0m00.01s | -1.12% 0m00.86s | Compilers/Z/CommonSubexpressionElimination.vo | 0m00.89s || -0m00.03s | -3.37% 0m00.85s | LegacyArithmetic/Double/Proofs/LoadImmediate.vo | 0m00.86s || -0m00.01s | -1.16% 0m00.84s | Compilers/Z/Syntax/Util.vo | 0m00.86s || -0m00.02s | -2.32% 0m00.83s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.vo | 0m00.74s || +0m00.08s | +12.16% 0m00.83s | Specific/Framework/ArithmeticSynthesis/SquareFromMul.vo | 0m00.73s || +0m00.09s | +13.69% 0m00.82s | Arithmetic/Saturated/UniformWeight.vo | 0m00.83s || -0m00.01s | -1.20% 0m00.82s | Specific/Framework/MontgomeryReificationTypes.vo | 0m00.74s || +0m00.07s | +10.81% 0m00.81s | Compilers/Named/FMapContext.vo | 0m00.85s || -0m00.03s | -4.70% 0m00.81s | Compilers/WfInversion.vo | 0m01.00s || -0m00.18s | -18.99% 0m00.80s | Specific/Framework/IntegrationTestTemporaryMiscCommon.vo | 0m00.85s || -0m00.04s | -5.88% 0m00.79s | Arithmetic/Saturated/MulSplitUnfolder.vo | 0m00.90s || -0m00.10s | -12.22% 0m00.78s | Arithmetic/Saturated/FreezeUnfolder.vo | 0m00.78s || +0m00.00s | +0.00% 0m00.78s | LegacyArithmetic/Double/Proofs/SelectConditional.vo | 0m00.70s || +0m00.08s | +11.42% 0m00.78s | Specific/Framework/ArithmeticSynthesis/BasePackage.vo | 0m00.69s || +0m00.09s | +13.04% 0m00.77s | Specific/Framework/MontgomeryReificationTypesPackage.vo | 0m00.76s || +0m00.01s | +1.31% 0m00.76s | Compilers/Named/AListContext.vo | 0m00.82s || -0m00.05s | -7.31% 0m00.75s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage.vo | 0m00.70s || +0m00.05s | +7.14% 0m00.74s | Arithmetic/MontgomeryReduction/WordByWord/Definition.vo | 0m00.72s || +0m00.02s | +2.77% 0m00.74s | Specific/Framework/ArithmeticSynthesis/FreezePackage.vo | 0m00.78s || -0m00.04s | -5.12% 0m00.74s | Specific/Framework/ArithmeticSynthesis/Ladderstep.vo | 0m00.71s || +0m00.03s | +4.22% 0m00.74s | Specific/Framework/ReificationTypesPackage.vo | 0m00.73s || +0m00.01s | +1.36% 0m00.73s | Compilers/MapCastByDeBruijnInterp.vo | 0m00.75s || -0m00.02s | -2.66% 0m00.73s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage.vo | 0m00.71s || +0m00.02s | +2.81% 0m00.72s | Arithmetic/Saturated/UniformWeightInstances.vo | 0m00.64s || +0m00.07s | +12.49% 0m00.72s | Compilers/InlineConstAndOpInterp.vo | 0m00.78s || -0m00.06s | -7.69% 0m00.71s | Specific/Framework/ArithmeticSynthesis/HelperTactics.vo | 0m00.69s || +0m00.02s | +2.89% 0m00.71s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage.vo | 0m00.70s || +0m00.01s | +1.42% 0m00.70s | Util/CPSUtil.vo | 0m00.86s || -0m00.16s | -18.60% 0m00.69s | Compilers/SmartMap.vo | 0m00.72s || -0m00.03s | -4.16% 0m00.69s | Experiments/NewPipeline/MiscCompilerPasses.vo | 0m01.00s || -0m00.31s | -31.00% 0m00.67s | Arithmetic/Saturated/Wrappers.vo | 0m00.66s || +0m00.01s | +1.51% 0m00.66s | Compilers/CommonSubexpressionEliminationInterp.vo | 0m00.69s || -0m00.02s | -4.34% 0m00.65s | Compilers/CommonSubexpressionElimination.vo | 0m00.64s || +0m00.01s | +1.56% 0m00.63s | LegacyArithmetic/Interface.vo | 0m00.87s || -0m00.24s | -27.58% 0m00.62s | Compilers/WfReflectiveGen.vo | 0m00.66s || -0m00.04s | -6.06% 0m00.61s | Compilers/Z/Bounds/MapCastByDeBruijnInterp.vo | 0m00.62s || -0m00.01s | -1.61% 0m00.61s | Compilers/Z/Bounds/Pipeline.vo | 0m00.72s || -0m00.10s | -15.27% 0m00.60s | Compilers/MapCastByDeBruijnWf.vo | 0m00.61s || -0m00.01s | -1.63% 0m00.59s | Compilers/Named/WfInterp.vo | 0m00.57s || +0m00.02s | +3.50% 0m00.58s | Compilers/InlineConstAndOpByRewriteWf.vo | 0m00.54s || +0m00.03s | +7.40% 0m00.58s | Compilers/MapBaseTypeWf.vo | 0m00.63s || -0m00.05s | -7.93% 0m00.58s | Compilers/Z/Named/RewriteAddToAdc.vo | 0m00.64s || -0m00.06s | -9.37% 0m00.57s | Compilers/Z/MapCastByDeBruijnInterp.vo | 0m00.51s || +0m00.05s | +11.76% 0m00.57s | Compilers/Z/Syntax.vo | 0m00.61s || -0m00.04s | -6.55% 0m00.57s | Experiments/PartialEvaluationWithLetIn.vo | 0m00.57s || +0m00.00s | +0.00% 0m00.56s | Compilers/Z/Bounds/InterpretationLemmas/Tactics.vo | 0m00.55s || +0m00.01s | +1.81% 0m00.56s | Compilers/Z/Bounds/Pipeline/Glue.vo | 0m00.55s || +0m00.01s | +1.81% 0m00.55s | Compilers/Z/Reify.vo | 0m00.53s || +0m00.02s | +3.77% 0m00.54s | Compilers/InterpWfRel.vo | 0m00.54s || +0m00.00s | +0.00% 0m00.54s | Compilers/Z/Bounds/RoundUpLemmas.vo | 0m00.56s || -0m00.02s | -3.57% 0m00.54s | LegacyArithmetic/Double/Core.vo | 0m00.52s || +0m00.02s | +3.84% 0m00.54s | LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.vo | 0m00.49s || +0m00.05s | +10.20% 0m00.54s | Util/Decidable/Decidable2Bool.vo | 0m00.69s || -0m00.14s | -21.73% 0m00.53s | Compilers/Z/CommonSubexpressionEliminationInterp.vo | 0m00.49s || +0m00.04s | +8.16% 0m00.52s | Compilers/ExprInversion.vo | 0m00.44s || +0m00.08s | +18.18% 0m00.52s | Compilers/GeneralizeVarInterp.vo | 0m00.51s || +0m00.01s | +1.96% 0m00.52s | Compilers/InterpWf.vo | 0m00.49s || +0m00.03s | +6.12% 0m00.52s | Compilers/Z/InlineConstAndOp.vo | 0m00.40s || +0m00.12s | +30.00% 0m00.52s | Compilers/Z/RewriteAddToAdc.vo | 0m00.51s || +0m00.01s | +1.96% 0m00.52s | Util/HList.vo | 0m00.59s || -0m00.06s | -11.86% 0m00.51s | Compilers/InputSyntax.vo | 0m00.52s || -0m00.01s | -1.92% 0m00.51s | Compilers/Z/Bounds/MapCastByDeBruijnWf.vo | 0m00.58s || -0m00.06s | -12.06% 0m00.51s | Compilers/Z/CommonSubexpressionEliminationWf.vo | 0m00.51s || +0m00.00s | +0.00% 0m00.50s | Compilers/Z/Bounds/MapCastByDeBruijn.vo | 0m00.53s || -0m00.03s | -5.66% 0m00.50s | Compilers/Z/FoldTypes.vo | 0m00.49s || +0m00.01s | +2.04% 0m00.50s | Util/ZBounded.vo | 0m00.54s || -0m00.04s | -7.40% 0m00.49s | Compilers/Z/MapCastByDeBruijn.vo | 0m00.48s || +0m00.01s | +2.08% 0m00.49s | Experiments/NewPipeline/UnderLets.vo | 0m00.55s || -0m00.06s | -10.90% 0m00.47s | Compilers/GeneralizeVarWf.vo | 0m00.46s || +0m00.00s | +2.17% 0m00.47s | Compilers/Named/PositiveContext/DefaultsProperties.vo | 0m00.51s || -0m00.04s | -7.84% 0m00.47s | Compilers/Z/MapCastByDeBruijnWf.vo | 0m00.47s || +0m00.00s | +0.00% 0m00.47s | LegacyArithmetic/ArchitectureToZLike.vo | 0m00.49s || -0m00.02s | -4.08% 0m00.47s | Util/AdditionChainExponentiation.vo | 0m00.44s || +0m00.02s | +6.81% 0m00.46s | Compilers/Named/DeadCodeEliminationInterp.vo | 0m00.49s || -0m00.02s | -6.12% 0m00.46s | Compilers/Named/WeakListContext.vo | 0m00.42s || +0m00.04s | +9.52% 0m00.46s | Compilers/Z/Bounds/Interpretation.vo | 0m00.45s || +0m00.01s | +2.22% 0m00.46s | Compilers/Z/GeneralizeVarInterp.vo | 0m00.49s || -0m00.02s | -6.12% 0m00.46s | Compilers/Z/InlineConstAndOpByRewrite.vo | 0m00.44s || +0m00.02s | +4.54% 0m00.46s | Compilers/Z/InlineConstAndOpInterp.vo | 0m00.50s || -0m00.03s | -7.99% 0m00.46s | Compilers/Z/InlineWf.vo | 0m00.45s || +0m00.01s | +2.22% 0m00.46s | Compilers/Z/InterpSideConditions.vo | 0m00.50s || -0m00.03s | -7.99% 0m00.46s | Compilers/Z/Named/DeadCodeElimination.vo | 0m00.39s || +0m00.07s | +17.94% 0m00.46s | Specific/Framework/CurveParameters.vo | 0m00.46s || +0m00.00s | +0.00% 0m00.46s | Specific/X25519/C64/CurveParameters.vo | 0m00.49s || -0m00.02s | -6.12% 0m00.45s | Compilers/Z/ArithmeticSimplifierUtil.vo | 0m00.48s || -0m00.02s | -6.24% 0m00.45s | Compilers/Z/GeneralizeVarWf.vo | 0m00.42s || +0m00.03s | +7.14% 0m00.45s | Compilers/Z/Inline.vo | 0m00.47s || -0m00.01s | -4.25% 0m00.45s | Compilers/Z/InlineInterp.vo | 0m00.47s || -0m00.01s | -4.25% 0m00.44s | Compilers/InlineConstAndOpByRewriteInterp.vo | 0m00.43s || +0m00.01s | +2.32% 0m00.44s | Compilers/Z/InlineConstAndOpByRewriteWf.vo | 0m00.51s || -0m00.07s | -13.72% 0m00.44s | Compilers/Z/InlineConstAndOpWf.vo | 0m00.52s || -0m00.08s | -15.38% 0m00.44s | Compilers/ZExtended/Syntax.vo | 0m00.59s || -0m00.14s | -25.42% 0m00.44s | Specific/Framework/IntegrationTestDisplayCommonTactics.vo | 0m00.43s || +0m00.01s | +2.32% 0m00.43s | Compilers/ZExtended/MapBaseType.vo | 0m00.48s || -0m00.04s | -10.41% 0m00.42s | Compilers/InlineConstAndOp.vo | 0m00.46s || -0m00.04s | -8.69% 0m00.42s | Compilers/InterpProofs.vo | 0m00.44s || -0m00.02s | -4.54% 0m00.42s | Compilers/Named/PositiveContext/Defaults.vo | 0m00.36s || +0m00.06s | +16.66% 0m00.42s | Compilers/Reify.vo | 0m00.49s || -0m00.07s | -14.28% 0m00.42s | Compilers/Z/InlineConstAndOpByRewriteInterp.vo | 0m00.43s || -0m00.01s | -2.32% 0m00.42s | Util/ZRange.vo | 0m00.61s || -0m00.19s | -31.14% 0m00.42s | Util/ZRange/Operations.vo | 0m00.50s || -0m00.08s | -16.00% 0m00.41s | Compilers/Inline.vo | 0m00.37s || +0m00.03s | +10.81% 0m00.41s | Compilers/Named/RegisterAssign.vo | 0m00.38s || +0m00.02s | +7.89% 0m00.41s | Compilers/Z/Named/DeadCodeEliminationInterp.vo | 0m00.47s || -0m00.06s | -12.76% 0m00.40s | Compilers/Z/GeneralizeVar.vo | 0m00.48s || -0m00.07s | -16.66% 0m00.40s | Specific/Framework/RawCurveParameters.vo | 0m00.43s || -0m00.02s | -6.97% 0m00.40s | Util/ZRange/Show.vo | 0m00.37s || +0m00.03s | +8.10% 0m00.39s | Compilers/ZExtended/InlineConstAndOpInterp.vo | 0m00.38s || +0m00.01s | +2.63% 0m00.38s | Compilers/Named/ContextProperties/Tactics.vo | 0m00.32s || +0m00.06s | +18.75% 0m00.38s | Compilers/Named/DeadCodeElimination.vo | 0m00.44s || -0m00.06s | -13.63% 0m00.38s | Compilers/Z/Bounds/Pipeline/OutputType.vo | 0m00.32s || +0m00.06s | +18.75% 0m00.37s | Compilers/CommonSubexpressionEliminationDenote.vo | 0m00.36s || +0m00.01s | +2.77% 0m00.37s | Compilers/GeneralizeVar.vo | 0m00.36s || +0m00.01s | +2.77% 0m00.37s | Specific/X2448/Karatsuba/C64/CurveParameters.vo | 0m00.38s || -0m00.01s | -2.63% 0m00.36s | Compilers/FoldTypes.vo | 0m00.34s || +0m00.01s | +5.88% 0m00.36s | Compilers/MapBaseType.vo | 0m00.32s || +0m00.03s | +12.49% 0m00.36s | Compilers/MapCastByDeBruijn.vo | 0m00.35s || +0m00.01s | +2.85% 0m00.36s | Compilers/Named/MapCast.vo | 0m00.38s || -0m00.02s | -5.26% 0m00.36s | Compilers/Z/TypeInversion.vo | 0m00.32s || +0m00.03s | +12.49% 0m00.36s | Compilers/ZExtended/InlineConstAndOpByRewrite.vo | 0m00.32s || +0m00.03s | +12.49% 0m00.36s | Specific/Framework/CurveParametersPackage.vo | 0m00.34s || +0m00.01s | +5.88% 0m00.36s | Specific/NISTP256/AMD128/CurveParameters.vo | 0m00.36s || +0m00.00s | +0.00% 0m00.36s | Specific/NISTP256/AMD64/CurveParameters.vo | 0m00.44s || -0m00.08s | -18.18% 0m00.35s | Compilers/CountLets.vo | 0m00.32s || +0m00.02s | +9.37% 0m00.35s | Util/BoundedWord.vo | 0m00.60s || -0m00.25s | -41.66% 0m00.34s | Compilers/InlineConstAndOpByRewrite.vo | 0m00.34s || +0m00.00s | +0.00% 0m00.34s | Compilers/InterpByIso.vo | 0m00.36s || -0m00.01s | -5.55% 0m00.34s | Compilers/Linearize.vo | 0m00.34s || +0m00.00s | +0.00% 0m00.34s | Compilers/Named/ContextOn.vo | 0m00.32s || +0m00.02s | +6.25% 0m00.34s | Compilers/Named/InterpSideConditions.vo | 0m00.35s || -0m00.00s | -2.85% 0m00.34s | Compilers/Named/InterpretToPHOAS.vo | 0m00.30s || +0m00.04s | +13.33% 0m00.34s | Compilers/StripExpr.vo | 0m00.31s || +0m00.03s | +9.67% 0m00.34s | Compilers/Z/OpInversion.vo | 0m00.32s || +0m00.02s | +6.25% 0m00.34s | Compilers/ZExtended/Syntax/Util.vo | 0m00.38s || -0m00.03s | -10.52% 0m00.34s | Util/IdfunWithAlt.vo | 0m00.50s || -0m00.15s | -31.99% 0m00.33s | Compilers/FilterLive.vo | 0m00.32s || +0m00.01s | +3.12% 0m00.33s | Compilers/Named/Compile.vo | 0m00.34s || -0m00.01s | -2.94% 0m00.33s | Compilers/Named/ContextDefinitions.vo | 0m00.34s || -0m00.01s | -2.94% 0m00.33s | Compilers/Named/IdContext.vo | 0m00.33s || +0m00.00s | +0.00% 0m00.33s | Compilers/Named/PositiveContext.vo | 0m00.38s || -0m00.04s | -13.15% 0m00.32s | Compilers/Named/CountLets.vo | 0m00.32s || +0m00.00s | +0.00% 0m00.32s | Compilers/Named/EstablishLiveness.vo | 0m00.36s || -0m00.03s | -11.11% 0m00.32s | Compilers/Named/GetNames.vo | 0m00.30s || +0m00.02s | +6.66% 0m00.32s | Compilers/Named/MapType.vo | 0m00.32s || +0m00.00s | +0.00% 0m00.32s | Compilers/Named/Syntax.vo | 0m00.39s || -0m00.07s | -17.94% 0m00.32s | Compilers/Tuple.vo | 0m00.41s || -0m00.08s | -21.95% 0m00.32s | Compilers/ZExtended/InlineConstAndOpByRewriteInterp.vo | 0m00.36s || -0m00.03s | -11.11% 0m00.32s | Compilers/ZExtended/InlineConstAndOpByRewriteWf.vo | 0m00.40s || -0m00.08s | -20.00% 0m00.32s | Compilers/ZExtended/InlineConstAndOpWf.vo | 0m00.36s || -0m00.03s | -11.11% 0m00.31s | Compilers/Named/ExprInversion.vo | 0m00.31s || +0m00.00s | +0.00% 0m00.31s | Compilers/Named/Wf.vo | 0m00.33s || -0m00.02s | -6.06% 0m00.30s | Compilers/Named/Context.vo | 0m00.32s || -0m00.02s | -6.25% 0m00.30s | Compilers/ZExtended/InlineConstAndOp.vo | 0m00.34s || -0m00.04s | -11.76% 0m00.28s | Compilers/Named/SmartMap.vo | 0m00.30s || -0m00.01s | -6.66% 0m00.26s | Util/SideConditions/ModInvPackage.vo | 0m00.28s || -0m00.02s | -7.14% 0m00.25s | Util/Option.vo | 0m00.25s || +0m00.00s | +0.00% 0m00.24s | Util/OptionList.vo | 0m00.27s || -0m00.03s | -11.11% 0m00.23s | Util/SideConditions/Autosolve.vo | 0m00.24s || -0m00.00s | -4.16% 0m00.22s | Compilers/EtaInterp.vo | 0m00.29s || -0m00.06s | -24.13% 0m00.14s | Compilers/RewriterWf.vo | 0m00.17s || -0m00.03s | -17.64% 0m00.11s | Util/ListUtil/SetoidList.vo | 0m00.13s || -0m00.02s | -15.38% 0m00.08s | Compilers/InterpSideConditions.vo | 0m00.07s || +0m00.00s | +14.28% 0m00.07s | Compilers/Eta.vo | 0m00.09s || -0m00.01s | -22.22% 0m00.04s | Compilers/RenameBinders.vo | 0m00.08s || -0m00.04s | -50.00%
* Compatibility after Coq PR#262 (continued).Gravatar Hugo Herbelin2018-09-26
| | | | | | This is a second instance of incompatibility induced by PR#262 (see 251ea49a). One fixes it the same, reducing the search space for a return clause by forbidding it to be obtained by small inversion.
* Compatibility with coq PR #8457Gravatar Frédéric Besson2018-09-25
| | | | | Explicitly clear hypothesis Bv_bound so that lia cannot use it.
* Export notations when importing primitiveGravatar Jason Gross2018-09-18
|
* remove unneeded proofGravatar jadep2018-09-17
|
* redo all Rows correctness proofs using partition and sanity, remove ↵Gravatar jadep2018-09-17
| | | | now-unused Saturated.DivMod
* remove now-unused nth_default hintsGravatar jadep2018-09-17
|
* fix up flatten partitioning proofs so that they don't use nth_defaultGravatar jadep2018-09-17
|
* remove commented-out code that is now clearly unneededGravatar jadep2018-09-17
|
* Change naming for partitionGravatar jadep2018-09-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 15:02:06 +0000