theory Arch_C

lemma pdeCheckIfMapped_ccorres:
  "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' \<top>
    (UNIV \<inter> {s. pde___ptr_to_struct_pde_C_' s = Ptr slot}) []
    (pdeCheckIfMapped slot)
    (Call pdeCheckIfMapped_'proc)" apply (cinit lift: pde___ptr_to_struct_pde_C_') apply (rule ccorres_pre_getObject_pde) apply (rule_tac P'="{s. \<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde'}"
     in ccorres_from_vcg_throws[where P="\<lambda>s. True"]) apply simp_all apply clarsimp apply (rule conseqPre, vcg) apply (clarsimp simp: typ_heap_simps' return_def) apply (case_tac pd, simp_all add: cpde_relation_invalid isInvalidPDE_def
                             split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (\<lambda>_. True) (UNIV \<inter> \<lbrace>\<acute>pde___ptr_to_struct_pde_C = pde_Ptr slot\<rbrace>) [] (pdeCheckIfMapped slot) (Call pdeCheckIfMapped_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pde___ptr_to_struct_pde_C. pde___ptr_to_struct_pde_C = pde_Ptr slot \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q56 pde___ptr_to_struct_pde_C) (?Q'56 pde___ptr_to_struct_pde_C) [SKIP] (do pd <- getObject slot;
return (pd \<noteq> ARM_H.InvalidPDE)
od) (\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pde___ptr_to_struct_pde_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>pde___ptr_to_struct_pde_C s s'. \<lbrakk>pde___ptr_to_struct_pde_C = pde_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q56 pde___ptr_to_struct_pde_C s \<and> s' \<in> ?Q'56 pde___ptr_to_struct_pde_C proof (prove)
goal (2 subgoals):
 1. \<And>pde___ptr_to_struct_pde_C pd. pde___ptr_to_struct_pde_C = pde_Ptr slot \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P62 pde___ptr_to_struct_pde_C pd) (?P'62 pde___ptr_to_struct_pde_C pd) [SKIP] (return (pd \<noteq> ARM_H.InvalidPDE)) (\<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pde___ptr_to_struct_pde_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>pde___ptr_to_struct_pde_C s s'. \<lbrakk>pde___ptr_to_struct_pde_C = pde_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde slot s \<longrightarrow> ?P62 pde___ptr_to_struct_pde_C pde s) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> ?P'62 pde___ptr_to_struct_pde_C pde} proof (prove)
goal (2 subgoals):
 1. \<And>pde___ptr_to_struct_pde_C pd. pde___ptr_to_struct_pde_C = pde_Ptr slot \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> {s. \<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde'} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pde___ptr_to_struct_pde_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (pd \<noteq> ARM_H.InvalidPDE) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = to_bool (ret__unsigned_long_' s)}
 2. \<And>pde___ptr_to_struct_pde_C s s'. \<lbrakk>pde___ptr_to_struct_pde_C = pde_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pde. ko_at' pde slot s \<longrightarrow> True) \<and> s' \<in> {s. \<forall>pde pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pde pde' \<longrightarrow> s \<in> {s. \<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pde pde'}} proof (prove)
goal (1 subgoal):
 1. \<And>pde___ptr_to_struct_pde_C pd. pde___ptr_to_struct_pde_C = pde_Ptr slot \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde') \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pde_Ptr slot);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>x\<in>fst (return (pd \<noteq> ARM_H.InvalidPDE) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr \<and> rv = to_bool (ret__unsigned_long_' s)} proof (prove)
goal (1 subgoal):
 1. \<And>pd \<sigma>. \<Gamma>\<turnstile> {s. (\<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde') \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned :== CALL pde_ptr_get_pdeType_'proc(pde_Ptr slot);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>x\<in>fst (return (pd \<noteq> ARM_H.InvalidPDE) \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr \<and> rv = to_bool (ret__unsigned_long_' s)} proof (prove)
goal (1 subgoal):
 1. \<And>pd \<sigma>. {s. (\<exists>pde'. cslift s (pde_Ptr slot) = Some pde' \<and> cpde_relation pd pde') \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c pde_Ptr slot \<and> (\<forall>t. ret__unsigned_' t = pde_get_tag (the (cslift s (pde_Ptr slot))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (pd \<noteq> ARM_H.InvalidPDE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_' := pde_get_tag (the (cslift s (pde_Ptr slot))), ret__unsigned_long_' := if pde_get_tag (the (cslift s (pde_Ptr slot))) \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> rv = to_bool (if pde_get_tag (the (cslift s (pde_Ptr slot))) \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)))} proof (prove)
goal (1 subgoal):
 1. \<And>pd \<sigma> x pde' t. \<lbrakk>(\<sigma>, x) \<in> rf_sr; cslift x (pde_Ptr slot) = Some pde'; cpde_relation pd pde'; ret__unsigned_' t = pde_get_tag pde'\<rbrakk> \<Longrightarrow> (pd \<noteq> ARM_H.InvalidPDE) = to_bool (if pde_get_tag pde' \<noteq> SCAST(32 signed \<rightarrow> 32) pde_pde_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) proof (prove)
goal:
No subgoals!