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
0edbe5e7
Commit
0edbe5e7
authored
Mar 09, 2018
by
Heiko Becker
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Add second parameter to fixed-points, tracking fractional bits
parent
fa1630cc
Changes
10
Expand all
Hide whitespace changes
Inline
Side-by-side
Showing
10 changed files
with
525 additions
and
396 deletions
+525
-396
coq/Expressions.v
coq/Expressions.v
+5
-90
coq/FPRangeValidator.v
coq/FPRangeValidator.v
+4
-5
coq/IEEE_connection.v
coq/IEEE_connection.v
+9
-9
coq/Infra/ExpressionAbbrevs.v
coq/Infra/ExpressionAbbrevs.v
+1
-1
coq/Infra/Ltacs.v
coq/Infra/Ltacs.v
+9
-0
coq/Infra/MachineType.v
coq/Infra/MachineType.v
+98
-64
coq/Infra/RationalSimps.v
coq/Infra/RationalSimps.v
+5
-5
coq/Infra/RealRationalProps.v
coq/Infra/RealRationalProps.v
+6
-4
coq/Infra/RealSimps.v
coq/Infra/RealSimps.v
+6
-2
coq/OrderedExpressions.v
coq/OrderedExpressions.v
+382
-216
No files found.
coq/Expressions.v
View file @
0edbe5e7
...
...
@@ -2,12 +2,11 @@
Formalization
of
the
base
exprression
language
for
the
flover
framework
**
)
From
Coq
Require
Import
Reals
.
Reals
micromega
.
Psatz
QArith
.
QArith
QArith
.
Qreals
Structures
.
Orders
.
Require
Import
Flover
.
Infra
.
RealRationalProps
Flover
.
Infra
.
RationalSimps
Flover
.
Infra
.
Ltacs
.
Require
Export
Flover
.
Infra
.
Abbrevs
Flover
.
Infra
.
RealSimps
Flover
.
Infra
.
NatSet
Flover
.
IntervalArithQ
Flover
.
IntervalArith
Flover
.
Infra
.
MachineType
.
Require
Import
Structures
.
Orders
.
From
Flover
Require
Import
Infra
.
RealRationalProps
Infra
.
Ltacs
.
From
Flover
Require
Export
Infra
.
Abbrevs
Infra
.
NatSet
Infra
.
MachineType
.
(
**
Expressions
will
use
binary
operators
.
...
...
@@ -113,90 +112,6 @@ Inductive expr (V:Type): Type :=
|
Fma
:
expr
V
->
expr
V
->
expr
V
->
expr
V
|
Downcast
:
mType
->
expr
V
->
expr
V
.
(
**
Boolean
equality
function
on
exprressions
.
Used
in
certificates
to
define
the
analysis
result
as
function
**
)
Fixpoint
exprEq
(
e1
:
expr
Q
)
(
e2
:
expr
Q
)
:=
match
e1
,
e2
with
|
Var
_
v1
,
Var
_
v2
=>
(
v1
=?
v2
)
|
Const
m1
n1
,
Const
m2
n2
=>
(
mTypeEq
m1
m2
)
&&
(
Qeq_bool
n1
n2
)
|
Unop
o1
e11
,
Unop
o2
e22
=>
(
unopEq
o1
o2
)
&&
(
exprEq
e11
e22
)
|
Binop
o1
e11
e12
,
Binop
o2
e21
e22
=>
(
binopEq
o1
o2
)
&&
(
exprEq
e11
e21
)
&&
(
exprEq
e12
e22
)
|
Fma
e11
e12
e13
,
Fma
e21
e22
e23
=>
(
exprEq
e11
e21
)
&&
(
exprEq
e12
e22
)
&&
(
exprEq
e13
e23
)
|
Downcast
m1
f1
,
Downcast
m2
f2
=>
(
mTypeEq
m1
m2
)
&&
(
exprEq
f1
f2
)
|
_
,
_
=>
false
end
.
Lemma
exprEq_refl
e
:
exprEq
e
e
=
true
.
Proof
.
induction
e
;
try
(
apply
andb_true_iff
;
split
);
simpl
in
*
;
auto
.
-
symmetry
;
apply
beq_nat_refl
.
-
apply
mTypeEq_refl
.
-
apply
Qeq_bool_iff
;
lra
.
-
case
u
;
auto
.
-
case
b
;
auto
.
-
firstorder
.
-
apply
mTypeEq_refl
.
Qed
.
Lemma
exprEq_sym
e
e
'
:
exprEq
e
e
'
=
exprEq
e
'
e
.
Proof
.
revert
e
'
.
induction
e
;
intros
e
'
;
destruct
e
'
;
simpl
;
try
auto
.
-
apply
Nat
.
eqb_sym
.
-
f_equal
.
+
apply
mTypeEq_sym
;
auto
.
+
apply
Qeq_bool_sym
.
-
f_equal
.
+
destruct
u
;
auto
.
+
apply
IHe
.
-
f_equal
.
+
f_equal
.
*
destruct
b
;
auto
.
*
apply
IHe1
.
+
apply
IHe2
.
-
f_equal
.
+
f_equal
;
auto
.
+
auto
.
-
f_equal
.
+
apply
mTypeEq_sym
;
auto
.
+
apply
IHe
.
Qed
.
Lemma
exprEq_trans
e
f
g
:
exprEq
e
f
=
true
->
exprEq
f
g
=
true
->
exprEq
e
g
=
true
.
Proof
.
revert
e
f
g
;
induction
e
;
destruct
f
;
intros
g
eq1
eq2
;
destruct
g
;
cbn
in
*
;
try
rewrite
Nat
.
eqb_eq
in
*
;
Flover_compute
;
try
congruence
;
type_conv
;
subst
;
try
auto
.
-
rewrite
mTypeEq_refl
;
simpl
.
rewrite
Qeq_bool_iff
in
*
;
lra
.
-
rewrite
unopEq_compat_eq
in
*
;
subst
.
rewrite
unopEq_refl
;
simpl
.
eapply
IHe
;
eauto
.
-
rewrite
binopEq_compat_eq
in
*
;
subst
.
rewrite
binopEq_refl
;
simpl
.
apply
andb_true_iff
.
split
;
[
eapply
IHe1
;
eauto
|
eapply
IHe2
;
eauto
].
-
rewrite
andb_true_iff
.
rewrite
andb_true_iff
.
split
;
[
split
;
[
eapply
IHe1
;
eauto
|
eapply
IHe2
;
eauto
]
|
eapply
IHe3
;
eauto
].
-
rewrite
mTypeEq_refl
;
simpl
.
eapply
IHe
;
eauto
.
Qed
.
Fixpoint
toRExp
(
e
:
expr
Q
)
:=
match
e
with
|
Var
_
v
=>
Var
R
v
...
...
coq/FPRangeValidator.v
View file @
0edbe5e7
(
*
TODO
:
Flocq
ops
open
machine_ieeeTheory
binary_ieeeTheory
lift_ieeeTheory
realTheory
*
)
Require
Import
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qreals
Coq
.
Reals
.
Reals
Coq
.
micromega
.
Psatz
.
Require
Import
Flover
.
Infra
.
MachineType
Flover
.
Typing
Flover
.
Infra
.
RealSimps
Flover
.
IntervalValidation
Flover
.
ErrorValidation
Flover
.
Commands
Flover
.
Environments
Flover
.
ssaPrgs
Flover
.
Infra
.
Ltacs
Flover
.
Infra
.
RealRationalProps
.
From
Flover
Require
Import
Expressions
Commands
Environments
ssaPrgs
Typing
IntervalValidation
ErrorValidation
Infra
.
Ltacs
Infra
.
RealRationalProps
.
Fixpoint
FPRangeValidator
(
e
:
expr
Q
)
(
A
:
analysisResult
)
typeMap
dVars
{
struct
e
}
:
bool
:=
match
FloverMap
.
find
e
typeMap
,
FloverMap
.
find
e
A
with
...
...
@@ -67,7 +66,7 @@ Ltac prove_fprangeval m v L1 R:=
|
H
:
_
=
true
|-
_
=>
andb_to_prop
H
end
);
destruct
(
Req_dec
v
0
);
try
auto
;
destruct
(
Rle_lt_dec
(
Rabs
v
)
(
Q2R
(
minValue
m
)))
%
R
(
*
denormal
case
*
);
destruct
(
Rle_lt_dec
(
Rabs
v
)
(
Q2R
(
minValue
_pos
m
)))
%
R
(
*
denormal
case
*
);
try
auto
;
destruct
(
Rle_lt_dec
(
Rabs
v
)
(
Q2R
(
maxValue
m
)))
%
R
;
lra
.
...
...
coq/IEEE_connection.v
View file @
0edbe5e7
...
...
@@ -17,7 +17,7 @@ Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :
end
.
Definition
normal_or_zero
v
:=
(
v
=
0
\
/
(
Q2R
(
minValue
M64
))
<=
(
Rabs
v
))
%
R
.
(
v
=
0
\
/
(
Q2R
(
minValue
_pos
M64
))
<=
(
Rabs
v
))
%
R
.
Definition
updFlEnv
x
v
E
:=
fun
y
=>
if
y
=?
x
...
...
@@ -239,7 +239,7 @@ Proof.
unfold
validFloatValue
,
B2Q
in
*
.
destruct
v
;
try
auto
;
destruct
validVal
;
unfold
Normal
in
*
;
unfold
Denormal
in
*
;
unfold
maxValue
,
minValue
,
maxExponent
,
minExponentPos
in
*
;
unfold
maxValue
,
minValue
_pos
,
maxExponent
,
minExponentPos
in
*
;
rewrite
Q2R_inv
in
*
;
unfold
bpowQ
in
*
.
-
assert
(
Z
.
pow_pos
radix2
1024
=
179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216
%
Z
)
by
(
vm_compute
;
auto
).
...
...
@@ -445,7 +445,7 @@ Proof.
(
evalBinop
b
(
B2R
53
1024
v_e1
)
(
B2R
53
1024
v_e2
))
%
R
).
destruct
(
rel_error_exists
)
as
[
eps
[
bounded_eps
round_eq
]].
+
eapply
Rle_trans
;
eauto
.
unfold
minValue
,
Z
.
pow_pos
;
simpl
.
unfold
minValue
_pos
,
Z
.
pow_pos
;
simpl
.
rewrite
Q2R_inv
.
*
apply
Rinv_le
.
{
rewrite
<-
Q2R0_is_0
.
apply
Qlt_Rlt
.
...
...
@@ -463,7 +463,7 @@ Proof.
repeat
rewrite
<-
INR_IPR
.
simpl
.
lra
.
*
unfold
Denormal
in
*
.
destruct
denormal_v
.
eapply
Rlt_trans
;
eauto
.
unfold
minValue
,
minExponentPos
,
bpow
.
unfold
minValue
_pos
,
minExponentPos
,
bpow
.
rewrite
Q2R_inv
.
{
unfold
Q2R
,
Qnum
,
Qden
.
rewrite
<-
Z2R_IZR
;
unfold
IZR
.
...
...
@@ -699,7 +699,7 @@ Proof.
rewrite
B2Q_B2R_eq
in
zero_b
;
auto
.
rewrite
zero_b
in
*
.
rewrite
Rabs_R0
in
H1
.
unfold
minValue
,
minExponentPos
in
H1
.
unfold
minValue
_pos
,
minExponentPos
in
H1
.
rewrite
Q2R_inv
in
H1
;
[
|
vm_compute
;
congruence
].
unfold
Q2R
,
Qnum
,
Qden
in
H1
.
assert
(
Z
.
pow_pos
2
1022
=
44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304
%
Z
)
...
...
@@ -732,7 +732,7 @@ Proof.
(
fun
x
=>
negb
(
Zeven
x
))
(
B2R
53
1024
v_e1
+
B2R
53
1024
v_e2
)
%
R
)
as
[
eps
[
eps_bounded
round_eq
]].
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
,
minExponentPos
.
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
_pos
,
minExponentPos
.
rewrite
Q2R_inv
;
[
|
vm_compute
;
congruence
].
unfold
Q2R
,
Qnum
,
Qden
.
rewrite
<-
Z2R_IZR
.
vm_compute
.
lra
.
}
...
...
@@ -776,7 +776,7 @@ Proof.
(
fun
x
=>
negb
(
Zeven
x
))
(
B2R
53
1024
v_e1
-
B2R
53
1024
v_e2
)
%
R
)
as
[
eps
[
eps_bounded
round_eq
]].
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
,
minExponentPos
.
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
_pos
,
minExponentPos
.
rewrite
Q2R_inv
;
[
|
vm_compute
;
congruence
].
unfold
Q2R
,
Qnum
,
Qden
.
rewrite
<-
Z2R_IZR
.
vm_compute
.
lra
.
}
...
...
@@ -822,7 +822,7 @@ Proof.
(
fun
x
=>
negb
(
Zeven
x
))
(
B2R
53
1024
v_e1
*
B2R
53
1024
v_e2
)
%
R
)
as
[
eps
[
eps_bounded
round_eq
]].
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
,
minExponentPos
.
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
_pos
,
minExponentPos
.
rewrite
Q2R_inv
;
[
|
vm_compute
;
congruence
].
unfold
Q2R
,
Qnum
,
Qden
.
rewrite
<-
Z2R_IZR
.
vm_compute
.
lra
.
}
...
...
@@ -869,7 +869,7 @@ Proof.
(
fun
x
=>
negb
(
Zeven
x
))
(
B2R
53
1024
v_e1
/
B2R
53
1024
v_e2
)
%
R
)
as
[
eps
[
eps_bounded
round_eq
]].
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
,
minExponentPos
.
{
eapply
Rle_trans
;
eauto
.
unfold
minValue
_pos
,
minExponentPos
.
rewrite
Q2R_inv
;
[
|
vm_compute
;
congruence
].
unfold
Q2R
,
Qnum
,
Qden
.
rewrite
<-
Z2R_IZR
.
vm_compute
.
lra
.
}
...
...
coq/Infra/ExpressionAbbrevs.v
View file @
0edbe5e7
...
...
@@ -6,7 +6,7 @@ Require Import Coq.QArith.QArith Coq.Reals.Reals Coq.QArith.Qreals Coq.QArith.QO
Require
Export
Flover
.
Infra
.
Abbrevs
Flover
.
Expressions
Flover
.
OrderedExpressions
.
Module
Q_orderedExps
:=
ExpOrderedType
(
Q_as_OT
).
Module
Q_orderedExps
:=
Exp
r
OrderedType
(
Q_as_OT
).
Module
legacy_OrderedQExps
:=
Structures
.
OrdersAlt
.
Backport_OT
(
Q_orderedExps
).
Module
FloverMap
:=
FMapAVL
.
Make
(
legacy_OrderedQExps
).
...
...
coq/Infra/Ltacs.v
View file @
0edbe5e7
...
...
@@ -17,6 +17,15 @@ Ltac andb_to_prop H :=
try
andb_to_prop
Left
;
try
andb_to_prop
Right
.
Ltac
split_bool
:=
match
goal
with
|
[
|-
(
_
&&
_
)
=
true
]
=>
apply
Is_true_eq_true
;
apply
andb_prop_intro
;
split
;
apply
Is_true_eq_left
|
_
=>
fail
"Cannot case split on non-boolean conjunction"
end
.
Ltac
canonize_Q_prop
:=
match
goal
with
|
[
H
:
Qle_bool
?
a
?
b
=
true
|-
_
]
=>
rewrite
Qle_bool_iff
in
H
...
...
coq/Infra/MachineType.v
View file @
0edbe5e7
...
...
@@ -4,31 +4,42 @@
@
author
:
Raphael
Monat
@
maintainer
:
Heiko
Becker
**
)
Require
Import
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qminmax
Coq
.
QArith
.
Qabs
Coq
.
QArith
.
Qpower
Coq
.
QArith
.
Qreals
Coq
.
Reals
.
Reals
Coq
.
micromega
.
Psatz
.
Require
Import
Flover
.
Infra
.
RealRationalProps
Flover
.
Infra
.
PosSimps
.
(
**
Define
machine
precision
as
datatype
.
**
)
Inductive
mType
:
Type
:=
M0
|
M16
|
M32
|
M64
|
F
(
w
:
positive
).
(
*|
M128
|
M256
*
)
(
*
From
Coq
*
)
(
*
Require
Import
QArith
.
QArith
QArith
.
Qminmax
QArith
.
Qabs
QArith
.
Qpower
*
)
(
*
QArith
.
Qreals
Reals
.
Reals
micromega
.
Psatz
.
*
)
(
*
From
Flover
Require
Import
Infra
.
RealRationalProps
Infra
.
Ltacs
.
*
)
(
*
<<<<<<<
ours
*
)
(
*
=======
*
)
From
Coq
.
QArith
Require
Import
Qpower
.
From
Flover
Require
Import
Infra
.
RealRationalProps
Infra
.
Ltacs
.
(
**
Injection
of
machine
types
into
Q
To
support
fixed
-
point
values
,
we
add
an
additional
paramer
,
v
which
is
the
value
represented
,
as
the
error
depends
on
the
fraction
bits
which
in
turn
depend
on
the
value
represented
Define
machine
precision
as
datatype
.
We
treat
Fixed
-
point
types
as
floats
,
like
Flocq
,
where
f
:
positive
specifies
the
fraction
size
and
w
:
the
width
of
the
base
field
.
**
)
Inductive
mType
:
Type
:=
M0
|
M16
|
M32
|
M64
|
F
(
w
:
positive
)
(
f
:
positive
).
(
*|
M128
|
M256
*
)
(
**
Compute
a
machine
epsilon
from
a
machine
types
in
Q
**
)
Definition
mTypeToQ
(
m
:
mType
)
(
v
:
Q
)
:
Q
:=
Definition
mTypeToQ
(
m
:
mType
)
:
Q
:=
match
m
with
|
M0
=>
0
|
M16
=>
(
Qpower
(
2
#
1
)
(
Zneg
11
))
|
M32
=>
(
Qpower
(
2
#
1
)
(
Zneg
24
))
|
M64
=>
(
Qpower
(
2
#
1
)
(
Zneg
53
))
|
F
w
=>
(
Qpower
(
2
#
1
)
(
Zneg
(
fractionBits
w
v
))
)
|
F
w
f
=>
Qpower
(
2
#
1
)
(
Zneg
f
)
(
*
(
*
the
epsilons
below
match
what
is
used
internally
in
flover
,
(
*
the
epsilons
below
match
what
is
used
internally
in
Daisy
,
although
these
value
do
not
match
the
IEEE
standard
*
)
|
M128
=>
(
Qpower
(
2
#
1
)
(
Zneg
105
))
|
M256
=>
(
Qpower
(
2
#
1
)
(
Zneg
211
))
*
)
...
...
@@ -37,17 +48,16 @@ Definition mTypeToQ (m:mType) (v:Q):Q :=
Arguments
mTypeToQ
_
/
.
Lemma
mTypeToQ_pos_Q
:
forall
m
v
,
0
<=
mTypeToQ
m
v
.
forall
m
,
0
<=
mTypeToQ
m
.
Proof
.
intros
*
.
destruct
m
eqn
:?
;
cbn
;
try
lra
.
pose
proof
(
Qpower_pos
(
2
#
1
)
(
Zneg
(
fractionBits
w
v
)))
as
pos_pow
.
cbn
in
*
.
apply
pos_pow
;
lra
.
intro
e
.
case_eq
e
;
intros
;
unfold
mTypeToQ
;
try
(
apply
Qle_bool_iff
;
auto
;
fail
).
apply
Qpower_pos
;
lra
.
Qed
.
Lemma
mTypeToQ_pos_R
:
forall
m
v
,
(
0
<=
Q2R
(
mTypeToQ
m
v
))
%
R
.
forall
m
,
(
0
<=
Q2R
(
mTypeToQ
m
))
%
R
.
Proof
.
intros
*
.
rewrite
<-
Q2R0_is_0
.
...
...
@@ -61,7 +71,7 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
|
M16
,
M16
=>
true
|
M32
,
M32
=>
true
|
M64
,
M64
=>
true
|
F
w1
,
F
w2
=>
(
w1
=?
w
2
)
%
positive
|
F
w1
f1
,
F
w2
f2
=>
(
w1
=?
w2
)
%
positive
&&
(
f1
=?
f
2
)
%
positive
(
*
|
M128
,
M128
=>
true
*
)
(
*
|
M256
,
M256
=>
true
*
)
|
_
,
_
=>
false
...
...
@@ -70,7 +80,8 @@ Definition mTypeEq (m1:mType) (m2:mType) :=
Lemma
mTypeEq_refl
(
m
:
mType
)
:
mTypeEq
m
m
=
true
.
Proof
.
intros
.
destruct
m
;
try
auto
;
simpl
.
apply
Pos
.
eqb_refl
.
intros
.
destruct
m
;
try
auto
;
simpl
.
repeat
rewrite
Pos
.
eqb_refl
;
auto
.
Qed
.
Lemma
mTypeEq_compat_eq
(
m1
:
mType
)
(
m2
:
mType
)
:
...
...
@@ -81,7 +92,7 @@ Proof.
case_eq
m2
;
intros
*
m2_case
;
subst
;
try
congruence
;
try
auto
;
try
simpl
in
eq_case
;
try
inversion
eq_case
.
-
f_equal
.
auto
using
Peqb_true_eq
.
-
andb_to_prop
eq_case
.
f_equal
;
auto
using
Peqb_true_eq
.
-
inversion
m2_case
.
apply
mTypeEq_refl
.
Qed
.
...
...
@@ -92,8 +103,9 @@ Proof.
-
hnf
;
intros
;
subst
.
rewrite
mTypeEq_refl
in
eq_case
.
congruence
.
-
case_eq
m1
;
intros
;
case_eq
m2
;
intros
;
subst
;
simpl
;
try
congruence
.
assert
(
w
<>
w0
)
by
(
hnf
;
intros
;
subst
;
congruence
).
rewrite
Pos
.
eqb_neq
;
auto
.
destruct
(
w
=?
w0
)
%
positive
eqn
:?
;
try
auto
.
destruct
(
f
=?
f0
)
%
positive
eqn
:?
;
try
auto
.
rewrite
Pos
.
eqb_eq
in
*
;
subst
.
congruence
.
Qed
.
Ltac
type_conv
:=
...
...
@@ -108,36 +120,40 @@ Lemma mTypeEq_sym (m1:mType) (m2:mType):
Proof
.
intros
.
destruct
m1
,
m2
;
simpl
;
auto
.
rewrite
Pos
.
eqb_sym
;
f_equal
.
apply
Pos
.
eqb_sym
.
Qed
.
(
**
Check
if
machine
precision
m1
is
more
precise
than
machine
precision
m2
.
M0
is
real
-
valued
evaluation
,
hence
the
most
precise
.
All
other
s
are
compared
by
All
floating
-
point
type
s
are
compared
by
mTypeToQ
m1
<=
mTypeToQ
m2
For
the
moment
,
fixed
-
point
and
floating
-
point
formats
are
incomparable
**
)
Definition
isMorePrecise
(
m1
:
mType
)
(
m2
:
mType
)
:=
match
m1
,
m2
with
|
M0
,
_
=>
true
|
F
f1
,
F
f2
=>
(
f1
<=?
f2
)
%
positive
|
F
f
,
_
=>
false
|
_
,
F
f
=>
false
|
_
,
_
=>
Qle_bool
(
mTypeToQ
m1
0
)
(
mTypeToQ
m2
0
)
|
F
w1
f1
,
F
w2
f2
=>
(
w1
<=?
w2
)
%
positive
&&
(
f1
<=?
f2
)
%
positive
|
F
w
f
,
_
=>
false
|
_
,
F
w
f
=>
false
|
_
,
_
=>
Qle_bool
(
mTypeToQ
m1
)
(
mTypeToQ
m2
)
end
.
(
*
More
efficient
version
for
performance
,
unfortunately
we
cannot
do
better
for
fixed
-
points
*
)
Definition
morePrecise
(
m1
:
mType
)
(
m2
:
mType
)
:=
match
m1
,
m2
with
|
M0
,
_
=>
true
|
F
w1
,
F
w2
=>
(
w1
<=?
w
2
)
%
positive
|
_
,
F
w
=>
false
|
F
w
,
_
=>
false
|
M16
,
M16
=>
true
|
M32
,
M32
=>
true
|
M32
,
M16
=>
true
|
M64
,
M0
=>
false
|
M64
,
_
=>
true
|
_
,
_
=>
false
|
M0
,
_
=>
true
|
F
w1
f1
,
F
w2
f2
=>
(
w1
<=?
w2
)
%
positive
&&
(
f1
<=?
f
2
)
%
positive
|
_
,
F
w
f
=>
false
|
F
w
f
,
_
=>
false
|
M16
,
M16
=>
true
|
M32
,
M32
=>
true
|
M32
,
M16
=>
true
|
M64
,
M0
=>
false
|
M64
,
_
=>
true
|
_
,
_
=>
false
end
.
Lemma
morePrecise_antisym
m1
m2
:
...
...
@@ -146,8 +162,11 @@ Lemma morePrecise_antisym m1 m2:
mTypeEq
m1
m2
=
true
.
Proof
.
destruct
m1
;
destruct
m2
;
simpl
;
auto
.
intros
le_m1m2
le_m2m1
.
apply
Pos
.
eqb_eq
.
apply
Pos
.
leb_le
in
le_m1m2
;
apply
Pos
.
leb_le
in
le_m2m1
.
intros
le_m1m2
le_m2m1
.
andb_to_prop
le_m1m2
.
andb_to_prop
le_m2m1
.
apply
Pos
.
leb_le
in
L
;
apply
Pos
.
leb_le
in
R
.
apply
Pos
.
leb_le
in
L0
;
apply
Pos
.
leb_le
in
R0
.
split_bool
;
apply
Pos
.
eqb_eq
;
apply
Pos
.
le_antisym
;
auto
.
Qed
.
...
...
@@ -158,8 +177,11 @@ Lemma morePrecise_trans m1 m2 m3:
Proof
.
destruct
m1
;
destruct
m2
;
destruct
m3
;
simpl
;
auto
;
intros
le1
le2
;
try
congruence
.
apply
Pos
.
leb_le
.
apply
Pos
.
leb_le
in
le1
.
apply
Pos
.
leb_le
in
le2
.
andb_to_prop
le1
;
andb_to_prop
le2
.
apply
Pos
.
leb_le
in
L
;
apply
Pos
.
leb_le
in
R
;
apply
Pos
.
leb_le
in
L0
;
apply
Pos
.
leb_le
in
R0
.
split_bool
;
apply
Pos
.
leb_le
;
eapply
Pos
.
le_trans
;
eauto
.
Qed
.
...
...
@@ -173,7 +195,8 @@ Lemma isMorePrecise_refl (m:mType) :
isMorePrecise
m
m
=
true
.
Proof
.
unfold
isMorePrecise
;
destruct
m
;
simpl
;
try
auto
.
apply
Pos
.
leb_le
.
apply
Pos
.
le_refl
.
split_bool
;
apply
Pos
.
leb_le
;
apply
Pos
.
le_refl
.
Qed
.
Lemma
M0_least_precision
(
m
:
mType
)
:
...
...
@@ -215,7 +238,7 @@ Definition maxExponent (m:mType) :positive :=
|
M16
=>
15
|
M32
=>
127
|
M64
=>
1023
|
F
f
=>
f
|
F
w
f
=>
f
end
.
Definition
minExponentPos
(
m
:
mType
)
:
positive
:=
...
...
@@ -224,38 +247,49 @@ Definition minExponentPos (m:mType) :positive :=
|
M16
=>
14
|
M32
=>
126
|
M64
=>
1022
|
F
f
=>
f
|
F
w
f
=>
f
end
.
(
**
Goldberg
-
Handbook
of
Floating
-
Point
Arithmetic
:
(
p
.183
)
(
𝛃
-
𝛃
^
(
1
-
p
))
*
𝛃
^
(
e_max
)
which
simplifies
to
2
^
(
e_max
)
for
base
2
Floating
-
point
types
:
Goldberg
-
Handbook
of
Floating
-
Point
Arithmetic
:
(
p
.183
)
(
𝛃
-
𝛃
^
(
1
-
p
))
*
𝛃
^
(
e_max
)
which
simplifies
to
2
^
(
e_max
)
for
base
2
Fixed
-
Points
:
it
is
maximum
possible
representable
integer
for
the
given
bits
w
times
the
maximum
possible
exponent
(
f
)
**
)
Definition
maxValue
(
m
:
mType
)
:=
(
Z
.
pow_pos
2
(
maxExponent
m
))
#
1.
match
m
with
|
F
w
f
=>
((
Z
.
pow_pos
2
(
w
-
1
))
-
1
)
*
(
Z
.
pow_pos
2
(
maxExponent
m
))
#
1
|
_
=>
(
Z
.
pow_pos
2
(
maxExponent
m
))
#
1
end
.
Definition
minValue
(
m
:
mType
)
:=
Qinv
((
Z
.
pow_pos
2
(
minExponentPos
m
))
#
1
).
(
*
Similarly
:
minimum
values
:
we
return
0
for
fixed
-
point
numbers
here
to
make
no
fixed
-
point
number
be
a
denormal
number
ever
*
)
Definition
minValue_pos
(
m
:
mType
)
:=
match
m
with
|
F
w
f
=>
0
|
_
=>
Qinv
((
Z
.
pow_pos
2
(
minExponentPos
m
))
#
1
)
end
.
(
*
*
Goldberg
-
Handbook
of
Floating
-
Point
Arithmetic
:
(
p
.183
)
𝛃
^
(
e_min
-
p
+
1
)
=
𝛃
^
(
e_min
-
1
)
for
base
2
*
*
)
Definition
minDenormalValue
(
m
:
mType
)
:=
Qinv
(
Z
.
pow_pos
2
(
minExponentPos
m
-
1
)
#
1
).
(
*
(
**
Goldberg
-
Handbook
of
Floating
-
Point
Arithmetic
:
(
p
.183
)
*
)
(
*
𝛃
^
(
e_min
-
p
+
1
)
=
𝛃
^
(
e_min
-
1
)
for
base
2
*
)
(
*
**
)
*
)
(
*
Definition
minDenormalValue
(
m
:
mType
)
:=
*
)
(
*
Qinv
(
Z
.
pow_pos
2
(
minExponentPos
m
-
1
)
#
1
).
*
)
Definition
normal
(
v
:
Q
)
(
m
:
mType
)
:=
Qle_bool
(
minValue
m
)
(
Qabs
v
)
&&
Qle_bool
(
Qabs
v
)
(
maxValue
m
).
Qle_bool
(
minValue
_pos
m
)
(
Qabs
v
)
&&
Qle_bool
(
Qabs
v
)
(
maxValue
m
).
Definition
denormal
(
v
:
Q
)
(
m
:
mType
)
:=
Qle_bool
(
Qabs
v
)
(
minValue
m
)
&&
negb
(
Qeq_bool
v
0
).
Qle_bool
(
Qabs
v
)
(
minValue
_pos
m
)
&&
negb
(
Qeq_bool
v
0
).
Definition
Normal
(
v
:
R
)
(
m
:
mType
)
:=
(
Q2R
(
minValue
m
)
<=
(
Rabs
v
)
/
\
(
Rabs
v
)
<=
Q2R
(
maxValue
m
))
%
R
.
(
Q2R
(
minValue
_pos
m
)
<=
(
Rabs
v
)
/
\
(
Rabs
v
)
<=
Q2R
(
maxValue
m
))
%
R
.
Definition
Denormal
(
v
:
R
)
(
m
:
mType
)
:=
((
Rabs
v
)
<
Q2R
(
minValue
m
)
/
\
~
(
v
=
0
))
%
R
.
((
Rabs
v
)
<
Q2R
(
minValue
_pos
m
)
/
\
~
(
v
=
0
))
%
R
.
(
**
Predicate
that
is
true
if
and
only
if
the
given
value
v
is
a
valid
floating
-
point
value
according
to
the
the
type
m
.
...
...
@@ -272,4 +306,4 @@ Definition validValue (v:Q) (m:mType) :=
match
m
with
|
M0
=>
true
|
_
=>
Qle_bool
(
Qabs
v
)
(
maxValue
m
)
end
.
end
.
\ No newline at end of file
coq/Infra/RationalSimps.v
View file @
0edbe5e7
(
**
Some
simplification
properties
of
rationals
,
not
proven
in
the
Standard
Library
**
)
Require
Import
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qminmax
Coq
.
QArith
.
Qabs
.
Require
Import
Coq
.
micromega
.
Psatz
.
**
)
From
Coq
.
QArith
Require
Export
QArith
Qminmax
Qabs
.
From
Coq
Require
Export
micromega
.
Psatz
.
Definition
Qleb
:=
Qle_bool
.
Definition
Qeqb
:=
Qeq_bool
.
(
*
Definition
machineEpsilon
:=
(
1
#(
2
^
53
)).
*
)
Definition
maxAbs
(
iv
:
Q
*
Q
)
:=
Qmax
(
Qabs
(
fst
iv
))
(
Qabs
(
snd
iv
)).
...
...
coq/Infra/RealRationalProps.v
View file @
0edbe5e7
(
**
Some
rewriting
properties
for
translating
between
rationals
and
real
numbers
.
These
are
used
in
the
soundness
proofs
since
we
want
to
have
the
final
theorem
on
the
real
valued
evaluation
.
**
)
Require
Import
Coq
.
QArith
.
QArith
Coq
.
QArith
.
Qminmax
Coq
.
QArith
.
Qabs
Coq
.
QArith
.
Qreals
Coq
.
Reals
.
Reals
Coq
.
micromega
.
Psatz
.
Require
Import
Flover
.
Infra
.
RationalSimps
Flover
.
Infra
.
RealSimps
.
**
)
From
Coq
.
QArith
Require
Export
Qreals
.
From
Flover
.
Infra
Require
Export
RationalSimps
RealSimps
.
Lemma
Q2R0_is_0
:
Q2R
0
=
0
%
R
.
...
...
coq/Infra/RealSimps.v
View file @
0edbe5e7
...
...
@@ -2,7 +2,11 @@
Some
simplification
properties
of
real
numbers
,
not
proven
in
the
Standard
Library
**
)
Require
Import
Coq
.
Reals
.
Reals
Coq
.
micromega
.
Psatz
Coq
.
Setoids
.
Setoid
.
From
Coq
Require
Import
Setoids
.
Setoid
.
From
Coq
Require
Export
Reals
.
Reals
micromega
.
Psatz
.
(
**
Define
the
maxAbs
function
on
R
and
prove
some
minor
properties
of
it
.
TODO:
Make
use
of
IVLO
and
IVhi
...
...
@@ -73,7 +77,7 @@ Qed.
Prove
that
using
eps
=
0
makes
the
evaluation
deterministic
**
)
Lemma
Rabs_0_impl_eq
(
d
:
R
)
:
Rle
(
Rabs
d
)
R0
->
d
=
R0
.
Rle
(
Rabs
d
)
0
->
d
=
0
%
R
.
Proof
.
intros
abs_leq_0
.
pose
proof
(
Rabs_pos
d
)
as
abs_geq_0
.
...
...
coq/OrderedExpressions.v
View file @
0edbe5e7
This diff is collapsed.
Click to expand it.
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