# Session WOOT_Strong_Eventual_Consistency

section ‹Preliminary Notes›

subsection ‹Algorithms in Isabelle›
imports
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
\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.

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
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.
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))"

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"

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"
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'"
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)"
hence "⋀x. x ∈ set (drop (Suc l) s) ⟹ x > v"
using assms apply (simp)
leI le_less_trans less_imp_le sorted_wrt_iff_nth_less)
ultimately show ?thesis
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"
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
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}"

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"

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"

lemma to_woot_character_keeps_S [simp]: "S (to_woot_character M m) = S m"

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
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 ⊢ ⇒ ⊢ | ⊣ ⇒ ⊣))"
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 {} []"
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)"
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
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

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 σ))"
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)"
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 σ))"
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
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"
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 (meson filter_is_subset imageI in_set_conv_nth subset_code(1))
apply (cases "u = length (filter is_visible s)")
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}) = {}"
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"
then show ?thesis by simp
next
case False
hence "set (nths s {k. l < Suc k ∧ Suc k < u}) = {}"
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)
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)
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
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
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 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

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
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
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
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)"
thus "⟦i⟧ ∈ set (ext_ids s)"
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})"
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
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)"
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)
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
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)"
moreover have "¬(Suc (length s) < u)" using assms(2)
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
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 (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' = ⊣"
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
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"

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)"
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}))"
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))"
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)

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)))"

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}"
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
moreover have "is_delete m ∨ m ∉ (make_set j (λk m. ∃s. event_at (i,k) (Receive s m)))"
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)
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 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

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)"
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"
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
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
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)"
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 ⟹
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"])
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
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`