上交所技术公司 朱立
毋庸置疑，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先生解释了其语义，发现双方最后想要在这一段表述的内容是完全一样的，只是原文表述理解起来不太容易]
底下是一个备忘，供了解basic hotstuff之下如何形成拓扑上的分叉（不是链的分叉）的：
重要笔记：event driven 算法和chained hotstuff 有些不同，首先是three-chain被放宽到最后一个指针可以不是直接parent，其次是pace maker里面不搜集齐备n-f的NEW VIEW也可以向下走（这个不影响 safety，从证明可以看出；然后就是node带有height字段，且和parent节点高度一定差1，在这里是没chained hotstuff那种插空块的玩法的。QChigh和bleaf的关系没有表面看的那么简单，考虑一下leader急速调用onBeat会如何就可以想到了——leaf的parent会和leaf.justify.node不一样。
至于chained hotstuff，空块可以用某些手法压缩，不一定真的要落盘那么多空块。
event driven的两个入口及大体的消息传递模式如下图。GENERIC消息的发出不一定如图上那样等前面的VOTE都回来才发出。
