src/Wal.bend fails

raw source on the hub · import 0x05fa0e42448e8e221df592b204de523d/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 63 · 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 66 · 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

@n:Nat -> String

def hash_str source · line 29 · raw

@s:String -> @h:U32 -> U32

def hash3 source · line 36 · raw

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

def chk4 source · line 39 · raw

@+h:U32 -> String

def enc_mut source · line 42 · raw

@m:Mut -> String

def enc_muts source · line 49 · raw

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

def encode source · line 56 · raw

@b:Batch -> String

def tag_dispatch source · line 69 · raw

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

def dash_step source · line 80 · 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 91 · raw

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

def semi_step source · line 98 · raw

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

def phase_router source · line 109 · raw

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

def dec_step source · line 158 · raw

@st:DecState -> @h:Char -> DecState

def dec_finish source · line 167 · raw

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

def dec_extract source · line 178 · raw

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

def dec_go source · line 183 · raw

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

def dec_run source · line 194 · 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 203 · raw

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

def decode source · line 212 · raw

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

def app_assoc source · line 217 · raw

@a:String -> @b:String -> @c:String -> {String.append(String.append(a, b), c) == String.append(a, String.append(b, c)) : String}

def app_nil_r source · line 225 · raw

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

def len_append source · line 232 · raw

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

def add_assoc source · line 240 · raw

@a:Nat -> @b:Nat -> @c:Nat -> {Nat.add(Nat.add(a, b), c) == Nat.add(a, Nat.add(b, c)) : Nat}

def list_app_assoc source · line 248 · raw

@a:List<&2, Mut> -> @b:List<&2, Mut> -> @c:List<&2, Mut> -> {List.append(&2, Mut, List.append(&2, Mut, a, b), c) == List.append(&2, Mut, a, List.append(&2, Mut, b, c)) : List<&2, Mut>}

def append_nil_r source · line 256 · raw

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

def jump source · line 265 · raw

@n:Nat -> @num0:Nat -> Nat

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

def jump_zero source · line 272 · raw

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

def jump_succ source · line 280 · raw

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

def dashspan source · line 290 · raw

@n:Nat -> @tail:String -> @muts0:List<&2, Mut> -> @tag:Char -> @next:Phase -> @+num0:Nat -> @kacc0:String -> {dec_run(String.length(String.append(dashes(n), tail)), String.append(dashes(n), tail), DS{RLen{next}, muts0, tag, num0, kacc0, "", "", True{}}) == dec_run(String.length(tail), tail, DS{RLen{next}, muts0, tag, jump(n, 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 300 · 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 311 · 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 322 · 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 336 · raw

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

Total-parser witness used by the hardening law.