Runtime conversion source for configured codebooks

A configured codebook carries a complete finite-or-exceptional denotation table, so it can be an exact source for explicit conversion. As a destination, the only quantizer supplied is nearest?: it scans the table and returns the first finite codeword minimizing |x - c|, with ties resolved to the lower word (see Formats.Codebook.nearestCode). It is not installed as a generic conversion instance because reserved-word handling and alternative tie rules are properties of a particular codebook application.

@[instance_reducible]

instance FloatLib.Floats.ExecFloat.Codebook.Conversion.exactDecoder {width : ℕ} {α : Type u} {book : Formats.Codebook width α} : ExactDecoder (Codebook book) α

A configured codebook decodes through its complete selected lookup table.

def FloatLib.Floats.ExecFloat.Codebook.Conversion.nearest? {width : ℕ} {α : Type u} {book : Formats.Codebook width α} [AddGroup α] [LinearOrder α] (x : α) : Option (Codebook book)

The nearest configured codeword to x, or none when the table has no finite word.

Ties resolve to the lower word. Formats.Codebook.nearestCode_spec proves that the selected word is finite and minimizes |x - c| over every finite codeword c.

theorem FloatLib.Floats.ExecFloat.Codebook.Conversion.decode_nearest? {width : ℕ} {α : Type u} {book : Formats.Codebook width α} [AddGroup α] [LinearOrder α] (x : α) (value : Codebook book) (hnearest : nearest? x = some value) : ∃ (decoded : α), value.decode = Numerics.NumericalValue.finite decoded ∧ ∀ (other : BitVec width) (otherValue : α), book.denote other = Numerics.NumericalValue.finite otherValue → |x - decoded| ≤ |x - otherValue|

Decoding the nearest configured codeword gives the closest finite table value.