JAR: JAM Axiomatic Reference

4.3. Work Types (§11)🔗

🔗inductive type
Jar.WorkError : Type
Jar.WorkError : Type

𝔼 : Work execution error. GP eq (109–111). Possible outcomes when refinement fails.

Constructors

outOfGas : Jar.WorkError
panic : Jar.WorkError
badExports : Jar.WorkError
oversize : Jar.WorkError
badCode : Jar.WorkError
bigCode : Jar.WorkError
🔗inductive type
Jar.WorkResult : Type
Jar.WorkResult : Type

Work result: either successful output blob or an error. GP eq (109).

Constructors

ok : ByteArray → Jar.WorkResult
err : Jar.WorkError → Jar.WorkResult
🔗structure
Jar.WorkDigest : Type
Jar.WorkDigest : Type

𝔻 : Work digest — the on-chain summary of a single refined work-item. GP eq (93–103). D = ⟨s, c, y, g, l, u, i, x, z, e⟩

Constructor

Jar.WorkDigest.mk

Fields

serviceId : Jar.ServiceId

s : Service index. ℕ_S.

codeHash : Hash

c : Service code hash at time of refinement. ℍ.

payloadHash : Hash

y : Payload hash. ℍ.

gasLimit : Jar.Gas

g : Gas limit for accumulation. ℕ_G.

result : Jar.WorkResult

l : Refinement result (output or error). 𝔹 ∪ 𝔼.

gasUsed : Jar.Gas

u : Actual gas used during refinement. ℕ_G.

importsCount : Nat

i : Number of imported segments. ℕ.

extrinsicsCount : Nat

x : Number of extrinsics. ℕ.

extrinsicsSize : Nat

z : Total extrinsic size in bytes. ℕ.

exportsCount : Nat

e : Number of exported segments. ℕ.

🔗structure
Jar.AvailabilitySpec : Type
Jar.AvailabilitySpec : Type

𝕐 : Availability specification for a work-package. GP eq (72–79). Y = ⟨p, l, u, e, n⟩

Constructor

Jar.AvailabilitySpec.mk

Fields

packageHash : Hash

p : Work-package hash. ℍ.

bundleLength : Jar.BlobLength

l : Auditable bundle length. ℕ_L.

erasureRoot : Hash

u : Erasure-coding root. ℍ.

segmentRoot : Hash

e : Exports segment root. ℍ.

segmentCount : Nat

n : Number of exported segments. ℕ.

🔗structure
Jar.RefinementContext : Type
Jar.RefinementContext : Type

ℂ : Refinement context. GP eq (57–66). C = ⟨a, s, b, l, t, p⟩

Constructor

Jar.RefinementContext.mk

Fields

anchorHash : Hash

a : Anchor block header hash. ℍ.

anchorStateRoot : Hash

s : Anchor state root. ℍ.

anchorBeefyRoot : Hash

b : Anchor accumulation-output log super-peak. ℍ.

lookupAnchorHash : Hash

l : Lookup-anchor header hash. ℍ.

lookupAnchorTimeslot : Jar.Timeslot

t : Lookup-anchor timeslot. ℕ_T.

prerequisites : Array Hash

p : Prerequisite work-package hashes. {ℍ} (power set).

🔗structure
Jar.WorkReport [Jar.JamConfig] : Type
Jar.WorkReport [Jar.JamConfig] : Type

ℝ : Work report. GP eq (32–45). R = ⟨s, c, x, a, o, l, d, g⟩

Constructor

Jar.WorkReport.mk

Fields

availSpec : Jar.AvailabilitySpec

s : Availability specification. 𝕐.

context : Jar.RefinementContext

c : Refinement context. ℂ.

coreIndex : Jar.CoreIndex

x : Core index. ℕ_C.

authorizerHash : Hash

a : Authorizer hash. ℍ.

authOutput : ByteArray

o : Authorization output/trace. 𝔹.

segmentRootLookup : Dict Hash Hash

l : Segment root lookup. ⟨ℍ→ℍ⟩.

digests : Array Jar.WorkDigest

d : Work digests. ⟦𝔻⟧_{1:I}.

authGasUsed : Jar.Gas

g : Authorization gas used. ℕ_G.

🔗structure
Jar.PendingReport [Jar.JamConfig] : Type
Jar.PendingReport [Jar.JamConfig] : Type

Pending report on a core: a work report with its reporting timeslot.

Constructor

Jar.PendingReport.mk

Fields

report : Jar.WorkReport

r : The work report. ℝ.

timeslot : Jar.Timeslot

t : Timeslot when reported. ℕ_T.

🔗structure
Jar.WorkItem : Type
Jar.WorkItem : Type

𝕎 : Work item. GP eq (77–87). W = ⟨s, c, y, g, a, e, i, x⟩

Constructor

Jar.WorkItem.mk

Fields

serviceId : Jar.ServiceId

s : Service index. ℕ_S.

codeHash : Hash

c : Code hash. ℍ.

payload : ByteArray

y : Payload. 𝔹.

gasLimit : Jar.Gas

g : Refinement gas limit. ℕ_G.

accGasLimit : Jar.Gas

a : Accumulation gas limit. ℕ_G.

exportsCount : Nat

e : Number of exports. ℕ.

imports : Array (Hash × Nat)

i : Import segment specifications. ⟦⟨ℍ, ℕ⟩⟧.

extrinsics : Array (Hash × Nat)

x : Extrinsic data hashes. ⟦⟨ℍ, ℕ⟩⟧.

🔗structure
Jar.WorkPackage : Type
Jar.WorkPackage : Type

ℙ : Work package. GP eq (64–74). P = ⟨j, h, u, f, c, w⟩

Constructor

Jar.WorkPackage.mk

Fields

authToken : ByteArray

j : Authorization token. 𝔹.

authCodeHost : Jar.ServiceId

h : Authorization code host service. ℕ_S.

authCodeHash : Hash

u : Authorization code hash. ℍ.

authConfig : ByteArray

f : Authorizer configuration blob. 𝔹.

context : Jar.RefinementContext

c : Refinement context. ℂ.

items : Array Jar.WorkItem

w : Work items. ⟦𝕎⟧_{1:I}.