Solidity: Docker image to wrap z3 behind http

[chriseth]

For remix, it would be helpful to have a docker image that exposes z3 / smtlib via HTTP so that it can be used from within the browser.

The idea would be to run the image either locally or on a server and connect remix to it via ajax requests.

The image should have an open port with an http server behind it, which forwards the request payload to the standard input of a z3 instance run using something like z3 -smt2 -in and responds with the contents of standard output of the command.

Example smtlib2 inputs look like:

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
(get-model)

The output of z3 on this would be:

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

During a single compilation run, multiple of these requests would be sent to the z3 "server".

[axic]

For privacy reasons I think the function names should be hashed. This would be the first instance Remix sending contract data out as part of the compilation process.

[eelkevdbos]

I would like to pick this one up. Should I reference the created repo / docker image in this thread or create a pull request somewhere?

[chriseth]

Thanks, @eelkevdbos ! You can put the dockerfile into the scripts directory (under a different name).

[eelkevdbos]

@chriseth I could inline the docker file but providing a 'script' seems more suitable and keeps the development of the wrapper less bound to the solidity project. We could also opt for a 'wget' approach of the go binary inside a vanilla golang docker image.

[chriseth]

@eelkevdbos wonderful, that's exactly the functionality that we need :-)

Would it be possible to make the image a "little" smaller than 700 MB? Also I'm not a big fan of using files external to the Dockerfile, at least for such tiny things - I guess that's a philosophical question...

[eelkevdbos]

I managed to compile z3 (4.5.0) for alpine linux. This creates a smaller image (200 MB), but the output differs:

alpine

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!0 Int) (x!1 Bool)) Int
    (ite (and (= x!0 11) (= x!1 true)) 0
      0))
)

debian stretch

sat
(model 
  (define-fun a () Int
    11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int
    (ite (and (= x!1 11) (= x!2 true)) 0
      0))
)

I can't really judge if this is a deal-breaker (it seems the index of starts at 0 instead of 1). Can you perhaps shine some light on the differences?

[chriseth]

Ah, that's great! The difference in the output is weird but does not change the behaviour (the x!1 are just names of local variables).

Another thing that I forgot to mention: The http server should respond to CORS requests and approve all of them.

[eelkevdbos]

Allright! I modified the request handler to approve all CORS requests. A simple docker pull evdb/z3-http would suffice to pull in the new image.

[eelkevdbos]

Updated to python, should be fine now, sorry for the wait.

[eelkevdbos]

Hi @chriseth is there anything I can do to help resolve this issue? I've updated the pull request to reflect the feedback given #3056

[chriseth]

I'm sorry, we are just not sure whether this is the way to go because it is still a little cumbersome. If we decide to do it like this, we will pick up your docker image again. Thanks for your help and sorry for the bad planning on our side.

[eelkevdbos]

No problem, I will look for some other low hanging fruit issue if available.

[leonardoalt]

This might not be needed anymore since we have https://github.com/ethereum/solidity/pull/8909