共享合约场景：Counter

状态：草案规范 (Phase 1–2) Counter 场景是第一个跨目标验收标准测试。它在 Lean 业务核心中练习可移植标量状态，而不涉及特定于链的账户模型。相关：可移植 IR, 能力注册表, Decisions。

场景定义

一个合约维护单个无符号 64 位计数器。

v0 不需要原生代币转账、跨合约调用或事件（v1 中可选 events.emit）。

能力 id	使用者
`storage.scalar`	所有操作
`caller.sender`	v1 中的可选访问控制

每个目标适配器将相同的逻辑场景映射到原生机制：

目标	状态表示	冒烟测试
`evm`	合约存储槽	Foundry + `vm.etch`
`wasm-cosmwasm`	宿主 KV 中的字符串键 `"count"`	`cosmwasm-check` + instantiate/execute/query
`solana-sbpf-asm`	账户数据字段	`sbpf test` (Mollusk) + Surfpool/Web3.js live smoke
`move-aptos`	签名者账户下的 `Counter` 资源	`aptos move test`
`psy-dpn`	Psy 存储字段，在 v0 中可能是 `Felt`/`U32`	`dargo compile` + 内存冒烟测试

目标特定的账户 schema 和 manifest 是适配器关注点——不会隐藏在可移植 Lean 逻辑内部。有关指令 manifest 格式和 direct-assembly 路线（D-026），请参阅 solana-sbpf-asm.md。

当两个并行 spike 独立通过时，Phase 2 即告完成：

--emit-sbpf-asm 产生可被 sbpf build 接受的有效 .s。
sbpf build 产生可加载的 eBPF ELF (.so)。
在 sbpf test (Mollusk) 和 Surfpool/Web3.js live smoke 中执行 initialize → increment → read counter。
指令 manifest (manifest.toml) 记录账户布局。
能力检查器用包含 target id 的诊断拒绝不支持的能力。

psy-dpn 不属于 Phase 2 退出标准，但它现在已经通过生成 .psy 源码和 Dargo 验证复用了 Counter 场景。

Counter IR 可以用 Psy 兼容的标量类型表示。
生成的 .psy 包可以使用 dargo compile 编译。
发射 DPN 电路 JSON 并记录在制品元数据中。
冒烟路径已经可运行，覆盖 dargo test、dargo compile、 dargo execute、dargo generate-abi 和制品元数据校验。

目标	路径	状态
EVM	`Examples/Evm/Contracts/Counter.lean`	代码库中
CosmWasm	`Examples/CosmWasm/Counter.lean`	已规划，不在代码库中
Solana	`Examples/Solana/Counter.lean` + manifest	已规划，不在代码库中（工作流 7）
Aptos	`Examples/Move/Aptos/Counter/`	已规划，不在代码库中
Psy DPN	`Examples/Psy/.golden.psy`, `scripts/psy/-smoke.sh`	代码库中