GitLab will be upgraded on 31 Jan 2023 from 2.00 pm (AEDT) to 3.00 pm (AEDT). During the update, GitLab and Mattermost services will not be available. If you have any concerns with this, please talk to us at N110 (b) CSIT building.

uvmTypesScript.sml 17.8 KB
Newer Older
1
open HolKernel Parse boolLib bossLib
2

3
4
5
6
open arithmeticTheory
open listTheory
open pairTheory
open pred_setTheory
7
open lcsymtacs
8
9

val _ = new_theory "uvmTypes"
10
11
val _ = ParseExtras.tight_equality()

12
val _ = Datatype `ref_type = REF | PTR`
Michael Norrish's avatar
Michael Norrish committed
13

14
val _ = Datatype`
15
  uvm_type =
16
  | Void
17
18
19
  | Int num
  | Float
  | Double
20
  | Ref (uvm_type + num)
21
  | IRef ref_type (uvm_type + num)
22
  | WeakRef (uvm_type + num)
23
  | FuncRef ref_type funcsig
24
25
  | ThreadRef
  | StackRef
26
27
  | FrameCursorRef
  | IrBuilderRef
28
  | TagRef64
29
  | Array uvm_type num
30
  | Vector uvm_type num
31
32
  | Hybrid (uvm_type list) uvm_type
  | Struct num (uvm_type list) ;
33
34

  funcsig = <|
35
36
    arg_types: uvm_type list;
    return_types: uvm_type list
37
  |>
38
39
`

40
41
42
43
44
45
46
47
48
49
50
51
52
val _ = set_fixity "→" (Infix(NONASSOC, 450))
val _ = overload_on("→", ``λa b. <| arg_types := a; return_types := b |>``)

(* Structs may contain self-references through refs and pointers. This is
   represented by a fixpoint: each struct has an ID number "fx", used as a
   fixpoint, and nested Ref/IRef/WeakRef types may contain the type
   "Fixpoint fx".
   
   The "struct_fixpoint" function performs one step of fixpoint expansion,
   replacing each "Fixpoint fx" with "Type (Struct fx ts)", where "ts" is the
   struct's members.
*)

53
54
55
val _ = overload_on("Type", ``INL : uvm_type -> uvm_type + num``)
val _ = overload_on("Fixpoint", ``INR : num -> uvm_type + num``)

56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
val uvm_type_size_mem = store_thm("uvm_type_size_mem",
  ``x xs. MEM x xs  uvm_type_size x < uvm_type2_size xs``,
  rw[] >> Induct_on `xs` >> rw[] >> fs[definition "uvm_type_size_def"])

val struct_fixpoint_def = TotalDefn.tDefine "struct_fixpoint" `

    struct_fixpoint (fx, ts) (Ref (Type t)) =
      Ref (Type (struct_fixpoint (fx, ts) t))
   struct_fixpoint (fx, ts) (Ref (Fixpoint fx')) =
      Ref (if fx = fx' then Type (Struct fx ts) else Fixpoint fx')
   struct_fixpoint (fx, ts) (IRef rt (Type t)) =
      IRef rt (Type (struct_fixpoint (fx, ts) t))
   struct_fixpoint (fx, ts) (IRef rt (Fixpoint fx')) =
      IRef rt (if fx = fx' then Type (Struct fx ts) else Fixpoint fx')
   struct_fixpoint (fx, ts) (WeakRef (Type t)) =
      WeakRef (Type (struct_fixpoint (fx, ts) t))
   struct_fixpoint (fx, ts) (WeakRef (Fixpoint fx')) =
      WeakRef (if fx = fx' then Type (Struct fx ts) else Fixpoint fx')
   struct_fixpoint (fx, ts) (Array t n) = Array (struct_fixpoint (fx, ts) t) n
   struct_fixpoint (fx, ts) (Vector t n) = Vector (struct_fixpoint (fx, ts) t) n
   struct_fixpoint (fx, ts) (Hybrid fts vt) =
      Hybrid (MAP (struct_fixpoint (fx, ts)) fts) (struct_fixpoint (fx, ts) vt)
   struct_fixpoint (fx, ts) (Struct fx' ts') =
      (if fx = fx' then Struct fx ts'
                   else Struct fx' (MAP (struct_fixpoint (fx, ts)) ts'))
   struct_fixpoint _ ty = ty

` (WF_REL_TAC `measure (uvm_type_size o SND)` >> rw[] >>
   metis_tac[uvm_type_size_mem, ADD_COMM, LESS_IMP_LESS_ADD])

