src/MemTable.bend checks

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

2 imports

import Base
import ./Keys.bend as Keys

Types

type Entry source · line 11 · raw

Data

Represent Entry data used by the in-memory table operations.

Entry

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

type MemTable source · line 15 · raw

Data

Represent MemTable data used by the in-memory table operations.

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

Definitions

def empty source · line 19 · raw

MemTable

Handle empty in the in-memory table operations.

def put source · line 23 · raw

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

Handle put in the in-memory table operations.

def del source · line 29 · raw

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

Handle del in the in-memory table operations.

def count source · line 35 · raw

@tab:MemTable -> Nat

Handle count in the in-memory table operations.

def scan_step source · line 43 · 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 55 · raw

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

Scan go for the in-memory table operations.

def get source · line 69 · raw

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

Handle get in the in-memory table operations.

def scan_hit_step source · line 76 · 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 93 · raw

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

Scan hit for the in-memory table operations.

def get_hit source · line 112 · raw

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

Return hit for the in-memory table operations.

def frozen_lemma source · line 118 · 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 136 · 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 147 · raw

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

Handle ryw bridge in the in-memory table operations.

def del_core source · line 157 · 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 166 · raw

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

Handle del bridge in the in-memory table operations.

def frozen_hit_lemma source · line 176 · 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 194 · 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 206 · raw

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

Resolve the hit for ryw bridge for the in-memory table operations.

def del_hit_core source · line 216 · 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 226 · raw

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

Resolve the hit for del bridge for the in-memory table operations.