Exact semantics of configured powers and fused minus-one exponentials

The configured operations refine the model kernels for every lawful storage codec. Their real semantics hold under the same domain conditions, independently of storage width. These are correctness results for exact boundary comparison, not bounds on execution cost.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_pow {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (pow base exponent) = (toModel base).pow (toModel exponent)

Configured power decodes to the model pow of the decoded operands.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp2 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp2 value) = (toModel value).exp2

Configured base-two exponential decodes to the model exp2.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp10 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp10 value) = (toModel value).exp10

Configured base-ten exponential decodes to the model exp10.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp2Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp2Minus1 value) = (toModel value).exp2Minus1

Configured base-two exponential minus one decodes to the fused model exp2Minus1.

@[simp]

theorem FloatLib.Floats.ExecFloat.Posit.toModel_exp10Minus1 {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) : toModel (exp10Minus1 value) = (toModel value).exp10Minus1

Configured base-ten exponential minus one decodes to the fused model exp10Minus1.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : 0 ≤ b) (hdomain : b ≠ 0 ∨ 0 < e) : toModel (pow base exponent) = Formats.Posit.Model.RealRounding.roundPositive format (↑b ^ ↑e)

Nonnegative configured bases in the real domain round the exact real power once.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_roundRat_of_neg {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : b < 0) (hinteger : e.den = 1) : toModel (pow base exponent) = Formats.Posit.Model.roundRat format (b ^ e.num)

Negative configured bases with integral exponents round their exact rational power once.

theorem FloatLib.Floats.ExecFloat.Posit.pow_eq_nar_of_neg_nonintegral {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (base exponent : ExecFloat (Formats.Posit.Configured.Family format code plan)) {b e : ℚ} (hbase : toRat? base = some b) (hexponent : toRat? exponent = some e) (hb : b < 0) (hinteger : e.den ≠ 1) : toModel (pow base exponent) = Formats.Posit.Model.nar format

A negative configured base with a nonintegral exponent produces NaR.

theorem FloatLib.Floats.ExecFloat.Posit.exp2_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp2 value) = Formats.Posit.Model.RealRounding.roundPositive format (2 ^ ↑e)

Every finite configured base-two exponential rounds the exact real power.

theorem FloatLib.Floats.ExecFloat.Posit.exp10_eq_roundPositive {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp10 value) = Formats.Posit.Model.RealRounding.roundPositive format (10 ^ ↑e)

Every finite configured base-ten exponential rounds the exact real power.

theorem FloatLib.Floats.ExecFloat.Posit.exp2Minus1_eq_round {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp2Minus1 value) = Formats.Posit.Model.RealRounding.round format (2 ^ ↑e - 1)

A finite configured base-two exponential minus one rounds the exact fused expression.

theorem FloatLib.Floats.ExecFloat.Posit.exp10Minus1_eq_round {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : ExecFloat (Formats.Posit.Configured.Family format code plan)) {e : ℚ} (hvalue : toRat? value = some e) : toModel (exp10Minus1 value) = Formats.Posit.Model.RealRounding.round format (10 ^ ↑e - 1)

A finite configured base-ten exponential minus one rounds the exact fused expression.