Theory NonInterferenceWhile

header {* \isaheader{Information Flow for While} *}

theory NonInterferenceWhile imports
  SemanticsWellFormed
  StaticControlDependences
  "../../InformationFlowSlicing/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 @{text 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)⇣\<surd>,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)⇣\<surd>,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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> 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 \<turnstile> n -\<Up>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 c⇣1 c⇣2)
  note IH2 = `!!n. labels_nodes c⇣2 n Skip ==> c⇣2 \<turnstile> n -\<Up>id-> (_Exit_)`
  from `labels_nodes (c⇣1;; c⇣2) n Skip` obtain l where "n = (_ l _)"
    and "l ≥ #:c⇣1" and "labels_nodes c⇣2 (_ l - #:c⇣1 _) Skip"
    by(cases n)(auto elim:labels.cases)
  from IH2[OF `labels_nodes c⇣2 (_ l - #:c⇣1 _) Skip`]
  have "c⇣2 \<turnstile> (_ l - #:c⇣1 _) -\<Up>id-> (_Exit_)" .
  with `l ≥ #:c⇣1` have "c⇣1;;c⇣2 \<turnstile> (_ l - #:c⇣1 _) ⊕ #:c⇣1 -\<Up>id-> (_Exit_) ⊕ #:c⇣1"
    by(fastforce intro:WCFG_SeqSecond)
  with `n = (_ l _)` `l ≥ #:c⇣1` show ?case by(simp add:id_def)
next
  case (Cond b c⇣1 c⇣2)
  note IH1 = `!!n. labels_nodes c⇣1 n Skip ==> c⇣1 \<turnstile> n -\<Up>id-> (_Exit_)`
  note IH2 = `!!n. labels_nodes c⇣2 n Skip ==> c⇣2 \<turnstile> n -\<Up>id-> (_Exit_)`
  from `labels_nodes (if (b) c⇣1 else c⇣2) n Skip`
  obtain l where "n = (_ l _)" and disj:"(l ≥ 1 ∧ labels_nodes c⇣1 (_ l - 1 _) Skip) ∨
    (l ≥ #:c⇣1 + 1 ∧ labels_nodes c⇣2 (_ l - #:c⇣1 - 1 _) Skip)"
    by(cases n) (fastforce elim:labels.cases)+
  from disj show ?case
  proof
    assume "1 ≤ l ∧ labels_nodes c⇣1 (_ l - 1 _) Skip"
    hence "1 ≤ l" and "labels_nodes c⇣1 (_ l - 1 _) Skip" by simp_all
    from IH1[OF `labels_nodes c⇣1 (_ l - 1 _) Skip`] 
    have "c⇣1 \<turnstile> (_ l - 1 _) -\<Up>id-> (_Exit_)" .
    with `1 ≤ l` have "if (b) c⇣1 else c⇣2 \<turnstile> (_ l - 1 _) ⊕ 1 -\<Up>id-> (_Exit_) ⊕ 1"
      by(fastforce intro:WCFG_CondThen)
    with `n = (_ l _)` `1 ≤ l` show ?case by(simp add:id_def)
  next
    assume "#:c⇣1 + 1 ≤ l ∧ labels_nodes c⇣2 (_ l - #:c⇣1 - 1 _) Skip"
    hence "#:c⇣1 + 1 ≤ l" and "labels_nodes c⇣2 (_ l - #:c⇣1 - 1 _) Skip" by simp_all
    from IH2[OF `labels_nodes c⇣2 (_ l - #:c⇣1 - 1 _) Skip`]
    have "c⇣2 \<turnstile> (_ l - #:c⇣1 - 1 _) -\<Up>id-> (_Exit_)" .
    with `#:c⇣1 + 1 ≤ l` have "if (b) c⇣1 else c⇣2 \<turnstile> (_ l - #:c⇣1 - 1 _) ⊕ (#:c⇣1 + 1)
      -\<Up>id-> (_Exit_) ⊕ (#:c⇣1 + 1)"
      by(fastforce intro:WCFG_CondElse)
    with `n = (_ l _)` `#:c⇣1 + 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 \<turnstile> nx -\<Up>id-> (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = \<Up>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 = \<Up>id"
      by(rule_tac x="(Node nx,\<Up>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 \<turnstile> (_Entry_) -(λs. True)⇣\<surd>-> (_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 \<turnstile> nx -\<Up>id-> (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = \<Up>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 = \<Up>id"
      by(rule_tac x="(Node nx,\<Up>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 \<turnstile> nx -\<Up>id-> (_Exit_)"
      by(rule final_edge)
    then obtain a where "valid_edge prog a" and "sourcenode a = nx"
      and "kind a = \<Up>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 = \<Up>id"
      by(rule_tac x="(Node nx,\<Up>id,Node (_Exit_))" in exI)
        (auto intro!:lve_edge simp:knd_def valid_edge_def)
  qed
qed

end

end