From 301af21a0d908762a83ebbd9c009bcd8d3af3100 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 8 Apr 2019 15:41:53 -0400 Subject: Make a single tactic to build the rewriter MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Parallelize across different rewriters, rather than across different parts of the rewriter. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m38.03s | Total | 20m17.67s || +0m20.36s | +1.67% ----------------------------------------------------------------------------------------------- N/A | RewriterFull.vo | 1m11.76s || -1m11.76s | -100.00% 0m56.15s | Rewriter/ToFancyWithCasts.vo | N/A || +0m56.14s | ∞ N/A | RewriterRulesInterpGood.vo | 0m51.06s || -0m51.06s | -100.00% 0m45.62s | Rewriter/NBE.vo | N/A || +0m45.61s | ∞ 0m44.32s | Rewriter/ArithWithCasts.vo | N/A || +0m44.32s | ∞ 0m24.56s | Rewriter/Arith.vo | N/A || +0m24.55s | ∞ N/A | RewriterRulesGood.vo | 0m21.60s || -0m21.60s | -100.00% 1m34.27s | RewriterWf2.vo | 1m43.16s || -0m08.88s | -8.61% 3m21.20s | p384_32.c | 3m28.08s || -0m06.87s | -3.30% 1m40.72s | Fancy/Barrett256.vo | 1m43.94s || -0m03.21s | -3.09% 0m41.11s | p521_64.c | 0m38.11s || +0m03.00s | +7.87% 0m47.88s | p521_32.c | 0m44.98s || +0m02.90s | +6.44% 0m23.68s | ExtractionOCaml/word_by_word_montgomery | 0m21.56s || +0m02.12s | +9.83% 0m58.92s | ExtractionHaskell/word_by_word_montgomery | 0m57.87s || +0m01.05s | +1.81% 0m20.05s | p448_solinas_64.c | 0m18.72s || +0m01.33s | +7.10% 0m15.19s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.76s || +0m01.42s | +10.39% 0m14.64s | ExtractionOCaml/unsaturated_solinas | 0m13.55s || +0m01.08s | +8.04% 0m09.19s | ExtractionOCaml/saturated_solinas | 0m10.69s || -0m01.50s | -14.03% 0m08.65s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.85s || -0m01.19s | -12.18% 0m07.71s | ExtractionOCaml/saturated_solinas.ml | 0m06.26s || +0m01.45s | +23.16% 0m05.93s | ExtractionHaskell/saturated_solinas.hs | 0m04.71s || +0m01.21s | +25.90% 0m01.16s | Rewriter/StripLiteralCasts.vo | N/A || +0m01.15s | ∞ 0m01.14s | Rewriter/ToFancy.vo | N/A || +0m01.13s | ∞ 0m44.44s | RewriterInterpProofs1.vo | 0m45.18s || -0m00.74s | -1.63% 0m39.85s | ExtractionHaskell/unsaturated_solinas | 0m40.68s || -0m00.82s | -2.04% 0m36.42s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.44s || -0m00.01s | -0.05% 0m36.21s | RewriterWf1.vo | 0m36.91s || -0m00.69s | -1.89% 0m34.81s | Fancy/Montgomery256.vo | 0m34.38s || +0m00.42s | +1.25% 0m30.85s | ExtractionHaskell/saturated_solinas | 0m31.77s || -0m00.91s | -2.89% 0m27.26s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.09s || +0m00.17s | +0.62% 0m26.88s | SlowPrimeSynthesisExamples.vo | 0m27.32s || -0m00.44s | -1.61% 0m20.88s | PushButtonSynthesis/BarrettReduction.vo | 0m21.17s || -0m00.29s | -1.36% 0m18.08s | secp256k1_32.c | 0m18.44s || -0m00.36s | -1.95% 0m17.39s | p256_32.c | 0m17.74s || -0m00.34s | -1.97% 0m15.12s | p434_64.c | 0m14.68s || +0m00.43s | +2.99% 0m09.02s | p224_32.c | 0m08.11s || +0m00.91s | +11.22% 0m07.91s | p384_64.c | 0m07.92s || -0m00.00s | -0.12% 0m07.89s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.50s || +0m00.38s | +5.19% 0m07.02s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.60s || -0m00.58s | -7.63% 0m06.91s | BoundsPipeline.vo | 0m06.92s || -0m00.00s | -0.14% 0m03.56s | PushButtonSynthesis/Primitives.vo | 0m03.53s || +0m00.03s | +0.84% 0m03.39s | PushButtonSynthesis/SmallExamples.vo | 0m03.25s || +0m00.14s | +4.30% 0m03.32s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.14s || +0m00.17s | +5.73% 0m02.83s | curve25519_32.c | 0m02.41s || +0m00.41s | +17.42% 0m02.72s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.62s || +0m00.10s | +3.81% 0m01.91s | secp256k1_64.c | 0m01.89s || +0m00.02s | +1.05% 0m01.75s | curve25519_64.c | 0m02.14s || -0m00.39s | -18.22% 0m01.60s | p224_64.c | 0m01.60s || +0m00.00s | +0.00% 0m01.43s | p256_64.c | 0m01.82s || -0m00.39s | -21.42% 0m01.30s | CLI.vo | 0m01.35s || -0m00.05s | -3.70% 0m01.22s | StandaloneOCamlMain.vo | 0m01.07s || +0m00.14s | +14.01% 0m01.18s | CompilersTestCases.vo | 0m01.14s || +0m00.04s | +3.50% 0m01.12s | StandaloneHaskellMain.vo | 0m01.14s || -0m00.01s | -1.75% 0m00.84s | RewriterProofsTactics.vo | N/A || +0m00.84s | ∞ 0m00.83s | RewriterProofs.vo | 0m01.06s || -0m00.23s | -21.69% --- src/RewriterProofsTactics.v | 107 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 src/RewriterProofsTactics.v (limited to 'src/RewriterProofsTactics.v') diff --git a/src/RewriterProofsTactics.v b/src/RewriterProofsTactics.v new file mode 100644 index 000000000..22fd16cbb --- /dev/null +++ b/src/RewriterProofsTactics.v @@ -0,0 +1,107 @@ +Require Import Crypto.Language. +Require Import Crypto.LanguageInversion. +Require Import Crypto.LanguageWf. +Require Import Crypto.UnderLetsProofs. +Require Import Crypto.GENERATEDIdentifiersWithoutTypesProofs. +Require Import Crypto.Rewriter. +Require Import Crypto.RewriterWf1. +Require Import Crypto.RewriterWf2. +Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.Util.Tactics.CacheTerm. +Require Import Crypto.Util.Tactics.ConstrFail. + +Module Compilers. + Import LanguageWf.Compilers. + Import GENERATEDIdentifiersWithoutTypes.Compilers. + Import GENERATEDIdentifiersWithoutTypesProofs.Compilers. + Import Rewriter.Compilers.RewriteRules. + Import RewriterWf1.Compilers.RewriteRules. + Import RewriterWf2.Compilers.RewriteRules. + Import RewriterInterpProofs1.Compilers.RewriteRules. + Import Rewriter.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.GoalType. + Import RewriterWf1.Compilers.RewriteRules.WfTactics.Tactic. + Import RewriterWf1.Compilers.RewriteRules.InterpTactics.Tactic. + + Module Import RewriteRules. + Definition VerifiedRewriter_of_Rewriter + (R : RewriterT) + (RWf : Wf_GoalT R) + (RInterp : Interp_GoalT R) + (RProofs : PrimitiveHList.hlist + (@snd bool Prop) + (List.skipn (dummy_count (Rewriter_data R)) (rewrite_rules_specs (Rewriter_data R)))) + : VerifiedRewriter. + Proof. + simple refine + (let HWf := _ in + let HInterp_gen := _ in + @Build_VerifiedRewriter (@Rewriter.Compilers.RewriteRules.GoalType.Rewrite R) HWf HInterp_gen (HInterp_gen _)); + [ | clear HWf ]; intros. + all: abstract ( + rewrite Rewrite_eq; cbv [Make.Rewrite]; rewrite rewrite_head_eq, all_rewrite_rules_eq; + first [ apply Compile.Wf_Rewrite; [ | assumption ]; + let wf_do_again := fresh "wf_do_again" in + (intros ? ? ? ? wf_do_again ? ?); + eapply @Compile.wf_assemble_identifier_rewriters; + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct + with nocore; + try reflexivity + | eapply Compile.InterpRewrite; [ | assumption ]; + intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); + eauto using + pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct, pattern.ident.unify_to_typed, + @ident.gen_interp_Proper, eq_refl + with nocore ]). + Defined. + + Ltac make_VerifiedRewriter R RWf RInterp RProofs := + let res := (eval hnf in (@VerifiedRewriter_of_Rewriter R RWf RInterp RProofs)) in + let res := lazymatch res with + | context Res[@Build_VerifiedRewriter ?R] + => let t := fresh "t" in + let R' := fresh in + let R' := constr:(fun t + => match R t return _ with + | R' => ltac:(let v := (eval hnf in R') in exact v) + end) in + context Res[@Build_VerifiedRewriter R'] + end in + res. + + Ltac Build_Rewriter include_interp specs_proofs := + let specs := lazymatch type of specs_proofs with + | PrimitiveHList.hlist (@snd bool Prop) ?specs => specs + | ?T + => let expected_type := uconstr:(PrimitiveHList.hlist (@snd bool Prop) ?[specs]) in + constr_fail_with ltac:(fun _ => fail 1 "Invalid type for specs_proofs:" T "Expected:" expected_type) + end in + let R_name := fresh "Rewriter_data" in + let R := Build_RewriterT include_interp specs in + let R := cache_term R R_name in + let Rwf := fresh "Rewriter_Wf" in + let Rwf := cache_proof_with_type_by (Wf_GoalT R) ltac:(idtac; prove_good ()) Rwf in + let RInterp := fresh "Rewriter_Interp" in + let RInterp := cache_proof_with_type_by (Interp_GoalT R) ltac:(idtac; prove_interp_good ()) RInterp in + make_VerifiedRewriter R Rwf RInterp specs_proofs. + + Module Export GoalType. + Export RewriterWf1.Compilers.RewriteRules.GoalType. + End GoalType. + + Module Export Tactic. + Module Export Settings. + Export Rewriter.Compilers.RewriteRules.Tactic.Settings. + End Settings. + + Ltac make_rewriter include_interp specs_proofs := + let res := Build_Rewriter include_interp specs_proofs in refine res. + + Tactic Notation "make_rewriter" constr(include_interp) constr(specs_proofs) := + make_rewriter include_interp specs_proofs. + End Tactic. + End RewriteRules. +End Compilers. -- cgit v1.2.3