theory InterruptAcc_R

lemma setIRQState_corres:
  "irq_state_relation state state' \<Longrightarrow>
   corres dc \<top> \<top> (set_irq_state state irq) (setIRQState state' irq)" apply (simp add: set_irq_state_def setIRQState_def
                   bind_assoc[symmetric]) apply (subgoal_tac "(state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)") apply (rule corres_guard_imp) apply (rule corres_split_nor) apply (simp add: getInterruptState_def setInterruptState_def
                         simpler_gets_def simpler_modify_def bind_def) apply (simp add: simpler_modify_def[symmetric]) apply (rule corres_trivial, rule corres_modify) apply (simp add: state_relation_def swp_def) apply (clarsimp simp: interrupt_state_relation_def) apply (rule corres_machine_op) apply (rule corres_Id | simp)+ apply (rule no_fail_maskInterrupt) apply (wp | simp)+ apply (clarsimp simp: irq_state_relation_def
                 split: irq_state.split_asm irqstate.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (set_irq_state state irq) (setIRQState state' irq) proof (prove)
goal (1 subgoal):
 1. irq_state_relation state state' \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)
od) (do y <- do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od;
doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq)
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>_. True) (\<lambda>_. True) (do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)
od) (do y <- do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od;
doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq)
od)
 2. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?Q1 ?Q'1 (do y <- modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>);
do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)
od) (do y <- do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od;
doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq)
od)
 2. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ?Q'1 s
 4. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?P5 ?P'5 (modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>)) (do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od)
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s
 7. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?P5 ?P'5 (\<lambda>s. ({((), s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>)}, False)) (\<lambda>s. ({((), s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := state')) (ksInterruptState s)\<rparr>)}, False))
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s
 7. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?P5 ?P'5 (modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>)) (modify (\<lambda>s. s\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s))(irq := state')) (ksInterruptState s)\<rparr>))
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P5 and ?Q5) s
 6. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> (?P'5 and ?Q'5) s
 7. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>, s'\<lparr>ksInterruptState := intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s'))(irq := state')) (ksInterruptState s')\<rparr>) \<in> state_relation
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 6. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 7. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (7 subgoals):
 1. \<And>s s'. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); pspace_relation (kheap s) (ksPSpace s') \<and> ekheap_relation (ekheap s) (ksPSpace s') \<and> sched_act_relation (scheduler_action s) (ksSchedulerAction s') \<and> ready_queues_relation (ready_queues s) (ksReadyQueues s') \<and> ghost_relation (kheap s) (gsUserPages s') (gsCNodes s') \<and> cdt_relation (\<lambda>y. cte_wp_at (\<lambda>_. True) y s) (cdt s) (ctes_of s') \<and> cdt_list_relation (cdt_list s) (cdt s) (ctes_of s') \<and> revokable_relation (is_original_cap s) (null_filter (caps_of_state s)) (ctes_of s') \<and> (arch_state s, ksArchState s') \<in> arch_state_relation \<and> interrupt_state_relation (interrupt_irq_node s) (interrupt_states s) (ksInterruptState s') \<and> cur_thread s = ksCurThread s' \<and> idle_thread s = ksIdleThread s' \<and> machine_state s = ksMachineState s' \<and> work_units_completed s = ksWorkUnitsCompleted s' \<and> domain_index s = ksDomScheduleIdx s' \<and> domain_list s = ksDomSchedule s' \<and> cur_domain s = ksCurDomain s' \<and> domain_time s = ksDomainTime s'\<rbrakk> \<Longrightarrow> interrupt_state_relation (interrupt_irq_node s) ((interrupt_states s)(irq := state)) (intStateIRQTable_update (\<lambda>_. (intStateIRQTable (ksInterruptState s'))(irq := state')) (ksInterruptState s'))
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 4. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 6. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 7. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres dc ?R5 ?R'5 (do_machine_op (maskInterrupt (state = irq_state.IRQInactive) irq)) (doMachineOp (maskInterrupt (state' = irqstate.IRQInactive) irq))
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x. ?R5\<rbrace>
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x. ?R'5\<rbrace>
 4. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 6. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> corres_underlying Id False True dc (\<lambda>_. True) (\<lambda>_. True) (maskInterrupt (state = irq_state.IRQInactive) irq) (maskInterrupt (state' = irqstate.IRQInactive) irq)
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 6. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (6 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (maskInterrupt (state' = irqstate.IRQInactive) irq)
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 5. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 6. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (5 subgoals):
 1. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q5\<rbrace> modify (\<lambda>s. s\<lparr>interrupt_states := (interrupt_states s)(irq := state)\<rparr>) \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive)\<rbrakk> \<Longrightarrow> \<lbrace>?Q'5\<rbrace> do st <- getInterruptState;
setInterruptState (intStateIRQTable_update (\<lambda>_. (intStateIRQTable st)(irq := state')) st)
od \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q5) s
 4. \<And>s. \<lbrakk>irq_state_relation state state'; (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive); True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'5) s
 5. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal (1 subgoal):
 1. irq_state_relation state state' \<Longrightarrow> (state = irq_state.IRQInactive) = (state' = irqstate.IRQInactive) proof (prove)
goal:
No subgoals!