Theory Ubx

theory Ubx
  imports Global OpUbx Env
    "VeriComp.Language"
begin


section ‹Unboxed caching›

subsection ‹Static representation›

datatype ('dyn, 'var, 'fun, 'label, 'op, 'opinl, 'opubx, 'num, 'bool) instr =
  IPush 'dyn | IPushUbx1 'num | IPushUbx2 'bool |
  IPop |
  IGet nat | IGetUbx type nat |
  ISet nat | ISetUbx type nat |
  ILoad 'var | ILoadUbx type 'var |
  IStore 'var | IStoreUbx type 'var |
  IOp 'op | IOpInl 'opinl | IOpUbx 'opubx |
  is_jump: ICJump 'label 'label |
  is_fun_call: ICall 'fun |
  is_return: IReturn

locale ubx =
  Fenv: env F_empty F_get F_add F_to_list +
  Henv: env heap_empty heap_get heap_add heap_to_list +
  nary_operations_ubx
    𝔒𝔭 𝔄𝔯𝔦𝔱𝔶
    ℑ𝔫𝔩𝔒𝔭 ℑ𝔫𝔩 ℑ𝔰ℑ𝔫𝔩 𝔇𝔢ℑ𝔫𝔩
    uninitialized is_true is_false box_ubx1 unbox_ubx1 box_ubx2 unbox_ubx2
    𝔘𝔟𝔵𝔒𝔭 𝔘𝔟𝔵 𝔅𝔬𝔵 𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭
  for
    ― ‹Functions environment›
    F_empty and
    F_get :: "'fenv ⇒ 'fun ⇒ ('label, ('dyn, 'var, 'fun, 'label, 'op, 'opinl, 'opubx, 'num, 'bool) instr) fundef option" and
    F_add and F_to_list and

    ― ‹Memory heap›
    heap_empty and
    heap_get :: "'henv ⇒ 'var × 'dyn ⇒ 'dyn option" and
    heap_add and heap_to_list and

    ― ‹Dynamic values›
    uninitialized :: 'dyn and is_true and is_false and

    ― ‹Unboxed values›
    box_ubx1 and unbox_ubx1 and
    box_ubx2 and unbox_ubx2 and

    ― ‹n-ary operations›
    𝔒𝔭 :: "'op ⇒ 'dyn list ⇒ 'dyn" and 𝔄𝔯𝔦𝔱𝔶 and
    ℑ𝔫𝔩𝔒𝔭 and ℑ𝔫𝔩 and ℑ𝔰ℑ𝔫𝔩 and 𝔇𝔢ℑ𝔫𝔩 :: "'opinl ⇒ 'op" and
    𝔘𝔟𝔵𝔒𝔭 :: "'opubx ⇒ ('dyn, 'num, 'bool) unboxed list ⇒ ('dyn, 'num, 'bool) unboxed option" and
    𝔘𝔟𝔵 :: "'opinl ⇒ type option list ⇒ 'opubx option" and
    𝔅𝔬𝔵 :: "'opubx ⇒ 'opinl" and
    𝔗𝔶𝔭𝔢𝔒𝔣𝔒𝔭
begin


lemmas map_option_funtype_comp_map_entry_rewrite_fundef_body[simp] =
  Fenv.map_option_comp_map_entry[of _ funtype "λfd. rewrite_fundef_body fd l pc instr" for l pc instr, simplified]

fun generalize_instr where
  "generalize_instr (IPushUbx1 n) = IPush (box_ubx1 n)" |
  "generalize_instr (IPushUbx2 b) = IPush (box_ubx2 b)" |
  "generalize_instr (IGetUbx _ n) = IGet n" |
  "generalize_instr (ISetUbx _ n) = ISet n" |
  "generalize_instr (ILoadUbx _ x) = ILoad x" |
  "generalize_instr (IStoreUbx _ x) = IStore x" |
  "generalize_instr (IOpUbx opubx) = IOpInl (𝔅𝔬𝔵 opubx)" |
  "generalize_instr instr = instr"

lemma instr_sel_generalize_instr[simp]:
  "is_jump (generalize_instr instr) ⟷ is_jump instr"
  "is_fun_call (generalize_instr instr) ⟷ is_fun_call instr"
  "is_return (generalize_instr instr) ⟷ is_return instr"
  unfolding atomize_conj
  by (cases instr; simp)

lemma instr_sel_generalize_instr_comp[simp]:
  "is_jump ∘ generalize_instr = is_jump" and
  "is_fun_call ∘ generalize_instr = is_fun_call" and
  "is_return ∘ generalize_instr = is_return"
  unfolding atomize_conj
  using instr_sel_generalize_instr by auto

fun generalize_fundef where
  "generalize_fundef (Fundef xs ar ret locals) =
    Fundef (map_ran (λ_. map generalize_instr) xs) ar ret locals"

lemma generalize_instr_idempotent[simp]:
  "generalize_instr (generalize_instr x) = generalize_instr x"
  by (cases x) simp_all

lemma generalize_instr_idempotent_comp[simp]:
  "generalize_instr ∘ generalize_instr = generalize_instr"
  by fastforce

lemma length_body_generalize_fundef[simp]: "length (body (generalize_fundef fd)) = length (body fd)"
  by (cases fd) (simp add: map_ran_def)

lemma arity_generalize_fundef[simp]: "arity (generalize_fundef fd) = arity fd"
  by (cases fd) simp

lemma return_generalize_fundef[simp]: "return (generalize_fundef fd) = return fd"
  by (cases fd) simp

lemma fundef_locals_generalize[simp]: "fundef_locals (generalize_fundef fd) = fundef_locals fd"
  by (cases fd; simp)

lemma funtype_generalize_fundef[simp]: "funtype (generalize_fundef fd) = funtype fd"
  by (cases fd; simp add: funtype_def)

lemmas map_option_comp_map_entry_generalize_fundef[simp] =
  Fenv.map_option_comp_map_entry[of _ funtype generalize_fundef, simplified]

lemma image_fst_set_body_generalize_fundef[simp]:
  "fst ` set (body (generalize_fundef fd)) = fst ` set (body fd)"
  by (cases fd) (simp add: dom_map_ran)

lemma map_of_generalize_fundef_conv:
  "map_of (body (generalize_fundef fd)) l = map_option (map generalize_instr) (map_of (body fd) l)"
  by (cases fd) (simp add: map_ran_conv)

lemma map_option_arity_get_map_entry_generalize_fundef[simp]:
  "map_option arity ∘ F_get (Fenv.map_entry F2 f generalize_fundef) =
   map_option arity ∘ F_get F2"
  by (auto intro: Fenv.map_option_comp_map_entry)

lemma instr_at_generalize_fundef_conv:
  "instr_at (generalize_fundef fd) l = map_option generalize_instr o instr_at fd l"
proof (intro ext)
  fix n
  show "instr_at (generalize_fundef fd) l n = (map_option generalize_instr ∘ instr_at fd l) n"
  proof (cases fd)
    case (Fundef bblocks ar locals)
    then show ?thesis
      by (cases "map_of bblocks l") (simp_all add: instr_at_def map_ran_conv)
  qed
qed


subsection ‹Semantics›

inductive step (infix ‹→› 55) where
  step_push:
    "next_instr (F_get F) f l pc = Some (IPush d) ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpDyn d # Σ) # st)" |

  step_push_ubx1:
    "next_instr (F_get F) f l pc = Some (IPushUbx1 n) ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpUbx1 n # Σ) # st)" |

  step_push_ubx2:
    "next_instr (F_get F) f l pc = Some (IPushUbx2 b) ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpUbx2 b # Σ) # st)" |

  step_pop:
    "next_instr (F_get F) f l pc = Some IPop ⟹
    State F H (Frame f l pc R (x # Σ) # st) → State F H (Frame f l (Suc pc) R Σ # st)" |

  step_get:
    "next_instr (F_get F) f l pc = Some (IGet n) ⟹
    n < length R ⟹ cast_Dyn (R ! n) = Some d ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpDyn d # Σ) # st)" |

  step_get_ubx_hit:
    "next_instr (F_get F) f l pc = Some (IGetUbx τ n) ⟹
    n < length R ⟹ cast_Dyn (R ! n) = Some d ⟹ unbox τ d = Some blob ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (blob # Σ) # st)" |

  step_get_ubx_miss:
    "next_instr (F_get F) f l pc = Some (IGetUbx τ n) ⟹
    n < length R ⟹ cast_Dyn (R ! n) = Some d ⟹ unbox τ d = None ⟹
    F' = Fenv.map_entry F f generalize_fundef ⟹
    State F H (Frame f l pc R Σ # st) → State F' H (box_stack f (Frame f l (Suc pc) R (OpDyn d # Σ) # st))" |

  step_set:
    "next_instr (F_get F) f l pc = Some (ISet n) ⟹
    n < length R ⟹ cast_Dyn blob = Some d ⟹ R' = R[n := OpDyn d] ⟹
    State F H (Frame f l pc R (blob # Σ) # st) → State F H (Frame f l (Suc pc) R' Σ # st)" |

  step_set_ubx:
    "next_instr (F_get F) f l pc = Some (ISetUbx τ n) ⟹
    n < length R ⟹ cast_and_box τ blob = Some d ⟹ R' = R[n := OpDyn d] ⟹
    State F H (Frame f l pc R (blob # Σ) # st) → State F H (Frame f l (Suc pc) R' Σ # st)" |

  step_load:
    "next_instr (F_get F) f l pc = Some (ILoad x) ⟹
    cast_Dyn i = Some i' ⟹ heap_get H (x, i') = Some d ⟹
    State F H (Frame f l pc R (i # Σ) # st) → State F H (Frame f l (Suc pc) R (OpDyn d # Σ) # st)" |

  step_load_ubx_hit:
    "next_instr (F_get F) f l pc = Some (ILoadUbx τ x) ⟹
    cast_Dyn i = Some i' ⟹ heap_get H (x, i') = Some d ⟹ unbox τ d = Some blob ⟹
    State F H (Frame f l pc R (i # Σ) # st) → State F H (Frame f l (Suc pc) R (blob # Σ) # st)" |

  step_load_ubx_miss:
    "next_instr (F_get F) f l pc = Some (ILoadUbx τ x) ⟹
    cast_Dyn i = Some i' ⟹ heap_get H (x, i') = Some d ⟹ unbox τ d = None ⟹
    F' = Fenv.map_entry F f generalize_fundef ⟹
    State F H (Frame f l pc R (i # Σ) # st) → State F' H (box_stack f (Frame f l (Suc pc) R (OpDyn d # Σ) # st))"  |

  step_store:
    "next_instr (F_get F) f l pc = Some (IStore x) ⟹
    cast_Dyn i = Some i' ⟹ cast_Dyn y = Some d ⟹ heap_add H (x, i') d = H' ⟹
    State F H (Frame f l pc R (i # y # Σ) # st) → State F H' (Frame f l (Suc pc) R Σ # st)" |

  step_store_ubx:
    "next_instr (F_get F) f l pc = Some (IStoreUbx τ x) ⟹
    cast_Dyn i = Some i' ⟹ cast_and_box τ blob = Some d ⟹ heap_add H (x, i') d = H' ⟹
    State F H (Frame f l pc R (i # blob # Σ) # st) → State F H' (Frame f l (Suc pc) R Σ # st)" |

  step_op:
    "next_instr (F_get F) f l pc = Some (IOp op) ⟹
    𝔄𝔯𝔦𝔱𝔶 op = ar ⟹ ar ≤ length Σ ⟹
    ap_map_list cast_Dyn (take ar Σ) = Some Σ' ⟹
    ℑ𝔫𝔩 op Σ' = None ⟹ 𝔒𝔭 op Σ' = x ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpDyn x # drop ar Σ) # st)" |

  step_op_inl:
    "next_instr (F_get F) f l pc = Some (IOp op) ⟹
    𝔄𝔯𝔦𝔱𝔶 op = ar ⟹ ar ≤ length Σ ⟹
    ap_map_list cast_Dyn (take ar Σ) = Some Σ' ⟹
    ℑ𝔫𝔩 op Σ' = Some opinl ⟹ ℑ𝔫𝔩𝔒𝔭 opinl Σ' = x ⟹
    F' = Fenv.map_entry F f (λfd. rewrite_fundef_body fd l pc (IOpInl opinl)) ⟹
    State F H (Frame f l pc R Σ # st) → State F' H (Frame f l (Suc pc) R (OpDyn x # drop ar Σ) # st)" |

  step_op_inl_hit:
    "next_instr (F_get F) f l pc = Some (IOpInl opinl) ⟹
    𝔄𝔯𝔦𝔱𝔶 (𝔇𝔢ℑ𝔫𝔩 opinl) = ar ⟹ ar ≤ length Σ ⟹
    ap_map_list cast_Dyn (take ar Σ) = Some Σ' ⟹
    ℑ𝔰ℑ𝔫𝔩 opinl Σ' ⟹ ℑ𝔫𝔩𝔒𝔭 opinl Σ' = x ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (OpDyn x # drop ar Σ) # st)" |

  step_op_inl_miss:
    "next_instr (F_get F) f l pc = Some (IOpInl opinl) ⟹
    𝔄𝔯𝔦𝔱𝔶 (𝔇𝔢ℑ𝔫𝔩 opinl) = ar ⟹ ar ≤ length Σ ⟹
    ap_map_list cast_Dyn (take ar Σ) = Some Σ' ⟹
    ¬ ℑ𝔰ℑ𝔫𝔩 opinl Σ' ⟹ ℑ𝔫𝔩𝔒𝔭 opinl Σ' = x ⟹
    F' = Fenv.map_entry F f (λfd. rewrite_fundef_body fd l pc (IOp (𝔇𝔢ℑ𝔫𝔩 opinl))) ⟹
    State F H (Frame f l pc R Σ # st) → State F' H (Frame f l (Suc pc) R (OpDyn x # drop ar Σ) # st)" |

  step_op_ubx:
    "next_instr (F_get F) f l pc = Some (IOpUbx opubx) ⟹
    𝔇𝔢ℑ𝔫𝔩 (𝔅𝔬𝔵 opubx) = op ⟹ 𝔄𝔯𝔦𝔱𝔶 op = ar ⟹ ar ≤ length Σ ⟹
    𝔘𝔟𝔵𝔒𝔭 opubx (take ar Σ) = Some x ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (x # drop ar Σ) # st)" |

  step_cjump:
    "next_instr (F_get F) f l pc = Some (ICJump lt lf) ⟹
    cast_Dyn y = Some d ⟹ is_true d ∧ l' = lt ∨ is_false d ∧ l' = lf ⟹
    State F H (Frame f l pc R (y # Σ) # st) → State F H (Frame f l' 0 R Σ # st)" |

  step_call:
    "next_instr (F_get F) f l pc = Some (ICall g) ⟹
    F_get F g = Some gd ⟹ arity gd ≤ length Σ ⟹
    list_all is_dyn_operand (take (arity gd) Σ) ⟹
    frameg = allocate_frame g gd (take (arity gd) Σ) (OpDyn uninitialized) ⟹
    State F H (Frame f l pc Rf Σ # st) → State F H (frameg # Frame f l pc Rf Σ # st)" |

  step_return:
    "next_instr (F_get F) g lg pcg = Some IReturn ⟹
    F_get F g = Some gd ⟹ arity gd ≤ length Σf ⟹
    length Σg = return gd ⟹ list_all is_dyn_operand Σg ⟹
    framef' = Frame f lf (Suc pcf) Rf (Σg @ drop (arity gd) Σf) ⟹
    State F H (Frame g lg pcg Rg Σg # Frame f lf pcf Rf Σf # st) → State F H (framef' # st)"

lemma step_deterministic:
  assumes "s1 → s2" and "s1 → s3"
  shows "s2 = s3"
  using assms
  apply (cases s1 s2 rule: step.cases)
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim!: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto simp: next_instr_length_instrs elim!: step.cases dest: is_true_and_is_false_implies_False) [1]
  done

lemma step_right_unique: "right_unique step"
  using step_deterministic
  by (rule right_uniqueI)

lemma final_finished:
  assumes "final F_get IReturn s"
  shows "finished step s"
  unfolding finished_def
proof (rule notI)
  assume "∃x. step s x"
  then obtain s' where "step s s'" by auto
  thus False
    using ‹final F_get IReturn s›
    by (auto simp: state_ok_def elim!: step.cases final.cases)
qed

sublocale ubx_sem: semantics step "final F_get IReturn"
  using final_finished step_deterministic
  by unfold_locales

definition load where
  "load ≡ Global.load F_get (OpDyn uninitialized)"

sublocale inca_lang: language step "final F_get IReturn" load
  by unfold_locales

end

end