Docker development image

Setting up a development environment with Coq can take some time. We have prepared a Docker image one can use for development of eLyKseeR and running proofs in Coq for formal verification of the system. This also gives us a stable environment to run reproducible tests.

The image also contains an OCaml compiler with all necessary libraries preinstalled. So it allows to extract code from Coq to OCaml and compile the command line programs.

Versions installed:

• coq 8.18.0
• ocaml 5.1.1

Visit Docker Hub: https://hub.docker.com/r/codieplusplus/elykseer-ml

Docker

Pull the image

There are images for Intel/AMD CPUs:

docker pull codieplusplus/elykseer-ml:amd64

or, ARM (aarch64) processors like on the newer Macs M[123]:

docker pull codieplusplus/elykseer-ml:arm64

Running an eLyKseeR container

Let's start with running a container that will not be persisted after we leave it:

docker run -it --rm codieplusplus/elykseer-ml:arm64

We are located in the checkout of the project where we can run git commands:

coq@9f37ae23a26b:~/elykseer-ml.git$ git fetch
remote: Enumerating objects: 19, done.
remote: Counting objects: 100% (19/19), done.
remote: Compressing objects: 100% (8/8), done.
remote: Total 19 (delta 11), reused 19 (delta 11), pack-reused 0
Unpacking objects: 100% (19/19), 4.82 KiB | 329.00 KiB/s, done.
From https://github.com/eLyKseeR/elykseer-ml
   dffe907..1425c92  main              -> origin/main

A run with Coq to verify the program:

coq@9f37ae23a26b:~/elykseer-ml.git$ make clean
CLEAN
coq@9f37ae23a26b:~/elykseer-ml.git$ make
COQDEP VFILES
COQC theories/Cstdio.v
COQC theories/Filesystem.v
COQC theories/Conversion.v
COQC theories/Nchunks.v
COQC theories/Configuration.v
COQC theories/Filesupport.v
COQC theories/Utilities.v
COQC theories/Assembly.v
COQC theories/Store.v
COQC theories/Environment.v
COQC theories/AssemblyCache.v
COQC theories/Processor.v
COQC theories/Version.v
COQC theories/MakeML.v

If no error is output, then this is a good sign and proof that everything is validated. This also extracted the OCaml code which we now compile and install to be able to execute the programs.

dune build && dune install --prefix ${HOME}/.local

Run tests

Now, we change to the home directory and prepare the setup for testing:

coq@9f37ae23a26b:~/elykseer-ml.git$ cd

coq@9f37ae23a26b:~$ ./setup.sh 
mkdir: created directory '/home/coq/elykseer.chunks'
mkdir: created directory '/home/coq/elykseer.db'

all setup.

The test run uses files of size 1, 4, and 8 megabytes consisting of random data. It will first create a backup of these, which will output a number of chunks files in the directory elykseer.chunks and meta data in elykseer.db . Then, it restores them and compares their checksums to the one of the original file.

coq@9f37ae23a26b:~$ ./run_test.sh 
1+0 records in
1+0 records out
1048576 bytes (1.0 MB, 1.0 MiB) copied, 0.00975533 s, 107 MB/s
4+0 records in
4+0 records out
4194304 bytes (4.2 MB, 4.0 MiB) copied, 0.0218318 s, 192 MB/s
8+0 records in
8+0 records out
8388608 bytes (8.4 MB, 8.0 MiB) copied, 0.0268092 s, 313 MB/s
test1M: OK
test4M: OK
test8M: OK
done.
get fchecksum: d4a2d5ce52f8675cbdebaaf13bbc6f41e5d5ebc3d200a0c3899d4017eaf644be
get fblocks: d4a2d5ce52f8675cbdebaaf13bbc6f41e5d5ebc3d200a0c3899d4017eaf644be
get fchecksum: 21994160f4af06b068e408585ad1f84bcf743455fed4d5ebfc50ee3d74672cec
get fblocks: 21994160f4af06b068e408585ad1f84bcf743455fed4d5ebfc50ee3d74672cec
get fchecksum: 7f4c347c34d4aafc55e23eb5642e0311dff57d92122b5e91d573c3f4882b1c31
get fblocks: 7f4c347c34d4aafc55e23eb5642e0311dff57d92122b5e91d573c3f4882b1c31
FILE 7f4c347c34d4aafc55e23eb5642e0311dff57d92122b5e91d573c3f4882b1c31
  restoring 4194304 bytes in file 'test4M' from 128 blocks
     -> 4194304 bytes
  restoring 8388608 bytes in file 'test8M' from 256 blocks
     -> 8388608 bytes
  restoring 1048576 bytes in file 'test1M' from 32 blocks
     -> 1048576 bytes
  restored 3 files with 13631488 bytes in total
test1M: OK
test4M: OK
test8M: OK

Done.