Theory B_Aodv_Loop_Freedom

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

section "Lift and transfer invariants to show loop freedom"

theory B_Aodv_Loop_Freedom
imports AWN.OClosed_Transfer AWN.Qmsg_Lifting B_Global_Invariants B_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 Γ⇩A⇩O⇩D⇩V i) (seqp_sos Γ⇩Q⇩M⇩S⇩G)"
      and "a ≠ τ"
    shows "σ' i = σ i"
  using assms by (rule qmsg_no_change_on_send_or_receive)

lemma par_nhop_quality_increases:
  shows "opaodv i ⟨⟨⇘i⇙ qmsg ⊨ (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 Γ⇩A⇩O⇩D⇩V (λ((σ, _), _, (σ', _)). ∀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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 Γ⇩A⇩O⇩D⇩V (λ((σ, _), 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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 Γ⇩A⇩O⇩D⇩V (λ(_, 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 Γ⇩A⇩O⇩D⇩V (λ(_, 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 ⟨⟨⇘i⇙ qmsg ⊨⇩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 Γ⇩A⇩O⇩D⇩V i) (seqp_sos Γ⇩Q⇩M⇩S⇩G))"
      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 ⟨⟨⇘i⇙ qmsg : 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 ⟨⟨⇘i⇙ qmsg : 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 ⟨⟨⇘i⇙ qmsg : 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 ⟨⟨⇘i⇙ qmsg : 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 ⟨⟨⇘i⇙ qmsg : R⇩i ⟩⇩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 ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o)
                                    (λσ _. oarrivemsg (λ_ _. True) σ)
                                    (other (λ_ _. True) {i})"
      and tr: "((σ, ζ), a, (σ', ζ')) ∈ trans (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⇩i⟩⇩o)"
      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 ⟨⟨⇘i⇙ qmsg) p ⊨
           (otherwith ((=)) (net_tree_ips p)
              (oarrivemsg (λσ m. msg_fresh σ m ∧ msg_zhops m)),
               other quality_increases (net_tree_ips p) →)
              global (λσ. ∀i∈net_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 ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩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 ⟨⟨⇘i⇙ qmsg : R⟩⇩o)
                                      (λσ _. oarrivemsg (λ_. rreq_rrep_sn) σ)
                                      (other (λ_ _. True) {i})"
         and tr: "((σ, s), a, (σ', s')) ∈ trans (⟨i : opaodv i ⟨⟨⇘i⇙ qmsg : R⟩⇩o)"
         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 ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩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 ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩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 ⟨⟨⇘i⇙ qmsg : R⟩⇩o ⊨⇩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 ⟨⟨⇘i⇙ qmsg) p)
           ⊨ (λ_ _ _. True, other quality_increases (net_tree_ips p) →)
              global (λσ. ∀i∈net_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 ⟨⟨⇘i⇙ qmsg) 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, ζ) ∈ σ⇩A⇩O⇩D⇩V i ∧ (∀j. j ≠ i ⟶ σ j ∈ fst ` σ⇩A⇩O⇩D⇩V j)} ⊆ σ⇩A⇩O⇩D⇩V'"
        unfolding σ⇩A⇩O⇩D⇩V_def σ⇩A⇩O⇩D⇩V'_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. j≠i ⟶ σ j ∈ (fst o id) ` init (paodv j)) } ⊆ init (opaodv i)"
        by simp
    next
      show "∀j. init (paodv j) ≠ {}"
        unfolding σ⇩A⇩O⇩D⇩V_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 σ⇩A⇩O⇩D⇩V_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 σ⇩A⇩O⇩D⇩V_def σ⇩Q⇩M⇩S⇩G_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 σ⇩A⇩O⇩D⇩V_def σ⇩Q⇩M⇩S⇩G_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 (λσ. ∀i∈net_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 "∀i∈net_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 "i∈net_tree_ips n")
        assume "i∉net_tree_ips n"
        from sr have "σ ∈ reachable (pnet (λi. paodv i ⟨⟨ qmsg) n) TT" ..
        hence "net_ips σ = net_tree_ips n" ..
        with ‹i∉net_tree_ips n› have "i∉net_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