domino-lang/domino

# Domino `Domino` 是一款工具，旨在帮助您管理在使用 State-Separation Proofs 框架进行密码学证明时那些繁琐的工作。 ## 功能 - 使用一种接近伪代码的自定义语言来处理 package、game 和证明 - 对 oracle 代码以及 package 之间的连线进行类型检查 - 检查 reduction game hop 是否有效 - 使用 SMT 求解器来证明具有不同代码的 game 之间的等价性 - 这需要用 SMT-LIB 手动编写 invariant，但不需要去证明它们。 - 生成 LaTeX cryptocode 和图表 ## 安装说明 要求： - 较新版本的 Rust toolchain。如果您还没有，请了解 [rustup]。 - 已安装 CVC5并将其添加到 `PATH` 中（构建 domino 不需要，但运行时需要） 使用 `cargo install --git https://github.com/domino-lang/domino domino` 安装该工具。 确保已安装的二进制文件位于您的 `PATH` 中。（默认情况下，Cargo 会安装到（`~/.cargo/bin`）。） ## 使用说明 进入项目目录并运行 `domino prove`。 要了解项目的结构，请查看 `example-projects/hello-world` 目录（抱歉，正式的文档已在 Roadmap 中）。 要为项目生成 LaTeX，请使用 `domino latex`。输出将位于相对于项目根目录的 `_build/latex` 中。 ## 模型 在最底层是 _package_，它们可以暴露 oracle（export）并调用其他 package 上的 oracle（import）。一个 package 同时拥有 _state_ 和 _constant parameter_。在上一层是 _game_，它将 package 实例化为 package instance，并为每个 import 分配要调用的 oracle。game 也具有可以在实例化期间分配给 package constant parameter 的 constant parameter。在最顶层是证明，它会实例化 game 并描述它们之间的 hop。包含 reduction game hop（基于假设的图论论证）和 equivalence game hop（我们使用 SMT 求解器来证明两个 game 的行为完全一致）。 ## 可靠性缺口 目前，该工具负责处理等价性证明中最困难的部分，但迄今为止，仍有两个属性需要手动检查： - **Invariant 归纳基础情况**：根据 invariant 的等价关系，左右基础状态是等价的。 - **随机映射的满射性**：随机映射描述了左右 game 中哪些随机值应当是等价的。为了确保随机值不会（例如）被全部约束为同一个值，需要进行此项检查。 ## Roadmap - [ ] 修复剩余的可靠性缺口 - [ ] 改进文档 - [ ] 改进错误报告 - [ ] Editor/LSP 支持 - [ ] 弥合可靠性缺口 - [ ] 自动确定优势项 - [ ] 类型参数 - 在实例化中，不仅允许分配常量，还允许分配类型。 - [ ] 自动为等价性证明寻找 invariant。

标签：Rust, 可视化界面, 定理证明, 密码学, 形式化验证, 手动系统调用, 编译工具, 网络流量审计, 通知系统