A Proof for Log Matching Property of Raft - 俺の Colimit を越えてゆけ

背景
Log Matching Property の証明
参考資料

背景

分散合意アルゴリズム Raft は kubernetes のクラスターの構成情報を保存する etcd の内部で使われておりお世話になっている方も多いアルゴリズムだと思います。
この記事では Raft の満たす重要な性質である Log Matching Property について証明します。

元々、『Raft を TLA+ で検証する』というタイトルの記事を書こうと考えて Raft の考案者 Diego Ongaro の博士論文を読み始めました（その記事は後日公開予定です）。
アルゴリズムは論文の 3 章に書かれているのですが、そこで Raft が常に成り立つことを保証する 5 つの性質の 1 つとして Log Matching Property を挙げています。
Log Matching Property は次のような性質です。

異なるログの 2 つの entry が同じインデックスと term を持つ場合、それらは同じコマンドを格納する。
異なるログの 2 つの entry が同じインデックスと term を持つ場合、ログは先行するすべての entry で一致する。

Diego Ongaro はこれらの性質を証明するのではなく TLA+ という形式仕様記述言語を使用して検証しています。
実用上はそれで十分なのですが、論文中で Log Matching Property の証明について次のように言及しています。

1 つ目の特性は、leader が与えられた term の与えられたログインデックスを持つ entry を最大 1 つ作成し、entry はログ内での位置を決して変更しないという事実からきています。2 つ目の特性は、AppendEntries によって実行される一貫性チェックによって保証されます。

私は、形式的な証明を沢山してきているので、この内容を元に Log Matching Property を脳内で証明しようと試みたのですが全くできる気配がありませんでした。
例えば、「entry はログ内での位置を決して変更しない」ことも証明しないといけない性質なのに証明せずに使用しています。
また、「AppendEntries によって実行される一貫性チェック」に関しても、AppendEntries は実用上の理由により、 follower のログの最後の entry の term が leader のログの同じインデックスの entry の term と一致すると、それ以下のログは一致しているとみなして再帰的な処理をやめてしまいます。
再帰的な処理をやめるというのが証明をする上でとても厄介で、寧ろこのような最適化はせずに leader のログを丸々 follower にコピーするというアルゴリズムになっている方が性質の証明はずっと簡単です。

結局納得できる証明を構成するのに Stay Home 期間の 2 週間を費やしました。
証明をするためのポイントは、一見無関係に見える leader のログの間の関係性をどのように論理式で表現し公理として採用するかという点でした。
この公理が強すぎると、今証明しようとしている Log Matching Property 自体を公理に誤って入れ込んでしまう可能性があります。
実際私も 1 週間くらい考えた末に証明できたと思い記事を書いていたのですが、証明を見直してみると Log Matching Property を仮定するような公理を元に証明していることに気付きやり直しました。
公理の最終案は以下になります。

$Axiom$
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, t \neq L_{t}[i].term \Rightarrow \\
\forall (l \colon Log),\ \exists (l' \colon Log)(t' \colon Term),\, L_{t}[i].term \le t' \lt t \land AppendEntries(i, t, l) = AppendEntries(i, t', l')
\end{equation}

この公理が以下の 3 つの気持ちを表現していることを感じ取ってもらえるでしょうか。

Raft では leader は自身のログに自身の term の entry しか追加しないこと
term $t$ の leader のログに term $t’$ の entry があったとしてもその entry が term $t’$ の leader によって term $t$ の leader のログに書き込まれたとは限らないこと
leader 同士のログはこの関係を通して互いに関連していること

十分に形式的に証明をしたつもりではいますが、Coq 等で実際に証明したわけではないので 100% 正しいとは言えません。
もし、誤りを見つけた方がいたらコメント欄で教えていただけると幸いです。

Log Matching Property の証明

データ構造と述語の定義

Log Matching Property を証明するためにまずデータ構造と述語を定義します。記述は特定の言語を想定していません。

// Index, Term は Nat の別名
type Index = Nat
type Term = Nat

// Entry は Term を指定して作成
Inductive Entry = makeEntry : Term -> Entry

// Log は Entry の List
type Log = List Entry

log の index は 1 から始まるとし index 0 へのアクセスは undefined とします。また、log $l$ の部分リスト $l[i..0]$ は空リストであると定義します。

