-
Notifications
You must be signed in to change notification settings - Fork 1
/
Generators.v
216 lines (189 loc) · 7.23 KB
/
Generators.v
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
Require Import ZArith PArith Lia List String.
Require Import Flocq.IEEE754.Binary Flocq.Core.Zaux Flocq.IEEE754.Bits.
Require Import Basics RelationClasses.
Import ListNotations.
From QuickChick Require Import QuickChick.
Set Warnings "-extraction-opaque-accessed,-extraction".
(** [subst_max] performs as many [subst] as possible, clearing all
trivial equalities from the context. *)
Ltac subst_max :=
repeat match goal with
| [H : ?X = _ |- _ ] => subst X
| [H : _ = ?X |- _] => subst X
end.
(** The Coq [inversion] tries to preserve your context by only adding
new equalities, and keeping the inverted hypothesis. Often, you
want the resulting equalities to be substituted everywhere. [inv]
performs this post-substitution. Often, you don't need the
original hypothesis anymore. [invc] extends [inv] and removes the
inverted hypothesis. Sometimes, you also want to perform
post-simplification. [invcs] extends [invc] and tries to simplify
what it can. *)
Ltac inv H := inversion H; subst_max.
Ltac invc H := inv H; clear H.
Ltac invcs H := invc H; simpl in *.
(** [tuple_inversion] inverses an equality of tuple into
equalities for each component. *)
Ltac tuple_inversion :=
match goal with
| [ H : (_, _, _, _) = (_, _, _, _) |- _ ] => invc H
| [ H : (_, _, _) = (_, _, _) |- _ ] => invc H
| [ H : (_, _) = (_, _) |- _ ] => invc H
end.
Open Scope string.
Instance show_binary : forall (prec emax : Z), Show (binary_float prec emax) := {
show c := match c with
| B754_zero _ _ false => "+0"
| B754_zero _ _ true => "-0"
| B754_infinity _ _ false => "+inf"
| B754_infinity _ _ true => "-inf"
| B754_nan _ _ false _ _ => "+NaN"
| B754_nan _ _ true _ _ => "-NaN"
| B754_finite _ _ s m e _ => (if s then "" else "-")
++ (show_Z (Z.pos m * 2 ^ e))
end
}.
Close Scope string.
Open Scope Z.
Let log2 := log_inf.
Let digits := compose Z.succ log2.
Lemma digits2_pos_log2 (m : positive) :
Z.pos (Digits.digits2_pos m) = Z.succ (log2 m).
Proof.
induction m; simpl; try (rewrite Pos2Z.inj_succ, IHm); reflexivity.
Qed.
Lemma digits2_pos_digits (m : positive) :
Z.pos (Digits.digits2_pos m) = digits m.
Proof.
unfold digits, compose.
apply digits2_pos_log2.
Qed.
(** ** Flocq's Binary.bounded rewritten in a form close to IEEE-754 *)
Lemma bounded_unfolded (prec emax : Z)
(prec_gt_0 : Flocq.Core.FLX.Prec_gt_0 prec) (Hmax : (prec < emax)%Z)
(m : positive) (e : Z) :
bounded prec emax m e = true
<->
(digits m < prec /\ e = 3 - emax - prec) \/
(digits m = prec /\ 3 - emax - prec <= e <= emax - prec).
Proof.
unfold FLX.Prec_gt_0, bounded, canonical_mantissa, FLT.FLT_exp in *.
rewrite Bool.andb_true_iff, Z.leb_le, <-Zeq_is_eq_bool, digits2_pos_digits.
remember (3 - emax - prec) as emin.
split; intro.
all: destruct (Z_lt_le_dec (digits m + e - prec) emin).
all: try rewrite Z.max_r in * by lia.
all: try rewrite Z.max_l in * by lia.
all: lia.
Qed.
Definition binary32 := binary_float 24 128.
Definition binary64 := binary_float 53 1024.
(* Generates B754_zero values *)
Definition zerg (prec emax : Z) :=
(liftGen (fun (s : bool) => B754_zero prec emax s))
(choose (true, false)).
(* Generates B754_infinity values *)
Definition infg (prec emax : Z) :=
(liftGen (fun (s : bool) => B754_infinity prec emax s))
(choose (true, false)).
(* Generates B754_nan values. Needs payload and nan_pl proof *)
Definition nang (prec emax : Z)
(pl : positive)
(np : nan_pl prec pl = true) :=
(liftGen (fun b => B754_nan prec emax b pl np))
(choose (true, false)).
Definition boundaries (prec emax : Z) (t : bool) :=
if t
then (1, 2^prec - 1, 3 - emax - prec, 3 - emax - prec)%Z
else (2^(prec - 1), 2^prec - 1, 3 - emax - prec, emax - prec)%Z.
(* Generates B754_finite values. Needs prec_gt_0 Hmax proof *)
Program Definition fing (prec emax : Z)
(prec_gt_0 : Flocq.Core.FLX.Prec_gt_0 prec)
(Hmax : (prec < emax)%Z) : G (binary_float prec emax) :=
bindGen' (choose (false, true)) (fun t => fun b0 =>
bindGen' (returnGen (boundaries prec emax t))
(fun '(m_min, m_max, e_min, e_max) => fun b1 =>
bindGen' (choose (false, true)) (fun (s : bool) => fun b2 =>
bindGen' (choose (m_min, m_max)) (fun (m : Z) => fun b3 =>
bindGen' (choose (e_min, e_max)) (fun (e : Z) => fun b4 =>
returnGen (B754_finite prec emax s (Z.to_pos m) e _)))))).
Next Obligation.
(* get rid of technical junk *)
clear s b0 b2; rename b3 into b2, b4 into b3.
apply semReturn in b1.
apply semChoose in b2.
apply semChoose in b3.
all: unfold is_true, set1, boundaries in *.
(* simplify *)
apply andb_prop in b2; destruct b2 as [B11 B12].
apply andb_prop in b3; destruct b3 as [B21 B22].
all: destruct t; try rewrite Z.leb_le in *.
Opaque Z.sub.
all: tuple_inversion.
all: try unfold FLX.Prec_gt_0 in *.
(* main goals *)
(* first main goal *)
1,2: rewrite bounded_unfolded.
all: unfold digits, Basics.compose, Z.succ, FLX.Prec_gt_0.
all: try lia.
1,2: rewrite <-Zlog2_log_inf.
1,2: rewrite Z2Pos.id.
2: lia.
assert (m < 2 ^ prec) by lia; clear B12; rename H into B12.
rewrite Z.log2_lt_pow2 in B12.
lia.
lia.
(* second main goal *)
assert (m < 2 ^ prec) by lia; clear B12; rename H into B12.
rewrite Z.log2_lt_pow2 in B12.
rewrite Z.log2_le_pow2 in B11.
right.
lia.
(* subgoals *)
1,2,3: clear Hmax e B21 B22 B12.
1,2,3: assert (0 <= prec - 1) by lia.
1,2,3: assert (0 < 2 ^ (prec - 1)).
1,3,5: apply Z.pow_pos_nonneg.
1,3,5: reflexivity.
1,2,3: auto.
1,2,3: lia.
-
assert (T : (1) = (2 - 1)) by lia; rewrite T; clear T.
rewrite <-Z.sub_le_mono_r.
assert (T : (2) = (2 ^ 1)) by lia; rewrite T; clear T.
apply Z.pow_le_mono_r; lia; lia.
-
clear m b2 e b3 H Hmax emax.
assert (2 ^ (prec - 1) < 2 ^ prec); [| lia].
apply Z.pow_lt_mono_r; lia.
Qed.
Theorem fing32_prec : FLX.Prec_gt_0 24.
Proof. unfold FLX.Prec_gt_0; reflexivity. Qed.
Theorem fing32_prec_emax : 24 < 128.
Proof. reflexivity. Qed.
(* Set of binary32 sub-generators *)
Definition zerg32 := zerg 24 128.
Definition infg32 := infg 24 128.
Definition nang32 (pl : positive) (np : nan_pl 24 pl = true)
:= nang 24 128 pl np.
Definition fing32 := fing 24 128 fing32_prec fing32_prec_emax.
(* Full binary32 generator *)
Definition binary32_gen (pl : positive) (np : nan_pl 24 pl = true)
: G (binary32) :=
freq_ zerg32 [(1, zerg32)%nat ; (1, infg32)%nat ;
(1, nang32 pl np)%nat ; (7, fing32)%nat].
Theorem fing64_prec : FLX.Prec_gt_0 53.
Proof. unfold FLX.Prec_gt_0; reflexivity. Qed.
Theorem fing64_prec_emax : 53 < 1024.
Proof. reflexivity. Qed.
(* Set of binary64 sub-generators *)
Definition zerg64 := zerg 53 1024.
Definition infg64 := infg 53 1024.
Definition nang64 (pl : positive) (np : nan_pl 53 pl = true)
:= nang 53 1024 pl np.
Definition fing64 := fing 53 1024 fing64_prec fing64_prec_emax.
(* Full binary64 generator *)
Definition binary64_gen (pl : positive) (np : nan_pl 53 pl = true)
: G (binary64) :=
freq_ zerg64 [(1, zerg64)%nat ; (1, infg64)%nat ;
(1, nang64 pl np)%nat ; (7, fing64)%nat].