zerocopy / v1

<!-- File: llms.txt -->

# Anneal Formal Verification Toolchain

> **Historical V1 documentation:** This document describes the prototype in
> `anneal/v1/`. It remains authoritative for using and maintaining V1, but it is
> not current Anneal design authority. See
> [`../PRINCIPLES.md`](../PRINCIPLES.md) for current project principles. Known
> differences are historical and need not be reconciled here.

> Anneal is a toolchain for formally verifying `unsafe` Rust code using Charon, Aeneas, and Lean 4, with a specific focus on memory layout and correctness boundaries.

**CRITICAL INSTRUCTION FOR AGENTS:** 
If you are new to Anneal, you **MUST** read the following documentation modules in strict, sequential order. Anneal proofs execute in a highly constrained environment (Orthogonal Weakest Precondition in Term Mode). If you attempt to guess tactics or skip these modules, you will fail.

## The Curriculum

1. **[Philosophy and Pipeline](docs/agent/01_philosophy_and_pipeline.md)**: Why Anneal exists, the Charon/Aeneas translation gap, and output directories (`target/anneal/<hash>`).
2. **[Rust to Lean Mapping](docs/agent/02_rust_to_lean_mapping.md)**: How Aeneas translates variables, the monadic `Result` environment, and the tuple destructuring of mutable borrows (`&mut T`).
3. **[Memory Model](docs/agent/03_memory_model.md)**: The "lower bound" axioms of physical memory, `Layout`, `Allocation`, `Referent`, and spatial inclusion (`FitsInAllocation`).
4. **[Specifications and Syntax](docs/agent/04_specifications_and_syntax.md)**: Annotation chains, the strict Python-style off-side indentation rules, strict implicit binders (`{{}}`), and bounds scoping.
5. **[Proof Architecture](docs/agent/05_proof_architecture.md)**: The most critical module. Explains Orthogonal WPs, `Pre`/`Post` struct derivation, Term Mode hygiene rules (why `simp_all` is illegal), and the `--allow-sorry` validation matrix.
6. **[Tactics and Tooling](docs/agent/06_tactics_and_tooling.md)**: A dictionary for `scalar_tac`, `<;>`, `Fin`, Aeneas APIs, and how to tell solver exhaustion from syntax errors.
7. **[Workflow](docs/agent/07_workflow.md)**: The recursive methodology for proving theorems, avoiding blind guessing, and using the `expand` command to evaluate the generated Lean models.

## Core Sources
[Anneal.lean](src/Anneal.lean) - The foundational Lean definitions and axioms that Anneal uses to verify memory.



<!-- File: docs/agent/01_philosophy_and_pipeline.md -->

# Module 1: Philosophy and Pipeline

Welcome to Anneal! Before you write your first specification or try to prove your first theorem, it's critical that you understand *what* Anneal is, *why* it exists, and *how* the mechanical pipeline works step-by-step. 

Without this mental model, you will struggle to debug issues, interpret errors, or understand why the tooling is structured the way it is.

## 1. The Functional Verification Gap 

### What are Charon and Aeneas?
Anneal does not translate Rust to Lean by itself. It delegates the heavy lifting of pure program verification to a pipeline consisting of two tools:
1. **Charon** parses your Rust code's Mid-level Intermediate Representation (MIR) and extracts it into an intermediate artifact called LLBC.
2. **Aeneas** reads that LLBC and performs a **purely functional translation**, emitting Lean 4 formal models.

Aeneas relies heavily on Rust's strict borrow-checker rules. Because safe Rust statically guarantees non-aliasing and immutability, Aeneas can structurally flatten your program into pure mathematical functions, entirely abstracting away raw physical memory, pointers, and manual spatial reasoning.

### The Unsafe Boundary
While Aeneas is incredibly powerful for *safe* Rust, its purely functional translation completely breaks down at the `unsafe` boundary. Aeneas cannot mathematically model a raw pointer (`*const T` or `*mut T`) or understand unsafe memory operations (like `ptr::read_unaligned()`), because these operations violate the functional abstraction of non-aliasing tree structures.

If Aeneas encounters an opaque external call or untranslatable unsafe operation, it emits it into Lean as an **opaque, uninterpreted axiom** (i.e. a function definition with no body).

### Why Anneal Exists
**This is exactly where Anneal comes in.** Anneal is designed specifically to bridge this functional verification gap. 

Anneal allows you to write inline mathematical specifications (preconditions and postconditions) for the safe wrappers around these unsafe operations. Anneal then acts as the glue:
1. It allows you to **axiomatize** the un-verifiable unsafe "leaf" operations that Aeneas cannot model functionally (using `unsafe(axiom)`).
2. It allows you to write the mathematical proofs that structurally define exactly what those opaque leaves do.
3. It relies on Aeneas to functionally verify the safe *glue code* and control flow that composes those leaves together.

In short, Anneal lets you enforce the mathematical safety of `unsafe` code at its boundary, enabling the rest of your crate to be verified using pure functional mathematics.

---

## 2. The Verification Pipeline

When you invoke Anneal via the CLI (e.g., `cargo run verify`), a complex pipeline executes behind the scenes. Understanding this pipeline is your most powerful tool for debugging.

1. **Extraction (Charon).** Anneal invokes Charon to parse your Rust codebase. 
   * **The `--start-from` Optimization:** Anneal tells Charon to only extract functions that actually carry `/// ```anneal` annotations and their transitive dependencies. You don't need to fear running Anneal on a massive crate—it automatically bounds the verification strictly to the dependency graph of the code you annotate.
2. **Translation (Aeneas).** Charon outputs an LLBC artifact. Anneal passes this artifact to Aeneas, which generates standard Lean 4 files modeling your Rust code functionally.
3. **Specification Generation (Anneal).** In parallel, Anneal's internal scanner reads your actual Rust source files, parses the mathematical specifications and proofs out of your `/// ```anneal` doc comments, and generates its own Lean file (usually called `<CrateName><Hash>.lean`).
4. **Compilation (Lake).** Anneal aggregates the Aeneas-generated functional models and its own Anneal-generated specifications, dropping them into isolated directories. It then invokes the Lean package manager (`lake`) to compile the proofs and check their mathematical correctness against the generated model.


<!-- File: docs/agent/02_rust_to_lean_mapping.md -->

# Module 2: Rust to Lean Mapping

Aeneas maps Rust concepts into pure mathematical models in Lean's standard library. Before writing specifications in Anneal, you must understand how your Rust variables mathematically exist inside Lean.

This module covers exactly how Rust code is structurally transformed.

## 1. Type Translation

When writing Lean specs, reference Aeneas types explicitly:

### Primitives
*   `u8`..`u128` → `Aeneas.Std.U8` .. `Aeneas.Std.U128`
*   `i8`..`i128` → `Aeneas.Std.I8` .. `Aeneas.Std.I128`
*   `usize` → `Aeneas.Std.Usize`
*   `isize` → `Aeneas.Std.Isize`
*   `bool` → `Bool`

### Strings and Text
*   `String` → `String`
*   `&str` → `str`
*   `char` → `char`

