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, simp_all)
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⟨_,/_⟩) ->\<lhd>_\<rhd>/ (1⟨_,/_⟩)" [0,0,0,0,0] 81)
where
"⟨c1,m1⟩ ->\<lhd>α\<rhd> ⟨c2,m2⟩ ≡ ((c1,m1),α,(c2,m2)) ∈ MWLsSteps_det" |
skip: "⟨skip⇘ι⇙,m⟩ ->\<lhd>[]\<rhd> ⟨None,m⟩" |
assign: "(E e m) = v ==>
⟨x :=⇘ι⇙ e,m⟩ ->\<lhd>[]\<rhd> ⟨None,m(x := v)⟩" |
seq1: "⟨c1,m⟩ ->\<lhd>α\<rhd> ⟨None,m'⟩ ==>
⟨c1;c2,m⟩ ->\<lhd>α\<rhd> ⟨Some c2,m'⟩" |
seq2: "⟨c1,m⟩ ->\<lhd>α\<rhd> ⟨Some c1',m'⟩ ==>
⟨c1;c2,m⟩ ->\<lhd>α\<rhd> ⟨Some (c1';c2),m'⟩" |
iftrue: "BMap (E b m) = True ==>
⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ ->\<lhd>[]\<rhd> ⟨Some c1,m⟩" |
iffalse: "BMap (E b m) = False ==>
⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ ->\<lhd>[]\<rhd> ⟨Some c2,m⟩" |
whiletrue: "BMap (E b m) = True ==>
⟨while⇘ι⇙ b do c od,m⟩ ->\<lhd>[]\<rhd> ⟨Some (c;(while⇘ι⇙ b do c od)),m⟩" |
whilefalse: "BMap (E b m) = False ==>
⟨while⇘ι⇙ b do c od,m⟩ ->\<lhd>[]\<rhd> ⟨None,m⟩" |
spawn: "⟨spawn⇘ι⇙ V,m⟩ ->\<lhd>V\<rhd> ⟨None,m⟩"
inductive_cases MWLsSteps_det_cases:
"⟨skip⇘ι⇙,m⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩"
"⟨x :=⇘ι⇙ e,m⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩"
"⟨c1;c2,m⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩"
"⟨if⇘ι⇙ b then c1 else c2 fi,m⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩"
"⟨while⇘ι⇙ b do c od,m⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩"
"⟨spawn⇘ι⇙ V,m⟩ ->\<lhd>α\<rhd> ⟨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⟩ ->\<lhd>α\<rhd> ⟨None,m'⟩ ==>
⟨cf @ [ci] @ ca,m⟩ => ⟨cf @ α @ ca,m'⟩" |
stepthreadi2: "⟨ci,m⟩ ->\<lhd>α\<rhd> ⟨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⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩
∧ (∀m''. (∃p α. ⟨c,m⟩ ->\<lhd>α\<rhd> ⟨p,m''⟩) --> m'' = m')"
by (induct, 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⟩ ->\<lhd>α\<rhd> ⟨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⟩ ->\<lhd>α\<rhd> ⟨p,m'⟩
==> set (PPV α) ⊆ set (PPc c)"
by (induct rule: MWLsSteps_det.induct, auto)
end
end