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 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.