[PROVING] `test_process_initialize_mint_freeze`

[Stevengre]

Branch & Commit

• Branch: jh/kmir-exec-test-setup
• Commit: fd2df2d (Remove analysis documentation files from test-properties)
• Proof file: artefacts/proof/entrypoint::test_process_initialize_mint_freeze-full.txt

🌲 PROOF TREE STRUCTURE

  ┌─ 1  🌳 ROOT      ((root, init))       │ line     2
  ├─ 3     NORMAL                        │ line   669
  ├─ 4     NORMAL                        │ line  1610
  ├─ 5  🔀 SPLIT     ((split))            │ line  2396
  ┃  ├─ 6     NORMAL                        │ line  3184
  ┃  ├─ 8  🔀 SPLIT     ((split))            │ line  3969
  ┃  ┃  ├─ 10    NORMAL                        │ line  4762
  ┃  ┃  └─ 14 ❌ STUCK     ((stuck, leaf))      │ line  5552
  ┃     ├─ 11    NORMAL                        │ line  6345
  ┃     ├─ 15 🔀 SPLIT     ((split))            │ line  7135
  ┃     ┃  ├─ 18    NORMAL                        │ line  7930
  ┃     ┃  └─ 22 ❌ STUCK     ((stuck, leaf))      │ line  8722
  ┃        ├─ 19    NORMAL                        │ line  9517
  ┃        ├─ 23    NORMAL                        │ line 10309
  ┃        ├─ 26 🔀 SPLIT     ((split))            │ line 11083
  ┃        ┃  ├─ 29    NORMAL                        │ line 11842
  ┃        ┃  └─ 33 ⏳ PENDING   ((leaf, pending))    │ line 12598
  ┃           ├─ 30    NORMAL                        │ line 13478
  ┃           └─ 34 ⏳ PENDING   ((leaf, pending))    │ line 14234
     ├─ 7     NORMAL                        │ line 15113
     ├─ 9  🔀 SPLIT     ((split))            │ line 15898
     ┃  ├─ 12    NORMAL                        │ line 16691
     ┃  └─ 16 ❌ STUCK     ((stuck, leaf))      │ line 17481
        ├─ 13    NORMAL                        │ line 18274
        ├─ 17 🔀 SPLIT     ((split))            │ line 19064
        ┃  ├─ 20    NORMAL                        │ line 19859
        ┃  └─ 24 ❌ STUCK     ((stuck, leaf))      │ line 20651
           ├─ 21    NORMAL                        │ line 21446
           ├─ 25 🔀 SPLIT     ((split))            │ line 22238
           ┃  ├─ 27    NORMAL                        │ line 23037
           ┃  └─ 31 ❌ STUCK     ((stuck, leaf))      │ line 23833
              ├─ 28    NORMAL                        │ line 24632
              └─ 32 ⏳ PENDING   ((leaf, pending))    │ line 25428
  ┌─ 2  🌳 ROOT      ((root, leaf, target, terminal)) │ line 26184

  📊 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]

Node 5 Investigation

• Why? It is a Split
• How? Check its branch condition

#switchMatch(
  0,
  thunk(
    #applyBinOp(
      binOpEq,
      thunk(
        #cast(
          thunk(
            #cast(
              thunk(
                #cast(
                  Float(?_EXEMPT_THRESHOLD:Float, 64),
                  castKindTransmute,
                  ty(601115),
                  ty(600142)
                )
              ),
              castKindTransmute,
              ty(600142),
              ty(600676)
            )
          ),
          castKindTransmute,
          ty(600676),
          ty(600142)
        )
      ),
      Integer(4611686018427387904, 64, false),
      false
    )
  )
)

• function: pinocchio::sysvars::rent::Rent::minimum_balance

Root Cause (GUESS)

The branch occurs because:

