theory CSpace_All

lemma lookupTargetSlot_ccorres':
  "ccorres
   (syscall_error_rel \<currency>  (\<lambda>w w'. w'= Ptr w \<and> depth \<le> word_bits)) lookupSlot_xf
   (\<lambda>s.  valid_pspace' s \<and> s  \<turnstile>' croot \<and>  depth < 2 ^ word_bits)
   (UNIV \<inter> {s. capptr_' s = capptr} \<inter>
            {s. ccap_relation croot (root_' s)} \<inter>
            {s. depth_' s = of_nat depth} ) []
  (lookupTargetSlot croot capptr depth)
  (Call lookupTargetSlot_'proc)" apply (cinit lift: capptr_' root_' depth_') apply (rule ccorres_trim_returnE) apply simp apply simp apply (ctac add: lookupSlotForCNodeOp_ccorres') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (\<lambda>s. valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) (UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>) [] (lookupTargetSlot croot capptr depth) (Call lookupTargetSlot_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>deptha root capptra. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (?Q146 deptha root capptra) (?Q'146 deptha root capptra) [SKIP] (lookupSlotForCNodeOp False croot capptr depth) (\<acute>ret__struct_lookupSlot_ret_C :== CALL lookupSlotForCNodeOp_'proc(SCAST(32 signed \<rightarrow> 32) false,root,capptra,deptha);;
return_C ret__struct_lookupSlot_ret_C_'_update ret__struct_lookupSlot_ret_C_')
 2. \<And>deptha root capptra s s'. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q146 deptha root capptra s \<and> s' \<in> ?Q'146 deptha root capptra proof (prove)
goal (4 subgoals):
 1. \<And>deptha root capptra s. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> s\<lparr>ret__struct_lookupSlot_ret_C_' := ret__struct_lookupSlot_ret_C_' s\<rparr> = s
 2. \<And>deptha root capptra f s. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ret__struct_lookupSlot_ret_C_' (global_exn_var_'_update f s) = ret__struct_lookupSlot_ret_C_' s
 3. \<And>deptha root capptra. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (?Q146 deptha root capptra) (?Q'146 deptha root capptra) [SKIP] (lookupSlotForCNodeOp False croot capptr depth) (\<acute>ret__struct_lookupSlot_ret_C :== CALL lookupSlotForCNodeOp_'proc(SCAST(32 signed \<rightarrow> 32) false,root,capptra,deptha))
 4. \<And>deptha root capptra s s'. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q146 deptha root capptra s \<and> s' \<in> ?Q'146 deptha root capptra proof (prove)
goal (3 subgoals):
 1. \<And>deptha root capptra f s. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ret__struct_lookupSlot_ret_C_' (global_exn_var_'_update f s) = ret__struct_lookupSlot_ret_C_' s
 2. \<And>deptha root capptra. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (?Q146 deptha root capptra) (?Q'146 deptha root capptra) [SKIP] (lookupSlotForCNodeOp False croot capptr depth) (\<acute>ret__struct_lookupSlot_ret_C :== CALL lookupSlotForCNodeOp_'proc(SCAST(32 signed \<rightarrow> 32) false,root,capptra,deptha))
 3. \<And>deptha root capptra s s'. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q146 deptha root capptra s \<and> s' \<in> ?Q'146 deptha root capptra proof (prove)
goal (2 subgoals):
 1. \<And>deptha root capptra. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr\<rbrakk> \<Longrightarrow> ccorres (syscall_error_rel \<currency> (\<lambda>w w'. w' = cte_Ptr w \<and> depth \<le> word_bits)) (liftxf errstate lookupSlot_ret_C.status_C lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_') (?Q146 deptha root capptra) (?Q'146 deptha root capptra) [SKIP] (lookupSlotForCNodeOp False croot capptr depth) (\<acute>ret__struct_lookupSlot_ret_C :== CALL lookupSlotForCNodeOp_'proc(SCAST(32 signed \<rightarrow> 32) false,root,capptra,deptha))
 2. \<And>deptha root capptra s s'. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q146 deptha root capptra s \<and> s' \<in> ?Q'146 deptha root capptra proof (prove)
goal (1 subgoal):
 1. \<And>deptha root capptra s s'. \<lbrakk>deptha = word_of_nat depth; ccap_relation croot root; capptra = capptr; (s, s') \<in> rf_sr; valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (valid_pspace' s \<and> valid_cap' croot s \<and> depth < 2 ^ word_bits) \<and> s' \<in> {s. depth_'_update (\<lambda>_. deptha) (capptr_'_update (\<lambda>_. capptra) (root_'_update (\<lambda>_. root) (isSource_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) false) s))) \<in> UNIV \<inter> \<lbrace>\<acute>capptr = capptr\<rbrace> \<inter> \<lbrace>to_bool \<acute>isSource = False\<rbrace> \<inter> \<lbrace>ccap_relation croot \<acute>root\<rbrace> \<inter> \<lbrace>\<acute>depth = word_of_nat depth\<rbrace>} proof (prove)
goal:
No subgoals!