Theory SM.Type_System

section ‹Type System›
theory Type_System
imports Main Gen_Scheduler_Refine Decide_Locality
begin
  text ‹Currently only a very basic type system:
    Checks that no expression contains overflowing numerals,
    and that all accessed variables exist.
›

  section ‹Typing of Programs›

  type_synonym tenv_valuation = "ident ⇀ unit"
  type_synonym tenv_fs = "tenv_valuation × tenv_valuation"

  definition ty_val :: "tenv_valuation ⇒ valuation ⇒ bool" where
    "ty_val Γ vars ≡ dom Γ = dom vars"

  abbreviation "ty_local_state Γ ls ≡ ty_val Γ (local_state.variables ls)"
  abbreviation "ty_global_state Γ gs ≡ ty_val Γ (global_state.variables gs)"

  fun ty_fs :: "tenv_fs ⇒ focused_state ⇒ bool" where
    "ty_fs (Γl, Γg) (ls,gs) ⟷ ty_local_state Γl ls ∧ ty_global_state Γg gs"

  declare ty_fs.simps[simp del]  

  fun ty_expr :: "tenv_fs ⇒ exp ⇀ unit"
  where
    "ty_expr (Γl, Γg) (e_var x) = (if x∈dom Γl ∨ x∈dom Γg then Some () else None)"
  | "ty_expr (Γl, Γg) (e_localvar x) = (if x∈dom Γl then Some () else None)"
  | "ty_expr (Γl, Γg) (e_globalvar x) = (if x∈dom Γg then Some () else None)"
  | "ty_expr _ (e_const c) = (if min_signed ≤ c ∧ c ≤ max_signed then Some () else None)"
  | "ty_expr (Γl, Γg) (e_bin bop e1 e2) = do {
      ty_expr (Γl, Γg) e1;
      ty_expr (Γl, Γg) e2;
      Some ()
    }"
  | "ty_expr (Γl, Γg) (e_un uop e) = do {
      ty_expr (Γl, Γg) e;
      Some ()
    }"

  lemma ty_expr_noerr: 
    notes [simp] = ty_fs.simps
    shows "ty_fs Γ fs ⟹ eval_exp e fs ≠ None ⟷ ty_expr Γ e ≠ None"
    apply (induction e)
    apply (cases fs, cases Γ)
    apply (auto split: option.splits simp: ty_val_def) []
    apply (cases fs, cases Γ)
    apply (auto split: option.splits simp: ty_val_def) []
    apply (cases fs, cases Γ)
    apply (auto split: option.splits simp: ty_val_def) []
    apply (cases fs, cases Γ)
    apply (auto split: option.splits simp: ty_val_def) []
    apply (cases fs, cases Γ)
    apply (auto split: option.splits Option.bind_splits simp: ty_val_def) []
    apply (cases fs, cases Γ)
    apply (auto split: option.splits simp: ty_val_def) []
    done

  lemma ty_expr_noerr': 
    "ty_fs Γ fs ⟹ ty_expr Γ e = Some () ⟷ (∃v. eval_exp e fs = Some v)"
    using ty_expr_noerr
    by auto

  type_synonym tenv_cmd = "tenv_fs × bool" 

  function ty_cmd :: "tenv_cmd ⇒ cmd ⇒ bool" where
    "ty_cmd ((Γl,Γg),loop) (Assign c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      (x∈dom Γl | x∈dom Γg) ∧ ty_expr (Γl,Γg) e ≠ None"
  | "ty_cmd ((Γl,Γg),loop) (Assign_local c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      (x∈dom Γl) ∧ ty_expr (Γl,Γg) e ≠ None"
  | "ty_cmd ((Γl,Γg),loop) (Assign_global c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      (x∈dom Γg) ∧ ty_expr (Γl,Γg) e ≠ None"
  | "ty_cmd ((Γl,Γg),loop) (Test e) ⟷ ty_expr (Γl,Γg) e ≠ None"
  | "ty_cmd ((Γl,Γg),loop) (Skip) ⟷ True"
  | "ty_cmd ((Γl,Γg),loop) (Seq c1 c2) ⟷ ty_cmd ((Γl,Γg),loop) c1 ∧ ty_cmd ((Γl,Γg),loop) c2"
  | "ty_cmd ((Γl,Γg),loop) (Or c1 c2) ⟷ ty_cmd ((Γl,Γg),loop) c1 ∧ ty_cmd ((Γl,Γg),loop) c2"
  | "ty_cmd ((Γl,Γg),loop) (Break) ⟷ loop"
  | "ty_cmd ((Γl,Γg),loop) (Continue) ⟷ loop"
  | "ty_cmd ((Γl,Γg),loop) (Iterate c1 c2) ⟷ ty_cmd ((Γl,Γg),True) c1 ∧ ty_cmd ((Γl,Γg),True) c2"
  | "ty_cmd ((Γl,Γg),loop) (Invalid) ⟷ False"
  by pat_completeness auto
  
  termination
    apply (relation "inv_image (reachable_term_order_aux <*mlex*> measure size) snd")
    apply (auto simp: mlex_prod_def)
    done
    
  theorem ty_cmd_no_internal: "ty_cmd (Γ,False) c ⟹ cfg c a c' ⟹ isl a"
    apply (rotate_tac)
    apply (induction rule: cfg.induct)
    apply (cases Γ, (auto) [])+
    done

  lemma ty_cmd_pres_aux: "ty_cmd ((Γl,Γg),loop) c ⟹ cfg c a c' ⟹ 
    (ty_cmd ((Γl,Γg),loop) c' ∨ a=Inr AIBreak ∨ a=Inr AIContinue)"  
    apply (rotate_tac)
    apply (induction arbitrary: loop rule: cfg.induct)
    apply auto
    done
  
  corollary ty_cmd_pres: 
    "ty_cmd ((Γl,Γg),False) c ⟹ cfg c a c' ⟹ ty_cmd ((Γl,Γg),False) c'"
    apply (frule (1) ty_cmd_pres_aux)
    apply (frule (1) ty_cmd_no_internal)
    apply auto
    done

  definition ty_proc_decl :: "tenv_valuation ⇒ proc_decl ⇒ bool" where
    "ty_proc_decl Γg pd ≡ let
      Γl = (λx. if x ∈ set (proc_decl.local_vars pd) then Some () else None)
    in
      ty_cmd ((Γl,Γg),False) (proc_decl.body pd)"

  definition ty_program :: "program ⇒ bool" where
    "ty_program prog == let
      Γg = (λx. if x∈set (program.global_vars prog) then Some () else None)
    in
      ∀pd∈set (program.processes prog). ty_proc_decl Γg pd"

  definition ty_local :: "cmd ⇒ local_state ⇒ global_state ⇒ bool" where
    "ty_local c ls gs ≡ ∃Γ. ty_cmd (Γ,False) c ∧ ty_fs Γ (ls,gs)"

  definition "cfg' c a c' ≡ cfg c (Inl a) c'"
  lemma cfg'_eq: "ty_cmd (Γ,False) c ⟹ cfg c a c' ⟷ (∃aa. a=Inl aa ∧ cfg' c aa c')"
    by (cases a) (auto dest: ty_cmd_no_internal[of _ c a c'] simp: cfg'_def)

  lemma cfg_eq: "ty_cmd (Γ,False) c ⟹ cfg' c a c' ⟷ cfg c (Inl a) c'" 
    by (auto simp: cfg'_eq)

  section ‹Typing of Actions›  
  text ‹
    We split the proof that steps from well-typed configurations
    do not fail and preserve well-typedness in two steps:
    
    First, we show that actions from well-types commands are well-typed.
    Then, we show that well-typed actions do not fail, and preserve 
      well-typedness.
›


  fun ty_la :: "tenv_fs ⇒ action ⇒ bool" where
    "ty_la (Γl,Γg) (AAssign c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      (x∈dom Γl ∨ x∈dom Γg) ∧ ty_expr (Γl,Γg) e ≠ None"  
  | "ty_la (Γl,Γg) (AAssign_local c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      x∈dom Γl ∧ ty_expr (Γl,Γg) e ≠ None"
  | "ty_la (Γl,Γg) (AAssign_global c x e) ⟷ ty_expr (Γl,Γg) c ≠ None ∧
      x∈dom Γg ∧ ty_expr (Γl,Γg) e ≠ None"
  | "ty_la (Γl,Γg) (ATest e) ⟷ ty_expr (Γl,Γg) e ≠ None"
  | "ty_la (Γl,Γg) (ASkip) ⟷ True"


  lemma ty_cmd_imp_ty_la_aux:
    assumes "ty_cmd (Γ,loop) c"
    assumes "cfg c (Inl a) c'"
    shows "ty_la Γ a"
    using assms (2,1)
    apply (induction c "Inl a::action+brk_ctd" c' arbitrary: loop)
    apply (case_tac [!] Γ)
    apply auto
    done

  lemma ty_cmd_imp_ty_la:
    assumes "ty_cmd (Γ,False) c"
    assumes "cfg' c a c'"
    shows "ty_la Γ a"
    using assms
    unfolding cfg_eq[OF assms(1)]
    by (rule ty_cmd_imp_ty_la_aux)

  lemma ty_en_defined:
    assumes "ty_fs Γ fs"
    assumes "ty_la Γ a"
    shows "la_en fs a ≠ None"
    using assms
    apply (cases Γ, cases fs)
    apply (cases a)
    apply (auto
      split: Option.bind_splits 
      dest: ty_expr_noerr)
    done

  lemma ty_ex_defined:  
    assumes "ty_fs Γ fs"
    assumes "ty_la Γ a"
    assumes "la_en fs a = Some True"
    shows "la_ex fs a ≠ None"
    using assms
    apply (cases Γ, cases fs)
    apply (cases a)
    apply (auto
      split: Option.bind_splits 
      dest: ty_expr_noerr, 
      auto simp: ty_val_def ty_fs.simps)
    apply blast+
    done

  lemma ty_ex_pres:
    assumes "ty_fs Γ fs"
    assumes "la_ex fs a = Some fs'"
    shows "ty_fs Γ fs'"
    using assms
    apply (cases Γ, cases fs)
    apply (cases a)
    apply (auto
      split: Option.bind_splits if_split_asm 
      dest: ty_expr_noerr, 
      auto simp: ty_val_def ty_fs.simps)
    done


  section ‹Actions that do not fail›  

  text ‹
    We define a refinement of the actions, which 
    map failure to not enabled/identity.
    
    This allows for simple POR-related proofs, as non-failure can
    be assumed.
  ›
  definition "la_en' fs a ≡ case la_en fs a of Some b ⇒ b | None ⇒ False"
  definition "la_ex' fs a ≡ case la_ex fs a of Some fs' ⇒ fs' | None ⇒ fs"

  interpretation li': Gen_Scheduler'_linit cfg' la_en' la_ex' "{init_gc prog}" global_config.state
    for prog .

  interpretation li': sched_typing
    cfg la_en la_ex
    cfg' la_en' la_ex'
    ty_local
    apply unfold_locales
    unfolding ty_local_def
    apply (auto 
      simp: cfg'_eq
      simp: la_en'_def dest: ty_en_defined[OF _ ty_cmd_imp_ty_la]
      simp: la_ex'_def dest: ty_ex_defined[OF _ ty_cmd_imp_ty_la]
      dest: ty_ex_pres ty_cmd_pres
      split: option.splits
      ) [4]

    apply (clarsimp)
    apply (intro exI conjI)
    apply assumption+
    apply (frule (1) ty_ex_pres)
    apply (simp add: ty_val_def ty_fs.simps)
    done
    
  locale well_typed_prog =
    fixes prog
    assumes well_typed_prog: "ty_program prog"
  begin
    lemma ty_init[simp, intro!]: "li'.wf_gglobal (init_gc prog)"
      using well_typed_prog
      apply (auto 
        simp: in_multiset_in_set
        simp: init_gc_def init_pc_def li'.wf_gglobal_def ty_local_def
        simp: ty_program_def ty_proc_decl_def
        dest!: split_list)
      apply (intro exI conjI)
      apply assumption
      apply (auto 
        simp: ty_fs.simps ty_val_def init_valuation_def 
        split: if_split_asm
        )
      done
 
    sublocale li': sched_typing_init
      cfg la_en la_ex
      cfg' la_en' la_ex'
      "{init_gc prog}" global_config.state
      ty_local
      apply unfold_locales
      by auto

    lemma "li'.sa.accept prog = ref_accept prog"  
      by (rule li'.accept_eq)

    lemma "ref_is_run prog r ⟷ (∃r'. r=Some o r' ∧ li'.sa.is_run prog r')"  
      by (rule li'.is_run_conv)

  end

end