Add fixed_size_op_to_word tactic

2 files changed, 50 insertions, 0 deletions

diff --git a/src/Util/FixedWordSizes.v b/src/Util/FixedWordSizes.v
index 8e2484ff6..2e0d6271b 100644
--- a/src/Util/FixedWordSizes.v
+++ b/src/Util/FixedWordSizes.v
@@ -96,3 +96,15 @@ Definition wland {logsz}
 Definition wlor {logsz}
   := word_case_dep (T:=fun _ word => word -> word -> word)
                    logsz wlor32 wlor64 wlor128 (fun _ => @wor _).
+
+Create HintDb fixed_size_constants discriminated.
+Hint Unfold word32 word64 word128
+     ZToWord ZToWord32 ZToWord64 ZToWord128
+     wordToZ word32ToZ word64ToZ word128ToZ
+     wadd wadd32 wadd64 wadd128
+     wsub wsub32 wsub64 wsub128
+     wmul wmul32 wmul64 wmul128
+     wshl wshl32 wshl64 wshl128
+     wshr wshr32 wshr64 wshr128
+     wland wland32 wland64 wland128
+     wlor wlor32 wlor64 wlor128 : fixed_size_constants.
diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v
index 09b15eb7c..7f8b7875a 100644
--- a/src/Util/FixedWordSizesEquality.v
+++ b/src/Util/FixedWordSizesEquality.v
@@ -176,3 +176,41 @@ Proof.
   intros sz1 sz2; break_match; intros; apply wordToZ_gen_ZToWord_gen_wordToZ_gen;
     handle_le.
 Qed.
+
+Local Ltac wordToZ_word_case_dep_t :=
+  let H := fresh in
+  intro H;
+  intros; unfold wordToZ, word_case_dep, wordT, word_case, word32, word64, word128, word32ToZ, word64ToZ, word128ToZ in *;
+  break_innermost_match;
+  change 128%nat with (2^7)%nat in *;
+  change 64%nat with (2^6)%nat in *;
+  change 32%nat with (2^5)%nat in *;
+  apply H.
+
+Lemma wordToZ_word_case_dep_binop' (wop : forall sz, word (2^sz) -> word (2^sz) -> word (2^sz))
+      (P : nat -> Z -> Z -> Z -> Type)
+  : (forall logsz (x y : word (2^logsz)), P logsz (wordToZ_gen x) (wordToZ_gen y) (wordToZ_gen (wop logsz x y)))
+    -> forall logsz (x y : wordT logsz), P logsz (wordToZ x) (wordToZ y) (wordToZ (word_case_dep (T:=fun _ W => W -> W -> W) logsz (wop 5) (wop 6) (wop 7) wop x y)).
+Proof. wordToZ_word_case_dep_t. Qed.
+Lemma wordToZ_word_case_dep_binop (wop : forall sz, word sz -> word sz -> word sz)
+      (P : nat -> Z -> Z -> Z -> Type)
+  : (forall logsz (x y : word (2^logsz)), P logsz (wordToZ_gen x) (wordToZ_gen y) (wordToZ_gen (wop (2^logsz) x y)))
+    -> forall logsz (x y : wordT logsz), P logsz (wordToZ x) (wordToZ y) (wordToZ (word_case_dep (T:=fun _ W => W -> W -> W) logsz (wop 32) (wop 64) (wop 128) (fun _ => wop _) x y)).
+Proof. apply wordToZ_word_case_dep_binop'. Qed.
+
+(** This converts goals involving (currently only binary) [wordT]
+    operations to the corresponding goals involving [word]
+    operations. *)
+Ltac fixed_size_op_to_word :=
+  repeat autounfold with fixed_size_constants in *;
+  lazymatch goal with
+  | [ |- context[wordToZ (word_case_dep (T:=?T) ?logsz (?wop 32) (?wop 64) (?wop 128) ?f ?x ?y)] ]
+    => move y at top; move x at top;
+       revert dependent logsz; intros logsz x y;
+       pattern (wordToZ x), (wordToZ y), (wordToZ (word_case_dep (T:=T) logsz (wop 32) (wop 64) (wop 128) f x y));
+       let P := lazymatch goal with |- ?P _ _ _ => P end in
+       let P := lazymatch (eval pattern logsz in P) with ?P _ => P end in
+       revert logsz x y;
+       refine (@wordToZ_word_case_dep_binop wop P _);
+       intros logsz x y; unfold wordToZ_gen; intros
+  end.