1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6(*<*) 7(* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *) 8theory GenDataportSystem 9imports UserDataport 10begin 11(*>*) 12 13subsection \<open>\label{ssec:dataportsys}Generated System Theory\<close> 14 15subsubsection \<open>\label{sssec:dataportsystypes}Types\<close> 16text \<open> 17 At the system level we have the now familiar generated types. 18\<close> 19 20type_synonym component = "(channel, component_state) comp" 21 22type_synonym lstate = "component_state local_state" 23 24type_synonym gstate = "(inst, channel, component_state) global_state" 25 26subsubsection \<open>\label{sssec:dataportsysuntrusted}Untrusted Components\<close> 27text \<open> 28 A definition is generated for the untrusted execution of the component, 29 @{term DataportTest}. In this definition there are two interfaces the 30 component can send and receive on, but the other details of the definition 31 are identical to the previous examples. 32\<close> 33 34definition 35 DataportTest_untrusted :: "(DataportTest_channel \<Rightarrow> channel) \<Rightarrow> component" 36where 37 "DataportTest_untrusted ch \<equiv> 38 LOOP ( 39 UserStep 40 \<squnion> ArbitraryRequest (ch DataportTest_d2) 41 \<squnion> ArbitraryResponse (ch DataportTest_d2) 42 \<squnion> ArbitraryRequest (ch DataportTest_d1) 43 \<squnion> ArbitraryResponse (ch DataportTest_d1))" 44 45subsubsection \<open>\label{sssec:dataportsysinst}Component Instances\<close> 46text \<open> 47 The definitions for untrusted execution of the two component instances are 48 generated by partially applying the untrusted definition of 49 @{term DataportTest} with different functions mapping its interfaces to 50 connections. In this way, two processes are formed that have identical local 51 behaviour, but have different effects when they perform communication 52 actions. 53\<close> 54 55definition 56 comp2_untrusted :: component 57where 58 "comp2_untrusted \<equiv> 59 DataportTest_untrusted (\<lambda>c. case c of DataportTest_d1 \<Rightarrow> simple2 60 | DataportTest_d2 \<Rightarrow> simple1)" 61 62definition 63 comp1_untrusted :: component 64where 65 "comp1_untrusted \<equiv> 66 DataportTest_untrusted (\<lambda>c. case c of DataportTest_d2 \<Rightarrow> simple2 67 | DataportTest_d1 \<Rightarrow> simple1)" 68 69subsubsection \<open>\label{ssecdataportsysmem}Shared Memory Components\<close> 70text \<open> 71 A component instance is generated for each connection involving a dataport, 72 as mentioned previously. As for events, the user is given no opportunity to 73 provide trusted definitions for these instances because we can automatically 74 generate their precise behaviour without ambiguity. 75\<close> 76 77definition 78 simple2\<^sub>d_instance :: component 79where 80 "simple2\<^sub>d_instance \<equiv> Buf\<^sub>d (\<lambda>_. simple2)" 81 82definition 83 simple1\<^sub>d_instance :: component 84where 85 "simple1\<^sub>d_instance \<equiv> Buf\<^sub>d (\<lambda>_. simple1)" 86 87subsubsection \<open>\label{sssec:dataportsysgs}Initial State\<close> 88text \<open> 89 The initial state for this system includes cases for the introduced shared 90 memory components, using the definitions presented above. Both begin in the 91 common initial memory state containing the empty map. 92\<close> 93 94definition 95 gs\<^sub>0 :: gstate 96where 97 "gs\<^sub>0 p \<equiv> case trusted p of Some s \<Rightarrow> Some s | _ \<Rightarrow> 98 (case p of comp2 \<Rightarrow> Some (comp2_untrusted, Component init_component_state) 99 | comp1 \<Rightarrow> Some (comp1_untrusted, Component init_component_state) 100 | simple2\<^sub>d \<Rightarrow> Some (simple2\<^sub>d_instance, init_memory_state) 101 | simple1\<^sub>d \<Rightarrow> Some (simple1\<^sub>d_instance, init_memory_state))" 102 103(*<*) 104end 105(*>*) 106