src/RecoverPure.bend
mylsm-lsm-store@0.5.0.0 · 165 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.5.0.0/src/MemTable.bend as MemTable
3import mylsm-lsm-store@0.5.0.0/src/Manifest.bend as Manifest
4import mylsm-lsm-store@0.5.0.0/src/Sstable.bend as Sstable
5
6# --- Flush-counter restore (pure) ---
7
8# Handle mid and in the pure recovery decisions.
9def mid_and(lhs: Bool, rhs: Bool) -> Bool:
10 match lhs:
11 case True{}:
12 rhs
13 case False{}:
14 False{}
15
16# Handle shape mid in the pure recovery decisions.
17def shape_mid(first: Bool, second: Bool, third: Bool) -> Bool:
18 mid_and(first, mid_and(second, third))
19
20# Table generations are compact decimal only. Unparsable middles are invalid
21# (no unary-dash legacy reads: no retrocompat).
22def gen_valid_read(parsed: Maybe<&2, Nat>) -> Bool:
23 match parsed:
24 case Some{n}:
25 True{}
26 case None{}:
27 False{}
28
29# Handle gen valid in the pure recovery decisions.
30def gen_valid(+middle: String) -> Bool:
31 gen_valid_read(Nat.read(middle))
32
33# Handle ov ok in the pure recovery decisions.
34def ov_ok(+big: Bool, +name: String, +ln: Nat) -> Bool:
35 match big:
36 case True{}:
37 shape_mid(String.starts_with(name, "l"), String.ends_with(name, ".tbl"), gen_valid(String.take(String.drop(name, 3n), Nat.sub(ln, 7n))))
38 case False{}:
39 False{}
40
41# Handle name shape in the pure recovery decisions.
42def name_shape(+name: String) -> Bool:
43 +ln = String.length(name)
44 ov_ok(Nat.is_le(7n, ln), name, ln)
45
46# Return the level name ok for the pure recovery decisions.
47def level_name_ok(+big: Bool, +name: String, +ln: Nat, +prefix: String, +prefix_len: Nat) -> Bool:
48 match big:
49 case False{}:
50 False{}
51 case True{}:
52 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)))))
53
54# Handle name shape level in the pure recovery decisions.
55def name_shape_level(+name: String, +level: Nat) -> Bool:
56 +prefix = "l" ++ Nat.show(level) ++ "-"
57 +prefix_len = String.length(prefix)
58 +ln = String.length(name)
59 level_name_ok(Nat.is_le(Nat.add(prefix_len, 4n), ln), name, ln, prefix, prefix_len)
60
61# Handle gen value read in the pure recovery decisions.
62def gen_value_read(parsed: Maybe<&2, Nat>) -> Nat:
63 match parsed:
64 case Some{n}:
65 n
66 case None{}:
67 0n
68
69# Handle gen value in the pure recovery decisions.
70def gen_value(+middle: String) -> Nat:
71 gen_value_read(Nat.read(middle))
72
73# Handle name gen in the pure recovery decisions.
74def name_gen(+name: String) -> Nat:
75 +ln = String.length(name)
76 gen_value(String.take(String.drop(name, 3n), Nat.sub(ln, 7n)))
77
78# Handle names ok in the pure recovery decisions.
79def names_ok(xs: List<&2, String>) -> Bool:
80 match xs:
81 case Nil{}:
82 True{}
83 case Con{h, t}:
84 mid_and(name_shape(h), names_ok(t))
85
86# Return the level names ok for the pure recovery decisions.
87def level_names_ok(+level: Nat, xs: List<&2, String>) -> Bool:
88 match xs:
89 case Nil{}:
90 True{}
91 case Con{h, t}:
92 mid_and(name_shape_level(h, level), level_names_ok(level, t))
93
94# Handle manifest names ok in the pure recovery decisions.
95def manifest_names_ok(levels: List<&2, List<&2, String>>, +level: Nat) -> Bool:
96 match levels:
97 case Nil{}:
98 True{}
99 case Con{names, rest}:
100 mid_and(Nat.is_le(level, 3n),
101 mid_and(level_names_ok(level, names), manifest_names_ok(rest, Nat.add(level, 1n))))
102
103# Handle names all in the pure recovery decisions.
104def names_all(lvls: List<&2, List<&2, String>>) -> List<&2, String>:
105 match lvls:
106 case Nil{}:
107 Nil{}
108 case Con{h, t}:
109 List.append(&2, String, h, names_all(t))
110
111# Handle cmax in the pure recovery decisions.
112def cmax(names: List<&2, String>, +cur: Nat) -> Nat:
113 match names:
114 case Nil{}:
115 cur
116 case Con{h, t}:
117 cmax(t, Nat.max(name_gen(h), cur))
118
119# Count gen in the pure recovery decisions.
120def count_gen(+lvls: List<&2, List<&2, String>>) -> Nat:
121 Nat.add(cmax(names_all(lvls), 0n), 1n)
122
123# Handle mfst lists in the pure recovery decisions.
124def mfst_lists(+mfst: Manifest.Manifest) -> List<&2, List<&2, String>>:
125 match mfst:
126 case Manifest.M{lvs}:
127 lvs
128
129# L0 may overlap by design. Every table within each level below L0 must have
130# a range disjoint from every peer; metadata makes this check independent of
131# SortedRun and avoids reparsing entries during recovery.
132def disjoint_with_table(+tbl: Sstable.Table, rest: List<&2, Sstable.Table>) -> Bool:
133 match rest:
134 case Nil{}:
135 True{}
136 case Con{+h, t}:
137 mid_and(Sstable.ranges_disjoint(tbl, h), disjoint_with_table(tbl, t))
138
139# Return the level pairwise disjoint for the pure recovery decisions.
140def level_pairwise_disjoint(tables: List<&2, Sstable.Table>) -> Bool:
141 match tables:
142 case Nil{}:
143 True{}
144 case Con{+h, +t}:
145 mid_and(disjoint_with_table(h, t), level_pairwise_disjoint(t))
146
147# Check lower-level levels disjoint for the pure recovery decisions.
148def lower_levels_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
149 match levels:
150 case Nil{}:
151 True{}
152 case Con{+level, rest}:
153 mid_and(level_pairwise_disjoint(level), lower_levels_disjoint(rest))
154
155# Handle l1 plus disjoint in the pure recovery decisions.
156def l1_plus_disjoint(levels: List<&2, List<&2, Sstable.Table>>) -> Bool:
157 match levels:
158 case Nil{}:
159 True{}
160 case Con{l0, lower}:
161 lower_levels_disjoint(lower)
162
163# Handle needs flush cap in the pure recovery decisions.
164def needs_flush_cap(+mem: MemTable.MemTable, +cap: Nat) -> Bool:
165 Nat.is_lt(cap, MemTable.count(mem))