Accounts

The Solana account model. An on-chain account carries five fields: its lamport balance (u64), the program that owns it, an opaque data blob, an executable flag (true for programs, false for data accounts), and the rent epoch at which rent next comes due.

Account.lamports is a Lamports (= UInt64), so credit and debit carry explicit no-overflow / no-underflow preconditions in their type signatures. The compiler will reject any call site that hasn't proved the relevant bound — modelling the Solana convention of checked_add / checked_sub returning Err on overflow, but at the type level.

Main definitions

• Solanalib.Account — the five-field on-chain account record.
• Solanalib.Account.credit — credit lamports, requires lhs + rhs < 2^64.
• Solanalib.Account.debit — debit lamports, requires amount ≤ balance.

Main statements

Projection @[simp] lemmas for every field of every operation, so simp can chain through .field accesses uniformly. The credit_lamports_toNat and debit_lamports_toNat variants drop the result into Nat for conservation-style reasoning where omega does the heavy lifting.

structure Solanalib.Account : Type

A Solana account: lamport balance, owning program, data blob, executable flag, and rent epoch.

• lamports : Lamports

  The number of lamports held by this account (u64 on chain).

• owner : Pubkey

  The program that owns this account and is authorised to mutate it.

• data : ByteArray

  The opaque data the account holds. Interpretation is owner-specific.

• executable : Bool

  True if this account is a program (BPF binary), false for data.

• rentEpoch : Lamports

  Slot at which rent next becomes due.

theorem Solanalib.Account.ext_iff {x y : Account} : x = y ↔ x.lamports = y.lamports ∧ x.owner = y.owner ∧ x.data = y.data ∧ x.executable = y.executable ∧ x.rentEpoch = y.rentEpoch

theorem Solanalib.Account.ext {x y : Account} (lamports : x.lamports = y.lamports) (owner : x.owner = y.owner) (data : x.data = y.data) (executable : x.executable = y.executable) (rentEpoch : x.rentEpoch = y.rentEpoch) : x = y

def Solanalib.instReprAccount.repr : Account → LamportsUnchecked → Std.Format

Equations

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

@[implicit_reducible]

instance Solanalib.instReprAccount : Repr Account

Equations

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

def Solanalib.instDecidableEqAccount.decEq (x✝ x✝¹ : Account) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Solanalib.instDecidableEqAccount : DecidableEq Account

Equations

• Solanalib.instDecidableEqAccount = Solanalib.instDecidableEqAccount.decEq

def Solanalib.Account.credit (a : Account) (amount : Lamports) (_h : a.lamports.toNat + amount.toNat < UInt64.size) : Account

Credit amount lamports to an account.

Requires a proof h that the resulting balance fits in u64, so the underlying UInt64 addition can never silently wrap. This mirrors what production Solana code does with checked_add, but lifted to a compile-time obligation.

Equations

• a.credit amount _h = { lamports := a.lamports + amount, owner := a.owner, data := a.data, executable := a.executable, rentEpoch := a.rentEpoch }

def Solanalib.Account.debit (a : Account) (amount : Lamports) (_h : amount ≤ a.lamports) : Account

Debit amount lamports from an account.

Requires a proof h that the account holds at least amount lamports, so the underlying UInt64 subtraction can never underflow / wrap.

Equations

• a.debit amount _h = { lamports := a.lamports - amount, owner := a.owner, data := a.data, executable := a.executable, rentEpoch := a.rentEpoch }

Projection @[simp] lemmas. The _toNat variants drop the equation into Nat, which is what omega needs for conservation arithmetic.

@[simp]

theorem Solanalib.Account.credit_lamports (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).lamports = a.lamports + n

@[simp]

theorem Solanalib.Account.credit_owner (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).owner = a.owner

@[simp]

theorem Solanalib.Account.credit_data (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).data = a.data

@[simp]

theorem Solanalib.Account.credit_executable (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).executable = a.executable

@[simp]

theorem Solanalib.Account.credit_rentEpoch (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).rentEpoch = a.rentEpoch

@[simp]

theorem Solanalib.Account.debit_lamports (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).lamports = a.lamports - n

@[simp]

theorem Solanalib.Account.debit_owner (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).owner = a.owner

@[simp]

theorem Solanalib.Account.debit_data (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).data = a.data

@[simp]

theorem Solanalib.Account.debit_executable (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).executable = a.executable

@[simp]

theorem Solanalib.Account.debit_rentEpoch (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).rentEpoch = a.rentEpoch

Bridging to Nat. Conservation-style theorems use these to translate Lamports (UInt64) operations into UncheckedLamports (Nat) where omega can close the arithmetic.

theorem Solanalib.Account.credit_lamports_toNat (a : Account) (n : Lamports) (h : a.lamports.toNat + n.toNat < UInt64.size) : (a.credit n h).lamports.toNat = a.lamports.toNat + n.toNat

theorem Solanalib.Account.debit_lamports_toNat (a : Account) (n : Lamports) (h : n ≤ a.lamports) : (a.debit n h).lamports.toNat = a.lamports.toNat - n.toNat