Implementation Backlog

Note: public validation command changes must update validation-gates.md in the same change.

This backlog turns the multi-chain design into reviewable engineering slices. It is intentionally scoped to local compiler, artifact, and smoke-test work. The cloud platform should wait until at least two materially different targets are working locally. Related docs:

Primary-chain completion covenant (D-045)

Before adding implementation scope for more chains, ProofForge must complete the three priority chains in this order:

solana-sbpf-asm — Solana direct sBPF assembly backend.
evm — Ethereum/EVM backend and deployment lane.
wasm-near — NEAR on the Wasm-family backend.

This is stronger than a research-roadmap preference. It is a product precondition tracked as Gate P0 in gate-status.md. “Complete” means target-first build/emission, local execution or deployment smoke, artifact/deploy metadata, capability diagnostics, resource budgets, CI coverage, and maintained docs for each of the three chains. New chains may receive docs-first research notes, and already-landed non-primary spikes may receive CI/security maintenance, but no additional chain should advance its registry stage, capability surface, testkit harness, or CI coverage before Gate P0 closes.

Workstream 1: Target Registry

Goal: make target selection explicit before adding more backends. Tasks:

Add target ids: evm, wasm-near, wasm-cosmwasm, solana-sbpf-asm, solana-sbpf-linker (superseded), solana-zig-fork, move-sui, move-aptos, psy-dpn.
Define target family, artifact kind, required tools, and capability set (see capability-registry.md).
Add a target lookup function for CLI and scripts.
Done: add an EVM-compatible chain profile layer for deployment metadata, starting with robinhood-chain-testnet under the evm compiler target.
Add diagnostics for unknown targets and unsupported capabilities.

Acceptance criteria:

evm can be represented as a target profile without changing current EVM behavior.
EVM-compatible chain profiles can reuse the evm compiler target without being returned by target-id lookup.
A target profile can declare external tool requirements.
Unsupported capability errors include target id, capability id, and source location when available.

Workstream 1.5: Portable IR and Shared Scenario

Goal: define the contract IR and Counter scenario before non-EVM spikes. Tasks:

Implement IR node types per portable-ir.md.
Express Counter per shared-scenario.md.
Lower Counter IR to EVM (directly or via EmitYul adapter).
Wire capability checker to capability-registry.md.

Acceptance criteria:

Counter module is representable in IR without EVM opcodes in the IR layer.
EVM build from IR matches existing Counter behavior.
At least one unsupported capability is rejected with a clear diagnostic.
IR version appears in artifact metadata when emitted.

Workstream 2: Artifact Metadata

See validation-gates.md for current and planned validation commands. Goal: every build should produce a machine-readable result that can later feed CI and the cloud platform. Tasks:

Done for EVM: add a proof-forge-artifact.json schema for EVM bytecode builds.
Done for EVM: emit metadata for --evm-bytecode and portable IR EVM bytecode fixture builds.
Done for EVM: include source module, target id, artifact paths, SHA-256, byte sizes, solc path/version, selector/signature metadata, and validation status.
Done for EVM: preserve SDK .evm-methods Solidity signatures in abi.methods[].signature for both proof-forge-artifact.json and proof-forge-deploy.json; validators check selector shape, duplicate method selectors/functions/signatures, generated Yul function names, and signature/arg-count consistency, and SDK example gates require signatures.
Done for EVM: emit and validate a ProofForge deploy manifest for every EVM bytecode build, recording runtime bytecode inputs, ABI selectors, deployable initcode, and the current not-generated transaction-broadcast status.
Done for EVM: generate an artifact-linked .init.bin creation bytecode file for each EVM bytecode build, record it in both proof-forge-artifact.json and proof-forge-deploy.json, and validate that the initcode header copies and returns the referenced runtime bytecode.
Done for EVM: add --evm-chain-profile <id> so bytecode builds can record a known EVM chain profile such as robinhood-chain-testnet or anvil-local in proof-forge-deploy.json; validators check profile id, chain id, RPC URLs, explorer, verifier, and deployment-block consistency without broadcasting.
Done for EVM: add --evm-constructor-args-hex <hex> so bytecode builds can append explicit ABI-encoded constructor arguments to generated .init.bin, record normalized hex/byte-size/SHA-256 constructor metadata in proof-forge-deploy.json, and validate that the initcode tail matches the manifest.
Done for EVM: add --evm-constructor-param <name:type> so bytecode builds can record static-word constructor ABI schema in artifact metadata and deploy manifests, validate supported schema types, and verify that an explicit ABI-encoded constructor-argument blob has the expected 32-byte word length.
Done for EVM: add --evm-constructor-arg <name=value> so bytecode builds can ABI-encode typed constructor values for uint256, uint64, uint32, bool, bytes32, and address, record whether constructor args came from typed values or raw hex, reject missing/duplicate/out-of-range values, and validate the generated initcode tail against metadata and deploy manifests.
Done for EVM: record structured portable IR selector-facing entrypoint ABI metadata in abi.entrypoints, including Solidity-style selector signatures, IR type names, ABI parameter/return types, flattened calldata word types/counts, and flattened return word types/counts; validators check selector/signature consistency with cast sig and EvmAbiAggregateProbe locks aggregate word layouts with --expect-entrypoint-abi.
Done for EVM: record portable IR event ABI metadata in abi.events, including Solidity-style event signatures, topic0, indexed/data fields, flattened ABI word types, and topic/data encodings; EventProbe validates every emitted event with --expect-event and cast keccak.
Done for EVM: extend scripts/evm/diagnostic-smoke.sh to lock constructor CLI diagnostics for unsupported dynamic constructor ABI types, missing or duplicate typed values, mixed typed/raw constructor argument sources, overflow, and malformed static-word values such as short addresses.
Done for EVM: add an Anvil deploy smoke that sends generated Counter .init.bin with cast send --create, records constructor ABI schema and typed constructor args plus a proof-forge-deploy-run.json artifact, records the eth_getTransactionByHash creation transaction JSON, validates the anvil-local chain profile, receipt/deployed address/runtime-code match and transaction input initcode, and exercises the Counter lifecycle over JSON-RPC.
Keep schema versioned from day one.

Acceptance criteria:

EVM bytecode build writes runtime bytecode, deployable initcode, metadata, and deploy manifest next to each other.
Metadata and deploy manifests can be parsed independently by CI scripts.
Portable IR bytecode metadata and deploy manifests can describe ABI-facing entrypoints, including selector signatures, flattened calldata word layout, and flattened return-data word layout.
Portable IR bytecode metadata and deploy manifests can describe ABI-facing events, including indexed topic encoding and non-indexed data-word encoding.
Deploy manifests can carry optional EVM chain profile metadata from the target registry while keeping transaction broadcast artifacts explicitly not-generated.
Local Anvil deployment can consume the generated deploy manifest and initcode, produce a validated deploy-run artifact, and prove the deployed runtime code matches the generated bytecode even when the initcode includes a typed or raw ABI-encoded constructor-argument tail with a recorded static constructor ABI schema; the deploy-run artifact also links the observed creation transaction JSON and validates that its input equals the generated initcode and that the deployment profile chain id matches the actual local chain.
EVM metadata can represent missing optional version data as null, not malformed metadata.

Workstream 3: EVM Baseline Hardening

See validation-gates.md for current and planned validation commands. Goal: keep EVM stable while the target model is introduced. Tasks:

