src/MemTable.bend
mylsm-lsm-store@0.5.0.0 · 257 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.5.0.0/src/Keys.bend as Keys
3import mylsm-lsm-store@0.5.0.0/src/StorageBytes.bend as StorageBytes
4
5# MemTable: newest-first prepend log (NOT sorted — sorting happens once at
6# flush). Rationale: put/del are O(1) with ZERO comparisons on the write
7# path, the fastest possible shape; reads scan newest-first (fine at the
8# 4096-entry cap); the scan state machine below is provable with only the
9# Keys.str_eq_refl rewrite (no ordering lemmas needed until flush sorts).
10
11# Represent Entry data used by the in-memory table operations.
12type Entry is Data:
13 Entry{key: String, val: Maybe<&2, String>}
14
15# Represent MemTable data used by the in-memory table operations.
16type MemTable is Data:
17 MT{entries: List<&2, Entry>}
18
19# Handle empty in the in-memory table operations.
20def empty() -> MemTable:
21 MT{Nil{}}
22
23# Handle put in the in-memory table operations.
24def put(tab: MemTable, key: String, val: String) -> MemTable:
25 match tab:
26 case MT{entries}:
27 MT{Con{Entry{key, Some{val}}, entries}}
28
29# Handle del in the in-memory table operations.
30def del(tab: MemTable, key: String) -> MemTable:
31 match tab:
32 case MT{entries}:
33 MT{Con{Entry{key, None{}}, entries}}
34
35# Handle count in the in-memory table operations.
36def count(tab: MemTable) -> Nat:
37 match tab:
38 case MT{entries}:
39 List.length(&2, Entry, entries)
40
41# Counts UTF-8 payload bytes for a value or tombstone.
42def payload_value_bytes(value: Maybe<&2, String>) -> Nat:
43 match value:
44 case None{}:
45 0n
46 case Some{text}:
47 StorageBytes.string_size(text)
48
49# Sums payload bytes across MemTable entries.
50def payload_entries_bytes(+entries: List<&2, Entry>) -> Nat:
51 match entries:
52 case Nil{}:
53 0n
54 case Con{Entry{key, value}, tail}:
55 Nat.add(Nat.add(StorageBytes.string_size(key), payload_value_bytes(value)),
56 payload_entries_bytes(tail))
57
58# Counts active and frozen MemTable payload bytes.
59def payload_bytes(tab: MemTable) -> Nat:
60 match tab:
61 case MT{entries}:
62 payload_entries_bytes(entries)
63
64# Scan state machine (Base List.merge pattern): the driver matches fuel +
65# structural state only; the leaf folds one entry (done-flag freezes the
66# answer — including tombstone None, which hides older versions).
67def scan_step(done: Bool, eq: Bool, hv: Maybe<&2, String>, ans: Maybe<&2, String>) -> (Bool & Maybe<&2, String>):
68 match done:
69 case True{}:
70 (True{}, ans)
71 case False{}:
72 match eq:
73 case True{}:
74 (True{}, hv)
75 case False{}:
76 (False{}, ans)
77
78# Scan go for the in-memory table operations.
79def scan_go(fuel: Nat, +key: String, st: (Bool & Maybe<&2, String>), entries: List<&2, Entry>) -> Maybe<&2, String>:
80 match fuel:
81 case 0n:
82 (done, ans) = st
83 ans
84 case 1n+f:
85 (done, ans) = st
86 match entries:
87 case Nil{}:
88 ans
89 case Con{Entry{ekey, val}, t}:
90 scan_go(f, key, scan_step(done, Keys.eq(ekey, key), val, ans), t)
91
92# Handle get in the in-memory table operations.
93def get(tab: MemTable, +key: String) -> Maybe<&2, String>:
94 match tab:
95 case MT{+entries}:
96 scan_go(List.length(&2, Entry, entries), key, (False{}, None{}), entries)
97
98# Hit-detecting scan: outer None = miss (keep searching older sources),
99# Some{val} = hit (val may be the None{} tombstone — stop, it shadows).
100def scan_hit_step(
101 done: Bool,
102 eq: Bool,
103 hv: Maybe<&2, String>,
104 ans: Maybe<&2, Maybe<&2, String>>
105) -> (Bool & Maybe<&2, Maybe<&2, String>>):
106 match done:
107 case True{}:
108 (True{}, ans)
109 case False{}:
110 match eq:
111 case True{}:
112 (True{}, Some{hv})
113 case False{}:
114 (False{}, ans)
115
116# Scan hit for the in-memory table operations.
117def scan_hit(
118 fuel: Nat,
119 +key: String,
120 st: (Bool & Maybe<&2, Maybe<&2, String>>),
121 entries: List<&2, Entry>
122) -> Maybe<&2, Maybe<&2, String>>:
123 match fuel:
124 case 0n:
125 (done, ans) = st
126 ans
127 case 1n+f:
128 (done, ans) = st
129 match entries:
130 case Nil{}:
131 ans
132 case Con{Entry{ekey, val}, t}:
133 scan_hit(f, key, scan_hit_step(done, Keys.eq(ekey, key), val, ans), t)
134
135# Return hit for the in-memory table operations.
136def get_hit(tab: MemTable, +key: String) -> Maybe<&2, Maybe<&2, String>>:
137 match tab:
138 case MT{+entries}:
139 scan_hit(List.length(&2, Entry, entries), key, (False{}, None{}), entries)
140
141# Lemma: a frozen (done) scan always answers ans.
142def frozen_lemma(
143 fuel: Nat,
144 key: String,
145 ans: Maybe<&2, String>,
146 entries: List<&2, Entry>
147) -> {scan_go(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, String>}:
148 match fuel:
149 case 0n:
150 {==}
151 case 1n+f:
152 match entries:
153 case Nil{}:
154 {==}
155 case Con{Entry{ekey, val}, t}:
156 %frozen_lemma(f, key, ans, t) : {scan_go(f, key, (True{}, ans), t) == _ : Maybe<&2, String>}
157 {==}
158
159# Lemma: reading a freshly-put key answers its value.
160def ryw_core(
161 +entries: List<&2, Entry>,
162 +key: String,
163 val: String,
164) -> {scan_go(List.length(&2, Entry, Con{Entry{key, Some{val}}, entries}), key, (False{}, None{}), Con{Entry{key, Some{val}}, entries}) == Some{val} : Maybe<&2, String>}:
165 %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_go(List.length(&2, Entry, entries), key, scan_step(False{}, _, Some{val}, None{}),
166 entries) == Some{val} : Maybe<&2, String>}
167 %frozen_lemma(List.length(&2, Entry, entries), key, Some{val}, entries) : {scan_go(List.length(&2, Entry, entries), key, (True{}, Some{val}), entries) == _ : Maybe<&2, String>}
168 {==}
169
170# Handle ryw bridge in the in-memory table operations.
171def ryw_bridge(
172 tab: MemTable,
173 +key: String,
174 +val: String
175) -> {get(put(tab, key, val), key) == Some{val} : Maybe<&2, String>}:
176 match tab:
177 case MT{entries}:
178 ryw_core(entries, key, val)
179
180# Lemma: reading a freshly-deleted key answers None (tombstone freezes).
181def del_core(
182 +entries: List<&2, Entry>,
183 +key: String,
184) -> {scan_go(List.length(&2, Entry, Con{Entry{key, None{}}, entries}), key, (False{}, None{}), Con{Entry{key, None{}}, entries}) == None{} : Maybe<&2, String>}:
185 %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_go(List.length(&2, Entry, entries), key, scan_step(False{}, _, None{}, None{}), entries) == None{} : Maybe<&2, String>}
186 %frozen_lemma(List.length(&2, Entry, entries), key, None{}, entries) : {scan_go(List.length(&2, Entry, entries), key, (True{}, None{}), entries) == _ : Maybe<&2, String>}
187 {==}
188
189# Handle del bridge in the in-memory table operations.
190def del_bridge(
191 tab: MemTable,
192 +key: String,
193 val: String
194) -> {get(del(put(tab, key, val), key), key) == None{} : Maybe<&2, String>}:
195 match tab:
196 case MT{entries}:
197 del_core(Con{Entry{key, Some{val}}, entries}, key)
198
199# Lemma: a frozen hit-scan always answers ans.
200def frozen_hit_lemma(
201 fuel: Nat,
202 key: String,
203 ans: Maybe<&2, Maybe<&2, String>>,
204 entries: List<&2, Entry>
205) -> {scan_hit(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, Maybe<&2, String>>}:
206 match fuel:
207 case 0n:
208 {==}
209 case 1n+f:
210 match entries:
211 case Nil{}:
212 {==}
213 case Con{Entry{ekey, val}, t}:
214 %frozen_hit_lemma(f, key, ans, t) : {scan_hit(f, key, (True{}, ans), t) == _ : Maybe<&2, Maybe<&2, String>>}
215 {==}
216
217# Lemma: hit-reading a freshly-put key answers a value hit.
218def ryw_hit_core(
219 +entries: List<&2, Entry>,
220 +key: String,
221 val: String,
222) -> {scan_hit(List.length(&2, Entry, Con{Entry{key, Some{val}}, entries}), key, (False{}, None{}), Con{Entry{key, Some{val}}, entries}) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}:
223 %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_hit(List.length(&2, Entry, entries), key, scan_hit_step(False{}, _, Some{val}, None{}),
224 entries) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}
225 %frozen_hit_lemma(List.length(&2, Entry, entries), key, Some{Some{val}}, entries) : {scan_hit(List.length(&2, Entry, entries), key, (True{}, Some{Some{val}}),
226 entries) == _ : Maybe<&2, Maybe<&2, String>>}
227 {==}
228
229# Resolve the hit for ryw bridge for the in-memory table operations.
230def hit_ryw_bridge(
231 tab: MemTable,
232 +key: String,
233 +val: String
234) -> {get_hit(put(tab, key, val), key) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}:
235 match tab:
236 case MT{entries}:
237 ryw_hit_core(entries, key, val)
238
239# Lemma: hit-reading a freshly-deleted key answers a tombstone hit.
240def del_hit_core(
241 +entries: List<&2, Entry>,
242 +key: String,
243) -> {scan_hit(List.length(&2, Entry, Con{Entry{key, None{}}, entries}), key, (False{}, None{}), Con{Entry{key, None{}}, entries}) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}:
244 %Equal.sym(Bool, Keys.eq(key, key), True{}, Keys.str_eq_refl(key)) : {scan_hit(List.length(&2, Entry, entries), key, scan_hit_step(False{}, _, None{}, None{}),
245 entries) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}
246 %frozen_hit_lemma(List.length(&2, Entry, entries), key, Some{None{}}, entries) : {scan_hit(List.length(&2, Entry, entries), key, (True{}, Some{None{}}), entries) == _ : Maybe<&2, Maybe<&2, String>>}
247 {==}
248
249# Resolve the hit for del bridge for the in-memory table operations.
250def hit_del_bridge(
251 tab: MemTable,
252 +key: String,
253 val: String
254) -> {get_hit(del(put(tab, key, val), key), key) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}:
255 match tab:
256 case MT{entries}:
257 del_hit_core(Con{Entry{key, Some{val}}, entries}, key)