fast-forward Daisy to latest state, readd regression test script and recompute...

fast-forward Daisy to latest state, readd regression test script and recompute regression tests as the certificate format has changed

.gitlab-ci.yml

@@ -5,7 +5,7 @@ variables:
 
 stages:
   - compile
-#  - regression
+  - regression
 
 cache:
   paths:
@@ -25,6 +25,6 @@ compile-hol:
      paths:
      - hol4/
 
-# regression-tests:
-#  stage: regression
-#  script: ./scripts/regressiontests.sh
\ No newline at end of file
+regression-tests:
+  stage: regression
+  script: ./scripts/regressiontests.sh

daisy @ 78f69d7f

-Subproject commit 8d4ad679922d52ac23b903fc4506eb7c10312dab
+Subproject commit 78f69d7fcdd795890f213134d66582ece116e14b

scripts/ci-hol4.sh

@@ -21,7 +21,6 @@ then
 else
     cd ./HOL4
     export HOLDIR="$(pwd)"
-    cd $HOLDIR
     git pull
     CURRHOL="$(git rev-parse HEAD)"
     if [[ "$CURRHOL" != "$HOLCOMMIT" ]];

testcases/regression/certificate_AdditionSimple.txt

@@ -3,6 +3,7 @@ Ret + 1657#5 MTYPE 64  Var 0
 
 GAMMA Var 0 MTYPE 64 
 
+
  PRE ? Var 0 ~100#1 100#1 
 
 ABS ? + 1657#5 MTYPE 64  Var 0 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 MTYPE 64  1657#5 1657#5 1657#45035996273704960 ? Var 0 ~100#1 100#1 25#2251799813685248 

testcases/regression/certificate_AdditionSimple.v

@@ -5,8 +5,9 @@ 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 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).

testcases/regression/certificate_AdditionSimpleAA.txt

+100 1 
+Ret + 1657#5 MTYPE 64  Var 0
+
+GAMMA Var 0 MTYPE 64 
+
+
+ PRE ? Var 0 ~100#1 100#1 
+
+ABS ? + 1657#5 MTYPE 64  Var 0 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 MTYPE 64  1657#5 1657#5 1657#45035996273704960 ? Var 0 ~100#1 100#1 25#2251799813685248 
+

testcases/regression/certificate_AdditionSimple_Fixed.v → testcases/regression/certificate_AdditionSimpleAA.v

 Require Import Flover.CertificateChecker.
-Definition C12 :expr Q := Const (F 32 22) ((1657)#(5)).
+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 :(nat -> option mType) := fun n =>
-if n =? 0 then Some (F 32 24) else None.
+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)), (9)#(16777216)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (1)#(16777216)) (FloverMap.add C12 (( (1657)#(5), (1657)#(5)), (1)#(4194304)) (FloverMap.empty (intv * error)))).
+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.

testcases/regression/certificate_AdditionSimpleAAScript.sml

+open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open simpLib realTheory realLib RealArith;
+
+val _ = new_theory "certificate_AdditionSimpleAA";
+
+
+val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
+val u0_def = Define `u0:(real expr) = Var 0`;
+val PlusC12u0 = Define `PlusC12u0:(real expr) = Binop Plus C12 u0`;;
+val RetPlusC12u0_def = Define `RetPlusC12u0 = Ret PlusC12u0`;
+
+
+val defVars_additionSimple_def = Define `
+ defVars_additionSimple : typeMap = 
+(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_empty))`;
+
+
+val thePrecondition_additionSimple_def = Define ` 
+ thePreconditionadditionSimple (n:num):interval = 
+if n = 0 then ( (-100)/(1), (100)/(1)) else (0,1)`;
+
+val absenv_additionSimple_def = RIGHT_CONV_RULE EVAL (Define `
+  absenv_additionSimple:analysisResult = 
+FloverMapTree_insert PlusC12u0 (( (1157)/(5), (2157)/(5)), (7771411516990528329)/(81129638414606681695789005144064)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))`);
+
+val _ = store_thm ("ErrorBound_additionSimple_Sound",
+``CertificateCheckerCmd RetPlusC12u0 absenv_additionSimple thePreconditionadditionSimple defVars_additionSimple``,
+ flover_eval_tac \\ fs[REAL_INV_1OVER]);
+
+
+ val _ = export_theory();