Keep proof-forge --evm-bytecode working.
EVM semantic plan migration TODO:
- Done: make ModulePlan target-driven so helper planning is derived from Target.resolveModule/resolveSpec Target.evm before Yul generation.
- Split ProofForge.Backend.Evm.IR into Validate, Lower, ToYul, and Metadata modules while keeping IR.lean as a compatibility facade until callers have moved.
- Done: move scalar and map storage slot Yul construction to StorageSlotPlan -> ToYul, starting with map value/presence slots used by storage paths.
- Extend StorageSlotPlan -> ToYul to array slots and struct-array field slots, then remove the old direct slot-expression builders from IR.lean.
- Add ExprPlan and StmtPlan so expression and statement validation, helper discovery, and target-specific lowering happen before Yul AST assembly.
- Add EntrypointPlan for selector dispatch, calldata guards, ABI word flattening, return-data encoding, and metadata selector layout.
- Add EventPlan for event signature topics, indexed-topic hashing, non-indexed data flattening, and metadata event layout.
- Add CrosscallPlan for typed call, value-bearing call, staticcall, delegatecall, create, and create2 helpers.
- Add MetadataPlan and deploy-artifact planning so bytecode metadata, initcode, deployment manifests, and chain profile references are produced from the same semantic plan.
- Delete the old custom semantic IR.lean -> Yul lowering only after each migrated capability is covered by plan-level diagnostics, golden Yul, solc bytecode generation, Foundry smokes, artifact metadata validation, and the EVM IR coverage manifest.
- Keep ProofForge.Compiler.Yul.AST and ProofForge.Compiler.Yul.Printer; the migration replaces backend semantic lowering, not the target AST/printer boundary.
Done: add EVM IR diagnostic smoke so unsupported portable IR shapes fail before Yul generation with stable messages.
Done: add an EVM IR coverage manifest gate so every portable IR constructor must be classified as lowered, validated, unsupported, or structural for the EVM backend.
Done: add AbiScalarProbe for portable IR EVM scalar ABI parameter decoding over U64, U32, and Bool, with golden Yul, solc bytecode, and Foundry malformed-calldata validation.
Done: add EVM IR assert and assert_eq lowering as Yul revert guards, with AssertProbe golden Yul, solc bytecode, and Foundry success/revert validation.
Done: add EVM IR mutable scalar local bindings and local assignment lowering, with AssignmentProbe golden Yul, solc bytecode, and Foundry success/revert validation.
Done: add EVM IR local and scalar storage compound assignment lowering for all portable AssignOp variants, with EvmAssignOpProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, metadata capability validation, and explicit diagnostics for malformed targets/types.
Done: add EVM IR statement-level if/else lowering as Yul switch blocks, with ConditionalProbe golden Yul, solc bytecode, Foundry runtime validation, plus EVM-specific branch-local early-return validation through EvmLoopProbe.
Done: add EVM IR boundedFor lowering as Yul for loops with static bounds, with EvmLoopProbe golden Yul, solc bytecode, Foundry runtime/raw storage validation, metadata capability validation, branch-local and loop-local early-return lowering through Yul leave, and explicit invalid range diagnostics.
Done: add EVM IR context read lowering for userId, contractId, and checkpointId as Yul caller(), address(), and number(), with ContextProbe golden Yul, solc bytecode, Foundry runtime validation, and metadata capability validation.
Done: add EVM IR nativeValue lowering as Yul callvalue(), with ContextProbe golden Yul, solc bytecode, Foundry value-bearing call validation, and value.native metadata capability validation.
Done: add EVM IR eventEmit lowering to Yul log1 with keccak256(Solidity-style event signature) topic0 and 32-byte word data fields, with EventProbe golden Yul, solc bytecode, Foundry recorded-log validation, metadata capability validation, and explicit malformed event diagnostics.
Done: add EVM IR eventEmitIndexed lowering to Yul log2/log3/log4 for up to three scalar indexed fields, with signature topic0, indexed topics, non-indexed 32-byte word data, EventProbe golden Yul, solc bytecode, Foundry recorded-log validation, metadata capability validation, and explicit indexed event diagnostics.
Done: close the EventProbe validation gap for multi-topic scalar indexed events. IndexedTwoValues(uint64,uint64,uint64) and IndexedThreeValues(uint64,uint64,uint64,uint64) now prove the generated Yul emits log3 and log4, preserves ordered scalar indexed topics, validates metadata selectors, compiles with solc, and passes Foundry recorded-log assertions.
Done: close the EventProbe validation gap for typed scalar event fields. TypedScalarEvent(bool,uint32,bytes32) and IndexedTypedScalar(bool,uint32,bytes32,uint64) now prove Bool, U32, and Hash event data words and indexed topics lower correctly, with Bool/U32 dispatcher guards, golden Yul, metadata selector checks, solc, and Foundry recorded-log assertions.
Done: extend EVM IR event data lowering beyond scalar words so non-indexed flat struct fields, scalar fixed-array fields, and fixed arrays of flat structs emit ABI-style flattened data words, with canonical Solidity-style event signatures such as PairEvent((uint64,uint64)), ArrayEvent(uint64[2]), and PairArrayEvent((uint64,uint64)[2]), EventProbe golden Yul, solc bytecode, Foundry recorded-log validation, metadata selector validation, and explicit diagnostics for unsupported aggregate indexed fields.
Done: extend EVM IR eventEmitIndexed lowering so flat struct indexed fields and fixed-array indexed fields whose elements are flat structs hash their ABI-style flattened words into indexed topics. EventProbe now covers IndexedPair((uint64,uint64),uint64) and IndexedPairArray((uint64,uint64)[2],uint64) with golden Yul, solc bytecode, metadata selector validation, Foundry recorded-log topic-hash checks, and a diagnostic for nested/unsupported aggregate indexed shapes.
Done: close the EventProbe validation gap for scalar fixed-array indexed topics by adding IndexedArray(uint64[2],uint64) golden Yul, metadata selector validation, solc bytecode generation, and Foundry recorded-log topic-hash checks.
Done: extend EventProbe nested fixed-array event aggregate coverage. MatrixEvent(uint64[2][2]) and PairMatrixEvent((uint64,uint64)[2][2]) prove recursive non-indexed data flattening for scalar and flat-struct leaves, while IndexedMatrix(uint64[2][2],uint64) and IndexedPairMatrix((uint64,uint64)[2][2],uint64) prove indexed aggregate topic hashing over recursively flattened ABI-style words. The smoke now locks the new selectors, event ABI metadata, golden Yul, solc bytecode, and Foundry recorded-log assertions; nested arrays with unsupported or non-flat leaves remain explicit diagnostics.
Done: add EventProbe coverage for storage-backed flat struct event data and indexed aggregate topics. StoragePairEvent((uint64,uint64)) and IndexedStoragePair((uint64,uint64),uint64) now prove that a whole scalar storage struct write can be read back through storageScalarRead, flattened into event data words, hashed into indexed topics, validated in golden Yul, checked in metadata selectors, compiled by solc, and decoded by Foundry recorded logs.
Done: add EventProbe coverage for storage-backed fixed-array event aggregates. StorageArrayEvent(uint64[2]), StoragePairArrayEvent((uint64,uint64)[2]), IndexedStorageArray(uint64[2],uint64), and IndexedStoragePairArray((uint64,uint64)[2],uint64) now prove that storage array reads and storage array struct field reads can feed non-indexed event data flattening and indexed aggregate topic hashing, with golden Yul, metadata selector checks, solc, and Foundry recorded-log validation.
Done: add EVM IR crosscallInvoke lowering to synchronous EVM call helpers with selector packing, word arguments, one-word returns, failed-call and short-return reverts, with EvmCrosscallProbe golden Yul, solc bytecode, Foundry runtime validation, metadata capability validation, and explicit malformed crosscall type diagnostics.
Done: add EVM IR crosscallInvokeTyped lowering for typed scalar-word crosscalls over Bool, U32, U64, and Hash, with return-type-specific Yul helpers, Bool/U32 return-data guards, EvmCrosscallProbe golden Yul, solc bytecode, Foundry valid/invalid typed-return validation, metadata entrypoint validation, diagnostics for aggregate argument/return shapes not covered at that stage, and explicit Psy unsupported diagnostics.
Done: extend EVM IR normal crosscallInvokeTyped return lowering beyond scalar words for direct entrypoint returns of flat structs and scalar fixed arrays, with ABI-word-shape-specific Yul helpers, multi-word return-data size checks, Bool/U32 range guards across aggregate return words, EvmCrosscallProbe golden Yul, solc bytecode, Foundry aggregate struct/array return validation, metadata selector validation, and explicit diagnostics for aggregate return shapes not covered at that stage.
Done: extend EVM IR typed crosscall argument lowering beyond scalar words so normal, value-bearing, static, and delegate typed calls can flatten flat struct and scalar fixed-array arguments into ABI words. EvmCrosscallProbe now covers normal struct and fixed-array arguments plus value/static/delegate struct arguments through golden Yul, solc bytecode, Foundry runtime checks, metadata selector validation, and explicit diagnostics for aggregate argument shapes not covered at that stage.
Done: add EVM IR crosscallInvokeValueTyped lowering for value-bearing typed crosscalls, forwarding an explicit U64 call-value expression through value-specific Yul helpers for scalar returns plus flat struct and scalar fixed-array entrypoint aggregate returns, with EvmCrosscallProbe golden Yul, solc bytecode, Foundry msg.value/callee-balance validation, aggregate Bool/U32 malformed-return guards, metadata entrypoint validation, EVM malformed value/return diagnostics, and explicit Psy unsupported diagnostics.
Done: add EVM IR crosscallInvokeStaticTyped lowering for typed staticcalls, using value-free Yul staticcall helpers with selector/scalar/flat-aggregate argument packing, scalar returns, flat struct and scalar fixed-array entrypoint aggregate returns, and Bool/U32 return guards, with EvmCrosscallProbe golden Yul, solc bytecode, Foundry U64 read-only return, Bool/U32/Hash static typed return, aggregate return validation, invalid typed-return, static-context state-write failure validation, metadata entrypoint validation, EVM malformed nested aggregate diagnostics, and explicit Psy unsupported diagnostics.
Done: add EVM IR crosscallInvokeDelegateTyped lowering for typed delegatecalls, using value-free Yul delegatecall helpers with selector/scalar/flat-aggregate argument packing, scalar returns, flat struct and scalar fixed-array entrypoint aggregate returns, and Bool/U32 return guards, with EvmCrosscallProbe golden Yul, solc bytecode, Foundry caller-storage read/write validation, Bool/U32/Hash delegate typed return validation, aggregate return validation, invalid typed-return validation, metadata entrypoint validation, EVM malformed nested aggregate diagnostics, and explicit Psy unsupported diagnostics.
Done: extend EVM IR typed crosscall aggregate coverage to fixed arrays of flat structs across normal, value-bearing, static, and delegate typed call arguments and direct entrypoint returns. EvmCrosscallProbe now validates RemotePair[2] ABI-word flattening, Bool/U32 field return guards, golden Yul, solc bytecode, Foundry runtime behavior, and metadata selectors across all four call modes.
Done: extend EVM IR typed crosscall aggregate coverage to nested scalar fixed arrays across normal, value-bearing, static, and delegate typed call arguments and direct entrypoint returns. EvmCrosscallProbe now validates uint64[2][2] ABI-word flattening, golden Yul, solc bytecode, metadata selectors, Foundry runtime behavior, value forwarding, staticcall behavior, and delegatecall behavior across all four call modes. At that milestone, diagnostics still rejected struct and other non-scalar nested fixed-array leaves; flat struct leaves are now covered by the follow-up item below.
Done: extend EVM IR typed crosscall aggregate coverage to nested fixed arrays whose leaves are flat structs. EvmCrosscallProbe now validates RemotePair[2][2] arguments and direct entrypoint returns across normal, value-bearing, static, and delegate typed calls, including ABI word flattening, Bool/U32 field guards, golden Yul, solc bytecode, metadata selectors, Foundry runtime behavior, value forwarding, staticcall behavior, and delegatecall behavior. Diagnostics still reject nested fixed-array leaves whose structs are non-flat or otherwise unsupported.
Done: add EVM IR crosscallCreate and crosscallCreate2 lowering for fixed init-code hex. Creation helpers write init code to memory, call Yul create/create2, revert on zero-address failure, return the deployed address word, and validate golden Yul, solc bytecode, metadata selectors, Foundry deployed runtime calls, deterministic CREATE2 address derivation, EVM malformed creation diagnostics, and Psy unsupported diagnostics.
Done: add EVM IR direct scalar expression validation for U64/U32 arithmetic, U64 exponentiation, U64/U32 bitwise operations and shifts, predicates, boolean operators, literals, immutable locals, supported casts, one-word returns, dispatcher guards, and assertion guards, with EvmExpressionProbe golden Yul, solc bytecode, Foundry runtime/malformed calldata validation, metadata capability validation, and CI coverage.
Done: add EVM IR Hash word lowering, hash4/hashValue packing, and hash/hash_two_to_one lowering through Yul keccak256 helpers, with EvmHashProbe golden Yul, solc bytecode, Foundry ABI/storage validation, metadata capability validation, and explicit Hash/U64 mismatch diagnostics.
Done: add EVM IR Map<U64, U64, N> storage lowering through Solidity-style keccak256(key, slot) mapping slots, with EvmMapProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, metadata capability validation, and explicit diagnostics for unsupported map shapes and statement-position misuse.
Done: add EVM IR single-segment mapKey storage path compound assignment over Map<U64, U64, N>, with EvmMapProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, metadata capability validation, and explicit diagnostics for expression-position and nested-path misuse.
Done: generalize EVM IR storage maps to word key/value shapes over U32, U64, Bool, and Hash, reusing Solidity-style keccak256(key, slot) mapping slots, with EvmTypedMapProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, U32/Bool calldata guards, metadata capability validation, CI coverage, and explicit diagnostics for non-word map shapes.
Done: add EVM IR storage.map.contains lowering through ProofForge-managed presence slots rooted at keccak256(slot || PROOF_FORGE_MAP_PRESENCE), with EvmMapProbe and EvmTypedMapProbe golden Yul, solc bytecode, Foundry value/presence-slot validation for U64/U32/Bool/Hash maps, zero-valued present-key coverage, metadata validation, and explicit diagnostics for statement-position misuse.
Done: add EVM IR nested map storage paths over consecutive mapKey segments, folding Solidity-style mapping slots for value storage and ProofForge-managed presence slots for final keys, with EvmMapProbe and EvmTypedMapProbe golden Yul, solc bytecode, Foundry raw-slot validation, U32 dispatcher guard coverage, metadata validation, and explicit diagnostics for mixed map/aggregate storage paths.
Done: add EVM IR U64 fixed storage array lowering as contiguous storage slots with runtime bounds checks, with EvmStorageArrayProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, metadata capability validation, and explicit diagnostics for unsupported array element types.
Done: add EVM IR single-segment index storage path read/write/compound assignment over U64 fixed storage arrays, reusing the bounded array slot helper and extending EvmStorageArrayProbe validation.
Done: generalize EVM IR word storage to Bool scalar storage and U32/Bool/Hash fixed storage arrays, reusing the bounded array slot helper, with EvmTypedStorageProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, U32 calldata range guards, metadata capability validation, CI coverage, and explicit diagnostics for unsupported non-word storage element types.
Done: add EVM IR immutable local fixed-array value lowering for U64, U32, Bool, and Hash elements with static literal indexes, direct fixed-array literal indexing, EvmArrayValueProbe golden Yul, solc bytecode, Foundry runtime validation, metadata capability validation, and explicit diagnostics for static out-of-bounds indexes.
Done: extend EVM IR local fixed-array lowering to mutable aggregate locals, including static element assignment, numeric element compound assignment, and U32/Bool/Hash element writes, with EvmArrayValueProbe golden Yul, solc bytecode, Foundry runtime validation, metadata entrypoint validation, CI coverage, and explicit diagnostics for immutable element assignment.
Done: extend EVM IR local fixed-array lowering to dynamic local/literal indexes by threading a lowering environment through expressions, generating length-specific Yul getter helpers for dynamic reads, lowering dynamic local element assignment and numeric compound assignment to switch blocks, and validating dynamic in-bounds/out-of-bounds behavior through EvmArrayValueProbe golden Yul, metadata entrypoints, solc bytecode, and Foundry runtime checks.
Done: add EVM IR whole local fixed-array assignment from local values and literals, snapshotting RHS elements into temporary Yul locals before writing target elements, and validating local-source and self-referential literal RHS behavior through EvmArrayValueProbe golden Yul, metadata entrypoints, solc bytecode, and Foundry runtime checks.
Done: extend EVM IR local fixed-array lowering to static nested scalar arrays, including immutable reads, mutable leaf assignment, numeric leaf compound assignment, nested whole-local assignment, and RHS snapshotting, with EvmArrayValueProbe golden Yul, metadata entrypoints, solc bytecode, and Foundry runtime checks. Flat struct nested leaves are covered by EvmStructArrayValueProbe; other unsupported aggregate leaves remain explicit diagnostics.
Done: extend EVM IR local fixed-array lowering to dynamic nested scalar array indexes, including nested getter helpers for reads, nested switch lowering for mutable leaf assignment and compound assignment, mixed static/dynamic path coverage, runtime out-of-bounds reverts, EvmArrayValueProbe golden Yul, metadata entrypoints, solc bytecode, and Foundry runtime checks.
Done: add EVM IR flat immutable local struct value lowering for U64, U32, Bool, and Hash fields, direct struct literal field access, EvmStructValueProbe golden Yul, solc bytecode, Foundry runtime validation, metadata capability validation, and explicit diagnostics for whole-struct storage misuse and nested fields.
Done: extend EVM IR flat local struct lowering to mutable aggregate locals, including static field assignment, numeric field compound assignment, and U32/Bool/Hash field writes, with EvmStructValueProbe golden Yul, solc bytecode, Foundry runtime validation, metadata entrypoint validation, CI coverage, and explicit diagnostics for immutable field assignment.
Done: add EVM IR whole local struct assignment from local values and literals, snapshotting RHS fields into temporary Yul locals before writing target fields, and validating local-source and self-referential literal RHS behavior through EvmStructValueProbe golden Yul, metadata entrypoints, solc bytecode, and Foundry runtime checks.
Done: add EVM IR local fixed arrays of flat structs, expanding each element field into deterministic Yul locals, supporting static and dynamic field(arrayGet(localArray, index), name) reads, mutable field assignment, numeric field compound assignment, whole local assignment from local arrays and self-referential array literals with RHS snapshotting, U64/U32/Bool/Hash field coverage, dynamic out-of-bounds reverts, EvmStructArrayValueProbe golden Yul, metadata entrypoint/capability validation, solc bytecode generation, Foundry runtime checks, and CI coverage.
Done: extend EVM IR nested local fixed arrays to flat struct leaves, expanding each nested element field into deterministic Yul locals, supporting static and dynamic nested field reads, nested mutable field assignment, numeric nested field compound assignment, whole nested local assignment from local arrays and self-referential nested array literals with RHS snapshotting, dynamic out-of-bounds reverts, refreshed EvmStructArrayValueProbe golden Yul, metadata entrypoint validation, solc bytecode generation, Foundry runtime checks, and coverage manifest updates.
Done: add EVM IR flat storage struct lowering for scalar storage structs and fixed storage arrays of flat structs, including direct struct field effects, scalar field storage paths, array index+field storage paths, numeric field compound assignment, whole scalar storage struct read/write with RHS snapshotting, storage-backed ABI struct returns, Bool/U32/Hash field coverage, EvmStorageStructProbe golden Yul, solc bytecode, Foundry runtime/raw-slot validation, metadata capability validation, CI coverage, and explicit diagnostics for missing fields and non-flat storage structs.
Done: validate storage-backed aggregate ABI returns for EVM IR by extending EvmStorageArrayProbe with return_values() over storage-array element reads and EvmStorageStructProbe with return_points() over fixed storage-array-of-struct field reads, including golden Yul, solc bytecode, metadata selector validation, Foundry ABI decoding, and raw-slot checks.
Done: add EVM IR static aggregate ABI lowering for fixed-array and struct parameters/returns, including nested scalar fixed arrays and fixed arrays of flat structs, with calldata word flattening, U32/Bool aggregate word guards, multi-word return-data encoding, EvmAbiAggregateProbe golden Yul, solc bytecode, Foundry runtime/malformed calldata validation, metadata capability validation, structured abi.entrypoints selector/calldata/return word-layout validation, CI coverage, and explicit diagnostics for Unit, zero-length arrays, non-flat struct fields, and crosscall-only unsupported nested fixed-array leaf shapes.
Done: close the EVM aggregate ABI validation gap for Hash leaves. HashPair(bytes32,bytes32), pick_hash(bytes32[2]), and make_hash_array(bytes32,bytes32) now prove Hash/bytes32 fields and fixed arrays flatten through calldata and return-data encoding, with golden Yul, metadata selector checks, solc, Foundry ABI decoding, and short bytes32[2] calldata rejection.
Done: add golden Yul outputs for SDK EVM examples (Counter, ArrayExample, SimpleToken, ERC20, Ownable, Pausable, and VerifiedVault) and make scripts/evm/build-examples.sh diff generated Yul against those fixtures before validating metadata.
Done: add metadata emission and validation around the current solc --strict-assembly flow for SDK and portable IR EVM bytecode builds.
Keep Foundry smoke as the mature EVM smoke test.