### Compound Types
*   `[T; N]` → `Aeneas.Array T N` (e.g., `[u32; 4]` → `Aeneas.Array Aeneas.Std.U32 4`)
*   `&[T]` → `Aeneas.Slice T` 
*   `(A, B)` → `A × B`

### Custom Types
*   **Structs**: Map to Lean `structure`.
*   **Enums**: Map to Lean `inductive`.
*   **Unions**: *Currently entirely unsupported by Aeneas.*

## 2. Pointers and References

Because Lean is purely functional, Aeneas must completely abstract memory away.

*   **Immutable References (`&T`, `&&T`)**: Flatten completely to the underlying value type `T`. Lean simply passes the value.
*   **Raw Pointers (`*const T`, `*mut T`)**: Map to `Anneal.ConstRawPtr T` and `Anneal.MutRawPtr T`. (See the Memory Model module for how to perform spatial reasoning on these).

### The Tuple Destructuring of Mutation (`&mut T`)
This is the most critical functional shift: **Aeneas models `&mut T` via state-updating transformations.** 

Because a pure function cannot mutate memory in-place, a Rust function taking or returning mutable borrows is structurally translated into a Lean function that returns a **tuple**. 
This tuple contains *both* the normal return value, and the new post-execution state of every mutated variable.

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

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

When you write proofs, you do not need to manually parse this tuple! Anneal intercepts it automatically and binds it to two distinct variables:
*   The original input is available as `x`.
*   The modified output is available as `x'`.

## 3. The Monadic Environment (`Result T`)

All functions translated by Aeneas return a monadic `Result T`, even if they cannot organically fail or panic in Rust. 

This is to mathematically model potential divergence (like division by zero, out-of-bounds panics, or infinite loops).
*   Functions returning `()` (Unit) map to `Result Unit`.
*   Functions returning `!` (Never) map structurally to a `Result` that inherently diverges (meaning it never resolves to `Result.ok`).

### Proving Correctness means Proving Success
When you write an `ensures` postcondition, you are inherently attempting to prove that the Aeneas `Result T` strictly resolves to `Result.ok T`. If your proof gets stuck, it frequently means that Lean believes there is a branch where your function panics or loops forever.

## 4. Aeneas Quirks & Workarounds

As Aeneas scales Rust to Lean, Anneal applies several structural patches that you must know about to avoid debugging bizarre errors.

### The Crate Namespace Translation
Aeneas generates top-level Lean modules using your package's name converted to `snake_case`. Anneal strictly adheres to this, explicitly converting hyphens (`-`) to underscores (`_`). 

**What this means for you:** If you are verifying a complex crate and need to manually unfold a function or reference an external definition, you must root it in this namespace (e.g. `unfold my_crate_name.my_function`).

### The Discriminant `isize` Hardcoding
When Aeneas translates Rust enumerations, it tags them with a `@[discriminant]` attribute for Lean's code generator. Because Aeneas omits the underlying type parameter, Anneal forcibly text-replaces this with `@[discriminant isize]`. 

**What this means for you:** If you use `#[repr(u8)]` or similar specialized tags on an enum, the Lean generated model still logically assumes the discriminant occupies an `isize` block of memory. This can lead to unexpected failures in sizing or alignment proofs for tightly packed structures.

### Opaque Functions and `noncomputable section`
Because `unsafe(axiom)` functions are translated into opaque Lean axioms (stubs with no bodies), Lean's bytecode compiler will aggressively reject the entire generated file if you attempt to build it. To suppress these errors, Anneal wraps the entirety of the generated `Funs.lean` file inside a `noncomputable section`.

**What this means for you:** You cannot use Lean's `#eval` command to test the runtime behavior of your verified functions computationally. They are strictly mathematical models.


<!-- File: docs/agent/03_memory_model.md -->

# Module 3: Memory Model

Anneal relies on pure functional translation for safe Rust, but safe Rust is ultimately just an abstraction over raw physical memory. When you write specifications for `unsafe` code—code that manipulates raw bytes and pointers—you must leave the functional world and reason spatially.

Anneal provides a mathematically rigorous model of physical memory for this exact purpose.

## 1. The "Lower Bound" Justification

Why does Anneal define its own memory model instead of using Aeneas's or Rust's?

Rust currently lacks a formalized "operational semantics"—an official, mathematically proven set of rules describing exactly what `rustc` is allowed to do with memory. Because this formal model doesn't exist, Anneal cannot assume *how* Rust structures its memory internally.

Instead, Anneal relies strictly on **minimal, universally guaranteed physical truths**. It models a "lower bound" of memory semantics—proving properties that must be physically true on any architecture, without making assumptions about compiler optimizations or undefined behavior flags that aren't strictly specified by Rust.

## 2. Core Abstractions Revealed

To reason about memory, you interact with several core Lean abstractions defined in `Anneal.lean`. While you don't always instantiate these directly, they form the basis of all spatial invariants.

### Layouts
Every type has a layout: a size and an alignment constraint. Anneal distinguishes between mathematical layouts (unbounded) and physical layouts (bounded by the address space).

```lean
/-- A mathematically idealized memory layout (size can exceed Usize::MAX) -/
structure SpecLayout where
  size : Nat
  align : Alignment
  sizeAligned : align.val.val ∣ size

/-- A valid physical memory layout (bounded by the machine's address space) -/
structure Layout where
  size : Usize
  align : Alignment
  sizeAligned : align.val.val ∣ size.val
```
Anneal provides typeclasses like `HasStaticLayout T` to automatically retrieve the `Layout` for any sized type `T`.

### Allocations and Referents
An **Allocation** represents a contiguous block of memory requested from the OS or allocator. A **Referent** represents the specific slice of memory that a pointer is allowed to address.

Crucially, Anneal represents the addressable space not just as a `base` and `size`, but as a mathematical `Set Nat`.

```lean
/-- Represents a Rust allocation (e.g. from Box, Vec, or static memory) -/
structure Allocation where
  base : Usize
  size : Usize
  addresses : Set Nat
  base_not_null : base.val ≠ 0
  size_le_isize_max : size.val ≤ Isize.max
  base_add_size_le_usize_max : base.val + size.val ≤ Usize.max
  bounds : ∀ a ∈ addresses, base.val ≤ a ∧ a < base.val + size.val

/-- The region of memory a specific pointer addresses -/
structure Referent where
  address : Usize
  size : Usize
  addresses : Set Nat
  addresses_are_usizes : ∀ a ∈ addresses, a ≤ Usize.max
  bounds : ∀ a ∈ addresses, address.val ≤ a ∧ a < address.val + size.val
```

## 3. The Four Principles of the Memory Model

When writing memory specifications (such as for a raw pointer wrapper), your proofs will rely on the following four principles:

### Principle 1: Mathematical vs Physical Separation
Anneal strictly separates mathematical models from physical representations.
*   Physical properties (like an address) are bounded (`Usize`, `Isize`).
*   Mathematical properties (like the `addresses : Set Nat`) use unbounded integers (`Nat`, `Int`) to prevent overflow reasoning during logical proofs. 

