def ryw_core

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

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

159# Lemma: reading a freshly-put key answers its value.
160def 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  {==}