Acceptance criteria:

lake build passes.
scripts/evm/diagnostic-smoke.sh passes.
scripts/evm/check-ir-coverage-manifest.py passes.
scripts/evm/build-examples.sh succeeds on a machine with solc.
scripts/evm/foundry-smoke.sh succeeds on a machine with Foundry.
The generated metadata points to the bytecode artifact and records target: evm.

Workstream 4: Wasm Host Runtime Split

Goal: make Wasm host adapters target-driven instead of assuming every Wasm contract is NEAR. Tasks:

Move chain extern declarations out of generic EmitZig runtime externs.
Add a target-selected host bridge list.
Keep NEAR bridge as the reference implementation.
Add a CosmWasm bridge skeleton with allocator and region ABI.

Acceptance criteria:

A Wasm build can select NEAR or CosmWasm bridge explicitly.
Generic Wasm runtime does not force-link NEAR host functions.
wasm-near and wasm-cosmwasm can have different required exports.

Workstream 5: CosmWasm Spike

Goal: prove that ProofForge can target another Wasm host besides NEAR. Tasks:

Add Lean.CosmWasm SDK skeleton (see wasm-family.md).
Add zigc-cosmwasm wrapper.
Add cosmwasm_contract_root.zig.
Export interface_version_8, allocate, deallocate, instantiate, execute, and query.
Add Counter example using JSON-backed messages.
Add cosmwasm-check smoke.

Acceptance criteria:

Counter Wasm passes cosmwasm-check.
instantiate, execute, and query are present in exports.
The smoke test can increment and query counter state.

Workstream 6: Solana sBPF Assembly Toolchain Integration (Phase 0)

Goal: validate the direct-assembly route end to end — a canned .s file round-trips through the blueshift-gg/sbpf toolchain into a loadable ELF. Supersedes the old sbpf-linker spike (D-026). Tasks:

Install sbpf via cargo install --git https://github.com/blueshift-gg/sbpf.git.
Add --emit-sbpf-asm CLI mode to proof-forge that writes a canned entrypoint.s (returns success, no account parsing).
Run sbpf build on the canned .s; verify a valid eBPF ELF is produced.
Verify sbpf disassemble round-trips the ELF.
Record toolchain version in artifact metadata.

Acceptance criteria:

sbpf build produces a .so recognized as ELF 64-bit LSB ... eBPF.
sbpf disassemble produces assembly matching the input.
--emit-sbpf-asm writes valid .s without assembly errors.
proof-forge-artifact.json records target: "solana-sbpf-asm".
sbpf installed to PATH via cargo install.

Reference: solana-sbpf-asm design doc, RFC 0005.

Workstream 7: Solana sBPF Assembly Counter Codegen (Phase 1)

Goal: lower the portable IR Counter module to sBPF assembly and pass sbpf test. This is the first real codegen backend for the assembly route. Tasks:

Implement ProofForge.Backend.Solana.StateLayout — compute per-account field offsets from the instruction manifest; emit .equ constants.
Implement ProofForge.Backend.Solana.SbpfAsm — lower IR.Module to .s:
- Entrypoint adapter: parse serialized accounts, dispatch on instruction discriminant.
- Account validation: signer, writable, owner checks per manifest.
- Expression lowering: literals, locals, add/sub, comparisons, casts.
- Statement lowering: letBind, assign, assignOp, ifElse, return, assert.
- Effect lowering: storageScalar read/write at account-data offsets.
Add --solana-elf CLI mode: emit .s then invoke sbpf build.
Generate instruction manifest (manifest.toml) alongside the .s.
Create Examples/Solana/Counter.lean + manifest.
Run sbpf test (Mollusk) and a Surfpool/Web3.js live deployment smoke.

Acceptance criteria:

Counter scenario (initialize, increment, get) passes sbpf test.
Surfpool/Web3.js live smoke passes (optional, gated on tool availability).
Capability checker rejects IR modules using unsupported capabilities with a clear diagnostic citing target id and capability id.
Same portable IR Counter module lowers to both EVM and Solana.
Artifact metadata records target: "solana-sbpf-asm", irVersion, entrypoints, and capabilities used.

Out of scope (Phase 2+): maps, struct types, events, bounded loops, Borsh serialization, full SPL Token data layouts, complete live CPI matrix coverage, and Rust/Pinocchio equivalence. CPI and PDA stay Solana-specific (D-027): the SDK routes them through target capability calls and sBPF helper actions instead of adding them to the portable IR. Reference: solana-sbpf-asm design doc § Phased Implementation Plan.

Phase 1 progress (incremental sub-items)

The Workstream 7 Phase 1 backend (ProofForge.Backend.Solana.SbpfAsm) lands incrementally. Each sub-item carries its own runnable validation gate so partial progress is visible before the full acceptance criteria close:

Solana SDK completion roadmap

Reference docs driving this roadmap:

Solana CPI and PDA docs: <https://solana.com/docs/core/cpi> and <https://solana.com/docs/core/pda>.
Anchor CPI/account-constraint docs: <https://www.anchor-lang.com/docs/basics/cpi> and <https://www.anchor-lang.com/docs/references/account-constraints>.
Pinocchio no-dependency / no-std program model: <https://docs.rs/pinocchio> and <https://github.com/anza-xyz/pinocchio>.

Baseline: as of 2026-07-02, the Solana path has direct sBPF assembly emission, Counter deployment through Surfpool/Web3.js, SDK capability metadata, generated manifest/artifact output, module-wide multi-account schemas, standard System/SPL Token CPI data packing, bump-allocator metadata, scalar entrypoint parameter decoding, typed PDA seed lowering, live System Program transfer plus create-account CPI validation, live SPL Token transfer_checked CPI validation, live SPL Token mint_to/burn/approve/revoke CPI validation, and live SPL Token set_authority CPI validation, plus live scalar events.emit log validation through sol_log_64_, live account-pubkey log validation through sol_log_pubkey, live state-backed data-log validation through sol_log_data, and live Clock.slot sysvar validation for contextRead checkpointId, plus live runtime.memory validation through sol_memcpy_, sol_memmove_, sol_memcmp_, and sol_memset_, plus live Solana-only crypto.hash validation through sol_sha256, sol_keccak256, and feature-gated sol_blake3, plus live Rent.lamports_per_byte_year sysvar validation through sol_get_rent_sysvar. It also covers live validation for all current RPC-exposed EpochSchedule fields through sol_get_epoch_schedule_sysvar: slots_per_epoch, leader_schedule_slot_offset, warmup, first_normal_epoch, and first_normal_slot, plus live EpochRewards validation through sol_get_epoch_rewards_sysvar for distribution_starting_block_height, num_partitions, parent_blockhash_word0..3, total_points_low/high, total_rewards, distributed_rewards, and active, plus feature-gated live LastRestartSlot.last_restart_slot validation through sol_get_sysvar with the SysvarLastRestartS1ot1111111111111111111111 sysvar id. Live SDK coverage now includes runtime.return_data lowering to sol_set_return_data and sol_get_return_data, with empty-read, set-return simulation, and same-instruction set/get roundtrip checks, plus runtime.compute_units lowering to feature-gated sol_remaining_compute_units state writes and profiling logs through sol_log_compute_units_. The estimates below assume one engineer working on this branch, the current direct-assembly architecture staying stable, and local sbpf/Surfpool/Solana CLI tooling remaining available.

Level	Estimated effort	Done when
SDK alpha: usable Solana programs	3-5 focused engineering days	Simple programs can use state, PDA seeds, scalar instruction parameters, System Program CPI, SPL Token CPI, logs/return data, and Web3.js behavior tests without hand-written assembly patches.
SDK beta: reference-comparable Solana backend	2-3 focused weeks	ProofForge output is compared against Rust/Pinocchio fixtures for the same account schema, covers key syscalls, validates live CPI behavior, and supports per-entrypoint account schemas.
Anchor/Pinocchio-class developer surface	4-6 focused weeks after beta	The SDK offers account constraints, typed account/data helpers, IDL/client generation, richer SPL/Token-2022 coverage, and stable diagnostics comparable to a framework-level workflow.

Completed alpha slices:

Instruction ABI hardening: parameter payload length bounds checks, per-entrypoint parameter schemas in manifest.toml and proof-forge-artifact.json, and stable scalar parameter metadata are now in place.
PDA typed seed lowering: literalSeed/utf8Seed, accountSeed, bumpSeed, and paramSeed descriptors now lower to Solana seed slices, bump? participates in the effective seed list, and declared PDA accounts can be checked against the derived pubkey.
PDA/Web3.js derivation fixture: scripts/solana/pda-web3-smoke.sh reads the generated SDK Vault typedSeeds artifact data and verifies literal/account/ bump descriptor semantics against PublicKey.findProgramAddressSync and PublicKey.createProgramAddressSync; the harness also covers UTF-8 and instruction-parameter resolver behavior.
Live System Program transfer CPI fixture: scripts/solana/system-cpi-web3-smoke.sh builds and deploys a generated transfer CPI program on Surfpool, invokes it through Web3.js, and proves both the lamport movement and state write.
Live System Program create-account CPI fixture: scripts/solana/system-create-account-cpi-web3-smoke.sh builds and deploys a generated create-account CPI program on Surfpool, invokes it through Web3.js, and proves the new account owner/space/lamports plus state writes.
Live SPL Token transfer-checked CPI fixture: scripts/solana/spl-token-transfer-cpi-web3-smoke.sh builds and deploys a generated transfer_checked CPI program on Surfpool, creates SPL Token test accounts with @solana/spl-token, invokes it through Web3.js, and proves the source/destination token balance deltas plus state writes.
Live SPL Token ops CPI fixture: scripts/solana/spl-token-ops-cpi-web3-smoke.sh builds and deploys a generated mint_to/burn/approve/revoke CPI program on Surfpool, validates the generated four-entrypoint artifact schema, creates SPL Token test accounts with @solana/spl-token, invokes all four generated entrypoints through Web3.js, and proves supply/balance/delegate changes plus state writes.
Live SPL Token authority CPI fixture: scripts/solana/spl-token-authority-cpi-web3-smoke.sh builds and deploys a generated set_authority CPI program on Surfpool, validates the generated single-entrypoint artifact schema, creates an SPL Token mint through @solana/spl-token, invokes the generated entrypoint through Web3.js, and proves mint authority moved to the requested new authority plus the marker state write.
Live scalar event, pubkey log, and data log fixture: scripts/solana/log-event-web3-smoke.sh builds and deploys a generated events.emit program on Surfpool, invokes it through Web3.js, verifies the generated sol_log_64_ transaction log contains the stable AmountEvent tag and scalar amount field, and proves the program-owned state account recorded the same value. The same fixture now validates Solana-only logAccountPubkey metadata, invokes the generated log_state_pubkey entrypoint, and proves sol_log_pubkey logs the state account’s base58 pubkey. It also validates Solana-only logStateData metadata, invokes log_state_data, and proves sol_log_data emits a base64 Program data: payload for the state-backed amount bytes.
Live Clock sysvar fixture: scripts/solana/clock-sysvar-web3-smoke.sh builds and deploys a generated contextRead checkpointId program on Surfpool, lowers it to sol_get_clock_sysvar, invokes it through Web3.js, and proves the recorded Clock.slot matches the observed transaction slot.
Live memory syscall fixture: scripts/solana/memory-web3-smoke.sh builds and deploys a generated runtime.memory program on Surfpool, invokes it through Web3.js, and proves sol_memcpy_, sol_memmove_, sol_memcmp_, and sol_memset_ effects by reading copied value, moved value, compare result, and fill bytes from program-owned state.
Return-data/compute-units SDK fixture: Tests/SolanaReturnDataCompute.lean proves runtime.return_data and runtime.compute_units route through Solana-only capability metadata, rejects on EVM, and render manifest sections plus sBPF helper calls for sol_set_return_data, sol_get_return_data, feature-gated sol_remaining_compute_units, and sol_log_compute_units_. scripts/solana/return-data-compute-web3-smoke.sh builds and deploys the generated --solana-return-data-compute-elf fixture on Surfpool, validates artifact action metadata, verifies no-data sol_get_return_data reads, confirms sol_set_return_data through Web3.js simulation returnData, checks a same-instruction set/get roundtrip including program id words, records a nonzero remaining-compute-units value, and confirms compute-unit logging.
Live SHA-256/Keccak-256/Blake3 syscall fixture: scripts/solana/crypto-hash-web3-smoke.sh builds and deploys a generated Solana-only crypto.hash program on Surfpool, invokes set_preimage, hash_preimage, keccak_preimage, and blake3_preimage through Web3.js, and proves the account-stored 32-byte digests match Node SHA-256 and @noble/hashes Keccak-256/Blake3 references for the same little-endian preimage. The Blake3 action is recorded as feature-gated in manifest and artifact metadata.
Live Rent sysvar fixture: scripts/solana/rent-sysvar-web3-smoke.sh builds and deploys a generated Solana-only sysvar target-extension program on Surfpool, invokes record_rent through Web3.js, and proves the recorded Rent.lamports_per_byte_year matches the Rent sysvar account data.
Live EpochSchedule sysvar fixture: scripts/solana/epoch-schedule-sysvar-web3-smoke.sh builds and deploys a generated Solana-only sysvar target-extension program on Surfpool, invokes record_epoch_schedule through Web3.js, and proves the recorded EpochSchedule.slots_per_epoch, EpochSchedule.leader_schedule_slot_offset, EpochSchedule.warmup, EpochSchedule.first_normal_epoch, and EpochSchedule.first_normal_slot match RPC getEpochSchedule() fields.
Live EpochRewards sysvar fixture: scripts/solana/epoch-rewards-sysvar-web3-smoke.sh builds and deploys a generated Solana-only sysvar target-extension program on Surfpool, invokes record_epoch_rewards through Web3.js, and proves that sol_get_epoch_rewards_sysvar records EpochRewards fields into state. parent_blockhash is exposed as four little-endian u64 word views and total_points is exposed as low/high u64 word views until the portable scalar layer has first-class wide-value output states.
Live LastRestartSlot sysvar fixture: scripts/solana/last-restart-slot-sysvar-web3-smoke.sh builds and deploys a generated Solana-only sysvar target-extension program on Surfpool, invokes record_last_restart_slot through Web3.js, and proves the feature-gated LastRestartSlot.last_restart_slot read lowers through sol_get_sysvar and matches the LastRestartSlot sysvar account data. The action is marked feature_gated in manifest and artifact metadata.

