foundry_evm_symbolic/runtime/

state.rs

use super::*;
use foundry_evm::revm::context_interface::cfg::gas::CALL_STIPEND;

const MAX_BOUND_ANALYSIS_VISITS: usize = 256;

#[derive(Clone, Debug)]
pub(crate) struct PathState {
    pub(crate) depth: usize,
    pub(crate) call_depth: usize,
    pub(crate) origin: Address,
    pub(crate) origin_word: SymExpr,
    pub(crate) gas_price: SymExpr,
    pub(crate) ffi_enabled: bool,
    pub(crate) block: SymbolicBlock,
    pub(crate) frame: CallFrame,
    pub(crate) world: SymbolicWorld,
    pub(crate) prank: SymbolicPrank,
    pub(crate) constraints: Vec<SymBoolExpr>,
    pub(crate) next_symbol: usize,
    pub(crate) recorded_logs: Option<Vec<SymbolicLog>>,
    /// Bumped by `recordLogs` and `getRecordedLogs*` so open frame checkpoints know the buffer
    /// was reset.
    pub(crate) recorded_logs_generation: u64,
    pub(crate) access_record: Option<AccessRecord>,
    pub(crate) root_calldata: Option<SymbolicCalldata>,
    /// Predicate context follows child calls but is not committed back to handler state.
    pub(crate) invariant_predicate: bool,
    corpus_seed_models: Vec<Arc<SymbolicModel>>,
    branch_target: Option<SymbolicBranchTarget>,
    branch_target_reached: bool,
    needs_feasibility_check: bool,
    pub(crate) loop_jumps: HashMap<usize, u32>,
    pub(crate) expected_revert: Option<ExpectedRevert>,
    pub(crate) assume_no_revert_next_call: Option<AssumeNoRevert>,
    pub(crate) expected_emit: Option<ExpectedEmit>,
    pub(crate) expected_calls: Vec<ExpectedCall>,
    pub(crate) expected_creates: Vec<ExpectedCreate>,
    pub(crate) call_mocks: Vec<CallMock>,
    pub(crate) function_mocks: Vec<FunctionMock>,
    pub(crate) persistent_accounts: HashSet<Address>,
    pub(crate) wallets: IndexSet<Address>,
    pub(crate) labels: HashMap<Address, String>,
    pub(crate) storage_load_hooks: HashMap<Address, SymbolicStorageHook>,
    pub(crate) storage_store_hooks: HashMap<Address, SymbolicStorageHook>,
    pub(crate) mapping_storage_store_hooks: HashMap<(Address, U256), SymbolicStorageHook>,
    pub(crate) mapping_hook_keccak_preimages: HashMap<(Address, SymExpr), Arc<[SymExpr]>>,
    pub(crate) storage_hook_active: bool,
    pub(crate) pending_storage_hook_revert: bool,
}

impl PathState {
    pub(crate) fn new(
        cx: &mut SymCx,
        address: Address,
        caller: Address,
        callvalue: U256,
        calldata: SymbolicCalldata,
        ffi_enabled: bool,
    ) -> Self {
        let mut state = Self::empty(cx, address, caller, ffi_enabled);
        let callvalue = SymExpr::constant(cx, callvalue);
        let call_data = calldata.call_data(cx);
        state.frame = CallFrame::new(cx, address, address, caller, callvalue, false, call_data);
        state.constraints = calldata.constraints().to_vec();
        state.root_calldata = Some(calldata);
        state
    }

    pub(crate) fn empty(
        cx: &mut SymCx,
        address: Address,
        caller: Address,
        ffi_enabled: bool,
    ) -> Self {
        let origin_word = SymExpr::constant(cx, address_word(caller));
        let gas_price = SymExpr::zero(cx);
        let block = SymbolicBlock::new(cx);
        let callvalue = SymExpr::zero(cx);
        let calldata = SymBytes::empty(cx);
        let calldata = SymCalldata::from_bytes(cx, calldata);
        let frame = CallFrame::new(cx, address, address, caller, callvalue, false, calldata);
        Self {
            depth: 0,
            call_depth: 0,
            origin: caller,
            origin_word,
            gas_price,
            ffi_enabled,
            block,
            frame,
            world: SymbolicWorld::default(),
            prank: SymbolicPrank::default(),
            constraints: Vec::new(),
            next_symbol: 0,
            recorded_logs: None,
            recorded_logs_generation: 0,
            access_record: None,
            root_calldata: None,
            invariant_predicate: false,
            corpus_seed_models: Vec::new(),
            branch_target: None,
            branch_target_reached: false,
            needs_feasibility_check: false,
            loop_jumps: HashMap::default(),
            expected_revert: None,
            assume_no_revert_next_call: None,
            expected_emit: None,
            expected_calls: Vec::new(),
            expected_creates: Vec::new(),
            call_mocks: Vec::new(),
            function_mocks: Vec::new(),
            persistent_accounts: HashSet::default(),
            wallets: IndexSet::default(),
            labels: HashMap::default(),
            storage_load_hooks: HashMap::default(),
            storage_store_hooks: HashMap::default(),
            mapping_storage_store_hooks: HashMap::default(),
            mapping_hook_keccak_preimages: HashMap::default(),
            storage_hook_active: false,
            pending_storage_hook_revert: false,
        }
    }

    pub(crate) fn apply_executor_env(&mut self, cx: &mut SymCx, executor: &ExecutorView<'_>) {
        self.block = SymbolicBlock::from_executor(cx, executor);
        self.gas_price = SymExpr::constant(cx, U256::from(executor.gas_price));
        for &(target, overwrite) in &executor.arbitrary_storage_targets {
            self.world.enable_arbitrary_storage(target, overwrite);
        }
        for &(target, source) in &executor.arbitrary_storage_copies {
            Arc::make_mut(&mut self.world.state).arbitrary_storage_copies.insert(target, source);
        }
        self.storage_load_hooks.extend(executor.storage_load_hooks.iter().copied());
        self.storage_store_hooks.extend(executor.storage_store_hooks.iter().copied());
        self.mapping_storage_store_hooks
            .extend(executor.mapping_storage_store_hooks.iter().copied());
    }

    pub(crate) fn child(&self, frame: CallFrame) -> Self {
        let mut child = self.clone();
        child.call_depth += 1;
        child.frame = frame;
        // A prank changes the call being entered; calls made by the callee use normal EVM caller
        // semantics unless the callee sets its own prank.
        child.prank = SymbolicPrank::default();
        child.loop_jumps.clear();
        child.expected_revert = None;
        child.assume_no_revert_next_call = None;
        child
    }

    /// Returns whether a CALL or CREATE issued by this frame runs as its own transaction, as
    /// Forge's call isolation does for calls made by the test, handler, or invariant frame.
    pub(crate) const fn starts_isolated_transaction(&self, executor: &ExecutorView<'_>) -> bool {
        executor.isolate && self.call_depth == 0
    }

    pub(crate) fn storage_hook_child(&self, frame: CallFrame) -> Self {
        let mut child = self.child(frame);
        child.storage_hook_active = true;
        child.recorded_logs = None;
        child.access_record = None;
        child.expected_emit = None;
        child.expected_calls.clear();
        child.expected_creates.clear();
        child.call_mocks.clear();
        child.function_mocks.clear();
        child.set_branch_target(None);
        child
    }

    pub(crate) fn copy_call_output_offset(
        &mut self,
        cx: &mut SymCx,
        dest: SymExpr,
        size: &BoundedCopySize,
    ) -> Result<(), SymbolicError> {
        let CallFrame { memory, return_data, .. } = &mut self.frame;
        memory.copy_call_output_offset(cx, dest, size, return_data)
    }

    pub(crate) fn constrained_usize(&self, cx: &mut SymCx, expr: &SymExpr) -> Option<usize> {
        self.constrained_usize_checked(cx, expr).and_then(Result::ok)
    }

    pub(crate) fn constrained_usize_checked(
        &self,
        cx: &mut SymCx,
        expr: &SymExpr,
    ) -> Option<Result<usize, U256>> {
        self.constrained_word(cx, expr).map(|value| usize::try_from(value).map_err(|_| value))
    }

    pub(crate) fn upper_bound_usize(&self, _cx: &mut SymCx, expr: &SymExpr) -> Option<usize> {
        let mut bounds = HashMap::default();
        let mut ordering = HashMap::default();
        let mut remaining = MAX_BOUND_ANALYSIS_VISITS;
        self.expr_upper_bound_usize_cached(expr, &mut bounds, &mut ordering, &mut remaining)
    }

    /// Returns a conservative lower bound for values representable as host memory offsets.
    pub(crate) fn lower_bound_usize(&self, expr: &SymExpr) -> usize {
        let mut lower_bounds = HashMap::default();
        let mut upper_bounds = HashMap::default();
        let mut ordering = HashMap::default();
        let mut remaining = MAX_BOUND_ANALYSIS_VISITS;
        self.expr_lower_bound_usize(
            expr,
            &mut lower_bounds,
            &mut upper_bounds,
            &mut ordering,
            &mut remaining,
        )
    }

    pub(crate) fn constrained_word(&self, cx: &mut SymCx, expr: &SymExpr) -> Option<U256> {
        expr.as_const().or_else(|| {
            self.constraints
                .iter()
                .find_map(|constraint| {
                    constraint.forces_expr_const_with_context(expr, &self.constraints)
                })
                .or_else(|| self.constrained_expr_value(cx, expr))
        })
    }

    pub(crate) fn constrained_expr_value(&self, cx: &mut SymCx, expr: &SymExpr) -> Option<U256> {
        if let Some(value) = expr.eval() {
            return Some(value);
        }
        if let Some(value) = expr.known_word() {
            return Some(value);
        }

        let mut vars = SymbolicVars::default();
        expr.collect_eval_vars(&mut vars);
        let mut model = SymbolicModel::default();
        for var in vars {
            let var_expr = SymExpr::get_var(cx, var);
            let value = self.constraints.iter().find_map(|constraint| {
                constraint.forces_expr_const_with_context(&var_expr, &self.constraints)
            })?;
            model.insert(var, value);
        }

        expr.eval_model(&model).ok()
    }

    pub(crate) fn split_corpus_seed_models(
        &self,
        condition: &SymBoolExpr,
    ) -> (Vec<Arc<SymbolicModel>>, Vec<Arc<SymbolicModel>>) {
        let mut true_models = Vec::new();
        let mut false_models = Vec::new();
        for model in &self.corpus_seed_models {
            match condition.eval_model_if_complete(model.as_ref()) {
                Ok(Some(true)) => true_models.push(Arc::clone(model)),
                Ok(Some(false)) => false_models.push(Arc::clone(model)),
                Ok(None) | Err(_) => {
                    true_models.push(Arc::clone(model));
                    false_models.push(Arc::clone(model));
                }
            }
        }
        (true_models, false_models)
    }

