src/Manifest.bend
mylsm-lsm-store@0.3.2.0 · 208 lines · 0 definitions
1import Base
2
3# Manifest (Task 5): which SSTables live at which level.
4# Format is positional (line i = level i, no level numbers to parse):
5# <name>,<name>
6# <name>
7# #<checksum-decimal>
8# Names are engine-generated (sst-<level>-<counter>.tbl) AND strictly
9# validated on parse ([A-Za-z0-9._-], not "." / ".."): T1 hostile bytes
10# must fail closed, never traverse directories (spec §8).
11# Checksum covers all content lines (fail-closed on corruption, like WAL).
12# Parsing leans on Base (split/join/starts_with/drop/read): precompiled,
13# trusted, zero proof burden — laws pin OUR format, not Base.
14
15type Manifest is Data:
16 M{levels: List<&2, List<&2, String>>}
17
18def mhash(str: String, seed: U32) -> U32:
19 match str:
20 case SNil{}:
21 seed
22 case SCon{c, t}:
23 mhash(t, U32.add(U32.mul(seed, 31), Char.to_u32(c)))
24
25def encode_line(names: List<&2, String>) -> String:
26 String.join(names, ",")
27
28def encode_lines(xss: List<&2, List<&2, String>>) -> List<&2, String>:
29 match xss:
30 case Nil{}:
31 Nil{}
32 case Con{h, t}:
33 Con{encode_line(h), encode_lines(t)}
34
35def serialize(mfst: Manifest) -> String:
36 match mfst:
37 case M{levels}:
38 +ls = encode_lines(levels)
39 +content = String.join(ls, SCon{Char.from_u32(10), SNil{}})
40 String.join(List.append(&2, String, ls, Con{"#" ++ U32.show(mhash(content, 7)), Nil{}}), SCon{Char.from_u32(10), SNil{}})
41
42# --- Strict name validation (structural recursion + leaves; no fuel:
43# recursion is unconditional, decisions combine via leaves) ---
44def name_ok_step(ok: Bool, good: Bool) -> Bool:
45 match ok:
46 case True{}:
47 good
48 case False{}:
49 False{}
50
51def nc_alpha(ok: Bool, ch: Char) -> Bool:
52 match ok:
53 case True{}:
54 True{}
55 case False{}:
56 Char.is_digit(ch)
57
58def nc_us(ok: Bool, +ch: Char) -> Bool:
59 match ok:
60 case True{}:
61 True{}
62 case False{}:
63 nc_alpha(Char.is_alpha(ch), ch)
64
65def nc_dot(ok: Bool, +ch: Char) -> Bool:
66 match ok:
67 case True{}:
68 True{}
69 case False{}:
70 nc_us(Char.is_eq(ch, Char.from_u32(95)), ch)
71
72def nc_dash(ok: Bool, +ch: Char) -> Bool:
73 match ok:
74 case True{}:
75 True{}
76 case False{}:
77 nc_dot(Char.is_eq(ch, Char.from_u32(46)), ch)
78
79def name_char_ok(+ch: Char) -> Bool:
80 nc_dash(Char.is_eq(ch, Char.from_u32(45)), ch)
81
82def name_go(str: String, ok: Bool) -> Bool:
83 match str:
84 case SNil{}:
85 ok
86 case SCon{h, t}:
87 name_go(t, name_ok_step(ok, name_char_ok(h)))
88
89def name_dots2(d2: Bool, str: String) -> Bool:
90 match d2:
91 case True{}:
92 False{}
93 case False{}:
94 name_go(str, True{})
95
96def name_dots(d1: Bool, d2: Bool, str: String) -> Bool:
97 match d1:
98 case True{}:
99 False{}
100 case False{}:
101 name_dots2(d2, str)
102
103def name_ok(str: String) -> Bool:
104 match str:
105 case SNil{}:
106 False{}
107 case SCon{+h, +t}:
108 name_dots(String.eq(SCon{h, t}, "."), String.eq(SCon{h, t}, ".."), SCon{h, t})
109
110def names_and(lhs: Bool, rhs: Bool) -> Bool:
111 match lhs:
112 case True{}:
113 rhs
114 case False{}:
115 False{}
116
117def names_ok(xs: List<&2, String>) -> Bool:
118 match xs:
119 case Nil{}:
120 True{}
121 case Con{h, t}:
122 names_and(name_ok(h), names_ok(t))
123
124# --- Parse: validate everything first (Bool), then parse unchecked
125# (total, structural, no Maybe in loops). Top dispatch is a leaf. ---
126def line_valid(line: String) -> Bool:
127 match line:
128 case SNil{}:
129 True{}
130 case SCon{h, t}:
131 names_ok(String.split(SCon{h, t}, Char.from_u32(44)))
132
133def body_valid(ls: List<&2, String>) -> Bool:
134 match ls:
135 case Nil{}:
136 True{}
137 case Con{h, t}:
138 names_and(line_valid(h), body_valid(t))
139
140def chk_rd(opt: Maybe<&2, U32>, content: String) -> Bool:
141 match opt:
142 case None{}:
143 False{}
144 case Some{v}:
145 U32.is_eq(v, mhash(content, 7))
146
147def chk_sw(sw: Bool, chk: String, content: String) -> Bool:
148 match sw:
149 case True{}:
150 chk_rd(U32.read(String.drop(chk, 1n)), content)
151 case False{}:
152 False{}
153
154def chk_valid(+chk: String, content: String) -> Bool:
155 chk_sw(String.starts_with(chk, "#"), chk, content)
156
157def valid_split(pair: (List<&2, String> & String)) -> Bool:
158 match pair:
159 case (+body, chk):
160 names_and(body_valid(body), chk_valid(chk, String.join(body, SCon{Char.from_u32(10), SNil{}})))
161
162def split_last(ls: List<&2, String>, acc: List<&2, String>) -> (List<&2, String> & String):
163 match ls:
164 case Nil{}:
165 (List.reverse(&2, String, acc), "")
166 case Con{h, Nil{}}:
167 (List.reverse(&2, String, acc), h)
168 case Con{h, Con{k, t}}:
169 split_last(Con{k, t}, Con{h, acc})
170
171def valid_lines(lines: List<&2, String>) -> Bool:
172 valid_split(split_last(lines, Nil{}))
173
174def valid_manifest(str: String) -> Bool:
175 valid_lines(String.split(str, Char.from_u32(10)))
176
177def parse_line_u(line: String) -> List<&2, String>:
178 match line:
179 case SNil{}:
180 Nil{}
181 case SCon{h, t}:
182 String.split(SCon{h, t}, Char.from_u32(44))
183
184def parse_levels_u(ls: List<&2, String>, acc: List<&2, List<&2, String>>) -> List<&2, List<&2, String>>:
185 match ls:
186 case Nil{}:
187 List.reverse(&2, List<&2, String>, acc)
188 case Con{h, t}:
189 parse_levels_u(t, Con{parse_line_u(h), acc})
190
191def parse_unchecked(pair: (List<&2, String> & String)) -> Manifest:
192 match pair:
193 case (body, chk):
194 M{parse_levels_u(body, Nil{})}
195
196def parse_dispatch(ok: Bool, str: String) -> Maybe<&2, Manifest>:
197 match ok:
198 case True{}:
199 Some{parse_unchecked(split_last(String.split(str, Char.from_u32(10)), Nil{}))}
200 case False{}:
201 None{}
202
203def parse(+str: String) -> Maybe<&2, Manifest>:
204 parse_dispatch(valid_manifest(str), str)
205
206# Total-parser witness used by the hardening law.
207def is_decided(+_m: Maybe<&2, Manifest>) -> Bool:
208 True{}