diff options
19 files changed, 554 insertions, 417 deletions
diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v index 62ff363e2..18cee5114 100644 --- a/src/Specific/IntegrationTestFreeze.v +++ b/src/Specific/IntegrationTestFreeze.v @@ -42,33 +42,28 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => B.Positional.Fdecode wt (BoundedWordToZ _ _ _ x). + Lemma feBW_bounded (a : feBW) + : 0 <= B.Positional.eval wt (BoundedWordToZ sz bitwidth bounds a) < 2 * Z.pos m. + Proof. + destruct a as [a H]; unfold BoundedWordToZ, proj1_sig. + revert H. + cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd]. + repeat match goal with + | [ |- context[wt ?n] ] + => let v := (eval compute in (wt n)) in change (wt n) with v + end. + intro; destruct_head'_and. + omega. + Qed. + (* TODO : change this to field once field isomorphism happens *) Definition freeze : { freeze : feBW -> feBW | forall a, phi (freeze a) = phi a }. Proof. - lazymatch goal with - | [ |- { f | forall a, ?phi (f a) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => phi f = rhs a) - end. - intros a. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig freeze_sig). - { set (freezeZ := proj1_sig freeze_sig). - context_to_dlet_in_rhs freezeZ. - cbv beta iota delta [freezeZ proj1_sig freeze_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. } - { destruct a as [a H]; unfold BoundedWordToZ, proj1_sig. - revert H. - cbv -[Z.le Z.add Z.mul Z.lt fst snd wordToZ wt]; cbn [fst snd]. - repeat match goal with - | [ |- context[wt ?n] ] - => let v := (eval compute in (wt n)) in change (wt n) with v - end. - intro; destruct_head'_and. - omega. } - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). + start_preglue. + do_rewrite_with_sig_by freeze_sig ltac:(fun _ => apply feBW_bounded); cbv_runtime. + all:fin_preglue. (* jgross start here! *) (*Set Ltac Profiling.*) Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *) diff --git a/src/Specific/IntegrationTestKaratsubaMul.v b/src/Specific/IntegrationTestKaratsubaMul.v index 9dc49ca00..0a29973a1 100644 --- a/src/Specific/IntegrationTestKaratsubaMul.v +++ b/src/Specific/IntegrationTestKaratsubaMul.v @@ -46,21 +46,9 @@ Section BoundedField25p5. { mul : feBW -> feBW -> feBW | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi f = rhs a b) - end. - intros a b. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig mul_sig). - symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)). - change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b). - context_to_dlet_in_rhs carry_mulZ. - cbv beta iota delta [carry_mulZ proj1_sig mul_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). + start_preglue. + do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime. + all:fin_preglue. (* jgross start here! *) (*Set Ltac Profiling.*) Time refine_reflectively. diff --git a/src/Specific/IntegrationTestLadderstep130.v b/src/Specific/IntegrationTestLadderstep130.v index 541dcaee8..4dd01d018 100644 --- a/src/Specific/IntegrationTestLadderstep130.v +++ b/src/Specific/IntegrationTestLadderstep130.v @@ -77,12 +77,7 @@ Section BoundedField25p5. /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. - lazymatch goal with - | [ |- { op | forall (a:?A) (b:?B) (c:?C), - let v := op a b c in - @?P a b c v } ] - => refine (@lift3_sig A B C _ P _) - end. + apply_lift_sig. intros a b c; cbv beta iota zeta. lazymatch goal with | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] @@ -102,11 +97,12 @@ Section BoundedField25p5. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. context_to_dlet_in_rhs (@M.xzladderstep _ _ _ _ _). cbv [M.xzladderstep a24_sig]. - do 4 lazymatch goal with - | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] - => context_to_dlet_in_rhs (@proj1_sig a b f_sig) - end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. + repeat lazymatch goal with + | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] + => context_to_dlet_in_rhs (@proj1_sig a b f_sig) + end. + cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig]. + cbv_runtime. refine (proj2 FINAL). } subst feW feW_bounded; cbv beta. (* jgross start here! *) diff --git a/src/Specific/IntegrationTestMontgomeryP256_128.v b/src/Specific/IntegrationTestMontgomeryP256_128.v index 00f751908..feca5ad9a 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition mul : { mul : feBW_small -> feBW_small -> feBW_small | forall A B, phi (mul A B) = F.mul (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig mulmod_256)) - by (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig mulmod_256)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (mulmodZ := proj1_sig mulmod_256). - context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ]. - cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by mulmod_256 op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v index 367f63a0b..a9fea3ef1 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Add.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Add.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition add : { add : feBW_small -> feBW_small -> feBW_small | forall A B, phi (add A B) = F.add (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig add)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig add)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (addZ := proj1_sig add). - context_to_dlet_in_rhs addZ; cbv [addZ]. - cbv beta iota delta [add add' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by add op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v index 6adeac3f9..3c605e348 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Nonzero.v @@ -44,18 +44,16 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition nonzero : { nonzero : feBW_small -> BoundedWord 1 bitwidth bound1 | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }. Proof. - lazymatch goal with - | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a) - end. - intros a. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. + apply_lift_sig; intros; eexists_sig_etransitivity. + all:cbv [feBW_of_feBW_small phi eval]. refine (_ : (if Decidable.dec (_ = 0) then true else false) = _). lazymatch goal with | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ] @@ -65,7 +63,7 @@ Section BoundedField25p5. | ] end. etransitivity; [ | eapply (proj2_sig nonzero) ]; - [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ]. + [ | solve [ op_sig_side_conditions_t () ].. ]. reflexivity. let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _). @@ -78,9 +76,8 @@ Section BoundedField25p5. try reflexivity. Z.ltb_to_lt; congruence. } } eexists_sig_etransitivity. - set (nonzeroZ := proj1_sig nonzero). - context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ]. - cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. + do_set_sig nonzero. + cbv_runtime. reflexivity. sig_dlet_in_rhs_to_context. match goal with diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v index 1a609d7b4..1869a7952 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Opp.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition opp : { opp : feBW_small -> feBW_small | forall A, phi (opp A) = F.opp (phi A) }. Proof. - lazymatch goal with - | [ |- { f | forall a, ?phi (?proj (f a)) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => phi (proj f) = rhs a) - end. - intros a. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig opp)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig opp)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (oppZ := proj1_sig opp). - context_to_dlet_in_rhs oppZ; cbv [oppZ]. - cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by opp op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v index 916659ab5..62b1ef328 100644 --- a/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v +++ b/src/Specific/IntegrationTestMontgomeryP256_128_Sub.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition sub : { sub : feBW_small -> feBW_small -> feBW_small | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig sub)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig sub)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (subZ := proj1_sig sub). - context_to_dlet_in_rhs subZ; cbv [subZ]. - cbv beta iota delta [sub sub' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by sub op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v index 4e012486c..2e46d22eb 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -1,6 +1,12 @@ (*** XXX TODO MOVE ALL THINGS IN THIS FILE TO BETTER PLACES *) +Require Import Coq.ZArith.BinInt. Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.Tuple. +Require Import Crypto.Util.Sigma.Lift. +Require Import Crypto.Util.Sigma.Associativity. +Require Import Crypto.Util.Sigma.MapProjections. +Require Import Crypto.Util.Tactics.MoveLetIn. +Require Import Crypto.Util.Tactics.DestructHead. Definition adjust_tuple2_tuple2_sig {A P Q} (v : { a : { a : tuple (tuple A 2) 2 | (P (fst (fst a)) /\ P (snd (fst a))) /\ (P (fst (snd a)) /\ P (snd (snd a))) } @@ -78,3 +84,113 @@ Definition sig_conj_by_impl2 {A} {P Q : A -> Prop} (H : forall a : A, Q a -> P a (H' : { a : A | Q a }) : { a : A | P a /\ Q a } := let (a, p) := H' in exist _ a (conj (H a p) p). + + +(** [apply_lift_sig] picks out which version of the [liftN_sig] lemma + to apply, and builds the appropriate arguments *) +Ltac make_P_for_apply_lift_sig P := + lazymatch P with + | fun (f : ?F) => forall (a : ?A), @?P f a + => constr:(fun (a : A) + => ltac:(lazymatch constr:(fun (f : F) + => ltac:(let v := (eval cbv beta in (P f a)) in + lazymatch (eval pattern (f a) in v) with + | ?k _ => exact k + end)) + with + | fun _ => ?P + => let v := make_P_for_apply_lift_sig P in + exact v + end)) + | _ => P + end. +Ltac apply_lift_sig := + let P := lazymatch goal with |- sig ?P => P end in + let P := make_P_for_apply_lift_sig P in + lazymatch goal with + | [ |- { f | forall a b c d e, _ } ] + => fail "apply_lift_sig does not yet support ≥ 5 binders" + | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C) (d : ?D), _ } ] + => apply (@lift4_sig A B C D _ P) + | [ |- { f | forall (a : ?A) (b : ?B) (c : ?C), _ } ] + => apply (@lift3_sig A B C _ P) + | [ |- { f | forall (a : ?A) (b : ?B), _ } ] + => apply (@lift2_sig A B _ P) + | [ |- { f | forall (a : ?A), _ } ] + => apply (@lift1_sig A _ P) + | [ |- { f | _ } ] + => idtac + end. +Ltac start_preglue := + apply_lift_sig; intros; + let phi := lazymatch goal with |- { f | ?phi _ = _ } => phi end in + eexists_sig_etransitivity; cbv [phi]. +Ltac do_set_sig f_sig := + let fZ := fresh f_sig in + set (fZ := proj1_sig f_sig); + context_to_dlet_in_rhs fZ; cbv beta delta [fZ]; + try cbv beta iota delta [proj1_sig f_sig]; + cbv beta iota delta [fst snd]. +Ltac do_rewrite_with_sig_by f_sig by_tac := + let lem := constr:(proj2_sig f_sig) in + let lemT := type of lem in + let lemT := (eval cbv beta zeta in lemT) in + rewrite <- (lem : lemT) by by_tac (); + do_set_sig f_sig. +Ltac do_rewrite_with_sig f_sig := do_rewrite_with_sig_by f_sig ltac:(fun _ => idtac). +Ltac do_rewrite_with_1sig_add_carry_by f_sig carry_sig by_tac := + let fZ := fresh f_sig in + rewrite <- (proj2_sig f_sig) by by_tac (); + symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry; + pose (fun a => proj1_sig carry_sig (proj1_sig f_sig a)) as fZ; + lazymatch goal with + | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a)] ] + => let G' := context G[fZ a] in change G' + end; + context_to_dlet_in_rhs fZ; cbv beta delta [fZ]; + try cbv beta iota delta [proj1_sig f_sig carry_sig]; + cbv beta iota delta [fst snd]. +Ltac do_rewrite_with_1sig_add_carry f_sig carry_sig := do_rewrite_with_1sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac). +Ltac do_rewrite_with_2sig_add_carry_by f_sig carry_sig by_tac := + let fZ := fresh f_sig in + rewrite <- (proj2_sig f_sig) by by_tac (); + symmetry; rewrite <- (proj2_sig carry_sig) by by_tac (); symmetry; + pose (fun a b => proj1_sig carry_sig (proj1_sig f_sig a b)) as fZ; + lazymatch goal with + | [ |- context G[proj1_sig carry_sig (proj1_sig f_sig ?a ?b)] ] + => let G' := context G[fZ a b] in change G' + end; + context_to_dlet_in_rhs fZ; cbv beta delta [fZ]; + try cbv beta iota delta [proj1_sig f_sig carry_sig]; + cbv beta iota delta [fst snd]. +Ltac do_rewrite_with_2sig_add_carry f_sig carry_sig := do_rewrite_with_2sig_add_carry_by f_sig carry_sig ltac:(fun _ => idtac). +Ltac fin_preglue := + [ > reflexivity + | repeat sig_dlet_in_rhs_to_context; + apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)) ]. + +Ltac factor_out_bounds_and_strip_eval op_bounded op_sig_side_conditions_t := + let feBW_small := lazymatch goal with |- { f : ?feBW_small | _ } => feBW_small end in + Associativity.sig_sig_assoc; + apply sig_conj_by_impl2; + [ let H := fresh in + intros ? H; + try lazymatch goal with + | [ |- (?eval _ < _)%Z ] + => cbv [eval] + end; + rewrite H; clear H; + eapply Z.le_lt_trans; + [ apply Z.eq_le_incl, f_equal | apply op_bounded ]; + [ repeat match goal with + | [ |- ?f ?x = ?g ?y ] + => is_evar y; unify x y; + apply (f_equal (fun fg => fg x)) + end; + clear; abstract reflexivity + | .. ]; + op_sig_side_conditions_t () + | apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)); + repeat match goal with + | [ H : feBW_small |- _ ] => destruct H as [? _] + end ]. diff --git a/src/Specific/MontgomeryP256_128.v b/src/Specific/MontgomeryP256_128.v index 9c0336503..b3df2a409 100644 --- a/src/Specific/MontgomeryP256_128.v +++ b/src/Specific/MontgomeryP256_128.v @@ -201,15 +201,16 @@ Proof.*) Definition montgomery_to_F (v : Z) : F m := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F. -Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. +Definition mulmod_256_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. Proof. exists (proj1_sig mulmod_256''). abstract ( @@ -226,6 +227,26 @@ Proof. ). Defined. +Definition mulmod_256 + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. +Proof. + let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in + (exists v). + abstract apply (proj2_sig mulmod_256_ext). +Defined. + +Lemma mulmod_256_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z. +Proof. apply (proj2_sig mulmod_256_ext). Qed. + Local Ltac t_fin := [ > reflexivity | repeat match goal with @@ -241,19 +262,20 @@ Local Ltac t_fin := | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small end.. ]. -Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. +Definition add_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (f A B) < eval p256)))%Z }. Proof. exists (proj1_sig add'). abstract ( @@ -266,19 +288,20 @@ Proof. ). Defined. -Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. +Definition sub_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (f A B) < eval p256)))%Z }. Proof. exists (proj1_sig sub'). abstract ( @@ -291,15 +314,16 @@ Proof. ). Defined. -Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (f A) < eval p256)))%Z }. +Definition opp_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> 0 <= eval (f A) < eval p256)))%Z }. Proof. exists (proj1_sig opp'). abstract ( @@ -312,11 +336,12 @@ Proof. ). Defined. -Definition nonzero : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. +Definition nonzero_ext + : { f:Tuple.tuple Z sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. Proof. exists (proj1_sig nonzero'). abstract ( @@ -334,5 +359,86 @@ Proof. ). Defined. +Definition add + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in + (exists v). + abstract apply (proj2_sig add_ext). +Defined. + +Lemma add_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (proj1_sig add A B) < eval p256))%Z. +Proof. apply (proj2_sig add_ext). Qed. + +Definition sub + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in + (exists v). + abstract apply (proj2_sig sub_ext). +Defined. + +Lemma sub_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z. +Proof. apply (proj2_sig sub_ext). Qed. + +Definition opp + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in + (exists v). + abstract apply (proj2_sig opp_ext). +Defined. + +Lemma opp_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> 0 <= eval (proj1_sig opp A) < eval p256))%Z. +Proof. apply (proj2_sig opp_ext). Qed. + +Definition nonzero + : { f:Tuple.tuple Z sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. +Proof. + let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in + (exists v). + abstract apply (proj2_sig nonzero_ext). +Defined. + + Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero). Print Assumptions for_assumptions. diff --git a/src/Specific/NISTP256/AMD64/MontgomeryP256.v b/src/Specific/NISTP256/AMD64/MontgomeryP256.v index e709cc3ea..e8b25a781 100644 --- a/src/Specific/NISTP256/AMD64/MontgomeryP256.v +++ b/src/Specific/NISTP256/AMD64/MontgomeryP256.v @@ -195,15 +195,17 @@ Proof.*) Definition montgomery_to_F (v : Z) : F m := (F.of_Z m v * F.of_Z m (r'^Z.of_nat sz)%Z)%F. -Definition mulmod_256 : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. + +Definition mulmod_256_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval B < eval p256 -> 0 <= eval (f A B) < eval p256)%Z) }. Proof. exists (proj1_sig mulmod_256''). abstract ( @@ -220,6 +222,26 @@ Proof. ). Defined. +Definition mulmod_256 + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) * montgomery_to_F (eval B))%F }. +Proof. + let v := (eval cbv [proj1_sig mulmod_256_ext mulmod_256'' mulmod_256' lift2_sig] in (proj1_sig mulmod_256_ext)) in + (exists v). + abstract apply (proj2_sig mulmod_256_ext). +Defined. + +Lemma mulmod_256_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval B < eval p256 -> 0 <= eval (proj1_sig mulmod_256 A B) < eval p256)%Z. +Proof. apply (proj2_sig mulmod_256_ext). Qed. + Local Ltac t_fin := [ > reflexivity | repeat match goal with @@ -235,19 +257,20 @@ Local Ltac t_fin := | [ |- (0 <= MontgomeryAPI.eval (Z.pos r) _)%Z ] => apply MontgomeryAPI.eval_small end.. ]. -Definition add : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. +Definition add_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (f A B) < eval p256)))%Z }. Proof. exists (proj1_sig add'). abstract ( @@ -260,19 +283,20 @@ Proof. ). Defined. -Definition sub : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> montgomery_to_F (eval (f A B)) - = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) - (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), - (eval A < eval p256 - -> eval B < eval p256 - -> 0 <= eval (f A B) < eval p256)))%Z }. +Definition sub_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (f A B) < eval p256)))%Z }. Proof. exists (proj1_sig sub'). abstract ( @@ -285,15 +309,16 @@ Proof. ). Defined. -Definition opp : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz - | let eval := MontgomeryAPI.eval (Z.pos r) in - ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> montgomery_to_F (eval (f A)) - = (F.opp (montgomery_to_F (eval A)))%F)) - /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> 0 <= eval (f A) < eval p256)))%Z }. +Definition opp_ext + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + ((forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)) + /\ (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> 0 <= eval (f A) < eval p256)))%Z }. Proof. exists (proj1_sig opp'). abstract ( @@ -306,11 +331,12 @@ Proof. ). Defined. -Definition nonzero : { f:Tuple.tuple Z sz -> Z - | let eval := MontgomeryAPI.eval (Z.pos r) in - forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), - (eval A < eval p256 - -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. +Definition nonzero_ext + : { f:Tuple.tuple Z sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. Proof. exists (proj1_sig nonzero'). abstract ( @@ -328,5 +354,85 @@ Proof. ). Defined. +Definition add + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) + montgomery_to_F (eval B))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig add_ext add' lift2_sig] in (proj1_sig add_ext)) in + (exists v). + abstract apply (proj2_sig add_ext). +Defined. + +Lemma add_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (proj1_sig add A B) < eval p256))%Z. +Proof. apply (proj2_sig add_ext). Qed. + +Definition sub + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> montgomery_to_F (eval (f A B)) + = (montgomery_to_F (eval A) - montgomery_to_F (eval B))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig sub_ext sub' lift2_sig] in (proj1_sig sub_ext)) in + (exists v). + abstract apply (proj2_sig sub_ext). +Defined. + +Lemma sub_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A) + (B : Tuple.tuple Z sz) (_ : small (Z.pos r) B), + (eval A < eval p256 + -> eval B < eval p256 + -> 0 <= eval (proj1_sig sub A B) < eval p256))%Z. +Proof. apply (proj2_sig sub_ext). Qed. + +Definition opp + : { f:Tuple.tuple Z sz -> Tuple.tuple Z sz + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> montgomery_to_F (eval (f A)) + = (F.opp (montgomery_to_F (eval A)))%F)%Z }. +Proof. + let v := (eval cbv [proj1_sig opp_ext opp' lift1_sig] in (proj1_sig opp_ext)) in + (exists v). + abstract apply (proj2_sig opp_ext). +Defined. + +Lemma opp_bounded + : let eval := MontgomeryAPI.eval (Z.pos r) in + (forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> 0 <= eval (proj1_sig opp A) < eval p256))%Z. +Proof. apply (proj2_sig opp_ext). Qed. + +Definition nonzero + : { f:Tuple.tuple Z sz -> Z + | let eval := MontgomeryAPI.eval (Z.pos r) in + forall (A : Tuple.tuple Z sz) (_ : small (Z.pos r) A), + (eval A < eval p256 + -> f A = 0 <-> (montgomery_to_F (eval A) = F.of_Z m 0))%Z }. +Proof. + let v := (eval cbv [proj1_sig nonzero_ext nonzero' lift1_sig] in (proj1_sig nonzero_ext)) in + (exists v). + abstract apply (proj2_sig nonzero_ext). +Defined. + Local Definition for_assumptions := (mulmod_256, add, sub, opp, nonzero). Print Assumptions for_assumptions. diff --git a/src/Specific/NISTP256/AMD64/feadd.v b/src/Specific/NISTP256/AMD64/feadd.v index 1ea0fbc35..5de6fc03a 100644 --- a/src/Specific/NISTP256/AMD64/feadd.v +++ b/src/Specific/NISTP256/AMD64/feadd.v @@ -39,37 +39,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition add : { add : feBW_small -> feBW_small -> feBW_small | forall A B, phi (add A B) = F.add (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig add)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig add)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (addZ := proj1_sig add). - context_to_dlet_in_rhs addZ; cbv [addZ]. - cbv beta iota delta [add add' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by add op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval add_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/NISTP256/AMD64/femul.v b/src/Specific/NISTP256/AMD64/femul.v index d600869bd..f87e6d26b 100644 --- a/src/Specific/NISTP256/AMD64/femul.v +++ b/src/Specific/NISTP256/AMD64/femul.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition mul : { mul : feBW_small -> feBW_small -> feBW_small | forall A B, phi (mul A B) = F.mul (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig mulmod_256)) - by (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig mulmod_256)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (mulmodZ := proj1_sig mulmod_256). - context_to_dlet_in_rhs mulmodZ; cbv [mulmodZ]. - cbv beta iota delta [mulmod_256 mulmod_256'' mulmod_256' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by mulmod_256 op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval mulmod_256_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. Time refine_reflectively_with_uint8_with anf. (* Finished transaction in 212.693 secs (212.576u,0.184s) (successful) *) diff --git a/src/Specific/NISTP256/AMD64/fenz.v b/src/Specific/NISTP256/AMD64/fenz.v index cfea6e957..b46460550 100644 --- a/src/Specific/NISTP256/AMD64/fenz.v +++ b/src/Specific/NISTP256/AMD64/fenz.v @@ -44,18 +44,16 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition nonzero : { nonzero : feBW_small -> BoundedWord 1 bitwidth bound1 | forall A, (BoundedWordToZ _ _ _ (nonzero A) =? 0) = (if Decidable.dec (phi A = F.of_Z m 0) then true else false) }. Proof. - lazymatch goal with - | [ |- { f | forall a, (?R (?phi (f a)) ?v) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => R (phi f) v = rhs a) - end. - intros a. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. + apply_lift_sig; intros; eexists_sig_etransitivity. + all:cbv [feBW_of_feBW_small phi eval]. refine (_ : (if Decidable.dec (_ = 0) then true else false) = _). lazymatch goal with | [ |- (if Decidable.dec ?x then _ else _) = (if Decidable.dec ?y then _ else _) ] @@ -65,7 +63,7 @@ Section BoundedField25p5. | ] end. etransitivity; [ | eapply (proj2_sig nonzero) ]; - [ | solve [ try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption ].. ]. + [ | solve [ op_sig_side_conditions_t () ].. ]. reflexivity. let decP := lazymatch goal with |- { c | _ = if Decidable.dec (?decP = 0) then _ else _ } => decP end in apply (@proj2_sig_map _ (fun c => BoundedWordToZ 1 _ _ c = decP) _). @@ -78,9 +76,8 @@ Section BoundedField25p5. try reflexivity. Z.ltb_to_lt; congruence. } } eexists_sig_etransitivity. - set (nonzeroZ := proj1_sig nonzero). - context_to_dlet_in_rhs nonzeroZ; cbv [nonzeroZ]. - cbv beta iota delta [nonzero nonzero' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_lor runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. + do_set_sig nonzero. + cbv_runtime. reflexivity. sig_dlet_in_rhs_to_context. match goal with diff --git a/src/Specific/NISTP256/AMD64/feopp.v b/src/Specific/NISTP256/AMD64/feopp.v index ef4ea6aa6..14342c238 100644 --- a/src/Specific/NISTP256/AMD64/feopp.v +++ b/src/Specific/NISTP256/AMD64/feopp.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition opp : { opp : feBW_small -> feBW_small | forall A, phi (opp A) = F.opp (phi A) }. Proof. - lazymatch goal with - | [ |- { f | forall a, ?phi (?proj (f a)) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => phi (proj f) = rhs a) - end. - intros a. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig opp)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig opp)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (oppZ := proj1_sig opp). - context_to_dlet_in_rhs oppZ; cbv [oppZ]. - cbv beta iota delta [opp opp' proj1_sig MontgomeryAPI.T lift1_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by opp op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval opp_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/NISTP256/AMD64/fesub.v b/src/Specific/NISTP256/AMD64/fesub.v index d01471804..adf278faa 100644 --- a/src/Specific/NISTP256/AMD64/fesub.v +++ b/src/Specific/NISTP256/AMD64/fesub.v @@ -40,37 +40,20 @@ Section BoundedField25p5. Let phi : feBW -> F m := fun x => montgomery_to_F (eval x). + Local Ltac op_sig_side_conditions_t _ := + try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head_hnf' sig; try assumption. + (* TODO : change this to field once field isomorphism happens *) Definition sub : { sub : feBW_small -> feBW_small -> feBW_small | forall A B, phi (sub A B) = F.sub (phi A) (phi B) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (?proj (f a b)) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi (proj f) = rhs a b) - end. - intros a b. - cbv [feBW_of_feBW_small]. - eexists_sig_etransitivity. all:cbv [phi eval]. - rewrite <- (proj1 (proj2_sig sub)) - by (try (hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _)); destruct_head' feBW_small; destruct_head' feBW; try assumption). - reflexivity. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - Associativity.sig_sig_assoc. - apply sig_conj_by_impl2. - { intros ? H; cbv [eval]; rewrite H; clear H. - apply (proj2 (proj2_sig sub)); destruct_head' feBW_small; try assumption; - hnf; rewrite <- (is_bounded_by_None_repeat_In_iff_lt _ _ _); destruct_head' feBW; assumption. } - eexists_sig_etransitivity. - set (subZ := proj1_sig sub). - context_to_dlet_in_rhs subZ; cbv [subZ]. - cbv beta iota delta [sub sub' proj1_sig MontgomeryAPI.T lift2_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). - do 2 match goal with - | [ H : feBW_small |- _ ] => destruct H as [? _] - end. + start_preglue. + all:cbv [feBW_of_feBW_small eval]. + do_rewrite_with_sig_by sub op_sig_side_conditions_t. + cbv_runtime. + all:fin_preglue. + factor_out_bounds_and_strip_eval sub_bounded op_sig_side_conditions_t. (* jgross start here! *) Set Ltac Profiling. (* Set Ltac Profiling. diff --git a/src/Specific/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v index 01d629bfb..155bcf9e1 100644 --- a/src/Specific/X25519/C64/femul.v +++ b/src/Specific/X25519/C64/femul.v @@ -46,21 +46,9 @@ Section BoundedField25p5. { mul : feBW -> feBW -> feBW | forall a b, phi (mul a b) = F.mul (phi a) (phi b) }. Proof. - lazymatch goal with - | [ |- { f | forall a b, ?phi (f a b) = @?rhs a b } ] - => apply lift2_sig with (P:=fun a b f => phi f = rhs a b) - end. - intros a b. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig mul_sig). - symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_mulZ := fun a b => proj1_sig carry_sig (proj1_sig mul_sig a b)). - change (proj1_sig carry_sig (proj1_sig mul_sig ?a ?b)) with (carry_mulZ a b). - context_to_dlet_in_rhs carry_mulZ. - cbv beta iota delta [carry_mulZ proj1_sig mul_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). + start_preglue. + do_rewrite_with_2sig_add_carry mul_sig carry_sig; cbv_runtime. + all:fin_preglue. (* jgross start here! *) (*Set Ltac Profiling.*) Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v index d7d717c61..0bba90c68 100644 --- a/src/Specific/X25519/C64/fesquare.v +++ b/src/Specific/X25519/C64/fesquare.v @@ -46,21 +46,9 @@ Section BoundedField25p5. { square : feBW -> feBW | forall a, phi (square a) = F.mul (phi a) (phi a) }. Proof. - lazymatch goal with - | [ |- { f | forall a, ?phi (f a) = @?rhs a } ] - => apply lift1_sig with (P:=fun a f => phi f = rhs a) - end. - intros a. - eexists_sig_etransitivity. all:cbv [phi]. - rewrite <- (proj2_sig square_sig). - symmetry; rewrite <- (proj2_sig carry_sig); symmetry. - set (carry_squareZ := fun a => proj1_sig carry_sig (proj1_sig square_sig a)). - change (proj1_sig carry_sig (proj1_sig square_sig ?a)) with (carry_squareZ a). - context_to_dlet_in_rhs carry_squareZ. - cbv beta iota delta [carry_squareZ proj1_sig square_sig carry_sig fst snd runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]. - reflexivity. - sig_dlet_in_rhs_to_context. - apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). + start_preglue. + do_rewrite_with_1sig_add_carry square_sig carry_sig; cbv_runtime. + all:fin_preglue. (* jgross start here! *) (*Set Ltac Profiling.*) Time refine_reflectively. (* Finished transaction in 19.348 secs (19.284u,0.036s) (successful) *) diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v index b88370a48..ad0037245 100644 --- a/src/Specific/X25519/C64/ladderstep.v +++ b/src/Specific/X25519/C64/ladderstep.v @@ -112,12 +112,7 @@ Section BoundedField25p5. /\ (feW_bounded (fst (snd xz)) /\ feW_bounded (snd (snd xz)))) /\ Tuple.map (n:=2) (Tuple.map (n:=2) phi) xz = FMxzladderstep (eval (proj1_sig a24_sig)) (phi x1) (Tuple.map (n:=2) phi Q) (Tuple.map (n:=2) phi Q') }. Proof. - lazymatch goal with - | [ |- { op | forall (a:?A) (b:?B) (c:?C), - let v := op a b c in - @?P a b c v } ] - => refine (@lift3_sig A B C _ P _) - end. + apply_lift_sig. intros a b c; cbv beta iota zeta. lazymatch goal with | [ |- { e | ?A -> ?B -> ?C -> @?E e } ] @@ -137,11 +132,12 @@ Section BoundedField25p5. cbv [proj1_sig]; cbv [Mxzladderstep_sig]. context_to_dlet_in_rhs (@Mxzladderstep _). cbv [Mxzladderstep M.xzladderstep a24_sig]. - do 5 lazymatch goal with - | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] - => context_to_dlet_in_rhs (@proj1_sig a b f_sig) - end. - cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig runtime_add runtime_and runtime_mul runtime_opp runtime_shr sz]; cbn [fst snd]. + repeat lazymatch goal with + | [ |- context[@proj1_sig ?a ?b ?f_sig _] ] + => context_to_dlet_in_rhs (@proj1_sig a b f_sig) + end. + cbv beta iota delta [proj1_sig mul_sig add_sig sub_sig carry_sig square_sig]. + cbv_runtime. refine (proj2 FINAL). } subst feW feW_bounded; cbv beta. (* jgross start here! *) |