(* It is safe to induct over the members of a type while recursively expanding
   all fixpoints with "struct_fixpoint", because fixpoints can only occur in
   referent types, and the referent of a type is not a member of that type.
   
   But recursive expansion of fixpoints does cause "uvm_type_size" to grow
   without bound, preventing HOL from easily proving termination of functions
   that use it. To work around this, we define a new measure, "uvm_type_depth",
   that does not have this limitation.
*)

val uvm_type_depth_def = TotalDefn.tDefine "uvm_type_depth" `
    uvm_type_depth (Array t _) = SUC (uvm_type_depth t)
   uvm_type_depth (Vector t _) = SUC (uvm_type_depth t)
   uvm_type_depth (Hybrid fts vt) =
      SUC (FOLDR MAX (uvm_type_depth vt) (MAP uvm_type_depth fts))
   uvm_type_depth (Struct _ ts) =
      SUC (FOLDR MAX 0 (MAP uvm_type_depth ts))
   uvm_type_depth _ = 0
` (WF_REL_TAC `measure uvm_type_size` >> rw[] >>
   metis_tac[uvm_type_size_mem, ADD_COMM, LESS_IMP_LESS_ADD])

val uvm_type_depth_ord = store_thm("uvm_type_depth_ord",

  ``(t n. uvm_type_depth t < uvm_type_depth (Array t n))
   (t n. uvm_type_depth t < uvm_type_depth (Vector t n))
   (ft fts vt. MEM ft fts  uvm_type_depth ft < uvm_type_depth (Hybrid fts vt))
   (fts vt. uvm_type_depth vt < uvm_type_depth (Hybrid fts vt))
   (fx t ts. MEM t ts  uvm_type_depth t < uvm_type_depth (Struct fx ts))``,

  rw[] >> simp[Once uvm_type_depth_def, MAX_DEF] >>
  FIRST [Induct_on `fts`, Induct_on `ts`] >> fs[] >> rw[MAX_DEF] >> fs[])

val struct_fixpoint_same_depth = store_thm("struct_fixpoint_same_depth",
  ``ty fx ts. uvm_type_depth (struct_fixpoint (fx, ts) ty) =  uvm_type_depth ty``,
  strip_tac >> measureInduct_on `uvm_type_size ty` >> Cases_on `ty` >> rw[] >>
  TRY (Cases_on `s`) >>
  simp[uvm_type_depth_def, struct_fixpoint_def] >>
  TRY (CASE_TAC >> simp[uvm_type_depth_def]) >>
  TRY (
    ho_match_mp_tac FOLDR_CONG >> rw[] >>
    TRY (rw[MAP_MAP_o] >> ho_match_mp_tac MAP_CONG >> rw[])) >>
  first_x_assum (match_mp_tac o
    (RIGHT_IMP_FORALL_CONV |> ONCE_DEPTH_CONV |> REPEATC |> CONV_RULE)) >>
  simp[definition "uvm_type_size_def"] >>
  metis_tac[uvm_type_size_mem, ADD_COMM, LESS_IMP_LESS_ADD])

(* Type conversions, as defined in the spec. These are primarily used in
   uvmBytesTheory and uvmIRTheory.

   https://gitlab.anu.edu.au/mu/mu-spec/blob/master/instruction-set.rst#conversion
*)

val _ = Datatype`
  convtype =
  | TRUNC
  | ZEXT
  | SEXT
  | FPTRUNC
  | FPEXT
  | FPTOUI
  | FPTOSI
  | UITOFP
  | SITOFP
  | BITCAST
  | REFCAST
  | PTRCAST
`