It is sometimes useful to convert bounded machine integers to `Nat` or `Int` using `.val` before doing arithmetic in your proofs.

> [!TIP]
> **Numerical Literal Suffixes (`#usize`):** Because memory modeling differentiates physical sizes from mathematical sizes, Lean will often raise ambiguity errors when you use bare numbers. You must often suffix numerical literals (e.g., `0#usize`) to explicitly specify their type class.

### Principle 2: Typeclass Automation
Instead of manually passing layout sizes and alignments, Anneal uses Lean's typeclass resolution (`[HasStaticLayout T]`) to implicitly carry physical bounds. You rarely construct a `Layout` manually; you lean on the generator to provide `HasStaticLayout T` and use `size_of T` or `align_of T`.

If you *must* manually instantiate typeclasses for a custom proof or lemma:
*   **Empty Typeclasses:** Some marker traits like `Sized` translate to empty typeclasses in Lean. You can legally instantiate them dynamically using the anonymous constructor `⟨⟩` (e.g., `have h_sized : Anneal.core.marker.Sized T := ⟨⟩`).
*   **Complex Layouts:** For complex typeclasses like `HasStaticLayout`, Lean's inference struggles with fully anonymous instantiations (e.g. `⟨_, _⟩`). If you need to manually construct one, you must alias it to a named `have` binding first before using it (e.g. `have h_layout : Anneal.HasStaticLayout T := { ... }`).

### Principle 3: Spatial Inclusion (The `FitsInAllocation` Axiom)
To prove that a pointer is safe to read or write, you must prove that its `Referent` (the memory it wants to touch) is physically contained within a valid `Allocation`.
Anneal formalizes this spatial relationship:
```lean
def FitsInAllocation (r : Referent) (a : Allocation) : Prop :=
  r.addresses ⊆ a.addresses ∧
  a.base.val ≤ r.address.val ∧ r.address.val + r.size.val ≤ a.base.val + a.size.val
```
If your `unsafe` code offsets a pointer, your specification must prove that the new `Referent` still satisfies `FitsInAllocation`.

### Principle 4: Logical Reflection (Contiguity)
Just because a pointer has a base address and a size does not mean the memory within that range is completely addressable (due to padding, uninitialized bytes, or fragmentation). To perform a bulk read/write, you must prove the memory is continuous:
```lean
def Referent.IsContiguous (r : Referent) : Prop :=
  ∀ a, r.address.val ≤ a ∧ a < r.address.val + r.size.val → a ∈ r.addresses
```
This is the heart of spatial reasoning in Anneal: mapping abstract types to their contiguous byte-level realities and ensuring they never violate the bounds of their parent `Allocation`.


<!-- File: docs/agent/04_specifications_and_syntax.md -->

# Module 4: Specifications and Syntax

Anneal specifications are written directly in your Rust source code using specialized documentation comments. Anneal parses these comments, extracts the mathematical logic, and weaves them into the Lean models generated by Aeneas.

## 1. Annotation Chains

To attach a specification to a function, struct, or trait, write a `///` doc-comment block immediately preceding the definition.

The block must begin with the `anneal` language string.
```rust
/// ```anneal
/// requires:
///   ...
/// ```
fn my_function() {}
```

### Proof vs Axiom Mode
By default, Anneal assumes all blocks are *proven* specifications (`spec` mode). You can optionally be explicit:
*   `/// ```anneal, spec` (The default. Requires a proof.)
*   `/// ```anneal, unsafe(axiom)` (Used when no proof is given.)

You may see other prefixes like `lean, anneal, spec` or `lean, anneal`. Anneal ignores everything strictly before `anneal`. The `lean` prefix is often added purely to trigger syntax highlighting in modern IDEs.

### The `context:` Block
In addition to attaching specs directly to items, you can define a standalone block that injects raw Lean code *outside* the theorem body entirely. This is used to define global helper lemmas, instances, or definitions that a theorem might need.
```rust
/// ```anneal
/// context:
///   lemma my_helper_lemma () : True := by trivial
/// ```
```

## 2. The Off-Side Rule (Indentation)

Anneal uses a strict, indentation-sensitive parser (similar to Python or YAML). **Whitespace is semantically significant.**

The rule is simple: **Any line that is 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.

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

**Fatal Error:**
```rust
/// ```anneal
/// requires:
///   let x = 5
///   let y =
///   x + 2    <-- ERROR: Not indented deeper than `let y =`
/// ```
```

### Block-Starting Keywords
Because of the strict parser, Anneal blocks must begin immediately with a recognized keyword (like `requires`, `ensures`, or `context`). Placing a comment (like `-- TODO`) at the top of the `/// ```anneal` block *before* a keyword will cause a parsing error.

## 3. Strict Implicit Binders (`{{ }}`)

When defining specifications that rely on Rust traits, you will frequently need to pass those traits to Lean dynamically. Lean uses implicit binders `{}` to automatically synthesize typeclasses.

However, Anneal explicitly disables standard implicits in favor of **Strict Implicit Binders**, written as `{{ }}` or `⦃ ⦄`.

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

**Why is this required?**
Standard implicits (`{}`) instruct Lean to eagerly guess and synthesize the typeclass immediately when the function is evaluated. For complex spatial traits (like `HasStaticLayout`), this eager synthesis often panics the solver before the proof even begins.
Strict implicits (`{{ }}`) politely instruct Lean to *delay* synthesis until the exact moment the trait is actively applied to a concrete value.

If you are refactoring a Anneal spec, do not replace `{{_sz: Sized Self}}` with `{_sz: Sized Self}`. You will likely break downstream proofs invisibly.

## 4. Bounds and Scoping

Specifications are defined using three primary clauses: `requires` (preconditions), `ensures` (postconditions), and `unsafe(axiom)` (un-verifiable trust boundaries).

Inside these clauses, you define **bounds**. A bound is a mathematical property that must be proven true.

### Anonymous Bounds
If you simply write an expression, you are defining an anonymous bound.

