UTxO账本及其上实现程序的性质

基于轨迹的属性是程序行为分析的黄金标准。这种类型分析的应用领域之一是加密货币账本，既用于分析账本本身的行为，也用于分析由账本调用的任何用户定义的程序，即智能合约。（扩展）UTxO账本模型是一种账本模型，其中所有智能合约代码都是无状态的，若要建模有状态的程序则需额外工作。我们正式化了将基于轨迹的分析应用于UTxO账本和合约的做法，表述为拓扑学、图论以及范畴论的语言。为描述UTxO账本执行的有效轨迹及其与在账本上实现的有状态程序行为的关系，我们定义了一个简单图的范畴，其中形成无限路径的路径构成超度量空间。在该范畴中，映射是简单图的任意部分滤镜定义的同态。实现于账本上的程序对应于该图的有效UTxO执行轨迹之上的非扩张映射。我们在该框架中论证安全属性，并证明了有效UTxO账本轨迹的性质。