Replace mir-semantics submodule with kompass

.gitmodules

@@ -1,4 +1,3 @@
-[submodule "p-token/test-properties/mir-semantics"]
-	path = p-token/test-properties/mir-semantics
-	url = https://github.com/runtimeverification/mir-semantics
-	branch = feature/p-token
+[submodule "p-token/test-properties/deps/stable-mir-json"]
+	path = p-token/test-properties/deps/stable-mir-json
+	url = https://github.com/runtimeverification/stable-mir-json.git

p-token/test-properties/Makefile

@@ -0,0 +1,7 @@
+TOP_DIR := $(shell pwd)
+
+stable-mir-json: CARGO_BUILD_OPTS =
+stable-mir-json:
+	cd deps/stable-mir-json && cargo build ${CARGO_BUILD_OPTS}
+	cd deps/stable-mir-json && cargo run --bin cargo_stable_mir_json -- ${TOP_DIR}/deps/stable-mir-json ${TOP_DIR}/deps
+	${TOP_DIR}/deps/.stable-mir-json/release.sh --version || ${TOP_DIR}/deps/.stable-mir-json/debug.sh --version

p-token/test-properties/VERIFICATION_GUIDE.md

@@ -133,13 +133,18 @@ assertions checking their effects due to them being behind similar feature flags
 
 ### Prerequisites
 
-1. Ensure submodules are initialized:
-   ```bash
-   cd test-properties
-   ./setup.sh
-   ```
+Ensure submodules are initialized and the environment is set up:
 
-2. Install `uv` if not already installed (Python package manager)
+```bash
+cd test-properties
+./setup.sh
+```
+
+Activate the virtual environment:
+
+```bash
+source deps/.venv/bin/activate
+```
 
 ### Running Tests
 
@@ -193,4 +198,4 @@ cargo build --features runtime-verification
 ## Notes
 
 - Default settings: max-depth 2000, max-iterations 500, timeout 1h
-- Results are stored in `artefacts/proof-SHA1-SHA2/` directory, where `SHA1` and `SHA2` indicate the version of `solana-token` and `mir-semantics` used.
+- Results are stored in `artefacts/proof-SHA-VER/` directory, where `SHA` and `VER` indicate the `solana-token` revision and `mir-semantics` version used, respectively.

p-token/test-properties/deps/kompass_release

@@ -0,0 +1 @@
+c3d68576bfa6d775ce5200e856bc977aafff20af

p-token/test-properties/run-fuzzer.py

@@ -1,4 +1,4 @@
-#!/usr/bin/env -S uv --project ./mir-semantics/kmir run
+#!/usr/bin/env python3
 
 from __future__ import annotations
 
@@ -98,7 +98,13 @@ def load_smir() -> SMIRInfo:
 
 
 def load_kmir(smir_info: SMIRInfo) -> KMIR:
-    return KMIR.from_kompiled_kore(smir_info, target_dir=TARGET_DIR, symbolic=False)
+    return KMIR.from_kompiled_kore(
+        smir_info,
+        target_dir=TARGET_DIR,
+        symbolic=False,
+        haskell_target='kompass.haskell',
+        llvm_target='kompass.llvm',
+    )
 
 
 def fuzz(kmir: KMIR, smir_info: SMIRInfo, test: str, seed: int) -> None:
@@ -109,6 +115,7 @@ def fuzz(kmir: KMIR, smir_info: SMIRInfo, test: str, seed: int) -> None:
         start_symbol=f'{TEST_PREFIX}{test}',
         depth=None,
         seed=seed,
+        llvm_target='kompass.llvm',
     )
 
     kore_text = pattern.text

p-token/test-properties/run-proofs.sh

@@ -81,9 +81,9 @@ set -u
 
 REPO_COMMIT=$(git rev-parse --short HEAD 2>/dev/null || echo "unknown")
 
