Theory Ipassmt

theory Ipassmt
imports Common_Primitive_Syntax
        "../Semantics_Ternary/Primitive_Normalization"
        Simple_Firewall.Iface
        Simple_Firewall.IP_Addr_WordInterval_toString (*for debug pretty-printing*)
        Automatic_Refinement.Misc (*dependnecy!*)
begin
  hide_const Misc.uncurry
  hide_fact Misc.uncurry_def
    
  text‹A mapping from an interface to its assigned ip addresses in CIDR notation›
  type_synonym 'i ipassignment="iface  ('i word × nat) list" (*technically, a set*)


subsection‹Sanity checking for an @{typ "'i ipassignment"}.›

  text‹warning if interface map has wildcards›
  definition ipassmt_sanity_nowildcards :: "'i ipassignment  bool" where
    "ipassmt_sanity_nowildcards ipassmt   iface  dom ipassmt. ¬ iface_is_wildcard iface"

    text‹Executable of the @{typ "'i ipassignment"} is given as a list.›
    lemma[code_unfold]: "ipassmt_sanity_nowildcards (map_of ipassmt)  ( iface  fst` set ipassmt. ¬ iface_is_wildcard iface)"
      by(simp add: ipassmt_sanity_nowildcards_def Map.dom_map_of_conv_image_fst)
  
  lemma ipassmt_sanity_nowildcards_match_iface:
      "ipassmt_sanity_nowildcards ipassmt 
       ipassmt (Iface ifce2) = None 
       ipassmt ifce = Some a 
       ¬ match_iface ifce ifce2"
  unfolding ipassmt_sanity_nowildcards_def 
  by (metis domIff iface.exhaust iface.sel option.distinct(1) iface_is_wildcard_def match_iface_case_nowildcard)


  (* use this in all exported code*)
  (*TODO: generate useful error message in exported code*)
  definition map_of_ipassmt :: "(iface × ('i word × nat) list) list  iface  ('i word × nat) list" where
    "map_of_ipassmt ipassmt = (
      if
        distinct (map fst ipassmt)  ipassmt_sanity_nowildcards (map_of ipassmt)
      then
        map_of ipassmt
      else undefined ⌦‹undefined_ipassmt_must_be_distinct_and_dont_have_wildcard_interfaces›)"


  text‹some additional (optional) sanity checks›
  
  text‹sanity check that there are no zone-spanning interfaces›
  definition ipassmt_sanity_disjoint :: "'i::len ipassignment  bool" where
    "ipassmt_sanity_disjoint ipassmt   i1  dom ipassmt.  i2  dom ipassmt. i1  i2 
          ipcidr_union_set (set (the (ipassmt i1)))  ipcidr_union_set (set (the (ipassmt i2))) = {}"
  
  lemma[code_unfold]: "ipassmt_sanity_disjoint (map_of ipassmt) 
    (let Is = fst` set ipassmt in 
      ( i1  Is.  i2  Is. i1  i2  wordinterval_empty (wordinterval_intersection (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1))))  (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))))"
    apply(simp add: ipassmt_sanity_disjoint_def Map.dom_map_of_conv_image_fst)
    apply(simp add: ipcidr_union_set_def)
    apply(simp add: l2wi)
    apply(simp add: ipcidr_to_interval_def)
    using ipset_from_cidr_ipcidr_to_interval by blast
  
  
  text‹Checking that the ipassmt covers the complete ipv4 address space.›
  definition ipassmt_sanity_complete :: "(iface × ('i::len word × nat) list) list  bool" where
    "ipassmt_sanity_complete ipassmt  distinct (map fst ipassmt)  ((ipcidr_union_set ` set ` (ran (map_of ipassmt)))) = UNIV"

    lemma[code_unfold]: "ipassmt_sanity_complete ipassmt  distinct (map fst ipassmt)  (let range = map snd ipassmt in 
        wordinterval_eq (wordinterval_Union (map (l2wi  (map ipcidr_to_interval)) range)) wordinterval_UNIV
        )"
     apply(cases "distinct (map fst ipassmt)")
      apply(simp add: ipassmt_sanity_complete_def)
      apply(simp add: Map.ran_distinct)
      apply(simp add: wordinterval_eq_set_eq wordinterval_Union)
      apply(simp add: l2wi)
      apply(simp add: ipcidr_to_interval_def)
      apply(simp add: ipcidr_union_set_def ipset_from_cidr_ipcidr_to_interval; fail)
     apply(simp add: ipassmt_sanity_complete_def)
     done



    value[code] "ipassmt_sanity_nowildcards (map_of [(Iface ''eth1.1017'', [(ipv4addr_of_dotdecimal (131,159,14,240), 28)])])"

  fun collect_ifaces' :: "'i::len common_primitive rule list  iface list" where
    "collect_ifaces' [] = []" |
    "collect_ifaces' ((Rule m a)#rs) = filter (λiface. iface  ifaceAny) (
                                      (map (λx. case x of Pos i  i | Neg i  i) (fst (primitive_extractor (is_Iiface, iiface_sel) m))) @
                                      (map (λx. case x of Pos i  i | Neg i  i) (fst (primitive_extractor (is_Oiface, oiface_sel) m))) @ collect_ifaces' rs)"

  definition collect_ifaces :: "'i::len common_primitive rule list  iface list" where
    "collect_ifaces rs  mergesort_remdups (collect_ifaces' rs)"
  lemma "set (collect_ifaces rs) = set (collect_ifaces' rs)"
    by(simp add: collect_ifaces_def mergesort_remdups_correct)

  text‹sanity check that all interfaces mentioned in the ruleset are also listed in the ipassmt. May fail for wildcard interfaces in the ruleset.›

  (*primitive_extractor requires normalized_nnf_primitives*)
  definition ipassmt_sanity_defined :: "'i::len common_primitive rule list  'i ipassignment  bool" where
    "ipassmt_sanity_defined rs ipassmt   iface  set (collect_ifaces rs). iface  dom ipassmt"

    lemma[code]: "ipassmt_sanity_defined rs ipassmt  ( iface  set (collect_ifaces rs). ipassmt iface  None)"
      by(simp add: ipassmt_sanity_defined_def Map.domIff)
  
    lemma "ipassmt_sanity_defined [
         Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (Iface ''eth1.1017'')))) action.Accept,
         Rule (MatchAnd (Match (Src (IpAddrNetmask (ipv4addr_of_dotdecimal (192,168,0,0)) 24))) (Match (IIface (ifaceAny)))) action.Accept,
         Rule MatchAny action.Drop]
             (map_of [(Iface ''eth1.1017'', [(ipv4addr_of_dotdecimal (131,159,14,240), 28)])])" by eval



  (*TODO: use and add code equation*)
  definition ipassmt_ignore_wildcard :: "'i::len ipassignment  'i ipassignment" where
    "ipassmt_ignore_wildcard ipassmt  λk. case ipassmt k of None  None 
                                                           | Some ips  if ipcidr_union_set (set ips) = UNIV then None else Some ips"

  lemma ipassmt_ignore_wildcard_le: "ipassmt_ignore_wildcard ipassmt m ipassmt"
    apply(simp add: ipassmt_ignore_wildcard_def map_le_def)
    apply(clarify)
    apply(simp split: option.split_asm if_split_asm)
    done

  definition ipassmt_ignore_wildcard_list:: "(iface × ('i::len word × nat) list) list  (iface × ('i word × nat) list) list" where
    "ipassmt_ignore_wildcard_list ipassmt = filter (λ(_,ips).  ¬ wordinterval_eq (l2wi (map ipcidr_to_interval ips)) wordinterval_UNIV) ipassmt"

  (*distinct fst ipassmt notwendig?*)
  lemma "distinct (map fst ipassmt) 
    map_of (ipassmt_ignore_wildcard_list ipassmt) = ipassmt_ignore_wildcard (map_of ipassmt)"
      apply(simp add: ipassmt_ignore_wildcard_list_def ipassmt_ignore_wildcard_def)
      apply(simp add: wordinterval_eq_set_eq)
      apply(simp add: l2wi)
      apply(simp add: ipcidr_to_interval_def)
      apply(simp add: fun_eq_iff)
      apply(clarify)
      apply(induction ipassmt)
       apply(simp; fail)
      apply(simp)
      apply(simp split:option.split option.split_asm)
      apply(simp add: ipcidr_union_set_def ipset_from_cidr_ipcidr_to_interval)
      apply(simp add: case_prod_unfold)
      by blast
      (*apply(safe)
                       apply(simp_all)
      by (simp add: rev_image_eqI)*)
      

  
  text‹Debug algorithm with human-readable output›
  definition debug_ipassmt_generic
    :: "('i::len wordinterval  string) 
          (iface × ('i word × nat) list) list  'i common_primitive rule list  string list" where
    "debug_ipassmt_generic toStr ipassmt rs  let ifaces = (map fst ipassmt) in [
      ''distinct: '' @ (if distinct ifaces then ''passed'' else ''FAIL!'')
      , ''ipassmt_sanity_nowildcards: '' @
          (if ipassmt_sanity_nowildcards (map_of ipassmt)
           then ''passed'' else ''fail: ''@list_toString iface_sel (filter iface_is_wildcard ifaces))
      , ''ipassmt_sanity_defined (interfaces defined in the ruleset are also in ipassmt): '' @ 
          (if ipassmt_sanity_defined rs (map_of ipassmt)
           then ''passed'' else ''fail: ''@list_toString iface_sel [i  (collect_ifaces rs). i  set ifaces])
      , ''ipassmt_sanity_disjoint (no zone-spanning interfaces): '' @
          (if ipassmt_sanity_disjoint (map_of ipassmt)
           then ''passed'' else ''fail: ''@list_toString (λ(i1,i2). ''('' @ iface_sel i1 @ '','' @ iface_sel i2 @ '')'')
               [(i1,i2)  List.product ifaces ifaces. i1  i2 
                ¬ wordinterval_empty (wordinterval_intersection
                                        (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1))))
                                        (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))
          ])
      , ''ipassmt_sanity_disjoint excluding UNIV interfaces: '' @
          (let ipassmt = ipassmt_ignore_wildcard_list ipassmt;
               ifaces = (map fst ipassmt)
           in
          (if ipassmt_sanity_disjoint (map_of ipassmt)
           then ''passed'' else ''fail: ''@list_toString (λ(i1,i2). ''('' @ iface_sel i1 @ '','' @ iface_sel i2 @ '')'')
               [(i1,i2)  List.product ifaces ifaces. i1  i2 
                ¬ wordinterval_empty (wordinterval_intersection
                                        (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i1))))
                                        (l2wi (map ipcidr_to_interval (the ((map_of ipassmt) i2)))))
          ]))
       , ''ipassmt_sanity_complete: '' @ 
          (if ipassmt_sanity_complete ipassmt
           then ''passed''
           else ''the following is not covered: '' @ 
            toStr (wordinterval_setminus wordinterval_UNIV (wordinterval_Union (map (l2wi  (map ipcidr_to_interval)) (map snd ipassmt)))))
      , ''ipassmt_sanity_complete excluding UNIV interfaces: '' @
          (let ipassmt = ipassmt_ignore_wildcard_list ipassmt
           in
          (if ipassmt_sanity_complete ipassmt
           then ''passed''
           else ''the following is not covered: '' @
            toStr (wordinterval_setminus wordinterval_UNIV (wordinterval_Union (map (l2wi  (map ipcidr_to_interval)) (map snd ipassmt))))))
      ]"

  definition "debug_ipassmt_ipv4  debug_ipassmt_generic ipv4addr_wordinterval_toString"
  definition "debug_ipassmt_ipv6  debug_ipassmt_generic ipv6addr_wordinterval_toString"


  lemma dom_ipassmt_ignore_wildcard:
    "idom (ipassmt_ignore_wildcard ipassmt)  i  dom ipassmt  ipcidr_union_set (set (the (ipassmt i)))  UNIV"
    apply(simp add: ipassmt_ignore_wildcard_def)
    apply(rule)
     apply(clarify)
     apply(simp split: option.split_asm if_split_asm)
     apply blast
    apply(clarify)
    apply(simp)
    done

  lemma ipassmt_ignore_wildcard_the:
    "ipassmt i = Some ips  ipcidr_union_set (set ips)  UNIV  (the (ipassmt_ignore_wildcard ipassmt i)) = ips"
    "ipassmt_ignore_wildcard ipassmt i = Some ips  the (ipassmt i) = ips"
    "ipassmt_ignore_wildcard ipassmt i = Some ips  ipcidr_union_set (set ips)  UNIV"
    by (simp_all add: ipassmt_ignore_wildcard_def split: option.split_asm if_split_asm)
    

  lemma ipassmt_sanity_disjoint_ignore_wildcards:
        "ipassmt_sanity_disjoint (ipassmt_ignore_wildcard ipassmt) 
         (i1dom ipassmt.
          i2dom ipassmt.
            ipcidr_union_set (set (the (ipassmt i1)))  UNIV 
            ipcidr_union_set (set (the (ipassmt i2)))  UNIV 
            i1  i2 
             ipcidr_union_set (set (the (ipassmt i1)))  ipcidr_union_set (set (the (ipassmt i2))) = {})"
    apply(simp add: ipassmt_sanity_disjoint_def)
    apply(rule)
     apply(clarify)
     apply(simp)
     subgoal for i1 i2 ips1 ips2
     apply(erule_tac x=i1 in ballE)
      prefer 2
      using dom_ipassmt_ignore_wildcard  apply (metis domI option.sel)
     apply(erule_tac x=i2 in ballE)
      prefer 2
      using dom_ipassmt_ignore_wildcard apply (metis domI domIff option.sel)
     by(simp add: ipassmt_ignore_wildcard_the; fail)
    apply(clarify)
    apply(simp)
    subgoal for i1 i2 ips1 ips2
    apply(erule_tac x=i1 in ballE)
     prefer 2
     using dom_ipassmt_ignore_wildcard apply auto[1]
    apply(erule_tac x=i2 in ballE)
     prefer 2
     using dom_ipassmt_ignore_wildcard apply auto[1]
    by(simp add: ipassmt_ignore_wildcard_the)
   done

  text‹Confusing names: @{const ipassmt_sanity_nowildcards} refers to wildcard interfaces.
       @{const ipassmt_ignore_wildcard} refers to the UNIV ip range.
›
  lemma ipassmt_sanity_nowildcards_ignore_wildcardD:
    "ipassmt_sanity_nowildcards ipassmt  ipassmt_sanity_nowildcards (ipassmt_ignore_wildcard ipassmt)"
    by (simp add: dom_ipassmt_ignore_wildcard ipassmt_sanity_nowildcards_def)
    

 lemma ipassmt_disjoint_nonempty_inj:
     assumes ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
        and ifce: "ipassmt ifce = Some i_ips"
        and a: "ipcidr_union_set (set i_ips)  {}"
        and k: "ipassmt k = Some i_ips"
     shows "k = ifce"
     proof(rule ccontr)
       assume "k  ifce"
       with ifce k ipassmt_disjoint have "ipcidr_union_set (set (the (ipassmt k)))  ipcidr_union_set (set (the (ipassmt ifce))) = {}"
         unfolding ipassmt_sanity_disjoint_def by fastforce
       thus False using a ifce k by auto 
     qed

  lemma ipassmt_ignore_wildcard_None_Some:
    "ipassmt_ignore_wildcard ipassmt ifce = None  ipassmt ifce = Some ips  ipcidr_union_set (set ips) = UNIV"
    by (metis domI domIff dom_ipassmt_ignore_wildcard option.sel)
    

 (*can this lemma be somehow useful?
   maybe when rewriting, we can try to rewrite in the ignore_wildcard space and just constrain the the other area?*)
 lemma ipassmt_disjoint_ignore_wildcard_nonempty_inj:
     assumes ipassmt_disjoint: "ipassmt_sanity_disjoint (ipassmt_ignore_wildcard ipassmt)"
        and ifce: "ipassmt ifce = Some i_ips"
        and a: "ipcidr_union_set (set i_ips)  {}"
        and k: "(ipassmt_ignore_wildcard ipassmt) k = Some i_ips"
     shows "k = ifce"
     proof(rule ccontr)
       assume "k  ifce"
       show False
       proof(cases "(ipassmt_ignore_wildcard ipassmt) ifce")
       case (Some i_ips') (*proofs mainly by sledgehammer*)
         hence "i_ips' = i_ips" using ifce ipassmt_ignore_wildcard_the(2) by fastforce
         hence "(ipassmt_ignore_wildcard ipassmt) k = Some i_ips" using Some ifce ipassmt_ignore_wildcard_def k by auto 
         thus False using Some i_ips' = i_ips k  ifce a ipassmt_disjoint ipassmt_disjoint_nonempty_inj by blast
       next
       case None
         with ipassmt_ignore_wildcard_None_Some have "ipcidr_union_set (set i_ips) = UNIV" using ifce by auto 
         thus False using ipassmt_ignore_wildcard_the(3) k by blast 
       qed
     qed

 lemma ipassmt_disjoint_inj_k: 
     assumes ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
        and ifce: "ipassmt ifce = Some ips"
        and k: "ipassmt k = Some ips'"
        and a: "p  ipcidr_union_set (set ips)"
        and b: "p  ipcidr_union_set (set ips')"
     shows "k = ifce"
     proof(rule ccontr)
       assume "k  ifce"
       with ipassmt_disjoint have
          "ipcidr_union_set (set (the (ipassmt k)))  ipcidr_union_set (set (the (ipassmt ifce))) = {}"
         unfolding ipassmt_sanity_disjoint_def using ifce k by blast
       hence "ipcidr_union_set (set ips')  ipcidr_union_set (set ips) = {}" by(simp add: k ifce)
       thus False using a b by blast
     qed

 (*might also work when we ignore UNIVs in the ipassmt? (not tested)*)
 lemma ipassmt_disjoint_matcheq_iifce_srcip:
        assumes ipassmt_nowild: "ipassmt_sanity_nowildcards ipassmt"
            and ipassmt_disjoint: "ipassmt_sanity_disjoint ipassmt"
            and ifce: "ipassmt ifce = Some i_ips"
            and p_ifce: "ipassmt (Iface (p_iiface p)) = Some p_ips  p_src p  ipcidr_union_set (set p_ips)"
        shows   "match_iface ifce (p_iiface p)  p_src p  ipcidr_union_set (set i_ips)"
    proof
     assume "match_iface ifce (p_iiface p)"
     thus "p_src p  ipcidr_union_set (set i_ips)"
       apply(cases "ifce = Iface (p_iiface p)")
        using ifce p_ifce apply force
       by (metis domI iface.sel iface_is_wildcard_def ifce ipassmt_nowild ipassmt_sanity_nowildcards_def match_iface.elims(2) match_iface_case_nowildcard)
   next
     assume a: "p_src p  ipcidr_union_set (set i_ips)"
     ― ‹basically, we need to reverse the map @{term ipassmt}

     from ipassmt_disjoint_nonempty_inj[OF ipassmt_disjoint ifce] a have ipassmt_inj: "k. ipassmt k = Some i_ips  k = ifce" by blast

     from ipassmt_disjoint_inj_k[OF ipassmt_disjoint ifce _ a] have ipassmt_inj_k:
      "k ips'. ipassmt k = Some ips'  p_src p  ipcidr_union_set (set ips')  k = ifce" by simp

     have ipassmt_inj_p: "ips'. p_src p  ipcidr_union_set (set ips')  (k. ipassmt k = Some ips')  ips' = i_ips"
       apply(clarify)
       apply(rename_tac ips' k)
       apply(subgoal_tac "k = ifce")
        using ifce apply simp
       using ipassmt_inj_k by simp

     from p_ifce have "(Iface (p_iiface p)) = ifce" using ipassmt_inj_p ipassmt_inj by blast 

     thus "match_iface ifce (p_iiface p)" using match_iface_refl by blast 
   qed



  definition ipassmt_generic_ipv4 :: "(iface × (32 word × nat) list) list" where
    "ipassmt_generic_ipv4 = [(Iface ''lo'', [(ipv4addr_of_dotdecimal (127,0,0,0),8)])]"

  definition ipassmt_generic_ipv6 :: "(iface × (128 word × nat) list) list" where
    "ipassmt_generic_ipv6 = [(Iface ''lo'', [(1,128)])]" (*::1/128*)



subsection‹IP Assignment difference›
  text‹Compare two ipassmts. Returns a list of tuples
    First entry of the tuple: things which are in the left ipassmt but not in the right.
    Second entry of the tupls: things which are in the right ipassmt but not in the left.›
  definition ipassmt_diff
    :: "(iface × ('i::len word × nat) list) list  (iface × ('i::len word × nat) list) list
         (iface × ('i word × nat) list × ('i word × nat) list) list"
  where
  "ipassmt_diff a b  let
      t = λs. (case s of None  Empty_WordInterval
                       | Some s  wordinterval_Union (map ipcidr_tuple_to_wordinterval s));
      k = λx y d. cidr_split (wordinterval_setminus (t (map_of x d)) (t (map_of y d)))
    in
      [(d, (k a b d, k b a d)). d  remdups (map fst (a @ b))]"
  
  
  text‹If an interface is defined in both ipassignments and there is no difference
       then the two ipassignements describe the same IP range for this interface.›
  lemma ipassmt_diff_ifce_equal: "(ifce, [], [])  set (ipassmt_diff ipassmt1 ipassmt2)  
         ifce  dom (map_of ipassmt1)  ifce  dom (map_of ipassmt2) 
           ipcidr_union_set (set (the ((map_of ipassmt1) ifce))) =
           ipcidr_union_set (set (the ((map_of ipassmt2) ifce)))"
    proof -
    have cidr_empty: "[] = cidr_split r  wordinterval_to_set r = {}" for r :: "'a wordinterval"
      apply(subst cidr_split_prefix[symmetric])
      by(simp)
    show "(ifce, [], [])  set (ipassmt_diff ipassmt1 ipassmt2)  
         ifce  dom (map_of ipassmt1)  ifce  dom (map_of ipassmt2) 
           ipcidr_union_set (set (the ((map_of ipassmt1) ifce))) =
           ipcidr_union_set (set (the ((map_of ipassmt2) ifce)))"
    apply(simp add: ipassmt_diff_def Let_def ipcidr_union_set_uncurry)
    apply(simp add: Set.image_iff)
    apply(elim conjE)
    apply(drule cidr_empty)+
    apply(simp)
    apply(simp add: domIff)
    apply(elim exE)
    apply(simp add: wordinterval_Union wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry)
    done
  qed

  lemma ipcidr_union_cidr_split[simp]: "ipcidr_union_set (set (cidr_split a)) = wordinterval_to_set a"
    by(simp add: ipcidr_union_set_uncurry cidr_split_prefix)

  lemma 
    defines "assmt as ifce  ipcidr_union_set (set (the ((map_of as ifce))))"
    assumes diffs: "(ifce, d1, d2)  set (ipassmt_diff ipassmt1 ipassmt2)"
        and  doms: "ifce  dom (map_of ipassmt1)" "ifce  dom (map_of ipassmt2)"
    shows "ipcidr_union_set (set d1) = assmt ipassmt1 ifce - assmt ipassmt2 ifce"
          "ipcidr_union_set (set d2) = assmt ipassmt2 ifce - assmt ipassmt1 ifce"
    using assms by (clarsimp simp add: ipassmt_diff_def Let_def assmt_def wordinterval_Union; simp add: ipcidr_union_set_uncurry uncurry_def wordinterval_to_set_ipcidr_tuple_to_wordinterval_uncurry)+
            
  
  text‹Explanation for interface @{term "Iface ''a''"}: 
          Left ipassmt: The IP range 4/30 contains the addresses 4,5,6,7
          Diff: right ipassmt contains 6/32, so 4,5,7 is only in the left ipassmt.
          IP addresses 4,5 correspond to subnet 4/30.›
  lemma "ipassmt_diff (ipassmt_generic_ipv4 @ [(Iface ''a'', [(4,30)])])
                       (ipassmt_generic_ipv4 @ [(Iface ''a'', [(6,32), (0,30)]), (Iface ''b'', [(42,32)])]) =
    [(Iface ''lo'', [], []),
     (Iface ''a'', [(4, 31),(7, 32)],
                   [(0, 30)]
     ),
     (Iface ''b'', [], [(42, 32)])]" by eval

end