Theory Publisher_Subscriber

(*
  Title:      Publisher_Subscriber.thy
  Author:     Diego Marmsoler
*)
section "A Theory of Publisher-Subscriber Architectures"
text‹
  In the following, we formalize the specification of the publisher subscriber pattern as described in~\<^cite>‹"Marmsoler2018c"›.
›
  
theory Publisher_Subscriber
imports Singleton
begin

subsection "Subscriptions"

datatype 'evt subscription = sub 'evt | unsub 'evt

subsection "Publisher-Subscriber Architectures"

locale publisher_subscriber =
  pb: singleton pbactive pbcmp +
  sb: dynamic_component sbcmp sbactive
    for pbactive :: "'pid ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60)
    and pbcmp :: "'pid ⇒ cnf ⇒ 'PB" (‹σ⇘_⇙(_)› [0,110]60)
    and sbactive :: "'sid ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60)
    and sbcmp :: "'sid ⇒ cnf ⇒ 'SB" (‹σ⇘_⇙(_)› [0,110]60) +
  fixes pbsb :: "'PB ⇒ ('evt set) subscription set"
    and pbnt :: "'PB ⇒ ('evt × 'msg)"             
    and sbnt :: "'SB ⇒ ('evt × 'msg) set"
    and sbsb :: "'SB ⇒ ('evt set) subscription"
  assumes conn1: "⋀k pid. ∥pid∥⇘k⇙
      ⟹ pbsb (σ⇘pid⇙(k)) = (⋃sid∈{sid. ∥sid∥⇘k⇙}. {sbsb (σ⇘sid⇙(k))})"
    and conn2: "⋀t n n'' sid pid E e m.
      ⟦t ∈ arch; ∥pid∥⇘t n⇙; ∥sid∥⇘t n⇙; sub E = sbsb (σ⇘sid⇙(t n)); n''≥ n; e ∈ E;
      ∄n' E'. n' ≥ n ∧ n' ≤ n'' ∧ ∥sid∥⇘t n'⇙ ∧
        unsub E' = sbsb (σ⇘sid⇙(t n')) ∧ e ∈ E';
      (e, m) = pbnt (σ⇘pid⇙(t n'')); ∥sid∥⇘t n''⇙⟧
      ⟹ pbnt (σ⇘pid⇙(t n'')) ∈ sbnt (σ⇘sid⇙(t n''))"
begin

subsubsection "Calculus Interpretation"
text ‹
\noindent
@{thm[source] pb.baIA}: @{thm pb.baIA [no_vars]}
›
text ‹
\noindent
@{thm[source] sb.baIA}: @{thm sb.baIA [no_vars]}
›
subsubsection "Results from Singleton"
abbreviation the_pb :: "'pid" where
"the_pb ≡ pb.the_singleton"

text ‹
\noindent
@{thm[source] pb.ts_prop(1)}: @{thm pb.ts_prop(1) [no_vars]}
›
text ‹
\noindent
@{thm[source] pb.ts_prop(2)}: @{thm pb.ts_prop(2) [no_vars]}
›

subsubsection "Architectural Guarantees"
text ‹
  The following theorem ensures that a subscriber indeed receives all messages associated with an event for which he is subscribed.
›
theorem msgDelivery:
  fixes t n n'' and sid::'sid and E e m
  assumes "t ∈ arch"
    and "∥sid∥⇘t n⇙"
    and "sub E = sbsb (σ⇘sid⇙(t n))"
    and "n'' ≥ n"
    and "∄n' E'. n' ≥ n ∧ n' ≤ n'' ∧ ∥sid∥⇘t n'⇙ ∧ unsub E' = sbsb(σ⇘sid⇙(t n'))
          ∧ e ∈ E'"
    and "e ∈ E"
    and "(e,m) = pbnt (σ⇘the_pb⇙(t n''))"
    and "∥sid∥⇘t n''⇙"
  shows "(e,m) ∈ sbnt (σ⇘sid⇙(t n''))"
  using assms conn2 pb.ts_prop(2) by simp

text ‹
  Since a publisher is actually a singleton, we can provide an alternative version of constraint @{thm[source] conn1}.
›
lemma conn1A:
  fixes k
  shows "pbsb (σ⇘the_pb⇙(k)) = (⋃sid∈{sid. ∥sid∥⇘k⇙}. {sbsb (σ⇘sid⇙(k))})"
  using conn1[OF pb.ts_prop(2)] .
end
  
end