theory Arch_C

lemma pteCheckIfMapped_ccorres:
  "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' \<top>
    (UNIV \<inter> {s. pte___ptr_to_struct_pte_C_' s = Ptr slot}) []
    (pteCheckIfMapped slot)
    (Call pteCheckIfMapped_'proc)" apply (cinit lift: pte___ptr_to_struct_pte_C_') apply (rule ccorres_pre_getObject_pte) apply (rule_tac P'="{s. \<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation rv pte'}"
     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 rv, simp_all add: isInvalidPTE_def pte_tag_defs pte_pte_invalid_def
                                    cpte_relation_def pte_pte_large_lift_def pte_get_tag_def
                                    pte_lift_def Let_def
                             split: if_split_asm) 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>pte___ptr_to_struct_pte_C = pte_Ptr slot\<rbrace>) [] (pteCheckIfMapped slot) (Call pteCheckIfMapped_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>pte___ptr_to_struct_pte_C. pte___ptr_to_struct_pte_C = pte_Ptr slot \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?Q56 pte___ptr_to_struct_pte_C) (?Q'56 pte___ptr_to_struct_pte_C) [SKIP] (do pt <- getObject slot;
return (pt \<noteq> ARM_H.InvalidPTE)
od) (\<acute>ret__unsigned_long :== CALL pte_ptr_get_pteType_'proc(pte___ptr_to_struct_pte_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>pte___ptr_to_struct_pte_C s s'. \<lbrakk>pte___ptr_to_struct_pte_C = pte_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q56 pte___ptr_to_struct_pte_C s \<and> s' \<in> ?Q'56 pte___ptr_to_struct_pte_C proof (prove)
goal (2 subgoals):
 1. \<And>pte___ptr_to_struct_pte_C rv. pte___ptr_to_struct_pte_C = pte_Ptr slot \<Longrightarrow> ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_' (?P62 pte___ptr_to_struct_pte_C rv) (?P'62 pte___ptr_to_struct_pte_C rv) [SKIP] (return (rv \<noteq> ARM_H.InvalidPTE)) (\<acute>ret__unsigned_long :== CALL pte_ptr_get_pteType_'proc(pte___ptr_to_struct_pte_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))
 2. \<And>pte___ptr_to_struct_pte_C s s'. \<lbrakk>pte___ptr_to_struct_pte_C = pte_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pte. ko_at' pte slot s \<longrightarrow> ?P62 pte___ptr_to_struct_pte_C pte s) \<and> s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> ?P'62 pte___ptr_to_struct_pte_C pte} proof (prove)
goal (2 subgoals):
 1. \<And>pte___ptr_to_struct_pte_C rv. pte___ptr_to_struct_pte_C = pte_Ptr slot \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> {s. \<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation rv pte'} \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned_long :== CALL pte_ptr_get_pteType_'proc(pte___ptr_to_struct_pte_C);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> rv = to_bool (ret__unsigned_long_' s)}
 2. \<And>pte___ptr_to_struct_pte_C s s'. \<lbrakk>pte___ptr_to_struct_pte_C = pte_Ptr slot; (s, s') \<in> rf_sr; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>pte. ko_at' pte slot s \<longrightarrow> True) \<and> s' \<in> {s. \<forall>pte pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation pte pte' \<longrightarrow> s \<in> {s. \<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation pte pte'}} proof (prove)
goal (1 subgoal):
 1. \<And>pte___ptr_to_struct_pte_C rv. pte___ptr_to_struct_pte_C = pte_Ptr slot \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation rv pte') \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned_long :== CALL pte_ptr_get_pteType_'proc(pte_Ptr slot);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>x\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<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>rv \<sigma>. \<Gamma>\<turnstile> {s. (\<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation rv pte') \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__unsigned_long :== CALL pte_ptr_get_pteType_'proc(pte_Ptr slot);;
return_C ret__unsigned_long_'_update (\<lambda>s. if ret__unsigned_long_' s \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) {},{s. \<exists>x\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<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>rv \<sigma>. {s. (\<exists>pte'. cslift s (pte_Ptr slot) = Some pte' \<and> cpte_relation rv pte') \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. s \<Turnstile>\<^sub>c pte_Ptr slot \<and> (\<forall>t. ret__unsigned_' t = pte_get_tag (the (cslift s (pte_Ptr slot))) \<longrightarrow> (pte_get_tag (the (cslift s (pte_Ptr slot))) = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := if SCAST(32 signed \<rightarrow> 32) pte_pte_small \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_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 SCAST(32 signed \<rightarrow> 32) pte_pte_small \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))) \<and> (pte_get_tag (the (cslift s (pte_Ptr slot))) \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> s \<Turnstile>\<^sub>c pte_Ptr slot \<and> pte_get_tag (the (cslift s (pte_Ptr slot))) = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<and> (\<forall>t. ret__unsigned_' t = reserved_CL (pte_pte_large_lift (the (cslift s (pte_Ptr slot)))) \<longrightarrow> (reserved_CL (pte_pte_large_lift (the (cslift s (pte_Ptr slot)))) = SCAST(32 signed \<rightarrow> 32) 1 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := if SCAST(32 signed \<rightarrow> 32) pte_pte_large \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_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 SCAST(32 signed \<rightarrow> 32) pte_pte_large \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))) \<and> (reserved_CL (pte_pte_large_lift (the (cslift s (pte_Ptr slot)))) \<noteq> SCAST(32 signed \<rightarrow> 32) 1 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (rv \<noteq> ARM_H.InvalidPTE) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := if False 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 False then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0))))))} proof (prove)
goal (1 subgoal):
 1. \<And>rv \<sigma> x pte' t. \<lbrakk>(\<sigma>, x) \<in> rf_sr; cslift x (pte_Ptr slot) = Some pte'; cpte_relation rv pte'; ret__unsigned_' t = pte_get_tag pte'\<rbrakk> \<Longrightarrow> (pte_get_tag pte' = SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> (rv \<noteq> ARM_H.InvalidPTE) = to_bool (if pte_pte_small \<noteq> pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) \<and> (pte_get_tag pte' \<noteq> SCAST(32 signed \<rightarrow> 32) pte_pte_small \<longrightarrow> pte_get_tag pte' = SCAST(32 signed \<rightarrow> 32) pte_pte_large \<and> ((\<exists>t. ret__unsigned_' t = reserved_CL (pte_pte_large_lift pte')) \<longrightarrow> (reserved_CL (pte_pte_large_lift pte') = 1 \<longrightarrow> (rv \<noteq> ARM_H.InvalidPTE) = to_bool (if pte_pte_large \<noteq> pte_pte_invalid then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0)) \<and> (reserved_CL (pte_pte_large_lift pte') \<noteq> 1 \<longrightarrow> rv = ARM_H.InvalidPTE))) proof (prove)
goal:
No subgoals!