[STATEMENT]
lemma store_cond_cap:
  assumes "store h c val = Success h'"
    and "val = Cap_v v"
  shows "\<exists> m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m)
          \<and> offset c \<ge> fst (bounds m) 
          \<and> offset c + |memval_type val|\<^sub>\<tau> \<le> snd (bounds m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
have cap_perms: "\<not>(\<not> perm_cap_store c \<and> tag v) \<and> \<not>(\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)
[PROOF STEP]
using store_cond_hard_cap(1)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(2)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(3)[where ?h=h and ?c=c and ?v=val and ?ret=h' and ?cv=v, OF assms(1)]
      store_cond_hard_cap(4)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(5)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(6)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      assms
[PROOF STATE]
proof (prove)
using this:
tag c = True
perm_store c = True
\<lbrakk>val = Cap_v v; tag v\<rbrakk> \<Longrightarrow> perm_cap_store c \<and> (perm_cap_store_local c \<or> perm_global v)
offset c + int |memval_type val|\<^sub>\<tau> \<le> int (base c + len c)
int (base c) \<le> offset c
offset c mod int |memval_type val|\<^sub>\<tau> = 0
store h c val = Success h'
val = Cap_v v

goal (1 subgoal):
 1. \<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> (\<not> perm_cap_store c \<and> tag v) \<and> \<not> (\<not> perm_cap_store_local c \<and> tag v \<and> \<not> perm_global v)

goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
using store_cond_hard_cap(1)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(2)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(3)[where ?h=h and ?c=c and ?v=val and ?ret=h' and ?cv=v, OF assms(1)]
      store_cond_hard_cap(4)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(5)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      store_cond_hard_cap(6)[where ?h=h and ?c=c and ?v=val and ?ret=h', OF assms(1)]
      assms
[PROOF STATE]
proof (prove)
using this:
tag c = True
perm_store c = True
\<lbrakk>val = Cap_v v; tag v\<rbrakk> \<Longrightarrow> perm_cap_store c \<and> (perm_cap_store_local c \<or> perm_global v)
offset c + int |memval_type val|\<^sub>\<tau> \<le> int (base c + len c)
int (base c) \<le> offset c
offset c mod int |memval_type val|\<^sub>\<tau> = 0
store h c val = Success h'
val = Cap_v v

goal (1 subgoal):
 1. \<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))
[PROOF STEP]
by (clarsimp split: ccval.split option.split_asm t.split_asm simp add: store_def cap_perms)
      (smt (verit) Mapping.lookup_update assms(1) result.distinct(1) result.sel(1) store_bound_violated_2 store_cond_hard_cap(3) store_def store_success store_tval_disjoint_bounds)
[PROOF STATE]
proof (state)
this:
\<exists>m. Mapping.lookup (heap_map h') (block_id c) = Some (Map m) \<and> int (fst (bounds m)) \<le> offset c \<and> offset c + int |memval_type val|\<^sub>\<tau> \<le> int (snd (bounds m))

goal:
No subgoals!
[PROOF STEP]
qed