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	type Entry is Data:
11	  Entry{key: String, val: Maybe<&2, String>}
12	
13	type MemTable is Data:
14	  MT{entries: List<&2, Entry>}
15	
16	def empty() -> MemTable:
17	  MT{Nil{}}
18	
19	def put(tab: MemTable, key: String, val: String) -> MemTable:
20	  match tab:
21	    case MT{entries}:
22	      MT{Con{Entry{key, Some{val}}, entries}}
23	
24	def del(tab: MemTable, key: String) -> MemTable:
25	  match tab:
26	    case MT{entries}:
27	      MT{Con{Entry{key, None{}}, entries}}
28	
29	def 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).
37	def 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	
48	def 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	
61	def 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).
68	def 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	
79	def 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	
92	def 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.
98	def 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.
111	def 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	
120	def 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).
126	def 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	
134	def 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.
140	def 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.
153	def 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	
162	def 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.
168	def 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	
176	def 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)