Aleo 专区

可移植 DSL → Aleo Instructions。Feature 清单、制品、profile 与诚实成熟度——源码发射 + 锁定 Leo 仅编译。

目标

aleo

族

ZK 应用链

Leo

4.0.2

域

BLS12-377 Fr

主制品

Aleo Instructions (.aleo)

轨道

engineering 已实现（scope ADR 未闭合）

可部署

false

成熟度

源码发射 + 锁定编译

Feature 清单

本专区记录的 Aleo 产品面计数（不是营销分数）。

合计

已支持

部分

显式拒绝

缺失

跨链对照：目标矩阵

执行模型（Leo 4）

Aleo 将私有证明执行与公开上链 finalization 分开。ProofForge 把可移植语义物化进该模型，不虚构 prove/deploy 成熟度。

私有证明上下文

Leo 4 fn 在链下运行。私有 transition 先落在这里。

公开 finalization

final {} / final fn 仅在 finalization 接受时提交 public mapping。

Record ≠ mapping

属主绑定的 record（custody/consume/nonce）与 public mapping 是不同轴。泛化 private 不能推导 record custody。

Instructions 优先 IR

产品主制品是 .aleo Instructions（官方中间 IR）。Leo 源仅用于对照/调试。

制品

文件	角色	说明
{programId}.aleo	产品主制品	Aleo Instructions 文本（官方中间 IR）。Plan → LowerPlanV1。Counter ≡ 锁定 golden。
{programId}.aleo-query-contract.json	旁路制品	网络状态描述：public mapping、bare view、resultDropped。内容哈希闭合。不是可执行 query。
{programId}.leo	调试 / 对照	Leo 4 源码。PROOF_FORGE_ALEO_EMIT_LEO=1 或 compile profile 双写。不是长期唯一权威。
.compiled.aleo · .abi.json · .leo-program.json	编译附加	仅在显式 compile profile 且锁定离线 leo build 后产出。deployable=false。

已支持 feature 列表

今天哪些可移植 DSL 能力能 lower 到 Aleo、哪些显式拒绝、哪些仍缺失。词汇与工程矩阵一致。

IR 与流水线

产品主制品是 Aleo Instructions，不是以 Leo 为唯一权威。Plan 身份绑定内容 digest。

6/8 已支持

SUPPORTED
Target-owned AleoPlan
ALEO-I1
planFromCapability 读取 CompiledSemanticV1；私有 lowering 构建 AleoPlan（绝非 NoirPlan / PsyPlan）。
SUPPORTED
Aleo Instructions 主发射
IR-0..IR-7 / G5-HARD
LowerPlanV1 → {id}.aleo。G5-HARD 空 residual 白名单：Plan 已准入但 lower 失败 → ALEO-IR-G5-HARD（禁止静默 Leo-only 主制品）。
SUPPORTED
规范 Plan 内容 digest
ALEO-I1
pf.aleo-plan.engineering.v1 绑定进 Registry / BuildIdentity。
SUPPORTED
query-contract 旁路
ALEO-I2
有序第二基础制品。固定键网络状态描述；不是 leo query / 不是编译器输入。
PARTIAL
Leo 4 调试发射
可选 .leo 供锁定 leo 对照（env / emitLeoDebug / 编译双写）。仅过渡用途。
SUPPORTED
Leo 4.0.2 Tool Lock（双平台）
ALEO-I3 / Tool Lock v4
darwin-arm64 + linux-x86_64 digest；无 PATH/cargo/brew 回退；隔离 HOME；leo build --offline --disable-update-check。
SUPPORTED
可选编译 finalize
ALEO-I4
Profile aleo-leo-4.0.2-u64-compile-v1 与 source profile 共享 Plan；发布三份内容绑定附加制品；缺工具 → fail closed 零发布。
MISSING
snarkVM / prove / deploy 运行时
ALEO-IR-7 / RPT-024
just aleo-runtime → PF-TOOLCHAIN-MISSING。无锁定 snarkOS/snarkVM/CRS。deployable=false。leo run 仅为解释器——不是 Instructions 运行时。

标量与域

核心整数包络 + Aleo 原生 BLS12-377 域。

4/7 已支持

SUPPORTED
UInt64 / UInt32 / UInt8
状态、算术、比较、位运算、移位、逻辑、pureCall 路径。
SUPPORTED
Int64
状态 / 算术 / 比较包络（G5-HARD Int64 路径）。
SUPPORTED
Bool / Unit
逻辑运算、断言、unit 返回。
SUPPORTED
Field BLS12-377 Fr
T14
精确 FieldSpec → Leo field；fieldAdd/Sub/Mul/Div/Neg。
FAIL-CLOSED
Field bn254
在 Aleo 上显式拒绝（请用 BLS12-377）。
FAIL-CLOSED
Field Goldilocks
Psy 侧域；非 Aleo。
FAIL-CLOSED
UInt128 / UInt256
宽整数未在 Aleo 产品路径开放。

聚合与容器

面向 Aleo 公共存储的 flatten-to-mapping 物化。

5/7 已支持

