Skip to content

eLyKseeR/elykseer-ml

Repository files navigation

Preparations

0.) if not yet done: opam init -a --bare

1.) create a compiler switch: opam switch create 5.1.1

Coq version used

opam pin add coq 8.18.0

more packages

opam repo add coq-released https://coq.inria.fr/opam/released

see the Dockerfile which other packages are installed.

Code generation

  1. create Coq's Makefile coq_makefile -f _CoqProject -o Makefile

  2. run proofs in Coq and extract ML code: make

  3. build library: dune build

  4. build and run executable (shows help): dune exec lxr_backup -- -h

Dependencies

Docker image

(in the following commands replace arm64 with amd64 if run on x86-64)

either build the image locally:

cd docker
DOCKER_BUILDKIT=1 docker build -t codieplusplus/elykseer-ml.arm64:local .

or, download it from Docker Hub:

docker pull codieplusplus/elykseer-ml.arm64:latest

run the image:

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

(one can also attach a local Visual Code editor to this container; install extensions "VsCoq" and "OCaml Platform" for source code highlighting)

experimenting with multiarch building

The images are available for Linux/amd64 and Linux/arm64 on Docker hub.

docker buildx build --platform linux/amd64,linux/arm64 -t codieplusplus/elykseer-ml:latest --push .

Executables

Backup

lxr_backup - backup files indicated on the command line to LXR

lxr_backup: vyxdnji
  -v verbose output
  -y dry run
  -x sets output path for encrypted chunks
  -d sets database path
  -n sets number of chunks (16-256) per assembly
  -j sets number of parallel processes
  -i sets own identifier
  -help  Display this list of options
  --help  Display this list of options
example

This examples assumes that an irmin database exists at path /data/elykseer.db. Create here a file irmin.yml with content:

root: /data/elykseer.db
store: git
contents: json-value

and initialise: irmin init

Moreover, the environment variable $MYID contains a unique string to distinguish between setups.

MYID="424242"

backup three files:

dune exec lxr_backup -- -v -x /data/elykseer.chunks -d /data/elykseer.db -n 16 -i $MYID ./test1M ./test4M ./test8M

compute file hash:

FHASH=$(./_build/default/bin/lxr_filehash.exe -f ./test1M)

get block meta data for this file as CSV output:

irmin get ${MYID}/relfiles/${FHASH:4:2}/${FHASH} | jq -r '
  .blocks[] | [.blockaid,.blockapos,.filepos,.blocksize] | @csv' | awk "{print \"${FHASH},\"\$0}"

lists:

86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","0","0","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","131072","131072","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","262144","262144","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","393216","393216","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","524288","524288","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","655360","655360","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","786432","786432","131072"
86b16ef62a8334325e612629cf25b26a77aaa0a59f50024ba9be5b3eb64d90b5,"0fd37df6acbce4a3c99a89161ce7f629aab205cac51cc71126dca0540c4ce437","917504","917504","131072"
Restore

lxr_restore - restore file(s) from LXR

lxr_restore: vxodnji
  -v verbose output
  -x sets path for encrypted chunks
  -o sets output path for restored files
  -d sets database path
  -n sets number of chunks (16-256) per assembly
  -j sets number of parallel processes
  -i sets own identifier
  -help  Display this list of options
  --help  Display this list of options
example
./_build/default/bin/lxr_restore.exe -v -x /data/elykseer.chunks -d /data/elykseer.db -o /tmp/ -i $MYID test4M test8M

outputs:

  restoring 8388607 bytes in file 'test8M' from 64 blocks
+✅ 'test8M'    restored with 8388607 bytes in total
  restoring 4194304 bytes in file 'test4M' from 32 blocks
+✅ 'test4M'    restored with 4194304 bytes in total
  restored 2 files with 12582911 bytes in total

The files were extracted to /tmp/ and can be compared with: md5sum /tmp/test4M test4M /tmp/test8M test8M

83b1a2506a5d1a50dd645ac59c35d147  /tmp/test4M
83b1a2506a5d1a50dd645ac59c35d147  test4M
e4379d58904294ab7ab6431191cd9801  /tmp/test8M
e4379d58904294ab7ab6431191cd9801  test8M
Verify

lxr_compare - compare file(s) against backuped blocks in LXR

lxr_compare: vdi
  -v verbose output
  -d sets database path
  -i sets own identifier
  -help  Display this list of options
  --help  Display this list of options
example
./_build/default/bin/lxr_compare.exe -v -d /data/elykseer.db -i $MYID ./test4M

outputs:

comparing file ./test4M against meta data
 +✅ block 1@0=131072
 +✅ block 2@131072=131072
 +✅ block 3@262144=131072
 +✅ block 4@393216=131072
 +✅ block 5@524288=131072
 +✅ block 6@655360=131072
 +✅ block 7@786432=131072
 +✅ block 8@917504=131072
 +✅ block 9@1048576=131072
 +✅ block 10@1179648=131072
 +✅ block 11@1310720=131072
 +✅ block 12@1441792=131072
 +✅ block 13@1572864=131072
 +✅ block 14@1703936=131072
 +✅ block 15@1835008=131072
 +✅ block 16@1966080=131072
 +✅ block 17@2097152=131072
 +✅ block 18@2228224=131072
 +✅ block 19@2359296=131072
 +✅ block 20@2490368=131072
 +✅ block 21@2621440=131072
 +✅ block 22@2752512=131072
 +✅ block 23@2883584=131072
 +✅ block 24@3014656=131072
 +✅ block 25@3145728=131072
 +✅ block 26@3276800=131072
 +✅ block 27@3407872=131072
 +✅ block 28@3538944=131072
 +✅ block 29@3670016=131072
 +✅ block 30@3801088=131072
 +✅ block 31@3932160=131072
 +✅ block 32@4063232=131072
comparison of 1 file with 1 equal