theory Tcb_C

lemma setMCPriority_ccorres:
  "ccorres dc xfdc
      (invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. mcp_' s = ucast priority})
      [] (setMCPriority t priority) (Call setMCPriority_'proc)" apply (rule ccorres_gen_asm) apply (cinit lift: tptr_' mcp_') apply (rule ccorres_move_c_guard_tcb) apply (rule threadSet_ccorres_lemma2[where P=\<top>]) apply vcg apply clarsimp apply (erule(1) rf_sr_tcb_update_no_queue2,
              (simp add: typ_heap_simps')+)[1] apply (rule ball_tcb_cte_casesI, simp+) apply (simp add: ctcb_relation_def cast_simps) apply (clarsimp simp: down_cast_same [symmetric] ucast_up_ucast is_up is_down) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and tcb_at' t and (\<lambda>s. priority \<le> maxPriority)) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>mcp = UCAST(8 \<rightarrow> 32) priority\<rbrace>) [] (setMCPriority t priority) (Call setMCPriority_'proc) proof (prove)
goal (1 subgoal):
 1. priority \<le> maxPriority \<Longrightarrow> ccorres dc xfdc (invs' and tcb_at' t) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>mcp = UCAST(8 \<rightarrow> 32) priority\<rbrace>) [] (setMCPriority t priority) (Call setMCPriority_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>mcp tptr. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q52 mcp tptr) (?Q'52 mcp tptr) [SKIP] (threadSet (tcbMCP_update (\<lambda>_. priority)) t) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbMCP_C''])) mcp))))
 2. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q52 mcp tptr s \<and> s' \<in> ?Q'52 mcp tptr proof (prove)
goal (2 subgoals):
 1. \<And>mcp tptr. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A58 mcp tptr) (?C'58 mcp tptr) [SKIP] (threadSet (tcbMCP_update (\<lambda>_. priority)) t) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbMCP_C''])) mcp)))
 2. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?A58 mcp tptr and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> ?C'58 mcp tptr \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>mcp tptr s tcb. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q60 mcp tptr s tcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbMCP_C''])) mcp)) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbMCP_update (\<lambda>_. priority) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>mcp tptr s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q60 mcp tptr s tcb
 3. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>mcp tptr s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbMCP_update (\<lambda>_. priority) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbMCP_C''])) mcp))) sa) \<in> rf_sr}
 2. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; (s, s') \<in> rf_sr; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbMCP_update (\<lambda>_. priority) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbMCP_C''])) (UCAST(8 \<rightarrow> 32) priority)))) s') \<in> rf_sr
 2. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbMCP_update (\<lambda>_. priority) tcb) = getF tcb
 2. \<And>s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbMCP_update (\<lambda>_. priority) tcb) (tcbMCP_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) priority) tcb')
 3. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>priority \<le> maxPriority; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbMCP_update (\<lambda>_. priority) tcb) (tcbMCP_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) priority) tcb')
 2. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>mcp tptr s s'. \<lbrakk>priority \<le> maxPriority; mcp = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (invs' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s \<and> s' \<in> UNIV \<inter> \<lbrace>True\<rbrace> proof (prove)
goal:
No subgoals!