Symbolic execution queue should be used to run SMT as well #934

msooseth · 2025-11-26T17:53:16Z

Description

This now finally does what I was aiming for :) You can pass in a function that will be run on the Expr End and the results will be collated. This is now done with the handler.

Notice that we now have to add a task for the Partial as well as the handler needs to be executed on this, here:

-                    -- got us to this point and return a partial leaf for the other side
-                    liftIO . atomically $ writeTChan res (Partial [] (TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels) (MaxIterationsReached vm.state.
pc vm.state.contract))
+                    -- got us to this point and queue a task to return a partial leaf for the other side
+                    let partialLeaf = Partial [] (TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels) (MaxIterationsReached vm.state.pc vm.state.contract
)
+                    liftIO $ atomically $ modifyTVar numTasks (+1)
+                    liftIO $ writeChan taskq $ t { vm = vm, stepper = pure partialLeaf }

This was actually done bye Claude Code at first, but I had to adjust quite a bit.

Now it finds the Cex for prove_inv_identity in src/ABDKMath64x64PropertyTests.sol:CryticABDKMath64x64Properties instantaneously, but keeps running.

I will write a cexHander for equivalence checking as a follow-up PR.

Checklist

tested locally
added automated tests
updated the docs
updated the changelog

msooseth · 2025-11-26T19:52:43Z

Now runs like:

[RUNNING] prove_inv_identity(int128)
   Counterexample:   [validated]
     calldata: prove_inv_identity(-108003701288662363396026832958930103201)
     result:   Revert: 0x4e487b710000000000000000000000000000000000000000000000000000000000000001
   [FAIL] prove_inv_identity
   [WARNING] hevm was only able to partially explore the test prove_inv_identity due to:
      3x -> SMT solver says: Result unknown by SMT solver

This will need an update to the docs. But it should be a lot easier to use for users.

gustavo-grieco · 2025-11-26T20:06:37Z

This is great, a leap forward in terms of usability (specially for getting counter examples!)

msooseth · 2025-11-26T20:14:52Z

Yes, this was the actual goal of the symbolic queue that Martin has helped with a lot. So we are finally making progress to be much more user-friendly, and show relevant results immediately.

Update ChangeLog some progress Making progress Cleaner Cleaner Changelog update Cleaner Fixing test.hs Fix rpc Cleanup Cleaner PR Fixing cexHander to cexHandler Update name of parameter

gustavo-grieco · 2025-12-01T15:12:38Z

Oh, btw, should stop the exploration immediately if a CEX if found?

msooseth · 2025-12-01T15:25:46Z

Oh, btw, should stop the exploration immediately if a CEX if found?

Yep, we are thinking about adding that option exactly :) I'll add it in a sec :)

Update Use Chan Cleanup

Cleaner Updte

msooseth · 2025-12-02T20:00:15Z

Oh, btw, should stop the exploration immediately if a CEX if found?

Yep, we are thinking about adding that option exactly :) I'll add it in a sec :)

OOops, forgot to add that. Will do it tomorrow as a separate PR. Should be very simple :)

blishko

I think this looks good! I have just a few small questions.

blishko · 2025-12-03T19:15:07Z

src/EVM/SymExec.hs

+    putStrLn $ "   Exploration finished, " <> show (length results) <> " branch(es) checked in call " <> call <> " of which partial: "
+                <> show (length smtResults)


I think this message here is misleading now.
At this point, not only exploration has finished, but also all the solving, no?
At least before, "exploration" meant only the first phase, excluding the solving.

Good point! I now did this:

commit c5a56bb3ebee5bcf42dc6cf7e1c2bb78c5920e9c (HEAD -> queue-check, origin/queue-check) Author: Mate Soos <[email protected]> Date: Thu Dec 4 12:59:01 2025 +0100 Better printing to the user diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index d26971b4..d702c11b 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -820,7 +820,9 @@ verifyInputsWithHandler verifyInputsWithHandler solvers opts fetcher preState post cexHandler = do conf <- readConfig let call = mconcat ["prefix 0x", getCallPrefix preState.state.calldata] - when conf.debug $ liftIO $ putStrLn $ " Exploring call " <> call + when conf.debug $ liftIO $ do + putStrLn $ " Keccak preimages in state: " <> (show $ length preState.keccakPreImgs) + putStrLn $ " Exploring call " <> call results <- executeVM fetcher opts.iterConf preState $ \leaf -> do -- Extract partial if applicable @@ -846,9 +848,8 @@ verifyInputsWithHandler solvers opts fetcher preState post cexHandler = do when conf.debug $ liftIO $ do putStrLn $ " Exploration and solving finished, " <> show (length results) <> " branch(es) checked in call " <> call <> " of which partial: " <> show (length smtResults) - putStrLn $ " Keccak preimages in state: " <> (show $ length preState.keccakPreImgs) let cexs = filter (\(res, _) -> not . isQed $ res) smtResults - putStrLn $ " Found " <> show (length cexs) <> " potential counterexample(s) in call " <> call + putStrLn $ " Found " <> show (length cexs) <> " counterexample(s) in call " <> call pure (smtResults, catMaybes partials) where

