> ## 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. # Development Log > This log records engineering milestones for ProofForge. It is not a replacement This log records engineering milestones for ProofForge. It is not a replacement for Git history. Use it to understand what changed, what was validated, and what the next engineering step is. ## Format Each entry should include: * date * commit or work range * summary * validation run * known limitations * next step ## 2026-07-03 ### Review Follow-up: RFC, Portfolio, and Gate State Alignment Commit: feature commit for review follow-up documentation alignment Summary: * Reconciled the post-review assessment with the current repository state: RFC 0009/D-039 already reflect CLI M1 as landed, and D-045/Gate P0 already freeze non-primary target advancement. * Updated the platform gap analysis so CLI and budget work no longer read as unplanned or unimplemented after RFC 0009 M1, D-040, RFC 0010, and Gate G0. * Updated the implementation backlog so Gate G0 is treated as closed and the remaining work is correctly scoped to Gate P0 production hardening and CLI M3/M4 migration. Validation run: ```sh theme={null} scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * This is a documentation alignment pass. It does not implement new FV-4 storage/aggregate trace obligations or change target capability ids. Next step: * Continue P0 hardening in priority order, with the next EVM FV-4 slice focused on map/fixed-array storage obligations unless Solana live-equivalence work takes priority. ### EVM Expression Assertion Executable Yul Trace Obligation Commit: feature commit for FV-4 EVM expression/assertion executable trace obligation Summary: * Extended `ProofForge.IR.Semantics` with predicate expressions, boolean operators, casts, bitwise/shift operators, exponentiation, and assertion / assertion-equality statement execution for the focused scalar subset. * Extended `ProofForge.Backend.Evm.YulSemantics` with `exp`, matching the Yul emitted for EVM expression probes. * Added `expression_evm_yul_executable_trace_ok`, which runs `EvmExpressionProbe` through the generated selector-dispatched Yul subset and compares observable return words against the IR trace. Validation run: ```sh theme={null} lake build ProofForge.IR.Semantics lake build ProofForge.Backend.Evm.YulSemantics lake build ProofForge.Backend.Evm.Refinement lake build ProofForge.Backend.Evm scripts/i18n/check-sync.sh git diff --check just check ``` Known limitations: * This covers successful assertion/expression paths only. Revert/error traces, maps, arrays, structs, aggregate returns, and full EVM word overflow semantics are still future FV-4 slices. Next step: * Extend executable obligations to map storage and fixed-array storage probes, then move into struct and aggregate return/state shapes. ### EVM ValueVault Executable Yul Trace Obligation Commit: feature commit for FV-4 ValueVault executable Yul trace obligation Summary: * Extended `ProofForge.IR.Semantics` with entrypoint argument binding, U32/U64 `sub`/`mul`/`div`/`mod`, `checkpointId`, and event field evaluation as a no-op state effect. * Extended `ProofForge.Backend.Evm.YulSemantics` with calldata argument words, calldata size, `number`, `keccak256`, and `log0` through `log4` execution as focused FV-4 primitives. * Added `value_vault_evm_yul_executable_trace_ok`, which runs the shared ValueVault scenario through the generated selector-dispatched Yul subset and compares observable return words against the scalar IR trace. Validation run: ```sh theme={null} lake build ProofForge.IR.Semantics lake build ProofForge.Backend.Evm.YulSemantics lake env lean ProofForge/Backend/Evm/Refinement.lean lake build ProofForge.Backend.Evm scripts/i18n/check-sync.sh git diff --check just check ``` Known limitations: * This is still a focused FV-4 slice, not a full EVM or libyul semantics. Event logs are modeled as no-op after field evaluation, block number is fixed at zero, `keccak256` returns a deterministic placeholder for the non-observable log/topic paths used here, and assertions/maps/arrays/aggregates are not covered yet. Next step: * Extend executable obligations from scalar storage to assertion, map, array, struct, and aggregate probes, then connect ValueVault user invariants to the IR semantics. ### EVM Counter Executable Yul Trace Obligation Commit: feature commit for FV-4 executable Yul trace obligation Summary: * Added `ProofForge.Backend.Evm.YulSemantics`, a narrow executable model for the Counter-shaped generated Yul subset. * Covered selector calldata decoding, dispatcher `switch`, internal function calls, local variables, `sstore`, `sload`, scalar arithmetic, `mstore`, and EVM `return` words. * Extended `ProofForge.Backend.Evm.Refinement` with `counter_evm_yul_executable_trace_ok`, which runs `initialize -> get -> increment -> get` through the generated Yul dispatcher and compares observable return words against the scalar IR trace. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.YulSemantics lake env lean ProofForge/Backend/Evm/Refinement.lean lake build ProofForge.Backend.Evm scripts/i18n/check-sync.sh git diff --check just check ``` Known limitations: * This is still a focused FV-4 slice, not a full EVM or libyul semantics. The interpreter fails explicitly for unsupported Yul constructs and currently covers the Counter path only. Next step: * Extend the Yul-subset interpreter and trace obligations toward ValueVault: multi-entry scalar storage behavior first, then assertions, maps, arrays, and aggregate return/state shapes. ### EVM Counter Formal Trace Surface Obligation Commit: feature commit for FV-4 EVM surface obligation Summary: * Added `ProofForge.Backend.Evm.Refinement` with a `TraceObligation` for the Counter `initialize -> get -> increment -> get` scenario. * Reused the scalar IR executable semantics to prove the expected observable trace (`0` then `1`) with `native_decide`. * Added an EVM/Yul surface obligation that checks generated Yul has the selector-dispatched top-level functions required by the same trace. * Imported the module from `ProofForge.Backend.Evm`, so the theorem is checked by the existing `just build` CI path. Validation run: ```sh theme={null} lake env lean ProofForge/Backend/Evm/Refinement.lean ``` Known limitations: * This is the first FV-4 EVM anchor, not a full EVM refinement theorem. It does not yet interpret Yul storage operations or return words. Next step: * Add a tiny Yul-subset interpreter for Counter-shaped Yul (`sstore`, `sload`, `add`, selector-dispatched calls, `return`) and compare its observable trace against the IR trace. ### Review Alignment: CLI RFC And Primary-Chain Portfolio Freeze Commit: feature commit for review alignment Summary: * Accepted RFC 0009 as the durable target-first CLI surface and recorded that M1 has already landed through the compatibility layer; M3/M4 remain open. * Corrected D-039 so it no longer reads as a pre-code freeze after code already exists, and added an explicit superseded-position note for that old wording. * Tightened the target portfolio wording: current product implementation is limited to `solana-sbpf-asm` -> `evm` -> `wasm-near`; `psy-dpn`, `aleo-leo`, and `wasm-cloudflare-workers` are maintenance-only inventory until Gate P0 closes. Validation run: ```sh theme={null} scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * This is a documentation and governance correction. It does not implement the missing end-to-end proof link between source-level invariants and generated EVM/Wasm artifacts. Next step: * Start FV-4 as a separate implementation slice: add an EVM trace obligation patterned after the existing NEAR trace obligation, then connect it to a concrete generated Yul/bytecode fixture and CI gate. ### Solana Pinocchio Live Equivalence Aggregate Gate Commit: feature commit for Pinocchio live aggregate gate Summary: * Added `scripts/solana/pinocchio-live-equivalence.sh` as one aggregate entrypoint for the five ProofForge-vs-Pinocchio live dual-deploy gates. * Added `just solana-pinocchio-live-equivalence` so local and future profiled CI lanes can run the full live suite through one command. * The aggregate gate runs every child harness, summarizes pass/skip/fail counts, fails on any real child failure, and returns skip code `2` when prerequisites are missing unless `PROOF_FORGE_PINOCCHIO_LIVE_ALLOW_SKIP=1` is explicitly set for a probe lane. Validation run: ```sh theme={null} bash -n scripts/solana/pinocchio-live-equivalence.sh scripts/solana/pinocchio-*-live-equivalence.sh SURFPOOL=/nonexistent-proof-forge-surfpool scripts/solana/pinocchio-live-equivalence.sh PROOF_FORGE_PINOCCHIO_LIVE_ALLOW_SKIP=1 SURFPOOL=/nonexistent-proof-forge-surfpool scripts/solana/pinocchio-live-equivalence.sh ``` Known limitations: * This creates the suite entrypoint and strict skip semantics; it does not yet install the Solana SBF toolchain in GitHub Actions or make live dual-deploy mandatory in default CI. Next step: * Add a profiled CI job that installs/checks Surfpool, Solana CLI, `cargo-build-sbf`, `sbpf`, Node, and npm, then runs the aggregate live suite without `PROOF_FORGE_PINOCCHIO_LIVE_ALLOW_SKIP`. ### Solana Pinocchio Live Harness Shared Helper Commit: feature commit for Pinocchio live harness hardening Summary: * Added a shared `scripts/solana/pinocchio-live-common.sh` helper for the five Pinocchio live dual-deploy harnesses. * Centralized Solana rustup/toolchain detection, `cargo-build-sbf` invocation, SBF repair hints, Pinocchio ELF discovery, skip/fail handling, and Surfpool cleanup. * Kept each harness-specific fixture, port, deployment, Web3.js scenario, and result comparison local to the existing live script. Validation run: ```sh theme={null} bash -n scripts/solana/pinocchio-live-common.sh scripts/solana/pinocchio-*-live-equivalence.sh just solana-pinocchio-reference-equivalence SURFPOOL=/nonexistent-proof-forge-surfpool scripts/solana/pinocchio-system-transfer-live-equivalence.sh ``` Known limitations: * This hardens the live harness implementation path but does not make the live dual-deploy gates mandatory in CI yet; that still depends on stable Solana rustc/platform-tools, Surfpool, Solana CLI, `sbpf`, Node, and npm availability in the runner. Next step: * Add a CI/profiled live-equivalence lane once the Solana SBF toolchain install path is deterministic enough for GitHub Actions, then extend reference coverage toward Token-2022. ### Gate G0 Closed Commit: documentation sign-off commit Summary: * Closed Gate G0 in the gate ledger after recording the successful current remote CI run for commit `0c52fb8`. * Clarified that Gate G0 closes only the shared behavior/resource-budget slice; Gate P0 remains open for the production-grade Solana, EVM, and NEAR/Wasm completion covenant. * Updated the target roadmap so Tier-1/new-chain advancement stays frozen on Gate P0, not the now-closed G0 slice. Validation run: ```sh theme={null} gh run watch 28658576786 --exit-status ``` Known limitations: * P0 is still open. Solana live dual-deploy equivalence, EVM semantic-plan migration, and NEAR/Wasm target-first local execution/deploy metadata sign-off remain the next production-hardening tracks. Next step: * Continue P0 in implementation order: Solana live Pinocchio dual-deploy hardening first, then EVM semantic-plan migration, then NEAR/Wasm target-first deploy metadata sign-off. ### Solana Pinocchio Reference Equivalence In CI Light Gate Commit: feature commit for Solana Pinocchio reference equivalence Summary: * Added source-only target-first emission for the Solana ContractSpec CPI fixtures (`system-cpi`, `system-create-account-cpi`, SPL Token transfer, ops, and authority) so reference-equivalence checks can validate artifact ABI/CPI metadata without requiring `sbpf`. * Added `just solana-pinocchio-reference-equivalence` and included it in `just solana-light`, which is the default CI Solana gate. * Added a CLI mapping regression test for the new target-first `--format s` routes and the existing `--format elf` routes. * Updated Pinocchio reference manifests with source fixture ids while keeping ELF fixture ids for live dual-deploy gates. Validation run: ```sh theme={null} lake build proof-forge lake env lean Tests/CliTargetFirst.lean just solana-pinocchio-reference-equivalence ``` Known limitations: * This closes the CI-safe source/reference half of the Pinocchio track only. Live dual-deploy equivalence still depends on Surfpool, Solana CLI, `sbpf`, and stable `cargo-build-sbf`/Solana rustc platform tools. Next step: * Continue Workstream 7 by hardening the live Pinocchio dual-deploy harnesses for reproducible local/CI toolchain installation. ### ValueVault Solana Budget Baselines Commit: feature commit for ValueVault Solana budget baselines Summary: * Added `--trace` to the unified testkit runner so budget work can print the raw per-call harness lines already stored in `CallOutcome.raw_line`. * Fixed the EVM ValueVault testkit harness so the `CAST` environment override is passed through to `proof-forge emit --cast`, matching the availability check that decides whether the EVM branch can run locally. * Fixed the target-first `proof-forge emit --target evm --fixture ... --format bytecode` compatibility mapper so it forwards `--cast` to the legacy EVM bytecode flags instead of silently falling back to `cast`. * Pinned Counter `near_gas` baselines and all ValueVault `solana_cu`, `evm_gas`, and `near_gas` baselines in the testkit scenarios. * Updated the Gate G0 ledger to reflect the repaired remote CI baseline and the now-implemented budget acceptance criteria; formal closure still waits for the current commit's remote CI/sign-off record. Validation run: ```sh theme={null} cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- --help .lake/build/bin/proof-forge emit --target evm --fixture value-vault --format bytecode --cast build/tools/cast-shim --yul-output /tmp/pf-vv.yul --artifact-output /tmp/pf-vv.json -o /tmp/pf-vv.bin cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario counter --trace cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target solana-sbpf-asm --trace CAST="$PWD/build/tools/cast-shim" cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --trace ``` Known limitations: * The testkit budget baselines are deterministic harness baselines; live-chain budget gates remain a separate Solana/Foundry hardening concern. Next step: * Run the current commit through CI, then record Gate G0 sign-off or continue the non-blocking Tier-0 hardening items: Solana Pinocchio CI equivalence and EVM semantic-plan migration. ### Unified Testkit Deploy Manifest Schema Checks Commit: feature commit for unified testkit deploy manifest schema checks Summary: * Added `exists`, `kind`, and `non_empty` assertions to nested `[[artifact.json]]` and `[[artifact.toml]]` checks, so scenario TOML can express presence, absence, type, and non-empty schema constraints without fixture-specific scripts. * Updated Counter and ValueVault scenarios to validate EVM deploy manifests as first-class artifacts, including init-code mode, absent chain profile, not-generated broadcast status, ABI/capability counts, and deploy manifest file references back to generated Yul, bytecode, and init-code artifacts. * Added targeted type/non-empty checks for key EVM and Solana metadata/manifest paths that were previously only implicitly checked by equality or script validators. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list CAST="$PWD/build/tools/cast-shim" just testkit ``` Known limitations: * `kind` and `non_empty` validate schema shape only; semantic relations across artifacts still use `[[artifact.file]]` and `[[artifact.jsonArtifact]]`. Next step: * Continue moving script-only artifact metadata validators into scenario TOML, then remove redundant script assertions once the unified testkit owns the same artifacts. ### Unified Testkit Structured Length Checks Commit: feature commit for unified testkit structured length checks Summary: * Added `length` assertions to nested `[[artifact.json]]` and `[[artifact.toml]]` scenario checks for arrays, objects/tables, and strings. * Updated Counter and ValueVault scenarios to pin generated ABI entrypoint, event, capability, artifact, Solana manifest instruction, Solana metadata instruction, and IDL instruction counts declaratively. * Extended the structured artifact unit test so JSON and TOML length checks are covered in `proof-forge-testkit-core`. Validation run: ```sh theme={null} cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace CAST="$PWD/build/tools/cast-shim" just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * `length` asserts collection/string shape, not the semantic meaning of each item; per-entry checks still need explicit `equals` or `contains` assertions. Next step: * Keep migrating old schema validators into scenario TOML, then remove duplicate script-only assertions once the testkit owns the same generated artifacts. ### Unified Testkit JSON Artifact Equality Checks Commit: feature commit for unified testkit JSON artifact equality checks Summary: * Added nested `[[artifact.jsonArtifact]]` scenario checks that compare a JSON value embedded in one artifact with another harness-produced JSON artifact. * Updated the Solana ValueVault scenario so metadata must embed the same IDL JSON as the generated `idl` artifact. * Moved ValueVault Solana IDL/client shape checks into scenario TOML through structured JSON assertions and text contains checks. Validation run: ```sh theme={null} cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace CAST="$PWD/build/tools/cast-shim" just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * JSON equality checks currently compare JSON values only; non-JSON artifacts still use `matches_file`, `contains`, structured TOML checks, or file-reference metadata checks. Next step: * Continue migrating duplicate per-target schema checks into scenario-declared artifact expectations where the harness already exposes the generated files. ### Unified Testkit Artifact File Metadata Checks Commit: feature commit for unified testkit artifact file metadata checks Summary: * Added nested `[[artifact.file]]` scenario checks that validate JSON metadata file entries against harness-produced artifacts by path, byte size, and SHA-256 hash. * Extended the EVM testkit harness to expose generated `init-code` and `deploy-manifest` artifacts alongside Yul, bytecode, and metadata, so EVM metadata references can be asserted declaratively. * Updated Counter and ValueVault scenarios so EVM and Solana metadata now prove their generated artifact references through the shared testkit runner. Validation run: ```sh theme={null} cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace CAST="$PWD/build/tools/cast-shim" just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * `[[artifact.file]]` currently validates JSON metadata entries; TOML file reference validation can be added if a target manifest needs the same path/bytes/hash relation. Next step: * Use the shared metadata file-reference checks to retire more duplicated per-target artifact hash validation from fixture-specific scripts where the testkit already owns the generated artifacts. ### Unified Testkit EVM ValueVault Golden Commit: feature commit for unified testkit EVM ValueVault golden Summary: * Added `Examples/Evm/ValueVault.golden.yul` as the reviewed Yul source snapshot for the portable ValueVault scenario. * Upgraded the `evm` Yul artifact in `testkit/scenarios/value-vault.toml` to check full generated-file equality through `matches_file`, while retaining focused substring checks for the contract object, entrypoints, logs, and block context access. * ValueVault now has scenario-declared source equality for `wasm-near` WAT, `evm` Yul, and `solana-sbpf-asm` assembly/manifest. Validation run: ```sh theme={null} .lake/build/bin/proof-forge --emit-value-vault-ir-yul --cast build/tools/cast-shim -o build/testkit/evm/value-vault/ValueVault.yul solc --strict-assembly build/testkit/evm/value-vault/ValueVault.yul --bin CAST="$PWD/build/tools/cast-shim" cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target evm cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * Local `just testkit` skips the ValueVault EVM runtime branch unless Foundry `cast` or a compatible `CAST` override is available; CI covers that branch with Foundry installed. Next step: * Move the remaining Workstream 26 M4 declarative coverage toward metadata hardening and retiring duplicate per-target script checks. ### Unified Testkit Solana ValueVault Golden Commit: feature commit for unified testkit Solana ValueVault golden Summary: * Added `Examples/Solana/ValueVault.golden.s` and `Examples/Solana/ValueVault.manifest.toml` as the reviewed Solana source/manifest snapshots for the portable ValueVault scenario. * Upgraded `testkit/scenarios/value-vault.toml` so the `solana-sbpf-asm` assembly and manifest artifacts check full generated-file equality through `matches_file`, while retaining focused substring checks for event lowering, syscall usage, storage layout, instruction names, and argument encodings. * ValueVault now has scenario-declared source equality for `wasm-near` WAT and `solana-sbpf-asm` assembly/manifest. At this point, EVM Yul remained the only ValueVault source artifact still using source-shape checks. Validation run: ```sh theme={null} cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target solana-sbpf-asm cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * At this point, ValueVault EVM Yul still used scenario-declared source-shape checks instead of complete golden equality. * Local `just testkit` skips the ValueVault EVM runtime branch when Foundry `cast` is unavailable; CI covers that branch with Foundry installed. Next step: * Add a full ValueVault EVM Yul golden once selector hydration is available in the validation environment used to refresh the snapshot. ### Unified Testkit Wasm ValueVault Golden Commit: feature commit for unified testkit Wasm ValueVault golden Summary: * Added `Examples/WasmNear/ValueVault.golden.wat` as the portable ValueVault WAT golden for the `wasm-near` EmitWat path. * Upgraded `testkit/scenarios/value-vault.toml` so its `wasm-near` artifact checks full generated-source equality through `matches_file`, while keeping focused substring checks for important imports, exports, and event logging. * ValueVault now has scenario-declared Wasm/NEAR WAT source equality in the unified testkit; its EVM Yul and Solana sBPF/manifest artifacts still use source-shape checks until their full golden snapshots are reviewed. Validation run: ```sh theme={null} lake env lean --run Tests/EmitWatValueVault.lean cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target wasm-near just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * ValueVault EVM Yul and Solana sBPF/manifest comparisons were still scenario-declared source-shape checks instead of complete golden equality. * Local `just testkit` skips the ValueVault EVM runtime branch when Foundry `cast` is unavailable; CI covers that branch with Foundry installed. Next step: * Add full ValueVault source goldens for EVM Yul and Solana sBPF/manifest once their emitted artifacts are stable enough to review as snapshots. ### Unified Testkit Wasm Counter Golden Commit: feature commit for unified testkit Wasm Counter golden Summary: * Added `Examples/WasmNear/Counter.golden.wat` as the portable IR Counter WAT golden for the `wasm-near` EmitWat path. * Moved the `wasm-near` Counter WAT equality check into `testkit/scenarios/counter.toml` through a scenario-declared `[[artifact]]` `matches_file` expectation. * Counter now has target-source golden equality in the unified testkit for all three priority targets: `wasm-near` WAT, `evm` Yul, and `solana-sbpf-asm` assembly plus manifest. Validation run: ```sh theme={null} lake env lean --run Tests/EmitWatSmoke.lean cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario counter --target wasm-near just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * ValueVault still uses scenario-declared WAT/Yul substring checks because it does not yet have committed portable-source goldens. Next step: * Add source goldens for ValueVault once its cross-target emitted source shape is stable enough to review as a snapshot. ### Unified Testkit EVM Counter Golden Commit: feature commit for unified testkit EVM Counter golden Summary: * Added `Examples/Evm/Counter.golden.yul` as the portable IR Counter Yul golden, separate from the older Lean SDK contract golden under `Examples/Evm/Contracts/`. * Moved the EVM Counter Yul equality check into `testkit/scenarios/counter.toml` through a scenario-declared `[[artifact]]` `matches_file` expectation. * Kept EVM runtime behavior in `testkit/harness-evm`; the harness now only publishes the generated `yul` artifact and the common scenario validator owns the source snapshot comparison. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario counter --target evm just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * ValueVault still uses scenario-declared Yul substring checks because it does not yet have a committed portable-source golden. Next step: * Add portable-source goldens for the remaining stable testkit fixtures, then decide which old golden-only shell checks can be retired or moved to scheduled chain-authentic gates. ### Unified Testkit Unsupported Capability Diagnostics Commit: feature commit for unified testkit diagnostic scenarios Summary: * Added `[[diagnostic]]` scenario expectations so testkit can run diagnostic-only scenarios without pretending they have runtime steps. * Added `testkit/scenarios/unsupported-crosscall.toml`, which asserts that `solana-sbpf-asm` rejects the portable `crosscall.invoke` capability with the expected target/capability diagnostic. * Added `Tests/TestkitSolanaCapabilityDiagnostic.lean` as the Lean-side diagnostic driver and wired `testkit/harness-solana` to execute it. * Updated runner target filtering and summary output so diagnostic-only scenarios participate in `just testkit` but do not interfere with positive target runs. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace lake env lean --run Tests/TestkitSolanaCapabilityDiagnostic.lean cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario unsupported-crosscall cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --target evm just testkit scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * The diagnostic scenario surface currently has one Solana capability case. More target/compiler diagnostics can move in as each harness exposes a small target-owned diagnostic driver. Next step: * Continue migrating deterministic artifact/source checks into scenario declarations, then decide which existing standalone diagnostic smokes should become additional `[[diagnostic]]` scenarios. ### Unified Testkit EVM Metadata Expectations Commit: feature commit for unified testkit EVM metadata expectations Summary: * Added scenario-declared EVM metadata checks for Counter and ValueVault, covering target identity, artifact kind, fixture/source kind, declared capabilities, ABI entrypoint names, and bytecode-generation validation status. * Removed the duplicated EVM harness metadata identity checks for `target`/`sourceKind`; `testkit/harness-evm` now reads metadata only for runtime selector dispatch. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml --workspace cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario counter --target evm cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target evm scripts/i18n/check-sync.sh git diff --check ``` Known limitations: * Local ValueVault EVM execution still skips when Foundry `cast` is not on `PATH`; CI covers the full path where Foundry is installed. Next step: * Continue migrating the remaining shell-only golden/source checks that are deterministic into scenario declarations, while keeping live Foundry/Anvil deployment gates separate. ### Unified Testkit Scenario Target Validation Commit: feature commit for unified testkit scenario target validation Summary: * Tightened scenario discovery so `testkit/core` rejects empty target ids, duplicate target ids, and artifact expectations that reference a target not declared in the scenario's `targets` list. * Added a negative unit test proving stale or mistyped artifact target expectations fail during `discover_scenarios`, before any target harness runs. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list ``` Known limitations: * This only validates scenario configuration. Harness availability still depends on optional target tools such as `cast`, `sbpf`, and `solana-keygen`. Next step: * Continue moving pure artifact assertions out of target harnesses and into scenario declarations until the remaining M4 shell-gate duplication is isolated to live/network-authentic smoke tests. ### Unified Testkit Solana Harness Thinning Commit: feature commit for Solana testkit artifact validation thinning Summary: * Removed duplicated Solana harness metadata and manifest semantic validators after their checks were moved into scenario-declared `[[artifact.json]]`/`[[artifact.toml]]` expectations. * Kept Solana harness parsing of `manifest.toml` instruction tags because that is runtime dispatch data, not a review-only artifact expectation. * Dropped the direct `serde_json` dependency from `testkit/harness-solana`. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo check --manifest-path testkit/Cargo.toml -p proof-forge-testkit-harness-solana cargo test --manifest-path testkit/Cargo.toml --workspace scripts/i18n/check-sync.sh git diff --check just testkit lake build ``` Known limitations: * The scenario still needs optional `sbpf` and `solana-keygen` before Solana artifact expectations execute. * Duplicated shell gates still exist; this only removes duplicated Solana harness-internal artifact semantics. Next step: * Continue moving pure artifact assertions out of target harnesses and then thin duplicated shell-only golden gates once `just testkit` covers them. ### Unified Testkit Structured Artifact Assertions Commit: feature commit for unified testkit structured artifact assertions Summary: * Extended `testkit/core` artifact expectations with nested `[[artifact.json]]` and `[[artifact.toml]]` checks. * Structured checks support dot paths plus array indexes, for example `validation.manifestGeneration` and `instruction[1].tag`. * Added scenario-declared structured checks for Solana Counter and ValueVault artifact metadata, manifest target/program fields, instruction names, tags, capabilities, and manifest-generation validation status. * Kept the Solana harness runtime parsing in place for instruction dispatch and metadata loading while moving the reviewable expectations into scenario TOML. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core cargo check --manifest-path testkit/Cargo.toml cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list just testkit ``` Known limitations: * Structured checks currently support equality and containment for JSON/TOML values. They do not yet provide unordered array matching or predicate filters such as `instruction[name=deposit]`. * Target harnesses still own runtime-critical parsing and some semantic validation until those checks can be represented safely in the scenario language. Next step: * Migrate the remaining metadata/manifest semantic checks out of target harnesses where they are pure artifact expectations, then begin thinning duplicated shell-only golden gates. ### Unified Testkit M4 Artifact Expectations Commit: feature commit for unified testkit artifact expectations Summary: * Added top-level `[[artifact]]` scenario expectations to `testkit/core`, with `target`, `name`, `matches_file`, and `contains` checks. * Wired all three harnesses to publish named artifacts back into the common validator: `wat` for `wasm-near`, `yul`/`bytecode`/`metadata` for `evm`, and `sbpf-asm`/`manifest`/`metadata`/`idl`/`client` for `solana-sbpf-asm`. * Moved the Solana Counter golden assembly and manifest comparisons into `testkit/scenarios/counter.toml`. * Moved ValueVault's WAT/Yul/sBPF/manifest/metadata source-shape checks into `testkit/scenarios/value-vault.toml`, reducing hardcoded per-fixture behavior in the harnesses. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core just testkit ``` Known limitations: * Artifact expectations currently cover whole-file equality and substring checks only. Structured JSON/TOML assertions still live in target harnesses and external validators. * The local EVM ValueVault artifact checks run only when Foundry `cast` is available; CI covers that path. Next step: * Add structured artifact assertions for metadata and manifest fields, then migrate more of `scripts/portable/value-vault-smoke.sh` and `scripts/solana/counter-smoke.sh` into scenario-declared checks. ### Unified Testkit ValueVault Scenario Commit: feature commit for unified testkit ValueVault scenario Summary: * Added typed scalar scenario args to `testkit/core`, so one TOML scenario can describe portable `u64`/`u32`/`bool` call parameters while each target harness performs its own ABI encoding. * Extended `runtime/offline-host` with `--inputs-hex`, allowing the deterministic NEAR/Wasm host to run a stateful call sequence whose calls use different Borsh input payloads. * Added `testkit/scenarios/value-vault.toml` covering `initialize -> deposit -> charge_fee -> release -> snapshot` plus balance and net-value queries. * Wired ValueVault into `wasm-near` through `Tests/EmitWatValueVault.lean`, into `solana-sbpf-asm` through the existing ValueVault sBPF emitter plus Mollusk, and into `evm` through the revm harness when Foundry `cast` is available for selector hydration. Validation run: ```sh theme={null} lake env lean --run Tests/EmitWatValueVault.lean cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target wasm-near cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target evm cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --scenario value-vault --target solana-sbpf-asm ``` Known limitations: * ValueVault's EVM branch still depends on `cast` because the current Contract SDK EVM path hydrates ABI selectors through Foundry; when `cast` is absent, the harness reports a target skip instead of hiding the dependency. * Testkit validates call order and portable return values. Event payloads, account/log traces, gas/compute budgets, and live deployment remain in the existing target-specific gates. Next step: * Start M4 by migrating more golden-source and artifact checks into scenario fixtures while keeping Foundry/Anvil, Surfpool, near-sandbox, dargo, and leo as chain-authentic gates. ### Unified Testkit M3 Solana Harness Commit: feature commit for unified testkit Solana harness Summary: * Added `testkit/harness-solana`, backed by `mollusk-svm`, as the third RFC 0007 target harness for the portable Counter scenario. * The Solana harness emits Counter sBPF assembly, checks the tracked golden assembly, validates `manifest.toml` and `proof-forge-artifact.json`, builds a standard `sbpf` ELF project, and executes the stateful `initialize -> get -> increment -> get` scenario through Mollusk. * Extended the testkit runner with explicit harness skip reporting so optional chain toolchains such as `sbpf`/`solana-keygen` can be absent without masking failures in always-available targets. * Extended `testkit/scenarios/counter.toml` so Counter now targets `wasm-near`, `evm`, and `solana-sbpf-asm`, with normalized trace parity across all executed targets. Validation run: ```sh theme={null} scripts/solana/counter-smoke.sh cargo fmt --manifest-path testkit/Cargo.toml --all cargo check --manifest-path testkit/Cargo.toml cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-harness-solana just testkit SBPF=/nonexistent-proof-forge-sbpf just testkit ``` Known limitations: * The Solana testkit harness currently supports the portable IR Counter fixture only. * `solana-sbpf-asm` is skipped with a clear reason when `sbpf` or `solana-keygen` is unavailable. * This is a Mollusk in-process runtime gate, not a Surfpool/Web3 live deployment gate. Next step: * Add the portable ValueVault scenario to the testkit and run it across the targets whose capability plans support the fixture. ### Unified Testkit M2 Trace Parity Commit: feature commit for unified testkit trace parity Summary: * Added a normalized observable trace comparison layer to `testkit/core`. * The runner now executes every selected target for a scenario, validates each target's declared expectations, then asserts cross-target parity for call order and portable return values. * EVM ABI return words and NEAR typed host returns are compared through the scenario's expected portable type, so target-specific hex encodings do not become false parity failures. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all -- --check cargo test --manifest-path testkit/Cargo.toml -p proof-forge-testkit-core cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run ``` Known limitations: * Trace parity currently covers call order and return values only; scenario state reads, events, errors, and resource budgets are still follow-up schema work before testkit M3/M4. * `solana-sbpf-asm` is not yet wired into testkit; it remains the M3 harness. Next step: * Add `harness-solana` on top of the existing Mollusk templates so the Counter scenario runs across `evm`, `wasm-near`, and `solana-sbpf-asm`. ### Unified Testkit M2 EVM Harness Commit: feature commit for unified testkit EVM harness Summary: * Added `testkit/harness-evm`, backed by `revm`, as the second target harness for RFC 0007. * Extended `testkit/scenarios/counter.toml` so the same portable Counter scenario runs against both `wasm-near` and `evm`. * The EVM harness emits portable IR Counter runtime bytecode and artifact metadata, loads selectors from metadata, installs the runtime bytecode into an in-memory EVM account, and executes each scenario call as a committed EVM transaction with sequential nonces. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all cargo check --manifest-path testkit/Cargo.toml cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- run --target evm just testkit ``` Known limitations: * The EVM harness currently covers the portable IR Counter fixture only. * It validates scenario-level behavior through `revm`; Foundry and Anvil remain the mature EVM runtime/deploy gates for broader contracts and live local chain behavior. * Cross-target comparison is still implicit through shared expectations; an explicit trace-diff layer should be added next. Next step: * Add a target trace comparison report so `wasm-near` and `evm` outcomes are compared directly for the shared scenario, then wire the first Solana/Mollusk or sBPF runner into the same testkit interface. ### Unified Testkit M1 Skeleton Commit: feature commit for unified testkit M1 skeleton Summary: * Added the RFC 0007 `testkit/` Rust workspace with core scenario parsing, NEAR harness wiring, and the `proof-forge-testkit` runner. * Added `testkit/scenarios/counter.toml` as the first declarative scenario. * Wired `just testkit`, `just testkit-list`, and the GitHub Actions `build-test` job. Validation run: ```sh theme={null} cargo fmt --manifest-path testkit/Cargo.toml --all cargo check --manifest-path testkit/Cargo.toml cargo run --manifest-path testkit/Cargo.toml -p proof-forge-testkit -- list just testkit ``` Known limitations: * This is the M1 `wasm-near` slice only. It wraps the existing deterministic `runtime/offline-host`; EVM/revm and Solana/Mollusk are not wired yet. * Cross-target equivalence assertions start in M2 after the EVM harness lands. Next step: * Add `harness-evm` on revm, load emitted runtime bytecode plus `.evm-methods`, and compare the Counter observable trace against `wasm-near`. ## 2026-07-02 ### EVM StorageSlotPlan ToYul Slice Commit: feature commit for `StorageSlotPlan -> ToYul` Summary: * Added `ProofForge.Backend.Evm.ToYul` as the first plan-to-Yul module in the EVM semantic-plan migration. * Moved scalar storage slot expressions and map value/presence slot expressions through `StorageSlotPlan -> ToYul` while keeping the existing `IR.lean` facade and generated Yul behavior stable. * Recorded the remaining EVM semantic-plan migration TODO in the implementation backlog, including `Validate`, `Lower`, `ToYul`, `Metadata`, `EntrypointPlan`, `EventPlan`, `CrosscallPlan`, and `MetadataPlan` stages. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.ToYul ProofForge.Backend.Evm.IR just evm-plan just evm-smoke map just evm-smoke typed-map just evm-smoke typed-storage just check just diff-check ``` Known limitations: * Array slots, struct-array field slots, expression plans, statement plans, entrypoint planning, events, crosscalls, and artifact metadata still need to move behind semantic plan boundaries. * `ProofForge.Backend.Evm.IR` remains the public compatibility facade until the migrated plan paths have complete validation coverage. Next step: * Extend `StorageSlotPlan -> ToYul` to array and struct-array slot plans, then begin extracting expression and statement planning out of `IR.lean`. ### Target-Driven EVM Module Plan Commit: feature commit for EVM capability-aware module planning Summary: * Extended `ProofForge.Backend.Evm.Plan` with a target-driven `ModulePlan` that preserves the resolved `Target.CapabilityPlan` for the EVM compiler target. * Moved EVM storage/helper planning behind `buildModulePlan`, so the backend can consume target-resolved capabilities instead of rediscovering helper requirements directly during final Yul lowering. * Added `lowerModuleWithPlan` in the EVM backend. The public `lowerModule` path now builds an EVM module plan first, then renders through the existing Yul AST path. * Extended `Tests/EvmPlan.lean` to verify target id, supported and unsupported capabilities, helper requirements, storage layout, map assign-op helper requirements, and explicit rejection of a non-EVM target plan. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.Plan lake build ProofForge.Backend.Evm.IR lake env lean --run Tests/EvmPlan.lean ``` Known limitations: * ABI dispatch, event plans, crosscall plans, constructor metadata, and artifact metadata still need to move behind `ModulePlan`. * The generated Yul is intentionally unchanged in this slice. Next step: * Move storage-path Yul expression construction to consume `StorageSlotPlan` directly, then promote ABI/event/crosscall metadata into `ModulePlan`. ### Solana sBPF And SDK PR Merge Commit: merge commit for PR #2 (`Solana supprot`) Summary: * Merged the Solana sBPF assembly backend work into the current EVM-focused mainline. * Added Solana backend modules for sBPF assembly AST/printer, state layout, register allocation, syscalls, manifests, packages, and SDK extension artifacts. * Added CLI modes for emitting Solana sBPF assembly, Solana ELF artifacts, Solana SDK assembly, and Solana-focused fixture artifacts. * Added Solana examples, diagnostics, SDK tests, target-routing tests, and Solana smoke scripts. * Resolved RFC numbering against the existing EVM semantic plan RFC: EVM keeps RFC 0004, Solana sBPF is RFC 0005, and the multi-chain Token SDK is RFC 0006. Validation run: ```sh theme={null} just solana-light just docs-check just check python3 -m json.tool scripts/i18n/manifest.json >/dev/null git diff --check ``` Known limitations: * Solana Mollusk/Surfpool runtime smoke scripts remain gated on local external tools such as Mollusk, Surfpool, Node, and npm. * The merge preserves EVM semantic-plan work; deeper integration between the new Solana SDK route and the portable multi-chain planning layer remains follow-up work. Next step: * Run the available Solana smoke scripts on a machine with the Solana/sBPF toolchain installed, then decide which Solana surface should be promoted from research to CI-tracked baseline. ### EVM Semantic Plan Storage Slice Commit: feature commit for the first EVM semantic plan slice Summary: * Added `ProofForge.Backend.Evm.Plan` as the first explicit semantic planning layer between portable IR and target-specific Yul lowering. * Modeled storage layout entries, scalar storage slot plans, map value slot plans, nested map value slot plans, map presence slot plans, and helper requirements without changing generated Yul output. * Added `Tests/EvmPlan.lean` to lock scalar/map/nested-map slot planning against the existing `EvmMapProbe` and `EvmTypedMapProbe` fixtures. * Added `just evm-plan` and a GitHub Actions step so the plan slice is checked independently before broader EVM smokes. Validation run: ```sh theme={null} just evm-plan ``` Known limitations: * The existing Yul generator still owns actual rendering; this slice creates the semantic structures and tests that later lowering can migrate onto. * The first plan slice covers scalar slots and consecutive `mapKey` paths only. Arrays, structs, ABI dispatch, event/crosscall helpers, and artifact metadata planning remain follow-up work. Next step: * Refactor the current EVM storage path lowering to consume plan nodes while preserving golden Yul output, then broaden the plan to arrays and flat storage structs. ### EVM Nested Map Storage Paths Commit: feature commit for EVM nested map storage paths Summary: * Extended EVM portable IR storage-path type checking so map-backed state accepts one or more consecutive `mapKey` segments when every key expression matches the map key type. * Lowered nested map value slots by folding the existing Solidity-style mapping helper, for example `keccak256(inner || keccak256(outer || slot))`. * Lowered nested map write and compound assignment paths so the final key's ProofForge-managed presence slot is marked alongside the value slot. * Extended `EvmMapProbe` with U64 nested map path lifecycle and dynamic-key coverage, and extended `EvmTypedMapProbe` with U32 nested map path coverage plus dispatcher range-guard checks. * Kept mixed map/aggregate storage paths as explicit diagnostics rather than silently lowering partial paths. Validation run: ```sh theme={null} lake build proof-forge just evm-smoke map just evm-smoke typed-map just evm-diagnostics just evm-coverage just docs-check just diff-check ``` Known limitations: * Nested map paths currently model EVM nested mapping slots over a single declared `Map` state by using consecutive keys of the same key type. * Mixed map/array/struct aggregate paths and non-word or aggregate map key/value shapes remain explicit unsupported surfaces. Next step: * Continue shrinking the remaining EVM storage surface around aggregate storage paths and broader ABI-facing storage-backed values. ### EVM Nested Fixed-Array Event Aggregates Commit: feature commit for EVM nested fixed-array event aggregates Summary: * Extended portable IR EVM event signature generation so nested fixed arrays are rendered recursively as Solidity-style event types such as `uint64[2][2]` and `(uint64,uint64)[2][2]`. * Extended event data-word lowering so nested fixed-array event fields flatten recursively into ABI-style words when their leaves are scalar words or flat structs. * Added `EventProbe` entrypoints for `MatrixEvent(uint64[2][2])`, `PairMatrixEvent((uint64,uint64)[2][2])`, `IndexedMatrix(uint64[2][2],uint64)`, and `IndexedPairMatrix((uint64,uint64)[2][2],uint64)`. * Tightened diagnostics so nested fixed arrays whose leaves are unsupported or non-flat still fail before Yul generation with explicit errors. Validation run: ```sh theme={null} just evm-smoke event ``` * Generated reproducible EventProbe Yul and runtime bytecode with `solc --strict-assembly`. * Validated new selector/event ABI metadata through `scripts/evm/validate-artifact-metadata.py`. * Foundry ran 24 EventProbe recorded-log tests, including nested scalar and nested flat-struct fixed-array data flattening plus indexed aggregate topic hashing. Known limitations: * Aggregate event fields with unsupported leaves, non-flat struct leaves, or richer first-class event declarations remain explicit unsupported surfaces for portable IR EVM. Next step: * Continue shrinking the EVM aggregate surface around remaining storage and ABI edge cases while keeping unsupported shapes diagnostic-first. ### EVM Entrypoint ABI Artifact Metadata Commit: `feat: record EVM entrypoint ABI metadata` Summary: * Portable IR EVM bytecode artifacts and deploy manifests now include structured `abi.entrypoints` metadata for selector-facing entrypoints. * Entrypoint metadata records the Solidity-style selector signature, parameter ABI types, flattened calldata word types/counts, return ABI type, flattened return word types/counts, and preserves the original IR type names. * `scripts/evm/validate-artifact-metadata.py` now validates entrypoint selectors with `cast sig`, while `scripts/evm/abi-aggregate-ir-smoke.sh` locks aggregate calldata/return word layouts through `--expect-entrypoint-abi`. Validation run: ```sh theme={null} lake build proof-forge scripts/evm/abi-aggregate-ir-smoke.sh ``` Known limitations: * The metadata describes the current static ABI-word surface. Dynamic ABI values remain an explicit unsupported surface for portable IR EVM. Next step: * Continue tightening metadata validation around deployment-facing manifests and expand first-class ABI schema coverage as the portable IR grows. ### EVM Event ABI Artifact Metadata Commit: `feat: record EVM event ABI metadata` Summary: * Portable IR EVM bytecode artifacts and deploy manifests now include `abi.events` entries for emitted events. * Event metadata records the Solidity-style event signature, `topic0`, indexed fields, non-indexed data fields, flattened ABI word types, and per-field topic/data encoding. * `scripts/evm/validate-artifact-metadata.py` validates event topics with `cast keccak`, and `scripts/evm/event-ir-smoke.sh` now locks all EventProbe event signatures through `--expect-event`. Validation run: ```sh theme={null} lake build proof-forge scripts/evm/event-ir-smoke.sh python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py ``` Known limitations: * Event metadata is emitted for portable IR modules; richer first-class event declarations remain an explicit unsupported surface. Next step: * Continue promoting ABI-facing metadata from smoke fixtures into a stable target manifest schema shared by EVM deployment tooling. ### EVM Anvil Chain Profile Deploy-Run Validation Commit: `feat: validate Anvil chain profiles` Summary: * Added `anvil-local` as a lookup-only EVM chain profile for local Foundry Anvil deployments on chain id `31337`. * `scripts/evm/anvil-deploy-smoke.sh` now regenerates Counter with `--evm-chain-profile anvil-local` by default when using the default Anvil chain id. * `proof-forge-deploy-run.json` now links the deploy manifest chain profile, and `scripts/evm/validate-deploy-run.py` validates that the profile, deployment chain id, actual Anvil chain id, and creation transaction evidence agree. Validation run: ```sh theme={null} lake build ProofForge.Target.Registry lake env lean --run Tests/TargetRegistry.lean python3 -m py_compile scripts/evm/validate-deploy-run.py bash -n scripts/evm/anvil-deploy-smoke.sh scripts/evm/anvil-deploy-smoke.sh ``` Known limitations: * `anvil-local` is intentionally a local validation profile; it does not imply public RPC broadcast support. Next step: * Promote profile-aware deploy-run generation into a first-class deploy command that can consume any supported EVM chain profile. ### EVM Creation Transaction Deploy-Run Artifact Commit: `feat: record EVM creation transactions` Summary: * Anvil deploy smoke now records the `eth_getTransactionByHash` creation transaction JSON alongside the `cast send --create` receipt. * `proof-forge-deploy-run.json` links that creation transaction artifact with path, byte size, and SHA-256 metadata. * `scripts/evm/validate-deploy-run.py` now validates that the creation transaction hash, sender, null `to`, block metadata, and initcode `input` match the deploy receipt and generated `.init.bin`. Validation run: ```sh theme={null} python3 -m py_compile scripts/evm/validate-deploy-run.py bash -n scripts/evm/anvil-deploy-smoke.sh scripts/evm/anvil-deploy-smoke.sh just evm-all ``` Known limitations: * This records a local Anvil creation transaction and receipt, not a signed raw transaction artifact or public RPC broadcast workflow. Next step: * Promote the deploy-run artifact shape into a first-class deploy/broadcast command that consumes `proof-forge-deploy.json`. ### EVM ABI Method Signature Metadata Commit: `feat: record EVM method signatures` Summary: * SDK `.evm-methods` sidecars now preserve the original Solidity method signature in `abi.methods[].signature` for EVM artifact metadata and deploy manifests. * Manual `--method selector:fn:argc:view|update` specs remain supported; those method entries use `null` signature metadata. * EVM metadata validators now check selector shape, duplicate method and entrypoint selectors, generated Yul function names, signature syntax, and signature/arg-count consistency. * SDK example builds and the Anvil deploy smoke now require method signatures in metadata validation. Validation run: ```sh theme={null} lake build proof-forge python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py bash -n scripts/evm/build-examples.sh bash -n scripts/evm/anvil-deploy-smoke.sh scripts/evm/build-examples.sh scripts/evm/anvil-deploy-smoke.sh ``` Known limitations: * The validators check selector format and method signature metadata, while the selector derivation itself still comes from Foundry `cast sig` during compilation. Next step: * Continue strengthening ABI-facing artifact checks and close remaining deploy/broadcast metadata gaps. ### EVM Constructor Diagnostic Coverage Commit: `test: cover EVM constructor CLI diagnostics` Summary: * Extended `scripts/evm/diagnostic-smoke.sh` beyond portable IR diagnostics to cover EVM constructor artifact-boundary CLI diagnostics. * The gate now locks unsupported dynamic constructor ABI types, missing constructor values, duplicate typed values, mixed typed/raw constructor sources, integer overflow, and malformed address-width inputs. * This turns the constructor value negative cases from one-off manual checks into CI-tracked `just evm-diagnostics` coverage. Validation run: ```sh theme={null} bash -n scripts/evm/diagnostic-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Constructor value encoding is still intentionally limited to static one-word ABI types; dynamic constructor ABI values remain unsupported with explicit diagnostics. Next step: * Continue closing the remaining EVM ABI/backend gaps, especially dynamic ABI surfaces and deploy/broadcast artifacts. ### EVM Typed Constructor Value Encoding Commit: `feat: encode EVM constructor values` Summary: * Added `--evm-constructor-arg ` for EVM bytecode modes. * Typed constructor args are ABI-encoded from the declared `--evm-constructor-param ` schema and support `uint256`, `uint64`, `uint32`, `bool`, `bytes32`, and `address`. * Constructor arg metadata now records whether the ABI blob came from typed CLI args or raw `--evm-constructor-args-hex`. * Validators accept and can assert constructor arg source, and Anvil deploy smoke now defaults to typed `initial=123` input for Counter. * CLI validation rejects missing typed values, duplicate typed values, out-of-range integer values, and mixing typed values with raw constructor hex. Validation run: ```sh theme={null} lake build proof-forge python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/validate-deploy-run.py bash -n scripts/evm/anvil-deploy-smoke.sh lake env proof-forge --evm-bytecode --root . --module contract --evm-constructor-param initial:uint256 --evm-constructor-arg initial=123 ... python3 scripts/evm/validate-artifact-metadata.py --expect-constructor-args-source=--evm-constructor-arg ... python3 scripts/evm/validate-deploy-manifest.py --expect-constructor-args-source=--evm-constructor-arg ... ``` Known limitations: * Constructor value encoding is limited to static one-word ABI types; dynamic constructor ABI types are still unsupported. * This still emits deployable initcode and local Anvil deploy-run artifacts, not signed transaction/broadcast artifacts for public RPC networks. Next step: * Add first-class EVM deploy/broadcast commands that consume the deploy manifest, or continue closing remaining non-dynamic EVM backend gaps. ### EVM Constructor ABI Schema Metadata Commit: `feat: record EVM constructor ABI schema` Summary: * Added `--evm-constructor-param ` for EVM bytecode modes. * Constructor params are recorded under `abi.constructor.params` in both `proof-forge-artifact.json` and `proof-forge-deploy.json` using static 32-byte ABI-word metadata. * Validators now check constructor ABI schema shape, supported static-word types, expected parameters, and constructor-argument byte length. * The Anvil deploy smoke now regenerates Counter with `--evm-constructor-param initial:uint256`, records `constructorAbi` in `Counter.proof-forge-deploy-run.json`, and validates it against the deploy manifest. Validation run: ```sh theme={null} lake build python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/validate-deploy-run.py bash -n scripts/evm/anvil-deploy-smoke.sh lake env proof-forge --evm-bytecode --root . --module contract --evm-constructor-param initial:uint256 --evm-constructor-args-hex 0x000000000000000000000000000000000000000000000000000000000000007b ... scripts/evm/anvil-deploy-smoke.sh just check just evm-all just psy-golden-sources git diff --check ``` Known limitations: * ProofForge records and validates static constructor ABI schema, but does not yet parse typed constructor values or ABI-encode them from CLI inputs. * Dynamic constructor ABI types remain out of scope for the current EVM schema slice. Next step: * Add typed constructor value parsing/encoding or move to a first-class EVM deploy/broadcast command that consumes the deploy manifest. ### Just-Based CI Command Entry Commit: feature commit for just-based CI command entry Summary: * Kept target-specific implementation logic in `scripts/`, but made the root `justfile` the shared developer and CI command entrypoint. * Installed pinned `just` 1.48.0 in GitHub Actions and replaced duplicated CI command blocks with existing recipes such as `just build`, `just target-registry`, `just docs-check`, `just psy-golden-sources`, and `just evm-smoke `. * Preserved separate GitHub Actions steps for EVM/Psy gates so CI failures stay easy to locate. * Updated README, development standards, validation gates, and Chinese mirrors to document the split between `just` orchestration and underlying scripts. Validation run: ```sh theme={null} ruby -e 'require "yaml"; YAML.load_file(".github/workflows/ci.yml"); puts "workflow yaml ok"' just --list just check just psy-golden-sources just --dry-run git diff --check ``` Known limitations: * CI now requires `just` installation before invoking common gate recipes. * Direct scripts remain supported because they are still the target-specific implementation surface. Next step: * Consider grouping future target recipes by imported `just` modules if the root `justfile` becomes hard to scan. ### EVM Constructor Args Initcode Tail Commit: feature commit for EVM constructor args initcode tail Summary: * Added `--evm-constructor-args-hex ` to EVM bytecode modes. * The CLI now normalizes ABI-encoded constructor args, appends them to generated `.init.bin` creation bytecode, and records the argument blob in `proof-forge-deploy.json` with hex, byte size, SHA-256, and source metadata. * Updated EVM metadata, deploy-manifest, and deploy-run validators so they parse the initcode header as `header + runtime + constructorArgs` instead of assuming the initcode ends at the runtime bytecode. * Extended `scripts/evm/anvil-deploy-smoke.sh` so CI deploys Counter initcode with a deterministic non-empty constructor-argument tail by default and records those args in `Counter.proof-forge-deploy-run.json`. Validation run: ```sh theme={null} lake build python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/validate-deploy-run.py scripts/evm/build-examples.sh scripts/evm/anvil-deploy-smoke.sh ``` Result: * No-argument SDK example builds still emit valid metadata and deploy manifests. * Counter Anvil deploy smoke regenerated `Counter.init.bin` with a 32-byte constructor argument blob (`0x...007b`), deployed it with `cast send --create`, and validated that the deployed runtime code still matches `Counter.bin`. * The deploy-run artifact records the constructor args and the Counter lifecycle still returned `0`, then `99`, `100`, and `99`. Known limitations: * Constructor args are accepted as an explicit ABI-encoded hex blob; ProofForge does not yet generate constructor ABI schemas or encode named constructor parameters from IR. * This still validates on local Anvil, not a live public RPC broadcast. Next step: * Add a first-class deployment command or broadcast artifact that consumes the deploy manifest, selected chain profile, private-key/wallet configuration, and constructor args without shell-script-specific glue. ### EVM Anvil Deploy-Run Smoke Commit: `feat: validate EVM initcode deployment on Anvil` Summary: * Added `scripts/evm/anvil-deploy-smoke.sh`, which starts a local Anvil chain and deploys generated `Counter.init.bin` with `cast send --create`. * The smoke records the creation transaction receipt, deployed address, local Anvil network id, referenced deploy manifest, initcode, runtime bytecode, and Counter lifecycle call results in `build/anvil-deploy-smoke/Counter.proof-forge-deploy-run.json`. * Added `scripts/evm/validate-deploy-run.py` to validate deploy-run artifacts, including receipt status, transaction/deployer consistency, deployed runtime code hash/size, and `get`/`set`/`increment`/`decrement` JSON-RPC behavior. * Wired the new smoke into `just evm-anvil-deploy`, `just evm-all`, and CI. Validation run: ```sh theme={null} python3 -m py_compile scripts/evm/validate-deploy-run.py scripts/evm/anvil-deploy-smoke.sh ``` Result: * Anvil chain id `31337` started locally. * `Counter.init.bin` deployed to `0x5fbdb2315678afecb367f032d93f642f64180aa3` with a successful creation receipt. * The on-chain deployed code matched `build/evm/Counter.bin`. * Counter JSON-RPC lifecycle returned `0`, then `99`, `100`, and `99`. Known limitations: * This is a local Anvil deploy-run artifact, not a live public RPC broadcast. * Constructor arguments remain empty. * Explorer verification and wallet UX are still future work. Next step: * Extend deploy-run generation toward chain-profile-aware live RPC deployment and constructor argument encoding, while keeping Anvil as the deterministic CI smoke. ### EVM Chain Profile Deploy Metadata Commit: `feat: record EVM chain profile deploy metadata` Summary: * Added `--evm-chain-profile ` for EVM bytecode modes. * Resolved EVM chain profiles from the target registry and recorded the selected profile in `proof-forge-deploy.json`, including profile id, chain id, RPC URLs, native gas symbol, explorer, verifier, and notes. * Extended the deploy `deployment` block with profile id, chain id, network name, RPC URLs, explorer/verifier metadata, and explicit `broadcastArtifact: null`. * Strengthened EVM metadata/deploy validators so selected profiles must match deployment fields and unselected profiles remain explicit `null`/empty fields. * Updated `AbiScalarProbe` EVM smoke to validate `robinhood-chain-testnet` and chain id `46630`. Validation run: ```sh theme={null} lake build python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/abi-scalar-ir-smoke.sh python3 scripts/evm/validate-deploy-manifest.py --root . --expect-fixture AbiScalarProbe --expect-source-kind portable-ir --expect-chain-profile robinhood-chain-testnet --expect-chain-id 46630 build/ir/AbiScalarProbe.proof-forge-deploy.json ``` Result: * `AbiScalarProbe.proof-forge-deploy.json` records `chainProfile.id: robinhood-chain-testnet`, `deployment.profileId: robinhood-chain-testnet`, and `deployment.chainId: 46630`. * Foundry ABI scalar smoke still ran 2 runtime tests successfully. Known limitations: * The manifest is still a deployment plan only. * Transaction signing, Foundry/Anvil broadcast JSON, deployed address recording, and explorer verification remain future work. Next step: * Generate a Foundry script or broadcast-oriented artifact from the deploy manifest, then validate it against Anvil without relying on live RPC. ### EVM Deploy Initcode Artifacts Commit: `feat: emit EVM deploy initcode artifacts` Summary: * Extended every EVM bytecode build to emit a sibling `.init.bin` deployable creation bytecode artifact in addition to the existing runtime `.bin`. * Updated `proof-forge-artifact.json` and `proof-forge-deploy.json` so EVM metadata records the initcode artifact, `creation.mode: init-code`, and `validation.initCodeGeneration: passed`. * Strengthened both EVM metadata validators to parse the initcode `PUSH/CODECOPY/RETURN` header and prove it copies and returns the exact referenced runtime bytecode artifact. * Refreshed English/Chinese EVM metadata docs, validation gates, and backlog notes to distinguish deployable initcode from future transaction broadcast manifests. Validation run: ```sh theme={null} lake build python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/build-examples.sh python3 scripts/evm/validate-deploy-manifest.py --root . --expect-fixture AbiScalarProbe --expect-source-kind portable-ir build/ir/AbiScalarProbe.proof-forge-deploy.json python3 scripts/evm/validate-deploy-manifest.py --root . --expect-fixture Counter.lean --expect-source-kind lean-sdk build/evm/Counter.proof-forge-deploy.json scripts/evm/foundry-smoke.sh ``` Result: * `AbiScalarProbe` generated `AbiScalarProbe.init.bin` and passed Foundry scalar ABI runtime checks. * SDK examples generated `.init.bin` artifacts for Counter, ArrayExample, SimpleToken, ERC20, Ownable, Pausable, and VerifiedVault; the validator accepted both small and multi-byte-length runtimes. * Foundry ran 5 runtime smoke tests, including deploying the generated Counter `.init.bin` through EVM `create` and then running the Counter lifecycle. Known limitations: * Constructor arguments are still empty. * Chain profile selection, signed/raw transaction generation, broadcast JSON, deployed address recording, and explorer verification remain future work. * Most Foundry smoke coverage still installs runtime bytecode with `vm.etch` for fast runtime checks; Counter now also has a real initcode `create` path. Next step: * Continue toward real deployment manifests by adding chain-profile selection and a Foundry/Anvil broadcast artifact, or return to the remaining EVM IR unsupported surfaces such as dynamic ABI values. ### EVM IR Hash Aggregate ABI Leaves Commit: `test: cover EVM hash aggregate ABI leaves` Summary: * Extended `EvmAbiAggregateProbe` with `HashPair` and `Hash` fixed-array ABI entrypoints: `echo_hash_pair((bytes32,bytes32))`, `make_hash_pair(bytes32,bytes32)`, `pick_hash(bytes32[2])`, and `make_hash_array(bytes32,bytes32)`. * Validated that `Hash` leaves flatten as Solidity `bytes32` words inside flat structs and fixed arrays for ABI-facing calldata and return data. * Refreshed the `EvmAbiAggregateProbe` golden Yul, selector metadata checks, Foundry ABI decode checks, coverage table, English/Chinese EVM target docs, validation gates, and backlog notes. Validation run: ```sh theme={null} scripts/evm/abi-aggregate-ir-smoke.sh ``` Result: * `EvmAbiAggregateProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 3 ABI aggregate tests, including `HashPair` calldata/return-data, `bytes32[2]` calldata/return-data, and short `bytes32[2]` calldata rejection. Known limitations: * Dynamic ABI values remain outside the portable IR EVM v0 surface. * Rich ABI tuples beyond flat word aggregates remain explicit future work. * Storage-backed aggregate ABI returns stay covered only by the fixed word-array and flat struct-array cases in the dedicated storage probes. Next step: * Continue shrinking aggregate ABI/crosscall gaps, or decide whether richer dynamic ABI values require a portable IR extension first. ## 2026-07-01 ### EVM IR Typed Scalar Event Fields Commit: feature commit for EVM IR typed scalar event fields Summary: * Extended `EventProbe` with typed scalar event entrypoints: `emit_typed_scalar_event(bool,uint32,bytes32)` and `emit_indexed_typed_scalar_event(bool,uint32,bytes32,uint256)`. * Validated `Bool`, `U32`, and `Hash` event data fields and indexed topics, including `Bool`/`U32` calldata range guards before the event lowering runs. * Refreshed `EventProbe` golden Yul, metadata selector checks, Foundry recorded-log checks, coverage, English/Chinese EVM target docs, validation gates, and implementation backlog notes. Validation run: ```sh theme={null} scripts/evm/event-ir-smoke.sh ``` Result: * `EventProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 20 EventProbe tests, including typed scalar data/topic checks and malformed `Bool`/`U32` calldata rejection. Known limitations: * Indexed event fields remain limited to three fields after the signature topic. * Nested fixed arrays, non-flat structs, and unsupported aggregate leaves remain explicit diagnostics for event fields. * First-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking the EVM event gap around richer event declarations, or move to another unsupported EVM capability surface. ### EVM IR Multi-Topic Indexed Events Commit: feature commit for EVM IR multi-topic indexed events Summary: * Extended `EventProbe` with two scalar indexed-event entrypoints: `emit_two_indexed_event(uint256,uint256,uint256)` and `emit_three_indexed_event(uint256,uint256,uint256,uint256)`. * Validated that `eventEmitIndexed` generates `log3` for two indexed fields and `log4` for three indexed fields, with ordered scalar topics and one non-indexed data word. * Refreshed `EventProbe` golden Yul, metadata selector checks, Foundry recorded-log checks, coverage, English/Chinese EVM target docs, validation gates, and implementation backlog notes. Validation run: ```sh theme={null} scripts/evm/event-ir-smoke.sh ``` Result: * `EventProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 17 EventProbe tests, including `log3` and `log4` scalar indexed event coverage. Known limitations: * Indexed event fields remain limited to three fields after the signature topic. * Nested fixed arrays, non-flat structs, and unsupported aggregate leaves remain explicit diagnostics for event fields. * First-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking the EVM event gap around richer event declarations, or move to another unsupported EVM capability surface. ### EVM IR Storage-Backed Event Fixed Arrays Commit: feature commit for EVM IR storage-backed event fixed arrays Summary: * Extended `EventProbe` with `storedValues` and `storedPairs` fixed storage arrays plus four entrypoints: `emit_storage_array_event(uint256,uint256)`, `emit_storage_pair_array_event(uint256,uint256,uint256,uint256)`, `emit_indexed_storage_array_event(uint256,uint256,uint256)`, and `emit_indexed_storage_pair_array_event(uint256,uint256,uint256,uint256,uint256)`. * Validated that storage array reads and storage array struct field reads can feed scalar fixed-array and fixed-array-of-flat-struct event aggregates. * Refreshed `EventProbe` golden Yul, metadata selector checks, Foundry recorded-log checks, coverage, English/Chinese EVM target docs, validation gates, and implementation backlog notes. Validation run: ```sh theme={null} scripts/evm/event-ir-smoke.sh ``` Result: * `EventProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 15 EventProbe tests, including storage-backed fixed-array data flattening and storage-backed fixed-array indexed topic hashing. Known limitations: * Indexed event fields remain limited to three fields after the signature topic. * Nested fixed arrays, non-flat structs, and unsupported aggregate leaves remain explicit diagnostics for event fields. * First-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking the EVM event gap around richer event declarations, or move to another unsupported EVM capability surface. ### EVM IR Storage-Backed Event Aggregates Commit: feature commit for EVM IR storage-backed aggregate events Summary: * Extended `EventProbe` with a flat scalar storage struct state and two entrypoints: `emit_storage_pair_event(uint256,uint256)` and `emit_indexed_storage_pair_event(uint256,uint256,uint256)`. * Validated the existing storage-backed event lowering path where a whole flat struct is written with `storageScalarWrite`, read with `storageScalarRead`, flattened into non-indexed event data words, or flattened and hashed into an indexed aggregate topic. * Refreshed `EventProbe` golden Yul, metadata selector checks, Foundry recorded-log checks, coverage, English target docs, Chinese target docs, validation gates, and implementation backlog notes. Validation run: ```sh theme={null} scripts/evm/event-ir-smoke.sh ``` Result: * `EventProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 11 EventProbe tests, including `StoragePairEvent` data flattening from storage reads and `IndexedStoragePair` topic hashing from storage reads. Known limitations: * Indexed event fields remain limited to three fields after the signature topic. * Nested fixed arrays, non-flat structs, and unsupported aggregate leaves remain explicit diagnostics for event fields. * First-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking the EVM event gap around richer event declarations, or move to another unsupported EVM capability surface. ### EVM IR Indexed Aggregate Event Topics Commit: feature commit for EVM IR indexed aggregate event topics Summary: * Extended `eventEmitIndexed` lowering so supported aggregate indexed fields no longer pretend to be scalar topics. Flat structs and fixed arrays whose elements are flat structs now flatten to ABI-style 32-byte words and use `keccak256` over those words as the indexed topic. * Preserved direct scalar indexed topics for `U32`, `U64`, `Bool`, and `Hash`. * Extended `EventProbe` with `emit_indexed_pair_event`, `emit_indexed_array_event`, and `emit_indexed_pair_array_event`, covering `IndexedPair((uint64,uint64),uint64)` and `IndexedArray(uint64[2],uint64)` and `IndexedPairArray((uint64,uint64)[2],uint64)`. * Replaced the old flat-aggregate indexed diagnostic with a nested aggregate indexed diagnostic, so unsupported event shapes still fail explicitly instead of lowering partially. * Refreshed golden Yul, artifact metadata selector checks, Foundry recorded-log checks, EVM diagnostics, coverage, English target docs, Chinese target docs, and implementation backlog notes. Validation run: ```sh theme={null} lake build scripts/evm/event-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Result: * `EventProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 9 EventProbe tests, including scalar indexed topics, flat struct indexed topic hashes, scalar fixed-array indexed topic hashes, fixed-array-of-flat-struct indexed topic hashes, aggregate data flattening, selector dispatch, and unknown-selector revert behavior. Known limitations: * Indexed event fields remain limited to three fields after the signature topic. * Nested fixed arrays, non-flat structs, and unsupported aggregate leaves remain explicit diagnostics for event fields. * First-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking the EVM event gap around richer event declarations, or move to the next uncovered EVM capability surface. ### EVM IR Nested Local Struct Arrays Commit: feature commit for EVM IR nested local struct arrays Summary: * Extended portable IR EVM local fixed-array lowering so nested fixed arrays can use flat struct leaves, expanding every nested element field into deterministic Yul locals such as `grid[1][0].age`. * Added static and dynamic nested struct field reads through nested local-array getter helpers, plus nested mutable field assignment and numeric compound assignment through bounds-checked `switch` lowering. * Added nested whole-local assignment from another local array and from self-referential nested array literals, preserving RHS snapshot semantics. * Extended `EvmStructArrayValueProbe` with `nested_struct_array_sum`, `nested_struct_array_dynamic_pick`, `nested_struct_array_update`, `nested_struct_array_whole_assign`, and `nested_struct_array_self_assign`. * Refreshed golden Yul, artifact metadata selector checks, Foundry smoke tests, EVM coverage manifest entries, English target docs, Chinese target docs, and implementation backlog notes. Validation run: ```sh theme={null} lake build scripts/evm/struct-array-value-ir-smoke.sh ``` Result: * `EvmStructArrayValueProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 14 StructArrayValueProbe tests, including nested flat-struct field reads, nested field mutation, nested whole assignment, RHS snapshotting, dynamic out-of-bounds reverts, and unknown-selector revert behavior. Known limitations: * Nested local fixed arrays are still limited to scalar word leaves or flat struct leaves. Non-flat struct leaves and other unsupported aggregate leaves remain explicit diagnostics. Next step: * Continue shrinking the EVM aggregate gap around unsupported nested aggregate leaves, richer event schemas, or broader cross-call return data. ### EVM IR Nested Struct Crosscall Fixed Arrays Commit: feature commit for EVM IR nested struct crosscall arrays Summary: * Extended typed crosscall aggregate word-shape validation so nested fixed arrays can use flat struct leaves such as `RemotePair[2][2]`, while non-flat struct leaves still fail with explicit diagnostics. * Added `EvmCrosscallProbe` entrypoints for `RemotePair[2][2]` arguments and direct entrypoint returns across normal, value-bearing, static, and delegate typed calls. * Refreshed `EvmCrosscallProbe.golden.yul`, metadata selector expectations, and the Foundry smoke harness with `Pair[2][2]` callee helpers. * Updated the EVM coverage manifest and target/validation docs to distinguish supported flat struct leaves from unsupported non-flat struct leaves. Validation run: ```sh theme={null} lake build scripts/i18n/check-sync.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/crosscall-ir-smoke.sh git diff --check ``` Result: * `EvmCrosscallProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 73 CrosscallProbe tests, including nested fixed-array flat-struct arguments and returns in normal, value-bearing, static, and delegate modes. Known limitations: * Dynamic ABI values, nested local fixed-array mutation beyond the current local-array surface, nested crosscall fixed arrays with non-flat or unsupported leaves, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking the EVM aggregate gap around dynamic ABI data, richer cross-call return data, or unsupported nested aggregate leaves. ### EVM IR Storage-Backed Aggregate ABI Returns Commit: feature commit for EVM IR storage-backed aggregate ABI returns Summary: * Extended `EvmStorageArrayProbe` with `return_values()`, which writes U64 storage-array elements, reads them back through `storageArrayRead`, and encodes those reads as a fixed-array ABI return. * Extended `EvmStorageStructProbe` with `return_points()`, which writes fields in a fixed storage array of flat structs, reads them back through `storageArrayStructFieldRead`, and encodes those reads as a fixed-array-of-struct ABI return. * Refreshed both storage probe golden Yul snapshots and metadata selector expectations. * Added Foundry ABI decoding checks for `uint256[3]` and `Point[2]` returns, while still validating the raw storage slots with `vm.load`. Validation run: ```sh theme={null} lake build scripts/i18n/check-sync.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/storage-array-ir-smoke.sh scripts/evm/storage-struct-ir-smoke.sh git diff --check ``` Result: * `EvmStorageArrayProbe` generated reproducible Yul and runtime bytecode, and Foundry ran 7 tests including the new storage-backed fixed-array return. * `EvmStorageStructProbe` generated reproducible Yul and runtime bytecode, and Foundry ran 12 tests including the new storage-backed fixed-array-of-struct return. Known limitations: * This covers fixed-size word arrays and fixed arrays of flat structs assembled from storage reads. Dynamic ABI values, richer storage-backed aggregate shapes, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking the EVM ABI/storage gap around dynamic ABI data, richer aggregate storage shapes, or return data that cannot be represented as a static word sequence. ### EVM IR Nested Crosscall Fixed Arrays Commit: `fb0828b` (`feat: support nested EVM crosscall arrays`) Summary: * Extended typed crosscall aggregate lowering so nested scalar fixed arrays such as `Array,2>` flatten to ABI words for normal, value-bearing, static, and delegate typed calls. * Added `EvmCrosscallProbe` entrypoints for nested scalar fixed-array arguments and direct entrypoint returns across all four call modes. * At this milestone, kept nested fixed arrays with struct or other non-scalar leaves as explicit unsupported diagnostics; flat struct leaves were covered by a later follow-up. * Refreshed `EvmCrosscallProbe.golden.yul`, metadata selector expectations, and the Foundry smoke harness with `uint64[2][2]` callee helpers. Validation run: ```sh theme={null} lake build lake env lean --run Tests/TargetRegistry.lean scripts/i18n/check-sync.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/crosscall-ir-smoke.sh git diff --check ``` Result: * `EvmCrosscallProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 65 CrosscallProbe tests, including nested scalar fixed-array arguments and returns in normal, value-bearing, static, and delegate modes. * GitHub Actions run `28514575022` passed on `main`. Known limitations: * Dynamic ABI values, nested local fixed-array mutation beyond the current local-array surface, nested crosscall fixed arrays with non-flat or unsupported leaves, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking the EVM aggregate gap around dynamic ABI data, storage backed aggregate ABI surfaces, or richer cross-call return data. ### EVM IR Nested Fixed-Array ABI Commit: feature commit for EVM IR nested fixed-array ABI Summary: * Extended EVM ABI word flattening for entrypoint parameters and returns from flat fixed arrays to nested scalar fixed arrays such as `Array,2>`. * Added deterministic flattened Yul local names for nested ABI array words and static nested index reads such as `matrix[0][1]`. * Extended `EvmAbiAggregateProbe` with `sum_matrix`, `make_matrix`, and `sum_small_matrix` entrypoints covering nested `U64`/`U32` ABI calldata, return-data encoding, and range guards. * Kept typed crosscall nested aggregate arrays explicitly unsupported with crosscall-specific diagnostics instead of silently inheriting ABI entrypoint support. Validation run: ```sh theme={null} lake build scripts/evm/diagnostic-smoke.sh scripts/evm/abi-aggregate-ir-smoke.sh ``` Result: * `EvmAbiAggregateProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry validated nested fixed-array parameters, nested fixed-array returns, malformed nested calldata length checks, and nested `U32` range guards. * EVM diagnostics now keep zero-length arrays, non-flat struct fields, nested crosscall aggregate arrays, and malformed crosscall surfaces explicit. Known limitations: * Nested fixed-array support is currently ABI-entrypoint focused. * Dynamic ABI values, nested local fixed-array mutation, nested crosscall aggregate arrays, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking the EVM aggregate gap around nested crosscall aggregates or dynamic ABI data. ### EVM IR Contract Creation Commit: feature commit for EVM IR contract creation Summary: * Added portable IR `crosscallCreate` and `crosscallCreate2` expressions for EVM contract creation from fixed init-code hex. * Lowered creation expressions to deterministic Yul helpers that write init code into memory, call `create(value, offset, length)` or `create2(value, offset, length, salt)`, revert on zero-address failure, and return the deployed address word. * Extended `EvmCrosscallProbe` with `deploy_create` and `deploy_create2` entrypoints using tiny init code that deploys a runtime returning U256 `42`. * Kept non-EVM target behavior explicit by adding Psy unsupported diagnostics for both creation expressions. Validation run: ```sh theme={null} lake build ProofForge.IR.Examples.EvmCrosscallProbe scripts/evm/diagnostic-smoke.sh scripts/psy/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/psy/check-ir-coverage-manifest.py scripts/evm/crosscall-ir-smoke.sh ``` Result: * `EvmCrosscallProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 57 CrosscallProbe tests, including `create` deployment, deterministic `create2` address validation, and calls into the deployed runtime. * EVM diagnostics now cover bad creation value type, malformed init-code hex, and bad `create2` salt type; Psy diagnostics cover unsupported creation nodes. Known limitations: * Creation init code is currently embedded as fixed hex in the IR expression. * Dynamic constructor arguments, artifact-linked init code, creation manifests, live transaction broadcasting, and variable-length cross-call return data remain future EVM IR work. Next step: * Continue closing EVM call-surface gaps around artifact-linked creation or variable-length ABI data. ### EVM IR Struct-Array Crosscall Aggregates Commit: feature commit for EVM IR struct-array crosscall aggregates Summary: * Extended the existing typed crosscall aggregate path to fixed arrays of flat structs. * Added `EvmCrosscallProbe` entrypoints for fixed-array-of-flat-struct typed arguments and direct aggregate returns across normal, value-bearing, static, and delegate call modes. * Reused the ABI-static flattening policy: `RemotePair[2]` lowers to four ABI words, preserving Bool and U32 return guards for every decoded element field. * Refreshed golden Yul, artifact metadata entrypoint expectations, Foundry callee fixtures, and coverage/target validation docs. Validation run: ```sh theme={null} lake build ProofForge.IR.Examples.EvmCrosscallProbe scripts/evm/crosscall-ir-smoke.sh ``` Result: * `EvmCrosscallProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 55 CrosscallProbe tests, including fixed-array-of-flat-struct arguments and returns in normal/value/static/delegate modes. * Metadata validation now checks all new struct-array crosscall selectors. Known limitations: * Aggregate crosscall arguments and returns remain limited to ABI-static flat shapes. * Nested dynamic arrays, variable-length return data, and artifact-linked creation remain future EVM IR work. Next step: * Continue closing the remaining EVM call-surface gaps around artifact-linked creation or variable-length ABI data. ### EVM IR Aggregate Crosscall Arguments Commit: feature commit for EVM IR aggregate crosscall arguments Summary: * Extended typed crosscall argument lowering beyond scalar words for normal, value-bearing, static, and delegate typed calls. * Reused the EVM ABI flattening rules for flat struct and scalar fixed-array arguments, so helper arity now reflects the ABI word count rather than the surface IR argument count. * Made crosscall helper discovery type-env aware, allowing let-bound local structs and fixed arrays to request the correct generated helper. * Extended `EvmCrosscallProbe` with normal struct and fixed-array arguments, value-bearing struct arguments, static struct arguments, and delegate struct arguments. * Kept nested aggregate crosscall argument shapes as explicit unsupported diagnostics. Validation run: ```sh theme={null} lake build scripts/evm/diagnostic-smoke.sh scripts/evm/crosscall-ir-smoke.sh ``` Result: * `EvmCrosscallProbe` generated reproducible Yul and runtime bytecode through `solc --strict-assembly`. * Foundry ran 35 CrosscallProbe tests, including aggregate argument calldata packing for normal/value/static/delegate typed calls. * EVM diagnostics ran 55 cases, including nested aggregate argument rejection. Known limitations: * Aggregate crosscall arguments are limited to ABI-static flat structs and scalar fixed arrays. * Value-bearing, static, and delegate typed crosscalls still return scalar words only. * Contract creation and variable-length return data remain future work. Next step: * Continue closing EVM call-surface gaps around aggregate returns for value/static/delegate calls or contract creation manifests. ### EVM IR Aggregate Crosscall Returns Commit: feature commit for EVM IR aggregate crosscall returns Summary: * Extended normal `crosscallInvokeTyped` returns beyond scalar words when the expression is returned directly from an ABI-facing entrypoint. * Lowered flat struct and scalar fixed-array crosscall return data through arity- and ABI-word-shape-specific Yul helpers such as `__proof_forge_crosscall_0_abi_bool_u32`, assigning multiple helper results directly to the entrypoint's ABI return words. * Preserved scalar behavior for value-bearing, static, and delegate typed crosscalls, and kept unsupported nested aggregate return shapes as explicit diagnostics. * Extended `EvmCrosscallProbe` with `call_remote_pair` and `call_remote_array`, refreshed golden Yul, metadata selector checks, Foundry aggregate struct/array return tests, malformed Bool/U32 aggregate return guard tests, coverage manifests, validation gates, target docs, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/i18n/check-sync.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/crosscall-ir-smoke.sh scripts/evm/foundry-smoke.sh ``` Known limitations: * Aggregate crosscall support is limited to normal typed calls returned directly from entrypoints. * Aggregate crosscall arguments, value/static/delegate aggregate returns, nested aggregate return data, contract creation, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking EVM cross-call gaps around aggregate arguments, value/static/delegate aggregate returns, or create/create2. ### EVM IR Typed Delegatecalls Commit: feature commit for EVM IR typed delegatecalls Summary: * Added portable IR `crosscallInvokeDelegateTyped` for EVM delegate calls that return one scalar word. * Lowered delegate calls to arity- and return-type-specific Yul helpers using `delegatecall(gas(), target, ...)`, sharing selector packing, scalar-word argument encoding, short-return checks, and Bool/U32 return guards with the other crosscall helper modes. * Kept delegate semantics explicit across backends: Psy IR v0 rejects delegate typed crosscalls with a stable unsupported diagnostic. * Extended `EvmCrosscallProbe` with U64/Bool/U32/Hash delegate entrypoints, refreshed golden Yul, Foundry caller-storage read/write checks, typed-return guard checks, metadata selector checks, EVM/Psy diagnostics, coverage manifests, target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/crosscall-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py scripts/i18n/check-sync.sh ``` Known limitations: * Delegate crosscalls are currently limited to scalar word arguments and one scalar word return (`U32`, `U64`, `Bool`, or `Hash`). * Contract creation, aggregate crosscall arguments/returns, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking EVM cross-call gaps around create/create2 or aggregate calldata/return-data. ### EVM IR Typed Staticcalls Commit: feature commit for EVM IR typed staticcalls Summary: * Added portable IR `crosscallInvokeStaticTyped` for read-only EVM cross-contract calls that return one scalar word. * Lowered typed static calls to arity- and return-type-specific Yul helpers using `staticcall(gas(), target, ...)`, sharing selector packing, scalar-word argument encoding, short-return checks, and Bool/U32 return guards with the existing call helpers. * Kept target semantics explicit across backends: Psy IR v0 rejects static typed crosscalls with a stable unsupported diagnostic rather than silently lowering them to the existing Felt-returning `__invoke_sync` form. * Extended `EvmCrosscallProbe` with `call_remote_static` plus Bool/U32/Hash static typed variants, refreshed golden Yul, Foundry read-only return, typed-return guard, and static-context state-write failure checks, metadata selector checks, EVM/Psy diagnostics, coverage manifests, target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/i18n/check-sync.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/crosscall-ir-smoke.sh ``` Known limitations: * Static crosscalls are currently limited to scalar word arguments and one scalar word return (`U32`, `U64`, `Bool`, or `Hash`). * `delegatecall`, contract creation, aggregate crosscall arguments/returns, and variable-length return data remain future EVM IR work. Next step: * Continue shrinking EVM cross-call gaps around `delegatecall`, create/create2, aggregate calldata/return-data, or richer artifact metadata for deployment. ### EVM IR Aggregate Event Data Commit: feature commit for EVM IR aggregate event data Summary: * Extended EVM `eventEmit` / `eventEmitIndexed` lowering so non-indexed event data fields can be scalar words, flat structs, scalar fixed arrays, or fixed arrays of flat structs. * Added canonical Solidity-style event signature generation for flat aggregate event fields, including `PairEvent((uint64,uint64))`, `ArrayEvent(uint64[2])`, and `PairArrayEvent((uint64,uint64)[2])`. * Flattened aggregate event data into ABI-style 32-byte words before `log1` through `log4`, preserving scalar indexed topics for `eventEmitIndexed`. * At the time of this entry, aggregate indexed fields still failed with a diagnostic instead of lowering. That limitation is resolved by the later "EVM IR Indexed Aggregate Event Topics" entry for flat supported aggregates. * Extended `EventProbe` with `emit_pair_event`, `emit_array_event`, and `emit_pair_array_event`, refreshed golden Yul, Foundry recorded-log checks, metadata selector checks, EVM diagnostics, coverage, target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build proof-forge scripts/evm/event-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * At the time of this entry, indexed event fields were scalar-only (`U32`, `U64`, `Bool`, or `Hash`) and limited to three indexed fields after the signature topic. Flat supported aggregate indexed fields are covered by the later "EVM IR Indexed Aggregate Event Topics" entry. * Richer first-class event declarations are still not represented in the portable IR. Next step: * Continue shrinking EVM gaps around richer cross-call return data, `staticcall`/`delegatecall`/creation call kinds, nested aggregate lowering, or real creation/broadcast manifests. ### EVM IR Indexed Event Topics Commit: feature commit for EVM IR indexed events Summary: * Added portable IR `eventEmitIndexed` for EVM-style events with scalar indexed fields and non-indexed data fields. * Lowered indexed events to Yul `log2`/`log3`/`log4`: topic0 is the Solidity-style event signature hash, indexed fields become topics, and non-indexed fields remain ABI-style 32-byte data words. * Kept indexed events explicit on non-EVM targets: Psy IR v0 rejects the new node with a diagnostic instead of silently dropping topic semantics. * Extended `EventProbe` with `emit_indexed_event`, refreshed golden Yul, Foundry recorded-log checks, metadata selector checks, EVM/Psy diagnostics, coverage manifests, target docs, validation gates, backlog, capability registry entries, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/event-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py scripts/i18n/check-sync.sh ``` Known limitations: * Indexed event fields are limited to scalar EVM word values (`U32`, `U64`, `Bool`, or `Hash`) and at most three indexed fields after the signature topic. * Aggregate event payloads and richer event declarations remain future work. Next step: * Continue shrinking EVM gaps around aggregate event payloads, richer cross-call return data, contract-creation call kinds, or nested aggregate lowering. ### EVM IR Solidity-Style Event Signatures Commit: feature commit for EVM IR event signature topics Summary: * Changed portable IR `eventEmit` topic0 derivation from the raw event-name hash to `keccak256(Solidity-style event signature)`. * Added EVM ABI type names for supported event scalar fields: `U32 -> uint32`, `U64 -> uint64`, `Bool -> bool`, and `Hash -> bytes32`. * Reworked the Yul event topic preimage writer to pack arbitrary-length UTF-8 signature strings into memory before hashing, removing the old 32-byte event name packing limit. * Updated `EventProbe` golden Yul, Foundry recorded-log assertion, coverage manifest, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/event-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/i18n/check-sync.sh ``` Known limitations: * Portable IR event payload fields remain limited to scalar word values: `U32`, `U64`, `Bool`, or `Hash`. * Richer event declarations are still not represented in the portable IR. Next step: * Continue shrinking event gaps around aggregate event payloads or richer event declarations, or move to another EVM surface such as richer cross-call return data or nested aggregate lowering. ### EVM IR Whole Storage Struct Read/Write Commit: feature commit for EVM IR whole storage struct read/write Summary: * Allowed `storageScalarRead` and `storageScalarWrite` to operate on flat scalar storage structs by expanding the struct into declaration-ordered EVM field slots. * Added aggregate-only lowering for struct storage reads: struct local bindings, struct field access, whole local struct assignment, and struct returns can consume `storageScalarRead` without treating the struct as a single EVM word. * Lowered whole scalar storage struct writes from local structs, struct literals, and storage struct reads with RHS field snapshotting before writing target slots. * Extended `EvmStorageStructProbe` with whole write/read-into-local, direct ABI struct return from storage, and self-referential storage write snapshot coverage. * Refreshed golden Yul, artifact metadata entrypoint checks, Foundry smoke tests, diagnostics, coverage manifest, target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/storage-struct-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Whole storage struct operations are limited to flat scalar storage structs whose fields lower to EVM words (`U32`, `U64`, `Bool`, or `Hash`). * Nested struct fields, non-flat struct storage, nested arrays, and dynamic or nested aggregate ABI values remain explicit diagnostics or documented gaps. Next step: * Continue shrinking the EVM aggregate unsupported surface around nested local aggregate shapes, broader storage-backed aggregate ABI values, richer cross-call return data, or event schema fidelity. ### EVM IR Struct Array Whole Local Assignment Commit: feature commit for EVM IR struct-array whole local assignment Summary: * Allowed `assign (.local name) value` for mutable local fixed arrays whose element type is a flat struct. * Lowered whole local struct-array assignment from another local struct array or a struct-array literal by snapshotting every RHS element field into temporary Yul locals before writing the expanded target fields. * Extended `EvmStructArrayValueProbe` with `whole_struct_array_assign()` and `self_struct_array_assign()` to validate local-source assignment and self-referential literal RHS snapshot semantics. * Refreshed the golden Yul, artifact metadata entrypoint checks, Foundry smoke harness, EVM coverage manifest, target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/struct-array-value-ir-smoke.sh ``` Known limitations: * Struct-array whole assignment is limited to fixed arrays whose element type is a flat struct over EVM word fields (`U32`, `U64`, `Bool`, or `Hash`). * Nested arrays, nested local structs, whole-struct storage reads/writes, and dynamic or nested aggregate ABI values remain explicit diagnostics. Next step: * Continue shrinking the remaining EVM aggregate unsupported surface, likely around nested aggregate locals, richer cross-call return data, or event schema fidelity. ### EVM IR Storage Map Contains Commit: feature commit for EVM IR storage map contains Summary: * Lowered `storage.map.contains` for EVM portable IR through ProofForge-managed presence slots instead of treating nonzero map values as presence. * Added `__proof_forge_map_presence_slot(slot, key)`, rooted at `keccak256(slot || PROOF_FORGE_MAP_PRESENCE)`, while preserving the existing Solidity-style value slot `keccak256(key || slot)`. * Updated map insert/set, map statement writes, and map storage-path compound assignment helpers to mark key presence whenever ProofForge writes a map key. * Extended `EvmMapProbe` with U64 contains coverage, including a zero-valued present key, and extended `EvmTypedMapProbe` with U32/Bool/Hash contains entrypoints. * Updated diagnostics so statement-position `storage.map.contains` fails with an expression-only diagnostic instead of an unsupported-capability error. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.IR proof-forge scripts/evm/map-ir-smoke.sh scripts/evm/typed-map-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Presence tracks keys written through ProofForge-generated map helpers; raw external storage mutation outside those helpers can still bypass the presence mapping. * Nested map paths and aggregate/non-word map key/value shapes remain explicit diagnostics. Next step: * Continue shrinking the remaining EVM aggregate unsupported surface, likely around nested aggregate locals, richer event schemas, or broader cross-call return data. ### EVM IR Whole Local Aggregate Assignment Commit: feature commit for EVM IR whole local aggregate assignment Summary: * Allowed `assign (.local name) value` for mutable local fixed-array and flat local struct values. * Lowered whole local fixed-array assignment from another local fixed-array or a fixed-array literal by snapshotting RHS element words into temporary Yul locals before assigning expanded target elements. * Lowered whole local struct assignment from another local struct or a struct literal by snapshotting RHS field words into temporary Yul locals before assigning expanded target fields. * Extended `EvmArrayValueProbe` with `whole_array_assign()` and `EvmStructValueProbe` with `whole_struct_assign()` to validate local-source assignment and self-referential literal RHS snapshot semantics. * Updated EVM diagnostics, coverage manifests, target docs, validation gates, backlog, and Chinese docs to remove the stale whole-local-aggregate assignment limitation. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.IR proof-forge scripts/evm/array-value-ir-smoke.sh scripts/evm/struct-value-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Whole local aggregate assignment is limited to flat fixed-array and flat struct locals whose elements/fields lower to EVM words. * Nested arrays, nested local structs, and whole-struct storage reads/writes remain explicit diagnostics. * Dynamic or nested aggregate ABI values remain out of scope for the current flat ABI lowering. Next step: * Continue shrinking the EVM aggregate unsupported surface around nested aggregate locals, richer cross-call return data, or event schema fidelity. ### EVM IR Dynamic Local Fixed-Array Indexes Commit: feature commit for EVM IR dynamic local fixed-array indexing Summary: * Threaded the EVM IR lowering environment through expression, effect, aggregate binding, return, and statement lowering so local aggregate shape is available during code generation. * Added dynamic `arrayGet` lowering for local fixed-array values and fixed-array literals using length-specific Yul getter helpers with default revert cases. * Added dynamic mutable local fixed-array element assignment and numeric compound assignment lowering with Yul `switch` blocks over expanded local elements. * Extended `EvmArrayValueProbe` with `dynamic_pick(uint256)` and `dynamic_update(uint256)`, refreshed golden Yul, metadata entrypoint validation, and Foundry assertions for in-bounds values and out-of-bounds reverts. * Updated EVM diagnostics, coverage manifests, target docs, validation gates, backlog, and Chinese docs to remove the stale dynamic-local-index limitation. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.IR proof-forge scripts/evm/array-value-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Dynamic fixed-array indexing is limited to local fixed-array values and fixed-array literals whose elements lower to EVM words. * Whole local aggregate assignment is handled by the later "EVM IR Whole Local Aggregate Assignment" entry. * Nested arrays, nested local structs, and whole-struct storage reads/writes remain explicit diagnostics. * Dynamic or nested aggregate ABI values remain out of scope for the current flat ABI lowering. Next step: * Continue shrinking the EVM aggregate unsupported surface, most likely around nested aggregate locals or richer cross-call return data. ### EVM Deploy Manifest Metadata Commit: feature commit for EVM deploy manifest metadata Summary: * Extended EVM bytecode modes to emit a ProofForge EVM deploy manifest next to each `proof-forge-artifact.json` metadata file. * The manifest records source kind/module, portable IR version when present, capabilities, ABI entrypoints or SDK methods, Yul/source inputs, runtime bytecode hash/size, and `creation.mode: runtime-bytecode`. * EVM artifact metadata now records the deploy manifest artifact and requires `validation.deployManifest: passed`. * Added a standalone `scripts/evm/validate-deploy-manifest.py` validator and extended `scripts/evm/validate-artifact-metadata.py` to validate the referenced deploy manifest against metadata. * Updated EVM target docs, validation gates, backlog, and Chinese docs to distinguish ProofForge runtime-bytecode manifests from future broadcast or creation-transaction manifests. Validation run: ```sh theme={null} lake build ProofForge.Cli proof-forge python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/validate-deploy-manifest.py scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/build-examples.sh python3 scripts/evm/validate-deploy-manifest.py --root . --expect-fixture AbiScalarProbe --expect-source-kind portable-ir build/ir/AbiScalarProbe.proof-forge-deploy.json python3 scripts/evm/validate-deploy-manifest.py --root . --expect-fixture Counter.lean --expect-source-kind lean-sdk build/evm/Counter.proof-forge-deploy.json ``` Known limitations: * The deploy manifest describes runtime bytecode deployment inputs only. * It does not yet generate constructor initcode, Foundry broadcast JSON, chain id, deployed address, or a signed/raw transaction. * Foundry smokes still install runtime bytecode with `vm.etch`. Next step: * Either extend EVM manifests toward creation/broadcast artifacts, or continue shrinking the remaining EVM IR unsupported surface around dynamic aggregates and richer cross-call returns. ### EVM IR Mutable Local Aggregates Commit: feature commit for EVM IR mutable local aggregate lowering Summary: * Extended EVM IR lowering for local fixed-array and flat struct values from immutable-only bindings to mutable aggregate locals. * Added static local fixed-array element assignment and numeric compound assignment over expanded Yul locals. * Added static local struct field assignment and numeric compound assignment over expanded Yul locals. * Extended `EvmArrayValueProbe` and `EvmStructValueProbe` with mutable `U64`/`U32`/`Bool`/`Hash` write paths, metadata entrypoint validation, refreshed golden Yul, and Foundry runtime assertions. * Updated EVM diagnostics so immutable aggregate element/field assignment still fails explicitly while mutable aggregate locals now lower successfully. * Updated EVM coverage, target docs, validation gates, backlog, and Chinese docs to remove stale mutable-local aggregate limitations. Validation run: ```sh theme={null} lake build ProofForge.IR.Examples.EvmArrayValueProbe ProofForge.IR.Examples.EvmStructValueProbe proof-forge scripts/evm/array-value-ir-smoke.sh scripts/evm/struct-value-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * Dynamic local fixed-array indexing is handled by the later "EVM IR Dynamic Local Fixed-Array Indexes" entry. * Whole local aggregate assignment remains an explicit diagnostic; update elements or fields directly for now. * Nested arrays, nested local structs, and whole-struct storage reads/writes remain explicit diagnostics. Next step: * Continue shrinking the EVM aggregate unsupported surface around nested aggregate locals or richer cross-call return data. ### EVM IR Scalar Expression Probe Commit: feature commit for EVM IR scalar expression validation Summary: * Added `ProofForge.IR.Examples.EvmExpressionProbe` to validate scalar expression lowering directly, separate from storage or assignment side effects. * Covered `U64` and `U32` arithmetic (`add`, `sub`, `mul`, `div`, `mod`), `U64` exponentiation, `U64`/`U32` bitwise operators and shifts, predicates, boolean `and`/`or`/`not`, scalar literals, immutable local reads, supported `U32`/`U64`/`Bool` casts, one-word scalar returns, and assertion guards. * Added CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Updated EVM coverage, target docs, validation gates, backlog, and Chinese docs so the scalar expression family now has runtime validation evidence instead of only structural lowering notes. Validation run: ```sh theme={null} lake build ProofForge.IR.Examples.EvmExpressionProbe proof-forge scripts/evm/expression-ir-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Known limitations: * EVM arithmetic still follows raw EVM word semantics; checked overflow, signed arithmetic, and target-specific numeric policies remain future design work. * Aggregate expression behavior remains covered by the array, struct, and ABI probes rather than this scalar expression probe. Next step: * Continue converting remaining `lowered` coverage rows into validated probes or explicit diagnostics, especially around target-specific artifact/deploy surfaces and any residual statement/effect validation gaps. ### EVM IR Typed Storage Maps Commit: feature commit for EVM IR typed storage maps Summary: * Generalized portable EVM storage maps from `Map` to word key/value maps over `U32`, `U64`, `Bool`, and `Hash`. * Reused the existing Solidity-style `keccak256(key, slot)` mapping slot helper for all supported word map shapes, preserving one declared storage slot per map state. * Added `ProofForge.IR.Examples.EvmTypedMapProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Covered ABI dispatcher guards for `U32` and `Bool` map parameters, expression-position previous-value returns, statement-position writes, `Hash`/`bytes32` map values, raw mapping slots, and single-segment `mapKey` storage-path read/write/compound assignment. * Updated EVM diagnostics, coverage, target docs, validation gates, and Chinese docs so unsupported map diagnostics now target non-word map shapes while `storage.map.contains` remains explicitly unsupported. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.IR ProofForge.IR.Examples.EvmTypedMapProbe proof-forge scripts/evm/typed-map-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Known limitations: * EVM storage maps still support only single-word key/value shapes. Aggregate, nested, dynamic, or non-word map key/value shapes remain explicit diagnostics. * `storage.map.contains` remains unsupported because EVM mappings do not track key presence without an auxiliary bitmap. * Nested map storage paths remain unsupported; `mapKey` paths are currently single-segment only. Next step: * Continue reducing the remaining EVM IR unsupported surface, likely around richer ABI/cross-call surfaces or target-specific deployment artifacts, with the same golden Yul, metadata, Foundry, diagnostics, and CI pattern. ### EVM IR Typed Storage Words Commit: feature commit for EVM IR typed storage word arrays Summary: * Generalized portable EVM storage arrays from `U64`-only arrays to word-scalar arrays over `U32`, `U64`, `Bool`, and `Hash`. * Enabled `Bool` scalar storage in the portable EVM backend; scalar storage still rejects unsupported non-word shapes explicitly. * Reused the existing contiguous `__proof_forge_array_slot(base, length, index)` helper for typed word arrays, preserving runtime out-of-bounds checks and deterministic slot layout. * Added `ProofForge.IR.Examples.EvmTypedStorageProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Updated EVM diagnostics, coverage, target docs, validation gates, and Chinese docs so `Unit` storage remains the explicit unsupported case while `Bool`/`U32`/`Hash` storage arrays are validated behavior. Validation run: ```sh theme={null} lake build ProofForge.Backend.Evm.IR proof-forge scripts/evm/typed-storage-ir-smoke.sh ``` Known limitations: * Typed storage arrays are still fixed-size word arrays. Nested arrays, dynamic storage arrays, and non-word storage elements remain future work. Next step: * Continue reducing the remaining EVM IR unsupported surface, likely either richer map shapes or the next ABI/control/cross-call gap, with the same golden Yul, metadata, Foundry, diagnostics, and CI pattern. ### EVM IR Flat Storage Structs Commit: feature commit for EVM IR flat storage struct lowering Summary: * Added EVM portable IR lowering for flat scalar storage structs and fixed storage arrays of flat structs. Scalar storage structs reserve one slot per field; struct arrays reserve `length * field_count` slots. * Added direct lowering for `storageStructFieldRead`/`Write` and `storageArrayStructFieldRead`/`Write`, plus generic storage paths using scalar `field` and array `index`+`field` segments. * Added the `__proof_forge_struct_array_slot` Yul helper with runtime out-of-bounds checks and deterministic `base + index * field_count + field_offset` slot derivation. * Added `ProofForge.IR.Examples.EvmStorageStructProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Updated EVM diagnostics and coverage so whole-struct storage reads/writes and missing fields fail explicitly before Yul generation. Validation run: ```sh theme={null} lake build proof-forge scripts/evm/storage-struct-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Known limitations: * Storage struct support is flat and field-based only. Whole-struct storage reads/writes, nested struct fields, map values shaped as structs, and dynamic storage arrays remain explicit future work. Next step: * Continue EVM portable IR support toward richer storage element types or the next unsupported ABI/control surface, keeping the same golden Yul, metadata, Foundry, diagnostics, and CI pattern. ### EVM IR Flat Aggregate ABI Commit: feature commit for EVM IR flat aggregate ABI lowering Summary: * Added EVM portable IR ABI flattening for flat static fixed-array and struct parameters. Fixed arrays lower to one calldata word per element, and structs lower to fields in declaration order. * Added dispatcher range guards for `U32` and `Bool` words inside aggregate ABI parameters. * Added multi-word return-data lowering for flat fixed-array and struct return values, including local fixed-array returns and struct literal returns. * Added `ProofForge.IR.Examples.EvmAbiAggregateProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Updated EVM diagnostics so Unit ABI values, zero-length ABI arrays, and nested aggregate ABI values fail explicitly before Yul generation. Validation run: ```sh theme={null} lake build scripts/evm/abi-aggregate-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Known limitations: * Aggregate ABI support is flat/static only. Nested aggregate ABI values, dynamic arrays, storage structs, mutable local structs, and struct arrays remain future work. Next step: * Continue the EVM backend toward storage struct layout or richer ABI/event schemas, using the same fixture, golden, metadata, Foundry, and CI pattern. ### CI ContextProbe Target Split Commit: bugfix commit for CI fixture isolation Summary: * Split `ContextProbe` target usage so the shared Psy fixture keeps only target-portable context reads. * Added `ProofForge.IR.Examples.EvmContextProbe` for EVM-only `nativeValue` coverage while preserving the existing `ContextProbe` Yul object name, selectors, golden Yul, and Foundry smoke behavior. * Updated EVM context CLI emission to use the EVM-specific fixture, while `--emit-context-ir-psy` continues to use the Psy-compatible fixture. * Fixed the GitHub Actions failure where the Psy golden source step attempted to lower `nativeValue`, which Psy IR v0 intentionally rejects. * Made `scripts/evm/build-examples.sh` explicitly build `ProofForge.Evm` before compiling SDK examples so clean CI environments have the SDK `.olean` needed by the Lean frontend. Validation run: ```sh theme={null} lake build # Full Check Psy golden sources block from .github/workflows/ci.yml scripts/evm/context-ir-smoke.sh scripts/evm/build-examples.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py git diff --check ``` Known limitations: * Psy still rejects `nativeValue` by design; EVM owns the current `callvalue()` lowering and runtime validation. Next step: * Re-run GitHub Actions on `main` and continue the EVM aggregate ABI work after CI is green. ### EVM IR Local Struct Values Commit: feature commit for EVM IR local struct values Summary: * Added EVM portable IR lowering for flat immutable local struct values by expanding each supported field into an internal Yul local. * Added direct field-access lowering for local struct values and struct literals over `U64`, `U32`, `Bool`, and `Hash` fields. * Registered partial `data.struct` support in the EVM target profile and metadata capability flow. * Added explicit diagnostics for struct storage, mutable local structs, nested struct fields, ABI-facing structs, duplicate/empty struct declarations, and unsupported field shapes. * Added `ProofForge.IR.Examples.EvmStructValueProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. Validation run: ```sh theme={null} lake build scripts/evm/struct-value-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py git diff --check ``` Known limitations: * This feature supports flat immutable local struct values only. Mutable local structs, nested structs, storage structs, struct arrays, ABI structs, and struct assignment paths remain future work. Next step: * Continue EVM aggregate coverage toward ABI aggregate values or storage struct layout once the target-specific EVM ABI/storage policy is specified. ### EVM IR Local Fixed-Array Values Commit: feature commit for EVM IR local fixed-array values Summary: * Added EVM portable IR lowering for immutable local fixed-array values by expanding each array element into an internal Yul local. * Added static `arrayGet` lowering for local fixed-array values and direct fixed-array literals over `U64`, `U32`, `Bool`, and `Hash` elements. * Added explicit diagnostics for mutable fixed-array locals, dynamic local fixed-array indexes, and static out-of-bounds indexes. * Added `ProofForge.IR.Examples.EvmArrayValueProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. Validation run: ```sh theme={null} lake build proof-forge scripts/evm/array-value-ir-smoke.sh scripts/evm/diagnostic-smoke.sh ``` Known limitations: * This feature supports immutable local fixed-array values with static indexes. Dynamic local indexes, mutable local arrays, nested arrays, aggregate ABI arrays, and storage arrays beyond the existing `U64` path remain future work. Next step: * Continue EVM aggregate coverage toward structs or ABI aggregate values, using the same fixture/golden/smoke/metadata pattern. ### EVM IR Array Index Storage Paths Commit: feature commit for EVM IR array index storage paths Summary: * Added EVM portable IR lowering for single-segment `StoragePathSegment.index` paths over `U64` fixed storage arrays. * Reused `__proof_forge_array_slot(base, length, index)` for generic `storagePathRead`, `storagePathWrite`, and `storagePathAssignOp` so direct array effects and storage paths share bounds-checking behavior. * Extended `EvmStorageArrayProbe` with `path_lifecycle()` and `path_assign_lifecycle()`. * Extended `scripts/evm/storage-array-ir-smoke.sh` to validate path read, write, compound assignment, metadata selectors, and raw storage slots. * Kept nested index paths, struct paths, and non-`U64` arrays explicitly rejected. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-storage-array-ir-yul -o build/ir/EvmStorageArrayProbe.yul diff -u Examples/Evm/EvmStorageArrayProbe.golden.yul build/ir/EvmStorageArrayProbe.yul scripts/evm/storage-array-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py git diff --check ``` Known limitations: * This feature supports exactly one `index` path segment over `U64` storage arrays. Nested array paths, struct fields, local fixed-array values, and aggregate ABI arrays remain future work. Next step: * Move from storage-array paths toward local fixed-array values or flat structs, depending on which aggregate surface is needed first. ### EVM IR U64 Storage Arrays Commit: feature commit for EVM IR U64 storage array lowering Summary: * Added EVM target-profile support for `storage.array` and partial `data.fixed_array`. * Added state-slot span accounting so fixed storage arrays reserve one EVM storage slot per element and later state starts after the full array span. * Added portable IR lowering for `storageArrayRead` and `storageArrayWrite` over `U64` storage arrays. * Lowered array access through `__proof_forge_array_slot(base, length, index)`, which reverts when the runtime index is out of bounds before `sload` or `sstore`. * Added `ProofForge.IR.Examples.EvmStorageArrayProbe`, CLI emission modes, golden Yul, Foundry smoke coverage, artifact metadata validation, and CI. * Kept local fixed-array values, aggregate ABI arrays, generic index storage paths, structs, and non-`U64` storage arrays explicitly rejected. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-storage-array-ir-yul -o build/ir/EvmStorageArrayProbe.yul diff -u Examples/Evm/EvmStorageArrayProbe.golden.yul build/ir/EvmStorageArrayProbe.yul scripts/evm/storage-array-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py git diff --check ``` Known limitations: * This feature covers `U64` storage arrays only. `U32`, `Hash`, `Bool`, struct arrays, local fixed-array values, ABI arrays, and generic index storage paths remain follow-up work. Next step: * Extend EVM aggregate support toward local fixed-array values or generic index storage paths, then move into structs once the array layout is stable. ### EVM IR Native Value Commit: feature commit for EVM IR native value lowering Summary: * Added EVM portable IR lowering for expression-position `nativeValue` as Yul `callvalue()`. * Extended `ProofForge.IR.Examples.ContextProbe` with `native_value()` and selector `0xf0eba40f`. * Extended `scripts/evm/context-ir-smoke.sh` so Foundry calls `native_value()` with attached value and verifies the returned word. * Updated EVM artifact metadata validation to require `value.native` and the `native_value:f0eba40f` entrypoint. * Moved `Expr.nativeValue` in `Tests/EvmCoverage.tsv` from unsupported to validated and removed the old unsupported diagnostic case. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-context-ir-yul -o build/ir/ContextProbe.yul diff -u Examples/Evm/ContextProbe.golden.yul build/ir/ContextProbe.yul scripts/evm/context-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py git diff --check ``` Known limitations: * `nativeValue` is exposed as the raw EVM call value word. Higher-level native asset accounting remains a target/runtime policy layer above this IR node. Next step: * Continue expanding EVM portable IR coverage one small capability at a time, with fixture, smoke, coverage, docs, commit, and push for each feature. ### EVM IR Map Path Compound Assignment Commit: feature commit for EVM IR map path compound assignment Summary: * Added EVM portable IR lowering for statement-position `storagePathAssignOp` on single-segment `mapKey` paths over `Map`. * Lowered map path compound assignment through generated Yul helpers named `__proof_forge_map_assign_`. * Kept mapping slot calculation inside the helper so the key expression is evaluated once and the computed storage slot is reused for `sload` and `sstore`. * Added type validation so storage path compound assignment requires matching numeric path/value types. * Kept nested map paths, array paths, and struct paths explicitly rejected until those storage layouts are implemented. * Extended `ProofForge.IR.Examples.EvmMapProbe` with `path_assign_lifecycle()`, updated `Examples/Evm/EvmMapProbe.golden.yul`, and extended `scripts/evm/map-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-map-ir-yul -o build/ir/EvmMapProbe.yul diff -u Examples/Evm/EvmMapProbe.golden.yul build/ir/EvmMapProbe.yul scripts/evm/map-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmMapProbe Yul includes selector dispatch for `path_assign_lifecycle()` and map assign helpers for all `AssignOp` variants. * Foundry verifies `path_assign_lifecycle()` returns `58`, the raw mapping slot for key `3003` is `58`, and existing map get/set/path behavior still passes. * EVM artifact metadata records and validates `storage.scalar`, `storage.map`, and `assertions.check`. * Diagnostics reject expression-position `storagePathAssignOp` and nested storage-path compound assignment. Known limitations at the time of this entry: * EVM IR storage path compound assignment supported only a single `mapKey` over `Map`. * Array index paths, struct field paths, nested paths, and non-`U64` map shapes remained explicit diagnostics. Next step: * Continue EVM portable IR support toward storage arrays, structs, aggregate ABI values, or checked arithmetic semantics. ### EVM IR Compound Assignment Commit: feature commit for EVM IR compound assignment Summary: * Added EVM portable IR lowering for `Statement.assignOp` on mutable local `U32`/`U64` bindings. * Added EVM portable IR lowering for statement-position `storageScalarAssignOp` on numeric scalar storage. * Lowered arithmetic/bitwise compound assignment to Yul `add/sub/mul/div/mod/and/or/xor`, and lowered shifts with EVM operand order through `shl(shift, value)` and `shr(shift, value)`. * Added type validation so compound assignment requires matching `U32` or `U64` operands, mutable local targets, and scalar numeric storage targets. * Kept aggregate assignment targets and storage path compound assignment outside this local/scalar feature; the following map path entry closes the single-segment `mapKey` subset. * Added `ProofForge.IR.Examples.EvmAssignOpProbe`, `--emit-evm-assign-op-ir-yul`, `--emit-evm-assign-op-ir-bytecode`, `Examples/Evm/EvmAssignOpProbe.golden.yul`, and `scripts/evm/assign-op-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-assign-op-ir-yul -o build/ir/EvmAssignOpProbe.yul diff -u Examples/Evm/EvmAssignOpProbe.golden.yul build/ir/EvmAssignOpProbe.yul scripts/evm/assign-op-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmAssignOpProbe Yul includes selector dispatch, local compound assignment, scalar storage `sstore(slot, op(sload(slot), value))`, and U32 ABI range guards. * Foundry verifies `compound_assignment(uint256)` returns `58`, raw storage slot `0` is `58`, `compound_u32(uint32)` returns `11`, and unknown selectors revert. * EVM artifact metadata records and validates `storage.scalar`. * Diagnostics reject non-local compound assignment targets, non-numeric compound operands, and expression-position scalar storage compound assignment. Known limitations: * EVM IR compound assignment in this entry supports only mutable local scalars and scalar storage; aggregate locals remain out of scope. * Operations use raw EVM word semantics and do not add checked-overflow behavior. Next step: * Continue EVM portable IR support toward storage arrays, structs, aggregate ABI values, or storage-path compound updates. ### EVM IR Bounded Loops Commit: feature commit for EVM IR bounded loops Summary: * Added EVM target support for `control.bounded_loop`. * Added EVM portable IR lowering for statement-position `boundedFor`. * Lowered bounded loops to Yul `for` loops with a static `let` index prelude, `lt(index, stopExclusive)` condition, and `index := add(index, 1)` post block. * Added type validation for loop bodies with the loop index available as an immutable `U32` local. * Added explicit diagnostics for invalid loop ranges and loop-local returns. * Added `ProofForge.IR.Examples.EvmLoopProbe`, `--emit-evm-loop-ir-yul`, `--emit-evm-loop-ir-bytecode`, `Examples/Evm/EvmLoopProbe.golden.yul`, and `scripts/evm/loop-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-loop-ir-yul -o build/ir/EvmLoopProbe.yul diff -u Examples/Evm/EvmLoopProbe.golden.yul build/ir/EvmLoopProbe.yul scripts/evm/loop-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmLoopProbe Yul includes selector dispatch and a Yul `for` loop that increments scalar storage three times. * Foundry verifies the returned value and raw storage slot are both `3`, plus unknown-selector revert behavior. * EVM artifact metadata records and validates `control.bounded_loop`. * Diagnostics reject invalid bounded-loop ranges and loop-local returns. Known limitations: * EVM IR bounded loops currently require static natural-number bounds from the portable IR node. * Loop-local `return`, `break`, and `continue` are not modeled yet. Next step: * Continue expanding EVM portable IR support for aggregate values, storage arrays, structs, or compound assignment. ### EVM IR Crosscalls Commit: feature commit for EVM IR crosscalls Summary: * Added EVM portable IR lowering for expression-position `crosscallInvoke`. * Defined the EVM IR v0 crosscall policy: target is an address word, method is a low-32-bit selector, arguments are 32-byte words, the call uses zero ETH value, and the result is one 32-byte return word. * Added arity-specific Yul helpers that pack calldata, call `call(gas(), target, 0, ...)`, revert on failed calls or short returns, and decode the returned word. * Added type validation so crosscall target, method, and every argument must be `U64`. * Added `ProofForge.IR.Examples.EvmCrosscallProbe`, `--emit-evm-crosscall-ir-yul`, `--emit-evm-crosscall-ir-bytecode`, `Examples/Evm/EvmCrosscallProbe.golden.yul`, and `scripts/evm/crosscall-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-crosscall-ir-yul -o build/ir/EvmCrosscallProbe.yul diff -u Examples/Evm/EvmCrosscallProbe.golden.yul build/ir/EvmCrosscallProbe.yul scripts/evm/crosscall-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmCrosscallProbe Yul includes selector dispatch, calldata size guards, zero/one/two-argument crosscall helpers, failed-call reverts, short-return reverts, and one-word return decoding. * Foundry verifies a Solidity callee for zero/one/two argument calls, callee reverts, short returns, and unknown-selector reverts. * EVM artifact metadata records and validates `crosscall.invoke`. * Diagnostics reject malformed crosscall target, method, and argument types. Known limitations at this slice: * This first crosscall slice modeled only synchronous zero-value `call`. * Later slices below add typed scalar returns and value-bearing typed scalar calls; `staticcall`, `delegatecall`, create/create2, aggregate arguments/returns, and variable-length return data remain future IR work. Next step: * Continue expanding the EVM portable IR surface toward typed scalar returns, aggregate ABI values, arrays, structs, or richer call semantics. ### EVM IR Typed Scalar Crosscalls Commit: feature commit for EVM IR typed scalar crosscalls Summary: * Added portable IR `crosscallInvokeTyped` as a typed scalar-word crosscall expression while preserving the existing `crosscallInvoke` U64 behavior and helper names. * Extended EVM lowering so typed crosscalls accept `Bool`, `U32`, `U64`, and `Hash` word arguments and return `Bool`, `U32`, `U64`, or `Hash`. * Generated return-type-specific Yul helpers such as `__proof_forge_crosscall_1_bool`, `__proof_forge_crosscall_1_u32`, and `__proof_forge_crosscall_1_hash`; Bool and U32 helpers reject out-of-range return words after `returndatacopy`. * Extended `EvmCrosscallProbe` with `call_remote_bool`, `call_remote_u32`, and `call_remote_hash`, plus Foundry callee methods for valid typed returns and malformed Bool/U32 return words. * Added explicit EVM diagnostics for unsupported typed crosscall aggregate arguments/returns and an explicit Psy diagnostic because Psy IR v0 still only supports untyped Felt-returning `crosscallInvoke`. * Updated golden Yul, EVM/Psy coverage manifests, validation gates, EVM target docs, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-crosscall-ir-yul -o build/ir/EvmCrosscallProbe.yul diff -u Examples/Evm/EvmCrosscallProbe.golden.yul build/ir/EvmCrosscallProbe.yul scripts/evm/crosscall-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/psy/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/psy/check-ir-coverage-manifest.py ``` Result: * Generated EvmCrosscallProbe Yul includes selector dispatch for the typed entrypoints, Bool/U32 calldata guards, typed crosscall helper names, and Bool/U32 return-data guards. * Foundry verifies U64 zero/one/two-argument calls, Bool/U32/Hash typed return calls, callee reverts, short returns, invalid Bool/U32 return words, and unknown-selector reverts. * EVM artifact metadata validates all six CrosscallProbe entrypoints and records `crosscall.invoke`. * Diagnostics reject unsupported typed crosscall aggregate arguments/returns, while Psy rejects typed crosscalls explicitly instead of silently lowering them as Felt calls. Known limitations: * Portable IR EVM crosscalls still model only synchronous `call`. * Aggregate arguments/returns, multi-word return data, `staticcall`, `delegatecall`, and create/create2 remain future IR work. Next step: * Continue closing EVM backend gaps around richer call semantics, ABI aggregate storage-backed surfaces, and unsupported-node diagnostics. ### EVM IR Value-Bearing Typed Crosscalls Commit: feature commit for EVM IR value-bearing typed crosscalls Summary: * Added portable IR `crosscallInvokeValueTyped` for synchronous EVM calls that forward an explicit `U64` call-value expression while returning a typed scalar word. * Extended EVM lowering with value-specific Yul helpers named like `__proof_forge_crosscall_value_0`; these helpers keep the same selector and calldata packing as scalar crosscalls but pass `call_value` into the EVM `call(gas(), target, call_value, ...)` value slot. * Extended `EvmCrosscallProbe` with `call_remote_value`, implemented using `.nativeValue` so the entrypoint forwards the ETH received by the probe to a payable callee. * Added Foundry coverage that calls the probe with value, asserts the payable callee receives `msg.value`, checks the callee balance, and verifies the probe does not retain the forwarded value. * Added explicit EVM diagnostics for malformed call-value type and unsupported aggregate return type, plus an explicit Psy unsupported diagnostic for value-bearing typed crosscalls. * Updated golden Yul, coverage manifests, validation gates, EVM target docs, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build scripts/evm/crosscall-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/psy/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/psy/check-ir-coverage-manifest.py ``` Result: * `EvmCrosscallProbe` now has seven metadata-validated entrypoints, including `call_remote_value:365f4a44`. * Generated Yul includes `__proof_forge_crosscall_value_0(target, selector, call_value)` and passes the helper value parameter to the `call` opcode. * Foundry verifies 12 crosscall runtime paths, including ETH forwarding through `probe.call{value: 1234}` to a payable callee. * EVM and Psy diagnostics cover the new portable IR node instead of relying on missing-pattern or silent lowering behavior. Known limitations: * Value-bearing crosscalls are currently limited to synchronous EVM `call` and single scalar-word return data. * `staticcall`, `delegatecall`, create/create2, aggregate arguments/returns, and multi-word or variable-length return data remain future IR work. Next step: * Continue closing EVM cross-contract gaps around richer call kinds and richer return-data encoding. ### EVM IR Events Commit: feature commit for EVM IR events Summary: * Added EVM portable IR lowering for statement-position `eventEmit`. * Defined the EVM IR v0 event policy: `topic0 = keccak256(Solidity-style event signature)` and log data is the sequence of 32-byte field words. * Added event name and field validation: event names must be non-empty; event fields must be `U32`, `U64`, `Bool`, or `Hash`; event emission remains statement-only. * Added `--emit-evm-event-ir-yul`, `--emit-evm-event-ir-bytecode`, `Examples/Evm/EventProbe.golden.yul`, and `scripts/evm/event-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-event-ir-yul -o build/ir/EventProbe.yul diff -u Examples/Evm/EventProbe.golden.yul build/ir/EventProbe.yul scripts/evm/event-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EventProbe Yul includes selector dispatch, calldata size guards, event signature hashing, field data writes, and `log1(0, 32, topic0)`. * Foundry verifies recorded logs for emitter address, topic0, decoded data, and unknown-selector reverts. * EVM artifact metadata records and validates `events.emit`. * Diagnostics reject expression-position events and malformed event names. Known limitations: * Event data fields are limited to scalar word values. * Indexed fields are now covered by `eventEmitIndexed`; aggregate event payloads and richer event declarations remain future work. Next step: * Extend aggregate event payloads or richer event declarations, or start cross-contract call lowering for the EVM portable IR backend. ### EVM IR Hash Words Commit: feature commit for EVM IR hash words Summary: * Added EVM portable IR lowering for `Hash` as a one-word EVM `bytes32` representation across locals, ABI parameters, ABI returns, and scalar storage. * Added `hash4` literal packing and dynamic `hashValue` packing from four `U64` limbs into one 256-bit word. * Added Yul helper lowering for `hash` and `hash_two_to_one` using `keccak256(0, 32)` and `keccak256(0, 64)`. * Added lightweight EVM IR type validation for the currently supported scalar and Hash subset so Hash/U64 mismatches fail before Yul generation. * Added `ProofForge.IR.Examples.EvmHashProbe`, `--emit-evm-hash-ir-yul`, `--emit-evm-hash-ir-bytecode`, `Examples/Evm/EvmHashProbe.golden.yul`, and `scripts/evm/hash-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-hash-ir-yul -o build/ir/EvmHashProbe.yul diff -u Examples/Evm/EvmHashProbe.golden.yul build/ir/EvmHashProbe.yul scripts/evm/hash-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmHashProbe Yul includes selector dispatch, ABI calldata size guards, Hash literal packing, dynamic Hash packing, `keccak256` helpers, Hash scalar storage reads/writes, and one-word return encoding. * Foundry verifies `bytes32` ABI params/returns, single-word and pair hashing, dynamic packing, Hash scalar storage, raw slot reads through `vm.load`, and unknown-selector reverts. * EVM artifact metadata records and validates `crypto.hash` and `storage.scalar`. * Diagnostics now treat Hash as supported in the EVM scalar subset and reject malformed Hash/U64 usage with explicit type mismatch messages. Known limitations: * EVM portable IR Hash currently uses a target-specific one-word `bytes32` representation; Psy still uses four Felt limbs. * Hash map key/value shapes are still unsupported; EVM map support remains limited to `Map`. * Aggregate hashing inputs, arrays, structs, and events remain future work. Next step: * Extend EVM maps to additional scalar key/value shapes, or add event emission lowering with indexed topic/data metadata. ### EVM IR Storage Maps Commit: feature commit for EVM IR storage maps Summary: * Added EVM portable IR lowering for `Map` storage state. * Added Solidity-style mapping slot helpers: `mstore(0, key)`, `mstore(32, slot)`, `keccak256(0, 64)`. * Added EVM lowering for `storageMapGet`, `storageMapInsert`, and `storageMapSet`; expression-position set/insert return the previous value. * Added single-segment `storagePathRead`/`storagePathWrite` support for `.mapKey` paths over `Map`. * Kept `storageMapContains` explicitly unsupported because EVM mappings do not track key presence without an auxiliary bitmap. * Added `ProofForge.IR.Examples.EvmMapProbe`, `--emit-evm-map-ir-yul`, `--emit-evm-map-ir-bytecode`, `Examples/Evm/EvmMapProbe.golden.yul`, and `scripts/evm/map-ir-smoke.sh`. * Updated EVM diagnostics, coverage manifest, CI, EVM target docs, validation gates, backlog, and Chinese docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-evm-map-ir-yul -o build/ir/EvmMapProbe.yul diff -u Examples/Evm/EvmMapProbe.golden.yul build/ir/EvmMapProbe.yul scripts/evm/map-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated EvmMapProbe Yul includes selector dispatch, scalar ABI calldata guards, map helper functions, map get/set/insert calls, assertion guards, and `keccak256(0, 64)` slot hashing. * Foundry verifies lifecycle behavior, parameterized read/write behavior, single-segment `mapKey` storage paths, unknown-selector reverts, and raw mapping slots with `vm.load`. * EVM artifact metadata records and validates `storage.scalar`, `storage.map`, and `assertions.check`. * Diagnostics reject unsupported Hash map shapes, `storage.map.contains`, and malformed map storage paths. Known limitations: * EVM portable IR map support is currently limited to `Map`. * `storage.map.contains` remains unsupported until the IR models an EVM presence bitmap or a different target-specific presence policy. * Nested map/struct/array storage paths are still rejected. Next step: * Extend maps to more scalar key/value shapes, or add EVM `crypto.hash` lowering with a clear Keccak-vs-portable-Hash semantic boundary. ### EVM IR Context Reads Commit: feature commit for EVM IR context reads Summary: * Added EVM portable IR lowering for `contextRead` expressions: `userId -> caller()`, `contractId -> address()`, and `checkpointId -> number()`. * Added an EVM selector to `ContextProbe` while preserving the existing Psy context fixture. * Added `--emit-context-ir-yul` and `--emit-context-ir-bytecode` CLI modes. * Added `Examples/Evm/ContextProbe.golden.yul` plus `scripts/evm/context-ir-smoke.sh`. * Updated EVM capability metadata so `ContextProbe` validates `caller.sender`, `account.explicit`, and `env.block`. * Updated EVM diagnostics, coverage manifest, CI, target docs, validation gates, backlog, and capability registry docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-context-ir-yul -o build/ir/ContextProbe.yul diff -u Examples/Evm/ContextProbe.golden.yul build/ir/ContextProbe.yul scripts/evm/context-ir-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py ``` Result: * Generated ContextProbe Yul contains selector dispatch for `sum_context(uint256,uint256)`, ABI calldata size guarding, and direct EVM context opcodes. * Foundry verifies `caller()` via `vm.prank`, `number()` via `vm.roll`, and `address()` via an etched runtime address. * EVM artifact metadata records and validates the three context capabilities. * Statement-position context reads remain rejected with an explicit diagnostic. Known limitations: * The current portable `ContextField` set covers only user id, contract id, and checkpoint id. * EVM context values are emitted as 256-bit words; address-width and narrower integer normalization are still future type-validation work. Next step: * Add EVM `crypto.hash` lowering with a clear Keccak-vs-portable-Hash semantic boundary, or start EVM storage map slot hashing. ### EVM Artifact Metadata Commit: feature commit for EVM artifact metadata Summary: * Added EVM `proof-forge-artifact.json` emission to `proof-forge` bytecode-producing modes, covering both `--evm-bytecode` SDK builds and portable IR EVM bytecode fixtures. * Added `--artifact-output` to override the metadata path; without an override, bytecode modes write `proof-forge-artifact.json` next to the bytecode output. * Added metadata fields for schema version, target id/family, artifact kind, source kind/module, portable IR version, capability ids, selector-facing ABI, `solc` path/version, Yul/bytecode/source artifact hashes and byte sizes, and validation status. * Added `scripts/evm/validate-artifact-metadata.py` for machine validation of EVM metadata files. * Updated EVM IR smoke scripts and `scripts/evm/build-examples.sh` so generated metadata is validated in CI. * Updated EVM target docs, validation gates, backlog, portable IR docs, and Chinese docs. Validation run: ```sh theme={null} lake build PATH="$HOME/.foundry/bin:$PATH" 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 python3 scripts/evm/validate-artifact-metadata.py --root . \ --expect-fixture Counter.lean \ --expect-source-kind lean-sdk \ build/evm/Counter.proof-forge-artifact.json bash -n scripts/evm/*.sh python3 -m py_compile scripts/evm/validate-artifact-metadata.py scripts/evm/conditional-ir-smoke.sh scripts/evm/assignment-ir-smoke.sh scripts/evm/assert-ir-smoke.sh scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/ir-counter-smoke.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * SDK EVM bytecode builds emit validated metadata with source, Yul, bytecode, method selectors, and `solc` validation status. * Portable IR EVM bytecode builds emit validated metadata with fixture name, source module, `irVersion: portable-ir-v0`, capability ids, ABI selectors, Yul/bytecode hashes, and validation status. * Each EVM IR smoke now writes a fixture-specific metadata file to avoid parallel-run overwrite races. * `scripts/evm/build-examples.sh` validates metadata for every SDK example with a sibling `.evm-methods` file. Known limitations: * EVM metadata is still build metadata, not a full deploy manifest. * `capabilities` are populated for portable IR fixtures; SDK builds currently record method metadata but not inferred SDK capability ids. Next step: * Add EVM context or hashing lowering as the next isolated capability slice, or turn metadata into a unified target manifest when more targets share the schema. ### EVM IR Conditionals Commit: feature commit for EVM IR conditionals Summary: * Added `control.conditional` to the EVM target profile. * Extended `ProofForge.Backend.Evm.IR` to lower portable IR `if/else` into Yul `switch condition case 0 { else } default { then }` blocks. * Kept branch-local `return` statements explicitly rejected because EVM IR `return` currently assigns the generated function result and does not yet emit Yul `leave` for early return semantics. * Added an EVM selector to `ConditionalProbe` while preserving Psy output. * Added `--emit-conditional-ir-yul` and `--emit-conditional-ir-bytecode` CLI modes. * Added `Examples/Evm/ConditionalProbe.golden.yul` and `scripts/evm/conditional-ir-smoke.sh`, then wired the smoke into CI. * Updated EVM diagnostics, coverage manifest, capability registry, validation docs, EVM target docs, and Chinese documentation. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-conditional-ir-yul -o build/ir/ConditionalProbe.yul diff -u Examples/Evm/ConditionalProbe.golden.yul build/ir/ConditionalProbe.yul lake env proof-forge --emit-conditional-ir-psy -o build/psy/ConditionalProbe.psy diff -u Examples/Psy/ConditionalProbe.golden.psy build/psy/ConditionalProbe.psy bash -n scripts/evm/*.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/conditional-ir-smoke.sh scripts/evm/assignment-ir-smoke.sh scripts/evm/assert-ir-smoke.sh scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/ir-counter-smoke.sh scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * Generated ConditionalProbe Yul matches the checked-in golden fixture and contains Yul `switch` blocks for both then and else paths. * Psy ConditionalProbe output remains unchanged after adding target-specific selector metadata. * `scripts/evm/conditional-ir-smoke.sh` compiles ConditionalProbe to bytecode and passes Foundry tests for the expected conditional lifecycle result and unknown-selector revert behavior. * EVM diagnostics now cover the remaining conditional boundary: branch-local return statements. Known limitations: * Conditional branch early returns are not supported until EVM IR return lowering grows Yul `leave`. * The EVM IR backend still has minimal expression type validation. Next step: * Add EVM artifact metadata or scalar context/hash lowering as the next isolated feature slice. ### EVM IR Local Assignment Commit: feature commit for EVM IR local assignment Summary: * Treated the capability-complete EVM backend prompt as an incremental validation contract: every portable IR node must either gain a positive EVM fixture or retain a documented diagnostic. * Extended `ProofForge.Backend.Evm.IR` so mutable scalar local bindings lower to Yul `let` declarations. * Extended EVM IR assignment lowering for local targets as Yul `:=` assignments, while keeping non-local assignment targets and compound assignment statements explicitly rejected. * Added `ProofForge.IR.Examples.AssignmentProbe` with `reassignment(uint256)`, covering mutable `U64` and `Bool` locals plus a bool guard that depends on assignment. * Added `--emit-assignment-ir-yul` and `--emit-assignment-ir-bytecode` CLI modes. * Added `Examples/Evm/AssignmentProbe.golden.yul` and `scripts/evm/assignment-ir-smoke.sh`, then wired the smoke into CI. * Updated EVM diagnostics, coverage manifest, validation docs, and the EVM target docs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-assignment-ir-yul -o build/ir/AssignmentProbe.yul diff -u Examples/Evm/AssignmentProbe.golden.yul build/ir/AssignmentProbe.yul bash -n scripts/evm/*.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/assignment-ir-smoke.sh scripts/evm/assert-ir-smoke.sh scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/ir-counter-smoke.sh scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * Generated AssignmentProbe Yul matches the checked-in golden fixture and contains `let total := seed`, `total := add(total, 7)`, and `matched := eq(total, 12)`. * `scripts/evm/assignment-ir-smoke.sh` compiles AssignmentProbe to bytecode and passes Foundry tests for the successful assignment path and the bool-guard revert path. * EVM diagnostics now cover the remaining assignment boundaries: non-local assignment targets and compound assignment statements. Known limitations: * Local assignment support is scalar-only (`U32`, `U64`, `Bool`). * Compound assignment, aggregate assignment paths, storage assignment paths, and artifact metadata remain separate EVM work items. Next step: * Add EVM IR statement-level conditional lowering or EVM artifact metadata as the next isolated feature slice. ### EVM IR Assertions Commit: feature commit for EVM IR assertions Summary: * Added `assertions.check` to the EVM target profile and capability registry. * Extended `ProofForge.Backend.Evm.IR` to lower portable IR `assert` into `if iszero(condition) { revert(0, 0) }`. * Extended EVM IR `assertEq` lowering into `if iszero(eq(lhs, rhs)) { revert(0, 0) }`. * Added an EVM selector to `AssertProbe` while preserving Psy's selector-ignore behavior. * Added `--emit-assert-ir-yul` and `--emit-assert-ir-bytecode` CLI modes. * Added `Examples/Evm/AssertProbe.golden.yul` and `scripts/evm/assert-ir-smoke.sh`, then wired the smoke into CI. * Updated EVM diagnostics and coverage manifest to treat assertions as lowered instead of unsupported. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-assert-ir-yul -o build/ir/AssertProbe.yul diff -u Examples/Evm/AssertProbe.golden.yul build/ir/AssertProbe.yul lake env proof-forge --emit-assert-ir-psy -o build/psy/AssertProbe.psy diff -u Examples/Psy/AssertProbe.golden.psy build/psy/AssertProbe.psy bash -n scripts/evm/*.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/assert-ir-smoke.sh scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/ir-counter-smoke.sh scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * Generated EVM AssertProbe Yul matches the checked-in golden fixture. * Psy AssertProbe output remains unchanged after adding target-specific selector metadata. * `scripts/evm/assert-ir-smoke.sh` compiles AssertProbe to bytecode and passes Foundry tests for both successful assertion execution and assertion-failure revert behavior. * Existing EVM ABI scalar, IR Counter, SDK example build, and Foundry smoke gates still pass. Known limitations: * EVM assertions currently revert with empty revert data. * Expression type validation is still minimal in the EVM IR backend. Next step: * Add EVM IR statement-level assignment or conditional lowering so larger portable IR fixtures can move from unsupported diagnostics to Foundry-backed positive coverage. ### EVM IR Scalar ABI Parameters Commit: feature commit for EVM IR scalar ABI parameters Summary: * Added `ProofForge.IR.Examples.AbiScalarProbe` with `mix(uint256,uint32,bool)` and `same(uint256,uint256)` portable IR entrypoints. * Extended `ProofForge.Backend.Evm.IR` so `U64`, `U32`, and `Bool` entrypoint parameters lower to Yul function parameters and dispatcher `calldataload` arguments. * Added dispatcher ABI guards for short calldata, out-of-range `uint32` values, and invalid `bool` encodings. * Added CLI modes: `--emit-abi-scalar-ir-yul` and `--emit-abi-scalar-ir-bytecode`. * Added `Examples/Evm/AbiScalarProbe.golden.yul` and `scripts/evm/abi-scalar-ir-smoke.sh`, then wired the smoke into CI. * Updated EVM diagnostics to reject only non-scalar ABI parameter types instead of rejecting every parameterized entrypoint. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-abi-scalar-ir-yul -o build/ir/AbiScalarProbe.yul diff -u Examples/Evm/AbiScalarProbe.golden.yul build/ir/AbiScalarProbe.yul bash -n scripts/evm/*.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/abi-scalar-ir-smoke.sh scripts/evm/ir-counter-smoke.sh scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * Generated Yul includes selector dispatch for `mix` and `same`, calldata size guards, `uint32` range validation, and `bool` encoding validation. * `scripts/evm/abi-scalar-ir-smoke.sh` compiles the fixture to bytecode, verifies the golden Yul snapshot, and passes Foundry tests for valid calls and malformed calldata reverts. * EVM diagnostic smoke passes after replacing the obsolete all-parameter rejection with Unit/Hash ABI parameter diagnostics. * Existing EVM SDK examples still build and the Foundry smoke suite passes all four tests. Known limitations: * This only covers scalar word ABI parameters and one-word returns. * Aggregate ABI values, dynamic data, events, and artifact metadata remain pending. Next step: * Add the next EVM IR positive fixture for either assertions/reverts or statement-level assignment before expanding storage layout. ### EVM IR Coverage And Diagnostics Baseline Commit: feature commit for EVM IR coverage and diagnostics Summary: * Added `Tests/EvmCoverage.tsv`, tracking every portable IR constructor as `lowered`, `validated`, `unsupported`, or `structural` for the current EVM IR backend. * Added `scripts/evm/check-ir-coverage-manifest.py` so new portable IR nodes must be classified for EVM before CI passes. * Added `Tests/EvmDiagnostics.lean` and `scripts/evm/diagnostic-smoke.sh`, covering explicit diagnostics for missing selectors, unsupported ABI parameters, missing returns, unsupported aggregate/control/storage/context surfaces, events, crosscalls, native value, and Hash expressions. * Fixed the EVM IR backend to reject non-Unit entrypoints that do not end with a return statement instead of emitting an unassigned `result`. * Wired the new EVM diagnostic and coverage gates into CI. Validation run: ```sh theme={null} lake build bash -n scripts/evm/*.sh scripts/evm/diagnostic-smoke.sh scripts/evm/check-ir-coverage-manifest.py scripts/evm/ir-counter-smoke.sh scripts/evm/build-examples.sh scripts/evm/foundry-smoke.sh git diff --check ``` Result: * `scripts/evm/diagnostic-smoke.sh` passes 25 diagnostic cases. * `scripts/evm/check-ir-coverage-manifest.py` confirms 91 portable IR constructor entries match `ProofForge/IR/Contract.lean`. * The EVM IR Counter smoke still compiles to bytecode and passes Foundry. * The existing EVM SDK examples still build and the Foundry smoke suite passes all four tests. Known limitations: * This feature does not expand EVM lowering support; unsupported surfaces remain explicit until implemented with Yul golden, solc, and Foundry coverage. * EVM artifact metadata is still pending. Next step: * Start replacing selected `unsupported` EVM coverage rows with Dapp-style Yul/Foundry-backed positive fixtures, one feature at a time. ### Psy Fixed Array Equality Commit: feature commit for Psy fixed-array equality Summary: * Allowed Psy IR equality validation for fixed-array value types after a Dargo probe confirmed Psy supports `assert_eq(xs, ys)`, `xs == ys`, and `xs != zs` for fixed arrays. * Extended `ArrayProbe` with `array_predicates`, covering fixed-array `assert_eq`, equality, and inequality over `[Felt; 3]` locals. * Updated `scripts/psy/array-smoke.sh` to compile and execute `array_predicates`, record `result_vm: [1]`, and include it in artifact metadata validation. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-array-ir-psy -o build/psy/ArrayProbe.psy diff -u Examples/Psy/ArrayProbe.golden.psy build/psy/ArrayProbe.psy bash -n scripts/psy/*.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/array-smoke.sh git diff --check ``` Result: * Generated ArrayProbe source includes `array_predicates`, using `assert_eq(xs, ys, ...)`, `xs == ys`, and `xs != zs`. * `scripts/psy/array-smoke.sh` validates `sum_literal`, `storage_lifecycle`, and `array_predicates` through Dargo test, compile, execute, ABI generation, deploy manifest, and artifact metadata checks. * Dargo execution returns `result_vm: [1]` for `array_predicates`. Known limitations: * This feature covers same-typed fixed-array equality only; mismatched element types and lengths still fail through the existing type checker. Next step: * Commit and push this single feature before starting the next Psy surface area. ### Psy Native U32 Storage Struct Paths Commit: feature commit for Psy native U32 storage struct paths Summary: * Fixed Psy `storagePathWrite` so U32 paths only cast to Felt for the validated Felt-backed U32 storage-array representation. * Allowed native U32 storage struct field paths to use Psy's own `u32` storage reference idiom for path writes, reads, and compound assignment. * Extended `StorageNestedAggregateProbe` with a native `Profile.rank: u32` storage field across scalar struct and storage-array paths. * Removed the obsolete diagnostic that rejected non-array U32 storage-path compound assignment. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-storage-nested-aggregate-ir-psy -o build/psy/StorageNestedAggregateProbe.psy diff -u Examples/Psy/StorageNestedAggregateProbe.golden.psy build/psy/StorageNestedAggregateProbe.psy scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/storage-nested-aggregate-smoke.sh ``` Result: * Generated StorageNestedAggregateProbe source emits native `pub rank: u32`, native U32 path writes such as `c.person.profile.rank = 9u32`, and native U32 path compound assignment such as `c.person.profile.rank += 4u32`. * `scripts/psy/diagnostic-smoke.sh` passes all 48 diagnostic cases after removing the obsolete unsupported U32 path case. * `scripts/psy/storage-nested-aggregate-smoke.sh` passes `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest validation, and artifact metadata validation. * Dargo execution returns `result_vm: [252]` for `storage_nested_lifecycle`. Known limitations: * Direct Psy `[u32; N]` contract storage arrays remain avoided because current `psyup` 0.1.0 rejects them with an `ArrayRef` mismatch. * Map value compound assignment remains outside the supported storage-path surface. Next step: * Continue shrinking storage and ABI edge cases into Dargo-backed fixtures, one committed feature at a time. ### Psy U32 Storage Path Assignment Commit: feature commit for Psy U32 storage path assignment Summary: * Extended Psy lowering for Felt-backed U32 storage arrays so `storagePathAssignOp` emits typed read/update/write code instead of raw Felt compound assignment. * Covered all `AssignOp` variants in `U32StorageArrayProbe`: arithmetic, modulo, bitwise, and shifts. * Kept non-array U32 storage-path compound assignment rejected with an explicit ProofForge diagnostic until that storage representation is validated. * Updated the golden Psy source, Dargo smoke expected result, coverage matrix, and validation docs. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-storage-array-smoke.sh ``` Result: * Generated U32StorageArrayProbe source rewrites U32 storage-path compound assignment as `.get() as u32`, typed operation, then `as Felt` writeback. * `scripts/psy/diagnostic-smoke.sh` passes all 49 diagnostic cases, including the remaining unsupported non-array U32 storage-path assignment boundary. * `scripts/psy/u32-storage-array-smoke.sh` passes `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest validation, and artifact metadata validation. * Dargo execution returns `result_vm: [28]` for `storage_lifecycle`. Known limitations: * Direct Psy `[u32; N]` contract storage arrays remain avoided because current `psyup` 0.1.0 rejects them with an `ArrayRef` mismatch. * U32 storage-path compound assignment is supported only for the validated Felt-backed storage-array representation, not arbitrary U32 struct paths. This struct-path limitation is superseded by the native U32 storage struct path entry above. Next step: * Continue closing one Psy storage or expression gap per feature branch, with Dargo-backed smoke coverage before each commit. ### Psy Hash Storage Coverage Commit: feature commit for Psy Hash storage coverage Summary: * Added `HashStorageProbe` as a portable IR fixture for native Psy scalar `Hash` storage and `[Hash; N]` storage arrays. * Extended Psy state validation so `StateDecl.kind = .scalar` with `type = .hash` lowers to `pub root: Hash`. * Added CLI emission through `--emit-hash-storage-ir-psy` plus a checked golden source fixture. * Added `scripts/psy/hash-storage-smoke.sh` to validate `dargo test`, `dargo compile`, two `dargo execute` entrypoints, `dargo generate-abi`, deploy manifest generation, and artifact metadata validation. Validation run: ```sh theme={null} lake build bash -n scripts/psy/*.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake env proof-forge --emit-hash-storage-ir-psy -o build/psy/HashStorageProbe.psy diff -u Examples/Psy/HashStorageProbe.golden.psy build/psy/HashStorageProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/hash-storage-smoke.sh git diff --check ``` Result: * Generated HashStorageProbe source lowers `pub root: Hash`, `pub roots: [Hash; 2]`, scalar Hash read/write, indexed Hash array read/write, and generic storage-path read/write. * Dargo execution validates `result_vm: [5, 6, 7, 8]` for scalar storage and `result_vm: [55, 66, 77, 88]` for storage-array access. Known limitations: * This does not change U32 storage arrays, which remain Felt-backed because Dargo v0.1.0 rejects direct `[u32; N]` contract storage arrays. Next step: * Continue replacing explicit unsupported storage diagnostics with Dargo-validated Psy storage idioms where the upstream toolchain accepts the shape. ### Psy Bool Storage Array Coverage Commit: feature commit for Psy Bool storage array coverage Summary: * Added `BoolStorageArrayProbe` as a portable IR fixture for native Psy `[bool; N]` fixed arrays and `bool` storage arrays. * Extended Psy state validation so `StateDecl.kind = .array N` with `type = .bool` lowers to `pub flags: [bool; N]`. * Added CLI emission through `--emit-bool-storage-array-ir-psy` plus a checked golden source fixture. * Replaced the previous unsupported bool storage-array diagnostic with an unsupported Unit storage-array diagnostic. * Added `scripts/psy/bool-storage-array-smoke.sh` to validate `dargo test`, `dargo compile`, two `dargo execute` entrypoints, `dargo generate-abi`, deploy manifest generation, and artifact metadata validation. Validation run: ```sh theme={null} lake build bash -n scripts/psy/*.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake env proof-forge --emit-bool-storage-array-ir-psy -o build/psy/BoolStorageArrayProbe.psy diff -u Examples/Psy/BoolStorageArrayProbe.golden.psy build/psy/BoolStorageArrayProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/bool-storage-array-smoke.sh git diff --check ``` Result: * Generated BoolStorageArrayProbe source lowers local `[bool; 3]` arrays, `pub flags: [bool; 3]` storage arrays, indexed storage read/write, generic storage-path read/write, and `bool as Felt` return casts. * Dargo execution validates `result_vm: [2]` for both `local_flags_sum` and `storage_lifecycle`. Known limitations: * This does not change the existing U32 storage-array representation; U32 arrays remain Felt-backed because Dargo v0.1.0 rejects direct `[u32; N]` contract storage arrays. Next step: * Continue shrinking explicit unsupported diagnostics into Dargo-validated Psy support where the upstream toolchain accepts the target shape. ### Psy Bool Scalar Storage Coverage Commit: feature commit for Psy Bool scalar storage coverage Summary: * Added `BoolStorageScalarProbe` as a portable IR fixture for native Psy `bool` scalar storage. * Added CLI emission through `--emit-bool-storage-scalar-ir-psy` plus a checked golden source fixture. * Added `scripts/psy/bool-storage-scalar-smoke.sh` to validate `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest generation, and artifact metadata validation. * Extended Psy coverage evidence, validation docs, and CI golden checks. Validation run: ```sh theme={null} lake build bash -n scripts/psy/*.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake env proof-forge --emit-bool-storage-scalar-ir-psy -o build/psy/BoolStorageScalarProbe.psy diff -u Examples/Psy/BoolStorageScalarProbe.golden.psy build/psy/BoolStorageScalarProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/bool-storage-scalar-smoke.sh git diff --check ``` Result: * Generated BoolStorageScalarProbe source lowers scalar storage to `pub flag: bool`, native Bool reads/writes, and `bool as Felt` return casts. * Dargo execution validates `result_vm: [1]`. Known limitations: * This entry covered native scalar `bool` storage only. The later BoolStorageArrayProbe entry supersedes the previous bool storage-array limitation. Next step: * Continue filling the Psy scalar/aggregate storage matrix one feature at a time, with Dargo execution backing each newly enabled shape. ### Psy Map Set Expression Return Coverage Commit: feature commit for Psy map set expression returns Summary: * Added Psy lowering and type validation for `storageMapSet` when used as an expression, matching upstream `MapRef::set` returning the previous `Hash`. * Extended `MapProbe` with `set_return_lifecycle` and `insert_return_lifecycle` to cover absent-key zero returns, previous-value returns, and latest-value reads. * Updated the MapProbe generated test to bind side-effectful method results before assertion, avoiding Dargo repeated-evaluation behavior for direct calls inside `assert_eq`. * Extended the MapProbe smoke to execute the new methods and validate artifact metadata against all returned results. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-map-ir-psy -o build/psy/MapProbe.psy diff -u Examples/Psy/MapProbe.golden.psy build/psy/MapProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/map-smoke.sh ``` Result: * `set_return_lifecycle` returns `result_vm: [31, 32, 33, 34]`. * `insert_return_lifecycle` returns `result_vm: [5, 6, 7, 8]`. Known limitations: * Psy map support remains deliberately limited to `Map` until non-Hash map value semantics are modeled explicitly in the portable IR. Next step: * Continue converting upstream Psy map/storage semantics into fixture-backed ProofForge IR coverage. ### Psy Generic Test Fallback Commit: feature commit for generic Psy fallback tests Summary: * Replaced the Psy backend's fixture-only test generation failure with a generic fallback test that instantiates `Ref`. * Added `GenericEntrypointProbe` as a valid non-whitelisted portable IR fixture to prove that arbitrary supported modules can render `.psy` source. * Added a Dargo-backed smoke script, golden source, CI golden check, deploy manifest generation, and artifact metadata validation for the new fixture. * Added an explicit empty-state diagnostic because Dargo v0.1.0 rejects empty `#[derive(Storage)]` contracts. Validation run: ```sh theme={null} lake build bash -n scripts/psy/*.sh scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake env proof-forge --emit-generic-entrypoint-ir-psy -o build/psy/GenericEntrypointProbe.psy diff -u Examples/Psy/GenericEntrypointProbe.golden.psy build/psy/GenericEntrypointProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/generic-entrypoint-smoke.sh git diff --check ``` Result: * Dargo accepts the generic generated test and executes `GenericEntrypointProbe.answer` with `result_vm: [42]`. * Psy diagnostic smoke now covers 49 malformed or unsupported IR cases. Known limitations: * The generic fallback only proves source/package validity and ref instantiation. Fixture-specific behavior still needs dedicated assertions and smoke scripts when a feature has semantic expectations. Next step: * Continue closing expression and storage coverage gaps with one fixture-backed feature at a time. ### Psy Identifier Diagnostics Commit: feature commit for Psy identifier validation Summary: * Added Psy backend validation for module, struct, field, state, entrypoint, parameter, local, and loop-index identifiers before source generation. * Added duplicate declaration checks for struct names, state ids, entrypoint names, struct field ids, and entrypoint parameter names. * Added diagnostic fixtures for invalid module identifiers, duplicate state ids, duplicate entrypoint names, and reserved local names. Validation run: ```sh theme={null} scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake build git diff --check ``` Result: * Psy diagnostic smoke now covers 48 malformed or unsupported IR cases. * Invalid or ambiguous names fail in ProofForge before Dargo parsing or typechecking. Known limitations: * The reserved-word list covers Psy keywords and builtin names used by current generated source. If Psy adds new reserved identifiers upstream, this list should be updated with the toolchain bump. Next step: * Continue reducing Dargo-discovered failures into ProofForge diagnostics. ### Psy U32 Scalar Storage Coverage Commit: feature commit for Psy U32 scalar storage coverage Summary: * Added `U32StorageScalarProbe` as a portable IR fixture for native Psy `u32` scalar storage. * Added CLI emission through `--emit-u32-storage-scalar-ir-psy` plus a checked golden source fixture. * Added `scripts/psy/u32-storage-scalar-smoke.sh` to validate `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest generation, and artifact metadata validation. * Extended Psy coverage evidence, validation docs, and CI golden checks. Validation run: ```sh theme={null} DARGO_STD_PATH=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/lib/psy-std/std.psy \ /tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ test --file /tmp/proof_forge_probe/u32_scalar_storage.psy lake build bash -n scripts/psy/*.sh lake env proof-forge --emit-u32-storage-scalar-ir-psy -o build/psy/U32StorageScalarProbe.psy diff -u Examples/Psy/U32StorageScalarProbe.golden.psy build/psy/U32StorageScalarProbe.psy scripts/psy/check-ir-coverage-manifest.py PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-storage-scalar-smoke.sh git diff --check ``` Result: * Generated U32StorageScalarProbe source lowers scalar storage to `pub value: u32`, native U32 reads/writes, and scalar `+=`. * Dargo execution validates `result_vm: [12]`. Known limitations: * This covers native scalar `u32` storage only. U32 storage arrays still use the existing Felt-backed representation because current `psyup` 0.1.0 rejects direct `[u32; N]` contract storage arrays. Next step: * Continue broadening Psy storage and ABI validation while keeping unsupported storage forms explicit. ### Psy Entrypoint Selector Diagnostic Commit: feature commit for Psy selector rejection Summary: * Added a Psy backend validation rule that rejects `Entrypoint.selector?` before source generation. * Documented that Psy/DPN entrypoints are addressed by contract method name via Dargo and the generated Psy ABI, so EVM-style selectors are target-invalid rather than ignored. * Added a `Tests/PsyDiagnostics.lean` case to lock the diagnostic text. Validation run: ```sh theme={null} scripts/psy/diagnostic-smoke.sh scripts/psy/check-ir-coverage-manifest.py lake build git diff --check ``` Result: * Malformed Psy IR modules with entrypoint selectors now fail with an explicit diagnostic instead of silently dropping selector metadata. Known limitations: * This does not add a Psy-native selector concept. If Psy later exposes stable selector metadata, the backend should model it separately from EVM selectors. Next step: * Continue expanding non-fixture-specific Psy package generation and deployment validation. ### Psy Shared Dargo Package Writer Commit: feature commit for shared Psy Dargo package generation Summary: * Added `scripts/psy/write-dargo-package.py` as the shared package writer for Dargo-backed Psy smoke fixtures. * Replaced repeated shell `rm`/`mkdir`/`cp`/`Dargo.toml` heredocs across all Dargo-backed smoke scripts with a single writer invocation. * Kept a smoke-directory guard in the writer so it only rewrites `dargo-*` package directories. Validation run: ```sh theme={null} PYTHONDONTWRITEBYTECODE=1 python3 -m py_compile \ scripts/psy/write-dargo-package.py \ scripts/psy/write-artifact-metadata.py \ scripts/psy/validate-artifact-metadata.py \ scripts/psy/check-ir-coverage-manifest.py bash -n scripts/psy/*.sh scripts/psy/check-ir-coverage-manifest.py lake build PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/counter-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-storage-array-smoke.sh ``` Result: * Both representative Dargo smokes generate packages through the shared writer, then pass `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy-manifest validation, and artifact metadata validation. * Existing metadata source/package-source parity and `Dargo.toml` manifest validation continue to pass. Known limitations: * This factors local Dargo package creation only; upstream compressed genesis deploy JSON and live node/prover smoke remain separate deployment work. Next step: * Continue toward upstream genesis deploy JSON/local node research. ### Psy Dargo Package Source Metadata Commit: feature commit for Psy Dargo package source metadata Summary: * Extended Psy artifact metadata to record the Dargo package source copy (`src/main.psy`) used by every Dargo-backed smoke fixture. * Updated metadata validation to check the package source path, byte size, SHA-256 hash, and hash parity with the generated `.psy` source. * Updated all Dargo-backed Psy smoke scripts to pass `"$PROJECT_DIR/src/main.psy"` into `write-artifact-metadata.py`. Validation run: ```sh theme={null} PYTHONDONTWRITEBYTECODE=1 python3 -m py_compile \ scripts/psy/write-artifact-metadata.py \ scripts/psy/validate-artifact-metadata.py \ scripts/psy/check-ir-coverage-manifest.py bash -n scripts/psy/*.sh lake build PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/counter-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-storage-array-smoke.sh ``` Result: * Counter and U32StorageArrayProbe smoke metadata now include `artifacts.packageSource`. * The metadata validator accepts the updated schema and proves the package source copy has the same SHA-256 hash as the generated source file. Known limitations: * This validates the generated Dargo package source copy, not upstream compressed genesis deploy JSON or live node/prover state. Next step: * Continue toward upstream genesis deploy JSON/local node research, or factor the repeated Dargo package generation into a reusable package writer. ### Psy Dargo Package Manifest Metadata Commit: feature commit for Psy Dargo package manifest metadata Summary: * Extended Psy artifact metadata to record the generated Dargo package manifest (`Dargo.toml`) for every Dargo-backed smoke fixture. * Updated metadata validation to check the manifest path, byte size, SHA-256 hash, `[package]` section, `type = "bin"`, and `[dependencies]` section. * Updated all Dargo-backed Psy smoke scripts to pass the generated `"$PROJECT_DIR/Dargo.toml"` into `write-artifact-metadata.py`. Validation run: ```sh theme={null} python3 -m py_compile \ scripts/psy/write-artifact-metadata.py \ scripts/psy/validate-artifact-metadata.py bash -n scripts/psy/*.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/counter-smoke.sh ``` Result: * Counter smoke metadata now includes `artifacts.dargoManifest` with a checked hash and package manifest shape. * The metadata validator accepts the updated schema after Dargo `test`, `compile`, `execute`, `generate-abi`, deploy manifest validation, and package manifest validation. Known limitations: * This records the generated Dargo package manifest, not Psy upstream compressed genesis deploy JSON or live node/prover state. Next step: * Continue toward upstream genesis deploy JSON/local node research, or factor the repeated Dargo package generation into a reusable package writer. ### Psy IR Coverage Manifest Gate Commit: feature commit for Psy IR coverage manifest validation Summary: * Added `Tests/PsyCoverage.tsv` as a constructor-level coverage manifest for the portable IR surface used by the Psy backend. * Added `scripts/psy/check-ir-coverage-manifest.py`, which parses `ProofForge/IR/Contract.lean` and fails if any tracked constructor is missing from the manifest or if the manifest contains stale/duplicate entries. * Added CI and validation docs for the new gate so future IR expansion must classify each constructor as lowered, validated, unsupported, or structural. Validation run: ```sh theme={null} python3 -m py_compile scripts/psy/check-ir-coverage-manifest.py scripts/psy/check-ir-coverage-manifest.py ``` Result: * The checker reports 88 constructor entries matching `ProofForge/IR/Contract.lean`. Known limitations: * The manifest is a structural guard, not behavioral proof. Supported rows still require fixture, golden, Dargo, and metadata validation when they describe runtime behavior. Next step: * Continue closing behavioral Psy gaps and use the manifest as a tripwire when extending the portable IR. ### Psy U32 Storage Array Lowering Commit: feature commit for Psy U32 storage array coverage Summary: * Added `U32StorageArrayProbe` as a dedicated portable IR fixture for U32 storage-array reads and writes. * Extended Psy sourcegen so portable U32 storage arrays lower to Felt-backed Psy storage arrays. Writes use `u32 as Felt`; reads use `.get() as u32`. * Reused the same representation for generic storage-path read/write effects over U32 array elements. * Kept U32 storage-path compound assignment explicitly rejected, because direct Felt storage `+=` would not preserve a clear U32 storage arithmetic boundary. * Added CLI, golden source, CI golden coverage, diagnostic coverage, Dargo smoke coverage, and validation docs for the new fixture. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-u32-storage-array-ir-psy -o build/psy/U32StorageArrayProbe.psy diff -u Examples/Psy/U32StorageArrayProbe.golden.psy build/psy/U32StorageArrayProbe.psy scripts/psy/diagnostic-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-storage-array-smoke.sh ``` Result: * Generated U32StorageArrayProbe source matches the checked-in golden fixture. * `scripts/psy/diagnostic-smoke.sh` passes all 43 diagnostic cases. * `scripts/psy/u32-storage-array-smoke.sh` passes `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest validation, and artifact metadata validation. * Dargo execution returns `result_vm: [48]` for `storage_lifecycle`. Known limitations: * Direct Psy `[u32; N]` contract storage arrays remain avoided because current `psyup` 0.1.0 rejects them with an `ArrayRef` mismatch. * U32 storage-path compound assignment is still unsupported; use explicit read/update/write. Next step: * Move the Psy deployment track toward upstream compressed genesis deploy JSON and local node/prover smoke work, or continue broadening Lean-to-IR extraction into the now-supported Psy surface. ### Psy Storage Compound Assignment Effects Commit: feature commit for Psy storage-reference compound assignment effects Summary: * Added portable IR storage effects for scalar storage compound assignment and generic storage-path compound assignment. * Extended Psy sourcegen to lower storage refs such as `c.total += 3`, `c.person.profile.age += 2`, and `c.people[1].score -= 9` to native Psy assignment operators. * Kept EVM IR v0 behavior explicit by rejecting the new storage compound effects with target-specific diagnostics. * Extended `StorageNestedAggregateProbe` to validate scalar storage compound assignment, nested scalar storage paths, and storage-array scalar paths under Dargo execution. * Added Psy diagnostics for storage compound effects used as expressions and malformed storage compound assignment value types. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-storage-nested-aggregate-ir-psy -o build/psy/StorageNestedAggregateProbe.psy diff -u Examples/Psy/StorageNestedAggregateProbe.golden.psy build/psy/StorageNestedAggregateProbe.psy scripts/psy/diagnostic-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/storage-nested-aggregate-smoke.sh ``` Result: * Generated StorageNestedAggregateProbe source matches the checked-in golden fixture. * `scripts/psy/diagnostic-smoke.sh` passes all 42 diagnostic cases. * `scripts/psy/storage-nested-aggregate-smoke.sh` passes `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest validation, and artifact metadata validation. * Dargo execution returns `result_vm: [229]` for `storage_nested_lifecycle`. Known limitations: * Map storage values remain excluded from compound assignment because the current supported map shape uses `get`/`set` over `Map`. * U32 storage arrays remain explicitly rejected until a stable Dargo-compatible storage idiom is identified. Next step: * Continue with U32 storage-array research or move toward upstream genesis deploy JSON/local node smoke work. ### Psy Compound Assignment Lowering Commit: feature commit for Psy compound assignment lowering Summary: * Added first-class `AssignOp` and `Statement.assignOp` nodes to the portable IR for `+=`, `-=`, `*=`, `/=`, `%=`, `|=`, `&=`, `^=`, `<<=`, and `>>=`. * Lowered compound assignments to native Psy assignment operators for mutable local, array-index, and field-path assignment targets. * Kept EVM IR v0 explicit by rejecting compound assignment statements with a dedicated diagnostic. * Extended `U32ArithmeticProbe` with arithmetic compound assignment coverage and `BitwiseProbe` with Felt/U32 bitwise and shift compound assignment coverage. * Added Psy diagnostics for malformed compound assignment value types and immutable compound assignment targets. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-u32-arithmetic-ir-psy -o build/psy/U32ArithmeticProbe.psy diff -u Examples/Psy/U32ArithmeticProbe.golden.psy build/psy/U32ArithmeticProbe.psy lake env proof-forge --emit-bitwise-ir-psy -o build/psy/BitwiseProbe.psy diff -u Examples/Psy/BitwiseProbe.golden.psy build/psy/BitwiseProbe.psy scripts/psy/diagnostic-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-arithmetic-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/bitwise-smoke.sh ``` Result: * Generated U32ArithmeticProbe and BitwiseProbe sources match the checked-in golden fixtures. * `scripts/psy/diagnostic-smoke.sh` passes all 39 diagnostic cases. * Dargo validates the updated U32ArithmeticProbe and BitwiseProbe sources with `test`, `compile`, `execute`, `generate-abi`, deploy manifest validation, and artifact metadata validation. Known limitations: * Compound assignment currently targets mutable local/aggregate assignment paths. Storage-reference compound assignment remains a separate design item because portable storage writes are modeled as effects. * U32 storage arrays remain explicitly rejected until a stable Dargo-compatible storage idiom is identified. Next step: * Continue with U32 storage-array research or add storage-reference compound assignment effects if that becomes the next Psy surface to close. ### Psy Map Storage Path Lowering Commit: feature commit for Psy map storage path coverage Summary: * Added `StoragePathSegment.mapKey` to the portable IR so generic storage path effects can target supported `Map` state. * Extended Psy storage path type resolution, validation, and source lowering so `storagePathRead "balances" #[.mapKey key]` lowers to `c.balances.get(key)` and `storagePathWrite "balances" #[.mapKey key] value` lowers to `c.balances.set(key, value)`. * Added map path key validation and explicit diagnostics for malformed map paths or wrong key types. * Extended `MapProbe` with `path_lifecycle`, updated its golden `.psy`, and updated `scripts/psy/map-smoke.sh` to execute both direct map effects and the generic map storage path entrypoint. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-map-ir-psy -o build/psy/MapProbe.psy diff -u Examples/Psy/MapProbe.golden.psy build/psy/MapProbe.psy scripts/psy/diagnostic-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/map-smoke.sh ``` Result: * Generated MapProbe source matches the checked-in golden fixture. * `scripts/psy/diagnostic-smoke.sh` passes all 37 diagnostic cases. * `scripts/psy/map-smoke.sh` passes `dargo test`, `dargo compile`, `dargo execute`, `dargo generate-abi`, deploy manifest validation, and artifact metadata validation. * Dargo execution returns `result_vm: [55, 66, 77, 88]` for `map_lifecycle` and `result_vm: [77, 88, 99, 111]` for `path_lifecycle`. Known limitations: * Map storage paths currently support direct `Map` key access. Nested map value traversal remains unsupported because Psy IR v0 only accepts Hash map values. * U32 storage arrays remain explicitly rejected until a stable Dargo-compatible storage idiom is identified. Next step: * Continue with U32 storage-array research or decide whether compound assignment should become IR sugar. ### Psy Deploy Manifests For All Dargo Smokes Commit: feature commit for broad Psy deploy manifest coverage Summary: * Added `scripts/psy/write-smoke-deploy-manifest.sh` as the shared smoke helper for deploy manifest generation and validation. * Updated every Dargo-backed Psy smoke script to write `target/proof-forge-deploy.json`, validate it, and record it as `deployJson` inside `target/proof-forge-artifact.json`. * Restored each smoke's deploy-oriented `dargo compile` artifact after `dargo execute` and `dargo generate-abi`, so deploy manifests describe the compile method set rather than an execution trace. * Kept `scripts/psy/diagnostic-smoke.sh` separate because it validates pre-codegen diagnostics and does not produce Dargo artifacts. * Updated validation docs, target notes, and backlog so the remaining deployment gap is specifically upstream compressed genesis deploy JSON plus local node/prover execution. Validation run: ```sh theme={null} python3 -m py_compile \ scripts/psy/write-deploy-manifest.py \ scripts/psy/validate-deploy-manifest.py \ scripts/psy/write-artifact-metadata.py \ scripts/psy/validate-artifact-metadata.py git diff --check lake build export PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy export DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo for script in scripts/psy/*-smoke.sh; do case "$script" in scripts/psy/diagnostic-smoke.sh) ;; *) "$script" ;; esac done scripts/psy/diagnostic-smoke.sh ``` Result: * All Dargo-backed Psy smokes generated DPN circuit JSON, ABI JSON, execute logs, `proof-forge-deploy.json`, and `proof-forge-artifact.json`. * Artifact metadata validation now checks deploy-manifest file hashes whenever `deployJson` is present. * Deploy manifests record the restored compile method set for each fixture. * `scripts/psy/diagnostic-smoke.sh` still passes all 35 diagnostic cases. Known limitations: * `proof-forge-deploy.json` remains ProofForge-owned metadata, not the upstream compressed genesis deploy JSON consumed by Psy node setup. * The local node/prover deployment smoke is still not implemented. Next step: * Research whether to vendor or wrap Psy's `gen_deploy_json` path, then add the smallest local node/prover smoke that consumes the resulting deployment package. ### Psy Counter Deploy Manifest Metadata Commit: feature commit for Psy Counter deploy manifest coverage Summary: * Added `scripts/psy/write-deploy-manifest.py` to produce `proof-forge-deploy.json` from the Counter `.psy` source, Dargo circuit JSON, and Dargo ABI JSON. * Added `scripts/psy/validate-deploy-manifest.py` to verify manifest schema, deployer format, state-tree height, source/circuit/ABI hashes, function whitelist ordering, and upstream genesis JSON status. * Updated `scripts/psy/counter-smoke.sh` so the Counter Dargo smoke now writes and validates `target/proof-forge-deploy.json`. * Re-runs `dargo compile` after `dargo execute` so deploy metadata points at the deploy-oriented compile artifact rather than the method-sequence execution trace. * Extended Psy artifact metadata to optionally record `deployJson` and require `validation.deployManifest = "passed"` whenever that artifact is present. * Documented that this is a ProofForge deploy manifest, not Psy's upstream compressed genesis deploy JSON from `gen_deploy_json`. Validation run: ```sh theme={null} python3 -m py_compile \ scripts/psy/write-deploy-manifest.py \ scripts/psy/validate-deploy-manifest.py \ scripts/psy/write-artifact-metadata.py \ scripts/psy/validate-artifact-metadata.py git diff --check PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/counter-smoke.sh ``` Result: * Counter generated source still matches `Examples/Psy/Counter.golden.psy`. * Dargo `test`, `compile`, `execute`, and `generate-abi` passed. * `dargo execute` returned `result_vm: [2]` after initialize plus two increments. * `proof-forge-deploy.json` and `proof-forge-artifact.json` were generated and validated. Known limitations: * The manifest is ProofForge-owned metadata, not the upstream compressed genesis deploy JSON consumed by Psy node setup. * The upstream `psy-dargo-cli/examples/gen_deploy_json.rs` path still requires Rust workspace internals; current released `dargo` does not expose it as a subcommand. * Only the Counter smoke emits deploy manifest metadata so far. Next step: * Either extend deploy manifest generation to the broader Psy fixture set, or research the smallest stable upstream boundary for genesis deploy JSON plus a local Psy node/prover smoke. ### Psy U32HashPackingProbe Dynamic Hash Construction Commit: feature commit for Psy U32 hash packing coverage Summary: * Added portable IR `Expr.hashValue` for dynamic `Hash` construction from four Felt-backed limbs. * Extended Psy type validation so each dynamic Hash part must be `U64`/Felt and malformed Hash construction fails before `.psy` generation. * Kept EVM IR v0 explicit by rejecting dynamic Hash value construction with a clear diagnostic. * Added `ProofForge.IR.Examples.U32HashPackingProbe`, aligned with the `[u32; 8]` limb packing idioms in the deposit-tree and mining-rewards precompiles. * Covered both local `[u32; 8]` literals and U32 ABI parameters packed into Psy `Hash` values through `lo + hi * 2^32`. * Added an explicit rejection diagnostic for U32 storage arrays after Dargo validation showed current `psyup` 0.1.0 rejects direct `[u32; N]` contract storage arrays with an `ArrayRef` type mismatch. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-u32-hash-packing-ir-psy -o build/psy/U32HashPackingProbe.psy ``` * Added `Examples/Psy/U32HashPackingProbe.golden.psy`. * Added `scripts/psy/u32-hash-packing-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, two `dargo execute` checks, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the U32HashPackingProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-u32-hash-packing-ir-psy -o build/psy/U32HashPackingProbe.psy diff -u Examples/Psy/U32HashPackingProbe.golden.psy build/psy/U32HashPackingProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-hash-packing-smoke.sh ``` Result: * Generated U32HashPackingProbe source matches the checked-in golden fixture. * `scripts/psy/u32-hash-packing-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned the expected four-Felt Hash values for both `pack_literal` and `pack_params`. * `scripts/psy/diagnostic-smoke.sh` passed all 35 diagnostic cases. Known limitations: * This adds Hash value construction and U32 limb packing, not Psy deploy JSON or live node/prover execution. * U32 storage arrays are explicitly rejected until a stable Psy storage idiom is validated against Dargo. * Compound assignment operators remain represented as explicit assignment plus expression nodes. * Map storage paths remain rejected until a stable Psy idiom is identified. Next step: * Decide whether to add compound assignment as IR sugar or leave it to a future source normalizer, then continue with map storage paths or deploy JSON. ### Psy BitwiseProbe Native Bitwise Expressions Commit: feature commit for Psy bitwise expression coverage Summary: * Added portable IR expression nodes for `&`, `|`, `^`, `<<`, and `>>`. * Extended Psy source generation for Felt-backed `U64` and `U32` bitwise expressions, with same-width numeric validation before `.psy` generation. * Added EVM IR lowering for the same pure bitwise/shift nodes through Yul `and`, `or`, `xor`, `shl`, and `shr` builtins. * Added explicit diagnostics for malformed bitwise and shift operands. * Added `ProofForge.IR.Examples.BitwiseProbe`, aligned with upstream `psy-compiler/tests/opcode_test.psy`, `tests/storage_u32_assign_ops_test.psy`, and precompile Merkle path idioms. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-bitwise-ir-psy -o build/psy/BitwiseProbe.psy ``` * Added `Examples/Psy/BitwiseProbe.golden.psy`. * Added `scripts/psy/bitwise-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the BitwiseProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-bitwise-ir-psy -o build/psy/BitwiseProbe.psy diff -u Examples/Psy/BitwiseProbe.golden.psy build/psy/BitwiseProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/bitwise-smoke.sh ``` Result: * Generated BitwiseProbe source matches the checked-in golden fixture. * `scripts/psy/bitwise-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [16]` for `bitwise_mix`. * `scripts/psy/diagnostic-smoke.sh` passed all 33 diagnostic cases. Known limitations: * Compound assignment operators such as `|=`, `&=`, `^=`, `<<=`, and `>>=` are still represented as explicit assignment plus expression nodes. * This does not yet add u32 storage arithmetic probes or map storage paths. Next step: * Add storage-heavy U32/Hash limb packing probes from the deposit-tree and mining-rewards precompiles, then decide whether compound assignment sugar belongs in the portable IR or only in sourcegen normalization. ### Psy U32ArithmeticProbe Native U32 Arithmetic Commit: feature commit for Psy U32 arithmetic coverage Summary: * Added portable IR `ValueType.u32` and `Literal.u32`. * Added portable IR expression nodes for division, modulo, exponentiation, and explicit casts. * Extended Psy source generation for `u32`, `Nu32` literals, `/`, `%`, `**`, and casts such as `z as bool` and `bb as Felt`. * Updated bounded-loop typing so generated `for i in 0u32..Nu32` loop indices are tracked as `U32`. * Extended numeric type validation so `U32` arithmetic remains type-consistent and malformed mixed-width arithmetic fails before source generation. * Added EVM IR lowering for the new pure arithmetic/cast nodes through Yul builtins or no-op casts. * Added `ProofForge.IR.Examples.U32ArithmeticProbe`, mirroring the core executable shape of upstream `psy-compiler/tests/u32_test.psy`. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-u32-arithmetic-ir-psy -o build/psy/U32ArithmeticProbe.psy ``` * Added `Examples/Psy/U32ArithmeticProbe.golden.psy`. * Added `scripts/psy/u32-arithmetic-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute --parameters 2,3`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the U32ArithmeticProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-u32-arithmetic-ir-psy -o build/psy/U32ArithmeticProbe.psy diff -u Examples/Psy/U32ArithmeticProbe.golden.psy build/psy/U32ArithmeticProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/u32-arithmetic-smoke.sh ``` Result: * Generated U32ArithmeticProbe source matches the checked-in golden fixture. * `scripts/psy/u32-arithmetic-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute --parameters 2,3` returned `result_vm: [1]` for `u32_arithmetic`. * `scripts/psy/diagnostic-smoke.sh` passed all 31 diagnostic cases. Known limitations: * This does not yet add bitwise shifts, bitwise and/or, u32 storage probes, or the full cast matrix used by the token/deposit-tree precompiles. * Cast lowering is intentionally explicit and rejects unsupported source/target pairs before `.psy` source generation. Next step: * Add bitwise operations and u32 array/hash-packing probes, since the Psy precompiles use `u32` limbs heavily for token addresses and tree roots. ### Psy ArithmeticProbe Sub/Mul Expressions Commit: feature commit for Psy arithmetic expression coverage Summary: * Added portable IR expression nodes for subtraction and multiplication. * Added Psy source generation for `-` and `*`, including parentheses around nested arithmetic operands where precedence would otherwise change meaning. * Added sourcegen diagnostics for malformed subtraction and multiplication operand types. * Added EVM IR lowering for the same pure arithmetic nodes through Yul builtins. * Added `ProofForge.IR.Examples.ArithmeticProbe`, covering subtraction, multiplication, and nested arithmetic precedence. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-arithmetic-ir-psy -o build/psy/ArithmeticProbe.psy ``` * Added `Examples/Psy/ArithmeticProbe.golden.psy`. * Added `scripts/psy/arithmetic-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the ArithmeticProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-arithmetic-ir-psy -o build/psy/ArithmeticProbe.psy diff -u Examples/Psy/ArithmeticProbe.golden.psy build/psy/ArithmeticProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/arithmetic-smoke.sh ``` Result: * Generated ArithmeticProbe source matches the checked-in golden fixture. * `scripts/psy/arithmetic-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [60]` for `arithmetic_mix`. * `scripts/psy/diagnostic-smoke.sh` passed all 29 diagnostic cases. Known limitations: * This adds subtraction and multiplication, not division, modulo, exponentiation, cast-heavy `u32` arithmetic, or compound assignment operators. * The IR still represents these values as `U64` mapped to Psy `Felt`; a dedicated `U32` surface should be added before copying upstream `u32_test` semantics directly. Next step: * Add division/modulo only after deciding whether they belong to Felt-backed `U64`, a new `U32` value type, or target-specific checked arithmetic helpers. ### Psy ConditionalProbe Statement If/Else Commit: feature commit for Psy conditional statement coverage Summary: * Added portable IR `Statement.ifElse` with a new `control.conditional` capability. * Added Psy source generation for `if condition { ... } else { ... };`, aligned with upstream `.psy` conditional syntax. * Added sourcegen diagnostics for non-Bool if conditions and branch-local bindings escaping their branch. * Kept EVM IR v0 explicit by rejecting statement-level if/else. * Added `ProofForge.IR.Examples.ConditionalProbe`, covering then and else branch execution over scalar storage. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-conditional-ir-psy -o build/psy/ConditionalProbe.psy ``` * Added `Examples/Psy/ConditionalProbe.golden.psy`. * Added `scripts/psy/conditional-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the ConditionalProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-conditional-ir-psy -o build/psy/ConditionalProbe.psy diff -u Examples/Psy/ConditionalProbe.golden.psy build/psy/ConditionalProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/conditional-smoke.sh ``` Result: * Generated ConditionalProbe source matches the checked-in golden fixture. * `scripts/psy/conditional-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [10]` for `conditional_lifecycle`. * `scripts/psy/diagnostic-smoke.sh` passed all 27 diagnostic cases. Known limitations: * This adds statement-level if/else, not else-if syntax sugar. * Non-unit entrypoints still need an explicit final top-level return statement; return coverage through both conditional branches is not analyzed yet. Next step: * Continue broadening Psy expression/arithmetic coverage or add map storage path support once a stable upstream Psy idiom is identified. ### Psy ExpressionPredicateProbe Boolean Predicates Commit: feature commit for Psy predicate expression coverage Summary: * Added portable IR expression nodes for equality, inequality, ordering comparisons, boolean conjunction, boolean disjunction, and boolean negation. * Added Psy lowering using upstream `.psy` idioms: `==`, `!=`, `<`, `<=`, `>`, `>=`, `&&`, `||`, and `!`. * Added sourcegen type diagnostics for malformed equality, comparison, and boolean operator operands. * Added EVM IR lowering for the same pure predicate nodes through Yul builtins. * Added `ProofForge.IR.Examples.ExpressionPredicateProbe`, covering predicate locals and assertion predicates. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-expression-predicate-ir-psy -o build/psy/ExpressionPredicateProbe.psy ``` * Added `Examples/Psy/ExpressionPredicateProbe.golden.psy`. * Added `scripts/psy/expression-predicate-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the ExpressionPredicateProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-expression-predicate-ir-psy -o build/psy/ExpressionPredicateProbe.psy diff -u Examples/Psy/ExpressionPredicateProbe.golden.psy build/psy/ExpressionPredicateProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/expression-predicate-smoke.sh ``` Result: * Generated ExpressionPredicateProbe source matches the checked-in golden fixture. * `scripts/psy/expression-predicate-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [16]` for `predicate_sum`. * `scripts/psy/diagnostic-smoke.sh` passed all 25 diagnostic cases. Known limitations: * This adds expression predicates, not statement-level `if/else` lowering. * Fixed-array equality was outside this original expression fixture; it is now covered separately by the Dargo-backed `ArrayProbe`. Next step: * Add statement-level conditional lowering or broaden arithmetic expression coverage with upstream/Dargo fixtures. ### Psy Sourcegen Type Diagnostics Commit: feature commit for Psy expression and statement type diagnostics Summary: * Added a lightweight Psy backend type environment for entrypoint parameters, local bindings, mutable locals, and bounded-loop indices. * Added sourcegen-time type inference and validation for literals, locals, fixed arrays, struct literals, field access, addition, hash operations, storage effects, context reads, assignment targets, assertions, and returns. * Added diagnostics for unknown locals, local/array/struct/hash type mismatches, immutable assignment, missing non-unit returns, and storage write type mismatches. * Kept existing lowering behavior unchanged for valid fixtures; this feature blocks malformed IR before `.psy` source is emitted. * Extended `Tests/PsyDiagnostics.lean` from 12 to 22 explicit rejection cases. Validation run: ```sh theme={null} lake build scripts/psy/diagnostic-smoke.sh lake env proof-forge --emit-counter-ir-psy -o build/psy/Counter.psy diff -u Examples/Psy/Counter.golden.psy build/psy/Counter.psy lake env proof-forge --emit-storage-nested-aggregate-ir-psy -o build/psy/StorageNestedAggregateProbe.psy diff -u Examples/Psy/StorageNestedAggregateProbe.golden.psy build/psy/StorageNestedAggregateProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/{counter,context,hash,map,assert,loop,array,struct,struct-array,abi-aggregate,nested-aggregate,storage-nested-aggregate}-smoke.sh ``` Result: * `scripts/psy/diagnostic-smoke.sh` passed all 22 diagnostic cases. * All checked Psy golden source snapshots remain unchanged. * All Psy Dargo smokes passed and revalidated source snapshots, DPN JSON, ABI JSON, execute logs, and `proof-forge-artifact.json`. Known limitations: * This is a sourcegen validation layer, not a formal type system for every future portable IR extension. * Assignment mutability is enforced for local/index/field paths rooted in local bindings; storage mutation continues to use explicit storage effects. Next step: * Continue closing Psy valid-surface gaps with either Dargo-backed fixtures or explicit diagnostics before adding new IR nodes. ### Psy StorageNestedAggregateProbe Storage Paths Commit: feature commit for storage nested aggregate Psy IR coverage Summary: * Added generic storage path read/write effects to the portable IR. * Added `StructField.isRef` so the IR can explicitly model Psy `#[ref]` fields for nested storage references. * Added Psy lowering for storage paths such as `c.person.profile.age` and `c.people[1].profile.age`, plus validation for empty paths and missing nested `#[ref]` markers. * Kept EVM IR v0 behavior explicit by rejecting storage path effects. * Added `ProofForge.IR.Examples.StorageNestedAggregateProbe`, covering scalar struct storage and fixed storage arrays of structs. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-storage-nested-aggregate-ir-psy -o build/psy/StorageNestedAggregateProbe.psy ``` * Added `Examples/Psy/StorageNestedAggregateProbe.golden.psy`. * Added `scripts/psy/storage-nested-aggregate-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Extended `Tests/PsyDiagnostics.lean` with invalid storage path cases. * Added CI coverage for the StorageNestedAggregateProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-storage-nested-aggregate-ir-psy -o build/psy/StorageNestedAggregateProbe.psy diff -u Examples/Psy/StorageNestedAggregateProbe.golden.psy build/psy/StorageNestedAggregateProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/storage-nested-aggregate-smoke.sh scripts/psy/diagnostic-smoke.sh ``` Result: * Generated StorageNestedAggregateProbe source matches the checked-in golden fixture. * `scripts/psy/storage-nested-aggregate-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [220]` for `storage_nested_lifecycle`. * `scripts/psy/diagnostic-smoke.sh` passed all 12 diagnostic cases. Known limitations: * Storage path lowering intentionally rejects map storage paths until a stable Psy idiom is identified and covered by an upstream-style fixture. * This does not yet produce deploy JSON or exercise a live Psy node/prover. Next step: * Research deploy JSON/live node execution for Psy artifacts, or continue expanding expression/path coverage behind diagnostic gates. ### Psy NestedAggregateProbe Mixed Aggregate Updates Commit: feature commit for nested aggregate Psy IR coverage Summary: * Added portable IR statements for mutable local bindings and assignment. * Added Psy lowering for `let mut` and nested assignment targets made from local names, array indexes, and field paths. * Kept EVM IR v0 behavior explicit by rejecting mutable local bindings and assignment statements. * Added `ProofForge.IR.Examples.NestedAggregateProbe`, covering a mutable `[Family; 2]` value whose `Family.children` field is `[Member; 2]`. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-nested-aggregate-ir-psy -o build/psy/NestedAggregateProbe.psy ``` * Added `Examples/Psy/NestedAggregateProbe.golden.psy`. * Added `scripts/psy/nested-aggregate-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Extended `Tests/PsyDiagnostics.lean` with an invalid assignment target case. * Added CI coverage for the NestedAggregateProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-nested-aggregate-ir-psy -o build/psy/NestedAggregateProbe.psy diff -u Examples/Psy/NestedAggregateProbe.golden.psy build/psy/NestedAggregateProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/nested-aggregate-smoke.sh scripts/psy/diagnostic-smoke.sh ``` Result: * `lake build` passed. * Generated NestedAggregateProbe source matches the checked-in golden fixture. * `scripts/psy/nested-aggregate-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [51]` for `nested_update_sum`. * `scripts/psy/diagnostic-smoke.sh` passed all 10 diagnostic cases. Known limitations: * This feature covers local nested aggregate mutation, not storage-backed nested aggregate mutation. * Assignment targets are intentionally limited to local/index/field paths. Next step: * Add storage-backed nested aggregate updates or deploy JSON metadata. ### Psy Unsupported Diagnostic Gate Commit: feature commit for Psy diagnostic regression coverage Summary: * Added `Tests/PsyDiagnostics.lean`, a runnable Lean diagnostic regression suite for Psy IR rejection paths. * Added `scripts/psy/diagnostic-smoke.sh`. * Covered explicit diagnostics for: * Unit entrypoint parameters * zero-length ABI fixed arrays * unknown ABI struct types * unsupported map key/value shapes * structs used in storage without `deriveStorage` * empty struct declarations * invalid bounded loop ranges * storage writes used as expressions * storage reads used as statements * invalid assignment targets * Added the diagnostic smoke to CI. * Documented the gate in README, validation gates, and `psy-dpn` target notes. Validation run: ```sh theme={null} scripts/psy/diagnostic-smoke.sh lake build ``` Result: * `scripts/psy/diagnostic-smoke.sh` passed all 10 diagnostic cases. * `lake build` passed. Known limitations: * This is a regression gate for representative unsupported shapes, not an exhaustive formal proof over every impossible IR construction. * Cross-target capability rejection matrices still need broader coverage. Next step: * Expand diagnostics as new Psy IR nodes are added, then continue with deeper mixed aggregate update coverage or deploy JSON metadata. ### Psy AbiAggregateProbe ABI Aggregates Commit: feature commit for ABI aggregate Psy IR coverage Summary: * Added entrypoint ABI type validation for Psy IR parameters and returns. * Rejected Unit parameters before source generation, while keeping Unit returns valid for void methods. * Validated entrypoint fixed-array ABI types as non-empty and struct ABI types as declared. * Added `ProofForge.IR.Examples.AbiAggregateProbe`, covering a struct parameter, fixed-array parameter, and struct return value. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-abi-aggregate-ir-psy -o build/psy/AbiAggregateProbe.psy ``` * Added `Examples/Psy/AbiAggregateProbe.golden.psy`. * Added `scripts/psy/abi-aggregate-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, three `dargo execute` calls, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the AbiAggregateProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-abi-aggregate-ir-psy -o build/psy/AbiAggregateProbe.psy diff -u Examples/Psy/AbiAggregateProbe.golden.psy build/psy/AbiAggregateProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/abi-aggregate-smoke.sh ``` Result: * `lake build` passed. * Generated AbiAggregateProbe source matches the checked-in golden fixture. * `scripts/psy/abi-aggregate-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [15]` for `sum_pair`. * `dargo execute` returned `result_vm: [6]` for `sum_array`. * `dargo execute` returned `result_vm: [9, 4]` for `make_pair`. Known limitations: * Dargo CLI aggregate execution is flattened to Felt vectors. * This feature validates flat struct and one-dimensional fixed-array ABI shapes, not deeply nested mixed aggregate ABI shapes. Next step: * Add deeper nested mixed aggregate update and ABI coverage from the upstream Psy syntax corpus, then continue toward deploy JSON metadata. ### Psy StructArrayProbe Struct Arrays Commit: feature commit for struct-array Psy IR coverage Summary: * Extended portable IR storage effects with indexed storage array struct field read/write nodes. * Extended Psy sourcegen to lower storage arrays of structs, whole struct array element writes, and indexed struct field reads through `.get()`. * Extended Psy state validation so fixed storage arrays can use `deriveStorage` struct element types. * Kept EVM IR v0 behavior explicit by rejecting storage array struct field effects. * Added `ProofForge.IR.Examples.StructArrayProbe`, covering local `[Person; 2]` struct arrays plus fixed storage arrays of structs. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-struct-array-ir-psy -o build/psy/StructArrayProbe.psy ``` * Added `Examples/Psy/StructArrayProbe.golden.psy`. * Added `scripts/psy/struct-array-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, two `dargo execute` calls, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the StructArrayProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-struct-array-ir-psy -o build/psy/StructArrayProbe.psy diff -u Examples/Psy/StructArrayProbe.golden.psy build/psy/StructArrayProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/struct-array-smoke.sh ``` Result: * `lake build` passed. * Generated StructArrayProbe source matches the checked-in golden fixture. * `scripts/psy/struct-array-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [100]` for `local_struct_array_sum`. * `dargo execute` returned `result_vm: [102]` for `storage_struct_array_lifecycle`. Known limitations: * This feature covers one-dimensional arrays of flat structs. * Deeply nested mixed aggregate updates still need dedicated coverage. * EVM IR v0 explicitly rejects struct-array storage field effects. Next step: * Add ABI-facing entrypoint aggregate parameters or return-shape validation, then continue toward deployment/deploy JSON metadata. ### Psy StructProbe Struct Values And Storage Commit: feature commit for struct Psy IR coverage Summary: * Extended portable IR with struct declarations, struct value types, struct literals, and field access expressions. * Registered `data.struct` as a target capability for struct values and field access. * Extended portable IR storage effects with scalar storage struct field read/write nodes. * Extended Psy sourcegen to emit `#[derive(Storage)]` struct declarations, `new Struct { ... }` literals, local field access, scalar storage struct assignment, and storage struct field reads through `.get()`. * Kept EVM IR v0 behavior explicit by rejecting struct literals, field access, struct typed let bindings, struct returns, and storage struct field effects. * Added `ProofForge.IR.Examples.StructProbe`, covering local struct literals plus scalar storage struct read/write behavior. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-struct-ir-psy -o build/psy/StructProbe.psy ``` * Added `Examples/Psy/StructProbe.golden.psy`. * Added `scripts/psy/struct-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, two `dargo execute` calls, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the StructProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-struct-ir-psy -o build/psy/StructProbe.psy diff -u Examples/Psy/StructProbe.golden.psy build/psy/StructProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/struct-smoke.sh ``` Result: * `lake build` passed. * Generated StructProbe source matches the checked-in golden fixture. * `scripts/psy/struct-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [30]` for `local_sum`. * `dargo execute` returned `result_vm: [26]` for `storage_lifecycle`. Known limitations: * This feature covers flat struct values and scalar storage structs. * Struct arrays, nested structs, and methods on structs still need dedicated coverage. * EVM IR v0 explicitly rejects struct IR nodes. Next step: * Combine structs with fixed arrays in a follow-up fixture aligned with upstream `array_test.psy` and `array_ref_struct_index_test.psy`. ### Psy ArrayProbe Fixed Arrays Commit: feature commit for fixed-array Psy IR coverage Summary: * Extended portable IR types with fixed arrays, represented as `[T; N]` in Psy. * Added `data.fixed_array` for fixed-size array values and `storage.array` for fixed array storage fields. * Extended portable IR expressions with fixed array literals and index reads. * Extended portable IR storage effects with fixed array index read/write nodes. * Extended Psy sourcegen to lower local array literals, index reads, storage array writes, and storage array reads through `.get()` when used as values. * Kept EVM IR v0 behavior explicit by rejecting fixed-array literals, index access, storage array effects, and fixed-array returns. * Added `ProofForge.IR.Examples.ArrayProbe`, covering local `[Felt; 3]` literals plus fixed storage array read/write behavior. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-array-ir-psy -o build/psy/ArrayProbe.psy ``` * Added `Examples/Psy/ArrayProbe.golden.psy`. * Added `scripts/psy/array-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, three `dargo execute` calls, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the ArrayProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-array-ir-psy -o build/psy/ArrayProbe.psy diff -u Examples/Psy/ArrayProbe.golden.psy build/psy/ArrayProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/array-smoke.sh ``` Result: * `lake build` passed. * Generated ArrayProbe source matches the checked-in golden fixture. * `scripts/psy/array-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [60]` for `sum_literal`. * `dargo execute` returned `result_vm: [31]` for `storage_lifecycle`. * `dargo execute` returned `result_vm: [1]` for `array_predicates`. Known limitations: * This feature covers one-dimensional fixed arrays over `Felt` and `Hash` storage elements. Struct arrays and nested arrays still need dedicated coverage. * Dynamic arrays and unbounded indexing are still unsupported. * EVM IR v0 explicitly rejects fixed-array IR nodes. Next step: * Add struct coverage next, then combine structs with arrays in a follow-up fixture aligned with upstream `array_test.psy`. ### Psy LoopProbe Bounded Loops Commit: feature commit for bounded-loop Psy IR coverage Summary: * Extended portable IR statements with a static `boundedFor` node. * Registered `control.bounded_loop` as a target capability and enabled it for `psy-dpn`. * Extended Psy sourcegen to lower `boundedFor` to Psy fixed-range `for` loops such as `for _i in 0u32..3u32`. * Kept EVM IR v0 behavior explicit by rejecting bounded loops with a diagnostic. * Added `ProofForge.IR.Examples.LoopProbe`, which resets scalar storage, runs a three-iteration loop, and returns the final count. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-loop-ir-psy -o build/psy/LoopProbe.psy ``` * Added `Examples/Psy/LoopProbe.golden.psy`. * Added `scripts/psy/loop-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the LoopProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-loop-ir-psy -o build/psy/LoopProbe.psy diff -u Examples/Psy/LoopProbe.golden.psy build/psy/LoopProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/loop-smoke.sh ``` Result: * `lake build` passed. * Generated LoopProbe source matches the checked-in golden fixture. * `scripts/psy/loop-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [3]` for `count_to_three`. Known limitations: * Loop lowering is deliberately static and bounded; dynamic or unbounded loops are still unsupported. * The portable IR still lacks array and struct coverage. * EVM IR v0 explicitly rejects bounded loops. Next step: * Add array coverage next, because upstream Psy tests and precompiles use fixed arrays heavily alongside bounded loops. ### Psy AssertProbe IR Assertions Commit: feature commit for dynamic nested EVM local arrays Summary: * Extended portable IR with statement-level `assert` and `assertEq` nodes. * Registered the `assertions` capability for target profiles and artifact metadata. * Extended Psy sourcegen to lower assertion statements into method bodies as `assert(condition, "message")` and `assert_eq(lhs, rhs, "message")`. * Added basic string escaping for generated Psy assertion messages. * Added `ProofForge.IR.Examples.AssertProbe`, which validates assertions inside a contract method body. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-assert-ir-psy -o build/psy/AssertProbe.psy ``` * Added `Examples/Psy/AssertProbe.golden.psy`. * Added `scripts/psy/assert-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the AssertProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-assert-ir-psy -o build/psy/AssertProbe.psy diff -u Examples/Psy/AssertProbe.golden.psy build/psy/AssertProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/assert-smoke.sh ``` Result: * `lake build` passed. * Generated AssertProbe source matches the checked-in golden fixture. * `scripts/psy/assert-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [12]` for `checked_sum(5,7)`. Known limitations: * Assertion conditions still depend on the currently narrow expression subset. * EVM IR v0 rejects assertion statements through capability diagnostics. Next step: * Add bounded-loop coverage next, because loops are heavily used by Psy precompiles and are required for array/tree-style contracts. ### Psy MapProbe Storage Map Coverage Commit: `427a0ec feat: support dynamic nested EVM local arrays` Summary: * Extended portable IR with fixed-capacity map state and `storage.map` effects: `contains`, `get`, `insert`, and `set`. * Extended Psy sourcegen to lower the supported map shape to `Map` and to reject unsupported map key/value types with an explicit diagnostic. * Added `ProofForge.IR.Examples.MapProbe` with scalar fields adjacent to the map to mirror upstream Psy storage-layout regression tests. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-map-ir-psy -o build/psy/MapProbe.psy ``` * Added `Examples/Psy/MapProbe.golden.psy`. * Added `scripts/psy/map-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, `dargo execute`, `dargo generate-abi`, and validates `proof-forge-artifact.json`. * Added CI coverage for the MapProbe Psy golden source snapshot. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-map-ir-psy -o build/psy/MapProbe.psy diff -u Examples/Psy/MapProbe.golden.psy build/psy/MapProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/map-smoke.sh ``` Result: * `lake build` passed. * Generated MapProbe source matches the checked-in golden fixture. * `scripts/psy/map-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [55, 66, 77, 88]` for `map_lifecycle`. Known limitations: * Psy map lowering currently supports only `Map`. * The portable IR still lacks first-class assertions, bounded loops, arrays, and structs. * EVM IR v0 explicitly rejects portable map storage. Next step: * Add IR-level assertions or bounded-loop coverage next, then validate the new node through Psy golden output and Dargo smoke. ### Psy HashProbe And Experimental Target Slice Commit: test commit for EVM SDK example golden Yul fixtures Summary: * Extended portable IR with `Hash`, four-Felt hash literals, typed `let` bindings, `hash`, and `hash_two_to_one` expressions. * Extended Psy sourcegen to lower hash values through upstream Psy idioms: `Hash`, `[a, b, c, d]`, `hash(data)`, and `hash_two_to_one(left, right)`. * Added `ProofForge.IR.Examples.HashProbe` with two contract methods: `poseidon_hash` and `poseidon_pair_hash`. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-hash-ir-psy -o build/psy/HashProbe.psy ``` * Added `Examples/Psy/HashProbe.golden.psy`. * Added `scripts/psy/hash-smoke.sh`, which generates a temporary Dargo package, runs `dargo test --file`, `dargo compile`, two `dargo execute` calls, `dargo generate-abi`, and writes `proof-forge-artifact.json`. * Added `scripts/psy/validate-artifact-metadata.py`; the Counter, ContextProbe, and HashProbe smokes now validate artifact hashes, byte sizes, capability records, validation flags, and expected execution results. * Added CI coverage for Psy golden source generation without requiring Dargo on GitHub Actions. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-hash-ir-psy -o build/psy/HashProbe.psy diff -u Examples/Psy/HashProbe.golden.psy build/psy/HashProbe.psy PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/counter-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/context-smoke.sh PSY_HOME=/tmp/proof_forge_refs/psyup-home-test/.psy \ DARGO=/tmp/proof_forge_refs/psyup-home-test/.psy/toolchains/psy-0.1.0/bin/dargo \ scripts/psy/hash-smoke.sh ``` Result: * `lake build` passed. * Generated HashProbe source matches the checked-in golden fixture. * `scripts/psy/hash-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * All three Psy smoke scripts validated `proof-forge-artifact.json` against the generated files and expected execution output. * `dargo execute` returned the expected four-Felt output for `poseidon_hash`. * `dargo execute` returned the expected four-Felt output for `poseidon_pair_hash`. Known limitations: * Hash support is deliberately narrow: fixed four-Felt `Hash` values only. * Psy storage maps, bounded loops, and deploy JSON are still not implemented. * EVM IR v0 explicitly rejects Hash values and hash expressions. Next step: * Add map/storage-map coverage from upstream `psy-compiler/tests` and `psy-precompiles`, then factor the repeated Dargo package generation logic. ### Psy ContextProbe Fixture And Artifact Metadata Commit: pending Summary: * Extended portable IR with `context.read` effects for `userId`, `contractId`, and `checkpointId`. * Extended Psy sourcegen to lower entrypoint parameters and context reads. * Added `ProofForge.IR.Examples.ContextProbe`, the first non-Counter Psy IR fixture. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-context-ir-psy -o build/psy/ContextProbe.psy ``` * Added `Examples/Psy/ContextProbe.golden.psy`. * Added `scripts/psy/context-smoke.sh`, which mirrors the Counter Dargo smoke: `dargo test --file`, `dargo compile`, `dargo execute`, and `dargo generate-abi`. * Added `scripts/psy/write-artifact-metadata.py` and wired both Psy smoke scripts to emit `proof-forge-artifact.json` with hashes for source, circuit JSON, ABI JSON, and execute logs. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-context-ir-psy -o build/psy/ContextProbe.psy diff -u Examples/Psy/ContextProbe.golden.psy build/psy/ContextProbe.psy scripts/psy/context-smoke.sh scripts/psy/counter-smoke.sh git diff --check ``` Result: * `lake build` passed. * ContextProbe emits reviewable Psy source with parameters and context reads. * Generated ContextProbe source matches the checked-in golden fixture. * `scripts/psy/context-smoke.sh` generated DPN JSON, ABI JSON, execute log, and `proof-forge-artifact.json`. * `dargo execute` returned `result_vm: [15]` for `sum_context(2,3)`. * `scripts/psy/counter-smoke.sh` now also emits `proof-forge-artifact.json`. Known limitations: * ContextProbe uses `_proof_forge_marker` storage because Dargo v0.1.0 panics on an empty `#[contract] #[derive(Storage)]` struct. * The IR still lacks maps, fixed arrays, assertions, hashes, bounded loops, and reusable package generation. * Dargo does not expose a `--version` flag, so metadata records the Dargo path and leaves the version null for now. Next step: * Add a curated upstream syntax regression subset from `psy-compiler/tests`, then expand the IR/sourcegen surface toward maps, arrays, assertions, and hashes. ## 2026-06-30 ### Psy Counter IR Sourcegen And Smoke Commit: pending Summary: * Added `ProofForge.Backend.Psy.IR`, a strict v0 source generator for the hand-written portable Counter IR fixture. * Added CLI support: ```sh theme={null} lake env proof-forge --emit-counter-ir-psy -o build/psy/Counter.psy ``` * Added `Examples/Psy/Counter.golden.psy` as the reviewed source snapshot. * Added `scripts/psy/counter-smoke.sh`, which: * regenerates Counter Psy source * compares it against the golden fixture * runs `dargo test --file` * creates a temporary Dargo package * runs `dargo compile --contract-name Counter --method-names initialize increment get` * checks the Dargo JSON artifact is non-empty * runs `dargo execute --contract-name Counter --method-names initialize increment increment get` * checks the local execution log contains `result_vm: [2]` * runs `dargo generate-abi --contract-name Counter --output-dir target --pretty` * checks the ABI JSON artifact is non-empty * Verified `psyup install 0.1.0` as a working macOS arm64 toolchain path for this smoke. * Recorded the upstream syntax/CI corpus: `psy-precompiles`, `tests`, and `psy-compiler`'s Makefile `build`/`ci` targets. Validation run: ```sh theme={null} lake build lake env proof-forge --emit-counter-ir-psy -o build/psy/Counter.psy diff -u Examples/Psy/Counter.golden.psy build/psy/Counter.psy psyup install 0.1.0 scripts/psy/counter-smoke.sh ``` Result: * `lake build` passed. * Counter IR emits reviewable Psy source. * Generated Psy source matches the checked-in golden fixture. * `scripts/psy/counter-smoke.sh` generated `build/psy/Counter.psy`, ran `dargo test --file`, ran `dargo compile`, produced `build/psy/dargo-counter/target/proof_forge_counter.json`, ran `dargo execute`, and verified `get` returned `result_vm: [2]` after two increments in the same local execution session. * The same smoke generated non-empty ABI output at `build/psy/dargo-counter/target/Counter.json`. * Direct `cargo install --git https://github.com/PsyProtocol/psy-compiler dargo` fetched `psy-compiler` but failed while Cargo updated the `psy-node` `psy-contracts` submodule URL. * `psyup` v0.1.1 currently has only a Linux x86\_64 release asset; macOS arm64 was validated by pinning `psyup install 0.1.0`. Known limitations: * The generator supports only the current no-argument Counter IR subset: `u64` scalar state, scalar read/write, `add`, let-bind, and return. * No deploy JSON, artifact metadata, or live Psy node smoke exists yet. `dargo execute` covers local user/contract execution, not network deployment. Next step: * Add `proof-forge-artifact.json` metadata to the Psy smoke, then decide whether CI should pin `psyup` v0.1.0 or wait for a newer macOS release asset. ### Psy/DPN SDK Skeleton Commit: `feat: add Psy DPN SDK skeleton` Summary: * Added `ProofForge.Psy` as the first Lean SDK surface for the `psy-dpn` ZK target. * Added primitive types and helpers: * `Felt` * `U32` * `Hash` * `ContractMetadata` * Added context, storage, IMT map, hash, and deferred invocation externs under the `lean_psy_*` naming convention. * Added a small `Examples/Psy/Counter.lean` SDK example. Validation run: ```sh theme={null} lake build lake env lean Examples/Psy/Counter.lean ``` Result: * Passed. Notes: * The example uses `initCounter` instead of `initialize` because `initialize` is a Lean command keyword. Known limitations: * The SDK is a source-generation boundary only; no Psy backend lowers these externs yet. * There is no Dargo package generation or `.psy` output yet. Next step: * Add a `psy-dpn` source generator for the hand-written Counter IR fixture. ### Portable IR Counter Runtime Dispatch Commit: `824f5f8 feat: add IR counter EVM runtime smoke` Summary: * Added EVM selector metadata to the hand-written Counter IR fixture. * Extended IR-to-Yul lowering to emit runtime selector dispatch for: * `initialize()` * `increment()` * `get()` * Added `proof-forge --emit-counter-ir-bytecode`, which compiles Counter IR through runtime Yul and `solc --strict-assembly`. * Added a dedicated Foundry smoke script for the IR Counter path: ```sh theme={null} scripts/evm/ir-counter-smoke.sh ``` Validation run: ```sh theme={null} lake build lake env proof-forge --emit-counter-ir-yul -o build/ir/Counter.yul lake env proof-forge --emit-counter-ir-bytecode -o build/ir/Counter.bin --yul-output build/ir/Counter.bytecode.yul solc --strict-assembly build/ir/Counter.yul --bin scripts/evm/ir-counter-smoke.sh ``` Result: * `lake build` passed. * Counter IR emits selector-dispatch Yul. * Counter IR emits non-empty EVM bytecode. * `solc --strict-assembly` accepts the generated runtime Yul. * Foundry smoke passes for `initialize`/`increment`/`get` and unknown-selector revert behavior. Known limitations: * The IR fixture is still hand-written; there is no Lean-source-to-IR extractor. * Only no-argument entrypoints are supported in the IR EVM dispatcher. Next step: * Promote the IR Counter path into CI once external tool gating is in place, and generalize the dispatcher beyond no-argument entrypoints. ### Portable IR Counter Lowering Commit: `787d437 feat: add portable IR counter lowering` Summary: * Added the first target registry modules: * `ProofForge.Target.Capability` * `ProofForge.Target.Registry` * `ProofForge.Target.Check` * Added the first portable contract IR: * `ValueType` * `StateDecl` * `Expr` * `Effect` * `Statement` * `Entrypoint` * `Module` * Added a hand-written Counter IR fixture in `ProofForge.IR.Examples.Counter`. * Added an EVM/Yul lowering path for the Counter-shaped IR subset. * Added CLI smoke command: ```sh theme={null} lake env proof-forge --emit-counter-ir-yul -o build/ir/Counter.yul ``` Validation run: ```sh theme={null} lake build lake env proof-forge --emit-counter-ir-yul -o build/ir/Counter.yul solc --strict-assembly build/ir/Counter.yul --bin ``` Result: * `lake build` passed. * Counter IR lowers to Yul. * `solc --strict-assembly` accepts the generated Yul. Known limitations: * The IR-generated Yul currently contains function definitions only. * It does not yet generate EVM calldata selector dispatch. * `solc` emits `00` for this debug object because no runtime dispatcher calls the generated functions yet. * Existing `--evm-bytecode` smoke still requires Foundry `cast`; it was not revalidated locally because `cast` was not on `PATH`. Next step: * Generate an EVM dispatcher/runtime wrapper from IR entrypoints so the IR path can produce callable bytecode and run through Foundry smoke. ### Psy DPN Target Research Commit: `ce5ab3e docs: add Psy DPN target research` Summary: * Added `psy-dpn` as a Research-stage target. * Classified Psy as a ZK circuit source-generation target. * Documented why the first integration path should generate `.psy` source and call Dargo instead of directly emitting DPN internals. * Added `zk.circuit` and `zk.proof` capability ids. * Added Chinese analysis for the Psy/DPN target. Validation run: ```sh theme={null} git diff --check ``` Result: * Documentation whitespace check passed before commit. Known limitations: * No Psy source generator exists yet. * No Dargo smoke exists in this repository. Next step: * Reuse the portable Counter IR fixture once the IR-to-sourcegen path exists. ### Portable IR And Target Planning Docs Commit: `9b7fce3 docs: add portable IR, capability registry, validation gates, and dev standards` Summary: * Added the first portable IR spec. * Added canonical capability ids. * Added shared Counter scenario. * Added validation gates and development standards. * Added implementation backlog slices for target registry, IR, metadata, EVM hardening, Wasm, Solana, Move, CI, and Psy. Validation run: ```sh theme={null} git diff --check ``` Result: * Documentation whitespace check passed before commit. Known limitations: * These were planning docs only; no IR code existed yet. Next step: * Implement the Target registry and Counter-shaped IR v0 in Lean. ### Multi-Chain Target Design Commit: `a5555e5 docs: add multichain target design` Summary: * Added the first multi-chain platform RFCs and Chinese feasibility/technical analysis. * Established the direction: Lean business logic plus target-specific adapters. * Documented EVM, Solana, Wasm-family, Move-family, and cloud platform tracks. Validation run: ```sh theme={null} git diff --check ``` Result: * Documentation whitespace check passed before commit. Known limitations: * Design-only milestone. Next step: * Split the design into concrete target registry, IR, and validation tasks. ### EVM Baseline Commits: * `34b1708 Initial ProofForge EVM backend` * `b7a5343 Add EVM examples and Foundry smoke tests` * `a97dd21 Add CI and integrate EVM bytecode CLI` Summary: * Added the initial EVM SDK and Yul backend. * Added EVM examples and Foundry smoke tests. * Added bytecode compilation through `solc --strict-assembly`. * Added CI around the baseline build and EVM smoke path. Current role: * EVM remains the first working target. * New IR work should use EVM as the first executable backend to validate semantics before adding more chains. ### EVM Nested Local Fixed Arrays Commit: pending Summary: * Extended portable IR EVM local fixed-array lowering to static nested scalar arrays. * Added deterministic Yul locals for nested leaves such as `matrix[1][0]`. * Covered static nested reads, mutable leaf assignment, numeric leaf compound assignment, nested whole-local assignment, and RHS snapshotting. * Extended nested local scalar fixed arrays to dynamic index paths, including nested getter helpers for reads and nested `switch` blocks for mutable leaf assignment and compound assignment. * Added `nested_dynamic_pick`, `nested_dynamic_row_pick`, `nested_dynamic_update`, and `nested_dynamic_row_update` coverage to `EvmArrayValueProbe`. Validation run: ```sh theme={null} lake build scripts/evm/array-value-ir-smoke.sh ``` Result: * Lean build passed. * Array value smoke produced reproducible golden Yul, compiled bytecode with `solc --strict-assembly`, validated metadata, and passed 17 Foundry tests. Known limitations: * Nested local arrays with unsupported aggregate or non-flat leaves remain explicit unsupported surfaces; flat struct leaves are covered by `EvmStructArrayValueProbe`. ### EVM SDK Example Golden Yul Commit: pending Summary: * Added tracked golden Yul fixtures for SDK EVM examples: `ArrayExample`, `Counter`, `SimpleToken`, `ERC20`, `Ownable`, `Pausable`, and `VerifiedVault`. * Updated `scripts/evm/build-examples.sh` to emit generated SDK Yul into `build/evm`, diff it against each sibling `.golden.yul`, compile bytecode, and validate ProofForge artifact metadata. * Updated EVM validation docs and example README files so changing an SDK example now includes updating its golden Yul fixture. Validation run: ```sh theme={null} scripts/evm/build-examples.sh ``` Result: * All seven SDK examples produced reproducible Yul matching the new golden fixtures. * All seven SDK examples compiled with `solc --strict-assembly` and validated EVM artifact/deploy metadata. Known limitations: * Runtime behavior remains covered by `scripts/evm/foundry-smoke.sh`. ### CI Baseline Repair + Upgrade Policy Resolver Commit: pending Summary: * Fixed the root `target/` ignore rule so `ProofForge/Target/HostBridge.lean` is no longer silently ignored on case-insensitive filesystems, while keeping Rust build output ignored in known target directories. * Replaced the missing GitHub Actions Rust setup action with `dtolnay/rust-toolchain@stable`, then pinned the CosmWasm smoke job to Rust `1.88.0` and `cosmwasm-check 2.2.9 --locked` after latest `cosmwasm-check` failed to link against newer Rust/Wasmer probestack symbols. * Wired `ContractSpec.upgradePolicy?` into target resolution so unsupported target/policy combinations fail before code generation, and supported policies emit `upgrade.policy.*` metadata. * Added a focused upgrade-policy smoke covering EVM, Solana, NEAR, Psy, JSON serialization, and escaping. * Corrected the Gate G0 ledger so it no longer claims `just check` is green before CI and docs sync evidence are actually green. Validation run: ```sh theme={null} lake build ProofForge.Target.Adapter lake env lean --run Tests/UpgradePolicy.lean lake build ProofForge.Target ``` Result: * Target adapter build, upgrade-policy smoke, and target library build passed locally before the full repo validation pass.