1	import Base
2	import ./Keys.bend as Keys
3	import ./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.
12	type Entry is Data:
13	  Entry{key: String, val: Maybe<&2, String>}
14	
15	# Represent MemTable data used by the in-memory table operations.
16	type MemTable is Data:
17	  MT{entries: List<&2, Entry>}
18	
19	# Handle empty in the in-memory table operations.
20	def empty() -> MemTable:
21	  MT{Nil{}}
22	
23	# Handle put in the in-memory table operations.
24	def 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.
30	def 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.
36	def 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.
42	def 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.
50	def 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.
59	def 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).
67	def 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.
79	def 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.
93	def 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).
100	def 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.
117	def 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.
136	def 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.
142	def 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.
160	def 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.
171	def 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).
181	def 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.
190	def 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.
200	def 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.
218	def 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.
230	def 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.
240	def 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.
250	def 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)