Theory NonInterferenceInter

section ‹HRB Slicing guarantees IFC Noninterference›

theory NonInterferenceInter 
  imports "HRB-Slicing.FundamentalProperty"
begin

subsection ‹Assumptions of this Approach›

text ‹
Classical IFC noninterference, a special case of a noninterference
definition using partial equivalence relations (per)
cite"SabelfeldS:01", partitions the variables (i.e.\ locations) into
security levels. Usually, only levels for secret or high, written
H›, and public or low, written L›, variables are
used. Basically, a program that is noninterferent has to fulfil one
basic property: executing the program in two different initial states
that may differ in the values of their H›-variables yields two
final states that again only differ in the values of their 
H›-variables; thus the values of the H›-variables did not
influence those of the L›-variables.

Every per-based approach makes certain
assumptions: (i) all \mbox{H›-variables} are defined at the
beginning of the program, (ii) all L›-variables are observed (or
used in our terms) at the end and (iii) every variable is either
H› or L›. This security label is fixed for a variable
and can not be altered during a program run. Thus, we have to extend 
the prerequisites of the slicing framework in cite"Wasserrab:09" accordingly
in a new locale:

›

locale NonInterferenceInterGraph =
  SDG sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses 
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node  'pname"
  and get_return_edges :: "'edge  'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node  'var set" and Use :: "'node  'var set"
  and ParamDefs :: "'node  'var list" and ParamUses :: "'node  'var set list" +
  fixes H :: "'var set"
  fixes L :: "'var set"
  fixes High :: "'node"  ("'('_High'_')")
  fixes Low :: "'node"   ("'('_Low'_')")
  assumes Entry_edge_Exit_or_High:
  "valid_edge a; sourcenode a = (_Entry_) 
     targetnode a = (_Exit_)  targetnode a = (_High_)"
  and High_target_Entry_edge:
  "a. valid_edge a  sourcenode a = (_Entry_)  targetnode a = (_High_) 
       kind a = (λs. True)"
  and Entry_predecessor_of_High:
  "valid_edge a; targetnode a = (_High_)  sourcenode a = (_Entry_)"
  and Exit_edge_Entry_or_Low: "valid_edge a; targetnode a = (_Exit_) 
     sourcenode a = (_Entry_)  sourcenode a = (_Low_)"
  and Low_source_Exit_edge:
  "a. valid_edge a  sourcenode a = (_Low_)  targetnode a = (_Exit_)  
       kind a = (λs. True)"
  and Exit_successor_of_Low:
  "valid_edge a; sourcenode a = (_Low_)  targetnode a = (_Exit_)"
  and DefHigh: "Def (_High_) = H" 
  and UseHigh: "Use (_High_) = H"
  and UseLow: "Use (_Low_) = L"
  and HighLowDistinct: "H  L = {}"
  and HighLowUNIV: "H  L = UNIV"

begin

lemma Low_neq_Exit: assumes "L  {}" shows "(_Low_)  (_Exit_)"
proof
  assume "(_Low_) = (_Exit_)"
  have "Use (_Exit_) = {}" by fastforce
  with UseLow L  {} (_Low_) = (_Exit_) show False by simp
qed


lemma valid_node_High [simp]:"valid_node (_High_)"
  using High_target_Entry_edge by fastforce

lemma valid_node_Low [simp]:"valid_node (_Low_)"
  using Low_source_Exit_edge by fastforce


lemma get_proc_Low:
  "get_proc (_Low_) = Main"
proof -
  from Low_source_Exit_edge obtain a where "valid_edge a"
    and "sourcenode a = (_Low_)" and "targetnode a = (_Exit_)"
    and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
  from valid_edge a intra_kind (kind a)
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with sourcenode a = (_Low_) targetnode a = (_Exit_) get_proc_Exit
  show ?thesis by simp
qed

lemma get_proc_High:
  "get_proc (_High_) = Main"
proof -
  from High_target_Entry_edge obtain a where "valid_edge a"
    and "sourcenode a = (_Entry_)" and "targetnode a = (_High_)"
    and "intra_kind (kind a)" by(fastforce simp:intra_kind_def)
  from valid_edge a intra_kind (kind a)
  have "get_proc (sourcenode a) = get_proc (targetnode a)" by(rule get_proc_intra)
  with sourcenode a = (_Entry_) targetnode a = (_High_) get_proc_Entry
  show ?thesis by simp
qed



lemma Entry_path_High_path:
  assumes "(_Entry_) -as→* n" and "inner_node n"
  obtains a' as' where "as = a'#as'" and "(_High_) -as'→* n" 
  and "kind a' = (λs. True)"