Completed beta scaffolding slices:

Pinocchio System transfer reference contract: references/solana/pinocchio/system-transfer contains a checked-in no-allocator Pinocchio reference for the same System transfer account schema as ProofForge.Solana.Examples.SystemCpi. The gate scripts/solana/pinocchio-system-transfer-equivalence.sh emits the ProofForge System CPI artifact and compares its instruction tag, parameter ABI, account order, signer/writable constraints, CPI protocol/data layout, and state-write contract against the reference manifest/source.
Pinocchio System transfer live-equivalence harness: scripts/solana/pinocchio-system-transfer-live-equivalence.sh is wired to build the ProofForge ELF and the checked-in Pinocchio reference ELF, deploy both programs to one Surfpool instance, invoke the same Web3.js transfer scenario for each, and compare recipient lamport deltas plus state writes. The harness currently skips when cargo-build-sbf cannot find Solana rustc/ platform-tools.
Pinocchio System create-account reference contract: references/solana/pinocchio/system-create-account contains a checked-in no-allocator Pinocchio reference for the same System Program create_account account schema as ProofForge.Solana.Examples.SystemCreateAccountCpi. The gate scripts/solana/pinocchio-system-create-account-equivalence.sh emits the ProofForge create-account CPI artifact and compares its instruction tag, two-parameter ABI, account order, signer/writable constraints, CPI protocol/data layout, lamports/space/owner contract, and two-field state-write contract against the reference manifest/source. With PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1, the same gate typechecks the reference against pinocchio-system.
Pinocchio System create-account live-equivalence harness: scripts/solana/pinocchio-system-create-account-live-equivalence.sh is wired to build the ProofForge ELF and the checked-in Pinocchio reference ELF, deploy both programs to one Surfpool instance, invoke the same Web3.js create-account scenario for each, and compare lamports/space inputs plus both state writes. The harness currently skips when cargo-build-sbf cannot find Solana rustc/platform-tools.
Pinocchio SPL Token transfer reference contract: references/solana/pinocchio/spl-token-transfer contains a checked-in no-allocator Pinocchio reference for the same SPL Token transfer_checked account schema as ProofForge.Solana.Examples.SplTokenTransferCheckedCpi. The gate scripts/solana/pinocchio-spl-token-transfer-equivalence.sh emits the ProofForge SPL Token CPI artifact and compares its instruction tag, parameter ABI, account order, signer/writable constraints, CPI protocol/data layout, decimals/amount contract, and state-write contract against the reference manifest/source. With PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1, the same gate typechecks the reference against pinocchio-token.
Pinocchio SPL Token transfer live-equivalence harness: scripts/solana/pinocchio-spl-token-transfer-live-equivalence.sh is wired to build the ProofForge ELF and the checked-in Pinocchio Token reference ELF, deploy both programs to one Surfpool instance, invoke the same Web3.js + @solana/spl-token transfer_checked scenario for each, and compare source/destination token balance deltas plus the amount state write. The harness currently skips when cargo-build-sbf cannot find Solana rustc/ platform-tools.
Pinocchio SPL Token ops reference contract: references/solana/pinocchio/spl-token-ops contains a checked-in no-allocator Pinocchio reference for the same SPL Token mint_to/burn/approve/revoke account schema as ProofForge.Solana.Examples.SplTokenOpsCpi. The gate scripts/solana/pinocchio-spl-token-ops-equivalence.sh emits the ProofForge SPL Token ops CPI artifact and compares its four instruction tags, parameter ABI, account order, signer/writable constraints, CPI protocol/data layout, SPL Token instruction contract, and state-write contract against the reference manifest/source. With PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1, the same gate typechecks the reference against pinocchio-token.
Pinocchio SPL Token ops live-equivalence harness: scripts/solana/pinocchio-spl-token-ops-live-equivalence.sh is wired to build the ProofForge ELF and the checked-in Pinocchio Token ops reference ELF, deploy both programs to one Surfpool instance, invoke the same Web3.js + @solana/spl-token mint/burn/approve/revoke scenario for each, and compare token effects plus all four amount/marker state writes. The harness currently skips when cargo-build-sbf cannot find Solana rustc/platform-tools.
Pinocchio SPL Token authority reference contract: references/solana/pinocchio/spl-token-authority contains a checked-in no-allocator Pinocchio reference for the same SPL Token set_authority account schema as ProofForge.Solana.Examples.SplTokenAuthorityCpi. The gate scripts/solana/pinocchio-spl-token-authority-equivalence.sh emits the ProofForge SPL Token authority CPI artifact and compares its instruction ABI, account order, signer/writable constraints, CPI protocol/data layout, SetAuthority instruction contract, and marker state-write contract against the reference manifest/source. With PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1, the same gate typechecks the reference against pinocchio-token.
Pinocchio SPL Token authority live-equivalence harness: scripts/solana/pinocchio-spl-token-authority-live-equivalence.sh is wired to build the ProofForge ELF and the checked-in Pinocchio Token authority reference ELF, deploy both programs to one Surfpool instance, invoke the same Web3.js + @solana/spl-token mint-authority transfer scenario for each, and compare mint authority plus marker state writes. The harness currently skips when cargo-build-sbf cannot find Solana rustc/platform-tools.

Completed developer-surface slices:

Portable ValueVault surface source: ProofForge.Contract.Surface now lets examples declare state slots, parameters, methods, and event fields once, then write entrypoint bodies through typed refs (read, write, bind, emit, ret) instead of raw ContractSpec string plumbing. ProofForge.Contract.Examples.ValueVault uses this layer and intentionally leaves selector? = none in the source.
Declaration-derived IR names: state_decl, binding_decl, method_decl, method_return_decl, and event_decl macros now derive IR names from Lean declarations, so the portable Counter and ValueVault sources no longer repeat raw strings for state slots, inputs, locals, method names, or event names. Tests assert the derived snake-case state/parameter/method names and PascalCase event names before routing the same source across EVM and Solana.
Source-facing declaration facade: contract_decl Name do ... derives the module name from a Lean identifier and keeps ContractSpec as the compiler-owned intermediate product rather than the user-visible authoring model. ProofForge.Contract.Examples.Counter and ProofForge.Contract.Examples.ValueVault now use this facade; the older *_ref macros remain as compatibility shims for older downstream source.
Contract Source Syntax v1: ProofForge.Contract.Source adds scoped contract_source syntax for state declarations, events, entrypoints, queries, source-local bindings, state assignment, event emission, returns, typed arithmetic operators, and Solana extension declarations for allocator, accounts, PDA derivation, and SPL Token CPI calls. ProofForge.Contract.Examples.Counter and ProofForge.Contract.Examples.ValueVault now author portable logic through this source block while the macro emits the same ContractSpec/portable IR boundary used by routing, EVM selector hydration, Solana instruction tags, IDL, and client artifact generation.
Legacy .learn parser/lowering seed: ProofForge.Contract.Learn now lexes and parses checked-in .learn files under Examples/Learn/ into a small source AST for the portable scalar/event subset, lowers that AST to ContractSpec/portable IR, and serves as a compatibility validation entrypoint rather than a new product source language. The primary authoring surface remains Lean .lean files and Lean SDK helpers. It proves that Counter.learn and ValueVault.learn produce the same IR modules as the current contract_source examples. The CLI still accepts .learn files through --learn --target evm and --learn --target solana-sbpf-asm, with --learn-yul, --learn-bytecode, and --learn-sbpf retained as lower-level compatibility convenience paths. scripts/portable/value-vault-smoke.sh uses Examples/Learn/ValueVault.learn as a legacy equivalence fixture and proves that compatibility entrypoint can route to EVM Yul/bytecode metadata and Solana sBPF assembly/manifest/IDL/client artifacts without hand-authoring ContractSpec.
Learn Solana target-extension syntax: ProofForge.Contract.Learn now parses SolanaVault.learn forms for solana allocator, solana account, solana pda, solana cpi ... spl_token_transfer_checked(...), and entry-level solana derive / solana invoke. The lowering reuses ProofForge.Solana builder helpers, so account/PDA/CPI metadata still flows through the existing capability plan, manifest, IDL, client, and sBPF assembly paths. Tests/LearnSource.lean checks that Learn-lowered SolanaVault has the same IR module and generated manifest as ProofForge.Solana.Examples.Vault.
Learn System Program CPI syntax: SystemCpi.learn and SystemCreateAccountCpi.learn now cover solana cpi ... system_transfer(...), solana cpi ... system_create_account(...) owner ..., and matching entry-level solana invoke statements. Tests/LearnSource.lean proves both Learn files lower to the same IR modules and generated manifests as the existing ProofForge.Solana.Examples.SystemCpi and ProofForge.Solana.Examples.SystemCreateAccountCpi source examples.
Learn SPL Token ops syntax: SplTokenOpsCpi.learn now covers selector-bearing Learn entrypoints plus spl_token_mint_to, spl_token_burn, spl_token_approve, and spl_token_revoke declarations/invocations. Tests/LearnSource.lean proves the Learn file lowers to the same IR module and generated manifest as ProofForge.Solana.Examples.SplTokenOpsCpi, keeping the string-heavy Builder code as an internal expected fixture rather than the user-facing syntax.
Learn log/return-data/compute-unit syntax: LogEvent.learn and ReturnDataCompute.learn now cover Solana pubkey/data log helper statements, return-data set/get statements, and remaining compute-unit read/log statements. Tests/LearnSource.lean proves both Learn files lower to the same IR modules and generated manifests as ProofForge.Solana.Examples.LogEvent and ProofForge.Solana.Examples.ReturnDataCompute, moving another syscall-facing SDK slice from Builder-only fixtures into user-facing Learn source.
Learn memory/crypto/sysvar syntax: Memory.learn, Crypto.learn, Rent.learn, EpochSchedule.learn, EpochRewards.learn, LastRestartSlot.learn, and Clock.learn now cover Solana memory helpers, SHA-256/Keccak-256/BLAKE3 helpers, and sysvar/context reads in user-facing Learn source. Tests/LearnSource.lean proves these Learn files lower to the same IR modules and generated manifests as the corresponding ProofForge.Solana.Examples.* fixtures.
Learn reference diagnostics: ProofForge.Contract.Learn now builds a declaration reference index while lowering and rejects unknown or mismatched Solana CPI invocations, unknown PDA derivations, invalid signer seeds, CPI declarations that use undeclared accounts, CPI account declarations that do not satisfy required writable or signer constraints, and helper statements that reference undeclared state/account names. Tests/LearnDiagnostics.lean pins these messages so Learn behaves like a checked language frontend instead of asking users to hand-author unchecked ContractSpec data.
Solana typed account surface: ProofForge.Solana.Surface now adds account_ref, pda_ref, and cpi_ref declarations plus typed PDA seed, account constraint, and SPL/System CPI helpers. ProofForge.Solana.Examples.Vault now uses dedicated contract_source items such as allocator bump, account ... writable, pda ... seeds [...], cpi ... spl_token_transfer_checked(...), derive pda ..., invoke ... spl_token_transfer_checked(...), and the same first-class source-syntax path now covers spl_token_set_authority(...) instead of raw account/PDA/CPI strings or use/do helper plumbing. The target extension emits declared account constraints into manifest.toml, proof-forge-artifact.json (solanaExtensions.accounts), and the generated account-validation schema.
System create-account source syntax: ProofForge.Contract.Source now exposes source-level cpi ... system_create_account(...) owner ... and invoke ... system_create_account(...) owner ... forms. ProofForge.Solana.Examples.SystemCreateAccountCpi uses those forms instead of the lower-level builder API while preserving the existing generated assembly, manifest, artifact, and Surfpool/Web3.js behavior gate.
SPL Token authority source syntax: ProofForge.Contract.Source now exposes source-level cpi ... spl_token_set_authority(...) authority_type(...) signer_seeds [...] and invoke ... spl_token_set_authority(...) authority_type(...) signer_seeds [...] forms. ProofForge.Solana.Examples.SplTokenAuthorityCpi uses those forms in a Lean .lean fixture, and the generated artifact, Surfpool/Web3.js behavior gate, and Pinocchio reference gates all validate the same lowering boundary.
Target-stage ABI selector hydration: the Learn/ValueVault CLI emit paths derive EVM selectors from each entrypoint’s Solidity ABI signature with cast sig immediately before EVM Yul/bytecode emission, validate any explicit selector against the derived value, and keep Solana routing independent by continuing to use target instruction tags. scripts/portable/value-vault-smoke.sh proves the same .learn source emits EVM Yul/bytecode metadata plus Solana sBPF assembly/manifest/artifact metadata.
Solana IDL and TypeScript client package output: ProofForge.Backend.Solana.Idl renders proof-forge-idl.json from the same instruction/account/PDA/CPI schema used by manifest.toml and artifact metadata. ProofForge.Backend.Solana.Client renders proof-forge-client.ts with Web3.js TransactionInstruction helpers, instruction-data encoding, and account-meta construction. Solana package printing, --emit-solana-sdk-sbpf, --emit-value-vault-ir-sbpf, and the Solana ELF contract-sdk path now emit and hash both files.

