新项目为裸机Rust提供离线形式化验证模板
来源标题：Show HN: Arcstone-Airlock-Blueprint – Offline Charon/Aeneas/Coq for Rust
Arcstone-Airlock-Blueprint发布，为#![no_std] Rust裸机系统提供开箱即用的解耦精化验证模板。目标crate无需修改源码或引入验证宏，验证流程在离线非root容器中通过Charon、Aeneas和Coq 8.18.0下游执行，实现Rust实现与Coq规格的等价性证明。审计输出REFINEMENT-AUDIT.json，经coqchk递归校验，admitted_axioms为0。
以下正文由 AI 翻译自 Hacker News 最新（原文版权归原站所有），可能存在偏差，重要内容请以原文为准。
面向裸机 #![no_std] Rust 系统的开箱即用解耦精化隔离舱模板
零上游验证侵入（C_ops = 0）：目标 #![no_std] Rust crate（crates/example-no-std-gate）不包含任何验证宏、幽灵变量、证明依赖，也没有任何源码修改。
下游生成代码精化（Rust_Impl ⊑ Coq_Spec）：Charon LLBC 提取（仅 --lib）、Aeneas 函数式合成以及 Coq 8.18.0 证明在下游针对只读快照运行，直接针对 Aeneas 合成的 Coq 模块证明等价性。
零未经批准的 axiom 蔓延（admitted_axioms: 0, unexpected_assumptions: 0）：验证在离线、非 root、能力已剥离的容器中运行（--network none --cap-drop ALL --read-only --user 65532:65532），并输出 REFINEMENT-AUDIT.json，该文件经由递归 coqchk -o、独立 Audit.v（Print Assumptions）对显式允许列表进行校验——允许列表包含固定版本的 Aeneas Primitives.v 指针宽度常量（ASSUMPTIONS.allow）、黄金定理语句固定以及沙箱内语义金丝雀变异体。
仅上游 DOI 拓扑：永久归档 DOI 严格保留在上游规范上（10.5281/zenodo.22665852、10.5281/zenodo.24041851、10.5281/zenodo.24093739）。本模板从不在下游铸造 DOI。
30 分钟快速上手（使用预构建的摘要固定 OCI 镜像）
前置条件 Rust 稳定工具链（1.82.0 + thumbv7em-none-eabihf 目标） Docker / OCI 运行时（支持 --network none 的 docker） Python 3.11+、git、sha256sum
第 1 步：运行快速上游内循环（< 15 秒） make quick make lint 该命令运行 cargo fmt --check、cargo clippy -- -D warnings、cargo test --locked、交叉编译到 thumbv7em-none-eabihf，并验证没有证明工具链泄漏到 crates/ 中。 python3 -m unittest discover -s airlock/tests -p 'test_*.py' -v
第 3 步：运行封闭式下游隔离舱（--network none） make airlock 该命令校验 PINS.lock，若本地未缓存则拉取摘要固定的验证器 OCI 镜像，并在 /work tmpfs 内执行完整的离线流水线：
正文由 探How 从来源站点 RSS 同步，内容未经改写；遇到排版缺失或需要图片、视频时请以原文为准。