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 crate 翻译成 BACKEND 后端（例如 fstar，coq）。
• json (cargo hax json)：将 crate 的类型化 AST 提取为 JSON 文件。

注意

• BACKEND可以是fstar、coq或easycrypt。支持的后端列表可以通过运行以下命令显示：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 是 rust 或 ocaml）。

出版物及其他材料

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

次要文献，使用 hacspec

• 📕 最后的冲刺

贡献

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