(* Type categories, as defined in the spec.

   https://gitlab.anu.edu.au/mu/mu-spec/blob/master/type-system.rst#types-and-type-constructors
*)
158

159
160
val floating_point_type_def = Define`
  floating_point_type = {Float; Double}
161
`
162

163
164
val object_referent_type_def = Define`
  object_referent_type = {Ref r | T}  {WeakRef r | T}
165
`
166

167
168
val reference_type_def = Define`
  reference_type = {IRef REF r | T}  object_referent_type
169
`
170

171
172
173
174
val opaque_reference_type_def = Define`
  opaque_reference_type =
    {FuncRef REF sig | T}
   {ThreadRef; StackRef; FrameCursorRef; IrBuilderRef}
175
`
176

177
178
179
180
181
182
val general_reference_type_def = Define`
  general_reference_type = reference_type  opaque_reference_type
`

val pointer_type_def = Define`
  pointer_type = {IRef PTR r | T}  {FuncRef PTR sig | T}
183
`
184

185
val scalar_type_def = Define`
186
187
188
  scalar_type =
    {Int n | T}  floating_point_type  pointer_type 
    general_reference_type  {TagRef64}
189
`
190

191
192
193
194
195
val composite_type_def = Define`
  composite_type =
    {Struct fx ts | T}  {Hybrid fts vt | T}  {Array t n | T} 
    {Vector t n | T}
`
196

197
198
val variable_length_type_def = Define`
  variable_length_type = {Hybrid fts vt | T}
199
`
200

201
202
203
204
205
val eq_comparable_type_def = Define`
  eq_comparable_type =
    {Int n | T}  pointer_type  {Ref r | T}  {IRef REF r | T} 
    opaque_reference_type
`
206

207
208
val ult_comparable_type_def = Define`
  ult_comparable_type = {Int n | T}  {IRef REF r | T}  pointer_type
209
210
`

211
212
213
214
215
216
217
218
219
220
val type_category_defs = foldl (uncurry CONJ) floating_point_type_def [
  object_referent_type_def, reference_type_def, opaque_reference_type_def,
  general_reference_type_def, pointer_type_def, scalar_type_def,
  composite_type_def, variable_length_type_def, eq_comparable_type_def,
  ult_comparable_type_def
]

(* A few other type categories, not from the spec. *)

(* A traced type is tracked by the garbage collector. *)
221
val (tracedtype_rules, tracedtype_ind, tracedtype_cases) = Hol_reln`
222
    (ty. tracedtype (Ref ty))
223
   (ty. tracedtype (IRef REF ty))
224
225
226
227
228
229
   (ty. tracedtype (WeakRef ty))
   (sz ty. tracedtype ty  tracedtype (Array ty sz))
   (sz ty. tracedtype ty  tracedtype (Vector ty sz))
   tracedtype ThreadRef
   tracedtype StackRef
   tracedtype TagRef64
Adam R. Nelson's avatar
Adam R. Nelson committed
230
   (fixty varty.
231
232
233
234
235
      (EXISTS tracedtype fixty  tracedtype varty)
     tracedtype (Hybrid fixty varty))
   (fx ty tys.
      tracedtype ty  MEM ty tys
     tracedtype (Struct fx tys))
236
`
237

Adam R. Nelson's avatar
Adam R. Nelson committed
238
(* A native-safe type can be handed off to the "native" world. *)
239
val (native_safe_rules, native_safe_ind, native_safe_cases) = Hol_reln`
240
241
242
243
244
245
    (n. native_safe (Int n))
   native_safe Float
   native_safe Double
   native_safe Void
   (ty n. native_safe ty  native_safe (Vector ty n))
   (ty n. native_safe ty  native_safe (Array ty n))
246
247
   (ty. native_safe (IRef PTR ty))
   (sig. native_safe (FuncRef PTR sig))
Adam R. Nelson's avatar
Adam R. Nelson committed
248
   (fty vty.
249
250
251
252
253
      EVERY native_safe fty  native_safe vty
     native_safe (Hybrid fty vty))
   (fx tys.
      EVERY native_safe tys
     native_safe (Struct fx tys))
254
`
255

256
257
258
259
260
261
262
263
264
265
266
267
268
(*
   maybe_vector : (uvm_type -> bool) -> uvm_type -> bool

   "maybe_vector P ty" checks to see if P is true of ty.  Alternatively,
   if ty is a vector type, it checks to see if P is true of the element
   type of the vector
*)
val maybe_vector_def = Define`
  maybe_vector P ty 
    P ty  case ty of Vector ty0 _ => P ty0 | _ => F
`


269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
(* A type is valid ("ok") if it meets the following criteria:

   ∙ Ints, arrays, and vectors have a length > 0.
   ∙ There are no free struct fixpoint variables.
   ∙ Variable-length types (hybrids) and void do not occur as members of a
     composite type.
   ∙ Referents of pointer types are native-safe.
*)

val (type_ok_rules, type_ok_ind, type_ok_cases) = Hol_reln`
    type_ok Void  type_ok Float  type_ok Double
   type_ok ThreadRef  type_ok StackRef  type_ok TagRef64
   type_ok FrameCursorRef  type_ok IrBuilderRef
   (n. 0 < n  type_ok (Int n))
   (t. type_ok t  type_ok (Ref (Type t)))
   (t. type_ok t  type_ok (IRef REF (Type t)))
   (t. type_ok t  native_safe t  type_ok (IRef PTR (Type t)))
   (t. type_ok t  type_ok (WeakRef (Type t)))
   (r ts1 ts2.
      EVERY type_ok ts1  EVERY type_ok ts2
       type_ok (FuncRef r (ts1  ts2)))
   (t n.
      0 < n  type_ok t  ¬variable_length_type t  t  Void
       type_ok (Array t n))
   (t n.
      0 < n  type_ok t  ¬variable_length_type t  scalar_type t
       type_ok (Vector t n))
   (fts vt.
      EVERY (λt. type_ok t  ¬variable_length_type t  t  Void) fts  
      type_ok vt  ¬variable_length_type vt  vt  Void
       type_ok (Hybrid fts vt))
   (fx ts.
      EVERY type_ok (MAP (struct_fixpoint (fx, ts)) ts) 
      ¬EXISTS variable_length_type ts 
      ¬MEM Void ts  ¬NULL ts
       type_ok (Struct fx ts))
305
306
`

307
(* Per the spec:
Michael Norrish's avatar
Michael Norrish committed
308

309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
   ∙ A _member_ of a composite type T is either a field of T if T is a struct,
     or an element of T if T is an array or a vector, or a field in the fixed
     part or any element in the variable part if T is a hybrid.

   ∙ A _component_ of type T is either itself or a member of any component of T.

   https://gitlab.anu.edu.au/mu/mu-spec/blob/master/type-system.rst#types-and-type-constructors
*)

val member_types_def = Define`
    member_types _ (Array t n) = GENLIST (K t) n
   member_types _ (Vector t n) = GENLIST (K t) n
   member_types (SOME sz) (Hybrid fts vt) = fts ++ GENLIST (K vt) sz
   member_types _ (Struct fx ts) = MAP (struct_fixpoint (fx, ts)) ts
   member_types _ _ = []
`

val member_type_def = Define `member_type ty t  MEM t (member_types (SOME 1) ty)`

val (component_type_rules, component_type_ind, component_type_cases) = Hol_reln`
    (t. component_type t t)
   (t m c. member_type t m  component_type m c  component_type t c)
`

(* There is a "component_types" function as well, but it is defined later. *)

