Aleo Leo Target

Status: Spike (local smoke exists — scripts/aleo/counter-smoke.sh)

Status: Spike (local smoke exists — scripts/aleo/counter-smoke.sh)

Candidate target id: aleo-leo

This note records the first ProofForge classification for Aleo and the implemented Road 1 spike. It does not add a Lean target profile yet; the spike validates the Leo source-generation boundary before any code registry changes.

Primary deliverables:

• ProofForge.Backend.Aleo.IR lowers the portable IR Counter fixture to Leo.
• proof-forge --emit-counter-ir-leo emits Counter.leo.
• Examples/Aleo/Counter.golden.leo is the tracked golden fixture.
• scripts/aleo/counter-smoke.sh generates a Leo package, runs leo build and leo test, writes proof-forge-artifact.json, and validates the metadata.
• ProofForge.Compiler.Leo.Emit additionally supports pure entrypoints with parameters/return values and control-flow statements (assert, if/else, boundedFor, assign, assignOp).
• proof-forge --emit-pure-math-ir-leo emits PureMath.leo.
• Examples/Aleo/PureMath.golden.leo is the tracked golden fixture.
• scripts/aleo/pure-math-smoke.sh validates the PureMath fixture end-to-end.

Primary sources:

• Aleo getting started
• Leo installation
• Aleo Instructions overview
• Public & Private State
• Programs
• Transactions
• Leo finalization model
• Leo CLI overview
• leo build
• leo execute
• leo test

Local Smoke

The Road 1 spike is validated end-to-end by:

./scripts/aleo/counter-smoke.sh

Prerequisites:

• Lean toolchain from lean-toolchain and a built proof-forge binary.
• python3 for package/manifest helpers.
• leo CLI on PATH (tested with Leo 4.0.2); if leo is missing, the script reports the generated Counter.leo and exits with code 127.

What it proves:

• Portable IR ProofForge.IR.Examples.Counter lowers to a Leo 4.0 program with a public mapping, @noupgrade constructor, and fn ... -> Final entry points whose final blocks read/write the mapping.
• Generated Leo source matches the tracked golden fixture Examples/Aleo/Counter.golden.leo.
• leo build produces Aleo Instructions (build/main.aleo) and ABI JSON (build/abi.json).
• leo test passes.
• proof-forge-artifact.json is produced and schema-validated.

What it does not prove:

• Private records, transitions, or proof generation.
• Direct Aleo Instructions generation.
• Devnet deployment or execute transactions.
• Cross-target equivalence with EVM/Psy Counter semantics.
• A standalone .avm bytecode file; the current leo build output embeds VM artifacts in the compiled package rather than emitting a separate file.

Classification

Aleo is a ZK-native smart-contract L1. It is not the same kind of target as Zcash, Psy/DPN, or Starknet.

The better first classification is:

Aleo ZK application sourcegen target
  with Leo as the first source-generation boundary
  with Aleo Instructions as the lower-level compiler target
  with Aleo VM bytecode, prover/verifier artifacts, ABI, and transaction proofs

Aleo is “ZK” because program execution is split between:

• proof context: private, off-chain execution that can consume/create records and generate ZK proofs;
• finalization context: public, on-chain execution that reads/writes mappings, storage variables, and storage vectors.

That means Aleo is closer to a privacy-aware contract chain than to a plain ZK circuit output target. ProofForge should model Aleo programs as deployable program packages, not just as circuits.

Why This Is Not The Same As Existing ZK Targets

Existing ProofForge ZK-related notes cover different shapes:

• psy-dpn: target source compiles to DPN circuit JSON artifacts.
• zcash-shielded: ZK proves protocol-defined shielded payment statements.
• kaspa-toccata: an L1 covenant may verify a proof inline or settle based-app state.
• starknet-cairo: Cairo contracts compile through Sierra/CASM; Starknet is not modeled as a generic circuit target.

Aleo needs its own family because:

• Leo programs are smart contracts with program ids, imports, entry functions, records, mappings, finalization logic, and deploy/execute transactions;
• private state uses records, which are encrypted and UTXO-like;
• public state uses mappings/storage updated by validators in final logic;
• execute transactions contain transitions and ZK proofs;
• build outputs include .aleo instructions, ABI, prover/verifier files, and Aleo VM bytecode;
• local validation can use leo build, leo test, leo execute, and devnet deployment flows.

Candidate Target Family

Do not add this to ProofForge.Target.Registry until the target model can express Aleo’s proof/finalization split and record/mapping state split.

Candidate family:

zk-app-sourcegen

Candidate backend pattern:

ProofForge portable IR subset
  -> generated Leo package
  -> leo build
  -> Aleo Instructions (.aleo)
  -> Aleo VM bytecode + ABI + prover/verifier artifacts
  -> leo test / leo execute / leo devnet validation metadata

Direct Aleo Instructions generation is a later road. It is attractive for a compiler backend, but Leo is the safer first artifact because it is the recommended developer language and exposes program structure more clearly.

Candidate artifact shape:

aleo-leo-package
  - generated Leo source
  - program id and imports
  - record / mapping / storage schema
  - proof-context entry functions
  - finalization manifest
  - compiled Aleo Instructions
  - AVM bytecode
  - ABI JSON
  - prover and verifier artifacts
  - execute/deploy transaction metadata
  - test/devnet validation result

