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