1	import Base
2	import ./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.
11	type Entry is Data:
12	  Entry{key: String, val: Maybe<&2, String>}
13	
14	# Represent MemTable data used by the in-memory table operations.
15	type MemTable is Data:
16	  MT{entries: List<&2, Entry>}
17	
18	# Handle empty in the in-memory table operations.
19	def empty() -> MemTable:
20	  MT{Nil{}}
21	
22	# Handle put in the in-memory table operations.
23	def 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.
29	def 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.
35	def 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).
43	def 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.
55	def 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.
69	def 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).
76	def 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.
93	def 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.
112	def 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.
118	def 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.
136	def 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.
147	def 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).
157	def 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.
166	def 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.
176	def 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.
194	def 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.
206	def 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.
216	def 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.
226	def 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)