对Basic HotStuff 证明的完善

上交所技术公司  朱立

毋庸置疑，HotStuff 是个非常棒的BFT算法，近期抢了不少眼球。本文考察了其论文中对Basic HotStuff 的证明过程，列出几处值得商榷之处，并给出了对证明的完善。经过完善，更好地证明了算法的正确性（包括Safety 和 Liveness）。

[插播一句：由圈内人士帮忙撮合，笔者很荣幸地联系到了算法作者 Ted Yin先生，有机会就本文内容和算法作者进行了交流并得到了他的认同。在交流过程中笔者也受益匪浅，在此表示感谢！]

本文针对的HotStuff 论文有二，其一是作者主页上的PODC2019论文, 其一是arxiv上的V5版本。两篇论文在Basic HotStuff部分的文字是一样的，所以下文仅举arxiv版本为例。

---

第一处瑕疵，在下图中高亮显示：

由于现在并不能确定视图v1和vs到底相隔多远，所以很可能中间间隔了多个视图，而且replica r 纵然在视图 v1中把lockedQC设置为基于w的precommitQC,  在视图v1+1中也有机会正常走完整个流程，从而安全地把lockedQC更新为某个基于w*的precommitQC, 且w*以w为其祖先，vs的minimality并不能阻止这种事情发生, 所以 r 在视图vs之前其实can have seen some other prepareQC with lower view， 这样一来证明文字就不够完美了。

[Ted Yin先生表示：原文的文字容易引起歧义，准确的表述是锁定的分支不会更换而非原来保存的lockedQC不会更换；笔者完全赞同这里的要点是说明锁定的分支不会再切换，下文自拟的证明也正是遵循了这个道理]

第二处瑕疵，如下图高亮所示：

很容易构造一个正常运作的场景，在进入GST之前所有的correct replica拥有完全一样的preparedQC和lockedQC，只不过前一轮的leader恰好崩溃了从而没法形成commitQC。进入GST后, highQC.viewNumber > lockedQC.viewNumber并不成立，这时 line 27 of Algorithm 1  can not be satisfied，所以这里的讨论并未穷尽一切可能，而是留下了一些死角。

[这一段没什么争议]

另有一处遗憾是：虽然原始论文中“Livelessness with two-phases”一节通过举出一个特定的二阶段版本证明不存在具备Optimistic Responsiveness且同时满足Safety和Liveness的二阶段版本，但单举出一个例子说不行，并不等于就真的证明了“任何情况下都不行”，逻辑上讲不太完美。

[此处Ted Yin先生解释说要构建一个证明impossibility的完整证明需要单独的一篇文章。这个非常可以理解，因此笔者也认同这里不是错误，只是一个遗憾]

---

下面笔者给的证明修正了前两个问题。为令证明易于理解，对Lemma 3 也进行了调整。

[对于Lemma 3原来的表述Ted Yin先生解释了其语义，发现双方最后想要在这一段表述的内容是完全一样的，只是原文表述理解起来不太容易]