```rust
/// ```anneal
/// requires:
///   x > 0
/// ```
```
This requires that `x > 0`. Internally, Anneal names this bound `h_anon`.

**The Singleton Limit:** Because Anneal collapses anonymous bounds into `h_anon`, **you may only have one anonymous bound per clause.** If you have multiple requirements, you must name them.

### Named Bounds
If multiple `requires` or `ensures` bounds are required, they must be named:

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

Naming your bounds is critical for two reasons:
1. It bypasses the `h_anon` singleton limit.
2. It allows you to explicitly reference the proven hypothesis (like `h_x_positive`) in downstream proofs or custom lemmas. Any name you provide here becomes an active variable in the local Lean context during verification.

## 5. Axioms and FFI

A specification provided with `unsafe(axiom)` tells Aeneas to skip analyzing the body of the function. Anneal will accept the specification without generating a proof obligation for the implementation body.

```rust
/// ```anneal, unsafe(axiom)
/// requires: a.val + b.val <= Usize.max
/// ensures: ret.val = a.val + b.val
/// ```
pub unsafe fn fast_add(a: usize, b: usize) -> usize {
    // ...
}
```

## 6. Type and Trait Invariants

In addition to function-level pre- and post-conditions, Anneal allows you to define structural properties of types and traits.

### `isValid`

> [!WARNING]
> `isValid` annotations are currently unsound. To use them, you must provide the `--unsound-allow-is-valid` flag to Anneal.

`isValid` defines a structural invariant for a type.

```rust
/// ```anneal
/// isValid self := self.val.val > 0
/// ```
pub struct PositiveUsize {
    val: usize,
}
```

Under the hood, this implements the `Anneal.IsValid` typeclass for that struct. Furthermore, when you use `PositiveUsize` in a function signature, Anneal **automatically injects `h_valid` arguments and returns** into the generated specs, ensuring the invariant is upheld continuously.

### `isSafe`

`isSafe` defines an invariant for an `unsafe` trait (e.g., enforcing that implementing types have an alignment of exactly 1).

```rust
/// ```anneal
/// isSafe : ∀ {{_sz : Anneal.core.marker.Sized Self}} {{tl : Anneal.HasStaticLayout Self}},
///   tl.layout.align.val.val = 1
/// ```
pub unsafe trait Unaligned: Sized {}
```

Implementers of the `unsafe trait` must provide a proof of `isSafe`.

**Crucially**, generic functions bounding on the trait (e.g., `fn foo<T: Unaligned>()`) **do not** automatically receive this mathematical assumption in their preconditions, because the trait bound alone does not prove the invariant holds in a generic context. You must explicitly request the `isSafe` property in your `requires` block (see Module 6 for how to consume and apply trait bounds).

# Appendix: Full Syntax Reference


## Syntax

Anneal annotations are a sequence of indentation-sensitive (Python-style) blocks:

````rust
/// ```anneal
/// requires: x > 0
/// ensures:
//     ret = x + 1
/// proof:
///   ...
/// ```
````

## Block Types

The full list of blocks is:
- `context`: Context used by all blocks
- `requires`: Pre-conditions
- `ensures`: Post-conditions
- `proof context`: Lemmas or other items used by multiple proofs
- `proof`: Proofs of post-conditions
- `isValid`: Type invariants
- `isSafe`: Trait invariants

## Named and Anonymous Bounds

`requires`, `ensures`, and `proof` define or discharge bounds. They can be anonymous or named:

````rust
/// ```anneal
/// requires (h_x_pos): x > 0
/// requires (h_even): x % 2 == 0
/// ensures: ret = x + 2
/// proof:
///   ...
/// ```
````

Bounds are namespaced to either pre-conditions or post-conditions. An anonymous proof is combined with an anonymous post-condition.

## `isValid` and `isSafe`

`isValid` defines invariants for a type. Its syntax is a (boolean) Lean function:

````rust
/// ```anneal
/// isValid self := self.x.val > 0
/// ```
````

`isSafe` defines invariants for an unsafe trait.

````rust
/// ```anneal
/// isSafe :
///   ∀ (self : Self), True
/// ```
````

## Axioms

A specification can be axiomatic, in which case a proof is not given. Note the `unsafe(axiom)` token.

````rust
/// ```anneal, unsafe(axiom)
/// requires: b.val > 0
/// ensures: ret.val = a.val / b.val
/// ```
pub unsafe fn safe_div(a: u32, b: u32) -> u32 { unsafe { a / b } }
````

## Implicit Variables