testcases/regression/certificate_AdditionSimpleScript.sml

@@ -4,15 +4,17 @@ open simpLib realTheory realLib RealArith;
 val _ = new_theory "certificate_AdditionSimple";
 
 
-val C12_def = Define `C12:(real exp) = Const M64 ((1657)/(5))`;
-val u0_def = Define `u0:(real exp) = Var 0`;
-val PlusC12u0 = Define `PlusC12u0:(real exp) = Binop Plus C12 u0`;;
+val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
+val u0_def = Define `u0:(real expr) = Var 0`;
+val PlusC12u0 = Define `PlusC12u0:(real expr) = Binop Plus C12 u0`;;
 val RetPlusC12u0_def = Define `RetPlusC12u0 = Ret PlusC12u0`;
 
 
 val defVars_additionSimple_def = Define `
- defVars_additionSimple (n:num) : mType option = 
-if (n = 0) then SOME M64 else NONE`;
+ defVars_additionSimple : typeMap = 
+(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_empty))`;
+
+
 val thePrecondition_additionSimple_def = Define ` 
  thePreconditionadditionSimple (n:num):interval = 
 if n = 0 then ( (-100)/(1), (100)/(1)) else (0,1)`;

testcases/regression/certificate_Doppler.txt

 100 1 
-Let Var 5 MTYPE 64 + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 Ret / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0
+Let Var 5 MTYPE 32 Cast MTYPE 32 + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 Ret / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0
+
+GAMMA Var 2 MTYPE 64 Var 5 MTYPE 32 Var 1 MTYPE 32 Var 0 MTYPE 64 
 
-GAMMA Var 2 MTYPE 64 Var 5 MTYPE 64 Var 1 MTYPE 64 Var 0 MTYPE 64 
 
  PRE ? Var 0 ~100#1 100#1 ? Var 1 20#1 20000#1 ? Var 2 ~30#1 50#1 
 
-ABS ? Var 5 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? 1657#5 MTYPE 64  1657#5 1657#5 1657#45035996273704960 ? * 3#5 MTYPE 64  Var 2 ~18#1 30#1 3650833728657301081634471694827535#365375409332725729550921208179070754913983135744 ? 3#5 MTYPE 64  3#5 3#5 3#45035996273704960 ? Var 2 ~30#1 50#1 25#4503599627370496  ? / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0 ~180700000#1138489 ~156700#5322249 4539010972026683303050120095327512216096422204478916695616374703820945778271922835308820707992089065905809072803102359543119833046473491986173951465620708023920966108209278836911630406540351629664583258832952458474781714583641201336156211255871250258363339134573360321968683520123662731962148793248799126762059670142230384240259443958280927316219469399605577522382054092479955357491038836701067526006061330750371234271363459989977730726293112263204327432621633884375#6946881575336902398274073006442580695940363163353906376754739965735202698392559846418891988118801115081550268650112893004414138824905360424712176030962427176970330198413894472430113124972848478861036028596232644451943248527831305533814306762870254280021814184312793167557111190875651884658457951357503922164630579910655264970400579248413892869201129019278339105434841776095040929995238102957547326071498788437802549670716277097027061404357118143901490561892403102252934918832128 ? * ~ Var 5 Var 1 ~7228000#1 ~6268#1 27893851128912527228254446719689338467872526596253813879482502889568449178778992649375#8343699359066055009355553539724812947666814540455674882605631280555545803830627148527195652096 ? ~ Var 5 ~1807#5 ~1567#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? Var 5 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? Var 1 20#1 20000#1 625#281474976710656 ? * + Var 5 Var 0 + Var 5 Var 0 1138489#25 5322249#25 31925542667783538931925887764808218521724458943918984144150813990256848378453146446353514550378395469015865480921312990060616935650290296361584748492021295664945174009#197864321178483627248402016815717752028105079280969471931250444874317780085225493736253120848994435991678137140812911471481092027445400967974036924081514534333285417718959308800 ? + Var 5 Var 0 1067#5 2307#5 22118872259511654165679074210367094250583915178799247531173589549131#148213874223764730142170860811120522052185580372019921970505707530128805939118080 ? Var 5 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? Var 0 ~100#1 100#1 25#2251799813685248 ? + Var 5 Var 0 1067#5 2307#5 22118872259511654165679074210367094250583915178799247531173589549131#148213874223764730142170860811120522052185580372019921970505707530128805939118080 ? Var 5 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? Var 0 ~100#1 100#1 25#2251799813685248 
+ABS ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Cast MTYPE 32 + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? 1657#5 MTYPE 64  1657#5 1657#5 1657#45035996273704960 ? * 3#5 MTYPE 64  Var 2 ~18#1 30#1 3650833728657301081634471694827535#365375409332725729550921208179070754913983135744 ? 3#5 MTYPE 64  3#5 3#5 3#45035996273704960 ? Var 2 ~30#1 50#1 25#4503599627370496  ? / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0 ~180700000#1138489 ~156700#5322249 3128798615377558964734587413815260935766775940003133188505004688351541231456980597512692494850911181122476079460422247077079176104347591604229243224768895229048954292495195716430601972291603510900358841802949847973326821449585470105361794370971246392326730165769086503662250520953800794720080442853388469377023727444437325832874114769965213547362197536886857310450874114551302656316164631446184855133337791662127325138346785397490340980930573694307935576641198224172023812349312175410753884375#32036808664321353711103483032138488273658359037549607658529725639211828966830820254532621633000657987120666498279218129796043154742555162761269493533793888535784577584907972014998498622632370186488026019213317308445273559994196553084922725810710211676061848042954653773443813684285036579995330627524678538042961243278389567362111169788921619483881120057899533645621131479344403647093086239019570741449266701692934633407390503406115529744843066088021266694728367150101865392734271463782370359902208 ? * ~ Var 5 Var 1 ~7228000#1 ~6268#1 627708954014028785690670388543358359225843737736535036700014937775757601384955913375#485667223056432267729865476705879726660601709763034880312953102434726071301302124544 ? ~ Var 5 ~1807#5 ~1567#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 1 20#1 20000#1 625#524288 ? * + Var 5 Var 0 + Var 5 Var 0 1138489#25 5322249#25 221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677#11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248 
 

testcases/regression/certificate_Doppler.v

@@ -4,6 +4,7 @@ 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.
@@ -13,19 +14,21 @@ 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 Lett15e6Rete10 := Let M64 5 e6 Rete10.
+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 defVars_doppler :(nat -> option mType) := fun n =>
-if n =? 2 then Some M64 else if n =? 5 then Some M64 else if n =? 1 then Some M64 else if n =? 0 then Some M64 else None.
 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)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048) ) (FloverMap.add e10 (( (-180700000)#(1138489), (-156700)#(5322249)), (4539010972026683303050120095327512216096422204478916695616374703820945778271922835308820707992089065905809072803102359543119833046473491986173951465620708023920966108209278836911630406540351629664583258832952458474781714583641201336156211255871250258363339134573360321968683520123662731962148793248799126762059670142230384240259443958280927316219469399605577522382054092479955357491038836701067526006061330750371234271363459989977730726293112263204327432621633884375)#(6946881575336902398274073006442580695940363163353906376754739965735202698392559846418891988118801115081550268650112893004414138824905360424712176030962427176970330198413894472430113124972848478861036028596232644451943248527831305533814306762870254280021814184312793167557111190875651884658457951357503922164630579910655264970400579248413892869201129019278339105434841776095040929995238102957547326071498788437802549670716277097027061404357118143901490561892403102252934918832128)) (FloverMap.add e9 (( (1138489)#(25), (5322249)#(25)), (31925542667783538931925887764808218521724458943918984144150813990256848378453146446353514550378395469015865480921312990060616935650290296361584748492021295664945174009)#(197864321178483627248402016815717752028105079280969471931250444874317780085225493736253120848994435991678137140812911471481092027445400967974036924081514534333285417718959308800)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (22118872259511654165679074210367094250583915178799247531173589549131)#(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e8 (( (1067)#(5), (2307)#(5)), (22118872259511654165679074210367094250583915178799247531173589549131)#(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMap.add u0 (( (-100)#(1), (100)#(1)), (25)#(2251799813685248)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add e7 (( (-7228000)#(1), (-6268)#(1)), (27893851128912527228254446719689338467872526596253813879482502889568449178778992649375)#(8343699359066055009355553539724812947666814540455674882605631280555545803830627148527195652096)) (FloverMap.add v1 (( (20)#(1), (20000)#(1)), (625)#(281474976710656)) (FloverMap.add UMint15 (( (-1807)#(5), (-1567)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMap.add t15 (( (1567)#(5), (1807)#(5)), (286015870425657721837309664377505636991869898457103)#(3291009114642412084309938365114701009965471731267159726697218048)) (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))))))))))))))))))).
+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 Lett15e6Rete10 absenv_doppler thePrecondition_doppler defVars_doppler = true.
+CertificateCheckerCmd Lett15CastM32e6Rete10 absenv_doppler thePrecondition_doppler defVars_doppler = true.
 Proof.
   vm_compute; auto.
 Qed.

testcases/regression/certificate_DopplerAA.txt

+100 1 
+Let Var 5 MTYPE 32 Cast MTYPE 32 + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 Ret / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0
+
+GAMMA Var 2 MTYPE 64 Var 5 MTYPE 32 Var 1 MTYPE 32 Var 0 MTYPE 64 
+
+
+ PRE ? Var 0 ~100#1 100#1 ? Var 1 20#1 20000#1 ? Var 2 ~30#1 50#1 
+
+ABS ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Cast MTYPE 32 + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? + 1657#5 MTYPE 64  * 3#5 MTYPE 64  Var 2 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? 1657#5 MTYPE 64  1657#5 1657#5 1657#45035996273704960 ? * 3#5 MTYPE 64  Var 2 ~18#1 30#1 3650833728657301081634471694827535#365375409332725729550921208179070754913983135744 ? 3#5 MTYPE 64  3#5 3#5 3#45035996273704960 ? Var 2 ~30#1 50#1 25#4503599627370496  ? / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0 ~1697764138654329772000#3490644748218790563 845148567992740137100#3490644748218790563 86789720644057150247866605447704701639542420366828894132198862668669714230796996017035083608214420357613914531567484222212219331055483511822890139010872023483027505740246147962523569787278664172305316497757644071254699998665282042562758048408625758851595888688321139287912787500084300448747342010732963228878699239161772886561738720968290627692004030895987294913860908138447593680198320054472132697520066221100165663039771347855801540617277134187668140137009343975368944377522556200084375#116581075971445025849972765325192688960688023193987481443423359259469524004578990495359777413108258534013101183101133893535361165723138789382125100532000290607255302844371142602120272808586051005748656571844135028373285214957706768877222323723316372017777470087619528348277265902992869293242456576370752686840418222478699145317598793362601803894470311876274014967799666442159459249464411902617752130127840333947718959260993021328099576810901846581180134891356519631659292569462696113720000512 ? * ~ Var 5 Var 1 ~7228000#1 473252#1 627708954014028785690670388543358359225843737736535036700014937775757601384955913375#485667223056432267729865476705879726660601709763034880312953102434726071301302124544 ? ~ Var 5 ~1807#5 ~1567#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 1 20#1 20000#1 625#524288 ? * + Var 5 Var 0 + Var 5 Var 0 369689#25 5322249#25 221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677#11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248 
+

testcases/regression/certificate_DopplerAA.v

+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.

testcases/regression/certificate_DopplerAAScript.sml

+open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open simpLib realTheory realLib RealArith;
+
+val _ = new_theory "certificate_DopplerAA";
+
+
+val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
+val C34_def = Define `C34:(real expr) = Const M64 ((3)/(5))`;
+val T2_def = Define `T2:(real expr) = Var 2`;
+val MultC34T2 = Define `MultC34T2:(real expr) = Binop Mult C34 T2`;;
+val PlusC12MultC34T2 = Define `PlusC12MultC34T2:(real expr) = Binop Plus C12 MultC34T2`;;
+val CastM32PlusC12MultC34T2 = Define `CastM32PlusC12MultC34T2 : real expr = Downcast M32 PlusC12MultC34T2`;;
+val t15_def = Define `t15:(real expr) = Var 5`;
+val UMint15 = Define `UMint15:(real expr) = Unop Neg t15`;
+val v1_def = Define `v1:(real expr) = Var 1`;
+val MultUMint15v1 = Define `MultUMint15v1:(real expr) = Binop Mult UMint15 v1`;;
+val u0_def = Define `u0:(real expr) = Var 0`;
+val Plust15u0 = Define `Plust15u0:(real expr) = Binop Plus t15 u0`;;
+val MultPlust15u0Plust15u0 = Define `MultPlust15u0Plust15u0:(real expr) = Binop Mult Plust15u0 Plust15u0`;;
+val DivMultUMint15v1MultPlust15u0Plust15u0 = Define `DivMultUMint15v1MultPlust15u0Plust15u0:(real expr) = Binop Div MultUMint15v1 MultPlust15u0Plust15u0`;;
+val RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `RetDivMultUMint15v1MultPlust15u0Plust15u0 = Ret DivMultUMint15v1MultPlust15u0Plust15u0`;
+val Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 = Let M32 5 CastM32PlusC12MultC34T2 RetDivMultUMint15v1MultPlust15u0Plust15u0`;
+
+
+val defVars_doppler_def = Define `
+ defVars_doppler : typeMap = 
+(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_insert (Var 1) (M32) (FloverMapTree_insert (Var 5) (M32) (FloverMapTree_insert (Var 2) (M64) (FloverMapTree_empty)))))`;
+
+
+val thePrecondition_doppler_def = Define ` 
+ thePreconditiondoppler (n:num):interval = 
+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)`;
+
+val absenv_doppler_def = RIGHT_CONV_RULE EVAL (Define `
+  absenv_doppler:analysisResult = 
+FloverMapTree_insert (Var 5) (( (1567)/(5), (1807)/(5)) , (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert DivMultUMint15v1MultPlust15u0Plust15u0 (( (-1697764138654329772000)/(3490644748218790563), (845148567992740137100)/(3490644748218790563)), (86789720644057150247866605447704701639542420366828894132198862668669714230796996017035083608214420357613914531567484222212219331055483511822890139010872023483027505740246147962523569787278664172305316497757644071254699998665282042562758048408625758851595888688321139287912787500084300448747342010732963228878699239161772886561738720968290627692004030895987294913860908138447593680198320054472132697520066221100165663039771347855801540617277134187668140137009343975368944377522556200084375)/(116581075971445025849972765325192688960688023193987481443423359259469524004578990495359777413108258534013101183101133893535361165723138789382125100532000290607255302844371142602120272808586051005748656571844135028373285214957706768877222323723316372017777470087619528348277265902992869293242456576370752686840418222478699145317598793362601803894470311876274014967799666442159459249464411902617752130127840333947718959260993021328099576810901846581180134891356519631659292569462696113720000512)) (FloverMapTree_insert MultPlust15u0Plust15u0 (( (369689)/(25), (5322249)/(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)/(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert MultUMint15v1 (( (-7228000)/(1), (473252)/(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)/(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMapTree_insert v1 (( (20)/(1), (20000)/(1)), (625)/(524288)) (FloverMapTree_insert UMint15 (( (-1807)/(5), (-1567)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert CastM32PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert MultC34T2 (( (-18)/(1), (30)/(1)), (3650833728657301081634471694827535)/(365375409332725729550921208179070754913983135744)) (FloverMapTree_insert T2 (( (-30)/(1), (50)/(1)), (25)/(4503599627370496)) (FloverMapTree_insert C34 (( (3)/(5), (3)/(5)), (3)/(45035996273704960)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))))))))))))))))))`);
+
+val _ = store_thm ("ErrorBound_doppler_Sound",
+``CertificateCheckerCmd Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 absenv_doppler thePreconditiondoppler defVars_doppler``,
+ flover_eval_tac \\ fs[REAL_INV_1OVER]);
+
+
+ val _ = export_theory();

