> ## Documentation Index > Fetch the complete documentation index at: https://gradiences.mintlify.site/llms.txt > Use this file to discover all available pages before exploring further. # Validation Gates > This page documents the runnable gates that validate ProofForge today and This page documents the runnable gates that validate ProofForge today and separates them from gates that are planned but not yet implemented. It mirrors actual scripts, root `justfile` recipes, and `.github/workflows/ci.yml`; it does not add or edit CI jobs. ## Current gates | Gate | Command | Prerequisites | What it proves | What it does not prove | | | | ------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ | ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | ------------------------------------------------------------------------------------------ | | 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]`through`dargo execute`, writes `proof-forge-deploy.json`and`proof-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 | | | ## Planned gates that are not runnable yet The following gates are `Planned` and do not exist in CI or as scripts: * `proof-forge build --target ` — unified target-oriented build command. * `proof-forge test --target ` — unified target-oriented test command. * Non-EVM, non-Psy `proof-forge-artifact.json` validation — artifact metadata schema validation for targets that do not yet write metadata. * Golden Yul/output snapshots — regression detection via snapshot diffing. * CosmWasm smoke — `cosmwasm-check` or `cw-multi-test` validation. * Solana sBPF assembly gates (target `solana-sbpf-asm`, D-026). These become runnable as Workstreams 6–7 land; the `sbpf` toolchain is validated locally (build + disassemble round-trip + `sbpf test` on the counter example): * **V-GATE-SOLANA-01** — `--emit-sbpf-asm` produces valid `.s` accepted by `sbpf build` (no assembly errors). Script: `scripts/solana/emit-asm-smoke.sh` (runnable, Phase 0 complete). * **V-GATE-SOLANA-02** — `sbpf build` produces a valid ELF that `sbpf disassemble` round-trips. Script: `scripts/solana/emit-asm-smoke.sh` (runnable, Phase 0 complete). * **V-GATE-SOLANA-03** — Counter scenario (initialize, increment, get) passes `sbpf test` (Mollusk). Script: `scripts/solana/counter-smoke.sh` (Phase 1 complete; 4 Mollusk assertions: initialize→0, increment 0→1, increment 5→6, get→return\_data). The emitted `.s` now includes the account-validation prologue (writable + owner checks) and is accompanied by `manifest.toml`; the tracked `Examples/Solana/Counter.golden.s` / `Counter.manifest.toml` are kept in sync by `scripts/solana/build-examples.sh`. * **V-GATE-SOLANA-04** — Counter scenario passes a Surfpool local simnet deployment and Web3.js behavior smoke. Script: `scripts/solana/surfpool-web3-smoke.sh` (optional, gated on `surfpool`, Solana CLI, `sbpf`, Node, and npm). The script builds the Counter ELF, starts Surfpool, deploys with `solana program deploy --use-rpc`, creates a program-owned counter account through `@solana/web3.js`, invokes initialize/increment/get, validates account data 0→1→2, and checks `get` return data. * **V-GATE-SOLANA-05** — Capability checker rejects IR modules using unsupported capabilities with a clear diagnostic citing target id and capability id. Script: `scripts/solana/diagnostic-smoke.sh` runs `Tests/SolanaDiagnostics.lean` and asserts 8 crosscall rejection cases (the generic `crosscall.invoke` family) all produce the expected message `target \`solana-sbpf-asm\` does not support capability \`crosscall.invoke\`: ...\`. (Phase 1 complete.) * **V-GATE-SOLANA-06** — `proof-forge-artifact.json` includes `target: "solana-sbpf-asm"`, `irVersion`, and entrypoint list. * **V-GATE-SOLANA-07** — `sbpf debug --elf --input` works interactively (developer ergonomics gate — not CI). * **V-GATE-SOLANA-08** — Control-flow + assertion IR coverage. Two halves: * Emission half (runnable, no `sbpf` required) — `scripts/solana/emit-control-smoke.sh` runs `--emit-control-ir-sbpf`, greps the emitted `.s` for the `control.conditional` / `control.assert` / `control.assert_eq` markers, the `assert_fail` (exit 2) and `assert_eq_fail` (exit 3) global labels, the dispatch lines for the three entrypoints, the comparison instructions `jeq`/`jlt` driving `r3` vs `r2`, asserts the asm is bit-for-bit reproducible across re-emissions, and validates the artifact metadata records `target: "solana-sbpf-asm"`, `fixture: "control-ir-sbpf"`, `sourceModule: "ControlFlowAssertProbe"`, and the `storage.scalar` / `control.conditional` / `assertions.check` / `account.explicit` capabilities. (Emission half complete.) * Runtime half (gated on `sbpf` + `cargo` + `solana-keygen`) — `scripts/solana/control-smoke.sh` assembles the emitted `.s` via `sbpf build` and runs the Mollusk test crate rendered from `Tests/solana/control_mollusk.rs.tpl`. Six Mollusk checks cover `lifecycle` from a zero and from a large pre-state (both land on 10u64 and return 10), `guarded_increment` from 3 (assert passes, count→4) and from 9 (assert reverts via `assert_fail` exit 2), and `equality_guard` from 7 (assertEq passes, count→7 and return 7) and from 42 (assertEq reverts via `assert_eq_fail` exit 3). The Mollusk fixtures disable `account_data_direct_mapping` / `direct_account_pointers_in_program_input` / `virtual_address_space_adjustments` so the Phase 1 lowering's legacy embedded account-data layout is exercised. (Phase 1 complete.) * **V-GATE-SOLANA-09** — PDA typed seed descriptor compatibility with Solana Web3.js. Script: `scripts/solana/pda-web3-smoke.sh` emits the SDK Vault artifact, installs `@solana/web3.js` in an isolated temp project, reads `solanaExtensions.pdas[].typedSeeds`, and checks that literal/account/bump descriptors reproduce the same PDA through `PublicKey.findProgramAddressSync` and `PublicKey.createProgramAddressSync`. The harness also covers UTF-8 and instruction-parameter seed resolver behavior. This is an offline derivation gate; it does not deploy or execute a transaction. * **V-GATE-SOLANA-10** — System Program transfer CPI live behavior through Surfpool and Web3.js. Script: `scripts/solana/system-cpi-web3-smoke.sh` builds the generated `--solana-system-cpi-elf` fixture, validates its artifact schema, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes the generated transfer entrypoint with a standard `@solana/web3.js` transaction, and checks both the recipient lamport delta and the program-owned state account's recorded lamports value. * **V-GATE-SOLANA-10R** — System Program transfer Pinocchio reference-equivalence contract. Script: `scripts/solana/pinocchio-system-transfer-equivalence.sh` emits the same `--solana-system-cpi-elf` fixture and compares its generated artifact against `references/solana/pinocchio/system-transfer/reference-manifest.json` plus source constants. This pins the reference account order, signer/writable constraints, instruction data shape, CPI protocol/data layout, and state-write contract before the later dual-deploy runtime harness. * **V-GATE-SOLANA-10L** — System Program transfer Pinocchio live equivalence. Script: `scripts/solana/pinocchio-system-transfer-live-equivalence.sh` builds the ProofForge ELF and the checked-in Pinocchio reference ELF, starts Surfpool, deploys both programs with separate program ids, invokes the same `@solana/web3.js` System transfer scenario against each, and compares the recipient lamport delta and program-owned state write. This gate skips when `cargo-build-sbf` cannot find Solana rustc/platform-tools; run `just solana-pinocchio-install-sbf-tools` to repair that toolchain. * **V-GATE-SOLANA-11** — System Program `create_account` CPI live behavior through Surfpool and Web3.js. Script: `scripts/solana/system-create-account-cpi-web3-smoke.sh` builds the generated `--solana-system-create-account-cpi-elf` fixture, validates its artifact schema, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes the generated create entrypoint with payer and new-account signers, and checks the new account owner, data length, lamports, plus the state account's recorded lamports and space values. * **V-GATE-SOLANA-11R** — System Program `create_account` Pinocchio reference equivalence. Script: `scripts/solana/pinocchio-system-create-account-equivalence.sh` emits the generated `--solana-system-create-account-cpi-elf` artifact, compares the instruction ABI, account order, signer/writable constraints, CPI protocol/data layout, lamports/space/owner contract, and two-field state-write contract against `references/solana/pinocchio/system-create-account`, and can additionally typecheck that reference with `pinocchio-system` when `PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1`. * **V-GATE-SOLANA-11L** — System Program `create_account` Pinocchio live equivalence. Script: `scripts/solana/pinocchio-system-create-account-live-equivalence.sh` builds the ProofForge ELF and the checked-in Pinocchio reference ELF, starts Surfpool, deploys both programs with separate program ids, invokes the same `@solana/web3.js` create-account scenario against each, and compares the lamports/space inputs plus the two program-owned state writes. This gate skips when `cargo-build-sbf` cannot find Solana rustc/platform-tools; run `just solana-pinocchio-install-sbf-tools` to repair that toolchain. * **V-GATE-SOLANA-12** — SPL Token `transfer_checked` CPI live behavior through Surfpool and Web3.js. Script: `scripts/solana/spl-token-transfer-cpi-web3-smoke.sh` builds the generated `--solana-spl-token-transfer-cpi-elf` fixture, validates its artifact schema, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, creates a mint plus source/destination token accounts through `@solana/spl-token`, invokes the generated transfer entrypoint with the source authority signer, and checks token balance deltas plus the state account's recorded amount. * **V-GATE-SOLANA-12R** — SPL Token `transfer_checked` Pinocchio reference equivalence. Script: `scripts/solana/pinocchio-spl-token-transfer-equivalence.sh` emits the generated `--solana-spl-token-transfer-cpi-elf` artifact, compares the instruction ABI, account order, signer/writable constraints, CPI protocol/data layout, decimals/amount contract, and state-write contract against `references/solana/pinocchio/spl-token-transfer`, and can additionally typecheck that reference with `pinocchio-token` when `PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1`. * **V-GATE-SOLANA-12L** — SPL Token `transfer_checked` Pinocchio live equivalence. Script: `scripts/solana/pinocchio-spl-token-transfer-live-equivalence.sh` builds the ProofForge ELF and the checked-in Pinocchio Token reference ELF, starts Surfpool, deploys both programs with separate program ids, invokes the same `@solana/web3.js` + `@solana/spl-token` transfer\_checked scenario against each, and compares source/destination token balance deltas plus the program-owned amount state write. This gate skips when `cargo-build-sbf` cannot find Solana rustc/platform-tools; run `just solana-pinocchio-install-sbf-tools` to repair that toolchain. * **V-GATE-SOLANA-13** — SPL Token `mint_to`/`burn`/`approve`/`revoke` CPI live behavior through Surfpool and Web3.js. Script: `scripts/solana/spl-token-ops-cpi-web3-smoke.sh` builds the generated `--solana-spl-token-ops-cpi-elf` fixture, validates artifact instruction schemas for four entrypoints, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, creates a mint plus source/destination token accounts through `@solana/spl-token`, invokes the generated mint, burn, approve, and revoke entrypoints with the source/mint authority signer, and checks supply/balance/delegate changes plus the state account's recorded mint, burn, approve, and revoke values. * **V-GATE-SOLANA-13R** — SPL Token `mint_to`/`burn`/`approve`/`revoke` Pinocchio reference equivalence. Script: `scripts/solana/pinocchio-spl-token-ops-equivalence.sh` emits the generated `--solana-spl-token-ops-cpi-elf` artifact, compares the four instruction ABIs, shared account order, signer/writable constraints, CPI protocol/data layout, SPL Token instruction tags, and state-write contract against `references/solana/pinocchio/spl-token-ops`, and can additionally typecheck that reference with `pinocchio-token` when `PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1`. * **V-GATE-SOLANA-13L** — SPL Token `mint_to`/`burn`/`approve`/`revoke` Pinocchio live equivalence. Script: `scripts/solana/pinocchio-spl-token-ops-live-equivalence.sh` builds the ProofForge ELF and the checked-in Pinocchio Token ops reference ELF, starts Surfpool, deploys both programs with separate program ids, invokes the same `@solana/web3.js` + `@solana/spl-token` mint/burn/approve/revoke scenario against each, and compares token effects plus the program-owned state writes. This gate skips when `cargo-build-sbf` cannot find Solana rustc/platform-tools; run `just solana-pinocchio-install-sbf-tools` to repair that toolchain. * **V-GATE-SOLANA-13A** — SPL Token `set_authority` CPI live behavior through Surfpool and Web3.js. Script: `scripts/solana/spl-token-authority-cpi-web3-smoke.sh` builds the generated `--solana-spl-token-authority-cpi-elf` fixture, validates the artifact's single-entrypoint ABI, starts Surfpool, deploys the ELF, creates an SPL Token mint through `@solana/spl-token`, invokes the generated program to transfer mint authority to a new authority pubkey read from the instruction accounts, and checks the mint authority plus state marker. * **V-GATE-SOLANA-13AR** — SPL Token `set_authority` Pinocchio reference equivalence. Script: `scripts/solana/pinocchio-spl-token-authority-equivalence.sh` emits the generated `--solana-spl-token-authority-cpi-elf` artifact, compares the instruction ABI, account order, signer/writable constraints, CPI metadata, `SetAuthority` instruction data contract, and marker state-write contract against `references/solana/pinocchio/spl-token-authority`, and can additionally typecheck that reference with `pinocchio-token` when `PROOF_FORGE_PINOCCHIO_CARGO_CHECK=1`. * **V-GATE-SOLANA-13AL** — SPL Token `set_authority` Pinocchio live equivalence. Script: `scripts/solana/pinocchio-spl-token-authority-live-equivalence.sh` builds the ProofForge ELF and the checked-in Pinocchio Token authority reference ELF, starts Surfpool, deploys both programs with separate program ids, invokes the same `@solana/web3.js` + `@solana/spl-token` mint-authority transfer scenario against each, and compares mint authority plus state marker. This gate skips when `cargo-build-sbf` cannot find Solana rustc/ platform-tools; run `just solana-pinocchio-install-sbf-tools` to repair that toolchain. * **V-GATE-SOLANA-14** — Solana `events.emit` scalar log plus `sol_log_pubkey` and `sol_log_data` live behavior through Surfpool and Web3.js. Script: `scripts/solana/log-event-web3-smoke.sh` builds the generated `--solana-log-event-elf` fixture, validates artifact instruction schema, `events.emit` capability metadata, Solana-only `pubkeyLogActions`, and Solana-only `dataLogActions`, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes the generated `emit` entrypoint with a scalar `amount` instruction parameter, checks the program-owned state account's recorded amount, checks transaction `logMessages` for the `sol_log_64_` output containing the stable `AmountEvent` tag and scalar value, invokes `log_state_pubkey`, checks transaction `logMessages` for the state account's base58 pubkey from `sol_log_pubkey`, invokes `log_state_data`, and checks transaction `logMessages` for the base64 `Program data:` payload from `sol_log_data`. * **V-GATE-SOLANA-15** — Solana Clock sysvar live behavior through Surfpool and Web3.js. Script: `scripts/solana/clock-sysvar-web3-smoke.sh` builds the generated `--solana-clock-sysvar-elf` fixture, validates artifact instruction schema and `env.block` capability metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes the generated `record` entrypoint, checks that `sol_get_clock_sysvar` wrote `Clock.slot` into the program-owned state account, and compares that value with the transaction slot from Web3.js metadata. * **V-GATE-SOLANA-16** — Solana memory syscall live behavior through Surfpool and Web3.js. Script: `scripts/solana/memory-web3-smoke.sh` builds the generated `--solana-memory-elf` fixture, validates `runtime.memory` artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `set_source` and `copy_compare_fill`, and checks copied value, moved value, memcmp result, and memset byte pattern in the program-owned state account. * **V-GATE-SOLANA-17** — Solana SHA-256/Keccak-256/Blake3 syscall live behavior through Surfpool and Web3.js. Script: `scripts/solana/crypto-hash-web3-smoke.sh` builds the generated `--solana-crypto-hash-elf` fixture, validates `crypto.hash` artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `set_preimage`, `hash_preimage`, `keccak_preimage`, and `blake3_preimage`, and compares the program-owned account's 32-byte digests against Node `crypto.createHash("sha256")` and `@noble/hashes` Keccak-256/Blake3 for the same preimage bytes. * **V-GATE-SOLANA-18** — Solana Rent sysvar live behavior through Surfpool and Web3.js. Script: `scripts/solana/rent-sysvar-web3-smoke.sh` builds the generated `--solana-rent-sysvar-elf` fixture, validates `sysvar` target extension artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `record_rent`, and compares the program-owned account's recorded `Rent.lamports_per_byte_year` with the Rent sysvar account's first `u64` word. * **V-GATE-SOLANA-19** — Solana EpochSchedule sysvar live behavior through Surfpool and Web3.js. Script: `scripts/solana/epoch-schedule-sysvar-web3-smoke.sh` builds the generated `--solana-epoch-schedule-sysvar-elf` fixture, validates `sysvar` target extension artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `record_epoch_schedule`, and compares the program-owned account's recorded `EpochSchedule.slots_per_epoch`, `EpochSchedule.leader_schedule_slot_offset`, `EpochSchedule.warmup`, `EpochSchedule.first_normal_epoch`, and `EpochSchedule.first_normal_slot` fields with RPC `getEpochSchedule()`. * **V-GATE-SOLANA-20** — Solana LastRestartSlot sysvar live behavior through Surfpool and Web3.js. Script: `scripts/solana/last-restart-slot-sysvar-web3-smoke.sh` builds the generated `--solana-last-restart-slot-sysvar-elf` fixture, validates feature-gated `sysvar` target-extension artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `record_last_restart_slot`, and compares the program-owned account's recorded `LastRestartSlot.last_restart_slot` with the LastRestartSlot sysvar account's first `u64` word. The generated assembly uses `sol_get_sysvar` with `SysvarLastRestartS1ot1111111111111111111111` to stay compatible with the current `sbpf` assembler while preserving the Solana SDK-level LastRestartSlot capability. * **V-GATE-SOLANA-21** — Solana EpochRewards sysvar live behavior through Surfpool and Web3.js. Script: `scripts/solana/epoch-rewards-sysvar-web3-smoke.sh` builds the generated `--solana-epoch-rewards-sysvar-elf` fixture, validates `sysvar` target extension artifact metadata for all current `EpochRewards` fields, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, invokes `record_epoch_rewards`, and compares the program-owned account's recorded `EpochRewards.distribution_starting_block_height`, `EpochRewards.num_partitions`, `EpochRewards.parent_blockhash_word0..3`, `EpochRewards.total_points_low/high`, `EpochRewards.total_rewards`, `EpochRewards.distributed_rewards`, and `EpochRewards.active` with the EpochRewards sysvar account data. * **V-GATE-SOLANA-22** — Solana return-data and compute-unit syscall live behavior through Surfpool and Web3.js. Script: `scripts/solana/return-data-compute-web3-smoke.sh` builds the generated `--solana-return-data-compute-elf` fixture, validates `runtime.return_data` and `runtime.compute_units` target-extension artifact metadata, starts Surfpool, deploys the ELF with `solana program deploy --use-rpc`, confirms `sol_set_return_data` via simulation `returnData`, checks empty `sol_get_return_data` reads, checks a same-instruction set/get roundtrip including the returned program id words, records a nonzero `sol_remaining_compute_units` value, and verifies `sol_log_compute_units_` emits compute-unit logs. * Move smoke — `aptos move compile/test` or Sui Move validation. * Cross-target capability rejection matrix — compile-time diagnostics for unsupported capability/target combinations beyond the target-specific Psy and EVM diagnostic smokes. ## Upfront validation rule for new target work Before a target exits `Research`, docs must name: 1. The external tools required. 2. The minimal artifact the target produces. 3. A local command or script that builds or validates the artifact. 4. The expected artifact path. 5. One observable success criterion. If no runnable local command exists, the target remains `Research`. ## Optional external tools Current CI installs `just` 1.48.0, Foundry stable, and `solc` 0.8.30. Local machines may not have `just`, `solc`, `cast`, `forge`, `psyup`, `dargo`, `sbpf`, `surfpool`, Solana CLI, Node, or npm. Missing `just` blocks the local command catalog but not direct script execution. Missing EVM tools block EVM toolchain gates but not `lake build`. Missing Psy tools block only the Psy smoke Dargo portions; source generation and golden diff still run before each script exits. Missing Solana tools block Solana assembly/runtime smokes but not Lean builds or target-registry checks. All Dargo-backed Psy smoke scripts also record the generated Dargo package source copy at `src/main.psy` and the generated `Dargo.toml` package manifest in `proof-forge-artifact.json`. The metadata validator checks the package source path, byte size, SHA-256 hash, and hash parity with the generated source file. It also checks the manifest path, byte size, SHA-256 hash, `[package]` section, `type = "bin"`, and `[dependencies]` section. Package generation is shared through `scripts/psy/write-dargo-package.py` so every smoke uses the same source-copy and manifest layout.