src/MemTable.bend source

src/MemTable.bend on the hub · documented module

import Baseimport ./Keys.bend as Keys# MemTable: newest-first prepend log (NOT sorted — sorting happens once at# flush). Rationale: put/del are O(1) with ZERO comparisons on the write# path, the fastest possible shape; reads scan newest-first (fine at the# 4096-entry cap); the scan state machine below is provable with only the# Keys.str_eq_refl rewrite (no ordering lemmas needed until flush sorts).type Entry is Data:  Entry{key: String, val: Maybe<&2, String>}type MemTable is Data:  MT{entries: List<&2, Entry>}def empty() -> MemTable:  MT{Nil{}}def put(t: MemTable, k: String, v: String) -> MemTable:  match t:    case MT{entries}:      MT{Con{Entry{k, Some{v}}, entries}}def del(t: MemTable, k: String) -> MemTable:  match t:    case MT{entries}:      MT{Con{Entry{k, None{}}, entries}}def count(t: MemTable) -> Nat:  match t:    case MT{entries}:      List.length(&2, Entry, entries)# Scan state machine (Base List.merge pattern): the driver matches fuel +# structural state only; the leaf folds one entry (done-flag freezes the# answer — including tombstone None, which hides older versions).def scan_step(done: Bool, eq: Bool, hv: Maybe<&2, String>, ans: Maybe<&2, String>) -> (Bool & Maybe<&2, String>):  match done:    case True{}:      (True{}, ans)    case False{}:      match eq:        case True{}:          (True{}, hv)        case False{}:          (False{}, ans)def scan_go(fuel: Nat, +k: String, st: (Bool & Maybe<&2, String>), entries: List<&2, Entry>) -> Maybe<&2, String>:  match fuel:    case 0n:      (done, ans) = st      ans    case 1n+f:      (done, ans) = st      match entries:        case Nil{}:          ans        case Con{Entry{key, val}, t}:          scan_go(f, k, scan_step(done, Keys.eq(key, k), val, ans), t)def get(t: MemTable, +k: String) -> Maybe<&2, String>:  match t:    case MT{+entries}:      scan_go(List.length(&2, Entry, entries), k, (False{}, None{}), entries)# Lemma: a frozen (done) scan always answers ans.def frozen_lemma(fuel: Nat, k: String, ans: Maybe<&2, String>, entries: List<&2, Entry>) -> {scan_go(fuel, k, (True{}, ans), entries) == ans : Maybe<&2, String>}:  match fuel:    case 0n:      {==}    case 1n+f:      match entries:        case Nil{}:          {==}        case Con{Entry{key, val}, t}:          %frozen_lemma(f, k, ans, t) : {scan_go(f, k, (True{}, ans), t) == _ : Maybe<&2, String>}          {==}# Lemma: reading a freshly-put key answers its value.def ryw_core(+entries: List<&2, Entry>, +k: String, v: String) -> {scan_go(List.length(&2, Entry, Con{Entry{k, Some{v}}, entries}), k, (False{}, None{}), Con{Entry{k, Some{v}}, entries}) == Some{v} : Maybe<&2, String>}:  %Equal.sym(Bool, Keys.eq(k, k), True{}, Keys.str_eq_refl(k)) : {scan_go(List.length(&2, Entry, entries), k, scan_step(False{}, _, Some{v}, None{}), entries) == Some{v} : Maybe<&2, String>}  %frozen_lemma(List.length(&2, Entry, entries), k, Some{v}, entries) : {scan_go(List.length(&2, Entry, entries), k, (True{}, Some{v}), entries) == _ : Maybe<&2, String>}  {==}def ryw_bridge(t: MemTable, +k: String, +v: String) -> {get(put(t, k, v), k) == Some{v} : Maybe<&2, String>}:  match t:    case MT{entries}:      ryw_core(entries, k, v)# Lemma: reading a freshly-deleted key answers None (tombstone freezes).def del_core(+entries: List<&2, Entry>, +k: String) -> {scan_go(List.length(&2, Entry, Con{Entry{k, None{}}, entries}), k, (False{}, None{}), Con{Entry{k, None{}}, entries}) == None{} : Maybe<&2, String>}:  %Equal.sym(Bool, Keys.eq(k, k), True{}, Keys.str_eq_refl(k)) : {scan_go(List.length(&2, Entry, entries), k, scan_step(False{}, _, None{}, None{}), entries) == None{} : Maybe<&2, String>}  %frozen_lemma(List.length(&2, Entry, entries), k, None{}, entries) : {scan_go(List.length(&2, Entry, entries), k, (True{}, None{}), entries) == _ : Maybe<&2, String>}  {==}def del_bridge(t: MemTable, +k: String, v: String) -> {get(del(put(t, k, v), k), k) == None{} : Maybe<&2, String>}:  match t:    case MT{entries}:      del_core(Con{Entry{k, Some{v}}, entries}, k)