Commit 31a9b505 authored by Heiko Becker's avatar Heiko Becker

Forward daisy to latest state of certificates branch and add some regression tests

parent d3a29e38
......@@ -5,6 +5,7 @@ variables:
stages:
- compile
- regression
compile-coq:
stage: compile
......@@ -21,3 +22,9 @@ compile-hol:
expire_in: 24h
paths:
- hol4/binary/
regression-tests:
stage: regression
only:
- master
script: ./scripts/regressiontests.sh
\ No newline at end of file
Subproject commit 61171aefca087e70600f83d673aaf74981bd8d7c
Subproject commit fc1b5c0d4bae293a50ff652a9c22ec68ea465d55
#!/bin/bash
cd ./testcases/regression
#Coq regression tests
for fname in ./*.v; do
coqc -R ../../coq Flover $fname
if [ $? -eq 1 ]
then
echo "Checking $fname failed"
exit 1;
fi
echo "Successfully checked $fname"
done
#HOL4 regression tests
for fname in ./*.sml; do
FILEPRE=${fname/Script.sml/}
FILENAME=$FILEPRE
$HOLDIR/bin/Holmake ${fname/Script.sml/Theory.sig} -q
if [ $? -eq 1 ]
then
echo "Checking $FILENAME has failed"
exit 1;
fi
echo "Successfully checked $FILENAME"
done
#Binary regression tests
for fname in ./*.txt; do
../../hol4/binary/cake_checker $fname
if [ $? -eq 1 ]
then
echo "Checking $fname has failed"
exit 1;
fi
echo "Successfully checked $fname";
done
COQAUX1 14eb2e5e017990f6a3f1ccef9be1fc57 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_AdditionSimple.v
42 90 context_used ";"
91 123 context_used ";"
124 166 context_used ";"
167 194 context_used ";"
197 300 context_used ";"
301 424 context_used ";"
426 777 context_used ";"
933 939 VernacProof "tac:no using:no"
960 964 proof_build_time "0.013"
--- ErrorBound_additionSimple_Sound "0.013"
960 964 context_used ";"
960 964 proof_check_time "0.010"
--- vo_compile_time "0.759"
COQAUX1 7830f6aeda2c910507e270bf93518d00 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_Doppler.v
42 90 context_used ";"
91 136 context_used ";"
137 169 context_used ";"
170 212 context_used ";"
213 255 context_used ";"
256 289 context_used ";"
290 332 context_used ";"
333 365 context_used ";"
366 412 context_used ";"
413 445 context_used ";"
446 488 context_used ";"
489 530 context_used ";"
531 572 context_used ";"
573 602 context_used ";"
603 652 context_used ";"
655 838 context_used ";"
839 1043 context_used ";"
1045 4798 context_used ";"
4935 4941 VernacProof "tac:no using:no"
4962 4966 proof_build_time "0.770"
--- ErrorBound_doppler_Sound "0.770"
4962 4966 context_used ";"
4962 4966 proof_check_time "0.719"
--- vo_compile_time "2.537"
COQAUX1 9cdd343852a339130dbc781256fbb137 /local/home/hbecker/Git_Repos/FloVer/testcases/regression/certificate_HimmilbeauLet.v
42 75 context_used ";"
76 119 context_used ";"
120 153 context_used ";"
154 196 context_used ";"
197 230 context_used ";"
231 274 context_used ";"
275 317 context_used ";"
318 351 context_used ";"
352 398 context_used ";"
399 441 context_used ";"
442 483 context_used ";"
484 530 context_used ";"
531 575 context_used ";"
576 620 context_used ";"
621 664 context_used ";"
665 694 context_used ";"
695 744 context_used ";"
745 810 context_used ";"
813 999 context_used ";"
1000 1156 context_used ";"
1158 5544 context_used ";"
5701 5707 VernacProof "tac:no using:no"
5728 5732 proof_build_time "0.228"
--- ErrorBound_himmilbeau_Sound "0.228"
5728 5732 context_used ";"
5728 5732 proof_check_time "0.229"
--- vo_compile_time "1.545"
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../../hol4 ../../hol4/Infra ../../hol4/cakeml/misc
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
HOLHEAP = heap
EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
all: $(HOLHEAP)
THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
TARGETS = $(patsubst %.sml,%.uo,$(THYFILES))
all: $(TARGETS) $(HOLHEAP)
.PHONY: all
BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
alistTheory arithmeticTheory bagTheory boolLib boolSimps bossLib \
combinTheory dep_rewrite finite_mapTheory indexedListsTheory lcsymtacs \
listTheory llistTheory markerLib realTheory realLib RealArith\
optionTheory pairLib pairTheory pred_setTheory \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
DIGEST 14eb2e5e017990f6a3f1ccef9be1fc57
Fcertificate_AdditionSimple
R15:39 Flover.CertificateChecker <> <> lib
def 53:55 <> C12
R58:60 Flover.Expressions <> exp ind
R62:62 Coq.QArith.QArith_base <> Q rec
R67:71 Flover.Expressions <> Const constr
R84:84 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R73:75 Flover.Infra.MachineType <> M64 constr
def 102:103 <> u0
R106:108 Flover.Expressions <> exp ind
R110:110 Coq.QArith.QArith_base <> Q rec
R115:117 Flover.Expressions <> Var constr
R119:119 Coq.QArith.QArith_base <> Q rec
def 135:136 <> e3
R139:141 Flover.Expressions <> exp ind
R143:143 Coq.QArith.QArith_base <> Q rec
R148:152 Flover.Expressions <> Binop constr
R163:164 certificate_AdditionSimple <> u0 def
R159:161 certificate_AdditionSimple <> C12 def
R154:157 Flover.Expressions <> Plus constr
def 178:182 <> Rete3
R187:189 Flover.Commands <> Ret constr
R191:192 certificate_AdditionSimple <> e3 def
def 208:229 <> defVars_additionSimple
R236:239 Coq.Init.Logic <> :type_scope:x_'->'_x not
R240:245 Coq.Init.Datatypes <> option ind
R247:251 Flover.Infra.MachineType <> mType ind
R233:235 Coq.Init.Datatypes <> nat ind
R270:273 Coq.Arith.PeanoNat <> :nat_scope:x_'=?'_x not
R269:269 certificate_AdditionSimple <> n var
R295:298 Coq.Init.Datatypes <> None constr
R281:284 Coq.Init.Datatypes <> Some constr
R286:288 Flover.Infra.MachineType <> M64 constr
def 312:341 <> thePrecondition_additionSimple
R343:349 Flover.Infra.Abbrevs <> precond def
R361:363 Coq.Init.Datatypes <> nat ind
R373:376 Coq.Arith.PeanoNat <> :nat_scope:x_'=?'_x not
R372:372 certificate_AdditionSimple <> n var
R414:414 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R418:418 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R422:422 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R416:416 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R420:420 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R384:385 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R396:397 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R407:407 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R386:386 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R391:392 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R403:403 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
def 437:457 <> absenv_additionSimple
R460:473 Flover.Infra.ExpressionAbbrevs <> analysisResult def
R494:506 Flover.Infra.ExpressionAbbrevs FloverMap add def
R598:610 Flover.Infra.ExpressionAbbrevs FloverMap add def
R668:680 Flover.Infra.ExpressionAbbrevs FloverMap add def
R743:757 Flover.Infra.ExpressionAbbrevs FloverMap empty def
R764:766 Coq.Init.Datatypes <> :type_scope:x_'*'_x not
R760:763 Flover.Infra.Abbrevs <> intv def
R767:771 Flover.Infra.Abbrevs <> error def
R686:686 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R712:713 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R740:740 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R687:688 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R699:700 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R711:711 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R695:695 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R707:707 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R720:720 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R682:684 certificate_AdditionSimple <> C12 def
R615:615 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R640:641 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R665:665 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R616:617 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R628:629 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R639:639 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R618:618 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R623:624 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R635:635 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R646:646 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R612:613 certificate_AdditionSimple <> u0 def
R511:511 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R537:538 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R595:595 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R512:513 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R524:525 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R536:536 Coq.Init.Datatypes <> :core_scope:'('_x_','_x_','_'..'_','_x_')' not
R520:520 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R532:532 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R560:560 Coq.QArith.QArith_base <> :Q_scope:x_'#'_x not
R508:509 certificate_AdditionSimple <> e3 def
prf 787:817 <> ErrorBound_additionSimple_Sound
R924:926 Coq.Init.Logic <> :type_scope:x_'='_x not
R821:841 Flover.CertificateChecker <> CertificateCheckerCmd def
R902:923 certificate_AdditionSimple <> defVars_additionSimple def
R871:900 certificate_AdditionSimple <> thePrecondition_additionSimple def
R849:869 certificate_AdditionSimple <> absenv_additionSimple def
R843:847 certificate_AdditionSimple <> Rete3 def
R927:930 Coq.Init.Datatypes <> true constr
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
Require Import Flover.CertificateChecker.
Definition C12 :exp Q := Const M64 ((1657)#(5)).
Definition u0 :exp Q := Var Q 0.
Definition e3 :exp Q := Binop Plus C12 u0.
Definition Rete3 := Ret e3.
Definition defVars_additionSimple :(nat -> option mType) := fun n =>
if n =? 0 then Some M64 else None.
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.
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
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 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`;
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``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
This diff is collapsed.
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
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
Require Import Flover.CertificateChecker.
Definition C12 :exp Q := Const M64 ((1657)#(5)).
Definition C34 :exp Q := Const M64 ((3)#(5)).
Definition T2 :exp Q := Var Q 2.
Definition e5 :exp Q := Binop Mult C34 T2.
Definition e6 :exp Q := Binop Plus C12 e5.
Definition t15 :exp Q := Var Q 5.
Definition UMint15 :exp Q := Unop Neg t15.
Definition v1 :exp Q := Var Q 1.
Definition e7 :exp Q := Binop Mult UMint15 v1.
Definition u0 :exp Q := Var Q 0.
Definition e8 :exp Q := Binop Plus t15 u0.
Definition e9 :exp Q := Binop Mult e8 e8.
Definition e10 :exp Q := Binop Div e7 e9.
Definition Rete10 := Ret e10.
Definition Lett15e6Rete10 := Let M64 5 e6 Rete10.
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))))))))))))))))))).
Theorem ErrorBound_doppler_Sound :
CertificateCheckerCmd Lett15e6Rete10 absenv_doppler thePrecondition_doppler defVars_doppler = true.
Proof.
vm_compute; auto.
Qed.
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_Doppler";
val C12_def = Define `C12:(real exp) = Const M64 ((1657)/(5))`;
val C34_def = Define `C34:(real exp) = Const M64 ((3)/(5))`;
val T2_def = Define `T2:(real exp) = Var 2`;
val MultC34T2 = Define `MultC34T2:(real exp) = Binop Mult C34 T2`;;
val PlusC12MultC34T2 = Define `PlusC12MultC34T2:(real exp) = Binop Plus C12 MultC34T2`;;
val t15_def = Define `t15:(real exp) = Var 5`;
val UMint15 = Define `UMint15:(real exp) = Unop Neg t15`;
val v1_def = Define `v1:(real exp) = Var 1`;
val MultUMint15v1 = Define `MultUMint15v1:(real exp) = Binop Mult UMint15 v1`;;
val u0_def = Define `u0:(real exp) = Var 0`;
val Plust15u0 = Define `Plust15u0:(real exp) = Binop Plus t15 u0`;;
val MultPlust15u0Plust15u0 = Define `MultPlust15u0Plust15u0:(real exp) = Binop Mult Plust15u0 Plust15u0`;;
val DivMultUMint15v1MultPlust15u0Plust15u0 = Define `DivMultUMint15v1MultPlust15u0Plust15u0:(real exp) = Binop Div MultUMint15v1 MultPlust15u0Plust15u0`;;
val RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `RetDivMultUMint15v1MultPlust15u0Plust15u0 = Ret DivMultUMint15v1MultPlust15u0Plust15u0`;
val Lett15PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `Lett15PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 = Let M64 5 PlusC12MultC34T2 RetDivMultUMint15v1MultPlust15u0Plust15u0`;
val defVars_doppler_def = Define `
defVars_doppler (n:num) : mType option =
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`;
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)) , (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert DivMultUMint15v1MultPlust15u0Plust15u0 (( (-180700000)/(1138489), (-156700)/(5322249)), (4539010972026683303050120095327512216096422204478916695616374703820945778271922835308820707992089065905809072803102359543119833046473491986173951465620708023920966108209278836911630406540351629664583258832952458474781714583641201336156211255871250258363339134573360321968683520123662731962148793248799126762059670142230384240259443958280927316219469399605577522382054092479955357491038836701067526006061330750371234271363459989977730726293112263204327432621633884375)/(6946881575336902398274073006442580695940363163353906376754739965735202698392559846418891988118801115081550268650112893004414138824905360424712176030962427176970330198413894472430113124972848478861036028596232644451943248527831305533814306762870254280021814184312793167557111190875651884658457951357503922164630579910655264970400579248413892869201129019278339105434841776095040929995238102957547326071498788437802549670716277097027061404357118143901490561892403102252934918832128)) (FloverMapTree_insert MultPlust15u0Plust15u0 (( (1138489)/(25), (5322249)/(25)), (31925542667783538931925887764808218521724458943918984144150813990256848378453146446353514550378395469015865480921312990060616935650290296361584748492021295664945174009)/(197864321178483627248402016815717752028105079280969471931250444874317780085225493736253120848994435991678137140812911471481092027445400967974036924081514534333285417718959308800)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (22118872259511654165679074210367094250583915178799247531173589549131)/(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (22118872259511654165679074210367094250583915178799247531173589549131)/(148213874223764730142170860811120522052185580372019921970505707530128805939118080)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert MultUMint15v1 (( (-7228000)/(1), (-6268)/(1)), (27893851128912527228254446719689338467872526596253813879482502889568449178778992649375)/(8343699359066055009355553539724812947666814540455674882605631280555545803830627148527195652096)) (FloverMapTree_insert v1 (( (20)/(1), (20000)/(1)), (625)/(281474976710656)) (FloverMapTree_insert UMint15 (( (-1807)/(5), (-1567)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (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 Lett15PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 absenv_doppler thePreconditiondoppler defVars_doppler``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
This diff is collapsed.
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
Require Import Flover.CertificateChecker.
Definition x10 :exp Q := Var Q 0.
Definition e1 :exp Q := Binop Mult x10 x10.
Definition x21 :exp Q := Var Q 1.
Definition e2 :exp Q := Binop Plus e1 x21.
Definition t14 :exp Q := Var Q 4.
Definition e3 :exp Q := Binop Mult x21 x21.
Definition e4 :exp Q := Binop Plus x10 e3.
Definition t25 :exp Q := Var Q 5.
Definition C56 :exp Q := Const M64 ((11)#(1)).
Definition e7 :exp Q := Binop Sub t14 C56.
Definition e8 :exp Q := Binop Mult e7 e7.
Definition C910 :exp Q := Const M64 ((7)#(1)).
Definition e11 :exp Q := Binop Sub t25 C910.
Definition e12 :exp Q := Binop Mult e11 e11.
Definition e13 :exp 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.
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_HimmilbeauLet";
val x10_def = Define `x10:(real exp) = Var 0`;
val Multx10x10 = Define `Multx10x10:(real exp) = Binop Mult x10 x10`;;
val x21_def = Define `x21:(real exp) = Var 1`;
val PlusMultx10x10x21 = Define `PlusMultx10x10x21:(real exp) = Binop Plus Multx10x10 x21`;;
val t14_def = Define `t14:(real exp) = Var 4`;
val Multx21x21 = Define `Multx21x21:(real exp) = Binop Mult x21 x21`;;
val Plusx10Multx21x21 = Define `Plusx10Multx21x21:(real exp) = Binop Plus x10 Multx21x21`;;
val t25_def = Define `t25:(real exp) = Var 5`;
val C12_def = Define `C12:(real exp) = Const M64 ((11)/(1))`;
val Subt14C12 = Define `Subt14C12:(real exp) = Binop Sub t14 C12`;;
val MultSubt14C12Subt14C12 = Define `MultSubt14C12Subt14C12:(real exp) = Binop Mult Subt14C12 Subt14C12`;;
val C34_def = Define `C34:(real exp) = Const M64 ((7)/(1))`;
val Subt25C34 = Define `Subt25C34:(real exp) = Binop Sub t25 C34`;;
val MultSubt25C34Subt25C34 = Define `MultSubt25C34Subt25C34:(real exp) = Binop Mult Subt25C34 Subt25C34`;;
val PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Define `PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34:(real exp) = Binop Plus MultSubt14C12Subt14C12 MultSubt25C34Subt25C34`;;
val RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Ret PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M64 5 Plusx10Multx21x21 RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val Lett14PlusMultx10x10x21Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett14PlusMultx10x10x21Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M64 4 PlusMultx10x10x21 Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val defVars_himmilbeau_def = Define `
defVars_himmilbeau (n:num) : mType option =
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`;
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)) , (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert (Var 5) (( (-30)/(1), (30)/(1)) , (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 (( (-1630)/(1), (3050)/(1)), (487221104469898338786214736384485254774988686254174245053949966326997127520915678921005561985107526535736733169631780463955289592797563726474122500394813215491039731582541464863345)/(142576269300693600582536612678134103902913390851517497830599766184352348975271168328309775353667856243082572174174825228459022022542982437445395666241319193382874833573758279690089818507706368)) (FloverMapTree_insert MultSubt25C34Subt25C34 (( (-851)/(1), (1369)/(1)), (44866120771362444857686649346472984093164433346912932734434048679126990349360865083173278510423947460944096667238715938574578896368729586451911668210669271295984241)/(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (1013630807309863120731683693458145474828298267349734195132723363865)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (1013630807309863120731683693458145474828298267349734195132723363865)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert MultSubt14C12Subt14C12 (( (-779)/(1), (1681)/(1)), (52598628855733566340954758429892096626280035552108502465466895493129796503242744882270069972736188166377760848721456131524041627993346956366876383676799845782258289)/(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (1066286953144141717003645981961786527395115480482574790071743938585)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (1066286953144141717003645981961786527395115480482574790071743938585)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Multx21x21 (( (-25)/(1), (25)/(1)), (6084722881095501802724119491379225)/(730750818665451459101842416358141509827966271488)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert PlusMultx10x10x21 (( (-30)/(1), (30)/(1)), (80382590053199673076296620063432129648297561292825)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (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 Lett14PlusMultx10x10x21Lett25Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau``,
daisy_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
\ No newline at end of file
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment