Theory NonInterferenceWhile

section ‹Information Flow for While›

theory NonInterferenceWhile imports
  Slicing.SemanticsWellFormed
  Slicing.StaticControlDependences
  LiftingIntra
begin

locale SecurityTypes =
  fixes H :: "vname set"
  fixes L :: "vname set"
  assumes HighLowDistinct: "H ∩ L = {}"
  and HighLowUNIV: "H ∪ L = UNIV"
begin


subsection ‹Lifting @{term labels_nodes} and Defining ‹final››

fun labels_LDCFG_nodes :: "cmd ⇒ w_node LDCFG_node ⇒ cmd ⇒ bool"
  where "labels_LDCFG_nodes prog (Node n) c = labels_nodes prog n c"
  | "labels_LDCFG_nodes prog n c = False"



lemmas WCFG_path_induct[consumes 1, case_names empty_path Cons_path]
  = CFG.path.induct[OF While_CFG_aux]


lemma lift_valid_node:
  assumes "CFG.valid_node sourcenode targetnode (valid_edge prog) n"
  shows "CFG.valid_node src trg
  (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
  (Node n)"
proof -
  from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) n›
  obtain a where "valid_edge prog a" and "n = sourcenode a ∨ n = targetnode a"
    by(fastforce simp:While_CFG.valid_node_def)
  from ‹n = sourcenode a ∨ n = targetnode a›
  show ?thesis
  proof
    assume "n = sourcenode a"
    show ?thesis
    proof(cases "sourcenode a = Entry")
      case True
      have "lift_valid_edge (valid_edge prog) sourcenode targetnode kind Entry Exit 
        (NewEntry,(λs. True)√,Node Entry)"
        by(fastforce intro:lve_Entry_edge)
      with While_CFGExit_wf_aux[of prog] ‹n = sourcenode a› True show ?thesis
        by(fastforce simp:CFG.valid_node_def[OF lift_CFG])
    next
      case False
      with ‹valid_edge prog a› ‹n = sourcenode a ∨ n = targetnode a›
      have "lift_valid_edge (valid_edge prog) sourcenode targetnode kind Entry Exit 
        (Node (sourcenode a),kind a,Node (targetnode a))"
        by(fastforce intro:lve_edge)
      with While_CFGExit_wf_aux[of prog] ‹n = sourcenode a› show ?thesis
        by(fastforce simp:CFG.valid_node_def[OF lift_CFG])
    qed
  next
    assume "n = targetnode a"
    show ?thesis
    proof(cases "targetnode a = Exit")
      case True
      have "lift_valid_edge (valid_edge prog) sourcenode targetnode kind Entry Exit 
        (Node Exit,(λs. True)√,NewExit)"
        by(fastforce intro:lve_Exit_edge)
      with While_CFGExit_wf_aux[of prog] ‹n = targetnode a› True show ?thesis
        by(fastforce simp:CFG.valid_node_def[OF lift_CFG])
    next
      case False
      with ‹valid_edge prog a› ‹n = sourcenode a ∨ n = targetnode a›
      have "lift_valid_edge (valid_edge prog) sourcenode targetnode kind Entry Exit 
        (Node (sourcenode a),kind a,Node (targetnode a))"
        by(fastforce intro:lve_edge)
      with While_CFGExit_wf_aux[of prog] ‹n = targetnode a› show ?thesis
        by(fastforce simp:CFG.valid_node_def[OF lift_CFG])
    qed
  qed
qed



lemma lifted_CFG_fund_prop:
  assumes "labels_LDCFG_nodes prog n c" and "⟨c,s⟩ →* ⟨c',s'⟩"
  shows "∃n' as. CFG.path src trg
  (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
  n as n' ∧ transfers (CFG.kinds knd as) s = s' ∧
  preds (CFG.kinds knd as) s ∧ labels_LDCFG_nodes prog n' c'"
proof -
  from ‹labels_LDCFG_nodes prog n c› obtain nx where "n = Node nx"
    and "labels_nodes prog nx c" by(cases n) auto
  from ‹labels_nodes prog nx c› ‹⟨c,s⟩ →* ⟨c',s'⟩›
  obtain n' as where "prog ⊢ nx -as→* n'" and "transfers (CFG.kinds kind as) s = s'"
    and "preds (CFG.kinds kind as) s" and "labels_nodes prog n' c'"
    by(auto dest:While_semantics_CFG_wf.fundamental_property)
  from ‹labels_nodes prog n' c'› have "labels_LDCFG_nodes prog (Node n') c'"
    by simp
  from ‹prog ⊢ nx -as→* n'› ‹transfers (CFG.kinds kind as) s = s'› 
    ‹preds (CFG.kinds kind as) s› ‹n = Node nx›
    ‹labels_nodes prog nx c› ‹labels_nodes prog n' c'›
  have "∃es. CFG.path src trg
    (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
    (Node nx) es (Node n') ∧ transfers (CFG.kinds knd es) s = s' ∧
    preds (CFG.kinds knd es) s"
  proof(induct arbitrary:n s c rule:WCFG_path_induct)
    case (empty_path n nx)
    from ‹CFG.valid_node sourcenode targetnode (valid_edge prog) n›
    have valid_node:"CFG.valid_node src trg
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
      (Node n)"
      by(rule lift_valid_node)
    have "CFG.kinds knd 
      ([]::(w_node LDCFG_node × state edge_kind × w_node LDCFG_node) list) = []"
      by(simp add:CFG.kinds_def[OF lift_CFG[OF While_CFGExit_wf_aux]])
    with ‹transfers (CFG.kinds kind []) s = s'› ‹preds (CFG.kinds kind []) s›
      valid_node
    show ?case
      by(fastforce intro:CFG.empty_path[OF lift_CFG[OF While_CFGExit_wf_aux]] 
                   simp:While_CFG.kinds_def)
  next
    case (Cons_path n'' as n' a nx)
    note IH = ‹⋀n s c. ⟦transfers (CFG.kinds kind as) s = s'; 
      preds (CFG.kinds kind as) s; n = LDCFG_node.Node n''; 
      labels_nodes prog n'' c; labels_nodes prog n' c'⟧
      ⟹ ∃es. CFG.path src trg
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
      (LDCFG_node.Node n'') es (LDCFG_node.Node n') ∧
      transfers (CFG.kinds knd es) s = s' ∧ preds (CFG.kinds knd es) s›
    from ‹transfers (CFG.kinds kind (a # as)) s = s'›
    have "transfers (CFG.kinds kind as) (transfer (kind a) s) = s'"
      by(simp add:While_CFG.kinds_def)
    from ‹preds (CFG.kinds kind (a # as)) s›
    have "preds (CFG.kinds kind as) (transfer (kind a) s)"
      and "pred (kind a) s" by(simp_all add:While_CFG.kinds_def)
    show ?case
    proof(cases "sourcenode a = (_Entry_)")
      case True
      with ‹sourcenode a = nx› ‹labels_nodes prog nx c› have False by simp
      thus ?thesis by simp
    next
      case False
      with ‹valid_edge prog a›
      have edge:"lift_valid_edge (valid_edge prog) sourcenode targetnode kind 
        Entry Exit (Node (sourcenode a),kind a,Node (targetnode a))"
        by(fastforce intro:lve_edge)
      from ‹prog ⊢ n'' -as→* n'›
      have "CFG.valid_node sourcenode targetnode (valid_edge prog) n''"
        by(rule While_CFG.path_valid_node)
      then obtain c'' where "labels_nodes prog n'' c''"
      proof(cases rule:While_CFGExit.valid_node_cases)
        case Entry
        with ‹targetnode a = n''› ‹valid_edge prog a› have False by fastforce
        thus ?thesis by simp
      next
        case Exit
        with ‹prog ⊢ n'' -as→* n'› have "n' = (_Exit_)" by fastforce
        with ‹labels_nodes prog n' c'› have False by fastforce
        thus ?thesis by simp
      next
        case inner
        then obtain l'' where [simp]:"n'' = (_ l'' _)" by(cases n'') auto
        with ‹valid_edge prog a› ‹targetnode a = n''› have "l'' < #:prog"
          by(fastforce intro:WCFG_targetlabel_less_num_nodes simp:valid_edge_def)
        then obtain c'' where "labels prog l'' c''"
          by(fastforce dest:less_num_inner_nodes_label)
        with that show ?thesis by fastforce
      qed
      from IH[OF ‹transfers (CFG.kinds kind as) (transfer (kind a) s) = s'›
        ‹preds (CFG.kinds kind as) (transfer (kind a) s)› _ this 
        ‹labels_nodes prog n' c'›]
      obtain es where "CFG.path src trg
        (lift_valid_edge (valid_edge prog) sourcenode targetnode kind 
        (_Entry_) (_Exit_)) (LDCFG_node.Node n'') es (LDCFG_node.Node n')"
        and "transfers (CFG.kinds knd es) (transfer (kind a) s) = s'"
        and "preds (CFG.kinds knd es) (transfer (kind a) s)" by blast
      with ‹targetnode a = n''› ‹sourcenode a = nx› edge
      have path:"CFG.path src trg
        (lift_valid_edge (valid_edge prog) sourcenode targetnode 
        kind (_Entry_) (_Exit_))
        (LDCFG_node.Node nx) ((Node (sourcenode a),kind a,Node (targetnode a))#es) 
        (LDCFG_node.Node n')"
        by(fastforce intro:CFG.Cons_path[OF lift_CFG[OF While_CFGExit_wf_aux]])
      from edge have "knd (Node (sourcenode a),kind a,Node (targetnode a)) = kind a"
        by(simp add:knd_def)
      with ‹transfers (CFG.kinds knd es) (transfer (kind a) s) = s'›
        ‹preds (CFG.kinds knd es) (transfer (kind a) s)› ‹pred (kind a) s›
      have "transfers 
        (CFG.kinds knd ((Node (sourcenode a),kind a,Node (targetnode a))#es)) s = s'"
        and "preds 
        (CFG.kinds knd ((Node (sourcenode a),kind a,Node (targetnode a))#es)) s"
        by(auto simp:CFG.kinds_def[OF lift_CFG[OF While_CFGExit_wf_aux]])
      with path show ?thesis by blast
    qed
  qed
  with ‹n = Node nx› ‹labels_LDCFG_nodes prog (Node n') c'›
  show ?thesis by fastforce
qed



fun final :: "cmd ⇒ bool"
  where "final Skip = True"
  | "final c = False"


lemma final_edge:
  "labels_nodes prog n Skip ⟹ prog ⊢ n -⇑id→ (_Exit_)"
proof(induct prog arbitrary:n)
  case Skip
  from ‹labels_nodes Skip n Skip› have "n = (_ 0 _)" 
    by(cases n)(auto elim:labels.cases)
  thus ?case by(fastforce intro:WCFG_Skip)
next
  case (LAss V e)
  from ‹labels_nodes (V:=e) n Skip› have "n = (_ 1 _)" 
    by(cases n)(auto elim:labels.cases)
  thus ?case by(fastforce intro:WCFG_LAssSkip)
next
  case (Seq c1 c2)
  note IH2 = ‹⋀n. labels_nodes c2 n Skip ⟹ c2 ⊢ n -⇑id→ (_Exit_)›
  from ‹labels_nodes (c1;; c2) n Skip› obtain l where "n = (_ l _)"
    and "l ≥ #:c1" and "labels_nodes c2 (_ l - #:c1 _) Skip"
    by(cases n)(auto elim:labels.cases)
  from IH2[OF ‹labels_nodes c2 (_ l - #:c1 _) Skip›]
  have "c2 ⊢ (_ l - #:c1 _) -⇑id→ (_Exit_)" .
  with ‹l ≥ #:c1› have "c1;;c2 ⊢ (_ l - #:c1 _) ⊕ #:c1 -⇑id→ (_Exit_) ⊕ #:c1"
    by(fastforce intro:WCFG_SeqSecond)
  with ‹n = (_ l _)› ‹l ≥ #:c1› show ?case by(simp add:id_def)
next
  case (Cond b c1 c2)
  note IH1 = ‹⋀n. labels_nodes c1 n Skip ⟹ c1 ⊢ n -⇑id→ (_Exit_)›
  note IH2 = ‹⋀n. labels_nodes c2 n Skip ⟹ c2 ⊢ n -⇑id→ (_Exit_)›
  from ‹labels_nodes (if (b) c1 else c2) n Skip›
  obtain l where "n = (_ l _)" and disj:"(l ≥ 1 ∧ labels_nodes c1 (_ l - 1 _) Skip) ∨
    (l ≥ #:c1 + 1 ∧ labels_nodes c2 (_ l - #:c1 - 1 _) Skip)"
    by(cases n) (fastforce elim:labels.cases)+
  from disj show ?case
  proof
    assume "1 ≤ l ∧ labels_nodes c1 (_ l - 1 _) Skip"
    hence "1 ≤ l" and "labels_nodes c1 (_ l - 1 _) Skip" by simp_all
    from IH1[OF ‹labels_nodes c1 (_ l - 1 _) Skip›] 
    have "c1 ⊢ (_ l - 1 _) -⇑id→ (_Exit_)" .
    with ‹1 ≤ l› have "if (b) c1 else c2 ⊢ (_ l - 1 _) ⊕ 1 -⇑id→ (_Exit_) ⊕ 1"
      by(fastforce intro:WCFG_CondThen)
    with ‹n = (_ l _)› ‹1 ≤ l› show ?case by(simp add:id_def)
  next
    assume "#:c1 + 1 ≤ l ∧ labels_nodes c2 (_ l - #:c1 - 1 _) Skip"
    hence "#:c1 + 1 ≤ l" and "labels_nodes c2 (_ l - #:c1 - 1 _) Skip" by simp_all
    from IH2[OF ‹labels_nodes c2 (_ l - #:c1 - 1 _) Skip›]
    have "c2 ⊢ (_ l - #:c1 - 1 _) -⇑id→ (_Exit_)" .
    with ‹#:c1 + 1 ≤ l› have "if (b) c1 else c2 ⊢ (_ l - #:c1 - 1 _) ⊕ (#:c1 + 1)
      -⇑id→ (_Exit_) ⊕ (#:c1 + 1)"
      by(fastforce intro:WCFG_CondElse)
    with ‹n = (_ l _)› ‹#:c1 + 1 ≤ l› show ?case by(simp add:id_def)
  qed
next
  case (While b c)
  from ‹labels_nodes (while (b) c) n Skip› have "n = (_ 1 _)" 
    by(cases n)(auto elim:labels.cases)
  thus ?case by(fastforce intro:WCFG_WhileFalseSkip)
qed




subsection ‹Semantic Non-Interference for Weak Order Dependence›

lemmas WODNonInterferenceGraph = 
  lift_wod_backward_slice[OF While_CFGExit_wf_aux HighLowDistinct HighLowUNIV]


lemma WODNonInterference:
  "NonInterferenceIntra src trg knd
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_))
     NewEntry (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
     (lift_Use (Uses prog) (_Entry_) (_Exit_) H L) id
     (CFG_wf.wod_backward_slice src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L))
     reds (labels_LDCFG_nodes prog)
     NewExit H L (LDCFG_node.Node (_Entry_)) (LDCFG_node.Node (_Exit_)) final"
proof -
  interpret NonInterferenceIntraGraph src trg knd
     "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_)"
     NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
     "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
     "CFG_wf.wod_backward_slice src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)"
     NewExit H L "LDCFG_node.Node (_Entry_)" "LDCFG_node.Node (_Exit_)"
    by(rule WODNonInterferenceGraph)
  interpret BackwardSlice_wf src trg knd
    "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
      (_Entry_) (_Exit_)"
    NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
    "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
    "CFG_wf.wod_backward_slice src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)" reds "labels_LDCFG_nodes prog"
  proof(unfold_locales)
    fix n c s c' s'
    assume "labels_LDCFG_nodes prog n c" and "⟨c,s⟩ →* ⟨c',s'⟩"
    thus "∃n' as. CFG.path src trg
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
      n as n' ∧ transfers (CFG.kinds knd as) s = s' ∧
      preds (CFG.kinds knd as) s ∧ labels_LDCFG_nodes prog n' c'"
      by(rule lifted_CFG_fund_prop)
  qed
  show ?thesis 
  proof(unfold_locales)
    fix c n
    assume "final c" and "labels_LDCFG_nodes prog n c"
    from ‹final c› have [simp]:"c = Skip" by(cases c) auto
    from ‹labels_LDCFG_nodes prog n c› obtain nx where [simp]:"n = Node nx"
      and "labels_nodes prog nx Skip" by(cases n) auto
    from ‹labels_nodes prog nx Skip› have "prog ⊢ nx -⇑id→ (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = ⇑id" and "targetnode a = (_Exit_)"
      by(auto simp:valid_edge_def)
    with ‹labels_nodes prog nx Skip›
    show "∃a. lift_valid_edge (valid_edge prog) sourcenode targetnode
      kind (_Entry_) (_Exit_) a ∧
      src a = n ∧ trg a = LDCFG_node.Node (_Exit_) ∧ knd a = ⇑id"
      by(rule_tac x="(Node nx,⇑id,Node (_Exit_))" in exI)
        (auto intro!:lve_edge simp:knd_def valid_edge_def)
  qed
qed


subsection ‹Semantic Non-Interference for Standard Control Dependence›

lemma inner_node_exists:"∃n. CFGExit.inner_node sourcenode targetnode 
  (valid_edge prog) (_Entry_) (_Exit_) n"
proof -
  have "prog ⊢ (_Entry_) -(λs. True)√→ (_0_)" by(rule WCFG_Entry)
  hence "CFG.valid_node sourcenode targetnode (valid_edge prog) (_0_)"
    by(auto simp:While_CFG.valid_node_def valid_edge_def)
  thus ?thesis by(auto simp:While_CFGExit.inner_node_def)
qed


lemmas SCDNonInterferenceGraph = 
  lift_PDG_standard_backward_slice[OF WStandardControlDependence.PDG_scd 
  WhilePostdomination_aux _ HighLowDistinct HighLowUNIV]


lemma SCDNonInterference:
  "NonInterferenceIntra src trg knd
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_))
     NewEntry (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
     (lift_Use (Uses prog) (_Entry_) (_Exit_) H L) id
     (PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (Postdomination.standard_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit))
     reds (labels_LDCFG_nodes prog)
     NewExit H L (LDCFG_node.Node (_Entry_)) (LDCFG_node.Node (_Exit_)) final"
proof -
  from inner_node_exists obtain n where "CFGExit.inner_node sourcenode targetnode 
    (valid_edge prog) (_Entry_) (_Exit_) n" by blast
  then interpret NonInterferenceIntraGraph src trg knd
     "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_)"
     NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
     "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
     "PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (Postdomination.standard_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit)"
     NewExit H L "LDCFG_node.Node (_Entry_)" "LDCFG_node.Node (_Exit_)"
    by(fastforce intro:SCDNonInterferenceGraph)
  interpret BackwardSlice_wf src trg knd
    "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
      (_Entry_) (_Exit_)"
    NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
    "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
    "PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (Postdomination.standard_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit)" reds "labels_LDCFG_nodes prog"
  proof(unfold_locales)
    fix n c s c' s'
    assume "labels_LDCFG_nodes prog n c" and "⟨c,s⟩ →* ⟨c',s'⟩"
    thus "∃n' as. CFG.path src trg
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
      n as n' ∧ transfers (CFG.kinds knd as) s = s' ∧
      preds (CFG.kinds knd as) s ∧ labels_LDCFG_nodes prog n' c'"
      by(rule lifted_CFG_fund_prop)
  qed
  show ?thesis 
  proof(unfold_locales)
    fix c n
    assume "final c" and "labels_LDCFG_nodes prog n c"
    from ‹final c› have [simp]:"c = Skip" by(cases c) auto
    from ‹labels_LDCFG_nodes prog n c› obtain nx where [simp]:"n = Node nx"
      and "labels_nodes prog nx Skip" by(cases n) auto
    from ‹labels_nodes prog nx Skip› have "prog ⊢ nx -⇑id→ (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = ⇑id" and "targetnode a = (_Exit_)"
      by(auto simp:valid_edge_def)
    with ‹labels_nodes prog nx Skip›
    show "∃a. lift_valid_edge (valid_edge prog) sourcenode targetnode
      kind (_Entry_) (_Exit_) a ∧
      src a = n ∧ trg a = LDCFG_node.Node (_Exit_) ∧ knd a = ⇑id"
      by(rule_tac x="(Node nx,⇑id,Node (_Exit_))" in exI)
        (auto intro!:lve_edge simp:knd_def valid_edge_def)
  qed
qed


subsection ‹Semantic Non-Interference for Weak Control Dependence›

lemmas WCDNonInterferenceGraph = 
  lift_PDG_weak_backward_slice[OF WWeakControlDependence.PDG_wcd 
  WhileStrongPostdomination_aux _ HighLowDistinct HighLowUNIV]


lemma WCDNonInterference:
  "NonInterferenceIntra src trg knd
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_))
     NewEntry (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
     (lift_Use (Uses prog) (_Entry_) (_Exit_) H L) id
     (PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (StrongPostdomination.weak_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit))
     reds (labels_LDCFG_nodes prog)
     NewExit H L (LDCFG_node.Node (_Entry_)) (LDCFG_node.Node (_Exit_)) final"
proof -
  from inner_node_exists obtain n where "CFGExit.inner_node sourcenode targetnode 
    (valid_edge prog) (_Entry_) (_Exit_) n" by blast
  then interpret NonInterferenceIntraGraph src trg knd
     "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
       (_Entry_) (_Exit_)"
     NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
     "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
     "PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (StrongPostdomination.weak_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit)"
     NewExit H L "LDCFG_node.Node (_Entry_)" "LDCFG_node.Node (_Exit_)"
    by(fastforce intro:WCDNonInterferenceGraph)
  interpret BackwardSlice_wf src trg knd
    "lift_valid_edge (valid_edge prog) sourcenode targetnode kind
      (_Entry_) (_Exit_)"
    NewEntry "lift_Def (Defs prog) (_Entry_) (_Exit_) H L"
    "lift_Use (Uses prog) (_Entry_) (_Exit_) H L" id
    "PDG.PDG_BS src trg
       (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
         (_Entry_) (_Exit_))
       (lift_Def (Defs prog) (_Entry_) (_Exit_) H L)
       (lift_Use (Uses prog) (_Entry_) (_Exit_) H L)
       (StrongPostdomination.weak_control_dependence src trg
         (lift_valid_edge (valid_edge prog) sourcenode targetnode kind
           (_Entry_) (_Exit_)) NewExit)" reds "labels_LDCFG_nodes prog"
  proof(unfold_locales)
    fix n c s c' s'
    assume "labels_LDCFG_nodes prog n c" and "⟨c,s⟩ →* ⟨c',s'⟩"
    thus "∃n' as. CFG.path src trg
     (lift_valid_edge (valid_edge prog) sourcenode targetnode kind (_Entry_) (_Exit_))
      n as n' ∧ transfers (CFG.kinds knd as) s = s' ∧
      preds (CFG.kinds knd as) s ∧ labels_LDCFG_nodes prog n' c'"
      by(rule lifted_CFG_fund_prop)
  qed
  show ?thesis 
  proof(unfold_locales)
    fix c n
    assume "final c" and "labels_LDCFG_nodes prog n c"
    from ‹final c› have [simp]:"c = Skip" by(cases c) auto
    from ‹labels_LDCFG_nodes prog n c› obtain nx where [simp]:"n = Node nx"
      and "labels_nodes prog nx Skip" by(cases n) auto
    from ‹labels_nodes prog nx Skip› have "prog ⊢ nx -⇑id→ (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = ⇑id" and "targetnode a = (_Exit_)"
      by(auto simp:valid_edge_def)
    with ‹labels_nodes prog nx Skip›
    show "∃a. lift_valid_edge (valid_edge prog) sourcenode targetnode
      kind (_Entry_) (_Exit_) a ∧
      src a = n ∧ trg a = LDCFG_node.Node (_Exit_) ∧ knd a = ⇑id"
      by(rule_tac x="(Node nx,⇑id,Node (_Exit_))" in exI)
        (auto intro!:lve_edge simp:knd_def valid_edge_def)
  qed
qed

end

end