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