bendtorch-load Releases (6): 1.3.0.0 0x740c8b0b33caef82367f13ef8a1ef41a indexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.3.0.0 1.2.0.0 0xa6af449466db11bf10f3a82bbeddb622 unindexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.2.0.0 1.1.1.0 0x0b2d574934489d8cf85589b273567833 unindexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.1.1.0 1.1.0.0 0x4922dce2dd59be0648ebd8f3643975ae unindexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.1.0.0 1.0.1.0 0xd81dbae31742e38f426cc4b4700c9e51 unindexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.0.1.0 1.0.0.0 0xf25754162a4d6294dc96b9870e0997fa unindexed https://jend.leeeet.dev/files.txt?path=bendtorch-load@1.0.0.0 Definitions (96): BendtorchLoad.require (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=require) def require(ok: Bool, +message: String) -> IO(Unit): BendtorchLoad.W64 (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64) type W64 is Data: W64{hi: U32, lo: U32} BendtorchLoad.W64.of (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.of) def W64.of(x: U32) -> W64: BendtorchLoad.W64.of_pair (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.of_pair) def W64.of_pair(p: U32 & U32) -> W64: BendtorchLoad.W64.bit (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.bit) def W64.bit(b: Bool) -> U32: BendtorchLoad.W64.eq (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.eq) def W64.eq(a: W64, b: W64) -> Bool: BendtorchLoad.W64.add_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.add_go) def W64.add_go(+ah: U32, +bh: U32, +s: U32, +al: U32) -> W64: BendtorchLoad.W64.add (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.add) # a + b, wrapping at 2^64: the low words' sum carries one when it wrapped (it is then below either term) def W64.add(a: W64, b: W64) -> W64: BendtorchLoad.W64.mul_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.mul_go) def W64.mul_go(+h: U32, +k: U32, +p0: U32, +p1: U32) -> W64: BendtorchLoad.W64.mul_small (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.mul_small) # a * k for k < 2^16 (enough for bytes a number and decimal digits), wrapping at 2^64: lo = l1 2^16 + l0, so # lo * k = (l1 k) 2^16 + l0 k, where both products fit a U32 def W64.mul_small(a: W64, +k: U32) -> W64: BendtorchLoad.W64.div10_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.div10_go) def W64.div10_go(+qh: U32, +r1: U32, +q1: U32, +l: U32) -> W64 & U32: BendtorchLoad.W64.div10 (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.div10) # (a / 10, a % 10), by long division in 16-bit steps so no partial remainder overflows a U32 def W64.div10(a: W64) -> W64 & U32: BendtorchLoad.W64.is_zero (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.is_zero) def W64.is_zero(a: W64) -> Bool: BendtorchLoad.W64.show_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.show_go) def W64.show_go(f: Nat, z: Bool, qr: W64 & U32, acc: String) -> String: BendtorchLoad.W64.show_if (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.show_if) def W64.show_if(z: Bool, +a: W64) -> String: BendtorchLoad.W64.show (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.show) # the decimal digits, as U32.show writes them def W64.show(+a: W64) -> String: BendtorchLoad.W64.digits (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.digits) def W64.digits(s: String, f: Nat) -> Bool: BendtorchLoad.W64.read_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.read_go) def W64.read_go(s: String, +acc: W64) -> W64: BendtorchLoad.W64.read_if (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.read_if) def W64.read_if(ok: Bool, s: String) -> Maybe<&2, W64>: BendtorchLoad.W64.read (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=W64.read) # A decimal number of 1 to 19 digits (every such number fits 64 bits); anything else is None def W64.read(s: String) -> Maybe<&2, W64>: BendtorchLoad.read_done (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read_done) def read_done(+path: String, +n: U32, r: File & (Array & Result<&1, &1, U32 & String, U32>)) -> IO(Array): BendtorchLoad.read_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read_go) def read_go(+path: String, +n: U32, f: File, +size: W64) -> IO(Array): BendtorchLoad.read_sized (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read_sized) def read_sized(+path: String, +n: U32, r: File & Result<&1, &1, U32 & String, U32 & U32>) -> IO(Array): BendtorchLoad.read (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read) # A raw, exact-size little-endian F32 file, read once into one source array: up to 2^32 - 1 numbers (16 GiB). def read(+path: String, +n: U32) -> IO(Array): BendtorchLoad.read_f32_at (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read_f32_at) # n little-endian F32 numbers at byte `off` of a file of any size (a tensor inside a larger file) def read_f32_at(+path: String, off: W64, +n: U32) -> IO(Array): BendtorchLoad.read_bf16_at (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=read_bf16_at) # n little-endian BF16 numbers at byte `off` of a file of any size, each widened exactly to F32 (bf16.to(torch.float32)) def read_bf16_at(+path: String, off: W64, +n: U32) -> IO(Array): BendtorchLoad.size_done (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=size_done) def size_done(r: File & Result<&1, &1, U32 & String, U32 & U32>) -> IO(W64): BendtorchLoad.size (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=size) # A file's size in bytes, at any size def size(+path: String) -> IO(W64): BendtorchLoad.weights_done (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=weights_done) def weights_done(-P: Type, +n: U32, r: T.PA

) -> IO(P): BendtorchLoad.weights (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=weights) # All parameters in Layer.dump order. The source array is released after the model's arrays are filled. def weights(~P: Type, ~X: Type, ~Y: Type, ~S: Type, ~m: T.Layer, +path: String, p: P) -> IO(P): BendtorchLoad.train_read (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=train_read) # The checkpoint layout is determined by the already initialized optimizer state, without a header: # SGD: parameters; momentum: parameters, buffer; Adam/AdamW: parameters, m, v, 1 - b1^t, 1 - b2^t; AdamW with packed # BF16 moments: parameters, the moments' tree (main.bend's pt_store), 1 - b1^t, 1 - b2^t, the whole file read. def train_read(~P: Type, ~X: Type, ~Y: Type, ~S: Type, ~m: T.Layer, +path: String, +base: U32, +copies: U32, +tail: U32, tr: T.Train

) -> IO(T.Train

): BendtorchLoad.cells_done (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=cells_done) def cells_done(r: File & Result<&1, &1, U32 & String, U32>) -> IO(U32): BendtorchLoad.cells_of (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=cells_of) # the number of F32 cells in a file (a packed-moment checkpoint carries its own sizes: its length is the file's) def cells_of(+path: String) -> IO(U32): BendtorchLoad.train (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=train) def train(~P: Type, ~X: Type, ~Y: Type, ~S: Type, ~m: T.Layer, +path: String, tr: T.Train

) -> IO(T.Train

): BendtorchLoad.Entry (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Entry) # one tensor the model expects, in Layer.dump order: its name in the file and its shape (rows, columns, ...) type Entry is Data: Entry{name: String, shape: List<&2, U32>} BendtorchLoad.St.entry_name (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.entry_name) def St.entry_name(e: Entry) -> String: BendtorchLoad.Tok (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Tok) type Tok is Data: TStr{s: String} TNum{v: W64} TPun{c: U32} TBad{c: U32} BendtorchLoad.Lex (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Lex) # the lexer's state between bytes: outside a token, inside a string (its characters reversed), just after a backslash # in a string, inside a number type Lex is Data: LOut{} LStr{acc: String} LEsc{acc: String} LNum{v: W64} BendtorchLoad.LexR (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=LexR) # a state and the tokens one byte completed, in order type LexR is Data: LexR{st: Lex, toks: List<&2, Tok>} BendtorchLoad.St.digit (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.digit) def St.digit(+b: U32) -> Bool: BendtorchLoad.St.space (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.space) def St.space(+b: U32) -> Bool: BendtorchLoad.St.pun (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.pun) # { } [ ] : , def St.pun(+b: U32) -> Bool: BendtorchLoad.St.out_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.out_go) def St.out_go(quote: Bool, digit: Bool, space: Bool, pun: Bool, +b: U32) -> LexR: BendtorchLoad.St.out (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.out) def St.out(+b: U32) -> LexR: BendtorchLoad.St.str_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.str_go) def St.str_go(quote: Bool, slash: Bool, +b: U32, acc: String) -> LexR: BendtorchLoad.St.num_end (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.num_end) # a number ends at the first byte that is not a digit, and that byte is then read as outside a token def St.num_end(+v: W64, r: LexR) -> LexR: BendtorchLoad.St.num_go (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.num_go) def St.num_go(digit: Bool, +b: U32, +v: W64) -> LexR: BendtorchLoad.St.step (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.step) def St.step(st: Lex, +b: U32) -> LexR: BendtorchLoad.St.push (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.push) # ts onto out, which holds the tokens so far in reverse def St.push(ts: List<&2, Tok>, out: List<&2, Tok>) -> List<&2, Tok>: BendtorchLoad.St.fin (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.fin) # the end of the header: a number ends there, an unfinished string is malformed def St.fin(st: Lex, out: List<&2, Tok>) -> List<&2, Tok>: BendtorchLoad.St.lex (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.lex) # the header's tokens, in order; r is what the previous byte left def St.lex(bs: List<&2, U32>, r: LexR, out: List<&2, Tok>) -> List<&2, Tok>: BendtorchLoad.Rec (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Rec) # one top-level entry of the header: a tensor (or __metadata__, which no layout names) type Rec is Data: Rec{name: String, dtype: String, shape: List<&2, W64>, offs: List<&2, W64>} BendtorchLoad.Ps (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Ps) # the pass over the tokens: the depth ({ and [ open a level), whether the last token was a colon, the last string, # the current entry's name and field, what the entry holds so far, the numbers of the open list, the entries read # (last first), and the count of tokens the header may not hold type Ps is Data: Ps{depth: U32, colon: Bool, pend: String, name: String, field: String, dtype: String, shape: List<&2, W64>, offs: List<&2, W64>, nums: List<&2, W64>, recs: List<&2, Rec>, bad: U32} BendtorchLoad.Sp.str (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.str) # a string is a value after a colon (the dtype, at depth 2) or else a key, kept until its colon def Sp.str(colon: Bool, is_dt: Bool, ps: Ps, s: String) -> Ps: BendtorchLoad.Sp.colon (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.colon) # a colon makes the last string the entry's name (depth 1) or the field's (depth 2) def Sp.colon(d1: Bool, d2: Bool, ps: Ps) -> Ps: BendtorchLoad.Sp.open (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.open) # { opens a level; at depth 2 an entry starts empty def Sp.open(fresh: Bool, ps: Ps) -> Ps: BendtorchLoad.Sp.close (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.close) # } closes a level; closing depth 2 ends an entry def Sp.close(emit: Bool, ps: Ps) -> Ps: BendtorchLoad.Sp.lopen (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.lopen) def Sp.lopen(ps: Ps) -> Ps: BendtorchLoad.Sp.lclose (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.lclose) # ] closes a list; at depth 3 it is the entry's shape or data_offsets def Sp.lclose(is_sh: Bool, is_of: Bool, ps: Ps) -> Ps: BendtorchLoad.Sp.comma (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.comma) def Sp.comma(ps: Ps) -> Ps: BendtorchLoad.Sp.num (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.num) # a number counts inside a list at depth 3; elsewhere it is not part of a tensor's entry def Sp.num(in_list: Bool, v: W64, ps: Ps) -> Ps: BendtorchLoad.Sp.pun (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.pun) def Sp.pun(colon: Bool, ob: Bool, cb: Bool, ol: Bool, cl: Bool, +d: U32, +f: String, ps: Ps) -> Ps: BendtorchLoad.Sp.step (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.step) def Sp.step(t: Tok, ps: Ps) -> Ps: BendtorchLoad.Sp.parse (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Sp.parse) def Sp.parse(ts: List<&2, Tok>, ps: Ps) -> Ps: BendtorchLoad.St.rec_name (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.rec_name) def St.rec_name(r: Rec) -> String: BendtorchLoad.St.find_put (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.find_put) def St.find_put(r: Rec, rest: Maybe<&2, Rec>, hit: Bool) -> Maybe<&2, Rec>: BendtorchLoad.St.find (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.find) # the entry named `name` def St.find(rs: List<&2, Rec>, +name: String) -> Maybe<&2, Rec>: BendtorchLoad.St.prod (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.prod) def St.prod(xs: List<&2, U32>) -> U32: BendtorchLoad.St.total (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.total) def St.total(es: List<&2, Entry>) -> U32: BendtorchLoad.St.shape_eq (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.shape_eq) def St.shape_eq(a: List<&2, W64>, b: List<&2, U32>) -> Bool: BendtorchLoad.St.show_u (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.show_u) def St.show_u(xs: List<&2, U32>, sep: String) -> String: BendtorchLoad.St.show_w (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.show_w) def St.show_w(xs: List<&2, W64>, sep: String) -> String: BendtorchLoad.Plan (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Plan) # where a tensor is and how to read it, or why it cannot be read type Plan is Data: PlanOk{name: String, bf16: Bool, off: W64, n: U32} PlanBad{msg: String} BendtorchLoad.St.plan_span (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.plan_span) def St.plan_span(ok: Bool, +name: String, bf16: Bool, off: W64, +n: U32) -> Plan: BendtorchLoad.St.plan_of (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.plan_of) # data_offsets must be [begin, end] with end - begin the tensor's bytes def St.plan_of(+name: String, bf16: Bool, +start: W64, +n: U32, +width: U32, of: List<&2, W64>) -> Plan: BendtorchLoad.St.plan_shape (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.plan_shape) def St.plan_shape(ok: Bool, +name: String, f32: Bool, +start: W64, +sh: List<&2, W64>, +want: List<&2, U32>, of: List<&2, W64>) -> Plan: BendtorchLoad.St.plan_dtype (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.plan_dtype) def St.plan_dtype(f32: Bool, bf16: Bool, +name: String, +dt: String, +start: W64, +sh: List<&2, W64>, +want: List<&2, U32>, of: List<&2, W64>) -> Plan: BendtorchLoad.St.plan (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.plan) def St.plan(+start: W64, e: Entry, mr: Maybe<&2, Rec>) -> Plan: BendtorchLoad.St.read (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.read) def St.read(bf16: Bool, f: File, off: W64, +n: U32, a: Array, +at: U32) -> IO(File & (Array & Result<&1, &1, U32 & String, U32>)): BendtorchLoad.St.got (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.got) def St.got(+path: String, +name: String, +n: U32, r: File & (Array & Result<&1, &1, U32 & String, U32>), k: File -> Array -> U32 -> IO(Array)) -> IO(Array): BendtorchLoad.St.then (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.then) # reads one planned tensor into cells at .., then goes on with k def St.then(+path: String, p: Plan, f: File, a: Array, +at: U32, k: File -> Array -> U32 -> IO(Array)) -> IO(Array): BendtorchLoad.St.fill (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.fill) # every tensor of es, in order, into consecutive cells from at def St.fill(es: List<&2, Entry>, +path: String, +start: W64, +recs: List<&2, Rec>, f: File, a: Array, +at: U32) -> IO(Array): BendtorchLoad.St.le32 (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.le32) def St.le32(+a: U32, +b: U32, +c: U32, +d: U32) -> U32: BendtorchLoad.St.le64 (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.le64) # the header's length: the file's first 8 bytes, little-endian def St.le64(bs: List<&2, U32>) -> Maybe<&2, W64>: BendtorchLoad.St.count (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.count) def St.count(bs: List<&2, U32>, +acc: U32) -> U32: BendtorchLoad.Header (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=Header) # A parsed safetensors header: where the data starts and each tensor's record. Reading it once lets a model be filled # one piece at a time (`piece`), so that no array of the whole model exists. One array for all of SmolLM2-1.7B's # 1.71e9 parameters takes a 2^31-cell block (8 GiB) whose memory the training step's smaller blocks never reuse. type Header is Data: Header{start: W64, recs: List<&2, Rec>} BendtorchLoad.St.parsed (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.parsed) def St.parsed(+path: String, +start: W64, ps: Ps) -> IO(Header): BendtorchLoad.St.header (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.header) def St.header(+path: String, +len: U32, r: File & Result<&1, &1, U32 & String, List<&2, U32>>) -> IO(Header): BendtorchLoad.St.length (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.length) # the format caps the header at 100 MB def St.length(f: File, +path: String, h: Maybe<&2, W64>) -> IO(Header): BendtorchLoad.St.first8 (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=St.first8) def St.first8(+path: String, r: File & Result<&1, &1, U32 & String, List<&2, U32>>) -> IO(Header): BendtorchLoad.header (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=header) # A safetensors file's header, parsed; the file is closed after it def header(+path: String) -> IO(Header): BendtorchLoad.tensors_from (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=tensors_from) # The tensors `layout` names, read from the file whose header is h, in the layout's order, into one array of n numbers def tensors_from(+path: String, h: Header, +n: U32, +layout: List<&2, Entry>) -> IO(Array): BendtorchLoad.tensors (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=tensors) # The tensors `layout` names, read from a safetensors file in its order into one array of n numbers (F32 as they are, # BF16 widened exactly). Each must be in the file with the shape given, as F32 or BF16, and the shapes must hold n # numbers in all; otherwise the program stops with a message naming the tensor. Other tensors in the file are ignored. def tensors(+path: String, +n: U32, +layout: List<&2, Entry>) -> IO(Array): BendtorchLoad.piece (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=piece) # One layer's parameters from the file whose header is h: `layout` names its tensors in Layer.dump order, and # Layer.load fills them; the array they were read into is gone once this answers def piece(~P: Type, ~X: Type, ~Y: Type, ~S: Type, ~m: T.Layer, +path: String, h: Header, +layout: List<&2, Entry>, p: P) -> IO(P): BendtorchLoad.two (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=two) # A pair of parameters filled one after the other: the first piece's source array is released before the second is read def two(-P1: Type, -P2: Type, p: T.Two, k1: P1 -> IO(P1), k2: P2 -> IO(P2)) -> IO(T.Two): BendtorchLoad.safetensors (https://jend.leeeet.dev/definition.txt?path=bendtorch-load@1.3.0.0/main.bend&name=safetensors) # All parameters from a safetensors file: `layout` names the model's tensors in Layer.dump order (a tied output head # is not in it, as SmolLM2's is not in its file), and Layer.load fills the parameters from them as `weights` does def safetensors(~P: Type, ~X: Type, ~Y: Type, ~S: Type, ~m: T.Layer, +path: String, +layout: List<&2, Entry>, p: P) -> IO(P):