Commit 2b3c798d authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'master'

Final proofs for SubdivChecker

See merge request AVA/FloVer!20
parents a40d99f5 316bad71
......@@ -67,14 +67,15 @@ Proof.
intros. cbn in *; congruence. }
exists Gamma; intros approxEnv_E1E2.
destruct subdivs.
- edestruct result_checking_sound; eauto.
intuition.
- edestruct result_checking_sound as ((outVars & Hssa) & validR & validErr & validFPR); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single; eauto.
destruct H5 as (? & ? & ?).
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & ?); eauto.
repeat eexists; eauto.
- (* general version of subdivs_checking_sound *) admit.
Admitted.
- edestruct subdivs_checking_sound as ((outVars & Hssa) & validR & validErr & validFPR); eauto.
edestruct validRanges_single as (iv_e & err_e & vR & find_e & eval_real_e & ?); eauto.
edestruct validErrorBoundsRec_single as ((vFP & mFP & eval_fp_e) & ?); eauto.
repeat eexists; eauto.
Qed.
(**
Soundness proof for the certificate checker.
......
......@@ -26,11 +26,10 @@ Theorem result_checking_sound (e: expr Q) (absenv: analysisResult) P Qmap defVar
unsat_queries Qmap ->
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma ->
ResultChecker e absenv P Qmap defVars Gamma = true ->
exists outVars,
ssa e (freeVars e) outVars /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(exists outVars, ssa e (freeVars e) outVars) /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma DeltaMap.
(**
The proofs is a simple composition of the soundness proofs for the range
validator and the error bound validator.
......@@ -56,7 +55,7 @@ Proof.
assert (NatSet.Subset (freeVars e -- NatSet.empty) (freeVars e)).
{ hnf; intros a in_empty.
set_tac. }
rename R into validFPRanges.
rename R into validFPR.
rename R0 into validRoundoffErr.
pose proof (validSSA_checks_freeVars _ _ L) as sub.
destruct (validSSA_sound e (preVars P)) as [outVars ssa_e]; auto.
......@@ -108,7 +107,7 @@ Corollary result_checking_sound_single (e: expr Q) (absenv: analysisResult) P Qm
Proof.
intros * deltas_matched P_valid unsat_qs valid_typeMap results_valid.
exists Gamma; intros approxE1E2.
edestruct result_checking_sound as (? & _ & validRange & Hsound & _); try eauto.
edestruct result_checking_sound as (_ & validRange & Hsound & _); try eauto.
eapply validRanges_single in validRange.
destruct validRange as [iv [err [vR [Hfind [eval_real validRange]]]]].
eapply validErrorBoundsRec_single in Hsound; eauto.
......
This diff is collapsed.
......@@ -462,4 +462,4 @@ Proof.
intros Hssa Hsub Hnotin Heval.
eapply eval_expr_det_ignore_bind2; [eauto |].
edestruct ssa_inv_let; eauto.
Qed
Qed.
......@@ -11,8 +11,19 @@
# #
##############################################################################
TIMECMD=""
PROVERS=(coq hol4 binary)
unameOut="$(uname -s)"
case "${unameOut}" in
Linux*) TIMECMD=/usr/bin/time;;
Darwin*) TIMECMD=/usr/local/bin/time;;
# CYGWIN*) machine=Cygwin;;
# MINGW*) machine=MinGw;;
# *) machine="UNKNOWN:${unameOut}"
esac
#PROVERS=(coq hol4 binary)
PROVERS=(coq)
arr=()
while IFS= read -r -d $'\0'; do
......@@ -24,10 +35,13 @@ DATE=`date +%H%M%d%m%y`
mkdir /tmp/artifact_fixed_$DATE
echo "Creating HOL4 heap for evaluation" >>$2
cd ./hol4/output/
Holmake heap >>$2
cd ../../
#echo "Creating HOL4 heap for evaluation" >>$2
#cd ./hol4/output/
#Holmake heap >>$2
#cd ../../
#echo "Daisy Coq, Daisy HOL4, Daisy Binary, Coq1, Coq2, Coq3, HOL4_1, HOL4_2, HOL4_3, CakeML1, CakeML2, CakeML3, Coqbin1, Coqbin2, Coqbin3" >>$1
echo "Daisy Coq, Coq1, Coq2, Coq3" >>$1
for file in "${arr[@]}"
do
......@@ -43,10 +57,13 @@ do
cd ./daisy
for prv in "${PROVERS[@]}"
do
RESULT=$( { /usr/bin/time -f ", %e" \
RESULT=$( { $TIMECMD -f ", %e" \
./daisy $FILEPATH --certificate=$prv \
--precision=Fixed32 \
--rangeMethod=smt \
--errorMethod=interval \
--divLimit=5 \
--totalOpt=150 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
......@@ -59,80 +76,81 @@ do
#run coq checker 3 times
echo "Working on Coq $CERTNAME" >>$2
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
rm ./daisy/output/$CERTNAME.vo
rm ./daisy/output/$CERTNAME.glob
RESULT=$( { /usr/bin/time -f ", %e" coqc -R ./coq Flover \
RESULT=$( { $TIMECMD -f ", %e" coqc -R ./coq Flover \
./daisy/output/$CERTNAME.v; } 2>&1)
echo -n $RESULT >>$1
#run HOL4 checker 3 times
cp ./daisy/output/*Script.sml ./hol4/output/
cd ./hol4/output/
echo "Working on $CERTNAME Theory.sig" >>$2
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
rm ./certificate_*Theory*
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
rm ./certificate_*Theory*
RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
RESULT=${RESULT#*M1}
RESULT=${RESULT%%M2*}
echo -n $RESULT >>$1
cd ../../
#run HOL4 binary 3 times
echo "Working on CakeML $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
# #run Coq binary 3 times
echo "Working on Coq binary $CERTNAME"
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo -n $RESULT >>$1
RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
./daisy/output/certificate_*".txt" >>$2; } 2>&1)
echo $RESULT >>$1
# #run HOL4 checker 3 times
# cp ./daisy/output/*Script.sml ./hol4/output/
# cd ./hol4/output/
# echo "Working on $CERTNAME Theory.sig" >>$2
# RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# rm ./certificate_*Theory*
#
# RESULT=$( { /usr/bin/time -f "M1, %e M2" Holmake $CERTNAME"Theory.sig"; } 2>&1)
# RESULT=${RESULT#*M1}
# RESULT=${RESULT%%M2*}
# echo -n $RESULT >>$1
#
# cd ../../
#
# #run HOL4 binary 3 times
# echo "Working on CakeML $CERTNAME"
# RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" hol4/binary/cake_checker \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
# echo -n $RESULT >>$1
#
# # #run Coq binary 3 times
# echo "Working on Coq binary $CERTNAME"
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo -n $RESULT >>$1
#
# RESULT=$( { /usr/bin/time -f ", %e" coq/binary/coq_checker_native \
# ./daisy/output/certificate_*".txt" >>$2; } 2>&1)
#
# echo $RESULT >>$1
echo "" >>$1
mv ./daisy/output/certificate_* /tmp/artifact_fixed_$DATE/
done
......@@ -65,8 +65,8 @@ do
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--divLimit=3 \
--totalOpt=100 \
--divLimit=5 \
--totalOpt=150 \
--results-csv=$FILENAME.csv \
>>$2 \
; } 2>&1 )
......@@ -81,8 +81,8 @@ do
--rangeMethod=smt \
--errorMethod=interval \
--subdiv \
--divLimit=3 \
--totalOpt=100 \
--divLimit=5 \
--totalOpt=150 \
--mixed-precision=testcases/daisy-mixed-precision-maps/$PMAP \
--results-csv=$FILENAME.csv \
>>$2 \
......
......@@ -23,11 +23,11 @@ object Science {
def carbonGas(T: Real, a: Real, b: Real, N: Real, p: Real, V: Real): Real = {
require(T >= 300 && T <= 300 && a >= 0.401 && a <= 0.401 && b >= 42.7e-6 && b <= 42.7e-6 && N >= 1000 && N <= 1000 &&
p >= 3.5e7 && p <= 3.5e7 && 0.1 < V && V < 0.5)
p >= 3.5e7 && p <= 3.5e7 && 0.1 <= V && V <= 0.5 && 0.1 < V && V < 0.5)
val k: Real = 1.3806503e-23
(p + a * (N / V) * (N / V)) * (V - N * b) - k * N * T
}
}
\ No newline at end of file
}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment