Failure to build Docker image for CHES23 paper artefacts about libjade HOT 3 CLOSED

Hi @rod-chapman, thanks for the report.

I propose a temporary fix below. For a permanent fix: could you report this issue in the Hakyber repository so we can document the fixing process? https://github.com/formosa-crypto/hakyber

Even though the problematic Dockerfile isn't in that repository, it should be.

• I reproduced the issue with Debian/Docker; I believe the problem is related to Opam package versions, but I'm no expert with Opam.

• I downloaded the artifact from here: https://artifacts.formosa-crypto.org/

• I changed the Dockerfile to the following:

FROM debian:latest
WORKDIR /root
COPY ./ /root/
RUN apt update && apt install -y opam cvc4 vim gcc clang
RUN opam init --auto-setup -y --disable-sandboxing -c ocaml-base-compiler.4.12.0
RUN eval $(opam env)
RUN opam install -y depext
RUN opam depext -y alt-ergo.2.4.2 z3.4.8.14
RUN opam install -y alt-ergo.2.4.2 z3.4.8.14
RUN opam pin -yn add easycrypt /root/easycrypt
RUN opam depext -y easycrypt && opam install -y easycrypt
RUN eval $(opam env) && easycrypt why3config
RUN opam depext -y jasmin && opam install -y jasmin
ENV PATH="$PATH:/root/jasmin/compiler/"
RUN echo "[general]\nidirs=Jasmin:/root/jasmin/eclib" >> /root/.config/easycrypt/easycrypt.conf
WORKDIR /root
CMD ["/bin/bash", "--login"]

Notes about the changes:

1. there was some issue with alt-ergo 2.4.1 / dune / EasyCrypt and, as such, I had to update to alt-ergo 2.4.2;
2. I had to install the Jasmin released 2022.09.2 instead of the one distributed with release package
3. notes on 2), this will likely change when we manage to do a proper fix and update the artifact; nonetheless, it seems to have no impact on checking the proofs given that the Jasmin compiler doesn't seem to be used when running make check;

After docker builds the image:

docker run -it hakyber bash
eval $(opam env)
make check

One last note: I didn't wait for make check to finish. One file is still being checked by EasyCrypt -- the other 136 were OK.

from libjade.

Thanks for the update. I raised Issue#6 over in the hakyber repo (Sorry I didn't find that to start with...)

from libjade.

I will close this issue given that it is being followed here: formosa-crypto/formosa-mlkem#6

from libjade.