| Unified testkit scenarios | just testkit | Rust/Cargo; Lean toolchain from lean-toolchain; solc for the EVM bytecode branch; Foundry cast for Contract SDK selector hydration on the ValueVault EVM branch; optional sbpf plus solana-keygen for the Solana/Mollusk branch | RFC 0007 testkit discovers testkit/scenarios/counter.toml and testkit/scenarios/value-vault.toml, emits WAT fixtures through Lean and runs them on the deterministic runtime/offline-host wasmtime NEAR host, emits EVM runtime bytecode plus artifact metadata and runs the covered scenarios in-process on revm when required EVM tools are available, emits Solana sBPF assembly/manifest/artifact metadata, builds sBPF ELF programs, runs stateful scenarios through mollusk-svm when optional Solana tools are available, validates scenario-declared artifact expectations including Counter golden source equality for Wasm/NEAR WAT, EVM Yul, and Solana assembly/manifest, ValueVault golden equality for Wasm/NEAR WAT, EVM Yul, and Solana sBPF assembly/manifest, structured JSON/TOML metadata/manifest path assertions including presence, absence, type, non-empty, and array/object/table/string length checks, EVM deploy manifest schema checks, JSON metadata file-reference checks for generated artifact path/byte-size/SHA-256 entries, cross-artifact JSON equality for embedded Solana IDL metadata, and ValueVault IDL/client shape checks, validates every target’s return expectations, asserts normalized observable trace parity across executed targets, and (per RFC 0010) reports per-step resource budgets: Solana CU from Mollusk, EVM gas from revm, and wasmtime fuel as an info-only NEAR gas proxy; counter.toml locks Solana CU and EVM gas baselines with tolerance bands and fails the run on regression | Live NEAR sandbox deployment, live EVM RPC/deployment behavior, Surfpool/Web3 Solana deployment behavior, replacement of all legacy per-target smoke scripts, event/log parity, protocol-fee or transaction-pricing modeling, exact NEAR gas equivalence | | |
| Lean package build | lake build | Lean toolchain from lean-toolchain | Library roots typecheck and proof-forge links | Generated Yul/bytecode validity, external tools, runtime behavior | | |
| Target registry smoke | lake env lean --run Tests/TargetRegistry.lean | Lean toolchain from lean-toolchain | The target registry exposes evm as a compiler target while EVM-compatible chain profiles such as robinhood-chain-testnet and anvil-local stay lookup-only deployment profiles | Deployment broadcast, live RPC or explorer reachability, wallet integration | | |
| EVM semantic plan smoke | just evm-plan | Lean toolchain from lean-toolchain | The EVM semantic plan builds from the target-resolved CapabilityPlan, rejects non-EVM target plans, and validates storage layout, scalar storage slots, map value slots, nested map value slots, map presence slots, map assign-op helper requirements, and planned helper requirements before Yul generation | Full ModulePlan ownership of ABI dispatch, events, crosscalls, constructor metadata, artifact metadata, solc acceptance, bytecode, runtime behavior, broader aggregate storage planning | | |
| Solana light gates | just solana-light | Lean toolchain from lean-toolchain; python3; optional cast for the portable ValueVault EVM selector-hydration/Yul branch; optional solc plus cast for its strict-assembly and EVM bytecode metadata branches; optional sbpf and solana-keygen for Solana SDK build branches | Solana target diagnostics, SDK metadata, SDK manifest, generated Solana IDL and TypeScript client artifacts, Contract Source Syntax v1 routing/render checks for Counter and portable ValueVault, Learn source lowering equivalence plus Learn reference diagnostics for CPI/PDA/state helper mistakes, typed account declaration metadata, CPI packing, log lowering, target routing, portable ValueVault Learn-source CLI emission to EVM Yul and Solana sBPF assembly/manifest/IDL/client artifact metadata, token spec, return-data/compute-units SDK helpers, Counter sBPF golden assembly/manifest diff, control-flow/assertion assembly emission, SDK extension artifact metadata, the CI-safe Pinocchio System/SPL Token reference-equivalence suite, and canned sBPF emission when sbpf is available | Full Mollusk runtime coverage, Surfpool/Web3 deployment smoke, public validator deployment, Solana transaction UX, live Pinocchio dual-deploy equivalence | | |
| Token SDK plan smoke | just learn-token-smoke | Lean toolchain from lean-toolchain; python3; optional solc for EVM bytecode; optional Node and npm for Web3.js validation | Validates the legacy .learn token path into the Lean TokenSpec boundary, emits ERC-20 Yul/bytecode metadata when solc is available, emits structured Solana SPL Token and Token-2022 plan JSON, checks mint/ATA/mint_to/transfer_checked/approve/burn/revoke/authority-change plan entries, checks Token-2022 transfer-fee extension routing and withheld-fee collection plan entries, and validates the Solana plan offline with @solana/spl-token / @solana/web3.js instruction builders when Node/npm are available | Live Surfpool execution of all token plan variants, actual token balances, public validator deployment, wallet UX, generated wrapper/transfer-hook programs | | |
| Solana token plan Surfpool/Web3.js smoke | just solana-token-plan-web3 | Lean toolchain from lean-toolchain; python3; surfpool; Solana CLI and solana-keygen; Node; npm | Emits the structured SPL Token plan, starts Surfpool, creates the mint and associated token accounts through @solana/spl-token, mints initial supply, executes the planned mint_to, transfer_checked, approve, burn, revoke, and mint-authority set_authority operations, then verifies token balances, supply, delegate state, and authority revocation through Web3.js reads | Token-2022 extension behavior, generated wrapper/transfer-hook programs, public validator deployment, wallet UX | | |
| Solana Token-2022 transfer-fee Surfpool/Web3.js smoke | just solana-token-2022-transfer-fee-web3 | Lean toolchain from lean-toolchain; python3; surfpool; Solana CLI and solana-keygen; Node; npm | Emits the structured Token-2022 transfer-fee plan, starts Surfpool, initializes a mint with TransferFeeConfig, creates Token-2022 associated token accounts, mints initial supply, executes TransferCheckedWithFee, verifies 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 verifies the fee receiver balance plus cleared withheld amounts through Web3.js reads | Confidential transfer setup, transfer-hook routing, generated wrapper/transfer-hook programs, public validator deployment, wallet UX | | |
| Solana Token-2022 non-transferable Surfpool/Web3.js smoke | just solana-token-2022-non-transferable-web3 | Lean toolchain from lean-toolchain; python3; surfpool; Solana CLI and solana-keygen; Node; npm | Emits a structured Token-2022 plan from the Lean .lean token fixture, starts Surfpool, initializes a mint with NonTransferable, creates Token-2022 associated token accounts, mints initial supply, verifies mint/account extensions, proves TransferChecked is rejected with Transfer is disabled for this mint, then burns the token and verifies balances and supply | Confidential transfer setup, transfer-hook routing, generated wrapper/transfer-hook programs, public validator deployment, wallet UX | | |
| Solana PDA Web3.js derivation smoke | just solana-pda-web3 | Lean toolchain from lean-toolchain; Node; npm | Emits the Solana SDK Vault artifact, reads PDA typedSeeds, and verifies literal/account/bump descriptor semantics against @solana/web3.js PublicKey.findProgramAddressSync and PublicKey.createProgramAddressSync; also covers the local resolver for UTF-8 and instruction-parameter seed descriptors | Live deployment or transaction execution; SPL Token CPI behavior | | |
| Solana System CPI Surfpool/Web3.js smoke | just solana-system-cpi-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated System Program transfer CPI ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the program through @solana/web3.js, verifies recipient lamports increased by the requested amount, and verifies the program-owned state account recorded the same lamports value | System create-account CPI, SPL Token CPI behavior, public validator deployment, Rust/Pinocchio equivalence | | |
| Solana Pinocchio reference-equivalence suite | just solana-pinocchio-reference-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Runs the five CI-safe Pinocchio reference-equivalence smokes below and is included in just solana-light / the default CI build-test job | Live dual-deploy equivalence, Pinocchio reference ELF builds | | |
| Solana Pinocchio System transfer reference-equivalence smoke | just solana-pinocchio-system-transfer-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Emits the generated System Program transfer CPI source/artifact metadata and compares its instruction ABI, account order, signer/writable requirements, CPI metadata, and lamports state write contract against the checked-in Pinocchio reference manifest/source under references/solana/pinocchio/system-transfer | Build/deploy the Pinocchio reference ELF and run ProofForge/reference programs through the same Web3.js harness | | |
| Solana Pinocchio System create_account reference-equivalence smoke | just solana-pinocchio-system-create-account-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Emits the generated System Program create_account CPI source/artifact metadata and compares its instruction ABI, account order, signer/writable requirements, CPI metadata, lamports/space/owner layout, and two-field state-write contract against the checked-in Pinocchio reference manifest/source under references/solana/pinocchio/system-create-account; the optional Cargo check typechecks the Pinocchio reference against pinocchio-system | Build/deploy the Pinocchio create_account reference ELF and run ProofForge/reference programs through the same Web3.js harness | | |
| Solana Pinocchio SPL Token transfer reference-equivalence smoke | just solana-pinocchio-spl-token-transfer-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Emits the generated SPL Token transfer_checked CPI source/artifact metadata and compares its instruction ABI, account order, signer/writable requirements, CPI metadata, decimals/amount layout, and amount state-write contract against the checked-in Pinocchio reference manifest/source under references/solana/pinocchio/spl-token-transfer; the optional Cargo check typechecks the Pinocchio reference against pinocchio-token | Build/deploy the Pinocchio SPL Token reference ELF and run ProofForge/reference programs through the same Web3.js harness | | |
| Solana Pinocchio SPL Token ops reference-equivalence smoke | just solana-pinocchio-spl-token-ops-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Emits the generated SPL Token mint_to/burn/approve/revoke CPI source/artifact metadata and compares its four instruction ABIs, shared account order, signer/writable requirements, CPI metadata, SPL Token instruction layouts, and state-write contract against the checked-in Pinocchio reference manifest/source under references/solana/pinocchio/spl-token-ops; the optional Cargo check typechecks the Pinocchio reference against pinocchio-token | Build/deploy the Pinocchio SPL Token ops reference ELF and run ProofForge/reference programs through the same Web3.js harness | | |
| Solana Pinocchio SPL Token authority reference-equivalence smoke | just solana-pinocchio-spl-token-authority-equivalence | Lean toolchain from lean-toolchain; python3; optional cargo when PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1 | Emits the generated SPL Token set_authority CPI source/artifact metadata and compares its instruction ABI, account order, signer/writable requirements, CPI metadata, SetAuthority instruction layout, and marker state-write contract against the checked-in Pinocchio reference manifest/source under references/solana/pinocchio/spl-token-authority; the optional Cargo check typechecks the Pinocchio reference against pinocchio-token | Build/deploy the Pinocchio SPL Token authority reference ELF and run ProofForge/reference programs through the same Web3.js harness | | |
| Solana Pinocchio System transfer live-equivalence smoke | just solana-pinocchio-system-transfer-live-equivalence | Lean toolchain from lean-toolchain; cargo-build-sbf with Solana rustc/platform-tools; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds the ProofForge System transfer CPI ELF and the checked-in Pinocchio reference ELF, deploys both programs to the same Surfpool instance, invokes the same Web3.js transfer scenario for each, and compares recipient lamport delta plus recorded state value | Move live equivalence into CI once Solana rustc is installed reliably; extend Pinocchio comparisons to Token-2022 and broader SPL helper coverage; just solana-pinocchio-install-sbf-tools repairs missing/corrupted platform-tools | | |
| Solana Pinocchio System create_account live-equivalence smoke | just solana-pinocchio-system-create-account-live-equivalence | Lean toolchain from lean-toolchain; cargo-build-sbf with Solana rustc/platform-tools; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds the ProofForge System create_account CPI ELF and the checked-in Pinocchio reference ELF, deploys both programs to the same Surfpool instance, invokes the same Web3.js create-account scenario for each, and compares lamports/space plus recorded state values | Move live equivalence into CI once Solana rustc is installed reliably; extend Pinocchio comparisons to Token-2022 and broader SPL helper coverage; just solana-pinocchio-install-sbf-tools repairs missing/corrupted platform-tools | | |
| Solana Pinocchio SPL Token transfer live-equivalence smoke | just solana-pinocchio-spl-token-transfer-live-equivalence | Lean toolchain from lean-toolchain; cargo-build-sbf with Solana rustc/platform-tools; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds the ProofForge SPL Token transfer_checked CPI ELF and the checked-in Pinocchio reference ELF, deploys both programs to the same Surfpool instance, invokes the same Web3.js token-transfer scenario for each, and compares token balance deltas plus recorded state values | Move live equivalence into CI once Solana rustc is installed reliably; extend Pinocchio comparisons to Token-2022 and broader SPL helper coverage; just solana-pinocchio-install-sbf-tools repairs missing/corrupted platform-tools | | |
| Solana Pinocchio SPL Token ops live-equivalence smoke | just solana-pinocchio-spl-token-ops-live-equivalence | Lean toolchain from lean-toolchain; cargo-build-sbf with Solana rustc/platform-tools; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds the ProofForge SPL Token mint_to/burn/approve/revoke CPI ELF and the checked-in Pinocchio reference ELF, deploys both programs to the same Surfpool instance, invokes the same Web3.js token-ops scenario for each, and compares mint/burn/approve/revoke token effects plus recorded state values | Move live equivalence into CI once Solana rustc is installed reliably; extend Pinocchio comparisons to Token-2022 and remaining SPL helper coverage; just solana-pinocchio-install-sbf-tools repairs missing/corrupted platform-tools | | |
| Solana Pinocchio SPL Token authority live-equivalence smoke | just solana-pinocchio-spl-token-authority-live-equivalence | Lean toolchain from lean-toolchain; cargo-build-sbf with Solana rustc/platform-tools; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds the ProofForge SPL Token set_authority CPI ELF and the checked-in Pinocchio reference ELF, deploys both programs to the same Surfpool instance, invokes the same Web3.js mint-authority transfer scenario for each, and compares mint authority plus recorded state marker | Move live equivalence into CI once Solana rustc is installed reliably; extend Pinocchio comparisons to Token-2022 and remaining SPL helper coverage; just solana-pinocchio-install-sbf-tools repairs missing/corrupted platform-tools | | |
| Solana System create_account CPI Surfpool/Web3.js smoke | just solana-system-create-account-cpi-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated System Program create_account CPI ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes it through @solana/web3.js, verifies the newly created account owner/space/lamports, and verifies the program-owned state account recorded the requested lamports and space | SPL Token CPI behavior, public validator deployment, live Rust/Pinocchio equivalence | | |
| Solana SPL Token transfer_checked CPI Surfpool/Web3.js smoke | just solana-spl-token-transfer-cpi-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated SPL Token transfer_checked CPI ELF, starts Surfpool, deploys with solana program deploy --use-rpc, creates a mint and token accounts through @solana/spl-token, invokes the generated program through @solana/web3.js, verifies source/destination token balances, and verifies the program-owned state account recorded the requested amount | Broader SPL Token/Token-2022 coverage, public validator deployment, live Rust/Pinocchio equivalence | | |
| Solana SPL Token ops CPI Surfpool/Web3.js smoke | just solana-spl-token-ops-cpi-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated SPL Token mint_to/burn/approve/revoke CPI ELF, starts Surfpool, deploys with solana program deploy --use-rpc, creates a mint and token accounts through @solana/spl-token, invokes the generated program through @solana/web3.js, verifies mint supply and token balance changes, verifies delegate allowance then revoke clearing, and verifies the program-owned state account recorded all requested values | Token-2022 extension behavior, public validator deployment | | |
| Solana SPL Token authority CPI Surfpool/Web3.js smoke | just solana-spl-token-authority-cpi-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated SPL Token set_authority CPI ELF, starts Surfpool, deploys with solana program deploy --use-rpc, creates a mint through @solana/spl-token, invokes the generated program through @solana/web3.js, verifies the mint authority moved to the requested new authority, and verifies the program-owned state account recorded the marker | Token-2022 extension behavior, public validator deployment | | |
| Solana log/event Surfpool/Web3.js smoke | just solana-log-event-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated events.emit/Solana log-extension ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies sol_log_64_ transaction logs contain the stable event tag and scalar field value, verifies the program-owned state account recorded the same value, verifies sol_log_pubkey logs the state account’s base58 pubkey, and verifies sol_log_data emits a base64 Program data: payload for state bytes | Anchor-compatible discriminator/Borsh event serialization, indexed events, sol_log_ payloads, historical indexing guarantees | | |
| Solana Clock sysvar Surfpool/Web3.js smoke | just solana-clock-sysvar-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated contextRead checkpointId ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies sol_get_clock_sysvar records Clock.slot into program-owned state, and compares it with transaction slot metadata | Richer Clock fields, public validator deployment | | |
| Solana Rent sysvar Surfpool/Web3.js smoke | just solana-rent-sysvar-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated Solana-only sysvar target-extension ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies sol_get_rent_sysvar records Rent.lamports_per_byte_year into program-owned state, and compares it with the Rent sysvar account data | Additional Rent fields, public validator deployment | | |
| Solana EpochSchedule sysvar Surfpool/Web3.js smoke | just solana-epoch-schedule-sysvar-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated Solana-only sysvar target-extension ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies sol_get_epoch_schedule_sysvar records all five current RPC-exposed EpochSchedule fields into program-owned state, and compares them with RPC getEpochSchedule() | Additional Clock/Rent fields, generic account-passed sysvar reads, public validator deployment | | |
| Solana EpochRewards sysvar Surfpool/Web3.js smoke | just solana-epoch-rewards-sysvar-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated Solana-only sysvar target-extension ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies sol_get_epoch_rewards_sysvar records all current EpochRewards scalar/word-view fields into program-owned state, and compares them with the EpochRewards sysvar account data | Additional Clock/Rent fields, generic account-passed sysvar reads, public validator deployment | | |
| Solana LastRestartSlot sysvar Surfpool/Web3.js smoke | just solana-last-restart-slot-sysvar-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated Solana-only sysvar target-extension ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes the generated program through @solana/web3.js, verifies the feature-gated LastRestartSlot.last_restart_slot read lowered through sol_get_sysvar, and compares the recorded value with the LastRestartSlot sysvar account data | Additional sysvars, public validator deployment, cluster feature-activation variance | | |
| Solana memory syscall Surfpool/Web3.js smoke | just solana-memory-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated runtime.memory ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes set_source plus copy_compare_fill through @solana/web3.js, and verifies program-owned account bytes prove sol_memcpy_, sol_memmove_, sol_memcmp_, and sol_memset_ executed | Broader account/data packing helpers, Rust/Pinocchio equivalence | | |
| Solana return-data/compute Surfpool/Web3.js smoke | just solana-return-data-compute-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated runtime.return_data/runtime.compute_units ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes it through @solana/web3.js, verifies sol_set_return_data through simulation returnData, verifies sol_get_return_data through empty reads and same-instruction set/get roundtrips, verifies sol_remaining_compute_units writes a nonzero state value, and verifies sol_log_compute_units_ emits compute-unit logs | CPI return-value handling, typed return payloads beyond u64, public-validator feature variance | | |
| Solana SHA-256/Keccak-256/Blake3 syscall Surfpool/Web3.js smoke | just solana-crypto-hash-web3 | Lean toolchain from lean-toolchain; surfpool; Solana CLI and solana-keygen; sbpf; Node; npm | Builds a generated Solana-only crypto.hash ELF, starts Surfpool, deploys with solana program deploy --use-rpc, invokes set_preimage, hash_preimage, keccak_preimage, and blake3_preimage through @solana/web3.js, and verifies account-stored digests against Node SHA-256 plus @noble/hashes Keccak-256/Blake3 for the same preimage bytes | Portable Expr.hash routing, Rust/Pinocchio equivalence | | |
| Yul generation smoke | lake env proof-forge --root . -o build/counter.yul Examples/Evm/Contracts/Counter.lean | Built proof-forge | Lean frontend/LCNF lowers a simple contract to Yul | solc acceptance, ABI dispatch, EVM runtime behavior | | |
| Yul-to-bytecode smoke | solc --strict-assembly build/counter.yul --bin | solc on PATH | Generated Yul is accepted by solc | Runtime semantics or method dispatch | | |
| Single EVM bytecode compile | lake env proof-forge --evm-bytecode --root . --module contract --artifact-output build/evm/Counter.proof-forge-artifact.json -o build/evm/Counter.bin Examples/Evm/Contracts/Counter.lean | solc, cast, python3, and Examples/Evm/Contracts/Counter.evm-methods | Lean -> Yul -> solc -> runtime bytecode with selector generation, deployable .init.bin creation bytecode, proof-forge-artifact.json metadata, and a proof-forge-deploy.json initcode manifest whose header copies and returns the referenced runtime bytecode; --evm-chain-profile <id> additionally records a known EVM chain profile in the deploy manifest without broadcasting; --evm-constructor-param <name:type> records static-word constructor ABI schema; --evm-constructor-arg <name=value> ABI-encodes supported static-word typed values; --evm-constructor-args-hex <hex> records and appends an ABI-encoded constructor-argument tail | Runtime behavior, gas, exhaustive ABI correctness, dynamic constructor ABI types, signed/raw transaction generation, real transaction broadcast | | |
| EVM examples compile | scripts/evm/build-examples.sh | cast, solc, python3, lake env proof-forge; optional PROOF_FORGE_BIN, CONTRACTS_DIR, EVM_OUT_DIR | Every .lean contract with a sibling .evm-methods compiles to reproducible Yul, .bin, and .init.bin, diffs generated Yul against the tracked SDK example golden fixtures, and validates EVM metadata hashes, initcode hashes/header/runtime linkage, deploy-manifest hashes, source/module info, solc info, SDK method selectors/functions, and required Solidity method signatures | Runtime behavior; contracts without .evm-methods are skipped by the script | | |
| Learn token ERC-20 VM smoke | just learn-token-evm-vm | Lean toolchain from lean-toolchain; solc; Node; npm | Parses Examples/Learn/ProofToken.learn, emits ERC-20 Yul/creation bytecode/artifact metadata through proof-forge --learn-token --target evm, deploys the generated creation bytecode in an EthereumJS VM, then verifies totalSupply, decimals, balanceOf, transfer, approve, allowance, transferFrom, optional burn, optional mint, Transfer/Approval topics, and insufficient-balance revert behavior | Live RPC deployment, gas accounting, wallet UX, stronger mint access-control policy | | |
| EVM runtime smoke | scripts/evm/foundry-smoke.sh | forge, cast, solc; optional EVM_OUT_DIR, EVM_FORGE_DIR | Foundry executes generated runtime bytecode for Counter, ArrayExample, SimpleToken, and VerifiedVault, executes the generated Counter .init.bin through EVM create, and includes revert checks | Formal proof coverage, cross-target equivalence, live RPC deployment, exhaustive edge coverage | | |
| EVM Anvil deploy smoke | scripts/evm/anvil-deploy-smoke.sh | anvil, cast, solc, python3; optional EVM_ANVIL_CHAIN_ID, EVM_ANVIL_CHAIN_PROFILE, EVM_ANVIL_PORT, EVM_ANVIL_RUN_DIR, EVM_ANVIL_CONSTRUCTOR_ARG, EVM_ANVIL_CONSTRUCTOR_ARGS_HEX, EVM_ANVIL_CONSTRUCTOR_PARAM | Starts a local Anvil chain, regenerates Counter initcode with deterministic typed initial=123 constructor input, initial:uint256 constructor ABI schema, and the anvil-local chain profile by default for chain id 31337, validates signature-bearing Counter method metadata and profile-aware deploy metadata, deploys generated Counter .init.bin through cast send --create, records constructor ABI schema, constructor args, creation receipt, creation transaction JSON, chain profile, and deployed address in Counter.proof-forge-deploy-run.json, validates that the creation transaction input equals the generated initcode, validates that the profile chain id matches the actual local chain, validates that the deployed runtime code equals Counter.bin, runs Counter get/set/increment/decrement through JSON-RPC, and validates the deploy-run artifact with scripts/evm/validate-deploy-run.py | Live public RPC deployment, explorer verification, wallet UX, dynamic constructor ABI types, long-running chain state | | |
| EVM ABI ScalarProbe IR smoke | scripts/evm/abi-scalar-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR U64, U32, and Bool ABI parameters lower to Yul function parameters and dispatcher calldata loads, match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including selector entrypoints and Yul/bytecode hashes, validate a chain-profile-aware deploy manifest for robinhood-chain-testnet with chain id 46630, return expected values through Foundry calls, and reject short calldata, out-of-range uint32, and invalid bool encodings | Aggregate ABI parameters/returns, storage behavior, live RPC deployment | | |
| EVM AssertProbe IR smoke | scripts/evm/assert-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR assert and assert_eq statements lower to Yul revert guards, match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including assertions.check, return the expected value through Foundry calls, and revert when the assertion fails | Rich revert data, expression type checking | | |
| EVM AssignmentProbe IR smoke | scripts/evm/assignment-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR mutable scalar locals and local assignment lower to Yul let declarations and := assignments, match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including selector entrypoints and artifact hashes, return the assigned value through Foundry calls, and revert when the assigned bool guard is false | Aggregate assignment paths, storage path assignment paths | | |
| EVM AssignOpProbe IR smoke | scripts/evm/assign-op-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR compound assignment lowers for mutable U32/U64 locals and U64 scalar storage, matches the golden Yul fixture, compiles to runtime bytecode with solc --strict-assembly, validates EVM metadata including storage.scalar, returns expected U64/U32 values through Foundry calls, verifies raw scalar storage with vm.load, and rejects unknown selectors | Aggregate assignment targets, checked overflow semantics beyond raw EVM word operations | | |
| EVM ConditionalProbe IR smoke | scripts/evm/conditional-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR statement-level if/else lowers to Yul switch blocks, matches the golden Yul fixture, compiles to runtime bytecode with solc --strict-assembly, validates EVM metadata including storage.scalar, control.conditional, assertions.check, returns the expected then/else storage result through Foundry calls, and rejects unknown selectors; branch-local early returns are covered by EvmLoopProbe | Richer control-flow analysis | | |
| EVM LoopProbe IR smoke | scripts/evm/loop-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR boundedFor lowers to Yul for loops with static bounds, branch-local and loop-local early returns lower to return-value assignments followed by Yul leave, generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes storage.scalar, control.conditional, and control.bounded_loop, Foundry validates loop-updated storage, raw storage slots, early-return values/effects, and unknown-selector reverts | Dynamic loop bounds, break/continue, richer control-flow analysis | | |
| EVM ContextProbe IR smoke | scripts/evm/context-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR context reads lower to Yul caller(), address(), and number(), nativeValue lowers to Yul callvalue(), match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including caller.sender, account.explicit, env.block, value.native, return expected Foundry vm.prank/vm.roll context values, return expected value from probe.call{value: ...}, and reject unknown selectors | Context fields beyond the current portable userId/contractId/checkpointId set, typed address-width validation | | |
| EVM EventProbe IR smoke | scripts/evm/event-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR eventEmit lowers to Yul log1 and eventEmitIndexed lowers to Yul log2/log3/log4, with topic0 = keccak256(Solidity-style event signature), U64/Bool/U32/Hash indexed scalar fields in topics, U64/Bool/U32/Hash scalar non-indexed fields in 32-byte word data, flat struct / scalar fixed-array / fixed-array-of-flat-struct non-indexed fields flattened into ABI-style data words from local values and storage reads, and supported aggregate indexed fields hashed into topics with keccak256 over flattened ABI-style words; generated Yul matches the golden fixture, compiles to runtime bytecode with solc --strict-assembly, validates EVM metadata including events.emit plus abi.events signatures, topic0, indexed/data fields, flattened word types, and topic/data encodings, verifies Foundry recorded logs for emitter/topic/data including TypedScalarEvent(bool,uint32,bytes32), PairEvent((uint64,uint64)), StoragePairEvent((uint64,uint64)), StorageArrayEvent(uint64[2]), ArrayEvent(uint64[2]), PairArrayEvent((uint64,uint64)[2]), StoragePairArrayEvent((uint64,uint64)[2]), IndexedTypedScalar(bool,uint32,bytes32,uint64), IndexedPair((uint64,uint64),uint64), IndexedStoragePair((uint64,uint64),uint64), IndexedTwoValues(uint64,uint64,uint64), IndexedThreeValues(uint64,uint64,uint64,uint64), IndexedStorageArray(uint64[2],uint64), IndexedArray(uint64[2],uint64), IndexedStoragePairArray((uint64,uint64)[2],uint64), and IndexedPairArray((uint64,uint64)[2],uint64), rejects malformed Bool/U32 calldata, and rejects unknown selectors | Richer event declarations, unsupported nested aggregate indexed shapes, indexed fields beyond 3 topics | | |
| EVM CrosscallProbe IR smoke | scripts/evm/crosscall-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR crosscallInvoke, crosscallInvokeTyped, crosscallInvokeValueTyped, crosscallInvokeStaticTyped, crosscallInvokeDelegateTyped, crosscallCreate, and crosscallCreate2 lower to arity-, return-type-, value-mode-, static-mode-, delegate-mode-, and creation-specific Yul helpers that pack selector/scalar-word, flat aggregate, and nested fixed-array arguments whose leaves are scalar words or flat structs, execute synchronous EVM call, staticcall, delegatecall, create, or create2, optionally forward U64 call value, revert on failed calls, too-short return data, or zero-address creation results, decode scalar and direct entrypoint aggregate return words, guard Bool/U32 return ranges across scalar and aggregate returns, match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including crosscall.invoke and all CrosscallProbe entrypoints, and verify Foundry U64 zero/one/two-argument calls, Bool/U32/Hash typed calls, flat struct/scalar fixed-array/fixed-array-of-flat-struct/nested fixed-array typed-call arguments with scalar or flat-struct leaves, flat struct/scalar fixed-array/fixed-array-of-flat-struct/nested fixed-array aggregate typed returns with scalar or flat-struct leaves in normal/value/static/delegate modes, aggregate Bool/U32 malformed-return guards in normal/value/static/delegate modes, native-value forwarding to a payable callee, value-bearing flat and nested scalar/flat-struct aggregate arguments, U64 read-only staticcall return behavior, Bool/U32/Hash static typed returns, static flat and nested scalar/flat-struct aggregate arguments, invalid static Bool/U32 return guards, static-context state-write failure, caller-storage delegatecall read/write behavior, Bool/U32/Hash delegate typed returns, delegate flat and nested scalar/flat-struct aggregate arguments, invalid delegate Bool/U32 return guards, fixed init-code create deployment, deterministic create2 address validation, deployed-runtime calls, invalid typed returns, and revert paths | Artifact-linked creation code, dynamic constructor arguments, non-flat nested aggregate leaves, variable-length return data | | |
| EVM ExpressionProbe IR smoke | scripts/evm/expression-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR scalar expressions lower directly to Yul for U64/U32 arithmetic, U64 exponentiation, U64/U32 bitwise operations and shifts, predicates, boolean operators, scalar literals, immutable local reads, supported casts, one-word returns, and assertion guards; generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes assertions.check, and Foundry validates runtime return values, U32/Bool calldata guards, malformed calldata reverts, and unknown-selector revert | Checked overflow semantics beyond raw EVM word operations, aggregate expressions covered by array/struct/ABI probes | | |
| EVM HashProbe IR smoke | scripts/evm/hash-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR Hash values lower to one-word EVM bytes32 ABI/storage values, hash4 and hashValue pack four limbs into one word, hash and hash_two_to_one lower to Yul keccak256 helpers, the generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes crypto.hash and storage.scalar, Foundry verifies ABI bytes32 parameters/returns plus raw scalar storage slots, and unknown selectors revert | Aggregate hashing inputs, typed address-width validation | | |
| EVM MapProbe IR smoke | scripts/evm/map-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR Map<U64, U64, N> storage lowers through Solidity-style keccak256(key, slot) value mapping slots plus ProofForge-managed presence slots for contains, matches the golden Yul fixture, compiles to runtime bytecode with solc --strict-assembly, validates EVM metadata including storage.scalar, storage.map, assertions.check, returns expected get/set/insert/contains values through Foundry calls, validates zero-valued present keys, validates single-segment and nested consecutive mapKey storage path reads, writes, and compound assignment, verifies raw value and presence slots with vm.load, and rejects unknown selectors | Typed word maps covered by EvmTypedMapProbe, array/struct storage paths, mixed map/aggregate storage paths | | |
| EVM TypedMapProbe IR smoke | scripts/evm/typed-map-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR Map<K, V, N> storage lowers for word key/value types (U32, Bool, Hash, and the existing U64) through Solidity-style keccak256(key, slot) value mapping slots plus ProofForge-managed presence slots for contains; generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes storage.scalar, storage.map, and assertions.check, Foundry validates U32/Bool/Hash map reads and writes, typed contains, previous-value returns, raw value and presence mapping slots, U32/Bool calldata guards, single-segment mapKey storage-path reads/writes, U32 map-path compound assignment, U32 nested mapKey path read/write/compound assignment with dispatcher range guards, and unknown-selector revert | Non-word or aggregate map key/value shapes, mixed map/aggregate storage paths | | |
| EVM StorageArrayProbe IR smoke | scripts/evm/storage-array-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR U64 fixed storage arrays lower to contiguous EVM storage slots with runtime index bounds checks, single-segment index storage paths lower to the same slot helper for read/write/compound assignment, fixed-array ABI returns can be assembled from storage element reads, match the golden Yul fixture, compile to runtime bytecode with solc --strict-assembly, validate EVM metadata including storage.scalar, storage.array, data.fixed_array, return expected lifecycle/read/write/path/aggregate values through Foundry calls, verify raw slot layout with vm.load, and reject out-of-bounds indexes and unknown selectors | U32/Bool/Hash storage arrays covered by EvmTypedStorageProbe, local fixed-array values and broader aggregate ABI behavior covered by EvmAbiAggregateProbe, nested index storage paths, structs | | |
| EVM TypedStorageProbe IR smoke | scripts/evm/typed-storage-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR Bool scalar storage and U32/Bool/Hash fixed storage arrays lower to contiguous EVM word slots with runtime index bounds checks, generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes storage.scalar, storage.array, data.fixed_array, and assertions.check, Foundry validates raw slot layout, ABI Bool/Hash returns, U32 calldata range guards, typed storage-path reads/writes, U32 storage-path compound assignment, out-of-bounds reverts, and unknown selectors | Non-word storage elements, nested index storage paths, struct arrays covered by EvmStorageStructProbe, typed maps covered by EvmTypedMapProbe | | |
| EVM StorageStructProbe IR smoke | scripts/evm/storage-struct-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR flat scalar storage structs lower to one EVM slot per field, whole scalar storage struct reads/writes expand over those field slots with RHS snapshotting for writes, fixed storage arrays of flat structs lower to contiguous field-expanded slots with runtime index bounds checks, scalar field and array index+field storage paths lower to the same slot formula for read/write/compound assignment, fixed-array-of-flat-struct ABI returns can be assembled from storage field reads, generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes storage.scalar, storage.array, data.fixed_array, and data.struct, Foundry validates U64/Bool/U32/Hash field behavior, whole storage struct read/write, ABI struct returns from storage, fixed-array-of-struct returns from storage, raw slot layout, out-of-bounds reverts, and unknown selectors | Nested struct fields, non-flat struct storage | | |
| EVM ArrayValueProbe IR smoke | scripts/evm/array-value-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR immutable and mutable local fixed-array values lower to per-element Yul locals, fixed-array literals plus static/dynamic index reads lower deterministically, static/dynamic local element assignment and numeric compound assignment update the expanded local, static and dynamic nested scalar local fixed-array reads lower through deterministic leaf locals and nested getter helpers, static and dynamic nested scalar leaf assignment/compound assignment lower through direct assignments or nested switch blocks, whole-local and whole-nested fixed-array assignment snapshots RHS elements before writing back, generated Yul matches the golden fixture, runtime bytecode compiles with solc --strict-assembly, EVM metadata includes data.fixed_array and assertions.check, Foundry returns expected U64/U32/Bool/Hash values, validates mutable element writes, validates nested dynamic read/write out-of-bounds reverts, and rejects unknown selectors | ABI aggregate behavior covered by EvmAbiAggregateProbe, nested arrays with non-scalar leaves | | |
| EVM StructArrayValueProbe IR smoke | scripts/evm/struct-array-value-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR local fixed arrays of flat structs lower to one Yul local per element field, field(arrayGet(localArray, index), name) supports static and dynamic field reads, mutable struct-array field assignment and numeric compound assignment update the expanded locals through static assignments or dynamic switch blocks, whole local assignment from another local struct array or a struct-array literal snapshots RHS fields before writing target fields, generated Yul matches the golden fixture, runtime bytecode compiles with solc --strict-assembly, EVM metadata includes data.fixed_array, data.struct, and assertions.check, Foundry returns expected U64/U32/Bool/Hash-backed values, validates self-referential RHS snapshot behavior, rejects dynamic out-of-bounds indexes, and rejects unknown selectors | Nested arrays, nested structs, aggregate ABI behavior covered by EvmAbiAggregateProbe | | |
| EVM StructValueProbe IR smoke | scripts/evm/struct-value-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR flat immutable and mutable local struct values lower to per-field Yul locals, struct literals and field access lower deterministically for U64/U32/Bool/Hash fields, static local field assignment and numeric compound assignment update the expanded local, whole-local struct assignment snapshots RHS fields before writing back, generated Yul matches the golden fixture, runtime bytecode compiles with solc --strict-assembly, EVM metadata includes data.struct and assertions.check, Foundry returns expected U64/U32/Bool/Hash values, validates mutable field writes, and rejects unknown selectors | Nested structs, storage struct behavior covered by EvmStorageStructProbe, ABI aggregate behavior covered by EvmAbiAggregateProbe, struct arrays | | |
| EVM AbiAggregateProbe IR smoke | scripts/evm/abi-aggregate-ir-smoke.sh | forge, solc, python3, Lean toolchain from lean-toolchain | Portable IR flat static struct, fixed-array, and nested scalar fixed-array ABI parameters flatten to contiguous calldata words, fixed arrays of flat structs flatten as tuple-array ABI words, U32 and Bool aggregate words get dispatcher range guards, Hash aggregate leaves lower as Solidity bytes32 words inside flat structs and fixed arrays, flat struct/fixed-array returns including nested scalar fixed arrays, fixed arrays of flat structs, HashPair structs, and Hash fixed arrays encode as multi-word ABI return data, generated Yul matches the golden fixture, bytecode compiles with solc --strict-assembly, metadata includes data.fixed_array, data.struct, and structured abi.entrypoints selector signatures plus calldata/return word layouts checked with cast sig and --expect-entrypoint-abi, Foundry validates aggregate calls/returns, malformed calldata reverts including short bytes32[2] calldata, and unknown selectors revert | Dynamic aggregate ABI values, storage-backed aggregate ABI returns beyond the fixed word-array and flat struct-array cases covered by EvmStorageArrayProbe and EvmStorageStructProbe, rich ABI tuples beyond flat word aggregates; typed crosscall aggregate behavior is covered by EvmCrosscallProbe | | |
| EVM diagnostic smoke | scripts/evm/diagnostic-smoke.sh | Lean toolchain from lean-toolchain | Unsupported or malformed EVM IR shapes fail before Yul generation with explicit diagnostics for missing selectors, unsupported ABI values such as Unit/zero-length arrays and non-flat struct fields, missing returns on incomplete control-flow paths, Hash/U64 type mismatches, unsupported array/struct/event surfaces, invalid bounded-loop ranges, malformed crosscall target/method/argument types, unsupported typed crosscall nested fixed-array non-flat struct leaves in arguments/returns, malformed value-bearing crosscall call value/return types and unsupported nested fixed-array non-flat struct leaves, unsupported static/delegate nested fixed-array non-flat struct leaves, malformed create/create2 value, salt, and init-code hex, unsupported map shapes, statement-position contains, malformed assignment/compound-assignment types and targets, storage-path compound assignment expression/nested-path misuse, and expression/statement effect misuse including statement-position context reads. It also checks EVM constructor CLI diagnostics for unsupported dynamic ABI types, missing or duplicate typed values, mixed typed/raw constructor argument sources, integer overflow, and malformed static-word values such as short addresses. | Exhaustive unsupported-surface coverage, solc behavior, Foundry runtime behavior, artifact metadata | | |
| EVM IR coverage manifest | scripts/evm/check-ir-coverage-manifest.py | python3 | Tests/EvmCoverage.tsv has one status/evidence row for every portable IR constructor in ProofForge/IR/Contract.lean, so new IR nodes cannot be added without recording whether EVM lowers, validates, or rejects them | Behavioral correctness, solc behavior, Foundry runtime behavior, artifact generation | | |
| Psy Counter IR smoke | scripts/psy/counter-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Counter portable IR lowers to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON with dargo compile, returns result_vm: [2] through dargo execute, emits non-empty ABI JSON, writes proof-forge-deploy.json, records it in proof-forge-artifact.json, and validates metadata/deploy-manifest hashes/capabilities/results | Upstream compressed genesis deploy JSON, live Psy node/prover behavior, broader IR coverage | | |
| Psy ExpressionPredicateProbe IR smoke | scripts/psy/expression-predicate-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers equality, inequality, ordering comparisons, boolean not/and/or, and assertion predicates to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [16] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Statement-level control flow, division/modulo/exponentiation, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy GenericEntrypointProbe IR smoke | scripts/psy/generic-entrypoint-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | A valid non-whitelisted Psy IR module lowers through the generic generated test fallback instead of a fixture-specific testBody branch, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [42] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Fixture-specific semantic assertions, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy ArithmeticProbe IR smoke | scripts/psy/arithmetic-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers subtraction, multiplication, and nested arithmetic precedence to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [60] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Division, modulo, exponentiation, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy U32ArithmeticProbe IR smoke | scripts/psy/u32-arithmetic-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers u32 ABI parameters, Nu32 literals, +, -, *, /, %, **, mutable assignment, arithmetic compound assignments, u32 as bool, and bool as Felt casts to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [1] through dargo execute --parameters 2,3, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | U32 storage behavior, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy BitwiseProbe IR smoke | scripts/psy/bitwise-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers Felt and u32 bitwise &, ` | , ^, <<, and >>expressions plus | =, &=, ^=, <<=, and >>=compound assignments to.psy, matches the golden fixture, passes dargo test —file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [16]throughdargo execute, writes proof-forge-deploy.jsonandproof-forge-artifact.json`, and validates deploy-manifest/metadata hashes/capabilities/results | u32 storage probes, upstream compressed genesis deploy JSON, live Psy node/prover behavior |
| Psy U32HashPackingProbe IR smoke | scripts/psy/u32-hash-packing-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers [u32; 8] literal limbs, U32 ABI parameters, casts to Felt, and dynamic Hash value construction to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns deterministic four-Felt Hash outputs for pack_literal and pack_params, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Storage-specific U32 behavior, map storage paths, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy U32StorageScalarProbe IR smoke | scripts/psy/u32-storage-scalar-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers native u32 scalar storage read/write and scalar += assignment to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [12] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Wider U32 storage assignment matrix, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy BoolStorageScalarProbe IR smoke | scripts/psy/bool-storage-scalar-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers native bool scalar storage read/write and bool as Felt return casts to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [1] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy BoolStorageArrayProbe IR smoke | scripts/psy/bool-storage-array-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers [bool; N] fixed-array literals/indexes, native bool storage arrays, indexed storage read/write, generic storage-path read/write, and bool as Felt casts to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [2] for both local_flags_sum and storage_lifecycle through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy U32StorageArrayProbe IR smoke | scripts/psy/u32-storage-array-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers portable U32 storage arrays to Felt-backed Psy storage arrays with explicit u32 as Felt writes, .get() as u32 reads, and storage-path compound assignments rewritten as typed read/update/write casts, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [28] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Direct native [u32; N] Psy contract storage arrays, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy ConditionalProbe IR smoke | scripts/psy/conditional-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers statement-level if/else branches with Bool conditions, branch-local bindings, scalar storage reads/writes, assertions, and returns to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [10] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Else-if sugar, conditionals that are the sole return terminator, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy ContextProbe IR smoke | scripts/psy/context-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Non-Counter Psy IR lowers parameters and context reads to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [15] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Maps, arrays, hashes, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy EventProbe IR smoke | scripts/psy/event-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers eventEmit to __emit([fields]) with an event-name comment, matches the golden fixture, passes dargo test --file, emits a PsyUserEventRecord with data: [42], produces non-empty DPN JSON and ABI JSON, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Event struct definitions, multi-field events, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy CrosscallProbe IR smoke | scripts/psy/crosscall-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers crosscallInvoke to __invoke_sync#<Felt>(target, method_id, [args]), matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Actual cross-contract execution (Psy 0.1.0 panics on the unimplemented cross-contract circuit gadget), upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy HashProbe IR smoke | scripts/psy/hash-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers Hash, typed hash let-bindings, hash, and hash_two_to_one to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns the expected four-Felt hash outputs through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Maps, storage maps, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy HashStorageProbe IR smoke | scripts/psy/hash-storage-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers native scalar Hash storage, native [Hash; N] storage arrays, indexed storage read/write, and generic storage-path read/write to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [5, 6, 7, 8] and result_vm: [55, 66, 77, 88] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy MapProbe IR smoke | scripts/psy/map-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers fixed-capacity Map<Hash, Hash, N> storage, contains/get/insert/set effects, expression-position set return values, and generic map storage paths to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [55, 66, 77, 88], result_vm: [77, 88, 99, 111], result_vm: [31, 32, 33, 34], and result_vm: [5, 6, 7, 8] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Bounded loops, arrays, structs, assertions, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy AssertProbe IR smoke | scripts/psy/assert-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers statement-level assert and assert_eq into generated method bodies, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [12] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Bounded loops, arrays, structs, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy LoopProbe IR smoke | scripts/psy/loop-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers static bounded for loops into generated method bodies, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [3] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Arrays, structs, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy ArrayProbe IR smoke | scripts/psy/array-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers fixed-array value types, array literals, index reads, fixed-array equality/inequality/assert_eq, and fixed storage array index read/write effects to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [60], result_vm: [31], and result_vm: [1] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Struct arrays, nested arrays, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy StructProbe IR smoke | scripts/psy/struct-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers struct declarations, struct literals, field access, scalar storage struct assignment, and scalar storage struct field read/write effects to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [30] and result_vm: [26] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Struct arrays, nested structs, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy StructArrayProbe IR smoke | scripts/psy/struct-array-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers fixed arrays of structs, storage arrays of structs, whole struct element writes, and indexed struct field read/write effects to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [100] and result_vm: [102] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Deeply nested mixed aggregate updates, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy AbiAggregateProbe IR smoke | scripts/psy/abi-aggregate-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers ABI-facing struct parameters, fixed-array parameters, and struct returns to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [15], result_vm: [6], and result_vm: [9, 4] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Deeply nested mixed aggregate updates, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy NestedAggregateProbe IR smoke | scripts/psy/nested-aggregate-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers mutable local aggregate bindings and nested assignment paths such as families[1].children[0].age = 31, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [51] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Storage-backed nested aggregate updates, upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy StorageNestedAggregateProbe IR smoke | scripts/psy/storage-nested-aggregate-smoke.sh | dargo on PATH; python3; psyup install 0.1.0 is known-good on macOS arm64 | Psy IR lowers generic storage paths across scalar storage structs, nested #[ref] fields, storage arrays, scalar storage compound assignment, storage-path compound assignment, and native U32 storage struct field paths to .psy, matches the golden fixture, passes dargo test --file, produces non-empty DPN JSON and ABI JSON, returns result_vm: [252] through dargo execute, writes proof-forge-deploy.json and proof-forge-artifact.json, and validates deploy-manifest/metadata hashes/capabilities/results | Upstream compressed genesis deploy JSON, live Psy node/prover behavior | | |
| Psy diagnostic smoke | scripts/psy/diagnostic-smoke.sh | Lean toolchain from lean-toolchain | Unsupported or malformed Psy IR shapes fail before source generation with explicit diagnostics for invalid Psy identifiers, duplicate declarations, reserved local names, empty contract state, Unit parameters, zero-length ABI arrays, unknown ABI structs, unsupported map shapes, unsupported Unit storage arrays, non-storage structs, empty structs, invalid bounded loops, effect expression/statement misuse, invalid assignment targets, invalid storage paths, expression/body type mismatches, immutable assignment, missing returns, malformed equality, malformed comparison, malformed Hash value construction, malformed arithmetic, unsupported casts, malformed bitwise/shift expressions, malformed compound assignment statements, malformed storage compound assignment effects, malformed boolean operators, malformed if conditions, and branch-local escape | Exhaustive unsupported-surface coverage, Dargo behavior, ProofForge deploy manifests, upstream compressed genesis deploy JSON | | |
| Psy IR coverage manifest | scripts/psy/check-ir-coverage-manifest.py | python3 | Tests/PsyCoverage.tsv has one status/evidence row for every portable IR constructor in ProofForge/IR/Contract.lean, so new IR nodes cannot be added without recording whether Psy lowers, validates, or rejects them | Behavioral correctness, Dargo behavior, artifact generation | | |
| CI baseline | .github/workflows/ci.yml build-test job | GitHub Actions Ubuntu, just 1.48.0, elan, Foundry stable, solc 0.8.30 | Clean-environment just build, just target-registry, just evm-plan, just solana-light, just docs-check, Wasm-NEAR diagnostic smoke, Wasm-NEAR/EmitWat IR coverage manifests, IR ownership rules, Wasm-NEAR formal semantics anchors, EmitWat offline host smoke, just psy-golden-sources, Psy diagnostic smoke, Psy IR coverage manifest, EVM diagnostic smoke, EVM IR coverage manifest, EVM ABI scalar IR smoke, EVM AssertProbe IR smoke, EVM AssignmentProbe IR smoke, EVM AssignOpProbe IR smoke, EVM ConditionalProbe IR smoke, EVM LoopProbe IR smoke, EVM ContextProbe IR smoke, EVM EventProbe IR smoke, EVM CrosscallProbe IR smoke, EVM ExpressionProbe IR smoke, EVM HashProbe IR smoke, EVM MapProbe IR smoke, EVM TypedMapProbe IR smoke, EVM StorageArrayProbe IR smoke, EVM StorageStructProbe IR smoke, EVM TypedStorageProbe IR smoke, EVM ArrayValueProbe IR smoke, EVM StructArrayValueProbe IR smoke, EVM StructValueProbe IR smoke, EVM AbiAggregateProbe IR smoke, EVM metadata/deploy-manifest validation, EVM compile, Foundry smoke, and Anvil deploy smoke. CI keeps separate GitHub Actions steps for failure localization, but each common gate is invoked through the root justfile recipe. | Optional Dargo target smokes, non-Ubuntu behavior | | |
| Aleo Counter IR smoke | scripts/aleo/counter-smoke.sh | leo CLI (4.0.2 tested) on PATH; python3; Lean toolchain from lean-toolchain | Portable IR Counter lowers to a Leo 4.0 program with @noupgrade constructor and fn ... -> Final entry points, matches Examples/Aleo/Counter.golden.leo, leo build produces main.aleo and abi.json, leo test passes, and proof-forge-artifact.json schema validation passes | Private records, transitions, proofs, direct Aleo Instructions, devnet deployment, cross-target equivalence, standalone .avm file | | |
| Aleo PureMath IR smoke | scripts/aleo/pure-math-smoke.sh | leo CLI (4.0.2 tested) on PATH; python3; Lean toolchain from lean-toolchain | Portable IR pure functions with params, if/else, boundedFor, assign, assignOp, and assert lower to a Leo 4.0 program, match Examples/Aleo/PureMath.golden.leo, leo build produces main.aleo and abi.json, leo test passes, and proof-forge-artifact.json schema validation passes | Stateful parameterized entrypoints, non-local assignment targets, dynamic loop bounds, standalone .avm file | | |
