theory Ipc_C

lemma handleArchFaultReply':
  notes option.case_cong_weak [cong] wordSize_def'[simp]
  shows "(do
    sb \<leftarrow> lookupIPCBuffer False s;
    msg \<leftarrow> getMRs s sb tag;
    handleArchFaultReply f r (msgLabel tag) msg
  od) x' = handleArchFaultReply' f s r tag x'" supply  empty_fail_cond[simp] apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def
                bit_def msgLengthBits_def msgRegisters_unfold
                fromIntegral_simp1 fromIntegral_simp2
                shiftL_word) apply (simp add: bind_assoc) apply (clarsimp simp: mapM_def sequence_def bind_assoc asUser_bind_distrib
                        asUser_return submonad_asUser.fn_stateAssert) apply (case_tac f) apply (clarsimp simp: handleArchFaultReply_def asUser_getRegister_discarded
                          bind_subst_lift [OF stateAssert_stateAssert]
                          pred_conj_def) apply (rule bind_apply_cong [OF refl], rename_tac sb s'') apply (rule bind_apply_cong [OF refl], rename_tac rv r'') apply (case_tac sb, simp_all add: word_size n_msgRegisters_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (do sb <- lookupIPCBuffer False s;
getMRs s sb tag >>= handleArchFaultReply f r (msgLabel tag)
od) x' = handleArchFaultReply' f s r tag x' proof (prove)
goal (1 subgoal):
 1. (do sb <- lookupIPCBuffer False s;
getMRs s sb tag >>= handleArchFaultReply f r (msgLabel tag)
od) x' = handleArchFaultReply' f s r tag x' proof (prove)
goal (1 subgoal):
 1. (do sb <- lookupIPCBuffer False s;
do intSize <- return (word_of_nat wordSize);
hardwareMRs <- return (map Register [register.R2, register.R3, register.R4, register.R5]);
hardwareMRValues <- asUser s $ mapM getRegister hardwareMRs;
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * intSize)) [word_of_nat $ length hardwareMRs + 1 .e. 0x78]) >>= mapM loadWordUser;
values <- return (hardwareMRValues @ bufferMRValues);
return $ take (unat $ msgLength tag) values
od >>= handleArchFaultReply f r (msgLabel tag)
od) x' = (do label <- return $ msgLabel tag;
mlen <- return $ msgLength tag;
case f of ARM_H.VMFault x xa \<Rightarrow> do sendBuf <- lookupIPCBuffer False s;
stateAssert (tcb_at' s) [];
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od
od) x' proof (prove)
goal (1 subgoal):
 1. (do sb <- lookupIPCBuffer False s;
hardwareMRValues <- asUser s (mapM getRegister [register.R2, register.R3, register.R4, register.R5]);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) hardwareMRValues @ take (unat (msgLength tag) - length hardwareMRValues) bufferMRValues)
od) x' = (case f of ARM_H.VMFault x xa \<Rightarrow> do sendBuf <- lookupIPCBuffer False s;
stateAssert (tcb_at' s) [];
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) x' proof (prove)
goal (1 subgoal):
 1. (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) [rv, rva, rvb, rvc] @ take (unat (msgLength tag) - Suc (Suc (Suc (Suc 0)))) bufferMRValues)
od) x' = (case f of ARM_H.VMFault x xa \<Rightarrow> do sendBuf <- lookupIPCBuffer False s;
stateAssert (tcb_at' s) [];
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) x' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. f = ARM_H.VMFault x1 x2 \<Longrightarrow> (do sb <- lookupIPCBuffer False s;
rv <- asUser s (getRegister register.R2);
rva <- asUser s (getRegister register.R3);
rvb <- asUser s (getRegister register.R4);
rvc <- asUser s (getRegister register.R5);
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
handleArchFaultReply f r (msgLabel tag) (take (unat (msgLength tag)) [rv, rva, rvb, rvc] @ take (unat (msgLength tag) - Suc (Suc (Suc (Suc 0)))) bufferMRValues)
od) x' = (case f of ARM_H.VMFault x xa \<Rightarrow> do sendBuf <- lookupIPCBuffer False s;
stateAssert (tcb_at' s) [];
case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) x' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. f = ARM_H.VMFault x1 x2 \<Longrightarrow> (do sb <- lookupIPCBuffer False s;
rv <- stateAssert (tcb_at' s) [];
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) x' = (do sendBuf <- lookupIPCBuffer False s;
y <- stateAssert (tcb_at' s) [];
y <- case sendBuf of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) x' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 sb s''. \<lbrakk>f = ARM_H.VMFault x1 x2; (sb, s'') \<in> fst (lookupIPCBuffer False s x')\<rbrakk> \<Longrightarrow> (do rv <- stateAssert (tcb_at' s) [];
bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) s'' = (do y <- stateAssert (tcb_at' s) [];
y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) s'' proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 sb s'' rv r''. \<lbrakk>f = ARM_H.VMFault x1 x2; (sb, s'') \<in> fst (lookupIPCBuffer False s x'); (rv, r'') \<in> fst (stateAssert (tcb_at' s) [] s'')\<rbrakk> \<Longrightarrow> (do bufferMRValues <- case sb of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * 4)) [word_of_nat $ length [register.R2, register.R3, register.R4, register.R5] + 1 .e. 0x78]) >>= mapM loadWordUser;
return True
od) r'' = (do y <- case sb of None \<Rightarrow> return () | Some bufferPtr \<Rightarrow> do mapM loadWordUser (map (\<lambda>i. bufferPtr + PPtr (i * 4)) [SCAST(32 signed \<rightarrow> 32) n_msgRegisters + 1 .e. 0x78]);
return ()
od;
return True
od) r'' proof (prove)
goal:
No subgoals!