leanprover/LNSym

# LNSym：Lean 中的原生代码符号模拟器 [](https://github.com/leanprover/LNSym/actions/workflows/makefile.yml) LNSym 是一个针对 Armv8 机器码程序的符号模拟器。 有关 LNSym 的许可，请参阅 [LICENSE](./LICENSE) 文件，外部贡献 指南请参阅 [CONTRIBUTING.md](./CONTRIBUTING.md)。 ## 前置条件 按照[这些说明](https://leanprover-community.github.io/get_started.html) 在您的机器上安装 Lean4 以及您首选编辑器的插件。 ## 构建说明 在 LNSym 的顶级目录下运行 `make` 以获取 Lean4 依赖， 构建此库（包括证明），并运行一致性 测试。请注意，如果您使用的不是 Aarch64 架构的机器，一致性 测试将被跳过。 默认的 `make` 命令对应于以下调用： ```make all VERBOSE=--verbose NUM_TESTS=20``` ### 其他 Makefile 目标 `clean`：移除构建输出。 `clean_all`：包含 `clean`，并移除 Lean 依赖以及 所有基准测试和分析数据。 `specs`：[在 `all` 下运行] 仅构建 感兴趣的原生代码程序的规范。 `proofs`：[在 `all` 下运行] 仅构建证明。 `tests`：[在 `all` 下运行] 构建具体测试。 `cosim`：[在 `all` 下运行] 执行一致性测试。 `awslc_elf`：执行 AWS-LC 的 ELF 加载测试。 `benchmarks`：运行符号模拟器的基准测试。 `profiler`：启用分析器的情况下，对每个基准测试运行一轮 ### 可在命令行中传入的 Makefile 变量 `VERBOSE`：详细模式；打印正在测试的指令的反汇编代码。 默认：开启。 `NUM_TESTS`：每个指令类的随机测试数量。默认：20。 ## 目录概览 - `Arm`：Armv8 Aarch64 ISA 的形式化 - `Specs`：感兴趣算法的规范 - `Proofs`：Arm 原生代码程序的证明 - `Tests`：Arm 原生代码程序的具体测试

标签：Armv8, Lean4, 定理证明, 形式化验证, 机器码模拟器, 符号执行