theory Untyped_AI

lemma create_cap_wps[wp]:
  "\<lbrace>pspace_aligned\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>"
  "\<lbrace>pspace_distinct\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>"
  "\<lbrace>cte_wp_at P p' and K (p' \<noteq> cref)\<rbrace>
       create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. cte_wp_at P p'\<rbrace>"
  "\<lbrace>valid_objs and valid_cap (default_cap tp oref sz dev)
            and real_cte_at cref\<rbrace>
       create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_objs\<rbrace>"
  "\<lbrace>valid_cap cap\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_cap cap\<rbrace>" apply (safe intro!: hoare_gen_asm) apply (simp_all add: create_cap_def) apply (wp set_cap_cte_wp_at' set_cdt_cte_wp_at
                set_cap_valid_objs set_cdt_valid_objs
                set_cdt_valid_cap set_cap_valid_cap
              | simp split del: if_split
                           add: real_cte_tcb_valid)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>pspace_aligned\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_aligned\<rbrace> &&& \<lbrace>pspace_distinct\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>) &&& \<lbrace>cte_wp_at P p' and K (p' \<noteq> cref)\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. cte_wp_at P p'\<rbrace> &&& \<lbrace>valid_objs and valid_cap (default_cap tp oref sz dev) and real_cte_at cref\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_objs\<rbrace> &&& \<lbrace>valid_cap cap\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_cap cap\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>pspace_aligned\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>
 2. \<lbrace>pspace_distinct\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>
 3. p' \<noteq> cref \<Longrightarrow> \<lbrace>cte_wp_at P p'\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. cte_wp_at P p'\<rbrace>
 4. \<lbrace>valid_objs and valid_cap (default_cap tp oref sz dev) and real_cte_at cref\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 5. \<lbrace>valid_cap cap\<rbrace> create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_cap cap\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>pspace_aligned\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. pspace_aligned\<rbrace>
 2. \<lbrace>pspace_distinct\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. pspace_distinct\<rbrace>
 3. p' \<noteq> cref \<Longrightarrow> \<lbrace>cte_wp_at P p'\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. cte_wp_at P p'\<rbrace>
 4. \<lbrace>valid_objs and valid_cap (default_cap tp oref sz dev) and real_cte_at cref\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. valid_objs\<rbrace>
 5. \<lbrace>valid_cap cap\<rbrace> do dest_p <- gets (\<lambda>s. cdt s cref);
cdt <- gets cdt;
y <- set_cdt (cdt(cref \<mapsto> p));
y <- do_extended_op (create_cap_ext p cref dest_p);
y <- set_original cref True;
set_cap (default_cap tp oref sz dev) cref
od \<lbrace>\<lambda>rv. valid_cap cap\<rbrace> proof (prove)
goal:
No subgoals!