From e832653f2eca18ed149f82a5a488a634a5887ee2 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 9 Aug 2018 17:04:41 -0400 Subject: Better transport lemmas in LanguageInversion After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------------------------------- 19m03.98s | Total | 19m03.09s || +0m00.89s | +0.07% -------------------------------------------------------------------------------------------------------------------- 4m32.38s | Experiments/NewPipeline/Toplevel1 | 4m33.84s || -0m01.46s | -0.53% 0m24.50s | Experiments/NewPipeline/UnderLetsProofs | 0m23.34s || +0m01.16s | +4.97% 5m55.71s | Experiments/NewPipeline/SlowPrimeSynthesisExamples | 5m55.23s || +0m00.47s | +0.13% 1m36.24s | Experiments/NewPipeline/Toplevel2 | 1m36.50s || -0m00.25s | -0.26% 0m39.34s | p521_32.c | 0m39.28s || +0m00.06s | +0.15% 0m38.62s | Experiments/NewPipeline/AbstractInterpretationWf | 0m38.04s || +0m00.57s | +1.52% 0m37.21s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery | 0m37.13s || +0m00.07s | +0.21% 0m35.25s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery | 0m35.00s || +0m00.25s | +0.71% 0m34.16s | Experiments/NewPipeline/LanguageInversion | 0m33.72s || +0m00.43s | +1.30% 0m32.71s | p521_64.c | 0m32.83s || -0m00.11s | -0.36% 0m23.87s | p384_32.c | 0m23.81s || +0m00.06s | +0.25% 0m21.16s | Experiments/NewPipeline/LanguageWf | 0m21.12s || +0m00.03s | +0.18% 0m20.25s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas | 0m20.41s || -0m00.16s | -0.78% 0m18.58s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas | 0m18.61s || -0m00.03s | -0.16% 0m13.59s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas | 0m13.53s || +0m00.06s | +0.44% 0m10.33s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas | 0m10.46s || -0m00.13s | -1.24% 0m08.56s | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml | 0m08.54s || +0m00.02s | +0.23% 0m08.47s | p384_64.c | 0m08.43s || +0m00.04s | +0.47% 0m05.43s | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml | 0m05.50s || -0m00.07s | -1.27% 0m05.39s | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.32s || +0m00.06s | +1.31% 0m04.01s | Experiments/NewPipeline/AbstractInterpretationProofs | 0m04.04s || -0m00.03s | -0.74% 0m04.00s | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml | 0m04.01s || -0m00.00s | -0.24% 0m03.90s | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs | 0m03.96s || -0m00.06s | -1.51% 0m03.84s | Experiments/NewPipeline/MiscCompilerPassesProofs | 0m03.83s || +0m00.00s | +0.26% 0m03.81s | p256_32.c | 0m03.74s || +0m00.06s | +1.87% 0m03.79s | secp256k1_32.c | 0m03.90s || -0m00.10s | -2.82% 0m03.13s | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs | 0m03.15s || -0m00.02s | -0.63% 0m02.09s | curve25519_32.c | 0m02.16s || -0m00.07s | -3.24% 0m02.08s | p224_32.c | 0m02.24s || -0m00.16s | -7.14% 0m01.69s | p224_64.c | 0m01.55s || +0m00.13s | +9.03% 0m01.58s | secp256k1_64.c | 0m01.64s || -0m00.05s | -3.65% 0m01.56s | p256_64.c | 0m01.51s || +0m00.05s | +3.31% 0m01.54s | curve25519_64.c | 0m01.45s || +0m00.09s | +6.20% 0m01.44s | Experiments/NewPipeline/CLI | 0m01.46s || -0m00.02s | -1.36% 0m01.32s | Experiments/NewPipeline/RewriterProofs | 0m01.38s || -0m00.05s | -4.34% 0m01.26s | Experiments/NewPipeline/StandaloneHaskellMain | 0m01.23s || +0m00.03s | +2.43% 0m01.19s | Experiments/NewPipeline/StandaloneOCamlMain | 0m01.20s || -0m00.01s | -0.83% --- src/Experiments/NewPipeline/LanguageInversion.v | 135 +++++++++++++----------- 1 file changed, 73 insertions(+), 62 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v index 825881771..962cabcea 100644 --- a/src/Experiments/NewPipeline/LanguageInversion.v +++ b/src/Experiments/NewPipeline/LanguageInversion.v @@ -90,8 +90,7 @@ Module Compilers. Local Ltac t_red := repeat first [ progress intros - | progress cbn [type.type_beq base.type.type_beq base.type.base_beq base.try_make_transport_cps base.try_make_base_transport_cps eq_rect andb] in * - | progress cbv [cpsreturn cpsbind cps_option_bind Option.bind cpscall] in * ]. + | progress cbn [type.type_beq base.type.type_beq base.type.base_beq base.try_make_transport_cps base.try_make_base_transport_cps eq_rect andb] in * ]. Local Ltac t := repeat first [ progress t_red | reflexivity @@ -110,30 +109,33 @@ Module Compilers. | [ H : _ |- _ ] => rewrite H end ]. - Lemma try_make_base_transport_cps_correct P t1 t2 T k - : base.try_make_base_transport_cps P t1 t2 T k - = k match Sumbool.sumbool_of_bool (base.type.base_beq t1 t2) with - | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_base_dec_bl _ _ pf) in id) - | right _ => None - end. - Proof. revert P t2 T k; induction t1, t2; t. Qed. + Lemma try_make_base_transport_cps_correct P t1 t2 + : base.try_make_base_transport_cps P t1 t2 + = fun T k + => k match Sumbool.sumbool_of_bool (base.type.base_beq t1 t2) with + | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_base_dec_bl _ _ pf) in id) + | right _ => None + end. + Proof. revert P t2; induction t1, t2; t. Qed. - Lemma try_make_transport_cps_correct P t1 t2 T k - : base.try_make_transport_cps P t1 t2 T k - = k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with - | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_type_dec_bl _ _ pf) in id) - | right _ => None - end. - Proof. revert P t2 T k; induction t1, t2; t_red; rewrite ?try_make_base_transport_cps_correct; t. Qed. + Lemma try_make_transport_cps_correct P t1 t2 + : base.try_make_transport_cps P t1 t2 + = fun T k + => k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with + | left pf => Some (rew [fun t => P t1 -> P t] (base.type.internal_type_dec_bl _ _ pf) in id) + | right _ => None + end. + Proof. revert P t2; induction t1, t2; t_red; rewrite ?try_make_base_transport_cps_correct; t. Qed. - Lemma try_transport_cps_correct P t1 t2 v T k - : base.try_transport_cps P t1 t2 v T k - = k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with - | left pf => Some (rew [P] (base.type.internal_type_dec_bl _ _ pf) in v) - | right _ => None - end. + Lemma try_transport_cps_correct P t1 t2 v + : base.try_transport_cps P t1 t2 v + = fun T k + => k match Sumbool.sumbool_of_bool (base.type.type_beq t1 t2) with + | left pf => Some (rew [P] (base.type.internal_type_dec_bl _ _ pf) in v) + | right _ => None + end. Proof. - cbv [base.try_transport_cps cpscall cps_option_bind cpsreturn cpsbind Option.bind]; rewrite try_make_transport_cps_correct; + cbv [base.try_transport_cps]; rewrite try_make_transport_cps_correct; t. Qed. @@ -189,7 +191,8 @@ Module Compilers. end. Ltac inversion_type_step := cbv [defaults.type_base] in *; - first [ lazymatch goal with + first [ base.type.inversion_type_step + | lazymatch goal with | [ H : ?x = ?x :> type.type _ |- _ ] => clear H | [ H : ?x = ?y :> type.type _ |- _ ] => subst x || subst y end @@ -233,12 +236,13 @@ Module Compilers. (base_type_lb : forall t1 t2, t1 = t2 -> base_type_beq t1 t2 = true) (try_make_transport_base_type_cps : forall (P : base_type -> Type) t1 t2, ~> option (P t1 -> P t2)) (try_make_transport_base_type_cps_correct - : forall P t1 t2 T k, - try_make_transport_base_type_cps P t1 t2 T k - = k match Sumbool.sumbool_of_bool (base_type_beq t1 t2) with - | left pf => Some (rew [fun t => P t1 -> P t] (base_type_bl _ _ pf) in id) - | right _ => None - end). + : forall P t1 t2, + try_make_transport_base_type_cps P t1 t2 + = fun T k + => k match Sumbool.sumbool_of_bool (base_type_beq t1 t2) with + | left pf => Some (rew [fun t => P t1 -> P t] (base_type_bl _ _ pf) in id) + | right _ => None + end). Let base_type_eq_dec : DecidableRel (@eq base_type) := dec_rel_of_bool_dec_rel base_type_beq base_type_bl base_type_lb. @@ -266,31 +270,34 @@ Module Compilers. | [ H : _ |- _ ] => rewrite H end ]. - Lemma try_make_transport_cps_correct P t1 t2 T k - : type.try_make_transport_cps try_make_transport_base_type_cps P t1 t2 T k - = k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with - | left pf => Some (rew [fun t => P t1 -> P t] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in id) - | right _ => None - end. - Proof. revert P t2 T k; induction t1, t2; t. Qed. - - Lemma try_transport_cps_correct P t1 t2 v T k - : type.try_transport_cps try_make_transport_base_type_cps P t1 t2 v T k - = k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with - | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v) - | right _ => None - end. + Lemma try_make_transport_cps_correct P t1 t2 + : type.try_make_transport_cps try_make_transport_base_type_cps P t1 t2 + = fun T k + => k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with + | left pf => Some (rew [fun t => P t1 -> P t] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in id) + | right _ => None + end. + Proof. revert P t2; induction t1, t2; t. Qed. + + Lemma try_transport_cps_correct P t1 t2 + : type.try_transport_cps try_make_transport_base_type_cps P t1 t2 + = fun v T k + => k match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with + | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v) + | right _ => None + end. Proof. - cbv [type.try_transport_cps cpscall cps_option_bind cpsreturn cpsbind Option.bind]; rewrite try_make_transport_cps_correct; + cbv [type.try_transport_cps]; rewrite try_make_transport_cps_correct; t. Qed. - Lemma try_transport_correct P t1 t2 v - : type.try_transport try_make_transport_base_type_cps P t1 t2 v - = match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with - | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v) - | right _ => None - end. + Lemma try_transport_correct P t1 t2 + : type.try_transport try_make_transport_base_type_cps P t1 t2 + = fun v + => match Sumbool.sumbool_of_bool (type.type_beq _ base_type_beq t1 t2) with + | left pf => Some (rew [P] (type.internal_type_dec_bl _ _ base_type_bl _ _ pf) in v) + | right _ => None + end. Proof. cbv [type.try_transport]; rewrite try_transport_cps_correct; reflexivity. Qed. End transport_cps. End type. @@ -328,8 +335,7 @@ Module Compilers. Ltac rewrite_type_transport_correct := cbv [type.try_transport_cps type.try_transport base.try_transport base.try_transport_cps] in *; - cbn [type.try_make_transport_cps] in *; - cbv [cpscall cpsbind cps_option_bind cpsreturn id] in *; + cbv [cpsbind cpscall cpsreturn id cps_option_bind] in *; repeat match goal with | [ |- context[type.try_make_transport_cps ?bmt ?P ?t1 ?t2] ] => erewrite type.try_make_transport_cps_correct @@ -341,6 +347,10 @@ Module Compilers. => rewrite base.try_make_transport_cps_correct | [ H : context[base.try_make_transport_cps ?P ?t1 ?t2] |- _ ] => rewrite base.try_make_transport_cps_correct in H + | [ |- context[base.try_make_base_transport_cps ?P ?t1 ?t2] ] + => rewrite base.try_make_base_transport_cps_correct + | [ H : context[base.try_make_base_transport_cps ?P ?t1 ?t2] |- _ ] + => rewrite base.try_make_base_transport_cps_correct in H end. Module ident. @@ -485,13 +495,11 @@ Module Compilers. | discriminate | reflexivity | progress type.inversion_type - | progress base.type.inversion_type | progress invert_match | progress ident.invert_match | progress break_innermost_match_hyps | exists eq_refl; cbn - | progress cbv [type.try_transport type.try_transport_cps type.try_make_transport_cps cpsbind cpscall cps_option_bind cpsreturn id] in * - | rewrite base.try_make_transport_cps_correct in * + | progress rewrite_type_transport_correct | progress type_beq_to_eq | congruence ]. @@ -539,8 +547,7 @@ Module Compilers. Proof. intros T k; subst e; cbn [invert_expr.reflect_list_cps']; cbv [id type_base] in *. rewrite_type_transport_correct; break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect]; try reflexivity. - etransitivity; rewrite rec; clear rec; [ | reflexivity ]; cbv [id]; break_innermost_match; try reflexivity. - all: do 2 (rewrite_type_transport_correct; break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect]; try reflexivity). + all: etransitivity; rewrite rec; clear rec; [ | reflexivity ]; cbv [id]; break_innermost_match; try reflexivity. Qed. @@ -571,7 +578,7 @@ Module Compilers. end. Proof. type.invert_one e; cbv [invert_expr.invert_nil invert_expr.invert_Ident type_base]; try reflexivity; - [ ident.invert_match; cbv [type_base] in *; base.type.inversion_type; reflexivity | ]. + [ ident.invert_match; cbv [type_base] in *; type.inversion_type; reflexivity | ]. do 2 (let f := match goal with f : expr (_ -> _) |- _ => f end in type.invert_one f; try reflexivity; []). cbv [type_base] in *; ident.invert; break_innermost_match_hyps; subst; destruct_head' False; try reflexivity; []. @@ -579,9 +586,13 @@ Module Compilers. cbv [invert_expr.reflect_list invert_expr.invert_cons invert_expr.invert_AppIdent2 invert_expr.invert_App2 invert_expr.invert_App Option.bind invert_expr.invert_Ident]. cbv [invert_expr.reflect_list_cps]. cbn [invert_expr.reflect_list_cps']. - rewrite_type_transport_correct; break_innermost_match_step; type_beq_to_eq; try discriminate; base.type.inversion_type; []. - rewrite reflect_list_cps'_id; cbv [id]; break_innermost_match; try reflexivity; []. - rewrite_type_transport_correct; break_innermost_match_step; type_beq_to_eq; base.type.inversion_type; try discriminate; reflexivity. + repeat first [ reflexivity + | discriminate + | progress rewrite_type_transport_correct + | progress type_beq_to_eq + | progress break_innermost_match + | progress type.inversion_type + | rewrite reflect_list_cps'_id; reflexivity ]. Qed. Lemma reify_list_nil {t} : reify_list nil = ([])%expr :> expr (base.type.list t). -- cgit v1.2.3