tarts:时序抗攻击类型系统

挞 这是一个旨在构建可证明不受时间攻击影响的系统的项目。 这是通过使用依赖类型和 Curry-Howard 同构让程序本身作为其时间恒定性的证明来实现的。 目前唯一编写的函数是相等，证明只是执行相同数量的基本布尔逻辑运算，但这个概念可以扩展到任何可以表示为原始布尔逻辑运算序列的函数。 笔记： 现在一切都相当糟糕，因为这仍然是非常早期的 pre-alpha 在 THOTCON 2015 上接受展示！