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