From e009769a6d0ccd9eb62f5a4eabfaef331d692ed2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Thu, 26 Dec 2024 23:23:16 +0100
Subject: [PATCH] Add fstar

---
 .github/workflows/smt2.yml | 9 +++++++++
 .gitmodules                | 3 +++
 fstar/build.sh             | 9 +++++++++
 fstar/fstar                | 1 +
 fstar/run.sh               | 8 ++++++++
 fstar/tests.sh             | 1 +
 make_smt2.sh               | 2 +-
 7 files changed, 32 insertions(+), 1 deletion(-)
 create mode 100755 fstar/build.sh
 create mode 160000 fstar/fstar
 create mode 100755 fstar/run.sh
 create mode 100755 fstar/tests.sh

diff --git a/.github/workflows/smt2.yml b/.github/workflows/smt2.yml
index ae9559817..d5de5523b 100644
--- a/.github/workflows/smt2.yml
+++ b/.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/setup-z3@v1.3
         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
 
diff --git a/.gitmodules b/.gitmodules
index d1150fc91..65268a33e 100644
--- a/.gitmodules
+++ b/.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
diff --git a/fstar/build.sh b/fstar/build.sh
new file mode 100755
index 000000000..c51459062
--- /dev/null
+++ b/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
diff --git a/fstar/fstar b/fstar/fstar
new file mode 160000
index 000000000..a3be6122b
--- /dev/null
+++ b/fstar/fstar
@@ -0,0 +1 @@
+Subproject commit a3be6122b76ec0ca29030e1ff72576dceeede19d
diff --git a/fstar/run.sh b/fstar/run.sh
new file mode 100755
index 000000000..62df1da2d
--- /dev/null
+++ b/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"
diff --git a/fstar/tests.sh b/fstar/tests.sh
new file mode 100755
index 000000000..774460112
--- /dev/null
+++ b/fstar/tests.sh
@@ -0,0 +1 @@
+find "$(realpath "$0" | xargs dirname)/fstar/tests" -name "*.fst" -type f
diff --git a/make_smt2.sh b/make_smt2.sh
index 5285383ce..18c56516a 100755
--- a/make_smt2.sh
+++ b/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