1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory GraphLangLemmas 8 9imports GraphLang CommonOpsLemmas 10 11begin 12 13definition 14 get_state_function_call :: "(string \<Rightarrow> graph_function option) 15 \<Rightarrow> (next_node \<times> state \<times> string) \<Rightarrow> string option" 16where 17 "get_state_function_call Gamma x \<equiv> case x of (NextNode nn, st, fname) \<Rightarrow> 18 (case Gamma fname of Some gf \<Rightarrow> 19 (case function_graph gf nn of Some (Call _ fname' _ _) \<Rightarrow> Some fname' | _ \<Rightarrow> None) 20 | None \<Rightarrow> None) 21 | _ \<Rightarrow> None" 22 23definition 24 exec_graph_invariant :: "(string \<Rightarrow> graph_function option) \<Rightarrow> string \<Rightarrow> stack \<Rightarrow> bool" 25where 26 "exec_graph_invariant Gamma gf xs = (xs \<noteq> [] 27 \<and> (\<forall>frame \<in> set (tl xs). get_state_function_call Gamma frame \<noteq> None) 28 \<and> map (Some o snd o snd) xs = map (get_state_function_call Gamma) (tl xs) @ [Some gf])" 29 30lemma exec_graph_invariant_Cons: 31 "exec_graph_invariant Gamma fname (x # xs) = (if xs = [] then snd (snd x) = fname 32 else (get_state_function_call Gamma (hd xs) = Some (snd (snd x)) 33 \<and> exec_graph_invariant Gamma fname xs))" 34 by (cases xs, auto simp add: exec_graph_invariant_def) 35 36lemma exec_step_invariant: 37 "(stack, stack') \<in> exec_graph_step Gamma 38 \<Longrightarrow> exec_graph_invariant Gamma gf stack 39 \<Longrightarrow> exec_graph_invariant Gamma gf stack'" 40 by (auto simp: all_exec_graph_step_cases exec_graph_invariant_Cons 41 get_state_function_call_def 42 split: graph_function.split_asm) 43 44lemma exec_trace_invariant': 45 "tr \<in> exec_trace Gamma gf 46 \<Longrightarrow> (\<forall>stack. tr i = Some stack 47 \<longrightarrow> exec_graph_invariant Gamma gf stack)" 48 apply (induct i) 49 apply (clarsimp simp: exec_trace_def exec_graph_invariant_def) 50 apply (clarsimp split: next_node.split_asm list.split_asm) 51 apply (clarsimp simp: exec_trace_def nat_trace_rel_def) 52 apply (drule_tac x=i in spec, clarsimp) 53 apply (auto elim: exec_step_invariant) 54 done 55 56lemmas exec_trace_invariant = exec_trace_invariant'[rule_format] 57 58lemma exec_trace_Nil: 59 "tr \<in> exec_trace Gamma gf \<Longrightarrow> tr i \<noteq> Some []" 60 apply safe 61 apply (drule(1) exec_trace_invariant) 62 apply (simp add: exec_graph_invariant_def) 63 done 64 65lemma exec_trace_step_cases: 66 assumes exec: "tr \<in> exec_trace Gamma gf" 67 shows "((tr i = None \<and> tr (Suc i) = None)) 68 \<or> (\<exists>state. tr i = Some [state] \<and> fst state \<in> {Ret, Err} \<and> tr (Suc i) = None) 69 \<or> (tr i \<noteq> None \<and> tr (Suc i) \<noteq> None \<and> (the (tr i), the (tr (Suc i))) \<in> exec_graph_step Gamma)" 70 using exec exec_trace_Nil[OF exec] 71 apply (clarsimp simp: exec_trace_def nat_trace_rel_def continuing_def Ball_def) 72 apply (drule_tac x=i in spec)+ 73 apply (auto split: list.split_asm option.split_asm prod.split_asm next_node.split_asm)[1] 74 done 75 76definition 77 reachable_step :: "(nat \<Rightarrow> node option) \<Rightarrow> (next_node \<times> next_node) set" 78where 79 "reachable_step graph = {(s, t). (case s of NextNode i \<Rightarrow> 80 (case graph i of None \<Rightarrow> False 81 | Some (Cond l r _) \<Rightarrow> (t = l \<or> t = r) 82 | Some (Basic c _) \<Rightarrow> t = c 83 | Some (Call c _ _ _) \<Rightarrow> t = c \<or> t = Err) | _ \<Rightarrow> False)}" 84 85abbreviation 86 "reachable_step' gf \<equiv> reachable_step (function_graph gf)" 87 88lemma exec_trace_None_dom_subset: 89 "tr n = None \<Longrightarrow> tr \<in> exec_trace Gamma f 90 \<Longrightarrow> dom tr \<subseteq> {..< n}" 91 unfolding exec_trace_def 92 by (blast elim: CollectE dest: trace_None_dom_subset) 93 94lemma trace_Some_dom_superset: 95 "tr \<in> nat_trace_rel c R 96 \<Longrightarrow> tr i = Some v 97 \<Longrightarrow> {..i} \<subseteq> dom tr" 98 apply (clarsimp, rule ccontr, clarsimp) 99 apply (drule(1) trace_None_dom_subset) 100 apply auto 101 done 102 103lemma nat_trace_rel_final: 104 "tr \<in> nat_trace_rel c R 105 \<Longrightarrow> tr i = Some v 106 \<Longrightarrow> \<not> c' v 107 \<Longrightarrow> restrict_map tr {.. i} \<in> nat_trace_rel c' R" 108 apply (frule(1) trace_Some_dom_superset) 109 apply (clarsimp simp: nat_trace_rel_def restrict_map_def Suc_le_eq) 110 apply (drule_tac c="Suc n" in subsetD, auto) 111 done 112 113lemma trace_None_dom_eq: 114 "tr n = None \<Longrightarrow> tr \<in> nat_trace_rel cont R 115 \<Longrightarrow> (\<exists>n'. n' \<le> n \<and> dom tr = {..< n'})" 116 apply (cases "\<forall>i. tr i = None") 117 apply (rule_tac x=0 in exI) 118 apply (simp add: fun_eq_iff) 119 apply clarsimp 120 apply (rule_tac x="Suc (Max (dom tr))" in exI) 121 apply (drule(1) nat_trace_Max_dom_None[rotated, simplified, OF exI]) 122 apply clarsimp 123 apply (frule(1) trace_None_dom_subset) 124 apply (rule conjI) 125 apply auto[1] 126 apply (rule equalityI) 127 apply (auto simp: less_Suc_eq_le intro!: Max_ge elim: finite_subset)[1] 128 apply (clarsimp, rule ccontr, clarsimp simp: less_Suc_eq_le) 129 apply (drule(1) trace_None_dom_subset)+ 130 apply auto 131 done 132 133lemma trace_end_eq_Some: 134 "tr \<in> nat_trace_rel c R 135 \<Longrightarrow> tr i = Some v 136 \<Longrightarrow> tr (Suc i) = None 137 \<Longrightarrow> trace_end tr = Some v" 138 apply (frule(1) trace_Some_dom_superset) 139 apply (frule(1) trace_None_dom_eq) 140 apply (clarsimp simp: le_Suc_eq lessThan_Suc_atMost[symmetric]) 141 apply (simp add: trace_end_def) 142 apply (subst Max_eqI[where x=i], simp_all) 143 apply auto 144 done 145 146lemma trace_end_cut: 147 "tr \<in> nat_trace_rel c R 148 \<Longrightarrow> tr i = Some v 149 \<Longrightarrow> trace_end (restrict_map tr {.. i}) = Some v" 150 apply (frule(1) trace_Some_dom_superset) 151 apply (simp add: trace_end_def Int_absorb1) 152 apply (subst Max_eqI[where x=i], simp_all) 153 apply (simp add: restrict_map_def) 154 apply (metis Suc_n_not_le_n) 155 done 156 157definition 158 trace_drop_n :: "nat \<Rightarrow> nat \<Rightarrow> trace \<Rightarrow> trace" 159where 160 "trace_drop_n start n_drop tr = (\<lambda>i. if (\<forall>j < i. tr (start + j) \<noteq> None 161 \<and> continuing (rev (drop n_drop (rev (the (tr (start + j))))))) 162 then option_map (rev o drop n_drop o rev) (tr (i + start)) else None)" 163 164lemma rev_drop_step: 165 "(stack, stack') \<in> exec_graph_step Gamma 166 \<Longrightarrow> continuing (rev (drop k (rev stack))) 167 \<Longrightarrow> (rev (drop k (rev stack)), rev (drop k (rev stack'))) \<in> exec_graph_step Gamma" 168 apply (subgoal_tac "\<exists>xs ys. stack = xs @ ys \<and> k = length ys") 169 apply clarsimp 170 apply (frule(1) exec_graph_step_stack_extend[THEN iffD1]) 171 apply clarsimp 172 apply (rule_tac x="take (length stack - k) stack" in exI) 173 apply (rule_tac x="drop (length stack - k) stack" in exI) 174 apply (cases "length (rev (drop k (rev stack)))") 175 apply simp 176 apply simp 177 done 178 179lemma rev_drop_continuing: 180 "continuing (rev (drop k (rev stack))) \<Longrightarrow> continuing stack" 181 by (simp add: continuing_def split: list.split next_node.split, 182 auto simp: drop_Cons split: nat.split_asm) 183 184lemma all_less_Suc_eq: 185 "(\<forall>x < Suc i. P x) = (P i \<and> (\<forall>x < i. P x))" 186 by (auto simp: less_Suc_eq) 187 188lemma exec_trace_drop_n_Cons: 189 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn'' = Some gf" 190 shows "tr i = Some ((NextNode n, st, fn'') # xs) 191 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 192 \<Longrightarrow> Gamma fn' = Some gf' 193 \<Longrightarrow> trace_drop_n (Suc i) (Suc (length xs)) tr \<in> exec_trace Gamma fn'" 194 using tr 195 apply (clarsimp simp: exec_trace_def) 196 apply (intro conjI) 197 apply (simp add: trace_drop_n_def) 198 apply (cut_tac exec_trace_step_cases[where i=i, OF tr(1)]) 199 apply (clarsimp simp: all_exec_graph_step_cases exec_graph_invariant_Cons 200 split: graph_function.split_asm) 201 apply (clarsimp simp: nat_trace_rel_def trace_drop_n_def 202 all_less_Suc_eq 203 split del: if_split) 204 apply (cut_tac i="Suc i + na" in exec_trace_Nil[OF tr(1)]) 205 apply (drule_tac x="Suc i + na" in spec)+ 206 apply (clarsimp simp: field_simps) 207 apply (safe, simp_all) 208 apply (safe intro!: rev_drop_step) 209 apply (auto dest!: rev_drop_continuing) 210 done 211 212lemma exec_trace_drop_n: 213 assumes tr: "tr \<in> exec_trace Gamma fn" "Gamma fn = Some gf" 214 shows "tr i = Some [(NextNode n, st, fn'')] 215 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 216 \<Longrightarrow> Gamma fn' = Some gf' 217 \<Longrightarrow> trace_drop_n (Suc i) 1 tr \<in> exec_trace Gamma fn'" 218 apply (frule exec_trace_invariant[OF tr(1)]) 219 apply (simp add: exec_graph_invariant_Cons) 220 apply (drule(2) exec_trace_drop_n_Cons[OF tr]) 221 apply simp 222 done 223 224lemma exec_trace_drop_n_rest_Cons: 225 "tr \<in> exec_trace Gamma fn 226 \<Longrightarrow> tr i = Some ((NextNode n, st, fn'') # xs) 227 \<Longrightarrow> Gamma fn'' = Some gf 228 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 229 \<Longrightarrow> Gamma fn' = Some gf' 230 \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) (Suc (length xs)) tr k = Some stk 231 \<longrightarrow> tr (Suc i + k) = Some (stk @ (NextNode n, st, fn'') # xs))" 232proof (induct k) 233 case 0 show ?case using 0 234 apply (clarsimp simp: trace_drop_n_def) 235 apply (frule_tac i=i in exec_trace_step_cases) 236 apply (clarsimp simp: exec_graph_step_def exec_graph_invariant_Cons 237 split: graph_function.split_asm) 238 done 239next 240 case (Suc k) 241 have rev_drop_eq: "\<And>xs ys n. length ys = n 242 \<Longrightarrow> (xs = rev (drop n (rev xs)) @ ys) 243 = (\<exists>zs. xs = zs @ ys)" 244 by auto 245 show ?case using Suc.prems Suc.hyps 246 apply (clarsimp simp: trace_drop_n_def field_simps) 247 apply (frule_tac i="Suc k + i" in exec_trace_step_cases) 248 apply (clarsimp simp: field_simps all_less_Suc_eq rev_drop_eq) 249 apply (clarsimp simp: exec_graph_step_stack_extend) 250 done 251qed 252 253lemma exec_trace_drop_n_rest: 254 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some gf 255 \<Longrightarrow> tr i = Some [(NextNode n, st, fn'')] 256 \<Longrightarrow> function_graph gf n = Some (Call nn fn' inps outps) 257 \<Longrightarrow> Gamma fn' = Some gf' 258 \<Longrightarrow> (\<forall>stk. trace_drop_n (Suc i) 1 tr k = Some stk 259 \<longrightarrow> tr (Suc i + k) = Some (stk @ [(NextNode n, st, fn'')]))" 260 apply (frule(1) exec_trace_invariant) 261 apply (clarsimp simp: exec_graph_invariant_Cons) 262 apply (drule(4) exec_trace_drop_n_rest_Cons) 263 apply auto 264 done 265 266lemma trace_drop_n_init: 267 "tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 268 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 269 \<Longrightarrow> Gamma fname = Some f' 270 \<Longrightarrow> tr i = Some [(NextNode n, st, fn')] 271 \<Longrightarrow> trace_drop_n (Suc i) 1 tr 0 = Some [(NextNode (entry_point f'), 272 init_vars (function_inputs f') inputs st, fname)]" 273 apply (frule(1) exec_trace_invariant) 274 apply (clarsimp simp: exec_graph_invariant_Cons) 275 apply (frule_tac i=i in exec_trace_step_cases, clarsimp) 276 apply (clarsimp simp: all_exec_graph_step_cases trace_drop_n_def) 277 done 278 279lemma exec_trace_init: 280 "tr \<in> exec_trace Gamma fn 281 \<Longrightarrow> \<exists>st gf. Gamma fn = Some gf \<and> tr 0 = Some [(NextNode (entry_point gf), st, fn)]" 282 by (clarsimp simp: exec_trace_def) 283 284lemma dom_Max_None: 285 "tr \<in> exec_trace Gamma f \<Longrightarrow> (tr (Max (dom tr)) \<noteq> None)" 286 apply (rule notI) 287 apply (frule(1) exec_trace_None_dom_subset) 288 apply (cases "dom tr = {}") 289 apply (clarsimp dest!: exec_trace_init) 290 apply (drule Max_in[rotated]) 291 apply (simp add: finite_subset) 292 apply clarsimp 293 done 294 295lemma trace_end_trace_drop_n_None: 296 "trace_end (trace_drop_n i j tr) = None \<Longrightarrow> tr \<in> exec_trace Gamma f 297 \<Longrightarrow> trace_drop_n i j tr \<in> exec_trace Gamma f' 298 \<Longrightarrow> trace_end tr = None" 299 apply (clarsimp simp: trace_end_def dom_Max_None split: if_split_asm) 300 apply (rule ccontr, simp) 301 apply (drule(1) exec_trace_None_dom_subset) 302 apply (drule_tac x="n + i + 1" in spec) 303 apply (clarsimp simp: trace_drop_n_def split: if_split_asm) 304 apply auto[1] 305 done 306 307lemma trace_end_trace_drop_n_Some: 308 "trace_end (trace_drop_n (Suc i) (Suc 0) tr) = Some [(Ret, st', dontcare)] 309 \<Longrightarrow> tr \<in> exec_trace Gamma fn \<Longrightarrow> Gamma fn = Some f 310 \<Longrightarrow> function_graph f n = Some (Call nn fname inputs outputs) 311 \<Longrightarrow> Gamma fname = Some f' 312 \<Longrightarrow> tr i = Some [(NextNode n, st, fn')] 313 \<Longrightarrow> \<exists>j. tr (Suc i + j) = Some [(nn, return_vars (function_outputs f') outputs st' st, fn)] 314" 315 apply (frule(4) exec_trace_drop_n) 316 apply (drule trace_end_SomeD, fastforce simp add: exec_trace_def) 317 apply clarsimp 318 apply (frule(4) exec_trace_drop_n_rest, simp, drule spec, drule(1) mp) 319 apply simp 320 apply (frule(1) exec_trace_invariant[where stack="[a, b]" for a b]) 321 apply (clarsimp simp: exec_graph_invariant_Cons get_state_function_call_def) 322 apply (frule_tac i="Suc i + na" in exec_trace_step_cases, clarsimp) 323 apply (clarsimp simp: all_exec_graph_step_cases) 324 apply (metis add_Suc_right) 325 done 326 327end 328