theory Machine_C

lemma setCurrentPD_ccorres:
  "ccorres dc xfdc \<top> (\<lbrace>\<acute>addr = pd\<rbrace>) []
           (doMachineOp (setCurrentPD pd))
           (Call setCurrentPD_'proc)" apply cinit' apply (clarsimp simp: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb
                         writeTTBR0_empty_fail empty_fail_cond
                   intro!: ccorres_cond_empty) apply (rule ccorres_rhs_assoc)+ apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: writeTTBR0Ptr_ccorres) apply (ctac (no_vcg) add: isb_ccorres) apply wp+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) \<lbrace>\<acute>addr = pd\<rbrace> [] (doMachineOp (setCurrentPD pd)) (Call setCurrentPD_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q66 ?Q'66 [SKIP] (doMachineOp (setCurrentPD pd)) (CALL dsb_'proc();;
CALL writeTTBR0Ptr_'proc(\<acute>addr);;
CALL isb_'proc())
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ?Q66 s \<and> s' \<in> ?Q'66 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q66 ?Q'66 [SKIP] (do rv <- doMachineOp dsb;
rv <- doMachineOp (writeTTBR0Ptr pd);
doMachineOp isb
od) (CALL dsb_'proc();;
CALL writeTTBR0Ptr_'proc();;
CALL isb_'proc())
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ?Q66 s \<and> s' \<in> ?Q'66 proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q66 ?Q'66 [SKIP] (do rv <- doMachineOp dsb;
rv <- doMachineOp (writeTTBR0Ptr pd);
doMachineOp isb
od) (CALL dsb_'proc();;
(CALL writeTTBR0Ptr_'proc();;
CALL isb_'proc()))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ?Q66 s \<and> s' \<in> ?Q'66 proof (prove)
goal (3 subgoals):
 1. \<And>rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q79 rv) (?Q'79 rv xfdca) [SKIP] (do rv <- doMachineOp (writeTTBR0Ptr pd);
doMachineOp isb
od) (CALL writeTTBR0Ptr_'proc();;
CALL isb_'proc())
 2. \<lbrace>?R79\<rbrace> doMachineOp dsb \<lbrace>?Q79\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R79) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'79 rv (xfdc t)} proof (prove)
goal (4 subgoals):
 1. \<And>rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q100 rv xfdca rva) (?Q'100 rv xfdca rva xfdcb) [SKIP] (doMachineOp isb) (CALL isb_'proc())
 2. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R102 rv\<rbrace> doMachineOp (writeTTBR0Ptr pd) \<lbrace>?Q100 rv xfdc\<rbrace>
 3. \<lbrace>?R79\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R102 rv\<rbrace>
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R79) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV \<inter> \<lbrace>\<acute>addr = pd\<rbrace>} \<inter> {s'. \<forall>ta rva. dc rva (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> ?Q'100 rv (xfdc t) rva (xfdc ta)}} proof (prove)
goal (3 subgoals):
 1. \<And>rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R102 rv\<rbrace> doMachineOp (writeTTBR0Ptr pd) \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<lbrace>?R79\<rbrace> doMachineOp dsb \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?R102 rv\<rbrace>
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?R79) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV \<inter> \<lbrace>\<acute>addr = pd\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> \<lbrace>\<acute>addr = pd\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s \<and> s' \<in> {s. s \<in> UNIV} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV \<inter> \<lbrace>\<acute>addr = pd\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> {s. s \<in> UNIV}}} proof (prove)
goal:
No subgoals!