Proof contract for configured codebook decoding

The installed ExactDecoder returns the selected codebook's table entry, including exceptional entries.

@[simp]

theorem FloatLib.Floats.ExecFloat.Codebook.Conversion.exactDecoder_run {width : ℕ} {α : Type u} {book : Formats.Codebook width α} (value : Codebook book) : ExactDecoder.run value = value.decode

The installed source capability returns the codebook's public decoding result.