TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.ExecFloat.Backends.TinyTable.Generic.Indexing

Native indexing for exhaustive byte tables #

The index proof shows that row-major USize arithmetic neither wraps nor leaves a generated table. The only size bound is encoding.radix ≤ 256; the radix need not be a power of two or come from a floating-point layout.

The executable formulas remain direct native arithmetic and all bounds erase after compilation. Table lookup therefore has no runtime certificate check, while generation and dispatch can rely on the proved index envelope.

source
@[inline]
def FloatLib.Floats.ExecFloat.Backend.TinyTable.binaryByteIndex (radix : USize) (left right : UInt8) :
USize

Native row-major index for two byte-backed operands.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Backend.TinyTable.unaryByteIndex (value : UInt8) :
    USize

    Native index for a unary byte table.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Backend.TinyTable.ternaryByteIndex (radix : USize) (left right addend : UInt8) :
      USize

      Native row-major index for three byte-backed operands.

      Instances For
        source
        theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.binaryByteIndex_toNat (radix : USize) (left right : UInt8) (hindex : left.toNat * radix.toNat + right.toNat < 2 ^ System.Platform.numBits) :
        (binaryByteIndex radix left right).toNat = left.toNat * radix.toNat + right.toNat

        A non-wrapping native binary index agrees with its natural-number expression.

        source
        @[simp]
        theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.unaryByteIndex_toNat (value : UInt8) :
        (unaryByteIndex value).toNat = value.toNat

        The native unary-table index preserves the byte's natural value.

        source
        theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.ternaryByteIndex_toNat (radix : USize) (left right addend : UInt8) (hleftMul : left.toNat * radix.toNat < 2 ^ System.Platform.numBits) (hpair : left.toNat * radix.toNat + right.toNat < 2 ^ System.Platform.numBits) (hpairMul : (left.toNat * radix.toNat + right.toNat) * radix.toNat < 2 ^ System.Platform.numBits) (hindex : (left.toNat * radix.toNat + right.toNat) * radix.toNat + addend.toNat < 2 ^ System.Platform.numBits) :
        (ternaryByteIndex radix left right addend).toNat = (left.toNat * radix.toNat + right.toNat) * radix.toNat + addend.toNat

        A non-wrapping native ternary index agrees with its natural-number expression.

        source
        theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.binaryIndex_noOverflow {Model : Type u} (encoding : Encoding Model) (radixWord : USize) (hradixWord : radixWord.toNat = encoding.radix) (left right : Code encoding) :
        left.val.toNat * radixWord.toNat + right.val.toNat < 2 ^ System.Platform.numBits

        Every two-input byte-table index fits both supported platform word widths.

        source
        theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.ternaryIndex_noOverflow {Model : Type u} (encoding : Encoding Model) (radixWord : USize) (hradixWord : radixWord.toNat = encoding.radix) (left right addend : Code encoding) :
        left.val.toNat * radixWord.toNat < 2 ^ System.Platform.numBits ∧ left.val.toNat * radixWord.toNat + right.val.toNat < 2 ^ System.Platform.numBits ∧ (left.val.toNat * radixWord.toNat + right.val.toNat) * radixWord.toNat < 2 ^ System.Platform.numBits ∧ (left.val.toNat * radixWord.toNat + right.val.toNat) * radixWord.toNat + addend.val.toNat < 2 ^ System.Platform.numBits

        Every intermediate of a three-input byte-table index fits a platform word.

        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Backend.TinyTable.radixWord {Model : Type u} (encoding : Encoding Model) :
        USize

        Native-word representation of an at-most-256-code encoding's radix.

        Instances For
          source
          @[simp]
          theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.radixWord_toNat {Model : Type u} (encoding : Encoding Model) :
          (radixWord encoding).toNat = encoding.radix

          The native radix constant denotes the mathematical encoding radix.

          source
          theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.binaryIndex_lt {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model) (left right : Code encoding) :
          (binaryByteIndex (radixWord encoding) left.val right.val).toNat < (binaryTotal encoding op).size

          Valid input bytes select an in-bounds binary table entry.

          source
          theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.unaryIndex_lt {Model : Type u} (encoding : Encoding Model) (op : Model → Model) (value : Code encoding) :
          (unaryByteIndex value.val).toNat < (unaryTotal encoding op).size

          Valid input bytes select an in-bounds unary table entry.

          source
          theorem FloatLib.Floats.ExecFloat.Backend.TinyTable.ternaryIndex_lt {Model : Type u} (encoding : Encoding Model) (op : Model → Model → Model → Model) (left right addend : Code encoding) :
          (ternaryByteIndex (radixWord encoding) left.val right.val addend.val).toNat < (ternaryTotal encoding op).size

          Valid input bytes select an in-bounds ternary table entry.