Merge branch 'master' into milnes-sigmapi

.ci/corecryptotest_reduce_keysize.sh

@@ -2,8 +2,8 @@
 set -e
 
 # For CI, use keysize_small
-sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' ucontrib/CoreCrypto/ml/Tests.ml
-sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' ucontrib/CoreCrypto/ml/Tests.ml
+sed -i.bak 's/let keysize = keysize_large/let keysize = keysize_small/' contrib/CoreCrypto/ml/Tests.ml
+sed -i.bak 's/let dh_param_size = dh_param_size_large/let dh_param_size = dh_param_size_small/' contrib/CoreCrypto/ml/Tests.ml
 
-# We leave ucontrib/CoreCrypto/ml/Tests.ml modified, unstaged.
+# We leave contrib/CoreCrypto/ml/Tests.ml modified, unstaged.
 # The CI teardown will forget this happened.

.devcontainer/devcontainer.json

@@ -1,6 +1,7 @@
 {
   "name": "F* minimal devcontainer",
   "build": {
+    "context": "..",
     "dockerfile": "minimal.Dockerfile"
   },
   "customizations": {

.devcontainer/minimal.Dockerfile

@@ -1,4 +1,5 @@
-FROM ubuntu:23.10
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:22.04
 
 SHELL ["/bin/bash", "-c"]
 
@@ -16,6 +17,7 @@ RUN apt-get update \
       python3 \
       python-is-python3 \
       libgmp-dev \
+      pkg-config \
       opam \
     && apt-get clean -y
 # FIXME: libgmp-dev should be installed automatically by opam,
@@ -33,6 +35,10 @@ RUN mkdir -p $HOME/bin
 # Make sure ~/bin is in the PATH
 RUN echo 'export PATH=$HOME/bin:$PATH' | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
 
+# Install Z3
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh ~/bin
+
 # Install dotnet
 ENV DOTNET_ROOT /home/$USER/dotnet
 RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
@@ -42,17 +48,12 @@ RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a
     rm -f dotnet-sdk*.tar.gz
 
 # Install OCaml
-ARG OCAML_VERSION=4.14.0
+ARG OCAML_VERSION=4.14.2
 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
 RUN opam option depext-run-installs=true
 ENV OPAMYES=1
-RUN opam install --yes batteries zarith stdint yojson dune menhir menhirLib mtime pprint sedlex ppxlib process ppx_deriving ppx_deriving_yojson memtrace
-
-# Get compiled Z3
-RUN wget -nv https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip \
- && unzip z3-4.8.5-x64-ubuntu-16.04.zip \
- && cp z3-4.8.5-x64-ubuntu-16.04/bin/z3 $HOME/bin/z3 \
- && rm -r z3-4.8.5-*
+COPY ./fstar.opam .
+RUN opam install --deps-only . && rm fstar.opam
 
 WORKDIR $HOME
 

.docker/base.Dockerfile

@@ -8,9 +8,8 @@
 # and it is copied into the home directory on the image. CI jobs
 # will NOT use this file.
 
-# We always try to build against the most current ubuntu image.
-# FIXME: Broken with 24.04, fixing it to 23.10 so we can keep working
-FROM ubuntu:23.10
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:22.04
 
 RUN apt-get update
 
@@ -34,9 +33,14 @@ RUN apt-get install -y --no-install-recommends \
       sudo \
       python3 \
       python-is-python3 \
+      pkg-config \
       opam \
       && apt-get clean -y
 
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
+
 # Create a new user and give them sudo rights
 # NOTE: we give them the name "opam" to keep compatibility with
 # derived hierarchical CI

.docker/dev-base.Dockerfile

@@ -0,0 +1,58 @@
+FROM ubuntu:24.04
+
+RUN apt-get update
+
+RUN apt-get install -y --no-install-recommends \
+      git \
+      sudo \
+      python3 \
+      python-is-python3 \
+      opam \
+      rustc \
+      curl \
+      ca-certificates \
+      rsync \
+      wget \
+      && apt-get clean -y
+
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
+
+RUN useradd -ms /bin/bash user
+RUN echo 'user ALL=NOPASSWD: ALL' >> /etc/sudoers
+USER user
+WORKDIR /home/user
+
+# Install OCaml
+ARG OCAML_VERSION=4.14.2
+RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
+RUN opam env --set-switch | tee --append $HOME/.profile $HOME/.bashrc $HOME/.bash_profile
+RUN opam option depext-run-installs=true
+ENV OPAMYES=1
+
+# F* dependencies. This is the only place where we read a file from
+# the F* repo.
+ADD fstar.opam ./fstar.opam
+RUN opam install -j$(nproc) --confirm-level=unsafe-yes --deps-only ./fstar.opam && opam clean
+
+# Some karamel dependencies too. hex for everparse
+RUN opam install -j$(nproc) --confirm-level=unsafe-yes fix fileutils visitors camlp4 wasm ulex uucp ctypes ctypes-foreign hex && opam clean
+
+RUN sudo apt install time
+
+# Sigh, install dotnet. The setup-dotnet action does not
+# work on a container apparently.
+ENV DOTNET_ROOT /dotnet
+RUN wget -nv https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
+    sudo mkdir -p $DOTNET_ROOT && \
+    sudo tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT && \
+    rm -f dotnet-sdk*.tar.gz
+RUN sudo ln -s $DOTNET_ROOT/dotnet /usr/local/bin/dotnet
+
+RUN rm fstar.opam # move up
+
+# install rust (move up and remove rustv)
+RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
+RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends llvm-dev libclang-dev clang libgmp-dev pkg-config
+RUN . "$HOME/.cargo/env" && rustup component add rustfmt && cargo install bindgen-cli

.docker/emacs/.emacs

@@ -8,14 +8,14 @@
 
 
 ;;set fstar includes, these should work for most tutorial examples, except those using hyperheap
-(setq fstar-subp-prover-args '("--include" "/home/build/FStar/ucontrib/Platform/fst" "--include" "/home/build/FStar/ucontrib/CoreCrypto/fst"))
+(setq fstar-subp-prover-args '("--include" "/home/build/FStar/contrib/Platform/fst" "--include" "/home/build/FStar/contrib/CoreCrypto/fst"))
 
 
 ;;this is what the above corresponds to on the command line:
-;fstar --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
+;fstar --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst
 
 ;;set fstar includes, these work for the the Encrypt-then-MAC example:
-;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/ucontrib/Platform/fst" "--include" "/home/FStar/FStar/ucontrib/CoreCrypto/fst"))
+;(setq fstar-subp-prover-args '("--include" "/home/FStar/FStar/ulib/hyperheap" "--include" "/home/FStar/FStar/contrib/Platform/fst" "--include" "/home/FStar/FStar/contrib/CoreCrypto/fst"))
 
 ;;this is what the above corresponds to on the command line:
-;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/ucontrib/Platform/fst --include /home/FStar/FStar/ucontrib/CoreCrypto/fst
+;fstar --include /home/FStar/FStar/ulib/hyperheap --include /home/FStar/FStar/contrib/Platform/fst --include /home/FStar/FStar/contrib/CoreCrypto/fst

.docker/nu_base.Dockerfile

@@ -1,6 +1,7 @@
 # For check-world workflow, should be coallesced to the other base.
 # This could definitely use a big cleanup too.
-FROM ubuntu:23.10
+# FIXME: z3.4.8.5-1 can no longer be installed on Ubuntu 24.04 because python3-distutils disappeared, and the z3 opam package has not been fixed for version 4.8.5, and 23.10 and all prior non-LTS are now EOL. Reverting to the previous LTS
+FROM ubuntu:24.04
 
 RUN apt-get update
 
@@ -9,12 +10,17 @@ RUN apt-get update
 RUN apt-get install -y --no-install-recommends \
       git \
       sudo \
+      ca-certificates \
       python3 \
       python-is-python3 \
       opam \
       rustc \
       && apt-get clean -y
 
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN get_fstar_z3.sh /usr/local/bin
+
 # Create a new user and give them sudo rights
 # NOTE: we give them the name "opam" to keep compatibility with
 # derived hierarchical CI
@@ -27,18 +33,6 @@ ENV HOME /home/opam
 WORKDIR $HOME
 SHELL ["/bin/bash", "--login", "-c"]
 
-# Install GitHub CLI
-# From https://github.com/cli/cli/blob/trunk/docs/install_linux.md#debian-ubuntu-linux-raspberry-pi-os-apt
-# This is only used by the workflow that makes a release and publishes
-# it, but no harm in having it in the base.
-RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \
-    && curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg | sudo dd of=/usr/share/keyrings/githubcli-archive-keyring.gpg \
-    && sudo chmod go+r /usr/share/keyrings/githubcli-archive-keyring.gpg \
-    && echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" | sudo tee /etc/apt/sources.list.d/github-cli.list > /dev/null \
-    && sudo apt-get update \
-    && sudo apt-get install gh -y \
-    && sudo apt-get clean
-
 # Install OCaml
 ARG OCAML_VERSION=4.14.2
 RUN opam init --compiler=$OCAML_VERSION --disable-sandboxing
@@ -49,6 +43,7 @@ ENV OPAMYES=1
 # F* dependencies. This is the only place where we read a file from
 # the F* repo.
 ADD fstar.opam $HOME/fstar.opam
+
 RUN opam install --confirm-level=unsafe-yes --deps-only $HOME/fstar.opam && opam clean
 
 # Some karamel dependencies

.docker/release.Dockerfile

@@ -4,7 +4,7 @@
 ARG ocaml_version=4.14
 ARG CI_THREADS=24
 
-FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version AS fstarbuild
+FROM ocaml/opam:ubuntu-22.04-ocaml-$ocaml_version AS fstarbuild
 
 # Needed for OPAM command below
 RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
@@ -15,11 +15,12 @@ RUN opam depext conf-gmp conf-m4
 
 ADD --chown=opam:opam ./fstar.opam fstar.opam
 
-# Install opam dependencies only, but not z3
-RUN grep -v z3 < fstar.opam > fstar-no-z3.opam && \
-    rm fstar.opam && \
-    opam install --deps-only ./fstar-no-z3.opam && \
-    rm fstar-no-z3.opam
+# Install opam dependencies only
+RUN opam install --deps-only ./fstar.opam
+
+# Install the relevant Z3 versions.
+COPY ./bin/get_fstar_z3.sh /usr/local/bin
+RUN sudo get_fstar_z3.sh /usr/local/bin
 
 # Install GitHub CLI
 # From https://github.com/cli/cli/blob/trunk/docs/install_linux.md#debian-ubuntu-linux-raspberry-pi-os-apt
@@ -32,7 +33,7 @@ RUN { type -p curl >/dev/null || sudo apt-get install curl -y ; } \
 
 # Install .NET
 RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
-  libicu66
+  libicu70
 
 # (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
 # CI dependencies: .NET Core
@@ -52,11 +53,6 @@ ENV PATH=${PATH}:$DOTNET_ROOT:$DOTNET_ROOT/tools
 RUN git config --global user.name "Dzomo, the Everest Yak" && \
     git config --global user.email "[email protected]"
 
-# Download and extract z3, but do not add it in the PATH
-# We download a z3 that does not depend on libgomp
-ADD --chown=opam:opam https://github.com/tahina-pro/z3/releases/download/z3-4.8.5-linux-clang/z3-4.8.5-linux-clang-x86_64.tar.gz z3.tar.gz
-RUN tar xf z3.tar.gz
-
 ADD --chown=opam:opam ./ FStar/
 
 # Check if we need to create a tag
@@ -66,7 +62,7 @@ RUN --mount=type=secret,id=DZOMO_GITHUB_TOKEN eval $(opam env) && env GH_TOKEN=$
 RUN eval $(opam env) && env OTHERFLAGS='--admit_smt_queries true' PATH=$HOME/z3:$PATH make -j $CI_THREADS -C FStar package
 
 # Test the package with its Z3, without OCaml or any other dependency
-FROM ubuntu:20.04 AS fstarnoocaml
+FROM ubuntu:22.04 AS fstarnoocaml
 
 # Install some dependencies
 RUN apt-get update && \

.docker/standalone.Dockerfile

@@ -19,7 +19,7 @@ ARG CI_BRANCH=master
 ARG CI_NO_KARAMEL=
 ARG RESOURCEMONITOR=
 ARG FSTAR_CI_NO_GITDIFF=
-RUN eval $(opam env) && Z3_LICENSE="$(opam config expand '%{prefix}%')/.opam-switch/sources/z3.4.8.5/LICENSE.txt" CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH
+RUN eval $(opam env) && CI_NO_KARAMEL=$CI_NO_KARAMEL .docker/build/build-standalone.sh $CI_THREADS $CI_BRANCH
 
 WORKDIR $HOME
 ENV FSTAR_HOME $HOME/FStar