src/MemTable.bend checks

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

3 imports

import Base
import ./Keys.bend as Keys
import ./StorageBytes.bend as StorageBytes

Types

type Entry source · line 12 · raw

Data

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

Entry

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

type MemTable source · line 16 · raw

Data

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

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

Definitions

def empty source · line 20 · raw

MemTable

Handle empty in the in-memory table operations.

def put source · line 24 · raw

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

Handle put in the in-memory table operations.

def del source · line 30 · raw

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

Handle del in the in-memory table operations.

def count source · line 36 · raw

@tab:MemTable -> Nat

Handle count in the in-memory table operations.

def payload_value_bytes source · line 42 · raw

@value:Maybe<&2, String> -> Nat

Counts UTF-8 payload bytes for a value or tombstone.

def payload_entries_bytes source · line 50 · raw

@+entries:List<&2, Entry> -> Nat

Sums payload bytes across MemTable entries.

def payload_bytes source · line 59 · raw

@tab:MemTable -> Nat

Counts active and frozen MemTable payload bytes.

def scan_step source · line 67 · 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 79 · 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 93 · raw

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

Handle get in the in-memory table operations.

def scan_hit_step source · line 100 · 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 117 · 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 136 · raw

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

Return hit for the in-memory table operations.

def frozen_lemma source · line 142 · 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 160 · 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 171 · 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 181 · 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 190 · 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 200 · 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 218 · 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 230 · 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 240 · 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 250 · 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.