Non-Overflow and other assumed invariants in `process_transfer` code

[jberthold]

This is a note about assumptions that process_transfer makes about its input code, which should eventually be reported to the authors and Solana stakeholders.

• Assumed Non-Overflow based on token supply

  The proof for the process_transfer properties exhibits arithmetic overflows caused by the following code:
  

  solana-token/p-token/src/processor/shared/transfer.rs

  Lines 167 to 169 in d19ea27

  	// Note: The amount of a token account is always within the range of the
  	// mint supply (`u64`).
  	destination_account.set_amount(destination_account.amount() + amount);

  
  As the comment above the code states, it is assumed that a token's maximum amount is bound by a u64 field in the mint for the token.
  Therefore, if (and only if) the sum of all amount fields in all accounts for a particular token is (at most) this maximum amount, the transfer performed here can safely assume that the addition does not overflow:
  • The source account must have sufficient funds ( amount <= src.amount())
  • The total supply limits the amounts as src.amount() + dest.amount() <= mint.supply for the respective mint.
  • It is checked beforehand that both accounts relate to the same mint.
    Therefore the sum is not overflowing.

  There is obviously no easy way to guarantee the invariant that \sum_{a \in accounts(mint)} a.amount() <= mint.supply except by tightly controlling the accounts created for the mint.

• Assumption that the _.is_native() field is consistent for all native accounts (i.e., relating to a mint which operates the native currency).

• Assumption that account_info.lamports is the same as account.amount() for an account when account.is_native()
  The code in
  

  solana-token/p-token/src/processor/shared/transfer.rs

  Lines 171 to 187 in d19ea27

  	if source_account.is_native() {
  	// SAFETY: single mutable borrow to `source_account_info` lamports.
  	let source_lamports = unsafe { source_account_info.borrow_mut_lamports_unchecked() };
  	*source_lamports = source_lamports
  	.checked_sub(amount)
  	.ok_or(TokenError::Overflow)?;
  	// SAFETY: single mutable borrow to `destination_account_info` lamports; the
  	// account is already validated to be different from
  	// `source_account_info`.
  	let destination_lamports =
  	unsafe { destination_account_info.borrow_mut_lamports_unchecked() };
  	*destination_lamports = destination_lamports
  	.checked_add(amount)
  	.ok_or(TokenError::Overflow)?;
  	}
  	}

  
  shows that the amount and the lamports fields are maintained in parallel (duplicating the amount) on transfers for all native accounts.

[jberthold]

Related: proofs...runtimeverification:solana-token:jb/process-transfer-debug avoids the custom overflow check

[jberthold]

About the lamports and account balance (amount) field correspondance, information from Febo is:

• lamports and amount are not the same, because of the rent (and rent exemption). The amount is initially the lamports minus the rent
• anyone can send lamports to the p-token account so the lamports may increase wrt. the amount
• as far as transfers within the p-token code are concerned, lamports and amount move together
• As a result, there is an invariant that the lamports will always be at least the amount