Add verus

.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

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

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

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

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

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"