# -*- coding: utf-8; mode: tcl; tab-width: 4; indent-tabs-mode: nil; c-basic-offset: 4 -*- vim:fenc=utf-8:ft=tcl:et:sw=4:ts=4:sts=4

PortSystem          1.0
PortGroup github    1.0
PortGroup ocaml     1.1

name                ocaml-hacl-star
github.setup        project-everest hacl-star 4b197eb54b41056e6c051f0162cf57a50ad5b380
version             20210824-[string range ${github.version} 0 6]
revision            1

categories          ocaml devel security
maintainers         {landonf @landonf} openmaintainer
license             Apache-2
description         High-assurance cryptographic library.
long_description    Formally verified library of modern cryptographic algorithms, \
                    including Curve25519, Ed25519, AES-GCM, Chacha20, Poly1305, SHA-2, \
                    SHA-3, HMAC, and HKDF. The code for all of these algorithms is \
                    formally verified using the F* verification framework for memory \
                    safety, functional correctness, and secret independence (resistance \
                    to some types of timing side-channels).

platforms           darwin

options             vale.version vale.distname vale.distfile
options             hacl-star.make_args

vale.version        0.3.16
vale.distname       vale-release-${vale.version}
vale.distfile       ${vale.distname}.zip

master_sites-append https://github.com/project-everest/vale/releases/download/v${vale.version}/:bootstrap
distfiles-append    ${vale.distfile}:bootstrap

patchfiles          patch-Makefile.diff \
                    patch-dist-configure-use-gmktemp \
                    patch-dist-gcc-compatible-use-install_name

checksums           ${distname}${extract.suffix} \
                    rmd160  1e42daa92a9857126839c67d03e6d2f801f30cd6 \
                    sha256  c9055c3a73ca8bc5308b5fea2be3431c2e762fb65da077c5ef6066832411b6d5 \
                    size    8962430 \
                    ${vale.distfile} \
                    rmd160  32eeb48eb90ce19703175904f600bc4d94973cbc \
                    sha256  1bb1af63258c1e8dad7431b259d09480d07d345b386d52262f63f9e119faf4cd \
                    size    3072558

extract.only        ${distname}${extract.suffix}

post-extract {
    set tar [findBinary tar ${portutil::autoconf::tar_command}]
    system -W ${worksrcpath}/vale "${tar} -C ${worksrcpath} -zxf ${distpath}/${vale.distfile}"
}

depends_build       port:gmake \
                    port:mono \
                    path:libexec/coreutils/libstdbuf.so:coreutils \
                    port:gtime \
                    port:gsed

depends_lib         port:fstar \
                    port:kremlin

# Required to build the ocaml-hacl-star bindings
subport ocaml-hacl-star-raw {
    ocaml.use_findlib   yes
    use_configure       no

    depends_build-append port:python38
    depends_lib-append  port:ocaml-ctypes

    # Common make arguments
    hacl-star.make_args HACL_HOME="${worksrcpath}" \
                        FSTAR_HOME="${prefix}/libexec/fstar/home" \
                        KREMLIN_HOME="${prefix}/libexec/kremlin/home" \
                        VALE_HOME="${worksrcpath}/${vale.distname}" \
                        OPENSSL_HOME="${prefix}/lib" \
                        PYTHON3="${prefix}/bin/python3.8"

    build.cmd           ${prefix}/bin/gmake
    build.args-append   {*}${hacl-star.make_args}

    # XXX: Avoid hitting SMT verification rlimit on macOS
    build.args-append   OTHERFLAGS="--z3rlimit_factor 32"

    destroot.dir        ${worksrcpath}/dist/gcc-compatible
    destroot.target     install-hacl-star-raw
    destroot.args-append {*}${hacl-star.make_args}
}

subport ocaml-hacl-star {
    depends_lib-append      port:ocaml-hacl-star-raw \
                            port:ocaml-zarith

    depends_build-append    port:ocaml-cppo

    ocaml.build_type        dune
    dune.root               ${worksrcpath}/bindings/ocaml
}