Theory Std

theory Std
  imports List_util Global Op Env Dynamic
    "VeriComp.Language"
begin


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

locale std =
  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 𝔒𝔭 𝔄𝔯𝔦𝔱𝔶
  for
    ― ‹Functions environment›
    F_empty and
    F_get :: "'fenv  'fun  ('label, ('dyn, 'var, 'fun, 'label, 'op) 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 𝔄𝔯𝔦𝔱𝔶
begin

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 Σ) = 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) 
    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) [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