src/Manifest.bend source

src/Manifest.bend on the hub · documented module

import Base# Manifest (Task 5): which SSTables live at which level.# Format is positional (line i = level i, no level numbers to parse):#   <name>,<name>#   <name>#   #<checksum-decimal># Names are engine-generated (sst-<level>-<counter>.tbl) AND strictly# validated on parse ([A-Za-z0-9._-], not "." / ".."): T1 hostile bytes# must fail closed, never traverse directories (spec §8).# Checksum covers all content lines (fail-closed on corruption, like WAL).# Parsing leans on Base (split/join/starts_with/drop/read): precompiled,# trusted, zero proof burden — laws pin OUR format, not Base.type Manifest is Data:  M{levels: List<&2, List<&2, String>>}def mhash(s: String, h: U32) -> U32:  match s:    case SNil{}:      h    case SCon{c, t}:      mhash(t, U32.add(U32.mul(h, 31), Char.to_u32(c)))def encode_line(names: List<&2, String>) -> String:  String.join(names, ",")def encode_lines(xss: List<&2, List<&2, String>>) -> List<&2, String>:  match xss:    case Nil{}:      Nil{}    case Con{h, t}:      Con{encode_line(h), encode_lines(t)}def serialize(m: Manifest) -> String:  match m:    case M{levels}:      +ls = encode_lines(levels)      +content = String.join(ls, SCon{Char.from_u32(10), SNil{}})      String.join(List.append(&2, String, ls, Con{"#" ++ U32.show(mhash(content, 7)), Nil{}}), SCon{Char.from_u32(10), SNil{}})# --- Strict name validation (structural recursion + leaves; no fuel:# recursion is unconditional, decisions combine via leaves) ---def name_ok_step(ok: Bool, good: Bool) -> Bool:  match ok:    case True{}:      good    case False{}:      False{}def nc_alpha(a: Bool, c: Char) -> Bool:  match a:    case True{}:      True{}    case False{}:      Char.is_digit(c)def nc_us(u: Bool, +c: Char) -> Bool:  match u:    case True{}:      True{}    case False{}:      nc_alpha(Char.is_alpha(c), c)def nc_dot(d: Bool, +c: Char) -> Bool:  match d:    case True{}:      True{}    case False{}:      nc_us(Char.is_eq(c, Char.from_u32(95)), c)def nc_dash(d: Bool, +c: Char) -> Bool:  match d:    case True{}:      True{}    case False{}:      nc_dot(Char.is_eq(c, Char.from_u32(46)), c)def name_char_ok(+c: Char) -> Bool:  nc_dash(Char.is_eq(c, Char.from_u32(45)), c)def name_go(s: String, ok: Bool) -> Bool:  match s:    case SNil{}:      ok    case SCon{h, t}:      name_go(t, name_ok_step(ok, name_char_ok(h)))def name_dots2(d2: Bool, s: String) -> Bool:  match d2:    case True{}:      False{}    case False{}:      name_go(s, True{})def name_dots(d1: Bool, d2: Bool, s: String) -> Bool:  match d1:    case True{}:      False{}    case False{}:      name_dots2(d2, s)def name_ok(s: String) -> Bool:  match s:    case SNil{}:      False{}    case SCon{+h, +t}:      name_dots(String.eq(SCon{h, t}, "."), String.eq(SCon{h, t}, ".."), SCon{h, t})def names_and(a: Bool, b: Bool) -> Bool:  match a:    case True{}:      b    case False{}:      False{}def names_ok(xs: List<&2, String>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{h, t}:      names_and(name_ok(h), names_ok(t))# --- Parse: validate everything first (Bool), then parse unchecked# (total, structural, no Maybe in loops). Top dispatch is a leaf. ---def line_valid(line: String) -> Bool:  match line:    case SNil{}:      True{}    case SCon{h, t}:      names_ok(String.split(SCon{h, t}, Char.from_u32(44)))def body_valid(ls: List<&2, String>) -> Bool:  match ls:    case Nil{}:      True{}    case Con{h, t}:      names_and(line_valid(h), body_valid(t))def chk_rd(m: Maybe<&2, U32>, content: String) -> Bool:  match m:    case None{}:      False{}    case Some{v}:      U32.is_eq(v, mhash(content, 7))def chk_sw(sw: Bool, chk: String, content: String) -> Bool:  match sw:    case True{}:      chk_rd(U32.read(String.drop(chk, 1n)), content)    case False{}:      False{}def chk_valid(+chk: String, content: String) -> Bool:  chk_sw(String.starts_with(chk, "#"), chk, content)def valid_split(p: (List<&2, String> & String)) -> Bool:  match p:    case (+body, chk):      names_and(body_valid(body), chk_valid(chk, String.join(body, SCon{Char.from_u32(10), SNil{}})))def split_last(ls: List<&2, String>, acc: List<&2, String>) -> (List<&2, String> & String):  match ls:    case Nil{}:      (List.reverse(&2, String, acc), "")    case Con{h, Nil{}}:      (List.reverse(&2, String, acc), h)    case Con{h, Con{k, t}}:      split_last(Con{k, t}, Con{h, acc})def valid_lines(lines: List<&2, String>) -> Bool:  valid_split(split_last(lines, Nil{}))def valid_manifest(s: String) -> Bool:  valid_lines(String.split(s, Char.from_u32(10)))def parse_line_u(line: String) -> List<&2, String>:  match line:    case SNil{}:      Nil{}    case SCon{h, t}:      String.split(SCon{h, t}, Char.from_u32(44))def parse_levels_u(ls: List<&2, String>, acc: List<&2, List<&2, String>>) -> List<&2, List<&2, String>>:  match ls:    case Nil{}:      List.reverse(&2, List<&2, String>, acc)    case Con{h, t}:      parse_levels_u(t, Con{parse_line_u(h), acc})def parse_unchecked(p: (List<&2, String> & String)) -> Manifest:  match p:    case (body, chk):      M{parse_levels_u(body, Nil{})}def parse_dispatch(ok: Bool, s: String) -> Maybe<&2, Manifest>:  match ok:    case True{}:      Some{parse_unchecked(split_last(String.split(s, Char.from_u32(10)), Nil{}))}    case False{}:      None{}def parse(+s: String) -> Maybe<&2, Manifest>:  parse_dispatch(valid_manifest(s), s)# Total-parser witness used by the hardening law.def is_decided(+m: Maybe<&2, Manifest>) -> Bool:  True{}