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
ad80ecfc
Commit
ad80ecfc
authored
May 23, 2018
by
Nikita Zyuzin
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Rearrange validErrorboundAA body;
Comment the check for already visited expressions
parent
a7ec017f
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
150 additions
and
148 deletions
+150
-148
coq/ErrorValidationAA.v
coq/ErrorValidationAA.v
+150
-148
No files found.
coq/ErrorValidationAA.v
View file @
ad80ecfc
...
...
@@ -22,93 +22,153 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
(
dVars
:
NatSet
.
t
)
(
*
let
-
bound
variables
encountered
previously
*
)
(
currNoise
:
nat
)
(
*
current
maximal
noise
term
*
)
(
errMap
:
FloverMap
.
t
(
affine_form
Q
))
(
*
previously
seen
affine
polys
*
)
:
option
(
FloverMap
.
t
(
affine_form
Q
)
*
nat
)
:=
olet
m
:=
FloverMap
.
find
e
typeMap
in
olet
dRes
:=
FloverMap
.
find
e
A
in
let
(
intv
,
err
)
:=
dRes
in
(
*
Error
bounds
are
intervals
symmetric
at
0
-->
the
bound
must
be
positive
here
*
)
if
(
negb
(
Qleb
0
err
))
then
None
else
(
*
We
have
already
checked
a
subexpression
*
)
if
(
FloverMap
.
mem
e
errMap
)
then
Some
(
errMap
,
currNoise
)
:
option
(
FloverMap
.
t
(
affine_form
Q
)
*
nat
)
:=
(
*
(
*
case
analysis
for
the
expression
*
)
*
)
(
*
if
(
FloverMap
.
mem
e
errMap
)
then
*
)
(
*
(
*
We
have
already
checked
a
subexpression
*
)
*
)
(
*
Some
(
errMap
,
currNoise
)
*
)
(
*
else
*
)
olet
m
:=
FloverMap
.
find
e
typeMap
in
olet
dRes
:=
FloverMap
.
find
e
A
in
let
(
intv
,
err
)
:=
dRes
in
(
*
Error
bounds
are
intervals
symmetric
at
0
-->
the
bound
must
be
positive
here
*
)
if
(
negb
(
Qleb
0
err
))
then
None
else
(
*
case
analysis
for
the
expression
*
)
match
e
with
|
Var
_
x
=>
match
e
with
|
Var
_
x
=>
if
(
NatSet
.
mem
x
dVars
)
then
Some
(
errMap
,
currNoise
)
(
*
previously
checked
defined
variable
*
)
else
(
*
Build
an
affine
polynomial
*
)
let
errNew
:=
computeErrorQ
(
maxAbs
intv
)
m
in
let
af
:=
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
currNoise
in
if
(
Qleb
errNew
err
)
then
Some
(
FloverMap
.
add
e
af
errMap
,
(
currNoise
+
1
)
%
nat
)
else
None
|
Expressions
.
Const
m
v
=>
(
*
Build
an
affine
polynomial
*
)
let
errNew
:=
computeErrorQ
(
maxAbs
intv
)
m
in
let
af
:=
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
currNoise
in
if
(
Qleb
errNew
err
)
then
Some
(
FloverMap
.
add
e
af
errMap
,
(
currNoise
+
1
)
%
nat
)
else
None
|
Expressions
.
Const
m
v
=>
let
errNew
:=
computeErrorQ
(
maxAbs
intv
)
m
in
let
af
:=
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
currNoise
in
if
(
Qleb
errNew
err
)
then
Some
(
FloverMap
.
add
(
elt
:=
affine_form
Q
)
e
af
errMap
,
(
currNoise
+
1
)
%
nat
)
else
None
|
Unop
Neg
e1
=>
|
Unop
Neg
e1
=>
olet
res
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap
,
maxNoise
)
:=
res
in
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap
in
match
FloverMap
.
find
e1
A
with
|
Some
(
iv_e1
,
err1
)
=>
if
(
Qeq_bool
err
err1
)
then
Some
(
FloverMap
.
add
e
afPolye1
newErrorMap
,
maxNoise
)
else
None
|
None
=>
None
end
|
Unop
Inv
e1
=>
None
|
Binop
b
e1
e2
=>
olet
res1
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
olet
res2
:=
validErrorboundAA
e2
typeMap
A
dVars
maxNoise1
newErrorMap1
in
let
(
newErrorMap2
,
maxNoise2
)
:=
res2
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap2
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye2
:=
FloverMap
.
find
e2
newErrorMap2
in
(
*
Analysis
results
for
e1
,
e2
*
)
match
FloverMap
.
find
e1
A
,
FloverMap
.
find
e2
A
with
|
None
,
_
=>
None
|
_
,
None
=>
None
|
Some
(
ive1
,
err1
),
Some
(
ive2
,
err2
)
=>
let
errIve1
:=
widenIntv
ive1
err1
in
let
errIve2
:=
widenIntv
ive2
err2
in
match
b
with
|
Plus
=>
let
actualRange
:=
(
addIntv
errIve1
errIve2
)
in
let
errNew
:=
computeErrorQ
(
maxAbs
actualRange
)
m
in
let
errPoly
:=
plus_aff
(
plus_aff
afPolye1
afPolye2
)
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
maxNoise2
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
1
)
%
nat
)
else
None
|
Sub
=>
let
mAbs
:=
(
maxAbs
(
subtractIntv
errIve1
errIve2
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
(
subtract_aff
afPolye1
afPolye2
)
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
maxNoise2
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
1
)
%
nat
)
let
(
newErrorMap
,
maxNoise
)
:=
res
in
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap
in
match
FloverMap
.
find
e1
A
with
|
Some
(
iv_e1
,
err1
)
=>
if
(
Qeq_bool
err
err1
)
then
Some
(
FloverMap
.
add
e
afPolye1
newErrorMap
,
maxNoise
)
else
None
|
Mult
=>
|
None
=>
None
end
|
Unop
Inv
e1
=>
None
|
Binop
b
e1
e2
=>
olet
res1
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
olet
res2
:=
validErrorboundAA
e2
typeMap
A
dVars
maxNoise1
newErrorMap1
in
let
(
newErrorMap2
,
maxNoise2
)
:=
res2
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap2
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye2
:=
FloverMap
.
find
e2
newErrorMap2
in
(
*
Analysis
results
for
e1
,
e2
*
)
match
FloverMap
.
find
e1
A
,
FloverMap
.
find
e2
A
with
|
None
,
_
=>
None
|
_
,
None
=>
None
|
Some
(
ive1
,
err1
),
Some
(
ive2
,
err2
)
=>
let
errIve1
:=
widenIntv
ive1
err1
in
let
errIve2
:=
widenIntv
ive2
err2
in
match
b
with
|
Plus
=>
let
actualRange
:=
(
addIntv
errIve1
errIve2
)
in
let
errNew
:=
computeErrorQ
(
maxAbs
actualRange
)
m
in
let
errPoly
:=
plus_aff
(
plus_aff
afPolye1
afPolye2
)
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
maxNoise2
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
1
)
%
nat
)
else
None
|
Sub
=>
let
mAbs
:=
(
maxAbs
(
subtractIntv
errIve1
errIve2
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
(
subtract_aff
afPolye1
afPolye2
)
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
maxNoise2
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
1
)
%
nat
)
else
None
|
Mult
=>
let
aaRangee1
:=
fromIntv
ive1
maxNoise2
in
let
aaRangee2
:=
fromIntv
ive2
(
maxNoise2
+
1
)
in
let
propError
:=
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
afPolye2
(
maxNoise2
+
2
))
(
mult_aff
aaRangee2
afPolye1
(
maxNoise2
+
3
)
))
(
mult_aff
afPolye1
afPolye2
(
maxNoise2
+
4
))
in
let
mAbs
:=
(
maxAbs
(
multIntv
errIve1
errIve2
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
propError
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
(
maxNoise2
+
5
))
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
6
)
%
nat
)
else
None
|
Div
=>
if
(((
Qleb
(
ivhi
errIve2
)
0
)
&&
(
negb
(
Qeq_bool
(
ivhi
errIve2
)
0
)))
||
((
Qleb
0
(
ivlo
errIve2
))
&&
(
negb
(
Qeq_bool
(
ivlo
errIve2
)
0
))))
then
let
aaRangee1
:=
fromIntv
ive1
maxNoise2
in
let
invertede2
:=
invertIntv
ive2
in
let
aaRangeInve2
:=
fromIntv
invertede2
(
maxNoise2
+
1
)
in
let
invertedErre2
:=
inverse_aff
afPolye2
(
maxNoise2
+
2
)
(
*
TODO
invert
*
)
in
let
propError
:=
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
invertedErre2
(
maxNoise2
+
3
))
(
mult_aff
aaRangeInve2
afPolye1
(
maxNoise2
+
4
)))
(
mult_aff
afPolye1
invertedErre2
(
maxNoise2
+
5
))
in
let
mAbs
:=
(
maxAbs
(
divideIntv
errIve1
errIve2
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
propError
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
(
maxNoise2
+
6
))
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
7
)
%
nat
)
else
None
else
None
end
end
|
Fma
e1
e2
e3
=>
olet
res1
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
olet
res2
:=
validErrorboundAA
e2
typeMap
A
dVars
maxNoise1
newErrorMap1
in
let
(
newErrorMap2
,
maxNoise2
)
:=
res2
in
olet
res3
:=
validErrorboundAA
e3
typeMap
A
dVars
maxNoise2
newErrorMap2
in
let
(
newErrorMap3
,
maxNoise3
)
:=
res3
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap3
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye2
:=
FloverMap
.
find
e2
newErrorMap3
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye3
:=
FloverMap
.
find
e3
newErrorMap3
in
match
FloverMap
.
find
e1
A
,
FloverMap
.
find
e2
A
,
FloverMap
.
find
e3
A
with
|
None
,
_
,
_
=>
None
|
_
,
None
,
_
=>
None
|
_
,
_
,
None
=>
None
|
Some
(
ive1
,
err1
),
Some
(
ive2
,
err2
),
Some
(
ive3
,
err3
)
=>
let
errIve1
:=
widenIntv
ive1
err1
in
let
errIve2
:=
widenIntv
ive2
err2
in
let
errIve3
:=
widenIntv
ive3
err3
in
let
aaRangee1
:=
fromIntv
ive1
maxNoise2
in
let
aaRangee2
:=
fromIntv
ive2
(
maxNoise2
+
1
)
in
let
propError
:=
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
afPolye2
(
maxNoise2
+
2
))
(
mult_aff
aaRangee2
afPolye1
(
maxNoise2
+
3
)
))
(
mult_aff
afPolye1
afPolye2
(
maxNoise2
+
4
))
in
let
mAbs
:=
(
maxAbs
(
multIntv
errIve1
errIve2
))
in
(
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
afPolye2
(
maxNoise2
+
2
))
(
mult_aff
aaRangee2
afPolye1
(
maxNoise2
+
3
)
))
(
mult_aff
afPolye1
afPolye2
(
maxNoise2
+
4
)))
afPolye3
in
let
mAbs
:=
(
maxAbs
(
addIntv
(
multIntv
errIve1
errIve2
)
errIve3
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
propError
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
(
maxNoise2
+
5
))
in
...
...
@@ -116,84 +176,24 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
6
)
%
nat
)
else
None
|
Div
=>
if
(((
Qleb
(
ivhi
errIve2
)
0
)
&&
(
negb
(
Qeq_bool
(
ivhi
errIve2
)
0
)))
||
((
Qleb
0
(
ivlo
errIve2
))
&&
(
negb
(
Qeq_bool
(
ivlo
errIve2
)
0
))))
then
let
aaRangee1
:=
fromIntv
ive1
maxNoise2
in
let
invertede2
:=
invertIntv
ive2
in
let
aaRangeInve2
:=
fromIntv
invertede2
(
maxNoise2
+
1
)
in
let
invertedErre2
:=
inverse_aff
afPolye2
(
maxNoise2
+
2
)
(
*
TODO
invert
*
)
in
let
propError
:=
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
invertedErre2
(
maxNoise2
+
3
))
(
mult_aff
aaRangeInve2
afPolye1
(
maxNoise2
+
4
)))
(
mult_aff
afPolye1
invertedErre2
(
maxNoise2
+
5
))
in
let
mAbs
:=
(
maxAbs
(
divideIntv
errIve1
errIve2
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
propError
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
(
maxNoise2
+
6
))
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap2
,
(
maxNoise2
+
7
)
%
nat
)
else
None
else
None
end
end
|
Fma
e1
e2
e3
=>
end
|
Downcast
m
e1
=>
olet
res1
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
olet
res2
:=
validErrorboundAA
e2
typeMap
A
dVars
maxNoise1
newErrorMap1
in
let
(
newErrorMap2
,
maxNoise2
)
:=
res2
in
olet
res3
:=
validErrorboundAA
e3
typeMap
A
dVars
maxNoise2
newErrorMap2
in
let
(
newErrorMap3
,
maxNoise3
)
:=
res3
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap3
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye2
:=
FloverMap
.
find
e2
newErrorMap3
in
(
*
Error
polynomial
for
e2
*
)
olet
afPolye3
:=
FloverMap
.
find
e3
newErrorMap3
in
match
FloverMap
.
find
e1
A
,
FloverMap
.
find
e2
A
,
FloverMap
.
find
e3
A
with
|
None
,
_
,
_
=>
None
|
_
,
None
,
_
=>
None
|
_
,
_
,
None
=>
None
|
Some
(
ive1
,
err1
),
Some
(
ive2
,
err2
),
Some
(
ive3
,
err3
)
=>
let
errIve1
:=
widenIntv
ive1
err1
in
let
errIve2
:=
widenIntv
ive2
err2
in
let
errIve3
:=
widenIntv
ive3
err3
in
let
aaRangee1
:=
fromIntv
ive1
maxNoise2
in
let
aaRangee2
:=
fromIntv
ive2
(
maxNoise2
+
1
)
in
let
propError
:=
plus_aff
(
plus_aff
(
plus_aff
(
mult_aff
aaRangee1
afPolye2
(
maxNoise2
+
2
))
(
mult_aff
aaRangee2
afPolye1
(
maxNoise2
+
3
)
))
(
mult_aff
afPolye1
afPolye2
(
maxNoise2
+
4
)))
afPolye3
in
let
mAbs
:=
(
maxAbs
(
addIntv
(
multIntv
errIve1
errIve2
)
errIve3
))
in
let
errNew
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
propError
(
fromIntv
(
mkIntv
(
-
errNew
)
errNew
)
(
maxNoise2
+
5
))
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap1
in
olet
aRes
:=
FloverMap
.
find
e1
A
in
let
(
ive1
,
err1
)
:=
aRes
in
let
errIve1
:=
widenIntv
ive1
err1
in
let
mAbs
:=
maxAbs
errIve1
in
let
newErr
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
afPolye1
(
fromIntv
(
mkIntv
(
-
newErr
)
newErr
)
maxNoise1
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap
2
,
(
maxNoise2
+
6
)
%
nat
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap
1
,
(
maxNoise1
+
1
)
%
nat
)
else
None
end
|
Downcast
m
e1
=>
olet
res1
:=
validErrorboundAA
e1
typeMap
A
dVars
currNoise
errMap
in
let
(
newErrorMap1
,
maxNoise1
)
:=
res1
in
(
*
Error
polynomial
for
e1
*
)
olet
afPolye1
:=
FloverMap
.
find
e1
newErrorMap1
in
olet
aRes
:=
FloverMap
.
find
e1
A
in
let
(
ive1
,
err1
)
:=
aRes
in
let
errIve1
:=
widenIntv
ive1
err1
in
let
mAbs
:=
maxAbs
errIve1
in
let
newErr
:=
computeErrorQ
mAbs
m
in
let
errPoly
:=
plus_aff
afPolye1
(
fromIntv
(
mkIntv
(
-
newErr
)
newErr
)
maxNoise1
)
in
let
errVal
:=
maxAbs
(
toIntv
errPoly
)
in
if
(
Qleb
errVal
err
)
then
Some
(
FloverMap
.
add
e
errPoly
newErrorMap1
,
(
maxNoise1
+
1
)
%
nat
)
else
None
end
.
end
.
(
**
Error
bound
command
validator
**
)
Fixpoint
validErrorboundAACmd
(
f
:
cmd
Q
)
(
*
analyzed
cmd
with
let
'
s
*
)
...
...
@@ -202,7 +202,7 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
(
dVars
:
NatSet
.
t
)
(
*
let
-
bound
variables
encountered
previously
*
)
(
currNoise
:
nat
)
(
*
current
maximal
noise
term
*
)
(
errMap
:
FloverMap
.
t
(
affine_form
Q
))
(
*
previously
seen
affine
polys
*
)
:
option
(
FloverMap
.
t
(
affine_form
Q
)
*
nat
)
:=
:
option
(
FloverMap
.
t
(
affine_form
Q
)
*
nat
)
:=
match
f
with
|
Let
m
x
e
g
=>
olet
res1
:=
validErrorboundAA
e
typeMap
A
dVars
currNoise
errMap
in
...
...
@@ -231,6 +231,8 @@ Fixpoint validErrorboundAACmd (f:cmd Q) (* analyzed cmd with let's *)
(
*
let
mAbs
:=
maxAbs
(
toIntv
af
)
in
*
)
(
*
(
Rabs
(
vR
-
vF
)
<=
(
Q2R
mAbs
))
%
R
.
*
)
(
*
Theorem
validErrorboundAA_sound
e
:
*
)
(
*
forall
E1
E2
P
Gamma
defVars
nR
A
elo
ehi
tMap
fVars
dVars
currNoise
maxNoise
initMap
resMap
M1
,
*
)
(
*
(
forall
e
vR
,
*
)
...
...
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