feat(rt): support round-trip transmute bytes <> u64 casts

[Stevengre]

• close P-TOKEN-HOTFIX: Conversions between [u8;8] and u64 #697

[jberthold]

Nice work! Just A few details to adjust...
We should probably add a simplification for the round-trip with symbolic values, like the one I added for amount in the p-token module.

[dkcumming]

Nice work.

[dkcumming]

I suspect this actually depends on architecture, and we do have access to that information in the configuration via the MachineInfo field Endian (link). Not sure if it is an easy inclusion but given we would then want to check it on different endian machines to ensure it works I think it's worth investigating right now. At least a note should be included as this should break on other architectures iiuc.

[jberthold]

Maybe we just add a TODO? We have a few more places where we assume little-endian byte order and machine word size 64bit.

[dkcumming]

I investigated this applied to p-token test_process_close_account, it is removing the thunk but there is no simplification so a large expression is what is left. I will make an issue to simplify this expression.

Details

#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 ( 600721 ) , ty ( 600142 ) )

=>

Integer ( ?AMOUNT:Int &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 +Int 256 *Int ?AMOUNT:Int >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 &Int 255 &Int 18446744073709551615 , 64 , false )