Hax

Hax 是一个用于高保证翻译的工具，可以将 Rust 的一个大型子集翻译成形式语言，如 F* 或 Coq。这扩展了 hacspec 项目的范围，该项目之前是一个嵌入 Rust 的领域特定语言（DSL），成为一个可以用于验证 Rust 程序的可使用工具。

那么现在的 hacspec 是什么？

hacspec 是可以与 hacspec 标准库一起使用，以编写简洁、可执行和可验证的 Rust 规范的 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 into --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 devshell 时自动可用作为命令 rebuild）

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

出版物及其他材料

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

次要文献，使用 hacspec

• 📕 最后的抵抗

贡献

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