testcases/regression/certificate_Himmilbeau.txt

+100 1 
+Let Var 4 MTYPE 64 + * Var 0 Var 0 Var 1 Let Var 5 MTYPE 32 Cast MTYPE 32 + Var 0 * Var 1 Var 1 Ret + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64 
+
+GAMMA Var 0 MTYPE 64 Var 1 MTYPE 32 Var 4 MTYPE 64 Var 5 MTYPE 32 
+
+
+ PRE ? Var 0 ~5#1 5#1 ? Var 1 ~5#1 5#1 
+
+ABS ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? + * Var 0 Var 0 Var 1 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? * Var 0 Var 0 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#16777216  ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? Cast MTYPE 32 + Var 0 * Var 1 Var 1 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? + Var 0 * Var 1 Var 1 ~30#1 30#1 190147601533197042302697458892825#42535295865117307932921825928971026432 ? Var 0 ~5#1 5#1 5#9007199254740992 ? * Var 1 Var 1 ~25#1 25#1 21110624511590425#4722366482869645213696 ? Var 1 ~5#1 5#1 5#16777216 ? Var 1 ~5#1 5#1 5#16777216  ? + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~1630#1 3050#1 139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425#285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736 ? * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  ~779#1 1681#1 773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~851#1 1369#1 172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009#372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 
+

