### Install Anneal and Toolchains

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

Installs Anneal and its required toolchains (Charon and Aeneas) using Cargo.

```bash
cargo install cargo-anneal@0.1.0-alpha.24
cargo anneal setup
```

--------------------------------

### Example Patterns for Teddy Algorithm

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/aho-corasick/src/packed/teddy/README.md

These are the example patterns used to illustrate the Teddy algorithm's fingerprinting mechanism.

```ignore
foo
bar
baz
```

--------------------------------

### Multi-bit Flag Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Shows examples of multi-bit flags 'A' and 'B'.

```rust
const A = 0b0000_0011;
const B = 0b1111_1111;
```

--------------------------------

### Example Haystack Block for Teddy Algorithm

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/aho-corasick/src/packed/teddy/README.md

This is an example 16-byte block from the haystack used to demonstrate Teddy's lookup process.

```ignore
bat cat foo bump
xxxxxxxxxxxxxxxx
```

--------------------------------

### Fingerprint Mapping Example (N=1)

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/aho-corasick/src/packed/teddy/README.md

Illustrates the mapping of single-byte fingerprints to patterns in the Teddy algorithm.

```ignore
f |--> foo
b |--> bar, baz
```

--------------------------------

### Single-bit Flag Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Provides examples of single-bit flags 'A' and 'B'.

```rust
const A = 0b0000_0001;
const B = 0b0000_0010;
```

--------------------------------

### Fat Teddy Verification Rearrangement Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/aho-corasick/src/packed/teddy/README.md

Shows how a Fat Teddy mask vector is rearranged for the verification step, consolidating bucket assignments for each offset into 16-bit integers, starting with offset 0.

```text
11000000 000000
```

--------------------------------

### SmallVec Stack and Heap Allocation Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/smallvec/README.md

Demonstrates how to initialize a SmallVec with stack capacity and how it automatically moves to heap allocation when exceeding capacity. Shows basic slice operations on the SmallVec.

```rust
use smallvec::{SmallVec, smallvec};
    
// This SmallVec can hold up to 4 items on the stack:
let mut v: SmallVec<[i32; 4]> = smallvec![1, 2, 3, 4];

// It will automatically move its contents to the heap if
// contains more than four items:
v.push(5);

// SmallVec points to a slice, so you can use normal slice
// indexing and other methods to access its contents:
v[0] = v[1] + v[2];
v.sort();
```

--------------------------------

### Version Gating Macro Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/agent_docs/development.md

This example demonstrates how to use `#[cfg(not(no_zerocopy_<feature>_<version>))]` to conditionally compile code based on the Rust version. It also shows the use of `#[cfg_attr(doc_cfg, doc(cfg(rust = "<version>")))]` for documenting feature availability.

```rust
quote! {
    #[allow(non_snake_case)]
    union ___ZerocopyVariants {
        #(#fields)*
    }
}
```

--------------------------------

### Empty Flags Value Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Shows an example of an empty flags value.

```rust
0b0000_0000
```

--------------------------------

### Use windows crate to call Windows APIs

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/windows-sys/readme.md

Import and use Windows APIs through the `windows` crate. This example demonstrates XML document manipulation and basic threading and UI functions.

```rust
use windows::
    core::*,
    Data::Xml::Dom::*,
    Win32::Foundation::*,
    Win32::System::Threading::*,
    Win32::UI::WindowsAndMessaging::*,
;

fn main() -> Result<()> {
    let doc = XmlDocument::new()?;
    doc.LoadXml(h!("<html>hello world</html>"))?;

    let root = doc.DocumentElement()?;
    assert!(root.NodeName()? == "html");
    assert!(root.InnerText()? == "hello world");

    unsafe {
        let event = CreateEventW(None, true, false, None)?;
        SetEvent(event)?;
        WaitForSingleObject(event, 0);
        CloseHandle(event)?;

        MessageBoxA(None, s!("Ansi"), s!("Caption"), MB_OK);
        MessageBoxW(None, w!("Wide"), w!("Caption"), MB_OK);
    }

    Ok(())
}
```

