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, remains subject to the byte limit.

Model.parse is the caller-facing entrypoint. Resource limits are opt-in with limits := true; 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 no exponent.

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)

The existing parser is exactly this scan followed by its original 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 explicit resource limits, retaining the complete IEEE status.

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, 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 exactly the original parser's outcome, including all exception flags.

def FloatLib.Floats.Formats.BinaryInterchange.Model.parse (fmt : FloatFormat) (input : String) (rounding : IEEERoundingMode := IEEERoundingMode.nearestEven) (limits : Bool := false) (maxBytes : ℕ := 4096) (maxExponent : ℕ := 10000) (status : Bool := false) : Except ParseError (match status with | true => IEEEOutcome fmt | false => Model fmt)

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

By default, conversion uses nearest-even rounding without resource limits and returns the value. With limits := true, maxBytes bounds the original UTF-8 input before scanning and maxExponent bounds the adjusted decimal or binary exponent before numerical conversion. With status := true, the result also carries all five IEEE exception flags.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_eq_run (fmt : FloatFormat) (input : String) (rounding : IEEERoundingMode) : parse fmt input rounding = Except.map (fun (x : IEEEOutcome fmt) => x.value) (TextParser.run fmt rounding 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) (rounding : IEEERoundingMode) (maxBytes maxExponent : ℕ) : parse fmt input rounding false maxBytes maxExponent true = TextParser.run fmt rounding 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) (rounding : IEEERoundingMode) (maxBytes maxExponent : ℕ) : parse fmt input rounding true maxBytes maxExponent = Except.map (fun (x : IEEEOutcome fmt) => x.value) (TextParser.runBounded fmt rounding { maxBytes := maxBytes, maxExponent := maxExponent } 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) (rounding : IEEERoundingMode) (maxBytes maxExponent : ℕ) : parse fmt input rounding true maxBytes maxExponent true = TextParser.runBounded fmt rounding { maxBytes := maxBytes, maxExponent := maxExponent } 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} {rounding : IEEERoundingMode} {maxBytes maxExponent : ℕ} {value : Model fmt} (hparse : parse fmt input rounding true maxBytes maxExponent = Except.ok value) : parse fmt input rounding = Except.ok value

A successful bounded parse returns exactly the value produced by unlimited parsing.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.parse_status_eq_of_parse_limits_status_eq_ok {fmt : FloatFormat} {input : String} {rounding : IEEERoundingMode} {maxBytes maxExponent : ℕ} {outcome : IEEEOutcome fmt} (hparse : parse fmt input rounding true maxBytes maxExponent true = Except.ok outcome) : parse fmt input rounding false 4096 10000 true = Except.ok outcome

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