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..b74639215d --- /dev/null +++ b/tools/aeneas-inline/src/main.rs @@ -0,0 +1,176 @@ +// 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) + } + + 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<'_> { + 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) { + 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_impl_item_fn(self, item); + self.unsupported -= 1 + usize::from(generic); + } + + 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()")); + } + + #[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/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/verification/aeneas/README.md b/verification/aeneas/README.md new file mode 100644 index 0000000000..c4c5247f43 --- /dev/null +++ b/verification/aeneas/README.md @@ -0,0 +1,411 @@ + + +# 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 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` | 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. 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 +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 + +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: + // contract example_spec ... + // for example ... + // requires h : ... + // ensures r => ... + // proof: + // ... + // ``` + ... +} +```` + +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. + +The proof declaration may be an ordinary `theorem` or the experimental +`contract` command from `lean/Contracts.lean`. For example, a predicate-preserving +corollary uses this syntax: + +```lean +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 +``` + +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, +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 +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. + +`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. + +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 +`@@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. + +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 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 +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 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. +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, + 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 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, 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: 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. +`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/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/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..57374812ea --- /dev/null +++ b/verification/aeneas/inline.py @@ -0,0 +1,480 @@ +#!/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: + 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})*', + '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') + 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 + # 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] + 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() + 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') + 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(): + # 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'] + 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') + + +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']} + # 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'] + name = identity(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)) + + 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 = [] + 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' + 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[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:] + 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..8273e867d0 --- /dev/null +++ b/verification/aeneas/inventory.json @@ -0,0 +1,49 @@ +{ + "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", + "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/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 new file mode 100644 index 0000000000..c0b42939bd --- /dev/null +++ b/verification/aeneas/lean/Check.lean @@ -0,0 +1,60 @@ +/- 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 +import ContractTests +import Corollaries +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 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)) || + env.getModuleIdxFor? declName == some proofModule 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/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/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 new file mode 100644 index 0000000000..46a42c684a --- /dev/null +++ b/verification/aeneas/lean/Obligations.lean @@ -0,0 +1,65 @@ +/- 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 + +-- 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 ∧ (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 ∧ (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 : 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) + (_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 new file mode 100644 index 0000000000..fd70069664 --- /dev/null +++ b/verification/aeneas/lean/Proofs.lean.in @@ -0,0 +1,21 @@ +/- 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 +public import Contracts +public import Arithmetic +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..bddc7579be --- /dev/null +++ b/verification/aeneas/negative-controls.sh @@ -0,0 +1,354 @@ +#!/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 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" +} +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 + +# 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 + +# 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 +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'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") +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 + +# 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") +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..7ad8aac412 --- /dev/null +++ b/verification/aeneas/prepare.py @@ -0,0 +1,125 @@ +#!/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' + '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' + '@[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..e490121eb3 --- /dev/null +++ b/verification/aeneas/run.sh @@ -0,0 +1,97 @@ +#!/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 + 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. + 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..3df7154970 --- /dev/null +++ b/verification/aeneas/scaffolding/Funs.lean @@ -0,0 +1,89 @@ +/- 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::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")@@ + +/-- [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..c08bb078be --- /dev/null +++ b/verification/aeneas/scaffolding/Types.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. -/ + +-- 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 + +/-- [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/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..3bce35f408 --- /dev/null +++ b/verification/aeneas/tests/test_inline.py @@ -0,0 +1,338 @@ +# 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 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'), + 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_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' + '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) + + 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/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/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 50454af00c..b544a00082 100644 --- a/zerocopy/src/util/mod.rs +++ b/zerocopy/src/util/mod.rs @@ -153,6 +153,48 @@ 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: + // contract padding_lt_alignment (len : Usize) (align : NonZeroUsize) + // for util.padding_needed_for len align + // 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] + // 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)] fn proof() { @@ -237,6 +279,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: + // 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 ∧ + // 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] + // 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)] fn proof() { @@ -256,6 +337,40 @@ 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: + // contract max_spec (a b : NonZeroUsize) + // for util.max a b + // ensures r => r.val = max a.val b.val ∧ (r = a ∨ r = b) ∧ + // a.val ≤ r.val ∧ b.val ≤ r.val + // proof: + // simp only [util.max, core.num.nonzero.NonZero.get, bind_ok] + // split + // · rename_i h + // 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 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 } else { @@ -266,6 +381,40 @@ 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: + // contract min_spec (a b : NonZeroUsize) + // for util.min a b + // ensures r => r.val = min a.val b.val ∧ (r = a ∨ r = b) ∧ + // r.val ≤ a.val ∧ r.val ≤ b.val + // proof: + // simp only [util.min, core.num.nonzero.NonZero.get, bind_ok] + // split + // · rename_i h + // 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 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 } else { 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`