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_Cimp_Base' % options.verification_base_name, outfile_name) ?*/ 17 18theory "/*? options.verification_base_name ?*/_Cimp_Base" imports 19 "CamkesGlueSpec.Types" 20 "CamkesGlueSpec.Abbreviations" 21 "CamkesGlueSpec.Connector" 22begin 23 24/*- macro show_native_type(type) --*/ 25 /*-- if type in ['int', 'int8_t', 'int16_t', 'int32_t', 'int64_t'] --*/ 26 int 27 /*-- elif type in ['unsigned int', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uintptr_t'] --*/ 28 nat 29 /*-- elif type in ['char', 'character'] --*/ 30 char 31 /*-- elif type == 'bool' --*/ 32 bool 33 /*-- elif type == 'string' --*/ 34 string 35 /*-- else --*/ 36 /*? raise(TemplateError('unsupported native type: %s' % type)) ?*/ 37 /*-- endif --*/ 38/*-- endmacro -*/ 39 40/*- macro show_wrapped_type(type) --*/ 41 /*-- if type in ['int', 'int8_t', 'int16_t', 'int32_t', 'int64_t'] --*/ 42 Integer 43 /*-- elif type in ['unsigned int', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uintptr_t'] --*/ 44 Number 45 /*-- elif type in ['char', 'character'] --*/ 46 Char 47 /*-- elif type == 'bool' --*/ 48 Boolean 49 /*-- elif type == 'string' --*/ 50 String 51 /*-- else --*/ 52 /*? raise(TemplateError('unsupported wrapped type: %s' % type)) ?*/ 53 /*-- endif --*/ 54/*-- endmacro -*/ 55 56/*- set instances = composition.instances -*/ 57/*- set connections = composition.connections -*/ 58/*- set components = set(map(lambda('x: x.type'), instances)) -*/ 59 60(** TPP: condense = True *) 61(* Connections *) 62datatype channel 63/*- for c in connections -*/ 64 /*- if loop.first --*/ 65 = 66 /*-- else --*/ 67 | 68 /*-- endif -*/ /*? c.name ?*/ 69/*- endfor -*/ 70(** TPP: condense = False *) 71 72(** TPP: condense = True *) 73(* Component instances *) 74datatype inst 75/*- for i in instances -*/ 76 /*- if loop.first --*/ 77 = 78 /*-- else --*/ 79 | 80 /*-- endif -*/ /*? i.name ?*/ 81/*- endfor -*/ 82/*- for c in connections -*/ 83 /*- if c.type.from_type == 'Event' -*/ 84 | /*? c.name ?*/\<^sub>e 85 /*- elif c.type.from_type == 'Dataport' -*/ 86 | /*? c.name ?*/\<^sub>d 87 /*- endif -*/ 88/*- endfor -*/ 89(** TPP: condense = False *) 90 91/*- for c in components -*/ 92 93(** TPP: condense = True *) 94(* /*? c.name ?*/'s interfaces *) 95datatype /*? c.name ?*/_channel 96/*- for i in c.uses + c.provides + c.emits + c.consumes + c.dataports -*/ 97 /*- if loop.first --*/ 98 = 99 /*-- else --*/ 100 | 101 /*-- endif -*/ /*? c.name ?*/_/*? i.name ?*/ 102/*- endfor -*/ 103(** TPP: condense = False *) 104 105 /*# Glue code for each outgoing procedural interface. #*/ 106 /*- for u in c.uses -*/ 107 /*- for i, m in enumerate(u.type.methods) -*/ 108(** TPP: condense = True *) 109definition 110 /*- set type_sig = ['(%s_channel \\<Rightarrow> channel) \\<Rightarrow>' % c.name] -*/ 111 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 112 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/ 113 /*- endfor -*/ 114 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 115 /*- do type_sig.append('(\'cs local_state') -*/ 116 /*- endif -*/ 117 /*- if m.return_type is not none -*/ 118 /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(m.return_type)) -*/ 119 /*- endif -*/ 120 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 121 /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(p.type)) -*/ 122 /*- endfor -*/ 123 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 124 /*# We had to unmarshal at least one parameter. #*/ 125 /*- do type_sig.append('\\<Rightarrow> \'cs local_state) \\<Rightarrow>') -*/ 126 /*- endif -*/ 127 /*- do type_sig.append('(channel, \'cs) comp') -*/ 128 Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ :: "/*? ' '.join(type_sig) ?*/" 129where 130 /*- set ch = isabelle_symbol('ch') -*/ 131 /*- set params = [ch] -*/ 132 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 133 /*- do params.append('%s\\<^sub>P' % p.name) -*/ 134 /*- endfor -*/ 135 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 136 /*- do params.append('embed_ret') -*/ 137 /*- endif -*/ 138 "Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ /*? ' '.join(params) ?*/ 139 /*-- set s = isabelle_symbol('s') --*/ 140 \<equiv> Request (\<lambda>/*? s ?*/. {\<lparr>q_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, q_data = Call /*? i ?*/ ( 141 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 142 /*? show_wrapped_type(p.type) ?*/ (/*? p.name ?*/\<^sub>P /*? s ?*/) # 143 /*- endfor -*/ 144 [])\<rparr>}) discard ;; 145 /*- set q = isabelle_symbol() -*/ 146 /*- set s = isabelle_symbol() -*/ 147 /*- set xs = isabelle_symbol() -*/ 148 Response (\<lambda>/*? q ?*/ /*? s ?*/. case q_data /*? q ?*/ of Return /*? xs ?*/ \<Rightarrow> 149 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 150 {(embed_ret /*? s ?*/ 151 /*- if m.return_type is not none -*/ 152 /*- set v = isabelle_symbol() -*/ 153 (case hd /*? xs ?*/ of /*? show_wrapped_type(m.return_type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/) 154 /*- endif -*/ 155 /*- for i, p in enumerate(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters)) -*/ 156 /*- set v = isabelle_symbol() -*/ 157 (case /*? xs ?*/ ! /*? i + (1 if m.return_type is not none else 0) ?*/ of /*? show_wrapped_type(p.type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/) 158 /*- endfor -*/ 159 /*- else -*/ 160 {(/*? s ?*/ 161 /*- endif -*/ 162 , \<lparr>a_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, a_data = Void\<rparr>)} | _ \<Rightarrow> {})" 163(** TPP: condense = False *) 164 /*- endfor -*/ 165 /*- endfor -*/ 166 167 /*# Glue code for each incoming procedural interface. #*/ 168 /*- for u in c.provides -*/ 169(** TPP: condense = True *) 170definition 171 /*- set type_sig = ['(%s_channel \\<Rightarrow> channel) \\<Rightarrow>' % c.name] -*/ 172 /*- for m in u.type.methods -*/ 173 /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/ 174 /*- do type_sig.append('(\'cs local_state \\<Rightarrow>') -*/ 175 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 176 /*- do type_sig.append('%s \\<Rightarrow>' % show_native_type(p.type)) -*/ 177 /*- endfor -*/ 178 /*- do type_sig.append('\'cs local_state) \\<Rightarrow>') -*/ 179 /*- endif -*/ 180 /*- do type_sig.append('(channel, \'cs) comp \\<Rightarrow>') -*/ 181 /*- if m.return_type is not none -*/ 182 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(m.return_type)) -*/ 183 /*- endif -*/ 184 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 185 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/ 186 /*- endfor -*/ 187 /*- endfor -*/ 188 /*- do type_sig.append('(channel, \'cs) comp') -*/ 189 Recv_/*? c.name ?*/_/*? u.name ?*/ :: "/*? ' '.join(type_sig) ?*/" 190where 191 /*- set ch = isabelle_symbol('ch') -*/ 192 /*- set params = [ch] -*/ 193 /*- for m in u.type.methods -*/ 194 /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/ 195 /*- do params.append('%s\\<^sub>E' % m.name) -*/ 196 /*- endif -*/ 197 /*- do params.append('%s_%s_%s' % (c.name, u.name, m.name)) -*/ 198 /*- if m.return_type is not none -*/ 199 /*- do params.append('%s_return\\<^sub>P' % m.name) -*/ 200 /*- endif -*/ 201 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 202 /*- do params.append('%s_%s\\<^sub>P' % (m.name, p.name)) -*/ 203 /*- endfor -*/ 204 /*- endfor -*/ 205 "Recv_/*? c.name ?*/_/*? u.name ?*/ /*? ' '.join(params) ?*/ 206 \<equiv> 207 /*- for i, m in enumerate(u.type.methods) -*/ 208 /*- if not loop.first -*/ 209 \<squnion> 210 /*- endif -*/ 211 /*- set q = isabelle_symbol() -*/ 212 /*- set s = isabelle_symbol() -*/ 213 /*- set n = isabelle_symbol() -*/ 214 /*- set xs = isabelle_symbol() -*/ 215 (Response (\<lambda>/*? q ?*/ /*? s ?*/. case q_data /*? q ?*/ of Call /*? n ?*/ /*? xs ?*/ \<Rightarrow> (if /*? n ?*/ = /*? i ?*/ then {( 216 /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/ 217 /*? m.name ?*/\<^sub>E /*? s ?*/ 218 /*- for k, p in enumerate(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters)) -*/ 219 /*- set v = isabelle_symbol() -*/ 220 (case /*? xs ?*/ ! /*? k ?*/ of /*? show_wrapped_type(p.type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/) 221 /*- endfor -*/ 222 /*- else -*/ 223 /*? s ?*/ 224 /*- endif -*/ 225 , \<lparr>a_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, a_data = Void\<rparr>)} else {}) | _ \<Rightarrow> {}) ;; 226 /*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ ;; 227 /*- set s = isabelle_symbol() -*/ 228 Request (\<lambda>/*? s ?*/. {\<lparr>q_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, q_data = Return ( 229 /*- if m.return_type is not none -*/ 230 /*? show_wrapped_type(m.return_type) ?*/ (/*? m.name ?*/_return\<^sub>P /*? s ?*/) # 231 /*- endif -*/ 232 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 233 /*? show_wrapped_type(p.type) ?*/ (/*? m.name ?*/_/*? p.name ?*/\<^sub>P /*? s ?*/) # 234 /*- endfor -*/ 235 [])\<rparr>}) discard) 236 /*- endfor -*/ 237 " 238(** TPP: condense = False *) 239 /*- endfor -*/ 240 241 /*# Glue code for each outgoing event interface. #*/ 242 /*- for u in c.emits -*/ 243(** TPP: condense = True *) 244definition 245 Emit_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp" 246where 247 /*- set ch = isabelle_symbol('ch') -*/ 248 "Emit_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ \<equiv> EventEmit (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/)" 249(** TPP: condense = False *) 250 /*- endfor -*/ 251 252 /*# Glue code for each incoming event interface. #*/ 253 /*- for u in c.consumes -*/ 254(** TPP: condense = True *) 255definition 256 Poll_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 257where 258 /*- set ch = isabelle_symbol('ch') -*/ 259 /*- set embed = isabelle_symbol('embed') -*/ 260 "Poll_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? embed ?*/ \<equiv> EventPoll (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? embed ?*/" 261(** TPP: condense = False *) 262 263(** TPP: condense = True *) 264definition 265 Wait_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 266where 267 /*- set embed = isabelle_symbol('embed') -*/ 268 "Wait_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? embed ?*/ \<equiv> EventWait (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? embed ?*/" 269(** TPP: condense = False *) 270 /*- endfor -*/ 271 272 /*# Glue code for dataport interfaces. #*/ 273 /*- for u in c.dataports -*/ 274(** TPP: condense = True *) 275definition 276 Read_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 277where 278 /*- set ch = isabelle_symbol('ch') -*/ 279 /*- set addr = isabelle_symbol('addr') -*/ 280 /*- set embed = isabelle_symbol('embed') -*/ 281 "Read_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? addr ?*/ /*? embed ?*/ \<equiv> MemoryRead (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? addr ?*/ /*? embed ?*/" 282(** TPP: condense = False *) 283 284(** TPP: condense = True *) 285definition 286 Write_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable) \<Rightarrow> (channel, 'cs) comp" 287where 288 /*- set ch = isabelle_symbol('ch') -*/ 289 /*- set addr = isabelle_symbol('addr') -*/ 290 /*- set proj = isabelle_symbol('proj') -*/ 291 "Write_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? addr ?*/ /*? proj ?*/ \<equiv> MemoryWrite (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? addr ?*/ /*? proj ?*/" 292(** TPP: condense = False *) 293 /*- endfor -*/ 294 295/*- endfor -*/ 296 297(* Component instantiations *) 298/*- for i in instances -*/ 299 /*- set c = i.type -*/ 300 301 /*- for u in c.uses -*/ 302 /*- for m in u.type.methods -*/ 303(** TPP: condense = True *) 304definition 305 /*- set type_sig = [] -*/ 306 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 307 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/ 308 /*- endfor -*/ 309 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 310 /*- do type_sig.append('(\'cs local_state') -*/ 311 /*- endif -*/ 312 /*- if m.return_type is not none -*/ 313 /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(m.return_type)) -*/ 314 /*- endif -*/ 315 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 316 /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(p.type)) -*/ 317 /*- endfor -*/ 318 /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/ 319 /*# We had to unmarshal at least one parameter. #*/ 320 /*- do type_sig.append('\\<Rightarrow> \'cs local_state) \\<Rightarrow>') -*/ 321 /*- endif -*/ 322 /*- do type_sig.append('(channel, \'cs) comp') -*/ 323 Call_/*? i.name ?*/_/*? u.name ?*/_/*? m.name ?*/ :: "/*? ' '.join(type_sig) ?*/" 324where 325 "Call_/*? i.name ?*/_/*? u.name ?*/_/*? m.name ?*/ \<equiv> 326 /*- set l = isabelle_symbol() -*/ 327 Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 328 /*- set j = joiner('|') -*/ 329 /*- for conn in connections -*/ 330 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 331 /*- if idx -*/ 332 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 333 /*- endif -*/ 334 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 335 /*- if idx -*/ 336 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 337 /*- endif -*/ 338 /*- endfor -*/ 339 )" 340(** TPP: condense = False *) 341 /*- endfor -*/ 342 /*- endfor -*/ 343 344 /*- for u in c.provides -*/ 345(** TPP: condense = True *) 346definition 347 /*- set type_sig = [] -*/ 348 /*- for m in u.type.methods -*/ 349 /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/ 350 /*- do type_sig.append('(\'cs local_state \\<Rightarrow>') -*/ 351 /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/ 352 /*- do type_sig.append('%s \\<Rightarrow>' % show_native_type(p.type)) -*/ 353 /*- endfor -*/ 354 /*- do type_sig.append('\'cs local_state) \\<Rightarrow>') -*/ 355 /*- endif -*/ 356 /*- do type_sig.append('(channel, \'cs) comp \\<Rightarrow>') -*/ 357 /*- if m.return_type -*/ 358 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(m.return_type)) -*/ 359 /*- endif -*/ 360 /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/ 361 /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/ 362 /*- endfor -*/ 363 /*- endfor -*/ 364 /*- do type_sig.append('(channel, \'cs) comp') -*/ 365 Recv_/*? i.name ?*/_/*? u.name ?*/ :: "/*? ' '.join(type_sig) ?*/" 366where 367 "Recv_/*? i.name ?*/_/*? u.name ?*/ \<equiv> 368 /*- set l = isabelle_symbol() -*/ 369 Recv_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 370 /*- set j = joiner('|') -*/ 371 /*- for conn in connections -*/ 372 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 373 /*- if idx -*/ 374 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 375 /*- endif -*/ 376 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 377 /*- if idx -*/ 378 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 379 /*- endif -*/ 380 /*- endfor -*/ 381 )" 382(** TPP: condense = False *) 383 /*- endfor -*/ 384 385 /*- for u in c.emits -*/ 386(** TPP: condense = True *) 387definition 388 Emit_/*? i.name ?*/_/*? u.name ?*/ :: "(channel, 'cs) comp" 389where 390 /*- set l = isabelle_symbol() -*/ 391 "Emit_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Emit_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 392 /*- set j = joiner('|') -*/ 393 /*- for conn in connections -*/ 394 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 395 /*- if idx -*/ 396 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 397 /*- endif -*/ 398 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 399 /*- if idx -*/ 400 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 401 /*- endif -*/ 402 /*- endfor -*/ 403 )" 404(** TPP: condense = False *) 405 /*- endfor -*/ 406 407 /*- for u in c.consumes -*/ 408(** TPP: condense = True *) 409definition 410 Poll_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 411where 412 /*- set l = isabelle_symbol() -*/ 413 "Poll_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Poll_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 414 /*- set j = joiner('|') -*/ 415 /*- for conn in connections -*/ 416 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 417 /*- if idx -*/ 418 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 419 /*- endif -*/ 420 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 421 /*- if idx -*/ 422 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 423 /*- endif -*/ 424 /*- endfor -*/ 425 )" 426(** TPP: condense = False *) 427 428(** TPP: condense = True *) 429definition 430 Wait_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 431where 432 /*- set l = isabelle_symbol() -*/ 433 "Wait_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Wait_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 434 /*- set j = joiner('|') -*/ 435 /*- for conn in connections -*/ 436 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 437 /*- if idx -*/ 438 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 439 /*- endif -*/ 440 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 441 /*- if idx -*/ 442 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 443 /*- endif -*/ 444 /*- endfor -*/ 445 )" 446(** TPP: condense = False *) 447 /*- endfor -*/ 448 449 /*- for u in c.dataports -*/ 450(** TPP: condense = True *) 451definition 452 Read_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp" 453where 454 /*- set l = isabelle_symbol() -*/ 455 "Read_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Read_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 456 /*- set j = joiner('|') -*/ 457 /*- for conn in connections -*/ 458 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 459 /*- if idx -*/ 460 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 461 /*- endif -*/ 462 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 463 /*- if idx -*/ 464 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 465 /*- endif -*/ 466 /*- endfor -*/ 467 )" 468(** TPP: condense = False *) 469 470(** TPP: condense = True *) 471definition 472 Write_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable) \<Rightarrow> (channel, 'cs) comp" 473where 474 /*- set l = isabelle_symbol() -*/ 475 "Write_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Write_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of 476 /*- set j = joiner('|') -*/ 477 /*- for conn in connections -*/ 478 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 479 /*- if idx -*/ 480 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 481 /*- endif -*/ 482 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 483 /*- if idx -*/ 484 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 485 /*- endif -*/ 486 /*- endfor -*/ 487 )" 488(** TPP: condense = False *) 489 /*- endfor -*/ 490 491/*- endfor -*/ 492 493locale system_state = 494 fixes init_component_state :: 'cs 495 fixes trusted :: "(inst, ((channel, 'cs) comp \<times> 'cs local_state)) map" 496begin 497 498/*- for c in components -*/ 499 /*# Emit a broad definition for each component if the user does not want to instantiate it. #*/ 500(** TPP: condense = True *) 501definition 502 /*? c.name ?*/_untrusted :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp" 503where 504 /*- set ch = isabelle_symbol('ch') -*/ 505 "/*? c.name ?*/_untrusted /*? ch ?*/ \<equiv> 506 LOOP ( 507 UserStep 508 /*- for i in c.uses + c.provides + c.emits + c.consumes + c.dataports -*/ 509 \<squnion> ArbitraryRequest (/*? ch ?*/ /*? c.name ?*/_/*? i.name ?*/) 510 \<squnion> ArbitraryResponse (/*? ch ?*/ /*? c.name ?*/_/*? i.name ?*/) 511 /*- endfor -*/ 512 )" 513(** TPP: condense = False *) 514/*- endfor -*/ 515 516/*# Emit simulated components for each event. #*/ 517/*- for e in reduce(lambda('xs, b: xs + ([b.type] if b.type not in xs else [])'), flatMap(lambda('x: x.emits + x.consumes'), components), []) -*/ 518 519(* Simulated component for event /*? e ?*/. *) 520type_synonym /*? e ?*/_channel = unit 521 522(** TPP: condense = True *) 523definition 524 /*? e ?*/ :: "(/*? e ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp" 525where 526 /*- set ch = isabelle_symbol('ch') -*/ 527 "/*? e ?*/ /*? ch ?*/ \<equiv> event (/*? ch ?*/ ())" 528(** TPP: condense = False *) 529/*- endfor -*/ 530 531/*# Emit simulated components for each dataport. #*/ 532/*- for d in reduce(lambda('xs, b: xs + ([b.type] if b.type not in xs else [])'), flatMap(lambda('x: x.dataports'), components), []) -*/ 533 /*# The built-in type 'Buf' is defined in Connector.thy. #*/ 534 /*- if d != 'Buf' -*/ 535 536type_synonym /*? d ?*/\<^sub>d_channel = unit 537 538(** TPP: condense = True *) 539definition 540 /*? d ?*/\<^sub>d :: "(/*? d ?*/\<^sub>d_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp" 541where 542 /*- set ch = isabelle_symbol('ch') -*/ 543 "/*? d ?*/\<^sub>d /*? ch ?*/ \<equiv> memory (/*? ch ?*/ ())" 544(** TPP: condense = False *) 545 /*- endif -*/ 546/*- endfor -*/ 547 548(* Component instantiations *) 549/*- for i in instances -*/ 550 /*- set c = i.type -*/ 551 552(** TPP: condense = True *) 553definition 554 /*? i.name ?*/_untrusted :: "(channel, 'cs) comp" 555where 556 /*- set l = isabelle_symbol() -*/ 557 "/*? i.name ?*/_untrusted \<equiv> /*? c.name ?*/_untrusted (\<lambda>/*? l ?*/. case /*? l ?*/ of 558 /*- set j = joiner('|') -*/ 559 /*- for conn in connections -*/ 560 /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 561 /*- if idx -*/ 562 /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 563 /*- endif -*/ 564 /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/ 565 /*- if idx -*/ 566 /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/ 567 /*- endif -*/ 568 /*- endfor -*/ 569 )" 570(** TPP: condense = False *) 571 572/*- endfor -*/ 573 574/*# Simulated component instance for each event connection. #*/ 575/*- for c in filter(lambda('x: x.type.from_type == \'Event\''), connections) -*/ 576definition 577 /*? c.name ?*/\<^sub>e_instance :: "(channel, 'cs) comp" 578where 579 "/*? c.name ?*/\<^sub>e_instance \<equiv> /*? c.from_interface.type ?*/ (\<lambda>_. /*? c.name ?*/)" 580/*- endfor -*/ 581 582/*# Simulated component instance for each dataport connection. #*/ 583/*- for c in filter(lambda('x: x.type.from_type == \'Dataport\''), connections) -*/ 584definition 585 /*? c.name ?*/\<^sub>d_instance :: "(channel, 'cs) comp" 586where 587 "/*? c.name ?*/\<^sub>d_instance \<equiv> /*? c.from_interface.type ?*/\<^sub>d (\<lambda>_. /*? c.name ?*/)" 588/*- endfor -*/ 589 590(* Global initial state *) 591/*# Even though this is generated as a mapping to an option type it is actually 592 ** full. 593 #*/ 594(** TPP: condense = True *) 595definition 596 gs\<^sub>0 :: "(inst, channel, 'cs) global_state" 597where 598 /*- set p = isabelle_symbol('p') -*/ 599 /*- set s = isabelle_symbol() -*/ 600 "gs\<^sub>0 /*? p ?*/ \<equiv> case trusted /*? p ?*/ of Some /*? s ?*/ \<Rightarrow> Some /*? s ?*/ | _ \<Rightarrow> (case /*? p ?*/ of 601 /*- set j = joiner('|') -*/ 602 /*- for i in instances -*/ 603 /*? j() ?*/ /*? i.name ?*/ \<Rightarrow> Some (/*? i.name ?*/_untrusted, Component init_component_state) 604 /*- endfor -*/ 605 /*- for c in connections -*/ 606 /*- if c.type.from_type == 'Event' -*/ 607 /*? j() ?*/ /*? c.name ?*/\<^sub>e \<Rightarrow> Some (/*? c.name ?*/\<^sub>e_instance, init_event_state) 608 /*- elif c.type.from_type == 'Dataport' -*/ 609 /*? j() ?*/ /*? c.name ?*/\<^sub>d \<Rightarrow> Some (/*? c.name ?*/\<^sub>d_instance, init_memory_state) 610 /*- endif -*/ 611 /*- endfor -*/ 612 )" 613(** TPP: condense = False *) 614 615end 616 617end 618