Session WOOT_Strong_Eventual_Consistency

Theory ErrorMonad

section ‹Preliminary Notes›

subsection ‹Algorithms in Isabelle›
theory ErrorMonad
  imports
    "Certification_Monads.Error_Monad"
begin

text ‹\noindent Isabelle's functions are mathematical functions and not necessarily algorithms. For
  example, it is possible to define a non-constructible function:›

fun non_constructible_function where
  "non_constructible_function f = (if (n. f n = 0) then 1 else 0)"

text ‹\noindent and even prove properties of them, like for example:

  \begin{center}
  @{lemma "non_constructible_function (λx. (Suc 0)) = (0 :: nat)" by auto}
  \end{center}

  In addition to that, some native functions in Isabelle are under-defined, e.g.,
  @{term "[] ! 1"}. But it is still possible to show lemmas about these undefined values, e.g.:
  @{lemma "[] ! 1 = [a,b] ! 3" by simp}.
  While it is possible to define a notion of algorithm in Isabelle~\cite{klein2018java}, we think
  that this is not necessary for the purpose of this formalization, since the reader needs to verify
  that the formalized functions correctly model the algorithms described by
  Oster et al.~\cite{oster2006data} anyway.
  However, we show that Isabelle can generate code for the functions, indicating that
  non-constructible terms are not being used within the algorithms.›

type_synonym error = String.literal

fun assert :: "bool  error + unit"
  where
    "assert False = error (STR ''Assertion failed.'')" |
    "assert True = return ()"

fun fromSingleton :: "'a list  error + 'a"
  where
    "fromSingleton [] = error (STR ''Expected list of length 1'')" |
    "fromSingleton (x # []) = return x" |
    "fromSingleton (x # y # ys) = error (STR ''Expected list of length 1'')"

text ‹Moreover, we use the error monad---modelled using the @{type sum} type---and
  build wrappers around partially defined Isabelle functions such that the
  evaluation of undefined terms and violation of invariants expected by the
  algorithms result in error values.

  We are able to show that all operations succeed without reaching unexpected states during the
  execution of the framework.›

end

Theory Data

section ‹The WOOT Framework \label{sec:wootFramework}›

theory Data
  imports Main Datatype_Order_Generator.Order_Generator
begin

text ‹%
  \begin{figure}[t]
    \centering
    \begin{tikzpicture}[
      peernode/.style={rectangle, draw=black, thick, scale=0.8},
      eventnode/.style={rectangle, draw=black, fill=black!20, thick,rounded corners=.1cm,
      scale=0.8},
      statenode/.style={rectangle, draw=black, thick,rounded corners=.1cm,
      scale=0.8},
    ]
    % Nodes.
    \node[peernode] (peerA) at (0, 0) {Peer A};
    \node[peernode] (peerB) at (4, 0) {Peer B};
    \node[peernode] (peerC) at (8, 0) {Peer C};
    \node[statenode] (stateA1) at (0, -1) {$[]$};
    \node[statenode] (stateB1) at (4, -1) {$[]$};
    \node[statenode] (stateC1) at (8, -1) {$[]$};
    \node[eventnode] (eventA1) at (0, -2) {\emph{Send} (InsM $\vdash (A,0) \dashv I)$};
    \node[eventnode] (eventB1) at (4, -2) {\emph{Send} (InsM $\vdash (B,0) \dashv N)$};
    \node[eventnode] (eventB2) at (4, -3) {\emph{Recv} $(B,0)$};
        % Lines.
    \node[statenode] (stateB2) at (4, -4) {$[N_{(B,0)}]$};
    \node[eventnode] (eventB3) at (4, -6) {\emph{Recv} $(A,0)$};
        % Lines
    \node[statenode] (stateB3) at (4, -7) {$[I_{(A,0)} N_{(B,0)}]$};
     \node[eventnode] (eventB4) at (4, -8) {\emph{Recv} $(C,1)$};
        % Lines.
    \node[statenode] (stateB4) at (4, -9) {$[I_{(A,0)} N_{(B,0)} K_{(C,1)}]$};
    \node[eventnode] (eventA2) at (0, -3) {\emph{Recv} $(A,0)$};
    \node[statenode] (stateA2) at (0, -4) {$[I_{(A,0)}]$};
    \node[eventnode] (eventA3) at (0, -6) {\emph{Recv} $(B,0)$};
    \node[statenode] (stateA3) at (0, -7) {$[I_{(A,0)}  N_{(B,0)}]$};
    \node[eventnode] (eventA4) at (0, -8) {\emph{Recv} $(C,1)$};
    \node[statenode] (stateA4) at (0, -9) {$[I_{(A,0)} N_{(B,0)} K_{(C,1)}]$};
    \node[eventnode] (eventC1) at (8, -3) {\emph{Recv} $(A,0)$};
    \node[statenode] (stateC2) at (8, -4) {$[I_{(A,0)}]$};
    \node[eventnode] (eventC2) at (8, -5) {\emph{Send} $InsM (A,0)  (C,1) \dashv K$};
    \node[eventnode] (eventC3) at (8, -6) {\emph{Recv} $(C,1)$};
    \node[statenode] (stateC3) at (8, -7) {$[I_{(A,0)} K_{(C,1)}]$};
    \node[eventnode] (eventC4) at (8, -8) {\emph{Recv} $(B,0)$};
    \node[statenode] (stateC4) at (8, -9) {$[I_{(A,0)} N_{(B,0)} K_{(C,1)}]$};
        % Lines.
    \draw[->] (peerA.south) -- (stateA1.north);
    \draw[->] (peerB.south) -- (stateB1.north);
    \draw[->] (peerC.south) -- (stateC1.north);
    \draw[->] (stateA1.south) -- (eventA1.north);
    \draw[->] (eventA1.south) -- (eventA2.north);
    \draw[->] (eventA2.south) -- (stateA2.north);
    \draw[->] (stateA2.south) -- (eventA3.north);
    \draw[->] (eventA3.south) -- (stateA3.north);
    \draw[->] (stateA3.south) -- (eventA4.north);
    \draw[->] (eventA4.south) -- (stateA4.north);
    \draw[->] (stateB1.south) -- (eventB1.north);
    \draw[->] (eventB1.south) -- (eventB2.north);
    \draw[->] (eventB2.south) -- (stateB2.north);
    \draw[->] (stateB2.south) -- (eventB3.north);
    \draw[->] (eventB3.south) -- (stateB3.north);
    \draw[->] (stateB3.south) -- (eventB4.north);
    \draw[->] (eventB4.south) -- (stateB4.north);
    \draw[->] (stateC1.south) -- (eventC1.north);
    \draw[->] (eventC1.south) -- (stateC2.north);
    \draw[->] (stateC2.south) -- (eventC2.north);
    \draw[->] (eventC2.south) -- (eventC3.north);
    \draw[->] (eventC3.south) -- (stateC3.north);
    \draw[->] (stateC3.south) -- (eventC4.north);
    \draw[->] (eventC4.south) -- (stateC4.north);
    \end{tikzpicture}%
    \caption{Example session with 3 peers. Each peer creates an update message and sends a copy of
      it to the other two peers. Each peer integrates the messages in a different order.
    The white rounded boxes represent states, for brevity we only show the W-character's symbol and
    identifier. Although a W-character's data structure stores the identifiers of its predecessor
    and successor from its original creation event. The gray round boxes represent events,
    we abbreviate the reception events, with the identifier of the W-character, although the peer
    receives the full insert message.}%
    \label{fig:session}%
  \end{figure}
  Following the presentation by Oster et al.~\cite{oster2006data} we describe the WOOT framework as
  an operation-based CRDT~\cite{shapiro2011conflict}.

  In WOOT, the shared data type is a string over an alphabet @{text "'Σ"}.
  Each peer starts with a prescribed initial state representing the empty string.
  Users can perform two types of edit operations on the string at their peer:
  \begin{itemize}
    \item Insert a new character.
    \item Delete an existing character.
  \end{itemize}

  Whenever a user performs one of these operations, their peer will create an update message (see
  Section~\ref{sec:edit}), integrate it immediately into its state, and send it to every other peer.

  An update message created at a peer may depend on at most two of the previously integrated
  messages at that peer.
  A message cannot be delivered to a peer if its antecedents have not been delivered to it yet.
  In Section~\ref{sec:networkModel} we describe a few possible methods to implement this
  requirement, as there is a trade-off between causal consistency and scalability.

  Once delivered to a remote peer, an update message will be integrated to the peers' state.
  The integration algorithm for an update message is the same whether the message originated at the
  same or at a different peer (see Section~\ref{sec:integrate}).

  The interaction of the WOOT Framework can be visualized using a space-time
  diagram~\cite{kshemkalyani2011distributed}.
  An example session between 3 peers is shown in Figure~\ref{fig:session}.
  Note that, each peer sees the edit operations in a different order.›

subsection ‹Symbol Identifiers \label{sec:symbolIdentifiers}›

text ‹The WOOT Framework requires a unique identifier for each insert operation, which it keeps
  associated with the inserted symbol.
  The identifier may not be used for another insertion operation on the same or any other peer.
  Moreover the set of identifiers must be endowed with a total linear order.
  We will denote the set of identifiers by @{text "'ℐ :: linorder" }.

  Note that the order on the identifiers is not directly used as a global order over the inserted
  symbols, in contrast to the sort-key based approaches: LSEQ, LOGOOT, or TreeDoc. In particular,
  this means we do not require the identifier space to be dense.

  In the modelling in Section \ref{sec:networkModel}, we will use the pair consisting of a unique
  identifier for the peer and the count of messages integrated or sent by that peer, with the
  lexicographic order induced by the Cartesian product of the peer identifier and the counter.

  It is however possible to use other methods to generate unique identifiers, as long as the above
  requirements are fulfilled.›

subsubsection ‹Extended Identifiers›

datatype 'ℐ extended
  = Begin ("")
  | InString 'ℐ ("(1_)")
  | End ("")
derive linorder extended

text ‹We embed the set of identifiers in an extension containing two additional elements
  denoting the smallest (resp. largest) element of the extension. The order of identifiers with
  respect to each other is preserved. The extended set is used in the corner cases, where a
  W-character is inserted at the beginning or end of the string - and there is no preceeding resp.
  succeeding W-character to reference. See also the following section.›

subsection ‹Messages \label{sec:messages}›