次に AppendEntries 関数を定義します。

Function AppendEntries(i: Index)(t: Term)(l: Log) : Log =
  if i = 0 then
    []
  else
    // AppendEntries で i-1 の log を作成して末尾に Lt[i] を追加
    if i > length(l) + 1 then
      AppendEntries(i-1, t, l)::Lt[i]
    elseif i = length(l) + 1 then
      // l の末尾の entry の term と Lt[i-1] の term が等しい場合は、l の後に Lt[i] を追加
      // そうでない場合は AppndEntries で i-1 の log を作成して末尾に Lt[i] を追加
      if l[i-1].term = Lt[i-1].term then
        l::Lt[i]
      else
        AppendEntries(i-1, t, l)::Lt[i]
      end
    else
      // i が length(l) + 1 より短い場合は l の末尾の entry を削除して AppendEntries を呼び出す
      AppendEntries(i, t, l[1..length(l)-1])
    end
  end

AppendEntries 関数は任意の index と term と log を受け取って長さが $i$ の log を返します。 $Lt$ は term $t$ における leader の log を表します。Raft では leader の log は時間とともに成長しますがここでは定数とし、 $i$ を変更することで模倣します。

log は entry のリストですが、Raft で扱う log は AppendEntries 関数を通して作成された log のみです。これを述語として表現します。

Inductive RaftLog : Term -> Log -> Prop :=
  | rlnil : ∀ (t: Term), RaftLog(t, [])
  | rlAppend:  ∀(t, t': Term)(l: Log)(i: Index), RaftLog(t', l) -> t' <= t -> RaftLog(t, AppendEntries(i, t, l)).

rlnil は任意の空リストは任意の term で RaftLog であるという意味です。
rlAppend は log $l$ が term $t' \le t$ で RaftLog( $t'$ , $l$ ) であるなら AppendEntries( $i$ , $t$ , $l$ ) は RaftLog であるという意味です。
任意の log を取り扱うのではなく、RaftLog(t, l) という述語が真になる log のみを考察の対象にします。

AppendEntries 関数の性質

AppendEntries 関数の性質について 4 つの Lemma(補題) を証明します。

Lemma AppendEntries 1 はアルゴリズム中の $i \lt length(l) + 1$ の場合に関する補題です。
log の長さが最終的な長さよりも長い場合は再帰的に末尾の entry が削除されます。AppendEntries に log をそのまま渡しても、log を先に短くしてから渡しても結果は変わりません。

$Lemma\ AppendEntries\ 1$
\begin{equation}
\forall (l\colon Log)(i\colon Index)(t \colon Term),\, i \le length(l) \Rightarrow AppendEntries(i, t, l) = AppendEntries(i, t, l[1..(i\!-\!1)])
\end{equation} $Proof$
log $l$ に関する帰納法を用いる。

$l = []$ の場合

$i \le length(l)$ より $i = 0$ であるから $AppendEntries(0, t, []) = AppendEntries(0, t, [])$ が成り立つ。

$l = l'::e$ の場合

