From 7abf53d03bc58399520bfaa7ce882a796409f2f3 Mon Sep 17 00:00:00 2001 From: Joshua Liebow-Feeser Date: Thu, 1 Oct 2026 18:43:13 -0400 Subject: [PATCH] Add inline Aeneas verification, checked in CI --- .github/workflows/ci.yml | 38 +- tools/Cargo.lock | 25 ++ tools/Cargo.toml | 1 + tools/aeneas-inline/Cargo.toml | 20 + tools/aeneas-inline/src/main.rs | 128 +++++++ verification/aeneas/README.md | 281 ++++++++++++++ verification/aeneas/golden.py | 166 +++++++++ verification/aeneas/golden/util.max.lean.in | 9 + verification/aeneas/golden/util.min.lean.in | 9 + .../golden/util.padding_needed_for.lean.in | 9 + ...down_to_next_multiple_of_alignment.lean.in | 9 + verification/aeneas/inline.py | 350 ++++++++++++++++++ verification/aeneas/inventory.json | 38 ++ verification/aeneas/lean/Check.lean | 27 ++ verification/aeneas/lean/Obligations.lean | 36 ++ verification/aeneas/lean/Proofs.lean.in | 19 + verification/aeneas/lean/Zerocopy.lean | 10 + .../aeneas/lean/Zerocopy/FunsExternal.lean | 24 ++ .../aeneas/lean/Zerocopy/TypesExternal.lean | 20 + verification/aeneas/negative-controls.sh | 117 ++++++ verification/aeneas/prepare.py | 121 ++++++ verification/aeneas/run.sh | 94 +++++ verification/aeneas/scaffolding/Funs.lean | 84 +++++ .../scaffolding/FunsExternal_Template.lean | 52 +++ verification/aeneas/scaffolding/Types.lean | 42 +++ .../scaffolding/TypesExternal_Template.lean | 42 +++ verification/aeneas/setup.sh | 66 ++++ verification/aeneas/tests/test_golden.py | 90 +++++ verification/aeneas/tests/test_inline.py | 211 +++++++++++ verification/aeneas/tests/test_prepare.py | 62 ++++ verification/aeneas/toolchain.sh | 32 ++ zerocopy/src/util/mod.rs | 125 +++++++ 32 files changed, 2356 insertions(+), 1 deletion(-) create mode 100644 tools/aeneas-inline/Cargo.toml create mode 100644 tools/aeneas-inline/src/main.rs create mode 100644 verification/aeneas/README.md create mode 100644 verification/aeneas/golden.py create mode 100644 verification/aeneas/golden/util.max.lean.in create mode 100644 verification/aeneas/golden/util.min.lean.in create mode 100644 verification/aeneas/golden/util.padding_needed_for.lean.in create mode 100644 verification/aeneas/golden/util.round_down_to_next_multiple_of_alignment.lean.in create mode 100644 verification/aeneas/inline.py create mode 100644 verification/aeneas/inventory.json create mode 100644 verification/aeneas/lean/Check.lean create mode 100644 verification/aeneas/lean/Obligations.lean create mode 100644 verification/aeneas/lean/Proofs.lean.in create mode 100644 verification/aeneas/lean/Zerocopy.lean create mode 100644 verification/aeneas/lean/Zerocopy/FunsExternal.lean create mode 100644 verification/aeneas/lean/Zerocopy/TypesExternal.lean create mode 100755 verification/aeneas/negative-controls.sh create mode 100644 verification/aeneas/prepare.py create mode 100755 verification/aeneas/run.sh create mode 100644 verification/aeneas/scaffolding/Funs.lean create mode 100644 verification/aeneas/scaffolding/FunsExternal_Template.lean create mode 100644 verification/aeneas/scaffolding/Types.lean create mode 100644 verification/aeneas/scaffolding/TypesExternal_Template.lean create mode 100755 verification/aeneas/setup.sh create mode 100644 verification/aeneas/tests/test_golden.py create mode 100644 verification/aeneas/tests/test_inline.py create mode 100644 verification/aeneas/tests/test_prepare.py create mode 100644 verification/aeneas/toolchain.sh diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ed995dd69b..a88395cedc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1043,6 +1043,42 @@ jobs: name: ${{ env.ZC_CI_IMAGE_ARCHIVE }} path: ${{ runner.temp }}/${{ env.ZC_CI_IMAGE_ARCHIVE }} + aeneas: + name: Aeneas translation and Lean proofs + runs-on: ubuntu-24.04 + timeout-minutes: 30 + env: + # Charon uses its own pinned Rust compiler. Keep the ordinary Rust CI + # flags (including randomized layouts) out of this extraction. + RUSTFLAGS: "" + RUSTDOCFLAGS: "" + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Install rustup + uses: dtolnay/rust-toolchain@02cb101ec7c40f2c49e1d9714d64511d8e1b74de # zizmor: ignore[superfluous-actions] + with: + toolchain: stable + + - name: Install the pinned Aeneas, Charon, Rust, and Lean bundle + run: bash verification/aeneas/setup.sh + + - name: Test Rust syntax ownership, discovery, and golden comparison + run: | + source verification/aeneas/toolchain.sh + export CARGO_TARGET_DIR="$PWD/target/aeneas/annotation-tool" + cargo +"$AENEAS_RUST_TOOLCHAIN" test --locked --manifest-path tools/Cargo.toml -p aeneas-inline + cargo +"$AENEAS_RUST_TOOLCHAIN" build --locked --manifest-path tools/Cargo.toml -p aeneas-inline + python3 -B -m unittest discover -s verification/aeneas/tests + + - name: Compare live extraction with goldens and prove both models + run: bash verification/aeneas/run.sh + + - name: Verify that admissions and incorrect code fail + run: bash verification/aeneas/negative-controls.sh + # Used to signal to branch protections that all other jobs have succeeded. all-jobs-succeed: # WARNING: This name is load-bearing! It's how GitHub's settings UI configures which jobs @@ -1053,7 +1089,7 @@ jobs: # success in branch protection, so this aggregation must fail closed. if: ${{ always() }} runs-on: ubuntu-latest - needs: [build_test, miri, codegen, coverage, kani, check_be_aarch64, check_avr_atmega, check_fmt, check_actions, check_readme, check_versions, check_msrv_is_minimal, check_stale_stderr, check-all-toolchains-tested, check-job-dependencies, check-todo, run-git-hooks, zizmor, build_docker_env] + needs: [aeneas, build_test, miri, codegen, coverage, kani, check_be_aarch64, check_avr_atmega, check_fmt, check_actions, check_readme, check_versions, check_msrv_is_minimal, check_stale_stderr, check-all-toolchains-tested, check-job-dependencies, check-todo, run-git-hooks, zizmor, build_docker_env] steps: - name: Reject workflow cancellation if: ${{ cancelled() }} diff --git a/tools/Cargo.lock b/tools/Cargo.lock index dcf1c43a89..459e8b6ecb 100644 --- a/tools/Cargo.lock +++ b/tools/Cargo.lock @@ -17,6 +17,16 @@ version = "2.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "320119579fcad9c21884f5c4861d16174d0e06250625266f50fe6898340abefa" +[[package]] +name = "aeneas-inline" +version = "0.0.0" +dependencies = [ + "proc-macro2", + "rustc_lexer", + "serde_json", + "syn", +] + [[package]] name = "aho-corasick" version = "1.1.4" @@ -432,6 +442,15 @@ version = "0.1.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d" +[[package]] +name = "rustc_lexer" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c86aae0c77166108c01305ee1a36a1e77289d7dc6ca0a3cd91ff4992de2d16a5" +dependencies = [ + "unicode-xid", +] + [[package]] name = "rustc_version" version = "0.4.1" @@ -729,6 +748,12 @@ version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254" +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" + [[package]] name = "unit-prefix" version = "0.5.2" diff --git a/tools/Cargo.toml b/tools/Cargo.toml index f7a1919ab9..59cdf9da94 100644 --- a/tools/Cargo.toml +++ b/tools/Cargo.toml @@ -8,6 +8,7 @@ [workspace] members = [ + "aeneas-inline", "cargo-zerocopy", "generate-readme", "ui-runner", diff --git a/tools/aeneas-inline/Cargo.toml b/tools/aeneas-inline/Cargo.toml new file mode 100644 index 0000000000..0af4a50c31 --- /dev/null +++ b/tools/aeneas-inline/Cargo.toml @@ -0,0 +1,20 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +[package] +name = "aeneas-inline" +edition.workspace = true +version.workspace = true +license.workspace = true +publish.workspace = true + +[dependencies] +proc-macro2 = { version = "1", features = ["span-locations"] } +rustc_lexer = "=0.1.0" +serde_json = "1" +syn = { version = "2", features = ["full", "visit"] } diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs new file mode 100644 index 0000000000..be464e732d --- /dev/null +++ b/tools/aeneas-inline/src/main.rs @@ -0,0 +1,128 @@ +// Copyright 2026 The Fuchsia Authors +// +// Licensed under a BSD-style license , Apache License, Version 2.0 +// , or the MIT +// license , at your option. +// This file may not be copied, modified, or distributed except according to +// those terms. + +//! Preserve Rust comments and associate annotations with parsed function braces. + +use std::{fs, io}; + +use proc_macro2::LineColumn; +use serde_json::{json, Value}; +use syn::visit::{self, Visit}; + +struct Functions<'a> { + source: &'a str, + modules: Vec, + unsupported: usize, + functions: Vec, +} + +impl Functions<'_> { + fn offset(&self, pos: LineColumn) -> usize { + let start = + self.source.split_inclusive('\n').take(pos.line - 1).map(str::len).sum::(); + start + + self.source[start..] + .char_indices() + .nth(pos.column) + .map_or(self.source[start..].len(), |(byte, _)| byte) + } +} + +impl<'ast> Visit<'ast> for Functions<'_> { + fn visit_item_mod(&mut self, item: &'ast syn::ItemMod) { + self.modules.push(item.ident.to_string()); + visit::visit_item_mod(self, item); + self.modules.pop(); + } + + fn visit_item_fn(&mut self, item: &'ast syn::ItemFn) { + let open = self.offset(item.block.brace_token.span.open().start()); + assert_eq!(&self.source[open..open + 1], "{", "Invalid function brace span"); + let mut path = self.modules.clone(); + path.push(item.sig.ident.to_string()); + self.functions.push(json!({ + "path": path.join("::"), "open": open, + "close": self.offset(item.block.brace_token.span.close().end()), + "supported": self.unsupported == 0, + })); + // Nested functions, impls, traits and macros need an explicit extension + // to identity resolution; never silently attribute them to a free fn. + self.unsupported += 1; + visit::visit_item_fn(self, item); + self.unsupported -= 1; + } + + fn visit_item_impl(&mut self, item: &'ast syn::ItemImpl) { + self.unsupported += 1; + visit::visit_item_impl(self, item); + self.unsupported -= 1; + } + + fn visit_item_trait(&mut self, item: &'ast syn::ItemTrait) { + self.unsupported += 1; + visit::visit_item_trait(self, item); + self.unsupported -= 1; + } +} + +fn inspect(source: &str) -> Result { + let mut offset = 0; + let mut comments = Vec::new(); + for token in rustc_lexer::tokenize(source) { + match token.kind { + rustc_lexer::TokenKind::LineComment | rustc_lexer::TokenKind::BlockComment { .. } => { + comments.push(json!({"start": offset, "end": offset + token.len})); + } + _ => {} + } + offset += token.len; + } + let syntax = syn::parse_file(source)?; + let mut visitor = + Functions { source, modules: Vec::new(), unsupported: 0, functions: Vec::new() }; + visitor.visit_file(&syntax); + Ok(json!({"comments": comments, "functions": visitor.functions})) +} + +fn main() -> Result<(), Box> { + let paths: Vec = serde_json::from_reader(io::stdin())?; + let mut result = serde_json::Map::new(); + for path in paths { + let source = fs::read_to_string(&path)?; + let inspected = inspect(&source).map_err(|error| format!("{path}: {error}"))?; + result.insert(path, inspected); + } + serde_json::to_writer(io::stdout(), &result)?; + Ok(()) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn preserves_real_comments_but_not_raw_string_contents() { + let source = + "fn f() { // real\n let x = r###\"// fake /* fake */\"###; /* outer /* inner */ */ }"; + let value = inspect(source).unwrap(); + assert_eq!(value["comments"].as_array().unwrap().len(), 2); + assert_eq!(value["functions"][0]["path"], "f"); + } + + #[test] + fn tracks_unicode_spans_modules_and_nested_functions_before_cfg_filtering() { + let source = "const 雪: u8 = 0; mod m { #[cfg(any())] fn f() { fn inner() {} } }"; + let value = inspect(source).unwrap(); + let functions = value["functions"].as_array().unwrap(); + assert_eq!(functions[0]["path"], "m::f"); + assert_eq!(functions[0]["supported"], true); + assert_eq!(functions[1]["supported"], false); + let open = functions[0]["open"].as_u64().unwrap() as usize; + assert!(source[open..].starts_with("{ fn inner()")); + } +} diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md new file mode 100644 index 0000000000..9d0c126579 --- /dev/null +++ b/verification/aeneas/README.md @@ -0,0 +1,281 @@ + + +# Aeneas verification in CI + +The `aeneas` job in `.github/workflows/ci.yml` compiles the current zerocopy +library with Charon, translates selected helpers to Lean with Aeneas, compares +the live output with goldens rendered from inline Rust comments, and +independently builds the inline proofs and checks their transitive axiom +dependencies against both models. +The existing required `All checks succeeded (ci.yml)` job depends on it. + +## Scope and proofs + +Extraction starts from these actual functions in `zerocopy/src/util/mod.rs`, +including their dependencies; there is no copied Rust implementation: + +| Rust function | Checked property | +| --- | --- | +| `max` | Terminates successfully and returns the mathematical maximum. | +| `min` | Terminates successfully and returns the mathematical minimum. | +| `padding_needed_for` | For any positive alignment, succeeds with padding strictly below that alignment. | +| `round_down_to_next_multiple_of_alignment` | For any positive power-of-two alignment, succeeds with a result no larger than the input and divisible by the alignment. | + +The theorems quantify over all values of the extracted unsigned integer model; +these are not finite collections of test inputs. Aeneas's Hoare specification +notation includes successful termination, rather than only a postcondition +conditional on success. The min/max proofs explicitly exhibit the result. + +CI uses the default features, debug assertions, and the runner's native +`x86_64-unknown-linux-gnu` target. Local replay also supports macOS arm64. This +initial scope does not prove minimum padding, maximality of rounded results, +all `DstLayout` operations, other feature/target combinations, or zerocopy's +memory safety. Aeneas currently targets a safe Rust subset; compiling the whole +unsafe crate to a complete verified model is a separate task. + +## Reproduce + +Install `rustup`, Python 3.9+, Git, curl, tar, and zstd, then run from the repository +root: + +```bash +bash verification/aeneas/setup.sh +bash verification/aeneas/run.sh +bash verification/aeneas/negative-controls.sh +python3 -B -m unittest discover -s verification/aeneas/tests +``` + +The runner builds `tools/aeneas-inline` with the pinned compiler. To run that +tool's own tests, use: + +```bash +source verification/aeneas/toolchain.sh +CARGO_TARGET_DIR=target/aeneas/annotation-tool \ + cargo +"$AENEAS_RUST_TOOLCHAIN" test --locked \ + --manifest-path tools/Cargo.toml -p aeneas-inline +``` + +`setup.sh` downloads SHA-256-checked release archives and installs the matching +Rust compiler with `rustc-dev` and `rust-src`. It fetches the pinned Lean +backend's Mathlib dependencies using its supplied lockfile. Cache downloads +are limited to modules imported by the backend and their dependencies. + +The resulting tools live in ignored `target/aeneas/toolchain`. To reuse an +existing installation with the same bundle layout, set `AENEAS_TOOLCHAIN_DIR`. +`run.sh` checks tool versions before extraction. It runs Charon with +`--preset=aeneas --sysroot default`, using Aeneas's builtin models for standard +library operations instead of regenerating a sysroot. Cargo resolves the +library's dependencies from its checked-in vendor configuration, offline and +locked. Charon is a compiler driver and selects its own Rust version; it does +not use zerocopy's ordinary Cargo wrapper or its stable/nightly aliases. + +Every run replaces `target/aeneas/verification` (live extraction) and +`target/aeneas/golden-verification` (checked-in model), including their compiled +Lean artifacts. This prevents stale declarations or the other model's artifacts +from passing after source is removed or renamed. Both retain Lean sources, +handwritten models/proofs, and resolved Lake manifests for inspection; the live +directory also retains LLBC. External templates are compared but never imported +into proofs as axioms. + +## Inline annotations and complete accounting + +Each annotated function starts with an ordinary Rust line-comment fence. The +opening comment must literally be the first non-whitespace token after the +function body's `{`; preceding comments, attributes, or statements are errors. +The following is schematic; actual annotations contain complete declarations: + +````rust +fn example() { + // ```aeneas + // model: + // def util.example ... := ... + // proof: + // theorem example_spec ... := by + // ... + // ``` + ... +} +```` + +Only `model:` followed by `proof:` is supported. Each section contains one +complete Lean declaration, indented by two spaces after the `// ` prefix. +Extraction removes exactly that prefix and section indentation, preserving +Lean's remaining indentation. Consecutive ordinary line comments are required; +doc comments, block comments, missing fences, extra sections, and extra +top-level Lean declarations are rejected. + +`inventory.json` independently registers each function's Rust identity, source +file, parsed function identity, Lean definition, theorem, and golden filename. +Removing or mistyping an existing annotation fails because its inventory entry +still requires it. Discovery searches repository Rust files regardless of +`cfg`, excluding only `.git`, `target`, `vendor`, and `.lake` directories. It +recognizes suspicious fence guards, including case variants and close spelling +errors, then requires exact syntax. A Rust lexer distinguishes comments from +string contents; `syn` resolves function braces and inline modules before +conditional compilation. An unknown annotation is an error, not an opt-in +that CI can overlook. + +Initial support covers free functions in conventional `zerocopy/src` module +paths. Methods, nested functions, macros, and custom module-path layouts need +explicit tooling support; an annotation in an unsupported position fails. +Every registered root must be extracted in the current CI configuration. +Charon's root identities, local source contents, file paths, and function-body +end spans must match the annotations. This prevents a same-named `cfg` +alternative or a stale extraction from standing in for the annotated body. + +Each annotation has exactly one function template in `golden/`, and every file +there must correspond to one registered annotation. That file contains one +`@@AENEAS_MODEL("rust::identity")@@` slot. `scaffolding/` separately retains the +generated types, external templates, trait dictionaries, and module structure; +each function slot appears there exactly once as +`@@AENEAS_GOLDEN("function.lean.in")@@`. Unknown, missing, repeated, or +unexpanded slots fail. `target/aeneas/rendered-golden` holds the assembled model +used for comparison. These invalid-Lean slots are expanded before compilation +and never interpreted as ordinary comments. + +Proof bodies live only in the Rust annotations. `lean/Proofs.lean.in` supplies +their shared imports and abbreviation. `lean/Obligations.lean` independently +records the required propositions; generated `Required.lean` checks each inline +theorem against its required type. A theorem of `True` with the correct name +cannot substitute for a required property. Removing coverage requires explicit +changes to the inventory, golden slots, scaffolding, and required propositions. +The claims remain the properties listed above, not complete verification of a +function's documentation or all compilation configurations. + +No parser can recognize every informal prose claim as a proof. The `aeneas` +fence is the reserved, CI-checked convention; other explanatory comments do not +claim this status. Near-miss guard detection and the independent inventory +protect that convention without treating all mathematical prose as annotations. + +## Updating models and fuzzy comparison + +Never edit an inline generated model or shared extraction scaffolding manually. +Regenerate them with: + +```bash +bash verification/aeneas/run.sh --update-goldens +``` + +This command performs a fresh extraction and checks the existing inline proofs +and required propositions against the live output before updating anything. +It then updates only the `model:` sections of Rust comments, function golden +slots, and shared scaffolding; proof text and executable Rust are preserved. +Finally it checks comparison and both model builds. Review and commit all +changed source comments and scaffolding alongside the Rust or pin changes that +prompted them. Ordinary CI never updates checked-in files. + +To add coverage, first add the fenced model/proof, inventory entry, and required +proposition. The update command creates the missing function golden only after +the live proof succeeds. Ordinary CI always requires the complete bijection. +The pinned generator's root declaration layout is deliberately checked during +updates; an incompatible layout requires an explicit tooling change. + +The fuzzy comparison ignores line and nested block comments (including source +locations), empty nonliteral lines, and trailing horizontal whitespace outside +literals. It preserves code, indentation, nonempty line boundaries, interior +whitespace, and string/character/quoted-identifier contents. Unsupported raw or +interpolated strings and malformed comments/literals fail closed. This is a +limited comparison for the pinned generator's syntax, not a general Lean +parser, alpha-equivalence checker, or semantic equivalence proof. Missing or +additional generated files, changes to external-template signatures, and code +changes fail with a normalized diff and require regeneration. + +After comparison succeeds, CI compiles the checked-in model and the unmodified +live model in separate fresh Lake workspaces. Both must prove the same four +properties and pass the required-type checks and axiom audit; neither imports +the other's compiled model. The live functions always come from Aeneas. Inline +definitions are inserted only into the checked-in model, never into live output. +The normalized text is only used for comparison, never for proof compilation. +This independently checks that accepted differences preserve the properties we +prove. Those properties do not fully specify every helper, so passing both +builds does not by itself establish full semantic equivalence. Keep accepted +fuzziness narrow; stronger equivalence claims require additional theorems. + +## Pins and upgrade procedure + +The selected release is +[`nightly-2026.10.01-ca282ec`](https://github.com/AeneasVerif/aeneas/releases/tag/nightly-2026.10.01-ca282ec). +`toolchain.sh` records its full Aeneas commit, the compatible Charon commit from +[`charon-pin`](https://github.com/AeneasVerif/aeneas/blob/ca282ec2312a96f6a985a4d23a663690816d3f3e/charon-pin), +Rust `nightly-2026-09-17`, Lean `4.31.0`, and platform archive digests. The release +supplies prebuilt Aeneas/Charon binaries and compiled Lean backend artifacts. +Its `lake-manifest.json` pins Mathlib and transitive dependencies; the generated +proof workspace shares those fetched dependencies through path entries instead +of resolving a second copy. + +Upgrade this tuple together. Verify archive digests, resolve the new +`charon-pin`, inspect that Charon revision's Rust toolchain and Aeneas's Lean +version, and run extraction and all proofs from fresh output. Review new +external templates, the generated helper bodies, proof statements, and axiom +results. Remove or adapt the naming workaround only after inspecting the new +output. Do not pair Aeneas with an independently selected Charon nightly. + +## Trust boundary and failure checks + +These are Lean theorems about generated functions. Transferring them to Rust +requires the following external correspondence premises, which this CI job +records but does not formally prove: + +- Rust MIR generation and Charon's LLBC extraction preserve these selected + functions' semantics for the pinned configuration. +- Aeneas's translation and the pinned integer, comparison, wrapping-subtraction, + bitwise, and assertion models represent those Rust operations faithfully. +- The handwritten `NonZero` wrapper represents its stored value; + `NonZero::get` succeeds with that value and `NonZeroUsizeInner::clone` + succeeds with a copy. These models abstract values, not niche encoding, + layout, validity, or memory operations. The wrapper over-approximates valid + Rust values by admitting zero; the alignment proofs explicitly require + positivity rather than assuming it through an axiom. +- Lean's kernel, its standard logic axioms, and the imported proof artifacts + check the encoded propositions correctly. Release checksums establish + artifact identity, not a proof of compiler or model correctness. + +`Check.lean` checks that required declarations are theorems and audits all +declarations in `Zerocopy.Proofs`, `Zerocopy.Obligations`, the translated +`Zerocopy.util` namespace, and the external `core.num` models. Only `propext`, +`Classical.choice`, and `Quot.sound` are allowed. New axioms, `sorryAx`, and +native evaluator proof +axioms fail this check. This does not establish the source-to-model +correspondence premises. +CI also runs failure controls in both workspaces: an admitted proof must fail +the axiom audit, an unrelated `True` theorem must fail its required type, and +reversing the translated `min` comparison must fail its proof. In the live +workspace, comment drift must pass fuzzy comparison and +proof checking, while reversing `min` must also fail comparison. These controls +edit scratch files and restore them before rechecking the original results. + +Extraction rejects warnings, translation errors, missing artifacts, and LLBC +whose `has_errors` is not exactly `false`, even when Charon exits zero. +`prepare.py` also repairs one pinned Aeneas naming collision: +`ZeroablePrimitive` has two `Copy` parent dictionaries, which Aeneas names +`markerCopyInst`. The second projection and its initializer are renamed +`innerCopyInst`. Both dictionary types and values are preserved, and no helper +body is changed. Each replacement must match exactly once; unexpected output +fails rather than silently applying a broader rewrite. + +## Research used + +The upstream [Aeneas README](https://github.com/AeneasVerif/aeneas) describes the +Charon-to-LLBC-to-Lean pipeline, required compatible pins, external model +workflow, and safe-subset limitations. The repository's `reference` branch +provided useful prior evidence: + +- [Compatible bundle drift](https://github.com/google/zerocopy/blob/ba4556c30835b56d108b0a6854a760bccf8438c5/reports/aeneas-compatible-bundle-source-drift-2026-09-30/REPORT.md) + identifies the newer Lean module output and the need to resolve Charon from + Aeneas's pin rather than release dates. +- [External models](https://github.com/google/zerocopy/blob/ba4556c30835b56d108b0a6854a760bccf8438c5/reports/aeneas-external-models-nightly-2026-06-03/REPORT.md) + explains the generated templates and the semantic boundary of model + registrations. +- [Whole-library Charon extraction](https://github.com/google/zerocopy/blob/ba4556c30835b56d108b0a6854a760bccf8438c5/reports/charon-zerocopy-library-repeat-order-nightly-2026-05-31/REPORT.md) + observed successful process exits with `has_errors: true`, supporting the + explicit LLBC completeness check. + +Those older experiments are not assumed to describe the current release's +runtime. This integration was validated with the pinned October 1 bundle and +fresh translations of the current checkout. diff --git a/verification/aeneas/golden.py b/verification/aeneas/golden.py new file mode 100644 index 0000000000..bbf6e29d2c --- /dev/null +++ b/verification/aeneas/golden.py @@ -0,0 +1,166 @@ +#!/usr/bin/env python3 +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Compare Aeneas snapshots with narrowly defined, literal-aware fuzziness.""" + +import argparse +import difflib +import re +from pathlib import Path + +FILES = ("Types.lean", "Funs.lean", "TypesExternal_Template.lean", + "FunsExternal_Template.lean") +HANDWRITTEN = {"TypesExternal.lean", "FunsExternal.lean"} +CHAR = re.compile(r"'(?:\\(?:u\{[0-9a-fA-F]+\}|.)|[^'\\\r\n])'") +HEADER = """/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +""" + + +def normalize(source): + # Preserve code, indentation, line boundaries, and literal bytes. Comments + # become a space (not concatenation), retaining their newlines. Only empty + # nonliteral lines and nonliteral trailing horizontal spaces are dropped. + lines = [] + line = [] + i = 0 + + def emit(char, literal=False): + if char == "\n": + finish() + else: + line.append((char, literal)) + + def finish(): + while line and line[-1][0] in " \t\r" and not line[-1][1]: + line.pop() + if line: + lines.append("".join(char for char, _ in line)) + line.clear() + + while i < len(source): + if source.startswith("--", i): + end = source.find("\n", i) + end = len(source) if end == -1 else end + emit(" ") + i = end + elif source.startswith("/-", i): + depth = 1 + emit(" ") + i += 2 + while depth: + if i == len(source): + raise ValueError("Unterminated Lean block comment") + if source.startswith("/-", i): + depth += 1 + i += 2 + elif source.startswith("-/", i): + depth -= 1 + i += 2 + else: + if source[i] == "\n": + emit("\n") + i += 1 + elif source[i] == '"' or source[i] == "«": + end_char = '"' if source[i] == '"' else "»" + # Raw and interpolated strings need their own lexer. This pinned + # generator emits neither; fail closed if an upgrade adds them. + if end_char == '"' and (re.search(r"r#*$", source[:i]) or + source[:i].endswith('!')): + raise ValueError("Unsupported raw or interpolated Lean string") + emit(source[i], True) + i += 1 + while True: + if i == len(source): + raise ValueError("Unterminated Lean literal") + char = source[i] + # Preserve empty lines INSIDE literals, unlike empty code lines. + if char == "\n" and not line: + line.append(("", True)) + emit(char, True) + i += 1 + if char == end_char: + break + if char == "\\" and end_char == '"': + if i == len(source): + raise ValueError("Unterminated Lean escape") + emit(source[i], True) + i += 1 + elif source[i] == "'" and (match := CHAR.match(source, i)): + for char in match[0]: + emit(char, True) + i = match.end() + else: + emit(source[i]) + i += 1 + finish() + return lines + + +def files(directory, live=False): + actual = {str(p.relative_to(directory)) for p in directory.rglob("*.lean")} + if live: + actual -= HANDWRITTEN + if actual != set(FILES): + raise ValueError(f"Unexpected generated file set in {directory}: " + f"missing={sorted(set(FILES) - actual)}, " + f"extra={sorted(actual - set(FILES))}") + return {name: (directory / name).read_bytes().decode("utf-8") for name in FILES} + + +def compare(live, golden): + generated = files(live, live=True) + checked_in = files(golden) + differences = [] + for name in FILES: + before, after = normalize(checked_in[name]), normalize(generated[name]) + if before != after: + differences.extend(difflib.unified_diff( + before, after, fromfile=f"golden/{name}", + tofile=f"live/{name}", lineterm="")) + return differences + + +def update(live, golden): + generated = files(live, live=True) + # Validate the complete candidate before changing any checked-in file. + for source in generated.values(): + normalize(source) + if golden.exists(): + files(golden) + golden.mkdir(parents=True, exist_ok=True) + for name in FILES: + (golden / name).write_text(HEADER + generated[name], encoding="utf-8") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("command", choices=["compare", "update"]) + parser.add_argument("live", type=Path) + parser.add_argument("golden", type=Path) + args = parser.parse_args() + if args.command == "update": + update(args.live, args.golden) + else: + differences = compare(args.live, args.golden) + if differences: + print("\n".join(differences)) + raise SystemExit("Aeneas goldens differ. Review the extraction and run " + "bash verification/aeneas/run.sh --update-goldens") + print("Live Aeneas output matches goldens under the fuzzy comparison") + + +if __name__ == "__main__": + main() diff --git a/verification/aeneas/golden/util.max.lean.in b/verification/aeneas/golden/util.max.lean.in new file mode 100644 index 0000000000..dace80ba80 --- /dev/null +++ b/verification/aeneas/golden/util.max.lean.in @@ -0,0 +1,9 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +@@AENEAS_MODEL("zerocopy::util::max")@@ diff --git a/verification/aeneas/golden/util.min.lean.in b/verification/aeneas/golden/util.min.lean.in new file mode 100644 index 0000000000..d5fd78bedd --- /dev/null +++ b/verification/aeneas/golden/util.min.lean.in @@ -0,0 +1,9 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +@@AENEAS_MODEL("zerocopy::util::min")@@ diff --git a/verification/aeneas/golden/util.padding_needed_for.lean.in b/verification/aeneas/golden/util.padding_needed_for.lean.in new file mode 100644 index 0000000000..2ddbfe7d5f --- /dev/null +++ b/verification/aeneas/golden/util.padding_needed_for.lean.in @@ -0,0 +1,9 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +@@AENEAS_MODEL("zerocopy::util::padding_needed_for")@@ diff --git a/verification/aeneas/golden/util.round_down_to_next_multiple_of_alignment.lean.in b/verification/aeneas/golden/util.round_down_to_next_multiple_of_alignment.lean.in new file mode 100644 index 0000000000..918795eef9 --- /dev/null +++ b/verification/aeneas/golden/util.round_down_to_next_multiple_of_alignment.lean.in @@ -0,0 +1,9 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +@@AENEAS_MODEL("zerocopy::util::round_down_to_next_multiple_of_alignment")@@ diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py new file mode 100644 index 0000000000..478f82a1cb --- /dev/null +++ b/verification/aeneas/inline.py @@ -0,0 +1,350 @@ +#!/usr/bin/env python3 +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Account for every inline Aeneas proof and render its checked-in model.""" + +import argparse +import difflib +import json +import os +import re +import subprocess +from pathlib import Path + +import golden + +MARKER = re.compile(r'`{2,}\s*([^\s`]+)') +MODEL_SLOT = re.compile(r'@@AENEAS_MODEL\("([^"\n]+)"\)@@') +GOLDEN_SLOT = re.compile(r'@@AENEAS_GOLDEN\("([^"\n]+)"\)@@') + + +def suspicious(text): + return any(word.lower().startswith("aeneas") or + difflib.SequenceMatcher(None, word.lower(), "aeneas").ratio() >= 0.7 + for word in MARKER.findall(text)) + + +def read_source(path): + return path.read_bytes().decode('utf-8') + + +def inventory(root): + data = json.loads((root / 'verification/aeneas/inventory.json').read_text()) + if data['version'] != 1 or not data['functions']: + raise ValueError('Unsupported or empty Aeneas proof inventory') + entries = data['functions'] + for key in ('rust', 'model', 'theorem', 'golden'): + if len({e[key] for e in entries}) != len(entries): + raise ValueError(f'Duplicate {key} in proof inventory') + for entry in entries: + if set(entry) != {'rust', 'file', 'syntax', 'model', 'theorem', 'golden'}: + raise ValueError('Unknown or missing inventory fields') + identifier = r'[A-Za-z_][A-Za-z_0-9]*' + patterns = {'rust': rf'{identifier}(?:::{identifier})*', + 'syntax': rf'{identifier}(?:::{identifier})*', + 'model': rf'{identifier}(?:\.{identifier})*', 'theorem': identifier} + if not all(re.fullmatch(pattern, entry[key]) for key, pattern in patterns.items()): + raise ValueError('Unsupported declaration identity in inventory') + if not re.fullmatch(r'[A-Za-z_][A-Za-z_0-9.]*\.lean\.in', entry['golden']): + raise ValueError('Golden must be a single .lean.in filename') + if not entry['file'].startswith('zerocopy/src/') or '..' in Path(entry['file']).parts: + raise ValueError('Only explicit zerocopy source files are supported') + relative = Path(entry['file']).relative_to('zerocopy/src') + modules = list(relative.parent.parts) + if relative.stem not in ('mod', 'lib'): + modules.append(relative.stem) + expected_rust = '::'.join(['zerocopy', *modules, entry['syntax']]) + if entry['rust'] != expected_rust: + raise ValueError('Rust identity must agree with the conventional source module path') + return entries + + +def source_files(root, entries): + # Discover across inactive cfg branches and all repository Rust sources, + # not just the registered files. Only generated/vendor directories are out + # of scope. A candidate in an unsupported source location is an error. + paths = {e['file'] for e in entries} + for directory, dirs, filenames in os.walk(root): + dirs[:] = [d for d in dirs if d not in {'.git', 'target', 'vendor', '.lake'}] + for name in filenames: + if name.endswith('.rs'): + path = Path(directory) / name + if suspicious(read_source(path)): + paths.add(str(path.relative_to(root))) + return sorted(paths) + + +def parse_file(source, syntax): + # Rust lexer offsets are bytes; Python slices are Unicode code points. + def char_offset(byte): + return len(source.encode('utf-8')[:byte].decode('utf-8')) + + comments = [(char_offset(c['start']), char_offset(c['end'])) + for c in syntax['comments']] + functions = [{**f, 'open': char_offset(f['open']), 'close': char_offset(f['close'])} + for f in syntax['functions']] + found = [] + consumed = set() + for index, (start, end) in enumerate(comments): + if index in consumed or not suspicious(source[start:end]): + continue + if source[start:end].rstrip() != '// ```aeneas': + raise ValueError('Malformed, unsupported, or misspelled aeneas fence') + owners = [f for f in functions if f['supported'] and f['open'] < start + and not source[f['open'] + 1:start].strip()] + if len(owners) != 1: + raise ValueError('Aeneas fence must be the first non-whitespace token after a function {') + payload = [] + payload_indices = [] + previous_end = end + consumed.add(index) + for following in range(index + 1, len(comments)): + a, b = comments[following] + if source[previous_end:a].strip(): + raise ValueError('Aeneas fence must contain consecutive line comments') + text = source[a:b].rstrip('\r') + consumed.add(following) + if text.rstrip() == '// ```': + break + if not text.startswith('// ') and text != '//': + raise ValueError('Aeneas payload requires ordinary // line comments') + payload.append(text[3:] if text.startswith('// ') else '') + payload_indices.append((a, b)) + previous_end = b + else: + raise ValueError('Unterminated aeneas fence') + if not payload or payload[0] != 'model:' or payload.count('proof:') != 1: + raise ValueError('Aeneas fence requires exactly model: then proof:') + split = payload.index('proof:') + sections = [] + for lines in (payload[1:split], payload[split + 1:]): + if not lines or any(line and not line.startswith(' ') for line in lines): + raise ValueError('Aeneas model/proof content must be indented by two spaces') + content = '\n'.join(line[2:] if line else '' for line in lines) + '\n' + normalized = golden.normalize(content) + if not normalized or any(line and not line[0].isspace() for line in normalized[1:]): + raise ValueError('Each section must contain exactly one top-level declaration') + sections.append(content) + indent = source[source.rfind('\n', 0, start) + 1:start] + if indent.strip(): + # Allow `{ // fence` but use normal indentation for regenerated lines. + indent = ' ' + first = payload_indices[1][0] + last = payload_indices[split][0] + model_start = source.rfind('\n', 0, first) + 1 + model_end = source.rfind('\n', 0, last) + 1 + found.append({'syntax': owners[0]['path'], 'model_text': sections[0], + 'proof_text': sections[1], 'model_start': model_start, + 'model_end': model_end, 'indent': indent, + 'newline': '\r\n' if '\r\n' in source else '\n', + 'open_line': source[:owners[0]['open']].count('\n') + 1, + 'end_line': source[:owners[0]['close']].count('\n') + 1, + 'end_col': owners[0]['close'] - source.rfind('\n', 0, owners[0]['close']) - 1}) + return found + + +def discover(root, tool, entries): + paths = source_files(root, entries) + result = subprocess.run([str(tool)], cwd=root, input=json.dumps(paths), + text=True, capture_output=True) + if result.returncode: + raise ValueError(f'Rust syntax inspection failed: {result.stderr}') + syntax = json.loads(result.stdout) + annotations = {} + for file in paths: + try: + found = parse_file(read_source(root / file), syntax[file]) + except ValueError as error: + raise ValueError(f'{file}: {error}') from error + for annotation in found: + matches = [e for e in entries if e['file'] == file and e['syntax'] == annotation['syntax']] + if len(matches) != 1: + raise ValueError(f'Unregistered annotation in {file}: {annotation["syntax"]}') + entry = matches[0] + if entry['rust'] in annotations: + raise ValueError(f'Duplicate annotation: {entry["rust"]}') + for section, keyword, name in [('model_text', 'def', entry['model']), + ('proof_text', 'theorem', entry['theorem'])]: + first = golden.normalize(annotation[section])[0] + if not re.match(rf'{keyword} {re.escape(name)}(?=\s|\(|$)', first): + raise ValueError(f'{entry["rust"]}: unexpected {keyword} declaration') + annotations[entry['rust']] = {**entry, **annotation} + missing = {e['rust'] for e in entries} - annotations.keys() + if missing: + raise ValueError(f'Missing inline annotations: {sorted(missing)}') + return annotations + + +def templates(root, entries, allow_missing=False): + directory = root / 'verification/aeneas/golden' + actual = {str(p.relative_to(directory)) for p in directory.rglob('*') if p.is_file()} + expected = {e['golden'] for e in entries} + if actual - expected or (not allow_missing and actual != expected): + raise ValueError(f'Annotation/golden bijection failed: missing={expected - actual}, extra={actual - expected}') + for entry in entries: + if allow_missing and not (directory / entry['golden']).exists(): + continue + text = (directory / entry['golden']).read_text() + if golden.normalize(text) != [f'@@AENEAS_MODEL("{entry["rust"]}")@@']: + raise ValueError(f'Golden must contain exactly its registered model slot: {entry["golden"]}') + + +def render(root, annotations, destination): + scaffolding = root / 'verification/aeneas/scaffolding' + actual = {p.name for p in scaffolding.iterdir() if p.is_file()} + if actual != set(golden.FILES): + raise ValueError('Unexpected shared Aeneas scaffolding file set') + by_golden = {a['golden']: a for a in annotations.values()} + used = [] + + def expand(match): + name = match[1] + if name not in by_golden: + raise ValueError(f'Unknown function golden slot: {name}') + used.append(name) + return by_golden[name]['model_text'].rstrip('\n') + + destination.mkdir(parents=True, exist_ok=True) + rendered = {name: GOLDEN_SLOT.sub(expand, (scaffolding / name).read_text()) + for name in golden.FILES} + if sorted(used) != sorted(by_golden): + raise ValueError('Every function golden must occur exactly once in scaffolding') + for name, text in rendered.items(): + if '@@AENEAS_' in text: + raise ValueError(f'Unexpanded Aeneas slot in {name}') + (destination / name).write_text(text) + + +def assemble(root, annotations, work): + wrapper = (root / 'verification/aeneas/lean/Proofs.lean.in').read_text() + if wrapper.count('@@AENEAS_PROOFS@@') != 1: + raise ValueError('Proof wrapper must have exactly one proof slot') + proofs = '\n'.join(a['proof_text'] for a in annotations.values()) + (work / 'Proofs.lean').write_text(wrapper.replace('@@AENEAS_PROOFS@@', proofs)) + required = ['import Lean', 'import Proofs', 'import Obligations', 'open Lean', ''] + for a in annotations.values(): + required.append(f'example : Zerocopy.Obligations.{a["theorem"]} := Zerocopy.Proofs.{a["theorem"]}') + names = ', '.join(f'`Zerocopy.Proofs.{a["theorem"]}' for a in annotations.values()) + required.append(f'def requiredTheorems : Array Name := #[{names}]') + (work / 'Required.lean').write_text('\n'.join(required) + '\n') + + +def check_bindings(root, annotations, llbc): + # Names alone are insufficient: cfg alternatives can define the same Rust + # path. Require Charon to have extracted the exact annotated source body. + translated = json.loads(llbc.read_text())['translated'] + files = {f['id']: f for f in translated['files']} + roots = {} + for function in translated['fun_decls']: + if not function or function['item_meta'].get('started_from') is not True: + continue + meta = function['item_meta'] + if not all(set(element) == {'Ident'} and element['Ident'][1] == 0 + for element in meta['name']): + raise ValueError('Unsupported extracted root identity') + name = '::'.join(element['Ident'][0] for element in meta['name']) + if name in roots: + raise ValueError('Duplicate extracted root identity') + roots[name] = meta + if roots.keys() != annotations.keys(): + raise ValueError('Extracted roots do not match the annotated inventory') + for rust, annotation in annotations.items(): + meta = roots[rust] + span = meta['span']['Untagged'] + data = span['data'] + file = files[data['file_id']] + source = read_source(root / annotation['file']).replace('\r\n', '\n') + if (meta.get('is_local') is not True or span['generated_from_span'] is not None + or file['name'] != {'Local': annotation['file'].removeprefix('zerocopy/')} + or file['contents'].replace('\r\n', '\n') != source + or not data['beg']['line'] <= annotation['open_line'] <= data['end']['line'] + or data['end'] != {'line': annotation['end_line'], 'col': annotation['end_col']}): + raise ValueError(f'Charon extracted a different source body for {rust}') + + +def split_live(source, entries): + # This intentionally supports the pinned generator's root-declaration + # layout only. Full-file comparison includes all remaining scaffolding; + # unexpected layouts, missing/duplicate roots or new output fail closed. + starts = list(re.finditer(r'^/-- \[(zerocopy::[^\]\n]+)\]:\n', source, re.M)) + if {m[1] for m in starts} != {e['rust'] for e in entries} or len(starts) != len(entries): + raise ValueError('Pinned Aeneas root declaration layout no longer matches inventory') + by_rust = {e['rust']: e for e in entries} + replacements = [] + models = {} + for index, match in enumerate(starts): + end = starts[index + 1].start() if index + 1 < len(starts) else source.rfind('\nend Zerocopy') + # Aeneas ends these documentation comments on the Source: line. + close = source.find('-/\n', match.start(), end) + if close < 0 or end < 0: + raise ValueError('Missing generated root documentation or namespace end') + declaration_start = close + 3 + model = source[declaration_start:end].rstrip() + '\n' + entry = by_rust[match[1]] + lines = golden.normalize(model) + if not lines or not re.match(rf'def {re.escape(entry["model"])}(?=\s|\(|$)', lines[0]): + raise ValueError('Unexpected generated Lean root identity') + if any(line and not line[0].isspace() for line in lines[1:]): + raise ValueError('Unsupported generated root declaration layout') + models[match[1]] = model + replacements.append((declaration_start, end, f'@@AENEAS_GOLDEN("{entry["golden"]}")@@\n\n')) + for start, end, replacement in reversed(replacements): + source = source[:start] + replacement + source[end:] + return models, source + + +def update(root, entries, annotations, live): + models, funs = split_live((live / 'Funs.lean').read_text(), entries) + golden.files(live, live=True) + changes = {} + for rust, annotation in annotations.items(): + payload = ''.join(annotation['indent'] + '// ' + line + annotation['newline'] + for line in models[rust].splitlines()) + changes.setdefault(annotation['file'], []).append( + (annotation['model_start'], annotation['model_end'], payload)) + for file, replacements in changes.items(): + path = root / file + source = read_source(path) + for start, end, replacement in sorted(replacements, reverse=True): + source = source[:start] + replacement + source[end:] + path.write_bytes(source.encode('utf-8')) + for entry in entries: + (root / 'verification/aeneas/golden' / entry['golden']).write_text( + golden.HEADER + f'@@AENEAS_MODEL("{entry["rust"]}")@@\n') + for name in golden.FILES: + text = funs if name == 'Funs.lean' else (live / name).read_text() + (root / 'verification/aeneas/scaffolding' / name).write_text(golden.HEADER + text) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('command', choices=['scan', 'scan-update', 'bindings', 'render', 'assemble', 'update']) + parser.add_argument('--root', type=Path, required=True) + parser.add_argument('--tool', type=Path, required=True) + parser.add_argument('--work', type=Path, required=True) + args = parser.parse_args() + entries = inventory(args.root) + annotations = discover(args.root, args.tool, entries) + if args.command == 'bindings': + check_bindings(args.root, annotations, args.work / 'zerocopy.llbc') + elif args.command == 'update': + update(args.root, entries, annotations, args.work) + elif args.command == 'assemble': + assemble(args.root, annotations, args.work) + else: + templates(args.root, entries, allow_missing=args.command == 'scan-update') + if args.command in ('scan', 'scan-update'): + (args.work / 'annotations.json').write_text(json.dumps(annotations, indent=2) + '\n') + (args.work / 'roots.txt').write_text(','.join(annotations) + '\n') + elif args.command == 'render': + render(args.root, annotations, args.work) + + +if __name__ == '__main__': + main() diff --git a/verification/aeneas/inventory.json b/verification/aeneas/inventory.json new file mode 100644 index 0000000000..80da2c36d0 --- /dev/null +++ b/verification/aeneas/inventory.json @@ -0,0 +1,38 @@ +{ + "license": "/- Copyright 2026 The Fuchsia Authors\n\nLicensed under a BSD-style license , Apache License, Version 2.0\n, or the MIT\nlicense , at your option.\nThis file may not be copied, modified, or distributed except according to\nthose terms. -/", + "version": 1, + "functions": [ + { + "rust": "zerocopy::util::max", + "file": "zerocopy/src/util/mod.rs", + "syntax": "max", + "model": "util.max", + "theorem": "max_spec", + "golden": "util.max.lean.in" + }, + { + "rust": "zerocopy::util::min", + "file": "zerocopy/src/util/mod.rs", + "syntax": "min", + "model": "util.min", + "theorem": "min_spec", + "golden": "util.min.lean.in" + }, + { + "rust": "zerocopy::util::padding_needed_for", + "file": "zerocopy/src/util/mod.rs", + "syntax": "padding_needed_for", + "model": "util.padding_needed_for", + "theorem": "padding_lt_alignment", + "golden": "util.padding_needed_for.lean.in" + }, + { + "rust": "zerocopy::util::round_down_to_next_multiple_of_alignment", + "file": "zerocopy/src/util/mod.rs", + "syntax": "round_down_to_next_multiple_of_alignment", + "model": "util.round_down_to_next_multiple_of_alignment", + "theorem": "round_down_spec", + "golden": "util.round_down_to_next_multiple_of_alignment.lean.in" + } + ] +} diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean new file mode 100644 index 0000000000..a7932e152c --- /dev/null +++ b/verification/aeneas/lean/Check.lean @@ -0,0 +1,27 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +import Required +open Lean Elab Command +run_elab do + let required := requiredTheorems + let env ← getEnv + for declName in required do + match env.find? declName with + | some (.thmInfo _) => pure () + | _ => throwError "Missing required theorem {declName}" + let prefixes := #[`Zerocopy.Proofs, `Zerocopy.Obligations, `Zerocopy.util, `core.num] + let mut audited := 0 + for (declName, _) in env.constants.toList do + if prefixes.any (·.isPrefixOf declName) then + let used ← collectAxioms declName + for ax in used do + unless #[`propext, `Classical.choice, `Quot.sound].contains ax do + throwError "{declName} depends on unapproved axiom {ax}" + audited := audited + 1 + logInfo m!"Checked axiom dependencies of {audited} declarations" diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean new file mode 100644 index 0000000000..58f7972ea8 --- /dev/null +++ b/verification/aeneas/lean/Obligations.lean @@ -0,0 +1,36 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy.Funs +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Obligations +abbrev NonZeroUsize := + core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner + +def max_spec : Prop := + ∀ (a b : NonZeroUsize), + ∃ r, util.max a b = .ok r ∧ r.val.val = Nat.max a.val.val b.val.val + +def min_spec : Prop := + ∀ (a b : NonZeroUsize), + ∃ r, util.min a b = .ok r ∧ r.val.val = Nat.min a.val.val b.val.val + +def padding_lt_alignment : Prop := + ∀ (len : Usize) (align : NonZeroUsize) + (_h : 0 < align.val.val), + util.padding_needed_for len align ⦃ p => p.val < align.val.val ⦄ + +def round_down_spec : Prop := + ∀ (n : Usize) (align : NonZeroUsize) + (_hpos : 0 < align.val.val) (_h : align.val.val.isPowerOfTwo), + util.round_down_to_next_multiple_of_alignment n align + ⦃ m => m.val ≤ n.val ∧ m.val % align.val.val = 0 ⦄ + +end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean.in b/verification/aeneas/lean/Proofs.lean.in new file mode 100644 index 0000000000..4814022daf --- /dev/null +++ b/verification/aeneas/lean/Proofs.lean.in @@ -0,0 +1,19 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy.Funs +import all Init.Data.Nat.Power2.Basic +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Proofs +abbrev NonZeroUsize := + core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner + +@@AENEAS_PROOFS@@ +end Zerocopy.Proofs diff --git a/verification/aeneas/lean/Zerocopy.lean b/verification/aeneas/lean/Zerocopy.lean new file mode 100644 index 0000000000..05ceea6bae --- /dev/null +++ b/verification/aeneas/lean/Zerocopy.lean @@ -0,0 +1,10 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy.Funs diff --git a/verification/aeneas/lean/Zerocopy/FunsExternal.lean b/verification/aeneas/lean/Zerocopy/FunsExternal.lean new file mode 100644 index 0000000000..c820466380 --- /dev/null +++ b/verification/aeneas/lean/Zerocopy/FunsExternal.lean @@ -0,0 +1,24 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Zerocopy.Types +@[expose] public section +open Aeneas Aeneas.Std +open Zerocopy + +-- External semantic models: Clone copies the value; NonZero::get returns its +-- stored integer without failure. Their correspondence to Rust is part of the +-- trusted boundary described in ../../README.md, not a theorem of this package. +def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone + (x : core.num.niche_types.NonZeroUsizeInner) : + Result core.num.niche_types.NonZeroUsizeInner := .ok x + +@[simp] def core.num.nonzero.NonZero.get + {T Inner : Type} (_inst : core.num.nonzero.ZeroablePrimitive T Inner) + (x : core.num.nonzero.NonZero T Inner) : Result T := .ok x.val diff --git a/verification/aeneas/lean/Zerocopy/TypesExternal.lean b/verification/aeneas/lean/Zerocopy/TypesExternal.lean new file mode 100644 index 0000000000..10c6e45a5b --- /dev/null +++ b/verification/aeneas/lean/Zerocopy/TypesExternal.lean @@ -0,0 +1,20 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +module +public import Aeneas +@[expose] public section +open Aeneas.Std + +-- These types model stored values, not Rust's niche encoding or memory layout. +-- The generic wrapper admits zero; the alignment theorems explicitly require +-- positivity. This over-approximation includes every valid NonZeroUsize. +abbrev core.num.niche_types.NonZeroUsizeInner := Usize + +structure core.num.nonzero.NonZero (T : Type) (_Inner : Type) where + val : T diff --git a/verification/aeneas/negative-controls.sh b/verification/aeneas/negative-controls.sh new file mode 100755 index 0000000000..4c941a4551 --- /dev/null +++ b/verification/aeneas/negative-controls.sh @@ -0,0 +1,117 @@ +#!/usr/bin/env bash +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +# Run after run.sh. Mutate generated scratch files, never checked-in sources. +set -euo pipefail +cd "$(dirname "$0")/../.." +repo=$PWD +tools_dir=${AENEAS_TOOLCHAIN_DIR:-"$repo/target/aeneas/toolchain"} +export PATH="$tools_dir/lean/bin:$PATH" +check_workspace() ( +cd "$repo/target/aeneas/$1" +echo "Testing failure controls in $1" +backup=$(mktemp -d) +cp Proofs.lean "$backup/Proofs.lean" +cp Zerocopy/Funs.lean "$backup/Funs.lean" +restore() { + cp "$backup/Proofs.lean" Proofs.lean + cp "$backup/Funs.lean" Zerocopy/Funs.lean + rm -rf "$backup" +} +trap restore EXIT + +if [[ $1 == verification ]]; then + echo '-- Harmless generated-comment difference' >> Zerocopy/Funs.lean + python3 "$repo/verification/aeneas/golden.py" compare \ + "$PWD/Zerocopy" "$repo/target/aeneas/rendered-golden" + lake build > "$backup/comment-build.log" 2>&1 || { + cat "$backup/comment-build.log" >&2; exit 1; + } + lake env lean -DwarningAsError=true Check.lean + echo "Confirmed: comment drift passes comparison and live proofs" +fi + +cat >> Proofs.lean <<'LEAN' +namespace Zerocopy.Proofs +theorem negative_control : True := by sorry +end Zerocopy.Proofs +LEAN +if ! lake build Required > "$backup/sorry-build.log" 2>&1; then + cat "$backup/sorry-build.log" >&2 + exit 1 +fi +if lake env lean Check.lean > "$backup/sorry-check.log" 2>&1; then + echo "Axiom audit accepted an admitted proof" >&2 + exit 1 +fi +if ! grep -q 'unapproved axiom' "$backup/sorry-check.log" || + ! grep -q 'sorryAx' "$backup/sorry-check.log"; then + cat "$backup/sorry-check.log" >&2 + exit 1 +fi +echo "Confirmed: the axiom audit rejects an admitted proof" +cp "$backup/Proofs.lean" Proofs.lean + +python3 - <<'PY' +from pathlib import Path +import re +p = Path("Proofs.lean") +s, count = re.subn(r'theorem min_spec\b.*?(?=\ntheorem |\nend Zerocopy.Proofs)', + 'theorem min_spec : True := by trivial\n', p.read_text(), flags=re.S) +if count != 1: + raise SystemExit("Obligation negative control no longer matches") +p.write_text(s) +PY +if lake build Required > "$backup/obligation-build.log" 2>&1; then + echo "Required obligation accepted an unrelated True theorem" >&2 + exit 1 +fi +if ! grep -Eq '(error: Required[.]lean:|Required[.]lean:.*error)' "$backup/obligation-build.log"; then + cat "$backup/obligation-build.log" >&2 + exit 1 +fi +echo "Confirmed: required obligations reject an unrelated True theorem" +cp "$backup/Proofs.lean" Proofs.lean + +python3 - <<'PY' +from pathlib import Path +p = Path("Zerocopy/Funs.lean") +s = p.read_text() +if s.count("if i > i1") != 1: + raise SystemExit("min negative control no longer matches generated output") +p.write_text(s.replace("if i > i1", "if i < i1")) +PY +if [[ $1 == verification ]]; then + if python3 "$repo/verification/aeneas/golden.py" compare \ + "$PWD/Zerocopy" "$repo/target/aeneas/rendered-golden" \ + > "$backup/mutated-compare.log" 2>&1; then + echo "Fuzzy comparison accepted an incorrect translated min" >&2 + exit 1 + fi + if ! grep -q 'Aeneas goldens differ' "$backup/mutated-compare.log"; then + cat "$backup/mutated-compare.log" >&2 + exit 1 + fi + echo "Confirmed: fuzzy comparison rejects an incorrect translated min" +fi +if lake build Required > "$backup/mutated-build.log" 2>&1; then + echo "Proofs accepted a min implementation with its comparison reversed" >&2 + exit 1 +fi +if ! grep -Eq '(error: Proofs[.]lean:|Proofs[.]lean:.*error)' "$backup/mutated-build.log"; then + cat "$backup/mutated-build.log" >&2 + exit 1 +fi +echo "Confirmed: the proofs reject an incorrect translated min" +cp "$backup/Funs.lean" Zerocopy/Funs.lean +lake build +lake env lean -DwarningAsError=true Check.lean +) +check_workspace golden-verification +check_workspace verification diff --git a/verification/aeneas/prepare.py b/verification/aeneas/prepare.py new file mode 100644 index 0000000000..93a28e97c9 --- /dev/null +++ b/verification/aeneas/prepare.py @@ -0,0 +1,121 @@ +#!/usr/bin/env python3 +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +"""Validate extraction, repair a pinned naming collision, and share Lake deps.""" + +import argparse +import json +import re +from pathlib import Path + + +def check_llbc(path): + data = json.loads(path.read_text()) + # Charon can exit successfully even when extraction was incomplete. + if data.get("has_errors") is not False: + raise ValueError("Charon LLBC is missing has_errors: false") + if not isinstance(data.get("translated"), dict): + raise ValueError("Charon LLBC is missing the translated crate") + + +def rename_copy_fields(types, funs): + # At this exact pin ZeroablePrimitive inherits Copy for both Self and its + # associated NonZeroInner. Aeneas gives both projections the same name. + # Rename ONLY the second projection and its initializer; retain both types + # and both dictionaries. Never change the translated helper bodies. + edits = [ + (types, '"markerCopyInst", "markerCopyInst"', + '"markerCopyInst", "innerCopyInst"'), + (types, "markerCopyInst : core.marker.Copy Self_NonZeroInner", + "innerCopyInst : core.marker.Copy Self_NonZeroInner"), + (funs, "markerCopyInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy", + "innerCopyInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy"), + ] + for content, old, _ in edits: + if content.count(old) != 1: + raise ValueError(f"Pinned Aeneas naming workaround no longer matches: {old}") + types = types.replace(edits[0][1], edits[0][2]).replace(edits[1][1], edits[1][2]) + funs = funs.replace(edits[2][1], edits[2][2]) + return types, funs + + +def share_manifest(workspace, backend): + # Read the upstream lockfile and reuse the dependencies fetched into the + # backend. A separate `lake update` here would clone and cache Mathlib twice. + upstream = json.loads((backend / "lake-manifest.json").read_text()) + packages = [{ + "type": "path", "scope": "", "name": "aeneas", "inherited": False, + "dir": str(backend), "manifestFile": "lake-manifest.json", + "configFile": "lakefile.lean", + }] + for dep in upstream["packages"]: + directory = backend / ".lake/packages" / dep["name"] + if not directory.is_dir(): + raise ValueError(f"Missing pinned Lean dependency: {directory}") + packages.append({ + "type": "path", "scope": dep["scope"], "name": dep["name"], + "inherited": True, "dir": str(directory), + "manifestFile": dep["manifestFile"], "configFile": dep["configFile"], + }) + manifest = { + "version": upstream["version"], "packagesDir": ".lake/packages", + "packages": packages, "name": "zerocopyVerification", "lakeDir": ".lake", + "fixedToolchain": False, + } + (workspace / "lake-manifest.json").write_text(json.dumps(manifest, indent=2) + "\n") + (workspace / "lakefile.lean").write_text( + 'import Lake\nopen Lake DSL\n' + f'require aeneas from {json.dumps(str(backend))}\n' + 'package zerocopyVerification\n' + '@[default_target] lean_lib Zerocopy\n' + '@[default_target] lean_lib Proofs\n' + 'lean_lib Obligations\n' + '@[default_target] lean_lib Required\n' + ) + + +def mathlib_imports(backend): + pattern = re.compile(r"^(?:(?:public|private|protected|meta)\s+)*import\s+(.+)$") + modules = set() + for path in backend.rglob("*.lean"): + if ".lake" in path.relative_to(backend).parts: + continue + for line in path.read_text().splitlines(): + match = pattern.match(line.strip()) + if match: + modules.update(m for m in match[1].split() if m.startswith("Mathlib.")) + if not modules: + raise ValueError("No Mathlib imports found in the pinned Aeneas backend") + return sorted(modules) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("command", choices=["llbc", "prepare", "workspace", "mathlib-imports"]) + parser.add_argument("path", type=Path) + parser.add_argument("--backend", type=Path) + args = parser.parse_args() + if args.command == "llbc": + check_llbc(args.path) + elif args.command == "mathlib-imports": + print("\n".join(mathlib_imports(args.path))) + elif args.command == "prepare": + types = args.path / "Zerocopy/Types.lean" + funs = args.path / "Zerocopy/Funs.lean" + types_text, funs_text = rename_copy_fields(types.read_text(), funs.read_text()) + types.write_text(types_text) + funs.write_text(funs_text) + if args.command in ("prepare", "workspace"): + if args.backend is None: + parser.error(f"{args.command} requires --backend") + share_manifest(args.path, args.backend.resolve()) + + +if __name__ == "__main__": + main() diff --git a/verification/aeneas/run.sh b/verification/aeneas/run.sh new file mode 100755 index 0000000000..8a5dd2a11f --- /dev/null +++ b/verification/aeneas/run.sh @@ -0,0 +1,94 @@ +#!/usr/bin/env bash +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +set -euo pipefail +update_goldens=false +case "${1:-}" in + "") [[ $# == 0 ]] ;; + --update-goldens) [[ $# == 1 ]]; update_goldens=true ;; + *) echo "Usage: $0 [--update-goldens]" >&2; exit 1 ;; +esac +cd "$(dirname "$0")/../.." +repo=$PWD +source verification/aeneas/toolchain.sh +tools_dir=${AENEAS_TOOLCHAIN_DIR:-"$repo/target/aeneas/toolchain"} +backend="$tools_dir/backends/lean" +[[ $("$tools_dir/aeneas" -version) == "aeneas $AENEAS_RELEASE" ]] +[[ $("$tools_dir/charon" toolchain-version) == "$AENEAS_RUST_TOOLCHAIN" ]] +[[ $("$tools_dir/charon" version) == "$CHARON_VERSION ($CHARON_REV)" ]] +[[ $(cat "$backend/lean-toolchain") == "$AENEAS_LEAN_TOOLCHAIN" ]] +export PATH="$tools_dir/lean/bin:$PATH" +export RUSTUP_TOOLCHAIN="$AENEAS_RUST_TOOLCHAIN" + +# Fresh sources AND oleans: a removed declaration cannot survive via a cache. +initialize_workspace() { + rm -rf "$1" + mkdir -p "$1/Zerocopy" + cp verification/aeneas/lean/*.lean "$1/" + cp verification/aeneas/lean/Zerocopy/*.lean "$1/Zerocopy/" + cp "$backend/lean-toolchain" "$1/lean-toolchain" +} +check_proofs() ( + cd "$1" + lake build + # Always run the audit, even if Lake caches its imports. + lake env lean -DwarningAsError=true Check.lean +) +work="$repo/target/aeneas/verification" +golden_work="$repo/target/aeneas/golden-verification" +rendered="$repo/target/aeneas/rendered-golden" +initialize_workspace "$work" +initialize_workspace "$golden_work" +rm -rf "$rendered" + +# Use a Rust parser for body ownership and a lexer for comments/literals. +CARGO_TARGET_DIR="$repo/target/aeneas/annotation-tool" \ + cargo +"$AENEAS_RUST_TOOLCHAIN" build --locked \ + --manifest-path tools/Cargo.toml -p aeneas-inline +inline_tool="$repo/target/aeneas/annotation-tool/debug/aeneas-inline" +inline_cmd=(python3 -B verification/aeneas/inline.py) +inline_args=(--root "$repo" --tool "$inline_tool") +scan=scan +if "$update_goldens"; then scan=scan-update; fi +"${inline_cmd[@]}" "$scan" "${inline_args[@]}" --work "$work" +roots=$(cat "$work/roots.txt") +"${inline_cmd[@]}" assemble "${inline_args[@]}" --work "$work" + +# This compiles the actual zerocopy library with its normal build script and +# default features. Start from these private helpers and their dependencies; +# whole-crate unsafe verification is outside the current Aeneas safe subset. +( + cd zerocopy + CARGO_TARGET_DIR="$repo/target/aeneas/rust" \ + "$tools_dir/charon" cargo --preset=aeneas --sysroot default \ + --start-from "$roots" \ + --dest-file "$work/zerocopy.llbc" --abort-on-error --error-on-warnings \ + -- --lib --locked --offline +) +python3 verification/aeneas/prepare.py llbc "$work/zerocopy.llbc" +"${inline_cmd[@]}" bindings "${inline_args[@]}" --work "$work" +"$tools_dir/aeneas" -backend lean -namespace Zerocopy -dest "$work/Zerocopy" \ + -split-files -abort-on-error -warnings-as-errors -no-progress-bar \ + "$work/zerocopy.llbc" +python3 verification/aeneas/prepare.py prepare "$work" --backend "$backend" +if "$update_goldens"; then + # Update explicitly, and only from a fresh extraction that passes proofs. + echo "Checking live model before updating goldens" + check_proofs "$work" + "${inline_cmd[@]}" update "${inline_args[@]}" --work "$work/Zerocopy" +fi +"${inline_cmd[@]}" render "${inline_args[@]}" --work "$rendered" +python3 verification/aeneas/golden.py compare "$work/Zerocopy" "$rendered" +cp "$rendered/"*.lean "$golden_work/Zerocopy/" +"${inline_cmd[@]}" assemble "${inline_args[@]}" --work "$golden_work" +python3 verification/aeneas/prepare.py workspace "$golden_work" --backend "$backend" +echo "Checking proofs and axioms against the checked-in golden model" +check_proofs "$golden_work" +echo "Checking proofs and axioms against the live Aeneas model" +check_proofs "$work" diff --git a/verification/aeneas/scaffolding/Funs.lean b/verification/aeneas/scaffolding/Funs.lean new file mode 100644 index 0000000000..9a04817e48 --- /dev/null +++ b/verification/aeneas/scaffolding/Funs.lean @@ -0,0 +1,84 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [zerocopy]: function definitions +module +public import Aeneas +public import Zerocopy.Types +public import Zerocopy.FunsExternal +@[expose] public section +open Aeneas Aeneas.Std Result ControlFlow Error +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false + +/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ +set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + +/- You can remove the following line by using the CLI option `-all-computable`: -/ +noncomputable section + +namespace Zerocopy + +/-- Trait implementation: [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 + Name pattern: [core::clone::Clone] -/ +@[reducible, rust_trait_impl + "core::clone::Clone"] +def core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone : + core.clone.Clone core.num.niche_types.NonZeroUsizeInner := { + clone := core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone +} + +/-- Trait implementation: [core::num::niche_types::{impl core::marker::Copy for core::num::niche_types::NonZeroUsizeInner}] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:24-17:28 + Name pattern: [core::marker::Copy] -/ +@[reducible, rust_trait_impl + "core::marker::Copy"] +def core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy : + core.marker.Copy core.num.niche_types.NonZeroUsizeInner := { + cloneInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone +} + +/-- Trait implementation: [core::num::nonzero::{impl core::num::nonzero::ZeroablePrimitive for usize}] + Source: '/rustc/library/core/src/num/nonzero.rs', lines 47:12-47:56 + Name pattern: [core::num::nonzero::ZeroablePrimitive] -/ +@[reducible, rust_trait_impl + "core::num::nonzero::ZeroablePrimitive"] +def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner : + core.num.nonzero.ZeroablePrimitive Std.Usize + core.num.niche_types.NonZeroUsizeInner := { + markerCopyInst := core.marker.CopyUsize + innerCopyInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy +} + +/-- [zerocopy::util::padding_needed_for]: + Source: 'src/util/mod.rs', lines 155:0-243:1 -/ +@@AENEAS_GOLDEN("util.padding_needed_for.lean.in")@@ + +/-- [zerocopy::util::round_down_to_next_multiple_of_alignment]: + Source: 'src/util/mod.rs', lines 264:0-321:1 -/ +@@AENEAS_GOLDEN("util.round_down_to_next_multiple_of_alignment.lean.in")@@ + +/-- [zerocopy::util::max]: + Source: 'src/util/mod.rs', lines 325:0-360:1 -/ +@@AENEAS_GOLDEN("util.max.lean.in")@@ + +/-- [zerocopy::util::min]: + Source: 'src/util/mod.rs', lines 364:0-399:1 -/ +@@AENEAS_GOLDEN("util.min.lean.in")@@ + + +end Zerocopy diff --git a/verification/aeneas/scaffolding/FunsExternal_Template.lean b/verification/aeneas/scaffolding/FunsExternal_Template.lean new file mode 100644 index 0000000000..ccb87a43d6 --- /dev/null +++ b/verification/aeneas/scaffolding/FunsExternal_Template.lean @@ -0,0 +1,52 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [zerocopy]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +module +public import Aeneas +public import Zerocopy.Types +@[expose] public section +open Aeneas Aeneas.Std Result ControlFlow Error +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false + +/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ +set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 +open Zerocopy + +/-- [core::num::niche_types::{impl core::clone::Clone for core::num::niche_types::NonZeroUsizeInner}::clone]: + Source: '/rustc/library/core/src/num/niche_types.rs', lines 17:17-17:22 + Name pattern: [core::num::niche_types::{core::clone::Clone}::clone] + Visibility: public -/ +@[rust_fun + "core::num::niche_types::{core::clone::Clone}::clone"] +axiom core.num.niche_types.NonZeroUsizeInner.Insts.CoreCloneClone.clone + : + core.num.niche_types.NonZeroUsizeInner → Result + core.num.niche_types.NonZeroUsizeInner + +/-- [core::num::nonzero::{core::num::nonzero::NonZero}::get]: + Source: '/rustc/library/core/src/num/nonzero.rs', lines 467:4-467:31 + Name pattern: [core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::get] + Visibility: public -/ +@[rust_fun + "core::num::nonzero::{core::num::nonzero::NonZero<@T, @Clause0_NonZeroInner>}::get"] +axiom core.num.nonzero.NonZero.get + {T : Type} {Clause0_NonZeroInner : Type} (ZeroablePrimitiveInst : + core.num.nonzero.ZeroablePrimitive T Clause0_NonZeroInner) : + core.num.nonzero.NonZero T Clause0_NonZeroInner → Result T + diff --git a/verification/aeneas/scaffolding/Types.lean b/verification/aeneas/scaffolding/Types.lean new file mode 100644 index 0000000000..687cf0b1f8 --- /dev/null +++ b/verification/aeneas/scaffolding/Types.lean @@ -0,0 +1,42 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [zerocopy]: type definitions +module +public import Aeneas +public import Zerocopy.TypesExternal +@[expose] public section +open Aeneas Aeneas.Std Result ControlFlow Error +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false + +/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ +set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + +namespace Zerocopy + +/-- Trait declaration: [core::num::nonzero::ZeroablePrimitive] + Source: '/rustc/library/core/src/num/nonzero.rs', lines 34:0-34:59 + Name pattern: [core::num::nonzero::ZeroablePrimitive] + Visibility: public -/ +@[rust_trait "core::num::nonzero::ZeroablePrimitive" + (parentClauses := ["markerCopyInst", "innerCopyInst"])] +structure core.num.nonzero.ZeroablePrimitive (Self : Type) (Self_NonZeroInner : + Type) where + markerCopyInst : core.marker.Copy Self + innerCopyInst : core.marker.Copy Self_NonZeroInner + +end Zerocopy diff --git a/verification/aeneas/scaffolding/TypesExternal_Template.lean b/verification/aeneas/scaffolding/TypesExternal_Template.lean new file mode 100644 index 0000000000..eb785fcd09 --- /dev/null +++ b/verification/aeneas/scaffolding/TypesExternal_Template.lean @@ -0,0 +1,42 @@ +/- Copyright 2026 The Fuchsia Authors + +Licensed under a BSD-style license , Apache License, Version 2.0 +, or the MIT +license , at your option. +This file may not be copied, modified, or distributed except according to +those terms. -/ + +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [zerocopy]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. +module +public import Aeneas +@[expose] public section +open Aeneas Aeneas.Std Result ControlFlow Error +set_option linter.dupNamespace false +set_option linter.hashCommand false +set_option linter.unusedVariables false +set_option linter.style.whitespace false +set_option linter.style.setOption false +set_option linter.style.longLine false + +/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/ +set_option maxHeartbeats 1000000 + +/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/ +set_option maxRecDepth 2048 + +/-- [core::num::niche_types::NonZeroUsizeInner] + Source: '/rustc/library/core/src/num/niche_types.rs', lines 20:8-20:55 + Name pattern: [core::num::niche_types::NonZeroUsizeInner] + Visibility: public -/ +@[rust_type "core::num::niche_types::NonZeroUsizeInner"] +axiom core.num.niche_types.NonZeroUsizeInner : Type + +/-- [core::num::nonzero::NonZero] + Source: '/rustc/library/core/src/num/nonzero.rs', lines 112:0-112:40 + Name pattern: [core::num::nonzero::NonZero] + Visibility: public -/ +@[rust_type "core::num::nonzero::NonZero"] +axiom core.num.nonzero.NonZero (T : Type) (Clause0_NonZeroInner : Type) : Type + diff --git a/verification/aeneas/setup.sh b/verification/aeneas/setup.sh new file mode 100755 index 0000000000..b5b2530432 --- /dev/null +++ b/verification/aeneas/setup.sh @@ -0,0 +1,66 @@ +#!/usr/bin/env bash +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +set -euo pipefail +cd "$(dirname "$0")/../.." +source verification/aeneas/toolchain.sh +mkdir -p target/aeneas + +# This directory is owned by this script. Publish a complete install only. +staging=$(mktemp -d "$PWD/target/aeneas/setup.XXXXXX") +trap 'rm -rf "$staging"' EXIT + +fetch() { + curl --fail --location --silent --show-error --retry 5 "$1" -o "$2" + python3 - "$2" "$3" <<'PY' +import hashlib +import sys +from pathlib import Path +digest = hashlib.sha256() +with Path(sys.argv[1]).open("rb") as archive: + for block in iter(lambda: archive.read(1024 * 1024), b""): + digest.update(block) +actual = digest.hexdigest() +if actual != sys.argv[2]: + raise SystemExit(f"SHA-256 mismatch for {sys.argv[1]}: {actual}") +PY +} + +fetch "https://github.com/AeneasVerif/aeneas/releases/download/$AENEAS_RELEASE/aeneas-$AENEAS_PLATFORM.tar.gz" \ + "$staging/aeneas.tar.gz" "$AENEAS_SHA256" +mkdir "$staging/toolchain" +tar -xzf "$staging/aeneas.tar.gz" -C "$staging/toolchain" +fetch "https://github.com/leanprover/lean4/releases/download/v$AENEAS_LEAN_VERSION/lean-$AENEAS_LEAN_VERSION-$AENEAS_LEAN_PLATFORM.tar.zst" \ + "$staging/lean.tar.zst" "$AENEAS_LEAN_SHA256" +mkdir "$staging/toolchain/lean" +tar --zstd -xf "$staging/lean.tar.zst" -C "$staging/toolchain/lean" --strip-components=1 + +[[ $("$staging/toolchain/aeneas" -version) == "aeneas $AENEAS_RELEASE" ]] +[[ $("$staging/toolchain/charon" toolchain-version) == "$AENEAS_RUST_TOOLCHAIN" ]] +[[ $("$staging/toolchain/charon" version) == "$CHARON_VERSION ($CHARON_REV)" ]] +[[ $(cat "$staging/toolchain/backends/lean/lean-toolchain") == "$AENEAS_LEAN_TOOLCHAIN" ]] +rustup toolchain install "$AENEAS_RUST_TOOLCHAIN" --profile minimal \ + --component rustc-dev --component rust-src + +# Fetch only Mathlib modules imported by this backend, plus their dependencies. +# The bundle contains a manifest with pinned dependency revisions. Lake loads +# it directly; do not run `lake update` and float the dependencies. +export PATH="$staging/toolchain/lean/bin:$PATH" +python3 verification/aeneas/prepare.py mathlib-imports \ + "$staging/toolchain/backends/lean" > "$staging/mathlib-imports.txt" +mathlib_modules=() +while IFS= read -r module; do + mathlib_modules+=("$module") +done < "$staging/mathlib-imports.txt" +( + cd "$staging/toolchain/backends/lean" + lake exe cache get "${mathlib_modules[@]}" +) +rm -rf target/aeneas/toolchain +mv "$staging/toolchain" target/aeneas/toolchain diff --git a/verification/aeneas/tests/test_golden.py b/verification/aeneas/tests/test_golden.py new file mode 100644 index 0000000000..ae187a143d --- /dev/null +++ b/verification/aeneas/tests/test_golden.py @@ -0,0 +1,90 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +import importlib.util +import tempfile +import unittest +from pathlib import Path + +spec = importlib.util.spec_from_file_location( + "golden", Path(__file__).parents[1] / "golden.py") +golden = importlib.util.module_from_spec(spec) +spec.loader.exec_module(golden) + + +class GoldenTests(unittest.TestCase): + def test_accepts_comments_blank_lines_and_trailing_whitespace(self): + before = 'def min := do\n if x > y\n then ok y\n else ok x\n' + after = ('-- generated source moved\n\n' + '/-- source location /- nested comment -/ -/\n' + 'def min := do \t\n if x > y -- explanation\n\n' + ' then ok y\n else ok x\n') + self.assertEqual(golden.normalize(before), golden.normalize(after)) + self.assertEqual(golden.normalize('x/- short -/y'), + golden.normalize('x/- much longer -/y')) + self.assertNotEqual(golden.normalize('x/- comment -/y'), + golden.normalize('xy')) + + def test_preserves_code_structure_and_literal_contents(self): + before = 'def min := do\n if x > y\n then ok y\n else ok x\n' + for after in [before.replace('>', '<'), before.replace('ok y', 'ok x'), + before.replace(' then', ' then'), + before.replace('if x', 'if x'), + before.replace('then ok y\n else', 'then ok y else')]: + self.assertNotEqual(golden.normalize(before), golden.normalize(after)) + for literal in ['"-- /- spaces -/"', '"a\\\"--b"', "'\"'", + '«-- /- spaces -/»', '"a\n\n \nb"']: + self.assertEqual(golden.normalize('def s := ' + literal), + ['def s := ' + part if i == 0 else part + for i, part in enumerate(literal.split('\n'))]) + self.assertNotEqual(golden.normalize('def s := "a "'), + golden.normalize('def s := "a "')) + self.assertNotEqual(golden.normalize('def s := "a\n\nb"'), + golden.normalize('def s := "a\nb"')) + + def test_rejects_malformed_or_unsupported_literals(self): + for source in ['/- unclosed', '"unclosed', '«unclosed', '"escape\\', + 'r#"raw"#', 's!"interpolated"']: + with self.assertRaises(ValueError): + golden.normalize(source) + + def test_full_file_set_and_template_signatures_are_checked(self): + with tempfile.TemporaryDirectory() as tmp: + live, snapshot = Path(tmp) / 'live', Path(tmp) / 'golden' + live.mkdir() + for name in golden.FILES: + (live / name).write_text('def x := 1\n') + for name in golden.HANDWRITTEN: + (live / name).write_text('def external := 2\n') + golden.update(live, snapshot) + self.assertEqual(golden.compare(live, snapshot), []) + self.assertTrue((snapshot / 'Types.lean').read_text().startswith('/- Copyright')) + original = {name: (snapshot / name).read_bytes() for name in golden.FILES} + (live / 'Funs.lean').write_text('def x := "unclosed\n') + with self.assertRaises(ValueError): + golden.update(live, snapshot) + self.assertEqual(original, + {name: (snapshot / name).read_bytes() for name in golden.FILES}) + (live / 'Funs.lean').write_text('def x := 1\n') + (live / 'TypesExternal_Template.lean').write_text('def x := 2\n') + self.assertTrue(golden.compare(live, snapshot)) + (live / 'Types.lean').unlink() + with self.assertRaises(ValueError): + golden.compare(live, snapshot) + (live / 'Types.lean').write_text('def x := 1\n') + (live / 'New.lean').write_text('def extra := 1\n') + with self.assertRaises(ValueError): + golden.compare(live, snapshot) + (live / 'New.lean').unlink() + (snapshot / 'Unexpected.lean').write_text('def extra := 1\n') + with self.assertRaises(ValueError): + golden.compare(live, snapshot) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py new file mode 100644 index 0000000000..9ca2a1449b --- /dev/null +++ b/verification/aeneas/tests/test_inline.py @@ -0,0 +1,211 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +import json +import copy +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[3] +sys.path.insert(0, str(ROOT / 'verification/aeneas')) +import inline + +TOOL = ROOT / 'target/aeneas/annotation-tool/debug/aeneas-inline' +BLOCK = (' // ```aeneas\n' + ' // model:\n' + ' // def util.f (x : Nat) :=\n' + ' // x\n' + ' // proof:\n' + ' // theorem f_spec : True := by\n' + ' // trivial\n' + ' // ```\n') +ENTRY = {'rust': 'zerocopy::util::f', 'file': 'zerocopy/src/util/mod.rs', + 'syntax': 'f', 'model': 'util.f', 'theorem': 'f_spec', 'golden': 'util.f.lean.in'} + + +def syntax(source): + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / 'source.rs' + path.write_bytes(source.encode()) + result = subprocess.run([str(TOOL)], input=json.dumps([str(path)]), + text=True, capture_output=True) + if result.returncode: + raise ValueError(result.stderr) + return json.loads(result.stdout)[str(path)] + + +class InlineTests(unittest.TestCase): + def parse(self, source): + return inline.parse_file(source, syntax(source)) + + def test_first_token_and_indentation_with_crlf_unicode_and_inactive_cfg(self): + for eol in ('\n', '\r\n'): + source = ('const 雪: u8 = 0;\n#[cfg(any())]\nfn f() {\n\n' + BLOCK + '}').replace('\n', eol) + found = self.parse(source) + self.assertEqual(len(found), 1) + self.assertEqual(found[0]['syntax'], 'f') + self.assertEqual(found[0]['model_text'], 'def util.f (x : Nat) :=\n x\n') + self.assertEqual(found[0]['newline'], eol) + self.assertIn('proof:', source[found[0]['model_end']:]) + + def test_rejects_comments_statements_and_nested_scopes_before_fence(self): + for before in ('// preceding comment\n', '/* preceding */', 'let x = 1;\n', + '#[allow(unused)] let x = 1;\n', '{\n'): + extra_end = '}' if before == '{\n' else '' + with self.subTest(before=before), self.assertRaises(ValueError): + self.parse('fn f() {\n' + before + BLOCK + extra_end + '}') + for source in (BLOCK + 'fn f() {}', + 'fn outer() { fn f() {\n' + BLOCK + '} }', + 'impl S { fn f() {\n' + BLOCK + '} }'): + with self.assertRaises(ValueError): + self.parse(source) + + def test_rejects_near_miss_guards_missing_sections_and_broken_fences(self): + variants = [BLOCK.replace('```aeneas', '```Aeneas'), + BLOCK.replace('```aeneas', '```aeneos'), + BLOCK.replace('```aeneas', '``aeneas'), + BLOCK.replace('```aeneas', '```aeneas v2'), + BLOCK.replace('// ```aeneas', '/// ```aeneas'), + BLOCK.replace('// proof:', '// proofs:'), + BLOCK.replace('// model:', '// proof:'), + BLOCK.replace('// def', '// def'), + BLOCK.replace(' // ```\n', ''), + BLOCK.replace(' // ```\n', ' // ``` trailing\n'), + BLOCK.replace(' // proof:', ' let x = 1;\n // proof:'), + BLOCK.replace(' // proof:', ' // def extra := 1\n // proof:')] + for block in variants: + with self.subTest(block=block), self.assertRaises(ValueError): + self.parse('fn f() {\n' + block + '}') + + def test_fake_fences_in_literals_are_not_annotations(self): + source = 'fn f() { let x = r###"\n' + BLOCK + '"###; }' + self.assertEqual(self.parse(source), []) + with self.assertRaises(ValueError): + self.parse('fn f() { /* ```aeneas\nmodel:\nproof:\n``` */ }') + + def test_discovery_registration_and_golden_bijection(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + source = root / ENTRY['file'] + source.parent.mkdir(parents=True) + source.write_text('fn f() {\n' + BLOCK + '}') + entries = [ENTRY] + self.assertEqual(set(inline.discover(root, TOOL, entries)), {ENTRY['rust']}) + directory = root / 'verification/aeneas/golden' + directory.mkdir(parents=True) + with self.assertRaises(ValueError): + inline.templates(root, entries) + inline.templates(root, entries, allow_missing=True) + golden = directory / ENTRY['golden'] + golden.write_text(f'@@AENEAS_MODEL("{ENTRY["rust"]}")@@\n') + inline.templates(root, entries) + extra = directory / 'orphan.lean.in' + extra.write_text('orphan') + with self.assertRaises(ValueError): + inline.templates(root, entries) + extra.unlink() + golden.write_text('@@AENEAS_MODEL("wrong")@@\n') + with self.assertRaises(ValueError): + inline.templates(root, entries) + source.write_text('fn f() {}') + with self.assertRaises(ValueError): + inline.discover(root, TOOL, entries) + source.write_text(('fn f() {\n' + BLOCK + '}\n') * 2) + with self.assertRaises(ValueError): + inline.discover(root, TOOL, entries) + source.write_text('fn f() {\n' + BLOCK + '}') + outside = root / 'unregistered.rs' + outside.write_text('fn other() {\n' + BLOCK + '}') + with self.assertRaises(ValueError): + inline.discover(root, TOOL, entries) + outside.unlink() + source.write_text('fn wrong() {\n' + BLOCK + '}') + with self.assertRaises(ValueError): + inline.discover(root, TOOL, entries) + + def test_generated_split_and_model_updates_preserve_proof_and_rust(self): + generated = ('module\nnamespace Zerocopy\n' + '/-- [zerocopy::util::f]:\n Source: location -/\n' + 'def util.f (x : Nat) :=\n x + 1\n\nend Zerocopy\n') + models, scaffold = inline.split_live(generated, [ENTRY]) + self.assertEqual(models[ENTRY['rust']], 'def util.f (x : Nat) :=\n x + 1\n') + self.assertIn('@@AENEAS_GOLDEN("util.f.lean.in")@@', scaffold) + for bad in (generated.replace('def util.f', 'def util.other'), + generated.replace('\nend Zerocopy', '\ndef extra := 1\nend Zerocopy'), + generated.replace('[zerocopy::util::f]', '[zerocopy::util::other]')): + with self.assertRaises(ValueError): + inline.split_live(bad, [ENTRY]) + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + source = root / ENTRY['file'] + source.parent.mkdir(parents=True) + original = ('fn f() {\n' + BLOCK + ' let x = 0;\n}').replace('\n', '\r\n') + source.write_bytes(original.encode()) + for folder in ('golden', 'scaffolding', 'live'): + (root / 'verification/aeneas' / folder).mkdir(parents=True) + live = root / 'verification/aeneas/live' + for name in inline.golden.FILES: + (live / name).write_text(generated if name == 'Funs.lean' else 'module\n') + annotations = inline.discover(root, TOOL, [ENTRY]) + inline.update(root, [ENTRY], annotations, live) + result = source.read_bytes().decode() + self.assertIn('// x + 1\r\n', result) + self.assertEqual(original[original.index(' // proof:'):], + result[result.index(' // proof:'):]) + self.assertEqual(original[:original.index(' // def')], + result[:result.index(' // def')]) + annotations = inline.discover(root, TOOL, [ENTRY]) + inline.templates(root, [ENTRY]) + rendered = root / 'rendered' + inline.render(root, annotations, rendered) + self.assertEqual(inline.golden.compare(live, rendered), []) + + def test_llbc_binding_rejects_cfg_alternatives_stale_sources_and_missing_roots(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + path = root / ENTRY['file'] + path.parent.mkdir(parents=True) + source = 'fn f() {\n' + BLOCK + '}\n' + path.write_text(source) + annotations = inline.discover(root, TOOL, [ENTRY]) + annotation = annotations[ENTRY['rust']] + data = {'translated': { + 'files': [{'id': 1, 'name': {'Local': 'src/util/mod.rs'}, 'contents': source}], + 'fun_decls': [{'item_meta': { + 'name': [{'Ident': [part, 0]} for part in ENTRY['rust'].split('::')], + 'started_from': True, 'is_local': True, + 'span': {'Untagged': {'generated_from_span': None, 'data': { + 'file_id': 1, 'beg': {'line': 1, 'col': 0}, + 'end': {'line': annotation['end_line'], 'col': annotation['end_col']}}}} + }}]}} + llbc = root / 'crate.llbc' + llbc.write_text(json.dumps(data)) + inline.check_bindings(root, annotations, llbc) + for kind in ('alternative', 'stale', 'missing', 'duplicate', 'wrong_file'): + bad = copy.deepcopy(data) + translated = bad['translated'] + if kind == 'alternative': + translated['fun_decls'][0]['item_meta']['span']['Untagged']['data']['end']['line'] += 1 + elif kind == 'stale': + translated['files'][0]['contents'] += '// stale\n' + elif kind == 'missing': + translated['fun_decls'] = [] + elif kind == 'duplicate': + translated['fun_decls'] *= 2 + else: + translated['files'][0]['name']['Local'] = 'src/other.rs' + llbc.write_text(json.dumps(bad)) + with self.subTest(kind=kind), self.assertRaises(ValueError): + inline.check_bindings(root, annotations, llbc) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/tests/test_prepare.py b/verification/aeneas/tests/test_prepare.py new file mode 100644 index 0000000000..795dcd072a --- /dev/null +++ b/verification/aeneas/tests/test_prepare.py @@ -0,0 +1,62 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +import importlib.util +import json +import tempfile +import unittest +from pathlib import Path + +spec = importlib.util.spec_from_file_location("prepare", Path(__file__).parents[1] / "prepare.py") +prepare = importlib.util.module_from_spec(spec) +spec.loader.exec_module(prepare) + + +class PrepareTests(unittest.TestCase): + def test_rejects_error_bearing_or_missing_llbc_status(self): + with tempfile.TemporaryDirectory() as tmp: + path = Path(tmp) / "crate.llbc" + for status in [True, None, 0, "false"]: + path.write_text(json.dumps({"has_errors": status, "translated": {}})) + with self.assertRaises(ValueError): + prepare.check_llbc(path) + path.write_text(json.dumps({"has_errors": False, "translated": {}})) + prepare.check_llbc(path) + + def test_renames_only_second_dictionary(self): + types = ('"markerCopyInst", "markerCopyInst"\n' + 'markerCopyInst : core.marker.Copy Self\n' + 'markerCopyInst : core.marker.Copy Self_NonZeroInner\n') + funs = ('markerCopyInst := core.marker.CopyUsize\n' + 'markerCopyInst := core.num.niche_types.NonZeroUsizeInner.Insts.CoreMarkerCopy\n' + 'def util.max := body\n') + new_types, new_funs = prepare.rename_copy_fields(types, funs) + self.assertIn('"markerCopyInst", "innerCopyInst"', new_types) + self.assertIn('markerCopyInst : core.marker.Copy Self\n', new_types) + self.assertIn('innerCopyInst : core.marker.Copy Self_NonZeroInner\n', new_types) + self.assertIn('markerCopyInst := core.marker.CopyUsize\n', new_funs) + self.assertTrue(new_funs.endswith('def util.max := body\n')) + # Upgrades, duplicate matches, and accidental repeated application fail. + for bad_types, bad_funs in [(types + types, funs), (types, ''), (new_types, new_funs)]: + with self.assertRaises(ValueError): + prepare.rename_copy_fields(bad_types, bad_funs) + + def test_imports_include_public_meta_and_exclude_dependency_cache(self): + with tempfile.TemporaryDirectory() as tmp: + backend = Path(tmp) + (backend / 'Aeneas.lean').write_text( + 'public import Mathlib.Data.BitVec\npublic meta import Mathlib.Tactic\n' + 'import Aeneas.Std\n') + (backend / '.lake').mkdir() + (backend / '.lake/Other.lean').write_text('import Mathlib\n') + self.assertEqual(prepare.mathlib_imports(backend), + ['Mathlib.Data.BitVec', 'Mathlib.Tactic']) + + +if __name__ == '__main__': + unittest.main() diff --git a/verification/aeneas/toolchain.sh b/verification/aeneas/toolchain.sh new file mode 100644 index 0000000000..448b13a02c --- /dev/null +++ b/verification/aeneas/toolchain.sh @@ -0,0 +1,32 @@ +# Copyright 2026 The Fuchsia Authors +# +# Licensed under a BSD-style license , Apache License, Version 2.0 +# , or the MIT +# license , at your option. +# This file may not be copied, modified, or distributed except according to +# those terms. + +# Upgrade the bundle as a unit; Charon is selected by Aeneas's charon-pin. +AENEAS_RELEASE=nightly-2026.10.01-ca282ec +AENEAS_REV=ca282ec2312a96f6a985a4d23a663690816d3f3e +CHARON_VERSION=0.1.276 +CHARON_REV=cf02e3f228f97ee7be3a415be56989053063326d +AENEAS_RUST_TOOLCHAIN=nightly-2026-09-17 +AENEAS_LEAN_TOOLCHAIN=leanprover/lean4:v4.31.0 +AENEAS_LEAN_VERSION=4.31.0 + +case "$(uname -s)-$(uname -m)" in + Linux-x86_64) + AENEAS_PLATFORM=linux-x86_64 + AENEAS_SHA256=473df2e5bab0439bfd1a68503ae02c7f88a8de4182e98e4e281590285ab01dee + AENEAS_LEAN_PLATFORM=linux + AENEAS_LEAN_SHA256=07a633cc8d9151cbc08825ea4cdda50d4b02a2c9cb852c0131b13046f49cad7f + ;; + Darwin-arm64) + AENEAS_PLATFORM=macos-aarch64 + AENEAS_SHA256=fac88099e9d687eb321499e43aef1418a4d06f7ae72ecba0b5fd7d38cf013ddd + AENEAS_LEAN_PLATFORM=darwin_aarch64 + AENEAS_LEAN_SHA256=264105500c8abdf37b68ffe03390a783ed259807807222698da8dd92d6ce0a27 + ;; + *) echo "Unsupported Aeneas CI toolchain platform" >&2; return 1 ;; +esac diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index 50454af00c..4850e8caa8 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -153,6 +153,34 @@ pub(crate) fn validate_aligned_to(t: T) -> Result<(), Alignment #[cfg_attr(not(zerocopy_inline_always), inline)] #[cfg_attr(zerocopy_inline_always, inline(always))] pub(crate) const fn padding_needed_for(len: usize, align: NonZeroUsize) -> usize { + // ```aeneas + // model: + // def util.padding_needed_for + // (len : Std.Usize) + // (align : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) : + // Result Std.Usize + // := do + // let i ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + // let mask ← i - 1#usize + // let i1 ← lift (core.num.Usize.wrapping_sub len 1#usize) + // let i2 ← lift (~~~ i1) + // ok (i2 &&& mask) + // proof: + // theorem padding_lt_alignment (len : Usize) (align : NonZeroUsize) + // (h : 0 < align.val.val) : + // util.padding_needed_for len align ⦃ p => p.val < align.val.val ⦄ := by + // unfold util.padding_needed_for + // simp only [core.num.nonzero.NonZero.get, bind_ok] + // step + // simp only [lift, bind_ok, WP.spec_ok, UScalar.val_and] + // have hbound : + // (~~~(core.num.Usize.wrapping_sub len 1#usize)).val &&& mask.val ≤ mask.val := + // Nat.and_le_right + // omega + // ``` #[cfg(kani)] #[kani::proof_for_contract(padding_needed_for)] fn proof() { @@ -237,6 +265,45 @@ pub(crate) const fn round_down_to_next_multiple_of_alignment( n: usize, align: NonZeroUsize, ) -> usize { + // ```aeneas + // model: + // def util.round_down_to_next_multiple_of_alignment + // (n : Std.Usize) + // (align : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) : + // Result Std.Usize + // := do + // let align1 ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner align + // let b ← core.num.Usize.is_power_of_two align1 + // massert b + // let i ← align1 - 1#usize + // let mask ← lift (~~~ i) + // ok (n &&& mask) + // proof: + // theorem round_down_spec (n : Usize) (align : NonZeroUsize) + // (hpos : 0 < align.val.val) (h : align.val.val.isPowerOfTwo) : + // util.round_down_to_next_multiple_of_alignment n align + // ⦃ m => m.val ≤ n.val ∧ m.val % align.val.val = 0 ⦄ := by + // unfold util.round_down_to_next_multiple_of_alignment + // simp only [core.num.nonzero.NonZero.get, bind_ok] + // step + // step + // step with UScalar.sub_bv_spec as ⟨mask, hval, hle, hbv⟩ + // simp only [lift, bind_ok, WP.spec_ok] + // constructor + // · simp only [UScalar.val_and] + // exact Nat.and_le_left + // · have clear : (n &&& ~~~mask).val &&& mask.val = 0 := by + // rw [← UScalar.val_and] + // change ((n.bv &&& ~~~mask.bv) &&& mask.bv).toNat = 0 + // simp [BitVec.and_assoc] + // unfold Nat.isPowerOfTwo at h + // rcases h with ⟨k, hk⟩ + // rw [hval, hk, Nat.and_two_pow_sub_one_eq_mod] at clear + // simpa only [hk] using clear + // ``` #[cfg(kani)] #[kani::proof_for_contract(round_down_to_next_multiple_of_alignment)] fn proof() { @@ -256,6 +323,35 @@ pub(crate) const fn round_down_to_next_multiple_of_alignment( #[cfg_attr(not(zerocopy_inline_always), inline)] #[cfg_attr(zerocopy_inline_always, inline(always))] pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { + // ```aeneas + // model: + // def util.max + // (a : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) + // (b : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) : + // Result (core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) + // := do + // let i ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a + // let i1 ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b + // if i < i1 + // then ok b + // else ok a + // proof: + // theorem max_spec (a b : NonZeroUsize) : + // ∃ r, util.max a b = .ok r ∧ r.val.val = Nat.max a.val.val b.val.val := by + // simp only [util.max, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + // split + // · rename_i h + // exact ⟨b, rfl, (Nat.max_eq_right (by omega)).symm⟩ + // · rename_i h + // exact ⟨a, rfl, (Nat.max_eq_left (by omega)).symm⟩ + // ``` if a.get() < b.get() { b } else { @@ -266,6 +362,35 @@ pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { #[cfg_attr(not(zerocopy_inline_always), inline)] #[cfg_attr(zerocopy_inline_always, inline(always))] pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { + // ```aeneas + // model: + // def util.min + // (a : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) + // (b : core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) : + // Result (core.num.nonzero.NonZero Std.Usize + // core.num.niche_types.NonZeroUsizeInner) + // := do + // let i ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner a + // let i1 ← + // core.num.nonzero.NonZero.get + // Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner b + // if i > i1 + // then ok b + // else ok a + // proof: + // theorem min_spec (a b : NonZeroUsize) : + // ∃ r, util.min a b = .ok r ∧ r.val.val = Nat.min a.val.val b.val.val := by + // simp only [util.min, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + // split + // · rename_i h + // exact ⟨b, rfl, (Nat.min_eq_right (by omega)).symm⟩ + // · rename_i h + // exact ⟨a, rfl, (Nat.min_eq_left (by omega)).symm⟩ + // ``` if a.get() > b.get() { b } else {