Theory D_Aodv_Loop_Freedom

(*  Title:       variants/d_fwdrreqs/Aodv_Loop_Freedom.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
*)

section "Lift and transfer invariants to show loop freedom"

theory D_Aodv_Loop_Freedom
imports AWN.OClosed_Transfer AWN.Qmsg_Lifting D_Global_Invariants D_Loop_Freedom
begin

subsection ‹Lift to parallel processes with queues›

lemma par_step_no_change_on_send_or_receive:
    fixes σ s a σ' s'
  assumes "((σ, s), a, (σ', s'))  oparp_sos i (oseqp_sos ΓAODV i) (seqp_sos ΓQMSG)"
      and "a  τ"
    shows "σ' i = σ i"
  using assms by (rule qmsg_no_change_on_send_or_receive)

lemma par_nhop_quality_increases:
  shows "opaodv i ⟨⟨⇘iqmsg  (otherwith ((=)) {i} (orecvmsg (λσ m.
                                    msg_fresh σ m  msg_zhops m)),
                                  other quality_increases {i} →)
                        global (λσ. dip. let nhip = the (nhop (rt (σ i)) dip)
                                          in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                                              (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
    proof (rule lift_into_qmsg [OF seq_nhop_quality_increases])
    show "opaodv i A (otherwith ((=)) {i}
                         (orecvmsg (λσ m. msg_fresh σ m  msg_zhops m)),
                        other quality_increases {i} →)
                       globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
    proof (rule ostep_invariant_weakenE [OF oquality_increases], simp_all)
      fix t :: "(((nat  state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
      assume "onll ΓAODV (λ((σ, _), _, (σ', _)). j. quality_increases (σ j) (σ' j)) t"
      thus "quality_increases (fst (fst t) i) (fst (snd (snd t)) i)"
        by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
    next
      fix σ σ' a
      assume "otherwith ((=)) {i}
                (orecvmsg (λσ m. msg_fresh σ m  msg_zhops m)) σ σ' a"
      thus "otherwith quality_increases {i} (orecvmsg (λ_. rreq_rrep_sn)) σ σ' a"
        by - (erule weaken_otherwith, auto)
    qed
  qed auto

lemma par_rreq_rrep_sn_quality_increases:
  "opaodv i ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                            globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
  proof -
    have "opaodv i A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF olocal_quality_increases])
         (auto dest!: onllD seqllD elim!: aodv_ex_labelE)
    hence "opaodv i ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                   globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

lemma par_rreq_rrep_nsqn_fresh_any_step:
  shows "opaodv i ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ,
                                   other (λ_ _. True) {i} →)
                                  globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
  proof -
    have "opaodv i A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
                       globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
    proof (rule ostep_invariant_weakenE [OF rreq_rrep_nsqn_fresh_any_step_invariant])
      fix t
      assume "onll ΓAODV (λ((σ, _), a, _). anycast (msg_fresh σ) a) t"
      thus "globala (λ(σ, a, σ'). anycast (msg_fresh σ) a) t"
        by (cases t) (clarsimp dest!: onllD, metis aodv_ex_label)
    qed auto
    hence "opaodv i ⟨⟨⇘iqmsg A (λσ _. (orecvmsg (λ_. rreq_rrep_sn)) σ, other (λ_ _. True) {i} →)
                                    globala (λ(σ, a, σ'). anycast (msg_fresh σ) a)"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

lemma par_anycast_msg_zhops:
  shows "opaodv i ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                  globala (λ(_, a, _). anycast msg_zhops a)"
  proof -
    from anycast_msg_zhops initiali_aodv oaodv_trans aodv_trans
      have "opaodv i A (act TT, other (λ_ _. True) {i} →)
                         seqll i (onll ΓAODV (λ(_, a, _). anycast msg_zhops a))"
        by (rule open_seq_step_invariant)
    hence "opaodv i A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                            globala (λ(_, a, _). anycast msg_zhops a)"
    proof (rule ostep_invariant_weakenE)
      fix t :: "(((nat  state) × (state, msg, pseqp, pseqp label) seqp), msg seq_action) transition"
      assume "seqll i (onll ΓAODV (λ(_, a, _). anycast msg_zhops a)) t"
      thus "globala (λ(_, a, _). anycast msg_zhops a) t"
        by (cases t) (clarsimp dest!: seqllD onllD, metis aodv_ex_label)
    qed simp_all
    hence "opaodv i ⟨⟨⇘iqmsg A (λσ _. orecvmsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
                                     globala (λ(_, a, _). anycast msg_zhops a)"
      by (rule lift_step_into_qmsg_statelessassm) simp_all
    thus ?thesis by rule auto
  qed

subsection ‹Lift to nodes›

lemma node_step_no_change_on_send_or_receive:
  assumes "((σ, NodeS i P R), a, (σ', NodeS i' P' R'))  onode_sos
                                      (oparp_sos i (oseqp_sos ΓAODV i) (seqp_sos ΓQMSG))"
      and "a  τ"
    shows "σ' i = σ i"
  using assms
  by (cases a) (auto elim!: par_step_no_change_on_send_or_receive)

lemma node_nhop_quality_increases:
  shows " i : opaodv i ⟨⟨⇘iqmsg : R o 
           (otherwith ((=)) {i}
              (oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m)),
              other quality_increases {i}
            →) global (λσ. dip. let nhip = the (nhop (rt (σ i)) dip)
                                  in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                                      (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
  by (rule node_lift [OF par_nhop_quality_increases]) auto

lemma node_quality_increases:
  " i : opaodv i ⟨⟨⇘iqmsg : R o A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
                                         other (λ_ _. True) {i} →)
                            globala (λ(σ, _, σ'). quality_increases (σ i) (σ' i))"
  by (rule node_lift_step_statelessassm [OF par_rreq_rrep_sn_quality_increases]) simp

lemma node_rreq_rrep_nsqn_fresh_any_step:
  shows " i : opaodv i ⟨⟨⇘iqmsg : R o A
          (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
          globala (λ(σ, a, σ'). castmsg (msg_fresh σ) a)"
  by (rule node_lift_anycast_statelessassm [OF par_rreq_rrep_nsqn_fresh_any_step])

lemma node_anycast_msg_zhops:
  shows " i : opaodv i ⟨⟨⇘iqmsg : R o A
          (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ, other (λ_ _. True) {i} →)
          globala (λ(_, a, _). castmsg msg_zhops a)"
  by (rule node_lift_anycast_statelessassm [OF par_anycast_msg_zhops])

lemma node_silent_change_only:
  shows " i : opaodv i ⟨⟨⇘iqmsg : Ri o A (λσ _. oarrivemsg (λ_ _. True) σ,
                                               other (λ_ _. True) {i} →)
          globala (λ(σ, a, σ'). a  τ  σ' i = σ i)"
  proof (rule ostep_invariantI, simp (no_asm), rule impI)
    fix σ ζ a σ' ζ'
    assume or: "(σ, ζ)  oreachable (i : opaodv i ⟨⟨⇘iqmsg : Rio)
                                    (λσ _. oarrivemsg (λ_ _. True) σ)
                                    (other (λ_ _. True) {i})"
      and tr: "((σ, ζ), a, (σ', ζ'))  trans (i : opaodv i ⟨⟨⇘iqmsg : Rio)"
      and "a  τn"
    from or obtain p R where "ζ = NodeS i p R"
      by - (drule node_net_state, metis)
    with tr have "((σ, NodeS i p R), a, (σ', ζ'))
                      onode_sos (oparp_sos i (trans (opaodv i)) (trans qmsg))"
      by simp
    thus "σ' i = σ i" using a  τn 
      by (cases rule: onode_sos.cases)
         (auto elim: qmsg_no_change_on_send_or_receive)
  qed

subsection ‹Lift to partial networks›

lemma arrive_rreq_rrep_nsqn_fresh_inc_sn [simp]:
  assumes "oarrivemsg (λσ m. msg_fresh σ m  P σ m) σ m"
    shows "oarrivemsg (λ_. rreq_rrep_sn) σ m"
  using assms by (cases m) auto

lemma opnet_nhop_quality_increases:
  shows "opnet (λi. opaodv i ⟨⟨⇘iqmsg) p 
           (otherwith ((=)) (net_tree_ips p)
              (oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m)),
               other quality_increases (net_tree_ips p) →)
              global (λσ. inet_tree_ips p. dip.
                          let nhip = the (nhop (rt (σ i)) dip)
                          in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                              (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
  proof (rule pnet_lift [OF node_nhop_quality_increases])
    fix i R
    have "i : opaodv i ⟨⟨⇘iqmsg : Ro A (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ,
                                              other (λ_ _. True) {i} →) globala (λ(σ, a, σ').
            castmsg (λm. msg_fresh σ m  msg_zhops m) a)"
    proof (rule ostep_invariantI, simp (no_asm))
      fix σ s a σ' s'
      assume or: "(σ, s)  oreachable (i : opaodv i ⟨⟨⇘iqmsg : Ro)
                                      (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ)
                                      (other (λ_ _. True) {i})"
         and tr: "((σ, s), a, (σ', s'))  trans (i : opaodv i ⟨⟨⇘iqmsg : Ro)"
         and am: "oarrivemsg (λ_. rreq_rrep_sn) σ a"
      from or tr am have "castmsg (msg_fresh σ) a"
        by (auto dest!: ostep_invariantD [OF node_rreq_rrep_nsqn_fresh_any_step])
      moreover from or tr am have "castmsg (msg_zhops) a"
        by (auto dest!: ostep_invariantD [OF node_anycast_msg_zhops])
      ultimately show "castmsg (λm. msg_fresh σ m  msg_zhops m) a"
        by (case_tac a) auto
    qed
    thus "i : opaodv i ⟨⟨⇘iqmsg : Ro A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, _).
               castmsg (λm. msg_fresh σ m  msg_zhops m) a)"
      by rule auto
  next
    fix i R
    show "i : opaodv i ⟨⟨⇘iqmsg : Ro A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, σ').
               a  τ  (d. a  i:deliver(d))  σ i = σ' i)"
      by (rule ostep_invariant_weakenE [OF node_silent_change_only]) auto
  next
    fix i R
    show "i : opaodv i ⟨⟨⇘iqmsg : Ro A
            (λσ _. oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m) σ,
             other quality_increases {i} →) globala (λ(σ, a, σ').
               a = τ  (d. a = i:deliver(d))  quality_increases (σ i) (σ' i))"
      by (rule ostep_invariant_weakenE [OF node_quality_increases]) auto
  qed simp_all

subsection ‹Lift to closed networks›

lemma onet_nhop_quality_increases:
  shows "oclosed (opnet (λi. opaodv i ⟨⟨⇘iqmsg) p)
            (λ_ _ _. True, other quality_increases (net_tree_ips p) →)
              global (λσ. inet_tree_ips p. dip.
                          let nhip = the (nhop (rt (σ i)) dip)
                          in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                              (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
  (is "_  (_, ?U →) ?inv")
  proof (rule inclosed_closed)
    from opnet_nhop_quality_increases
      show "opnet (λi. opaodv i ⟨⟨⇘iqmsg) p
                (otherwith ((=)) (net_tree_ips p) inoclosed, ?U →) ?inv"
    proof (rule oinvariant_weakenE)
      fix σ σ' :: "ip  state" and a :: "msg node_action"
      assume "otherwith ((=)) (net_tree_ips p) inoclosed σ σ' a"
      thus "otherwith ((=)) (net_tree_ips p)
              (oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m)) σ σ' a"
      proof (rule otherwithEI)
        fix σ :: "ip  state" and a :: "msg node_action"
        assume "inoclosed σ a"
        thus "oarrivemsg (λσ m. msg_fresh σ m  msg_zhops m) σ a"
        proof (cases a)
          fix ii ni ms
          assume "a = ii¬ni:arrive(ms)"
          moreover with inoclosed σ a obtain d di where "ms = newpkt(d, di)"
            by (cases ms) auto
          ultimately show ?thesis by simp
        qed simp_all
      qed
    qed
  qed

subsection ‹Transfer into the standard model›

interpretation aodv_openproc: openproc paodv opaodv id
  rewrites "aodv_openproc.initmissing = initmissing"
  proof -
    show "openproc paodv opaodv id"
    proof unfold_locales
      fix i :: ip
      have "{(σ, ζ). (σ i, ζ)  σAODV i  (j. j  i  σ j  fst ` σAODV j)}  σAODV'"
        unfolding σAODV_def σAODV'_def
        proof (rule equalityD1)
          show "f p. {(σ, ζ). (σ i, ζ)  {(f i, p)}  (j. j  i
                       σ j  fst ` {(f j, p)})} = {(f, p)}"
            by (rule set_eqI) auto
        qed
      thus "{ (σ, ζ) |σ ζ s. s  init (paodv i)
                              (σ i, ζ) = id s
                              (j. ji  σ j  (fst o id) ` init (paodv j)) }  init (opaodv i)"
        by simp
    next
      show "j. init (paodv j)  {}"
        unfolding σAODV_def by simp
    next
      fix i s a s' σ σ'
      assume "σ i = fst (id s)"
         and "σ' i = fst (id s')"
         and "(s, a, s')  trans (paodv i)"
      then obtain q q' where "s = (σ i, q)"
                         and "s' = (σ' i, q')"
                         and "((σ i, q), a, (σ' i, q'))  trans (paodv i)" 
         by (cases s, cases s') auto
      from this(3) have "((σ, q), a, (σ', q'))  trans (opaodv i)"
        by simp (rule open_seqp_action [OF aodv_wf])

      with s = (σ i, q) and s' = (σ' i, q')
        show "((σ, snd (id s)), a, (σ', snd (id s')))  trans (opaodv i)"
          by simp
    qed
    then interpret opn: openproc paodv opaodv id .
    have [simp]: "i. (SOME x. x  (fst o id) ` init (paodv i)) = aodv_init i"
      unfolding σAODV_def by simp
    hence "i. openproc.initmissing paodv id i = initmissing i"
      unfolding opn.initmissing_def opn.someinit_def initmissing_def
      by (auto split: option.split)
    thus "openproc.initmissing paodv id = initmissing" ..
  qed

interpretation aodv_openproc_par_qmsg: openproc_parq paodv opaodv id qmsg
  rewrites "aodv_openproc_par_qmsg.netglobal = netglobal"
    and "aodv_openproc_par_qmsg.initmissing = initmissing"
  proof -
    show "openproc_parq paodv opaodv id qmsg"
      by (unfold_locales) simp
    then interpret opq: openproc_parq paodv opaodv id qmsg .

    have im: "σ. openproc.initmissing (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) σ
                                                                                    = initmissing σ"
      unfolding opq.initmissing_def opq.someinit_def initmissing_def
      unfolding σAODV_def σQMSG_def by (clarsimp cong: option.case_cong)
    thus "openproc.initmissing (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) = initmissing"
      by (rule ext)
    have "P σ. openproc.netglobal (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) P σ
                                                                                = netglobal P σ"
      unfolding opq.netglobal_def netglobal_def opq.initmissing_def initmissing_def opq.someinit_def
      unfolding σAODV_def σQMSG_def
      by (clarsimp cong: option.case_cong
                   simp del: One_nat_def
                   simp add: fst_initmissing_netgmap_default_aodv_init_netlift
                                                  [symmetric, unfolded initmissing_def])
    thus "openproc.netglobal (λi. paodv i ⟨⟨ qmsg) (λ(p, q). (fst (id p), snd (id p), q)) = netglobal"
      by auto
  qed

lemma net_nhop_quality_increases:
  assumes "wf_net_tree n"
  shows "closed (pnet (λi. paodv i ⟨⟨ qmsg) n)  netglobal
                           (λσ. i dip. let nhip = the (nhop (rt (σ i)) dip)
                                        in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                                             (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
        (is "_  netglobal (λσ. i. ?inv σ i)")
  proof -
    from wf_net_tree n
      have proto: "closed (pnet (λi. paodv i ⟨⟨ qmsg) n)  netglobal (λσ. inet_tree_ips n. dip.
                                            let nhip = the (nhop (rt (σ i)) dip)
                                            in dip  vD (rt (σ i))  vD (rt (σ nhip))  nhip  dip
                                                 (rt (σ i)) ⊏⇘dip(rt (σ nhip)))"
        by (rule aodv_openproc_par_qmsg.close_opnet [OF _ onet_nhop_quality_increases])
    show ?thesis
    unfolding invariant_def opnet_sos.opnet_tau1
    proof (rule, simp only: aodv_openproc_par_qmsg.netglobalsimp
                            fst_initmissing_netgmap_pair_fst, rule allI)
      fix σ i
      assume sr: "σ  reachable (closed (pnet (λi. paodv i ⟨⟨ qmsg) n)) TT"
      hence "inet_tree_ips n. ?inv (fst (initmissing (netgmap fst σ))) i"
        by - (drule invariantD [OF proto],
              simp only: aodv_openproc_par_qmsg.netglobalsimp
                         fst_initmissing_netgmap_pair_fst)
      thus "?inv (fst (initmissing (netgmap fst σ))) i"
      proof (cases "inet_tree_ips n")
        assume "inet_tree_ips n"
        from sr have "σ  reachable (pnet (λi. paodv i ⟨⟨ qmsg) n) TT" ..
        hence "net_ips σ = net_tree_ips n" ..
        with inet_tree_ips n have "inet_ips σ" by simp
        hence "(fst (initmissing (netgmap fst σ))) i = aodv_init i"
          by simp
        thus ?thesis by simp
      qed metis
    qed
  qed

subsection ‹Loop freedom of AODV›

theorem aodv_loop_freedom:
  assumes "wf_net_tree n"
  shows "closed (pnet (λi. paodv i ⟨⟨ qmsg) n)  netglobal (λσ. dip. irrefl ((rt_graph σ dip)+))"
  using assms by (rule aodv_openproc_par_qmsg.netglobal_weakenE
                          [OF net_nhop_quality_increases inv_to_loop_freedom])

end