### Project Load Timing Output

Source: https://github.com/acornprover/acorn/blob/master/PROFILE.md

Example output showing the breakdown of project setup and dependency loading times.

```text
project setup: 59.7ms
  cache load: 58.9ms
target/dependency load: 8.367s
total measured: 8.426s
modules loaded: 596
targets: 117
wall clock: 0:08.75
CPU: 99%
max RSS: 3.55 GiB
```

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

### Install Acorn from source

Source: https://github.com/acornprover/acorn/blob/master/README.md

Initialize submodules and run the test suite to verify the local environment.

```bash
cd ~/acorn
git submodule update --init
cargo test -q
```

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

### Install release dependencies

Source: https://github.com/acornprover/acorn/blob/master/RELEASE.md

Commands to install necessary cross-compilation tools for Linux and Mac builds.

```bash
rustup target add aarch64-apple-darwin
snap install zig --classic --beta
cargo install --locked cargo-zigbuild
```

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

### Basic Instance Declaration

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

A minimal example of declaring an instance for a typeclass.

```acorn
    inductive Z1 {
        zero
    }

    typeclass S: Singleton {
        value: S

        unique(x: S) {
            x = S.value
        }
    }

    instance Z1: Singleton {
        let value: Z1 = Z1.zero
    }
    
```

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

### Lambda Normalization Example

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Demonstrates normalizing lambdas within function calls by synthesizing terms.

```acorn
            type Nat: axiom
            let zero: Nat = axiom
            define apply(f: Nat -> Nat, a: Nat) -> Nat { f(a) }
            theorem goal { apply(function(x: Nat) { x }, zero) = zero }
```

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

### Install VS Code extension dependencies

Source: https://github.com/acornprover/acorn/blob/master/README.md

Install required Node.js dependencies for the extension and assistant components.

```bash
cd ~/acorn/vscode/extension
npm install
cd ~/acorn/vscode/assistant
npm install
```

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

### Multi-Threaded Timing Output

Source: https://github.com/acornprover/acorn/blob/master/PROFILE.md

Example output from a 20-thread performance check.

```text
target/module load counter: 10.370s
certificate checking counter: 11.889s
  cached cert checks: 59.308s summed worker time
total measured: 12.370s
certificate throughput: 7,861 certs/s
wall clock: 0:12.83
CPU: 1,224%
max RSS: 4.78 GiB
```

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

### Rewrite Consistency Example

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Defines natural numbers and axioms for addition and multiplication to test rewrite logic consistency.

```acorn
            type Nat: axiom
            let zero: Nat = axiom
            let suc: Nat -> Nat = axiom
            let addx: (Nat, Nat) -> Nat = axiom
            let mulx: (Nat, Nat) -> Nat = axiom
            axiom add_suc(a: Nat, b: Nat) { addx(suc(a), b) = suc(addx(a, b)) }
            axiom suc_ne(a: Nat) { suc(a) != a }
            axiom mul_suc(a: Nat, b: Nat) { addx(a, mulx(a, b)) = mulx(a, suc(b)) }
            theorem goal(a: Nat) { suc(a) != a }
```

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

### Templated Proof Example

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Shows the definition of a templated function and the use of axioms to prove a goal involving templated claims.

```acorn
            type Thing: axiom
            let t1: Thing = axiom
            let t2: Thing = axiom
            let t3: Thing = axiom

            define foo[T](x: T) -> Bool { axiom }

            axiom a12 { foo(t1) implies foo(t2) }
            axiom a23 { foo(t2) implies foo(t3) }
            theorem goal { foo(t1) implies foo(t3) }
```

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

### Single-Threaded Timing Output

Source: https://github.com/acornprover/acorn/blob/master/PROFILE.md

Example output from a single-threaded performance check.

```text
target/module load: 40.793s
certificate checking: 60.327s
  cached cert checks: 35.779s
  other verification: 24.548s
total measured: 101.348s
certificate throughput: 1,549 certs/s
wall clock: 1:41.72
CPU: 100%
max RSS: 3.50 GiB
```

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

### Define Proof Inside Destructuring Let

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/proof_blocks.md

Provides an example of using a proof block to handle destructuring in a let statement.

```acorn
type Nat: axiom

inductive Option[T] {
    none
    some(T)
}

let y: Option[Nat] = axiom

let Option.some(x) = y by {
    let witness: Nat = axiom
    axiom witness_eq {
        Option.some(witness) = y
    }
    witness_eq
}

theorem destructured_value {
    Option.some(x) = y
}
```

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

### Proving With Partial Application

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Shows how to use partial application within theorem goals.

```acorn
            type Nat: axiom
            let zero: Nat = axiom
            let addx: (Nat, Nat) -> Nat = axiom
            theorem goal(f: Nat -> Nat) { f = addx(zero) implies f(zero) = addx(zero, zero) }
```

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

### Partial Application Theorem Instantiation

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/normalization.md

Demonstrates using a helper theorem to prove equality under partial application.

```acorn
    type Nat: axiom

    theorem helper(a: Nat -> Nat, m: Nat, n: Nat) {
        m = n implies a(m) = a(n)
    }

    theorem goal(f: (Nat, Nat) -> Nat, i: Nat, m: Nat, n: Nat) {
        m = n implies f(i, m) = f(i, n)
    } by {
        if m = n {
            helper(f(i), m, n)
            f(i, m) = f(i, n)
        }
    }
    
```

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

