Correctness of the fixed UInt8 posit backend

Each monomorphic UInt8 operation first agrees with the shared carrier-generic packed kernel, then inherits that kernel's proof against the representation-independent specification.

Addition and subtraction

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.add_eq_spec {format : Format} (width_le : format.bits ≤ 8) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : add width_le left right = Spec.add left right

Fixed UInt8 addition refines configured posit addition.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.sub_eq_spec {format : Format} (width_le : format.bits ≤ 8) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : sub width_le left right = Spec.sub left right

Fixed UInt8 subtraction refines configured posit subtraction.

Multiplication and division

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.mul_eq_spec {format : Format} (width_le : format.bits ≤ 8) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : mul width_le left right = Spec.mul left right

Fixed UInt8 multiplication refines configured posit multiplication.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.div_eq_spec {format : Format} (width_le : format.bits ≤ 8) (left right : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : div width_le left right = Spec.div left right

Fixed UInt8 division refines configured posit division.

Square root and fused multiply-add

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.sqrt_eq_spec {format : Format} (width_le : format.bits ≤ 8) (value : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : sqrt width_le value = Spec.sqrt value

Fixed UInt8 square root refines configured posit square root.

theorem FloatLib.Floats.Formats.Posit.Configured.Backend.Byte.fma_eq_spec {format : Format} (width_le : format.bits ≤ 8) (left right addend : ExecFloat (Family format (Code (StoragePlan.byte width_le)) (StoragePlan.byte width_le))) : fma width_le left right addend = Spec.fma left right addend

Fixed UInt8 FMA refines configured posit FMA.