When running the test_process_transfer proof, I find the following values stored in locals:
ListItem (typedValue (
thunk ( #cast ( Range ( ListItem (Integer ( ARG_UINT214:Int , 8 , false ))
ListItem (Integer ( ARG_UINT215:Int , 8 , false ))
ListItem (Integer ( ARG_UINT216:Int , 8 , false ))
ListItem (Integer ( ARG_UINT217:Int , 8 , false ))
ListItem (Integer ( ARG_UINT218:Int , 8 , false ))
ListItem (Integer ( ARG_UINT219:Int , 8 , false ))
ListItem (Integer ( ARG_UINT220:Int , 8 , false ))
ListItem (Integer ( ARG_UINT221:Int , 8 , false ))
) , castKindTransmute , ty ( 600087 ) , ty ( 600086 ) ) ) ,
ty ( 600086 ),
mutabilityNot )
)
where types are
| Type |
TypeInfo |
| 600086 |
Uint(info=<UintTy.U64: 8>) |
| 600087 |
ArrayT(element_type=600036, length=8) |
| 600036 |
Uint(info=<UintTy.U8: 1>) |
This is a u64 converted from an input array. Maybe we can variable-abstract this somehow?
A bit later we also have a local
ListItem (typedValue (
thunk ( #cast ( Range ( ListItem (Integer ( ?AMOUNT:Int &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
ListItem (Integer ( ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 , 8 , false ))
) , castKindTransmute , ty ( 600087 ) , ty ( 600086 ) ) ) ,
ty ( 600086 ) ,
mutabilityNot )
)
This is a u64 AMOUNT from an interface account (introduced by the cheatcode_is_account, and then converted to a [u8;8] and back. The back-conversion became thunked but it should just be AMOUNT again (with the right side conditions). This can just be a simplification rule
test_process_transferand it is not trivial to handle this problem.When running the
test_process_transferproof, I find the following values stored in locals:where types are
This is a
u64converted from an input array. Maybe we can variable-abstract this somehow?A bit later we also have a local
This is a
u64AMOUNTfrom an interface account (introduced by thecheatcode_is_account, and then converted to a[u8;8]and back. The back-conversion became thunked but it should just beAMOUNTagain (with the right side conditions). This can just be a simplification rule