JAR: JAM Axiomatic Reference

2.2. Identifiers and Indices🔗

🔗def
Jar.Timeslot : Type
Jar.Timeslot : Type

ℕ_T ≡ ℕ_{2^32} : Timeslot index (32-bit unsigned). GP eq (28).

🔗def
Jar.ServiceId : Type
Jar.ServiceId : Type

ℕ_S ≡ ℕ_{2^32} : Service identifier (32-bit unsigned). GP §9.

🔗def
Jar.BlobLength : Type
Jar.BlobLength : Type

ℕ_L ≡ ℕ_{2^32} : Blob length values. GP §3.4.

🔗def
Jar.CoreIndex [j : Jar.JamConfig] : Type
Jar.CoreIndex [j : Jar.JamConfig] : Type

Core index: ℕ_{C}. Bounded by config.C.

🔗def
Jar.ValidatorIndex [j : Jar.JamConfig] : Type
Jar.ValidatorIndex [j : Jar.JamConfig] :
  Type

Validator index: ℕ_{V}. Bounded by config.V.