**`ret`**: The return value of the function, assuming it returns (doesn't panic or loop forever).

**`arg'`**: The value of the referent of a mutable reference `arg: &mut T` after the function returns.

## Implicit Bounds & Hypotheses

Anneal automatically defines or injects the following structural names.

**`h_anon`**: The singleton name assigned to an anonymous `requires` or `ensures` block. These are namespaced to either pre-conditions or post-conditions, so they don't conflict.

````rust
/// ```anneal
/// requires: x > 0        -- Named `h_anon`
/// ensures: ret = x + 1   -- Named `h_anon`
/// proof:                 -- Proves `h_anon`
///   ...
/// ```
````

**`h_<arg>_is_valid`**: An auto-injected precondition asserting that the argument `arg` satisfies its type invariant (`isValid`).

````rust
/// ```anneal
/// requires (h_x_is_valid): isValid x -- Don't actually write this; it's implicit
/// ```
fn foo(x: MyType) {}
````

**`h_<arg>'_is_valid`**: An auto-injected postcondition asserting that a mutable reference `arg` satisfies its type invariant after the function returns.

````rust
/// ```anneal
/// ensures (h_x'_is_valid): isValid x' -- Don't actually write this; it's implicit
/// proof (h_x'_is_valid):
///   ... -- Prove the postcondition
/// ```
fn foo(x: &mut MyType) {}
````

**`h_ret_is_valid`**: An auto-injected postcondition asserting that the return value satisfies its type invariant.

````rust
/// ```anneal
/// proof (h_ret_is_valid):
///   ...
/// ```
fn foo() -> MyType {}
````

**`h_progress`**: The statement that the function terminates without panicking.

````rust
/// ```anneal
/// proof (h_progress):    -- Prove execution doesn't fail (e.g. divide by zero) or loop forever
///   ...
/// ```
fn safe_div(x: u32, y: u32) -> u32 {}
````

**`h_returns`**: The hypothesis binding the successful evaluation of the function to the implicitly-available values `ret`, `arg'`, etc.

````rust
/// ```anneal
/// ensures (h_res): ret = x + y
/// proof (h_res):
///   -- `h_returns` is in scope here
///   ...
/// ```
pub fn add(x: u32, y: u32) -> u32 { x.wrapping_add(y) }
````

Because we prove progress and correctness separately, our correctness proof is *actually* a proof of correctness *conditional on progress*. `h_returns` is this condition: it asserts that the function call successfully evaluated to the values available in the proof context (`ret`, `x'`, etc.).

The values available in the proof context are automatically destructured for you:
*   `ret`: The final return value of the function.
*   `x'`, `y'`, etc.: The post-states of any mutable references passed to the function.


<!-- File: docs/agent/05_proof_architecture.md -->

# Module 5: Proof Architecture

The biggest conceptual hurdle in Anneal is understanding *how* your proofs are mathematically structured and evaluated. 

If you try to write proofs by blindly guessing tactics, you will fail. You must understand the engine. This module explains the "Orthogonal WP" architecture and the strict "Term Mode" hygiene rules that govern Anneal proofs.

## 1. Orthogonal WP Proofs

Aeneas generates verification goals using **Weakest Preconditions (WP)**. In a standard WP framework, you step through the execution of a function line-by-line. If the execution gets "stuck" (e.g., you can't prove a loop terminates or a division is safe), the entire proof halts. 

Anneal uses a custom architecture called **Orthogonal WP**.

Orthogonal WP mathematically decouples the proof into two completely independent goals:
1.  **Progress (`h_progress`):** Proving that the `Result T` successfully resolves to `.ok` (i.e., the function doesn't panic, loop forever, or violate Rust rules).
2.  **Correctness (`h_returns`):** Proving that the *returned values* satisfy your `ensures` bounds and `isValid` invariants.

**Why is this important?** 
Because they are orthogonal, *Anneal allows you to write the correctness proof even if the progress proof fails.* This means that missing termination proofs no longer block you from verifying your actual logical invariants.

## 2. The Verification Environment

When Anneal generates a theorem for your function, it sets up an incredibly convenient environment for you before your custom `proof context:` even begins. 

You do not start with a blank slate. Anneal automatically performs:

### State Setup (`Pre`)
Anneal aggregates all your `requires` bounds, `unsafe(axiom)` traits, and implicit type invariants into a `Pre` struct. It then automatically destructured this struct via an `rcases` tactic.
**Result:** Every named precondition (e.g., `h_x_positive`) is immediately available as a free variable in your local Lean context. You do not need to use `intro` to bring preconditions into scope.

### State Capture (`h_returns`)
Anneal intercepts the final execution tuple (which contains both the standard return value and the post-state of all mutated `&mut` borrows) and binds it.
**Result:** Mutated inputs are available as `var'` (e.g., `x'`), and the final return value is available as `ret`. 

> [!TIP]
> **Zero-Sized Return Optimization:** If your function returns `()` or `!`, Anneal completely eliminates `ret` from the environment. There is no `ret` variable to prove things about!

## 3. The `Post` Struct

When you provide a manual proof for a named bound, you write it in a block like this:
```rust
/// ```anneal, proof
/// proof (h_my_bound):
///   scalar_tac
/// ```
```

Internally, Anneal aggregates all your postconditions and invariants into a struct called `Post` containing proofs of all post-conditions. Your proof blocks are literally injected into the `exact { ... }` instantiation of this struct using `:= by`.

```lean
-- Conceptual Anneal internal structure
exact {
  h_ret_is_valid := by verify_is_valid ...
  h_my_bound := by <YOUR PROOF TEXT HERE>
}
```

Because Anneal separates *progress* and *correctness* proofs, **you cannot use `progress` or `eval_progress`** inside these fields.

## 4. Omitting Proofs

Anneal provides `autoParam` macros that automatically attempt to solve missing proofs (e.g., `verify_is_valid`, `verify_user_bound`). If you do not provide a `proof:` block for an `ensures` clause, Anneal uses these macros to try `simp_all` and `scalar_tac` for you.

### The `--allow-sorry` Trap

You can run Anneal with `--allow-sorry` to temporarily skip failing proofs. 

**Understand exactly what this does:** It simply configures the `autoParam` macros to degrade to a `sorry` axiom if they fail. 

**What it does NOT do:** It does *not* magically silence syntax errors or broken logic in your manual `proof:` blocks. If you write:
```rust
/// ```anneal, proof
/// proof (foo):
///   some_garbage_tactic_that_doesnt_exist
/// ```
```
This will *still fail to compile* even with `--allow-sorry`. 


<!-- File: docs/agent/06_tactics_and_tooling.md -->

# Module 6: Tactics and Tooling

While Anneal completely abstracts the boilerplate of theorem generation, you still need to write the mathematical proofs for your `requires` and `ensures` bounds. 

This module serves as a survival dictionary for the most common Lean 4 tactics and Aeneas APIs you will encounter.

## 1. The Core Tactics

### `scalar_tac`
This is Aeneas's custom arithmetic solver, and arguably the most important tactic in Anneal. 
*   **What it does:** It automatically proves linear arithmetic inequalities and equalities involving bounded integers (e.g., `Usize.val ≤ Usize.max`). It natively understands the `.val` unwrapping of Aeneas primitives.
*   **When to use it:** Almost constantly. If a bound is purely arithmetic (e.g., proving an index is within a slice length, or an offset doesn't overflow `isize`), `scalar_tac` solves it.
*   **Limitations:** It only handles linear arithmetic (addition, subtraction, multiplication by constants). If your proof involves non-linear arithmetic (like `x * y > z` or modulo operations), `scalar_tac` will fail and you must manually apply algebraic theorems before calling it.

### `simp_all`
The "simplify all" tactic.
*   **What it does:** It aggressively applies all known `@[simp]` lemmas in the environment to simplify your goal and your hypotheses, and attempts to close trivial goals.
*   **When to use it:** When setting up a custom lemma or when you need to unroll complex structure definitions into simpler boolean propositions.

### `intro`
*   **What it does:** When your goal is a function or an implication (e.g., `A → B`), `intro x` takes `A` from the goal, assumes it is true, and adds it to your local context as hypothesis `x`, leaving `B` as the new goal.
*   **When to use it:** Primarily when writing custom lemmas or manual WP progress proofs that involve implications, or when unpacking the `Option`/`Result` matching logic. (Note: You do not need `intro` for your preconditions; Anneal natively destructured them into your context using `rcases`).

### `eval_progress` / `progress`
*   **What they do:** These tactics "step" through the Aeneas Weakest Precondition (WP) evaluator. If you have a sequence of statements in a function, `progress` handles the WP extraction to move execution to the next line of code.
*   **WARNING IN ANNEAL:** Due to Orthogonal WP (see Module 5), the progress goal evaluates entirely independently from your correctness `proof:` blocks, using the generated `eval_progress` tactic. You cannot use `progress` inside a Correctness proof because the WP state is already destructured. If `eval_progress` fails to automatically discharge the Progress goal, you must manually use `progress` inside an explicit `proof (h_progress):` block.

## 2. Tactic Combinators

### `<;>` (The "And Then" Combinator)
You will often see tactics chained together like `cases x <;> simp_all`.
*   **What it does:** `A <;> B` applies tactic `A` to the current goal. If `A` splits the goal into multiple subgoals (like branching on an `if` statement or an `enum`), it then immediately applies tactic `B` to **every single resulting subgoal**.
*   **Why it's powerful:** It instantly prunes impossible error states. If you split a `Result` into `.ok` and `.fail`, running `<;> simp_all` will usually instantly solve and close the impossible `.fail` branch, leaving you to focus solely on the `.ok` branch.

## 3. Essential Aeneas APIs

When writing specifications, you will inevitably interact with definitions from Aeneas's standard library.

### `Usize` Bounds for Slices
*   **What it is:** While purely mathematical arrays might be indexed with strictly bounded types (like `Fin n`), Aeneas models Rust slice and array indices natively using machine integers (e.g., `Usize`).
*   **Why it matters:** When indexing into a slice, Aeneas enforces the bounds logically via function preconditions (e.g., `0 <= i.val` and `i.val < slice.length`) rather than at the type level. You use `scalar_tac` to transparently discharge these bound assertions.

### `Aeneas.Std.bind_tc_ok`
*   **What it is:** A fundamental `@[simp]` theorem in Aeneas (`(do let y <- .ok x; f y) = f x`).
*   **Why it matters:** If you are forced to manually step through a monadic sequence, `bind_tc_ok` simplifies the bind operation downward *after* you have already proven that the preceding statement evaluated to `.ok`. It allows you to seamlessly "fast-forward" the simulated execution.

### `spec_imp_exists`
*   **What it is:** A foundational `theorem` (`Aeneas.Std.WP.spec_imp_exists`) for Weakest Preconditions.
*   **Why it matters:** When resolving the Orthogonal WP Progress goal, you must prove that there *exists* a valid return value `y` such that `test = ok y`. This theorem converts standard WP `spec` constraints into the existential proof required to close that goal.

## 4. Troubleshooting: Exhaustion vs Syntax

If a proof compilation fails, you must immediately diagnose whether it is a **solver exhaustion** or a **syntax error**.

**Solver Exhaustion (`autoParam` failure):**
*   **Symptom:** The error output complains about `autoParam` failing, or says something like *"Missing explicit proof for named bound... Lean cannot automatically prove that this value satisfies the `isValid` type invariant."*
*   **Cause:** The Anneal auto-solver (`verify_user_bound` or `verify_is_valid`) attempted to use `scalar_tac` and `simp_all`, but got stuck. 
*   **Fix:** You must provide a manual `proof (bound_name):` block to hold Lean's hand through the logic.

**Syntax / Tactic Errors:**
*   **Symptom:** The error points specifically at a line *inside* your `proof:` block and complains about "unknown identifier", "unexpected token", or "tactic failed".
*   **Cause:** You wrote invalid Lean syntax, you used a tactic that doesn't apply to the current goal state (like `progress` inside a correctness block), or your Python-string indentation is incorrect.
*   **Fix:** Fix the syntax. Remember that `--allow-sorry` will **not** save you from these errors. If you just want to skip the failing proof entirely, you must delete the entire `proof:` block.


<!-- File: docs/agent/07_workflow.md -->

# How to write an Anneal proof

This document contains advice on how to structure your thinking and workflow when writing Anneal proofs.

## Philosophy

Writing a Lean proof is not like other forms of software engineering. A Lean proof is *far* more brittle than a "normal" program. Starting with a complete draft and iterating **will not work**. You will never know whether you are going down blind alleys and spinning your wheels or making real progress. This approach will lead to frustration and wasted time, and likely won't produce a working proof.

## Workflow

The following is a workflow for solving [problem]. It is recursive – you will use this workflow to solve sub-problems as well.

1. Make sure you understand your goal, context, and constraints for [problem] *completely* and *precisely*.
    1. Spend as much time as you need *thinking* in order to come to this understanding.
    2. If there is any ambiguity whatsoever, ask for clarification.
    3. Repeat the process of clarification-asking and thinking until you have a *complete* and *precise* understanding of your goal, context, and constraints.
    4. Record this in as much details as you can in comments the file you are editing.
2. Once you understand the goal, context, and constraints for [problem], brainstorm a *complete* solution. Your solution must be *complete*, as the act of thinking through details may make you realize that you need to adjust your high-level plan.
    1. Spend as much time as it takes to think through your solution *completely* until you are confident that *every detail* is correct.
    2. Record this in as much details as you can in comments the file you are editing.
3. You are now ready to start writing code.
    1. Start with the specification (`requires` and `ensures` clauses).
    2. Get these working with the `verify` subcommand and the `--allow-sorry` flag, omitting any proofs.
    3. Iterate until everything verifies, implying that your specification is internally consistent. This does not necessarily mean that it's the *right* specification, only that Anneal understands it.
    4. Run the `expand` subcommand to see what Lean is generated, and make sure it looks like what you expect. This will help you when you start writing proofs.
4. Move on to the proof.
    1. First, break the proof down into lemmas. Spend as much time as you need thinking through the lemmas and how they fit together to prove the main proof.
    2. Write the *definitions* of each lemma, but do *not* prove them – leave their proofs as `sorry` for now.
5. Write the top-level proof, using the lemmas you defined in the previous step.
    1. Iterate until this proof verifies, using the `--allow-sorry` flag.
    2. If you get stuck *at all*, consider whether you need to re-visit a previous step or "pop up" one level of abstraction to reconsider your broader plan.
6. Once the top-level proof verifies, you can start proving the lemmas one by one. For each lemma, you will use *this entire workflow*, but applied to [sub-problem] instead of the top-level [problem].

Overall, your workflow will look like a recursive application of this entire workflow. Always be prepared to "pop up" one level of abstraction to reconsider your broader plan.

## Tips

When writing a proof, follow these tips:

1. Always *think deeply* before writing any code.
2. Question *all* assumptions.
3. Make liberal use of scratch `.lean` files to test out ideas.
4. The `expand` subcommand will print the generated Lean, and is *extremely* helpful in debugging.
5. If something isn't working, don't assume you know why. Instead, **STOP**. Move into debugging mode, producing a stand-alone experiment to confirm *all* your assumptions before continuing.
6. Specifications can have bugs too. Always consider whether a specification needs to be adjusted to match your understanding of the problem.
7. Proofs are more tractable when the proofs themselves and the code they model are broken down into small bits. If you are having trouble with a proof, consider breaking it further down into lemmas, or breaking the *code* that it models into smaller functions, types, etc.
8. Write extensive notes in code comments. Write notes to record your plans, what you've tried, what you've learned, what you still don't understand, etc.

## Specifics

You will use these two commands to interact with Anneal. Both accept `--help`.

1. Run `cargo run verify` to verify a target.
2. Use `cargo run expand` to see the generated Lean code.
3. Use `cargo run generate` to generate `.lean` files on the filesystem. You can use these to iterate on specifications and proofs using normal Lean tooling (`lake`, `lean`, etc) and copy results back to `.rs` files when you are done.

You will likely want to start with `cargo run generate`, then iterate on `.lean` files directly, and only use `cargo run verify` for final verification once you have copied your work from temporary `.lean` files back to the source of truth `.rs` files.


<!-- File: src/Anneal.lean -->

```lean
instance {ty} : Neg (Aeneas.Std.IScalar ty)

instance {ty} : OfNat (Aeneas.Std.IScalar ty) 0

instance {ty} : OfNat (Aeneas.Std.UScalar ty) 0

class IsValid (α : Type) where
  isValid : α → Prop

instance (priority

/-- The core theorem that mathematically decouples the WP
    into strictly orthogonal Progress and Correctness subgoals. -/
theorem wp_prove_orthogonal {α} {m : Result α} {P : α → Prop} :
  (∃ y, m = .ok y) → (∀ y, m = .ok y → P y) → WP.spec m P

/--
  A proof that a number is a valid alignment (a non-zero power of two).
  This reflects Rust's requirement that all layout alignments are non-zero powers
  of two.
-/
def IsAlignment (n : Nat) : Prop

/-- A validated Rust alignment, bundling the value and its proof. -/
structure Alignment where
  val : Usize
  isValid : IsAlignment val.val

instance : Inhabited Alignment

/--
  A stub for the `Sized` trait.

  Currently, `Sized` is implemented as a Lean `class` to leverage Lean's
  automatic typeclass resolution for computing memory layouts. However, this is
  a temporary workaround. Aeneas translates Rust traits into explicit dictionary
  `structure`s rather than Lean typeclasses to preserve the deterministic,
  single-implementation coherence of Rust's trait resolution.

  Because of this mismatch, Anneal cannot currently generate valid theorem
  signatures for Rust functions that use trait bounds (the generated Lean
  functions expect explicit dictionary arguments that Anneal's typeclass-based
  approach does not supply).

  Once Aeneas is updated to emit marker traits like `Sized` as explicit
  dictionaries, this `class` should be removed. Anneal will then accept the
  Aeneas-generated trait dictionaries in its theorems to guarantee soundness,
  while keeping internal mathematical layout proofs (like `HasStaticLayout`) as
  Lean `class`es to retain automated proof synthesis.

  FIXME(https://github.com/AeneasVerif/aeneas/issues/821): Remove this and
  replace it with the Aeneas-generated trait dictionary once supported.
-/
class Sized (α : Type)

instance : Sized Aeneas.Std.U8

instance : Sized Aeneas.Std.U16

instance : Sized Aeneas.Std.U32

instance : Sized Aeneas.Std.U64

instance : Sized Aeneas.Std.U128

instance : Sized Aeneas.Std.Usize

instance : Sized Aeneas.Std.I8

instance : Sized Aeneas.Std.I16

instance : Sized Aeneas.Std.I32

instance : Sized Aeneas.Std.I64

instance : Sized Aeneas.Std.I128

instance : Sized Aeneas.Std.Isize

instance : Sized Bool

instance : Sized Char

instance : Sized Unit

instance [Sized α] [Sized β] : Sized (α × β)

def deriveSizedCmd (declName : Name) : CommandElabM Unit

/--
  A mathematically idealized memory layout for a value.

  This layout is defined by a size and an alignment. It is unbounded by the
  physical constraints of the machine, meaning that its size is not constrained
  to fit within `Usize`. It is used to reason about the layout of values whose
  sizes may exceed the maximum addressable memory.
-/
structure SpecLayout where
  size : Nat
  align : Alignment
  sizeAligned : align.val.val ∣ size

/--
  A valid physical memory layout for a value.

  This layout is defined by a size and an alignment. It is bounded by the
  physical constraints of the machine, meaning that its size is guaranteed to
  fit within the addressable memory bounds of `Usize`. It is used to represent
  the layout of a value that actually exists in physical memory.
-/
structure Layout where
  size : Usize
  align : Alignment
  sizeAligned : align.val.val ∣ size.val

/--
  A proof that a mathematical layout size is small enough to exist in physical
  memory.

  This proof establishes that the size of a mathematical layout fits within
  `Usize.max`, meaning the layout can describe a physical value.
-/
class FitsInUsize (lay : SpecLayout) : Prop where
  fits : lay.size ≤ Usize.max

instance (lay : Layout) : FitsInUsize lay.toSpecLayout

/--
  The ability to compute a mathematically idealized layout for a runtime value.

  Some types in Rust, such as slices and trait objects, do not have a statically
  known size or alignment. Their layout depends on the specific value instance.
  This class provides the idealized, unbounded layout for a given dynamically
  sized value. Note that `layout` maps from the Lean lowering of a Rust value to
  the layout of the Rust value that it represents, not to the layout of the Lean
  value itself.
-/
class HasSpecLayout (α : Type) where
  layout : α → SpecLayout

/--
  The ability to compute a valid physical layout for a runtime value.

  Some types in Rust, such as slices and trait objects, do not have a statically
  known size or alignment. Their layout depends on the specific value instance.
  This class provides the bounded, physical layout for a given dynamically sized
  value. It requires a proof that the corresponding mathematical layout fits
  within physical memory. Note that `layout` maps from the Lean lowering of a
  Rust value to the layout of the Rust value that it represents, not to the
  layout of the Lean value itself.
-/
class HasLayout (α : Type) [HasSpecLayout α] where
  layout : (val : α) → (h : FitsInUsize (HasSpecLayout.layout val)) → Layout

/--
  A blanket implementation providing a physical layout for any value whose
  mathematical layout fits in memory.
-/
instance {α : Type} [HasSpecLayout α] : HasLayout α

/--
  The mathematically idealized layout for values of a statically sized type.

  Types that implement `core::marker::Sized` have a layout that is known at
  compile time and is identical for all instances of the type. This class
  provides that static, unbounded layout property.
-/
class HasStaticSpecLayout (α : Type) [core.marker.Sized α] where
  layout : SpecLayout

/--
  The valid physical layout for values of a statically sized type.

  Types that implement `core::marker::Sized` have a layout that is known at
  compile time and is identical for all instances of the type. This class
  provides that static, bounded layout property, assuming the corresponding
  mathematical layout fits within physical memory.
-/
class HasStaticLayout (α : Type) [core.marker.Sized α] where
  layout : Layout

/--
  The mathematical layout properties that are statically known for all instances
  of a slice-based dynamically-sized type (Slice DST).
-/
structure SpecSliceDstLayout where
  trailingOffset : Nat
  elementSize : Nat
  align : Alignment

/--
  Provides the static slice DST layout properties for a given type.

  This is analogous to `SpecHasStaticLayout`, but for types that are `!Sized`
  and end in a slice. It provides the unbounded, mathematical layout properties.
-/
class SpecSliceDstTypeLayout (α : Type) where
  layout : SpecSliceDstLayout

/--
  Extracts the dynamic trailing element count for a value of a Slice DST.
-/
class TrailingSlice (α : Type) where
  len : α → Nat

/-- Rounds `val` up to the nearest multiple of `align`. -/
def roundUpToAlign (val align : Nat) : Nat

/-- A theorem stating that rounding up always produces a value greater than or equal to the original value. -/
theorem roundUpToAlign_ge (val align : Nat) (h : 0 < align) :
  val ≤ roundUpToAlign val align

/-- A theorem stating that if the resulting padded value is non-zero, it must be at least the alignment. -/
theorem align_le_roundUpToAlign (val align : Nat) (h_val : 0 < val) (h_align : 0 < align) :
  align ≤ roundUpToAlign val align

/--
  Computes the exact mathematical size of a `repr(C)` Slice DST instance.

  This computation uses the static layout information and the dynamic trailing
  element count. It is not constrained by physical memory limits.
-/
def reprCSliceDstSize (info : SpecSliceDstLayout) (elemCount : Nat) : Nat

/--
  A theorem stating that the unpadded size rounded up to the alignment is always
  perfectly divisible by the alignment.
-/
theorem reprCSliceDstSize_aligned (info : SpecSliceDstLayout) (elemCount : Nat) :
  info.align.val.val ∣ reprCSliceDstSize info elemCount

/-- Marker trait for types that are explicitly `#[repr(C)]`. -/
class ReprC (α : Type)

/--
  A blanket implementation providing a mathematical value layout for `#[repr(C)]`
  Slice DSTs.

  If a type is a Slice DST, and we can extract its length, and it is `#[repr(C)]`,
  we can compute its exact mathematical size.
-/
instance {α : Type} [SpecSliceDstTypeLayout α] [ts : TrailingSlice α] [ReprC α] : HasSpecLayout α

/--
  A blanket implementation providing static slice DST layout properties for
  slices.

  Slices `[T]` are modeled as Slice DSTs with a trailing offset of exactly
  zero.
-/
instance {T : Type} [core.marker.Sized T] [tl : HasStaticSpecLayout T] : SpecSliceDstTypeLayout (Aeneas.Std.Slice T)

/--
  Retrieve the dynamic length of a slice value.
-/
instance {T : Type} : TrailingSlice (Aeneas.Std.Slice T)

/--
  We consider slices to be `#[repr(C)]` so that they can utilize the blanket
  implementation to compute their value layout.
-/
instance {T : Type} : ReprC (Aeneas.Std.Slice T)

def test_has_layout : HasLayout Aeneas.Std.U16

instance {T : Type} {M : Aeneas.Std.Mutability} : core.marker.Sized (Aeneas.Std.RawPtr T M)

/--
  The specification for `core::mem::size_of`.
  This defines the expected behavior of `size_of`: it returns the static size
  defined by the type's `HasStaticLayout`.
-/
abbrev size_of_spec (size_of_fun : Type → Result Usize) : Prop

/--
  The specification for `core::mem::align_of`.
  This defines the expected behavior of `align_of`: it returns the static
  alignment defined by the type's `HasStaticLayout`.
-/
abbrev align_of_spec (align_of_fun : Type → Result Usize) : Prop

/--
  Represents a Rust allocation.
  An allocation has a base address, a size, and a set of memory addresses.
  Because there is no guarantee that an allocation is contiguous, `addresses`
  is modeled as an arbitrary `Set Nat` rather than a contiguous range.
-/
structure Allocation where
  base : Usize
  size : Usize
  addresses : Set Nat

  -- `base` is not equal to null (address 0)
  base_not_null : base.val ≠ 0

  -- `size <= isize::MAX`
  size_le_isize_max : size.val ≤ Isize.max

  -- `base + size <= usize::MAX`
  base_add_size_le_usize_max : base.val + size.val ≤ Usize.max

  -- For all addresses `a` in `addresses`, `a` is in the range `base .. (base + size)`
  bounds : ∀ a ∈ addresses, base.val ≤ a ∧ a < base.val + size.val

theorem offset_le_isize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) :
    a - alloc.base.val ≤ Isize.max

theorem offset_non_negative (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) :
    alloc.base.val ≤ a

theorem address_le_usize_max (alloc : Allocation) (a : Nat) (ha : a ∈ alloc.addresses) :
    a ≤ Usize.max

/--
  Retrieves the properties of a pointer's referent.
  The referent is the region of memory that the pointer addresses.
-/
structure Referent where
  -- The start address of the referent
  address : Usize
  -- The size of the referent in bytes
  size : Usize
  -- The mathematical set of addresses that make up the referent
  addresses : Set Nat

  bounds : ∀ a ∈ addresses, address.val ≤ a ∧ a < address.val + size.val

  addresses_are_usizes : ∀ a ∈ addresses, a ≤ Usize.max

instance : Nonempty Referent

/--
  A predicate indicating that a referent's set of addresses fills the contiguous
  range `[address, address + size)`. This means every address in that range
  belongs to the referent's addresses.
-/
def Referent.IsContiguous (r : Referent) : Prop

/--
  A predicate indicating that a referent fits entirely within a given allocation.
  This means that all logical addresses of the referent are addresses allocated
  in the allocation, and the contiguous address range of the referent is
  a sub-range of the contiguous address range of the allocation.
-/
def FitsInAllocation (r : Referent) (a : Allocation) : Prop

/--
  A helper theorem proving that any address belonging to a referent that
  fits in an allocation is strictly less than the allocation's upper bound.
-/
theorem FitsInAllocation.address_bounds_alloc (r : Referent) (a : Allocation) (h : FitsInAllocation r a) (addr : Nat) (ha : addr ∈ r.addresses) :
  addr < a.base.val + a.size.val

/--
  A class for types that act as pointers with a well-defined referent.
-/
class HasReferent (P : Type) where
  referent : P → Referent

instance {T : Type} {M : Aeneas.Std.Mutability} : HasReferent (Aeneas.Std.RawPtr T M)

/--
  Extracts the mathematical SpecLayout from a statically sized referent.
  This allows users to immediately map from a pointer's raw referent to
  its type-level mathematical properties.
-/
def Referent.toStaticSpecLayout {T : Type} [core.marker.Sized T] [tl : HasStaticSpecLayout T] (_r : Referent) : SpecLayout

/--
  Extracts the metadata of a pointer.
  `P` is the pointer type.
-/
class HasMetadata (P : Type) (M : outParam Type) where
  metadata : P → M

instance {T : Type} [core.marker.Sized T] {M : Aeneas.Std.Mutability} : HasMetadata (Aeneas.Std.RawPtr T M) Unit

instance {T : Type} [SpecSliceDstTypeLayout T] {M : Aeneas.Std.Mutability} :
  HasMetadata (Aeneas.Std.RawPtr T M) Usize

theorem metadata_eq_raw_slice {T : Type} [SpecSliceDstTypeLayout T] {M : Aeneas.Std.Mutability} (val : Aeneas.Std.RawPtr T M) :
  Anneal.HasMetadata.metadata val = Anneal.raw_slice_dst_ptr_metadata val

axiom referent_size_sized {T : Type} [core.marker.Sized T] [lay : HasStaticLayout T] {M : Aeneas.Std.Mutability}
  (p : Aeneas.Std.RawPtr T M) :
  (raw_ptr_referent p).size = lay.layout.size

/--
  Intrinsic structural boundary representing the Rust guarantee that an allocation bounded by `isize::MAX`
  cannot overflow `usize::MAX` during intermediate addition logic for padding calculations.
-/
axiom slice_dst_padding_no_overflow {T : Type} [ReprC T] [lay : SpecSliceDstTypeLayout T] {M : Aeneas.Std.Mutability} (val : Aeneas.Std.RawPtr T M) :
  lay.layout.trailingOffset + lay.layout.elementSize * (raw_slice_dst_ptr_metadata val).val + lay.layout.align.val ≤ Aeneas.Std.Usize.max

/--
  A theorem stating the physical size of a `repr(C)` slice DST referent.

  This axiom states that the physical size of the referent is exactly equal to
  the mathematically computed size of the slice DST (its offset plus its length
  times its element size, padded to its alignment). Because this axiom requires
  a proof that the referent fits within a valid physical allocation, it
  implicitly guarantees that the computed mathematical size fits within physical
  memory limits.
-/
axiom referent_size_slice_dst {T : Type} [ReprC T] [lay : SpecSliceDstTypeLayout T] {M : Aeneas.Std.Mutability}
  (alloc : Allocation) [md : HasMetadata (Aeneas.Std.RawPtr T M) Usize]
  (p : Aeneas.Std.RawPtr T M) (h_fits : FitsInAllocation (raw_ptr_referent p) alloc) :
  (raw_ptr_referent p).size.val = reprCSliceDstSize lay.layout (md.metadata p).val
```