Theory IntegrateAlgorithm

subsection ‹Integration algorithm \label{sec:integrate}›

text ‹In this section we describe the algorithm to integrate a received message into a peers'
  state.›

theory IntegrateAlgorithm
  imports BasicAlgorithms Data
begin

fun fromSome :: "'a option ⇒ error + 'a"
  where
    "fromSome (Some x) = return x" |
    "fromSome None = error (STR ''Expected Some'')"

lemma fromSome_ok_simp [simp]: "(fromSome x = Inr y) = (x = Some y)"
  by (cases x, simp+)

fun substr :: "'a list ⇒ nat ⇒ nat ⇒ 'a list" where
  "substr s l u = take (u - (Suc l)) (drop l s)"

fun concurrent ::
  "('ℐ, 'Σ) woot_character list
  ⇒ nat
  ⇒ nat
  ⇒ ('ℐ, 'Σ) woot_character
  ⇒ error + ('ℐ extended list)"
  where
    "concurrent s l u w =
      do {
        p_pos ← idx s (P w);
        s_pos ← idx s (S w);
        return (if (p_pos ≤ l ∧ s_pos ≥ u) then [⟦I w⟧] else [])
      }"

function integrate_insert
  where
    "integrate_insert m w p s =
      do {
        l ← idx w p;
        u ← idx w s;
        assert (l < u);
        if Suc l = u then
          return ((take l w)@[to_woot_char m]@(drop l w))
        else do {
          d ← mapM (concurrent w l u) (substr w l u);
          assert (concat d ≠ []);
          (p', s') ← fromSome (find ((λx.⟦I m⟧ < x ∨ x = s) ∘ snd) 
                        (zip (p#concat d) (concat d@[s])));
          integrate_insert m w p' s'
        }
      }"
  by fastforce+

fun integrate_delete ::
  "('ℐ :: linorder) delete_message
  ⇒ ('ℐ, 'Σ) woot_character list
  ⇒ error + ('ℐ, 'Σ) woot_character list"
  where
    "integrate_delete (DeleteMessage i) s =
      do {
        k ← idx s ⟦i⟧;
        w ← nth s k;
        list_update s k 
          (case w of (InsertMessage p i u _) ⇒ InsertMessage p i u None)
      }"

fun integrate ::
  "('ℐ, 'Σ) woot_character list
  ⇒ ('ℐ :: linorder, 'Σ) message
  ⇒ error + ('ℐ, 'Σ) woot_character list"
  where
    "integrate s (Insert m) = integrate_insert m s (P m) (S m)" |
    "integrate s (Delete m) = integrate_delete m s"

text ‹Algorithm @{term integrate} describes the main function that is called when a new message
  @{term m} has to be integrated into the state @{term s} of a peer.
  It is called both when @{term m} was generated locally or received from another peer.
  Note that we require that the antecedant messages have already been integrated. See also 
  Section \ref{sec:networkModel} for the delivery assumptions that ensure this requirement.

  Algorithm @{term integrate_delete} describes the procedure to integrate a delete message:
  @{term "DeleteMessage i"}.
  The algorithm just replaces the symbol of the W-character with identifier @{term i} with the value
  @{term "None"}.
  It is not possible to entirely remove a W-character if it is deleted, since there might be 
  unreceived insertion messages that depend on its position.

  Algorithm @{term integrate_insert} describes the procedure to integrate an insert message:
  @{term "m = InsertMessage p i s σ"}.
  Since insertion operations can happen concurrently and the order of message delivery is not fixed,
  it can happen that a remote peer receiving @{term m} finds multiple possible insertion points 
  between the predecessor @{term p} and successor @{term s} that were recorded when the message 
  was generated.
  An example of this situation is the conflict between
  @{term "InsertMessage ⊢ (A,0 :: nat) ⊣ (CHR ''I'')"} and @{term "InsertMessage ⊢ (B,0 :: nat) ⊣ (CHR ''N'')"}
  in Figure~\ref{fig:session}.

  A first attempt to resolve this would be to insert the W-characters by choosing an insertion point
  using the order induced by their identifiers to achieve a consistent ordering.
  But this method fails in some cases: a counter-example was found by 
  Oster et al.~\<^cite>‹‹section 2› in "oster2006data"›.

  The solution introduced by the authors of WOOT is to restrict the identifier comparison to the 
  set of W-characters in the range @{term "substr l u s"} whose predecessor and successor are
  outside of the possible range, i.e. @{text "idx s (P w) ≤ l"} and @{text "idx s (S w) ≥ u"}.

  New narrowed bounds are selected by finding the first W-character within that restricted set 
  with an identifier strictly larger than the identifier of the new W-character.

  This leads to a narrowed range where the found character forms an upper bound and its immediately
  preceeding character the lower bound. The method is applied recursively until the insertion point 
  is uniquely determined.

  Note that the fact that this strategy leads to a consistent ordering has only been verified for a
  bounded model.
  One of the contributions of this paper is to provide a complete proof for it.›

end