Updated solvers

[weaversa]

The cryptol-remote-api container pulls in the latest August release of the solvers -- https://github.com/GaloisInc/cryptol/blob/master/cryptol-remote-api/Dockerfile

where as saw-remote-api is using the year old release of solvers -- https://github.com/GaloisInc/saw-script/blob/master/saw-remote-api/Dockerfile

Will you consider updating the saw-remote-api's solvers to the latest?

[weaversa]

Same here: https://github.com/GaloisInc/saw-script/blob/master/saw/Dockerfile

[RyanGlScott]

Sure, we could update them. One minor complication is that we can't jump straight to the latest what4-solvers snapshot, as the SAW Docker images use Ubuntu 18.04, but what4-solvers' latest snapshot supports Ubuntu 20.04 as the minimum. We could still update it to snapshot-20220721, however, and that is relatively up to date.

Alternatively, we could wait until we fix #1741, as we will have to update the what4-solvers snapshot to the latest one in order to fix that issue.

[weaversa]

I'm cheating a bit here by relying on you to build the tools...but it all seems to work on 22.04.

FROM public.ecr.aws/lts/ubuntu:22.04_stable

USER root

RUN ln -snf /usr/share/zoneinfo/$CONTAINER_TIMEZONE /etc/localtime && echo $CONTAINER_TIMEZONE > /etc/timezone

RUN apt-get update \
    && apt-get install -y libgmp10 libgomp1 libffi8 libncurses6 libtinfo6 libreadline8 libnuma-dev openssl openjdk-11-jdk-headless \
    && apt-get clean && rm -rf /var/lib/apt/lists/*

COPY --from=ghcr.io/galoisinc/saw-remote-api:nightly /usr/local/bin /usr/local/bin

# Grab updated solvers from cryptol-remote-api container
COPY --from=ghcr.io/galoisinc/cryptol-remote-api:nightly /usr/local/bin /usr/local/bin

RUN useradd -m saw && chown -R saw:saw /home/saw
USER saw

ENV LANG=C.UTF-8 \
    LC_ALL=C.UTF-8

ENTRYPOINT ["/usr/local/bin/saw-remote-api"]

WORKDIR /home/saw
# Create self-signed certificates for HTTPS testing purposes - N.B.,
# clients must opt in to accepting these by passing `verify=False` to
# the `cryptol.connect` method (otherwise a security error is raised).
RUN openssl req -nodes -newkey rsa:2048 -keyout server.key -out server.csr \
      -subj "/C=GB/ST=London/L=London/O=Acme Widgets/OU=IT Department/CN=localhost"
RUN openssl x509 -req -days 365 -in server.csr -signkey server.key -out server.crt

CMD ["http", "--host", "0.0.0.0", "--port", "8080", "/"]

EXPOSE 8080

[RyanGlScott]

It's possible that it could work by accident, but I worry about there being incompatibilities between shared libraries used on Ubuntu 18.04 and 22.04. In practice, I've definitely encountered scenarios where solvers built for one version don't work on another due to glibc version differences.