### Use Typeclass Axiom on Instance

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Illustrates defining a typeclass, creating an instance for a specific type, and proving a theorem using the instance.

```acorn
    typeclass F: FooTrue {
        b: Bool
    }

    define foo[T](t: T) -> Bool {
        axiom
    }

    axiom foo_true[F: FooTrue](a: F) {
        foo(a)
    }

    inductive Z1 {
        zero
    }

    instance Z1: FooTrue {
        let b: Bool = true
    }

    theorem goal(z: Z1) {
        foo(z)
    }
    
```

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

### Define Instance with Define

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Demonstrates implementing a typeclass instance using the define keyword for the function implementation.

```acorn
    inductive Z1 {
        zero
    }

    typeclass T: TwoColored {
        is_red: T -> Bool
    }

    instance Z1: TwoColored {
        define is_red(self) -> Bool {
            true
        }
    }

    theorem goal {
        TwoColored.is_red(Z1.zero)
    }
    
```

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

### Update acornlib submodule

Source: https://github.com/acornprover/acorn/blob/master/RELEASE.md

Commands to update the local acornlib submodule before starting a release.

```bash
cd acornlib
git pull origin master
cd ..
```

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

### Define Instance with Let

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Demonstrates implementing a typeclass instance using a let binding for the function definition.

```acorn
    inductive Z1 {
        zero
    }

    typeclass T: TwoColored {
        is_red: T -> Bool
    }

    instance Z1: TwoColored {
        let is_red: Z1 -> Bool = function(z: Z1) {
            true
        }
    }

    theorem goal {
        TwoColored.is_red(Z1.zero)
    }
    
```

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

### Failing Transport Without Index Equality

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/transport.md

An example of a transport operation that fails because the required index equality is not established.

```acorn
type Nat: axiom
type Item: axiom

structure Fin[n: Nat] {
    value: Nat
}

theorem bad(n: Nat, k: Nat, v: Fin[n] -> Item) {
    true
} by {
    let w: Fin[k] -> Item = transport v
}
```

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

### Use an Imported Axiom in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/verification.md

Shows how to define axioms and use them to prove a theorem involving function morphisms.

```acorn
type Bar: axiom
let bar: Bar = axiom
let morph: Bar -> Bar = axiom
axiom meq(b: Bar) { morph(b) = morph(bar) }

theorem goal(a: Bar, b: Bar) { morph(a) = morph(b) }
```

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

### Vector Tail Transport

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/transport.md

Complex example showing transport preservation for vector structures defined over finite indices.

```acorn
type Nat: axiom

define suc(n: Nat) -> Nat {
    axiom
}

structure Fin[n: Nat] {
    value: Nat
}

define fin_cast_suc(n: Nat, x: Fin[n]) -> Fin[suc(n)] {
    Fin[suc(n)].new(x.value)
}

theorem fin_cast_suc_value(n: Nat, x: Fin[n]) {
    fin_cast_suc(n, x).value = x.value
}

structure Vector[T, n: Nat] {
    entry: Fin[n] -> T
}

define vector_tail_entry[T](n: Nat, xs: Vector[T, suc(n)], i: Fin[n]) -> T {
    xs.entry(fin_cast_suc(n, i))
}

define vector_tail[T](n: Nat, xs: Vector[T, suc(n)]) -> Vector[T, n] {
    Vector[T, n].new(vector_tail_entry[T](n, xs))
}

theorem vector_tail_entry_eq[T](n: Nat, xs: Vector[T, suc(n)], i: Fin[n]) {
    vector_tail[T](n, xs).entry(i) = xs.entry(fin_cast_suc(n, i))
}

theorem transport_preserves_vector_tail[T](m: Nat, n: Nat, xs: Vector[T, suc(m)]) {
    m = n implies true
} by {
    if m = n {
        let ys: Vector[T, suc(n)] = transport xs
        let xt: Vector[T, m] = vector_tail[T](m, xs)
        let yt: Vector[T, n] = vector_tail[T](n, ys)
        let zt: Vector[T, n] = transport xt
        forall(i: Fin[m], j: Fin[n]) {
            if i.value = j.value {
                fin_cast_suc_value(m, i)
                fin_cast_suc_value(n, j)
                fin_cast_suc(m, i).value = fin_cast_suc(n, j).value
                yt.entry(j) = ys.entry(fin_cast_suc(n, j))
                xt.entry(i) = xs.entry(fin_cast_suc(m, i))
                ys.entry(fin_cast_suc(n, j)) = xs.entry(fin_cast_suc(m, i))
                yt.entry(j) = xt.entry(i)
            }
        }
    }
}
```

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

### Evaluate performance

Source: https://github.com/acornprover/acorn/blob/master/CLAUDE.md

Build in release mode and measure execution time for performance-sensitive changes.

```bash
cargo build --profile release
```

```bash
time cargo run --profile release -- check
```

```bash
time cargo run --profile release -- reprove real.double_sum
```

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

### Execute Project Load Profiling

Source: https://github.com/acornprover/acorn/blob/master/PROFILE.md

Builds the profile_load binary and executes it with time tracking to measure project loading performance.

```bash
cargo build --profile release --bin profile_load
/usr/bin/time -v target/release/profile_load
```

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

### Implement Parameterized Instance Schemes

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Shows how to define and use parameterized instances for typeclasses.

