From cf703d51fd7ca378dd15b5df7f838bdee2e133cd Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 4 Nov 2025 19:48:03 +1100 Subject: [PATCH 1/6] new defaults: 2000 steps, 500 iterations, 1h timeout --- .github/workflows/rv-run-proofs.yaml | 8 ++++---- p-token/test-properties/run-proofs.sh | 8 ++++---- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/rv-run-proofs.yaml b/.github/workflows/rv-run-proofs.yaml index 6f75b7d..e00fbaa 100644 --- a/.github/workflows/rv-run-proofs.yaml +++ b/.github/workflows/rv-run-proofs.yaml @@ -30,7 +30,7 @@ on: description: Timeout for running the proofs required: false type: string - default: 7200 # 2h + default: 3600 # 1h concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true @@ -85,7 +85,7 @@ jobs: ;; esac - - name: "Build with stable_mir_json" + - name: "Build with stable_mir_json" run: | cd "${{ steps.vars.outputs.crate_dir }}" RUSTC=stable_mir_json cargo build --features runtime-verification @@ -178,8 +178,8 @@ jobs: kmir prove-rs --smir "artefacts/${{ needs.compile.outputs.artifact_name }}.json" \ --start-symbol "${{ needs.compile.outputs.start_prefix }}${{ matrix.proof }}" \ --verbose \ - --max-depth 500 \ - --max-iterations 100 \ + --max-depth 2000 \ + --max-iterations 500 \ --proof-dir artefacts/proof \ || echo "Runner signals proof failure" diff --git a/p-token/test-properties/run-proofs.sh b/p-token/test-properties/run-proofs.sh index debd727..a98cb34 100755 --- a/p-token/test-properties/run-proofs.sh +++ b/p-token/test-properties/run-proofs.sh @@ -3,8 +3,8 @@ # Run all start symbols given as arguments (or read them from proofs.md # table if -a given) with given run options (-o) and timeout (-t). # Options and defaults: -# -t NUM : timeout in seconds (default 7200) -# -o STRING: prove-rs options. Default "--max-iterations 100 --max-depth 500" +# -t NUM : timeout in seconds (default 1h=3600) +# -o STRING: prove-rs options. Default "--max-iterations 500 --max-depth 2000" # -a : run all start symbols from first table in `proofs.md` (1st column) # -m : run all start symbols from multisig table in `proofs.md` (2nd column) # -c : continue existing proofs instead of reloading (which is default) @@ -22,8 +22,8 @@ ARTIFACT_BASENAME="${ARTIFACT_BASENAME:-p-token}" ALL_NAMES=$(sed -n -e 's/^| \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md) MULTISIG_NAMES=$(sed -n -e 's/^| m | \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md) -TIMEOUT=7200 -PROVE_OPTS="--max-iterations 100 --max-depth 500" +TIMEOUT=3600 +PROVE_OPTS="--max-iterations 500 --max-depth 2000" RELOAD_OPT="--reload" while getopts ":t:o:amc" opt; do From 8b90eef2622b3ee973871ec5a2df120ad99bda25 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 4 Nov 2025 19:57:41 +1100 Subject: [PATCH 2/6] remove -dirty suffixing of commit hashes (always dirty anyway) --- p-token/test-properties/run-proofs.sh | 7 ------- 1 file changed, 7 deletions(-) diff --git a/p-token/test-properties/run-proofs.sh b/p-token/test-properties/run-proofs.sh index a98cb34..5875bed 100755 --- a/p-token/test-properties/run-proofs.sh +++ b/p-token/test-properties/run-proofs.sh @@ -65,15 +65,8 @@ fi set -u REPO_COMMIT=$(git rev-parse --short HEAD 2>/dev/null || echo "unknown") -if git status --porcelain 1>/dev/null 2>&1 && [ -n "$(git status --porcelain 2>/dev/null)" ]; then - REPO_COMMIT="${REPO_COMMIT}-dirty" -fi MIR_COMMIT=$(git -C mir-semantics rev-parse --short HEAD 2>/dev/null || echo "unknown") -if git -C mir-semantics status --porcelain 1>/dev/null 2>&1 && \ - [ -n "$(git -C mir-semantics status --porcelain 2>/dev/null)" ]; then - MIR_COMMIT="${MIR_COMMIT}-dirty" -fi PROOF_DIR="${ARTIFACTS_DIR:-artefacts}/proof-${REPO_COMMIT}-${MIR_COMMIT}" mkdir -p "${PROOF_DIR}" From bdf9286421b06806e695154d568af2ab4d093b52 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Tue, 4 Nov 2025 22:59:59 +1100 Subject: [PATCH 3/6] alternative proof selection script/table --- p-token/test-properties/select-proofs.sh | 89 ++++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100755 p-token/test-properties/select-proofs.sh diff --git a/p-token/test-properties/select-proofs.sh b/p-token/test-properties/select-proofs.sh new file mode 100755 index 0000000..882cd78 --- /dev/null +++ b/p-token/test-properties/select-proofs.sh @@ -0,0 +1,89 @@ +# /bin/bash +# +# Usage: ./select-proofs.sh "Table Header" +# - select the proofs from one of the tables in the file +# (the first match will be taken) +########################################################## + +USAGE=$(head -6 $0) + +if [ -z "$1" ]; then + head -6 $0 + exit 1 +fi + +HEADING="$1" + +if ! (grep -e "^| $HEADING" $0 > /dev/null); then + echo "[ERROR] '| $HEADING..': not a table header. Must provide a table heading to select proofs." + exit 1 +fi + +sed -n -e "/^| ${HEADING}.*/,/^\$/ {/| ${HEADING}.*/d; /^\$/q; s/^| \(test_p[a-zA-Z0-9_]*\) .*/\1/p}" < Date: Wed, 5 Nov 2025 11:19:33 +1100 Subject: [PATCH 4/6] update VERIFICATION_GUIDE.md to current state --- p-token/test-properties/VERIFICATION_GUIDE.md | 57 ++++++++++--------- 1 file changed, 30 insertions(+), 27 deletions(-) diff --git a/p-token/test-properties/VERIFICATION_GUIDE.md b/p-token/test-properties/VERIFICATION_GUIDE.md index 6c5b5fe..074fd1f 100644 --- a/p-token/test-properties/VERIFICATION_GUIDE.md +++ b/p-token/test-properties/VERIFICATION_GUIDE.md @@ -6,7 +6,7 @@ This guide explains how to run formal verification for the p-token Solana progra ## Architecture -After the merge of `dc/test-hack` branch, the codebase uses conditional compilation to separate production and verification code: +The codebase uses conditional compilation to separate production and verification code: - **Production code**: `src/entrypoint.rs` - Used for normal builds - **Verification code**: `src/entrypoint-runtime-verification.rs` - Used when `runtime-verification` feature is enabled @@ -19,10 +19,32 @@ Cheatcode functions are markers used by the formal verification tools to inject fn cheatcode_is_account(_: &AccountInfo) {} fn cheatcode_is_mint(_: &AccountInfo) {} fn cheatcode_is_rent(_: &AccountInfo) {} -fn cheatcode_is_multisig(_: &AccountInfo) {} // Currently unsupported and behind feature flag "multisig" +fn cheatcode_is_multisig(_: &AccountInfo) {} // Currently unsupported ``` -These functions are no-ops at runtime but provide type hints to the verification tools. +These functions are no-ops at runtime but set up data required for the verification. + +### Assumptions implemented in cheat codes + +* Calling `cheatcode_is_{account,mint,multisig,rent}` asserts that the `Account` pointed-to by `AccountInfo` + is followed in memory by the respective data structure, `state::account::Account`, `state::mint::Mint`, + `state::multisig::Multisig`, or `sysvars::rent::Rent`. +* The cheat codes will set the data length (`data_len`) of the `AccountInfo` to the correct value for the underlying object: + | Object | `data_len` | + |--------- | ---------- | + | Account | 165 | + | Mint | 82 | + | Rent | 17 | + | Multisig | 355 | +* For the `Rent` sysvar, the proofs make additional assumptions to avoid overflows and imprecise `Float` computation: + - The `lamports_per_byteyear` is assumed to be less than `2^32` (to avoid overflows during rent computation). + - The `exemption_threshold` is fixed to value `2.0` (default). This means that computations will be performed in `u64`. + - The `burn_percent` value is assumed to be between 0 and 100 (to avoid underflows during rent computation). +* Access to the data structure is provided by intercepting the following Rust functions: + - `AccountInfo::borrow_data_unchecked` and `AccountInfo::borrow_mut_data_unchecked` + - `Transmutable::load_unchecked` and `Transmutable::load_mut_unchecked` for the instances `Account`, `Mint`, `Multisig` + - `sysvars::rent::Rent::from_bytes_unchecked` and `sysvars::rent::Rent::get` + and replacing their function body execution by an effect that provides the desired access (read-only or mutable). ## Running Verification @@ -56,10 +78,7 @@ cd test-properties ./run-verification.sh -t 600 test_process_transfer # With custom prove-rs options -./run-verification.sh -o "--max-iterations 50 --max-depth 300" test_process_transfer - -# With multisig feature enabled -./run-verification.sh --multisig test_process_transfer +./run-verification.sh -o "--max-iterations 50 --max-depth 200" test_process_transfer ``` ## Test Functions @@ -69,21 +88,12 @@ All test functions are located in `src/entrypoint-runtime-verification.rs` and f - Each function has cheatcode calls at the beginning to mark account types - Functions use fixed-size arrays for formal verification compatibility -## Feature Flags - -### runtime-verification +## Feature Flag `runtime-verification` Required for all verification tests. Enables the verification-specific entrypoint (entrypoint-runtime-verification.rs) and test functions. -### multisig (optional) -Enables cheat codes for all Owner / Authority accounts to be `Multisig` (by default these are `Account`). When enabled: -- Owner / Authority accounts are instantiated as `Multisig` with symbolic arguments via `cheatcode_is_multisig` (TODO: not implemented yet) -- `Multisig`-specific validation logic is included in proof harnesses - -Use `--multisig` flag with run-verification.sh to enable this feature. - ## Available Tests -See `tests.md` for the complete list of available test functions and their current status. +See `proofs.md` for the complete list of available test functions. ## Troubleshooting @@ -96,14 +106,7 @@ If you get errors about the entrypoint module not being found, ensure you're bui cargo build --features runtime-verification ``` -### Multisig Support -To enable multisig account validation in verification tests, use both features: -```bash -cargo build --features "runtime-verification,multisig" -``` - ## Notes -- The verification process can take significant time (20+ minutes per test) -- Default settings: max-depth 200, max-iterations 30, timeout 1200s -- Results are stored in `artefacts/proof/` directory \ No newline at end of file +- 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. \ No newline at end of file From 3a1e5535aefdd10a98e46e9e02457b000a5e5e68 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 6 Nov 2025 12:14:47 +1100 Subject: [PATCH 5/6] Add log-to-file option to run-proofs.sh script When `-l FILE` is given, all output will be written to FILE. instead of stdout/stderr. This allows for running proofs in parallel with `xargs -P 0 -n ./run-proofs.sh -l log-name` while retaining ordered output. --- p-token/test-properties/run-proofs.sh | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/p-token/test-properties/run-proofs.sh b/p-token/test-properties/run-proofs.sh index 5875bed..cbe1f95 100755 --- a/p-token/test-properties/run-proofs.sh +++ b/p-token/test-properties/run-proofs.sh @@ -8,6 +8,7 @@ # -a : run all start symbols from first table in `proofs.md` (1st column) # -m : run all start symbols from multisig table in `proofs.md` (2nd column) # -c : continue existing proofs instead of reloading (which is default) +# -l FILE : log output to file "$NAME.PID" instead of stdout # # Always runs verbosely, always uses artefacts/proof # as proof directory @@ -25,8 +26,9 @@ MULTISIG_NAMES=$(sed -n -e 's/^| m | \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs. TIMEOUT=3600 PROVE_OPTS="--max-iterations 500 --max-depth 2000" RELOAD_OPT="--reload" +LOG_FILE="" -while getopts ":t:o:amc" opt; do +while getopts ":t:o:l:amc" opt; do case $opt in t) TIMEOUT=$OPTARG @@ -34,6 +36,9 @@ while getopts ":t:o:amc" opt; do o) PROVE_OPTS=$OPTARG ;; + l) + LOG_FILE="$OPTARG.$$" + ;; a) TESTS=${ALL_NAMES} ;; @@ -55,13 +60,18 @@ shift $((OPTIND-1)) # Collect tests if [ -z "$TESTS" ]; then - if [ -z "$@" ]; then + if [ "$#" -eq 0 ]; then echo "[ERROR] No test function names given. Use -a or provide at least one name." 1>&2 exit 2 fi TESTS=$@ fi +if [ ! -z "$LOG_FILE" ]; then + echo "[INFO] Logging output to file $LOG_FILE instead of stdout" + exec &> $LOG_FILE +fi + set -u REPO_COMMIT=$(git rev-parse --short HEAD 2>/dev/null || echo "unknown") From 7476d6866899e58f9af82ab5aa349aa0c7c86e39 Mon Sep 17 00:00:00 2001 From: Jost Berthold Date: Thu, 6 Nov 2025 12:30:51 +1100 Subject: [PATCH 6/6] better discribution of passing proofs among groups of 3,4,5 --- p-token/test-properties/mir-semantics | 2 +- p-token/test-properties/select-proofs.sh | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/p-token/test-properties/mir-semantics b/p-token/test-properties/mir-semantics index 42b4b08..638f28b 160000 --- a/p-token/test-properties/mir-semantics +++ b/p-token/test-properties/mir-semantics @@ -1 +1 @@ -Subproject commit 42b4b087e99cd8149b6be5fb0093bc550fe09db1 +Subproject commit 638f28b2309b23ac432b2fc0f18fb4ea22c2f676 diff --git a/p-token/test-properties/select-proofs.sh b/p-token/test-properties/select-proofs.sh index 882cd78..0b268e7 100755 --- a/p-token/test-properties/select-proofs.sh +++ b/p-token/test-properties/select-proofs.sh @@ -24,20 +24,20 @@ sed -n -e "/^| ${HEADING}.*/,/^\$/ {/| ${HEADING}.*/d; /^\$/q; s/^| \(test_p[a-z | Passing | |-----------------------------------------------| | test_ptoken_domain_data | -| test_process_approve | +| test_process_burn | | test_process_approve_checked | | test_process_withdraw_excess_lamports_account | | test_process_transfer | | test_process_mint_to | -| test_process_burn | +| test_process_approve | | test_process_close_account | -| test_process_transfer_checked | +| test_process_sync_native | | test_process_burn_checked | | test_process_revoke | | test_process_freeze_account | | test_process_thaw_account | | test_process_mint_to_checked | -| test_process_sync_native | +| test_process_transfer_checked | | test_process_get_account_data_size | | test_process_initialize_immutable_owner | | test_process_set_authority_account |