Remaining Thunks

[JuanCoRo]

Thunks

Known thunks in the proofs and where do they appear in proofs. See below for more explanation on the thunks.

Thunk Nº	Thunks	Problematic	Summary
1	operandConstant ( constOperand ( ... span: span ( 600186 ) , ...	?	(?) Closure type
2	#cast ( Integer ( ?STATE:Int , 8 , false ) , castKindTransmute , ...	No	u8 -> AccountState
3	#cast ( Float ( 0.20000000000000000e1 , 64 ) , castKindTransmute , ...	No	F64 -> U64
4	operandMove ( place ( ... local: local ( 4 ) , projection: .ProjectionElems ) )	?	??
5	#cast ( Reference ( 0 , place ( ... local: local ( 2 ) , ... ) ...	?	castKindPointerCoercion
6	UnableToDecode ( b"\x00" , typeInfoUnionType ( "core::mem::MaybeUninit<u8>" ...	?	??

Thunk-per-proofs table.

Checked Proofs	Present Thunks
test_ptoken_domain_data
test_process_initialize_account	1 2 3
test_process_initialize_account2	1 2 3
test_process_get_account_data_size	1
test_process_initialize_immutable_owner	1 2
test_process_sync_native	1 2
test_process_approve_checked	1 2 4 5
test_process_approve	1 2 4 5
test_process_freeze_account	1 2 4 5
test_process_initialize_account3	1 2 3 5
test_process_initialize_mint_freeze	3 5
test_process_initialize_mint2_freeze	3 5
test_process_initialize_mint_no_freeze	3 5
test_process_initialize_mint2_no_freeze	3 5
test_process_mint_to	1 2 4 5
test_process_mint_to_checked	1 2 4 5
test_process_revoke	1 2 4 5
test_process_thaw_account	1 2 4 5
test_process_withdraw_excess_lamports_account	1 2 3 4 5
test_process_withdraw_excess_lamports_mint	1 3 4 5
test_process_burn	1 2
test_process_burn_checked	1 2
test_process_close_account	1 2 5
test_process_set_authority_account	1 2 5
test_process_set_authority_mint	1 2 4
test_process_transfer_checked	1 2
test_process_transfer	1 2
test_process_amount_to_ui_amount	1 6
test_process_ui_amount_to_amount	stuck

1

Full thunk

 thunk ( operandConstant ( constOperand ( ... span: span ( 600186 ) , userTy: noUserTypeAnnotationIndex ,
    const: mirConst ( ... kind: constantKindZeroSized , ty: ty ( 600113 ) , id: mirConstId ( 375 ) ) ) ) )

Explanation:

The characteristic trait is (probably) that type 600113`` is unknown. In this case, the most likely reason is that this is a closure reference and was not extracted by stable-mir-json`

Safety

??

2

Full thunk

thunk ( #cast ( Integer ( ?STATE:Int , 8 , false ) , castKindTransmute , ty ( 600077 ) , ty ( 600110 ) ) )

Explanation:

The thunked cast is a transmute between u8 (ty ( 600077 )) and the enum AccountState (ty ( 600110 )),
which has three variants: Uninitialized, Initialized and Frozen.

Safety:

The rule that seems to make this work is the following:

  rule <k> #discriminant(
              thunk(#cast (Integer(DATA, _, false), castKindTransmute, _, TY)),
              TY
            ) => Integer(DATA, 0, false) // HACK: bit width 0 means "flexible"
          ...
        </k>
    requires #isEnumWithoutFields(lookupTy(TY))

The rule is not taking into account the width of the transmuted integer.

3

Full Thunk

thunk ( #cast ( Float ( 0.20000000000000000e1 , 64 ) , castKindTransmute , ty ( 601188 ) , ty ( 600142 ) ) )

Explanation

Transmute cast between an F64 (ty ( 601188 )) and a U64 (ty ( 600142 )).

We already have a specific rule which compares this against the expected u64 with the same bit pattern.

  rule <k> #applyBinOp (
              binOpEq,
              thunk(#cast(Float(VAL, 64), castKindTransmute, _, _)),
              Integer ( 4611686018427387904 , 64 , false ),
              false
            ) => BoolVal(true)
         ...
       </k>
    requires VAL ==Float 2.0

If we don't want to have the thunk at all, we can rewrite this #cast with this specific Float value to the expected u64.

Safety

Safe

4

Full Thunk

thunk ( operandMove ( place ( ... local: local ( 4 ) , projection: .ProjectionElems ) ) )

Where <locals> is

<locals>
    ListItem (newLocal ( ty ( 600094 ) , mutabilityMut ))

    ListItem (typedValue ( Reference ( 1 , place ( ... local: local ( 27 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 600019 ) , mutabilityNot ))

    ListItem (typedValue ( Moved , ty ( 600054 ) , mutabilityMut ))

    ListItem (typedValue ( Moved , ty ( 600165 ) , mutabilityMut ))

    ListItem (newLocal ( ty ( 600028 ) , mutabilityMut ))

    ListItem (newLocal ( ty ( 600107 ) , mutabilityNot ))

    ListItem (newLocal ( ty ( 600088 ) , mutabilityMut ))
</locals>

Explanation

Source:

function: <core::result::Result<(), pinocchio::program_error::ProgramError> as core::clone::Clone>::clone
span: ust/library/core/src/result.rs:1727

This attempts to Move an uninitialised local (newLocal at index 4). So we don't auto-create the value yet on operandMove or operandCopy, and should probably do that.

Safety

???

5

Full Thunk

thunk ( #cast ( Reference ( 0 , place ( ... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , castKindPointerCoercion ( pointerCoercionUnsize ) , ty ( 600020 ) , ty ( 600001 ) ) )

Where <locals> is

<locals>
    ListItem (newLocal ( ty ( 600002 ) , mutabilityMut ))

    ListItem (typedValue ( Aggregate ( variantIdx ( 0 ) , .List ) , ty ( 600003 ) , mutabilityNot ))

    ListItem (typedValue ( Reference ( 1 , place ( ... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 600019 ) , mutabilityNot ))

    ListItem (typedValue ( AllocRef ( allocId ( 600101 ) , .ProjectionElems , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 600019 ) , mutabilityNot ))

    ListItem (typedValue ( Aggregate ( variantIdx ( 0 ) , .List ) , ty ( 600005 ) , mutabilityNot ))

    ListItem (newLocal ( ty ( 600001 ) , mutabilityMut ))

    ListItem (typedValue ( Reference ( 0 , place ( ... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 600020 ) , mutabilityNot ))

    ListItem (newLocal ( ty ( 600001 ) , mutabilityMut ))

    ListItem (newLocal ( ty ( 600020 ) , mutabilityNot ))
</locals>

Explanation

Source:

function: core::panicking::assert_failed::<core::result::Result<(), pinocchio::program_error::ProgramError>, core::result::Result<(), pinocchio::program_error::ProgramError>>
span: /library/core/src/panicking.rs:373

Severity

???

6

Full Thunk

thunk ( UnableToDecode ( b"\x00" , typeInfoUnionType ( "core::mem::MaybeUninit<u8>" , adtDef ( 600149 ) ) ) )

Explanation

???

Severity

???