TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.Posit.Configured.Value.Proof

Correctness of the configured posit value interface #

The public constructors form a lossless equivalence with the exact-width model and every in-range word. Exact decoding and classification preserve the standardized zero and NaR observations, and the common Boolean comparison API agrees with the configured signed-word order.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compare_def {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compare right = some (cmp (toModel left) (toModel right))

The common comparison capability reduces to signed-word posit comparison.

This theorem is the public semantic boundary for proofs: clients need not unfold the typeclass instance or depend on its implementation name.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.toModel_ofModel {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (value : Formats.Posit.Model format) :
toModel (ofModel value) = value

Decoding immediately after packing a posit proof model returns the original model.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.ofModel_toModel {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)) :
ofModel (toModel value) = value

Packing immediately after decoding a configured posit returns the original value.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.ofNatBits_toNatBits {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)) :
ofNatBits (toNatBits value) = value

Reconstructing a configured posit from its complete word is lossless.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.toNatBits_ofNatBits_of_lt {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (bits : ℕ) (bits_lt : bits < format.modulus) :
toNatBits (ofNatBits bits) = bits

Reading an in-range complete posit word immediately after constructing it returns that word.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.decode_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
decode zero = Numerics.NumericalValue.finite 0

The configured zero code denotes the ordinary rational value zero.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.decode_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
decode nar = Numerics.NumericalValue.exceptional Numerics.ExceptionalValue.notAReal

The configured NaR code denotes the common exceptional Not-a-Real observation.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.isZero_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
isZero zero = true

The configured zero code is recognized as zero.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.isNaR_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
isNaR nar = true

The configured NaR code is recognized as Not-a-Real.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.isNaR_zero {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
isNaR zero = false

The configured zero code is not Not-a-Real.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.isZero_nar {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] :
isZero nar = false

The configured NaR code is not the ordinary zero code.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.toRat?_eq_none_iff {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)) :
toRat? value = none ↔ isNaR value = true

The public optional rational view is absent precisely for the unique NaR value.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareEqual_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareEqual right = true ↔ left = right

Boolean posit equality agrees exactly with equality of configured values.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareNotEqual_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareNotEqual right = true ↔ left ≠ right

Boolean posit inequality agrees exactly with inequality of configured values.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareLess_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareLess right = true ↔ left < right

Boolean posit less-than agrees with the standard signed-word order.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareLessEqual_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareLessEqual right = true ↔ left ≤ right

Boolean posit less-than-or-equal agrees with the standard signed-word order.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareGreater_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareGreater right = true ↔ left > right

Boolean posit greater-than agrees with the standard signed-word order.

source
@[simp]
theorem FloatLib.Floats.ExecFloat.Posit.compareGreaterEqual_eq_true_iff {format : Formats.Posit.Format} {plan : Formats.Posit.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.Posit.Model format) code] (left right : ExecFloat (Formats.Posit.Configured.Family format code plan)) :
left.compareGreaterEqual right = true ↔ left ≥ right

Boolean posit greater-than-or-equal agrees with the standard signed-word order.