前瞻自由作为时间非干扰：回测和智能体交易流程的可验证正确性属性

前瞻偏差（使用决策时期之后的信息来做出该时期的决策）是回测或机器学习评估夸大一个在部署时会令人失望的系统的主要方式。该领域使用特定于构造的配方和经验检测器来管理它，这些方法仅在各自渠道内是可靠的，并且其沉默不能证明任何东西。我们表明，前瞻自由实际上是一个形式化属性：固定一个时期，要求未来不影响现在是对时间索引信息格的时间非干扰。从这一识别出发，我们开发了一个流程演算，将数据项的可用性与其参考时间分开，并界定了问题的边界。在可用性可能依赖于数据值的地方，前瞻自由是不可判定的（实际上是Pi-0-1-hard）：泄漏是递归可枚举的，但自由不是。在值无关片段上（涵盖窗口化、重采样、连接、时点和历史读取以及智能体检索），我们给出了一个类型和效应系统，它是健全的，并且在线性时间内可判定。一个工件证实了该理论：检查线性扩展，一个独立的预言机证明在接受的流程中没有泄漏，并且检查器捕获了差分和分块检测器遗漏的每一个植入泄漏。