Skip to content

Commit beed3f4

Browse files
jbertholdjberthold
authored
Script updates: new defaults, no dirty, new helper script (#90)
* update defaults in `run-proofs.sh`: max-depth 2000, max-iterations 500 , timeout 1h * remove the `-dirty` suffixing in the `run-proofs.sh` script (not useful) * new helper script to select proofs from a group (groups stored within the script) * update `VERIFICATION_GUIDE.md` to reflect reality better and mention assumptions we make in cheat codes.
1 parent 31c5fec commit beed3f4

File tree

5 files changed

+140
-45
lines changed

5 files changed

+140
-45
lines changed

‎.github/workflows/rv-run-proofs.yaml‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ on:
3030
description: Timeout for running the proofs
3131
required: false
3232
type: string
33-
default: 7200 # 2h
33+
default: 3600 # 1h
3434
concurrency:
3535
group: ${{ github.workflow }}-${{ github.ref }}
3636
cancel-in-progress: true
@@ -85,7 +85,7 @@ jobs:
8585
;;
8686
esac
8787
88-
- name: "Build with stable_mir_json"
88+
- name: "Build with stable_mir_json"
8989
run: |
9090
cd "${{ steps.vars.outputs.crate_dir }}"
9191
RUSTC=stable_mir_json cargo build --features runtime-verification
@@ -178,8 +178,8 @@ jobs:
178178
kmir prove-rs --smir "artefacts/${{ needs.compile.outputs.artifact_name }}.json" \
179179
--start-symbol "${{ needs.compile.outputs.start_prefix }}${{ matrix.proof }}" \
180180
--verbose \
181-
--max-depth 500 \
182-
--max-iterations 100 \
181+
--max-depth 2000 \
182+
--max-iterations 500 \
183183
--proof-dir artefacts/proof \
184184
|| echo "Runner signals proof failure"
185185

‎p-token/test-properties/VERIFICATION_GUIDE.md‎

Lines changed: 30 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ This guide explains how to run formal verification for the p-token Solana progra
66

77
## Architecture
88

9-
After the merge of `dc/test-hack` branch, the codebase uses conditional compilation to separate production and verification code:
9+
The codebase uses conditional compilation to separate production and verification code:
1010

1111
- **Production code**: `src/entrypoint.rs` - Used for normal builds
1212
- **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
1919
fn cheatcode_is_account(_: &AccountInfo) {}
2020
fn cheatcode_is_mint(_: &AccountInfo) {}
2121
fn cheatcode_is_rent(_: &AccountInfo) {}
22-
fn cheatcode_is_multisig(_: &AccountInfo) {} // Currently unsupported and behind feature flag "multisig"
22+
fn cheatcode_is_multisig(_: &AccountInfo) {} // Currently unsupported
2323
```
2424

25-
These functions are no-ops at runtime but provide type hints to the verification tools.
25+
These functions are no-ops at runtime but set up data required for the verification.
26+
27+
### Assumptions implemented in cheat codes
28+
29+
* Calling `cheatcode_is_{account,mint,multisig,rent}` asserts that the `Account` pointed-to by `AccountInfo`
30+
is followed in memory by the respective data structure, `state::account::Account`, `state::mint::Mint`,
31+
`state::multisig::Multisig`, or `sysvars::rent::Rent`.
32+
* The cheat codes will set the data length (`data_len`) of the `AccountInfo` to the correct value for the underlying object:
33+
| Object | `data_len` |
34+
|--------- | ---------- |
35+
| Account | 165 |
36+
| Mint | 82 |
37+
| Rent | 17 |
38+
| Multisig | 355 |
39+
* For the `Rent` sysvar, the proofs make additional assumptions to avoid overflows and imprecise `Float` computation:
40+
- The `lamports_per_byteyear` is assumed to be less than `2^32` (to avoid overflows during rent computation).
41+
- The `exemption_threshold` is fixed to value `2.0` (default). This means that computations will be performed in `u64`.
42+
- The `burn_percent` value is assumed to be between 0 and 100 (to avoid underflows during rent computation).
43+
* Access to the data structure is provided by intercepting the following Rust functions:
44+
- `AccountInfo::borrow_data_unchecked` and `AccountInfo::borrow_mut_data_unchecked`
45+
- `Transmutable::load_unchecked` and `Transmutable::load_mut_unchecked` for the instances `Account`, `Mint`, `Multisig`
46+
- `sysvars::rent::Rent::from_bytes_unchecked` and `sysvars::rent::Rent::get`
47+
and replacing their function body execution by an effect that provides the desired access (read-only or mutable).
2648

2749
## Running Verification
2850

@@ -56,10 +78,7 @@ cd test-properties
5678
./run-verification.sh -t 600 test_process_transfer
5779

5880
# With custom prove-rs options
59-
./run-verification.sh -o "--max-iterations 50 --max-depth 300" test_process_transfer
60-
61-
# With multisig feature enabled
62-
./run-verification.sh --multisig test_process_transfer
81+
./run-verification.sh -o "--max-iterations 50 --max-depth 200" test_process_transfer
6382
```
6483

6584
## Test Functions
@@ -69,21 +88,12 @@ All test functions are located in `src/entrypoint-runtime-verification.rs` and f
6988
- Each function has cheatcode calls at the beginning to mark account types
7089
- Functions use fixed-size arrays for formal verification compatibility
7190

72-
## Feature Flags
73-
74-
### runtime-verification
91+
## Feature Flag `runtime-verification`
7592
Required for all verification tests. Enables the verification-specific entrypoint (entrypoint-runtime-verification.rs) and test functions.
7693

77-
### multisig (optional)
78-
Enables cheat codes for all Owner / Authority accounts to be `Multisig` (by default these are `Account`). When enabled:
79-
- Owner / Authority accounts are instantiated as `Multisig` with symbolic arguments via `cheatcode_is_multisig` (TODO: not implemented yet)
80-
- `Multisig`-specific validation logic is included in proof harnesses
81-
82-
Use `--multisig` flag with run-verification.sh to enable this feature.
83-
8494
## Available Tests
8595

86-
See `tests.md` for the complete list of available test functions and their current status.
96+
See `proofs.md` for the complete list of available test functions.
8797

8898
## Troubleshooting
8999

@@ -96,14 +106,7 @@ If you get errors about the entrypoint module not being found, ensure you're bui
96106
cargo build --features runtime-verification
97107
```
98108

99-
### Multisig Support
100-
To enable multisig account validation in verification tests, use both features:
101-
```bash
102-
cargo build --features "runtime-verification,multisig"
103-
```
104-
105109
## Notes
106110

107-
- The verification process can take significant time (20+ minutes per test)
108-
- Default settings: max-depth 200, max-iterations 30, timeout 1200s
109-
- Results are stored in `artefacts/proof/` directory
111+
- Default settings: max-depth 2000, max-iterations 500, timeout 1h
112+
- 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/mir-semantics‎

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

Lines changed: 16 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,12 @@
33
# Run all start symbols given as arguments (or read them from proofs.md
44
# table if -a given) with given run options (-o) and timeout (-t).
55
# Options and defaults:
6-
# -t NUM : timeout in seconds (default 7200)
7-
# -o STRING: prove-rs options. Default "--max-iterations 100 --max-depth 500"
6+
# -t NUM : timeout in seconds (default 1h=3600)
7+
# -o STRING: prove-rs options. Default "--max-iterations 500 --max-depth 2000"
88
# -a : run all start symbols from first table in `proofs.md` (1st column)
99
# -m : run all start symbols from multisig table in `proofs.md` (2nd column)
1010
# -c : continue existing proofs instead of reloading (which is default)
11+
# -l FILE : log output to file "$NAME.PID" instead of stdout
1112
#
1213
# Always runs verbosely, always uses artefacts/proof
1314
# as proof directory
@@ -22,18 +23,22 @@ ARTIFACT_BASENAME="${ARTIFACT_BASENAME:-p-token}"
2223
ALL_NAMES=$(sed -n -e 's/^| \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md)
2324
MULTISIG_NAMES=$(sed -n -e 's/^| m | \(test_p[a-zA-Z0-9:_]*\) *|.*/\1/p' proofs.md)
2425

25-
TIMEOUT=7200
26-
PROVE_OPTS="--max-iterations 100 --max-depth 500"
26+
TIMEOUT=3600
27+
PROVE_OPTS="--max-iterations 500 --max-depth 2000"
2728
RELOAD_OPT="--reload"
29+
LOG_FILE=""
2830

29-
while getopts ":t:o:amc" opt; do
31+
while getopts ":t:o:l:amc" opt; do
3032
case $opt in
3133
t)
3234
TIMEOUT=$OPTARG
3335
;;
3436
o)
3537
PROVE_OPTS=$OPTARG
3638
;;
39+
l)
40+
LOG_FILE="$OPTARG.$$"
41+
;;
3742
a)
3843
TESTS=${ALL_NAMES}
3944
;;
@@ -55,25 +60,23 @@ shift $((OPTIND-1))
5560

5661
# Collect tests
5762
if [ -z "$TESTS" ]; then
58-
if [ -z "$@" ]; then
63+
if [ "$#" -eq 0 ]; then
5964
echo "[ERROR] No test function names given. Use -a or provide at least one name." 1>&2
6065
exit 2
6166
fi
6267
TESTS=$@
6368
fi
6469

70+
if [ ! -z "$LOG_FILE" ]; then
71+
echo "[INFO] Logging output to file $LOG_FILE instead of stdout"
72+
exec &> $LOG_FILE
73+
fi
74+
6575
set -u
6676

6777
REPO_COMMIT=$(git rev-parse --short HEAD 2>/dev/null || echo "unknown")
68-
if git status --porcelain 1>/dev/null 2>&1 && [ -n "$(git status --porcelain 2>/dev/null)" ]; then
69-
REPO_COMMIT="${REPO_COMMIT}-dirty"
70-
fi
7178

7279
MIR_COMMIT=$(git -C mir-semantics rev-parse --short HEAD 2>/dev/null || echo "unknown")
73-
if git -C mir-semantics status --porcelain 1>/dev/null 2>&1 && \
74-
[ -n "$(git -C mir-semantics status --porcelain 2>/dev/null)" ]; then
75-
MIR_COMMIT="${MIR_COMMIT}-dirty"
76-
fi
7780

7881
PROOF_DIR="${ARTIFACTS_DIR:-artefacts}/proof-${REPO_COMMIT}-${MIR_COMMIT}"
7982
mkdir -p "${PROOF_DIR}"

‎p-token/test-properties/select-proofs.sh‎

Lines changed: 89 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,89 @@
1+
# /bin/bash
2+
#
3+
# Usage: ./select-proofs.sh "Table Header"
4+
# - select the proofs from one of the tables in the file
5+
# (the first match will be taken)
6+
##########################################################
7+
8+
USAGE=$(head -6 $0)
9+
10+
if [ -z "$1" ]; then
11+
head -6 $0
12+
exit 1
13+
fi
14+
15+
HEADING="$1"
16+
17+
if ! (grep -e "^| $HEADING" $0 > /dev/null); then
18+
echo "[ERROR] '| $HEADING..': not a table header. Must provide a table heading to select proofs."
19+
exit 1
20+
fi
21+
22+
sed -n -e "/^| ${HEADING}.*/,/^\$/ {/| ${HEADING}.*/d; /^\$/q; s/^| \(test_p[a-zA-Z0-9_]*\) .*/\1/p}" <<EOF
23+
24+
| Passing |
25+
|-----------------------------------------------|
26+
| test_ptoken_domain_data |
27+
| test_process_burn |
28+
| test_process_approve_checked |
29+
| test_process_withdraw_excess_lamports_account |
30+
| test_process_transfer |
31+
| test_process_mint_to |
32+
| test_process_approve |
33+
| test_process_close_account |
34+
| test_process_sync_native |
35+
| test_process_burn_checked |
36+
| test_process_revoke |
37+
| test_process_freeze_account |
38+
| test_process_thaw_account |
39+
| test_process_mint_to_checked |
40+
| test_process_transfer_checked |
41+
| test_process_get_account_data_size |
42+
| test_process_initialize_immutable_owner |
43+
| test_process_set_authority_account |
44+
45+
| Failing nodes |
46+
|-----------------------------------------|
47+
| test_process_initialize_account |
48+
| test_process_initialize_account2 |
49+
| test_process_initialize_account3 |
50+
| test_process_initialize_mint_freeze |
51+
| test_process_initialize_mint2_freeze |
52+
| test_process_initialize_mint_no_freeze |
53+
| test_process_initialize_mint2_no_freeze |
54+
55+
| Other issues |
56+
|----------------------------------|
57+
| test_process_amount_to_ui_amount |
58+
| test_process_ui_amount_to_amount |
59+
60+
| Performance issues |
61+
|--------------------------------------------|
62+
| test_process_withdraw_excess_lamports_mint |
63+
| test_process_set_authority_mint |
64+
65+
66+
| Missing Multisig cheat code |
67+
|---------------------------------------------------------|
68+
| test_process_withdraw_excess_lamports_multisig |
69+
| test_process_approve_multisig |
70+
| test_process_approve_checked_multisig |
71+
| test_process_withdraw_excess_lamports_account_multisig |
72+
| test_process_withdraw_excess_lamports_mint_multisig |
73+
| test_process_withdraw_excess_lamports_multisig_multisig |
74+
| test_process_transfer_multisig |
75+
| test_process_mint_to_multisig |
76+
| test_process_burn_multisig |
77+
| test_process_close_account_multisig |
78+
| test_process_transfer_checked_multisig |
79+
| test_process_burn_checked_multisig |
80+
| test_process_revoke_multisig |
81+
| test_process_freeze_account_multisig |
82+
| test_process_thaw_account_multisig |
83+
| test_process_mint_to_checked_multisig |
84+
| test_process_set_authority_account_multisig |
85+
| test_process_set_authority_mint_multisig |
86+
| test_process_initialize_multisig |
87+
| test_process_initialize_multisig2 |
88+
89+
EOF

0 commit comments

Comments
 (0)