帰納法の仮定より次のことが成り立つ。
\begin{equation}
\forall (i\colon Index)(t\colon Term),\, i \le length(l') \Rightarrow AppendEntries(i, t, l') = AppendEntries(i, t, l'[1..(i\!-\!1)])
\end{equation}
$i \le length(l'::e)$ より $i = length(l'::e)$ の場合と $i \lt length(l'::e)$ の場合を考える。

$i = length(l'::e)$ の場合

$i \lt length(l'::e)+1$ であるから
\begin{align*}
AppendEntries(i, t, l'::e) &= AppendEntries(i, t, l') \\
&= AppendEntries(i, t, (l'::e)[1..(i\!-\!1)])
\end{align*}

$i \lt length(l'::e)$ の場合

$i \lt length(l'::e)$ であるから
\begin{align*}
AppendEntries(i, t, l'::e) &= AppendEntries(i, t, l')
\end{align*}
が成り立つ。一方で、 $i \le length(l')$ であるから仮定より次のことが成り立つ。
\begin{align*}
AppendEntries(i, t, l') &= AppendEntries(i, t, l'[1..(i\!-\!1)]) \\
&= AppendEntries(i, t, (l'::e)[1..(i\!-\!1)])
\end{align*}

$\square$

Lemma AppendEntries 2 は空リストに対して term $t$ において AppendEntries を実行すると term $t$ の leader の log と一致することを意味します。

$Lemma\ AppendEntries\ 2$
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, AppendEntries(i, t, [ ]) = L_{t}[1..i]
\end{equation} $Proof$
index $i$ に関する帰納法を用いる。

$i = 0$ の場合

\begin{equation}
AppendEntries(0, t, [ ]) = [] = L_{t}[1..0]
\end{equation}

$i = k$ の場合

$i \lt k$ のとき次式が成り立つと仮定する。
\begin{equation}
\forall (t \colon Term),\, AppendEntries(i, t, [ ]) = L_{t}[1..i]
\end{equation}
$i = k \gt 0$ とすると、

$k \gt 1$ の場合

\begin{align*}
AppendEntries(k, t, [ ]) &= AppendEntries(k-1, t, [ ])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k] \ (\because \rm{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

$k = 1$ の場合

\begin{align*}
AppendEntries(1, t, [ ]) &= AppendEntries([ ], t, [ ])::L_{t}[1] \\
&= L_{t}[1]
\end{align*}

$\square$

証明は省略しますが Lemma AppendEntries 2 より term $t$ の leader の log の部分 log $L_{t}[1..i]$ は RaftLog であることが示せます。

$Lemma\ RaftLog\ 1$
\begin{equation}
\forall (i \colon Index)(t\colon Term),\, RaftLog(t, L_{t}[1..i])
\end{equation}

Lemma AppendEntries 3 は任意の log $l$ から term $t$ において長さ $i$ の log を AppendEntries で作成すると、末尾は term $t$ の leader の $i$ 番目の entry と一致することを意味します。

$Lemma\ AppendEntries\ 3$
\begin{equation}
\forall (i\colon Index)(t \colon Term)(l\colon Log),\, AppendEntries(i, t, l)[i] = L_{t}[i]
\end{equation} $Proof$

$i = 0$ の場合

\begin{equation}
AppendEntries(0, t, l)[0] = undefined = L_{t}[0]
\end{equation}

$i \gt length(l)+1$ の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (AppendEntries(i\!-\!1,t,l)::Lt[i])[i] \\
&= Lt[i]
\end{align*}

$i = length(l)+1$ の場合
$l[i\!-\!1].term = L_{t}[i\!-\!1].term$ の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (l::Lt[i])[i] \\
&= Lt[i]
\end{align*}

$l[i\!-\!1].term \neq L_{t}[i\!-\!1].term$ の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= (AppendEntries(i\!-\!1,t,l)::Lt[i])[i] \\
&= Lt[i]
\end{align*}

$i \lt length(l)+1$ の場合

\begin{align*}
AppendEntries(i, t, l)[i] &= AppendEntries(i,t,l[1..(length(l)\!-\!1)])[i] \\
&= AppendEntries(i,t,l[1..(i\!-\!1)])[i] \ (\because Lemma\ AppendEntries\ 1) \\
&= Lt[i] \ (\because i = length(l)+1 \rm{の場合と同様の議論により})
\end{align*}

$\square$

Lemma AppendEntries 4 は任意の log $l$ から term $t$ において長さ $i$ の log を AppendEntries で作成すると、 $i\!-\!1$ 番目の entry の term は term $t$ の leader の $i\!-\!1$ 番目の entry の term と一致することを意味します。

$Lemma\ AppendEntries\ 4$
\begin{equation}
\forall (i\colon Index)(t \colon Term)(l\colon Log),\, i \gt 1 \Rightarrow AppendEntries(i, t, l)[i\!-\!1].term = L_{t}[i\!-\!1].term
\end{equation} $Proof$

$i \gt length(l)+1$ の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= (AppendEntries(i\!-\!1,t,l)::L_{t}[i])[i\!-\!1].term \\
&= AppendEntries(i\!-\!1,t,l)[i\!-\!1].term \\
&= Lt[i\!-\!1].term \ (\because Lemma\ AppendEntries\ 3)
\end{align*}

$i = length(l)+1$ の場合
$l[i\!-\!1].term = L_{t}[i\!-\!1].term$ の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= (l::L_{t}[i])[i\!-\!1].term \\
&= l[i\!-\!1].term \\
&= Lt[i\!-\!1].term
\end{align*}

$l[i\!-\!1].term \neq L_{t}[i\!-\!1].term$ の場合

$i \lt length(l)+1$ の場合

\begin{align*}
AppendEntries(i, t, l)[i\!-\!1].term &= AppendEntries(i,t,l[1..(i\!-\!1)])[i\!-\!1].term\ (\because Lemma\ AppendEntries\ 1) \\
&= Lt[i\!-\!1].term\ (\because i = length(l)+1 \rm{の場合と同様の議論により})
\end{align*}

$\square$

leader の log に関する性質

leader の log に関する性質でここまでで定義したデータ型や述語では表現できていない性質があります。それは、leader は現在の term を持つ entry を自身の log に追記し、自身の log から以前の term の entry を修正、削除しないことです。
現在の term を $t$ とすると、leader の log $L_{t}$ に含まれる term $t' \lt t$ の entry は leader 自身が $L_{t}$ に書き込むことはありません。一方で、term $t'$ の leader が書き込んだとも限りません。
この Raft の性質を表現するために以下の論理式を公理として追加します。

この公理を用いて 6 つの補題を証明します。
Lemma leader 1 は leader の log が index $i$ に term $t$ の entry を持つなら、その entry は term $t$ の leader の index $i$ の entry と一致することを意味します。

$Lemma\ leader\ 1$
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, L_{t}[i] = L_{L_{t}[i].term}[i]
\end{equation} $Proof$
二項関係 $R \colon Term \to Term \to Prop$ を $R\,y\,x = y \lt x \land L_{t}[i].term \le y$ と定義する。また $P \colon Term \to Prop$ を $P\,x = L_{x}[i] = L_{L_{t}[i].term}[i]$ と定義する。
二項関係 $R$ が well founded relation であることを利用して well founded induction を用いて次を証明する。
\begin{equation}
\forall (x\colon Term),\, \left( \forall (y \colon Term),\, y \lt x \land L_{t}[i].term \le y \Rightarrow L_{y}[i] = L_{L_{t}[i].term}[i] \right) \Rightarrow L_{x}[i] = L_{L_{t}[i].term}[i]
\end{equation}
$x = L_{t}[i].term$ なら $L_{x}[i] = L_{L_{t}[i].term}[i]$ が成り立つので、 $x \neq L_{t}[i].term$ とする。すると公理より次が成り立つ。
\begin{equation}
\exists (l' \colon Log)(y \colon Term),\, L_{t}[i].term \le y \lt x \land AppendEntries(i, x, [ ]) = AppendEntries(i, y, l')
\end{equation}
Lemma AppendEntries 2, 3 より $AppendEntries(i, x, [])[i] = L_{x}[i]$ が成り立つ。よって
\begin{align*}
L_{x}[i] &= AppendEntries(i, x, [ ])[i] \\
&= AppendEntries(i, y, l')[i] \\
&= L_{y}[i] \ (\because Lemma\ AppendEntries\ 3) \\
&= L_{L_{t}[i].term}[i]\ (\because \rm{帰納法の仮定})
\end{align*}

$\square$

Lemma leader 2 は term を跨いだ AppendEntries 関数の一貫性に関する補題です。
任意の log $l$ に対して term $t$ で長さが $i$ の log を AppendEntries 関数で作成すると、その log は、ある log $l'$ が存在して、term $L_{t}[i]$ において AppendEntries 関数で作成した log と一致します。

$Lemma\ leader\ 2$
\begin{equation}
\forall (i\colon Index)(t \colon Term),\, \forall (l \colon Log),\ \exists (l' \colon Log),\, AppendEntries(i, t, l) = AppendEntries(i, L_{t}[i].term, l')
\end{equation} $Proof$
Lemma leader 1 と同様に二項関係 $R \colon Term \to Term \to Prop$ を $R\,y\,x = y \lt x \land L_{t}[i].term \le y$ と定義する。また $P \colon Term \to Prop$ を $P\,x = \forall (l\colon Log),\, \exists (l' \colon Log),\, AppendEntries(i, x, l) = AppendEntries(i, L_{t}[i].term, l')$ と定義する。
公理より
\begin{equation}
\exists (l' \colon Log)(y \colon Term),\, L_{t}[i].term \le y \lt x \land AppendEntries(i, x, l) = AppendEntries(i, y, l')
\end{equation}
帰納法の仮定より次が成り立つ。
\begin{equation}
\exists (l'' \colon Log),\, AppendEntries(i, y, l') = AppendEntries(i, L_{t}[i].term, l'')
\end{equation}
以上より
\begin{align*}
AppendEntries(i, x, l) &= AppendEntries(i, y, l') \\
&= AppendEntries(i, L_{t}[i].term, l'')
\end{align*}

$\square$

Lemma leader 3 は Lemma leader 1 と似ていますが index が $i\!-\!1$ になっています。
$t' = L_{t}[i].term$ なら、Lemma leader 1 より $L_{t}[i] = L_{t'}[i]$ が成り立ちますが $L_{t}[i\!-\!1$ ] と $L_{t'}[i\!-\!1]$ の関係については term の一致が証明できます。
$i\!-\!1$ の term が一致していることから、Lemma leader 1 を使えば entry が一致していることが言えますが Lemma leader 3 は Lemma leader 4 を証明するための準備なのでこれで十分です。

$Lemma\ leader\ 3$
\begin{equation}
\forall (i\colon Index)(t,t' \colon Term),\, i \gt 1 \Rightarrow t' = L_{t}[i].term \Rightarrow L_{t}[i\!-\!1].term = L_{t'}[i\!-\!1].term
\end{equation} $Proof$
\begin{align*}
L_{t}[i\!-\!1].term &= L_{t}[1..i][i\!-\!1].term \\
&= AppendEntries(i, t, [ ])[i\!-\!1].term \ (\because\ Lemma\ AppendEntries\ 2) \\
&= AppendEntries(i, t', l')[i\!-\!1].term \ (\because\ Lemma\ leader\ 2) \\
&= L_{t'}[i\!-\!1].term \ (\because Lemma\ AppendEntries\ 4) \\
\end{align*}

$\square$

$t' = L_{t}[i].term$ のとき、index $i$ の entry が $L_{t'}[i]$ と一致することは Lemma leader 1 で証明しました。
Lemma leader 4 は index $i$ の entry だけではなく index $1$ から $i$ までの全ての entry が一致することを意味します。

$Lemma\ leader\ 4$
\begin{equation}
\forall (i\colon Index)(t,t' \colon Term),\, t' = L_{t}[i].term \Rightarrow L_{t}[1..i] = L_{t'}[1..i]
\end{equation} $Proof$
$i$ に関する帰納法で示す。

$i = 1$ の場合

Lemma leader 1 より $L_{t}[1] = L_{t'}[1]$ が成り立つ。

$i = k$ の場合

Lemma leader 3 より $L_{t}[i\!-\!1].term = L_{t'}[i\!-\!1].term$ が成り立つ。 $L_{t}[i\!-\!1].term = t''$ とすると次が成り立つ。
\begin{align*}
L_{t}[1..(i\!-\!1)] &= L_{t''}[1..(i\!-\!1)]\ (\because \rm{帰納法の仮定}) \\
&= L_{t'}[1..(i\!-\!1)]
\end{align*}
よって、
\begin{align*}
L_{t}[1..i] &= L_{t}[1..(i\!-\!1)]::L_{t}[i] \\
&= L_{t'}[1..(i\!-\!1)]::L_{t}[i] \\
&= L_{t'}[1..(i\!-\!1)]::L_{t'}[i]\ (\because Lemma\ leader\ 1) \\
&= L_{t'}[1..i]
\end{align*}

$\square$

Lemma leader 5 は AppendEntries 関数は leader の log のコピー関数であることを意味します。

$Lemma\ leader\ 5$
\begin{equation}
\forall (t' \colon Term)(l \colon Log),\, RaftLog(t', l) \Rightarrow \forall (i \colon Index)(t \colon Term),\, AppendEntries(i, t, l) = L_{t}[1..i]
\end{equation} $Proof$
$RaftLog(t', l)$ に関する帰納法で示す。

$l = []$ の場合

Lemma AppendEntries 2 より $AppendEntries(i, t, []) = L_{t}[1..i]$ が成り立つ。

$l = AppendEntries(length(l), t', l')$ の場合

帰納法の仮定より $l = AppendEntries(length(l), t', l') = L_{t'}[1..length(l)]$ が成り立つ。
つまり、今証明すべきことは次の論理式である。
\begin{equation}
\forall (i \colon Index)(t \colon Term),\, AppendEntries(i, t, L_{t'}[1..length(l)]) = L_{t}[1..i]
\end{equation}
index $i$ に関する帰納法で示す。

$i = 0$ の場合

$AppendEntries(0, t, L_{t'}[1..length(l)]) = [] = L_{t}[1..0]$ が成り立つ。

$i = k$ の場合
$k \gt length(l)+1$ の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..length(l)]) &= AppendEntries(k\!-\!1, t, L_{t'}[1..length(l)])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k]\ (\because \text{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

$k = length(l)+1$ の場合
$L_{t'}[1..(k\!-\!1)][k\!-\!1].term = L_{t}[k\!-\!1].term$ の場合

$L_{t'}[1..(k\!-\!1)][k\!-\!1].term = L_{t}[k\!-\!1].term = t'''$ とすると Lemma leader 4 より次が成り立つ。
\begin{align*}
L_{t'}[1..(k\!-\!1)] &= L_{t'''}[1..(k\!-\!1)] \\
&= L_{t}[1..(k\!-\!1)]
\end{align*}
よって
\begin{align*}
AppendEntries(k, t, L_{t'}[1..(k\!-\!1)]) &= L_{t'}[1..(k\!-\!1)]::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k] \\
&= L_{t}[1..k]
\end{align*}

$L_{t'}[1..(k\!-\!1)][k\!-\!1].term \neq L_{t}[k\!-\!1$ .term] の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..(k\!-\!1)]) &= AppendEntries(k\!-\!1, t, L_{t'}[1..(k\!-\!1)])::L_{t}[k] \\
&= L_{t}[1..(k\!-\!1)]::L_{t}[k]\ (\because \text{帰納法の仮定}) \\
&= L_{t}[1..k]
\end{align*}

$k \lt length(l)+1$ の場合

\begin{align*}
AppendEntries(k, t, L_{t'}[1..length(l)]) &= AppendEntries(k, t, L_{t'}[1..(length(l)\!-\!1)]) \\
&= AppendEntries(k, t, L_{t'}[1..(k\!-\!1)])\ (\because Lemma\ AppendEntries\ 1) \\
&= L_{t}[1..k]\ (\because k = length(l)+1 \rm{の場合と同様}\ Lemma\ RaftLog\ 1) \\
\end{align*}

$\square$

Lemma leader 6 は Log Matching Property を証明するための最後の補題です。
log $l$ が RaftLog で $t = l[i].term$ なら $l$ の部分 log $l[1..i]$ は $L_{t}[1..i]$ と一致することを意味します。

$Lemma\ leader\ 6$
\begin{equation}
\forall (i \colon Index)(t, t' \colon Term)(l \colon Log),\, RaftLog(t', l) \Rightarrow t = l[i].term \Rightarrow l[1..i] = L_{t}[1..i]
\end{equation} $Proof$
RaftLog に関する帰納法で示す。

$l = []$ の場合

$[]$ に対する term が定義されないので trivial に成り立つものとする。

$l = AppendEntries(length(l), t', l')$ の場合

Lemma leader 5 より次が成り立つ。
\begin{align*}
l[1..i] &= AppendEntries(length(l), t', l')[1..i] \\
&= L_{t'}[1..length(l)][1..i] \ (\because Lemma\ leader\ 5) \\
&= L_{t'}[1..i]
\end{align*}
$t = l[i].term = L_{t'}[i].term$ が成り立つから、Lemma leader 4 より $l[1..i] = L_{t'}[1..i] = L_{t}[1..i]$ が成り立つ。

$\square$

Log Matching Property の証明

以上の準備を元に Log Matching Property を証明します。

$Theorem\ Log\ Matching\ Property$
\begin{equation}
\forall (l_{1}, l_{2}\colon Log)(t_{1},t_{2}\colon Term)(i: Index),\, RaftLog(t_{1}, l_{1}) \Rightarrow RaftLog(t_{2}, l_{2}) \Rightarrow l_{1}[i].term = l_{2}[i].term \Rightarrow l_{1}[1..i] = l_{2}[1..i]
\end{equation} $Proof$
$l_{1}[i].term = l_{2}[i].term = t$ とすると Lemma leader 6 より $l_{1}[1..i] = L_{t}[1..i] = l_{2}[1..i]$ が成り立つ。