Add fstar

.github/workflows/smt2.yml

@@ -18,20 +18,29 @@ jobs:
           submodules: 'recursive'
           fetch-depth: 0
 
+      # Dafny likes `4.12.1`, FStar likes `4.13.3`, Viper likes `4.8.7`
       - name: Install Z3 for newer version
         uses: pavpanchekha/[email protected]
         with:
           version: 4.12.1
           distribution: 'glibc-2.35'
 
+      # Dafny
       - name: Setup dotnet
         uses: actions/setup-dotnet@v4
         with:
           dotnet-version: 6.0.x
 
+      # Dafny & Carbon
       - name: Install Boogie
         run: dotnet tool install --global boogie
 
+      # FStar
+      - name: Set-up OCaml
+        uses: ocaml/setup-ocaml@v3
+        with:
+          ocaml-compiler: 5
+
       - name: Make smt2 files
         run: ./make_smt2.sh
 

.gitmodules

@@ -7,3 +7,6 @@
 [submodule "viper/viper_client"]
 	path = viper/viper_client
 	url = https://github.com/viperproject/viper_client.git
+[submodule "fstar/fstar"]
+	path = fstar/fstar
+	url = https://github.com/FStarLang/FStar.git

fstar/build.sh

@@ -0,0 +1,9 @@
+# Requires `opam` and `coreutils`
+cd "$(dirname "$0")/fstar"
+
+export PATH="$(pwd)/z3/bin:$PATH"
+if [ ! -f ./bin/fstar.exe ]; then
+    ./bin/get_fstar_z3.sh ./z3/bin
+    opam install --deps-only -y .
+    make -j 6
+fi

fstar/run.sh

@@ -0,0 +1,8 @@
+FSTAR="$(dirname "$0" | realpath)/fstar/bin/fstar.exe"
+
+OUT="$(pwd)/$(dirname "$2")"
+mkdir -p "$OUT"
+cd "$OUT"
+
+Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')
+"$FSTAR" --z3version "$Z3_VERSION" --log_queries "$1"

fstar/tests.sh

@@ -0,0 +1 @@
+find "$(realpath "$0" | xargs dirname)/fstar/tests" -name "*.fst" -type f

make_smt2.sh

@@ -3,7 +3,7 @@
 
 VERIFIERS="$@"
 if [ -z "$VERIFIERS" ]; then
-    VERIFIERS="dafny silicon carbon"
+    VERIFIERS="fstar dafny silicon carbon"
 fi
 
 git submodule update --init --recursive &> /dev/null