theory Invoke_C

lemma cleanCacheRange_RAM_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanCacheRange_RAM_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (hoare_rule HoarePartial.ProcNoRec1, rule allI) apply (rule conseqPre) apply (vcg exspec=cleanL2Range_preserves_bytes exspec=cleanCacheRange_PoC_preserves_bytes exspec=dsb_preserves_bytes) apply (fastforce elim!: byte_regions_unmodified_trans) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanCacheRange_RAM_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  Guard GhostStateError \<lbrace>fst ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)\<rbrace> (\<acute>globals :== ghost'state_'_update (snd ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)));;
CALL cleanCacheRange_PoC_'proc(\<acute>start,\<acute>end,\<acute>pstart);;
CALL dsb_'proc();;
Guard GhostStateError \<lbrace>fst ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)\<rbrace> (\<acute>globals :== ghost'state_'_update (snd ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)));;
CALL plat_cleanL2Range_'proc(\<acute>pstart,\<acute>pstart + (\<acute>end - \<acute>start))
CATCH SKIP
END \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'5 s) TRY
  Guard GhostStateError \<lbrace>fst ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)\<rbrace> (\<acute>globals :== ghost'state_'_update (snd ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)));;
CALL cleanCacheRange_PoC_'proc(\<acute>start,\<acute>end,\<acute>pstart);;
CALL dsb_'proc();;
Guard GhostStateError \<lbrace>fst ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)\<rbrace> (\<acute>globals :== ghost'state_'_update (snd ((gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id)));;
CALL plat_cleanL2Range_'proc(\<acute>pstart,\<acute>pstart + (\<acute>end - \<acute>start))
CATCH SKIP
END \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace>
 2. \<And>s. {s} \<subseteq> ?P'5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>fst ((ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id) \<longrightarrow> (\<forall>t. hrs_htd \<^bsup>t\<^esup>t_hrs = hrs_htd \<acute>t_hrs \<and> byte_regions_unmodified \<acute>t_hrs \<^bsup>t\<^esup>t_hrs \<longrightarrow> (\<forall>ta. hrs_htd \<^bsup>ta\<^esup>t_hrs = hrs_htd \<acute>t_hrs \<and> byte_regions_unmodified \<^bsup>t\<^esup>t_hrs \<^bsup>ta\<^esup>t_hrs \<longrightarrow> fst ((ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (snd ((ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id) \<acute>ghost'state) = 0 \<or> \<acute>end - \<acute>start \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) (snd ((ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state = 0 \<or> \<acute>end - \<acute>start \<le> ghost_assertion_data_get cap_get_capSizeBits_'proc (\<lambda>x. snd (snd x)) \<acute>ghost'state) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id) \<acute>ghost'state)) \<and> \<acute>start \<le> \<acute>end \<and> \<acute>pstart \<le> \<acute>pstart + (\<acute>end - \<acute>start), id) \<longrightarrow> (\<forall>t. hrs_htd \<^bsup>t\<^esup>t_hrs = hrs_htd \<acute>t_hrs \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<^bsup>t\<^esup>t_hrs \<longrightarrow> hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<^bsup>t\<^esup>t_hrs)))\<rbrace> proof (prove)
goal:
No subgoals!