diff options
Diffstat (limited to 'common/Values.v')
| -rw-r--r-- | common/Values.v | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index d086c69f..802d827b 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1259,6 +1259,16 @@ Proof. rewrite H. decEq. apply Int.shl_rolm. exact H. Qed. +Theorem shll_rolml: + forall x n, + Int.ltu n Int64.iwordsize' = true -> + shll x (Vint n) = rolml x n (Int64.shl Int64.mone (Int64.repr (Int.unsigned n))). +Proof. + intros. destruct x; auto. simpl. rewrite H. rewrite <- Int64.shl_rolm. unfold Int64.shl. + rewrite Int64.int_unsigned_repr. constructor. unfold Int64.ltu. rewrite Int64.int_unsigned_repr. + apply H. +Qed. + Theorem shru_rolm: forall x n, Int.ltu n Int.iwordsize = true -> @@ -1268,6 +1278,17 @@ Proof. rewrite H. decEq. apply Int.shru_rolm. exact H. Qed. +Theorem shrlu_rolml: + forall x n, + Int.ltu n Int64.iwordsize' = true -> + shrlu x (Vint n) = rolml x (Int.sub Int64.iwordsize' n) (Int64.shru Int64.mone (Int64.repr (Int.unsigned n))). +Proof. + intros. destruct x; auto. simpl. rewrite H. + rewrite Int64.int_sub_ltu by apply H. rewrite Int64.repr_unsigned. rewrite <- Int64.shru_rolm. unfold Int64.shru'. unfold Int64.shru. + rewrite Int64.unsigned_repr. reflexivity. apply Int64.int_unsigned_range. + unfold Int64.ltu. rewrite Int64.int_unsigned_repr. auto. +Qed. + Theorem shrx_carry: forall x y z, shrx x y = Some z -> |