Merge branch '_taramana_release'

.github/setup-macos.sh

@@ -3,7 +3,7 @@
 # Install OCaml and other GNU build tools
 # coreutils: for the `install` command used in install-ulib.sh
 export OPAMYES=1
-brew install opam bash gnu-getopt coreutils gnu-sed
+brew install opam bash gnu-getopt coreutils gnu-sed make
 opam init --compiler=4.12.0
 eval $(opam env)
 

.github/workflows/linux-build.yaml

@@ -4,14 +4,22 @@ on:
 jobs:
   build:
     runs-on: [self-hosted, linux, X64]
-    defaults:
-      run:
-        # Setting the default shell to bash. This is not only more standard,
-        # but also makes sure that we run with -o pipefail, so we can safely
-        # pipe data (such as | tee LOG) without missing out on failures
-        # and getting false positives. If you want to change the default shell,
-        # keep in mind you need a way to handle this.
-        shell: bash
     steps:
       - name: Check out repo        
         uses: actions/checkout@v2
+      - name: Identify the base FStar branch and the notification channel
+        run: |
+          echo "FSTAR_BRANCH=$(jq -c -r '.BranchName' .docker/build/config.json)" >> $GITHUB_ENV
+      - name: Build Steel and its dependencies
+        run: |
+          ci_docker_image_tag=steel:local-binary-run-$GITHUB_RUN_ID-$GITHUB_RUN_ATTEMPT
+          docker buildx build --secret id=DZOMO_GITHUB_TOKEN -t $ci_docker_image_tag -f src/ci/package.Dockerfile --build-arg FSTAR_BRANCH=$FSTAR_BRANCH --build-arg CI_BRANCH=$GITHUB_REF_NAME .
+          docker run $ci_docker_image_tag /bin/bash -c 'cat $STEEL_HOME/src/ci/steel.tar.gz || true' > steel.tar.gz
+          gunzip steel.tar.gz
+        env:
+          DZOMO_GITHUB_TOKEN: ${{ secrets.DZOMO_GITHUB_TOKEN }}
+      - name: Archive Steel package
+        uses: actions/upload-artifact@v3
+        with:
+          name: steel.tar
+          path: steel.tar

.github/workflows/macos-build.yml

@@ -14,3 +14,23 @@ jobs:
       uses: actions/checkout@v3
       with:
         path: steel
+    - name: Checkout everest
+      uses: actions/checkout@v3
+      with:
+        repository: project-everest/everest
+        path: steel/.github/everest
+    - name: Install .NET SDK
+      uses: actions/setup-dotnet@v3
+      with:
+        dotnet-version: '6.0.x'
+    - name: Setup dependencies
+      run: ./steel/.github/setup-macos.sh
+    - name: Package Steel
+      run: |
+        source steel/.github/env.sh
+        steel/src/ci/package.sh -j
+    - name: Upload artifact
+      uses: actions/upload-artifact@v3
+      with:
+        name: steel-Darwin_x86_64.tar.gz
+        path: steel/src/ci/steel.tar.gz

.gitignore

@@ -12,6 +12,7 @@ lib/steel/META
 lib/steel/dune-package
 *.krml
 *.o
+LICENSE-z3.txt
 
 # Created by CI
 BUILDLOG

pulse2rust/src/.gitignore

@@ -0,0 +1 @@
+_build

pulse2rust/src/ocaml/Cargo.toml

@@ -7,7 +7,7 @@ authors = ["Aseem Rastogi"]
 edition = "2018"
 
 [lib]
-crate-type = ["staticlib", "cdylib"]
+crate-type = ["staticlib"]
 path = "rust/src/lib.rs"
 
 [dependencies]

pulse2rust/src/ocaml/dune