-MIR_COMMIT=$(git -C mir-semantics rev-parse --short HEAD 2>/dev/null || echo "unknown")
+MIR_VERSION=$(python3 -c 'import kmir; print(kmir.__version__)' || echo "unknown")
 
-PROOF_DIR="${ARTIFACTS_DIR:-artefacts}/proof-${REPO_COMMIT}-${MIR_COMMIT}"
+PROOF_DIR="${ARTIFACTS_DIR:-artefacts}/proof-${REPO_COMMIT}-${MIR_VERSION}"
 mkdir -p "${PROOF_DIR}"
 
 # Default proof status directory to live inside the hashed artefacts/proof directory
@@ -107,9 +107,9 @@ for name in $TESTS; do
     start_time=$(date +%s)
 
     timeout --preserve-status -v ${TIMEOUT} \
-        uv --project mir-semantics/kmir run -- \
         kmir prove-rs --smir "${ARTIFACTS_DIR:-artefacts}/${ARTIFACT_BASENAME}.smir.json" \
-        --proof-dir "${PROOF_DIR}" --verbose --start-symbol $start ${RELOAD_OPT} ${MAX_WORKERS:+--max-workers $MAX_WORKERS} ${PROVE_OPTS}
+        --proof-dir "${PROOF_DIR}" --verbose --start-symbol $start ${RELOAD_OPT} ${MAX_WORKERS:+--max-workers $MAX_WORKERS} ${PROVE_OPTS} \
+        --haskell-target kompass.haskell --llvm-lib-target kompass.llvm-library
     prove_rc=$?
 
     end_time=$(date +%s)
@@ -138,15 +138,15 @@ for name in $TESTS; do
         echo "total_duration_seconds: ${total_duration}"
         echo "prove_exit_code: ${prove_rc}"
         echo "repo_commit: ${REPO_COMMIT}"
-        echo "mir_semantics_commit: ${MIR_COMMIT}"
+        echo "mir_semantics_version: ${MIR_VERSION}"
         echo ""
     } > "${status_file}"
 
-    uv --project mir-semantics/kmir run -- \
-       kmir show --proof-dir "${PROOF_DIR}" ${ARTIFACT_BASENAME}.smir.$start \
-       --full-printer > "${PROOF_DIR}/${name}-full.txt"
-    uv --project mir-semantics/kmir run -- \
-       kmir show --proof-dir "${PROOF_DIR}" ${ARTIFACT_BASENAME}.smir.$start \
-       --statistics --leaves >> "${status_file}"
+    kmir show --proof-dir "${PROOF_DIR}" ${ARTIFACT_BASENAME}.smir.$start \
+       --full-printer > "${PROOF_DIR}/${name}-full.txt" \
+       --haskell-target kompass.haskell
+    kmir show --proof-dir "${PROOF_DIR}" ${ARTIFACT_BASENAME}.smir.$start \
+       --statistics --leaves >> "${status_file}" \
+       --haskell-target kompass.haskell
     echo "==========================================================================="
 done

p-token/test-properties/run-verification.sh

@@ -35,7 +35,7 @@ cd "$SCRIPT_DIR"
 echo "Building p-token with features: $FEATURES"
 cd ..
 cargo clean
-export RUSTC=$PWD/test-properties/mir-semantics/deps/.stable-mir-json/release.sh
+export RUSTC=$PWD/deps/.stable-mir-json/release.sh
 
 # Build with runtime-verification feature to get test functions
 cargo build --features "$FEATURES"
@@ -46,8 +46,8 @@ cd test-properties
 echo "Linking SMIR files..."
 SMIRS=$(ls ../../target/debug/deps/*smir.json | sort)
 mkdir -p artefacts/
-uv --project mir-semantics/kmir run -- kmir link ${SMIRS} -o artefacts/p-token.smir.json
+kmir link ${SMIRS} -o artefacts/p-token.smir.json
 
 # Now run the proofs
 echo "Running verification proofs..."
-./run-proofs.sh "$@"
+./run-proofs.sh "$@"