def ryw_hit_core

mylsm-lsm-store@0.6.0.1 · src/MemTable.bend:217

import Base
import mylsm-lsm-store@0.6.0.1/src/Keys.bend as Keys

217# Lemma: hit-reading a freshly-put key answers a value hit.
218def 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  {==}