Add proofs for doubling shl,shr,shrd

After    | File Name                                                     | Before   || Change
------------------------------------------------------------------------------------------------
0m14.81s | Total                                                         | 0m00.00s || +0m14.81s
------------------------------------------------------------------------------------------------
0m08.87s | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate |   N/A    || +0m08.86s
0m02.82s | BoundedArithmetic/Double/Proofs/ShiftLeft                     |   N/A    || +0m02.81s
0m02.72s | BoundedArithmetic/Double/Proofs/ShiftRight                    |   N/A    || +0m02.72s
0m00.40s | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic          |   N/A    || +0m00.40s

4 files changed, 167 insertions, 0 deletions

diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
new file mode 100644
index 000000000..29d6ddde8
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Proofs/ShiftLeft.v
@@ -0,0 +1,43 @@
+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.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 shl.
+  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_left_immediate_double : is_shift_left_immediate (shl_double n).
+  Proof.
+    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 x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith.
+    unfold shl_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 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 shl.
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
new file mode 100644
index 000000000..81ac0e9f4
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic.v
@@ -0,0 +1,38 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
+
+Local Open Scope Z_scope.
+
+Local Arguments Z.pow !_ !_.
+Local Arguments Z.mul !_ !_.
+
+Ltac shift_left_right_t :=
+  repeat match goal with
+         | [ |- ?x = ?x ] => reflexivity
+         | [ |- Z.testbit ?x ?n = Z.testbit ?x ?n' ] => apply f_equal; try omega
+         | [ |- orb (Z.testbit ?x _) (Z.testbit ?y _) = orb (Z.testbit ?x _) (Z.testbit ?y _) ]
+           => apply f_equal2
+         | _ => progress Z.ltb_to_lt
+         | _ => progress subst
+         | _ => progress unfold AutoRewrite.rewrite_eq
+         | _ => progress intros
+         | _ => omega
+         | _ => solve [ trivial ]
+         | _ => progress break_match_step ltac:(fun _ => idtac)
+         | [ |- context[Z.lor (?x >> ?count) (Z.pow2_mod (?y << (?n - ?count)) ?n)] ]
+           => unique assert (0 <= Z.lor (x >> count) (Z.pow2_mod (y << (n - count)) n) < 2 ^ n) by (autorewrite with Zshift_to_pow; auto with zarith nia)
+         | _ => progress push_decode
+         | _ => progress Z.rewrite_mod_small
+         | _ => progress autorewrite with convert_to_Ztestbit
+         | _ => progress autorewrite with zsimplify_fast
+         | [ |- _ = _ :> Z ] => apply Z.bits_inj'; intros
+         | _ => progress autorewrite with Ztestbit_full
+         | _ => progress autorewrite with bool_congr
+         | [ |- Z.testbit _ (?x - ?y + (?y - ?z)) = false ]
+           => autorewrite with zsimplify
+         | [ H : 0 <= ?x < 2^?n |- Z.testbit ?x ?n' = false ]
+           => assert (n <= n') by auto with zarith; progress Ztestbit
+         | _ => progress Ztestbit_full
+         end.
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRight.v b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v
new file mode 100644
index 000000000..6a9fffbb1
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Proofs/ShiftRight.v
@@ -0,0 +1,44 @@
+Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
+Require Import Crypto.BoundedArithmetic.Interface.
+Require Import Crypto.BoundedArithmetic.Double.Core.
+Require Import Crypto.BoundedArithmetic.Double.Proofs.Decode.
+Require Import Crypto.BoundedArithmetic.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.
+    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 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.
diff --git a/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v
new file mode 100644
index 000000000..8e9506de8
--- /dev/null
+++ b/src/BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.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.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 shrd.
+  Context (n : Z) {W}
+          {ldi : load_immediate W}
+          {shrd : shift_right_doubleword_immediate W}
+          {decode : decoder n W}
+          {isdecode : is_decode decode}
+          {isldi : is_load_immediate ldi}
+          {isshrd : is_shift_right_doubleword_immediate shrd}.
+
+  Local Ltac zutil_arith ::= solve [ auto with nocore omega ].
+
+  Global Instance is_shift_right_doubleword_immediate_double : is_shift_right_doubleword_immediate (shrd_double n).
+  Proof.
+    intros high low count Hcount; hnf in Hcount.
+    unfold shrd_double, shift_right_doubleword_immediate_double; simpl.
+    generalize (decode_range low).
+    generalize (decode_range high).
+    generalize (decode_range (fst low)).
+    generalize (decode_range (snd low)).
+    generalize (decode_range (fst high)).
+    generalize (decode_range (snd high)).
+    assert (forall x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith.
+    assert (forall n' x, 2^n <= 2^n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith.
+    assert (forall n' x, n <= n' -> 0 <= x < 2^n -> 0 <= x < 2^n') by auto with zarith omega.
+    autorewrite with simpl_tuple_decoder; push_decode.
+    shift_left_right_t.
+  Qed.
+End shrd.