secc
/
seL4-L4.verified
mirror of https://github.com/seL4/l4v.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

trivial: rename arch_split -> arch-split 

Unifying the tag between Github labels, docs, and so on will make it
less confusing to grep for and deal with.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2024-07-24 11:23:08 +10:00 committed by Rafal Kolanski
parent 423e5d44e7
commit 0875edf96a
320 changed files with 754 additions and 754 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
docs/arch-split.md
View File

@ -111,7 +111,7 @@ theory Retype_R
imports VSpace_R
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma placeNewObject_def2:
"placeNewObject ptr val gb = createObjects' ptr 1 (injectKO val) gb"
@ -199,7 +199,7 @@ architecture. If we saw such a reference in a generic theory, we would
immediately recognise that something was wrong.
The convention is that in architecture-specific theories, we initially
give *all* types, constants and lemmas with the architecture-specific
give *all* types, constants and lemmas the architecture-specific
`arch_global_naming` scheme. Then, in generic theories, we use
*requalification* to selectively extract just those types, constants and
facts which are expected to exist on all architectures.
@ -339,7 +339,7 @@ available unqualified until the end of the context block. Indeed, in this case,
the only purpose of the anonymous context block is to limit the scope of this
`interpretation`.
Note: It is critical to the success of arch_split that we *never* interpret the
Note: It is critical to the success of arch-split that we *never* interpret the
Arch locale, *except* inside an appropriate context block.
In a generic theory, we typically only interpret the Arch locale to keep
@ -770,7 +770,7 @@ will only ever look at the heap, so this proof will always work.
There are some considerations when using this strategy:
1. We use the Arch locale without a `global_naming`, as its performance better
1. We use the Arch locale without `global_naming`, as its performance is better
than entering the Arch locale and proving the lemma there. This means its
qualified name will be `Arch.valid_arch_cap_pspaceI`, but this is acceptable
since:
@ -869,7 +869,7 @@ The workflow:
intra-theory dependencies" above.
- Look in the generic theory for a block of the form
`context Arch begin (* FIXME: arch_split *) ... end`.
`context Arch begin (* FIXME: arch-split *) ... end`.
- These indicate things that we've previously classified as belonging in an
arch-specific theory.
@ -881,7 +881,7 @@ The workflow:
- Look for subsequent breakage in the generic theory.
- If this is in a subsequent Arch block (`context Arch begin (* FIXME:
arch_split *) ... end`), just move that block.
arch-split *) ... end`), just move that block.
- Otherwise, if it's not obvious what to do, have a conversation with someone.
We'll add more tips here as the process becomes clearer.

2
proof/access-control/ARM/ArchIpc_AC.thy
View File

@ -192,7 +192,7 @@ declare arch_get_sanitise_register_info_inv[Ipc_AC_assms]
end
context is_extended begin interpretation Arch . (*FIXME: arch_split*)
context is_extended begin interpretation Arch . (*FIXME: arch-split*)
lemma list_integ_lift_in_ipc[Ipc_AC_assms]:
assumes li:

2
proof/access-control/ARM/ExampleSystem.thy
View File

@ -8,7 +8,7 @@ theory ExampleSystem
imports ArchAccess_AC
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
nat_to_bl :: "nat \<Rightarrow> nat \<Rightarrow> bool list option"

2
proof/access-control/RISCV64/ExampleSystem.thy
View File

@ -8,7 +8,7 @@ theory ExampleSystem
imports ArchAccess_AC
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
nat_to_bl :: "nat \<Rightarrow> nat \<Rightarrow> bool list option"

2
proof/bisim/Syscall_S.thy
View File

@ -8,7 +8,7 @@ theory Syscall_S
imports Separation
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma syscall_bisim:
assumes bs:

6
proof/crefine/AARCH64/ADT_C.thy
View File

@ -220,7 +220,7 @@ end
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
@ -345,7 +345,7 @@ lemma cint_rel_to_H:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"cstate_to_machine_H s \<equiv>
@ -630,7 +630,7 @@ lemma carch_state_to_H_correct:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>

2
proof/crefine/AARCH64/Arch_C.thy
View File

@ -12,7 +12,7 @@ begin
unbundle l4v_word_context
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch unmapPageTable
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"

2
proof/crefine/AARCH64/CLevityCatch.thy
View File

@ -73,7 +73,7 @@ qed
(* end holding area *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
(* Short-hand for unfolding cumbersome machine constants *)
(* FIXME MOVE these should be in refine, and the _eq forms should NOT be declared [simp]! *)

2
proof/crefine/AARCH64/DetWP.thy
View File

@ -9,7 +9,7 @@ theory DetWP
imports "Lib.DetWPLib" "CBaseRefine.Include_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma det_wp_doMachineOp [wp]:
"det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)"

2
proof/crefine/AARCH64/Fastpath_C.thy
View File

@ -17,7 +17,7 @@ imports
"CLib.MonadicRewrite_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setCTE_obj_at'_queued:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>"

2
proof/crefine/AARCH64/Fastpath_Defs.thy
View File

@ -15,7 +15,7 @@ theory Fastpath_Defs
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"fastpaths sysc \<equiv> case sysc of

2
proof/crefine/AARCH64/Fastpath_Equiv.thy
View File

@ -45,7 +45,7 @@ lemma setCTE_tcbContext:
apply (rule setObject_cte_obj_at_tcb', simp_all)
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setThreadState_tcbContext:
"setThreadState st tptr \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"

2
proof/crefine/AARCH64/Invoke_C.thy
View File

@ -1382,7 +1382,7 @@ lemma decodeCNodeInvocation_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemmas setCTE_def3 = setCTE_def2[THEN eq_reflection]

8
proof/crefine/AARCH64/Ipc_C.thy
View File

@ -14,7 +14,7 @@ imports
IsolatedThreadAction
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"replyFromKernel_success_empty thread \<equiv> do
@ -292,7 +292,7 @@ lemma ccap_relation_reply_helpers:
cap_reply_cap_lift_def word_size
elim!: ccap_relationE)
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
(*FIXME: fupdate simplification issues for 2D arrays *)
abbreviation "syscallMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
@ -315,7 +315,7 @@ lemma syscallMessage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"handleArchFaultReply' f sender receiver tag \<equiv>
@ -1041,7 +1041,7 @@ lemma setMR_ccorres_dc:
end
(* FIXME: move *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setMR
for valid_pspace'[wp]: "valid_pspace'"
crunch setMR

4
proof/crefine/AARCH64/IsolatedThreadAction.thy
View File

@ -156,7 +156,7 @@ lemma partial_overwrite_fun_upd:
apply (clarsimp split: if_split)
done
context begin interpretation Arch . (*FIXME: arch_split*)
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)
@ -1349,7 +1349,7 @@ 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*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>

2
proof/crefine/AARCH64/Recycle_C.thy
View File

@ -533,7 +533,7 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply simp+
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_asidpool_gs[wp]:
"setObject ptr (vcpu::asidpool) \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace>"

4
proof/crefine/AARCH64/Retype_C.thy
View File

@ -41,7 +41,7 @@ lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x80000000000000
apply simp
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma map_option_byte_to_word_heap:
assumes disj: "\<And>(off :: 9 word) x. x<8 \<Longrightarrow> p + ucast off * 8 + x \<notin> S " (*9=page table index*)
@ -7833,7 +7833,7 @@ lemma APIType_capBits_min:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
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>"

2
proof/crefine/AARCH64/SR_lemmas_C.thy
View File

@ -12,7 +12,7 @@ imports
"Refine.Invariants_H"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
section "vm rights"

2
proof/crefine/AARCH64/Schedule_C.thy
View File

@ -12,7 +12,7 @@ begin
instance tcb :: no_vcpu by intro_classes auto
(*FIXME: arch_split: move up?*)
(*FIXME: arch-split: move up?*)
context Arch begin
context begin global_naming global
requalify_facts

8
proof/crefine/AARCH64/StateRelation_C.thy
View File

@ -10,7 +10,7 @@ theory StateRelation_C
imports Wellformed_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"lifth p s \<equiv> the (clift (t_hrs_' s) p)"
@ -81,7 +81,7 @@ text \<open>
which can subsequently be instantiated for
@{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}.
\<close>
locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*)
locale state_rel = Arch + substitute_pre + (*FIXME: arch-split*)
fixes armKSKernelVSpace_C :: "machine_word \<Rightarrow> arm_vspace_region_use"
locale kernel = kernel_all_substitute + state_rel
@ -133,7 +133,7 @@ definition carch_state_relation :: "Arch.kernel_state \<Rightarrow> globals \<Ri
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool"
@ -709,7 +709,7 @@ where
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
\<longrightarrow> abitmap2 (d, i) = 0)"
end (* interpretation Arch . (*FIXME: arch_split*) *)
end (* interpretation Arch . (*FIXME: arch-split*) *)
definition
region_is_bytes' :: "machine_word \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"

6
proof/crefine/AARCH64/SyscallArgs_C.thy
View File

@ -13,13 +13,13 @@ imports
StoreWord_C DetWP
begin
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
context kernel_m begin
abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
declare word_neq_0_conv[simp del]
@ -1201,7 +1201,7 @@ lemma getSyscallArg_ccorres_foo:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);

2
proof/crefine/AARCH64/Syscall_C.thy
View File

@ -15,7 +15,7 @@ imports
Arch_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch replyFromKernel
for sch_act_wf[wp]: "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
end

4
proof/crefine/AARCH64/Tcb_C.thy
View File

@ -59,7 +59,7 @@ lemma doMachineOp_sched:
apply fastforce
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch restart
for curThread[wp]: "\<lambda>s. P (ksCurThread s)"
(wp: crunch_wps simp: crunch_simps)
@ -1105,7 +1105,7 @@ lemma Arch_performTransfer_ccorres:
apply simp+
done
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"

2
proof/crefine/AARCH64/VSpace_C.thy
View File

@ -19,7 +19,7 @@ autocorres
c_locale = kernel_all_substitute
] "../c/build/$L4V_ARCH/kernel_all.c_pp"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)

4
proof/crefine/AARCH64/Wellformed_C.thy
View File

@ -15,7 +15,7 @@ imports
"CSpec.Substitute"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
(* Takes an address and ensures it can be given to a function expecting a canonical address.
Canonical addresses on 64-bit machines aren't really 64-bit, due to bus sizes. Hence, structures
@ -303,7 +303,7 @@ record cte_CL =
cap_CL :: cap_CL
cteMDBNode_CL :: mdb_node_CL
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cte_lift :: "cte_C \<rightharpoonup> cte_CL"

6
proof/crefine/ARM/ADT_C.thy
View File

@ -193,7 +193,7 @@ end
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
@ -320,7 +320,7 @@ lemma cint_rel_to_H:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"cstate_to_machine_H s \<equiv>
@ -625,7 +625,7 @@ lemma (in kernel_m) carch_state_to_H_correct:
apply (fastforce simp: valid_asid_table'_def)
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>

2
proof/crefine/ARM/Arch_C.thy
View File

@ -9,7 +9,7 @@ theory Arch_C
imports Recycle_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch unmapPageTable
for ctes_of[wp]: "\<lambda>s. P (ctes_of s)"
(wp: crunch_wps simp: crunch_simps)

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

@ -13,7 +13,7 @@ imports
Boolean_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
(* Rule previously in the simpset, now not. *)
declare ptr_add_def' [simp]

2
proof/crefine/ARM/DetWP.thy
View File

@ -8,7 +8,7 @@ theory DetWP
imports "Lib.DetWPLib" "CBaseRefine.Include_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma det_wp_doMachineOp [wp]:
"det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)"

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

@ -17,7 +17,7 @@ imports
"CLib.MonadicRewrite_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setCTE_obj_at'_queued:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>"

2
proof/crefine/ARM/Fastpath_Defs.thy
View File

@ -15,7 +15,7 @@ theory Fastpath_Defs
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"fastpaths sysc \<equiv> case sysc of

2
proof/crefine/ARM/Fastpath_Equiv.thy
View File

@ -45,7 +45,7 @@ lemma setCTE_tcbContext:
apply (rule setObject_cte_obj_at_tcb', simp_all)
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setThreadState_tcbContext:
"setThreadState st tptr \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"

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

@ -1097,7 +1097,7 @@ lemma offset_xf_for_sequence:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateHWASIDEntry
for pde_mappings'[wp]: "valid_pde_mappings'"
end
@ -1140,7 +1140,7 @@ lemma invalidateASIDEntry_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateASIDEntry
for obj_at'[wp]: "obj_at' P p"
crunch flushSpace

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

@ -1371,7 +1371,7 @@ lemma decodeCNodeInvocation_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setCTE_sch_act_wf[wp]:
"\<lbrace> \<lambda>s. sch_act_wf (ksSchedulerAction s) s \<rbrace>

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

@ -13,7 +13,7 @@ imports
IsolatedThreadAction
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"replyFromKernel_success_empty thread \<equiv> do
@ -275,7 +275,7 @@ lemma ccap_relation_reply_helpers:
cap_reply_cap_lift_def word_size
elim!: ccap_relationE)
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
(*FIXME: fupdate simplification issues for 2D arrays *)
abbreviation "syscallMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
@ -298,7 +298,7 @@ lemma syscallMessage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"handleArchFaultReply' f sender receiver tag \<equiv> do
@ -883,7 +883,7 @@ lemma setMR_ccorres_dc:
end
(* FIXME: move *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setMR
for valid_pspace'[wp]: "valid_pspace'"
crunch setMR

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

@ -9,7 +9,7 @@ theory IsolatedThreadAction
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
datatype tcb_state_regs =
TCBStateRegs (tsrState : thread_state) (tsrContext : "MachineTypes.register \<Rightarrow> machine_word")
@ -960,7 +960,7 @@ 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*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>

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

@ -8,7 +8,7 @@ theory PSpace_C
imports Ctac_lemmas_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_obj_at_pre:
"\<lbrakk> updateObject ko = updateObject_default ko;

2
proof/crefine/ARM/Recycle_C.thy
View File

@ -350,7 +350,7 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply simp+
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateTLBByASID
for pde_mappings'[wp]: "valid_pde_mappings'"

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

@ -10,7 +10,7 @@ theory Refine_C
imports Init_C Fastpath_Equiv Fastpath_C CToCRefine
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch handleVMFault
for ksQ[wp]: "\<lambda>s. P (ksReadyQueues s)"
(ignore: getFAR getDFSR getIFSR)

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

@ -17,7 +17,7 @@ declare word_neq_0_conv [simp del]
instance cte_C :: array_outer_max_size
by intro_classes simp
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma map_option_byte_to_word_heap:
assumes disj: "\<And>(off :: 10 word) x. x<4 \<Longrightarrow> p + ucast off * 4 + x \<notin> S "
@ -4141,7 +4141,7 @@ lemma placeNewObject_pde:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
end
lemma dom_disj_union:
@ -6356,7 +6356,7 @@ lemma APIType_capBits_min:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
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>"

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

@ -10,7 +10,7 @@ imports
"Refine.Invariants_H"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
section "ctes"

2
proof/crefine/ARM/Schedule_C.thy
View File

@ -9,7 +9,7 @@ theory Schedule_C
imports Tcb_C Detype_C
begin
(*FIXME: arch_split: move up?*)
(*FIXME: arch-split: move up?*)
context Arch begin
context begin global_naming global
requalify_facts

6
proof/crefine/ARM/StateRelation_C.thy
View File

@ -8,7 +8,7 @@ theory StateRelation_C
imports Wellformed_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"lifth p s \<equiv> the (clift (t_hrs_' s) p)"
@ -100,7 +100,7 @@ text \<open>
which can subsequently be instantiated for
@{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}.
\<close>
locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*)
locale state_rel = Arch + substitute_pre + (*FIXME: arch-split*)
fixes armKSKernelVSpace_C :: "machine_word \<Rightarrow> arm_vspace_region_use"
locale kernel = kernel_all_substitute + state_rel
@ -134,7 +134,7 @@ where
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool"

6
proof/crefine/ARM/SyscallArgs_C.thy
View File

@ -12,13 +12,13 @@ imports
StoreWord_C DetWP
begin
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
context kernel_m begin
abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
declare word_neq_0_conv[simp del]
@ -1256,7 +1256,7 @@ lemma getSyscallArg_ccorres_foo:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);

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

@ -14,7 +14,7 @@ imports
Arch_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch replyFromKernel
for sch_act_wf[wp]: "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
end

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

@ -58,7 +58,7 @@ lemma doMachineOp_sched:
apply fastforce
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch restart
for curThread[wp]: "\<lambda>s. P (ksCurThread s)"
@ -1029,7 +1029,7 @@ lemma Arch_performTransfer_ccorres:
apply simp+
done
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"

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

@ -1141,7 +1141,7 @@ lemma rf_sr_armKSNextASID:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateASID
for armKSNextASID[wp]: "\<lambda>s. P (armKSNextASID (ksArchState s))"
@ -1615,7 +1615,7 @@ lemma doFlush_ccorres:
done
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setVMRootForFlush
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"
(wp: crunch_wps)
@ -1860,7 +1860,7 @@ lemma flushPage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch flushPage
for no_0_obj'[wp]: "no_0_obj'"
end

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

@ -14,7 +14,7 @@ imports
"CSpec.Substitute"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
abbreviation
cte_Ptr :: "word32 \<Rightarrow> cte_C ptr" where "cte_Ptr == Ptr"
@ -232,7 +232,7 @@ record cte_CL =
cap_CL :: cap_CL
cteMDBNode_CL :: mdb_node_CL
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cte_lift :: "cte_C \<rightharpoonup> cte_CL"

4
proof/crefine/ARM_HYP/ADT_C.thy
View File

@ -213,7 +213,7 @@ end
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
@ -634,7 +634,7 @@ lemma (in kernel_m) carch_state_to_H_correct:
apply (fastforce simp: valid_asid_table'_def)
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>

2
proof/crefine/ARM_HYP/Arch_C.thy
View File

@ -11,7 +11,7 @@ begin
unbundle l4v_word_context
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch unmapPageTable
for ctes_of[wp]: "\<lambda>s. P (ctes_of s)"
(wp: crunch_wps simp: crunch_simps)

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

@ -13,7 +13,7 @@ imports
Boolean_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
declare word_neq_0_conv [simp del]

2
proof/crefine/ARM_HYP/DetWP.thy
View File

@ -8,7 +8,7 @@ theory DetWP
imports "Lib.DetWPLib" "CBaseRefine.Include_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma det_wp_doMachineOp [wp]:
"det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)"

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

@ -17,7 +17,7 @@ imports
"CLib.MonadicRewrite_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setCTE_obj_at'_queued:
"\<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>"

2
proof/crefine/ARM_HYP/Fastpath_Defs.thy
View File

@ -15,7 +15,7 @@ theory Fastpath_Defs
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"fastpaths sysc \<equiv> case sysc of

2
proof/crefine/ARM_HYP/Fastpath_Equiv.thy
View File

@ -45,7 +45,7 @@ lemma setCTE_tcbContext:
apply (rule setObject_cte_obj_at_tcb', simp_all)
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setThreadState_tcbContext:
"setThreadState st tptr \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>"

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

@ -1131,7 +1131,7 @@ lemma offset_xf_for_sequence:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateHWASIDEntry
for pde_mappings'[wp]: "valid_pde_mappings'"
end
@ -1174,7 +1174,7 @@ lemma invalidateASIDEntry_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateASIDEntry
for obj_at'[wp]: "obj_at' P p"
crunch flushSpace

2
proof/crefine/ARM_HYP/Invoke_C.thy
View File

@ -1390,7 +1390,7 @@ lemma decodeCNodeInvocation_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemmas setCTE_def3 = setCTE_def2[THEN eq_reflection]

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

@ -13,7 +13,7 @@ imports
IsolatedThreadAction
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"replyFromKernel_success_empty thread \<equiv> do
@ -346,7 +346,7 @@ lemma ccap_relation_reply_helpers:
cap_reply_cap_lift_def word_size
elim!: ccap_relationE)
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
(*FIXME: fupdate simplification issues for 2D arrays *)
abbreviation "syscallMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
@ -369,7 +369,7 @@ lemma syscallMessage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"handleArchFaultReply' f sender receiver tag \<equiv>
@ -1088,7 +1088,7 @@ lemma setMR_ccorres_dc:
end
(* FIXME: move *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setMR
for valid_pspace'[wp]: "valid_pspace'"
crunch setMR

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

@ -9,7 +9,7 @@ theory IsolatedThreadAction
imports ArchMove_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
datatype tcb_state_regs =
TCBStateRegs (tsrState : thread_state) (tsrContext : "MachineTypes.register \<Rightarrow> machine_word")
@ -1235,7 +1235,7 @@ 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*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>

2
proof/crefine/ARM_HYP/Recycle_C.thy
View File

@ -576,7 +576,7 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply simp+
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateTLBByASID
for pde_mappings'[wp]: "valid_pde_mappings'"

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

@ -20,7 +20,7 @@ instance cte_C :: array_outer_max_size
instance virq_C :: array_inner_packed
by intro_classes simp
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma map_option_byte_to_word_heap:
@ -4713,7 +4713,7 @@ lemma placeNewObject_pde:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
end
lemma dom_disj_union:
@ -7691,7 +7691,7 @@ lemma APIType_capBits_min:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
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>"

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

@ -10,7 +10,7 @@ imports
"Refine.Invariants_H"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
section "ctes"

2
proof/crefine/ARM_HYP/Schedule_C.thy
View File

@ -11,7 +11,7 @@ begin
instance tcb :: no_vcpu by intro_classes auto
(*FIXME: arch_split: move up?*)
(*FIXME: arch-split: move up?*)
context Arch begin
context begin global_naming global
requalify_facts

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

@ -8,7 +8,7 @@ theory StateRelation_C
imports Wellformed_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"lifth p s \<equiv> the (clift (t_hrs_' s) p)"
@ -96,7 +96,7 @@ text \<open>
which can subsequently be instantiated for
@{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}.
\<close>
locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*)
locale state_rel = Arch + substitute_pre + (*FIXME: arch-split*)
fixes armKSKernelVSpace_C :: "machine_word \<Rightarrow> arm_vspace_region_use"
locale kernel = kernel_all_substitute + state_rel
@ -139,7 +139,7 @@ where
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool"
@ -702,7 +702,7 @@ where
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
\<longrightarrow> abitmap2 (d, i) = 0)"
end (* interpretation Arch . (*FIXME: arch_split*) *)
end (* interpretation Arch . (*FIXME: arch-split*) *)
definition
region_is_bytes' :: "word32 \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"

6
proof/crefine/ARM_HYP/SyscallArgs_C.thy
View File

@ -12,13 +12,13 @@ imports
StoreWord_C DetWP
begin
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
context kernel_m begin
abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
declare word_neq_0_conv[simp del]
@ -1289,7 +1289,7 @@ lemma getSyscallArg_ccorres_foo:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);

2
proof/crefine/ARM_HYP/Syscall_C.thy
View File

@ -14,7 +14,7 @@ imports
Arch_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch replyFromKernel
for sch_act_wf[wp]: "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
end

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

@ -58,7 +58,7 @@ lemma doMachineOp_sched:
apply fastforce
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch restart
for curThread[wp]: "\<lambda>s. P (ksCurThread s)"
@ -1090,7 +1090,7 @@ lemma Arch_performTransfer_ccorres:
apply simp+
done
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"

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

@ -9,7 +9,7 @@ theory VSpace_C
imports TcbAcc_C CSpace_C PSpace_C TcbQueue_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)
@ -1218,7 +1218,7 @@ lemma rf_sr_armKSNextASID:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch invalidateASID
for armKSNextASID[wp]: "\<lambda>s. P (armKSNextASID (ksArchState s))"
@ -2727,7 +2727,7 @@ lemma doFlush_ccorres:
done
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setVMRootForFlush
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"
(wp: crunch_wps)
@ -3041,7 +3041,7 @@ lemmas unfold_checkMapping_return
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch flushPage
for no_0_obj'[wp]: "no_0_obj'"
end

4
proof/crefine/ARM_HYP/Wellformed_C.thy
View File

@ -14,7 +14,7 @@ imports
"CSpec.Substitute"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
abbreviation
cte_Ptr :: "word32 \<Rightarrow> cte_C ptr" where "cte_Ptr == Ptr"
@ -265,7 +265,7 @@ record cte_CL =
cap_CL :: cap_CL
cteMDBNode_CL :: mdb_node_CL
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cte_lift :: "cte_C \<rightharpoonup> cte_CL"

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

@ -194,7 +194,7 @@ end
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
@ -566,7 +566,7 @@ lemma carch_state_to_H_correct:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>

2
proof/crefine/RISCV64/Arch_C.thy
View File

@ -12,7 +12,7 @@ begin
unbundle l4v_word_context
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch unmapPageTable
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"

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

@ -13,7 +13,7 @@ imports
Boolean_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
(* Short-hand for unfolding cumbersome machine constants *)
(* FIXME MOVE these should be in refine, and the _eq forms should NOT be declared [simp]! *)

2
proof/crefine/RISCV64/DetWP.thy
View File

@ -9,7 +9,7 @@ theory DetWP
imports "Lib.DetWPLib" "CBaseRefine.Include_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma det_wp_doMachineOp [wp]:
"det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)"

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

@ -1382,7 +1382,7 @@ lemma decodeCNodeInvocation_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemmas setCTE_def3 = setCTE_def2[THEN eq_reflection]

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

@ -14,7 +14,7 @@ imports
IsolatedThreadAction
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"replyFromKernel_success_empty thread \<equiv> do
@ -294,7 +294,7 @@ lemma ccap_relation_reply_helpers:
cap_reply_cap_lift_def word_size
elim!: ccap_relationE)
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
(*FIXME: fupdate simplification issues for 2D arrays *)
abbreviation "syscallMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
@ -317,7 +317,7 @@ lemma syscallMessage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"handleArchFaultReply' f sender receiver tag \<equiv> do
@ -1015,7 +1015,7 @@ lemma setMR_ccorres_dc:
end
(* FIXME: move *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setMR
for valid_pspace'[wp]: "valid_pspace'"
crunch setMR

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

@ -112,7 +112,7 @@ lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
@ -161,7 +161,7 @@ lemma partial_overwrite_fun_upd:
apply (clarsimp split: if_split)
done
context begin interpretation Arch . (*FIXME: arch_split*)
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)
@ -994,7 +994,7 @@ 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*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>

2
proof/crefine/RISCV64/Recycle_C.thy
View File

@ -520,7 +520,7 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply simp+
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch deleteASIDPool
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"
(wp: crunch_wps getObject_inv loadObject_default_inv

2
proof/crefine/RISCV64/Refine_C.thy
View File

@ -20,7 +20,7 @@ imports
CToCRefine
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch handleVMFault
for ksQ[wp]: "\<lambda>s. P (ksReadyQueues s)"
end

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

@ -46,7 +46,7 @@ lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x80000000000000
apply simp
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma map_option_byte_to_word_heap:
assumes disj: "\<And>(off :: 9 word) x. x<8 \<Longrightarrow> p + ucast off * 8 + x \<notin> S " (*9=page table index*)
@ -6797,7 +6797,7 @@ lemma APIType_capBits_min:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
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>"

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

@ -11,7 +11,7 @@ imports
"Refine.Invariants_H"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
section "vm rights"

2
proof/crefine/RISCV64/Schedule_C.thy
View File

@ -10,7 +10,7 @@ theory Schedule_C
imports Tcb_C Detype_C
begin
(*FIXME: arch_split: move up?*)
(*FIXME: arch-split: move up?*)
context Arch begin
context begin global_naming global
requalify_facts

8
proof/crefine/RISCV64/StateRelation_C.thy
View File

@ -9,7 +9,7 @@ theory StateRelation_C
imports Wellformed_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"lifth p s \<equiv> the (clift (t_hrs_' s) p)"
@ -80,7 +80,7 @@ text \<open>
which can subsequently be instantiated for
@{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}.
\<close>
locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*)
locale state_rel = Arch + substitute_pre + (*FIXME: arch-split*)
fixes riscvKSKernelVSpace_C :: "machine_word \<Rightarrow> riscvvspace_region_use"
locale kernel = kernel_all_substitute + state_rel
@ -129,7 +129,7 @@ where
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool"
@ -631,7 +631,7 @@ where
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
\<longrightarrow> abitmap2 (d, i) = 0)"
end (* interpretation Arch . (*FIXME: arch_split*) *)
end (* interpretation Arch . (*FIXME: arch-split*) *)
definition
region_is_bytes' :: "machine_word \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"

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

@ -13,13 +13,13 @@ imports
StoreWord_C DetWP
begin
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
context kernel_m begin
abbreviation "msgRegistersC \<equiv> kernel_all_substitute.msgRegisters"
lemmas msgRegistersC_def = kernel_all_substitute.msgRegisters_def
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
declare word_neq_0_conv[simp del]
@ -1190,7 +1190,7 @@ lemma getSyscallArg_ccorres_foo:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma invocation_eq_use_type:
"\<lbrakk> value \<equiv> (value' :: 32 signed word);

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

@ -15,7 +15,7 @@ imports
Arch_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch replyFromKernel
for sch_act_wf[wp]: "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
end

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

@ -59,7 +59,7 @@ lemma doMachineOp_sched:
apply fastforce
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch restart
for curThread[wp]: "\<lambda>s. P (ksCurThread s)"
@ -1113,7 +1113,7 @@ lemma Arch_performTransfer_ccorres:
apply simp+
done
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
abbreviation "frameRegistersC \<equiv> kernel_all_substitute.frameRegisters"
lemmas frameRegistersC_def = kernel_all_substitute.frameRegisters_def
abbreviation "gpRegistersC \<equiv> kernel_all_substitute.gpRegisters"

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

@ -19,7 +19,7 @@ autocorres
c_locale = kernel_all_substitute
] "../c/build/$L4V_ARCH/kernel_all.c_pp"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma ccorres_name_pre_C:
"(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g)

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

@ -15,7 +15,7 @@ imports
"CSpec.Substitute"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
abbreviation
cte_Ptr :: "word64 \<Rightarrow> cte_C ptr" where "cte_Ptr == Ptr"
@ -246,7 +246,7 @@ record cte_CL =
cap_CL :: cap_CL
cteMDBNode_CL :: mdb_node_CL
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cte_lift :: "cte_C \<rightharpoonup> cte_CL"

4
proof/crefine/X64/ADT_C.thy
View File

@ -201,7 +201,7 @@ end
consts
Init_C' :: "unit observable \<Rightarrow> cstate global_state set"
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition "Init_C \<equiv> \<lambda>((tc,s),m,e). Init_C' ((tc, truncate_state s),m,e)"
@ -604,7 +604,7 @@ lemma carch_state_to_H_correct:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma tcb_queue_rel_unique:
"hp NULL = None \<Longrightarrow>

2
proof/crefine/X64/Arch_C.thy
View File

@ -11,7 +11,7 @@ begin
unbundle l4v_word_context
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch unmapPageTable, unmapPageDirectory, unmapPDPT
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"

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

@ -13,7 +13,7 @@ imports
Boolean_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
(* Short-hand for unfolding cumbersome machine constants *)

2
proof/crefine/X64/DetWP.thy
View File

@ -8,7 +8,7 @@ theory DetWP
imports "Lib.DetWPLib" "CBaseRefine.Include_C"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma det_wp_doMachineOp [wp]:
"det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)"

2
proof/crefine/X64/Invoke_C.thy
View File

@ -1380,7 +1380,7 @@ lemma decodeCNodeInvocation_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemmas setCTE_def3 = setCTE_def2[THEN eq_reflection]

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

@ -13,7 +13,7 @@ imports
IsolatedThreadAction
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"replyFromKernel_success_empty thread \<equiv> do
@ -293,7 +293,7 @@ lemma ccap_relation_reply_helpers:
cap_reply_cap_lift_def word_size
elim!: ccap_relationE)
(*FIXME: arch_split: C kernel names hidden by Haskell names *)
(*FIXME: arch-split: C kernel names hidden by Haskell names *)
(*FIXME: fupdate simplification issues for 2D arrays *)
abbreviation "syscallMessageC \<equiv> kernel_all_global_addresses.fault_messages.[unat MessageID_Syscall]"
lemmas syscallMessageC_def = kernel_all_substitute.fault_messages_def
@ -316,7 +316,7 @@ lemma syscallMessage_ccorres:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"handleArchFaultReply' f sender receiver tag \<equiv> do
@ -1016,7 +1016,7 @@ lemma setMR_ccorres_dc:
end
(* FIXME: move *)
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch setMR
for valid_pspace'[wp]: "valid_pspace'"
crunch setMR

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

@ -111,7 +111,7 @@ lemmas setNotification_tcb = set_ntfn_tcb_obj_at'
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify:
fixes v :: "'a :: pspace_storable" shows
@ -162,7 +162,7 @@ lemma partial_overwrite_fun_upd:
apply (clarsimp split: if_split)
done
context begin interpretation Arch . (*FIXME: arch_split*)
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)
@ -982,7 +982,7 @@ 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*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma setObject_modify_assert:
"\<lbrakk> updateObject v = updateObject_default v \<rbrakk>

2
proof/crefine/X64/Recycle_C.thy
View File

@ -555,7 +555,7 @@ lemma heap_to_user_data_in_user_mem'[simp]:
apply simp+
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch deleteASIDPool
for gsMaxObjectSize[wp]: "\<lambda>s. P (gsMaxObjectSize s)"
(wp: crunch_wps getObject_inv loadObject_default_inv

2
proof/crefine/X64/Refine_C.thy
View File

@ -20,7 +20,7 @@ imports
CToCRefine
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
crunch handleVMFault
for ksQ[wp]: "\<lambda>s. P (ksReadyQueues s)"
end

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

@ -46,7 +46,7 @@ lemma zero_le_sint: "\<lbrakk> 0 \<le> (a :: machine_word); a < 0x80000000000000
apply simp
done
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
lemma map_option_byte_to_word_heap:
assumes disj: "\<And>(off :: 9 word) x. x<8 \<Longrightarrow> p + ucast off * 8 + x \<notin> S " (*9=page table index*)
@ -7908,7 +7908,7 @@ lemma APIType_capBits_min:
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
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>"

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

@ -10,7 +10,7 @@ imports
"Refine.Invariants_H"
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
section "ctes"

2
proof/crefine/X64/Schedule_C.thy
View File

@ -9,7 +9,7 @@ theory Schedule_C
imports Tcb_C Detype_C
begin
(*FIXME: arch_split: move up?*)
(*FIXME: arch-split: move up?*)
context Arch begin
context begin global_naming global
requalify_facts

8
proof/crefine/X64/StateRelation_C.thy
View File

@ -8,7 +8,7 @@ theory StateRelation_C
imports Wellformed_C
begin
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
"lifth p s \<equiv> the (clift (t_hrs_' s) p)"
@ -79,7 +79,7 @@ text \<open>
which can subsequently be instantiated for
@{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}.
\<close>
locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*)
locale state_rel = Arch + substitute_pre + (*FIXME: arch-split*)
fixes x64KSKernelVSpace_C :: "machine_word \<Rightarrow> x64vspace_region_use"
locale kernel = kernel_all_substitute + state_rel
@ -197,7 +197,7 @@ where
end
context begin interpretation Arch . (*FIXME: arch_split*)
context begin interpretation Arch . (*FIXME: arch-split*)
definition
cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool"
@ -863,7 +863,7 @@ where
((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize))
\<longrightarrow> abitmap2 (d, i) = 0)"
end (* interpretation Arch . (*FIXME: arch_split*) *)
end (* interpretation Arch . (*FIXME: arch-split*) *)
definition
region_is_bytes' :: "machine_word \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool"

Some files were not shown because too many files have changed in this diff Show More