diff options
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v')
-rw-r--r-- | src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v new file mode 100644 index 000000000..00a6d03cd --- /dev/null +++ b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v @@ -0,0 +1,42 @@ +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 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 using isdecode isshrd. + 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. |