Primitive Encoders

def

Jar.Codec.encodeFixedNat : Nat → Nat → ByteArray
Jar.Codec.encodeFixedNat :
  Nat → Nat → ByteArray

𝓔_l : Fixed-width LE encoding. GP eq (C.12). Encodes natural x into exactly l bytes, little-endian.

def

Jar.Codec.decodeFixedNat (bs : ByteArray) : Nat
Jar.Codec.decodeFixedNat
  (bs : ByteArray) : Nat

Decode fixed-width LE bytes back to a natural number.

def

Jar.Codec.encodeNat (x : Nat) : ByteArray
Jar.Codec.encodeNat (x : Nat) : ByteArray

𝓔 : Variable-length natural encoding. GP eq (C.1). Encodes naturals up to 2^64 into 1–9 bytes.

def

Jar.Codec.encodeOption.{u_1} {α : Type u_1} (f : α → ByteArray) :
  Option α → ByteArray
Jar.Codec.encodeOption.{u_1}
  {α : Type u_1} (f : α → ByteArray) :
  Option α → ByteArray

¿x : Optional discriminator encoding. GP eq (C.6). None → [0], Some x → [1] ++ 𝓔(x).

def

Jar.Codec.encodeLengthPrefixed (data : ByteArray) : ByteArray
Jar.Codec.encodeLengthPrefixed
  (data : ByteArray) : ByteArray

↕x : Length-prefixed encoding. GP eq (C.4). Prepends the byte-length of the encoded data as a variable-length natural.

def

Jar.Codec.encodeBits (bs : Array Bool) : ByteArray
Jar.Codec.encodeBits (bs : Array Bool) :
  ByteArray

Pack a boolean array into bytes, LSB-first within each byte. GP eq (C.9).

def

Jar.Codec.concatBytes (parts : Array ByteArray) : ByteArray
Jar.Codec.concatBytes
  (parts : Array ByteArray) : ByteArray

Concatenate an array of ByteArrays.

def

Jar.Codec.encodeArray.{u_1} {α : Type u_1} (f : α → ByteArray)
  (xs : Array α) : ByteArray
Jar.Codec.encodeArray.{u_1} {α : Type u_1}
  (f : α → ByteArray) (xs : Array α) :
  ByteArray

Encode an array of items and concatenate (for fixed-size element encoding).

def

Jar.Codec.encodeLengthPrefixedArray.{u_1} {α : Type u_1}
  (f : α → ByteArray) (xs : Array α) : ByteArray
Jar.Codec.encodeLengthPrefixedArray.{u_1}
  {α : Type u_1} (f : α → ByteArray)
  (xs : Array α) : ByteArray

Encode an array with byte-length prefix (for backward compat).

def

Jar.Codec.encodeCountPrefixedArray.{u_1} {α : Type u_1}
  (f : α → ByteArray) (xs : Array α) : ByteArray
Jar.Codec.encodeCountPrefixedArray.{u_1}
  {α : Type u_1} (f : α → ByteArray)
  (xs : Array α) : ByteArray

Encode a sequence with count prefix. GP eq (C.4): 𝓔([x₁, ..., xₙ]) ≡ 𝓔(n) ⌢ 𝓔(x₁) ⌢ ... ⌢ 𝓔(xₙ).

JAR: Join-Accumulate Refine

16.1. Primitive Encoders🔗