Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
F
FloVer
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
5
Issues
5
List
Boards
Labels
Service Desk
Milestones
Operations
Operations
Incidents
Analytics
Analytics
Repository
Value Stream
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Commits
Issue Boards
Open sidebar
AVA
FloVer
Commits
85bbd305
Commit
85bbd305
authored
Mar 09, 2018
by
Heiko Becker
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' into fixed_point_checking
parents
0edbe5e7
43aa5724
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
15 additions
and
15 deletions
+15
-15
coq/IEEE_connection.v
coq/IEEE_connection.v
+15
-15
No files found.
coq/IEEE_connection.v
View file @
85bbd305
...
...
@@ -126,15 +126,15 @@ Definition bpowQ (r:radix) (e: Z) :=
Definition
B2Q
:=
fun
prec
emax
:
Z
=>
let
emin
:=
(
3
-
emax
-
prec
)
%
Z
in
let
fexpr
:=
Fcore_FLT
.
FLT_exp
r
emin
prec
in
let
fexpr
:=
Fcore_FLT
.
FLT_exp
emin
prec
in
fun
f
:
binary_float
prec
emax
=>
match
f
with
|
B754_zero
_
_
_
=>
0
%
Q
|
B754_infinity
_
_
_
=>
(
bpowQ
radix2
emax
)
+
1
%
Q
|
B754_nan
_
_
_
_
=>
(
bpowQ
radix2
emax
)
+
1
%
Q
|
B754_finite
_
_
s
m
e
_
=>
let
f_new
:
Fcore_defs
.
float
radix2
:=
{|
Fcore_defs
.
Fnum
:=
cond_Zopp
s
(
'
m
);
Fcore_defs
.
Fexp
r
:=
e
|}
in
(
Fcore_defs
.
Fnum
f_new
#
1
)
*
bpowQ
radix2
(
Fcore_defs
.
Fexp
r
f_new
)
let
f_new
:
Fcore_defs
.
float
radix2
:=
{|
Fcore_defs
.
Fnum
:=
cond_Zopp
s
(
'
m
);
Fcore_defs
.
Fexp
:=
e
|}
in
(
Fcore_defs
.
Fnum
f_new
#
1
)
*
bpowQ
radix2
(
Fcore_defs
.
Fexp
f_new
)
end
.
Lemma
B2Q_B2R_eq
:
...
...
@@ -393,7 +393,7 @@ Proof.
Qed
.
Lemma
round_0_zero
:
(
Fcore_generic_fmt
.
round
radix2
(
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
)
(
Fcore_generic_fmt
.
round
radix2
(
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
)
(
round_mode
mode_NE
)
0
)
=
0
%
R
.
Proof
.
unfold
Fcore_generic_fmt
.
round
.
simpl
.
...
...
@@ -408,7 +408,7 @@ Proof.
assert
(
Rcompare
(
0
)
(
/
2
)
=
Lt
).
{
apply
Rcompare_Lt
.
lra
.
}
rewrite
H0
.
unfold
Fcore_generic_fmt
.
canonic_exp
r
.
unfold
Fcore_generic_fmt
.
canonic_exp
.
unfold
Fcore_defs
.
F2R
;
simpl
.
rewrite
Rmult_0_l
.
auto
.
Qed
.
...
...
@@ -422,20 +422,20 @@ Lemma validValue_bounded b v_e1 v_e2:
(
Rabs
(
Fcore_generic_fmt
.
round
radix2
(
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
)
(
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
)
(
round_mode
mode_NE
)
(
evalBinop
b
(
B2R
53
1024
v_e1
)
(
B2R
53
1024
v_e2
))))
(
bpow
radix2
1024
)
=
true
.
Proof
.
simpl
.
pose
proof
(
fexp
r
_correct
53
1024
eq_refl
)
as
fexpr_corr
.
pose
proof
(
fexp_correct
53
1024
eq_refl
)
as
fexpr_corr
.
assert
(
forall
k
:
Z
,
(
-
1022
<
k
)
%
Z
->
(
53
<=
k
-
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
k
)
%
Z
)
(
53
<=
k
-
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
k
)
%
Z
)
as
expr_valid
.
{
intros
k
k_pos
.
unfold
Fcore_FLT
.
FLT_exp
r
;
simpl
.
unfold
Fcore_FLT
.
FLT_exp
;
simpl
.
destruct
(
Z
.
max_spec_le
(
k
-
53
)
(
-
1074
));
omega
.
}
pose
proof
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
)
pose
proof
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
)
(
-
1022
)
%
Z
53
%
Z
expr_valid
)
as
rel_error_exists
.
intros
[
normal_v
|
zero_v
]
validVal
;
...
...
@@ -477,7 +477,7 @@ Proof.
Qed
.
(
*
(
fexpr_correct
53
1024
eq_refl
)
as
fexpr_corr
.
*
)
(
*
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
)
*
)
(
*
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
)
*
)
(
*
(
-
1022
)
%
Z
53
%
Z
)
*
)
Lemma
eval_expr_gives_IEEE
(
e
:
expr
fl64
)
:
forall
E1
E2
E2_real
Gamma
tMap
vR
A
P
fVars
dVars
,
...
...
@@ -672,14 +672,14 @@ Proof.
clear
H2
H12
dVars_sound
dVars_valid
usedVars_64bit
vars_typed
fVars_defined
usedVars_sound
R2
R1
L1
L
R6
L0
R3
R4
L2
R5
R7
L5
Heqo
Heqo0
Heqo1
IHe1
IHe2
.
pose
proof
(
fexp
r
_correct
53
1024
eq_refl
)
as
fexpr_corr
.
pose
proof
(
fexp_correct
53
1024
eq_refl
)
as
fexpr_corr
.
assert
(
forall
k
:
Z
,
(
-
1022
<
k
)
%
Z
->
(
53
<=
k
-
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
k
)
%
Z
)
(
53
<=
k
-
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
k
)
%
Z
)
as
expr_valid
.
{
intros
k
k_pos
.
unfold
Fcore_FLT
.
FLT_exp
r
;
simpl
.
unfold
Fcore_FLT
.
FLT_exp
;
simpl
.
destruct
(
Z
.
max_spec_le
(
k
-
53
)
(
-
1074
));
omega
.
}
pose
proof
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
r
(
3
-
1024
-
53
)
53
)
pose
proof
(
relative_error_N_ex
radix2
(
Fcore_FLT
.
FLT_exp
(
3
-
1024
-
53
)
53
)
(
-
1022
)
%
Z
53
%
Z
expr_valid
)
as
rel_error_exists
.
rewrite
eval_float_e1
,
eval_float_e2
in
H1
.
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment