diff options
Diffstat (limited to 'riscV/ExtValues.v')
-rw-r--r-- | riscV/ExtValues.v | 123 |
1 files changed, 123 insertions, 0 deletions
diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v new file mode 100644 index 00000000..edf359ef --- /dev/null +++ b/riscV/ExtValues.v @@ -0,0 +1,123 @@ +Require Import Coqlib. +Require Import Integers. +Require Import Values. +Require Import Floats. +Require Import Memory. +Require Import Lia. + +Definition bits_of_float x := + match x with + | Vfloat f => Vlong (Float.to_bits f) + | _ => Vundef + end. + +Definition bits_of_single x := + match x with + | Vsingle f => Vint (Float32.to_bits f) + | _ => Vundef + end. + +Definition float_of_bits x := + match x with + | Vlong f => Vfloat (Float.of_bits f) + | _ => Vundef + end. + +Definition single_of_bits x := + match x with + | Vint f => Vsingle (Float32.of_bits f) + | _ => Vundef + end. + +Definition bitwise_select_long b vtrue vfalse := + Int64.or (Int64.and (Int64.neg b) vtrue) + (Int64.and (Int64.sub b Int64.one) vfalse). + +Lemma bitwise_select_long_true : + forall vtrue vfalse, + bitwise_select_long Int64.one vtrue vfalse = vtrue. +Proof. + intros. unfold bitwise_select_long. cbn. + change (Int64.neg Int64.one) with Int64.mone. + rewrite Int64.and_commut. + rewrite Int64.and_mone. + rewrite Int64.sub_idem. + rewrite Int64.and_commut. + rewrite Int64.and_zero. + apply Int64.or_zero. +Qed. + +Lemma bitwise_select_long_false : + forall vtrue vfalse, + bitwise_select_long Int64.zero vtrue vfalse = vfalse. +Proof. + intros. unfold bitwise_select_long. cbn. + rewrite Int64.neg_zero. + rewrite Int64.and_commut. + rewrite Int64.and_zero. + rewrite Int64.sub_zero_r. + change (Int64.neg Int64.one) with Int64.mone. + rewrite Int64.and_commut. + rewrite Int64.and_mone. + rewrite Int64.or_commut. + apply Int64.or_zero. +Qed. + +Definition select01_long (vb : val) (vtrue : val) (vfalse : val) : val := + match vb with + | (Vint b) => + if Int.eq b Int.one + then vtrue + else if Int.eq b Int.zero + then vfalse + 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. + +Lemma select01_long_true: + forall vt vf, + select01_long Vtrue vt vf = vt. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. reflexivity. +Qed. + +Lemma select01_long_false: + forall vt vf, + select01_long Vfalse vt vf = vf. +Proof. + intros. unfold select01_long. cbn. + rewrite Int.eq_true. + rewrite Int.eq_false. reflexivity. + cbv. discriminate. +Qed. + +Lemma float_bits_normalize: + forall v1, + ExtValues.float_of_bits (Val.normalize (ExtValues.bits_of_float v1) AST.Tlong) = + Val.normalize v1 AST.Tfloat. +Proof. + destruct v1; cbn; trivial. + f_equal. + apply Float.of_to_bits. +Qed. + +Lemma single_bits_normalize: + forall v1, + ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) = + Val.normalize v1 AST.Tsingle. +Proof. + destruct v1; cbn; trivial. + f_equal. + apply Float32.of_to_bits. +Qed. |