Hax

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

那么现在的 hacspec 是什么呢？

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

用法

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

• into (cargo hax into BACKEND)：将 Rust 包翻译成后端 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）

只需将代码克隆到仓库中，然后运行 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 上开始 讨论，或提交一个 问题 来讨论您的贡献。