section ‹General purpose definitions and lemmas›

theory Misc imports 
  Main
begin

text ‹A handy abbreviation when working with maps›
abbreviation make_map :: "'a set ⇒ 'b ⇒ ('a ⇀ 'b)" ("[ _ |=> _ ]")
where
  "[ks |=> v] ≡ λk. if k ∈ ks then Some v else None"

text ‹Projecting the components of a triple›
definition "fst3 ≡ fst"
definition "snd3 ≡ fst ∘ snd"
definition "thd3 ≡ snd ∘ snd"

lemma fst3_simp [simp]: "fst3 (a,b,c) = a" by (simp add: fst3_def)
lemma snd3_simp [simp]: "snd3 (a,b,c) = b" by (simp add: snd3_def)
lemma thd3_simp [simp]: "thd3 (a,b,c) = c" by (simp add: thd3_def)

end

section ‹Syntax of KPL›

theory KPL_syntax imports 
  Misc
begin

text‹Locations of local variables›
typedecl V 

text ‹C strings›
typedecl name

text ‹Procedure names›
typedecl proc_name

text ‹Local-id, group-id›
type_synonym lid = nat
type_synonym gid = nat

text ‹Fully-qualified thread-id›
type_synonym tid = "gid × lid"

text ‹Let @{term "(G,T)"} range over threadsets›
type_synonym threadset = "gid set × (gid ⇀ lid set)"

text ‹Returns the set of tids in a threadset›
fun tids :: "threadset ⇒ tid set"
where
  "tids (G,T) = {(i,j) | i j. i ∈ G ∧ j ∈ the (T i)}"

type_synonym word = nat  (* should really be machine words *)

datatype loc =
  Name name
| Var V

text ‹Local expressions›
datatype local_expr =
  Loc loc
| Gid
| Lid
| eTrue
| eConj local_expr local_expr  (infixl "∧*" 50)
| eNot local_expr              ("¬*")

text ‹Basic statements›
datatype basic_stmt =
  Assign loc local_expr
| Read loc local_expr
| Write local_expr local_expr

text ‹Statements›
datatype stmt =
  Basic basic_stmt
| Seq stmt stmt (infixl ";;" 50)
| Local name stmt
| If local_expr stmt stmt
| While local_expr stmt
| WhileDyn local_expr stmt
| Call proc_name local_expr
| Barrier
| Break
| Continue
| Return

text ‹Procedures comprise a procedure name, parameter name, and a body statement›
record proc = 
  proc_name :: proc_name
  param :: name
  body :: stmt

text ‹Kernels›
record kernel = 
  groups :: nat
  threads :: nat
  procs :: "proc list"
  main :: stmt

end

section ‹Well-formedness of KPL kernels›

theory KPL_wellformedness imports 
  KPL_syntax
begin

text ‹
  Well-formed local expressions. @{term "wf_local_expr ns e"} 
  means that 
  \begin{itemize} 
  \item @{term e} does not mention any internal locations, and
  \item any name mentioned by @{term e} is in the set @{term ns}.
  \end{itemize}
›
fun wf_local_expr :: "name set ⇒ local_expr ⇒ bool"
where
  "wf_local_expr ns (Loc (Var j)) = False"
| "wf_local_expr ns (Loc (Name n)) = (n ∈ ns)"
| "wf_local_expr ns (e1 ∧* e2) =
  (wf_local_expr ns e1 ∧ wf_local_expr ns e2)"
| "wf_local_expr ns (¬* e) = wf_local_expr ns e"
| "wf_local_expr ns _ = True"

text ‹
  Well-formed basic statements. @{term "wf_basic_stmt ns b"} 
  means that 
  \begin{itemize}
  \item @{term b} does not mention any internal locations, and
  \item any name mentioned by @{term b} is in the set @{term ns}.
  \end{itemize}
