Semantics of interior Posit field layouts

The native guard/sticky packer constructs an unsigned Posit from a regime prefix and a retained exponent/fraction tail. This module proves the representation-independent meaning of the two interior layouts:

• a positive regime is a run of ones followed by a zero terminator;
• a negative regime is a run of zeros followed by a one terminator.

Both the retained code and the standard's one-bit-wider rounding boundary use these layouts. Keeping the decoder argument here lets scalar, fixed-limb, division, and square-root kernels share one proof without depending on UInt64.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_maxPositive (format : Format) : nonnegativeRatAt format (format.signMaskNat - 1) = 2 ^ ((Int.ofNat format.payloadBits - 1) * 4)

Decode the all-ones positive payload.

maxPos has a regime run occupying the complete payload, no terminator, and no trailing field. Its regime value is therefore payloadBits - 1.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_positiveInterior (format : Format) (run tail : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) (htail : tail < 2 ^ (format.payloadBits - run - 1)) : have code := (2 ^ run - 1) * 2 ^ (format.payloadBits - run) + tail; nonnegativeRatAt format code = trailingRat (format.payloadBits - run - 1) tail * 2 ^ ((Int.ofNat run - 1) * 4)

Decode an interior positive-regime layout.

The hypotheses say that the regime run and its terminator fit in the payload and that tail fits in every remaining position. The result exposes the exact tail value and regime scale while hiding all variable-length decoder bookkeeping.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_negativeInterior (format : Format) (run tail : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) (htail : tail < 2 ^ (format.payloadBits - run - 1)) : have code := 2 ^ (format.payloadBits - run - 1) + tail; nonnegativeRatAt format code = trailingRat (format.payloadBits - run - 1) tail * 2 ^ (-Int.ofNat run * 4)

Decode an interior negative-regime layout.

The terminator is the single one above tail. The leading-zero count therefore recovers run, and the low tail positions have the same rational interpretation as in the positive layout.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_positiveInteriorCarry (format : Format) (run : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) : nonnegativeRatAt format ((2 ^ run - 1) * 2 ^ (format.payloadBits - run) + (2 ^ (format.payloadBits - run - 1) - 1) + 1) = 2 ^ (Int.ofNat run * 4)

Decode the successor of a positive-regime code whose retained tail is all ones.

Adding one carries through the complete retained tail into the regime. For an interior run this produces the zero-tail base of the next positive regime; at the final run it produces maxPos. This is the representation lemma needed to prove that the native lower candidate and its packed successor are adjacent Posits.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_negativeInteriorCarry (format : Format) (run : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) : nonnegativeRatAt format (2 ^ (format.payloadBits - run - 1) + (2 ^ (format.payloadBits - run - 1) - 1) + 1) = 2 ^ ((-Int.ofNat run + 1) * 4)

Decode the successor of a negative-regime code whose retained tail is all ones.

The carry shortens the run of leading zeros, so the successor is the zero-tail base of the next larger regime. The run = 1 case crosses the central regime boundary and is handled explicitly.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_positiveInteriorThreshold (format : Format) (run tail : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) (htail : tail < 2 ^ (format.payloadBits - run - 1)) : nonnegativeRatAt format.nextPrecision (2 * ((2 ^ run - 1) * 2 ^ (format.payloadBits - run) + tail) + 1) = trailingRat (format.payloadBits - run - 1 + 1) (2 * tail + 1) * 2 ^ ((Int.ofNat run - 1) * 4)

Decode the standard one-bit-wider boundary above a positive-regime retained code.

Doubling the retained code appends 0; adding one changes only that new bit. Consequently the regime is unchanged and the trailing field is exactly 2 * tail + 1.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.nonnegativeRatAt_negativeInteriorThreshold (format : Format) (run tail : ℕ) (hrunPos : 0 < run) (hrun : run < format.payloadBits) (htail : tail < 2 ^ (format.payloadBits - run - 1)) : nonnegativeRatAt format.nextPrecision (2 * (2 ^ (format.payloadBits - run - 1) + tail) + 1) = trailingRat (format.payloadBits - run - 1 + 1) (2 * tail + 1) * 2 ^ (-Int.ofNat run * 4)

Decode the standard one-bit-wider boundary above a negative-regime retained code.

As in the positive case, appending 1 preserves the regime and extends the trailing field by one bit. The theorem is separated only because the two variable-length regime layouts differ.