Theory KPL_execution_thread

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