Exact finite-codebook runtime model

A Codebook width α assigns a complete semantic value to each BitVec width. The runtime carrier is always the exact-width bit vector; proof-indexed views are isolated in Core.Proof.

structure FloatLib.Floats.Formats.Codebook (width : ℕ) (α : Type u) : Type u

Complete denotation of every word in an exact-width lookup encoding.

• denote : BitVec width → Numerics.NumericalValue α

  Meaning of each stored word.

@[reducible]

def FloatLib.Floats.Formats.Codebook.Code {width : ℕ} {α : Type u} (_book : Codebook width α) : Type

Runtime storage type of a codebook.

The transparent definition compiles to the underlying BitVec while preserving the selected codebook in elaborated types for inspection and family-specific APIs.

@[inline]

def FloatLib.Floats.Formats.Codebook.ofNatBits {width : ℕ} {α : Type u} (book : Codebook width α) (bits : ℕ) : book.Code

Construct a codebook value from a natural-number bit pattern.

@[inline]

def FloatLib.Floats.Formats.Codebook.toNatBits {width : ℕ} {α : Type u} (book : Codebook width α) (code : book.Code) : ℕ

Extract a codebook value as a natural-number bit pattern.

def FloatLib.Floats.Formats.Codebook.numericalSystem {width : ℕ} {α : Type u} (book : Codebook width α) : Numerics.NumericalSystem

Expose a codebook through the family-independent numerical-system interface.