p-token: Add clarifications from formal verification report (#155)

* Comment for I-02

* Comment for I-04

* Comment for I-06 and I-07

* Comment for I-08

* Comment for I-09

* Comment for I-10

* Comment for I-11

* Comment for I-12

* Fix formatting

* Add syscall keyword

Author: febo

pinocchio/interface/src/instruction.rs

@@ -53,7 +53,18 @@ pub enum TokenInstruction {
     /// Multisignature accounts can used in place of any single owner/delegate
     /// accounts in any token instruction that require an owner/delegate to be
     /// present.  The variant field represents the number of signers (M)
-    /// required to validate this multisignature account.
+    /// required to validate this multisignature account. This number must be
+    /// less than or equal to the number of signers provided in the accounts
+    /// list, otherwise the multisignature account will be unusable.
+    ///
+    /// Note that M is not validated to be less than or equal to the number of
+    /// signers provided in the accounts list, so it is the caller's
+    /// responsibility to ensure a valid M value is provided.
+    ///
+    /// Duplicate signer accounts are not rejected. The caller must ensure each
+    /// signer is unique and appears only once in the accounts list, otherwise
+    /// a repeated signer can count more than once and effectively lower the
+    /// configured M threshold.
     ///
     /// The [`TokenInstruction::InitializeMultisig`] instruction requires no
     /// signers and MUST be included within the same Transaction as the
@@ -79,6 +90,9 @@ pub enum TokenInstruction {
     /// amounts of SOL and Tokens will be transferred to the destination
     /// account.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate
@@ -100,6 +114,9 @@ pub enum TokenInstruction {
     /// Approves a delegate.  A delegate is given the authority over tokens on
     /// behalf of the source account's owner.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -120,6 +137,11 @@ pub enum TokenInstruction {
 
     /// Revokes the delegate's authority.
     ///
+    /// Note that a delegate can revoke its own delegation.
+    ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -137,6 +159,9 @@ pub enum TokenInstruction {
     /// Note that when setting a new account owner authority on a native
     /// token account, the current close authority (if any) will be removed.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single authority
@@ -157,6 +182,9 @@ pub enum TokenInstruction {
     /// Mints new tokens to an account.  The native mint does not support
     /// minting.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single authority
@@ -178,6 +206,9 @@ pub enum TokenInstruction {
     /// Burns tokens by removing them from an account.  `Burn` does not support
     /// accounts associated with the native mint, use `CloseAccount` instead.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate
@@ -199,6 +230,9 @@ pub enum TokenInstruction {
     /// Close an account by transferring all its SOL to the destination account.
     /// Non-native accounts may only be closed if its token amount is zero.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -216,6 +250,9 @@ pub enum TokenInstruction {
     /// Freeze an Initialized account using the Mint's `freeze_authority` (if
     /// set).
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -232,6 +269,9 @@ pub enum TokenInstruction {
 
     /// Thaw a Frozen account using the Mint's `freeze_authority` (if set).
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -255,6 +295,9 @@ pub enum TokenInstruction {
     /// decimals value is checked by the caller.  This may be useful when
     /// creating transactions offline or within a hardware wallet.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate
@@ -284,6 +327,9 @@ pub enum TokenInstruction {
     /// decimals value is checked by the caller.  This may be useful when
     /// creating transactions offline or within a hardware wallet.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner
@@ -313,6 +359,9 @@ pub enum TokenInstruction {
     /// decimals value is checked by the caller.  This may be useful when
     /// creating transactions offline or within a hardware wallet.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single authority
@@ -341,6 +390,9 @@ pub enum TokenInstruction {
     /// by the caller. This may be useful when creating transactions offline or
     /// within a hardware wallet.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate
@@ -384,6 +436,11 @@ pub enum TokenInstruction {
     /// `system_instruction::transfer` to move lamports to a wrapped token
     /// account, and needs to have its token `amount` field updated.
     ///
+    /// The rent-exempt reserve is recomputed by the instruction using the Rent
+    /// sysvar, retrieved either through the syscall or passed as an extra
+    /// account. As a result, the token `amount` field value can increase or
+    /// decrease according to the rent-exempt reserve requirement.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Using runtime Rent sysvar
@@ -455,7 +512,9 @@ pub enum TokenInstruction {
     /// before [`TokenInstruction::InitializeAccount`].
     ///
     /// No-ops in this version of the program, but is included for compatibility
-    /// with the Associated Token Account program.
+    /// with the Associated Token Account program. Note that when the
+    /// instruction is executed as part of a [`TokenInstruction::Batch`],
+    /// the account must be owned by the Token program.
     ///
     /// Accounts expected by this instruction:
     ///
@@ -487,6 +546,9 @@ pub enum TokenInstruction {
     /// Return data can be fetched using `sol_get_return_data` and deserializing
     /// the return data as a little-endian `u64`.
     ///
+    /// Note that the length of `ui_amount` is limited to `257` digits
+    /// (characters), including digits after the decimal point.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   0. `[]` The mint to calculate for.
@@ -500,6 +562,9 @@ pub enum TokenInstruction {
     /// owned account by sending them to any other account, leaving behind only
     /// lamports for rent exemption.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate
@@ -518,6 +583,9 @@ pub enum TokenInstruction {
     ///
     /// This is useful to unwrap lamports from a wrapped SOL account.
     ///
+    /// This instruction accepts multisignature accounts owned by either
+    /// the Token or Token-2022 programs.
+    ///
     /// Accounts expected by this instruction:
     ///
     ///   * Single owner/delegate

pinocchio/interface/src/state/account.rs

@@ -15,6 +15,11 @@ pub const INCINERATOR_ID: Pubkey =
 const SYSTEM_PROGRAM_ID: Pubkey = pinocchio_pubkey::pubkey!("11111111111111111111111111111111");
 
 /// Internal representation of a token account data.
+///
+/// Note that when loading an `Account` from bytes, this implementation does not
+/// check the validity of `COption` fields, since the trailing 3 bytes are
+/// ignored. As a result, it is possible to load an `Account` with invalid
+/// `COption` values.
 #[repr(C)]
 pub struct Account {
     /// The mint associated with this account

pinocchio/interface/src/state/mint.rs

@@ -4,6 +4,11 @@ use {
 };
 
 /// Internal representation of a mint data.
+///
+/// Note that when loading a `Mint` from bytes, this implementation does not
+/// check the validity of `COption` fields, since the trailing 3 bytes are
+/// ignored. As a result, it is possible to load a `Mint` with invalid `COption`
+/// values.
 #[repr(C)]
 pub struct Mint {
     /// Optional authority used to mint new tokens. The mint authority may only

pinocchio/interface/src/state/mod.rs

@@ -9,6 +9,15 @@ pub mod mint;
 pub mod multisig;
 
 /// Type alias for fields represented as `COption`.
+///
+/// Note that only the first byte of the 4-byte array is used to
+/// represent the `Option` discriminant, while the remaining 3 bytes
+/// are padding to ensure alignment. The program does not modify
+/// these padding bytes and leaves them as `0`.
+///
+/// Reading a `COption` value with nonzero trailing padding bytes
+/// does not result in an error, since they are ignored in this
+/// implementation.
 pub type COption<T> = ([u8; 4], T);
 
 /// Marker trait for types that can be cast from a raw pointer.

scripts/solana.dic

@@ -50,3 +50,4 @@ APY
 codama
 autogenerated
 sdk
+syscall