diff options
| -rw-r--r-- | src/Specific/GF25519Bounded.v | 80 | ||||
| -rw-r--r-- | src/Specific/GF25519BoundedCommon.v | 18 | ||||
| -rw-r--r-- | src/Specific/GF25519Reflective/Common.v | 9 | ||||
| -rw-r--r-- | src/Util/HList.v | 9 | ||||
| -rw-r--r-- | src/Util/Tuple.v | 28 |
5 files changed, 85 insertions, 59 deletions
diff --git a/src/Specific/GF25519Bounded.v b/src/Specific/GF25519Bounded.v index 81de77008..b8f1ef25b 100644 --- a/src/Specific/GF25519Bounded.v +++ b/src/Specific/GF25519Bounded.v @@ -24,8 +24,16 @@ Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. Local Open Scope Z. +Local Ltac simpl_tuple_map1 := + repeat match goal with + | [ |- context[@Tuple.map 1 ?A ?B ?f] ] + => replace (@Tuple.map 1 A B f) with f by (clear; abstract reflexivity) + | [ H : context[@Tuple.map 1 ?A ?B ?f] |- _ ] + => replace (@Tuple.map 1 A B f) with f in H by (clear; abstract reflexivity) + end. Local Ltac cbv_tuple_map := + simpl_tuple_map1; cbv [Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list' HList.hlistP HList.hlistP']. Local Ltac post_bounded_t := @@ -150,10 +158,11 @@ Proof. change word64ToZ with Interpretations64.WordW.wordWToZ in *. rewrite Hgm. - cbv [modulusW Tuple.map]. + cbv [modulusW Tuple.map Tuple.map']. cbv [on_tuple List.map to_list to_list' from_list from_list' HList.hlistP HList.hlistP' - Tuple.map2 on_tuple2 ListUtil.map2 fe25519WToZ length_fe25519]. + Tuple.map2 on_tuple2 ListUtil.map2 fe25519WToZ length_fe25519 Tuple.map Tuple.map']. + simpl @fst in *; simpl @snd in *. cbv [postfreeze GF25519.postfreeze]. cbv [Let_In]. @@ -225,7 +234,8 @@ Proof. { reflexivity. } { reflexivity. } { intros; pose proof (fun k0 k1 X Y => proj1 (mulW_correct_and_bounded (k0, k1) (conj X Y))) as H'. - cbv [Curry.curry2 Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list'] in H'. + cbv [Curry.curry2 Tuple.map Tuple.map' Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list'] in H'. + simpl @fst in *; simpl @snd in *. rewrite <- H' by assumption. apply mulW_correct_and_bounded; split; assumption. } { intros; rewrite (fun X Y => proj1 (mulW_correct_and_bounded (_, _) (conj X Y))) by assumption; reflexivity. } @@ -344,32 +354,44 @@ Proof. end; change sqrt_m1 with (fe25519WToZ sqrt_m1W); pose proof (fun X Y => proj1 (mulW_correct_and_bounded (sqrt_m1W, a) (conj X Y))) as correctness; - let cbv_in_all _ := (cbv [fe25519WToZ Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list' fe25519WToZ Curry.curry2 HList.hlistP HList.hlistP'] in *; idtac) in - cbv_in_all (); - let solver _ := (repeat match goal with - | _ => progress subst - | _ => progress unfold fst, snd - | _ => progress cbv_in_all () - | [ |- ?x /\ ?x ] => cut x; [ intro; split; assumption | ] - | [ |- is_bounded ?op = true ] - => let H := fresh in - lazymatch op with - | context[mulW (_, _)] => pose proof mulW_correct_and_bounded as H - | context[mulW_noinline (_, _)] => pose proof mulW_correct_and_bounded as H - | context[powW _ _] => pose proof powW_correct_and_bounded as H - | context[sqrt_m1W] => vm_compute; reflexivity - | _ => assumption - end; - cbv_in_all (); - apply H - end) in - rewrite <- correctness by solver (); clear correctness; - let lem := fresh in - pose proof eqbW_correct as lem; cbv_in_all (); rewrite <- lem by solver (); clear lem; - pose proof (pull_bool_if fe25519WToZ) as lem; cbv_in_all (); rewrite lem by solver (); clear lem; - subst_evars; reflexivity + let cbv_in_all _ := (cbv [fe25519WToZ Tuple.map Tuple.map' Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list' fe25519WToZ Curry.curry2 HList.hlistP HList.hlistP' fst snd] in *; idtac) in + let solver _ := (repeat match goal with H := ?e |- _ => is_evar e; clearbody H end; + abstract + (repeat match goal with + | _ => progress subst + | _ => progress unfold fst, snd + | _ => progress cbv_in_all () + | [ |- ?x /\ ?x ] => cut x; [ intro; split; assumption | ] + | [ |- is_bounded ?op = true ] + => let H := fresh in + lazymatch op with + | context[mulW (_, _)] => pose proof mulW_correct_and_bounded as H + | context[mulW_noinline (_, _)] => pose proof mulW_correct_and_bounded as H + | context[powW _ _] => pose proof powW_correct_and_bounded as H + | context[sqrt_m1W] => vm_compute; reflexivity + | _ => assumption + end; + cbv_in_all (); + apply H + end)) in + specialize_by solver (); + (* munging for fast [Defined] >.< *) + let T := type of correctness in + let T' := (eval unfold Tuple.map at 2 in T) in + let T' := (eval cbv [Curry.curry2 Tuple.map' fst snd] in T') in + let correctness' := fresh "correctness'" in + assert (correctness' : T') by (clear -correctness; abstract (rewrite correctness; reflexivity)); + rewrite <- correctness' by fail; + clear correctness'; + cbv [Tuple.map Tuple.map']; + let lem := fresh in + pose proof eqbW_correct as lem; + rewrite <- lem by solver (); clear lem; + pose proof (pull_bool_if fe25519WToZ) as lem; rewrite lem by solver (); clear lem; + subst_evars; reflexivity end. } Unfocus. + assert (Hfold : forall x, fe25519WToZ x = fe25519WToZ x) by reflexivity. unfold fe25519WToZ at 2 in Hfold. etransitivity. @@ -395,8 +417,8 @@ Proof. => apply powW_correct_and_bounded; assumption | [ |- is_bounded (snd (?WToZ (_, powW _ _))) = true ] => generalize powW_correct_and_bounded; - cbv [snd Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list' HList.hlistP HList.hlistP']; - let H := fresh in intro H; apply H; assumption + simpl_tuple_map1; + abstract (let H := fresh in intro H; apply H; assumption) | [ |- is_bounded (?WToZ (mulW (_, _))) = true ] => apply mulW_correct_and_bounded; split; [ vm_compute; reflexivity | ] end. diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v index e9abe2f74..a3914951e 100644 --- a/src/Specific/GF25519BoundedCommon.v +++ b/src/Specific/GF25519BoundedCommon.v @@ -288,7 +288,7 @@ Definition word31_to_unbounded_word (x : word 31) : unbounded_word 31. Proof. apply (word_to_unbounded_word x); reflexivity. Defined. Local Opaque word64. -Declare Reduction app_tuple_map := cbv [app_wire_digitsW app_fe25519W app_fe25519 HList.mapt HList.mapt' Tuple.map on_tuple List.map List.app length_fe25519 List.length wire_widths Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' fst snd]. +Declare Reduction app_tuple_map := cbv [app_wire_digitsW app_fe25519W app_fe25519 HList.mapt HList.mapt' Tuple.map Tuple.map' fst snd on_tuple List.map List.app length_fe25519 List.length wire_widths Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' fst snd]. Definition fe25519WToZ (x : fe25519W) : Specific.GF25519.fe25519 := Eval app_tuple_map in app_fe25519W x (Tuple.map (fun v : word64 => v : Z)). @@ -322,14 +322,14 @@ Ltac unfold_is_bounded_in' H := end. Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map List.map fold_right List.rev List.app length_fe25519 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple] in H. + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map Tuple.map' List.map fold_right List.rev List.app length_fe25519 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple] in H. Ltac unfold_is_bounded_in H := preunfold_is_bounded_in H; unfold_is_bounded_in' H. Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map List.map fold_right List.rev List.app length_fe25519 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple]. + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 Tuple.map Tuple.map' List.map fold_right List.rev List.app length_fe25519 List.length wire_widths HList.hlistP HList.hlistP' Tuple.on_tuple]. Ltac unfold_is_bounded := preunfold_is_bounded; @@ -349,7 +349,7 @@ Local Ltac prove_lt_bit_width := Lemma fe25519ZToW_WToZ (x : fe25519W) : fe25519ZToW (fe25519WToZ x) = x. Proof. hnf in x; destruct_head' prod; cbv [fe25519WToZ fe25519ZToW]. - rewrite !ZToWord64_word64ToZ; reflexivity. + simpl; rewrite !ZToWord64_word64ToZ; reflexivity. Qed. Lemma fe25519WToZ_ZToW x : is_bounded x = true -> fe25519WToZ (fe25519ZToW x) = x. @@ -358,7 +358,7 @@ Proof. intro H. unfold_is_bounded_in H; destruct_head' and. Z.ltb_to_lt. - rewrite !word64ToZ_ZToWord64 by prove_lt_bit_width. + simpl; rewrite !word64ToZ_ZToWord64 by prove_lt_bit_width. reflexivity. Qed. @@ -366,13 +366,13 @@ Lemma fe25519W_word64ize_id x : fe25519W_word64ize x = x. Proof. hnf in x; destruct_head' prod. cbv [fe25519W_word64ize]; - repeat apply f_equal2; apply word64ize_id. + simpl; repeat apply f_equal2; apply word64ize_id. Qed. Lemma wire_digitsW_word64ize_id x : wire_digitsW_word64ize x = x. Proof. hnf in x; destruct_head' prod. cbv [wire_digitsW_word64ize]; - repeat apply f_equal2; apply word64ize_id. + simpl; repeat apply f_equal2; apply word64ize_id. Qed. Definition uncurry_unop_fe25519W {T} (op : fe25519W -> T) @@ -511,6 +511,7 @@ Lemma proj1_fe25519_exist_fe25519 x pf : proj1_fe25519 (exist_fe25519 x pf) = x. Proof. hnf in x; destruct_head' prod. cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W fe25519WToZ proj_word Build_bounded_word Build_bounded_word']. + simpl. unfold_is_bounded_in pf. destruct_head' and. Z.ltb_to_lt. @@ -543,6 +544,7 @@ Lemma proj1_wire_digits_exist_wire_digits x pf : proj1_wire_digits (exist_wire_d Proof. hnf in x; destruct_head' prod. cbv [proj1_wire_digits exist_wire_digits proj1_wire_digitsW wire_digitsWToZ proj_word Build_bounded_word Build_bounded_word' app_wire_digits HList.mapt HList.mapt' length wire_widths fst snd]. + simpl. unfold_is_bounded_in pf. destruct_head' and. Z.ltb_to_lt. @@ -694,6 +696,7 @@ Proof. generalize (encode_bounded x); generalize (ModularBaseSystem.encode x). intros y pf; intros; hnf in y; destruct_head_hnf' prod. cbv [proj1_fe25519 exist_fe25519 proj1_fe25519W Build_bounded_word Build_bounded_word' fe25519WToZ proj_word]. + simpl. unfold_is_bounded_in pf. destruct_head' and. Z.ltb_to_lt. @@ -706,6 +709,7 @@ Lemma decode_exist_fe25519 x pf Proof. hnf in x; destruct_head' prod. cbv [decode proj1_fe25519 exist_fe25519 proj1_fe25519W Build_bounded_word Build_bounded_word' fe25519WToZ proj_word]. + simpl. unfold_is_bounded_in pf. destruct_head' and. Z.ltb_to_lt. diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v index 3e39809f5..f702216e5 100644 --- a/src/Specific/GF25519Reflective/Common.v +++ b/src/Specific/GF25519Reflective/Common.v @@ -371,7 +371,7 @@ Section gen. | progress rewrite ?Tuple.map_S, ?Tuple.map2_S, ?Tuple.strip_eta_tuple'_dep | progress break_match_hyps | rewrite Bool.andb_true_iff; apply conj - | unfold Tuple.map, Tuple.map2; simpl; rewrite Bool.andb_true_iff; apply conj ] + | unfold Tuple.map, Tuple.map', Tuple.map2; simpl; rewrite Bool.andb_true_iff; apply conj ] ). } Defined. @@ -561,8 +561,9 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := repeat match goal with x := _ |- _ => subst x end; cbv [id binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded - Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list + Tuple.map Tuple.map' Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list Relations.proj_eq_rel SmartVarfMap interp_flat_type smart_interp_flat_map domain fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower codomain WordW.to_Z nm_op_args_to_bounded nm_op_args_to_bounded' n_op_args_to_bounded n_op_args_to_bounded' unop_args_to_bounded' Relations.interp_flat_type_rel_pointwise Relations.interp_flat_type_rel_pointwise_gen_Prop] in Hbounds_left, Hbounds_right; + simpl @fst in Hbounds_left, Hbounds_right; simpl @snd in Hbounds_left, Hbounds_right; simpl @interp_flat_type in *; (let v := (eval unfold WordW.interp_base_type in (WordW.interp_base_type TZ)) in change (WordW.interp_base_type TZ) with v in *); @@ -585,7 +586,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := (split; [ exact Hbounds_left | ]); cbv [interp_flat_type] in *; cbv [fst snd - Tuple.map Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list Tuple.from_list' + Tuple.map Tuple.map' Tuple.on_tuple Tuple.to_list Tuple.to_list' List.map Tuple.from_list Tuple.from_list Tuple.from_list' make_bound Datatypes.length wire_widths wire_digit_bounds PseudoMersenneBaseParams.limb_widths bounds binop_bounds_good unop_bounds_good unopFEToWire_bounds_good unopWireToFE_bounds_good unopFEToZ_bounds_good op9_4_bounds_good @@ -596,7 +597,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args := destruct_head' and; Z.ltb_to_lt; change WordW.wordWToZ with word64ToZ in *; - cbv [Tuple.map HList.hlist Tuple.on_tuple Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' List.map HList.hlist' fst snd fe25519WToZ HList.hlistP HList.hlistP']; + cbv [Tuple.map Tuple.map' HList.hlist Tuple.on_tuple Tuple.from_list Tuple.from_list' Tuple.to_list Tuple.to_list' List.map HList.hlist' fst snd fe25519WToZ HList.hlistP HList.hlistP']; cbv [WordW.bit_width BitSize64.bit_width Z.of_nat Pos.of_succ_nat Pos.succ] in *; repeat split; unfold_is_bounded; Z.ltb_to_lt; diff --git a/src/Util/HList.v b/src/Util/HList.v index 1a724f84b..2a135c75c 100644 --- a/src/Util/HList.v +++ b/src/Util/HList.v @@ -91,11 +91,10 @@ Qed. Lemma map_is_mapt {n A F B} (f : A -> B) {ts : tuple A n} (ls : hlist F ts) : Tuple.map f ts = mapt (fun x _ => f x) ls. Proof. - destruct n as [|n]; [ reflexivity | ]. + destruct n as [|n]; simpl; [ destruct ts; reflexivity | ]. induction n as [|n IHn]; [ reflexivity | ]. - { unfold mapt in *; simpl @mapt' in *. - rewrite <- IHn; clear IHn. - rewrite <- (@Tuple.map_S n _ _ f); destruct ts; reflexivity. } + { simpl in *; rewrite <- IHn; clear IHn. + reflexivity. } Qed. Lemma map_is_mapt' {n A F B} (f : A -> B) {ts : tuple A (S n)} (ls : hlist' F ts) @@ -147,7 +146,7 @@ Global Instance mapt_Proper {n A F B} : Proper ((forall_relation (fun x => pointwise_relation _ Logic.eq)) ==> forall_relation (fun ts => Logic.eq ==> Logic.eq)) - (@HList.mapt n A F B). + (@mapt n A F B). Proof. unfold forall_relation, pointwise_relation, respectful. repeat intro; subst; destruct n as [|n]; [ reflexivity | ]. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index c23e10c2c..d175954d2 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -214,15 +214,18 @@ Definition on_tuple {A B} (f:list A -> list B) from_list m (f (to_list n xs)) (H (to_list n xs) (length_to_list xs)). -Definition map {n A B} (f:A -> B) (xs:tuple A n) : tuple B n - := on_tuple (List.map f) (fun _ => eq_trans (map_length _ _)) xs. +Section map. + (* Put the types and function in the context, so that the fixpoint doesn't depend on them *) + Context {A B} (f:A -> B). + + Fixpoint map' {n} : tuple' A n -> tuple' B n + := match n with + | 0 => f + | S n' => fun x : tuple' _ _ * _ => (@map' n' (fst x), f (snd x)) + end. +End map. -Fixpoint map' {n A B} (f:A -> B) : tuple' A n -> tuple' B n - := match n with - | 0 => f - | S n' => fun x : tuple' _ _ * _ => (@map' n' A B f (fst x), f (snd x)) - end. -Definition map_fix {n A B} (f:A -> B) : tuple A n -> tuple B n +Definition map {n A B} (f:A -> B) : tuple A n -> tuple B n := match n with | 0 => fun x => x | S n' => map' f @@ -287,9 +290,9 @@ Ltac tuples_from_lists := Lemma map_to_list {A B n ts} (f : A -> B) : List.map f (@to_list A n ts) = @to_list B n (map f ts). Proof. - tuples_from_lists; unfold map, on_tuple. - repeat (rewrite to_list_from_list || rewrite from_list_to_list). - reflexivity. + destruct n; simpl; [ reflexivity | ]. + induction n; simpl in *; [ reflexivity | ]. + destruct ts; simpl; congruence. Qed. Lemma to_list_map2 {A B C n xs ys} (f : A -> B -> C) @@ -767,9 +770,6 @@ Qed. Lemma map_append' {A B n} (f:A->B) : forall (x:tuple' A n) (a:A), map f (append (n:=S n) a x) = append (f a) (map (n:=S n) f x). Proof. - cbv [map append on_tuple]; intros. - simpl to_list. simpl List.map. rewrite from_list_cons. - cbv [append]; f_equal. rewrite <-!from_list_default_eq with (d:=f a). reflexivity. Qed. |