kings-crown/FVELER_Isabelle huggingface dataset:
theory Eval_CAMKES_CDL

lemma sorted_distinct_conv:
  "sorted_distinct xs = (sorted xs \<and> distinct xs)" apply (induct xs) apply simp apply (rename_tac x xs, case_tac xs) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sorted_distinct xs = (sorted xs \<and> distinct xs) proof (prove)
goal (2 subgoals):
 1. sorted_distinct [] = (sorted [] \<and> distinct [])
 2. \<And>a xs. sorted_distinct xs = (sorted xs \<and> distinct xs) \<Longrightarrow> sorted_distinct (a # xs) = (sorted (a # xs) \<and> distinct (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. sorted_distinct xs = (sorted xs \<and> distinct xs) \<Longrightarrow> sorted_distinct (a # xs) = (sorted (a # xs) \<and> distinct (a # xs)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>sorted_distinct xs = (sorted xs \<and> distinct xs); xs = []\<rbrakk> \<Longrightarrow> sorted_distinct (x # xs) = (sorted (x # xs) \<and> distinct (x # xs))
 2. \<And>x xs a list. \<lbrakk>sorted_distinct xs = (sorted xs \<and> distinct xs); xs = a # list\<rbrakk> \<Longrightarrow> sorted_distinct (x # xs) = (sorted (x # xs) \<and> distinct (x # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs a list. \<lbrakk>sorted_distinct xs = (sorted xs \<and> distinct xs); xs = a # list\<rbrakk> \<Longrightarrow> sorted_distinct (x # xs) = (sorted (x # xs) \<and> distinct (x # xs)) proof (prove)
goal:
No subgoals!
theory Eval_CAMKES_CDL

lemma graph_of_map_of:
  "distinct (map fst binds) \<Longrightarrow> graph_of (map_of binds) = set binds" by (simp add: graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (map fst binds) \<Longrightarrow> graph_of (map_of binds) = set binds
theory Eval_CAMKES_CDL

lemma graph_of_map_of_simp:
  "sorted_distinct (map fst binds) \<Longrightarrow> graph_of (map_of binds) = set binds" by (simp add: graph_of_def sorted_distinct_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sorted_distinct (map fst binds) \<Longrightarrow> graph_of (map_of binds) = set binds
theory Eval_CAMKES_CDL

lemma graph_of_map_of__sorted_eval:
  "graph_of (map_of binds) =
     (if sorted_distinct (rev (map fst binds)) then set binds else graph_of_map_of__eval_FAIL binds)" by (simp add: graph_of_map_of sorted_distinct_conv graph_of_map_of__eval_FAIL_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_of (map_of binds) = (if sorted_distinct (rev (map fst binds)) then set binds else graph_of_map_of__eval_FAIL binds)
theory Eval_CAMKES_CDL

lemma graph_of_map_of__distinct_eval:
  "graph_of (map_of binds) =
     (if distinct (map fst binds) then set binds else graph_of_map_of__eval_FAIL binds)" by (simp add: graph_of_map_of graph_of_map_of__eval_FAIL_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_of (map_of binds) = (if distinct (map fst binds) then set binds else graph_of_map_of__eval_FAIL binds)
theory Eval_CAMKES_CDL

lemma range_map_of_ptr_range:
  "\<lbrakk> RangeMap.range_map_of binds (p :: cdl_object_id) = Some ((p, p + 2^sz), l) \<rbrakk> \<Longrightarrow>
   (x \<in> ptr_range p sz) = (p \<le> x \<and> x < p + 2^sz)" apply (drule RangeMap.range_map_of_SomeD) apply (subst ptr_range_in_range) apply unat_arith apply (simp add: RangeMap.in_range.simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l) \<Longrightarrow> (x \<in> ptr_range p sz) = (p \<le> x \<and> x < p + 2 ^ sz) proof (prove)
goal (1 subgoal):
 1. ((p, p + 2 ^ sz), l) \<in> set binds \<and> p \<le> p \<and> p < p + 2 ^ sz \<Longrightarrow> (x \<in> ptr_range p sz) = (p \<le> x \<and> x < p + 2 ^ sz) proof (prove)
goal (2 subgoals):
 1. ((p, p + 2 ^ sz), l) \<in> set binds \<and> p \<le> p \<and> p < p + 2 ^ sz \<Longrightarrow> 0 < p + 2 ^ sz
 2. ((p, p + 2 ^ sz), l) \<in> set binds \<and> p \<le> p \<and> p < p + 2 ^ sz \<Longrightarrow> RangeMap.in_range (p, p + 2 ^ sz) x = (p \<le> x \<and> x < p + 2 ^ sz) proof (prove)
goal (1 subgoal):
 1. ((p, p + 2 ^ sz), l) \<in> set binds \<and> p \<le> p \<and> p < p + 2 ^ sz \<Longrightarrow> RangeMap.in_range (p, p + 2 ^ sz) x = (p \<le> x \<and> x < p + 2 ^ sz) proof (prove)
goal:
No subgoals!
theory Eval_CAMKES_CDL

lemma range_tree_ptr_range:
  "\<lbrakk> RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds;
     RangeMap.monotonic_key_ranges binds;
     RangeMap.range_map_of binds (p :: cdl_object_id) = Some ((p, p + 2^sz), l);
     x \<in> ptr_range p sz \<rbrakk> \<Longrightarrow>
   RangeMap.lookup_range_tree tree x = Some ((p, p + 2^sz), l)" apply (subst (asm) range_map_of_ptr_range) apply fastforce apply (simp only:) apply (drule RangeMap.range_map_of_SomeD) apply (blast intro: RangeMap.range_map_of_single RangeMap.monotonic_key_ranges_disjoint) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l); x \<in> ptr_range p sz\<rbrakk> \<Longrightarrow> RangeMap.lookup_range_tree tree x = Some ((p, p + 2 ^ sz), l) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l)\<rbrakk> \<Longrightarrow> RangeMap.range_map_of ?binds p = Some ((p, p + 2 ^ sz), ?l)
 2. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l); p \<le> x \<and> x < p + 2 ^ sz\<rbrakk> \<Longrightarrow> RangeMap.lookup_range_tree tree x = Some ((p, p + 2 ^ sz), l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l); p \<le> x \<and> x < p + 2 ^ sz\<rbrakk> \<Longrightarrow> RangeMap.lookup_range_tree tree x = Some ((p, p + 2 ^ sz), l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; RangeMap.range_map_of binds p = Some ((p, p + 2 ^ sz), l); p \<le> x \<and> x < p + 2 ^ sz\<rbrakk> \<Longrightarrow> RangeMap.range_map_of binds x = Some ((p, p + 2 ^ sz), l) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>RangeMap.lookup_range_tree tree = RangeMap.range_map_of binds; RangeMap.monotonic_key_ranges binds; p \<le> x \<and> x < p + 2 ^ sz; ((p, p + 2 ^ sz), l) \<in> set binds \<and> p \<le> p \<and> p < p + 2 ^ sz\<rbrakk> \<Longrightarrow> RangeMap.range_map_of binds x = Some ((p, p + 2 ^ sz), l) proof (prove)
goal:
No subgoals!
theory Eval_CAMKES_CDL

lemma Ball_eval:
  "Ball (insert x s) P = (P x \<and> Ball s P)"
  "Ball Set.empty P = True" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Ball (insert x s) P = (P x \<and> Ball s P) &&& Ball {} P = True
theory Eval_CAMKES_CDL

lemma bintrunc_1_1:
  "bintrunc 1 1 = 1" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit 1 1 = 1
theory Eval_CAMKES_CDL

lemma pow_2_numeral:
  "(2::'a::{numeral,semiring_1,power})^0 = 1"
  "(2::'a)^1 = 2"
  "(2::'a)^numeral n = 2 * 2^(numeral n - 1)" apply simp apply simp apply (metis numeral_eq_Suc pred_numeral_def power_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2::'a) ^ 0 = (1::'a) &&& (2::'a) ^ 1 = (2::'a) &&& (2::'a) ^ numeral n = (2::'a) * (2::'a) ^ (numeral n - 1) proof (prove)
goal (2 subgoals):
 1. (2::'a) ^ 1 = (2::'a)
 2. (2::'a) ^ numeral n = (2::'a) * (2::'a) ^ (numeral n - 1) proof (prove)
goal (1 subgoal):
 1. (2::'a) ^ numeral n = (2::'a) * (2::'a) ^ (numeral n - 1) proof (prove)
goal:
No subgoals!
theory EgTop

lemma "\<forall>p. \<exists>e s. gs\<^sub>0 p = Some (e, s) \<and>
           (e = client_untrusted \<or>
            \<not>(\<exists>c. sends e {x. q_channel x = c \<and> q_data x = Return [String ''baz'']} \<and>
              receives_on c client_untrusted))" oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>p. \<exists>e s. gs\<^sub>0 p = Some (e, s) \<and> (e = client_untrusted \<or> (\<nexists>c. sends e {x. q_channel x = c \<and> q_data x = Return [String ''baz'']} \<and> receives_on c client_untrusted))
theory RPCFrom

lemma seL4_GetIPCBuffer_wp':
  "\<forall>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and>
             s = s'\<rbrace>
         seL4_GetIPCBuffer'
        \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s
                 (Ptr (scast seL4_GlobalsFrame)) \<and>
               s = s'\<rbrace>!" apply (rule allI) apply (simp add:seL4_GetIPCBuffer'_def) apply wp apply (clarsimp simp:globals_frame_intact_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> seL4_GetIPCBuffer' \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> seL4_GetIPCBuffer' \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrace>\<lambda>s. globals_frame_intact s \<and> s = s'\<rbrace> do y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)));
gets (\<lambda>s. heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))
od \<lbrace>\<lambda>r s. r = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) \<and> s = s'\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s' s. globals_frame_intact s \<and> s = s' \<Longrightarrow> (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) = heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) \<and> s = s') \<and> is_valid_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma seL4_SetMR_wp[wp_unsafe]:
  notes seL4_SetMR_axiom[simp]
  shows
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        i \<ge> 0 \<and>
        i < seL4_MsgMaxLength \<and>
        (\<forall>x. P x (setMR s (nat i) v))\<rbrace>
    exec_concrete lift_global_heap (seL4_SetMR' i v)
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_SetMR_lifted'_def) apply (wp seL4_GetIPCBuffer_wp) apply (simp add:setMR_def globals_frame_intact_def ipc_buffer_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> (\<forall>x. P x (setMR s (nat i) v))\<rbrace> exec_concrete lift_global_heap (seL4_SetMR' i v) \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v)\<rbrace> do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. i < 120);
y <- guard (\<lambda>s. 0 \<le> i);
modify (\<lambda>s. s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(ret' := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s ret'))\<rparr>)
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> i \<and> i < 120 \<and> P () (setMR s (nat i) v) \<Longrightarrow> globals_frame_intact s \<and> (P () (s\<lparr>heap_seL4_IPCBuffer__C := (heap_seL4_IPCBuffer__C s)(heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)) := msg_C_update (\<lambda>a. Arrays.update a (nat i) v) (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))))\<rparr>) \<and> 0 \<le> i) \<and> i < 120 proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma seL4_GetMR_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. \<forall>x. i \<ge> 0 \<and>
            i < seL4_MsgMaxLength \<and>
            globals_frame_intact s \<and>
            ipc_buffer_valid s \<and>
            P x s\<rbrace>
    seL4_GetMR' i
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_GetMR'_def) apply (wp seL4_GetIPCBuffer_wp) apply (simp add:globals_frame_intact_def ipc_buffer_valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> P x s\<rbrace> seL4_GetMR' i \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x. P x s)\<rbrace> do ret' <- seL4_GetIPCBuffer';
y <- guard (\<lambda>s. i < 120);
y <- guard (\<lambda>s. 0 \<le> i);
y <- guard (\<lambda>s. is_valid_seL4_IPCBuffer__C s ret');
gets (\<lambda>s. msg_C (heap_seL4_IPCBuffer__C s ret').[unat (word_of_int i)])
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. 0 \<le> i \<and> i < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x. P x s) \<Longrightarrow> globals_frame_intact s \<and> ((P (msg_C (heap_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))).[unat (word_of_int i)]) s \<and> is_valid_seL4_IPCBuffer__C s (heap_seL4_IPCBuffer__C'ptr s (PTR(seL4_IPCBuffer__C ptr) (SCAST(32 signed \<rightarrow> 32) seL4_GlobalsFrame)))) \<and> 0 \<le> i) \<and> i < 120 proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma abort_wp[wp]:
  "\<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>!" by (rule validNF_false_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>!
theory RPCFrom

lemma seL4_Call_wp[wp_unsafe]:
  notes seL4_SetMR_wp[wp] seL4_GetMR_wp[wp]
  shows
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace>
    seL4_Call' cap info
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Call'_def) apply (wp seL4_GetIPCBuffer_wp) apply (simp add:globals_frame_intact_def ipc_buffer_valid_def setMRs_def
                  setMR_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> seL4_Call' cap info \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> do ret' <- seL4_GetMR' 0;
ret'a <- seL4_GetMR' 1;
ret'b <- seL4_GetMR' 2;
ret'c <- seL4_GetMR' 3;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 ret');
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 ret'a);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 ret'b);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 ret'c);
return info
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3)) \<Longrightarrow> \<forall>x. 0 \<le> 0 \<and> 0 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xa. 0 \<le> 1 \<and> 1 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xb. 0 \<le> 2 \<and> 2 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>xc. 0 \<le> 3 \<and> 3 < 120 \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xd. globals_frame_intact (setMR s (nat 0) x) \<and> ipc_buffer_valid (setMR s (nat 0) x) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xd. globals_frame_intact (setMR (setMR s (nat 0) x) (nat 1) xa) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) x) (nat 1) xa) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xd. globals_frame_intact (setMR (setMR (setMR s (nat 0) x) (nat 1) xa) (nat 2) xb) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) x) (nat 1) xa) (nat 2) xb) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xd. P info (setMR (setMR (setMR (setMR s (nat 0) x) (nat 1) xa) (nat 2) xb) (nat 3) xc)))))))) proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma seL4_Poll_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update
          (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and>
        badge \<noteq> NULL \<and>
        is_valid_w32 s badge\<rbrace>
    seL4_Poll' cap badge
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Poll'_def seL4_GetIPCBuffer'_def) apply (wp seL4_SetMR_wp) apply (simp add:globals_frame_intact_def ipc_buffer_valid_def setMRs_def
                  setMR_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge\<rbrace> seL4_Poll' cap badge \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge\<rbrace> do info___struct_seL4_MessageInfo_C <- unknown;
msg0___unsigned <- unknown;
msg1___unsigned <- unknown;
msg2___unsigned <- unknown;
msg3___unsigned <- unknown;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 msg0___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 msg1___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 msg2___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 msg3___unsigned);
y <- when (badge \<noteq> NULL) (do y <- guard (\<lambda>s. is_valid_w32 s badge);
modify (heap_w32_update (\<lambda>a. a(badge := cap)))
od);
return info___struct_seL4_MessageInfo_C
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x b v0 v1 v2 v3. P x (heap_w32_update (\<lambda>a. a(badge := b)) (setMRs s v0 v1 v2 v3))) \<and> badge \<noteq> NULL \<and> is_valid_w32 s badge \<Longrightarrow> \<forall>x xa xb xc xd. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR s (nat 0) xa) \<and> ipc_buffer_valid (setMR s (nat 0) xa) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xe. if badge \<noteq> NULL then P x (heap_w32_update (\<lambda>a. a(badge := cap)) (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd)) \<and> is_valid_w32 (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd) badge else P x (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd))))) proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma seL4_Wait_wp[wp_unsafe]:
  "\<lbrace>\<lambda>s. globals_frame_intact s \<and>
        ipc_buffer_valid s \<and>
        (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace>
    seL4_Wait' cap NULL
   \<lbrace>P\<rbrace>!" apply (simp add:seL4_Wait'_def) apply (wp seL4_SetMR_wp) apply (simp add:globals_frame_intact_def ipc_buffer_valid_def setMRs_def
                  setMR_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> seL4_Wait' cap NULL \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3))\<rbrace> do info___struct_seL4_MessageInfo_C <- unknown;
msg0___unsigned <- unknown;
msg1___unsigned <- unknown;
msg2___unsigned <- unknown;
msg3___unsigned <- unknown;
y <- exec_concrete lift_global_heap (seL4_SetMR' 0 msg0___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 1 msg1___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 2 msg2___unsigned);
y <- exec_concrete lift_global_heap (seL4_SetMR' 3 msg3___unsigned);
return info___struct_seL4_MessageInfo_C
od \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. globals_frame_intact s \<and> ipc_buffer_valid s \<and> (\<forall>x v0 v1 v2 v3. P x (setMRs s v0 v1 v2 v3)) \<Longrightarrow> \<forall>x xa xb xc xd. globals_frame_intact s \<and> ipc_buffer_valid s \<and> 0 \<le> 0 \<and> 0 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR s (nat 0) xa) \<and> ipc_buffer_valid (setMR s (nat 0) xa) \<and> 0 \<le> 1 \<and> 1 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> ipc_buffer_valid (setMR (setMR s (nat 0) xa) (nat 1) xb) \<and> 0 \<le> 2 \<and> 2 < 120 \<and> (\<forall>xe. globals_frame_intact (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> ipc_buffer_valid (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) \<and> 0 \<le> 3 \<and> 3 < 120 \<and> (\<forall>xe. P x (setMR (setMR (setMR (setMR s (nat 0) xa) (nat 1) xb) (nat 2) xc) (nat 3) xd))))) proof (prove)
goal:
No subgoals!
theory RPCFrom

lemma RPCFrom_run_nf: "\<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> RPCFrom__run' \<lbrace>P\<rbrace>!" apply (simp add: RPCFrom__run'_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> RPCFrom__run' \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r. P r s\<rbrace> return 0 \<lbrace>P\<rbrace>! proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>r. P r s \<Longrightarrow> P 0 s proof (prove)
goal:
No subgoals!
theory RPCTo

lemma abort_wp[wp]:
  "\<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>!" by (rule validNF_false_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> abort' \<lbrace>P\<rbrace>!