src/MemTable.bend fails

raw source on the hub · import mylsm-lsm-store@0.3.1.0/src/MemTable.bend as MemTable

2 imports

import Base
import ./Keys.bend as Keys

Types

type Entry source · line 10 · raw

Data

Entry

@key:String -> @val:Maybe<&2, String> -> Entry

type MemTable source · line 13 · raw

Data

MT
```
@entries:List<&2, Entry> -> MemTable
```

Definitions

def empty source · line 16 · raw

MemTable

def put source · line 19 · raw

@tab:MemTable -> @key:String -> @val:String -> MemTable

def del source · line 24 · raw

@tab:MemTable -> @key:String -> MemTable

def count source · line 29 · raw

@tab:MemTable -> Nat

def scan_step source · line 37 · raw

@done:Bool -> @eq:Bool -> @hv:Maybe<&2, String> -> @ans:Maybe<&2, String> -> Pair(Bool, Maybe<&2, String>)

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_go source · line 48 · raw

@fuel:Nat -> @+key:String -> @st:Pair(Bool, Maybe<&2, String>) -> @entries:List<&2, Entry> -> Maybe<&2, String>

def get source · line 61 · raw

@tab:MemTable -> @+key:String -> Maybe<&2, String>

def scan_hit_step source · line 68 · raw

@done:Bool -> @eq:Bool -> @hv:Maybe<&2, String> -> @ans:Maybe<&2, Maybe<&2, String>> -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)

Hit-detecting scan: outer None = miss (keep searching older sources), Some{val} = hit (val may be the None{} tombstone — stop, it shadows).

def scan_hit source · line 79 · raw

@fuel:Nat -> @+key:String -> @st:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> @entries:List<&2, Entry> -> Maybe<&2, Maybe<&2, String>>

def get_hit source · line 92 · raw

@tab:MemTable -> @+key:String -> Maybe<&2, Maybe<&2, String>>

def frozen_lemma source · line 98 · raw

@fuel:Nat -> @key:String -> @ans:Maybe<&2, String> -> @entries:List<&2, Entry> -> {scan_go(fuel, key, (True{}, ans), entries) == ans : Maybe<&2, String>}

Lemma: a frozen (done) scan always answers ans.

def ryw_core source · line 111 · raw

@+entries:List<&2, Entry> -> @+key:String -> @val:String -> {scan_go(List.length(&2, Entry, Entry{key, Some{val}} <> entries), key, (False{}, None{}), Entry{key, Some{val}} <> entries) == Some{val} : Maybe<&2, String>}

Lemma: reading a freshly-put key answers its value.

def ryw_bridge source · line 120 · raw

@tab:MemTable -> @+key:String -> @+val:String -> {get(put(tab, key, val), key) == Some{val} : Maybe<&2, String>}

def del_core source · line 126 · raw

@+entries:List<&2, Entry> -> @+key:String -> {scan_go(List.length(&2, Entry, Entry{key, None{}} <> entries), key, (False{}, None{}), Entry{key, None{}} <> entries) == None{} : Maybe<&2, String>}

Lemma: reading a freshly-deleted key answers None (tombstone freezes).

def del_bridge source · line 134 · raw

@tab:MemTable -> @+key:String -> @val:String -> {get(del(put(tab, key, val), key), key) == None{} : Maybe<&2, String>}

def frozen_hit_lemma source · line 140 · raw

@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>>}

Lemma: a frozen hit-scan always answers ans.

def ryw_hit_core source · line 153 · raw

@+entries:List<&2, Entry> -> @+key:String -> @val:String -> {scan_hit(List.length(&2, Entry, Entry{key, Some{val}} <> entries), key, (False{}, None{}), Entry{key, Some{val}} <> entries) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}

Lemma: hit-reading a freshly-put key answers a value hit.

def hit_ryw_bridge source · line 162 · raw

@tab:MemTable -> @+key:String -> @+val:String -> {get_hit(put(tab, key, val), key) == Some{Some{val}} : Maybe<&2, Maybe<&2, String>>}

def del_hit_core source · line 168 · raw

@+entries:List<&2, Entry> -> @+key:String -> {scan_hit(List.length(&2, Entry, Entry{key, None{}} <> entries), key, (False{}, None{}), Entry{key, None{}} <> entries) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}

Lemma: hit-reading a freshly-deleted key answers a tombstone hit.

def hit_del_bridge source · line 176 · raw

@tab:MemTable -> @+key:String -> @val:String -> {get_hit(del(put(tab, key, val), key), key) == Some{None{}} : Maybe<&2, Maybe<&2, String>>}