36 Input/output, networking, time, randomness, cryptography

36.1 Buffered output — forget to flush and translation refuses#

module buffered .
rem run: main

use outbuf .

proc main input out cap io . input al cap allocator . output u8 . effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 8 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  var p owned outbuf.pending be outbuf.buf_open 1 .
  let r1 result (owned outbuf.pending) outbuf.io_error be outbuf.buf_write out p buf "buffered " .
  guard is_ok r1 . else return 2 .
  var p2 owned outbuf.pending be ok_value r1 .
  let r2 result (owned outbuf.pending) outbuf.io_error be outbuf.buf_write out p2 buf "output\n" .
  guard is_ok r2 . else return 3 .
  var p3 owned outbuf.pending be ok_value r2 .
  let f result void outbuf.io_error be outbuf.buf_finish out p3 buf .
  guard is_ok f . else return 4 .
  return 0 .
end

$ lowentc --run main buffered.low
buffered output
main() = 0

• outbuf.buf_open 1 makes pending output to emit to standard output (1). It is owned outbuf.pending.
• outbuf.buf_write out p buf s gathers s into the buffer, emitting and continuing when the buffer fills. It takes a pending value and returns a new one (ownership moves along).
• outbuf.buf_finish emits the remaining bytes and ends the pending value.

The buffer is only 8 bytes, so it is flushed once partway through writing “buffered “. The output is the same. Gathering and emitting instead of write_out byte by byte is the value of buffering. Forget the final buf_finish and the bytes left in the buffer vanish. So translation refuses.

module unflushed .
rem expect: E-OWN-INCOMPLETE

use outbuf .

proc main input out cap io . input al cap allocator . output u8 . effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 64 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  var p owned outbuf.pending be outbuf.buf_open 1 .
  let r1 result (owned outbuf.pending) outbuf.io_error be outbuf.buf_write out p buf "lost?\n" .
  guard is_ok r1 . else return 2 .
  var p2 owned outbuf.pending be ok_value r1 .
  return 0 .
end

$ lowentc --check unflushed.low
14:0 E-OWN-INCOMPLETE: this value is dropped automatically at the end of scope — but the program itself declares an op that takes this type `owned` BY VALUE and returns a `result`: finishing it CAN FAIL. An automatic drop is a RELEASE (total, non-suspending), and it has nowhere to hand you that failure — it would SWALLOW it. A fallible finish (flush/commit/close) is a COMPLETION and must be EXPLICIT: call it and handle the `result`. If you really mean to discard the value and its failure, say so with `drop`. RFC-0058

buf_finish takes owned pending and returns a result, so pending is a type needing completion (chapter 19). The defect “the last line was not printed” shows before running.

36.2 Networking — handles are resources#

module loopback .
rem run: main

use net .

proc main input k cap net . input al cap allocator . output u8 . effects io alloc .
do
  let po option net.pair be net.pair_of k .
  guard is_some po . else return 1 .
  var p owned net.pair be some_value po .
  let sent option u64 be net.send_all k (net.pair_a p) "ping" .
  guard is_some sent . else return 2 .
  let g option mut slice u8 be alloc_bytes al capacity 16 .
  guard is_some g . else return 3 .
  let got option u64 be net.recv_once k (net.pair_b p) (some_value g) .
  let s result void net.net_error be net.shut_pair k p .
  guard is_some got . else return 4 .
  guard is_ok s . else return 5 .
  return narrow u8 (some_value got) .
end

$ lowentc --run main loopback.low
main() = 4

net.pair_of makes a pair of connections joined to each other within the process. “ping” is sent through one side (pair_a) and received on the other (pair_b), getting 4 bytes. net.shut_pair closes the pair. Closing can fail and gives a result.

net’s connections and listeners are resources like files’ handles. If sockets are not closed, a server runs out of descriptors the longer it runs. serve, dial and take open TCP loopback connections, and every op takes cap net as its first argument. The head shows that code not using this module cannot reach the network.

36.3 Randomness — reproducible sequences and operating-system entropy#

module dice .
rem run: roll 42
rem run: roll 42
rem run: roll 43

use random .

fn roll input seed u64 . output u64 .
do
  let s1 u64 be random.step seed .
  return add (random.below_biased s1 6) 1 .
end

$ lowentc --run roll dice.low 42
roll(42) = 3
$ lowentc --run roll dice.low 42
roll(42) = 3
$ lowentc --run roll dice.low 43
roll(43) = 5

random.step computes the next value from a seed. It is a pure fn with no capabilities or effects. Rolling twice with the same seed 42 gives 3 both times. Randomness that must be reproducible, as in simulations, tests and procedural generation, uses this.

Operating-system entropy is obtained with random.bytes k dst, which receives cap random. Randomness that must not be predictable, like keys and nonces, goes this way. The two jobs get different names and capabilities because merged, tests that must reproduce would depend on operating-system entropy, or conversely keys would come from a predictable sequence. below_biased is, as its name says, a biased range reduction. The name carries the meaning that it is not used where bias matters.

36.4 Time — monotonic clocks and wall clocks#

module timing .

use clock .

proc elapsed_work input k cap clock . output u64 . effects none .
do
  let start u64 be clock.now_ns k .
  var i u64 be 0 .
  var acc u64 be 0 .
  while lt i 1000 . do
    set acc (wrap_add acc i) .
    set i (add i 1) .
  end
  return clock.since_ns k start .
end

$ lowentc --check timing.low
== check: ok ==

