Aleo for Agents is offline at present

blog·2026-10-12·11 min read

Project of the Week: Build an Aleo Execution-Key Preflight Planner

Introduction

Aleo proving workers have an awkward habit: they discover expensive work after accepting the job.

Process::execute needs a proving key for every function request in an authorization. When a record crosses call.dynamic, it also needs a record translation key. Missing keys are synthesized and cached during execution, which can turn an ordinary request into a sudden burst of CPU time and memory allocation.

That is too late for an operator to make a sensible scheduling decision.

snarkVM PR #3524 adds Process::execution_keys. Given an authorization, the API reports the complete set of required keys, their kinds, and whether each key is absent from the current Process cache. No proof is generated during inspection.

I like the boundary here. Authorization determines the execution graph, while proving consumes expensive cryptographic material for that graph. A worker should inspect the graph between those two stages.

The planner we build will:

  • Load the root program and its runtime-selected callee.
  • Authorize a concrete execution without proving it.
  • Sort every required key into a stable manifest.
  • Reject the job when its cold-key count or estimated memory exceeds a configured budget.

The estimates are operator policy, not protocol facts. Key sizes vary with circuit shape, and a deserialized proving key may have a different allocation profile from a freshly synthesized one. Measure your own workloads rather than copying my defaults into production.

What we're building

Our fixture has two Leo programs.

warm_token.aleo mints a private Ticket record and exposes forward, which accepts a dyn record. preflight_router.aleo chooses the token program at runtime and sends the record through a dynamic call. The router also increments public storage in its final { } block so the fixture covers current state syntax.

That route requires at least the root function key and the dynamically selected callee's function key. Because a record crosses call.dynamic, snarkVM also reports the applicable translation material.

The Rust binary produces JSON like this:

json
{
  "program": "preflight_router.aleo",
  "function": "route",
  "cold_keys": 3,
  "estimated_cold_mib": 704,
  "allowed": false,
  "keys": [
    {
      "locator": "preflight_router.aleo/route",
      "kind": "function",
      "missing": true,
      "estimated_mib": 256
    }
  ]
}

A rejected plan never reaches Process::execute. Your scheduler can send it to a warm-up queue, move it onto a larger worker, or decline it before synthesis begins.

The cache status is process-local. Starting the CLI in a fresh process means every uncached artifact starts cold. A production prover should run the same planner inside its resident worker after loading persisted keys into that worker's Process.

Prerequisites

Use Leo 4.4.x and the snarkVM branch containing PR #3524. Rust should match the toolchain pinned by that snarkVM checkout.

bash
leo --version
rustc --version
cargo --version