```acorn
    typeclass F: Field {
        one: F
    }

    typeclass G: Group {
        id: G
    }

    type Foo: axiom
    let foo: Foo = axiom

    instance Foo: Field {
        let one: Foo = foo
    }

    structure NonZero[T] {
        value: T
    }

    instance NonZero[F: Field]: Group {
        let id: NonZero[F] = NonZero[F].new(Field.one[F])
    }

    theorem goal {
        Group.id[NonZero[Foo]] = Group.id[NonZero[Foo]]
    }
```

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

### Run Acorn Performance Benchmarks

Source: https://github.com/acornprover/acorn/blob/master/PROFILE.md

Commands to build the project and execute performance checks with timing enabled for both single and multi-threaded scenarios.

```bash
cargo build --profile release
/usr/bin/time -v target/release/acorn check --jobs 1 --timing
/usr/bin/time -v target/release/acorn check --jobs 20 --timing
RUSTFLAGS="-C force-frame-pointers=yes" cargo build --bin=acorn --profile=fastdev
perf record -e cycles:u -g --call-graph fp -o perf.data target/fastdev/acorn check --jobs 1 --timing
```

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

### Using Typeclass Theorems

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Illustrates how axioms defined on typeclasses can be applied to specific instances within a proof.

```acorn
    typeclass F: Foo {
        foo: F -> Bool
    }

    axiom always_foo[F: Foo](x: F) {
        x.foo
    }

    inductive Bar {
        bar
    }

    let qux: Bool = axiom

    instance Bar: Foo {
        define foo(self) -> Bool {
            qux
        }
    }

    theorem goal {
        qux
    } by {
        Foo.foo(Bar.bar)
    }
    
```

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

### Define Proof Inside Forall Block

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/proof_blocks.md

Shows how to structure a proof within a forall quantification block.

```acorn
type Thing: axiom
let t: Thing = axiom
let foo: Thing -> Bool = axiom
axiom foo_t { foo(t) }
forall(x: Thing) {
    x = t implies foo(x)
}
```

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

### Match Branches in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Demonstrates using match expressions with local let bindings to handle Option types.

```acorn
type Nat: axiom

inductive Option[T] {
    none
    some(T)
}

define local_match(opt: Option[Nat], fallback: Nat) -> Nat {
    match opt {
        Option.none {
            let y = fallback
            y
        }
        Option.some(x) {
            let z: Nat = x
            z
        }
    }
}

theorem local_match_none(fallback: Nat) {
    local_match(Option.none[Nat], fallback) = fallback
}

theorem local_match_some(x: Nat, fallback: Nat) {
    local_match(Option.some(x), fallback) = x
}
```

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

### Boolean Equality Axioms

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/equality.md

Demonstrates defining boolean axioms and proving equality between them.

```acorn
let a: Bool = axiom
let b: Bool = axiom
axiom {
    a implies b
}
axiom {
    b implies a
}
theorem goal {
    a = b
}
```

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

### Replay Generic Partial Application Certificate

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Demonstrates theorem proving with generic types and partial function application.

```acorn
inductive Point {
    point
}

define constant[T, U](u: U, t: T) -> U {
    u
}

define apply_fn[T, U](f: T -> U, x: T) -> U {
    f(x)
}

theorem partial_constant_replay(a: Point, x: Point) {
    apply_fn(constant[Point, Point](a), x) = a
}
```

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

### Prove With Imported Existential

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/search.md

Demonstrates a basic existential proof using an axiom to satisfy a theorem goal.

```acorn
        type Nat: axiom

        let f: Nat -> Bool = axiom

        axiom exists_a_fa {
            exists(a: Nat) { f(a) }
        }

        theorem goal {
            exists(a: Nat) { f(a) }
        }
```

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

### Execute release script

Source: https://github.com/acornprover/acorn/blob/master/RELEASE.md

Run the primary release script to bump versions and trigger build processes.

```bash
./scripts/release.sh
```

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

### Local Let With Proof In If Expression

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/transport.md

Demonstrates using transport within an if-expression, requiring a proof of equality between the source and target types.

```acorn
type Nat: axiom

structure Box[n: Nat] {
    value: Nat
}

axiom branch_equal(p: Bool, n: Nat, k: Nat) {
    p implies n = k
}

define local_transport_if_with_proof(p: Bool, n: Nat, k: Nat, box: Box[n], fallback: Nat) -> Nat {
    if p {
        let y: Box[k] = transport box by {
            branch_equal(p, n, k)
        }
        y.value
    } else {
        fallback
    }
}

theorem local_transport_if_with_proof_then(
    p: Bool,
    n: Nat,
    k: Nat,
    box: Box[n],
    fallback: Nat
) {
    p implies local_transport_if_with_proof(p, n, k, box, fallback) = box.value
}
```

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

### Build ONNX Runtime for Windows

Source: https://github.com/acornprover/acorn/blob/master/WINDOWS.md

Execute this command from the onnxruntime directory to build the runtime with static MSVC runtime support.

```powershell
./build.bat --config Release --parallel --skip_tests --enable_msvc_static_runtime --cmake_generator "Visual Studio 17 2022"
```

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

### Generate Proof with Forall Goal

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Demonstrates a theorem involving nested implications and universal quantification.

