Finite byte encodings

The generic byte-table backend represents a format through a finite encoding bijection. A format contributes only a proved bijection between its exact model and a nonempty set of at most 256 ordinals. No IEEE, Posit, rounding, or exceptional-value policy is built into this layer.

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.uget_eq_get (array : ByteArray) (index : USize) (hindex : index.toNat < array.size) : array.uget index hindex = array[index.toNat]

ByteArray.uget and proof-indexed natural lookup select the same byte.

structure FloatLib.Floats.ExecFloat.Backend.TinyTable.Encoding (Model : Type u) : Type u

A proved finite encoding of an exact model.

radix_le_byte is the only storage-specific assumption. The inverse laws make table generation and lookup representation-preserving; no numerical property is required.

• radix : Nat

  Number of valid code words.

• radix_pos : 0 < self.radix

  The encoding is nonempty.

• radix_le_byte : self.radix ≤ 256

  Every code word fits in one byte.

• decode : Fin self.radix → Model

  Decode one valid ordinal into the exact model.

• encode : Model → Fin self.radix

  Encode one exact model as its unique ordinal.

• decode_encode (value : Model) : self.decode (self.encode value) = value

  Decoding after encoding preserves the model.

• encode_decode (code : Fin self.radix) : self.encode (self.decode code) = code

  Encoding after decoding preserves the ordinal.

@[reducible, inline]

abbrev FloatLib.Floats.ExecFloat.Backend.TinyTable.Code {Model : Type u} (encoding : Encoding Model) : Type

Direct byte carrier for one finite encoding. Its range proof is erased.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.Encoding.decodeCode {Model : Type u} (encoding : Encoding Model) (code : Code encoding) : Model

Convert a direct byte code into the exact model.

@[inline]

def FloatLib.Floats.ExecFloat.Backend.TinyTable.Encoding.encodeCode {Model : Type u} (encoding : Encoding Model) (value : Model) : Code encoding

Pack an exact model into the direct byte carrier.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.Encoding.decodeCode_encodeCode {Model : Type u} (encoding : Encoding Model) (value : Model) : encoding.decodeCode (encoding.encodeCode value) = value

Decoding a directly encoded model value recovers that value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.Encoding.encodeCode_decodeCode {Model : Type u} (encoding : Encoding Model) (code : Code encoding) : encoding.encodeCode (encoding.decodeCode code) = code

Encoding a decoded direct byte code recovers that code.