theory CSpace_AI

lemma reply_masters_mdb:
  assumes r: "reply_masters_mdb m cs"
  assumes s: "cs src = Some src_cap"
  assumes d: "cs dest = Some cap.NullCap"
  assumes c: "weak_derived cap src_cap"
  shows "reply_masters_mdb m' (cs (dest \<mapsto> cap, src \<mapsto> cap.NullCap))" unfolding reply_masters_mdb_def using r c s d apply (intro allI impI) apply (subst descendants) unfolding m'_def m''_def apply (simp split: if_split_asm) apply (hypsubst) apply (simp only: weak_derived_Reply reply_masters_mdb_def) apply fastforce apply (simp only: reply_masters_mdb_def) apply (simp del: split_paired_All split_paired_Ex) apply (intro conjI impI) apply (fastforce simp add:weak_derived_Reply) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_masters_mdb m' (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> m' ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m'. \<exists>rights'. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
using this:
reply_masters_mdb m cs
weak_derived cap src_cap
cs src = Some src_cap
cs dest = Some NullCap

goal (1 subgoal):
 1. \<forall>ptr t rights. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr = Some (ReplyCap t True rights) \<longrightarrow> m' ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m'. \<exists>rights'. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> m' ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m'. \<exists>rights'. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> m' ptr = None \<and> (\<forall>ptr'\<in>if ptr = src then {} else if ptr = dest then descendants_of src m else descendants_of ptr m - {src} \<union> (if src \<in> descendants_of ptr m then {dest} else {}). \<exists>rights'. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (if (if ptr = src then None else (m(dest := m src)) ptr) = Some src then Some dest else (m(dest := m src, src := None)) ptr) = None \<and> (\<forall>ptr'\<in>if ptr = src then {} else if ptr = dest then descendants_of src m else descendants_of ptr m - {src} \<union> (if src \<in> descendants_of ptr m then {dest} else {}). \<exists>rights'. (cs(dest \<mapsto> cap, src \<mapsto> NullCap)) ptr' = Some (ReplyCap t False rights')) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived (ReplyCap t True rights) src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr = dest; cap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> m src = None \<and> (\<forall>ptr'\<in>descendants_of src m. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))
 2. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived (ReplyCap t True rights) src_cap; cs src = Some src_cap; cs dest = Some NullCap; cap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> m src = None \<and> (\<forall>ptr'\<in>descendants_of src m. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))
 2. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); \<exists>R'. src_cap = ReplyCap t True R'; cs src = Some src_cap; cs dest = Some NullCap; cap = ReplyCap t True rights\<rbrakk> \<Longrightarrow> m src = None \<and> (\<forall>ptr'\<in>descendants_of src m. ptr' \<noteq> dest \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))
 2. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>reply_masters_mdb m cs; weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> m ptr \<noteq> Some src \<and> (m ptr \<noteq> Some src \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t rights. cs ptr = Some (ReplyCap t True rights) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> None \<noteq> Some src \<and> (None \<noteq> Some src \<longrightarrow> None = None \<and> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> None \<noteq> Some src \<and> (None \<noteq> Some src \<longrightarrow> None = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))))) proof (prove)
goal (1 subgoal):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights)\<rbrakk> \<Longrightarrow> (src \<in> descendants_of ptr m \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights') \<and> (\<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights'))))) \<and> (src \<notin> descendants_of ptr m \<longrightarrow> (\<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))))) proof (prove)
goal (3 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<exists>rights'. cap = ReplyCap t False rights'
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 3. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal (2 subgoals):
 1. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<in> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m - {src}. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))
 2. \<And>ptr t rights. \<lbrakk>\<forall>ptr t. (\<exists>rights. cs ptr = Some (ReplyCap t True rights)) \<longrightarrow> m ptr = None \<and> (\<forall>ptr'\<in>descendants_of ptr m. \<exists>rights'. cs ptr' = Some (ReplyCap t False rights')); weak_derived cap src_cap; cs src = Some src_cap; cs dest = Some NullCap; ptr \<noteq> src; ptr \<noteq> dest; cs ptr = Some (ReplyCap t True rights); src \<notin> descendants_of ptr m\<rbrakk> \<Longrightarrow> \<forall>ptr'\<in>descendants_of ptr m. (ptr' = dest \<longrightarrow> (\<exists>rights'. cap = ReplyCap t False rights')) \<and> (ptr' \<noteq> dest \<longrightarrow> ptr' \<noteq> src \<and> (ptr' \<noteq> src \<longrightarrow> (\<exists>rights'. cs ptr' = Some (ReplyCap t False rights')))) proof (prove)
goal:
No subgoals!