Correctness of flattened packed-word exact-dyadic posit arithmetic

The flattened packed-word kernels agree with the shared exact-dyadic operations, preserve the complete posit encoding range, and admit verified compiler substitutions. Executable definitions live in FloatLib.Floats.Formats.Posit.Arithmetic.Word.Packed.Dyadic.Runtime.

Addition

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.addWordsCodeFlat_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) : addWordsCodeFlat heligible left right = addWordsCode heligible left right

Flattened scalar-field addition is the exact packed-word addition.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.addWordsCodeFlatValid_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : addWordsCodeFlatValid heligible left right hleft hright = addWordsCodeFlat heligible left right

Valid-word addition is exactly flattened packed-word addition.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.addWordsCodeFlatValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : addWordsCodeFlatValid heligible left right hleft hright < format.modulus

Every valid-word addition result is a complete in-range posit encoding.

@[csimp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.addWordsCode_eq_addWordsCodeFlat : @addWordsCode = @addWordsCodeFlat

Compile exact packed addition through scalar-field elimination.

Subtraction

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.subWordsCodeFlat_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) : subWordsCodeFlat heligible left right = subWordsCode heligible left right

Flattened scalar-field subtraction is the exact packed-word subtraction.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.subWordsCodeFlatValid_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : subWordsCodeFlatValid heligible left right hleft hright = subWordsCodeFlat heligible left right

Valid-word subtraction is exactly flattened packed-word subtraction.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.subWordsCodeFlatValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : subWordsCodeFlatValid heligible left right hleft hright < format.modulus

Every valid-word subtraction result is a complete in-range posit encoding.

@[csimp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.subWordsCode_eq_subWordsCodeFlat : @subWordsCode = @subWordsCodeFlat

Compile exact packed subtraction through scalar-field elimination.

Multiplication

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.mulWordsCodeFlat_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) : mulWordsCodeFlat heligible left right = mulWordsCode heligible left right

Flattened scalar-field multiplication is the exact packed-word multiplier.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.mulWordsCodeFlatValid_eq {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : mulWordsCodeFlatValid heligible left right hleft hright = mulWordsCodeFlat heligible left right

Valid-word multiplication is exactly flattened packed-word multiplication.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.mulWordsCodeFlatValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) : mulWordsCodeFlatValid heligible left right hleft hright < format.modulus

Every valid-word multiplication result is a complete in-range posit encoding.

@[csimp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.mulWordsCode_eq_mulWordsCodeFlat : @mulWordsCode = @mulWordsCodeFlat

Compile exact packed multiplication through scalar-field elimination.

Fused multiply-add

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.fmaWordsCodeFlat_eq {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) : fmaWordsCodeFlat heligible left right addend = fmaWordsCode heligible left right addend

Flattened scalar-field FMA is the exact packed-word FMA.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.fmaWordsCodeFlatValid_eq {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) : fmaWordsCodeFlatValid heligible left right addend hleft hright haddend = fmaWordsCodeFlat heligible left right addend

Valid-word FMA is exactly flattened packed-word FMA.

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.fmaWordsCodeFlatValid_lt_modulus {format : Format} (heligible : NativeWord.Eligible format) (left right addend : UInt64) (hleft : left.toNat < format.modulus) (hright : right.toNat < format.modulus) (haddend : addend.toNat < format.modulus) : fmaWordsCodeFlatValid heligible left right addend hleft hright haddend < format.modulus

Every valid-word FMA result is a complete in-range posit encoding.

@[csimp]

theorem FloatLib.Floats.Formats.Posit.Model.NativeWordArithmetic.fmaWordsCode_eq_fmaWordsCodeFlat : @fmaWordsCode = @fmaWordsCodeFlat

Compile exact packed FMA through scalar-field elimination.