theory Retype_C

lemma insertNewCap_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (hoare_rule HoarePartial.ProcNoRec1) apply (rule allI, rule conseqPre, vcg exspec=mdb_node_ptr_set_mdbPrev_preserves_bytes
    exspec=mdb_node_ptr_set_mdbNext_preserves_bytes
    exspec=mdb_node_get_mdbNext_modifies exspec=mdb_node_new_modifies) apply (safe intro!: byte_regions_unmodified_hrs_mem_update
    elim!: byte_regions_unmodified_trans byte_regions_unmodified_trans[rotated],
    simp_all add: h_t_valid_field) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  lvar_nondet_init next_' next_'_update;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c parent_' s} (\<acute>ret__unsigned :== CALL mdb_node_get_mdbNext_'proc(h_val (hrs_mem \<acute>t_hrs) (mdb_Ptr &(\<acute>parent\<rightarrow>[''cteMDBNode_C'']))));;
\<acute>next :== cte_Ptr (UCAST(32 \<rightarrow> 32) \<acute>ret__unsigned);;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (cap_Ptr &(\<acute>slot\<rightarrow>[''cap_C''])) \<acute>cap)));;
\<acute>ret__struct_mdb_node_C :== CALL mdb_node_new_'proc(UCAST(32 \<rightarrow> 32) (ptr_val \<acute>next),SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,UCAST(32 \<rightarrow> 32) (ptr_val \<acute>parent));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c slot_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (mdb_Ptr &(\<acute>slot\<rightarrow>[''cteMDBNode_C''])) \<acute>ret__struct_mdb_node_C)));;
IF \<acute>next \<noteq> NULL THEN
  Guard C_Guard {s. s \<Turnstile>\<^sub>c next_' s} (CALL mdb_node_ptr_set_mdbPrev_'proc(mdb_Ptr &(\<acute>next\<rightarrow>[''cteMDBNode_C'']),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>slot)))
FI;;
Guard C_Guard {s. s \<Turnstile>\<^sub>c parent_' s} (CALL mdb_node_ptr_set_mdbNext_'proc(mdb_Ptr &(\<acute>parent\<rightarrow>[''cteMDBNode_C'']),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>slot)))
CATCH SKIP
END \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> {sa. \<forall>v. sa \<Turnstile>\<^sub>c parent_' sa \<longrightarrow> sa \<Turnstile>\<^sub>c slot_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t slot_' sa \<longrightarrow> (\<forall>t ta. (cte_Ptr (UCAST(32 \<rightarrow> 32) (ret__unsigned_' t)) \<noteq> NULL \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t cte_Ptr (UCAST(32 \<rightarrow> 32) (ret__unsigned_' t)) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) (t_hrs_' (globals t)) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t parent_' sa \<longrightarrow> (\<forall>tb. hrs_htd (t_hrs_' (globals tb)) = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals tb)) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals tb))))) \<and> (cte_Ptr (UCAST(32 \<rightarrow> 32) (ret__unsigned_' t)) = NULL \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<Turnstile>\<^sub>t parent_' sa \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) (t_hrs_' (globals t)) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (mdb_Ptr &(slot_' sa\<rightarrow>[''cteMDBNode_C''])) (ret__struct_mdb_node_C_' ta)) (hrs_mem_update (heap_update (cap_Ptr &(slot_' sa\<rightarrow>[''cap_C''])) (cap_' sa)) (t_hrs_' (globals sa)))) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (t_hrs_' (globals t)))))} proof (prove)
goal:
No subgoals!