theory Retype_C

lemma mdb_node_ptr_set_mdbNext_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'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) apply (clarsimp simp: ) apply (intro byte_regions_unmodified_hrs_mem_update byte_regions_unmodified_refl,
    simp_all add: typ_heap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call mdb_node_ptr_set_mdbNext_'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
  SKIP;;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))))))))));;
Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (Guard ShiftError \<lbrace>0 \<le>s 0\<rbrace> (Guard ShiftError \<lbrace>0 <s 0x20\<rbrace> (Guard ArrayBounds \<lbrace>1 <s 2\<rbrace> (Guard ArrayBounds \<lbrace>0 \<le>s 1\<rbrace> (Guard C_Guard {s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem \<acute>t_hrs) (PTR(32 word[2]) &(\<acute>mdb_node_ptr\<rightarrow>[''words_C''])).[unat 1] || (\<acute>v32 >> unat 0) && 0xFFFFFFF8))))))))))))
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. 1 <s 2 \<longrightarrow> 0 \<le>s 1 \<longrightarrow> sa \<Turnstile>\<^sub>c mdb_node_ptr_' sa \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa))) \<Turnstile>\<^sub>t mdb_node_ptr_' sa \<longrightarrow> 0 \<le>s 0 \<longrightarrow> 0 <s 0x20 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] || (v32_' sa >> unat 0) && 0xFFFFFFF8))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa)))) = hrs_htd (t_hrs_' (globals s)) \<and> byte_regions_unmodified (t_hrs_' (globals s)) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa)))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] || (v32_' sa >> unat 0) && 0xFFFFFFF8))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C'']))) (unat 1) (h_val (hrs_mem (t_hrs_' (globals sa))) (PTR(32 word[2]) &(mdb_node_ptr_' sa\<rightarrow>[''words_C''])).[unat 1] && ~~ 0xFFFFFFF8))) (t_hrs_' (globals sa))))} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<Turnstile>\<^sub>c mdb_node_ptr_' s \<Longrightarrow> byte_regions_unmodified (t_hrs_' (globals s)) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])).[Suc 0] && 7))) (t_hrs_' (globals s)))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])).[Suc 0] && 7))) (t_hrs_' (globals s)))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])).[Suc 0] || v32_' s && 0xFFFFFFF8))) (hrs_mem_update (heap_update (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])) (Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C'']))) (Suc 0) (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(32 word[2]) &(mdb_node_ptr_' s\<rightarrow>[''words_C''])).[Suc 0] && 7))) (t_hrs_' (globals s)))) proof (prove)
goal:
No subgoals!