From 1384a29170bbb8b166b90f73bafea8d1948568af Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 9 Apr 2019 21:27:59 -0400 Subject: Replace the python script with Ltac code We now rely on Ltac rather than python to generate the raw identifiers. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 22m05.90s | Total | 21m51.87s || +0m14.03s | +1.07% ----------------------------------------------------------------------------------------------- 0m49.25s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m55.23s || -0m05.97s | -10.82% 0m19.14s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.35s || +0m05.79s | +43.37% 0m36.52s | ExtractionHaskell/saturated_solinas | 0m32.60s || +0m03.92s | +12.02% 0m24.00s | SlowPrimeSynthesisExamples.vo | 0m27.22s || -0m03.21s | -11.82% 0m08.55s | ExtractionOCaml/saturated_solinas.ml | 0m05.49s || +0m03.06s | +55.73% 3m24.98s | p384_32.c | 3m22.52s || +0m02.45s | +1.21% 1m03.78s | ExtractionHaskell/word_by_word_montgomery | 1m01.13s || +0m02.64s | +4.33% 0m47.85s | p521_32.c | 0m45.77s || +0m02.07s | +4.54% 1m42.64s | Fancy/Barrett256.vo | 1m41.49s || +0m01.14s | +1.13% 0m40.30s | p521_64.c | 0m42.20s || -0m01.90s | -4.50% 0m18.02s | p256_32.c | 0m19.03s || -0m01.01s | -5.30% 0m14.70s | ExtractionOCaml/unsaturated_solinas | 0m13.33s || +0m01.36s | +10.27% 0m14.28s | p434_64.c | 0m15.39s || -0m01.11s | -7.21% 0m09.82s | p224_32.c | 0m08.77s || +0m01.05s | +11.97% 0m08.59s | p384_64.c | 0m07.36s || +0m01.22s | +16.71% 0m05.18s | ExtractionHaskell/saturated_solinas.hs | 0m06.59s || -0m01.41s | -21.39% 1m34.02s | RewriterWf2.vo | 1m34.23s || -0m00.20s | -0.22% 0m56.16s | Rewriter/ToFancyWithCasts.vo | 0m55.41s || +0m00.75s | +1.35% 0m45.85s | Rewriter/NBE.vo | 0m45.23s || +0m00.62s | +1.37% 0m44.51s | Rewriter/ArithWithCasts.vo | 0m44.12s || +0m00.39s | +0.88% 0m44.10s | RewriterInterpProofs1.vo | 0m43.89s || +0m00.21s | +0.47% 0m43.66s | ExtractionHaskell/unsaturated_solinas | 0m43.25s || +0m00.40s | +0.94% 0m36.46s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.36s || +0m00.10s | +0.27% 0m36.09s | RewriterWf1.vo | 0m36.07s || +0m00.02s | +0.05% 0m34.50s | Fancy/Montgomery256.vo | 0m34.30s || +0m00.20s | +0.58% 0m27.13s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.99s || +0m00.14s | +0.51% 0m24.70s | Rewriter/Arith.vo | 0m24.26s || +0m00.43s | +1.81% 0m22.75s | ExtractionOCaml/word_by_word_montgomery | 0m22.15s || +0m00.60s | +2.70% 0m20.96s | PushButtonSynthesis/BarrettReduction.vo | 0m20.74s || +0m00.22s | +1.06% 0m18.96s | p448_solinas_64.c | 0m19.32s || -0m00.35s | -1.86% 0m18.16s | secp256k1_32.c | 0m18.13s || +0m00.03s | +0.16% 0m14.62s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.77s || +0m00.84s | +6.17% 0m11.84s | ExtractionOCaml/saturated_solinas | 0m11.30s || +0m00.53s | +4.77% 0m09.55s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.14s || +0m00.41s | +4.48% 0m08.42s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.16s || +0m00.25s | +3.18% 0m06.96s | BoundsPipeline.vo | 0m06.85s || +0m00.11s | +1.60% 0m06.54s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.17s || -0m00.62s | -8.78% 0m03.57s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.10s | +3.17% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.01s | +0.29% 0m03.30s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || +0m00.07s | +2.48% 0m02.83s | curve25519_32.c | 0m02.86s || -0m00.02s | -1.04% 0m02.70s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s || +0m00.07s | +2.66% 0m02.08s | Rewriter.vo | 0m02.02s || +0m00.06s | +2.97% 0m01.60s | curve25519_64.c | 0m01.82s || -0m00.21s | -12.08% 0m01.47s | secp256k1_64.c | 0m01.94s || -0m00.47s | -24.22% 0m01.34s | p224_64.c | 0m01.71s || -0m00.36s | -21.63% 0m01.33s | CLI.vo | 0m01.38s || -0m00.04s | -3.62% 0m01.32s | p256_64.c | 0m01.77s || -0m00.44s | -25.42% 0m01.28s | Rewriter/ToFancy.vo | 0m01.36s || -0m00.08s | -5.88% 0m01.23s | Rewriter/StripLiteralCasts.vo | 0m01.08s || +0m00.14s | +13.88% 0m01.16s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.02s | -1.69% 0m01.13s | CompilersTestCases.vo | 0m01.18s || -0m00.05s | -4.23% 0m01.07s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.05s | -4.46% 0m00.83s | RewriterAll.vo | 0m00.66s || +0m00.16s | +25.75% 0m00.78s | RewriterAllTactics.vo | 0m00.83s || -0m00.04s | -6.02% --- src/GENERATEDIdentifiersWithoutTypesProofs.v | 89 ++++++++++++---------------- 1 file changed, 37 insertions(+), 52 deletions(-) (limited to 'src/GENERATEDIdentifiersWithoutTypesProofs.v') diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v index 9094a8a98..2bab688dc 100644 --- a/src/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v @@ -84,7 +84,8 @@ Module Compilers. Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident. Import Datatypes. (* for Some, None, option *) - Global Instance eq_ident_Decidable : DecidableRel (@eq ident) := ident_eq_dec. + Global Instance eq_ident_Decidable : DecidableRel (@eq ident) + := dec_rel_of_bool_dec_rel ident_beq ident_bl ident_lb. Lemma to_typed_invert_bind_args_gen t idc p f : @invert_bind_args t idc p = Some f @@ -116,30 +117,45 @@ Module Compilers. exact (proj2_sig (@to_typed_invert_bind_args_gen t idc p f pf)). Defined. + Lemma invert_bind_args_to_typed p f + : invert_bind_args (to_typed p f) p = Some f. + Proof. + destruct p; cbn in *; + repeat first [ reflexivity + | progress destruct_head'_unit + | progress destruct_head'_prod + | progress destruct_head' (@PrimitiveSigma.Primitive.sigT) ]. + Qed. + + Lemma is_simple_correct0 p + : is_simple p = true + <-> (forall f1 f2, type_of p f1 = type_of p f2). + Proof. + destruct p; cbn; split; intro H; + try solve [ reflexivity | exfalso; discriminate ]. + all: repeat first [ match goal with + | [ H : nat -> ?A |- _ ] => specialize (H O) + | [ H : unit -> ?A |- _ ] => specialize (H tt) + | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H + | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H + | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y)) + | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H + end + | congruence ]. + Qed. + Lemma is_simple_correct p : is_simple p = true <-> (forall t1 idc1 t2 idc2, @invert_bind_args t1 idc1 p <> None -> @invert_bind_args t2 idc2 p <> None -> t1 = t2). Proof. - split; intro H; - [ | specialize (fun f1 f2 => H _ (@to_typed p f1) _ (@to_typed p f2)) ]; - destruct p; cbn in *; try solve [ reflexivity | exfalso; discriminate ]; - repeat first [ progress intros * - | match goal with - | [ |- ?x = ?x ] => reflexivity - | [ |- ?x = ?x -> _ ] => intros _ - | [ |- None <> None -> ?P ] => exact (@quick_invert_neq_option _ P None None) - | [ |- Some _ <> None -> _ ] => intros _ - | [ |- None <> Some _ -> _ ] => intros _ - | [ H : forall x y, Some _ <> None -> _ |- _ ] => specialize (fun x y => H x y Some_neq_None) - | [ H : nat -> ?A |- _ ] => specialize (H O) - | [ H : unit -> ?A |- _ ] => specialize (H tt) - | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H - | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H - | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y)) - | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H - end - | break_innermost_match_step - | congruence ]. + rewrite is_simple_correct0; split; intro H. + { intros t1 idc1 t2 idc2 H1 H2. + destruct (invert_bind_args idc1 p) eqn:?, (invert_bind_args idc2 p) eqn:?; try congruence. + erewrite (type_of_invert_bind_args t1), (type_of_invert_bind_args t2) by eassumption. + apply H. } + { intros f1 f2. + apply (H _ (to_typed p f1) _ (to_typed p f2)); + rewrite invert_bind_args_to_typed; congruence. } Qed. End ident. End Raw. @@ -152,13 +168,6 @@ Module Compilers. : @eta_ident_cps T t idc f = f t idc. Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed. -(* - Lemma is_simple_strip_types_iff_type_vars_nil {t} idc - : Raw.ident.is_simple (@strip_types t idc) = true - <-> type_vars idc = List.nil. - Proof. destruct idc; cbn; intuition congruence. Qed. -*) - Lemma unify_to_typed {t t' pidc idc} : forall v, @unify t t' pidc idc = Some v @@ -180,30 +189,6 @@ Module Compilers. Proof. destruct idc; cbn; break_innermost_match; exact Some_neq_None. Qed. - - Lemma to_typed_of_typed_ident {t idc} - : forall v, - unify (@of_typed_ident t idc) idc = Some v - -> forall evm pf, - (rew [Compilers.ident] pf in to_typed (@of_typed_ident t idc) evm v) - = idc. - Proof. - destruct idc. - all: repeat first [ break_innermost_match_step - | break_innermost_match_hyps_step - | progress intros - | reflexivity - | progress subst - | progress inversion_option - | progress eliminate_hprop_eq - | progress fold (@base.subst_default) - | progress cbn in * - | lazymatch goal with - | [ H : context[base.subst_default (base.relax ?t) ?evm] |- _ ] - => generalize dependent (base.subst_default (base.relax t) evm) - end - | progress Compilers.type.inversion_type ]. - Qed. End ident. End pattern. End Compilers. -- cgit v1.2.3