foundry_evm_symbolic/
lib.rs

1//! Foundry's symbolic EVM executor.
2
3#![cfg_attr(not(test), warn(unused_crate_dependencies))]
4
5use alloy_dyn_abi::{DynSolType, DynSolValue, JsonAbiExt};
6use alloy_json_abi::Function;
7use alloy_primitives::{
8    Address, B256, Bytes, I256, U256, hex, keccak256,
9    map::{HashMap, HashSet, IndexSet},
10};
11use alloy_signer::SignerSync;
12use alloy_signer_local::{
13    PrivateKeySigner,
14    coins_bip39::{English, Wordlist},
15};
16use alloy_sol_types::SolCall;
17use base64::prelude::*;
18use foundry_cheatcodes_spec::{SymbolicVm, Vm};
19use foundry_config::{SymbolicConfig, SymbolicExplorationOrder, SymbolicStorageLayout};
20use foundry_evm::{
21    constants::{CALLER, CHEATCODE_ADDRESS, DEFAULT_CREATE2_DEPLOYER, HARDHAT_CONSOLE_ADDRESS},
22    core::{backend::DatabaseExt, evm::FoundryEvmNetwork},
23    executors::Executor,
24    revm::{
25        bytecode::{Bytecode, JumpTable, opcode},
26        context::{Block, Cfg, Transaction},
27        database::DatabaseRef,
28        precompile::{blake2, bn254, hash, identity, kzg_point_evaluation, modexp, secp256k1},
29        primitives::hardfork::SpecId,
30    },
31};
32use serde::{Deserialize, Serialize};
33use std::{
34    collections::VecDeque,
35    fmt::{self, Write as _},
36    io::Write,
37    ops::{ControlFlow, Deref, DerefMut},
38    path::{Path, PathBuf},
39    process::{Command, Stdio},
40    sync::{
41        Arc,
42        atomic::{AtomicBool, Ordering},
43        mpsc,
44    },
45    thread,
46    time::{Duration, Instant, SystemTime, UNIX_EPOCH},
47};
48use thiserror::Error;
49use tracing::{debug, trace, trace_span, warn};
50
51#[cfg(test)]
52use std::collections::BTreeMap;
53
54mod abi;
55mod consts;
56mod executor;
57mod runtime;
58
59pub use consts::BUILTIN_SYMBOLIC_SOLVERS;
60pub(crate) use consts::*;
61pub use runtime::{PortfolioDiagnostics, SymbolicBranchTarget, SymbolicError, SymbolicRunInput};
62
63#[derive(Clone, Copy, Debug, PartialEq, Eq)]
64enum SymbolicVmCheatcode {
65    CreateAddress,
66    CreateBool,
67    CreateBytes,
68    CreateBytesSized,
69    CreateBytesFixed(usize),
70    CreateCalldata,
71    CreateInt,
72    CreateIntBits(usize),
73    CreateString,
74    CreateStringSized,
75    CreateUint,
76    CreateUintBits(usize),
77    EnableSymbolicStorage,
78    SnapshotStorage,
79    SnapshotState,
80}
81
82impl SymbolicVmCheatcode {
83    fn from_selector(selector: [u8; 4]) -> Option<Self> {
84        match selector {
85            SymbolicVm::createAddressCall::SELECTOR => Some(Self::CreateAddress),
86            SymbolicVm::createBoolCall::SELECTOR => Some(Self::CreateBool),
87            SymbolicVm::createBytes_0Call::SELECTOR => Some(Self::CreateBytes),
88            SymbolicVm::createBytes_1Call::SELECTOR => Some(Self::CreateBytesSized),
89            SymbolicVm::createCalldataCall::SELECTOR => Some(Self::CreateCalldata),
90            SymbolicVm::createIntCall::SELECTOR => Some(Self::CreateInt),
91            SymbolicVm::createString_0Call::SELECTOR => Some(Self::CreateString),
92            SymbolicVm::createString_1Call::SELECTOR => Some(Self::CreateStringSized),
93            SymbolicVm::createUintCall::SELECTOR => Some(Self::CreateUint),
94            SymbolicVm::enableSymbolicStorageCall::SELECTOR
95            | Vm::setArbitraryStorage_0Call::SELECTOR => Some(Self::EnableSymbolicStorage),
96            SymbolicVm::snapshotStorageCall::SELECTOR => Some(Self::SnapshotStorage),
97            Vm::snapshotStateCall::SELECTOR => Some(Self::SnapshotState),
98            _ => {
99                for &(bits, candidate) in symbolic_create_uint_selectors() {
100                    if selector == candidate {
101                        return Some(Self::CreateUintBits(bits));
102                    }
103                }
104                for &(bits, candidate) in symbolic_create_int_selectors() {
105                    if selector == candidate {
106                        return Some(Self::CreateIntBits(bits));
107                    }
108                }
109                for &(bytes, candidate) in symbolic_create_bytes_selectors() {
110                    if selector == candidate {
111                        return Some(Self::CreateBytesFixed(bytes));
112                    }
113                }
114                None
115            }
116        }
117    }
118
119    const fn min_input_words(self) -> usize {
120        match self {
121            Self::CreateUint
122            | Self::CreateInt
123            | Self::CreateBytesSized
124            | Self::CreateStringSized
125            | Self::EnableSymbolicStorage
126            | Self::SnapshotStorage => 1,
127            Self::CreateAddress
128            | Self::CreateBool
129            | Self::CreateBytes
130            | Self::CreateBytesFixed(_)
131            | Self::CreateCalldata
132            | Self::CreateIntBits(_)
133            | Self::CreateString
134            | Self::CreateUintBits(_)
135            | Self::SnapshotState => 0,
136        }
137    }
138}
139
140/// Outcome of a symbolic test execution.
141///
142/// The forge runner treats `Safe` as a passing symbolic test, `Counterexample` as a
143/// candidate failure that must be replayed concretely, and `Incomplete` as a failing
144/// test because the symbolic engine could not prove the property with the supported
145/// semantics and configured resource limits.
146#[derive(Clone, Debug)]
147pub enum SymbolicRunResult {
148    /// All explored paths completed without a feasible failure.
149    Safe {
150        /// Execution counters collected during the run.
151        stats: SymbolicStats,
152        /// One concrete successful input, when requested by the caller.
153        success_input: Option<SymbolicConcreteInput>,
154    },
155    /// A feasible failure was found.
156    Counterexample {
157        /// ABI-typed argument values extracted from the solver model.
158        args: Vec<DynSolValue>,
159        /// ABI-encoded calldata for the failing invocation.
160        calldata: Bytes,
161        /// Execution counters collected before the counterexample was returned.
162        stats: SymbolicStats,
163    },
164    /// Execution was intentionally stopped because V1 semantics were insufficient.
165    Incomplete {
166        /// Category describing why symbolic execution stopped before proving the test.
167        kind: SymbolicStopReason,
168        /// Human-readable explanation of the unsupported construct or exhausted limit.
169        reason: String,
170        /// Execution counters collected before execution stopped.
171        stats: SymbolicStats,
172    },
173}
174
175/// One concrete symbolic input materialized from a solver model.
176#[derive(Clone, Debug)]
177pub struct SymbolicConcreteInput {
178    /// ABI-typed argument values extracted from the solver model.
179    pub args: Vec<DynSolValue>,
180    /// ABI-encoded calldata for replay.
181    pub calldata: Bytes,
182}
183
184/// Result of best-effort symbolic exploration toward one branch target.
185#[derive(Debug)]
186pub struct SymbolicBranchTargetSearchResult {
187    /// Concrete inputs whose completed root path reached the requested branch outcome.
188    pub candidates: Vec<SymbolicConcreteInput>,
189    /// Underlying execution result, retained so callers can report incomplete exploration.
190    pub execution: SymbolicRunResult,
191}
192
193/// A concrete invariant target selected from Foundry's invariant discovery.
194#[derive(Clone, Debug)]
195pub struct SymbolicInvariantTarget {
196    /// Address that receives the sequence call.
197    pub address: Address,
198    /// Human-readable contract identifier used in counterexample rendering.
199    pub contract_name: Option<String>,
200    /// ABI function invoked with symbolic arguments.
201    pub function: Function,
202}
203
204/// Input for best-effort invariant candidate search after one symbolic handler call.
205pub struct SymbolicInvariantCandidateInput<'a, FEN: FoundryEvmNetwork> {
206    /// Concrete Foundry executor containing the replayed invariant frontier prefix.
207    pub executor: &'a Executor<FEN>,
208    /// Address of the deployed invariant test contract.
209    pub invariant_address: Address,
210    /// Invariant functions checked independently after the handler call.
211    pub invariants: &'a [&'a Function],
212    /// Optional campaign hook checked from the unchanged post-handler state.
213    pub after_invariant: Option<&'a Function>,
214    /// Concrete handler target selected from the captured frontier.
215    pub target: &'a SymbolicInvariantTarget,
216    /// Sender of the captured handler call.
217    pub handler_sender: Address,
218    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
219    pub ffi_enabled: bool,
220}
221
222/// One unconfirmed symbolic input produced by invariant candidate search.
223#[derive(Clone, Debug)]
224pub struct SymbolicInvariantCandidate {
225    /// Index within [`SymbolicInvariantCandidateInput::invariants`] predicted to fail.
226    pub invariant_idx: usize,
227    /// Concrete handler call extracted from the solver model.
228    pub step: SymbolicInvariantStep,
229    /// Concrete setup-storage values needed to replay the candidate.
230    pub storage: Vec<SymbolicStorageAssignment>,
231}
232
233/// An execution or solver limitation encountered during best-effort candidate search.
234#[derive(Clone, Debug, PartialEq, Eq)]
235pub struct SymbolicInvariantSearchLimitation {
236    /// Category describing why part of the search could not complete.
237    pub kind: SymbolicStopReason,
238    /// Human-readable description of the limitation.
239    pub reason: String,
240}
241
242impl From<SymbolicError> for SymbolicInvariantSearchLimitation {
243    fn from(error: SymbolicError) -> Self {
244        Self { kind: error.stop_reason(), reason: error.to_string() }
245    }
246}
247
248/// Result of best-effort invariant candidate search after one symbolic handler call.
249#[derive(Clone, Debug)]
250pub struct SymbolicInvariantCandidateSearchResult {
251    /// Unconfirmed candidates that must be replayed concretely by the caller.
252    pub candidates: Vec<SymbolicInvariantCandidate>,
253    /// First encountered search limitation, if any. `None` is not a proof of safety.
254    pub limitation: Option<SymbolicInvariantSearchLimitation>,
255}
256
257/// Input for bounded symbolic invariant execution.
258pub struct SymbolicInvariantRunInput<'a, FEN: FoundryEvmNetwork> {
259    /// Concrete Foundry executor used as the source of deployed bytecode and backend state.
260    pub executor: &'a Executor<FEN>,
261    /// Address of the deployed invariant test contract.
262    pub invariant_address: Address,
263    /// Default sender used when invariant targeting does not configure senders.
264    pub sender: Address,
265    /// Invariant function checked after each symbolic sequence step.
266    pub invariant: &'a Function,
267    /// Optional `afterInvariant` hook to execute after a passing invariant check.
268    pub after_invariant: Option<&'a Function>,
269    /// Concrete target/selector set discovered by Foundry invariant targeting.
270    pub targets: Vec<SymbolicInvariantTarget>,
271    /// Concrete sender set discovered by Foundry invariant targeting.
272    pub senders: Vec<Address>,
273    /// Sender addresses excluded by Foundry invariant targeting.
274    pub excluded_senders: Vec<Address>,
275    /// Maximum number of sequence calls to execute.
276    pub depth: usize,
277    /// Concrete invariant check interval. `0` means only check at sequence end.
278    pub check_interval: u32,
279    /// Whether ordinary target-call reverts should be reported as failures.
280    pub fail_on_revert: bool,
281    /// Whether symbolic `vm.ffi` calls are allowed to execute subprocesses.
282    pub ffi_enabled: bool,
283}
284
285/// One concrete storage value required to replay a symbolic invariant candidate.
286#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
287pub struct SymbolicStorageAssignment {
288    /// Account whose storage slot should be initialized.
289    pub address: Address,
290    /// Concrete storage slot.
291    pub slot: U256,
292    /// Concrete value extracted from the solver model.
293    pub value: U256,
294}
295
296/// Outcome of bounded symbolic invariant execution.
297#[derive(Clone, Debug)]
298pub enum SymbolicInvariantRunResult {
299    /// No feasible invariant failure was found within the configured sequence depth.
300    Safe(SymbolicStats),
301    /// A feasible invariant or handler failure was found.
302    Counterexample {
303        /// Which part of the invariant run produced the failure.
304        kind: SymbolicInvariantCounterexampleKind,
305        /// Concrete sequence extracted from the solver model.
306        sequence: Vec<SymbolicInvariantStep>,
307        /// Concrete setup-storage values needed for replay.
308        storage: Vec<SymbolicStorageAssignment>,
309        /// Execution counters collected before the counterexample was returned.
310        stats: SymbolicStats,
311    },
312    /// Execution stopped before proving the invariant.
313    Incomplete {
314        /// Category describing why symbolic execution stopped.
315        kind: SymbolicStopReason,
316        /// Human-readable explanation of the unsupported construct or exhausted limit.
317        reason: String,
318        /// Execution counters collected before execution stopped.
319        stats: SymbolicStats,
320    },
321}
322
323/// Part of a symbolic invariant run that produced a replayable counterexample.
324#[derive(Clone, Copy, Debug, PartialEq, Eq)]
325pub enum SymbolicInvariantCounterexampleKind {
326    /// An `invariant_*` or `afterInvariant` check failed.
327    Predicate,
328    /// A fuzzed target/handler call failed with an assertion.
329    Handler,
330}
331
332/// One concrete step in a symbolic invariant counterexample sequence.
333#[derive(Clone, Debug)]
334pub struct SymbolicInvariantStep {
335    /// Sender used for the call.
336    pub sender: Address,
337    /// Target address called by the sequence step.
338    pub address: Address,
339    /// Human-readable contract identifier, when known.
340    pub contract_name: Option<String>,
341    /// ABI function name.
342    pub function_name: String,
343    /// ABI function signature.
344    pub signature: String,
345    /// ABI-typed arguments extracted from the solver model.
346    pub args: Vec<DynSolValue>,
347    /// ABI-encoded calldata for replay.
348    pub calldata: Bytes,
349}
350
351/// High-level reason a symbolic run stopped without a proof or replayed counterexample.
352#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
353pub enum SymbolicStopReason {
354    /// The executor reached a supported-but-incomplete semantic boundary.
355    Stuck,
356    /// Every explored execution path ended in an ordinary revert.
357    RevertAll,
358    /// The solver timed out or returned `unknown`.
359    Timeout,
360    /// An internal engine, backend, or solver process error occurred.
361    Error,
362}
363
364/// Symbolic execution counters.
365#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Serialize, Deserialize)]
366pub struct SymbolicStats {
367    /// Number of explored symbolic paths.
368    pub paths: usize,
369    /// Number of normalized solver queries issued during the run.
370    pub solver_queries: usize,
371    /// Number of queries sent to the SMT backend after local fast paths.
372    #[serde(default)]
373    pub smt_queries: usize,
374    /// Number of satisfiability checks requested by the executor.
375    #[serde(default)]
376    pub sat_queries: usize,
377    /// Number of concrete model requests requested by the executor.
378    #[serde(default)]
379    pub model_queries: usize,
380    /// Number of satisfiability checks served from the normalized cache.
381    #[serde(default)]
382    pub sat_cache_hits: usize,
383    /// Number of model requests served from the normalized model cache.
384    #[serde(default)]
385    pub model_cache_hits: usize,
386    /// Number of satisfiable witnesses produced by local hard-arithmetic search.
387    #[serde(default)]
388    pub heuristic_witnesses: usize,
389    /// Wall-clock time spent waiting on backend solver subprocesses, in milliseconds.
390    #[serde(default)]
391    pub solver_time_ms: u64,
392    /// Total SMT-LIB input bytes sent to backend solver subprocesses.
393    #[serde(default)]
394    pub smt_input_bytes: u64,
395    /// Largest single SMT-LIB query input sent to a backend solver subprocess, in bytes.
396    #[serde(default)]
397    pub smt_max_query_bytes: u64,
398    /// Wall-clock time spent building SMT-LIB query strings, in milliseconds.
399    #[serde(default)]
400    pub smt_build_time_ms: u64,
401    /// Longest single backend solver subprocess query, in milliseconds.
402    #[serde(default)]
403    pub smt_max_query_time_ms: u64,
404}
405
406/// SMT-LIB-backed symbolic executor.
407///
408/// This executor is intentionally separate from the concrete revm executor used by
409/// Foundry. It consumes bytecode and state from an existing [`Executor`], explores
410/// symbolic branches, and returns either a proof result, a counterexample candidate,
411/// or an incomplete result.
412pub struct SymbolicExecutor {
413    config: SymbolicConfig,
414    cx: runtime::SymCx,
415    solver: runtime::SmtLibSubprocessSolver,
416    deferred_incomplete: Option<DeferredIncomplete>,
417    deadline: Option<Instant>,
418    nested_deferred_mode: DeferredPathMode,
419    stateless_retry_safe: bool,
420}
421
422#[derive(Clone, Copy, Debug, PartialEq, Eq)]
423enum DeferredPathMode {
424    Skip,
425    Yield,
426    Drain,
427}
428
429#[derive(Clone, Copy, Debug, PartialEq, Eq)]
430enum DeferredIncomplete {
431    Unsupported(&'static str),
432    SolverUnknown,
433    HardArithmetic,
434}
435
436fn symbolic_create_uint_selectors() -> &'static [(usize, [u8; 4]); 32] {
437    static SELECTORS: [(usize, [u8; 4]); 32] = [
438        (8, SymbolicVm::createUint8Call::SELECTOR),
439        (16, SymbolicVm::createUint16Call::SELECTOR),
440        (24, SymbolicVm::createUint24Call::SELECTOR),
441        (32, SymbolicVm::createUint32Call::SELECTOR),
442        (40, SymbolicVm::createUint40Call::SELECTOR),
443        (48, SymbolicVm::createUint48Call::SELECTOR),
444        (56, SymbolicVm::createUint56Call::SELECTOR),
445        (64, SymbolicVm::createUint64Call::SELECTOR),
446        (72, SymbolicVm::createUint72Call::SELECTOR),
447        (80, SymbolicVm::createUint80Call::SELECTOR),
448        (88, SymbolicVm::createUint88Call::SELECTOR),
449        (96, SymbolicVm::createUint96Call::SELECTOR),
450        (104, SymbolicVm::createUint104Call::SELECTOR),
451        (112, SymbolicVm::createUint112Call::SELECTOR),
452        (120, SymbolicVm::createUint120Call::SELECTOR),
453        (128, SymbolicVm::createUint128Call::SELECTOR),
454        (136, SymbolicVm::createUint136Call::SELECTOR),
455        (144, SymbolicVm::createUint144Call::SELECTOR),
456        (152, SymbolicVm::createUint152Call::SELECTOR),
457        (160, SymbolicVm::createUint160Call::SELECTOR),
458        (168, SymbolicVm::createUint168Call::SELECTOR),
459        (176, SymbolicVm::createUint176Call::SELECTOR),
460        (184, SymbolicVm::createUint184Call::SELECTOR),
461        (192, SymbolicVm::createUint192Call::SELECTOR),
462        (200, SymbolicVm::createUint200Call::SELECTOR),
463        (208, SymbolicVm::createUint208Call::SELECTOR),
464        (216, SymbolicVm::createUint216Call::SELECTOR),
465        (224, SymbolicVm::createUint224Call::SELECTOR),
466        (232, SymbolicVm::createUint232Call::SELECTOR),
467        (240, SymbolicVm::createUint240Call::SELECTOR),
468        (248, SymbolicVm::createUint248Call::SELECTOR),
469        (256, SymbolicVm::createUint256Call::SELECTOR),
470    ];
471    &SELECTORS
472}
473
474fn symbolic_create_int_selectors() -> &'static [(usize, [u8; 4]); 32] {
475    static SELECTORS: [(usize, [u8; 4]); 32] = [
476        (8, SymbolicVm::createInt8Call::SELECTOR),
477        (16, SymbolicVm::createInt16Call::SELECTOR),
478        (24, SymbolicVm::createInt24Call::SELECTOR),
479        (32, SymbolicVm::createInt32Call::SELECTOR),
480        (40, SymbolicVm::createInt40Call::SELECTOR),
481        (48, SymbolicVm::createInt48Call::SELECTOR),
482        (56, SymbolicVm::createInt56Call::SELECTOR),
483        (64, SymbolicVm::createInt64Call::SELECTOR),
484        (72, SymbolicVm::createInt72Call::SELECTOR),
485        (80, SymbolicVm::createInt80Call::SELECTOR),
486        (88, SymbolicVm::createInt88Call::SELECTOR),
487        (96, SymbolicVm::createInt96Call::SELECTOR),
488        (104, SymbolicVm::createInt104Call::SELECTOR),
489        (112, SymbolicVm::createInt112Call::SELECTOR),
490        (120, SymbolicVm::createInt120Call::SELECTOR),
491        (128, SymbolicVm::createInt128Call::SELECTOR),
492        (136, SymbolicVm::createInt136Call::SELECTOR),
493        (144, SymbolicVm::createInt144Call::SELECTOR),
494        (152, SymbolicVm::createInt152Call::SELECTOR),
495        (160, SymbolicVm::createInt160Call::SELECTOR),
496        (168, SymbolicVm::createInt168Call::SELECTOR),
497        (176, SymbolicVm::createInt176Call::SELECTOR),
498        (184, SymbolicVm::createInt184Call::SELECTOR),
499        (192, SymbolicVm::createInt192Call::SELECTOR),
500        (200, SymbolicVm::createInt200Call::SELECTOR),
501        (208, SymbolicVm::createInt208Call::SELECTOR),
502        (216, SymbolicVm::createInt216Call::SELECTOR),
503        (224, SymbolicVm::createInt224Call::SELECTOR),
504        (232, SymbolicVm::createInt232Call::SELECTOR),
505        (240, SymbolicVm::createInt240Call::SELECTOR),
506        (248, SymbolicVm::createInt248Call::SELECTOR),
507        (256, SymbolicVm::createInt256Call::SELECTOR),
508    ];
509    &SELECTORS
510}
511
512fn symbolic_create_bytes_selectors() -> &'static [(usize, [u8; 4]); 32] {
513    static SELECTORS: [(usize, [u8; 4]); 32] = [
514        (1, SymbolicVm::createBytes1Call::SELECTOR),
515        (2, SymbolicVm::createBytes2Call::SELECTOR),
516        (3, SymbolicVm::createBytes3Call::SELECTOR),
517        (4, SymbolicVm::createBytes4Call::SELECTOR),
518        (5, SymbolicVm::createBytes5Call::SELECTOR),
519        (6, SymbolicVm::createBytes6Call::SELECTOR),
520        (7, SymbolicVm::createBytes7Call::SELECTOR),
521        (8, SymbolicVm::createBytes8Call::SELECTOR),
522        (9, SymbolicVm::createBytes9Call::SELECTOR),
523        (10, SymbolicVm::createBytes10Call::SELECTOR),
524        (11, SymbolicVm::createBytes11Call::SELECTOR),
525        (12, SymbolicVm::createBytes12Call::SELECTOR),
526        (13, SymbolicVm::createBytes13Call::SELECTOR),
527        (14, SymbolicVm::createBytes14Call::SELECTOR),
528        (15, SymbolicVm::createBytes15Call::SELECTOR),
529        (16, SymbolicVm::createBytes16Call::SELECTOR),
530        (17, SymbolicVm::createBytes17Call::SELECTOR),
531        (18, SymbolicVm::createBytes18Call::SELECTOR),
532        (19, SymbolicVm::createBytes19Call::SELECTOR),
533        (20, SymbolicVm::createBytes20Call::SELECTOR),
534        (21, SymbolicVm::createBytes21Call::SELECTOR),
535        (22, SymbolicVm::createBytes22Call::SELECTOR),
536        (23, SymbolicVm::createBytes23Call::SELECTOR),
537        (24, SymbolicVm::createBytes24Call::SELECTOR),
538        (25, SymbolicVm::createBytes25Call::SELECTOR),
539        (26, SymbolicVm::createBytes26Call::SELECTOR),
540        (27, SymbolicVm::createBytes27Call::SELECTOR),
541        (28, SymbolicVm::createBytes28Call::SELECTOR),
542        (29, SymbolicVm::createBytes29Call::SELECTOR),
543        (30, SymbolicVm::createBytes30Call::SELECTOR),
544        (31, SymbolicVm::createBytes31Call::SELECTOR),
545        (32, SymbolicVm::createBytes32Call::SELECTOR),
546    ];
547    &SELECTORS
548}
549
550/// Returns whether `solver` is one of Foundry's semantic symbolic solver names.
551pub fn symbolic_solver_is_builtin(solver: &str) -> bool {
552    BUILTIN_SYMBOLIC_SOLVERS.contains(&solver)
553}
554
555/// Returns a warning when a configured symbolic solver portfolio has unavailable entries.
556pub fn symbolic_solver_portfolio_availability_warning(config: &SymbolicConfig) -> Option<String> {
557    runtime::solver_portfolio_availability_warning(config)
558}
559
560#[cfg(test)]
561mod tests;
foundry_evm_symbolic/lib.rs

foundry_evm_symbolic/
lib.rs
