diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-02-02 10:21:17 +0100 |
| commit | d2159e300b2d5e017a3144c747d34949b2ff2769 (patch) | |
| tree | 2186636bc3f2e85b5effd19f9e7c23f4183545aa /riscV/ExtValues.v | |
| parent | e0f1a90c2dcf7c43137064470ce4b12368b8435d (diff) | |
| download | compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.tar.gz compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.zip | |
begin implementing select
Diffstat (limited to 'riscV/ExtValues.v')
| -rw-r--r-- | riscV/ExtValues.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v index e0557de4..81688ca6 100644 --- a/riscV/ExtValues.v +++ b/riscV/ExtValues.v @@ -73,3 +73,13 @@ Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val := else Vundef | _ => Vundef end. + +Lemma normalize_select01: + forall x y z, Val.normalize (select01_long x y z) AST.Tlong = select01_long x (Val.normalize y AST.Tlong) (Val.normalize z AST.Tlong). +Proof. + unfold select01_long. + intros. + destruct x; cbn; trivial. + destruct (Int.eq i Int.one); trivial. + destruct (Int.eq i Int.zero); trivial. +Qed. |