Script updates: new defaults, no dirty, new helper script

.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"
 

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
+- 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.

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

@@ -3,11 +3,12 @@
 # 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)
+#   -l FILE  : log output to file "$NAME.PID" instead of stdout
 #
 # Always runs verbosely, always uses artefacts/proof
 # as proof directory
@@ -22,18 +23,22 @@ 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"
+LOG_FILE=""
 
-while getopts ":t:o:amc" opt; do
+while getopts ":t:o:l:amc" opt; do
     case $opt in
         t)
             TIMEOUT=$OPTARG
             ;;
         o)
             PROVE_OPTS=$OPTARG
             ;;
+        l)
+            LOG_FILE="$OPTARG.$$"
+            ;;
         a)
             TESTS=${ALL_NAMES}
             ;;
@@ -55,25 +60,23 @@ 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")
-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}"

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}" <<EOF
+
+| Passing                                       |
+|-----------------------------------------------|
+| test_ptoken_domain_data                       |
+| test_process_burn                             |
+| test_process_approve_checked                  |
+| test_process_withdraw_excess_lamports_account |
+| test_process_transfer                         |
+| test_process_mint_to                          |
+| test_process_approve                          |
+| test_process_close_account                    |
+| 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_transfer_checked                 |
+| test_process_get_account_data_size            |
+| test_process_initialize_immutable_owner       |
+| test_process_set_authority_account            |
+
+| Failing nodes                           |
+|-----------------------------------------|
+| test_process_initialize_account         |
+| test_process_initialize_account2        |
+| test_process_initialize_account3        |
+| test_process_initialize_mint_freeze     |
+| test_process_initialize_mint2_freeze    |
+| test_process_initialize_mint_no_freeze  |
+| test_process_initialize_mint2_no_freeze |
+
+| Other issues                     |
+|----------------------------------|
+| test_process_amount_to_ui_amount |
+| test_process_ui_amount_to_amount |
+
+| Performance issues                         |
+|--------------------------------------------|
+| test_process_withdraw_excess_lamports_mint |
+| test_process_set_authority_mint            |
+
+
+| Missing Multisig cheat code                             |
+|---------------------------------------------------------|
+| test_process_withdraw_excess_lamports_multisig          |
+| test_process_approve_multisig                           |
+| test_process_approve_checked_multisig                   |
+| test_process_withdraw_excess_lamports_account_multisig  |
+| test_process_withdraw_excess_lamports_mint_multisig     |
+| test_process_withdraw_excess_lamports_multisig_multisig |
+| test_process_transfer_multisig                          |
+| test_process_mint_to_multisig                           |
+| test_process_burn_multisig                              |
+| test_process_close_account_multisig                     |
+| test_process_transfer_checked_multisig                  |
+| test_process_burn_checked_multisig                      |
+| test_process_revoke_multisig                            |
+| test_process_freeze_account_multisig                    |
+| test_process_thaw_account_multisig                      |
+| test_process_mint_to_checked_multisig                   |
+| test_process_set_authority_account_multisig             |
+| test_process_set_authority_mint_multisig                |
+| test_process_initialize_multisig                        |
+| test_process_initialize_multisig2                       |
+
+EOF