[GH-ISSUE #2395] [Design] Solidity: expose fork-profiled EVM disassembly and bounded control-flow evidence #804

New issue

Open

opened 2026-10-15 18:28:36 +00:00 by bsakaguchi · 1 comment

bsakaguchi commented

2026-10-15 18:28:36 +00:00

Owner

Originally created by @matbrgz on GitHub (Oct 12, 2026).
Original GitHub issue: https://github.com/morluto/rea/issues/2395

Analyst question and current gap

REA's interface-only EVMole adapter explicitly excludes disassembly/basic-block/CFG facets and leaves hardfork unknown. Selector inference cannot explain branches or establish the semantics of later-fork instructions.

Proposed outcome

Evaluate an existing engine behind a separately scoped static instruction/CFG contract, with actual adapter/engine version and admitted fork profile.
Retain byte PCs, opcode bytes, PUSH immediate spans, block boundaries and direct/unresolved jump edges; immediate data is not executable code.
Distinguish unknown/unavailable dynamic jump targets from exhaustively resolved edges; bound graph/result growth.
Report unsupported fork/opcode/container profiles precisely. Legacy flat bytecode admission does not imply EOF or every L2 variant.
Label reconstructed expressions/pseudocode as derivations/inferences if proposed later; this first contract does not execute code or silently reuse an engine's Latest default.

Acceptance and verification

Owned compiler fixtures span documented optimizer/viaIR settings and representative admitted fork targets.
Tests distinguish PUSH immediates containing JUMPDEST-like bytes, truncated PUSH data, dynamic jumps, PUSH0 and admitted transient-storage opcodes.
Unknown fork and EOF-style inputs preserve explicit unsupported profiles.
CLI/MCP retain identity, unresolved edges, bounds and cancellation; actual engine runs verify every supported profile.
Record one feature specification, one implementation plan and incremental tasks under docs/specs/solidity/fork-cfg/ before code.

Scope and relationships

Independently scoped follow-up to roadmap #972 and existing EVM interface PR #1051; parent TIOBE language tracker #2383. Initial analysis uses caller-selected local evidence and owned fixtures. New provider choices require the explicit CONTRIBUTING.md maintainer decision before substantial implementation for integration. Runtime acquisition, local execution and blockchain mutation are not implicit parts of this feature.

Primary references

Originally created by @matbrgz on GitHub (Oct 12, 2026). Original GitHub issue: https://github.com/morluto/rea/issues/2395 [![Type: Architecture / RFC](https://img.shields.io/badge/type-architecture_%2F_RFC-darkred.svg?style=flat-square)](https://github.com/morluto/rea) [![Status: Proposed](https://img.shields.io/badge/status-proposed-blue.svg?style=flat-square)](https://github.com/morluto/rea) [![Ecosystem: REA](https://img.shields.io/badge/ecosystem-morluto%2Frea-8A2BE2.svg?style=flat-square)](https://github.com/morluto/rea) ## Analyst question and current gap REA's interface-only EVMole adapter explicitly excludes disassembly/basic-block/CFG facets and leaves hardfork unknown. Selector inference cannot explain branches or establish the semantics of later-fork instructions. ## Proposed outcome - Evaluate an existing engine behind a separately scoped static instruction/CFG contract, with actual adapter/engine version and admitted fork profile. - Retain byte PCs, opcode bytes, PUSH immediate spans, block boundaries and direct/unresolved jump edges; immediate data is not executable code. - Distinguish unknown/unavailable dynamic jump targets from exhaustively resolved edges; bound graph/result growth. - Report unsupported fork/opcode/container profiles precisely. Legacy flat bytecode admission does not imply EOF or every L2 variant. - Label reconstructed expressions/pseudocode as derivations/inferences if proposed later; this first contract does not execute code or silently reuse an engine's Latest default. ## Acceptance and verification - [ ] Owned compiler fixtures span documented optimizer/viaIR settings and representative admitted fork targets. - [ ] Tests distinguish PUSH immediates containing JUMPDEST-like bytes, truncated PUSH data, dynamic jumps, PUSH0 and admitted transient-storage opcodes. - [ ] Unknown fork and EOF-style inputs preserve explicit unsupported profiles. - [ ] CLI/MCP retain identity, unresolved edges, bounds and cancellation; actual engine runs verify every supported profile. - [ ] Record one feature specification, one implementation plan and incremental tasks under docs/specs/solidity/fork-cfg/ before code. ## Scope and relationships Independently scoped follow-up to roadmap #972 and existing EVM interface PR #1051; parent TIOBE language tracker #2383. Initial analysis uses caller-selected local evidence and owned fixtures. New provider choices require the explicit CONTRIBUTING.md maintainer decision before substantial implementation for integration. Runtime acquisition, local execution and blockchain mutation are not implicit parts of this feature. ## Primary references - [EIP-3855 PUSH0](https://eips.ethereum.org/EIPS/eip-3855) - [EIP-1153 transient storage](https://eips.ethereum.org/EIPS/eip-1153)

bsakaguchi added the

labels

2026-10-15 18:28:36 +00:00

bsakaguchi commented

2026-10-15 18:28:37 +00:00

Author

Owner

@matbrgz commented on GitHub (Oct 12, 2026):

Triage & Architectural Review Notes

Objective (ELI5):
Provide fork-aware EVM disassembly and bounded basic-block control flow graphs (CFGs) without infinite expansion risk.

Technical Constraints:

Fork Profiles: Explicitly account for opcode introducers across EVM hardforks:
- Shanghai (PUSH0 0x5f)
- Cancun (TLOAD 0x5c, TSTORE 0x5d, MCOPY 0x5e)
- Prague / Osaka future opcodes.
CFG Bounds: Jump destinations (JUMPDEST 0x5b) linked via static PUSH<N> analysis must enforce bounded exploration depth and block count to guard against maliciously tangled jump tables or decompiler traps.

@matbrgz commented on GitHub (Oct 12, 2026): ### Triage & Architectural Review Notes **Objective (ELI5):** Provide fork-aware EVM disassembly and bounded basic-block control flow graphs (CFGs) without infinite expansion risk. **Technical Constraints:** - **Fork Profiles:** Explicitly account for opcode introducers across EVM hardforks: - Shanghai (`PUSH0` `0x5f`) - Cancun (`TLOAD` `0x5c`, `TSTORE` `0x5d`, `MCOPY` `0x5e`) - Prague / Osaka future opcodes. - **CFG Bounds:** Jump destinations (`JUMPDEST` `0x5b`) linked via static `PUSH<N>` analysis must enforce bounded exploration depth and block count to guard against maliciously tangled jump tables or decompiler traps.

bsakaguchi referenced this issue

2026-10-16 21:16:18 +00:00

[PR #804] [CLOSED] fix(native): recognize only whole otool command headers #2251

bsakaguchi referenced this issue

2026-10-16 21:16:27 +00:00

[PR #815] [MERGED] fix: integrate 24 reviewed browser/native/semantics corrections #2262

bsakaguchi added

enhancement

and removed

enhancement

labels

2026-10-31 00:29:42 +00:00