Add shl,shr,shrd to repeated doubling

After    | File Name                                                              | Before   || Change
---------------------------------------------------------------------------------------------------------
0m03.99s | Total                                                                  | 0m03.08s || +0m00.90s
---------------------------------------------------------------------------------------------------------
0m01.14s | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.02s || +0m00.11s
0m00.52s | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.53s || -0m00.01s
0m00.51s | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.51s || +0m00.00s
0m00.47s | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate |   N/A    || +0m00.47s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.54s || -0m00.08s
0m00.46s | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                |   N/A    || +0m00.46s
0m00.44s | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.49s || -0m00.04s

3 files changed, 91 insertions, 4 deletions

diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v b/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
index 666d4593b..873985fa3 100644
--- a/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/Decode.v
@@ -76,18 +76,33 @@ Section decode.
   Global Existing Instance is_repeated_tuple_decode.
 End decode.
 
-Ltac is_cls_fixpoint_t decode n exp is_clsv IH :=
+Ltac is_cls_fixpoint_t_gen decode n exp generalize_is_clsv IH :=
   let exp' := fresh exp in
   destruct exp as [|exp'];
   [ clear IH;
-    destruct decode; generalize is_clsv;
+    destruct decode; generalize_is_clsv ();
     simpl;
     change (Z.of_nat 2 ^ Z.of_nat 0) with 1;
     generalize (Z.mul_1_l n); generalize (1 * n);
     intro; clear; induction 1;
-    exact (fun x => x)
-  | specialize (IH exp');
+    intros; repeat apply pair; assumption
+  | specialize (IH exp'); revert IH;
+    repeat match goal with
+           | [ |- (_ * _)%type -> _ ]
+             => let x := fresh in
+                let y := fresh in
+                intros [x y]; revert x y
+           | [ |- _ -> _ ]
+             => intro
+           end;
     simpl @repeated_tuple_decoder; simpl;
     change (Z.of_nat (S exp')) with (Z.of_nat (1 + exp'));
     rewrite (Nat2Z.inj_add 1 exp'), Z.pow_add_r, Z.pow_1_r, <- !Z.mul_assoc, <- decoder_eta by omega;
+    repeat apply pair;
     try exact _ ].
+
+Ltac is_cls_fixpoint_t decode n exp is_clsv IH :=
+  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv) IH.
+
+Ltac is_cls_fixpoint_t2 decode n exp is_clsv1 is_clsv2 IH :=
+  is_cls_fixpoint_t_gen decode n exp ltac:(fun _ => generalize is_clsv1, is_clsv2) IH.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
new file mode 100644
index 000000000..401e3a015
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight.v
@@ -0,0 +1,42 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftLeft.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftRight.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.LoadImmediate.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.BitwiseOr.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section shift_left_right.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {ldi : load_immediate W}
+          {is_ldi : is_load_immediate ldi}
+          {shl : shift_left_immediate W}
+          {is_shl : is_shift_left_immediate shl}
+          {shr : shift_right_immediate W}
+          {is_shr : is_shift_right_immediate shr}
+          {or : bitwise_or W}
+          {is_or : is_bitwise_or or}.
+
+  Fixpoint is_shift_left_right_immediate_repeated_double {exp : nat}
+    : (is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp))
+       * is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp)))%type.
+  Proof. is_cls_fixpoint_t2 decode n exp is_shl is_shr (@is_shift_left_right_immediate_repeated_double). Qed.
+  Global Instance is_shift_left_immediate_repeated_double {exp : nat}
+    : is_shift_left_immediate (shift_left_immediate_repeated_double (exp:=exp))
+    := fst (@is_shift_left_right_immediate_repeated_double exp).
+  Global Instance is_shift_right_immediate_repeated_double {exp : nat}
+    : is_shift_right_immediate (shift_right_immediate_repeated_double (exp:=exp))
+    := snd (@is_shift_left_right_immediate_repeated_double exp).
+End shift_left_right.
diff --git a/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
new file mode 100644
index 000000000..00d41c57f
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate.v
@@ -0,0 +1,30 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.ShiftRightDoubleWordImmediate.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Core.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.Double.Repeated.Proofs.LoadImmediate.
+Require Import Crypto.Util.ZUtil.
+
+Local Open Scope Z_scope.
+Local Arguments Z.mul !_ !_.
+Local Arguments Z.pow : simpl never.
+Local Arguments Z.of_nat : simpl never.
+Local Opaque tuple_decoder.
+
+Section shift_right_doubleword_immediate.
+  Context {n W}
+          {decode : decoder n W}
+          {is_decode : is_decode decode}
+          {ldi : load_immediate W}
+          {is_ldi : is_load_immediate ldi}
+          {shrd : shift_right_doubleword_immediate W}
+          {is_shrd : is_shift_right_doubleword_immediate shrd}.
+
+  Fixpoint is_shift_right_doubleword_immediate_repeated_double {exp : nat}
+    : is_shift_right_doubleword_immediate (shift_right_doubleword_immediate_repeated_double (exp:=exp)).
+  Proof. is_cls_fixpoint_t decode n exp is_shrd (@is_shift_right_doubleword_immediate_repeated_double). Qed.
+  Global Existing Instance is_shift_right_doubleword_immediate_repeated_double.
+End shift_right_doubleword_immediate.