Shared fixed-word posit kernels

The public UInt8, UInt16, UInt32, and UInt64 entry points are thin monomorphic wrappers around these always-inlined definitions. Arithmetic is performed by the same proved packed UInt64 kernels for every carrier; only widening and narrowing vary.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.widened_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} {value : α} (hvalue : carrier.toNat value < format.modulus) : (carrier.toUInt64 value).toNat < format.modulus

Widening an in-range carrier word to UInt64 keeps it below the posit modulus.

Always-inlined raw kernels

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.addRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : α

Carrier-generic packed addition.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.subRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : α

Carrier-generic packed subtraction.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.mulRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : α

Carrier-generic packed multiplication.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.divRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : α

Carrier-generic packed division.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.sqrtRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (value : α) (hvalue : carrier.toNat value < format.modulus) : α

Carrier-generic packed square root.

@[always_inline]

def FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.fmaRaw {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) (format : Format) (width_le : format.bits ≤ capacity) (left right addend : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) (haddend : carrier.toNat addend < format.modulus) : α

Carrier-generic packed fused multiply-add.

Shared range certificates

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.addRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (addRaw carrier format width_le left right hleft hright) < format.modulus

Raw addition of in-range words returns a word below the posit modulus.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.subRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (subRaw carrier format width_le left right hleft hright) < format.modulus

Raw subtraction of in-range words returns a word below the posit modulus.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.mulRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (mulRaw carrier format width_le left right hleft hright) < format.modulus

Raw multiplication of in-range words returns a word below the posit modulus.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.divRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (divRaw carrier format width_le left right hleft hright) < format.modulus

Raw division of in-range words returns a word below the posit modulus.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.sqrtRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (value : α) (hvalue : carrier.toNat value < format.modulus) : carrier.toNat (sqrtRaw carrier format width_le value hvalue) < format.modulus

The raw square root of an in-range word is below the posit modulus.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.fmaRaw_lt_modulus {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right addend : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) (haddend : carrier.toNat addend < format.modulus) : carrier.toNat (fmaRaw carrier format width_le left right addend hleft hright haddend) < format.modulus

Raw fused multiply-add of in-range words returns a word below the posit modulus.

Shared observations used by semantic refinement

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.validCode_eq_of_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (value : α) (hvalue : carrier.toNat value < format.modulus) (result : ℕ) (result_lt : result < format.modulus) (value_eq : carrier.toNat value = carrier.toNat (carrier.ofNat result)) : ⟨value, hvalue⟩ = ⟨carrier.ofNat result, ⋯⟩

Two range-checked carrier values are equal when their natural-number observations agree.

The width hypothesis is used only to construct the right-hand range certificate. This theorem is proof-only and does not change the monomorphic fixed-word runtime boundary.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.addRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (addRaw carrier format width_le left right hleft hright) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.addWordsCodeFlatValid ⋯ (carrier.toUInt64 left) (carrier.toUInt64 right) ⋯ ⋯))

Raw fixed-carrier addition and configured native packing produce the same code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.subRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (subRaw carrier format width_le left right hleft hright) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.subWordsCodeFlatValid ⋯ (carrier.toUInt64 left) (carrier.toUInt64 right) ⋯ ⋯))

Raw fixed-carrier subtraction and configured native packing produce the same code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.mulRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (mulRaw carrier format width_le left right hleft hright) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.PackedProduct.mulWordsCodeValid ⋯ (carrier.toUInt64 left) (carrier.toUInt64 right) ⋯ ⋯))

Raw fixed-carrier multiplication and configured native packing produce the same code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.divRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) : carrier.toNat (divRaw carrier format width_le left right hleft hright) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.PackedQuotient.divWordsCodeValid ⋯ (carrier.toUInt64 left) (carrier.toUInt64 right) ⋯ ⋯))

Raw fixed-carrier division and configured native packing produce the same code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.sqrtRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (value : α) (hvalue : carrier.toNat value < format.modulus) : carrier.toNat (sqrtRaw carrier format width_le value hvalue) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeValid ⋯ (carrier.toUInt64 value) ⋯))

Raw fixed-carrier square root and configured native packing produce the same code.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.fmaRaw_toNat_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right addend : α) (hleft : carrier.toNat left < format.modulus) (hright : carrier.toNat right < format.modulus) (haddend : carrier.toNat addend < format.modulus) : carrier.toNat (fmaRaw carrier format width_le left right addend hleft hright haddend) = carrier.toNat (carrier.ofNat (Model.NativeWordArithmetic.fmaWordsCodeFlatValid ⋯ (carrier.toUInt64 left) (carrier.toUInt64 right) (carrier.toUInt64 addend) ⋯ ⋯ ⋯))

Raw fixed-carrier FMA and configured native packing produce the same code.

Range-checked carrier equalities

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.addCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : { bits : α // carrier.toNat bits < format.modulus }) : ⟨addRaw carrier format width_le ↑left ↑right ⋯ ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.addWordsCodeFlatValid ⋯ (carrier.toUInt64 ↑left) (carrier.toUInt64 ↑right) ⋯ ⋯), ⋯⟩

Fixed-carrier addition returns the same range-checked code as exact native-word packing.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.subCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : { bits : α // carrier.toNat bits < format.modulus }) : ⟨subRaw carrier format width_le ↑left ↑right ⋯ ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.subWordsCodeFlatValid ⋯ (carrier.toUInt64 ↑left) (carrier.toUInt64 ↑right) ⋯ ⋯), ⋯⟩

Fixed-carrier subtraction returns the same code as exact native-word packing.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.mulCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : { bits : α // carrier.toNat bits < format.modulus }) : ⟨mulRaw carrier format width_le ↑left ↑right ⋯ ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.PackedProduct.mulWordsCodeValid ⋯ (carrier.toUInt64 ↑left) (carrier.toUInt64 ↑right) ⋯ ⋯), ⋯⟩

Fixed-carrier multiplication returns the same code as exact native-word packing.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.divCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right : { bits : α // carrier.toNat bits < format.modulus }) : ⟨divRaw carrier format width_le ↑left ↑right ⋯ ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.PackedQuotient.divWordsCodeValid ⋯ (carrier.toUInt64 ↑left) (carrier.toUInt64 ↑right) ⋯ ⋯), ⋯⟩

Fixed-carrier division returns the same code as exact native-word packing.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.sqrtCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (value : { bits : α // carrier.toNat bits < format.modulus }) : ⟨sqrtRaw carrier format width_le ↑value ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.PackedSquareRoot.sqrtWordCodeValid ⋯ (carrier.toUInt64 ↑value) ⋯), ⋯⟩

Fixed-carrier square root returns the same code as exact native-word packing.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.FixedWords.fmaCode_eq {α : Type} {capacity : ℕ} (carrier : Carrier α capacity) {format : Format} (width_le : format.bits ≤ capacity) (left right addend : { bits : α // carrier.toNat bits < format.modulus }) : ⟨fmaRaw carrier format width_le ↑left ↑right ↑addend ⋯ ⋯ ⋯, ⋯⟩ = ⟨carrier.ofNat (Model.NativeWordArithmetic.fmaWordsCodeFlatValid ⋯ (carrier.toUInt64 ↑left) (carrier.toUInt64 ↑right) (carrier.toUInt64 ↑addend) ⋯ ⋯ ⋯), ⋯⟩

Fixed-carrier FMA returns the same code as exact native-word packing.