Commit 56ad16c8 authored by Heiko Becker's avatar Heiko Becker

Merge branch 'master' into 'master'

Cleanup for submission

See merge request AVA/FloVer!21
parents 2b3c798d b9576264
......@@ -3074,7 +3074,7 @@ Proof.
- apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto.
- admit.
Admitted.
Abort.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key,
......@@ -3200,7 +3200,7 @@ Proof.
cbn in Hiv.
now rewrite Rabs_Rle_condition.
- admit.
Admitted.
Abort.
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
......@@ -3817,4 +3817,4 @@ Proof.
cbn in H12.
now rewrite Rabs_Rle_condition.
Qed.
*)
\ 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.
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