Failure to build Docker image for CHES23 paper artefacts

[rod-chapman]

Dear Jasmin/LibJade/Easycrypt team.

I am trying to build the Docker image for the artefacts that accompany the CHES'23 "Formally verifying Cyber" paper.

I am using Docker version 20.10.17, build 100c701 on an Intel-baed Mac, running macOS 13.3.1

Following the README.md file, I get

docker build -t hakyber .

[+] Building 1406.8s (20/22)                                                                                          
 => [internal] load build definition from Dockerfile                                                             0.0s
 => => transferring dockerfile: 1.16kB                                                                           0.0s
 => [internal] load .dockerignore                                                                                0.0s
 => => transferring context: 2B                                                                                  0.0s
 => [internal] load metadata for docker.io/library/debian:latest                                                 1.7s
 => [ 1/18] FROM docker.io/library/debian:latest@sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b85  11.7s
 => => resolve docker.io/library/debian:latest@sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b8511c  0.0s
 => => sha256:63d62ae233b588d6b426b7b072d79d1306bfd02a72bff1fc045b8511cc89ee09 1.85kB / 1.85kB                   0.0s
 => => sha256:32888a3c745e38e72a5f49161afc7bb52a263b8f5ea1b3b4a6af537678f29491 529B / 529B                       0.0s
 => => sha256:34b4fa67dc04381e908b662ed69b3dbe8015fa723a746c66cc870a5330520981 1.46kB / 1.46kB                   0.0s
 => => sha256:918547b9432687b1e1d238e82dc1e0ea0b736aafbf3c402eea98c6db81a9cb65 55.05MB / 55.05MB                 9.7s
 => => extracting sha256:918547b9432687b1e1d238e82dc1e0ea0b736aafbf3c402eea98c6db81a9cb65                        1.8s
 => [internal] load build context                                                                                0.4s
 => => transferring context: 14.51MB                                                                             0.4s
 => [ 2/18] WORKDIR /root                                                                                        0.2s
 => [ 3/18] RUN apt update && apt install -y --force-yes opam cvc4 vim gcc clang                                99.6s
 => [ 4/18] RUN opam init --auto-setup -y --disable-sandboxing -c ocaml-base-compiler.4.12.0                   123.9s
 => [ 5/18] RUN eval $(opam env)                                                                                 0.2s 
 => [ 6/18] COPY ./ /root/                                                                                       0.2s 
 => [ 7/18] RUN opam pin -yn add easycrypt /root/easycrypt                                                       0.9s 
 => [ 8/18] RUN opam pin -yn add jasmin /root/jasmin                                                             0.9s 
 => [ 9/18] RUN opam repo add coq-released https://coq.inria.fr/opam/released && opam pin -yn add coq-mathcomp-  3.7s 
 => [10/18] RUN opam install -y depext                                                                           6.2s 
 => [11/18] RUN opam depext -y easycrypt && opam install -y easycrypt                                          137.8s 
 => [12/18] RUN opam depext -y alt-ergo.2.4.1 z3.4.8.14                                                          9.9s 
 => [13/18] RUN opam install -y alt-ergo.2.4.1 z3.4.8.14                                                       602.0s 
 => [14/18] RUN eval $(opam env) && easycrypt why3config                                                         0.4s 
 => [15/18] RUN opam depext -y jasmin && opam install -y --deps-only jasmin                                    405.5s 
 => ERROR [16/18] RUN eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make instal  2.1s 
------                                                                                                                
 > [16/18] RUN eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make install:            
