BendtorchLoad.St.length: def of bendtorch-load@1.3.0.0
Import: import bendtorch-load@1.3.0.0/main.bend as BendtorchLoad
Lines 550-558 of bendtorch-load@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-load@1.3.0.0/main.bend&start_line=550&end_line=558

import Base

# the format caps the header at 100 MB
def St.length(f: File, +path: String, h: Maybe<&2, W64>) -> IO(Header):
  match h:
    case None{}: IO.die(Header, 1, path ++ ": shorter than a safetensors header")
    case Some{W64{hi, +lo}}:
      do IO<Header>:
        require(Bool.and(U32.is_zero(hi), U32.is_le(lo, 100000000)), path ++ ": a safetensors header past 100 MB")
        r : File & Result<&1, &1, U32 & String, List<&2, U32>> <- File.read_at(f, 8, lo)
        St.header(path, lo, r)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=File.read_at
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.die
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_zero
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Header
  https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.header
  https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64
  https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=require