select_long

1 files changed, 38 insertions, 0 deletions

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index 0f29e837..5e6ebf02 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -38,3 +38,41 @@ Proof.
   rewrite Int.or_commut.
   apply Int.or_zero.
 Qed.
+
+Definition bitwise_select_long b vtrue vfalse :=
+  let b' := Val.longofint b in
+  Val.orl (Val.andl (Val.negl b') vtrue)
+          (Val.andl (Val.subl b' (Vlong Int64.one)) vfalse).
+
+Lemma bitwise_select_long_true :
+  forall vtrue vfalse,
+    bitwise_select_long (Val.of_optbool (Some true)) (Vlong vtrue) (Vlong vfalse)
+    = Vlong vtrue.
+Proof.
+  intros. cbn. f_equal.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.sub_idem.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  apply Int64.or_zero.
+Qed.
+
+Lemma bitwise_select_long_false :
+  forall vtrue vfalse,
+    bitwise_select_long (Val.of_optbool (Some false)) (Vlong vtrue) (Vlong vfalse)
+    = Vlong vfalse.
+Proof.
+  intros. cbn. f_equal.
+  change (Int64.repr (Int.signed Int.zero)) with Int64.zero.
+  rewrite Int64.neg_zero.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_zero.
+  rewrite Int64.sub_zero_r.
+  change (Int64.neg Int64.one) with Int64.mone.
+  rewrite Int64.and_commut.
+  rewrite Int64.and_mone.
+  rewrite Int64.or_commut.
+  apply Int64.or_zero.
+Qed.