Commit b9576264 authored by Joachim Bard's avatar Joachim Bard

removing old CI testcases

parent fa8496dd
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 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 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.
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