theory CNodeInv_R

lemma cteMove_invs' [wp]:
  "\<lbrace>\<lambda>x. invs' x \<and> ex_cte_cap_to' word2 x \<and>
            cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and>
            cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and>
            cte_wp_at' (\<lambda>c. (cteCap c) \<noteq> NullCap) word1 x \<and>
            x \<turnstile>' capability \<and>
            cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace>
     cteMove capability word1 word2
   \<lbrace>\<lambda>y. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def pred_conj_def) apply (rule hoare_pre) apply ((rule hoare_vcg_conj_lift, (wp cteMove_ifunsafe')[1])
                  | rule hoare_vcg_conj_lift[rotated])+ apply (unfold cteMove_def) apply (wp cur_tcb_lift valid_queues_lift haskell_assert_inv
                sch_act_wf_lift ct_idle_or_in_cur_domain'_lift2 tcb_in_cur_domain'_lift)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. invs' x \<and> ex_cte_cap_wp_to' (\<lambda>_. True) word2 x \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 x \<and> valid_cap' capability x \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>y. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>x. valid_pspace' x \<and> sch_act_wf (ksSchedulerAction x) x \<and> Invariants_H.valid_queues x \<and> sym_refs (state_refs_of' x) \<and> if_live_then_nonz_cap' x \<and> if_unsafe_then_cap' x \<and> valid_idle' x \<and> valid_global_refs' x \<and> valid_arch_state' x \<and> valid_irq_node' (irq_node' x) x \<and> valid_irq_handlers' x \<and> valid_irq_states' x \<and> valid_machine_state' x \<and> irqs_masked' x \<and> valid_queues' x \<and> ct_not_inQ x \<and> ct_idle_or_in_cur_domain' x \<and> valid_pde_mappings' x \<and> pspace_domain_valid x \<and> ksCurDomain x \<le> maxDomain \<and> ksDomSchedule x \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule x). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule x = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx x < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' x \<and> cur_tcb' x \<and> ex_cte_cap_wp_to' (\<lambda>_. True) word2 x \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 x \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 x \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 x \<and> valid_cap' capability x \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 x\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>y x. valid_pspace' x \<and> sch_act_wf (ksSchedulerAction x) x \<and> Invariants_H.valid_queues x \<and> sym_refs (state_refs_of' x) \<and> if_live_then_nonz_cap' x \<and> if_unsafe_then_cap' x \<and> valid_idle' x \<and> valid_global_refs' x \<and> valid_arch_state' x \<and> valid_irq_node' (irq_node' x) x \<and> valid_irq_handlers' x \<and> valid_irq_states' x \<and> valid_machine_state' x \<and> irqs_masked' x \<and> valid_queues' x \<and> ct_not_inQ x \<and> ct_idle_or_in_cur_domain' x \<and> valid_pde_mappings' x \<and> pspace_domain_valid x \<and> ksCurDomain x \<le> maxDomain \<and> ksDomSchedule x \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule x). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule x = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx x < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' x \<and> cur_tcb' x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>y x. valid_pspace' x \<and> sch_act_wf (ksSchedulerAction x) x \<and> Invariants_H.valid_queues x \<and> sym_refs (state_refs_of' x) \<and> if_live_then_nonz_cap' x \<and> if_unsafe_then_cap' x \<and> valid_idle' x \<and> valid_global_refs' x \<and> valid_arch_state' x \<and> valid_irq_node' (irq_node' x) x \<and> valid_irq_handlers' x \<and> valid_irq_states' x \<and> valid_machine_state' x \<and> irqs_masked' x \<and> valid_queues' x \<and> ct_not_inQ x \<and> ct_idle_or_in_cur_domain' x \<and> valid_pde_mappings' x \<and> pspace_domain_valid x \<and> ksCurDomain x \<le> maxDomain \<and> ksDomSchedule x \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule x). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule x = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx x < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' x \<and> cur_tcb' x\<rbrace>
 2. \<And>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) word2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s \<and> valid_cap' capability s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s \<Longrightarrow> ?Q s proof (prove)
goal (18 subgoals):
 1. \<lbrace>?P'99\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
 2. \<lbrace>?P96\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv s. ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined))\<rbrace>
 3. \<lbrace>?P93\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv s. ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined)\<rbrace>
 4. \<lbrace>?P90\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv s. \<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x\<rbrace>
 5. \<lbrace>?P87\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv s. ksDomSchedule s \<noteq> []\<rbrace>
 6. \<lbrace>?P84\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv s. ksCurDomain s \<le> maxDomain\<rbrace>
 7. \<lbrace>?P81\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace>
 8. \<lbrace>?P78\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>
 9. \<lbrace>?P75\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>
 10. \<lbrace>?P72\<rbrace> cteMove capability word1 word2 \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<lbrace>?P'99\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>
 2. \<lbrace>?P96\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv s. ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined))\<rbrace>
 3. \<lbrace>?P93\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv s. ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined)\<rbrace>
 4. \<lbrace>?P90\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv s. \<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x\<rbrace>
 5. \<lbrace>?P87\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv s. ksDomSchedule s \<noteq> []\<rbrace>
 6. \<lbrace>?P84\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv s. ksCurDomain s \<le> maxDomain\<rbrace>
 7. \<lbrace>?P81\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv. pspace_domain_valid\<rbrace>
 8. \<lbrace>?P78\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>
 9. \<lbrace>?P75\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>
 10. \<lbrace>?P72\<rbrace> do oldCTE <- getCTE word2;
haskell_assert (isNullCap $ cteCap oldCTE) [];
haskell_assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer) [];
cte <- getCTE word1;
mdb <- return (cteMDBNode cte);
updateCap word2 capability;
updateCap word1 capability.NullCap;
updateMDB word2 (const mdb);
updateMDB word1 (const nullMDBNode);
updateMDB (mdbPrev mdb) (mdbNext_update (\<lambda>_. word2));
updateMDB (mdbNext mdb) (mdbPrev_update (\<lambda>_. word2))
od \<lbrace>\<lambda>rv. ct_not_inQ\<rbrace>
A total of 18 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> cur_tcb' s \<and> ex_cte_cap_wp_to' (\<lambda>_. True) word2 s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s \<and> valid_cap' capability s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s \<Longrightarrow> (valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s \<and> valid_cap' capability s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s) \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> (if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c \<noteq> capability.NullCap) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s) \<and> (if_unsafe_then_cap' and cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 and ex_cte_cap_wp_to' (\<lambda>_. True) word2 and cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1) s \<and> valid_idle' s \<and> (valid_global_refs' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s) \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> (valid_irq_handlers' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s) \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> (untyped_ranges_zero' s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. weak_derived' (cteCap c) capability) word1 s \<and> cte_wp_at' (\<lambda>c. isUntypedCap (cteCap c) \<longrightarrow> capability = cteCap c) word1 s \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.NullCap) word2 s) \<and> cur_tcb' s proof (prove)
goal:
No subgoals!