›
fun wf_basic_stmt :: "name set ⇒ basic_stmt ⇒ bool"
where
  "wf_basic_stmt ns (Assign x e) = wf_local_expr ns e"
| "wf_basic_stmt ns (Read x e) = wf_local_expr ns e"
| "wf_basic_stmt ns (Write e1 e2) = 
  (wf_local_expr ns e1 ∧ wf_local_expr ns e2)"

text ‹
  Well-formed statements. @{term "wf_stmt ns F S"} means:
  \begin{itemize}
  \item @{term S} only calls procedures whose name is in @{term F},
  \item @{term S} does not contain @{term WhileDyn}, 
  \item @{term S} does not mention internal variables, 
  \item @{term S} only mentions names in @{term ns}, and
  \item @{term S} does not declare the same name twice, e.g. @{term "Local x (Local x foo)"}.
  \end{itemize}
›
fun wf_stmt :: "name set ⇒ proc_name set ⇒ stmt ⇒ bool"
where
  "wf_stmt ns F (Basic b) = wf_basic_stmt ns b"
| "wf_stmt ns F (S1 ;; S2) = (wf_stmt ns F S1 ∧ wf_stmt ns F S2)"
| "wf_stmt ns F (Local n S) = (n ∉ ns ∧ wf_stmt ({n} ∪ ns) F S)"
| "wf_stmt ns F (If e S1 S2) = 
  (wf_local_expr ns e ∧ wf_stmt ns F S1 ∧ wf_stmt ns F S2)"
| "wf_stmt ns F (While e S) = 
  (wf_local_expr ns e ∧ wf_stmt ns F S)"
| "wf_stmt ns F (WhileDyn _ _) = False"
| "wf_stmt ns F (Call f e) = (f ∈ F ∧ wf_local_expr ns e)"
| "wf_stmt _ _ _ = True"

text ‹@{term "no_return S"} holds if @{term S} does not contain a @{term Return} statement›
fun no_return :: "stmt ⇒ bool"
where
  "no_return (S1 ;; S2) = (no_return S1 ∧ no_return S2)"
| "no_return (Local n S) = no_return S"
| "no_return (If e S1 S2) = (no_return S1 ∧ no_return S2)"
| "no_return (While e S) = (no_return S)"
| "no_return Return = False"
| "no_return _ = True"

text ‹Well-formed kernel›
definition wf_kernel :: "kernel ⇒ bool"
where
  "wf_kernel P ≡
  let F = set (map proc_name (procs P)) in
 
  ― ‹The main statement must not refer to ∗‹any› variable, except those it locally defines.›
  wf_stmt {} F (main P)

  ― ‹The main statement contains no return statement.›
∧ no_return (main P)
 
  ― ‹A procedure body may refer only to its argument.›
∧ list_all (λf. wf_stmt {param f} F (body f)) (procs P)"


end

section ‹Thread, group and kernel states›

theory KPL_state imports 
  KPL_syntax
begin

text ‹Thread state›
record thread_state =
  (* We use "V + bool" to indicate that the domain of
     l is extended with two extra values. Let's say
     that "l (Inr True)" returns the gid, and that
     "l (Inr False)" returns the lid. *)
  l :: "V + bool ⇒ word" 
  sh :: "nat ⇒ word"
  R :: "nat set"
  W :: "nat set"

abbreviation "GID ≡ Inr True"
abbreviation "LID ≡ Inr False"

text ‹Group state›
record group_state = 
  thread_states :: "lid ⇀ thread_state" ("_ ⇩t⇩s" [1000] 1000)
  R_group :: "(lid × nat) set"
  W_group :: "(lid × nat) set"

text ‹Valid group state›
fun valid_group_state :: "(gid ⇀ lid set) ⇒ gid ⇒ group_state ⇒ bool"
where
  "valid_group_state T i γ = (
  dom (γ ⇩t⇩s) = the (T i) ∧
  (∀j ∈ the (T i).
  l (the (γ ⇩t⇩s j)) GID = i ∧
  l (the (γ ⇩t⇩s j)) LID = j))"

