diff options
| -rw-r--r-- | riscV/ExtValues.v | 12 |
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. |