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.