Repository navigation
Conversation
Symbolic ecrecover checked only `v`, so a signature with `r = 0` or `s = 0` counted as recoverable and a true property reported a counterexample that did not replay. Require `r` and `s` in `[1, n)` as the precompile does; outside that range it returns no data.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
Please address the ecrecover counterexample replay regression below.
| )); | ||
| valid.push(scalar.nonzero_bool(cx)); | ||
| } | ||
| let valid_v = SymBoolExpr::and(cx, valid); |
There was a problem hiding this comment.
Please preserve replayable malformed-signature witnesses when adding this predicate. The existing ecrecover_basic_modeling test (assert(ecrecover(h, v, r, s) != address(0)) with unconstrained inputs) now reports incomplete symbolic execution (Error): symbolic counterexample did not replay instead of the expected replay-confirmed assertion failure; the head CI job reproduces this on all three attempts. There are trivial concrete counterexamples (for example all-zero inputs), so this loses an existing counterexample-finding capability and breaks the CLI suite. The scalar bounds are correct, but witness selection/replay needs to continue finding a concrete invalid signature rather than stopping at the abstract recovery mismatch.
With `r` and `s` range-checked, the solver picked well-formed inputs whose modeled recovery failed through the opaque term, and concrete ecrecover recovered an address, so the counterexample did not replay. Fork a symbolic ECRECOVER call: the malformed path returns no data and continues first, so its counterexamples replay exactly; the well-formed path keeps the opaque recovery model.
mattsse
left a comment
mattsse
left a comment
There was a problem hiding this comment.
The previous replay finding is fixed. One redirected-call regression remains below.
| } | ||
| state.constraints = | ||
| if malformed_sat { malformed_constraints } else { well_formed_constraints }; | ||
| let outcome = execute_symbolic_precompile(&mut self.cx, to, input, input_len, spec_id)?; |
There was a problem hiding this comment.
Use the resolved code_address for precompile execution here and in the both-feasible branch. The caller dispatches this helper using code_address, but passes the original to; these differ after vm.mockFunction. For example, mock address(4) to address(1) for abi.encode(bytes32(0), uint256(27), bytes32(0), bytes32(0)), then staticcall address(4): concrete execution and the previous symbolic implementation return empty ecrecover output, whereas this call executes identity and returns all 128 input bytes. Redirecting an ordinary contract instead produces unsupported precompile. Keep the original recipient for call effects, but execute the resolved ecrecover precompile.
Run the resolved precompile address after mockFunction redirects a call. Keep the original recipient for call effects. Concrete fuzz and symbolic CLI tests agree on the empty ecrecover result.
Why
Symbolic ecrecover treated signatures with r = 0 or s = 0 as recoverable, so true properties reported a counterexample that did not replay. Found by symdiff (Tempo).
Change
Symbolic ecrecover validity also requires r and s nonzero and below the secp256k1 order. Case folded into
symbolic_ecrecover_return_data_conformance.Downstream
Base
mablr/evm2-migration. No public behavior change outside the buggy case.