theory Arch_DR

lemma set_object_simple_corres:
  "\<lbrakk> obj = transform_object undefined 0 (Some etcb') obj' \<rbrakk> \<Longrightarrow>
   dcorres dc \<top> (not_idle_thread ptr
             and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr)
      (KHeap_D.set_object ptr obj) (KHeap_A.set_object ptr obj')" apply (clarsimp simp: KHeap_D.set_object_def set_object_def) apply (rule dcorres_symb_exec_r) apply (rule corres_assert_rhs[where P'="not_idle_thread ptr and
           obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr"]) apply (fold modify_def) apply (rule corres_modify) apply (clarsimp simp: transform_def transform_objects_def not_idle_thread_def obj_at_def
                          transform_current_thread_def
                    cong: if_cong) apply (rule ext, simp split: if_split) apply (intro conjI impI allI) apply (clarsimp simp: transform_object_def
                    split: Structures_A.kernel_object.split) apply (clarsimp simp: restrict_map_def map_add_def) apply (wpsimp wp: get_object_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> dcorres dc (\<lambda>_. True) (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) (KHeap_D.set_object ptr obj) (KHeap_A.set_object ptr obj') proof (prove)
goal (1 subgoal):
 1. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> dcorres dc (\<lambda>_. True) (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) (modify (dupdate_cdl_object ptr (transform_object undefined 0 (Some etcb') obj'))) (do kobj <- KHeap_A.get_object ptr;
y <- assert (a_type kobj = a_type obj');
s <- get;
put (update_kheap ((kheap s)(ptr \<mapsto> obj')) s)
od) proof (prove)
goal (3 subgoals):
 1. \<And>rv. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> dcorres dc (\<lambda>_. True) (?Q'1 rv) (modify (dupdate_cdl_object ptr (transform_object undefined 0 (Some etcb') obj'))) (do y <- assert (a_type rv = a_type obj');
s <- get;
put (update_kheap ((kheap s)(ptr \<mapsto> obj')) s)
od)
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>?Q'1\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) (modify (dupdate_cdl_object ptr (transform_object undefined 0 (Some etcb') obj'))) (do s <- get;
put (update_kheap ((kheap s)(ptr \<mapsto> obj')) s)
od)
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) (modify (dupdate_cdl_object ptr (transform_object undefined 0 (Some etcb') obj'))) (modify (\<lambda>s. update_kheap ((kheap s)(ptr \<mapsto> obj')) s))
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s s'. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; True; (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s'; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}\<rbrakk> \<Longrightarrow> (dupdate_cdl_object ptr (transform_object undefined 0 (Some etcb') obj') s, update_kheap ((kheap s')(ptr \<mapsto> obj')) s') \<in> {ss'. transform (snd ss') = fst ss'}
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s' ko. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; ptr \<noteq> idle_thread s'; kheap s' ptr = Some ko; \<not> is_tcb ko; same_caps obj' ko; obj_bits ko = obj_bits obj'\<rbrakk> \<Longrightarrow> (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s') ptra ((ekheap s' |` (- {idle_thread s'})) ptra)) (if ptra = ptr then Some obj' else (kheap s' |` (- {idle_thread s'} - {ptr})) ptra)) = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr)))(ptr \<mapsto> transform_object undefined 0 (Some etcb') obj')
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s' ko x. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; ptr \<noteq> idle_thread s'; kheap s' ptr = Some ko; \<not> is_tcb ko; same_caps obj' ko; obj_bits ko = obj_bits obj'\<rbrakk> \<Longrightarrow> (x = ptr \<longrightarrow> transform_object (machine_state s') ptr (ekheap s' ptr) obj' = transform_object undefined 0 (Some etcb') obj') \<and> (x \<noteq> ptr \<longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s') ptra ((ekheap s' |` (- {idle_thread s'})) ptra)) (if ptra = ptr then Some obj' else (kheap s' |` (- {idle_thread s'} - {ptr})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x)
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s' ko x. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; ptr \<noteq> idle_thread s'; kheap s' ptr = Some ko; \<not> is_tcb ko; same_caps obj' ko; obj_bits ko = obj_bits obj'; x = ptr\<rbrakk> \<Longrightarrow> transform_object (machine_state s') ptr (ekheap s' ptr) obj' = transform_object undefined 0 (Some etcb') obj'
 2. \<And>rv s' ko x. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; ptr \<noteq> idle_thread s'; kheap s' ptr = Some ko; \<not> is_tcb ko; same_caps obj' ko; obj_bits ko = obj_bits obj'; x \<noteq> ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s') ptra ((ekheap s' |` (- {idle_thread s'})) ptra)) (if ptra = ptr then Some obj' else (kheap s' |` (- {idle_thread s'} - {ptr})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x
 3. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 4. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s' ko x. \<lbrakk>obj = transform_object undefined 0 (Some etcb') obj'; a_type rv = a_type obj'; ptr \<noteq> idle_thread s'; kheap s' ptr = Some ko; \<not> is_tcb ko; same_caps obj' ko; obj_bits ko = obj_bits obj'; x \<noteq> ptr\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptra. map_option (transform_object (machine_state s') ptra ((ekheap s' |` (- {idle_thread s'})) ptra)) (if ptra = ptr then Some obj' else (kheap s' |` (- {idle_thread s'} - {ptr})) ptra))) x = ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s'}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s') ptr ((ekheap s' |` (- {idle_thread s'})) ptr)) ((kheap s' |` (- {idle_thread s'})) ptr))) x
 2. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 3. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (2 subgoals):
 1. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. a_type r = a_type obj' \<longrightarrow> (not_idle_thread ptr and obj_at (\<lambda>obj. \<not> is_tcb obj \<and> same_caps obj' obj \<and> obj_bits obj = obj_bits obj') ptr) s\<rbrace>
 2. \<And>cs. obj = transform_object undefined 0 (Some etcb') obj' \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> KHeap_A.get_object ptr \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal:
No subgoals!