Laws and correctness of shared fixed-carrier guard-and-sticky rounding

LawfulTailCarrier and LawfulCandidateCarrier state the natural-number meaning of the carrier operations that GuardStickyCarrier uses. Each law is as narrow as the shared kernel needs: the arithmetic laws hold only under the bounds the kernel establishes, so wrapping machine operations satisfy them. Concrete UInt64 and UInt128 records are proved lawful beside their kernels.

Given a lawful carrier of capacity bits and a format whose payload is shorter than capacity, the theorems below show that the shared kernel is an execution refinement of the arbitrary-width direct rounder: tailBit_eq_spec and tailHasNonzeroAfter_eq_spec for inspection, lowerCandidateFromFields_toNat for packing, and roundNormalizedPositive_toNat_eq_direct for the complete positive rounder against DirectDyadicPacking.roundPositiveCode.

structure FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.LawfulTailCarrier {α : Type} (carrier : TailCarrier α) (toNat : α → ℕ) : Prop

Natural-number semantics of a finite-tail carrier.

This explicit record lives in Prop; the executable carrier contains only the operations.

• bitAt_eq_testBit (value : α) (index : ℕ) : carrier.bitAt value index = (toNat value).testBit index

  Carrier bit reads agree with natural-number bit reads.

• hasLowBits_eq (value : α) (width : ℕ) : carrier.hasLowBits value width = (toNat value % 2 ^ width != 0)

  Carrier suffix tests are natural-number remainder tests.

structure FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.LawfulCandidateCarrier {α : Type} (carrier : CandidateCarrier α) (toNat : α → ℕ) (capacity : ℕ) extends FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.LawfulTailCarrier carrier.toTailCarrier toNat : Prop

Natural-number semantics of a candidate carrier of capacity bits.

Each law holds only under the bound the shared rounder establishes before applying the operation, so the record can be instantiated by wrapping machine arithmetic. Like LawfulTailCarrier, it is an explicit proof record rather than a typeclass.

• bitAt_eq_testBit (value : α) (index : ℕ) : carrier.bitAt value index = (toNat value).testBit index
• hasLowBits_eq (value : α) (width : ℕ) : carrier.hasLowBits value width = (toNat value % 2 ^ width != 0)
• toNat_lt (value : α) : toNat value < 2 ^ capacity

  Every carrier value is below 2 ^ capacity.

• toNat_ofWord (word : UInt64) : toNat (carrier.ofWord word) = word.toNat

  Embedding a machine word is exact.

• shiftLeft_toNat (value : α) (shift : ℕ) : shift < capacity → toNat value <<< shift < 2 ^ capacity → toNat (carrier.shiftLeft value shift) = toNat value <<< shift

  A left shift below the carrier width whose result fits is exact.

• shiftRight_toNat (value : α) (shift : ℕ) : shift < capacity → toNat (carrier.shiftRight value shift) = toNat value >>> shift

  A right shift below the carrier width is exact.

• fractionBelow_toNat (value : α) (leading : ℕ) : leading < capacity → 2 ^ leading ≤ toNat value → toNat value < 2 ^ (leading + 1) → toNat (carrier.fractionBelow value leading) = toNat value - 2 ^ leading

  Removing the leading one of a normalized significand subtracts its power of two.

• add_toNat (left right : α) : toNat left + toNat right < 2 ^ capacity → toNat (carrier.add left right) = toNat left + toNat right

  Addition is exact when the mathematical sum fits the carrier.

• lowOnes_toNat (width : ℕ) : width < capacity → toNat (carrier.lowOnes width) = 2 ^ width - 1

  The low-ones mask below the carrier width has its mathematical value.

• increment_toNat (value : α) : toNat value + 1 < 2 ^ capacity → toNat (carrier.increment value) = toNat value + 1

  The successor is exact when it fits the carrier.

• isOdd_eq (value : α) : carrier.isOdd value = (toNat value % 2 != 0)

  The parity test reads the least significant bit.

• log2_eq (value : α) : carrier.log2 value = (toNat value).log2

  The leading-bit index is the natural-number logarithm.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailBit_eq_spec {α : Type} {carrier : TailCarrier α} {toNat : α → ℕ} (lawful : LawfulTailCarrier carrier toNat) (exponentField : UInt64) (significand : α) (leading index : ℕ) : tailBit carrier exponentField significand leading index = GuardStickyRounding.tailBit exponentField.toNat (toNat significand) leading index

Shared carrier bit inspection reads the representation-independent normalized tail stream.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailHasNonzeroAfter_eq_spec {α : Type} {carrier : TailCarrier α} {toNat : α → ℕ} (lawful : LawfulTailCarrier carrier toNat) (exponentField : UInt64) (significand : α) (leading consumed : ℕ) : tailHasNonzeroAfter carrier exponentField significand leading consumed = GuardStickyRounding.tailHasNonzeroAfter exponentField.toNat (toNat significand) leading consumed

