google-zerocopy

The MSRV for Zerocopy depends on which features you are using:

1. Without the derive feature: The MSRV is defined by the package.rust-version field in Cargo.toml. Increasing the MSRV is treated as a semver-breaking change (e.g., moving from 0.1 to 0.2).
2. With the derive feature (or using zerocopy-derive): The MSRV is inherited from the maximum MSRV of all dependencies. Note that because some dependencies (like syn) do not treat MSRV increases as semver-breaking, your effective MSRV might increase within a single semver version train.

Anneal provides a set of Lean axioms and type classes to reason about Rust's memory model, which is particularly useful for verifying unsafe code involving raw pointer manipulation or manual layout calculations.

Instead of modeling the entire Rust abstract machine, Anneal uses "lower-bound" guarantees from the Rust Reference, such as:

• Alignment: Sized types have a non-zero power-of-two alignment.
• Size: The size of a type is a multiple of its alignment.

These guarantees are encapsulated in the Anneal standard library. For example, the Layout class is used to model type layout:

class Layout (ɑ : Type) where
  size : Nat
  align : Nat
  validAlignment : Alignment align
  sizeAligned : size | align

Because proof context: is evaluated during structural instantiation (exact), it executes after the WPs are split. Crucially, this means it executes after the preconditions (Pre struct) have been destructured.

As a result, logic inside proof context: has full access to your user-defined requires hypotheses (e.g., h_positive). You can use these hypotheses to build shared setup logic for your ensures proofs.

Anneal uses a strict, indentation-sensitive parser. Whitespace is semantically significant.

• Any line indented further than the leading clause belongs to that clause.
• If you break an expression across multiple lines, every continuation line must be indented deeper than the line that started it.
• Block-Starting Keywords: Blocks must begin immediately with a recognized keyword (e.g., requires, ensures, context). Do not place comments (like -- TODO) at the top of the /// ```anneal block before the keyword, or parsing will fail.

/// ```anneal
/// requires:
///   let x = 5
///   let y =
///     x + 2
/// ```

The project follows specific directory structures for different types of tests:

• Unit Tests: Place in a mod tests module within the source file being tested.
• UI/Compile-Fail Tests (zerocopy): Place in tests/ui-* (top-level). The top-level tests/ directory is reserved exclusively for UI tests.
• UI/Compile-Fail Tests (zerocopy-derive): Place in zerocopy-derive/tests/ui-*.
• Derive Integration Tests: Place in zerocopy-derive/tests.
• Derive Output Tests: Place unit tests verifying generated code (token streams) in zerocopy-derive/src/output_tests.rs.

Bounds are mathematical properties defined within requires (preconditions), ensures (postconditions), or unsafe(axiom) clauses.

Anonymous Bounds

If you write an expression without a name, it is an anonymous bound. Anneal assigns it the name h_anon. Limitation: You may only have one anonymous bound per clause because Anneal collapses them into the same h_anon name.

Named Bounds

To use multiple bounds in a single clause, or to reference a bound in a proof, you must name them using the syntax (name): expression.

/// ```anneal
/// requires (h_x_positive): x > 0
/// requires (h_y_safe): y < 100
/// ```

/// ```anneal
/// requires:
///   x > 0
/// ```

Because Lean is purely functional, Aeneas cannot perform in-place mutation. Instead, it models mutable borrows (&mut T) by returning a tuple containing the original return value and the new state of the mutated variable.

Key Behavior:

• Structural Translation: A function like fn add_one(x: &mut u32) -> bool is translated into a Lean function returning Result (Bool × U32).
• Anneal Automation: When writing proofs, you do not need to manually handle the tuple. Anneal automatically binds the original input to the original name (e.g., x) and the modified output to a primed name (e.g., x').

// Rust
fn add_one(x: &mut u32) -> bool { ... }

-- Translated Lean structure (Conceptual)
def add_one (x : U32) : Result (Bool × U32) := ...

Anneal optimizes the Post structure for functions that return () (Unit) or ! (diverging/Never).

To avoid type-checking failures caused by Aeneas's tuple elision (where Unit is often removed from result tuples) and to prevent proof bloat, Anneal omits the ret parameter from the Post struct for these types. This allows Anneal to use the exact ⟨⟩ optimization, which instantly discharges the empty Post structure and prevents the proof context from being cluttered with useless ret bindings.

When passing Rust traits to Lean, do not use standard Lean implicit binders {}. Instead, use Strict Implicit Binders, written as {{ }} or ⦃ ⦄.

Why? Standard implicits ({}) cause Lean to eagerly synthesize typeclasses, which can cause the solver to panic on complex spatial traits (like HasStaticLayout). Strict implicits ({{ }}) delay synthesis until the trait is actively applied to a concrete value.

Warning: Do not refactor {{_sz: Sized Self}} to {_sz: Sized Self}, as this will break downstream proofs.

/// ```anneal
/// unsafe(axiom):
///   {{_sz: core::marker::Sized Self}}
/// ```

When performing a security audit in zerocopy, you must verify that all unsafe code is properly documented and justified.

Checklist:

• Every unsafe block must have a // SAFETY: comment.
• Every unsafe function, unsafe trait, and macro with safety preconditions must have /// # Safety documentation.
• All safety comments and documentation must comply with the rules defined in unsafe_code.md.

Note on TODOs: A // SAFETY: TODO comment or a /// TODO within a /// # Safety section is considered a valid placeholder. Do not flag these as missing safety justifications or critical issues, as they are intended to be resolved before merging.