Current boundary:

ProofForge.Contract.Learn is now a legacy .learn compatibility parser/lowering seed rather than a new product source language. It covers the portable Counter/ValueVault subset and the Vault-level Solana account/PDA/SPL Token transfer CPI subset, System Program transfer/create-account CPI, SPL Token mint/burn/approve/revoke CPI, and Solana log/return-data/compute-unit/memory/crypto/sysvar helper statements. During lowering, Solana CPI/PDA declarations and entrypoint helper statements are cross-checked against declared references. CPI account operands must be declared with solana account ...; CPI writable/signer requirements are checked against those declarations, so the remaining string names are compiler-owned identifiers rather than unchecked user-authored specs. ProofForge.Contract.Source and Lean SDK helpers remain the primary authoring frontend; .learn files are retained only as legacy compatibility and equivalence fixtures that reuse the same lowering boundary by compile-time target id. The next authoring gap is to extend the Lean .lean surface to Token-2022, typed account/data references, and richer Pinocchio-style account validation ergonomics; legacy --learn package emission is not the direction for new syntax work.

Remaining priority slices:

Rust/Pinocchio equivalence fixtures (2-4 days): make the Pinocchio live equivalence harnesses pass in CI/local environments by installing Solana rustc/platform-tools reliably, then extend static and live reference coverage to Token-2022 and remaining SPL helper paths beyond the checked transfer/mint/burn/approve/revoke/set-authority set. The key comparison points are account order, signer/writable checks, CPI instruction data, and observable state changes.
Richer structured logs, account data, and typed return helpers (3-5 days): extend the current scalar sol_log_64_/sol_log_data event path to string logs, Anchor-style discriminator/Borsh payloads, and indexed event forms; add typed return payload helpers beyond u64, portable Expr.hash routing where the hash semantics match the target, and broader account/data packing helpers that reuse the new memory/syscall path, with JavaScript reference checks.
Runtime allocation lowering (1-2 days): route heap-backed SDK structures through runtime.allocator, emit actual downward bump-pointer allocation code when needed, and reject allocation-using structures under noAllocator.
Dynamic per-entrypoint account schemas (3-5 days): replace the current module-wide fixed schema with runtime account parsing before dispatch, so instruction-data offsets no longer depend on every entrypoint sharing the same account list.
Token-2022 and richer SPL coverage (3-5 days per iteration): add checked Token-2022 extension routes, associated-token account setup flows, and remaining SPL variants beyond the covered mint-authority set_authority path without moving those details into portable IR.
Developer ergonomics and framework surface (3-5 days per iteration): extend the new surface layer toward Lean .lean/Lean SDK contract syntax with richer typed account/data wrappers, richer generated client APIs, broader SPL/Token-2022 helper coverage, and diagnostics that map generated assembly failures back to SDK declarations.

The fastest credible route to a more complete SDK is therefore: the alpha observability baseline is now in place, so next close the richer beta syscall and return-data slices, then remove remaining architecture shortcuts before adding Anchor/Pinocchio-class ergonomics.

Workstream 8: Move Source Generation POC (Aptos first)

Goal: avoid pretending Move is another Lean runtime target. Tasks:

Done: define a Move-compatible subset of the portable IR (see move-family.md).
Done: generate one Aptos Move counter package via proof-forge --emit-counter-ir-aptos.
Done: generate Move.toml, sources/counter.move, and tests/counter_tests.move.
Done: add golden fixtures and scripts/aptos/build-examples.sh diff gate.
Done: add Tests/AptosDiagnostics.lean so unsupported capabilities fail before codegen.
In CI: run aptos move compile/test (the AptosFramework git dependency fetch is slow and may time out locally; the CI job uses a 10-minute timeout).
Document verifier restrictions that must feed back into IR design.

Acceptance criteria:

Generated Aptos Move source shape is locked by golden fixtures and diff gate.
Generated package has unit tests (tests/counter_tests.move).
Unsupported Lean constructs fail before codegen.
Follow-up Sui object POC is documented as a separate milestone.

Workstream 9: CI Expansion

See validation-gates.md for current and planned validation commands. Goal: keep CI useful without requiring every external chain tool on day one. Tasks:

Keep lake build as always-on CI.
Add EVM smoke only when solc and Foundry are available.
Add optional jobs for CosmWasm, Solana, and Move with clear tool checks.
Add artifact metadata validation as a tool-independent job.

Acceptance criteria:

Base CI does not fail because optional chain tools are missing.
Target-specific CI jobs fail loudly when their toolchain is present but the target build fails.
Metadata schema validation runs without chain tools.

Workstream 10: Psy DPN ZK Target Spike

Goal: validate a ZK circuit sourcegen target without coupling ProofForge to Psy compiler internals. Tasks:

Done: generate one Counter .psy source file from a portable IR fixture.
Done: add a temporary Dargo package generator in scripts/psy/counter-smoke.sh.
Done: document dargo test --file as the first local smoke runner.
Done: run dargo compile with the psyup v0.1.0 macOS arm64 toolchain and capture DPN circuit JSON.
Done: run dargo execute as a local user/contract session and assert the Counter result after two increments.
Done: call dargo generate-abi and capture non-empty ABI JSON.
Done: emit proof-forge-artifact.json with target id psy-dpn for Psy smoke artifacts.
Done: add ContextProbe as a non-Counter fixture for parameter lowering and context reads.
Done: add HashProbe for Hash, typed hash let-bindings, hash, and hash_two_to_one, aligned with upstream Psy hash tests.
Done: validate Psy artifact metadata, including hashes, byte sizes, capabilities, validation flags, and expected execution results.
Done: add map/storage-map, assertions, bounded-loop, array, struct, aggregate ABI, nested aggregate, storage nested aggregate, U32 arithmetic, and bitwise coverage from the upstream psy-compiler/tests and psy-precompiles corpus.
Done: add U32/Hash limb packing coverage for local arrays and ABI parameters from the upstream psy-precompiles corpus.
Done: emit and validate ProofForge deploy manifests for all Dargo-backed Psy smoke compile outputs.
Done: add map storage path coverage for Map<Hash, Hash, N> with Dargo compile/execute validation.
Done: add expression-position storageMapSet lowering and MapProbe coverage for upstream map edge semantics where set and repeated insert return the previous Hash value.
Done: add storage-reference compound assignment coverage for scalar storage and generic storage paths with Dargo compile/execute validation.
Done: add native U32 scalar storage coverage using Psy pub value: u32 storage plus scalar += assignment, with Dargo compile/execute validation.
Done: add native Bool scalar storage coverage using Psy pub flag: bool storage plus bool as Felt return casts, with Dargo compile/execute validation.
Done: add native Bool fixed-array and storage-array coverage using Psy [bool; N] literals/indexing plus pub flags: [bool; N] storage, with Dargo compile/execute validation.
Done: add native Hash scalar and storage-array coverage using Psy pub root: Hash and pub roots: [Hash; N], with Dargo compile/execute validation.
Done: add fixed-array equality coverage using Psy assert_eq, ==, and != over [Felt; N] locals, with Dargo compile/execute validation.
Done: add U32 storage array coverage using Felt-backed storage plus explicit U32 read/write casts, with Dargo compile/execute validation.
Done: add Felt-backed U32 storage-array path compound assignment lowering as explicit read/update/write casts, with Dargo compile/execute validation.
Done: add native U32 storage struct field path writes, reads, and compound assignment coverage, with Dargo compile/execute validation.
Done: add a Psy IR coverage manifest gate so every portable IR constructor must be classified as lowered, validated, unsupported, or structural for the Psy backend.
Done: factor Dargo smoke package generation into a shared writer so every Psy smoke creates the same src/main.psy and Dargo.toml layout before metadata validation.
Done: allow EVM-style entrypoint selectors in the Psy backend as target-specific ABI metadata; Psy source generation uses method names only and may record the selector in artifact metadata for cross-target traceability.
Done: validate Psy identifiers and duplicate declarations before source generation so invalid names do not fall through to Dargo parser/typechecker failures.
Done: add a generic generated test fallback for valid Psy IR modules that do not have fixture-specific assertions, backed by GenericEntrypointProbe, golden source, Dargo compile/execute validation, ABI generation, deploy manifest generation, and artifact metadata validation.
Convert the deploy manifest path to upstream compressed genesis deploy JSON once the Psy tooling exposes a stable boundary, then exercise a local node/prover deployment smoke.
Record Dargo/Psy compiler version or commit once the toolchain exposes a stable value.

Acceptance criteria:

Generated .psy source is readable and checked into a golden fixture or snapshot.
dargo compile produces a non-empty JSON artifact on a machine with the Psy toolchain.
dargo execute returns result_vm: [2] for the Counter lifecycle.
dargo execute returns result_vm: [15] for ContextProbe’s sum_context(2,3) lifecycle.
dargo execute returns deterministic four-Felt outputs for HashProbe’s poseidon_hash and poseidon_pair_hash entrypoints.
dargo generate-abi produces a non-empty ABI JSON artifact.
dargo execute returns result_vm: [42] for the generic non-whitelisted GenericEntrypointProbe.
Artifact metadata records target id, fixture id, used capabilities, artifact paths, hashes, byte sizes, Dargo package source copy, Dargo package manifest, and validation status.
Artifact metadata is machine-validated by the Psy smoke scripts.
Artifact metadata records Dargo/Psy compiler version or commit once available.
Unsupported non-circuit-friendly IR nodes fail before source generation.
CI either pins a known-good psyup release or skips this gate clearly when a matching toolchain tarball is unavailable.

Workstream 11: Kaspa Toccata Research Target

Goal: decide whether and how ProofForge should support Kaspa’s Toccata programmability stack without pretending it is an EVM, account-state, or generic ZK circuit target. Tasks:

Done: add a docs-first target note for candidate id kaspa-toccata.
Classify the target as UTXO covenant/based-app research, not zk-circuit-sourcegen.
Review candidate capabilities for UTXO state, covenant lineage, transaction v1, user lanes, compute budgets, and inline proof verification.
Decide whether the first spike should generate Silverscript or only produce a target manifest around hand-authored covenant source.
Define a tiny L1 covenant Counter-like scenario with successor-output validation.
Define the minimal artifact metadata shape for covenant source, transaction v1 manifest, covenant lineage manifest, and optional proof verifier manifest.
Defer based-app support until the L1 covenant artifact shape is clear.

Acceptance criteria:

docs/targets/kaspa-toccata.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish inline ZK verification from psy-dpn-style circuit source generation.

Workstream 12: Stellar Soroban Research Target

Goal: decide whether and how ProofForge should support Stellar smart contracts without treating all Wasm contract chains as one target. Tasks:

Done: add a docs-first target note for candidate id wasm-stellar-soroban.
Classify Soroban as a Wasm-host candidate, not a generic Wasm artifact target.
Decide whether the first spike should generate a native Rust/Soroban package or wait for a direct Lean-to-Wasm host bridge.
Review candidate capabilities for address authorization, contract-account authorization, storage TTL, contract spec metadata, and Stellar assets.
Define a tiny Counter-like scenario that exercises storage and event output.
Define artifact metadata for Wasm, contract spec, deployment manifest, toolchain versions, and validation result.
Identify the local smoke command set: stellar contract build, sandbox or testnet deploy, and invoke.

Acceptance criteria:

docs/targets/stellar-soroban.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Soroban from NEAR and CosmWasm despite all three using Wasm artifacts.

Workstream 13: Internet Computer Research Target

Goal: decide whether and how ProofForge should support Internet Computer canisters without treating every Wasm artifact as the same contract target. Tasks:

Done: add a docs-first target note for candidate id wasm-icp-canister.
Classify ICP canisters as a Wasm-host candidate, not a generic Wasm artifact target.
Decide whether the first spike should generate a native Motoko/Rust CDK package or wait for a direct Lean-to-Wasm canister bridge.
Review candidate capabilities for Candid, update/query method modes, stable memory, orthogonal persistence, principals, cycles, async inter-canister calls, canister lifecycle, certified data, and management canister APIs.
Define a tiny Counter-like scenario with one update method and one query method.
Define artifact metadata for Wasm, Candid, canister manifest, stable-state or upgrade policy, toolchain versions, and validation result.
Identify the local smoke command set: local replica, PocketIC, or ICP CLI canister install/call flow.

