From b1e01eb3864ab32ab9bc0e7031c3e51afdde29fb Mon Sep 17 00:00:00 2001
From: Tony Garnock-Jones <tonyg@leastfixedpoint.com>
Date: Fri, 10 Jun 2022 17:49:08 +0200
Subject: [PATCH] preserves-binary-cheatsheet.md

---
 preserves-binary-cheatsheet.md | 52 ++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)
 create mode 100644 preserves-binary-cheatsheet.md

diff --git a/preserves-binary-cheatsheet.md b/preserves-binary-cheatsheet.md
new file mode 100644
index 0000000..9e5d9d8
--- /dev/null
+++ b/preserves-binary-cheatsheet.md
@@ -0,0 +1,52 @@
+---
+no_site_title: true
+title: "Preserves Cheatsheets"
+---
+
+Tony Garnock-Jones <tonyg@leastfixedpoint.com>  
+June 2022. Version 0.7.0.
+
+## Machine-Oriented Binary Syntax
+
+For a value `v`, we write `«v»` for the binary encoding of `v`.
+
+### Atoms
+
+                          «#f» = [0xA0]
+                          «#t» = [0xA1]
+           «F» when F ∈ Float  = [0xA2] ++ binary32(F)
+           «D» when D ∈ Double = [0xA2] ++ binary64(D)
+    «x» when x ∈ SignedInteger = [0xA3] ++ intbytes(x)
+                           «S» = [0xA4] ++ utf8(S)  if S ∈ String
+                                 [0xA5] ++ S        if S ∈ ByteString
+                                 [0xA6] ++ utf8(S)  if S ∈ Symbol
+
+`intbytes(x)` gives the big-endian two's-complement signed binary
+representation of `x`, taking exactly as many whole bytes as needed to
+unambiguously identify the value and its sign. `intbytes(0)` is the
+empty byte sequence.
+
+### Compounds
+
+               «<L F_1...F_m>» = [0xA7] ++ seq(«L», «F_1», ..., «F_m»)
+                 «[X_1...X_m]» = [0xA8] ++ seq(«X_1», ..., «X_m»)
+                «#{E_1...E_m}» = [0xA9] ++ seq(«E_1», ..., «E_m»)
+         «{K_1:V_1...K_m:V_m}» = [0xAA] ++ seq(«K_1», «V_1», ..., «K_m», «V_m»)
+
+    seq(R_1, ... R_m) = len(R_1) ++ R_1 ++...++ len(R_m) ++ R_m
+
+    len(m) = e(m, 128)
+           where e(v, d) = [v + d]                           if v < 128
+                           e(v / 128, 0) ++ [(v % 128) + d]  if v ≥ 128
+
+### Embeddeds
+
+                         «#!V» = [0xBF] ++ «V»
+
+### Annotations
+
+To annotate a `Repr` `r` (that *MUST NOT* itself already be annotated)
+with some sequence of `Value`s `[v_1, ..., v_m]`, surround `r` as
+follows:
+
+    [0xBE] ++ len(r) ++ r ++ len(v_1) ++ v_1 ++...++ len(v_m) ++ v_m