    pub(crate) fn set_corpus_seed_models(&mut self, models: Vec<Arc<SymbolicModel>>) {
        self.corpus_seed_models = models;
    }

    pub(crate) const fn corpus_seed_model_count(&self) -> usize {
        self.corpus_seed_models.len()
    }

    pub(crate) const fn set_branch_target(&mut self, target: Option<SymbolicBranchTarget>) {
        self.branch_target = target;
        self.branch_target_reached = false;
    }

    pub(crate) const fn branch_target(&self) -> Option<SymbolicBranchTarget> {
        self.branch_target
    }

    pub(crate) const fn mark_branch_target_reached(&mut self) {
        self.branch_target_reached = true;
    }

    pub(crate) fn inherit_branch_target_progress(&mut self, child: &Self) {
        if self.branch_target == child.branch_target && child.branch_target_reached {
            self.mark_branch_target_reached();
        }
    }

    pub(crate) fn take_noncommitting_check_state(&mut self, check: &mut Self) {
        self.constraints = std::mem::take(&mut check.constraints);
        self.next_symbol = self.next_symbol.max(check.next_symbol);
        self.world.merge_replay_metadata_from(&check.world);
        self.storage_load_hooks = std::mem::take(&mut check.storage_load_hooks);
        self.storage_store_hooks = std::mem::take(&mut check.storage_store_hooks);
        self.mapping_storage_store_hooks = std::mem::take(&mut check.mapping_storage_store_hooks);
    }

    pub(crate) fn take_call_outcome_state(&mut self, child: &mut Self) {
        self.constraints = std::mem::take(&mut child.constraints);
        self.next_symbol = child.next_symbol;
        self.inherit_branch_target_progress(child);
        self.storage_load_hooks = std::mem::take(&mut child.storage_load_hooks);
        self.storage_store_hooks = std::mem::take(&mut child.storage_store_hooks);
        self.mapping_storage_store_hooks = std::mem::take(&mut child.mapping_storage_store_hooks);
        self.mapping_hook_keccak_preimages =
            std::mem::take(&mut child.mapping_hook_keccak_preimages);
        self.recorded_logs = child.recorded_logs.take();
        self.recorded_logs_generation = child.recorded_logs_generation;
        self.access_record = child.access_record.take();
        // Inspector state survives child reverts and exceptional halts.
        self.block = child.block.clone();
        self.expected_calls = std::mem::take(&mut child.expected_calls);
        self.call_mocks = std::mem::take(&mut child.call_mocks);
        self.function_mocks = std::mem::take(&mut child.function_mocks);
    }

    /// Drops logs recorded by a failed call that started with `len` logs in `generation`.
    ///
    /// If the buffer was replaced during the call, every log it holds was recorded by the call.
    pub(crate) fn discard_failed_call_logs(&mut self, len: usize, generation: u64) {
        if let Some(logs) = &mut self.recorded_logs {
            logs.truncate(if generation == self.recorded_logs_generation { len } else { 0 });
        }
    }

    pub(crate) fn take_reverted_top_level_effects(&mut self, mut reverted: Self) {
        let recorded_logs_len = self.recorded_logs.as_ref().map_or(0, Vec::len);
        let recorded_logs_generation = self.recorded_logs_generation;
        self.take_noncommitting_check_state(&mut reverted);
        self.block = reverted.block;
        self.recorded_logs = reverted.recorded_logs;
        self.recorded_logs_generation = reverted.recorded_logs_generation;
        self.discard_failed_call_logs(recorded_logs_len, recorded_logs_generation);
        self.access_record = reverted.access_record;
        self.expected_revert = reverted.expected_revert;
        self.assume_no_revert_next_call = reverted.assume_no_revert_next_call;
        self.expected_emit = reverted.expected_emit;
        self.expected_calls = reverted.expected_calls;
        self.expected_creates = reverted.expected_creates;
        self.call_mocks = reverted.call_mocks;
        self.function_mocks = reverted.function_mocks;
    }

    /// Returns `true` if the path can be materialized into a replayable corpus seed.
    ///
    /// Gas-dependent constraints are never modeled, so a seed for such a path would carry a
    /// fabricated `gasleft()` value; skip the seed rather than failing the whole run.
    pub(crate) fn can_materialize_seed(&self) -> bool {
        !self.constraints.iter().any(SymBoolExpr::contains_gasleft)
    }

    pub(crate) const fn satisfies_branch_target(&self) -> bool {
        self.branch_target.is_none() || self.branch_target_reached
    }

    pub(crate) const fn defer_feasibility_check(&mut self) {
        self.needs_feasibility_check = true;
    }

    pub(crate) const fn take_deferred_feasibility_check(&mut self) -> bool {
        let needs_check = self.needs_feasibility_check;
        self.needs_feasibility_check = false;
        needs_check
    }

