Bounded static storage

Bounded UInt8, UInt16, UInt32, and UInt64 carriers store exact natural-number encodings. Callers choose a carrier and prove that the encoding fits both the format bound and the word's capacity.

The bounds are propositions erased from the runtime carrier. The packing functions and their round-trip laws are independent of the numerical format using them.

@[reducible, inline]

abbrev FloatLib.Numerics.StaticStorage.BoundedCode (α : Type u) (toNat : α → ℕ) (bound : ℕ) : Type u

A primitive carrier whose natural-number view lies below a format-specific bound.

@[reducible, inline]

abbrev FloatLib.Numerics.StaticStorage.ByteCode (bound : ℕ) : Type

An in-range encoding stored directly in UInt8.

@[reducible, inline]

abbrev FloatLib.Numerics.StaticStorage.Word16Code (bound : ℕ) : Type

An in-range encoding stored directly in UInt16.

@[reducible, inline]

abbrev FloatLib.Numerics.StaticStorage.Word32Code (bound : ℕ) : Type

An in-range encoding stored directly in UInt32.

@[reducible, inline]

abbrev FloatLib.Numerics.StaticStorage.Word64Code (bound : ℕ) : Type

An in-range encoding stored directly in UInt64.

theorem FloatLib.Numerics.StaticStorage.lt_capacity {bits bound width : ℕ} (hbits : bits < bound) (bound_le : bound ≤ 2 ^ width) : bits < 2 ^ width

An encoding below its format bound fits any storage width containing that bound.

@[inline]

def FloatLib.Numerics.StaticStorage.ByteCode.ofNat {bound : ℕ} (bits : ℕ) (hbound : bits < bound) (hcapacity : bits < 2 ^ 8) : ByteCode bound

Narrow an in-range encoding to a direct byte carrier.

@[simp]

theorem FloatLib.Numerics.StaticStorage.ByteCode.toNat_ofNat {bound bits : ℕ} (hbound : bits < bound) (hcapacity : bits < 2 ^ 8) : (ofNat bits hbound hcapacity).val.toNat = bits

Reading a byte immediately after packing returns the supplied encoding.

@[inline]

def FloatLib.Numerics.StaticStorage.Word16Code.ofNat {bound : ℕ} (bits : ℕ) (hbound : bits < bound) (hcapacity : bits < 2 ^ 16) : Word16Code bound

Narrow an in-range encoding to a direct 16-bit carrier.

@[simp]

theorem FloatLib.Numerics.StaticStorage.Word16Code.toNat_ofNat {bound bits : ℕ} (hbound : bits < bound) (hcapacity : bits < 2 ^ 16) : (ofNat bits hbound hcapacity).val.toNat = bits

Reading a 16-bit word immediately after packing returns the supplied encoding.

@[inline]

def FloatLib.Numerics.StaticStorage.Word32Code.ofNat {bound : ℕ} (bits : ℕ) (hbound : bits < bound) (hcapacity : bits < 2 ^ 32) : Word32Code bound

Narrow an in-range encoding to a direct 32-bit carrier.

@[simp]

theorem FloatLib.Numerics.StaticStorage.Word32Code.toNat_ofNat {bound bits : ℕ} (hbound : bits < bound) (hcapacity : bits < 2 ^ 32) : (ofNat bits hbound hcapacity).val.toNat = bits

Reading a 32-bit word immediately after packing returns the supplied encoding.

@[inline]

def FloatLib.Numerics.StaticStorage.Word64Code.ofNat {bound : ℕ} (bits : ℕ) (hbound : bits < bound) (hcapacity : bits < 2 ^ 64) : Word64Code bound

Narrow an in-range encoding to a direct 64-bit carrier.

@[simp]

theorem FloatLib.Numerics.StaticStorage.Word64Code.toNat_ofNat {bound bits : ℕ} (hbound : bits < bound) (hcapacity : bits < 2 ^ 64) : (ofNat bits hbound hcapacity).val.toNat = bits

Reading a 64-bit word immediately after packing returns the supplied encoding.