theory Retype_R

lemma createObjects_iflive':
  "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> \<not> live' val
        \<and> n \<noteq> 0
        \<and> range_cover ptr sz (objBitsKO val + gbits) n
        \<and> pspace_aligned' s \<and> pspace_distinct' s
        \<and> pspace_no_overlap' ptr sz s\<rbrace>
     createObjects' ptr n val gbits
   \<lbrace>\<lambda>rv s. if_live_then_nonz_cap' s\<rbrace>" apply (rule hoare_pre) apply (simp only: if_live_then_nonz_cap'_def
                     ex_nonz_cap_to'_def imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift
             hoare_vcg_ex_lift createObjects_orig_ko_wp_at2'
             createObjects_orig_cte_wp_at') apply clarsimp apply (intro conjI allI impI) apply simp_all apply (rule ccontr) apply clarsimp apply (drule(1) if_live_then_nonz_capE') apply (fastforce simp: ex_nonz_cap_to'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> createObjects' ptr n val gbits \<lbrace>\<lambda>rv s. \<forall>ptr. \<not> ko_wp_at' live' ptr s \<or> (\<exists>cref. cte_wp_at' (\<lambda>c. ptr \<in> zobj_refs' (cteCap c)) cref s)\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap' s \<and> \<not> live' val \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gbits) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<Longrightarrow> \<forall>x. range_cover ptr (?sz6 x) (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> ko_wp_at' live' x s \<and> (live' val \<longrightarrow> \<not> True) \<and> pspace_no_overlap' ptr (?sz6 x) s \<or> (\<exists>xa. range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<and> pspace_no_overlap' ptr (?sz8 x xa) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz6 x) (objBitsKO val + gbits) n \<and> \<not> ko_wp_at' live' x s \<and> pspace_no_overlap' ptr (?sz6 x) s proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s\<rbrakk> \<Longrightarrow> range_cover ptr (?sz6 x) (objBitsKO val + gbits) n
 2. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s\<rbrakk> \<Longrightarrow> \<not> ko_wp_at' live' x s
 3. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr (?sz6 x) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s\<rbrakk> \<Longrightarrow> \<not> ko_wp_at' live' x s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s; \<not> \<not> ko_wp_at' live' x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>if_live_then_nonz_cap' s; \<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s; ko_wp_at' live' x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<not> live' val; 0 < n; range_cover ptr sz (objBitsKO val + gbits) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>xa. cte_wp_at' (\<lambda>c. x \<in> zobj_refs' (cteCap c)) xa s \<longrightarrow> range_cover ptr (?sz8 x xa) (objBitsKO val + gbits) n \<longrightarrow> \<not> pspace_no_overlap' ptr (?sz8 x xa) s; ko_wp_at' live' x s; ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!