ProofForge

CosmWasm

wasm-validated-alpha · check + mock + wasmd rung-1

目标

cosmwasm

族

Wasm 宿主

轨道

engineering

成熟度

wasm-validated-alpha · check + mock + wasmd rung-1

主制品

WAT/Wasm + CosmWasm package

工具锁定

wat2wasm + cosmwasm-check + mock 语料；wasmd Docker rung-1

可部署

true

Feature 清单

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

7

合计

3

已支持

2

部分

1

显式拒绝

1

缺失

跨链对照：目标矩阵

执行模型

Cosmos Wasm 宿主

消息驱动合约；SubMsg schedule 语义 PARTIAL。

Alpha 标签

registry 成熟度 wasm-validated-alpha——不是 formal SupportClaim。

窄容器面

Map/Bytes 通常 FC；以公共 UInt 路径为主。

wasmd rung-1

Docker 工程观察——非主网证据。

制品

文件角色
*.wat / wasm + check artifacts主制品

Feature 列表

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

流水线

CosmWasmPlan → WAT → check/mock/wasmd。

2/4 已支持

  • SUPPORTED

    UInt 公共 MVP

    state/param/result UInt8..64 + 带检查算术 + 控制流。

  • SUPPORTED

    cosmwasm-check + mock

    锁定工程语料（约 28 项 mock 级）。

  • FAIL-CLOSED

    Map / Bytes / 宽整数

    MVP 面之外。

  • MISSING

    主网 / formal

    未声称。

副作用

emit/revert/assert；schedule 经 SubMsg 为 PARTIAL。

1/3 已支持

  • SUPPORTED

    emit / revert / assert

    attributes / ContractResult::Err 路径。

  • PARTIAL

    schedule（SubMsg）

    reply 路径语义 PARTIAL。

  • PARTIAL

    contextRead

    instantiate/execute 子集上的 unixTime/blockHeight/caller。

Profile

cosmwasm-wasm-u64-v1

公共 UInt8/16/32/64 MVP；标签 wasm-validated-alpha。

构建

lake env .lake/build/bin/proof-forge-next build \
  Examples/Counter.lean \
  --module Examples.Counter \
  --target cosmwasm -o build/counter-cosmwasm
开放名单 →目标矩阵 →