--------------------------------

### Parse and Match Version Requirements

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/semver/README.md

This example demonstrates how to parse a version requirement string and check if a given version matches it. It covers both non-matching and matching cases.

```rust
use semver::{BuildMetadata, Prerelease, Version, VersionReq};

fn main() {
    let req = VersionReq::parse(">=1.2.3, <1.8.0").unwrap();

    // Check whether this requirement matches version 1.2.3-alpha.1 (no)
    let version = Version {
        major: 1,
        minor: 2,
        patch: 3,
        pre: Prerelease::new("alpha.1").unwrap(),
        build: BuildMetadata::EMPTY,
    };
    assert!(!req.matches(&version));

    // Check whether it matches 1.3.0 (yes it does)
    let version = Version::parse("1.3.0").unwrap();
    assert!(req.matches(&version));
}
```

--------------------------------

### Context Hygiene with `proof context:`

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/named_bounds.md

Shows how to use `proof context:` to inject shared setup code into Lean's Term Mode before struct initialization, ensuring context hygiene.

```rust
/// ensures (h_pos): ret > 0
/// ensures (h_even): ret % 2 == 0
/// proof context:
///   have h_shared : ret = 2 := by simp [foo]
/// proof (h_pos): ...
/// proof (h_even): ...
```

```lean
exact
  have h_shared : ret = 2 := by simp [foo]
  {
    h_pos := by ...
    h_even := by ...
  }
```

--------------------------------

### General Flags Formatting Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Demonstrates how flags values are formatted into text across different modes, showing named flags and combined flags.

```text
0b0000_0000 = ""
0b0000_0001 = "A"
0b0000_0010 = "B"
0b0000_0011 = "A | B"
0b0000_0011 = "AB"
0b0000_1111 = "A | B | C"
```

--------------------------------

### Example Bits Values for u8

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Illustrates different bits values for the u8 bits type, showing binary representations.

```rust
0b0000_0000
0b1111_1111
0b1010_0101
```

--------------------------------

### Simple Regex Compilation Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/regex/HACKING.md

Illustrates the compiled opcode sequence for the regular expression 'a|b', showing Save, Split, literal match, and Match instructions.

```text
000 Save(0)
001 Split(2, 3)
002 'a' (goto: 4)
003 'b'
004 Save(1)
005 Match
```

--------------------------------

### Use windows-sys crate to call Windows APIs

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/windows-sys/readme.md

Import and use Windows APIs directly through the `windows-sys` crate. This example shows basic threading and UI functions using raw function pointers.

```rust
use windows_sys::
    core::*,
    Win32::Foundation::*,
    Win32::System::Threading::*,
    Win32::UI::WindowsAndMessaging::*,
;

fn main() {
    unsafe {
        let event = CreateEventW(std::ptr::null(), 1, 0, std::ptr::null());
        SetEvent(event);
        WaitForSingleObject(event, 0);
        CloseHandle(event);

        MessageBoxA(0, s!("Ansi"), s!("Caption"), MB_OK);
        MessageBoxW(0, w!("Wide"), w!("Caption"), MB_OK);
    }
}
```

--------------------------------

### Example JSON Structure

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/serde_json/README.md

This is an example of a typical JSON object structure, illustrating key-value pairs, nested objects, and arrays.

```json
{
    "name": "John Doe",
    "age": 43,
    "address": {
        "street": "10 Downing Street",
        "city": "London"
    },
    "phones": [
        "+44 1234567",
        "+44 2345678"
    ]
}

```

--------------------------------

### Valid Anneal Syntax Example

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/design.md

Demonstrates correct usage of Anneal syntax within Rust documentation comments, including keywords and indentation for nested clauses.

