From da18ce9158e65037232f914dce2b6d598d63e233 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 20 Jan 2026 13:07:17 +0000 Subject: [PATCH 01/10] Add `deps/kompass_release` --- p-token/test-properties/deps/kompass_release | 1 + 1 file changed, 1 insertion(+) create mode 100644 p-token/test-properties/deps/kompass_release diff --git a/p-token/test-properties/deps/kompass_release b/p-token/test-properties/deps/kompass_release new file mode 100644 index 00000000..112d548e --- /dev/null +++ b/p-token/test-properties/deps/kompass_release @@ -0,0 +1 @@ +73d0a02f23a8e4ea6b5446b2d65b122920c2cc9a From be98fd6b38f7f05757592fd25adb7b64730cc0a9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 20 Jan 2026 13:09:24 +0000 Subject: [PATCH 02/10] Remove submodule `mir-semantics` --- .gitmodules | 4 ---- p-token/test-properties/mir-semantics | 1 - 2 files changed, 5 deletions(-) delete mode 160000 p-token/test-properties/mir-semantics diff --git a/.gitmodules b/.gitmodules index 02258435..e69de29b 100644 --- a/.gitmodules +++ b/.gitmodules @@ -1,4 +0,0 @@ -[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 diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics deleted file mode 160000 index 9017feed..00000000 --- a/p-token/test-properties/mir-semantics +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 9017feed560c7a8ba92a37e3d09fc60052f694eb From 48ceb8e96be467beca194be64a6d1c1cd889aeb6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 20 Jan 2026 13:17:09 +0000 Subject: [PATCH 03/10] Add submodule `stable-mir-json` --- .gitmodules | 3 +++ p-token/test-properties/deps/stable-mir-json | 1 + 2 files changed, 4 insertions(+) create mode 160000 p-token/test-properties/deps/stable-mir-json diff --git a/.gitmodules b/.gitmodules index e69de29b..2d153300 100644 --- a/.gitmodules +++ b/.gitmodules @@ -0,0 +1,3 @@ +[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 diff --git a/p-token/test-properties/deps/stable-mir-json b/p-token/test-properties/deps/stable-mir-json new file mode 160000 index 00000000..a5b714d8 --- /dev/null +++ b/p-token/test-properties/deps/stable-mir-json @@ -0,0 +1 @@ +Subproject commit a5b714d89d0c12c7f4b00602a95ad2d3a34530f0 From b6c09aba6bdde5192c6ccf7b3b0ebf45b34f9af6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 09:40:33 +0000 Subject: [PATCH 04/10] Adjust `setup.sh` --- p-token/test-properties/Makefile | 7 ++++ p-token/test-properties/setup.sh | 66 ++++++++++++++++++++++++-------- 2 files changed, 57 insertions(+), 16 deletions(-) create mode 100644 p-token/test-properties/Makefile diff --git a/p-token/test-properties/Makefile b/p-token/test-properties/Makefile new file mode 100644 index 00000000..068dac46 --- /dev/null +++ b/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 diff --git a/p-token/test-properties/setup.sh b/p-token/test-properties/setup.sh index adb2ee02..f5b80731 100755 --- a/p-token/test-properties/setup.sh +++ b/p-token/test-properties/setup.sh @@ -1,9 +1,10 @@ #!/bin/bash # # Setup for running property tests with kmir (defaults for p-token). -# - checks out submodule mir-semantics (recursively incl. stable-mir-json) -# - builds stable-mir-json and mir-semantics +# - sets up a virtual environment with kompass installed +# - checks out and builds submodule stable-mir-json # - builds the selected crate with STABLE MIR and links SMIR JSON into artefacts +# - builds the K definitions # # Usage: # ./setup.sh [OPTIONS] @@ -18,7 +19,8 @@ # ARTIFACT_BASENAME Artefact base name (default: p-token) # # After running it, one can use: -# `uv --project mir-semantics/kmir run -- kmir ...` +# source deps/.venv/bin/activate +# kmir ... ###################################################################### set -xeuo pipefail @@ -29,6 +31,7 @@ SKIP_SUBMODULES=true CRATE_DIR="${CRATE_DIR:-$(realpath "${SCRIPT_DIR}/..")}" ARTIFACT_BASENAME="${ARTIFACT_BASENAME:-p-token}" + while [[ $# -gt 0 ]]; do case $1 in --skip-submodules) @@ -44,36 +47,60 @@ done cd "${SCRIPT_DIR}" + +############################# +# Step 1: Set up kompass venv +############################# + +VENV_DIR='deps/.venv' +KOMPASS_URL='https://github.com/runtimeverification/kompass' +KOMPASS_VERSION=$(cat deps/kompass_release) + +if [[ -d "$VENV_DIR" ]]; then + echo "Virtual environment already exists at ${VENV_DIR}" + source "$VENV_DIR/bin/activate" +else + echo "Creating virtual environment at ${VENV_DIR}" + python3 -m venv "${VENV_DIR}" + + echo "Installing kompass" + source "$VENV_DIR/bin/activate" + pip install --upgrade pip + pip install "git+${KOMPASS_URL}@${KOMPASS_VERSION}" +fi + + +############################### +# Step 2: Build stable-mir-json +############################### + # Refresh/check out submodules (unless skipped) if [ "${SKIP_SUBMODULES}" = false ]; then echo "Refreshing git submodules..." git submodule update --init --recursive git submodule status --recursive - - echo "Checking out mir-semantics at origin/feature/p-token..." - if git -C mir-semantics status --porcelain | grep -v '^?? ' >/dev/null; then - echo "Skipping checkout: tracked local changes detected." - else - git -C mir-semantics fetch origin feature/p-token || true - git -C mir-semantics checkout --quiet origin/feature/p-token || true - fi else echo "Skipping git submodule refresh..." fi # Ensure stable-mir-json acts as its own workspace to avoid root workspace capture. # Add an empty [workspace] if missing (idempotent, independent of git status). -SMJ_CARGO_TOML="mir-semantics/deps/stable-mir-json/Cargo.toml" +SMJ_CARGO_TOML="deps/stable-mir-json/Cargo.toml" if ! grep -q '^\[workspace\]' "$SMJ_CARGO_TOML"; then printf "\n\n# avoid workspace confusion in token repo\n[workspace]\n" >> "$SMJ_CARGO_TOML" fi -# Build mir-semantics and stable-mir-json -make -C mir-semantics stable-mir-json build +# Build stable-mir-json +make stable-mir-json CARGO_BUILD_OPTS=--release -export RUSTC=$PWD/mir-semantics/deps/.stable-mir-json/release.sh +export RUSTC=$PWD/deps/.stable-mir-json/release.sh ${RUSTC} --version + +############################## +# Step 3: Build and link tests +############################## + # Build selected crate with stable-mir-json (clean first) pushd "${CRATE_DIR}" >/dev/null # Force cargo to emit artifacts under the crate's own target directory @@ -91,4 +118,11 @@ ls ${SMIRS} # Link all SMIR JSON and store in artefacts directory mkdir -p "${ARTEFACTS_DIR:-artefacts}/" -uv --project mir-semantics/kmir run -- kmir link ${SMIRS} -o "${ARTEFACTS_DIR:-artefacts}/${ARTIFACT_BASENAME}.smir.json" +kmir link ${SMIRS} -o "${ARTEFACTS_DIR:-artefacts}/${ARTIFACT_BASENAME}.smir.json" + + +############################# +# Step 4: Build K definitions +############################# + +kdist --verbose build -j4 kompass.\* From d744e4e4cd0c4deb4950dc50917f52df8edd50db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 10:05:59 +0000 Subject: [PATCH 05/10] Adjust `run_fuzzer.py` --- p-token/test-properties/run-fuzzer.py | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/p-token/test-properties/run-fuzzer.py b/p-token/test-properties/run-fuzzer.py index 1cd46a30..b6e4f7c8 100755 --- a/p-token/test-properties/run-fuzzer.py +++ b/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 From e519858124cc6e6f5ca79b496e264a800e4f0ef7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 10:29:19 +0000 Subject: [PATCH 06/10] Adjust `run-proofs.sh` --- p-token/test-properties/run-proofs.sh | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/p-token/test-properties/run-proofs.sh b/p-token/test-properties/run-proofs.sh index cba63a60..912cd524 100755 --- a/p-token/test-properties/run-proofs.sh +++ b/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 From 10bfdcacf586b978fd07c4c891e7b01425f55980 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 10:34:22 +0000 Subject: [PATCH 07/10] Adjust `run-verification.sh` --- p-token/test-properties/run-verification.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/p-token/test-properties/run-verification.sh b/p-token/test-properties/run-verification.sh index c29b6a45..89bb3284 100755 --- a/p-token/test-properties/run-verification.sh +++ b/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 "$@" \ No newline at end of file +./run-proofs.sh "$@" From 644622a4a379b5244093764d673e161fe770fe3e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 10:56:42 +0000 Subject: [PATCH 08/10] Adjust `analyze_all_intrinsics` --- .../scripts/analyze_all_intrinsics.py | 122 +++++++++--------- 1 file changed, 64 insertions(+), 58 deletions(-) diff --git a/p-token/test-properties/scripts/analyze_all_intrinsics.py b/p-token/test-properties/scripts/analyze_all_intrinsics.py index 420277b9..c5d4fa1e 100644 --- a/p-token/test-properties/scripts/analyze_all_intrinsics.py +++ b/p-token/test-properties/scripts/analyze_all_intrinsics.py @@ -6,6 +6,8 @@ from collections import defaultdict, Counter from pathlib import Path +from pyk.kdist import kdist + def extract_intrinsic_name(func_symbol): """Extract the intrinsic name from a mangled function symbol""" intrinsics = { @@ -60,7 +62,7 @@ def extract_intrinsic_name(func_symbol): 'min_align_of_val': 'min_align_of_val', 'size_of_val': 'size_of_val' } - + for key in intrinsics: if key in func_symbol.lower(): return intrinsics[key] @@ -69,36 +71,36 @@ def extract_intrinsic_name(func_symbol): def analyze_proof_output(proof_file): """Analyze proof output file for stuck intrinsics""" stuck_intrinsics = set() - + if not proof_file.exists(): return stuck_intrinsics - + content = proof_file.read_text() - + # Look for #execIntrinsic patterns intrinsic_pattern = r'#execIntrinsic\s*\(\s*symbol\s*\(\s*"([^"]+)"\s*\)' matches = re.findall(intrinsic_pattern, content) stuck_intrinsics.update(matches) - + # Look for stuck nodes with intrinsic mentions if 'raw_eq' in content and 'pending' in content: stuck_intrinsics.add('raw_eq') if 'assert_inhabited' in content and 'pending' in content: stuck_intrinsics.add('assert_inhabited') - + return stuck_intrinsics def analyze_smir(filename): """Comprehensive intrinsics analysis for entire program verification""" with open(filename, 'r') as f: data = json.load(f) - + # Track all intrinsics all_intrinsics = set() test_intrinsics = defaultdict(set) function_intrinsics = defaultdict(set) intrinsic_usage_count = Counter() - + # Analyze functions list for intrinsic symbols functions = data.get('functions', []) if isinstance(functions, list): @@ -110,23 +112,23 @@ def analyze_smir(filename): if intrinsic: all_intrinsics.add(intrinsic) intrinsic_usage_count[intrinsic] += 1 - + # Analyze all items (functions) in detail for item in data.get('items', []): name = item.get('name', '') body = item.get('body') - + if not body: continue - + # Track intrinsics per function func_intrinsics = set() - + for block in body.get('blocks', []): # Check terminator terminator = block.get('terminator', {}) term_kind = terminator.get('kind', {}) - + # Check for Call terminators if term_kind.get('Call'): call = term_kind['Call'] @@ -136,7 +138,7 @@ def analyze_smir(filename): if intrinsic: func_intrinsics.add(intrinsic) intrinsic_usage_count[intrinsic] += 1 - + # Check statements for stmt in block.get('statements', []): stmt_kind = stmt.get('kind', {}) @@ -148,26 +150,26 @@ def analyze_smir(filename): if intrinsic: func_intrinsics.add(intrinsic) intrinsic_usage_count[intrinsic] += 1 - + if func_intrinsics: function_intrinsics[name] = func_intrinsics all_intrinsics.update(func_intrinsics) - + # Special tracking for test functions if 'test_' in name and 'entrypoint' in name: test_intrinsics[name] = func_intrinsics - + # Analyze proof outputs for stuck intrinsics proof_dir = Path('artefacts/proof') stuck_intrinsics_by_test = {} - + if proof_dir.exists(): for proof_file in proof_dir.glob('*.json'): test_name = proof_file.stem.replace('p-token.smir.', '') stuck = analyze_proof_output(proof_file) if stuck: stuck_intrinsics_by_test[test_name] = stuck - + return { 'all_intrinsics': all_intrinsics, 'test_intrinsics': test_intrinsics, @@ -179,22 +181,26 @@ def analyze_smir(filename): def check_mir_semantics_support(): """Check which intrinsics are implemented in mir-semantics""" implemented = set() - mir_semantics_path = Path('mir-semantics/kmir/src/kmir/kdist/mir-semantics') - - if mir_semantics_path.exists(): - # Search for intrinsic implementations - for k_file in mir_semantics_path.rglob('*.md'): - content = k_file.read_text() - if 'intrinsic' in content.lower(): - # Look for rule definitions - if 'rule [intrinsic-' in content or 'rule #execIntrinsic' in content: - # Extract implemented intrinsics - if 'black_box' in content: - implemented.add('black_box') - if 'copy_nonoverlapping' in content: - implemented.add('copy_nonoverlapping') - # Add more as we find them - + + # Search for intrinsic implementations + k_source_dirs = [kdist.which(target) for target in ['mir-semantics.source', 'kompass.source']] + k_source_files = [file for files in [source_dir.rglob('*.md') for source_dir in k_source_dirs] for file in files] + + print('K source files') + print('--------------') + for k_file in k_source_files: + print(str(k_file)) + content = k_file.read_text() + if 'intrinsic' in content.lower(): + # Look for rule definitions + if 'rule [intrinsic-' in content or 'rule #execIntrinsic' in content: + # Extract implemented intrinsics + if 'black_box' in content: + implemented.add('black_box') + if 'copy_nonoverlapping' in content: + implemented.add('copy_nonoverlapping') + # Add more as we find them + return implemented def generate_report(analysis): @@ -203,27 +209,27 @@ def generate_report(analysis): test_intrinsics = analysis['test_intrinsics'] usage_count = analysis['intrinsic_usage_count'] stuck_by_test = analysis['stuck_intrinsics_by_test'] - + # Check what's implemented implemented = check_mir_semantics_support() - + # Categorize intrinsics missing = all_intrinsics - implemented blocking = set() for stuck_set in stuck_by_test.values(): blocking.update(stuck_set) - + print("=" * 100) print("COMPREHENSIVE INTRINSICS ANALYSIS FOR P-TOKEN (entrypoint.rs) VERIFICATION") print("=" * 100) - + print("\n## SUMMARY") print("-" * 50) print(f"Total unique intrinsics found: {len(all_intrinsics)}") print(f"Implemented in K semantics: {len(implemented)}") print(f"Missing implementations: {len(missing)}") print(f"Currently blocking tests: {len(blocking)}") - + print("\n## ALL INTRINSICS REQUIRED") print("-" * 50) for intrinsic in sorted(all_intrinsics): @@ -231,7 +237,7 @@ def generate_report(analysis): blocking_mark = " 🚫 BLOCKING" if intrinsic in blocking else "" count = usage_count[intrinsic] print(f"{status} {intrinsic:<30} (used {count} times){blocking_mark}") - + print("\n## MISSING INTRINSICS (Need Implementation)") print("-" * 50) if missing: @@ -241,12 +247,12 @@ def generate_report(analysis): priority_missing.append((intrinsic, "HIGH - Currently blocking tests")) else: priority_missing.append((intrinsic, "MEDIUM - May be needed")) - + for intrinsic, priority in priority_missing: print(f"- {intrinsic:<30} Priority: {priority}") else: print("None - all intrinsics are implemented") - + print("\n## INTRINSICS BY TEST FUNCTION") print("-" * 50) for test_name in sorted(test_intrinsics.keys()): @@ -254,13 +260,13 @@ def generate_report(analysis): short_name = test_name.replace('entrypoint::', '') intrinsics = test_intrinsics[test_name] stuck = stuck_by_test.get(test_name, set()) - + print(f"\n### {short_name}") for intrinsic in sorted(intrinsics): status = "✅" if intrinsic in implemented else "❌" stuck_mark = " (STUCK HERE)" if intrinsic in stuck else "" print(f" {status} {intrinsic}{stuck_mark}") - + print("\n## BLOCKING ANALYSIS") print("-" * 50) if stuck_by_test: @@ -272,11 +278,11 @@ def generate_report(analysis): print(f" - {intrinsic}") else: print("No tests found stuck on intrinsics") - + print("\n## IMPLEMENTATION PRIORITY") print("-" * 50) print("Based on test blockage and usage frequency:\n") - + # Calculate priority priority_scores = {} for intrinsic in missing: @@ -284,33 +290,33 @@ def generate_report(analysis): if intrinsic in blocking: score += 1000 # High priority for blocking priority_scores[intrinsic] = score - + # Sort by priority sorted_priority = sorted(priority_scores.items(), key=lambda x: x[1], reverse=True) - + for i, (intrinsic, score) in enumerate(sorted_priority[:10], 1): blocking_status = "BLOCKING" if intrinsic in blocking else "Not blocking" print(f"{i}. {intrinsic:<25} (Score: {score}, Usage: {usage_count[intrinsic]}, Status: {blocking_status})") - + print("\n## INTRINSIC CATEGORIES") print("-" * 50) - + categories = { 'Memory Operations': ['copy_nonoverlapping', 'write_bytes', 'transmute'], 'Pointer Operations': ['raw_eq', 'ptr_guaranteed_cmp', 'ptr_offset_from', 'ptr_offset_from_unsigned'], - 'Type Operations': ['assert_inhabited', 'assert_zero_valid', 'assert_mem_uninitialized_valid', + 'Type Operations': ['assert_inhabited', 'assert_zero_valid', 'assert_mem_uninitialized_valid', 'size_of', 'align_of', 'type_id', 'type_name', 'discriminant_value'], - 'Arithmetic': ['saturating_add', 'saturating_sub', 'wrapping_add', 'wrapping_sub', + 'Arithmetic': ['saturating_add', 'saturating_sub', 'wrapping_add', 'wrapping_sub', 'wrapping_mul', 'unchecked_add', 'unchecked_sub', 'unchecked_mul', 'unchecked_div', 'unchecked_rem', 'exact_div'], - 'Bit Operations': ['bswap', 'bitreverse', 'ctpop', 'ctlz', 'cttz', + 'Bit Operations': ['bswap', 'bitreverse', 'ctpop', 'ctlz', 'cttz', 'rotate_left', 'rotate_right', 'unchecked_shl', 'unchecked_shr'], 'Control Flow': ['cold_path', 'unlikely', 'likely', 'assume', 'unreachable', 'abort'], 'Debug/Test': ['black_box', 'forget'], 'Other': ['float_to_int_unchecked', 'const_eval_select', 'is_val_statically_known', 'vtable_size', 'vtable_align', 'min_align_of_val', 'size_of_val'] } - + for category, intrinsics in categories.items(): found = [i for i in intrinsics if i in all_intrinsics] if found: @@ -318,7 +324,7 @@ def generate_report(analysis): for intrinsic in found: status = "✅" if intrinsic in implemented else "❌" print(f" {status} {intrinsic}") - + return { 'total': len(all_intrinsics), 'implemented': len(implemented), @@ -332,7 +338,7 @@ def generate_report(analysis): print("Analyzing p-token.smir.json for all intrinsics...") analysis = analyze_smir('artefacts/p-token.smir.json') summary = generate_report(analysis) - + print("\n" + "=" * 100) print("FINAL SUMMARY FOR VERIFICATION") print("=" * 100) @@ -342,4 +348,4 @@ def generate_report(analysis): The most critical missing intrinsics are those that appear in multiple tests and are currently causing proof failures. Implementing these will unblock formal verification. -""") \ No newline at end of file +""") From bc70b23af3180d4a1c3f18044af3601361853f87 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 21 Jan 2026 11:04:44 +0000 Subject: [PATCH 09/10] Adjust `VERIFICATION_GUIDE.md` --- p-token/test-properties/VERIFICATION_GUIDE.md | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/p-token/test-properties/VERIFICATION_GUIDE.md b/p-token/test-properties/VERIFICATION_GUIDE.md index 14e4cab7..f0f31132 100644 --- a/p-token/test-properties/VERIFICATION_GUIDE.md +++ b/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. From 7ea15bb99b539658ebb258b2da8af0afbd445308 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Fri, 24 Apr 2026 13:48:20 -0500 Subject: [PATCH 10/10] Update kompass to latest master (kmir 0.4.213) --- p-token/test-properties/deps/kompass_release | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/p-token/test-properties/deps/kompass_release b/p-token/test-properties/deps/kompass_release index 112d548e..5696fbeb 100644 --- a/p-token/test-properties/deps/kompass_release +++ b/p-token/test-properties/deps/kompass_release @@ -1 +1 @@ -73d0a02f23a8e4ea6b5446b2d65b122920c2cc9a +c3d68576bfa6d775ce5200e856bc977aafff20af