kings-crown/FVELER_Isabelle huggingface dataset:
theory Schedule_DR

lemma get_ipc_buffer_words_nextPC [simp]:
  "get_ipc_buffer_words m (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) =
   get_ipc_buffer_words m tcb" by (rule ext) (simp add: get_ipc_buffer_words_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_ipc_buffer_words m (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) = get_ipc_buffer_words m tcb
theory Schedule_DR

lemma get_tcb_mrs_nextPC [simp]:
  "get_tcb_mrs m (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) =
   get_tcb_mrs m tcb" by (simp add: get_tcb_mrs_def Let_def arch_tcb_context_get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb_mrs m (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) = get_tcb_mrs m tcb
theory Schedule_DR

lemma transform_tcb_NextIP:
  "transform_tcb m t (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP:= pc))) tcb)
  = transform_tcb m t tcb" by (auto simp add: transform_tcb_def transform_full_intent_def Let_def
                     cap_register_def ARM.capRegister_def
                     arch_tcb_context_get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_tcb m t (tcb_arch_update (tcb_context_update (\<lambda>ctx. ctx(NextIP := pc))) tcb) = transform_tcb m t tcb
theory Schedule_DR

lemma as_user_setNextPC_corres:
  "dcorres dc \<top> \<top> (return x) (as_user t (setNextPC pc))" supply option.case_cong[cong] apply (clarsimp simp: corres_underlying_def gets_the_def
                   as_user_def setNextPC_def get_tcb_def
                   setRegister_def simpler_modify_def
                   select_f_def return_def in_monad
                   set_object_def get_object_def
                  split: option.splits Structures_A.kernel_object.splits) apply (subst tcb_context_update_aux) apply (simp add: transform_def transform_current_thread_def) apply (clarsimp simp: transform_objects_update_kheap_same_caps
                        transform_tcb_NextIP transform_objects_update_same
                        arch_tcb_update_aux3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (as_user t (setNextPC pc)) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (as_user t (setNextPC pc)) proof (prove)
goal (1 subgoal):
 1. \<And>b x2a. kheap b t = Some (TCB x2a) \<Longrightarrow> transform (update_kheap ((kheap b)(t \<mapsto> TCB (x2a\<lparr>tcb_arch := arch_tcb_context_set ((arch_tcb_context_get (tcb_arch x2a))(NextIP := pc)) (tcb_arch x2a)\<rparr>))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b x2a. kheap b t = Some (TCB x2a) \<Longrightarrow> transform (update_kheap ((kheap b)(t \<mapsto> TCB (x2a\<lparr>tcb_arch := tcb_context_update (\<lambda>ctx. ctx(NextIP := pc)) (tcb_arch x2a)\<rparr>))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b x2a. kheap b t = Some (TCB x2a) \<Longrightarrow> transform_objects (update_kheap ((kheap b)(t \<mapsto> TCB (x2a\<lparr>tcb_arch := tcb_context_update (\<lambda>ctx. ctx(NextIP := pc)) (tcb_arch x2a)\<rparr>))) b) = transform_objects b proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma arch_decode_irq_control_error_corres:
  "\<not> (\<exists> ui. (Some (IrqControlIntent ui)) = (transform_intent (invocation_type label) args)) \<Longrightarrow>
     dcorres (dc \<oplus> anyrel) \<top> \<top>
      (throwError e)
      (Decode_A.arch_decode_irq_control_invocation label args slot (map fst excaps))" unfolding arch_decode_irq_control_invocation_def apply (cases "invocation_type label"; simp add: arch_decode_irq_control_invocation_def) apply (simp add: transform_intent_def arch_transform_intent_issue_irq_handler_def
               split: list.splits arch_invocation_label.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (IrqControlIntent ui) = transform_intent (invocation_type label) args \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (local.arch_decode_irq_control_invocation label args slot (map fst excaps)) proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (IrqControlIntent ui) = transform_intent (invocation_type label) args \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (if invocation_type label = ArchInvocationLabel ARMIRQIssueIRQHandler then if 4 \<le> length args \<and> 1 \<le> length (map fst excaps) then let irq_word = args ! 0; trigger = args ! 1; index = args ! 2; depth = args ! 3; cnode = map fst excaps ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE arch_check_irq irq_word;
irq_active <- liftE $ is_irq_active irq;
whenE irq_active $ throwError RevokeFirst;
dest_slot <- lookup_target_slot cnode (data_to_cptr index) (unat depth);
CSpaceAcc_A.ensure_empty dest_slot;
returnOk $ ArchIRQControlIssue irq dest_slot slot (trigger \<noteq> 0)
odE else throwError TruncatedMessage else throwError IllegalOperation) proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>\<forall>ui. Some (IrqControlIntent ui) \<noteq> transform_intent (ArchInvocationLabel x2) args; invocation_type label = ArchInvocationLabel x2\<rbrakk> \<Longrightarrow> 4 \<le> length args \<and> Suc 0 \<le> length excaps \<longrightarrow> x2 = ARMIRQIssueIRQHandler \<longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (let irq_word = args ! 0; irq = UCAST(32 \<rightarrow> 10) irq_word in doE y <- arch_check_irq irq_word;
irq_active <- liftE (is_irq_active irq);
y <- whenE irq_active (throwError RevokeFirst);
dest_slot <- CSpace_A.lookup_slot_for_cnode_op False (map fst excaps ! 0) (to_bl (args ! 2)) (unat (args ! 3));
y <- CSpaceAcc_A.ensure_empty dest_slot;
returnOk (ArchIRQControlIssue irq dest_slot slot (args ! Suc 0 \<noteq> 0))
odE) proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma decode_irq_handler_error_corres:
  "\<not> (\<exists> ui. (Some (IrqHandlerIntent ui)) = (transform_intent (invocation_type label') undefined)) \<Longrightarrow>
     dcorres (dc \<oplus> anyrel) \<top> \<top>
      (throwError e)
      (Decode_A.decode_irq_handler_invocation label' x' excaps')" by (auto simp: Decode_A.decode_irq_handler_invocation_def transform_intent_def
           simp flip: gen_invocation_type_eq split: list.splits )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<nexists>ui. Some (IrqHandlerIntent ui) = transform_intent (invocation_type label') undefined \<Longrightarrow> dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (throwError e) (Decode_A.decode_irq_handler_invocation label' x' excaps')
theory Interrupt_DR

lemma maskInterrupt_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt a x \<lbrace>\<lambda>x ms. underlying_memory ms = m\<rbrace>" by (simp add:maskInterrupt_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt a x \<lbrace>\<lambda>x ms. underlying_memory ms = m\<rbrace>
theory Interrupt_DR

lemma ackInterrupt_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> ackInterrupt x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" by (simp add:ackInterrupt_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> ackInterrupt x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
theory Interrupt_DR

lemma resetTimer_underlying_memory[wp]:
  "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> resetTimer \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" apply (simp add:resetTimer_def machine_op_lift_def) apply (simp add:machine_rest_lift_def ignore_failure_def split_def) apply wp apply (clarsimp simp:valid_def simpler_modify_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> resetTimer \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_rest_lift (ignore_failure resetTimer_impl) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> do mr <- gets machine_state_rest;
p <- select_f (if fst (resetTimer_impl mr) = {} then ({((), mr)}, False) else (fst (resetTimer_impl mr), False));
modify (machine_state_rest_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. underlying_memory s = m \<Longrightarrow> \<forall>x\<in>fst (if fst (resetTimer_impl (machine_state_rest s)) = {} then ({((), machine_state_rest s)}, False) else (fst (resetTimer_impl (machine_state_rest s)), False)). underlying_memory (s\<lparr>machine_state_rest := snd x\<rparr>) = m proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma transform_domain_time_update[iff]:
  "transform (s\<lparr>domain_time := a\<rparr>) = transform s" by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform (domain_time_update (\<lambda>_. a) s) = transform s
theory Interrupt_DR

lemma dec_domain_time_transform: "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> dec_domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" by (clarsimp simp: dec_domain_time_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> dec_domain_time \<lbrace>\<lambda>r s. transform s = cs\<rbrace>
theory Interrupt_DR

lemma timer_tick_dcorres: "dcorres dc P P' (return ()) timer_tick" apply (rule corres_noop) apply (simp add: timer_tick_def reschedule_required_def set_scheduler_action_def etcb_at_def split: option.splits | wp tcb_sched_action_transform dec_domain_time_transform thread_set_time_slice_transform | wpc | wp (once) hoare_vcg_all_lift hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return ()) timer_tick proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> P' s'\<rbrace> timer_tick \<lbrace>\<lambda>rv s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> dc () rv\<rbrace>
 2. \<And>s. \<lbrakk>P s; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> {ss'. transform (snd ss') = fst ss'} \<and> P' s') timer_tick proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma set_irq_state_original:
  "\<lbrace>\<lambda>s. P (is_original_cap s slot)\<rbrace> set_irq_state a b
         \<lbrace>\<lambda>rv s. P (is_original_cap s slot)\<rbrace>" by (clarsimp simp:set_irq_state_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_original_cap s slot)\<rbrace> set_irq_state a b \<lbrace>\<lambda>rv s. P (is_original_cap s slot)\<rbrace>
theory Interrupt_DR

lemma set_irq_state_dwp:
  "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace>
         set_irq_state irq_state.IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace>" apply (simp add:set_irq_state_def) apply (wp do_machine_op_wp) apply clarsimp apply (wp maskInterrupt_underlying_memory)+ apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def
                       transform_current_thread_def transform_asid_table_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> set_irq_state IRQSignal word \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(word := IRQSignal)\<rparr>);
do_machine_op (maskInterrupt False word)
od \<lbrace>\<lambda>r s. transform s = cs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y. \<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt False word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q1\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(word := IRQSignal)\<rparr>) \<lbrace>\<lambda>y ps. transform ps = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> maskInterrupt False word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>
 2. \<lbrace>?Q1\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(word := IRQSignal)\<rparr>) \<lbrace>\<lambda>y ps. transform ps = cs\<rbrace>
 3. \<And>s. transform s = cs \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. transform s = cs \<Longrightarrow> transform (s\<lparr>interrupt_states := (interrupt_states s)(word := IRQSignal)\<rparr>) = cs proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma dmo_setIRQTrigger_dcorres:
  "dcorres dc \<top> \<top> (return ()) (do_machine_op (setIRQTrigger irq trigger))" by (wpsimp simp: setIRQTrigger_def wp: dcorres_machine_op_noop)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (do_machine_op (setIRQTrigger irq trigger))
theory Interrupt_DR

lemma dcorres_invoke_irq_control:
  "dcorres dc \<top> (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs)
    (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation))
    (Interrupt_A.invoke_irq_control irq_control_invocation)" apply (case_tac irq_control_invocation) apply (simp add:corres_free_fail Interrupt_D.invoke_irq_control_def dcorres_invoke_irq_control_body) apply (simp add: dcorres_arch_invoke_irq_control[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation)) (Interrupt_A.invoke_irq_control irq_control_invocation) proof (prove)
goal (2 subgoals):
 1. \<And>x11 x12 x13. irq_control_invocation = IRQControl x11 x12 x13 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation)) (Interrupt_A.invoke_irq_control irq_control_invocation)
 2. \<And>x2. irq_control_invocation = ArchIRQControl x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation)) (Interrupt_A.invoke_irq_control irq_control_invocation) proof (prove)
goal (1 subgoal):
 1. \<And>x2. irq_control_invocation = ArchIRQControl x2 \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and irq_control_inv_valid irq_control_invocation and valid_etcbs) (Interrupt_D.invoke_irq_control (translate_irq_control_invocation irq_control_invocation)) (Interrupt_A.invoke_irq_control irq_control_invocation) proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma op_eq_simp: "((=) y) = (\<lambda>x. x = y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) y = (\<lambda>x. x = y)
theory Interrupt_DR

lemma get_irq_slot_not_idle_wp:
  "\<lbrace>valid_idle and valid_irq_node \<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>rv. not_idle_thread (fst rv)\<rbrace>" apply (wpsimp simp:get_irq_slot_def) apply (rule irq_node_image_not_idle) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle and valid_irq_node\<rbrace> KHeap_A.get_irq_slot word \<lbrace>\<lambda>rv. not_idle_thread (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_idle s; valid_irq_node s\<rbrakk> \<Longrightarrow> not_idle_thread (interrupt_irq_node s word) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_idle s; valid_irq_node s\<rbrakk> \<Longrightarrow> valid_idle s
 2. \<And>s. \<lbrakk>valid_idle s; valid_irq_node s\<rbrakk> \<Longrightarrow> valid_irq_node s proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma cte_wp_at_neq_slot_set_cap:
  "slot\<noteq> slot'  \<Longrightarrow> \<lbrace>cte_wp_at P slot and cte_at slot'\<rbrace>
            CSpaceAcc_A.set_cap cap.NullCap slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace>" apply (wp set_cap_cte_wp_at_cases) apply (clarsimp simp:cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slot \<noteq> slot' \<Longrightarrow> \<lbrace>cte_wp_at P slot and cte_wp_at (\<lambda>_. True) slot'\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot' \<lbrace>\<lambda>rv. cte_wp_at P slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>slot \<noteq> slot'; (cte_wp_at P slot and cte_wp_at (\<lambda>_. True) slot') s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) slot' s \<and> (slot = slot' \<longrightarrow> P cap.NullCap) \<and> (slot \<noteq> slot' \<longrightarrow> cte_wp_at P slot s) proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma cap_delete_one_not_idle [wp]:
  "\<lbrace>not_idle_thread t\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. not_idle_thread t\<rbrace>" apply (simp add: not_idle_thread_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>not_idle_thread t\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. not_idle_thread t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. t \<noteq> idle_thread s\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s. t \<noteq> idle_thread s\<rbrace> proof (prove)
goal:
No subgoals!
theory Interrupt_DR

lemma is_ntfn_capD:
  "is_ntfn_cap cap \<Longrightarrow> \<exists>ptr b rights. cap = cap.NotificationCap ptr b rights" by (case_tac cap,simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Structures_A.is_ntfn_cap cap \<Longrightarrow> \<exists>ptr b rights. cap = cap.NotificationCap ptr b rights
theory Syscall_DR

lemma decode_invocation_endpointcap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label') args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.EndpointCap a b c \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" apply (clarsimp simp: Decode_A.decode_invocation_def
                        Decode_D.decode_invocation_def) apply (rule corres_returnOk) apply (clarsimp simp: cdl_invocation_relation_def translate_invocation_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = cap.EndpointCap a b c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.EndpointCap a b c; excaps = transform_cap_list excaps'; invoked_cap' = cap.EndpointCap a b c; AllowWrite \<in> c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cdl_invocation.InvokeEndpoint (SyncMessage b (AllowGrant \<in> c) (AllowGrantReply \<in> c) a))) (returnOk (invocation.InvokeEndpoint a b (AllowGrant \<in> c) (AllowGrantReply \<in> c))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.EndpointCap a b c; excaps = transform_cap_list excaps'; invoked_cap' = cap.EndpointCap a b c; AllowWrite \<in> c; (s, s') \<in> {ss'. transform (snd ss') = fst ss'}; True; True\<rbrakk> \<Longrightarrow> cdl_invocation_relation (cdl_invocation.InvokeEndpoint (SyncMessage b (AllowGrant \<in> c) (AllowGrantReply \<in> c) a)) (invocation.InvokeEndpoint a b (AllowGrant \<in> c) (AllowGrantReply \<in> c)) proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma decode_invocation_notificationcap_corres:
  "\<lbrakk> Some intent = transform_intent (invocation_type label') args';
     invoked_cap_ref = transform_cslot_ptr invoked_cap_ref';
     invoked_cap = transform_cap invoked_cap';
     excaps = transform_cap_list excaps';
     invoked_cap' = cap.NotificationCap a b c \<rbrakk> \<Longrightarrow>
    dcorres (dc \<oplus> cdl_invocation_relation) \<top> \<top>
        (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent)
        (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps')" apply (clarsimp simp: Decode_A.decode_invocation_def Decode_D.decode_invocation_def) apply (auto simp: cdl_invocation_relation_def translate_invocation_def
             split:rights.splits intro!:corres_returnOk) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = transform_cap invoked_cap'; excaps = transform_cap_list excaps'; invoked_cap' = cap.NotificationCap a b c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (Decode_D.decode_invocation invoked_cap invoked_cap_ref excaps intent) (Decode_A.decode_invocation label' args' cap_index' invoked_cap_ref' invoked_cap' excaps') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Some intent = transform_intent (invocation_type label') args'; invoked_cap_ref = transform_cslot_ptr invoked_cap_ref'; invoked_cap = cdl_cap.NotificationCap a b c; excaps = transform_cap_list excaps'; invoked_cap' = cap.NotificationCap a b c; AllowWrite \<in> c\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> cdl_invocation_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (cdl_invocation.InvokeNotification (Signal b a))) (returnOk (invocation.InvokeNotification a b)) proof (prove)
goal:
No subgoals!
theory Syscall_DR

lemma fst_hd_map_eq: "\<lbrakk> xs \<noteq> []; fst (hd xs) = x \<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x" apply (case_tac xs) apply (auto simp: fst_def hd_def split: list.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xs \<noteq> []; fst (hd xs) = x\<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>xs \<noteq> []; fst (hd xs) = x; xs = []\<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x
 2. \<And>a list. \<lbrakk>xs \<noteq> []; fst (hd xs) = x; xs = a # list\<rbrakk> \<Longrightarrow> fst (hd (map (\<lambda>(x, y). (f x, g y)) xs)) = f x proof (prove)
goal:
No subgoals!