Something went wrong. Try again.
The Monad language. Dependent types, functional programming compiled with LLVM. Hobby project. monad-lang.org
dependent-types language compiler programming-language functional-programming
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477/// Wire framing: turning an accumulated byte stream into whole messages,/// for both protocols this toolkit's consumers speak.////// LSP frames a message as `Content-Length: N\r\n\r\n` followed by exactly/// N bytes of UTF-8 JSON. MCP frames it as one JSON value per line. The two/// differ only in where a message ends, which is why they share one outcome/// type rather than each growing their own reader.////// THE READER IS A PURE FUNCTION OVER AN ACCUMULATED BUFFER, and that is not/// a stylistic choice -- it is the whole reason this module exists. The/// natural first implementation is a loop: `read a line`, `parse the headers/// on it`, `read N more bytes`. It CANNOT survive a read that splits a/// header. A stream hands back whatever it has, so `read` routinely returns/// `"Content-Len"` with no newline anywhere in it, and a line-oriented reader/// has no answer for "the buffer is a strict prefix of a header" -- it must/// either block (never knowing how much more to ask for) or guess. The guess/// that looks reasonable, treating the partial line as a whole line, drops a/// message silently, and the failure shows up one request later as a/// desynchronized stream that reads like a client bug.////// Making the answer a VALUE removes the guess: `FrameRead.need_more` IS the/// partial case, so the caller's loop is "append what arrived, ask again",/// and there is nowhere for a partial frame to be lost. It also makes every/// one of those cases testable without a socket, which is how the header-split/// and terminator-inside-a-body tests below are written.////// The second half of the same hazard is a `\r\n\r\n` INSIDE a JSON string/// body -- entirely legal JSON, and a thing a client does the moment a user/// types a blank line into a document. `content_length` mode therefore parses/// the header first and then takes exactly the declared number of bytes; it/// never searches the buffer for a terminator that a body could also match./// A reader that scanned for the terminator instead would split that message/// in two, which is the same silent desynchronization by another route.////// Case sensitivity of the header name: matched EXACTLY, as/// `Content-Length:`. The LSP specification fixes that spelling and every/// mainstream client emits it that way, so case folding would be code with no/// caller. The choice is safe in the direction that matters -- a differently/// cased header does not silently mis-parse, it comes back as/// `FrameRead.bad_header`, which the server reports and logs.////// HOW MUCH MORE TO ASK FOR IS ALSO A VALUE, in `framing_needed`, and it is/// what keeps the caller's loop from costing a read per byte. The loop still/// reads "append what arrived, ask again", but the native underneath reads to/// a REQUESTED LENGTH rather than returning whatever is available, so a caller/// that always asks for one byte turns a large message into hundreds of/// syscalls while a caller that always asks for a large chunk blocks until the/// peer fills it -- which for a request/response protocol is a deadlock./// `framing_needed` separates the two cases that the buffer state actually/// distinguishes: `Option.none` while the header is still incomplete, and the/// outstanding byte count once `Content-Length` is known, so the read is one/// byte per header byte and then exactly the body in a single call.////// It NEVER answers zero, and that is a correctness rule rather than a/// rounding choice: an empty result IS the end-of-stream signal, so requesting/// zero bytes would be indistinguishable from the peer closing the connection/// and the caller would exit in the middle of a session. A frame that is/// already complete therefore reports a floor of one, which the caller/// re-examines before reading.////// The reader loop itself lives with its consumer, `motes/lsp/src/server.mo`.use toolkit::bytes { byte_cr, byte_lf, byte_space }/// How far into a buffer a `Content-Length` header may extend before it is/// treated as malformed rather than incomplete.////// This is a bound on WORK, not a protocol limit, and it is why the header/// scan can slice a window instead of converting the whole buffer: a real/// header is under a hundred bytes, so a terminator past this point is a/// broken peer (or something that is not speaking LSP at all), and reporting/// `bad_header` immediately beats scanning a megabyte looking for one.def header_window_max : I64 := 8192/// The ten ASCII digits, in value order. `digit_value` indexes this.def digit_chars : String := "0123456789"def content_length_header : String := "Content-Length:"/// Up to how large a `Content-Length` value is believed.////// The accumulator folds digits into an `I64`, so without a cap a peer/// declaring `Content-Length: 99999999999999999999` wraps the accumulator/// around to a small or negative number and the frame is accepted with the/// wrong length -- a desynchronization produced by a plausible typo rather/// than an attack. Any real message is far under this.def content_length_max : I64 := 100000000/// Which framing a stream uses. The two are not negotiated; a server knows/// which protocol it was started as.////// The name is `FramingMode` rather than the obvious `Framing` on purpose, and/// both halves of the reason are worth keeping. `motes/http/src/types.mo`/// already declares a `Framing` -- a different type, about a response's body/// length -- and it also names a constructor `content_length`, and it `open`s/// it, so within any file that imports HTTP the bare name `content_length`/// means HTTP's. Nothing compiles both motes today, which is why this is not/// an error anywhere and why it would go unnoticed until it is not:/// whole-program scope is shared, this repo has already lost an afternoon to/// two same-named inductives that broke codegen elaboration, and the failure/// flipped on module load order. The second half is that `mode` is what every/// caller already calls this value, so the qualified name says what the type/// is for rather than what module it happens to live in.pub type FramingMode { content_length, newline_delimited,}/// The result of offering an accumulated buffer to `framing_read`.////// `need_more` is a first-class answer rather than an error, because "the/// buffer is a strict prefix of a frame" is the normal state of a stream that/// has not finished delivering a message. `bad_header` is the opposite: the/// frame ended where it should but its header is unusable, which no amount of/// further reading fixes.pub type FrameRead { need_more, frame (body : String) (rest : String), bad_header (reason : String),}// --- Byte-level helpers ---//// Everything here works on `List U8` from `String.to_list` rather than on// `String.get`, for one reason: `String.get` is the O(1) byte read this would// prefer, but it is not `pub` in `init/src/string.mo`, and reaching across// motes for it draws a `cross_mote_package_private` warning on every check.// The alternative is not `String.get_char`, which decodes the whole string// into a `Vec<char>` on EVERY call and would make each of these loops// quadratic (its own doc says so). The conversions here are bounded: the// header scan converts at most `header_window_max` bytes, and the body is// never converted at all -- its length comes from `String.length`.def is_byte (o : Option U8) (b : U8) : Bool := match o { Option.none => false, Option.some x => U8.beq x b, }/// The digit `b` denotes, or -1 if it is not a digit.////// A scan of `digit_chars` rather than `U8.sub b 48u8`, and the reason is/// where the types stop. `U8.sub` IS `pub`, so the subtraction is available --/// but it yields a `U8`, and there is no way to widen a `U8` into an `I64`/// across a mote boundary: `U8` exposes `to_u64` and `to_u32` and neither is/// `pub` (`init/src/number.mo:259`, `:262`). Indexing a ten-character string/// answers the question directly, in the type the fold already accumulates.////// (`U8.gt` IS `pub` where `U8.lt` is not, so a range test could have been/// written here. It is not, because a range test gets no further than the/// subtraction above -- the value still has to come out as an `I64`.)#[partial]def digit_value (b : U8) : I64 := digit_value_go (String.to_list digit_chars) b 0#[partial]def digit_value_go (bs : List U8) (b : U8) (i : I64) : I64 := match bs { List.empty => -1, List.cons x rest => if U8.beq x b then i else digit_value_go rest b (I64.add i 1), }/// The index just past the first `\r\n\r\n` in `bs`, or -1 for none.////// Written as one flat recursion carrying the three preceding bytes rather/// than four nested matches, and the flattening is about how it compiles/// rather than how it reads: the previous byte of the match is the only state/// the search needs, so it travels as a parameter. `i` is the index of `b`,/// which is why the answer is `i + 1` -- the position after the `\n` that/// completes the terminator, which is also where the body begins.#[partial]def find_terminator (bs : List U8) (i : I64) (p1 : Option U8) (p2 : Option U8) (p3 : Option U8) : I64 := match bs { List.empty => -1, List.cons b rest => let hit : Bool := is_byte p3 byte_cr && is_byte p2 byte_lf && is_byte p1 byte_cr && U8.beq b byte_lf in if hit then I64.add i 1 else find_terminator rest (I64.add i 1) (Option.some b) p1 p2, }/// The index of the first `\n` in `bs`, or `Option.none` for none.#[partial]def find_lf (bs : List U8) (i : I64) : Option I64 := match bs { List.empty => Option.none, List.cons b rest => if U8.beq b byte_lf then Option.some i else find_lf rest (I64.add i 1), }/// Drop one trailing `\r` -- the carriage return of a line's `\r\n`.def trim_cr (line : String) : String := let n : I64 := String.length line in if I64.lt 0 n then if String.beq (String.slice line (n - 1) 1) "\r" then String.slice line 0 (n - 1) else line else line// --- The `Content-Length` header ---/// Reverse a list of header lines.////// Local rather than `List.reverse`, and the reason is where the name lives:/// `List.reverse` and `List.length` are defs in `std/src/list.mo`, and a/// framing module that pulls in `std` for four lines of list reversal has/// taken a dependency it will never use again. `init`'s `List` constructors/// and `String` primitives are all this module needs, and keeping it that way/// is what lets the tests below run against nothing but the prelude.#[partial]def framing_reverse_lines (ss : List String) (acc : List String) : List String := match ss { List.empty => acc, List.cons s rest => framing_reverse_lines rest (List.cons s acc), }/// Split a header region into its `\r\n`-separated lines.////// Flat recursion carrying the current line's start index, for the same/// reason `find_terminator` carries its previous byte: `start` is the only/// state a split needs, and holding it explicitly keeps every arm a/// single-level match. The region never contains a blank line -- it stops at/// the `\r\n\r\n` that terminated it -- so an empty trailing element is not a/// case here, and `trim_cr` handles the `\r` each line still carries.#[partial]pub def framing_header_lines (region : String) : List String := header_lines_go region (String.to_list region) 0 0 List.empty#[partial]def header_lines_go (region : String) (bs : List U8) (i : I64) (start : I64) (acc : List String) : List String := match bs { List.empty => framing_reverse_lines (List.cons (trim_cr (String.slice region start (i - start))) acc) List.empty, List.cons b rest => if U8.beq b byte_lf then header_lines_go region rest (I64.add i 1) (I64.add i 1) (List.cons (trim_cr (String.slice region start (i - start))) acc) else header_lines_go region rest (I64.add i 1) start acc, }/// The value of the `Content-Length` header, or `Option.none`.////// Stops at the FIRST line carrying the name, including when that line's/// value is unparseable. A file with the header twice is malformed, and/// falling through to a second one would accept a message whose length two/// parties disagree about -- which is the desynchronization this module is/// built to avoid, arrived at from the other direction.#[partial]def find_content_length (lines : List String) : Option I64 := match lines { List.empty => Option.none, List.cons l rest => if String.starts_with content_length_header l then parse_len (String.drop (String.length content_length_header) l) else find_content_length rest, }/// Every byte is a space.#[partial]def all_spaces (bs : List U8) : Bool := match bs { List.empty => true, List.cons b rest => if U8.beq b byte_space then all_spaces rest else false, }/// Read a decimal length out of everything after `Content-Length:`.////// STRICT about what else the value may contain, which the caller's/// consequences make non-negotiable rather than pedantic. Leading spaces are/// skipped, then digits are folded, then only spaces may follow. A lenient/// fold that stopped at the first non-digit would read `Content-Length: 0x10`/// as 0 and take no bytes, leaving 16 bytes of body in the buffer to be/// re-parsed as the next frame's header -- the desynchronization this module/// exists to prevent, entered through a header nobody validated. So a/// trailing non-digit is `Option.none`, and the caller reports it.////// `started` distinguishes "no digit seen yet" from "the value so far is 0",/// which is the one case a sentinel accumulator would get wrong:/// `Content-Length: 0` is a legal empty body, and `Content-Length:` with/// nothing after it is not a header at all.////// The unconsumed tail travels out with the number so the caller can inspect/// it: `Pair` rather than a second scan, because the fold already knows/// exactly where the digits stopped.#[partial]def parse_len (value : String) : Option I64 := match parse_len_go (String.to_list value) false 0 { Option.none => Option.none, Option.some p => match p { Pair.pair n tail => if all_spaces tail then Option.some n else Option.none, }, }#[partial]def parse_len_go (bs : List U8) (started : Bool) (acc : I64) : Option (Pair I64 (List U8)) := match bs { List.empty => if started then Option.some (Pair.pair acc List.empty) else Option.none, List.cons b rest => let d : I64 := digit_value b in if I64.lt d 0 then if started then Option.some (Pair.pair acc bs) else parse_len_go rest false acc else if I64.gt acc content_length_max then Option.none else parse_len_go rest true (I64.add (I64.mul acc 10) d), }// --- The two framings ---/// Offer an accumulated buffer to the reader.////// The contract every caller depends on: on `FrameRead.frame body rest`,/// `rest` is the unconsumed remainder and MUST be fed back in, because a/// client may pipeline. Dropping it loses every message that arrived in the/// same read as this one -- a burst that a fast client produces routinely.pub def framing_read (mode : FramingMode) (buf : String) : FrameRead := match mode { FramingMode.content_length => read_content_length buf, FramingMode.newline_delimited => read_newline_delimited buf, }#[partial]def read_content_length (buf : String) : FrameRead := let len : I64 := String.length buf in let window_len : I64 := if I64.lt len header_window_max then len else header_window_max in let window : String := String.slice buf 0 window_len in let after : I64 := find_terminator (String.to_list window) 0 Option.none Option.none Option.none in if I64.lt after 0 then // No terminator anywhere in the window. Under the window size that is a // partial header and the answer is to wait; AT the window size the header // cannot grow into a legal one, so waiting would hang on a broken peer. if I64.lt len header_window_max then FrameRead.need_more else FrameRead.bad_header "no header terminator within the window" else frame_after_header buf after/// Take the declared number of bytes after a located terminator.////// `after` is the index just past the `\r\n\r\n`, so the header region is/// exactly `[0, after - 4)` -- the four bytes of the terminator belong to/// neither the header nor the body.#[partial]def frame_after_header (buf : String) (after : I64) : FrameRead := let region : String := String.slice buf 0 (after - 4) in match find_content_length (framing_header_lines region) { Option.none => FrameRead.bad_header "missing or malformed Content-Length header", Option.some n => if I64.lt (String.length buf) (I64.add after n) then FrameRead.need_more else FrameRead.frame (String.slice buf after n) (String.drop (I64.add after n) buf), }/// A whole JSON value per line, which is MCP's framing.////// The buffer is rescanned from the start on every call, so feeding this one/// byte at a time is quadratic in the line's length. That is left alone/// deliberately: unlike the header scan there is no bound to slice to, since/// a legal message is however long it is, and the mode's messages are small/// and arrive whole off a local pipe. A stream that never sends a newline/// grows the buffer without limit, which is the protocol's own hazard -- MCP/// messages may not contain a raw newline, so framing them is exactly what/// this does and a peer that withholds one is the peer's bug.#[partial]def read_newline_delimited (buf : String) : FrameRead := match find_lf (String.to_list buf) 0 { Option.none => FrameRead.need_more, Option.some i => FrameRead.frame (trim_cr (String.slice buf 0 i)) (String.drop (I64.add i 1) buf), }// --- How much more is needed ---/// How many more bytes the buffer needs before it holds one whole frame, or/// `Option.none` when that number is not yet known.////// `framing_read` answering `need_more` covers two cases that cost a reader/// very different numbers of reads, and telling them apart is the whole reason/// this exists. A buffer whose HEADER is incomplete can only be extended by/// reading more and asking again -- nothing in it says how long the header will/// be -- so the honest read there is one byte, and the honest answer is/// `Option.none`. A buffer whose header IS complete names exactly how many body/// bytes are still outstanding, and the peer is going to send exactly that many,/// so the reader can take them in ONE read. A stream loop that could not ask/// this question would read a whole message one byte at a time, which is one/// syscall per byte of every message the client sends.////// NEVER ZERO, and the floor is not cosmetic: the caller's natural move is to/// read exactly this many bytes, and `read_stdin_exact 0` returns the empty/// string -- which is that native's end-of-stream signal. A zero here would make/// a caller that has not reached the end of anything exit the loop. The floor is/// 1 byte, which always either makes progress or reports the end truthfully.////// `Option.none` for `newline_delimited`, deliberately: a line has no declared/// length, so there is nothing to compute and a caller reads until the newline/// arrives. It is also `Option.none` for a buffer that is already a frame or is/// malformed, both of which `framing_read` answers on its own -- this is a/// question a caller asks only after being told `need_more`.#[partial]pub def framing_needed (mode : FramingMode) (buf : String) : Option I64 := match mode { FramingMode.content_length => needed_content_length buf, FramingMode.newline_delimited => Option.none, }/// The same header scan `read_content_length` runs, stopping at the point where/// the two cases diverge.#[partial]def needed_content_length (buf : String) : Option I64 := let len : I64 := String.length buf in let window_len : I64 := if I64.lt len header_window_max then len else header_window_max in let window : String := String.slice buf 0 window_len in let after : I64 := find_terminator (String.to_list window) 0 Option.none Option.none Option.none in if I64.lt after 0 then Option.none else needed_after_header buf after#[partial]def needed_after_header (buf : String) (after : I64) : Option I64 := let region : String := String.slice buf 0 (after - 4) in match find_content_length (framing_header_lines region) { Option.none => Option.none, Option.some n => let want : I64 := I64.sub (I64.add after n) (String.length buf) in if I64.lt want 1 then Option.some 1 else Option.some want, }// --- Test-only helpers ---//// The outcome type carries two payloads on one constructor and a reason// string on another, so a test cannot pattern-match its way to a body// without nesting differently-typed arms. These flatten it instead./// The body of a completed frame, or `Option.none` for either other outcome.pub def frame_body (r : FrameRead) : Option String := match r { FrameRead.need_more => Option.none, FrameRead.frame body _rest => Option.some body, FrameRead.bad_header _reason => Option.none, }/// What is left after a completed frame, or `Option.none` for either other/// outcome.pub def frame_rest (r : FrameRead) : Option String := match r { FrameRead.need_more => Option.none, FrameRead.frame _body rest => Option.some rest, FrameRead.bad_header _reason => Option.none, }/// The reason a header was rejected, or `Option.none` for either other/// outcome.pub def frame_reason (r : FrameRead) : Option String := match r { FrameRead.need_more => Option.none, FrameRead.frame _body _rest => Option.none, FrameRead.bad_header reason => Option.some reason, }pub def is_need_more (r : FrameRead) : Bool := match r { FrameRead.need_more => true, FrameRead.frame _body _rest => false, FrameRead.bad_header _reason => false, }