View this page as Markdown

assume_nonce

Declares the exact account nonce supplied for one address in a PROGRAM's initial state.

Example

Local

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"}]

API reference

Exact signatures with descriptions, requirements, inputs, returns, and examples.

assume_nonce(ADDRESS, UBIGINT, VARCHAR) #

Declares the exact account nonce supplied for one address in a PROGRAM's initial state.

Inputs

Name Type Use
address ADDRESS

Address whose initial nonce is fixed by this assumption.

required positional
nonce UBIGINT

Exact unsigned 64-bit account nonce.

required positional
reason VARCHAR

Non-NULL valid UTF-8 text recorded in the assumption manifest; it does not affect the semantic assumption root.

required positional

Returns

Name Type
assumption ASSUMPTION

Nonce ASSUMPTION. Returns an ASSUMPTION for one nonce coordinate. PROGRAM rejects another assumption for that coordinate.

Guidance

PROGRAM validation

Duplicate nonce assumptions for the same address fail when PROGRAM is constructed.

Related functions

Category and tags

Category
Simulation
Tag
Simulate