JAR: Join-Accumulate Refine

6.7. Protocol Configuration🔗

🔗structure
Jar.Params : Type
Jar.Params : Type

Protocol configuration: parameters that differ across variants. Verified against grey/crates/grey-types/src/config.rs.

Constructor

Jar.Params.mk

Fields

V : Nat

V : Total number of validators.

C : Nat

C : Total number of cores.

E : Nat

E : Epoch length in timeslots.

N_TICKETS : Nat

N : Ticket entries per validator.

Y_TAIL : Nat

Y : Ticket submission end slot.

K_MAX_TICKETS : Nat

K : Max tickets per extrinsic.

R_ROTATION : Nat

R : Validator-core rotation period in timeslots.

H_RECENT : Nat

H : Recent history size in blocks.

G_A : Nat

G_A : Gas allocated per work-report accumulation.

G_I : Nat

G_I : Gas allocated for Is-Authorized.

G_R : Nat

G_R : Gas allocated for Refine.

G_T : Nat

G_T : Total accumulation gas per block.

O_POOL : Nat

O : Authorization pool size per core.

Q_QUEUE : Nat

Q : Authorization queue size per core.

I_MAX_ITEMS : Nat

I : Max work items per package.

J_MAX_DEPS : Nat

J : Max dependency items in a work-report.

T_MAX_EXTRINSICS : Nat

T : Max extrinsics per work-package.

U_TIMEOUT : Nat

U : Availability timeout in timeslots.

D_EXPUNGE : Nat

D : Preimage expunge period in timeslots.

L_MAX_ANCHOR : Nat

L : Max lookup anchor age in timeslots.

B_I : Nat

B_I : Additional minimum balance per mapping item.

B_L : Nat

B_L : Additional minimum balance per data octet.

B_S : Nat

B_S : Base minimum balance for a service.

W_P : Nat

W_P : Erasure pieces per segment.

🔗structure
Jar.Params.Valid (cfg : Jar.Params) : Prop
Jar.Params.Valid (cfg : Jar.Params) : Prop

Positivity proofs required for Fin types to be inhabited.

Constructor

Jar.Params.Valid.mk

Fields

hV : 0 < cfg.V
hC : 0 < cfg.C
hE : 0 < cfg.E
hN : 0 < cfg.N_TICKETS
🔗def
Jar.Params.isValidValCount (cfg : Jar.Params) (z : Nat) : Bool
Jar.Params.isValidValCount
  (cfg : Jar.Params) (z : Nat) : Bool

Valid validator count: multiples of 3 in [6, 3*(C+1)]. GP#514 §safrole. V = {3c | c ∈ ℕ, 2 ≤ c ≤ C+1} = {6, 9, 12, ..., 3*(C+1)}.

🔗inductive type
Jar.MemoryModel : Type
Jar.MemoryModel : Type

PVM memory model. Controls program initialization layout.

Constructors

segmented : Jar.MemoryModel

GP v0.7.2: 4 disjoint regions with per-page RO/RW/inaccessible permissions.

linear : Jar.MemoryModel

Contiguous linear: single RW region at address 0, no guard zone.

🔗inductive type
Jar.GasModel : Type
Jar.GasModel : Type

PVM gas metering model.

Constructors

perInstruction : Jar.GasModel

GP v0.7.2: 1 gas per instruction.

basicBlockFull : Jar.GasModel

Per-basic-block cost via full pipeline simulation (ROB + EU contention).

basicBlockSinglePass : Jar.GasModel

Per-basic-block cost via single-pass O(n) model (register-done tracking).

🔗inductive type
Jar.CapabilityModel : Type
Jar.CapabilityModel : Type

PVM capability model.

Constructors

none : Jar.CapabilityModel

No capability model (v0.7.2 / jar1 v1).

v2 : Jar.CapabilityModel

Capability-based execution (JAVM v2).

🔗type class
Jar.EconModel (econ xfer : Type) : Type
Jar.EconModel (econ xfer : Type) : Type

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.

🔗type class
Jar.JarConfig : Type 1
Jar.JarConfig : Type 1

JarConfig: provides protocol configuration and validity proofs. Used by struct types and Fin-based index aliases. Extended by JarVariant (in Jar/Variant.lean) to add JAVM function fields.

Instance Constructor

Jar.JarConfig.mk

Methods

name : String

Variant name, e.g. "gp072_tiny", "gp072_full".

config : Jar.Params
valid : Jar.JarConfig.config.Valid
memoryModel : Jar.MemoryModel

PVM memory layout for program initialization.

gasModel : Jar.GasModel

PVM gas metering strategy.

capabilityModel : Jar.CapabilityModel

PVM capability model: .none = flat memory, .v2 = capability-based.

useCompactDeblob : Bool

PVM blob deblob encoding: true = JAM compact natural, false = u32 LE (jar1).

variableValidators : Bool

Whether validator set size is variable (GP#514). When true, designate hostcall accepts a length argument and active core count scales with validator count. Default false for gp072 variants.

EconType : Type

Economic model type for service accounts (BalanceEcon or QuotaEcon).

TransferType : Type

Transfer payload type (BalanceTransfer or QuotaTransfer).

econBEq : BEq Jar.JarConfig.EconType

BEq instance for economic model (required for state comparison).

econInhabited : Inhabited Jar.JarConfig.EconType

Inhabited instance for economic model (required for default construction).

xferBEq : BEq Jar.JarConfig.TransferType

BEq instance for transfer payload.

xferInhabited : Inhabited Jar.JarConfig.TransferType

Inhabited instance for transfer payload.

econRepr : Repr Jar.JarConfig.EconType

Repr instance for economic model (for debugging).

xferRepr : Repr Jar.JarConfig.TransferType

Repr instance for transfer payload (for debugging).

econModel : Jar.EconModel Jar.JarConfig.EconType Jar.JarConfig.TransferType

EconModel instance linking EconType and TransferType.

🔗def
Jar.Params.full : Jar.Params
Jar.Params.full : Jar.Params

Full specification constants (Gray Paper v0.7.2).

🔗def
Jar.Params.tiny : Jar.Params
Jar.Params.tiny : Jar.Params

Tiny test configuration. Verified against grey/crates/grey-types/src/config.rs Config::tiny() (Rust side).

🔗def
Jar.cfg [j : Jar.JarConfig] : Jar.Params
Jar.cfg [j : Jar.JarConfig] : Jar.Params

Access config field via JarConfig typeclass.