Update hevm with arithmetic abstraction and execution optimizations

[gustavo-grieco]

Enable arithmetic abstraction for symbolic execution and reduce concrete execution overhead. Stack and Nix now pin hevm to b36def2111d4edc60107ea5753d7b51ce30b4249 from argotorg/hevm#1075. This revision already contains the hevm changes referenced by #1621.

Integrate #1621's remaining optimizations: build hevm with -O2 in Stack and Nix, and disable Keccak preimage recording for campaigns without symbolic execution. For symbolic campaigns, recording stays enabled from VM initialization through deployment and concrete transaction replay, so later solver calls receive the earlier preimages. FFI configuration is preserved.

Arithmetic abstraction is enabled for exploration and verification through the internal symExecAbstractArith = True switch. YAML and CLI configuration are deferred.

Regression coverage under Z3 and Bitwuzla checks completed arithmetic proofs, rejection of spurious multiplication models, and concrete replay of division/multiplication counterexamples. The small arithmetic-abstraction.sol fixture proves multiplication monotonicity with bounds preventing overflow. With solc 0.8.25 and a 30-second SMT budget, the measured CLI comparison (including compilation) was:

Solver	Abstraction enabled	Abstraction disabled
Z3 4.15.4	Verified in 1.58s	Unknown after 31.85s
Bitwuzla 0.8.2	Verified in 1.58s	Unknown after 31.74s

The Keccak regression first solves a hash check using a constructor preimage and replays the generated transaction. It then records a new hash in another transaction and solves a second check. It requires the exact original arguments and successful reproduction of each assertion failure. A separate case verifies that concrete-only campaigns still hash correctly without collecting preimages.

Validation:

• Stack build with -Werror; all 60 selected configuration, symbolic, assertion, overflow, replay, and cheatcode tests passed with solc 0.8.25.
• Keccak and arithmetic-abstraction regressions also passed under both solvers with solc 0.5.17.
• Temporarily clearing preimages at the solver boundary caused both Keccak regressions to fail: the solvers returned the spurious argument 0 instead of the stored secret. Restoring the preimages made them pass.
• hlint lib src and git diff --check passed.
• Nix source hash and optimization settings updated; Nix build not run.