Candidate Capabilities

These are research candidates, not canonical capability ids yet.

Candidate capability	Meaning
lang.leo	Target emits Leo source packages.
ir.aleo_instructions	Build emits or consumes Aleo Instructions.
vm.aleo_avm	Target runs on the Aleo VM, not Algorand AVM.
artifact.avm	Build emits Aleo VM bytecode.
artifact.aleo_abi	Build emits Aleo ABI metadata.
proof.prover_key	Build or execute flow produces prover artifacts.
proof.verifier_key	Build or deploy flow records verifier artifacts.
execution.transition	Entry execution produces a transition and proof.
execution.finalize	Program has public on-chain finalization logic.
state.record	Private state is held in encrypted records.
state.mapping	Public state is held in mappings.
state.storage	Public state may use storage variables or storage vectors.
input.private	Function input is private proof-context data.
input.public	Function input is public data.
output.private	Function output is private by default.
output.public	Function output is public.
program.import	Program imports and calls another Aleo program.
program.upgrade	Deployment may support explicit program upgrades.
transaction.execute	Validation can produce an execute transaction.
transaction.deploy	Validation can produce or inspect a deploy transaction.
fee.credits	Fees are paid in Aleo Credits, publicly or privately.
test.leo	Validation uses Leo tests.
test.aleo_devnet	Validation uses Leo devnet or devnode-backed flows.

zk.circuit alone is not sufficient for Aleo. It may describe the proof aspect, but Aleo also needs program, state, transaction, and finalization capabilities.

Implementation Roads

Road 1: Leo Sourcegen Package

Use this road first.

First spike:

• choose a tiny Counter-like program;
• generate Leo source with one entry fn and one final { } block;
• use a public mapping for the counter;
• run leo build and record .aleo, ABI, bytecode, and toolchain metadata;
• run leo test, with --prove as an optional heavier gate.

This validates the compiler boundary without taking responsibility for Aleo VM internals.

Road 2: Private Record Flow

Use this road to validate Aleo’s ZK-specific value proposition.

First spike:

• define a simple private record type;
• consume one record and create one successor record in a proof-context entry function;
• keep record contents private while exposing only required public outputs or finalize effects;
• run leo execute --print or SDK-backed execution to inspect transaction and proof metadata.

This is the path that proves Aleo support is more than an account-chain source generator.

Road 3: Direct Aleo Instructions

Use this road only after Leo sourcegen proves the semantics.

First spike:

• lower a tiny typed IR fixture directly to .aleo instructions;
• preserve public/private input annotations;
• generate or validate prover/verifier artifacts through the official toolchain;
• compare output against Leo-generated Aleo Instructions for the same behavior.

This road is useful for compiler precision, but it has a larger semantic surface than Leo sourcegen.

Non-Goals For The First Pass

• Do not add aleo-leo to the code registry before candidate capabilities are reviewed.
• Do not classify Aleo as only a generic ZK circuit target.
• Do not confuse Aleo VM with Algorand AVM.
• Do not model records as EVM storage or as Zcash shielded notes.
• Do not model final blocks as private execution; finalization is public and on-chain.
• Do not claim full Aleo support until there is a reproducible local build/test command.
• Do not start with direct Aleo Instructions if Leo sourcegen is enough to validate the first spike.

Research Exit Criteria

Aleo can leave Research only when we have:

• a reviewed target profile proposal;
• a committed capability proposal for Leo, Aleo Instructions, Aleo VM bytecode, transitions, finalization, records, mappings, proofs, ABI, fees, and devnet validation;
• a minimal artifact manifest schema for Leo source, compiled outputs, prover/verifier artifacts, ABI, and transaction/deploy metadata;
• a toolchain decision for local validation using Leo CLI, SDK, devnet, or devnode;
• one reproducible local command or script that validates a tiny Leo program package, even if proving-heavy gates are optional in CI.

Status: The Road 1 spike satisfies the reproducible local command and artifact manifest schema criteria. The remaining criteria (target profile, full capability proposal, devnet validation) stay open until private records and transitions are reviewed.

Research Exit Plan

A detailed design spec covering Research exit + Road 1 spike is in docs/superpowers/specs/2026-07-01-aleo-leo-design.md.

The spec finalizes:

• Target family: zk-app-sourcegen.
• Canonical capabilities for the first spike: lang.leo, vm.aleo_avm, artifact.avm, artifact.aleo_abi, execution.finalize, state.mapping, input.public, output.public, test.leo.
• Research-only capabilities for future spikes: ir.aleo_instructions, proof.prover_key, proof.verifier_key, execution.transition, state.record, state.storage, input.private, output.private, program.import, program.upgrade, transaction.execute, transaction.deploy, fee.credits, test.aleo_devnet.
• Artifact manifest schema for aleo-leo-package.
• Toolchain decision: leo build + leo test primary; prove/execute optional.
• Spike scope: Road 1 only, public mapping Counter from ProofForge.IR.Examples.Counter.

The Road 1 spike is implemented; code registry changes (ProofForge.Target.Capability / ProofForge.Target.Registry) remain deferred until the proof/finalization split and private-record roadmap are reviewed.