ProofForge

Psy

source-only · 可选 dargo + host-heavy 本地 VM 路径

目标

psy

族

ZK 应用链

轨道

engineering

成熟度

source-only · 可选 dargo + host-heavy 本地 VM 路径

主制品

Dargo / Psy source

工具锁定

官方 dargo v0.1.0 + 捆绑 std（可选 runtime 非 ordinary CI）

可部署

false

Feature 清单

本目标的产品面计数（工程词汇，不是营销分数）。

13

合计

6

已支持

3

部分

3

显式拒绝

1

缺失

跨链对照：目标矩阵

执行模型

Goldilocks 域

T14 Field Goldilocks 已 lower；bn254/BLS FC。

可选 runtime 路径

just psy-runtime host-heavy Counter/WideCounter——非网络部署。

容器限制

Map/Bytes 状态 fail-closed；命名聚合 + Array 已开。

Engineering leaf

scope ADR 闭合前不扩成 accepted Phase 1。

制品

文件角色
Psy / Dargo sources主制品

Feature 列表

今天能 lower 什么、显式拒绝什么、仍缺失什么。

流水线与工具

PsyPlan → Dargo 源；可选锁定 dargo + runtime 脚本。

2/4 已支持

  • SUPPORTED

    源码物化

    registry 已实现 materializer。

  • SUPPORTED

    dargo 编译锁定

    官方 dargo v0.1.0 + 捆绑 std。

  • PARTIAL

    本地 VM / base-proof 路径

    可选 host-heavy just psy-runtime；非 ordinary CI；Darwin runtime 未充分实跑。

  • MISSING

    网络 UPS / deploy

    无产品网络闭环。

状态与类型

Goldilocks + 聚合；Map/Bytes/Principal FC。

2/4 已支持

  • SUPPORTED

    Field Goldilocks

    T14

    Psy 原生域算术。

  • SUPPORTED

    Struct/Enum/Array/Option

    H3 + Option UInt64 状态。

  • FAIL-CLOSED

    Map / Bytes 状态

    Psy 产品路径显式 fail-closed。

  • PARTIAL

    UInt128（VM profile）

    仅 psy-dargo-0.1.0-vm-v1 上 4×UInt32 limbs。

副作用

核心纯计算/控制流强；context/assets FC。

2/5 已支持

  • SUPPORTED

    pureCall / if / match / for

    产品 lower 路径。

  • SUPPORTED

    emit / revert / assert

    Psy 上已 lower。

  • FAIL-CLOSED

    contextRead

    Fail-closed。

  • PARTIAL

    externalCall

    __invoke_sync 源；语义 PARTIAL。

  • FAIL-CLOSED

    schedule

    Fail-closed。

Profile

psy-source-v1

默认源码发射（registry source-only）。

psy-dargo-0.1.0-vm-v1

更宽 UInt128 limb 面的 VM profile；host-heavy 可选 runtime。

构建

lake env .lake/build/bin/proof-forge-next build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target psy -o build/counter-psy

# optional host-heavy (not ordinary CI):
# just psy-runtime
开放名单 →目标矩阵 →