Theory Language

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
section ‹Language for Instantiating the SIFUM-Security Property›

theory Language
imports Preliminaries
begin

subsection ‹Syntax›

datatype 'var ModeUpd = Acq "'var" Mode (infix "+=m" 75)
  | Rel "'var" Mode (infix "-=m" 75)

datatype ('var, 'aexp, 'bexp) Stmt = Assign "'var" "'aexp" (infix "←" 130)
  | Skip
  | ModeDecl "('var, 'aexp, 'bexp) Stmt" "'var ModeUpd" ("_@[_]" [0, 0] 150)
  | Seq "('var, 'aexp, 'bexp) Stmt" "('var, 'aexp, 'bexp) Stmt" (infixr ";;" 150)
  | If "'bexp" "('var, 'aexp, 'bexp) Stmt" "('var, 'aexp, 'bexp) Stmt"
  | While "'bexp" "('var, 'aexp, 'bexp) Stmt"
  | Await "'bexp" "('var, 'aexp, 'bexp) Stmt"
  | Stop

type_synonym ('var, 'aexp, 'bexp) EvalCxt = "('var, 'aexp, 'bexp) Stmt list"

locale sifum_lang_no_dma =
  fixes evalA :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  fixes evalB :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
  fixes aexp_vars :: "'AExp ⇒ 'Var set"
  fixes bexp_vars :: "'BExp ⇒ 'Var set"
  assumes Var_finite : "finite {(x :: 'Var). True}"
  assumes eval_vars_detA : "⟦ ∀ x ∈ aexp_vars e. mem1 x = mem2 x ⟧ ⟹ evalA mem1 e = evalA mem2 e"
  assumes eval_vars_detB : "⟦ ∀ x ∈ bexp_vars b. mem1 x = mem2 x ⟧ ⟹ evalB mem1 b = evalB mem2 b"

locale sifum_lang = sifum_lang_no_dma evalA evalB aexp_vars bexp_vars
  for evalA :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  and evalB :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
  and aexp_vars :: "'AExp ⇒ 'Var set"
  and bexp_vars :: "'BExp ⇒ 'Var set"+
  fixes dma :: "'Var ⇒ Sec"

context sifum_lang_no_dma
begin

(* To make the examples look a bit nicer in the PDF. *)

notation (latex output)
  Seq ("_; _" 60)

notation (Rule output)
  Seq ("_ ; _" 60)

notation (Rule output)
  If ("if _ then _ else _ fi" 50)

notation (Rule output)
  While ("while _ do _ done")

notation (Rule output)
  Await ("await _ do _ done")

abbreviation confw_abv :: "('Var, 'AExp, 'BExp) Stmt ⇒
  'Var Mds ⇒ ('Var, 'Val) Mem ⇒ (_,_,_) LocalConf"
  ("⟨_, _, _⟩w" [0, 120, 120] 100)
  where
  "⟨ c, mds, mem ⟩w ≡ ((c, mds), mem)"

subsection ‹Semantics›

primrec update_modes :: "'Var ModeUpd ⇒ 'Var Mds ⇒ 'Var Mds"
  where
  "update_modes (Acq x m) mds = mds (m := insert x (mds m))" |
  "update_modes (Rel x m) mds = mds (m := {y. y ∈ mds m ∧ y ≠ x})"

fun updated_var :: "'Var ModeUpd ⇒ 'Var"
  where
  "updated_var (Acq x _) = x" |
  "updated_var (Rel x _) = x"

fun updated_mode :: "'Var ModeUpd ⇒ Mode"
  where
  "updated_mode (Acq _ m) = m" |
  "updated_mode (Rel _ m) = m"

inductive_set evalw_simple :: "(('Var, 'AExp, 'BExp) Stmt × ('Var, 'Val) Mem) rel"
and evalw_simple_abv :: "(('Var, 'AExp, 'BExp) Stmt × ('Var, 'Val) Mem) ⇒
  ('Var, 'AExp, 'BExp) Stmt × ('Var, 'Val) Mem ⇒ bool"
  (infixr "↝s" 60)
  where
  "c ↝s c' ≡ (c, c') ∈ evalw_simple" |
  assign: "((x ← e, mem), (Stop, mem (x := evalA mem e))) ∈ evalw_simple" |
  skip: "((Skip, mem), (Stop, mem)) ∈ evalw_simple" |
  seq_stop: "((Seq Stop c, mem), (c, mem)) ∈ evalw_simple" |
  if_true: "⟦ evalB mem b ⟧ ⟹ ((If b t e, mem), (t, mem)) ∈ evalw_simple" |
  if_false: "⟦ ¬ evalB mem b ⟧ ⟹ ((If b t e, mem), (e, mem)) ∈ evalw_simple" |
  while: "((While b c, mem), (If b (c ;; While b c) Stop, mem)) ∈ evalw_simple"

lemma cond:
  "((If b t e, mem), (if evalB mem b then t else e, mem)) ∈ evalw_simple"
  apply(case_tac "evalB mem b")
   apply(auto intro: evalw_simple.intros)
  done

primrec cxt_to_stmt :: "('Var, 'AExp, 'BExp) EvalCxt ⇒ ('Var, 'AExp, 'BExp) Stmt
  ⇒ ('Var, 'AExp, 'BExp) Stmt"
  where
  "cxt_to_stmt [] c = c" |
  "cxt_to_stmt (c # cs) c' = Seq c' (cxt_to_stmt cs c)"

(* Design decision: Add "normal" rule for sequential statements here as well.
  Otherwise, one would have to take care of adding some sort of normalization
  later, so that one doesn't get stuck on expressions of the form (c ;; c') ;; c''.
*)
(* Normalization turned out to be more difficult, as it made the proofs of several
  helpful lemmas below quite difficult. *)

lemma rtrancl_mono_proof[mono]:
  "(⋀a b. x a b ⟶ y a b) ⟹ rtranclp x a b ⟶ rtranclp y a b"
  apply (rule impI, rotate_tac, induct rule: rtranclp.induct)
   apply simp_all
  apply (metis rtranclp.intros)
  done

lemma trancl_mono_proof[mono]:
  "(⋀a b. x a b ⟶ y a b) ⟹ tranclp x a b ⟶ tranclp y a b"
  apply (rule impI, rotate_tac, induct rule: tranclp.induct)
   apply simp_all
   apply blast
  by fastforce

inductive no_await :: "('Var, 'AExp, 'BExp) Stmt ⇒ bool" where
  "no_await (x ← e)" |
  "no_await c1 ⟹ no_await c2 ⟹ no_await (c1 ;; c2)" |
  "no_await c1 ⟹ no_await c2 ⟹ no_await (If b c1 c2)" |
  "no_await c ⟹ no_await (While b c)" |
  "no_await Skip" |
  "no_await Stop" |
  "no_await c ⟹ no_await (c@[m])"

inductive is_final :: "('Var, 'AExp, 'BExp) Stmt ⇒ bool" where
  "is_final Stop" |
  "is_final c ⟹ is_final (c@[m])"

inductive_set evalw :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf rel"
and evalw_abv :: "(('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒ bool"
  (infixr "↝w" 60)
where
  "c ↝w c' ≡ (c, c') ∈ evalw" |
  unannotated: "⟦ (c, mem) ↝s (c', mem') ⟧
    ⟹ (⟨cxt_to_stmt E c, mds, mem⟩w, ⟨cxt_to_stmt E c', mds, mem'⟩w) ∈ evalw" |
  seq: "⟦ ⟨c1, mds, mem⟩w ↝w ⟨c1', mds', mem'⟩w ⟧ ⟹ (⟨(c1 ;; c2), mds, mem⟩w, ⟨(c1' ;; c2), mds', mem'⟩w) ∈ evalw" |
  decl: "⟦ ⟨c, update_modes mu mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟧ ⟹
         (⟨cxt_to_stmt E (ModeDecl c mu), mds, mem⟩w, ⟨cxt_to_stmt E c', mds', mem'⟩w) ∈ evalw" |
(* This is added instead of defining evalp -- see next comment*)
  await: "⟦evalB mem b; no_await c1;
         (⟨c1, mds, mem⟩w, ⟨c2, mds', mem'⟩w) ∈ evalw+;
         is_final c2⟧ ⟹
         (⟨Await b c1, mds, mem⟩w, ⟨c2, mds', mem'⟩w) ∈ evalw"

abbreviation evalw_plus :: "
  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒
                  (('Var, 'AExp, 'BExp) Stmt, 'Var, 'Val) LocalConf ⇒ bool" ("_ ↝w+ _") where
"ctx ↝w+ ctx' ≡ (ctx, ctx') ∈ evalw+"
  
subsection ‹Semantic Properties›

text ‹The following lemmas simplify working with evaluation contexts
  in the soundness proofs for the type system(s).›

inductive_cases eval_elim: "(((c, mds), mem), ((c', mds'), mem')) ∈ evalw"
inductive_cases stop_no_eval' [elim]: "((Stop, mem), (c', mem')) ∈ evalw_simple"
inductive_cases assign_elim' [elim]: "((x ← e, mem), (c', mem')) ∈ evalw_simple"
inductive_cases skip_elim' [elim]: "(Skip, mem) ↝s (c', mem')"

lemma cxt_inv:
  "⟦ cxt_to_stmt E c = c' ; ⋀ p q. c' ≠ Seq p q ⟧ ⟹ E = [] ∧ c' = c"
  by (metis cxt_to_stmt.simps(1) cxt_to_stmt.simps(2) neq_Nil_conv)

lemma cxt_inv_assign:
  "⟦ cxt_to_stmt E c = x ← e ⟧ ⟹ c = x ← e ∧ E = []"
  by (metis Stmt.simps(11) cxt_inv)

lemma cxt_inv_skip:
  "⟦ cxt_to_stmt E c = Skip ⟧ ⟹ c = Skip ∧ E = []"
  by (metis Stmt.simps(23) cxt_inv)

lemma cxt_inv_stop:
  "cxt_to_stmt E c = Stop ⟹ c = Stop ∧ E = []"
  by (metis Stmt.simps(49) cxt_inv)

lemma cxt_inv_if:
  "cxt_to_stmt E c = If e p q ⟹ c = If e p q ∧ E = []"
  by (metis Stmt.simps(43) cxt_inv)
  
lemma ctx_inv_anno:
  "cxt_to_stmt E c = c'@[mu] ⟹ c = c'@[mu] ∧ E = []"
  using cxt_inv by blast 
  
lemma cxt_inv_await:
  "cxt_to_stmt E c = Await e p ⟹ c = Await e p  ∧ E = []"
  by (metis Stmt.simps(47) cxt_inv)

lemma cxt_inv_while:
  "cxt_to_stmt E c = While e p ⟹ c = While e p ∧ E = []"
  by (metis Stmt.simps(45) cxt_inv)

lemma skip_elim [elim]:
  "⟨Skip, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹ c' = Stop ∧ mds = mds' ∧ mem = mem'"
  apply (erule eval_elim)
     apply (metis (lifting) cxt_inv_skip cxt_to_stmt.simps(1) skip_elim')
    apply (metis Stmt.simps(24))
   apply (metis Stmt.simps(21) cxt_inv_skip)
  by simp

lemma assign_elim [elim]:
  "⟨x ← e, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹ c' = Stop ∧ mds = mds' ∧ mem' = mem (x := evalA mem e)"
  apply (erule eval_elim)
     apply (rename_tac c c'a E)
     apply (subgoal_tac "c = x ← e ∧ E = []")
      apply force 
     apply auto
      apply (metis cxt_inv_assign)
     apply (metis cxt_inv_assign)
    apply (metis Stmt.simps(9) cxt_inv_assign)
   apply (metis Stmt.simps(9) cxt_inv_assign)
  by (metis Stmt.simps(9) cxt_inv_assign)

inductive_cases if_elim' [elim!]: "(If b p q, mem) ↝s (c', mem')"

lemma if_elim [elim]:
  "⋀ P.
    ⟦ ⟨If b p q, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ;
     ⟦ c' = p; mem' = mem ; mds' = mds ; evalB mem b ⟧ ⟹ P ;
     ⟦ c' = q; mem' = mem ; mds' = mds ; ¬ evalB mem b ⟧ ⟹ P ⟧ ⟹ P"
  apply (erule eval_elim)
     apply (metis (no_types) cxt_inv_if cxt_to_stmt.simps(1) if_elim')
    apply (metis Stmt.simps(43))
   apply (metis Stmt.simps(35) cxt_inv_if)
  by simp

inductive_cases await_elim' [elim!]: "⟨Await b p, mds, mem⟩w ↝w ⟨c',mds', mem'⟩w"

inductive_cases while_elim' [elim!]: "(While e c, mem) ↝s (c', mem')"

lemma while_elim [elim]:
  "⟦ ⟨While e c, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟧ ⟹ c' = If e (c ;; While e c) Stop ∧ mds' = mds ∧ mem' = mem"
  apply (erule eval_elim)
     apply (metis (no_types) cxt_inv_while cxt_to_stmt.simps(1) while_elim')
    apply (metis Stmt.simps(45))
   apply (metis (lifting) Stmt.simps(37) cxt_inv_while)
  by simp

inductive_cases upd_elim' [elim]: "(c@[upd], mem) ↝s (c', mem')"

lemma upd_elim [elim]:
  "⟨c@[upd], mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹ ⟨c, update_modes upd mds, mem⟩w ↝w ⟨c', mds', mem'⟩w"
  apply (erule eval_elim)
     apply (metis (lifting) Stmt.simps(33) cxt_inv upd_elim')
    apply (metis Stmt.simps(34))
   apply (metis (lifting) Stmt.simps(2) Stmt.simps(33) cxt_inv cxt_to_stmt.simps(1))
  by simp

lemma cxt_seq_elim [elim]:
  "c1 ;; c2 = cxt_to_stmt E c ⟹ (E = [] ∧ c = c1 ;; c2) ∨ (∃ c' cs. E = c' # cs ∧ c = c1 ∧ c2 = cxt_to_stmt cs c')"
  apply (cases E)
   apply (metis cxt_to_stmt.simps(1))
  by (metis Stmt.simps(3) cxt_to_stmt.simps(2))

inductive_cases seq_elim' [elim]: "(c1 ;; c2, mem) ↝s (c', mem')"

lemma stop_no_eval: "¬ (⟨Stop, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w)"
  apply auto
  apply (erule eval_elim)
     apply (metis cxt_inv_stop stop_no_eval')
    apply (metis Stmt.simps(49))
   apply (metis Stmt.simps(41) cxt_inv_stop)
  by simp

lemma seq_stop_elim [elim]:
  "⟨Stop ;; c, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹ c' = c ∧ mds' = mds ∧ mem' = mem"
  apply (erule eval_elim)
     apply clarify
     apply (metis (no_types) cxt_seq_elim cxt_to_stmt.simps(1) seq_elim' stop_no_eval')
    apply (metis Stmt.inject(3) stop_no_eval)
   apply (metis Stmt.distinct(28) Stmt.distinct(36) cxt_seq_elim)
  by simp

lemma cxt_stmt_seq:
  "c ;; cxt_to_stmt E c' = cxt_to_stmt (c' # E) c"
  by (metis cxt_to_stmt.simps(2))


lemma seq_elim [elim]:
  "⟦ ⟨c1 ;; c2, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ; c1 ≠ Stop ⟧ ⟹
  (∃ c1'. ⟨c1, mds, mem⟩w ↝w ⟨c1', mds', mem'⟩w ∧ c' = c1' ;; c2)"
  apply (erule eval_elim)
    apply clarify
    apply (drule cxt_seq_elim)
    apply (erule disjE)
     apply blast 
    apply auto
   apply (metis cxt_to_stmt.simps(1) evalw.unannotated)
  apply (subgoal_tac "c1 = c@[mu]")
   apply simp
   apply (drule cxt_seq_elim)
   apply (metis Stmt.distinct(27) cxt_stmt_seq cxt_to_stmt.simps(1) evalw.decl)
  using cxt_seq_elim by blast

lemma stop_cxt: "Stop = cxt_to_stmt E c ⟹ c = Stop"
  by (metis Stmt.simps(50) cxt_to_stmt.simps(1) cxt_to_stmt.simps(2) neq_Nil_conv)

(* Additional helper lemmas added by TobyM and RobS *)

lemmas decl_evalw = decl[OF unannotated, OF skip, where E="[]", simplified, where E1="[]", simplified]
lemmas seq_stop_evalw = unannotated[OF seq_stop, where E="[]", simplified]
lemmas assign_evalw = unannotated[OF assign, where E="[]", simplified]
lemmas if_evalw = unannotated[OF cond, where E="[]", simplified]
lemmas if_false_evalw = unannotated[OF if_false, where E="[]", simplified]
lemmas skip_evalw = unannotated[OF skip, where E="[]", simplified]
lemmas while_evalw = unannotated[OF while, where E="[]", simplified]

lemma decl_evalw':
  assumes mem_unchanged: "mem' = mem"
  assumes upd: "mds' = update_modes upd mds"
  shows "(⟨Skip@[upd], mds, mem⟩w, ⟨Stop, mds', mem'⟩w) ∈ evalw"
  using assms decl_evalw
  by auto

lemma assign_evalw':
  "⟦mds = mds'; mem' = mem(x := evalA mem e)⟧ ⟹
  ⟨x ← e, mds, mem⟩w ↝w ⟨Stop, mds', mem'⟩w"
  using assign_evalw
  by simp

(* Following the naming convention, but we actually apply these as dest, not elim rules... *)

lemma seq_decl_elim:
  "⟨(Skip@[upd]) ;; c, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹
   c' = Stop ;; c ∧ mem' = mem ∧ mds' = update_modes upd mds"
  apply(drule seq_elim, simp)
  apply(erule exE, clarsimp)
  apply(drule upd_elim)
  apply(drule skip_elim, clarsimp)
  done

lemma seq_assign_elim:
  "⟨(x ← e) ;; c, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟹
   c' = Stop ;; c ∧ mds' = mds ∧ mem' = mem(x := evalA mem e)"
  apply(drule seq_elim, simp)
  apply(erule exE, clarsimp)
  apply(drule assign_elim, clarsimp)
  done

lemma no_await_trans: 
  "⟦ no_await c; ⟨c, mds, mem⟩w ↝w ⟨c', mds', mem'⟩w ⟧ ⟹ no_await c'"
  apply (induct arbitrary: c' mds rule: "no_await.induct")
        using assign_elim "no_await.simps" apply blast
       apply (rename_tac c1 c2 c3 mds)
       apply (case_tac "c1 = Stop")
        apply (simp, frule seq_stop_elim, clarsimp)
        using seq_elim no_await.intros apply metis
       using if_elim no_await.intros apply blast
      apply (frule while_elim, clarsimp)
     apply (rename_tac c b)
     apply (subgoal_tac "no_await (While b c)")
      apply (subgoal_tac "no_await (c ;; While b c)")
       using no_await.intros apply blast
      using no_await.intros apply blast
     using no_await.intros apply blast
    using no_await.intros skip_elim apply fast
   using no_await.intros stop_no_eval apply fast
  using no_await.intros upd_elim by fast

lemma no_await_no_await[elim]: "⟦ no_await c ⟧ ⟹ c ≠ Await b c'"
  using no_await.cases Stmt.distinct by fast

lemma no_await_trancl_impl: 
  "⟦ctx ↝w+ ctx'⟧ ⟹ no_await (fst (fst ctx)) ⟶ no_await (fst (fst ctx'))"
  apply (erule trancl.induct, clarsimp)
   using no_await_trans apply blast
  apply clarsimp
  using no_await_trans by blast
  
lemma no_await_trancl: 
  "⟦ctx ↝w+ ctx'; no_await (fst (fst ctx))⟧ ⟹ no_await (fst (fst ctx'))" 
  using no_await_trancl_impl by blast

lemma await_elim: 
  "⟦⟨Await b c1, mds, mem⟩w ↝w ⟨c2, mds', mem'⟩w⟧ ⟹ 
    evalB mem b ∧ no_await c1 ∧ is_final c2  ∧
    ⟨c1, mds, mem⟩w ↝w+ ⟨c2, mds', mem'⟩w"
  apply (erule "evalw.cases"; clarsimp)
   apply (subgoal_tac "cxt_to_stmt E c = Await b c1")
    apply (drule cxt_inv_await)
    using "evalw_simple.cases" apply force
   apply simp
  by (metis Stmt.distinct(33) cxt_inv_await)
  
end

end