testcases/regression/certificate_Himmilbeau.v

+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 (( (-1630)#(1), (3050)#(1)), (139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425)#(285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736)) (FloverMap.add e12 (( (-851)#(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 (( (-779)#(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.

testcases/regression/certificate_HimmilbeauAA.txt

+100 1 
+Let Var 4 MTYPE 64 + * Var 0 Var 0 Var 1 Let Var 5 MTYPE 32 Cast MTYPE 32 + Var 0 * Var 1 Var 1 Ret + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64 
+
+GAMMA Var 0 MTYPE 64 Var 1 MTYPE 32 Var 4 MTYPE 64 Var 5 MTYPE 32 
+
+
+ PRE ? Var 0 ~5#1 5#1 ? Var 1 ~5#1 5#1 
+
+ABS ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? + * Var 0 Var 0 Var 1 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? * Var 0 Var 0 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#16777216  ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? Cast MTYPE 32 + Var 0 * Var 1 Var 1 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? + Var 0 * Var 1 Var 1 ~30#1 30#1 190147601533197042302697458892825#42535295865117307932921825928971026432 ? Var 0 ~5#1 5#1 5#9007199254740992 ? * Var 1 Var 1 ~25#1 25#1 21110624511590425#4722366482869645213696 ? Var 1 ~5#1 5#1 5#16777216 ? Var 1 ~5#1 5#1 5#16777216  ? + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~2710#1 3050#1 139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425#285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736 ? * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  ~1439#1 1681#1 773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~1271#1 1369#1 172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009#372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 
+

testcases/regression/certificate_HimmilbeauAA.v

+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.

testcases/regression/certificate_HimmilbeauAAScript.sml

+open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
+open simpLib realTheory realLib RealArith;
+
+val _ = new_theory "certificate_HimmilbeauAA";
+
+
+val x10_def = Define `x10:(real expr) = Var 0`;
+val Multx10x10 = Define `Multx10x10:(real expr) = Binop Mult x10 x10`;;
+val x21_def = Define `x21:(real expr) = Var 1`;
+val PlusMultx10x10x21 = Define `PlusMultx10x10x21:(real expr) = Binop Plus Multx10x10 x21`;;
+val t14_def = Define `t14:(real expr) = Var 4`;
+val Multx21x21 = Define `Multx21x21:(real expr) = Binop Mult x21 x21`;;
+val Plusx10Multx21x21 = Define `Plusx10Multx21x21:(real expr) = Binop Plus x10 Multx21x21`;;
+val CastM32Plusx10Multx21x21 = Define `CastM32Plusx10Multx21x21 : real expr = Downcast M32 Plusx10Multx21x21`;;
+val t25_def = Define `t25:(real expr) = Var 5`;
+val C12_def = Define `C12:(real expr) = Const M64 ((11)/(1))`;
+val Subt14C12 = Define `Subt14C12:(real expr) = Binop Sub t14 C12`;;
+val MultSubt14C12Subt14C12 = Define `MultSubt14C12Subt14C12:(real expr) = Binop Mult Subt14C12 Subt14C12`;;
+val C34_def = Define `C34:(real expr) = Const M64 ((7)/(1))`;
+val Subt25C34 = Define `Subt25C34:(real expr) = Binop Sub t25 C34`;;
+val MultSubt25C34Subt25C34 = Define `MultSubt25C34Subt25C34:(real expr) = Binop Mult Subt25C34 Subt25C34`;;
+val PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Define `PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34:(real expr) = Binop Plus MultSubt14C12Subt14C12 MultSubt25C34Subt25C34`;;
+val RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Ret PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
+val Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M32 5 CastM32Plusx10Multx21x21 RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
+val Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M64 4 PlusMultx10x10x21 Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
+
+
+val defVars_himmilbeau_def = Define `
+ defVars_himmilbeau : typeMap = 
+(FloverMapTree_insert (Var 5) (M32) (FloverMapTree_insert (Var 4) (M64) (FloverMapTree_insert (Var 1) (M32) (FloverMapTree_insert (Var 0) (M64) (FloverMapTree_empty)))))`;
+
+
+val thePrecondition_himmilbeau_def = Define ` 
+ thePreconditionhimmilbeau (n:num):interval = 
+if n = 0 then ( (-5)/(1), (5)/(1)) else if n = 1 then ( (-5)/(1), (5)/(1)) else (0,1)`;
+
+val absenv_himmilbeau_def = RIGHT_CONV_RULE EVAL (Define `
+  absenv_himmilbeau:analysisResult = 
+FloverMapTree_insert (Var 4) (( (-30)/(1), (30)/(1)) , (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert (Var 5) (( (-30)/(1), (30)/(1)) , (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 (( (-2710)/(1), (3050)/(1)), (139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425)/(285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736)) (FloverMapTree_insert MultSubt25C34Subt25C34 (( (-1271)/(1), (1369)/(1)), (172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009)/(372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert MultSubt14C12Subt14C12 (( (-1439)/(1), (1681)/(1)), (773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649)/(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert CastM32Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (190147601533197042302697458892825)/(42535295865117307932921825928971026432)) (FloverMapTree_insert Multx21x21 (( (-25)/(1), (25)/(1)), (21110624511590425)/(4722366482869645213696)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert PlusMultx10x10x21 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert Multx10x10 (( (-25)/(1), (25)/(1)), (6084722881095501802724119491379225)/(730750818665451459101842416358141509827966271488)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_empty))))))))))))))))))))))))))))`);
+
+val _ = store_thm ("ErrorBound_himmilbeau_Sound",
+``CertificateCheckerCmd Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau``,
+ flover_eval_tac \\ fs[REAL_INV_1OVER]);
+
+
+ val _ = export_theory();

testcases/regression/certificate_HimmilbeauLet.txt

-100 1 
-Let Var 4 MTYPE 64 + * Var 0 Var 0 Var 1 Let Var 5 MTYPE 64 + Var 0 * Var 1 Var 1 Ret + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64 
-
-GAMMA Var 0 MTYPE 64 Var 1 MTYPE 64 Var 4 MTYPE 64 Var 5 MTYPE 64 
-
- PRE ? Var 0 ~5#1 5#1 ? Var 1 ~5#1 5#1 
-
-ABS ? Var 4 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? + * Var 0 Var 0 Var 1 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? * Var 0 Var 0 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#9007199254740992  ? Var 5 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? + Var 0 * Var 1 Var 1 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? Var 0 ~5#1 5#1 5#9007199254740992 ? * Var 1 Var 1 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 1 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#9007199254740992  ? + * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~1630#1 3050#1 487221104469898338786214736384485254774988686254174245053949966326997127520915678921005561985107526535736733169631780463955289592797563726474122500394813215491039731582541464863345#142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368 ? * - Var 4 11#1 MTYPE 64  - Var 4 11#1 MTYPE 64  ~779#1 1681#1 52598628855733566340954758429892096626280035552108502465466895493129796503242744882270069972736188166377760848721456131524041627993346956366876383676799845782258289#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 1066286953144141717003645981961786527395115480482574790071743938585#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? - Var 4 11#1 MTYPE 64  ~41#1 19#1 1066286953144141717003645981961786527395115480482574790071743938585#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64  11#1 11#1 11#9007199254740992 ? * - Var 5 7#1 MTYPE 64  - Var 5 7#1 MTYPE 64  ~851#1 1369#1 44866120771362444857686649346472984093164433346912932734434048679126990349360865083173278510423947460944096667238715938574578896368729586451911668210669271295984241#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 1013630807309863120731683693458145474828298267349734195132723363865#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 5 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 ? - Var 5 7#1 MTYPE 64  ~37#1 23#1 1013630807309863120731683693458145474828298267349734195132723363865#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 5 ~30#1 30#1 80382590053199673076296620063432129648297561292825#6582018229284824168619876730229402019930943462534319453394436096 ? 7#1 MTYPE 64  7#1 7#1 7#9007199254740992 
-

testcases/regression/certificate_HimmilbeauLet.v

-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 Rete13 := Ret e13.
-Definition Lett25e4Rete13 := Let M64 5 e4 Rete13.
-Definition Lett14e2Lett25e4Rete13 := Let M64 4 e2 Lett25e4Rete13.
-
-
-Definition defVars_himmilbeau :(nat -> option mType) := fun n =>
-if n =? 0 then Some M64 else if n =? 1 then Some M64 else if n =? 4 then Some M64 else if n =? 5 then Some M64 else None.
-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)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096) ) (FloverMap.add (Var Q 5) (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096) ) (FloverMap.add e13 (( (-1630)#(1), (3050)#(1)), (487221104469898338786214736384485254774988686254174245053949966326997127520915678921005561985107526535736733169631780463955289592797563726474122500394813215491039731582541464863345)#(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMap.add e12 (( (-851)#(1), (1369)#(1)), (44866120771362444857686649346472984093164433346912932734434048679126990349360865083173278510423947460944096667238715938574578896368729586451911668210669271295984241)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e11 (( (-37)#(1), (23)#(1)), (1013630807309863120731683693458145474828298267349734195132723363865)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (( (7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e11 (( (-37)#(1), (23)#(1)), (1013630807309863120731683693458145474828298267349734195132723363865)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C910 (( (7)#(1), (7)#(1)), (7)#(9007199254740992)) (FloverMap.add t25 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e8 (( (-779)#(1), (1681)#(1)), (52598628855733566340954758429892096626280035552108502465466895493129796503242744882270069972736188166377760848721456131524041627993346956366876383676799845782258289)#(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMap.add e7 (( (-41)#(1), (19)#(1)), (1066286953144141717003645981961786527395115480482574790071743938585)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (( (11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e7 (( (-41)#(1), (19)#(1)), (1066286953144141717003645981961786527395115480482574790071743938585)#(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMap.add C56 (( (11)#(1), (11)#(1)), (11)#(9007199254740992)) (FloverMap.add t14 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e4 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add e3 (( (-25)#(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 e2 (( (-30)#(1), (30)#(1)), (80382590053199673076296620063432129648297561292825)#(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMap.add x21 (( (-5)#(1), (5)#(1)), (5)#(9007199254740992)) (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 Lett14e2Lett25e4Rete13 absenv_himmilbeau thePrecondition_himmilbeau defVars_himmilbeau = true.
-Proof.
-  vm_compute; auto.
-Qed.

testcases/regression/certificate_HimmilbeauLetScript.sml

-open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
-open simpLib realTheory realLib RealArith;