proof(atomize_elim)
  from (_Entry_) -as→* n inner_node n
  show "a' as'. as = a'#as'  (_High_) -as'→* n  kind a' = (λs. True)"
  proof(induct n'"(_Entry_)" as n rule:path.induct)
    case (Cons_path n'' as n' a)
    from n'' -as→* n' inner_node n' have "n''  (_Exit_)" 
      by(fastforce simp:inner_node_def)
    with valid_edge a sourcenode a = (_Entry_) targetnode a = n''
    have "n'' = (_High_)" by -(drule Entry_edge_Exit_or_High,auto)
    from High_target_Entry_edge
    obtain a' where "valid_edge a'" and "sourcenode a' = (_Entry_)"
      and "targetnode a' = (_High_)" and "kind a' = (λs. True)"
      by blast
    with valid_edge a sourcenode a = (_Entry_) targetnode a = n''
      n'' = (_High_)
    have "a = a'" by(auto dest:edge_det)
    with n'' -as→* n' n'' = (_High_) kind a' = (λs. True) show ?case by blast
  qed fastforce
qed


lemma Exit_path_Low_path:
  assumes "n -as→* (_Exit_)" and "inner_node n"
  obtains a' as' where "as = as'@[a']" and "n -as'→* (_Low_)"
  and "kind a' = (λs. True)"
proof(atomize_elim)
  from n -as→* (_Exit_)
  show "as' a'. as = as'@[a']  n -as'→* (_Low_)  kind a' = (λs. True)"
  proof(induct as rule:rev_induct)
    case Nil
    with inner_node n show ?case by fastforce
  next
    case (snoc a' as')
    from n -as'@[a']→* (_Exit_)
    have "n -as'→* sourcenode a'" and "valid_edge a'" and "targetnode a' = (_Exit_)"
      by(auto elim:path_split_snoc)
    { assume "sourcenode a' = (_Entry_)"
      with n -as'→* sourcenode a' have "n = (_Entry_)"
        by(blast intro!:path_Entry_target)
      with inner_node n have False by(simp add:inner_node_def) }
    with valid_edge a' targetnode a' = (_Exit_) have "sourcenode a' = (_Low_)"
      by(blast dest!:Exit_edge_Entry_or_Low)
    from Low_source_Exit_edge
    obtain ax where "valid_edge ax" and "sourcenode ax = (_Low_)"
      and "targetnode ax = (_Exit_)" and "kind ax = (λs. True)"
      by blast
    with valid_edge a' targetnode a' = (_Exit_) sourcenode a' = (_Low_)
    have "a' = ax" by(fastforce intro:edge_det)
    with n -as'→* sourcenode a' sourcenode a' = (_Low_) kind ax = (λs. True)
    show ?case by blast
  qed
qed


lemma not_Low_High: "V  L  V  H"
  using HighLowUNIV
  by fastforce

lemma not_High_Low: "V  H  V  L"
  using HighLowUNIV
  by fastforce


subsection ‹Low Equivalence›

text ‹
In classical noninterference, an external observer can only see public values,
in our case the L›-variables. If two states agree in the values of all 
L›-variables, these states are indistinguishable for him. 
\emph{Low equivalence} groups those states in an equivalence class using 
the relation L:
›

definition lowEquivalence :: "('var  'val) list  ('var  'val) list  bool" 
(infixl "L" 50)
  where "s L s'  V  L. hd s V = hd s' V"

text ‹The following lemmas connect low equivalent states with
relevant variables as necessary in the correctness proof for slicing.›

lemma relevant_vars_Entry:
  assumes "V  rv S (CFG_node (_Entry_))" and "(_High_)  HRB_slice SCFG"
  shows "V  L"
proof -
  from V  rv S (CFG_node (_Entry_)) obtain as n' 
    where "(_Entry_) -asι* parent_node n'" 
    and "n'  HRB_slice S" and "V  UseSDG n'"
    and "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
           V  DefSDG n''" by(fastforce elim:rvE)
  from (_Entry_) -asι* parent_node n' have "valid_node (parent_node n')"
    by(fastforce intro:path_valid_node simp:intra_path_def)
  thus ?thesis
  proof(cases "parent_node n'" rule:valid_node_cases)
    case Entry
    with V  UseSDG n' have False
      by -(drule SDG_Use_parent_Use,simp add:Entry_empty)
    thus ?thesis by simp
  next
    case Exit
    with V  UseSDG n' have False
      by -(drule SDG_Use_parent_Use,simp add:Exit_empty)
    thus ?thesis by simp
  next
    case inner
    with (_Entry_) -asι* parent_node n' obtain a' as' where "as = a'#as'"
      and "(_High_) -as'ι* parent_node n'"
      by(fastforce elim:Entry_path_High_path simp:intra_path_def)
    from (_Entry_) -asι* parent_node n' as = a'#as'
    have "sourcenode a' = (_Entry_)" by(fastforce elim:path.cases simp:intra_path_def)
    show ?thesis
    proof(cases "as' = []")
      case True
      with (_High_) -as'ι* parent_node n' have "parent_node n' = (_High_)"
        by(fastforce simp:intra_path_def)
      with n'  HRB_slice S (_High_)  HRB_slice SCFG
      have False 
        by(fastforce dest:valid_SDG_node_in_slice_parent_node_in_slice 
                    simp:SDG_to_CFG_set_def)
      thus ?thesis by simp
    next
      case False
      with (_High_) -as'ι* parent_node n' have "hd (sourcenodes as') = (_High_)"
        by(fastforce intro:path_sourcenode simp:intra_path_def)
      from False have "hd (sourcenodes as')  set (sourcenodes as')"
        by(fastforce intro:hd_in_set simp:sourcenodes_def)
      with as = a'#as' have "hd (sourcenodes as')  set (sourcenodes as)"
        by(simp add:sourcenodes_def)
      from hd (sourcenodes as') = (_High_)
      have "valid_node (hd (sourcenodes as'))" by simp
      have "valid_SDG_node (CFG_node (_High_))" by simp
      with hd (sourcenodes as') = (_High_)
        hd (sourcenodes as')  set (sourcenodes as)
        n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
         V  DefSDG n''
      have "V  Def (_High_)"
        by(fastforce dest:CFG_Def_SDG_Def[OF valid_node (hd (sourcenodes as'))])
      hence "V  H" by(simp add:DefHigh)
      thus ?thesis by(rule not_High_Low)
    qed
  qed
qed



lemma lowEquivalence_relevant_nodes_Entry:
  assumes "s L s'" and "(_High_)  HRB_slice SCFG"
  shows "V  rv S (CFG_node (_Entry_)). hd s V = hd s' V"
proof
  fix V assume "V  rv S (CFG_node (_Entry_))"
  with (_High_)  HRB_slice SCFG have "V  L" by -(rule relevant_vars_Entry)
  with s L s' show "hd s V = hd s' V" by(simp add:lowEquivalence_def)
qed


subsection ‹The Correctness Proofs›

text ‹
In the following, we present two correctness proofs that slicing
guarantees IFC noninterference. In both theorems, CFG_node
(_High_) ∉ HRB_slice S›, where CFG_node (_Low_) ∈ S›, makes
sure that no high variable (which are all defined in (_High_)›)
can influence a low variable (which are all used in (_Low_)›).


First, a theorem regarding (_Entry_) -as→* (_Exit_)› paths in the 
control flow graph (CFG), which agree to a complete program execution:›


lemma slpa_rv_Low_Use_Low:
  assumes "CFG_node (_Low_)  S"
  shows "same_level_path_aux cs as; upd_cs cs as = []; same_level_path_aux cs as';
    c  set cs. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
   i < length cs. V  rv S (CFG_node (sourcenode (cs!i))). 
    fst (s!Suc i) V = fst (s'!Suc i) V; i < Suc (length cs). snd (s!i) = snd (s'!i);
   V  rv S (CFG_node m). state_val s V = state_val s' V;
   preds (slice_kinds S as) s; preds (slice_kinds S as') s';
   length s = Suc (length cs); length s' = Suc (length cs)
    V  Use (_Low_). state_val (transfers(slice_kinds S as) s) V =
                      state_val (transfers(slice_kinds S as') s') V"
proof(induct arbitrary:m as' s s' rule:slpa_induct)
  case (slpa_empty cs)
  from m -[]→* (_Low_) have "m = (_Low_)" by fastforce
  from m -[]→* (_Low_) have "valid_node m"
    by(rule path_valid_node)+
  { fix V assume "V  Use (_Low_)"
    moreover
    from valid_node m m = (_Low_) have "(_Low_) -[]ι* (_Low_)"
      by(fastforce intro:empty_path simp:intra_path_def)
    moreover
    from valid_node m m = (_Low_) CFG_node (_Low_)  S
    have "CFG_node (_Low_)  HRB_slice S"
      by(fastforce intro:HRB_slice_refl)
    ultimately have "V  rv S (CFG_node m)" 
      using m = (_Low_)
      by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
  hence "V  Use (_Low_). V  rv S (CFG_node m)" by simp
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    from m -as'→* (_Low_) m = (_Low_) have "as' = []"
    proof(induct m as' m'"(_Low_)" rule:path.induct)
      case (Cons_path m'' as a m)
      from valid_edge a sourcenode a = m m = (_Low_)
      have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
      with targetnode a = m'' m'' -as→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?case by simp
    qed simp
    with V  Use (_Low_). V  rv S (CFG_node m)
      V  rv S (CFG_node m). state_val s V = state_val s' V Nil
    show ?thesis by(auto simp:slice_kinds_def)
  qed
next
  case (slpa_intra cs a as)
  note IH = m as' s s'. upd_cs cs as = []; same_level_path_aux cs as'; 
    aset cs. valid_edge a; m -as→* (_Low_); m -as'→* (_Low_);
    i<length cs. Vrv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V; 
    i<Suc (length cs). snd (s ! i) = snd (s' ! i);
    Vrv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length cs); length s' = Suc (length cs)
     VUse (_Low_). state_val (transfers(slice_kinds S as) s) V =
    state_val (transfers(slice_kinds S as') s') V
  note rvs = i<length cs. Vrv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V
  from m -a # as→* (_Low_) have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with m -as'→* (_Low_) have "m = (_Low_)" by fastforce
      with valid_edge a sourcenode a = m have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from valid_edge a sourcenode a = m m = (_Low_) 
        targetnode a = (_Exit_) valid_edge a' sourcenode a' = (_Low_) 
        targetnode a' = (_Exit_)
      have "a = a'" by(fastforce dest:edge_det)
      with kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with targetnode a = (_Exit_) targetnode a -as→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with m -as'→* (_Low_) have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from preds (slice_kinds S (a # as)) s
      obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
      from preds (slice_kinds S as') s' as' = ax # asx 
      obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
        by(cases s')(auto simp:slice_kinds_def)
      have "intra_kind (kind ax)"
      proof(cases "kind ax" rule:edge_kind_cases)
        case (Call Q r p fs)
        have False
        proof(cases "sourcenode a  HRB_slice SCFG")
          case True
          with intra_kind (kind a) have "slice_kind S a = kind a"
            by -(rule slice_intra_kind_in_slice)
          from valid_edge ax kind ax = Q:r↪⇘pfs
          have unique:"∃!a'. valid_edge a'  sourcenode a' = sourcenode ax  
            intra_kind(kind a')" by(rule call_only_one_intra_edge)
          from valid_edge ax kind ax = Q:r↪⇘pfs obtain x 
            where "x  get_return_edges ax" by(fastforce dest:get_return_edge_call)
          with valid_edge ax obtain a' where "valid_edge a'" 
            and "sourcenode a' = sourcenode ax" and "kind a' = (λcf. False)"
            by(fastforce dest:call_return_node_edge)
          with valid_edge a sourcenode a = m sourcenode ax = m
            intra_kind (kind a) unique
          have "a' = a" by(fastforce simp:intra_kind_def)
          with kind a' = (λcf. False) slice_kind S a = kind a
            preds (slice_kinds S (a#as)) s
          have False by(cases s)(auto simp:slice_kinds_def)
          thus ?thesis by simp
        next
          case False
          with kind ax = Q:r↪⇘pfs sourcenode a = m sourcenode ax = m
          have "slice_kind S ax = (λcf. False):r↪⇘pfs"
            by(fastforce intro:slice_kind_Call)
          with as' = ax # asx preds (slice_kinds S as') s'
          have False by(cases s')(auto simp:slice_kinds_def)
          thus ?thesis by simp
        qed
        thus ?thesis by simp
      next
        case (Return Q p f)
        from valid_edge ax kind ax = Q↩⇘pf valid_edge a intra_kind (kind a)
          sourcenode a = m sourcenode ax = m
        have False by -(drule return_edges_only,auto simp:intra_kind_def)
        thus ?thesis by simp
      qed simp
      with same_level_path_aux cs as' as' = ax#asx
      have "same_level_path_aux cs asx" by(fastforce simp:intra_kind_def)
      show ?thesis
      proof(cases "targetnode a = targetnode ax")
        case True
        with valid_edge a valid_edge ax sourcenode a = m sourcenode ax = m
        have "a = ax" by(fastforce intro:edge_det)
        with valid_edge a intra_kind (kind a) sourcenode a = m
          Vrv S (CFG_node m). state_val s V = state_val s' V
          preds (slice_kinds S (a # as)) s
          preds (slice_kinds S as') s' as' = ax # asx
        have rv:"Vrv S (CFG_node (targetnode a)). 
          state_val (transfer (slice_kind S a) s) V =
          state_val (transfer (slice_kind S a) s') V"
          by -(rule rv_edge_slice_kinds,auto)
        from upd_cs cs (a # as) = [] intra_kind (kind a)
        have "upd_cs cs as = []" by(fastforce simp:intra_kind_def)
        from targetnode ax -asx→* (_Low_) a = ax
        have "targetnode a -asx→* (_Low_)" by simp
        from valid_edge a intra_kind (kind a)
        obtain cfx 
          where cfx:"transfer (slice_kind S a) s = cfx#cfs  snd cfx = snd cf"
          apply(cases cf)
          apply(cases "sourcenode a  HRB_slice SCFG") apply auto
          apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          apply(auto simp:intra_kind_def)
          apply(drule slice_kind_Upd) apply auto 
          by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
        from valid_edge a intra_kind (kind a)
        obtain cfx' 
          where cfx':"transfer (slice_kind S a) s' = cfx'#cfs'  snd cfx' = snd cf'"
          apply(cases cf')
          apply(cases "sourcenode a  HRB_slice SCFG") apply auto
          apply(fastforce dest:slice_intra_kind_in_slice simp:intra_kind_def)
          apply(auto simp:intra_kind_def)
          apply(drule slice_kind_Upd) apply auto 
          by(erule kind_Predicate_notin_slice_slice_kind_Predicate) auto
        with cfx i < Suc (length cs). snd (s!i) = snd (s'!i)
        have snds:"i<Suc(length cs).
          snd (transfer (slice_kind S a) s ! i) = 
          snd (transfer (slice_kind S a) s' ! i)" 
          by auto(case_tac i,auto)
        from rvs cfx cfx' have rvs':"i<length cs.
          Vrv S (CFG_node (sourcenode (cs ! i))).
          fst (transfer (slice_kind S a) s ! Suc i) V =
          fst (transfer (slice_kind S a) s' ! Suc i) V"
          by fastforce
        from preds (slice_kinds S (a # as)) s
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
        moreover
        from preds (slice_kinds S as') s' as' = ax # asx a = ax
        have "preds (slice_kinds S asx) (transfer (slice_kind S a) s')" 
          by(simp add:slice_kinds_def)
        moreover
        from valid_edge a intra_kind (kind a)
        have "length (transfer (slice_kind S a) s) = length s"
          by(cases "sourcenode a  HRB_slice SCFG")
        (auto dest:slice_intra_kind_in_slice slice_kind_Upd
          elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
        with length s = Suc (length cs)
        have "length (transfer (slice_kind S a) s) = Suc (length cs)"
          by simp
        moreover
        from a = ax valid_edge a intra_kind (kind a)
        have "length (transfer (slice_kind S a) s') = length s'"
          by(cases "sourcenode ax  HRB_slice SCFG")
        (auto dest:slice_intra_kind_in_slice slice_kind_Upd
          elim:kind_Predicate_notin_slice_slice_kind_Predicate simp:intra_kind_def)
        with length s' = Suc (length cs)
        have "length (transfer (slice_kind S a) s') = Suc (length cs)"
          by simp
        moreover
        from IH[OF upd_cs cs as = [] same_level_path_aux cs asx 
          cset cs. valid_edge c targetnode a -as→* (_Low_) 
          targetnode a -asx→* (_Low_) rvs' snds rv calculation]
          as' = ax # asx a = ax
        show ?thesis by(simp add:slice_kinds_def)
      next
        case False
        from i < Suc(length cs). snd (s!i) = snd (s'!i)
        have "snd (hd s) = snd (hd s')" by(erule_tac x="0" in allE) fastforce
        with valid_edge a valid_edge ax sourcenode a = m
          sourcenode ax = m as' = ax # asx False
          intra_kind (kind a) intra_kind (kind ax)
          preds (slice_kinds S (a # as)) s
          preds (slice_kinds S as') s'
          Vrv S (CFG_node m). state_val s V = state_val s' V
          length s = Suc (length cs) length s' = Suc (length cs)
        have False by(fastforce intro!:rv_branching_edges_slice_kinds_False[of a ax])
        thus ?thesis by simp
      qed
    qed
  qed
next
  case (slpa_Call cs a as Q r p fs)
  note IH = m as' s s'. 
    upd_cs (a # cs) as = []; same_level_path_aux (a # cs) as';
    cset (a # cs). valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
    i<length (a # cs). Vrv S (CFG_node (sourcenode ((a # cs) ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V;
    i<Suc (length (a # cs)). snd (s ! i) = snd (s' ! i);
    Vrv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length (a # cs)); length s' = Suc (length (a # cs))
     VUse (_Low_). state_val (transfers(slice_kinds S as) s) V =
    state_val (transfers(slice_kinds S as') s') V
  note rvs = i<length cs. Vrv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V
  from m -a # as→* (_Low_) have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  from cset cs. valid_edge c valid_edge a
  have "cset (a # cs). valid_edge c" by simp
  show ?case
   proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with m -as'→* (_Low_) have "m = (_Low_)" by fastforce
      with valid_edge a sourcenode a = m have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from valid_edge a sourcenode a = m m = (_Low_) 
        targetnode a = (_Exit_) valid_edge a' sourcenode a' = (_Low_) 
        targetnode a' = (_Exit_)
      have "a = a'" by(fastforce dest:edge_det)
      with kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with targetnode a = (_Exit_) targetnode a -as→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with m -as'→* (_Low_) have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from preds (slice_kinds S (a # as)) s
      obtain cf cfs where [simp]:"s = cf#cfs" by(cases s)(auto simp:slice_kinds_def)
      from preds (slice_kinds S as') s' as' = ax # asx 
      obtain cf' cfs' where [simp]:"s' = cf'#cfs'"
        by(cases s')(auto simp:slice_kinds_def)
      have "Q r p fs. kind ax = Q:r↪⇘pfs"
      proof(cases "kind ax" rule:edge_kind_cases)
        case Intra
        have False
        proof(cases "sourcenode ax  HRB_slice SCFG")
          case True
          with intra_kind (kind ax) 
          have "slice_kind S ax = kind ax"
            by -(rule slice_intra_kind_in_slice)
          from valid_edge a kind a = Q:r↪⇘pfs
          have unique:"∃!a'. valid_edge a'  sourcenode a' = sourcenode a  
            intra_kind(kind a')" by(rule call_only_one_intra_edge)
          from valid_edge a kind a = Q:r↪⇘pfs obtain x 
            where "x  get_return_edges a" by(fastforce dest:get_return_edge_call)
          with valid_edge a obtain a' where "valid_edge a'" 
            and "sourcenode a' = sourcenode a" and "kind a' = (λcf. False)"
            by(fastforce dest:call_return_node_edge)
          with valid_edge ax sourcenode ax = m sourcenode a = m
            intra_kind (kind ax) unique
          have "a' = ax" by(fastforce simp:intra_kind_def)
          with kind a' = (λcf. False) 
            slice_kind S ax = kind ax as' = ax # asx
            preds (slice_kinds S as') s'
          have False by(simp add:slice_kinds_def)
          thus ?thesis by simp
        next
          case False
          with kind a = Q:r↪⇘pfs sourcenode ax = m sourcenode a = m
          have "slice_kind S a = (λcf. False):r↪⇘pfs"
            by(fastforce intro:slice_kind_Call)
          with preds (slice_kinds S (a # as)) s
          have False by(simp add:slice_kinds_def)
          thus ?thesis by simp
        qed
        thus ?thesis by simp
      next
        case (Return Q' p' f')
        from valid_edge ax kind ax = Q'↩⇘p'f' valid_edge a kind a = Q:r↪⇘pfs
          sourcenode a = m sourcenode ax = m
        have False by -(drule return_edges_only,auto)
        thus ?thesis by simp
      qed simp
      have "sourcenode a  HRB_slice SCFG"
      proof(rule ccontr)
        assume "sourcenode a  HRB_slice SCFG"
        from this kind a = Q:r↪⇘pfs
        have "slice_kind S a = (λcf. False):r↪⇘pfs"
          by(rule slice_kind_Call)
        with preds (slice_kinds S (a # as)) s
        show False by(simp add:slice_kinds_def)
      qed
      with preds (slice_kinds S (a # as)) s kind a = Q:r↪⇘pfs
      have "pred (kind a) s" 
        by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
      from sourcenode a  HRB_slice SCFG
        sourcenode a = m sourcenode ax = m
      have "sourcenode ax  HRB_slice SCFG" by simp
      with as' = ax # asx preds (slice_kinds S as') s' 
        Q r p fs. kind ax = Q:r↪⇘pfs
      have "pred (kind ax) s'"
        by(fastforce dest:slice_kind_Call_in_slice simp:slice_kinds_def)
      { fix V assume "V  Use (sourcenode a)"
        from valid_edge a have "sourcenode a -[]ι* sourcenode a"
          by(fastforce intro:empty_path simp:intra_path_def)
        with sourcenode a  HRB_slice SCFG
          valid_edge a V  Use (sourcenode a)
        have "V  rv S (CFG_node (sourcenode a))"
          by(auto intro!:rvI CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def) }
      with Vrv S (CFG_node m). state_val s V = state_val s' V
        sourcenode a = m
      have Use:"V  Use (sourcenode a). state_val s V = state_val s' V" by simp
      from i<Suc (length cs). snd (s ! i) = snd (s' ! i)
      have "snd (hd s) = snd (hd s')"  by fastforce
      with valid_edge a kind a = Q:r↪⇘pfs valid_edge ax
        Q r p fs. kind ax = Q:r↪⇘pfs sourcenode a = m sourcenode ax = m
        pred (kind a) s pred (kind ax) s' Use length s = Suc (length cs)
        length s' = Suc (length cs)
      have [simp]:"ax = a" by(fastforce intro!:CFG_equal_Use_equal_call)
      from same_level_path_aux cs as' as' = ax#asx kind a = Q:r↪⇘pfs
        Q r p fs. kind ax = Q:r↪⇘pfs
      have "same_level_path_aux (a # cs) asx" by simp
      from targetnode ax -asx→* (_Low_) have "targetnode a -asx→* (_Low_)" by simp
      from kind a = Q:r↪⇘pfs upd_cs cs (a # as) = [] 
      have "upd_cs (a # cs) as = []" by simp
      from sourcenode a  HRB_slice SCFG kind a = Q:r↪⇘pfs
      have slice_kind:"slice_kind S a = 
        Q:r↪⇘p(cspp (targetnode a) (HRB_slice S) fs)"
        by(rule slice_kind_Call_in_slice)
      from i<Suc (length cs). snd (s ! i) = snd (s' ! i) slice_kind
      have snds:"i<Suc (length (a # cs)).
        snd (transfer (slice_kind S a) s ! i) =
        snd (transfer (slice_kind S a) s' ! i)"
        by auto(case_tac i,auto)
      from valid_edge a kind a = Q:r↪⇘pfs obtain ins outs 
        where "(p,ins,outs)  set procs" by(fastforce dest!:callee_in_procs)
      with valid_edge a kind a = Q:r↪⇘pfs
      have "length (ParamUses (sourcenode a)) = length ins"
        by(fastforce intro:ParamUses_call_source_length)
      with valid_edge a
      have "i < length ins. V  (ParamUses (sourcenode a))!i. V  Use (sourcenode a)"
        by(fastforce intro:ParamUses_in_Use)
      with V  Use (sourcenode a). state_val s V = state_val s' V
      have "i < length ins. V  (ParamUses (sourcenode a))!i. 
        state_val s V = state_val s' V"
        by fastforce
      with valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
        pred (kind a) s pred (kind ax) s'
      have "i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i"
        by(fastforce intro!:CFG_call_edge_params)
      from valid_edge a kind a = Q:r↪⇘pfs (p,ins,outs)  set procs
      have "length fs = length ins" by(rule CFG_call_edge_length)
      { fix i assume "i < length fs"
        with length fs = length ins have "i < length ins" by simp
        from i < length fs have "(params fs (fst cf))!i = (fs!i) (fst cf)"
          by(rule params_nth)
        moreover
        from i < length fs have "(params fs (fst cf'))!i = (fs!i) (fst cf')"
          by(rule params_nth)
        ultimately have "(fs!i) (fst (hd s)) = (fs!i) (fst (hd s'))"
          using i < length ins
            i < length ins. (params fs (fst (hd s)))!i = (params fs (fst (hd s')))!i
          by simp }
      hence "i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
      { fix i assume "i < length fs"
        with i < length fs. (fs ! i) (fst cf) = (fs ! i) (fst cf')
        have "(fs ! i) (fst cf) = (fs ! i) (fst cf')" by simp
        have "((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf) =
          ((csppa (targetnode a) (HRB_slice S) 0 fs)!i)(fst cf')"
        proof(cases "Formal_in(targetnode a,i + 0)   HRB_slice S")
          case True
          with i < length fs 
          have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = fs!i"
            by(rule csppa_Formal_in_in_slice)
          with (fs ! i) (fst cf) = (fs ! i) (fst cf') show ?thesis by simp
        next
          case False
          with i < length fs 
          have "(csppa (targetnode a) (HRB_slice S) 0 fs)!i = Map.empty"
            by(rule csppa_Formal_in_notin_slice)
          thus ?thesis by simp
        qed }
      hence eq:"i < length fs.
        ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf) =
        ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
        by(simp add:cspp_def)
      { fix i assume "i < length fs"
        hence "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf))!i =
          ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf)"
          by(fastforce intro:params_nth)
        moreover
        from i < length fs
        have "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf'))!i =
          ((cspp (targetnode a) (HRB_slice S) fs)!i)(fst cf')"
          by(fastforce intro:params_nth)
        ultimately 
        have "(params (cspp (targetnode a) (HRB_slice S) fs)
          (fst cf))!i =
          (params (cspp (targetnode a) (HRB_slice S) fs)(fst cf'))!i"
          using eq i < length fs by simp }
      hence "params (cspp (targetnode a) (HRB_slice S) fs)(fst cf) =
        params (cspp (targetnode a) (HRB_slice S) fs)(fst cf')"
        by(simp add:list_eq_iff_nth_eq)
      with slice_kind (p,ins,outs)  set procs
      obtain cfx where [simp]:
        "transfer (slice_kind S a) (cf#cfs) = cfx#cf#cfs"
        "transfer (slice_kind S a) (cf'#cfs') = cfx#cf'#cfs'"
        by auto
      hence rv:"Vrv S (CFG_node (targetnode a)).
        state_val (transfer (slice_kind S a) s) V = 
        state_val (transfer (slice_kind S a) s') V" by simp
      from rvs Vrv S (CFG_node m). state_val s V = state_val s' V 
        sourcenode a = m
      have rvs':"i<length (a # cs). 
        Vrv S (CFG_node (sourcenode ((a # cs) ! i))).
        fst ((transfer (slice_kind S a) s) ! Suc i) V = 
        fst ((transfer (slice_kind S a) s') ! Suc i) V"
        by auto(case_tac i,auto)
      from preds (slice_kinds S (a # as)) s
      have "preds (slice_kinds S as)
        (transfer (slice_kind S a) s)" by(simp add:slice_kinds_def)
      moreover
      from preds (slice_kinds S as') s' as' = ax#asx
      have "preds (slice_kinds S asx)
        (transfer (slice_kind S a) s')" by(simp add:slice_kinds_def)
      moreover
      from length s = Suc (length cs)
      have "length (transfer (slice_kind S a) s) = 
        Suc (length (a # cs))" by simp
      moreover
      from length s' = Suc (length cs)
      have "length (transfer (slice_kind S a) s') = 
        Suc (length (a # cs))" by simp
      moreover
      from IH[OF upd_cs (a # cs) as = [] same_level_path_aux (a # cs) asx
        cset (a # cs). valid_edge c targetnode a -as→* (_Low_)
        targetnode a -asx→* (_Low_) rvs' snds rv calculation] as' = ax#asx
      show ?thesis by(simp add:slice_kinds_def)
    qed
  qed
next
  case (slpa_Return cs a as Q p f c' cs')
  note IH = m as' s s'. upd_cs cs' as = []; same_level_path_aux cs' as'; 
    cset cs'. valid_edge c; m -as→* (_Low_); m -as'→* (_Low_);
    i<length cs'. Vrv S (CFG_node (sourcenode (cs' ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V; 
    i<Suc (length cs'). snd (s ! i) = snd (s' ! i);
    Vrv S (CFG_node m). state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s';
    length s = Suc (length cs'); length s' = Suc (length cs')
     VUse (_Low_). state_val (transfers(slice_kinds S as) s) V =
                       state_val (transfers(slice_kinds S as') s') V
  note rvs = i<length cs. Vrv S (CFG_node (sourcenode (cs ! i))).
    fst (s ! Suc i) V = fst (s' ! Suc i) V
  from m -a # as→* (_Low_) have "sourcenode a = m" and "valid_edge a"
    and "targetnode a -as→* (_Low_)" by(auto elim:path_split_Cons)
  from cset cs. valid_edge c cs = c' # cs'
  have "valid_edge c'" and "cset cs'. valid_edge c" by simp_all
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with m -as'→* (_Low_) have "m = (_Low_)" by fastforce
      with valid_edge a sourcenode a = m have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from valid_edge a sourcenode a = m m = (_Low_) 
        targetnode a = (_Exit_) valid_edge a' sourcenode a' = (_Low_) 
        targetnode a' = (_Exit_)
      have "a = a'" by(fastforce dest:edge_det)
      with kind a' = (λs. True) have "kind a = (λs. True)" by simp
      with targetnode a = (_Exit_) targetnode a -as→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with m -as'→* (_Low_) have "sourcenode ax = m" and "valid_edge ax"
        and "targetnode ax -asx→* (_Low_)" by(auto elim:path_split_Cons)
      from valid_edge a valid_edge ax kind a = Q↩⇘pf
        sourcenode a = m sourcenode ax = m
      have "Q f. kind ax = Q↩⇘pf" by(auto dest:return_edges_only)
      with same_level_path_aux cs as' as' = ax#asx cs = c' # cs'
      have "ax  get_return_edges c'" and "same_level_path_aux cs' asx" by auto
      from valid_edge c' ax  get_return_edges c' a  get_return_edges c'
      have [simp]:"ax = a" by(rule get_return_edges_unique)
      from targetnode ax -asx→* (_Low_) have "targetnode a -asx→* (_Low_)" by simp
      from upd_cs cs (a # as) = [] kind a = Q↩⇘pf cs = c' # cs'
        a  get_return_edges c'
      have "upd_cs cs' as = []" by simp
      from length s = Suc (length cs) cs = c' # cs'
      obtain cf cfx cfs where "s = cf#cfx#cfs"
        by(cases s,auto,case_tac list,fastforce+)
      from length s' = Suc (length cs) cs = c' # cs'
      obtain cf' cfx' cfs' where "s' = cf'#cfx'#cfs'"
        by(cases s',auto,case_tac list,fastforce+)
      from rvs cs = c' # cs' s = cf#cfx#cfs s' = cf'#cfx'#cfs'
      have rvs1:"i<length cs'. 
        Vrv S (CFG_node (sourcenode (cs' ! i))).
        fst ((cfx#cfs) ! Suc i) V = fst ((cfx'#cfs') ! Suc i) V"
        and "Vrv S (CFG_node (sourcenode c')). 
        (fst cfx) V = (fst cfx') V"
        by auto
      from valid_edge c' a  get_return_edges c'
      obtain Qx rx px fsx where "kind c' = Qx:rx↪⇘pxfsx"
        by(fastforce dest!:only_call_get_return_edges)
      have "V  rv S (CFG_node (targetnode a)).
        V  rv S (CFG_node (sourcenode c'))"
      proof
        fix V assume "V  rv S (CFG_node (targetnode a))"
        from valid_edge c' a  get_return_edges c'
        obtain a' where edge:"valid_edge a'" "sourcenode a' = sourcenode c'"
          "targetnode a' = targetnode a" "intra_kind (kind a')"
          by -(drule call_return_node_edge,auto simp:intra_kind_def)
        from V  rv S (CFG_node (targetnode a))
        obtain as n' where "targetnode a -asι* parent_node n'"
          and "n'  HRB_slice S" and "V  UseSDG n'"
          and all:"n''. valid_SDG_node n''  parent_node n''  set (sourcenodes as) 
           V  DefSDG n''" by(fastforce elim:rvE)
        from targetnode a -asι* parent_node n' edge
        have "sourcenode c' -a'#asι* parent_node n'"
          by(fastforce intro:Cons_path simp:intra_path_def)
        from valid_edge c' kind c' = Qx:rx↪⇘pxfsx have "Def (sourcenode c') = {}"
          by(rule call_source_Def_empty)
        hence "n''. valid_SDG_node n''  parent_node n'' = sourcenode c'
           V  DefSDG n''" by(fastforce dest:SDG_Def_parent_Def)
        with all sourcenode a' = sourcenode c'
        have "n''. valid_SDG_node n''  parent_node n''  set (sourcenodes (a'#as)) 
           V  DefSDG n''" by(fastforce simp:sourcenodes_def)
        with sourcenode c' -a'#asι* parent_node n' 
          n'  HRB_slice S V  UseSDG n'
        show "V  rv S (CFG_node (sourcenode c'))"
          by(fastforce intro:rvI)
      qed
      show ?thesis
      proof(cases "sourcenode a  HRB_slice SCFG")
        case True
        from valid_edge c' a  get_return_edges c'
        have "get_proc (targetnode c') = get_proc (sourcenode a)"
          by -(drule intra_proc_additional_edge,
            auto dest:get_proc_intra simp:intra_kind_def)
        moreover
        from valid_edge c' kind c' = Qx:rx↪⇘pxfsx
        have "get_proc (targetnode c') = px" by(rule get_proc_call)
        moreover
        from valid_edge a kind a = Q↩⇘pf
        have "get_proc (sourcenode a) = p" by(rule get_proc_return)
        ultimately have [simp]:"px = p" by simp
        from valid_edge c' kind c' = Qx:rx↪⇘pxfsx
        obtain ins outs where "(p,ins,outs)  set procs"
          by(fastforce dest!:callee_in_procs)
        with sourcenode a  HRB_slice SCFG
          valid_edge a kind a = Q↩⇘pf
        have slice_kind:"slice_kind S a = 
          Q↩⇘p(λcf cf'. rspp (targetnode a) (HRB_slice S) outs cf' cf)"
          by(rule slice_kind_Return_in_slice)
        with s = cf#cfx#cfs s' = cf'#cfx'#cfs'
        have sx:"transfer (slice_kind S a) s = 
          (rspp (targetnode a) (HRB_slice S) outs (fst cfx) (fst cf),
          snd cfx)#cfs"
          and sx':"transfer (slice_kind S a) s' = 
          (rspp (targetnode a) (HRB_slice S) outs (fst cfx') (fst cf'),
          snd cfx')#cfs'"
          by simp_all
        with rvs1 have rvs':"i<length cs'. 
          Vrv S (CFG_node (sourcenode (cs' ! i))).
          fst ((transfer (slice_kind S a) s) ! Suc i) V = 
          fst ((transfer (slice_kind S a) s') ! Suc i) V"
          by fastforce
        from slice_kind i<Suc (length cs). snd (s ! i) = snd (s' ! i) cs = c' # cs'
          s = cf#cfx#cfs s' = cf'#cfx'#cfs'
        have snds:"i<Suc (length cs').
          snd (transfer (slice_kind S a) s ! i) =
          snd (transfer (slice_kind S a) s' ! i)"
          apply auto apply(case_tac i) apply auto
          by(erule_tac x="Suc (Suc nat)" in allE) auto
        have "Vrv S (CFG_node (targetnode a)).
          (rspp (targetnode a) (HRB_slice S) outs 
          (fst cfx) (fst cf)) V =
          (rspp (targetnode a) (HRB_slice S) outs 
          (fst cfx') (fst cf')) V"
        proof
          fix V assume "V  rv S (CFG_node (targetnode a))"
          show "(rspp (targetnode a) (HRB_slice S) outs 
            (fst cfx) (fst cf)) V =
            (rspp (targetnode a) (HRB_slice S) outs 
            (fst cfx') (fst cf')) V"
          proof(cases "V  set (ParamDefs (targetnode a))")
            case True
            then obtain i where "i < length (ParamDefs (targetnode a))"
              and "(ParamDefs (targetnode a))!i = V"
              by(fastforce simp:in_set_conv_nth)
            from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs
            have "length(ParamDefs (targetnode a)) = length outs"
              by(fastforce intro:ParamDefs_return_target_length)
            show ?thesis
            proof(cases "Actual_out(targetnode a,i)  HRB_slice S")
              case True
              with i < length (ParamDefs (targetnode a)) valid_edge a
                length(ParamDefs (targetnode a)) = length outs
                (ParamDefs (targetnode a))!i = V[THEN sym]
              have rspp_eq:"(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx) (fst cf)) V = 
                (fst cf)(outs!i)"
                "(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx') (fst cf')) V = 
                (fst cf')(outs!i)"
                by(auto intro:rspp_Actual_out_in_slice)
              from valid_edge a kind a = Q↩⇘pf (p,ins,outs)  set procs
              have "V  set outs. V  Use (sourcenode a)" by(fastforce dest:outs_in_Use)
              have "V  Use (sourcenode a). V  rv S (CFG_node m)"
              proof
                fix V assume "V  Use (sourcenode a)"
                from valid_edge a sourcenode a = m
                have "parent_node (CFG_node m) -[]ι* parent_node (CFG_node m)"
                  by(fastforce intro:empty_path simp:intra_path_def)
                with sourcenode a  HRB_slice SCFG 
                  V  Use (sourcenode a) sourcenode a = m valid_edge a
                show "V  rv S (CFG_node m)"
                  by -(rule rvI,
                    auto intro!:CFG_Use_SDG_Use simp:SDG_to_CFG_set_def sourcenodes_def)
              qed
              with V  set outs. V  Use (sourcenode a)
              have "V  set outs. V  rv S (CFG_node m)" by simp
              with Vrv S (CFG_node m). state_val s V = state_val s' V
                s = cf#cfx#cfs s' = cf'#cfx'#cfs'
              have "V  set outs. (fst cf) V = (fst cf') V" by simp
              with i < length (ParamDefs (targetnode a))
                length(ParamDefs (targetnode a)) = length outs
              have "(fst cf)(outs!i) = (fst cf')(outs!i)" by fastforce
              with rspp_eq show ?thesis by simp
            next
              case False
              with i < length (ParamDefs (targetnode a)) valid_edge a
                length(ParamDefs (targetnode a)) = length outs
                (ParamDefs (targetnode a))!i = V[THEN sym]
              have rspp_eq:"(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx) (fst cf)) V = 
                (fst cfx)((ParamDefs (targetnode a))!i)"
                "(rspp (targetnode a) 
                (HRB_slice S) outs (fst cfx') (fst cf')) V = 
                (fst cfx')((ParamDefs (targetnode a))!i)"
                by(auto intro:rspp_Actual_out_notin_slice)
              from Vrv S (CFG_node (sourcenode c')). 
                (fst cfx) V = (fst cfx') V
                V  rv S (CFG_node (targetnode a))
                V  rv S (CFG_node (targetnode a)).
                V  rv S (CFG_node (sourcenode c'))
                (ParamDefs (targetnode a))!i = V[THEN sym]
              have "(fst cfx) (ParamDefs (targetnode a) ! i) =
                (fst cfx') (ParamDefs (targetnode a) ! i)" by fastforce
              with rspp_eq show ?thesis by fastforce
            qed
          next
            case False
            with Vrv S (CFG_node (sourcenode c')). 
              (fst cfx) V = (fst cfx') V
              V  rv S (CFG_node (targetnode a))
              V  rv S (CFG_node (targetnode a)).
              V  rv S (CFG_node (sourcenode c'))
            show ?thesis by(fastforce simp:rspp_def map_merge_def)
          qed
        qed
        with sx sx'
        have rv':"Vrv S (CFG_node (targetnode a)).
          state_val (transfer (slice_kind S a) s) V =
          state_val (transfer (slice_kind S a) s') V"
          by fastforce
        from preds (slice_kinds S (a # as)) s
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)"
          by(simp add:slice_kinds_def)
        moreover
        from preds (slice_kinds S as') s' as' = ax#asx
        have "preds (slice_kinds S asx) 
          (transfer (slice_kind S a) s')"
          by(simp add:slice_kinds_def)
        moreover
        from length s = Suc (length cs) cs = c' # cs' sx
        have "length (transfer (slice_kind S a) s) = Suc (length cs')"
          by(simp,simp add:s = cf#cfx#cfs)
        moreover
        from length s' = Suc (length cs) cs = c' # cs' sx'
        have "length (transfer (slice_kind S a) s') = Suc (length cs')"
          by(simp,simp add:s' = cf'#cfx'#cfs')
        moreover
        from IH[OF upd_cs cs' as = [] same_level_path_aux cs' asx 
          cset cs'. valid_edge c targetnode a -as→* (_Low_) 
          targetnode a -asx→* (_Low_) rvs' snds rv' calculation] as' = ax#asx
        show ?thesis by(simp add:slice_kinds_def)
      next
        case False
        from this kind a = Q↩⇘pf
        have slice_kind:"slice_kind S a = (λcf. True)↩⇘p(λcf cf'. cf')"
          by(rule slice_kind_Return)
        with s = cf#cfx#cfs s' = cf'#cfx'#cfs'
        have [simp]:"transfer (slice_kind S a) s = cfx#cfs"
          "transfer (slice_kind S a) s' = cfx'#cfs'" by simp_all
        from slice_kind i<Suc (length cs). snd (s ! i) = snd (s' ! i) 
          cs = c' # cs' s = cf#cfx#cfs s' = cf'#cfx'#cfs'
        have snds:"i<Suc (length cs').
          snd (transfer (slice_kind S a) s ! i) =
          snd (transfer (slice_kind S a) s' ! i)" by fastforce
        from rvs1 have rvs':"i<length cs'. 
          Vrv S (CFG_node (sourcenode (cs' ! i))).
          fst ((transfer (slice_kind S a) s) ! Suc i) V = 
          fst ((transfer (slice_kind S a) s') ! Suc i) V"
          by fastforce
        from V  rv S (CFG_node (targetnode a)).
          V  rv S (CFG_node (sourcenode c'))
          Vrv S (CFG_node (sourcenode c')). 
          (fst cfx) V = (fst cfx') V
        have rv':"Vrv S (CFG_node (targetnode a)).
          state_val (transfer (slice_kind S a) s) V =
          state_val (transfer (slice_kind S a) s') V" by simp
        from preds (slice_kinds S (a # as)) s
        have "preds (slice_kinds S as) 
          (transfer (slice_kind S a) s)"
          by(simp add:slice_kinds_def)
        moreover
        from preds (slice_kinds S as') s' as' = ax#asx
        have "preds (slice_kinds S asx) 
          (transfer (slice_kind S a) s')"
          by(simp add:slice_kinds_def)
        moreover
        from length s = Suc (length cs) cs = c' # cs'
        have "length (transfer (slice_kind S a) s) = Suc (length cs')"
          by(simp,simp add:s = cf#cfx#cfs)
        moreover
        from length s' = Suc (length cs) cs = c' # cs'
        have "length (transfer (slice_kind S a) s') = Suc (length cs')"
          by(simp,simp add:s' = cf'#cfx'#cfs')
        moreover
        from IH[OF upd_cs cs' as = [] same_level_path_aux cs' asx 
          cset cs'. valid_edge c targetnode a -as→* (_Low_) 
          targetnode a -asx→* (_Low_) rvs' snds rv' calculation] as' = ax#asx
        show ?thesis by(simp add:slice_kinds_def)
      qed
    qed
  qed
qed


lemma rv_Low_Use_Low:
  assumes "m -as* (_Low_)" and "m -as'* (_Low_)" and "get_proc m = Main"
  and "V  rv S (CFG_node m). cf V = cf' V"
  and "preds (slice_kinds S as) [(cf,undefined)]"
  and "preds (slice_kinds S as') [(cf',undefined)]"
  and "CFG_node (_Low_)  S"
  shows "V  Use (_Low_). 
    state_val (transfers(slice_kinds S as) [(cf,undefined)]) V =
    state_val (transfers(slice_kinds S as') [(cf',undefined)]) V"
proof(cases as)
  case Nil
  with m -as* (_Low_) have "valid_node m" and "m = (_Low_)" 
    by(auto intro:path_valid_node simp:vp_def)
  { fix V assume "V  Use (_Low_)"
    moreover
    from valid_node m m = (_Low_) have "(_Low_) -[]ι* (_Low_)"
      by(fastforce intro:empty_path simp:intra_path_def)
    moreover
    from valid_node m m = (_Low_) CFG_node (_Low_)  S
    have "CFG_node (_Low_)  HRB_slice S"
      by(fastforce intro:HRB_slice_refl)
    ultimately have "V  rv S (CFG_node m)" using m = (_Low_)
      by(auto intro!:rvI CFG_Use_SDG_Use simp:sourcenodes_def) }
  hence "V  Use (_Low_). V  rv S (CFG_node m)" by simp
  show ?thesis
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    from m -as'* (_Low_) have "m -as'→* (_Low_)" by(simp add:vp_def)
    from m -as'→* (_Low_) m = (_Low_) have "as' = []"
    proof(induct m as' m'"(_Low_)" rule:path.induct)
      case (Cons_path m'' as a m)
      from valid_edge a sourcenode a = m m = (_Low_)
      have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
      with targetnode a = m'' m'' -as→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?case by simp
    qed simp
    with Nil V  rv S (CFG_node m). cf V = cf' V
      V  Use (_Low_). V  rv S (CFG_node m)
    show ?thesis by(fastforce simp:slice_kinds_def)
  qed
next
  case (Cons ax asx)
  with m -as* (_Low_) have "sourcenode ax = m" and "valid_edge ax"
    and "targetnode ax -asx→* (_Low_)"
    by(auto elim:path_split_Cons simp:vp_def)
  show ?thesis
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with m -as'* (_Low_) have "m = (_Low_)" by(fastforce simp:vp_def)
      with valid_edge ax sourcenode ax = m have "targetnode ax = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain a' where "valid_edge a'"
        and "sourcenode a' = (_Low_)" and "targetnode a' = (_Exit_)"
        and "kind a' = (λs. True)" by blast
      from valid_edge ax sourcenode ax = m m = (_Low_) 
        targetnode ax = (_Exit_) valid_edge a' sourcenode a' = (_Low_) 
        targetnode a' = (_Exit_)
      have "ax = a'" by(fastforce dest:edge_det)
      with kind a' = (λs. True) have "kind ax = (λs. True)" by simp
      with targetnode ax = (_Exit_) targetnode ax -asx→* (_Low_)
      have "(_Low_) = (_Exit_)" by -(drule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax' asx')
      from m -as* (_Low_) have "valid_path_aux [] as" and "m -as→* (_Low_)"
        by(simp_all add:vp_def valid_path_def)
      from this as = ax#asx get_proc m = Main
      have "same_level_path_aux [] as  upd_cs [] as = []"
        by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
        (fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
      hence "same_level_path_aux [] as" and "upd_cs [] as = []" by simp_all
      from m -as'* (_Low_) have "valid_path_aux [] as'" and "m -as'→* (_Low_)"
        by(simp_all add:vp_def valid_path_def)
      from this as' = ax'#asx' get_proc m = Main
      have "same_level_path_aux [] as'  upd_cs [] as' = []"
        by -(rule vpa_Main_slpa[of _ _ m "(_Low_)"],
        (fastforce intro!:get_proc_Low simp:valid_call_list_def)+)
      hence "same_level_path_aux [] as'" by simp
      from same_level_path_aux [] as upd_cs [] as = []
        same_level_path_aux [] as' m -as→* (_Low_) m -as'→* (_Low_)
        V  rv S (CFG_node m). cf V = cf' V CFG_node (_Low_)  S
        preds (slice_kinds S as) [(cf,undefined)]
        preds (slice_kinds S as') [(cf',undefined)]
      show ?thesis by -(erule slpa_rv_Low_Use_Low,auto)
    qed
  qed
qed



lemma nonInterference_path_to_Low:
  assumes "[cf] L [cf']" and "(_High_)  HRB_slice SCFG"
  and "CFG_node (_Low_)  S"
  and "(_Entry_) -as* (_Low_)" and "preds (kinds as) [(cf,undefined)]"
  and "(_Entry_) -as'* (_Low_)" and "preds (kinds as') [(cf',undefined)]"
  shows "map fst (transfers (kinds as) [(cf,undefined)]) L 
         map fst (transfers (kinds as') [(cf',undefined)])"
proof -
  from (_Entry_) -as* (_Low_) preds (kinds as) [(cf,undefined)]
    CFG_node (_Low_)  S
  obtain asx where "preds (slice_kinds S asx) [(cf,undefined)]"
    and "V  Use (_Low_). 
    state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V = 
    state_val (transfers (kinds as) [(cf,undefined)]) V"
    and "slice_edges S [] as = slice_edges S [] asx"
    and "transfers (kinds as) [(cf,undefined)]  []"
    and "(_Entry_) -asx* (_Low_)" 
    by(erule fundamental_property_of_static_slicing)
  from (_Entry_) -as'* (_Low_) preds (kinds as') [(cf',undefined)]
    CFG_node (_Low_)  S
  obtain asx' where "preds (slice_kinds S asx') [(cf',undefined)]"
    and "V  Use (_Low_). 
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V = 
    state_val (transfers(kinds as') [(cf',undefined)]) V"
    and "slice_edges S [] as' = 
    slice_edges S [] asx'"
    and "transfers (kinds as') [(cf',undefined)]  []"
    and "(_Entry_) -asx'* (_Low_)"
    by(erule fundamental_property_of_static_slicing)
  from [cf] L [cf'] (_High_)  HRB_slice SCFG
  have "V  rv S (CFG_node (_Entry_)). cf V = cf' V" 
    by(fastforce dest:lowEquivalence_relevant_nodes_Entry)
  with (_Entry_) -asx *(_Low_) (_Entry_) -asx'* (_Low_)
    CFG_node (_Low_)  S preds (slice_kinds S asx) [(cf,undefined)]
    preds (slice_kinds S asx') [(cf',undefined)]
  have "V  Use (_Low_). 
    state_val (transfers(slice_kinds S asx) [(cf,undefined)]) V =
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V"
    by -(rule rv_Low_Use_Low,auto intro:get_proc_Entry)
  with V  Use (_Low_). 
    state_val (transfers (slice_kinds S asx) [(cf,undefined)]) V = 
    state_val (transfers (kinds as) [(cf,undefined)]) V
    V  Use (_Low_). 
    state_val (transfers(slice_kinds S asx') [(cf',undefined)]) V = 
    state_val (transfers(kinds as') [(cf',undefined)]) V
    transfers (kinds as) [(cf,undefined)]  [] 
    transfers (kinds as') [(cf',undefined)]  []
  show ?thesis by(fastforce simp:lowEquivalence_def UseLow neq_Nil_conv)
qed


theorem nonInterference_path:
  assumes "[cf] L [cf']" and "(_High_)  HRB_slice SCFG"
  and "CFG_node (_Low_)  S"
  and "(_Entry_) -as* (_Exit_)" and "preds (kinds as) [(cf,undefined)]"
  and "(_Entry_) -as'* (_Exit_)" and "preds (kinds as') [(cf',undefined)]"
  shows "map fst (transfers (kinds as) [(cf,undefined)]) L 
  map fst (transfers (kinds as') [(cf',undefined)])"
proof -
  from (_Entry_) -as* (_Exit_) obtain x xs where "as = x#xs"
    and "(_Entry_) = sourcenode x" and "valid_edge x" 
    and "targetnode x -xs→* (_Exit_)"
    apply(cases "as = []")
     apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(fastforce elim:path_split_Cons simp:vp_def)
  from (_Entry_) -as* (_Exit_) have "valid_path as" by(simp add:vp_def)
  from valid_edge x have "valid_node (targetnode x)" by simp
  hence "inner_node (targetnode x)"
  proof(cases rule:valid_node_cases)
    case Entry
    with valid_edge x have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with targetnode x -xs→* (_Exit_) have "xs = []"
      by -(drule path_Exit_source,auto)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)" by blast
    from valid_edge x valid_edge z (_Entry_) = sourcenode x 
      sourcenode z = (_Entry_) Exit targetnode z = (_Exit_)
    have "x = z" by(fastforce intro:edge_det)
    with preds (kinds as) [(cf,undefined)] as = x#xs xs = []
      kind z = (λs. False) 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with targetnode x -xs→* (_Exit_) obtain x' xs' where "xs = xs'@[x']"
    and "targetnode x -xs'→* (_Low_)" and "kind x' = (λs. True)"
    by(fastforce elim:Exit_path_Low_path)
  with (_Entry_) = sourcenode x valid_edge x
  have "(_Entry_) -x#xs'→* (_Low_)" by(fastforce intro:Cons_path)
  from valid_path as as = x#xs xs = xs'@[x']
  have "valid_path (x#xs')"
    by(simp add:valid_path_def del:valid_path_aux.simps)
      (rule valid_path_aux_split,simp)
  with (_Entry_) -x#xs'→* (_Low_) have "(_Entry_) -x#xs'* (_Low_)"
    by(simp add:vp_def)
  from as = x#xs xs = xs'@[x'] have "as = (x#xs')@[x']" by simp
  with preds (kinds as) [(cf,undefined)] 
  have "preds (kinds (x#xs')) [(cf,undefined)]"
    by(simp add:kinds_def preds_split)
  from (_Entry_) -as'* (_Exit_) obtain y ys where "as' = y#ys"
    and "(_Entry_) = sourcenode y" and "valid_edge y" 
    and "targetnode y -ys→* (_Exit_)"
    apply(cases "as' = []")
     apply(clarsimp simp:vp_def,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(fastforce elim:path_split_Cons simp:vp_def)
  from (_Entry_) -as'* (_Exit_) have "valid_path as'" by(simp add:vp_def)
  from valid_edge y have "valid_node (targetnode y)" by simp
  hence "inner_node (targetnode y)"
  proof(cases rule:valid_node_cases)
    case Entry
    with valid_edge y have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with targetnode y -ys→* (_Exit_) have "ys = []"
      by -(drule path_Exit_source,auto)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)" by blast
    from valid_edge y valid_edge z (_Entry_) = sourcenode y 
      sourcenode z = (_Entry_) Exit targetnode z = (_Exit_)
    have "y = z" by(fastforce intro:edge_det)
    with preds (kinds as') [(cf',undefined)] as' = y#ys ys = []
      kind z = (λs. False) 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with targetnode y -ys→* (_Exit_) obtain y' ys' where "ys = ys'@[y']"
    and "targetnode y -ys'→* (_Low_)" and "kind y' = (λs. True)"
    by(fastforce elim:Exit_path_Low_path)
  with (_Entry_) = sourcenode y valid_edge y
  have "(_Entry_) -y#ys'→* (_Low_)" by(fastforce intro:Cons_path)
  from valid_path as' as' = y#ys ys = ys'@[y']
  have "valid_path (y#ys')"
    by(simp add:valid_path_def del:valid_path_aux.simps)
      (rule valid_path_aux_split,simp)
  with (_Entry_) -y#ys'→* (_Low_) have "(_Entry_) -y#ys'* (_Low_)"
    by(simp add:vp_def)
  from as' = y#ys ys = ys'@[y'] have "as' = (y#ys')@[y']" by simp
  with preds (kinds as') [(cf',undefined)] 
  have "preds (kinds (y#ys')) [(cf',undefined)]"
    by(simp add:kinds_def preds_split)
  from [cf] L [cf'] (_High_)  HRB_slice SCFG CFG_node (_Low_)  S
    (_Entry_) -x#xs'* (_Low_) preds (kinds (x#xs')) [(cf,undefined)]
    (_Entry_) -y#ys'* (_Low_) preds (kinds (y#ys')) [(cf',undefined)]
  have "map fst (transfers (kinds (x#xs')) [(cf,undefined)]) L 
    map fst (transfers (kinds (y#ys')) [(cf',undefined)])"
    by(rule nonInterference_path_to_Low)
  with as = x#xs xs = xs'@[x'] kind x' = (λs. True)
    as' = y#ys ys = ys'@[y'] kind y' = (λs. True)
  show ?thesis
    apply(cases "transfers (map kind xs') (transfer (kind x) [(cf,undefined)])")
    apply (auto simp add:kinds_def transfers_split)
    by((cases "transfers (map kind ys') (transfer (kind y) [(cf',undefined)])"),
       (auto simp add:kinds_def transfers_split))+
qed


end

text ‹The second theorem assumes that we have a operational semantics,
whose evaluations are written ⟨c,s⟩ ⇒ ⟨c',s'⟩› and which conforms 
to the CFG. The correctness theorem then states that if no high variable
influenced a low variable and the initial states were low equivalent, the
reulting states are again low equivalent:›


locale NonInterferenceInter = 
  NonInterferenceInterGraph sourcenode targetnode kind valid_edge Entry 
    get_proc get_return_edges procs Main Exit Def Use ParamDefs ParamUses 
    H L High Low +
  SemanticsProperty sourcenode targetnode kind valid_edge Entry get_proc
    get_return_edges procs Main Exit Def Use ParamDefs ParamUses sem identifies
  for sourcenode :: "'edge  'node" and targetnode :: "'edge  'node"
  and kind :: "'edge  ('var,'val,'ret,'pname) edge_kind" 
  and valid_edge :: "'edge  bool"
  and Entry :: "'node" ("'('_Entry'_')")  and get_proc :: "'node  'pname"
  and get_return_edges :: "'edge  'edge set"
  and procs :: "('pname × 'var list × 'var list) list" and Main :: "'pname"
  and Exit::"'node"  ("'('_Exit'_')") 
  and Def :: "'node  'var set" and Use :: "'node  'var set"
  and ParamDefs :: "'node  'var list" and ParamUses :: "'node  'var set list"
  and sem :: "'com  ('var  'val) list  'com  ('var  'val) list  bool" 
    ("((1_,/_) / (1_,/_))" [0,0,0,0] 81)
  and identifies :: "'node  'com  bool" ("_  _" [51,0] 80)
  and H :: "'var set" and L :: "'var set" 
  and High :: "'node"  ("'('_High'_')") and Low :: "'node" ("'('_Low'_')") +
  fixes final :: "'com  bool"
  assumes final_edge_Low: "final c; n  c 
     a. valid_edge a  sourcenode a = n  targetnode a = (_Low_)  kind a = id"
begin


text‹The following theorem needs the explicit edge from (_High_)›
  to n›. An approach using a init› predicate for initial statements,
  being reachable from (_High_)› via a (λs. True) edge,
  does not work as the same statement could be identified by several nodes, some
  initial, some not. E.g., in the program \texttt{while (True) Skip;;Skip}
  two nodes identify this inital statement: the initial node and the node
  within the loop (because of loop unrolling).›

theorem nonInterference:
  assumes "[cf1] L [cf2]" and "(_High_)  HRB_slice SCFG"
  and "CFG_node (_Low_)  S"
  and "valid_edge a" and "sourcenode a = (_High_)" and "targetnode a = n" 
  and "kind a = (λs. True)" and "n  c" and "final c'"
  and "c,[cf1]  c',s1" and "c,[cf2]  c',s2"
  shows "s1 L s2"
proof -
  from High_target_Entry_edge obtain ax where "valid_edge ax"
    and "sourcenode ax = (_Entry_)" and "targetnode ax = (_High_)"
    and "kind ax = (λs. True)" by blast
  from n  c c,[cf1]  c',s1
  obtain n1 as1 cfs1 where "n -as1* n1" and "n1  c'"
    and "preds (kinds as1) [(cf1,undefined)]" 
    and "transfers (kinds as1) [(cf1,undefined)] = cfs1" and "map fst cfs1 = s1"
    by(fastforce dest:fundamental_property)
  from n -as1* n1 valid_edge a sourcenode a = (_High_) targetnode a = n
    kind a = (λs. True)
  have "(_High_) -a#as1* n1" by(fastforce intro:Cons_path simp:vp_def valid_path_def)
  from<