src/RecoverPure.bend source

src/RecoverPure.bend on the hub · documented module

import Baseimport ./MemTable.bend as MemTableimport ./Manifest.bend as Manifestimport ./Sstable.bend as Sstable# --- Flush-counter restore (pure) ---# Handle mid and in the pure recovery decisions.def mid_and(lhs: Bool, rhs: Bool) -> Bool:  match lhs:    case True{}:      rhs    case False{}:      False{}# Handle shape mid in the pure recovery decisions.def shape_mid(first: Bool, second: Bool, third: Bool) -> Bool:  mid_and(first, mid_and(second, third))# Table generations are compact decimal only. Unparsable middles are invalid# (no unary-dash legacy reads: no retrocompat).def gen_valid_read(parsed: Maybe<&2, Nat>) -> Bool:  match parsed:    case Some{n}:      True{}    case None{}:      False{}# Handle gen valid in the pure recovery decisions.def gen_valid(+middle: String) -> Bool:  gen_valid_read(Nat.read(middle))# Handle ov ok in the pure recovery decisions.def ov_ok(+big: Bool, +name: String, +ln: Nat) -> Bool:  match big:    case True{}:      shape_mid(String.starts_with(name, "l"), String.ends_with(name, ".tbl"), gen_valid(String.take(String.drop(name, 3n), Nat.sub(ln, 7n))))    case False{}:      False{}# Handle name shape in the pure recovery decisions.def name_shape(+name: String) -> Bool:  +ln = String.length(name)  ov_ok(Nat.is_le(7n, ln), name, ln)# Return the level name ok for the pure recovery decisions.def level_name_ok(+big: Bool, +name: String, +ln: Nat, +prefix: String, +prefix_len: Nat) -> Bool:  match big:    case False{}:      False{}    case True{}:      shape_mid(String.starts_with(name, prefix), String.ends_with(name, ".tbl"), gen_valid(String.take(String.drop(name, prefix_len), Nat.sub(ln, Nat.add(prefix_len, 4n)))))# Handle name shape level in the pure recovery decisions.def name_shape_level(+name: String, +level: Nat) -> Bool:  +prefix = "l" ++ Nat.show(level) ++ "-"  +prefix_len = String.length(prefix)  +ln = String.length(name)  level_name_ok(Nat.is_le(Nat.add(prefix_len, 4n), ln), name, ln, prefix, prefix_len)# Handle gen value read in the pure recovery decisions.def gen_value_read(parsed: Maybe<&2, Nat>) -> Nat:  match parsed:    case Some{n}:      n    case None{}:      0n# Handle gen value in the pure recovery decisions.def gen_value(+middle: String) -> Nat:  gen_value_read(Nat.read(middle))# Handle name gen in the pure recovery decisions.def name_gen(+name: String) -> Nat:  +ln = String.length(name)  gen_value(String.take(String.drop(name, 3n), Nat.sub(ln, 7n)))# Handle names ok in the pure recovery decisions.def names_ok(xs: List<&2, String>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{h, t}:      mid_and(name_shape(h), names_ok(t))# Return the level names ok for the pure recovery decisions.def level_names_ok(+level: Nat, xs: List<&2, String>) -> Bool:  match xs:    case Nil{}:      True{}    case Con{h, t}:      mid_and(name_shape_level(h, level), level_names_ok(level, t))# Handle manifest names ok in the pure recovery decisions.def manifest_names_ok(levels: List<&2, List<&2, String>>, +level: Nat) -> Bool:  match levels:    case Nil{}:      True{}    case Con{names, rest}:      mid_and(level_names_ok(level, names), manifest_names_ok(rest, Nat.add(level, 1n)))# Handle names all in the pure recovery decisions.def names_all(lvls: List<&2, List<&2, String>>) -> List<&2, String>:  match lvls:    case Nil{}:      Nil{}    case Con{h, t}:      List.append(&2, String, h, names_all(t))# Handle cmax in the pure recovery decisions.def cmax(names: List<&2, String>, +cur: Nat) -> Nat:  match names:    case Nil{}:      cur    case Con{h, t}:      cmax(t, Nat.max(name_gen(h), cur))# Count gen in the pure recovery decisions.def count_gen(+lvls: List<&2, List<&2, String>>) -> Nat:  Nat.add(cmax(names_all(lvls), 0n), 1n)# Handle mfst lists in the pure recovery decisions.def mfst_lists(+mfst: Manifest.Manifest) -> List<&2, List<&2, String>>:  match mfst:    case Manifest.M{lvs}:      lvs# L0 may overlap by design. Every table within each level below L0 must have# a range disjoint from every peer; metadata makes this check independent of# SortedRun and avoids reparsing entries during recovery.def disjoint_with_table(+tbl: Sstable.Table, rest: List<&2, Sstable.Table>) -> Bool:  match rest:    case Nil{}:      True{}    case Con{+h, t}:      mid_and(Sstable.ranges_disjoint(tbl, h), disjoint_with_table(tbl, t))# Return the level pairwise disjoint for the pure recovery decisions.def level_pairwise_disjoint(tables: List<&2, Sstable.Table>) -> Bool:  match tables:    case Nil{}:      True{}    case Con{+h, +t}:      mid_and(disjoint_with_table(h, t), level_pairwise_disjoint(t))# Check lower-level levels disjoint for the pure recovery decisions.def lower_levels_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:  match levels:    case Nil{}:      True{}    case Con{+level, rest}:      mid_and(level_pairwise_disjoint(level), lower_levels_disjoint(rest))# Handle l1 plus disjoint in the pure recovery decisions.def l1_plus_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:  match levels:    case Nil{}:      True{}    case Con{l0, lower}:      lower_levels_disjoint(lower)# Handle needs flush cap in the pure recovery decisions.def needs_flush_cap(+mem: MemTable.MemTable, +cap: Nat) -> Bool:  Nat.is_lt(cap, MemTable.count(mem))