diff --git a/thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy b/thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy --- a/thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy +++ b/thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy @@ -1,548 +1,548 @@ theory Inca_to_Ubx_compiler imports Inca_to_Ubx_simulation Result "VeriComp.Compiler" "HOL-Library.Monad_Syntax" begin section \Generic program rewriting\ context fixes rewrite_instr :: "nat \ 'a \ 'stack \ ('err, 'b \ 'stack) result" begin fun rewrite_prog :: "nat \ 'a list \ 'stack \ ('err, 'b list \ 'stack) result" where "rewrite_prog _ [] \ = Ok ([], \)" | "rewrite_prog n (x # xs) \ = do { (x', \') \ rewrite_instr n x \; (xs', \'') \ rewrite_prog (Suc n) xs \'; Ok (x' # xs', \'') }" lemma rewrite_prog_map_f: assumes "\x \1 n x' \2. rewrite_instr n x \1 = Ok (x', \2) \ f x' = x" shows "rewrite_prog n xs \1 = Ok (ys, \2) \ map f ys = xs" by (induction xs arbitrary: \1 n ys; auto simp: assms) end fun gen_pop_push where "gen_pop_push instr (domain, codomain) \ = ( let ar = length domain in if ar \ length \ \ take ar \ = domain then Ok (instr, codomain # drop ar \) else Error () )" context inca_to_ubx_simulation begin lemma sp_rewrite_prog: assumes "rewrite_prog f n p1 \1 = Ok (p2, \2)" and "\x \1 n x' \2. f n x \1 = Ok (x', \2) \ Subx.sp_instr F x' \1 = Ok \2" shows "Subx.sp F p2 \1 = Ok \2" using assms(1) by (induction p1 arbitrary: \1 n p2; auto simp: assms(2)) section \Lifting\ context fixes get_arity :: "'fun \ nat option" and load_oracle :: "nat \ type option" begin fun lift_instr where "lift_instr (Inca.IPush x) \ = Ok (IPush x, None # \)" | "lift_instr Inca.IPop (_ # \) = Ok (IPop, \)" | "lift_instr (Inca.ILoad x) (None # \) = Ok (ILoad x, None # \)" | "lift_instr (Inca.IStore x) (None # None # \) = Ok (IStore x, \)" | "lift_instr (Inca.IOp op) \ = gen_pop_push (IOp op) (replicate (\\\\\ op) None, None) \" | "lift_instr (Inca.IOpInl opinl) \ = gen_pop_push (IOpInl opinl) (replicate (\\\\\ (\
\\\\ opinl)) None, None) \" | "lift_instr (Inca.ICall f) \ = do { ar \ Result.of_option () (get_arity f); gen_pop_push (ICall f) (replicate ar None, None) \ }" | "lift_instr _ _ = Error ()" definition lift where "lift = rewrite_prog (\_. lift_instr)" lemma sp_lift_instr: assumes "lift_instr instr \1 = Ok (instr', \2)" and "\x. rel_option (\ar fd. arity fd = ar) (get_arity x) (F x)" shows "Subx.sp_instr F instr' \1 = Ok \2" using assms(1) proof (induction instr \1 rule: lift_instr.induct) fix f \ n assume "lift_instr (Inca.ICall f) \ = Ok (instr', \2)" thus "Subx.sp_instr F instr' \ = Ok \2" using assms(2)[of f] by (auto simp: option_rel_Some1) qed (auto simp add: Let_def) lemma sp_lift: assumes "lift n p1 \1 = Ok (p2, \2)" and "\x. rel_option (\ar fd. arity fd = ar) (get_arity x) (F x)" shows "Subx.sp F p2 \1 = Ok \2" using assms by (auto elim!: sp_rewrite_prog sp_lift_instr simp: lift_def) lemma norm_lift_instr: "lift_instr x \1 = Ok (x', \2) \ norm_instr x' = x" by (induction x \1 rule: lift_instr.induct; auto simp: Let_def ) lemma norm_lift: assumes "lift n xs \1 = Ok (ys, \2)" shows "map norm_instr ys = xs" by (auto intro!: rewrite_prog_map_f[OF _ assms[unfolded lift_def]] simp: norm_lift_instr) section \Optimization\ fun result_alternative :: "('a, 'b) result \ ('a, 'b) result \ ('a, 'b) result" (infixr "<|>" 51) where "result_alternative (Ok x) _ = Ok x" | "result_alternative _ (Ok x) = Ok x" | "result_alternative (Error e) _ = Error e" definition try_unbox where "try_unbox \ x \ unbox mk_instr \ (case unbox x of Some n \ Ok (mk_instr n, Some \ # \) | None \ Error ())" fun optim_instr where "optim_instr _ (IPush d) \ = - try_unbox Num d \ unbox_num IPushNumUbx <|> - try_unbox Bool d \ unbox_bool IPushBoolUbx <|> + try_unbox Ubx1 d \ unbox_ubx1 IPushUbx1 <|> + try_unbox Ubx2 d \ unbox_ubx2 IPushUbx2 <|> Ok (IPush d, None # \) " | - "optim_instr _ (IPushNumUbx n) \ = Ok (IPushNumUbx n, Some Num # \)" | - "optim_instr _ (IPushBoolUbx b) \ = Ok (IPushBoolUbx b, Some Bool # \)" | + "optim_instr _ (IPushUbx1 n) \ = Ok (IPushUbx1 n, Some Ubx1 # \)" | + "optim_instr _ (IPushUbx2 b) \ = Ok (IPushUbx2 b, Some Ubx2 # \)" | "optim_instr _ IPop (_ # \) = Ok (IPop, \)" | "optim_instr n (ILoad x) (None # \) = ( case load_oracle n of Some \ \ Ok (ILoadUbx \ x, Some \ # \) | _ \ Ok (ILoad x, None # \) )" | "optim_instr _ (ILoadUbx \ x) (None # \) = Ok (ILoadUbx \ x, Some \ # \)" | "optim_instr _ (IStore x) (None # None # \) = Ok (IStore x, \)" | "optim_instr _ (IStoreUbx \\<^sub>1 x) (None # Some \\<^sub>2 # \) = (if \\<^sub>1 = \\<^sub>2 then Ok (IStoreUbx \\<^sub>1 x, \) else Error ())" | "optim_instr _ (IOp op) \ = gen_pop_push (IOp op) (replicate (\\\\\ op) None, None) \" | "optim_instr _ (IOpInl opinl) \ = ( let ar = \\\\\ (\
\\\\ opinl) in if ar \ length \ then case \\\ opinl (take ar \) of None \ gen_pop_push (IOpInl opinl) (replicate ar None, None) \ | Some opubx \ Ok (IOpUbx opubx, snd (\\\\\\\\ opubx) # drop ar \) else Error () )" | "optim_instr _ (IOpUbx opubx) \ = gen_pop_push (IOpUbx opubx) (\\\\\\\\ opubx) \" | "optim_instr _ (ICall f) \ = do { ar \ Result.of_option () (get_arity f); gen_pop_push (ICall f) (replicate ar None, None) \ }" | "optim_instr _ _ _ = Error ()" definition optim where "optim \ rewrite_prog optim_instr" lemma norm_optim_instr: "optim_instr n x \1 = Ok (x', \2) \ norm_instr x' = norm_instr x" for x \1 n x' \2 proof (induction n x \1 rule: optim_instr.induct) fix d \1 n assume "optim_instr n (Ubx.IPush d) \1 = Ok (x', \2)" thus "norm_instr x' = norm_instr (Ubx.instr.IPush d)" - using Subx.box_unbox_inverse_num Subx.box_unbox_inverse_bool + using Subx.box_unbox_inverse by (auto elim!: result_alternative.elims simp: try_unbox_def option.case_eq_if) next fix x \1 n assume assms: "optim_instr n (Ubx.ILoad x) (None # \1) = Ok (x', \2)" thus "norm_instr x' = norm_instr (Ubx.ILoad x)" proof (cases "load_oracle n") case None then show ?thesis using assms by simp next case (Some x) then show ?thesis using assms by (cases x) auto qed next fix opinl \1 n assume assms: "optim_instr n (IOpInl opinl) \1 = Ok (x', \2)" then have arity_le_\1: "\\\\\ (\
\\\\ opinl) \ length \1" using prod.inject by fastforce show "norm_instr x' = norm_instr (IOpInl opinl)" proof (cases "\\\ opinl (take (\\\\\ (\
\\\\ opinl)) \1)") case None then show ?thesis using assms arity_le_\1 by (simp add: Let_def) next case (Some opubx) then show ?thesis using assms arity_le_\1 by (auto simp: case_prod_beta Subx.\\\_invertible) qed next fix opubx \1 n assume assms: "optim_instr n (IOpUbx opubx) \1 = Ok (x', \2)" then show "norm_instr x' = norm_instr (IOpUbx opubx)" by (cases "\\\\\\\\ opubx"; auto simp: Let_def) qed (auto simp: Let_def) lemma norm_optim: assumes "optim n xs \1 = Ok (ys, \2)" shows "map norm_instr ys = map norm_instr xs" using assms unfolding optim_def by (induction xs arbitrary: \1 n ys \2; auto simp: norm_optim_instr) lemma sp_optim_instr: assumes "optim_instr n instr \1 = Ok (instr', \2)" and "\x. rel_option (\ar fd. arity fd = ar) (get_arity x) (F x) " shows "Subx.sp_instr F instr' \1 = Ok \2" using assms(1) apply (induction n instr \1 rule: optim_instr.induct; (auto simp: Let_def; fail)?) subgoal for _ d by (auto elim!: result_alternative.elims simp: try_unbox_def option.case_eq_if) subgoal for n by (cases "load_oracle n"; auto) subgoal for _ opinl \ apply (simp add: Let_def) apply (cases "\\\ opinl (take (\\\\\ (\
\\\\ opinl)) \)") apply (auto dest: list_all_eq_const_imp_replicate simp: case_prod_beta Let_def min.absorb2) subgoal for opubx using Subx.\\\\\\\\_\\\\\[of opubx] by (cases "\\\\\\\\ opubx"; auto simp: Subx.\\\_invertible dest: Subx.\\\_opubx_type) done subgoal for _ opubx by (cases "\\\\\\\\ opubx"; auto simp add: Let_def) subgoal for _ f using assms(2)[of f] by (auto simp: option_rel_Some1) done lemma sp_optim: assumes "optim n p1 \1 = Ok (p2, \2)" and "\x. rel_option (\ar fd. arity fd = ar) (get_arity x) (F x)" shows "Subx.sp F p2 \1 = Ok \2" using assms by (auto elim!: sp_rewrite_prog sp_optim_instr simp: optim_def) section \Compilation of function definition\ fun compile_fundef where "compile_fundef (Fundef instrs ar) = do { (xs, \\<^sub>1) \ lift 0 instrs (replicate ar None :: type option list); \ \Ensure that the function returns a single dynamic result\ () \ if \\<^sub>1 = [None] then Ok () else Error (); (ys, \\<^sub>2) \ optim 0 xs (replicate ar None); Ok (Fundef ( if \\<^sub>2 = [None] then ys \ \use optimization\ else xs \ \cancel optimization\ ) ar) }" lemma rel_compile_fundef: assumes "compile_fundef fd1 = Ok fd2" shows "rel_fundef norm_eq fd1 fd2" proof (cases fd1) case (Fundef xs ar) obtain ys zs \2 where lift_xs: "lift 0 xs (replicate ar None :: type option list) = Ok (ys, [None])" and optim_ys: "optim 0 ys (replicate ar None :: type option list) = Ok (zs, \2)" and check: "fd2 = Fundef (if \2 = [None] then zs else ys) ar" using assms unfolding Fundef unfolding compile_fundef.simps by (auto simp: Nitpick.case_unit_unfold if_then_else_distributive) then have "map norm_instr ys = xs" by (auto intro: norm_lift) show ?thesis proof (cases "\2 = [None]") case True then show ?thesis using True Fundef using check norm_lift[OF lift_xs, symmetric] using norm_optim[OF optim_ys, symmetric] by (simp add: list.rel_map list.rel_refl) next case False then show ?thesis using Fundef check norm_lift[OF lift_xs, symmetric] by (simp add: list.rel_map list.rel_refl) qed qed lemma sp_compile_fundef: assumes "compile_fundef fd1 = Ok fd2" and "\x. rel_option (\ar fd. arity fd = ar) (get_arity x) (F x)" shows "sp_fundef F fd2 (body fd2) = Ok [None]" proof (cases fd1) case (Fundef xs ar) with assms show ?thesis by (auto elim!: sp_optim sp_lift simp: sp_fundef_def Nitpick.case_unit_unfold if_eq_const_conv) qed end end locale inca_ubx_compiler = inca_to_ubx_simulation Finca_empty Finca_get for Finca_empty and Finca_get :: "_ \ 'fun \ _ option" + fixes load_oracle :: "'fun \ nat \ type option" begin section \Compilation of function environment\ definition compile_env_entry where "compile_env_entry \ \ x = map_result id (Pair (fst x)) (compile_fundef \ (\ (fst x)) (snd x))" lemma rel_compile_env_entry: assumes "compile_env_entry \ \ (f, fd1) = Ok (f, fd2)" shows "rel_fundef norm_eq fd1 fd2" using assms unfolding compile_env_entry_def using rel_compile_fundef by auto lemma sp_compile_env_entry: assumes "compile_env_entry \ \ (f, fd1) = Ok (f, fd2)" and "\x. rel_option (\ar fd. arity fd = ar) (\ x) (F x)" shows "sp_fundef F fd2 (body fd2) = Ok [None]" using assms unfolding compile_env_entry_def by (auto elim: sp_compile_fundef) definition compile_env where "compile_env \ \ e \ map_result id Subx.Fenv.from_list (Result.those (map (compile_env_entry \ \) (Finca_to_list e))) " lemma list_assoc_those_compile_env_entries: "Result.those (map (compile_env_entry \ \) xs) = Ok ys \ rel_option (\fd1 fd2. compile_fundef \ (\ f) fd1 = Ok fd2) (map_of xs f) (map_of ys f)" proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) then obtain y ys' where xs_def: "ys = y # ys'" and comp_x: "compile_env_entry \ \ x = Ok y" and comp_xs: "Result.those (map (compile_env_entry \ \) xs) = Ok ys'" by auto obtain g fd1 fd2 where prods: "x = (g, fd1)" "y = (g, fd2)" using comp_x by (cases x) (auto simp: compile_env_entry_def) have "compile_fundef \ (\ g) fd1 = Ok fd2" using comp_x unfolding prods compile_env_entry_def by auto then show ?case unfolding prods xs_def using Cons.IH[OF comp_xs] by simp qed lemma compile_env_rel_compile_fundef: assumes "compile_env \ \ F1 = Ok F2" shows "rel_option (\fd1 fd2. compile_fundef \ (\ f) fd1 = Ok fd2) (Finca_get F1 f) (Fubx_get F2 f)" proof - obtain xs where those_xs: "Result.those (map (compile_env_entry \ \) (Finca_to_list F1)) = Ok xs" using assms[unfolded compile_env_def] by auto hence F2_def: "F2 = Subx.Fenv.from_list xs" using assms[unfolded compile_env_def] by simp show ?thesis proof (cases "map_of (Finca_to_list F1) f") case None then show ?thesis unfolding F2_def Subx.Fenv.from_list_correct[symmetric] unfolding Sinca.Fenv.to_list_correct[symmetric] using list_assoc_those_compile_env_entries[OF those_xs, of f] by simp next case (Some fd1) then show ?thesis unfolding F2_def Subx.Fenv.from_list_correct[symmetric] unfolding Sinca.Fenv.to_list_correct[symmetric] using list_assoc_those_compile_env_entries[OF those_xs, of f] by simp qed qed lemma rel_those_compile_env_entries: "Result.those (map (compile_env_entry \ \) xs) = Ok ys \ rel_fundefs (Finca_get (Sinca.Fenv.from_list xs)) (Fubx_get (Subx.Fenv.from_list ys))" proof (induction xs arbitrary: ys) case Nil then show ?case using rel_fundefs_empty by simp next case (Cons x xs) then obtain y ys' where xs_def: "ys = y # ys'" and comp_x: "compile_env_entry \ \ x = Ok y" and comp_xs: "Result.those (map (compile_env_entry \ \) xs) = Ok ys'" by auto obtain f fd1 fd2 where prods: "x = (f, fd1)" "y = (f, fd2)" using comp_x by (cases x) (auto simp: compile_env_entry_def) have "rel_fundef norm_eq fd1 fd2" using rel_compile_env_entry[OF comp_x[unfolded prods]] . then show ?case unfolding prods xs_def unfolding Sinca.Fenv.from_list_correct[symmetric] Subx.Fenv.from_list_correct[symmetric] unfolding rel_fundefs_def apply auto using Cons.IH[OF comp_xs] unfolding Sinca.Fenv.from_list_correct[symmetric] Subx.Fenv.from_list_correct[symmetric] by (simp add: rel_fundefs_def) qed lemma rel_fundefs_compile_env: assumes "compile_env \ \ e = Ok e'" shows "rel_fundefs (Finca_get e) (Fubx_get e')" proof - obtain xs where FOO: "Result.those (map (compile_env_entry \ \) (Finca_to_list e)) = Ok xs" and BAR: "e' = Subx.Fenv.from_list xs" using assms by (auto simp: compile_env_def) show ?thesis using rel_those_compile_env_entries[OF FOO] unfolding BAR unfolding Sinca.Fenv.get_from_list_to_list . qed lemma sp_fundefs_compile_env: assumes "compile_env \ \ F1 = Ok F2" and "\x. rel_option (\ar fd. arity fd = ar) (\ x) (Finca_get F1 x)" shows "sp_fundefs (Fubx_get F2)" unfolding sp_fundefs_def proof (intro allI impI) fix f fd2 assume F2_f: "Fubx_get F2 f = Some fd2" then obtain fd1 where "Finca_get F1 f = Some fd1" and compile_fd1: "compile_fundef \ (\ f) fd1 = Ok fd2" using compile_env_rel_compile_fundef[OF assms(1), of f] by (auto simp: option_rel_Some2) note rel_F1_F2 = rel_fundefs_compile_env[OF assms(1)] have "rel_option (\ar fd. arity fd = ar) (\ f) (Fubx_get F2 f)" for f using assms(2)[of f] proof (cases rule: option.rel_cases) case None then show ?thesis using rel_fundefs_None1[OF rel_F1_F2] by simp next case (Some ar fd1) then obtain fd2 where "Fubx_get F2 f = Some fd2" and rel_fd1_fd2: "rel_fundef (\x y. x = norm_instr y) fd1 fd2" using rel_fundefs_Some1[OF rel_F1_F2] by (meson rel_fundefs_Some1) with Some show ?thesis by (simp add: rel_fundef_arities) qed thus "sp_fundef (Fubx_get F2) fd2 (body fd2) = Ok [None]" by (auto intro!: sp_compile_fundef[OF compile_fd1]) qed section \Compilation of program\ fun compile where "compile (Prog F H f) = Result.to_option (do { F' \ compile_env (map_option arity \ Finca_get F) load_oracle F; Ok (Prog F' H f) })" lemma compile_load: assumes compile_p1: "compile p1 = Some p2" and load: "Subx.load p2 s2" shows "\s1. Sinca.load p1 s1 \ match s1 s2" proof - obtain F1 H main where p1_def: "p1 = Prog F1 H main" by (cases p1) simp then obtain F2 where compile_F1: "compile_env (map_option arity \ Finca_get F1) load_oracle F1 = Ok F2" and p2_def: "p2 = Prog F2 H main" using compile_p1 by auto note rel_F1_F2 = rel_fundefs_compile_env[OF compile_F1] show ?thesis using assms(2) unfolding p2_def proof (cases _ s2 rule: Subx.load.cases) case (1 fd2) let ?s1 = "State F1 H [Frame main 0 []]" from 1 obtain fd1 where Fstd_main: "Finca_get F1 main = Some fd1" and "compile_fundef (map_option arity \ Finca_get F1) (load_oracle main) fd1 = Ok fd2" using compile_env_rel_compile_fundef[OF compile_F1, of main] by (auto simp: option_rel_Some2) with 1 have "arity fd1 = 0" using fundef.rel_sel rel_compile_fundef by metis hence "Sinca.load p1 ?s1" unfolding p1_def by (auto intro!: Sinca.load.intros[OF Fstd_main]) moreover have "?s1 \ s2" proof - have "sp_fundefs (Fubx_get F2)" by (auto intro: sp_fundefs_compile_env[OF compile_F1] simp: option.rel_map option.rel_refl) moreover have "rel_stacktraces (Fubx_get F2) [Frame main 0 []] [Frame main 0 []] None" using 1 by (auto intro!: rel_stacktraces.intros simp: sp_fundef_def) ultimately show ?thesis unfolding 1 using rel_F1_F2 by (auto intro!: match.intros) qed ultimately show ?thesis by auto qed qed interpretation std_to_inca_compiler: compiler Sinca.step Subx.step Sinca.final Subx.final Sinca.load Subx.load "\_ _. False" "\_. match" compile using compile_load by unfold_locales auto end end diff --git a/thys/Interpreter_Optimizations/Inca_to_Ubx_simulation.thy b/thys/Interpreter_Optimizations/Inca_to_Ubx_simulation.thy --- a/thys/Interpreter_Optimizations/Inca_to_Ubx_simulation.thy +++ b/thys/Interpreter_Optimizations/Inca_to_Ubx_simulation.thy @@ -1,1923 +1,1934 @@ theory Inca_to_Ubx_simulation imports List_util Option_applicative Result "VeriComp.Simulation" Inca Ubx Ubx_type_inference Unboxed_lemmas begin section \Locale imports\ locale inca_to_ubx_simulation = Sinca: inca Finca_empty Finca_get Finca_add Finca_to_list heap_empty heap_get heap_add heap_to_list is_true is_false \\ \\\\\ \\\\\ \\\ \\\\\ \
\\\\ + Subx: ubx_sp Fubx_empty Fubx_get Fubx_add Fubx_to_list heap_empty heap_get heap_add heap_to_list - is_true is_false box_num unbox_num box_bool unbox_bool + is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2 \\ \\\\\ \\\\\ \\\ \\\\\ \
\\\\ \\\\\ \\\ \\\ \\\\\\\\ for \ \Functions environments\ Finca_empty and Finca_get :: "'fenv_inca \ 'fun \ ('dyn, 'var, 'fun, 'op, 'opinl) Inca.instr fundef option" and Finca_add and Finca_to_list and Fubx_empty and - Fubx_get :: "'fenv_ubx \ 'fun \ ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx) Ubx.instr fundef option" and + Fubx_get :: "'fenv_ubx \ 'fun \ ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx, 'ubx1, 'ubx2) Ubx.instr fundef option" and Fubx_add and Fubx_to_list and \ \Memory heap\ heap_empty and heap_get :: "'henv \ 'var \ 'dyn \ 'dyn option" and heap_add and heap_to_list and \ \Unboxed values\ is_true and is_false and - box_num and unbox_num and - box_bool and unbox_bool and + box_ubx1 and unbox_ubx1 and + box_ubx2 and unbox_ubx2 and \ \n-ary operations\ \\ and \\\\\ and \\\\\ and \\\ and \\\\\ and \
\\\\ and \\\\\ and \\\ and \\\ and \\\\\\\\ begin declare Subx.sp_append[simp] section \Strongest postcondition\ definition sp_fundef where "sp_fundef F fd xs \ Subx.sp F xs (replicate (arity fd) None)" lemmas sp_fundef_generalize = Subx.sp_generalize[where \ = "replicate (arity fd) None" for fd, simplified, folded sp_fundef_def] lemma eq_sp_to_eq_sp_fundef: - assumes "Subx.sp F1 = (Subx.sp F2 :: ('dyn, 'id, _, _, _, _) Ubx.instr list \ _)" - shows "sp_fundef F1 = (sp_fundef F2 :: _ \ ('dyn, 'id, _, _, _, _) Ubx.instr list \ _)" + assumes "Subx.sp F1 = (Subx.sp F2 :: ('dyn, 'id, _, _, _, _, 'num, 'bool) Ubx.instr list \ _)" + shows "sp_fundef F1 = (sp_fundef F2 :: _ \ ('dyn, 'id, _, _, _, _, 'num, 'bool) Ubx.instr list \ _)" using assms(1) by (intro ext; simp add: sp_fundef_def) definition sp_fundefs where "sp_fundefs F \ \f fd. F f = Some fd \ sp_fundef F fd (body fd) = Ok [None]" section \Normalization\ fun norm_instr where "norm_instr (Ubx.IPush d) = Inca.IPush d" | - "norm_instr (Ubx.IPushNumUbx n) = Inca.IPush (box_num n)" | - "norm_instr (Ubx.IPushBoolUbx b) = Inca.IPush (box_bool b)" | + "norm_instr (Ubx.IPushUbx1 n) = Inca.IPush (box_ubx1 n)" | + "norm_instr (Ubx.IPushUbx2 b) = Inca.IPush (box_ubx2 b)" | "norm_instr Ubx.IPop = Inca.IPop" | "norm_instr (Ubx.ILoad x) = Inca.ILoad x" | "norm_instr (Ubx.ILoadUbx _ x) = Inca.ILoad x" | "norm_instr (Ubx.IStore x) = Inca.IStore x" | "norm_instr (Ubx.IStoreUbx _ x) = Inca.IStore x" | "norm_instr (Ubx.IOp op) = Inca.IOp op" | "norm_instr (Ubx.IOpInl op) = Inca.IOpInl op" | "norm_instr (Ubx.IOpUbx op) = Inca.IOpInl (\\\ op)" | "norm_instr (Ubx.ICJump n) = Inca.ICJump n" | "norm_instr (Ubx.ICall x) = Inca.ICall x" definition rel_fundefs where "rel_fundefs f g = (\x. rel_option (rel_fundef (\y z. y = norm_instr z)) (f x) (g x))" abbreviation (input) norm_eq where "norm_eq x y \ x = norm_instr y" lemma norm_generalize_instr: "norm_instr (Subx.generalize_instr instr) = norm_instr instr" by (cases instr) simp_all lemma rel_fundef_body_nth: assumes "rel_fundef norm_eq fd1 fd2" and "pc < length (body fd1)" shows "body fd1 ! pc = norm_instr (body fd2 ! pc)" using assms by (auto dest: list_all2_nthD simp: fundef.rel_sel) lemma rel_fundef_rewrite_body: assumes "rel_fundef norm_eq fd1 fd2" and "norm_instr (body fd2 ! pc) = norm_instr instr" shows "rel_fundef norm_eq fd1 (rewrite_fundef_body fd2 pc instr)" using assms(1) proof (cases rule: fundef.rel_cases) case (Fundef xs ar' ys ar) hence "length xs = length ys" by (simp add: list_all2_conv_all_nth) hence "length xs = length (rewrite ys pc instr)" by simp hence "list_all2 norm_eq xs (rewrite ys pc instr)" proof (elim list_all2_all_nthI) fix n assume "n < length xs" hence "n < length ys" by (simp add: \length xs = length ys\) thus "xs ! n = norm_instr (rewrite ys pc instr ! n)" using list_all2_nthD[OF \list_all2 norm_eq xs ys\ \n < length xs\, symmetric] using assms(2)[unfolded Fundef(2), simplified] by (cases "pc = n"; simp) qed thus ?thesis using Fundef by simp qed lemma rel_fundef_generalize: assumes "rel_fundef norm_eq fd1 fd2" shows "rel_fundef norm_eq fd1 (Subx.generalize_fundef fd2)" using assms(1) proof (cases rule: fundef.rel_cases) case (Fundef xs ar' ys ar) hence "list_all2 (\x y. x = norm_instr y) xs (map Subx.generalize_instr ys)" by (auto elim!: list_all2_mono simp: list.rel_map norm_generalize_instr) thus ?thesis using Fundef by simp qed lemma rel_fundefs_empty: "rel_fundefs (\_. None) (\_. None)" by (simp add: rel_fundefs_def) lemma rel_fundefs_None1: assumes "rel_fundefs f g" and "f x = None" shows "g x = None" by (metis assms rel_fundefs_def rel_option_None1) lemma rel_fundefs_None2: assumes "rel_fundefs f g" and "g x = None" shows "f x = None" by (metis assms rel_fundefs_def rel_option_None2) lemma rel_fundefs_Some1: assumes "rel_fundefs f g" and "f x = Some y" shows "\z. g x = Some z \ rel_fundef norm_eq y z" proof - from assms(1) have "rel_option (rel_fundef norm_eq) (f x) (g x)" unfolding rel_fundefs_def by simp with assms(2) show ?thesis by (simp add: option_rel_Some1) qed lemma rel_fundefs_Some2: assumes "rel_fundefs f g" and "g x = Some y" shows "\z. f x = Some z \ rel_fundef norm_eq z y" proof - from assms(1) have "rel_option (rel_fundef norm_eq) (f x) (g x)" unfolding rel_fundefs_def by simp with assms(2) show ?thesis by (simp add: option_rel_Some2) qed lemma rel_fundefs_rel_option: assumes "rel_fundefs f g" and "\x y. rel_fundef norm_eq x y \ h x y" shows "rel_option h (f z) (g z)" proof - have "rel_option (rel_fundef norm_eq) (f z) (g z)" using assms(1)[unfolded rel_fundefs_def] by simp then show ?thesis unfolding rel_option_unfold by (auto simp add: assms(2)) qed section \Equivalence of call stacks\ -definition norm_stack :: "'dyn unboxed list \ 'dyn list" where +definition norm_stack :: "('dyn, 'ubx1, 'ubx2) unboxed list \ 'dyn list" where "norm_stack \ \ List.map Subx.norm_unboxed \" lemma norm_stack_Nil[simp]: "norm_stack [] = []" by (simp add: norm_stack_def) lemma norm_stack_Cons[simp]: "norm_stack (d # \) = Subx.norm_unboxed d # norm_stack \" by (simp add: norm_stack_def) lemma norm_stack_append: "norm_stack (xs @ ys) = norm_stack xs @ norm_stack ys" by (simp add: norm_stack_def) lemmas drop_norm_stack = drop_map[where f = Subx.norm_unboxed, folded norm_stack_def] lemmas take_norm_stack = take_map[where f = Subx.norm_unboxed, folded norm_stack_def] lemmas norm_stack_map = map_map[where f = Subx.norm_unboxed, folded norm_stack_def] lemma norm_box_stack[simp]: "norm_stack (map Subx.box_operand \) = norm_stack \" by (induction \) (auto simp: norm_stack_def) lemma length_norm_stack[simp]: "length (norm_stack xs) = length xs" by (simp add: norm_stack_def) definition is_valid_fun_call where "is_valid_fun_call get fd2 n \2 g \ n < length (body fd2) \ body fd2 ! n = ICall g \ (\gd. get g = Some gd \ list_all is_dyn_operand (take (arity gd) \2))" inductive rel_stacktraces for get where rel_stacktraces_Nil: "rel_stacktraces get [] [] opt" | rel_stacktraces_Cons: "rel_stacktraces get st1 st2 (Some f) \ \1 = norm_stack \2 \ get f = Some fd2 \ sp_fundef get fd2 (take n (body fd2)) = Ok (map typeof \2) \ pred_option (is_valid_fun_call get fd2 n \2) opt \ rel_stacktraces get (Frame f n \1 # st1) (Frame f n \2 # st2) opt" definition all_same_arities where "all_same_arities F1 F2 \ \f. rel_option (\fd gd. arity fd = arity gd) (F1 f) (F2 f)" lemma all_same_arities_commutative: "all_same_arities F1 F2 = all_same_arities F2 F1" proof assume "all_same_arities F1 F2" then show "all_same_arities F2 F1" unfolding all_same_arities_def by (simp add: rel_option_unfold) next assume "all_same_arities F2 F1" then show "all_same_arities F1 F2" unfolding all_same_arities_def by (simp add: rel_option_unfold) qed lemma sp_instr_same_arities: "all_same_arities F1 F2 \ Subx.sp_instr F1 x ys = Subx.sp_instr F2 x ys" proof (induction F1 x ys rule: Subx.sp_instr.induct) fix F1 f \ assume assms: "all_same_arities F1 F2" show "Subx.sp_instr F1 (Ubx.ICall f) \ = Subx.sp_instr F2 (Ubx.ICall f) \" proof (cases "F1 f") case None then have "F2 f = None" using HOL.spec[OF assms[unfolded all_same_arities_def], of f] by simp with None show ?thesis by simp next case (Some a) then obtain b where "F2 f = Some b" and "arity a = arity b" using HOL.spec[OF assms[unfolded all_same_arities_def], of f] by (auto simp: option_rel_Some1) with Some show ?thesis by simp qed qed simp_all lemma sp_same_arities: assumes "all_same_arities F1 F2" shows "Subx.sp F1 = Subx.sp F2" proof (intro ext allI) fix xs ys show "Subx.sp F1 xs ys = Subx.sp F2 xs ys" proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) show ?case apply simp apply (cases "(F1, x, ys)" rule: Subx.sp_instr.cases; simp add: Cons.IH Let_def) subgoal for opubx apply (cases "\\\\\\\\ opubx") by (auto simp: Cons.IH Let_def) subgoal for f apply (rule option.rel_induct[of "(\fd gd. arity fd = arity gd)" "F1 f" "F2 f"]) using assms(1)[unfolded all_same_arities_def] by (auto simp add: Cons.IH) done qed qed lemmas sp_fundef_same_arities = sp_same_arities[THEN eq_sp_to_eq_sp_fundef] lemma all_same_arities_add: assumes "Fubx_get F f = Some fd1" and "arity fd1 = arity fd2" shows "all_same_arities (Fubx_get F) (Fubx_get (Fubx_add F f fd2))" unfolding all_same_arities_def proof (intro allI) fix g show "rel_option (\fd gd. arity fd = arity gd) (Fubx_get F g) (Fubx_get (Fubx_add F f fd2) g)" using assms by (cases "f = g") (simp_all add: option.rel_refl) qed lemma all_same_arities_generalize_fundef: assumes "Fubx_get F f = Some fd" shows "all_same_arities (Fubx_get F) (Fubx_get (Fubx_add F f (Subx.generalize_fundef fd)))" using all_same_arities_add[OF assms(1)] using ubx.arity_generalize_fundef by simp lemma rel_stacktraces_box: assumes "rel_stacktraces F1 xs ys opt" and "F2 f = map_option Subx.generalize_fundef (F1 f)" and "\g. f \ g \ F2 g = F1 g" and "all_same_arities F1 F2" shows "rel_stacktraces F2 xs (Subx.box_stack f ys) opt" using assms(1) proof (induction xs ys opt rule: rel_stacktraces.induct) case rel_stacktraces_Nil then show ?case by (auto intro: rel_stacktraces.intros) next case (rel_stacktraces_Cons st1 st2 g \1 \2 gd n opt) note sp_F1_eq_sp_F2[simp] = sp_same_arities[OF assms(4)] note sp_fundef_F1_eq_sp_fundef_F2[simp] = eq_sp_to_eq_sp_fundef[OF sp_F1_eq_sp_F2] show ?case apply simp proof (intro conjI impI) assume "f = g" then have get2_g: "F2 g = Some (Subx.generalize_fundef gd)" using assms(2) \F1 g = Some gd\ by simp show "rel_stacktraces F2 (Frame g n \1 # st1) (Frame g n (map Subx.box_operand \2) # Subx.box_stack g st2) opt" proof (intro rel_stacktraces.intros) show "rel_stacktraces F2 st1 (Subx.box_stack g st2) (Some g)" using rel_stacktraces_Cons.IH unfolding \f = g\ by simp next show "\1 = norm_stack (map Subx.box_operand \2)" using \\1 = norm_stack \2\ by simp next show "F2 g = Some (Subx.generalize_fundef gd)" using get2_g . next show "sp_fundef F2 (Subx.generalize_fundef gd) (take n (body (Subx.generalize_fundef gd))) = Ok (map typeof (map Subx.box_operand \2))" using sp_fundef_generalize[OF rel_stacktraces_Cons.hyps(4)] by (simp add: take_map sp_fundef_def) next show "pred_option (is_valid_fun_call F2 (Subx.generalize_fundef gd) n (map Subx.box_operand \2)) opt" proof (cases opt) case (Some h) then show ?thesis using rel_stacktraces_Cons.hyps(5) apply (simp add: take_map list.pred_map list.pred_True is_valid_fun_call_def) using \f = g\ assms(3) get2_g by fastforce qed simp qed next assume "f \ g" show "rel_stacktraces F2 (Frame g n \1 # st1) (Frame g n \2 # Subx.box_stack f st2) opt" using rel_stacktraces_Cons assms(3)[OF \f \ g\] apply (auto intro!: rel_stacktraces.intros; cases opt; simp add: sp_fundef_def is_valid_fun_call_def) subgoal for h using assms(2,3) by (cases "f = h"; auto) done qed qed lemma rel_stacktraces_generalize: assumes "rel_stacktraces (Fubx_get F) st1 st2 (Some f)" and "Fubx_get F f = Some fd " and sp_prefix: "sp_fundef (Fubx_get F) fd (take pc (body fd)) = Ok (None # map typeof \2)" and norm_stacks: "\1 = norm_stack \2" and pc_in_range: "pc < length (body fd)" and sp_instr: "Subx.sp_instr (Fubx_get F) (Subx.generalize_instr (body fd ! pc)) (None # map (\_. None) \2) = Ok (None # map (typeof \ Subx.box_operand) \2)" shows "rel_stacktraces (Fubx_get (Fubx_add F f (Subx.generalize_fundef fd))) (Frame f (Suc pc) (d # \1) # st1) (Frame f (Suc pc) (OpDyn d # map Subx.box_operand \2) # Subx.box_stack f st2) None" proof - let ?fd' = "Subx.generalize_fundef fd" let ?F' = "Fubx_add F f ?fd'" show ?thesis proof (intro rel_stacktraces_Cons) show "rel_stacktraces (Fubx_get ?F') st1 (Subx.box_stack f st2) (Some f)" using assms(2) all_same_arities_generalize_fundef by (auto intro: rel_stacktraces_box[OF assms(1)]) next show "d # \1 = norm_stack (OpDyn d # map Subx.box_operand \2)" using norm_stacks by simp next show "Fubx_get ?F' f = Some ?fd'" by simp next show "sp_fundef (Fubx_get ?F') ?fd' (take (Suc pc) (body ?fd')) = Ok (map typeof (OpDyn d # map Subx.box_operand \2))" unfolding all_same_arities_generalize_fundef[THEN sp_fundef_same_arities, OF assms(2), symmetric] using sp_fundef_generalize[OF sp_prefix] sp_instr by (auto simp add: sp_fundef_def take_map take_Suc_conv_app_nth[OF pc_in_range]) qed simp_all qed lemma rel_fundefs_rewrite: assumes rel_F1_F2: "rel_fundefs (Finca_get F1) (Fubx_get F2)" and F2_get_f: "Fubx_get F2 f = Some fd2" and F2_add_f: "Fubx_add F2 f (rewrite_fundef_body fd2 pc instr) = F2'" and eq_norm: "norm_instr (body fd2 ! pc) = norm_instr instr" shows "rel_fundefs (Finca_get F1) (Fubx_get F2')" unfolding rel_fundefs_def proof fix x show "rel_option (rel_fundef norm_eq) (Finca_get F1 x) (Fubx_get F2' x)" proof (cases "x = f") case True then have F2'_get_x: "Fubx_get F2' x = Some (rewrite_fundef_body fd2 pc instr)" using F2_add_f by auto obtain fd1 where "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_get_f] by auto thus ?thesis unfolding F2'_get_x option_rel_Some2 using True rel_fundef_rewrite_body[OF rel_fd1_fd2 eq_norm] by auto next case False then have "Fubx_get F2' x = Fubx_get F2 x" using F2_add_f by auto then show ?thesis using rel_F1_F2 rel_fundefs_def by fastforce qed qed lemma rel_fundef_rewrite_both: assumes "rel_fundef norm_eq fd1 fd2" and "norm_instr y = x" shows "rel_fundef norm_eq (rewrite_fundef_body fd1 pc x) (rewrite_fundef_body fd2 pc y)" using assms by (auto simp: fundef.rel_sel) lemma rel_fundefs_rewrite_both: assumes rel_init: "rel_fundefs (Finca_get F1) (Fubx_get F2)" and rel_new: "rel_fundef norm_eq fd1 fd2" shows "rel_fundefs (Finca_get (Finca_add F1 f fd1)) (Fubx_get (Fubx_add F2 f fd2))" unfolding rel_fundefs_def proof fix x show "rel_option (rel_fundef norm_eq) (Finca_get (Finca_add F1 f fd1) x) (Fubx_get (Fubx_add F2 f fd2) x)" proof (cases "x = f") case True then show ?thesis using rel_new by simp next case False then show ?thesis using rel_init by (simp add: rel_fundefs_def) qed qed lemma rel_fundefs_generalize: assumes rel_F1_F2: "rel_fundefs (Finca_get F1) (Fubx_get F2)" and F2_get_f: "Fubx_get F2 f = Some fd2" shows "rel_fundefs (Finca_get F1) (Fubx_get (Fubx_add F2 f (Subx.generalize_fundef fd2)))" unfolding rel_fundefs_def proof let ?F2' = "(Fubx_add F2 f (Subx.generalize_fundef fd2))" fix x show "rel_option (rel_fundef norm_eq) (Finca_get F1 x) (Fubx_get ?F2' x)" proof (cases "x = f") case True then have F2'_get_x: "Fubx_get ?F2' x = Some (Subx.generalize_fundef fd2)" using Subx.Fenv.get_add_eq by auto obtain fd1 where "Finca_get F1 f = Some fd1" and "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_get_f] by auto thus ?thesis unfolding F2'_get_x option_rel_Some2 using True rel_fundef_generalize by auto next case False then have "Fubx_get ?F2' x = Fubx_get F2 x" using Subx.Fenv.get_add_neq by auto then show ?thesis using rel_F1_F2 rel_fundefs_def by fastforce qed qed lemma rel_stacktraces_rewrite_fundef: assumes "rel_stacktraces (Fubx_get F2) xs ys opt" and "Fubx_get F2 f = Some fd" and "pc < length (body fd)" and "\\. Subx.sp_instr (Fubx_get F2) (body fd ! pc) \ = Subx.sp_instr (Fubx_get F2) instr \" and "\ is_fun_call (body fd ! pc)" shows "rel_stacktraces (Fubx_get (Fubx_add F2 f (rewrite_fundef_body fd pc instr))) xs ys opt" using assms(1) proof (induction xs ys opt rule: rel_stacktraces.induct) case rel_stacktraces_Nil then show ?case by (auto intro: rel_stacktraces.intros) next case (rel_stacktraces_Cons st1 st2 g \1 \2 gd n opt) have same_arities: "all_same_arities (Fubx_get F2) (Fubx_get (Fubx_add F2 f (rewrite_fundef_body fd pc instr)))" using all_same_arities_add[OF assms(2)] by simp show ?case proof (cases "g = f") case True then have "gd = fd" using assms(2) rel_stacktraces_Cons.hyps(3) by auto thus ?thesis using True rel_stacktraces_Cons apply (auto intro!: rel_stacktraces.intros simp: sp_fundef_same_arities[OF same_arities, symmetric]) apply (cases "n \ pc"; simp add: sp_fundef_def) subgoal using assms(3,4) by (simp add: Subx.sp_rewrite_eq_Ok take_rewrite_swap) subgoal using rel_stacktraces_Cons.hyps(5) proof (induction opt) case (Some h) hence "rewrite (body fd) pc instr ! n = Ubx.ICall h" using \gd = fd\ apply (simp add: is_valid_fun_call_def) by (metis assms(5) instr.disc nth_rewrite_neq) then show ?case using Some \gd = fd\ apply (simp add: is_valid_fun_call_def) by (metis arity_rewrite_fundef_body assms(2) option.inject Subx.Fenv.get_add_eq Subx.Fenv.get_add_neq) qed simp done next case False thus ?thesis using rel_stacktraces_Cons apply (auto intro!: rel_stacktraces.intros simp: sp_fundef_same_arities[OF same_arities, symmetric]) proof (induction opt) case (Some h) then show ?case using Some assms(2) by (cases "h = f"; simp add: is_valid_fun_call_def) qed simp qed qed section \Matching relation\ lemma sp_fundefs_get: assumes "sp_fundefs F" and "F f = Some fd" shows "sp_fundef F fd (body fd) = Ok [None]" using assms by (simp add: sp_fundefs_def) lemma sp_fundefs_generalize: assumes "sp_fundefs (Fubx_get F)" and "Fubx_get F f = Some fd" shows "sp_fundefs (Fubx_get (Fubx_add F f (Subx.generalize_fundef fd)))" unfolding sp_fundefs_def proof (intro allI impI) fix g gd assume get_g: "Fubx_get (Fubx_add F f (Subx.generalize_fundef fd)) g = Some gd" note sp_F_eq_sp_F' = all_same_arities_generalize_fundef[OF assms(2), THEN sp_same_arities, symmetric] show "sp_fundef (Fubx_get (Fubx_add F f (Subx.generalize_fundef fd))) gd (body gd) = Ok [None]" proof (cases "f = g") case True then have "gd = Subx.generalize_fundef fd" using get_g by simp then show ?thesis using assms by (simp add: sp_fundefs_def sp_fundef_def sp_F_eq_sp_F' Subx.sp_generalize2) next case False then show ?thesis using get_g assms by (simp add: sp_fundefs_def sp_fundef_def sp_F_eq_sp_F') qed qed lemma sp_fundefs_add: assumes "sp_fundefs (Fubx_get F)" and "sp_fundef (Fubx_get F) fd (body fd) = Ok [None]" and "all_same_arities (Fubx_get F) (Fubx_get (Fubx_add F f fd))" shows "sp_fundefs (Fubx_get (Fubx_add F f fd))" unfolding sp_fundefs_def proof (intro allI impI) fix g gd assume "Fubx_get (Fubx_add F f fd) g = Some gd" show "sp_fundef (Fubx_get (Fubx_add F f fd)) gd (body gd) = Ok [None]" proof (cases "f = g") case True then have "gd = fd" using \Fubx_get (Fubx_add F f fd) g = Some gd\ by simp then show ?thesis unfolding sp_fundef_same_arities[OF assms(3), symmetric] using assms(2) by simp next case False then show ?thesis unfolding sp_fundef_same_arities[OF assms(3), symmetric] using \Fubx_get (Fubx_add F f fd) g = Some gd\ using sp_fundefs_get[OF assms(1)] by simp qed qed inductive match (infix "\" 55) where "rel_fundefs (Finca_get F1) (Fubx_get F2) \ sp_fundefs (Fubx_get F2) \ rel_stacktraces (Fubx_get F2) st1 st2 None \ match (State F1 H st1) (State F2 H st2)" section \Backward simulation\ lemma traverse_cast_Dyn_to_norm: "traverse cast_Dyn xs = Some ys \ norm_stack xs = ys" proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) from Cons.prems show ?case by (auto intro: Cons.IH elim: cast_Dyn.elims simp: Option.bind_eq_Some_conv) qed lemma traverse_cast_Dyn_to_all_Dyn: "traverse cast_Dyn xs = Some ys \ list_all (\x. typeof x = None) xs" proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) from Cons.prems show ?case by (auto intro: Cons.IH elim: cast_Dyn.elims simp: Option.bind_eq_Some_conv) qed lemma backward_lockstep_simulation: assumes "Subx.step s2 s2'" and "s1 \ s2" shows "\s1'. Sinca.step s1 s1' \ s1' \ s2'" using assms(2,1) proof (induction s1 s2 rule: match.induct) case (1 F1 F2 st1 st2 H) have rel_F1_F2: "rel_fundefs (Finca_get F1) (Fubx_get F2)" using 1 by simp have sp_F2: "sp_fundefs (Fubx_get F2)" using 1 by simp from "1"(3,4) show ?case proof (induction st1 st2 "None :: 'fun option" rule: rel_stacktraces.induct) case rel_stacktraces_Nil hence False by (auto elim: Subx.step.cases) thus ?case by simp next case (rel_stacktraces_Cons st1 st2 f \1 \2 fd2 pc) have F2_f: "Fubx_get F2 f = Some fd2" using rel_stacktraces_Cons by simp have rel_st1_st2: "rel_stacktraces (Fubx_get F2) st1 st2 (Some f)" using rel_stacktraces_Cons by simp have sp_fundef_prefix: "sp_fundef (Fubx_get F2) fd2 (take pc (body fd2)) = Ok (map typeof \2)" using rel_stacktraces_Cons by simp have \1_def: "\1 = norm_stack \2" using rel_stacktraces_Cons by simp note sp_fundef_def[simp] note sp_prefix = sp_fundef_prefix[unfolded sp_fundef_def] have sp_generalized: "Subx.sp (Fubx_get (Fubx_add F2 f (Subx.generalize_fundef fd2))) (map Subx.generalize_instr (take pc (body fd2))) (replicate (arity fd2) None) = Ok (map (\_. None) \2)" using Subx.sp_generalize[OF sp_prefix, simplified] using all_same_arities_generalize_fundef[OF F2_f] by (simp add: sp_same_arities) from rel_stacktraces_Cons.prems(1) show ?case proof (induction "State F2 H (Frame f pc \2 # st2)" s2' rule: Subx.step.induct) case (step_push fd2' d) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (d # \1) # st1)" have "?STEP ?s1'" using step_push fd1_thms by (auto intro: Sinca.step_push simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" using step_push rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next - case (step_push_num fd2' n) + case (step_push_ubx1 fd2' n) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - - let ?s1' = "State F1 H (Frame f (Suc pc) (box_num n # \1) # st1)" + let ?s1' = "State F1 H (Frame f (Suc pc) (box_ubx1 n # \1) # st1)" have "?STEP ?s1'" - using step_push_num fd1_thms + using step_push_ubx1 fd1_thms by (auto intro: Sinca.step_push simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" - using step_push_num rel_stacktraces_Cons rel_F1_F2 sp_F2 + using step_push_ubx1 rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next - case (step_push_bool fd2' b) + case (step_push_ubx2 fd2' b) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - - let ?s1' = "State F1 H (Frame f (Suc pc) (box_bool b # \1) # st1)" + let ?s1' = "State F1 H (Frame f (Suc pc) (box_ubx2 b # \1) # st1)" have "?STEP ?s1'" - using step_push_bool fd1_thms + using step_push_ubx2 fd1_thms by (auto intro: Sinca.step_push simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" - using step_push_bool rel_stacktraces_Cons rel_F1_F2 sp_F2 + using step_push_ubx2 rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next case (step_pop fd2' x \2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (norm_stack \2') # st1)" have "?STEP ?s1'" unfolding \1_def using step_pop fd1_thms by (auto intro!: Sinca.step_pop simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" using step_pop rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next case (step_load fd2' x i i' d \2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (d # norm_stack \2') # st1)" have pc_in_range: "pc < length (body fd1)" using rel_fd1_fd2 step_load(2) by simp have "?STEP ?s1'" using step_load rel_fundef_body_nth[OF rel_fd1_fd2 pc_in_range] by (auto intro!: Sinca.step_load[OF F1_f pc_in_range, of x] dest: cast_inversions(1) simp: \1_def) moreover have "?MATCH ?s1'" using step_load refl rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros(2)[OF rel_st1_st2] dest!: cast_inversions(1) simp: take_Suc_conv_app_nth[OF step_load(2), simplified]) ultimately show "?thesis" by blast qed next case (step_load_ubx_hit fd2' \ x i i' d blob \2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (d # norm_stack \2') # st1)" have pc_in_range: "pc < length (body fd1)" using rel_fd1_fd2 step_load_ubx_hit(2) by simp have "?STEP ?s1'" using step_load_ubx_hit rel_fundef_body_nth[OF rel_fd1_fd2 pc_in_range] by (auto intro!: Sinca.step_load[OF F1_f pc_in_range, of x] dest: cast_inversions(1) simp: rel_fundef_body_nth \1_def) moreover have "?MATCH ?s1'" using step_load_ubx_hit rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros intro: rel_stacktraces.intros(2)[OF rel_st1_st2] dest!: cast_inversions(1) simp: take_Suc_conv_app_nth[OF step_load_ubx_hit(2), simplified]) ultimately show "?thesis" by blast qed next case (step_load_ubx_miss fd2' \ x i i' d F2' \2') - then have [simp]: "fd2' = fd2" using F2_f by simp + then have fd2'_def[simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (d # norm_stack \2') # st1)" have pc_in_range: "pc < length (body fd1)" using rel_fd1_fd2 step_load_ubx_miss(2) by simp have "?STEP ?s1'" using step_load_ubx_miss F1_f rel_fd1_fd2 by (auto intro!: Sinca.step_load[OF F1_f pc_in_range, of x] dest!: cast_inversions(1) simp: rel_fundef_body_nth \1_def) moreover have "?MATCH ?s1'" - using step_load_ubx_miss - using rel_fundefs_generalize[OF rel_F1_F2 F2_f] - using sp_fundefs_generalize[OF sp_F2 F2_f] - using rel_stacktraces_generalize[OF rel_st1_st2 F2_f] - using sp_fundef_prefix - by (auto intro!: match.intros dest: cast_inversions) + proof (rule match.intros) + show "rel_fundefs (Finca_get F1) (Fubx_get F2')" + unfolding step_load_ubx_miss.hyps(7)[symmetric] + using rel_fundefs_generalize[OF rel_F1_F2 F2_f] + by simp + next + show "sp_fundefs (Fubx_get F2')" + unfolding step_load_ubx_miss.hyps(7)[symmetric] + using sp_fundefs_generalize[OF sp_F2 F2_f] + by simp + next + show "rel_stacktraces (Fubx_get F2') + (Frame f (Suc pc) (d # norm_stack \2') # st1) + (Subx.box_stack f (Frame f (Suc pc) (OpDyn d # \2') # st2)) None" + using step_load_ubx_miss sp_fundef_prefix + by (auto intro!: rel_stacktraces_generalize[OF rel_st1_st2 F2_f] dest: cast_inversions) + qed ultimately show "?thesis" by blast qed next case (step_store fd2' x i i' y d H' \2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H' (Frame f (Suc pc) (norm_stack \2') # st1)" have "?STEP ?s1'" unfolding \1_def using step_store fd1_thms by (auto intro!: Sinca.step_store dest!: cast_inversions simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" using step_store rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros rel_stacktraces.intros dest!: cast_inversions simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next case (step_store_ubx fd2' \ x i i' blob d H' \2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H' (Frame f (Suc pc) (norm_stack \2') # st1)" have pc_in_range: "pc < length (body fd1)" using rel_fd1_fd2 step_store_ubx.hyps(2) by auto have "?STEP ?s1'" unfolding \1_def \i # blob # \2' = \2\[symmetric] using step_store_ubx pc_in_range by (auto intro!: Sinca.step_store[OF F1_f] dest!: cast_inversions simp: rel_fundef_body_nth[OF rel_fd1_fd2]) moreover have "?MATCH ?s1'" using step_store_ubx rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros rel_stacktraces.intros dest!: cast_inversions simp: take_Suc_conv_app_nth) ultimately show "?thesis" by blast qed next case (step_op fd2' op ar \2' x) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1)" have "?STEP ?s1'" unfolding \1_def using step_op fd1_thms take_norm_stack traverse_cast_Dyn_to_norm by (auto intro!: Sinca.step_op simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" using step_op rel_stacktraces_Cons rel_F1_F2 sp_F2 by (auto intro!: match.intros rel_stacktraces.intros simp: take_Suc_conv_app_nth drop_norm_stack Let_def take_map drop_map traverse_cast_Dyn_replicate) ultimately show "?thesis" by blast qed next case (step_op_inl fd2' op ar \2' opinl x F2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?F1' = "Finca_add F1 f (rewrite_fundef_body fd1 pc (Inca.IOpInl opinl))" let ?s1' = "State ?F1' H (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1)" have "?STEP ?s1'" unfolding \1_def using step_op_inl F1_f rel_fd1_fd2 take_norm_stack traverse_cast_Dyn_to_norm by (auto intro!: Sinca.step_op_inl simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" proof show "rel_fundefs (Finca_get ?F1') (Fubx_get F2')" using step_op_inl.hyps(9) using rel_fundefs_rewrite_both[OF rel_F1_F2] using rel_fundef_rewrite_both[OF rel_fd1_fd2] by auto next show "sp_fundefs (Fubx_get F2')" using step_op_inl.hyps all_same_arities_add sp_fundefs_get[OF sp_F2] using Sinca.\\\_invertible by (auto intro!: sp_fundefs_add[OF sp_F2] Subx.sp_rewrite_eq_Ok simp: Subx.sp_instr_op Let_def) next have sp_F2_F2': "Subx.sp (Fubx_get F2) = Subx.sp (Fubx_get F2')" using step_op_inl.hyps(1,9) by (auto intro!: sp_same_arities all_same_arities_add) let ?fd2' = "rewrite_fundef_body fd2' pc (Ubx.IOpInl opinl)" show "rel_stacktraces (Fubx_get F2') (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1) (Frame f (Suc pc) (OpDyn x # drop ar \2) # st2) None" using step_op_inl proof (intro rel_stacktraces.intros) show "rel_stacktraces (Fubx_get F2') st1 st2 (Some f)" using step_op_inl Sinca.\\\_invertible by (auto intro!: rel_stacktraces_rewrite_fundef[OF rel_st1_st2] simp: Subx.sp_instr_op) next show "sp_fundef (Fubx_get F2') ?fd2' (take (Suc pc) (body ?fd2')) = Ok (map typeof (OpDyn x # drop ar \2))" using step_op_inl Sinca.\\\_invertible sp_prefix using traverse_cast_Dyn_to_all_Dyn by (auto simp: take_Suc_conv_app_nth[of pc] sp_F2_F2'[symmetric] Let_def take_map drop_map traverse_cast_Dyn_replicate) qed (auto simp add: drop_norm_stack) qed ultimately show "?thesis" by blast qed next case (step_op_inl_hit fd2' opinl ar \2' x) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1)" have "?STEP ?s1'" unfolding \1_def using step_op_inl_hit fd1_thms take_norm_stack traverse_cast_Dyn_to_norm by (auto intro!: Sinca.step_op_inl_hit simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" using step_op_inl_hit rel_stacktraces_Cons rel_F1_F2 sp_F2 apply (auto intro!: match.intros rel_stacktraces.intros simp: take_Suc_conv_app_nth) using drop_norm_stack apply blast by (simp add: Let_def drop_map take_map traverse_cast_Dyn_replicate) ultimately show "?thesis" by blast qed next case (step_op_inl_miss fd2' opinl ar \2' x F2') then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where F1_f: "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?F1' = "Finca_add F1 f (rewrite_fundef_body fd1 pc (Inca.IOp (\
\\\\ opinl)))" let ?s1' = "State ?F1' H (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1)" have "?STEP ?s1'" unfolding \1_def using step_op_inl_miss F1_f rel_fd1_fd2 take_norm_stack traverse_cast_Dyn_to_norm by (auto intro!: Sinca.step_op_inl_miss simp: rel_fundef_body_nth) moreover have "?MATCH ?s1'" proof show "rel_fundefs (Finca_get ?F1') (Fubx_get F2')" using step_op_inl_miss using rel_fundefs_rewrite_both[OF rel_F1_F2] using rel_fundef_rewrite_both[OF rel_fd1_fd2] by auto next show "sp_fundefs (Fubx_get F2')" using step_op_inl_miss.hyps all_same_arities_add sp_fundefs_get[OF sp_F2] by (auto intro!: sp_fundefs_add[OF sp_F2] Subx.sp_rewrite_eq_Ok simp: Subx.sp_instr_op[symmetric]) next have sp_F2_F2': "Subx.sp (Fubx_get F2) = Subx.sp (Fubx_get F2')" using step_op_inl_miss by (auto intro!: sp_same_arities all_same_arities_add) let ?fd2' = "rewrite_fundef_body fd2' pc (Ubx.IOp (\
\\\\ opinl))" show "rel_stacktraces (Fubx_get F2') (Frame f (Suc pc) (x # drop ar (norm_stack \2)) # st1) (Frame f (Suc pc) (OpDyn x # drop ar \2) # st2) None" proof show "rel_stacktraces (Fubx_get F2') st1 st2 (Some f)" using step_op_inl_miss.hyps by (auto intro: rel_stacktraces_rewrite_fundef[OF rel_st1_st2] simp: Subx.sp_instr_op[symmetric]) next show "Fubx_get F2' f = Some ?fd2'" using step_op_inl_miss Subx.Fenv.get_add_eq by blast next show "sp_fundef (Fubx_get F2') ?fd2' (take (Suc pc) (body ?fd2')) = Ok (map typeof (OpDyn x # drop ar \2))" using \pc < length (body fd2')\ using sp_prefix step_op_inl_miss traverse_cast_Dyn_to_all_Dyn by (auto simp add: take_Suc_conv_app_nth[of pc] sp_F2_F2'[symmetric] traverse_cast_Dyn_replicate take_map drop_map) qed (simp_all add: drop_norm_stack) qed ultimately show "?thesis" by blast qed next case (step_op_ubx fd2' opubx op ar x) then have [simp]: "fd2' = fd2" using F2_f by simp obtain fd1 where fd1_thms: "Finca_get F1 f = Some fd1" "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame f (Suc pc) (Subx.norm_unboxed x # drop ar (norm_stack \2)) # st1)" have "pc < length (body fd1)" using fd1_thms(2) step_op_ubx.hyps(2) by auto hence nth_fd1: "body fd1 ! pc = Inca.instr.IOpInl (\\\ opubx)" using rel_fundef_body_nth[OF fd1_thms(2)] using \body fd2' ! pc = IOpUbx opubx\ by simp have "\\\\\ (\\\ opubx) (take ar (map Subx.norm_unboxed \2))" using step_op_ubx by (auto intro: Sinca.\\\_\\\\\ Subx.\\\\\_to_\\\ simp: take_map) hence "?STEP ?s1'" unfolding norm_stack_def \1_def using step_op_ubx fd1_thms(1) nth_fd1 \pc < length (body fd1)\ using Subx.\\\\\_correct by (auto intro!: Sinca.step_op_inl_hit simp: take_map) moreover have "?MATCH ?s1'" using step_op_ubx rel_stacktraces_Cons rel_F1_F2 sp_F2 Subx.\\\\\\\\_complete by (auto intro!: match.intros rel_stacktraces.intros simp: take_Suc_conv_app_nth drop_norm_stack Let_def drop_map take_map min.absorb2) ultimately show "?thesis" by blast qed next case (step_cjump_true fd2' n x \2') then have False using F2_f sp_fundefs_get[OF sp_F2, unfolded sp_fundef_def, THEN Subx.sp_no_jump] nth_mem by force thus ?case by simp next case (step_cjump_false fd2' n x \2') then have False using F2_f sp_fundefs_get[OF sp_F2, unfolded sp_fundef_def, THEN Subx.sp_no_jump] nth_mem by force thus ?case by simp next case (step_fun_call f' fd2' pc' g gd2 ar \2' frame\<^sub>g) then have [simp]: "f' = f" "pc' = pc" "fd2' = fd2" using F2_f by auto obtain fd1 where "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto obtain gd1 where "Finca_get F1 g = Some gd1" and rel_gd1_gd2: "rel_fundef norm_eq gd1 gd2" using step_fun_call rel_fundefs_Some2[OF rel_F1_F2] by blast have pc_in_range: "pc < length (body fd1)" using \pc' < length (body fd2')\ rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame g 0 (take (arity gd1) \1) # Frame f pc \1 # st1)" have "?STEP ?s1'" using step_fun_call rel_stacktraces_Cons.hyps(2) pc_in_range using \Finca_get F1 f = Some fd1\ \Finca_get F1 g = Some gd1\ using rel_fundef_body_nth[OF rel_fd1_fd2] using rel_fundef_arities[OF rel_gd1_gd2, symmetric] by (auto intro!: Sinca.step_fun_call) moreover have "?MATCH ?s1'" proof show "rel_fundefs (Finca_get F1) (Fubx_get F2)" using rel_F1_F2 . next show "sp_fundefs (Fubx_get F2)" using sp_F2 . next show "rel_stacktraces (Fubx_get F2) (Frame g 0 (take (arity gd1) \1) # Frame f pc \1 # st1) (frame\<^sub>g # Frame f pc \2 # st2) None" unfolding step_fun_call(9) proof (rule rel_stacktraces.intros(2)) show "rel_stacktraces (Fubx_get F2) (Frame f pc \1 # st1) (Frame f pc \2 # st2) (Some g)" using rel_st1_st2 F2_f \1_def sp_prefix using step_fun_call by (auto intro!: rel_stacktraces.intros elim!: list.pred_mono_strong simp: is_valid_fun_call_def) next show "take (arity gd1) \1 = norm_stack (take ar \2')" using \1_def rel_fundef_arities[OF rel_gd1_gd2] using step_fun_call by (simp add: take_norm_stack) next show "Fubx_get F2 g = Some gd2" using step_fun_call by simp next show "sp_fundef (Fubx_get F2) gd2 (take 0 (body gd2)) = Ok (map typeof (take ar \2'))" using step_fun_call by (auto elim: replicate_eq_map) qed simp_all qed ultimately show "?thesis" by blast qed next case (step_fun_end f' fd2' \2\<^sub>g pc' \2' frame\<^sub>g g pc\<^sub>g frame\<^sub>g' st2') then have [simp]: "f' = f" "fd2' = fd2" "pc' = pc" "\2' = \2" using F2_f by auto obtain fd1 where "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some2[OF rel_F1_F2 F2_f] by auto obtain gd2 \1\<^sub>g st1' where st1_def: "st1 = Frame g pc\<^sub>g \1\<^sub>g # st1'" and "\1\<^sub>g = norm_stack \2\<^sub>g" and rel_st1'_st2': "rel_stacktraces (Fubx_get F2) st1' st2' (Some g)" and "Fubx_get F2 g = Some gd2" and sp_prefix_gd2: "Subx.sp (Fubx_get F2) (take pc\<^sub>g (body gd2)) (replicate (arity gd2) None) = Ok (map typeof \2\<^sub>g)" and pc\<^sub>g_in_range: "pc\<^sub>g < length (body gd2)" and "body gd2 ! pc\<^sub>g = Ubx.ICall f" and prefix_all_dyn_\2\<^sub>g: "list_all is_dyn_operand (take (arity fd2) \2\<^sub>g)" using rel_st1_st2 step_fun_end by (auto elim: rel_stacktraces.cases simp: is_valid_fun_call_def) have pc_at_end: "pc = length (body fd1)" using \pc' = length (body fd2')\ using rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F1 H (Frame g (Suc pc\<^sub>g) (\1 @ drop (arity fd1) \1\<^sub>g) # st1')" have "?STEP ?s1'" using step_fun_end.hyps(2) using st1_def \\1\<^sub>g = norm_stack \2\<^sub>g\ using \Finca_get F1 f = Some fd1\ pc_at_end using rel_fundef_arities[OF rel_fd1_fd2, symmetric] by (auto intro!: Sinca.step_fun_end) moreover have "?MATCH ?s1'" using rel_F1_F2 sp_F2 proof show "rel_stacktraces (Fubx_get F2) (Frame g (Suc pc\<^sub>g) (\1 @ drop (arity fd1) \1\<^sub>g) # st1') (frame\<^sub>g' # st2') None" unfolding step_fun_end(6) using rel_st1'_st2' proof (rule rel_stacktraces.rel_stacktraces_Cons) show "\1 @ drop (arity fd1) \1\<^sub>g = norm_stack (\2' @ drop (arity fd2') \2\<^sub>g)" using \1_def \\1\<^sub>g = norm_stack \2\<^sub>g\ using rel_fundef_arities[OF rel_fd1_fd2] by (simp add: norm_stack_append drop_norm_stack) next show "Fubx_get F2 g = Some gd2" using \Fubx_get F2 g = Some gd2\ . next have "arity fd2 \ length \2\<^sub>g" using step_fun_end.hyps(2) by simp moreover have "list_all (\x. x = None) (take (arity fd2) (map typeof \2\<^sub>g))" using prefix_all_dyn_\2\<^sub>g by (auto elim!: list.pred_mono_strong simp: take_map list.pred_map is_dyn_operand_def) moreover have "map typeof \2 = [None]" using \pc' = length (body fd2')\ sp_prefix using sp_fundefs_get[OF sp_F2 F2_f] by simp ultimately show "sp_fundef (Fubx_get F2) gd2 (take (Suc pc\<^sub>g) (body gd2)) = Ok (map typeof (\2' @ drop (arity fd2') \2\<^sub>g))" using sp_prefix_gd2 using \body gd2 ! pc\<^sub>g = Ubx.ICall f\ F2_f by (auto dest: list_all_eq_const_imp_replicate simp: take_Suc_conv_app_nth[OF pc\<^sub>g_in_range] Let_def drop_map) qed simp qed ultimately show "?thesis" by blast qed qed qed qed lemma match_final_backward: "s1 \ s2 \ Subx.final s2 \ Sinca.final s1" proof (induction s1 s2 rule: match.induct) case (1 F1 F2 st1 st2 H) obtain f fd2 pc \2 where st2_def: "st2 = [Frame f pc \2]" and "Fubx_get F2 f = Some fd2" and "pc = length (body fd2)" using \Subx.final (State F2 H st2)\ by (auto elim!: Subx.final.cases) obtain \1 where st1_def: "st1 = [Frame f pc \1]" using \rel_stacktraces (Fubx_get F2) st1 st2 None\ unfolding st2_def by (auto elim!: rel_stacktraces.cases) obtain fd1 where "Finca_get F1 f = Some fd1" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using \rel_fundefs (Finca_get F1) (Fubx_get F2)\ \Fubx_get F2 f = Some fd2\ using rel_fundefs_Some2 by fastforce have "length (body fd1) = length (body fd2)" using rel_fd1_fd2 by simp thus ?case unfolding st1_def using \Finca_get F1 f = Some fd1\ \pc = length (body fd2)\ by (auto intro: Sinca.final.intros) qed sublocale inca_to_ubx_simulation: backward_simulation Sinca.step Subx.step Sinca.final Subx.final "\_ _. False" "\_. match" using match_final_backward backward_lockstep_simulation lockstep_to_plus_backward_simulation[of match Subx.step Sinca.step] by unfold_locales auto section \Forward simulation\ lemma traverse_cast_Dyn_eq_norm_stack: assumes "list_all (\x. x = None) (map typeof xs)" shows "traverse cast_Dyn xs = Some (norm_stack xs)" using assms proof (induction xs) case Nil then show ?case by simp next case (Cons x xs) from Cons.prems have typeof_x: "typeof x = None" and typeof_xs: "list_all (\x. x = None) (map typeof xs)" by simp_all obtain x' where "x = OpDyn x'" using typeof_unboxed_inversion(1)[OF typeof_x] by auto then show ?case using Cons.IH[OF typeof_xs] by simp qed lemma forward_lockstep_simulation: assumes "Sinca.step s1 s1'" and "s1 \ s2" shows "\s2'. Subx.step s2 s2' \ s1' \ s2'" using assms(2,1) proof (induction s1 s2 rule: match.induct) case (1 F1 F2 st1 st2 H) have rel_F1_F2: "rel_fundefs (Finca_get F1) (Fubx_get F2)" using 1 by simp have sp_F2: "sp_fundefs (Fubx_get F2)" using 1 by simp note rel_fundefs_rewrite_both' = rel_fundef_rewrite_both[THEN rel_fundefs_rewrite_both[OF rel_F1_F2]] from "1"(3,4) show ?case proof (induction st1 st2 "None :: 'fun option" rule: rel_stacktraces.induct) case rel_stacktraces_Nil hence False by (auto elim: Sinca.step.cases) thus ?case by simp next case (rel_stacktraces_Cons st1 st2 f \1 \2 fd2 pc) have F2_f: "Fubx_get F2 f = Some fd2" using rel_stacktraces_Cons by simp have rel_st1_st2: "rel_stacktraces (Fubx_get F2) st1 st2 (Some f)" using rel_stacktraces_Cons by simp have sp_fundef_prefix: "sp_fundef (Fubx_get F2) fd2 (take pc (body fd2)) = Ok (map typeof \2)" using rel_stacktraces_Cons by simp have \1_def: "\1 = norm_stack \2" using rel_stacktraces_Cons by simp note sp_fundef_def[simp] note sp_prefix = sp_fundef_prefix[unfolded sp_fundef_def] note ex_F1_f = rel_fundefs_Some2[OF rel_F1_F2 F2_f] note sp_fundef_full = sp_fundefs_get[OF sp_F2 \Fubx_get F2 f = Some fd2\] note sp_full = sp_fundef_full[unfolded sp_fundef_def] hence sp_sufix: "Subx.sp (Fubx_get F2) (body fd2 ! pc # drop (Suc pc) (body fd2)) (map typeof \2) = Ok [None]" if pc_in_range: "pc < length (body fd2)" unfolding Cons_nth_drop_Suc[OF pc_in_range] unfolding Subx.sp_eq_bind_take_drop[of _ "body fd2" _ pc] unfolding sp_prefix by simp from rel_stacktraces_Cons.prems(1) show ?case proof (induction "State F1 H (Frame f pc \1 # st1)" s1' rule: Sinca.step.induct) case (step_push fd1 d) hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_push rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_push rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") using step_push norm_instr_nth_body proof (cases "body fd2 ! pc") case (IPush d2) then have d_def: "d = d2" using norm_instr_nth_body step_push.hyps(3) by auto let ?s2' = "State F2 H (Frame f (Suc pc) (OpDyn d2 # \2) # st2)" have "?STEP ?s2'" using IPush step_push d_def F2_f pc_in_range by (auto intro: Subx.step_push) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def using IPush d_def sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto next - case (IPushNumUbx n) - then have d_def: "d = box_num n" + case (IPushUbx1 n) + then have d_def: "d = box_ubx1 n" using norm_instr_nth_body step_push.hyps(3) by auto - let ?s2' = "State F2 H (Frame f (Suc pc) (OpNum n # \2) # st2)" + let ?s2' = "State F2 H (Frame f (Suc pc) (OpUbx1 n # \2) # st2)" have "?STEP ?s2'" - using IPushNumUbx step_push d_def F2_f pc_in_range - by (auto intro: Subx.step_push_num) + using IPushUbx1 step_push d_def F2_f pc_in_range + by (auto intro: Subx.step_push_ubx1) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def - using IPushNumUbx d_def sp_prefix take_Suc_conv_app_nth[OF pc_in_range] + using IPushUbx1 d_def sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto next - case (IPushBoolUbx b) - then have d_def: "d = box_bool b" + case (IPushUbx2 b) + then have d_def: "d = box_ubx2 b" using norm_instr_nth_body step_push.hyps(3) by auto - let ?s2' = "State F2 H (Frame f (Suc pc) (OpBool b # \2) # st2)" + let ?s2' = "State F2 H (Frame f (Suc pc) (OpUbx2 b # \2) # st2)" have "?STEP ?s2'" - using IPushBoolUbx step_push d_def F2_f pc_in_range - by (auto intro: Subx.step_push_bool) + using IPushUbx2 step_push d_def F2_f pc_in_range + by (auto intro: Subx.step_push_ubx2) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def - using IPushBoolUbx d_def sp_prefix take_Suc_conv_app_nth[OF pc_in_range] + using IPushUbx2 d_def sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto qed simp_all next case (step_pop fd1 x \1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_pop rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_pop rel_fundef_body_length[OF rel_fd1_fd2] by simp obtain x' \2' where \2_def: "\2 = x' # \2'" and "\1' = norm_stack \2'" using step_pop \\1 = norm_stack \2\ norm_stack_def by auto show ?case (is "\x. ?STEP x \ ?MATCH x") using step_pop norm_instr_nth_body proof (cases "body fd2 ! pc") case IPop let ?s2' = "State F2 H (Frame f (Suc pc) \2' # st2)" have "?STEP ?s2'" using IPop step_pop F2_f pc_in_range \2_def by (auto intro: Subx.step_pop) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \\1' = norm_stack \2'\ using IPop sp_prefix take_Suc_conv_app_nth[OF pc_in_range] \2_def by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto qed simp_all next case (step_load fd1 var i d \1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_load rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_load rel_fundef_body_length[OF rel_fd1_fd2] by simp obtain i' \2' where \2_def: "\2 = i' # \2'" and norm_i': "Subx.norm_unboxed i' = i" and "norm_stack \2' = \1'" using step_load \1_def norm_stack_def by auto show ?case (is "\x. ?STEP x \ ?MATCH x") using step_load norm_instr_nth_body proof (cases "body fd2 ! pc") case (ILoad var') then have [simp]: "var' = var" using norm_instr_nth_body step_load.hyps(3) by auto let ?s2' = "State F2 H (Frame f (Suc pc) (OpDyn d # \2') # st2)" have "i' = OpDyn i" using sp_sufix[OF pc_in_range, unfolded \2_def ILoad, simplified] using norm_i' by (cases i'; simp) hence "?STEP ?s2'" using ILoad step_load F2_f pc_in_range by (auto intro!: Subx.step_load simp: \2_def) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def using ILoad sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros simp: \norm_stack \2' = \1'\ \i' = OpDyn i\ \2_def) ultimately show ?thesis by auto next case (ILoadUbx \ var') then have [simp]: "var' = var" using norm_instr_nth_body step_load.hyps(3) by auto have [simp]: "i' = OpDyn i" using sp_sufix[OF pc_in_range, unfolded \2_def ILoadUbx, simplified] using norm_i' by (cases i'; simp) show ?thesis proof (cases "Subx.unbox \ d") case None let ?F2' = "Fubx_add F2 f (Subx.generalize_fundef fd2)" let ?frame = "Frame f (Suc pc) (OpDyn d # \2')" let ?s2' = "State ?F2' H (Subx.box_stack f (?frame # st2))" have "?STEP ?s2'" using None ILoadUbx using step_load pc_in_range F2_f by (auto intro!: Subx.step_load_ubx_miss simp add: \2_def simp del: Subx.box_stack_Cons) moreover have "?MATCH ?s2'" using rel_fundefs_generalize[OF rel_F1_F2 F2_f] using sp_fundefs_generalize[OF sp_F2 F2_f] using sp_fundef_prefix ILoadUbx using pc_in_range by (auto intro!: match.intros rel_stacktraces_generalize[OF rel_st1_st2 F2_f] simp: \2_def \norm_stack \2' = \1'\) ultimately show ?thesis by auto next case (Some blob) let ?s2' = "State F2 H (Frame f (Suc pc) (blob # \2') # st2)" have "?STEP ?s2'" using Some ILoadUbx step_load F2_f pc_in_range by (auto intro: Subx.step_load_ubx_hit simp: \2_def) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def using Some ILoadUbx sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros simp: \norm_stack \2' = \1'\ \2_def) ultimately show ?thesis by auto qed qed simp_all next case (step_store fd1 var i x H' \1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_store rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_store rel_fundef_body_length[OF rel_fd1_fd2] by simp obtain i' x' \2' where \2_def: "\2 = i' # x' # \2'" and norm_i': "Subx.norm_unboxed i' = i" and norm_x': "Subx.norm_unboxed x' = x" and "norm_stack \2' = \1'" using step_store \1_def norm_stack_def by auto show ?case (is "\x. ?STEP x \ ?MATCH x") using step_store norm_instr_nth_body proof (cases "body fd2 ! pc") case (IStore var') then have [simp]: "var' = var" using norm_instr_nth_body step_store.hyps(3) by auto note sp_sufix' = sp_sufix[OF pc_in_range, unfolded \2_def IStore, simplified] have [simp]: "i' = OpDyn i" using norm_i' sp_sufix' by (cases i'; simp) have [simp]: "x' = OpDyn x" using norm_x' sp_sufix' by (cases x'; simp) let ?s2' = "State F2 (heap_add H (var, i) x) (Frame f (Suc pc) \2' # st2)" have "?STEP ?s2'" using IStore \2_def pc_in_range F2_f by (auto intro: Subx.step_store) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \2_def using \norm_stack \2' = \1'\ \heap_add H (var, i) x = H'\ using IStore sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto next case (IStoreUbx \ var') then have [simp]: "var' = var" using norm_instr_nth_body step_store.hyps(3) by auto note sp_sufix' = sp_sufix[OF pc_in_range, unfolded \2_def IStoreUbx, simplified] have [simp]: "i' = OpDyn i" using norm_i' sp_sufix' by (cases i'; simp) have typeof_x'[simp]: "typeof x' = Some \" using sp_sufix' apply (auto simp add: Result.bind_eq_Ok_conv elim!: Subx.sp_instr.elims) by (metis result.simps(4)) let ?s2' = "State F2 (heap_add H (var, i) x) (Frame f (Suc pc) \2' # st2)" have "?STEP ?s2'" unfolding \2_def using F2_f pc_in_range IStoreUbx using Subx.typeof_and_norm_unboxed_imp_cast_and_box[OF typeof_x' norm_x'] by (auto intro!: Subx.step_store_ubx) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \2_def using \norm_stack \2' = \1'\ \heap_add H (var, i) x = H'\ using IStoreUbx sp_prefix take_Suc_conv_app_nth[OF pc_in_range] by (auto intro!: match.intros rel_stacktraces.intros) ultimately show ?thesis by auto qed simp_all next case (step_op fd1 op ar x) hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_op rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_op rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") using step_op norm_instr_nth_body proof (cases "body fd2 ! pc") case (IOp op') then have "op' = op" using norm_instr_nth_body step_op.hyps(3) by auto hence "ar \ length \2" and all_arg_Dyn: "list_all (\x. x = None) (map typeof (take ar \2))" using IOp step_op sp_sufix[OF pc_in_range] by (auto simp: take_map) let ?s2' = "State F2 H (Frame f (Suc pc) (OpDyn x # drop ar \2) # st2)" have "?STEP ?s2'" using IOp step_op \op' = op\ \1_def pc_in_range F2_f using traverse_cast_Dyn_eq_norm_stack[OF all_arg_Dyn] by (auto intro!: Subx.step_op simp: take_norm_stack) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f using IOp sp_prefix take_Suc_conv_app_nth[OF pc_in_range] using arg_cong[OF \1_def, of "drop ar"] \ar \ length \2\ using \op' = op\ all_arg_Dyn \1_def \\\\\\ op = ar\ by (auto intro!: match.intros rel_stacktraces.intros dest: list_all_eq_const_imp_replicate simp: drop_norm_stack[symmetric] Let_def take_map drop_map) ultimately show ?thesis by auto qed simp_all next case (step_op_inl fd1 op ar opinl x F1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_op_inl rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_op_inl rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") using step_op_inl norm_instr_nth_body proof (cases "body fd2 ! pc") case (IOp op') then have "op' = op" using norm_instr_nth_body step_op_inl.hyps(3) by simp hence "ar \ length \2" and all_arg_Dyn: "list_all (\x. x = None) (map typeof (take ar \2))" using IOp step_op_inl sp_sufix[OF pc_in_range] by (auto simp: take_map) let ?fd2' = "rewrite_fundef_body fd2 pc (Ubx.IOpInl opinl)" let ?F2' = "Fubx_add F2 f ?fd2'" let ?frame = "Frame f (Suc pc) (OpDyn x # drop ar \2)" let ?s2' = "State ?F2' H (?frame # st2)" have "?STEP ?s2'" using IOp step_op_inl \op' = op\ using \1_def pc_in_range \Fubx_get F2 f = Some fd2\ using all_arg_Dyn take_norm_stack traverse_cast_Dyn_eq_norm_stack by (auto intro!: Subx.step_op_inl) moreover have "?MATCH ?s2'" proof show "rel_fundefs (Finca_get F1') (Fubx_get ?F2')" using step_op_inl rel_fd1_fd2 by (auto intro: rel_fundefs_rewrite_both') next have "arity fd2 = arity ?fd2'" by simp hence "all_same_arities (Fubx_get F2) (Fubx_get ?F2')" using all_same_arities_add[OF F2_f] by simp thus "sp_fundefs (Fubx_get ?F2')" apply (auto intro!: sp_fundefs_add[OF sp_F2]) apply (rule Subx.sp_rewrite_eq_Ok[OF pc_in_range _ sp_full]) apply (rule allI) unfolding IOp apply (rule Subx.sp_instr_op) using Sinca.\\\_invertible \op' = op\ step_op_inl.hyps(6) by blast next have "rel_stacktraces (Fubx_get F2) (Frame f (Suc pc) (x # drop ar \1) # st1) (?frame # st2) None" using rel_st1_st2 sp_prefix F2_f using IOp take_Suc_conv_app_nth[OF pc_in_range] using arg_cong[OF \1_def, of "drop ar"] \ar \ length \2\ using \op' = op\ step_op_inl.hyps(4) all_arg_Dyn by (auto intro!: rel_stacktraces.intros dest: list_all_eq_const_imp_replicate simp: drop_norm_stack[symmetric] Let_def take_map drop_map) thus "rel_stacktraces (Fubx_get ?F2') (Frame f (Suc pc) (x # drop ar \1) # st1) (?frame # st2) None" using F2_f pc_in_range IOp using Sinca.\\\_invertible \op' = op\ step_op_inl.hyps(6) by (auto intro!: rel_stacktraces_rewrite_fundef simp: Subx.sp_instr_op Let_def) qed ultimately show ?thesis by auto qed simp_all next case (step_op_inl_hit fd1 opinl ar x) hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_op_inl_hit rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_op_inl_hit rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") using step_op_inl_hit norm_instr_nth_body proof (cases "body fd2 ! pc") case (IOpInl opinl') then have "opinl' = opinl" using norm_instr_nth_body step_op_inl_hit.hyps(3) by simp hence "ar \ length \2" and all_arg_Dyn: "list_all (\x. x = None) (map typeof (take ar \2))" using IOpInl step_op_inl_hit sp_sufix[OF pc_in_range] by (auto simp: take_map) let ?s2' = "State F2 H (Frame f (Suc pc) (OpDyn x # drop ar \2) # st2)" have "?STEP ?s2'" using IOpInl step_op_inl_hit \opinl' = opinl\ using \1_def pc_in_range F2_f all_arg_Dyn by (auto intro: Subx.step_op_inl_hit traverse_cast_Dyn_eq_norm_stack simp: take_norm_stack) moreover have "?MATCH ?s2'" using rel_F1_F2 sp_F2 rel_st1_st2 F2_f using IOpInl sp_prefix take_Suc_conv_app_nth[OF pc_in_range] using arg_cong[OF \1_def, of "drop ar"] using \ar \ length \2\ \opinl' = opinl\ step_op_inl_hit.hyps(4,5) all_arg_Dyn by (auto intro!: match.intros rel_stacktraces.intros dest: list_all_eq_const_imp_replicate simp: drop_norm_stack[symmetric] Let_def take_map drop_map) ultimately show ?thesis by auto next case (IOpUbx opubx) then have "\\\ opubx = opinl" using norm_instr_nth_body step_op_inl_hit.hyps(3) by simp hence \\\\\_opubx[simp]: "\\\\\ (\
\\\\ (\\\ opubx)) = ar" using step_op_inl_hit.hyps(4,5) by simp note sp_sufix' = sp_sufix[OF pc_in_range, unfolded IOpUbx, simplified, unfolded Let_def, simplified] obtain dom codom where typeof_opubx: "\\\\\\\\ opubx = (dom, codom)" using prod.exhaust_sel by blast hence dom_def: "dom = map typeof (take ar \2)" unfolding \\\\\_opubx[unfolded Subx.\\\\\\\\_\\\\\, symmetric] using sp_sufix' by (auto simp: Let_def take_map) obtain x' where eval_op: "\\\\\ opubx (take ar \2) = Some x'" and typeof_x': "typeof x' = codom" using typeof_opubx[unfolded dom_def, THEN Subx.\\\\\\\\_correct] by auto let ?s2' = "State F2 H (Frame f (Suc pc) (x' # drop ar \2) # st2)" have "?STEP ?s2'" using \1_def step_op_inl_hit eval_op \\\\\_opubx using pc_in_range IOpUbx F2_f by (auto intro!: Subx.step_op_ubx) moreover have "?MATCH ?s2'" proof - have "x = Subx.norm_unboxed x'" using Subx.\\\\\_correct[OF eval_op, unfolded \\\\ opubx = opinl\] using step_op_inl_hit \1_def by (simp add: take_map norm_stack_def) thus ?thesis using rel_F1_F2 sp_F2 rel_st1_st2 F2_f \1_def using sp_prefix take_Suc_conv_app_nth[OF pc_in_range, unfolded IOpUbx] using step_op_inl_hit using typeof_opubx typeof_x' by (auto intro!: match.intros rel_stacktraces.intros simp: dom_def drop_norm_stack Let_def min.absorb2 take_map drop_map) qed ultimately show ?thesis by auto qed simp_all next case (step_op_inl_miss fd1 opinl ar x F1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_op_inl_miss rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_op_inl_miss rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case (is "\x. ?STEP x \ ?MATCH x") using step_op_inl_miss norm_instr_nth_body proof (cases "body fd2 ! pc") case (IOpInl opinl') then have "opinl' = opinl" using norm_instr_nth_body step_op_inl_miss.hyps(3) by simp hence "ar \ length \2" and all_arg_Dyn: "list_all (\x. x = None) (map typeof (take ar \2))" using IOpInl step_op_inl_miss sp_sufix[OF pc_in_range] by (auto simp: take_map) let ?fd2' = "rewrite_fundef_body fd2 pc (Ubx.IOp (\
\\\\ opinl))" let ?F2' = "Fubx_add F2 f ?fd2'" let ?frame = "Frame f (Suc pc) (OpDyn x # drop ar \2)" let ?s2' = "State ?F2' H (?frame # st2)" have "?STEP ?s2'" using IOpInl step_op_inl_miss \opinl' = opinl\ using \1_def pc_in_range F2_f using traverse_cast_Dyn_eq_norm_stack[OF all_arg_Dyn] by (auto intro!: Subx.step_op_inl_miss simp: take_norm_stack) moreover have "?MATCH ?s2'" proof show "rel_fundefs (Finca_get F1') (Fubx_get ?F2')" using step_op_inl_miss rel_fd1_fd2 by (auto intro: rel_fundefs_rewrite_both') next show "sp_fundefs (Fubx_get ?F2')" using IOpInl \opinl' = opinl\ all_same_arities_add[OF F2_f] sp_full by (auto intro: sp_fundefs_add[OF sp_F2] simp: Subx.sp_instr_op[symmetric] Subx.sp_rewrite[OF pc_in_range]) next have "rel_stacktraces (Fubx_get F2) (Frame f (Suc pc) (x # drop ar \1) # st1) (?frame # st2) None" using rel_st1_st2 sp_prefix F2_f using IOpInl \1_def take_Suc_conv_app_nth[OF pc_in_range] using \ar \ length \2\ \opinl' = opinl\ step_op_inl_miss.hyps(4,5) using all_arg_Dyn by (auto intro!: rel_stacktraces.intros dest: list_all_eq_const_imp_replicate simp: drop_norm_stack Let_def take_map drop_map) thus "rel_stacktraces (Fubx_get ?F2') (Frame f (Suc pc) (x # drop ar \1) # st1) (?frame # st2) None" using F2_f pc_in_range IOpInl by (auto intro: rel_stacktraces_rewrite_fundef simp: \opinl' = opinl\ Let_def Subx.sp_instr_op[symmetric]) qed ultimately show ?thesis by auto next case (IOpUbx opubx) then have "\\\ opubx = opinl" using norm_instr_nth_body step_op_inl_miss.hyps(3) by simp hence \\\\\_opubx: "\\\\\ (\
\\\\ (\\\ opubx)) = ar" using step_op_inl_miss.hyps(4,5) by simp obtain dom codom where "\\\\\\\\ opubx = (dom, codom)" using prod.exhaust_sel by blast hence "\\\\\\\\ opubx = (map typeof (take ar \2), codom)" unfolding \\\\\_opubx[unfolded Subx.\\\\\\\\_\\\\\, symmetric] using sp_sufix[OF pc_in_range] unfolding IOpUbx by (auto simp: Let_def case_prod_beta take_map) then obtain x where eval_op: "\\\\\ opubx (take ar \2) = Some x" using Subx.\\\\\\\\_correct by blast hence "\\\\\ opinl (take ar \1)" unfolding \1_def norm_stack_def using \\\\ opubx = opinl\ by (auto intro: Sinca.\\\_\\\\\ Subx.\\\\\_to_\\\ simp: take_map) hence False using step_op_inl_miss by auto thus ?thesis by simp qed simp_all next case (step_cjump_true fd1 n \1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_cjump_true rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_cjump_true rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case using step_cjump_true norm_instr_nth_body proof (cases "body fd2 ! pc") case (ICJump n') then have False using F2_f sp_fundefs_get[OF sp_F2, unfolded sp_fundef_def, THEN Subx.sp_no_jump] using nth_mem pc_in_range by fastforce thus ?thesis by simp qed simp_all next case (step_cjump_false fd1 n \1') hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using ex_F1_f by simp hence norm_instr_nth_body: "norm_instr (body fd2 ! pc) = body fd1 ! pc" using step_cjump_false rel_fundef_body_nth by metis have pc_in_range: "pc < length (body fd2)" using step_cjump_false rel_fundef_body_length[OF rel_fd1_fd2] by simp show ?case using step_cjump_false norm_instr_nth_body proof (cases "body fd2 ! pc") case (ICJump n') then have False using F2_f sp_fundefs_get[OF sp_F2, unfolded sp_fundef_def, THEN Subx.sp_no_jump] using nth_mem pc_in_range by fastforce thus ?thesis by simp qed simp_all next case (step_fun_call f' fd1 pc' g gd1 \1' frame\<^sub>g) hence [simp]: "f' = f" "pc' = pc" "\1' = \1" by auto hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using step_fun_call ex_F1_f by simp obtain gd2 where "Fubx_get F2 g = Some gd2" and rel_gd1_gd2: "rel_fundef norm_eq gd1 gd2" using step_fun_call rel_fundefs_Some1[OF rel_F1_F2] by blast have pc_in_range: "pc < length (body fd2)" using step_fun_call rel_fd1_fd2 by simp have nth_body2: "body fd2 ! pc = Ubx.ICall g" using rel_fundef_body_nth[OF rel_fd1_fd2 \pc' < length (body fd1)\, symmetric] unfolding \body fd1 ! pc' = Inca.ICall g\ by (cases "body fd2 ! pc'"; simp) have prefix_\2_all_Dyn: "list_all (\x. x = None) (map typeof (take (arity gd2) \2))" using \Fubx_get F2 g = Some gd2\ sp_sufix[OF pc_in_range] nth_body2 by (auto simp: Let_def take_map) hence all_dyn_args: "list_all is_dyn_operand (take (arity gd2) \2)" by (auto elim: list.pred_mono_strong simp add: list.pred_map comp_def) show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?args = "map OpDyn (norm_stack (take (arity gd2) \2))" let ?frame = "Frame g 0 ?args" let ?s1' = "State F2 H (?frame # Frame f pc \2 # st2)" have "?STEP ?s1'" proof - have "arity gd2 \ length \2" using \arity gd1 \ length \1'\ using rel_fundef_arities[OF rel_gd1_gd2] \1_def by simp thus ?thesis using pc_in_range nth_body2 using \Fubx_get F2 g = Some gd2\ rel_stacktraces_Cons.hyps(3) using all_dyn_args by (auto intro!: Subx.step_fun_call[of _ _ fd2] nth_equalityI simp: typeof_unboxed_eq_const list_all_length norm_stack_def) qed moreover have "?MATCH ?s1'" using rel_F1_F2 sp_F2 proof show "rel_stacktraces (Fubx_get F2) (frame\<^sub>g # Frame f pc \1 # st1) (?frame # Frame f pc \2 # st2) None" unfolding step_fun_call(7) proof (rule rel_stacktraces.intros) show "rel_stacktraces (Fubx_get F2) (Frame f pc \1 # st1) (Frame f pc \2 # st2) (Some g)" using pc_in_range nth_body2 rel_stacktraces_Cons using \Fubx_get F2 g = Some gd2\ all_dyn_args by (auto intro!: rel_stacktraces.intros simp: is_valid_fun_call_def) next show "take (arity gd1) \1' = norm_stack ?args" using \1_def using rel_fundef_arities[OF rel_gd1_gd2] by (simp add: norm_stack_map take_norm_stack) next show "Fubx_get F2 g = Some gd2" using \Fubx_get F2 g = Some gd2\ . next show "sp_fundef (Fubx_get F2) gd2 (take 0 (body gd2)) = Ok (map typeof ?args)" using \1_def step_fun_call.hyps(5) using rel_fundef_arities[OF rel_gd1_gd2] by (simp add: map_replicate_const) qed simp_all qed ultimately show "?thesis" by blast qed next case (step_fun_end f' fd1 \1\<^sub>g pc' \1' frame\<^sub>g g pc\<^sub>g frame\<^sub>g' st1') hence [simp]: "f' = f" "pc' = pc" "\1' = \1" by auto hence rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using step_fun_end ex_F1_f by simp note arities_fd1_fd2 = rel_fundef_arities[OF rel_fd1_fd2] obtain \2\<^sub>g st2' where st2_def: "st2 = Frame g pc\<^sub>g \2\<^sub>g # st2'" using step_fun_end rel_st1_st2 by (auto elim: rel_stacktraces.cases) hence all_dyn_prefix_\2\<^sub>g: "list_all (\x. x = None) (map typeof (take (arity fd2) \2\<^sub>g))" using step_fun_end rel_st1_st2 F2_f by (auto elim!: rel_stacktraces.cases[of _ "_ # _"] list.pred_mono_strong simp: list.pred_map is_valid_fun_call_def) show ?case (is "\x. ?STEP x \ ?MATCH x") proof - let ?s1' = "State F2 H (Frame g (Suc pc\<^sub>g) (\2 @ drop (arity fd2) \2\<^sub>g) # st2')" have "?STEP ?s1'" unfolding st2_def using step_fun_end st2_def rel_st1_st2 using arities_fd1_fd2 using rel_fundef_body_length[OF rel_fd1_fd2] by (auto intro!: Subx.step_fun_end[OF \Fubx_get F2 f = Some fd2\] elim!: rel_stacktraces.cases[of _ "_ # _"]) moreover have "?MATCH ?s1'" proof - have "map typeof \2 = [None]" using step_fun_end st2_def rel_st1_st2 using rel_fd1_fd2 sp_full sp_prefix by (auto elim!: rel_stacktraces.cases[of _ "_ # _"]) thus ?thesis using step_fun_end st2_def rel_st1_st2 using arities_fd1_fd2 \1_def F2_f all_dyn_prefix_\2\<^sub>g by (auto intro!: match.intros rel_stacktraces.intros intro: rel_F1_F2 sp_F2 elim!: rel_stacktraces.cases[of _ "_ # _"] dest: list_all_eq_const_imp_replicate simp: take_Suc_conv_app_nth Let_def drop_norm_stack take_map drop_map simp: is_valid_fun_call_def) qed ultimately show ?thesis by auto qed qed qed qed lemma match_final_forward: "s1 \ s2 \ Sinca.final s1 \ Subx.final s2" proof (induction s1 s2 rule: match.induct) case (1 F1 F2 st1 st2 H) obtain f fd1 pc \1 where st1_def: "st1 = [Frame f pc \1]" and F1_f: "Finca_get F1 f = Some fd1" and pc_def: "pc = length (body fd1)" using \Sinca.final (State F1 H st1)\ by (auto elim: Sinca.final.cases) obtain \2 where st2_def: "st2 = [Frame f pc \2]" using \rel_stacktraces (Fubx_get F2) st1 st2 None\ unfolding st1_def by (auto elim: rel_stacktraces.cases) obtain fd2 where F2_f: "Fubx_get F2 f = Some fd2" and rel_fd1_fd2: "rel_fundef norm_eq fd1 fd2" using rel_fundefs_Some1[OF \rel_fundefs (Finca_get F1) (Fubx_get F2)\ F1_f] by auto have "length (body fd1) = length (body fd2)" using rel_fd1_fd2 by simp thus ?case unfolding st2_def pc_def using F2_f by (auto intro: Subx.final.intros) qed sublocale inca_ubx_forward_simulation: forward_simulation Sinca.step Subx.step Sinca.final Subx.final "\_ _. False" "\_. match" using match_final_forward forward_lockstep_simulation using lockstep_to_plus_forward_simulation[of match Sinca.step _ Subx.step] by unfold_locales auto section \Bisimulation\ sublocale inca_ubx_bisimulation: bisimulation Sinca.step Subx.step Sinca.final Subx.final "\_ _. False" "\_. match" by unfold_locales end end diff --git a/thys/Interpreter_Optimizations/OpUbx.thy b/thys/Interpreter_Optimizations/OpUbx.thy --- a/thys/Interpreter_Optimizations/OpUbx.thy +++ b/thys/Interpreter_Optimizations/OpUbx.thy @@ -1,43 +1,45 @@ theory OpUbx imports OpInl Unboxed begin section \n-ary operations\ locale nary_operations_ubx = nary_operations_inl \\ \\\\\ \\\\\ \\\ \\\\\ \
\\\\ + - unboxedval is_true is_false box_num unbox_num box_bool unbox_bool + unboxedval is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2 for \\ :: "'op \ 'dyn list \ 'dyn" and \\\\\ and \\\\\ and \\\ and \\\\\ and \
\\\\ :: "'opinl \ 'op" and - is_true :: "'dyn \ bool" and is_false and box_num and unbox_num and box_bool and unbox_bool + + is_true :: "'dyn \ bool" and is_false and + box_ubx1 :: "'ubx1 \ 'dyn" and unbox_ubx1 and + box_ubx2 :: "'ubx2 \ 'dyn" and unbox_ubx2 + fixes - \\\\\ :: "'opubx \ 'dyn unboxed list \ 'dyn unboxed option" and + \\\\\ :: "'opubx \ ('dyn, 'ubx1, 'ubx2) unboxed list \ ('dyn, 'ubx1, 'ubx2) unboxed option" and \\\ :: "'opinl \ type option list \ 'opubx option" and \\\ :: "'opubx \ 'opinl" and \\\\\\\\ :: "'opubx \ type option list \ type option" assumes \\\_invertible: "\\\ opinl ts = Some opubx \ \\\ opubx = opinl" and \\\\\_correct: "\\\\\ opubx \ = Some z \ \\\\\ (\\\ opubx) (map norm_unboxed \) = norm_unboxed z" and \\\\\_to_\\\: "\\\\\ opubx \ = Some z \ \\\ (\
\\\\ (\\\ opubx)) (map norm_unboxed \) = Some (\\\ opubx)" and \\\\\\\\_\\\\\: "\\\\\ (\
\\\\ (\\\ opubx)) = length (fst (\\\\\\\\ opubx))" and \\\_opubx_type: "\\\ opinl ts = Some opubx \ fst (\\\\\\\\ opubx) = ts" and \\\\\\\\_correct: "\\\\\\\\ opubx = (map typeof xs, \) \ \y. \\\\\ opubx xs = Some y \ typeof y = \" and \\\\\\\\_complete: "\\\\\ opubx xs = Some y \ \\\\\\\\ opubx = (map typeof xs, typeof y)" begin end end \ No newline at end of file diff --git a/thys/Interpreter_Optimizations/Op_example.thy b/thys/Interpreter_Optimizations/Op_example.thy --- a/thys/Interpreter_Optimizations/Op_example.thy +++ b/thys/Interpreter_Optimizations/Op_example.thy @@ -1,241 +1,241 @@ theory Op_example imports OpUbx Ubx_type_inference Global Unboxed_lemmas begin section \Dynamic values\ datatype dynamic = DNil | DBool bool | DNum nat definition is_true where "is_true d = (d = DBool True)" definition is_false where "is_false d = (d = DBool False)" definition box_bool :: "bool \ dynamic" where "box_bool = DBool" definition box_num :: "nat \ dynamic" where "box_num = DNum" fun unbox_num :: "dynamic \ nat option" where "unbox_num (DNum n) = Some n" | "unbox_num _ = None" fun unbox_bool :: "dynamic \ bool option" where "unbox_bool (DBool b) = Some b" | "unbox_bool _ = None" interpretation unboxed_dynamic: unboxedval is_true is_false box_num unbox_num box_bool unbox_bool proof (unfold_locales; (simp add: is_true_def is_false_def)?) fix d n show "unbox_num d = Some n \ box_num n = d" by (cases d; simp add: box_num_def) next fix d b show "unbox_bool d = Some b \ box_bool b = d" by (cases d; simp add: box_bool_def) qed section \Normal operations\ datatype op = OpNeg | OpAdd | OpMul fun ar :: "op \ nat" where "ar OpNeg = 1" | "ar OpAdd = 2" | "ar OpMul = 2" fun eval_Neg :: "dynamic list \ dynamic" where "eval_Neg [DBool b] = DBool (\b)" | "eval_Neg [_] = DNil" fun eval_Add :: "dynamic list \ dynamic" where "eval_Add [DBool x, DBool y] = DBool (x \ y)" | "eval_Add [DNum x, DNum y] = DNum (x + y)" | "eval_Add [_, _] = DNil" fun eval_Mul :: "dynamic list \ dynamic" where "eval_Mul [DBool x, DBool y] = DBool (x \ y)" | "eval_Mul [DNum x, DNum y] = DNum (x * y)" | "eval_Mul [_, _] = DNil" fun eval :: "op \ dynamic list \ dynamic" where "eval OpNeg = eval_Neg" | "eval OpAdd = eval_Add" | "eval OpMul = eval_Mul" lemma eval_arith_domain: "length xs = ar op \ \y. eval op xs = y" by simp interpretation op_Op: nary_operations eval ar using eval_arith_domain by (unfold_locales; simp) section \Inlined operations\ datatype opinl = OpAddNum | OpMulNum fun inl :: "op \ dynamic list \ opinl option" where "inl OpAdd [DNum _, DNum _] = Some OpAddNum" | "inl OpMul [DNum _, DNum _] = Some OpMulNum" | "inl _ _ = None" inductive isinl :: "opinl \ dynamic list \ bool" where "isinl OpAddNum [DNum _, DNum _]" | "isinl OpMulNum [DNum _, DNum _]" fun deinl :: "opinl \ op" where "deinl OpAddNum = OpAdd" | "deinl OpMulNum = OpMul" lemma inl_inj: "inj inl" unfolding inj_def proof (intro allI impI) fix x y assume "inl x = inl y" thus "x = y" unfolding fun_eq_iff by (cases x; cases y; auto elim: inl.elims simp: HOL.eq_commute[of None]) qed lemma inl_invertible: "inl op xs = Some opinl \ deinl opinl = op" by (induction op xs rule: inl.induct; simp) fun eval_AddNum :: "dynamic list \ dynamic" where "eval_AddNum [DNum x, DNum y] = DNum (x + y)" | "eval_AddNum [DBool x, DBool y] = DBool (x \ y)" | "eval_AddNum [_, _] = DNil" fun eval_MulNum :: "dynamic list \ dynamic" where "eval_MulNum [DNum x, DNum y] = DNum (x * y)" | "eval_MulNum [DBool x, DBool y] = DBool (x \ y)" | "eval_MulNum [_, _] = DNil" fun eval_inl :: "opinl \ dynamic list \ dynamic" where "eval_inl OpAddNum = eval_AddNum" | "eval_inl OpMulNum = eval_MulNum" lemma eval_AddNum_correct: "length xs = 2 \ eval_AddNum xs = eval_Add xs" by (induction xs rule: eval_AddNum.induct; simp) lemma eval_MulNum_correct: "length xs = 2 \ eval_MulNum xs = eval_Mul xs" by (induction xs rule: eval_MulNum.induct; simp) lemma eval_inl_correct: "length xs = ar (deinl opinl) \ eval_inl opinl xs = eval (deinl opinl) xs" using eval_AddNum_correct eval_MulNum_correct by (cases opinl; simp) lemma inl_isinl: "inl op xs = Some opinl \ isinl opinl xs" by (induction op xs rule: inl.induct; auto intro: isinl.intros) interpretation op_OpInl: nary_operations_inl eval ar eval_inl inl isinl deinl using inl_invertible using eval_inl_correct using inl_isinl by (unfold_locales; simp) section \Unboxed operations\ datatype opubx = OpAddNumUbx fun ubx :: "opinl \ type option list \ opubx option" where - "ubx OpAddNum [Some Num, Some Num] = Some OpAddNumUbx" | + "ubx OpAddNum [Some Ubx1, Some Ubx1] = Some OpAddNumUbx" | "ubx _ _ = None" fun deubx :: "opubx \ opinl" where "deubx OpAddNumUbx = OpAddNum" lemma ubx_invertible: "ubx opinl xs = Some opubx \ deubx opubx = opinl" by (induction opinl xs rule: ubx.induct; simp) -fun eval_AddNumUbx :: "dynamic unboxed list \ dynamic unboxed option" where - "eval_AddNumUbx [OpNum x, OpNum y] = Some (OpNum (x + y))" | +fun eval_AddNumUbx :: "(dynamic, nat, bool) unboxed list \ (dynamic, nat, bool) unboxed option" where + "eval_AddNumUbx [OpUbx1 x, OpUbx1 y] = Some (OpUbx1 (x + y))" | "eval_AddNumUbx _ = None" -fun eval_ubx :: "opubx \ dynamic unboxed list \ dynamic unboxed option" where +fun eval_ubx :: "opubx \ (dynamic, nat, bool) unboxed list \ (dynamic, nat, bool) unboxed option" where "eval_ubx OpAddNumUbx = eval_AddNumUbx" lemma eval_ubx_correct: "eval_ubx opubx xs = Some z \ eval_inl (deubx opubx) (map unboxed_dynamic.norm_unboxed xs) = unboxed_dynamic.norm_unboxed z" apply (cases opubx; simp) apply (induction xs rule: eval_AddNumUbx.induct; auto) by (simp add: box_num_def) lemma eval_ubx_to_inl: assumes "eval_ubx opubx \ = Some z" shows "inl (deinl (deubx opubx)) (map unboxed_dynamic.norm_unboxed \) = Some (deubx opubx)" proof (cases opubx) case OpAddNumUbx then have "eval_AddNumUbx \ = Some z" using assms by simp then show ?thesis using OpAddNumUbx apply (induction \ rule: eval_AddNumUbx.induct; simp) by (simp add: box_num_def) qed subsection \Abstract interpretation\ fun typeof_opubx :: "opubx \ type option list \ type option" where - "typeof_opubx OpAddNumUbx = ([Some Num, Some Num], Some Num)" + "typeof_opubx OpAddNumUbx = ([Some Ubx1, Some Ubx1], Some Ubx1)" lemma ubx_imp_typeof_opubx: "ubx opinl ts = Some opubx \ fst (typeof_opubx opubx) = ts" by (induction opinl ts rule: ubx.induct; simp) lemma typeof_opubx_correct: "typeof_opubx opubx = (map typeof xs, codomain) \ \y. eval_ubx opubx xs = Some y \ typeof y = codomain" proof (induction opubx) case OpAddNumUbx - obtain n1 n2 where xs_def: "xs = [OpNum n1, OpNum n2]" and "codomain = Some Num" + obtain n1 n2 where xs_def: "xs = [OpUbx1 n1, OpUbx1 n2]" and "codomain = Some Ubx1" using OpAddNumUbx[symmetric] by (auto dest!: typeof_unboxed_inversion) then show ?case by simp qed lemma typeof_opubx_complete: "eval_ubx opubx xs = Some y \ typeof_opubx opubx = (map typeof xs, typeof y)" proof (induction opubx) case OpAddNumUbx then show ?case by (auto elim: eval_AddNumUbx.elims) qed lemma typeof_opubx_ar: "length (fst (typeof_opubx opubx)) = ar (deinl (deubx opubx))" by (induction opubx; simp) interpretation op_OpUbx: nary_operations_ubx eval ar eval_inl inl isinl deinl is_true is_false box_num unbox_num box_bool unbox_bool eval_ubx ubx deubx typeof_opubx using ubx_invertible using eval_ubx_correct using eval_ubx_to_inl using ubx_imp_typeof_opubx using typeof_opubx_correct using typeof_opubx_complete using typeof_opubx_ar by (unfold_locales; (simp; fail)?) end \ No newline at end of file diff --git a/thys/Interpreter_Optimizations/Ubx.thy b/thys/Interpreter_Optimizations/Ubx.thy --- a/thys/Interpreter_Optimizations/Ubx.thy +++ b/thys/Interpreter_Optimizations/Ubx.thy @@ -1,218 +1,218 @@ theory Ubx imports Global OpUbx Env "VeriComp.Language" begin section \Unboxed caching\ -datatype ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx) instr = - IPush 'dyn | IPushNumUbx nat | IPushBoolUbx bool | +datatype ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx, 'num, 'bool) instr = + IPush 'dyn | IPushUbx1 'num | IPushUbx2 'bool | IPop | ILoad 'var | ILoadUbx type 'var | IStore 'var | IStoreUbx type 'var | IOp 'op | IOpInl 'opinl | IOpUbx 'opubx | is_jump: ICJump nat | is_fun_call: ICall 'fun locale ubx = Fenv: env F_empty F_get F_add F_to_list + Henv: env heap_empty heap_get heap_add heap_to_list + nary_operations_ubx \\ \\\\\ \\\\\ \\\ \\\\\ \
\\\\ - is_true is_false box_num unbox_num box_bool unbox_bool + is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2 \\\\\ \\\ \\\ \\\\\\\\ for \ \Functions environment\ F_empty and - F_get :: "'fenv \ 'fun \ ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx) instr fundef option" and + F_get :: "'fenv \ 'fun \ ('dyn, 'var, 'fun, 'op, 'opinl, 'opubx, 'num, 'bool) instr fundef option" and F_add and F_to_list and \ \Memory heap\ heap_empty and heap_get :: "'henv \ 'var \ 'dyn \ 'dyn option" and heap_add and heap_to_list and \ \Unboxed values\ is_true :: "'dyn \ bool" and is_false and - box_num and unbox_num and - box_bool and unbox_bool and + box_ubx1 and unbox_ubx1 and + box_ubx2 and unbox_ubx2 and \ \n-ary operations\ \\ :: "'op \ 'dyn list \ 'dyn" and \\\\\ and \\\\\ and \\\ and \\\\\ and \
\\\\ :: "'opinl \ 'op" and - \\\\\ :: "'opubx \ 'dyn unboxed list \ 'dyn unboxed option" and + \\\\\ :: "'opubx \ ('dyn, 'num, 'bool) unboxed list \ ('dyn, 'num, 'bool) unboxed option" and \\\ :: "'opinl \ type option list \ 'opubx option" and \\\ :: "'opubx \ 'opinl" and \\\\\\\\ begin fun generalize_instr where - "generalize_instr (IPushNumUbx n) = IPush (box_num n)" | - "generalize_instr (IPushBoolUbx b) = IPush (box_bool b)" | + "generalize_instr (IPushUbx1 n) = IPush (box_ubx1 n)" | + "generalize_instr (IPushUbx2 b) = IPush (box_ubx2 b)" | "generalize_instr (ILoadUbx _ x) = ILoad x" | "generalize_instr (IStoreUbx _ x) = IStore x" | "generalize_instr (IOpUbx opubx) = IOpInl (\\\ opubx)" | "generalize_instr instr = instr" fun generalize_fundef where "generalize_fundef (Fundef xs ar) = Fundef (map generalize_instr xs) ar" lemma generalize_instr_idempotent[simp]: "generalize_instr (generalize_instr x) = generalize_instr x" by (cases x) simp_all lemma generalize_instr_idempotent_comp[simp]: "generalize_instr \ generalize_instr = generalize_instr" by fastforce lemma generalize_fundef_length[simp]: "length (body (generalize_fundef fd)) = length (body fd)" by (cases fd) simp lemma body_generalize_fundef[simp]: "body (generalize_fundef fd) = map generalize_instr (body fd)" by (cases fd) simp lemma arity_generalize_fundef[simp]: "arity (generalize_fundef fd2) = arity fd2" by (cases fd2) simp -inductive final :: "('fenv, 'henv, ('fun, 'dyn unboxed) frame) state \ bool" where +inductive final where "F_get F f = Some fd \ pc = length (body fd) \ final (State F H [Frame f pc \])" subsection \Semantics\ inductive step (infix "\" 55) where step_push: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPush d \ State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpDyn d # \) # st)" | - step_push_num: - "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPushNumUbx n \ - State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpNum n # \) # st)" | + step_push_ubx1: + "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPushUbx1 n \ + State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpUbx1 n # \) # st)" | - step_push_bool: - "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPushBoolUbx b \ - State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpBool b # \) # st)" | + step_push_ubx2: + "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPushUbx2 b \ + State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpUbx2 b # \) # st)" | step_pop: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IPop \ State F H (Frame f pc (x # \) # st) \ State F H (Frame f (Suc pc) \ # st)" | step_load: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ILoad x \ cast_Dyn i = Some i' \ heap_get H (x, i') = Some d \ State F H (Frame f pc (i # \) # st) \ State F H (Frame f (Suc pc) (OpDyn d # \) # st)" | step_load_ubx_hit: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ILoadUbx \ x \ cast_Dyn i = Some i' \ heap_get H (x, i') = Some d \ unbox \ d = Some blob \ State F H (Frame f pc (i # \) # st) \ State F H (Frame f (Suc pc) (blob # \) # st)" | step_load_ubx_miss: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ILoadUbx \ x \ cast_Dyn i = Some i' \ heap_get H (x, i') = Some d \ unbox \ d = None \ F_add F f (generalize_fundef fd) = F' \ State F H (Frame f pc (i # \) # st) \ State F' H (box_stack f (Frame f (Suc pc) (OpDyn d # \) # st))" | step_store: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IStore x \ cast_Dyn i = Some i' \ cast_Dyn y = Some d \ heap_add H (x, i') d = H' \ State F H (Frame f pc (i # y # \) # st) \ State F H' (Frame f (Suc pc) \ # st)" | step_store_ubx: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IStoreUbx \ x \ cast_Dyn i = Some i' \ cast_and_box \ blob = Some d \ heap_add H (x, i') d = H' \ State F H (Frame f pc (i # blob # \) # st) \ State F H' (Frame f (Suc pc) \ # st)" | step_op: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IOp op \ \\\\\ op = ar \ ar \ length \ \ traverse cast_Dyn (take ar \) = Some \' \ \\\ op \' = None \ \\ op \' = x \ State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpDyn x # drop ar \) # st)" | step_op_inl: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IOp op \ \\\\\ op = ar \ ar \ length \ \ traverse cast_Dyn (take ar \) = Some \' \ \\\ op \' = Some opinl \ \\\\\ opinl \' = x \ F_add F f (rewrite_fundef_body fd pc (IOpInl opinl)) = F' \ State F H (Frame f pc \ # st) \ State F' H (Frame f (Suc pc) (OpDyn x # drop ar \) # st)" | step_op_inl_hit: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IOpInl opinl \ \\\\\ (\
\\\\ opinl) = ar \ ar \ length \ \ traverse cast_Dyn (take ar \) = Some \' \ \\\\\ opinl \' \ \\\\\ opinl \' = x \ State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (OpDyn x # drop ar \) # st)" | step_op_inl_miss: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IOpInl opinl \ \\\\\ (\
\\\\ opinl) = ar \ ar \ length \ \ traverse cast_Dyn (take ar \) = Some \' \ \ \\\\\ opinl \' \ \\\\\ opinl \' = x \ F_add F f (rewrite_fundef_body fd pc (IOp (\
\\\\ opinl))) = F' \ State F H (Frame f pc \ # st) \ State F' H (Frame f (Suc pc) (OpDyn x # drop ar \) # st)" | step_op_ubx: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = IOpUbx opubx \ \
\\\\ (\\\ opubx) = op \ \\\\\ op = ar \ ar \ length \ \ \\\\\ opubx (take ar \) = Some x \ State F H (Frame f pc \ # st) \ State F H (Frame f (Suc pc) (x # drop ar \) # st)" | step_cjump_true: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ICJump n \ cast_Dyn y = Some d \ is_true d \ State F H (Frame f pc (y # \) # st) \ State F H (Frame f n \ # st)" | step_cjump_false: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ICJump n \ cast_Dyn y = Some d \ is_false d \ State F H (Frame f pc (y # \) # st) \ State F H (Frame f (Suc pc) \ # st)" | step_fun_call: "F_get F f = Some fd \ pc < length (body fd) \ body fd ! pc = ICall g \ F_get F g = Some gd \ arity gd = ar \ ar \ length \ \ frame\<^sub>f = Frame f pc \ \ list_all is_dyn_operand (take ar \) \ frame\<^sub>g = Frame g 0 (take ar \) \ State F H (frame\<^sub>f # st) \ State F H (frame\<^sub>g # frame\<^sub>f # st)" | step_fun_end: "F_get F g = Some gd \ arity gd \ length \\<^sub>f \ pc\<^sub>g = length (body gd) \ frame\<^sub>g = Frame g pc\<^sub>g \\<^sub>g \ frame\<^sub>f = Frame f pc\<^sub>f \\<^sub>f \ frame\<^sub>f' = Frame f (Suc pc\<^sub>f) (\\<^sub>g @ drop (arity gd) \\<^sub>f) \ State F H (frame\<^sub>g # frame\<^sub>f # st) \ State F H (frame\<^sub>f' # st)" theorem step_deterministic: "s1 \ s2 \ s1 \ s3 \ s2 = s3" by (induction rule: step.induct; erule step.cases; safe; auto dest: is_true_and_is_false_implies_False) lemma final_finished: "final s \ finished step s" unfolding finished_def proof assume "final s" and "\x. step s x" then obtain s' where "step s s'" by auto thus False using \final s\ by (auto elim!: step.cases final.cases) qed sublocale ubx_sem: semantics step final using final_finished step_deterministic by unfold_locales inductive load :: "('fenv, 'a, 'fun) prog \ ('fenv, 'a, ('fun, 'b) frame) state \ bool" where "F_get F main = Some fd \ arity fd = 0 \ load (Prog F H main) (State F H [Frame main 0 []])" sublocale inca_lang: language step final load by unfold_locales end end \ No newline at end of file diff --git a/thys/Interpreter_Optimizations/Ubx_type_inference.thy b/thys/Interpreter_Optimizations/Ubx_type_inference.thy --- a/thys/Interpreter_Optimizations/Ubx_type_inference.thy +++ b/thys/Interpreter_Optimizations/Ubx_type_inference.thy @@ -1,210 +1,210 @@ theory Ubx_type_inference imports Result Ubx "HOL-Library.Monad_Syntax" begin section \Type of operations\ locale ubx_sp = ubx F_empty F_get F_add F_to_list heap_empty heap_get heap_add heap_to_list - is_true is_false box_num unbox_num box_bool unbox_bool + is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2 \\ \\\\\ \\\\\ \\\ \\\\\ \
\\\\ \\\\\ \\\ \\\ \\\\\\\\ for \ \Functions environment\ F_empty and F_get and F_add and F_to_list and \ \Memory heap\ heap_empty and heap_get and heap_add and heap_to_list and \ \Unboxed values\ is_true and is_false and - box_num and unbox_num and - box_bool and unbox_bool and + box_ubx1 and unbox_ubx1 and + box_ubx2 and unbox_ubx2 and \ \n-ary operations\ \\ and \\\\\ and \\\\\ and \\\ and \\\\\ and \
\\\\ and \\\\\ and \\\ and \\\ and \\\\\\\\ begin section \Strongest postcondition of instructions\ fun sp_gen_pop_push where "sp_gen_pop_push (domain, codom) \ = ( let ar = length domain in if ar \ length \ \ take ar \ = domain then Ok (codom # drop ar \) else Error () )" fun sp_instr :: "('fun \ _ fundef option) \ _ \ type option list \ (unit, type option list) result" where "sp_instr _ (IPush _) \ = Ok (None # \)" | - "sp_instr _ (IPushNumUbx _) \ = Ok (Some Num # \)" | - "sp_instr _ (IPushBoolUbx _) \ = Ok (Some Bool # \)" | + "sp_instr _ (IPushUbx1 _) \ = Ok (Some Ubx1 # \)" | + "sp_instr _ (IPushUbx2 _) \ = Ok (Some Ubx2 # \)" | "sp_instr _ IPop (_ # \) = Ok \" | "sp_instr _ (ILoad _) (None # \) = Ok (None # \)" | "sp_instr _ (ILoadUbx \ _) (None # \) = Ok (Some \ # \)" | "sp_instr _ (IStore _) (None # None # \) = Ok \" | "sp_instr _ (IStoreUbx \\<^sub>1 _) (None # Some \\<^sub>2 # \) = (if \\<^sub>1 = \\<^sub>2 then Ok \ else Error ())" | "sp_instr _ (IOp op) \ = sp_gen_pop_push (replicate (\\\\\ op) None, None) \" | "sp_instr _ (IOpInl opinl) \ = sp_gen_pop_push (replicate (\\\\\ (\
\\\\ opinl)) None, None) \" | "sp_instr _ (IOpUbx opubx) \ = sp_gen_pop_push (\\\\\\\\ opubx) \" | "sp_instr F (ICall f) \ = do { fd \ Result.of_option () (F f); sp_gen_pop_push (replicate (arity fd) None, None) \ }" | "sp_instr _ _ _ = Error ()" lemma sp_instr_no_jump: "sp_instr F instr \ = Ok type \ \ is_jump instr" by (induction instr \ rule: sp_instr.induct) simp_all lemma map_constant[simp]: "\x \ set xs. x = y \ map (\_. y) xs = xs" by (simp add: map_idI) lemma sp_generalize_instr: assumes "sp_instr F x \ = Ok \'" shows "sp_instr F (generalize_instr x) (map (\_. None) \) = Ok (map (\_. None) \')" using assms apply (induction F x \ rule: sp_instr.induct; (auto simp: Let_def take_map drop_map; fail)?) subgoal for _ opubx apply (cases "\\\\\\\\ opubx") by (auto simp add: Let_def take_map drop_map map_replicate_const \\\\\\\\_\\\\\) done lemma map_typeof_box: "map typeof (map box_operand \) = replicate (length \) None" proof (induction \) case Nil then show ?case by simp next case (Cons x xs) then show ?case by (cases x) simp_all qed section \Strongest postcondition of function definitions\ fun sp :: "('fun \ _ fundef option) \ _ list \ type option list \ (unit, type option list) result" where "sp _ [] \ = Ok \" | "sp F (instr # p) \ = do { \' \ sp_instr F instr \; sp F p \' }" lemma sp_no_jump: "sp F xs \ = Ok type \ \x \ set xs. \ is_jump x" by (induction xs arbitrary: \; auto dest: sp_instr_no_jump) lemma sp_append: "sp F (xs @ ys) \ = sp F xs \ \ sp F ys" proof (induction xs arbitrary: \) case Nil then show ?case by simp next case (Cons x xs) then show ?case by (cases "sp_instr F x \"; simp) qed lemmas sp_eq_bind_take_drop = sp_append[of _ "take n xs" "drop n xs" for n xs, unfolded append_take_drop_id] lemma sp_generalize: assumes "sp F xs \ = Ok \'" shows "sp F (map generalize_instr xs) (map (\_. None) \) = Ok (map (\_. None) \')" using assms proof (induction xs arbitrary: \ \') case Nil then show ?case using assms(1) by simp next case (Cons x xs) show ?case proof (cases "sp_instr F x \") case (Error x1) then show ?thesis using Cons.prems by auto next case (Ok \'') show ?thesis using Cons sp_generalize_instr[OF Ok] by (simp add: Ok) qed qed lemma sp_generalize2: assumes "sp F xs (replicate n None) = Ok \'" shows "sp F (map generalize_instr xs) (replicate n None) = Ok (map (\_. None) \')" using assms using sp_generalize by fastforce lemma comp_K[simp]: "(\_. x) \ f = (\_. x)" by auto lemma is_ok_sp_generalize: assumes "is_ok (sp F xs (map (\_. None) \))" shows "is_ok (sp F (map generalize_instr xs) (map (\_. None) \))" proof - from assms obtain res where 0: "sp F xs (map (\_. None) \) = Ok res" by (auto simp add: is_ok_def) show ?thesis using sp_generalize[OF 0] by simp qed lemma is_ok_sp_generalize2: assumes "is_ok (sp F xs (replicate n None))" shows "is_ok (sp F (map generalize_instr xs) (replicate n None))" using assms is_ok_sp_generalize by (metis Ex_list_of_length map_replicate_const) lemma sp_instr_op: assumes "\
\\\\ opinl = op" shows "sp_instr F (IOp op) \ = sp_instr F (IOpInl opinl) \" by (rule sp_instr.cases[of "(F, (IOp op), \)"]; simp add: Let_def assms) lemma sp_list_update: assumes "n < length xs" and "\\. sp_instr F (xs ! n) \ = sp_instr F x \" shows "sp F (xs[n := x]) = sp F xs" proof (intro ext) fix ys have "sp F (take n xs @ x # drop (Suc n) xs) ys = sp F (take n xs @ xs ! n # drop (Suc n) xs) ys" unfolding sp_append using assms(2) by (cases "sp F (take n xs) ys"; simp) thus "sp F (xs[n := x]) ys = sp F xs ys" unfolding id_take_nth_drop[OF assms(1), symmetric] unfolding upd_conv_take_nth_drop[OF assms(1), symmetric] by assumption qed lemma sp_list_update_eq_Ok: assumes "n < length xs" and "\\. sp_instr F (xs ! n) \ = sp_instr F x \" and "sp F xs ys = Ok zs" shows "sp F (xs[n := x]) ys = Ok zs" unfolding sp_list_update[OF assms(1,2)] using assms(3) by assumption lemma is_ok_sp_list_update: assumes "is_ok (sp F xs types)" and "pc < length xs" and "\\. sp_instr F (xs ! pc) \ = sp_instr F instr \" shows "is_ok (sp F (xs[pc := instr]) types)" proof - from assms(1) obtain types' where "sp F xs types = Ok types'" unfolding is_ok_def by auto thus ?thesis using sp_list_update[OF assms(2,3)] by simp qed lemmas sp_rewrite = sp_list_update[folded rewrite_def] lemmas sp_rewrite_eq_Ok = sp_list_update_eq_Ok[folded rewrite_def] lemmas is_ok_sp_rewrite = is_ok_sp_list_update[folded rewrite_def] end end \ No newline at end of file diff --git a/thys/Interpreter_Optimizations/Unboxed.thy b/thys/Interpreter_Optimizations/Unboxed.thy --- a/thys/Interpreter_Optimizations/Unboxed.thy +++ b/thys/Interpreter_Optimizations/Unboxed.thy @@ -1,65 +1,66 @@ theory Unboxed imports Global Dynamic begin -datatype type = Bool | Num +datatype type = Ubx1 | Ubx2 -datatype 'dyn unboxed = +datatype ('dyn, 'ubx1, 'ubx2) unboxed = is_dyn_operand: OpDyn 'dyn | - OpNum nat | - OpBool bool + OpUbx1 'ubx1 | + OpUbx2 'ubx2 fun typeof where "typeof (OpDyn _) = None" | - "typeof (OpNum _) = Some Num" | - "typeof (OpBool _) = Some Bool" + "typeof (OpUbx1 _) = Some Ubx1" | + "typeof (OpUbx2 _) = Some Ubx2" -fun cast_Dyn :: "'dyn unboxed \ 'dyn option" where +fun cast_Dyn where "cast_Dyn (OpDyn d) = Some d" | "cast_Dyn _ = None" -fun cast_Num :: "'dyn unboxed \ nat option" where - "cast_Num (OpNum n) = Some n" | - "cast_Num _ = None" +fun cast_Ubx1 where + "cast_Ubx1 (OpUbx1 x) = Some x" | + "cast_Ubx1 _ = None" -fun cast_Bool :: "'dyn unboxed \ bool option" where - "cast_Bool (OpBool b) = Some b" | - "cast_Bool _ = None" +fun cast_Ubx2 where + "cast_Ubx2 (OpUbx2 x) = Some x" | + "cast_Ubx2 _ = None" locale unboxedval = dynval is_true is_false for is_true :: "'dyn \ bool" and is_false + fixes - box_num :: "nat \ 'dyn" and unbox_num :: "'dyn \ nat option" and - box_bool :: "bool \ 'dyn" and unbox_bool :: "'dyn \ bool option" + box_ubx1 :: "'ubx1 \ 'dyn" and unbox_ubx1 :: "'dyn \ 'ubx1 option" and + box_ubx2 :: "'ubx2 \ 'dyn" and unbox_ubx2 :: "'dyn \ 'ubx2 option" assumes - box_unbox_inverse_num: "unbox_num d = Some n \ box_num n = d" and - box_unbox_inverse_bool: "unbox_bool d = Some b \ box_bool b = d" + box_unbox_inverse: + "unbox_ubx1 d = Some u1 \ box_ubx1 u1 = d" + "unbox_ubx2 d = Some u2 \ box_ubx2 u2 = d" begin -fun unbox :: "type \ 'dyn \ 'dyn unboxed option" where - "unbox Num = map_option OpNum \ unbox_num" | - "unbox Bool = map_option OpBool \ unbox_bool" - -fun cast_and_box :: "type \ 'dyn unboxed \ 'dyn option" where - "cast_and_box Num = map_option box_num \ cast_Num" | - "cast_and_box Bool = map_option box_bool \ cast_Bool" +fun unbox :: "type \ 'dyn \ ('dyn, 'ubx1, 'ubx2) unboxed option" where + "unbox Ubx1 = map_option OpUbx1 \ unbox_ubx1" | + "unbox Ubx2 = map_option OpUbx2 \ unbox_ubx2" -fun norm_unboxed :: "'dyn unboxed \ 'dyn" where +fun cast_and_box where + "cast_and_box Ubx1 = map_option box_ubx1 \ cast_Ubx1" | + "cast_and_box Ubx2 = map_option box_ubx2 \ cast_Ubx2" + +fun norm_unboxed where "norm_unboxed (OpDyn d) = d" | - "norm_unboxed (OpNum n) = box_num n" | - "norm_unboxed (OpBool b) = box_bool b" + "norm_unboxed (OpUbx1 x) = box_ubx1 x" | + "norm_unboxed (OpUbx2 x) = box_ubx2 x" -fun box_operand :: "'dyn unboxed \ 'dyn unboxed" where +fun box_operand where "box_operand (OpDyn d) = OpDyn d" | - "box_operand (OpNum n) = OpDyn (box_num n)" | - "box_operand (OpBool b) = OpDyn (box_bool b)" + "box_operand (OpUbx1 x) = OpDyn (box_ubx1 x)" | + "box_operand (OpUbx2 x) = OpDyn (box_ubx2 x)" fun box_frame where "box_frame f (Frame g pc \) = Frame g pc (if f = g then map box_operand \ else \)" definition box_stack where "box_stack f \ map (box_frame f)" end end \ No newline at end of file diff --git a/thys/Interpreter_Optimizations/Unboxed_lemmas.thy b/thys/Interpreter_Optimizations/Unboxed_lemmas.thy --- a/thys/Interpreter_Optimizations/Unboxed_lemmas.thy +++ b/thys/Interpreter_Optimizations/Unboxed_lemmas.thy @@ -1,89 +1,90 @@ theory Unboxed_lemmas imports Unboxed begin lemma typeof_bind_OpDyn[simp]: "typeof \ OpDyn = (\_. None)" by auto lemma is_dyn_operand_eq_typeof: "is_dyn_operand = (\x. typeof x = None)" proof (intro ext) - fix x :: "'dyn unboxed" + fix x show "is_dyn_operand x = (typeof x = None)" by (cases x; simp) qed lemma is_dyn_operand_eq_typeof_Dyn[simp]: "is_dyn_operand x \ typeof x = None" by (cases x; simp) lemma typeof_unboxed_eq_const: - fixes x :: "'dyn unboxed" + fixes x shows - "typeof x = None \ (\d :: 'dyn. x = OpDyn d)" - "typeof x = Some Num \ (\n :: nat. x = OpNum n)" - "typeof x = Some Bool \ (\b :: bool. x = OpBool b)" + "typeof x = None \ (\d. x = OpDyn d)" + "typeof x = Some Ubx1 \ (\n. x = OpUbx1 n)" + "typeof x = Some Ubx2 \ (\b. x = OpUbx2 b)" by (cases x; simp)+ lemmas typeof_unboxed_inversion = typeof_unboxed_eq_const[THEN iffD1] lemma cast_inversions: "cast_Dyn x = Some d \ x = OpDyn d" - "cast_Num x = Some n \ x = OpNum n" - "cast_Bool x = Some b \ x = OpBool b" + "cast_Ubx1 x = Some n \ x = OpUbx1 n" + "cast_Ubx2 x = Some b \ x = OpUbx2 b" by (cases x; simp)+ lemma traverse_cast_Dyn_replicate: assumes "traverse cast_Dyn xs = Some ys" shows "map typeof xs = replicate (length xs) None" using assms proof (induction xs arbitrary: ys) case Nil then show ?case by simp next case (Cons x xs) from Cons.prems show ?case by (auto intro: Cons.IH dest: cast_inversions(1) simp add: bind_eq_Some_conv) qed context unboxedval begin lemma unbox_typeof[simp]: "unbox \ d = Some blob \ typeof blob = Some \" by (cases \; auto) lemma cast_and_box_imp_typeof[simp]: "cast_and_box \ blob = Some d \ typeof blob = Some \" + using cast_inversions[of blob] by (induction \; auto dest: cast_inversions[of blob]) lemma norm_unbox_inverse[simp]: "unbox \ d = Some blob \ norm_unboxed blob = d" - using box_unbox_inverse_num box_unbox_inverse_bool + using box_unbox_inverse by (cases \; auto) lemma norm_cast_and_box_inverse[simp]: "cast_and_box \ blob = Some d \ norm_unboxed blob = d" - by (induction \; auto elim: cast_Dyn.elims cast_Num.elims cast_Bool.elims) + by (induction \; auto elim: cast_Dyn.elims cast_Ubx1.elims cast_Ubx2.elims) lemma typeof_and_norm_unboxed_imp_cast_and_box: assumes "typeof x' = Some \" "norm_unboxed x' = x" shows "cast_and_box \ x' = Some x" using assms by (induction \; induction x'; simp) lemma norm_unboxed_bind_OpDyn[simp]: "norm_unboxed \ OpDyn = id" by auto lemmas box_stack_Nil[simp] = list.map(1)[of "box_frame f" for f, folded box_stack_def] lemmas box_stack_Cons[simp] = list.map(2)[of "box_frame f" for f, folded box_stack_def] lemma typeof_box_operand[simp]: "typeof (box_operand x) = None" by (cases x; simp) lemma is_dyn_box_operand: "is_dyn_operand (box_operand x)" by (cases x) simp_all lemma is_dyn_operand_comp_box_operand[simp]: "is_dyn_operand \ box_operand = (\_. True)" using is_dyn_box_operand by auto lemma norm_box_operand[simp]: "norm_unboxed (box_operand x) = norm_unboxed x" by (cases x) simp_all end end \ No newline at end of file