    fn expr_upper_bound_usize_cached(
        &self,
        expr: &SymExpr,
        bounds: &mut HashMap<SymExpr, Option<usize>>,
        ordering: &mut HashMap<(SymExpr, SymExpr), bool>,
        remaining: &mut usize,
    ) -> Option<usize> {
        if let Some(bound) = bounds.get(expr) {
            return *bound;
        }
        if let Some(value) = expr.as_const() {
            return usize::try_from(value).ok();
        }

        let constraint_bound = self.constraint_upper_bound_usize(expr);
        let structural_bound = remaining.checked_sub(1).and_then(|next| {
            *remaining = next;
            match expr.kind() {
                SymExprKind::Const(value) => usize::try_from(*value).ok(),
                SymExprKind::Var(_)
                | SymExprKind::GasLeft(_)
                | SymExprKind::Keccak { .. }
                | SymExprKind::Hash { .. } => None,
                SymExprKind::Not(_) => None,
                SymExprKind::TernOp(_, _, _, modulus) => match modulus.as_const() {
                    Some(modulus) if modulus.is_zero() => Some(0),
                    Some(modulus) => usize::try_from(modulus - U256::ONE).ok(),
                    None => self
                        .expr_upper_bound_usize_cached(modulus, bounds, ordering, remaining)
                        .and_then(|bound| bound.checked_sub(1)),
                },
                SymExprKind::Ite(condition, left, right) => {
                    let left_bound =
                        self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining);
                    let right_bound =
                        self.expr_upper_bound_usize_cached(right, bounds, ordering, remaining);
                    match (left_bound, right_bound) {
                        (Some(left_bound), Some(right_bound)) => Some(left_bound.max(right_bound)),
                        (None, Some(right_bound)) => condition
                            .implies_unsigned_less_or_equal(true, left, right, remaining)
                            .then_some(right_bound),
                        (Some(left_bound), None) => condition
                            .implies_unsigned_less_or_equal(false, right, left, remaining)
                            .then_some(left_bound),
                        (None, None) => None,
                    }
                }
                SymExprKind::BinOp(op, left, right) => match op {
                    SymBinOp::Add => self
                        .expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?
                        .checked_add(
                            self.expr_upper_bound_usize_cached(right, bounds, ordering, remaining)?,
                        ),
                    SymBinOp::Mul => self
                        .expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?
                        .checked_mul(
                            self.expr_upper_bound_usize_cached(right, bounds, ordering, remaining)?,
                        ),
                    SymBinOp::UDiv => {
                        let left =
                            self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?;
                        match right.as_const()? {
                            divisor if divisor.is_zero() => Some(0),
                            divisor => Some(left / usize::try_from(divisor).ok()?),
                        }
                    }
                    SymBinOp::URem => match right.as_const() {
                        Some(divisor) if divisor.is_zero() => Some(0),
                        Some(divisor) => usize::try_from(divisor - U256::ONE).ok(),
                        None => {
                            self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining)
                        }
                    },
                    SymBinOp::And => right
                        .as_const()
                        .and_then(|value| usize::try_from(value).ok())
                        .or_else(|| left.as_const().and_then(|value| usize::try_from(value).ok()))
                        .map(|mask| {
                            self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining)
                                .or_else(|| {
                                    self.expr_upper_bound_usize_cached(
                                        right, bounds, ordering, remaining,
                                    )
                                })
                                .map_or(mask, |bound| bound.min(mask))
                        }),
                    SymBinOp::Shr => {
                        let left =
                            self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?;
                        let shift = usize::try_from(right.as_const()?).ok()?;
                        Some(if shift >= usize::BITS as usize { 0 } else { left >> shift })
                    }
                    SymBinOp::Sub => {
                        if let Some(difference) = left
                            .constant_difference(right)
                            .and_then(|difference| usize::try_from(difference).ok())
                        {
                            return Some(difference);
                        }
                        let left_bound =
                            self.expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?;
                        self.expressions_are_unsigned_ordered(right, left, ordering, remaining)
                            .then_some(left_bound)
                    }
                    SymBinOp::Shl => match right.as_const() {
                        Some(shift) if shift >= U256::from(256) => Some(0),
                        Some(shift) => usize::try_from(shift).ok().and_then(|shift| {
                            let bound = self
                                .expr_upper_bound_usize_cached(left, bounds, ordering, remaining)?;
                            if bound == 0 {
                                return Some(0);
                            }
                            let factor = 1usize.checked_shl(u32::try_from(shift).ok()?)?;
                            bound.checked_mul(factor)
                        }),
                        None => None,
                    },
                    SymBinOp::SDiv
                    | SymBinOp::SRem
                    | SymBinOp::Or
                    | SymBinOp::Xor
                    | SymBinOp::Sar => None,
                },
            }
        });

        let bound = match (constraint_bound, structural_bound) {
            (Some(left), Some(right)) => Some(left.min(right)),
            (Some(bound), None) | (None, Some(bound)) => Some(bound),
            (None, None) => None,
        };
        bounds.insert(expr.clone(), bound);
        bound
    }

    fn expressions_are_unsigned_ordered(
        &self,
        left: &SymExpr,
        right: &SymExpr,
        ordering: &mut HashMap<(SymExpr, SymExpr), bool>,
        remaining: &mut usize,
    ) -> bool {
        if left == right {
            return true;
        }
        let key = (left.clone(), right.clone());
        if let Some(ordered) = ordering.get(&key) {
            return *ordered;
        }
        let Some(next) = remaining.checked_sub(1) else { return false };
        *remaining = next;

        let ordered = if let (Some(left), Some(right)) = (left.as_const(), right.as_const()) {
            left <= right
        } else if let SymExprKind::Ite(condition, then_value, else_value) = left.kind() {
            let then_ordered = condition
                .implies_unsigned_less_or_equal(true, then_value, right, remaining)
                || self.expressions_are_unsigned_ordered(then_value, right, ordering, remaining);
            let else_ordered = condition
                .implies_unsigned_less_or_equal(false, else_value, right, remaining)
                || self.expressions_are_unsigned_ordered(else_value, right, ordering, remaining);
            then_ordered && else_ordered
        } else if let SymExprKind::Ite(condition, then_value, else_value) = right.kind() {
            let then_ordered = condition
                .implies_unsigned_less_or_equal(true, left, then_value, remaining)
                || self.expressions_are_unsigned_ordered(left, then_value, ordering, remaining);
            let else_ordered = condition
                .implies_unsigned_less_or_equal(false, left, else_value, remaining)
                || self.expressions_are_unsigned_ordered(left, else_value, ordering, remaining);
            then_ordered && else_ordered
        } else {
            false
        };
        ordering.insert(key, ordered);
        ordered
    }

    fn expr_lower_bound_usize(
        &self,
        expr: &SymExpr,
        lower_bounds: &mut HashMap<SymExpr, usize>,
        upper_bounds: &mut HashMap<SymExpr, Option<usize>>,
        ordering: &mut HashMap<(SymExpr, SymExpr), bool>,
        remaining: &mut usize,
    ) -> usize {
        if let Some(bound) = lower_bounds.get(expr) {
            return *bound;
        }
        if let Some(value) = expr.as_const().and_then(|value| usize::try_from(value).ok()) {
            return value;
        }
        let Some(next) = remaining.checked_sub(1) else {
            return 0;
        };
        *remaining = next;

        let bound = match expr.kind() {
            SymExprKind::Const(value) => usize::try_from(*value).unwrap_or_default(),
            SymExprKind::Ite(_, left, right) => {
                let left = self.expr_lower_bound_usize(
                    left,
                    lower_bounds,
                    upper_bounds,
                    ordering,
                    remaining,
                );
                let right = self.expr_lower_bound_usize(
                    right,
                    lower_bounds,
                    upper_bounds,
                    ordering,
                    remaining,
                );
                left.min(right)
            }
            SymExprKind::BinOp(SymBinOp::Add, left, right) => {
                let no_wrap = self
                    .expr_upper_bound_usize_cached(left, upper_bounds, ordering, remaining)
                    .and_then(|left| {
                        self.expr_upper_bound_usize_cached(right, upper_bounds, ordering, remaining)
                            .and_then(|right| left.checked_add(right))
                    })
                    .is_some();
                if no_wrap {
                    let left = self.expr_lower_bound_usize(
                        left,
                        lower_bounds,
                        upper_bounds,
                        ordering,
                        remaining,
                    );
                    let right = self.expr_lower_bound_usize(
                        right,
                        lower_bounds,
                        upper_bounds,
                        ordering,
                        remaining,
                    );
                    left.checked_add(right).unwrap_or_default()
                } else {
                    0
                }
            }
            SymExprKind::BinOp(SymBinOp::Sub, left, right) => left
                .constant_difference(right)
                .and_then(|difference| usize::try_from(difference).ok())
                .unwrap_or_default(),
            SymExprKind::BinOp(SymBinOp::Or, left, right) => {
                let left = self.expr_lower_bound_usize(
                    left,
                    lower_bounds,
                    upper_bounds,
                    ordering,
                    remaining,
                );
                let right = self.expr_lower_bound_usize(
                    right,
                    lower_bounds,
                    upper_bounds,
                    ordering,
                    remaining,
                );
                left.max(right)
            }
            SymExprKind::Var(_)
            | SymExprKind::GasLeft(_)
            | SymExprKind::Keccak { .. }
            | SymExprKind::Hash { .. }
            | SymExprKind::Not(_)
            | SymExprKind::BinOp(_, _, _)
            | SymExprKind::TernOp(_, _, _, _) => 0,
        };
        lower_bounds.insert(expr.clone(), bound);
        bound
    }

    pub(crate) fn constraint_upper_bound_usize(&self, expr: &SymExpr) -> Option<usize> {
        let mut bound: Option<usize> = None;
        for constraint in &self.constraints {
            if let Some(candidate) = constraint.upper_bound_usize(expr) {
                bound = Some(bound.map_or(candidate, |bound| bound.min(candidate)));
            }
        }
        bound
    }

    pub(crate) fn expect_constrained_usize(
        &self,
        cx: &mut SymCx,
        expr: SymExpr,
        reason: &'static str,
    ) -> Result<usize, SymbolicError> {
        self.constrained_usize(cx, &expr).ok_or(SymbolicError::Unsupported(reason))
    }

    pub(crate) fn expect_constrained_word(
        &self,
        cx: &mut SymCx,
        expr: SymExpr,
        reason: &'static str,
    ) -> Result<U256, SymbolicError> {
        self.constrained_word(cx, &expr).ok_or(SymbolicError::Unsupported(reason))
    }

    pub(crate) fn bin_word(&mut self, cx: &mut SymCx, op: SymBinOp) -> Result<(), SymbolicError> {
        let a = self.stack.pop()?;
        let b = self.stack.pop()?;
        self.stack.push(SymExpr::binop(cx, op, a, b))
    }

    pub(crate) fn bin_word_div_zero_guard(
        &mut self,
        cx: &mut SymCx,
        op: SymBinOp,
    ) -> Result<(), SymbolicError> {
        let a = self.stack.pop()?;
        let b = self.stack.pop()?;
        let zero = SymExpr::zero(cx);
        let condition = SymBoolExpr::eq(cx, b.clone(), zero.clone());
        let expr = SymExpr::binop(cx, op, a, b);
        self.stack.push(SymExpr::ite(cx, condition, zero, expr))
    }

    pub(crate) fn cmp_word_condition(
        &mut self,
        cx: &mut SymCx,
        op: SymCmpOp,
    ) -> Result<SymBoolExpr, SymbolicError> {
        let a = self.stack.pop()?;
        let b = self.stack.pop()?;
        Ok(SymBoolExpr::cmp(cx, op, a, b))
    }

    pub(crate) fn shift_word(&mut self, cx: &mut SymCx, op: SymBinOp) -> Result<(), SymbolicError> {
        let shift = self.stack.pop()?;
        let value = self.stack.pop()?;
        let expr = SymExpr::binop(cx, op, value, shift);
        let result = expr.known_word().map(|word| SymExpr::constant(cx, word)).unwrap_or(expr);
        self.stack.push(result)
    }

    pub(crate) fn exp_word(&mut self, cx: &mut SymCx) -> Result<(), SymbolicError> {
        let base = self.stack.pop()?;
        let exponent = self.stack.pop()?;
        let result = if let Some(exponent) = self.constrained_word(cx, &exponent) {
            if let Some(base_value) = base.as_const() {
                SymExpr::constant(cx, base_value.wrapping_pow(exponent))
            } else if exponent <= U256::from(SYMBOLIC_EXP_CONCRETE_EXPONENT_LIMIT) {
                exp_expr_for_concrete_exponent(
                    cx,
                    base,
                    usize::try_from(exponent).expect("checked symbolic exponent"),
                )
            } else {
                return Err(SymbolicError::Unsupported("symbolic EXP base"));
            }
        } else {
            let exponent_limit = if base.as_const().is_some() {
                CONCRETE_BASE_SYMBOLIC_EXPONENT_LIMIT
            } else {
                SYMBOLIC_EXP_CONCRETE_EXPONENT_LIMIT
            };
            let max_exponent = self
                .upper_bound_usize(cx, &exponent)
                .filter(|exponent| *exponent <= exponent_limit as usize)
                .ok_or(SymbolicError::Unsupported("symbolic EXP exponent"))?;
            let mut expr = SymExpr::zero(cx);
            for candidate in (0..=max_exponent).rev() {
                let candidate_expr = SymExpr::constant(cx, U256::from(candidate));
                let condition = SymBoolExpr::eq(cx, exponent.clone(), candidate_expr);
                let value = exp_expr_for_concrete_exponent(cx, base.clone(), candidate);
                expr = SymExpr::ite(cx, condition, value, expr);
            }
            expr
        };
        self.stack.push(result)
    }

    pub(crate) fn balance(
        &self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> SymExpr {
        self.world.balance_word_for_address(cx, executor, address)
    }

    pub(crate) fn balance_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        self.world.balance_word(cx, executor, address_expr)
    }

    pub(crate) fn extcode_size_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        self.world.extcode_size_word(cx, executor, address_expr)
    }

    pub(crate) fn extcode_hash_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        self.world.extcode_hash_word(cx, executor, address_expr)
    }

    pub(crate) fn extcode_bytes_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
        offset: SymExpr,
        size: usize,
    ) -> Result<SymBytes, SymbolicError> {
        self.world.extcode_bytes_word(cx, executor, address_expr, offset, size)
    }

    pub(crate) fn pop_address_word_or_symbolic_slot(
        &mut self,
        cx: &mut SymCx,
    ) -> Result<(SymExpr, Address), SymbolicError> {
        let expr = self.stack.pop()?;
        let address = self.address_or_symbolic_slot(cx, expr.clone());
        Ok((expr, address))
    }

    pub(crate) fn address_or_symbolic_slot(&mut self, cx: &mut SymCx, expr: SymExpr) -> Address {
        if let Some(value) = self.constrained_word(cx, &expr) {
            return word_to_address(value);
        }
        self.world.resolve_address(&expr).unwrap_or_else(|| self.world.symbolic_address_slot(expr))
    }

    pub(crate) fn fresh_word(&mut self, cx: &mut SymCx, prefix: &'static str) -> SymExpr {
        let id = self.next_symbol;
        self.next_symbol += 1;
        SymExpr::var(cx, &format!("{prefix}_{id}"))
    }

    pub(crate) fn fresh_gasleft(&mut self, cx: &mut SymCx) -> SymExpr {
        let id = self.next_symbol;
        self.next_symbol += 1;
        SymExpr::gas_left(cx, id)
    }

    pub(crate) fn fresh_bounded_uint(&mut self, cx: &mut SymCx, bits: U256) -> SymExpr {
        let value = self.fresh_word(cx, "symbolic");
        if bits < U256::from(256) {
            let upper = if bits.is_zero() {
                U256::ZERO
            } else {
                U256::ONE << usize::try_from(bits).expect("checked bit width")
            };
            self.constraints.push(SymBoolExpr::cmp_word_const(cx, SymCmpOp::Ult, &value, upper));
        }
        value
    }

    pub(crate) fn fresh_bytes(&mut self, cx: &mut SymCx, len: usize) -> Vec<SymExpr> {
        (0..len).map(|_| self.fresh_bounded_uint(cx, U256::from(8))).collect()
    }

    pub(crate) fn fresh_printable_ascii_bytes(
        &mut self,
        cx: &mut SymCx,
        len: usize,
    ) -> Vec<SymExpr> {
        (0..len)
            .map(|_| {
                let byte = self.fresh_bounded_uint(cx, U256::from(8));
                self.constraints.push(SymBoolExpr::cmp_word_const(
                    cx,
                    SymCmpOp::Uge,
                    &byte,
                    U256::from(0x20),
                ));
                self.constraints.push(SymBoolExpr::cmp_word_const(
                    cx,
                    SymCmpOp::Ule,
                    &byte,
                    U256::from(0x7e),
                ));
                byte
            })
            .collect()
    }

    pub(crate) fn fresh_bounded_int(&mut self, cx: &mut SymCx, bits: U256) -> SymExpr {
        let value = self.fresh_word(cx, "symbolic");
        if bits.is_zero() {
            self.constraints.push(SymBoolExpr::eq_word_const(cx, &value, U256::ZERO));
        } else if bits < U256::from(256) {
            let magnitude = U256::ONE << (usize::try_from(bits).expect("checked bit width") - 1);
            let lt = SymBoolExpr::cmp_word_const(cx, SymCmpOp::Ult, &value, magnitude);
            let ge = SymBoolExpr::cmp_word_const(
                cx,
                SymCmpOp::Uge,
                &value,
                U256::ZERO.wrapping_sub(magnitude),
            );
            let condition = SymBoolExpr::or(cx, vec![lt, ge]);
            self.constraints.push(condition);
        }
        value
    }

    pub(crate) fn prank_for_next_call(&mut self) -> (Address, SymExpr, Option<(Address, SymExpr)>) {
        if let Some((caller, caller_word)) = self.prank.next_caller.take() {
            (caller, caller_word, self.prank.next_origin.take())
        } else {
            match self.prank.persistent_caller.clone() {
                Some((caller, caller_word)) => {
                    (caller, caller_word, self.prank.persistent_origin.clone())
                }
                None => {
                    (self.address, self.address_word.clone(), self.prank.persistent_origin.clone())
                }
            }
        }
    }

    pub(crate) fn read_callers_words(&self, cx: &mut SymCx) -> Vec<SymExpr> {
        let (mode, caller, origin) = if let Some((_, caller_word)) = self.prank.next_caller.as_ref()
        {
            (
                U256::from(3),
                caller_word.clone(),
                self.prank
                    .next_origin
                    .as_ref()
                    .map(|(_, origin_word)| origin_word.clone())
                    .unwrap_or_else(|| self.origin_word.clone()),
            )
        } else if let Some((_, caller_word)) = self.prank.persistent_caller.as_ref() {
            (
                U256::from(4),
                caller_word.clone(),
                self.prank
                    .persistent_origin
                    .as_ref()
                    .map(|(_, origin_word)| origin_word.clone())
                    .unwrap_or_else(|| self.origin_word.clone()),
            )
        } else {
            (U256::ZERO, self.caller_word.clone(), self.origin_word.clone())
        };
        vec![SymExpr::constant(cx, mode), caller, origin]
    }

    pub(crate) fn record_log(&mut self, log: SymbolicLog) {
        if let Some(logs) = &mut self.recorded_logs {
            logs.push(log);
        }
    }

    pub(crate) fn record_sload(&mut self, address: Address, slot: SymExpr) {
        if let Some(record) = &mut self.access_record {
            record.read(address, slot);
        }
    }

    pub(crate) fn record_sstore(&mut self, address: Address, slot: SymExpr) {
        if let Some(record) = &mut self.access_record {
            record.write(address, slot);
        }
    }

    pub(crate) fn expectations_satisfied(&self) -> bool {
        self.expected_revert.is_none()
            && self.expected_emit.as_ref().is_none_or(ExpectedEmit::is_satisfied)
            && self.expected_calls.iter().all(ExpectedCall::is_satisfied)
            && self.expected_creates.is_empty()
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) struct SymbolicStorageHook {
    pub(crate) callback_target: Address,
    pub(crate) callback_selector: [u8; 4],
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct SymbolicLog {
    topics: Arc<[SymExpr]>,
    data_len: SymExpr,
    data: SymBytes,
    emitter: Address,
}

impl SymbolicLog {
    pub(crate) fn new(
        topics: Vec<SymExpr>,
        data_len: SymExpr,
        data: SymBytes,
        emitter: Address,
    ) -> Self {
        Self { topics: topics.into(), data_len, data, emitter }
    }

    pub(crate) fn into_parts(self) -> (Arc<[SymExpr]>, SymExpr, SymBytes, Address) {
        (self.topics, self.data_len, self.data, self.emitter)
    }
}

#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub(crate) struct AccessRecord {
    reads: HashMap<Address, Vec<SymExpr>>,
    writes: HashMap<Address, Vec<SymExpr>>,
}

