CVC5 fails with Cryptol 3.0.0

[jpziegler]

Using the latest Cryptol docker container, Cryptol doesn't detect CVC5 via the command :s prover=cvc5, even though it is present in the path.

Oddly, running :s prover=w4-cvc5 works fine.

% docker run -it ghcr.io/galoisinc/cryptol
┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :s prover=cvc5
Warning: cvc5 installation not found
Cryptol> :s prover=w4-cvc5
Cryptol> 

[RyanGlScott]

I can reproduce this. My current hypothesis: this happens because the Docker image bundles cvc5-1.0.2, which suffers from https://github.com/cvc5/cvc5/issues/8900. This issue can arise when using cvc5 in combination with the way SBV communicates with SMT solvers. What4, on the other hand, communicates with solvers a different way, which is why the issue does not appear with prover=w4-cvc5. (Note that prover=cvc5 is an alias for prover=sbv-cvc5.)

Normally, https://github.com/cvc5/cvc5/issues/8900 is harmless on Linux, as it will just create a stray file named "stdout" in the same directory where you run cvc5. But the Cryptol Docker image is a different story, since the default entrypoint to the image is in a read-only directory. And sure enough, if you try to run the same command that SBV performs under the hood in the Docker image, it fails:

cryptol@8dc4383d833b:/$ cvc5 ~/a.smt2 
(error "Error in option parsing: Cannot open file: `""stdout""': unknown reason")

I think the simplest solution would be to use a newer cvc5 version in the Cryptol Docker image that doesn't suffer from https://github.com/cvc5/cvc5/issues/8900, such as cvc5-1.0.5.

[RyanGlScott]

I believe #1549 has fixed this. I'll reopen this until I've had a chance to verify this in the next nightly Cryptol Docker build (which should happen within 24 hours).

[RyanGlScott]

Unfortunately, the nightly build still doesn't quite work, but this time, the mistake was caught by CI:

  > [build 17/19] RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .)     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .)     && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .)     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .)     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .):
------
Dockerfile:42
--------------------
  41 |     ENV PATH=/usr/local/bin:/cryptol/rootfs/usr/local/bin:$PATH
  42 | >>> RUN    ! $(cryptol -c ":s prover=yices" | tail -n +2 | grep -q .) \
  43 | >>>     #    && ! $(cryptol -c ":s prover=mathsat" | tail -n +2 | grep -q .) \
  44 | >>>     && ! $(cryptol -c ":s prover=cvc4" | tail -n +2 | grep -q .) \
  45 | >>>     && ! $(cryptol -c ":s prover=cvc5" | tail -n +2 | grep -q .) \
  46 | >>>     && ! $(cryptol -c ":s prover=abc" | tail -n +2 | grep -q .) \
  47 | >>>     # && ! $(cryptol -c ":s prover=boolector" | tail -n +2 | grep -q .) \
  48 | >>>     && ! $(cryptol -c ":s prover=z3" | tail -n +2 | grep -q .)
  49 |     RUN mkdir -p rootfs/"${CRYPTOLPATH}" \
--------------------
ERROR: failed to solve: process "/bin/sh -c ! $(cryptol -c \":s prover=yices\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=cvc4\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=cvc5\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=abc\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=z3\" | tail -n +2 | grep -q .)" did not complete successfully: exit code: 1
Error: buildx failed with: ERROR: failed to solve: process "/bin/sh -c ! $(cryptol -c \":s prover=yices\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=cvc4\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=cvc5\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=abc\" | tail -n +2 | grep -q .)     && ! $(cryptol -c \":s prover=z3\" | tail -n +2 | grep -q .)" did not complete successfully: exit code: 1

And indeed, I am able to reproduce this with cryptol-3.0.0 and cvc5-1.0.5. This time, the issue is that we are building Cryptol against too old of a version of SBV (9.2), which lacks some important subprocess-related changes that were added as part of a fix for https://github.com/LeventErkok/sbv/issues/644. I've confirmed locally that building against a newer SBV version fixes the issue.

[RyanGlScott]

This issue appears to be resolved with the latest nightly Docker image:

┏━╸┏━┓╻ ╻┏━┓╺┳╸┏━┓╻  
┃  ┣┳┛┗┳┛┣━┛ ┃ ┃ ┃┃  
┗━╸╹┗╸ ╹ ╹   ╹ ┗━┛┗━╸
version 3.0.0.99
https://cryptol.net  :? for help

Loading module Cryptol
Cryptol> :s prover=cvc5
Cryptol> :prove \(x : [8]) -> x * 2 == x << 1
Q.E.D.
(Total Elapsed Time: 0.007s, using "CVC5")

As such, I'll close this issue. Please re-open this (or file another issue) if you encounter something else amiss with Cryptol's CVC5 support.