open HolKernel Parse boolLib bossLib

open arithmeticTheory
open listTheory
open pairTheory
open pred_setTheory
open lcsymtacs

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

val _ = Datatype `ref_type = REF | PTR`

val _ = Datatype`
  uvm_type =
  | Void
  | Int num
  | Float
  | Double
  | Ref (uvm_type + num)
  | IRef ref_type (uvm_type + num)
  | WeakRef (uvm_type + num)
  | FuncRef ref_type funcsig
  | ThreadRef
  | StackRef
  | FrameCursorRef
  | IrBuilderRef
  | TagRef64
  | Array uvm_type num
  | Vector uvm_type num
  | Hybrid (uvm_type list) uvm_type
  | Struct num (uvm_type list) ;

  funcsig = <|
    arg_types: uvm_type list;
    return_types: uvm_type list
  |>
`

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.
*)

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

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
*)

val floating_point_type_def = Define`
  floating_point_type = {Float; Double}
`

val object_referent_type_def = Define`
  object_referent_type = {Ref r | T} ∪ {WeakRef r | T}
`

val reference_type_def = Define`
  reference_type = {IRef REF r | T} ∪ object_referent_type
`

val opaque_reference_type_def = Define`
  opaque_reference_type =
    {FuncRef REF sig | T}
  ∪ {ThreadRef; StackRef; FrameCursorRef; IrBuilderRef}
`

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}
`

val scalar_type_def = Define`
  scalar_type =
    {Int n | T} ∪ floating_point_type ∪ pointer_type ∪
    general_reference_type ∪ {TagRef64}
`

val composite_type_def = Define`
  composite_type =
    {Struct fx ts | T} ∪ {Hybrid fts vt | T} ∪ {Array t n | T} ∪
    {Vector t n | T}
`

val variable_length_type_def = Define`
  variable_length_type = {Hybrid fts vt | T}
`

val eq_comparable_type_def = Define`
  eq_comparable_type =
    {Int n | T} ∪ pointer_type ∪ {Ref r | T} ∪ {IRef REF r | T} ∪
    opaque_reference_type
`

val ult_comparable_type_def = Define`
  ult_comparable_type = {Int n | T} ∪ {IRef REF r | T} ∪ pointer_type
`

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. *)
val (tracedtype_rules, tracedtype_ind, tracedtype_cases) = Hol_reln`
    (∀ty. tracedtype (Ref ty))
  ∧ (∀ty. tracedtype (IRef REF ty))
  ∧ (∀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
  ∧ (∀fixty varty.
      (EXISTS tracedtype fixty ∨ tracedtype varty)
    ⇒ tracedtype (Hybrid fixty varty))
  ∧ (∀fx ty tys.
      tracedtype ty ∧ MEM ty tys
    ⇒ tracedtype (Struct fx tys))
`

(* A native-safe type can be handed off to the "native" world. *)
val (native_safe_rules, native_safe_ind, native_safe_cases) = Hol_reln`
    (∀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))
  ∧ (∀ty. native_safe (IRef PTR ty))
  ∧ (∀sig. native_safe (FuncRef PTR sig))
  ∧ (∀fty vty.
      EVERY native_safe fty ∧ native_safe vty
    ⇒ native_safe (Hybrid fty vty))
  ∧ (∀fx tys.
      EVERY native_safe tys
    ⇒ native_safe (Struct fx tys))
`

(*
   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
`


(* 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))
`

(* Per the spec:

   ∙ 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
`

(* The function "component_types" returns a list of lists, representing the
   types that can be used to access each offset of the parent type.
   
   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
    | [] => [[t]]
    | ts => (let ts' = LIST_BIND ts (component_types NONE) in
             SNOC t (HD ts')::TL ts')
` (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)
`


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


(* 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[]
*)

val _ = export_theory()