```rust
/// ```lean, anneal, spec
/// context:                   -- New section (Baseline: 0 spaces)
///   open Aeneas              -- Valid continuation (2 > 0)
///   let limit := 100         -- Valid continuation (2 > 0)
///
/// requires:                  -- New section (Baseline: 0 spaces)
///   x < limit                -- Valid continuation (2 > 0)
///   && x > 0                 -- Valid continuation (2 > 0)
///
/// ensures: ret = x + 1       -- New section (Baseline: 0 spaces)
///
/// proof:                     -- New section (Baseline: 0 spaces)
///   intros                   -- Valid continuation (2 > 0)
///   simp [limit] at *        -- Valid continuation (2 > 0)
/// ```
```

--------------------------------

### Anneal Indentation Rule Example

Source: https://github.com/google/zerocopy/blob/main/anneal/llms-full.txt

Demonstrates the correct indentation for multi-line expressions in Anneal. Continuation lines must be indented deeper than the leading clause.

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

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

--------------------------------

### Running Debugger Visualizer Tests Locally

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/smallvec/debug_metadata/README.md

Example command to run debugger visualizer tests specifically for the debugger_visualizer binary, enabling the debugger_visualizer feature and setting test threads to 1 to ensure sequential execution.

```bash
cargo test --test debugger_visualizer --features debugger_visualizer -- --test-threads=1
```

--------------------------------

### Lazy Static Macro Implementation

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/syn/README.md

A procedural macro example reimplementing the lazy_static crate, demonstrating how to parse function-like macro input.

```rust
lazy_static! {
    static ref USERNAME: Regex = Regex::new("^[a-z0-9_-]{3,16}$").unwrap();
}
```

--------------------------------

### Run Rust Implementation Benchmark

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/ryu/README.md

Clone the Rust implementation of Ryū and use Cargo to run its upstream benchmark example. This measures the performance against the original C implementation.

```console
$ git clone https://github.com/dtolnay/ryu rust-ryu
$ cd rust-ryu
$ cargo run --example upstream_benchmark --release

```

--------------------------------

### Derive Macro Usage Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/syn/README.md

Demonstrates how to apply the 'HeapSize' derive macro to a struct. This allows the struct to automatically implement the 'HeapSize' trait.

```rust
#[derive(HeapSize)]
struct Demo<'a, T: ?Sized> {
    a: Box<T>,
    b: u8,
    c: &'a str,
    d: String,
}
```

--------------------------------

### Run Anneal to Expand Examples

Source: https://github.com/google/zerocopy/blob/main/anneal/AGENTS.md

Use `cargo run expand` to see the generated Lean code for a module without verification. This is useful for inspecting the output of Aeneas and Anneal.

```bash
cargo run expand --example abs
```

--------------------------------

### Rustfmt Bailout Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/prettyplease/README.md

This code snippet demonstrates a scenario where rustfmt fails to format a large section of code, resulting in it being placed on a single line. This is contrasted with prettyplease's design to avoid such pathological cases.

```rust
            match segments[5] {
                0 => write!(f, "::{}", ipv4),
                0xffff => write!(f, "::ffff:{}", ipv4),
                _ => unreachable!(),
            }
        } else { # [derive (Copy , Clone , Default)] struct Span { start : usize , len : usize , } let zeroes = { let mut longest = Span :: default () ; let mut current = Span :: default () ; for (i , & segment) in segments . iter () . enumerate () { if segment == 0 { if current . len == 0 { current . start = i ; } current . len += 1 ; if current . len > longest . len { longest = current ; } } else { current = Span :: default () ; } } longest } ; # [doc = " Write a colon-separated part of the address"] # [inline] fn fmt_subslice (f : & mut fmt :: Formatter < '_ > , chunk : & [u16]) -> fmt :: Result { if let Some ((first , tail)) = chunk . split_first () { write ! (f , "{:x}" , first) ? ; for segment in tail { f . write_char (':') ? ; write ! (f , "{:x}" , segment) ? ; } } Ok (()) } if zeroes . len > 1 { fmt_subslice (f , & segments [.. zeroes . start]) ? ; f . write_str ("::") ? ; fmt_subslice (f , & segments [zeroes . start + zeroes . len ..]) } else { fmt_subslice (f , & segments) } }
    } else {
        const IPV6_BUF_LEN: usize = (4 * 8) + 7;
        let mut buf = [0u8; IPV6_BUF_LEN];
        let mut buf_slice = &mut buf[..];

```

--------------------------------

### Example of Failing Proof with `--allow-sorry`

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/05_proof_architecture.md

Even with the `--allow-sorry` flag, compilation will fail if your manual proof block contains syntax errors or non-existent tactics.

```rust
/// ```anneal, proof
/// proof (foo):
///   some_garbage_tactic_that_doesnt_exist
/// ```
```

--------------------------------

### Rust quote! Macro Syntax Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/quote/README.md

Demonstrates the basic syntax of the quote! macro for generating Rust code structures and implementations. Interpolation is used for variables like #generics, #where_clause, #field_ty, etc.

```rust
let tokens = quote! {
    struct SerializeWith #generics #where_clause {
        value: &'a #field_ty,
        phantom: core::marker::PhantomData<#item_ty>,
    }

    impl #generics serde::Serialize for SerializeWith #generics #where_clause {
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: serde::Serializer,
        {
            #path(self.value, serializer)
        }
    }

    SerializeWith {
        value: #value,
        phantom: core::marker::PhantomData::<#item_ty>,
    }
};
```

--------------------------------

### Rust's safe usize::strict_div example

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

Illustrates a safe Rust function that must handle all possible input values, including edge cases like division by zero, by either returning a value or panicking.

```rust
impl usize {
    /// # Panics
    /// 
    /// This function will panic if `rhs` is zero.
    pub fn strict_div(self, rhs: usize) -> usize;
}
```

--------------------------------

### Basic Derive Macro Implementation

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/syn/README.md

An example of a basic derive macro function in Rust. It parses input tokens into a syntax tree, uses 'quote' for code generation, and returns the expanded tokens.

```rust
use proc_macro::TokenStream;
use quote::quote;
use syn::{parse_macro_input, DeriveInput};

#[proc_macro_derive(MyMacro)]
pub fn my_macro(input: TokenStream) -> TokenStream {
    // Parse the input tokens into a syntax tree
    let input = parse_macro_input!(input as DeriveInput);

    // Build the output, possibly using quasi-quotation
    let expanded = quote! {
        // ...
    };

    // Hand the output tokens back to the compiler
    TokenStream::from(expanded)
}
```

--------------------------------

### Orthogonal WP Proof in Lean

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/named_bounds.md

Demonstrates how to use `wp_prove_orthogonal` to separate progress and correctness goals in Lean. This allows for targeted failure analysis and ensures correctness even if progress stalls.

```lean
-- Generated by Anneal
apply wp_prove_orthogonal
· -- Goal 1: Progress
  eval_progress "Execution stalled..."
· -- Goal 2: Correctness
  intro y hy
  exact { ... } -- The Post struct evaluates safely here!
```

--------------------------------

### Instantiating Postconditions with `exact {}`

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/named_bounds.md

Demonstrates how to instantiate a `Post` structure using `exact {}` for independent subset evaluation. Missing fields are automatically handled by Lean's `autoParam` macro.

```lean
-- ... inside the theorem ...
exact {
  h_incremented := by
    -- User's `proof (h_incremented)` block gets injected perfectly here!
    omega
  -- Notice that `h_ret_is_valid` is intentionally missing ...
}
```

--------------------------------

### Buggy unsafe Rust code example

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

A concrete example of calling an unsafe Rust function with an illegal value, which would result in undefined behavior and memory safety bugs.

```rust
let res: usize = unsafe { 1usize.unchecked_div_exact(0) };
```

--------------------------------

### Unnamed Flag Example

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Illustrates the definition of an unnamed flag.

```rust
const _ = 0b0000_0001;
```

--------------------------------

### Non-Empty Flags Value Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Illustrates flags values that are not empty.

```rust
0b0000_0001
0b0110_0000
```

--------------------------------

### Intersection of Flags Values

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Examples of the bitwise AND operation between two flags values.

```rust
0b0000_0001 & 0b0000_0010 = 0b0000_0000
```

```rust
0b1111_1100 & 0b1111_0111 = 0b1111_0100
```

```rust
0b1111_1111 & 0b1111_1111 = 0b1111_1111
```

--------------------------------

### Anneal CLI Verify Help

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/design.md

Displays help information for the `cargo anneal verify` command, including options for allowing 'sorry' in proofs and specifying the manifest path or package.

```bash
$ cargo anneal verify --help
Verify a crate

Usage: cargo anneal verify [OPTIONS]

Options:
      --allow-sorry            Allow `sorry` in proofs and inject `sorry` for missing proofs
      --manifest-path <PATH>   Path to Cargo.toml
  -p, --package <SPEC>         Package to process
      --workspace              Process all packages in the workspace
      ... (standard cargo targeting flags) ...

```

--------------------------------

### Union of Flags Values

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Examples of the bitwise OR operation between two flags values.

```rust
0b0000_0001 | 0b0000_0010 = 0b0000_0011
```

```rust
0b0000_0000 | 0b1111_1111 = 0b1111_1111
```

--------------------------------

### Build and Check on Supported Toolchains

Source: https://github.com/google/zerocopy/blob/main/zerocopy/agent_docs/validation.md

Ensure the library builds successfully on the minimum supported Rust version (MSRV) and stable toolchains, including tests. Also, perform a full check with all features on the nightly toolchain.

```bash
./cargo.sh +msrv check --tests --features __internal_use_only_features_that_work_on_stable
```

```bash
./cargo.sh +stable check --tests --features __internal_use_only_features_that_work_on_stable
```

```bash
./cargo.sh +nightly check --tests --all-features
```

```bash
./cargo.sh +nightly clippy --tests --all-features --workspace
```

--------------------------------

### Flags Value Non-Intersection Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Provides flags values that do not intersect with 0b0000_0011.

```rust
0b0000_0000
0b1111_0000
```

--------------------------------

### Using quote! in build.rs with prettyplease

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/quote/README.md

Demonstrates how to use the quote! macro in a build script to generate Rust code, parse it with syn, format it using prettyplease, and write it to a file. This process helps in creating human-readable generated code.

```rust
let output = quote! { ... };
let syntax_tree = syn::parse2(output).unwrap();
let formatted = prettyplease::unparse(&syntax_tree);

let out_dir = env::var_os("OUT_DIR").unwrap();
let dest_path = Path::new(&out_dir).join("out.rs");
fs::write(dest_path, formatted).unwrap();
```

--------------------------------

### Flags Value Intersection Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Lists flags values that intersect with 0b0000_0011.

```rust
0b0000_0010
0b0000_0001
0b1111_1111
```

--------------------------------

### Flags Value Non-Containment Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Shows flags values that are not contained within 0b0000_0011.

```rust
0b0000_1000
0b0000_0110
```

--------------------------------

### Flags Value Containment Examples

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Demonstrates flags values that are contained within 0b0000_0011.

```rust
0b0000_0000
0b0000_0010
0b0000_0001
0b0000_0011
```

--------------------------------

### Symmetric Difference of Flags Values

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Examples of the bitwise exclusive OR (XOR) operation between two flags values.

```rust
0b0000_0001 ^ 0b0000_0010 = 0b0000_0011
```

```rust
0b0000_1111 ^ 0b0000_0011 = 0b0000_1100
```

```rust
0b1100_0000 ^ 0b0011_0000 = 0b1111_0000
```

--------------------------------

### Derive HeapSize Macro

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/syn/README.md

Example of a struct deriving HeapSize, which can lead to compilation errors if a field type does not implement HeapSize.

```rust
#[derive(HeapSize)]
struct Broken {
    ok: String,
    bad: std::thread::Thread,
}
```

--------------------------------

### Basic Serde Serialization and Deserialization in Rust

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/serde/crates-io.md

Demonstrates how to derive Serialize and Deserialize for a struct and then convert it to and from a JSON string. Ensure the `serde_json` crate is added as a dependency.

```rust
use serde::{Deserialize, Serialize};