(* Per the spec, a component C is a _prefix_ of a type T if any of the following
   is true:

   ∙ C is T itself.
   ∙ T is a struct and C is its first field.
   ∙ T is a hybrid and C is its first field of the fixed part, or the fixed part
     of T has no fields and C is the first element of the variable part.
   ∙ T is an array<T n> or vector<T n> and n ≥ 1, and C is its first element.
   ∙ C is a prefix of another prefix of T.

   https://gitlab.anu.edu.au/mu/mu-spec/blob/master/memory.rst#prefix-rule
*)

val (prefix_type_rules, prefix_type_ind, prefix_type_cases) = Hol_reln`
    (t. prefix_type t t)
   (fx t ts. prefix_type (Struct fx (t::ts)) (struct_fixpoint (fx, t::ts) t))
   (t ts vt. prefix_type (Hybrid (t::ts) vt) t)
   (vt. prefix_type (Hybrid [] vt) vt)
   (t n. 0 < n  prefix_type (Array t n) t)
   (t n. 0 < n  prefix_type (Vector t n) t)
   (t1 t2 t3. prefix_type t1 t2  prefix_type t2 t3  prefix_type t1 t3)
`

val scalar_prefix_def = Define`
    scalar_prefix (Array t _) = t
   scalar_prefix (Vector t _) = t
   scalar_prefix (Hybrid (t::_) _) = t
   scalar_prefix (Hybrid [] t) = t
   scalar_prefix (Struct _ []) = Void
   scalar_prefix (Struct _ (t::_)) = t
   scalar_prefix t = t
Michael Norrish's avatar
Michael Norrish committed
366
367
`

368
369
(* The function "component_types" returns a list of lists, representing the
   types that can be used to access each offset of the parent type.
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
   
   This is the format that uvmMemoryTheory uses to represent typed cells in the
   memory.
*)

(* A few lemmas are necessary to prove termination: *)

val member_types_depth = store_thm("member_types_depth",
  ``t sz m. MEM m (member_types sz t)
            uvm_type_depth m < uvm_type_depth t``,
  Cases >> Cases >> rw[member_types_def, MEM_GENLIST, MEM_MAP] >>
  fs[uvm_type_depth_ord, struct_fixpoint_same_depth])

val LIST_BIND_CONG = prove(
  ``l1 l2 f f'. (l1 = l2)  (x. MEM x l2  (f x = f' x))
                (LIST_BIND l1 f = LIST_BIND l2 f')``,
  prove_tac[LIST_BIND_def, MAP_CONG])

val _ = DefnBase.add_cong LIST_BIND_CONG

(* ...with those lemmas, the function itself is actually very simple! *)

val component_types_def = TotalDefn.tDefine "component_types" `
  component_types sz t =
    case member_types sz t of
395
396
397
    | [] => [[t]]
    | ts => (let ts' = LIST_BIND ts (component_types NONE) in
             SNOC t (HD ts')::TL ts')
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
` (WF_REL_TAC `measure (uvm_type_depth o SND)` >> prove_tac[member_types_depth])

val max_offset_def = Define `max_offset = LENGTH o component_types NONE`

(* Per the spec, a _memory array_ is defined as a contiguous memory location of
   components of the same type. The array type, the vector type as well as the
   variable part of a hybrid are all represented in the memory as memory arrays.

   Nested array, vector and variable part of hybrid can be considered as a
   single memory array with the innermost element type of the nested type as the
   element type.

   https://gitlab.anu.edu.au/mu/mu-spec/blob/master/memory.rst#array-rule
*)

val (array_type_rules, array_type_ind, array_type_cases) = Hol_reln`
    (t. array_type 0 t t)
   (off t t' n.
      off < n * max_offset t
     array_type (off MOD max_offset t) t t'
     array_type off (Array t n) t')
   (off t t' n.
      off < n * max_offset t
     array_type (off MOD max_offset t) t t'
     array_type off (Vector t n) t')
   (off fts vt t.
      SUM (MAP max_offset fts)  off
     array_type ((off - SUM (MAP max_offset fts)) MOD max_offset vt) vt t
     array_type off (Hybrid fts vt) t)
Michael Norrish's avatar
Michael Norrish committed
427
428
`

429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505

