theory CNodeInv_R

lemma nullcaps_n: "valid_nullcaps n" proof - from valid have "valid_nullcaps m" .. thus ?thesis using dest_derived src_derived apply (clarsimp simp: valid_nullcaps_def) apply (frule n_cap) apply (frule revokable) apply (frule badge_n) apply (frule n_prev) apply (drule n_next) apply (insert src dest) apply (frule_tac x=src in spec) apply (frule_tac x=dest in spec) apply (erule_tac x=p in allE) apply simp apply (case_tac n) apply (clarsimp simp: s_d_swap_def nullMDBNode_def ARM_H.nullPointer_def split: if_split_asm) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_nullcaps n proof (state)
goal (1 subgoal):
 1. valid_nullcaps n proof (chain)
picking this:
valid_mdb_ctes m proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. valid_nullcaps m proof (state)
this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
using this:
valid_nullcaps m

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
using this:
valid_nullcaps m
weak_derived' dest_cap dcap
weak_derived' src_cap scap

goal (1 subgoal):
 1. valid_nullcaps n proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.NullCap na)\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.NullCap na); if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node')\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.NullCap na); if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.NullCap na); if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'; if p = src then mdbFirstBadged na = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged na = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged na = mdbFirstBadged node'\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p na. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; n p = Some (CTE capability.NullCap na); if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable na = mdbRevocable dest_node else if p = dest then mdbRevocable na = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable na = mdbRevocable node'; if p = src then mdbFirstBadged na = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged na = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged na = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap na))) = mdbPrev (cteMDBNode z)\<rbrakk> \<Longrightarrow> na = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap n))) = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode (CTE capability.NullCap n))) = mdbNext (cteMDBNode z)\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap n))) = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode (CTE capability.NullCap n))) = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node)\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap n))) = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode (CTE capability.NullCap n))) = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<forall>n. m src = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>\<forall>p n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap n))) = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode (CTE capability.NullCap n))) = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<forall>n. m src = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; \<forall>n. m dest = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbPrev (cteMDBNode (CTE capability.NullCap n))) = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swp p) = Some z \<and> s_d_swp (mdbNext (cteMDBNode (CTE capability.NullCap n))) = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); \<forall>n. m src = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; \<forall>n. m dest = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; \<forall>n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n. \<lbrakk>weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swap p src dest) = Some z \<and> s_d_swap (mdbPrev n) src dest = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swap p src dest) = Some z \<and> s_d_swap (mdbNext n) src dest = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); src_cap = capability.NullCap \<longrightarrow> src_node = nullMDBNode; dest_cap = capability.NullCap \<longrightarrow> dest_node = nullMDBNode; \<forall>n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal (1 subgoal):
 1. \<And>p n x1 x2 x3 x4. \<lbrakk>weak_derived' dest_cap dcap; weak_derived' src_cap scap; if p = src then capability.NullCap = dcap else if p = dest then capability.NullCap = scap else \<exists>node'. m p = Some (CTE capability.NullCap node'); if p = src then mdbRevocable n = mdbRevocable dest_node else if p = dest then mdbRevocable n = mdbRevocable src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbRevocable n = mdbRevocable node'; if p = src then mdbFirstBadged n = mdbFirstBadged dest_node else if p = dest then mdbFirstBadged n = mdbFirstBadged src_node else \<exists>cap' node'. m p = Some (CTE cap' node') \<and> mdbFirstBadged n = mdbFirstBadged node'; \<exists>z. m (s_d_swap p src dest) = Some z \<and> s_d_swap (mdbPrev n) src dest = mdbPrev (cteMDBNode z); \<exists>z. m (s_d_swap p src dest) = Some z \<and> s_d_swap (mdbNext n) src dest = mdbNext (cteMDBNode z); m src = Some (CTE src_cap src_node); m dest = Some (CTE dest_cap dest_node); src_cap = capability.NullCap \<longrightarrow> src_node = nullMDBNode; dest_cap = capability.NullCap \<longrightarrow> dest_node = nullMDBNode; \<forall>n. m p = Some (CTE capability.NullCap n) \<longrightarrow> n = nullMDBNode; n = MDB x1 x2 x3 x4\<rbrakk> \<Longrightarrow> n = nullMDBNode proof (prove)
goal:
No subgoals! proof (state)
this:
valid_nullcaps n

goal:
No subgoals!