src/Wal.bend fails

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

2 imports

import Base
import ./Keys.bend as Keys

Types

type Mut source · line 13 · raw

Data

Put
```
@key:String -> @val:String -> Mut
```
Del
```
@key:String -> Mut
```

type Batch source · line 17 · raw

Data

Batch
```
@muts:List<&2, Mut> -> Batch
```

type Phase source · line 66 · raw

Data

PTag
```
Phase
```
RLen
```
@next:Phase -> Phase
```
PKey
```
Phase
```
PVal
```
Phase
```
PChk
```
Phase
```
PSemi
```
Phase
```
DKey
```
Phase
```
DChk
```
Phase
```
DSemi
```
Phase
```

type DecState source · line 69 · raw

Data

DS

@phase:Phase -> @muts:List<&2, Mut> -> @tag:Char -> @num:Nat -> @kacc:String -> @vacc:String -> @cacc:String -> @ok:Bool -> DecState

Definitions

def dashes source · line 22 · raw

@num:Nat -> String

def hash_str source · line 29 · raw

@str:String -> @acc:U32 -> U32

def hash3 source · line 36 · raw

@tag:Char -> @key:String -> @val:String -> U32

def chk4 source · line 39 · raw

@+word:U32 -> String

def enc_mut source · line 42 · raw

@mut:Mut -> String

def enc_muts source · line 49 · raw

@muts:List<&2, Mut> -> String

def encode source · line 56 · raw

@batch:Batch -> String

def stage source · line 61 · raw

@+staged:List<&2, Batch> -> @+batch:Batch -> List<&2, Batch>

def tag_dispatch source · line 72 · raw

@put:Bool -> @del:Bool -> @+muts:List<&2, Mut> -> DecState

def dash_step source · line 83 · raw

@dash:Bool -> @colon:Bool -> @next:Phase -> @+muts:List<&2, Mut> -> @+tag:Char -> @+num:Nat -> @+kacc:String -> @+vacc:String -> @+cacc:String -> DecState

def chk_next source · line 94 · raw

@ceq:Bool -> @next:Phase -> @+muts:List<&2, Mut> -> @+tag:Char -> @+key:String -> @+val:String -> DecState

def semi_step source · line 101 · raw

@semi:Bool -> @put:Bool -> @+muts:List<&2, Mut> -> @+key:String -> @+val:String -> DecState

def phase_router source · line 112 · raw

@phase:Phase -> @+muts:List<&2, Mut> -> @+tag:Char -> @+num:Nat -> @+kacc:String -> @+vacc:String -> @+cacc:String -> @+ch:Char -> DecState

def dec_step source · line 161 · raw

@st:DecState -> @ch:Char -> DecState

def dec_finish source · line 170 · raw

@ok:Bool -> @phase:Phase -> @+muts:List<&2, Mut> -> Pair(List<&2, Mut>, Bool)

def dec_extract source · line 181 · raw

@st:DecState -> Pair(List<&2, Mut>, Bool)

def dec_go source · line 186 · raw

@fuel:Nat -> @rest:String -> @st:DecState -> Pair(List<&2, Mut>, Bool)

def dec_run source · line 197 · raw

@fuel:Nat -> @rest:String -> @st:DecState -> DecState

Fuel-exact runner: consumes exactly len-bounded input, returns the state (no extraction — callers extract). Proof-only workhorse.

def dec_wrap source · line 206 · raw

@pair:Pair(List<&2, Mut>, Bool) -> Maybe<&2, Batch>

def decode source · line 215 · raw

@+str:String -> Maybe<&2, Batch>

def app_assoc source · line 220 · raw

@sa:String -> @sb:String -> @sc:String -> {String.append(String.append(sa, sb), sc) == String.append(sa, String.append(sb, sc)) : String}

def app_nil_r source · line 228 · raw

@str:String -> {String.append(str, "") == str : String}

def len_append source · line 235 · raw

@sa:String -> @sb:String -> {String.length(String.append(sa, sb)) == Nat.add(String.length(sa), String.length(sb)) : Nat}

def add_assoc source · line 243 · raw

@n1:Nat -> @n2:Nat -> @n3:Nat -> {Nat.add(Nat.add(n1, n2), n3) == Nat.add(n1, Nat.add(n2, n3)) : Nat}

def list_app_assoc source · line 251 · raw

@xs:List<&2, Mut> -> @ys:List<&2, Mut> -> @zs:List<&2, Mut> -> {List.append(&2, Mut, List.append(&2, Mut, xs, ys), zs) == List.append(&2, Mut, xs, List.append(&2, Mut, ys, zs)) : List<&2, Mut>}

def append_nil_r source · line 263 · raw

@+xs:List<&2, Mut> -> {List.append(&2, Mut, xs, []) == xs : List<&2, Mut>}

def jump source · line 272 · raw

@num:Nat -> @num0:Nat -> Nat

Unary counter: jump(n, num0) = num0 + n as 1n-chains (no appends, no assoc).

def jump_zero source · line 279 · raw

@num:Nat -> {jump(num, 0n) == num : Nat}

def jump_succ source · line 287 · raw

@num:Nat -> @num0:Nat -> {jump(num, 1n+num0) == 1n+jump(num, num0) : Nat}

def dashspan source · line 297 · raw

@num:Nat -> @tail:String -> @muts0:List<&2, Mut> -> @tag:Char -> @next:Phase -> @+num0:Nat -> @kacc0:String -> {dec_run(String.length(String.append(dashes(num), tail)), String.append(dashes(num), tail), DS{RLen{next}, muts0, tag, num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, jump(num, num0), kacc0, "", "", True{}}) : DecState}

RLen dash-run skip (unified len phase; next stored, never matched here). Fuel is len(span++tail): deconstructs with the Nat induction, tail opaque.

def keyspan source · line 315 · raw

@key:String -> @+kacc0:String -> @tail:String -> @muts0:List<&2, Mut> -> @tag:Char -> @vacc0:String -> {dec_run(String.length(String.append(key, tail)), String.append(key, tail), DS{PKey{}, muts0, tag, String.length(key), kacc0, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PKey{}, muts0, tag, 0n, String.append(kacc0, key), vacc0, "", True{}}) : DecState}

PKEY take: consumes key bytes; kacc0 generalized. Fuel is len(key++tail).

def valspan source · line 333 · raw

@val:String -> @+vacc0:String -> @tail:String -> @muts0:List<&2, Mut> -> @tag:Char -> @kacc:String -> {dec_run(String.length(String.append(val, tail)), String.append(val, tail), DS{PVal{}, muts0, tag, String.length(val), kacc, vacc0, "", True{}}) == dec_run(String.length(tail), tail, DS{PVal{}, muts0, tag, 0n, kacc, String.append(vacc0, val), "", True{}}) : DecState}

PVAL take: mirror for values.

def dkeyspan source · line 351 · raw

@key:String -> @+kacc0:String -> @tail:String -> @muts0:List<&2, Mut> -> @tag:Char -> {dec_run(String.length(String.append(key, tail)), String.append(key, tail), DS{DKey{}, muts0, tag, String.length(key), kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{DKey{}, muts0, tag, 0n, String.append(kacc0, key), "", "", True{}}) : DecState}

DKEY take: mirror for delete keys.

def is_decided source · line 371 · raw

@+_m:Maybe<&2, Batch> -> Bool

Total-parser witness used by the hardening law.