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).

JAR: JAM Axiomatic Reference

11.1. Primitive Encoders🔗