@@ -7,7 +7,7 @@
   (no-infer
    (progn
     (run cargo build)
-    (run cp target/debug/deps/librustast_bindings.a ./librustast_bindings.a)
+    (run cp target/debug/librustast_bindings.a ./librustast_bindings.a)
    ))))
 
 (executable

share/steel/examples/pulse/Makefile

@@ -43,3 +43,28 @@ CBOR_CHECKED_FILES=$(filter $(CACHE_DIRECTORY)/CBOR.% $(CACHE_DIRECTORY)/CDDL.%
 
 .PHONY: cbor
 cbor: lib $(CBOR_CHECKED_FILES)
+
+PREFIX ?= /usr/local
+ifeq ($(OS),Windows_NT)
+  STEEL_INSTALL_PREFIX=$(shell cygpath -m $(PREFIX))
+else
+  STEEL_INSTALL_PREFIX=$(PREFIX)
+endif
+export STEEL_INSTALL_PREFIX
+
+ifeq (,$(INSTALL))
+  INSTALL := $(shell ginstall --version 2>/dev/null | cut -c -8 | head -n 1)
+  ifdef INSTALL
+     INSTALL := ginstall
+  else
+     INSTALL := install
+  endif
+  export INSTALL
+endif
+
+.PHONY: install-lib %.install
+
+%.install: %
+	$(INSTALL) -m 644 -D $< $(STEEL_INSTALL_PREFIX)/share/steel/examples/pulse/$<
+
+install-lib: $(addsuffix .install,$(PULSE_LIB_CHECKED_FILES) $(wildcard lib/*.fst lib/*.fsti))

src/ci/.gitignore

@@ -0,0 +1,3 @@
+steel
+steel.zip
+steel.tar.gz

src/ci/package-README.md

@@ -0,0 +1,84 @@
+# The Steel and Pulse separation logic system for F*
+
+## Contents of this package
+
+This binary package contains z3 4.8.5, F*, Karamel, Steel, Pulse, and
+(except on Windows) Pulse2Rust:
+
+* in `bin`: the executables for z3, F* and Karamel
+
+* in `lib/steel`:
+  * the Steel F* modules of the `Steel` and `Steel.ST` namespaces
+  * the Steel F* plugin, `steel.cmxs`, containing the Steel and Pulse
+    tactics, and the Steel and SteelC extraction to krml, is installed
+    here
+  * the LibSteel C library, `libsteel.a`, containing an implementation of
+    what used to be the Steel part of krmllib (currently binding the
+    pthreads spinlock), is installed here
+
+* in `lib/steel/runtime`: the Steel OCaml runtime,
+  `steel_runtime.cmxa`, necessary to compile and run Steel code
+  extracted to OCaml, is installed here
+
+* in `lib/steel/pulse`: the Pulse F* modules of the `Pulse` namespace
+  (except `Pulse.Lib`)
+
+* in `lib/steel/c`: the SteelC F* modules of the `Steel.C` and
+  `Steel.ST.C` namespaces
+
+* in `include/steel`: the C include files necessary to compile Steel
+  code extracted to C
+
+* in `share/steel`: `Makefile.include`, the GNU Make rules to verify
+  Steel and Pulse code
+
+* in `share/steel/examples/pulse`:
+  * in `lib`: the Pulse user library files (namespace `Pulse.Lib`)
+  * in `_output/cache`: the corresponding `.checked` files
+
+* in `pulse2rust`: the executable for Pulse2Rust. (Absent from the
+  Windows binary package)
+
+## Using Steel and Pulse
+
+### Writing a Makefile to verify Steel or Pulse code
+
+Steel and Pulse come with `share/steel/Makefile.include`, which contains the
+GNU Make rules to call F* with the Steel include path and the Steel/Pulse
+plugin loaded.
+
+1. Make sure the `bin` subdirectory is in your `PATH`.
+
+2. Define the `STEEL_HOME` environment variable to the root directory
+   of this package.
+
+3. (Optional) In your Makefile, define the following variables with `+=` or `:=` :
+   * `FSTAR_FILES`: some more F* files to verify, in addition to the
+     `*.fst` and `.fsti` files of your project
+   * `EXCLUDE_FILES`: some F* to skip for verification
+   * `FSTAR_OPTIONS`: additional options to pass to F*. While
+     `Makefile.include` is already configured to use Steel, you need
+     to add more options if you need Pulse and/or SteelC:
+     * if you want to use Pulse, add `--include $STEEL_HOME/lib/steel/pulse`
+     * if you want to use SteelC, add `--include $STEEL_HOME/lib/steel/c`
+   * `FSTAR_DEP_OPTIONS`: additional options to pass to F* to compute
+     dependencies (in addition to `FSTAR_OPTIONS`), such as `--extract`
+   * `FSTAR_ML_CODEGEN`: useful only if you want to extract OCaml
+     code. If you want to extract a F* plugin, set this option to
+     `Plugin`. Otherwise, it is set by default to `OCaml`.
+
+4. After those variable definitions, insert `include
+   $STEEL_HOME/share/steel/Makefile.include` to your Makefile.
+
+5. In your project directory, run `make -j verify`
+
+### Calling F* directly
+
+If you already have an existing `Makefile` for your Steel- or
+Pulse-based project, you now need to pass new options to your Makefile
+to use Steel from this repository, as described in this section.
+
+To call F* with Steel or Pulse, pass the following options to F*:
+* in all cases, `--include $STEEL_HOME/lib/steel --load_cmxs steel`
+* if you want to use Pulse, add `--include $STEEL_HOME/lib/steel/pulse`
+* if you want to use SteelC, add `--include $STEEL_HOME/lib/steel/c`

src/ci/package.Dockerfile

@@ -0,0 +1,62 @@
+# This Dockerfile should be run from the root Steel directory
+
+ARG ocaml_version=4.12
+FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version
+
+# CI dependencies for the Wasm11 test: node.js
+RUN curl -fsSL https://deb.nodesource.com/setup_16.x | sudo -E bash -
+RUN sudo apt-get install -y --no-install-recommends nodejs
+
+# install rust
+RUN curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y
+
+ARG opamthreads=24
+
+# (for .NET, cf. https://aka.ms/dotnet-missing-libicu )
+# CI dependencies: .NET Core
+# Repository install may incur some (transient?) failures (see for instance https://github.com/dotnet/sdk/issues/27082 )
+# So, we use manual install instead, from https://docs.microsoft.com/en-us/dotnet/core/install/linux-scripted-manual#manual-install
+ENV DOTNET_ROOT /home/opam/dotnet
+RUN sudo apt-get install --yes --no-install-recommends \
+    libicu-dev \
+    wget \
+    && \
+    wget https://download.visualstudio.microsoft.com/download/pr/cd0d0a4d-2a6a-4d0d-b42e-dfd3b880e222/008a93f83aba6d1acf75ded3d2cfba24/dotnet-sdk-6.0.400-linux-x64.tar.gz && \
+    mkdir -p $DOTNET_ROOT && \
+    tar xf dotnet-sdk-6.0.400-linux-x64.tar.gz -C $DOTNET_ROOT
+
+ENV PATH=${PATH}:$DOTNET_ROOT:$DOTNET_ROOT/tools
+
+ADD --chown=opam:opam ./ steel/
+
+# Install F* and Karamel from the Karamel CI install script
+# FIXME: the `opam depext` command should be unnecessary with opam 2.1
+ENV FSTAR_HOME=$HOME/FStar
+ENV KRML_HOME=$HOME/karamel
+RUN sudo apt-get update && sudo apt-get install --yes --no-install-recommends \
+    wget \
+    jq \
+    && \
+    git clone --branch $(jq -c -r '.RepoVersions.fstar' steel/src/ci/config.json || echo master) https://github.com/FStarLang/FStar $FSTAR_HOME && \
+    eval $(opam env) && \
+    opam depext conf-gmp z3.4.8.5-1 conf-m4 && \
+    opam install --deps-only $FSTAR_HOME/fstar.opam && \
+    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads && \
+    git clone --branch $(jq -c -r '.RepoVersions.karamel' steel/src/ci/config.json || echo master) https://github.com/FStarLang/karamel $KRML_HOME && \
+    eval $(opam env) && $KRML_HOME/.docker/build/install-other-deps.sh && \
+    env OTHERFLAGS='--admit_smt_queries true' make -C $KRML_HOME -j $opamthreads
+
+# FIXME: The recent changes to MLish and bootstrapping mean that we must
+# not try to check prims.fst or the rest of ulib in --MLish mode, since
+# some files fail to do so. This will happen when trying to extract the
+# files in src/syntax_extension, as there are no checked files for them.
+# So, call the F* makefile to bootstrap F* and generate the files. This
+# is probably only a bandaid... but I'm not sure what the best thing to
+# do is.
+RUN eval $(opam env) && \
+    env OTHERFLAGS='--admit_smt_queries true' make -C $FSTAR_HOME -j $opamthreads bootstrap
+
+# Produce the binary package
+RUN eval $(opam env) && . $HOME/.cargo/env && steel/src/ci/package.sh -j $opamthreads
+
+ENV STEEL_HOME $HOME/steel

src/ci/package.sh

@@ -0,0 +1,93 @@
+#!/usr/bin/env bash
+
+set -e
+set -x
+
+if [[ -z "$OS" ]] ; then
+    OS=$(uname)
+fi
+
+is_windows=false
+if [[ "$OS" = "Windows_NT" ]] ; then
+   is_windows=true
+fi
+
+fixpath () {
+    if $is_windows ; then
+        cygpath -m "$1"
+    else
+        echo "$1"
+    fi
+}
+
+cp0=$(which gcp >/dev/null 2>&1 && echo gcp || echo cp)
+cp="$cp0 --preserve=mode,timestamps"
+make="$(which gmake >/dev/null 2>&1 && echo gmake || echo make)"
+
+# make sure the package has not already been built
+cd $(cd `dirname $0` && pwd)
+[[ ! -e steel ]]
+
+# download the z3 license file
+if ! [[ -f LICENSE-z3.txt ]] ; then
+    curl -o LICENSE-z3.txt https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt
+fi
+
+# build a F* package
+if [[ -z "$FSTAR_HOME" ]] ; then
+   if ! [[ -d FStar ]] ; then
+       git clone https://github.com/FStarLang/FStar
+   fi
+   FSTAR_HOME=$(pwd)/FStar
+fi
+export FSTAR_HOME=$(fixpath "$FSTAR_HOME")
+old_FSTAR_HOME="$FSTAR_HOME"
+fstar_package_dir=$(fixpath "$FSTAR_HOME"/src/ocaml-output/fstar)
+rm -rf "$fstar_package_dir"
+Z3_LICENSE=$(pwd)/LICENSE-z3.txt $make -C "$FSTAR_HOME" package "$@"
+
+# build Karamel and add it to the package
+if [[ -z "$KRML_HOME" ]] ; then
+    if ! [[ -d karamel ]] ; then
+        git clone https://github.com/FStarLang/karamel
+    fi
+    KRML_HOME=$(pwd)/karamel
+fi
+export KRML_HOME=$(fixpath "$KRML_HOME")
+$make -C "$KRML_HOME" minimal "$@"
+OTHERFLAGS='--admit_smt_queries true' $make -C "$KRML_HOME"/krmllib verify-all "$@"
+$cp -L $KRML_HOME/krml $fstar_package_dir/bin/krml$exe
+$cp -r $KRML_HOME/krmllib $fstar_package_dir/
+$cp -r $KRML_HOME/include $fstar_package_dir/
+$cp -r $KRML_HOME/misc $fstar_package_dir/
+
+# assume current directory is $STEEL_HOME/src/ci
+export STEEL_HOME=$(fixpath $(cd ../.. && pwd))
+
+# use the package to build Steel
+export FSTAR_HOME="$fstar_package_dir"
+OTHERFLAGS='--admit_smt_queries true' $make -C "$STEEL_HOME" "$@"
+$make -C "$STEEL_HOME"/share/steel/examples/pulse lib "$@"
+mkdir -p "$old_FSTAR_HOME"/src/.cache.boot
+if ! $is_windows ; then
+    FSTAR_HOME="$old_FSTAR_HOME" $make -C "$STEEL_HOME"/pulse2rust "$@"
+fi
+
+# install Steel into the package directory
+export PREFIX="$FSTAR_HOME"
+$make -C "$STEEL_HOME" install "$@"
+$make -C "$STEEL_HOME"/share/steel/examples/pulse install-lib "$@"
+if ! $is_windows ; then
+    mkdir -p "$PREFIX"/pulse2rust
+    $cp "$STEEL_HOME"/pulse2rust/main.exe "$PREFIX"/pulse2rust/
+fi
+
+# create the archive package
+mv "$PREFIX" steel
+rm -rf steel/share/fstar steel/INSTALL.md steel/README.md steel/version.txt
+$cp package-README.md steel/README.md
+if $is_windows ; then
+  zip -r -9 steel.zip steel
+else
+  tar czf steel.tar.gz steel
+fi