Sticky flags and scoped rounding laws

Flags raised by an operation remain set after later operations. Clearing and restoring affect exactly the requested group. Scoped rounding restores the caller's direction while preserving the flags produced by the inner computation.

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.restoreFlags_allFlags (environment : Environment) (saved : Numerics.IEEEStatus) : environment.restoreFlags saved.saveAllFlags Numerics.IEEEStatus.allFlags = { rounding := environment.rounding, flags := saved }

Restoring every flag from a snapshot replaces the flags and keeps the rounding direction.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.accept_value (environment : Environment) (outcome : Outcome) : (environment.accept outcome).1 = outcome.value

Exception accumulation never changes the operation's delivered datum.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.run_rounding (environment : Environment) (operation : RoundingMode → Outcome) : (environment.run operation).2.rounding = environment.rounding

An operation preserves the ambient rounding direction.

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.run_isSet (environment : Environment) (operation : RoundingMode → Outcome) (exception : Numerics.IEEEException) : (environment.run operation).2.flags.isSet exception = (environment.flags.isSet exception || (operation environment.rounding).status.isSet exception)

A flag after execution is the disjunction of its previous and newly raised states.

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.accept_accept_flags (environment : Environment) (first second : Outcome) : ((environment.accept first).2.accept second).2.flags = environment.flags.union (first.status.union second.status)

Two operations accumulate the union of both outcomes and the initial flags.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.withRounding_rounding {α : Type u_1} (environment : Environment) (rounding : RoundingMode) (computation : Environment → α × Environment) : (environment.withRounding rounding computation).2.rounding = environment.rounding

Scoped rounding restores the caller's direction, regardless of the inner computation.

theorem FloatLib.Floats.Formats.DecimalInterchange.Environment.withRounding_flags {α : Type u_1} (environment : Environment) (rounding : RoundingMode) (computation : Environment → α × Environment) : (environment.withRounding rounding computation).2.flags = (computation { rounding := rounding, flags := environment.flags }).2.flags

Scoped rounding preserves the inner computation's resulting exception flags.