theory Intent_DR

lemma dcorres_store_word_conservative:
  " within_page obuf ptr sz \<Longrightarrow>
    dcorres dc (\<lambda>_. True)
     (ko_at (ArchObj (DataPage dev sz)) obuf and valid_objs and
      pspace_distinct and
      pspace_aligned and valid_etcbs)
     (corrupt_frame obuf) (do_machine_op (storeWord ptr b))" apply (rule dcorres_expand_pfx,clarsimp) apply (case_tac "\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf") apply (rule corres_dummy_return_pl[where b="()"]) apply (rule corres_dummy_return_r) apply (rule corres_guard_imp) apply (rule corres_split[where r'=dc]) apply (erule dcorres_store_word_safe) apply simp apply (rule dcorres_dummy_corrupt_frame) apply wp+ apply simp apply simp apply (clarsimp) apply (frule ipc_frame_ptr_at_sz_at,simp+) apply (rule corres_guard_imp[OF store_word_corres]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. within_page obuf ptr sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (ako_at (DataPage dev sz) obuf and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs) (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b))
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do return ();
corrupt_frame obuf
od) (do_machine_op (storeWord ptr b))
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do return ();
corrupt_frame obuf
od) (do_machine_op (storeWord ptr b) >>= return)
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc (?Q12 s') (?Q'12 s') (do return ();
corrupt_frame obuf
od) (do_machine_op (storeWord ptr b) >>= return)
 2. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> ?Q12 s' s
 3. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> ?Q'12 s' s
 4. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc (?P16 s') (?P'16 s') (return ()) (do_machine_op (storeWord ptr b))
 2. \<And>s' rv x. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; dc rv x\<rbrakk> \<Longrightarrow> dcorres dc (?R16 s' rv) (?R'16 s' x) (K_bind (corrupt_frame obuf) rv) (return x)
 3. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s'\<rbrace> return () \<lbrace>?R16 s'\<rbrace>
 4. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s'\<rbrace> do_machine_op (storeWord ptr b) \<lbrace>?R'16 s'\<rbrace>
 5. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> (?P16 s' and ?Q16 s') s
 6. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (?P'16 s' and ?Q'16 s') s
 7. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (6 subgoals):
 1. \<And>s' rv x. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; dc rv x\<rbrakk> \<Longrightarrow> dcorres dc (?R16 s' rv) (?R'16 s' x) (K_bind (corrupt_frame obuf) rv) (return x)
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s'\<rbrace> return () \<lbrace>?R16 s'\<rbrace>
 3. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s'\<rbrace> do_machine_op (storeWord ptr b) \<lbrace>?R'16 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q16 s') s
 5. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (ako_at (DataPage (?dev21 s') sz) obuf and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> obuf) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'16 s') s
 6. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> dcorres dc (?R16 s' ()) (?R'16 s' ()) (corrupt_frame obuf) (return ())
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s'\<rbrace> return () \<lbrace>?R16 s'\<rbrace>
 3. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s'\<rbrace> do_machine_op (storeWord ptr b) \<lbrace>?R'16 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q16 s') s
 5. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (ako_at (DataPage (?dev21 s') sz) obuf and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> obuf) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'16 s') s
 6. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 s'\<rbrace> return () \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 s'\<rbrace> do_machine_op (storeWord ptr b) \<lbrace>\<lambda>a. valid_etcbs\<rbrace>
 3. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q16 s') s
 4. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (ako_at (DataPage (?dev21 s') sz) obuf and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> obuf) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and ?Q'16 s') s
 5. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (3 subgoals):
 1. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>a. True)) s
 2. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (ako_at (DataPage (?dev21 s') sz) obuf and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> obuf) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and valid_etcbs) s
 3. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf; s' = s\<rbrakk> \<Longrightarrow> (ako_at (DataPage (?dev21 s') sz) obuf and (\<lambda>s. \<forall>buf thread. ipc_frame_ptr_at buf thread s \<longrightarrow> buf \<noteq> obuf) and valid_objs and pspace_distinct and pspace_aligned and valid_etcbs and valid_etcbs) s
 2. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; \<not> (\<forall>buf. (\<exists>thread. ipc_frame_ptr_at buf thread s') \<longrightarrow> buf \<noteq> obuf)\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<And>s' thread. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; ipc_frame_ptr_at obuf thread s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<And>s' thread. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; ipc_frame_ptr_at obuf thread s'; ipc_frame_sz_at sz thread s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame obuf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (3 subgoals):
 1. \<And>s' thread. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; ipc_frame_ptr_at obuf thread s'; ipc_frame_sz_at sz thread s'\<rbrakk> \<Longrightarrow> within_page obuf ptr (?sz35 s' thread)
 2. \<And>s' thread s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; ipc_frame_ptr_at obuf thread s'; ipc_frame_sz_at sz thread s'; transform s' = s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' thread s. \<lbrakk>within_page obuf ptr sz; ako_at (DataPage dev sz) obuf s'; valid_objs s'; pspace_distinct s'; pspace_aligned s'; valid_etcbs s'; ipc_frame_ptr_at obuf thread s'; ipc_frame_sz_at sz thread s'; s' = s\<rbrakk> \<Longrightarrow> (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at obuf (?s_id35 s' thread) and ipc_frame_sz_at (?sz35 s' thread) (?s_id35 s' thread) and valid_etcbs) s proof (prove)
goal:
No subgoals!