foundry_evm_symbolic/runtime/
precompiles.rs

1use super::*;
2
3pub(crate) fn precompile_number(address: Address) -> Option<u8> {
4    let bytes = address.as_slice();
5    if bytes[..PRECOMPILE_ADDRESS_LEADING_ZEROS].iter().any(|byte| *byte != 0) {
6        return None;
7    }
8    match bytes[PRECOMPILE_ADDRESS_LEADING_ZEROS] {
9        1..=10 => Some(bytes[PRECOMPILE_ADDRESS_LEADING_ZEROS]),
10        _ => None,
11    }
12}
13
14pub(crate) fn precompile_number_for_spec(address: Address, spec_id: SpecId) -> Option<u8> {
15    match precompile_number(address)? {
16        5..=8 if spec_id < SpecId::BYZANTIUM => None,
17        9 if spec_id < SpecId::ISTANBUL => None,
18        10 if spec_id < SpecId::CANCUN => None,
19        number => Some(number),
20    }
21}
22
23/// Returns the canonical precompiles active under `spec_id`.
24pub(crate) fn active_precompiles(spec_id: SpecId) -> &'static Precompiles {
25    Precompiles::new(PrecompileSpecId::from_spec_id(spec_id))
26}
27
28/// Returns whether `address` is a canonical precompile active under `spec_id`.
29pub(crate) fn is_precompile_for_spec(address: Address, spec_id: SpecId) -> bool {
30    active_precompiles(spec_id).contains(&address)
31}
32
33/// Executes a canonical precompile on concrete input with effectively unlimited gas.
34///
35/// Returns `None` when the precompile fails.
36pub(crate) fn execute_precompile(
37    cx: &mut SymCx,
38    address: Address,
39    input: &[u8],
40    spec_id: SpecId,
41) -> Result<Option<SymReturnData>, SymbolicError> {
42    let Some(precompile) = active_precompiles(spec_id).get(&address) else {
43        return Err(SymbolicError::Unsupported("unsupported precompile"));
44    };
45    match precompile.execute(input, u64::MAX, 0) {
46        Ok(output) if output.is_success() => {
47            Ok(Some(SymReturnData::from_concrete_bytes(cx, output.bytes.to_vec())))
48        }
49        _ => Ok(None),
50    }
51}
52
53pub(crate) fn execute_symbolic_precompile(
54    cx: &mut SymCx,
55    address: Address,
56    input: SymBytes,
57    input_len: SymExpr,
58    spec_id: SpecId,
59) -> Result<Option<SymReturnData>, SymbolicError> {
60    if let Some(input_len) = input_len.as_const()
61        && let Ok(input_len) = usize::try_from(input_len)
62        && input_len <= input.len()
63        && let Ok(input) =
64            input.slice_concrete(cx, 0, input_len).concrete_bytes(cx, "symbolic precompile input")
65    {
66        return execute_precompile(cx, address, &input, spec_id);
67    }
68
69    match precompile_number_for_spec(address, spec_id) {
70        Some(1) => {
71            // ECRECOVER ignores trailing bytes and pads short input with zeros.
72            let input = SymBytes::sized(cx, input, input_len, 128);
73            if let Ok(input) = input.concrete_bytes(cx, "symbolic ecrecover input") {
74                return execute_precompile(cx, address, &input, spec_id);
75            }
76            let v = input.word_at(cx, 32);
77            let v27 = SymBoolExpr::eq_word_const(cx, &v, U256::from(27));
78            let v28 = SymBoolExpr::eq_word_const(cx, &v, U256::from(28));
79            let valid_v = SymBoolExpr::or(cx, vec![v27, v28]);
80            if valid_v.as_const() == Some(false) {
81                return Ok(Some(SymReturnData::empty(cx)));
82            }
83
84            let input = input.materialize(cx);
85            let input_len = SymExpr::constant(cx, U256::from(128));
86            let word = symbolic_hash_word_with_len(cx, "ecrecover", input, input_len);
87            // Recovery may fail even with a valid v. Use an otherwise discarded byte of the
88            // opaque word so this choice is independent of the low 160-bit recovered address.
89            let recovered = byte_word(cx, U256::ZERO, word.clone()).nonzero_bool(cx);
90            let recovered = SymBoolExpr::and(cx, vec![valid_v, recovered]);
91            let full_len = SymExpr::constant(cx, U256::from(32));
92            let empty_len = SymExpr::zero(cx);
93            let len = SymExpr::ite(cx, recovered, full_len, empty_len);
94            let mut bytes = vec![SymExpr::zero(cx); 12];
95            bytes.extend((12..32).map(|idx| byte_word(cx, U256::from(idx), word.clone())));
96            let bytes = SymBytes::exprs(cx, bytes);
97            Ok(Some(SymReturnData { len_word: len, bytes }))
98        }
99        Some(2) => {
100            let input = input.materialize(cx);
101            let word = symbolic_hash_word_with_len(cx, "sha256", input, input_len);
102            let bytes = word.into_byte_exprs(cx);
103            Ok(Some(SymReturnData::from_byte_exprs(cx, bytes)))
104        }
105        Some(3) => {
106            let input = input.materialize(cx);
107            let word = symbolic_hash_word_with_len(cx, "ripemd160", input, input_len);
108            let mut bytes = vec![SymExpr::zero(cx); 12];
109            bytes.extend((12..32).map(|idx| byte_word(cx, U256::from(idx), word.clone())));
110            Ok(Some(SymReturnData::from_byte_exprs(cx, bytes)))
111        }
112        Some(4) => Ok(Some(SymReturnData { len_word: input_len, bytes: input })),
113        Some(5) => symbolic_modexp_precompile(cx, &input, input_len),
114        Some(6) => {
115            let input_len = input_len.as_usize_or("symbolic precompile input")?;
116            if input_len > input.len() {
117                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
118            }
119            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
120                return Err(SymbolicError::Unsupported(
121                    "symbolic bn254 precompile validity not modeled",
122                ));
123            }
124            Ok(Some(symbolic_fixed_len_precompile_output(cx, "bn254_add", &input, input_len, 64)))
125        }
126        Some(7) => {
127            let input_len = input_len.as_usize_or("symbolic precompile input")?;
128            if input_len > input.len() {
129                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
130            }
131            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
132                return Err(SymbolicError::Unsupported(
133                    "symbolic bn254 precompile validity not modeled",
134                ));
135            }
136            Ok(Some(symbolic_fixed_len_precompile_output(cx, "bn254_mul", &input, input_len, 64)))
137        }
138        Some(8) => {
139            let input_len = input_len.as_usize_or("symbolic precompile input")?;
140            if input_len % 192 != 0 {
141                return Ok(None);
142            }
143            if input_len > input.len() {
144                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
145            }
146            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
147                return Err(SymbolicError::Unsupported(
148                    "symbolic bn254 precompile validity not modeled",
149                ));
150            }
151            Ok(Some(symbolic_fixed_len_precompile_output(
152                cx,
153                "bn254_pairing",
154                &input,
155                input_len,
156                32,
157            )))
158        }
159        Some(9) => {
160            let input_len = input_len.as_usize_or("symbolic precompile input")?;
161            if input_len != 213 {
162                return Ok(None);
163            }
164            if input_len > input.len() {
165                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
166            }
167            let flag = input.byte(cx, 212);
168            match flag.as_const() {
169                Some(flag) if flag.is_zero() || flag == U256::ONE => {}
170                Some(_) => return Ok(None),
171                None => {
172                    return Err(SymbolicError::Unsupported(
173                        "symbolic blake2f precompile final flag not modeled",
174                    ));
175                }
176            }
177            Ok(Some(symbolic_fixed_len_precompile_output(cx, "blake2f", &input, input_len, 64)))
178        }
179        Some(10) => Err(SymbolicError::Unsupported("KZG handled by execute_kzg_precompile_call")),
180        _ => {
181            let input_len = input_len.as_usize_or("symbolic precompile input")?;
182            if input_len > input.len() {
183                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
184            }
185            let input = input
186                .slice_concrete(cx, 0, input_len)
187                .concrete_bytes(cx, "symbolic precompile input")?;
188            execute_precompile(cx, address, &input, spec_id)
189        }
190    }
191}
192
193pub(crate) fn symbolic_modexp_precompile(
194    cx: &mut SymCx,
195    input: &SymBytes,
196    input_len: SymExpr,
197) -> Result<Option<SymReturnData>, SymbolicError> {
198    let input_len = input_len.as_usize_or("symbolic precompile input")?;
199    if input_len > input.len() {
200        return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
201    }
202
203    let modulus_len = concrete_precompile_word_at(cx, input, 64)?;
204    let modulus_len = usize::try_from(modulus_len)
205        .ok()
206        .ok_or(SymbolicError::Unsupported("symbolic modexp output length"))?;
207    if modulus_len > 4096 {
208        return Err(SymbolicError::Unsupported("symbolic modexp output length"));
209    }
210    Ok(Some(symbolic_fixed_len_precompile_output(cx, "modexp", input, input_len, modulus_len)))
211}
212
213pub(crate) fn concrete_precompile_word_at(
214    cx: &mut SymCx,
215    input: &SymBytes,
216    offset: usize,
217) -> Result<U256, SymbolicError> {
218    let mut bytes = [0u8; 32];
219    for (idx, byte) in bytes.iter_mut().enumerate() {
220        let word = input.byte(cx, offset + idx);
221        *byte = word.as_const_or("symbolic precompile length header")?.to::<u8>();
222    }
223    Ok(U256::from_be_bytes(bytes))
224}
225
226pub(crate) fn symbolic_fixed_len_precompile_output(
227    cx: &mut SymCx,
228    algorithm: &'static str,
229    input: &SymBytes,
230    input_len: usize,
231    output_len: usize,
232) -> SymReturnData {
233    let input_len_word = SymExpr::constant(cx, U256::from(input_len));
234    let input = input.materialize(cx);
235    let mut bytes = Vec::with_capacity(output_len);
236    for chunk in 0..output_len.div_ceil(32) {
237        let mut chunk_input = Vec::with_capacity(input.len() + 1);
238        chunk_input.push(SymExpr::constant(cx, U256::from(chunk)));
239        chunk_input.extend(input.iter().cloned());
240        bytes.extend(
241            symbolic_hash_word_with_len(cx, algorithm, chunk_input, input_len_word.clone())
242                .into_byte_exprs(cx),
243        );
244    }
245    bytes.truncate(output_len);
246    SymReturnData::from_byte_exprs(cx, bytes)
247}
foundry_evm_symbolic/runtime/precompiles.rs

foundry_evm_symbolic/runtime/
precompiles.rs
