Commit 5dbe22dc authored by Heiko Becker's avatar Heiko Becker

fforward CakeML to master branch, fforward HOL

parent 46d9b0cc
[submodule "hol4/cakeml"]
branch = FMA_support
branch = master
path = hol4/cakeml
url = https://github.com/CakeML/cakeml.git
[submodule "daisy"]
branch = certified
branch = certified
path = daisy
url = ../../AVA/daisy.git
8e183cc626814e8bfbee46abcbf51798ee1c69b6
570cfc9afd5e6ac1fd5a51e50c0780453c975124
......@@ -107,6 +107,9 @@ val validErrorbound_def = Define `
else F)`;
add_unevaluated_function ``validErrorbound``;
add_unevaluated_function ``minAbsFun``;
add_unevaluated_function ``noDivzero``;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (typeMap: (real expr # mType) binTree)
......@@ -167,6 +170,9 @@ val validErrorboundCorrectVariable_eval = store_thm (
>- (Cases_on `lookup v dVars` \\ fs[domain_lookup])
\\ fs[eval_expr_cases, toRExpMap_def, toRTMap_def, option_case_eq]);
add_unevaluated_function ``computeError``;
add_unevaluated_function ``maxAbs``;
val validErrorboundCorrectVariable = store_thm (
"validErrorboundCorrectVariable",
``! (E1 E2:env) A fVars dVars (v:num) (nR nF err nlo nhi:real) (P:precond) m
......@@ -290,7 +296,7 @@ val validErrorboundCorrectAddition = store_thm (
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [validIntervalAdd_def, contained_def] interval_addition_valid)
\\ fs[contained_def]);
\\ fs[contained_def, widenInterval_def]);
val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtraction",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr)
......@@ -337,7 +343,7 @@ val validErrorboundCorrectSubtraction = store_thm ("validErrorboundCorrectSubtra
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [validIntervalSub_def, contained_def] interval_subtraction_valid)
\\ fs[contained_def]);
\\ fs[contained_def, widenInterval_def]);
val multiplicationErroBounded = store_thm ("multiplicationErrorBounded",
``!(nR1 nR2 nF1 nF2: real) (err1 err2: real) (e1lo e1hi e2lo e2hi: real).
......@@ -985,7 +991,7 @@ val validErrorboundCorrectMult = store_thm ("validErrorboundCorrectMult",
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ assume_tac (REWRITE_RULE [contained_def] interval_multiplication_valid)
\\ fs[contained_def]);
\\ fs[contained_def, widenInterval_def]);
val divisionErrorBounded = store_thm (
"divisionErrorBounded",
......@@ -2092,13 +2098,14 @@ val validErrorboundCorrectDiv = store_thm ("validErrorboundCorrectDiv",
\\ qexists_tac `nR2` \\ conj_tac
\\ simp[contained_def])
\\ irule REAL_LE_ADD2 \\ conj_tac
>- (irule divisionErrorBounded \\ fs[])
>- (irule (REWRITE_RULE [IVlo_def, IVhi_def, widenInterval_def, invertInterval_def] divisionErrorBounded)
\\ fs[widenInterval_def])
\\ qmatch_abbrev_tac `_ <= computeError (maxAbs iv) _`
\\ PairCases_on `iv` \\ irule computeError_up
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ match_mp_tac maxAbs
\\ assume_tac (REWRITE_RULE [contained_def] interval_division_valid)
\\ fs[contained_def, noDivzero_def]);
\\ fs[contained_def, widenInterval_def, noDivzero_def]);
val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
``!(E1 E2:env) (A:analysisResult) (e1:real expr) (e2:real expr) (e3: real expr)
......@@ -2176,7 +2183,7 @@ val validErrorboundCorrectFma = store_thm ("validErrorboundCorrectFma",
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ match_mp_tac maxAbs
\\ assume_tac (REWRITE_RULE [validIntervalAdd_def, contained_def] interval_addition_valid)
\\ fs[contained_def, IVlo_def, IVhi_def, noDivzero_def]);
\\ fs[contained_def, widenInterval_def, IVlo_def, IVhi_def, noDivzero_def]);
val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding",
``!(E1 E2:env) (A:analysisResult) (e:real expr)
......@@ -2207,8 +2214,10 @@ val validErrorboundCorrectRounding = store_thm ("validErrorboundCorrectRounding"
\\ unabbrev_all_tac \\ fs[maxAbs_def]
\\ match_mp_tac maxAbs
\\ assume_tac (REWRITE_RULE [contained_def] distance_gives_iv)
\\ fs[] \\ first_x_assum irule
\\ find_exists_tac \\ fs[]);
\\ fs[widenInterval_def]
\\ res_tac
\\ ntac 2 (first_x_assum (qspec_then `(elo, ehi)` assume_tac))
\\ rpt (first_x_assum (destruct) \\ fs[]));
(**
Soundness theorem for the error bound validator.
......@@ -2381,7 +2390,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ TRY (irule Binop_dist'
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `v1`, `v2`]
\\ fs[perturb_def, mTypeToR_pos])
\\ simp[Once validErrorbound_def])
\\ simp[Once validErrorbound_def, widenInterval_def, invertInterval_def])
>- (rename1 `Fma e1 e2 e3` \\ fs[]
\\ Flover_compute ``validErrorbound``
\\ rveq \\ fs[toREval_def]
......@@ -2493,7 +2502,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ irule Fma_dist'
\\ qexistsl_tac [`0`, `REAL`, `REAL`, `REAL`, `REAL`, `nR1`, `nR2`, `nR3`]
\\ fs[perturb_def, mTypeToR_pos])
\\ once_rewrite_tac [validErrorbound_def] \\ fs[])
\\ once_rewrite_tac [validErrorbound_def] \\ fs[widenInterval_def])
>- (rename1 `Downcast m1 e1` \\ fs[]
\\ Flover_compute ``validErrorbound``
\\ rveq \\ fs[toREval_def]
......@@ -2533,7 +2542,7 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ fs[]
\\ rpt conj_tac
>- (first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (once_rewrite_tac [validErrorbound_def] \\ fs[])
>- (once_rewrite_tac [validErrorbound_def] \\ fs[widenInterval_def])
\\ irule Downcast_dist' \\ fs[updDefVars_def]
\\ find_exists_tac \\ fs[]
\\ qexistsl_tac [`delta`, `v1`]
......
......@@ -251,7 +251,7 @@ val binary_unfolding = store_thm("binary_unfolding",
(Binop b (Var 1) (Var 2)) (perturb (evalBinop b v1 v2) m delta) m``,
fs [updEnv_def,updDefVars_def,join_fl_def,eval_expr_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'` \\ fs[]
\\ qexists_tac `delta` \\ fs[]
\\ IMP_RES_TAC Gamma_det \\ fs[]);
val fma_unfolding = store_thm("fma_unfolding",
......@@ -268,7 +268,7 @@ val fma_unfolding = store_thm("fma_unfolding",
(Fma (Var 1) (Var 2) (Var 3)) (perturb (evalFma v1 v2 v3) m delta) m``,
fs [updEnv_def,updDefVars_def,join_fl3_def,join_fl_def,eval_expr_cases,APPLY_UPDATE_THM,PULL_EXISTS]
\\ rpt strip_tac
\\ qexists_tac `delta'` \\ fs[]
\\ qexists_tac `delta` \\ fs[]
\\ IMP_RES_TAC Gamma_det \\ fs[]);
val eval_eq_env = store_thm (
......@@ -280,17 +280,17 @@ val eval_eq_env = store_thm (
Induct \\ rpt strip_tac \\ fs[eval_expr_cases]
>- (`E1 n = E2 n` by (first_x_assum irule)
\\ fs[])
>- (qexists_tac `delta'` \\ fs[])
>- (qexists_tac `delta` \\ fs[])
>- (rveq \\ qexistsl_tac [`m'`, `v1`] \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexistsl_tac [`m'`, `v1`] \\ fs[]
\\ qexists_tac `delta'` \\ fs[]
\\ qexists_tac `delta` \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`]
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta`]
\\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[])
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta'`]
>- (rveq \\ qexistsl_tac [`m1`, `m2`, `m3`, `v1`, `v2`, `v3`, `delta`]
\\ fs[] \\ prove_tac [])
>- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[]
>- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta`] \\ fs[]
\\ first_x_assum drule \\ disch_then irule \\ fs[]));
val swap_Gamma_eval_expr = store_thm (
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic 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))
TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
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 \
cakeml/translator/ml_translatorLib \
cakeml/basis/basis_ffiLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
$(HOLHEAP): $(DEPS)
$(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
endif
#ifdef POLY
#HOLHEAP = heap
#EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
#all: $(HOLHEAP)
#
#THYFILES = $(patsubst %Script.sml,%Theory.uo,$(wildcard *.sml))
#TARGETS0 = $(patsubst %Theory.sml,,$(THYFILES))
#TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
#
#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 \
# cakeml/translator/ml_translatorLib \
# cakeml/basis/basis_ffiLib
#
#DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
#
#$(HOLHEAP): $(DEPS)
# $(protect $(HOLDIR)/bin/buildheap) -o $(HOLHEAP) $(BARE_THYS)
#endif
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory;
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory RealArith;
open MachineTypeTheory ExpressionsTheory RealSimpsTheory FloverTactics
CertificateCheckerTheory FPRangeValidatorTheory IntervalValidationTheory
ExpressionAbbrevsTheory
......@@ -137,31 +137,61 @@ val Binop_to_Rop_def = Define `
| Mult => $*
| Div => $/ `;
Theorem real_div_pow:
! a n m. a <> 0 /\ n >= m ==> a pow n / a pow m = a pow (n - m)
Proof
Induct_on `n` \\ rpt strip_tac
>- (Cases_on `m` \\ fs[pow])
\\ fs[pow]
\\ Cases_on `m` \\ fs[pow]
\\ `n >= n'` by (fs[])
\\ res_tac
\\ first_x_assum (qspec_then `a` (fn thm => rewrite_tac[(GSYM thm)]))
\\ qspecl_then [`a`, `a pow n'`] destruct REAL_INV_MUL
>- (conj_tac \\ fs[]
\\ Cases_on `n'` \\ fs[pow, POW_ZERO_EQ])
\\ fs[real_div, REAL_MUL_ASSOC]
\\ `a * a pow n * inv a * inv (a pow n') = a * inv a * a pow n * inv (a pow n')`
by (REAL_ASM_ARITH_TAC)
\\ pop_assum (fn thm => once_rewrite_tac [thm])
\\ fs[REAL_MUL_RINV]
QED
val pow_simp1 = Q.prove (`2 pow 2047 / 2 pow 1023 = 2 pow 1024`,
qspecl_then [`2`, `2047`,`1023`] destruct real_div_pow \\ fs[]);
val pow_simp2 = Q.prove (`2 pow 2046 / 2 pow 1023 = 2 pow 1023`,
qspecl_then [`2`, `2046`,`1023`] destruct real_div_pow \\ fs[]);
val threshold_64_bit_lt_maxValue = store_thm ("threshold_64_bit_lt_maxValue",
``maxValue M64 < threshold (:52 # 11)``,
fs[threshold_def, maxValue_def, maxExponent_def]
rewrite_tac[threshold_def, maxValue_def, maxExponent_def, GSYM REAL_OF_NUM_POW]
\\ simp[pow_simp2]
\\ once_rewrite_tac [GSYM REAL_MUL_RID]
\\ once_rewrite_tac [GSYM REAL_MUL_ASSOC]
\\ irule REAL_LT_LMUL_IMP
\\ fs[]
\\ irule REAL_LT_LMUL_IMP \\ fs[]
\\ once_rewrite_tac [real_sub]
\\ once_rewrite_tac [GSYM REAL_LT_ADDNEG2]
\\ once_rewrite_tac [REAL_NEGNEG]
\\ once_rewrite_tac [RealArith.REAL_ARITH ``2:real = 1+1``]
\\ irule REAL_LT_IADD
\\ irule REAL_LT_IADD \\ fs[]
\\ once_rewrite_tac [GSYM REAL_INV1]
\\ irule REAL_LT_INV \\ fs[]);
\\ irule REAL_LT_INV \\ fs[]
\\ `1 = 2 pow 0` by (fs[pow])
\\ pop_assum (fn thm => once_rewrite_tac [thm])
\\ irule REAL_POW_MONO_LT \\ fs[]);
val normalValue_implies_normalization = store_thm ("validFloatValue_implies_normalization",
``!v.
normal v M64 ==>
normalizes (:52 #11) v``,
rpt strip_tac
\\ fs[normal_def, normalizes_def, wordsTheory.INT_MAX_def, minValue_pos_def,
minExponentPos_def, wordsTheory.INT_MIN_def, wordsTheory.dimindex_11,
rewrite_tac[normal_def, minValue_pos_def, maxValue_def, GSYM REAL_OF_NUM_POW]
\\ rpt strip_tac
\\ fs[normalizes_def, wordsTheory.INT_MAX_def, minExponentPos_def,
wordsTheory.INT_MIN_def, wordsTheory.dimindex_11,
wordsTheory.UINT_MAX_def, wordsTheory.dimword_11]
\\ irule REAL_LET_TRANS
\\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue]);
\\ qexists_tac `maxValue M64` \\ fs[threshold_64_bit_lt_maxValue, GSYM REAL_OF_NUM_POW, maxValue_def]);
val normalValue_implies_finiteness = store_thm ("normalValue_implies_finiteness",
``!v.
......@@ -200,65 +230,64 @@ val normal_value_is_float_value = store_thm (
\\ rewrite_tac[float_value_def]
\\ rw_thm_asm `normal _ _` normal_def
\\ fs[float_to_real_def]
\\ every_case_tac \\ fs[maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def]
>-( Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[]
\\ Cases_on `n'` \\ fs[])
>- (Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[]
\\ TRY (Cases_on `n'` \\ fs[])
\\ Cases_on `ff.Significand` \\ fs[]
\\ Cases_on `n` \\ fs[]
\\ qpat_x_assum `abs _ <= _` MP_TAC
\\ qmatch_abbrev_tac `abs (cst1 * cst2) <= cst3 ==> _`
\\ strip_tac
>- (`abs (cst1 * cst2) = cst1 * cst2`
by (once_rewrite_tac[ABS_REFL]
\\ irule REAL_LE_MUL \\ rpt conj_tac
\\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
\\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
\\ fs[]
\\ irule REAL_LE_ADD \\ fs[]
\\ irule REAL_LE_MUL \\ fs[]
\\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
\\ rw_asm_star `abs _ = _`
\\ `cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
\\ irule REAL_LE_TRANS
\\ qexists_tac `cst1 * cst2` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
\\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1:real = cst1 * 1``]
\\ once_rewrite_tac [RealArith.REAL_ARITH ``cst1 * cst2 * 1 = cst1 * cst2:real``]
\\ irule REAL_LE_LMUL_IMP
\\ unabbrev_all_tac \\ fs[]
\\ once_rewrite_tac [REAL_LE_ADDR]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[])
\\ `abs (cst1 * cst2) = -(cst1 * cst2)`
by (once_rewrite_tac[abs]
\\ `~ (0 <= cst1 * cst2)` suffices_by (fs[] )
\\ unabbrev_all_tac
\\ once_rewrite_tac [REAL_MUL_LNEG]
\\ fs[]
\\ qmatch_abbrev_tac `~ (cst1 * cst2 <= 0:real)`
\\ once_rewrite_tac [REAL_NOT_LE]
\\ irule REAL_LT_MUL \\ conj_tac
\\ TRY (unabbrev_all_tac \\ fs[]\\FAIL_TAC "")
\\ unabbrev_all_tac \\ once_rewrite_tac [real_div]
\\ irule REAL_LT_ADD \\ fs[]
\\ irule REAL_LT_MUL \\ fs[]
\\ once_rewrite_tac [REAL_INV_1OVER] \\ fs[])
\\ rw_asm_star `abs _ = _`
\\ `- cst1 <= cst3` suffices_by (unabbrev_all_tac \\ fs[])
\\ irule REAL_LE_TRANS
\\ qexists_tac `- (cst1 * cst2)` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
\\ once_rewrite_tac [RealArith.REAL_ARITH ``-cst1:real = -cst1 * 1``]
\\ once_rewrite_tac [RealArith.REAL_ARITH ``- (cst1 * cst2) * 1 = - cst1 * cst2:real``]
\\ irule REAL_LE_LMUL_IMP
\\ unabbrev_all_tac \\ fs[]
\\ once_rewrite_tac [REAL_LE_ADDR]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[]));
\\ every_case_tac
\\ fs [maxValue_def, maxExponent_def, minValue_pos_def, minExponentPos_def, GSYM REAL_OF_NUM_POW, pow_simp1, REAL_DIV_LZERO]
>-(Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[pow]
>- (fs[GSYM POW_ABS, abs, REAL_OF_NUM_POW])
\\ Cases_on `n'` \\ fs[pow,REAL_ABS_MUL, abs, REAL_OF_NUM_POW])
\\ qpat_x_assum `abs _ <= _` MP_TAC
\\ qmatch_abbrev_tac `abs (cst1 * cst2) <= cst3 ==> _`
\\ strip_tac
\\ Cases_on `ff.Sign` \\ fs[]
\\ Cases_on `n` \\ fs[pow]
>- (unabbrev_all_tac
\\ fs[ABS_MUL, GSYM POW_ABS]
\\ `abs 2 = 2` by (fs[abs]) \\ fs[]
\\ `abs (1 + &w2n ff.Significand / 2 pow 52) = 1 + &w2n ff.Significand / 2 pow 52`
by (rewrite_tac [ABS_REFL]
\\ irule REAL_LE_ADD \\ fs[])
\\ `2 pow 1024 <= 2 pow 1023`
by (irule REAL_LE_TRANS \\ find_exists_tac \\ fs[]
\\ rewrite_tac [REAL_LDISTRIB, REAL_MUL_RID]
\\ qabbrev_tac `res = 2 pow 1024 + 2 pow 1024 * (&w2n ff.Significand / 2 pow 52)`
\\ qspec_then `2 pow 1024` (fn thm => once_rewrite_tac [GSYM thm]) REAL_ADD_RID
\\ unabbrev_all_tac
\\ irule REAL_LE_LADD_IMP
\\ irule REAL_LE_MUL \\ fs[])
\\ fs[REAL_OF_NUM_POW])
\\ Cases_on `n'` \\ fs[]
\\ Cases_on `ff.Significand` \\ fs[]
\\ Cases_on `n` \\ fs[pow]
\\ `abs (cst1 * cst2) = -(cst1 * cst2)`
by (once_rewrite_tac[abs]
\\ `~ (0 <= cst1 * cst2)` suffices_by (fs[] )
\\ unabbrev_all_tac
\\ once_rewrite_tac [REAL_MUL_LNEG] \\ fs[]
\\ CCONTR_TAC \\ fs[REAL_LDISTRIB]
\\ `0 <= - (2 pow 1024)`
by (irule REAL_LE_TRANS \\ find_exists_tac \\ fs[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_ADD]
\\ qabbrev_tac `res = 2 pow 1024 + 2 pow 1024 * (&SUC n' / 2 pow 52)`
\\ qspec_then `2 pow 1024` (fn thm => once_rewrite_tac [GSYM thm]) REAL_ADD_RID
\\ unabbrev_all_tac
\\ irule REAL_LE_LADD_IMP
\\ irule REAL_LE_MUL \\ fs[])
\\ fs[REAL_OF_NUM_POW])
\\ rw_asm_star `abs _ = _`
\\ `- cst1 <= cst3`
suffices_by (unabbrev_all_tac \\ fs[REAL_NEG_LMUL, REAL_NEGNEG, REAL_OF_NUM_POW])
\\ irule REAL_LE_TRANS
\\ qexists_tac `- (cst1 * cst2)` \\ conj_tac \\ TRY (unabbrev_all_tac \\ fs[]\\ FAIL_TAC "")
\\ once_rewrite_tac [RealArith.REAL_ARITH ``-cst1:real = -cst1 * 1``]
\\ once_rewrite_tac [RealArith.REAL_ARITH ``- (cst1 * cst2) * 1 = - cst1 * cst2:real``]
\\ irule REAL_LE_LMUL_IMP
\\ unabbrev_all_tac \\ fs[]
\\ once_rewrite_tac [REAL_LE_ADDR]
\\ conj_tac
>- (once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ once_rewrite_tac[ REAL_INV_1OVER] \\ fs[])
\\ fs[GSYM REAL_NEG_MINUS1]);
val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
``!ff:(52,11) float.
......@@ -267,54 +296,58 @@ val denormal_value_is_float_value = store_thm ("denormal_value_is_float_value",
rpt strip_tac
\\rewrite_tac[float_value_def]
\\rw_thm_asm `denormal _ _` denormal_def
\\ TOP_CASE_TAC
\\ fs[]
\\ TOP_CASE_TAC \\ fs[]
\\ rw_thm_asm `abs _ < _` float_to_real_def
\\ fs[]
\\ `ff.Exponent <> 0w` by fs[]
\\ fs[]
\\ `ff.Exponent <> 0w` by fs[] \\ fs[]
\\ Cases_on `ff` \\ fs[]
\\ `w2n (-1w:word11) = 2047` by EVAL_TAC
\\ `w2n c0 = 2047` by fs[]
\\ fs[]
\\ `w2n (-1w:word11) = 2047` by EVAL_TAC
\\ `w2n c0 = 2047` by fs[] \\ fs[]
\\ TOP_CASE_TAC \\ fs[minValue_pos_def, minExponentPos_def]
\\ fs[REAL_ABS_MUL, POW_M1]
>- (`44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <= inv 1`
by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
\\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
\\ fs[REAL_INV1])
>- (Cases_on `c1` \\ fs[]
\\ `1 < abs (1 + &n / 4503599627370496)`
by (fs[abs]
\\ `0:real <= 1 + &n / 4503599627370496`
by (irule REAL_LE_TRANS
\\ qexists_tac `1` \\ fs[]
\\ once_rewrite_tac [GSYM REAL_ADD_RID]
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ irule REAL_LE_LADD_IMP
\\ fs[REAL_ADD_RID, real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[]
by (irule REAL_LTE_TRANS \\ asm_exists_tac \\ fs[])
\\ fs[REAL_INV1])
\\ Cases_on `c1` \\ fs[]
\\ `1 < abs (1 + &n / 4503599627370496)`
by (fs[abs]
\\ `0:real <= 1 + &n / 4503599627370496`
by (irule REAL_LE_TRANS
\\ qexists_tac `1` \\ fs[]
\\ once_rewrite_tac [GSYM REAL_ADD_RID]
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ irule REAL_LT_IADD
\\ irule REAL_LE_LADD_IMP
\\ fs[REAL_ADD_RID, real_div]
\\ irule REAL_LT_MUL \\ fs[]
\\ irule REAL_INV_POS \\ fs[])
\\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <= inv 1`
by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[]
\\ once_rewrite_tac [GSYM REAL_ADD_RID]
\\ once_rewrite_tac [GSYM REAL_ADD_ASSOC]
\\ irule REAL_LT_IADD
\\ fs[REAL_ADD_RID, real_div]
\\ irule REAL_LT_MUL \\ fs[]
\\ irule REAL_INV_POS \\ fs[])
\\ `44942328371557897693232629769725618340449424473557664318357520289433168951375240783177119330601884005280028469967848339414697442203604155623211857659868531094441973356216371319075554900311523529863270738021251442209537670585615720368478277635206809290837627671146574559986811484619929076208839082406056034304⁻¹ <= inv 1`
by (irule REAL_INV_LE_ANTIMONO_IMPR \\ fs[])
\\ fs[pow_simp1, REAL_DIV_LZERO, ABS_1, REAL_OF_NUM_POW, abs]
\\ `179769313486231590772930519078902473361797697894230657273430081157732675805500963132708477322407536021120113879871393357658789768814416622492847430639474124377767893424865485276302219601246094119453082952085005768838150682342462881473913110540827237163350510684586298239947245938479716304835356329624224137216 < inv 1`
by (irule REAL_LTE_TRANS \\ once_rewrite_tac[CONJ_COMM] \\ asm_exists_tac \\ fs[]
\\ qmatch_goalsub_abbrev_tac `cst1 < cst2`
\\ irule REAL_LT_TRANS \\ qexists_tac `cst1 * abs (1 + &n / 4503599627370496)`
\\ `0 <= (1:real) + &n / 4503599627370496`
by (irule REAL_LE_ADD \\ fs[real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[]
\\ irule REAL_LT_TRANS \\ qexists_tac `cst1 * (1 + &n / 4503599627370496)`
\\ fs[]
\\ once_rewrite_tac [GSYM REAL_MUL_RID]
\\ once_rewrite_tac [GSYM REAL_MUL_ASSOC] \\ irule REAL_LT_LMUL_IMP
\\ fs[]
\\ unabbrev_all_tac \\ fs[])
\\ fs[REAL_INV1]));
\\ fs[REAL_INV1]);
val validValue_gives_float_value = store_thm ("validValue_gives_float_value",
``!ff:(52,11) float.
......@@ -424,7 +457,9 @@ val float_to_real_real_to_float_zero_id = store_thm ("float_to_real_real_to_floa
once_rewrite_tac[real_to_float_def]
\\ `float_round roundTiesToEven F 0 = (float_plus_zero(:α#β))`
by (irule round_roundTiesToEven_is_plus_zero
\\ fs[ulp_def, ULP_def])
\\ fs[ulp_def, ULP_def, real_div]
\\ irule REAL_LE_MUL \\ fs[pow]
\\ irule REAL_LE_INV \\ irule POW_POS \\ fs[])
\\ fs[float_to_real_def, float_plus_zero_def]);
val div_eq0_general = store_thm ("div_eq0_general",
......@@ -766,9 +801,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[ulp_def, ULP_def])
\\ fs[float_to_real_round_zero_is_zero]
\\ qexists_tac `0` \\ fs[])
by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[float_to_real_round_zero_is_zero])
(* Subtraction, normal value *)
>- (fs[fp64_sub_def, fp64_to_float_float_to_fp64, evalBinop_def]
\\ `normal (evalBinop Sub (float_to_real (fp64_to_float vF1))
......@@ -812,7 +849,10 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ fs[perturb_def, mTypeToR_pos, evalBinop_def]
\\ fs[validValue_gives_float_value, float_round_with_flags_def]
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[ulp_def, ULP_def])
by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs[ float_to_real_round_zero_is_zero])
(* Multiplication *)
>- (fs[fp64_mul_def, fp64_to_float_float_to_fp64, evalBinop_def]
......@@ -856,8 +896,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ fs[float_round_with_flags_def, dmode_def,
fp64_to_float_float_to_fp64, perturb_def]
\\ Cases_on `(fp64_to_float vF1).Sign (fp64_to_float vF2).Sign`
\\ `2 * abs (0:real) <= ulp (:52#11)`
by (fs[ulp_def, ULP_def])
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs [round_roundTiesToEven_is_plus_zero,
round_roundTiesToEven_is_minus_zero, zero_to_real]
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
......@@ -934,8 +977,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ fs[validValue_gives_float_value]
\\ simp [float_round_with_flags_def]
\\ Cases_on `(fp64_to_float vF1).Sign (fp64_to_float vF2).Sign`
\\ `2 * abs (0:real) <= ulp (:52#11)`
by (fs[ulp_def, ULP_def])
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs [round_roundTiesToEven_is_plus_zero,
round_roundTiesToEven_is_minus_zero, zero_to_real]
\\ rveq
......@@ -943,7 +989,7 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
by (fs[GSYM float_is_zero_to_real, float_is_zero_def])
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToR_pos])
\\ fs[perturb_def, mTypeToR_pos, float_to_real_round_zero_is_zero])
>- (fs[fp64_div_def, dmode_def, fp64_to_float_float_to_fp64,
float_div_def, evalBinop_def]
\\ `float_to_real (fp64_to_float vF1) = 0`
......@@ -954,8 +1000,11 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
\\ fs[validValue_gives_float_value]
\\ simp [float_round_with_flags_def]
\\ Cases_on `(fp64_to_float vF1).Sign (fp64_to_float vF2).Sign`
\\ `2 * abs (0:real) <= ulp (:52#11)`
by (fs[ulp_def, ULP_def])
\\ `2 * abs (0:real) <= ulp (:52 #11)`
by (fs[REAL_ABS_0, ulp_def, ULP_def, REAL_OF_NUM_POW]
\\ once_rewrite_tac [real_div]
\\ irule REAL_LE_MUL \\ fs[]
\\ irule REAL_LE_INV \\ fs[])
\\ fs [round_roundTiesToEven_is_plus_zero,
round_roundTiesToEven_is_minus_zero, zero_to_real]
\\ rveq
......@@ -963,7 +1012,7 @@ val eval_expr_gives_IEEE = store_thm ("eval_expr_gives_IEEE",
by (fs[GSYM float_is_zero_to_real, float_is_zero_def])
\\ qexistsl_tac [`M64`, `M64`, `float_to_real (fp64_to_float vF1)`,
`float_to_real (fp64_to_float vF2)`, `0:real`]
\\ fs[perturb_def, mTypeToR_pos]))
\\ fs[perturb_def, mTypeToR_pos, float_to_real_round_zero_is_zero]))
>- (rename1 `Fma (toRExp e1) (toRExp e2) (toRExp e3)`
\\ IMP_RES_TAC validRanges_single
\\ rw_thm_asm `validTypes _ _` validTypes_def
......
......@@ -3,7 +3,7 @@
Used in soundness proofs for error bound validator.
**)
open realTheory realLib RealArith
open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
open AbbrevsTheory ExpressionsTheory RealSimpsTheory FloverTactics;
open preamble
val _ = new_theory "IntervalArith";
......@@ -81,15 +81,23 @@ invertInterval (iv:interval) = (1 /(IVhi iv), 1 /(IVlo iv))`;
val addInterval_def = Define `
addInterval (iv1:interval) (iv2:interval) = absIntvUpd (+) iv1 iv2`;
add_unevaluated_function ``addInterval``;
val subtractInterval_def = Define `
subtractInterval (iv1:interval) (iv2:interval) = addInterval iv1 (negateInterval iv2)`;
add_unevaluated_function ``subtractInterval``;
val multInterval_def = Define `
multInterval (iv1:interval) (iv2:interval) = absIntvUpd ( * ) iv1 iv2`;
add_unevaluated_function ``multInterval``;
val divideInterval_def = Define `
divideInterval iv1 iv2 = multInterval iv1 (invertInterval iv2)`;
add_unevaluated_function ``divideInterval``;
val minAbsFun_def = Define `
minAbsFun iv = min (abs (FST iv)) (abs (SND iv))`;
......
......@@ -131,7 +131,7 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
validTypes f Gamma ==>
validRanges f A E (toRTMap (toRExpMap Gamma))``,
Induct_on `f`
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac
\\ once_rewrite_tac [usedVars_def, toREval_def] \\ rpt strip_tac \\ rveq
\\ Flover_compute ``validIntervalbounds`` \\ rveq
(* Defined variable case *)
>- (rw_thm_asm `dVars_range_valid _ _ _` dVars_range_valid_def
......@@ -233,7 +233,8 @@ val validIntervalbounds_sound = store_thm ("validIntervalbounds_sound",
addInterval_def,
absIntvUpd_def,
contained_def] interval_addition_valid)
\\ fs[] \\ real_prove)
\\ fs[] \\ res_tac
\\ real_prove)
(* Sub case *)
>- (fs[evalBinop_def, isSupersetInterval_def, absIntvUpd_def,
subtractInterval_def, addInterval_def, negateInterval_def]
......@@ -426,18 +427,18 @@ val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[])
>- (`valid (invertInterval iv)`
by (irule iv_inv_preserves_valid \\ fs[])
\\ fs[valid_def, isSupersetInterval_def]
>- (irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[])
\\ find_exists_tac \\ fs[invertInterval_def])
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]
\\ irule REAL_LE_TRANS
\\ asm_exists_tac \\ fs[]))
\\ find_exists_tac \\ fs[invertInterval_def]))
>- (rename1 `Binop b f1 f2`
\\ rpt (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[])
\\ rveq \\ fs[]
......
Subproject commit c158f1ade07e9eb7d2db9fc7e8d9faff8156452f
Subproject commit 52270c049337b1915a61c946c535e43a0d2084b5
......@@ -27,7 +27,7 @@ val getConst_def = Define `
getConst (c:char) = ORD c - 48`;
val lexConst_def = Define`
lexConst (input:tvarN) (akk:num) =
lexConst (input:string) (akk:num) =
case input of
| STRING char input' =>
if (isDigit char)
......@@ -36,7 +36,7 @@ val lexConst_def = Define`
|"" => (akk, input)`;
val lexName_def = Define `