1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Utilities for the machine level which are not machine-dependent.
9*)
10
11chapter "Machine Accessor Functions"
12
13theory MiscMachine_A
14imports Machine_A "ExecSpec.MachineExports"
15begin
16
17context begin interpretation Arch .
18
19requalify_types
20  user_context
21  user_monad
22  register
23  data
24  obj_ref
25  asid_high_len
26  asid_high_index
27  asid_low_len
28  asid_low_index
29  asid_len
30  asid_rep_len
31  asid
32  cap_ref
33  length_type
34  vspace_ref
35
36requalify_consts
37  nat_to_cref
38  msg_info_register
39  msg_registers
40  cap_register
41  badge_register
42  frame_registers
43  gp_registers
44  exception_message
45  syscall_message
46  new_context
47  slot_bits
48  oref_to_data
49  data_to_oref
50  vref_to_data
51  data_to_vref
52  nat_to_len
53  data_to_nat
54  data_to_16
55  data_to_cptr
56  combine_ntfn_badges
57
58end
59
60(* Needs to be done here after plain type names are exported *)
61translations
62  (type) "'a user_monad" <= (type) "user_context \<Rightarrow> ('a \<times> user_context) set \<times> bool"
63
64definition
65  asid_high_bits :: nat
66where
67  "asid_high_bits \<equiv> LENGTH(asid_high_len)"
68
69definition
70  asid_low_bits :: nat
71where
72  "asid_low_bits \<equiv> LENGTH(asid_low_len)"
73
74definition
75  asid_bits :: nat
76where
77  "asid_bits \<equiv> LENGTH(asid_len)"
78
79lemmas asid_bits_defs =
80  asid_bits_def asid_high_bits_def asid_low_bits_def
81
82(* Sanity checks. *)
83lemma asid_bits_len_checks:
84  "asid_bits = asid_high_bits + asid_low_bits"
85  "asid_bits \<le> LENGTH(asid_rep_len)"
86  unfolding asid_bits_defs by auto
87
88end
89