```acorn
            type Nat: axiom
            let f: Nat -> Bool = axiom
            let g: Nat -> Bool = axiom
            let h: Nat -> Bool = axiom
            axiom fimpg { forall(x: Nat) { f(x) implies g(x) } }
            axiom gimph { forall(x: Nat) { g(x) implies h(x) } }
            theorem goal { forall(x: Nat) { f(x) implies h(x) } }
```

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

### Proof Condensing Combining Two Theorems

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Shows how to combine multiple axioms to prove a target theorem.

```acorn
        type Nat: axiom
        let a: Nat = axiom
        let f: Nat -> Bool = axiom
        let g: Nat -> Bool = axiom
        axiom fimpg(x: Nat) { f(x) implies g(x) }
        axiom fa { f(a) }
        theorem goal { g(a) }
```

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

### Define Complex Attributes and Prove Theorems

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Shows how to define attributes using existential quantifiers and prove a theorem by manually satisfying the attribute conditions.

```acorn
    inductive Color {
        red
        blue
    }

    structure Set[K] {
        contains: K -> Bool
    }

    attributes Set[Color] {
        define has_red(self) -> Bool {
            exists(a: Color) {
                self.contains(Color.red)
            }
        }

        define has_non(self, c: Color) -> Bool {
            exists(a: Color) {
                self.contains(a) and a != c
            }
        }

        define red_splits(self) -> Bool {
            self.has_red and self.has_non(Color.red)
        }
    }

    define true_fn(c: Color) -> Bool {
        true
    }

    let universal = Set.new(true_fn)

    theorem goal {
        universal.red_splits
    } by {
        let b = Color.blue
        universal.contains(b) and b != Color.red
        universal.has_non(Color.red)
        universal.contains(Color.red)
        universal.has_red
    }
    
```

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

### Cite a Parametric Theorem in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/verification.md

Demonstrates defining a parametric theorem and invoking it within a goal.

```acorn
type Nat: axiom
let zero: Nat = axiom
theorem foo[T](a: T) { a = a }
theorem goal { foo(zero) }
```

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

### Prove With Unifying Closures

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/normalization.md

Shows how the prover handles closure unification within axioms and theorems.

```acorn
    type Nat: axiom
    let foo: (Nat -> Nat) -> Bool = axiom
    let bar: (Nat, Nat) -> Nat = axiom

    axiom ax(a: Nat) {
        foo(function(b: Nat) {
            bar(b, a)
        })
    }

    theorem goal(a: Nat) {
        foo(function(b: Nat) {
            bar(b, a)
        })
    } by {
        ax(a)
    }
    
```

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

### Utilize Instance Forwards

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Demonstrates how the prover utilizes instance relationships in proofs when extending typeclasses.

```acorn
    typeclass F: Foo {
        property: Bool
    }

    typeclass B: Bar extends Foo {
        vacuous_condition(b: B) {
            b = b
        }
    }

    type MyType: axiom

    let b: Bool = axiom

    instance MyType: Foo {
        let property: Bool = b
    }

    axiom ax[B: Bar] {
        B.property
    }

    instance MyType: Bar

theorem goal {
    MyType.property
}
    
```

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

### Build Acorn Language Server

Source: https://github.com/acornprover/acorn/blob/master/WINDOWS.md

Execute this script from the acorn directory to perform the final release build.

```powershell
./winbuild.bat
```

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

### Instantiate typeclasses with generic parameters

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Shows how to define a typeclass with an operation and instantiate it for a specific inductive type using a generic equality function.

```acorn
    typeclass F: Foo {
        op: (F, F) -> Bool

        self_true(x: F) {
            x.op(x)
        }
    }

    define equals[T](x: T, y: T) -> Bool {
        x = y
    }

    inductive Color {
        red
        blue
    }

    instance Color: Foo {
        let op: (Color, Color) -> Bool = equals
    }
    
```

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

### Functional Substitution in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Demonstrates defining axioms and theorems involving functional mapping and finding minimums.

```acorn
            type Nat: axiom
            define find(f: Nat -> Bool) -> Nat { axiom }
            define is_min(f: Nat -> Bool) -> (Nat -> Bool) { axiom }
            define gcd_term(p: Nat) -> (Nat -> Bool) { axiom }
            let p: Nat = axiom
            let f: Nat -> Bool = is_min(gcd_term(p))
            theorem goal { find(is_min(gcd_term(p))) = find(f) }
```

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

### Generate Training Shards

Source: https://github.com/acornprover/acorn/blob/master/python/README.md

Converts trace files into binary shards for training. Supports positive-preserving negative sampling or uniform reservoir sampling.

```bash
uv run acorn-build-scorer-shards TRACE... \
  --max-negatives 20000000 \
  --shard-rows 1000000 \
  --workers 0 \
  --out ../tmp/shards
```

```bash
uv run acorn-build-scorer-shards TRACE... \
  --sample-records 5000000 \
  --shard-rows 1000000 \
  --out ../tmp/shards
```

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

### Semantics of Let Satisfy Syntax

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Demonstrates the use of the satisfy keyword to define a witness that meets specific constraints.

```acorn
    type Nat: axiom
    let zero: Nat = axiom
    let one: Nat = axiom
    axiom zero_neq_one {
        zero != one
    }

    let witness: Nat satisfy {
        witness != one
    }

    theorem goal {
        witness != one
    }
    
```

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

