select through bitwise operations

1 files changed, 40 insertions, 0 deletions

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
new file mode 100644
index 00000000..0f29e837
--- /dev/null
+++ b/riscV/ExtValues.v
@@ -0,0 +1,40 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Values.
+Require Import Floats.
+
+Definition bitwise_select_int b vtrue vfalse :=
+  Val.or (Val.and (Val.neg b) vtrue)
+         (Val.and (Val.sub b Vone) vfalse).
+
+Lemma bitwise_select_int_true :
+  forall vtrue vfalse,
+    bitwise_select_int (Val.of_optbool (Some true)) (Vint vtrue) (Vint vfalse)
+    = Vint vtrue.
+Proof.
+  intros. cbn. f_equal.
+  change (Int.neg Int.one) with Int.mone.
+  rewrite Int.and_commut.
+  rewrite Int.and_mone.
+  rewrite Int.sub_idem.
+  rewrite Int.and_commut.
+  rewrite Int.and_zero.
+  apply Int.or_zero.
+Qed.
+
+Lemma bitwise_select_int_false :
+  forall vtrue vfalse,
+    bitwise_select_int (Val.of_optbool (Some false)) (Vint vtrue) (Vint vfalse)
+    = Vint vfalse.
+Proof.
+  intros. cbn. f_equal.
+  rewrite Int.neg_zero.
+  rewrite Int.and_commut.
+  rewrite Int.and_zero.
+  rewrite Int.sub_zero_r.
+  change (Int.neg Int.one) with Int.mone.
+  rewrite Int.and_commut.
+  rewrite Int.and_mone.
+  rewrite Int.or_commut.
+  apply Int.or_zero.
+Qed.