foundry_evm_symbolic/runtime/
precompiles.rs

1use super::*;
2
3/// Returns whether `is_known_cheatcode` holds.
4pub(crate) fn is_known_cheatcode(address: Address) -> bool {
5    address == CHEATCODE_ADDRESS || address == SYMBOLIC_VM_COMPAT_ADDRESS
6}
7
8/// Returns whether `is_console` holds.
9pub(crate) fn is_console(address: Address) -> bool {
10    address == HARDHAT_CONSOLE_ADDRESS
11}
12
13/// Returns the `precompile_number` precompile helper result.
14pub(crate) fn precompile_number(address: Address) -> Option<u8> {
15    let bytes = address.as_slice();
16    if bytes[..PRECOMPILE_ADDRESS_LEADING_ZEROS].iter().any(|byte| *byte != 0) {
17        return None;
18    }
19    match bytes[PRECOMPILE_ADDRESS_LEADING_ZEROS] {
20        1..=10 => Some(bytes[PRECOMPILE_ADDRESS_LEADING_ZEROS]),
21        _ => None,
22    }
23}
24
25/// Returns the `precompile_address` precompile helper result.
26pub(crate) fn precompile_address(number: u8) -> Address {
27    let mut bytes = [0u8; 20];
28    bytes[PRECOMPILE_ADDRESS_LEADING_ZEROS] = number;
29    Address::from(bytes)
30}
31
32/// Returns whether `is_supported_precompile` holds.
33pub(crate) fn is_supported_precompile(address: Address) -> bool {
34    precompile_number(address).is_some()
35}
36
37/// Computes the `execute_precompile` precompile helper result.
38pub(crate) fn execute_precompile(
39    address: Address,
40    input: &[u8],
41) -> Result<Option<SymReturnData>, SymbolicError> {
42    let output = match precompile_number(address) {
43        Some(1) => secp256k1::ec_recover_run(input, u64::MAX),
44        Some(2) => hash::sha256_run(input, u64::MAX),
45        Some(3) => hash::ripemd160_run(input, u64::MAX),
46        Some(4) => identity::identity_run(input, u64::MAX),
47        Some(5) => modexp::berlin_run(input, u64::MAX),
48        Some(6) => bn254::run_add(input, bn254::add::ISTANBUL_ADD_GAS_COST, u64::MAX),
49        Some(7) => bn254::run_mul(input, bn254::mul::ISTANBUL_MUL_GAS_COST, u64::MAX),
50        Some(8) => bn254::run_pair(
51            input,
52            bn254::pair::ISTANBUL_PAIR_PER_POINT,
53            bn254::pair::ISTANBUL_PAIR_BASE,
54            u64::MAX,
55        ),
56        Some(9) => blake2::run(input, u64::MAX),
57        Some(10) => {
58            return Err(SymbolicError::Unsupported("KZG point-evaluation precompile not modeled"));
59        }
60        _ => return Err(SymbolicError::Unsupported("unsupported precompile")),
61    };
62
63    match output {
64        Ok(output) => Ok(Some(SymReturnData::from_concrete_bytes(output.bytes.to_vec()))),
65        Err(_) => Ok(None),
66    }
67}
68
69/// Computes the `execute_symbolic_precompile` precompile helper result.
70pub(crate) fn execute_symbolic_precompile(
71    address: Address,
72    input: Vec<SymWord>,
73    input_len: SymWord,
74) -> Result<Option<SymReturnData>, SymbolicError> {
75    if input.iter().all(|byte| matches!(byte, SymWord::Concrete(_)))
76        && let SymWord::Concrete(input_len) = input_len
77        && input_len <= U256::from(input.len())
78    {
79        let input_len = input_len.to::<usize>();
80        let input = concrete_bytes(&input[..input_len], "symbolic precompile input")?;
81        return execute_precompile(address, &input);
82    }
83
84    match precompile_number(address) {
85        Some(1) => {
86            let word = symbolic_hash_word_with_len("ecrecover", input, input_len);
87            let mut bytes = vec![SymWord::zero(); 12];
88            bytes.extend((12..32).map(|idx| byte_word(U256::from(idx), word.clone())));
89            Ok(Some(SymReturnData::from_symbolic_bytes(bytes)))
90        }
91        Some(2) => Ok(Some(SymReturnData::from_symbolic_bytes(word_bytes(
92            symbolic_hash_word_with_len("sha256", input, input_len),
93        )))),
94        Some(3) => {
95            let word = symbolic_hash_word_with_len("ripemd160", input, input_len);
96            let mut bytes = vec![SymWord::zero(); 12];
97            bytes.extend((12..32).map(|idx| byte_word(U256::from(idx), word.clone())));
98            Ok(Some(SymReturnData::from_symbolic_bytes(bytes)))
99        }
100        Some(4) => Ok(Some(SymReturnData::from_symbolic_bytes_with_len(input, input_len))),
101        Some(5) => symbolic_modexp_precompile(input, input_len),
102        Some(6) => {
103            let input_len = input_len.into_usize("symbolic precompile input")?;
104            if input_len > input.len() {
105                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
106            }
107            if input_has_symbolic_bytes(&input, input_len) {
108                return Err(SymbolicError::Unsupported(
109                    "symbolic bn254 precompile validity not modeled",
110                ));
111            }
112            Ok(Some(symbolic_fixed_len_precompile_output("bn254_add", input, input_len, 64)))
113        }
114        Some(7) => {
115            let input_len = input_len.into_usize("symbolic precompile input")?;
116            if input_len > input.len() {
117                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
118            }
119            if input_has_symbolic_bytes(&input, input_len) {
120                return Err(SymbolicError::Unsupported(
121                    "symbolic bn254 precompile validity not modeled",
122                ));
123            }
124            Ok(Some(symbolic_fixed_len_precompile_output("bn254_mul", input, input_len, 64)))
125        }
126        Some(8) => {
127            let input_len = input_len.into_usize("symbolic precompile input")?;
128            if input_len % 192 != 0 {
129                return Ok(None);
130            }
131            if input_len > input.len() {
132                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
133            }
134            if input_has_symbolic_bytes(&input, input_len) {
135                return Err(SymbolicError::Unsupported(
136                    "symbolic bn254 precompile validity not modeled",
137                ));
138            }
139            Ok(Some(symbolic_fixed_len_precompile_output("bn254_pairing", input, input_len, 32)))
140        }
141        Some(9) => {
142            let input_len = input_len.into_usize("symbolic precompile input")?;
143            if input_len != 213 {
144                return Ok(None);
145            }
146            if input_len > input.len() {
147                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
148            }
149            match input.get(212) {
150                Some(SymWord::Concrete(flag)) if flag.is_zero() || *flag == U256::from(1) => {}
151                Some(SymWord::Concrete(_)) => return Ok(None),
152                Some(SymWord::Expr(_)) => {
153                    return Err(SymbolicError::Unsupported(
154                        "symbolic blake2f precompile final flag not modeled",
155                    ));
156                }
157                None => {
158                    return Err(SymbolicError::Unsupported(
159                        "out-of-bounds symbolic precompile input",
160                    ));
161                }
162            }
163            Ok(Some(symbolic_fixed_len_precompile_output("blake2f", input, input_len, 64)))
164        }
165        Some(10) => Err(SymbolicError::Unsupported("KZG point-evaluation precompile not modeled")),
166        _ => {
167            let input_len = input_len.into_usize("symbolic precompile input")?;
168            let input = concrete_bytes(
169                input
170                    .get(..input_len)
171                    .ok_or(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"))?,
172                "symbolic precompile input",
173            )?;
174            execute_precompile(address, &input)
175        }
176    }
177}
178
179fn input_has_symbolic_bytes(input: &[SymWord], input_len: usize) -> bool {
180    input.iter().take(input_len).any(|byte| matches!(byte, SymWord::Expr(_)))
181}
182
183/// Returns the `symbolic_modexp_precompile` precompile helper result.
184pub(crate) fn symbolic_modexp_precompile(
185    input: Vec<SymWord>,
186    input_len: SymWord,
187) -> Result<Option<SymReturnData>, SymbolicError> {
188    let input_len = input_len.into_usize("symbolic precompile input")?;
189    if input_len > input.len() {
190        return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
191    }
192
193    let modulus_len = concrete_precompile_word_at(&input, 64)?;
194    let modulus_len = u256_to_usize(modulus_len)
195        .ok_or(SymbolicError::Unsupported("symbolic modexp output length"))?;
196    if modulus_len > 4096 {
197        return Err(SymbolicError::Unsupported("symbolic modexp output length"));
198    }
199    Ok(Some(symbolic_fixed_len_precompile_output("modexp", input, input_len, modulus_len)))
200}
201
202/// Returns the `concrete_precompile_word_at` precompile helper result.
203pub(crate) fn concrete_precompile_word_at(
204    input: &[SymWord],
205    offset: usize,
206) -> Result<U256, SymbolicError> {
207    let mut bytes = [0u8; 32];
208    for (idx, byte) in bytes.iter_mut().enumerate() {
209        *byte = match input.get(offset + idx) {
210            Some(SymWord::Concrete(byte)) => byte.to::<u8>(),
211            Some(_) => return Err(SymbolicError::Unsupported("symbolic precompile length header")),
212            None => 0,
213        };
214    }
215    Ok(U256::from_be_bytes(bytes))
216}
217
218/// Returns the `symbolic_fixed_len_precompile_output` precompile helper result.
219pub(crate) fn symbolic_fixed_len_precompile_output(
220    algorithm: &'static str,
221    input: Vec<SymWord>,
222    input_len: usize,
223    output_len: usize,
224) -> SymReturnData {
225    let input_len_word = SymWord::Concrete(U256::from(input_len));
226    let mut bytes = Vec::with_capacity(output_len);
227    for chunk in 0..output_len.div_ceil(32) {
228        let mut chunk_input = Vec::with_capacity(input.len() + 1);
229        chunk_input.push(SymWord::Concrete(U256::from(chunk)));
230        chunk_input.extend(input.iter().cloned());
231        bytes.extend(word_bytes(symbolic_hash_word_with_len(
232            algorithm,
233            chunk_input,
234            input_len_word.clone(),
235        )));
236    }
237    bytes.truncate(output_len);
238    SymReturnData::from_symbolic_bytes(bytes)
239}
foundry_evm_symbolic/runtime/precompiles.rs

foundry_evm_symbolic/runtime/
precompiles.rs