clock.now_ns is a monotonic clock. It never goes backwards, so two readings can be subtracted (since_ns). It is not an absolute time. The wall clock (local_packed, year_of and so on) is the date and time people use, and it can go backwards with time zone changes or clock synchronisation. Measuring elapsed time with a wall clock can give negative numbers. The two make different promises, so the ops differ.

Reading a clock gives different answers for the same input, breaking determinism. That is why cap clock is needed. But it leaves no trace outside, so the effect is none (chapter 16). This example’s answer differs on each run, so this book’s verification script only checks it. sleep_ms waits, so it is the wait effect.

36.5 The HTTP request parser — its heart is rejection#

module request_line .
rem run: classify [71,69,84,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]
rem run: classify [66,82,69,87,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]

use http .

fn classify input req slice u8 . output u64 .
do
  let m u64 be http.method_code req .
  guard http.version_ok req . else return 99 .
  return m .
end

$ lowentc --run classify request_line.low [71,69,84,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]
classify([71,69,84,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]) = 1
  arg0 (written) = [71,69,84,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]
$ lowentc --run classify request_line.low [66,82,69,87,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]
classify([66,82,69,87,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]) = 0
  arg0 (written) = [66,82,69,87,32,47,32,72,84,84,80,47,49,46,49,13,10,13,10]

http.method_code gives a request’s method as a number (GET is 1), and http.version_ok answers whether the request line’s version is valid. The unknown method BREW is

0. The parser is pure computation and has no capabilities. Receiving bytes from a connection (net) and interpreting them (http) are different modules.

The design principle of this parser is not to accept ambiguous input. Request smuggling lives where servers and proxies accept an ambiguous request differently. Accepting leniently things like spaces in header names, duplicate length headers or malformed line endings creates that gap. This module does not build responses — it is the side that reads requests.

36.6 Cryptography — the order of the stack and the missing top#

The cryptographic modules are all pure computation (L0) and are stacked in layers towards TLS 1.3.

The top of each module document warns how it goes wrong when used alone. chacha is not safe alone (→ aead), aes used alone is usually wrong (→ gcm), poly’s key must be fresh per message, and gcm’s nonce must never repeat. Filtering small-order points for x25519 is the caller’s job. If you use cryptography, sealing starts from aead.

And the top does not exist yet. tlssrv performs the whole handshake but transport over real sockets is not there yet, and der is not a certificate infrastructure (PKI); certificates are received from outside. The principle of not pretending to have what does not exist matters most in cryptography.

36.7 Common mistakes#

module mistake_pendingmoved .
rem expect: E-OWN-MOVED

use outbuf .

proc main input out cap io . input al cap allocator . output u8 . effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 64 .
  guard is_some g . else return 1 .
  let buf mut slice u8 be some_value g .
  var p owned outbuf.pending be outbuf.buf_open 1 .
  let r1 result (owned outbuf.pending) outbuf.io_error be outbuf.buf_write out p buf "first\n" .
  guard is_ok r1 . else return 2 .
  rem ✘ writes again with the old pending value `p` that `write` took --- the new one is inside `r1`
  let r2 result (owned outbuf.pending) outbuf.io_error be outbuf.buf_write out p buf "second\n" .
  drop r2 .
  return 0 .
end

$ lowentc --check mistake_pendingmoved.low
mistake_pendingmoved.low:15:0 E-OWN-MOVED: this `owned` value was already MOVED (consumed) — using it again is use-after-move, which SPEC-004 §4.8 has always called a compile error and which nothing enforced. To keep using it, either CONSUME AND PUT IT BACK (`set <name> <new value>` re-initialises the place — that is how a handle threads through a loop), or borrow it LOCALLY with `ref h`. ☞ borrowing across an OP BOUNDARY is not lowered yet (E-IR-UNSUP says so at the call site), so `f (ref h)` is not a way out today

module mistake_sameseed .
rem run: two_rolls 2

use random .

rem ✘ both rolls start from the same seed --- the two dice always match
fn two_rolls input seed u64 . output u64 .
do
  let a u64 be add (random.below_biased (random.step seed) 6) 1 .
  let b u64 be add (random.below_biased (random.step seed) 6) 1 .
  return add (mul a 10) b .
end

$ lowentc --run two_rolls mistake_sameseed.low 2
two_rolls(2) = 55

module sameseed_fixed .
rem run: two_rolls 2

use random .

rem the next roll starts from the state the previous roll produced
fn two_rolls input seed u64 . output u64 .
do
  let s1 u64 be random.step seed .
  let s2 u64 be random.step s1 .
  let a u64 be add (random.below_biased s1 6) 1 .
  let b u64 be add (random.below_biased s2 6) 1 .
  return add (mul a 10) b .
end

$ lowentc --run two_rolls sameseed_fixed.low 2
two_rolls(2) = 56

module recv_partial .
rem run: main

use net .

proc main input k cap net . input al cap allocator . output u8 . effects io alloc .
do
  let po option net.pair be net.pair_of k .
  guard is_some po . else return 1 .
  var p owned net.pair be some_value po .
  let sent option u64 be net.send_all k (net.pair_a p) "ping pong" .
  guard is_some sent . else return 2 .
  rem nine bytes were sent, but the receive buffer has four slots --- one receive takes at most the buffer's size
  let g option mut slice u8 be alloc_bytes al capacity 4 .
  guard is_some g . else return 3 .
  let got option u64 be net.recv_once k (net.pair_b p) (some_value g) .
  let s result void net.net_error be net.shut_pair k p .
  drop s .
  guard is_some got . else return 4 .
  return narrow u8 (some_value got) .
end

$ lowentc --run main recv_partial.low
main() = 4

36.8 This chapter’s syntax at a glance#