theory CNodeInv_AI

lemma set_cap_id:
  "cte_wp_at ((=) c) p s \<Longrightarrow> set_cap c p s = ({((),s)}, False)" apply (clarsimp simp: cte_wp_at_cases) apply (cases p) apply (erule disjE) apply clarsimp apply (simp add: set_cap_def get_object_def bind_assoc exec_gets) apply (rule conjI) apply (clarsimp simp: set_object_def) apply (frule get_object_some) apply (drule_tac t="fun" in map_upd_triv) apply (clarsimp simp: bind_def get_def return_def put_def a_type_def) apply (cases s) apply simp apply (rule ext, simp) apply (clarsimp simp: get_object_def gets_def get_def bind_def assert_def return_def) apply clarsimp apply (simp add: set_cap_def get_object_def bind_assoc
                   exec_gets set_object_def exec_get put_def) apply (clarsimp simp: tcb_cap_cases_def
                 split: if_split_asm,
         simp_all add: map_upd_triv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cte_wp_at ((=) c) p s \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. (\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some c) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)) \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(\<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some c) \<or> (\<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)); p = (a, b)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>p = (a, b); \<exists>sz fun. kheap s (fst p) = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun (snd p) = Some c\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False)
 2. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> set_cap c (a, b) s = ({((), s)}, False)
 2. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> (b \<in> dom fun \<longrightarrow> set_object a (CNode sz (fun(b \<mapsto> c))) s = ({((), s)}, False)) \<and> (b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False))
 2. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<in> dom fun \<longrightarrow> set_object a (CNode sz (fun(b \<mapsto> c))) s = ({((), s)}, False)
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> (do kobj <- get_object a;
y <- assert (a_type kobj = a_type (CNode sz (fun(b \<mapsto> c))));
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode sz (fun(b \<mapsto> c)))\<rparr>)
od) s = ({((), s)}, False)
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c; get_object a s = ({(CNode sz fun, s)}, False)\<rbrakk> \<Longrightarrow> (do kobj <- get_object a;
y <- assert (a_type kobj = a_type (CNode sz (fun(b \<mapsto> c))));
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode sz (fun(b \<mapsto> c)))\<rparr>)
od) s = ({((), s)}, False)
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; get_object a s = ({(CNode sz fun, s)}, False); fun(b \<mapsto> c) = fun\<rbrakk> \<Longrightarrow> (do kobj <- get_object a;
y <- assert (a_type kobj = a_type (CNode sz (fun(b \<mapsto> c))));
s <- get;
put (s\<lparr>kheap := (kheap s)(a \<mapsto> CNode sz (fun(b \<mapsto> c)))\<rparr>)
od) s = ({((), s)}, False)
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; get_object a s = ({(CNode sz fun, s)}, False); fun(b \<mapsto> c) = fun\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> CNode sz fun)\<rparr> = s
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun kheapa cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; get_object a s = ({(CNode sz fun, s)}, False); fun(b \<mapsto> c) = fun; s = \<lparr>kheap = kheapa, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> CNode sz fun)\<rparr> = s
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun kheap cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state exst. \<lbrakk>p = (a, b); kheap a = Some (CNode sz fun); well_formed_cnode_n sz fun; get_object a \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr> = ({(CNode sz fun, \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>)}, False); fun(b \<mapsto> c) = fun; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, exst = exst\<rparr>\<rbrakk> \<Longrightarrow> kheap(a \<mapsto> CNode sz fun) = kheap
 2. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 3. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun. \<lbrakk>p = (a, b); kheap s a = Some (CNode sz fun); well_formed_cnode_n sz fun; fun b = Some c\<rbrakk> \<Longrightarrow> b \<notin> dom fun \<longrightarrow> fail s = ({((), s)}, False)
 2. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>p = (a, b); \<exists>tcb. kheap s (fst p) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases (snd p) = Some (get, set, restr)) \<and> c = get tcb)\<rbrakk> \<Longrightarrow> set_cap c p s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); c = get tcb; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> set_cap (get tcb) (a, b) s = ({((), s)}, False) proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get set restr. \<lbrakk>p = (a, b); kheap s a = Some (TCB tcb); c = get tcb; tcb_cap_cases b = Some (get, set, restr)\<rbrakk> \<Longrightarrow> (b = tcb_cnode_index 4 \<longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_ipcframe := get tcb\<rparr>))\<rparr> = s) \<and> (b \<noteq> tcb_cnode_index 4 \<longrightarrow> (b = tcb_cnode_index 3 \<longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_caller := get tcb\<rparr>))\<rparr> = s) \<and> (b \<noteq> tcb_cnode_index 3 \<longrightarrow> (b = tcb_cnode_index 2 \<longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_reply := get tcb\<rparr>))\<rparr> = s) \<and> (b \<noteq> tcb_cnode_index 2 \<longrightarrow> (b = tcb_cnode_index (Suc 0) \<longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_vtable := get tcb\<rparr>))\<rparr> = s) \<and> (b \<noteq> tcb_cnode_index (Suc 0) \<longrightarrow> (b = tcb_cnode_index 0 \<longrightarrow> s\<lparr>kheap := (kheap s)(a \<mapsto> TCB (tcb\<lparr>tcb_ctable := get tcb\<rparr>))\<rparr> = s) \<and> (b \<noteq> tcb_cnode_index 0 \<longrightarrow> fail s = ({((), s)}, False)))))) proof (prove)
goal:
No subgoals!