diff options
Diffstat (limited to 'src/SpecificGen')
-rw-r--r-- | src/SpecificGen/GF2213_32Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF2213_32BoundedCommon.v | 13 | ||||
-rw-r--r-- | src/SpecificGen/GF2519_32Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF2519_32BoundedCommon.v | 13 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_32Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_32BoundedCommon.v | 13 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_64Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF25519_64BoundedCommon.v | 13 | ||||
-rw-r--r-- | src/SpecificGen/GF41417_32Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF41417_32BoundedCommon.v | 13 | ||||
-rw-r--r-- | src/SpecificGen/GF5211_32Bounded.v | 8 | ||||
-rw-r--r-- | src/SpecificGen/GF5211_32BoundedCommon.v | 13 |
12 files changed, 84 insertions, 42 deletions
diff --git a/src/SpecificGen/GF2213_32Bounded.v b/src/SpecificGen/GF2213_32Bounded.v index 2947aacfc..e274923d6 100644 --- a/src/SpecificGen/GF2213_32Bounded.v +++ b/src/SpecificGen/GF2213_32Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v index 8caf225aa..df7031c2c 100644 --- a/src/SpecificGen/GF2213_32BoundedCommon.v +++ b/src/SpecificGen/GF2213_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2213_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2213_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2213_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split diff --git a/src/SpecificGen/GF2519_32Bounded.v b/src/SpecificGen/GF2519_32Bounded.v index ca448e458..facfc1a9f 100644 --- a/src/SpecificGen/GF2519_32Bounded.v +++ b/src/SpecificGen/GF2519_32Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v index 998dd899d..0830e8438 100644 --- a/src/SpecificGen/GF2519_32BoundedCommon.v +++ b/src/SpecificGen/GF2519_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2519_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe2519_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe2519_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split diff --git a/src/SpecificGen/GF25519_32Bounded.v b/src/SpecificGen/GF25519_32Bounded.v index 7dddfe2c5..748cf05eb 100644 --- a/src/SpecificGen/GF25519_32Bounded.v +++ b/src/SpecificGen/GF25519_32Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v index 4c186fd26..1695681c4 100644 --- a/src/SpecificGen/GF25519_32BoundedCommon.v +++ b/src/SpecificGen/GF25519_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split diff --git a/src/SpecificGen/GF25519_64Bounded.v b/src/SpecificGen/GF25519_64Bounded.v index 71b859d32..6dedca56b 100644 --- a/src/SpecificGen/GF25519_64Bounded.v +++ b/src/SpecificGen/GF25519_64Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word128ToZ (_ ^- (Interpretations128.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord128 with Interpretations128.WordW.ZToWordW in *. + change ZToWord128 with Interpretations128.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations128.WordW.wordWToZ_sub; rewrite !Interpretations128.WordW.wordWToZ_land; rewrite !Interpretations128.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord128 with Interpretations128.WordW.ZToWordW in *. + change ZToWord128 with Interpretations128.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations128.WordW.wordWToZ_sub; rewrite !Interpretations128.WordW.wordWToZ_land; rewrite !Interpretations128.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v index d1e3c6407..3d3a761af 100644 --- a/src/SpecificGen/GF25519_64BoundedCommon.v +++ b/src/SpecificGen/GF25519_64BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_64WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe25519_64WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe25519_64 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split diff --git a/src/SpecificGen/GF41417_32Bounded.v b/src/SpecificGen/GF41417_32Bounded.v index be7cf5714..fdcbe21ea 100644 --- a/src/SpecificGen/GF41417_32Bounded.v +++ b/src/SpecificGen/GF41417_32Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v index fec786e23..92a90bd16 100644 --- a/src/SpecificGen/GF41417_32BoundedCommon.v +++ b/src/SpecificGen/GF41417_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe41417_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe41417_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split diff --git a/src/SpecificGen/GF5211_32Bounded.v b/src/SpecificGen/GF5211_32Bounded.v index c879a3b19..ca0fdc26c 100644 --- a/src/SpecificGen/GF5211_32Bounded.v +++ b/src/SpecificGen/GF5211_32Bounded.v @@ -150,7 +150,8 @@ Proof. { match goal with |- (_,word64ToZ (_ ^- (Interpretations64.WordW.ZToWordW ?x) ^& _)) = (_,_ - (?y &' _)) => assert (x = y) as Hxy by reflexivity; repeat rewrite <-Hxy; clear Hxy end. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; @@ -169,12 +170,13 @@ Proof. end. } - unfold_is_bounded. - change ZToWord64 with Interpretations64.WordW.ZToWordW in *. + change ZToWord64 with Interpretations64.WordW.ZToWordW in *; + preunfold_is_bounded. rewrite !Interpretations64.WordW.wordWToZ_sub; rewrite !Interpretations64.WordW.wordWToZ_land; rewrite !Interpretations64.WordW.wordWToZ_ZToWordW; repeat match goal with |- _ /\ _ => split; Z.ltb_to_lt end; + Z.ltb_to_lt; unfold_is_bounded; Z.ltb_to_lt; try match goal with | |- 0 <= ModularBaseSystemListZOperations.neg _ _ < 2 ^ _ => apply ModularBaseSystemListZOperationsProofs.neg_range; omega | |- 0 <= _ < 2 ^ Z.of_nat _ => vm_compute; split; [refine (fun x => match x with eq_refl => I end) | reflexivity] diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v index 911fdb5ba..a12b1287c 100644 --- a/src/SpecificGen/GF5211_32BoundedCommon.v +++ b/src/SpecificGen/GF5211_32BoundedCommon.v @@ -300,14 +300,19 @@ Ltac unfold_is_bounded_in' H := unfold_is_bounded_in' H2 | _ => idtac end. -Ltac unfold_is_bounded_in H := +Ltac preunfold_is_bounded_in H := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ in H; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths] in H; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths] in H. +Ltac unfold_is_bounded_in H := + preunfold_is_bounded_in H; unfold_is_bounded_in' H. -Ltac unfold_is_bounded := +Ltac preunfold_is_bounded := unfold is_bounded, wire_digits_is_bounded, is_bounded_gen, fe5211_32WToZ, wire_digitsWToZ; - cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths]; + cbv [to_list length bounds wire_digit_bounds from_list from_list' map2 on_tuple2 to_list' ListUtil.map2 List.map fold_right List.rev List.app length_fe5211_32 List.length wire_widths]. + +Ltac unfold_is_bounded := + preunfold_is_bounded; repeat match goal with | [ |- andb _ _ = true ] => apply andb_true_intro | [ |- and _ _ ] => split |