#[derive(Serialize, Deserialize, Debug)]
struct Point {
    x: i32,
    y: i32,
}

fn main() {
    let point = Point { x: 1, y: 2 };

    // Convert the Point to a JSON string.
    let serialized = serde_json::to_string(&point).unwrap();

    // Prints serialized = {"x":1,"y":2}
    println!("serialized = {}", serialized);

    // Convert the JSON string back to a Point.
    let deserialized: Point = serde_json::from_str(&serialized).unwrap();

    // Prints deserialized = Point { x: 1, y: 2 }
    println!("deserialized = {:?}", deserialized);
}
```

--------------------------------

### Using guard for resource management with cleanup

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/scopeguard/README.md

Shows how to use the `guard` function to manage a resource (like a file) and ensure a cleanup closure is executed upon scope exit. This is useful for file synchronization or other resource deallocation tasks.

```Rust
use scopeguard::guard;
use std::fs::File;
use std::io::Write;

fn g() {
    let f = File::create("newfile.txt").unwrap();
    let mut file = guard(f, |f| {
        // write file at return or panic
        let _ = f.sync_all();
    });
    // access the file through the scope guard itself
    file.write_all(b"test me\n").unwrap();
}
```

--------------------------------

### Difference of Flags Values

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Examples of the bitwise AND operation between one flags value and the complement of another. This operation truncates the result in the complement.

```rust
0b0000_0001 & !0b0000_0010 = 0b0000_0001
```

```rust
0b0000_1101 & !0b0000_0011 = 0b0000_1100
```

```rust
0b1111_1111 & !0b0000_0001 = 0b1111_1110
```

--------------------------------

### Rustc Formatting: Non-multiple-of-4 indentation

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/prettyplease/README.md

Shows an example of rustc using indentation that is not a multiple of 4, which is not the standard practice in modern Rust code.

```rust
pub const fn to_ipv6_mapped(&self) -> Ipv6Addr {
    let [a, b, c, d] = self.octets();
    Ipv6Addr{inner:
                 c::in6_addr{
                                 s6_addr:
                                 [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0xFF,
                                  0xFF, a, b, c, d],
                             },
}
}
```

--------------------------------

### Run Upstream C Benchmark

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/ryu/README.md

Clone the original C implementation of Ryū and use Bazel to run its benchmark suite. This allows for direct comparison of performance.

```console
$ git clone https://github.com/ulfjack/ryu c-ryu
$ cd c-ryu
$ bazel run -c opt //ryu/benchmark:ryu_benchmark

```

--------------------------------

### Conceptual Anneal Internal Structure

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/05_proof_architecture.md

This illustrates how Anneal internally structures the verification of postconditions and invariants. Your manual proofs are injected into the `exact` instantiation.

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

--------------------------------

### Compare Benchmark Results

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/regex/HACKING.md

Capture current benchmark results to a file and compare them against older results using `cargo-benchcmp`. This is useful for tracking performance improvements over time.

```bash
(cd bench && ./run rust | tee old)
...
(cd bench && ./run rust | tee new)
cargo benchcmp old new --improvements
```

--------------------------------

### Complement of Flags Value

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/bitflags/spec.md

Examples of the bitwise NOT operation on a flags value, which also truncates the result. This operation is necessary because the negation can set unknown bits.

```rust
!0b0000_0000 = 0b0000_1111
```

```rust
!0b0000_1111 = 0b0000_0000
```

```rust
!0b1111_1000 = 0b0000_0111
```

--------------------------------

### Generate Lean Files with Anneal

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

Generates the `.lean` files on disk, allowing for iteration on proofs using standard Lean tooling before copying them back to Rust source.

```bash
cargo anneal generate
```

--------------------------------

### Anonymous `isSafe` Specification

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/04_specifications_and_syntax.md

An example of an anonymous `isSafe` specification for an unsafe trait, defining a universally quantified property that must hold for all implementers of the trait.

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

--------------------------------

### Anonymous `isValid` Specification

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/04_specifications_and_syntax.md

An example of an anonymous `isValid` specification for a type, defining a boolean Lean function that must hold true for instances of the type.

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

--------------------------------

### Format Rust Code with prettyplease

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/prettyplease/README.md

This snippet demonstrates how to format a Rust code string using prettyplease. It requires the 'prettyplease' and 'syn' crates. The code first parses an input string into a syntax tree and then uses prettyplease to format it.

```rust
// [dependencies]
// prettyplease = "0.2"
// syn = { version = "2", default-features = false, features = ["full", "parsing"] }

