Documentation

LeanMlir.LEBytes

Little-endian packing for the FFI buffers #

Every buffer the runtimes read — shape descriptors, labels, token ids, anchor priors, f32 tensors — is little-endian. These are the writers and the readers (F32.readLabel is readU32LE at record granularity). Import-free, so the pure-data ParamLayouts can use them.

source
@[inline]
def pushU32LE (acc : ByteArray) (v : Nat) :
ByteArray

Append v mod 2³² as 4 little-endian bytes (an int32 / uint32 record).

Equations
Instances For
    source
    @[inline]
    def pushU64LE (acc : ByteArray) (v : Nat) :
    ByteArray

    Append v mod 2⁶⁴ as 8 little-endian bytes (a uint64 record).

    Equations
    Instances For
      source
      @[inline]
      def pushF32LE (acc : ByteArray) (x : Float) :
      ByteArray

      Append x as 4 little-endian f32 bytes (narrowing f64 → Float32).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[inline]
        def pushF64LE (acc : ByteArray) (x : Float) :
        ByteArray

        Append x as 8 little-endian f64 bytes.

        Equations
        Instances For
          source
          @[inline]
          def readU32LE (ba : ByteArray) (off : Nat) :
          Nat

          The little-endian uint32 at BYTE offset off.

          Equations
          Instances For
            source
            @[inline]
            def readU64LE (ba : ByteArray) (off : Nat) :
            Nat

            The little-endian uint64 at BYTE offset off.

            Equations
            Instances For