分布式系统，不变式，可信偏序
一个分布式系统可以被表示为一个事件驱动的状态机。
这里是在说整个系统，不是节点协议。
系统处于任何一个状态时，都有对应的一组此状态下的合法事件，以及对于每个事件的状态转移。
这些事件和状态转移为系统的所有合法状态建立起一种偏序关系。
一个分布式系统，从最笼统的角度看待，就是在全部的合法状态下都能保证某些不变式始终成立。
系统状态可以沿着这个偏序关系图中的箭头以任意的方式跳来跳去，先递送（deliver）这个消息或者那个，在递送之间隔着任意的时间跨度而触发超时，但是无论如何
- 前提：只要系统状态还在这个图的范围内跳来跳去
- 命题：分布式系统的实现就会保证某些不变式依然成立
因此一个看待分布式系统的高维视角可以是它消除了系统中的不确定性，将不确定的分布式系统底层细节对上层隐藏了起来，不管实际发生的轨迹（trace）如何都能「粉饰太平」。这与此处主题无关不多展开。
我们有成熟的工具来验证「命题」部分的成立（即模型检查或形式化验证）。而「前提」的定义却通常依赖于直觉上的假设，而且在不同的场合还时常有细节上的变化。
但是，大体上我们可以认为「前提」，也即分布式系统中每个系统状态下可能发生的事件和状态转移，遵循节点本地物理时间流逝和节点间收发消息的先后关系，即Lamport因果。
假设我们有一种可信偏序设施，可以用来建立起符合Lamport因果的偏序关系，那么它就像一个「虚拟机」，可以支持分布式应用运行在一个标准化的「虚拟世界」中，确保其状态只在合法状态之间转移，保证了「前提」，从而确保「命题」的成立。
这带来了系统状态与物理硬件之间的灵活映射。系统状态中的每个节点状态不用分要对应到一个物理节点上。
实际上，所有的物理节点变得同构且与应用逻辑解耦了。每个物理节点所做的是站在整个系统的角度，试图在转移状态图中前进。
挑战：怎么把拜占庭给框（frame）进这个叙事。
Cover目前所面临的最大难题是偏序关系缺乏市场。
这里描述的是一个为其寻找市场的思路：将视角朝下移动，聚焦每个分布式系统生来就带有的偏序关系。
A less abstract story也许会更好，但是还得想想。