Theory Parallel_Composition

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

locale WHATWHERE_Secure_Programs =
L? : MWLs_semantics "E" "BMap"
+ WWs? : WHATWHERE "MWLsSteps_det" "E" "pp" "DA" "lH"
for E :: "('exp, 'id, 'val) Evalfunction"
and BMap :: "'val  bool"
and DA :: "('id, 'd::order) DomainAssignment"
and lH :: "('d, 'exp) lHatches"
begin

lemma SdlHPPB_restricted_on_PP_is_SdlHPPB:
  assumes SdlHPPB: "SdlHPPB d PP R'"
  assumes inR': "(V,V)  R'"
  assumes Rdef: "R = {(V',V''). (V',V'')  R' 
     set (PPV V')  set (PPV V)
     set (PPV V'')  set (PPV V)}"
  shows "SdlHPPB d PP R"
proof (simp add: Strong_dlHPP_Bisimulation_def, auto)
  from SdlHPPB have "sym R'" 
    by (simp add: Strong_dlHPP_Bisimulation_def)
  with Rdef show "sym R" 
    by (simp add: sym_def)
next
  from SdlHPPB have "trans R'" 
    by (simp add: Strong_dlHPP_Bisimulation_def)
  with Rdef show "trans R" 
    by (simp add: trans_def, auto)
next
  fix V' V''
  assume inR_part: "(V',V'')  R"
  with SdlHPPB Rdef show "length V' = length V''"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
next
  fix V' V'' i
  assume inR_part: "(V',V'')  R"
  assume irange: "i < length V'"
  assume notIDC: 
    "¬ IDC d (V'!i) (htchLoc (pp (V'!i)))"
  with SdlHPPB inR_part irange Rdef 
  show "NDC d (V'!i)"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
next
  fix V' V'' i α p m1 m1' m2
  assume inR_part: "(V',V'')  R"
  assume irange: "i < length V'"
  assume step: "V'!i,m1 →⊲α p,m2"
  assume dhequal: "m1 ∼⇘d,(htchLocSet PP)m1'"
  
  from inR_part SdlHPPB Rdef have eqlen: "length V' = length V''"
    by (simp add: Strong_dlHPP_Bisimulation_def, auto)
  
  from inR_part Rdef 
  have "set (PPV V')  set (PPV V)  set (PPV V'')  set (PPV V)"
    by auto
  
  with irange PPc_in_PPV_version eqlen
  have PPc_Vs_at_i: 
    "set (PPc (V'!i))  set (PPV V)  set (PPc (V''!i))  set (PPV V)"
    by (metis subset_trans)
  
  from SdlHPPB inR_part Rdef irange step dhequal
    strongdlHPPB_aux[of "d" "PP" "R'" "i" 
    "V'" "V''" "m1" "α" "p" "m2" "m1'"]
  obtain p' α' m2' where stepreq: "V''!i,m1' →⊲α' p',m2' 
    stepResultsinR p p' R'  (α,α')  R' 
    dhequality_alternative d PP (pp (V'!i)) m2 m2'"
    by auto
  have Rpp': "stepResultsinR p p' R"
  proof -
    {
      fix c c'
      assume step1: "V'!i,m1 →⊲α Some c,m2"
      assume step2: "V''!i,m1' →⊲α' Some c',m2'"
      assume inR'_res: "([c],[c'])  R'"
      
      from PPc_Vs_at_i step1 step2 PPsc_of_step
      have "set (PPc c)  set (PPV V)  set (PPc c')  set (PPV V)"
        by (metis (no_types) option.sel xt1(6))
      
      with inR'_res Rdef have "([c],[c'])  R"
        by auto
    }
    thus ?thesis      
      by (metis step stepResultsinR_def stepreq)
  qed
             
  have Rαα': "(α,α')  R"
  proof - 
    from PPc_Vs_at_i step stepreq PPsα_of_step have 
      "set (PPV α)  set (PPV V)  set (PPV α')  set (PPV V)"
      by (metis (no_types) xt1(6))
    with stepreq Rdef show ?thesis
      by auto
  qed
  
  from stepreq Rpp' Rαα' show 
    "p' α' m2'. V''!i,m1' →⊲α' p',m2' 
    stepResultsinR p p' R  (α,α')  R 
    dhequality_alternative d PP (pp (V'!i)) m2 m2'"
    by auto
qed


theorem parallel_composition:
  " i < length V. WHATWHERE_Secure [V!i]; unique_PPV V 
   WHATWHERE_Secure V"
proof (simp add: WHATWHERE_Secure_def, induct V, auto)
  fix d PP
  from WHATWHERE_empty 
  show "R. SdlHPPB d PP R  ([],[])  R"
    by (simp add: WHATWHERE_Secure_def)
next
  fix c V d PP
  assume IH: " i < length V.
    d PP. R. SdlHPPB d PP R  ([V!i],[V!i])  R;
    unique_PPV V 
     d PP. R. SdlHPPB d PP R  (V,V)  R"
  assume ISassump: "i < Suc (length V).
    d PP. R. SdlHPPB d PP R  ([(c#V)!i],[(c#V)!i])  R"
  assume uniPPcV: "unique_PPV (c#V)"
  
  hence IHassump1: "unique_PPV V"
    by (simp add: unique_PPV_def)

  from uniPPcV have nocommonPP: "set (PPc c)  set (PPV V) = {}"
    by (simp add: unique_PPV_def)
  
  from ISassump have IHassump2: "i < length V. 
    d PP. R. SdlHPPB d PP R  ([V!i],[V!i])  R"
    by auto

  with IHassump1 IH obtain RV' where RV'assump:
    "SdlHPPB d PP RV'  (V,V)  RV'"
    by blast

  define RV where "RV = {(V',V''). (V',V'')  RV'  set (PPV V')  set (PPV V)
     set (PPV V'')  set (PPV V)}"

  with RV'assump RV_def SdlHPPB_restricted_on_PP_is_SdlHPPB
  have SdlHPPRV: "SdlHPPB d PP RV"
    by force

  from ISassump obtain Rc' where Rc'assump: 
    "SdlHPPB d PP Rc'  ([c],[c])  Rc'"
    by (metis append_Nil drop_Nil neq0_conv not_Cons_self 
      nth_append_length Cons_nth_drop_Suc zero_less_Suc)
 
  define Rc where "Rc = {(V',V''). (V',V'')  Rc'  set (PPV V')  set (PPc c)
     set (PPV V'')  set (PPc c)}"

  with Rc'assump Rc_def SdlHPPB_restricted_on_PP_is_SdlHPPB
  have SdlHPPRc: "SdlHPPB d PP Rc"
    by force

  from nocommonPP have "Domain RV  Domain Rc  {[]}"
    by (simp add: RV_def Rc_def, auto,
      metis Int_mono inf_commute inf_idem le_bot nocommonPP unique_V_uneq)

  with commonArefl_subset_commonDomain
  have Areflassump1: "Arefl RV  Arefl Rc  {[]}"
    by force
    
  define R where "R = {(V',V''). c c' W W'. V' = c#W  V'' = c'#W'  W  []
     W'  []  ([c],[c'])  Rc  (W,W')  RV}"

  with RV_def RV'assump Rc_def Rc'assump have inR: 
    "V  []  (c#V,c#V)  R"
    by auto
    
  from R_def Rc_def RV_def nocommonPP
  have "Domain R  Domain (Rc  RV) = {}"
    by (simp add: R_def Rc_def RV_def, auto,
      metis inf_bot_right le_inf_iff subset_empty unique_V_uneq,
      metis (opaque_lifting, no_types) inf_absorb1 inf_bot_right le_inf_iff unique_c_uneq)
            
  with commonArefl_subset_commonDomain
  have Areflassump2: "Arefl R  Arefl (Rc  RV)  {[]}"
    by force

  have disjuptoR: 
    "disj_dlHPP_Bisimulation_Up_To_R' d PP (Rc  RV) R"
    proof (simp add: disj_dlHPP_Bisimulation_Up_To_R'_def, auto)
        from Areflassump1 SdlHPPRc SdlHPPRV Union_Strong_dlHPP_Bisim
        show "SdlHPPB d PP (Rc  RV)"
          by force
      next
        from SdlHPPRV have symRV: "sym RV"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        from SdlHPPRc have symRc: "sym Rc"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        with symRV R_def show "sym R"
          by (simp add: sym_def, auto)
      next
        from SdlHPPRV have transRV: "trans RV"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        from SdlHPPRc have transRc: "trans Rc"
          by (simp add: Strong_dlHPP_Bisimulation_def)
        show "trans R"
           proof -
            {
            fix V V' V''
            assume p1: "(V,V')  R"
            assume p2: "(V',V'')  R"
            have "(V,V'')  R"
              proof -
                from p1 R_def obtain c c' W W' where p1assump:
                  "V = c#W  V' = c'#W'  W  []  W'  [] 
                  ([c],[c'])  Rc  (W,W')  RV"
                  by auto
                with p2 R_def obtain c'' W'' where p2assump:
                  "V'' = c''#W''  W''  [] 
                  ([c'],[c''])  Rc  (W',W'')  RV"
                  by auto
                with p1assump transRc transRV have 
                  trans_assump: "([c],[c''])  Rc  (W,W'')  RV"
                  by (simp add: trans_def, blast)
                with p1assump p2assump R_def show ?thesis
                  by auto
              qed
             }
            thus ?thesis unfolding trans_def by blast
           qed
      next
        fix V V'
        assume "(V,V')  R"
        with R_def SdlHPPRV show "length V = length V'"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)
      next
        fix V V' i
        assume inR: "(V,V')  R"
        assume irange: "i < length V"
        assume notIDC: "¬ IDC d (V!i) 
          (htchLoc (pp (V!i)))"
        from inR R_def obtain c c' W W' where VV'assump:
          "V = c#W  V'=c'#W'  W  []  W'  [] 
          ([c],[c'])  Rc  (W,W')  RV"
          by auto
        ― ‹Case separation for i›
        from VV'assump SdlHPPRc have Case_i0:
          "i = 0  (NDC d (V!i) 
            IDC d (V!i) (htchLoc (pp (V!i))))"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)

        from VV'assump SdlHPPRV have "i < length W. 
          (NDC d (W!i) 
            IDC d (W!i) (htchLoc (pp (W!i))))"
          by (simp add: Strong_dlHPP_Bisimulation_def, auto)

        with irange VV'assump have Case_in0:
          "i > 0  (NDC d (V!i)  
          IDC d (V!i) (htchLoc (pp (V!i))))"
          by simp
        from notIDC Case_i0 Case_in0 
        show "NDC d (V!i)"
          by auto
      next
        fix V V' m1 m1' m2 α p i
        assume inR: "(V,V')  R"
        assume irange: "i < length V"
        assume step: "V!i,m1 →⊲α p,m2"
        assume dhequal: "m1 ∼⇘d,(htchLocSet PP)m1'"
        
        from inR R_def obtain c c' W W' where VV'assump:
          "V = c#W  V'=c'#W'  W  []  W'  [] 
          ([c],[c'])  Rc  (W,W')  RV"
          by auto
        ― ‹Case separation for i›
        from VV'assump SdlHPPRc strongdlHPPB_aux[of "d" "PP" 
          "Rc" "0" "[c]" "[c']"] step dhequal
        have Case_i0:
          "i = 0  p' α' m2'.
          V'!i,m1' →⊲α' p',m2' 
          stepResultsinR p p' (R  (Rc  RV)) 
          ((α,α')  R  (α,α')  Rc  (α,α')  RV) 
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by (simp add: stepResultsinR_def, blast)

        from step VV'assump irange have rewV: 
          "i > 0  (i-Suc 0) < length W  V!i = W!(i-Suc 0)"
          by simp

        with irange VV'assump step dhequal SdlHPPRV 
          strongdlHPPB_aux[of "d" "PP" "RV" _ "W" "W'"]
        have Case_in0:
          "i > 0   p' α' m2'.
          V'!i,m1' →⊲α' p',m2' 
          stepResultsinR p p' (R  (Rc  RV)) 
          ((α,α')  R  (α,α')  Rc  (α,α')  RV) 
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by (simp add: stepResultsinR_def, blast)
        
        from Case_i0 Case_in0 
        show "p' α' m2'.
          V'!i,m1' →⊲α' p',m2' 
          stepResultsinR p p' (R  (Rc  RV)) 
          ((α,α')  R  (α,α')  Rc  (α,α')  RV) 
          dhequality_alternative d PP (pp (V!i)) m2 m2'"
          by auto
      qed
  with Areflassump2 Rc'assump Up_To_Technique
  show "R. SdlHPPB d PP R  (c#V, c#V)  R"
    by (metis UnCI inR)

qed

end

end