text ‹Predicated statements›
type_synonym pred_stmt = "stmt × local_expr"
type_synonym pred_basic_stmt = "basic_stmt × local_expr"

text ‹Kernel state›
type_synonym kernel_state = 
  "(gid ⇀ group_state) × pred_stmt list × V list"

text ‹Valid kernel state›
fun valid_kernel_state :: "threadset ⇒ kernel_state ⇒ bool"
where
  "valid_kernel_state (G,T) (κ, ss, _) = (
  dom κ = G ∧
  (∀i ∈ G. valid_group_state T i (the (κ i))))"

text ‹Valid initial kernel state›
fun valid_initial_kernel_state :: "stmt ⇒ threadset ⇒ kernel_state ⇒ bool"
where
  "valid_initial_kernel_state S (G,T) (κ, ss, vs) = ( 
  valid_kernel_state (G,T) (κ, ss, vs) ∧
  (ss = [(S, eTrue)]) ∧
  (∀i ∈ G. R_group (the (κ i)) = {} ∧ W_group (the (κ i)) = {}) ∧
  (∀i ∈ G. ∀j ∈ the (T i). R (the ((the (κ i))⇩t⇩s j)) = {}
    ∧ W (the ((the (κ i))⇩t⇩s j)) = {}) ∧
  (∀i ∈ G. ∀j ∈ the (T i). ∀v :: V. 
    l (the ((the (κ i))⇩t⇩s j)) (Inl v) = 0) ∧
  (∀i ∈ G. ∀i' ∈ G. ∀j ∈ the (T i). ∀j' ∈ the (T i').
    sh (the ((the (κ i))⇩t⇩s j)) = 
    sh (the ((the (κ i'))⇩t⇩s j'))) ∧
  (vs = []))"

end

section ‹Execution rules for threads›

theory KPL_execution_thread imports 
  KPL_state
begin

text ‹Evaluate a local expression down to a word›
fun eval_word :: "local_expr ⇒ thread_state ⇒ word"
where
  "eval_word (Loc (Var v)) τ = l τ (Inl v)"
(* eval_word (Loc (Name n)) τ = undefined *)
| "eval_word Lid τ = l τ LID"
| "eval_word Gid τ = l τ GID"
| "eval_word eTrue τ = 1"
| "eval_word (e1 ∧* e2) τ = 
  (eval_word e1 τ * eval_word e2 τ)"
| "eval_word (¬* e) τ = (if eval_word e τ = 0 then 1 else 0)"

text ‹Evaluate a local expression down to a boolean›
fun eval_bool :: "local_expr ⇒ thread_state ⇒ bool"
where
  "eval_bool e τ = (eval_word e τ ≠ 0)"

text ‹Abstraction level: none, equality abstraction, or adversarial abstraction›
datatype abs_level = No_Abst | Eq_Abst | Adv_Abst

text ‹The rules of Figure 4, plus two additional rules 
  for adversarial abstraction (Fig 7b)›
inductive step_t 
  :: "abs_level ⇒ (thread_state × pred_basic_stmt) ⇒ thread_state ⇒ bool"  
where
  T_Disabled: 
  "¬ (eval_bool p τ) ⟹ step_t a (τ, (b, p)) τ"
| T_Assign: 
  "⟦ eval_bool p τ ; l' = (l τ) (Inl v := eval_word e τ) ⟧ 
  ⟹ step_t a (τ, (Assign (Var v) e, p)) (τ (| l := l' |))"
| T_Read: 
  "⟦ eval_bool p τ ; l' = (l τ) (Inl v := sh τ (eval_word e τ)) ;
  R' = R τ ∪ { eval_word e τ } ; a ∈ {No_Abst, Eq_Abst} ⟧ 
  ⟹ step_t a (τ, (Read (Var v) e, p)) (τ (| l := l', R := R' |))"
| T_Write: 
  "⟦ eval_bool p τ ; 
  sh' = (sh τ) (eval_word e1 τ := eval_word e2 τ) ;
  W' = W τ ∪ { eval_word e1 τ } ; a ∈ {No_Abst, Eq_Abst} ⟧ 
  ⟹ step_t a (τ, (Write e1 e2, p)) (τ (| sh := sh', W := W' |))"
| T_Read_Adv:
  "⟦ eval_bool p τ ; l' = (l τ) (Inl v := asterisk) ;
  R' = R τ ∪ { eval_word e τ } ⟧ 
  ⟹ step_t Adv_Abst (τ, (Read (Var v) e, p)) (τ (| l := l', R := R' |))"
| T_Write_Adv:
  "⟦ eval_bool p τ ; W' = W τ ∪ { eval_word e1 τ } ⟧ 
  ⟹ step_t Adv_Abst (τ, (Write e1 e2, p)) (τ (| ⌦‹sh := sh',› W := W' |))"

text ‹Rephrasing ‹T_Assign› to make it more usable›
lemma T_Assign_helper: 
  "⟦ eval_bool p τ ; l' = (l τ) (Inl v := eval_word e τ) ; τ' = τ (| l := l' |) ⟧ 
  ⟹ step_t a (τ, (Assign (Var v) e, p)) τ'"
by (auto simp add: step_t.T_Assign)

text ‹Rephrasing ‹T_Read› to make it more usable›
lemma T_Read_helper: 
  "⟦ eval_bool p τ ; l' = (l τ) (Inl v := sh τ (eval_word e τ)) ;
  R' = R τ ∪ { eval_word e τ } ; a ∈ {No_Abst, Eq_Abst} ; 
  τ' = τ (| l := l', R := R' |) ⟧ 
  ⟹ step_t a (τ, (Read (Var v) e, p)) τ'"
by (auto simp add: step_t.T_Read)

text ‹Rephrasing ‹T_Write› to make it more usable›
lemma T_Write_helper:
  "⟦ eval_bool p τ ; 
  sh' = (sh τ) (eval_word e1 τ := eval_word e2 τ) ;
  W' = W τ ∪ { eval_word e1 τ } ; a ∈ {No_Abst, Eq_Abst} ;
  τ' = τ (| sh := sh', W := W' |) ⟧ 
  ⟹ step_t a (τ, (Write e1 e2, p)) τ'"
by (auto simp add: step_t.T_Write)

end

section ‹Execution rules for groups›

theory KPL_execution_group imports 
  KPL_execution_thread
begin

text ‹Intra-group race detection›
definition group_race 
  :: "lid set ⇒ (lid ⇀ thread_state) ⇒ bool"
where "group_race T γ ≡ 
  ∃j ∈ T. ∃k ∈ T. j ≠ k ∧ 
  W (the (γ j)) ∩ (R (the (γ k)) ∪ W (the (γ k))) ≠ {}"

text ‹The constraints for the @{term "merge"} map›
inductive pre_merge 
  :: "lid set ⇒ (lid ⇀ thread_state) ⇒ nat ⇒ word ⇒ bool"
where 
  "⟦ j ∈ T ; z ∈ W (the (γ j)) ; dom γ = T ⟧ ⟹
  pre_merge T γ z (sh (the (γ j)) z)"
| "⟦ ∀j ∈ T. z ∉ W (the (γ j)) ; dom γ = T ⟧ ⟹ 
  pre_merge T γ z (sh (the (γ 0)) z)"

inductive_cases pre_merge_inv [elim!]: "pre_merge P γ z z'"

text ‹The @{term "merge"} map maps each nat to the word that 
   satisfies the above constaints. The ‹merge_is_unique›
   lemma shows that there exists exactly one such word 
   per nat, provided there are no group races.›
definition merge :: "lid set ⇒ (lid ⇀ thread_state) ⇒ nat ⇒ word"
where "merge T γ ≡ λz. The (pre_merge T γ z)"

lemma no_races_imp_no_write_overlap: 
  "¬ (group_race T γ) ⟹ 
  ∀i ∈ T. ∀j ∈ T. 
  i ≠ j ⟶ W (the (γ i)) ∩ W (the (γ j)) = {}"
unfolding group_race_def 
by blast

lemma merge_is_unique:
  assumes "dom γ = T"
  assumes "¬ (group_race T γ)"
  shows "∃!z'. pre_merge T γ z z'"
apply (insert assms)
apply (drule no_races_imp_no_write_overlap)
apply (intro allI ex_ex1I)
apply (metis pre_merge.intros)
apply clarify
proof -
  fix z1 z2
  assume a: "∀i∈dom γ. ∀j∈dom γ. i ≠ j ⟶ W (the (γ i)) ∩ W (the (γ j)) = {}"
  assume "pre_merge (dom γ) γ z z1" 
  and "pre_merge (dom γ) γ z z2"
  thus "z1 = z2"
  apply (elim pre_merge_inv)
  apply (rename_tac j1 j2)
  apply (case_tac "j1 = j2")
  apply auto[1]
  apply simp
  apply (subgoal_tac "W (the (γ j1)) ∩ W (the (γ j2)) = {}")
  apply auto[1]
  apply (auto simp add: a)
  done
qed
 
text ‹The rules of Figure 5, plus an additional rule for
  equality abstraction (Fig 7a), plus an additional rule for
  adversarial abstraction (Fig 7b)›
inductive step_g
  :: "abs_level ⇒ gid ⇒ (gid ⇀ lid set) ⇒ (group_state × pred_stmt) ⇒ group_state option ⇒ bool"
where
  G_Race:
  "⟦ ∀j ∈ the (T i). step_t a (the (γ ⇩t⇩s j), (s, p)) (the (γ' ⇩t⇩s j)) ; 
    group_race (the (T i)) ((γ' :: group_state)⇩t⇩s) ⟧
  ⟹ step_g a i T (γ, (Basic s, p)) None"
| G_Basic:
  "⟦ ∀j ∈ the (T i). step_t a (the (γ ⇩t⇩s j), (s, p)) (the (γ' ⇩t⇩s j)) ; 
    ¬ (group_race (the (T i)) (γ' ⇩t⇩s)) ;
    R_group γ' = R_group γ ∪ (⋃j ∈ the (T i). ({j} × R (the (γ' ⇩t⇩s j)))) ;
    W_group γ' = W_group γ ∪ (⋃j ∈ the (T i). ({j} × W (the (γ' ⇩t⇩s j)))) ⟧
  ⟹ step_g a i T (γ, (Basic s, p)) (Some γ')"
| G_No_Op:
  "∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j)))
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ)"
| G_Divergence:
  "⟦ j ≠ k ; j ∈ the (T i) ; k ∈ the (T i) ;
   eval_bool p (the (γ ⇩t⇩s j)) ; ¬ (eval_bool p (the (γ ⇩t⇩s k))) ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) None"
