diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 21:02:18 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-01 21:02:18 +0100 |
commit | 325b9f028f91b65e191d48dc8482da8d1ccb5d2b (patch) | |
tree | eb794b34806cce0280f6565cfbeedd76a5a3816d | |
parent | 485952d5513a9de25f7e3ee3ca7a35442f154d04 (diff) | |
download | compcert-kvx-325b9f028f91b65e191d48dc8482da8d1ccb5d2b.tar.gz compcert-kvx-325b9f028f91b65e191d48dc8482da8d1ccb5d2b.zip |
bitwise_select_value_correct
-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. |