foundry_evm_symbolic/runtime/
precompiles.rs

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

foundry_evm_symbolic/runtime/
precompiles.rs
