assume_no_code

WITH actors AS (
  SELECT
    '0x1000000000000000000000000000000000000001'::ADDRESS AS sender,
    '0x2000000000000000000000000000000000000002'::ADDRESS AS writer
),
authored AS (
  SELECT [
    -- Funds the one-Wei transfer in step zero.
    assume_native_balance(sender, 1000000::UINT256, 'funds step value transfer'::VARCHAR),
    -- Supplies the transaction context consumed by step zero.
    assume_nonce(sender, 0::UBIGINT, 'step sender nonce'::VARCHAR),
    assume_no_code(sender, 'step sender is an EOA'::VARCHAR),
    assume_native_balance(writer, 0::UINT256, 'receives step value'::VARCHAR),
    assume_nonce(writer, 0::UBIGINT, 'call target nonce'::VARCHAR),
    -- This runtime consumes calldata and stores its first word.
    assume_code(writer, '0x60003560005500'::BYTES, 'step code stores calldata word'::VARCHAR),
    assume_storage(
      writer,
      '0x0000000000000000000000000000000000000000000000000000000000000000'::BYTES32,
      '0x0000000000000000000000000000000000000000000000000000000000000000'::BYTES32,
      'step writes slot zero'::VARCHAR
    )
  ] AS assumptions,
  execute_call(
    sender,
    writer,
    '0x000000000000000000000000000000000000000000000000000000000000002a'::BYTES,
    1::UINT256,
    100000::UBIGINT
  ) AS step
  FROM actors
),
candidate AS (
  SELECT program(assumptions, [step]) AS program, assumptions
  FROM authored
)
SELECT
  len(assumptions)::INTEGER AS assumption_count,
  program IS NOT NULL AS runnable
FROM candidate;
-- => [{"assumption_count":7,"runnable":"true"}]