bitwise_select_value_correct

1 files changed, 12 insertions, 0 deletions

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index f9996a97..591507ed 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -183,3 +183,15 @@ Definition bitwise_select_value vt m b vtrue vfalse :=
                                         (int64_of_value m vtrue)
                                         (int64_of_value m vfalse)).
 
+Theorem bitwise_select_value_correct :
+  forall m (b : bool) vtrue vfalse,
+    bitwise_select_value (vtype_of (if b then vtrue else vfalse))
+                         m (if b then Int64.one else Int64.zero) vtrue vfalse =
+    if b then vtrue else vfalse.
+Proof.
+  intros. unfold bitwise_select_value. destruct b.
+  - rewrite bitwise_select_long_true.
+    apply int64_of_value_correct.
+  - rewrite bitwise_select_long_false.
+    apply int64_of_value_correct.
+Qed.