| G_Sync:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := merge P (γ ⇩t⇩s), R := {}, W := {} |) ⟧ 
  ⟹ step_g No_Abst i T (γ, (Barrier, p)) (Some γ')"
| G_Sync_Eq:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := sh', R := {}, W := {} |) ⟧ 
  ⟹ step_g Eq_Abst i T (γ, (Barrier, p)) (Some γ')"
| G_Sync_Adv:
  "⟦ ∀j ∈ the (T i). eval_bool p (the (γ ⇩t⇩s j)) ;
    ∀j ∈ the (T i). ∃sh'. the (γ' ⇩t⇩s j) = (the (γ ⇩t⇩s j)) (| 
    sh := sh', R := {}, W := {} |) ⟧ 
  ⟹ step_g Adv_Abst i T (γ, (Barrier, p)) (Some γ')"

text ‹Rephrasing ‹G_No_Op› to make it more usable›
lemma G_No_Op_helper:
  "⟦ ∀j ∈ the (T i). ¬ (eval_bool p (the (γ ⇩t⇩s j))) ; γ = γ' ⟧
  ⟹ step_g a i T (γ, (Barrier, p)) (Some γ')"
by (simp add: step_g.G_No_Op)


end

section ‹Execution rules for kernels›

theory KPL_execution_kernel imports 
  KPL_execution_group
begin

text ‹Inter-group race detection›
definition kernel_race 
  :: "gid set ⇒ (gid ⇀ group_state) ⇒ bool"
where "kernel_race G κ ≡ 
  ∃i ∈ G. ∃j ∈ G. i ≠ j ∧ 
  (snd ` (W_group (the (κ i)))) ∩ 
  (snd ` (R_group (the (κ j))) ∪ snd ` (W_group (the (κ j)))) ≠ {}"

text ‹Replaces top-level @{term Break} with ‹v := true››
fun belim :: "stmt ⇒ V ⇒ stmt"
where 
  "belim (Basic b) v = Basic b"
| "belim (S1 ;; S2) v = (belim S1 v ;; belim S2 v)"
| "belim (Local n S) v = Local n (belim S v)"
| "belim (If e S1 S2) v = If e (belim S1 v) (belim S2 v)"
| "belim (While e S) v = While e S" (* only top-level *)
(* belim (WhileDyn e S) v = undefined *)
| "belim (Call f e) v = Call f e"
| "belim Barrier v = Barrier"
| "belim Break v = Basic (Assign (Var v) eTrue)"
| "belim Continue v = Continue"
| "belim Return v = Return"

text ‹Replaces top-level @{term Continue} with ‹v := true››
fun celim :: "stmt ⇒ V ⇒ stmt"
where 
  "celim (Basic b) v = Basic b"
| "celim (S1 ;; S2) v = (celim S1 v ;; celim S2 v)"
| "celim (Local n S) v = Local n (celim S v)"
| "celim (If e S1 S2) v = If e (celim S1 v) (celim S2 v)"
| "celim (While e S) v = While e S" (* only top-level *)
(* celim (WhileDyn e S) v = undefined *)
| "celim (Call f e) v = Call f e"
| "celim Barrier v = Barrier"
| "celim Break v = Break"
| "celim Continue v = Basic (Assign (Var v) eTrue)"
| "celim Return v = Return"

text ‹@{term "subst_basic_stmt n v loc"} replaces @{term n} with @{term v} inside @{term loc}›
fun subst_loc :: "name ⇒ V ⇒ loc ⇒ loc"
where
  "subst_loc n v (Var w) = Var w"
| "subst_loc n v (Name m) = (if n = m then Var v else Name m)"

text ‹@{term "subst_local_expr n v e"} replaces @{term n} with @{term v} inside @{term e}›
fun subst_local_expr 
  :: "name ⇒ V ⇒ local_expr ⇒ local_expr"
where
  "subst_local_expr n v (Loc loc) = Loc (subst_loc n v loc)"
| "subst_local_expr n v Gid = Gid"
| "subst_local_expr n v Lid = Lid"
| "subst_local_expr n v eTrue = eTrue"
| "subst_local_expr n v (e1 ∧* e2) = 
  (subst_local_expr n v e1 ∧* subst_local_expr n v e2)"
| "subst_local_expr n v (¬* e) = ¬* (subst_local_expr n v e)"

text ‹@{term "subst_basic_stmt n v b"} replaces @{term n} with @{term v} inside @{term b}›
fun subst_basic_stmt :: "name ⇒ V ⇒ basic_stmt ⇒ basic_stmt"
where 
  "subst_basic_stmt n v (Assign loc e) = 
  Assign (subst_loc n v loc) (subst_local_expr n v e)"
| "subst_basic_stmt n v (Read loc e) =
  Read (subst_loc n v loc) (subst_local_expr n v e)"
| "subst_basic_stmt n v (Write e1 e2) =
  Write (subst_local_expr n v e1) (subst_local_expr n v e2)"

text ‹@{term "subst_stmt n v s t"} holds if @{term t} is the result 
  of replacing @{term n} with @{term v} inside @{term s}›
inductive subst_stmt :: "name ⇒ V ⇒ stmt ⇒ stmt ⇒ bool"
where 
  "subst_stmt n v (Basic b) (Basic (subst_basic_stmt n v b))"
| "⟦ subst_stmt n v S1 S1' ; subst_stmt n v S2 S2' ⟧ ⟹
  subst_stmt n v (S1 ;; S2) (S1' ;; S2')"
| "⟦ m ≠ n ; subst_stmt n v S S' ⟧ ⟹ 
  subst_stmt n v (Local m S) (Local m S')"
| "⟦ subst_stmt n v S1 S1' ; subst_stmt n v S2 S2' ⟧ ⟹ 
  subst_stmt n v (If e S1 S2) (If e S1' S2')"
| "subst_stmt n v S S' ⟹ subst_stmt n v (While e S) (While e S')" 
(* subst_stmt n v (WhileDyn e S) undefined *)
| "subst_stmt n v (Call f e) (Call f e)"
| "subst_stmt n v Barrier Barrier"
| "subst_stmt n v Break Break"
| "subst_stmt n v Continue Continue"
| "subst_stmt n v Return Return"

text ‹@{term "param_subst f u"} replaces @{term f}'s parameter with @{term u}›
definition param_subst :: "proc list ⇒ proc_name ⇒ V ⇒ stmt"
where "param_subst fs f u ≡ 
  let proc = THE proc. proc ∈ set fs ∧ proc_name proc = f in
  THE S'. subst_stmt (param proc) u (body proc) S'"

text ‹Replace @{term "Return"} with ‹v := true››
fun relim :: "stmt ⇒ V ⇒ stmt"
where 
  "relim (Basic b) v = Basic b"
(* Additional rule for adversarial abstraction (Fig 7b) *)
| "relim (S1 ;; S2) v = (relim S1 v ;; relim S2 v)"
| "relim (Local n S) v = Local n (relim S v)"
| "relim (If e S1 S2) v = If e (relim S1 v) (relim S2 v)"
| "relim (While e S) v = While e (relim S v)"
(* relim (WhileDyn e S) v = undefined *)
| "relim (Call f e) v = Call f e"
| "relim Barrier v = Barrier"
| "relim Break v = Break"
| "relim Continue v = Continue"
| "relim Return v = Basic (Assign (Var v) eTrue)"

text ‹Fresh variables›
definition fresh :: "V ⇒ V list ⇒ bool"
where "fresh v vs ≡ v ∉ set vs"

text ‹The rules of Figure 6›
inductive step_k
  :: "abs_level ⇒ proc list ⇒ threadset ⇒ kernel_state ⇒ kernel_state option ⇒ bool"
where
  K_Inter_Group_Race:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Basic b, p)) (Some (the (κ' i))) ;
     kernel_race P κ' ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic b, p) # ss, vs) None"
| K_Intra_Group_Race:
  "⟦ i ∈ G; step_g a i T (the (κ i), (Basic s, p)) None ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic s, p) # ss, vs) None"
| K_Basic:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Basic b, p)) (Some (the (κ' i))) ;
     ¬ (kernel_race G κ') ⟧ ⟹
  step_k a fs (G,T) (κ, (Basic b, p) # ss, vs) (Some (κ',ss, vs))"
| K_Divergence:
  "⟦ i ∈ G; step_g a i T (the (κ i), (Barrier, p)) None ⟧ ⟹
  step_k a fs (G,T) (κ, (Barrier, p) # ss, vs) None"
| K_Sync:
  "⟦ ∀i ∈ G. step_g a i T (the (κ i), (Barrier, p)) (Some (the (κ' i))) ;
     ¬ (kernel_race G κ') ⟧ ⟹
  step_k a fs (G,T) (κ, (Barrier, p) # ss, vs) (Some (κ',ss, vs))"
| K_Seq:
  "step_k a fs (G,T) (κ, (S1 ;; S2, p) # ss, vs) 
  (Some (κ, (S1, p) # (S2, p) # ss, vs))"
| K_Var:
  "fresh v vs ⟹ 
  step_k a fs (G,T) (κ, (Local n S, p) # ss, vs)  
  (Some (κ, (THE S'. subst_stmt n v S S', p) # ss, v # vs))"
| K_If: 
  "fresh v vs ⟹ 
  step_k a fs (G,T) (κ, (If e S1 S2, p) # ss, vs) (Some (κ, 
  (Basic (Assign (Var v) e), p) 
  # (S1, p ∧* Loc (Var v)) 
  # (S2, p ∧* ¬* (Loc (Var v))) # ss, v # vs))"
| K_Open:
  "fresh v vs ⟹
  step_k a fs (G,T) (κ, (While e S, p) # ss, vs) (Some (κ, 
  (WhileDyn e (belim S v), p ∧* ¬* (Loc (Var v))) # ss, v # vs))"
| K_Iter:
  "⟦ i ∈ G ; j ∈ the (T i) ; 
  eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j)) ; 
  fresh u vs ; fresh v vs; u ≠ v ⟧ ⟹
  step_k a fs (G,T) (κ, (WhileDyn e S, p) # ss, vs) (Some (κ, 
  (Basic (Assign (Var u) e), p) 
  # (celim S v, p ∧* Loc (Var u) ∧* ¬* (Loc (Var v))) 
  # (WhileDyn e S, p) # ss, u # v # vs))"
| K_Done:
  "∀i ∈ G. ∀j ∈ the (T i). 
  ¬ (eval_bool (p ∧* e) (the ((the (κ i))⇩t⇩s j))) ⟹
  step_k a fs (G,T) (κ, (WhileDyn e S, p) # ss, vs) (Some (κ, ss, vs))"
| K_Call: 
  "⟦ fresh u vs ; fresh v vs ; u ≠ v ; s = param_subst fs f u ⟧ ⟹
  step_k a fs (G,T) (κ, (Call f e, p) # ss, vs ) 
  (Some (κ, (Basic (Assign (Var u) e) ;; relim s v, 
  p ∧* ¬* (Loc (Var v))) # ss, u # v # vs))"



end

(* 
Title:       Kernel_programming_language.thy
Author:      John Wickerson
Date:        2 April 2014
Description: 
  This theory file accompanies the article "The Design and 
  Implementation of a Verification Technique for GPU Kernels" 
  by Adam Betts, Nathan Chong, Alastair F. Donaldson, Jeroen
  Ketema, Shaz Qadeer, Paul Thomson and John Wickerson. It
  formalises all of the definitions provided in Sections 3
  and 4. 
*)

theory Kernel_programming_language imports
(* 1. SOME GENERAL PURPOSE STUFF *)
  Misc
(* 2. SYNTAX OF KPL *)
  KPL_syntax
(* 3. WELL-FORMEDNESS OF KPL KERNELS *)
  KPL_wellformedness
(* 4. THREAD, GROUP, AND KERNEL STATES *)
  KPL_state
(* 5. EXECUTION RULES FOR THREADS *)
  KPL_execution_thread
(* 6. EXECUTION RULES FOR GROUPS *)
  KPL_execution_group
(* 7. EXECUTION RULES FOR KERNELS *)
  KPL_execution_kernel
begin 

end