[PROVING] `test_process_initialize_account`

[Stevengre]

STATUS:

• Pending without un-expected behavior, except for the Float branching.
• Node 8 looks suspicious with #execTerminator

TODOS:

• Same as [PROVING] test_process_initialize_mint_freeze #4
• Investigate more on Node 8

[Stevengre]

• Branch: jh/kmir-exec-test-setup
• Commit: fd2df2d (Remove analysis documentation files from test-properties)

┌─ 1  🌳 ROOT      ((root, init))       │ line     2
├─ 3     NORMAL                        │ line   905
├─ 4     NORMAL                        │ line  2231
├─ 5  🔀 SPLIT     ((split))            │ line  3177
┃  ├─ 6     NORMAL                        │ line  4135
┃  └─ 8  ❌ STUCK     ((stuck, leaf))      │ line  5090
   ├─ 7     NORMAL                        │ line  6047
   ├─ 9     NORMAL                        │ line  7002
   ├─ 10    NORMAL                        │ line  8204
   ├─ 11 🔀 SPLIT     ((split))            │ line  9178
   ┃  ├─ 12    NORMAL                        │ line 10158
   ┃  ├─ 14 🔀 SPLIT     ((split))            │ line 11135
   ┃  ┃  ├─ 16    NORMAL                        │ line 12120
   ┃  ┃  └─ 20 ❌ STUCK     ((stuck, leaf))      │ line 13102
   ┃     ├─ 17    NORMAL                        │ line 14087
   ┃     ├─ 21 🔀 SPLIT     ((split))            │ line 15069
   ┃     ┃  ├─ 24    NORMAL                        │ line 16056
   ┃     ┃  └─ 28 ❌ STUCK     ((stuck, leaf))      │ line 17040
   ┃        ├─ 25    NORMAL                        │ line 18027
   ┃        ├─ 29    NORMAL                        │ line 19011
   ┃        └─ 32 ⏳ PENDING   ((leaf, pending))    │ line 19965
      ├─ 13    NORMAL                        │ line 20924
      ├─ 15 🔀 SPLIT     ((split))            │ line 21901
      ┃  ├─ 18    NORMAL                        │ line 22886
      ┃  └─ 22 ❌ STUCK     ((stuck, leaf))      │ line 23868
         ├─ 19    NORMAL                        │ line 24853
         ├─ 23 🔀 SPLIT     ((split))            │ line 25835
         ┃  ├─ 26    NORMAL                        │ line 26822
         ┃  └─ 30 ❌ STUCK     ((stuck, leaf))      │ line 27806
            ├─ 27    NORMAL                        │ line 28793
            ├─ 31 🔀 SPLIT     ((split))            │ line 29777
            ┃  └─ 33 ⏳ PENDING   ((leaf, pending))    │ line 30768
               └─ 34 ⏳ PENDING   ((leaf, pending))    │ line 31759
┌─ 2  🌳 ROOT      ((root, leaf, target, terminal)) │ line 32747

📊 STATISTICS
════════════════════════════════════════
📈 Total nodes: 34

  ⚪ Normal      :  17
  ⏳ Pending     :   3
  🌳 Root        :   2
  🔀 Split       :   7
  ❌ Stuck       :   5

🎯 Proof Outcome:
  ❌ STUCK: 5 branch(es) got stuck
  ⏳ PENDING: 3 branch(es) still pending

[Stevengre]

All Split Nodes and Branch Condition Analysis:

1. Node 5 - Account State Check (entrypoint::get_account)

• Condition: ?STATE ≤ 2
• Node 6: When STATE > 2 (account state greater than 2)
• Node 7: When STATE ≤ 2 (account state less than or equal to 2)

2. Node 11 - Floating Point Threshold Comparison (Rent::is_default_rent_threshold)

• Condition: Float(?_EXEMPT_THRESHOLD) == 2.0
• Node 12: When threshold equals 2.0
• Node 13: When threshold does not equal 2.0

3. Node 14 & 15 - Addition Overflow Check (Rent::minimum_balance)

• Condition: Check if ARG_UINT71 + 128 overflows
• Node 16/18: When no overflow occurs
• Node 17/19: When overflow occurs
• Same overflow check pattern as the previous two specs

4. Node 21 & 23 - Multiplication Overflow Check (Rent::minimum_balance)

• Condition: Check if (ARG_UINT71 + 128) * LMP_PER_BYTEYEAR overflows
• Node 24/26: When no overflow occurs
• Node 25/27: When overflow occurs

5. Node 31 - Multiplication Overflow Check (Rent::minimum_balance)

• Condition: Check if (ARG_UINT71 + 128) * LMP_PER_BYTEYEAR * 2 overflows
• Node 33: When no overflow occurs
• Node 34: When overflow occurs

[Stevengre]

Summary Analysis of All Leaf Node Status:

STUCK Nodes (5 nodes):

1. Node 8 - Stuck during terminatorKindCall execution in ty(600773)

   • Special: This is the only STUCK node not in Rent::minimum_balance
   • Related to invalid account state (STATE > 2) path

2. Node 20, 22 - Addition overflow AssertError(binOpAdd, 128 + local(3))

   • Both in ty(600759) = Rent::minimum_balance
   • Caller: ty(600436)

3. Node 28, 30 - Multiplication overflow AssertError(binOpMul)

   • Node 28: local(14) × local(16)
   • Node 30: local(6) × local(8)
   • Both in ty(600759) = Rent::minimum_balance

PENDING Nodes (3 nodes):

1. Node 32 - Processing complex pointer and projection operations in ty(600497)

   • #traverseProjection and #readProjection operations
   • Involves dereferencing (projectionElemDeref)

2. Node 33, 34 - In ty(600759) = Rent::minimum_balance

   • Waiting for multiplication overflow check (ARG_UINT71 + 128) * LMP_PER_BYTEYEAR * 2
   • Both nodes are in the same #expect state

[Stevengre]

Analysis of Node 8

This is the core::result::unwrap_failed function, which is a panic function in the Rust standard library that is triggered when Result::unwrap() is called on an Err value.

So ty(600118) does exist in SMIR as a normal symbol (NormalSym) corresponding to core::result::unwrap_failed. This explains why Node 8 gets stuck - it is attempting to call a panic function that never returns.

#execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandConstant ( constOperand ( ... span: span ( 603488 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindZeroSized , ty: ty ( 600118 ) , id: mirConstId ( 39 ) ) ) ) , args: operandConstant ( constOperand ( ... span: span ( 603489 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00+\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... provSize: 0 , allocId: allocId ( 55 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 600073 ) , id: mirConstId ( 378 ) ) ) )  operandMove ( place ( ... local: local ( 5 ) , projection: .ProjectionElems ) )  .Operands , destination: place ( ... local: local ( 4 ) , projection: .ProjectionElems ) , target: noBasicBlockIdx , unwind: unwindActionCleanup ( basicBlockIdx ( 4 ) ) ) , span: span ( 603490 ) ) ) ~> .K

[600118, {'NormalSym': '_ZN4core6result13unwrap_failed17h698bf754bc36b600E'}]