adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

crefine: split fastpath, rearrange Refine-based theory imports 

Several parts of CRefine did not or should not depend on anything
C-related, but the import hierarchy (and theory content) did not reflect
this. Namely:
* Move_C and ArchMove_C were intended to hold items that could be moved
  to Refine yet used `kernel_m` locale and imported the C spec.
* IsolatedThreadAction indicates how to rearrange statements in the
  design spec and has nothing to do with the C spec or framework.
* Fastpath_C contained the design spec of the fastpath, the design spec
  rewrite proofs, and the C refinement. Having to rebuild nearly all of
  CRefine to work on rewrite proofs wasted time.

In the new import hierarchy:
* Move_C imports only Refine; ArchMove_C builds on Move_C
* IsolatedThreadAction imports only ArchMove_C
* The fastpath proofs are split into the spec definition (Fastpath_Defs)
  and rewrite proofs (Fastpath_Equiv), which don't depend on anything
  C-related, with their C refinement remaining in Fastpath_C.

While it is possible to separate out the fastpath definitions and rewire
proofs into a separate image or even move them to Refine, development
experience indicates keeping them alongside their C refinement remains
more convenient for the proof engineer involved.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-05-05 16:26:38 +10:00 committed by Rafal Kolanski
parent d7867393f0
commit 9d404be331
66 changed files with 4848 additions and 4791 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

77
proof/crefine/ARM/ArchMove_C.thy
View File

@ -178,6 +178,83 @@ lemma valid_untyped':
nat_le_linear power_overflow sub_wrap add_0
add_0_right word_add_increasing word_less_1 word_less_sub_1)
(* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should
be equivalent to what we have in the abstract/design specs. We want a number for this definition
that automatically updates if the number of registers changes, and we sanity check it later
in msgRegisters_size_sanity *)
definition size_msgRegisters :: nat where
size_msgRegisters_pre_def: "size_msgRegisters \<equiv> size (ARM.msgRegisters)"
schematic_goal size_msgRegisters_def:
"size_msgRegisters = numeral ?x"
unfolding size_msgRegisters_pre_def ARM.msgRegisters_def
by (simp add: upto_enum_red fromEnum_def enum_register del: Suc_eq_numeral)
(simp only: Suc_eq_plus1_left, simp del: One_nat_def)
lemma length_msgRegisters[simplified size_msgRegisters_def]:
"length ARM_H.msgRegisters = size_msgRegisters"
by (simp add: size_msgRegisters_pre_def ARM_H.msgRegisters_def)
lemma cap_case_isPageDirectoryCap:
"(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid
| _ => g)
= (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, setThreadState,
updateFreeIndex, preemptionPoint
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps
ignore_del: preemptionPoint)
end
end

45
proof/crefine/ARM/CLevityCatch.thy
View File

@ -14,8 +14,6 @@ begin
context begin interpretation Arch . (*FIXME: arch_split*)
declare word_neq_0_conv [simp del]
(* Rule previously in the simpset, now not. *)
declare ptr_add_def' [simp]
@ -60,14 +58,6 @@ lemma no_overlap_new_cap_addrs_disjoint:
declare empty_fail_doMachineOp [simp]
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord)
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma asUser_get_registers:
"\<lbrace>tcb_at' target\<rbrace>
asUser target (mapM getRegister xs)
@ -93,36 +83,19 @@ lemma asUser_get_registers:
obj_at'_def)
done
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
(* only exists in Haskell, only used for C refinement *)
crunches writeTTBR0Ptr
for (empty_fail) empty_fail[wp,simp]
end
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
end

4
proof/crefine/ARM/CSpaceAcc_C.thy
View File

@ -181,10 +181,6 @@ lemma ccorres_pre_getIdleThread:
apply (clarsimp simp: rf_sr_ksIdleThread)
done
lemma cd_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma curDomain_sp:
"\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>"
apply wp

7
proof/crefine/ARM/CSpace_RAB_C.thy
View File

