...
 
Commits (18)
......@@ -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.
......
......@@ -3074,8 +3074,8 @@ Proof.
- apply validErrorboundAA_sound_binop; auto.
- apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto.
- (*FIXME *)
Qed.
- admit.
Abort.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key,
......@@ -3200,7 +3200,12 @@ Proof.
end.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
<<<<<<< HEAD
- (* FIXME *)
=======
- admit.
Abort.
>>>>>>> master
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
......@@ -3817,4 +3822,4 @@ Proof.
cbn in H12.
now rewrite Rabs_Rle_condition.
Qed.
*)
\ No newline at end of file
*)
......@@ -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.
Subproject commit 78f69d7fcdd795890f213134d66582ece116e14b
Subproject commit 7acebe9f434d9882401f73a0d4a14e9e5e4844a8
......@@ -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
}
......@@ -2,21 +2,25 @@ Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :FloverMap.t mType :=
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
].
Definition absenv_additionSimple :analysisResult := Eval compute in
FloverMap.add e3 (( (1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Theorem ErrorBound_additionSimple_Sound :
CertificateCheckerCmd Rete3 absenv_additionSimple thePrecondition_additionSimple defVars_additionSimple = true.
Proof.
vm_compute; auto.
Qed.
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else (0#1,0#1).
Definition absenv_additionSimple :analysisResult := Eval compute in
FloverMap.add e3 (( (1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Theorem ErrorBound_additionSimple_Sound :
CertificateCheckerCmd Rete3 absenv_additionSimple thePrecondition_additionSimple defVars_additionSimple = true.
Proof.
vm_compute; auto.
Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple_sub0 :=
(FloverMap.add u0 ((-100)#(1), (-100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub1 :=
(FloverMap.add u0 ((-100)#(3), (100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub2 :=
(FloverMap.add u0 ((100)#(3), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition querymap_additionSimple_sub0 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub1 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub2 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition absenv_additionSimple_sub0: analysisResult :=
FloverMap.add e3 (((1157)#(5), (4471)#(15)), (19711354849075188187)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(1), (-100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub1: analysisResult :=
FloverMap.add e3 (((4471)#(15), (5471)#(15)), (21512794700023386587)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(3), (100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub2: analysisResult :=
FloverMap.add e3 (((5471)#(15), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((100)#(3), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
(thePrecondition_additionSimple_sub0, absenv_additionSimple_sub0, querymap_additionSimple_sub0);(thePrecondition_additionSimple_sub1, absenv_additionSimple_sub1, querymap_additionSimple_sub1);(thePrecondition_additionSimple_sub2, absenv_additionSimple_sub2, querymap_additionSimple_sub2)].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition u0 :expr Q := Var Q 0.
Definition e3 :expr Q := Binop Plus C12 u0.
Definition defVars_additionSimple: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType)).
Definition thePrecondition_additionSimple_sub0 :=
(FloverMap.add u0 ((-100)#(1), (-100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub1 :=
(FloverMap.add u0 ((-100)#(3), (100)#(3)) (FloverMap.empty intv),
TrueQ).
Definition thePrecondition_additionSimple_sub2 :=
(FloverMap.add u0 ((100)#(3), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition querymap_additionSimple_sub0 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub1 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition querymap_additionSimple_sub2 :=
FloverMap.empty (SMTLogic * SMTLogic).
Definition absenv_additionSimple_sub0: analysisResult :=
FloverMap.add e3 (((1157)#(5), (4471)#(15)), (19711354849075188187)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(1), (-100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub1: analysisResult :=
FloverMap.add e3 (((4471)#(15), (5471)#(15)), (21512794700023386587)#(243388915243820045087367015432192)) (FloverMap.add u0 (((-100)#(3), (100)#(3)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition absenv_additionSimple_sub2: analysisResult :=
FloverMap.add e3 (((5471)#(15), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((100)#(3), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition subdivs_additionSimple: list (precond * analysisResult * usedQueries) := [
(thePrecondition_additionSimple_sub0, absenv_additionSimple_sub0, querymap_additionSimple_sub0);(thePrecondition_additionSimple_sub1, absenv_additionSimple_sub1, querymap_additionSimple_sub1);(thePrecondition_additionSimple_sub2, absenv_additionSimple_sub2, querymap_additionSimple_sub2)].
Definition thePrecondition_additionSimple :=
(FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv),
TrueQ).
Definition absenv_additionSimple: analysisResult :=
FloverMap.add e3 (((1157)#(5), (2157)#(5)), (7771411516990528329)#(81129638414606681695789005144064)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add C12 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))).
Definition querymap_additionSimple :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_additionSimple_sound :
CertificateChecker e3 absenv_additionSimple thePrecondition_additionSimple querymap_additionSimple subdivs_additionSimple defVars_additionSimple= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition C34 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition e5 :expr Q := Binop Mult C34 T2.
Definition e6 :expr Q := Binop Plus C12 e5.
Definition CastM32e6 :expr Q := Downcast M32 e6.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e7 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e8 :expr Q := Binop Plus t15 u0.
Definition e9 :expr Q := Binop Mult e8 e8.
Definition e10 :expr Q := Binop Div e7 e9.
Definition Rete10 := Ret e10.
Definition Lett15CastM32e6Rete10 := Let M32 5 CastM32e6 Rete10.
Definition defVars_doppler :FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M32) (FloverMap.add (Var Q 5) (M32) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition thePrecondition_doppler:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else if n =? 1 then ( (20)#(1), (20000)#(1)) else if n =? 2 then ( (-30)#(1), (50)#(1)) else (0#1,0#1).
Definition absenv_doppler :analysisResult := Eval compute in
FloverMap.add (Var Q 5) (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840) ) (FloverMap.add e10 (( (-180700000)#(1138489), (-156700)#(5322249)), (3128798615377558964734587413815260935766775940003133188505004688351541231456980597512692494850911181122476079460422247077079176104347591604229243224768895229048954292495195716430601972291603510900358841802949847973326821449585470105361794370971246392326730165769086503662250520953800794720080442853388469377023727444437325832874114769965213547362197536886857310450874114551302656316164631446184855133337791662127325138346785397490340980930573694307935576641198224172023812349312175410753884375)#(32036808664321353711103483032138488273658359037549607658529725639211828966830820254532621633000657987120666498279218129796043154742555162761269493533793888535784577584907972014998498622632370186488026019213317308445273559994196553084922725810710211676061848042954653773443813684285036579995330627524678538042961243278389567362111169788921619483881120057899533645621131479344403647093086239019570741449266701692934633407390503406115529744843066088021266694728367150101865392734271463782370359902208)) (FloverMap.add e9 (( (1138489)#(25), (5322249)#(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)#(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)#(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)#(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e7 (( (-7228000)#(1), (-6268)#(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)#(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMap.add v1 (( (20)#(1), (20000)#(1)), (625)#(524288)) (FloverMap.add UMint15 (( (-1807)#(5), (-1567)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add CastM32e6 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e6 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e5 (( (-18)#(1), (30)#(1)), (3650833728657301081634471694827535)#(365375409332725729550921208179070754913983135744)) (FloverMap.add T2 (( (-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C34 (( (3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))))))))))))))))))).
Theorem ErrorBound_doppler_Sound :
CertificateCheckerCmd Lett15CastM32e6Rete10 absenv_doppler thePrecondition_doppler defVars_doppler = true.
Proof.
vm_compute; auto.
Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((1657)#(5)).
Definition C34 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition e5 :expr Q := Binop Mult C34 T2.
Definition e6 :expr Q := Binop Plus C12 e5.
Definition CastM32e6 :expr Q := Downcast M32 e6.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e7 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e8 :expr Q := Binop Plus t15 u0.
Definition e9 :expr Q := Binop Mult e8 e8.
Definition e10 :expr Q := Binop Div e7 e9.
Definition Rete10 := Ret e10.
Definition Lett15CastM32e6Rete10 := Let M32 5 CastM32e6 Rete10.
Definition defVars_doppler :FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M32) (FloverMap.add (Var Q 5) (M32) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition thePrecondition_doppler:precond := fun (n:nat) =>
if n =? 0 then ( (-100)#(1), (100)#(1)) else if n =? 1 then ( (20)#(1), (20000)#(1)) else if n =? 2 then ( (-30)#(1), (50)#(1)) else (0#1,0#1).
Definition absenv_doppler :analysisResult := Eval compute in
FloverMap.add (Var Q 5) (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840) ) (FloverMap.add e10 (( (-1697764138654329772000)#(3490644748218790563), (845148567992740137100)#(3490644748218790563)), (86789720644057150247866605447704701639542420366828894132198862668669714230796996017035083608214420357613914531567484222212219331055483511822890139010872023483027505740246147962523569787278664172305316497757644071254699998665282042562758048408625758851595888688321139287912787500084300448747342010732963228878699239161772886561738720968290627692004030895987294913860908138447593680198320054472132697520066221100165663039771347855801540617277134187668140137009343975368944377522556200084375)#(116581075971445025849972765325192688960688023193987481443423359259469524004578990495359777413108258534013101183101133893535361165723138789382125100532000290607255302844371142602120272808586051005748656571844135028373285214957706768877222323723316372017777470087619528348277265902992869293242456576370752686840418222478699145317598793362601803894470311876274014967799666442159459249464411902617752130127840333947718959260993021328099576810901846581180134891356519631659292569462696113720000512)) (FloverMap.add e9 (( (369689)#(25), (5322249)#(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)#(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)#(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)#(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e7 (( (-7228000)#(1), (473252)#(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)#(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMap.add v1 (( (20)#(1), (20000)#(1)), (625)#(524288)) (FloverMap.add UMint15 (( (-1807)#(5), (-1567)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add CastM32e6 (( (1567)#(5), (1807)#(5)), (5946853494151590254223768460713179402300517371078900237055784124491)#(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMap.add e6 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e5 (( (-18)#(1), (30)#(1)), (3650833728657301081634471694827535)#(365375409332725729550921208179070754913983135744)) (FloverMap.add T2 (( (-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C34 (( (3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.empty (intv * error)))))))))))))))))))).
Theorem ErrorBound_doppler_Sound :
CertificateCheckerCmd Lett15CastM32e6Rete10 absenv_doppler thePrecondition_doppler defVars_doppler = true.
Proof.
vm_compute; auto.
Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition C34 :expr Q := Const M64 ((1657)#(5)).
Definition FMA5mult :expr Q := Binop Mult C12 T2.
Definition FMA5 :expr Q := Fma C12 T2 C34.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e6 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e7 :expr Q := Binop Plus t15 u0.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition e9 :expr Q := Binop Div e6 e8.
Definition Let10 := Let M64 5 FMA5 e9.
Definition defVars_doppler: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition subdivs_doppler: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_doppler :=
(FloverMap.add T2 ((-30)#(1), (50)#(1)) (FloverMap.add v1 ((20)#(1), (20000)#(1)) (FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv))),
(AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ)).
Definition absenv_doppler: analysisResult :=
FloverMap.add Let10 (((-180700000)#(1138489), (-156700)#(5322249)), (6830474556051150717276799761411546903312647039023687172223811352204070680260786237572370408687560441727006035326226907571046644765565610826295450225945821689766113946084926436173485860032840000964523515885271737730095253157325021312893152796246718141576145498964466082789239458535219584103497743580035241118781706960333496399469040697857641019083062655105934801391066722947827783153125)#(10652421913510213733898407083420012913520344863420275587860254841070206042654275053211239601233990813544801557039628247004768110951082434032072365979905419580587655195775106519963774511263809230729529345878113187715691336518180342419923881592311850124427434616938294137618896157525426696073050860327859392612474295413649439400913925656013708636956880301351141496628302550147680567001131206431473664)) (FloverMap.add e9 (((-180700000)#(1138489), (-156700)#(5322249)), (6830474556051150717276799761411546903312647039023687172223811352204070680260786237572370408687560441727006035326226907571046644765565610826295450225945821689766113946084926436173485860032840000964523515885271737730095253157325021312893152796246718141576145498964466082789239458535219584103497743580035241118781706960333496399469040697857641019083062655105934801391066722947827783153125)#(10652421913510213733898407083420012913520344863420275587860254841070206042654275053211239601233990813544801557039628247004768110951082434032072365979905419580587655195775106519963774511263809230729529345878113187715691336518180342419923881592311850124427434616938294137618896157525426696073050860327859392612474295413649439400913925656013708636956880301351141496628302550147680567001131206431473664)) (FloverMap.add e8 (((1138489)#(25), (5322249)#(25)), (386016739293039129357381964239803461348537618308829254644034741686921309846763562236550650398450203284331927422628136288220741271295481)#(2438866054934368930766872835775911176366092298957008711608716374707321670952941890718989143018353102468614789938598924137068730999443972895539200)) (FloverMap.add e7 (((1067)#(5), (2307)#(5)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e7 (((1067)#(5), (2307)#(5)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e6 (((-7228000)#(1), (-6268)#(1)), (3035133155978965067333019855358048910502028922472741755023387525129375)#(926336713898529563388567880069503262826159877325124512315660672063305037119488)) (FloverMap.add v1 (((20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMint15 (((-1807)#(5), (-1567)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add FMA5 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add C34 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add T2 (((-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C12 (((3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.empty (intv * error))))))))))))))))))).
Definition querymap_doppler :=
FloverMap.empty (SMTLogic * SMTLogic).
Theorem ErrorBound_doppler_sound :
CertificateChecker Let10 absenv_doppler thePrecondition_doppler querymap_doppler subdivs_doppler defVars_doppler= true.
Proof. vm_compute; auto. Qed.
Require Import Flover.CertificateChecker.
Definition C12 :expr Q := Const M64 ((3)#(5)).
Definition T2 :expr Q := Var Q 2.
Definition C34 :expr Q := Const M64 ((1657)#(5)).
Definition FMA5mult :expr Q := Binop Mult C12 T2.
Definition FMA5 :expr Q := Fma C12 T2 C34.
Definition t15 :expr Q := Var Q 5.
Definition UMint15 :expr Q := Unop Neg t15.
Definition v1 :expr Q := Var Q 1.
Definition e6 :expr Q := Binop Mult UMint15 v1.
Definition u0 :expr Q := Var Q 0.
Definition e7 :expr Q := Binop Plus t15 u0.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition e9 :expr Q := Binop Div e6 e8.
Definition Let10 := Let M64 5 FMA5 e9.
Definition defVars_doppler: FloverMap.t mType :=
(FloverMap.add (Var Q 0) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 2) (M64) (FloverMap.empty mType))))).
Definition subdivs_doppler: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_doppler :=
(FloverMap.add T2 ((-30)#(1), (50)#(1)) (FloverMap.add v1 ((20)#(1), (20000)#(1)) (FloverMap.add u0 ((-100)#(1), (100)#(1)) (FloverMap.empty intv))),
(AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ)).
Definition absenv_doppler: analysisResult :=
FloverMap.add Let10 (((-9223372036854775323)#(67009023665787196), (-5384171002265600)#(159863851257405257)), (6395146761044357765503690801371276441765368447015101151813296635119433028390557896565475544956496553833459191531639848229164847988961573864464670748776813353525138213843738842546201283089853904954629246749165169810621322980144875026220656880567564902052374804615727126723160410736986845127244991996621049078998530821579057621625396893839494221224899982880254084100240465023731783153125)#(10652421913510219219409264963744548661917487941121320395994513318430551904512362747199924221778332168092965488723607243456011259465287188475318845213631543374252546820055908805724854791821012630200619036164098945114325414650541776464238357256998182652973892059080760766652998114554695566408635758783296967862860271493631237713524640412280353981040909615148658257257365203796839224604304840970993664)) (FloverMap.add e9 (((-9223372036854775323)#(67009023665787196), (-5384171002265600)#(159863851257405257)), (6395146761044357765503690801371276441765368447015101151813296635119433028390557896565475544956496553833459191531639848229164847988961573864464670748776813353525138213843738842546201283089853904954629246749165169810621322980144875026220656880567564902052374804615727126723160410736986845127244991996621049078998530821579057621625396893839494221224899982880254084100240465023731783153125)#(10652421913510219219409264963744548661917487941121320395994513318430551904512362747199924221778332168092965488723607243456011259465287188475318845213631543374252546820055908805724854791821012630200619036164098945114325414650541776464238357256998182652973892059080760766652998114554695566408635758783296967862860271493631237713524640412280353981040909615148658257257365203796839224604304840970993664)) (FloverMap.add e8 (((1138489)#(25), (159863851257405257)#(858993459200)), (357420066689505453360604417031945985271053151583235238178647155606033671479078134881359541739295517978633657744644427266878325030655481)#(2438866054934368930766872835775911176366092298957008711608716374707321670952941890718989143018353102468614789938598924137068730999443972895539200)) (FloverMap.add e7 (((1067)#(5), (8835207)#(20480)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e7 (((1067)#(5), (8835207)#(20480)), (2400881814725341027317566428674268637100018046599243)#(16455045573212060421549691825573505049827358656335798633486090240)) (FloverMap.add u0 (((-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add e6 (((-7228000)#(1), (-6268)#(1)), (3035133155978965067333019855358048910502028922472741755023387525129375)#(926336713898529563388567880069503262826159877325124512315660672063305037119488)) (FloverMap.add v1 (((20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMint15 (((-1807)#(5), (-1567)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add t15 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add FMA5 (((1567)#(5), (1807)#(5)), (30537195899257956888111864510152719)#(365375409332725729550921208179070754913983135744)) (FloverMap.add C34 (((1657)#(5), (1657)#(5)), (1657)#(45035996273704960)) (FloverMap.add T2 (((-30)#(1), (50)#(1)), (25)#(4503599627370496)) (FloverMap.add C12 (((3)#(5), (3)#(5)), (3)#(45035996273704960)) (FloverMap.empty (intv * error))))))))))))))))))).
Definition querymap_doppler :=
FloverMap.add Let10 ((AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5))))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) (ConstQ ((-9223372036854775323)#(67009023665787196)))) TrueQ)), FalseQ) (FloverMap.add e9 ((AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (DivQ (TimesQ (UMinusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5))))) (VarQ 1)) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) (ConstQ ((-9223372036854775323)#(67009023665787196)))) TrueQ)), FalseQ) (FloverMap.add e8 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((159863851257405257)#(858993459200))) (TimesQ (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0)))) TrueQ))) (FloverMap.add e7 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((8835207)#(20480))) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0))) TrueQ))) (FloverMap.add e7 (FalseQ, (AndQ (AndQ (LessEqQ (ConstQ ((-100)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((100)#(1)))) (AndQ (LessEqQ (ConstQ ((20)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((20000)#(1)))) (AndQ (LessEqQ (ConstQ ((-30)#(1))) (VarQ 2)) (AndQ (LessEqQ (VarQ 2) (ConstQ ((50)#(1)))) (AndQ (LessEqQ (PlusQ (VarQ 0) (VarQ 2)) (ConstQ ((100)#(1)))) TrueQ))))))) (AndQ (LessQ (ConstQ ((8835207)#(20480))) (PlusQ (PlusQ (TimesQ (ConstQ ((3)#(5))) (VarQ 2)) (ConstQ ((1657)#(5)))) (VarQ 0))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)))))).
Theorem ErrorBound_doppler_sound :
CertificateChecker Let10 absenv_doppler thePrecondition_doppler querymap_doppler subdivs_doppler defVars_doppler= true.
Proof. vm_compute; auto. Qed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This source diff could not be displayed because it is too large. You can view the blob instead.
Require Import Flover.CertificateChecker.
Definition x10 :expr Q := Var Q 0.
Definition e1 :expr Q := Binop Mult x10 x10.
Definition x21 :expr Q := Var Q 1.
Definition e2 :expr Q := Binop Plus e1 x21.
Definition t14 :expr Q := Var Q 4.
Definition e3 :expr Q := Binop Mult x21 x21.
Definition e4 :expr Q := Binop Plus x10 e3.
Definition CastM32e4 :expr Q := Downcast M32 e4.
Definition t25 :expr Q := Var Q 5.
Definition C56 :expr Q := Const M64 ((11)#(1)).
Definition e7 :expr Q := Binop Sub t14 C56.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition C910 :expr Q := Const M64 ((7)#(1)).
Definition e11 :expr Q := Binop Sub t25 C910.
Definition e12 :expr Q := Binop Mult e11 e11.
Definition e13 :expr Q := Binop Plus e8 e12.
Definition Rete13 := Ret e13.
Definition Lett25CastM32e4Rete13 := Let M32 5 CastM32e4 Rete13.
Definition Lett14e2Lett25CastM32e4Rete13 := Let M64 4 e2 Lett25CastM32e4Rete13.
Definition defVars_himmilbeau :FloverMap.t mType :=
(FloverMap.add (Var Q 5) (M32) (FloverMap.add (Var Q 4) (M64) (FloverMap.add (Var Q 1) (M32) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))))).
Definition thePrecondition_himmilbeau:precond := fun (n:nat) =>
if n =? 0 then ( (-5)#(1), (5)#(1)) else if n =? 1 then ( (-5)#(1), (5)#(1)) else (0#1,0#1).
Definition absenv_himmilbeau :analysisResult := Eval compute in
FloverMap.add (Var Q 4) (( (-30)#(1), (30)#(1)), (1961594369037173916351814399292228280199748452939370332185)#(6582018229284824168619876730229402019930943462534319453394436096) ) (FloverMap.add (Var Q 5) (( (-30)#(1), (30)#(1)), (4466206448905498720458189731062635560985)#(713623846352979940529142984724747568191373312) ) (FloverMap.add e13 (( (-2710)#(1), (3050)#(1)), (139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425)#(285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736)) (FloverMap.add e12 (( (-1271)#(1), (1369)#(1)), (172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009)#(372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872)) (FloverMap.add e11 (( (-37)#(1), (23)#(1)), (40228011429500474146133911235065735963306515172659036185)#(6427752177035961102167848369364650410088811975131171341205504)) (FloverMap.add C910 (( (7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (( (-30)#(1), (30)#(1)), (4466206448905498720458189731062635560985)#(713623846352979940529142984724747568191373312)) (FloverMap.add e11 (( (-37)#(1), (23)#(1)), (40228011429500474146133911235065735963306515172659036185)#(6427752177035961102167848369364650410088811975131171341205504)) (FloverMap.add C910 (( (7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (( (-30)#(1), (30)#(1)), (4466206448905498720458189731062635560985)#(713623846352979940529142984724747568191373312)) (FloverMap.add e8 (( (-1439)#(1), (1681)#(1)), (773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e7 (( (-41)#(1), (19)#(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (( (11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (( (-30)#(1), (30)#(1)), (1961594369037173916351814399292228280199748452939370332185)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e7 (( (-41)#(1), (19)#(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (( (11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (( (-30)#(1), (30)#(1)), (1961594369037173916351814399292228280199748452939370332185)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add CastM32e4 (( (-30)#(1), (30)#(1)), (4466206448905498720458189731062635560985)#(713623846352979940529142984724747568191373312)) (FloverMap.add e4 (( (-30)#(1), (30)#(1)), (190147601533197042302697458892825)#(42535295865117307932921825928971026432)) (FloverMap.add e3 (( (-25)#(1), (25)#(1)), (21110624511590425)#(4722366482869645213696)) (FloverMap.add x21 (( (-5)#(1), (5)#(1)), (5)#(16777216)) (FloverMap.add x21 (( (-5)#(1), (5)#(1)), (5)#(16777216)) (FloverMap.add x10 (( (-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add e2 (( (-30)#(1), (30)#(1)), (1961594369037173916351814399292228280199748452939370332185)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add x21 (( (-5)#(1), (5)#(1)), (5)#(16777216)) (FloverMap.add e1 (( (-25)#(1), (25)#(1)), (6084722881095501802724119491379225)#(730750818665451459101842416358141509827966271488)) (FloverMap.add x10 (( (-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x10 (( (-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.empty (intv * error))))))))))))))))))))))))))))).
Theorem ErrorBound_himmilbeau_Sound :
CertificateCheckerCmd Lett14e2Lett25CastM32e4Rete13 absenv_himmilbeau thePrecondition_himmilbeau defVars_himmilbeau = true.
Proof.
vm_compute; auto.
Qed.
Require Import Flover.CertificateChecker.
Definition x10 :expr Q := Var Q 0.
Definition e1 :expr Q := Binop Mult x10 x10.
Definition x21 :expr Q := Var Q 1.
Definition e2 :expr Q := Binop Plus e1 x21.
Definition t14 :expr Q := Var Q 4.
Definition e3 :expr Q := Binop Mult x21 x21.
Definition e4 :expr Q := Binop Plus x10 e3.
Definition t25 :expr Q := Var Q 5.
Definition C56 :expr Q := Const M64 ((11)#(1)).
Definition e7 :expr Q := Binop Sub t14 C56.
Definition e8 :expr Q := Binop Mult e7 e7.
Definition C910 :expr Q := Const M64 ((7)#(1)).
Definition e11 :expr Q := Binop Sub t25 C910.
Definition e12 :expr Q := Binop Mult e11 e11.
Definition e13 :expr Q := Binop Plus e8 e12.
Definition Let14 := Let M64 5 e4 e13.
Definition Let15 := Let M64 4 e2 Let14.
Definition defVars_himmilbeau: FloverMap.t mType :=
(FloverMap.add (Var Q 5) (M64) (FloverMap.add (Var Q 4) (M64) (FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))))).
Definition subdivs_himmilbeau: list (precond * analysisResult * usedQueries) := [
].
Definition thePrecondition_himmilbeau :=
(FloverMap.add x21 ((-5)#(1), (5)#(1)) (FloverMap.add x10 ((-5)#(1), (5)#(1)) (FloverMap.empty intv)),
TrueQ).
Definition absenv_himmilbeau: analysisResult :=
FloverMap.add Let15 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add Let14 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add e13 (((-2539445)#(1073741824), (890)#(1)), (214326632700533617242861152656345650019577498247133528214421121374194110240108056161295111503685251789492904723213079331326398813638014683212103657629022558066392458762474278093425)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add e12 (((-391)#(65536), (529)#(1)), (24494476745446527224805203707196455287788610482184994605367511523865495355084763447144119690867611178754214656532304097974615641183339850168336901755850382009959025)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e11 (((-12)#(1), (23)#(1)), (921482552099875582371005419234933846549265058874253722785201258521)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (((7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e11 (((-12)#(1), (23)#(1)), (921482552099875582371005419234933846549265058874253722785201258521)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (((7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e8 (((-209)#(65536), (361)#(1)), (19967444739687434637754919059652361566527336890697100496795325241802486801511301449055543161938200539717368949324161383771403052570803743760393603174179185581097585)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e7 (((-16)#(1), (19)#(1)), (921482552099875585294008693896739682956634724306819762097066344473)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (((11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e7 (((-16)#(1), (19)#(1)), (921482552099875585294008693896739682956634724306819762097066344473)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (((11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add t25 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e4 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e3 (((0)#(1), (25)#(1)), (6084722881095501802724119491379225)#(730750818665451459101842416358141509827966271488)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add t14 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e2 (((-5)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add x21 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add e1 (((0)#(1), (25)#(1)), (6084722881095501802724119491379225)#(730750818665451459101842416358141509827966271488)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.add x10 (((-5)#(1), (5)#(1)), (5)#(9007199254740992)) (FloverMap.empty (intv * error)))))))))))))))))))))))))))))).
Definition querymap_himmilbeau :=
FloverMap.add Let15 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add Let14 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add e13 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (PlusQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))))) (ConstQ ((-2539445)#(1073741824)))) TrueQ)), FalseQ) (FloverMap.add e12 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1)))) (MinusQ (PlusQ (VarQ 0) (TimesQ (VarQ 1) (VarQ 1))) (ConstQ ((7)#(1))))) (ConstQ ((-391)#(65536)))) TrueQ)), FalseQ) (FloverMap.add e8 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1)))) (MinusQ (PlusQ (TimesQ (VarQ 0) (VarQ 0)) (VarQ 1)) (ConstQ ((11)#(1))))) (ConstQ ((-209)#(65536)))) TrueQ)), FalseQ) (FloverMap.add e3 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (VarQ 1) (VarQ 1)) (ConstQ ((0)#(1)))) TrueQ)), FalseQ) (FloverMap.add e1 ((AndQ (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 0)) (AndQ (LessEqQ (VarQ 0) (ConstQ ((5)#(1)))) (AndQ (LessEqQ (ConstQ ((-5)#(1))) (VarQ 1)) (AndQ (LessEqQ (VarQ 1) (ConstQ ((5)#(1)))) TrueQ)))) (AndQ (LessQ (TimesQ (VarQ 0) (VarQ 0)) (ConstQ ((0)#(1)))) TrueQ)), FalseQ) (FloverMap.empty (SMTLogic * SMTLogic)))))))).
Theorem ErrorBound_himmilbeau_sound :
CertificateChecker Let15 absenv_himmilbeau thePrecondition_himmilbeau querymap_himmilbeau subdivs_himmilbeau defVars_himmilbeau= true.
Proof. vm_compute; auto. Qed.
This diff is collapsed.
This diff is collapsed.