JAR: JAM Axiomatic Reference

4.1. Validator Types (§6)🔗

🔗structure
Jar.ValidatorKey : Type
Jar.ValidatorKey : Type

𝕂 : Validator key set. GP eq (56). K = 𝔹_336 decomposed as: k_b (Bandersnatch) ∥ k_e (Ed25519) ∥ k_l (BLS) ∥ k_m (metadata). Total: 32 + 32 + 144 + 128 = 336 bytes.

Constructor

Jar.ValidatorKey.mk

Fields

bandersnatch : BandersnatchPublicKey

k_b : Bandersnatch key for block sealing and VRF. 𝔹_32.

ed25519 : Ed25519PublicKey

k_e : Ed25519 key for signing guarantees, assurances, judgments. 𝔹_32.

bls : BlsPublicKey

k_l : BLS key for Beefy commitments. 𝔹_144.

metadata : OctetSeq 128

k_m : Metadata (hardware address etc). 𝔹_128.

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

𝕋 : Safrole seal-key ticket. GP eq (42). T = ⟨id ∈ ℍ, entry_index ∈ ℕ_N⟩

Constructor

Jar.Ticket.mk

Fields

id : Hash

y : VRF output (ticket identifier).

attempt : Jar.TicketEntryIndex

a : Attempt/entry index ∈ {0, 1}.

🔗inductive type
Jar.SealKeySeries [Jar.JamConfig] : Type
Jar.SealKeySeries [Jar.JamConfig] : Type

The seal-key series γ_s is either a sequence of E tickets (normal mode) or a sequence of E Bandersnatch keys (fallback mode). GP eq (39–41).

Constructors

tickets [Jar.JamConfig] :
  Array Jar.Ticket → Jar.SealKeySeries

Regular mode: E tickets determine seal keys.

fallback [Jar.JamConfig] :
  Array BandersnatchPublicKey → Jar.SealKeySeries

Fallback mode: E Bandersnatch public keys directly.

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

γ : Safrole consensus state. GP eq (34–37). γ ≡ ⟨γ_k, γ_z, γ_s, γ_a⟩

Constructor

Jar.SafroleState.mk

Fields

pendingKeys : Array Jar.ValidatorKey

γ_k : Pending validator keys for next epoch. ⟦𝕂⟧_V.

ringRoot : BandersnatchRingRoot

γ_z : Epoch ring root for ticket submissions.

sealKeys : Jar.SealKeySeries

γ_s : Seal-key series (tickets or fallback keys).

ticketAccumulator : Array Jar.Ticket

γ_a : Ticket accumulator for next epoch. ⟦𝕋⟧_{:E}.

🔗structure
Jar.Entropy : Type
Jar.Entropy : Type

η : Entropy accumulator. GP eq (68). η ≡ ⟦ℍ⟧_4 — a 4-element tuple of hashes.

Constructor

Jar.Entropy.mk

Fields

current : Hash

η_0 : Current accumulator.

previous : Hash

η_1 : Previous epoch's randomness.

twoBack : Hash

η_2 : Two epochs ago.

threeBack : Hash

η_3 : Three epochs ago.