Acceptance criteria:

docs/targets/internet-computer.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish ICP canisters from NEAR, CosmWasm, and Soroban despite all using Wasm artifacts.

Workstream 14: TON TVM Research Target

Goal: decide whether and how ProofForge should support TON smart contracts without pretending TVM contracts are EVM, Wasm-host, Move, or ZK targets. Tasks:

Done: add a docs-first target note for candidate id ton-tvm.
Classify TON as a TVM/Tolk sourcegen candidate.
Decide whether the first spike should generate Tolk source/package artifacts or wait for a lower-level TVM/cell IR.
Review candidate capabilities for cells, TL-B metadata, inbound messages, outbound messages, get methods, action lists, StateInit, account status, TVM gas, and jetton/token integration.
Define a tiny Counter-like scenario with one internal message and one get method.
Define artifact metadata for source, TVM/BOC output, interface metadata, initial state, message/action schema, toolchain versions, and validation result.
Identify the local smoke command set: Acton/Tolk compile and local test or emulator validation.

Acceptance criteria:

docs/targets/ton-tvm.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish TON TVM from Wasm-host, EVM, Move, and ZK targets.

Workstream 15: Bitcoin Cash CashScript Research Target

Goal: decide whether and how ProofForge should support Bitcoin Cash smart contracts without pretending UTXO spend paths are stateful contract method calls. Tasks:

Done: add a docs-first target note for candidate id bch-cashscript.
Classify BCH/CashScript as a UTXO script/covenant sourcegen candidate.
Decide whether the first spike should generate CashScript source/package artifacts before any lower-level BCH Script path.
Review candidate capabilities for UTXO state, P2SH scripts, unlockers, transaction introspection, covenants, local state, CashTokens, timelocks, signature checks, CashScript artifacts, and transaction-builder validation.
Define a tiny UTXO spend scenario with at least one contract function and a transaction-builder smoke.
Define artifact metadata for .cash source, cashc artifact JSON, bytecode, constructor/unlocker manifest, transaction scenario, toolchain versions, and validation result.
Identify the local smoke command set: cashc, CashScript SDK, MockNetworkProvider, and optional chipnet/node-backed validation.

Acceptance criteria:

docs/targets/bitcoin-cash-cashscript.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish BCH/CashScript from EVM, Wasm-host, Move, generic Bitcoin, and Kaspa/Toccata targets.

Workstream 16: Algorand AVM Research Target

Goal: decide whether and how ProofForge should support Algorand smart contracts without pretending AVM applications are EVM, Wasm-host, Move, Solana, TVM, UTXO, or ZK circuit targets. Tasks:

Done: add a docs-first target note for candidate id algorand-avm.
Classify Algorand as an AVM/TEAL source or package-generation candidate.
Decide whether the first spike should generate Algorand Python or Algorand TypeScript package artifacts before any direct TEAL emitter path.
Review candidate capabilities for stateful applications, LogicSig programs, ARC-4 ABI/app specs, global/local/box storage, transaction groups, resource references, inner transactions, Algorand Standard Assets, AVM budget, and AlgoKit/Puya artifacts.
Define a tiny stateful Counter-like application with one update method, one read/query path, explicit storage schema, and localnet or simulator-backed validation.
Define artifact metadata for source, approval bytecode, clear-state bytecode, optional LogicSig bytecode, ABI/app spec, storage schema, resource references, toolchain versions, and validation result.
Identify the local smoke command set: AlgoKit/Puya compile plus LocalNet or simulator-backed create/call/query validation.

Acceptance criteria:

docs/targets/algorand-avm.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Algorand AVM from Wasm-host, EVM, Move, Solana, TVM, UTXO, and ZK targets.

Workstream 17: Cardano Plutus/Aiken Research Target

Goal: decide whether and how ProofForge should support Cardano smart contracts without pretending eUTXO validators are stateful method-call contracts. Tasks:

Done: add a docs-first target note for candidate id cardano-plutus-aiken.
Classify Cardano as an eUTXO validator sourcegen candidate.
Decide whether the first spike should generate Aiken source before any direct Plutus/UPLC path.
Review candidate capabilities for eUTXO state, validator roles, datum, redeemer, script context, validity ranges, transaction balancing, native tokens, execution units, and Plutus blueprints.
Define a tiny Counter-like eUTXO state-machine scenario with successor-output validation.
Define artifact metadata for Aiken source, UPLC/Plutus validators, blueprint, datum/redeemer schemas, transaction scenario, execution units, toolchain versions, and validation result.
Identify the local smoke command set: Aiken compile/test plus emulator, SDK-backed transaction, or cardano-node-backed validation.

Acceptance criteria:

docs/targets/cardano-plutus-aiken.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Cardano from EVM, Wasm-host, Move, Solana, TVM, AVM, generic Bitcoin, BCH/CashScript, and Kaspa/Toccata targets.

Workstream 18: Tezos Michelson/LIGO Research Target

Goal: decide whether and how ProofForge should support Tezos smart contracts without hiding Michelson operation-list semantics behind generic contract calls. Tasks:

Done: add a docs-first target note for candidate id tezos-michelson-ligo.
Classify Tezos as a Michelson source/artifact target with LIGO as the first sourcegen path.
Review candidate capabilities for Michelson code, entrypoints, typed Micheline storage, big_map, operation lists, views, events, tickets, Sapling, delegation, gas/storage burn, and LIGO artifacts.
Define a tiny Counter-like contract with one entrypoint, one view, typed storage, and a local test or sandbox validation flow.
Define artifact metadata for LIGO source, Michelson output, parameter/storage schema, operation list, view/event manifest, toolchain versions, and validation result.
Identify the local smoke command set: LIGO compile/test plus Octez sandbox or equivalent Tezos local validation.

Acceptance criteria:

docs/targets/tezos-michelson-ligo.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Tezos from EVM, Wasm-host, Move, Solana, TVM, AVM, UTXO, and ZK targets.

Workstream 19: Starknet Cairo Research Target

Goal: decide whether and how ProofForge should support Starknet smart contracts without treating Cairo chain contracts as generic ZK circuits. Tasks:

Done: add a docs-first target note for candidate id starknet-cairo.
Classify Starknet as a Cairo/Sierra/CASM sourcegen candidate.
Review candidate capabilities for Cairo source, Sierra, CASM, class declaration, class hash, Starknet ABI, storage, account abstraction, syscalls, L1/L2 messaging, Starknet fee/resource constraints, and Starknet Foundry validation.
Define a tiny Counter-like contract with storage, an increment external function, a read function, and one event.
Define artifact metadata for Cairo source, Sierra/CASM artifacts, ABI, selector/class-hash metadata, deployment manifest, toolchain versions, and validation result.
Identify the local smoke command set: Scarb build plus snforge or devnet-backed tests.

Acceptance criteria:

docs/targets/starknet-cairo.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Starknet from EVM, Wasm-host, Move, Solana, TVM, AVM, UTXO, and psy-dpn-style ZK circuit targets.

Workstream 22: Aleo Leo Research Target

Goal: decide whether and how ProofForge should support Aleo programs without treating Aleo as only a generic ZK circuit target or confusing Aleo VM with Algorand AVM. Tasks:

Done: add a docs-first target note for candidate id aleo-leo.
Classify Aleo as a ZK application sourcegen candidate with Leo as the first source boundary, Aleo Instructions as the lower-level compiler target, and Aleo VM bytecode as the deployable execution artifact.
Review candidate capabilities for Leo source, Aleo Instructions, Aleo VM, AVM bytecode, ABI, prover/verifier artifacts, transitions, finalization, records, mappings, storage, public/private inputs and outputs, program imports/upgrades, execute/deploy transactions, Credits fees, Leo tests, and devnet validation.
Define a tiny Counter-like program with one entry fn, one public mapping, and one final { } block.
Define a second private-record scenario that consumes one encrypted record, creates a successor record, and records public/finalization effects only when required.
Define artifact metadata for Leo source, program id/imports, record/mapping schemas, finalization manifest, Aleo Instructions, Aleo VM bytecode, ABI, prover/verifier artifacts, execute/deploy transaction metadata, toolchain versions, and validation result.
Identify the local smoke command set: leo build, leo test, optional leo test --prove, leo execute --print, and devnet/devnode-backed deploy or execute validation.

Acceptance criteria:

docs/targets/aleo-leo.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Aleo from psy-dpn, Zcash Shielded, Kaspa/Toccata inline ZK, Starknet Cairo, Algorand AVM, and generic source-generation targets.

Workstream 20: Bitcoin Script/Miniscript Research Target

Goal: decide whether and how ProofForge should support Bitcoin base-layer spending policies without pretending Bitcoin Script is a general smart-contract runtime. Tasks:

Done: add a docs-first target note for candidate id bitcoin-script-miniscript.
Classify Bitcoin as a limited UTXO spending-policy target through Script, Miniscript, descriptors, PSBT, and Bitcoin Core validation.
Review candidate capabilities for Bitcoin Script, Miniscript, descriptors, SegWit, Taproot, Tapscript, witness stacks, sighash modes, hash locks, threshold multisig, PSBT flows, standardness, weight/fee constraints, and Bitcoin Core regtest validation.
Define a tiny spending-policy scenario such as “A can spend immediately, or B can spend after a relative timelock.”
Define artifact metadata for policy, descriptor, output script, witness requirements, PSBT/raw transaction scenario, weight/fee, toolchain versions, and validation result.
Identify the local smoke command set: Bitcoin Core regtest, descriptor import or address derivation, PSBT signing/finalization, and testmempoolaccept or equivalent spend validation.

Acceptance criteria:

docs/targets/bitcoin-script-miniscript.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Bitcoin Script/Miniscript from EVM, Wasm-host, Move, Solana, TVM, AVM, Cardano eUTXO, BCH/CashScript, Kaspa/Toccata, and generic smart-contract targets.

Workstream 21: Zcash Shielded Research Target

Goal: decide whether and how ProofForge should support Zcash shielded payments without treating Zcash as either plain Bitcoin Script or a generic ZK smart-contract chain. Tasks:

Done: add a docs-first target note for candidate id zcash-shielded.
Classify Zcash as a privacy UTXO/ZK payment candidate with transparent Zcash flows plus Sapling/Orchard shielded pools.
Review candidate capabilities for shielded privacy, transparent pool crossings, Sapling, Orchard, shielded notes, note commitments, nullifiers, commitment tree anchors, Zcash protocol proofs, private witnesses, value-balance constraints, viewing keys, unified addresses, privacy policy, and zcashd/library validation.
Define a tiny shielded payment scenario such as “spend one Orchard note, create one Orchard note, reveal one nullifier, preserve value balance, and pay a transparent fee.”
Define how a JDL-Z11-like script may express shield, spendNote, createNote, revealNullifier, selectAnchor, and privacyPolicy while rejecting global mutable shielded storage, method dispatch, and arbitrary proof verification.
Define artifact metadata for transparent inputs/outputs, shielded pool, note input/output schema, nullifiers, anchors, value balance, witness/proving requirements, viewing-key disclosure, toolchain versions, and validation result.
Identify the local smoke command set: zcashd RPC or a compatible Rust wallet/protocol library, with an explicit fallback blocker if local proving is too heavy for CI.

Acceptance criteria:

docs/targets/zcash-shielded.md records the target classification and non-goals.
Capability candidates remain documented but are not added to ProofForge.Target.Capability until reviewed.
The first spike has a reproducible local validation command or a documented external-tool blocker.
The docs distinguish Zcash from Bitcoin Script/Miniscript, BCH/CashScript, Kaspa/Toccata inline ZK, psy-dpn circuit sourcegen, and generic smart contracts.

Workstream 23: Multi-Chain Token SDK

Goal: let users describe fungible token intent once, then let --target choose ERC-20 contract generation on EVM or SPL Token / Token-2022 plans on Solana without exposing chain-specific code at the user-facing SDK layer. Tasks:

