Theory Language

theory Language
imports Preliminaries
(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
header {* Language for Instantiating the SIFUM-Security Property *}

theory Language
imports Main 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 "\<leftarrow>" 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"
  | Stop

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

locale sifum_lang =
  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"
  fixes dma :: "'Var => Sec"
  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"

context sifum_lang
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")

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 "\<leadsto>s" 60)
  where
  "c \<leadsto>s c' ≡ (c, c') ∈ evalw_simple" |
  assign: "((x \<leftarrow> 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"

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. *)

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 "\<leadsto>w" 60)
  where
  "c \<leadsto>w c' ≡ (c, c') ∈ evalw" |
  unannotated: "[| (c, mem) \<leadsto>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 \<leadsto>w ⟨c1', mds', mem'⟩w |] ==> (⟨(c1 ;; c2), mds, mem⟩w, ⟨(c1' ;; c2), mds', mem'⟩w) ∈ evalw" |
  decl: "[| ⟨c, update_modes mu mds, mem⟩w \<leadsto>w ⟨c', mds', mem'⟩w |] ==>
         (⟨cxt_to_stmt E (ModeDecl c mu), mds, mem⟩w, ⟨cxt_to_stmt E c', mds', mem'⟩w) ∈ 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 \<leftarrow> e, mem), (c', mem')) ∈ evalw_simple"
inductive_cases skip_elim' [elim]: "(Skip, mem) \<leadsto>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 \<leftarrow> e |] ==> c = x \<leftarrow> 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(21) cxt_inv)

lemma cxt_inv_stop:
  "cxt_to_stmt E c = Stop ==> c = Stop ∧ E = []"
  by (metis Stmt.simps(40) 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(37) cxt_inv)

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

lemma skip_elim [elim]:
  "⟨Skip, mds, mem⟩w \<leadsto>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(20))
  by (metis Stmt.simps(18) cxt_inv_skip)

lemma assign_elim [elim]:
  "⟨x \<leftarrow> e, mds, mem⟩w \<leadsto>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 \<leftarrow> e ∧ E = []")
     apply auto
      apply (metis cxt_inv_assign)
     apply (metis cxt_inv_assign)
    apply (metis Stmt.simps(8) cxt_inv_assign)
   apply (metis Stmt.simps(8) cxt_inv_assign)
  by (metis Stmt.simps(8) cxt_inv_assign)

inductive_cases if_elim' [elim!]: "(If b p q, mem) \<leadsto>s (c', mem')"

lemma if_elim [elim]:
  "!! P.
    [| ⟨If b p q, mds, mem⟩w \<leadsto>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(36))
  by (metis Stmt.simps(30) cxt_inv_if)

inductive_cases while_elim' [elim!]: "(While e c, mem) \<leadsto>s (c', mem')"

lemma while_elim [elim]:
  "[| ⟨While e c, mds, mem⟩w \<leadsto>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(38))
  by (metis (lifting) Stmt.simps(33) cxt_inv_while)

inductive_cases upd_elim' [elim]: "(c@[upd], mem) \<leadsto>s (c', mem')"

lemma upd_elim [elim]:
  "⟨c@[upd], mds, mem⟩w \<leadsto>w ⟨c', mds', mem'⟩w ==> ⟨c, update_modes upd mds, mem⟩w \<leadsto>w ⟨c', mds', mem'⟩w"
  apply (erule eval_elim)
    apply (metis (lifting) Stmt.simps(28) cxt_inv upd_elim')
   apply (metis Stmt.simps(29))
  by (metis (lifting) Stmt.simps(2) Stmt.simps(29) cxt_inv cxt_to_stmt.simps(1))

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) \<leadsto>s (c', mem')"

lemma stop_no_eval: "¬ (⟨Stop, mds, mem⟩w \<leadsto>w ⟨c', mds', mem'⟩w)"
  apply auto
  apply (erule eval_elim)
    apply (metis cxt_inv_stop stop_no_eval')
   apply (metis Stmt.simps(41))
  by (metis Stmt.simps(35) cxt_inv_stop)

lemma seq_stop_elim [elim]:
  "⟨Stop ;; c, mds, mem⟩w \<leadsto>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)
  by (metis Stmt.distinct(23) Stmt.distinct(29) cxt_seq_elim)

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 \<leadsto>w ⟨c', mds', mem'⟩w ; c1 ≠ Stop |] ==>
  (∃ c1'. ⟨c1, mds, mem⟩w \<leadsto>w ⟨c1', mds', mem'⟩w ∧ c' = c1' ;; c2)"
  apply (erule eval_elim)
    apply clarify
    apply (drule cxt_seq_elim)
    apply (erule disjE)
     apply (metis cxt_to_stmt.simps(1) evalw.unannotated seq_elim')
    apply auto
   apply (metis cxt_to_stmt.simps(1) evalw.unannotated)
  apply (subgoal_tac "c1 = c@[mu]")
   apply simp
   apply auto
   apply (drule cxt_seq_elim)
   apply (metis Stmt.distinct(23) cxt_stmt_seq cxt_to_stmt.simps(1) evalw.decl)
  by (metis Stmt.distinct(23) cxt_seq_elim)

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

end

end