1. Symbolic float variable: ?_EXEMPT_THRESHOLD:Float represents Solana's rent exemption threshold
2. Expected value: 2.0 years (Solana's standard rent exemption period)
3. Type conversion: Triple castKindTransmute operations convert float to integer representation
4. Comparison: Checks if exemption threshold equals default 2.0 value vs other values

Business Logic

This implements Solana's rent exemption rule where accounts need balance equivalent to 2 years of rent to be exempt. The symbolic executor cannot determine the concrete value of ?_EXEMPT_THRESHOLD:Float, forcing exploration of both branches.

Technical Issue

This is a known Solana ecosystem problem (issue #23854): using floating-point values in sysvars creates unnecessary complexity for formal verification tools.

Possible Solution Open to Discuss

• Implement #cast( ... , castKindTransmute, ...) for Float type;

Not easy to handle this specific case. Need a systematic design for the casting and type system.

• Provide a specific rule for ?_EXEMPT_THRESHOLD to regard it as an integer

Using pyk to transform this unsolved pattern to something that is easy to reason about

• Change the code from float to integer.

Easy to implement, hard to be accepted. As for the issue for this float type is recognized at 2022, and it is still here for now.

[Stevengre]

Node 8 branch point:

  #expect ( BoolVal ( notBool ARG_UINT71:Int +Int 128 &Int 18446744073709551615 ==Int ARG_UINT71:Int +Int 128 ) , false ,
  assertMessageOverflow ( binOpAdd , operandConstant ( ... bytes: b"\x80\x00\x00\x00\x00\x00\x00\x00" ... ) , operandCopy ( place (
   ... local: local ( 3 ) ... ) ) ) )
  Function context: pinocchio::sysvars::rent::Rent::minimum_balance

Node 10 condition:

constraint: notBool notBool ARG_UINT71:Int +Int 128 &Int 18446744073709551615 ==Int ARG_UINT71:Int +Int 128 ==Bool false

Node 11 condition:

constraint: notBool ARG_UINT71:Int +Int 128 &Int 18446744073709551615 ==Int ARG_UINT71:Int +Int 128 ==Bool false

This is an overflow check branch, checking whether ARG_UINT71 + 128 will overflow (whether it equals itself after AND operation with mask 18446744073709551615 = 0xFFFFFFFFFFFFFFFF).

[Stevengre]

1. Nodes 8, 9: Addition overflow check ARG_UINT71 + 128
2. Nodes 15, 17: Multiplication overflow check (ARG_UINT71 + 128) * LMP_PER_BYTEYEAR
3. Node 25: Multiplication overflow check (ARG_UINT71 + 128) * LMP_PER_BYTEYEAR * 2
4. Node 26: Not an overflow check - this is a switch statement that selects different branches based on the ?INITIALISED value:
   • When value is 0, jumps to basicBlockIdx(3)
   • When value is 1, jumps to basicBlockIdx(2)
   • Other values jump to basicBlockIdx(1)

[Stevengre]

All STUCK nodes are in function ty(600759) (i.e., Rent::minimum_balance), all stuck due to arithmetic overflow assertion errors:

1. Node 14 & 16: Addition overflow - #ProgramError(AssertError(assertMessageOverflow(binOpAdd, ...)))
   • Involves addition of constant 128 (b"\x80\x00\x00\x00\x00\x00\x00\x00") with local(3)
2. Node 22 & 24: Multiplication overflow - #ProgramError(AssertError(assertMessageOverflow(binOpMul, ...)))
   • Node 22: local(14) × local(16)
   • Node 24: local(6) × local(8)
3. Node 31: Multiplication overflow - #ProgramError(AssertError(assertMessageOverflow(binOpMul, ...)))
   • local(5) × constant 2 (b"\x02\x00\x00\x00\x00\x00\x00\x00")

[Stevengre]

Except for the Float thing, it looks good to me overall, just need to investigate further, therefore here is what to do next:

• Modify run_proofs.sh to allow continuous proof.