Hacspec lib files

proof-libs/coq/ssprove/.gitignore

@@ -0,0 +1,8 @@
+*.vo*
+*.aux
+*.glob
+*.cache
+.Makefile.d
+Makefile
+Makefile.conf
+src/_temp/

proof-libs/coq/ssprove/README.md

@@ -0,0 +1,30 @@
+## Dependencies
+
+The coq libraries uses `ssprove/jasmin` for machine signed and unsigned integer modulo arithmetic, and `coqword` for finite field arithmetic on prime modulus (to support hacspec's `nat_mod p` type).
+This requires the following repository:
+
+```
+opam repo add coq-released https://coq.inria.fr/opam/released --all-switches
+```
+
+Then one can install the dependencies through `opam` (assuming you have coq installed through opam)
+
+```
+opam update
+opam install conf-ppl.1 -y
+opam install coq-mathcomp-word.2.0 -y
+opam pin jasmin https://github.com/SSProve/ssprove.git#3d40bc89 -y
+opam pin ssprove https://github.com/SSProve/ssprove.git#bead4e76acbb69b3ecf077cece56cd3fbde501e3 -y
+opam upgrade -y
+```
+the development uses the Jasmin branch of SSProve, meaning one might need to install these from source.
+
+## Docker
+
+There is a docker container with the dependencies installed (Coq / Rust) at `ghcr.io/cmester0/hacspec_ssprove:8.15.2`.
+
+## Compiling the coq files
+
+In folder `/coq_ssprove`, type `make`. This compiles the coq libraries and the compiled examples, as defined in `_CoqProject`.
+
+If you want to add a new example to `_CoqProject`, such that it is compiled through `make`, you should run `coq_makefile -f _CoqProject -o Makefile` in `/coq` to update the makefile.

proof-libs/coq/ssprove/_CoqProject

@@ -0,0 +1,20 @@
+-R src/ Hacspec
+-arg -w
+-arg all
+
+src/Hacspec_Lib_Comparable.v
+src/LocationUtility.v
+src/ChoiceEquality.v
+src/Hacspec_Lib_Pre.v
+src/Hacspec_Lib.v
+
+# src/Hacspec_Aes_Jazz.v
+# src/Hacspec_Xor.v
+
+# src/Hacspec_Aes.v
+# src/Hacspec_Bls12_381.v
+# src/Hacspec_Poly1305.v
+# src/Hacspec_Curve25519.v
+# src/Hacspec_Gf128.v
+# src/Hacspec_P256.v
+# src/Hacspec_Sha256.v

proof-libs/coq/ssprove/coq-hacspec-ssprove.opam

@@ -0,0 +1,21 @@
+opam-version: "2.0"
+name: "coq-hacspec-ssprove"
+version: "dev"
+synopsis: "Hacspec coq library"
+maintainer: "Lasse Letager Hansen <[email protected]>"
+authors: ["Lasse Letager Hansen <[email protected]>"]
+homepage: "https://github.com/hacspec/hacspec"
+bug-reports: "https://github.com/hacspec/hacspec/issues"
+depends: [
+  "ssprove" {= "dev"}
+  "jasmin" {= "dev"}
+  "coq" {>= "8.15.2"}
+]
+build: [
+  ["coq_makefile" "-f" "_CoqProject" "-o" "Makefile"]
+  [make "clean"]
+  [make "-j%{jobs}%"]
+]
+install: [
+  [make "install"]
+]

proof-libs/coq/ssprove/docker_build/Dockerfile

@@ -0,0 +1,28 @@
+FROM coqorg/coq:8.15.2-ocaml-4.14.0-flambda
+RUN curl https://sh.rustup.rs -sSf | sh -s -- -y
+ENV PATH $HOME/.cargo/bin:$PATH
+RUN rustup update
+RUN rustup toolchain install nightly-2022-07-04
+RUN rustup component add --toolchain nightly-2022-07-04 rustc-dev llvm-tools-preview rust-analysis rust-src
+RUN rustc --version
+RUN cargo --version
+RUN sudo apt-get update
+RUN sudo apt-get install libppl-dev -y
+RUN sudo apt-get install libmpfr-dev -y
+RUN opam update
+RUN opam switch create 4.12.0
+RUN eval $(opam env --switch=4.12.0)
+RUN opam config list; opam repo list; opam list
+RUN opam repo add coq-released https://coq.inria.fr/opam/released --all-switches
+RUN opam update
+RUN opam pin coq 8.15.2 -y
+RUN eval $(opam env)
+RUN git clone https://github.com/jasmin-lang/jasmin.git
+RUN git clone https://github.com/SSProve/ssprove.git
+RUN cd jasmin && git checkout 3d40bc89 && cd ..
+RUN opam install -y --verbose ./jasmin/. --working-dir
+RUN eval $(opam env)
+RUN cd ssprove && git checkout jasmin && cd ..
+RUN opam upgrade -y
+RUN (opam install -y --verbose ./ssprove/ssprove.opam --working-dir) || echo "failed"
+RUN cd ssprove && make -j7 && opam install -y --verbose ./ssprove.opam --working-dir --assume-built