Theory Inca

theory Inca
  imports Global OpInl Env Dynamic
    "VeriComp.Language"
begin


section ‹Inline caching›

subsection ‹Static representation›

datatype ('dyn, 'var, 'fun, 'label, 'op, 'opinl) instr =
  IPush 'dyn |
  IPop |
  IGet nat |
  ISet nat |
  ILoad 'var |
  IStore 'var |
  IOp 'op |
  IOpInl 'opinl |
  is_jump: ICJump 'label 'label |
  ICall 'fun |
  is_return: IReturn

locale inca =
  Fenv: env F_empty F_get F_add F_to_list +
  Henv: env heap_empty heap_get heap_add heap_to_list +
  dynval uninitialized is_true is_false +
  nary_operations_inl 𝔒𝔭 𝔄𝔯𝔦𝔱𝔶 ℑ𝔫𝔩𝔒𝔭 ℑ𝔫𝔩 ℑ𝔰ℑ𝔫𝔩 𝔇𝔢ℑ𝔫𝔩
  for
    ― ‹Functions environment›
    F_empty and
    F_get :: "'fenv ⇒ 'fun ⇒ ('label, ('dyn, 'var, 'fun, 'label, 'op, 'opinl) 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

    ― ‹n-ary operations›
    𝔒𝔭 :: "'op ⇒ 'dyn list ⇒ 'dyn" and 𝔄𝔯𝔦𝔱𝔶 and
    ℑ𝔫𝔩𝔒𝔭 and ℑ𝔫𝔩 and ℑ𝔰ℑ𝔫𝔩 and 𝔇𝔢ℑ𝔫𝔩 :: "'opinl ⇒ 'op"
begin


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 (d # Σ) # st)" |

  step_pop:
    "next_instr (F_get F) f l pc = Some IPop ⟹
    State F H (Frame f l pc R (d # Σ) # 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 ⟹ d = R ! n ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (d # Σ) # st)" |

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

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

  step_store:
    "next_instr (F_get F) f l pc = Some (IStore x) ⟹
    heap_add H (x, y) d = H' ⟹
    State F H (Frame f l pc R (y # d # Σ) # 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 Σ ⟹ ℑ𝔫𝔩 op (take ar Σ) = None ⟹
    𝔒𝔭 op (take ar Σ) = x ⟹
    State F H (Frame f l pc R Σ # st) → State F H (Frame f l (Suc pc) R (x # drop ar Σ) # st)" |

  step_op_inl:
    "next_instr (F_get F) f l pc = Some (IOp op) ⟹
    𝔄𝔯𝔦𝔱𝔶 op = ar ⟹ ar ≤ length Σ ⟹ ℑ𝔫𝔩 op (take ar Σ) = Some opinl ⟹
    ℑ𝔫𝔩𝔒𝔭 opinl (take ar Σ) = 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 (x # drop ar Σ) # st)" |

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

  step_op_inl_miss:
    "next_instr (F_get F) f l pc = Some (IOpInl opinl) ⟹
    𝔄𝔯𝔦𝔱𝔶 (𝔇𝔢ℑ𝔫𝔩 opinl) = ar ⟹ ar ≤ length Σ ⟹ ¬ ℑ𝔰ℑ𝔫𝔩 opinl (take ar Σ) ⟹
    ℑ𝔫𝔩𝔒𝔭 opinl (take ar Σ) = 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 (x # drop ar Σ) # st)" |

  step_cjump:
    "next_instr (F_get F) f l pc = Some (ICJump lt lf) ⟹
    is_true d ∧ l' = lt ∨ is_false d ∧ l' = lf ⟹
    State F H (Frame f l pc R (d # Σ) # 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 Σ ⟹
    frameg = allocate_frame g gd (take (arity gd) Σ) uninitialized ⟹
    State F H (Frame f l pc R Σ # st) → State F H (frameg # Frame f l pc R Σ # 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 ⟹ 
    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 elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto elim: step.cases dest: is_true_and_is_false_implies_False) [3]
  apply (auto 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 semantics step "final F_get IReturn"
  using final_finished step_deterministic
  by unfold_locales

definition load where
  "load ≡ Global.load F_get uninitialized"

sublocale language step "final F_get IReturn" load
  by unfold_locales

end

end