aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-03-08 18:29:37 -0500
committerGravatar Jason Gross <jgross@mit.edu>2019-03-08 18:55:41 -0500
commit77644445a7320998cbb6a4bf1cdb0e437723e1eb (patch)
treee220db01c9c4197b7b894080805ff1cd230175d7
parentddd7df2bc75cc2b368aef9bcd02c4344651705e4 (diff)
Allow more reucrsion in wf_safe_t_step
After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------------------- 31m53.77s | Total | 32m03.39s || -0m09.62s | -0.50% ----------------------------------------------------------------------------------------------------------- 3m14.32s | p384_32.c | 3m17.09s || -0m02.77s | -1.40% 0m18.13s | secp256k1_32.c | 0m20.29s || -0m02.16s | -10.64% 1m56.46s | RewriterRulesGood.vo | 1m58.15s || -0m01.68s | -1.43% 1m47.38s | Fancy/Barrett256.vo | 1m48.40s || -0m01.02s | -0.94% 0m55.66s | AbstractInterpretationWf.vo | 0m54.26s || +0m01.39s | +2.58% 0m46.39s | p521_32.c | 0m44.46s || +0m01.92s | +4.34% 0m41.97s | ExtractionHaskell/unsaturated_solinas | 0m43.02s || -0m01.05s | -2.44% 0m29.71s | ExtractionHaskell/saturated_solinas | 0m30.81s || -0m01.09s | -3.57% 0m15.02s | ExtractionOCaml/unsaturated_solinas | 0m13.40s || +0m01.61s | +12.08% 0m06.21s | ExtractionOCaml/saturated_solinas.ml | 0m07.39s || -0m01.17s | -15.96% 2m50.82s | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m50.03s || +0m00.78s | +0.46% 2m37.53s | Fancy/Compiler.vo | 2m37.78s || -0m00.25s | -0.15% 2m02.37s | RewriterWf2.vo | 2m01.63s || +0m00.74s | +0.60% 1m48.26s | RewriterRulesInterpGood.vo | 1m48.36s || -0m00.10s | -0.09% 0m57.65s | ExtractionHaskell/word_by_word_montgomery | 0m58.06s || -0m00.41s | -0.70% 0m55.33s | RewriterInterpProofs1.vo | 0m56.16s || -0m00.82s | -1.47% 0m41.18s | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo | 0m40.54s || +0m00.64s | +1.57% 0m40.34s | p521_64.c | 0m40.14s || +0m00.20s | +0.49% 0m37.24s | Fancy/Montgomery256.vo | 0m37.94s || -0m00.69s | -1.84% 0m36.23s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.49s || -0m00.26s | -0.71% 0m36.23s | UnderLetsProofs.vo | 0m37.19s || -0m00.96s | -2.58% 0m35.05s | AbstractInterpretationProofs.vo | 0m34.69s || +0m00.35s | +1.03% 0m30.73s | AbstractInterpretationZRangeProofs.vo | 0m30.15s || +0m00.58s | +1.92% 0m28.92s | LanguageWf.vo | 0m28.74s || +0m00.18s | +0.62% 0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.12s || +0m00.16s | +0.62% 0m26.70s | PushButtonSynthesis/MontgomeryReductionReificationCache.vo | 0m26.88s || -0m00.17s | -0.66% 0m25.49s | RewriterWf1.vo | 0m25.30s || +0m00.18s | +0.75% 0m25.03s | SlowPrimeSynthesisExamples.vo | 0m24.13s || +0m00.90s | +3.72% 0m22.83s | ExtractionOCaml/word_by_word_montgomery | 0m22.92s || -0m00.09s | -0.39% 0m20.14s | p448_solinas_64.c | 0m20.16s || -0m00.01s | -0.09% 0m19.64s | p256_32.c | 0m19.47s || +0m00.17s | +0.87% 0m16.09s | p434_64.c | 0m16.00s || +0m00.08s | +0.56% 0m15.98s | PushButtonSynthesis/BarrettReductionReificationCache.vo | 0m15.93s || +0m00.05s | +0.31% 0m13.45s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.60s || -0m00.15s | -1.10% 0m11.14s | ExtractionOCaml/saturated_solinas | 0m11.11s || +0m00.03s | +0.27% 0m09.60s | p224_32.c | 0m09.30s || +0m00.29s | +3.22% 0m09.21s | ExtractionHaskell/word_by_word_montgomery.hs | 0m09.87s || -0m00.65s | -6.68% 0m08.44s | p384_64.c | 0m08.62s || -0m00.17s | -2.08% 0m08.22s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.21s || -0m00.99s | -10.74% 0m07.01s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.69s || -0m00.68s | -8.84% 0m06.80s | BoundsPipeline.vo | 0m06.73s || +0m00.06s | +1.04% 0m05.68s | Fancy/Prod.vo | 0m05.76s || -0m00.08s | -1.38% 0m05.44s | ExtractionHaskell/saturated_solinas.hs | 0m06.42s || -0m00.97s | -15.26% 0m05.28s | PushButtonSynthesis/SaturatedSolinasReificationCache.vo | 0m05.92s || -0m00.63s | -10.81% 0m03.67s | MiscCompilerPassesProofs.vo | 0m03.62s || +0m00.04s | +1.38% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.64s || -0m00.10s | -2.74% 0m03.45s | PushButtonSynthesis/SmallExamples.vo | 0m03.45s || +0m00.00s | +0.00% 0m03.24s | PushButtonSynthesis/BarrettReduction.vo | 0m03.21s || +0m00.03s | +0.93% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.18s || +0m00.00s | +0.31% 0m03.02s | curve25519_32.c | 0m03.32s || -0m00.29s | -9.03% 0m02.78s | PushButtonSynthesis/MontgomeryReduction.vo | 0m02.86s || -0m00.08s | -2.79% 0m02.10s | curve25519_64.c | 0m01.93s || +0m00.17s | +8.80% 0m01.62s | p256_64.c | 0m01.63s || -0m00.00s | -0.61% 0m01.52s | secp256k1_64.c | 0m01.44s || +0m00.08s | +5.55% 0m01.38s | p224_64.c | 0m01.70s || -0m00.32s | -18.82% 0m01.34s | CLI.vo | 0m01.42s || -0m00.07s | -5.63% 0m01.16s | StandaloneHaskellMain.vo | 0m01.14s || +0m00.02s | +1.75% 0m01.15s | RewriterProofs.vo | 0m01.14s || +0m00.01s | +0.87% 0m01.00s | StandaloneOCamlMain.vo | 0m01.19s || -0m00.18s | -15.96% 0m00.59s | PushButtonSynthesis/LegacySynthesisTactics.vo | 0m00.68s || -0m00.09s | -13.23% 0m00.43s | PushButtonSynthesis/ReificationCache.vo | 0m00.53s || -0m00.10s | -18.86%
Diffstat
-rw-r--r--src/LanguageWf.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/LanguageWf.v b/src/LanguageWf.v
index 0ec717e70..34b140979 100644
--- a/src/LanguageWf.v
+++ b/src/LanguageWf.v
@@ -1235,6 +1235,9 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
| [ H : context[List.In _ (_ ++ _)%list] |- _ ] => rewrite in_app_iff in H
| [ H : context[expr.wf _ _ _] |- expr.wf _ _ _ ]
=> eapply H; clear H; eauto with nocore; solve [ repeat wf_safe_t_step ]
+ end
+ | match goal with
+ | [ |- _ \/ _ ] => constructor; solve [ repeat wf_safe_t_step ]
end ].
Ltac wf_unsafe_t_step :=
first [ solve [ eauto with nocore ]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-04 02:19:14 +0000