Skip to content

feat: add symbolic stack backend path - #85

Open
tcrypt25519 wants to merge 36 commits into
mainfrom
ts/jetdbg
Open

feat: add symbolic stack backend path#85
tcrypt25519 wants to merge 36 commits into
mainfrom
ts/jetdbg

Conversation

@tcrypt25519

Copy link
Copy Markdown
Owner

Summary

  • add a selectable symbolic stack backend and monomorphized stack operations
  • advance symbolic control-flow handling, including dynamic JUMP/JUMPI through conservative site-local switches
  • document the symbolic-stack roadmap and current CFG limitations

Verification

  • cargo check -p jet
  • cargo test -p jet --test test_roms
  • JET_SYMBOLIC_STACK=1 cargo test -p jet --test test_roms
  • cargo clippy -p jet --all-targets -- -D warnings

tcrypt25519 and others added 30 commits February 13, 2026 02:43
* Remove vstack code from builder and tests

Deletes all vstack infrastructure: the `vstack` option from `Options`,
the `_vstack` field and methods from `BuildCtx`, the `__sync_vstack`
helper and all its call sites, and all commented-out vstack branches
in the stack push/pop helpers and `push` opcode. Also cleans up
`use_vstack` CLI arguments in jetdbg and the disabled vstack test
variant in `rom_tests!`.

https://claude.ai/code/session_015PYMujjEHLtp7nkvCHF5PK

* Remove __ prefix from private identifiers and move them below public fns

Strips the double-underscore convention from all private helpers in
ops.rs (e.g. __stack_pop_2 → stack_pop_2, __call_stack_push_i256 →
call_stack_push_i256) and from the two pub(crate) entry points
(__build_return → build_return, __invalid_jump_return →
invalid_jump_return). Reorders the file so all pub(crate) opcode
implementations appear first, followed by a clearly-marked "Private
helpers" section. Updates the one external call site in contract.rs.

https://claude.ai/code/session_015PYMujjEHLtp7nkvCHF5PK

* chore: CI change 🤖

* Fix extra argument in invalid_opcode test

Options::new takes (mode, emit_llvm, assert); remove the stray `false`
that was inserted before the `assert` argument.

https://claude.ai/code/session_015PYMujjEHLtp7nkvCHF5PK

* Remove unused invalid_jump_return function

Dead code with no call sites; flagged by clippy -D warnings.

https://claude.ai/code/session_015PYMujjEHLtp7nkvCHF5PK

* Remove vstack references from docs

The vstack infrastructure and Options flag were removed in this PR.
Update architecture.md, architecture-notes.md, and manifesto.md to:
- Drop the BuildCtx _vstack field from struct snippets
- Rename the "Hybrid Stack Model" section to "Real Stack Model" and
  remove the vstack-enabled code example and planned-optimization prose
- Remove __sync_vstack from the control flow pattern snippet
- Update helper function names to match the renamed (no-__ prefix) API
- Remove vstack from Known TODOs, Future Opportunities, Suggested Next
  Steps, Options description, and the Glossary
- Remove the "Virtual Stack Optimization" and "The Virtual Stack"
  caution-zone sections from the manifesto

https://claude.ai/code/session_015PYMujjEHLtp7nkvCHF5PK

---------

