Binary character input with explicit resource limits

The byte limit is checked before scanning, including before trimming ASCII whitespace. The exponent limit applies to the parsed exponent after fractional digits adjust its scale. Both checks precede exact numerical conversion. Accepted values are never clamped or approximated to satisfy a limit: their value and exception status agree with TextParser.run.

Infinity and NaN spellings have exponent magnitude zero. Their text, including every NaN payload digit, counts toward the byte limit.

Model.parse is the caller-facing entrypoint. Resource limits are opt-in with limits := some { maxBytes := 100, maxExponent := 1000 }, where an omitted field keeps its default, and status := true includes all IEEE exception flags. The TextParser namespace contains implementation helpers used by this entrypoint and its correctness proofs.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.ParseLimits : Type

Caller-selected limits on input bytes and the magnitude of the adjusted parsed exponent.

• maxBytes : ℕ

  Maximum UTF-8 byte length of the original input, including edge whitespace.

• maxExponent : ℕ

  Maximum absolute decimal or binary exponent after accounting for fractional digits.

def FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqParseLimits.decEq (x✝ x✝¹ : ParseLimits) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instDecidableEqParseLimits : DecidableEq ParseLimits

def FloatLib.Floats.Formats.BinaryInterchange.Model.instReprParseLimits.repr : ParseLimits → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instReprParseLimits : Repr ParseLimits

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.instInhabitedParseLimits : Inhabited ParseLimits

def FloatLib.Floats.Formats.BinaryInterchange.Model.TextValue.exponentMagnitude : TextValue → ℕ

Magnitude of the adjusted decimal or binary exponent. Special values have magnitude zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.readTextInput (input : String) : Except ParseError TextValue

Scan with the same ASCII trimming and syntax errors as TextParser.run, without rounding.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.run_eq_bind_readTextInput (fmt : FloatFormat) (mode : IEEERoundingMode) (input : String) : run fmt mode input = (readTextInput input).bind (convertText fmt mode)

TextParser.run is this scan followed by its numerical conversion.

def FloatLib.Floats.Formats.BinaryInterchange.Model.readTextWithLimits (limits : ParseLimits) (input : String) : Except ParseError TextValue

Check the original byte length before scanning, then check the adjusted exponent before conversion. The successful result is the scanned value itself, so conversion does not scan the input again.

def FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.runBounded (fmt : FloatFormat) (mode : IEEERoundingMode) (limits : ParseLimits) (input : String) : Except ParseError (IEEEOutcome fmt)

Implementation core with resource limits, keeping the complete IEEE status and the ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readTextWithLimits_eq_ok_iff (limits : ParseLimits) (input : String) (value : TextValue) : readTextWithLimits limits input = Except.ok value ↔ input.utf8ByteSize ≤ limits.maxBytes ∧ readTextInput input = Except.ok value ∧ value.exponentMagnitude ≤ limits.maxExponent

A successful bounded scan is exactly an original scan satisfying both resource limits.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readTextWithLimits_byte_bound {limits : ParseLimits} {input : String} {value : TextValue} (hread : readTextWithLimits limits input = Except.ok value) : input.utf8ByteSize ≤ limits.maxBytes

The byte bound holds for the original input, before any edge whitespace is removed.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readTextWithLimits_exponent_bound {limits : ParseLimits} {input : String} {value : TextValue} (hread : readTextWithLimits limits input = Except.ok value) : value.exponentMagnitude ≤ limits.maxExponent

Every successful scan respects the bound on its actual adjusted exponent.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.readTextWithLimits_eq_readTextInput (limits : ParseLimits) (input : String) (hbytes : input.utf8ByteSize ≤ limits.maxBytes) (hexponent : ∀ (value : TextValue), readTextInput input = Except.ok value → value.exponentMagnitude ≤ limits.maxExponent) : readTextWithLimits limits input = readTextInput input

When the original input meets the limits, bounded scanning preserves syntax errors as well.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.runBounded_eq_run (fmt : FloatFormat) (mode : IEEERoundingMode) (limits : ParseLimits) (input : String) (hbytes : input.utf8ByteSize ≤ limits.maxBytes) (hexponent : ∀ (value : TextValue), readTextInput input = Except.ok value → value.exponentMagnitude ≤ limits.maxExponent) : runBounded fmt mode limits input = run fmt mode input

