作者: Long Meng、Benedikt Wagner、George Kadianakis、Francesco Risitano 感谢 Tom Wambsgans、Thomas Coratger、Arantxa Zapico 以及其他...
PQ-DAS 的形式化验证安全性 感谢 Alex Hicks 提供反馈和讨论。 本文及详细的安全性证明大纲由人类作者撰写,向 Lean 的翻译工作在 AI 的大力帮助下完成。 **免责声明。**这里的 lean 代码证明的是关于抽象方...