theory ArchKHeap_AI

lemma set_object_asid_map:
  "\<lbrace>valid_asid_map and
    obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p\<rbrace>
  set_object p ko
  \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: valid_asid_map_def set_object_def get_object_def) apply wp apply (clarsimp simp: vspace_at_asid_def simp del: fun_upd_apply) apply (drule bspec, blast) apply clarsimp apply (rule vs_lookup_stateI, assumption) apply (clarsimp simp: obj_at_def) apply blast apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p\<rbrace> set_object p ko \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)) and obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p\<rbrace> do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh p = Some y);
return (the (kh p))
od;
y <- assert (a_type kobj = a_type ko);
s <- get;
put (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
od \<lbrace>\<lambda>_ s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd s \<and> asid \<noteq> 0)) and obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p) s \<Longrightarrow> (\<exists>y. kheap s p = Some y) \<longrightarrow> a_type (the (kheap s p)) = a_type ko \<longrightarrow> dom (arm_asid_map (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>))) \<subseteq> {0..mask local.asid_bits} \<and> (\<forall>x\<in>graph_of (arm_asid_map (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>))). case x of (asid, hwasid, pd) \<Rightarrow> vspace_at_asid asid pd (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) \<and> asid \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; \<forall>x\<in>graph_of (arm_asid_map (arch_state s)). case x of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s))\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); case (a, aa, b) of (asid, hwasid, pd) \<Rightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<and> asid \<noteq> 0\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) \<and> a \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s y a aa b koa pa. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; ko_at koa pa s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs koa \<subseteq> vs_refs ko') pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
 2. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. \<And>s y a aa b ab ba. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; vs_refs y \<subseteq> vs_refs ko; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0; kheap s p = Some y; (ab, ba) \<in> vs_refs y\<rbrakk> \<Longrightarrow> (ab, ba) \<in> vs_refs ko
 2. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s y a aa b. \<lbrakk>dom (arm_asid_map (arch_state s)) \<subseteq> {0..mask local.asid_bits}; obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p s; kheap s p = Some y; a_type y = a_type ko; (a, aa, b) \<in> graph_of (arm_asid_map (arch_state s)); ([VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] \<rhd> b) s; a \<noteq> 0\<rbrakk> \<Longrightarrow> graph_of (asid_table s) \<subseteq> graph_of (asid_table (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) proof (prove)
goal:
No subgoals!