Hax

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

那么现在的 hacspec 是什么呢？

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

使用方法

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

• into (cargo hax into BACKEND)：将 Rust crate 翻译为后端 BACKEND（例如 fstar，coq）。
• json (cargo hax json)：将您的 crate 的类型化 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 开发壳时，它作为 rebuild 命令自动可用）

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

出版物及其他材料

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

关于使用 hacspec 的次级文献

• 📕 最后的稻草

贡献

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