Representation theorems for configured codebooks

Wrapping and unwrapping preserve the complete exact-width word. Natural-number construction reduces modulo 2 ^ width.

@[simp]

theorem FloatLib.Floats.ExecFloat.Codebook.toCode_ofCode {width : ℕ} {α : Type u} {book : Formats.Codebook width α} (code : book.Code) : (ofCode code).toCode = code

Unwrapping a freshly wrapped codebook word returns the original word.

@[simp]

theorem FloatLib.Floats.ExecFloat.Codebook.ofCode_toCode {width : ℕ} {α : Type u} {book : Formats.Codebook width α} (value : Codebook book) : ofCode value.toCode = value

Rewrapping the word of a codebook value returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.Codebook.toNatBits_ofNatBits {width : ℕ} {α : Type u} {book : Formats.Codebook width α} (bits : ℕ) : (ofNatBits bits).toNatBits = bits % 2 ^ width

Encoding then reading a natural bit pattern reduces it modulo 2 ^ width.