### Proving With Generic Structure

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Shows how to define a generic structure and prove a theorem about its attribute methods.

```acorn
    structure Pair[T, U] {
        first: T
        second: U
    }

    attributes Pair[T, U] {
        define swap(self) -> Pair[U, T] {
            Pair.new(self.second, self.first)
        }
    }

    theorem swap_def[T, U](p: Pair[T, U]) {
        p.swap = Pair.new(p.second, p.first)
    }
```

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

### Unwrap Option in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/normalization.md

Demonstrates the syntax for defining inductive types and structures with constraints, followed by an option unwrapping pattern.

```acorn
    type Nat: axiom
    let zero: Nat = axiom
    let foo: Nat -> Bool = axiom

    inductive Option[T] {
        some(T)
        none
    }

    // TODO: move this after FooNat once empty constrained types are allowed
    axiom foo_zero {
        foo(zero)
    }

    structure FooNat {
        n: Nat
    } constraint {
        foo(n)
    }

    let Option.some(bar) = FooNat.new(zero)
```

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

### Extracting Narrow Proof in Acorn

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Demonstrates defining axioms and theorems to establish a chain of implications.

```acorn
            let b: Bool = axiom
            let f1: Bool -> Bool = axiom
            let f2: Bool -> Bool = axiom
            let f3: Bool -> Bool = axiom
            let f4: Bool -> Bool = axiom
            axiom a1 { f1(b) }
            axiom a12(x: Bool) { f1(x) implies f2(x) }
            axiom a23(x: Bool) { f2(x) implies f3(x) }
            axiom a34(x: Bool) { f3(x) implies f4(x) }
            theorem goal(x: Bool) { f4(b) }
```

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

### Basic Unification

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Illustrates the use of existential quantification and axiom-based unification.

```acorn
            type Nat: axiom
            let zero: Nat = axiom
            let f: (Nat, Nat) -> Bool = axiom
            axiom f_zero_right(x: Nat) { f(x, zero) }
            theorem goal { exists(x: Nat) { f(zero, x) } }
```

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

### Normalizing Instance Aliases

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Illustrates the use of instance aliases to map typeclass methods to defined attributes.

```acorn
    typeclass M: Magma {
        mul: (M, M) -> M
    }

    inductive Foo {
        foo
    }

    attributes Foo {
        define mul(self, other: Foo) -> Foo {
            Foo.foo
        }
    }

    instance Foo: Magma {
        let mul: (Foo, Foo) -> Foo = Foo.mul
    }

    theorem goal(a: Foo) {
        Magma.mul(a, a) = a * a
    }
```

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

### Verify Complicated Theorem Application

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Demonstrates the use of transitive axioms to prove a relationship between three variables.

```acorn
            type Nat: axiom
            let a: Nat = axiom
            let b: Nat = axiom
            let c: Nat = axiom
            let f: (Nat, Nat) -> Bool = axiom
            axiom trans(x: Nat, y: Nat, z: Nat) {
                f(x, y) and f(y, z) implies f(x, z)
            }
            axiom fab { f(a, b) }
            axiom fbc { f(b, c) }
            theorem goal {
                f(a, c)
            }
            
```

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

### Verify Existence Theorem

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Shows how to prove an existential statement based on an axiom involving an implication.

```acorn
            type Nat: axiom
            let a: Nat = axiom
            let f: Nat -> Bool = axiom
            let g: (Nat, Nat) -> Bool = axiom
            axiom foo(x: Nat) {
                f(x) implies exists(y: Nat) { g(x, y) and g(y, x) }
            }
            theorem goal {
                f(a) implies exists(y: Nat) { g(a, y) and g(y, a) }
            }
            
```

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

### Run standard development checks

Source: https://github.com/acornprover/acorn/blob/master/CLAUDE.md

Execute these commands before finalizing any Rust code changes to ensure quality and formatting.

```bash
cargo test
```

```bash
cargo check
```

```bash
cargo fmt
```

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

### Run Markdown Prover Tests

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/README.md

Executes the full suite of Markdown-based prover tests using cargo.

```sh
cargo test mdtests
```

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

### Branch-Local Satisfy in Theorem Claims

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Demonstrates how branch-local witnesses in theorem and proof-block claims are handled to ensure synthetic witnesses are not exposed directly.

```acorn
type Empty: axiom
let empty: Empty = axiom

define absurd(e: Empty) -> Bool {
    true
}

theorem theorem_claim {
    if true {
        let x: Empty satisfy {
            true
        }
        absurd(x)
    } else {
        true
    }
}

theorem proof_claim {
    true
} by {
    if true {
        let x: Empty satisfy {
            true
        }
        absurd(x)
    } else {
        true
    }
}
```

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

### Verify Functional Existence

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/search.md

Demonstrates resolution involving functional existence and free variables.

```acorn
        type Nat: axiom
        let is_min: (Nat -> Bool, Nat) -> Bool = axiom
        let foo: Nat -> (Nat -> Bool) = axiom
        axiom has_min(f: Nat -> Bool, n: Nat) {
            f(n) implies exists(m: Nat) { is_min(f, m) }
        }
        axiom foo_is_true_somewhere(a: Nat) {
            exists(b: Nat) { foo(a, b) }
        }
        let min_foo(a: Nat) -> b: Nat satisfy {
            is_min(foo(a), b)
        }
        
```

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

### Build Scorer Shards

Source: https://github.com/acornprover/acorn/blob/master/python/README.md

Converts raw trace files into binary shards for efficient training, allowing for negative sample limiting and parallel processing.

```bash
cd python
uv run acorn-build-scorer-shards \
  ../tmp/acorn-eval-latest/traces/depth-first-[0-9][0-9][0-9][0-9][0-9][0-9].jsonl.zst \
  ../tmp/acorn-eval-latest/traces/onnx-[0-9][0-9][0-9][0-9][0-9][0-9].jsonl.zst \
  ../tmp/acorn-eval-latest/traces/onnx-no-shallow-[0-9][0-9][0-9][0-9][0-9][0-9].jsonl.zst \
  ../tmp/acorn-eval-latest/traces/trained-5m-[0-9][0-9][0-9][0-9][0-9][0-9].jsonl.zst \
  ../tmp/acorn-eval-latest/traces/trained-5m-no-shallow-[0-9][0-9][0-9][0-9][0-9][0-9].jsonl.zst \
  --out ../tmp/shards/model-YYYYMMDD-latest-allpos-neg20m \
  --max-negatives 20000000 \
  --shard-rows 1000000 \
  --workers 0 \
  --overwrite
```

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

### Verify Constraint Theorem

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/constraints.md

Demonstrates a theorem proving that a structure satisfies its defined constraint.

```acorn
structure Foo {
    first: Bool
    second: Bool
} constraint {
    first or second
}
theorem goal(f: Foo) {
    f.first or f.second
}
```

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

### Destructuring with Explicit Proof

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Demonstrates using a proof block to satisfy a pattern match requirement when destructuring an Option type.

```acorn
type Nat: axiom

inductive Option[T] {
    none
    some(T)
}

axiom every_option_some(y: Option[Nat]) {
    exists(x: Nat) {
        Option.some(x) = y
    }
}

define local_unwrap_with_proof(y: Option[Nat]) -> Nat {
    let Option.some(x) = y by {
        every_option_some(y)
    }
    x
}

theorem local_unwrap_with_proof_some(n: Nat) {
    local_unwrap_with_proof(Option.some(n)) = n
}
```

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

### Verify Partial Application Theorem Citation

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/normalization.md

Shows how to cite a theorem that relies on specific attributes and axioms for partial application proofs.

```acorn
        type Ix: axiom
        type Val: axiom

        attributes Ix {
            define lte(self, other: Ix) -> Bool { axiom }
        }

        attributes Val {
            define lte(self, other: Val) -> Bool { axiom }
        }

        define good(a: Ix -> Val) -> Bool {
            true
        }

        axiom base_distant(a: Ix -> Val, m: Ix, n: Ix) {
            m <= n implies a(m) <= a(n)
        }

        theorem distant(a: Ix -> Val, m: Ix, n: Ix) {
            good(a) and m <= n implies a(m) <= a(n)
        } by {
            if good(a) and m <= n {
                base_distant(a, m, n)
                a(m) <= a(n)
            }
        }

        theorem goal(f: (Ix, Ix) -> Val, i: Ix, m: Ix, n: Ix) {
            m <= n implies f(i, m) <= f(i, n)
        } by {
            if m <= n {
                good(f(i))
                distant(f(i), m, n)
                f(i, m) <= f(i, n)
            }
        }
        
```

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

### Destructuring Structure

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Shows how to destructure and reconstruct a custom structure using local let bindings.

```acorn
type Nat: axiom

structure Pair {
    first: Nat
    second: Nat
}

define local_pair_rebuild(a: Nat, b: Nat) -> Pair {
    let Pair.new(x, y) = Pair.new(a, b)
    Pair.new(x, y)
}

theorem local_pair_rebuild_reduces(a: Nat, b: Nat) {
    local_pair_rebuild(a, b) = Pair.new(a, b)
}
```

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

### Let Satisfy With Explicit Proof

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Provides an explicit proof block to satisfy a variable constraint.

```acorn
type Nat: axiom

axiom equal_witness_exists(n: Nat) {
    exists(x: Nat) {
        x = n
    }
}

define local_satisfy_with_proof(n: Nat) -> Nat {
    let x: Nat satisfy {
        x = n
    } by {
        equal_witness_exists(n)
    }
    x
}

theorem local_satisfy_with_proof_reduces(n: Nat) {
    local_satisfy_with_proof(n) = n
}
```

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

### Prove theorems with multiple type variables

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Illustrates the use of inductive types with type parameters and axioms to prove equality in a theorem block.

```acorn
    inductive Nil[T] {
        nil
    }

    let map[T, U]: (Nil[T], T -> U) -> Nil[U] = axiom
    let morph[T]: Nil[T] -> Nil[T] = axiom

    theorem goal[T, U](items: Nil[T], f: T -> U) {
        map(items, f) = morph(map(items, f))
    } by {
        map(items, f) = Nil.nil[U]
        morph(map(items, f)) = Nil.nil[U]
    }
    
```

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

### Use Parameterized Attributes

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Illustrates defining attributes with generic parameters and calling them using both type-based and object-based syntax.

```acorn
    structure BoolPair {
        first: Bool
        second: Bool
    }

    attributes BoolPair {
        define apply_first<T>(self, f: Bool -> T) -> T {
            f(self.first)
        }
    }

    theorem type_attr_syntax(b: BoolPair, f: Bool -> Bool) {
        BoolPair.apply_first(b, f) = f(b.first)
    }

    theorem obj_attr_syntax(b: BoolPair, f: Bool -> Bool) {
        b.apply_first(f) = f(b.first)
    }

    structure Pair<T, U> {
        first: T
        second: U
    }

    attributes Pair<T, U> {
        define map_first<V>(self, f: T -> V) -> V {
            f(self.first)
        }
    }

    theorem type_attr_generic<A, B, C>(p: Pair<A, B>, f: A -> C) {
        Pair.map_first(p, f) = f(p.first)
    }

    theorem obj_attr_generic<A, B, C>(p: Pair<A, B>, f: A -> C) {
        p.map_first(f) = f(p.first)
    }
```

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

### Verify CUDA Environment

Source: https://github.com/acornprover/acorn/blob/master/python/README.md

Checks PyTorch version and CUDA availability to ensure the environment is correctly configured for GPU training.

```bash
cd python
uv run python -c "import torch; print(torch.__version__); print(torch.cuda.is_available()); print(torch.cuda.get_device_name(0) if torch.cuda.is_available() else 'no cuda')"
```

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

### Prove statements with BoxedBool

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/normalization.md

Demonstrates normalization by proving a theorem involving a boxed boolean structure.

```acorn
    structure BoxedBool {
        value: Bool
    }

    define boxed_and(a: BoxedBool, b: BoxedBool) -> BoxedBool {
        BoxedBool.new(a.value and b.value)
    }

    theorem goal(b: BoxedBool) {
        not b.value implies not boxed_and(b, b).value
    }
    
```

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

### Instance Condition with Operator Witnesses

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Shows how instance conditions replay nested existential witnesses when refuting universally quantified operator expressions.

```acorn
    typeclass A: Add {
        add: (A, A) -> A
    }

    typeclass A: LTE {
        lte: (A, A) -> Bool
    }

    type Real: axiom

    let real_add: (Real, Real) -> Real = axiom
    let real_lte: (Real, Real) -> Bool = axiom
    let d: (Real, Real) -> Real = axiom

    instance Real: Add {
        let add: (Real, Real) -> Real = real_add
    }

    instance Real: LTE {
        let lte: (Real, Real) -> Bool = real_lte
    }

    axiom d_triangle(x: Real, y: Real, z: Real) {
        d(x, z) <= d(x, y) + d(y, z)
    }

    typeclass M: Metric {
        distance: (M, M) -> Real

        triangle(x: M, y: M, z: M) {
            x.distance(z) <= x.distance(y) + y.distance(z)
        }
    }

    instance Real: Metric {
        let distance: (Real, Real) -> Real = d
    }
```

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

### Implement nested branch-local satisfy conditions

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Shows that a local let-satisfy condition can contain its own branch-local local witnesses.

```acorn
type Empty: axiom
let empty: Empty = axiom

define absurd(e: Empty) -> Bool {
    true
}

define nested_satisfy(flag: Bool) -> Bool {
    let x: Bool satisfy {
        if true {
            let e: Empty satisfy {
                true
            }
            absurd(e)
        } else {
            true
        }
    }
    x
}
```

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

### Prove With Match Statement

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Demonstrates using a match statement within a theorem proof to handle different inductive cases.

```acorn
    type Nat: axiom
    attributes Nat {
        define suc(self) -> Nat { axiom }
    }

    inductive Int {
        from_nat(Nat)
        neg_suc(Nat)
    }

    define abs_case_1(a: Int, n: Nat) -> Bool {
        a = Int.from_nat(n)
    }

    define abs_case_2(a: Int, n: Nat) -> Bool {
        exists(k: Nat) {
            a = Int.neg_suc(k) and n = k.suc
        }
    }

    define abs(a: Int) -> Nat {
        match a {
            Int.from_nat(n) {
                n
            }
            Int.neg_suc(k) {
                k.suc
            }
        }
    }

    theorem goal(a: Int) {
        abs_case_1(a, abs(a)) or abs_case_2(a, abs(a))
    } by {
        match a {
            Int.from_nat(n) {
                abs_case_1(a, abs(a))
            }
            Int.neg_suc(k) {
                abs_case_2(a, abs(a))
            }
        }
    }
```

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

### Define Multivar Let Satisfy Syntax

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Demonstrates the use of the satisfy keyword to define constraints on multiple variables.

```acorn
    type Nat: axiom
    let zero: Nat = axiom
    let one: Nat = axiom
    axiom zero_neq_one {
        zero != one
    }

    let (x: Nat, y: Nat) satisfy {
        x != y
    }

    theorem goal {
        x != y
    }
    
```

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

### Execute full reprove

Source: https://github.com/acornprover/acorn/blob/master/CLAUDE.md

Run a full reprove to identify obscure bugs, noting that this process is slow and may result in unverified propositions.

```bash
cargo run --profile release --features validate -- reprove
```

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

### Proof Indirect From Goal

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Demonstrates an indirect proof approach involving multiple implications.

```acorn
            type Nat: axiom
            let f: Nat -> Bool = axiom
            let g: Nat -> Bool = axiom
            let h: Nat -> Bool = axiom
            axiom fimpg(x: Nat) { f(x) implies g(x) }
            axiom gimph(x: Nat) { g(x) implies h(x) }
            axiom fimpnh(x: Nat) { f(x) implies not h(x) }
            theorem goal(x: Nat) { not f(x) }
```

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