Co-authored-by: Claude <noreply@anthropic.com>
…ering (#64)

* Initial plan

* Add comprehensive technical documentation for EVM bytecode to LLVM blocks lowering

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Update docs/bytecode-to-llvm-blocks.md

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update docs/bytecode-to-llvm-blocks.md

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Update docs/bytecode-to-llvm-blocks.md

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>

* Clarify block lifecycle documentation for zero-length blocks

Address feedback that "empty rom == open" doesn't hold for consecutive
JUMPDESTs, which create closed blocks with zero-length rom slices.
Update Block Lifecycle section to accurately describe the implementation's
use of is_empty() as a reassignment guard rather than state indicator.

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
Co-authored-by: Tyler Smith <mail@tcry.pt>
Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
* fix: Handle in-instruction branches.
* Initial plan

* Remove all nightly references from DEVELOPMENT.md and rust-toolchain.toml

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Update CI workflow steps to match actual workflow more precisely

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Clarify CI auto-formatting behavior in documentation

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
… of truth

jet_runtime/src/lib.rs defined ADDRESS_SIZE_BYTES = 2, shadowing the correct
value (20) from jet_ir::constants via `pub use jet_ir::*`. This caused all
address operations (binding, builtins, exec Address type) to silently truncate
every 20-byte EVM address to 2 bytes.

Fix: remove the entire duplicate constants block from jet_runtime/src/lib.rs.
All constants are already in jet_ir/src/constants.rs and re-exported via
`pub use jet_ir::*`. Update coinbase fixtures in jetdbg.rs and roms/mod.rs to
use the correct 20-byte length.

Also: update docs/TREE.md to reflect current crate structure (adds jet_ir,
jet_push_macros, new runtime files; removes defunct scratch/ and crates-bk/).
Delete examples/temp.ll scratch file.

Closes #68

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>
Updated the MIT License with correct year and author.
* fix: call jet_mem_expand before jet.mem.load in MLOAD

MLOAD was not calling jet_mem_expand before reading from memory, unlike
MSTORE and MSTORE8 which both expand first. If MLOAD was executed with
an offset at or near the current memory capacity, jet.mem.load would
compute memory_ptr + offset and jet.stack.push.ptr would then read 32
bytes (i256) from that address — potentially outside the allocated
region — causing an intermittent segfault.

The fix mirrors the existing pattern: call jet_mem_expand(ctx, offset, 32)
first so the buffer is guaranteed to cover [offset, offset+32). Since
jet_mem_expand may reallocate and update ctx.memory_ptr, jet.mem.load
then re-reads the fresh pointer from the context struct, so no dangling
pointer is ever used.

https://claude.ai/code/session_01XcNd32HQupXsdnVd4KmX6f

* fix: update test framework and CALL bytecode to use 20-byte addresses

After ADDRESS_SIZE_BYTES was corrected from 2 to 20 (commit 84b96e0),
the test harness still registered contracts with 2-byte addresses
("0x0000", "0x0001"), while jet_contract_call now reads 20 bytes from
the EVM stack word to build the lookup key — producing a 40-hex-char
address that never matched.

The mismatch caused jet_contract_fn_lookup to return 0 (not found),
so jet_contract_call returned early without initialising ctx.sub_call.
With sub_call still None (null), the subsequent RETURNDATASIZE
instruction dereferenced a null pointer → SIGSEGV.

Fix:
- _test_rom_body now generates 20-byte zero-padded addresses for both
  contract registration and the run_contract entry point, using
  ADDRESS_SIZE_BYTES as the single source of truth.
- basic_call_with_return_data upgrades PUSH2 to PUSH20 so the callee
  address on the EVM stack matches what jet_contract_call looks up.

https://claude.ai/code/session_01XcNd32HQupXsdnVd4KmX6f

* fix: check jet_mem_expand return value in MLOAD, MSTORE, MSTORE8

All three memory ops were ignoring the i8 return code from jet_mem_expand.
If expansion fails (ArithmeticOverflow=-2, AllocationFailed=-3), the JIT
code proceeded to read/write through an unexpanded pointer, leading to
out-of-bounds memory access.

Add call_mem_expand_checked: emits the expand call, compares the result
to 0, and on error branches to a new block that returns ReturnCode::Invalid
from the contract function immediately. On success execution continues in
a new ok block. MLOAD, MSTORE, and MSTORE8 all use this helper instead of
the unchecked build_call.

https://claude.ai/code/session_01XcNd32HQupXsdnVd4KmX6f

---------

Co-authored-by: Claude <noreply@anthropic.com>
* chore: Cleanup docs.
* Initial plan

* Add stack bounds checking to prevent memory corruption

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Fix Use-After-Free vulnerability in memory pointer handling

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Fix ADDMOD and MULMOD to use 512-bit precision for EVM compliance

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Add symbol mappings for ADDMOD and MULMOD builtins

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* Refactor ADDMOD/MULMOD helpers to reduce code duplication

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* chore: CI change 🤖

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
Co-authored-by: tcrypt25519 <mail@tcry.pt>
* feat: introduce Address newtype to replace raw [u8; 20] (closes #75)

Replace the private `type Address = [u8; ADDRESS_SIZE_BYTES]` alias
with a proper `Address([u8; 20])` newtype in `jet_runtime::address`.

Key properties of the new type:
- `#[repr(transparent)]` over `[u8; 20]` — identical memory layout,
  compatible with `#[repr(C)]` structs like `BlockInfo`
- Derives `Clone`, `Copy`, `PartialEq`, `Eq`, `Hash`, `Default`
- `Display` / `Debug` emit lowercase `0x`-prefixed hex
- `FromStr` / `TryFrom<&str>` parse hex strings with optional `0x`
  prefix and left-pad short forms (e.g. `"0x1234"`) to 20 bytes
- `From<[u8; 20]>` / `Into<[u8; 20]>` and `AsRef<[u8]>` for
  zero-cost interop with existing byte-slice APIs
- `Address::ZERO` constant and `as_bytes_mut` for in-place mutation

Updated across the codebase:
- `BlockInfo::coinbase` field and getter now use `Address`
- `mangle_contract_fn` takes `&Address`; `jet_contract_fn_lookup`
  builds an `Address` from the little-endian stack bytes (fixing an
  implicit reversal that previously produced inconsistent names)
- `Engine::build_contract` / `run_contract` take `Address` by value
- `Manager::add_contract_function` / `verify_contract` take `Address`
- Test helpers and `jetdbg` construct addresses via `Address::new`,
  `Address::ZERO`, and `str::parse::<Address>()`

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

* chore: CI change 🤖

* fix: update invalid_opcode test to use Address

Missed in the initial pass — the test called build_contract with a bare
&str; update it to pass Address::ZERO instead.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

* fix: address review feedback — panic safety, alloc-free parsing, LEN constant

Three issues raised in code review:

1. jet_contract_fn_lookup: add .take(ADDRESS_SIZE_BYTES) so a 32-byte
   EVM stack word cannot index past the 20-byte `bytes` array and panic.
   The address lives in the low bytes of the word, so after reversing
   (little- to big-endian) we only need the first 20 bytes.

2. FromStr: replace format! + hex::decode (two heap allocations) with a
   stack-allocated [u8; 40] padding buffer and hex::decode_to_slice,
   making address parsing allocation-free.

3. Address::LEN: source from jet_ir::ADDRESS_SIZE_BYTES instead of a
   duplicated literal so the canonical address length is defined once.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

* chore: CI change 🤖

* refactor: self-referential LEN constant as single source of truth

Address::LEN = 20 is now the sole definition of address width.
Every use of the literal 20 (or 40 for hex) inside the type and
its impls is replaced:

- struct field:        [u8; Self::LEN]
- ZERO constant:       [0u8; Self::LEN]
- new / as_bytes*:     [u8; Self::LEN]
- From impls:          [u8; Address::LEN]
- FromStr stack bufs:  Address::HEX_LEN (= Self::LEN * 2, private const)
- tests:               Address::LEN / Address::HEX_LEN

Removes the previous jet_ir::ADDRESS_SIZE_BYTES dependency; the
canonical length now lives in Address itself.

Co-Authored-By: Claude Sonnet 4.5 <noreply@anthropic.com>

* chore: CI change 🤖

---------

Co-authored-by: Claude Sonnet 4.5 <noreply@anthropic.com>
* fix: keccak.

* fix: add null checks and return code validation for KECCAK256 (#79)

* Initial plan

* fix: add null check and return code validation for KECCAK256

- Add null pointer check for ctx in jet_ops_keccak256
- Check return code from jet_ops_keccak256 and propagate errors via Invalid return code
- Use minimal unsafe scopes with SAFETY comments per Rust 2024 edition requirements

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* refactor: consolidate unsafe blocks in jet_ops_keccak256

Consolidate multiple unsafe blocks for accessing ctx fields into a single
unsafe block that dereferences ctx once, improving readability while
maintaining the same safety guarantees.

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* docs: clarify safety requirements and add SAFETY comment

- Clarify safety documentation for ctx parameter (valid if non-null)
- Add SAFETY comment for IntValue::new call for consistency

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* docs: improve safety documentation clarity

- Clarify undefined behavior when result pointer is null
- Expand SAFETY comment for IntValue::new to explain the contract

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* chore: CI change 🤖

* docs: validate u32 safety for EVM memory operations (ADR-004) (#80)

* Initial plan

* docs: add ADR-004 explaining why u32 is safe for EVM memory operations

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* docs: remove line numbers and clarify implemented opcodes in ADR-004

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
* Initial plan

* docs: Update .github/copilot-instructions.md with comprehensive onboarding guide

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* docs: Address PR feedback on copilot-instructions.md

- Remove resolved known issues (test segfaults, SDIV overflow, KECCAK256 fixed)
- Update stack helper function names (remove leading underscores)
- Remove references to deleted docs/ext/evm/*.mdx files
- Add evm-spec-lookup skill as EVM spec reference
- Add docs/process/segfault-troubleshooting.md for P0 segfault handling
- Emphasize agents must NOT add #[allow] pragmas without permission
- Link to docs/process/new-opcode.md instead of duplicating content
- Add memory-based stack and jump tables as architecture limitations
- Update last updated date to 2026-02-16

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

* docs: Fix code examples and CI step count in copilot-instructions.md

- Correct CI pipeline steps from 15 to 16 (missing "Log LLVM shared libraries")
- Fix division by zero example: mark select pattern as "ALSO WRONG"
- Update basic block creation API to correct form: bctx.env.context().append_basic_block()
- Fix function names: stack_push_int() without leading underscores
- Add reference to build_zero_guard() helper function
- Clarify that explicit branching is the ONLY correct approach for div-by-zero

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
Co-authored-by: Tyler Smith <mail@tcry.pt>
* docs: Uodate architecture doc.

* tweak: Reduce non-required pub visibility.

* docs: Add rustdoc comments.

* docs: Update docs.

* fix

* chore: CI change 🤖

* Fix documentation errors in PR #82 review comments (#83)

* Initial plan

* fix: address PR #82 review comments - correct documentation errors

Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>

---------

Co-authored-by: Copilot <198982749+Copilot@users.noreply.github.com>
Co-authored-by: tcrypt25519 <212655132+tcrypt25519@users.noreply.github.com>
Add symbolic block-state handling for static jumps and joins, share non-jump opcode dispatch between stack backends, and document the current lowering model.

Also add targeted JUMPI join tests and jumpdest indexing so symbolic target lookup stays explicit and cheap.
Lower symbolic dynamic JUMP and taken JUMPI through site-local switches over known JUMPDEST targets, carrying the post-pop symbolic stack to each conservative successor.

Add ROM coverage for computed JUMP and JUMPI targets in both runtime and symbolic modes, and update the symbolic stack design note.
# Conflicts:
#	Cargo.lock
#	Cargo.toml
#	crates/jet_ir/src/types.rs
@semanticdiff-com

semanticdiff-com Bot commented May 16, 2026

Copy link
Copy Markdown

Review changes with  SemanticDiff

@gemini-code-assist gemini-code-assist Bot left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Code Review

This pull request introduces a symbolic stack lowering path to the Jet EVM JIT compiler, enabling compile-time tracking of stack values and more efficient IR generation. It refactors opcode implementations to use a generic StackBackend trait, supporting both runtime and symbolic modes, and upgrades the project to LLVM 22. A new jetdbg CLI tool is also included for contract debugging. Review feedback identifies a bug in the symbolic handling of PUSH data where bytes are incorrectly reversed, and recommends using safe Inkwell methods to replace unnecessary unsafe blocks in the stack backend implementation.

IterItem::PushData(_, _, data) => {
let mut new_data = [0u8; 32];
new_data[..data.len()].copy_from_slice(data);
new_data[..data.len()].reverse();

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

high

The reverse() call here appears to be a bug. According to the architecture documentation and the instructions::Iter implementation, PUSH data is already converted to little-endian (bytes reversed) by the iterator. Since ops::push expects little-endian bytes to construct its i256 limbs, reversing them again here will turn them back into big-endian, leading to incorrect values for multi-byte PUSH opcodes.

                ops::push(bctx, new_data)?;

Comment thread crates/jet/src/builder/stack.rs Outdated
let loaded = bctx
.builder
.build_load(bctx.env.types().i256, ptr, "load_int")?;
let word = unsafe { IntValue::new(loaded.as_value_ref()) };

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The use of unsafe and as_value_ref() here is unnecessary. Since loaded is a BasicValueEnum resulting from an i256 load, you can use the safe into_int_value() method provided by Inkwell.

Suggested change
let word = unsafe { IntValue::new(loaded.as_value_ref()) };
let word = loaded.into_int_value();

Comment thread crates/jet/src/builder/stack.rs Outdated
&[bctx.registers.exec_ctx.into(), index_value.into()],
"stack_peek_word_result",
)?;
let ptr = unsafe { PointerValue::new(ret.as_value_ref()) };

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

medium

The use of unsafe and as_value_ref() can be avoided here by using into_pointer_value() on the result of the peek call.

Suggested change
let ptr = unsafe { PointerValue::new(ret.as_value_ref()) };
let ptr = ret.try_as_basic_value().left().unwrap().into_pointer_value();

Build symbolic-mode control flow from a fixed-point abstract stack pass before IR emission. Pre-create entry phis for planned block variants, specialize bytecode blocks by incoming stack height, and lower dynamic jumps through variants without falling back to runtime stack traffic.

Preserve known-u64 metadata through symbolic DUP so planned static jump edges and emitted symbolic state agree. Add ROM coverage for backward-only targets, duplicate-carried jump targets, and differing-height joins.
@tcrypt25519
tcrypt25519 force-pushed the ts/jetdbg branch 2 times, most recently from c8b6900 to a70e414 Compare July 28, 2026 16:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants