1 files changed, 44 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v
new file mode 100644
index 000000000..16e7c5d6a
--- /dev/null
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v
@@ -0,0 +1,44 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.LegacyArithmetic.Double.Core.
+Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
+Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic.
+Require Import Crypto.Util.ZUtil.
+(*Require Import Crypto.Util.Tactics.*)
+
+Local Open Scope Z_scope.
+
+Local Opaque tuple_decoder.
+Local Arguments Z.pow !_ !_.
+Local Arguments Z.mul !_ !_.
+
+Section shr.
+  Context (n : Z) {W}
+          {ldi : load_immediate W}
+          {shl : shift_left_immediate W}
+          {shr : shift_right_immediate W}
+          {or : bitwise_or W}
+          {decode : decoder n W}
+          {isdecode : is_decode decode}
+          {isldi : is_load_immediate ldi}
+          {isshl : is_shift_left_immediate shl}
+          {isshr : is_shift_right_immediate shr}
+          {isor : is_bitwise_or or}.
+
+  Global Instance is_shift_right_immediate_double : is_shift_right_immediate (shr_double n).
+  Proof using Type*.
+    intros r count H; hnf in H.
+    assert (0 < 2^count) by auto with zarith.
+    assert (0 < 2^(n+count)) by auto with zarith.
+    assert (forall n', ~n' + count < n -> 2^n <= 2^(n'+count)) by auto with zarith omega.
+    assert (forall n', ~n' + count < n -> 2^n <= 2^(n'+count)) by auto with zarith omega.
+    unfold shr_double; simpl.
+    generalize (decode_range r).
+    pose proof (decode_range (fst r)).
+    pose proof (decode_range (snd r)).
+    assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith).
+    assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega.
+    autorewrite with simpl_tuple_decoder; push_decode.
+    shift_left_right_t.
+  Qed.
+End shr.