Pubkey

A Solana public key — a 32-byte identifier used as the address of every account on the cluster. Real on-chain pubkeys are interpreted in two ways depending on context: as compressed Ed25519 curve points (regular wallet/program addresses) or as off-curve hashes (Program Derived Addresses). This module captures the raw byte-array shape; the curve / PDA distinction is layered on in Solanalib.Pda.

Main definitions

• Solanalib.Pubkey — the 32-byte identifier wrapper.

Implementation notes

The 32-byte length constraint is not yet enforced in the type. A later refinement will replace ByteArray with a length-indexed Vector UInt8 32 once we have a use site that actually needs the bound. For algebraic theorems about pubkey equality, the current shape is sufficient.

@[implicit_reducible]

instance instReprByteArray_solanalib : Repr ByteArray

Equations

• instReprByteArray_solanalib = { reprPrec := instReprByteArray_solanalib.repr }

def instReprByteArray_solanalib.repr : ByteArray → Nat → Std.Format

Equations

• instReprByteArray_solanalib.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "data" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.data)).group) " }"

structure Solanalib.Pubkey : Type

A Solana public key: a 32-byte identifier serving as an account address.

Intentionally not tagged @[ext]. Tagging it would cause the ext tactic on enclosing types (e.g. Account) to descend through the owner field into byte-array internals, generating goals about ByteArray.data.size that we don't want to discharge. If a future theorem genuinely needs byte-level pubkey extensionality, use Pubkey.mk.injEq directly.

• bytes : ByteArray

  The raw bytes of the pubkey. Conceptually length 32.

@[implicit_reducible]

instance Solanalib.instReprPubkey : Repr Pubkey

Equations

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

def Solanalib.instReprPubkey.repr : Pubkey → Nat → Std.Format

Equations

• Solanalib.instReprPubkey.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "bytes" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.bytes)).group) " }"

def Solanalib.instDecidableEqPubkey.decEq (x✝ x✝¹ : Pubkey) : Decidable (x✝ = x✝¹)

Equations

• Solanalib.instDecidableEqPubkey.decEq { bytes := a } { bytes := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Solanalib.instDecidableEqPubkey : DecidableEq Pubkey

Equations

• Solanalib.instDecidableEqPubkey = Solanalib.instDecidableEqPubkey.decEq