Conflicting cheat code use (`withdraw_excess_lamports`)

[jberthold]

The proof test_process_withdraw_excess_lamports showed an unexpected cheat code projection.
The proof gets stuck with the following K cell:

<k>
  #traverseProjection (
    toStack ( 2 , local ( 2 ) ) ,
    Aggregate ( variantIdx ( 0 ) , ListItem (Integer ( ARG_UINT1:Int , 8 , false ))
      ListItem (Integer ( ARG_UINT2:Int , 8 , false ))
      ListItem (Integer ( ARG_UINT3:Int , 8 , false ))
      ListItem (Integer ( ARG_UINT4:Int , 8 , false ))
... (this is input data representing an `AccountInfo` struct)
      ListItem (Integer ( ARG_UINT70:Int , 64 , false ))
      ListItem (Integer ( 165 , 64 , false ))
    ) , 
    PAccountIMint  .ProjectionElems ,
    CtxPAccountPAcc ( IAcc ( ...) ) )  .Contexts )
  ~> #derefTruncate ( noMetadata , projectionElemField ( fieldIdx ( 3 ) , ty ( 600077 ) )  .ProjectionElems )

• The #derefTruncate shows there was a Deref projection before
• Context CtxPAccountPAcc( IAcc(...)) shows we are accessing the Account structure of a PAccountAccount set up by cheatcode_is_account
• the remaining projection (in #derefTruncate wants to read field 3 (the integer with ARG_UINT3)

What is wrong is the PAccountIMint projection. This projection is out of place here for two reasons

1. There was no Mint set up, it must have been an interface account (IAcc in context)
2. We already projected to the Account so we cannot project to a second component any more.

After fixing the DELEGATE key branching issue, proof test_process_burn showed the same problem:
After running the whole proof,

the proof tree shows a number of stuck nodes.

┌─ 1  🌳 ROOT      ((root, init))       │ line     2
├─ 3     NORMAL                        │ line   719
├─ 4  🔀 SPLIT     ((split))            │ line  6542
┃  ├─ 5     NORMAL                        │ line 11849
┃  ├─ 7     NORMAL                        │ line 17153
┃  ├─ 9     NORMAL                        │ line 22991
┃  ├─ 10    NORMAL                        │ line 28830
┃  ├─ 11 🔀 SPLIT     ((split))            │ line 34153
┃  ┃  ├─ 12    NORMAL                        │ line 39531
┃  ┃  ├─ 14    NORMAL                        │ line 44906
┃  ┃  ├─ 16 🔀 SPLIT     ((split))            │ line 50810
┃  ┃  ┃  ├─ 18    NORMAL                        │ line 56189
┃  ┃  ┃  ├─ 22    NORMAL                        │ line 61565
┃  ┃  ┃  ├─ 26 🔀 SPLIT     ((split))            │ line 67050
┃  ┃  ┃  ┃  ├─ 30    NORMAL                        │ line 72429
┃  ┃  ┃  ┃  ├─ 38    NORMAL                        │ line 77805
┃  ┃  ┃  ┃  └─ 46 ❌ STUCK     ((stuck, leaf))      │ line 83199
┃  ┃  ┃     ├─ 31    NORMAL                        │ line 89198
┃  ┃  ┃     ├─ 39    NORMAL                        │ line 94574
┃  ┃  ┃     └─ 47 ❌ STUCK     ((stuck, leaf))      │ line 99961
┃  ┃     ├─ 19    NORMAL                        │ line 105960
┃  ┃     ├─ 23    NORMAL                        │ line 111336
┃  ┃     ├─ 27 🔀 SPLIT     ((split))            │ line 117249
┃  ┃     ┃  ├─ 32    NORMAL                        │ line 122629
┃  ┃     ┃  ├─ 40    NORMAL                        │ line 128006
┃  ┃     ┃  └─ 48 ❌ STUCK     ((stuck, leaf))      │ line 133401
┃  ┃        ├─ 33    NORMAL                        │ line 139401
┃  ┃        ├─ 41    NORMAL                        │ line 144778
┃  ┃        └─ 49 ❌ STUCK     ((stuck, leaf))      │ line 150166
┃     ├─ 13    NORMAL                        │ line 156197
┃     ├─ 15    NORMAL                        │ line 161572
┃     ├─ 17 🔀 SPLIT     ((split))            │ line 166985
┃     ┃  ├─ 20    NORMAL                        │ line 172394
┃     ┃  ├─ 24    NORMAL                        │ line 177800
┃     ┃  ├─ 28 🔀 SPLIT     ((split))            │ line 183347
┃     ┃  ┃  ├─ 34    NORMAL                        │ line 188756
┃     ┃  ┃  ├─ 42    NORMAL                        │ line 194162
┃     ┃  ┃  └─ 50 ❌ STUCK     ((stuck, leaf))      │ line 199586
┃     ┃     ├─ 35    NORMAL                        │ line 205615
┃     ┃     ├─ 43    NORMAL                        │ line 211021
┃     ┃     └─ 51 ❌ STUCK     ((stuck, leaf))      │ line 216438
┃        ├─ 21    NORMAL                        │ line 222467
┃        ├─ 25    NORMAL                        │ line 227873
┃        ├─ 29 🔀 SPLIT     ((split))            │ line 233816
┃        ┃  ├─ 36    NORMAL                        │ line 239226
┃        ┃  ├─ 44    NORMAL                        │ line 244633
┃        ┃  └─ 52 ❌ STUCK     ((stuck, leaf))      │ line 250058
┃           ├─ 37    NORMAL                        │ line 256088
┃           ├─ 45    NORMAL                        │ line 261495
┃           └─ 53 ❌ STUCK     ((stuck, leaf))      │ line 266913
   ├─ 6     NORMAL                        │ line 272943
   └─ 8  ❌ STUCK     ((stuck, leaf))      │ line 278247
┌─ 2  🌳 ROOT      ((root, leaf, target, terminal)) │ line 283581
📊 STATISTICS
════════════════════════════════════════
📈 Total nodes: 53
  ⚪ Normal      :  34
  🌳 Root        :   2
  🔀 Split       :   8
  ❌ Stuck       :   9
🎯 Proof Outcome:
  ❌ STUCK: 9 branch(es) got stuck

All stuck nodes except the last one have the same problem. The `--full-printer` proof tree is attached here:

test_process_burn-full.txt.gz

[Stevengre]

The problem might be (in test_process_burn):

929 |  cheatcode_is_mint(&accounts[1]);
...
948 |  let mint_owner = get_account(&accounts[1]).owner;

[Stevengre]

owner is from AccountInfo, therefore when we want an owner, we should use something like

let mint_owner = *accounts[1].owner();

• This branch is based on dc/multsig-flag that provides experimental changes: jh/29-unexpected-cheatcode-projection
• The following provides current exploration of the test_process_burn with the default setup:

Log before existing proof:

INFO 2025-09-30 08:21:28,212 pyk.kore.rpc - Sending request to localhost:38889: 132950329490752-013 - execute
INFO 2025-09-30 08:21:28,980 pyk.kore.rpc - [PID=2039479][stde] [proxy] Processing request 132950329490752-013
timeout: sending signal TERM to command ‘uv’

┌─ 1 (root, init)
│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
│   span: st/library/core/src/fmt/mod.rs:343
│
│  (200 steps)
├─ 3
│   #execTerminator ( terminator ( ... kind: assert ( ... cond: operandMove ( place
│   function: pinocchio_token_program::entrypoint::test_process_burn
│   span: ypoint-runtime-verification.rs:931
│
│  (200 steps)
├─ 4
│   #setArgsFromStack ( 2 , .Operands )
~> #execBlock ( basicBlock ( ... statements:
│   function: pinocchio_token_program::entrypoint::get_account
│   span: ypoint-runtime-verification.rs:359
│
│  (157 steps)
├─ 5 (split)
│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
│   function: <pinocchio_token_interface::state::account_state::AccountState as core::convert::TryFrom<u8>>::try_from
┃
┃ (branch)
┣━━┓ subst: .Subst
┃  ┃ constraint:
┃  ┃     notBool ?STATE:Int <=Int 2
┃  │
┃  ├─ 6
┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
┃  │   function: <pinocchio_token_interface::state::account_state::AccountState as core::convert::TryFrom<u8>>::try_from
┃  │
┃  │  (200 steps)
┃  ├─ 8
┃  │   #setUpCalleeData ( monoItemFn ( ... name: symbol ( "core::result::Result::<&pino
┃  │   function: core::result::Result::<&pinocchio_token_interface::state::account::Account, pinocchio::program_error::ProgramError>::unwrap
┃  │   span: ust/library/core/src/result.rs:1102
┃  │
┃  │  (200 steps)
┃  ├─ 10
┃  │   Aggregate ( variantIdx ( 0 ) , ListItem (Reference ( 3 , place ( ... local: loca
┃  │   function: core::result::Result::<&pinocchio_token_interface::state::account::Account, pinocchio::program_error::ProgramError>::unwrap
┃  │   span: ust/library/core/src/result.rs:1102
┃  │
┃  │  (200 steps)
┃  ├─ 11
┃  │   #setLocalValue ( place ( ... local: local ( 43 ) , projection: .ProjectionElems
┃  │   function: pinocchio_token_program::entrypoint::test_process_burn
┃  │   span: ypoint-runtime-verification.rs:940
┃  │
┃  │  (200 steps)
┃  ├─ 12
┃  │   operandCopy ( place ( ... local: local ( 50 ) , projection: .ProjectionElems ) )
┃  │   function: pinocchio_token_program::entrypoint::test_process_burn
┃  │   span: ypoint-runtime-verification.rs:941
┃  │
┃  │  (200 steps)
┃  └─ 13 (leaf, pending)
┃      #mkPAccByteRef ( place ( ... local: local ( 2 ) , projection: .ProjectionElems )
┃      function: pinocchio_token_program::entrypoint::get_account
┃
┗━━┓ subst: .Subst
   ┃ constraint:
   ┃     ?STATE:Int <=Int 2
   │
   ├─ 7
   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
   │   function: <pinocchio_token_interface::state::account_state::AccountState as core::convert::TryFrom<u8>>::try_from
   │
   │  (186 steps)
   └─ 9 (stuck, leaf)
       #traverseProjection ( toLocal ( 2 ) , AllocRef ( allocId ( 600604 ) , .Projectio
       function: <pinocchio_token_interface::state::account_state::AccountState as core::cmp::PartialEq>::eq
       span: ace/src/state/account_state.rs:4


┌─ 2 (root, leaf, target, terminal)
│   #EndProgram ~> .K



STATISTICS
-----------
Total nodes: 11

Node roles (exclusive):
  pending : 1  ids: 13
  failing : 1  ids: 9
  split   : 1  ids: 5
  normal  : 8  ids: 3, 4, 6, 7, 8, 10, 11, 12
  (root nodes omitted from totals: 1, 2)

Leaf paths from init:
  total leaves (non-root): 2
  reachable leaves       : 2
  total steps            : 2300

  leaf 9: steps 743, path 1 -> 3 -> 4 -> 5 -> 7 -> 9
  leaf 13: steps 1557, path 1 -> 3 -> 4 -> 5 -> 6 -> 8 -> 10 -> 11 -> 12 -> 13

LEAF <k> CELLS
---------------
Node 9:
  #traverseProjection ( toLocal ( 2 ) , AllocRef ( allocId ( 600604 ) , .ProjectionElems , noMetadata ) , projectionElemDeref  .ProjectionElems , .Contexts )
  ~> #readProjection ( false )
  ~> #freezer#discriminant(_,_)_RT-DATA_Evaluation_Evaluation_MaybeTy0_ ( ty ( 600110 ) ~> .K )
  ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place ( ... local: local ( 4 ) , projection: .ProjectionElems ) ~> .K )
  ~> #execStmts ( statement ( ... kind: statementKindAssign ( ... place: place ( ... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place ( ... local: local ( 3 ) , projection: .ProjectionElems ) ) , operandCopy ( place ( ... local: local ( 4 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 619141 ) )  .Statements )
  ~> #execTerminator ( terminator ( ... kind: terminatorKindReturn , span: span ( 619140 ) ) )

Node 13:
  #mkPAccByteRef ( place ( ... local: local ( 2 ) , projection: .ProjectionElems ) , PtrLocal ( 2 , place ( ... local: local ( 3 ) , projection: .ProjectionElems ) , mutabilityNot , ptrEmulation ( noMetadata ) ) , mutabilityNot )
  ~> #execBlockIdx ( basicBlockIdx ( 1 ) )

[jberthold]

Inspecting test_process_withdraw_excess_lamports (running on the latest setup as of 2025 10 03) shows the same misguided projection: an Account has been set up but some code attempts to access it as a Mint.
Looking at the property code, indeed account[0] is accessed both as an Account and as a Mint in the value extraction before the function under test is running.

solana-token/p-token/src/entrypoint-runtime-verification.rs

Lines 3368 to 3371 in 77df1ea

	let src_account_owner = get_account(&accounts[0]).owner;
	let src_account_is_native = get_account(&accounts[0]).is_native();
	let src_mint_initialised = get_mint(&accounts[0]).is_initialized();
	let src_mint_mint_authority = get_mint(&accounts[0]).mint_authority().cloned();

The best solution is probably to split this test into the two cases, removing code that relates to the Mint case from the original.

[jberthold]

Fixed in #40 , splitting the proof.