Done: add RFC 0006, ProofForge.Contract.Token.TokenSpec, target token plans, and Tests/TokenSpec.lean.
Done: add legacy Learn token intent source syntax, ProofForge.Contract.Token.Learn, Examples/Learn/ProofToken.learn, Examples/Learn/FeeToken.learn, Tests/TokenLearn.lean, and proof-forge --learn-token --target <id> plan emission as a compatibility path into TokenSpec.
Done: add the first EVM ERC-20 artifact emitter for Learn token sources: ProofForge.Contract.Token.Evm, Tests/TokenEvm.lean, standard ERC-20 selectors/events in metadata, Yul generation, and solc --strict-assembly bytecode validation through --learn-token --target evm.
Done: add scripts/portable/learn-token-smoke.sh / just learn-token-smoke to validate the EVM ERC-20 token artifact path and the Solana Token-2022 plan path from Learn source.
Done: add scripts/evm/learn-token-erc20-vm-smoke.sh / just learn-token-evm-vm to deploy the generated ERC-20 creation bytecode in an EthereumJS VM and validate standard ERC-20 calls, Transfer/Approval topics, and insufficient-balance revert behavior.
Done: implement Solana SPL Token / Token-2022 deployment plan rendering at the Lean TokenSpec layer. solanaTokenDeploymentPlan now records mint account creation, associated token accounts, mint_to, transfer_checked, approve, burn, revoke, authority changes, Token-2022 extension initialization, Solana program ids, and source documentation references.
Done: route Token-2022 features such as transfer_fee, non_transferable, confidential_transfer, and transfer_hook to Token-2022 extension metadata rather than custom per-token programs. The planner rejects the documented incompatible transfer_fee + non_transferable combination.
Done: extend scripts/portable/learn-token-smoke.sh so the legacy .learn input path reuses the Lean TokenSpec plan, emits both SPL Token and Token-2022 structured plan JSON, and validates the plan offline with @solana/spl-token / @solana/web3.js instruction builders.
Done: add scripts/solana/token-plan-web3-smoke.sh / just solana-token-plan-web3 to execute the structured legacy SPL Token plan on Surfpool. The live runner creates the mint and associated token accounts, mints initial supply, executes the planned mint_to, transfer_checked, approve, burn, revoke, and mint-authority set_authority operations, and validates balances, supply, delegate state, and authority revocation with Web3.js reads.
Done: add scripts/solana/token-2022-transfer-fee-web3-smoke.sh / just solana-token-2022-transfer-fee-web3 to execute the structured Token-2022 transfer-fee plan on Surfpool. The live runner initializes TransferFeeConfig, creates Token-2022 associated token accounts, mints initial supply, executes TransferCheckedWithFee, validates the source balance, recipient net balance, and recipient withheld fee, directly withdraws withheld fees from a token account, then runs a second transfer, harvests withheld fees to the mint, withdraws them from the mint, and validates the fee receiver balance plus cleared account/mint withheld amounts with Web3.js reads.
Done: add ProofForge.Contract.Token.Examples.SoulboundToken, Tests/TokenPlanEmit.lean, scripts/solana/token-2022-non-transferable-web3-smoke.sh, and just solana-token-2022-non-transferable-web3 to execute a Lean .lean TokenSpec-backed Token-2022 non-transferable plan on Surfpool. The live runner initializes NonTransferable, creates Token-2022 associated token accounts, mints initial supply, verifies mint/account extensions, proves TransferChecked is rejected, then burns the token and validates balances and supply with Web3.js reads.
Implement EVM ERC-20 lowering: ABI/selectors, balance/allowance storage, total supply, transfer/approve/transferFrom, mint/burn options, events, and broader Foundry/Web3 behavior tests.
Continue Surfpool live validation for Token-2022 extension plans beyond the transfer-fee initialization, checked-transfer, direct withdraw, and harvest-to-mint withdraw paths plus non-transferable transfer rejection: confidential transfer setup and transfer-hook routing.
Add optional Solana wrapper/authority/transfer-hook program generation for custom policies such as capped supply or custom transfer restrictions.
Extend token-specific artifact metadata with live deployment accounts, tool versions, and validation-run results once the Surfpool plan runner lands.

Acceptance criteria:

A Lean-authored TokenSpec has deterministic EVM and Solana token plans; the legacy Learn token source lowers to the same TokenSpec boundary.
EVM output emits ERC-20 Yul/bytecode and passes ERC-20 behavior tests using standard Web3/Foundry calls.
Solana output renders structured SPL Token / Token-2022 plans, validates the instruction builders offline with @solana/spl-token, and now executes the legacy SPL Token plan plus the Token-2022 transfer-fee and non-transferable plans on Surfpool to create mints and token accounts, mint supply, transfer tokens where allowed, validate balances, verify withheld transfer fees, collect those fees through both direct account withdraw and harvest-to-mint plus mint withdraw, reject non-transferable TransferChecked, and burn non-transferable supply. Confidential transfer and transfer-hook behavior remains follow-up.
Documentation clearly says Solana does not default to a per-token SPL contract; it uses SPL Token / Token-2022 programs by plan and CPI.

Workstream 24: Architecture Convergence Follow-ups (post-merge)

The 2026-07 branch consolidation merged solana-supprot, lookdown (Wasm/NEAR), aleo-support, and cloudflare-support into the trunk, resolved the D-025/D-026/D-027 decision-id collisions (NEAR decisions renumbered to D-029–D-031, Aleo to D-032, Cloudflare to D-033), unified the capability matrix, and fixed the IR.Statement.release semantic conflicts in the EVM event walker, Leo emitter, and TS emitter. Remaining follow-ups: Tasks:

