Abstraction over the economic model for service accounts. Pure logic — no encoding/serialization methods (those are in EconEncode). Instances are provided for BalanceEcon and QuotaEcon in Accounts.lean.
Instance Constructor
Jar.EconModel.mk
Methods
canAffordStorage : econ → Nat → Nat → Nat → Nat → Nat → Bool
Check if a service can afford the given storage footprint. bI, bL, bS are the storage deposit constants (from Params).
debitForNewService : econ → Nat → Nat → UInt64 → Nat → Nat → Nat → Nat → Nat → Option econ
Debit the creator's econ for new service creation.
newGratis is the new account's gratis value (from register).
callerItems/callerBytes are the caller's current storage footprint.
Returns none if insufficient funds/quota.
newServiceEcon : Nat → Nat → UInt64 → Nat → Nat → Nat → econ
Create initial econ state for a newly created service.
creditTransfer : econ → xfer → econ
Credit an incoming transfer's economic payload.
debitTransfer : econ → UInt64 → Option econ
Check transfer affordability and return debited econ. Returns none if insufficient balance (BalanceEcon only).
absorbEjected : econ → econ → econ
Absorb an ejected service's economic value.
setQuota : econ → UInt64 → UInt64 → Option econ
Set storage quota (jar1 only). Returns none if not supported by this economic model.
makeTransferPayload : UInt64 → xfer
Create transfer payload from the amount register value.
encodeTransferAmount : xfer → ByteArray
Encode transfer payload as 8 bytes (for PVM on-transfer arguments).
encodeInfo : econ → Nat → Nat → Nat → Nat → Nat → ByteArray
Encode econ fields for the info host call (5). Must produce exactly 24 bytes. bI, bL, bS are the storage deposit constants.
serializeEcon : econ → ByteArray
Serialize econ fields for state Merklization. Must produce exactly 16 bytes.
deserializeEcon : ByteArray → Nat → Option (econ × Nat)
Deserialize econ fields. Returns (econ, bytes consumed) or none.
econToJson : econ → List (String × Lean.Json)
Convert econ fields to JSON key-value pairs for ServiceAccount serialization.
econFromJson? : Lean.Json → Except String econ
Parse econ fields from JSON.
xferToJson : xfer → List (String × Lean.Json)
Convert transfer payload to JSON key-value pairs.
xferFromJson? : Lean.Json → Except String xfer
Parse transfer payload from JSON.