foundry_evm_symbolic/
consts.rs

1use alloy_primitives::{Address, U256, address};
2use std::time::Duration;
3
4// HD wallet key derivation
5pub(crate) const DEFAULT_DERIVATION_PATH_PREFIX: &str = "m/44'/60'/0'/0/";
6pub(crate) const MAX_REMEMBER_KEYS: u32 = 64;
7pub(crate) const SYMBOLIC_VM_COMPAT_ADDRESS: Address =
8    address!("0xF3993A62377BCd56AE39D773740A5390411E8BC9");
9
10// EVM execution limits
11pub(crate) const EVM_STACK_LIMIT: usize = 1024;
12pub(crate) const CALL_VALUE_STIPEND: u64 = 2300;
13
14// Symbolic exponentiation limits
15pub(crate) const SYMBOLIC_EXP_CONCRETE_EXPONENT_LIMIT: u64 = 32;
16pub(crate) const CONCRETE_BASE_SYMBOLIC_EXPONENT_LIMIT: u64 = 256;
17
18// Revert selectors and assertion constants
19pub(crate) const PANIC_SELECTOR: [u8; 4] = [0x4e, 0x48, 0x7b, 0x71];
20pub(crate) const ERROR_SELECTOR: [u8; 4] = [0x08, 0xc3, 0x79, 0xa0];
21pub(crate) const ASSERT_PANIC_CODE: U256 = U256::from_limbs([1, 0, 0, 0]);
22pub(crate) const ASSERTION_FAILED_PREFIX: &str = "assertion failed";
23
24// ABI encoding lengths
25pub(crate) const ABI_SELECTOR_PLUS_WORD_LEN: usize = 36; // selector (4) + one ABI word (32)
26pub(crate) const ERROR_DATA_MIN_LEN: usize = 68; // selector (4) + offset (32) + length (32)
27
28// Precompile address layout
29pub(crate) const PRECOMPILE_ADDRESS_LEADING_ZEROS: usize = 19;
30
31// Solver subprocess supervision.
32pub(crate) const SOLVER_CANCEL_CHECK_INTERVAL: Duration = Duration::from_millis(50);
33
34// Portfolio scheduler launch delays.
35pub(crate) const SECOND_PORTFOLIO_SOLVER_DELAY: Duration = Duration::from_millis(100);
36pub(crate) const RESCUE_PORTFOLIO_SOLVER_DELAY: Duration = Duration::from_millis(500);
37
38// Portfolio scheduler tuning
39pub(crate) const PORTFOLIO_SCHEDULER_HISTORY: usize = 8;
40pub(crate) const PORTFOLIO_SCHEDULER_MIN_RECENCY_WEIGHT: i64 = 1;
41pub(crate) const PORTFOLIO_SCHEDULER_SPEED_BONUS_CAP_MS: u128 = 100;
42pub(crate) const PORTFOLIO_SCHEDULER_MAX_SPEED_BONUS: i64 = 100;
43
44// Solver query cache limits
45pub(crate) const SYMBOLIC_SOLVER_SAT_CACHE_MAX_ENTRIES: usize = 4096;
46pub(crate) const SYMBOLIC_SOLVER_MODEL_CACHE_MAX_ENTRIES: usize = 512;
47
48// Hard arithmetic witness search limits
49pub(crate) const HARD_ARITH_FALLBACK_MAX_VARS: usize = 4;
50pub(crate) const HARD_ARITH_FALLBACK_MAX_CANDIDATES_PER_VAR: usize = 24;
51pub(crate) const HARD_ARITH_FALLBACK_MAX_ASSIGNMENTS: usize = 50_000;
52
53/// Symbolic solver names with built-in command-line mappings.
54pub const BUILTIN_SYMBOLIC_SOLVERS: &[&str] =
55    &["z3", "yices", "cvc5", "cvc5-int", "bitwuzla", "bitwuzla-abs"];
foundry_evm_symbolic/consts.rs

foundry_evm_symbolic/
consts.rs
