From fbc3eb312fd8263c965deb11d9d33f8f84cafbdf Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 1 Oct 2026 18:43:13 -0400 Subject: [PATCH 1/4] Add inline Aeneas verification, checked in CI gherrit-pr-id: Gf75ukj4vvtufg6dwjpfa3bx5a457sw74 --- .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 { From 83ba7cdc48d6a8576db6af9716be8671c7ae1c1c Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 09:40:40 -0400 Subject: [PATCH 2/4] Introduce inline Aeneas contracts with unchanged proof requirements Add a contract command for total Aeneas specifications and an explicit partial variant. Migrate the four existing inline proofs without changing their preconditions or postconditions: padding and round-down retain their original proof bodies, and min/max reuse their existential proofs through a WP adapter. Check macro quantifiers, tuple binders, panic, and divergence against independent propositions. Recognize contract declarations in inline tooling and retain the independent required-type checks against both golden and live models. Validation: fresh extraction and both Lean model builds and axiom audits, 15 Python tests, two Rust parser tests, 16 negative controls, and repository pre-push checks passed. gherrit-pr-id: Gmasez6fvx2c6chogoybuzpgyoykiaupc Agent-authored-by: AI agent acting on joshlf's behalf --- verification/aeneas/README.md | 60 ++++++++++- verification/aeneas/inline.py | 10 +- verification/aeneas/lean/Check.lean | 6 +- verification/aeneas/lean/ContractTests.lean | 72 +++++++++++++ verification/aeneas/lean/Contracts.lean | 64 ++++++++++++ verification/aeneas/lean/Proofs.lean.in | 1 + verification/aeneas/negative-controls.sh | 55 +++++++++- verification/aeneas/prepare.py | 2 + verification/aeneas/run.sh | 3 + verification/aeneas/tests/test_inline.py | 20 ++++ zerocopy/src/util/mod.rs | 106 +++++++++++--------- 11 files changed, 341 insertions(+), 58 deletions(-) create mode 100644 verification/aeneas/lean/ContractTests.lean create mode 100644 verification/aeneas/lean/Contracts.lean diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index 9d0c126579..cf00a83f97 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -30,7 +30,8 @@ including their dependencies; there is no copied Rust implementation: 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. +conditional on success. The min/max proofs explicitly exhibit the result before +converting it to the same total specification. 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 @@ -96,8 +97,12 @@ fn example() { // model: // def util.example ... := ... // proof: - // theorem example_spec ... := by - // ... + // contract example_spec ... + // for example ... + // requires h : ... + // ensures r => ... + // proof: + // ... // ``` ... } @@ -110,6 +115,49 @@ 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. +The proof declaration may be an ordinary `theorem` or the experimental +`contract` command from `lean/Contracts.lean`. For example, one of the macro tests +uses this syntax: + +```lean +contract identity_spec (x : Nat) + for Result.ok x + ensures ret => ret = x + proof: + exact WP.spec.ret rfl +``` + +The command expands to an ordinary theorem whose named requirements are +proposition-valued parameters and whose conclusion is Aeneas's `WP.spec`. +Under those requirements, the function must return successfully and satisfy +the postcondition. Panic and divergence both fail the contract, even when the +postcondition is `True`. Requirements are optional; omitting them adds no +preconditions. Multiple requirements all apply, in their written order. +Output binders reuse Aeneas's notation, including tuple patterns and multiple +binders for return values and mutable post-states. Argument binders and the +function application remain explicit; this prototype does not infer Rust +signatures, inject type invariants, or introduce separate proof automation. + +An explicit `partial contract` instead expands to `WP.dspec`. It permits +divergence, rejects panic and other failures, and requires the postcondition +for successful returns. All registered contracts use the total form. +`Obligations.lean` retains their independently written required propositions. + +Both workspaces build `ContractTests.lean`, which checks independently written +theorem types, named requirements, omitted requirements, tuple outputs, and +partial contracts. The axiom audit covers these tests and the contract module. +Failure controls also compile contracts that attempt to accept panic, +divergence in the total form, or an incorrect return in the partial form, and +require proof failures. This is a test-bed syntax experiment, not a commitment +to Anneal's eventual annotation language. + +The four inline proofs use this syntax without changing their previous +preconditions or postconditions. Padding still requires only a positive +alignment; round-down retains both positivity and the power-of-two requirement. +The old explicit min/max result proofs are reused through +`WP.exists_imp_spec`; required-type checks use the converse equivalence to +compare them with the independently written successful-result requirements. + `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 @@ -238,12 +286,14 @@ records but does not formally prove: `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`, +`Zerocopy.util` namespace, the external `core.num` models, and the contract macro +and test namespaces. 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 +CI also runs failure controls in both workspaces: impossible total and partial +contracts must fail their proofs, 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 diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index 478f82a1cb..a20212690c 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -172,7 +172,8 @@ def discover(root, tool, entries): 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): + declarations = 'def' if keyword == 'def' else '(?:theorem|contract|partial contract)' + if not re.match(rf'{declarations} {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() @@ -229,7 +230,12 @@ def assemble(root, annotations, work): (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"]}') + # Total contracts and explicit successful-result requirements are equivalent. + name = a['theorem'] + required.append(f'example : Zerocopy.Obligations.{name} := by\n' + f' simpa only [Zerocopy.Obligations.{name}, ' + 'Aeneas.Std.WP.spec_equiv_exists] ' + f'using Zerocopy.Proofs.{name}') 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') diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index a7932e152c..076926785a 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -7,6 +7,7 @@ This file may not be copied, modified, or distributed except according to those terms. -/ import Required +import ContractTests open Lean Elab Command run_elab do let required := requiredTheorems @@ -15,10 +16,11 @@ run_elab 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 prefixes := #[`Zerocopy.Proofs, `Zerocopy.Obligations, `Zerocopy.util, `core.num, + `AeneasContracts, `ContractTests] let mut audited := 0 for (declName, _) in env.constants.toList do - if prefixes.any (·.isPrefixOf declName) then + if prefixes.any (·.isPrefixOf (privateToUserName declName)) then let used ← collectAxioms declName for ax in used do unless #[`propext, `Classical.choice, `Quot.sound].contains ax do diff --git a/verification/aeneas/lean/ContractTests.lean b/verification/aeneas/lean/ContractTests.lean new file mode 100644 index 0000000000..fbdf1610af --- /dev/null +++ b/verification/aeneas/lean/ContractTests.lean @@ -0,0 +1,72 @@ +/- 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 Contracts +@[expose] public section +open Aeneas Aeneas.Std +namespace ContractTests + +-- Omitted requirements mean True; a successful result is still required. +contract identity_spec (x : Nat) + for Result.ok x + ensures ret => ret = x + proof: + exact WP.spec.ret rfl + +-- Named requirements are available without introductions in the proof body. +contract transitive_spec (x y z : Nat) + for Result.ok x + requires hxy : x = y + requires hyz : y = z + ensures ret => ret = z + proof: + exact WP.spec.ret (hxy.trans hyz) + +-- Reuse Aeneas's tuple-aware binders for returns and mutable post-states. +contract tuple_spec (x : Nat) + for Result.ok (x, x + 1) + ensures ret x' => ret = x ∧ x' = x + 1 + proof: + simp + +partial contract diverging_spec + for (Result.div : Result Nat) + ensures _ => False + proof: + exact WP.dspec.div _ + +partial contract partial_identity_spec (x : Nat) + for Result.ok x + ensures ret => ret = x + proof: + exact WP.dspec.ret rfl + +-- These independently written types pin the macro's quantifiers and outcomes. +example : ∀ x : Nat, WP.spec (Result.ok x) (fun ret => ret = x) := identity_spec +example : ∀ x y z : Nat, x = y → y = z → + WP.spec (Result.ok x) (fun ret => ret = z) := transitive_spec +example : ∀ x : Nat, WP.spec (Result.ok (x, x + 1)) + (fun (ret, x') => ret = x ∧ x' = x + 1) := tuple_spec +example : WP.dspec (Result.div : Result Nat) (fun _ => False) := diverging_spec +example : ∀ x : Nat, WP.dspec (Result.ok x) (fun ret => ret = x) := partial_identity_spec + +theorem panic_rejected : + ¬ WP.spec (Result.fail Error.panic : Result Nat) (fun _ => True) := by simp + +theorem divergence_rejected : + ¬ WP.spec (Result.div : Result Nat) (fun _ => True) := by simp + +-- Partial correctness must reject panic and incorrect successful returns too. +theorem partial_panic_rejected : + ¬ WP.dspec (Result.fail Error.panic : Result Nat) (fun _ => True) := by simp + +theorem partial_wrong_return_rejected : + ¬ WP.dspec (Result.ok 0) (fun ret : Nat => ret = 1) := by simp + +end ContractTests diff --git a/verification/aeneas/lean/Contracts.lean b/verification/aeneas/lean/Contracts.lean new file mode 100644 index 0000000000..0c958635ae --- /dev/null +++ b/verification/aeneas/lean/Contracts.lean @@ -0,0 +1,64 @@ +/- 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 +public meta import Lean +public section + +open Lean Aeneas Aeneas.Std + +namespace AeneasContracts + +declare_syntax_cat contractRequirement +syntax "requires " ident " : " term : contractRequirement + +/-- A total contract establishes successful termination and its postcondition. +Each named requirement becomes a proposition-valued theorem parameter. +Output binders use Aeneas's existing tuple-aware specification notation. -/ +syntax "contract " ident bracketedBinder* " for " term + contractRequirement* " ensures " term+ " => " term + " proof:" tacticSeq : command + +/-- A partial contract permits divergence, but still excludes failure. +Successful results must satisfy the postcondition. -/ +syntax "partial " "contract " ident bracketedBinder* " for " term + contractRequirement* " ensures " term+ " => " term + " proof:" tacticSeq : command + +private meta def requirementBinders (requirements : Array Syntax) : + MacroM (Array (TSyntax ``Lean.Parser.Term.bracketedBinder)) := + requirements.mapM fun requirement => do + match requirement with + | `(contractRequirement| requires $id:ident : $pre:term) => + `(bracketedBinder| ($id : ($pre : Prop))) + | _ => Macro.throwUnsupported + +macro_rules + | `(contract $id:ident $args:bracketedBinder* for $call:term + $requirements:contractRequirement* ensures $x => $post:term + proof: $body:tacticSeq) => do + let premises ← requirementBinders requirements + `(theorem $id $args* $premises* : $call ⦃ $x => $post ⦄ := by $body) + | `(contract $id:ident $args:bracketedBinder* for $call:term + $requirements:contractRequirement* ensures $x $xs:term* => $post:term + proof: $body:tacticSeq) => do + let premises ← requirementBinders requirements + `(theorem $id $args* $premises* : $call ⦃ $x $xs* => $post ⦄ := by $body) + | `(partial contract $id:ident $args:bracketedBinder* for $call:term + $requirements:contractRequirement* ensures $x => $post:term + proof: $body:tacticSeq) => do + let premises ← requirementBinders requirements + `(theorem $id $args* $premises* : $call ⦃ $x => $post ⦄div := by $body) + | `(partial contract $id:ident $args:bracketedBinder* for $call:term + $requirements:contractRequirement* ensures $x $xs:term* => $post:term + proof: $body:tacticSeq) => do + let premises ← requirementBinders requirements + `(theorem $id $args* $premises* : $call ⦃ $x $xs* => $post ⦄div := by $body) + +end AeneasContracts diff --git a/verification/aeneas/lean/Proofs.lean.in b/verification/aeneas/lean/Proofs.lean.in index 4814022daf..06e0a01d06 100644 --- a/verification/aeneas/lean/Proofs.lean.in +++ b/verification/aeneas/lean/Proofs.lean.in @@ -8,6 +8,7 @@ those terms. -/ module public import Zerocopy.Funs +public import Contracts import all Init.Data.Nat.Power2.Basic @[expose] public section open Aeneas Aeneas.Std diff --git a/verification/aeneas/negative-controls.sh b/verification/aeneas/negative-controls.sh index 4c941a4551..b9cfcefd29 100755 --- a/verification/aeneas/negative-controls.sh +++ b/verification/aeneas/negative-controls.sh @@ -37,6 +37,59 @@ if [[ $1 == verification ]]; then echo "Confirmed: comment drift passes comparison and live proofs" fi +# Exercise the actual command expansion, not just its underlying WP predicates. +reject_contract() { + local description=$1 + cat >> Proofs.lean + if lake build Required > "$backup/contract-build.log" 2>&1; then + echo "Contract syntax accepted $description" >&2; exit 1 + fi + if ! grep -Eq '(error: Proofs[.]lean:|Proofs[.]lean:.*error)' "$backup/contract-build.log" || + ! grep -q 'unsolved goals' "$backup/contract-build.log" || + ! grep -q '⊢ False' "$backup/contract-build.log"; then + cat "$backup/contract-build.log" >&2; exit 1 + fi + echo "Confirmed: contract syntax rejects $description" + cp "$backup/Proofs.lean" Proofs.lean +} +reject_contract "panic under a total contract" <<'LEAN' +namespace Zerocopy.Proofs +contract panic_control + for (Result.fail Error.panic : Result Nat) + requires h : True + ensures _ => True + proof: + simp +end Zerocopy.Proofs +LEAN +reject_contract "divergence under a total contract" <<'LEAN' +namespace Zerocopy.Proofs +contract divergence_control + for (Result.div : Result Nat) + ensures _ => True + proof: + simp +end Zerocopy.Proofs +LEAN +reject_contract "panic under a partial contract" <<'LEAN' +namespace Zerocopy.Proofs +partial contract partial_panic_control + for (Result.fail Error.panic : Result Nat) + ensures _ => True + proof: + simp +end Zerocopy.Proofs +LEAN +reject_contract "an incorrect successful return under a partial contract" <<'LEAN' +namespace Zerocopy.Proofs +partial contract partial_return_control + for Result.ok (0 : Nat) + ensures ret => ret = 1 + proof: + simp +end Zerocopy.Proofs +LEAN + cat >> Proofs.lean <<'LEAN' namespace Zerocopy.Proofs theorem negative_control : True := by sorry @@ -62,7 +115,7 @@ 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)', +s, count = re.subn(r'contract min_spec\b.*?(?=\n(?:theorem|contract|partial contract) |\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") diff --git a/verification/aeneas/prepare.py b/verification/aeneas/prepare.py index 93a28e97c9..c59c60babc 100644 --- a/verification/aeneas/prepare.py +++ b/verification/aeneas/prepare.py @@ -74,6 +74,8 @@ def share_manifest(workspace, backend): f'require aeneas from {json.dumps(str(backend))}\n' 'package zerocopyVerification\n' '@[default_target] lean_lib Zerocopy\n' + 'lean_lib Contracts\n' + '@[default_target] lean_lib ContractTests\n' '@[default_target] lean_lib Proofs\n' 'lean_lib Obligations\n' '@[default_target] lean_lib Required\n' diff --git a/verification/aeneas/run.sh b/verification/aeneas/run.sh index 8a5dd2a11f..cc9564b4a2 100755 --- a/verification/aeneas/run.sh +++ b/verification/aeneas/run.sh @@ -37,6 +37,9 @@ initialize_workspace() { check_proofs() ( cd "$1" lake build + for source in Proofs.lean ContractTests.lean; do + lake env lean -DwarningAsError=true "$source" + done # Always run the audit, even if Lake caches its imports. lake env lean -DwarningAsError=true Check.lean ) diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index 9ca2a1449b..a909e624d6 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -131,6 +131,26 @@ def test_discovery_registration_and_golden_bijection(self): with self.assertRaises(ValueError): inline.discover(root, TOOL, entries) + def test_contract_declarations_are_registered_and_preserved(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + source = root / ENTRY['file'] + source.parent.mkdir(parents=True) + for keyword in ('contract', 'partial contract'): + block = BLOCK.replace('theorem f_spec : True := by\n' + ' // trivial', + keyword + ' f_spec (x : Nat)\n' + ' // for Result.ok x\n' + ' // ensures ret => ret = x\n' + ' // proof:\n' + ' // rfl') + source.write_text('fn f() {\n' + block + '}') + annotation = inline.discover(root, TOOL, [ENTRY])[ENTRY['rust']] + self.assertTrue(annotation['proof_text'].startswith(keyword + ' f_spec ')) + source.write_text('fn f() {\n' + block.replace('f_spec ', 'wrong_spec ') + '}') + with self.assertRaisesRegex(ValueError, 'unexpected theorem declaration'): + inline.discover(root, TOOL, [ENTRY]) + def test_generated_split_and_model_updates_preserve_proof_and_rust(self): generated = ('module\nnamespace Zerocopy\n' '/-- [zerocopy::util::f]:\n Source: location -/\n' diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index 4850e8caa8..88a9705ade 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -169,17 +169,19 @@ pub(crate) const fn padding_needed_for(len: usize, align: NonZeroUsize) -> 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 + // contract padding_lt_alignment (len : Usize) (align : NonZeroUsize) + // for util.padding_needed_for len align + // requires h : 0 < align.val.val + // ensures p => p.val < align.val.val + // proof: + // 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)] @@ -282,27 +284,29 @@ pub(crate) const fn round_down_to_next_multiple_of_alignment( // 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 + // contract round_down_spec (n : Usize) (align : NonZeroUsize) + // for util.round_down_to_next_multiple_of_alignment n align + // requires hpos : 0 < align.val.val + // requires h : align.val.val.isPowerOfTwo + // ensures m => m.val ≤ n.val ∧ m.val % align.val.val = 0 + // proof: + // 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)] @@ -343,14 +347,17 @@ pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { // 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⟩ + // contract max_spec (a b : NonZeroUsize) + // for util.max a b + // ensures r => r.val.val = Nat.max a.val.val b.val.val + // proof: + // apply WP.exists_imp_spec + // 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 @@ -382,14 +389,17 @@ pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { // 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⟩ + // contract min_spec (a b : NonZeroUsize) + // for util.min a b + // ensures r => r.val.val = Nat.min a.val.val b.val.val + // proof: + // apply WP.exists_imp_spec + // 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 From fec742aa31827b9fa4477d7b1f5ee0a07d7082c7 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Thu, 1 Oct 2026 22:49:50 -0400 Subject: [PATCH 3/4] Strengthen arithmetic contracts and compose layout padding proofs Specify exact padding and round-down results, their extremal properties, and min/max membership and bounds. Factor the arithmetic into reusable lemmas and prove that layout padding preserves alignment and the shallow-padding flag. Support inline proofs on inherent methods, order caller proofs by declared callee dependencies, and audit those dependencies after elaboration. Keep independent required propositions and add mutation controls for the stronger claims against both golden and freshly extracted models. Validation: golden/live Lean checks, negative controls, inline tooling tests, and repository pre-push checks passed. gherrit-pr-id: Gxi6wprpgshggdrhvt64jphmjwhociog5 Agent-authored-by: AI agent acting on joshlf's behalf --- tools/aeneas-inline/src/main.rs | 74 +++++-- verification/aeneas/README.md | 172 +++++++++++----- .../layout.DstLayout.pad_to_align.lean.in | 9 + verification/aeneas/inline.py | 152 +++++++++++++-- verification/aeneas/inventory.json | 11 ++ verification/aeneas/lean/Arithmetic.lean | 168 ++++++++++++++++ verification/aeneas/lean/Check.lean | 37 +++- verification/aeneas/lean/Corollaries.lean | 160 +++++++++++++++ verification/aeneas/lean/Obligations.lean | 49 ++++- verification/aeneas/lean/Proofs.lean.in | 1 + verification/aeneas/negative-controls.sh | 184 ++++++++++++++++++ verification/aeneas/prepare.py | 2 + verification/aeneas/run.sh | 2 +- verification/aeneas/scaffolding/Funs.lean | 5 + verification/aeneas/scaffolding/Types.lean | 22 +++ verification/aeneas/tests/test_inline.py | 109 ++++++++++- zerocopy/src/layout.rs | 79 ++++++++ zerocopy/src/util/mod.rs | 76 +++++--- 18 files changed, 1193 insertions(+), 119 deletions(-) create mode 100644 verification/aeneas/golden/layout.DstLayout.pad_to_align.lean.in create mode 100644 verification/aeneas/lean/Arithmetic.lean create mode 100644 verification/aeneas/lean/Corollaries.lean diff --git a/tools/aeneas-inline/src/main.rs b/tools/aeneas-inline/src/main.rs index be464e732d..b74639215d 100644 --- a/tools/aeneas-inline/src/main.rs +++ b/tools/aeneas-inline/src/main.rs @@ -31,6 +31,18 @@ impl Functions<'_> { .nth(pos.column) .map_or(self.source[start..].len(), |(byte, _)| byte) } + + fn function(&mut self, ident: &syn::Ident, block: &syn::Block) { + let open = self.offset(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(ident.to_string()); + self.functions.push(json!({ + "path": path.join("::"), "open": open, + "close": self.offset(block.brace_token.span.close().end()), + "supported": self.unsupported == 0, + })); + } } impl<'ast> Visit<'ast> for Functions<'_> { @@ -41,26 +53,41 @@ impl<'ast> Visit<'ast> for Functions<'_> { } 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.function(&item.sig.ident, &item.block); + // Never attribute nested functions to the enclosing function or method. self.unsupported += 1; visit::visit_item_fn(self, item); self.unsupported -= 1; } fn visit_item_impl(&mut self, item: &'ast syn::ItemImpl) { + // Support simple, nongeneric inherent impls in their type's module. + // Qualified Self types, trait impls and generics need explicit identity + // resolution; annotations there must continue to fail closed. + let ident = match item.self_ty.as_ref() { + syn::Type::Path(path) if path.qself.is_none() => path.path.get_ident(), + _ => None, + }; + if let Some(ident) = ident.filter(|_| { + item.trait_.is_none() && item.generics.params.is_empty() && self.unsupported == 0 + }) { + self.modules.push(ident.to_string()); + visit::visit_item_impl(self, item); + self.modules.pop(); + } else { + self.unsupported += 1; + visit::visit_item_impl(self, item); + self.unsupported -= 1; + } + } + + fn visit_impl_item_fn(&mut self, item: &'ast syn::ImplItemFn) { + let generic = !item.sig.generics.params.is_empty(); + self.unsupported += usize::from(generic); + self.function(&item.sig.ident, &item.block); self.unsupported += 1; - visit::visit_item_impl(self, item); - self.unsupported -= 1; + visit::visit_impl_item_fn(self, item); + self.unsupported -= 1 + usize::from(generic); } fn visit_item_trait(&mut self, item: &'ast syn::ItemTrait) { @@ -125,4 +152,25 @@ mod tests { let open = functions[0]["open"].as_u64().unwrap() as usize; assert!(source[open..].starts_with("{ fn inner()")); } + + #[test] + fn resolves_simple_inherent_methods_and_rejects_other_impl_forms() { + for (implementation, supported) in [ + ("impl S", true), + ("impl S", false), + ("impl Trait for S", false), + ("impl m::S", false), + ] { + let source = + format!("mod m {{ {implementation} {{ fn f() {{ fn nested() {{}} }} }} }}"); + let value = inspect(&source).unwrap(); + assert_eq!(value["functions"][0]["supported"], supported); + assert_eq!(value["functions"][1]["supported"], false); + if supported { + assert_eq!(value["functions"][0]["path"], "m::S::f"); + } + } + let value = inspect("impl S { fn f() {} }").unwrap(); + assert_eq!(value["functions"][0]["supported"], false); + } } diff --git a/verification/aeneas/README.md b/verification/aeneas/README.md index cf00a83f97..c4c5247f43 100644 --- a/verification/aeneas/README.md +++ b/verification/aeneas/README.md @@ -17,27 +17,44 @@ 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: +Extraction starts from these actual helpers in `zerocopy/src/util/mod.rs` and +the method in `zerocopy/src/layout.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. | +| `max` | Returns the mathematical maximum, selects an input, and bounds both inputs from above. | +| `min` | Returns the mathematical minimum, selects an input, and bounds both inputs from below. | +| `padding_needed_for` | For power-of-two alignment, returns padding below it and exactly `(align - len % align) % align`, the least padding making the sum aligned, with zero padding exactly when the input is aligned. | +| `round_down_to_next_multiple_of_alignment` | For power-of-two alignment, returns exactly `n - n % align`, the greatest aligned value at most `n`; the next multiple exceeds `n`. | +| `DstLayout::pad_to_align` | For sized layouts, power-of-two alignment and an exact padded size that fits guarantee the least aligned size at least the input; alignment is preserved and the shallow-unpadded flag becomes its old value AND the input being aligned. All DST layouts return unchanged, with no arithmetic preconditions. | 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 before -converting it to the same total specification. +these are not finite collections of test inputs. All five inline specifications +use `contract`, whose Aeneas Hoare specification includes successful termination, +rather than only a postcondition conditional on success. + +`lean/Corollaries.lean` composes the inline theorems: min/max preserve any +predicate shared by both inputs; round-down is monotone, is the identity on +aligned inputs, and is idempotent; layout padding is the identity on aligned +sized layouts and DSTs, and is idempotent. The idempotence contracts prove both +calls succeed, including that the first result meets the second call's needs. +The original `size + align - 1 <= usize::MAX` precondition is also checked as a +sufficient condition for the layout contract's exact fit requirement. + +Comparisons use the unsigned scalar's existing order directly (`m ≤ n`, +`p < align.val`, `min a.val b.val`). Arithmetic postconditions explicitly bind +`Nat` values (`let N : Nat := n`) so addition and remainder are unbounded +mathematical operations. The corresponding Rust scalar arithmetic operators +return checked `Result` values and are not interchangeable with these formulas. +`NonZero` still needs one `.val` to unwrap its stored scalar. Power-of-two +requirements already imply positivity, so padding, round-down, and sized-layout +contracts do not repeat a positive-alignment requirement. 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 +scope does not prove 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 @@ -116,15 +133,20 @@ doc comments, block comments, missing fences, extra sections, and extra top-level Lean declarations are rejected. The proof declaration may be an ordinary `theorem` or the experimental -`contract` command from `lean/Contracts.lean`. For example, one of the macro tests -uses this syntax: +`contract` command from `lean/Contracts.lean`. For example, a predicate-preserving +corollary uses this syntax: ```lean -contract identity_spec (x : Nat) - for Result.ok x - ensures ret => ret = x +contract max_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop) + for util.max a b + requires ha : P a + requires hb : P b + ensures r => P r proof: - exact WP.spec.ret rfl + step with max_spec a b as ⟨r, _, hchoice, _, _⟩ + rcases hchoice with h | h + · simpa only [h] using ha + · simpa only [h] using hb ``` The command expands to an ordinary theorem whose named requirements are @@ -141,7 +163,8 @@ signatures, inject type invariants, or introduce separate proof automation. An explicit `partial contract` instead expands to `WP.dspec`. It permits divergence, rejects panic and other failures, and requires the postcondition for successful returns. All registered contracts use the total form. -`Obligations.lean` retains their independently written required propositions. +`Obligations.lean` retains their independently written required propositions, +and the layout caller still applies the same padding theorem through `step`. Both workspaces build `ContractTests.lean`, which checks independently written theorem types, named requirements, omitted requirements, tuple outputs, and @@ -151,13 +174,6 @@ divergence in the total form, or an incorrect return in the partial form, and require proof failures. This is a test-bed syntax experiment, not a commitment to Anneal's eventual annotation language. -The four inline proofs use this syntax without changing their previous -preconditions or postconditions. Padding still requires only a positive -alignment; round-down retains both positivity and the power-of-two requirement. -The old explicit min/max result proofs are reused through -`WP.exists_imp_spec`; required-type checks use the converse equivalence to -compare them with the independently written successful-result requirements. - `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 @@ -169,13 +185,18 @@ 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. +Support covers free functions and nongeneric methods in simple nongeneric +inherent impls, in conventional `zerocopy/src` module paths. An inherent impl's +named Self type must be defined in the same module. Trait impls, qualified Self +types, generic impls/methods, nested functions, macros, and custom module-path +layouts need explicit tooling support; an unsupported annotation 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. +For inherent methods, the binding check resolves Charon's named Self type, +including its deduplicated representation, and checks the full type identity; +a matching method name alone is insufficient. Each annotation has exactly one function template in `golden/`, and every file there must correspond to one registered annotation. That file contains one @@ -187,15 +208,61 @@ 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 +The five registered proof bodies live in the Rust annotations; shared arithmetic +lemmas and composition corollaries live in Lean modules. `lean/Proofs.lean.in` +supplies the inline proofs' 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. +theorem against its required proposition, using Aeneas's proved +`WP.spec_equiv_exists` equivalence to normalize total specifications and +existential successful-result statements, and proved scalar order/minimum/maximum +equivalences to normalize scalar comparisons to mathematical values. The min/max +obligations retain their independent existential shape and now also require input +selection and bounds. The layout obligation is checked separately in both +branches because its independently generated matchers have different names. 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. +## Composing proofs + +An inventory entry may declare `depends_on`, a list of registered Rust function +identities whose exported theorems its proof uses. Omission means an empty list. +These are proof dependencies, not the Rust call graph: a mathematical lemma may +be useful even when its function is not called. Unknown or repeated identities, +self dependencies, and cycles fail before extraction. Proof assembly uses a +deterministic topological order, independent of source or inventory order. + +`DstLayout::pad_to_align` declares a dependency on `padding_needed_for`. Its +inline proof unfolds only the caller, applies `padding_lt_alignment` to the +padding call, then uses the checked-add specification and arithmetic to rule +out overflow and establish the result. It does not unfold the callee. + +For sized layouts, the theorem requires power-of-two alignment and that the +exact padded size `S + (A - S % A) % A` fits in `usize`, where `S` is the input +size and `A` its alignment. It proves that the result remains sized, with that +exact size: the least multiple of `A` at least `S`, and less than `S + A`. The +alignment field is preserved, and `statically_shallow_unpadded` becomes its +original value AND `S % A == 0`. For DST layouts, the entire layout is +unchanged, including the trailing-slice offset, element size, alignment, and +shallow-unpadded flag, with no arithmetic preconditions. The conservative +`S + A - 1 <= usize::MAX` headroom condition remains available as a sufficient +condition through `pad_to_align_sized_headroom` in `Corollaries.lean`. + +Generated `Required.lean` records the declared theorem edges. `Check.lean` +inspects elaborated theorem types and proof terms, following local helper +declarations and stopping at other registered theorems. Every referenced +registered theorem must be declared, and every declared dependency must appear +in the elaborated proof. This catches both accidental dependencies on an +earlier declaration and stale dependency lists. Each callee's own edges and +transitive axiom dependencies are checked separately. + +Both fresh workspaces assemble and compile the complete proof chain against +their respective generated models. They share proof source, never compiled +proofs or model definitions. Golden caller proofs use golden callee theorems; +live caller proofs use live callee theorems. + 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 @@ -235,8 +302,9 @@ 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 +live model in separate fresh Lake workspaces. Both must prove the same five +contracts and composition corollaries 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. @@ -273,32 +341,44 @@ 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. + checked-addition, bitwise, and assertion models represent those Rust + operations faithfully. The translated layout records and variants represent + their stored fields, not physical Rust layout or niche encoding. - 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. + Rust values by admitting zero; the alignment proofs establish positivity + from their explicit power-of-two requirement 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, the external `core.num` models, and the contract macro -and test namespaces. Only `propext`, +`Check.lean` checks that required declarations are theorems, validates their +declared proof edges, and audits all declarations in `Zerocopy` (including +proofs, obligations, translated layout types/methods, and utility helpers) and +the external `core.num` models, arithmetic lemmas, composition corollaries, +contract module, and contract tests. Private +helper names are included. 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: impossible total and partial -contracts must fail their proofs, an admitted proof must fail +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. +In both workspaces, removing the padding theorem must fail the caller's proof, +undeclared and unused theorem dependencies must fail the dependency audit, and +an incorrect translated padding callee must fail the proof chain. Exact +contracts reject always-zero padding and round-down, a wrong shallow-padding +flag, and a changed DST layout. Replacing round-down with its valid earlier +weaker contract must fail the independent required-type check. Unit tests +also reject missing dependencies and cycles and exercise method ownership and +Charon Self-type binding. Extraction rejects warnings, translation errors, missing artifacts, and LLBC whose `has_errors` is not exactly `false`, even when Charon exits zero. diff --git a/verification/aeneas/golden/layout.DstLayout.pad_to_align.lean.in b/verification/aeneas/golden/layout.DstLayout.pad_to_align.lean.in new file mode 100644 index 0000000000..58df8027b6 --- /dev/null +++ b/verification/aeneas/golden/layout.DstLayout.pad_to_align.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::layout::DstLayout::pad_to_align")@@ diff --git a/verification/aeneas/inline.py b/verification/aeneas/inline.py index a20212690c..57374812ea 100644 --- a/verification/aeneas/inline.py +++ b/verification/aeneas/inline.py @@ -43,7 +43,8 @@ def inventory(root): 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'}: + fields = {'rust', 'file', 'syntax', 'model', 'theorem', 'golden'} + if not fields <= set(entry) or set(entry) - fields - {'depends_on'}: raise ValueError('Unknown or missing inventory fields') identifier = r'[A-Za-z_][A-Za-z_0-9]*' patterns = {'rust': rf'{identifier}(?:::{identifier})*', @@ -62,9 +63,42 @@ def inventory(root): expected_rust = '::'.join(['zerocopy', *modules, entry['syntax']]) if entry['rust'] != expected_rust: raise ValueError('Rust identity must agree with the conventional source module path') + proof_order(entries) return entries +def proof_order(entries): + """Validate explicit proof edges and order independently of source order.""" + by_rust = {entry['rust']: entry for entry in entries} + for entry in entries: + dependencies = entry.get('depends_on', []) + if (not isinstance(dependencies, list) + or not all(isinstance(dep, str) for dep in dependencies) + or len(set(dependencies)) != len(dependencies)): + raise ValueError(f'{entry["rust"]}: invalid or duplicate proof dependencies') + missing = set(dependencies) - by_rust.keys() + if missing: + raise ValueError(f'{entry["rust"]}: missing proof dependencies: {sorted(missing)}') + ordered, visiting, visited = [], [], set() + + def visit(rust): + if rust in visiting: + cycle = visiting[visiting.index(rust):] + [rust] + raise ValueError('Cyclic proof dependencies: ' + ' -> '.join(cycle)) + if rust in visited: + return + visiting.append(rust) + for dependency in sorted(by_rust[rust].get('depends_on', [])): + visit(dependency) + visiting.pop() + visited.add(rust) + ordered.append(by_rust[rust]) + + for rust in sorted(by_rust): + visit(rust) + return ordered + + 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 @@ -226,18 +260,37 @@ 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()) + ordered = proof_order(list(annotations.values())) + proofs = '\n'.join(a['proof_text'] for a in ordered) (work / 'Proofs.lean').write_text(wrapper.replace('@@AENEAS_PROOFS@@', proofs)) required = ['import Lean', 'import Proofs', 'import Obligations', 'open Lean', ''] for a in annotations.values(): - # Total contracts and explicit successful-result requirements are equivalent. + # Normalize total WP and scalar order to independently written arithmetic. + # Layout matchers have different declaration names in the two modules; + # check both branches explicitly instead of assuming definitional equality. name = a['theorem'] - required.append(f'example : Zerocopy.Obligations.{name} := by\n' - f' simpa only [Zerocopy.Obligations.{name}, ' - 'Aeneas.Std.WP.spec_equiv_exists] ' - f'using Zerocopy.Proofs.{name}') + if name == 'pad_to_align_spec': + body = (f' unfold Zerocopy.Obligations.{name}\n' + ' intro self\n' + ' cases hs : self.size_info <;>\n' + ' simpa only [hs, Aeneas.Std.WP.spec_equiv_exists] ' + f'using Zerocopy.Proofs.{name} self') + else: + body = (f' simpa only [Zerocopy.Obligations.{name}, ' + 'Aeneas.Std.WP.spec_equiv_exists, Aeneas.Std.UScalar.eq_equiv, ' + 'Aeneas.Std.UScalar.coe_max, Zerocopy.Arithmetic.coe_min, ' + 'Aeneas.Std.UScalar.lt_equiv, Aeneas.Std.UScalar.le_equiv] ' + f'using Zerocopy.Proofs.{name}') + required.append(f'example : Zerocopy.Obligations.{name} := by\n{body}') names = ', '.join(f'`Zerocopy.Proofs.{a["theorem"]}' for a in annotations.values()) required.append(f'def requiredTheorems : Array Name := #[{names}]') + edges = [] + for a in ordered: + dependencies = ', '.join(f'`Zerocopy.Proofs.{annotations[dep]["theorem"]}' + for dep in a.get('depends_on', [])) + edges.append(f'(`Zerocopy.Proofs.{a["theorem"]}, #[{dependencies}])') + required.append('def proofDependencies : Array (Name × Array Name) := #[\n ' + + ',\n '.join(edges) + '\n]') (work / 'Required.lean').write_text('\n'.join(required) + '\n') @@ -246,15 +299,74 @@ def check_bindings(root, annotations, llbc): # 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']} + # At the pinned Charon version named Self types may be deduplicated. Only + # collect the Adt type domain, not unrelated Value/Deduplicated domains. + adts = {} + + def collect_adts(value): + if isinstance(value, dict): + if (set(value) == {'Value'} and isinstance(value['Value'], list) + and len(value['Value']) == 2 and isinstance(value['Value'][0], int)): + index, body = value['Value'] + if (isinstance(body, dict) and set(body) == {'Adt'} + and isinstance(body['Adt'], dict) + and set(body['Adt']) == {'id', 'generics', 'builtin'}): + if index in adts and adts[index] != body: + raise ValueError('Ambiguous deduplicated Charon Self type') + adts[index] = body + for child in value.values(): + collect_adts(child) + elif isinstance(value, list): + for child in value: + collect_adts(child) + + collect_adts(translated) + type_names = {t['def_id']: t['item_meta']['name'] + for t in translated.get('type_decls', []) if t} + + def identifiers(name): + if not all(set(element) == {'Ident'} and element['Ident'][1] == 0 for element in name): + raise ValueError('Unsupported extracted root identity') + return [element['Ident'][0] for element in name] + + def identity(name): + impls = [i for i, element in enumerate(name) if 'Impl' in element] + if not impls: + return '::'.join(identifiers(name)) + if impls != [len(name) - 2]: + raise ValueError('Unsupported extracted inherent method identity') + index = impls[0] + implementation = name[index]['Impl'] + if set(implementation) != {'Ty'}: + raise ValueError('Trait impl roots are unsupported') + implementation = implementation['Ty'] + if (implementation['kind'] != 'InherentImplBlock' + or any(implementation['params'].values())): + raise ValueError('Generic impl roots are unsupported') + wrapped = implementation['skip_binder'] + if set(wrapped) == {'Value'}: + body = wrapped['Value'][1] + elif set(wrapped) == {'Deduplicated'}: + body = adts.get(wrapped['Deduplicated'], {}) + else: + body = {} + if set(body) != {'Adt'}: + raise ValueError('Inherent Self must resolve to a named type') + adt = body['Adt'] + if adt['builtin'] is not None or any(adt['generics'].values()): + raise ValueError('Generic or builtin Self roots are unsupported') + self_name = identifiers(type_names.get(adt['id'], [])) + prefix = identifiers(name[:index]) + if not self_name or self_name[:-1] != prefix: + raise ValueError('Inherent Self must be defined in the annotated module') + return '::'.join([*self_name, *identifiers(name[index + 1:])]) + 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']) + name = identity(meta['name']) if name in roots: raise ValueError('Duplicate extracted root identity') roots[name] = meta @@ -279,7 +391,18 @@ def split_live(source, entries): # 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): + + def identity(display): + if '{' not in display: + return display + match = re.fullmatch(r'(.+::)\{([^{}]+)::([A-Za-z_][A-Za-z_0-9]*)\}::' + r'([A-Za-z_][A-Za-z_0-9]*)', display) + if not match or match[1] != match[2] + '::': + raise ValueError('Unsupported generated inherent method identity') + return match[1] + match[3] + '::' + match[4] + + identities = [identity(m[1]) for m in starts] + if set(identities) != {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 = [] @@ -292,13 +415,14 @@ def split_live(source, entries): 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]] + rust = identities[index] + entry = by_rust[rust] 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 + models[rust] = 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:] diff --git a/verification/aeneas/inventory.json b/verification/aeneas/inventory.json index 80da2c36d0..8273e867d0 100644 --- a/verification/aeneas/inventory.json +++ b/verification/aeneas/inventory.json @@ -2,6 +2,17 @@ "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::layout::DstLayout::pad_to_align", + "file": "zerocopy/src/layout.rs", + "syntax": "DstLayout::pad_to_align", + "model": "layout.DstLayout.pad_to_align", + "theorem": "pad_to_align_spec", + "golden": "layout.DstLayout.pad_to_align.lean.in", + "depends_on": [ + "zerocopy::util::padding_needed_for" + ] + }, { "rust": "zerocopy::util::max", "file": "zerocopy/src/util/mod.rs", diff --git a/verification/aeneas/lean/Arithmetic.lean b/verification/aeneas/lean/Arithmetic.lean new file mode 100644 index 0000000000..74f75c3c67 --- /dev/null +++ b/verification/aeneas/lean/Arithmetic.lean @@ -0,0 +1,168 @@ +/- 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 +import all Init.Data.Nat.Power2.Basic +@[expose] public section +open Aeneas Aeneas.Std +namespace Zerocopy.Arithmetic + +/-- Scalar minimum agrees with mathematical minimum. -/ +theorem coe_min (a b : Usize) : + ((min a b : Usize) : Nat) = Nat.min (a : Nat) (b : Nat) := by + by_cases h : a ≤ b + · rw [min_eq_left h] + exact (Nat.min_eq_left ((UScalar.le_equiv _ _).mp h)).symm + · have hba : b ≤ a := le_of_not_ge h + rw [min_eq_right hba] + exact (Nat.min_eq_right ((UScalar.le_equiv _ _).mp hba)).symm + +/-- The unique bounded padding that makes the sum divisible by alignment. -/ +theorem padding_unique (len align p : Nat) (hpos : 0 < align) + (hlt : p < align) (haligned : (len + p) % align = 0) : + p = (align - len % align) % align := by + have hr := Nat.mod_lt len hpos + have hsum : (len % align + p) % align = 0 := by + rw [Nat.add_mod, Nat.mod_eq_of_lt hlt] at haligned + exact haligned + by_cases hzero : len % align = 0 + · simpa only [hzero, Nat.zero_add, Nat.mod_eq_of_lt hlt, + Nat.sub_zero, Nat.mod_self] using hsum + · have hge : align ≤ len % align + p := by + by_contra h + rw [Nat.mod_eq_of_lt (by omega)] at hsum + omega + rw [Nat.mod_eq_sub_mod hge, Nat.mod_eq_of_lt (by omega)] at hsum + rw [Nat.mod_eq_of_lt (by omega)] + omega + +/-- Exact padding also gives minimality and the zero-padding criterion. -/ +theorem padding_properties (len align p : Nat) (hpos : 0 < align) + (hlt : p < align) (haligned : (len + p) % align = 0) : + p = (align - len % align) % align ∧ + (∀ q : Nat, (len + q) % align = 0 → p ≤ q) ∧ + (p = 0 ↔ len % align = 0) := by + refine ⟨padding_unique len align p hpos hlt haligned, ?_, ?_⟩ + · intro q hq + have hqm : (len + q % align) % align = 0 := by + rw [Nat.add_mod] at hq + rw [Nat.add_mod, Nat.mod_mod] + exact hq + have heq := padding_unique len align (q % align) hpos + (Nat.mod_lt q hpos) hqm + have hp := padding_unique len align p hpos hlt haligned + have := Nat.mod_le q align + omega + · constructor + · intro hp + simpa only [hp, Nat.add_zero] using haligned + · intro hl + have hp := padding_unique len align p hpos hlt haligned + simpa only [hl, Nat.sub_zero, Nat.mod_self] using hp + +/-- Clearing and retaining a bit mask partition the original word exactly. -/ +theorem mask_partition (n mask : Usize) : + (n &&& ~~~mask).val + (n &&& mask).val = n.val := by + have hdisjoint : (n.bv &&& ~~~mask.bv) &&& (n.bv &&& mask.bv) = 0 := by + ext i + simp only [BitVec.getElem_and, BitVec.getElem_not] + cases n.bv[i] <;> cases mask.bv[i] <;> simp + have hjoin : (n.bv &&& ~~~mask.bv) ||| (n.bv &&& mask.bv) = n.bv := by + ext i + simp only [BitVec.getElem_or, BitVec.getElem_and, BitVec.getElem_not] + cases n.bv[i] <;> cases mask.bv[i] <;> decide + have hsum := BitVec.add_eq_or_of_and_eq_zero _ _ hdisjoint + rw [hjoin] at hsum + have := congrArg BitVec.toNat hsum + rw [BitVec.toNat_add_of_and_eq_zero hdisjoint] at this + exact this + +/-- A power-of-two alignment divides the word modulus. -/ +theorem alignment_dvd_size (align : Usize) (h : align.val.isPowerOfTwo) : + align.val ∣ UScalar.size .Usize := by + obtain ⟨k, hk⟩ := h + have hsize := UScalar.hSize align + rw [UScalar.size, hk] at hsize ⊢ + exact Nat.pow_dvd_pow 2 ((Nat.pow_le_pow_iff_right (a := 2) (by decide)).mp (by omega)) + +/-- Complementing the wrapping predecessor produces modular negation. -/ +theorem complement_predecessor (len : Usize) : + (~~~(core.num.Usize.wrapping_sub len 1#usize)).val = + if len.val = 0 then 0 else UScalar.size .Usize - len.val := by + change (~~~(len.bv - (1#usize).bv)).toNat = _ + rw [BitVec.toNat_not] + have hsize := UScalar.hSize len + have hone : (1#usize).val = 1 := by simp + by_cases hz : len.val = 0 + · simp only [hz, if_true] + rw [BitVec.toNat_sub, UScalar.bv_toNat, UScalar.bv_toNat] + change 2 ^ System.Platform.numBits - 1 - + ((2 ^ System.Platform.numBits - (1#usize).val) + len.val) % 2 ^ System.Platform.numBits = 0 + rw [hz, hone, Nat.add_zero, Nat.mod_eq_of_lt (by have := Nat.two_pow_pos System.Platform.numBits; omega)] + omega + · simp only [hz, if_false] + rw [BitVec.toNat_sub_of_le (by simpa only [BitVec.le_def, UScalar.bv_toNat, hone] using (show 1 ≤ len.val by omega)), UScalar.bv_toNat, UScalar.bv_toNat, hone] + change 2 ^ System.Platform.numBits - 1 - (len.val - 1) = UScalar.size .Usize - len.val + rw [UScalar.size] at hsize ⊢ + change len.val < 2 ^ System.Platform.numBits at hsize + change 2 ^ System.Platform.numBits - 1 - (len.val - 1) = + 2 ^ System.Platform.numBits - len.val + omega + +/-- The padding bit mask aligns the unbounded sum, including wrapping at zero. -/ +theorem padding_mask_aligned (len align mask : Usize) + (h : align.val.isPowerOfTwo) (hm : mask.val = align.val - 1) : + (len.val + (~~~(core.num.Usize.wrapping_sub len 1#usize) &&& mask).val) + % align.val = 0 := by + have hmod := Nat.mod_eq_zero_of_dvd (alignment_dvd_size align h) + have hsum : (len.val + (~~~(core.num.Usize.wrapping_sub len 1#usize)).val) + % align.val = 0 := by + rw [complement_predecessor] + split + · rename_i hz + simp only [hz, Nat.zero_add, Nat.zero_mod] + · have hsize := UScalar.hSize len + rw [Nat.add_sub_of_le (by omega)] + exact hmod + obtain ⟨k, hk⟩ := h + rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod] + rw [hk, Nat.add_mod] at hsum + rw [Nat.add_mod, Nat.mod_mod] + exact hsum + +/-- The exact arithmetic result of clearing the low alignment bits. -/ +theorem round_down_exact (n align mask : Usize) + (h : align.val.isPowerOfTwo) (hm : mask.val = align.val - 1) : + (n &&& ~~~mask).val = n.val - n.val % align.val := by + have hp := mask_partition n mask + have hlow : (n &&& mask).val = n.val % align.val := by + obtain ⟨k, hk⟩ := h + rw [UScalar.val_and, hm, hk, Nat.and_two_pow_sub_one_eq_mod] + rw [hlow] at hp + omega + +/-- An exact round-down result is aligned and the greatest such lower bound. -/ +theorem round_down_properties (n align m : Nat) (hpos : 0 < align) + (hm : m = n - n % align) : + m ≤ n ∧ m % align = 0 ∧ n < m + align ∧ + (∀ q : Nat, q ≤ n → q % align = 0 → q ≤ m) := by + have hr := Nat.mod_lt n hpos + have hrle := Nat.mod_le n align + have hmul : m = (n / align) * align := by + rw [Nat.div_mul_self_eq_mod_sub_self, hm] + refine ⟨by omega, ?_, by omega, ?_⟩ + · rw [hmul, Nat.mul_mod_left] + · intro q hqn hqa + have hdiv := Nat.div_le_div_right (c := align) hqn + have hle := Nat.mul_le_mul_right align hdiv + rw [Nat.div_mul_self_eq_mod_sub_self, Nat.div_mul_self_eq_mod_sub_self, + hqa, Nat.sub_zero, ← hm] at hle + exact hle + +end Zerocopy.Arithmetic diff --git a/verification/aeneas/lean/Check.lean b/verification/aeneas/lean/Check.lean index 076926785a..c0b42939bd 100644 --- a/verification/aeneas/lean/Check.lean +++ b/verification/aeneas/lean/Check.lean @@ -8,6 +8,7 @@ those terms. -/ import Required import ContractTests +import Corollaries open Lean Elab Command run_elab do let required := requiredTheorems @@ -16,11 +17,41 @@ run_elab do match env.find? declName with | some (.thmInfo _) => pure () | _ => throwError "Missing required theorem {declName}" - let prefixes := #[`Zerocopy.Proofs, `Zerocopy.Obligations, `Zerocopy.util, `core.num, - `AeneasContracts, `ContractTests] + let some proofModule := env.getModuleIdxFor? required[0]! + | throwError "Required proofs must be imported from the generated Proofs module" + for (declName, declared) in proofDependencies do + -- Inspect elaborated terms, including compiler-generated local helpers. + -- Stop at another registered theorem: its own edges are checked separately. + let mut pending := #[declName] + let mut visited : NameHashSet := {} + let mut actual : Array Name := #[] + while !pending.isEmpty do + let current := pending.back! + pending := pending.pop + if visited.contains current then continue + visited := visited.insert current + let some info := env.find? current + | throwError "Missing proof declaration {current}" + let references := info.type.getUsedConstants ++ + ((info.value? (allowOpaque := true)).map (·.getUsedConstants)).getD #[] + for used in references do + if used == declName then continue + if required.contains used then + unless actual.contains used do actual := actual.push used + else if env.getModuleIdxFor? used == some proofModule then + pending := pending.push used + for used in actual do + unless declared.contains used do + throwError "{declName} has undeclared proof dependency {used}" + for used in declared do + unless actual.contains used do + throwError "{declName} has unused proof dependency {used}" + logInfo m!"Checked proof dependencies of {proofDependencies.size} theorems" + let prefixes := #[`Zerocopy, `core.num, `AeneasContracts, `ContractTests] let mut audited := 0 for (declName, _) in env.constants.toList do - if prefixes.any (·.isPrefixOf (privateToUserName declName)) then + if prefixes.any (·.isPrefixOf (privateToUserName declName)) || + env.getModuleIdxFor? declName == some proofModule then let used ← collectAxioms declName for ax in used do unless #[`propext, `Classical.choice, `Quot.sound].contains ax do diff --git a/verification/aeneas/lean/Corollaries.lean b/verification/aeneas/lean/Corollaries.lean new file mode 100644 index 0000000000..8461b0abbf --- /dev/null +++ b/verification/aeneas/lean/Corollaries.lean @@ -0,0 +1,160 @@ +/- 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 Proofs +@[expose] public section +open Aeneas Aeneas.Std Aeneas.Std.Result +namespace Zerocopy.Corollaries +open Proofs + +/- Selecting either input preserves any predicate shared by both inputs. -/ +contract max_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop) + for util.max a b + requires ha : P a + requires hb : P b + ensures r => P r + proof: + step with max_spec a b as ⟨r, _, hchoice, _, _⟩ + rcases hchoice with h | h + · simpa only [h] using ha + · simpa only [h] using hb + +contract min_preserves (a b : NonZeroUsize) (P : NonZeroUsize → Prop) + for util.min a b + requires ha : P a + requires hb : P b + ensures r => P r + proof: + step with min_spec a b as ⟨r, _, hchoice, _, _⟩ + rcases hchoice with h | h + · simpa only [h] using ha + · simpa only [h] using hb + +/-- Aligned inputs are fixed points of round-down. -/ +theorem round_down_aligned (n : Usize) (align : NonZeroUsize) + (hpow : (align.val : Nat).isPowerOfTwo) + (haligned : (n : Nat) % (align.val : Nat) = 0) : + util.round_down_to_next_multiple_of_alignment n align = .ok n := by + obtain ⟨m, hm, _, hexact, _, _, _⟩ := + WP.spec_imp_exists (round_down_spec n align hpow) + have heq : m = n := UScalar.eq_of_val_eq (by + simpa only [haligned, Nat.sub_zero] using hexact) + simpa only [heq] using hm + +contract round_down_idempotent (n : Usize) (align : NonZeroUsize) + for (do + let m ← util.round_down_to_next_multiple_of_alignment n align + let m' ← util.round_down_to_next_multiple_of_alignment m align + ok (m, m')) + requires hpow : (align.val : Nat).isPowerOfTwo + ensures m m' => m' = m + proof: + step with round_down_spec n align hpow as ⟨m, _, _, haligned, _, _⟩ + rw [round_down_aligned m align hpow haligned] + simp only [bind_ok, WP.spec_ok, WP.uncurry'_pair] + +contract round_down_monotone (a b : Usize) (align : NonZeroUsize) + for (do + let m ← util.round_down_to_next_multiple_of_alignment a align + let m' ← util.round_down_to_next_multiple_of_alignment b align + ok (m, m')) + requires hab : a ≤ b + requires hpow : (align.val : Nat).isPowerOfTwo + ensures m m' => m ≤ m' + proof: + step with round_down_spec a align hpow as ⟨m, hbound, _, haligned, _, _⟩ + step with round_down_spec b align hpow as ⟨m', _, _, _, _, hgreatest⟩ + apply (UScalar.le_equiv _ _).mpr + exact hgreatest m.val ((UScalar.le_equiv _ _).mp (le_trans hbound hab)) haligned + +/-- The original headroom condition implies the exact fit requirement. -/ +theorem pad_to_align_sized_headroom (self : layout.DstLayout) (size : Usize) + (hs : self.size_info = layout.SizeInfo.Sized size) + (hpow : (self.align.val : Nat).isPowerOfTwo) + (hroom : (size : Nat) + (self.align.val : Nat) - 1 ≤ Usize.max) : + ∃ r, layout.DstLayout.pad_to_align self = .ok r := by + have hpos := Nat.pos_of_isPowerOfTwo hpow + have hlt := Nat.mod_lt (self.align.val.val - size.val % self.align.val.val) hpos + have hp := pad_to_align_spec self (by + simp only [hs] + exact ⟨hpow, by omega⟩) + obtain ⟨r, hr, _⟩ := WP.spec_imp_exists hp + exact ⟨r, hr⟩ + +/-- Padding an already aligned sized layout or any DST is the identity. -/ +theorem pad_to_align_aligned (self : layout.DstLayout) + (h : ∀ size, self.size_info = layout.SizeInfo.Sized size → + (self.align.val : Nat).isPowerOfTwo ∧ + (size : Nat) % (self.align.val : Nat) = 0) : + layout.DstLayout.pad_to_align self = .ok self := by + cases hs : self.size_info with + | SliceDst dst => + have hp := pad_to_align_spec self (by simp only [hs]) + obtain ⟨r, hr, _, heq⟩ := WP.spec_imp_exists hp + simp only [hs] at heq + simpa only [heq] using hr + | Sized size => + obtain ⟨hpow, haligned⟩ := h size hs + have hp := pad_to_align_spec self (by + simp only [hs] + refine ⟨hpow, ?_⟩ + simp only [haligned, Nat.sub_zero, Nat.mod_self, Nat.add_zero] + scalar_tac) + obtain ⟨r, hr, halign, hpost⟩ := WP.spec_imp_exists hp + simp only [hs] at hpost + obtain ⟨padded, hinfo, hexact, _, _, _, _, hflag⟩ := hpost + have heq : padded = size := UScalar.eq_of_val_eq (by + simpa only [haligned, Nat.sub_zero, Nat.mod_self, Nat.add_zero] using hexact) + have hflag' : r.statically_shallow_unpadded = self.statically_shallow_unpadded := by + simpa only [haligned, decide_true, Bool.and_true] using hflag + have hrself : r = self := by + cases r + cases self + simp_all + simpa only [hrself] using hr + +/- Reapplying layout padding succeeds and leaves the first result unchanged. -/ +contract pad_to_align_idempotent (self : layout.DstLayout) + for (do + let r ← layout.DstLayout.pad_to_align self + let r' ← layout.DstLayout.pad_to_align r + ok (r, r')) + requires h : ∀ size, self.size_info = layout.SizeInfo.Sized size → + let S : Nat := size + let A : Nat := self.align.val + A.isPowerOfTwo ∧ S + (A - S % A) % A ≤ Usize.max + ensures r r' => r' = r + proof: + have hp := pad_to_align_spec self (by + cases hs : self.size_info with + | Sized size => exact h size hs + | SliceDst dst => trivial) + obtain ⟨r, hr, halign, hpost⟩ := WP.spec_imp_exists hp + rw [hr, bind_ok] + have hraligned : ∀ size, r.size_info = layout.SizeInfo.Sized size → + (r.align.val : Nat).isPowerOfTwo ∧ + (size : Nat) % (r.align.val : Nat) = 0 := by + cases hs : self.size_info with + | SliceDst dst => + simp only [hs] at hpost + intro size hsize + rw [hpost, hs] at hsize + contradiction + | Sized size => + obtain ⟨hpow, _⟩ := h size hs + simp only [hs] at hpost + obtain ⟨padded, hinfo, _, _, _, haligned, _, _⟩ := hpost + intro size' hsize + rw [hinfo] at hsize + cases hsize + simpa only [halign] using And.intro hpow haligned + rw [pad_to_align_aligned r hraligned] + simp only [bind_ok, WP.spec_ok, WP.uncurry'_pair] + +end Zerocopy.Corollaries diff --git a/verification/aeneas/lean/Obligations.lean b/verification/aeneas/lean/Obligations.lean index 58f7972ea8..46a42c684a 100644 --- a/verification/aeneas/lean/Obligations.lean +++ b/verification/aeneas/lean/Obligations.lean @@ -14,23 +14,52 @@ namespace Zerocopy.Obligations abbrev NonZeroUsize := core.num.nonzero.NonZero Usize core.num.niche_types.NonZeroUsizeInner +-- Written independently of the contract expansions, using mathematical values. 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 + ∀ (a b : NonZeroUsize), ∃ r, util.max a b = .ok r ∧ + r.val.val = Nat.max a.val.val b.val.val ∧ (r = a ∨ r = b) ∧ + a.val.val ≤ r.val.val ∧ b.val.val ≤ r.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 + ∀ (a b : NonZeroUsize), ∃ r, util.min a b = .ok r ∧ + r.val.val = Nat.min a.val.val b.val.val ∧ (r = a ∨ r = b) ∧ + r.val.val ≤ a.val.val ∧ r.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 ⦄ + ∀ (len : Usize) (align : NonZeroUsize) (_h : align.val.val.isPowerOfTwo), + util.padding_needed_for len align ⦃ p => p.val < align.val.val ∧ + p.val = (align.val.val - len.val % align.val.val) % align.val.val ∧ + (len.val + p.val) % align.val.val = 0 ∧ + (∀ q : Nat, (len.val + q) % align.val.val = 0 → p.val ≤ q) ∧ + (p.val = 0 ↔ len.val % align.val.val = 0) ⦄ 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 ⦄ + (_h : align.val.val.isPowerOfTwo), + util.round_down_to_next_multiple_of_alignment n align ⦃ m => + m.val ≤ n.val ∧ m.val = n.val - n.val % align.val.val ∧ + m.val % align.val.val = 0 ∧ n.val < m.val + align.val.val ∧ + (∀ q : Nat, q ≤ n.val → q % align.val.val = 0 → q ≤ m.val) ⦄ + +def pad_to_align_spec : Prop := + ∀ (self : layout.DstLayout) + (_h : match self.size_info with + | layout.SizeInfo.Sized size => + self.align.val.val.isPowerOfTwo ∧ + size.val + (self.align.val.val - size.val % self.align.val.val) + % self.align.val.val ≤ Usize.max + | layout.SizeInfo.SliceDst _ => True), + layout.DstLayout.pad_to_align self ⦃ r => r.align = self.align ∧ + match self.size_info with + | layout.SizeInfo.Sized size => ∃ padded, + r.size_info = layout.SizeInfo.Sized padded ∧ + padded.val = size.val + (self.align.val.val - size.val % self.align.val.val) + % self.align.val.val ∧ + size.val ≤ padded.val ∧ padded.val < size.val + self.align.val.val ∧ + padded.val % self.align.val.val = 0 ∧ + (∀ q : Nat, size.val ≤ q → q % self.align.val.val = 0 → padded.val ≤ q) ∧ + r.statically_shallow_unpadded = + (self.statically_shallow_unpadded && decide (size.val % self.align.val.val = 0)) + | layout.SizeInfo.SliceDst _ => r = self ⦄ end Zerocopy.Obligations diff --git a/verification/aeneas/lean/Proofs.lean.in b/verification/aeneas/lean/Proofs.lean.in index 06e0a01d06..fd70069664 100644 --- a/verification/aeneas/lean/Proofs.lean.in +++ b/verification/aeneas/lean/Proofs.lean.in @@ -9,6 +9,7 @@ those terms. -/ module public import Zerocopy.Funs public import Contracts +public import Arithmetic import all Init.Data.Nat.Power2.Basic @[expose] public section open Aeneas Aeneas.Std diff --git a/verification/aeneas/negative-controls.sh b/verification/aeneas/negative-controls.sh index b9cfcefd29..bddc7579be 100755 --- a/verification/aeneas/negative-controls.sh +++ b/verification/aeneas/negative-controls.sh @@ -18,9 +18,11 @@ cd "$repo/target/aeneas/$1" echo "Testing failure controls in $1" backup=$(mktemp -d) cp Proofs.lean "$backup/Proofs.lean" +cp Required.lean "$backup/Required.lean" cp Zerocopy/Funs.lean "$backup/Funs.lean" restore() { cp "$backup/Proofs.lean" Proofs.lean + cp "$backup/Required.lean" Required.lean cp "$backup/Funs.lean" Zerocopy/Funs.lean rm -rf "$backup" } @@ -90,6 +92,145 @@ partial contract partial_return_control end Zerocopy.Proofs LEAN +# The caller must actually have its callee theorem available during elaboration. +python3 - <<'PY' +from pathlib import Path +p = Path("Proofs.lean") +s = p.read_text() +old = 'contract padding_lt_alignment ' +if s.count(old) != 1: + raise SystemExit("Callee theorem negative control no longer matches") +p.write_text(s.replace(old, 'contract unavailable_padding_lt_alignment ')) +PY +if lake build Proofs > "$backup/dependency-build.log" 2>&1; then + echo "Caller proof accepted an unavailable callee theorem" >&2 + exit 1 +fi +if ! grep -q 'Unknown identifier.*padding_lt_alignment' "$backup/dependency-build.log"; then + cat "$backup/dependency-build.log" >&2; exit 1 +fi +echo "Confirmed: caller proof rejects an unavailable callee theorem" +cp "$backup/Proofs.lean" Proofs.lean + +# A private alias outside the proof namespace must not hide a callee reference. +python3 - <<'PY' +from pathlib import Path +p = Path("Proofs.lean") +s = p.read_text() +alias = '''end Zerocopy.Proofs +namespace DependencyControl +private def padding_alias := Zerocopy.Proofs.padding_lt_alignment +end DependencyControl +namespace Zerocopy.Proofs + +''' +call = 'step with padding_lt_alignment size self.align hpow' +if s.count('contract pad_to_align_spec ') != 1 or s.count(call) != 1: + raise SystemExit("Private helper dependency control no longer matches") +s = s.replace('contract pad_to_align_spec ', alias + 'contract pad_to_align_spec ') +p.write_text(s.replace(call, 'step with DependencyControl.padding_alias size self.align hpow')) +PY +lake build Required > "$backup/helper-build.log" 2>&1 || { + cat "$backup/helper-build.log" >&2; exit 1; +} +lake env lean -DwarningAsError=true Check.lean > "$backup/helper-check.log" 2>&1 || { + cat "$backup/helper-check.log" >&2; exit 1; +} +echo "Confirmed: dependency audit follows a private helper outside the proof namespace" + +# Terms remain valid when an edge is omitted; the dependency audit must catch it. +python3 - <<'PY' +from pathlib import Path +p = Path("Required.lean") +s = p.read_text() +old = '(`Zerocopy.Proofs.pad_to_align_spec, #[`Zerocopy.Proofs.padding_lt_alignment])' +if s.count(old) != 1: + raise SystemExit("Undeclared dependency negative control no longer matches") +p.write_text(s.replace(old, '(`Zerocopy.Proofs.pad_to_align_spec, #[])')) +PY +lake build Required > "$backup/undeclared-build.log" 2>&1 || { + cat "$backup/undeclared-build.log" >&2; exit 1; +} +if lake env lean Check.lean > "$backup/undeclared-check.log" 2>&1; then + echo "Dependency audit accepted an undeclared proof reference" >&2; exit 1 +fi +if ! grep -q 'undeclared proof dependency.*padding_lt_alignment' "$backup/undeclared-check.log"; then + cat "$backup/undeclared-check.log" >&2; exit 1 +fi +echo "Confirmed: dependency audit rejects an undeclared proof reference" +cp "$backup/Required.lean" Required.lean +cp "$backup/Proofs.lean" Proofs.lean + +python3 - <<'PY' +from pathlib import Path +p = Path("Required.lean") +s = p.read_text() +old = '(`Zerocopy.Proofs.max_spec, #[])' +if s.count(old) != 1: + raise SystemExit("Unused dependency negative control no longer matches") +p.write_text(s.replace(old, '(`Zerocopy.Proofs.max_spec, #[`Zerocopy.Proofs.min_spec])')) +PY +lake build Required > "$backup/unused-build.log" 2>&1 || { + cat "$backup/unused-build.log" >&2; exit 1; +} +if lake env lean Check.lean > "$backup/unused-check.log" 2>&1; then + echo "Dependency audit accepted an unused proof dependency" >&2; exit 1 +fi +if ! grep -q 'unused proof dependency.*min_spec' "$backup/unused-check.log"; then + cat "$backup/unused-check.log" >&2; exit 1 +fi +echo "Confirmed: dependency audit rejects an unused proof dependency" +cp "$backup/Required.lean" Required.lean + +python3 - <<'PY' +from pathlib import Path +p = Path("Zerocopy/Funs.lean") +s = p.read_text() +old = 'ok (i2 &&& mask)' +if s.count(old) != 1: + raise SystemExit("Callee model negative control no longer matches") +p.write_text(s.replace(old, 'ok i')) +PY +if lake build Required > "$backup/callee-model-build.log" 2>&1; then + echo "Proof chain accepted an incorrect translated padding callee" >&2; exit 1 +fi +if ! grep -Eq '(error: Proofs[.]lean:|Proofs[.]lean:.*error)' "$backup/callee-model-build.log"; then + cat "$backup/callee-model-build.log" >&2; exit 1 +fi +echo "Confirmed: proof chain rejects an incorrect translated padding callee" +cp "$backup/Funs.lean" Zerocopy/Funs.lean + +# These mutations satisfy earlier weak bounds but violate the exact contracts. +reject_model() { + local description=$1 + python3 - "$2" "$3" <<'PYCONTROL' +from pathlib import Path +import sys +p = Path("Zerocopy/Funs.lean") +s = p.read_text() +old, new = sys.argv[1:] +if s.count(old) != 1: + raise SystemExit("Strong model negative control no longer matches") +p.write_text(s.replace(old, new)) +PYCONTROL + if lake build Required > "$backup/strong-model-build.log" 2>&1; then + echo "Proofs accepted $description" >&2; exit 1 + fi + if ! grep -Eq '(error: Proofs[.]lean:|Proofs[.]lean:.*error)' "$backup/strong-model-build.log"; then + cat "$backup/strong-model-build.log" >&2; exit 1 + fi + echo "Confirmed: exact contracts reject $description" + cp "$backup/Funs.lean" Zerocopy/Funs.lean +} +reject_model "always-zero padding" 'ok (i2 &&& mask)' 'ok 0#usize' +reject_model "always-zero round-down" 'ok (n &&& mask)' 'ok 0#usize' +reject_model "an incorrect shallow-padding flag" \ + 'statically_shallow_unpadded := (static_padding = 0#usize)' \ + 'statically_shallow_unpadded := true' +reject_model "a changed DST layout" \ + 'layout.SizeInfo.SliceDst _ => ok (0#usize, self.size_info)' \ + 'layout.SizeInfo.SliceDst _ => ok (0#usize, layout.SizeInfo.Sized 0#usize)' + cat >> Proofs.lean <<'LEAN' namespace Zerocopy.Proofs theorem negative_control : True := by sorry @@ -132,6 +273,49 @@ fi echo "Confirmed: required obligations reject an unrelated True theorem" cp "$backup/Proofs.lean" Proofs.lean +# The earlier round-down contract is true, but too weak for current obligations. +cat > "$backup/weaker-round.lean" <<'LEAN' +contract round_down_spec (n : Usize) (align : NonZeroUsize) + for util.round_down_to_next_multiple_of_alignment n align + requires h : (align.val : Nat).isPowerOfTwo + ensures m => m ≤ n ∧ m.val % align.val.val = 0 + proof: + have hpos := Nat.pos_of_isPowerOfTwo h + 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] + have hexact := Arithmetic.round_down_exact n align.val mask h hval + obtain ⟨hbound, haligned, _, _⟩ := + Arithmetic.round_down_properties _ _ _ hpos hexact + exact ⟨(UScalar.le_equiv _ _).mpr hbound, haligned⟩ +LEAN +python3 - "$backup/weaker-round.lean" <<'PYCONTROL' +from pathlib import Path +import re +import sys +p = Path("Proofs.lean") +s, count = re.subn( + r'contract round_down_spec\b.*?(?=\n(?:theorem|contract|partial contract) |\nend Zerocopy.Proofs)', + Path(sys.argv[1]).read_text(), p.read_text(), flags=re.S) +if count != 1: + raise SystemExit("Weaker round-down control no longer matches") +p.write_text(s) +PYCONTROL +lake build Proofs > "$backup/weaker-proof-build.log" 2>&1 || { + cat "$backup/weaker-proof-build.log" >&2; exit 1; +} +if lake build Required > "$backup/weaker-required-build.log" 2>&1; then + echo "Required obligations accepted the earlier weak round-down contract" >&2; exit 1 +fi +if ! grep -Eq '(error: Required[.]lean:|Required[.]lean:.*error)' "$backup/weaker-required-build.log"; then + cat "$backup/weaker-required-build.log" >&2; exit 1 +fi +echo "Confirmed: a valid weaker contract fails independent required-type checks" +cp "$backup/Proofs.lean" Proofs.lean + python3 - <<'PY' from pathlib import Path p = Path("Zerocopy/Funs.lean") diff --git a/verification/aeneas/prepare.py b/verification/aeneas/prepare.py index c59c60babc..7ad8aac412 100644 --- a/verification/aeneas/prepare.py +++ b/verification/aeneas/prepare.py @@ -75,6 +75,8 @@ def share_manifest(workspace, backend): 'package zerocopyVerification\n' '@[default_target] lean_lib Zerocopy\n' 'lean_lib Contracts\n' + 'lean_lib Arithmetic\n' + '@[default_target] lean_lib Corollaries\n' '@[default_target] lean_lib ContractTests\n' '@[default_target] lean_lib Proofs\n' 'lean_lib Obligations\n' diff --git a/verification/aeneas/run.sh b/verification/aeneas/run.sh index cc9564b4a2..e490121eb3 100755 --- a/verification/aeneas/run.sh +++ b/verification/aeneas/run.sh @@ -37,7 +37,7 @@ initialize_workspace() { check_proofs() ( cd "$1" lake build - for source in Proofs.lean ContractTests.lean; do + for source in Arithmetic.lean Proofs.lean ContractTests.lean Corollaries.lean; do lake env lean -DwarningAsError=true "$source" done # Always run the audit, even if Lake caches its imports. diff --git a/verification/aeneas/scaffolding/Funs.lean b/verification/aeneas/scaffolding/Funs.lean index 9a04817e48..3df7154970 100644 --- a/verification/aeneas/scaffolding/Funs.lean +++ b/verification/aeneas/scaffolding/Funs.lean @@ -68,6 +68,11 @@ def Usize.Insts.CoreNumNonzeroZeroablePrimitiveNonZeroUsizeInner : Source: 'src/util/mod.rs', lines 155:0-243:1 -/ @@AENEAS_GOLDEN("util.padding_needed_for.lean.in")@@ +/-- [zerocopy::layout::{zerocopy::layout::DstLayout}::pad_to_align]: + Source: 'src/layout.rs', lines 492:4-562:5 + Visibility: public -/ +@@AENEAS_GOLDEN("layout.DstLayout.pad_to_align.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")@@ diff --git a/verification/aeneas/scaffolding/Types.lean b/verification/aeneas/scaffolding/Types.lean index 687cf0b1f8..c08bb078be 100644 --- a/verification/aeneas/scaffolding/Types.lean +++ b/verification/aeneas/scaffolding/Types.lean @@ -39,4 +39,26 @@ structure core.num.nonzero.ZeroablePrimitive (Self : Type) (Self_NonZeroInner : markerCopyInst : core.marker.Copy Self innerCopyInst : core.marker.Copy Self_NonZeroInner +/-- [zerocopy::layout::TrailingSliceLayout] + Source: 'src/layout.rs', lines 52:0-68:1 -/ +structure layout.TrailingSliceLayout (E : Type) where + offset : Std.Usize + elem_size : E + +/-- [zerocopy::layout::SizeInfo] + Source: 'src/layout.rs', lines 45:0-48:1 -/ +@[discriminant isize] +inductive layout.SizeInfo (E : Type) where +| Sized : Std.Usize → layout.SizeInfo E +| SliceDst : layout.TrailingSliceLayout E → layout.SizeInfo E + +/-- [zerocopy::layout::DstLayout] + Source: 'src/layout.rs', lines 33:0-41:1 + Visibility: public -/ +structure layout.DstLayout where + align : core.num.nonzero.NonZero Std.Usize + core.num.niche_types.NonZeroUsizeInner + size_info : layout.SizeInfo Std.Usize + statically_shallow_unpadded : Bool + end Zerocopy diff --git a/verification/aeneas/tests/test_inline.py b/verification/aeneas/tests/test_inline.py index a909e624d6..3bce35f408 100644 --- a/verification/aeneas/tests/test_inline.py +++ b/verification/aeneas/tests/test_inline.py @@ -64,10 +64,59 @@ def test_rejects_comments_statements_and_nested_scopes_before_fence(self): 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 + '} }'): + 'impl Trait for S { fn f() {\n' + BLOCK + '} }'): with self.assertRaises(ValueError): self.parse(source) + def test_inherent_method_ownership_and_unsupported_impls(self): + found = self.parse('mod m { impl S { fn f(self) {\n' + BLOCK + '} } }') + self.assertEqual(found[0]['syntax'], 'm::S::f') + for implementation, method in [('impl S', 'fn f()'), + ('impl Trait for S', 'fn f()'), + ('impl m::S', 'fn f()'), + ('impl S', 'fn f()')]: + with self.subTest(implementation=implementation, method=method), self.assertRaises(ValueError): + self.parse(implementation + ' { ' + method + ' {\n' + BLOCK + '} }') + + def test_proof_dependency_order_is_independent_of_source_order(self): + caller = {'rust': 'caller', 'depends_on': ['callee']} + callee = {'rust': 'callee'} + independent = {'rust': 'independent'} + expected = [callee, caller, independent] + self.assertEqual(inline.proof_order([caller, independent, callee]), expected) + self.assertEqual(inline.proof_order([independent, callee, caller]), expected) + + def test_proof_dependency_validation(self): + for dependencies, message in [(['missing'], 'missing proof dependencies'), + (['callee', 'callee'], 'duplicate'), + ('callee', 'invalid'), + ([None], 'invalid'), + (['caller'], 'Cyclic')]: + with self.subTest(dependencies=dependencies), self.assertRaisesRegex(ValueError, message): + inline.proof_order([{'rust': 'caller', 'depends_on': dependencies}, + {'rust': 'callee'}]) + with self.assertRaisesRegex(ValueError, 'caller -> callee -> caller|callee -> caller -> callee'): + inline.proof_order([{'rust': 'caller', 'depends_on': ['callee']}, + {'rust': 'callee', 'depends_on': ['caller']}]) + + def test_assembly_orders_proofs_and_records_declared_edges(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + wrapper = root / 'verification/aeneas/lean/Proofs.lean.in' + wrapper.parent.mkdir(parents=True) + wrapper.write_text('@@AENEAS_PROOFS@@') + caller = {'rust': 'caller', 'theorem': 'caller_spec', + 'depends_on': ['callee'], 'proof_text': 'theorem caller_spec := callee_spec\n'} + callee = {'rust': 'callee', 'theorem': 'callee_spec', + 'proof_text': 'theorem callee_spec : True := by trivial\n'} + work = root / 'work' + work.mkdir() + inline.assemble(root, {'caller': caller, 'callee': callee}, work) + proof = (work / 'Proofs.lean').read_text() + self.assertLess(proof.index('theorem callee_spec'), proof.index('theorem caller_spec')) + required = (work / 'Required.lean').read_text() + self.assertIn('(`Zerocopy.Proofs.caller_spec, #[`Zerocopy.Proofs.callee_spec])', required) + def test_rejects_near_miss_guards_missing_sections_and_broken_fences(self): variants = [BLOCK.replace('```aeneas', '```Aeneas'), BLOCK.replace('```aeneas', '```aeneos'), @@ -226,6 +275,64 @@ def test_llbc_binding_rejects_cfg_alternatives_stale_sources_and_missing_roots(s with self.subTest(kind=kind), self.assertRaises(ValueError): inline.check_bindings(root, annotations, llbc) + def test_inherent_method_llbc_identity_resolves_named_self(self): + with tempfile.TemporaryDirectory() as tmp: + root = Path(tmp) + entry = {**ENTRY, 'rust': 'zerocopy::util::S::f', 'syntax': 'S::f', 'model': 'util.S.f'} + path = root / entry['file'] + path.parent.mkdir(parents=True) + source = 'struct S; impl S { fn f(self) {\n' + BLOCK.replace('def util.f', 'def util.S.f') + '} }\n' + path.write_text(source) + annotations = inline.discover(root, TOOL, [entry]) + annotation = annotations[entry['rust']] + type_name = [{'Ident': [part, 0]} for part in ['zerocopy', 'util', 'S']] + body = {'Adt': {'id': 1, 'builtin': None, + 'generics': {'regions': [], 'types': [], 'const_generics': [], 'trait_refs': []}}} + impl = {'Ty': {'kind': 'InherentImplBlock', 'params': {'types': [], 'regions': []}, + 'skip_binder': {'Deduplicated': 3}}} + name = [*type_name[:2], {'Impl': impl}, {'Ident': ['f', 0]}] + data = {'translated': { + 'files': [{'id': 1, 'name': {'Local': 'src/util/mod.rs'}, 'contents': source}], + 'item_names': [{'value': {'Value': [3, body]}}], + 'type_decls': [{'def_id': 1, 'item_meta': {'name': type_name}}], + 'fun_decls': [{'item_meta': { + 'name': name, '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 ('wrong_self', 'missing_self', 'generic', 'trait', 'cross_module'): + bad = copy.deepcopy(data) + translated = bad['translated'] + implementation = translated['fun_decls'][0]['item_meta']['name'][2]['Impl'] + if kind == 'wrong_self': + translated['type_decls'][0]['item_meta']['name'][-1]['Ident'][0] = 'T' + elif kind == 'missing_self': + implementation['Ty']['skip_binder']['Deduplicated'] = 99 + elif kind == 'generic': + implementation['Ty']['params']['types'] = ['T'] + elif kind == 'trait': + implementation.clear() + implementation['Trait'] = 0 + else: + translated['type_decls'][0]['item_meta']['name'][1]['Ident'][0] = 'other' + llbc.write_text(json.dumps(bad)) + with self.subTest(kind=kind), self.assertRaises(ValueError): + inline.check_bindings(root, annotations, llbc) + + def test_generated_inherent_method_identity_and_module_agreement(self): + entry = {**ENTRY, 'rust': 'zerocopy::util::S::f', 'model': 'util.S.f'} + generated = ('module\nnamespace Zerocopy\n' + '/-- [zerocopy::util::{zerocopy::util::S}::f]:\n Source: location -/\n' + 'def util.S.f (x : Nat) :=\n x\n\nend Zerocopy\n') + models, _ = inline.split_live(generated, [entry]) + self.assertIn(entry['rust'], models) + with self.assertRaises(ValueError): + inline.split_live(generated.replace('{zerocopy::util::S}', '{zerocopy::other::S}'), [entry]) + if __name__ == '__main__': unittest.main() diff --git a/zerocopy/src/layout.rs b/zerocopy/src/layout.rs index d58786d637..58495316ad 100644 --- a/zerocopy/src/layout.rs +++ b/zerocopy/src/layout.rs @@ -490,6 +490,85 @@ impl DstLayout { #[must_use] #[inline] pub const fn pad_to_align(self) -> Self { + // ```aeneas + // model: + // def layout.DstLayout.pad_to_align + // (self : layout.DstLayout) : Result layout.DstLayout := do + // let (static_padding, size_info) ← + // match self.size_info with + // | layout.SizeInfo.Sized unpadded_size => + // do + // let padding ← util.padding_needed_for unpadded_size self.align + // let o ← lift (Usize.checked_add unpadded_size padding) + // match o with + // | none => fail panic + // | some size => ok (padding, layout.SizeInfo.Sized size) + // | layout.SizeInfo.SliceDst _ => ok (0#usize, self.size_info) + // if self.statically_shallow_unpadded + // then + // ok + // { + // self + // with + // size_info, statically_shallow_unpadded := (static_padding = 0#usize) + // } + // else ok { self with size_info } + // proof: + // contract pad_to_align_spec (self : layout.DstLayout) + // for layout.DstLayout.pad_to_align self + // requires h : match self.size_info with + // | layout.SizeInfo.Sized size => + // let S : Nat := size + // let A : Nat := self.align.val + // A.isPowerOfTwo ∧ S + (A - S % A) % A ≤ Usize.max + // | layout.SizeInfo.SliceDst _ => True + // ensures r => r.align = self.align ∧ match self.size_info with + // | layout.SizeInfo.Sized size => ∃ padded, + // r.size_info = layout.SizeInfo.Sized padded ∧ + // let S : Nat := size + // let A : Nat := self.align.val + // let R : Nat := padded + // R = S + (A - S % A) % A ∧ S ≤ R ∧ R < S + A ∧ R % A = 0 ∧ + // (∀ q : Nat, S ≤ q → q % A = 0 → R ≤ q) ∧ + // r.statically_shallow_unpadded = + // (self.statically_shallow_unpadded && decide (S % A = 0)) + // | layout.SizeInfo.SliceDst _ => r = self + // proof: + // unfold layout.DstLayout.pad_to_align + // cases hs : self.size_info with + // | SliceDst dst => + // simp only [hs] at h ⊢ + // cases hshallow : self.statically_shallow_unpadded <;> + // cases self <;> simp_all [bind_ok] + // | Sized size => + // simp only [hs] at h ⊢ + // obtain ⟨hpow, hroom⟩ := h + // step with padding_lt_alignment size self.align hpow as + // ⟨padding, hbound, hexact, haligned, hminimal, hzero⟩ + // have hbound := (UScalar.lt_equiv _ _).mp hbound + // have hadd := Usize.checked_add_bv_spec size padding + // cases hchecked : Usize.checked_add size padding with + // | none => + // simp only [hchecked] at hadd + // omega + // | some padded => + // simp only [hchecked] at hadd + // have hflag : (padding = 0#usize) = (size.val % self.align.val.val = 0) := by + // apply propext + // rw [← hzero] + // exact ⟨fun hp => by simp [hp], fun hp => UScalar.eq_of_val_eq (by simpa using hp)⟩ + // cases hshallow : self.statically_shallow_unpadded <;> + // simp only [lift, bind_ok, Bool.false_eq_true, if_false, if_true] + // all_goals + // refine ⟨rfl, padded, rfl, by omega, by omega, by omega, ?_, ?_, ?_⟩ + // · simpa only [hadd] using haligned + // · intro q hq hqa + // have := hminimal (q - size.val) (by + // rw [Nat.add_sub_of_le hq] + // exact hqa) + // omega + // · simp [hflag] + // ``` use util::padding_needed_for; let (static_padding, size_info) = match self.size_info { diff --git a/zerocopy/src/util/mod.rs b/zerocopy/src/util/mod.rs index 88a9705ade..b544a00082 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -171,17 +171,29 @@ pub(crate) const fn padding_needed_for(len: usize, align: NonZeroUsize) -> usize // proof: // contract padding_lt_alignment (len : Usize) (align : NonZeroUsize) // for util.padding_needed_for len align - // requires h : 0 < align.val.val - // ensures p => p.val < align.val.val + // requires h : (align.val : Nat).isPowerOfTwo + // ensures p => p < align.val ∧ + // let L : Nat := len + // let A : Nat := align.val + // let P : Nat := p + // P = (A - L % A) % A ∧ (L + P) % A = 0 ∧ + // (∀ q : Nat, (L + q) % A = 0 → P ≤ q) ∧ (P = 0 ↔ L % A = 0) // proof: + // have hpos := Nat.pos_of_isPowerOfTwo h // 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 + // simp only [lift, bind_ok, WP.spec_ok] + // have hbound : (~~~(core.num.Usize.wrapping_sub len 1#usize) &&& mask).val + // < align.val.val := by + // have := Nat.and_le_right (n := (~~~(core.num.Usize.wrapping_sub len 1#usize)).val) + // (m := mask.val) + // rw [UScalar.val_and] + // omega + // have haligned := Arithmetic.padding_mask_aligned len align.val mask h (by omega) + // obtain ⟨hexact, hminimal, hzero⟩ := + // Arithmetic.padding_properties _ _ _ hpos hbound haligned + // exact ⟨(UScalar.lt_equiv _ _).mpr hbound, hexact, haligned, hminimal, hzero⟩ // ``` #[cfg(kani)] #[kani::proof_for_contract(padding_needed_for)] @@ -286,27 +298,25 @@ pub(crate) const fn round_down_to_next_multiple_of_alignment( // proof: // contract round_down_spec (n : Usize) (align : NonZeroUsize) // for util.round_down_to_next_multiple_of_alignment n align - // requires hpos : 0 < align.val.val - // requires h : align.val.val.isPowerOfTwo - // ensures m => m.val ≤ n.val ∧ m.val % align.val.val = 0 + // requires h : (align.val : Nat).isPowerOfTwo + // ensures m => m ≤ n ∧ + // let N : Nat := n + // let A : Nat := align.val + // let M : Nat := m + // M = N - N % A ∧ M % A = 0 ∧ N < M + A ∧ + // (∀ q : Nat, q ≤ N → q % A = 0 → q ≤ M) // proof: + // have hpos := Nat.pos_of_isPowerOfTwo h // 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 + // have hexact := Arithmetic.round_down_exact n align.val mask h hval + // obtain ⟨hbound, haligned, hnext, hgreatest⟩ := + // Arithmetic.round_down_properties _ _ _ hpos hexact + // exact ⟨(UScalar.le_equiv _ _).mpr hbound, hexact, haligned, hnext, hgreatest⟩ // ``` #[cfg(kani)] #[kani::proof_for_contract(round_down_to_next_multiple_of_alignment)] @@ -349,15 +359,17 @@ pub(crate) const fn max(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { // proof: // contract max_spec (a b : NonZeroUsize) // for util.max a b - // ensures r => r.val.val = Nat.max a.val.val b.val.val + // ensures r => r.val = max a.val b.val ∧ (r = a ∨ r = b) ∧ + // a.val ≤ r.val ∧ b.val ≤ r.val // proof: - // apply WP.exists_imp_spec - // simp only [util.max, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + // simp only [util.max, core.num.nonzero.NonZero.get, bind_ok] // split // · rename_i h - // exact ⟨b, rfl, (Nat.max_eq_right (by omega)).symm⟩ + // exact WP.spec.ret ⟨(max_eq_right (le_of_lt h)).symm, Or.inr rfl, + // le_of_lt h, le_rfl⟩ // · rename_i h - // exact ⟨a, rfl, (Nat.max_eq_left (by omega)).symm⟩ + // exact WP.spec.ret ⟨(max_eq_left (le_of_not_gt h)).symm, Or.inl rfl, + // le_rfl, le_of_not_gt h⟩ // ``` if a.get() < b.get() { b @@ -391,15 +403,17 @@ pub(crate) const fn min(a: NonZeroUsize, b: NonZeroUsize) -> NonZeroUsize { // proof: // contract min_spec (a b : NonZeroUsize) // for util.min a b - // ensures r => r.val.val = Nat.min a.val.val b.val.val + // ensures r => r.val = min a.val b.val ∧ (r = a ∨ r = b) ∧ + // r.val ≤ a.val ∧ r.val ≤ b.val // proof: - // apply WP.exists_imp_spec - // simp only [util.min, core.num.nonzero.NonZero.get, bind_ok, UScalar.lt_equiv] + // simp only [util.min, core.num.nonzero.NonZero.get, bind_ok] // split // · rename_i h - // exact ⟨b, rfl, (Nat.min_eq_right (by omega)).symm⟩ + // exact WP.spec.ret ⟨(min_eq_right (le_of_lt h)).symm, Or.inr rfl, + // le_of_lt h, le_rfl⟩ // · rename_i h - // exact ⟨a, rfl, (Nat.min_eq_left (by omega)).symm⟩ + // exact WP.spec.ret ⟨(min_eq_left (le_of_not_gt h)).symm, Or.inl rfl, + // le_rfl, le_of_not_gt h⟩ // ``` if a.get() > b.get() { b From f7e72dcc608f6e370540395bd2c8c1a006a5ba07 Mon Sep 17 00:00:00 2001 From: Josh Liebow-Feeser Date: Fri, 2 Oct 2026 03:17:02 -0400 Subject: [PATCH 4/4] Normalize UI diagnostics using the selected compiler sysroot Use the compiler's actual sysroot, including custom RUSTUP_HOME installations, when normalizing source paths. Replace the broad path regex, which could consume preceding diagnostic lines, with exact path matching. Regenerate the affected MSRV, stable, and nightly snapshots through the UI runner. gherrit-pr-id: Gzdelmzn5y42ab3htat7lqrwovbusi5sh Validation: UI snapshot generation on MSRV, stable, and nightly; nightly workspace UI replay. --- tools/ui-runner/src/main.rs | 21 +- .../tests/ui/try_transmute_ref.nightly.stderr | 18 +- .../tests/ui/try_transmute_ref.stable.stderr | 18 +- .../tests/ui/struct.msrv.stderr | 262 +++++++++++++++++- 4 files changed, 312 insertions(+), 7 deletions(-) diff --git a/tools/ui-runner/src/main.rs b/tools/ui-runner/src/main.rs index 933bef1b3a..095ed784ca 100644 --- a/tools/ui-runner/src/main.rs +++ b/tools/ui-runner/src/main.rs @@ -10,6 +10,7 @@ use std::{ env, fmt::Debug, path::{Path, PathBuf}, + process::Command, }; use ui_test::{ @@ -37,6 +38,13 @@ fn main() { ); let toolchain = env::var("ZEROCOPY_UI_TEST_TOOLCHAIN") .expect("ZEROCOPY_UI_TEST_TOOLCHAIN must be set by tests/ui.rs"); + let sysroot = Command::new("rustc") + .env("RUSTUP_TOOLCHAIN", &toolchain) + .args(["--print", "sysroot"]) + .output() + .expect("failed to query the UI compiler's sysroot"); + assert!(sysroot.status.success(), "failed to query the UI compiler's sysroot"); + let sysroot = PathBuf::from(String::from_utf8(sysroot.stdout).unwrap().trim()); let root = env::current_dir().unwrap(); let mut config = Config::rustc(tests_dir.clone()); @@ -50,15 +58,20 @@ fn main() { let workspace_root = env::var("ZEROCOPY_WORKSPACE_ROOT").map(PathBuf::from).unwrap_or_else(|_| root.clone()); + // Normalize the selected compiler's actual source path, including a custom + // RUSTUP_HOME. Exact path matching also preserves neighboring diagnostics; + // a regex with [^/] could consume newlines before the source path. + config + .comment_defaults + .base() + .normalize_stderr + .push((sysroot.as_path().into(), b"$RUSTUP_TOOLCHAIN".to_vec())); + config.stderr_filter(&workspace_root.display().to_string(), "$$WORKSPACE"); if let Ok(canonical) = std::fs::canonicalize(&workspace_root) { config.stderr_filter(&canonical.display().to_string(), "$$WORKSPACE"); } - // Normalize paths to rustlib source code, which will differ between developer - // machines and CI runners. - config.stderr_filter(r"(/[^/]+)+/\.rustup/toolchains/[^/]+/", b"$$RUSTUP_TOOLCHAIN/"); - config.stderr_filter(&tests_dir.display().to_string(), "$$DIR"); if let Ok(canonical) = std::fs::canonicalize(&tests_dir) { config.stderr_filter(&canonical.display().to_string(), "$$DIR"); diff --git a/zerocopy/tests/ui/try_transmute_ref.nightly.stderr b/zerocopy/tests/ui/try_transmute_ref.nightly.stderr index 4401e6fc19..dc23c09f2f 100644 --- a/zerocopy/tests/ui/try_transmute_ref.nightly.stderr +++ b/zerocopy/tests/ui/try_transmute_ref.nightly.stderr @@ -1,5 +1,21 @@ error[E0308]: mismatched types - --> tests$RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/result.rs:561:5 + --> $DIR/try_transmute_ref.rs:19:33 + | + 19 | let _: Result<&mut u8, _> = try_transmute_ref!(&0u8); + | ^^^^^^^^^^^^^^^^^^^^^^^^ + | | + | types differ in mutability + | arguments to this enum variant are incorrect + | + = note: expected mutable reference `&mut u8` + found reference `&_` +help: the type constructed contains `&_` due to the type of the argument passed + --> $DIR/try_transmute_ref.rs:19:33 + | + 19 | let _: Result<&mut u8, _> = try_transmute_ref!(&0u8); + | ^^^^^^^^^^^^^^^^^^^^^^^^ this argument influences the type of `Ok` +note: tuple variant defined here + --> $RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/result.rs:561:5 | 561 | Ok(#[stable(feature = "rust1", since = "1.0.0")] T), | ^^ diff --git a/zerocopy/tests/ui/try_transmute_ref.stable.stderr b/zerocopy/tests/ui/try_transmute_ref.stable.stderr index de3630c06e..0dad3206a3 100644 --- a/zerocopy/tests/ui/try_transmute_ref.stable.stderr +++ b/zerocopy/tests/ui/try_transmute_ref.stable.stderr @@ -1,5 +1,21 @@ error[E0308]: mismatched types - --> tests$RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/result.rs:561:5 + --> $DIR/try_transmute_ref.rs:19:33 + | + 19 | let _: Result<&mut u8, _> = try_transmute_ref!(&0u8); + | ^^^^^^^^^^^^^^^^^^^^^^^^ + | | + | types differ in mutability + | arguments to this enum variant are incorrect + | + = note: expected mutable reference `&mut u8` + found reference `&_` +help: the type constructed contains `&_` due to the type of the argument passed + --> $DIR/try_transmute_ref.rs:19:33 + | + 19 | let _: Result<&mut u8, _> = try_transmute_ref!(&0u8); + | ^^^^^^^^^^^^^^^^^^^^^^^^ this argument influences the type of `Ok` +note: tuple variant defined here + --> $RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/result.rs:561:5 | 561 | Ok(#[stable(feature = "rust1", since = "1.0.0")] T), | ^^ diff --git a/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr b/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr index 6ef759542c..6358819d63 100644 --- a/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr +++ b/zerocopy/zerocopy-derive/tests/ui/struct.msrv.stderr @@ -1,7 +1,267 @@ error: this conflicts with another representation hint --> $DIR/struct.rs:210:11 | -210 | #[repr(C, C)] /$RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/mem/mod.rs:303:22 +210 | #[repr(C, C)] // zerocopy-derive conservatively treats these as conflicting reprs + | ^ + +error: must have a non-align #[repr(...)] attribute in order to guarantee this type's memory layout + --> $DIR/struct.rs:216:10 + | +216 | #[derive(IntoBytes)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: must have a non-align #[repr(...)] attribute in order to guarantee this type's memory layout + --> $DIR/struct.rs:223:10 + | +223 | #[derive(IntoBytes)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: must have a non-align #[repr(...)] attribute in order to guarantee this type's memory layout + --> $DIR/struct.rs:250:10 + | +250 | #[derive(IntoBytes)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: must have a non-align #[repr(...)] attribute in order to guarantee this type's memory layout + --> $DIR/struct.rs:270:10 + | +270 | #[derive(IntoBytes)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: cannot derive `Unaligned` on type with alignment greater than 1 + --> $DIR/struct.rs:302:11 + | +302 | #[repr(C, align(2))] + | ^^^^^ + +error: this conflicts with another representation hint + --> $DIR/struct.rs:308:8 + | +308 | #[repr(transparent, align(2))] + | ^^^^^^^^^^^ + +error: this conflicts with another representation hint + --> $DIR/struct.rs:317:16 + | +317 | #[repr(packed, align(2))] + | ^^^^^ + +error: this conflicts with another representation hint + --> $DIR/struct.rs:324:18 + | +324 | #[repr(align(1), align(2))] + | ^^^^^ + +error: this conflicts with another representation hint + --> $DIR/struct.rs:330:18 + | +330 | #[repr(align(2), align(4))] + | ^^^^^ + +error: must have #[repr(C)], #[repr(transparent)], or #[repr(packed)] attribute in order to guarantee this type's alignment + --> $DIR/struct.rs:334:10 + | +334 | #[derive(Unaligned)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `Unaligned` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: must have #[repr(C)], #[repr(transparent)], or #[repr(packed)] attribute in order to guarantee this type's alignment + --> $DIR/struct.rs:339:10 + | +339 | #[derive(Unaligned)] + | ^^^^^^^^^ + | + = note: this error originates in the derive macro `Unaligned` (in Nightly builds, run with -Z macro-backtrace for more info) + +error: this conflicts with another representation hint + --> $DIR/struct.rs:353:8 + | +353 | #[repr(C, packed(2))] + | ^ + +error: `crate` attribute requires a path as the value + --> $DIR/struct.rs:371:20 + | +371 | #[zerocopy(crate = "zerocopy_renamed"typo)] + | ^^^^^^^^^^^^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:377:20 + | +377 | #[zerocopy(crate = "Self::foo")] + | ^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:383:20 + | +383 | #[zerocopy(crate = "::crate::foo")] + | ^^^^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:389:20 + | +389 | #[zerocopy(crate = "foo::crate::bar")] + | ^^^^^^^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:395:20 + | +395 | #[zerocopy(crate = "foo::super::bar")] + | ^^^^^^^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:401:20 + | +401 | #[zerocopy(crate = "foo::Self::bar")] + | ^^^^^^^^^^^^^^^^ + +error: `crate` attribute requires a valid module path + --> $DIR/struct.rs:407:20 + | +407 | #[zerocopy(crate = "foo::self")] + | ^^^^^^^^^^^ + +error[E0692]: transparent struct cannot have other repr hints + --> $DIR/struct.rs:308:8 + | +308 | #[repr(transparent, align(2))] + | ^^^^^^^^^^^ ^^^^^^^^ + +error[E0277]: the size for values of type `[u8]` cannot be known at compilation time + --> $DIR/struct.rs:31:10 + | +31 | #[derive(KnownLayout)] + | ^^^^^^^^^^^ doesn't have a size known at compile-time + | + = help: within `KL00`, the trait `Sized` is not implemented for `[u8]` +note: required because it appears within the type `KL00` + --> $DIR/struct.rs:34:8 + | +34 | struct KL00(u8, NotKnownLayoutDst); + | ^^^^ + = help: see issue #48214 + = note: this error originates in the derive macro `KnownLayout` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the size for values of type `[u8]` cannot be known at compilation time + --> $DIR/struct.rs:38:10 + | +38 | #[derive(KnownLayout)] + | ^^^^^^^^^^^ doesn't have a size known at compile-time + | + = help: within `KL02`, the trait `Sized` is not implemented for `[u8]` +note: required because it appears within the type `KL02` + --> $DIR/struct.rs:41:8 + | +41 | struct KL02(u8, [u8]); + | ^^^^ + = help: see issue #48214 + = note: this error originates in the derive macro `KnownLayout` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `NotKnownLayoutDst: zerocopy_renamed::KnownLayout` is not satisfied + --> $DIR/struct.rs:45:10 + | +45 | #[derive(KnownLayout)] + | ^^^^^^^^^^^ the trait `zerocopy_renamed::KnownLayout` is not implemented for `NotKnownLayoutDst` + | + = help: see issue #48214 + = note: this error originates in the derive macro `KnownLayout` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `NotKnownLayout: zerocopy_renamed::KnownLayout` is not satisfied + --> $DIR/struct.rs:53:10 + | +53 | #[derive(KnownLayout)] + | ^^^^^^^^^^^ the trait `zerocopy_renamed::KnownLayout` is not implemented for `NotKnownLayout` + | + = help: see issue #48214 + = note: this error originates in the derive macro `KnownLayout` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `UnsafeCell<()>: zerocopy_renamed::Immutable` is not satisfied + --> $DIR/struct.rs:63:10 + | +63 | #[derive(Immutable)] + | ^^^^^^^^^ the trait `zerocopy_renamed::Immutable` is not implemented for `UnsafeCell<()>` + | + = help: see issue #48214 + = note: this error originates in the derive macro `Immutable` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `UnsafeCell: zerocopy_renamed::Immutable` is not satisfied + --> $DIR/struct.rs:70:10 + | +70 | #[derive(Immutable)] + | ^^^^^^^^^ the trait `zerocopy_renamed::Immutable` is not implemented for `UnsafeCell` + | + = note: required because of the requirements on the impl of `zerocopy_renamed::Immutable` for `[UnsafeCell; 0]` + = help: see issue #48214 + = note: this error originates in the derive macro `Immutable` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `AU16: zerocopy_renamed::Unaligned` is not satisfied + --> $DIR/struct.rs:120:10 + | +120 | #[derive(IntoBytes)] + | ^^^^^^^^^ the trait `zerocopy_renamed::Unaligned` is not implemented for `AU16` + | + = help: see issue #48214 + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `(): PaddingFree` is not satisfied + --> $DIR/struct.rs:129:10 + | +129 | #[derive(IntoBytes)] + | ^^^^^^^^^ the trait `PaddingFree` is not implemented for `()` + | + = help: the following implementations were found: + <() as PaddingFree> + = help: see issue #48214 + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the trait bound `(): PaddingFree` is not satisfied + --> $DIR/struct.rs:139:10 + | +139 | #[derive(IntoBytes)] + | ^^^^^^^^^ the trait `PaddingFree` is not implemented for `()` + | + = help: the following implementations were found: + <() as PaddingFree> + = help: see issue #48214 + = note: this error originates in the derive macro `IntoBytes` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the size for values of type `[u8]` cannot be known at compilation time + --> $DIR/struct.rs:158:10 + | +158 | #[derive(IntoBytes)] + | ^^^^^^^^^ doesn't have a size known at compile-time + | + = help: within `IntoBytes4`, the trait `Sized` is not implemented for `[u8]` +note: required because it appears within the type `IntoBytes4` + --> $DIR/struct.rs:163:8 + | +163 | struct IntoBytes4 { + | ^^^^^^^^^^ +note: required by a bound in `std::mem::size_of` + --> $RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/mem/mod.rs:303:22 + | +303 | pub const fn size_of() -> usize { + | ^ required by this bound in `std::mem::size_of` + = note: this error originates in the macro `::zerocopy_renamed::struct_padding` (in Nightly builds, run with -Z macro-backtrace for more info) + +error[E0277]: the size for values of type `[u8]` cannot be known at compilation time + --> $DIR/struct.rs:165:8 + | +165 | b: SliceU8, + | ^^^^^^^ doesn't have a size known at compile-time + | + = help: the trait `Sized` is not implemented for `[u8]` +note: required by a bound in `std::mem::size_of` + --> $RUSTUP_TOOLCHAIN/lib/rustlib/src/rust/library/core/src/mem/mod.rs:303:22 | 303 | pub const fn size_of() -> usize { | ^ required by this bound in `std::mem::size_of`