theory Invoke_C

lemma invokeCNodeInsert_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src
                     and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap)
       (UNIV \<inter> {s. destSlot_' s = Ptr dest} \<inter>
               {s. srcSlot_' s = Ptr src} \<inter>
               {s. ccap_relation cap (cap_' s)}) []
       (invokeCNode (Insert cap src dest))
  (Call invokeCNodeInsert_'proc)" apply (cinit lift: destSlot_' srcSlot_' cap_' simp del: return_bind cong:call_ignore_cong) apply (simp add: liftE_def) apply (ctac (no_vcg) add: cteInsert_ccorres) apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def) apply wp apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) (UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr dest\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = cte_Ptr src\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace>) [] (invokeCNode (Insert cap src dest)) (Call invokeCNodeInsert_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q145 capa srcSlot destSlot) (?Q'145 capa srcSlot destSlot) [SKIP] (liftE (cteInsert cap src dest)) (CALL cteInsert_'proc(capa,srcSlot,destSlot);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q145 capa srcSlot destSlot s \<and> s' \<in> ?Q'145 capa srcSlot destSlot proof (prove)
goal (2 subgoals):
 1. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q145 capa (cte_Ptr src) (cte_Ptr dest)) (?Q'145 capa (cte_Ptr src) (cte_Ptr dest)) [SKIP] (do r <- cteInsert cap src dest;
return (Inr ())
od) (CALL cteInsert_'proc(capa,cte_Ptr src,cte_Ptr dest);;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q145 capa srcSlot destSlot s \<and> s' \<in> ?Q'145 capa srcSlot destSlot proof (prove)
goal (3 subgoals):
 1. \<And>capa srcSlot destSlot rv xfdc. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; dc rv xfdc\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q156 capa srcSlot destSlot rv) (?Q'170 capa rv xfdc) [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> \<lbrace>?R164 capa (cte_Ptr src) (cte_Ptr dest)\<rbrace> cteInsert cap src dest \<lbrace>?Q156 capa srcSlot destSlot\<rbrace>
 3. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and ?R164 capa srcSlot destSlot) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'169 capa srcSlot destSlot t rv}
flex-flex pairs:
\<lambda>capa t rv. ?Q'170 capa rv (xfdc t) \<equiv>\<^sup>? \<lambda>capa. ?Q'169 capa (cte_Ptr src) (cte_Ptr dest) proof (prove)
goal (3 subgoals):
 1. \<And>capa srcSlot destSlot rv xfdc. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; dc rv xfdc\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> \<lbrace>?R164 capa (cte_Ptr src) (cte_Ptr dest)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and ?R164 capa srcSlot destSlot) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>capa srcSlot destSlot rv xfdc \<sigma>. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; dc rv xfdc\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> \<lbrace>?R164 capa (cte_Ptr src) (cte_Ptr dest)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and ?R164 capa srcSlot destSlot) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV} proof (prove)
goal (3 subgoals):
 1. \<And>capa \<sigma> x. \<lbrakk>ccap_relation cap capa; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (return (Inr ()) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (\<lambda>y. ()) ret__unsigned_long_' (x\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> \<lbrace>?R164 capa (cte_Ptr src) (cte_Ptr dest)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and ?R164 capa srcSlot destSlot) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV} proof (prove)
goal (2 subgoals):
 1. \<And>capa srcSlot destSlot. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest\<rbrakk> \<Longrightarrow> \<lbrace>?R164 capa (cte_Ptr src) (cte_Ptr dest)\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and ?R164 capa srcSlot destSlot) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV} proof (prove)
goal (1 subgoal):
 1. \<And>capa srcSlot destSlot s s'. \<lbrakk>ccap_relation cap capa; srcSlot = cte_Ptr src; destSlot = cte_Ptr dest; (s, s') \<in> rf_sr; (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap) src and valid_mdb' and pspace_aligned' and valid_objs' and valid_cap' cap) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' (\<lambda>scte. capMasterCap (cteCap scte) = capMasterCap cap \<or> is_simple_cap' cap) src and valid_mdb' and valid_objs' and pspace_aligned' and valid_cap' cap and cte_wp_at' (\<lambda>c. True) src and (\<lambda>a. True)) s \<and> s' \<in> {s. destSlot_'_update (\<lambda>_. destSlot) (srcSlot_'_update (\<lambda>_. srcSlot) (newCap_'_update (\<lambda>_. capa) s)) \<in> UNIV \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace> \<inter> \<lbrace>\<acute>destSlot = destSlot\<rbrace> \<inter> \<lbrace>\<acute>srcSlot = srcSlot\<rbrace> \<inter> \<lbrace>ccap_relation cap \<acute>newCap\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV} proof (prove)
goal:
No subgoals!