theory CSpace_I

lemma valid_badges_0_update:
  assumes nx: "mdbNext (cteMDBNode cte) = 0"
  assumes pv: "mdbPrev (cteMDBNode cte) = 0"
  assumes p: "m p = Some cte'"
  assumes m: "no_mdb cte'"
  assumes 0: "no_0 m"
  assumes d: "valid_dlist m"
  assumes v: "valid_badges m"
  shows "valid_badges (m(p \<mapsto> cte))" proof (unfold valid_badges_def, clarify) fix c c' cap cap' n n' assume c: "(m(p \<mapsto> cte)) c = Some (CTE cap n)" assume c': "(m(p \<mapsto> cte)) c' = Some (CTE cap' n')" assume nxt: "m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'" assume r: "sameRegionAs cap cap'" from p 0 have p0: "p \<noteq> 0" by (clarsimp simp: no_0_def) from c' p0 0 have "c' \<noteq> 0" by (clarsimp simp: no_0_def) with nx nxt have cp: "c \<noteq> p" by (clarsimp simp add: mdb_next_unfold) moreover from pv nx nxt p p0 c d m 0 have "c' \<noteq> p" apply clarsimp apply (simp add: mdb_next_unfold split: if_split_asm) apply (erule (1) valid_dlistEn, simp) apply (clarsimp simp: no_mdb_def no_0_def) done moreover with nxt c c' cp have "m \<turnstile> c \<leadsto> c'" by (simp add: mdb_next_unfold) ultimately show "(isEndpointCap cap \<longrightarrow>
            capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow>
            capEPBadge cap' \<noteq> 0 \<longrightarrow>
            mdbFirstBadged n') \<and>
        (isNotificationCap cap \<longrightarrow>
            capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow>
            capNtfnBadge cap' \<noteq> 0 \<longrightarrow>
            mdbFirstBadged n')" using r c c' v by (fastforce simp: valid_badges_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_badges (m(p \<mapsto> cte)) proof (state)
goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
(m(p \<mapsto> cte)) c = Some (CTE cap n)

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
global.sameRegionAs cap cap'

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
m p = Some cte'
no_0 m proof (prove)
using this:
m p = Some cte'
no_0 m

goal (1 subgoal):
 1. p \<noteq> 0 proof (state)
this:
p \<noteq> 0

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')
p \<noteq> 0
no_0 m proof (prove)
using this:
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')
p \<noteq> 0
no_0 m

goal (1 subgoal):
 1. c' \<noteq> 0 proof (state)
this:
c' \<noteq> 0

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
c' \<noteq> 0 proof (prove)
using this:
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
c' \<noteq> 0

goal (1 subgoal):
 1. c \<noteq> p proof (state)
this:
c \<noteq> p

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
c \<noteq> p

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
mdbPrev (cteMDBNode cte) = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
m p = Some cte'
p \<noteq> 0
(m(p \<mapsto> cte)) c = Some (CTE cap n)
valid_dlist m
no_mdb cte'
no_0 m proof (prove)
using this:
mdbPrev (cteMDBNode cte) = 0
mdbNext (cteMDBNode cte) = 0
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
m p = Some cte'
p \<noteq> 0
(m(p \<mapsto> cte)) c = Some (CTE cap n)
valid_dlist m
no_mdb cte'
no_0 m

goal (1 subgoal):
 1. c' \<noteq> p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mdbPrev (cteMDBNode cte) = 0; mdbNext (cteMDBNode cte) = 0; m(p \<mapsto> cte) \<turnstile> c \<leadsto> p; m p = Some cte'; p \<noteq> 0; (if c = p then Some cte else m c) = Some (CTE cap n); valid_dlist m; no_mdb cte'; no_0 m; c' = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist m; no_mdb cte'; no_0 m; c' = mdbNext n; mdbPrev (cteMDBNode cte) = 0; mdbNext (cteMDBNode cte) = 0; p = mdbNext n; m (mdbNext n) = Some cte'; mdbNext n \<noteq> 0; c \<noteq> mdbNext n; m c = Some (CTE cap n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte'a. \<lbrakk>no_mdb cte'; no_0 m; c' = mdbNext n; mdbPrev (cteMDBNode cte) = 0; mdbNext (cteMDBNode cte) = 0; p = mdbNext n; m (mdbNext n) = Some cte'; mdbNext n \<noteq> 0; c \<noteq> mdbNext n; m c = Some (CTE cap n); m (mdbNext (cteMDBNode (CTE cap n))) = Some cte'a; mdbPrev (cteMDBNode cte'a) = c\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
c' \<noteq> p

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (state)
this:
c' \<noteq> p

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
(m(p \<mapsto> cte)) c = Some (CTE cap n)
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')
c \<noteq> p
c' \<noteq> p proof (prove)
using this:
m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'
(m(p \<mapsto> cte)) c = Some (CTE cap n)
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')
c \<noteq> p
c' \<noteq> p

goal (1 subgoal):
 1. m \<turnstile> c \<leadsto> c' proof (state)
this:
m \<turnstile> c \<leadsto> c'

goal (1 subgoal):
 1. \<And>pa p' cap node cap' node'. \<lbrakk>(m(p \<mapsto> cte)) pa = Some (CTE cap node); (m(p \<mapsto> cte)) p' = Some (CTE cap' node'); m(p \<mapsto> cte) \<turnstile> pa \<leadsto> p'; global.sameRegionAs cap cap'\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged node') proof (chain)
picking this:
c \<noteq> p
c' \<noteq> p
m \<turnstile> c \<leadsto> c' proof (prove)
using this:
c \<noteq> p
c' \<noteq> p
m \<turnstile> c \<leadsto> c'

goal (1 subgoal):
 1. (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n') proof (prove)
using this:
c \<noteq> p
c' \<noteq> p
m \<turnstile> c \<leadsto> c'
global.sameRegionAs cap cap'
(m(p \<mapsto> cte)) c = Some (CTE cap n)
(m(p \<mapsto> cte)) c' = Some (CTE cap' n')
valid_badges m

goal (1 subgoal):
 1. (isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n') proof (state)
this:
(isEndpointCap cap \<longrightarrow> capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> capEPBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n') \<and> (isNotificationCap cap \<longrightarrow> capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> capNtfnBadge cap' \<noteq> 0 \<longrightarrow> mdbFirstBadged n')

goal:
No subgoals!