theory Finalise_DR

lemma dcorres_find_pd_for_asid:
  "dcorres ( dc \<oplus> (=)) \<top> valid_idle
    (cdl_find_pd_for_asid (transform_asid a, b))
    (find_pd_for_asid a)" apply (simp add:cdl_find_pd_for_asid_def find_pd_for_asid_def transform_asid_def) apply (simp add:liftE_bindE assertE_assert) apply (rule dcorres_symb_exec_r[where Q' = "\<lambda>r. valid_idle"]) apply (simp add:gets_def) apply (rule dcorres_get) apply (clarsimp simp:cdl_asid_table_transform liftE_bindE
      transform_asid_table_entry_def split:option.splits) apply (simp add:get_asid_pool_def get_object_def gets_the_def gets_def bind_assoc) apply (rule dcorres_get) apply (clarsimp simp: obj_at_def opt_object_asid_pool
                          assert_opt_def has_slots_def opt_cap_def slots_of_def assert_def
                          corres_free_fail
                   split: Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp:transform_asid_pool_contents_def
      object_slots_def transform_asid_pool_entry_def split:option.splits) apply (rule corres_guard_imp[OF dcorres_returnOk]) apply (simp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (=)) (\<lambda>_. True) valid_idle (cdl_find_pd_for_asid (transform_asid a, b)) (find_pd_for_asid a) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (=)) (\<lambda>_. True) valid_idle (doE asid_table <- liftE (gets cdl_asid_table);
pd_cap_ref <- case asid_table (unat (asid_high_bits_of a)) of None \<Rightarrow> throw | Some (AsidPoolCap ptr xa) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) ((unat (asid_high_bits_of a), unat (UCAST(32 \<rightarrow> 10) a)), b)) | Some _ \<Rightarrow> throw;
liftE (KHeap_D.get_cap pd_cap_ref) >>=E case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE) (doE y <- assertE (0 < a);
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> (=)) (\<lambda>_. True) valid_idle (do asid_table <- gets cdl_asid_table;
doE pd_cap_ref <- case asid_table (unat (asid_high_bits_of a)) of None \<Rightarrow> throw | Some (AsidPoolCap ptr xa) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) ((unat (asid_high_bits_of a), unat (UCAST(32 \<rightarrow> 10) a)), b)) | Some _ \<Rightarrow> throw;
KHeap_D.get_cap pd_cap_ref >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE
od) (do y <- assert (0 < a);
asid_table <- gets (arm_asid_table \<circ> arch_state);
doE pool <- case asid_table (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. dcorres (dc \<oplus> (=)) (\<lambda>_. True) valid_idle (do asid_table <- gets cdl_asid_table;
doE pd_cap_ref <- case asid_table (unat (asid_high_bits_of a)) of None \<Rightarrow> throw | Some (AsidPoolCap ptr xa) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) ((unat (asid_high_bits_of a), unat (UCAST(32 \<rightarrow> 10) a)), b)) | Some _ \<Rightarrow> throw;
KHeap_D.get_cap pd_cap_ref >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE
od) (do asid_table <- gets (arm_asid_table \<circ> arch_state);
doE pool <- case asid_table (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE
od)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> (=)) (\<lambda>_. True) valid_idle (do s <- get;
doE pd_cap_ref <- case cdl_asid_table s (unat (asid_high_bits_of a)) of None \<Rightarrow> throw | Some (AsidPoolCap ptr xa) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) ((unat (asid_high_bits_of a), unat (UCAST(32 \<rightarrow> 10) a)), b)) | Some _ \<Rightarrow> throw;
KHeap_D.get_cap pd_cap_ref >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE
od) (do s <- get;
doE pool <- case asid_table s (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE
od)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s sa. \<lbrakk>s = transform sa; True; valid_idle sa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) s) ((=) sa) (doE pd_cap_ref <- case cdl_asid_table s (unat (asid_high_bits_of a)) of None \<Rightarrow> throw | Some (AsidPoolCap ptr xa) \<Rightarrow> returnOk (ptr, (snd \<circ> fst) ((unat (asid_high_bits_of a), unat (UCAST(32 \<rightarrow> 10) a)), b)) | Some _ \<Rightarrow> throw;
KHeap_D.get_cap pd_cap_ref >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
odE) (doE pool <- case asid_table sa (asid_high_bits_of a) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sa x2. \<lbrakk>valid_idle sa; asid_table sa (asid_high_bits_of a) = Some x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) (transform sa)) ((=) sa) (KHeap_D.get_cap (x2, unat (UCAST(32 \<rightarrow> 10) a)) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (do pool <- get_asid_pool x2;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
od)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sa x2. \<lbrakk>valid_idle sa; asid_table sa (asid_high_bits_of a) = Some x2\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) (transform sa)) ((=) sa) (do x <- get;
assert_opt (opt_cap (x2, unat (UCAST(32 \<rightarrow> 10) a)) x) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)
od) (do x <- get;
xa <- assert (\<exists>y. kheap x x2 = Some y);
pool <- case the (kheap x x2) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
od)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>sa x2 x xa. \<lbrakk>valid_idle sa; asid_table sa (asid_high_bits_of a) = Some x2; x = transform xa; transform sa = x; sa = xa\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) x) ((=) xa) (assert_opt (opt_cap (x2, unat (UCAST(32 \<rightarrow> 10) a)) x) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (do x <- assert (\<exists>y. kheap xa x2 = Some y);
pool <- case the (kheap xa x2) of ArchObj (ASIDPool xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
case pool (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
od)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2 xa x1. \<lbrakk>valid_idle xa; asid_table xa (asid_high_bits_of a) = Some x2; kheap xa x2 = Some (ArchObj (ASIDPool x1))\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) (transform xa)) ((=) xa) ((case object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents x1\<rparr>) (unat (UCAST(32 \<rightarrow> 10) a)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) >>= case_cdl_cap throw (\<lambda>bool set1 set2. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word1 word2 set. throw) (\<lambda>word set. throw) (\<lambda>word. throw) (\<lambda>word1 word2 nat1 nat2. throw) (\<lambda>word. throw) throw (\<lambda>word1 word2 bool1 bool2 bool3 bool4. throw) (\<lambda>word bool1 bool2. throw) (\<lambda>word. throw) throw throw throw (\<lambda>word. throw) (\<lambda>bool word set nat cdl_frame_cap_type option. throw) (\<lambda>word cdl_frame_cap_type option. throw) (\<lambda>pd x xa. returnOk pd) throw (\<lambda>word nat. throw) (\<lambda>word set. throw) throw (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw) (\<lambda>word. throw)) (case x1 (UCAST(32 \<rightarrow> 10) a) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x2 xa x1 x2a. \<lbrakk>valid_idle xa; asid_table xa (asid_high_bits_of a) = Some x2; kheap xa x2 = Some (ArchObj (ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) a) = Some x2a\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> (=)) ((=) (transform xa)) ((=) xa) (returnOk x2a) (returnOk x2a)
 2. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 3. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x2 xa x1 x2a. \<lbrakk>valid_idle xa; asid_table xa (asid_high_bits_of a) = Some x2; kheap xa x2 = Some (ArchObj (ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) a) = Some x2a\<rbrakk> \<Longrightarrow> x2a = x2a
 2. \<And>x2 xa x1 x2a s. \<lbrakk>valid_idle xa; asid_table xa (asid_high_bits_of a) = Some x2; kheap xa x2 = Some (ArchObj (ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) a) = Some x2a; transform xa = s\<rbrakk> \<Longrightarrow> True
 3. \<And>x2 xa x1 x2a s. \<lbrakk>valid_idle xa; asid_table xa (asid_high_bits_of a) = Some x2; kheap xa x2 = Some (ArchObj (ASIDPool x1)); x1 (UCAST(32 \<rightarrow> 10) a) = Some x2a; xa = s\<rbrakk> \<Longrightarrow> True
 4. \<lbrace>valid_idle\<rbrace> assert (0 < a) \<lbrace>\<lambda>r. valid_idle\<rbrace>
 5. \<And>cs. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> assert (0 < a) \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!