Quelle  Aodv_Predicates.thy

(*  Title:       Aodv_Predicates.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke, Inria
*)

section "Invariant assumptions and properties"

theory Aodv_Predicates
imports Aodv
begin

text ‹Definitions for expression assumptions on incoming messages and properties of
 outgoing messages.›

abbreviation not_Pkt :: "msg ==> bool"
where "not_Pkt m ≡ case m of Pkt _ _ _ ==> False | _ ==> True"

definition msg_sender :: "msg ==> ip"
where "msg_sender m ≡ case m of Rreq _ _ _ _ _ _ _ ipc ==> ipc
                              | Rrep _ _ _ _ ipc ==> ipc
                              | Rerr _ ipc ==> ipc
                              | Pkt _ _ ipc ==> ipc"

lemma msg_sender_simps [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
                          msg_sender (Rreq hops rreqid dip dsn dsk oip osn sip) = sip"
  "∧hops dip dsn oip sip. msg_sender (Rrep hops dip dsn oip sip) = sip"
  "∧dests sip. msg_sender (Rerr dests sip) = sip"
  "∧d dip sip. msg_sender (Pkt d dip sip) = sip"
  unfolding msg_sender_def by simp_all

definition msg_zhops :: "msg ==> bool"
where "msg_zhops m ≡ case m of
                                 Rreq hopsc _ dipc _ _ oipc _ sipc ==> hopsc = 0 ⟶ oipc = sipc
                               | Rrep hopsc dipc _ _ sipc ==> hopsc = 0 ⟶ dipc = sipc
                               | _ ==> True"

lemma msg_zhops_simps [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
           msg_zhops (Rreq hops rreqid dip dsn dsk oip osn sip) = (hops = 0 ⟶ oip = sip)"
  "∧hops dip dsn oip sip. msg_zhops (Rrep hops dip dsn oip sip) = (hops = 0 ⟶ dip = sip)"
  "∧dests sip. msg_zhops (Rerr dests sip) = True"
  "∧d dip. msg_zhops (Newpkt d dip) = True"
  "∧d dip sip. msg_zhops (Pkt d dip sip) = True"
  unfolding msg_zhops_def by simp_all

definition rreq_rrep_sn :: "msg ==> bool"
where "rreq_rrep_sn m ≡ case m of Rreq _ _ _ _ _ _ osnc _ ==> osnc ≥ 1
                                | Rrep _ _ dsnc _ _ ==> dsnc ≥ 1
                                | _ ==> True"

lemma rreq_rrep_sn_simps [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
           rreq_rrep_sn (Rreq hops rreqid dip dsn dsk oip osn sip) = (osn ≥ 1)"
  "∧hops dip dsn oip sip. rreq_rrep_sn (Rrep hops dip dsn oip sip) = (dsn ≥ 1)"
  "∧dests sip. rreq_rrep_sn (Rerr dests sip) = True"
  "∧d dip. rreq_rrep_sn (Newpkt d dip) = True"
  "∧d dip sip. rreq_rrep_sn (Pkt d dip sip) = True"
  unfolding rreq_rrep_sn_def by simp_all

definition rreq_rrep_fresh :: "rt ==> msg ==> bool"
where "rreq_rrep_fresh crt m ≡ case m of Rreq hopsc _ _ _ _ oipc osnc ipcc ==> (ipcc ≠ oipc ⟶
                                                oipc∈kD(crt) ∧ (sqn crt oipc > osnc
                                                                ∨ (sqn crt oipc = osnc
                                                                   ∧ the (dhops crt oipc) ≤ hopsc
                                                                   ∧ the (flag crt oipc) = val)))
                                | Rrep hopsc dipc dsnc _ ipcc ==> (ipcc ≠ dipc ⟶
                                                                    dipc∈kD(crt)
                                                                  ∧ sqn crt dipc = dsnc
                                                                  ∧ the (dhops crt dipc) = hopsc
                                                                  ∧ the (flag crt dipc) = val)
                                | _ ==> True"

lemma rreq_rrep_fresh [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
           rreq_rrep_fresh crt (Rreq hops rreqid dip dsn dsk oip osn sip) =
                               (sip ≠ oip ⟶ oip∈kD(crt)
                                            ∧ (sqn crt oip > osn
                                               ∨ (sqn crt oip = osn
                                                  ∧ the (dhops crt oip) ≤ hops
                                                  ∧ the (flag crt oip) = val)))"
  "∧hops dip dsn oip sip. rreq_rrep_fresh crt (Rrep hops dip dsn oip sip) =
                               (sip ≠ dip ⟶ dip∈kD(crt)
                                              ∧ sqn crt dip = dsn
                                              ∧ the (dhops crt dip) = hops
                                              ∧ the (flag crt dip) = val)"
  "∧dests sip. rreq_rrep_fresh crt (Rerr dests sip) = True"
  "∧d dip. rreq_rrep_fresh crt (Newpkt d dip) = True"
  "∧d dip sip. rreq_rrep_fresh crt (Pkt d dip sip) = True"
  unfolding rreq_rrep_fresh_def by simp_all

definition rerr_invalid :: "rt ==> msg ==> bool"
where "rerr_invalid crt m ≡ case m of Rerr destsc _ ==> (∀ripc∈dom(destsc).
                                            (ripc∈iD(crt) ∧ the (destsc ripc) = sqn crt ripc))
                                | _ ==> True"

lemma rerr_invalid [simp]:
  "∧hops rreqid dip dsn dsk oip osn sip.
                           rerr_invalid crt (Rreq hops rreqid dip dsn dsk oip osn sip) = True"
  "∧hops dip dsn oip sip. rerr_invalid crt (Rrep hops dip dsn oip sip) = True"
  "∧dests sip. rerr_invalid crt (Rerr dests sip) = (∀rip∈dom(dests).
                                                 rip∈iD(crt) ∧ the (dests rip) = sqn crt rip)"
  "∧d dip. rerr_invalid crt (Newpkt d dip) = True"
  "∧d dip sip. rerr_invalid crt (Pkt d dip sip) = True"
  unfolding rerr_invalid_def by simp_all

definition
  initmissing :: "(nat ==> state option) × 'a ==> (nat ==> state) × 'a"
where
  "initmissing σ = (λi. case (fst σ) i of None ==> aodv_init i | Some s ==> s, snd σ)"

lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i ∉ net_ips σ"
    shows "fst (initmissing (netgmap fst σ)) i = aodv_init i"
  using assms unfolding initmissing_def by simp

lemma fst_initmissing_netgmap_pair_fst [simp]:
  "fst (initmissing (netgmap (λ(p, q). (fst (id p), snd (id p), q)) s))
                                               = fst (initmissing (netgmap fst s))"
  unfolding initmissing_def by auto

text ‹We introduce a streamlined alternative to @{term initmissing} with @{term netgmap}
 to simplify invariant statements and thus facilitate their comprehension and
 presentation.›

lemma fst_initmissing_netgmap_default_aodv_init_netlift:
  "fst (initmissing (netgmap fst s)) = default aodv_init (netlift fst s)"
  unfolding initmissing_def default_def
  by (simp add: fst_netgmap_netlift del: One_nat_def)

definition
  netglobal :: "((nat ==> state) ==> bool) ==> ((state × 'b) × 'c) net_state ==> bool"
where
  "netglobal P ≡ (λs. P (default aodv_init (netlift fst s)))"

end