# 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)
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
```