From 067d1f14b03d83dcb1c0a60808919ceff6205836 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 3 Apr 2019 16:43:48 -0400 Subject: Automate more of the rewriter reification, proof Now we actually make use of the rewrite-rule-specific proofs, rather than duplicating them inline. We now support reifying `ident.gets_inlined` to `SubstVarLike.is_var_fst_snd_pair_opp_cast`. We also now fix a bug where we previously incorrectly substituted context variables when reifying side conditions (needed for correct reification of split-mul things, coming up soon). Things are unfortunately a bit slow. I'm not sure what's up with my proof of `reflect_ident_iota_interp_related`; it seems more complicated than it should be (maybe partly due to funext concerns). Next up is to split out the rewrite rule generation bits into separate files and have a single tactic that builds the entire package for us (in prep for making the rewriter builder a vernacular). After that I want to more fully parameterize things over `ident`, and then also over the non-container base-types (which will require some reworking of how we handle special identifiers). Additionally, I want to make the rewrite rule definitions not depend on Language.v. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 20m50.18s | Total | 23m01.24s || -2m11.06s | -9.48% ----------------------------------------------------------------------------------------------- 0m27.24s | RewriterRulesGood.vo | 1m34.94s || -1m07.70s | -71.30% 0m54.89s | RewriterRulesInterpGood.vo | 1m57.72s || -1m02.82s | -53.37% 1m37.88s | RewriterWf2.vo | 1m47.69s || -0m09.81s | -9.10% 1m16.71s | Rewriter.vo | 1m12.61s || +0m04.10s | +5.64% 0m37.14s | ExtractionHaskell/unsaturated_solinas | 0m40.06s || -0m02.92s | -7.28% 0m36.10s | RewriterWf1.vo | 0m33.12s || +0m02.98s | +8.99% 0m18.31s | p256_32.c | 0m20.70s || -0m02.39s | -11.54% 1m43.31s | Fancy/Barrett256.vo | 1m42.09s || +0m01.21s | +1.19% 0m32.46s | ExtractionHaskell/saturated_solinas | 0m30.92s || +0m01.53s | +4.98% 0m23.44s | ExtractionOCaml/word_by_word_montgomery | 0m22.26s || +0m01.17s | +5.30% 0m12.17s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.58s || -0m01.41s | -10.38% 0m10.04s | p224_32.c | 0m08.20s || +0m01.83s | +22.43% 0m09.98s | ExtractionOCaml/saturated_solinas | 0m11.67s || -0m01.68s | -14.48% 0m07.80s | ExtractionOCaml/saturated_solinas.ml | 0m06.16s || +0m01.63s | +26.62% 0m06.87s | ExtractionHaskell/saturated_solinas.hs | 0m04.98s || +0m01.88s | +37.95% 3m23.11s | p384_32.c | 3m22.61s || +0m00.50s | +0.24% 0m59.32s | ExtractionHaskell/word_by_word_montgomery | 0m58.76s || +0m00.56s | +0.95% 0m46.19s | p521_32.c | 0m47.16s || -0m00.96s | -2.05% 0m45.26s | RewriterInterpProofs1.vo | 0m45.64s || -0m00.38s | -0.83% 0m39.50s | p521_64.c | 0m38.97s || +0m00.53s | +1.36% 0m36.38s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.00s || +0m00.38s | +1.05% 0m34.40s | Fancy/Montgomery256.vo | 0m34.63s || -0m00.23s | -0.66% 0m26.95s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.44s || +0m00.50s | +1.92% 0m25.62s | SlowPrimeSynthesisExamples.vo | 0m26.04s || -0m00.41s | -1.61% 0m24.39s | RewriterRulesProofs.vo | 0m24.18s || +0m00.21s | +0.86% 0m20.49s | PushButtonSynthesis/BarrettReduction.vo | 0m20.62s || -0m00.13s | -0.63% 0m18.54s | p448_solinas_64.c | 0m19.15s || -0m00.60s | -3.18% 0m17.37s | secp256k1_32.c | 0m17.70s || -0m00.32s | -1.86% 0m14.80s | p434_64.c | 0m14.16s || +0m00.64s | +4.51% 0m14.05s | ExtractionOCaml/unsaturated_solinas | 0m14.28s || -0m00.22s | -1.61% 0m09.17s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.58s || -0m00.41s | -4.27% 0m08.47s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.22s || +0m00.25s | +3.04% 0m07.69s | p384_64.c | 0m07.72s || -0m00.02s | -0.38% 0m06.80s | BoundsPipeline.vo | 0m06.65s || +0m00.14s | +2.25% 0m06.49s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.59s || +0m00.90s | +16.10% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.08s | +2.31% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.36s || -0m00.00s | -0.29% 0m03.19s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.15s || +0m00.04s | +1.26% 0m02.79s | curve25519_32.c | 0m03.32s || -0m00.52s | -15.96% 0m02.66s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.73s || -0m00.06s | -2.56% 0m02.55s | RewriterRules.vo | 0m02.52s || +0m00.02s | +1.19% 0m01.98s | curve25519_64.c | 0m01.57s || +0m00.40s | +26.11% 0m01.78s | p224_64.c | 0m01.30s || +0m00.48s | +36.92% 0m01.60s | secp256k1_64.c | 0m01.74s || -0m00.13s | -8.04% 0m01.45s | p256_64.c | 0m01.55s || -0m00.10s | -6.45% 0m01.34s | RewriterProofs.vo | 0m01.16s || +0m00.18s | +15.51% 0m01.33s | CLI.vo | 0m01.40s || -0m00.06s | -4.99% 0m01.12s | StandaloneOCamlMain.vo | 0m01.09s || +0m00.03s | +2.75% 0m01.10s | CompilersTestCases.vo | 0m01.08s || +0m00.02s | +1.85% 0m01.08s | StandaloneHaskellMain.vo | 0m01.02s || +0m00.06s | +5.88% --- src/RewriterProofs.v | 64 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 38 insertions(+), 26 deletions(-) (limited to 'src/RewriterProofs.v') diff --git a/src/RewriterProofs.v b/src/RewriterProofs.v index 0587aec51..6da5a9e47 100644 --- a/src/RewriterProofs.v +++ b/src/RewriterProofs.v @@ -13,6 +13,7 @@ Require Import Crypto.Rewriter. Require Import Crypto.RewriterWf1. Require Import Crypto.RewriterWf2. Require Import Crypto.RewriterInterpProofs1. +Require Import Crypto.RewriterRulesProofs. Require Import Crypto.RewriterRulesGood. Require Import Crypto.RewriterRulesInterpGood. Require Import Crypto.Util.Tactics.BreakMatch. @@ -54,14 +55,25 @@ Module Compilers. Module Import RewriteRules. - Local Ltac start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := + Local Ltac start_Wf_or_interp_proof Rewrite_folded := let Rewrite := lazymatch goal with | [ |- Wf ?e ] => head e | [ |- expr.Interp _ ?e == _ ] => head e end in - cbv [Rewrite]; rewrite rewrite_head_eq; cbv [rewrite_head0]; rewrite all_rewrite_rules_eq. - Local Ltac start_Wf_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := - start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0; + progress change Rewrite with Rewrite_folded; cbv [Rewrite_folded]; + let data := lazymatch goal with |- context[Make.Rewrite ?data] => data end in + let data_head := head data in + cbv [Make.Rewrite]; + rewrite (rewrite_head_eq data); + let lem := fresh in + pose proof (all_rewrite_rules_eq data) as lem; + cbv [data_head rewrite_head0 default_fuel all_rewrite_rules rewrite_rules]; + unfold data_head at 1 in lem; + cbv [all_rewrite_rules] in lem; + let h := lazymatch goal with |- context[Compile.Rewrite ?rewrite_head] => head rewrite_head end in + cbv [h]; rewrite lem; clear lem. + Local Ltac start_Wf_proof Rewrite_folded := + start_Wf_or_interp_proof Rewrite_folded; apply Compile.Wf_Rewrite; [ | assumption ]; let wf_do_again := fresh "wf_do_again" in (intros ? ? ? ? wf_do_again ? ?); @@ -70,8 +82,8 @@ Module Compilers. pattern.Raw.ident.to_typed_invert_bind_args, pattern.ident.eta_ident_cps_correct with nocore; try reflexivity. - Local Ltac start_Interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0 := - start_Wf_or_interp_proof rewrite_head_eq all_rewrite_rules_eq rewrite_head0; + Local Ltac start_Interp_proof Rewrite_folded := + start_Wf_or_interp_proof Rewrite_folded; eapply Compile.InterpRewrite; [ | assumption ]; intros; eapply Compile.interp_assemble_identifier_rewriters with (pident_to_typed:=@pattern.ident.to_typed); eauto using @@ -81,22 +93,22 @@ Module Compilers. Lemma Wf_RewriteNBE {t} e (Hwf : Wf e) : Wf (@RewriteNBE t e). Proof. - start_Wf_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0). + start_Wf_proof RewriteNBE_folded. apply nbe_rewrite_rules_good. Qed. Lemma Wf_RewriteArith (max_const_val : Z) {t} e (Hwf : Wf e) : Wf (@RewriteArith max_const_val t e). Proof. - start_Wf_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). + start_Wf_proof RewriteArith_folded. apply arith_rewrite_rules_good. Qed. Lemma Wf_RewriteArithWithCasts {t} e (Hwf : Wf e) : Wf (@RewriteArithWithCasts t e). Proof. - start_Wf_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0). + start_Wf_proof RewriteArithWithCasts_folded. apply arith_with_casts_rewrite_rules_good. Qed. Lemma Wf_RewriteStripLiteralCasts {t} e (Hwf : Wf e) : Wf (@RewriteStripLiteralCasts t e). Proof. - start_Wf_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0). + start_Wf_proof RewriteStripLiteralCasts_folded. apply strip_literal_casts_rewrite_rules_good. Qed. Lemma Wf_RewriteToFancy (invert_low invert_high : Z -> Z -> option Z) @@ -104,8 +116,8 @@ Module Compilers. (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) {t} e (Hwf : Wf e) : Wf (@RewriteToFancy invert_low invert_high t e). Proof. - start_Wf_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). - eapply fancy_rewrite_rules_good; eassumption. + start_Wf_proof RewriteToFancy_folded. + apply fancy_rewrite_rules_good; assumption. Qed. Lemma Wf_RewriteToFancyWithCasts (invert_low invert_high : Z -> Z -> option Z) @@ -114,39 +126,39 @@ Module Compilers. (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2)) {t} e (Hwf : Wf e) : Wf (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e). Proof. - start_Wf_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0). - eapply fancy_with_casts_rewrite_rules_good; eassumption. + start_Wf_proof RewriteToFancyWithCasts_folded. + apply fancy_with_casts_rewrite_rules_good; assumption. Qed. Lemma Interp_gen_RewriteNBE {cast_outside_of_range t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteNBE t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof nbe_rewrite_head_eq nbe_all_rewrite_rules_eq (@nbe_rewrite_head0). - apply nbe_rewrite_rules_interp_good. + start_Interp_proof RewriteNBE_folded. + apply nbe_rewrite_rules_interp_good, nbe_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteArith {cast_outside_of_range} (max_const_val : Z) {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArith max_const_val t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof arith_rewrite_head_eq arith_all_rewrite_rules_eq (@arith_rewrite_head0). - apply arith_rewrite_rules_interp_good. + start_Interp_proof RewriteArith_folded. + apply arith_rewrite_rules_interp_good, arith_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteArithWithCasts {cast_outside_of_range} {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteArithWithCasts t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof arith_with_casts_rewrite_head_eq arith_with_casts_all_rewrite_rules_eq (@arith_with_casts_rewrite_head0). - apply arith_with_casts_rewrite_rules_interp_good. + start_Interp_proof RewriteArithWithCasts_folded. + apply arith_with_casts_rewrite_rules_interp_good, arith_with_casts_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteStripLiteralCasts {cast_outside_of_range} {t} e (Hwf : Wf e) : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteStripLiteralCasts t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof strip_literal_casts_rewrite_head_eq strip_literal_casts_all_rewrite_rules_eq (@strip_literal_casts_rewrite_head0). - apply strip_literal_casts_rewrite_rules_interp_good. + start_Interp_proof RewriteStripLiteralCasts_folded. + apply strip_literal_casts_rewrite_rules_interp_good, strip_literal_casts_rewrite_rules_proofs. Qed. Lemma Interp_gen_RewriteToFancy {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) @@ -156,8 +168,8 @@ Module Compilers. : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancy invert_low invert_high t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof fancy_rewrite_head_eq fancy_all_rewrite_rules_eq (@fancy_rewrite_head0). - eapply fancy_rewrite_rules_interp_good; eassumption. + start_Interp_proof RewriteToFancy_folded. + apply fancy_rewrite_rules_interp_good; try assumption; apply fancy_rewrite_rules_proofs; assumption. Qed. Lemma Interp_gen_RewriteToFancyWithCasts {cast_outside_of_range} (invert_low invert_high : Z -> Z -> option Z) @@ -168,8 +180,8 @@ Module Compilers. : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteToFancyWithCasts invert_low invert_high value_range flag_range t e) == expr.Interp (@ident.gen_interp cast_outside_of_range) e. Proof. - start_Interp_proof fancy_with_casts_rewrite_head_eq fancy_with_casts_all_rewrite_rules_eq (@fancy_with_casts_rewrite_head0). - eapply fancy_with_casts_rewrite_rules_interp_good; eassumption. + start_Interp_proof RewriteToFancyWithCasts_folded. + apply fancy_with_casts_rewrite_rules_interp_good; try assumption; apply fancy_with_casts_rewrite_rules_proofs; assumption. Qed. Lemma Interp_RewriteNBE {t} e (Hwf : Wf e) : Interp (@RewriteNBE t e) == Interp e. -- cgit v1.2.3