(******************************************************************************)


(* Type members, components, and prefixes have some guarantees and invariants.*)

val member_types_fixed_size = store_thm("member_types_fixed_size",

  ``t m sz. type_ok t  MEM m (member_types sz t)
            ¬variable_length_type m  m  Void``,

  rw[Once type_ok_cases] >> Cases_on `sz` >>
  fs[member_types_def, MEM_GENLIST, MEM_MAP, EVERY_MEM] >>
  fs[type_category_defs, FORALL_PROD] >> res_tac >>
  Cases_on `y` >> TRY (Cases_on `s`) >> ONCE_REWRITE_TAC[struct_fixpoint_def] >>
  fs[theorem "uvm_type_distinct"] >> rw[])

(* The invariant "type_ok" should be propagated by all functions that manipulate
   types.
*)

val type_ok_dest = store_thm("type_ok_dest",

  ``(t. type_ok (Ref (Type t))  type_ok t)
   (t. type_ok (WeakRef (Type t))  type_ok t)
   (r t. type_ok (IRef r (Type t))  type_ok t)
   (t n. type_ok (Array t n)  type_ok t)
   (t n. type_ok (Vector t n)  type_ok t)
   (ft fts vt. MEM ft fts  type_ok (Hybrid fts vt)  type_ok ft)
   (fts vt. type_ok (Hybrid fts vt)  type_ok vt)
   (fx t ts. MEM t ts  type_ok (Struct fx ts)
              type_ok (struct_fixpoint (fx, ts) t))``,

  rw[] >> pop_assum (assume_tac o ONCE_REWRITE_RULE [type_ok_cases]) >>
  fs[EVERY_MEM, MEM_MAP] >> prove_tac[])

(*
val struct_fixpoint_ok = store_thm("struct_fixpoint_ok",
  ``∀t fx ts. type_ok t ∧ EVERY type_ok ts
            ⇒ type_ok (struct_fixpoint (fx, ts) t)``,
  Induct
  rw[]
  reverse (Induct_on `t`)
  strip_tac >> measureInduct_on `uvm_type_depth t` >>
  Cases_on `t` >> TRY (Cases_on `s`) >> rw[Once struct_fixpoint_def] >>
  imp_res_tac type_ok_dest >>
  assume_tac uvm_type_depth_ord
  
  (* TODO: Continue here *)
  metis_tac[type_ok_dest, uvm_type_depth_ord, type_ok_rules]

val member_type_ok = store_thm("member_types_ok",
  ``∀t m sz. type_ok t ∧ MEM m (member_types sz t) ⇒ type_ok m``,
  rw[Once type_ok_cases] >> fs[member_types_def, MEM_GENLIST, MEM_MAP, EVERY_MEM]

val prefix_ok = store_thm("prefix_ok",
  ``∀ty pre. type_ok ty ∧ prefix_of ty pre ⇒ type_ok pre``,
)
*)

(* Note that FuncRefs are not native_safe, but are not traced either, so the
   reverse implication doesn't hold *)
(*
val native_safe_nottraced = store_thm("native_safe_nottraced",
  ``∀ty. type_ok ty ∧ native_safe ty ⇒ ¬tracedtype ty``,
  strip_tac >> measureInduct_on `uvm_type_depth ty` >>
  rw[Once native_safe_cases, Once tracedtype_cases, combinTheory.o_DEF] >>
  TRY (fs[EVERY_MEM] >> metis_tac[type_ok_dest, uvm_type_depth_ord]) >>
  Cases_on `fx = fx'` >> Cases_on `tys = tys'` >> Cases_on `MEM ty' tys'` >>
  fs[EVERY_MEM] >> res_tac
  (* TODO: need struct_fixpoint_ok to continue *)
  
  metis_tac[type_ok_dest, uvm_type_depth_ord, struct_fixpoint_same_depth]

  TRY (fs[Once type_ok_cases, Once uvm_type_depth_def] >> NO_TAC) >> rw[]
*)

506
val _ = export_theory()
507