Correctness of direct exact-dyadic posit packing

The one-pass scale, regime, exponent, fraction, guard, and sticky calculation in Direct.Runtime refines the exact posit rounding specification at every width. It covers regimes that consume the payload, appended-bit threshold ties, finite-endpoint saturation, and negative results obtained through posit negation.

Direct packing avoids the reference rounder's search. Their equality gives both algorithms the same semantics at every configured width.

Complete arbitrary-width rounding

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositiveCode_eq_dyadic (format : Format) (target : Numerics.Dyadic) : roundPositiveCode format target = DyadicRounding.roundPositiveCode format target

Direct positive rounding selects exactly the shared exact-dyadic code.

Shift-with-jam preservation

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositiveCode_shiftRightJam (format : Format) (window : ℕ) (hwindow : 2 ≤ window) (hpayload : format.payloadBits ≤ window) (significand shift : ℕ) (exponent : ℤ) (hlower : 2 ^ (shift + window) ≤ significand) (hupper : significand < 2 ^ (shift + window + 1)) (hjammedUpper : Numerics.shiftRightJam significand shift < 2 ^ (window + 1)) : roundPositiveCode format { negative := false, significand := Numerics.shiftRightJam significand shift, exponent := exponent + Int.ofNat shift } = roundPositiveCode format { negative := false, significand := significand, exponent := exponent }

Retaining a normalized leading window and jamming every discarded one into its low bit preserves the complete direct Posit code.

The theorem is independent of a storage carrier. The retained value has its leading one at index window, so it occupies window + 1 bits. The bounds 2 ≤ window and format.payloadBits ≤ window leave room for the rounding information. The dyadic exponent increases by the discarded shift.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositiveCode_lt_signMask (format : Format) (target : Numerics.Dyadic) : roundPositiveCode format target < format.signMaskNat

Direct positive rounding always returns a nonnegative finite code.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundPositive_eq_dyadic (format : Format) (target : Numerics.Dyadic) : roundPositive format target = DyadicRounding.roundPositive format target

Direct positive result packing is extensionally the shared dyadic rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.roundCode_lt_modulus (format : Format) (value : Numerics.Dyadic) : roundCode format value < format.modulus

Every direct signed code is a valid complete Posit encoding.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.ofNatBits_roundCode (format : Format) (value : Numerics.Dyadic) : ofNatBits (roundCode format value) = round format value

Re-encoding the direct code gives the model-valued direct rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.round_eq_dyadic (format : Format) (value : Numerics.Dyadic) : round format value = DyadicRounding.round format value

Complete direct exact-dyadic rounding equals the exact model rounder.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicPacking.round_eq_roundRat (format : Format) (value : Numerics.Dyadic) : round format value = roundRat format value.toRat

Complete direct rounding therefore equals exact rational Posit Standard rounding.