# 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 ≠ {} ⟹ (∃z∈Q. ∀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 "∃z∈Q. ∀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 "m⇩_{1}"}, @{text "m⇩_{2}"} 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 "m⇩_{1}"} (resp. @{text "m⇩_{2}"}) is still applicable on the state reached by applying @{text "m⇩_{2}"} (resp. @{text "m⇩_{1}"}) 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