impl AccessRecord {
    pub(crate) fn read(&mut self, address: Address, slot: SymExpr) {
        Self::push_unique_slot(self.reads.entry(address).or_default(), slot);
    }

    pub(crate) fn write(&mut self, address: Address, slot: SymExpr) {
        self.read(address, slot.clone());
        Self::push_unique_slot(self.writes.entry(address).or_default(), slot);
    }

    pub(crate) fn addresses(&self) -> Vec<Address> {
        let mut addresses = HashSet::<Address>::default();
        addresses.extend(self.reads.keys().copied());
        addresses.extend(self.writes.keys().copied());
        let mut addresses = addresses.into_iter().collect::<Vec<_>>();
        addresses.sort_unstable();
        addresses
    }

    pub(crate) fn read_slots(&self, address: Address) -> Vec<SymExpr> {
        self.reads.get(&address).cloned().unwrap_or_default()
    }

    pub(crate) fn write_slots(&self, address: Address) -> Vec<SymExpr> {
        self.writes.get(&address).cloned().unwrap_or_default()
    }

    fn push_unique_slot(slots: &mut Vec<SymExpr>, slot: SymExpr) {
        if !slots.iter().any(|existing| existing == &slot) {
            slots.push(slot);
        }
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct ExpectedRevert {
    data: ExpectedRevertData,
    reverter: Option<SymExpr>,
    remaining: u64,
}

impl ExpectedRevert {
    pub(crate) fn new(data: ExpectedRevertData, reverter: Option<SymExpr>, remaining: u64) -> Self {
        Self { data, reverter, remaining: remaining.max(1) }
    }

    pub(crate) const fn consume_one(&mut self) -> bool {
        self.remaining = self.remaining.saturating_sub(1);
        self.remaining == 0
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        reverter: Address,
        return_data: &SymReturnData,
    ) -> Option<SymBoolExpr> {
        let mut conditions = Vec::new();
        if let Some(expected_reverter) = &self.reverter {
            conditions.push(expected_reverter.address_match_condition(cx, reverter));
        }
        match &self.data {
            ExpectedRevertData::Any => {}
            ExpectedRevertData::Prefix(prefix) => {
                if return_data.len() < prefix.len() {
                    return None;
                }
                let prefix_len = SymExpr::constant(cx, U256::from(prefix.len()));
                conditions.push(SymBoolExpr::cmp_word_expr(
                    cx,
                    SymCmpOp::Uge,
                    &return_data.len_word,
                    prefix_len,
                ));
                conditions.extend((0..prefix.len()).map(|offset| {
                    let expected = prefix.byte(cx, offset);
                    let actual = return_data.byte(cx, offset);
                    SymBoolExpr::eq(cx, actual, expected)
                }));
            }
            ExpectedRevertData::Exact(data) => {
                if return_data.len() < data.len() {
                    return None;
                }
                let len = SymExpr::constant(cx, U256::from(data.len()));
                conditions.push(SymBoolExpr::eq(cx, return_data.len_word.clone(), len));
                conditions.extend((0..data.len()).map(|offset| {
                    let expected = data.byte(cx, offset);
                    let actual = return_data.byte(cx, offset);
                    SymBoolExpr::eq(cx, actual, expected)
                }));
            }
        }
        Some(SymBoolExpr::and(cx, conditions))
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) enum ExpectedRevertData {
    Any,
    Prefix(SymBytes),
    Exact(SymBytes),
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) enum AssumeNoRevert {
    Any,
    Filtered(Vec<ExpectedRevert>),
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct ExpectedCall {
    callee: SymExpr,
    value: Option<U256>,
    gas: Option<u64>,
    min_gas: Option<u64>,
    data: SymBytes,
    expected: u64,
    observed: u64,
    exact: bool,
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct ExpectedCreate {
    bytecode: Vec<u8>,
    deployer: SymExpr,
    kind: CreateKind,
}

impl ExpectedCreate {
    pub(crate) const fn new(bytecode: Vec<u8>, deployer: SymExpr, kind: CreateKind) -> Self {
        Self { bytecode, deployer, kind }
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        deployer: Address,
        kind: CreateKind,
        bytecode: &[u8],
    ) -> Option<SymBoolExpr> {
        (self.kind == kind && self.bytecode == bytecode)
            .then(|| self.deployer.address_match_condition(cx, deployer))
    }
}

impl ExpectedCall {
    pub(crate) fn new(
        callee: SymExpr,
        value: Option<U256>,
        gas: Option<u64>,
        min_gas: Option<u64>,
        data: SymBytes,
        count: Option<u64>,
    ) -> Self {
        let (gas, min_gas) = if value.is_some_and(|value| !value.is_zero()) {
            (
                gas.map(|gas| gas.saturating_add(CALL_STIPEND)),
                min_gas.map(|gas| gas.saturating_add(CALL_STIPEND)),
            )
        } else {
            (gas, min_gas)
        };
        Self {
            callee,
            value,
            gas,
            min_gas,
            data,
            expected: count.unwrap_or(1),
            observed: 0,
            exact: count.is_some(),
        }
    }

    pub(crate) const fn value(&self) -> Option<U256> {
        self.value
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        callee: Address,
        value: Option<U256>,
        gas: &SymExpr,
        calldata: &SymBytes,
    ) -> Result<Option<SymBoolExpr>, SymbolicError> {
        if !self.value.is_none_or(|expected| value.is_some_and(|value| expected == value))
            || !self.gas_matches(gas, value)?
        {
            return Ok(None);
        }
        let Some(data_condition) = calldata.prefix_condition(cx, &self.data) else {
            return Ok(None);
        };
        let callee_condition = self.callee.address_match_condition(cx, callee);
        Ok(Some(SymBoolExpr::and(cx, vec![callee_condition, data_condition])))
    }

    fn gas_matches(&self, gas: &SymExpr, value: Option<U256>) -> Result<bool, SymbolicError> {
        if self.gas.is_none() && self.min_gas.is_none() {
            return Ok(true);
        }
        let mut gas = gas.as_const_or("symbolic expected call gas")?;
        if value.is_some_and(|value| !value.is_zero()) {
            gas = gas.saturating_add(U256::from(CALL_STIPEND));
        }
        Ok(self.gas.is_none_or(|expected| gas == U256::from(expected))
            && self.min_gas.is_none_or(|expected| gas >= U256::from(expected)))
    }

    pub(crate) const fn observe(&mut self) -> bool {
        if self.exact && self.observed >= self.expected {
            return false;
        }
        self.observed = self.observed.saturating_add(1);
        true
    }

    pub(crate) const fn is_satisfied(&self) -> bool {
        if self.exact { self.observed == self.expected } else { self.observed >= self.expected }
    }
}

/// Registers an expected call using the concrete cheatcode's keyed-additive semantics.
pub(crate) fn register_expected_call(
    expected_calls: &mut Vec<ExpectedCall>,
    cx: &mut SymCx,
    expected: ExpectedCall,
) -> Result<(), &'static str> {
    if let Some(existing) = expected_calls
        .iter_mut()
        .find(|call| call.callee == expected.callee && call.data.same_bytes(cx, &expected.data))
    {
        if expected.exact {
            return Err("counted expected calls can only bet set once");
        }
        if existing.exact {
            return Err("cannot overwrite a counted expectCall with a non-counted expectCall");
        }
        existing.expected += 1;
    } else {
        expected_calls.push(expected);
    }
    Ok(())
}

#[derive(Clone, Debug)]
pub(crate) struct CallMock {
    pub(crate) callee: SymExpr,
    value: Option<U256>,
    pub(crate) data: SymBytes,
    returns: Vec<SymReturnData>,
    reverts: bool,
    calls: usize,
}

impl CallMock {
    pub(crate) const fn new(
        callee: SymExpr,
        value: Option<U256>,
        data: SymBytes,
        returns: Vec<SymReturnData>,
        reverts: bool,
    ) -> Self {
        Self { callee, value, data, returns, reverts, calls: 0 }
    }

    pub(crate) const fn value(&self) -> Option<U256> {
        self.value
    }

    pub(crate) fn specificity(&self) -> (usize, bool) {
        (self.data.len(), self.value.is_some())
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        callee: Address,
        value: Option<U256>,
        calldata: &SymBytes,
    ) -> Option<SymBoolExpr> {
        if !self.value.is_none_or(|expected| value.is_some_and(|value| expected == value)) {
            return None;
        }
        let data_condition = calldata.prefix_condition(cx, &self.data)?;
        let callee_condition = self.callee.address_match_condition(cx, callee);
        Some(SymBoolExpr::and(cx, vec![callee_condition, data_condition]))
    }

    pub(crate) fn next_outcome(&mut self, cx: &mut SymCx) -> CallMockOutcome {
        let idx = self.calls.min(self.returns.len().saturating_sub(1));
        self.calls = self.calls.saturating_add(1);
        CallMockOutcome {
            return_data: self.returns.get(idx).cloned().unwrap_or_else(|| SymReturnData::empty(cx)),
            reverts: self.reverts,
        }
    }
}

#[derive(Clone, Debug)]
pub(crate) struct CallMockOutcome {
    return_data: SymReturnData,
    reverts: bool,
}

impl CallMockOutcome {
    pub(crate) fn into_parts(self) -> (SymReturnData, bool) {
        (self.return_data, self.reverts)
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct FunctionMock {
    callee: SymExpr,
    target: Address,
    data: SymBytes,
}

impl FunctionMock {
    pub(crate) const fn new(callee: SymExpr, target: Address, data: SymBytes) -> Self {
        Self { callee, target, data }
    }

    pub(crate) fn matches_definition(
        &self,
        cx: &mut SymCx,
        callee: &SymExpr,
        data: &SymBytes,
    ) -> bool {
        self.callee == *callee && self.data.same_bytes(cx, data)
    }

    pub(crate) const fn set_target(&mut self, target: Address) {
        self.target = target;
    }

    pub(crate) fn calldata_len(&self) -> usize {
        self.data.len()
    }

    pub(crate) const fn target(&self) -> Address {
        self.target
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        callee: Address,
        calldata: &SymBytes,
    ) -> Option<SymBoolExpr> {
        let data_condition = calldata.prefix_condition(cx, &self.data)?;
        let callee_condition = self.callee.address_match_condition(cx, callee);
        Some(SymBoolExpr::and(cx, vec![callee_condition, data_condition]))
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct ExpectedEmit {
    checks: ExpectedEmitChecks,
    emitter: Option<SymExpr>,
    remaining: u64,
    template: Option<SymbolicLog>,
}

impl ExpectedEmit {
    pub(crate) fn new(
        checks: ExpectedEmitChecks,
        emitter: Option<SymExpr>,
        remaining: u64,
    ) -> Self {
        Self { checks, emitter, remaining: remaining.max(1), template: None }
    }

    pub(crate) const fn is_satisfied(&self) -> bool {
        self.template.is_none() && self.remaining == 0
    }

    pub(crate) const fn template(&self) -> Option<&SymbolicLog> {
        self.template.as_ref()
    }

    pub(crate) fn set_template(&mut self, log: SymbolicLog) {
        self.template = Some(log);
    }

    pub(crate) fn consume_one(&mut self) -> bool {
        self.remaining = self.remaining.saturating_sub(1);
        if self.remaining == 0 {
            self.template = None;
            true
        } else {
            false
        }
    }

    pub(crate) fn match_condition(
        &self,
        cx: &mut SymCx,
        template: &SymbolicLog,
        actual: &SymbolicLog,
    ) -> Option<SymBoolExpr> {
        let mut conditions = Vec::new();
        if let Some(expected_emitter) = &self.emitter {
            conditions.push(expected_emitter.address_match_condition(cx, actual.emitter));
        }
        for (idx, &check_topic) in self.checks.topics.iter().enumerate() {
            if !check_topic {
                continue;
            }
            match (template.topics.get(idx), actual.topics.get(idx)) {
                (Some(left), Some(right)) => {
                    conditions.push(SymBoolExpr::eq(cx, left.clone(), right.clone()));
                }
                (None, None) => {}
                _ => return None,
            }
        }

        if self.checks.data {
            conditions.push(SymBoolExpr::eq(
                cx,
                template.data_len.clone(),
                actual.data_len.clone(),
            ));
            if template.data.len() != actual.data.len() {
                return None;
            }
            conditions.extend((0..template.data.len()).map(|idx| {
                let template = template.data.byte(cx, idx);
                let actual = actual.data.byte(cx, idx);
                SymBoolExpr::eq(cx, template, actual)
            }));
        }

        Some(SymBoolExpr::and(cx, conditions))
    }
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub(crate) struct ExpectedEmitChecks {
    topics: [bool; 4],
    data: bool,
}

impl Default for ExpectedEmitChecks {
    fn default() -> Self {
        Self { topics: [true; 4], data: true }
    }
}

impl ExpectedEmitChecks {
    pub(crate) fn from_non_anonymous_args(
        cx: &mut SymCx,
        memory: &SymMemory,
        args_offset: usize,
    ) -> Result<Self, SymbolicError> {
        Ok(Self {
            topics: [
                true,
                read_abi_bool_arg(cx, memory, args_offset, 0, "symbolic vm.expectEmit")?,
                read_abi_bool_arg(cx, memory, args_offset, 1, "symbolic vm.expectEmit")?,
                read_abi_bool_arg(cx, memory, args_offset, 2, "symbolic vm.expectEmit")?,
            ],
            data: read_abi_bool_arg(cx, memory, args_offset, 3, "symbolic vm.expectEmit")?,
        })
    }

    pub(crate) fn from_anonymous_args(
        cx: &mut SymCx,
        memory: &SymMemory,
        args_offset: usize,
    ) -> Result<Self, SymbolicError> {
        Ok(Self {
            topics: [
                read_abi_bool_arg(cx, memory, args_offset, 0, "symbolic vm.expectEmitAnonymous")?,
                read_abi_bool_arg(cx, memory, args_offset, 1, "symbolic vm.expectEmitAnonymous")?,
                read_abi_bool_arg(cx, memory, args_offset, 2, "symbolic vm.expectEmitAnonymous")?,
                read_abi_bool_arg(cx, memory, args_offset, 3, "symbolic vm.expectEmitAnonymous")?,
            ],
            data: read_abi_bool_arg(cx, memory, args_offset, 4, "symbolic vm.expectEmitAnonymous")?,
        })
    }
}

impl Deref for PathState {
    type Target = CallFrame;

    fn deref(&self) -> &Self::Target {
        &self.frame
    }
}

impl DerefMut for PathState {
    fn deref_mut(&mut self) -> &mut Self::Target {
        &mut self.frame
    }
}

#[derive(Clone, Debug)]
pub(crate) struct CallFrame {
    pub(crate) pc: usize,
    pub(crate) address: Address,
    pub(crate) address_word: SymExpr,
    pub(crate) storage_address: Address,
    pub(crate) caller: Address,
    pub(crate) caller_word: SymExpr,
    pub(crate) callvalue: SymExpr,
    pub(crate) is_static: bool,
    pub(crate) calldata: SymCalldata,
    pub(crate) stack: SymStack,
    pub(crate) memory: SymMemory,
    pub(crate) return_data: SymReturnData,
}

impl CallFrame {
    pub(crate) fn new(
        cx: &mut SymCx,
        address: Address,
        storage_address: Address,
        caller: Address,
        callvalue: SymExpr,
        is_static: bool,
        calldata: SymCalldata,
    ) -> Self {
        Self {
            pc: 0,
            address,
            address_word: SymExpr::constant(cx, address_word(address)),
            storage_address,
            caller,
            caller_word: SymExpr::constant(cx, address_word(caller)),
            callvalue,
            is_static,
            calldata,
            stack: SymStack::default(),
            memory: SymMemory::default(),
            return_data: SymReturnData::empty(cx),
        }
    }
}

#[derive(Clone, Debug, Default, PartialEq, Eq)]
pub(crate) struct SymbolicPrank {
    next_caller: Option<(Address, SymExpr)>,
    next_origin: Option<(Address, SymExpr)>,
    persistent_caller: Option<(Address, SymExpr)>,
    persistent_origin: Option<(Address, SymExpr)>,
}

impl SymbolicPrank {
    pub(crate) fn set_next(
        &mut self,
        caller: (Address, SymExpr),
        origin: Option<(Address, SymExpr)>,
    ) {
        self.next_caller = Some(caller);
        self.next_origin = origin;
    }

    pub(crate) fn set_persistent(
        &mut self,
        caller: (Address, SymExpr),
        origin: Option<(Address, SymExpr)>,
    ) {
        self.persistent_caller = Some(caller);
        self.persistent_origin = origin;
    }

    pub(crate) const fn has_active(&self) -> bool {
        self.next_caller.is_some()
            || self.next_origin.is_some()
            || self.persistent_caller.is_some()
            || self.persistent_origin.is_some()
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub(crate) struct StorageWrite {
    address: Address,
    key: SymExpr,
    value: SymExpr,
}

impl StorageWrite {
    pub(crate) const fn new(address: Address, key: SymExpr, value: SymExpr) -> Self {
        Self { address, key, value }
    }

    pub(crate) fn select_from(
        cx: &mut SymCx,
        writes: &[Self],
        address: Address,
        key: SymExpr,
        base: SymExpr,
    ) -> SymExpr {
        let mut value = base;
        for write in writes.iter().filter(|write| write.address == address) {
            value =
                key.clone().select_storage_write(cx, write.key.clone(), write.value.clone(), value);
        }
        value
    }
}

/// World data shared copy-on-write by branched paths and snapshots.
#[derive(Clone, Debug, Default)]
pub(crate) struct SymbolicWorldState {
    storage: Vec<StorageWrite>,
    transient_storage: Vec<StorageWrite>,
    created_accounts: HashSet<Address>,
    current_transaction_created_accounts: HashSet<Address>,
    balances: HashMap<Address, SymExpr>,
    code_cache: HashMap<Address, SymCode>,
    nonces: HashMap<Address, u64>,
    existing_accounts: HashSet<Address>,
    destroyed_accounts: HashSet<Address>,
    arbitrary_storage_accounts: HashMap<Address, bool>,
    arbitrary_storage_copies: HashMap<Address, Address>,
    arbitrary_storage_all: bool,
    zero_init_symbolic_storage: bool,
    symbolic_address_aliases: HashMap<SymExpr, Address>,
    replay_storage_slots: HashMap<Symbol, Vec<SymbolicReplayStorageSlot>>,
    replay_symbolic_storage_keys: HashMap<Symbol, Vec<(Address, SymExpr)>>,
}

#[derive(Clone, Debug)]
struct SymbolicReplayStorageSlot {
    address: Address,
    slot: U256,
}

#[derive(Clone, Debug, Default)]
pub(crate) struct SymbolicWorld {
    state: Arc<SymbolicWorldState>,
    snapshots: HashMap<U256, Arc<SymbolicWorldState>>,
    next_snapshot_id: u64,
}

impl Deref for SymbolicWorld {
    type Target = SymbolicWorldState;

    fn deref(&self) -> &Self::Target {
        &self.state
    }
}

impl SymbolicWorld {
    pub(crate) fn is_destroyed(&self, address: Address) -> bool {
        self.destroyed_accounts.contains(&address)
    }

    pub(crate) fn set_storage_layout(&mut self, layout: SymbolicStorageLayout) {
        let state = Arc::make_mut(&mut self.state);
        state.arbitrary_storage_all = matches!(layout, SymbolicStorageLayout::Generic);
        state.zero_init_symbolic_storage = matches!(layout, SymbolicStorageLayout::ZeroInit);
    }

    pub(crate) fn sload(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
        key: SymExpr,
        concrete_key: Option<U256>,
    ) -> Result<SymExpr, SymbolicError> {
        let base = self.storage_base(cx, executor, address, &key, concrete_key)?;
        let read_key = concrete_key.map(|key| SymExpr::constant(cx, key)).unwrap_or(key);
        Ok(StorageWrite::select_from(cx, &self.storage, address, read_key, base))
    }

    pub(crate) fn sstore(&mut self, address: Address, key: SymExpr, value: SymExpr) {
        Arc::make_mut(&mut self.state).storage.push(StorageWrite::new(address, key, value));
    }

    pub(crate) fn tload(&self, cx: &mut SymCx, address: Address, key: SymExpr) -> SymExpr {
        let base = SymExpr::zero(cx);
        StorageWrite::select_from(cx, &self.transient_storage, address, key, base)
    }

    pub(crate) fn tstore(&mut self, address: Address, key: SymExpr, value: SymExpr) {
        Arc::make_mut(&mut self.state)
            .transient_storage
            .push(StorageWrite::new(address, key, value));
    }

    /// Clears transaction-scoped state at a top-level call boundary.
    pub(crate) fn clear_transaction_scoped_state(&mut self) {
        let state = Arc::make_mut(&mut self.state);
        state.transient_storage.clear();
        state.current_transaction_created_accounts.clear();
    }

    /// Clears transient storage for a call that runs as its own transaction.
    pub(crate) fn clear_transient_storage(&mut self) {
        if !self.transient_storage.is_empty() {
            Arc::make_mut(&mut self.state).transient_storage.clear();
        }
    }

    /// Restores `outer`'s transient storage after a call that ran as its own transaction.
    pub(crate) fn restore_transient_storage(&mut self, outer: &Self) {
        if !self.transient_storage.is_empty() || !outer.transient_storage.is_empty() {
            Arc::make_mut(&mut self.state).transient_storage = outer.transient_storage.clone();
        }
    }

    pub(crate) fn mark_current_transaction_created(&mut self, address: Address) {
        let state = Arc::make_mut(&mut self.state);
        state.created_accounts.insert(address);
        state.current_transaction_created_accounts.insert(address);
    }

    /// Returns whether `address` was created in the current top-level symbolic transaction.
    pub(crate) fn was_created_in_current_transaction(&self, address: Address) -> bool {
        self.current_transaction_created_accounts.contains(&address)
    }

    pub(crate) fn enable_arbitrary_storage(&mut self, address: Address, overwrite: bool) {
        Arc::make_mut(&mut self.state).arbitrary_storage_accounts.insert(address, overwrite);
    }

    pub(crate) fn replay_storage_symbols(&self) -> SymbolicVars {
        self.replay_storage_slots
            .keys()
            .chain(self.replay_symbolic_storage_keys.keys())
            .copied()
            .collect()
    }

    pub(crate) fn replay_storage_assignments(
        &self,
        model: &SymbolicModel,
    ) -> Result<Vec<SymbolicStorageAssignment>, SymbolicError> {
        let mut assignments = std::collections::BTreeMap::<(Address, U256), U256>::new();
        for (symbol, slots) in &self.replay_storage_slots {
            let Some(value) = model.get(symbol).copied() else { continue };
            for slot in slots {
                match assignments.entry((slot.address, slot.slot)) {
                    std::collections::btree_map::Entry::Vacant(entry) => {
                        entry.insert(value);
                    }
                    std::collections::btree_map::Entry::Occupied(entry)
                        if *entry.get() == value => {}
                    std::collections::btree_map::Entry::Occupied(_) => {
                        return Err(SymbolicError::Solver(
                            "conflicting symbolic storage replay assignments".to_string(),
                        ));
                    }
                }
            }
        }
        // Replay validates aliases between symbolic keys that take the same concrete value.
        for (symbol, reads) in &self.replay_symbolic_storage_keys {
            let Some(value) = model.get(symbol).copied() else { continue };
            for (address, key) in reads {
                if let Some(slot) = key.eval_model_if_complete(model)? {
                    assignments.entry((*address, slot)).or_insert(value);
                }
            }
        }
        Ok(assignments
            .into_iter()
            .map(|((address, slot), value)| SymbolicStorageAssignment { address, slot, value })
            .collect())
    }

    pub(crate) fn resolve_address(&self, expr: &SymExpr) -> Option<Address> {
        expr.as_const().map(word_to_address).or_else(|| {
            self.symbolic_address_aliases.get(expr).copied().or_else(|| {
                self.symbolic_address_aliases.iter().find_map(|(alias, address)| {
                    expr.symbolic_address_equivalent(alias).then_some(*address)
                })
            })
        })
    }

    pub(crate) fn symbolic_address_slot(&mut self, expr: SymExpr) -> Address {
        if let Some(address) = self.resolve_address(&expr) {
            return address;
        }
        let address = expr.representative_symbolic_address();
        Arc::make_mut(&mut self.state).symbolic_address_aliases.insert(expr, address);
        address
    }

    pub(crate) fn symbolic_word_for_address(&self, address: Address) -> Option<SymExpr> {
        self.symbolic_address_aliases
            .iter()
            .find_map(|(word, slot)| (*slot == address).then(|| word.clone()))
    }

    pub(crate) fn snapshot_state(&mut self) -> U256 {
        let id = U256::from(self.next_snapshot_id);
        self.next_snapshot_id = self.next_snapshot_id.saturating_add(1);
        self.snapshots.insert(id, Arc::clone(&self.state));
        id
    }

    pub(crate) fn restore_snapshot(&mut self, id: U256) -> bool {
        let Some(snapshot) = self.snapshots.get(&id) else {
            return false;
        };
        self.state = Arc::clone(snapshot);
        true
    }

    pub(crate) fn delete_snapshot(&mut self, id: U256) -> bool {
        self.snapshots.remove(&id).is_some()
    }

    pub(crate) fn delete_snapshots(&mut self) {
        self.snapshots.clear();
    }

    pub(crate) fn storage_base(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
        key: &SymExpr,
        concrete_key: Option<U256>,
    ) -> Result<SymExpr, SymbolicError> {
        if let Some(base) = self.arbitrary_storage_base(cx, executor, address, key, concrete_key)? {
            return Ok(base);
        }
        if self.created_accounts.contains(&address) {
            return Ok(SymExpr::zero(cx));
        }
        if let Some(key) = concrete_key {
            return executor
                .backend
                .storage_ref(address, key)
                .map(|value| SymExpr::constant(cx, value))
                .map_err(|err| SymbolicError::Backend(err.to_string()));
        }
        if let Some(key) = key.as_const() {
            executor
                .backend
                .storage_ref(address, key)
                .map(|value| SymExpr::constant(cx, value))
                .map_err(|err| SymbolicError::Backend(err.to_string()))
        } else if self.zero_init_symbolic_storage {
            Ok(SymExpr::zero(cx))
        } else {
            let name = symbolic_storage_symbol(cx, address, key);
            Ok(SymExpr::get_var(cx, name))
        }
    }

    fn arbitrary_storage_base(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
        key: &SymExpr,
        concrete_key: Option<U256>,
    ) -> Result<Option<SymExpr>, SymbolicError> {
        if let Some(slot) = concrete_key.or_else(|| key.as_const())
            && !self.arbitrary_storage_all
        {
            let overwrite_arbitrary_storage =
                self.arbitrary_storage_accounts.get(&address).copied();
            let has_arbitrary_storage = overwrite_arbitrary_storage.is_some();
            let is_copied_storage =
                !has_arbitrary_storage && self.arbitrary_storage_copies.contains_key(&address);
            let preserve_nonzero_slot =
                overwrite_arbitrary_storage == Some(false) || is_copied_storage;
            if preserve_nonzero_slot {
                let concrete = executor
                    .backend
                    .storage_ref(address, slot)
                    .map_err(|err| SymbolicError::Backend(err.to_string()))?;
                if !concrete.is_zero() {
                    return Ok(Some(SymExpr::constant(cx, concrete)));
                }
            }
        }

        Ok(self.unchecked_arbitrary_storage_base(cx, address, key, concrete_key))
    }

    fn unchecked_arbitrary_storage_base(
        &mut self,
        cx: &mut SymCx,
        address: Address,
        key: &SymExpr,
        concrete_key: Option<U256>,
    ) -> Option<SymExpr> {
        let overwrite_arbitrary_storage = self.arbitrary_storage_accounts.get(&address).copied();
        let has_arbitrary_storage = overwrite_arbitrary_storage.is_some();
        let copied_source = (!has_arbitrary_storage)
            .then(|| self.arbitrary_storage_copies.get(&address).copied())
            .flatten();
        let symbol_address = if self.arbitrary_storage_all || has_arbitrary_storage {
            address
        } else {
            copied_source?
        };
        let symbol = symbolic_storage_symbol(cx, symbol_address, key);
        if let Some(slot) = concrete_key.or_else(|| key.as_const()) {
            if self.arbitrary_storage_all || has_arbitrary_storage {
                self.record_replay_storage_slot(symbol, address, slot);
            }
            if let Some(source) = copied_source {
                self.record_replay_storage_slot(symbol, source, slot);
                self.record_replay_storage_slot(symbol, address, slot);
            }
        } else if self.arbitrary_storage_all && copied_source.is_none() {
            // Generic storage replays reads at symbolic keys too.
            self.record_replay_symbolic_storage_key(symbol, address, key);
        }
        let value = SymExpr::get_var(cx, symbol);
        if let Some(source) = copied_source {
            self.sstore(source, key.clone(), value.clone());
        }
        Some(value)
    }

    fn record_replay_storage_slot(&mut self, symbol: Symbol, address: Address, slot: U256) {
        if self.replay_storage_slots.get(&symbol).is_some_and(|slots| {
            slots.iter().any(|existing| existing.address == address && existing.slot == slot)
        }) {
            return;
        }
        Arc::make_mut(&mut self.state)
            .replay_storage_slots
            .entry(symbol)
            .or_default()
            .push(SymbolicReplayStorageSlot { address, slot });
    }

    fn record_replay_symbolic_storage_key(
        &mut self,
        symbol: Symbol,
        address: Address,
        key: &SymExpr,
    ) {
        if self.replay_symbolic_storage_keys.get(&symbol).is_some_and(|reads| {
            reads.iter().any(|(existing, existing_key)| *existing == address && existing_key == key)
        }) {
            return;
        }
        Arc::make_mut(&mut self.state)
            .replay_symbolic_storage_keys
            .entry(symbol)
            .or_default()
            .push((address, key.clone()));
    }

    fn merge_replay_metadata_from(&mut self, other: &Self) {
        for (symbol, slots) in &other.replay_storage_slots {
            for slot in slots {
                self.record_replay_storage_slot(*symbol, slot.address, slot.slot);
            }
        }
        for (symbol, reads) in &other.replay_symbolic_storage_keys {
            for (address, key) in reads {
                self.record_replay_symbolic_storage_key(*symbol, *address, key);
            }
        }
        let state = Arc::make_mut(&mut self.state);
        for (expr, address) in &other.symbolic_address_aliases {
            state.symbolic_address_aliases.entry(expr.clone()).or_insert(*address);
        }
    }

    pub(crate) fn backend_balance(&self, executor: &ExecutorView<'_>, address: Address) -> U256 {
        executor
            .backend
            .basic_ref(address)
            .ok()
            .flatten()
            .map(|account| account.balance)
            .unwrap_or_default()
    }

    pub(crate) fn balance_word_for_address(
        &self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> SymExpr {
        if self.destroyed_accounts.contains(&address) {
            return SymExpr::zero(cx);
        }
        self.balances
            .get(&address)
            .cloned()
            .unwrap_or_else(|| SymExpr::constant(cx, self.backend_balance(executor, address)))
    }

    pub(crate) fn balance_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        if let Some(address) = self.resolve_address(&address_expr) {
            return Ok(self.balance_word_for_address(cx, executor, address));
        }

        let expr = address_expr;
        let representative = expr.representative_symbolic_address();
        let mut result = self.balance_word_for_address(cx, executor, representative);
        // Cheatcode accounts can hold balances even though they are not code candidates.
        let cheatcode_addresses = [CHEATCODE_ADDRESS, SYMBOLIC_VM_COMPAT_ADDRESS];
        for address in self.known_addresses(executor).into_iter().chain(cheatcode_addresses) {
            let balance = self.balance_word_for_address(cx, executor, address);
            let address = SymExpr::constant(cx, address_word(address));
            let condition = SymBoolExpr::eq(cx, expr.clone(), address);
            result = SymExpr::ite(cx, condition, balance, result);
        }

        Ok(result)
    }

    pub(crate) fn set_balance_word(&mut self, address: Address, value: SymExpr) {
        let account_exists = !value.as_const().is_some_and(|value| value.is_zero());
        let state = Arc::make_mut(&mut self.state);
        state.balances.insert(address, value);
        if account_exists {
            state.existing_accounts.insert(address);
            state.destroyed_accounts.remove(&address);
        }
    }

    pub(crate) fn transfer(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        from: Address,
        to: Address,
        value: SymExpr,
    ) {
        if from == to || value.as_const().is_some_and(|value| value.is_zero()) {
            return;
        }
        let from_balance = self.balance_word_for_address(cx, executor, from);
        let to_balance = self.balance_word_for_address(cx, executor, to);
        let from_balance = SymExpr::binop(cx, SymBinOp::Sub, from_balance, value.clone());
        let to_balance = SymExpr::binop(cx, SymBinOp::Add, to_balance, value);
        self.set_balance_word(from, from_balance);
        self.set_balance_word(to, to_balance);
    }

    pub(crate) fn nonce(
        &self,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<u64, SymbolicError> {
        if self.destroyed_accounts.contains(&address) {
            return Ok(self.nonces.get(&address).copied().unwrap_or_default());
        }
        if let Some(nonce) = self.nonces.get(&address) {
            return Ok(*nonce);
        }
        executor
            .backend
            .basic_ref(address)
            .map_err(|err| SymbolicError::Backend(err.to_string()))
            .map(|account| account.map(|account| account.nonce).unwrap_or_default())
    }

    pub(crate) fn set_nonce(&mut self, address: Address, nonce: u64) {
        let state = Arc::make_mut(&mut self.state);
        state.nonces.insert(address, nonce);
        if nonce != 0 {
            state.existing_accounts.insert(address);
            state.destroyed_accounts.remove(&address);
        }
    }

    pub(crate) fn increment_nonce(
        &mut self,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<(), SymbolicError> {
        let nonce = self.nonce(executor, address)?;
        self.set_nonce(address, nonce.saturating_add(1));
        Ok(())
    }

    pub(crate) fn has_code_or_nonce(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<bool, SymbolicError> {
        if self.destroyed_accounts.contains(&address) {
            return Ok(false);
        }
        Ok(!self.extcode(cx, executor, address)?.is_empty() || self.nonce(executor, address)? != 0)
    }

    pub(crate) fn install_code(&mut self, address: Address, code: SymCode) {
        let state = Arc::make_mut(&mut self.state);
        state.code_cache.insert(address, code);
        state.existing_accounts.insert(address);
        state.destroyed_accounts.remove(&address);
    }

    /// Implements legacy `SELFDESTRUCT` semantics.
    pub(crate) fn selfdestruct_legacy(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
        beneficiary: Address,
    ) -> Result<(), SymbolicError> {
        let balance = self.balance_word_for_address(cx, executor, address);
        if beneficiary != address && !balance.as_const().is_some_and(|value| value.is_zero()) {
            let beneficiary_balance = self.balance_word_for_address(cx, executor, beneficiary);
            let beneficiary_balance =
                SymExpr::binop(cx, SymBinOp::Add, beneficiary_balance, balance);
            self.set_balance_word(beneficiary, beneficiary_balance);
        }
        let nonce = if self.nonces.contains_key(&address) {
            None
        } else {
            Some(self.nonce(executor, address)?)
        };
        let zero = SymExpr::zero(cx);
        let empty_code = SymCode::empty(cx);
        let state = Arc::make_mut(&mut self.state);
        state.balances.insert(address, zero);
        state.code_cache.insert(address, empty_code);
        if let Some(nonce) = nonce {
            state.nonces.insert(address, nonce);
        }
        state.storage.retain(|write| write.address != address);
        state.transient_storage.retain(|write| write.address != address);
        state.created_accounts.remove(&address);
        state.current_transaction_created_accounts.remove(&address);
        state.existing_accounts.remove(&address);
        state.destroyed_accounts.insert(address);
        Ok(())
    }

    /// Implements Cancun+ `SELFDESTRUCT` semantics for accounts not created in the current tx.
    pub(crate) fn selfdestruct_cancun_existing(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
        beneficiary: Address,
    ) {
        let balance = self.balance_word_for_address(cx, executor, address);
        if beneficiary != address && !balance.as_const().is_some_and(|value| value.is_zero()) {
            let beneficiary_balance = self.balance_word_for_address(cx, executor, beneficiary);
            // Symbolic balances are treated as possibly non-zero, matching transfer's
            // account-existence approximation.
            let beneficiary_balance =
                SymExpr::binop(cx, SymBinOp::Add, beneficiary_balance, balance);
            self.set_balance_word(beneficiary, beneficiary_balance);
            let zero = SymExpr::zero(cx);
            Arc::make_mut(&mut self.state).balances.insert(address, zero);
        }
    }

    pub(crate) fn account_exists(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<bool, SymbolicError> {
        if address == CHEATCODE_ADDRESS || address == SYMBOLIC_VM_COMPAT_ADDRESS {
            return Ok(true);
        }
        if self.destroyed_accounts.contains(&address) {
            return Ok(false);
        }
        if self.existing_accounts.contains(&address) {
            return Ok(true);
        }
        if self
            .balances
            .get(&address)
            .is_some_and(|balance| !balance.as_const().is_some_and(|value| value.is_zero()))
            || self.nonces.get(&address).is_some_and(|nonce| *nonce != 0)
            || self.code_cache.get(&address).is_some_and(|code| !code.is_empty())
        {
            Arc::make_mut(&mut self.state).existing_accounts.insert(address);
            return Ok(true);
        }

        let Some(account) = executor
            .backend
            .basic_ref(address)
            .map_err(|err| SymbolicError::Backend(err.to_string()))?
        else {
            return Ok(false);
        };

        if account.nonce != 0 || !account.balance.is_zero() {
            Arc::make_mut(&mut self.state).existing_accounts.insert(address);
            return Ok(true);
        }

        if let Some(code) = account.code.as_ref()
            && !code.is_empty()
        {
            let code = SymCode::from_bytecode(cx, code);
            let state = Arc::make_mut(&mut self.state);
            state.code_cache.insert(address, code);
            state.existing_accounts.insert(address);
            return Ok(true);
        }

        Ok(false)
    }

    pub(crate) fn extcode(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<SymCode, SymbolicError> {
        if address == CHEATCODE_ADDRESS || address == SYMBOLIC_VM_COMPAT_ADDRESS {
            return Ok(SymCode::concrete(cx, vec![0]));
        }
        if self.destroyed_accounts.contains(&address) {
            return Ok(SymCode::empty(cx));
        }
        if let Some(code) = self.code_cache.get(&address) {
            return Ok(code.clone());
        }
        let account = executor
            .backend
            .basic_ref(address)
            .map_err(|err| SymbolicError::Backend(err.to_string()))?;
        if let Some(account) = account.as_ref()
            && (account.nonce != 0
                || !account.balance.is_zero()
                || account.code.as_ref().is_some_and(|code| !code.is_empty()))
        {
            Arc::make_mut(&mut self.state).existing_accounts.insert(address);
        }
        let bytecode = account.as_ref().and_then(|account| account.code.as_ref());
        let code = bytecode
            .map(|bytecode| SymCode::from_bytecode(cx, bytecode))
            .unwrap_or_else(|| SymCode::empty(cx));
        Arc::make_mut(&mut self.state).code_cache.insert(address, code.clone());
        Ok(code)
    }

    pub(crate) fn extcode_hash_for_address(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address: Address,
    ) -> Result<SymExpr, SymbolicError> {
        if self.account_exists(cx, executor, address)? {
            let code = self.extcode(cx, executor, address)?;
            let bytes = code.read_byte_exprs(cx, 0, code.len());
            Ok(keccak_word(cx, bytes))
        } else {
            Ok(SymExpr::zero(cx))
        }
    }

    pub(crate) fn extcode_size_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        if let Some(address) = self.resolve_address(&address_expr) {
            let len = self.extcode(cx, executor, address)?.len();
            return Ok(SymExpr::constant(cx, U256::from(len)));
        }

        let expr = address_expr;
        let representative = expr.representative_symbolic_address();
        let len = self.extcode(cx, executor, representative)?.len();
        let mut result = SymExpr::constant(cx, U256::from(len));
        for address in self.known_addresses(executor) {
            let len = self.extcode(cx, executor, address)?.len();
            let address = SymExpr::constant(cx, address_word(address));
            let condition = SymBoolExpr::eq(cx, expr.clone(), address);
            let len = SymExpr::constant(cx, U256::from(len));
            result = SymExpr::ite(cx, condition, len, result);
        }

        Ok(result)
    }

    pub(crate) fn extcode_hash_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        if let Some(address) = self.resolve_address(&address_expr) {
            return self.extcode_hash_for_address(cx, executor, address);
        }

        let expr = address_expr;
        let representative = expr.representative_symbolic_address();
        let mut result = self.extcode_hash_for_address(cx, executor, representative)?;
        for address in self.known_addresses(executor) {
            let hash = self.extcode_hash_for_address(cx, executor, address)?;
            let address = SymExpr::constant(cx, address_word(address));
            let condition = SymBoolExpr::eq(cx, expr.clone(), address);
            result = SymExpr::ite(cx, condition, hash, result);
        }

        Ok(result)
    }

    pub(crate) fn extcode_bytes_word(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        address_expr: SymExpr,
        offset: SymExpr,
        size: usize,
    ) -> Result<SymBytes, SymbolicError> {
        if let Some(address) = self.resolve_address(&address_expr) {
            return Ok(self.extcode(cx, executor, address)?.read_bytes_offset(cx, offset, size));
        }

        let expr = address_expr;
        let representative = expr.representative_symbolic_address();
        let mut result = self.extcode(cx, executor, representative)?.read_byte_exprs_offset(
            cx,
            offset.clone(),
            size,
        );
        for address in self.known_addresses(executor) {
            let bytes = self.extcode(cx, executor, address)?.read_byte_exprs_offset(
                cx,
                offset.clone(),
                size,
            );
            let address = SymExpr::constant(cx, address_word(address));
            let condition = SymBoolExpr::eq(cx, expr.clone(), address);
            for (idx, byte) in bytes.into_iter().enumerate() {
                result[idx] = SymExpr::ite(cx, condition.clone(), byte, result[idx].clone());
            }
        }

        Ok(SymBytes::exprs(cx, result))
    }

    pub(crate) fn symbolic_call_targets(
        &mut self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
    ) -> Result<Vec<Address>, SymbolicError> {
        let mut targets = Vec::new();
        for address in self.known_addresses(executor) {
            if is_precompile_for_spec(address, executor.spec_id) {
                continue;
            }
            if !self.extcode(cx, executor, address)?.is_empty() {
                targets.push(address);
            }
        }
        Ok(targets)
    }

    /// Returns the concrete accounts a symbolic address may alias, in address order.
    ///
    /// Includes accounts that exist only in the backend, such as contracts deployed in `setUp`,
    /// which the world caches only once touched. Cheatcode addresses are excluded.
    fn known_addresses(&self, executor: &ExecutorView<'_>) -> Vec<Address> {
        let mut addresses = self
            .code_cache
            .keys()
            .chain(self.balances.keys())
            .chain(&self.existing_accounts)
            .chain(&executor.account_addresses)
            .copied()
            .filter(|address| {
                *address != CHEATCODE_ADDRESS && *address != SYMBOLIC_VM_COMPAT_ADDRESS
            })
            .collect::<Vec<_>>();
        addresses.sort_unstable();
        addresses.dedup();
        addresses
    }
}

fn symbolic_storage_symbol(cx: &mut SymCx, address: Address, key: &SymExpr) -> Symbol {
    stable_symbol(
        cx,
        "storage",
        format!("{address:?}:{:?}", ExpressionDigests::identity([key])).as_bytes(),
    )
}

#[derive(Clone, Debug)]
pub(crate) struct SymbolicBlock {
    pub(crate) chain_id: SymExpr,
    pub(crate) coinbase: Address,
    pub(crate) timestamp: SymExpr,
    pub(crate) number: SymExpr,
    pub(crate) difficulty: SymExpr,
    pub(crate) gaslimit: SymExpr,
    pub(crate) basefee: SymExpr,
    pub(crate) blob_basefee: SymExpr,
    pub(crate) block_hashes: HashMap<U256, SymExpr>,
    pub(crate) blob_hashes: Vec<B256>,
}

impl SymbolicBlock {
    pub(crate) fn new(cx: &mut SymCx) -> Self {
        Self {
            chain_id: SymExpr::one(cx),
            coinbase: Address::ZERO,
            timestamp: SymExpr::zero(cx),
            number: SymExpr::zero(cx),
            difficulty: SymExpr::zero(cx),
            gaslimit: SymExpr::zero(cx),
            basefee: SymExpr::zero(cx),
            blob_basefee: SymExpr::zero(cx),
            block_hashes: HashMap::default(),
            blob_hashes: Vec::new(),
        }
    }

    pub(crate) fn from_executor(cx: &mut SymCx, executor: &ExecutorView<'_>) -> Self {
        let block = &executor.block;
        Self {
            chain_id: SymExpr::constant(cx, U256::from(executor.chain_id)),
            coinbase: block.coinbase,
            timestamp: SymExpr::constant(cx, block.timestamp),
            number: SymExpr::constant(cx, block.number),
            difficulty: SymExpr::constant(cx, block.difficulty),
            gaslimit: SymExpr::constant(cx, U256::from(block.gas_limit)),
            basefee: SymExpr::constant(cx, U256::from(block.basefee)),
            blob_basefee: SymExpr::constant(cx, U256::from(block.blob_basefee)),
            block_hashes: HashMap::default(),
            blob_hashes: executor.blob_hashes.clone(),
        }
    }

    pub(crate) fn set_block_hash(
        &mut self,
        block_number: U256,
        block_hash: SymExpr,
    ) -> Result<(), SymbolicError> {
        let current = self.number.as_const_or("symbolic vm.setBlockhash current number")?;
        if block_number < current && current - block_number <= U256::from(256) {
            self.block_hashes.insert(block_number, block_hash);
        }
        Ok(())
    }

    pub(crate) fn block_hash(
        &self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        block_number: U256,
    ) -> Result<SymExpr, SymbolicError> {
        let current = self.number.as_const_or("symbolic BLOCKHASH current number")?;
        if block_number >= current || current - block_number > U256::from(256) {
            return Ok(SymExpr::zero(cx));
        }
        if let Some(hash) = self.block_hashes.get(&block_number) {
            return Ok(hash.clone());
        }
        let Ok(block_number) = u64::try_from(block_number) else {
            return Ok(SymExpr::zero(cx));
        };
        let hash = executor
            .backend
            .block_hash_ref(block_number)
            .map_err(|err| SymbolicError::Backend(err.to_string()))?;
        Ok(SymExpr::constant(cx, U256::from_be_slice(hash.as_slice())))
    }

    pub(crate) fn block_hash_word(
        &self,
        cx: &mut SymCx,
        executor: &ExecutorView<'_>,
        block_number: SymExpr,
    ) -> Result<SymExpr, SymbolicError> {
        if let Some(block_number) = block_number.as_const() {
            return self.block_hash(cx, executor, block_number);
        }
        let current = self.number.as_const_or("symbolic BLOCKHASH current number")?;
        if current.is_zero() {
            return Ok(SymExpr::zero(cx));
        }

        let mut result = SymExpr::zero(cx);
        let max_distance =
            usize::try_from(current.min(U256::from(256))).expect("checked blockhash distance");
        for distance in (1..=max_distance).rev() {
            let candidate = current - U256::from(distance);
            let hash = self.block_hash(cx, executor, candidate)?;
            if hash.as_const().is_some_and(|hash| hash.is_zero()) {
                continue;
            }
            let candidate = SymExpr::constant(cx, candidate);
            let condition = SymBoolExpr::eq(cx, block_number.clone(), candidate);
            result = SymExpr::ite(cx, condition, hash, result);
        }

        Ok(result)
    }
}