Said once

Three copies, one layer

Every part that reads a disk, a frame or a request reads numbers out of bytes, and each wrote its own: sysf little-endian into words, sysk little-endian into bounded numbers, sysn big-endian, a mix of both. sysk also calls sysn's. sysl 001 takes them into one layer, sysl/bytes, with one name for each byte order, width and result; each part then drops its copy, in a change of its own. Pick a part.

The names

A read gives a word, the bits as they are; a number is an as away, and sysp knows its range: (as i64 (bytes-get-le32 b at)) is in [0, 2³²) with nothing more said. tests/callers.sysp restates every replaced function's contract this way, and make check proves it with the library.

The laws

Every binary format here is built from these gets and puts, so their laws are the ones every format's proof stands on (sysl 017, the first step of the suite's docs/research/formats.md). bytes-le32, bytes-le64, bytes-be16, bytes-be32 and bytes-be48 are spec functions (sysp 071), what the bytes at b[at, ...) say: the four-byte ones by constant shifts, the wider ones from them, so no proof sees a shift counted by a loop. Each get ensures it gives exactly that value. Each put ensures its bytes then say v, and bytes-same: every other byte is as it was. So a get after a put gives the put's value back, which tests/callers.sysp's was-put-get proves for every width with nothing named, in 4,394 units of z3's work.

The specs are opaque (sysp 093): in another file each is a value known only as equal where its arguments are, so a caller pays nothing for their bit operations, and has a get after a put by those two contracts alone. Not opaque, each was unfolded into every caller, and sysl's own host-step, which names none, went from 0.3M of z3's work to 190M. A caller still gains a line per get or put, one that tells z3 nothing, and that is enough to move a fragile query: sysn's ip-head went from 0.1M to 19M on a % over a word turned into a number, which sysp traced, and which bit operations on the word made robust (sysn 030). Puts into one buffer of a struct are cheap since sysp 097, which keeps the rest of the struct across each call: sysf's ds-snap-make, ten puts into the pool's cache, took 53M before it and 2.7M with it. A caller that writes beside a field and reads the field back sees no frame through the hidden values; when a format needs that, a lemma in bytes.sysp will state it from bytes-same. bytes-put-le64, two bytes-put-le32s, is the costliest at 6.7M, for carrying the low half past the high one's write; eight byte writes took 11M.

Text into a buffer

sysl 003 lifts the second layer, sysl/text, from sysk's lines and sysn's reports. Every function writes into a buffer from an offset and returns where the next byte goes, so calls chain, (text-dec t (text-bytes t k "n=") n), as Plan 9's seprint returns the end of what it printed. Nothing is written past the buffer's end, and what does not fit is left out as each says. sysk's lines keep their length in byte 0, so each line- function writes at one past it; tests/callers.sysp proves them so, and sysn's say-ip, which stays in sysn.

The hex digit is the layer's own, private; both parts' hex-digit go. sysk keeps its line format and its line- names, each a call of sysl now; sysn keeps say-ip, since only sysn writes addresses.

Numbers read from a buffer

sysl 012 begins the inverse, sysl/scan, with the decimal reader sysk had twice: sx-number in its s-expressions, up to six digits, and netd's tcp-number, a port. (scan-dec t at e max) reads t[at, e) as a number no greater than max, or answers -1 when the range is empty, holds a byte that is not a digit, or says more than max. Its contract says a number came only from digits. What stays each caller's is its format: six digits at most for an s-expression's number, a newline after a port and a port of 0 refused; tests/callers.sysp proves both callers' contracts over it.

Both sides say what the digits are worth (sysl 014). text-dec-value is the value of a slice of digits, the first the most significant, a spec function that calls itself (sysp 071), and text-digits says every byte of a slice is one. text-dec ensures what it wrote is digits whose value is n, the first not 0 unless n is: ACL2's three theorems for a printer, proven as SPARK proves GNAT's Image_Unsigned, the quotient not yet printed the reader's accumulator, with one assertion for the step where m's last digit leaves m / 10 one place up. scan-dec ensures its number is the value of the digits it read. And it never refuses digits whose value is within max (sysl 016), by two lemmas proven by induction (sysp 090): 10^k is at least 1, and digits have a value of at least 0. A third, scan-dec-step, says the number read so far, with the next digit, is no more than the whole, so the loop's refusal of a number over max is never a refusal of digits within it; kept apart, it leaves the loop none of the multiplication, and scan-dec proves in 3M of z3's work where it took 5.6M. So tests/callers.sysp proves the round trip, Candle's theorem for a printer: what text-dec wrote, scan-dec reads back as n.

A caller pays for none of this unless it asks. A spec function is unfolded only where a function names it (sysp 075); elsewhere it is a name, the same for the same slice, so sysn's reports, which call text-dec some forty-five times, prove as before (38M of z3 work, where unfolding everywhere took 977M). Two claims went to keep the callers cheap: that text-dec changes nothing beside what it writes, and that scan-dec's bytes were all digits, each stated with a forall that every caller carried (sysl 012). No caller used either.

The rules

What comes, and for whom