Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
AVA
FloVer
Commits
c40f3832
Commit
c40f3832
authored
Apr 11, 2019
by
Heiko Becker
Browse files
Merge branch 'master' into SMT_Subdiv
parents
9bd48857
babc1c42
Changes
2
Hide whitespace changes
Inline
Side-by-side
README.md
View file @
c40f3832
...
...
@@ -25,15 +25,14 @@ or
```
bash
$
./daisy file
--certificate
=
hol4
```
or for
one of the
binar
ies
or for
the HOL4
binar
y
```
bash
$
./daisy file
--certificate
=
binary
```
The certificate will be generated in the output folder of Daisy.
To make sure that the certificate can be validated in the logics, please use
`--errorMethod=interval`
and either
`--rangeMethod=interval`
or
`--rangeMethod=affine`
.
Unfortunately, affine polynomials are currently only supported on the branch
`affine_arithmetic`
.
Full support for fixed-point programs is also only available in
`affine_arithmetic`
.
The support for affine arithmetic is implemented in the branch
[
FMCAD2018
][
1
]
and is currently disabled on master.
## Checking Coq certificates
...
...
@@ -62,8 +61,6 @@ $ coqc -R ./ Flover output/CERTIFICATE_FILE.v
```
where
`./`
is FloVer's
`coq`
folder.
The generated binary can be run with
`coq_checker_native CERTIFICATE_FILE`
.
## Checking HOL4 certificates
As only some versions of HOL4 are known to compile with CakeML, we provide a
...
...
coq/SubdivsChecker.v
View file @
c40f3832
...
...
@@ -610,7 +610,12 @@ Definition checkPreconds (subdivs: list precond) (P: precond) :=
let
Piv
:=
FloverMap
.
elements
(
fst
P
)
in
let
Ps
:=
map
(
fun
P
=>
FloverMap
.
elements
(
fst
P
))
subdivs
in
let
S_qs
:=
map
snd
subdivs
in
covers
Piv
(
sort
Ps
)
&&
forallbTailrec
(
fun
q
=>
SMTLogic_eqb
q
(
snd
P
))
S_qs
.
(
*
Check
that
join
of
the
preconditions
for
the
subdivisions
covers
the
global
precondition
*
)
covers
Piv
(
sort
Ps
)
&&
(
*
Check
that
additional
constraints
encoded
by
Daisy
agree
for
each
subdivision
*
)
forallbTailrec
(
fun
q
=>
SMTLogic_eqb
q
(
snd
P
))
S_qs
.
Lemma
checkPreconds_sound
(
subdivs
:
list
precond
)
E
P
:
checkPreconds
subdivs
P
=
true
->
...
...
@@ -703,7 +708,7 @@ Proof.
{
apply
unsat_qs
.
apply
in_map_iff
.
now
exists
(
P1
,
A
,
Qmap
).
}
repeat
split
;
eauto
using
resultLeq_range_sound
,
resultLeq_error_sound
.
Qed
.
(
*
exists
Gamma
;
intros
approxE1E2
.
assert
(
approxEnv
E1
(
toRExpMap
Gamma
)
A
(
freeVars
e
)
NatSet
.
empty
E2
)
as
approxE1E2
'
...
...
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