arch_split: split up Invariants_AI
This commit is contained in:
Daniel Matichuk
parent
1018d01b6f
commit
df8261c121
|
|
@ -13,9 +13,11 @@ keywords "qualify" :: thy_decl and "end_qualify" :: thy_decl
|
|||
begin
|
||||
ML \<open>
|
||||
|
||||
type qualify_args = {name : string, deep : bool}
|
||||
|
||||
structure Data = Theory_Data
|
||||
(
|
||||
type T = (theory * string) option *
|
||||
type T = (theory * qualify_args) option *
|
||||
((string *
|
||||
((binding Symtab.table) * (* facts *)
|
||||
(binding Symtab.table) * (* consts *)
|
||||
|
|
@ -51,37 +53,55 @@ fun map_consts_of str f thy = map_tabs_of str (@{apply 3(2)} f) thy;
|
|||
|
||||
fun map_types_of str f thy = map_tabs_of str (@{apply 3(3)} f) thy;
|
||||
|
||||
fun make_bind nm =
|
||||
fun make_bind space thy nm =
|
||||
let
|
||||
val base = Long_Name.explode nm |> tl |> rev |> tl |> rev;
|
||||
in fold (Binding.qualify false) base (Binding.make (Long_Name.base_name nm, Position.none)) end;
|
||||
val short_name =
|
||||
Name_Space.extern_shortest (Proof_Context.init_global thy) space nm
|
||||
|> Long_Name.explode |> rev |> tl |> rev;
|
||||
val long_name = Long_Name.explode nm |> tl |> rev |> tl |> rev;
|
||||
|
||||
fun do_make_bind (short_qual :: l) (_ :: l') b = Binding.qualify true short_qual (do_make_bind l l' b)
|
||||
| do_make_bind [] (long_qual :: l) b = Binding.qualify false long_qual (do_make_bind [] l b)
|
||||
| do_make_bind [] [] b = b
|
||||
| do_make_bind _ _ _ = raise Fail "Mismatched long and short identifiers"
|
||||
|
||||
val b = do_make_bind short_name long_name (Binding.make (Long_Name.base_name nm, Position.none))
|
||||
|
||||
in b end;
|
||||
|
||||
fun get_new_facts old_thy facts =
|
||||
Facts.dest_static false [Global_Theory.facts_of old_thy] facts
|
||||
|> map (fn (nm, _) => `make_bind nm);
|
||||
let
|
||||
val space = Facts.space_of facts;
|
||||
in
|
||||
Facts.dest_static false [Global_Theory.facts_of old_thy] facts
|
||||
|> map (fn (nm, _) => `(make_bind space old_thy) nm)
|
||||
end
|
||||
|
||||
fun get_new_consts old_thy consts =
|
||||
let
|
||||
val new_consts = #constants (Consts.dest consts)
|
||||
|> map fst;
|
||||
|
||||
val space = #const_space (Consts.dest consts);
|
||||
|
||||
val consts =
|
||||
filter (fn nm => not (can (Consts.the_const (Sign.consts_of old_thy)) nm) andalso
|
||||
can (Consts.the_const consts) nm) new_consts
|
||||
|> map (fn nm => `make_bind nm);
|
||||
|> map (fn nm => `(make_bind space old_thy) nm);
|
||||
|
||||
in consts end;
|
||||
|
||||
fun get_new_types old_thy types =
|
||||
let
|
||||
val new_types = #types (Type.rep_tsig types);
|
||||
val space = Name_Space.space_of_table new_types;
|
||||
|
||||
val old_types = #types (Type.rep_tsig (Sign.tsig_of old_thy));
|
||||
|
||||
val types = (new_types
|
||||
|> Name_Space.fold_table (fn (nm, _) =>
|
||||
not (Name_Space.defined old_types nm) ? cons nm)) []
|
||||
|> map (fn nm => `make_bind nm);
|
||||
|> map (fn nm => `(make_bind space old_thy) nm);
|
||||
in types end;
|
||||
|
||||
fun add_qualified qual nm =
|
||||
|
|
@ -95,40 +115,46 @@ fun make_bind_local nm =
|
|||
val base = Long_Name.explode nm |> tl |> tl |> rev |> tl |> rev;
|
||||
in fold (Binding.qualify true) base (Binding.make (Long_Name.base_name nm, Position.none)) end;
|
||||
|
||||
fun set_global_qualify str thy =
|
||||
fun set_global_qualify (args : qualify_args) thy =
|
||||
let
|
||||
val str = #name args
|
||||
val _ = Locale.check thy (str, Position.none)
|
||||
val _ = case get_qualify thy of SOME _ => error "Already in a qualify block!" | NONE => ();
|
||||
|
||||
val thy' = Data.map (apfst (K (SOME (thy,args)))) thy;
|
||||
|
||||
in if #deep args then
|
||||
let
|
||||
|
||||
val facts =
|
||||
Facts.fold_static (fn (nm, _) => add_qualified str nm) (Global_Theory.facts_of thy) []
|
||||
|> map (`make_bind_local)
|
||||
|
||||
val consts = fold (fn (nm, _) => add_qualified str nm) (#constants (Consts.dest (Sign.consts_of thy))) []
|
||||
|> map (`make_bind_local)
|
||||
|> map (`make_bind_local)
|
||||
|
||||
val types =
|
||||
Name_Space.fold_table (fn (nm, _) => add_qualified str nm) (#types (Type.rep_tsig (Sign.tsig_of thy))) []
|
||||
|> map (`make_bind_local)
|
||||
|
||||
|
||||
val thy' = thy
|
||||
val thy'' = thy'
|
||||
|> map_facts_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) facts)
|
||||
|> map_consts_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) consts)
|
||||
|> map_types_of str (fold (fn (b, nm) => (Symtab.update (nm, b))) types)
|
||||
|
||||
val thy'' = thy'
|
||||
|> Data.map (apfst (K (SOME (thy,str))))
|
||||
|> fold (fn (nm, b) => Global_Theory.alias_fact b nm) (Symtab.dest (get_facts_of thy' str))
|
||||
|> fold (fn (nm, b) => Sign.const_alias b nm) (Symtab.dest (get_consts_of thy' str))
|
||||
|> fold (fn (nm, b) => Sign.type_alias b nm) (Symtab.dest (get_types_of thy' str))
|
||||
val thy''' = thy''
|
||||
|> fold (fn (nm, b) => Global_Theory.alias_fact b nm) (Symtab.dest (get_facts_of thy'' str))
|
||||
|> fold (fn (nm, b) => Sign.const_alias b nm) (Symtab.dest (get_consts_of thy'' str))
|
||||
|> fold (fn (nm, b) => Sign.type_alias b nm) (Symtab.dest (get_types_of thy'' str))
|
||||
|
||||
in thy'' end
|
||||
in thy''' end
|
||||
else thy'
|
||||
end
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword qualify} "begin global qualification"
|
||||
(Parse.name >>
|
||||
(fn str => Toplevel.theory (set_global_qualify str)));
|
||||
(Parse.name -- Args.mode "deep">>
|
||||
(fn (str, deep) => Toplevel.theory (set_global_qualify {name = str, deep = deep})));
|
||||
|
||||
fun syntax_alias global_alias local_alias b name =
|
||||
Local_Theory.declaration {syntax = true, pervasive = true} (fn phi =>
|
||||
|
|
@ -143,11 +169,13 @@ val type_alias = syntax_alias Sign.type_alias Proof_Context.type_alias;
|
|||
|
||||
fun end_global_qualify thy =
|
||||
let
|
||||
val (old_thy, nm) =
|
||||
val (old_thy, args) =
|
||||
case get_qualify thy of
|
||||
SOME x => x
|
||||
| NONE => error "Not in a global qualify"
|
||||
|
||||
val nm = #name args
|
||||
|
||||
val facts = get_new_facts old_thy (Global_Theory.facts_of thy);
|
||||
|
||||
val consts = get_new_consts old_thy (Sign.consts_of thy);
|
||||
|
|
@ -158,20 +186,25 @@ fun end_global_qualify thy =
|
|||
val thy' = thy
|
||||
|> map_facts_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) facts)
|
||||
|> map_consts_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) consts)
|
||||
|> map_types_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) types)
|
||||
|> (fn thy => fold (Global_Theory.hide_fact false o fst) (Symtab.dest (get_facts_of thy nm)) thy)
|
||||
|> (fn thy => fold (Sign.hide_const false o fst) (Symtab.dest (get_consts_of thy nm)) thy)
|
||||
|> (fn thy => fold (Sign.hide_type false o fst) (Symtab.dest (get_types_of thy nm)) thy)
|
||||
|> Data.map (apfst (K NONE))
|
||||
|> map_types_of nm (fold (fn (b, nm) => (Symtab.update (nm, b))) types);
|
||||
|
||||
val lthy = Named_Target.begin (nm, Position.none) thy';
|
||||
val facts' = (if #deep args then (map swap (Symtab.dest (get_facts_of thy' nm))) else facts);
|
||||
val consts' = (if #deep args then (map swap (Symtab.dest (get_consts_of thy' nm))) else consts);
|
||||
val types' = (if #deep args then (map swap (Symtab.dest (get_types_of thy' nm))) else types);
|
||||
|
||||
val thy'' = thy'
|
||||
|> (fn thy => fold (Global_Theory.hide_fact false o snd) facts' thy)
|
||||
|> (fn thy => fold (Sign.hide_const false o snd) consts' thy)
|
||||
|> (fn thy => fold (Sign.hide_type false o snd) types' thy);
|
||||
|
||||
val lthy = Named_Target.begin (nm, Position.none) thy'';
|
||||
|
||||
val lthy' = lthy
|
||||
|> fold (uncurry fact_alias o swap) (Symtab.dest (get_facts_of thy' nm))
|
||||
|> fold (uncurry const_alias o swap) (Symtab.dest (get_consts_of thy' nm))
|
||||
|> fold (uncurry type_alias o swap) (Symtab.dest (get_types_of thy' nm));
|
||||
|> fold (uncurry fact_alias) facts'
|
||||
|> fold (uncurry const_alias) consts'
|
||||
|> fold (uncurry type_alias) types';
|
||||
|
||||
in Local_Theory.exit_global lthy' end
|
||||
in Local_Theory.exit_global lthy' |> Data.map (apfst (K NONE)) end
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword end_qualify} "end global qualification"
|
||||
|
|
|
|||
|
|
@ -4,11 +4,10 @@
|
|||
*)
|
||||
|
||||
theory Unqualify
|
||||
imports Main
|
||||
imports Cardinality
|
||||
keywords "unqualify_facts" :: thy_decl and "unqualify_consts" :: thy_decl and "unqualify_types" :: thy_decl
|
||||
begin
|
||||
|
||||
|
||||
ML \<open>
|
||||
|
||||
local
|
||||
|
|
@ -28,6 +27,13 @@ fun make_binding b =
|
|||
val pos = Binding.pos_of b;
|
||||
in make_binding_raw (nm, pos) end
|
||||
|
||||
fun make_notation b =
|
||||
|
||||
let
|
||||
val str = Binding.name_of b
|
||||
|> String.translate(fn #"_" => "'_" | x => Char.toString x)
|
||||
|
||||
in str end
|
||||
|
||||
in
|
||||
|
||||
|
|
@ -70,21 +76,23 @@ val _ =
|
|||
val _ =
|
||||
Outer_Syntax.command @{command_keyword unqualify_consts} "unqualify consts"
|
||||
(Parse.opt_target -- Scan.option (Args.parens Parse.name) --
|
||||
Scan.repeat1 (Parse.position Parse.term) >> (fn ((target,qual),bs) =>
|
||||
Scan.repeat1 (Parse.position (Parse.const -- Scan.option (Parse.$$$ "::" |-- Parse.typ))) >> (fn ((target,qual),bs) =>
|
||||
Toplevel.local_theory NONE target (fn lthy =>
|
||||
let
|
||||
|
||||
val ts = map (`(Syntax.parse_term lthy o fst)) bs;
|
||||
fun read_const (t, T_in) =
|
||||
let
|
||||
val (nm, T) = dest_Const (Proof_Context.read_const {proper = true, strict = false} lthy t);
|
||||
val _ = case map_option (Syntax.read_typ lthy) T_in of
|
||||
SOME T' => (Syntax.check_term lthy (Const (nm, T')); ())
|
||||
| NONE => ()
|
||||
in (nm, T) end
|
||||
|
||||
fun get_const
|
||||
(( t as Const ("_type_constraint_", _) $
|
||||
(Const ("_type_constraint_", _) $
|
||||
Const (nm, _))), (_, pos)) = ((nm, pos), t)
|
||||
| get_const (t as (Const ("_type_constraint_", _) $
|
||||
Const (nm, _)), (_, pos)) = ((nm, pos), t)
|
||||
| get_const (t, (_,pos)) = error ("Not a constant or abbreviation: " ^ Syntax.string_of_term lthy t ^ Position.here pos)
|
||||
val ts = map (`( read_const o fst)) bs;
|
||||
|
||||
val ts' = map (apsnd (Syntax.check_term lthy) o apfst make_binding_raw o get_const) ts;
|
||||
fun get_const (((nm, T) , (_, pos))) = ((nm, pos), Const (nm, T))
|
||||
|
||||
val ts' = map (apfst make_binding_raw o get_const) ts;
|
||||
|
||||
val naming = Sign.naming_of (Proof_Context.theory_of lthy)
|
||||
|> the_default I (map_option Name_Space.mandatory_path qual);
|
||||
|
|
@ -93,42 +101,45 @@ val _ =
|
|||
let
|
||||
val thy' = Context.theory_map (Name_Space.map_naming (K naming)) thy;
|
||||
val export = Morphism.term (Local_Theory.standard_morphism lthy (Proof_Context.init_global thy));
|
||||
|
||||
|
||||
in
|
||||
fold (fn (b, t) =>
|
||||
let
|
||||
val b' = make_binding b;
|
||||
val b' = b
|
||||
|> make_binding;
|
||||
val t' = export t;
|
||||
|
||||
in
|
||||
Sign.add_abbrev Print_Mode.input (b', export t) #> snd
|
||||
Sign.add_abbrev Print_Mode.internal(b', t') #> snd #>
|
||||
Sign.notation true ("", false) [(t', Delimfix (make_notation b'))]
|
||||
end) ts' thy'
|
||||
end) lthy
|
||||
|
||||
in
|
||||
lthy'
|
||||
end)))
|
||||
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command @{command_keyword unqualify_types} "unqualify types"
|
||||
(Parse.opt_target -- Scan.option (Args.parens Parse.name) --
|
||||
Scan.repeat1 (Parse.position Parse.typ) >> (fn ((target,qual),bs) =>
|
||||
Scan.repeat1 (Parse.position Parse.type_const) >> (fn ((target,qual),bs) =>
|
||||
Toplevel.local_theory NONE target (fn lthy =>
|
||||
let
|
||||
|
||||
|
||||
fun err (T, pos) =
|
||||
error ("Not a defined type or type synonym: " ^ Syntax.string_of_typ lthy T ^ Position.here pos)
|
||||
|
||||
|
||||
val Ts = map (`(Syntax.parse_typ lthy o fst)) bs;
|
||||
val Ts = map (`(Proof_Context.read_type_name {proper = true, strict = false} lthy o fst)) bs;
|
||||
|
||||
fun get_type (T, (_, pos)) = case try dest_Type T of
|
||||
SOME (nm, Ts) => (if can dest_funT T then err (T,pos) else ((nm, pos), (T,Ts)))
|
||||
SOME (nm, Ts) => (if can dest_funT T then err (T,pos) else ((nm, pos), (nm,Ts)))
|
||||
| NONE => err (T,pos)
|
||||
|
||||
fun check_Ts (T,Ts) = (Syntax.check_typ lthy T,
|
||||
fold Term.add_tfree_namesT Ts [])
|
||||
|
||||
val Ts' = map (apsnd check_Ts o apfst make_binding_raw o get_type) Ts;
|
||||
val Ts' = map (apfst make_binding_raw o get_type) Ts;
|
||||
|
||||
val naming = Sign.naming_of (Proof_Context.theory_of lthy)
|
||||
|> the_default I (map_option Name_Space.mandatory_path qual);
|
||||
|
|
@ -137,11 +148,24 @@ val _ =
|
|||
let
|
||||
val thy' = Context.theory_map (Name_Space.map_naming (K naming)) thy;
|
||||
in
|
||||
fold (fn (b, (T,frees)) =>
|
||||
fold (fn (b, (nm,frees_raw)) =>
|
||||
let
|
||||
|
||||
val Ts = lthy
|
||||
|> Variable.invent_types (map (fn _ => Proof_Context.default_sort lthy ("'a",~1)) frees_raw)
|
||||
|> fst
|
||||
|> map TFree
|
||||
|
||||
val T = Type (nm, Ts)
|
||||
val frees = map (fst o dest_TFree) Ts
|
||||
val b' = make_binding b;
|
||||
|
||||
val str = make_notation b'
|
||||
|> fold (fn _ => fn s => "_ " ^ s) Ts
|
||||
|
||||
in
|
||||
Sign.add_type_abbrev lthy (b',frees, T)
|
||||
Sign.add_type_abbrev lthy (b',frees, T) #>
|
||||
Sign.type_notation true ("", false) [(T, Delimfix str)]
|
||||
end) Ts' thy'
|
||||
end) lthy
|
||||
|
||||
|
|
@ -150,7 +174,6 @@ val _ =
|
|||
end)))
|
||||
|
||||
end
|
||||
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
|
@ -0,0 +1,40 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory ArchBits_AI
|
||||
imports "../Invariants_AI"
|
||||
begin
|
||||
|
||||
context Arch begin
|
||||
|
||||
lemma invs_unique_table_caps[elim!]:
|
||||
"invs s \<Longrightarrow> unique_table_caps (arch_caps_of_state s)"
|
||||
by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
|
||||
|
||||
lemma invs_unique_refs[elim!]:
|
||||
"invs s \<Longrightarrow> unique_table_refs (arch_caps_of_state s)"
|
||||
by (simp add: invs_def valid_state_def valid_arch_caps_def)
|
||||
|
||||
|
||||
lemma invs_pd_caps:
|
||||
"invs s \<Longrightarrow> valid_table_caps s"
|
||||
by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
|
||||
|
||||
lemma invs_valid_vs_lookup[elim!]:
|
||||
"invs s \<Longrightarrow> valid_vs_lookup s "
|
||||
by (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
|
||||
|
||||
lemma pbfs_atleast_pageBits:
|
||||
"pageBits \<le> pageBitsForSize sz"
|
||||
by (cases sz) (auto simp: pageBits_def)
|
||||
|
||||
end
|
||||
|
||||
end
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -203,6 +203,7 @@ lemma throw_on_false_bcorres[wp]: "bcorres f f' \<Longrightarrow> bcorres (thro
|
|||
done
|
||||
|
||||
context Arch begin
|
||||
thm refl
|
||||
crunch (bcorres)bcorres[wp]: arch_finalise_cap truncate_state (simp: swp_def)
|
||||
unqualify_facts arch_finalise_cap_bcorres[wp]
|
||||
end
|
||||
|
|
|
|||
|
|
@ -9,7 +9,7 @@
|
|||
*)
|
||||
|
||||
theory Bits_AI
|
||||
imports Invariants_AI
|
||||
imports "./$L4V_ARCH/ArchBits_AI"
|
||||
begin
|
||||
|
||||
lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp'
|
||||
|
|
@ -107,8 +107,4 @@ lemma empty_on_failure_wp[wp]:
|
|||
apply assumption
|
||||
done
|
||||
|
||||
lemma pbfs_atleast_pageBits:
|
||||
"pageBits \<le> pageBitsForSize sz"
|
||||
by (cases sz) (auto simp: pageBits_def)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -0,0 +1,142 @@
|
|||
(*
|
||||
* Copyright 2014, General Dynamics C4 Systems
|
||||
*
|
||||
* This software may be distributed and modified according to the terms of
|
||||
* the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
* See "LICENSE_GPLv2.txt" for details.
|
||||
*
|
||||
* @TAG(GD_GPL)
|
||||
*)
|
||||
|
||||
theory InvariantsPre_AI
|
||||
imports LevityCatch_AI
|
||||
begin
|
||||
|
||||
context Arch begin
|
||||
|
||||
unqualify_types
|
||||
aa_type
|
||||
|
||||
unqualify_consts
|
||||
aa_type :: "arch_kernel_obj \<Rightarrow> aa_type"
|
||||
|
||||
end
|
||||
|
||||
section "Locale Setup"
|
||||
|
||||
locale pspace_update_eq' =
|
||||
fixes f :: "'z::state_ext state \<Rightarrow> 'c::state_ext state"
|
||||
assumes pspace: "kheap (f s) = kheap s"
|
||||
|
||||
locale Arch_pspace_update_eq = pspace_update_eq'
|
||||
sublocale Arch_pspace_update_eq \<subseteq> Arch .
|
||||
|
||||
locale pspace_update_eq = pspace_update_eq'
|
||||
|
||||
|
||||
locale arch_update_eq' =
|
||||
fixes f :: "'z::state_ext state \<Rightarrow> 'c::state_ext state"
|
||||
assumes arch: "arch_state (f s) = arch_state s"
|
||||
|
||||
locale Arch_arch_update_eq = arch_update_eq'
|
||||
sublocale Arch_arch_update_eq \<subseteq> Arch .
|
||||
|
||||
locale arch_update_eq = arch_update_eq'
|
||||
|
||||
locale arch_idle_update_eq_more =
|
||||
fixes f :: "'z::state_ext state \<Rightarrow> 'c::state_ext state"
|
||||
assumes idle: "idle_thread (f s) = idle_thread s"
|
||||
assumes irq: "interrupt_irq_node (f s) = interrupt_irq_node s"
|
||||
|
||||
locale Arch_arch_idle_update_eq = Arch_arch_update_eq + arch_idle_update_eq_more
|
||||
sublocale Arch_arch_idle_update_eq \<subseteq> Arch .
|
||||
|
||||
locale arch_idle_update_eq = arch_update_eq + arch_idle_update_eq_more
|
||||
|
||||
|
||||
locale Arch_p_arch_update_eq = Arch_pspace_update_eq + Arch_arch_update_eq
|
||||
sublocale Arch_p_arch_update_eq \<subseteq> Arch .
|
||||
|
||||
locale p_arch_update_eq = pspace_update_eq + arch_update_eq
|
||||
|
||||
locale Arch_p_arch_idle_update_eq = Arch_p_arch_update_eq + Arch_arch_idle_update_eq
|
||||
locale p_arch_idle_update_eq = p_arch_update_eq + arch_idle_update_eq
|
||||
|
||||
locale Arch_p_arch_idle_update_int_eq = Arch_p_arch_idle_update_eq + Arch_pspace_update_eq
|
||||
|
||||
section "Base definitions for Invariants"
|
||||
|
||||
definition
|
||||
obj_at :: "(Structures_A.kernel_object \<Rightarrow> bool) \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||
where
|
||||
"obj_at P ref s \<equiv> \<exists>ko. kheap s ref = Some ko \<and> P ko"
|
||||
|
||||
abbreviation
|
||||
"ko_at k \<equiv> obj_at (op = k)"
|
||||
|
||||
abbreviation
|
||||
aobj_at :: "(arch_kernel_obj \<Rightarrow> bool) \<Rightarrow> obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||
where
|
||||
"aobj_at P ref s \<equiv> obj_at (\<lambda>ob. case ob of ArchObj aob \<Rightarrow> P aob | _ \<Rightarrow> False) ref s"
|
||||
|
||||
lemma aobj_at_def:
|
||||
"aobj_at P ref = (\<lambda>s. \<exists>ako. kheap s ref = Some (ArchObj ako) \<and> P ako)"
|
||||
apply (rule ext)
|
||||
apply (clarsimp simp add: obj_at_def)
|
||||
apply (rule iffI)
|
||||
apply clarsimp
|
||||
apply (case_tac ko; clarsimp)
|
||||
apply clarsimp
|
||||
done
|
||||
|
||||
abbreviation
|
||||
"ako_at k \<equiv> aobj_at (op = k)"
|
||||
|
||||
abbreviation
|
||||
"atyp_at T \<equiv> aobj_at (\<lambda>ob. aa_type ob = T)"
|
||||
|
||||
lemma obj_atE:
|
||||
"\<lbrakk> obj_at P p s; \<And>ko. \<lbrakk> kheap s p = Some ko; P ko \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
|
||||
by (auto simp: obj_at_def)
|
||||
|
||||
lemma obj_at_weakenE:
|
||||
"\<lbrakk> obj_at P r s; \<And>ko. P ko \<Longrightarrow> P' ko \<rbrakk> \<Longrightarrow> obj_at P' r s"
|
||||
by (clarsimp simp: obj_at_def)
|
||||
|
||||
lemma ko_at_weakenE:
|
||||
"\<lbrakk> ko_at k ptr s; P k \<rbrakk> \<Longrightarrow> obj_at P ptr s"
|
||||
by (erule obj_at_weakenE, simp)
|
||||
|
||||
lemma aobj_atE:
|
||||
"\<lbrakk> aobj_at P p s; \<And>ko. \<lbrakk> kheap s p = Some (ArchObj ko); P ko \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
|
||||
by (auto simp: aobj_at_def)
|
||||
|
||||
lemma aobj_at_weakenE:
|
||||
"\<lbrakk> aobj_at P r s; \<And>ko. P ko \<Longrightarrow> P' ko \<rbrakk> \<Longrightarrow> aobj_at P' r s"
|
||||
by (clarsimp simp: aobj_at_def)
|
||||
|
||||
lemma ako_at_weakenE:
|
||||
"\<lbrakk> ako_at k ptr s; P k \<rbrakk> \<Longrightarrow> aobj_at P ptr s"
|
||||
by (erule aobj_at_weakenE, simp)
|
||||
|
||||
definition
|
||||
pspace_aligned :: "'z::state_ext state \<Rightarrow> bool"
|
||||
where
|
||||
"pspace_aligned s \<equiv>
|
||||
\<forall>x \<in> dom (kheap s). is_aligned x (obj_bits (the (kheap s x)))"
|
||||
|
||||
lemma pspace_alignedD [intro?]:
|
||||
"\<lbrakk> kheap s p = Some ko; pspace_aligned s \<rbrakk> \<Longrightarrow> is_aligned p (obj_bits ko)"
|
||||
unfolding pspace_aligned_def by (drule bspec, blast, simp)
|
||||
|
||||
text "objects don't overlap"
|
||||
definition
|
||||
pspace_distinct :: "'z::state_ext state \<Rightarrow> bool"
|
||||
where
|
||||
"pspace_distinct \<equiv>
|
||||
\<lambda>s. \<forall>x y ko ko'. kheap s x = Some ko \<and> kheap s y = Some ko' \<and> x \<noteq> y \<longrightarrow>
|
||||
{x .. x + (2 ^ obj_bits ko - 1)} \<inter>
|
||||
{y .. y + (2 ^ obj_bits ko' - 1)} = {}"
|
||||
|
||||
|
||||
end
|
||||
File diff suppressed because it is too large
Load Diff
|
|
@ -191,12 +191,12 @@ qualify ARM
|
|||
record arch_state =
|
||||
arm_globals_frame :: obj_ref
|
||||
arm_asid_table :: "word8 \<rightharpoonup> obj_ref"
|
||||
arm_hwasid_table :: "hw_asid \<rightharpoonup> asid"
|
||||
arm_next_asid :: hw_asid
|
||||
arm_asid_map :: "asid \<rightharpoonup> (hw_asid \<times> obj_ref)"
|
||||
arm_hwasid_table :: "ARM.hw_asid \<rightharpoonup> ARM.asid"
|
||||
arm_next_asid :: ARM.hw_asid
|
||||
arm_asid_map :: "ARM.asid \<rightharpoonup> (ARM.hw_asid \<times> obj_ref)"
|
||||
arm_global_pd :: obj_ref
|
||||
arm_global_pts :: "obj_ref list"
|
||||
arm_kernel_vspace :: arm_vspace_region_uses
|
||||
arm_kernel_vspace :: ARM.arm_vspace_region_uses
|
||||
|
||||
end_qualify
|
||||
|
||||
|
|
|
|||
|
|
@ -24,19 +24,19 @@ imports
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_update_cap_data :: data \<Rightarrow> arch_cap \<Rightarrow> cap"
|
||||
"arch_derive_cap :: arch_cap \<Rightarrow> (arch_cap,'z::state_ext) se_monad"
|
||||
"arch_finalise_cap :: arch_cap \<Rightarrow> bool \<Rightarrow> (cap,'z::state_ext) s_monad"
|
||||
"arch_is_physical :: arch_cap \<Rightarrow> bool"
|
||||
"arch_same_region_as :: arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
|
||||
"same_aobject_as :: arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
|
||||
"arch_has_recycle_rights :: arch_cap \<Rightarrow> bool"
|
||||
"arch_recycle_cap :: bool \<Rightarrow> arch_cap \<Rightarrow> (arch_cap,'z::state_ext) s_monad"
|
||||
arch_update_cap_data ::"data \<Rightarrow> arch_cap \<Rightarrow> cap"
|
||||
arch_derive_cap :: "arch_cap \<Rightarrow> (arch_cap,'z::state_ext) se_monad"
|
||||
arch_finalise_cap :: "arch_cap \<Rightarrow> bool \<Rightarrow> (cap,'z::state_ext) s_monad"
|
||||
arch_is_physical :: "arch_cap \<Rightarrow> bool"
|
||||
arch_same_region_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
|
||||
same_aobject_as :: "arch_cap \<Rightarrow> arch_cap \<Rightarrow> bool"
|
||||
arch_has_recycle_rights :: "arch_cap \<Rightarrow> bool"
|
||||
arch_recycle_cap :: "bool \<Rightarrow> arch_cap \<Rightarrow> (arch_cap,'z::state_ext) s_monad"
|
||||
|
||||
"msg_max_length :: nat"
|
||||
"cap_transfer_data_size :: nat"
|
||||
"msg_max_extra_caps :: nat"
|
||||
"msg_align_bits :: nat"
|
||||
msg_max_length :: "nat"
|
||||
cap_transfer_data_size :: "nat"
|
||||
msg_max_extra_caps :: "nat"
|
||||
msg_align_bits :: "nat"
|
||||
|
||||
|
||||
text {* This theory develops an abstract model of \emph{capability
|
||||
|
|
|
|||
|
|
@ -23,15 +23,15 @@ imports
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"ArchDefaultExtraRegisters :: arch_copy_register_sets"
|
||||
"check_valid_ipc_buffer :: vspace_ref \<Rightarrow> cap \<Rightarrow> (unit,'z::state_ext) se_monad"
|
||||
"is_valid_vtable_root :: cap \<Rightarrow> bool"
|
||||
"arch_decode_irq_control_invocation
|
||||
:: data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list \<Rightarrow> (arch_irq_control_invocation,'z::state_ext) se_monad"
|
||||
"arch_data_to_obj_type :: nat \<Rightarrow> aobject_type option"
|
||||
"arch_decode_invocation ::
|
||||
data \<Rightarrow> data list \<Rightarrow> cap_ref \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
|
||||
(arch_invocation,'z::state_ext) se_monad"
|
||||
ArchDefaultExtraRegisters :: "arch_copy_register_sets"
|
||||
check_valid_ipc_buffer :: "vspace_ref \<Rightarrow> cap \<Rightarrow> (unit,'z::state_ext) se_monad"
|
||||
is_valid_vtable_root :: "cap \<Rightarrow> bool"
|
||||
arch_decode_irq_control_invocation
|
||||
:: "data \<Rightarrow> data list \<Rightarrow> cslot_ptr \<Rightarrow> cap list \<Rightarrow> (arch_irq_control_invocation,'z::state_ext) se_monad"
|
||||
arch_data_to_obj_type :: "nat \<Rightarrow> aobject_type option"
|
||||
arch_decode_invocation ::
|
||||
"data \<Rightarrow> data list \<Rightarrow> cap_ref \<Rightarrow> cslot_ptr \<Rightarrow> arch_cap \<Rightarrow> (cap \<times> cslot_ptr) list \<Rightarrow>
|
||||
(arch_invocation,'z::state_ext) se_monad"
|
||||
|
||||
|
||||
text {*
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ imports Ipc_A
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_invoke_irq_control :: arch_irq_control_invocation \<Rightarrow> (unit,'z::state_ext) p_monad"
|
||||
arch_invoke_irq_control :: "arch_irq_control_invocation \<Rightarrow> (unit,'z::state_ext) p_monad"
|
||||
|
||||
|
||||
text {* Tests whether an IRQ identifier is in use. *}
|
||||
|
|
|
|||
|
|
@ -19,8 +19,8 @@ imports Tcb_A
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"set_message_info :: obj_ref \<Rightarrow> message_info \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
"lookup_ipc_buffer :: bool \<Rightarrow> obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad"
|
||||
set_message_info :: "obj_ref \<Rightarrow> message_info \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
lookup_ipc_buffer :: "bool \<Rightarrow> obj_ref \<Rightarrow> (obj_ref option,'z::state_ext) s_monad"
|
||||
|
||||
section {* Getting and setting the message info register. *}
|
||||
|
||||
|
|
|
|||
|
|
@ -34,29 +34,29 @@ unqualify_types
|
|||
|
||||
|
||||
unqualify_consts
|
||||
"nat_to_cref :: nat \<Rightarrow> nat \<Rightarrow> cap_ref"
|
||||
"msg_info_register :: register"
|
||||
"msg_registers :: register list"
|
||||
"cap_register :: register"
|
||||
"badge_register :: register"
|
||||
"frame_registers :: register list"
|
||||
"gp_registers :: register list"
|
||||
"exception_message :: register list"
|
||||
"syscall_message :: register list"
|
||||
nat_to_cref :: "nat \<Rightarrow> nat \<Rightarrow> cap_ref"
|
||||
msg_info_register :: "register"
|
||||
msg_registers :: "register list"
|
||||
cap_register :: "register"
|
||||
badge_register :: "register"
|
||||
frame_registers :: "register list"
|
||||
gp_registers :: "register list"
|
||||
exception_message :: "register list"
|
||||
syscall_message :: "register list"
|
||||
|
||||
"new_context :: user_context"
|
||||
"slot_bits :: nat"
|
||||
"oref_to_data :: obj_ref \<Rightarrow> data"
|
||||
"data_to_oref :: data \<Rightarrow> obj_ref"
|
||||
"vref_to_data :: vspace_ref \<Rightarrow> data"
|
||||
"data_to_vref :: data \<Rightarrow> vspace_ref"
|
||||
"nat_to_len :: nat \<Rightarrow> length_type"
|
||||
"data_to_nat :: data \<Rightarrow> nat"
|
||||
"data_to_16 :: data \<Rightarrow> 16 word"
|
||||
"data_to_cptr :: data \<Rightarrow> cap_ref"
|
||||
"data_offset_to_nat :: data_offset \<Rightarrow> nat"
|
||||
"combine_ntfn_badges :: data \<Rightarrow> data \<Rightarrow> data"
|
||||
"combine_ntfn_msgs :: data \<Rightarrow> data \<Rightarrow> data"
|
||||
new_context :: "user_context"
|
||||
slot_bits :: "nat"
|
||||
oref_to_data :: "obj_ref \<Rightarrow> data"
|
||||
data_to_oref :: "data \<Rightarrow> obj_ref"
|
||||
vref_to_data :: "vspace_ref \<Rightarrow> data"
|
||||
data_to_vref :: "data \<Rightarrow> vspace_ref"
|
||||
nat_to_len :: "nat \<Rightarrow> length_type"
|
||||
data_to_nat :: "data \<Rightarrow> nat"
|
||||
data_to_16 :: "data \<Rightarrow> 16 word"
|
||||
data_to_cptr :: "data \<Rightarrow> cap_ref"
|
||||
data_offset_to_nat :: "data_offset \<Rightarrow> nat"
|
||||
combine_ntfn_badges :: "data \<Rightarrow> data \<Rightarrow> data"
|
||||
combine_ntfn_msgs :: "data \<Rightarrow> data \<Rightarrow> data"
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -23,10 +23,10 @@ imports
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_default_cap :: aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> arch_cap"
|
||||
"default_arch_object :: aobject_type \<Rightarrow> nat \<Rightarrow> arch_kernel_obj"
|
||||
"init_arch_objects :: apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
|
||||
arch_default_cap :: "aobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> arch_cap"
|
||||
default_arch_object :: "aobject_type \<Rightarrow> nat \<Rightarrow> arch_kernel_obj"
|
||||
init_arch_objects :: "apiobject_type \<Rightarrow> obj_ref \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> obj_ref list \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
|
||||
|
||||
section "Creating Caps"
|
||||
|
||||
|
|
|
|||
|
|
@ -19,8 +19,8 @@ imports "./$L4V_ARCH/Arch_A"
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_switch_to_thread :: obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
"arch_switch_to_idle_thread :: (unit,'z::state_ext) s_monad"
|
||||
arch_switch_to_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
arch_switch_to_idle_thread :: "(unit,'z::state_ext) s_monad"
|
||||
|
||||
abbreviation
|
||||
"idle st \<equiv> st = Structures_A.IdleThreadState"
|
||||
|
|
|
|||
|
|
@ -31,13 +31,13 @@ unqualify_types (in Arch)
|
|||
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"acap_rights :: arch_cap \<Rightarrow> vm_rights"
|
||||
"acap_rights_update :: vm_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap"
|
||||
"arch_kobj_size :: arch_kernel_obj \<Rightarrow> nat"
|
||||
"arch_obj_size :: arch_cap \<Rightarrow> nat"
|
||||
"aobj_ref :: arch_cap \<rightharpoonup> obj_ref"
|
||||
"asid_high_bits :: nat"
|
||||
"asid_low_bits :: nat"
|
||||
acap_rights :: "arch_cap \<Rightarrow> vm_rights"
|
||||
acap_rights_update :: "vm_rights \<Rightarrow> arch_cap \<Rightarrow> arch_cap"
|
||||
arch_kobj_size :: "arch_kernel_obj \<Rightarrow> nat"
|
||||
arch_obj_size :: "arch_cap \<Rightarrow> nat"
|
||||
aobj_ref :: "arch_cap \<rightharpoonup> obj_ref"
|
||||
asid_high_bits :: "nat"
|
||||
asid_low_bits :: "nat"
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ imports
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_perform_invocation :: arch_invocation \<Rightarrow> (data list,'z::state_ext) p_monad"
|
||||
"handle_vm_fault :: obj_ref \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::state_ext) f_monad"
|
||||
arch_perform_invocation :: "arch_invocation \<Rightarrow> (data list,'z::state_ext) p_monad"
|
||||
handle_vm_fault :: "obj_ref \<Rightarrow> vmfault_type \<Rightarrow> (unit,'z::state_ext) f_monad"
|
||||
|
||||
|
||||
text{*
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ imports CSpace_A
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"in_user_frame :: obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||
in_user_frame :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool"
|
||||
|
||||
text {* Store or load a word at an offset from an IPC buffer. *}
|
||||
definition
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ imports TcbAcc_A Schedule_A
|
|||
begin
|
||||
|
||||
unqualify_consts (in Arch)
|
||||
"arch_activate_idle_thread :: obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
arch_activate_idle_thread :: "obj_ref \<Rightarrow> (unit,'z::state_ext) s_monad"
|
||||
|
||||
section "Activating Threads"
|
||||
|
||||
|
|
|
|||
|
|
@ -13,9 +13,7 @@ chapter "Architecture-specific Invocation Label Functions"
|
|||
theory ArchLabelFuns_H
|
||||
imports "../InvocationLabels_H"
|
||||
begin
|
||||
|
||||
context ARM begin
|
||||
|
||||
text {*
|
||||
Arch-specific functions on invocation labels
|
||||
*}
|
||||
|
|
@ -41,6 +39,7 @@ where
|
|||
| ArchInvocationLabel ARMPageUnify_Instruction \<Rightarrow> True
|
||||
| _ \<Rightarrow> False
|
||||
)"
|
||||
end
|
||||
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -14,13 +14,12 @@ theory InvocationLabels_H
|
|||
imports "$L4V_ARCH/ArchInvocationLabels_H"
|
||||
begin
|
||||
|
||||
text {*
|
||||
An enumeration of all system call labels.
|
||||
*}
|
||||
|
||||
unqualify_types (in Arch)
|
||||
arch_invocation_label
|
||||
|
||||
text {*
|
||||
An enumeration of all system call labels.
|
||||
*}
|
||||
|
||||
datatype invocation_label =
|
||||
InvalidInvocation
|
||||
|
|
@ -51,7 +50,7 @@ datatype invocation_label =
|
|||
| IRQClearIRQHandler
|
||||
| IRQSetMode
|
||||
| DomainSetSet
|
||||
| ArchInvocationLabel arch_invocation_label
|
||||
| ArchInvocationLabel ArchInvocationLabels_H.ARM.arch_invocation_label
|
||||
|
||||
(* invocation_label instance proofs *)
|
||||
(*<*)
|
||||
|
|
|
|||
|
|
@ -15,8 +15,10 @@ imports
|
|||
"../../../lib/Enumeration"
|
||||
"../../../lib/WordSetup"
|
||||
"../../../lib/wp/NonDetMonad"
|
||||
Setup_Locale
|
||||
Platform
|
||||
begin
|
||||
qualify ARM (deep)
|
||||
|
||||
(* !!! Generated File !!! Skeleton in ../haskell-translator/ARMMachineTypes.thy *)
|
||||
|
||||
|
|
@ -112,4 +114,5 @@ definition
|
|||
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs ONLY HardwareASID VMFaultType VMPageSize pageBits pageBitsForSize
|
||||
#INCLUDE_HASKELL SEL4/Machine/Hardware/ARM.lhs instanceproofs ONLY HardwareASID VMFaultType VMPageSize
|
||||
|
||||
end_qualify
|
||||
end
|
||||
|
|
|
|||
|
|
@ -11,14 +11,14 @@
|
|||
chapter "Architecture-specific Invocation Labels"
|
||||
|
||||
theory ArchInvocationLabels_H
|
||||
imports "../../../lib/Enumeration"
|
||||
imports "../../../lib/Enumeration" "../../machine/ARM/Setup_Locale"
|
||||
begin
|
||||
|
||||
qualify ARM
|
||||
text {*
|
||||
An enumeration of arch-specific system call labels.
|
||||
*}
|
||||
|
||||
#INCLUDE_HASKELL SEL4/API/InvocationLabels/ARM.lhs ONLY ArchInvocationLabel
|
||||
#INCLUDE_HASKELL SEL4/API/InvocationLabels/ARM.lhs instanceproofs ONLY ArchInvocationLabel
|
||||
|
||||
end_qualify
|
||||
end
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ chapter "Architecture-specific Invocation Label Functions"
|
|||
theory ArchLabelFuns_H
|
||||
imports "../InvocationLabels_H"
|
||||
begin
|
||||
|
||||
context ARM begin
|
||||
text {*
|
||||
Arch-specific functions on invocation labels
|
||||
*}
|
||||
|
|
@ -21,3 +21,4 @@ text {*
|
|||
#INCLUDE_HASKELL SEL4/API/Invocation/ARM.lhs ONLY isPDFlushLabel isPageFlushLabel
|
||||
|
||||
end
|
||||
end
|
||||
|
|
|
|||
|
|
@ -11,7 +11,7 @@
|
|||
chapter "Kernel Events"
|
||||
|
||||
theory Event_H
|
||||
imports "../machine/$L4V_ARCH/MachineTypes"
|
||||
imports "../machine/MachineExports"
|
||||
begin
|
||||
|
||||
text {*
|
||||
|
|
|
|||
|
|
@ -14,11 +14,14 @@ theory InvocationLabels_H
|
|||
imports "$L4V_ARCH/ArchInvocationLabels_H"
|
||||
begin
|
||||
|
||||
unqualify_types (in Arch)
|
||||
arch_invocation_label
|
||||
|
||||
text {*
|
||||
An enumeration of all system call labels.
|
||||
*}
|
||||
|
||||
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ArchLabels=ArchInvocationLabels_H ONLY InvocationLabel
|
||||
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs ArchLabels=ArchInvocationLabels_H.ARM ONLY InvocationLabel
|
||||
#INCLUDE_HASKELL SEL4/API/InvocationLabels.lhs instanceproofs
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
Built from git repo at /Users/dmatichuk/verification-x64/seL4/haskell by dmatichuk
|
||||
Built from git repo at /Users/dmatichuk/verification-archsplit/seL4/haskell by dmatichuk
|
||||
|
||||
Generated from changeset:
|
||||
3238a2f Merge commit 'e11bb32f7858a23403929cf3a5be04ab75a2991f' into arch_split
|
||||
e35adcb remove mentions of ARM from arch-independent invocation labels
|
||||
|
||||
|
|
|
|||
|
|
@ -35,7 +35,7 @@ text {*
|
|||
*}
|
||||
|
||||
|
||||
qualify ARM
|
||||
qualify ARM (deep)
|
||||
|
||||
section "The Operations"
|
||||
|
||||
|
|
|
|||
|
|
@ -18,8 +18,7 @@ imports
|
|||
Setup_Locale
|
||||
Platform
|
||||
begin
|
||||
|
||||
qualify ARM
|
||||
qualify ARM (deep)
|
||||
|
||||
(* !!! Generated File !!! Skeleton in ../haskell-translator/ARMMachineTypes.thy *)
|
||||
|
||||
|
|
@ -52,21 +51,16 @@ datatype register =
|
|||
|
||||
type_synonym machine_word = "word32"
|
||||
|
||||
|
||||
|
||||
consts
|
||||
initContext :: "(register * machine_word) list"
|
||||
|
||||
consts
|
||||
sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
|
||||
|
||||
|
||||
(*<*)
|
||||
(* register instance proofs *)
|
||||
(*<*)
|
||||
instantiation register :: enum begin
|
||||
|
||||
definition
|
||||
enum_register: "enum_class.enum \<equiv>
|
||||
[
|
||||
|
|
@ -189,6 +183,13 @@ record
|
|||
|
||||
consts irq_oracle :: "nat \<Rightarrow> word8"
|
||||
|
||||
text {*
|
||||
The machine monad is used for operations on the state defined above.
|
||||
*}
|
||||
type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
|
||||
|
||||
translations
|
||||
(type) "'c machine_monad" <= (type) "(machine_state, 'c) nondet_monad"
|
||||
|
||||
text {*
|
||||
After kernel initialisation all IRQs are masked.
|
||||
|
|
@ -313,6 +314,7 @@ instance by (intro_classes, simp add: enum_alt_vmpage_size)
|
|||
end
|
||||
|
||||
(*>*)
|
||||
end_qualify
|
||||
|
||||
|
||||
end_qualify
|
||||
end
|
||||
|
|
|
|||
|
|
@ -21,27 +21,27 @@ unqualify_types
|
|||
irq
|
||||
|
||||
unqualify_consts
|
||||
"getActiveIRQ :: (irq option) machine_monad"
|
||||
"maskInterrupt :: bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
|
||||
"freeMemory :: machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
"loadWord :: machine_word \<Rightarrow> machine_word machine_monad"
|
||||
"storeWord :: machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
"storeWordVM :: machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
"setNextPC :: machine_word \<Rightarrow> unit user_monad"
|
||||
"getRestartPC :: machine_word user_monad"
|
||||
"setRegister :: register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
"getRegister :: register \<Rightarrow> machine_word user_monad"
|
||||
"sanitiseRegister :: register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
"initContext :: (register * machine_word) list"
|
||||
"exceptionMessage :: register list"
|
||||
"syscallMessage :: register list"
|
||||
"gpRegisters :: register list"
|
||||
"frameRegisters :: register list"
|
||||
"setInterruptMode :: irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
|
||||
"ackInterrupt :: irq \<Rightarrow> unit machine_monad"
|
||||
"resetTimer :: unit machine_monad"
|
||||
"maxIRQ :: irq"
|
||||
"minIRQ :: irq"
|
||||
getActiveIRQ :: "(irq option) machine_monad"
|
||||
maskInterrupt :: "bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
|
||||
freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
|
||||
loadWord :: "machine_word \<Rightarrow> machine_word machine_monad"
|
||||
storeWord :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
|
||||
setNextPC :: "machine_word \<Rightarrow> unit user_monad"
|
||||
getRestartPC :: "machine_word user_monad"
|
||||
setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
|
||||
getRegister :: "register \<Rightarrow> machine_word user_monad"
|
||||
sanitiseRegister :: "register \<Rightarrow> machine_word \<Rightarrow> machine_word"
|
||||
initContext :: "(register * machine_word) list"
|
||||
exceptionMessage :: "register list"
|
||||
syscallMessage :: "register list"
|
||||
gpRegisters :: "register list"
|
||||
frameRegisters :: "register list"
|
||||
setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
|
||||
ackInterrupt :: "irq \<Rightarrow> unit machine_monad"
|
||||
resetTimer :: "unit machine_monad"
|
||||
maxIRQ :: "irq"
|
||||
minIRQ :: "irq"
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -14,14 +14,17 @@ imports "./$L4V_ARCH/MachineTypes"
|
|||
begin
|
||||
|
||||
context Arch begin
|
||||
|
||||
|
||||
unqualify_types
|
||||
machine_state
|
||||
machine_state_rest
|
||||
|
||||
|
||||
unqualify_consts
|
||||
"machine_state_rest :: machine_state \<Rightarrow> machine_state_rest"
|
||||
"machine_state_rest_update :: (machine_state_rest \<Rightarrow> machine_state_rest) \<Rightarrow> machine_state \<Rightarrow> machine_state"
|
||||
underlying_memory :: "machine_state \<Rightarrow> machine_word \<Rightarrow> word8"
|
||||
irq_masks :: "machine_state \<Rightarrow> irq \<Rightarrow> bool"
|
||||
machine_state_rest :: "machine_state \<Rightarrow> machine_state_rest"
|
||||
machine_state_rest_update :: "(machine_state_rest \<Rightarrow> machine_state_rest) \<Rightarrow> machine_state \<Rightarrow> machine_state"
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -31,7 +34,7 @@ text {*
|
|||
type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
|
||||
|
||||
translations
|
||||
(type) "'c machine_monad" <= (type) "(machine_state, 'c) nondet_monad"
|
||||
(type) "'c machine_monad" <= (type) "machine_state \<Rightarrow> ('c \<times> machine_state) set \<times> bool"
|
||||
|
||||
type_synonym 'a machine_rest_monad = "(machine_state_rest, 'a) nondet_monad"
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue