Authenticated Append-Only Skiplists (AAOSLs) enable maintenance and querying of an authenticated log (such as a blockchain) without requiring any single party to store or verify the entire log, or to trust another party regarding its contents. AAOSLs can help to enable efficient dynamic participation (e.g., in consensus) and reduce storage overhead. In this paper, we formalize an AAOSL originally described by Maniatis and Baker, and prove its key correctness properties. Our model and proofs are machine checked in Agda. Our proofs apply to a generalization of the original construction and provide confidence that instances of this generalization can be used in practice. Our formalization effort has also yielded some simplifications and optimizations.

翻译：经认证的仅存附加列表(AAOSLs)能够维持和查询经认证的日志(如块链),而无需任何单一方储存或核查整个日志,或信任另一方对日志内容的信任。 AAOSLs可以帮助高效率的动态参与(如达成共识)和减少存储管理管理。在本文中,我们正式确定一个原由Maniatis和Baker描述的AAOSL, 并证明它的关键正确性能。我们的模型和证据是在Agda进行机器检查的。我们的证据适用于原始构造的概括化,并提供可以实际使用这种概括性实例的信心。我们的正规化工作也产生了一些简化和优化。