datatype ('ℐ, ) insert_message =
  InsertMessage (P:"'ℐ extended") (I:'ℐ) (S:"'ℐ extended") (Σ:)

datatype 'ℐ delete_message = DeleteMessage 'ℐ

datatype ('ℐ, ) message =
  Insert "('ℐ, ) insert_message" |
  Delete "'ℐ delete_message"

text ‹Two kinds of update messages are exchanged in the WOOT Framework, indicating
  respectively an insertion or a deletion of a character. Thus the set of messages is a sum
  type @{type "message"}.

  An insert message @{term "Insert m"} has the following four components:
  \begin{itemize}
  \item @{term "P m"} and @{term "S m"} denote the identifiers  of the character immediately
     preceding (resp. succeeding) the character at the time of its insertion.
     The special value @{term ""} (resp. @{term ""}) indicates that there
     was no such character, i.e., that it was inserted at the beginning (resp. end) of the string.
  \item @{term "I m"} denotes the unique identifier associated to the character (as described in
     Subsection~\ref{sec:symbolIdentifiers}).
  \item @{term m"} denotes the inserted character.
  \end{itemize}›

subsection ‹States \label{sec:states}›

type_synonym ('ℐ, ) woot_character = "('ℐ,  option) insert_message"

text ‹A W-character @{term "w"} is the representation of an inserted character in the state of a
  peer. It has the same semantics and notation for its components as an insert message, with the
  difference that @{term w"} can be @{term "Some σ"} denoting an inserted character, or
  @{term "None"} if the character has already been deleted.
  Because of this overlap in semantics, we define the type of W-characters as a type synonym.

  The state of a peer is then a string of W-characters
  @{text "s :: ('ℐ, 'Σ) woot_character list"}.
  The initial state is the empty string @{term "[]"}.
  The string the user sees is the sequence of symbols omitting @{term "None"}s, i.e., the sequence:
  @{text "[σ. Some σ ← map Σ s]"}.›

fun to_woot_char :: "('ℐ, ) insert_message  ('ℐ, ) woot_character"
  where
    "to_woot_char (InsertMessage p i s σ) = InsertMessage p i s (Some σ)"

text ‹An insert message can be converted into a W-character by applying @{term Some} to the symbol
  component.›

end

Theory BasicAlgorithms

subsection ‹Basic Algorithms›

theory BasicAlgorithms
  imports Data ErrorMonad
begin

text ‹
  In this section, we introduce preliminary definitions and functions, required by the
  integration and edit algorithms in the following sections.
›

definition ext_ids :: "('ℐ, ) woot_character list  'ℐ extended list"
  where "ext_ids s = #(map (λx.  I x ) s)@[]"

text ‹
  The function @{term ext_ids} returns the set of extended identifiers in a string @{term s},
  including the beginning and end markers @{term ""} and @{term ""}.
›

fun idx :: "('ℐ, ) woot_character list  'ℐ extended  error + nat"
  where
    "idx s i = fromSingleton (filter (λj. (ext_ids s ! j = i)) [0..<(length (ext_ids s))])"

text ‹
  The function @{term idx} returns the index in @{term w} of a W-character with a given identifier
   @{term i}:
  %
  \begin{itemize}
  \item If the identifier @{term i} occurs exactly once in the string then
        @{term "idx s i = return (j+1)"} where @{term "I (s ! j) = i"}, otherwise
        @{term "idx s i"} will be an error.
  \item @{term "idx s  = Inr 0"} and @{term "idx s  = return (length w + 1)"}.
  \end{itemize}
›

fun nth :: "('ℐ, ) woot_character list  nat  error + ('ℐ, ) woot_character"
  where
    "nth s 0 = error (STR ''Index has to be >= 1.'')" |
    "nth s (Suc k) = (
      if k < (length s) then
        return (s ! k)
      else
        error (STR ''Index has to be <= length s''))"

text ‹
  The function @{text nth} returns the W-character at a given index in @{term s}.
  The first character has the index 1.
›

fun list_update ::
  "('ℐ, ) woot_character list  nat  ('ℐ, ) woot_character  
  error + ('ℐ, ) woot_character list"
  where
    "list_update s (Suc k) v = (
        if k < length s then
          return (List.list_update s k v)
        else
          error (STR ''Illegal arguments.''))" |
    "list_update _ 0 _ = error (STR ''Illegal arguments.'')"

text ‹
  The function @{text list_update} substitutes the W-character at the index @{term "k"} in
  @{term s} with the W-character @{term v}. As before, we use the convention of using the index 1
  for the first character.
›

end

Theory CreateAlgorithms

subsection ‹Edit Operations \label{sec:edit}›

theory CreateAlgorithms
  imports BasicAlgorithms
begin

fun is_visible :: "('ℐ, ) woot_character  bool"
  where "is_visible (InsertMessage _ _ _ s) = (s  None)"

fun nth_visible :: "('ℐ, ) woot_character list  nat  error + 'ℐ extended"
  where
    "nth_visible s k = (let v = ext_ids (filter is_visible s) in 
      if k < length v then 
        return (v ! k) 
      else 
        error (STR ''Argument k out of bounds.''))"

text ‹Let @{term l} be the count of visible symbols in @{term s}. The function
  @{term "nth_visible s n"}:
  %
  \begin{itemize}
  \item Returns the identifier of the $n$-th visible element in $s$ if $1 \leq n \leq l$.
  \item Returns @{term } if $n = 0$, and @{term } if $n = l + 1$.
  \item Returns an error otherwise.
  \end{itemize}
  %
  Note that, with this definition, the first visible character in the string has the index $1$.

  Algorithms @{text create_insert} and @{term create_delete} detail the process by which messages
  are created in response to a user action.›

fun from_non_extended :: "'ℐ extended  error + 'ℐ"
  where
    "from_non_extended  i  = Inr i" |
    "from_non_extended _ = error (STR ''Expected InString'')"

fun create_insert :: 
  "('ℐ, ) woot_character list  nat     'ℐ  error + ('ℐ, ) message"
  where "create_insert s n σ' i =
    do {
      p  nth_visible s n;
      q  nth_visible s (n + 1);
      return (Insert (InsertMessage p i q σ'))
    }"

text ‹In particular, when a user inserts a character @{term σ'} between visible position
  @{term n} and its successor of the string of a peer with state @{term s}, @{term create_insert}
  starts by retrieving the identifiers @{term p} of the last visible character before @{term n}
  in @{term w} (or @{term } if no such character exists) and @{text q} of the first
  visible one after @{term n} (or @{term }).

  It then broadcasts the message @{term "Insert (InsertMessage p i q σ')"} with the new
  identifier @{term i}.›

fun create_delete :: "('ℐ, ) woot_character list  nat  error + ('ℐ, ) message"
  where "create_delete s n =
    do {
      m  nth_visible s n;
      i  from_non_extended m;
      return (Delete (DeleteMessage i))
    }"

text ‹When the user deletes the visible character at position @{term n}, @{term create_delete}
  retrieves the identifier @{term i} of the @{term n}'th visible character in @{term s} and
  broadcasts the message @{term "Delete (DeleteMessage i)"}.

  In both cases the message will be integrated into the peer's own state, with the same
  algorithm that integrates messages received from other peers.›

end

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 ::
  "('a, 's) woot_character list
   nat
   nat
   ('a, 's) woot_character
   error + ('a 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 ::
  "('a :: linorder) delete_message
   ('a, 's) woot_character list
   error + ('a, 's) 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 ::
  "('a, 's) woot_character list
   ('a :: linorder, 's) message
   error + ('a, 's) 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]{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

Theory DistributedExecution

subsection ‹Network Model \label{sec:networkModel}›

text ‹In the past subsections, we described the algorithms each peer uses to integrate received
  messages and broadcast new messages when an edit operation has been made on that peer.

  In this section, we model the WOOT Framework as a distributed application and set the
  basis for the consistency properties, we want to establish.

  We assume a finite set of peers starting with the same initial state of an empty W-string, each
  peer reaches a finite set of subsequent states, caused by the integration of received (or locally
  generated messages). A message is always generated from a concrete state of a peer, using the
  algorithms described in Section \ref{sec:edit}. Moreover, we assume that the same message will only
  be delivered once to a peer. Finally, we assume that the happened before relation, formed by
  \begin{itemize}
  \item Subsequent states of the same peer
  \item States following the reception and states that were the generation sites
  \end{itemize}
  do not contain loops. (Equivalently that the transitive closure of the relation is a strict
  partial order.)

  The latter is a standard assumption in the modelling of distributed systems (compare e.g.
  \cite[Chapter 6.1]{raynal2013}) effectively implied by the fact that there are no physical causal
  loops.

  Additionally, we assume that a message will be only received by a peer, when the antecedent
  messages have already been received by the peer. This is a somewhat technical assumption to
  simplify the description of the system. In a practical implementation a peer would buffer the set
  of messages that cannot yet be integrated. Note that this assumption is automatically implied if
  causal delivery is assumed.

  We establish two properties under the above assumptions
  \begin{itemize}
  \item The integration algorithm never fails.
  \item Two peers having received the same set of messages will be in the same state.
  \end{itemize}

  The model assumptions are derived from Gomes et al.\cite{gomes2017verifying} and
  Shapiro et al.\cite{shapiro:inria-00555588} with minor modifications required for WOOT.›

theory DistributedExecution
  imports IntegrateAlgorithm CreateAlgorithms "HOL-Library.Product_Lexorder"
begin

type_synonym 'p event_id = "'p × nat"

datatype ('p,'s) event =
  Send "('p event_id, 's) message" |
  Receive "'p event_id" "('p event_id, 's) message"

text ‹The type variable @{typ "'p"} denotes a unique identifier identifying a peer.
  We model each peer's history as a finite sequence of events, where each event is either
  the reception or broadcast of a message.
  The index of the event in a peer's history and its identifier form a pair uniquely identifying
  an event in a distributed execution of the framework.
  In the case of a reception, @{term "Receive s m"} indicated the reception of the message @{term m}
  sent at event @{term "s"}.

  In the following we introduce the locale @{text "dist_execution_preliminary"} from which the
  @{text "dist_execution"} locale will inherit. The reason for the introduction of two
  locales is technical - in particular, it is not possible to interleave definitions and assumptions
  within the definition of a locale. The preliminary locale only introduces the assumption that the
  set of participating peers is finite.›

locale dist_execution_preliminary =
  fixes events :: "('p :: linorder)  ('p,'s) event list"
  ― ‹We introduce a locale fixing the sequence of events per peer.›

  assumes fin_peers: "finite (UNIV :: 'p set)"
  ― ‹We are assuming a finite set of peers.›

begin

fun is_valid_event_id
  where "is_valid_event_id (i,j) = (j < length (events i))"

fun event_pred
  where "event_pred (i,j) p  = (is_valid_event_id (i,j)  p (events i ! j))"

fun event_at
  where "event_at i m = event_pred i ((=) m)"

fun is_reception
  where
    "is_reception i j = event_pred j (λe. case e of Receive s _  s = i | _  False)"

fun happened_immediately_before where
  "happened_immediately_before i j = (
     is_valid_event_id i 
     is_valid_event_id j 
     ((fst i = fst j  Suc (snd i) = snd j)  is_reception i j))"

text ‹
  The @{term happened_immediately_before} describes immediate causal precedence:
  \begin{itemize}
    \item An events causally precedes the following event on the same peer.
    \item A message broadcast event causally precedes the reception event of it.
  \end{itemize}

  The transitive closure of this relation is the famous happened before relation introduced
  by Lamport\cite{Lamport1978}.

  In the @{text "dist_execution"} we will assume that the relation is acyclic - which implies that
  the transitive closure @{term "happened_immediately_before++"} is a strict partial
  order.
›

text ‹Each peer passes through a sequence of states, which may change after receiving a message.
  We denote the initial state of peer $p$ as $(p,0)$ and the state after
  event $(p,i)$ as $(p,i+1)$. Note that there is one more state per peer than events, since we
  are count both the initial and terminal state of a peer.›

fun is_valid_state_id
  where "is_valid_state_id (i,j) = (j  length (events i))"

fun received_messages
  where
    "received_messages (i,j) = [m. (Receive _ m)  (take j (events i))]"

fun state where "state i = foldM integrate [] (received_messages i)"

text ‹Everytime a peer receives a message its state is updated by integrating the message. The
  function @{term state} returns the state for a given state id.›

end

text ‹ The function @{text deps} computes the identifiers a message depends on. ›

fun extended_to_set :: "'a extended  'a set"
  where
    "extended_to_set i = {i}" |
    "extended_to_set _ = {}"

fun deps :: "('id, 's) message  'id set"
  where
    "deps (Insert (InsertMessage l _ u _)) = extended_to_set l  extended_to_set u" |
    "deps (Delete (DeleteMessage i)) = {i}"

locale dist_execution = dist_execution_preliminary +
  assumes no_data_corruption:
    "i s m. event_at i (Receive s m)  event_at s (Send m)"
  ― ‹A received message must also have been actually broadcast. Note that, we do not
  assume that a broadcast message will be received by all peers, similar to the modelling made by
  \cite[Section 5.2]{gomes2017verifying}.›

  assumes at_most_once:
    "i j s m.
    event_at i (Receive s m) 
    event_at j (Receive s m) 
    fst i = fst j  i = j"
  ― ‹A peer will never receive the same message twice. Note that this is something
  that can be easily implemented in the application layer, if the underlying transport mechanism
  does not guarantee it.›

  assumes acyclic_happened_before:
    "acyclicP happened_immediately_before"
  ― ‹The immediate causal precendence relation is acyclic, which implies that its
  closure, the \emph{happened before} relation is a strict partial order.›

  assumes semantic_causal_delivery:
    "m s i j i'. event_at (i,j) (Receive s m)  i'  deps m 
      s' j' m'. event_at (i,j') (Receive s' (Insert m'))  j' < j  I m' = i'"
  ― ‹A message will only be delivered to a peer, if its
  antecedents have already been delivered. (See beginning of this Section for the reason of this
  assumption).›

  assumes send_correct:
    "m i. event_at i (Send m) 
    (n σ. return m = state i  (λs. create_insert s n σ i)) 
    (n. return m = state i  (λs. create_delete s n))"
  ― ‹A peer broadcasts messages by running the @{term create_insert} or @{term create_delete}
     algorithm on its current state. In the case of an insertion the new character is assigned
     the event id as its identifier. Note that, it would be possible to assume, a different choice
     for allocating unique identifiers to new W-characters. We choose the event id since it is
     automatically unique.›

begin

text ‹Based on the assumptions above we show in Section \ref{sec:strong_eventual_consistency}:
  \begin{itemize}
    \item \emph{Progress}: All reached states @{term "state i"} will be successful, i.e., the
          algorithm @{term integrate} terminates and does not fail.
    \item \emph{Strong Eventual Consistency}: Any pair of states  @{term "state i"}
          and @{term "state j"} which have been reached after receiving the same set of messages,
          i.e., @{term "set (received_messages i) = set (received_messages j)"} will be equal.
  \end{itemize}›

end

end

Theory SortKeys

section ‹Formalized Proof \label{sec:proof}›

theory SortKeys
  imports Data "HOL-Library.List_Lexorder" "HOL-Library.Product_Lexorder"
begin

datatype sort_dir =
  Left |
  Right
derive linorder sort_dir

lemma sort_dir_less_def [simp]: "(x < y) = (x = Left  y = Right)" 
  by (cases x, case_tac [!] y, simp_all add:less_sort_dir_def)

datatype 'a sort_key = 
  NonFinal "('a × sort_dir)" "'a sort_key" | 
  Final 'a

type_synonym 'id position = "'id sort_key extended"

fun embed_dir where "embed_dir (x,Left) = (x, 0)" | "embed_dir (x,Right) = (x, Suc (Suc 0))"

lemma embed_dir_inj [simp]: "(embed_dir x = embed_dir y) = (x = y)"
  by (cases x, cases y, case_tac [!] "snd x", case_tac [!] "snd y", simp+)

lemma embed_dir_mono [simp]: "(embed_dir x < embed_dir y) = (x < y)"
  by (cases x, cases y, case_tac [!] "snd x", case_tac [!] "snd y", (simp add:less_sort_dir_def)+)

fun sort_key_embedding :: "'a sort_key  ('a × nat) list"
  where 
   "sort_key_embedding (NonFinal x y) = embed_dir x#(sort_key_embedding y)" |
   "sort_key_embedding (Final i) = [(i, Suc 0)]" 

lemma sort_key_embedding_injective: 
  "sort_key_embedding x = sort_key_embedding y  x = y"
  apply (induct x arbitrary: y)
  apply (metis embed_dir_inj list.distinct(1) list.inject sort_key.exhaust
      sort_key_embedding.simps)
  by (metis fst_conv list.distinct(1) list.inject sort_key.exhaust
      sort_key_embedding.simps)

instantiation sort_key :: (ord) ord
begin
definition sort_key_less_eq_def [simp]: 
  "(x :: ('a :: ord) sort_key)  y  
    (sort_key_embedding x  sort_key_embedding y)"

definition sort_key_less_def [simp]: 
  "(x :: ('a :: ord) sort_key) < y  
    (sort_key_embedding x < sort_key_embedding y)"

instance ..
end

instantiation sort_key :: (order) order
begin
instance by (intro_classes, simp_all add: less_le_not_le sort_key_embedding_injective)
end

instantiation sort_key :: (linorder) linorder
begin
instance by (intro_classes, meson less_imp_le not_le sort_key_less_eq_def)
end

end

Theory Psi

subsection ‹Definition of \texorpdfstring{$\Psi$}{Psi}\label{sec:psi}›

theory Psi
  imports SortKeys "HOL-Eisbach.Eisbach"
begin

fun extended_size :: "('a sort_key) extended  nat"
  where
    "extended_size x = size x" |
    "extended_size _ = 0"

lemma extended_simps [simp]:
  "( < x) = (x  )"
  "(x' < y') = (x' < y')"
  "x' < "
  "¬(x' < )"
  "¬( < x)"
  "  x"
  "(x'  y') = ((x' :: 'a :: linorder)  y')"
  "x  "
  "¬(x'  )"
  "(  x) = (x = )"
  by (case_tac [!] x, simp_all add:less_extended_def less_eq_extended_def le_less)

fun int_size where "int_size (l,u) = max (extended_size l) (extended_size u)"

lemma position_cases:
  assumes " y z. x = NonFinal (y,Left) z  p"
  assumes " y z. x = NonFinal (y,Right) z  p"
  assumes " y. x = Final y  p"
  assumes "x =   p"
  assumes "x =   p"
  shows "p"
  by (metis assms embed_dir.cases extended_size.cases sort_key_embedding.cases)

fun derive_pos ::
  "('a :: linorder) × sort_dir  'a sort_key extended  'a sort_key extended"
  where
    "derive_pos h NonFinal x y = 
      (if h < x then  else (if x < h then  else y))" |
    "derive_pos h Final x = 
      (if fst h < x  fst h = x  snd h = Left then  else )" |
    "derive_pos _  = " |
    "derive_pos _  = "

lemma derive_pos_mono: "x  y  derive_pos h x  derive_pos h y"
  apply (cases h, cases "snd h")
  apply (rule_tac [!] position_cases [where x=x])
  apply (rule_tac [!] position_cases [where x=y])
  by (simp_all, auto)

fun γ :: "('a :: linorder) position  sort_dir  'a × sort_dir"
  where
    "γ NonFinal x y _ = x" |
    "γ Final x d = (x,d)" |
    "γ  _ = undefined" |
    "γ  _ = undefined"

fun derive_left  where
  "derive_left (l, u) = (derive_pos (γ l Right) l, derive_pos (γ l Right) u)"

fun derive_right where
  "derive_right (l, u) = (derive_pos (γ u Left) l, derive_pos (γ u Left) u)"

fun is_interval where "is_interval (l,u) = (l < u)"

fun elem where "elem x (l,u) = (l < x  x < u)"

fun subset where "subset (l,u) (l',u') = (l'  l  u  u')"

method interval_split for x :: "('a :: linorder) position × 'a position" = 
  (case_tac [!] x, 
   rule_tac [!] position_cases [where x="fst x"], 
   rule_tac [!] position_cases [where x="snd x"])

lemma derive_size:
  "Final i  fst x  is_interval x  int_size (derive_left x) < int_size x" 
  "snd x  Final i  is_interval x  int_size (derive_right x) < int_size x"
  by (interval_split x, simp_all add:less_SucI)

lemma derive_interval:
  "Final i  fst x  is_interval x  is_interval (derive_left x)"
  "snd x  Final i  is_interval x  is_interval (derive_right x)"
  by (interval_split x, simp_all, auto)

function Ψ :: "('a :: linorder) position × 'a position  'a  'a sort_key"
  where
    "Ψ (l,u) i = Final i"
      if "l < Final i  Final i < u" |
    "Ψ (l,u) i = NonFinal (γ l Right) (Ψ (derive_left (l,u)) i)" 
      if "Final i  l  l < u" |
    "Ψ (l,u) i = NonFinal (γ u Left) (Ψ (derive_right (l,u)) i)" 
      if "u  Final i  l < u" |
    "Ψ (l,u) i = undefined" if "u  l"
  by (metis leI old.prod.exhaust, auto)

termination
  apply (relation "measure (λ(p,i). int_size p)", simp)
  using derive_size by fastforce+

proposition psi_elem: "is_interval x  elem Ψ x i x"
proof (induct "int_size x" arbitrary:x rule: nat_less_induct)
  case 1
  consider (a) "Final i  fst x" | (b) "elem Final i x" | (c) "snd x  Final i"
    using not_le by (metis elem.simps prod.collapse)
  then show ?case
  proof (cases)
    case a
    hence "elem  Ψ (derive_left x) i (derive_left x)"
      by (metis 1 derive_size(1) derive_interval(1))
    then show ?thesis using a "1"(2)
      by (interval_split x, simp_all del:Ψ.simps, auto)
  next
    case b
    then show ?thesis by (cases x, simp)
  next
    case c 
    hence "elem  Ψ (derive_right x) i (derive_right x)"
      by (metis 1 derive_size(2) derive_interval(2))
    then show ?thesis using c "1"(2)
      by (interval_split x, simp_all del:Ψ.simps, auto)
  qed
qed

proposition psi_mono:
  assumes "i1 < i2"
  shows "is_interval x  Ψ x i1 < Ψ x i2"
proof (induct "int_size x" arbitrary:x rule: nat_less_induct)
  case 1
  have a:"Final i1 < Final i2"
    using assms by auto
  then consider 
    (a) "Final i1  fst x  Final i2  fst x" | 
    (b) "Final i1  fst x  elem Final i2 x" | 
    (c) "Final i1  fst x  snd x  Final i2" |
    (d) "elem Final i1 x   elem Final i2 x" |
    (e) "elem Final i1 x  snd x  Final i2" |
    (f) "snd x  Final i2  snd x  Final i1" 
    using assms "1"(2) apply (cases x) 
    by (metis (mono_tags, hide_lams) dual_order.strict_trans elem.simps
        fst_conv leI snd_conv)
  then show ?case
  proof (cases)
    case a
    hence (derive_left x) i1  < Ψ (derive_left x) i2"
      by (metis 1 derive_size(1) derive_interval(1))
    thus ?thesis using a "1"(2) by (cases x, simp)
  next
    case b
    thus ?thesis using "1"(2) apply (cases x, simp) 
      by (rule_tac [!] position_cases [where x="fst x"], simp_all)
  next
    case c
    show ?thesis
    proof (cases (fst x) Right = γ (snd x) Left")
      case True 
      have e:"is_interval (derive_left x)" using c "1"(2) derive_interval(1) by blast
      have f:"derive_left x = derive_right x" using True by (cases x, simp)
      have h:(derive_left x) i1 < Ψ (derive_right x) i2"
        apply (cases x, simp only: f) 
        by (metis "1.hyps" "1.prems" c derive_size(2) e f)
      show ?thesis using c "1"(2) h True by (cases x, simp)
    next
      case False
      hence (fst x) Right < γ (snd x) Left" using "1"(2) c
      by (interval_split x, simp_all, auto)
      then show ?thesis using c "1"(2) by (cases x, simp)
    qed
  next
    case d
    thus ?thesis using "1"(2) a by (cases x, simp)
  next
    case e
    thus ?thesis using "1"(2) apply (cases x, simp) 
      by (rule_tac [!] position_cases [where x="snd x"], simp_all del:Ψ.simps)
  next
    case f
    hence b:(derive_right x) i1  < Ψ (derive_right x) i2" 
      by (metis 1 derive_size(2) derive_interval(2))
    thus ?thesis using f "1"(2) by (cases x, simp)
  qed
qed

proposition psi_narrow:
  "elem Ψ x' i x  subset x x'  Ψ x' i = Ψ x i" 
proof (induct "int_size x'" arbitrary: x x' rule: nat_less_induct)
  case 1
  have a: "is_interval x" using "1"(2)
    by (metis dual_order.strict_trans elem.elims(2) is_interval.simps)
  have d: "is_interval x'" using a "1"(3) apply (cases x', cases x, simp) by auto
  consider
    (before) "Final i  fst x'" |
    (between) "elem Final i x'" | 
    (after) "snd x'  Final i" using 1 apply simp
    by (metis elem.simps leI prod.collapse)
  then show ?case
  proof (cases)
    case before
    have b: "Final i  fst x" using before 1 apply (cases x)
      by (metis dual_order.trans fst_conv subset.elims(2))
    obtain z where z_def: x' i = NonFinal (γ (fst x') Right) z" 
      using before d apply (cases x') by simp
    have c:(fst x') Right = γ (fst x) Right"
      using "1"(3) z_def "1"(2) apply (cases x, cases x', simp)
      apply (rule_tac [!] position_cases [where x="fst x"])
      apply (rule_tac [!] position_cases [where x="fst x'"])
      using before by (simp_all del:Ψ.simps, auto)
    have c1:"subset (derive_left x) (derive_left x')"
      using c "1"(3) by (cases x, cases x', simp add:derive_pos_mono)
    have g:"z = Ψ (derive_left x') i" using z_def before d by (cases x', simp)
    have "elem NonFinal (γ (fst x) Right) z x" 
      using "1"(2) z_def by (simp add: c)
    hence "elem z (derive_left x)" using before b
      by (interval_split x, simp_all del:Ψ.simps, auto)
    hence (derive_left x') i = Ψ (derive_left x) i"
      using "1"(1) before d c1 apply (simp only:g)
      by (metis (no_types) derive_size(1))
    thus ?thesis using before b a d c by (cases x, cases x', simp)
  next
    case between
    thus ?thesis using 1 by (cases x, cases x', auto) 
  next
    case after
    have b: "snd x  Final i" using after 1 apply (cases x) 
      by (metis (mono_tags, hide_lams) dual_order.trans prod.exhaust_sel
          subset.simps)
    obtain z where z_def:x' i = NonFinal (γ (snd x') Left) z" 
      using after d by (cases x', simp)
    have c:(snd x') Left = γ (snd x) Left"
      using "1"(3) z_def "1"(2) apply (simp, cases x, cases x')
      apply (rule_tac [!] position_cases [where x="snd x"])
      apply (rule_tac [!] position_cases [where x="snd x'"]) using after
      by (simp_all del:Ψ.simps, auto)
    have c1:"subset (derive_right x) (derive_right x')"
      using c "1"(3) by (cases x, cases x', simp add:derive_pos_mono)
    have g:"z = Ψ (derive_right x') i" using z_def after d by (cases x', simp)
    have "elem NonFinal (γ (snd x) Left) z x" 
      using "1"(2) z_def by (simp add: c)
    hence "elem z (derive_right x)" using after b
      by (interval_split x, simp_all del:Ψ.simps, auto)
    hence (derive_right x') i = Ψ (derive_right x) i"
      using "1"(1) after d c1 apply (simp only:g)   
      by (metis (no_types) derive_size(2))
    thus ?thesis using after b a d c by (cases x, cases x', simp)
  qed
qed

definition preserve_order :: "'a :: linorder  'a  'b :: linorder  'b  bool"
  where "preserve_order x y u v  (x < y  u < v)  (x > y  u > v)"

proposition psi_preserve_order:
  fixes l l' u u' i i'
  assumes "elem Ψ (l, u) i (l',u')"
  assumes "elem Ψ (l', u') i' (l, u)"
  shows "preserve_order i i' Ψ (l,u) i Ψ (l', u') i'"
proof -
  have "l < u" using assms(2) by auto
  hence a:"elem Ψ (l, u) i (max l l', min u u')"
    using assms(1) psi_elem by fastforce
  hence b:(l,u) i = Ψ (max l l', min u u') i"
    by (simp add: psi_narrow)
  have "l' < u'" using assms(1) by auto
  hence "elem Ψ (l',u') i' (max l l', min u u')"
    using assms(2) psi_elem by fastforce
  hence c:(l',u') i' = Ψ (max l l', min u u') i'"
    by (simp add: psi_narrow)
  hence "max l l' < min u u'" using a min_def by auto
  then show ?thesis apply (simp only: preserve_order_def b c)
    using psi_mono extended_simps(2) is_interval.simps by blast
qed

end

Theory Sorting

subsection ‹Sorting›

text ‹Some preliminary lemmas about sorting.›

theory Sorting
  imports Main "HOL.List" "HOL-Library.Sublist"
begin

lemma insort:
  assumes "Suc l < length s"
  assumes "s ! l < (v :: 'a :: linorder)"
  assumes "s ! (l+1) > v"
  assumes "sorted_wrt (<) s"
  shows "sorted_wrt (<) ((take (Suc l) s)@v#(drop (Suc l) s))"
proof -
  have "sorted_wrt (<) (take (Suc l) s@(drop (Suc l) s))"
    using assms(4) by simp
  moreover have
    "x. x  set (take (Suc l) s) = (i. i < (Suc l)  i < length s  s ! i = x)" 
    by (metis in_set_conv_nth length_take min_less_iff_conj nth_take)
  hence "x. x  set (take (Suc l) s)  x < v"
    using assms apply (simp) 
    using less_Suc_eq sorted_wrt_nth_less by fastforce
  moreover have
    "x. x  set (drop (Suc l) s) = (i. Suc l + i < length s  s ! (Suc l + i) = x)"
    using assms(1) by (simp add:in_set_conv_nth add.commute less_diff_conv)
  hence "x. x  set (drop (Suc l) s)  x > v"
    using assms apply (simp) 
    by (metis add.right_neutral add_diff_cancel_left' diff_Suc_Suc diff_is_0_eq'
        leI le_less_trans less_imp_le sorted_wrt_iff_nth_less)
  ultimately show ?thesis
    by (simp add:sorted_wrt_append del:append_take_drop_id)
qed

lemma sorted_wrt_irrefl_distinct:
  assumes "irreflp r"
  shows "sorted_wrt r xs  distinct xs"
  using assms by (induction xs, simp, simp, meson irreflp_def)

lemma sort_set_unique_h:
  assumes "irreflp r  transp r"
  assumes "set (x#xs) = set (y#ys)" 
  assumes "z  set xs. r x z" 
  assumes "z  set ys. r y z" 
  shows "x = y  set xs = set ys"
  by (metis assms insert_eq_iff irreflp_def list.set_intros(1)
      list.simps(15) set_ConsD transpD)

lemma sort_set_unique_rel:
  assumes "irreflp r  transp r"
  assumes "set x = set y"
  assumes "sorted_wrt r x"
  assumes "sorted_wrt r y"
  shows "x = y"
proof -
  have "length x = length y" 
    using assms by (metis sorted_wrt_irrefl_distinct distinct_card)
  then show ?thesis using assms 
    apply(induct rule:list_induct2, simp, simp)
    by (metis assms(1) list.simps(15) sort_set_unique_h) 
qed

lemma sort_set_unique:
  assumes "set x = set y"
  assumes "sorted_wrt (<) (map (f :: ('a  ('b :: linorder)))  x)"
  assumes "sorted_wrt (<) (map f y)"
  shows "x = y"
  using assms apply (simp add:sorted_wrt_map) 
  by (metis (no_types, lifting) irreflp_def less_irrefl sort_set_unique_rel 
      transpD transpI transp_less)

text ‹If two sequences contain the same element and strictly increasing with respect.›

lemma subseq_imp_sorted:
  assumes "subseq s t"
  assumes "sorted_wrt p t"
  shows "sorted_wrt p s"
proof -
  have "sorted_wrt p s  ¬ sorted_wrt p t"
  apply (rule list_emb.induct[where P="(=)"])
  using list_emb_set assms by fastforce+
  thus ?thesis using assms by blast
qed

text ‹If a sequence @{text t} is sorted with respect to a relation @{text p} then a subsequence will 
  be as well.›

fun to_ord where "to_ord r x y = (¬(r** y x))"

lemma trancl_idemp: "r++++ x y = r++ x y" 
  by (metis r_into_rtranclp reflclp_tranclp rtranclp_idemp rtranclp_reflclp 
      rtranclp_tranclp_tranclp tranclp.cases tranclp.r_into_trancl)

lemma top_sort:
  fixes rp
  assumes "acyclicP r"
  shows "finite s  (l. set l = s  sorted_wrt (to_ord r) l  distinct l)"
proof (induction "card s" arbitrary:s)
  case 0
  then show ?case by auto
next
  case (Suc n)
  hence "s  {}" by auto
  moreover 
  have "acyclicP (r++)" using assms
    by (simp add:acyclic_def trancl_def trancl_idemp)
  hence "acyclic ({(x,y). r++ x y}  s × s)"
    by (meson acyclic_subset inf_le1)
  hence "wf ({(x,y). r++ x y}  s × s)" using Suc 
    by (metis card.infinite finite_Int finite_SigmaI nat.distinct(1) 
        wf_iff_acyclic_if_finite)
  ultimately obtain z where 
    "z  s  (y. (y, z)   ({(x,y). r++ x y}  s × s)  y  s)" 
    by (metis ex_in_conv wf_eq_minimal)
  hence z_def: "z  s  (y. r++ y z  y  s)" by blast
  hence "card (s - {z}) = n"
    by (metis One_nat_def Suc.hyps(2) card_Diff_singleton_if card.infinite 
        diff_Suc_Suc diff_zero nat.simps(3))
  then obtain l where l_def: 
    "set l = s - {z}  sorted_wrt (to_ord r) l  distinct l" 
    by (metis Zero_not_Suc card.infinite finite_Diff Suc)
  hence "set (z#l) = s" using z_def by auto
  moreover have "y  set l. ¬(r** y z)" using z_def l_def rtranclpD by force
  ultimately show ?case 
    by (metis distinct.simps(2) insert_absorb l_def list.simps(15) 
        sorted_wrt.simps(2) to_ord.elims(3))
qed

lemma top_sort_eff:
  assumes "irreflp p++"
  assumes "sorted_wrt (to_ord p) x" 
  assumes "i < length x"
  assumes "j < length x"
  assumes "(p++ (x ! i) (x ! j))"
  shows "i < j"
  using assms apply (cases "i > j")
   apply (metis sorted_wrt_nth_less r_into_rtranclp reflclp_tranclp
          rtranclp_idemp rtranclp_reflclp to_ord.simps)
  by (metis irreflp_def nat_neq_iff)

end

Theory Consistency

subsection ‹Consistency of sets of WOOT Messages \label{sec:consistency}›

theory Consistency
  imports SortKeys Psi Sorting DistributedExecution
begin

definition insert_messages :: "('ℐ, ) message set  ('ℐ, ) insert_message set"
  where "insert_messages M = {x. Insert x  M}"

lemma insert_insert_message: 
  "insert_messages (M  {Insert m}) = insert_messages M  {m}"
  by (simp add:insert_messages_def, simp add:set_eq_iff)

definition delete_messages :: "('a, 's) message set  'a delete_message set"
  where "delete_messages M = {x. Delete x  M}"

fun depends_on where "depends_on M x y = (x  M  y  M  I x  deps (Insert y))"

definition a_conditions ::
  "(('a :: linorder), 's) insert_message set  ('a extended  'a position)  bool"
  where "a_conditions M a = (
    a  < a  
    (m. m  M  a (P m) < a (S m) 
                   a I m = Ψ (a (P m), a (S m)) (I m)))"

definition consistent :: "('a :: linorder, 's) message set  bool"
  where "consistent M 
    inj_on I (insert_messages M) 
    ( (deps ` M)  (I ` insert_messages M)) 
    wfP (depends_on (insert_messages M)) 
    (a. a_conditions (insert_messages M) a)"

lemma consistent_subset:
  assumes "consistent N"
  assumes "M  N"
  assumes " (deps ` M)  (I ` insert_messages M)"
  shows "consistent M"
proof -
  have a:"insert_messages M  insert_messages N"
    using assms(2) insert_messages_def by blast
  hence b:"inj_on I (insert_messages M)"
    using assms(1) consistent_def inj_on_subset by blast
  have "wfP (depends_on (insert_messages N))"
    using assms(1) consistent_def by blast
  moreover have 
    "depends_on (insert_messages M)  depends_on (insert_messages N)" 
    using a by auto
  ultimately have c:"wfP (depends_on (insert_messages M))"
    using a wf_subset [to_pred] by blast
  obtain a where "a_conditions (insert_messages N) a"
    using assms(1) consistent_def by blast
  hence "a_conditions (insert_messages M) a"
    by (meson a a_conditions_def subset_iff)
  thus ?thesis using b c assms(3) consistent_def by blast
qed

lemma pred_is_dep: "P m =  i   i  deps (Insert m)"
  by (metis Un_iff deps.simps(1) extended.set_intros extended.simps(27)
      extended_to_set.simps(1) insert_message.exhaust_sel)

lemma succ_is_dep: "S m =  i   i  deps (Insert m)"
  by (metis Un_insert_right deps.simps(1) extended_to_set.simps(1) insertI1
      insert_message.exhaust_sel)

lemma a_subset:
  fixes M N a
  assumes "M  N"
  assumes "a_conditions (insert_messages N) a"
  shows "a_conditions (insert_messages M) a"
  using assms by (simp add:a_conditions_def insert_messages_def, blast)

definition delete_maybe :: "'ℐ   ('ℐ, ) message set      option" where 
  "delete_maybe i D s = (if Delete (DeleteMessage i)  D then None else Some s)"

definition to_woot_character ::
  "('ℐ, ) message set  ('ℐ, ) insert_message  ('ℐ, ) woot_character"
  where
    "to_woot_character D m = (
       case m of
         (InsertMessage l i u s)  InsertMessage l i u (delete_maybe i D s))"

lemma to_woot_character_keeps_i [simp]: "I (to_woot_character M m) = I m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_keeps_i_lifted [simp]: 
  "I ` to_woot_character M ` X = I ` X"
  by (metis (no_types, lifting) image_cong image_image to_woot_character_keeps_i)

lemma to_woot_character_keeps_P [simp]: "P (to_woot_character M m) = P m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_keeps_S [simp]: "S (to_woot_character M m) = S m"
  by (cases m, simp add:to_woot_character_def)

lemma to_woot_character_insert_no_eff:
  "to_woot_character (insert (Insert m) M) = to_woot_character M"
  by (rule HOL.ext, simp add:delete_maybe_def to_woot_character_def insert_message.case_eq_if)

definition is_associated_string ::
  "('a, 's) message set  ('a :: linorder, 's) woot_character list  bool"
  where "is_associated_string M s  (
    consistent M 
    set s = to_woot_character M ` (insert_messages M) 
    (a. a_conditions (insert_messages M) a  
         sorted_wrt (<) (map a (ext_ids s))))"

fun is_certified_associated_string where
  "is_certified_associated_string M (Inr v) = is_associated_string M v" |
  "is_certified_associated_string M (Inl _) = False"

lemma associated_string_unique:
  assumes "is_associated_string M s"
  assumes "is_associated_string M t"
  shows "s = t"
  using assms
  apply (simp add:ext_ids_def is_associated_string_def consistent_def
         sorted_wrt_append)
  by (metis sort_set_unique)

lemma is_certified_associated_string_unique:
  assumes "is_certified_associated_string M s"
  assumes "is_certified_associated_string M t"
  shows "s = t"
  using assms by (case_tac s, case_tac [!] t, (simp add:associated_string_unique)+)

lemma empty_consistent: "consistent {}"
proof -
  have "a_conditions {} (λx. (case x of    |   ))"
    by (simp add: a_conditions_def)
  hence "f. a_conditions {} f" by blast
  moreover have "wfP (depends_on {})" by (simp add: wfP_eq_minimal)
  ultimately show ?thesis by (simp add:consistent_def insert_messages_def)
qed

lemma empty_associated: "is_associated_string {} []"
  by (simp add:is_associated_string_def insert_messages_def empty_consistent 
      ext_ids_def a_conditions_def)

text ‹The empty set of messages is consistent and the associated string is the empty string.›

end

Theory CreateConsistent

subsection ‹Create Consistent\label{sec:create_consistent}›

theory CreateConsistent
  imports CreateAlgorithms Consistency
begin

lemma nth_visible_inc':
  assumes "sorted_wrt (<) (map a (ext_ids s))"
  assumes "nth_visible s n = Inr i"
  assumes "nth_visible s (Suc n) = Inr j"
  shows "a i < a j" 
proof -
  have "subseq (ext_ids (filter is_visible s)) (ext_ids s)" 
    by (simp add: ext_ids_def subseq_map)
  hence "sorted_wrt (<) (map a (ext_ids (filter is_visible s)))"
    using assms(1) subseq_imp_sorted sorted_wrt_map by blast
  moreover have a:"Suc n < length (ext_ids (filter is_visible s))" 
    apply (rule classical) using assms(3) by simp
  ultimately show ?thesis using assms(2) assms(3) apply (simp) 
    using sorted_wrt_nth_less by fastforce
qed

lemma nth_visible_eff:
  assumes "nth_visible s n = Inr i"
  shows "extended_to_set i  I ` set s"
proof -
  have "i  set (ext_ids (filter is_visible s))"
    apply (cases "n < length (ext_ids (filter is_visible s))")
    using assms by auto
  thus ?thesis  
    apply (simp add: ext_ids_def) 
    using extended.inject by auto
qed

lemma subset_mono:
  assumes "N  M"
  shows "I ` insert_messages N  I ` insert_messages M"
proof -
  have "insert_messages N  insert_messages M" using assms
    by (metis (no_types, lifting) Collect_mono_iff insert_messages_def subsetCE)
  thus ?thesis by (simp add: image_mono)
qed

lemma deps_insert:
  assumes " (deps ` M)  (I ` insert_messages M)"
  assumes "deps m  I ` insert_messages M"
  shows " (deps ` (M  {m}))  (I ` insert_messages (M  {m}))"
proof -
  have "deps m  I ` insert_messages (M  {m})" using assms(2) subset_mono
    by (metis Un_upper1 order_trans)
  thus ?thesis using assms(1) apply (simp) 
    by (meson rev_subsetD subsetI subset_insertI subset_mono)
qed

lemma wf_add:
  fixes m :: "('a,'b) insert_message"
  assumes "wfP (depends_on M)"
  assumes "n. n  (M  {m})  I m  deps (Insert n)"
  assumes "m  M"
  shows "wfP (depends_on (M  {m}))" 
proof -
  have "Q. Q  {}  (zQ. y. (y  M  {m})  (z  M  {m}) 
           I y  deps (Insert z)  y  Q)"
  proof -
    fix Q :: "('a, 'b) insert_message set"
    assume b:"Q  {}"
    show "zQ. y. (y  M  {m})  (z  M  {m})  I y  deps (Insert z)
            y  Q"
    proof (cases "x. x  Q - {m}")
      case True
      hence "z Q - {m}. y. (y  M)  (z  M)  I y  deps (Insert z)
              y  Q - {m}"
        by (metis depends_on.simps assms(1) wfP_eq_minimal)
      then show ?thesis using assms(2) DiffD2 by auto
    next
      case False
      hence "Q = {m}" using b by blast
      thus ?thesis using assms(2) by blast
    qed
  qed
  thus ?thesis by (simp add:wfP_eq_minimal, blast)
qed

lemma create_insert_p_s_ordered:
  assumes "is_associated_string N s"
  assumes "a_conditions (insert_messages N) a"
  assumes "Inr (Insert m) = create_insert s n σ new_id"
  shows "a (P m) < a (S m)"
proof -
  obtain p q where pq_def: 
    "create_insert s n σ new_id = Inr (Insert (InsertMessage p new_id q σ))" 
    by (metis (no_types, lifting) One_nat_def add.right_neutral add_Suc_right 
        create_insert.elims sum.case_eq_if sum.simps(4) assms(3) bind_def)
  have "Inr p = nth_visible s n" using pq_def Error_Monad.bindE by fastforce
  moreover have "Inr q = nth_visible s (Suc n)" 
    using pq_def Error_Monad.bindE by fastforce  
  ultimately have "a p < a q"
    using assms by (metis is_associated_string_def nth_visible_inc')
  moreover have "m = InsertMessage p new_id q σ"
    using assms(3) pq_def by auto
  ultimately show ?thesis by (simp add: pq_def)
qed

lemma create_insert_consistent:
  assumes "consistent M"
  assumes "is_associated_string N s"
  assumes "N  M"
  assumes "Inr m = create_insert s n σ new_id"
  assumes "new_id  I ` insert_messages M"
  shows "consistent (M  {m})"
proof -
  obtain p q where pq_def:
    "create_insert s n σ new_id = Inr (Insert (InsertMessage p new_id q σ))"
    by (metis (no_types, lifting) One_nat_def add.right_neutral add_Suc_right 
        create_insert.elims assms(4) sum.case_eq_if sum.simps(4) bind_def)
  define m' where "m' = InsertMessage p new_id q σ" 
  hence a:"m = Insert m'" using pq_def assms(4) by auto
  hence d: "create_insert s n σ new_id = Inr (Insert m')"
    using pq_def assms by simp
  have b:"I m' = new_id" using m'_def by (simp add:I_def)
  hence "inj_on I (insert_messages M  {m'})" using assms(5) assms(1)
    using consistent_def by fastforce
  hence "inj_on I (insert_messages (M  {m}))" using assms(4) pq_def m'_def
    by (metis Inr_inject insert_insert_message)
  moreover 
  have p:"extended_to_set p  I ` set s" using pq_def nth_visible_eff by fastforce 
  have q: "extended_to_set q  I ` set s"
    using pq_def apply (simp add:bind_def del:nth_visible.simps)
    apply (cases "nth_visible s n", simp)
    by (cases "nth_visible s (Suc n)", simp, simp add: nth_visible_eff)  
  have "extended_to_set p  extended_to_set q  I ` set s" using p q by simp
  hence "extended_to_set p  extended_to_set q  I ` insert_messages N"
    by (metis assms(2) is_associated_string_def to_woot_character_keeps_i_lifted)
  hence "extended_to_set p  extended_to_set q  I ` insert_messages M" 
    using assms(3) subset_mono by blast
  hence c:"deps m  I ` insert_messages M" using pq_def assms(4) by auto
  hence " (deps ` (M  {m}))  (I ` insert_messages (M  {m}))"
    by (metis consistent_def assms(1) deps_insert)
  moreover have w: 
    "n  insert_messages M  {m'}. deps (Insert n)  I ` insert_messages M" 
    by (metis a c consistent_def assms(1) Sup_le_iff imageI insert_iff 
        insert_is_Un insert_messages_def mem_Collect_eq sup.commute)
  hence "n  insert_messages M  {m'}. I m'  deps (Insert n)"
    using b assms(5) by blast 
  hence "wfP (depends_on (insert_messages M  {m'}))" 
    by (metis Un_insert_right insert_absorb wf_add assms(1)
        consistent_def sup_bot.right_neutral)
  moreover obtain a where a_def: "a_conditions (insert_messages M) a"
    using consistent_def  assms(1) by blast
  define a' where 
    "a' = (λi. if i =  new_id  then Ψ (a (P m'), a(S m')) new_id else a i)"   
  hence "a_conditions (insert_messages (M  {m})) a'"
  proof -
    have "a'  < a' " using a'_def a_conditions_def a_def by auto
    moreover have 
      "m''. m''  (insert_messages M  {m'})  
          a'(P m'') < a'(S m'')  
          a' I m'' = Ψ (a'(P m''), a'(S m'')) (I m'')" 
    proof 
      fix m''
      assume e:" m''  (insert_messages M  {m'})"
      show "a'(P m'') < a'(S m'')  a'  I m'' = 
            Ψ (a'(P m''), a'(S m'')) (I m'')" 
      proof (cases "m''  insert_messages M")
        case True
        moreover have "deps (Insert m'')  I ` insert_messages M" 
          using e w by blast
        hence "P m''   new_id   S m''   new_id "
          by (meson assms(5) contra_subsetD pred_is_dep succ_is_dep)
        moreover have "I m''  new_id" 
          using assms(5) True by blast
        ultimately show ?thesis using a_def True 
          by (simp add: a_conditions_def a'_def)
      next
        case False
        moreover have "I m'' = new_id" using False b e by blast
        moreover have "deps (Insert m'')  I ` insert_messages M"
          using False a c e by blast
        hence "P m''   new_id   S m''   new_id " 
          by (meson assms(5) contra_subsetD pred_is_dep succ_is_dep)
        moreover have "a_conditions (insert_messages N) a" 
          using a_def a_subset assms is_associated_string_def by blast
        hence "a (P m') < a (S m')"
          by (metis assms(2) d create_insert_p_s_ordered)
        hence "a' (P m'') < a' (S m'')" using calculation a'_def False e by auto
        ultimately show ?thesis using e a'_def by auto
      qed
    qed
    ultimately show "?thesis" using a_conditions_def 
      by (metis a insert_insert_message)
  qed
  ultimately show "?thesis" using consistent_def a by (metis insert_insert_message)
qed

lemma bind_simp: "(x  (λl. y l) = Inr r)  (y (projr x) = Inr r)"
  using isOK_I by force

lemma create_delete_consistent:
  assumes "consistent M"
  assumes "is_associated_string N s"
  assumes "N  M"
  assumes "Inr m = create_delete s n"
  shows "consistent (M  {m})"
proof -
  obtain i where pq_def: "create_delete s n = Inr (Delete (DeleteMessage i))"
    by (metis (no_types, lifting) Error_Monad.bindE create_delete.simps assms(4)) 
  hence a: "m = Delete (DeleteMessage i)" using assms(4) by auto
  hence b: "insert_messages (M  {m}) = insert_messages M" 
    by (simp add:insert_messages_def)
  have "n  0" apply (rule classical) using pq_def by (simp add:bind_def ext_ids_def) 
  then obtain u where "n = Suc u" using not0_implies_Suc by blast
  then have "i  I ` set s" using pq_def 
    apply (cases "u < length (filter is_visible s)")
    apply (simp add:bind_simp ext_ids_def nth_append) 
    apply (meson filter_is_subset imageI in_set_conv_nth subset_code(1))
    apply (cases "u = length (filter is_visible s)")
    by (simp add:bind_def ext_ids_def nth_append)+
  hence "i  I ` insert_messages N" using assms
    by (metis is_associated_string_def to_woot_character_keeps_i_lifted)
  hence c:"deps m  I ` insert_messages M" using a 
    by (metis assms(3) deps.simps(2) singletonD subsetCE subsetI subset_mono)
  then show "?thesis" using assms(1) b by (simp add:consistent_def)
qed

end

Theory IntegrateInsertCommute

subsection ‹Termination Proof for @{term integrate_insert}\label{sec:integrate_term}›

theory IntegrateInsertCommute
  imports IntegrateAlgorithm Consistency CreateConsistent
begin

text ‹In the following we show that @{term integrate_insert} terminates. Note that, this does not
  yet imply that the return value will not be an error state.›

lemma substr_simp [simp]: "substr s l u = nths s {k. l < Suc k  Suc k < u}"
proof (cases "l  length s")
  case True
  have "set (nths (take l s) {k. l < Suc k  Suc k < u}) = {}" 
    by (simp add:set_nths)
  hence "nths (take l s) {k. l < Suc k  Suc k < u} = []" by blast
  moreover have "{j. Suc (j + l) < u} = {..<(u-Suc l)}" by auto
  moreover have "min (length s) l = l" using True by auto
  ultimately
    have "nths (take l s @ drop l s) {k. l < Suc k  Suc k < u} = substr s l u"
    by (simp add:nths_append del:append_take_drop_id)
  then show ?thesis by simp
next
  case False
  hence "set (nths s {k. l < Suc k  Suc k < u}) = {}"
    by (simp add:set_nths)
  hence "nths s {k. l < Suc k  Suc k < u} = []" by blast
  thus ?thesis using False by simp
qed

declare substr.simps [simp del]

text ‹Instead of simplifying @{term substr} with its definition we use @{thm [source] substr_simp}
  as a simplification rule. The right hand side of @{thm [source] substr_simp} is a better
  representation within proofs. However, we cannot directly define @{term substr} using the right
  hand side as it is not constructible term for Isabelle.›

lemma int_ins_loop_term_1:
  assumes "isOK (mapM (concurrent w l u) t)"
  assumes "x  set (concat (projr (mapM (concurrent w l u) t)))"
  shows "x  (InString  I) ` (set t)"
  using assms
  by (induction t, simp, simp add: bind_simp del:idx.simps set_concat, blast)

lemma fromSingleton_simp: "(fromSingleton xs = Inr x) = ([x] = xs)"
  by (cases xs rule: fromSingleton.cases, auto)

lemma filt_simp: "([b] = filter p [0..<n]) =
   (p b  b < n  (y < n. p y  b = y))" 
  apply (induction n, simp, simp) 
  by (metis atLeast_upt cancel_comm_monoid_add_class.diff_cancel 
      filter_empty_conv lessThan_iff less_Suc_eq neq0_conv zero_less_diff)

lemma substr_eff: 
  assumes "x  (InString  I) ` set (substr w l u)"
  assumes "isOK (idx w x)"
  shows "l < (projr (idx w x))  (projr (idx w x)) < u"
proof -
  obtain i where i_def: "idx w x = Inr i" using assms(2) by blast
  then have "l < i  i < u" using assms(1) 
    apply (simp add: set_nths image_iff fromSingleton_simp filt_simp)
    apply (simp add:ext_ids_def) 
    by (metis (no_types, lifting) Suc_mono length_map less_SucI list_update_id
        list_update_same_conv map_update nth_Cons_Suc nth_append)
  thus ?thesis using i_def by auto
qed

lemma find_zip:
  assumes "find (cond  snd) (zip (p#v) (v@[s])) = Some (x,y)" 
  assumes "v  []"
  shows
    "cond y"
    "x  set v  y  set v"
    "x = p  (x  set v  ¬(cond x))"
    "y = s  (y  set v)"
proof -
  obtain i where i_def:
    "i < Suc (length v)"
    "(zip (p#v) (v@[s])) ! i = (x,y)"
    "cond y"
    "j. j < i  ¬(cond ((v@[s])!j))"
    using assms apply (simp add:find_Some_iff) by force
  show "cond y" using i_def by auto
  show "x  set v  y  set v" using assms(2) i_def(1,2)
    by (metis fst_conv in_set_conv_nth length_0_conv length_Cons length_append_singleton
        less_Suc_eq less_Suc_eq_0_disj nth_Cons_Suc nth_append nth_zip snd_conv)
  show "x = p  (x  set v  (¬(cond x)))"
    apply (cases i)
    using i_def(2) apply auto[1]
    by (metis Suc_less_eq fst_conv i_def(1,2,4) length_Cons
        length_append_singleton lessI nth_Cons_Suc nth_append nth_mem nth_zip)
  show "y = s  y  set v"
    by (metis diff_is_0_eq' i_def(1,2) in_set_conv_nth length_Cons
        length_append_singleton less_Suc_eq_le nth_Cons_0 nth_append nth_zip snd_conv)
qed

fun int_ins_measure'
  where
    "int_ins_measure' (m,w,p,s) = (
      do {
        l  idx w p;
        u  idx w s;
        assert (l < u);
        return (u - l)
      })"

fun int_ins_measure
  where
    "int_ins_measure (m,w,p,s) = case_sum (λe. 0) id (int_ins_measure' (m,w,p,s))"

text ‹We show that during the iteration of @{term integrate_insert}, the arguments are decreasing
  with respect to @{term int_ins_measure}. Note, this means that the distance between the
  W-characters with identifiers @{term p} (resp. @{term s}) is decreasing.›

lemma int_ins_loop_term:
  assumes "idx w p = Inr l"
  assumes "idx w s = Inr u"
  assumes "mapM (concurrent w l u) (substr w l u) = Inr d" 
  assumes "concat d  []"
  assumes "find ((λx.I m < x  x = s)  snd) 
    (zip (p#concat d) (concat d@[s])) = Some r"
  shows "int_ins_measure (m, w, r) < u - l"
proof -
  have a: "x y. x  set (concat d)  idx w x = Inr y  l < y  y < u"
    using int_ins_loop_term_1 substr_eff assms(3) by (metis isOK_I sum.sel(2))
  hence b: "l < u" using assms
    by (metis concat.simps(1) diff_is_0_eq less_imp_le_nat
        mapM.simps(1) not_less_eq substr.simps sum.sel(2) take0)
  obtain p' s' where ps_def: "r = (p', s')" by (cases r, simp+)
  show ?thesis
  proof (cases "int_ins_measure' (m, w, r)")
    case (Inl a)
    then show ?thesis using b by (simp add:ps_def)
  next
    case (Inr b)
    then obtain l' u' where ps'_def: "idx w p' = Inr l'" "idx w s' = Inr u'"
      using ps_def apply (simp add:bind_simp del:idx.simps) by blast
    then have "l'  l  l' < u  u' > l  u'  u  (l' > l  u' < u)"
      using a b ps_def find_zip(2,3,4) assms(1,2,4,5)
      by (metis (no_types, lifting) Inr_inject order.order_iff_strict)
    thus ?thesis using ps_def ps'_def apply (simp add:bind_simp del:idx.simps)
      by (cases "l' < u'", simp del:idx.simps, linarith, simp del:idx.simps)
  qed
qed

lemma assert_ok_simp [simp]: "(assert p = Inr z) = p" by (cases p, simp+)

termination integrate_insert
  apply (relation "measure int_ins_measure", simp)
  using int_ins_loop_term by (simp del:idx.simps, blast)

subsection ‹Integrate Commutes›

locale integrate_insert_commute =
  fixes M :: "('a :: linorder, 's) message set"
  fixes a :: "'a extended  'a position"
  fixes s :: "('a, 's) woot_character list"
  assumes associated_string_assm: "is_associated_string M s"
  assumes a_conditions_assm: "a_conditions (insert_messages M) a"
begin

lemma dist_ext_ids: "distinct (ext_ids s)"
  using associated_string_assm a_conditions_assm
  apply (simp add:is_associated_string_def sorted_wrt_map)
  by (metis (mono_tags) irreflp_def le_less not_le sorted_wrt_irrefl_distinct)

lemma I_inj_on_S:
  "l < length s  u < length s  I(s ! l) = I(s ! u)  l = u"
  using dist_ext_ids apply (simp add:ext_ids_def)
  using nth_eq_iff_index_eq by fastforce

lemma idx_find: 
  assumes "x < length (ext_ids s)"
  assumes "ext_ids s ! x = i"
  shows "idx s i = Inr x"
  using assms dist_ext_ids nth_eq_iff_index_eq
  by (simp add:filt_simp fromSingleton_simp, blast)

lemma obtain_idx:
  assumes "x  set (ext_ids s)" 
  shows "i. idx s x = Inr i" 
  using idx_find assms by (metis in_set_conv_nth)

lemma sorted_a:
  assumes "idx s x = Inr l"
  assumes "idx s y = Inr u"
  shows "(l  u) = (a x  a y)"
proof -
  have "sorted_wrt (<) (map a (ext_ids s))" 
    using associated_string_assm a_conditions_assm is_associated_string_def by blast
  then show ?thesis
  using assms apply (simp add:filt_simp fromSingleton_simp)
  by (metis leD leI le_less length_map nth_map sorted_wrt_nth_less)
qed

lemma sorted_a_le: "idx s x = Inr l  idx s y = Inr u  (l < u) = (a x < a y)"
  by (meson sorted_a not_le)

lemma idx_intro_ext: "i < length (ext_ids s)  idx s (ext_ids s ! i) = Inr i"
  using dist_ext_ids by (simp add:fromSingleton_simp filt_simp  nth_eq_iff_index_eq)

lemma idx_intro:
  assumes "i < length s"
  shows "idx s I (s ! i) = Inr (Suc i)"
proof -
  have "ext_ids s  ! (Suc i) = I (s ! i)  Suc i < length (ext_ids s)"
    using assms by (simp add:ext_ids_def nth_append)
  thus ?thesis using idx_intro_ext by force
qed

end

locale integrate_insert_commute_insert = integrate_insert_commute +
  fixes m
  assumes consistent_assm: "consistent (M  {Insert m})"
  assumes insert_assm: "Insert m  M"
  assumes a_conditions_assm_2: 
    "a_conditions (insert_messages (M  {Insert m})) a"
begin

definition invariant where 
  "invariant pm sm = (pm  set (ext_ids s)  sm  set (ext_ids s) 
   subset (a pm, a sm) (a (P m), a (S m))  
   elem (a I m) (a pm, a sm))"

fun is_concurrent where 
  "is_concurrent pm sm x = (x  set s  
   subset (a pm, a sm) (a (P x), a (S x))  
   elem (a I x) (a pm, a sm))"

lemma no_id_collision: "I m  I ` insert_messages M"
proof -
  have "inj_on I (insert_messages (M  {Insert m}))"
    using consistent_def consistent_assm by fastforce
  hence "I m  I ` insert_messages M  Insert m  M"
    by (simp add: image_iff inj_on_eq_iff insert_messages_def)
  thus ?thesis using insert_assm by blast
qed
      
lemma not_deleted: "to_woot_char m = to_woot_character M m"
proof -
  have "Delete (DeleteMessage (I m))  M"
  proof
    assume "Delete (DeleteMessage (I m))  M"
    hence "deps (Delete (DeleteMessage (I m)))  I ` insert_messages M"
      using consistent_assm associated_string_assm
      apply (simp add:consistent_def is_associated_string_def)
      using image_subset_iff by fastforce
    thus "False" using no_id_collision by simp
  qed
  thus "to_woot_char m = to_woot_character M m"
    by (cases m, simp add:to_woot_character_def delete_maybe_def)
qed

lemma invariant_imp_sorted:
  assumes "Suc l < length (ext_ids s)"
  assumes "a(ext_ids s ! l) < a I m  a I m < a(ext_ids s ! (l+1))"
  shows "sorted_wrt (<) (map a (ext_ids ((take l s)@to_woot_char m#drop l s)))"
proof -
  have "l  length s" using assms(1) by (simp add:ext_ids_def)
  hence "ext_ids (take l s@to_woot_char m#drop l s) = 
        (take (Suc l) (ext_ids s))@I m#(drop (Suc l) (ext_ids s))"
    by (cases m, simp add:ext_ids_def take_map drop_map)
  thus ?thesis
    using assms associated_string_assm is_associated_string_def a_conditions_assm
    apply (simp flip:take_map drop_map)
    by (rule insort, simp+, blast)
qed

lemma no_self_dep: "¬ depends_on (insert_messages M  {m}) m m"
proof -
  have "wfP (depends_on (insert_messages M  {m}))"
    using consistent_assm
    apply (simp add:consistent_def)
    by (metis Un_insert_right insert_insert_message sup_bot.right_neutral)
  thus ?thesis 
    by (metis mem_Collect_eq wfP_eq_minimal)
qed

lemma pred_succ_order:
  "m'  (insert_messages M  {m})  a(P m') < a I m'  a(S m') > a I m'"
  by (metis elem.simps is_interval.simps psi_elem a_conditions_def 
      a_conditions_assm_2 insert_insert_message)

lemma find_dep:
  assumes "Insert m'  (M  {Insert m})"
  assumes "i  deps (Insert m')"
  shows "i  set (ext_ids s)"
proof -
  have "i  I ` insert_messages M"
  proof (cases "m' = m")
    case True
    hence "i  I ` insert_messages (M  {Insert m})"
      using assms consistent_assm
      by (simp add:consistent_def, blast)
    moreover have "i  I m" using assms True no_self_dep by auto
    ultimately show ?thesis
      by (metis (no_types, lifting) UnE image_Un image_empty image_insert 
          insert_insert_message singletonD)
  next
    case False
    hence "Insert m'  M" using assms by simp
    then show "i  I ` insert_messages M"
      using assms is_associated_string_def associated_string_assm consistent_def
      by (metis (no_types, hide_lams) Union_iff contra_subsetD image_iff)
  qed
  hence "i  I ` (set s)"
    using associated_string_assm by (simp add:is_associated_string_def)
  thus "i  set (ext_ids s)"
    by (simp add:ext_ids_def image_iff) 
qed

lemma find_pred:
  "m'  (insert_messages M  {m})  P m'  set (ext_ids s)"
  using find_dep by (cases "P m'", (simp add:ext_ids_def insert_messages_def pred_is_dep)+)

lemma find_succ:
  "m'  (insert_messages M  {m})  S m'  set (ext_ids s)"
  using find_dep by (cases "S m'", (simp add:ext_ids_def insert_messages_def succ_is_dep)+)

fun is_certified_associated_string' where
  "is_certified_associated_string' (Inr v) = (
    set v = to_woot_character (M  {Insert m}) ` 
      (insert_messages (M  {Insert m})) 
    sorted_wrt (<) (map a (ext_ids v)))" |
  "is_certified_associated_string' (Inl _) = False" 

lemma integrate_insert_final_step:
  assumes "invariant pm sm"
  assumes "idx s pm = Inr l"
  assumes "idx s sm = Inr (Suc l)" 
  shows "is_certified_associated_string' (Inr (take l s@(to_woot_char m)#drop l s))"
proof -
  define t where "t = (take l s@(to_woot_char m)#drop l s)"
  hence "set t = set s  {to_woot_char m}"
    by (metis Un_insert_right append_take_drop_id list.simps(15) 
        set_append sup_bot.right_neutral)
  hence 
    "set t = to_woot_character M ` insert_messages M  {to_woot_character M m}"
    using not_deleted by (metis associated_string_assm is_associated_string_def)
  hence 
    "set t = to_woot_character (M  {Insert m}) ` insert_messages (M  {Insert m})"
    apply (simp add: to_woot_character_insert_no_eff) 
    using insert_insert_message by fastforce
  moreover have "sorted_wrt (<) (map a (ext_ids t))" using assms invariant_imp_sorted
    by (simp add:invariant_def fromSingleton_simp filt_simp t_def)
  ultimately show ?thesis 
    using t_def associated_string_assm by (simp add:is_associated_string_def)
qed

lemma concurrent_eff:
  assumes "idx s pm = Inr l"
  assumes "idx s sm = Inr u"
  obtains d where "mapM (concurrent s l u) (substr s l u) = Inr d  
    set (concat d) = InString ` I ` {x. is_concurrent pm sm x}"
proof -
  define t where "t = substr s l u"
  have "set t  set s  (isOK (mapM (concurrent s l u) t) 
    set (concat (projr (mapM (concurrent s l u) t))) = 
    InString ` I ` {x. x  set t  a (P x)  a pm  a (S x)  a sm})"
  proof (induction t)
    case Nil
    then show ?case by simp
  next
    case (Cons th tt)
    hence "th  to_woot_character M ` insert_messages M" 
      using associated_string_assm by (simp add: is_associated_string_def)
    then obtain th' where th'_def: 
      "th'  insert_messages M  P th' = P th  S th' = S th"
      by (metis image_iff to_woot_character_keeps_P to_woot_character_keeps_S)
    obtain l' where l'_def: "idx s (P th) = Inr l'"
      using th'_def find_pred obtain_idx by fastforce
    obtain u' where u'_def: "idx s (S th) = Inr u'"
      using th'_def find_succ obtain_idx by fastforce
    have "{x. x = I th  l'  l  u  u'} = 
      InString ` I ` {x. x = th  a (P x)  a pm  a sm  a (S x)}"
      using sorted_a l'_def u'_def assms 
      by (rule_tac set_eqI, simp add:image_iff, blast)
    then show ?case 
      using Cons 
      by (simp add:bind_simp l'_def u'_def 
          concurrent.simps[where w=th] del:idx.simps, auto)
  qed
  moreover have 
    "x. (x  set (substr s l u)) = (x  set s  a pm < a I x  a I x < a sm)"
    apply (simp add:set_nths in_set_conv_nth)
    using sorted_a_le idx_intro assms by blast
  ultimately have "
    isOK (mapM (concurrent s l u) (substr s l u))  
    set (concat (projr (mapM (concurrent s l u) (substr s l u)))) = 
      InString ` I ` {x. is_concurrent pm sm x}"
    by (simp only:t_def, fastforce)
  thus ?thesis using that by auto
qed

lemma concurrent_eff_2:
  assumes "invariant pm sm" 
  assumes "is_concurrent pm sm x"
  shows "preserve_order I x I m (a I x) (a I m)"
proof -
  have "x  to_woot_character M ` insert_messages M" 
    using assms(2) associated_string_assm is_associated_string_def 
      is_concurrent.elims(2) by blast
  then obtain x' where x'_def: "I x = I x'  P x = P x'  S x = S x'  x'  insert_messages M"
    using to_woot_character_keeps_P to_woot_character_keeps_S 
      to_woot_character_keeps_i by fastforce
  have "elem (a I x) (a (P m), a (S m))"
    using assms by (simp add: invariant_def, auto) 
  moreover have "elem (a I m) (a (P x), a (S x))" 
    using assms by (simp add: invariant_def, auto)
  moreover have "a_conditions (insert_messages M  {m}) a"
    by (metis insert_insert_message a_conditions_assm_2)
  ultimately have "preserve_order (I x) (I m) (a I x) (a I m)" 
    by (simp add: a_conditions_def psi_preserve_order x'_def)
  thus ?thesis by (simp add: preserve_order_def)
qed

lemma concurrent_eff_3:
  assumes "idx s pm = Inr l"
  assumes "idx s sm = Inr u"
  assumes "Suc l < u"
  shows "{x. is_concurrent pm sm x}  {}"
proof -
  define H where
    "H = {x. x  insert_messages M  a pm < a I x  a I x < a sm}"
  have "wfP (depends_on (insert_messages M))"
    using associated_string_assm by (simp add: consistent_def is_associated_string_def)
  moreover have f:"H  insert_messages M" using H_def by blast
  hence "depends_on H  depends_on (insert_messages M)" by auto
  ultimately have "wfP (depends_on H)" using wf_subset [to_pred] by blast
  moreover
  have u: "l < length s" using assms(2) assms(3) 
    by (simp add:fromSingleton_simp filt_simp, simp add:ext_ids_def)
  hence v:"a pm < a I(s ! l)  a I(s ! l) < a sm" 
    using sorted_a_le assms u idx_intro by blast
  have "I (s ! l)  I ` insert_messages M"
    by (metis image_eqI associated_string_assm is_associated_string_def nth_mem 
        to_woot_character_keeps_i_lifted u)
  hence "x. x  H" using v H_def by auto
  ultimately obtain z where z_def: "z  H" " y. depends_on H y z  y  H"
    by (metis wfP_eq_minimal)
  have a:"x. x  deps (Insert z)  ¬(a pm < a x  a x < a sm)"
  proof -
    fix x
    assume a:"x  deps (Insert z)"
    hence "x  I ` insert_messages M" 
      using insert_messages_def associated_string_assm 
      apply (simp add:consistent_def is_associated_string_def)
      using H_def z_def(1) by blast
    then obtain x' where x'_def: "x'  insert_messages M  x = I x'" by blast
    hence "x'  H" using z_def 
      using a depends_on.simps by blast
    thus "¬(a pm < a x  a x < a sm)" using H_def x'_def by blast
  qed
  have "ext_ids s ! 0 =   0 < length (ext_ids s)" by (simp add:ext_ids_def)
  hence b:"¬(a pm < a )"
    by (metis not_less_zero  sorted_a_le assms(1) idx_intro_ext)
  have "ext_ids s ! (Suc (length s)) =   Suc (length s) < length (ext_ids s)"
    by (simp add:nth_append ext_ids_def)
  moreover have "¬(Suc (length s) < u)" using assms(2)
    by (simp add:fromSingleton_simp filt_simp, simp add:ext_ids_def)
  ultimately have c:"¬(a  < a sm)" by (metis sorted_a_le assms(2) idx_intro_ext)
  have d:"a (P z)  a pm"
    using a b c pred_is_dep pred_succ_order H_def z_def(1) by (cases "P z", fastforce+)
  have e:"a (S z)  a sm"
    using a b c succ_is_dep pred_succ_order H_def z_def(1) by (cases "S z", fastforce+)
  have "to_woot_character M z  set s" 
    using f associated_string_assm is_associated_string_def z_def(1) by fastforce
  hence "is_concurrent pm sm (to_woot_character M z)"
    using H_def z_def(1) d e by simp
  thus ?thesis by blast
qed

lemma integrate_insert_result_helper:
  "invariant pm sm  m' = m  s' = s  
  is_certified_associated_string' (integrate_insert m' s' pm sm)"
proof (induction m' s' pm sm rule:integrate_insert.induct)
  case (1 m' s' pm sm)
  obtain l where l_def: "idx s pm = Inr l" 
    using "1"(2) invariant_def obtain_idx by blast
  obtain u where u_def: "idx s sm = Inr u"
    using "1"(2) invariant_def obtain_idx by blast
  show ?case
  proof (cases "Suc l = u")
    case True
    then show ?thesis
      apply (simp add:l_def u_def 1 del:idx.simps is_certified_associated_string'.simps)
      using "1"(2) l_def u_def integrate_insert_final_step by blast
  next
    case False
    have "a pm < a sm" using invariant_def "1"(2) by auto
    hence a:"l < u" using sorted_a_le  l_def u_def by blast
    obtain d where d_def: "mapM (concurrent s l u) (substr s l u) = Inr d   
      set (concat d) = InString ` I ` {x. is_concurrent pm sm x}" 
      by (metis concurrent_eff l_def u_def)
    have b:"concat d  []" 
      by (metis Suc_lessI concurrent_eff_3 False l_def u_def 
          a d_def empty_set image_is_empty)
    have c:"x. x  set (concat d)  
      preserve_order x I m (a x) (a I m)  x  set (ext_ids s) 
       a pm < a x  a x < a sm"
      using 1(2) d_def concurrent_eff_2 
      by (simp del:set_concat add:ext_ids_def, blast)
    obtain pm' sm' where ps'_def: "find ((λx.I m < x  x = sm)  snd)
         (zip (pm # concat d) (concat d @ [sm])) = Some (pm',sm')"
      (is "?lhs = ?rhs")
      apply (cases "?lhs")
      apply (simp add:find_None_iff) 
       apply (metis in_set_conv_decomp in_set_impl_in_set_zip2 length_Cons 
              length_append_singleton) 
      by fastforce
    have d:"pm' = pm  pm'  set (concat d)" using ps'_def b
      by (metis (full_types) find_zip(3))
    hence "pm'  set (ext_ids s)" using c 1(2) invariant_def by auto
    hence "pm'  InString ` I ` insert_messages M  pm' =   pm' = "
      apply (simp add:ext_ids_def)
      by (metis image_image associated_string_assm is_associated_string_def 
          to_woot_character_keeps_i_lifted)
    hence "pm'  I m" using no_id_collision by blast
    hence "(pm' = pm  pm' < I m)  (sm' = sm  sm' > I m  sm'  set (concat d))" 
      by (metis (mono_tags, lifting) ps'_def b find_zip(1) find_zip(3) find_zip(4) less_linear)
    hence e:"invariant pm' sm'"
      using 1(2) c d apply (simp add:invariant_def del:set_concat) 
      by (meson dual_order.strict_trans leD leI preserve_order_def)
    show ?thesis apply (subst integrate_insert.simps)
      using a b e ps'_def 1 d_def False l_def u_def
      by (simp add:1 del:idx.simps integrate_insert.simps)
  qed
qed

lemma integrate_insert_result:
  "is_certified_associated_string' (integrate_insert m s (P m) (S m))"
proof -
  have "invariant (P m) (S m)" 
    using find_pred find_succ pred_succ_order by (simp add:invariant_def)
  thus ?thesis using integrate_insert_result_helper by blast
qed
end

lemma integrate_insert_result:
  assumes "consistent (M  {Insert m})"
  assumes "Insert m  M"
  assumes "is_associated_string M s"
  shows "is_certified_associated_string (M  {Insert m}) (integrate_insert m s (P m) (S m))"
proof -
  obtain t where t_def: "(integrate_insert m s (P m) (S m)) = Inr t 
    set t = to_woot_character (M  {Insert m}) ` (insert_messages (M  {Insert m}))"
  proof -
    fix tt
    assume a:"(t. (integrate_insert m s (P m) (S m)) = Inr t 
          set t = to_woot_character (M  {Insert m}) ` insert_messages (M  {Insert m}) 
          tt)"
    obtain a where a_def: "a_conditions (insert_messages (M  {Insert m})) a"
      using consistent_def assms by blast
    moreover have "a_conditions (insert_messages M) a"
      using assms a_subset is_associated_string_def a_def by blast
    ultimately interpret integrate_insert_commute_insert "M" "a" "s" "m"
      using assms by (simp add: integrate_insert_commute_insert_def integrate_insert_commute_def (*
                *) integrate_insert_commute_insert_axioms.intro)
    show tt using a integrate_insert_result
      apply (cases "integrate_insert m s (P m) (S m)") by auto 
  qed
  have b:"a. a_conditions (insert_messages (M  {Insert m})) a  
    sorted_wrt (<) (map a (ext_ids t))"
  proof -
    fix a
    assume c:"a_conditions (insert_messages (M  {Insert m})) a"
    moreover have "a_conditions (insert_messages M) a"
      using assms a_subset is_associated_string_def c by blast
    ultimately interpret integrate_insert_commute_insert "M" "a" "s" "m"
      using assms by (simp add: integrate_insert_commute_insert_def integrate_insert_commute_def (*
                *) integrate_insert_commute_insert_axioms.intro)
    show "sorted_wrt (<) (map a (ext_ids t))" 
      using integrate_insert_result t_def by simp
  qed
  show "?thesis" using b t_def assms(1) by (simp add:is_associated_string_def)
qed 

locale integrate_insert_commute_delete = integrate_insert_commute +
  fixes m
  assumes consistent_assm: "consistent (M  {Delete m})"
begin

fun delete :: "('a, 's) woot_character  ('a, 's) woot_character"
  where "delete (InsertMessage p i u _) = InsertMessage p i u None"

definition delete_only_m :: "('a, 's) woot_character  ('a, 's) woot_character"
  where "delete_only_m x = (if DeleteMessage (I x) = m then delete x else x)"

lemma set_s: "set s = to_woot_character M ` insert_messages M"
  using associated_string_assm by (simp add:is_associated_string_def)

lemma delete_only_m_effect:
  "delete_only_m (to_woot_character M x) = to_woot_character (M  {Delete m}) x"
  apply (cases x, simp add:to_woot_character_def delete_maybe_def)
  by (metis delete_only_m_def insert_message.sel(2) delete.simps)

lemma integrate_delete_result:
  "is_certified_associated_string (M  {Delete m}) (integrate_delete m s)"
proof (cases m)
  case (DeleteMessage i)
  have "deps (Delete m)  I ` insert_messages (M  {Delete m})"
    using consistent_assm by (simp add:consistent_def DeleteMessage)
  hence "i  I ` insert_messages (M  {Delete m})" using DeleteMessage by auto
  hence "i  I ` set s" using set_s by (simp add:insert_messages_def)
  then obtain k where k_def: "I (s ! k) = i  k < length s" 
    by (metis imageE in_set_conv_nth)
  hence "ext_ids s ! (Suc k) = i  Suc k < length (ext_ids s)" 
    by (simp add:ext_ids_def nth_append)
  hence g:"idx s i = Inr (Suc k)" apply (simp add:fromSingleton_simp filt_simp)
     using dist_ext_ids nth_eq_iff_index_eq by fastforce
  moreover define t where "t = List.list_update s k (delete (s ! k))"
  ultimately have a: "integrate_delete m s = Inr t"
    using k_def DeleteMessage by (cases "s ! k", simp)
  have "j. j < length s  (DeleteMessage (I(s ! j)) = m) = (j = k)" 
    apply (simp add: DeleteMessage) using I_inj_on_S k_def by blast
  hence "List.list_update s k (delete (s ! k)) = map delete_only_m s"
    by (rule_tac nth_equalityI, (simp add:k_def delete_only_m_def)+)
  hence "set t = delete_only_m ` set s" using t_def by auto
  also have "... = to_woot_character (M  {Delete m}) ` (insert_messages M)"
    using set_s delete_only_m_effect image_cong by (metis (no_types, lifting) image_image)
  finally have b:
    "set t = to_woot_character (M  {Delete m}) ` (insert_messages (M  {Delete m}))"
    by (simp add: insert_messages_def)
  have "ext_ids s = ext_ids t"
    apply (cases "s ! k", simp add:t_def ext_ids_def) 
    by (metis (no_types, lifting) insert_message.sel(2) list_update_id map_update)
  moreover have "a. a_conditions (insert_messages M) a  sorted_wrt (<) (map a (ext_ids s))"
    using associated_string_assm is_associated_string_def by blast
  ultimately have c: "a. a_conditions (insert_messages (M  {Delete m})) a
                   sorted_wrt (<) (map a (ext_ids t))" 
    by (simp add:insert_messages_def)
  show ?thesis
    apply (simp add:a is_associated_string_def b c)
    using consistent_assm by fastforce
qed
end

lemma integrate_delete_result:
  assumes "consistent (M  {Delete m})"
  assumes "is_associated_string M s"
  shows "is_certified_associated_string (M  {Delete m}) (integrate_delete m s)"
proof -
  obtain a where a_def: "a_conditions (insert_messages (M  {Delete m})) a" 
    using consistent_def assms by blast
  moreover have "a_conditions (insert_messages M) a"
    using assms a_subset is_associated_string_def a_def by blast
  ultimately interpret integrate_insert_commute_delete "M" "a" "s" "m"
    using assms by (simp add: integrate_insert_commute_def integrate_insert_commute_delete.intro
            integrate_insert_commute_delete_axioms.intro)
  show "?thesis" using integrate_delete_result by blast
qed

fun is_delete :: "(('a, 's) message)  bool" 
  where 
    "is_delete (Insert m) = False" |
    "is_delete (Delete m) = True"

proposition integrate_insert_commute:
  assumes "consistent (M  {m})"
  assumes "is_delete m  m  M"
  assumes "is_associated_string M s"
  shows "is_certified_associated_string (M  {m}) (integrate s m)"
  using assms integrate_insert_result integrate_delete_result by (cases m, fastforce+)

end

Theory StrongConvergence

subsection ‹Strong Convergence›

theory StrongConvergence
  imports IntegrateInsertCommute CreateConsistent HOL.Finite_Set DistributedExecution
begin

lemma  (in dist_execution) happened_before_same:
  assumes "i < j"
  assumes "j < length (events k)"
  shows "(happened_immediately_before)++ (k,i) (k,j)" 
proof -
  obtain v where v_def: "j = Suc i + v" using assms(1) less_iff_Suc_add by auto
  have "is_valid_event_id (k, Suc i + v)  (happened_immediately_before)++ (k,i) (k, Suc i + v)"
    apply (induction v, simp add: tranclp.r_into_trancl)
    by (metis Suc_lessD add_Suc_right fst_conv happened_immediately_before.elims(3) 
        is_valid_event_id.simps snd_conv tranclp.simps)
  then show ?thesis
    using is_valid_event_id.simps v_def assms by blast
qed

definition make_set where "make_set (k :: nat) p = {x. j. p j x  j < k}"

lemma make_set_nil [simp]: "make_set 0 p = {}" by (simp add:make_set_def)

lemma make_set_suc [simp]: "make_set (Suc k) p = make_set k p  {x. p k x}"
  using less_Suc_eq by (simp add:make_set_def, blast)

lemma (in dist_execution) received_messages_eff:
  assumes "is_valid_state_id (i,j)"
  shows "set (received_messages (i,j)) = make_set j (λk x. (s. event_at (i, k) (Receive s x)))" 
  using assms by (induction j, simp add:make_set_def, simp add: take_Suc_conv_app_nth)

lemma (in dist_execution) finite_valid_event_ids:
  "finite {i. is_valid_event_id i}"
proof -
  define X where "X = {p. events p = events p}"
  have "finite X  m. (p  X. (length (events p)) < m)" 
    apply (induction rule:finite_induct, simp)
    by (metis gt_ex insert_iff le_less_trans less_imp_not_less not_le_imp_less)
  then obtain m where m_def: "p. length (events p) < m" using X_def fin_peers by auto
  have "{(i,j). is_valid_event_id (i,j)}  {(i,j). j < m}" 
    using m_def by (simp add: Collect_mono_iff less_trans)
  also have "...  X × {j. j < m}" using X_def by blast
  finally have "{i. is_valid_event_id i}  X × {j. j < m}" 
    by (simp add: subset_iff)
  thus ?thesis
    using fin_peers finite_Collect_less_nat finite_cartesian_product
        infinite_super subset_eq
    by (metis UNIV_I)
qed

lemma (in dist_execution) send_insert_id_1:
  "state i  (λs. create_insert s n σ i) = Inr (Insert m)  I m = i"
  by fastforce

lemma (in dist_execution) send_insert_id_2:
  "state i  (λs. create_delete s n) = Inr (Insert m)  False"
  by fastforce

lemma (in dist_execution) send_insert_id:
  "event_at i (Send (Insert m))  I m = i" 
  using send_correct send_insert_id_1 send_insert_id_2 by metis

lemma (in dist_execution) recv_insert_once:
  "event_at (i,j) (Receive s (Insert m))  event_at (i,k) (Receive t (Insert m))  j = k"
  using no_data_corruption send_insert_id at_most_once
  by (simp, metis (mono_tags) Pair_inject event_pred.simps fst_conv is_valid_event_id.simps)

proposition integrate_insert_commute':
  fixes M m s
  assumes "consistent M"
  assumes "is_delete m  m  T"
  assumes "m  M"
  assumes "T  M"
  assumes "deps m  I ` insert_messages T" 
  assumes "is_certified_associated_string T s"
  shows "is_certified_associated_string (T  {m}) (s  (λt. integrate t m))" 
proof (cases s)
  case (Inl a)
  then show ?thesis using assms by simp
next
  case (Inr b)
  have "T  {m}  M" using assms(3) assms(4) by simp 
  moreover have " (deps ` (T  {m}))  I ` insert_messages (T  {m})" 
    using assms(5) assms(6) Inr apply (simp add:is_associated_string_def consistent_def)
    by (meson dual_order.trans subset_insertI subset_mono)
  ultimately have "consistent (T  {m})"
    using assms consistent_subset by force 
  then show ?thesis using integrate_insert_commute assms(2) assms(6) Inr by auto
qed

lemma foldM_rev: "foldM f s (li@[ll]) = foldM f s li  (λt. f t ll)"
  by (induction li arbitrary:s, simp+)

lemma  (in dist_execution) state_is_associated_string':
  fixes i M
  assumes "j  length (events i)"
  assumes "consistent M"
  assumes "make_set j (λk m. s. event_at (i,k) (Receive s m))  M"
  shows "is_certified_associated_string (make_set j (λk m. s. event_at (i,k) (Receive s m))) (state (i,j))"
  using assms
proof (induction j)
  case 0
  then show ?case by (simp add: empty_associated)
next
  case (Suc j)
  have b:"j < length (events i)" using Suc by auto
  show ?case
  proof (cases "events i ! j")
    case (Send m)
    then show ?thesis using Suc by (simp add: take_Suc_conv_app_nth) 
  next
    case (Receive s m)
    moreover have "is_delete m  m  (make_set j (λk m. s. event_at (i,k) (Receive s m)))"
      apply (cases m) using recv_insert_once Receive b apply (simp add: make_set_def) 
      apply (metis nat_neq_iff)
      by (simp)
    moreover have "deps m  I ` insert_messages (make_set j (λk m. s. event_at (i,k) (Receive s m)))"
      apply (rule subsetI)
      using semantic_causal_delivery Receive b apply (simp add:insert_messages_def image_iff make_set_def) by metis
    ultimately show ?thesis 
      using Suc apply (cases s, simp add:take_Suc_conv_app_nth foldM_rev)
      using integrate_insert_commute' by fastforce
  qed  
qed

lemma  (in dist_execution) sent_before_recv:
  assumes "event_at (i,k) (Receive s m)"
  assumes "j < length (events i)"
  assumes "k < j" 
  shows "event_at s (Send m)  happened_immediately_before++ s (i,j)"
proof -
  have a:"event_at s (Send m)"
    using assms no_data_corruption by blast
  hence "happened_immediately_before s (i,k)" 
    using assms by (cases s, simp, metis (mono_tags, lifting) event.simps(6))
  hence "(happened_immediately_before)++ s (i,j)" using happened_before_same 
    by (meson assms(2) assms(3) tranclp_into_tranclp2)
  thus ?thesis using a by blast
qed

lemma (in dist_execution) irrefl_p: "irreflp (happened_immediately_before++)" 
  by (meson acyclic_def dist_execution.acyclic_happened_before
      dist_execution_axioms irreflpI tranclp_unfold)

lemma (in dist_execution) new_messages_keep_consistency:
  assumes "consistent M"
  assumes "event_at i (Send m)"
  assumes "set (received_messages i)  M"
  assumes "i  I ` insert_messages M"
  shows "consistent (insert m M)"
proof -
  have a:"is_valid_state_id i" using assms(2) by (cases i, simp)
  consider 
    (1) "(n σ. Inr m = (state i)  (λs. create_insert s n σ i))" |
    (2) "(n.   Inr m = (state i)  (λs. create_delete s n))" 
    by (metis (full_types) send_correct assms(2))
  then show ?thesis 
    proof (cases)
    case 1
    then obtain s n' σ where s_def:
      "Inr s = state i" "Inr m = create_insert s n' σ i" 
      by (cases "state i", simp, simp add:bind_def, blast)
    moreover have "is_associated_string (set (received_messages i)) s"
      using a assms(1) assms(3) apply (cases i, simp only:received_messages_eff)
      using s_def(1) state_is_associated_string'
      by (simp, metis (mono_tags, lifting) is_certified_associated_string.simps(1))
    ultimately show ?thesis using create_insert_consistent s_def assms 
      by (metis Un_insert_right sup_bot.right_neutral)
  next
    case 2
    then obtain s n' where s_def:
      "Inr s = state i" "Inr m = create_delete s n'" 
      by (cases "state i", simp, simp add:bind_def, blast)
    moreover have "is_associated_string (set (received_messages i)) s"
      using a assms(1) assms(3) apply (cases i, simp only:received_messages_eff)
      using s_def(1) state_is_associated_string'
      by (simp, metis (mono_tags, lifting) is_certified_associated_string.simps(1))
    ultimately show ?thesis using create_delete_consistent s_def assms 
      by (metis Un_insert_right sup_bot.right_neutral)
  qed
qed

lemma (in dist_execution) sent_messages_consistent:
  "consistent {m. (i. event_at i (Send m))}"
proof -
  obtain ids where ids_def: "set ids = {i. is_valid_event_id i}  
    sorted_wrt (to_ord (happened_immediately_before)) ids  distinct ids"
    using top_sort finite_valid_event_ids  by (metis acyclic_happened_before)
  have "x y. happened_immediately_before++ x y  x  set ids  y  set ids"
    using converse_tranclpE ids_def tranclp.cases by fastforce
  hence a:"x y. happened_immediately_before++ x y 
    (i j. i < j  j < length ids  ids ! i = x  ids ! j = y)"
    by (metis top_sort_eff ids_def  distinct_Ex1 irrefl_p)
  define n where "n = length ids"
  have "n  length ids  consistent (make_set n (λk x. event_at (ids ! k) (Send x)))"
  proof (induction n)
    case 0
    then show ?case using empty_consistent by simp
  next
    case (Suc n)
    moreover obtain i j where ij_def: 
      "ids ! n = (i,j)" "n < length ids"
      "is_valid_event_id (i,j)" "is_valid_state_id (i,j)"
      by (metis Suc.prems Suc_le_lessD ids_def is_valid_event_id.elims(2) is_valid_state_id.simps
          le_eq_less_or_eq mem_Collect_eq nth_mem)
    moreover have "set (received_messages (i,j))  make_set n (λk x. event_at (ids ! k) (Send x))"
      using ij_def apply (simp add:received_messages_eff del:received_messages.simps, rule_tac subsetI)
      using sent_before_recv a apply (simp add:make_set_def) 
      by (metis (no_types, hide_lams) distinct_Ex1 ids_def in_set_conv_nth)
    moreover have "(i,j)  I ` insert_messages (make_set n (λk x. event_at (ids ! k) (Send x)))"
        apply (simp add:insert_messages_def image_iff make_set_def del:event_at.simps)  
        using ids_def le_eq_less_or_eq nth_eq_iff_index_eq send_insert_id  
        by (metis dual_order.strict_trans1 ij_def(1) ij_def(2) less_not_refl)
    ultimately show ?case using Suc
      apply (cases "events i ! j")
      using new_messages_keep_consistency [where i = "(i,j)"] by simp+
  qed
  moreover have "make_set n (λk x. event_at (ids ! k) (Send x)) = {x. (i. event_at i (Send x))}" 
    apply (simp add:make_set_def n_def, rule set_eqI, subst surjective_pairing, simp only:event_pred.simps)
    using ids_def apply simp 
    by (metis fst_conv in_set_conv_nth is_valid_event_id.simps mem_Collect_eq prod.exhaust_sel snd_conv) 
  ultimately show ?thesis using ids_def n_def by simp
qed

lemma (in dist_execution) received_messages_were_sent:
  assumes "is_valid_state_id (i,j)"
  shows "make_set j (λk m. (s. event_at (i, k) (Receive s m)))  {m. i. event_at i (Send m)}"
  using no_data_corruption by (simp add:make_set_def, rule_tac subsetI, fastforce)

lemma (in dist_execution) state_is_associated_string:
  assumes "is_valid_state_id i"
  shows "is_certified_associated_string (set (received_messages i)) (state i)"
  using state_is_associated_string' received_messages_eff
    sent_messages_consistent received_messages_were_sent assms by (cases i, simp)

end

Theory SEC

section ‹Strong Eventual Consistency \label{sec:strong_eventual_consistency}›

theory SEC
  imports StrongConvergence
begin

text ‹In the following theorem we establish that all reached states are successful. This
implies with the unconditional termination property (Section \ref{sec:integrate_term}) of it that 
the integration algorithm never fails.›

theorem (in dist_execution) no_failure:
  fixes i
  assumes "is_valid_state_id i"
  shows "isOK (state i)"
  apply (cases "state i")
  by (metis assms state_is_associated_string is_certified_associated_string.simps(2), simp)

text ‹The following theorem establishes that any pair of peers having received the same
set of updates, will be in the same state.›

theorem (in dist_execution) strong_convergence:
  assumes "is_valid_state_id i"
  assumes "is_valid_state_id j"
  assumes "set (received_messages i) = set (received_messages j)"
  shows "state i = state j"
  using state_is_associated_string is_certified_associated_string_unique by (metis assms)

text ‹As we noted in Section~\ref{sec:networkModel}, we have not assumed eventual delivery, but
  a corollary of this theorem with the eventual delivery assumption implies eventual consistency.
  Since finally all peer would have received all messages, i.e., an equal set.›

section ‹Code generation›

export_code integrate create_insert create_delete in Haskell
  module_name WOOT file_prefix "code"

section ‹Proof Outline\label{sec:proof_outline}›

text ‹
  In this section we outline and motivate the approach we took to prove the strong eventual
  consistency of WOOT.

  While introducing operation-based CRDTs Shapiro et al. also establish
  \cite{shapiro2011conflict}[Theorem 2.2]. If the following two conditions are met:
  \begin{itemize}
    \item
      Concurrent operations commute, i.e., if a pair of operations @{text "m1"},
      @{text "m2"} is concurrent with respect to the order induced by the happened-before
      relation, and they are both applicable to a state @{text "s"}, then the message
      @{text "m1"} (resp. @{text "m2"}) is still applicable on the state reached by
      applying  @{text "m2"} (resp. @{text "m1"}) on @{text "s"} and the resulting
      states are equal.
    \item Assuming causal delivery, the messages are applicable.
  \end{itemize}
  Then the CRDT has strong convergence.
  The same authors extend the above result in \cite[Proposition 2.2]{shapiro:inria-00555588}
  to more general delivery orders $\xrightarrow{d}$ (weaker than the one induced by the
  happened-before relation), i.e., two messages may be causally dependent but concurrent with
  respect to $\xrightarrow{d}$. Assuming operations that are concurrent with respect to
  $\xrightarrow{d}$ commute, and messages are applicable, when the
  delivery order respects $\xrightarrow{d}$ then again the CRDT has strong convergence.

  A key difficulty of the consistency proof of the WOOT framework is that the applicability
  condition for the WOOT framework has three constraints:
  \begin{enumerate}
    \item \label{en:proof:deps_are_met} Dependencies must be met.
    \item \label{en:proof:id_distinct} Identifiers must be distinct.
    \item The order must be consistent, i.e. the predecessor W-character must appear before the
      successor W-character in the state an insert message is being integrated.
  \end{enumerate}

  The first constraint is a direct consequence of the semantic causal delivery order. The uniqueness
  of identifiers can be directly established by analyzing the implementation of the message creation
  algorithms. Alternatively, Gomes et al.~\cite{gomes2017verifying} use an axiomatic approach, where
  they require the underlying network protocol to deliver messages with unique identifiers. They
  provide a formal framework in Isabelle/HOL that can be used to show consistency of arbitrary
  CRDTs. Their results could be used to establish constraints \ref{en:proof:deps_are_met} and
  \ref{en:proof:id_distinct}.

  The last constraint is the most intricate one, and forces us to use a different method to
  establish the strong eventual consistency. The fact that the order constraint is fulfilled is a
  consequence of the consistency property. But the current fundamental lemmas require applicability
  of the operations in the first place to establish consistency, which would result in a circular
  argument.

  Zeller et. al. actually predict the above circumstance in the context of state-based CRDTs
  \cite{DBLP:conf/forte/ZellerBP14}:
  \begin{displayquote}
  In theory it could even be the case that there are two reachable states for which the merge
  operation does not yield the correct result, but where the two states can never be reached in the
  same execution.
  \end{displayquote}

  Because of the above, we treat WOOT as a distributed message passing algorithm and show
  convergence by establishing a global invariant, which is maintained during the execution of the
  framework. The invariant captures that the W-characters appear in the same order on all peers.
  It has strong convergence as a consequence, in the special case, when peers have received
  the same set of updates. It also implies that the generated messages will be applicable.

  \begin{figure}
    \centering
    \begin{tikzpicture}[
      statenode/.style={circle, draw=black, fill=black!20, thick, minimum size=5mm},
      curstatenode/.style={circle, draw=black, fill=black!60, thick, minimum size=5mm},
      peernode/.style={rectangle, draw=black, thick, minimum size=5mm},
    ]
    %Nodes
    \node[peernode] (peerA) at (1.5cm, 3cm) {Peer A};
    \node[peernode] (peerB) at (1.5cm, 2cm) {Peer B};
    \node[peernode] (peerC) at (1.5cm, 1cm) {Peer C};
    \node[statenode] (stateA2) at (4cm, 3cm) {};
    \node[curstatenode] (stateB2) at (5cm, 2cm) {};
    \node[statenode] (stateC2) at (3.5cm, 1cm) {};
    \node[statenode] (stateA3) at (5.5cm, 3cm) {};
    \node[statenode] (stateB3) at (7cm, 2cm) {};
    \node[statenode] (stateC3) at (6.5cm, 1cm) {};
    \node[statenode] (stateA4) at (7.5cm, 3cm) {};
    \draw[->] (peerA.east) -- (stateA2.west);
    \draw[->] (peerB.east) -- (stateB2.west);
    \draw[->] (peerC.east) -- (stateC2.west);
    \draw[->] (stateA2.east) -- (stateA3.west);
    \draw[->] (stateB2.east) -- (stateB3.west);
    \draw[->] (stateC2.east) -- (stateC3.west);
    \draw[->] (stateC2) -- (stateA2);
    \draw[->] (stateC2) -- (stateB2);
    \draw[->] (stateA3) -- (stateC3);
    \draw[->] (stateA3) -- (stateB3);
    \draw[->] (stateA3) -- (stateA4);
    \draw (5cm,3.5cm) to[bend right] (4.8cm,0.5cm);
    \end{tikzpicture}
    \caption{Example state graph, where the consistency is established left of the bend curve.}
    \label{fig:state_graph}
  \end{figure}

  In Figure~\ref{fig:state_graph}, we exemplify an induction step in a proof over the execution
  of the framework. The invariant is established for all states left of the dashed lines, and we
  show that it remains true if we include the state, drawn in dark gray. Note that induction
  proceeds in an order consistent with the happened-before relation.

  The technique we are using is to define a relation @{term is_associated_string} from a set of
  messages to the final state their application leads to. Crucially, that relation can be defined
  in a message-order independent way. We show that it correctly models the behaviour of Algorithm
  @{term "integrate"} by establishing that applying the integration algorithm to the associated
  string of a set @{term "M"} leads to the associated string of the set @{term "M  {m}"}
  in Proposition @{thm [source] integrate_insert_commute}.

  We also show that at most one @{text s} fulfills @{term "is_associated_string M s"},
  which automatically implies commutativity (cf. Lemma @{thm [source] "associated_string_unique"}).

  Note that the domain of the relation @{term "is_associated_string"} consists of the sets of
  messages that we call @{term "consistent"}. We show that, in every state of a peer, the set of
  received messages will be consistent.
  The main ingredient required for the definition of a consistent set of messages as the relation
  @{term "is_associated_string"} are \emph{sort keys} associated to the W-characters, which we will
  explain in the following Section.
›

subsection ‹ Sort Keys ›

text ‹
  There is an implicit sort key, which is deterministically computable, using the immutable data
  associated to a W-character and the data of the W-characters it (transitively) depends on.

  We show that Algorithm @{term "integrate"} effectively maintains the W-characters ordered with
  respect to that sort key, which is the reason we can construct the mapping
  @{term "is_associated_string"} in a message-order
  independent way. An alternative viewpoint would be to see Algorithm @{term "integrate_insert"} as
  an optimized version of a more mundane algorithm, that just inserts the W-characters using this
  implicit sort key.

  Since the sort key is deterministically computable using the immutable data associated to a
  W-character and the data of the W-characters it (transitively) depends on, all peers could
  perform this computation independently, which leads to the conclusion that the W-characters
  will be ordered consistently across all peers.

  The construction relies on a combinator @{term "Ψ"} that computes the sort key for a
  W-character, and which requires as input:
  \begin{itemize}
    \item The unique identifier associated to a W-character.
    \item The sort keys of the predecessor/successor W-characters.
  \end{itemize}
  Its values are elements of a totally ordered space.

  Note that the predecessor (resp. successor) W-character of a W-character is the W-character that
  was immediately before (resp. after) it at the time it was inserted. Like its unique identifier,
  it is immutable data associated with that W-character. Sometimes a W-character is inserted at the
  beginning (resp. end) of the string. For those W-characters, we use the special smallest
  (resp. largest) sort keys, denoted by @{term ""} (resp. @{term ""}) as predecessor
  (resp. successor). These keys themselves are never associated to a W-character.

  We will write @{term (l,u) i"} for the value computed by the combinator for a W-character
  with identifier @{term "i"}, assuming the sort key of its predecessor (resp. successor) is
  @{term "l"} (resp. @{term "u"}).

  For example, the sort key for a W-character with identifier @{term "i"} inserted in an empty
  string (hence its predecessor is @{term ""} and its successor is @{term ""}) 
  will be  @{term (,) i"}. A W-character
  inserted between that character and the end of the string, with identifier j, would be assigned
  the sort key @{term (Ψ (,) i,) j"}.

  The sort key needs to fulfill a couple of properties, to be useful:

  There should never be a pair of W-characters with the same sort key. Note, if this happens, even
  if those W-characters were equal or ordered consistently, we would not be able to insert a new
  W-character between those W-characters.

  Since the W-characters have themselves unique identifiers, a method to insure the above property
  is to require that @{term "Ψ"} be injective with respect to the identifier of the W-character
  it computes a sort key for, i.e.,
  @{term (l,u) i = Ψ (l',u') i'  i = i'"}.

  Another essential property is that the W-characters with predecessor having the sort key
  @{term "l"} and successor having the sort key @{term "u"}  should have a sort key that is between
  @{term "l"} and @{term "u"}, such that the W-character is inserted between the preceding and
  succeeding W-character, i.e., @{text "l < Ψ (l,u) i < u"}.

  This latter property ensures intention preservation, i.e. the inserted W-character will be placed
  at the place the user intended.

  If we review function @{term "concurrent"}, then we see that the algorithm compares W-characters
  by identifier, in the special case, when the inserted W-character is compared to a W-character
  whose predecessor and successor are outside of the range it is to be inserted in. A careful
  investigation, leads to the conclusion that:

  If @{text "l ≤ l' < Ψ (l,u) i < u' ≤ u"} then @{text "Ψ(l,u) i"} can be compared
  with @{text "Ψ(l',u') i'"} by comparing @{text "i"} with @{text "i'"}, i.e.:
  \begin{itemize}
    \item @{text "i < i' ⟹ Ψ (l,u) i < Ψ(l',u') i'"}
  \end{itemize}

  In Section \ref{sec:psi} we show that a combinator @{term "Ψ"} with the above properties can
  be constructed (cf. Propositions @{thm [source] psi_narrow psi_mono psi_elem}).
  Using the sort keys we can define the notion of a consistent set of messages as well as the
  relation @{term "is_associated_string"} in a message-order independent way.›

subsection ‹ Induction ›

text ‹
  We have a couple of criteria that define a consistent set of messages:

  \begin{itemize}
    \item Each insert message in the set has a unique identifier.
    \item If a message depends on another message identifier, a message with that identifier will
      be present. Note that for insert messages, these are the predecessor/successor W-characters
      if present. For delete messages it is the corresponding insert message.
    \item The dependencies form a well-order, i.e., there is no dependency cycle.
    \item It is possible to assign sort keys to each insert message, such that
      the assigned sort key for each insert message is equal to the value returned by the
      @{term "Ψ"} for it, using the associated sort keys of its predecessor and successors,
      i.e.,
      @{term "a (P m) < a (S m) 
              a I m = Ψ (a (P m), a (S m)) (I m)"}.
      Note that we also require that sort key of the predecessor is smaller than the sort key of the
      successor.
  \end{itemize}

  The relation @{term "is_associated_string"} is then defined by ordering the insert messages
  according to the assigned sort keys above and marking W-characters, for which there are delete
  messages as deleted.

  The induction proof (Lemma @{thm [source] dist_execution.sent_messages_consistent}) over the
  states of the framework is straight forward: Using Lemma @{thm [source] top_sort} we find a
  possible order of the states consistent with the happened before relation. The induction invariant
  is that the set of generated messages by all peers is
  consistent (independent of whether they have been received by all peers (yet)). The latter also
  implies that the subset a peer has received in any of those states is consistent, using the
  additional fact that each messages dependencies will be delivered before the message itself
  (see also Lemma @{thm [source] consistent_subset} and
  Proposition @{thm [source] integrate_insert_commute'}).
  For the induction step, we rely on the results from Section \ref{sec:create_consistent} that any
  additional created messages will keep the set of messages consistent and that the peers' states
  will be consistent with the (consistent subset of) messages they received (Lemma @{thm [source]
  dist_execution.state_is_associated_string'}).›
end

Theory Example

section ‹Example\label{sec:example}›

theory Example
  imports SEC
begin

text ‹In this section we formalize the example from Figure \ref{fig:session} for a possible run of 
the WOOT framework with three peers, each performing an edit operation. We verify that it fulfills
the conditions of the locale @{locale dist_execution} and apply the theorems.›

datatype example_peers
  = PeerA
  | PeerB
  | PeerC
derive linorder example_peers

fun example_events :: "example_peers  (example_peers, char) event list" where
  "example_events PeerA = [
      Send (Insert (InsertMessage  (PeerA, 0)  CHR ''B'')),
      Receive (PeerA, 0) (Insert (InsertMessage  (PeerA, 0)  CHR ''B'')),
      Receive (PeerB, 0) (Insert (InsertMessage  (PeerB, 0)  CHR ''A'')),
      Receive (PeerC, 1) (Insert (InsertMessage (PeerA, 0)  (PeerC, 1)  CHR ''R''))
  ]" |
  "example_events PeerB = [
      Send (Insert (InsertMessage  (PeerB, 0)  CHR ''A'')),
      Receive (PeerB, 0) (Insert (InsertMessage  (PeerB, 0)  CHR ''A'')),
      Receive (PeerA, 0) (Insert (InsertMessage  (PeerA, 0)  CHR ''B'')),
      Receive (PeerC, 1) (Insert (InsertMessage (PeerA, 0)  (PeerC, 1)  CHR ''R''))
  ]" |
  "example_events PeerC = [
      Receive (PeerA, 0) (Insert (InsertMessage  (PeerA, 0)  CHR ''B'')),
      Send (Insert (InsertMessage (PeerA, 0)  (PeerC, 1)  CHR ''R'')),
      Receive (PeerC, 1) (Insert (InsertMessage (PeerA, 0)  (PeerC, 1)  CHR ''R'')),
      Receive (PeerB, 0) (Insert (InsertMessage  (PeerB, 0)  CHR ''A''))
  ]"

text ‹The function @{term example_events} returns the sequence of events that each 
peer evaluates. We instantiate the preliminary context by showing that the set of 
peers is finite.›

interpretation example: dist_execution_preliminary "example_events"
proof
  have a:"UNIV = {PeerA, PeerB, PeerC}" 
    using example_events.cases by auto
  show "finite (UNIV :: example_peers set)" by (simp add:a)
qed

text ‹
  To prove that the @{term happened_before} relation is acyclic, we provide an  order on the state
  that is consistent with it, i.e.:
  \begin{itemize}
  \item  The assigned indicies for
  successive states of the same peer are increasing.
  \item The assigned index of a state receiving a message is 
    larger than the assigned index of the messages source state.
  \end{itemize}
›

fun witness_acyclic_events :: "example_peers event_id  nat"
  where 
    "witness_acyclic_events (PeerA, 0) = 0" |
    "witness_acyclic_events (PeerB, 0) = 1" |
    "witness_acyclic_events (PeerA, (Suc 0)) = 2" |
    "witness_acyclic_events (PeerB, (Suc 0)) = 3" |
    "witness_acyclic_events (PeerC, 0) = 4" |
    "witness_acyclic_events (PeerC, (Suc 0)) = 5" |
    "witness_acyclic_events (PeerC, (Suc (Suc 0))) = 6" |
    "witness_acyclic_events (PeerC, (Suc (Suc (Suc 0)))) = 7" |
    "witness_acyclic_events (PeerA, (Suc (Suc 0))) = 8" |
    "witness_acyclic_events (PeerA, (Suc (Suc (Suc 0)))) = 9" |
    "witness_acyclic_events (PeerB, (Suc (Suc 0))) = 8" |
    "witness_acyclic_events (PeerB, (Suc (Suc (Suc 0)))) = 9" |
    "witness_acyclic_events (PeerA, (Suc (Suc (Suc (Suc n))))) = undefined" |
    "witness_acyclic_events (PeerB, (Suc (Suc (Suc (Suc n))))) = undefined" |
    "witness_acyclic_events (PeerC, (Suc (Suc (Suc (Suc n))))) = undefined"

text ‹
  To prove that the created messages make sense, we provide the edit operation
  that results with it. The first function is the inserted letter and the second
  function is the position the letter was inserted.
›

fun witness_create_letter :: "example_peers event_id  char"
  where 
    "witness_create_letter (PeerA, 0) = CHR ''B''" |
    "witness_create_letter (PeerB, 0) = CHR ''A''" |
    "witness_create_letter (PeerC, Suc 0) = CHR ''R''"

fun witness_create_position :: "example_peers event_id  nat"
  where 
    "witness_create_position (PeerA, 0) = 0" |
    "witness_create_position (PeerB, 0) = 0" |
    "witness_create_position (PeerC, Suc 0) = 1"

text ‹
  To prove that dependencies of a message are received before a message, we
  provide the event id as well as the message, when the peer received a 
  messages dependency.›

fun witness_deps_received_at :: "example_peers event_id  example_peers event_id  nat"
  where
    "witness_deps_received_at (PeerA, Suc (Suc (Suc 0))) (PeerA, 0) = 1" |
    "witness_deps_received_at (PeerB, Suc (Suc (Suc 0))) (PeerA, 0) = 2" |
    "witness_deps_received_at (PeerC, Suc (Suc 0)) (PeerA, 0) = 0"

fun witness_deps_received_is :: "example_peers event_id  example_peers event_id  (example_peers event_id, char) insert_message"
  where
    "witness_deps_received_is (PeerA, Suc (Suc (Suc 0))) (PeerA, 0) = (InsertMessage  (PeerA, 0)  CHR ''B'')" |
    "witness_deps_received_is (PeerB, Suc (Suc (Suc 0))) (PeerA, 0) = (InsertMessage  (PeerA, 0)  CHR ''B'')" |
    "witness_deps_received_is (PeerC, Suc (Suc 0)) (PeerA, 0) = (InsertMessage  (PeerA, 0)  CHR ''B'')"

lemma well_order_consistent:
  fixes i j 
  assumes "example.happened_immediately_before i j"
  shows "witness_acyclic_events i < witness_acyclic_events j"
  using assms
  apply (rule_tac [!] witness_acyclic_events.cases [where x="i"])
  apply (rule_tac [!] witness_acyclic_events.cases [where x="j"])
  by simp+

text ‹Finally we show that the @{term example_events} meet the assumptions
  for the distributed execution context.›

interpretation example: dist_execution "example_events"
proof
  fix i s m
  show 
    "dist_execution_preliminary.event_at example_events i (Receive s m) 
     dist_execution_preliminary.event_at example_events s (Send m)"
    apply (rule_tac [!] witness_acyclic_events.cases [where x="i"])
    by simp+
next
  fix i j s :: "example_peers event_id"
  fix m
  show "example.event_at i (Receive s m) 
       example.event_at j (Receive s m)  fst i = fst j  i = j"
  apply (rule_tac [!] witness_acyclic_events.cases [where x="i"])
  apply (rule_tac [!] witness_acyclic_events.cases [where x="j"])
    by simp+
next
  have "wf (inv_image {(x,y). x < y} witness_acyclic_events)"
    by (simp add: wf_less)
  moreover have "{(x, y). example.happened_immediately_before x y} 
    inv_image {(x,y). x < y} witness_acyclic_events" 
    using well_order_consistent by auto
  ultimately have "wfP example.happened_immediately_before" 
    using well_order_consistent wfP_def wf_subset by blast
  thus "acyclicP example.happened_immediately_before"
    using wfP_acyclicP by blast
next
  fix m s i j i'
  have "example.event_at (i, j) (Receive s m) 
       i'  deps m 
      example.event_at (i, witness_deps_received_at (i, j) i') (Receive (I (witness_deps_received_is (i, j) i')) (Insert (witness_deps_received_is (i, j) i')))  witness_deps_received_at (i, j) i' < j  I (witness_deps_received_is (i, j) i') = i'"
    apply (rule_tac [!] witness_acyclic_events.cases [where x="(i,j)"])
    by simp+
  thus "example.event_at (i, j) (Receive s m) 
       i'  deps m 
       s' j' m'.
          example.event_at (i, j') (Receive s' (Insert m'))  j' < j  I m' = i'"
    by blast
next
  fix m i
  have "example.event_at i (Send m) 
        Inr m = example.state i  (λs. create_insert s (witness_create_position i) (witness_create_letter i) i)"
    apply (rule_tac [!] witness_acyclic_events.cases [where x="i"])
    by (simp add:ext_ids_def)+
  thus "example.event_at i (Send m) 
           (n σ. return m = example.state i  (λs. create_insert s n σ i)) 
           (n. return m = example.state i  (λs. create_delete s n))"
    by blast
qed

text ‹As expected all peers reach the same final state.›

lemma
  "example.state (PeerA, 4) = Inr [
    InsertMessage  (PeerA, 0)  (Some CHR ''B''),
    InsertMessage  (PeerB, 0)  (Some CHR ''A''),
    InsertMessage (PeerA, 0)  (PeerC, 1)  (Some CHR ''R'')]"
  "example.state (PeerA, 4) = example.state (PeerB, 4)"
  "example.state (PeerB, 4) = example.state (PeerC, 4)"
  by (simp del:substr_simp add:ext_ids_def substr.simps less_example_peers_def)+

text ‹We can also derive the equivalence of states using the strong
  convergence theorem. For example the set of received messages in
  the third state of peer A and B is equivalent, even though they were
  not received in the same order:›

lemma
  "example.state (PeerA, 3) = example.state (PeerB, 3)"
proof -
  have "example.is_valid_state_id (PeerA, 3)" by auto
  moreover have "example.is_valid_state_id (PeerB, 3)" by auto
  moreover have
    "set (example.received_messages (PeerA, 3)) = 
     set (example.received_messages (PeerB, 3))"
    by auto
  ultimately show ?thesis
    by (rule example.strong_convergence)
qed

text ‹Similarly we can conclude that reached states are successful.›
lemma
  "isOK (example.state (PeerC, 4))"
proof -
  have "example.is_valid_state_id (PeerC, 4)" by auto
  thus ?thesis by (rule example.no_failure)
qed

end