So the printing should be better I think!

src/EVM/UnitTest.hs

src/EVM/SymExec.hs

hevm.cabal

Update

msooseth · 2025-12-04T12:22:22Z

Thanks, you have made this a lot better :) Can you take another look maybe?

blishko

This one is ready!

msooseth force-pushed the queue-check branch 3 times, most recently from 496d50b to f6d8375 Compare November 26, 2025 19:51

msooseth force-pushed the queue-check branch 3 times, most recently from 61c2bce to 39f6258 Compare November 26, 2025 20:33

msooseth changed the title ~~[DRAFT] Symbolic execution queue should be used to run SMT as well~~ Symbolic execution queue should be used to run SMT as well Nov 26, 2025

msooseth marked this pull request as ready for review November 26, 2025 20:36

msooseth requested a review from blishko November 26, 2025 20:36

Symbolic execution queue should be used to run SMT as well

b543b4c

Update ChangeLog some progress Making progress Cleaner Cleaner Changelog update Cleaner Fixing test.hs Fix rpc Cleanup Cleaner PR Fixing cexHander to cexHandler Update name of parameter

msooseth force-pushed the queue-check branch from f922e0b to b543b4c Compare December 1, 2025 10:44

msooseth force-pushed the queue-check branch 2 times, most recently from 76ec6be to 749a796 Compare December 2, 2025 13:00

Initial process queue

1ab45a2

Update Use Chan Cleanup

msooseth force-pushed the queue-check branch from 749a796 to 1ab45a2 Compare December 2, 2025 15:14

Cleaner channels

b77cc4a

msooseth force-pushed the queue-check branch from c1d22eb to 7e2f24c Compare December 2, 2025 15:50

msooseth added 2 commits December 2, 2025 16:58

No need for reschan

fcd5021

Cleaner Updte

Update to fix deadlock

4bf8057

msooseth force-pushed the queue-check branch from 7e2f24c to 4bf8057 Compare December 2, 2025 16:01

blishko reviewed Dec 3, 2025

View reviewed changes

msooseth added 3 commits December 4, 2025 12:41

Cleaner toProps

5ec5f47

Fixing printing

08e889f

Better printing to the user

c5a56bb

msooseth added 2 commits December 4, 2025 13:16

Fixing Err Bool as pointed out by @blishko

5540297

Update

No need for these Monads here

52c8ba8

blishko approved these changes Dec 4, 2025

View reviewed changes

msooseth merged commit 137355e into main Dec 4, 2025
6 of 7 checks passed

msooseth deleted the queue-check branch December 4, 2025 13:15

		putStrLn $ " Exploration finished, " <> show (length results) <> " branch(es) checked in call " <> call <> " of which partial: "
		<> show (length smtResults)

Symbolic execution queue should be used to run SMT as well #934

Symbolic execution queue should be used to run SMT as well #934

Uh oh!

Conversation

msooseth commented Nov 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Checklist

Uh oh!

msooseth commented Nov 26, 2025

Uh oh!

gustavo-grieco commented Nov 26, 2025

Uh oh!

msooseth commented Nov 26, 2025

Uh oh!

gustavo-grieco commented Dec 1, 2025

Uh oh!

msooseth commented Dec 1, 2025

Uh oh!

msooseth commented Dec 2, 2025

Uh oh!

blishko left a comment

Choose a reason for hiding this comment

Uh oh!

blishko Dec 3, 2025

Choose a reason for hiding this comment

Uh oh!

msooseth Dec 4, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

msooseth commented Dec 4, 2025

Uh oh!

blishko left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

msooseth commented Nov 26, 2025 •

edited

Loading