1/*#
2 *# Copyright 2017, Data61
3 *# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 *# ABN 41 687 119 230.
5 *#
6 *# This software may be distributed and modified according to the terms of
7 *# the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 *# See "LICENSE_BSD2.txt" for details.
9 *#
10 *# @TAG(DATA61_BSD)
11 #*/
12
13(* /*? macros.generated_file_notice() ?*/ *)
14
15/*? macros.check_isabelle_outfile(
16        '%s_Arch_Spec' % options.verification_base_name, outfile_name) ?*/
17
18theory "/*? options.verification_base_name ?*/_Arch_Spec" imports
19  "CamkesAdlSpec.Types_CAMKES"
20  "CamkesAdlSpec.Library_CAMKES"
21  "CamkesAdlSpec.Wellformed_CAMKES"
22  "Lib.Qualify"
23begin
24
25/*- set group_labels = macros.integrity_group_labels(me.composition, me.configuration) -*/
26
27(*
28 * We restrict the scope of all names to a locale with the same name
29 * as our theory. This ensures that entity names from the CAmkES
30 * assembly won't overlap with names we use elsewhere.
31 *)
32
33locale /*? options.verification_base_name ?*/_Arch_Spec
34begin
35
36/*- macro camkes_type(type) -*/
37    /*- if type == 'int' -*/
38        Primitive (Numerical Integer)
39    /*- elif type == 'unsigned int' -*/
40        Primitive (Numerical UnsignedInteger)
41    /*- elif type == 'real' -*/
42        Primitive (Numerical Real)
43    /*- elif type == 'char' -*/
44        Primitive (Textual char)
45    /*- elif type == 'character' -*/
46        Primitive (Textual Character)
47    /*- elif type == 'boolean' -*/
48        Primitive (Numerical Boolean)
49    /*- elif type == 'string' -*/
50        Primitive (Textual String)
51    /*- else -*/
52        CType ''/*? type ?*/''
53    /*- endif -*/
54/*- endmacro -*/
55
56/*- macro param_type(param) -*/
57    /*- if param.array -*/
58        Array (SizedArray
59        /*- if type == 'int' -*/
60            (Numerical Integer)
61        /*- elif type == 'unsigned int' -*/
62            (Numerical UnsignedInteger)
63        /*- elif type == 'real' -*/
64            (Numerical Real)
65        /*- elif type == 'char' -*/
66            (Textual char)
67        /*- elif type == 'character' -*/
68            (Textual Character)
69        /*- elif type == 'boolean' -*/
70            (Numerical Boolean)
71        /*- else -*/
72            /*? raise(TemplateError('unsupported type: array of %s' % param.type)) ?*/
73        /*- endif -*/
74    /*- else -*/
75    /*- endif -*/
76    /*? 'Array (SizedArray (' if param.array else '' ?*/
77    /*? camkes_type(param.type) ?*/
78    /*? '))' if param.array else '' ?*/
79/*- endmacro -*/
80
81/*- if hasattr(me, 'name') and me.name is not none -*/
82    /*- set assembly = me.name -*/
83/*- else -*/
84    /*- set assembly = 'assembly\'' -*/
85/*- endif -*/
86
87/*- if hasattr(me.composition, 'name') and me.composition.name is not none -*/
88    /*- set composition = me.composition.name -*/
89/*- else -*/
90    /*- set composition = 'composition\'' -*/
91/*- endif -*/
92
93/*- if me.configuration is not none and hasattr(me.configuration, 'name') and me.configuration.name is not none -*/
94    /*- set configuration = me.configuration.name -*/
95/*- else -*/
96    /*- set configuration = 'configuration\'' -*/
97/*- endif -*/
98
99(* Connector types *)
100/*- for i in uniq(map(lambda('x: x.type'), me.composition.connections)) -*/
101definition
102    /*? isabelle_connector(i.name) ?*/ :: connector
103where[wellformed_CAMKES_simps]:
104    "/*? isabelle_connector(i.name) ?*/ \<equiv> /*-
105  if i.get_attribute('isabelle_connector_spec') -*//*? i.get_attribute('isabelle_connector_spec').default ?*//*-
106  else -*/\<lparr>
107        connector_type = /*? 'HardwareConnector' if i.from_hardware or i.to_hardware else 'NativeConnector' ?*/,
108        connector_interface =
109          /*- if i.from_type == 'Dataport' -*/
110            DataportInterface,
111          /*- elif i.from_type == 'Event' -*/
112            EventInterface,
113          /*- elif i.from_type == 'Procedure' -*/
114            RPCInterface,
115          /*- endif -*/
116        connector_access = \<lparr>
117            access_from_to   = undefined ''TODO /*? isabelle_connector(i.name) ?*/.access_from_to'',
118            access_to_from   = undefined ''TODO /*? isabelle_connector(i.name) ?*/.access_to_from'',
119            access_from_conn = undefined ''TODO /*? isabelle_connector(i.name) ?*/.access_from_conn'',
120            access_to_conn   = undefined ''TODO /*? isabelle_connector(i.name) ?*/.access_to_conn''
121        \<rparr> \<rparr>/*-
122  endif -*/"
123lemma[wellformed_CAMKES_simps]: "wellformed_connector /*? isabelle_connector(i.name) ?*/"
124  by (auto simp: wellformed_CAMKES_simps /*? isabelle_connector(i.name) ?*/_def)
125/*- endfor -*/
126
127(* Procedure interfaces *)
128/*- for i in uniq(map(lambda('x: x.type'), flatMap(lambda('x: x.type.uses + x.type.provides'), me.composition.instances))) -*/
129definition
130    /*? isabelle_procedure(i.name) ?*/ :: procedure
131where[wellformed_CAMKES_simps]:
132    "/*? isabelle_procedure(i.name) ?*/ \<equiv>
133    /*- for m in i.methods -*/
134        \<lparr> m_return_type =
135        /*- if m.return_type -*/
136            Some (/*? camkes_type(m.return_type) ?*/)
137        /*- else -*/
138            None
139        /*- endif -*/
140        , m_name = ''/*? m.name ?*/'',
141        m_parameters =
142        /*- for p in m.parameters -*/
143            \<lparr> p_type = /*? param_type(p) ?*/,
144            p_direction =
145            /*- if p.direction in ['in', 'refin'] -*/
146                InParameter
147            /*- elif p.direction == 'out' -*/
148                OutParameter
149            /*- else -*/
150                /*? assert(p.direction == 'inout') ?*/
151                InOutParameter
152            /*- endif -*/
153            , p_name = ''/*? p.name ?*/'' \<rparr> #
154        /*- endfor -*/
155        [] \<rparr> #
156    /*- endfor -*/
157    []"
158
159lemma wf_/*? isabelle_procedure(i.name) ?*/: "wellformed_procedure /*? isabelle_procedure(i.name) ?*/"
160  by (simp add: wellformed_CAMKES_simps)
161/*- endfor -*/
162
163(* Event interfaces *)
164/*- for index, i in enumerate(uniq(map(lambda('x: x.type'), flatMap(lambda('x: x.type.emits + x.type.consumes'), me.composition.instances)))) -*/
165definition
166    /*? isabelle_event(i) ?*/ :: event
167where[wellformed_CAMKES_simps]:
168    "/*? isabelle_event(i) ?*/ \<equiv> /*? index ?*/"
169
170lemma wf_/*? isabelle_event(i) ?*/: "wellformed_event /*? isabelle_event(i) ?*/"
171  by (simp add: wellformed_CAMKES_simps)
172/*- endfor -*/
173
174(* Dataport interfaces *)
175
176/*- for i in uniq(map(lambda('x: x.type'), flatMap(lambda('x: x.type.dataports'), me.composition.instances))) -*/
177definition
178    /*? isabelle_dataport(i) ?*/ :: dataport
179where[wellformed_CAMKES_simps]:
180    "/*? isabelle_dataport(i) ?*/ \<equiv> Some ''/*? i ?*/''"
181
182lemma wf_/*? isabelle_dataport(i) ?*/: "wellformed_dataport /*? isabelle_dataport(i) ?*/"
183  by (simp add: wellformed_CAMKES_simps)
184/*- endfor -*/
185
186/*- for c in uniq(map(lambda('x: x.type'), me.composition.instances)) -*/
187definition
188    /*? isabelle_instance(c.name) ?*/ :: component
189where[wellformed_CAMKES_simps]:
190    "/*? isabelle_instance(c.name) ?*/ \<equiv> \<lparr>
191        control =
192        /*- if c.control -*/
193            True
194        /*- else -*/
195            False
196        /*- endif -*/
197        ,
198        hardware =
199        /*- if c.hardware -*/
200            True
201        /*- else -*/
202            False
203        /*- endif -*/
204        ,
205        requires =
206        /*- for i in c.uses -*//*-
207                if c.interface_is_exported(i.name) -*/
208            \<comment> \<open>Exported interface/*- endif -*/
209            (''/*? i.name ?*/'', (/*? 'InterfaceOptional' if hasattr(i, 'optional') and i.optional else 'InterfaceRequired'
210                                  ?*/, /*? isabelle_procedure(i.type.name) ?*/)) #/*-
211                if c.interface_is_exported(i.name) -*/
212            \<close>/*- endif -*/
213        /*- endfor -*/
214        [],
215        provides =
216        /*- for i in c.provides -*//*-
217                if c.interface_is_exported(i.name) -*/
218            \<comment> \<open>Exported interface/*- endif -*/
219            (''/*? i.name ?*/'', /*? isabelle_procedure(i.type.name) ?*/) #/*-
220                if c.interface_is_exported(i.name) -*/
221            \<close>/*- endif -*/
222        /*- endfor -*/
223        [],
224        dataports =
225        /*- for i in c.dataports -*//*-
226                if c.interface_is_exported(i) -*/
227            \<comment> \<open>Exported interface/*- endif -*/
228            (''/*? i ?*/'', /*? isabelle_dataport(i.type) ?*/) #/*-
229                if c.interface_is_exported(i) -*/
230            \<close>/*- endif -*/
231        /*- endfor -*/
232        [],
233        emits =
234        /*- for i in c.emits -*//*-
235                if c.interface_is_exported(i) -*/
236            \<comment> \<open>Exported interface/*- endif -*/
237            (''/*? i ?*/'', /*? isabelle_event(i.type) ?*/) #/*-
238                if c.interface_is_exported(i) -*/
239            \<close>/*- endif -*/
240        /*- endfor -*/
241        [],
242        consumes =
243        /*- for i in c.consumes -*//*-
244                if c.interface_is_exported(i) -*/
245            \<comment> \<open>Exported interface/*- endif -*/
246            (''/*? i ?*/'', (/*? 'InterfaceOptional' if hasattr(i, 'optional') and i.optional else 'InterfaceRequired'
247                             ?*/, /*? isabelle_event(i.type) ?*/)) #/*-
248                if c.interface_is_exported(i) -*/
249            \<close>/*- endif -*/
250        /*- endfor -*/
251        [],
252        attributes =
253        /*- for a in c.attributes -*/
254            (''/*? a.name ?*/'', /*? camkes_type(a.type) ?*/) #
255        /*- endfor -*/
256        []
257    \<rparr>"
258
259lemma wf_/*? isabelle_instance(c.name) ?*/: "wellformed_component /*? isabelle_instance(c.name) ?*/"
260  by (simp add: wellformed_CAMKES_simps)
261/*- endfor -*/
262
263/*- for i in me.composition.instances -*/
264definition
265    /*? isabelle_component(i.name) ?*/ :: component
266where[wellformed_CAMKES_simps]:
267    "/*? isabelle_component(i.name) ?*/ \<equiv> /*? isabelle_instance(i.type.name) ?*/"
268
269lemma wf_/*? isabelle_component(i.name) ?*/: "wellformed_component /*? isabelle_component(i.name) ?*/"
270  by (simp add: wellformed_CAMKES_simps)
271/*- endfor -*/
272
273/*- for c in me.composition.connections -*/
274definition
275    /*? isabelle_connection(c.name) ?*/ :: connection
276where[wellformed_CAMKES_simps]:
277    "/*? isabelle_connection(c.name) ?*/ \<equiv> \<lparr>
278        conn_type = /*? isabelle_connector(c.type.name) ?*/,
279        conn_from =
280        /*- for i, from_end in enumerate(c.from_ends) -*/
281          (''/*? from_end.instance.name ?*/'', ''/*? from_end.interface.name ?*/'') #
282        /*- endfor -*/
283          [],
284        conn_to =
285        /*- for i, to_end in enumerate(c.to_ends) -*/
286          (''/*? to_end.instance.name ?*/'', ''/*? to_end.interface.name ?*/'') #
287        /*- endfor -*/
288          []
289    \<rparr>"
290
291lemma wf_/*? isabelle_connection(c.name) ?*/: "wellformed_connection /*? isabelle_connection(c.name) ?*/"
292  by (simp add: wellformed_CAMKES_simps)
293/*- endfor -*/
294
295definition
296    /*? composition ?*/ :: composition
297where[wellformed_CAMKES_simps]:
298    "/*? composition ?*/ \<equiv> \<lparr>
299        components =
300        /*- for c in me.composition.instances -*/
301            (''/*? c.name ?*/'', /*? isabelle_component(c.name) ?*/) #
302        /*- endfor -*/
303        [],
304        connections =
305        /*- for c in me.composition.connections -*/
306            (''/*? c.name ?*/'', /*? isabelle_connection(c.name) ?*/) #
307        /*- endfor -*/
308        [],
309        group_labels =
310        /*- for l, g in sorted(group_labels.items()) -*/
311            (''/*? l ?*/'', ''/*? g ?*/'') #
312        /*- endfor -*/
313        []
314    \<rparr>"
315
316lemma wf_/*? composition ?*/: "wellformed_composition /*? composition ?*/"
317  by (simp add: wellformed_CAMKES_simps)
318
319definition
320    /*? configuration ?*/ :: "configuration option"
321where[wellformed_CAMKES_simps]:
322    "/*? configuration ?*/ \<equiv>
323    /*- if me.configuration -*/
324        Some (
325        /*- for s in me.configuration.settings -*/
326            (''/*? s.instance ?*/'', ''/*? s.attribute ?*/'', ''/*? s.value ?*/'') #
327        /*- endfor -*/
328        [])
329    /*- else -*/
330        None
331    /*- endif -*/
332    "
333
334lemma wf_/*? configuration ?*/:
335/*- if me.configuration -*/
336    "wellformed_configuration (the /*? configuration ?*/)"
337    by (simp add: wellformed_CAMKES_simps)
338/*- else -*/
339    (* No configuration *)/*# If there is no configuration it is trivially wellformed. #*/
340    "True"
341    by simp
342/*- endif -*/
343
344definition
345    /*? assembly ?*/ :: assembly
346where[wellformed_CAMKES_simps]:
347    "/*? assembly ?*/ \<equiv> \<lparr>
348        composition = /*? composition ?*/,
349        configuration = /*? configuration ?*/,
350        policy_extra = {/*? ', '.join(map(lambda("x: \"(''%s'', %s, ''%s'')\" % x"), sorted(get_policy_extra()))) ?*/}
351    \<rparr>"
352
353lemma wf_/*? assembly ?*/: "wellformed_assembly /*? assembly ?*/"
354  by (simp add: wellformed_CAMKES_simps)
355
356end
357
358end
359