Instructions

A Solana instruction is the unit of program invocation: a target program identified by its pubkey, a list of accounts the program may read or write, and an opaque data payload the program interprets itself.

This module matches the on-chain layout exactly so downstream specs about transaction processing, CPI semantics, and Anchor account validation can reason about real instructions:

// solana-instruction
pub struct Instruction {
    pub program_id: Pubkey,
    pub accounts:   Vec<AccountMeta>,
    pub data:       Vec<u8>,
}

pub struct AccountMeta {
    pub pubkey:      Pubkey,
    pub is_signer:   bool,
    pub is_writable: bool,
}

Main definitions

• Solanalib.AccountMeta — pubkey plus the signer/writable flags that declare how an instruction expects to use a given account.
• Solanalib.Instruction — program id, account-meta list, opaque data.

structure Solanalib.AccountMeta : Type

Metadata about how an instruction expects to use a given account.

isSigner = true means the transaction must carry a signature from this account's pubkey; isWritable = true means the program may mutate the account's lamports or data. The runtime rejects the transaction if a program tries to write an account marked read-only, or if a required signer hasn't signed.

• pubkey : Pubkey

  The account's address.

• isSigner : Bool

  True iff the transaction must carry a valid signature for pubkey.

• isWritable : Bool

  True iff the invoked program may mutate this account.

theorem Solanalib.AccountMeta.ext {x y : AccountMeta} (pubkey : x.pubkey = y.pubkey) (isSigner : x.isSigner = y.isSigner) (isWritable : x.isWritable = y.isWritable) : x = y

theorem Solanalib.AccountMeta.ext_iff {x y : AccountMeta} : x = y ↔ x.pubkey = y.pubkey ∧ x.isSigner = y.isSigner ∧ x.isWritable = y.isWritable

@[implicit_reducible]

instance Solanalib.instReprAccountMeta : Repr AccountMeta

Equations

• Solanalib.instReprAccountMeta = { reprPrec := Solanalib.instReprAccountMeta.repr }

def Solanalib.instReprAccountMeta.repr : AccountMeta → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Solanalib.instDecidableEqAccountMeta.decEq (x✝ x✝¹ : AccountMeta) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Solanalib.instDecidableEqAccountMeta : DecidableEq AccountMeta

Equations

• Solanalib.instDecidableEqAccountMeta = Solanalib.instDecidableEqAccountMeta.decEq

structure Solanalib.Instruction : Type

A Solana instruction: which program to call, which accounts to pass, and what payload to deliver. The program interprets data itself.

• programId : Pubkey

  The pubkey of the program that will execute this instruction.

• accounts : List AccountMeta

  The accounts the instruction reads or writes, with their access modes.

• data : ByteArray

  Opaque bytes delivered to the program; encoding is program-specific.

theorem Solanalib.Instruction.ext_iff {x y : Instruction} : x = y ↔ x.programId = y.programId ∧ x.accounts = y.accounts ∧ x.data = y.data

theorem Solanalib.Instruction.ext {x y : Instruction} (programId : x.programId = y.programId) (accounts : x.accounts = y.accounts) (data : x.data = y.data) : x = y

@[implicit_reducible]

instance Solanalib.instReprInstruction : Repr Instruction

Equations

• Solanalib.instReprInstruction = { reprPrec := Solanalib.instReprInstruction.repr }

def Solanalib.instReprInstruction.repr : Instruction → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Solanalib.instDecidableEqInstruction : DecidableEq Instruction

Equations

• Solanalib.instDecidableEqInstruction = Solanalib.instDecidableEqInstruction.decEq

def Solanalib.instDecidableEqInstruction.decEq (x✝ x✝¹ : Instruction) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Solanalib.Instruction.signers (ix : Instruction) : List Pubkey

The list of accounts an instruction requires to be signers.

Equations

• ix.signers = List.filterMap (fun (m : Solanalib.AccountMeta) => if m.isSigner = true then some m.pubkey else none) ix.accounts

def Solanalib.Instruction.writables (ix : Instruction) : List Pubkey

The list of accounts an instruction may mutate.

Equations

• ix.writables = List.filterMap (fun (m : Solanalib.AccountMeta) => if m.isWritable = true then some m.pubkey else none) ix.accounts