Posit sign and unsigned magnitude

Posit negation is two's complement over the complete encoded word. Field decoding works on the corresponding unsigned magnitude, so this module isolates the representation laws connecting the two views.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.neg {format : Format} (value : Model format) : Model format

Negate a posit by taking the two's complement of its entire encoded word.

This operation fixes both zero and NaR and exchanges every positive finite code with its negative counterpart, exactly as specified by the posit encoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.neg_zero (format : Format) : (zero format).neg = zero format

Posit negation fixes the unique zero encoding.

@[simp]

theorem FloatLib.Floats.Formats.Posit.Model.neg_nar (format : Format) : (nar format).neg = nar format

Posit two's-complement negation fixes the unique NaR encoding.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.signBit {format : Format} (value : Model format) : Bool

Whether the encoded sign bit is set.

theorem FloatLib.Floats.Formats.Posit.Model.signBit_eq_decide {format : Format} (value : Model format) : value.signBit = decide (format.signMaskNat ≤ value.toNatBits)

Sign-bit inspection is unsigned comparison with the descriptor's sign mask.

theorem FloatLib.Floats.Formats.Posit.Model.signBit_ofNatBits_eq_decide (format : Format) (code : ℕ) (hcode : code < format.modulus) : (ofNatBits code).signBit = decide (format.signMaskNat ≤ code)

Exact-width encoding exposes the expected sign for every in-range natural word.

theorem FloatLib.Floats.Formats.Posit.Model.signBit_ofNatBits_eq_false (format : Format) (code : ℕ) (hcode : code < format.signMaskNat) : (ofNatBits code).signBit = false

An in-range word below the sign mask has a clear sign bit.

@[inline]

def FloatLib.Floats.Formats.Posit.Model.magnitudeBits {format : Format} (value : Model format) : ℕ

Unsigned magnitude word used to decode the regime and trailing fields.

Negative posit encodings are the two's complement of the corresponding positive word.

theorem FloatLib.Floats.Formats.Posit.Model.magnitudeBits_ofNatBits_of_lt_signMask (format : Format) (code : ℕ) (hcode : code < format.signMaskNat) : (ofNatBits code).magnitudeBits = code

A nonnegative in-range encoding is its own unsigned decoding magnitude.

theorem FloatLib.Floats.Formats.Posit.Model.magnitudeBits_lt_signMask_of_ne_nar {format : Format} (value : Model format) (hnar : value ≠ nar format) : value.magnitudeBits < format.signMaskNat

Every posit other than NaR has unsigned magnitude strictly below the sign mask.

theorem FloatLib.Floats.Formats.Posit.Model.magnitudeBits_ne_zero_of_ne_zero {format : Format} (value : Model format) (hzero : value ≠ zero format) : value.magnitudeBits ≠ 0

Every nonzero posit has nonzero unsigned magnitude.