2 files changed, 13 insertions, 0 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index b5e3ed7e..0a4b3ef6 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -234,6 +234,9 @@ Nondetfunction mul (e1: expr) (e2: expr) :=
   | _, _ => Eop Omul (e1:::e2:::Enil)
   end.
 
+Definition mulhs (e1: expr) (e2: expr) := Eop Omulhs (e1 ::: e2 ::: Enil).
+Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil).
+
 (** ** Bitwise and, or, xor *)
 
 Nondetfunction andimm (n1: int) (e2: expr) := 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 548fbce2..7f3da409 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -367,6 +367,16 @@ Proof.
   TrivialExists.
 Qed.
 
+Theorem eval_mulhs: binary_constructor_sound mulhs Val.mulhs.
+Proof.
+  unfold mulhs; red; intros; TrivialExists.
+Qed.
+  
+Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu.
+Proof.
+  unfold mulhu; red; intros; TrivialExists.
+Qed.
+  
 Theorem eval_andimm:
   forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)).
 Proof.