theory CSpace_R

lemma cteInsert_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace>" apply (simp add: cteInsert_def valid_machine_state'_def pointerInDeviceData_def
                   pointerInUserData_def) apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift) apply (wp setObject_typ_at_inv setObject_ksMachine updateObject_default_inv |
          intro hoare_drop_imp|assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>p. \<lbrace>typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace>
 2. \<And>p. \<lbrace>typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. typ_at' UserDataDeviceT (p && ~~ mask pageBits)\<rbrace>
 3. \<And>p. \<lbrace>\<lambda>s. underlying_memory (ksMachineState s) p = 0\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv s. underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!