### Define Body with Local Lets

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/local_lets.md

Basic usage of local let bindings within a function definition.

```acorn
type Nat: axiom

define local_identity(n: Nat) -> Nat {
    let x = n
    let y: Nat = x
    y
}

theorem local_identity_reduces(n: Nat) {
    local_identity(n) = n
}
```

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

### Local Let With Explicit Proof

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/transport.md

Shows a standard transport operation where an explicit axiom provides the proof for type conversion.

```acorn
type Nat: axiom

structure Box[n: Nat] {
    value: Nat
}

axiom all_equal(n: Nat, k: Nat) {
    n = k
}

define local_transport_with_proof(n: Nat, k: Nat, box: Box[n]) -> Nat {
    let y: Box[k] = transport box by {
        all_equal(n, k)
    }
    y.value
}

theorem local_transport_with_proof_value(n: Nat, k: Nat, box: Box[n]) {
    local_transport_with_proof(n, k, box) = box.value
}
```

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

### Claim Before Explicit False with Inconsistent Assumptions

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/basics.md

Shows how claims are handled when assumptions are inconsistent, allowing for vacuous proofs before an explicit false.

```acorn
            let a: Bool = axiom
            let b: Bool = axiom
            axiom a_eq_b { a = b }
            if a != b {
                // This claim should succeed - the assumptions are inconsistent,
                // so any claim is vacuously true. The prover will find the inconsistency
                // when trying to prove "a = b implies a = a", but since `false` comes
                // later, this should be allowed.
                a = b implies a = a
                false
            }
```

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

### Nested Static Attribute Certificate Replay

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Demonstrates using nested structures and static attributes to facilitate theorem unfolding.

```acorn
    inductive MyList[T] {
        nil
        cons(T, MyList[T])
    }

    structure Box[T] {
        items: MyList[T]
    }

    define box_from_list[T](items: MyList[T]) -> Box[T] {
        Box.new(items)
    }

    attributes Box[T] {
        let from_list: MyList[T] -> Box[T] = box_from_list
    }

    define nested_list[A](items: MyList[A]) -> MyList[Box[A]] {
        MyList.nil[Box[A]]
    }

    define nested_box[A](items: MyList[A]) -> Box[Box[A]] {
        Box.from_list[Box[A]](nested_list[A](items))
    }

    theorem nested_box_unfold[A](items: MyList[A]) {
        nested_box[A](items) = Box.from_list[Box[A]](nested_list[A](items))
    }
    
```

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

### Define Proof Inside Theorem Block

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/proof_blocks.md

Demonstrates embedding a proof block directly after a theorem definition.

```acorn
type Thing: axiom
let t: Thing = axiom
theorem reflexivity(x: Thing) {
    x = x
} by {
    reflexivity(t)
}
```

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

### Define Proof Inside If Block

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/language/proof_blocks.md

Illustrates the usage of proof blocks within conditional logic.

```acorn
type Thing: axiom
forall(x: Thing, y: Thing) {
    if x = y {
        x = y
    }
}
```

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

### Prove With Parameterized Constant

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/typeclasses.md

Uses a typeclass to define a parameterized constant and proves equality between two instances.

```acorn
    typeclass P: PointedSet {
        point: P
    }

    let get_point1[P: PointedSet]: P = P.point
    let get_point2[P: PointedSet]: P = P.point

    theorem goal[P: PointedSet] {
        get_point1[P] = get_point2[P]
    }
    
```

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

### Implement Generic Attribute Match

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/attributes.md

Shows how to define a generic map attribute for an inductive Option type and verify it with a theorem.

```acorn
    inductive Option<T> {
        none
        some(T)
    }

    attributes Option<T> {
        define map<U>(self, f: T -> U) -> Option<U> {
            match self {
                Option.none {
                    Option.none<U>
                }
                Option.some(t) {
                    Option.some(f(t))
                }
            }
        }
    }

    theorem goal<T, U>(t: T, f: T -> U) {
        Option.some(t).map(f) = Option.some(f(t))
    }
```

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

### Proof Condensing Induction

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/proof_generation.md

Demonstrates the use of induction axioms to prove properties over natural numbers.

```acorn
        type Nat: axiom
        let zero: Nat = axiom
        let suc: Nat -> Nat = axiom
        axiom induction(f: Nat -> Bool) {
            f(zero) and forall(k: Nat) { f(k) implies f(suc(k)) } implies forall(n: Nat) { f(n) }
        }
        let foo: Nat -> Bool = axiom
        theorem goal { foo(zero) and forall(k: Nat) { foo(k) implies foo(suc(k)) } implies forall(n: Nat) { foo(n) } }
```

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

### Transporting Functions Over Indexed Structures

Source: https://github.com/acornprover/acorn/blob/master/src/tests/prover/mdtest/transport.md

Shows how to transport a function over an indexed structure when the indices are proven equal.

```acorn
type Nat: axiom
type Item: axiom

structure Fin[n: Nat] {
    value: Nat
}

theorem goal(n: Nat, k: Nat, v: Fin[n] -> Item) {
    n = k implies true
} by {
    if n = k {
        let w: Fin[k] -> Item = transport v
        forall(i: Fin[n], j: Fin[k]) {
            i.value = j.value implies w(j) = v(i)
        }
    }
}
```