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
23pub(crate) fn execute_precompile(
24    cx: &mut SymCx,
25    address: Address,
26    input: &[u8],
27    spec_id: SpecId,
28) -> Result<Option<SymReturnData>, SymbolicError> {
29    let output = match precompile_number_for_spec(address, spec_id) {
30        Some(1) => secp256k1::ec_recover_run(input, u64::MAX),
31        Some(2) => hash::sha256_run(input, u64::MAX),
32        Some(3) => hash::ripemd160_run(input, u64::MAX),
33        Some(4) => identity::identity_run(input, u64::MAX),
34        Some(5) => modexp::berlin_run(input, u64::MAX),
35        Some(6) => bn254::run_add(input, bn254::add::ISTANBUL_ADD_GAS_COST, u64::MAX),
36        Some(7) => bn254::run_mul(input, bn254::mul::ISTANBUL_MUL_GAS_COST, u64::MAX),
37        Some(8) => bn254::run_pair(
38            input,
39            bn254::pair::ISTANBUL_PAIR_PER_POINT,
40            bn254::pair::ISTANBUL_PAIR_BASE,
41            u64::MAX,
42        ),
43        Some(9) => blake2::run(input, u64::MAX),
44        Some(10) => kzg_point_evaluation::run(input, u64::MAX),
45        _ => return Err(SymbolicError::Unsupported("unsupported precompile")),
46    };
47
48    match output {
49        Ok(output) => Ok(Some(SymReturnData::from_concrete_bytes(cx, output.bytes.to_vec()))),
50        Err(_) => Ok(None),
51    }
52}
53
54pub(crate) fn execute_symbolic_precompile(
55    cx: &mut SymCx,
56    address: Address,
57    input: SymBytes,
58    input_len: SymExpr,
59    spec_id: SpecId,
60) -> Result<Option<SymReturnData>, SymbolicError> {
61    if let Some(input_len) = input_len.as_const()
62        && let Ok(input_len) = usize::try_from(input_len)
63        && input_len <= input.len()
64        && let Ok(input) =
65            input.slice_concrete(cx, 0, input_len).concrete_bytes(cx, "symbolic precompile input")
66    {
67        return execute_precompile(cx, address, &input, spec_id);
68    }
69
70    match precompile_number_for_spec(address, spec_id) {
71        Some(1) => {
72            // ECRECOVER ignores trailing bytes and pads short input with zeros.
73            let input = SymBytes::sized(cx, input, input_len, 128);
74            if let Ok(input) = input.concrete_bytes(cx, "symbolic ecrecover input") {
75                return execute_precompile(cx, address, &input, spec_id);
76            }
77            let v = input.word_at(cx, 32);
78            let v27 = SymBoolExpr::eq_word_const(cx, &v, U256::from(27));
79            let v28 = SymBoolExpr::eq_word_const(cx, &v, U256::from(28));
80            let valid_v = SymBoolExpr::or(cx, vec![v27, v28]);
81            if valid_v.as_const() == Some(false) {
82                return Ok(Some(SymReturnData::empty(cx)));
83            }
84
85            let input = input.materialize(cx);
86            let input_len = SymExpr::constant(cx, U256::from(128));
87            let word = symbolic_hash_word_with_len(cx, "ecrecover", input, input_len);
88            // Recovery may fail even with a valid v. Use an otherwise discarded byte of the
89            // opaque word so this choice is independent of the low 160-bit recovered address.
90            let recovered = byte_word(cx, U256::ZERO, word.clone()).nonzero_bool(cx);
91            let recovered = SymBoolExpr::and(cx, vec![valid_v, recovered]);
92            let full_len = SymExpr::constant(cx, U256::from(32));
93            let empty_len = SymExpr::zero(cx);
94            let len = SymExpr::ite(cx, recovered, full_len, empty_len);
95            let mut bytes = vec![SymExpr::zero(cx); 12];
96            bytes.extend((12..32).map(|idx| byte_word(cx, U256::from(idx), word.clone())));
97            let bytes = SymBytes::exprs(cx, bytes);
98            Ok(Some(SymReturnData { len_word: len, bytes }))
99        }
100        Some(2) => {
101            let input = input.materialize(cx);
102            let word = symbolic_hash_word_with_len(cx, "sha256", input, input_len);
103            let bytes = word.into_byte_exprs(cx);
104            Ok(Some(SymReturnData::from_byte_exprs(cx, bytes)))
105        }
106        Some(3) => {
107            let input = input.materialize(cx);
108            let word = symbolic_hash_word_with_len(cx, "ripemd160", input, input_len);
109            let mut bytes = vec![SymExpr::zero(cx); 12];
110            bytes.extend((12..32).map(|idx| byte_word(cx, U256::from(idx), word.clone())));
111            Ok(Some(SymReturnData::from_byte_exprs(cx, bytes)))
112        }
113        Some(4) => Ok(Some(SymReturnData { len_word: input_len, bytes: input })),
114        Some(5) => symbolic_modexp_precompile(cx, &input, input_len),
115        Some(6) => {
116            let input_len = input_len.as_usize_or("symbolic precompile input")?;
117            if input_len > input.len() {
118                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
119            }
120            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
121                return Err(SymbolicError::Unsupported(
122                    "symbolic bn254 precompile validity not modeled",
123                ));
124            }
125            Ok(Some(symbolic_fixed_len_precompile_output(cx, "bn254_add", &input, input_len, 64)))
126        }
127        Some(7) => {
128            let input_len = input_len.as_usize_or("symbolic precompile input")?;
129            if input_len > input.len() {
130                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
131            }
132            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
133                return Err(SymbolicError::Unsupported(
134                    "symbolic bn254 precompile validity not modeled",
135                ));
136            }
137            Ok(Some(symbolic_fixed_len_precompile_output(cx, "bn254_mul", &input, input_len, 64)))
138        }
139        Some(8) => {
140            let input_len = input_len.as_usize_or("symbolic precompile input")?;
141            if input_len % 192 != 0 {
142                return Ok(None);
143            }
144            if input_len > input.len() {
145                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
146            }
147            if (0..input_len).any(|idx| input.byte(cx, idx).as_const().is_none()) {
148                return Err(SymbolicError::Unsupported(
149                    "symbolic bn254 precompile validity not modeled",
150                ));
151            }
152            Ok(Some(symbolic_fixed_len_precompile_output(
153                cx,
154                "bn254_pairing",
155                &input,
156                input_len,
157                32,
158            )))
159        }
160        Some(9) => {
161            let input_len = input_len.as_usize_or("symbolic precompile input")?;
162            if input_len != 213 {
163                return Ok(None);
164            }
165            if input_len > input.len() {
166                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
167            }
168            let flag = input.byte(cx, 212);
169            match flag.as_const() {
170                Some(flag) if flag.is_zero() || flag == U256::ONE => {}
171                Some(_) => return Ok(None),
172                None => {
173                    return Err(SymbolicError::Unsupported(
174                        "symbolic blake2f precompile final flag not modeled",
175                    ));
176                }
177            }
178            Ok(Some(symbolic_fixed_len_precompile_output(cx, "blake2f", &input, input_len, 64)))
179        }
180        Some(10) => Err(SymbolicError::Unsupported("KZG handled by execute_kzg_precompile_call")),
181        _ => {
182            let input_len = input_len.as_usize_or("symbolic precompile input")?;
183            if input_len > input.len() {
184                return Err(SymbolicError::Unsupported("out-of-bounds symbolic precompile input"));
185            }
186            let input = input
187                .slice_concrete(cx, 0, input_len)
188                .concrete_bytes(cx, "symbolic precompile input")?;
189            execute_precompile(cx, address, &input, spec_id)
190        }
191    }
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.as_const_or("symbolic precompile length header")?.to::<u8>();
223    }
224    Ok(U256::from_be_bytes(bytes))
225}
226
227pub(crate) fn symbolic_fixed_len_precompile_output(
228    cx: &mut SymCx,
229    algorithm: &'static str,
230    input: &SymBytes,
231    input_len: usize,
232    output_len: usize,
233) -> SymReturnData {
234    let input_len_word = SymExpr::constant(cx, U256::from(input_len));
235    let input = input.materialize(cx);
236    let mut bytes = Vec::with_capacity(output_len);
237    for chunk in 0..output_len.div_ceil(32) {
238        let mut chunk_input = Vec::with_capacity(input.len() + 1);
239        chunk_input.push(SymExpr::constant(cx, U256::from(chunk)));
240        chunk_input.extend(input.iter().cloned());
241        bytes.extend(
242            symbolic_hash_word_with_len(cx, algorithm, chunk_input, input_len_word.clone())
243                .into_byte_exprs(cx),
244        );
245    }
246    bytes.truncate(output_len);
247    SymReturnData::from_byte_exprs(cx, bytes)
248}
foundry_evm_symbolic/runtime/precompiles.rs

foundry_evm_symbolic/runtime/
precompiles.rs
