From 2e04489747703565b4eedcfd301e42a3a1599210 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Sun, 29 Dec 2024 15:39:30 +0100
Subject: [PATCH] Add verus

---
 .gitmodules         |  3 +++
 make_smt2.sh        |  2 +-
 verus/build.sh      |  7 +++++++
 verus/run-single.sh |  6 ++++++
 verus/run.sh        | 14 ++++++++++++++
 verus/tests.sh      |  1 +
 verus/verus         |  1 +
 7 files changed, 33 insertions(+), 1 deletion(-)
 create mode 100755 verus/build.sh
 create mode 100755 verus/run-single.sh
 create mode 100755 verus/run.sh
 create mode 100755 verus/tests.sh
 create mode 160000 verus/verus

diff --git a/.gitmodules b/.gitmodules
index 65268a33e..0b9c35b58 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -10,3 +10,6 @@
 [submodule "fstar/fstar"]
 	path = fstar/fstar
 	url = https://github.com/FStarLang/FStar.git
+[submodule "verus/verus"]
+	path = verus/verus
+	url = https://github.com/verus-lang/verus.git
diff --git a/make_smt2.sh b/make_smt2.sh
index 3c9e00221..7a4bafe20 100755
--- a/make_smt2.sh
+++ b/make_smt2.sh
@@ -3,7 +3,7 @@
 
 VERIFIERS="$@"
 if [ -z "$VERIFIERS" ]; then
-    VERIFIERS="fstar dafny silicon carbon"
+    VERIFIERS="verus fstar dafny silicon carbon"
 fi
 
 git submodule update --init --recursive &> /dev/null
diff --git a/verus/build.sh b/verus/build.sh
new file mode 100755
index 000000000..9eda08f08
--- /dev/null
+++ b/verus/build.sh
@@ -0,0 +1,7 @@
+cd "$(dirname "$0")/verus/source"
+
+if [ ! -f ./target-verus/release/verus ]; then
+    source ../tools/activate
+    ./tools/get-z3.sh
+    vargo build --release
+fi
diff --git a/verus/run-single.sh b/verus/run-single.sh
new file mode 100755
index 000000000..89305631a
--- /dev/null
+++ b/verus/run-single.sh
@@ -0,0 +1,6 @@
+OUT="$(pwd)/${2%.*}"
+
+mkdir -p "$(dirname "$OUT")"
+
+cd "$(dirname "$0")/verus/source"
+./target-verus/release/verus --log-dir "$OUT" --log smt --rlimit "$3" $1
diff --git a/verus/run.sh b/verus/run.sh
new file mode 100755
index 000000000..89473584e
--- /dev/null
+++ b/verus/run.sh
@@ -0,0 +1,14 @@
+OP=($2)
+OUT="$(pwd)/$(echo "${OP[0]%.*}" | sed 's/ /_/g')/${OP[1]}"
+mkdir -p "$(dirname "$OUT")"
+
+cd "$(dirname "$0")/verus/source"
+export VERUS_EXTRA_ARGS="--log-dir $OUT --log smt --rlimit $3"
+export VARGO_IN_NEXTEST=true
+TEST=($1)
+FILE=${TEST[0]#$(pwd)/rust_verify_test/tests/}
+vargo test --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact &> /dev/null || exit 1
+if [ -f "$OUT/root.smt2" ]; then
+  mv "$OUT/root.smt2" "$OUT.smt2"
+  rmdir "$OUT" || true
+fi
diff --git a/verus/tests.sh b/verus/tests.sh
new file mode 100755
index 000000000..62fbbccde
--- /dev/null
+++ b/verus/tests.sh
@@ -0,0 +1 @@
+grep -oEr "#\[test\] (\w+)" "$(realpath "$(dirname "$0")")/verus/source/rust_verify_test/tests" | sed -E "s|^(.*):#\[test\] ([a-zA-Z_0-9-]+)|\1 \2|g"
diff --git a/verus/verus b/verus/verus
new file mode 160000
index 000000000..dad7116b9
--- /dev/null
+++ b/verus/verus
@@ -0,0 +1 @@
+Subproject commit dad7116b903fc938e1dd15f35fc80dc6698bd001