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