issue(spl): NDBranches caused by `#traverseProjection` with `#adjustRef`

[Stevengre]

In test_process_burn, NDBranches are caused by the following term

│           #traverseProjection ( toStack ( 4 , local ( 91 ) ) , #adjustRef ( ?SplIsNativeCOpt:Value , 3 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│              ))
│            ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplTokenOwnerKey:List ))
│              ))
│            ListItem (Integer ( ?SplAmount:Int , 64 , false ))
│            ListItem (#adjustRef ( ?SplDelegateCOpt:Value , 3 ))
│            ListItem (Integer ( ?SplAccountState:Int , 8 , false ))
│            ListItem (#adjustRef ( ?SplIsNativeCOpt:Value , 3 ))
│            ListItem (Integer ( ?SplDelegatedAmount:Int , 64 , false ))
│            ListItem (#adjustRef ( ?SplCloseAuthCOpt:Value , 3 ))
│            , 5 , ty ( 5800474 ) )  CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│                ))
│              ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplTokenOwnerKey:List ))
│                ))
│              ListItem (Integer ( ?SplAmount:Int , 64 , false ))
│              ListItem (#adjustRef ( ?SplDelegateCOpt:Value , 3 ))
│              ListItem (Integer ( ?SplAccountState:Int , 8 , false ))
│              ListItem (#adjustRef ( ?SplIsNativeCOpt:Value , 3 ))
│              ListItem (Integer ( ?SplDelegatedAmount:Int , 64 , false ))
│              ListItem (#adjustRef ( ?SplCloseAuthCOpt:Value , 3 ))
│              ))
│            , 0 , ty ( 5800463 ) )  CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│                  ))
│                ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplTokenOwnerKey:List ))
│                  ))
│                ListItem (Integer ( ?SplAmount:Int , 64 , false ))
│                ListItem (#adjustRef ( ?SplDelegateCOpt:Value , 3 ))
│                ListItem (Integer ( ?SplAccountState:Int , 8 , false ))
│                ListItem (#adjustRef ( ?SplIsNativeCOpt:Value , 3 ))
│                ListItem (Integer ( ?SplDelegatedAmount:Int , 64 , false ))
│                ListItem (#adjustRef ( ?SplCloseAuthCOpt:Value , 3 ))
│                ))
│              ))
│            , 0 , ty ( 5800482 ) )  .Contexts )

My initial thought is that this is caused by the uninterpreted #adjustRef.
Another possible solution is to unwrap the insider of these symbolic values.

• reproduce this with small program;

[Stevengre]

In test_process_set_authority_account

├─ 4
│     <generatedTop>
│       <kmir>
│         <k>
│           #traverseProjection ( toStack ( 2 , local ( 54 ) ) , #adjustRef ( ?SplCloseAuthCOpt:Value , 1 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│              ))

[Stevengre]

In test_process_set_authority_mint:

├─ 3
│     <generatedTop>
│       <kmir>
│         <k>
│           #traverseProjection ( toStack ( 2 , local ( 38 ) ) , #adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (#adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ))
│            ListItem (Integer ( ?SplMintSupply:Int , 64 , false ))
│            ListItem (Integer ( ?SplMintDecimals:Int , 8 , false ))
│            ListItem (BoolVal ( false ))
│            ListItem (#adjustRef ( ?SplMintFreezeAuthorityCOpt:Value , 1 ))
│            , 0 , ty ( 5800443 ) )  CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (#adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ))
│              ListItem (Integer ( ?SplMintSupply:Int , 64 , false ))
│              ListItem (Integer ( ?SplMintDecimals:Int , 8 , false ))
│              ListItem (BoolVal ( false ))
│              ListItem (#adjustRef ( ?SplMintFreezeAuthorityCOpt:Value , 1 ))
│              ))

[Stevengre]

Same in test_process_thaw_account

├─ 4
│     <generatedTop>
│       <kmir>
│         <k>
│           #traverseProjection ( toStack ( 4 , local ( 50 ) ) , #adjustRef ( ?SplIsNativeCOpt:Value , 3 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│              ))
│            ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplTokenOwnerKey:List ))
│              ))
│            ListItem (Integer ( ?SplAmount:Int , 64 , false ))
│            ListItem (#adjustRef ( ?SplDelegateCOpt:Value , 3 ))
│            ListItem (Integer ( ?SplAccountState:Int , 8 , false ))
│            ListItem (#adjustRef ( ?SplIsNativeCOpt:Value , 3 ))
│            ListItem (Integer ( ?SplDelegatedAmount:Int , 64 , false ))
│            ListItem (#adjustRef ( ?SplCloseAuthCOpt:Value , 3 ))

[Stevengre]

Same in test_process_withdraw_excess_lamports_account

│  (343 steps)
├─ 4
│     <generatedTop>
│       <kmir>
│         <k>
│           #traverseProjection ( toStack ( 4 , local ( 55 ) ) , #adjustRef ( ?SplIsNativeCOpt:Value , 3 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (Range ( ?SplMintKey:List ))
│              ))

[Stevengre]

Same in test_process_withdraw_excess_lamports_mint:

│  (1667 steps)
├─ 3
│     <generatedTop>
│       <kmir>
│         <k>
│           #traverseProjection ( toStack ( 2 , local ( 49 ) ) , #adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ) , .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem (#adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ))
│            ListItem (Integer ( ?SplMintSupply:Int , 64 , false ))
│            ListItem (Integer ( ?SplMintDecimals:Int , 8 , false ))
│            ListItem (BoolVal ( false ))
│            ListItem (#adjustRef ( ?SplMintFreezeAuthorityCOpt:Value , 1 ))
│            , 0 , ty ( 5800443 ) )  CtxField ( variantIdx ( 0 ) , ListItem (Aggregate ( variantIdx ( 0 ) , ListItem (#adjustRef ( ?SplMintAuthorityCOpt:Value , 1 ))