SUPPORTED
命名 Struct / Enum
H3
construct / fieldGet / fieldSet / variantTag / variantPayload（H3）。
SUPPORTED
Array UInt64
H3 / N-ANON-RESULT
状态 flatten-to-mapping + 索引操作；匿名 Array 结果 ≤8 叶。
SUPPORTED
dense Map UInt64（cap-2）
MapSnapshot
occ/key/val 叶；IndexGet→Option；IndexSet upsert；storeAggregate 先 get 再 set 快照。
SUPPORTED
定长 Bytes N
N×u8 mapping + 带检查 u8 通道。动态 Bytes 索引 FC。
SUPPORTED
Option UInt64 状态
BL-35
tag+payload 双 mapping；entry 面 match。Option 参数 / 嵌套 / 非 UInt64 仍 FC。
FAIL-CLOSED
String 状态 / match
未在 Aleo 开放。
FAIL-CLOSED
Principal 状态/参数
Aleo 上 pilotPrincipalPolicyNone。

控制流与纯计算

Instructions 诚实 lower if/match/for；无静默部分操作码。

6/6 已支持

SUPPORTED
pureCall / 本地 fn
产品 lower 路径内联纯函数。
SUPPORTED
if / match
Instructions 中 branch.eq / position；同构造器多臂经 Normalize。
SUPPORTED
有界 for
静态 for 展开进 Instructions。
SUPPORTED
assertOp / bare assert
产品路径带检查断言。
SUPPORTED
bare revert
相对 effect 诚实矩阵：bare revert 为 LOWERED。
SUPPORTED
Op.Constant 字面量内联
ALEO-CONST
字面量 Constant → Plan lowerLiteral → Instructions immediate。

副作用、资产与上下文

Aleo 模型不同：私有证明 vs 公开 finalization。许多副作用按设计保持 fail-closed。

1/7 已支持

SUPPORTED
commit 身份透传
产品路径身份 commit。
FAIL-CLOSED
emit
Plan 级 fail-closed（effect 诚实矩阵）。
FAIL-CLOSED
externalCall（同步）
resolver + plan 拒绝；不做 PARTIAL 假 Yes。
FAIL-CLOSED
schedule（异步）
resolver + plan 拒绝。
FAIL-CLOSED
contextRead
Aleo 产品路径无 unixTime / blockHeight / caller。
FAIL-CLOSED
pf.assets（5 个 QN）
ADR-0029 Phase D
零绑定：Aleo 资产模型是 record custody，不是账户余额金库。未绑定 → PF-REQ-UNSUPPORTED。
MISSING
record mint / consume custody
设计为未来 custody v2 种子（PfAssetsDispositionV1）。尚未产品化。

ABI 与返回

entry/view 返回面，对 computed-view 保持诚实。

2/3 已支持

SUPPORTED
命名聚合 entry 返回
非 Final 的 entry 元组叶。
SUPPORTED
匿名 Array / Option 返回
Array UInt64 N≤8 / Option UInt64；Map/Bytes 结果 FC。
FAIL-CLOSED
基于状态的 computed view
仅准入 bare view；多叶 computed view FC。

Profile

source (default)

零工具 finalize。产出 .aleo + .aleo-query-contract.json。

aleo-leo-4.0.2-u64-compile-v1

锁定离线 leo build。同一 Plan digest；增加 compiled.aleo / abi.json / leo-program.json 附加制品。

构建

# Portable Counter → Aleo Instructions package
lake env .lake/build/bin/proof-forge-next build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target aleo \
  -o build/counter-aleo

# Optional Leo 4 source for locked-leo compare
PROOF_FORGE_ALEO_EMIT_LEO=1 \
  lake env .lake/build/bin/proof-forge-next build \
    Examples/Counter.lean \
    --module Examples.Counter \
    --target aleo \
    -o build/counter-aleo-leo

Aleo dApp 前端（Wallet Adapter）

远程 MCP 打包 PRODUCT-ALEO-DAPP-FRONTEND-WALLET，并指向仓库模板 templates/aleo-dapp-ui（钱包 + StateCell UI）。PF 不 vendor/pin @provablehq 包，也不在浏览器代签。

templates/aleo-dapp-ui

templates/aleo-dapp-ui 在 GitHub 打开 →

Feature 清单

执行模型（Leo 4）

私有证明上下文

公开 finalization

Record ≠ mapping

Instructions 优先 IR

制品

已支持 feature 列表

IR 与流水线

Target-owned AleoPlan

Aleo Instructions 主发射

规范 Plan 内容 digest

query-contract 旁路

Leo 4 调试发射

Leo 4.0.2 Tool Lock（双平台）

可选编译 finalize

snarkVM / prove / deploy 运行时

标量与域

UInt64 / UInt32 / UInt8

Int64

Bool / Unit

Field BLS12-377 Fr

Field bn254

Field Goldilocks

UInt128 / UInt256

聚合与容器

命名 Struct / Enum

Array UInt64

dense Map UInt64（cap-2）

定长 Bytes N

Option UInt64 状态

String 状态 / match

Principal 状态/参数

控制流与纯计算

pureCall / 本地 fn

if / match

有界 for

assertOp / bare assert

bare revert

Op.Constant 字面量内联

副作用、资产与上下文

commit 身份透传

emit

externalCall（同步）

schedule（异步）

contextRead

pf.assets（5 个 QN）

record mint / consume custody

ABI 与返回

命名聚合 entry 返回

匿名 Array / Option 返回

基于状态的 computed view

Profile

构建

Aleo dApp 前端（Wallet Adapter）