theory Finalise_DR

lemma find_free_hw_asid_dwp[wp]:
  "\<lbrace>\<lambda>s. transform s = cs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>" apply (clarsimp simp:find_free_hw_asid_def) apply (wp|wpc)+ apply (clarsimp simp:transform_arch_state) apply (wp do_machine_op_wp |clarsimp simp:)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>xa s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. transform s = cs\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateLocalTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid <- return (next_asid + 1);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := new_next_asid\<rparr>\<rparr>);
return next_asid
od | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>xa s. transform s = cs\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid x xa. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?B17 hw_asid_table next_asid x xa\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform (a\<lparr>arch_state := arch_state a\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>) = cs\<rbrace>
 2. \<And>hw_asid_table next_asid x. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?B15 hw_asid_table next_asid x\<rbrace> do_machine_op $ invalidateLocalTLB_ASID next_asid \<lbrace>?B17 hw_asid_table next_asid x\<rbrace>
 3. \<And>hw_asid_table next_asid. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?R11 hw_asid_table next_asid\<rbrace> invalidate_asid $ the $ hw_asid_table next_asid \<lbrace>?B15 hw_asid_table next_asid\<rbrace>
 4. \<And>hw_asid_table next_asid x2. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = Some x2 \<Longrightarrow> \<lbrace>?R12 hw_asid_table next_asid x2\<rbrace> return x2 \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>
 5. \<And>hw_asid_table. \<lbrace>?B1 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<longrightarrow> ?R11 hw_asid_table next_asid s) \<and> (\<forall>x. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = Some x \<longrightarrow> ?R12 hw_asid_table next_asid x s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?B1\<rbrace>
 7. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>hw_asid_table next_asid. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?B17 hw_asid_table next_asid () ()\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>
 2. \<And>hw_asid_table next_asid x. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?B15 hw_asid_table next_asid x\<rbrace> do_machine_op $ invalidateLocalTLB_ASID next_asid \<lbrace>?B17 hw_asid_table next_asid x\<rbrace>
 3. \<And>hw_asid_table next_asid. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<Longrightarrow> \<lbrace>?R11 hw_asid_table next_asid\<rbrace> invalidate_asid $ the $ hw_asid_table next_asid \<lbrace>?B15 hw_asid_table next_asid\<rbrace>
 4. \<And>hw_asid_table next_asid x2. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = Some x2 \<Longrightarrow> \<lbrace>?R12 hw_asid_table next_asid x2\<rbrace> return x2 \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>
 5. \<And>hw_asid_table. \<lbrace>?B1 hw_asid_table\<rbrace> gets (arm_next_asid \<circ> arch_state) \<lbrace>\<lambda>next_asid s. (find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = None \<longrightarrow> ?R11 hw_asid_table next_asid s) \<and> (\<forall>x. find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) = Some x \<longrightarrow> ?R12 hw_asid_table next_asid x s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_hwasid_table \<circ> arch_state) \<lbrace>?B1\<rbrace>
 7. \<And>s. transform s = cs \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!