Record the branch policy in development-standards.md: chains are directories and target ids, not branches; changes to ProofForge/IR/*, ProofForge/Target/*, ProofForge/Contract/{Spec,Intent,Source}*, docs/capability-registry.md, docs/decisions.md, and docs/portable-ir.md land on main in standalone PRs.
Record the i18n rule: feature branches do not touch docs/zh/*.zh.md or scripts/i18n/manifest.json; translation sync runs on main only.
Retire the merged remote branches (DaviRain-Su/solana-supprot, DaviRain-Su/lookdown, DaviRain-Su/aleo-support, DaviRain-Su/cloudflare-support) after the consolidation PR lands.
Regenerate stale docs/zh translations flagged by the post-merge manifest (hand-merged decision/capability tables are synced; narrative docs that changed under auto-merge should be re-run through translate-docs.py).
Decide whether the Solana bump-allocator selection unifies under the merged TargetProfile.deploymentAllocator? abstraction or stays target-local; record the outcome in decisions.md.
Unify the CI workflow: the merged .github/workflows/ci.yml now carries EVM, Solana-light, NEAR, and Psy gates; add the Aleo and TS/Cloudflare smokes as optional jobs once their toolchains (leo, tsc/wrangler) are pinned.
Naming cleanup: decide the public SDK name, schedule the Lean.Evm → ProofForge.* namespace rename, and enforce the Learn freeze (authoring-model).
Declare ContractSpec → EVM Plan → Yul the EVM product pipeline in RFC 0004; label LCNF → EmitYul as the Lean-native experimental path.
Decide whether wasm-cloudflare-workers keeps its registry entry under wasmHost or moves to a distinct off-chain host family (no consensus, no on-chain state) so it does not dilute capability semantics; record in decisions.md alongside D-033.
Done: record Gate G0 and the stricter Gate P0 primary-chain completion covenant in decisions.md, target-roadmap.md, and gate-status.md. Gate G0 closes the shared behavior/budget slice; until Gate P0 closes, new and non-primary targets stay docs-only or maintenance-only — no registry, capability, testkit, CI, or product-scope advancement.

Acceptance criteria:

docs/decisions.md shows one linear decision log (D-001…D-045, no duplicate ids), records the allocator-unification outcome, and aligns D-039/RFC 0009 plus D-045/Gate P0 with the codebase’s actual state.
Development standards contain the branch and i18n rules.
All four merged chain branches are deleted or archived.

Workstream 25: Formal Verification Roadmap

Goal: convert the platform’s core promises into machine-checked theorems, per formal-verification.md. Tasks (see the roadmap for full statements):

FV-1: prove capability routing soundness, rejection completeness, and Solana target-extension isolation for resolveSpec (D-027/D-028 as theorems).
FV-2: extend ProofForge/IR/Semantics.lean beyond the scalar subset (maps, arrays, structs, ifElse, boundedFor, events) and prove determinism plus bounded-loop termination.
FV-3: prove the IR/Ownership.lean checker sound against release-aware semantics (no use-after-release, no double release), justifying the three divergent release lowerings (EmitWat allocator, EVM/Psy reject, TS no-op).
FV-4: EVM Counter, ValueVault, and EvmExpressionProbe executable trace obligations are done in Backend/Evm/Refinement.lean, backed by Backend/Evm/YulSemantics.lean. The obligations mirror Backend/WasmNear/Refinement.lean for scalar IR traces, check the selector-dispatched Yul surface, and execute the focused emitted Yul subset (calldataload, calldatasize, sstore, sload, scalar arithmetic, exp, bitwise/shift operators, comparisons, casts, assertions, number, keccak256, log0-log4, mstore, return) to compare observable EVM return words against the IR trace. ValueVault covers calldata arguments, multi-entry scalar storage updates, block-number context reads, event field evaluation, and return words; EvmExpressionProbe covers assertion success paths, assertEq, predicate expressions, U32/U64 arithmetic, casts, bitwise operators, and shifts. Next: extend the interpreter and obligations toward maps, arrays, structs, and aggregate return/state shapes; keep Psy/Solana on differential gates until interpreters exist.
FV-5: state checked-arithmetic overflow/division semantics once in the IR value domain and add the overflow branch to backend obligations.
FV-6: prove .learn-vs-contract_source lowering equivalence for the paired fixture subset (decidable ContractSpec equality).
FV-7: prove Token SDK plan invariants (total feature routing, documented incompatibility diagnostics, plan well-formedness).
FV-8: user-facing contract invariants over IR semantics, ValueVault as the worked example.

Acceptance criteria:

Each landed FV item is a decide-checkable theorem or Lean test wired into CI, not an external-tool dependency.
A backend cannot move from Experimental to Supported without its FV-4 trace obligation and shared-scenario differential gate.

Workstream 26: Unified Rust Test Framework (testkit)

Goal: replace per-chain shell/Node harness sprawl with one declarative scenario format and Rust in-process executors, per RFC 0007. Tasks (one milestone per implementing branch):

M1: create the testkit/ Cargo workspace (core + scenario TOML model, discovery, reporting); port runtime/offline-host into harness-near (wasmtime + NEAR host shim, allocator counters preserved); Counter scenario green on wasm-near; add just testkit and one CI step.
M2: harness-evm on revm — load emitted runtime bytecode, dispatch via .evm-methods selectors, decode return words; Counter green on evm; first cross-target equivalence assertion (evm ↔ wasm-near observable traces).
M3: harness-solana on mollusk-svm — absorb the Tests/solana/*_mollusk.rs.tpl logic as library code; Counter green on all three targets. Status: Counter is now wired through mollusk-svm in testkit/harness-solana, including golden assembly, manifest, artifact metadata, sBPF ELF build, stateful scenario execution, and three-target trace parity when sbpf and solana-keygen are available. ValueVault is now covered by testkit/scenarios/value-vault.toml, typed scalar scenario args, runtime/offline-host --inputs-hex, the NEAR/Wasm EmitWat fixture, the Solana ValueVault sBPF/Mollusk harness, and the EVM/revm harness when Foundry cast is available for selector hydration.
M4: migrate golden-file comparisons and per-fixture behavior scripts into scenario steps; retire duplicated shell scripts; collapse the per-fixture CI steps into the testkit run. Live/chain-authentic gates (Foundry, Anvil deploy, Surfpool, near-sandbox, dargo, leo) remain separate scheduled or labeled jobs. Status: the first M4 slice is in place through scenario-declared [[artifact]] expectations. Counter’s Solana golden assembly/manifest checks and ValueVault’s WAT/Yul/sBPF/manifest/metadata source-shape checks now live in scenario TOML instead of hardcoded fixture-specific harness branches. The second slice adds nested [[artifact.json]] and [[artifact.toml]] checks so Solana Counter and ValueVault metadata/manifest fields, instruction names/tags, capability membership, and validation status are asserted declaratively by the scenario runner. The follow-up slice removes the duplicated Solana harness-internal metadata/manifest semantic validators and leaves only runtime dispatch parsing in testkit/harness-solana. The next slice tightens scenario discovery so empty or duplicate target ids and artifact expectations for undeclared targets fail before any harness runs. The current EVM slice moves EVM artifact metadata identity, capability, validation, and ABI entrypoint-name expectations into scenario-declared [[artifact.json]] checks, leaving testkit/harness-evm responsible only for selector parsing and runtime execution. The current diagnostic slice adds scenario-declared [[diagnostic]] expectations and a diagnostic-only unsupported-crosscall scenario that proves solana-sbpf-asm rejects the portable crosscall.invoke capability with the expected target/capability message. The current EVM golden slice adds Examples/Evm/Counter.golden.yul as the portable IR Counter Yul golden and makes testkit/scenarios/counter.toml assert the generated EVM Yul through matches_file; the older Lean SDK contract golden stays under Examples/Evm/Contracts/. The current Wasm/NEAR golden slice adds Examples/WasmNear/Counter.golden.wat and makes the same Counter scenario assert generated EmitWat output through matches_file, so Counter now has scenario-declared source equality for wasm-near, evm, and solana-sbpf-asm. The current ValueVault Wasm/NEAR golden slice adds Examples/WasmNear/ValueVault.golden.wat and makes testkit/scenarios/value-vault.toml assert generated EmitWat output through matches_file. The current ValueVault Solana golden slice adds Examples/Solana/ValueVault.golden.s and Examples/Solana/ValueVault.manifest.toml, making the same scenario assert generated sBPF assembly and manifest output through matches_file. The current ValueVault EVM golden slice adds Examples/Evm/ValueVault.golden.yul and makes the same scenario assert generated EVM Yul through matches_file, so ValueVault now has scenario-declared source equality for wasm-near, solana-sbpf-asm, and evm. The current metadata file-reference slice adds nested [[artifact.file]] checks, makes scenarios assert that JSON metadata file entries point at harness-produced artifacts and match path, byte size, and SHA-256 hash, and exposes EVM init-code/deploy-manifest outputs as testkit artifacts. The current cross-artifact JSON slice adds nested [[artifact.jsonArtifact]] checks, validates that Solana ValueVault metadata embeds the same IDL JSON as the generated IDL artifact, and moves the ValueVault IDL/client schema-shape checks into scenario TOML. The current structured-length slice adds length assertions to nested [[artifact.json]]/[[artifact.toml]] checks and uses them to pin Counter and ValueVault ABI entrypoint, event, capability, artifact, manifest instruction, Solana instruction, and IDL instruction counts declaratively. The current structured-schema slice adds exists, kind, and non_empty checks for nested JSON/TOML artifact assertions, then makes Counter and ValueVault validate EVM deploy manifests as first-class scenario artifacts, including init-code mode, absent chain profile, not-generated broadcast status, ABI and capability shape, and file references back to generated Yul, bytecode, and init-code artifacts.

Acceptance criteria:

One scenario file drives all three priority targets when optional Solana tooling is available; adding a covered feature requires no new script, recipe, or CI step.
A scenario using an unsupported capability asserts compile-time rejection with a diagnostic (never silently skips a target).
Runner is deterministic and network-free by default; revm, mollusk-svm, and wasmtime versions are pinned.
Lean-side compiler tests (diagnostics, coverage manifests, formal anchors) remain in Tests/*.lean and are not moved.

Workstream 27: Allocator Abstraction Unification

Goal: one chain-neutral allocator model bound per target, per RFC 0008; resolves the Workstream 24 allocator-unification decision. Tasks:

M1: generalize ProofForge/IR/Allocator.lean to the strategy/region/release triple (existing constructors map onto it; EmitWat behavior unchanged); record the decision in decisions.md.
M2: fold Solana’s RuntimeAllocator (Backend/Solana/Extension.lean) into the shared model — solana.allocator.* metadata keys stay as the Solana configuration syntax but populate the shared type; IDL renders from it; Tests/SolanaAllocator.lean updated.
M3: add the explicit EVM binding (bump over call-scratch memory; documents what EmitYul/EVM plan already do); define the criteria for moving EVM release from rejection to checked no-op (blocked on FV-3 ownership soundness).
M4: allocator behavior scenario in testkit (Workstream 26) across the three harnesses; NEAR asserts allocator counters, EVM/Solana assert observable-trace equality with release as no-op.

Acceptance criteria:

One AllocatorModel type is consumed by EmitWat, the Solana backend, and the EVM binding; no parallel allocator records remain.
Persistent-state models (EVM storage, Solana accounts, NEAR storage) are explicitly out of scope and unchanged.
Capability gating via runtime.allocator cites alloc.* ids in diagnostics for unsupported release/strategy demands.

Workstream 28: Target Portfolio Sequencing

Goal: execute the tiered portfolio in target-roadmap.md (D-034). Gates, not dates; one milestone per implementing branch. Completion-first rule (D-044, 2026-07-03): finish the three Tier-0 targets — solana-sbpf-asm, evm, wasm-near, in that implementation priority — to full DoD (behavior parity and resource budgets per D-040) before any new-chain advancement. Per-criterion status lives in gate-status.md.

Tier-0 completion (current top priority, blocks everything below)

Done: NEAR budget reporting is wired through the testkit as a wasmtime-fuel proxy, with Counter and ValueVault baselines pinned alongside Solana CU and EVM gas. A precise NEAR host-gas model remains a P0 hardening refinement, not a Gate G0 blocker.
Done: ValueVault budget baselines are pinned for solana_cu, evm_gas, and near_gas across the three primary targets in testkit/scenarios/value-vault.toml.
EVM semantic-plan migration (Workstream 3): ExprPlan, StmtPlan, EntrypointPlan, EventPlan, CrosscallPlan, MetadataPlan — then retire the old IR.lean -> Yul lowering. Non-blocking for Gate G0 budgets but on the EVM hardening track.
Solana Pinocchio CI equivalence (Workstream 7): the source/reference equivalence suite is included in just solana-light; remaining work is to make the live-equivalence harnesses pass in CI by installing Solana rustc/ platform-tools reliably.
Freeze the landed Aptos/CosmWasm spikes at their current M1/M2 state: no Tier-1 M3/M4, no registry stage, no Tier-2 start, until Gate P0 closes.

Tasks:

Done: Gate G0 (Tier-0 behavior/budget slice) is closed. Evidence lives in gate-status.md.
Gate P0 (primary-chain sign-off): Gate G0 plus the remaining production-grade hardening for Solana, Ethereum/EVM, and NEAR/Wasm from D-045.
Tier 1a wasm-cosmwasm: M1 CosmWasm host imports + region-allocator ABI in EmitWat (the cosmWasmRegion binding from RFC 0008); M2 Counter artifact passes cosmwasm-check; M3 testkit harness-cosmwasm scenario green with cross-target equivalence vs wasm-near; M4 registry stage → Experimental.
Tier 1b move-aptos (parallel to 1a): M1 IR → Move module printer for the Counter subset; M2 aptos move test gate + golden fixture; M3 testkit CLI-wrapped executor; M4 capability rows validated; move-sui only after M4.
Tier 2 (each behind its enabler, see roadmap): wasm-stellar-soroban after CosmWasm M4; wasm-icp-canister additionally requires an async/inter-canister design note before any code; starknet-cairo is the first sourcegen-lane pick after Aptos M4; ton-tvm, algorand-avm, cardano-plutus-aiken, tezos-michelson-ligo follow the one-active-sourcegen-spike rule.
Tier 3 Bitcoin policy family (opens at Gate G2 = both Tier-1 exits): M1 policy IR (predicate tree) + policy.* capability ids in the registry docs; M2 rust-miniscript/descriptor emission for the 2-of-3 + timelock-recovery shared policy scenario; M3 PSBT/regtest testkit gate; M4 Lean policy-property checks (path reachability, participant non-omission) as decide-checked theorems. bch-cashscript, zcash-shielded, and kaspa-toccata stay parked behind M4.

Acceptance criteria:

Primary-chain completion covenant (D-045): solana-sbpf-asm, evm, wasm-near reach production-grade DoD before any Tier-1 advancement; the landed Aptos/CosmWasm spikes stay frozen at M1/M2.
No Tier-1 code lands before Gate P0; no Tier-2 target starts before its listed enabler; at most one sourcegen spike is active at any time.
Policy-family targets never appear in contract-family capability rows; they get a separate policy.* section in the capability registry when Tier 3 opens.

Workstreams 29–33: Platform Hardening (planning-first)

These come from the 2026-07 gap analysis. Each starts as an RFC, not code; sequencing hooks are listed in the gap doc.

Workstream 29 — CLI product surface. RFC 0009 is accepted and M1 is landed: proof-forge build|emit|check --target <id> --fixture <id> exists through the compatibility layer, check is a real validation verb, list commands are wired, and legacy flags have alias/deprecation metadata. Remaining work is M3/M4: migrate scripts/testkit callers to the target-first surface and delete the legacy flag zoo only after the compatibility window.
Workstream 30 — Versioning and compatibility policy. RFC covering IR version rules (tied to the coverage-manifest gate), artifact/deploy schema stability, append-only capability ids, and SDK deprecation policy.
Workstream 31 — Resource budgets as gates. ✅ Implemented. The testkit scenario schema supports per-step solana_cu, evm_gas, and near_gas budgets with baselines and tolerance bands; the runner reports measured budgets and fails on regression. Counter baselines are locked for Solana CU and EVM gas; NEAR gas is reported as wasmtime fuel (info-only proxy) until a precise host-gas model lands. Gate G0 in target-roadmap.md and validation-gates.md now requires budget assertions.
Workstream 32 — Deployment lifecycle, upgrades, signing. RFC for an upgrade-policy intent (immutable | authority | governance) lowered honestly per chain (Solana upgrade authority, EVM immutable/proxy, NEAR account keys, Aleo @noupgrade) or rejected; unsigned-transaction signing boundary; live-gate key conventions. M1 is implemented: ContractSpec.upgradePolicy? is serialized in ContractSpec JSON, the target resolver rejects unsupported target/policy combinations before code generation, and resolved plans emit upgrade.policy.* artifact metadata for supported policies.
Workstream 33 — Runtime error model + client generation. Portable error codes with per-target encodings and expect.error scenario vocabulary (plan with Workstream 31’s schema change); then a client-schema layer generalizing the Solana IDL/TS client generation to all targets (implementation waits for testkit M3). Milestones:
- M1: Add ErrorRef (assertion_id + optional user_code) to the portable IR assert/assertEq constructors and update every backend pattern match to compile with the new shape. message remains the fallback text. ✅ Implemented.
- M2: Implement per-target error encodings for EVM, Solana, and NEAR: EVM reverts with abi.encode(uint32 assertion_id, string user_code); Solana returns ProgramError::Custom(assertion_id); NEAR panics with a PF:{id}:{code} prefix. ✅ Implemented.
- M3: Extend testkit schema and harnesses with expect.error so a scenario step can assert the exact assertion_id/user_code on failure.
- M4: Define target-neutral ContractSpec JSON schema and generate Solana IDL/client, EVM ABI wrapper, and NEAR wrapper sketches from it.

Suggested Order

Workstreams 1, 1.5, 2–3, 6–7 (registry, portable IR, EVM metadata, Solana asm) are substantially complete; remaining per-target detail lives in each workstream. The forward order follows the tier gates of target-roadmap.md (D-034):

Architecture convergence follow-ups (Workstream 24) and FV-1/FV-2 from the formal verification roadmap (Workstream 25). In parallel, finish the platform-hardening follow-through from the gap analysis: CLI M3/M4 migration after RFC 0009 M1, runtime error vocabulary for testkit, and the versioning / deployment lifecycle policies (30/32, docs-agent parallel track).
Parallel: unified testkit (Workstream 26) and allocator unification (Workstream 27) — testkit M1/M2 has no dependency on allocator M1/M2; allocator M4 lands after testkit M3.
Gate P0 (primary-chain completion covenant, D-045): finish solana-sbpf-asm, evm, wasm-near — in that implementation priority — to production-grade DoD. Gate G0 is the behavior/resource-budget slice; Gate P0 also includes Solana Pinocchio CI equivalence, EVM semantic-plan migration, and NEAR/Wasm local execution, artifact, diagnostic, and CI sign-off. The landed Aptos/CosmWasm spikes stay frozen at M1/M2 until this closes. Per-criterion status: gate-status.md.
Parallel Tier 1 (only after Gate P0 closes): wasm-cosmwasm (Workstreams 5/28) and move-aptos (Workstreams 8/28).
Tier 2 per enabler: Soroban after CosmWasm; Sui and the sourcegen lane (Starknet first pick) after Aptos; ICP additionally behind an async design note; one sourcegen spike at a time (Workstreams 12–19/22, 28).
Bitcoin policy family at Gate G2 (Workstreams 11/15/20/21, 28) — miniscript first, then CashScript/Zcash/Kaspa behind it.
Multi-chain Token SDK follow-ups (Workstream 23) continue alongside, and the remaining live-gate CI matrix (Workstream 9) grows with each target.
Cloud platform design refresh (prerequisite: two+ targets at Experimental with shared-scenario parity; D-010).

​Primary-chain completion covenant (D-045)

​Workstream 1: Target Registry

​Workstream 1.5: Portable IR and Shared Scenario

​Workstream 2: Artifact Metadata

​Workstream 3: EVM Baseline Hardening

​Workstream 4: Wasm Host Runtime Split

​Workstream 5: CosmWasm Spike

​Workstream 6: Solana sBPF Assembly Toolchain Integration (Phase 0)

​Workstream 7: Solana sBPF Assembly Counter Codegen (Phase 1)

​Phase 1 progress (incremental sub-items)

​Solana SDK completion roadmap

​Workstream 8: Move Source Generation POC (Aptos first)

​Workstream 9: CI Expansion

​Workstream 10: Psy DPN ZK Target Spike

​Workstream 11: Kaspa Toccata Research Target

​Workstream 12: Stellar Soroban Research Target

​Workstream 13: Internet Computer Research Target

​Workstream 14: TON TVM Research Target

​Workstream 15: Bitcoin Cash CashScript Research Target

​Workstream 16: Algorand AVM Research Target

​Workstream 17: Cardano Plutus/Aiken Research Target

​Workstream 18: Tezos Michelson/LIGO Research Target

​Workstream 19: Starknet Cairo Research Target

​Workstream 22: Aleo Leo Research Target

​Workstream 20: Bitcoin Script/Miniscript Research Target

​Workstream 21: Zcash Shielded Research Target

​Workstream 23: Multi-Chain Token SDK

​Workstream 24: Architecture Convergence Follow-ups (post-merge)

​Workstream 25: Formal Verification Roadmap

​Workstream 26: Unified Rust Test Framework (testkit)

​Workstream 27: Allocator Abstraction Unification

​Workstream 28: Target Portfolio Sequencing

​Tier-0 completion (current top priority, blocks everything below)

​Workstreams 29–33: Platform Hardening (planning-first)

​Suggested Order

Primary-chain completion covenant (D-045)

Workstream 1: Target Registry

Workstream 1.5: Portable IR and Shared Scenario

Workstream 2: Artifact Metadata

Workstream 3: EVM Baseline Hardening

Workstream 4: Wasm Host Runtime Split

Workstream 5: CosmWasm Spike

Workstream 6: Solana sBPF Assembly Toolchain Integration (Phase 0)

Workstream 7: Solana sBPF Assembly Counter Codegen (Phase 1)

Phase 1 progress (incremental sub-items)

Solana SDK completion roadmap

Workstream 8: Move Source Generation POC (Aptos first)

Workstream 9: CI Expansion

Workstream 10: Psy DPN ZK Target Spike

Workstream 11: Kaspa Toccata Research Target

Workstream 12: Stellar Soroban Research Target

Workstream 13: Internet Computer Research Target

Workstream 14: TON TVM Research Target

Workstream 15: Bitcoin Cash CashScript Research Target

Workstream 16: Algorand AVM Research Target

Workstream 17: Cardano Plutus/Aiken Research Target

Workstream 18: Tezos Michelson/LIGO Research Target

Workstream 19: Starknet Cairo Research Target

Workstream 22: Aleo Leo Research Target

Workstream 20: Bitcoin Script/Miniscript Research Target

Workstream 21: Zcash Shielded Research Target

Workstream 23: Multi-Chain Token SDK

Workstream 24: Architecture Convergence Follow-ups (post-merge)

Workstream 25: Formal Verification Roadmap

Workstream 26: Unified Rust Test Framework (testkit)

Workstream 27: Allocator Abstraction Unification

Workstream 28: Target Portfolio Sequencing

Tier-0 completion (current top priority, blocks everything below)

Workstreams 29–33: Platform Hardening (planning-first)

Suggested Order