const INPUT: &str = stringify! {
    use crate::{
          lazy::{Lazy, SyncLazy, SyncOnceCell}, panic,
        sync::{ atomic::{AtomicUsize, Ordering::SeqCst},
            mpsc::channel, Mutex, },
      thread,
    };
    impl<T, U> Into<U> for T where U: From<T> {
        fn into(self) -> U { U::from(self) }
    }
};

fn main() {
    let syntax_tree = syn::parse_file(INPUT).unwrap();
    let formatted = prettyplease::unparse(&syntax_tree);
    print!("{}", formatted);
}
```

--------------------------------

### Valid Indentation in Anneal

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/04_specifications_and_syntax.md

Anneal uses indentation-sensitive parsing. Continuation lines within a clause must be indented deeper than the line that started the clause.

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

--------------------------------

### Rust Token Visualization

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/prettyplease/README.md

A visualization of Rust tokens processed by the pretty printing algorithm, showing different token types and group breaking behaviors.

```text
use crate::«{·
‹    lazy::«{·‹Lazy,· SyncLazy,· SyncOnceCell›·}»,·
    panic,·
    sync::«{·
‹        atomic::«{·‹AtomicUsize,· Ordering::SeqCst›·}»,·
        mpsc::channel,· Mutex›,·
    }»,·
    thread›,·
}»;·
«‹«impl<«·T‹›,· U‹›·»>» Into<«·U·»>· for T›·
where·
    U:‹ From<«·T·»>›,
{
«    fn into(·«·self·») -> U {·
‹        U::from(«·self·»)›
»    }
»}

```

--------------------------------

### Run Rust Benchmarks

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/regex/HACKING.md

Execute the Rust benchmarks for the regex crate. This is the primary command for running performance tests on the Rust implementation.

```bash
(cd bench && ./run rust)
```

--------------------------------

### Anneal's verified unchecked_div_exact example

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

Shows how Anneal annotations can encode safety preconditions for unsafe functions, preventing the compilation of code that violates these preconditions.

```rust
impl usize {
    /// # Safety
    /// 
    /// ```anneal
    /// requires(nonzero): rhs != 0
    /// requires(divides): self % rhs == 0
    /// ```
    pub unsafe fn unchecked_div_exact(self, rhs: usize) -> usize;
}
```

--------------------------------

### Basic Anneal Specification Syntax

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/agent/04_specifications_and_syntax.md

Anneal annotations use indentation-sensitive blocks for specifications. This example shows the basic structure with `requires`, `ensures`, and `proof` blocks.

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

--------------------------------

### Unicode Character Class Difference

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/regex/UNICODE.md

Match non-ASCII letters using character class difference. This example finds characters in the 'Letter' Unicode property that are not in the 'Ascii' property.

```regex
[\p{Letter}--[\p{Ascii}]]
```

--------------------------------

### Configure Anneal to Allow 'sorry' in Lean Proofs

Source: https://github.com/google/zerocopy/blob/main/anneal/AGENTS.md

For integration tests, add `"--allow-sorry"` to the `args` array in `anneal.toml` to permit unimplemented Lean proofs marked with `sorry` during development.

```toml
args = ["verify", "--allow-sorry"]
```

--------------------------------

### Basic JSON Value Construction

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/serde_json/README.md

Demonstrates the basic usage of the json! macro to create a serde_json::Value object representing a person's details. Shows how to access nested elements and convert the Value to a JSON string.

```rust
use serde_json::json;

