src/MemTable.bend

mylsm-lsm-store@0.3.2.0 · 179 lines · 22 definitions

1import Base
2import mylsm-lsm-store@0.3.2.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
10type Entry is Data:
11  Entry{key: String, val: Maybe<&2, String>}
12
13type MemTable is Data:
14  MT{entries: List<&2, Entry>}
15
16def empty() -> MemTable:
17  MT{Nil{}}
18
19def put(tab: MemTable, key: String, val: String) -> MemTable:
20  match tab:
21    case MT{entries}:
22      MT{Con{Entry{key, Some{val}}, entries}}
23
24def del(tab: MemTable, key: String) -> MemTable:
25  match tab:
26    case MT{entries}:
27      MT{Con{Entry{key, None{}}, entries}}
28
29def count(tab: MemTable) -> Nat:
30  match tab:
31    case MT{entries}:
32      List.length(&2, Entry, entries)
33
34# Scan state machine (Base List.merge pattern): the driver matches fuel +
35# structural state only; the leaf folds one entry (done-flag freezes the
36# answer — including tombstone None, which hides older versions).
37def scan_step(done: Bool, eq: Bool, hv: Maybe<&2, String>, ans: Maybe<&2, String>) -> (Bool & Maybe<&2, String>):
38  match done:
39    case True{}:
40      (True{}, ans)
41    case False{}:
42      match eq:
43        case True{}:
44          (True{}, hv)
45        case False{}:
46          (False{}, ans)
47
48def scan_go(fuel: Nat, +key: String, st: (Bool & Maybe<&2, String>), entries: List<&2, Entry>) -> Maybe<&2, String>:
49  match fuel:
50    case 0n:
51      (done, ans) = st
52      ans
53    case 1n+f:
54      (done, ans) = st
55      match entries:
56        case Nil{}:
57          ans
58        case Con{Entry{ekey, val}, t}:
59          scan_go(f, key, scan_step(done, Keys.eq(ekey, key), val, ans), t)
60
61def get(tab: MemTable, +key: String) -> Maybe<&2, String>:
62  match tab:
63    case MT{+entries}:
64      scan_go(List.length(&2, Entry, entries), key, (False{}, None{}), entries)
65
66# Hit-detecting scan: outer None = miss (keep searching older sources),
67# Some{val} = hit (val may be the None{} tombstone — stop, it shadows).
68def scan_hit_step(done: Bool, eq: Bool, hv: Maybe<&2, String>, ans: Maybe<&2, Maybe<&2, String>>) -> (Bool & Maybe<&2, Maybe<&2, String>>):
69  match done:
70    case True{}:
71      (True{}, ans)
72    case False{}:
73      match eq:
74        case True{}:
75          (True{}, Some{hv})
76        case False{}:
77          (False{}, ans)
78
79def scan_hit(fuel: Nat, +key: String, st: (Bool & Maybe<&2, Maybe<&2, String>>), entries: List<&2, Entry>) -> Maybe<&2, 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_hit(f, key, scan_hit_step(done, Keys.eq(ekey, key), val, ans), t)
91
92def get_hit(tab: MemTable, +key: String) -> Maybe<&2, Maybe<&2, String>>:
93  match tab:
94    case MT{+entries}:
95      scan_hit(List.length(&2, Entry, entries), key, (False{}, None{}), entries)
96
97# Lemma: a frozen (done) scan always answers ans.
98def frozen_lemma(fuel: Nat, key: String, ans: Maybe<&2, String>, entries: List<&2, Entry>) -> {scan_go(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, String>}:
99  match fuel:
100    case 0n:
101      {==}
102    case 1n+f:
103      match entries:
104        case Nil{}:
105          {==}
106        case Con{Entry{ekey, val}, t}:
107          %frozen_lemma(f, key, ans, t) : {scan_go(f, key, (True{}, ans), t) == _ : Maybe<&2, String>}
108          {==}
109
110# Lemma: reading a freshly-put key answers its value.
111def ryw_core(
112  +entries: List<&2, Entry>,
113  +key: String,
114  val: String,
115) -> {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>}:
116  %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{}), entries) == Some{val} : Maybe<&2, String>}
117  %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>}
118  {==}
119
120def ryw_bridge(tab: MemTable, +key: String, +val: String) -> {get(put(tab, key, val), key) == Some{val} : Maybe<&2, String>}:
121  match tab:
122    case MT{entries}:
123      ryw_core(entries, key, val)
124
125# Lemma: reading a freshly-deleted key answers None (tombstone freezes).
126def del_core(
127  +entries: List<&2, Entry>,
128  +key: String,
129) -> {scan_go(List.length(&2, Entry, Con{Entry{key, None{}}, entries}), key, (False{}, None{}), Con{Entry{key, None{}}, entries}) == None{} : Maybe<&2, String>}:
130  %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>}
131  %frozen_lemma(List.length(&2, Entry, entries), key, None{}, entries) : {scan_go(List.length(&2, Entry, entries), key, (True{}, None{}), entries) == _ : Maybe<&2, String>}
132  {==}
133
134def del_bridge(tab: MemTable, +key: String, val: String) -> {get(del(put(tab, key, val), key), key) == None{} : Maybe<&2, String>}:
135  match tab:
136    case MT{entries}:
137      del_core(Con{Entry{key, Some{val}}, entries}, key)
138
139# Lemma: a frozen hit-scan always answers ans.
140def frozen_hit_lemma(fuel: Nat, key: String, ans: Maybe<&2, Maybe<&2, String>>, entries: List<&2, Entry>) -> {scan_hit(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, Maybe<&2, String>>}:
141  match fuel:
142    case 0n:
143      {==}
144    case 1n+f:
145      match entries:
146        case Nil{}:
147          {==}
148        case Con{Entry{ekey, val}, t}:
149          %frozen_hit_lemma(f, key, ans, t) : {scan_hit(f, key, (True{}, ans), t) == _ : Maybe<&2, Maybe<&2, String>>}
150          {==}
151
152# Lemma: hit-reading a freshly-put key answers a value hit.
153def ryw_hit_core(
154  +entries: List<&2, Entry>,
155  +key: String,
156  val: String,
157) -> {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>>}:
158  %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{}), entries) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}
159  %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}}), entries) == _ : Maybe<&2, Maybe<&2, String>>}
160  {==}
161
162def hit_ryw_bridge(tab: MemTable, +key: String, +val: String) -> {get_hit(put(tab, key, val), key) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}:
163  match tab:
164    case MT{entries}:
165      ryw_hit_core(entries, key, val)
166
167# Lemma: hit-reading a freshly-deleted key answers a tombstone hit.
168def del_hit_core(
169  +entries: List<&2, Entry>,
170  +key: String,
171) -> {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>>}:
172  %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{}), entries) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}
173  %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>>}
174  {==}
175
176def hit_del_bridge(tab: MemTable, +key: String, val: String) -> {get_hit(del(put(tab, key, val), key), key) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}:
177  match tab:
178    case MT{entries}:
179      del_hit_core(Con{Entry{key, Some{val}}, entries}, key)