git clone [https://github.com/ProvableHQ/snarkVM.git](https://github.com/ProvableHQ/snarkVM.git) vendor/snarkVM
cd vendor/snarkVM
git fetch origin pull/3524/head:execution-keys
git checkout execution-keys
cd ../..

The tutorial uses a local path dependency so Cargo builds against the exact checkout you inspected. After the PR lands, pin the merged commit in your own repository instead of tracking a moving branch.

Create the workspace:

bash
mkdir -p execution-key-planner/fixtures/warm_token/src
mkdir -p execution-key-planner/fixtures/preflight_router/src
mkdir -p execution-key-planner/planner/src
cd execution-key-planner

The resulting layout is:

text
execution-key-planner/
  fixtures/
    warm_token/
      program.json
      src/main.leo
    preflight_router/
      program.json
      src/main.leo
  planner/
    Cargo.toml
    src/main.rs
  vendor/
    snarkVM/

If you cloned vendor/snarkVM beside the project rather than inside it, adjust the dependency path in Cargo.toml.

Step-by-step

1. Build the record program

Create fixtures/warm_token/program.json:

json
{
  "program": "warm_token.aleo",
  "version": "0.1.0",
  "description": "Dynamic-record fixture for execution-key planning",
  "license": "MIT",
  "leo": "4.4.0",
  "dependencies": null,
  "dev_dependencies": null
}

Create fixtures/warm_token/src/main.leo:

leo
program warm_token.aleo {
    record Ticket {
        owner: address,
        amount: u64,
    }

    fn mint(receiver: address, amount: u64) -> Ticket {
        return Ticket {
            owner: receiver,
            amount: amount,
        };
    }

    fn forward(input: dyn record, expected_owner: address) -> dyn record {
        assert_eq(input.owner, expected_owner);
        return input;
    }

    @noupgrade
    constructor() {}
}

Ticket has the mandatory owner: address field. mint gives us a concrete record for local testing. forward deliberately uses dyn record, so a runtime-selected call can receive a record whose concrete program type was not part of the router's static import graph.

The owner assertion is useful. It forces the callee to inspect the dynamic record instead of acting as a meaningless pass-through.

Build and run it:

bash
cd fixtures/warm_token
leo build
leo run mint \
  aleo1rhgdu77hgyqd3xjj8ucu3jj9r2krwz6mnzyd80gncr5fxcwlh5rsvzp9px \
  25u64
cd ../..

Save the returned record plaintext. We will call it $TICKET below.

2. Build the dynamic router

Create fixtures/preflight_router/program.json:

json
{
  "program": "preflight_router.aleo",
  "version": "0.1.0",
  "description": "Runtime router used by the execution-key planner",
  "license": "MIT",
  "leo": "4.4.0",
  "dependencies": null,
  "dev_dependencies": null
}

Create fixtures/preflight_router/src/main.leo:

leo
interface Forwarder {
    fn forward(input: dyn record, expected_owner: address) -> dyn record;
}

program preflight_router.aleo {
    storage routed_count: u64;

    fn route(
        target: identifier,
        input: dyn record,
        expected_owner: address,
    ) -> (dyn record, Final) {
        let output: dyn record = Forwarder@(target)::forward(
            input,
            expected_owner,
        );

        return (output, final {
            routed_count = routed_count.unwrap_or(0u64) + 1u64;
        });
    }

    @noupgrade
    constructor() {}
}

The Forwarder interface fixes the callable signature. It does not prove that every runtime program is a good implementation. The selected program still has to be loaded, the function signature must match, and dynamic field reads may halt if the record layout is wrong.

Forwarder@(target)::forward compiles to a dynamic call. Since input crosses that call as a record, the execution needs translation material in addition to ordinary function keys.

The storage write belongs in final { }. routed_count is public state and never enters the private proof-side record data.

Build the router:

bash
cd fixtures/preflight_router
leo build
cd ../..

Run it with the compiled callee loaded at runtime:

bash
export OWNER=aleo1rhgdu77hgyqd3xjj8ucu3jj9r2krwz6mnzyd80gncr5fxcwlh5rsvzp9px
export TICKET='<paste the complete record returned by leo run mint>'

cd fixtures/preflight_router
leo run route \
  "'warm_token'" \
  "$TICKET" \
  "$OWNER" \
  --with ../warm_token/build/main.aleo
cd ../..

--with matters because dynamic callees are not ordinary manifest dependencies. The router's source does not import warm_token.aleo, so the VM needs the compiled callee supplied at runtime. That separation is the composability boundary discussed in the earlier stub-ordering post.

3. Create the Rust planner

Create planner/Cargo.toml:

toml
[package]
name = "execution-key-planner"
version = "0.1.0"
edition = "2024"

[dependencies]
anyhow = "1"
clap = { version = "4", features = ["derive"] }
rand = "0.8"
serde = { version = "1", features = ["derive"] }
serde_json = "1"
snarkvm = { path = "../vendor/snarkVM" }

Create planner/src/main.rs:

rust
use anyhow::{bail, Context, Result};
use clap::Parser;
use rand::thread_rng;
use serde::Serialize;
use snarkvm::prelude::{
    CurrentAleo, CurrentNetwork, Identifier, PrivateKey, Process, Program,
    ProgramID, Value,
};
use std::{fs, path::PathBuf, str::FromStr};

#[derive(Parser)]
struct Args {
    #[arg(long)]
    private_key: String,

    #[arg(long)]
    program: String,

    #[arg(long)]
    function: String,

    #[arg(long = "load", required = true)]
    programs: Vec<PathBuf>,

    #[arg(long = "input")]
    inputs: Vec<String>,

    #[arg(long, default_value_t = 2)]
    max_cold_keys: usize,

    #[arg(long, default_value_t = 256)]
    function_mib: u64,

    #[arg(long, default_value_t = 192)]
    translation_mib: u64,

    #[arg(long, default_value_t = 512)]
    max_cold_mib: u64,

    #[arg(long, default_value = "warmup-manifest.json")]
    output: PathBuf,
}

#[derive(Serialize)]
struct PlannedKey {
    locator: String,
    kind: String,
    missing: bool,
    estimated_mib: u64,
}

#[derive(Serialize)]
struct Plan {
    program: String,
    function: String,
    cold_keys: usize,
    estimated_cold_mib: u64,
    max_cold_keys: usize,
    max_cold_mib: u64,
    allowed: bool,
    keys: Vec<PlannedKey>,
}

fn main() -> Result<()> {
    let args = Args::parse();
    let mut process = Process::<CurrentNetwork>::load()?;

    for path in &args.programs {
        let source = fs::read_to_string(path)
            .with_context(|| format!("reading {}", path.display()))?;
        let program = Program::<CurrentNetwork>::from_str(&source)
            .with_context(|| format!("parsing {}", path.display()))?;
        process.add_program(&program)?;
    }

    let private_key = PrivateKey::<CurrentNetwork>::from_str(&args.private_key)?;
    let program_id = ProgramID::<CurrentNetwork>::from_str(&args.program)?;
    let function = Identifier::<CurrentNetwork>::from_str(&args.function)?;
    let inputs = args
        .inputs
        .iter()
        .map(|value| Value::<CurrentNetwork>::from_str(value))
        .collect::<Result<Vec<_>, _>>()?;

    let authorization = process.authorize::<CurrentAleo, _>(
        &private_key,
        program_id,
        function,
        inputs.iter(),
        &mut thread_rng(),
    )?;

    let execution_keys = process.execution_keys(&authorization)?;
    let mut keys = Vec::with_capacity(execution_keys.len());

    for key in execution_keys {
        let kind_debug = format!("{:?}", key.kind());
        let is_translation = kind_debug.contains("Translation");
        let kind = if is_translation {
            "record_translation"
        } else {
            "function"
        };
        let estimated_mib = if is_translation {
            args.translation_mib
        } else {
            args.function_mib
        };

        keys.push(PlannedKey {
            locator: key.locator().to_string(),
            kind: kind.to_owned(),
            missing: key.is_missing(),
            estimated_mib,
        });
    }

    keys.sort_by(|a, b| {
        a.kind
            .cmp(&b.kind)
            .then_with(|| a.locator.cmp(&b.locator))
    });

    let cold_keys = keys.iter().filter(|key| key.missing).count();
    let estimated_cold_mib = keys
        .iter()
        .filter(|key| key.missing)
        .map(|key| key.estimated_mib)
        .sum();
    let allowed = cold_keys <= args.max_cold_keys
        && estimated_cold_mib <= args.max_cold_mib;

    let plan = Plan {
        program: args.program,
        function: args.function,
        cold_keys,
        estimated_cold_mib,
        max_cold_keys: args.max_cold_keys,
        max_cold_mib: args.max_cold_mib,
        allowed,
        keys,
    };

    let json = serde_json::to_string_pretty(&plan)?;
    fs::write(&args.output, format!("{json}\n"))?;
    println!("{json}");

    if !allowed {
        bail!("execution exceeds the configured warm-up budget");
    }

    Ok(())
}

The planner authorizes first because dynamic targets and concrete records live in the authorization. Inspecting the root function name alone cannot reveal the full execution graph.

execution_keys walks that authorization and checks the current process cache. We then add local memory estimates, sort by kind and locator, and serialize the result. Sorting keeps the manifest stable across runs, which makes it suitable for CI diffs and deployment review.

The small Debug conversion around kind() keeps this sample independent of enum spelling while PR #3524 is under review. Once your pinned snarkVM revision has settled, match its public kind enum directly and let the compiler reject any new key category.

Build the CLI:

bash
cd planner
cargo build --release
cd ..

4. Run the preflight

Use the published Leo dev key only for local work:

bash
export PRIVATE_KEY=APrivateKey1zkp8CZNn3yeCseEtxuVPbDCwSyhGW6yZKUYKfgXmcpoGPWH
export OWNER=aleo1rhgdu77hgyqd3xjj8ucu3jj9r2krwz6mnzyd80gncr5fxcwlh5rsvzp9px
export TICKET='<paste the complete record returned by leo run mint>'

./planner/target/release/execution-key-planner \
  --private-key "$PRIVATE_KEY" \
  --program preflight_router.aleo \
  --function route \
  --load fixtures/warm_token/build/main.aleo \
  --load fixtures/preflight_router/build/main.aleo \
  --input "'warm_token'" \
  --input "$TICKET" \
  --input "$OWNER" \
  --max-cold-keys 4 \
  --function-mib 256 \
  --translation-mib 192 \
  --max-cold-mib 1024 \
  --output warmup-manifest.json

Program load order is dependency order. Our fixture has no static imports, but loading the runtime callee before the router makes the intended setup plain.

A cold process should report missing entries. Run the planner inside a resident process with keys already inserted and the same locators should become warm. Recreating Process for every invocation throws that cache state away.

Testing

Start with a budget that cannot pass:

bash
set +e
./planner/target/release/execution-key-planner \
  --private-key "$PRIVATE_KEY" \
  --program preflight_router.aleo \
  --function route \
  --load fixtures/warm_token/build/main.aleo \
  --load fixtures/preflight_router/build/main.aleo \
  --input "'warm_token'" \
  --input "$TICKET" \
  --input "$OWNER" \
  --max-cold-keys 0 \
  --max-cold-mib 0 \
  --output rejected.json
status=$?
set -e

test "$status" -ne 0

The command still writes rejected.json. Operators need the reason for refusal, not a silent nonzero exit.

Check deterministic output by running twice against equivalent fresh processes:

bash
cp rejected.json first.json

set +e
./planner/target/release/execution-key-planner \
  --private-key "$PRIVATE_KEY" \
  --program preflight_router.aleo \
  --function route \
  --load fixtures/warm_token/build/main.aleo \
  --load fixtures/preflight_router/build/main.aleo \
  --input "'warm_token'" \
  --input "$TICKET" \
  --input "$OWNER" \
  --max-cold-keys 0 \
  --max-cold-mib 0 \
  --output second.json
set -e

diff -u first.json second.json

Finally, inspect whether a translation row exists:

bash
jq -e '.keys[] | select(.kind == "record_translation")' first.json

If that query finds nothing, inspect the compiled router and confirm that it contains a dynamic call carrying a record:

bash
grep -n "call.dynamic" fixtures/preflight_router/build/main.aleo

Do not treat max-cold-keys as a memory limit. A tiny circuit and a large circuit each count as one function key. Keep the memory budget too, then replace the sample estimates with measurements from your exact programs and snarkVM build. The benchmark harness from September's project is a good place to collect synthesis time and peak RSS.

What's next

The useful production shape is a resident proving service with two queues: admitted jobs and warm-up work. Authorization enters the planner, cold manifests go to the warm-up queue, and only jobs within policy reach proving.

Persist each manifest beside the program edition and circuit identity. A locator by itself is not enough after an upgrade changes the circuit behind a familiar function name.

I would also record actual synthesis duration and RSS delta per locator. Feed those observations back into the next budget calculation instead of maintaining one estimate for every function. Translation keys deserve their own measurements because their cost follows record layouts rather than ordinary function complexity.

Prepared program contexts solve repeated parsing and import setup, as covered in the reusable proving-context tutorial. Execution-key preflight solves a different problem: deciding whether the worker can afford the cryptographic artifacts required by one concrete authorization.

Keep those layers separate. A prepared program can still have cold proving material, and a warm key cache does not mean the runtime-selected program graph was loaded correctly.

The final deployment rule is blunt: never let an uninspected authorization choose how much proving-key memory your worker allocates. Call execution_keys, compare the cold set with policy, and synthesize on your schedule.