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 : Status) : environment.restoreFlags (Numerics.IEEEStatus.saveAllFlags saved) Numerics.IEEEStatus.allFlags = { rounding := environment.rounding, flags := saved }

Restoring all saved flags preserves the current 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 : Exception) : Numerics.IEEEStatus.isSet (environment.run operation).2.flags exception = (Numerics.IEEEStatus.isSet environment.flags exception || Numerics.IEEEStatus.isSet (operation environment.rounding).status 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 = Numerics.IEEEStatus.union environment.flags (Numerics.IEEEStatus.union first.status 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.