blob: edf359ef21314f6af17c2033ab466d1e1d96b59a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
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.
|
