Theory MWLs

(*
Title: WHATandWHERE-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory MWLs
imports Strong_Security.Types
begin

― ‹type parameters not instantiated:›
― ‹'exp: expressions (arithmetic, boolean...)›
― ‹'val: numbers, boolean constants....›
― ‹'id: identifier names›

― ‹SYNTAX›

datatype ('exp, 'id) MWLsCom
  = Skip "nat" ("skip⇘_⇙" [50] 70)
  | Assign "'id" "nat" "'exp"
       ("_:=⇘_⇙ _" [70,50,70] 70)

  | Seq "('exp, 'id) MWLsCom"
         "('exp, 'id) MWLsCom"
       ("_;_" [61,60] 60)

  | If_Else "nat" "'exp" "('exp, 'id) MWLsCom"
         "('exp, 'id) MWLsCom"
       ("if⇘_⇙ _ then _ else _ fi" [50,80,79,79] 70)

  | While_Do "nat" "'exp" "('exp, 'id) MWLsCom"
       ("while⇘_⇙ _ do _ od" [50,80,79] 70)

  | Spawn "nat" "(('exp, 'id) MWLsCom) list"
       ("spawn⇘_⇙ _" [50,70] 70)

― ‹function for obtaining the program point of some MWLsloc command›
primrec pp ::"('exp, 'id) MWLsCom ⇒ nat"
where
"pp (skip⇘ι⇙) = ι" |
"pp (x :=⇘ι⇙ e) = ι" |
"pp (c1;c2) = pp c1" |
"pp (if⇘ι⇙ b then c1 else c2 fi) = ι" |
"pp (while⇘ι⇙ b do c od) = ι" |
"pp (spawn⇘ι⇙ V) = ι"

― ‹mutually recursive functions to collect program points of commands and thread pools›
primrec PPc :: "('exp,'id) MWLsCom ⇒ nat list"
and PPV :: "('exp,'id) MWLsCom list ⇒ nat list"
where
"PPc (skip⇘ι⇙) = [ι]" |
"PPc (x :=⇘ι⇙ e) = [ι]" |
"PPc (c1;c2) = (PPc c1) @ (PPc c2)" |
"PPc (if⇘ι⇙ b then c1 else c2 fi) =  [ι] @ (PPc c1) @ (PPc c2)" |
"PPc (while⇘ι⇙ b do c od) = [ι] @ (PPc c)" |
"PPc (spawn⇘ι⇙ V) = [ι] @ (PPV V)" |

"PPV [] = []" |
"PPV (c#V) = (PPc c) @ (PPV V)"

― ‹predicate indicating that a command only contains unique program points›
definition unique_PPc :: "('exp, 'id) MWLsCom ⇒ bool"
where
"unique_PPc c = distinct (PPc c)"

― ‹predicate indicating that a thread pool only contains unique program points›
definition unique_PPV :: "('exp, 'id) MWLsCom list ⇒ bool"
where
"unique_PPV V = distinct (PPV V)"

lemma PPc_nonempt: "PPc c ≠ []"
  by (induct c) auto

lemma unique_c_uneq: "set (PPc c) ∩ set (PPc c') = {} ⟹ c ≠ c'"
  by (insert PPc_nonempt, force)

lemma V_nonempt_PPV_nonempt: "V ≠ [] ⟹ PPV V ≠ []"
  by (auto, induct V, simp_all, insert PPc_nonempt, force)

lemma unique_V_uneq:
"⟦V ≠ []; V' ≠ []; set (PPV V) ∩ set (PPV V') = {}⟧ ⟹ V ≠ V'"
  by (auto, induct V, simp_all, insert V_nonempt_PPV_nonempt, auto)

lemma PPc_in_PPV: "c ∈ set V ⟹ set (PPc c) ⊆ set (PPV V)"
  by (induct V, auto)

lemma listindices_aux: "i < length V ⟹ (V!i) ∈ set V"
  by (metis nth_mem)

lemma PPc_in_PPV_version:
  "i < length V ⟹ set (PPc (V!i)) ⊆ set (PPV V)"
  by (rule PPc_in_PPV, erule listindices_aux)

lemma uniPPV_uniPPc: "unique_PPV V ⟹ (∀i < length V. unique_PPc (V!i))"
  by (auto, simp add: unique_PPV_def, induct V,
    auto simp add: unique_PPc_def,
    metis in_set_conv_nth length_Suc_conv set_ConsD)

― ‹SEMANTICS›

locale MWLs_semantics =
fixes E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val ⇒ bool"
begin

― ‹steps semantics, set of deterministic steps from commands to program states›
inductive_set
MWLsSteps_det ::
  "('exp, 'id, 'val, ('exp, 'id) MWLsCom) TLSteps"
and MWLslocSteps_det' ::
  "('exp, 'id, 'val, ('exp, 'id) MWLsCom) TLSteps_curry"
("(1⟨_,/_⟩) →⊲_⊳/ (1⟨_,/_⟩)" [0,0,0,0,0] 81)
where
"⟨c1,m1⟩ →⊲α⊳ ⟨c2,m2⟩ ≡ ((c1,m1),α,(c2,m2)) ∈ MWLsSteps_det" |
skip: "⟨skip⇘ι⇙,m⟩ →⊲[]⊳ ⟨None,m⟩" |
assign: "(E e m) = v ⟹
  ⟨x :=⇘ι⇙ e,m⟩ →⊲[]⊳ ⟨None,m(x := v)⟩" |
seq1: "⟨c1,m⟩ →⊲α⊳ ⟨None,m'⟩ ⟹
  ⟨c1;c2,m⟩ →⊲α⊳ ⟨Some c2,m'⟩" |
seq2: "⟨c1,m⟩ →⊲α⊳ ⟨Some c1',m'⟩ ⟹
  ⟨c1;c2,m⟩ →⊲α⊳ ⟨Some (c1';c2),m'⟩" |
iftrue: "BMap (E b m) = True ⟹
  ⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ →⊲[]⊳ ⟨Some c1,m⟩" |
iffalse: "BMap (E b m) = False ⟹
  ⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ →⊲[]⊳ ⟨Some c2,m⟩" |
whiletrue: "BMap (E b m) = True ⟹
  ⟨while⇘ι⇙ b do c od,m⟩ →⊲[]⊳ ⟨Some (c;(while⇘ι⇙ b do c od)),m⟩" |
whilefalse: "BMap (E b m) = False ⟹
  ⟨while⇘ι⇙ b do c od,m⟩ →⊲[]⊳ ⟨None,m⟩" |
spawn: "⟨spawn⇘ι⇙ V,m⟩ →⊲V⊳ ⟨None,m⟩"

inductive_cases MWLsSteps_det_cases:
"⟨skip⇘ι⇙,m⟩ →⊲α⊳ ⟨p,m'⟩"
"⟨x :=⇘ι⇙ e,m⟩ →⊲α⊳ ⟨p,m'⟩"
"⟨c1;c2,m⟩ →⊲α⊳ ⟨p,m'⟩"
"⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ →⊲α⊳ ⟨p,m'⟩"
"⟨while⇘ι⇙ b do c od,m⟩ →⊲α⊳ ⟨p,m'⟩"
"⟨spawn⇘ι⇙ V,m⟩ →⊲α⊳ ⟨p,m'⟩"

― ‹non-deterministic, possibilistic system step (added for intuition, not used in the proofs)›
inductive_set
MWLsSteps_ndet ::
  "('exp, 'id, 'val, ('exp, 'id) MWLsCom) TPSteps"
and MWLsSteps_ndet' ::
  "('exp, 'id, 'val, ('exp, 'id) MWLsCom) TPSteps_curry"
("(1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩)" [0,0,0,0] 81)
where
"⟨V,m⟩ ⇒ ⟨V',m'⟩ ≡ ((V,m),(V',m')) ∈ MWLsSteps_ndet" |
stepthreadi1: "⟨ci,m⟩ →⊲α⊳ ⟨None,m'⟩ ⟹
  ⟨cf @ [ci] @ ca,m⟩ ⇒ ⟨cf @ α @ ca,m'⟩" |
stepthreadi2: "⟨ci,m⟩ →⊲α⊳ ⟨Some c',m'⟩ ⟹
  ⟨cf @ [ci] @ ca,m⟩ ⇒ ⟨cf @ [c'] @ α @ ca,m⟩"


― ‹lemma about existence and uniqueness of next memory of a step›
lemma nextmem_exists_and_unique:
"∃m' p α. ⟨c,m⟩ →⊲α⊳ ⟨p,m'⟩
  ∧ (∀m''. (∃p α. ⟨c,m⟩ →⊲α⊳ ⟨p,m''⟩) ⟶ m'' = m')"
  by (induct c, auto, metis MWLsSteps_det.skip MWLsSteps_det_cases(1),
    metis MWLsSteps_det_cases(2) MWLsSteps_det.assign,
    metis (no_types) MWLsSteps_det.seq1 MWLsSteps_det.seq2
    MWLsSteps_det_cases(3) not_Some_eq,
    metis MWLsSteps_det.iffalse MWLsSteps_det.iftrue
    MWLsSteps_det_cases(4),
    metis MWLsSteps_det.whilefalse MWLsSteps_det.whiletrue
    MWLsSteps_det_cases(5),
    metis MWLsSteps_det.spawn MWLsSteps_det_cases(6))

lemma PPsc_of_step:
"⟦ ⟨c,m⟩ →⊲α⊳ ⟨p,m'⟩; ∃c'. p = Some c' ⟧
  ⟹ set (PPc (the p)) ⊆ set (PPc c)"
  by (induct rule: MWLsSteps_det.induct, auto)

lemma PPsα_of_step:
"⟨c,m⟩ →⊲α⊳ ⟨p,m'⟩
  ⟹ set (PPV α) ⊆ set (PPc c)"
  by (induct rule: MWLsSteps_det.induct, auto)


end

end