1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6chapter \<open>\label{h:userstubs}Component Behaviour\<close>
7
8(*<*)
9theory UserStubs
10imports Types
11begin
12(*>*)
13
14text \<open>
15  The definitions of a full system are expected to come from a combination of
16  generated and user-provided theories. The \camkes generator utility creates a
17  base theory using the types and definitions previously discussed that defines
18  primitive operations of a specific system. The user is then expected to
19  provide a theory that defines the trusted components of the system, building
20  on top of these definitions. The generator also produces a theory describing
21  the system as a whole that builds on top of the user's intermediate theory.
22  Final reasoning about system properties is expected to be done in another
23  theory building on this generated system theory.
24
25  These theory dependencies are depicted in \autoref{fig:thydeps}.
26
27  \begin{figure}[h]
28    \begin{center}
29      \includegraphics[width=300px]{imgs/thydeps}
30    \end{center}
31    \caption{\label{fig:thydeps}Theorem dependencies}
32  \end{figure}
33
34  The remainder of this section describes the default contents of the intermediate
35  user theory if none other is provided.
36\<close>
37
38text \<open>
39  When using the generated theories, the user is expected to provide the
40  following type instantiations and definitions:
41
42  \begin{itemize}
43    \item A type for @{term component_state} representing the local state that
44      should be represented for each component;
45    \item An initial @{term component_state} for untrusted components to be
46      given on startup; and
47    \item A (possibly empty) mapping from component instance identifiers to
48      trusted component definitions.
49  \end{itemize}
50
51  If parts of this are unnecessary for the user's aims, then they can import
52  the default implementations described below.
53\<close>
54
55subsection \<open>\label{ssec:componentstate}Local Component State\<close>
56text \<open>
57  The user should specify a type for @{term component_state} if they want to
58  reason about the behaviour of user-provided code. If not, then the type
59  @{term unit} captures the irrelevance of this.
60\<close>
61type_synonym component_state = unit
62
63text \<open>
64  The generated theories need to be
65  provided with a default value for the local state type. This is used as the
66  initial
67  local state for untrusted components. This definition must be visible even if
68  there are no untrusted components in the system, although in this case it
69  will not be used.
70\<close>
71definition
72  init_component_state :: component_state
73where
74  "init_component_state \<equiv> ()"
75
76subsection \<open>\label{ssec:untrusted}Untrusted Components\<close>
77text \<open>
78  Any component which does not have its definition supplied will be given a
79  generated definition that allows it to non-deterministically perform any
80  local operation or send or receive anything on any channel available to it.
81  Without providing definitions of any trusted components it will generally be
82  impossible to reason about anything beyond architectural properties of the
83  system.
84\<close>
85
86subsection \<open>\label{ssec:trusted}Trusted Components\<close>
87text \<open>
88  Trusted components should be given a defined program text (type
89  @{term component}) and an initial local state. The user should provide a
90  definition of @{term trusted}, a mapping from component instances to a pair
91  of component and initial local state. Any instance not present in the mapping
92  will be assigned the broad definition described in the previous paragraph.
93
94  The default mapping is as defined below, empty, causing all instances to fall
95  back on their untrusted definitions. The types @{term component} and
96  @{term lstate} are overridden in the generated theories and do not need to be
97  provided here or by the user, but they make the definition of @{term trusted}
98  more readable.
99\<close>
100
101type_synonym ('channel) component = "('channel, component_state) comp"
102
103type_synonym lstate = "component_state local_state"
104
105definition
106  trusted :: "('inst, ('channel component \<times> lstate)) map"
107where
108  "trusted \<equiv> Map.empty"
109
110(*<*)
111end
112(*>*)
113