theory Invoke_C

lemma ccorres_cross_retype_zero_bytes_over_guard:
  "range_cover ptr sz (APIType_capBits newType userSize) num_ret
    \<Longrightarrow> ccorres_underlying rf_sr Gamm rvr xf arrel axf P' Q hs af cf
    \<Longrightarrow> ccorres_underlying rf_sr Gamm rvr xf arrel axf
        ((\<lambda>s. invs' s
      \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx
          \<and> idx \<le> unat (ptr && mask sz)) p s) and P')
      {s'. (\<not> dev \<longrightarrow> region_actually_is_zero_bytes ptr
            (num_ret * 2 ^ APIType_capBits newType userSize) s')
         \<and> (\<exists>cte cte' idx. cslift s' (cte_Ptr p) = Some cte'
                 \<and> ccte_relation cte cte' \<and> cteCap cte = UntypedCap dev (ptr && ~~ mask sz) sz idx)
         \<longrightarrow> s' \<in> Q} hs af cf" apply (erule ccorres_guard_imp2) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule(1) rf_sr_ctes_of_clift, clarsimp) apply (frule(2) rf_sr_cte_relation) apply (case_tac dev) apply fastforce apply (frule(1) retype_offs_region_actually_is_zero_bytes, (simp | clarsimp)+) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; ccorres_underlying rf_sr Gamm rvr xf arrel axf P' Q hs af cf\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr Gamm rvr xf arrel axf ((\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx \<and> idx \<le> unat (ptr && mask sz)) p s) and P') {s'. (\<not> dev \<longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<and> (\<exists>cte cte' idx. cslift s' (cte_Ptr p) = Some cte' \<and> ccte_relation cte cte' \<and> cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) \<longrightarrow> s' \<in> Q} hs af cf proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; ((\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. \<exists>idx. cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx \<and> idx \<le> unat (ptr && mask sz)) p s) and P') s; s' \<in> {s'. (\<not> dev \<longrightarrow> region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<and> (\<exists>cte cte' idx. cslift s' (cte_Ptr p) = Some cte' \<and> ccte_relation cte cte' \<and> cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx) \<longrightarrow> s' \<in> Q}\<rbrakk> \<Longrightarrow> P' s \<and> s' \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>s s' cte idx. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some cte; cteCap cte = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte cte'. ccte_relation cte cte' \<longrightarrow> cslift s' (cte_Ptr p) = Some cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx))\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ccte_relation (cte_to_H y) cte'\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal (2 subgoals):
 1. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ccte_relation (cte_to_H y) cte'; dev\<rbrakk> \<Longrightarrow> s' \<in> Q
 2. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ccte_relation (cte_to_H y) cte'; \<not> dev\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<not> dev \<and> (region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s' \<longrightarrow> heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr \<noteq> replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0) \<or> (\<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap dev (ptr && ~~ mask sz) sz idx)); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ccte_relation (cte_to_H y) cte'; \<not> dev\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal (1 subgoal):
 1. \<And>s s' idx cte' y. \<lbrakk>range_cover ptr sz (APIType_capBits newType userSize) num_ret; (s, s') \<in> rf_sr; invs' s; P' s; ctes_of s p = Some (cte_to_H y); cap_to_H (cap_CL y) = capability.UntypedCap False (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); \<forall>cte. ccte_relation cte cte' \<longrightarrow> (\<forall>idx. cteCap cte \<noteq> capability.UntypedCap False (ptr && ~~ mask sz) sz idx); cslift s' (cte_Ptr p) = Some cte'; cte_lift cte' = Some y; c_valid_cte cte'; ccte_relation (cte_to_H y) cte'; \<not> dev; region_actually_is_bytes ptr (num_ret * 2 ^ APIType_capBits newType userSize) s'; heap_list (hrs_mem (t_hrs_' (globals s'))) (num_ret * 2 ^ APIType_capBits newType userSize) ptr = replicate (num_ret * 2 ^ APIType_capBits newType userSize) 0\<rbrakk> \<Longrightarrow> s' \<in> Q proof (prove)
goal:
No subgoals!