[FEATURE] Hard-wire conversions between [u8;8] and u64 #6
Description
- Status: Blocked with unknown issues for lowering the proof with introduced rules in P-TOKEN-HOTFIX: Conversions between [u8;8] and u64 mir-semantics#697.
- Behavior: Investigate later because this may not block
test_process_transferand it is not trivial to handle this problem.
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
Metadata
Metadata
Assignees
Labels
No labels