Within the declared limits, bounded and original parsing agree on every value, flag, ternary value, and error.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.runBounded_eq_ok_iff (fmt : FloatFormat) (mode : IEEERoundingMode) (limits : ParseLimits) (input : String) (outcome : IEEEOutcome fmt) : runBounded fmt mode limits input = Except.ok outcome ↔ input.utf8ByteSize ≤ limits.maxBytes ∧ ∃ (value : TextValue), readTextInput input = Except.ok value ∧ value.exponentMagnitude ≤ limits.maxExponent ∧ convertText fmt mode value = Except.ok outcome

Successful bounded conversion comes from an original scanned value within the exponent limit. The original input satisfies the byte bound, and conversion preserves the full outcome.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.TextParser.run_eq_of_runBounded_eq_ok {fmt : FloatFormat} {mode : IEEERoundingMode} {limits : ParseLimits} {input : String} {outcome : IEEEOutcome fmt} (hparse : runBounded fmt mode limits input = Except.ok outcome) : run fmt mode input = Except.ok outcome

A bounded success is the unlimited parser's outcome, including all exception flags and the ternary value.

def FloatLib.Floats.Formats.BinaryInterchange.Model.parse (fmt : FloatFormat) (input : String) (mode : IEEERoundingMode := IEEERoundingMode.nearest) (limits : Option ParseLimits := none) (status : Bool := false) : Except ParseError (match status with | true => IEEEOutcome fmt | false => Model fmt)

Parse text with an optional rounding direction mode, resource limits, and IEEE exception status.

By default, conversion uses nearest-even rounding without resource limits and returns the value. With limits := some bounds, bounds.maxBytes bounds the original UTF-8 input before scanning and bounds.maxExponent bounds the adjusted decimal or binary exponent before numerical conversion, and some {} selects the default bounds. With status := true, the result also carries all five IEEE exception flags and the ternary value. Without it, the scanned text goes through Internal.Value.convertText, so finite numeric input runs no rounding classifier.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_eq_run (fmt : FloatFormat) (input : String) (mode : IEEERoundingMode) : parse fmt input mode = Except.map (fun (x : IEEEOutcome fmt) => x.value) (TextParser.run fmt mode input)

With limits and status disabled, parsing returns the exact core's value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_status_eq_run (fmt : FloatFormat) (input : String) (mode : IEEERoundingMode) : parse fmt input mode none true = TextParser.run fmt mode input

Status-enabled parsing without limits returns the complete exact core outcome.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_limits_eq_runBounded_map (fmt : FloatFormat) (input : String) (mode : IEEERoundingMode) (limits : ParseLimits) : parse fmt input mode (some limits) = Except.map (fun (x : IEEEOutcome fmt) => x.value) (TextParser.runBounded fmt mode limits input)

With limits enabled and status disabled, parsing returns the bounded core's value.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_limits_status_eq_runBounded (fmt : FloatFormat) (input : String) (mode : IEEERoundingMode) (limits : ParseLimits) : parse fmt input mode (some limits) true = TextParser.runBounded fmt mode limits input

With limits and status enabled, parsing returns the complete bounded core outcome.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_eq_of_parse_limits_eq_ok {fmt : FloatFormat} {input : String} {mode : IEEERoundingMode} {limits : ParseLimits} {value : Model fmt} (hparse : parse fmt input mode (some limits) = Except.ok value) : parse fmt input mode = Except.ok value

A successful bounded parse returns the value of unlimited parsing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_status_eq_of_parse_limits_status_eq_ok {fmt : FloatFormat} {input : String} {mode : IEEERoundingMode} {limits : ParseLimits} {outcome : IEEEOutcome fmt} (hparse : parse fmt input mode (some limits) true = Except.ok outcome) : parse fmt input mode none true = Except.ok outcome

A bounded parse with status preserves the unlimited parser's value, every exception flag, and the ternary value.