#20 0.345 [WARNING] Running as root is not recommended                                                                
#20 0.351 rm -f CIL/*.ml CIL/*.mli ../proofs/extraction.vo                                                            
#20 0.352 make -C ../proofs extraction                                                                                
#20 0.353 make[1]: Entering directory '/root/jasmin/proofs'                                                           
#20 0.353 coq_makefile -f _CoqProject -o Makefile.coq
#20 0.356 rm -f lang/ocaml/*.ml lang/ocaml/*.mli
#20 0.358 rm -f lang/extraction.vo
#20 0.359 make -f Makefile.coq lang/extraction.vo
#20 0.360 make[2]: Entering directory '/root/jasmin/proofs'
#20 0.407 COQDEP VFILES
#20 0.465 *** Warning: in file 3rdparty/ssrring.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.465 *** Warning: in file arch/arch_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.466 *** Warning: in file arch/arch_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.466 *** Warning: in file arch/arch_sem.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.468 *** Warning: in file arch/spp_arch_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.468 *** Warning: in file compiler/allocation.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.470 *** Warning: in file compiler/arm_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.470 *** Warning: in file compiler/arm_instr_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.473 *** Warning: in file compiler/arm_instr_decl_lemmas.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.473 *** Warning: in file compiler/arm_lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.474 *** Warning: in file compiler/arm_lowering_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.475 *** Warning: in file compiler/arm_params_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.476 *** Warning: in file compiler/array_expansion.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.476 *** Warning: in file compiler/array_expansion_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.477 *** Warning: in file compiler/array_copy_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.480 *** Warning: in file compiler/constant_prop.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.483 *** Warning: in file compiler/lea.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.485 *** Warning: in file compiler/lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.488 *** Warning: in file compiler/propagate_inline.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.489 *** Warning: in file compiler/remove_globals.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.489 *** Warning: in file compiler/remove_globals_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.490 *** Warning: in file compiler/stack_alloc.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.491 *** Warning: in file compiler/stack_alloc_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.493 *** Warning: in file compiler/stack_alloc_proof_2.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.497 *** Warning: in file compiler/x86_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.497 *** Warning: in file compiler/x86_extra.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.498 *** Warning: in file compiler/x86_instr_decl.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.499 *** Warning: in file compiler/x86_lowering.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.500 *** Warning: in file compiler/x86_lowering_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.502 *** Warning: in file compiler/x86_params.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.502 *** Warning: in file compiler/x86_params_proof.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.503 *** Warning: in file lang/array.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.503 *** Warning: in file lang/expr.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.505 *** Warning: in file lang/gen_map.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.505 *** Warning: in file lang/global.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.506 *** Warning: in file lang/low_memory.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.507 *** Warning: in file lang/memory_model.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.509 *** Warning: in file lang/sem.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.510 *** Warning: in file lang/sem_op_typed.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.511 *** Warning: in file lang/sem_type.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.511 *** Warning: in file lang/utils.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.512 *** Warning: in file lang/values.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.514 *** Warning: in file lang/warray_.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.515 *** Warning: in file lang/word.v, library ssrZ is required from root mathcomp.word and has not been found in the loadpath!
#20 0.568 COQC 3rdparty/xseq.v
#20 0.569 COQC ssrmisc/oseq.v
#20 1.252 COQC 3rdparty/ssrring.v
#20 1.279 COQC lang/shift_kind.v
#20 1.363 COQC lang/utils.v
#20 1.649 File "./3rdparty/ssrring.v", line 10, characters 0-39:
#20 1.649 Error: Cannot find a physical path bound to logical path
#20 1.649 ssrZ with prefix mathcomp.word.
#20 1.649 
#20 1.704 make[2]: *** [Makefile.coq:793: 3rdparty/ssrring.vo] Error 1
#20 1.704 make[2]: *** Waiting for unfinished jobs....
#20 1.977 File "./lang/utils.v", line 7, characters 0-39:
#20 1.977 Error: Cannot find a physical path bound to logical path
#20 1.977 ssrZ with prefix mathcomp.word.
#20 1.977 
#20 2.049 make[2]: Leaving directory '/root/jasmin/proofs'
#20 2.049 make[2]: *** [Makefile.coq:793: lang/utils.vo] Error 1
#20 2.049 make[1]: *** [Makefile:20: extraction] Error 2
#20 2.049 make[1]: Leaving directory '/root/jasmin/proofs'
#20 2.050 make: *** [Makefile:70: CIL] Error 2
------
executor failed running [/bin/sh -c eval $(opam env) && cd /root/jasmin/compiler && make CIL -j 2 && make -j 2 && make install]: exit code: 2

[tfaoliveira]

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.

[rod-chapman]

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

[tfaoliveira]

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