fn main() {
    // The type of `john` is `serde_json::Value`
    let john = json!({
        "name": "John Doe",
        "age": 43,
        "phones": [
            "+44 1234567",
            "+44 2345678"
        ]
    });

    println!("first phone number: {}", john["phones"][0]);

    // Convert to a string of JSON and print it out
    println!("{}", john.to_string());
}
```

--------------------------------

### Anneal's verified call to unchecked_div_exact

Source: https://github.com/google/zerocopy/blob/main/anneal/README.md

An example demonstrating that Anneal prevents the compilation of unsafe code calls if the safety preconditions, specified via annotations, cannot be proven.

```rust
let res: usize = unsafe { 1usize.unchecked_div_exact(0) }; // ERROR: Cannot prove `rhs != 0`
```

--------------------------------

### XID_Start Check Assembly

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/unicode-ident/README.md

This assembly code snippet demonstrates the logic for checking the XID_Start property. It utilizes a two-level trie and bit manipulation for efficient lookups.

```assembly
is_xid_start:
	mov eax, edi
	mov ecx, offset unicode_ident::ZERO
	shr eax, 9
	cmp edi, 210432
	lea rax, [rax + unicode_ident::tables::TRIE_START]
	cmovb rcx, rax
	movzx eax, byte ptr [rcx]
	mov ecx, 1539
	bextr ecx, edi, ecx
	and edi, 7
	shl eax, 5
	movzx eax, byte ptr [rax + rcx + unicode_ident::tables::LEAF]
	bt eax, edi
	setb al
	ret
```

--------------------------------

### Workaround for `progress` Tactic using `proof (h_progress)`

Source: https://github.com/google/zerocopy/blob/main/anneal/docs/design/named_bounds.md

Demonstrates the recommended workaround for using the `progress` tactic by relocating it to a `proof (h_progress):` block. This block natively supports tactic mode evaluation for Weakest Preconditions, allowing `progress` to function correctly.

```rust
/// proof (h_progress):
///   unfold parent_func at *
///   progress as ⟨ ret_val, h_valid ⟩
///   unfold parent_func at h_ret_
///   simp_all [parent_func, sub_func]
```

--------------------------------

### Add quote Crate Dependency

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/quote/README.md

To use the quote crate, add it as a dependency in your Cargo.toml file. This example shows the TOML syntax for adding the quote crate version 1.0.

```toml
[dependencies]
quote = "1.0"
```

--------------------------------

### Conditional Compilation with cfg_if! Macro

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/cfg-if/README.md

Demonstrates how to define a function 'foo' with different implementations based on Unix and 32-bit target configurations. The first matching condition determines the function's implementation.

```rust
cfg_if::cfg_if! {
    if #[cfg(unix)] {
        fn foo() { /* unix specific functionality */ }
    } else if #[cfg(target_pointer_width = "32")] {
        fn foo() { /* non-unix, 32-bit functionality */ }
    } else {
        fn foo() { /* fallback implementation */ }
    }
}

fn main() {
    foo();
}
```

--------------------------------

### DFA Search Implementation

Source: https://github.com/google/zerocopy/blob/main/zerocopy/vendor/aho-corasick/DESIGN.md

Demonstrates the search logic for a Deterministic Finite Automaton (DFA). This implementation is optimized for speed, as each byte of input deterministically advances the automaton by one state without requiring failure transitions.

```rust
fn contains(dfa: &DFA, haystack: &[u8]) -> bool {
  let mut state_id = dfa.start();
  // If the empty pattern is in dfa, then state_id is a match state.
  if dfa.is_match(state_id) {
    return true;
  }
  for (i, &b) in haystack.iter().enumerate() {
    // An Aho-Corasick DFA *never* has a missing state that requires
    // failure transitions to be followed. One byte of input advances the
    // automaton by one state. Always.
    state_id = dfa.next_state(state_id, b);
    if dfa.is_match(state_id) {
      return true;
    }
  }
  false
}
```