theory Fastpath_C

lemma cap_page_directory_cap_get_capPDBasePtr_spec2:
  "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace>
     Call cap_page_directory_cap_get_capPDBasePtr_'proc
   \<lbrace>cap_get_tag \<^bsup>s\<^esup>cap = scast cap_page_directory_cap
       \<longrightarrow> \<acute>ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply (hoare_rule HoarePartial.ProcNoRec1) apply vcg apply (clarsimp simp: word_sle_def word_sless_def
                        cap_page_directory_cap_lift_def
                        cap_lift_page_directory_cap mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace> Call cap_page_directory_cap_get_capPDBasePtr_'proc \<lbrace>cap_get_tag \<^bsup>s\<^esup>cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> \<acute>ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace> TRY
  lvar_nondet_init ret_' ret_'_update;;
SKIP;;
Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>0 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 0\<rbrace> (\<acute>ret :== cap_C.words_C \<acute>cap.[unat 0] && 0xFFFFC000 << unat 0))));;
\<acute>ret__int :== (if 0 \<noteq> 0 then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  Guard ShiftError \<lbrace>0 \<le>s 0x1F\<rbrace> (Guard ShiftError \<lbrace>0x1F <s 0x20\<rbrace> (\<acute>ret__int :== (if \<acute>ret && (1 << unat 0x1F) \<noteq> 0 then 1 else 0)))
FI;;
IF \<not> \<not> \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret :== \<acute>ret || SCAST(32 signed \<rightarrow> 32) 0
FI;;
return_C ret__unsigned_'_update ret_';;
Guard DontReach {} SKIP
CATCH SKIP
END \<lbrace>cap_get_tag \<^bsup>s\<^esup>cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> \<acute>ret__unsigned = capPDBasePtr_CL (cap_page_directory_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. True \<Longrightarrow> 0 \<le>s 0 \<and> 0 <s 0x20 \<and> 0 <s 2 \<and> 0 \<le>s 0 \<and> ((if False then 1 else 0) \<noteq> 0 \<longrightarrow> 0 \<le>s 0x1F \<and> 0x1F <s 0x20 \<and> ((if (cap_C.words_C cap.[unat 0] && 0xFFFFC000 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) \<noteq> 0 \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> (cap_C.words_C cap.[unat 0] && 0xFFFFC000 << unat 0) || SCAST(32 signed \<rightarrow> 32) 0 = capPDBasePtr_CL (cap_page_directory_cap_lift cap)) \<and> ((if (cap_C.words_C cap.[unat 0] && 0xFFFFC000 << unat 0) && (1 << unat 0x1F) \<noteq> 0 then 1 else 0) = 0 \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> cap_C.words_C cap.[unat 0] && 0xFFFFC000 << unat 0 = capPDBasePtr_CL (cap_page_directory_cap_lift cap))) \<and> ((if False then 1 else 0) = 0 \<longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> cap_C.words_C cap.[unat 0] && 0xFFFFC000 << unat 0 = capPDBasePtr_CL (cap_page_directory_cap_lift cap)) proof (prove)
goal:
No subgoals!