Hax

hax 是一个用于高保证翻译的工具，可以将 Rust 的大多数子集翻译成形式语言，如 F* 或 Coq。这扩展了 hacspec 项目的范围，hacspec 之前是一个嵌入 Rust 的 DSL，现在是一个可用于验证 Rust 程序的工具。

那么现在的 hacspec 是什么呢？

hacspec 是 Rust 的函数子集，可以与 hacspec 标准库一起使用，以简洁、可执行和可验证的方式在 Rust 中编写规范。这些规范可以用 hax 翻译成形式语言。

使用方法

Hax 是一个 cargo 子命令。命令 cargo hax 接受以下子命令

• into (cargo hax into BACKEND)：将 Rust 包翻译成后端 BACKEND（例如 fstar，coq）。
• json (cargo hax json)：将你的包的带类型抽象语法树（AST）提取为 JSON 文件。

注意

• BACKEND 可以是 fstar、coq 或 easycrypt。支持的 backend 列表可以通过运行 cargo hax --help 来显示。
• 子命令 cargo hax 接受选项，使用 cargo hax --help 来列出它们。
• 子命令 cargo hax into 也接受选项，使用 cargo hax into --help 来列出它们。

安装

示例

有一组示例展示了 hax 可以为您做什么。请查看 示例目录

在 Hax 上进行黑客攻击

编辑源代码（Nix）

只需克隆并 cd 到仓库中，然后运行 nix develop .。您还可以使用 direnv，配合 编辑器集成。

此存储库的结构

• rust-frontend/：Rust 库，它通过挂钩 rust 编译器并提取其内部类型化抽象语法树 THIR 作为 JSON。
• engine/：简化并精化引擎，将程序从 Rust 语言转换为各种后端（请参阅 engine/backends/）。
• cli/：Cargo 的 hax 子命令。

重新编译

您可以使用 .utils/rebuild.sh 脚本（在 Nix 开发外壳中使用时，作为 rebuild 命令自动提供）

• rebuild：重新构建 Rust 然后是 OCaml 部分；
• rebuild TARGET：重新构建 TARGET 部分（《TARGET》是 rust 或 ocaml）。

出版物和其他材料

• 📕 技术报告
• 📕 HACSpec：通往高保证密码学的大门
• 📕 原始 hacspec 论文

使用 hacspec 的次级文献

• 📕 最后的障碍

贡献

在开始任何工作之前，请加入 Zulip 聊天，在 Github 上开始 讨论，或提交 问题 来讨论您的贡献。