journal.bend relies on unsafe/foreign
raw source on the hub · import bend-kit-journal@0.1.0.0/journal.bend as Journal
Append-only journal: checksummed frames, fsync'd appends, and crash recovery of the committed prefix. Source: https://github.com/paymog/bend-kit/tree/main/journal
3 imports
import Base import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes import bend-kit-hash@0.1.0.0/hash.bend as Hash
Types
type Tail source · line 14 · raw
Data
Clean: the input ends on a frame boundary. Torn: the input ends inside a frame. A crash cut the last append short. Corrupt: a whole header or a whole frame fails its check. Recovery does not go past it.
CleanTail
TornTail
Corrupt@why:String -> Tail
type Step source · line 20 · raw
@-P:Type -> @-S:Type -> Type
One decoding step. Short, Bad, and End give the input back untouched, at the frame start.
End@-P:Type -> @-S:Type -> @s:S -> Step<P, S>
Short@-P:Type -> @-S:Type -> @s:S -> Step<P, S>
Bad@-P:Type -> @-S:Type -> @why:String -> @s:S -> Step<P, S>
Got@-P:Type -> @-S:Type -> @p:P -> @s:S -> Step<P, S>
type Recovery source · line 27 · raw
@-a:Quant -> @-P:Kind(a) -> @-S:Type -> Type
The committed records in order, how the input ends, and the input from the first frame not taken.
Recovery@-a:Quant -> @-P:Kind(a) -> @-S:Type -> @records:List<a, P> -> @tail:Tail -> @rest:S -> Recovery<a, P, S>
type Replay source · line 31 · raw
@-A:Type -> @-S:Type -> Type
The state after every committed record, how the input ends, and the input from the first frame not taken.
Replay@-A:Type -> @-S:Type -> @acc:A -> @tail:Tail -> @rest:S -> Replay<A, S>
type Cur source · line 233 · raw
Type
The Bytes instance. A cursor reads b from pos; pos only moves forward, past whole frames.
Cur@b:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> @pos:U32 -> Cur
type Journal source · line 309 · raw
Type
An open journal. max caps a record's length. end is the file's length. ok turns False when an append fails: what reached the disk is then unknown, so appends stop until the journal is reopened.
Journal@file:File -> @max:U32 -> @end:U32 -> @ok:Bool -> Journal
Definitions
def list.fits source · line 165 · raw
@xs:List<&2, U32> -> @+at:U32 -> @+n:U32 -> Pair(List<&2, U32>, Bool)
def list.field source · line 169 · raw
@xs:List<&2, U32> -> U32
def list.u32 source · line 176 · raw
@xs:List<&2, U32> -> @+at:U32 -> Pair(List<&2, U32>, U32)
def list.cut source · line 180 · raw
@xs:List<&2, U32> -> @+hs:U32 -> @+len:U32 -> Pair(List<&2, U32>, List<&2, U32>)
def list.skip source · line 184 · raw
@xs:List<&2, U32> -> @+hs:U32 -> @+len:U32 -> List<&2, U32>
def crc.bit source · line 187 · raw
@n:Nat -> @+c:U32 -> U32
def crc.go source · line 194 · raw
@xs:List<&2, U32> -> @+c:U32 -> U32
def list.crc source · line 202 · raw
@xs:List<&2, U32> -> U32
CRC-32 (ISO-HDLC, as zlib and Hash.crc32) of a list of octets, bit by bit.
def list.sum source · line 205 · raw
@xs:List<&2, U32> -> Pair(List<&2, U32>, U32)
def list.next source · line 209 · raw
@+max:U32 -> @xs:List<&2, U32> -> Step<List<&2, U32>, List<&2, U32>>
def list.recover source · line 212 · raw
@n:Nat -> @+max:U32 -> @xs:List<&2, U32> -> Recovery<&2, List<&2, U32>, List<&2, U32>>
def list.head source · line 218 · raw
@+len:U32 -> @+sum:U32 -> List<&2, U32>
def list.frame source · line 221 · raw
@+p:List<&2, U32> -> List<&2, U32>
def list.log source · line 225 · raw
@rs:List<&2, List<&2, U32>> -> List<&2, U32>
The frames of rs, one after another: what appending each record writes.
def cur.fits source · line 236 · raw
@c:Cur -> @+at:U32 -> @+n:U32 -> Pair(Cur, Bool)
def cur.field source · line 240 · raw
@m:Maybe<&2, U32> -> U32
def cur.u32.fin source · line 247 · raw
@+pos:U32 -> @r:Pair(0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes, Maybe<&2, U32>) -> Pair(Cur, U32)
def cur.u32 source · line 251 · raw
@c:Cur -> @+at:U32 -> Pair(Cur, U32)
def cur.cut.fin source · line 255 · raw
@+pos:U32 -> @r:Pair(0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes, 0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes) -> Pair(Cur, 0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes)
def cur.cut source · line 259 · raw
@c:Cur -> @+hs:U32 -> @+len:U32 -> Pair(Cur, 0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes)
def cur.skip source · line 263 · raw
@c:Cur -> @+hs:U32 -> @+len:U32 -> Cur
def cur.sum source · line 268 · raw
@p:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> Pair(0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes, U32)
ponytail: Hash.crc32 builds its 256-entry table per record; share one table if recovery gets hot.
def fuel source · line 272 · raw
@+len:U32 -> Nat
Every frame of b holds at least 12 octets, so len / 12 + 1 steps reach the end.
def frame.of source · line 280 · raw
@+len:U32 -> @r:Pair(0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes, U32) -> 0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes
def frame source · line 285 · raw
@p:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> 0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes
The frame that appending p writes.
def open.cut source · line 312 · raw
@r:Pair(File, Result<&1, &1, Pair(U32, String), Unit>) -> @+max:U32 -> @+end:U32 -> @-A:Type -> @acc:A -> IO(Result<&1, &1, Pair(U32, String), Pair(Journal, A)>)
def open.tail source · line 322 · raw
@t:Tail -> @file:File -> @+max:U32 -> @+pos:U32 -> @-A:Type -> @acc:A -> IO(Result<&1, &1, Pair(U32, String), Pair(Journal, A)>)
def open.replayed source · line 336 · raw
@file:File -> @+max:U32 -> @-A:Type -> @r:Replay<A, Cur> -> IO(Result<&1, &1, Pair(U32, String), Pair(Journal, A)>)
def append.back source · line 357 · raw
@+max:U32 -> @+end:U32 -> @+len:U32 -> @r:Pair(File, Result<&1, &1, Pair(U32, String), Unit>) -> Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>)
def append.write source · line 364 · raw
@file:File -> @+max:U32 -> @+end:U32 -> @f:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> IO(Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>))
def append.refuse source · line 370 · raw
@file:File -> @+max:U32 -> @+end:U32 -> @+ok:Bool -> @e:Pair(U32, String) -> IO(Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>))
def append.size source · line 375 · raw
@over:Bool -> @big:Bool -> @file:File -> @+max:U32 -> @+end:U32 -> @p:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> IO(Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>))
The file stays under 4 GiB, so every offset and the next open's read fit a U32.
def append.ok source · line 384 · raw
@ok:Bool -> @file:File -> @+max:U32 -> @+end:U32 -> @p:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> IO(Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>))
def append source · line 394 · raw
@j:Journal -> @p:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> IO(Pair(Journal, Result<&1, &1, Pair(U32, String), Unit>))
Appends p as one frame and answers once it is fsynced: Done means durable, under the trust assumptions in README.md. After a Fail the record may or may not survive a reopen.
def close source · line 398 · raw
@j:Journal -> IO(Unit)
Templates
template next.verdict source · line 38 · raw
@-P:Type -> @-S:Type -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @ok:Bool -> @+len:U32 -> @s:S -> @p:P -> Step<P, S>
template next.summed source · line 45 · raw
@-P:Type -> @-S:Type -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @+want:U32 -> @+len:U32 -> @s:S -> @r:Pair(P, U32) -> Step<P, S>
template next.cut source · line 49 · raw
@-P:Type -> @-S:Type -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+want:U32 -> @+len:U32 -> @r:Pair(S, P) -> Step<P, S>
template next.want source · line 53 · raw
@-P:Type -> @-S:Type -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+len:U32 -> @r:Pair(S, U32) -> Step<P, S>
template next.body source · line 57 · raw
@-P:Type -> @-S:Type -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+len:U32 -> @r:Pair(S, Bool) -> Step<P, S>
template next.size source · line 65 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @over:Bool -> @+len:U32 -> @s:S -> Step<P, S>
template next.head source · line 72 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @ok:Bool -> @+max:U32 -> @+len:U32 -> @s:S -> Step<P, S>
template next.lenx source · line 79 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+max:U32 -> @+len:U32 -> @r:Pair(S, U32) -> Step<P, S>
template next.len source · line 83 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+max:U32 -> @r:Pair(S, U32) -> Step<P, S>
template next.start source · line 89 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+max:U32 -> @r:Pair(S, Bool) -> Step<P, S>
The two length fields are checked before the payload is waited for, so a damaged length is Bad and never a Torn tail that hides the frames after it.
template next.any source · line 97 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+max:U32 -> @r:Pair(S, Bool) -> Step<P, S>
template next source · line 106 · raw
@-P:Type -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @+max:U32 -> @s:S -> Step<P, S>
One frame from s. max caps a payload's length.
template recover.con source · line 109 · raw
@-a:Quant -> @-P:Kind(a) -> @-S:Type -> @p:P -> @r:Recovery<a, P, S> -> Recovery<a, P, S>
template recover.go source · line 115 · raw
@-a:Quant -> @-P:Kind(a) -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @n:Nat -> @+max:U32 -> @st:Step<P, S> -> Recovery<a, P, S>
Every frame from st on. Once n frames are taken, the next one is the last: the tail is Corrupt, and rest starts after it. Callers give n at least the frame count, so this never happens.
template recover source · line 135 · raw
@-a:Quant -> @-P:Kind(a) -> @-S:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @n:Nat -> @+max:U32 -> @s:S -> Recovery<a, P, S>
Every committed record of s, in order.
template replay.go source · line 139 · raw
@-P:Type -> @-S:Type -> @-A:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @-step:(@_:A -> @_:P -> A) -> @n:Nat -> @+max:U32 -> @st:Step<P, S> -> @acc:A -> Replay<A, S>
step folded over every frame from st on, without a list of the records. n as in recover.go.
template replay source · line 158 · raw
@-P:Type -> @-S:Type -> @-A:Type -> @-fits:(@_:S -> @+at:U32 -> @+n:U32 -> Pair(S, Bool)) -> @-u32:(@_:S -> @+at:U32 -> Pair(S, U32)) -> @-cut:(@_:S -> @+hs:U32 -> @+len:U32 -> Pair(S, P)) -> @-skip:(@_:S -> @+hs:U32 -> @+len:U32 -> S) -> @-sum:(@_:P -> Pair(P, U32)) -> @-step:(@_:A -> @_:P -> A) -> @n:Nat -> @+max:U32 -> @s:S -> @acc:A -> Replay<A, S>
template list.replay source · line 215 · raw
@-A:Type -> @-step:(@_:A -> @_:List<&2, U32> -> A) -> @n:Nat -> @+max:U32 -> @xs:List<&2, U32> -> @acc:A -> Replay<A, List<&2, U32>>
template replay.bytes source · line 276 · raw
@-A:Type -> @-step:(@_:A -> @_:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> A) -> @+max:U32 -> @b:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> @acc:A -> Replay<A, Cur>
step folded over every committed record of b, in order. rest.pos is where the committed prefix ends.
template open.read source · line 341 · raw
@-A:Type -> @-step:(@_:A -> @_:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> A) -> @r:Result<&1, &1, Pair(U32, String), Pair(File, Pair(U32, Array<U32>))> -> @+max:U32 -> @acc:A -> IO(Result<&1, &1, Pair(U32, String), Pair(Journal, A)>)
template open source · line 352 · raw
@-A:Type -> @-step:(@_:A -> @_:0x49814d83de8f70993a43e1002be29ecd/bytes.Bytes -> A) -> @path:String -> @+max:U32 -> @limit:U32 -> @acc:A -> IO(Result<&1, &1, Pair(U32, String), Pair(Journal, A)>)
Opens the journal at path and folds step over its committed records, from acc. A torn tail is cut off and fsynced before open answers. A corrupt frame fails with EINVAL and its offset; the file is left as it is. max caps a record's length; limit caps the file's size.
Effects (foreign code)
effect open.words source · line 293 · raw
@path:String -> @limit:U32 -> IO(Result<&1, &1, Pair(U32, String), Pair(File, Pair(U32, Array<U32>))>)
Opens path for reading and appending, creating it, and fsyncs its directory. Answers the file and its whole contents. Fails with EFBIG when the file holds more than limit octets.
foreign: effs/journal.c, effs/journal.js
effect append.words source · line 298 · raw
@file:File -> @len:U32 -> @words:Array<U32> -> IO(Pair(File, Result<&1, &1, Pair(U32, String), Unit>))
Writes len octets of words at the end of file, then fsyncs it.
foreign: effs/journal.c, effs/journal.js
effect truncate source · line 303 · raw
@file:File -> @len:U32 -> IO(Pair(File, Result<&1, &1, Pair(U32, String), Unit>))
Cuts file to len octets, then fsyncs it.
foreign: effs/journal.c, effs/journal.js