Bit preservation and datum semantics of decimal sign operations

Decimal sign replacement preserves every payload bit, including in noncanonical words. Decoding commutes with sign replacement, negation, absolute value, and sign copying for every codec.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.isSignMinus_withSign (s : Bool) (d : Datum) : (withSign s d).isSignMinus = s

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.withSign_isSignMinus (d : Datum) : withSign d.isSignMinus d = d

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.withSign_withSign (s t : Bool) (d : Datum) : withSign t (withSign s d) = withSign t d

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.negate_eq_withSign (d : Datum) : d.negate = withSign (!d.isSignMinus) d

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.negate_negate (d : Datum) : d.negate.negate = d

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.withSign_valid (f : Format) (s : Bool) (d : Datum) : Valid f (withSign s d) ↔ Valid f d

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.withSign_isSignaling (s : Bool) (d : Datum) : (withSign s d).isSignaling = d.isSignaling

theorem FloatLib.Floats.Formats.DecimalInterchange.Datum.negate_toRat? (d : Datum) : d.negate.toRat? = Option.map (fun (x : ℚ) => -x) d.toRat?

Reversing a finite sign negates the exact rational, including at zero.

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.negative_withSign (f : Format) (s : Bool) (w : BitVec f.bitWidth) : negative f (withSign f s w) = s

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.payload_withSign (f : Format) (s : Bool) (w : BitVec f.bitWidth) : payload f (withSign f s w) = payload f w

All bits below the sign are unchanged, even for noncanonical words.

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.pack_negative_payload (f : Format) (w : BitVec f.bitWidth) : pack f (negative f w) (payload f w) = w

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.withSign_negative (f : Format) (w : BitVec f.bitWidth) : withSign f (negative f w) w = w

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.withSign_withSign (f : Format) (s t : Bool) (w : BitVec f.bitWidth) : withSign f t (withSign f s w) = withSign f t w

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.negate_negate (f : Format) (w : BitVec f.bitWidth) : negate f (negate f w) = w

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.abs_abs (f : Format) (w : BitVec f.bitWidth) : abs f (abs f w) = abs f w

@[simp]

theorem FloatLib.Floats.Formats.DecimalInterchange.Bits.copySign_self (f : Format) (w : BitVec f.bitWidth) : copySign f w w = w

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_withSign (codec : Codec) (f : Format) (s : Bool) (w : BitVec f.bitWidth) : codec.decode f (Bits.withSign f s w) = Datum.withSign s (codec.decode f w)

Decoding sign replacement preserves the coefficient, quantum and NaN metadata. This holds for every codec and every word, without a canonicality hypothesis.

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_isSignMinus (codec : Codec) (f : Format) (w : BitVec f.bitWidth) : (codec.decode f w).isSignMinus = Bits.negative f w

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_negate (codec : Codec) (f : Format) (w : BitVec f.bitWidth) : codec.decode f (Bits.negate f w) = (codec.decode f w).negate

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_abs (codec : Codec) (f : Format) (w : BitVec f.bitWidth) : codec.decode f (Bits.abs f w) = (codec.decode f w).abs

theorem FloatLib.Floats.Formats.DecimalInterchange.Codec.decode_copySign (codec : Codec) (f : Format) (x y : BitVec f.bitWidth) : codec.decode f (Bits.copySign f x y) = (codec.decode f x).copySign (codec.decode f y)