Shared carrier suffix inspection is the representation-independent sticky-bit query.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.isLessPowerOfTwoAtLeading_leadingBit_eq_isLess_minPositive (format : Format) (significand : ℕ) (exponent : ℤ) : Numerics.Dyadic.isLessPowerOfTwoAtLeading significand exponent (DirectDyadicPacking.leadingBit significand) (-(4 * Int.ofNat (format.payloadBits - 1))) = { negative := false, significand := significand, exponent := exponent }.isLess (DyadicRounding.minPositive format)

The direct rounder's leading-bit underflow test is exact comparison against the smallest positive posit. This fact is independent of the native carrier used by a backend.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.emod_four_toNat_lt (scale : ℤ) : (scale.emod 4).toNat < 4

The exponent field extracted from a scale occupies the two standard exponent bits.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyRounding.toNat_ofNat_emod_four_toNat (scale : ℤ) : (UInt64.ofNat (scale.emod 4).toNat).toNat = (scale.emod 4).toNat

Storing the two-bit exponent field in a machine word is exact.

Packed field refinement

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.fractionPrefix_toNat {α : Type} {carrier : CandidateCarrier α} {toNat : α → ℕ} {capacity : ℕ} (lawful : LawfulCandidateCarrier carrier toNat capacity) (significand : α) (leading count : ℕ) (hleading : leading < capacity) (hcount : count < capacity) (hlower : 2 ^ leading ≤ toNat significand) (hupper : toNat significand < 2 ^ (leading + 1)) : toNat (fractionPrefix carrier significand leading count) = DirectDyadicPacking.fractionPrefix (toNat significand) leading count

The shared fraction-prefix kernel implements the representation-independent normalized prefix.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.tailPrefix_toNat {α : Type} {carrier : CandidateCarrier α} {toNat : α → ℕ} {capacity : ℕ} (lawful : LawfulCandidateCarrier carrier toNat capacity) (exponentField : UInt64) (significand : α) (leading count : ℕ) (hleading : leading < capacity) (hcount : count < capacity) (hexponent : exponentField.toNat < 4) (hlower : 2 ^ leading ≤ toNat significand) (hupper : toNat significand < 2 ^ (leading + 1)) : toNat (tailPrefix carrier exponentField significand leading count) = DirectDyadicPacking.tailPrefix exponentField.toNat (toNat significand) leading count

The shared exponent/fraction prefix is the representation-independent tail prefix.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.lowerCandidateFromFields_toNat {α : Type} {carrier : CandidateCarrier α} {toNat : α → ℕ} {capacity : ℕ} (lawful : LawfulCandidateCarrier carrier toNat capacity) (format : Format) (regime : ℤ) (exponentField : UInt64) (significand : α) (leading : ℕ) (hpayload : format.payloadBits < capacity) (hleading : leading < capacity) (hexponent : exponentField.toNat < 4) (hlower : 2 ^ leading ≤ toNat significand) (hupper : toNat significand < 2 ^ (leading + 1)) : toNat (lowerCandidateFromFields carrier format regime exponentField significand leading) = DirectDyadicPacking.lowerCandidateFromFields format regime exponentField.toNat (toNat significand) leading

Shared field packing implements the representation-independent lower-candidate constructor whenever the format's payload is shorter than the carrier.

Rounding

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.roundInterior_toNat {α : Type} {carrier : CandidateCarrier α} {toNat : α → ℕ} {capacity : ℕ} (lawful : LawfulCandidateCarrier carrier toNat capacity) (format : Format) (regime : ℤ) (exponentField : UInt64) (significand : α) (leading regimeFieldBits : ℕ) (hpayload : format.payloadBits < capacity) (hleading : leading < capacity) (hexponent : exponentField.toNat < 4) (hlower : 2 ^ leading ≤ toNat significand) (hupper : toNat significand < 2 ^ (leading + 1)) : toNat (roundInterior carrier format regime exponentField significand leading regimeFieldBits) = GuardStickyRounding.roundInteriorCodeFromFields format regime exponentField.toNat (toNat significand) leading regimeFieldBits

The shared interior rounder implements the field-oriented nearest-even rule.

The theorem covers packed field construction, guard/sticky inspection, retained parity, and the increment, whose result fits the carrier.

theorem FloatLib.Floats.Formats.Posit.Model.GuardStickyCarrier.roundNormalizedPositive_toNat_eq_direct {α : Type} {carrier : CandidateCarrier α} {toNat : α → ℕ} {capacity : ℕ} (lawful : LawfulCandidateCarrier carrier toNat capacity) (format : Format) (significand : α) (exponent : ℤ) (hpayload : format.payloadBits < capacity) (hnonzero : toNat significand ≠ 0) (hnotUnderflow : { negative := false, significand := toNat significand, exponent := exponent }.isLess (DyadicRounding.minPositive format) = false) : toNat (roundNormalizedPositive carrier format significand exponent) = DirectDyadicPacking.roundPositiveCode format { negative := false, significand := toNat significand, exponent := exponent }

The shared normalized rounder is the arbitrary-width direct positive rounder.

The hypotheses are the checks a caller performs before entering the carrier: the significand is nonzero and the value is not below minPos. The payload bound is what makes every intermediate fit the carrier.