@ -74,13 +74,6 @@ lemma ccorres_req:
apply (clarsimp elim!: bexI [rotated])
done
lemma valid_cap_cte_at':
"\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'"
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (rule real_cte_at')
apply (erule spec)
done
declare ucast_id [simp]
declare resolveAddressBits.simps [simp del]

1761
proof/crefine/ARM/Fastpath_C.thy
View File

File diff suppressed because it is too large Load Diff

167
proof/crefine/ARM/Fastpath_Defs.thy Normal file
View File

@ -0,0 +1,167 @@
(*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2022, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(* Contains the design specification of optimised fast paths though the kernel.
These paths check for specific circumstances before engaging, otherwise
falling back to the full kernel design specification (callKernel).
For this reason, fastpath + callKernel is expected to be semantically
identical to callKernel. *)
theory Fastpath_Defs
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
definition
"fastpaths sysc \<equiv> case sysc of
SysCall \<Rightarrow> doE
curThread \<leftarrow> liftE $ getCurThread;
mi \<leftarrow> liftE $ getMessageInfo curThread;
cptr \<leftarrow> liftE $ asUser curThread $ getRegister capRegister;
fault \<leftarrow> liftE $ threadGet tcbFault curThread;
pickFastpath \<leftarrow> liftE $ alternative (return True) (return False);
unlessE (fault = None \<and> msgExtraCaps mi = 0
\<and> msgLength mi \<le> of_nat size_msgRegisters \<and> pickFastpath)
$ throwError ();
ctab \<leftarrow> liftE $ getThreadCSpaceRoot curThread >>= getCTE;
epCap \<leftarrow> unifyFailure (doE t \<leftarrow> resolveAddressBits (cteCap ctab) cptr (size cptr);
liftE (getSlotCap (fst t)) odE);
unlessE (isEndpointCap epCap \<and> capEPCanSend epCap)
$ throwError ();
ep \<leftarrow> liftE $ getEndpoint (capEPPtr epCap);
unlessE (isRecvEP ep) $ throwError ();
dest \<leftarrow> returnOk $ hd $ epQueue ep;
newVTable \<leftarrow> liftE $ getThreadVSpaceRoot dest >>= getCTE;
unlessE (isValidVTableRoot $ cteCap newVTable) $ throwError ();
pd \<leftarrow> returnOk $ capPDBasePtr $ capCap $ cteCap newVTable;
curDom \<leftarrow> liftE $ curDomain;
curPrio \<leftarrow> liftE $ threadGet tcbPriority curThread;
destPrio \<leftarrow> liftE $ threadGet tcbPriority dest;
highest \<leftarrow> liftE $ isHighestPrio curDom destPrio;
unlessE (destPrio \<ge> curPrio \<or> highest) $ throwError ();
unlessE (capEPCanGrant epCap \<or> capEPCanGrantReply epCap) $ throwError ();
asidMap \<leftarrow> liftE $ gets $ armKSASIDMap o ksArchState;
unlessE (\<exists>v. {hwasid. (hwasid, pd) \<in> ran asidMap} = {v})
$ throwError ();
destDom \<leftarrow> liftE $ threadGet tcbDomain dest;
unlessE (destDom = curDom) $ throwError ();
liftE $ do
setEndpoint (capEPPtr epCap)
(case tl (epQueue ep) of [] \<Rightarrow> IdleEP | _ \<Rightarrow> RecvEP (tl (epQueue ep)));
threadSet (tcbState_update (\<lambda>_. BlockedOnReply)) curThread;
replySlot \<leftarrow> getThreadReplySlot curThread;
callerSlot \<leftarrow> getThreadCallerSlot dest;
replySlotCTE \<leftarrow> getCTE replySlot;
assert (mdbNext (cteMDBNode replySlotCTE) = 0
\<and> isReplyCap (cteCap replySlotCTE)
\<and> capReplyMaster (cteCap replySlotCTE)
\<and> mdbFirstBadged (cteMDBNode replySlotCTE)
\<and> mdbRevocable (cteMDBNode replySlotCTE));
destState \<leftarrow> getThreadState dest;
cteInsert (ReplyCap curThread False (blockingIPCCanGrant destState)) replySlot callerSlot;
forM_x (take (unat (msgLength mi)) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser curThread (getRegister r);
asUser dest (setRegister r v) od);
setThreadState Running dest;
Arch.switchToThread dest;
setCurThread dest;
asUser dest $ zipWithM_x setRegister
[badgeRegister, msgInfoRegister]
[capEPBadge epCap, wordFromMessageInfo (mi\<lparr> msgCapsUnwrapped := 0 \<rparr>)];
stateAssert kernelExitAssertions []
od
odE <catch> (\<lambda>_. callKernel (SyscallEvent sysc))
| SysReplyRecv \<Rightarrow> doE
curThread \<leftarrow> liftE $ getCurThread;
mi \<leftarrow> liftE $ getMessageInfo curThread;
cptr \<leftarrow> liftE $ asUser curThread $ getRegister capRegister;
fault \<leftarrow> liftE $ threadGet tcbFault curThread;
pickFastpath \<leftarrow> liftE $ alternative (return True) (return False);
unlessE (fault = None \<and> msgExtraCaps mi = 0
\<and> msgLength mi \<le> of_nat size_msgRegisters \<and> pickFastpath)
$ throwError ();
ctab \<leftarrow> liftE $ getThreadCSpaceRoot curThread >>= getCTE;
epCap \<leftarrow> unifyFailure (doE t \<leftarrow> resolveAddressBits (cteCap ctab) cptr (size cptr);
liftE (getSlotCap (fst t)) odE);
unlessE (isEndpointCap epCap \<and> capEPCanReceive epCap)
$ throwError ();
bound_ntfn \<leftarrow> liftE $ getBoundNotification curThread;
active_ntfn \<leftarrow> liftE $ case bound_ntfn of None \<Rightarrow> return False
| Some ntfnptr \<Rightarrow> liftM isActive $ getNotification ntfnptr;
unlessE (\<not> active_ntfn) $ throwError ();
ep \<leftarrow> liftE $ getEndpoint (capEPPtr epCap);
unlessE (\<not> isSendEP ep) $ throwError ();
callerSlot \<leftarrow> liftE $ getThreadCallerSlot curThread;
callerCTE \<leftarrow> liftE $ getCTE callerSlot;
callerCap \<leftarrow> returnOk $ cteCap callerCTE;
unlessE (isReplyCap callerCap \<and> \<not> capReplyMaster callerCap)
$ throwError ();
caller \<leftarrow> returnOk $ capTCBPtr callerCap;
callerFault \<leftarrow> liftE $ threadGet tcbFault caller;
unlessE (callerFault = None) $ throwError ();
newVTable \<leftarrow> liftE $ getThreadVSpaceRoot caller >>= getCTE;
unlessE (isValidVTableRoot $ cteCap newVTable) $ throwError ();
curDom \<leftarrow> liftE $ curDomain;
callerPrio \<leftarrow> liftE $ threadGet tcbPriority caller;
highest \<leftarrow> liftE $ isHighestPrio curDom callerPrio;
unlessE highest $ throwError ();
pd \<leftarrow> returnOk $ capPDBasePtr $ capCap $ cteCap newVTable;
asidMap \<leftarrow> liftE $ gets $ armKSASIDMap o ksArchState;
unlessE (\<exists>v. {hwasid. (hwasid, pd) \<in> ran asidMap} = {v})
$ throwError ();
callerDom \<leftarrow> liftE $ threadGet tcbDomain caller;
unlessE (callerDom = curDom) $ throwError ();
liftE $ do
epCanGrant \<leftarrow> return $ capEPCanGrant epCap;
threadSet (tcbState_update (\<lambda>_. BlockedOnReceive (capEPPtr epCap) epCanGrant)) curThread;
setEndpoint (capEPPtr epCap)
(case ep of IdleEP \<Rightarrow> RecvEP [curThread] | RecvEP ts \<Rightarrow> RecvEP (ts @ [curThread]));
mdbPrev \<leftarrow> liftM (mdbPrev o cteMDBNode) $ getCTE callerSlot;
assert (mdbPrev \<noteq> 0);
updateMDB mdbPrev (mdbNext_update (K 0) o mdbFirstBadged_update (K True)
o mdbRevocable_update (K True));
setCTE callerSlot makeObject;
forM_x (take (unat (msgLength mi)) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser curThread (getRegister r);
asUser caller (setRegister r v) od);
setThreadState Running caller;
Arch.switchToThread caller;
setCurThread caller;
asUser caller $ zipWithM_x setRegister
[badgeRegister, msgInfoRegister]
[0, wordFromMessageInfo (mi\<lparr> msgCapsUnwrapped := 0 \<rparr>)];
stateAssert kernelExitAssertions []
od
odE <catch> (\<lambda>_. callKernel (SyscallEvent sysc))
| _ \<Rightarrow> callKernel (SyscallEvent sysc)"
end
end

1901
proof/crefine/ARM/Fastpath_Equiv.thy Normal file
View File

File diff suppressed because it is too large Load Diff

5
proof/crefine/ARM/Finalise_C.thy
View File

@ -13,11 +13,6 @@ begin
declare if_split [split del]
lemma empty_fail_getEndpoint:
"empty_fail (getEndpoint ep)"
unfolding getEndpoint_def
by (auto intro: empty_fail_getObject)
definition
"option_map2 f m = option_map f \<circ> m"

4
proof/crefine/ARM/Invoke_C.thy
View File

@ -1412,10 +1412,6 @@ lemma deleteObjects_gsCNodes_at_pt:
| wp (once) hoare_drop_imps)+
done
crunches setThreadState, updateFreeIndex, preemptionPoint
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(simp: unless_def whenE_def ignore_del: preemptionPoint)
lemma resetUntypedCap_gsCNodes_at_pt:
"\<lbrace>(\<lambda>s. P (gsCNodes s ptr))
and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot

7
proof/crefine/ARM/IpcCancel_C.thy
View File

@ -2505,13 +2505,6 @@ lemma cancelSignal_ccorres [corres]:
| clarsimp simp: eq_commute
| drule_tac x=thread in bspec)+
lemma ko_at_valid_ep':
"\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
apply (erule obj_atE')
apply (erule (1) valid_objsE')
apply (simp add: projectKOs valid_obj'_def)
done
lemma cmap_relation_ep:
"(s, s') \<in> rf_sr \<Longrightarrow>
cmap_relation (map_to_eps (ksPSpace s)) (cslift s') Ptr (cendpoint_relation (cslift s'))"

7
proof/crefine/ARM/Ipc_C.thy
View File

@ -1279,13 +1279,6 @@ lemma ccorres_add_getRegister:
apply fastforce
done
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma exceptionMessage_ccorres:
"n < unat n_exceptionMessage
\<Longrightarrow> register_from_H (ARM_H.exceptionMessage ! n)

52
proof/crefine/ARM/IsolatedThreadAction.thy
View File

@ -5,7 +5,7 @@
*)
theory IsolatedThreadAction
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
imports ArchMove_C
begin
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
@ -119,7 +119,8 @@ lemmas setEndpoint_obj_at_tcb' = setEndpoint_obj_at'_tcb
lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
context kernel_m begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
@ -138,8 +139,6 @@ lemma setObject_modify:
apply (simp add: simpler_modify_def)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma getObject_return:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d;
@ -233,6 +232,8 @@ lemma isolate_thread_actions_asUser:
apply (case_tac ko, simp)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setRegister_simple:
"setRegister r v = (\<lambda>con. ({((), con (r := v))}, False))"
by (simp add: setRegister_def simpler_modify_def)
@ -240,6 +241,7 @@ lemma setRegister_simple:
lemma zipWithM_setRegister_simple:
"zipWithM_x setRegister rs vs
= (\<lambda>con. ({((), foldl (\<lambda>con (r, v). con (r := v)) con (zip rs vs))}, False))"
supply if_split[split del]
apply (simp add: zipWithM_x_mapM_x)
apply (induct ("zip rs vs"))
apply (simp add: mapM_x_Nil return_def)
@ -260,6 +262,7 @@ lemma map_to_ctes_partial_overwrite:
"\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
map_to_ctes (partial_overwrite idx tsrs (ksPSpace s))
= ctes_of s"
supply if_split[split del]
apply (rule ext)
apply (frule dom_partial_overwrite[where tsrs=tsrs])
apply (simp add: map_to_ctes_def partial_overwrite_def
@ -609,6 +612,7 @@ lemma page_directory_at_partial_overwrite:
lemma findPDForASID_isolatable:
"thread_actions_isolatable idx (findPDForASID asid)"
supply if_split[split del]
apply (simp add: findPDForASID_def liftE_bindE liftME_def bindE_assoc
case_option_If2 assertE_def liftE_def checkPDAt_def
stateAssert_def2
@ -648,6 +652,7 @@ lemma getHWASID_isolatable:
lemma setVMRoot_isolatable:
"thread_actions_isolatable idx (setVMRoot t)"
supply if_split[split del]
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def
locateSlot_conv getSlotCap_def
cap_case_isPageDirectoryCap if_bool_simps
@ -706,24 +711,17 @@ lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>
lemmas empty_fail_user_getreg = empty_fail_asUser[OF empty_fail_getRegister]
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma copyMRs_simple:
"msglen \<le> of_nat (length ARM_H.msgRegisters) \<longrightarrow>
"msglen \<le> of_nat (length msgRegisters) \<longrightarrow>
copyMRs sender sbuf receiver rbuf msglen
= forM_x (take (unat msglen) ARM_H.msgRegisters)
= forM_x (take (unat msglen) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser receiver (setRegister r v) od)
>>= (\<lambda>rv. return msglen)"
apply (clarsimp simp: copyMRs_def mapM_discarded)
apply (rule bind_cong[OF refl])
apply (simp add: length_msgRegisters n_msgRegisters_def min_def
word_le_nat_alt
apply (simp add: min_def word_le_nat_alt length_msgRegisters
upto_enum_red fromEnum_def enum_register
split: option.split)
apply (simp add: upto_enum_def mapM_Nil)
done
@ -732,16 +730,16 @@ lemma doIPCTransfer_simple_rewrite:
"monadic_rewrite True True
((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0
\<and> msgLength (messageInfoFromWord msgInfo)
\<le> of_nat (length ARM_H.msgRegisters))
\<le> of_nat (length msgRegisters))
and obj_at' (\<lambda>tcb. tcbFault tcb = None
\<and> (atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender)
(doIPCTransfer sender ep badge grant rcvr)
(do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od)
(take (unat (msgLength (messageInfoFromWord msgInfo))) ARM_H.msgRegisters);
(take (unat (msgLength (messageInfoFromWord msgInfo))) msgRegisters);
y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
asUser rcvr (setRegister ARM_H.badgeRegister badge)
asUser rcvr (setRegister badgeRegister badge)
od)"
supply if_cong[cong]
apply (rule monadic_rewrite_gen_asm)
@ -875,7 +873,7 @@ lemma oblivious_setVMRoot_schact:
lemma oblivious_switchToThread_schact:
"oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)"
apply (simp add: Thread_H.switchToThread_def ARM_H.switchToThread_def bind_assoc
apply (simp add: Thread_H.switchToThread_def switchToThread_def bind_assoc
getCurThread_def setCurThread_def threadGet_def liftM_def
threadSet_def tcbSchedEnqueue_def unless_when asUser_def
getQueue_def setQueue_def storeWordUser_def setRegister_def
@ -937,8 +935,6 @@ begin
crunch obj_at_dom[wp]: rescheduleRequired "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
end
context kernel_m begin
lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
@ -970,6 +966,8 @@ lemma bind_assoc:
= do x \<leftarrow> m; y \<leftarrow> f x; g y od"
by (rule bind_assoc)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>
\<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
@ -994,6 +992,7 @@ lemma setObject_modify_assert:
lemma setEndpoint_isolatable:
"thread_actions_isolatable idx (setEndpoint p e)"
supply if_split[split del]
apply (simp add: setEndpoint_def setObject_modify_assert
assert_def)
apply (case_tac "p \<in> range idx")
@ -1087,6 +1086,7 @@ lemma partial_overwrite_fun_upd2:
lemma setCTE_isolatable:
"thread_actions_isolatable idx (setCTE p v)"
supply if_split[split del]
apply (simp add: setCTE_assert_modify)
apply (clarsimp simp: thread_actions_isolatable_def
monadic_rewrite_def fun_eq_iff
@ -1149,7 +1149,7 @@ lemma assert_isolatable:
lemma cteInsert_isolatable:
"thread_actions_isolatable idx (cteInsert cap src dest)"
supply if_cong[cong]
supply if_split[split del] if_cong[cong]
apply (simp add: cteInsert_def updateCap_def updateMDB_def
Let_def setUntypedCapAsFull_def)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -1249,7 +1249,7 @@ lemma threadGet_isolatable:
lemma switchToThread_isolatable:
"thread_actions_isolatable idx (Arch.switchToThread t)"
apply (simp add: ARM_H.switchToThread_def
apply (simp add: switchToThread_def
storeWordUser_def stateAssert_def2)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
gets_isolatable setVMRoot_isolatable
@ -1319,7 +1319,7 @@ lemma tcb_at_KOTCB_upd:
= tcb_at' p s"
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
split: if_split)
apply (simp add: ps_clear_def)
apply (fastforce simp add: ps_clear_def)
done
definition
@ -1335,6 +1335,7 @@ lemma copy_register_isolate:
asUser dest (setRegister r' (rf v)) od)
(isolate_thread_actions idx (return ())
(copy_register_tsrs x y r r' rf) id)"
supply if_split[split del]
apply (simp add: asUser_def split_def bind_assoc
getRegister_def setRegister_def
select_f_returns isolate_thread_actions_def
@ -1479,7 +1480,7 @@ lemmas fastpath_isolate_rewrites
lemma lookupIPCBuffer_isolatable:
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
supply if_cong[cong]
supply if_split[split del] if_cong[cong]
apply (simp add: lookupIPCBuffer_def)
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
@ -1500,6 +1501,7 @@ lemma setThreadState_rewrite_simple:
(\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s)
(setThreadState st t)
(threadSet (tcbState_update (\<lambda>_. st)) t)"
supply if_split[split del]
apply (simp add: setThreadState_def)
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans)

11
proof/crefine/ARM/PSpace_C.thy
View File

@ -8,14 +8,7 @@ theory PSpace_C
imports Ctac_lemmas_C
begin
context kernel begin
lemma koTypeOf_injectKO:
fixes v :: "'a :: pspace_storable" shows
"koTypeOf (injectKO v) = koType TYPE('a)"
apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
apply (simp add: project_koType[symmetric])
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_obj_at_pre:
"\<lbrakk> updateObject ko = updateObject_default ko;
@ -48,7 +41,9 @@ lemma setObject_obj_at_pre:
apply clarsimp
done
end
context kernel begin
lemma setObject_ccorres_helper:
fixes ko :: "'a :: pspace_storable"

12
proof/crefine/ARM/Refine_C.thy
View File

@ -7,7 +7,7 @@
chapter "Toplevel Refinement Statement"
theory Refine_C
imports Init_C Fastpath_C CToCRefine
imports Init_C Fastpath_Equiv Fastpath_C CToCRefine
begin
context begin interpretation Arch . (*FIXME: arch_split*)
@ -18,6 +18,14 @@ end
context kernel_m
begin
text \<open>Assemble fastpaths\<close>
lemmas fastpath_call_ccorres_callKernel
= monadic_rewrite_ccorres_assemble[OF fastpath_call_ccorres fastpath_callKernel_SysCall_corres]
lemmas fastpath_reply_recv_ccorres_callKernel
= monadic_rewrite_ccorres_assemble[OF fastpath_reply_recv_ccorres fastpath_callKernel_SysReplyRecv_corres]
declare liftE_handle [simp]
lemma schedule_sch_act_wf:
@ -609,13 +617,13 @@ lemma ccorres_get_registers:
"StrictC'_register_defs")
done
lemma callKernel_withFastpath_corres_C:
"corres_underlying rf_sr False True dc
(all_invs' e)
\<top>
(callKernel e) (callKernel_withFastpath_C e)"
using no_fail_callKernel [of e] callKernel_corres_C [of e]
supply if_split[split del]
apply (cases "e = SyscallEvent syscall.SysCall \<or>
e = SyscallEvent syscall.SysReplyRecv")
apply (simp_all add: callKernel_withFastpath_C_def

5
proof/crefine/ARM/Retype_C.thy
View File

@ -6444,11 +6444,6 @@ end
context begin interpretation Arch . (*FIXME: arch_split*)
crunches insertNewCap, Arch_createNewCaps, threadSet, "Arch.createObject"
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps)
lemma createNewCaps_1_gsCNodes_p:
"\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>"
apply (simp add: createNewCaps_def)

74
proof/crefine/ARM/SR_lemmas_C.thy
View File

@ -296,67 +296,6 @@ lemma cmdbnode_relation_mdb_node_to_H [simp]:
unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def
by (fastforce split: option.splits)
(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*)
lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ tcbBlockSizeBits"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)
hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
thus ?thesis using yq by simp
qed
lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
apply (rule is_aligned_no_overflow' [OF al])
done
thus ?thesis using yq by (simp add: field_simps)
qed
lemmas tcbSlots =
tcbCTableSlot_def tcbVTableSlot_def
tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
lemma updateObject_cte_tcb:
assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
shows "updateObject ctea (KOTCB tcb) ptr ptr' next =
(do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
definition
tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> word32 \<times> word32 \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> word32 option"
where
@ -665,10 +604,6 @@ proof -
qed fact+
qed
lemma ctes_of_cte_at:
"ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
by (simp add: cte_wp_at_ctes_of)
lemma cor_map_relI:
assumes dm: "dom am = dom am'"
and rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';
@ -953,6 +888,7 @@ abbreviation
lemma valid_mdb_ctes_of_next:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbNext (cteMDBNode cte)) s"
unfolding valid_mdb'_def valid_mdb_ctes_def
supply word_neq_0_conv[simp del]
apply clarsimp
apply (erule (2) valid_dlistE)
apply (simp add: cte_wp_at_ctes_of)
@ -961,6 +897,7 @@ lemma valid_mdb_ctes_of_next:
lemma valid_mdb_ctes_of_prev:
"\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbPrev (cteMDBNode cte)) s"
unfolding valid_mdb'_def valid_mdb_ctes_def
supply word_neq_0_conv[simp del]
apply clarsimp
apply (erule (2) valid_dlistE)
apply (simp add: cte_wp_at_ctes_of)
@ -2196,6 +2133,9 @@ lemma unat_scast_numDomains:
"unat (SCAST(32 signed \<rightarrow> machine_word_len) Kernel_C.numDomains) = unat Kernel_C.numDomains"
by (simp add: scast_eq sint_numDomains_to_H unat_numDomains_to_H numDomains_machine_word_safe)
end
end
lemma msgRegisters_size_sanity:
"size_msgRegisters = unat (n_msgRegisters)"
by (simp add: n_msgRegisters_def size_msgRegisters_def)
end
end

16
proof/crefine/ARM/Syscall_C.thy
View File

@ -1131,22 +1131,6 @@ lemma deleteCallerCap_ccorres [corres]:
tcb_aligned')
done
(* FIXME: MOVE *)
lemma cap_case_EndpointCap_NotificationCap:
"(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
| NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3
| _ \<Rightarrow> h)
= (if isEndpointCap cap
then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
(capEPCanGrant cap) (capEPCanGrantReply cap)
else if isNotificationCap cap
then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
else h)"
by (simp add: isCap_simps
split: capability.split)
lemma invs_valid_objs_strengthen:
"invs' s \<longrightarrow> valid_objs' s" by fastforce

11
proof/crefine/ARM/Tcb_C.thy
View File

@ -8,17 +8,6 @@ theory Tcb_C
imports Delete_C Ipc_C
begin
lemma asUser_obj_at' :
"\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
including no_pre
apply (simp add: asUser_def)
apply wp
apply (case_tac "t=t'"; clarsimp)
apply (rule hoare_drop_imps)
apply wp
done
lemma getObject_sched:
"(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
(x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"

12
proof/crefine/ARM/VSpace_C.thy
View File

@ -786,18 +786,6 @@ lemma lookupPTSlot_ccorres:
split: ARM_H.pde.split_asm)
done
lemma cap_case_isPageDirectoryCap:
"(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid
| _ => g)
= (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
(* FIXME: MOVE to CSpaceAcc_C *)
lemma ccorres_pre_gets_armKSASIDTable_ksArchState:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"

89
proof/crefine/ARM_HYP/ArchMove_C.thy
View File

@ -231,18 +231,6 @@ lemma empty_fail_archThreadGet [intro!, wp, simp]:
"empty_fail (archThreadGet f p)"
by (simp add: archThreadGet_def getObject_def split_def)
lemma cap_case_EndpointCap_NotificationCap:
"(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
| NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3
| _ \<Rightarrow> h)
= (if isEndpointCap cap
then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
(capEPCanGrant cap) (capEPCanGrantReply cap)
else if isNotificationCap cap
then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
else h)"
by (simp add: isCap_simps split: capability.split, blast)
lemma mab_gt_2 [simp]:
"2 \<le> msg_align_bits" by (simp add: msg_align_bits)
@ -583,6 +571,83 @@ lemma valid_untyped':
nat_le_linear power_overflow sub_wrap add_0
add_0_right word_add_increasing word_less_1 word_less_sub_1)
(* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should
be equivalent to what we have in the abstract/design specs. We want a number for this definition
that automatically updates if the number of registers changes, and we sanity check it later
in msgRegisters_size_sanity *)
definition size_msgRegisters :: nat where
size_msgRegisters_pre_def: "size_msgRegisters \<equiv> size (ARM_HYP.msgRegisters)"
schematic_goal size_msgRegisters_def:
"size_msgRegisters = numeral ?x"
unfolding size_msgRegisters_pre_def ARM_HYP.msgRegisters_def
by (simp add: upto_enum_red fromEnum_def enum_register del: Suc_eq_numeral)
(simp only: Suc_eq_plus1_left, simp del: One_nat_def)
lemma length_msgRegisters[simplified size_msgRegisters_def]:
"length ARM_HYP_H.msgRegisters = size_msgRegisters"
by (simp add: size_msgRegisters_pre_def ARM_HYP_H.msgRegisters_def)
lemma cap_case_isPageDirectoryCap:
"(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid
| _ => g)
= (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, setThreadState,
updateFreeIndex, preemptionPoint
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps
ignore_del: preemptionPoint)
end
end

42
proof/crefine/ARM_HYP/CLevityCatch.thy
View File

@ -60,14 +60,6 @@ lemma no_overlap_new_cap_addrs_disjoint:
declare empty_fail_doMachineOp [simp]
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord)
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getExtraCPtrs [intro!, simp]:
"empty_fail (getExtraCPtrs sendBuffer info)"
apply (simp add: getExtraCPtrs_def)
@ -114,32 +106,6 @@ lemma asUser_get_registers:
obj_at'_def)
done
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma exec_Basic_Guard_UNIV:
"Semantic.exec \<Gamma> (Basic f;; Guard F UNIV (Basic g)) x y =
Semantic.exec \<Gamma> (Basic (g o f)) x y"
@ -171,4 +137,12 @@ lemma option_to_ptr_not_0:
"\<lbrakk> p \<noteq> 0 ; option_to_ptr v = Ptr p \<rbrakk> \<Longrightarrow> v = Some p"
by (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
end

3
proof/crefine/ARM_HYP/CSpaceAcc_C.thy
View File

@ -188,9 +188,6 @@ lemma ccorres_pre_getIdleThread:
done
lemma cd_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma curDomain_sp:
"\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>"
apply wp

8
proof/crefine/ARM_HYP/CSpace_RAB_C.thy
View File

@ -92,14 +92,6 @@ lemma ccorres_req:
apply (clarsimp elim!: bexI [rotated])
done
lemma valid_cap_cte_at':
"\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'"
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (rule real_cte_at')
apply (erule spec)
done
lemma rightsFromWord_wordFromRights:
"rightsFromWord (wordFromRights rghts) = rghts"
apply (cases rghts)

2219
proof/crefine/ARM_HYP/Fastpath_C.thy
View File

File diff suppressed because it is too large Load Diff

167
proof/crefine/ARM_HYP/Fastpath_Defs.thy Normal file
View File

@ -0,0 +1,167 @@
(*
* Copyright 2014, General Dynamics C4 Systems
* Copyright 2022, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: GPL-2.0-only
*)
(* Contains the design specification of optimised fast paths though the kernel.
These paths check for specific circumstances before engaging, otherwise
falling back to the full kernel design specification (callKernel).
For this reason, fastpath + callKernel is expected to be semantically
identical to callKernel. *)
theory Fastpath_Defs
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
definition
"fastpaths sysc \<equiv> case sysc of
SysCall \<Rightarrow> doE
curThread \<leftarrow> liftE $ getCurThread;
mi \<leftarrow> liftE $ getMessageInfo curThread;
cptr \<leftarrow> liftE $ asUser curThread $ getRegister capRegister;
fault \<leftarrow> liftE $ threadGet tcbFault curThread;
pickFastpath \<leftarrow> liftE $ alternative (return True) (return False);
unlessE (fault = None \<and> msgExtraCaps mi = 0
\<and> msgLength mi \<le> of_nat size_msgRegisters \<and> pickFastpath)
$ throwError ();
ctab \<leftarrow> liftE $ getThreadCSpaceRoot curThread >>= getCTE;
epCap \<leftarrow> unifyFailure (doE t \<leftarrow> resolveAddressBits (cteCap ctab) cptr (size cptr);
liftE (getSlotCap (fst t)) odE);
unlessE (isEndpointCap epCap \<and> capEPCanSend epCap)
$ throwError ();
ep \<leftarrow> liftE $ getEndpoint (capEPPtr epCap);
unlessE (isRecvEP ep) $ throwError ();
dest \<leftarrow> returnOk $ hd $ epQueue ep;
newVTable \<leftarrow> liftE $ getThreadVSpaceRoot dest >>= getCTE;
unlessE (isValidVTableRoot $ cteCap newVTable) $ throwError ();
pd \<leftarrow> returnOk $ capPDBasePtr $ capCap $ cteCap newVTable;
curDom \<leftarrow> liftE $ curDomain;
curPrio \<leftarrow> liftE $ threadGet tcbPriority curThread;
destPrio \<leftarrow> liftE $ threadGet tcbPriority dest;
highest \<leftarrow> liftE $ isHighestPrio curDom destPrio;
unlessE (destPrio \<ge> curPrio \<or> highest) $ throwError ();
unlessE (capEPCanGrant epCap \<or> capEPCanGrantReply epCap) $ throwError ();
asidMap \<leftarrow> liftE $ gets $ armKSASIDMap o ksArchState;
unlessE (\<exists>v. {hwasid. (hwasid, pd) \<in> ran asidMap} = {v})
$ throwError ();
destDom \<leftarrow> liftE $ threadGet tcbDomain dest;
unlessE (destDom = curDom) $ throwError ();
liftE $ do
setEndpoint (capEPPtr epCap)
(case tl (epQueue ep) of [] \<Rightarrow> IdleEP | _ \<Rightarrow> RecvEP (tl (epQueue ep)));
threadSet (tcbState_update (\<lambda>_. BlockedOnReply)) curThread;
replySlot \<leftarrow> getThreadReplySlot curThread;
callerSlot \<leftarrow> getThreadCallerSlot dest;
replySlotCTE \<leftarrow> getCTE replySlot;
assert (mdbNext (cteMDBNode replySlotCTE) = 0
\<and> isReplyCap (cteCap replySlotCTE)
\<and> capReplyMaster (cteCap replySlotCTE)
\<and> mdbFirstBadged (cteMDBNode replySlotCTE)
\<and> mdbRevocable (cteMDBNode replySlotCTE));
destState \<leftarrow> getThreadState dest;
cteInsert (ReplyCap curThread False (blockingIPCCanGrant destState)) replySlot callerSlot;
forM_x (take (unat (msgLength mi)) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser curThread (getRegister r);
asUser dest (setRegister r v) od);
setThreadState Running dest;
Arch.switchToThread dest;
setCurThread dest;
asUser dest $ zipWithM_x setRegister
[badgeRegister, msgInfoRegister]
[capEPBadge epCap, wordFromMessageInfo (mi\<lparr> msgCapsUnwrapped := 0 \<rparr>)];
stateAssert kernelExitAssertions []
od
odE <catch> (\<lambda>_. callKernel (SyscallEvent sysc))
| SysReplyRecv \<Rightarrow> doE
curThread \<leftarrow> liftE $ getCurThread;
mi \<leftarrow> liftE $ getMessageInfo curThread;
cptr \<leftarrow> liftE $ asUser curThread $ getRegister capRegister;
fault \<leftarrow> liftE $ threadGet tcbFault curThread;
pickFastpath \<leftarrow> liftE $ alternative (return True) (return False);
unlessE (fault = None \<and> msgExtraCaps mi = 0
\<and> msgLength mi \<le> of_nat size_msgRegisters \<and> pickFastpath)
$ throwError ();
ctab \<leftarrow> liftE $ getThreadCSpaceRoot curThread >>= getCTE;
epCap \<leftarrow> unifyFailure (doE t \<leftarrow> resolveAddressBits (cteCap ctab) cptr (size cptr);
liftE (getSlotCap (fst t)) odE);
unlessE (isEndpointCap epCap \<and> capEPCanReceive epCap)
$ throwError ();
bound_ntfn \<leftarrow> liftE $ getBoundNotification curThread;
active_ntfn \<leftarrow> liftE $ case bound_ntfn of None \<Rightarrow> return False
| Some ntfnptr \<Rightarrow> liftM isActive $ getNotification ntfnptr;
unlessE (\<not> active_ntfn) $ throwError ();
ep \<leftarrow> liftE $ getEndpoint (capEPPtr epCap);
unlessE (\<not> isSendEP ep) $ throwError ();
callerSlot \<leftarrow> liftE $ getThreadCallerSlot curThread;
callerCTE \<leftarrow> liftE $ getCTE callerSlot;
callerCap \<leftarrow> returnOk $ cteCap callerCTE;
unlessE (isReplyCap callerCap \<and> \<not> capReplyMaster callerCap)
$ throwError ();
caller \<leftarrow> returnOk $ capTCBPtr callerCap;
callerFault \<leftarrow> liftE $ threadGet tcbFault caller;
unlessE (callerFault = None) $ throwError ();
newVTable \<leftarrow> liftE $ getThreadVSpaceRoot caller >>= getCTE;
unlessE (isValidVTableRoot $ cteCap newVTable) $ throwError ();
curDom \<leftarrow> liftE $ curDomain;
callerPrio \<leftarrow> liftE $ threadGet tcbPriority caller;
highest \<leftarrow> liftE $ isHighestPrio curDom callerPrio;
unlessE highest $ throwError ();
pd \<leftarrow> returnOk $ capPDBasePtr $ capCap $ cteCap newVTable;
asidMap \<leftarrow> liftE $ gets $ armKSASIDMap o ksArchState;
unlessE (\<exists>v. {hwasid. (hwasid, pd) \<in> ran asidMap} = {v})
$ throwError ();
callerDom \<leftarrow> liftE $ threadGet tcbDomain caller;
unlessE (callerDom = curDom) $ throwError ();
liftE $ do
epCanGrant \<leftarrow> return $ capEPCanGrant epCap;
threadSet (tcbState_update (\<lambda>_. BlockedOnReceive (capEPPtr epCap) epCanGrant)) curThread;
setEndpoint (capEPPtr epCap)
(case ep of IdleEP \<Rightarrow> RecvEP [curThread] | RecvEP ts \<Rightarrow> RecvEP (ts @ [curThread]));
mdbPrev \<leftarrow> liftM (mdbPrev o cteMDBNode) $ getCTE callerSlot;
assert (mdbPrev \<noteq> 0);
updateMDB mdbPrev (mdbNext_update (K 0) o mdbFirstBadged_update (K True)
o mdbRevocable_update (K True));
setCTE callerSlot makeObject;
forM_x (take (unat (msgLength mi)) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser curThread (getRegister r);
asUser caller (setRegister r v) od);
setThreadState Running caller;
Arch.switchToThread caller;
setCurThread caller;
asUser caller $ zipWithM_x setRegister
[badgeRegister, msgInfoRegister]
[0, wordFromMessageInfo (mi\<lparr> msgCapsUnwrapped := 0 \<rparr>)];
stateAssert kernelExitAssertions []
od
odE <catch> (\<lambda>_. callKernel (SyscallEvent sysc))
| _ \<Rightarrow> callKernel (SyscallEvent sysc)"
end
end

1908
proof/crefine/ARM_HYP/Fastpath_Equiv.thy Normal file
View File

File diff suppressed because it is too large Load Diff

5
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -13,11 +13,6 @@ begin
declare if_split [split del]
lemma empty_fail_getEndpoint:
"empty_fail (getEndpoint ep)"
unfolding getEndpoint_def
by (auto intro: empty_fail_getObject)
definition
"option_map2 f m = option_map f \<circ> m"

7
proof/crefine/ARM_HYP/IpcCancel_C.thy
View File

@ -2685,13 +2685,6 @@ lemma cancelSignal_ccorres [corres]:
| clarsimp simp: eq_commute
| drule_tac x=thread in bspec)+
lemma ko_at_valid_ep':
"\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
apply (erule obj_atE')
apply (erule (1) valid_objsE')
apply (simp add: projectKOs valid_obj'_def)
done
lemma cmap_relation_ep:
"(s, s') \<in> rf_sr \<Longrightarrow>
cmap_relation (map_to_eps (ksPSpace s)) (cslift s') Ptr (cendpoint_relation (cslift s'))"

7
proof/crefine/ARM_HYP/Ipc_C.thy
View File

@ -1535,13 +1535,6 @@ lemma ccorres_add_getRegister:
apply fastforce
done
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma exceptionMessage_ccorres:
"n < unat n_exceptionMessage
\<Longrightarrow> register_from_H (ARM_HYP_H.exceptionMessage ! n)

66
proof/crefine/ARM_HYP/IsolatedThreadAction.thy
View File

@ -5,7 +5,7 @@
*)
theory IsolatedThreadAction
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
imports ArchMove_C
begin
datatype tcb_state_regs = TCBStateRegs "thread_state" "MachineTypes.register \<Rightarrow> machine_word"
@ -117,10 +117,26 @@ lemmas setEndpoint_obj_at_tcb' = setEndpoint_obj_at'_tcb
lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
context kernel_m begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
(1 :: word32) < 2 ^ objBits v \<rbrakk>
\<Longrightarrow> setObject p v s
= modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s"
apply (clarsimp simp: setObject_def split_def exec_gets
obj_at'_def projectKOs lookupAround2_known1
assert_opt_def updateObject_default_def
bind_assoc)
apply (simp add: projectKO_def alignCheck_assert)
apply (simp add: project_inject objBits_def)
apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO)
apply (frule(2) in_magnitude_check[where s'=s])
apply (simp add: magnitudeCheck_assert in_monad)
apply (simp add: simpler_modify_def)
done
lemma getObject_return:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d;
@ -214,6 +230,8 @@ lemma isolate_thread_actions_asUser:
apply (case_tac ko, simp)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma getRegister_simple:
"getRegister r = (\<lambda>con. ({(con r, con)}, False))"
by (simp add: getRegister_def simpler_gets_def)
@ -253,6 +271,7 @@ lemma map_to_ctes_partial_overwrite:
"\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
map_to_ctes (partial_overwrite idx tsrs (ksPSpace s))
= ctes_of s"
supply if_split[split del]
apply (rule ext)
apply (frule dom_partial_overwrite[where tsrs=tsrs])
apply (simp add: map_to_ctes_def partial_overwrite_def
@ -571,6 +590,7 @@ lemma page_directory_at_partial_overwrite:
lemma findPDForASID_isolatable:
"thread_actions_isolatable idx (findPDForASID asid)"
supply if_split[split del]
apply (simp add: findPDForASID_def liftE_bindE liftME_def bindE_assoc
case_option_If2 assertE_def liftE_def checkPDAt_def
stateAssert_def2
@ -767,6 +787,7 @@ lemma restoreVirtTimer_isolatable:
lemma vcpuSave_isolatable:
"thread_actions_isolatable idx (vcpuSave v)"
supply if_split[split del]
apply (clarsimp simp: vcpuSave_def armvVCPUSave_def thread_actions_isolatable_fail when_def
split: option.splits)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -834,6 +855,7 @@ lemma liftM_getObject_return_tcb:
lemma threadGet_vcpu_isolatable:
"thread_actions_isolatable idx (threadGet (atcbVCPUPtr o tcbArch) t)"
supply if_split[split del]
apply (clarsimp simp: threadGet_def thread_actions_isolatable_def)
apply (clarsimp simp: isolate_thread_actions_def)
apply (clarsimp simp: monadic_rewrite_def)
@ -875,6 +897,7 @@ lemma getTCB_threadGet:
lemma setVMRoot_isolatable:
"thread_actions_isolatable idx (setVMRoot t)"
supply if_split[split del]
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def locateSlot_conv getSlotCap_def
cap_case_isPageDirectoryCap if_bool_simps whenE_def liftE_def
checkPDNotInASIDMap_def stateAssert_def2
@ -930,23 +953,16 @@ lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>
lemmas empty_fail_user_getreg = empty_fail_asUser[OF empty_fail_getRegister]
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma copyMRs_simple:
"msglen \<le> of_nat (length ARM_HYP_H.msgRegisters) \<longrightarrow>
"msglen \<le> of_nat (length msgRegisters) \<longrightarrow>
copyMRs sender sbuf receiver rbuf msglen
= forM_x (take (unat msglen) ARM_HYP_H.msgRegisters)
= forM_x (take (unat msglen) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser receiver (setRegister r v) od)
>>= (\<lambda>rv. return msglen)"
apply (clarsimp simp: copyMRs_def mapM_discarded)
apply (rule bind_cong[OF refl])
apply (simp add: length_msgRegisters n_msgRegisters_def min_def
apply (simp add: length_msgRegisters min_def
word_le_nat_alt
split: option.split)
apply (simp add: upto_enum_def mapM_Nil)
@ -956,16 +972,16 @@ lemma doIPCTransfer_simple_rewrite:
"monadic_rewrite True True
((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0
\<and> msgLength (messageInfoFromWord msgInfo)
\<le> of_nat (length ARM_HYP_H.msgRegisters))
\<le> of_nat (length msgRegisters))
and obj_at' (\<lambda>tcb. tcbFault tcb = None
\<and> (atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender)
(doIPCTransfer sender ep badge grant rcvr)
(do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od)
(take (unat (msgLength (messageInfoFromWord msgInfo))) ARM_HYP_H.msgRegisters);
(take (unat (msgLength (messageInfoFromWord msgInfo))) msgRegisters);
y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
asUser rcvr (setRegister ARM_HYP_H.badgeRegister badge)
asUser rcvr (setRegister badgeRegister badge)
od)"
supply if_cong[cong]
apply (rule monadic_rewrite_gen_asm)
@ -1153,7 +1169,7 @@ lemma oblivious_vcpuSwitch_schact:
lemma oblivious_switchToThread_schact:
"oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)"
apply (simp add: Thread_H.switchToThread_def ARM_HYP_H.switchToThread_def bind_assoc
apply (simp add: Thread_H.switchToThread_def switchToThread_def bind_assoc
getCurThread_def setCurThread_def threadGet_def liftM_def
threadSet_def tcbSchedEnqueue_def unless_when asUser_def
getQueue_def setQueue_def storeWordUser_def setRegister_def
@ -1210,8 +1226,6 @@ crunch obj_at_prio[wp]: cteDeleteOne "obj_at' (\<lambda>tcb. P (tcbPriority tcb)
setThreadState_obj_at_unchanged setNotification_tcb setBoundNotification_obj_at_unchanged
simp: crunch_simps unless_def)
context kernel_m begin
lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
@ -1243,6 +1257,8 @@ lemma bind_assoc:
= do x \<leftarrow> m; y \<leftarrow> f x; g y od"
by (rule bind_assoc)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>
\<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
@ -1267,6 +1283,7 @@ lemma setObject_modify_assert:
lemma setEndpoint_isolatable:
"thread_actions_isolatable idx (setEndpoint p e)"
supply if_split[split del]
apply (simp add: setEndpoint_def setObject_modify_assert
assert_def)
apply (case_tac "p \<in> range idx")
@ -1360,6 +1377,7 @@ lemma partial_overwrite_fun_upd2:
lemma setCTE_isolatable:
"thread_actions_isolatable idx (setCTE p v)"
supply if_split[split del]
apply (simp add: setCTE_assert_modify)
apply (clarsimp simp: thread_actions_isolatable_def
monadic_rewrite_def fun_eq_iff
@ -1422,7 +1440,7 @@ lemma assert_isolatable:
lemma cteInsert_isolatable:
"thread_actions_isolatable idx (cteInsert cap src dest)"
supply if_cong[cong]
supply if_split[split del] if_cong[cong]
apply (simp add: cteInsert_def updateCap_def updateMDB_def
Let_def setUntypedCapAsFull_def)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -1522,7 +1540,7 @@ lemma threadGet_isolatable:
lemma switchToThread_isolatable:
"thread_actions_isolatable idx (Arch.switchToThread t)"
apply (simp add: ARM_HYP_H.switchToThread_def getTCB_threadGet
apply (simp add: switchToThread_def getTCB_threadGet
storeWordUser_def stateAssert_def2)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
gets_isolatable setVMRoot_isolatable
@ -1596,7 +1614,7 @@ lemma tcb_at_KOTCB_upd:
= tcb_at' p s"
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
split: if_split)
apply (simp add: ps_clear_def)
apply (fastforce simp add: ps_clear_def)
done
definition
@ -1643,6 +1661,7 @@ lemma copy_register_isolate:
asUser dest (setRegister r' (rf v)) od)
(isolate_thread_actions idx (return ())
(copy_register_tsrs x y r r' rf) id)"
supply if_split[split del]
apply (simp add: asUser_def split_def bind_assoc
getRegister_def setRegister_def
select_f_returns isolate_thread_actions_def
@ -1791,7 +1810,7 @@ lemmas fastpath_isolate_rewrites
lemma lookupIPCBuffer_isolatable:
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
supply if_cong[cong]
supply if_split[split del] if_cong[cong]
apply (simp add: lookupIPCBuffer_def)
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
@ -1811,6 +1830,7 @@ lemma setThreadState_rewrite_simple:
(\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s)
(setThreadState st t)
(threadSet (tcbState_update (\<lambda>_. st)) t)"
supply if_split[split del]
apply (simp add: setThreadState_def)
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans)

7
proof/crefine/ARM_HYP/PSpace_C.thy
View File

@ -10,13 +10,6 @@ begin
context kernel begin
lemma koTypeOf_injectKO:
fixes v :: "'a :: pspace_storable" shows
"koTypeOf (injectKO v) = koType TYPE('a)"
apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
apply (simp add: project_koType[symmetric])
done
lemma setObject_obj_at_pre:
"\<lbrakk> updateObject ko = updateObject_default ko;
(1 :: word32) < 2 ^ objBits ko \<rbrakk>

10
proof/crefine/ARM_HYP/Refine_C.thy
View File

@ -7,7 +7,7 @@
chapter "Toplevel Refinement Statement"
theory Refine_C
imports Init_C Fastpath_C CToCRefine
imports Init_C Fastpath_Equiv Fastpath_C CToCRefine
begin
context begin interpretation Arch . (*FIXME: arch_split*)
@ -18,6 +18,14 @@ end
context kernel_m
begin
text \<open>Assemble fastpaths\<close>
lemmas fastpath_call_ccorres_callKernel
= monadic_rewrite_ccorres_assemble[OF fastpath_call_ccorres fastpath_callKernel_SysCall_corres]
lemmas fastpath_reply_recv_ccorres_callKernel
= monadic_rewrite_ccorres_assemble[OF fastpath_reply_recv_ccorres fastpath_callKernel_SysReplyRecv_corres]
declare liftE_handle [simp]
lemma schedule_sch_act_wf:

5
proof/crefine/ARM_HYP/Retype_C.thy
View File

@ -7836,11 +7836,6 @@ end
context begin interpretation Arch . (*FIXME: arch_split*)
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps)
lemma createNewCaps_1_gsCNodes_p:
"\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>"
apply (simp add: createNewCaps_def)

65
proof/crefine/ARM_HYP/SR_lemmas_C.thy
View File

@ -310,67 +310,6 @@ lemma cmdbnode_relation_mdb_node_to_H [simp]:
unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def
by (fastforce split: option.splits)
(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*)
lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs[simp]
from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ tcbBlockSizeBits"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)
hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
thus ?thesis using yq by simp
qed
lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs[simp]
from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
apply (rule is_aligned_no_overflow' [OF al])
done
thus ?thesis using yq by (simp add: field_simps)
qed
lemmas tcbSlots =
tcbCTableSlot_def tcbVTableSlot_def
tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
lemma updateObject_cte_tcb:
assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
shows "updateObject ctea (KOTCB tcb) ptr ptr' next =
(do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
definition
tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> word32 \<times> word32 \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> word32 option"
where
@ -705,10 +644,6 @@ proof -
qed fact+
qed
lemma ctes_of_cte_at:
"ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
by (simp add: cte_wp_at_ctes_of)
lemma cor_map_relI:
assumes dm: "dom am = dom am'"
and rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';

11
proof/crefine/ARM_HYP/Tcb_C.thy
View File

@ -8,17 +8,6 @@ theory Tcb_C
imports Delete_C Ipc_C
begin
lemma asUser_obj_at' :
"\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
including no_pre
apply (simp add: asUser_def)
apply wp
apply (case_tac "t=t'"; clarsimp)
apply (rule hoare_drop_imps)
apply wp
done
lemma getObject_sched:
"(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
(x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"

12
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -865,18 +865,6 @@ lemma lookupPTSlot_ccorres:
split: ARM_HYP_H.pde.split_asm)
done
lemma cap_case_isPageDirectoryCap:
"(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid
| _ => g)
= (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
(* FIXME: MOVE to CSpaceAcc_C *)
lemma ccorres_pre_gets_armKSASIDTable_ksArchState:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"

152
proof/crefine/Move_C.thy
View File

@ -8,7 +8,7 @@
(* Arch generic lemmas that should be moved into theory files before CRefine *)
theory Move_C
imports CBaseRefine.Include_C
imports Refine.Refine
begin
lemma dumb_bool_for_all: "(\<forall>x. x) = False"
@ -414,15 +414,6 @@ lemma reset_name_seq_bound_helper:
apply simp
done
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
(* FIXME move to lib/Eisbach_Methods *)
(* FIXME consider printing error on solve goal apply *)
context
@ -470,14 +461,15 @@ lemma word_minus_1_shiftr:
apply (simp only: uint_word_ariths uint_div uint_power_lower)
apply (subst mod_pos_pos_trivial, fastforce, fastforce)+
apply (subst mod_pos_pos_trivial)
apply (simp add: word_less_def)
apply (simp add: word_less_def word_le_def)
apply (subst uint_1[symmetric])
apply (fastforce intro: uint_sub_lt2p)
apply (subst int_div_sub_1, fastforce)
apply (clarsimp simp: and_mask_dvd low_bits_zero)
apply (subst mod_pos_pos_trivial)
apply (metis le_step_down_int mult_zero_left shiftr_div_2n shiftr_div_2n_w uint_0_iff
uint_nonnegative word_not_simps(1))
apply (simp add: word_le_def)
apply (metis mult_zero_left neq_zero div_positive_int linorder_not_le uint_2p_alt word_div_lt_eq_0
word_less_def zless2p)
apply (metis shiftr_div_2n uint_1 uint_sub_lt2p)
apply fastforce
done
@ -1351,4 +1343,138 @@ begin
declare less_Suc0[iff del]
end
lemma koTypeOf_injectKO:
fixes v :: "'a :: pspace_storable" shows
"koTypeOf (injectKO v) = koType TYPE('a)"
apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
apply (simp add: project_koType[symmetric])
done
lemma ctes_of_cte_at:
"ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
by (simp add: cte_wp_at_ctes_of)
lemmas tcbSlots =
tcbCTableSlot_def tcbVTableSlot_def
tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
lemma updateObject_cte_tcb:
assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
shows "updateObject ctea (KOTCB tcb) ptr ptr' next =
(do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ tcbBlockSizeBits"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)
hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
thus ?thesis using yq by simp
qed
lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
apply (rule is_aligned_no_overflow' [OF al])
done
thus ?thesis using yq by (simp add: field_simps)
qed
lemma valid_cap_cte_at':
"\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk>
\<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'"
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (rule real_cte_at')
apply (erule spec)
done
lemma cd_wp[wp]:
"\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma empty_fail_getEndpoint:
"empty_fail (getEndpoint ep)"
unfolding getEndpoint_def
by (auto intro: empty_fail_getObject)
lemma ko_at_valid_ep':
"\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
apply (erule obj_atE')
apply (erule (1) valid_objsE')
apply (simp add: projectKOs valid_obj'_def)
done
lemma cap_case_EndpointCap_NotificationCap:
"(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
| NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3
| _ \<Rightarrow> h)
= (if isEndpointCap cap
then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
(capEPCanGrant cap) (capEPCanGrantReply cap)
else if isNotificationCap cap
then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
else h)"
by (simp add: isCap_simps
split: capability.split split del: if_split)
lemma asUser_obj_at':
"\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
including no_pre
apply (simp add: asUser_def)
apply wpsimp
apply (case_tac "t=t'"; clarsimp)
apply (rule hoare_drop_imps)
apply wp
done
(* FIXME: partial copy from SR_Lemmas since only map_to_ctes is defined.
All of the update_*_map_tos in SR_lemmas can be moved up. *)
lemma update_ep_map_to_ctes:
fixes P :: "endpoint \<Rightarrow> bool"
assumes at: "obj_at' P p s"
shows "map_to_ctes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ctes (ksPSpace s)"
using at
by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI
simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)
(* FIXME: move to MonadicRewrite *)
lemma monadic_rewrite_gets_l:
"(\<And>x. monadic_rewrite F E (P x) (g x) m)
\<Longrightarrow> monadic_rewrite F E (\<lambda>s. P (f s) s) (gets f >>= (\<lambda>x. g x)) m"
by (auto simp add: monadic_rewrite_def exec_gets)
end

67
proof/crefine/RISCV64/ArchMove_C.thy
View File

@ -358,6 +358,73 @@ lemma getActiveIRQ_neq_Some0x3FF:
apply (auto dest: use_valid intro: getActiveIRQ_neq_Some0x3FF')
done
(* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should
be equivalent to what we have in the abstract/design specs. We want a number for this definition
that automatically updates if the number of registers changes, and we sanity check it later
in msgRegisters_size_sanity *)
definition size_msgRegisters :: nat where
size_msgRegisters_pre_def: "size_msgRegisters \<equiv> size (RISCV64.msgRegisters)"
schematic_goal size_msgRegisters_def:
"size_msgRegisters = numeral ?x"
unfolding size_msgRegisters_pre_def RISCV64.msgRegisters_def
by (simp add: upto_enum_red fromEnum_def enum_register del: Suc_eq_numeral)
(simp only: Suc_eq_plus1_left, simp del: One_nat_def)
lemma length_msgRegisters[simplified size_msgRegisters_def]:
"length RISCV64_H.msgRegisters = size_msgRegisters"
by (simp add: size_msgRegisters_pre_def RISCV64_H.msgRegisters_def)
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace>
asUser t (getRegister r)
\<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def getRegister_def in_monad atcbContextGet_def)
done
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, setThreadState,
updateFreeIndex, preemptionPoint
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps
ignore_del: preemptionPoint)
end
end

43
proof/crefine/RISCV64/CLevityCatch.thy
View File

@ -61,14 +61,6 @@ lemma no_overlap_new_cap_addrs_disjoint:
apply auto
done
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord)
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getExtraCPtrs [intro!, simp]:
"empty_fail (getExtraCPtrs sendBuffer info)"
apply (simp add: getExtraCPtrs_def)
@ -115,32 +107,6 @@ lemma asUser_get_registers:
obj_at'_def)
done
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma exec_Basic_Guard_UNIV:
"Semantic.exec \<Gamma> (Basic f;; Guard F UNIV (Basic g)) x y =
Semantic.exec \<Gamma> (Basic (g o f)) x y"
@ -172,4 +138,13 @@ lemma option_to_ptr_not_0:
"\<lbrakk> p \<noteq> 0 ; option_to_ptr v = Ptr p \<rbrakk> \<Longrightarrow> v = Some p"
by (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
end

4
proof/crefine/RISCV64/CSpaceAcc_C.thy
View File

@ -188,10 +188,6 @@ lemma ccorres_pre_getIdleThread:
apply (clarsimp simp: rf_sr_ksIdleThread)
done
lemma cd_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma curDomain_sp:
"\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>"
apply wp

7
proof/crefine/RISCV64/CSpace_RAB_C.thy
View File

@ -92,13 +92,6 @@ lemma ccorres_req:
apply (clarsimp elim!: bexI [rotated])
done
lemma valid_cap_cte_at':
"\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'"
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (rule real_cte_at')
apply (erule spec)
done
declare mask_64_max_word [simp]
lemma rightsFromWord_wordFromRights:

5
proof/crefine/RISCV64/Finalise_C.thy
View File

@ -31,11 +31,6 @@ lemma ccorres_dc_comp:
declare if_split [split del]
lemma empty_fail_getEndpoint:
"empty_fail (getEndpoint ep)"
unfolding getEndpoint_def
by (auto intro: empty_fail_getObject)
definition
"option_map2 f m = option_map f \<circ> m"

6
proof/crefine/RISCV64/Invoke_C.thy
View File

@ -1413,12 +1413,6 @@ crunch sch_act_wf[wp]: insertNewCap "\<lambda>s. sch_act_wf (ksSchedulerAction s
crunch ksCurThread[wp]: deleteObjects "\<lambda>s. P (ksCurThread s)"
(wp: crunch_wps simp: unless_def)
(* FIXME RAF move to Retype_C to extend original *)
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, doMachineOp
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps)
lemma deleteObjects_gsCNodes_at_pt:
"\<lbrace>(\<lambda>s. P (gsCNodes s ptr))
and K (ptr \<notin> {ptr_base .. ptr_base + 2 ^ sz - 1} \<and> is_aligned ptr_base sz)\<rbrace>

7
proof/crefine/RISCV64/IpcCancel_C.thy
View File

@ -2642,13 +2642,6 @@ lemma cancelSignal_ccorres [corres]:
| clarsimp simp: eq_commute
| drule_tac x=thread in bspec)+
lemma ko_at_valid_ep':
"\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
apply (erule obj_atE')
apply (erule (1) valid_objsE')
apply (simp add: projectKOs valid_obj'_def)
done
(* FIXME: MOVE *)
lemma ccorres_pre_getEndpoint [corres_pre]:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"

7
proof/crefine/RISCV64/Ipc_C.thy
View File

@ -1459,13 +1459,6 @@ lemma ccorres_add_getRegister:
apply fastforce
done
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma exceptionMessage_ccorres:
"n < unat n_exceptionMessage
\<Longrightarrow> register_from_H (RISCV64_H.exceptionMessage ! n)

67
proof/crefine/RISCV64/IsolatedThreadAction.thy
View File

@ -6,7 +6,7 @@
*)
theory IsolatedThreadAction
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
imports ArchMove_C
begin
context begin interpretation Arch .
@ -128,10 +128,24 @@ lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
end
context kernel_m begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
(1 :: machine_word) < 2 ^ objBits v \<rbrakk>
\<Longrightarrow> setObject p v s
= modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s"
apply (clarsimp simp: setObject_def split_def exec_gets obj_at'_def lookupAround2_known1
assert_opt_def updateObject_default_def bind_assoc)
apply (simp add: projectKO_def alignCheck_assert)
apply (simp add: project_inject objBits_def)
apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO)
apply (frule(2) in_magnitude_check[where s'=s])
apply (simp add: magnitudeCheck_assert in_monad)
apply (simp add: simpler_modify_def)
done
lemma getObject_return:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d;
@ -163,6 +177,8 @@ lemma partial_overwrite_fun_upd:
apply (clarsimp split: if_split)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma get_tcb_state_regs_ko_at':
"ko_at' ko p s \<Longrightarrow> get_tcb_state_regs (ksPSpace s p)
= TCBStateRegs (tcbState ko) ((user_regs o atcbContextGet o tcbArch) ko)"
@ -266,6 +282,7 @@ lemma map_to_ctes_partial_overwrite:
"\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
map_to_ctes (partial_overwrite idx tsrs (ksPSpace s))
= ctes_of s"
supply if_split[split del]
apply (rule ext)
apply (frule dom_partial_overwrite[where tsrs=tsrs])
apply (simp add: map_to_ctes_def partial_overwrite_def
@ -615,6 +632,7 @@ lemma page_table_at_partial_overwrite:
lemma findVSpaceForASID_isolatable:
"thread_actions_isolatable idx (findVSpaceForASID asid)"
supply if_split[split del]
apply (simp add: findVSpaceForASID_def liftE_bindE liftME_def bindE_assoc
case_option_If2 assertE_def liftE_def checkPTAt_def
stateAssert_def2
@ -678,6 +696,7 @@ lemma cap_case_isPageTableCap:
lemma setVMRoot_isolatable:
"thread_actions_isolatable idx (setVMRoot t)"
supply if_split[split del]
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def
locateSlot_conv getSlotCap_def
if_bool_simps cap_case_isPageTableCap
@ -702,7 +721,10 @@ lemma transferCaps_simple:
return (mi\<lparr>msgExtraCaps := 0, msgCapsUnwrapped := 0\<rparr>)
od"
apply (cases mi)
apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv cong: option.case_cong)
apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv)
apply (rule ext bind_apply_cong[OF refl])+
apply (simp add: upto_enum_def
split: option.split)
done
lemma transferCaps_simple_rewrite:
@ -731,23 +753,16 @@ lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>
lemmas empty_fail_user_getreg = empty_fail_asUser[OF empty_fail_getRegister]
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma copyMRs_simple:
"msglen \<le> of_nat (length RISCV64_H.msgRegisters) \<longrightarrow>
"msglen \<le> of_nat (length msgRegisters) \<longrightarrow>
copyMRs sender sbuf receiver rbuf msglen
= forM_x (take (unat msglen) RISCV64_H.msgRegisters)
= forM_x (take (unat msglen) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser receiver (setRegister r v) od)
>>= (\<lambda>rv. return msglen)"
apply (clarsimp simp: copyMRs_def mapM_discarded)
apply (rule bind_cong[OF refl])
apply (simp add: length_msgRegisters n_msgRegisters_def min_def
apply (simp add: length_msgRegisters min_def
word_le_nat_alt
split: option.split)
apply (simp add: upto_enum_def mapM_Nil)
@ -757,16 +772,16 @@ lemma doIPCTransfer_simple_rewrite:
"monadic_rewrite True True
((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0
\<and> msgLength (messageInfoFromWord msgInfo)
\<le> of_nat (length RISCV64_H.msgRegisters))
\<le> of_nat (length msgRegisters))
and obj_at' (\<lambda>tcb. tcbFault tcb = None
\<and> (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender)
(doIPCTransfer sender ep badge grant rcvr)
(do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od)
(take (unat (msgLength (messageInfoFromWord msgInfo))) RISCV64_H.msgRegisters);
(take (unat (msgLength (messageInfoFromWord msgInfo))) msgRegisters);
y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
asUser rcvr (setRegister RISCV64_H.badgeRegister badge)
asUser rcvr (setRegister badgeRegister badge)
od)"
supply if_cong[cong]
apply (rule monadic_rewrite_gen_asm)
@ -916,7 +931,7 @@ lemma oblivious_setVMRoot_schact:
lemma oblivious_switchToThread_schact:
"oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)"
apply (simp add: Thread_H.switchToThread_def RISCV64_H.switchToThread_def bind_assoc
apply (simp add: Thread_H.switchToThread_def switchToThread_def bind_assoc
getCurThread_def setCurThread_def threadGet_def liftM_def
threadSet_def tcbSchedEnqueue_def unless_when asUser_def
getQueue_def setQueue_def storeWordUser_def setRegister_def
@ -972,8 +987,6 @@ crunch obj_at_prio[wp]: cteDeleteOne "obj_at' (\<lambda>tcb. P (tcbPriority tcb)
setThreadState_obj_at_unchanged setNotification_tcb setBoundNotification_obj_at_unchanged
simp: crunch_simps unless_def)
context kernel_m begin
lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
@ -1005,6 +1018,8 @@ lemma bind_assoc:
= do x \<leftarrow> m; y \<leftarrow> f x; g y od"
by (rule bind_assoc)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>
\<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
@ -1029,6 +1044,7 @@ lemma setObject_modify_assert:
lemma setEndpoint_isolatable:
"thread_actions_isolatable idx (setEndpoint p e)"
supply if_split[split del]
apply (simp add: setEndpoint_def setObject_modify_assert
assert_def)
apply (case_tac "p \<in> range idx")
@ -1127,6 +1143,7 @@ lemma atcbContextSetSetGet_eq[simp]:
lemma setCTE_isolatable:
"thread_actions_isolatable idx (setCTE p v)"
supply if_split[split del]
apply (simp add: setCTE_assert_modify)
apply (clarsimp simp: thread_actions_isolatable_def
monadic_rewrite_def fun_eq_iff
@ -1189,7 +1206,7 @@ lemma assert_isolatable:
lemma cteInsert_isolatable:
"thread_actions_isolatable idx (cteInsert cap src dest)"
supply if_cong[cong]
supply if_split[split del] if_cong[cong]
apply (simp add: cteInsert_def updateCap_def updateMDB_def
Let_def setUntypedCapAsFull_def)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
@ -1289,7 +1306,7 @@ lemma threadGet_isolatable:
lemma switchToThread_isolatable:
"thread_actions_isolatable idx (Arch.switchToThread t)"
apply (simp add: RISCV64_H.switchToThread_def
apply (simp add: switchToThread_def
storeWordUser_def stateAssert_def2)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
gets_isolatable setVMRoot_isolatable
@ -1359,7 +1376,7 @@ lemma tcb_at_KOTCB_upd:
= tcb_at' p s"
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
split: if_split)
apply (simp add: ps_clear_def)
apply (fastforce simp add: ps_clear_def)
done
definition
@ -1407,6 +1424,7 @@ lemma copy_register_isolate:
asUser dest (setRegister r' (rf v)) od)
(isolate_thread_actions idx (return ())
(copy_register_tsrs x y r r' rf) id)"
supply if_split[split del]
apply (simp add: asUser_def split_def bind_assoc
getRegister_def setRegister_def
select_f_returns isolate_thread_actions_def
@ -1556,7 +1574,7 @@ lemmas fastpath_isolate_rewrites
lemma lookupIPCBuffer_isolatable:
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
supply if_cong[cong]
supply if_cong[cong] if_split[split del]
apply (simp add: lookupIPCBuffer_def)
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
@ -1577,6 +1595,7 @@ lemma setThreadState_rewrite_simple:
(\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s)
(setThreadState st t)
(threadSet (tcbState_update (\<lambda>_. st)) t)"
supply if_split[split del]
apply (simp add: setThreadState_def)
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans)

7
proof/crefine/RISCV64/PSpace_C.thy
View File

@ -11,13 +11,6 @@ begin
context kernel begin
lemma koTypeOf_injectKO:
fixes v :: "'a :: pspace_storable" shows
"koTypeOf (injectKO v) = koType TYPE('a)"
apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
apply (simp add: project_koType[symmetric])
done
lemma setObject_obj_at_pre:
"\<lbrakk> updateObject ko = updateObject_default ko;
(1 :: machine_word) < 2 ^ objBits ko \<rbrakk>

5
proof/crefine/RISCV64/Retype_C.thy
View File

@ -6916,11 +6916,6 @@ end
context begin interpretation Arch . (*FIXME: arch_split*)
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps)
lemma createNewCaps_1_gsCNodes_p:
"\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>"
apply (simp add: createNewCaps_def)

65
proof/crefine/RISCV64/SR_lemmas_C.thy
View File

@ -288,67 +288,6 @@ lemma cmdbnode_relation_mdb_node_to_H [simp]:
unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def
by (fastforce split: option.splits)
(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*)
lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ 9"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)
hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
thus ?thesis using yq by simp
qed
lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
apply (rule is_aligned_no_overflow' [OF al])
done
thus ?thesis using yq by (simp add: field_simps)
qed
lemmas tcbSlots =
tcbCTableSlot_def tcbVTableSlot_def
tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
lemma updateObject_cte_tcb:
assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
shows "updateObject ctea (KOTCB tcb) ptr ptr' next =
(do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
definition
tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> machine_word \<times> machine_word \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option"
where
@ -658,10 +597,6 @@ proof -
qed fact+
qed
lemma ctes_of_cte_at:
"ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
by (simp add: cte_wp_at_ctes_of)
lemma cor_map_relI:
assumes dm: "dom am = dom am'"
and rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';

15
proof/crefine/RISCV64/Syscall_C.thy
View File

@ -1144,21 +1144,6 @@ lemma deleteCallerCap_ccorres [corres]:
tcb_aligned')
done
(* FIXME: MOVE *)
lemma cap_case_EndpointCap_NotificationCap:
"(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
| NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3
| _ \<Rightarrow> h)
= (if isEndpointCap cap
then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
(capEPCanGrant cap) (capEPCanGrantReply cap)
else if isNotificationCap cap
then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
else h)"
by (simp add: isCap_simps
split: capability.split)
(* FIXME: MOVE to Corres_C.thy *)
lemma ccorres_trim_redundant_throw_break:
"\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c;

5
proof/crefine/RISCV64/Tcb_C.thy
View File

@ -9,11 +9,6 @@ theory Tcb_C
imports Delete_C Ipc_C
begin
lemma asUser_obj_at' :
"\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
including no_pre
by (wpsimp wp: hoare_vcg_ball_lift threadGet_wp simp: split_def asUser_def)
lemma getObject_sched:
"(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
(x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"

16
proof/crefine/RISCV64/VSpace_C.thy
View File

@ -849,22 +849,6 @@ lemma ccorres_abstract_known:
apply simp
done
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
(1 :: machine_word) < 2 ^ objBits v \<rbrakk>
\<Longrightarrow> setObject p v s
= modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s"
apply (clarsimp simp: setObject_def split_def exec_gets obj_at'_def lookupAround2_known1
assert_opt_def updateObject_default_def bind_assoc)
apply (simp add: projectKO_def alignCheck_assert)
apply (simp add: project_inject objBits_def)
apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO)
apply (frule(2) in_magnitude_check[where s'=s])
apply (simp add: magnitudeCheck_assert in_monad)
apply (simp add: simpler_modify_def)
done
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g"

78
proof/crefine/X64/ArchMove_C.thy
View File

@ -454,6 +454,84 @@ lemma valid_untyped':
nat_le_linear power_overflow sub_wrap add_0
add_0_right word_add_increasing word_less_1 word_less_sub_1)
(* We don't have access to n_msgRegisters from C here, but the number of msg registers in C should
be equivalent to what we have in the abstract/design specs. We want a number for this definition
that automatically updates if the number of registers changes, and we sanity check it later
in msgRegisters_size_sanity *)
definition size_msgRegisters :: nat where
size_msgRegisters_pre_def: "size_msgRegisters \<equiv> size (X64.msgRegisters)"
schematic_goal size_msgRegisters_def:
"size_msgRegisters = numeral ?x"
unfolding size_msgRegisters_pre_def X64.msgRegisters_def
by (simp add: upto_enum_red fromEnum_def enum_register del: Suc_eq_numeral)
(simp only: Suc_eq_plus1_left, simp del: One_nat_def)
lemma length_msgRegisters[simplified size_msgRegisters_def]:
"length X64_H.msgRegisters = size_msgRegisters"
by (simp add: size_msgRegisters_pre_def X64_H.msgRegisters_def)
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord ef_dmo')
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace>
asUser t (getRegister r)
\<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def getRegister_def in_monad atcbContextGet_def)
done
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject, setThreadState,
updateFreeIndex, preemptionPoint
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps
ignore_del: preemptionPoint)
lemma cap_case_isPML4Cap:
"(case cap of ArchObjectCap (PML4Cap pm (Some asid)) \<Rightarrow> fn pm asid | _ => g)
= (if (if isArchObjectCap cap then if isPML4Cap (capCap cap) then capPML4MappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPML4BasePtr (capCap cap)) (the (capPML4MappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPML4Cap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
end
end

43
proof/crefine/X64/CLevityCatch.thy
View File

@ -51,14 +51,6 @@ lemma no_overlap_new_cap_addrs_disjoint:
declare empty_fail_doMachineOp [simp]
lemma empty_fail_loadWordUser[intro!, simp]:
"empty_fail (loadWordUser x)"
by (simp add: loadWordUser_def ef_loadWord)
lemma empty_fail_getMRs[iff]:
"empty_fail (getMRs t buf mi)"
by (auto simp add: getMRs_def split: option.split)
lemma empty_fail_getExtraCPtrs [intro!, simp]:
"empty_fail (getExtraCPtrs sendBuffer info)"
apply (simp add: getExtraCPtrs_def)
@ -80,33 +72,6 @@ lemma empty_fail_unifyFailure [intro!, simp]:
handleE'_def throwError_def
split: sum.splits)
lemma empty_fail_getReceiveSlots:
"empty_fail (getReceiveSlots r rbuf)"
proof -
note
empty_fail_assertE[iff]
empty_fail_resolveAddressBits[iff]
show ?thesis
apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def
split: option.split)
apply (rule empty_fail_bind)
apply (simp add: capTransferFromWords_def)
apply (simp add: emptyOnFailure_def unifyFailure_def)
apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure,
simp_all add: empty_fail_whenEs)
apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def
lookupSlotForThread_def liftME_def
getThreadCSpaceRoot_def locateSlot_conv bindE_assoc
lookupSlotForCNodeOp_def lookupErrorOnFailure_def
cong: if_cong)
apply (intro empty_fail_bindE,
simp_all add: getSlotCap_def)
apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI,
simp_all add: empty_fail_whenEs rangeCheck_def)
done
qed
lemma exec_Basic_Guard_UNIV:
"Semantic.exec \<Gamma> (Basic f;; Guard F UNIV (Basic g)) x y =
Semantic.exec \<Gamma> (Basic (g o f)) x y"
@ -138,4 +103,12 @@ lemma option_to_ptr_not_0:
"\<lbrakk> p \<noteq> 0 ; option_to_ptr v = Ptr p \<rbrakk> \<Longrightarrow> v = Some p"
by (clarsimp simp: option_to_ptr_def option_to_0_def split: option.splits)
schematic_goal sz8_helper:
"((-1) << 8 :: addr) = ?v"
by (simp add: shiftl_t2n)
lemmas reset_name_seq_bound_helper2
= reset_name_seq_bound_helper[where sz=8 and v="v :: addr" for v,
simplified sz8_helper word_bits_def[symmetric],
THEN name_seq_bound_helper]
end

6
proof/crefine/X64/CSpaceAcc_C.thy
View File

@ -187,15 +187,11 @@ lemma ccorres_pre_getIdleThread:
apply (clarsimp simp: rf_sr_ksIdleThread)
done
lemma cd_wp [wp]: "\<lbrace>\<lambda>s. P (ksCurDomain s) s\<rbrace> curDomain \<lbrace>P\<rbrace>"
by (unfold curDomain_def, wp)
lemma curDomain_sp:
"\<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. ksCurDomain s = rv \<and> P s\<rbrace>"
apply wp
apply simp
done
done
lemma rf_sr_ksCurDomain:
"(s, s') \<in> rf_sr \<Longrightarrow> ksCurDomain_' (globals s')

7
proof/crefine/X64/CSpace_RAB_C.thy
View File

@ -92,13 +92,6 @@ lemma ccorres_req:
apply (clarsimp elim!: bexI [rotated])
done
lemma valid_cap_cte_at':
"\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'"
apply (clarsimp simp: isCap_simps valid_cap'_def)
apply (rule real_cte_at')
apply (erule spec)
done
declare mask_64_max_word [simp]
lemma rightsFromWord_wordFromRights:

5
proof/crefine/X64/Finalise_C.thy
View File

@ -13,11 +13,6 @@ begin
declare if_split [split del]
lemma empty_fail_getEndpoint:
"empty_fail (getEndpoint ep)"
unfolding getEndpoint_def
by (auto intro: empty_fail_getObject)
definition
"option_map2 f m = option_map f \<circ> m"

7
proof/crefine/X64/IpcCancel_C.thy
View File

@ -2696,13 +2696,6 @@ lemma cancelSignal_ccorres [corres]:
| clarsimp simp: eq_commute
| drule_tac x=thread in bspec)+
lemma ko_at_valid_ep':
"\<lbrakk>ko_at' ep p s; valid_objs' s\<rbrakk> \<Longrightarrow> valid_ep' ep s"
apply (erule obj_atE')
apply (erule (1) valid_objsE')
apply (simp add: projectKOs valid_obj'_def)
done
(* FIXME: MOVE *)
lemma ccorres_pre_getEndpoint [corres_pre]:
assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"

7
proof/crefine/X64/Ipc_C.thy
View File

@ -1466,13 +1466,6 @@ lemma ccorres_add_getRegister:
apply fastforce
done
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma exceptionMessage_ccorres:
"n < unat n_exceptionMessage
\<Longrightarrow> register_from_H (X64_H.exceptionMessage ! n)

73
proof/crefine/X64/IsolatedThreadAction.thy
View File

@ -5,7 +5,7 @@
*)
theory IsolatedThreadAction
imports "CLib.MonadicRewrite_C" Finalise_C CSpace_All SyscallArgs_C
imports ArchMove_C
begin
context begin interpretation Arch .
@ -127,10 +127,26 @@ lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
end
context kernel_m begin
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
(1 :: machine_word) < 2 ^ objBits v \<rbrakk>
\<Longrightarrow> setObject p v s
= modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s"
apply (clarsimp simp: setObject_def split_def exec_gets
obj_at'_def projectKOs lookupAround2_known1
assert_opt_def updateObject_default_def
bind_assoc)
apply (simp add: projectKO_def alignCheck_assert)
apply (simp add: project_inject objBits_def)
apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO)
apply (frule(2) in_magnitude_check[where s'=s])
apply (simp add: magnitudeCheck_assert in_monad)
apply (simp add: simpler_modify_def)
done
lemma getObject_return:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> \<And>a b c d. (loadObject a b c d :: 'a kernel) = loadObject_default a b c d;
@ -162,6 +178,8 @@ lemma partial_overwrite_fun_upd:
apply (clarsimp split: if_split)
done
context begin interpretation Arch . (*FIXME: arch_split*)
lemma get_tcb_state_regs_ko_at':
"ko_at' ko p s \<Longrightarrow> get_tcb_state_regs (ksPSpace s p)
= TCBStateRegs (tcbState ko) ((user_regs o atcbContextGet o tcbArch) ko)"
@ -265,6 +283,7 @@ lemma map_to_ctes_partial_overwrite:
"\<forall>x. tcb_at' (idx x) s \<Longrightarrow>
map_to_ctes (partial_overwrite idx tsrs (ksPSpace s))
= ctes_of s"
supply if_split[split del]
apply (rule ext)
apply (frule dom_partial_overwrite[where tsrs=tsrs])
apply (simp add: map_to_ctes_def partial_overwrite_def
@ -614,6 +633,7 @@ lemma page_map_l4_at_partial_overwrite:
lemma findVSpaceForASID_isolatable:
"thread_actions_isolatable idx (findVSpaceForASID asid)"
supply if_split[split del]
apply (simp add: findVSpaceForASID_def liftE_bindE liftME_def bindE_assoc
case_option_If2 assertE_def liftE_def checkPML4At_def
stateAssert_def2
@ -680,6 +700,7 @@ lemma setCurrentUserVSpaceRoot_isolatable:
lemma setVMRoot_isolatable:
"thread_actions_isolatable idx (setVMRoot t)"
supply if_split[split del]
apply (simp add: setVMRoot_def getThreadVSpaceRoot_def
locateSlot_conv getSlotCap_def
cap_case_isPML4Cap if_bool_simps
@ -706,8 +727,11 @@ lemma transferCaps_simple:
return (mi\<lparr>msgExtraCaps := 0, msgCapsUnwrapped := 0\<rparr>)
od"
apply (cases mi)
apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv
cong: option.case_cong)
apply (cases mi)
apply (clarsimp simp: transferCaps_def getThreadCSpaceRoot_def locateSlot_conv)
apply (rule ext bind_apply_cong[OF refl])+
apply (simp add: upto_enum_def
split: option.split)
done
lemma transferCaps_simple_rewrite:
@ -736,23 +760,16 @@ lemma lookupIPC_inv: "\<lbrace>P\<rbrace> lookupIPCBuffer f t \<lbrace>\<lambda>
lemmas empty_fail_user_getreg = empty_fail_asUser[OF empty_fail_getRegister]
lemma user_getreg_rv:
"\<lbrace>obj_at' (\<lambda>tcb. P ((user_regs o atcbContextGet o tcbArch) tcb r)) t\<rbrace> asUser t (getRegister r) \<lbrace>\<lambda>rv s. P rv\<rbrace>"
apply (simp add: asUser_def split_def)
apply (wp threadGet_wp)
apply (clarsimp simp: obj_at'_def projectKOs getRegister_def in_monad atcbContextGet_def)
done
lemma copyMRs_simple:
"msglen \<le> of_nat (length X64_H.msgRegisters) \<longrightarrow>
"msglen \<le> of_nat (length msgRegisters) \<longrightarrow>
copyMRs sender sbuf receiver rbuf msglen
= forM_x (take (unat msglen) X64_H.msgRegisters)
= forM_x (take (unat msglen) msgRegisters)
(\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser receiver (setRegister r v) od)
>>= (\<lambda>rv. return msglen)"
apply (clarsimp simp: copyMRs_def mapM_discarded)
apply (rule bind_cong[OF refl])
apply (simp add: length_msgRegisters n_msgRegisters_def min_def
apply (simp add: length_msgRegisters min_def
word_le_nat_alt
split: option.split)
apply (simp add: upto_enum_def mapM_Nil)
@ -762,16 +779,16 @@ lemma doIPCTransfer_simple_rewrite:
"monadic_rewrite True True
((\<lambda>_. msgExtraCaps (messageInfoFromWord msgInfo) = 0
\<and> msgLength (messageInfoFromWord msgInfo)
\<le> of_nat (length X64_H.msgRegisters))
\<le> of_nat (length msgRegisters))
and obj_at' (\<lambda>tcb. tcbFault tcb = None
\<and> (user_regs o atcbContextGet o tcbArch) tcb msgInfoRegister = msgInfo) sender)
(doIPCTransfer sender ep badge grant rcvr)
(do rv \<leftarrow> mapM_x (\<lambda>r. do v \<leftarrow> asUser sender (getRegister r);
asUser rcvr (setRegister r v)
od)
(take (unat (msgLength (messageInfoFromWord msgInfo))) X64_H.msgRegisters);
(take (unat (msgLength (messageInfoFromWord msgInfo))) msgRegisters);
y \<leftarrow> setMessageInfo rcvr ((messageInfoFromWord msgInfo) \<lparr>msgCapsUnwrapped := 0\<rparr>);
asUser rcvr (setRegister X64_H.badgeRegister badge)
asUser rcvr (setRegister badgeRegister badge)
od)"
supply if_cong[cong]
apply (rule monadic_rewrite_gen_asm)
@ -923,7 +940,7 @@ lemma oblivious_setVMRoot_schact:
lemma oblivious_switchToThread_schact:
"oblivious (ksSchedulerAction_update f) (ThreadDecls_H.switchToThread t)"
apply (simp add: Thread_H.switchToThread_def X64_H.switchToThread_def bind_assoc
apply (simp add: Thread_H.switchToThread_def switchToThread_def bind_assoc
getCurThread_def setCurThread_def threadGet_def liftM_def
threadSet_def tcbSchedEnqueue_def unless_when asUser_def
getQueue_def setQueue_def storeWordUser_def setRegister_def
@ -979,8 +996,6 @@ crunch obj_at_prio[wp]: cteDeleteOne "obj_at' (\<lambda>tcb. P (tcbPriority tcb)
setThreadState_obj_at_unchanged setNotification_tcb setBoundNotification_obj_at_unchanged
simp: crunch_simps unless_def)
context kernel_m begin
lemma setThreadState_no_sch_change:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s) \<and> (runnable' st \<or> t \<noteq> ksCurThread s)\<rbrace>
setThreadState st t
@ -1012,6 +1027,8 @@ lemma bind_assoc:
= do x \<leftarrow> m; y \<leftarrow> f x; g y od"
by (rule bind_assoc)
context begin interpretation Arch . (*FIXME: arch_split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>
\<Longrightarrow> setObject p v = do f \<leftarrow> gets (obj_at' (\<lambda>v'. v = v' \<or> True) p);
@ -1036,6 +1053,7 @@ lemma setObject_modify_assert:
lemma setEndpoint_isolatable:
"thread_actions_isolatable idx (setEndpoint p e)"
supply if_split[split del]
apply (simp add: setEndpoint_def setObject_modify_assert
assert_def)
apply (case_tac "p \<in> range idx")
@ -1136,6 +1154,7 @@ lemma atcbContextSetSetGet_eq[simp]:
lemma setCTE_isolatable:
"thread_actions_isolatable idx (setCTE p v)"
supply if_split[split del]
apply (simp add: setCTE_assert_modify)
apply (clarsimp simp: thread_actions_isolatable_def
monadic_rewrite_def fun_eq_iff
@ -1198,9 +1217,9 @@ lemma assert_isolatable:
lemma cteInsert_isolatable:
"thread_actions_isolatable idx (cteInsert cap src dest)"
supply if_split[split del] if_cong[cong]
apply (simp add: cteInsert_def updateCap_def updateMDB_def
Let_def setUntypedCapAsFull_def
cong: if_cong)
Let_def setUntypedCapAsFull_def)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
thread_actions_isolatable_if
thread_actions_isolatable_returns assert_isolatable
@ -1298,7 +1317,7 @@ lemma threadGet_isolatable:
lemma switchToThread_isolatable:
"thread_actions_isolatable idx (Arch.switchToThread t)"
apply (simp add: X64_H.switchToThread_def
apply (simp add: switchToThread_def
storeWordUser_def stateAssert_def2)
apply (intro thread_actions_isolatable_bind[OF _ _ hoare_pre(1)]
gets_isolatable setVMRoot_isolatable
@ -1368,7 +1387,7 @@ lemma tcb_at_KOTCB_upd:
= tcb_at' p s"
apply (clarsimp simp: obj_at'_def projectKOs objBits_simps
split: if_split)
apply (simp add: ps_clear_def)
apply (fastforce simp add: ps_clear_def)
done
definition
@ -1416,6 +1435,7 @@ lemma copy_register_isolate:
asUser dest (setRegister r' (rf v)) od)
(isolate_thread_actions idx (return ())
(copy_register_tsrs x y r r' rf) id)"
supply if_split[split del]
apply (simp add: asUser_def split_def bind_assoc
getRegister_def setRegister_def
select_f_returns isolate_thread_actions_def
@ -1565,7 +1585,7 @@ lemmas fastpath_isolate_rewrites
lemma lookupIPCBuffer_isolatable:
"thread_actions_isolatable idx (lookupIPCBuffer w t)"
supply if_cong[cong]
supply if_cong[cong] supply if_split[split del]
apply (simp add: lookupIPCBuffer_def)
apply (rule thread_actions_isolatable_bind)
apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
@ -1586,6 +1606,7 @@ lemma setThreadState_rewrite_simple:
(\<lambda>s. (runnable' st \<or> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> t \<noteq> ksCurThread s) \<and> tcb_at' t s)
(setThreadState st t)
(threadSet (tcbState_update (\<lambda>_. st)) t)"
supply if_split[split del]
apply (simp add: setThreadState_def)
apply (rule monadic_rewrite_imp)
apply (rule monadic_rewrite_trans)

7
proof/crefine/X64/PSpace_C.thy
View File

@ -10,13 +10,6 @@ begin
context kernel begin
lemma koTypeOf_injectKO:
fixes v :: "'a :: pspace_storable" shows
"koTypeOf (injectKO v) = koType TYPE('a)"
apply (cut_tac v1=v in iffD2 [OF project_inject, OF refl])
apply (simp add: project_koType[symmetric])
done
lemma setObject_obj_at_pre:
"\<lbrakk> updateObject ko = updateObject_default ko;
(1 :: machine_word) < 2 ^ objBits ko \<rbrakk>

5
proof/crefine/X64/Retype_C.thy
View File

@ -8031,11 +8031,6 @@ end
context begin interpretation Arch . (*FIXME: arch_split*)
crunches insertNewCap, Arch_createNewCaps, threadSet, Arch.createObject
for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
(wp: crunch_wps setObject_ksPSpace_only
simp: unless_def updateObject_default_def crunch_simps)
lemma createNewCaps_1_gsCNodes_p:
"\<lbrace>\<lambda>s. P (gsCNodes s p) \<and> p \<noteq> ptr\<rbrace> createNewCaps newType ptr 1 n dev\<lbrace>\<lambda>rv s. P (gsCNodes s p)\<rbrace>"
apply (simp add: createNewCaps_def)

65
proof/crefine/X64/SR_lemmas_C.thy
View File

@ -292,67 +292,6 @@ lemma cmdbnode_relation_mdb_node_to_H [simp]:
unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def
by (fastforce split: option.splits)
(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*)
lemma tcb_cte_cases_in_range1:
assumes tc:"tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "x \<le> y"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ 9"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al
by (rule is_aligned_no_overflow)
hence "x \<le> x + q" using qv
apply simp
apply unat_arith
apply simp
done
thus ?thesis using yq by simp
qed
lemma tcb_cte_cases_in_range2:
assumes tc: "tcb_cte_cases (y - x) = Some v"
and al: "is_aligned x tcbBlockSizeBits"
shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1"
proof -
note objBits_defs [simp]
from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1"
unfolding tcb_cte_cases_def
by (simp add: diff_eq_eq split: if_split_asm)
have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv
apply (rule word_plus_mono_right)
apply (rule is_aligned_no_overflow' [OF al])
done
thus ?thesis using yq by (simp add: field_simps)
qed
lemmas tcbSlots =
tcbCTableSlot_def tcbVTableSlot_def
tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
lemma updateObject_cte_tcb:
assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)"
shows "updateObject ctea (KOTCB tcb) ptr ptr' next =
(do alignCheck ptr' (objBits tcb);
magnitudeCheck ptr' next (objBits tcb);
return (KOTCB (updF (\<lambda>_. ctea) tcb))
od)"
using tc unfolding tcb_cte_cases_def
apply -
apply (clarsimp simp add: updateObject_cte Let_def
tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n
split: if_split_asm cong: if_cong)
done
definition
tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> machine_word \<times> machine_word \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option"
where
@ -701,10 +640,6 @@ proof -
qed fact+
qed
lemma ctes_of_cte_at:
"ctes_of s p = Some x \<Longrightarrow> cte_at' p s"
by (simp add: cte_wp_at_ctes_of)
lemma cor_map_relI:
assumes dm: "dom am = dom am'"
and rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y';

15
proof/crefine/X64/Syscall_C.thy
View File

@ -1142,21 +1142,6 @@ lemma deleteCallerCap_ccorres [corres]:
tcb_aligned')
done
(* FIXME: MOVE *)
lemma cap_case_EndpointCap_NotificationCap:
"(case cap of EndpointCap v0 v1 v2 v3 v4 v5 \<Rightarrow> f v0 v1 v2 v3 v4 v5
| NotificationCap v0 v1 v2 v3 \<Rightarrow> g v0 v1 v2 v3
| _ \<Rightarrow> h)
= (if isEndpointCap cap
then f (capEPPtr cap) (capEPBadge cap) (capEPCanSend cap) (capEPCanReceive cap)
(capEPCanGrant cap) (capEPCanGrantReply cap)
else if isNotificationCap cap
then g (capNtfnPtr cap) (capNtfnBadge cap) (capNtfnCanSend cap) (capNtfnCanReceive cap)
else h)"
by (simp add: isCap_simps
split: capability.split)
(* FIXME: MOVE to Corres_C.thy *)
lemma ccorres_trim_redundant_throw_break:
"\<lbrakk>ccorres_underlying rf_sr \<Gamma> arrel axf arrel axf G G' (SKIP # hs) a c;

5
proof/crefine/X64/Tcb_C.thy
View File

@ -8,11 +8,6 @@ theory Tcb_C
imports Delete_C Ipc_C
begin
lemma asUser_obj_at' :
"\<lbrace> K(t\<noteq>t') and obj_at' P t' \<rbrace> asUser t f \<lbrace> \<lambda>_. obj_at' (P::Structures_H.tcb \<Rightarrow> bool) t' \<rbrace>"
including no_pre
by (wpsimp wp: hoare_vcg_ball_lift threadGet_wp simp: split_def asUser_def)
lemma getObject_sched:
"(x::tcb, s') \<in> fst (getObject t s) \<Longrightarrow>
(x,s'\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>) \<in> fst (getObject t (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>))"

29
proof/crefine/X64/VSpace_C.thy
View File

@ -840,17 +840,6 @@ lemma lookupPTSlot_ccorres:
split: X64_H.pde.splits if_splits)
done
lemma cap_case_isPML4Cap:
"(case cap of ArchObjectCap (PML4Cap pm (Some asid)) \<Rightarrow> fn pm asid | _ => g)
= (if (if isArchObjectCap cap then if isPML4Cap (capCap cap) then capPML4MappedASID (capCap cap) \<noteq> None else False else False)
then fn (capPML4BasePtr (capCap cap)) (the (capPML4MappedASID (capCap cap))) else g)"
apply (cases cap; simp add: isArchObjectCap_def)
apply (rename_tac arch_capability)
apply (case_tac arch_capability, simp_all add: isPML4Cap_def)
apply (rename_tac option)
apply (case_tac option; simp)
done
abbreviation
"findVSpaceForASID_xf \<equiv> liftxf errstate findVSpaceForASID_ret_C.status_C findVSpaceForASID_ret_C.vspace_root_C ret__struct_findVSpaceForASID_ret_C_'"
@ -1071,24 +1060,6 @@ lemma ccorres_abstract_known:
apply simp
done
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
"\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v;
(1 :: machine_word) < 2 ^ objBits v \<rbrakk>
\<Longrightarrow> setObject p v s
= modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s"
apply (clarsimp simp: setObject_def split_def exec_gets
obj_at'_def projectKOs lookupAround2_known1
assert_opt_def updateObject_default_def
bind_assoc)
apply (simp add: projectKO_def alignCheck_assert)
apply (simp add: project_inject objBits_def)
apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO)
apply (frule(2) in_magnitude_check[where s'=s])
apply (simp add: magnitudeCheck_assert in_monad)
apply (simp add: simpler_modify_def)
done
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)
\<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g"