JAR: Join-Accumulate Refine

3.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.JarConfig] : Type
Jar.CoreIndex [j : Jar.JarConfig] : Type

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

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

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

🔗def
Jar.EpochIndex [j : Jar.JarConfig] : Type
Jar.EpochIndex [j : Jar.JarConfig] : Type

Epoch slot index: ℕ_{E}. Bounded by config.E.

🔗def
Jar.TicketEntryIndex [Jar.JarConfig] : Type
Jar.TicketEntryIndex [Jar.JarConfig] :
  Type

Ticket entry index: ℕ_{N}. Raw Nat — validation enforces bounds.